awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Lie.LieTheorem (goal)
Goal:
R : Type u_1
L : Type u_2
A : Type u_3
V : Type u_4
inst : CommRing R
inst_1 : IsPrincipalIdealRing R
inst_2 : IsDomain R
inst_3 : CharZero R
inst_4 : LieRing L
inst_5 : LieAlgebra R L
inst_6 : LieRing A
inst_7 : LieAlgebra R A
inst_8 : Bracket L A
inst_9 : Bracket A L
inst_10 : AddCommGroup V
inst_11 : Module R V
inst_12 : Module.Free R V
inst_13 : Module.Finite R V
inst_14 : LieRingModule L V
inst_15 : LieModule R L V
inst_16 : LieRingModule A V
inst_17 : LieModule R A V
inst_18 : IsLieTower L A V
inst_19 : IsLieTower A L V
χ : A → R
z : L
v : V
hv : ∀ (x : A), ⁅x, v⁆ = χ x • v
a : A
hv' : v ≠ 0
this : χ ⁅z, a⁆ = 0
rw : ⁅⁅a, z⁆, v⁆ + ⁅z, ⁅a, v⁆⁆ = χ a • ⁅z, v⁆
rw₁ : ⁅⁅a, z⁆, v⁆ + ⁅z, χ a • v⁆ = χ a • ⁅z, v⁆
rw₂ : ⁅⁅a, z⁆, v⁆ + χ a • ⁅z, v⁆ = χ a • ⁅z, v⁆
rw₃ : -⁅⁅z, a⁆, v⁆ + χ a • ⁅z, v⁆ = χ a • ⁅z, v⁆
rw₄ : -(χ ⁅z, a⁆ • v) + χ a • ⁅z, v⁆ = χ a • ⁅z, v⁆
rw₅ : -HSMul.hSMul.{u_1, u_4, u_4} (α := R) 0 v + χ a • ⁅z, v⁆ = χ a • ⁅z, v⁆
rw₆ : -0 + χ a • ⁅z, v⁆ = χ a • ⁅z, v⁆
rw₇ : 0 + χ a • ⁅z, v⁆ = χ a • ⁅z, v⁆
⊢ ⁅a, ⁅z, v⁆⁆ = χ a • ⁅z, v⁆
have rw₈ : χ a • ⁅z, v⁆ = χ a • ⁅z, v⁆
Tactic: rw [leibniz_lie, hv a, lie_smul, lie_swap_lie, hv, this, zero_smul, neg_zero, zero_add]
-- Lean 4 proof step from Mathlib.Algebra.Lie.LieTheorem (goal)
Goal:
R : Type u_1
L : Type u_2
A : Type u_3
V : Type u_4
inst : CommRing R
inst_1 : IsPrincipalIdealRing R
inst_2 : IsDomain R
inst_3 : CharZero R
inst_4 : LieRing L
inst_5 : LieAlgebra R L
inst_6 : LieRing A
inst_7 : LieAlgebra R A
inst_8 : Bracket L A
inst_9 : Bracket A L
inst_10 : AddCommGroup V
inst_11 : Module R V
inst_12 : Module.Free R V
inst_13 : Module.Finite R V
inst_14 : LieRingModule L V
inst_15 : LieModule R L V
inst_16 : LieRingModule A V
inst_17 : LieModule R A V
inst_18 : IsLieTower L A V
inst_19 : IsLieTower A L V
χ : A → R
z : L
v : V
hv : ∀ (x : A), ⁅x, v⁆ = χ x • v
a : A
hv' : v ≠ 0
⊢ ⁅a, ⁅z, v⁆⁆ = χ a • ⁅z, v⁆
have inr : χ ⁅z, a⁆ = 0
Tactic: suffices χ ⁅z, a⁆ = 0 by
    rw [leibniz_lie, hv a, lie_smul, lie_swap_lie, hv, this, zero_smul, neg_zero, zero_add]
-- Lean 4 proof step from Mathlib.Algebra.Lie.LieTheorem (goal)
Goal:
R : Type u_1
L : Type u_2
A : Type u_3
V : Type u_4
inst : CommRing R
inst_1 : IsPrincipalIdealRing R
inst_2 : IsDomain R
inst_3 : CharZero R
inst_4 : LieRing L
inst_5 : LieAlgebra R L
inst_6 : LieRing A
inst_7 : LieAlgebra R A
inst_8 : Bracket L A
inst_9 : Bracket A L
inst_10 : AddCommGroup V
inst_11 : Module R V
inst_12 : Module.Free R V
inst_13 : Module.Finite R V
inst_14 : LieRingModule L V
inst_15 : LieModule R L V
inst_16 : LieRingModule A V
inst_17 : LieModule R A V
inst_18 : IsLieTower L A V
inst_19 : IsLieTower A L V
χ : A → R
z : L
v : V
hv : ∀ (x : A), ⁅x, v⁆ = χ x • v
a : A
hv' : v ≠ 0
U' : ℕ →o Submodule R V :=
  {
    toFun := fun (n : ℕ) ↦
      Submodule.span R
        {x : V |
          ∃ i < n,
            (HPow.hPow (α := Module.End R V)
                    (((toEnd R L V : LieHom.{u_1, u_2, u_4} R L (Module.End R V)) : (a : L) → Module.End R V) z :
                      Module.End R V)
                    i :
                  (a : V) → V)
                v =
              x},
    monotone' := ⋯ }
n : ℕ
⊢ LE.le.{u_4} (α := Submodule R V)
    (Submodule.map (R := R) (M := V) (σ₁₂ := RingHom.id R)
      (((toEnd R L V : LieHom.{u_1, u_2, u_4} R L (Module.End R V)) : (a : L) → Module.End R V) z)
      ((U' : (a : ℕ) → Submodule R V) n))
    ((U' : (a : ℕ) → Submodule R V) (n + 1))
have simp : LE.le.{u_4} (α := Submodule R V)
  (Submodule.span R
    ((fun (a : V) ↦ ⁅z, a⁆) ''
      {x : V |
        ∃ i < n,
          (HPow.hPow (α := Module.End R V)
                  (((toEnd R L V : LieHom.{u_1, u_2, u_4} R L (Module.End R V)) : (a : L) → Module.End R V) z :
                    Module.End R V)
                  i :
                (a : V) → V)
              v =
            x}))
  (Submodule.span R
    {x : V |
      ∃ i < n + 1,
        (HPow.hPow (α := Module.End R V)
                (((toEnd R L V : LieHom.{u_1, u_2, u_4} R L (Module.End R V)) : (a : L) → Module.End R V) z :
                  Module.End R V)
                i :
              (a : V) → V)
            v =
          x})
Tactic: simp only [OrderHom.coe_mk, Submodule.map_span, toEnd_apply_apply, U']
-- Lean 4 proof step from Mathlib.Algebra.Lie.LieTheorem (goal)
Goal:
R : Type u_1
L : Type u_2
A : Type u_3
V : Type u_4
inst : CommRing R
inst_1 : IsPrincipalIdealRing R
inst_2 : IsDomain R
inst_3 : CharZero R
inst_4 : LieRing L
inst_5 : LieAlgebra R L
inst_6 : LieRing A
inst_7 : LieAlgebra R A
inst_8 : Bracket L A
inst_9 : Bracket A L
inst_10 : AddCommGroup V
inst_11 : Module R V
inst_12 : Module.Free R V
inst_13 : Module.Finite R V
inst_14 : LieRingModule L V
inst_15 : LieModule R L V
inst_16 : LieRingModule A V
inst_17 : LieModule R A V
inst_18 : IsLieTower L A V
inst_19 : IsLieTower A L V
χ : A → R
z : L
v : V
hv : ∀ (x : A), ⁅x, v⁆ = χ x • v
a : A
hv' : v ≠ 0
U' : ℕ →o Submodule R V :=
  {
    toFun := fun (n : ℕ) ↦
      Submodule.span R
        {x : V |
          ∃ i < n,
            (HPow.hPow (α := Module.End R V)
                    (((toEnd R L V : LieHom.{u_1, u_2, u_4} R L (Module.End R V)) : (a : L) → Module.End R V) z :
                      Module.End R V)
                    i :
                  (a : V) → V)
                v =
              x},
    monotone' := ⋯ }
n : ℕ
⊢ LE.le.{u_4} (α := Submodule R V)
    (Submodule.span R
      ((fun (a : V) ↦ ⁅z, a⁆) ''
        {x : V |
          ∃ i < n,
            (HPow.hPow (α := Module.End R V)
                    (((toEnd R L V : LieHom.{u_1, u_2, u_4} R L (Module.End R V)) : (a : L) → Module.End R V) z :
                      Module.End R V)
                    i :
                  (a : V) → V)
                v =
              x}))
    (Submodule.span R
      {x : V |
        ∃ i < n + 1,
          (HPow.hPow (α := Module.End R V)
                  (((toEnd R L V : LieHom.{u_1, u_2, u_4} R L (Module.End R V)) : (a : L) → Module.End R V) z :
                    Module.End R V)
                  i :
                (a : V) → V)
              v =
            x})
have h : Subset.{u_4} (α := Set V)
  ((fun (a : V) ↦ ⁅z, a⁆) ''
    {x : V |
      ∃ i < n,
        (HPow.hPow (α := Module.End R V)
                (((toEnd R L V : LieHom.{u_1, u_2, u_4} R L (Module.End R V)) : (a : L) → Module.End R V) z :
                  Module.End R V)
                i :
              (a : V) → V)
            v =
          x})
  {x : V |
    ∃ i < n + 1,
      (HPow.hPow (α := Module.End R V)
              (((toEnd R L V : LieHom.{u_1, u_2, u_4} R L (Module.End R V)) : (a : L) → Module.End R V) z :
                Module.End R V)
              i :
            (a : V) → V)
          v =
        x}
Tactic: apply Submodule.span_mono
-- Lean 4 proof step from Mathlib.Algebra.Lie.LieTheorem (goal)
Goal:
R : Type u_1
L : Type u_2
A : Type u_3
V : Type u_4
inst : CommRing R
inst_1 : IsPrincipalIdealRing R
inst_2 : IsDomain R
inst_3 : CharZero R
inst_4 : LieRing L
inst_5 : LieAlgebra R L
inst_6 : LieRing A
inst_7 : LieAlgebra R A
inst_8 : Bracket L A
inst_9 : Bracket A L
inst_10 : AddCommGroup V
inst_11 : Module R V
inst_12 : Module.Free R V
inst_13 : Module.Finite R V
inst_14 : LieRingModule L V
inst_15 : LieModule R L V
inst_16 : LieRingModule A V
inst_17 : LieModule R A V
inst_18 : IsLieTower L A V
inst_19 : IsLieTower A L V
χ : A → R
z : L
v : V
hv : ∀ (x : A), ⁅x, v⁆ = χ x • v
a : A
hv' : v ≠ 0
U' : ℕ →o Submodule R V :=
  {
    toFun := fun (n : ℕ) ↦
      Submodule.span R
        {x : V |
          ∃ i < n,
            (HPow.hPow (α := Module.End R V)
                    (((toEnd R L V : LieHom.{u_1, u_2, u_4} R L (Module.End R V)) : (a : L) → Module.End R V) z :
                      Module.End R V)
                    i :
                  (a : V) → V)
                v =
              x},
    monotone' := ⋯ }
n : ℕ
⊢ Subset.{u_4} (α := Set V)
    ((fun (a : V) ↦ ⁅z, a⁆) ''
      {x : V |
        ∃ i < n,
          (HPow.hPow (α := Module.End R V)
                  (((toEnd R L V : LieHom.{u_1, u_2, u_4} R L (Module.End R V)) : (a : L) → Module.End R V) z :
                    Module.End R V)
                  i :
                (a : V) → V)
              v =
            x})
    {x : V |
      ∃ i < n + 1,
        (HPow.hPow (α := Module.End R V)
                (((toEnd R L V : LieHom.{u_1, u_2, u_4} R L (Module.End R V)) : (a : L) → Module.End R V) z :
                  Module.End R V)
                i :
              (a : V) → V)
            v =
          x}
have h : ∀ a < n,
  ∃ b < n + 1,
    Eq (α := V)
      ((HPow.hPow (α := Module.End R V)
              (((toEnd R L V : LieHom.{u_1, u_2, u_4} R L (Module.End R V)) : (a : L) → Module.End R V) z :
                Module.End R V)
              b :
            (a : V) → V)
          v :
        V)
      ((HPow.hPow (α := Module.End R V)
              (((toEnd R L V : LieHom.{u_1, u_2, u_4} R L (Module.End R V)) : (a : L) → Module.End R V) z :
                Module.End R V)
              (a + 1) :
            (a : V) → V)
          v :
        V)
Tactic: suffices ∀ a < n, ∃ b < n + 1, ((π z) ^ b) v = ((π z) ^ (a + 1)) v by simpa [pow_succ']
-- Lean 4 proof step from Mathlib.Algebra.Lie.LieTheorem (hypothesis)
Goal:
R : Type u_1
L : Type u_2
A : Type u_3
V : Type u_4
inst : CommRing R
inst_1 : IsPrincipalIdealRing R
inst_2 : IsDomain R
inst_3 : CharZero R
inst_4 : LieRing L
inst_5 : LieAlgebra R L
inst_6 : LieRing A
inst_7 : LieAlgebra R A
inst_8 : Bracket L A
inst_9 : Bracket A L
inst_10 : AddCommGroup V
inst_11 : Module R V
inst_12 : Module.Free R V
inst_13 : Module.Finite R V
inst_14 : LieRingModule L V
inst_15 : LieModule R L V
inst_16 : LieRingModule A V
inst_17 : LieModule R A V
inst_18 : IsLieTower L A V
inst_19 : IsLieTower A L V
χ : A → R
z : L
v : V
hv : ∀ (x : A), ⁅x, v⁆ = χ x • v
a : A
hv' : v ≠ 0
U' : ℕ →o Submodule R V :=
  {
    toFun := fun (n : ℕ) ↦
      Submodule.span R
        {x : V |
          ∃ i < n,
            (HPow.hPow (α := Module.End R V)
                    (((toEnd R L V : LieHom.{u_1, u_2, u_4} R L (Module.End R V)) : (a : L) → Module.End R V) z :
                      Module.End R V)
                    i :
                  (a : V) → V)
                v =
              x},
    monotone' := ⋯ }
⊢ χ ⁅z, a⁆ = 0
have map_U'_le : ∀ (n : ℕ),
  LE.le.{u_4} (α := Submodule R V)
    (Submodule.map (R := R) (M := V) (σ₁₂ := RingHom.id R)
      (((toEnd R L V : LieHom.{u_1, u_2, u_4} R L (Module.End R V)) : (a : L) → Module.End R V) z)
      ((U' : (a : ℕ) → Submodule R V) n))
    ((U' : (a : ℕ) → Submodule R V) (n + 1))
Tactic: have map_U'_le (n : ℕ) : Submodule.map (π z) (U' n) ≤ U' (n + 1) := by
    simp only [OrderHom.coe_mk, Submodule.map_span, toEnd_apply_apply, U']
    apply Submodule.span_mono
    suffices ∀ a < n, ∃ b < n + 1, ((π z) ^ b) v = ((π z) ^ (a + 1)) v by simpa [pow_succ']
    aesop
-- Lean 4 proof step from Mathlib.Algebra.Lie.LieTheorem (goal)
Goal:
R : Type u_1
L : Type u_2
A : Type u_3
V : Type u_4
inst : CommRing R
inst_1 : IsPrincipalIdealRing R
inst_2 : IsDomain R
inst_3 : CharZero R
inst_4 : LieRing L
inst_5 : LieAlgebra R L
inst_6 : LieRing A
inst_7 : LieAlgebra R A
inst_8 : Bracket L A
inst_9 : Bracket A L
inst_10 : AddCommGroup V
inst_11 : Module R V
inst_12 : Module.Free R V
inst_13 : Module.Finite R V
inst_14 : LieRingModule L V
inst_15 : LieModule R L V
inst_16 : LieRingModule A V
inst_17 : LieModule R A V
inst_18 : IsLieTower L A V
inst_19 : IsLieTower A L V
χ : A → R
z : L
v : V
hv : ∀ (x : A), ⁅x, v⁆ = χ x • v
a : A
hv' : v ≠ 0
U' : ℕ →o Submodule R V :=
  {
    toFun := fun (n : ℕ) ↦
      Submodule.span R
        {x : V |
          ∃ i < n,
            (HPow.hPow (α := Module.End R V)
                    (((toEnd R L V : LieHom.{u_1, u_2, u_4} R L (Module.End R V)) : (a : L) → Module.End R V) z :
                      Module.End R V)
                    i :
                  (a : V) → V)
                v =
              x},
    monotone' := ⋯ }
map_U'_le :
  ∀ (n : ℕ),
    LE.le.{u_4} (α := Submodule R V)
      (Submodule.map (R := R) (M := V) (σ₁₂ := RingHom.id R)
        (((toEnd R L V : LieHom.{u_1, u_2, u_4} R L (Module.End R V)) : (a : L) → Module.End R V) z)
        ((U' : (a : ℕ) → Submodule R V) n))
      ((U' : (a : ℕ) → Submodule R V) (n + 1))
w : A
n : ℕ
⊢ LE.le.{u_4} (α := Submodule R V) (Submodule.map (T χ w) ((U' : (a : ℕ) → Submodule R V) (n + 1)))
    ((U' : (a : ℕ) → Submodule R V) n)
have simp : Subset (α := Set V)
  {x : V |
    ∃ i < n + 1,
      (HPow.hPow (α := Module.End R V)
              (((toEnd R L V : LieHom.{u_1, u_2, u_4} R L (Module.End R V)) : (a : L) → Module.End R V) z :
                Module.End R V)
              i :
            (a : V) → V)
          v =
        x}
  ((⇑(T χ w) : (a : V) → V) ⁻¹'
    (↑(Submodule.span R
          {x : V |
            ∃ i < n,
              (HPow.hPow (α := Module.End R V)
                      (((toEnd R L V : LieHom.{u_1, u_2, u_4} R L (Module.End R V)) : (a : L) → Module.End R V) z :
                        Module.End R V)
                      i :
                    (a : V) → V)
                  v =
                x}) :
      Set V))
Tactic: simp only [OrderHom.coe_mk, U', Submodule.map_span, Submodule.span_le, Set.image_subset_iff]
-- Lean 4 proof step from Mathlib.Algebra.Lie.LieTheorem (goal)
Goal:
R : Type u_1
L : Type u_2
A : Type u_3
V : Type u_4
inst : CommRing R
inst_1 : IsPrincipalIdealRing R
inst_2 : IsDomain R
inst_3 : CharZero R
inst_4 : LieRing L
inst_5 : LieAlgebra R L
inst_6 : LieRing A
inst_7 : LieAlgebra R A
inst_8 : Bracket L A
inst_9 : Bracket A L
inst_10 : AddCommGroup V
inst_11 : Module R V
inst_12 : Module.Free R V
inst_13 : Module.Finite R V
inst_14 : LieRingModule L V
inst_15 : LieModule R L V
inst_16 : LieRingModule A V
inst_17 : LieModule R A V
inst_18 : IsLieTower L A V
inst_19 : IsLieTower A L V
χ : A → R
z : L
v : V
hv : ∀ (x : A), ⁅x, v⁆ = χ x • v
a : A
hv' : v ≠ 0
U' : ℕ →o Submodule R V :=
  {
    toFun := fun (n : ℕ) ↦
      Submodule.span R
        {x : V |
          ∃ i < n,
            (HPow.hPow (α := Module.End R V)
                    (((toEnd R L V : LieHom.{u_1, u_2, u_4} R L (Module.End R V)) : (a : L) → Module.End R V) z :
                      Module.End R V)
                    i :
                  (a : V) → V)
                v =
              x},
    monotone' := ⋯ }
map_U'_le :
  ∀ (n : ℕ),
    LE.le.{u_4} (α := Submodule R V)
      (Submodule.map (R := R) (M := V) (σ₁₂ := RingHom.id R)
        (((toEnd R L V : LieHom.{u_1, u_2, u_4} R L (Module.End R V)) : (a : L) → Module.End R V) z)
        ((U' : (a : ℕ) → Submodule R V) n))
      ((U' : (a : ℕ) → Submodule R V) (n + 1))
w : A
n : ℕ
⊢ Subset (α := Set V)
    {x : V |
      ∃ i < n + 1,
        (HPow.hPow (α := Module.End R V)
                (((toEnd R L V : LieHom.{u_1, u_2, u_4} R L (Module.End R V)) : (a : L) → Module.End R V) z :
                  Module.End R V)
                i :
              (a : V) → V)
            v =
          x}
    ((⇑(T χ w) : (a : V) → V) ⁻¹'
      (↑(Submodule.span R
            {x : V |
              ∃ i < n,
                (HPow.hPow (α := Module.End R V)
                        (((toEnd R L V : LieHom.{u_1, u_2, u_4} R L (Module.End R V)) : (a : L) → Module.End R V) z :
                          Module.End R V)
                        i :
                      (a : V) → V)
                    v =
                  x}) :
        Set V))
have simp : ∀ a < n + 1,
  Membership.mem (α := V) (γ := Submodule R V)
    (Submodule.span R
      {x : V |
        ∃ i < n,
          (HPow.hPow (α := Module.End R V)
                  (((toEnd R L V : LieHom.{u_1, u_2, u_4} R L (Module.End R V)) : (a : L) → Module.End R V) z :
                    Module.End R V)
                  i :
                (a : V) → V)
              v =
            x})
    ((T χ w : (a : V) → V)
        ((HPow.hPow (α := Module.End R V)
                (((toEnd R L V : LieHom.{u_1, u_2, u_4} R L (Module.End R V)) : (a : L) → Module.End R V) z :
                  Module.End R V)
                a :
              (a : V) → V)
            v :
          V) :
      V)
Tactic: simp only [Set.subset_def, Set.mem_setOf_eq, Set.mem_preimage, SetLike.mem_coe,
      forall_exists_index, and_imp, forall_apply_eq_imp_iff₂]
-- Lean 4 proof step from Mathlib.Algebra.Lie.LieTheorem (goal)
Goal:
R : Type u_1
L : Type u_2
A : Type u_3
V : Type u_4
inst : CommRing R
inst_1 : IsPrincipalIdealRing R
inst_2 : IsDomain R
inst_3 : CharZero R
inst_4 : LieRing L
inst_5 : LieAlgebra R L
inst_6 : LieRing A
inst_7 : LieAlgebra R A
inst_8 : Bracket L A
inst_9 : Bracket A L
inst_10 : AddCommGroup V
inst_11 : Module R V
inst_12 : Module.Free R V
inst_13 : Module.Finite R V
inst_14 : LieRingModule L V
inst_15 : LieModule R L V
inst_16 : LieRingModule A V
inst_17 : LieModule R A V
inst_18 : IsLieTower L A V
inst_19 : IsLieTower A L V
χ : A → R
z : L
v : V
hv : ∀ (x : A), ⁅x, v⁆ = χ x • v
a : A
hv' : v ≠ 0
U' : ℕ →o Submodule R V :=
  {
    toFun := fun (n : ℕ) ↦
      Submodule.span R
        {x : V |
          ∃ i < n,
            (HPow.hPow (α := Module.End R V)
                    (((toEnd R L V : LieHom.{u_1, u_2, u_4} R L (Module.End R V)) : (a : L) → Module.End R V) z :
                      Module.End R V)
                    i :
                  (a : V) → V)
                v =
              x},
    monotone' := ⋯ }
map_U'_le :
  ∀ (n : ℕ),
    LE.le.{u_4} (α := Submodule R V)
      (Submodule.map (R := R) (M := V) (σ₁₂ := RingHom.id R)
        (((toEnd R L V : LieHom.{u_1, u_2, u_4} R L (Module.End R V)) : (a : L) → Module.End R V) z)
        ((U' : (a : ℕ) → Submodule R V) n))
      ((U' : (a : ℕ) → Submodule R V) (n + 1))
w : A
n : ℕ
⊢ ∀ a < n + 1,
    Membership.mem (α := V) (γ := Submodule R V)
      (Submodule.span R
        {x : V |
          ∃ i < n,
            (HPow.hPow (α := Module.End R V)
                    (((toEnd R L V : LieHom.{u_1, u_2, u_4} R L (Module.End R V)) : (a : L) → Module.End R V) z :
                      Module.End R V)
                    i :
                  (a : V) → V)
                v =
              x})
      ((T χ w : (a : V) → V)
          ((HPow.hPow (α := Module.End R V)
                  (((toEnd R L V : LieHom.{u_1, u_2, u_4} R L (Module.End R V)) : (a : L) → Module.End R V) z :
                    Module.End R V)
                  a :
                (a : V) → V)
              v :
            V) :
        V)
have zero : ∀ (w : A),
  ∀ a < HAdd.hAdd (α := ℕ) 0 1,
    Membership.mem (α := V) (γ := Submodule R V)
      (Submodule.span R
        {x : V |
          ∃ i < 0,
            (HPow.hPow (α := Module.End R V)
                    (((toEnd R L V : LieHom.{u_1, u_2, u_4} R L (Module.End R V)) : (a : L) → Module.End R V) z :
                      Module.End R V)
                    i :
                  (a : V) → V)
                v =
              x})
      ((T χ w : (a : V) → V)
          ((HPow.hPow (α := Module.End R V)
                  (((toEnd R L V : LieHom.{u_1, u_2, u_4} R L (Module.End R V)) : (a : L) → Module.End R V) z :
                    Module.End R V)
                  a :
                (a : V) → V)
              v :
            V) :
        V)
Tactic: induction n generalizing w
Cleared hypotheses: w, n
-- Lean 4 proof step from Mathlib.Algebra.Lie.LieTheorem (hypothesis)
Goal:
R : Type u_1
L : Type u_2
A : Type u_3
V : Type u_4
inst : CommRing R
inst_1 : IsPrincipalIdealRing R
inst_2 : IsDomain R
inst_3 : CharZero R
inst_4 : LieRing L
inst_5 : LieAlgebra R L
inst_6 : LieRing A
inst_7 : LieAlgebra R A
inst_8 : Bracket L A
inst_9 : Bracket A L
inst_10 : AddCommGroup V
inst_11 : Module R V
inst_12 : Module.Free R V
inst_13 : Module.Finite R V
inst_14 : LieRingModule L V
inst_15 : LieModule R L V
inst_16 : LieRingModule A V
inst_17 : LieModule R A V
inst_18 : IsLieTower L A V
inst_19 : IsLieTower A L V
χ : A → R
z : L
v : V
hv : ∀ (x : A), ⁅x, v⁆ = χ x • v
a : A
hv' : v ≠ 0
U' : ℕ →o Submodule R V :=
  {
    toFun := fun (n : ℕ) ↦
      Submodule.span R
        {x : V |
          ∃ i < n,
            (HPow.hPow (α := Module.End R V)
                    (((toEnd R L V : LieHom.{u_1, u_2, u_4} R L (Module.End R V)) : (a : L) → Module.End R V) z :
                      Module.End R V)
                    i :
                  (a : V) → V)
                v =
              x},
    monotone' := ⋯ }
map_U'_le :
  ∀ (n : ℕ),
    LE.le.{u_4} (α := Submodule R V)
      (Submodule.map (R := R) (M := V) (σ₁₂ := RingHom.id R)
        (((toEnd R L V : LieHom.{u_1, u_2, u_4} R L (Module.End R V)) : (a : L) → Module.End R V) z)
        ((U' : (a : ℕ) → Submodule R V) n))
      ((U' : (a : ℕ) → Submodule R V) (n + 1))
⊢ χ ⁅z, a⁆ = 0
have T_apply_succ : ∀ (w : A) (n : ℕ),
  LE.le.{u_4} (α := Submodule R V) (Submodule.map (T χ w) ((U' : (a : ℕ) → Submodule R V) (n + 1)))
    ((U' : (a : ℕ) → Submodule R V) n)
Tactic: have T_apply_succ (w : A) (n : ℕ) :
      Submodule.map (T χ w) (U' (n + 1)) ≤ U' n := by
    simp only [OrderHom.coe_mk, U', Submodule.map_span, Submodule.span_le, Set.image_subset_iff]
    simp only [Set.subset_def, Set.mem_setOf_eq, Set.mem_preimage, SetLike.mem_coe,
      forall_exists_index, and_imp, forall_apply_eq_imp_iff₂]
    induction n generalizing w
    · simp only [zero_add, Nat.lt_one_iff, LinearMap.sub_apply, LieModule.toEnd_apply_apply,
        LinearMap.smul_apply, Module.End.one_apply, forall_eq, pow_zero, hv w, sub_self, zero_mem]
    · next n hn =>
      intro m hm
      obtain (hm | rfl) : m < n + 1 ∨ m = n + 1 := by lia
      · exact U'.mono (Nat.le_succ n) (hn w m hm)
      have H : ∀ w, ⁅w, (π z ^ n) v⁆ = (T χ w) ((π z ^ n) v) + χ w • ((π z ^ n) v) := by simp
      rw [T, LinearMap.sub_apply, pow_succ', Module.End.mul_apply, LieModule.toEnd_apply_apply,
        LieModule.toEnd_apply_apply, LinearMap.smul_apply, Module.End.one_apply, leibniz_lie,
        lie_swap_lie w z, H, H, lie_add, lie_smul, add_sub_assoc, add_sub_assoc, sub_self, add_zero]
      refine add_mem (neg_mem <| add_mem ?_ ?_) ?_
      · exact U'.mono n.le_succ (hn _ n n.lt_succ_self)
      · exact Submodule.smul_mem _ _ (Submodule.subset_span ⟨n, n.lt_succ_self, rfl⟩)
      · exact map_U'_le _ <| Submodule.mem_map_of_mem <| hn w n n.lt_succ_self