-- Module: Mathlib.Algebra.Lie.LieTheorem
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))
n : ℕ
hn :
  ∀ (w : A),
    ∀ 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)
w : A
hm : n + 1 < n + 1 + 1
H :
  ∀ (w : A),
    ⁅w,
        (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)
              n :
            (a : V) → V)
          v⁆ =
      HAdd.hAdd (α := V)
        ((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)
                    n :
                  (a : V) → V)
                v :
              V) :
          V)
        (HSMul.hSMul (β := V) (χ w)
          ((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)
                  n :
                (a : V) → V)
              v :
            V))
inr :
  Membership.mem (γ := Submodule R V)
    (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})
    (HAdd.hAdd (β := V)
      (-HAdd.hAdd (α := V)
          ((T χ ⁅z, 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)
                      n :
                    (a : V) → V)
                  v :
                V) :
            V)
          (HSMul.hSMul (β := V) (χ ⁅z, w⁆)
            ((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)
                    n :
                  (a : V) → V)
                v :
              V)))
      (⁅z,
          (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)
                    n :
                  (a : V) → V)
                v :
              V)⁆ :
        V))
⊢ Membership.mem (α := V) (γ := Submodule R V)
    (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})
    ((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)
                (n + 1) :
              (a : V) → V)
            v :
          V) :
      V)

Tactic:
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]

Premises used: add_sub_assoc, leibniz_lie, sub_self, LinearMap.smul_apply, lie_smul, Module.End.one_apply, LieModule.toEnd_apply_apply, LinearMap.sub_apply, _private.0.LieModule.T, Module.End.mul_apply, add_zero, pow_succ', lie_add, lie_swap_lie