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α : ¬α.IsZero
e : chainBotCoeff (⇑α : (a : ↥H) → K) β + chainTopCoeff (⇑α : (a : ↥H) → K) β < chainLength α β
⊢ rootSpace H
      (-HSMul.hSMul (β := (a : ↥H) → K) (chainBotCoeff (⇑α : (a : ↥H) → K) β + chainTopCoeff (⇑α : (a : ↥H) → K) β).succ
            (⇑α : (a : ↥H) → K) +
        (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (a : ↥H) → K)) =
    ⊥
have neg : rootSpace H
    (HSMul.hSMul (β := (a : ↥H) → K) (chainBotCoeff (⇑α : (a : ↥H) → K) β).succ (-(⇑α : (a : ↥H) → K)) +
      (⇑β : (a : ↥H) → K)) =
  ⊥
Tactic: rw [← Nat.succ_add, ← Nat.cast_smul_eq_nsmul ℤ, ← neg_smul, coe_chainTop, ← add_assoc,
      ← add_smul, Nat.cast_add, neg_add, add_assoc, neg_add_cancel, add_zero, neg_smul, ← smul_neg,
      Nat.cast_smul_eq_nsmul]
-- 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
⊢ chainTopCoeff (⇑α : (a : ↥H) → K) β + chainBotCoeff (⇑α : (a : ↥H) → K) β = chainLength α β
have rw : chainBotCoeff (⇑α : (a : ↥H) → K) β + chainTopCoeff (⇑α : (a : ↥H) → K) β = chainLength α β
Tactic: rw [add_comm, chainBotCoeff_add_chainTopCoeff]
-- 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
rw : chainBotCoeff (⇑α : (a : ↥H) → K) β + chainTopCoeff (⇑α : (a : ↥H) → K) β = chainLength α β
⊢ chainTopCoeff (⇑α : (a : ↥H) → K) β + chainBotCoeff (⇑α : (a : ↥H) → K) β = chainLength α β
have rw₁ : chainLength α β = chainLength α β
Tactic: rw [add_comm, chainBotCoeff_add_chainTopCoeff]
-- 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
⊢ chainLength (-α) β = chainLength α β
have rw : chainBotCoeff (⇑(-α) : (a : ↥H) → K) β + chainTopCoeff (⇑(-α) : (a : ↥H) → K) β = chainLength α β
Tactic: rw [← chainBotCoeff_add_chainTopCoeff, ← chainBotCoeff_add_chainTopCoeff, add_comm,
    Weight.coe_neg, chainTopCoeff_neg, chainBotCoeff_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
rw : chainBotCoeff (⇑(-α) : (a : ↥H) → K) β + chainTopCoeff (⇑(-α) : (a : ↥H) → K) β = chainLength α β
⊢ chainLength (-α) β = chainLength α β
have rw₁ : chainBotCoeff (⇑(-α) : (a : ↥H) → K) β + chainTopCoeff (⇑(-α) : (a : ↥H) → K) β =
  chainBotCoeff (⇑α : (a : ↥H) → K) β + chainTopCoeff (⇑α : (a : ↥H) → K) β
Tactic: rw [← chainBotCoeff_add_chainTopCoeff, ← chainBotCoeff_add_chainTopCoeff, add_comm,
    Weight.coe_neg, chainTopCoeff_neg, chainBotCoeff_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
rw : chainBotCoeff (⇑(-α) : (a : ↥H) → K) β + chainTopCoeff (⇑(-α) : (a : ↥H) → K) β = chainLength α β
rw₁ :
  chainBotCoeff (⇑(-α) : (a : ↥H) → K) β + chainTopCoeff (⇑(-α) : (a : ↥H) → K) β =
    chainBotCoeff (⇑α : (a : ↥H) → K) β + chainTopCoeff (⇑α : (a : ↥H) → K) β
⊢ chainLength (-α) β = chainLength α β
have rw₂ : chainTopCoeff (⇑(-α) : (a : ↥H) → K) β + chainBotCoeff (⇑(-α) : (a : ↥H) → K) β =
  chainBotCoeff (⇑α : (a : ↥H) → K) β + chainTopCoeff (⇑α : (a : ↥H) → K) β
Tactic: rw [← chainBotCoeff_add_chainTopCoeff, ← chainBotCoeff_add_chainTopCoeff, add_comm,
    Weight.coe_neg, chainTopCoeff_neg, chainBotCoeff_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
rw : chainBotCoeff (⇑(-α) : (a : ↥H) → K) β + chainTopCoeff (⇑(-α) : (a : ↥H) → K) β = chainLength α β
rw₁ :
  chainBotCoeff (⇑(-α) : (a : ↥H) → K) β + chainTopCoeff (⇑(-α) : (a : ↥H) → K) β =
    chainBotCoeff (⇑α : (a : ↥H) → K) β + chainTopCoeff (⇑α : (a : ↥H) → K) β
rw₂ :
  chainTopCoeff (⇑(-α) : (a : ↥H) → K) β + chainBotCoeff (⇑(-α) : (a : ↥H) → K) β =
    chainBotCoeff (⇑α : (a : ↥H) → K) β + chainTopCoeff (⇑α : (a : ↥H) → K) β
⊢ chainLength (-α) β = chainLength α β
have rw₃ : chainTopCoeff (-(⇑α : (a : ↥H) → K)) β + chainBotCoeff (-(⇑α : (a : ↥H) → K)) β =
  chainBotCoeff (⇑α : (a : ↥H) → K) β + chainTopCoeff (⇑α : (a : ↥H) → K) β
Tactic: rw [← chainBotCoeff_add_chainTopCoeff, ← chainBotCoeff_add_chainTopCoeff, add_comm,
    Weight.coe_neg, chainTopCoeff_neg, chainBotCoeff_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
rw : chainBotCoeff (⇑(-α) : (a : ↥H) → K) β + chainTopCoeff (⇑(-α) : (a : ↥H) → K) β = chainLength α β
rw₁ :
  chainBotCoeff (⇑(-α) : (a : ↥H) → K) β + chainTopCoeff (⇑(-α) : (a : ↥H) → K) β =
    chainBotCoeff (⇑α : (a : ↥H) → K) β + chainTopCoeff (⇑α : (a : ↥H) → K) β
rw₂ :
  chainTopCoeff (⇑(-α) : (a : ↥H) → K) β + chainBotCoeff (⇑(-α) : (a : ↥H) → K) β =
    chainBotCoeff (⇑α : (a : ↥H) → K) β + chainTopCoeff (⇑α : (a : ↥H) → K) β
rw₃ :
  chainTopCoeff (-(⇑α : (a : ↥H) → K)) β + chainBotCoeff (-(⇑α : (a : ↥H) → K)) β =
    chainBotCoeff (⇑α : (a : ↥H) → K) β + chainTopCoeff (⇑α : (a : ↥H) → K) β
⊢ chainLength (-α) β = chainLength α β
have rw₄ : chainBotCoeff (⇑α : (a : ↥H) → K) β + chainBotCoeff (-(⇑α : (a : ↥H) → K)) β =
  chainBotCoeff (⇑α : (a : ↥H) → K) β + chainTopCoeff (⇑α : (a : ↥H) → K) β
Tactic: rw [← chainBotCoeff_add_chainTopCoeff, ← chainBotCoeff_add_chainTopCoeff, add_comm,
    Weight.coe_neg, chainTopCoeff_neg, chainBotCoeff_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
rw : chainBotCoeff (⇑(-α) : (a : ↥H) → K) β + chainTopCoeff (⇑(-α) : (a : ↥H) → K) β = chainLength α β
rw₁ :
  chainBotCoeff (⇑(-α) : (a : ↥H) → K) β + chainTopCoeff (⇑(-α) : (a : ↥H) → K) β =
    chainBotCoeff (⇑α : (a : ↥H) → K) β + chainTopCoeff (⇑α : (a : ↥H) → K) β
rw₂ :
  chainTopCoeff (⇑(-α) : (a : ↥H) → K) β + chainBotCoeff (⇑(-α) : (a : ↥H) → K) β =
    chainBotCoeff (⇑α : (a : ↥H) → K) β + chainTopCoeff (⇑α : (a : ↥H) → K) β
rw₃ :
  chainTopCoeff (-(⇑α : (a : ↥H) → K)) β + chainBotCoeff (-(⇑α : (a : ↥H) → K)) β =
    chainBotCoeff (⇑α : (a : ↥H) → K) β + chainTopCoeff (⇑α : (a : ↥H) → K) β
rw₄ :
  chainBotCoeff (⇑α : (a : ↥H) → K) β + chainBotCoeff (-(⇑α : (a : ↥H) → K)) β =
    chainBotCoeff (⇑α : (a : ↥H) → K) β + chainTopCoeff (⇑α : (a : ↥H) → K) β
⊢ chainLength (-α) β = chainLength α β
have rw₅ : chainBotCoeff (⇑α : (a : ↥H) → K) β + chainTopCoeff (⇑α : (a : ↥H) → K) β =
  chainBotCoeff (⇑α : (a : ↥H) → K) β + chainTopCoeff (⇑α : (a : ↥H) → K) β
Tactic: rw [← chainBotCoeff_add_chainTopCoeff, ← chainBotCoeff_add_chainTopCoeff, add_comm,
    Weight.coe_neg, chainTopCoeff_neg, chainBotCoeff_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
⊢ Eq.{u_1 + 1} (α := K) ((β : (a : ↥H) → K) (coroot α) : K)
    ((↑(HSub.hSub (α := ℤ) (↑(chainBotCoeff (⇑α : (a : ↥H) → K) β) : ℤ) (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ)) :
        K) :
      K)
have rw : Eq.{u_1 + 1} (α := K)
  (↑((↑(chainTopCoeff (⇑α : (a : ↥H) → K) β + chainBotCoeff (⇑α : (a : ↥H) → K) β) : ℤ) -
        HMul.hMul (α := ℤ) 2 (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ)) :
    K)
  (↑(HSub.hSub (α := ℤ) (↑(chainBotCoeff (⇑α : (a : ↥H) → K) β) : ℤ) (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ)) : K)
Tactic: rw [apply_coroot_eq_cast', ← chainTopCoeff_add_chainBotCoeff]
-- 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
⊢ Eq.{u_1 + 1} (α := K)
    (↑((↑(chainTopCoeff (⇑α : (a : ↥H) → K) β + chainBotCoeff (⇑α : (a : ↥H) → K) β) : ℤ) -
          HMul.hMul (α := ℤ) 2 (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ)) :
      K)
    (↑(HSub.hSub (α := ℤ) (↑(chainBotCoeff (⇑α : (a : ↥H) → K) β) : ℤ) (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ)) :
      K)
have e_a : (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β + chainBotCoeff (⇑α : (a : ↥H) → K) β) : ℤ) -
    HMul.hMul (α := ℤ) 2 (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ) =
  HSub.hSub (α := ℤ) (↑(chainBotCoeff (⇑α : (a : ↥H) → K) β) : ℤ) (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ)
Tactic: congr 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
n : ℤ
hn : rootSpace H (HSMul.hSMul (β := (a : ↥H) → K) (-n) (⇑α : (a : ↥H) → K) + (⇑β : (a : ↥H) → K)) ≠ ⊥
⊢ n ≤ (↑(chainBotCoeff (⇑α : (a : ↥H) → K) β) : ℤ)
have contrapose! : ∀ (hn : (↑(chainBotCoeff (⇑α : (a : ↥H) → K) β) : ℤ) < n),
  rootSpace H (HSMul.hSMul (β := (a : ↥H) → K) (-n) (⇑α : (a : ↥H) → K) + (⇑β : (a : ↥H) → K)) = ⊥
Tactic: contrapose! hn
Cleared hypotheses: hn
-- 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 : ℤ
hn : (↑(chainBotCoeff (⇑α : (a : ↥H) → K) β) : ℤ) < n
⊢ rootSpace H (HSMul.hSMul (β := (a : ↥H) → K) (-n) (⇑α : (a : ↥H) → K) + (⇑β : (a : ↥H) → K)) = ⊥
have lift : ∀ (n : ℕ) (hn : LT.lt (α := ℤ) (↑(chainBotCoeff (⇑α : (a : ↥H) → K) β) : ℤ) (↑n : ℤ)),
  rootSpace H (HSMul.hSMul (α := ℤ) (β := (a : ↥H) → K) (-(↑n : ℤ)) (⇑α : (a : ↥H) → K) + (⇑β : (a : ↥H) → K)) = ⊥
Tactic: lift n to ℕ using (Nat.cast_nonneg _).trans hn.le
Cleared hypotheses: n, hn
-- 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
n : ℕ
hn : LT.lt (α := ℤ) (↑(chainBotCoeff (⇑α : (a : ↥H) → K) β) : ℤ) (↑n : ℤ)
⊢ rootSpace H (HSMul.hSMul (α := ℤ) (β := (a : ↥H) → K) (-(↑n : ℤ)) (⇑α : (a : ↥H) → K) + (⇑β : (a : ↥H) → K)) = ⊥
have hn₁ : chainLength α β < n + chainTopCoeff (⇑α : (a : ↥H) → K) β
Tactic: rw [Nat.cast_lt, ← @Nat.add_lt_add_iff_right (chainTopCoeff α β),
    chainBotCoeff_add_chainTopCoeff] at hn
Cleared hypotheses: hn
-- 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
n : ℕ
hn : chainLength α β < n + chainTopCoeff (⇑α : (a : ↥H) → K) β
⊢ rootSpace H (HSMul.hSMul (α := ℤ) (β := (a : ↥H) → K) (-(↑n : ℤ)) (⇑α : (a : ↥H) → K) + (⇑β : (a : ↥H) → K)) = ⊥
have this : rootSpace H
    (-HSMul.hSMul (β := (a : ↥H) → K) (n + chainTopCoeff (⇑α : (a : ↥H) → K) β) (⇑α : (a : ↥H) → K) +
      (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (a : ↥H) → K)) =
  ⊥
Tactic: have := rootSpace_neg_nsmul_add_chainTop_of_lt α β hα hn
-- 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 : ℕ
hn : chainLength α β < n + chainTopCoeff (⇑α : (a : ↥H) → K) β
this :
  rootSpace H
      (-HSMul.hSMul (β := (a : ↥H) → K) (n + chainTopCoeff (⇑α : (a : ↥H) → K) β) (⇑α : (a : ↥H) → K) +
        (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (a : ↥H) → K)) =
    ⊥
⊢ rootSpace H (HSMul.hSMul (α := ℤ) (β := (a : ↥H) → K) (-(↑n : ℤ)) (⇑α : (a : ↥H) → K) + (⇑β : (a : ↥H) → K)) = ⊥
have rwa : ∀
  (this :
    rootSpace H
        (-HSMul.hSMul (α := ℤ) (β := (a : ↥H) → K) (↑(n + chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ)
              (⇑α : (a : ↥H) → K) +
          (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (a : ↥H) → K)) =
      ⊥),
  rootSpace H (HSMul.hSMul (α := ℤ) (β := (a : ↥H) → K) (-(↑n : ℤ)) (⇑α : (a : ↥H) → K) + (⇑β : (a : ↥H) → K)) = ⊥
Tactic: rwa [← Nat.cast_smul_eq_nsmul ℤ, ← neg_smul, coe_chainTop, ← add_assoc,
    ← add_smul, Nat.cast_add, neg_add, add_assoc, neg_add_cancel, add_zero] at this
Cleared hypotheses: this
-- 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 : ℕ
hn : chainLength α β < n + chainTopCoeff (⇑α : (a : ↥H) → K) β
this :
  rootSpace H
      (-HSMul.hSMul (β := (a : ↥H) → K) (n + chainTopCoeff (⇑α : (a : ↥H) → K) β) (⇑α : (a : ↥H) → K) +
        (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (a : ↥H) → K)) =
    ⊥
rwa :
  ∀
    (this :
      rootSpace H
          (-HSMul.hSMul (α := ℤ) (β := (a : ↥H) → K) (↑(n + chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ)
                (⇑α : (a : ↥H) → K) +
            (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (a : ↥H) → K)) =
        ⊥),
    rootSpace H (HSMul.hSMul (α := ℤ) (β := (a : ↥H) → K) (-(↑n : ℤ)) (⇑α : (a : ↥H) → K) + (⇑β : (a : ↥H) → K)) = ⊥
⊢ rootSpace H (HSMul.hSMul (α := ℤ) (β := (a : ↥H) → K) (-(↑n : ℤ)) (⇑α : (a : ↥H) → K) + (⇑β : (a : ↥H) → K)) = ⊥
have rwa₁ : ∀
  (this :
    rootSpace H
        (HSMul.hSMul (α := ℤ) (β := (a : ↥H) → K) (-(↑(n + chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ))
            (⇑α : (a : ↥H) → K) +
          (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (a : ↥H) → K)) =
      ⊥),
  rootSpace H (HSMul.hSMul (α := ℤ) (β := (a : ↥H) → K) (-(↑n : ℤ)) (⇑α : (a : ↥H) → K) + (⇑β : (a : ↥H) → K)) = ⊥
Tactic: rwa [← Nat.cast_smul_eq_nsmul ℤ, ← neg_smul, coe_chainTop, ← add_assoc,
    ← add_smul, Nat.cast_add, neg_add, add_assoc, neg_add_cancel, add_zero] at this
Cleared hypotheses: this
-- 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 : ℕ
hn : chainLength α β < n + chainTopCoeff (⇑α : (a : ↥H) → K) β
this :
  rootSpace H
      (-HSMul.hSMul (β := (a : ↥H) → K) (n + chainTopCoeff (⇑α : (a : ↥H) → K) β) (⇑α : (a : ↥H) → K) +
        (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (a : ↥H) → K)) =
    ⊥
rwa :
  ∀
    (this :
      rootSpace H
          (-HSMul.hSMul (α := ℤ) (β := (a : ↥H) → K) (↑(n + chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ)
                (⇑α : (a : ↥H) → K) +
            (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (a : ↥H) → K)) =
        ⊥),
    rootSpace H (HSMul.hSMul (α := ℤ) (β := (a : ↥H) → K) (-(↑n : ℤ)) (⇑α : (a : ↥H) → K) + (⇑β : (a : ↥H) → K)) = ⊥
rwa₁ :
  ∀
    (this :
      rootSpace H
          (HSMul.hSMul (α := ℤ) (β := (a : ↥H) → K) (-(↑(n + chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ))
              (⇑α : (a : ↥H) → K) +
            (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (a : ↥H) → K)) =
        ⊥),
    rootSpace H (HSMul.hSMul (α := ℤ) (β := (a : ↥H) → K) (-(↑n : ℤ)) (⇑α : (a : ↥H) → K) + (⇑β : (a : ↥H) → K)) = ⊥
⊢ rootSpace H (HSMul.hSMul (α := ℤ) (β := (a : ↥H) → K) (-(↑n : ℤ)) (⇑α : (a : ↥H) → K) + (⇑β : (a : ↥H) → K)) = ⊥
have rwa₂ : ∀
  (this :
    rootSpace H
        (HSMul.hSMul (α := ℤ) (β := (a : ↥H) → K) (-(↑(n + chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ))
            (⇑α : (a : ↥H) → K) +
          (HSMul.hSMul (α := ℤ) (β := ↥H → K) (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ) (⇑α : (a : ↥H) → K) +
            (⇑β : (a : ↥H) → K))) =
      ⊥),
  rootSpace H (HSMul.hSMul (α := ℤ) (β := (a : ↥H) → K) (-(↑n : ℤ)) (⇑α : (a : ↥H) → K) + (⇑β : (a : ↥H) → K)) = ⊥
Tactic: rwa [← Nat.cast_smul_eq_nsmul ℤ, ← neg_smul, coe_chainTop, ← add_assoc,
    ← add_smul, Nat.cast_add, neg_add, add_assoc, neg_add_cancel, add_zero] at this
Cleared hypotheses: this
-- 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 : ℕ
hn : chainLength α β < n + chainTopCoeff (⇑α : (a : ↥H) → K) β
this :
  rootSpace H
      (-HSMul.hSMul (β := (a : ↥H) → K) (n + chainTopCoeff (⇑α : (a : ↥H) → K) β) (⇑α : (a : ↥H) → K) +
        (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (a : ↥H) → K)) =
    ⊥
rwa :
  ∀
    (this :
      rootSpace H
          (-HSMul.hSMul (α := ℤ) (β := (a : ↥H) → K) (↑(n + chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ)
                (⇑α : (a : ↥H) → K) +
            (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (a : ↥H) → K)) =
        ⊥),
    rootSpace H (HSMul.hSMul (α := ℤ) (β := (a : ↥H) → K) (-(↑n : ℤ)) (⇑α : (a : ↥H) → K) + (⇑β : (a : ↥H) → K)) = ⊥
rwa₁ :
  ∀
    (this :
      rootSpace H
          (HSMul.hSMul (α := ℤ) (β := (a : ↥H) → K) (-(↑(n + chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ))
              (⇑α : (a : ↥H) → K) +
            (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (a : ↥H) → K)) =
        ⊥),
    rootSpace H (HSMul.hSMul (α := ℤ) (β := (a : ↥H) → K) (-(↑n : ℤ)) (⇑α : (a : ↥H) → K) + (⇑β : (a : ↥H) → K)) = ⊥
rwa₂ :
  ∀
    (this :
      rootSpace H
          (HSMul.hSMul (α := ℤ) (β := (a : ↥H) → K) (-(↑(n + chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ))
              (⇑α : (a : ↥H) → K) +
            (HSMul.hSMul (α := ℤ) (β := ↥H → K) (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ) (⇑α : (a : ↥H) → K) +
              (⇑β : (a : ↥H) → K))) =
        ⊥),
    rootSpace H (HSMul.hSMul (α := ℤ) (β := (a : ↥H) → K) (-(↑n : ℤ)) (⇑α : (a : ↥H) → K) + (⇑β : (a : ↥H) → K)) = ⊥
⊢ rootSpace H (HSMul.hSMul (α := ℤ) (β := (a : ↥H) → K) (-(↑n : ℤ)) (⇑α : (a : ↥H) → K) + (⇑β : (a : ↥H) → K)) = ⊥
have rwa₃ : ∀
  (this :
    rootSpace H
        (HSMul.hSMul (α := ℤ) (β := (a : ↥H) → K) (-(↑(n + chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ))
              (⇑α : (a : ↥H) → K) +
            HSMul.hSMul (α := ℤ) (β := ↥H → K) (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ) (⇑α : (a : ↥H) → K) +
          (⇑β : (a : ↥H) → K)) =
      ⊥),
  rootSpace H (HSMul.hSMul (α := ℤ) (β := (a : ↥H) → K) (-(↑n : ℤ)) (⇑α : (a : ↥H) → K) + (⇑β : (a : ↥H) → K)) = ⊥
Tactic: rwa [← Nat.cast_smul_eq_nsmul ℤ, ← neg_smul, coe_chainTop, ← add_assoc,
    ← add_smul, Nat.cast_add, neg_add, add_assoc, neg_add_cancel, add_zero] at this
Cleared hypotheses: this
-- 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 : ℕ
hn : chainLength α β < n + chainTopCoeff (⇑α : (a : ↥H) → K) β
this :
  rootSpace H
      (-HSMul.hSMul (β := (a : ↥H) → K) (n + chainTopCoeff (⇑α : (a : ↥H) → K) β) (⇑α : (a : ↥H) → K) +
        (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (a : ↥H) → K)) =
    ⊥
rwa :
  ∀
    (this :
      rootSpace H
          (-HSMul.hSMul (α := ℤ) (β := (a : ↥H) → K) (↑(n + chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ)
                (⇑α : (a : ↥H) → K) +
            (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (a : ↥H) → K)) =
        ⊥),
    rootSpace H (HSMul.hSMul (α := ℤ) (β := (a : ↥H) → K) (-(↑n : ℤ)) (⇑α : (a : ↥H) → K) + (⇑β : (a : ↥H) → K)) = ⊥
rwa₁ :
  ∀
    (this :
      rootSpace H
          (HSMul.hSMul (α := ℤ) (β := (a : ↥H) → K) (-(↑(n + chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ))
              (⇑α : (a : ↥H) → K) +
            (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (a : ↥H) → K)) =
        ⊥),
    rootSpace H (HSMul.hSMul (α := ℤ) (β := (a : ↥H) → K) (-(↑n : ℤ)) (⇑α : (a : ↥H) → K) + (⇑β : (a : ↥H) → K)) = ⊥
rwa₂ :
  ∀
    (this :
      rootSpace H
          (HSMul.hSMul (α := ℤ) (β := (a : ↥H) → K) (-(↑(n + chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ))
              (⇑α : (a : ↥H) → K) +
            (HSMul.hSMul (α := ℤ) (β := ↥H → K) (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ) (⇑α : (a : ↥H) → K) +
              (⇑β : (a : ↥H) → K))) =
        ⊥),
    rootSpace H (HSMul.hSMul (α := ℤ) (β := (a : ↥H) → K) (-(↑n : ℤ)) (⇑α : (a : ↥H) → K) + (⇑β : (a : ↥H) → K)) = ⊥
rwa₃ :
  ∀
    (this :
      rootSpace H
          (HSMul.hSMul (α := ℤ) (β := (a : ↥H) → K) (-(↑(n + chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ))
                (⇑α : (a : ↥H) → K) +
              HSMul.hSMul (α := ℤ) (β := ↥H → K) (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ) (⇑α : (a : ↥H) → K) +
            (⇑β : (a : ↥H) → K)) =
        ⊥),
    rootSpace H (HSMul.hSMul (α := ℤ) (β := (a : ↥H) → K) (-(↑n : ℤ)) (⇑α : (a : ↥H) → K) + (⇑β : (a : ↥H) → K)) = ⊥
⊢ rootSpace H (HSMul.hSMul (α := ℤ) (β := (a : ↥H) → K) (-(↑n : ℤ)) (⇑α : (a : ↥H) → K) + (⇑β : (a : ↥H) → K)) = ⊥
have rwa₄ : ∀
  (this :
    rootSpace H
        (HSMul.hSMul (β := (a : ↥H) → K)
            (HAdd.hAdd (α := ℤ) (-(↑(n + chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ))
              (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ))
            (⇑α : (a : ↥H) → K) +
          (⇑β : (a : ↥H) → K)) =
      ⊥),
  rootSpace H (HSMul.hSMul (α := ℤ) (β := (a : ↥H) → K) (-(↑n : ℤ)) (⇑α : (a : ↥H) → K) + (⇑β : (a : ↥H) → K)) = ⊥
Tactic: rwa [← Nat.cast_smul_eq_nsmul ℤ, ← neg_smul, coe_chainTop, ← add_assoc,
    ← add_smul, Nat.cast_add, neg_add, add_assoc, neg_add_cancel, add_zero] at this
Cleared hypotheses: this