awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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))
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)
trace_za_zero :
  Eq.{u_1 + 1} (α := R)
    ((LinearMap.trace R ↥U : (a : ↥U →ₗ[R] ↥U) → R)
        (((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) :
      R)
    (0 : R)
w : A
key :
  ∀ (i : ℕ) (hi : i ≠ 0),
    ∃ j < i,
      LE.le.{u_4} (α := Submodule R V) (Submodule.map (T χ w) ((U' : (a : ℕ) → Submodule R V) i))
        ((U' : (a : ℕ) → Submodule R V) j)
x : ↥U
this : Membership.mem (γ := Submodule R V) (Module.End.maxGenEigenspace (T χ w) 0) (↑x : V)
⊢ ∃ (n : ℕ),
    Eq (α := ↥U)
      ((HPow.hPow (α := Module.End R ↥U) (T.{u_1, u_3, u_4} (V := ↥U) χ w : Module.End R ↥U) n : (a : ↥U) → ↥U) x : ↥U)
      (0 : ↥U)
have this₁ : ∃ (k : ℕ), Eq (α := V) ((HPow.hPow (α := Module.End R V) (T χ w) k : (a : V) → V) (↑x : V) : V) (0 : V)
Tactic: simp only [Module.End.mem_maxGenEigenspace, zero_smul, sub_zero] at this
Cleared hypotheses: this
-- 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))
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)
trace_za_zero :
  Eq.{u_1 + 1} (α := R)
    ((LinearMap.trace R ↥U : (a : ↥U →ₗ[R] ↥U) → R)
        (((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) :
      R)
    (0 : R)
w : A
key :
  ∀ (i : ℕ) (hi : i ≠ 0),
    ∃ j < i,
      LE.le.{u_4} (α := Submodule R V) (Submodule.map (T χ w) ((U' : (a : ℕ) → Submodule R V) i))
        ((U' : (a : ℕ) → Submodule R V) j)
x : ↥U
this : ∃ (k : ℕ), Eq (α := V) ((HPow.hPow (α := Module.End R V) (T χ w) k : (a : V) → V) (↑x : V) : V) (0 : V)
⊢ ∃ (n : ℕ),
    Eq (α := ↥U)
      ((HPow.hPow (α := Module.End R ↥U) (T.{u_1, u_3, u_4} (V := ↥U) χ w : Module.End R ↥U) n : (a : ↥U) → ↥U) x : ↥U)
      (0 : ↥U)
have h : ∀ (n : ℕ) (hn : Eq (α := V) ((HPow.hPow (α := Module.End R V) (T χ w) n : (a : V) → V) (↑x : V) : V) (0 : V)),
  Eq (α := ↥U)
    ((HPow.hPow (α := Module.End R ↥U) (T.{u_1, u_3, u_4} (V := ↥U) χ w : Module.End R ↥U) n : (a : ↥U) → ↥U) x : ↥U)
    (0 : ↥U)
Tactic: peel this with n hn
-- 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))
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)
trace_za_zero :
  Eq.{u_1 + 1} (α := R)
    ((LinearMap.trace R ↥U : (a : ↥U →ₗ[R] ↥U) → R)
        (((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) :
      R)
    (0 : R)
w : A
key :
  ∀ (i : ℕ) (hi : i ≠ 0),
    ∃ j < i,
      LE.le.{u_4} (α := Submodule R V) (Submodule.map (T χ w) ((U' : (a : ℕ) → Submodule R V) i))
        ((U' : (a : ℕ) → Submodule R V) j)
x : ↥U
this : ∃ (k : ℕ), Eq (α := V) ((HPow.hPow (α := Module.End R V) (T χ w) k : (a : V) → V) (↑x : V) : V) (0 : V)
n : ℕ
hn : Eq (α := V) ((HPow.hPow (α := Module.End R V) (T χ w) n : (a : V) → V) (↑x : V) : V) (0 : V)
⊢ Eq (α := ↥U)
    ((HPow.hPow (α := Module.End R ↥U) (T.{u_1, u_3, u_4} (V := ↥U) χ w : Module.End R ↥U) n : (a : ↥U) → ↥U) x : ↥U)
    (0 : ↥U)
have h : Eq.{u_4 + 1} (α := V)
  (↑((HPow.hPow (α := Module.End R ↥U) (T.{u_1, u_3, u_4} (V := ↥U) χ w : Module.End R ↥U) n : (a : ↥U) → ↥U) x) : V)
  (↑0 : V)
Tactic: ext
-- 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))
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)
trace_za_zero :
  Eq.{u_1 + 1} (α := R)
    ((LinearMap.trace R ↥U : (a : ↥U →ₗ[R] ↥U) → R)
        (((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) :
      R)
    (0 : R)
w : A
key :
  ∀ (i : ℕ) (hi : i ≠ 0),
    ∃ j < i,
      LE.le.{u_4} (α := Submodule R V) (Submodule.map (T χ w) ((U' : (a : ℕ) → Submodule R V) i))
        ((U' : (a : ℕ) → Submodule R V) j)
x : ↥U
this : ∃ (k : ℕ), Eq (α := V) ((HPow.hPow (α := Module.End R V) (T χ w) k : (a : V) → V) (↑x : V) : V) (0 : V)
n : ℕ
hn : Eq (α := V) ((HPow.hPow (α := Module.End R V) (T χ w) n : (a : V) → V) (↑x : V) : V) (0 : V)
⊢ Eq.{u_4 + 1} (α := V)
    (↑((HPow.hPow (α := Module.End R ↥U) (T.{u_1, u_3, u_4} (V := ↥U) χ w : Module.End R ↥U) n : (a : ↥U) → ↥U) x) : V)
    (↑0 : V)
have h : Eq (α := V)
  ((↑((HPow.hPow (α := Module.End R ↥U) (T.{u_1, u_3, u_4} (V := ↥U) χ w : Module.End R ↥U) n : (a : ↥U) → ↥U) x) : V) :
    V)
  ((HPow.hPow (α := Module.End R V) (T χ w) n : (a : V) → V) (↑x : V) : V)
Tactic: simp only [ZeroMemClass.coe_zero, ← hn]
-- 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))
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)
trace_za_zero :
  Eq.{u_1 + 1} (α := R)
    ((LinearMap.trace R ↥U : (a : ↥U →ₗ[R] ↥U) → R)
        (((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) :
      R)
    (0 : R)
w : A
key :
  ∀ (i : ℕ) (hi : i ≠ 0),
    ∃ j < i,
      LE.le.{u_4} (α := Submodule R V) (Submodule.map (T χ w) ((U' : (a : ℕ) → Submodule R V) i))
        ((U' : (a : ℕ) → Submodule R V) j)
x : ↥U
this : ∃ (k : ℕ), Eq (α := V) ((HPow.hPow (α := Module.End R V) (T χ w) k : (a : V) → V) (↑x : V) : V) (0 : V)
n : ℕ
⊢ Eq (α := V)
    ((↑((HPow.hPow (α := Module.End R ↥U) (T.{u_1, u_3, u_4} (V := ↥U) χ w : Module.End R ↥U) n : (a : ↥U) → ↥U) x) :
        V) :
      V)
    ((HPow.hPow (α := Module.End R V) (T χ w) n : (a : V) → V) (↑x : V) : V)
have h : Eq (α := V)
  ((↑((HPow.hPow (α := Module.End R ↥U) (β := ℕ) (T.{u_1, u_3, u_4} (V := ↥U) χ w : Module.End R ↥U) 0 : (a : ↥U) → ↥U)
          x) :
      V) :
    V)
  ((HPow.hPow (α := Module.End R V) (β := ℕ) (T χ w) 0 : (a : V) → V) (↑x : V) : V)
Tactic: induction n
Cleared hypotheses: n
-- 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))
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)
trace_za_zero :
  Eq.{u_1 + 1} (α := R)
    ((LinearMap.trace R ↥U : (a : ↥U →ₗ[R] ↥U) → R)
        (((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) :
      R)
    (0 : R)
w : A
key :
  ∀ (i : ℕ) (hi : i ≠ 0),
    ∃ j < i,
      LE.le.{u_4} (α := Submodule R V) (Submodule.map (T χ w) ((U' : (a : ℕ) → Submodule R V) i))
        ((U' : (a : ℕ) → Submodule R V) j)
⊢ ∀ (m : ↥U),
    ∃ (n : ℕ),
      Eq (α := ↥U)
        ((HPow.hPow (α := Module.End R ↥U) (T.{u_1, u_3, u_4} (V := ↥U) χ w : Module.End R ↥U) n : (a : ↥U) → ↥U) m :
          ↥U)
        (0 : ↥U)
have h : LE.le.{u_4} (α := Submodule R V) (⨆ (i : ℕ), (U' : (a : ℕ) → Submodule R V) i) (Module.End.maxGenEigenspace (T χ w) 0)
Tactic: suffices ⨆ i, U' i ≤ Module.End.maxGenEigenspace (T χ w) 0 by
      intro x
      specialize this x.2
      simp only [Module.End.mem_maxGenEigenspace, zero_smul, sub_zero] at this
      peel this with n hn
      ext
      simp only [ZeroMemClass.coe_zero, ← hn]; clear hn
      induction n <;> simp_all [pow_succ']
-- 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))
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)
trace_za_zero :
  Eq.{u_1 + 1} (α := R)
    ((LinearMap.trace R ↥U : (a : ↥U →ₗ[R] ↥U) → R)
        (((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) :
      R)
    (0 : R)
w : A
key :
  ∀ (i : ℕ) (hi : i ≠ 0),
    ∃ j < i,
      LE.le.{u_4} (α := Submodule R V) (Submodule.map (T χ w) ((U' : (a : ℕ) → Submodule R V) i))
        ((U' : (a : ℕ) → Submodule R V) j)
⊢ LE.le.{u_4} (α := Submodule R V) (⨆ (i : ℕ), (U' : (a : ℕ) → Submodule R V) i) (Module.End.maxGenEigenspace (T χ w) 0)
have h : ∀ (i : ℕ),
  LE.le (α := Submodule R V) ((U' : (a : ℕ) → Submodule R V) i : Submodule R V)
    (Module.End.maxGenEigenspace (T χ w) 0 : Submodule R V)
Tactic: apply iSup_le
-- 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))
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)
trace_za_zero :
  Eq.{u_1 + 1} (α := R)
    ((LinearMap.trace R ↥U : (a : ↥U →ₗ[R] ↥U) → R)
        (((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) :
      R)
    (0 : R)
w : A
key :
  ∀ (i : ℕ) (hi : i ≠ 0),
    ∃ j < i,
      LE.le.{u_4} (α := Submodule R V) (Submodule.map (T χ w) ((U' : (a : ℕ) → Submodule R V) i))
        ((U' : (a : ℕ) → Submodule R V) j)
i : ℕ
x : V
hx : Membership.mem (γ := Submodule R V) ((U' : (a : ℕ) → Submodule R V) i : Submodule R V) x
⊢ Membership.mem (γ := Submodule R V) (Module.End.maxGenEigenspace (T χ w) 0) x
have h : ∃ (k : ℕ), Eq (α := V) ((HPow.hPow (α := Module.End R V) (T χ w) k : (a : V) → V) x : V) (0 : V)
Tactic: simp only [Module.End.mem_maxGenEigenspace, zero_smul, sub_zero]