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α : ¬α.IsZero
neg : chainBotCoeff (⇑α : (a : ↥H) → K) β + chainTopCoeff (⇑α : (a : ↥H) → K) β ≤ chainLength α β
neg₁ : chainLength α β ≤ chainBotCoeff (⇑α : (a : ↥H) → K) β + chainTopCoeff (⇑α : (a : ↥H) → K) β
⊢ chainBotCoeff (⇑α : (a : ↥H) → K) β + chainTopCoeff (⇑α : (a : ↥H) → K) β = chainLength α β

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α : ¬α.IsZero
neg : ¬(chainLength α β - chainTopCoeff (⇑α : (a : ↥H) → K) β).succ ≤ chainTopCoeff (⇑(-α) : (a : ↥H) → K) β
⊢ chainBotCoeff (⇑α : (a : ↥H) → K) β + chainTopCoeff (⇑α : (a : ↥H) → K) β ≤ chainLength α β

Tactic:
rw [← Nat.le_sub_iff_add_le (chainTopCoeff_le_chainLength α β),
      ← not_lt, ← Nat.succ_le_iff, chainBotCoeff, ← Weight.coe_neg]

Premises used: Nat.le_sub_iff_add_le, LieModule.chainBotCoeff, not_lt, LieAlgebra.IsKilling.chainTopCoeff_le_chainLength, Nat.succ_le_iff, 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
hα : ¬α.IsZero
e : (chainLength α β - chainTopCoeff (⇑α : (a : ↥H) → K) β).succ ≤ chainTopCoeff (⇑(-α) : (a : ↥H) → K) β
neg :
  Eq (α := LieSubmodule K (↥H) L)
    (genWeightSpace L
      (HSMul.hSMul (β := ↥H → K) (chainLength α β - chainTopCoeff (⇑α : (a : ↥H) → K) β).succ (⇑(-α) : (a : ↥H) → K) +
        (⇑β : (a : ↥H) → K)))
    ⊥
⊢ False

Tactic:
apply genWeightSpace_nsmul_add_ne_bot_of_le _ _ e

Premises used: LieModule.genWeightSpace_nsmul_add_ne_bot_of_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α : ¬α.IsZero
e : (chainLength α β - chainTopCoeff (⇑α : (a : ↥H) → K) β).succ ≤ chainTopCoeff (⇑(-α) : (a : ↥H) → K) β
neg :
  Eq (α := LieSubmodule K (↥H) L)
    (genWeightSpace L
      (-HSMul.hSMul (β := ↥H → K) (chainLength α β + 1) (⇑α : (a : ↥H) → K) +
        (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (a : ↥H) → K)))
    ⊥
⊢ Eq (α := LieSubmodule K (↥H) L)
    (genWeightSpace L
      (HSMul.hSMul (β := ↥H → K) (chainLength α β - chainTopCoeff (⇑α : (a : ↥H) → K) β).succ (⇑(-α) : (a : ↥H) → K) +
        (⇑β : (a : ↥H) → K)))
    ⊥

Tactic:
rw [← Nat.cast_smul_eq_nsmul ℤ, Nat.cast_succ, Nat.cast_sub (chainTopCoeff_le_chainLength α β),
      LieModule.Weight.coe_neg, smul_neg, ← neg_smul, neg_add_rev, neg_sub, sub_eq_neg_add,
      ← add_assoc, ← neg_add_rev, add_smul, add_assoc, ← coe_chainTop, neg_smul,
      ← @Nat.cast_one ℤ, ← Nat.cast_add, Nat.cast_smul_eq_nsmul]

Premises used: neg_add_rev, Nat.cast_succ, neg_smul, neg_sub, Nat.cast_sub, add_assoc, LieModule.coe_chainTop, sub_eq_neg_add, smul_neg, Int, Nat.cast_add, add_smul, Nat.cast_smul_eq_nsmul, LieAlgebra.IsKilling.chainTopCoeff_le_chainLength, Nat.cast_one, 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
hα : ¬α.IsZero
e : (chainLength α β - chainTopCoeff (⇑α : (a : ↥H) → K) β).succ ≤ chainTopCoeff (⇑(-α) : (a : ↥H) → K) β
⊢ Eq (α := LieSubmodule K (↥H) L)
    (genWeightSpace L
      (-HSMul.hSMul (β := ↥H → K) (chainLength α β + 1) (⇑α : (a : ↥H) → K) +
        (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (a : ↥H) → K)))
    ⊥

Tactic:
rootSpace_neg_nsmul_add_chainTop_of_lt α β hα (Nat.lt_succ_self _)

Premises used: LieAlgebra.IsKilling.rootSpace_neg_nsmul_add_chainTop_of_lt, Nat.lt_succ_self
-- 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α : ¬α.IsZero
e : (chainLength α β - chainTopCoeff (⇑α : (a : ↥H) → K) β).succ ≤ chainTopCoeff (⇑(-α) : (a : ↥H) → K) β
⊢ Eq (α := LieSubmodule K (↥H) L)
    (genWeightSpace L
      (-HSMul.hSMul (β := ↥H → K) (chainLength α β + 1) (⇑α : (a : ↥H) → K) +
        (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (a : ↥H) → K)))
    ⊥

Tactic:
exact rootSpace_neg_nsmul_add_chainTop_of_lt α β hα (Nat.lt_succ_self _)

Premises used: LieAlgebra.IsKilling.rootSpace_neg_nsmul_add_chainTop_of_lt, Nat.lt_succ_self
-- 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α : ¬α.IsZero
neg : ¬chainBotCoeff (⇑α : (a : ↥H) → K) β + chainTopCoeff (⇑α : (a : ↥H) → K) β < chainLength α β
⊢ chainLength α β ≤ chainBotCoeff (⇑α : (a : ↥H) → K) β + chainTopCoeff (⇑α : (a : ↥H) → K) β

Tactic:
rw [← not_lt]

Premises used: not_lt
-- 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α : ¬α.IsZero
e : chainBotCoeff (⇑α : (a : ↥H) → K) β + chainTopCoeff (⇑α : (a : ↥H) → K) β < chainLength α β
neg :
  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)) =
    ⊥
⊢ False

Tactic:
apply rootSpace_neg_nsmul_add_chainTop_of_le α β e

Premises used: LieAlgebra.IsKilling.rootSpace_neg_nsmul_add_chainTop_of_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α : ¬α.IsZero
e : chainBotCoeff (⇑α : (a : ↥H) → K) β + chainTopCoeff (⇑α : (a : ↥H) → K) β < chainLength α β
neg :
  rootSpace H
      (HSMul.hSMul (β := (a : ↥H) → K) (chainBotCoeff (⇑α : (a : ↥H) → K) β).succ (-(⇑α : (a : ↥H) → K)) +
        (⇑β : (a : ↥H) → K)) =
    ⊥
⊢ 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)) =
    ⊥

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]

Premises used: neg_smul, add_assoc, LieModule.coe_chainTop, neg_add, smul_neg, Int, Nat.cast_add, neg_add_cancel, add_smul, Nat.cast_smul_eq_nsmul, Nat.succ_add, add_zero
-- 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α : ¬α.IsZero
e : chainBotCoeff (⇑α : (a : ↥H) → K) β + chainTopCoeff (⇑α : (a : ↥H) → K) β < chainLength α β
⊢ rootSpace H
      (HSMul.hSMul (β := (a : ↥H) → K) (chainBotCoeff (⇑α : (a : ↥H) → K) β).succ (-(⇑α : (a : ↥H) → K)) +
        (⇑β : (a : ↥H) → K)) =
    ⊥

Tactic:
genWeightSpace_chainTopCoeff_add_one_nsmul_add (-α) β (Weight.IsNonZero.neg hα)

Premises used: LieModule.Weight.IsNonZero.neg, LieModule.chainBotCoeff, LieModule.genWeightSpace_chainTopCoeff_add_one_nsmul_add, DFunLike.coe, 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α : ¬α.IsZero
e : chainBotCoeff (⇑α : (a : ↥H) → K) β + chainTopCoeff (⇑α : (a : ↥H) → K) β < chainLength α β
⊢ rootSpace H
      (HSMul.hSMul (β := (a : ↥H) → K) (chainBotCoeff (⇑α : (a : ↥H) → K) β).succ (-(⇑α : (a : ↥H) → K)) +
        (⇑β : (a : ↥H) → K)) =
    ⊥

Tactic:
exact genWeightSpace_chainTopCoeff_add_one_nsmul_add (-α) β (Weight.IsNonZero.neg hα)

Premises used: LieModule.Weight.IsNonZero.neg, LieModule.genWeightSpace_chainTopCoeff_add_one_nsmul_add, DFunLike.coe, 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
rw : chainBotCoeff (⇑α : (a : ↥H) → K) β + chainTopCoeff (⇑α : (a : ↥H) → K) β = chainLength α β
rw₁ rw₂ : chainLength α β = chainLength α β
⊢ chainTopCoeff (⇑α : (a : ↥H) → K) β + chainBotCoeff (⇑α : (a : ↥H) → K) β = chainLength α β

Tactic:
rw [add_comm, chainBotCoeff_add_chainTopCoeff]

Premises used: add_comm, LieAlgebra.IsKilling.chainBotCoeff_add_chainTopCoeff
-- Module: Mathlib.Algebra.Lie.Weights.RootSystem
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : LieRing L
inst_3 : LieAlgebra K L
inst_4 : IsKilling K L
inst_5 : FiniteDimensional K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H) L
α β : Weight K (↥H) L
⊢ chainBotCoeff (⇑α : (a : ↥H) → K) β ≤ chainLength α β

Tactic:
(Nat.le_add_left _ _).trans_eq (chainTopCoeff_add_chainBotCoeff α β)

Premises used: LE.le.trans_eq, Nat.le_add_left, LieAlgebra.IsKilling.chainTopCoeff_add_chainBotCoeff
-- 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
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) β
rw₅ rw₆ :
  chainBotCoeff (⇑α : (a : ↥H) → K) β + chainTopCoeff (⇑α : (a : ↥H) → K) β =
    chainBotCoeff (⇑α : (a : ↥H) → K) β + chainTopCoeff (⇑α : (a : ↥H) → K) β
⊢ chainLength (-α) β = chainLength α β

Tactic:
rw [← chainBotCoeff_add_chainTopCoeff, ← chainBotCoeff_add_chainTopCoeff, add_comm,
    Weight.coe_neg, chainTopCoeff_neg, chainBotCoeff_neg]

Premises used: add_comm, LieModule.chainBotCoeff_neg, LieAlgebra.IsKilling.chainBotCoeff_add_chainTopCoeff, LieModule.chainTopCoeff_neg, 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
inst_8 : Nontrivial L
⊢ chainLength 0 β = 0

Tactic:
simp [← chainBotCoeff_add_chainTopCoeff]

Premises used: LieAlgebra.IsKilling.chainBotCoeff_add_chainTopCoeff
-- Module: Mathlib.Algebra.Lie.Weights.RootSystem
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : LieRing L
inst_3 : LieAlgebra K L
inst_4 : IsKilling K L
inst_5 : FiniteDimensional K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H) L
α β : Weight K (↥H) L
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)
⊢ Eq.{u_1 + 1} (α := K) ((β : (a : ↥H) → K) (coroot α) : K)
    ((↑(HSub.hSub (α := ℤ) (↑(chainBotCoeff (⇑α : (a : ↥H) → K) β) : ℤ) (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ)) :
        K) :
      K)

Tactic:
rw [apply_coroot_eq_cast', ← chainTopCoeff_add_chainBotCoeff]

Premises used: LieAlgebra.IsKilling.apply_coroot_eq_cast', LieAlgebra.IsKilling.chainTopCoeff_add_chainBotCoeff
-- 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
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) β) : ℤ)
⊢ 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:
congr 1
-- 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
⊢ (↑(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:
lia
-- 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 : ℤ
hn : rootSpace H (HSMul.hSMul (β := (a : ↥H) → K) (-n) (⇑α : (a : ↥H) → K) + (⇑β : (a : ↥H) → K)) ≠ ⊥
contrapose! :
  ∀ (hn : (↑(chainBotCoeff (⇑α : (a : ↥H) → K) β) : ℤ) < n),
    rootSpace H (HSMul.hSMul (β := (a : ↥H) → K) (-n) (⇑α : (a : ↥H) → K) + (⇑β : (a : ↥H) → K)) = ⊥
⊢ n ≤ (↑(chainBotCoeff (⇑α : (a : ↥H) → K) β) : ℤ)

Tactic:
contrapose! hn
-- 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 : ℤ
hn : (↑(chainBotCoeff (⇑α : (a : ↥H) → K) β) : ℤ) < n
⊢ 0 ≤ n

Tactic:
(Nat.cast_nonneg _).trans hn.le

Premises used: Nat.cast_nonneg, LT.lt.le, LE.le.trans
-- 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 : ℤ
hn : (↑(chainBotCoeff (⇑α : (a : ↥H) → K) β) : ℤ) < n
lift :
  ∀ (n : ℕ) (hn : LT.lt (α := ℤ) (↑(chainBotCoeff (⇑α : (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 n to ℕ using (Nat.cast_nonneg _).trans hn.le

Premises used: Nat.cast_nonneg, LT.lt.le, LE.le.trans
-- 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 : ℕ
hn : LT.lt (α := ℤ) (↑(chainBotCoeff (⇑α : (a : ↥H) → K) β) : ℤ) (↑n : ℤ)
⊢ chainLength α β < n + chainTopCoeff (⇑α : (a : ↥H) → K) β

Tactic:
rw [Nat.cast_lt, ← @Nat.add_lt_add_iff_right (chainTopCoeff α β),
    chainBotCoeff_add_chainTopCoeff] at hn

Premises used: LieAlgebra.IsKilling.chainBotCoeff_add_chainTopCoeff, Nat.cast_lt, Nat.add_lt_add_iff_right
-- 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 : ℕ
hn : chainLength α β < n + chainTopCoeff (⇑α : (a : ↥H) → K) β
⊢ 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
-- 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 : ℤ
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) β) : ℤ)
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)) ≠ ⊥
⊢ 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
-- 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 : ℤ
hn rwa rwa₁ rwa₂ rwa₃ : 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:
rwa [neg_neg]

Premises used: 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
n : ℤ
mp :
  ∀ (hn : rootSpace H (HSMul.hSMul (β := (a : ↥H) → K) n (⇑α : (a : ↥H) → K) + (⇑β : (a : ↥H) → K)) ≠ ⊥),
    n ≤ (↑(chainTopCoeff (⇑α : (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) β) : ℤ)

Tactic:
refine (fun hn ↦ ⟨?_, le_chainBotCoeff_of_rootSpace_ne_top α β hα _ (by rwa [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
n : ℤ
hn : rootSpace H (HSMul.hSMul (β := (a : ↥H) → K) n (⇑α : (a : ↥H) → K) + (⇑β : (a : ↥H) → K)) ≠ ⊥
mp : n ≤ (↑(chainBotCoeff (⇑(-α) : (a : ↥H) → K) β) : ℤ)
⊢ n ≤ (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ)

Tactic:
rw [← chainBotCoeff_neg, ← Weight.coe_neg]

Premises used: LieModule.chainBotCoeff_neg, 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
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)) ≠ ⊥
⊢ n ≤ (↑(chainBotCoeff (⇑(-α) : (a : ↥H) → K) β) : ℤ)

Tactic:
apply le_chainBotCoeff_of_rootSpace_ne_top _ _ hα.neg

Premises used: LieModule.Weight.IsNonZero.neg, LieAlgebra.IsKilling.le_chainBotCoeff_of_rootSpace_ne_top
-- 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 : ℤ
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)) ≠ ⊥
mp₂ : rootSpace H (- -HSMul.hSMul (β := (a : ↥H) → K) n (⇑α : (a : ↥H) → K) + (⇑β : (a : ↥H) → K)) ≠ ⊥
mp₃ mp₄ mp₅ 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)) ≠ ⊥

Tactic:
rwa [neg_smul, Weight.coe_neg, smul_neg, neg_neg]

Premises used: neg_smul, neg_neg, smul_neg, LieModule.Weight.coe_neg