awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Lie.Weights.IsSimple
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : LieRing L
inst_3 : LieAlgebra K L
inst_4 : FiniteDimensional K L
inst_5 : IsKilling K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H) L
q : Submodule K (Dual.{u_1, u_2} K ↥H)
hq :
  ∀ (i : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
    q ∈ End.invtSubmodule (↑(RootPairing.reflection (rootSystem H) i) : Dual K ↥H →ₗ[K] Dual K ↥H)
χ : Weight K (↥H) L
x_χ m_α : L
hx_χ : Membership.mem (γ := LieSubmodule K (↥H) L) (genWeightSpace L (⇑χ : (a : ↥H) → K)) x_χ
α : Weight K (↥H) L
hαq : Weight.toLinear K (↥H) L α ∈ q
hα₀ : α.IsNonZero
w_plus : Weight.toLinear K (↥H) L χ + Weight.toLinear K (↥H) L α ≠ 0
w_minus : Weight.toLinear K (↥H) L χ - Weight.toLinear K (↥H) L α ≠ 0
w_chi : Weight.toLinear K (↥H) L χ ≠ 0
m_pos m_neg : L
y : ↥H
hy : Membership.mem (γ := LieIdeal K ↥H) (corootSpace (⇑α : (a : ↥H) → K)) y
h_bracket_sum : ⁅x_χ, m_α⁆ = ⁅x_χ, m_pos⁆ + ⁅x_χ, m_neg⁆ + ⁅x_χ, (↑y : L)⁆
h_pos_containment :
  Membership.mem (γ := LieSubmodule K (↥H) L)
    (genWeightSpace L (HAdd.hAdd (α := (a : ↥H) → K) (⇑χ : (a : ↥H) → K) (⇑α : (a : ↥H) → K))) ⁅x_χ, m_pos⁆
h_neg_containment :
  Membership.mem (γ := LieSubmodule K (↥H) L)
    (genWeightSpace L (HSub.hSub (α := (a : ↥H) → K) (⇑χ : (a : ↥H) → K) (⇑α : (a : ↥H) → K))) ⁅x_χ, m_neg⁆
h_chi_not_in_q : Weight.toLinear K (↥H) L χ ∉ q
S : RootPairing (↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) K (Dual.{u_1, u_2} K ↥H) ↥H := rootSystem H
exists_root_index :
  ∀ (γ : Weight K (↥H) L) (hγ : γ.IsNonZero),
    ∃ (i : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
      (S.root : (a : ↥LieSubalgebra.root) → Dual K ↥H) i = Weight.toLinear K (↥H) L γ
h_plus_bot :
  Eq (α := LieSubmodule K (↥H) L)
    (genWeightSpace L (⇑(Weight.toLinear K (↥H) L χ + Weight.toLinear K (↥H) L α) : (a : ↥H) → K)) ⊥
h_minus_bot :
  Eq (α := LieSubmodule K (↥H) L)
    (genWeightSpace L (⇑(Weight.toLinear K (↥H) L χ - Weight.toLinear K (↥H) L α) : (a : ↥H) → K)) ⊥
i : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))
hi : (S.root : (a : ↥LieSubalgebra.root) → Dual K ↥H) i = Weight.toLinear K (↥H) L χ
j : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))
hj : (S.root : (a : ↥LieSubalgebra.root) → Dual K ↥H) j = Weight.toLinear K (↥H) L α
⊢ S.pairing i j = 0

Tactic:
have h_pairing_zero : S.pairing i j = 0 := by
    apply RootPairing.pairing_eq_zero_of_add_notMem_of_sub_notMem S
    · intro h_eq; exact w_minus (by rw [← hi, ← hj, h_eq, sub_self])
    · intro h_eq; exact w_plus (by rw [← hi, ← hj, h_eq, neg_add_cancel])
    · intro ⟨idx, hidx⟩
      have : genWeightSpace L (S.root idx) ≠ ⊥ := idx.val.genWeightSpace_ne_bot
      rw [hidx, hi, hj] at this
      exact this h_plus_bot
    · intro ⟨idx, hidx⟩
      have : genWeightSpace L (S.root idx) ≠ ⊥ := idx.val.genWeightSpace_ne_bot
      rw [hidx, hi, hj] at this
      exact this h_minus_bot
-- Module: Mathlib.Algebra.Lie.Weights.IsSimple
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : LieRing L
inst_3 : LieAlgebra K L
inst_4 : FiniteDimensional K L
inst_5 : IsKilling K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H) L
q : Submodule K (Dual.{u_1, u_2} K ↥H)
hq :
  ∀ (i : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
    q ∈ End.invtSubmodule (↑(RootPairing.reflection (rootSystem H) i) : Dual K ↥H →ₗ[K] Dual K ↥H)
χ : Weight K (↥H) L
x_χ m_α : L
hx_χ : Membership.mem (γ := LieSubmodule K (↥H) L) (genWeightSpace L (⇑χ : (a : ↥H) → K)) x_χ
α : Weight K (↥H) L
hαq : Weight.toLinear K (↥H) L α ∈ q
hα₀ : α.IsNonZero
w_plus : Weight.toLinear K (↥H) L χ + Weight.toLinear K (↥H) L α ≠ 0
w_minus : Weight.toLinear K (↥H) L χ - Weight.toLinear K (↥H) L α ≠ 0
w_chi : Weight.toLinear K (↥H) L χ ≠ 0
m_pos m_neg : L
y : ↥H
hy : Membership.mem (γ := LieIdeal K ↥H) (corootSpace (⇑α : (a : ↥H) → K)) y
h_bracket_sum : ⁅x_χ, m_α⁆ = ⁅x_χ, m_pos⁆ + ⁅x_χ, m_neg⁆ + ⁅x_χ, (↑y : L)⁆
h_pos_containment :
  Membership.mem (γ := LieSubmodule K (↥H) L)
    (genWeightSpace L (HAdd.hAdd (α := (a : ↥H) → K) (⇑χ : (a : ↥H) → K) (⇑α : (a : ↥H) → K))) ⁅x_χ, m_pos⁆
h_neg_containment :
  Membership.mem (γ := LieSubmodule K (↥H) L)
    (genWeightSpace L (HSub.hSub (α := (a : ↥H) → K) (⇑χ : (a : ↥H) → K) (⇑α : (a : ↥H) → K))) ⁅x_χ, m_neg⁆
h_chi_not_in_q : Weight.toLinear K (↥H) L χ ∉ q
S : RootPairing (↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) K (Dual.{u_1, u_2} K ↥H) ↥H := rootSystem H
exists_root_index :
  ∀ (γ : Weight K (↥H) L) (hγ : γ.IsNonZero),
    ∃ (i : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
      (S.root : (a : ↥LieSubalgebra.root) → Dual K ↥H) i = Weight.toLinear K (↥H) L γ
h_plus_bot :
  Eq (α := LieSubmodule K (↥H) L)
    (genWeightSpace L (⇑(Weight.toLinear K (↥H) L χ + Weight.toLinear K (↥H) L α) : (a : ↥H) → K)) ⊥
h_minus_bot :
  Eq (α := LieSubmodule K (↥H) L)
    (genWeightSpace L (⇑(Weight.toLinear K (↥H) L χ - Weight.toLinear K (↥H) L α) : (a : ↥H) → K)) ⊥
i : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))
hi : (S.root : (a : ↥LieSubalgebra.root) → Dual K ↥H) i = Weight.toLinear K (↥H) L χ
j : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))
hj : (S.root : (a : ↥LieSubalgebra.root) → Dual K ↥H) j = Weight.toLinear K (↥H) L α
h_pairing_zero : S.pairing i j = 0
rw :
  Membership.mem (γ := LieSubmodule K (↥H) L)
    (genWeightSpace L (⇑(Weight.toLinear K (↥H) L χ + Weight.toLinear K (↥H) L α) : (a : ↥H) → K)) ⁅x_χ, m_pos⁆
⊢ Membership.mem (γ := LieSubmodule K (↥H) L) ⊥ ⁅x_χ, m_pos⁆

Tactic:
rw [← h_plus_bot]
-- Module: Mathlib.Algebra.Lie.Weights.IsSimple
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : LieRing L
inst_3 : LieAlgebra K L
inst_4 : FiniteDimensional K L
inst_5 : IsKilling K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H) L
q : Submodule K (Dual.{u_1, u_2} K ↥H)
hq :
  ∀ (i : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
    q ∈ End.invtSubmodule (↑(RootPairing.reflection (rootSystem H) i) : Dual K ↥H →ₗ[K] Dual K ↥H)
χ : Weight K (↥H) L
x_χ m_α : L
hx_χ : Membership.mem (γ := LieSubmodule K (↥H) L) (genWeightSpace L (⇑χ : (a : ↥H) → K)) x_χ
α : Weight K (↥H) L
hαq : Weight.toLinear K (↥H) L α ∈ q
hα₀ : α.IsNonZero
w_plus : Weight.toLinear K (↥H) L χ + Weight.toLinear K (↥H) L α ≠ 0
w_minus : Weight.toLinear K (↥H) L χ - Weight.toLinear K (↥H) L α ≠ 0
w_chi : Weight.toLinear K (↥H) L χ ≠ 0
m_pos m_neg : L
y : ↥H
hy : Membership.mem (γ := LieIdeal K ↥H) (corootSpace (⇑α : (a : ↥H) → K)) y
h_bracket_sum : ⁅x_χ, m_α⁆ = ⁅x_χ, m_pos⁆ + ⁅x_χ, m_neg⁆ + ⁅x_χ, (↑y : L)⁆
h_pos_containment :
  Membership.mem (γ := LieSubmodule K (↥H) L)
    (genWeightSpace L (HAdd.hAdd (α := (a : ↥H) → K) (⇑χ : (a : ↥H) → K) (⇑α : (a : ↥H) → K))) ⁅x_χ, m_pos⁆
h_neg_containment :
  Membership.mem (γ := LieSubmodule K (↥H) L)
    (genWeightSpace L (HSub.hSub (α := (a : ↥H) → K) (⇑χ : (a : ↥H) → K) (⇑α : (a : ↥H) → K))) ⁅x_χ, m_neg⁆
h_chi_not_in_q : Weight.toLinear K (↥H) L χ ∉ q
S : RootPairing (↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) K (Dual.{u_1, u_2} K ↥H) ↥H := rootSystem H
exists_root_index :
  ∀ (γ : Weight K (↥H) L) (hγ : γ.IsNonZero),
    ∃ (i : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
      (S.root : (a : ↥LieSubalgebra.root) → Dual K ↥H) i = Weight.toLinear K (↥H) L γ
h_plus_bot :
  Eq (α := LieSubmodule K (↥H) L)
    (genWeightSpace L (⇑(Weight.toLinear K (↥H) L χ + Weight.toLinear K (↥H) L α) : (a : ↥H) → K)) ⊥
h_minus_bot :
  Eq (α := LieSubmodule K (↥H) L)
    (genWeightSpace L (⇑(Weight.toLinear K (↥H) L χ - Weight.toLinear K (↥H) L α) : (a : ↥H) → K)) ⊥
i : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))
hi : (S.root : (a : ↥LieSubalgebra.root) → Dual K ↥H) i = Weight.toLinear K (↥H) L χ
j : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))
hj : (S.root : (a : ↥LieSubalgebra.root) → Dual K ↥H) j = Weight.toLinear K (↥H) L α
h_pairing_zero : S.pairing i j = 0
⊢ Membership.mem (γ := LieSubmodule K (↥H) L)
    (genWeightSpace L (⇑(Weight.toLinear K (↥H) L χ + Weight.toLinear K (↥H) L α) : (a : ↥H) → K)) ⁅x_χ, m_pos⁆

Tactic:
h_pos_containment

Premises used: Set.Mem, setOf
-- Module: Mathlib.Algebra.Lie.Weights.IsSimple
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : LieRing L
inst_3 : LieAlgebra K L
inst_4 : FiniteDimensional K L
inst_5 : IsKilling K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H) L
q : Submodule K (Dual.{u_1, u_2} K ↥H)
hq :
  ∀ (i : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
    q ∈ End.invtSubmodule (↑(RootPairing.reflection (rootSystem H) i) : Dual K ↥H →ₗ[K] Dual K ↥H)
χ : Weight K (↥H) L
x_χ m_α : L
hx_χ : Membership.mem (γ := LieSubmodule K (↥H) L) (genWeightSpace L (⇑χ : (a : ↥H) → K)) x_χ
α : Weight K (↥H) L
hαq : Weight.toLinear K (↥H) L α ∈ q
hα₀ : α.IsNonZero
w_plus : Weight.toLinear K (↥H) L χ + Weight.toLinear K (↥H) L α ≠ 0
w_minus : Weight.toLinear K (↥H) L χ - Weight.toLinear K (↥H) L α ≠ 0
w_chi : Weight.toLinear K (↥H) L χ ≠ 0
m_pos m_neg : L
y : ↥H
hy : Membership.mem (γ := LieIdeal K ↥H) (corootSpace (⇑α : (a : ↥H) → K)) y
h_bracket_sum : ⁅x_χ, m_α⁆ = ⁅x_χ, m_pos⁆ + ⁅x_χ, m_neg⁆ + ⁅x_χ, (↑y : L)⁆
h_pos_containment :
  Membership.mem (γ := LieSubmodule K (↥H) L)
    (genWeightSpace L (HAdd.hAdd (α := (a : ↥H) → K) (⇑χ : (a : ↥H) → K) (⇑α : (a : ↥H) → K))) ⁅x_χ, m_pos⁆
h_neg_containment :
  Membership.mem (γ := LieSubmodule K (↥H) L)
    (genWeightSpace L (HSub.hSub (α := (a : ↥H) → K) (⇑χ : (a : ↥H) → K) (⇑α : (a : ↥H) → K))) ⁅x_χ, m_neg⁆
h_chi_not_in_q : Weight.toLinear K (↥H) L χ ∉ q
S : RootPairing (↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) K (Dual.{u_1, u_2} K ↥H) ↥H := rootSystem H
exists_root_index :
  ∀ (γ : Weight K (↥H) L) (hγ : γ.IsNonZero),
    ∃ (i : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
      (S.root : (a : ↥LieSubalgebra.root) → Dual K ↥H) i = Weight.toLinear K (↥H) L γ
h_plus_bot :
  Eq (α := LieSubmodule K (↥H) L)
    (genWeightSpace L (⇑(Weight.toLinear K (↥H) L χ + Weight.toLinear K (↥H) L α) : (a : ↥H) → K)) ⊥
h_minus_bot :
  Eq (α := LieSubmodule K (↥H) L)
    (genWeightSpace L (⇑(Weight.toLinear K (↥H) L χ - Weight.toLinear K (↥H) L α) : (a : ↥H) → K)) ⊥
i : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))
hi : (S.root : (a : ↥LieSubalgebra.root) → Dual K ↥H) i = Weight.toLinear K (↥H) L χ
j : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))
hj : (S.root : (a : ↥LieSubalgebra.root) → Dual K ↥H) j = Weight.toLinear K (↥H) L α
h_pairing_zero : S.pairing i j = 0
⊢ Membership.mem (γ := LieSubmodule K (↥H) L)
    (genWeightSpace L (⇑(Weight.toLinear K (↥H) L χ + Weight.toLinear K (↥H) L α) : (a : ↥H) → K)) ⁅x_χ, m_pos⁆

Tactic:
exact h_pos_containment
-- Module: Mathlib.Algebra.Lie.Weights.IsSimple
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : LieRing L
inst_3 : LieAlgebra K L
inst_4 : FiniteDimensional K L
inst_5 : IsKilling K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H) L
q : Submodule K (Dual.{u_1, u_2} K ↥H)
hq :
  ∀ (i : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
    q ∈ End.invtSubmodule (↑(RootPairing.reflection (rootSystem H) i) : Dual K ↥H →ₗ[K] Dual K ↥H)
χ : Weight K (↥H) L
x_χ m_α : L
hx_χ : Membership.mem (γ := LieSubmodule K (↥H) L) (genWeightSpace L (⇑χ : (a : ↥H) → K)) x_χ
α : Weight K (↥H) L
hαq : Weight.toLinear K (↥H) L α ∈ q
hα₀ : α.IsNonZero
w_plus : Weight.toLinear K (↥H) L χ + Weight.toLinear K (↥H) L α ≠ 0
w_minus : Weight.toLinear K (↥H) L χ - Weight.toLinear K (↥H) L α ≠ 0
w_chi : Weight.toLinear K (↥H) L χ ≠ 0
m_pos m_neg : L
y : ↥H
hy : Membership.mem (γ := LieIdeal K ↥H) (corootSpace (⇑α : (a : ↥H) → K)) y
h_bracket_sum : ⁅x_χ, m_α⁆ = ⁅x_χ, m_pos⁆ + ⁅x_χ, m_neg⁆ + ⁅x_χ, (↑y : L)⁆
h_pos_containment :
  Membership.mem (γ := LieSubmodule K (↥H) L)
    (genWeightSpace L (HAdd.hAdd (α := (a : ↥H) → K) (⇑χ : (a : ↥H) → K) (⇑α : (a : ↥H) → K))) ⁅x_χ, m_pos⁆
h_neg_containment :
  Membership.mem (γ := LieSubmodule K (↥H) L)
    (genWeightSpace L (HSub.hSub (α := (a : ↥H) → K) (⇑χ : (a : ↥H) → K) (⇑α : (a : ↥H) → K))) ⁅x_χ, m_neg⁆
h_chi_not_in_q : Weight.toLinear K (↥H) L χ ∉ q
S : RootPairing (↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) K (Dual.{u_1, u_2} K ↥H) ↥H := rootSystem H
exists_root_index :
  ∀ (γ : Weight K (↥H) L) (hγ : γ.IsNonZero),
    ∃ (i : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
      (S.root : (a : ↥LieSubalgebra.root) → Dual K ↥H) i = Weight.toLinear K (↥H) L γ
h_plus_bot :
  Eq (α := LieSubmodule K (↥H) L)
    (genWeightSpace L (⇑(Weight.toLinear K (↥H) L χ + Weight.toLinear K (↥H) L α) : (a : ↥H) → K)) ⊥
h_minus_bot :
  Eq (α := LieSubmodule K (↥H) L)
    (genWeightSpace L (⇑(Weight.toLinear K (↥H) L χ - Weight.toLinear K (↥H) L α) : (a : ↥H) → K)) ⊥
i : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))
hi : (S.root : (a : ↥LieSubalgebra.root) → Dual K ↥H) i = Weight.toLinear K (↥H) L χ
j : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))
hj : (S.root : (a : ↥LieSubalgebra.root) → Dual K ↥H) j = Weight.toLinear K (↥H) L α
h_pairing_zero : S.pairing i j = 0
⊢ Membership.mem (γ := LieSubmodule K (↥H) L) ⊥ ⁅x_χ, m_pos⁆

Tactic:
have h_in_bot : ⁅x_χ, m_pos⁆ ∈ (⊥ : LieSubmodule K H L) := by
      rw [← h_plus_bot]
      exact h_pos_containment
-- Module: Mathlib.Algebra.Lie.Weights.IsSimple
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : LieRing L
inst_3 : LieAlgebra K L
inst_4 : FiniteDimensional K L
inst_5 : IsKilling K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H) L
q : Submodule K (Dual.{u_1, u_2} K ↥H)
hq :
  ∀ (i : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
    q ∈ End.invtSubmodule (↑(RootPairing.reflection (rootSystem H) i) : Dual K ↥H →ₗ[K] Dual K ↥H)
χ : Weight K (↥H) L
x_χ m_α : L
hx_χ : Membership.mem (γ := LieSubmodule K (↥H) L) (genWeightSpace L (⇑χ : (a : ↥H) → K)) x_χ
α : Weight K (↥H) L
hαq : Weight.toLinear K (↥H) L α ∈ q
hα₀ : α.IsNonZero
w_plus : Weight.toLinear K (↥H) L χ + Weight.toLinear K (↥H) L α ≠ 0
w_minus : Weight.toLinear K (↥H) L χ - Weight.toLinear K (↥H) L α ≠ 0
w_chi : Weight.toLinear K (↥H) L χ ≠ 0
m_pos m_neg : L
y : ↥H
hy : Membership.mem (γ := LieIdeal K ↥H) (corootSpace (⇑α : (a : ↥H) → K)) y
h_bracket_sum : ⁅x_χ, m_α⁆ = ⁅x_χ, m_pos⁆ + ⁅x_χ, m_neg⁆ + ⁅x_χ, (↑y : L)⁆
h_pos_containment :
  Membership.mem (γ := LieSubmodule K (↥H) L)
    (genWeightSpace L (HAdd.hAdd (α := (a : ↥H) → K) (⇑χ : (a : ↥H) → K) (⇑α : (a : ↥H) → K))) ⁅x_χ, m_pos⁆
h_neg_containment :
  Membership.mem (γ := LieSubmodule K (↥H) L)
    (genWeightSpace L (HSub.hSub (α := (a : ↥H) → K) (⇑χ : (a : ↥H) → K) (⇑α : (a : ↥H) → K))) ⁅x_χ, m_neg⁆
h_chi_not_in_q : Weight.toLinear K (↥H) L χ ∉ q
S : RootPairing (↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) K (Dual.{u_1, u_2} K ↥H) ↥H := rootSystem H
exists_root_index :
  ∀ (γ : Weight K (↥H) L) (hγ : γ.IsNonZero),
    ∃ (i : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
      (S.root : (a : ↥LieSubalgebra.root) → Dual K ↥H) i = Weight.toLinear K (↥H) L γ
h_plus_bot :
  Eq (α := LieSubmodule K (↥H) L)
    (genWeightSpace L (⇑(Weight.toLinear K (↥H) L χ + Weight.toLinear K (↥H) L α) : (a : ↥H) → K)) ⊥
h_minus_bot :
  Eq (α := LieSubmodule K (↥H) L)
    (genWeightSpace L (⇑(Weight.toLinear K (↥H) L χ - Weight.toLinear K (↥H) L α) : (a : ↥H) → K)) ⊥
i : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))
hi : (S.root : (a : ↥LieSubalgebra.root) → Dual K ↥H) i = Weight.toLinear K (↥H) L χ
j : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))
hj : (S.root : (a : ↥LieSubalgebra.root) → Dual K ↥H) j = Weight.toLinear K (↥H) L α
h_pairing_zero : S.pairing i j = 0
h_in_bot : Membership.mem (γ := LieSubmodule K (↥H) L) ⊥ ⁅x_χ, m_pos⁆
rwa rwa₁ rwa₂ rwa₃ : ∀ (h_in_bot : ⁅x_χ, m_pos⁆ = 0), ⁅x_χ, m_pos⁆ = 0
⊢ ⁅x_χ, m_pos⁆ = 0

Tactic:
rwa [LieSubmodule.mem_bot] at h_in_bot

Premises used: LieSubmodule.mem_bot
-- Module: Mathlib.Algebra.Lie.Weights.IsSimple
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : LieRing L
inst_3 : LieAlgebra K L
inst_4 : FiniteDimensional K L
inst_5 : IsKilling K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H) L
q : Submodule K (Dual.{u_1, u_2} K ↥H)
hq :
  ∀ (i : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
    q ∈ End.invtSubmodule (↑(RootPairing.reflection (rootSystem H) i) : Dual K ↥H →ₗ[K] Dual K ↥H)
χ : Weight K (↥H) L
x_χ m_α : L
hx_χ : Membership.mem (γ := LieSubmodule K (↥H) L) (genWeightSpace L (⇑χ : (a : ↥H) → K)) x_χ
α : Weight K (↥H) L
hαq : Weight.toLinear K (↥H) L α ∈ q
hα₀ : α.IsNonZero
w_plus : Weight.toLinear K (↥H) L χ + Weight.toLinear K (↥H) L α ≠ 0
w_minus : Weight.toLinear K (↥H) L χ - Weight.toLinear K (↥H) L α ≠ 0
w_chi : Weight.toLinear K (↥H) L χ ≠ 0
m_pos m_neg : L
y : ↥H
hy : Membership.mem (γ := LieIdeal K ↥H) (corootSpace (⇑α : (a : ↥H) → K)) y
h_bracket_sum : ⁅x_χ, m_α⁆ = ⁅x_χ, m_pos⁆ + ⁅x_χ, m_neg⁆ + ⁅x_χ, (↑y : L)⁆
h_pos_containment :
  Membership.mem (γ := LieSubmodule K (↥H) L)
    (genWeightSpace L (HAdd.hAdd (α := (a : ↥H) → K) (⇑χ : (a : ↥H) → K) (⇑α : (a : ↥H) → K))) ⁅x_χ, m_pos⁆
h_neg_containment :
  Membership.mem (γ := LieSubmodule K (↥H) L)
    (genWeightSpace L (HSub.hSub (α := (a : ↥H) → K) (⇑χ : (a : ↥H) → K) (⇑α : (a : ↥H) → K))) ⁅x_χ, m_neg⁆
h_chi_not_in_q : Weight.toLinear K (↥H) L χ ∉ q
S : RootPairing (↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) K (Dual.{u_1, u_2} K ↥H) ↥H := rootSystem H
exists_root_index :
  ∀ (γ : Weight K (↥H) L) (hγ : γ.IsNonZero),
    ∃ (i : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
      (S.root : (a : ↥LieSubalgebra.root) → Dual K ↥H) i = Weight.toLinear K (↥H) L γ
h_plus_bot :
  Eq (α := LieSubmodule K (↥H) L)
    (genWeightSpace L (⇑(Weight.toLinear K (↥H) L χ + Weight.toLinear K (↥H) L α) : (a : ↥H) → K)) ⊥
h_minus_bot :
  Eq (α := LieSubmodule K (↥H) L)
    (genWeightSpace L (⇑(Weight.toLinear K (↥H) L χ - Weight.toLinear K (↥H) L α) : (a : ↥H) → K)) ⊥
i : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))
hi : (S.root : (a : ↥LieSubalgebra.root) → Dual K ↥H) i = Weight.toLinear K (↥H) L χ
j : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))
hj : (S.root : (a : ↥LieSubalgebra.root) → Dual K ↥H) j = Weight.toLinear K (↥H) L α
h_pairing_zero : S.pairing i j = 0
⊢ ⁅x_χ, m_pos⁆ = 0

Tactic:
have h_pos_zero : ⁅x_χ, m_pos⁆ = 0 := by
    have h_in_bot : ⁅x_χ, m_pos⁆ ∈ (⊥ : LieSubmodule K H L) := by
      rw [← h_plus_bot]
      exact h_pos_containment
    rwa [LieSubmodule.mem_bot] at h_in_bot
-- Module: Mathlib.Algebra.Lie.Weights.IsSimple
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : LieRing L
inst_3 : LieAlgebra K L
inst_4 : FiniteDimensional K L
inst_5 : IsKilling K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H) L
q : Submodule K (Dual.{u_1, u_2} K ↥H)
hq :
  ∀ (i : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
    q ∈ End.invtSubmodule (↑(RootPairing.reflection (rootSystem H) i) : Dual K ↥H →ₗ[K] Dual K ↥H)
χ : Weight K (↥H) L
x_χ m_α : L
hx_χ : Membership.mem (γ := LieSubmodule K (↥H) L) (genWeightSpace L (⇑χ : (a : ↥H) → K)) x_χ
α : Weight K (↥H) L
hαq : Weight.toLinear K (↥H) L α ∈ q
hα₀ : α.IsNonZero
w_plus : Weight.toLinear K (↥H) L χ + Weight.toLinear K (↥H) L α ≠ 0
w_minus : Weight.toLinear K (↥H) L χ - Weight.toLinear K (↥H) L α ≠ 0
w_chi : Weight.toLinear K (↥H) L χ ≠ 0
m_pos m_neg : L
y : ↥H
hy : Membership.mem (γ := LieIdeal K ↥H) (corootSpace (⇑α : (a : ↥H) → K)) y
h_bracket_sum : ⁅x_χ, m_α⁆ = ⁅x_χ, m_pos⁆ + ⁅x_χ, m_neg⁆ + ⁅x_χ, (↑y : L)⁆
h_pos_containment :
  Membership.mem (γ := LieSubmodule K (↥H) L)
    (genWeightSpace L (HAdd.hAdd (α := (a : ↥H) → K) (⇑χ : (a : ↥H) → K) (⇑α : (a : ↥H) → K))) ⁅x_χ, m_pos⁆
h_neg_containment :
  Membership.mem (γ := LieSubmodule K (↥H) L)
    (genWeightSpace L (HSub.hSub (α := (a : ↥H) → K) (⇑χ : (a : ↥H) → K) (⇑α : (a : ↥H) → K))) ⁅x_χ, m_neg⁆
h_chi_not_in_q : Weight.toLinear K (↥H) L χ ∉ q
S : RootPairing (↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) K (Dual.{u_1, u_2} K ↥H) ↥H := rootSystem H
exists_root_index :
  ∀ (γ : Weight K (↥H) L) (hγ : γ.IsNonZero),
    ∃ (i : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
      (S.root : (a : ↥LieSubalgebra.root) → Dual K ↥H) i = Weight.toLinear K (↥H) L γ
h_plus_bot :
  Eq (α := LieSubmodule K (↥H) L)
    (genWeightSpace L (⇑(Weight.toLinear K (↥H) L χ + Weight.toLinear K (↥H) L α) : (a : ↥H) → K)) ⊥
h_minus_bot :
  Eq (α := LieSubmodule K (↥H) L)
    (genWeightSpace L (⇑(Weight.toLinear K (↥H) L χ - Weight.toLinear K (↥H) L α) : (a : ↥H) → K)) ⊥
i : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))
hi : (S.root : (a : ↥LieSubalgebra.root) → Dual K ↥H) i = Weight.toLinear K (↥H) L χ
j : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))
hj : (S.root : (a : ↥LieSubalgebra.root) → Dual K ↥H) j = Weight.toLinear K (↥H) L α
h_pairing_zero : S.pairing i j = 0
h_pos_zero : ⁅x_χ, m_pos⁆ = 0
rw :
  Membership.mem (γ := LieSubmodule K (↥H) L)
    (genWeightSpace L (⇑(Weight.toLinear K (↥H) L χ - Weight.toLinear K (↥H) L α) : (a : ↥H) → K)) ⁅x_χ, m_neg⁆
⊢ Membership.mem (γ := LieSubmodule K (↥H) L) ⊥ ⁅x_χ, m_neg⁆

Tactic:
rw [← h_minus_bot]
-- Module: Mathlib.Algebra.Lie.Weights.IsSimple
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : LieRing L
inst_3 : LieAlgebra K L
inst_4 : FiniteDimensional K L
inst_5 : IsKilling K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H) L
q : Submodule K (Dual.{u_1, u_2} K ↥H)
hq :
  ∀ (i : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
    q ∈ End.invtSubmodule (↑(RootPairing.reflection (rootSystem H) i) : Dual K ↥H →ₗ[K] Dual K ↥H)
χ : Weight K (↥H) L
x_χ m_α : L
hx_χ : Membership.mem (γ := LieSubmodule K (↥H) L) (genWeightSpace L (⇑χ : (a : ↥H) → K)) x_χ
α : Weight K (↥H) L
hαq : Weight.toLinear K (↥H) L α ∈ q
hα₀ : α.IsNonZero
w_plus : Weight.toLinear K (↥H) L χ + Weight.toLinear K (↥H) L α ≠ 0
w_minus : Weight.toLinear K (↥H) L χ - Weight.toLinear K (↥H) L α ≠ 0
w_chi : Weight.toLinear K (↥H) L χ ≠ 0
m_pos m_neg : L
y : ↥H
hy : Membership.mem (γ := LieIdeal K ↥H) (corootSpace (⇑α : (a : ↥H) → K)) y
h_bracket_sum : ⁅x_χ, m_α⁆ = ⁅x_χ, m_pos⁆ + ⁅x_χ, m_neg⁆ + ⁅x_χ, (↑y : L)⁆
h_pos_containment :
  Membership.mem (γ := LieSubmodule K (↥H) L)
    (genWeightSpace L (HAdd.hAdd (α := (a : ↥H) → K) (⇑χ : (a : ↥H) → K) (⇑α : (a : ↥H) → K))) ⁅x_χ, m_pos⁆
h_neg_containment :
  Membership.mem (γ := LieSubmodule K (↥H) L)
    (genWeightSpace L (HSub.hSub (α := (a : ↥H) → K) (⇑χ : (a : ↥H) → K) (⇑α : (a : ↥H) → K))) ⁅x_χ, m_neg⁆
h_chi_not_in_q : Weight.toLinear K (↥H) L χ ∉ q
S : RootPairing (↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) K (Dual.{u_1, u_2} K ↥H) ↥H := rootSystem H
exists_root_index :
  ∀ (γ : Weight K (↥H) L) (hγ : γ.IsNonZero),
    ∃ (i : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
      (S.root : (a : ↥LieSubalgebra.root) → Dual K ↥H) i = Weight.toLinear K (↥H) L γ
h_plus_bot :
  Eq (α := LieSubmodule K (↥H) L)
    (genWeightSpace L (⇑(Weight.toLinear K (↥H) L χ + Weight.toLinear K (↥H) L α) : (a : ↥H) → K)) ⊥
h_minus_bot :
  Eq (α := LieSubmodule K (↥H) L)
    (genWeightSpace L (⇑(Weight.toLinear K (↥H) L χ - Weight.toLinear K (↥H) L α) : (a : ↥H) → K)) ⊥
i : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))
hi : (S.root : (a : ↥LieSubalgebra.root) → Dual K ↥H) i = Weight.toLinear K (↥H) L χ
j : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))
hj : (S.root : (a : ↥LieSubalgebra.root) → Dual K ↥H) j = Weight.toLinear K (↥H) L α
h_pairing_zero : S.pairing i j = 0
h_pos_zero : ⁅x_χ, m_pos⁆ = 0
⊢ Membership.mem (γ := LieSubmodule K (↥H) L)
    (genWeightSpace L (⇑(Weight.toLinear K (↥H) L χ - Weight.toLinear K (↥H) L α) : (a : ↥H) → K)) ⁅x_χ, m_neg⁆

Tactic:
h_neg_containment

Premises used: Set.Mem, setOf