awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Lie.Weights.RootSystem
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : LieRing L
inst_3 : LieAlgebra K L
inst_4 : IsKilling K L
inst_5 : FiniteDimensional K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H) L
α β : Weight K (↥H) L
hα : α.IsNonZero
n : ℤ
h₁ : n ≤ (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ)
h₂ : -n ≤ (↑(chainBotCoeff (⇑α : (a : ↥H) → K) β) : ℤ)
⊢ let k := (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ) - n;
  k = (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ) - n

Tactic:
set k := chainTopCoeff α β - n with hk

Premises used: 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 : 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
mpr :
  ∀ (k : ℤ) (hk : k = (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ) - n),
    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)) ≠ ⊥

Tactic:
clear_value k
-- 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
n : ℤ
h₁ : n ≤ (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ)
h₂ : -n ≤ (↑(chainBotCoeff (⇑α : (a : ↥H) → K) β) : ℤ)
k : ℤ
hk : k = (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ) - n
rw : n ≤ (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ)
⊢ 0 ≤ k

Tactic:
rw [hk, le_sub_iff_add_le, zero_add]

Premises used: zero_add, le_sub_iff_add_le
-- 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
n : ℤ
h₁ : n ≤ (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ)
h₂ : -n ≤ (↑(chainBotCoeff (⇑α : (a : ↥H) → K) β) : ℤ)
k : ℤ
hk : k = (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ) - n
⊢ n ≤ (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ)

Tactic:
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
n : ℤ
h₁ : n ≤ (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ)
h₂ : -n ≤ (↑(chainBotCoeff (⇑α : (a : ↥H) → K) β) : ℤ)
k : ℤ
hk : k = (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ) - n
⊢ n ≤ (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ)

Tactic:
exact 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
n : ℤ
h₁ : n ≤ (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ)
h₂ : -n ≤ (↑(chainBotCoeff (⇑α : (a : ↥H) → K) β) : ℤ)
k : ℤ
hk : k = (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ) - n
mpr :
  ∀ (k : ℕ) (hk : (↑k : ℤ) = (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ) - n),
    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)) ≠ ⊥

Tactic:
lift k to ℕ using (by rw [hk, le_sub_iff_add_le, zero_add]; exact 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
n : ℤ
h₁ : n ≤ (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ)
h₂ : -n ≤ (↑(chainBotCoeff (⇑α : (a : ↥H) → K) β) : ℤ)
k : ℕ
hk : (↑k : ℤ) = (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ) - n
⊢ n = HSub.hSub (α := ℤ) (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ) (↑k : ℤ)

Tactic:
rw [eq_sub_iff_add_eq, ← eq_sub_iff_add_eq'] at hk

Premises used: eq_sub_iff_add_eq', eq_sub_iff_add_eq
-- 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
n : ℤ
h₁ : n ≤ (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ)
h₂ : -n ≤ (↑(chainBotCoeff (⇑α : (a : ↥H) → K) β) : ℤ)
k : ℕ
hk : n = HSub.hSub (α := ℤ) (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ) (↑k : ℤ)
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)) ≠
      ⊥
⊢ rootSpace H (HSMul.hSMul (β := (a : ↥H) → K) n (⇑α : (a : ↥H) → K) + (⇑β : (a : ↥H) → K)) ≠ ⊥

Tactic:
subst hk
-- 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 : ℕ
h₁ :
  HSub.hSub (α := ℤ) (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ) (↑k : ℤ) ≤
    (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ)
h₂ :
  -HSub.hSub (α := ℤ) (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ) (↑k : ℤ) ≤
    (↑(chainBotCoeff (⇑α : (a : ↥H) → K) β) : ℤ)
⊢ k ≤ chainLength α β

Tactic:
simp only [neg_sub, tsub_le_iff_right, ← Nat.cast_add, Nat.cast_le,
      chainBotCoeff_add_chainTopCoeff] at h₂

Premises used: neg_sub, tsub_le_iff_right, Nat.cast_add, LieAlgebra.IsKilling.chainBotCoeff_add_chainTopCoeff, Nat.cast_le
-- 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 : ℕ
h₁ :
  HSub.hSub (α := ℤ) (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ) (↑k : ℤ) ≤
    (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ)
h₂ : k ≤ chainLength α β
⊢ 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₂
-- 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
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) β) : ℤ)
rw₃ rw₄ :
  -(↑(chainBotCoeff (⇑α : (a : ↥H) → K) β) : ℤ) ≤ n ∧ 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

Tactic:
rw [rootSpace_zsmul_add_ne_bot_iff α β hα n, Finset.mem_Icc, and_comm, neg_le]

Premises used: neg_le, Finset.mem_Icc, and_comm, LieAlgebra.IsKilling.rootSpace_zsmul_add_ne_bot_iff
-- Module: Mathlib.Algebra.Lie.Weights.RootSystem
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : LieRing L
inst_3 : LieAlgebra K L
inst_4 : IsKilling K L
inst_5 : FiniteDimensional K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H) L
α β : Weight K (↥H) L
hα : α.IsNonZero
β' : 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
a₁ : (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ) - n ≤ (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β') : ℤ)
⊢ (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β') : ℤ) = (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ) - n

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- 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
β' : 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

Tactic:
le_sub_iff_add_le.mpr ((rootSpace_zsmul_add_ne_bot_iff α β hα _).mp ?_).1

Premises used: Iff.mpr, LieAlgebra.IsKilling.rootSpace_zsmul_add_ne_bot_iff, And.left, Iff.mp, le_sub_iff_add_le
-- 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
β' : Weight K (↥H) L
n : ℤ
hβ' : (⇑β' : (a : ↥H) → K) = HSMul.hSMul (β := (a : ↥H) → K) n (⇑α : (a : ↥H) → K) + (⇑β : (a : ↥H) → K)
a :
  rootSpace H
      (HSMul.hSMul (β := (a : ↥H) → K) ((↑(chainTopCoeff (⇑α : (a : ↥H) → K) β') : ℤ) + n) (⇑α : (a : ↥H) → K) +
        (⇑β : (a : ↥H) → K)) ≠
    ⊥
⊢ (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β') : ℤ) ≤ (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ) - n

Tactic:
refine le_sub_iff_add_le.mpr ((rootSpace_zsmul_add_ne_bot_iff α β hα _).mp ?_).1

Premises used: Iff.mpr, LieAlgebra.IsKilling.rootSpace_zsmul_add_ne_bot_iff, And.left, Iff.mp, le_sub_iff_add_le
-- 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
β' : Weight K (↥H) L
n : ℤ
hβ' : (⇑β' : (a : ↥H) → K) = HSMul.hSMul (β := (a : ↥H) → K) n (⇑α : (a : ↥H) → K) + (⇑β : (a : ↥H) → K)
a : rootSpace H (⇑(chainTop (⇑α : (a : ↥H) → K) β') : (a : ↥H) → K) ≠ ⊥
⊢ rootSpace H
      (HSMul.hSMul (β := (a : ↥H) → K) ((↑(chainTopCoeff (⇑α : (a : ↥H) → K) β') : ℤ) + n) (⇑α : (a : ↥H) → K) +
        (⇑β : (a : ↥H) → K)) ≠
    ⊥

Tactic:
rw [add_smul, add_assoc, ← hβ', ← coe_chainTop]

Premises used: add_assoc, LieModule.coe_chainTop, add_smul
-- Module: Mathlib.Algebra.Lie.Weights.RootSystem
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : LieRing L
inst_3 : LieAlgebra K L
inst_4 : IsKilling K L
inst_5 : FiniteDimensional K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H) L
α β : Weight K (↥H) L
hα : α.IsNonZero
β' : Weight K (↥H) L
n : ℤ
hβ' : (⇑β' : (a : ↥H) → K) = HSMul.hSMul (β := (a : ↥H) → K) n (⇑α : (a : ↥H) → K) + (⇑β : (a : ↥H) → K)
⊢ rootSpace H (⇑(chainTop (⇑α : (a : ↥H) → K) β') : (a : ↥H) → K) ≠ ⊥

Tactic:
(chainTop α β').2

Premises used: LieModule.chainTop, DFunLike.coe, 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
β' : Weight K (↥H) L
n : ℤ
hβ' : (⇑β' : (a : ↥H) → K) = HSMul.hSMul (β := (a : ↥H) → K) n (⇑α : (a : ↥H) → K) + (⇑β : (a : ↥H) → K)
⊢ rootSpace H (⇑(chainTop (⇑α : (a : ↥H) → K) β') : (a : ↥H) → K) ≠ ⊥

Tactic:
exact (chainTop α β').2

Premises used: LieModule.chainTop, DFunLike.coe, 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
β' : 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) β') : ℤ)

Tactic:
((rootSpace_zsmul_add_ne_bot_iff α β' hα _).mp ?_).1

Premises used: LieAlgebra.IsKilling.rootSpace_zsmul_add_ne_bot_iff, And.left, Iff.mp
-- 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
β' : Weight K (↥H) L
n : ℤ
hβ' : (⇑β' : (a : ↥H) → K) = HSMul.hSMul (β := (a : ↥H) → K) n (⇑α : (a : ↥H) → K) + (⇑β : (a : ↥H) → K)
a :
  rootSpace H
      (HSMul.hSMul (β := (a : ↥H) → K) ((↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ) - n) (⇑α : (a : ↥H) → K) +
        (⇑β' : (a : ↥H) → K)) ≠
    ⊥
⊢ (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ) - n ≤ (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β') : ℤ)

Tactic:
refine ((rootSpace_zsmul_add_ne_bot_iff α β' hα _).mp ?_).1

Premises used: LieAlgebra.IsKilling.rootSpace_zsmul_add_ne_bot_iff, And.left, Iff.mp
-- 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
β' : Weight K (↥H) L
n : ℤ
hβ' : (⇑β' : (a : ↥H) → K) = HSMul.hSMul (β := (a : ↥H) → K) n (⇑α : (a : ↥H) → K) + (⇑β : (a : ↥H) → K)
a : rootSpace H (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (a : ↥H) → K) ≠ ⊥
⊢ rootSpace H
      (HSMul.hSMul (β := (a : ↥H) → K) ((↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ) - n) (⇑α : (a : ↥H) → K) +
        (⇑β' : (a : ↥H) → K)) ≠
    ⊥

Tactic:
rw [hβ', ← add_assoc, ← add_smul, sub_add_cancel, ← coe_chainTop]

Premises used: add_assoc, LieModule.coe_chainTop, add_smul, sub_add_cancel
-- 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
β' : Weight K (↥H) L
n : ℤ
hβ' : (⇑β' : (a : ↥H) → K) = HSMul.hSMul (β := (a : ↥H) → K) n (⇑α : (a : ↥H) → K) + (⇑β : (a : ↥H) → K)
⊢ rootSpace H (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (a : ↥H) → K) ≠ ⊥

Tactic:
(chainTop α β).2

Premises used: LieModule.chainTop, DFunLike.coe, 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
β' : Weight K (↥H) L
n : ℤ
hβ' : (⇑β' : (a : ↥H) → K) = HSMul.hSMul (β := (a : ↥H) → K) n (⇑α : (a : ↥H) → K) + (⇑β : (a : ↥H) → K)
⊢ rootSpace H (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (a : ↥H) → K) ≠ ⊥

Tactic:
exact (chainTop α β).2

Premises used: LieModule.chainTop, DFunLike.coe, 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
β' : 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)
rwa₁ : (⇑β' : (a : ↥H) → K) = - -HSMul.hSMul (β := (a : ↥H) → K) n (⇑α : (a : ↥H) → K) + (⇑β : (a : ↥H) → K)
rwa₂ rwa₃ rwa₄ 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)

Tactic:
rwa [neg_smul, smul_neg, neg_neg]

Premises used: neg_smul, neg_neg, smul_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
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)

Tactic:
have : (β' : H → K) = -n • (-α) + β := by rwa [neg_smul, smul_neg, 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
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
rw₄ rw₅ : (↑(chainTopCoeff (⇑(-α) : (a : ↥H) → K) β) : ℤ) + n = (↑(chainTopCoeff (⇑(-α) : (a : ↥H) → K) β) : ℤ) + n
⊢ (↑(chainBotCoeff (⇑α : (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]

Premises used: LieModule.Weight.IsNonZero.neg, LieModule.chainBotCoeff, LieAlgebra.IsKilling.chainTopCoeff_of_eq_zsmul_add, Neg.neg, sub_neg_eq_add, LieModule.Weight.coe_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
n : ℤ
hβ' : (⇑β' : (a : ↥H) → K) = HSMul.hSMul (β := (a : ↥H) → K) n (⇑α : (a : ↥H) → K) + (⇑β : (a : ↥H) → K)
pos : ∀ (hα : α.IsZero), chainLength α β' = chainLength α β
neg : ∀ (hα : ¬α.IsZero), chainLength α β' = chainLength α β
⊢ chainLength α β' = chainLength α β

Tactic:
by_cases hα : α.IsZero

Premises used: LieModule.Weight.IsZero
-- Module: Mathlib.Algebra.Lie.Weights.RootSystem
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : LieRing L
inst_3 : LieAlgebra K L
inst_4 : IsKilling K L
inst_5 : FiniteDimensional K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H) L
α β β' : Weight K (↥H) L
n : ℤ
hβ' : (⇑β' : (a : ↥H) → K) = HSMul.hSMul (β := (a : ↥H) → K) n (⇑α : (a : ↥H) → K) + (⇑β : (a : ↥H) → K)
hα : α.IsZero
pos : 0 = chainLength α β
pos₁ pos₂ : Eq (α := ℕ) 0 0
⊢ chainLength α β' = chainLength α β

Tactic:
rw [chainLength_of_isZero _ _ hα, chainLength_of_isZero _ _ hα]

Premises used: LieAlgebra.IsKilling.chainLength_of_isZero
-- Module: Mathlib.Algebra.Lie.Weights.RootSystem
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : LieRing L
inst_3 : LieAlgebra K L
inst_4 : IsKilling K L
inst_5 : FiniteDimensional K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H) L
α β β' : Weight K (↥H) L
n : ℤ
hβ' : (⇑β' : (a : ↥H) → K) = HSMul.hSMul (β := (a : ↥H) → K) n (⇑α : (a : ↥H) → K) + (⇑β : (a : ↥H) → K)
hα : ¬α.IsZero
neg : Eq (α := ℤ) (↑(chainLength α β') : ℤ) (↑(chainLength α β) : ℤ)
⊢ chainLength α β' = chainLength α β

Tactic:
apply Nat.cast_injective (R := ℤ)

Premises used: Nat.cast_injective
-- 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
symm : 1 = chainTopCoeff.{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 = 1

Tactic:
symm
-- 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
h₁ : 1 ≤ chainTopCoeff.{u_1, u_2, u_2} (R := K) (L := ↥H) (M := L) (⇑α : (a : ↥H) → K) 0
h₂ : ¬1 < chainTopCoeff.{u_1, u_2, u_2} (R := K) (L := ↥H) (M := L) (⇑α : (a : ↥H) → K) 0
⊢ 1 = chainTopCoeff.{u_1, u_2, u_2} (R := K) (L := ↥H) (M := L) (⇑α : (a : ↥H) → K) 0

Tactic:
apply eq_of_le_of_not_lt

Premises used: eq_of_le_of_not_lt