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
inst_8 : Nontrivial L
hα : α.IsNonZero
⊢ chainBotCoeff.{u_1, u_2, u_2} (R := K) (L := ↥H) (M := L) (⇑α : (a : ↥H) → K) 0 = 1

Tactic:
chainTopCoeff_zero_right (-α) hα.neg

Premises used: LieModule.Weight.IsNonZero.neg, LieModule.chainBotCoeff, LieAlgebra.IsKilling.chainTopCoeff_zero_right, Neg.neg
-- 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
inst_8 : Nontrivial L
hα : α.IsNonZero
rw :
  chainBotCoeff.{u_1, u_2, u_2} (R := K) (L := ↥H) (M := L) (⇑α : (a : ↥H) → K) 0 +
      chainTopCoeff.{u_1, u_2, u_2} (R := K) (L := ↥H) (M := L) (⇑α : (a : ↥H) → K) 0 =
    2
rw₁ : chainBotCoeff.{u_1, u_2, u_2} (R := K) (L := ↥H) (M := L) (⇑α : (a : ↥H) → K) 0 + 1 = 2
rw₂ rw₃ : HAdd.hAdd (α := ℕ) 1 1 = 2
⊢ chainLength α 0 = 2

Tactic:
rw [← chainBotCoeff_add_chainTopCoeff, chainTopCoeff_zero_right α hα,
    chainBotCoeff_zero_right α hα]

Premises used: LieAlgebra.IsKilling.chainTopCoeff_zero_right, LieAlgebra.IsKilling.chainBotCoeff_zero_right, LieAlgebra.IsKilling.chainBotCoeff_add_chainTopCoeff
-- 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
inl : Subsingleton L → rootSpace H (HSMul.hSMul (α := ℕ) (β := (a : ↥H) → K) 2 (⇑α : (a : ↥H) → K)) = ⊥
inr : Nontrivial L → rootSpace H (HSMul.hSMul (α := ℕ) (β := (a : ↥H) → K) 2 (⇑α : (a : ↥H) → K)) = ⊥
⊢ rootSpace H (HSMul.hSMul (α := ℕ) (β := (a : ↥H) → K) 2 (⇑α : (a : ↥H) → K)) = ⊥

Tactic:
cases subsingleton_or_nontrivial L

Premises used: subsingleton_or_nontrivial
-- 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 : Subsingleton L
⊢ rootSpace H (HSMul.hSMul (α := ℕ) (β := (a : ↥H) → K) 2 (⇑α : (a : ↥H) → K)) = ⊥

Tactic:
IsEmpty.elim inferInstance α

Premises used: IsEmpty.elim, inferInstance
-- 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 : Subsingleton L
⊢ rootSpace H (HSMul.hSMul (α := ℕ) (β := (a : ↥H) → K) 2 (⇑α : (a : ↥H) → K)) = ⊥

Tactic:
exact IsEmpty.elim inferInstance α
-- 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 : Nontrivial L
⊢ rootSpace H (HSMul.hSMul (α := ℕ) (β := (a : ↥H) → K) 2 (⇑α : (a : ↥H) → K)) = ⊥

Tactic:
simpa [chainTopCoeff_zero_right α hα] using
    genWeightSpace_chainTopCoeff_add_one_nsmul_add α (0 : Weight K H L) hα

Premises used: LieAlgebra.IsKilling.chainTopCoeff_zero_right, LieModule.genWeightSpace_chainTopCoeff_add_one_nsmul_add, OfNat.ofNat, DFunLike.coe
-- 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
by_contra : ∀ (h : ¬rootSpace H (HSMul.hSMul (α := K) (β := (a : ↥H) → K) 2⁻¹ (⇑α : (a : ↥H) → K)) = ⊥), False
⊢ rootSpace H (HSMul.hSMul (α := K) (β := (a : ↥H) → K) 2⁻¹ (⇑α : (a : ↥H) → K)) = ⊥

Tactic:
by_contra 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 : ¬rootSpace H (HSMul.hSMul (α := K) (β := (a : ↥H) → K) 2⁻¹ (⇑α : (a : ↥H) → K)) = ⊥
W : Weight K (↥H) L :=
  { toFun := HSMul.hSMul (α := K) (β := (a : ↥H) → K) 2⁻¹ (⇑α : (a : ↥H) → K), genWeightSpace_ne_bot' := h }
change : HSMul.hSMul (α := ℕ) 2 (HSMul.hSMul (α := K) (β := (a : ↥H) → K) 2⁻¹ (⇑α : (a : ↥H) → K)) = (⇑α : (a : ↥H) → K)
⊢ HSMul.hSMul (α := ℕ) (β := (a : ↥H) → K) 2 (⇑W : (a : ↥H) → K) = (⇑α : (a : ↥H) → K)

Tactic:
change 2 • (2⁻¹ : K) • (α : H → K) = α

Premises used: Inv.inv, OfNat.ofNat, DFunLike.coe
-- 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 : ¬rootSpace H (HSMul.hSMul (α := K) (β := (a : ↥H) → K) 2⁻¹ (⇑α : (a : ↥H) → K)) = ⊥
W : Weight K (↥H) L :=
  { toFun := HSMul.hSMul (α := K) (β := (a : ↥H) → K) 2⁻¹ (⇑α : (a : ↥H) → K), genWeightSpace_ne_bot' := h }
rw : HSMul.hSMul (β := (a : ↥H) → K) (HMul.hMul (α := K) (↑2 : K) 2⁻¹) (⇑α : (a : ↥H) → K) = (⇑α : (a : ↥H) → K)
⊢ HSMul.hSMul (α := ℕ) 2 (HSMul.hSMul (α := K) (β := (a : ↥H) → K) 2⁻¹ (⇑α : (a : ↥H) → K)) = (⇑α : (a : ↥H) → K)

Tactic:
rw [← Nat.cast_smul_eq_nsmul K, smul_smul]

Premises used: smul_smul, Nat.cast_smul_eq_nsmul
-- 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 : ¬rootSpace H (HSMul.hSMul (α := K) (β := (a : ↥H) → K) 2⁻¹ (⇑α : (a : ↥H) → K)) = ⊥
W : Weight K (↥H) L :=
  { toFun := HSMul.hSMul (α := K) (β := (a : ↥H) → K) 2⁻¹ (⇑α : (a : ↥H) → K), genWeightSpace_ne_bot' := h }
⊢ HSMul.hSMul (β := (a : ↥H) → K) (HMul.hMul (α := K) (↑2 : K) 2⁻¹) (⇑α : (a : ↥H) → K) = (⇑α : (a : ↥H) → K)

Tactic:
simp
-- 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 : ¬rootSpace H (HSMul.hSMul (α := K) (β := (a : ↥H) → K) 2⁻¹ (⇑α : (a : ↥H) → K)) = ⊥
W : Weight K (↥H) L :=
  { toFun := HSMul.hSMul (α := K) (β := (a : ↥H) → K) 2⁻¹ (⇑α : (a : ↥H) → K), genWeightSpace_ne_bot' := h }
⊢ HSMul.hSMul (α := ℕ) (β := (a : ↥H) → K) 2 (⇑W : (a : ↥H) → K) = (⇑α : (a : ↥H) → K)

Tactic:
have hW : 2 • (W : H → K) = α := by
    change 2 • (2⁻¹ : K) • (α : H → K) = α
    rw [← Nat.cast_smul_eq_nsmul K, smul_smul]; simp
-- 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 : ¬rootSpace H (HSMul.hSMul (α := K) (β := (a : ↥H) → K) 2⁻¹ (⇑α : (a : ↥H) → K)) = ⊥
W : Weight K (↥H) L :=
  { toFun := HSMul.hSMul (α := K) (β := (a : ↥H) → K) 2⁻¹ (⇑α : (a : ↥H) → K), genWeightSpace_ne_bot' := h }
hW : HSMul.hSMul (α := ℕ) (β := (a : ↥H) → K) 2 (⇑W : (a : ↥H) → K) = (⇑α : (a : ↥H) → K)
apply : Eq (α := LieSubmodule K (↥H) L) (genWeightSpace L (⇑α : (a : ↥H) → K)) ⊥
⊢ False

Tactic:
apply α.genWeightSpace_ne_bot

Premises used: 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
α : Weight K (↥H) L
hα : α.IsNonZero
h : ¬rootSpace H (HSMul.hSMul (α := K) (β := (a : ↥H) → K) 2⁻¹ (⇑α : (a : ↥H) → K)) = ⊥
W : Weight K (↥H) L :=
  { toFun := HSMul.hSMul (α := K) (β := (a : ↥H) → K) 2⁻¹ (⇑α : (a : ↥H) → K), genWeightSpace_ne_bot' := h }
hW : HSMul.hSMul (α := ℕ) (β := (a : ↥H) → K) 2 (⇑W : (a : ↥H) → K) = (⇑α : (a : ↥H) → K)
e : Eq (α := (a : ↥H) → K) (⇑W : (a : ↥H) → K) 0
⊢ HSMul.hSMul (α := ℕ) (β := (a : ↥H) → K) 2 (⇑W : (a : ↥H) → K) = HSMul.hSMul (α := ℕ) (β := (a : ↥H) → K) 2 0

Tactic:
apply_fun (2 • ·) at e

Premises used: HSMul.hSMul, OfNat.ofNat
-- 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 : ¬rootSpace H (HSMul.hSMul (α := K) (β := (a : ↥H) → K) 2⁻¹ (⇑α : (a : ↥H) → K)) = ⊥
W : Weight K (↥H) L :=
  { toFun := HSMul.hSMul (α := K) (β := (a : ↥H) → K) 2⁻¹ (⇑α : (a : ↥H) → K), genWeightSpace_ne_bot' := h }
hW : HSMul.hSMul (α := ℕ) (β := (a : ↥H) → K) 2 (⇑W : (a : ↥H) → K) = (⇑α : (a : ↥H) → K)
e : HSMul.hSMul (α := ℕ) (β := (a : ↥H) → K) 2 (⇑W : (a : ↥H) → K) = HSMul.hSMul (α := ℕ) (β := (a : ↥H) → K) 2 0
⊢ α.IsZero

Tactic:
simpa [hW] using e
-- 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 : ¬rootSpace H (HSMul.hSMul (α := K) (β := (a : ↥H) → K) 2⁻¹ (⇑α : (a : ↥H) → K)) = ⊥
W : Weight K (↥H) L :=
  { toFun := HSMul.hSMul (α := K) (β := (a : ↥H) → K) 2⁻¹ (⇑α : (a : ↥H) → K), genWeightSpace_ne_bot' := h }
hW : HSMul.hSMul (α := ℕ) (β := (a : ↥H) → K) 2 (⇑W : (a : ↥H) → K) = (⇑α : (a : ↥H) → K)
⊢ rootSpace H (HSMul.hSMul (α := ℕ) (β := (a : ↥H) → K) 2 (⇑W : (a : ↥H) → K)) = ⊥

Tactic:
have := rootSpace_two_smul W (fun (e : (W : H → K) = 0) ↦ hα <| by
    apply_fun (2 • ·) at e; simpa [hW] using e)
-- 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 : ¬rootSpace H (HSMul.hSMul (α := K) (β := (a : ↥H) → K) 2⁻¹ (⇑α : (a : ↥H) → K)) = ⊥
W : Weight K (↥H) L :=
  { toFun := HSMul.hSMul (α := K) (β := (a : ↥H) → K) 2⁻¹ (⇑α : (a : ↥H) → K), genWeightSpace_ne_bot' := h }
hW : HSMul.hSMul (α := ℕ) (β := (a : ↥H) → K) 2 (⇑W : (a : ↥H) → K) = (⇑α : (a : ↥H) → K)
this : rootSpace H (HSMul.hSMul (α := ℕ) (β := (a : ↥H) → K) 2 (⇑W : (a : ↥H) → K)) = ⊥
rwa rwa₁ rwa₂ rwa₃ :
  ∀ (this : rootSpace H (⇑α : (a : ↥H) → K) = ⊥),
    Eq (α := LieSubmodule K (↥H) L) (genWeightSpace L (⇑α : (a : ↥H) → K)) ⊥
⊢ Eq (α := LieSubmodule K (↥H) L) (genWeightSpace L (⇑α : (a : ↥H) → K)) ⊥

Tactic:
rwa [hW] at 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
k : K
h : (⇑β : (a : ↥H) → K) = HSMul.hSMul (β := (a : ↥H) → K) k (⇑α : (a : ↥H) → K)
inl : Subsingleton L → k = -1 ∨ k = 0 ∨ k = 1
inr : Nontrivial L → k = -1 ∨ k = 0 ∨ k = 1
⊢ k = -1 ∨ k = 0 ∨ k = 1

Tactic:
cases subsingleton_or_nontrivial L

Premises used: subsingleton_or_nontrivial
-- 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
k : K
h : (⇑β : (a : ↥H) → K) = HSMul.hSMul (β := (a : ↥H) → K) k (⇑α : (a : ↥H) → K)
h_1 : Subsingleton L
⊢ k = -1 ∨ k = 0 ∨ k = 1

Tactic:
IsEmpty.elim inferInstance α

Premises used: IsEmpty.elim, inferInstance
-- 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
k : K
h : (⇑β : (a : ↥H) → K) = HSMul.hSMul (β := (a : ↥H) → K) k (⇑α : (a : ↥H) → K)
h_1 : Subsingleton L
⊢ k = -1 ∨ k = 0 ∨ k = 1

Tactic:
exact IsEmpty.elim inferInstance α
-- 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
k : K
h : (⇑β : (a : ↥H) → K) = HSMul.hSMul (β := (a : ↥H) → K) k (⇑α : (a : ↥H) → K)
h_1 : Nontrivial L
⊢ Eq.{u_1 + 1} (α := K) ((β : (a : ↥H) → K) (coroot α) : K)
    ((↑((↑(chainLength α β) : ℤ) - HMul.hMul (α := ℤ) 2 (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ)) : K) : K)

Tactic:
have H := apply_coroot_eq_cast' α β
-- 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_1 : LieSubalgebra K L
inst_6 : H_1.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H_1) L
α β : Weight K (↥H_1) L
hα : α.IsNonZero
k : K
h : (⇑β : (a : ↥H_1) → K) = HSMul.hSMul (β := (a : ↥H_1) → K) k (⇑α : (a : ↥H_1) → K)
h_1 : Nontrivial L
H :
  Eq.{u_1 + 1} (α := K) ((β : (a : ↥H_1) → K) (coroot α) : K)
    ((↑((↑(chainLength α β) : ℤ) - HMul.hMul (α := ℤ) 2 (↑(chainTopCoeff (⇑α : (a : ↥H_1) → K) β) : ℤ)) : K) : K)
⊢ HSMul.hSMul (β := (a : ↥H_1) → K) k (⇑α : (a : ↥H_1) → K) (coroot α) =
    (↑((↑(chainLength α β) : ℤ) - HMul.hMul (α := ℤ) 2 (↑(chainTopCoeff (⇑α : (a : ↥H_1) → K) β) : ℤ)) : K)

Tactic:
rw [h] 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_1 : LieSubalgebra K L
inst_6 : H_1.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H_1) L
α β : Weight K (↥H_1) L
hα : α.IsNonZero
k : K
h : (⇑β : (a : ↥H_1) → K) = HSMul.hSMul (β := (a : ↥H_1) → K) k (⇑α : (a : ↥H_1) → K)
h_1 : Nontrivial L
H :
  HSMul.hSMul (β := (a : ↥H_1) → K) k (⇑α : (a : ↥H_1) → K) (coroot α) =
    (↑((↑(chainLength α β) : ℤ) - HMul.hMul (α := ℤ) 2 (↑(chainTopCoeff (⇑α : (a : ↥H_1) → K) β) : ℤ)) : K)
⊢ HSMul.hSMul (β := K) k 2 =
    (↑((↑(chainLength α β) : ℤ) - HMul.hMul (α := ℤ) 2 (↑(chainTopCoeff (⇑α : (a : ↥H_1) → K) β) : ℤ)) : K)

Tactic:
simp only [Pi.smul_apply, root_apply_coroot hα] at H

Premises used: LieAlgebra.IsKilling.root_apply_coroot, Pi.smul_apply
-- 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_1 : LieSubalgebra K L
inst_6 : H_1.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H_1) L
α β : Weight K (↥H_1) L
hα : α.IsNonZero
k : K
h : (⇑β : (a : ↥H_1) → K) = HSMul.hSMul (β := (a : ↥H_1) → K) k (⇑α : (a : ↥H_1) → K)
h_1 : Nontrivial L
H :
  HSMul.hSMul (β := K) k 2 =
    (↑((↑(chainLength α β) : ℤ) - HMul.hMul (α := ℤ) 2 (↑(chainTopCoeff (⇑α : (a : ↥H_1) → K) β) : ℤ)) : K)
inr : ∀ (n : ℕ) (hn : chainLength α β = n + n), k = -1 ∨ k = 0 ∨ k = 1
inr₁ : ∀ (n : ℕ) (hn : chainLength α β = 2 * n + 1), k = -1 ∨ k = 0 ∨ k = 1
⊢ k = -1 ∨ k = 0 ∨ k = 1

Tactic:
rcases (chainLength α β).even_or_odd with (⟨n, hn⟩ | ⟨n, hn⟩)

Premises used: LieAlgebra.IsKilling.chainLength, Nat.even_or_odd
-- 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_1 : LieSubalgebra K L
inst_6 : H_1.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H_1) L
α β : Weight K (↥H_1) L
hα : α.IsNonZero
k : K
h : (⇑β : (a : ↥H_1) → K) = HSMul.hSMul (β := (a : ↥H_1) → K) k (⇑α : (a : ↥H_1) → K)
h_1 : Nontrivial L
H :
  HSMul.hSMul (β := K) k 2 =
    (↑((↑(chainLength α β) : ℤ) - HMul.hMul (α := ℤ) 2 (↑(chainTopCoeff (⇑α : (a : ↥H_1) → K) β) : ℤ)) : K)
n : ℕ
hn : chainLength α β = n + n
⊢ HSMul.hSMul (β := K) k 2 =
    (↑((↑(2 * n) : ℤ) - HMul.hMul (α := ℤ) 2 (↑(chainTopCoeff (⇑α : (a : ↥H_1) → K) β) : ℤ)) : K)

Tactic:
rw [hn, ← two_mul] at H

Premises used: two_mul
-- 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_1 : LieSubalgebra K L
inst_6 : H_1.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H_1) L
α β : Weight K (↥H_1) L
hα : α.IsNonZero
k : K
h : (⇑β : (a : ↥H_1) → K) = HSMul.hSMul (β := (a : ↥H_1) → K) k (⇑α : (a : ↥H_1) → K)
h_1 : Nontrivial L
H :
  HSMul.hSMul (β := K) k 2 =
    (↑((↑(chainLength α β) : ℤ) - HMul.hMul (α := ℤ) 2 (↑(chainTopCoeff (⇑α : (a : ↥H_1) → K) β) : ℤ)) : K)
n : ℕ
hn : chainLength α β = n + n
H₁ :
  HSMul.hSMul (β := K) k 2 =
    (↑((↑(2 * n) : ℤ) - HMul.hMul (α := ℤ) 2 (↑(chainTopCoeff (⇑α : (a : ↥H_1) → K) β) : ℤ)) : K)
⊢ chainLength α β = n + n

Tactic:
rw [hn, ← two_mul] at H

Premises used: two_mul
-- 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_1 : LieSubalgebra K L
inst_6 : H_1.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H_1) L
α β : Weight K (↥H_1) L
hα : α.IsNonZero
k : K
h : (⇑β : (a : ↥H_1) → K) = HSMul.hSMul (β := (a : ↥H_1) → K) k (⇑α : (a : ↥H_1) → K)
h_1 : Nontrivial L
n : ℕ
H :
  HSMul.hSMul (β := K) k 2 =
    (↑((↑(2 * n) : ℤ) - HMul.hMul (α := ℤ) 2 (↑(chainTopCoeff (⇑α : (a : ↥H_1) → K) β) : ℤ)) : K)
hn : chainLength α β = n + n
⊢ k = HSub.hSub (α := K) (↑n : K) (↑(chainTopCoeff (⇑α : (a : ↥H_1) → K) β) : K)

Tactic:
simp only [smul_eq_mul, Nat.cast_mul, Nat.cast_ofNat, ← mul_sub, ← mul_comm (2 : K),
      Int.cast_sub, Int.cast_mul, Int.cast_ofNat, Int.cast_natCast,
      mul_eq_mul_left_iff, OfNat.ofNat_ne_zero, or_false] at H

Premises used: Nat.cast_ofNat, Int.cast_natCast, OfNat.ofNat_ne_zero, mul_sub, Int.cast_sub, mul_eq_mul_left_iff, Int.cast_ofNat, Int.cast_mul, Nat.cast_mul, mul_comm, or_false, smul_eq_mul, OfNat.ofNat
-- 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_1 : LieSubalgebra K L
inst_6 : H_1.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H_1) L
α β : Weight K (↥H_1) L
hα : α.IsNonZero
k : K
h : (⇑β : (a : ↥H_1) → K) = HSMul.hSMul (β := (a : ↥H_1) → K) k (⇑α : (a : ↥H_1) → K)
h_1 : Nontrivial L
n : ℕ
hn : chainLength α β = n + n
H : k = HSub.hSub (α := K) (↑n : K) (↑(chainTopCoeff (⇑α : (a : ↥H_1) → K) β) : K)
⊢ k = (↑(HSub.hSub (α := ℤ) (↑n : ℤ) (↑(chainTopCoeff (⇑α : (a : ↥H_1) → K) β) : ℤ)) : K)

Tactic:
rw [← Int.cast_natCast, ← Int.cast_natCast (chainTopCoeff α β), ← Int.cast_sub] at H

Premises used: Int.cast_natCast, Int.cast_sub, LieModule.chainTopCoeff, DFunLike.coe
-- 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_1 : LieSubalgebra K L
inst_6 : H_1.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H_1) L
α β : Weight K (↥H_1) L
hα : α.IsNonZero
k : K
h : (⇑β : (a : ↥H_1) → K) = HSMul.hSMul (β := (a : ↥H_1) → K) k (⇑α : (a : ↥H_1) → K)
h_1 : Nontrivial L
n : ℕ
hn : chainLength α β = n + n
H : k = (↑(HSub.hSub (α := ℤ) (↑n : ℤ) (↑(chainTopCoeff (⇑α : (a : ↥H_1) → K) β) : ℤ)) : K)
rw : rootSpace H_1 (⇑β : (a : ↥H_1) → K) ≠ ⊥
⊢ rootSpace H_1
      (HSMul.hSMul (β := (a : ↥H_1) → K) (HSub.hSub (α := ℤ) (↑n : ℤ) (↑(chainTopCoeff (⇑α : (a : ↥H_1) → K) β) : ℤ))
          (⇑α : (a : ↥H_1) → K) +
        (⇑0 : (a : ↥H_1) → K)) ≠
    ⊥

Tactic:
rw [← Int.cast_smul_eq_zsmul K, ← H, ← h, Weight.coe_zero, add_zero]

Premises used: LieModule.Weight.coe_zero, add_zero, 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_1 : LieSubalgebra K L
inst_6 : H_1.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H_1) L
α β : Weight K (↥H_1) L
hα : α.IsNonZero
k : K
h : (⇑β : (a : ↥H_1) → K) = HSMul.hSMul (β := (a : ↥H_1) → K) k (⇑α : (a : ↥H_1) → K)
h_1 : Nontrivial L
n : ℕ
hn : chainLength α β = n + n
H : k = (↑(HSub.hSub (α := ℤ) (↑n : ℤ) (↑(chainTopCoeff (⇑α : (a : ↥H_1) → K) β) : ℤ)) : K)
⊢ rootSpace H_1 (⇑β : (a : ↥H_1) → K) ≠ ⊥

Tactic:
β.2

Premises used: 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_1 : LieSubalgebra K L
inst_6 : H_1.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H_1) L
α β : Weight K (↥H_1) L
hα : α.IsNonZero
k : K
h : (⇑β : (a : ↥H_1) → K) = HSMul.hSMul (β := (a : ↥H_1) → K) k (⇑α : (a : ↥H_1) → K)
h_1 : Nontrivial L
n : ℕ
hn : chainLength α β = n + n
H : k = (↑(HSub.hSub (α := ℤ) (↑n : ℤ) (↑(chainTopCoeff (⇑α : (a : ↥H_1) → K) β) : ℤ)) : K)
⊢ rootSpace H_1 (⇑β : (a : ↥H_1) → K) ≠ ⊥

Tactic:
exact β.2

Premises used: 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_1 : LieSubalgebra K L
inst_6 : H_1.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H_1) L
α β : Weight K (↥H_1) L
hα : α.IsNonZero
k : K
h : (⇑β : (a : ↥H_1) → K) = HSMul.hSMul (β := (a : ↥H_1) → K) k (⇑α : (a : ↥H_1) → K)
h_1 : Nontrivial L
n : ℕ
hn : chainLength α β = n + n
H : k = (↑(HSub.hSub (α := ℤ) (↑n : ℤ) (↑(chainTopCoeff (⇑α : (a : ↥H_1) → K) β) : ℤ)) : K)
⊢ Membership.mem (γ := Finset ℤ)
    (Finset.Icc (-(↑(chainBotCoeff.{u_1, u_2, u_2} (R := K) (L := ↥H_1) (M := L) (⇑α : (a : ↥H_1) → K) 0) : ℤ))
      (↑(chainTopCoeff.{u_1, u_2, u_2} (R := K) (L := ↥H_1) (M := L) (⇑α : (a : ↥H_1) → K) 0) : ℤ))
    (HSub.hSub (α := ℤ) (↑n : ℤ) (↑(chainTopCoeff (⇑α : (a : ↥H_1) → K) β) : ℤ))

Tactic:
have := (rootSpace_zsmul_add_ne_bot_iff_mem α 0 hα (n - chainTopCoeff α β)).mp
      (by rw [← Int.cast_smul_eq_zsmul K, ← H, ← h, Weight.coe_zero, add_zero]; exact β.2)