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 : ℤ
⊢ rootSpace H (HSMul.hSMul (β := (a : ↥H) → K) n (⇑α : (a : ↥H) → K) + (⇑β : (a : ↥H) → K)) ≠ ⊥ ↔
    n ≤ (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ) ∧ -n ≤ (↑(chainBotCoeff (⇑α : (a : ↥H) → K) β) : ℤ)
have mp : rootSpace H (HSMul.hSMul (β := (a : ↥H) → K) n (⇑α : (a : ↥H) → K) + (⇑β : (a : ↥H) → K)) ≠ ⊥ →
  n ≤ (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ) ∧ -n ≤ (↑(chainBotCoeff (⇑α : (a : ↥H) → K) β) : ℤ)
Tactic: constructor
-- 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 : ℤ
mp :
  rootSpace H (HSMul.hSMul (β := (a : ↥H) → K) n (⇑α : (a : ↥H) → K) + (⇑β : (a : ↥H) → K)) ≠ ⊥ →
    n ≤ (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ) ∧ -n ≤ (↑(chainBotCoeff (⇑α : (a : ↥H) → K) β) : ℤ)
⊢ rootSpace H (HSMul.hSMul (β := (a : ↥H) → K) n (⇑α : (a : ↥H) → K) + (⇑β : (a : ↥H) → K)) ≠ ⊥ ↔
    n ≤ (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ) ∧ -n ≤ (↑(chainBotCoeff (⇑α : (a : ↥H) → K) β) : ℤ)
have mpr : n ≤ (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ) ∧ -n ≤ (↑(chainBotCoeff (⇑α : (a : ↥H) → K) β) : ℤ) →
  rootSpace H (HSMul.hSMul (β := (a : ↥H) → K) n (⇑α : (a : ↥H) → K) + (⇑β : (a : ↥H) → K)) ≠ ⊥
Tactic: constructor
-- 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 : ℤ
⊢ rootSpace H (HSMul.hSMul (β := (a : ↥H) → K) n (⇑α : (a : ↥H) → K) + (⇑β : (a : ↥H) → K)) ≠ ⊥ →
    n ≤ (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ) ∧ -n ≤ (↑(chainBotCoeff (⇑α : (a : ↥H) → K) β) : ℤ)
have mp : ∀ (hn : rootSpace H (HSMul.hSMul (β := (a : ↥H) → K) n (⇑α : (a : ↥H) → K) + (⇑β : (a : ↥H) → K)) ≠ ⊥),
  n ≤ (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ)
Tactic: refine (fun hn ↦ ⟨?_, le_chainBotCoeff_of_rootSpace_ne_top α β hα _ (by rwa [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
n : ℤ
hn : rootSpace H (HSMul.hSMul (β := (a : ↥H) → K) n (⇑α : (a : ↥H) → K) + (⇑β : (a : ↥H) → K)) ≠ ⊥
⊢ n ≤ (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ)
have mp : n ≤ (↑(chainBotCoeff (⇑(-α) : (a : ↥H) → K) β) : ℤ)
Tactic: rw [← chainBotCoeff_neg, ← Weight.coe_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
n : ℤ
hn : rootSpace H (HSMul.hSMul (β := (a : ↥H) → K) n (⇑α : (a : ↥H) → K) + (⇑β : (a : ↥H) → K)) ≠ ⊥
⊢ n ≤ (↑(chainBotCoeff (⇑(-α) : (a : ↥H) → K) β) : ℤ)
have mp : rootSpace H (HSMul.hSMul (β := (a : ↥H) → K) (-n) (⇑(-α) : (a : ↥H) → K) + (⇑β : (a : ↥H) → K)) ≠ ⊥
Tactic: apply le_chainBotCoeff_of_rootSpace_ne_top _ _ hα.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
n : ℤ
hn : 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 mp : rootSpace H (-HSMul.hSMul (β := (a : ↥H) → K) n (⇑(-α) : (a : ↥H) → K) + (⇑β : (a : ↥H) → K)) ≠ ⊥
Tactic: rwa [neg_smul, Weight.coe_neg, 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
n : ℤ
hn : rootSpace H (HSMul.hSMul (β := (a : ↥H) → K) n (⇑α : (a : ↥H) → K) + (⇑β : (a : ↥H) → K)) ≠ ⊥
mp : 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 mp₁ : rootSpace H (-HSMul.hSMul (β := (a : ↥H) → K) n (-(⇑α : (a : ↥H) → K)) + (⇑β : (a : ↥H) → K)) ≠ ⊥
Tactic: rwa [neg_smul, Weight.coe_neg, 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
n : ℤ
hn : rootSpace H (HSMul.hSMul (β := (a : ↥H) → K) n (⇑α : (a : ↥H) → K) + (⇑β : (a : ↥H) → K)) ≠ ⊥
mp : rootSpace H (-HSMul.hSMul (β := (a : ↥H) → K) n (⇑(-α) : (a : ↥H) → K) + (⇑β : (a : ↥H) → K)) ≠ ⊥
mp₁ : 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 mp₂ : rootSpace H (- -HSMul.hSMul (β := (a : ↥H) → K) n (⇑α : (a : ↥H) → K) + (⇑β : (a : ↥H) → K)) ≠ ⊥
Tactic: rwa [neg_smul, Weight.coe_neg, 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
n : ℤ
h₁ : n ≤ (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ)
h₂ : -n ≤ (↑(chainBotCoeff (⇑α : (a : ↥H) → K) β) : ℤ)
⊢ rootSpace H (HSMul.hSMul (β := (a : ↥H) → K) n (⇑α : (a : ↥H) → K) + (⇑β : (a : ↥H) → K)) ≠ ⊥
have hk : let k := (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ) - n;
k = (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ) - n
Tactic: set k := chainTopCoeff α β - n with hk
-- 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 : ℤ
h₁ : n ≤ (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ)
h₂ : -n ≤ (↑(chainBotCoeff (⇑α : (a : ↥H) → K) β) : ℤ)
k : ℤ := (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ) - n
hk : k = (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ) - n
⊢ rootSpace H (HSMul.hSMul (β := (a : ↥H) → K) n (⇑α : (a : ↥H) → K) + (⇑β : (a : ↥H) → K)) ≠ ⊥
have mpr : ∀ (k : ℤ) (hk : k = (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ) - n),
  rootSpace H (HSMul.hSMul (β := (a : ↥H) → K) n (⇑α : (a : ↥H) → K) + (⇑β : (a : ↥H) → K)) ≠ ⊥
Tactic: clear_value k
Cleared hypotheses: k, hk
-- 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 : ℤ
h₁ : n ≤ (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ)
h₂ : -n ≤ (↑(chainBotCoeff (⇑α : (a : ↥H) → K) β) : ℤ)
k : ℤ
hk : k = (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ) - n
⊢ rootSpace H (HSMul.hSMul (β := (a : ↥H) → K) n (⇑α : (a : ↥H) → K) + (⇑β : (a : ↥H) → K)) ≠ ⊥
have mpr : ∀ (k : ℕ) (hk : (↑k : ℤ) = (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ) - n),
  rootSpace H (HSMul.hSMul (β := (a : ↥H) → K) n (⇑α : (a : ↥H) → K) + (⇑β : (a : ↥H) → K)) ≠ ⊥
Tactic: lift k to ℕ using (by rw [hk, le_sub_iff_add_le, zero_add]; exact h₁)
Cleared hypotheses: k, hk
-- 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 : ℤ
h₁ : n ≤ (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ)
h₂ : -n ≤ (↑(chainBotCoeff (⇑α : (a : ↥H) → K) β) : ℤ)
k : ℕ
hk : (↑k : ℤ) = (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ) - n
⊢ rootSpace H (HSMul.hSMul (β := (a : ↥H) → K) n (⇑α : (a : ↥H) → K) + (⇑β : (a : ↥H) → K)) ≠ ⊥
have hk₁ : n = HSub.hSub (α := ℤ) (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ) (↑k : ℤ)
Tactic: rw [eq_sub_iff_add_eq, ← eq_sub_iff_add_eq'] at hk
Cleared hypotheses: hk
-- 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 : ℤ
h₁ : n ≤ (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ)
h₂ : -n ≤ (↑(chainBotCoeff (⇑α : (a : ↥H) → K) β) : ℤ)
k : ℕ
hk : n = HSub.hSub (α := ℤ) (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ) (↑k : ℤ)
⊢ rootSpace H (HSMul.hSMul (β := (a : ↥H) → K) n (⇑α : (a : ↥H) → K) + (⇑β : (a : ↥H) → K)) ≠ ⊥
have mpr : ∀
  (h₁ :
    HSub.hSub (α := ℤ) (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ) (↑k : ℤ) ≤
      (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ))
  (h₂ :
    -HSub.hSub (α := ℤ) (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ) (↑k : ℤ) ≤
      (↑(chainBotCoeff (⇑α : (a : ↥H) → K) β) : ℤ)),
  rootSpace H
      (HSMul.hSMul (β := (a : ↥H) → K) (HSub.hSub (α := ℤ) (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ) (↑k : ℤ))
          (⇑α : (a : ↥H) → K) +
        (⇑β : (a : ↥H) → K)) ≠
    ⊥
Tactic: subst hk
Cleared hypotheses: n, h₁, h₂, hk
-- 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
k : ℕ
h₁ :
  HSub.hSub (α := ℤ) (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ) (↑k : ℤ) ≤
    (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ)
h₂ :
  -HSub.hSub (α := ℤ) (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ) (↑k : ℤ) ≤
    (↑(chainBotCoeff (⇑α : (a : ↥H) → K) β) : ℤ)
⊢ rootSpace H
      (HSMul.hSMul (β := (a : ↥H) → K) (HSub.hSub (α := ℤ) (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ) (↑k : ℤ))
          (⇑α : (a : ↥H) → K) +
        (⇑β : (a : ↥H) → K)) ≠
    ⊥
have h₃ : k ≤ chainLength α β
Tactic: simp only [neg_sub, tsub_le_iff_right, ← Nat.cast_add, Nat.cast_le,
      chainBotCoeff_add_chainTopCoeff] at h₂
Cleared hypotheses: h₂
-- 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
k : ℕ
h₁ :
  HSub.hSub (α := ℤ) (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ) (↑k : ℤ) ≤
    (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ)
h₂ : k ≤ chainLength α β
⊢ rootSpace H
      (HSMul.hSMul (β := (a : ↥H) → K) (HSub.hSub (α := ℤ) (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ) (↑k : ℤ))
          (⇑α : (a : ↥H) → K) +
        (⇑β : (a : ↥H) → K)) ≠
    ⊥
have this : rootSpace H
    (-HSMul.hSMul (β := (a : ↥H) → K) k (⇑α : (a : ↥H) → K) + (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (a : ↥H) → K)) ≠
  ⊥
Tactic: have := rootSpace_neg_nsmul_add_chainTop_of_le α β 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
hα : α.IsNonZero
k : ℕ
h₁ :
  HSub.hSub (α := ℤ) (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ) (↑k : ℤ) ≤
    (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ)
h₂ : k ≤ chainLength α β
this :
  rootSpace H
      (-HSMul.hSMul (β := (a : ↥H) → K) k (⇑α : (a : ↥H) → K) + (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (a : ↥H) → K)) ≠
    ⊥
⊢ rootSpace H
      (HSMul.hSMul (β := (a : ↥H) → K) (HSub.hSub (α := ℤ) (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ) (↑k : ℤ))
          (⇑α : (a : ↥H) → K) +
        (⇑β : (a : ↥H) → K)) ≠
    ⊥
have mpr : ∀
  (this :
    rootSpace H
        (-HSMul.hSMul (β := (a : ↥H) → K) 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) (HSub.hSub (α := ℤ) (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ) (↑k : ℤ))
          (⇑α : (a : ↥H) → K) +
        (⇑β : (a : ↥H) → K)) ≠
    ⊥
Tactic: rwa [coe_chainTop, ← Nat.cast_smul_eq_nsmul ℤ, ← neg_smul,
      ← add_assoc, ← add_smul, ← sub_eq_neg_add] 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
k : ℕ
h₁ :
  HSub.hSub (α := ℤ) (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ) (↑k : ℤ) ≤
    (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ)
h₂ : k ≤ chainLength α β
this :
  rootSpace H
      (-HSMul.hSMul (β := (a : ↥H) → K) k (⇑α : (a : ↥H) → K) + (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (a : ↥H) → K)) ≠
    ⊥
mpr :
  ∀
    (this :
      rootSpace H
          (-HSMul.hSMul (β := (a : ↥H) → K) 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) (HSub.hSub (α := ℤ) (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ) (↑k : ℤ))
            (⇑α : (a : ↥H) → K) +
          (⇑β : (a : ↥H) → K)) ≠
      ⊥
⊢ rootSpace H
      (HSMul.hSMul (β := (a : ↥H) → K) (HSub.hSub (α := ℤ) (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ) (↑k : ℤ))
          (⇑α : (a : ↥H) → K) +
        (⇑β : (a : ↥H) → K)) ≠
    ⊥
have mpr₁ : ∀
  (this :
    rootSpace H
        (-HSMul.hSMul (α := ℤ) (β := (a : ↥H) → K) (↑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) (HSub.hSub (α := ℤ) (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ) (↑k : ℤ))
          (⇑α : (a : ↥H) → K) +
        (⇑β : (a : ↥H) → K)) ≠
    ⊥
Tactic: rwa [coe_chainTop, ← Nat.cast_smul_eq_nsmul ℤ, ← neg_smul,
      ← add_assoc, ← add_smul, ← sub_eq_neg_add] 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
k : ℕ
h₁ :
  HSub.hSub (α := ℤ) (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ) (↑k : ℤ) ≤
    (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ)
h₂ : k ≤ chainLength α β
this :
  rootSpace H
      (-HSMul.hSMul (β := (a : ↥H) → K) k (⇑α : (a : ↥H) → K) + (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (a : ↥H) → K)) ≠
    ⊥
mpr :
  ∀
    (this :
      rootSpace H
          (-HSMul.hSMul (β := (a : ↥H) → K) 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) (HSub.hSub (α := ℤ) (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ) (↑k : ℤ))
            (⇑α : (a : ↥H) → K) +
          (⇑β : (a : ↥H) → K)) ≠
      ⊥
mpr₁ :
  ∀
    (this :
      rootSpace H
          (-HSMul.hSMul (α := ℤ) (β := (a : ↥H) → K) (↑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) (HSub.hSub (α := ℤ) (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ) (↑k : ℤ))
            (⇑α : (a : ↥H) → K) +
          (⇑β : (a : ↥H) → K)) ≠
      ⊥
⊢ rootSpace H
      (HSMul.hSMul (β := (a : ↥H) → K) (HSub.hSub (α := ℤ) (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ) (↑k : ℤ))
          (⇑α : (a : ↥H) → K) +
        (⇑β : (a : ↥H) → K)) ≠
    ⊥
have mpr₂ : ∀
  (this :
    rootSpace H
        (HSMul.hSMul (α := ℤ) (β := (a : ↥H) → K) (-(↑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) (HSub.hSub (α := ℤ) (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ) (↑k : ℤ))
          (⇑α : (a : ↥H) → K) +
        (⇑β : (a : ↥H) → K)) ≠
    ⊥
Tactic: rwa [coe_chainTop, ← Nat.cast_smul_eq_nsmul ℤ, ← neg_smul,
      ← add_assoc, ← add_smul, ← sub_eq_neg_add] 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
k : ℕ
h₁ :
  HSub.hSub (α := ℤ) (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ) (↑k : ℤ) ≤
    (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ)
h₂ : k ≤ chainLength α β
this :
  rootSpace H
      (-HSMul.hSMul (β := (a : ↥H) → K) k (⇑α : (a : ↥H) → K) + (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (a : ↥H) → K)) ≠
    ⊥
mpr :
  ∀
    (this :
      rootSpace H
          (-HSMul.hSMul (β := (a : ↥H) → K) 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) (HSub.hSub (α := ℤ) (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ) (↑k : ℤ))
            (⇑α : (a : ↥H) → K) +
          (⇑β : (a : ↥H) → K)) ≠
      ⊥
mpr₁ :
  ∀
    (this :
      rootSpace H
          (-HSMul.hSMul (α := ℤ) (β := (a : ↥H) → K) (↑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) (HSub.hSub (α := ℤ) (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ) (↑k : ℤ))
            (⇑α : (a : ↥H) → K) +
          (⇑β : (a : ↥H) → K)) ≠
      ⊥
mpr₂ :
  ∀
    (this :
      rootSpace H
          (HSMul.hSMul (α := ℤ) (β := (a : ↥H) → K) (-(↑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) (HSub.hSub (α := ℤ) (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ) (↑k : ℤ))
            (⇑α : (a : ↥H) → K) +
          (⇑β : (a : ↥H) → K)) ≠
      ⊥
⊢ rootSpace H
      (HSMul.hSMul (β := (a : ↥H) → K) (HSub.hSub (α := ℤ) (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ) (↑k : ℤ))
          (⇑α : (a : ↥H) → K) +
        (⇑β : (a : ↥H) → K)) ≠
    ⊥
have mpr₃ : ∀
  (this :
    rootSpace H
        (HSMul.hSMul (α := ℤ) (β := (a : ↥H) → K) (-(↑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) (HSub.hSub (α := ℤ) (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ) (↑k : ℤ))
          (⇑α : (a : ↥H) → K) +
        (⇑β : (a : ↥H) → K)) ≠
    ⊥
Tactic: rwa [coe_chainTop, ← Nat.cast_smul_eq_nsmul ℤ, ← neg_smul,
      ← add_assoc, ← add_smul, ← sub_eq_neg_add] 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 : ℤ
⊢ 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 ≤ (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ) ∧ -n ≤ (↑(chainBotCoeff (⇑α : (a : ↥H) → K) β) : ℤ) ↔
  Membership.mem (γ := Finset ℤ)
    (Finset.Icc (-(↑(chainBotCoeff (⇑α : (a : ↥H) → K) β) : ℤ)) (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ)) n
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
⊢ 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 ≤ (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ) ∧ -n ≤ (↑(chainBotCoeff (⇑α : (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]