awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Lie.Weights.RootSystem
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 : IsKilling K L
inst_5 : FiniteDimensional K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H) L
α β : Weight K (↥H) L
hβ : β.IsNonZero
hα : ¬α.IsZero
h : (⇑β : (a : ↥H) → K) = HSMul.hSMul (α := K) (β := (a : ↥H) → K) (-1) (⇑α : (a : ↥H) → K)
⊢ β = -α ∨ β = α

Tactic:
exact .inl (by ext; rw [h, neg_one_smul]; rfl)
-- Module: Mathlib.Algebra.Lie.Weights.RootSystem
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 : IsKilling K L
inst_5 : FiniteDimensional K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H) L
α β : Weight K (↥H) L
hβ : β.IsNonZero
hα : ¬α.IsZero
h : (⇑β : (a : ↥H) → K) = HSMul.hSMul (α := K) (β := (a : ↥H) → K) 0 (⇑α : (a : ↥H) → K)
rwa rwa₁ rwa₂ rwa₃ : ∀ (h : Eq (α := (a : ↥H) → K) (⇑β : (a : ↥H) → K) 0), β.IsZero
⊢ β.IsZero

Tactic:
rwa [zero_smul] at h

Premises used: zero_smul
-- Module: Mathlib.Algebra.Lie.Weights.RootSystem
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 : IsKilling K L
inst_5 : FiniteDimensional K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H) L
α β : Weight K (↥H) L
hβ : β.IsNonZero
hα : ¬α.IsZero
h : (⇑β : (a : ↥H) → K) = HSMul.hSMul (α := K) (β := (a : ↥H) → K) 0 (⇑α : (a : ↥H) → K)
⊢ β = -α ∨ β = α

Tactic:
cases hβ (by rwa [zero_smul] at h)
-- Module: Mathlib.Algebra.Lie.Weights.RootSystem
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 : IsKilling K L
inst_5 : FiniteDimensional K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H) L
α β : Weight K (↥H) L
hβ : β.IsNonZero
hα : ¬α.IsZero
h : (⇑β : (a : ↥H) → K) = HSMul.hSMul (α := K) (β := (a : ↥H) → K) 1 (⇑α : (a : ↥H) → K)
h₁ : ∀ (x : ↥H), Eq.{u_1 + 1} (α := K) ((β : (a : ↥H) → K) x : K) ((α : (a : ↥H) → K) x : K)
⊢ β = α

Tactic:
ext
-- Module: Mathlib.Algebra.Lie.Weights.RootSystem
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 : IsKilling K L
inst_5 : FiniteDimensional K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H) L
α β : Weight K (↥H) L
hβ : β.IsNonZero
hα : ¬α.IsZero
h : (⇑β : (a : ↥H) → K) = HSMul.hSMul (α := K) (β := (a : ↥H) → K) 1 (⇑α : (a : ↥H) → K)
x : ↥H
h₁ : HSMul.hSMul (α := K) (β := (a : ↥H) → K) 1 (⇑α : (a : ↥H) → K) x = (α : (a : ↥H) → K) x
h₂ h₃ : Eq.{u_1 + 1} (α := K) ((α : (a : ↥H) → K) x : K) ((α : (a : ↥H) → K) x : K)
⊢ Eq.{u_1 + 1} (α := K) ((β : (a : ↥H) → K) x : K) ((α : (a : ↥H) → K) x : K)

Tactic:
rw [h, one_smul]

Premises used: one_smul
-- Module: Mathlib.Algebra.Lie.Weights.RootSystem
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 : IsKilling K L
inst_5 : FiniteDimensional K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H) L
α β : Weight K (↥H) L
hβ : β.IsNonZero
hα : ¬α.IsZero
h : (⇑β : (a : ↥H) → K) = HSMul.hSMul (α := K) (β := (a : ↥H) → K) 1 (⇑α : (a : ↥H) → K)
⊢ β = -α ∨ β = α

Tactic:
exact .inr (by ext; rw [h, one_smul])
-- Module: Mathlib.Algebra.Lie.Weights.RootSystem
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 : IsKilling K L
inst_5 : FiniteDimensional K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H) L
α_1 β_1 α β : Weight K (↥H) L
pos :
  ∀ (hα : α.IsZero),
    Ne (α := LieSubmodule K (↥H) L)
      (genWeightSpace L
        ((⇑β : (a : ↥H) → K) -
          HSMul.hSMul (α := K) (β := (a : ↥H) → K) ((β : (a : ↥H) → K) (coroot α) : K) (⇑α : (a : ↥H) → K)))
      ⊥
neg :
  ∀ (hα : ¬α.IsZero),
    Ne (α := LieSubmodule K (↥H) L)
      (genWeightSpace L
        ((⇑β : (a : ↥H) → K) -
          HSMul.hSMul (α := K) (β := (a : ↥H) → K) ((β : (a : ↥H) → K) (coroot α) : K) (⇑α : (a : ↥H) → K)))
      ⊥
⊢ Ne (α := LieSubmodule K (↥H) L)
    (genWeightSpace L
      ((⇑β : (a : ↥H) → K) -
        HSMul.hSMul (α := K) (β := (a : ↥H) → K) ((β : (a : ↥H) → K) (coroot α) : K) (⇑α : (a : ↥H) → K)))
    ⊥

Tactic:
by_cases hα : α.IsZero

Premises used: LieModule.Weight.IsZero
-- Module: Mathlib.Algebra.Lie.Weights.RootSystem
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 : IsKilling K L
inst_5 : FiniteDimensional K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H) L
α_1 β_1 α β : Weight K (↥H) L
hα : α.IsZero
⊢ Ne (α := LieSubmodule K (↥H) L)
    (genWeightSpace L
      ((⇑β : (a : ↥H) → K) -
        HSMul.hSMul (α := K) (β := (a : ↥H) → K) ((β : (a : ↥H) → K) (coroot α) : K) (⇑α : (a : ↥H) → K)))
    ⊥

Tactic:
simpa [hα.eq] using β.genWeightSpace_ne_bot

Premises used: LieModule.Weight.IsZero.eq, LieModule.Weight.genWeightSpace_ne_bot
-- Module: Mathlib.Algebra.Lie.Weights.RootSystem
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 : IsKilling K L
inst_5 : FiniteDimensional K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H) L
α_1 β_1 α β : Weight K (↥H) L
hα : ¬α.IsZero
neg :
  -HSub.hSub (α := ℤ) (↑(chainBotCoeff (⇑α : (a : ↥H) → K) β) : ℤ) (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ) ≤
      (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ) ∧
    - -HSub.hSub (α := ℤ) (↑(chainBotCoeff (⇑α : (a : ↥H) → K) β) : ℤ) (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ) ≤
      (↑(chainBotCoeff (⇑α : (a : ↥H) → K) β) : ℤ)
⊢ Ne (α := LieSubmodule K (↥H) L)
    (genWeightSpace L
      ((⇑β : (a : ↥H) → K) -
        HSMul.hSMul (α := K) (β := (a : ↥H) → K) ((β : (a : ↥H) → K) (coroot α) : K) (⇑α : (a : ↥H) → K)))
    ⊥

Tactic:
rw [sub_eq_neg_add, apply_coroot_eq_cast α β, ← neg_smul, ← Int.cast_neg,
      Int.cast_smul_eq_zsmul, rootSpace_zsmul_add_ne_bot_iff α β hα]

Premises used: Int.cast_neg, neg_smul, sub_eq_neg_add, LieAlgebra.IsKilling.apply_coroot_eq_cast, LieAlgebra.IsKilling.rootSpace_zsmul_add_ne_bot_iff, Int.cast_smul_eq_zsmul
-- Module: Mathlib.Algebra.Lie.Weights.RootSystem
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 : IsKilling K L
inst_5 : FiniteDimensional K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H) L
α_1 β_1 α β : Weight K (↥H) L
hα : ¬α.IsZero
⊢ -HSub.hSub (α := ℤ) (↑(chainBotCoeff (⇑α : (a : ↥H) → K) β) : ℤ) (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ) ≤
      (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ) ∧
    - -HSub.hSub (α := ℤ) (↑(chainBotCoeff (⇑α : (a : ↥H) → K) β) : ℤ) (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ) ≤
      (↑(chainBotCoeff (⇑α : (a : ↥H) → K) β) : ℤ)

Tactic:
lia
-- Module: Mathlib.Algebra.Lie.Weights.RootSystem
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 : IsKilling K L
inst_5 : FiniteDimensional K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H) L
α β : Weight K (↥H) L
hβ : β.IsNonZero
e : Weight.IsZero (reflectRoot α β : Weight K (↥H) L)
pos : ∀ (hα : α.IsZero), Eq.{u_1 + 1} (α := K) ((β : (a : ↥H) → K) (coroot α) : K) (0 : K)
neg : ∀ (hα : ¬α.IsZero), Eq.{u_1 + 1} (α := K) ((β : (a : ↥H) → K) (coroot α) : K) (0 : K)
⊢ Eq.{u_1 + 1} (α := K) ((β : (a : ↥H) → K) (coroot α) : K) (0 : K)

Tactic:
by_cases hα : α.IsZero

Premises used: LieModule.Weight.IsZero
-- Module: Mathlib.Algebra.Lie.Weights.RootSystem
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 : IsKilling K L
inst_5 : FiniteDimensional K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H) L
α β : Weight K (↥H) L
hβ : β.IsNonZero
e : Weight.IsZero (reflectRoot α β : Weight K (↥H) L)
hα : α.IsZero
⊢ Eq.{u_1 + 1} (α := K) ((β : (a : ↥H) → K) (coroot α) : K) (0 : K)

Tactic:
simp [coroot_eq_zero_iff.mpr hα]

Premises used: Iff.mpr, LieAlgebra.IsKilling.coroot_eq_zero_iff
-- Module: Mathlib.Algebra.Lie.Weights.RootSystem
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 : IsKilling K L
inst_5 : FiniteDimensional K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H) L
α β : Weight K (↥H) L
hβ : β.IsNonZero
e : Weight.IsZero (reflectRoot α β : Weight K (↥H) L)
hα : ¬α.IsZero
⊢ Eq.{u_1 + 1} (α := K) ((β : (a : ↥H) → K) (coroot α) : K) (0 : K)

Tactic:
simpa [root_apply_coroot hα, mul_two] using congr_fun (sub_eq_zero.mp e) (coroot α)

Premises used: sub_eq_zero, LieAlgebra.IsKilling.coroot, LieAlgebra.IsKilling.root_apply_coroot, Iff.mp, congr_fun, mul_two
-- Module: Mathlib.Algebra.Lie.Weights.RootSystem
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 : IsKilling K L
inst_5 : FiniteDimensional K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H) L
α β : Weight K (↥H) L
hβ : β.IsNonZero
e : Weight.IsZero (reflectRoot α β : Weight K (↥H) L)
⊢ Eq.{u_1 + 1} (α := K) ((β : (a : ↥H) → K) (coroot α) : K) (0 : K)

Tactic:
have : β (coroot α) = 0 := by
    by_cases hα : α.IsZero
    · simp [coroot_eq_zero_iff.mpr hα]
    simpa [root_apply_coroot hα, mul_two] using congr_fun (sub_eq_zero.mp e) (coroot α)
-- Module: Mathlib.Algebra.Lie.Weights.RootSystem
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 : IsKilling K L
inst_5 : FiniteDimensional K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H) L
α β : Weight K (↥H) L
hβ : β.IsNonZero
e : Weight.IsZero (reflectRoot α β : Weight K (↥H) L)
this : Eq.{u_1 + 1} (α := K) ((β : (a : ↥H) → K) (coroot α) : K) (0 : K)
h :
  ∀ (x : ↥H),
    Eq.{u_1 + 1} (α := K) (((reflectRoot α β : Weight K (↥H) L) : (a : ↥H) → K) x : K) ((β : (a : ↥H) → K) x : K)
⊢ reflectRoot α β = β

Tactic:
ext
-- Module: Mathlib.Algebra.Lie.Weights.RootSystem
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 : IsKilling K L
inst_5 : FiniteDimensional K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H) L
α β : Weight K (↥H) L
hβ : β.IsNonZero
e : Weight.IsZero (reflectRoot α β : Weight K (↥H) L)
this : Eq.{u_1 + 1} (α := K) ((β : (a : ↥H) → K) (coroot α) : K) (0 : K)
x : ↥H
⊢ Eq.{u_1 + 1} (α := K) (((reflectRoot α β : Weight K (↥H) L) : (a : ↥H) → K) x : K) ((β : (a : ↥H) → K) x : K)

Tactic:
simp [reflectRoot, this]

Premises used: LieAlgebra.IsKilling.reflectRoot
-- Module: Mathlib.Algebra.Lie.Weights.RootSystem
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 : IsKilling K L
inst_5 : FiniteDimensional K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H) L
α β : Weight K (↥H) L
hβ : β.IsNonZero
e : Weight.IsZero (reflectRoot α β : Weight K (↥H) L)
this : Eq.{u_1 + 1} (α := K) ((β : (a : ↥H) → K) (coroot α) : K) (0 : K)
⊢ reflectRoot α β = β

Tactic:
have : reflectRoot α β = β := by ext; simp [reflectRoot, this]
-- Module: Mathlib.Algebra.Lie.Weights.RootSystem
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 : IsKilling K L
inst_5 : FiniteDimensional K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H) L
α β : Weight K (↥H) L
hβ : β.IsNonZero
e : Weight.IsZero (reflectRoot α β : Weight K (↥H) L)
this_1 : Eq.{u_1 + 1} (α := K) ((β : (a : ↥H) → K) (coroot α) : K) (0 : K)
this : reflectRoot α β = β
⊢ False

Tactic:
hβ (this ▸ e)

Premises used: Eq.rec
-- Module: Mathlib.Algebra.Lie.Weights.RootSystem
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 : IsKilling K L
inst_5 : FiniteDimensional K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H) L
α β : Weight K (↥H) L
hβ : β.IsNonZero
e : Weight.IsZero (reflectRoot α β : Weight K (↥H) L)
this_1 : Eq.{u_1 + 1} (α := K) ((β : (a : ↥H) → K) (coroot α) : K) (0 : K)
this : reflectRoot α β = β
⊢ False

Tactic:
exact hβ (this ▸ e)

Premises used: Eq.rec
-- Module: Mathlib.Algebra.Lie.Weights.RootSystem
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 : IsKilling K L
inst_5 : FiniteDimensional K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H) L
α_1 β_1 : Weight K (↥H) L
α β : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))
h :
  Eq (α := Dual.{u_1, u_2} K ↥H)
    ((fun (x : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) ↦ Weight.toLinear K (↥H) L (↑x : Weight K (↥H) L)) α)
    ((fun (x : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) ↦ Weight.toLinear K (↥H) L (↑x : Weight K (↥H) L)) β)
a :
  ∀ (x : ↥H),
    Eq.{u_1 + 1} (α := K) (((↑α : Weight K (↥H) L) : (a : ↥H) → K) x : K)
      (((↑β : Weight K (↥H) L) : (a : ↥H) → K) x : K)
⊢ α = β

Tactic:
ext x
-- Module: Mathlib.Algebra.Lie.Weights.RootSystem
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 : IsKilling K L
inst_5 : FiniteDimensional K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H) L
α_1 β_1 : Weight K (↥H) L
α β : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))
h :
  Eq (α := Dual.{u_1, u_2} K ↥H)
    ((fun (x : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) ↦ Weight.toLinear K (↥H) L (↑x : Weight K (↥H) L)) α)
    ((fun (x : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) ↦ Weight.toLinear K (↥H) L (↑x : Weight K (↥H) L)) β)
x : ↥H
⊢ Eq.{u_1 + 1} (α := K) (((↑α : Weight K (↥H) L) : (a : ↥H) → K) x : K) (((↑β : Weight K (↥H) L) : (a : ↥H) → K) x : K)

Tactic:
simpa using LinearMap.congr_fun h x

Premises used: LinearMap.congr_fun
-- Module: Mathlib.Algebra.Lie.Weights.RootSystem
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 : IsKilling K L
inst_5 : FiniteDimensional K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H) L
α_1 β_1 α : Weight K (↥H) L
hα : Membership.mem (γ := Finset (Weight K (↥H) L)) (LieSubalgebra.root : Finset (Weight K (↥H) L)) α
β : Weight K (↥H) L
hβ : Membership.mem (γ := Finset (Weight K (↥H) L)) (LieSubalgebra.root : Finset (Weight K (↥H) L)) β
h :
  Function.comp (β := Weight K (↥H) L) (coroot : (α : Weight K (↥H) L) → ↥H)
      (Subtype.val (p := fun (x : Weight K (↥H) L) ↦
          Membership.mem (γ := Finset (Weight K (↥H) L)) (LieSubalgebra.root : Finset (Weight K (↥H) L)) x) :
        (self : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) → Weight K (↥H) L)
      (Subtype.mk (p := fun (x : Weight K (↥H) L) ↦
        Membership.mem (γ := Finset (Weight K (↥H) L)) (LieSubalgebra.root : Finset (Weight K (↥H) L)) x) α hα) =
    Function.comp (β := Weight K (↥H) L) (coroot : (α : Weight K (↥H) L) → ↥H)
      (Subtype.val (p := fun (x : Weight K (↥H) L) ↦
          Membership.mem (γ := Finset (Weight K (↥H) L)) (LieSubalgebra.root : Finset (Weight K (↥H) L)) x) :
        (self : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) → Weight K (↥H) L)
      (Subtype.mk (p := fun (x : Weight K (↥H) L) ↦
        Membership.mem (γ := Finset (Weight K (↥H) L)) (LieSubalgebra.root : Finset (Weight K (↥H) L)) x) β hβ)
⊢ Subtype.mk (p := fun (x : Weight K (↥H) L) ↦
      Membership.mem (γ := Finset (Weight K (↥H) L)) (LieSubalgebra.root : Finset (Weight K (↥H) L)) x) α hα =
    Subtype.mk (p := fun (x : Weight K (↥H) L) ↦
      Membership.mem (γ := Finset (Weight K (↥H) L)) (LieSubalgebra.root : Finset (Weight K (↥H) L)) x) β hβ

Tactic:
simpa using h
-- Module: Mathlib.Algebra.Lie.Weights.RootSystem
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 : IsKilling K L
inst_5 : FiniteDimensional K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H) L
α_1 β : Weight K (↥H) L
x : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))
α : Weight K (↥H) L
hα : Membership.mem (γ := Finset (Weight K (↥H) L)) (LieSubalgebra.root : Finset (Weight K (↥H) L)) α
⊢ α.IsNonZero

Tactic:
simpa using hα
-- Module: Mathlib.Algebra.Lie.Weights.RootSystem
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 : IsKilling K L
inst_5 : FiniteDimensional K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H) L
α_1 β : Weight K (↥H) L
x : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))
α : Weight K (↥H) L
hα : Membership.mem (γ := Finset (Weight K (↥H) L)) (LieSubalgebra.root : Finset (Weight K (↥H) L)) α
⊢ Eq.{u_1 + 1} (α := K)
    ((((LinearMap.id : (a : Dual K ↥H) → ↥H →ₗ[K] K)
              (({
                    toFun := fun (x : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) ↦
                      Weight.toLinear K (↥H) L (↑x : Weight K (↥H) L),
                    inj' := ⋯ } :
                  (a : ↥LieSubalgebra.root) → Dual K ↥H)
                (Subtype.mk (p := fun (x : Weight K (↥H) L) ↦
                  Membership.mem (γ := Finset (Weight K (↥H) L)) (LieSubalgebra.root : Finset (Weight K (↥H) L)) x) α
                  hα)) :
            LinearMap.{u_1, u_1, u_2, u_1} (RingHom.id K) (↥H) K) :
          (a : ↥H) → K)
        ((({
                  toFun :=
                    Function.comp (β := Weight K (↥H) L) (coroot : (α : Weight K (↥H) L) → ↥H)
                      (Subtype.val (p := fun (x : Weight K (↥H) L) ↦
                          Membership.mem (γ := Finset (Weight K (↥H) L)) (LieSubalgebra.root : Finset (Weight K (↥H) L))
                            x) :
                        (self : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) → Weight K (↥H) L),
                  inj' := ⋯ } :
                ↥(LieSubalgebra.root : Finset (Weight K (↥H) L)) ↪ ↥H) :
              (a : ↥LieSubalgebra.root) → ↥H)
            (Subtype.mk (p := fun (x : Weight K (↥H) L) ↦
              Membership.mem (γ := Finset (Weight K (↥H) L)) (LieSubalgebra.root : Finset (Weight K (↥H) L)) x) α hα) :
          ↥H) :
      K)
    (2 : K)

Tactic:
simpa using root_apply_coroot <| by simpa using hα

Premises used: LieAlgebra.IsKilling.root_apply_coroot
-- Module: Mathlib.Algebra.Lie.Weights.RootSystem
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 : IsKilling K L
inst_5 : FiniteDimensional K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H) L
α_1 β_1 α : Weight K (↥H) L
hα : Membership.mem (γ := Finset (Weight K (↥H) L)) (LieSubalgebra.root : Finset (Weight K (↥H) L)) α
β : Weight K (↥H) L
hβ : Membership.mem (γ := Finset (Weight K (↥H) L)) (LieSubalgebra.root : Finset (Weight K (↥H) L)) β
⊢ β.IsNonZero

Tactic:
simpa using hβ
-- Module: Mathlib.Algebra.Lie.Weights.RootSystem
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 : IsKilling K L
inst_5 : FiniteDimensional K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H) L
α_1 β_1 α : Weight K (↥H) L
hα : Membership.mem (γ := Finset (Weight K (↥H) L)) (LieSubalgebra.root : Finset (Weight K (↥H) L)) α
β : Weight K (↥H) L
hβ : Membership.mem (γ := Finset (Weight K (↥H) L)) (LieSubalgebra.root : Finset (Weight K (↥H) L)) β
⊢ Weight.IsNonZero (reflectRoot α β : Weight K (↥H) L)

Tactic:
simpa using reflectRoot_isNonZero α β <| by simpa using hβ

Premises used: LieAlgebra.IsKilling.reflectRoot_isNonZero
-- Module: Mathlib.Algebra.Lie.Weights.RootSystem
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 : IsKilling K L
inst_5 : FiniteDimensional K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H) L
α_1 β_1 α : Weight K (↥H) L
hα : Membership.mem (γ := Finset (Weight K (↥H) L)) (LieSubalgebra.root : Finset (Weight K (↥H) L)) α
β : Weight K (↥H) L
hβ : Membership.mem (γ := Finset (Weight K (↥H) L)) (LieSubalgebra.root : Finset (Weight K (↥H) L)) β
⊢ Membership.mem (α := Dual.{u_1, u_2} K ↥H) (γ := Set (Dual.{u_1, u_2} K ↥H))
    (Set.range (ι := ↥(LieSubalgebra.root : Finset (Weight K (↥H) L)))
      (⇑{
            toFun := fun (x : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) ↦
              Weight.toLinear K (↥H) L (↑x : Weight K (↥H) L),
            inj' := ⋯ } :
        (a : ↥LieSubalgebra.root) → Dual K ↥H))
    (((preReflection (R := K) (M := Dual.{u_1, u_2} K ↥H)
              (({
                      toFun := fun (x : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) ↦
                        Weight.toLinear K (↥H) L (↑x : Weight K (↥H) L),
                      inj' := ⋯ } :
                    (a : ↥LieSubalgebra.root) → Dual K ↥H)
                  (Subtype.mk (p := fun (x : Weight K (↥H) L) ↦
                    Membership.mem (γ := Finset (Weight K (↥H) L)) (LieSubalgebra.root : Finset (Weight K (↥H) L)) x) α
                    hα) :
                Dual.{u_1, u_2} K ↥H)
              ((LinearMap.flip LinearMap.id : (a : ↥H) → Dual K ↥H →ₗ[K] K)
                  ((({
                          toFun :=
                            Function.comp (β := Weight K (↥H) L) (coroot : (α : Weight K (↥H) L) → ↥H)
                              (Subtype.val (p := fun (x : Weight K (↥H) L) ↦
                                  Membership.mem (γ := Finset (Weight K (↥H) L))
                                    (LieSubalgebra.root : Finset (Weight K (↥H) L)) x) :
                                (self : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) → Weight K (↥H) L),
                          inj' := ⋯ } :
                        ↥(LieSubalgebra.root : Finset (Weight K (↥H) L)) ↪ ↥H) :
                      (a : ↥LieSubalgebra.root) → ↥H)
                    (Subtype.mk (p := fun (x : Weight K (↥H) L) ↦
                      Membership.mem (γ := Finset (Weight K (↥H) L)) (LieSubalgebra.root : Finset (Weight K (↥H) L)) x)
                      α hα)) :
                Dual.{u_1, u_2} K ↥H →ₗ[K] K) :
            End K (Dual.{u_1, u_2} K ↥H)) :
          (a : Dual K ↥H) → Dual K ↥H)
        (({
              toFun := fun (x : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) ↦
                Weight.toLinear K (↥H) L (↑x : Weight K (↥H) L),
              inj' := ⋯ } :
            (a : ↥LieSubalgebra.root) → Dual K ↥H)
          (Subtype.mk (p := fun (x : Weight K (↥H) L) ↦
            Membership.mem (γ := Finset (Weight K (↥H) L)) (LieSubalgebra.root : Finset (Weight K (↥H) L)) x) β hβ)) :
      Dual.{u_1, u_2} K ↥H)

Tactic:
simpa using
        ⟨reflectRoot α β, by simpa using reflectRoot_isNonZero α β <| by simpa using hβ, rfl⟩
-- Module: Mathlib.Algebra.Lie.Weights.RootSystem
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 : IsKilling K L
inst_5 : FiniteDimensional K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H) L
α β : Weight K (↥H) L
⊢ Eq (α := Submodule K (LinearMap.{u_1, u_1, u_2, u_1} (RingHom.id K) (↥H) K))
    (Submodule.span K (Set.image (α := Weight K (↥H) L) (Weight.toLinear K (↥H) L) {α : Weight K (↥H) L | α.IsNonZero}))
    ⊤

Tactic:
span_weight_isNonZero_eq_top K L H

Premises used: LieAlgebra.IsKilling.span_weight_isNonZero_eq_top