-- Mathlib/Algebra/Lie/Weights/Killing.lean
lemma _root_.IsSl2Triple.h_eq_coroot {α : Weight K H L} (hα : α.IsNonZero)
    {h e f : L} (ht : IsSl2Triple h e f) (heα : e ∈ rootSpace H α) (hfα : f ∈ rootSpace H (- α)) :
    h = coroot α

Proof state:
K : Type u_2
L : Type u_3
inst✝⁷ : LieRing L
inst✝⁶ : Field K
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : IsKilling K L
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : CharZero K
α : Weight K (↥H) L
hα : α.IsNonZero
e f : L
heα : e ∈ rootSpace H ⇑α
hfα : f ∈ rootSpace H (-⇑α)
hef : ⁅e, f⁆ = ((killingForm K L) e) f • ↑((cartanEquivDual H).symm (Weight.toLinear K (↥H) L α))
h : ↥H
ht : IsSl2Triple (↑h) e f
this : 2 • e = α h • e
⊢ α h = 2

Tactic:
exact smul_left_injective K ht.e_ne_zero this.symm

Result:
no goals

Proof state:
case intro.e_self
K : Type u_2
L : Type u_3
inst✝⁷ : LieRing L
inst✝⁶ : Field K
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : IsKilling K L
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : CharZero K
α : Weight K (↥H) L
hα : α.IsNonZero
e f : L
heα : e ∈ rootSpace H ⇑α
hfα : f ∈ rootSpace H (-⇑α)
hef : ⁅e, f⁆ = ((killingForm K L) e) f • ↑((cartanEquivDual H).symm (Weight.toLinear K (↥H) L α))
h : ↥H
ht : IsSl2Triple (↑h) e f
key : α h = 2
⊢ ∃ s, s • h = coroot α

Tactic:
set α' := (cartanEquivDual H).symm α with hα'

Result:
case intro.e_self
K : Type u_2
L : Type u_3
inst✝⁷ : LieRing L
inst✝⁶ : Field K
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : IsKilling K L
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : CharZero K
α : Weight K (↥H) L
hα : α.IsNonZero
e f : L
heα : e ∈ rootSpace H ⇑α
hfα : f ∈ rootSpace H (-⇑α)
h : ↥H
ht : IsSl2Triple (↑h) e f
key : α h = 2
α' : ↥H := (cartanEquivDual H).symm (Weight.toLinear K (↥H) L α)
hef : ⁅e, f⁆ = ((killingForm K L) e) f • ↑α'
hα' : α' = (cartanEquivDual H).symm (Weight.toLinear K (↥H) L α)
⊢ ∃ s, s • h = coroot α

Proof state:
case intro.e_self
K : Type u_2
L : Type u_3
inst✝⁷ : LieRing L
inst✝⁶ : Field K
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : IsKilling K L
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : CharZero K
α : Weight K (↥H) L
hα : α.IsNonZero
e f : L
heα : e ∈ rootSpace H ⇑α
hfα : f ∈ rootSpace H (-⇑α)
hef : ⁅e, f⁆ = ((killingForm K L) e) f • ↑((cartanEquivDual H).symm (Weight.toLinear K (↥H) L α))
h : ↥H
ht : IsSl2Triple (↑h) e f
key : α h = 2
⊢ h = coroot α

Tactic:
suffices ∃ s : K, s • h = coroot α by
  obtain ⟨s, hs⟩ := this
  replace this : s = 1 := by simpa [root_apply_coroot hα, key] using congr_arg α hs
  rwa [this, one_smul] at hs

Result:
case intro.e_self
K : Type u_2
L : Type u_3
inst✝⁷ : LieRing L
inst✝⁶ : Field K
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : IsKilling K L
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : CharZero K
α : Weight K (↥H) L
hα : α.IsNonZero
e f : L
heα : e ∈ rootSpace H ⇑α
hfα : f ∈ rootSpace H (-⇑α)
hef : ⁅e, f⁆ = ((killingForm K L) e) f • ↑((cartanEquivDual H).symm (Weight.toLinear K (↥H) L α))
h : ↥H
ht : IsSl2Triple (↑h) e f
key : α h = 2
⊢ ∃ s, s • h = coroot α

Proof state:
K : Type u_2
L : Type u_3
inst✝⁷ : LieRing L
inst✝⁶ : Field K
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : IsKilling K L
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : CharZero K
α : Weight K (↥H) L
hα : α.IsNonZero
e f : L
heα : e ∈ rootSpace H ⇑α
hfα : f ∈ rootSpace H (-⇑α)
hef : ⁅e, f⁆ = ((killingForm K L) e) f • ↑((cartanEquivDual H).symm (Weight.toLinear K (↥H) L α))
h : ↥H
ht : IsSl2Triple (↑h) e f
this : ⁅h, e⁆ = α h • e
⊢ α h = 2

Tactic:
rw [LieSubalgebra.coe_bracket_of_module, ht.lie_h_e_smul K] at this

Result:
K : Type u_2
L : Type u_3
inst✝⁷ : LieRing L
inst✝⁶ : Field K
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : IsKilling K L
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : CharZero K
α : Weight K (↥H) L
hα : α.IsNonZero
e f : L
heα : e ∈ rootSpace H ⇑α
hfα : f ∈ rootSpace H (-⇑α)
hef : ⁅e, f⁆ = ((killingForm K L) e) f • ↑((cartanEquivDual H).symm (Weight.toLinear K (↥H) L α))
h : ↥H
ht : IsSl2Triple (↑h) e f
this : 2 • e = α h • e
⊢ α h = 2

Proof state:
K : Type u_2
L : Type u_3
inst✝⁷ : LieRing L
inst✝⁶ : Field K
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : IsKilling K L
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : CharZero K
α : Weight K (↥H) L
hα : α.IsNonZero
e f : L
heα : e ∈ rootSpace H ⇑α
hfα : f ∈ rootSpace H (-⇑α)
hef : ⁅e, f⁆ = ((killingForm K L) e) f • ↑((cartanEquivDual H).symm (Weight.toLinear K (↥H) L α))
h : ↥H
ht : IsSl2Triple (↑h) e f
⊢ α h = 2

Tactic:
have := lie_eq_smul_of_mem_rootSpace heα h

Result:
K : Type u_2
L : Type u_3
inst✝⁷ : LieRing L
inst✝⁶ : Field K
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : IsKilling K L
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : CharZero K
α : Weight K (↥H) L
hα : α.IsNonZero
e f : L
heα : e ∈ rootSpace H ⇑α
hfα : f ∈ rootSpace H (-⇑α)
hef : ⁅e, f⁆ = ((killingForm K L) e) f • ↑((cartanEquivDual H).symm (Weight.toLinear K (↥H) L α))
h : ↥H
ht : IsSl2Triple (↑h) e f
this : ⁅h, e⁆ = α h • e
⊢ α h = 2

Proof state:
case h
K : Type u_2
L : Type u_3
inst✝⁷ : LieRing L
inst✝⁶ : Field K
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : IsKilling K L
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : CharZero K
α : Weight K (↥H) L
hα : α.IsNonZero
e f : L
heα : e ∈ rootSpace H ⇑α
hfα : f ∈ rootSpace H (-⇑α)
h : ↥H
ht : IsSl2Triple (↑h) e f
key : α h = 2
α' : ↥H := (cartanEquivDual H).symm (Weight.toLinear K (↥H) L α)
hef : ⁅e, f⁆ = ((killingForm K L) e) f • ↑α'
hα' : α' = (cartanEquivDual H).symm (Weight.toLinear K (↥H) L α)
h_eq : h = ((killingForm K L) e) f • α'
hef₀ : ((killingForm K L) e) f ≠ 0
⊢ (2 • (α α')⁻¹ * (((killingForm K L) e) f)⁻¹) • h = coroot α

Tactic:
rw [h_eq, smul_smul, mul_assoc, inv_mul_cancel₀ hef₀, mul_one, smul_assoc, coroot]

Result:
no goals

Proof state:
K : Type u_2
L : Type u_3
inst✝⁷ : LieRing L
inst✝⁶ : Field K
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : IsKilling K L
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : CharZero K
α : Weight K (↥H) L
hα : α.IsNonZero
e f : L
heα : e ∈ rootSpace H ⇑α
hfα : f ∈ rootSpace H (-⇑α)
h : ↥H
ht : IsSl2Triple (↑h) e f
key : α h = 2
α' : ↥H := (cartanEquivDual H).symm (Weight.toLinear K (↥H) L α)
hef : ⁅e, f⁆ = ((killingForm K L) e) f • ↑α'
hα' : α' = (cartanEquivDual H).symm (Weight.toLinear K (↥H) L α)
h_eq : h = ((killingForm K L) e) f • α'
⊢ ((killingForm K L) e) f ≠ 0

Tactic:
have := ht.h_ne_zero

Result:
K : Type u_2
L : Type u_3
inst✝⁷ : LieRing L
inst✝⁶ : Field K
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : IsKilling K L
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : CharZero K
α : Weight K (↥H) L
hα : α.IsNonZero
e f : L
heα : e ∈ rootSpace H ⇑α
hfα : f ∈ rootSpace H (-⇑α)
h : ↥H
ht : IsSl2Triple (↑h) e f
key : α h = 2
α' : ↥H := (cartanEquivDual H).symm (Weight.toLinear K (↥H) L α)
hef : ⁅e, f⁆ = ((killingForm K L) e) f • ↑α'
hα' : α' = (cartanEquivDual H).symm (Weight.toLinear K (↥H) L α)
h_eq : h = ((killingForm K L) e) f • α'
this : ↑h ≠ 0
⊢ ((killingForm K L) e) f ≠ 0