-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Killing (goal)
Goal:
K : Type u_2
L : Type u_3
inst : LieRing L
inst_1 : Field K
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : IsKilling K L
inst_6 : IsTriangularizable K (↥H) L
inst_7 : CharZero K
α : Weight K (↥H) L
x y : ↥H
hx : Membership.mem (γ := Submodule K ↥H) (Weight.ker (M := L) (χ := α)) x
hy :
  Membership.mem (γ := Submodule K ↥H)
    (span K
      {x : ↥H | ∃ y ∈ rootSpace H (⇑α : (a : ↥H) → K), ∃ z ∈ rootSpace H (-(⇑α : (a : ↥H) → K)), ⁅y, z⁆ = (↑x : L)})
    y
mem :
  ∀ (z : ↥H)
    (hz :
      Membership.mem (γ := Set ↥H)
        {x : ↥H | ∃ y ∈ rootSpace H (⇑α : (a : ↥H) → K), ∃ z ∈ rootSpace H (-(⇑α : (a : ↥H) → K)), ⁅y, z⁆ = (↑x : L)}
        z),
    Eq.{u_2 + 1} (α := K)
      ((((traceForm K (↥H) L : (a : ↥H) → ↥H →ₗ[K] K) x : LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id K) (↥H) K) :
            (a : ↥H) → K)
          z :
        K)
      (0 : K)
zero :
  Eq.{u_2 + 1} (α := K)
    ((((traceForm K (↥H) L : (a : ↥H) → ↥H →ₗ[K] K) x : LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id K) (↥H) K) :
          (a : ↥H) → K)
        0 :
      K)
    (0 : K)
add :
  ∀ (x_1 y : ↥H),
    Membership.mem (γ := Submodule K ↥H)
        (span K
          {x : ↥H | ∃ y ∈ rootSpace H (⇑α : (a : ↥H) → K), ∃ z ∈ rootSpace H (-(⇑α : (a : ↥H) → K)), ⁅y, z⁆ = (↑x : L)})
        x_1 →
      Membership.mem (γ := Submodule K ↥H)
          (span K
            {x : ↥H |
              ∃ y ∈ rootSpace H (⇑α : (a : ↥H) → K), ∃ z ∈ rootSpace H (-(⇑α : (a : ↥H) → K)), ⁅y, z⁆ = (↑x : L)})
          y →
        ∀
          (hx :
            Eq.{u_2 + 1} (α := K)
              ((((traceForm K (↥H) L : (a : ↥H) → ↥H →ₗ[K] K) x :
                      LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id K) (↥H) K) :
                    (a : ↥H) → K)
                  x_1 :
                K)
              (0 : K))
          (hy :
            Eq.{u_2 + 1} (α := K)
              ((((traceForm K (↥H) L : (a : ↥H) → ↥H →ₗ[K] K) x :
                      LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id K) (↥H) K) :
                    (a : ↥H) → K)
                  y :
                K)
              (0 : K)),
          Eq.{u_2 + 1} (α := K)
            ((((traceForm K (↥H) L : (a : ↥H) → ↥H →ₗ[K] K) x : LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id K) (↥H) K) :
                  (a : ↥H) → K)
                (x_1 + y) :
              K)
            (0 : K)
⊢ Eq.{u_2 + 1} (α := K)
    ((((traceForm K (↥H) L : (a : ↥H) → ↥H →ₗ[K] K) x : LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id K) (↥H) K) :
          (a : ↥H) → K)
        y :
      K)
    (0 : K)
have smul : ∀ (a : K) (x_1 : ↥H),
  Membership.mem (γ := Submodule K ↥H)
      (span K
        {x : ↥H | ∃ y ∈ rootSpace H (⇑α : (a : ↥H) → K), ∃ z ∈ rootSpace H (-(⇑α : (a : ↥H) → K)), ⁅y, z⁆ = (↑x : L)})
      x_1 →
    ∀
      (hz :
        Eq.{u_2 + 1} (α := K)
          ((((traceForm K (↥H) L : (a : ↥H) → ↥H →ₗ[K] K) x : LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id K) (↥H) K) :
                (a : ↥H) → K)
              x_1 :
            K)
          (0 : K)),
      Eq.{u_2 + 1} (α := K)
        ((((traceForm K (↥H) L : (a : ↥H) → ↥H →ₗ[K] K) x : LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id K) (↥H) K) :
              (a : ↥H) → K)
            (a • x_1) :
          K)
        (0 : K)
Tactic: induction hy using Submodule.span_induction with
  | mem z hz =>
    obtain ⟨u, hu, v, -, huv⟩ := hz
    change killingForm K L (x : L) (z : L) = 0
    replace hx : α x = 0 := by simpa using hx
    rw [← huv, ← traceForm_apply_lie_apply, ← LieSubalgebra.coe_bracket_of_module,
      lie_eq_smul_of_mem_rootSpace hu, hx, zero_smul, map_zero, LinearMap.zero_apply]
  | zero => simp
  | add _ _ _ _ hx hy => simp [hx, hy]
  | smul _ _ _ hz => simp [hz]
Cleared hypotheses: hy