awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.RootSystem (goal)
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
n : ℤ
rw :
  n ≤ (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ) ∧ -n ≤ (↑(chainBotCoeff (⇑α : (a : ↥H) → K) β) : ℤ) ↔
    Membership.mem (γ := Finset ℤ)
      (Finset.Icc (-(↑(chainBotCoeff (⇑α : (a : ↥H) → K) β) : ℤ)) (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ)) n
rw₁ :
  n ≤ (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ) ∧ -n ≤ (↑(chainBotCoeff (⇑α : (a : ↥H) → K) β) : ℤ) ↔
    -(↑(chainBotCoeff (⇑α : (a : ↥H) → K) β) : ℤ) ≤ n ∧ n ≤ (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ)
⊢ rootSpace H (HSMul.hSMul (β := (a : ↥H) → K) n (⇑α : (a : ↥H) → K) + (⇑β : (a : ↥H) → K)) ≠ ⊥ ↔
    Membership.mem (γ := Finset ℤ)
      (Finset.Icc (-(↑(chainBotCoeff (⇑α : (a : ↥H) → K) β) : ℤ)) (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ)) n
have rw₂ : -n ≤ (↑(chainBotCoeff (⇑α : (a : ↥H) → K) β) : ℤ) ∧ n ≤ (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ) ↔
  -(↑(chainBotCoeff (⇑α : (a : ↥H) → K) β) : ℤ) ≤ n ∧ n ≤ (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ)
Tactic: rw [rootSpace_zsmul_add_ne_bot_iff α β hα n, Finset.mem_Icc, and_comm, neg_le]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.RootSystem (goal)
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
n : ℤ
rw :
  n ≤ (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ) ∧ -n ≤ (↑(chainBotCoeff (⇑α : (a : ↥H) → K) β) : ℤ) ↔
    Membership.mem (γ := Finset ℤ)
      (Finset.Icc (-(↑(chainBotCoeff (⇑α : (a : ↥H) → K) β) : ℤ)) (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ)) n
rw₁ :
  n ≤ (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ) ∧ -n ≤ (↑(chainBotCoeff (⇑α : (a : ↥H) → K) β) : ℤ) ↔
    -(↑(chainBotCoeff (⇑α : (a : ↥H) → K) β) : ℤ) ≤ n ∧ n ≤ (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ)
rw₂ :
  -n ≤ (↑(chainBotCoeff (⇑α : (a : ↥H) → K) β) : ℤ) ∧ n ≤ (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ) ↔
    -(↑(chainBotCoeff (⇑α : (a : ↥H) → K) β) : ℤ) ≤ n ∧ n ≤ (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ)
⊢ rootSpace H (HSMul.hSMul (β := (a : ↥H) → K) n (⇑α : (a : ↥H) → K) + (⇑β : (a : ↥H) → K)) ≠ ⊥ ↔
    Membership.mem (γ := Finset ℤ)
      (Finset.Icc (-(↑(chainBotCoeff (⇑α : (a : ↥H) → K) β) : ℤ)) (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ)) n
have rw₃ : -(↑(chainBotCoeff (⇑α : (a : ↥H) → K) β) : ℤ) ≤ n ∧ n ≤ (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ) ↔
  -(↑(chainBotCoeff (⇑α : (a : ↥H) → K) β) : ℤ) ≤ n ∧ n ≤ (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ)
Tactic: rw [rootSpace_zsmul_add_ne_bot_iff α β hα n, Finset.mem_Icc, and_comm, neg_le]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.RootSystem (goal)
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
β' : Weight K (↥H) L
n : ℤ
hβ' : (⇑β' : (a : ↥H) → K) = HSMul.hSMul (β := (a : ↥H) → K) n (⇑α : (a : ↥H) → K) + (⇑β : (a : ↥H) → K)
⊢ (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β') : ℤ) = (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ) - n
have a : (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β') : ℤ) ≤ (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ) - n
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.RootSystem (goal)
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
β' : Weight K (↥H) L
n : ℤ
hβ' : (⇑β' : (a : ↥H) → K) = HSMul.hSMul (β := (a : ↥H) → K) n (⇑α : (a : ↥H) → K) + (⇑β : (a : ↥H) → K)
a : (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β') : ℤ) ≤ (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ) - n
⊢ (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β') : ℤ) = (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ) - n
have a₁ : (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ) - n ≤ (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β') : ℤ)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.RootSystem (goal)
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
β' : Weight K (↥H) L
n : ℤ
hβ' : (⇑β' : (a : ↥H) → K) = HSMul.hSMul (β := (a : ↥H) → K) n (⇑α : (a : ↥H) → K) + (⇑β : (a : ↥H) → K)
⊢ (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β') : ℤ) ≤ (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ) - n
have a : rootSpace H
    (HSMul.hSMul (β := (a : ↥H) → K) ((↑(chainTopCoeff (⇑α : (a : ↥H) → K) β') : ℤ) + n) (⇑α : (a : ↥H) → K) +
      (⇑β : (a : ↥H) → K)) ≠
  ⊥
Tactic: refine le_sub_iff_add_le.mpr ((rootSpace_zsmul_add_ne_bot_iff α β hα _).mp ?_).1
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.RootSystem (goal)
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
β' : Weight K (↥H) L
n : ℤ
hβ' : (⇑β' : (a : ↥H) → K) = HSMul.hSMul (β := (a : ↥H) → K) n (⇑α : (a : ↥H) → K) + (⇑β : (a : ↥H) → K)
⊢ rootSpace H
      (HSMul.hSMul (β := (a : ↥H) → K) ((↑(chainTopCoeff (⇑α : (a : ↥H) → K) β') : ℤ) + n) (⇑α : (a : ↥H) → K) +
        (⇑β : (a : ↥H) → K)) ≠
    ⊥
have a : rootSpace H (⇑(chainTop (⇑α : (a : ↥H) → K) β') : (a : ↥H) → K) ≠ ⊥
Tactic: rw [add_smul, add_assoc, ← hβ', ← coe_chainTop]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.RootSystem (goal)
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
β' : Weight K (↥H) L
n : ℤ
hβ' : (⇑β' : (a : ↥H) → K) = HSMul.hSMul (β := (a : ↥H) → K) n (⇑α : (a : ↥H) → K) + (⇑β : (a : ↥H) → K)
⊢ (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ) - n ≤ (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β') : ℤ)
have a : rootSpace H
    (HSMul.hSMul (β := (a : ↥H) → K) ((↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ) - n) (⇑α : (a : ↥H) → K) +
      (⇑β' : (a : ↥H) → K)) ≠
  ⊥
Tactic: refine ((rootSpace_zsmul_add_ne_bot_iff α β' hα _).mp ?_).1
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.RootSystem (goal)
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
β' : Weight K (↥H) L
n : ℤ
hβ' : (⇑β' : (a : ↥H) → K) = HSMul.hSMul (β := (a : ↥H) → K) n (⇑α : (a : ↥H) → K) + (⇑β : (a : ↥H) → K)
⊢ rootSpace H
      (HSMul.hSMul (β := (a : ↥H) → K) ((↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ) - n) (⇑α : (a : ↥H) → K) +
        (⇑β' : (a : ↥H) → K)) ≠
    ⊥
have a : rootSpace H (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (a : ↥H) → K) ≠ ⊥
Tactic: rw [hβ', ← add_assoc, ← add_smul, sub_add_cancel, ← coe_chainTop]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.RootSystem (goal)
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
β' : Weight K (↥H) L
n : ℤ
hβ' : (⇑β' : (a : ↥H) → K) = HSMul.hSMul (β := (a : ↥H) → K) n (⇑α : (a : ↥H) → K) + (⇑β : (a : ↥H) → K)
⊢ (⇑β' : (a : ↥H) → K) = HSMul.hSMul (β := (a : ↥H) → K) (-n) (-(⇑α : (a : ↥H) → K)) + (⇑β : (a : ↥H) → K)
have rwa : (⇑β' : (a : ↥H) → K) = -HSMul.hSMul (β := (a : ↥H) → K) n (-(⇑α : (a : ↥H) → K)) + (⇑β : (a : ↥H) → K)
Tactic: rwa [neg_smul, smul_neg, neg_neg]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.RootSystem (goal)
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
β' : Weight K (↥H) L
n : ℤ
hβ' : (⇑β' : (a : ↥H) → K) = HSMul.hSMul (β := (a : ↥H) → K) n (⇑α : (a : ↥H) → K) + (⇑β : (a : ↥H) → K)
rwa : (⇑β' : (a : ↥H) → K) = -HSMul.hSMul (β := (a : ↥H) → K) n (-(⇑α : (a : ↥H) → K)) + (⇑β : (a : ↥H) → K)
⊢ (⇑β' : (a : ↥H) → K) = HSMul.hSMul (β := (a : ↥H) → K) (-n) (-(⇑α : (a : ↥H) → K)) + (⇑β : (a : ↥H) → K)
have rwa₁ : (⇑β' : (a : ↥H) → K) = - -HSMul.hSMul (β := (a : ↥H) → K) n (⇑α : (a : ↥H) → K) + (⇑β : (a : ↥H) → K)
Tactic: rwa [neg_smul, smul_neg, neg_neg]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.RootSystem (hypothesis)
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
β' : Weight K (↥H) L
n : ℤ
hβ' : (⇑β' : (a : ↥H) → K) = HSMul.hSMul (β := (a : ↥H) → K) n (⇑α : (a : ↥H) → K) + (⇑β : (a : ↥H) → K)
⊢ (↑(chainBotCoeff (⇑α : (a : ↥H) → K) β') : ℤ) = (↑(chainBotCoeff (⇑α : (a : ↥H) → K) β) : ℤ) + n
have this : (⇑β' : (a : ↥H) → K) = HSMul.hSMul (β := (a : ↥H) → K) (-n) (-(⇑α : (a : ↥H) → K)) + (⇑β : (a : ↥H) → K)
Tactic: have : (β' : H → K) = -n • (-α) + β := by rwa [neg_smul, smul_neg, neg_neg]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.RootSystem (goal)
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
β' : Weight K (↥H) L
n : ℤ
hβ' : (⇑β' : (a : ↥H) → K) = HSMul.hSMul (β := (a : ↥H) → K) n (⇑α : (a : ↥H) → K) + (⇑β : (a : ↥H) → K)
this : (⇑β' : (a : ↥H) → K) = HSMul.hSMul (β := (a : ↥H) → K) (-n) (-(⇑α : (a : ↥H) → K)) + (⇑β : (a : ↥H) → K)
⊢ (↑(chainBotCoeff (⇑α : (a : ↥H) → K) β') : ℤ) = (↑(chainBotCoeff (⇑α : (a : ↥H) → K) β) : ℤ) + n
have rw : (↑(chainTopCoeff (-(⇑α : (a : ↥H) → K)) β') : ℤ) = (↑(chainBotCoeff (⇑α : (a : ↥H) → K) β) : ℤ) + n
Tactic: rw [chainBotCoeff, chainBotCoeff, ← Weight.coe_neg,
    chainTopCoeff_of_eq_zsmul_add (-α) β hα.neg β' (-n) this, sub_neg_eq_add]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.RootSystem (goal)
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
β' : Weight K (↥H) L
n : ℤ
hβ' : (⇑β' : (a : ↥H) → K) = HSMul.hSMul (β := (a : ↥H) → K) n (⇑α : (a : ↥H) → K) + (⇑β : (a : ↥H) → K)
this : (⇑β' : (a : ↥H) → K) = HSMul.hSMul (β := (a : ↥H) → K) (-n) (-(⇑α : (a : ↥H) → K)) + (⇑β : (a : ↥H) → K)
rw : (↑(chainTopCoeff (-(⇑α : (a : ↥H) → K)) β') : ℤ) = (↑(chainBotCoeff (⇑α : (a : ↥H) → K) β) : ℤ) + n
⊢ (↑(chainBotCoeff (⇑α : (a : ↥H) → K) β') : ℤ) = (↑(chainBotCoeff (⇑α : (a : ↥H) → K) β) : ℤ) + n
have rw₁ : (↑(chainTopCoeff (-(⇑α : (a : ↥H) → K)) β') : ℤ) = (↑(chainTopCoeff (-(⇑α : (a : ↥H) → K)) β) : ℤ) + n
Tactic: rw [chainBotCoeff, chainBotCoeff, ← Weight.coe_neg,
    chainTopCoeff_of_eq_zsmul_add (-α) β hα.neg β' (-n) this, sub_neg_eq_add]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.RootSystem (goal)
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
β' : Weight K (↥H) L
n : ℤ
hβ' : (⇑β' : (a : ↥H) → K) = HSMul.hSMul (β := (a : ↥H) → K) n (⇑α : (a : ↥H) → K) + (⇑β : (a : ↥H) → K)
this : (⇑β' : (a : ↥H) → K) = HSMul.hSMul (β := (a : ↥H) → K) (-n) (-(⇑α : (a : ↥H) → K)) + (⇑β : (a : ↥H) → K)
rw : (↑(chainTopCoeff (-(⇑α : (a : ↥H) → K)) β') : ℤ) = (↑(chainBotCoeff (⇑α : (a : ↥H) → K) β) : ℤ) + n
rw₁ : (↑(chainTopCoeff (-(⇑α : (a : ↥H) → K)) β') : ℤ) = (↑(chainTopCoeff (-(⇑α : (a : ↥H) → K)) β) : ℤ) + n
⊢ (↑(chainBotCoeff (⇑α : (a : ↥H) → K) β') : ℤ) = (↑(chainBotCoeff (⇑α : (a : ↥H) → K) β) : ℤ) + n
have rw₂ : (↑(chainTopCoeff (⇑(-α) : (a : ↥H) → K) β') : ℤ) = (↑(chainTopCoeff (⇑(-α) : (a : ↥H) → K) β) : ℤ) + n
Tactic: rw [chainBotCoeff, chainBotCoeff, ← Weight.coe_neg,
    chainTopCoeff_of_eq_zsmul_add (-α) β hα.neg β' (-n) this, sub_neg_eq_add]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.RootSystem (goal)
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
β' : Weight K (↥H) L
n : ℤ
hβ' : (⇑β' : (a : ↥H) → K) = HSMul.hSMul (β := (a : ↥H) → K) n (⇑α : (a : ↥H) → K) + (⇑β : (a : ↥H) → K)
this : (⇑β' : (a : ↥H) → K) = HSMul.hSMul (β := (a : ↥H) → K) (-n) (-(⇑α : (a : ↥H) → K)) + (⇑β : (a : ↥H) → K)
rw : (↑(chainTopCoeff (-(⇑α : (a : ↥H) → K)) β') : ℤ) = (↑(chainBotCoeff (⇑α : (a : ↥H) → K) β) : ℤ) + n
rw₁ : (↑(chainTopCoeff (-(⇑α : (a : ↥H) → K)) β') : ℤ) = (↑(chainTopCoeff (-(⇑α : (a : ↥H) → K)) β) : ℤ) + n
rw₂ : (↑(chainTopCoeff (⇑(-α) : (a : ↥H) → K) β') : ℤ) = (↑(chainTopCoeff (⇑(-α) : (a : ↥H) → K) β) : ℤ) + n
⊢ (↑(chainBotCoeff (⇑α : (a : ↥H) → K) β') : ℤ) = (↑(chainBotCoeff (⇑α : (a : ↥H) → K) β) : ℤ) + n
have rw₃ : (↑(chainTopCoeff (⇑(-α) : (a : ↥H) → K) β) : ℤ) - -n = (↑(chainTopCoeff (⇑(-α) : (a : ↥H) → K) β) : ℤ) + n
Tactic: rw [chainBotCoeff, chainBotCoeff, ← Weight.coe_neg,
    chainTopCoeff_of_eq_zsmul_add (-α) β hα.neg β' (-n) this, sub_neg_eq_add]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.RootSystem (goal)
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
β' : Weight K (↥H) L
n : ℤ
hβ' : (⇑β' : (a : ↥H) → K) = HSMul.hSMul (β := (a : ↥H) → K) n (⇑α : (a : ↥H) → K) + (⇑β : (a : ↥H) → K)
this : (⇑β' : (a : ↥H) → K) = HSMul.hSMul (β := (a : ↥H) → K) (-n) (-(⇑α : (a : ↥H) → K)) + (⇑β : (a : ↥H) → K)
rw : (↑(chainTopCoeff (-(⇑α : (a : ↥H) → K)) β') : ℤ) = (↑(chainBotCoeff (⇑α : (a : ↥H) → K) β) : ℤ) + n
rw₁ : (↑(chainTopCoeff (-(⇑α : (a : ↥H) → K)) β') : ℤ) = (↑(chainTopCoeff (-(⇑α : (a : ↥H) → K)) β) : ℤ) + n
rw₂ : (↑(chainTopCoeff (⇑(-α) : (a : ↥H) → K) β') : ℤ) = (↑(chainTopCoeff (⇑(-α) : (a : ↥H) → K) β) : ℤ) + n
rw₃ : (↑(chainTopCoeff (⇑(-α) : (a : ↥H) → K) β) : ℤ) - -n = (↑(chainTopCoeff (⇑(-α) : (a : ↥H) → K) β) : ℤ) + n
⊢ (↑(chainBotCoeff (⇑α : (a : ↥H) → K) β') : ℤ) = (↑(chainBotCoeff (⇑α : (a : ↥H) → K) β) : ℤ) + n
have rw₄ : (↑(chainTopCoeff (⇑(-α) : (a : ↥H) → K) β) : ℤ) + n = (↑(chainTopCoeff (⇑(-α) : (a : ↥H) → K) β) : ℤ) + n
Tactic: rw [chainBotCoeff, chainBotCoeff, ← Weight.coe_neg,
    chainTopCoeff_of_eq_zsmul_add (-α) β hα.neg β' (-n) this, sub_neg_eq_add]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.RootSystem (goal)
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
n : ℤ
hβ' : (⇑β' : (a : ↥H) → K) = HSMul.hSMul (β := (a : ↥H) → K) n (⇑α : (a : ↥H) → K) + (⇑β : (a : ↥H) → K)
⊢ chainLength α β' = chainLength α β
have pos : ∀ (hα : α.IsZero), chainLength α β' = chainLength α β
Tactic: by_cases hα : α.IsZero
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.RootSystem (goal)
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
n : ℤ
hβ' : (⇑β' : (a : ↥H) → K) = HSMul.hSMul (β := (a : ↥H) → K) n (⇑α : (a : ↥H) → K) + (⇑β : (a : ↥H) → K)
pos : ∀ (hα : α.IsZero), chainLength α β' = chainLength α β
⊢ chainLength α β' = chainLength α β
have neg : ∀ (hα : ¬α.IsZero), chainLength α β' = chainLength α β
Tactic: by_cases hα : α.IsZero
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.RootSystem (goal)
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
n : ℤ
hβ' : (⇑β' : (a : ↥H) → K) = HSMul.hSMul (β := (a : ↥H) → K) n (⇑α : (a : ↥H) → K) + (⇑β : (a : ↥H) → K)
hα : α.IsZero
⊢ chainLength α β' = chainLength α β
have pos : 0 = chainLength α β
Tactic: rw [chainLength_of_isZero _ _ hα, chainLength_of_isZero _ _ hα]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.RootSystem (goal)
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
n : ℤ
hβ' : (⇑β' : (a : ↥H) → K) = HSMul.hSMul (β := (a : ↥H) → K) n (⇑α : (a : ↥H) → K) + (⇑β : (a : ↥H) → K)
hα : α.IsZero
pos : 0 = chainLength α β
⊢ chainLength α β' = chainLength α β
have pos₁ : Eq (α := ℕ) 0 0
Tactic: rw [chainLength_of_isZero _ _ hα, chainLength_of_isZero _ _ hα]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.RootSystem (goal)
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
n : ℤ
hβ' : (⇑β' : (a : ↥H) → K) = HSMul.hSMul (β := (a : ↥H) → K) n (⇑α : (a : ↥H) → K) + (⇑β : (a : ↥H) → K)
hα : ¬α.IsZero
⊢ chainLength α β' = chainLength α β
have neg : Eq (α := ℤ) (↑(chainLength α β') : ℤ) (↑(chainLength α β) : ℤ)
Tactic: apply Nat.cast_injective (R := ℤ)
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.RootSystem (goal)
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
n : ℤ
hβ' : (⇑β' : (a : ↥H) → K) = HSMul.hSMul (β := (a : ↥H) → K) n (⇑α : (a : ↥H) → K) + (⇑β : (a : ↥H) → K)
hα : ¬α.IsZero
⊢ Eq (α := ℤ) (↑(chainLength α β') : ℤ) (↑(chainLength α β) : ℤ)
have neg : Eq (α := ℤ) (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β' + chainBotCoeff (⇑α : (a : ↥H) → K) β') : ℤ)
  (↑(chainLength α β) : ℤ)
Tactic: rw [← chainTopCoeff_add_chainBotCoeff, ← chainTopCoeff_add_chainBotCoeff,
      Nat.cast_add, Nat.cast_add, chainTopCoeff_of_eq_zsmul_add α β hα β' n hβ',
      chainBotCoeff_of_eq_zsmul_add α β hα β' n hβ', sub_eq_add_neg, add_add_add_comm,
      neg_add_cancel, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.RootSystem (goal)
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
n : ℤ
hβ' : (⇑β' : (a : ↥H) → K) = HSMul.hSMul (β := (a : ↥H) → K) n (⇑α : (a : ↥H) → K) + (⇑β : (a : ↥H) → K)
hα : ¬α.IsZero
neg :
  Eq (α := ℤ) (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β' + chainBotCoeff (⇑α : (a : ↥H) → K) β') : ℤ)
    (↑(chainLength α β) : ℤ)
⊢ Eq (α := ℤ) (↑(chainLength α β') : ℤ) (↑(chainLength α β) : ℤ)
have neg₁ : Eq (α := ℤ) (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β' + chainBotCoeff (⇑α : (a : ↥H) → K) β') : ℤ)
  (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β + chainBotCoeff (⇑α : (a : ↥H) → K) β) : ℤ)
Tactic: rw [← chainTopCoeff_add_chainBotCoeff, ← chainTopCoeff_add_chainBotCoeff,
      Nat.cast_add, Nat.cast_add, chainTopCoeff_of_eq_zsmul_add α β hα β' n hβ',
      chainBotCoeff_of_eq_zsmul_add α β hα β' n hβ', sub_eq_add_neg, add_add_add_comm,
      neg_add_cancel, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.RootSystem (goal)
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
n : ℤ
hβ' : (⇑β' : (a : ↥H) → K) = HSMul.hSMul (β := (a : ↥H) → K) n (⇑α : (a : ↥H) → K) + (⇑β : (a : ↥H) → K)
hα : ¬α.IsZero
neg :
  Eq (α := ℤ) (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β' + chainBotCoeff (⇑α : (a : ↥H) → K) β') : ℤ)
    (↑(chainLength α β) : ℤ)
neg₁ :
  Eq (α := ℤ) (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β' + chainBotCoeff (⇑α : (a : ↥H) → K) β') : ℤ)
    (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β + chainBotCoeff (⇑α : (a : ↥H) → K) β) : ℤ)
⊢ Eq (α := ℤ) (↑(chainLength α β') : ℤ) (↑(chainLength α β) : ℤ)
have neg₂ : HAdd.hAdd (α := ℤ) (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β') : ℤ) (↑(chainBotCoeff (⇑α : (a : ↥H) → K) β') : ℤ) =
  (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β + chainBotCoeff (⇑α : (a : ↥H) → K) β) : ℤ)
Tactic: rw [← chainTopCoeff_add_chainBotCoeff, ← chainTopCoeff_add_chainBotCoeff,
      Nat.cast_add, Nat.cast_add, chainTopCoeff_of_eq_zsmul_add α β hα β' n hβ',
      chainBotCoeff_of_eq_zsmul_add α β hα β' n hβ', sub_eq_add_neg, add_add_add_comm,
      neg_add_cancel, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.RootSystem (goal)
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
n : ℤ
hβ' : (⇑β' : (a : ↥H) → K) = HSMul.hSMul (β := (a : ↥H) → K) n (⇑α : (a : ↥H) → K) + (⇑β : (a : ↥H) → K)
hα : ¬α.IsZero
neg :
  Eq (α := ℤ) (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β' + chainBotCoeff (⇑α : (a : ↥H) → K) β') : ℤ)
    (↑(chainLength α β) : ℤ)
neg₁ :
  Eq (α := ℤ) (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β' + chainBotCoeff (⇑α : (a : ↥H) → K) β') : ℤ)
    (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β + chainBotCoeff (⇑α : (a : ↥H) → K) β) : ℤ)
neg₂ :
  HAdd.hAdd (α := ℤ) (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β') : ℤ) (↑(chainBotCoeff (⇑α : (a : ↥H) → K) β') : ℤ) =
    (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β + chainBotCoeff (⇑α : (a : ↥H) → K) β) : ℤ)
⊢ Eq (α := ℤ) (↑(chainLength α β') : ℤ) (↑(chainLength α β) : ℤ)
have neg₃ : HAdd.hAdd (α := ℤ) (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β') : ℤ) (↑(chainBotCoeff (⇑α : (a : ↥H) → K) β') : ℤ) =
  HAdd.hAdd (α := ℤ) (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ) (↑(chainBotCoeff (⇑α : (a : ↥H) → K) β) : ℤ)
Tactic: rw [← chainTopCoeff_add_chainBotCoeff, ← chainTopCoeff_add_chainBotCoeff,
      Nat.cast_add, Nat.cast_add, chainTopCoeff_of_eq_zsmul_add α β hα β' n hβ',
      chainBotCoeff_of_eq_zsmul_add α β hα β' n hβ', sub_eq_add_neg, add_add_add_comm,
      neg_add_cancel, add_zero]