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)
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)
trace_T_U_zero :
  ∀ (w : A),
    Eq.{u_1 + 1} (α := R)
      ((LinearMap.trace R ↥U : (a : ↥U →ₗ[R] ↥U) → R) (T.{u_1, u_3, u_4} (V := ↥U) χ w : Module.End R ↥U) : R) (0 : R)
trace_za :
  (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) =
    HSMul.hSMul (β := R) (χ ⁅z, a⁆) (↑(finrank.{u_1, u_4} R ↥U) : R)
inr : Nontrivial.{u_4} ↥U
⊢ finrank.{u_1, u_4} R ↥U ≠ 0

Tactic:
suffices Nontrivial U from Module.finrank_pos.ne'
-- 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)
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)
trace_T_U_zero :
  ∀ (w : A),
    Eq.{u_1 + 1} (α := R)
      ((LinearMap.trace R ↥U : (a : ↥U →ₗ[R] ↥U) → R) (T.{u_1, u_3, u_4} (V := ↥U) χ w : Module.End R ↥U) : R) (0 : R)
trace_za :
  (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) =
    HSMul.hSMul (β := R) (χ ⁅z, a⁆) (↑(finrank.{u_1, u_4} R ↥U) : R)
apply : Membership.mem (γ := Submodule R V) ((U' : (a : ℕ) → Submodule R V) 1 : Submodule R V) v
⊢ v ∈ U

Tactic:
apply Submodule.mem_iSup_of_mem 1

Premises used: Submodule.mem_iSup_of_mem, OfNat.ofNat
-- 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)
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)
trace_T_U_zero :
  ∀ (w : A),
    Eq.{u_1 + 1} (α := R)
      ((LinearMap.trace R ↥U : (a : ↥U →ₗ[R] ↥U) → R) (T.{u_1, u_3, u_4} (V := ↥U) χ w : Module.End R ↥U) : R) (0 : R)
trace_za :
  (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) =
    HSMul.hSMul (β := R) (χ ⁅z, a⁆) (↑(finrank.{u_1, u_4} R ↥U) : R)
right : (1 : (a : V) → V) v = v
right₁ right₂ : 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)
          0 :
        (a : V) → V)
      v =
    v

Tactic:
rw [pow_zero, Module.End.one_apply]

Premises used: pow_zero, Module.End.one_apply
-- 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)
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)
trace_T_U_zero :
  ∀ (w : A),
    Eq.{u_1 + 1} (α := R)
      ((LinearMap.trace R ↥U : (a : ↥U →ₗ[R] ↥U) → R) (T.{u_1, u_3, u_4} (V := ↥U) χ w : Module.End R ↥U) : R) (0 : R)
trace_za :
  (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) =
    HSMul.hSMul (β := R) (χ ⁅z, a⁆) (↑(finrank.{u_1, u_4} R ↥U) : R)
⊢ v ∈ U

Tactic:
have hvU : v ∈ U := by
    apply Submodule.mem_iSup_of_mem 1
    apply Submodule.subset_span
    use 0, zero_lt_one
    rw [pow_zero, Module.End.one_apply]
-- 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)
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)
trace_T_U_zero :
  ∀ (w : A),
    Eq.{u_1 + 1} (α := R)
      ((LinearMap.trace R ↥U : (a : ↥U →ₗ[R] ↥U) → R) (T.{u_1, u_3, u_4} (V := ↥U) χ w : Module.End R ↥U) : R) (0 : R)
trace_za :
  (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) =
    HSMul.hSMul (β := R) (χ ⁅z, a⁆) (↑(finrank.{u_1, u_4} R ↥U) : R)
hvU : v ∈ U
⊢ Subtype.mk (p := fun (x : V) ↦ x ∈ U) v hvU ≠ 0

Tactic:
simp [hv']
-- 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)
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)
trace_T_U_zero :
  ∀ (w : A),
    Eq.{u_1 + 1} (α := R)
      ((LinearMap.trace R ↥U : (a : ↥U →ₗ[R] ↥U) → R) (T.{u_1, u_3, u_4} (V := ↥U) χ w : Module.End R ↥U) : R) (0 : R)
trace_za :
  (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) =
    HSMul.hSMul (β := R) (χ ⁅z, a⁆) (↑(finrank.{u_1, u_4} R ↥U) : R)
hvU : v ∈ U
⊢ Nontrivial.{u_4} ↥U

Tactic:
exact nontrivial_of_ne ⟨v, hvU⟩ 0 <| by simp [hv']

Premises used: nontrivial_of_ne, OfNat.ofNat
-- Module: Mathlib.Algebra.Lie.LieTheorem
Goal:
k : Type u_1
inst : Field k
L : Type u_2
inst_1 : LieRing L
inst_2 : LieAlgebra k L
V : Type u_3
inst_3 : AddCommGroup V
inst_4 : Module k V
inst_5 : LieRingModule L V
inst_6 : LieModule k L V
inst_7 : CharZero k
inst_8 : Module.Finite k V
inst_9 : IsTriangularizable k L V
A : LieIdeal k L
hA : IsCoatom (↑A : Submodule k L)
χ₀ : Module.Dual.{u_1, u_2} k ↥A
inst_10 : Nontrivial.{u_3} ↥(weightSpace V (⇑χ₀ : (a : ↥A) → k))
obtain :
  ∀ (z : L) (hz : z ∉ (↑A : Submodule k L)),
    ∃ (χ : Module.Dual k L), Nontrivial.{u_3} ↥(weightSpace V (⇑χ : (a : L) → k))
⊢ ∃ (χ : Module.Dual k L), Nontrivial.{u_3} ↥(weightSpace V (⇑χ : (a : L) → k))

Tactic:
obtain ⟨z, -, hz⟩ := SetLike.exists_of_lt (hA.lt_top)

Premises used: SetLike.exists_of_lt, IsCoatom.lt_top
-- Module: Mathlib.Algebra.Lie.LieTheorem
Goal:
k : Type u_1
inst : Field k
L : Type u_2
inst_1 : LieRing L
inst_2 : LieAlgebra k L
V : Type u_3
inst_3 : AddCommGroup V
inst_4 : Module k V
inst_5 : LieRingModule L V
inst_6 : LieModule k L V
inst_7 : CharZero k
inst_8 : Module.Finite k V
inst_9 : IsTriangularizable k L V
A : LieIdeal k L
hA : IsCoatom (↑A : Submodule k L)
χ₀ : Module.Dual.{u_1, u_2} k ↥A
inst_10 : Nontrivial.{u_3} ↥(weightSpace V (⇑χ₀ : (a : ↥A) → k))
z : L
hz : z ∉ (↑A : Submodule k L)
⊢ z ≠ 0

Tactic:
aesop
-- Module: Mathlib.Algebra.Lie.LieTheorem
Goal:
k : Type u_1
inst : Field k
L : Type u_2
inst_1 : LieRing L
inst_2 : LieAlgebra k L
V : Type u_3
inst_3 : AddCommGroup V
inst_4 : Module k V
inst_5 : LieRingModule L V
inst_6 : LieModule k L V
inst_7 : CharZero k
inst_8 : Module.Finite k V
inst_9 : IsTriangularizable k L V
A : LieIdeal k L
hA : IsCoatom (↑A : Submodule k L)
χ₀ : Module.Dual.{u_1, u_2} k ↥A
inst_10 : Nontrivial.{u_3} ↥(weightSpace V (⇑χ₀ : (a : ↥A) → k))
z : L
hz : z ∉ (↑A : Submodule k L)
e : LinearEquiv.{u_1, u_1, u_2, u_1} (RingHom.id k) (↥(k ∙ z)) k :=
  LinearEquiv.symm (LinearEquiv.toSpanNonzeroSingleton k L z ⋯)
⊢ ∀ (x : ↥(k ∙ z)), HSMul.hSMul.{u_1, u_2, u_2} (α := k) ((e : (a : ↥(k ∙ z)) → k) x : k) z = (↑x : L)

Tactic:
simp [e]
-- Module: Mathlib.Algebra.Lie.LieTheorem
Goal:
k : Type u_1
inst : Field k
L : Type u_2
inst_1 : LieRing L
inst_2 : LieAlgebra k L
V : Type u_3
inst_3 : AddCommGroup V
inst_4 : Module k V
inst_5 : LieRingModule L V
inst_6 : LieModule k L V
inst_7 : CharZero k
inst_8 : Module.Finite k V
inst_9 : IsTriangularizable k L V
A : LieIdeal k L
hA : IsCoatom (↑A : Submodule k L)
χ₀ : Module.Dual.{u_1, u_2} k ↥A
inst_10 : Nontrivial.{u_3} ↥(weightSpace V (⇑χ₀ : (a : ↥A) → k))
z : L
hz : z ∉ (↑A : Submodule k L)
e : LinearEquiv.{u_1, u_1, u_2, u_1} (RingHom.id k) (↥(k ∙ z)) k :=
  LinearEquiv.symm (LinearEquiv.toSpanNonzeroSingleton k L z ⋯)
⊢ ∀ (x : ↥(k ∙ z)), HSMul.hSMul.{u_1, u_2, u_2} (α := k) ((e : (a : ↥(k ∙ z)) → k) x : k) z = (↑x : L)

Tactic:
have he : ∀ x, e x • z = x := by simp [e]
-- Module: Mathlib.Algebra.Lie.LieTheorem
Goal:
k : Type u_1
inst : Field k
L : Type u_2
inst_1 : LieRing L
inst_2 : LieAlgebra k L
V : Type u_3
inst_3 : AddCommGroup V
inst_4 : Module k V
inst_5 : LieRingModule L V
inst_6 : LieModule k L V
inst_7 : CharZero k
inst_8 : Module.Finite k V
inst_9 : IsTriangularizable k L V
A : LieIdeal k L
hA : IsCoatom (↑A : Submodule k L)
χ₀ : Module.Dual.{u_1, u_2} k ↥A
inst_10 : Nontrivial.{u_3} ↥(weightSpace V (⇑χ₀ : (a : ↥A) → k))
z : L
hz : z ∉ (↑A : Submodule k L)
e : LinearEquiv.{u_1, u_1, u_2, u_1} (RingHom.id k) (↥(k ∙ z)) k :=
  LinearEquiv.symm (LinearEquiv.toSpanNonzeroSingleton k L z ⋯)
he : ∀ (x : ↥(k ∙ z)), HSMul.hSMul.{u_1, u_2, u_2} (α := k) ((e : (a : ↥(k ∙ z)) → k) x : k) z = (↑x : L)
⊢ IsCompl (↑A : Submodule k L) (k ∙ z)

Tactic:
have hA : IsCompl A.toSubmodule (k ∙ z) := isCompl_span_singleton_of_isCoatom_of_notMem hA hz
-- Module: Mathlib.Algebra.Lie.LieTheorem
Goal:
k : Type u_1
inst : Field k
L : Type u_2
inst_1 : LieRing L
inst_2 : LieAlgebra k L
V : Type u_3
inst_3 : AddCommGroup V
inst_4 : Module k V
inst_5 : LieRingModule L V
inst_6 : LieModule k L V
inst_7 : CharZero k
inst_8 : Module.Finite k V
inst_9 : IsTriangularizable k L V
A : LieIdeal k L
hA_1 : IsCoatom (↑A : Submodule k L)
χ₀ : Module.Dual.{u_1, u_2} k ↥A
inst_10 : Nontrivial.{u_3} ↥(weightSpace V (⇑χ₀ : (a : ↥A) → k))
z : L
hz : z ∉ (↑A : Submodule k L)
e : LinearEquiv.{u_1, u_1, u_2, u_1} (RingHom.id k) (↥(k ∙ z)) k :=
  LinearEquiv.symm (LinearEquiv.toSpanNonzeroSingleton k L z ⋯)
he : ∀ (x : ↥(k ∙ z)), HSMul.hSMul.{u_1, u_2, u_2} (α := k) ((e : (a : ↥(k ∙ z)) → k) x : k) z = (↑x : L)
hA : IsCompl (↑A : Submodule k L) (k ∙ z)
π₁ : L →ₗ[k] ↥A := (↑A : Submodule k L).projectionOnto (k ∙ z) hA
π₂ : L →ₗ[k] ↥(k ∙ z) := projectionOnto (k ∙ z) (LieIdeal.toLieSubalgebra k L A).toSubmodule ⋯
W : LieSubmodule k L V := weightSpaceOfIsLieTower k (A := ↥A) V (⇑χ₀ : (a : ↥A) → k)
⊢ Nontrivial.{u_3} ↥W

Tactic:
have : Nontrivial W := inferInstanceAs (Nontrivial (weightSpace V χ₀))
-- Module: Mathlib.Algebra.Lie.LieTheorem
Goal:
k : Type u_1
inst : Field k
L : Type u_2
inst_1 : LieRing L
inst_2 : LieAlgebra k L
V : Type u_3
inst_3 : AddCommGroup V
inst_4 : Module k V
inst_5 : LieRingModule L V
inst_6 : LieModule k L V
inst_7 : CharZero k
inst_8 : Module.Finite k V
inst_9 : IsTriangularizable k L V
A : LieIdeal k L
hA_1 : IsCoatom (↑A : Submodule k L)
χ₀ : Module.Dual.{u_1, u_2} k ↥A
inst_10 : Nontrivial.{u_3} ↥(weightSpace V (⇑χ₀ : (a : ↥A) → k))
z : L
hz : z ∉ (↑A : Submodule k L)
e : LinearEquiv.{u_1, u_1, u_2, u_1} (RingHom.id k) (↥(k ∙ z)) k :=
  LinearEquiv.symm (LinearEquiv.toSpanNonzeroSingleton k L z ⋯)
he : ∀ (x : ↥(k ∙ z)), HSMul.hSMul.{u_1, u_2, u_2} (α := k) ((e : (a : ↥(k ∙ z)) → k) x : k) z = (↑x : L)
hA : IsCompl (↑A : Submodule k L) (k ∙ z)
π₁ : L →ₗ[k] ↥A := (↑A : Submodule k L).projectionOnto (k ∙ z) hA
π₂ : L →ₗ[k] ↥(k ∙ z) := projectionOnto (k ∙ z) (LieIdeal.toLieSubalgebra k L A).toSubmodule ⋯
W : LieSubmodule k L V := weightSpaceOfIsLieTower k (A := ↥A) V (⇑χ₀ : (a : ↥A) → k)
this : Nontrivial.{u_3} ↥W
hf :
  Eq.{u_3 + 1} (α := Submodule k ↥W)
    (⨆ (μ : k),
      ((Module.End.genEigenspace.{u_1, u_3} (M := ↥W)
              (((toEnd.{u_1, u_2, u_3} k L ↥W : LieHom.{u_1, u_2, u_3} k L (Module.End k ↥W)) :
                  (a : L) → Module.End k ↥W)
                z)
              μ :
            ℕ∞ →o Submodule k ↥W) :
          (a : ℕ∞) → Submodule k ↥W)
        ⊤)
    ⊤
k₁ : ℕ∞
⊢ ∃ (c : k),
    Module.End.HasEigenvalue.{u_1, u_3} (M := ↥W)
      (((toEnd.{u_1, u_2, u_3} k L ↥W : LieHom.{u_1, u_2, u_3} k L (Module.End k ↥W)) : (a : L) → Module.End k ↥W) z) c

Tactic:
apply Module.End.exists_hasEigenvalue_of_genEigenspace_eq_top

Premises used: Module.End.exists_hasEigenvalue_of_genEigenspace_eq_top