awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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))
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)
w : A
x : V
U : Submodule R V := ⨆ (k : ℕ), (U' : (a : ℕ) → Submodule R V) k
hx : x ∈ U.carrier
rw : ∀ (i : ℕ), Submodule.map (T χ w) ((U' : (a : ℕ) → Submodule R V) i) ≤ U
⊢ Submodule.map (T χ w) U ≤ U

Tactic:
rw [Submodule.map_iSup, iSup_le_iff]

Premises used: Submodule.map_iSup, iSup_le_iff
-- 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))
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)
w : A
x : V
U : Submodule R V := ⨆ (k : ℕ), (U' : (a : ℕ) → Submodule R V) k
hx : x ∈ U.carrier
⊢ Submodule.map (T χ w) ((U' : (a : ℕ) → Submodule R V) 0) ≤ U

Tactic:
simp [U']
-- 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))
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)
w : A
x : V
U : Submodule R V := ⨆ (k : ℕ), (U' : (a : ℕ) → Submodule R V) k
hx : x ∈ U.carrier
i : ℕ
⊢ Submodule.map (T χ w) ((U' : (a : ℕ) → Submodule R V) (i + 1)) ≤ U

Tactic:
(T_apply_succ w i).trans (le_iSup _ _)

Premises used: le_iSup, LE.le.trans
-- 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))
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)
w : A
x : V
U : Submodule R V := ⨆ (k : ℕ), (U' : (a : ℕ) → Submodule R V) k
hx : x ∈ U.carrier
i : ℕ
⊢ Submodule.map (T χ w) ((U' : (a : ℕ) → Submodule R V) (i + 1)) ≤ U

Tactic:
exact (T_apply_succ w i).trans (le_iSup _ _)

Premises used: le_iSup, LE.le.trans
-- 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))
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)
U : LieSubmodule R A V :=
  let __Submodule : Submodule R V := ⨆ (k : ℕ), (U' : (a : ℕ) → Submodule R V) k;
  { toSubmodule := __Submodule, lie_mem := ⋯ }
x : V
hx : x ∈ U
suffices :
  Submodule.map (σ₁₂ := 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 : Submodule R V) ≤
    (↑U : Submodule R V)
⊢ Membership.mem (α := V) U
    (((((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 : V) → V)
        x :
      V)

Tactic:
suffices Submodule.map (π z) U ≤ U from this <| Submodule.mem_map_of_mem hx
-- 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))
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)
U : LieSubmodule R A V :=
  let __Submodule : Submodule R V := ⨆ (k : ℕ), (U' : (a : ℕ) → Submodule R V) k;
  { toSubmodule := __Submodule, lie_mem := ⋯ }
x : V
hx : x ∈ U
simp :
  ∀ (i : ℕ),
    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) i))
      (⨆ (k : ℕ), (U' : (a : ℕ) → Submodule R V) k)
⊢ Submodule.map (σ₁₂ := 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 : Submodule R V) ≤
    (↑U : Submodule R V)

Tactic:
simp only [U, Submodule.map_iSup, iSup_le_iff]

Premises used: Submodule.map_iSup, iSup_le_iff
-- 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))
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)
U : LieSubmodule R A V :=
  let __Submodule : Submodule R V := ⨆ (k : ℕ), (U' : (a : ℕ) → Submodule R V) k;
  { toSubmodule := __Submodule, lie_mem := ⋯ }
x : V
hx : x ∈ U
⊢ ∀ (i : ℕ),
    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) i))
      (⨆ (k : ℕ), (U' : (a : ℕ) → Submodule R V) k)

Tactic:
fun i ↦ (map_U'_le i).trans (le_iSup _ _)

Premises used: le_iSup, HAdd.hAdd, LE.le.trans, OfNat.ofNat, DFunLike.coe
-- 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))
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)
U : LieSubmodule R A V :=
  let __Submodule : Submodule R V := ⨆ (k : ℕ), (U' : (a : ℕ) → Submodule R V) k;
  { toSubmodule := __Submodule, lie_mem := ⋯ }
x : V
hx : x ∈ U
⊢ ∀ (i : ℕ),
    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) i))
      (⨆ (k : ℕ), (U' : (a : ℕ) → Submodule R V) k)

Tactic:
exact fun i ↦ (map_U'_le i).trans (le_iSup _ _)

Premises used: le_iSup, HAdd.hAdd, LE.le.trans, OfNat.ofNat, DFunLike.coe
-- 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))
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)
U : LieSubmodule R A V :=
  let __Submodule : Submodule R V := ⨆ (k : ℕ), (U' : (a : ℕ) → Submodule R V) k;
  { toSubmodule := __Submodule, lie_mem := ⋯ }
⊢ ∀ (x : V) (hx : x ∈ U),
    Membership.mem (α := V) U
      (((((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 : V) → V)
          x :
        V)

Tactic:
have hzU (x : V) (hx : x ∈ U) : (π z) x ∈ U := by
    suffices Submodule.map (π z) U ≤ U from this <| Submodule.mem_map_of_mem hx
    simp only [U, Submodule.map_iSup, iSup_le_iff]
    exact fun i ↦ (map_U'_le i).trans (le_iSup _ _)
-- 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))
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)
U : LieSubmodule R A V :=
  let __Submodule : Submodule R V := ⨆ (k : ℕ), (U' : (a : ℕ) → Submodule R V) k;
  { toSubmodule := __Submodule, lie_mem := ⋯ }
hzU :
  ∀ (x : V) (hx : x ∈ U),
    Membership.mem (α := V) U
      (((((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 : V) → V)
          x :
        V)
x : V
hx : x ∈ U
h : ⁅⁅z, a⁆, x⁆ = ⁅z, ⁅a, x⁆⁆ - ⁅a, ⁅z, x⁆⁆
⊢ Eq.{u_4 + 1} (α := V)
    (↑(((((toEnd.{u_1, u_3, u_4} R A ↥U : LieHom.{u_1, u_3, u_4} R A (Module.End R ↥U)) : (a : A) → Module.End R ↥U)
                ⁅z, a⁆ :
              Module.End R ↥U) :
            (a : ↥U) → ↥U)
          (Subtype.mk (p := fun (x : V) ↦ x ∈ U) x hx)) :
      V)
    (↑(((⁅LinearMap.restrict
                  (((toEnd R L V : LieHom.{u_1, u_2, u_4} R L (Module.End R V)) : (a : L) → Module.End R V) z) hzU,
                ((toEnd.{u_1, u_3, u_4} R A ↥U : LieHom.{u_1, u_3, u_4} R A (Module.End R ↥U)) :
                    (a : A) → Module.End R ↥U)
                  a⁆ :
              Module.End R ↥U) :
            (a : ↥U) → ↥U)
          (Subtype.mk (p := fun (x : V) ↦ x ∈ U) x hx)) :
      V)

Tactic:
change ⁅⁅z, a⁆, x⁆ = ⁅z, ⁅a, x⁆⁆ - ⁅a, ⁅z, x⁆⁆
-- 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))
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)
U : LieSubmodule R A V :=
  let __Submodule : Submodule R V := ⨆ (k : ℕ), (U' : (a : ℕ) → Submodule R V) k;
  { toSubmodule := __Submodule, lie_mem := ⋯ }
hzU :
  ∀ (x : V) (hx : x ∈ U),
    Membership.mem (α := V) U
      (((((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 : V) → V)
          x :
        V)
x : V
hx : x ∈ U
⊢ ⁅⁅z, a⁆, x⁆ = ⁅z, ⁅a, x⁆⁆ - ⁅a, ⁅z, x⁆⁆

Tactic:
simp only [leibniz_lie z a, add_sub_cancel_right]

Premises used: leibniz_lie, add_sub_cancel_right