-- Mathlib/Algebra/Lie/Weights/Killing.lean
lemma coe_corootSpace_eq_span_singleton' (α : Weight K H L) :
    (corootSpace α).toSubmodule = K ∙ (cartanEquivDual H).symm α

Proof state:
case refine_1
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✝ : PerfectField K
α : Weight K (↥H) L
x : L
hx : x ∈ H
hx' : x ∈ span K {x | ∃ y ∈ rootSpace H ⇑α, ∃ z ∈ rootSpace H (-⇑α), ⁅y, z⁆ = x}
this : x ∈ span K ↑(span K {↑((cartanEquivDual H).symm (Weight.toLinear K (↥H) L α))})
⊢ ⟨x, hx⟩ ∈ span K {(cartanEquivDual H).symm (Weight.toLinear K (↥H) L α)}

Tactic:
rw [Submodule.span_span] at this

Result:
case refine_1
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✝ : PerfectField K
α : Weight K (↥H) L
x : L
hx : x ∈ H
hx' : x ∈ span K {x | ∃ y ∈ rootSpace H ⇑α, ∃ z ∈ rootSpace H (-⇑α), ⁅y, z⁆ = x}
this : x ∈ span K {↑((cartanEquivDual H).symm (Weight.toLinear K (↥H) L α))}
⊢ ⟨x, hx⟩ ∈ span K {(cartanEquivDual H).symm (Weight.toLinear K (↥H) L α)}

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✝ : PerfectField K
α : Weight K (↥H) L
t : K
hx : t • ↑((cartanEquivDual H).symm (Weight.toLinear K (↥H) L α)) ∈ H
hx' :
  t • ↑((cartanEquivDual H).symm (Weight.toLinear K (↥H) L α)) ∈
    span K {x | ∃ y ∈ rootSpace H ⇑α, ∃ z ∈ rootSpace H (-⇑α), ⁅y, z⁆ = x}
⊢ t • (cartanEquivDual H).symm (Weight.toLinear K (↥H) L α) =
    ⟨t • ↑((cartanEquivDual H).symm (Weight.toLinear K (↥H) L α)), hx⟩

Tactic:
simp only [Subtype.ext_iff]

Result:
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✝ : PerfectField K
α : Weight K (↥H) L
t : K
hx : t • ↑((cartanEquivDual H).symm (Weight.toLinear K (↥H) L α)) ∈ H
hx' :
  t • ↑((cartanEquivDual H).symm (Weight.toLinear K (↥H) L α)) ∈
    span K {x | ∃ y ∈ rootSpace H ⇑α, ∃ z ∈ rootSpace H (-⇑α), ⁅y, z⁆ = x}
⊢ ↑(t • (cartanEquivDual H).symm (Weight.toLinear K (↥H) L α)) =
    t • ↑((cartanEquivDual H).symm (Weight.toLinear K (↥H) L α))

Proof state:
case refine_1
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✝ : PerfectField K
α : Weight K (↥H) L
x : L
hx : x ∈ H
hx' : x ∈ span K {x | ∃ y ∈ rootSpace H ⇑α, ∃ z ∈ rootSpace H (-⇑α), ⁅y, z⁆ = x}
this : x ∈ span K {↑((cartanEquivDual H).symm (Weight.toLinear K (↥H) L α))}
⊢ ⟨x, hx⟩ ∈ span K {(cartanEquivDual H).symm (Weight.toLinear K (↥H) L α)}

Tactic:
rw [Submodule.mem_span_singleton] at this ⊢

Result:
case refine_1
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✝ : PerfectField K
α : Weight K (↥H) L
x : L
hx : x ∈ H
hx' : x ∈ span K {x | ∃ y ∈ rootSpace H ⇑α, ∃ z ∈ rootSpace H (-⇑α), ⁅y, z⁆ = x}
this : ∃ a, a • ↑((cartanEquivDual H).symm (Weight.toLinear K (↥H) L α)) = x
⊢ ∃ a, a • (cartanEquivDual H).symm (Weight.toLinear K (↥H) L α) = ⟨x, hx⟩

Proof state:
case refine_1
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✝ : PerfectField K
α : Weight K (↥H) L
x : L
hx : x ∈ H
this :
  {x | ∃ y ∈ rootSpace H ⇑α, ∃ z ∈ rootSpace H (-⇑α), ⁅y, z⁆ = x} ⊆
    ↑(span K {↑((cartanEquivDual H).symm (Weight.toLinear K (↥H) L α))})
hx' : x ∈ span K {x | ∃ y ∈ rootSpace H ⇑α, ∃ z ∈ rootSpace H (-⇑α), ⁅y, z⁆ = x}
⊢ ⟨x, hx⟩ ∈ span K {(cartanEquivDual H).symm (Weight.toLinear K (↥H) L α)}

Tactic:
replace this := Submodule.span_mono this hx'

Result:
case refine_1
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✝ : PerfectField K
α : Weight K (↥H) L
x : L
hx : x ∈ H
hx' : x ∈ span K {x | ∃ y ∈ rootSpace H ⇑α, ∃ z ∈ rootSpace H (-⇑α), ⁅y, z⁆ = x}
this : x ∈ span K ↑(span K {↑((cartanEquivDual H).symm (Weight.toLinear K (↥H) L α))})
⊢ ⟨x, hx⟩ ∈ span K {(cartanEquivDual H).symm (Weight.toLinear K (↥H) L α)}

Proof state:
case intro.intro.intro.intro
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✝ : PerfectField K
α : Weight K (↥H) L
x : L
hx : x ∈ H
hx' : ⟨x, hx⟩ ∈ ↑(corootSpace ⇑α)
e : L
heα : e ∈ rootSpace H ⇑α
f : L
hfα : f ∈ rootSpace H (-⇑α)
⊢ ∃ a,
    a • ↑((cartanEquivDual H).symm (Weight.toLinear K (↥H) L α)) =
      ((killingForm K L) e) f • ↑((cartanEquivDual H).symm (Weight.toLinear K (↥H) L α))

Tactic:
exact ⟨killingForm K L e f, rfl⟩

Result:
no goals

Proof state:
case refine_1
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✝ : PerfectField K
α : Weight K (↥H) L
x : L
hx : x ∈ H
hx' : ⟨x, hx⟩ ∈ ↑(corootSpace ⇑α)
⊢ ⟨x, hx⟩ ∈ span K {(cartanEquivDual H).symm (Weight.toLinear K (↥H) L α)}

Tactic:
have : {⁅y, z⁆ | (y ∈ rootSpace H α) (z ∈ rootSpace H (-α))} ⊆
    K ∙ ((cartanEquivDual H).symm α : L) := by
  rintro - ⟨e, heα, f, hfα, rfl⟩
  rw [lie_eq_killingForm_smul_of_mem_rootSpace_of_mem_rootSpace_neg heα hfα, SetLike.mem_coe,
    Submodule.mem_span_singleton]
  exact ⟨killingForm K L e f, rfl⟩

Result:
case refine_1
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✝ : PerfectField K
α : Weight K (↥H) L
x : L
hx : x ∈ H
hx' : ⟨x, hx⟩ ∈ ↑(corootSpace ⇑α)
this :
  {x | ∃ y ∈ rootSpace H ⇑α, ∃ z ∈ rootSpace H (-⇑α), ⁅y, z⁆ = x} ⊆
    ↑(span K {↑((cartanEquivDual H).symm (Weight.toLinear K (↥H) L α))})
⊢ ⟨x, hx⟩ ∈ span K {(cartanEquivDual H).symm (Weight.toLinear K (↥H) L α)}

Proof state:
case refine_1
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✝ : PerfectField K
α : Weight K (↥H) L
⊢ ↑(corootSpace ⇑α) ≤ span K {(cartanEquivDual H).symm (Weight.toLinear K (↥H) L α)}

Tactic:
intro ⟨x, hx⟩ hx'

Result:
case refine_1
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✝ : PerfectField K
α : Weight K (↥H) L
x : L
hx : x ∈ H
hx' : ⟨x, hx⟩ ∈ ↑(corootSpace ⇑α)
⊢ ⟨x, hx⟩ ∈ span K {(cartanEquivDual H).symm (Weight.toLinear K (↥H) L α)}