def IsInXi0_23_7 {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (rd : PositiveRootData Δ) (mu lam : ↥Δ.𝔥 →ₗ[R] R) : Prop

def WeylStabilizer_23_7 {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (wg : WeylGroupData Δ) (lam : ↥Δ.𝔥 →ₗ[R] R) : Set wg.W

def BruhatLE_23_7 {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (rd : PositiveRootData Δ) (mu nu : ↥Δ.𝔥 →ₗ[R] R) : Prop

def IsDominant_23_7 {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (rd : PositiveRootData Δ) (wg : WeylGroupData Δ) (lam : ↥Δ.𝔥 →ₗ[R] R) : Prop

structure IsProperRep_23_7 {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (rd : PositiveRootData Δ) (wg : WeylGroupData Δ) (mu lam : ↥Δ.𝔥 →ₗ[R] R) : Prop

• lam_dominant : IsDominant_23_7 rd wg lam
• in_xi0 : IsInXi0_23_7 rd mu lam
• mu_minimal (w : wg.W) : w ∈ WeylStabilizer_23_7 wg lam → BruhatLE_23_7 rd mu (wg.dualAction w mu)

def WeylOrbitPair_23_7 {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (wg : WeylGroupData Δ) (mu lam : ↥Δ.𝔥 →ₗ[R] R) : Set ((↥Δ.𝔥 →ₗ[R] R) × (↥Δ.𝔥 →ₗ[R] R))

structure BilinFormData_23_7 {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (wg : WeylGroupData Δ) [LE R] : Type u

• normSq : (↥Δ.𝔥 →ₗ[R] R) → R
• weyl_invariant (w : wg.W) (v : ↥Δ.𝔥 →ₗ[R] R) : self.normSq (wg.dualAction w v) = self.normSq v
• normSq_sub_weyl_invariant (w : wg.W) (a b : ↥Δ.𝔥 →ₗ[R] R) : self.normSq (wg.dualAction w a - wg.dualAction w b) = self.normSq (a - b)

structure SupportData_23_7 {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (wg : WeylGroupData Δ) : Type u

• support : Set ((↥Δ.𝔥 →ₗ[R] R) × (↥Δ.𝔥 →ₗ[R] R))
• weyl_equivariant (w : wg.W) (p : (↥Δ.𝔥 →ₗ[R] R) × (↥Δ.𝔥 →ₗ[R] R)) : p ∈ self.support → (wg.dualAction w p.1, wg.dualAction w p.2) ∈ self.support

def maximalSupport_23_7 {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} [LE R] {wg : WeylGroupData Δ} (B : BilinFormData_23_7 wg) (S : SupportData_23_7 wg) : Set ((↥Δ.𝔥 →ₗ[R] R) × (↥Δ.𝔥 →ₗ[R] R))

theorem theorem_20_13_bruhat_lower_bound {R : Type u} [CommRing R] [IsDomain R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (rd : PositiveRootData Δ) (wg : WeylGroupData Δ) (S : SupportData_23_7 wg) (mu lam phi : ↥Δ.𝔥 →ₗ[R] R) (_h_mu_in_S : (mu, lam) ∈ S.support) (_h_phi_in_S : (phi, lam) ∈ S.support) : BruhatLE_23_7 rd mu phi

theorem lemma_23_4_i_extracted {R : Type u} [CommRing R] [IsDomain R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (rd : PositiveRootData Δ) (wg : WeylGroupData Δ) [LinearOrder R] (B : BilinFormData_23_7 wg) (lam phi mu : ↥Δ.𝔥 →ₗ[R] R) (_hlam_dom : IsDominant_23_7 rd wg lam) (_hmu_le_phi : BruhatLE_23_7 rd mu phi) (_hphi_le_lam : BruhatLE_23_7 rd phi lam) : B.normSq (lam - phi) ≤ B.normSq (lam - mu)

theorem lemma_23_4_ii_extracted {R : Type u} [CommRing R] [IsDomain R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (rd : PositiveRootData Δ) (wg : WeylGroupData Δ) [LinearOrder R] (B : BilinFormData_23_7 wg) (lam phi mu : ↥Δ.𝔥 →ₗ[R] R) (_hlam_dom : IsDominant_23_7 rd wg lam) (_hmu_le_phi : BruhatLE_23_7 rd mu phi) (_hphi_le_lam : BruhatLE_23_7 rd phi lam) (_hnorm_eq : B.normSq (lam - phi) = B.normSq (lam - mu)) : ∃ w ∈ WeylStabilizer_23_7 wg lam, wg.dualAction w phi = mu

theorem support_in_xi0 {R : Type u} [CommRing R] [IsDomain R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (rd : PositiveRootData Δ) (wg : WeylGroupData Δ) (S : SupportData_23_7 wg) (mu lam : ↥Δ.𝔥 →ₗ[R] R) (_h_in_S : (mu, lam) ∈ S.support) : IsInXi0_23_7 rd mu lam

theorem support_decomposition {R : Type u} [CommRing R] [IsDomain R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (wg : WeylGroupData Δ) (S : SupportData_23_7 wg) (lam : ↥Δ.𝔥 →ₗ[R] R) (p : (↥Δ.𝔥 →ₗ[R] R) × (↥Δ.𝔥 →ₗ[R] R)) (_hp : p ∈ S.support) (_hblock : ∀ q ∈ S.support, ∃ (w : wg.W), q.2 = wg.dualAction w lam) : ∃ (w : wg.W) (phi : ↥Δ.𝔥 →ₗ[R] R), (phi, lam) ∈ S.support ∧ p = (wg.dualAction w phi, wg.dualAction w lam)

theorem theorem_20_13_upper_bound {R : Type u} [CommRing R] [IsDomain R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (rd : PositiveRootData Δ) (wg : WeylGroupData Δ) (S : SupportData_23_7 wg) (lam phi : ↥Δ.𝔥 →ₗ[R] R) (_h_in_S : (phi, lam) ∈ S.support) : BruhatLE_23_7 rd phi lam

theorem lemma_23_7_maximal_support {R : Type u} [CommRing R] [IsDomain R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (rd : PositiveRootData Δ) (wg : WeylGroupData Δ) [LinearOrder R] [IsStrictOrderedRing R] (B : BilinFormData_23_7 wg) (S : SupportData_23_7 wg) (mu lam : ↥Δ.𝔥 →ₗ[R] R) (hlam_dom : IsDominant_23_7 rd wg lam) (hmu_in_S : (mu, lam) ∈ S.support) (hmu_max : ∀ q ∈ S.support, B.normSq (q.2 - q.1) ≤ B.normSq (lam - mu)) (hblock : ∀ q ∈ S.support, ∃ (w : wg.W), q.2 = wg.dualAction w lam) : maximalSupport_23_7 B S = WeylOrbitPair_23_7 wg mu lam ∧ IsProperRep_23_7 rd wg mu lam