-- Mathlib/Algebra/Lie/Weights/RootSystem.lean
lemma eq_neg_one_or_eq_zero_or_eq_one_of_eq_smul
    (hα : α.IsNonZero) (k : K) (h : (β : H → K) = k • α) :
    k = -1 ∨ k = 0 ∨ k = 1

Proof state:
case inr.inl.intro
K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra K L
inst✝³ : IsKilling K L
inst✝² : FiniteDimensional K L
H✝ : LieSubalgebra K L
inst✝¹ : H✝.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H✝) L
α β : Weight K (↥H✝) L
hα : α.IsNonZero
k : K
h : ⇑β = k • ⇑α
h✝ : Nontrivial L
n : ℕ
H : k • 2 = ↑(↑(2 * n) - 2 * ↑(chainTopCoeff (⇑α) β))
hn : chainLength α β = n + n
⊢ k = -1 ∨ k = 0 ∨ k = 1

Tactic:
simp only [smul_eq_mul, Nat.cast_mul, Nat.cast_ofNat, ← mul_sub, ← mul_comm (2 : K),
  Int.cast_sub, Int.cast_mul, Int.cast_ofNat, Int.cast_natCast,
  mul_eq_mul_left_iff, OfNat.ofNat_ne_zero, or_false] at H

Result:
case inr.inl.intro
K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra K L
inst✝³ : IsKilling K L
inst✝² : FiniteDimensional K L
H✝ : LieSubalgebra K L
inst✝¹ : H✝.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H✝) L
α β : Weight K (↥H✝) L
hα : α.IsNonZero
k : K
h : ⇑β = k • ⇑α
h✝ : Nontrivial L
n : ℕ
hn : chainLength α β = n + n
H : k = ↑n - ↑(chainTopCoeff (⇑α) β)
⊢ k = -1 ∨ k = 0 ∨ k = 1

Proof state:
case inr.inl.intro
K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra K L
inst✝³ : IsKilling K L
inst✝² : FiniteDimensional K L
H✝ : LieSubalgebra K L
inst✝¹ : H✝.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H✝) L
α β : Weight K (↥H✝) L
hα : α.IsNonZero
k : K
h : ⇑β = k • ⇑α
h✝ : Nontrivial L
n : ℕ
hn : chainLength α β = n + n
k' : ℤ := ↑n - ↑(chainTopCoeff (⇑α) β)
H : k = ↑k'
this : k' ∈ Finset.Icc (-1) 1
⊢ k = -1 ∨ k = 0 ∨ k = 1

Tactic:
subst H

Result:
case inr.inl.intro
K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra K L
inst✝³ : IsKilling K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
α β : Weight K (↥H) L
hα : α.IsNonZero
h✝ : Nontrivial L
n : ℕ
hn : chainLength α β = n + n
k' : ℤ := ↑n - ↑(chainTopCoeff (⇑α) β)
this : k' ∈ Finset.Icc (-1) 1
h : ⇑β = ↑k' • ⇑α
⊢ ↑k' = -1 ∨ ↑k' = 0 ∨ ↑k' = 1

Proof state:
case inr.inl.intro
K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra K L
inst✝³ : IsKilling K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
α β : Weight K (↥H) L
hα : α.IsNonZero
h✝ : Nontrivial L
n : ℕ
hn : chainLength α β = n + n
k' : ℤ := ↑n - ↑(chainTopCoeff (⇑α) β)
this✝ : k' ∈ Finset.Icc (-1) 1
h : ⇑β = ↑k' • ⇑α
this : k' ∈ {-1, 0, 1}
⊢ ↑k' = -1 ∨ ↑k' = 0 ∨ ↑k' = 1

Tactic:
simpa only [Int.reduceNeg, Finset.mem_insert, Finset.mem_singleton, ← @Int.cast_inj K,
  Int.cast_zero, Int.cast_neg, Int.cast_one] using this

Result:
no goals

Proof state:
K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra K L
inst✝³ : IsKilling K L
inst✝² : FiniteDimensional K L
H✝ : LieSubalgebra K L
inst✝¹ : H✝.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H✝) L
α β : Weight K (↥H✝) L
hα : α.IsNonZero
k : K
h : ⇑β = k • ⇑α
h✝ : Nontrivial L
n : ℕ
hn : chainLength α β = 2 * n + 1
H : k * 2 / 2 = ↑(↑(2 * n + 1) - 2 * ↑(chainTopCoeff (⇑α) β)) / 2
⊢ k = ↑n + 2⁻¹ - ↑(chainTopCoeff (⇑α) β)

Tactic:
simpa [sub_div, add_div] using H

Result:
no goals