awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Lie.Abelian
Goal:
R : Type u
L : Type v
M : Type w
N : Type w₁
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : AddCommGroup N
inst_8 : Module R N
inst_9 : LieRingModule L N
inst_10 : LieModule R L N
f : M →ₗ⁅R,L⁆ N
⊢ (↑((LinearEquiv.symm maxTrivLinearMapEquivLieModuleHom : (a : M →ₗ⁅R,L⁆ N) → ↥(maxTrivSubmodule R L (M →ₗ[R] N))) f) :
      M →ₗ[R] N) =
    (↑f : M →ₗ[R] N)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Lie.Abelian
Goal:
R : Type u
L : Type v
M : Type w
N : Type w₁
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : AddCommGroup N
inst_8 : Module R N
inst_9 : LieRingModule L N
inst_10 : LieModule R L N
⊢ IsLieAbelian.{v} ↥(center R L)

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.Algebra.Lie.Abelian
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
⊢ Eq (α := LieIdeal R L) (LieHom.ker (ad R L)) (LieModule.ker R L L)

Tactic:
rfl

Premises used: LieAlgebra.ad, LieModule.ker, rfl
-- Module: Mathlib.Algebra.Lie.Abelian
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
h :
  ∀ (y : L),
    Membership.mem (γ := LieSubmodule R L L) (LieModule.ker R L L) y ↔
      Membership.mem (γ := LieSubmodule R L L) (center R L) y
⊢ Eq (α := LieIdeal R L) (LieModule.ker R L L) (center R L)

Tactic:
ext y
-- Module: Mathlib.Algebra.Lie.Abelian
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
y : L
⊢ Membership.mem (γ := LieSubmodule R L L) (LieModule.ker R L L) y ↔
    Membership.mem (γ := LieSubmodule R L L) (center R L) y

Tactic:
simp only [LieModule.mem_maxTrivSubmodule, LieModule.mem_ker, ← lie_skew _ y, neg_eq_zero]

Premises used: LieModule.mem_ker, neg_eq_zero, LieModule.mem_maxTrivSubmodule, lie_skew
-- Module: Mathlib.Algebra.Lie.Abelian
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
h : I ≤ center R L
⊢ IsLieAbelian.{v} ↥I

Tactic:
haveI : LieModule.IsTrivial L I := (LieModule.trivial_iff_le_maximal_trivial R L L I).mpr h
  LieIdeal.isLieAbelian_of_trivial R L I

Premises used: LieIdeal.isLieAbelian_of_trivial
-- Module: Mathlib.Algebra.Lie.Abelian
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
⊢ IsLieAbelian L ↔ Eq (α := LieIdeal R L) (center R L) ⊤

Tactic:
LieModule.isTrivial_iff_max_triv_eq_top R L L

Premises used: LieModule.isTrivial_iff_max_triv_eq_top
-- Module: Mathlib.Algebra.Lie.Abelian
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
rw : Eq (α := LieIdeal R L) (LieModule.ker R L L) ⊥ ↔ Eq (α := LieIdeal R L) (center R L) ⊥
rw₁ rw₂ : Eq (α := LieIdeal R L) (center R L) ⊥ ↔ Eq (α := LieIdeal R L) (center R L) ⊥
⊢ LieModule.IsFaithful R L L ↔ Eq (α := LieIdeal R L) (center R L) ⊥

Tactic:
rw [LieModule.isFaithful_iff_ker_eq_bot, self_module_ker_eq_center]

Premises used: LieAlgebra.self_module_ker_eq_center, LieModule.isFaithful_iff_ker_eq_bot
-- Module: Mathlib.Algebra.Lie.Abelian
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : LieModule.IsFaithful R L L
⊢ Eq (α := LieIdeal R L) (center R L) ⊥

Tactic:
(isFaithful_self_iff R L).mp inferInstance

Premises used: inferInstance, Iff.mp, LieAlgebra.isFaithful_self_iff
-- Module: Mathlib.Algebra.Lie.Abelian
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
x : L
hx : Membership.mem (γ := LieIdeal R L) (LieAlgebra.center R L) x
y : L
rw :
  Commute.{w} (S := Module.End R M)
    (((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) y : Module.End R M)
    (((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) x : Module.End R M)
rw₁ :
  Eq.{w + 1} (α := Module.End R M)
    (Bracket.bracket (L := Module.End R M)
        (((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) y : Module.End R M)
        (((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) x) :
      Module.End R M)
    (0 : Module.End R M)
rw₂ :
  Eq.{w + 1} (α := Module.End R M)
    (((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) ⁅y, x⁆ : Module.End R M)
    (0 : Module.End R M)
rw₃ :
  Eq.{w + 1} (α := Module.End R M)
    (((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) 0) 0
rw₄ rw₅ : Eq.{w + 1} (α := Module.End R M) 0 0
⊢ Commute.{w} (S := Module.End R M)
    (((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) x : Module.End R M)
    (((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) y : Module.End R M)

Tactic:
rw [Commute.symm_iff, commute_iff_lie_eq, ← LieHom.map_lie, hx y, map_zero]

Premises used: LieHom.map_lie, map_zero, Commute.symm_iff, commute_iff_lie_eq
-- Module: Mathlib.Algebra.Lie.Abelian
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
x : L
hx : Membership.mem (γ := LieIdeal R L) (LieAlgebra.center R L) x
y : L
⊢ Commute.{w} (S := Module.End R M)
    (((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) y : Module.End R M)
    (((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) x : Module.End R M)

Tactic:
(LieModule.commute_toEnd_of_mem_center_left M hx y).symm

Premises used: Commute.symm, LieModule.commute_toEnd_of_mem_center_left
-- Module: Mathlib.Algebra.Lie.Abelian
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
N : LieSubmodule R L M
I : LieIdeal R L
inst_6 : LieModule.IsTrivial L M
suffices : ⁅I, N⁆ ≤ ⊥
⊢ ⁅I, N⁆ = ⊥

Tactic:
suffices ⁅I, N⁆ ≤ ⊥ from le_bot_iff.mp this
-- Module: Mathlib.Algebra.Lie.Abelian
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
N : LieSubmodule R L M
I : LieIdeal R L
inst_6 : LieModule.IsTrivial L M
rw : {x : M | ∃ (x_1 : ↥I) (n : ↥N), ⁅(↑x_1 : L), (↑n : M)⁆ = x} ⊆ (↑⊥ : Set M)
⊢ ⁅I, N⁆ ≤ ⊥

Tactic:
rw [lieIdeal_oper_eq_span, LieSubmodule.lieSpan_le]

Premises used: LieSubmodule.lieIdeal_oper_eq_span, LieSubmodule.lieSpan_le
-- Module: Mathlib.Algebra.Lie.Abelian
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
N : LieSubmodule R L M
I : LieIdeal R L
inst_6 : LieModule.IsTrivial L M
m : M
x : ↥I
n : ↥N
h : ⁅(↑x : L), (↑n : M)⁆ = m
⊢ 0 = m

Tactic:
rw [trivial_lie_zero] at h

Premises used: trivial_lie_zero
-- Module: Mathlib.Algebra.Lie.Abelian
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
N : LieSubmodule R L M
I : LieIdeal R L
inst_6 : LieModule.IsTrivial L M
m : M
x : ↥I
n : ↥N
h : 0 = m
⊢ m ∈ (↑⊥ : Set M)

Tactic:
simp [← h]
-- Module: Mathlib.Algebra.Lie.Abelian
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
simp : IsLieAbelian.{v} ↥I ↔ ∀ (y : L) (x : ↥I) (x_1 : ↥I), ⁅(↑x : L), (↑x_1 : L)⁆ = y → y = 0
⊢ IsLieAbelian.{v} ↥I ↔ ⁅I, I⁆ = ⊥

Tactic:
simp only [_root_.eq_bot_iff, lieIdeal_oper_eq_span, LieSubmodule.lieSpan_le,
    LieSubmodule.bot_coe, Set.subset_singleton_iff, Set.mem_setOf_eq, exists_imp]

Premises used: Set.subset_singleton_iff, LieSubmodule.bot_coe, Set.mem_setOf_eq, LieSubmodule.lieIdeal_oper_eq_span, LieSubmodule.lieSpan_le, eq_bot_iff, exists_imp
-- Module: Mathlib.Algebra.Lie.Abelian
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
h : IsLieAbelian.{v} ↥I
z : L
x : ↥I
y : ↥I
hz : ⁅(↑x : L), (↑y : L)⁆ = z
⊢ ⁅x, y⁆ = 0

Tactic:
apply h.trivial

Premises used: LieModule.IsTrivial.trivial
-- Module: Mathlib.Algebra.Lie.Abelian
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
⊢ IsLieAbelian.{v} ↥I ↔ ∀ (y : L) (x : ↥I) (x_1 : ↥I), ⁅(↑x : L), (↑x_1 : L)⁆ = y → y = 0

Tactic:
refine
    ⟨fun h z x y hz =>
      hz.symm.trans
        (((I : LieSubalgebra R L).coe_bracket x y).symm.trans
          ((coe_zero_iff_zero _ _).mpr (by apply h.trivial))),
      fun h => ⟨fun x y => ((I : LieSubalgebra R L).coe_zero_iff_zero _).mp (h _ x y rfl)⟩⟩
-- Module: Mathlib.Algebra.Lie.Abelian
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
N : LieSubmodule R L M
I : LieIdeal R L
hN : IsAtom N
h : ⁅I, N⁆ ≠ ⊥
⊢ ⁅I, N⁆ = N

Tactic:
(hN.le_iff_eq h).mp <| LieSubmodule.lie_le_right N I

Premises used: LieSubmodule.lie_le_right, Iff.mp, IsAtom.le_iff_eq
-- Module: Mathlib.Algebra.Lie.Abelian
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
hI : IsAtom I
h : ¬IsLieAbelian.{u_2} ↥I
⊢ ⁅I, I⁆ = I

Tactic:
lie_eq_self_of_isAtom_of_ne_bot hI <| not_imp_not.mpr (lie_abelian_iff_lie_self_eq_bot I).mpr h

Premises used: Iff.mpr, LieSubmodule.lie_abelian_iff_lie_self_eq_bot, lie_eq_self_of_isAtom_of_ne_bot, not_imp_not
-- Module: Mathlib.Algebra.Lie.Abelian
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
⊢ ∀ (x y : L) (m : TrivialLieModule R L M), 0 = HAdd.hAdd (α := TrivialLieModule R L M) 0 0

Tactic:
simp
-- Module: Mathlib.Algebra.Lie.Abelian
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
⊢ ∀ (x : L) (m n : TrivialLieModule R L M), 0 = HAdd.hAdd (α := TrivialLieModule R L M) 0 0

Tactic:
simp
-- Module: Mathlib.Algebra.Lie.Abelian
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
⊢ ∀ (t : R) (x : L) (m : TrivialLieModule R L M), ⁅t • x, m⁆ = t • ⁅x, m⁆

Tactic:
simp [trivial_lie_zero]

Premises used: trivial_lie_zero
-- Module: Mathlib.Algebra.Lie.Abelian
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
⊢ ∀ (t : R) (x : L) (m : TrivialLieModule R L M), ⁅x, t • m⁆ = t • ⁅x, m⁆

Tactic:
simp [trivial_lie_zero]

Premises used: trivial_lie_zero
-- Module: Mathlib.Algebra.Lie.AdjointAction.Basic
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
a b : A
h : Commute a b
rw :
  SemiconjBy (M := Module.End R A) ((ad R A : (a : A) → Module.End R A) a : Module.End R A)
    ((ad R A : (a : A) → Module.End R A) b : Module.End R A) ((ad R A : (a : A) → Module.End R A) b : Module.End R A)
rw₁ :
  HMul.hMul (α := Module.End R A) (β := Module.End R A) ((ad R A : (a : A) → Module.End R A) a : Module.End R A)
      ((ad R A : (a : A) → Module.End R A) b : Module.End R A) =
    HMul.hMul (α := Module.End R A) (β := Module.End R A) ((ad R A : (a : A) → Module.End R A) b : Module.End R A)
      ((ad R A : (a : A) → Module.End R A) a : Module.End R A)
rw₂ :
  HMul.hMul (α := Module.End R A) (β := Module.End R A) ((ad R A : (a : A) → Module.End R A) a : Module.End R A)
        ((ad R A : (a : A) → Module.End R A) b : Module.End R A) -
      HMul.hMul (α := Module.End R A) (β := Module.End R A) ((ad R A : (a : A) → Module.End R A) b : Module.End R A)
        ((ad R A : (a : A) → Module.End R A) a : Module.End R A) =
    0
rw₃ :
  Eq (α := Module.End R A)
    (Bracket.bracket (L := Module.End R A) ((ad R A : (a : A) → Module.End R A) a : Module.End R A)
        ((ad R A : (a : A) → Module.End R A) b) :
      Module.End R A)
    (0 : Module.End R A)
rw₄ : Eq (α := Module.End R A) ((ad R A : (a : A) → Module.End R A) ⁅a, b⁆ : Module.End R A) (0 : Module.End R A)
rw₅ :
  Eq (α := Module.End R A) ((ad R A : (a : A) → Module.End R A) (a * b - b * a) : Module.End R A) (0 : Module.End R A)
rw₆ : Eq (α := Module.End R A) ((ad R A : (a : A) → Module.End R A) 0 : Module.End R A) (0 : Module.End R A)
rw₇ rw₈ : Eq.{u_2 + 1} (α := Module.End R A) 0 0
⊢ Commute (S := Module.End R A) ((ad R A : (a : A) → Module.End R A) a : Module.End R A)
    ((ad R A : (a : A) → Module.End R A) b : Module.End R A)

Tactic:
rw [Commute, SemiconjBy, ← sub_eq_zero, ← Ring.lie_def,
    ← (LieAlgebra.ad R A).map_lie, Ring.lie_def, sub_eq_zero.mpr h, map_zero]

Premises used: Iff.mpr, sub_eq_zero, LieAlgebra.ad, SemiconjBy, Commute, LieHom.map_lie, map_zero, Ring.lie_def
-- Module: Mathlib.Algebra.Lie.AdjointAction.Basic
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
a : A
h : IsNilpotent a
rw :
  IsNilpotent
    (HSub.hSub (α := (a : A) → A →ₗ[R] A) (β := (b : A) → A →ₗ[R] A) (LinearMap.mulLeft R) (LinearMap.mulRight R) a)
⊢ IsNilpotent (R := Module.End R A) ((ad R A : (a : A) → Module.End R A) a : Module.End R A)

Tactic:
rw [LieAlgebra.ad_eq_lmul_left_sub_lmul_right]

Premises used: LieAlgebra.ad_eq_lmul_left_sub_lmul_right
-- Module: Mathlib.Algebra.Lie.AdjointAction.Basic
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
a : A
h rwa rwa₁ rwa₂ rwa₃ : IsNilpotent a
⊢ IsNilpotent (R := A →ₗ[R] A) (LinearMap.mulLeft R a)

Tactic:
rwa [LinearMap.isNilpotent_mulLeft_iff]

Premises used: LinearMap.isNilpotent_mulLeft_iff
-- Module: Mathlib.Algebra.Lie.AdjointAction.Basic
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
a : A
h : IsNilpotent a
⊢ IsNilpotent (R := A →ₗ[R] A) (LinearMap.mulLeft R a)

Tactic:
have hl : IsNilpotent (LinearMap.mulLeft R a) := by rwa [LinearMap.isNilpotent_mulLeft_iff]
-- Module: Mathlib.Algebra.Lie.AdjointAction.Basic
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
a : A
h : IsNilpotent a
hl : IsNilpotent (R := A →ₗ[R] A) (LinearMap.mulLeft R a)
rwa rwa₁ rwa₂ rwa₃ : IsNilpotent a
⊢ IsNilpotent (R := A →ₗ[R] A) (LinearMap.mulRight R a)

Tactic:
rwa [LinearMap.isNilpotent_mulRight_iff]

Premises used: LinearMap.isNilpotent_mulRight_iff
-- Module: Mathlib.Algebra.Lie.AdjointAction.Basic
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
a : A
h : IsNilpotent a
hl : IsNilpotent (R := A →ₗ[R] A) (LinearMap.mulLeft R a)
⊢ IsNilpotent (R := A →ₗ[R] A) (LinearMap.mulRight R a)

Tactic:
have hr : IsNilpotent (LinearMap.mulRight R a) := by rwa [LinearMap.isNilpotent_mulRight_iff]
-- Module: Mathlib.Algebra.Lie.AdjointAction.Basic
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
a : A
h : IsNilpotent a
hl : IsNilpotent (R := A →ₗ[R] A) (LinearMap.mulLeft R a)
hr : IsNilpotent (R := A →ₗ[R] A) (LinearMap.mulRight R a)
⊢ IsNilpotent
    (HSub.hSub (α := (a : A) → A →ₗ[R] A) (β := (b : A) → A →ₗ[R] A) (LinearMap.mulLeft R) (LinearMap.mulRight R) a)

Tactic:
(LinearMap.commute_mulLeft_right a a).isNilpotent_sub hl hr

Premises used: LinearMap.commute_mulLeft_right, Commute.isNilpotent_sub
-- Module: Mathlib.Algebra.Lie.AdjointAction.Basic
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
a : A
h : IsNilpotent a
hl : IsNilpotent (R := A →ₗ[R] A) (LinearMap.mulLeft R a)
hr : IsNilpotent (R := A →ₗ[R] A) (LinearMap.mulRight R a)
⊢ IsNilpotent
    (HSub.hSub (α := (a : A) → A →ₗ[R] A) (β := (b : A) → A →ₗ[R] A) (LinearMap.mulLeft R) (LinearMap.mulRight R) a)

Tactic:
exact (LinearMap.commute_mulLeft_right a a).isNilpotent_sub hl hr

Premises used: LinearMap.commute_mulLeft_right, Commute.isNilpotent_sub
-- Module: Mathlib.Algebra.Lie.AdjointAction.Basic
Goal:
R : Type u_1
inst : CommRing R
L : Type u_3
inst_1 : LieRing L
inst_2 : LieAlgebra R L
K : LieSubalgebra R L
x : ↥K
h : IsNilpotent (R := Module.End R L) ((LieAlgebra.ad R L : (a : L) → Module.End R L) (↑x : L) : Module.End R L)
obtain :
  ∀ (n : ℕ)
    (hn :
      HPow.hPow (α := Module.End R L) ((LieAlgebra.ad R L : (a : L) → Module.End R L) (↑x : L) : Module.End R L) n = 0),
    IsNilpotent (R := Module.End R ↥K) ((LieAlgebra.ad R ↥K : (a : ↥K) → Module.End R ↥K) x : Module.End R ↥K)
⊢ IsNilpotent (R := Module.End R ↥K) ((LieAlgebra.ad R ↥K : (a : ↥K) → Module.End R ↥K) x : Module.End R ↥K)

Tactic:
obtain ⟨n, hn⟩ := h
-- Module: Mathlib.Algebra.Lie.AdjointAction.Basic
Goal:
R : Type u_1
inst : CommRing R
L : Type u_3
inst_1 : LieRing L
inst_2 : LieAlgebra R L
K : LieSubalgebra R L
x : ↥K
n : ℕ
hn : HPow.hPow (α := Module.End R L) ((LieAlgebra.ad R L : (a : L) → Module.End R L) (↑x : L) : Module.End R L) n = 0
h : HPow.hPow (α := Module.End R ↥K) ((LieAlgebra.ad R ↥K : (a : ↥K) → Module.End R ↥K) x : Module.End R ↥K) n = 0
⊢ IsNilpotent (R := Module.End R ↥K) ((LieAlgebra.ad R ↥K : (a : ↥K) → Module.End R ↥K) x : Module.End R ↥K)

Tactic:
use n
-- Module: Mathlib.Algebra.Lie.AdjointAction.Basic
Goal:
R : Type u_1
inst : CommRing R
L : Type u_3
inst_1 : LieRing L
inst_2 : LieAlgebra R L
K : LieSubalgebra R L
x : ↥K
n : ℕ
hn : HPow.hPow (α := Module.End R L) ((LieAlgebra.ad R L : (a : L) → Module.End R L) (↑x : L) : Module.End R L) n = 0
⊢ HPow.hPow (α := Module.End R ↥K) ((LieAlgebra.ad R ↥K : (a : ↥K) → Module.End R ↥K) x : Module.End R ↥K) n = 0

Tactic:
Module.End.submodule_pow_eq_zero_of_pow_eq_zero (K.ad_comp_incl_eq x) hn

Premises used: Set.Mem, Module.End.submodule_pow_eq_zero_of_pow_eq_zero, LieSubalgebra.ad_comp_incl_eq
-- Module: Mathlib.Algebra.Lie.AdjointAction.Basic
Goal:
R : Type u_1
inst : CommRing R
L : Type u_3
inst_1 : LieRing L
inst_2 : LieAlgebra R L
K : LieSubalgebra R L
x : ↥K
n : ℕ
hn : HPow.hPow (α := Module.End R L) ((LieAlgebra.ad R L : (a : L) → Module.End R L) (↑x : L) : Module.End R L) n = 0
⊢ HPow.hPow (α := Module.End R ↥K) ((LieAlgebra.ad R ↥K : (a : ↥K) → Module.End R ↥K) x : Module.End R ↥K) n = 0

Tactic:
exact Module.End.submodule_pow_eq_zero_of_pow_eq_zero (K.ad_comp_incl_eq x) hn

Premises used: Module.End.submodule_pow_eq_zero_of_pow_eq_zero, LieSubalgebra.ad_comp_incl_eq
-- Module: Mathlib.Algebra.Lie.AdjointAction.Basic
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
L : LieSubalgebra R A
x : ↥L
h : IsNilpotent (↑x : A)
⊢ IsNilpotent (R := Module.End R ↥L) ((ad R ↥L : (a : ↥L) → Module.End R ↥L) x : Module.End R ↥L)

Tactic:
L.isNilpotent_ad_of_isNilpotent_ad <| LieAlgebra.ad_nilpotent_of_nilpotent h

Premises used: LieAlgebra.ad_nilpotent_of_nilpotent, LieSubalgebra.isNilpotent_ad_of_isNilpotent_ad
-- Module: Mathlib.Algebra.Lie.AdjointAction.Basic
Goal:
K : Type u_1
V : Type u_2
inst : Field K
inst_1 : PerfectField K
inst_2 : AddCommGroup V
inst_3 : Module K V
inst_4 : FiniteDimensional K V
a : Module.End K V
ha : a.IsSemisimple
rw :
  (HSub.hSub (α := (a : Module.End K V) → Module.End K V →ₗ[K] Module.End K V) (β :=
      (b : Module.End K V) → Module.End K V →ₗ[K] Module.End K V) (LinearMap.mulLeft K) (LinearMap.mulRight K)
      a).IsSemisimple
⊢ Module.End.IsSemisimple.{u_1, u_2} (R := K) (M := Module.End K V)
    ((ad K (Module.End K V) : (a : Module.End K V) → Module.End K (Module.End K V)) a)

Tactic:
rw [LieAlgebra.ad_eq_lmul_left_sub_lmul_right]

Premises used: LieAlgebra.ad_eq_lmul_left_sub_lmul_right
-- Module: Mathlib.Algebra.Lie.AdjointAction.Basic
Goal:
K : Type u_1
V : Type u_2
inst : Field K
inst_1 : PerfectField K
inst_2 : AddCommGroup V
inst_3 : Module K V
inst_4 : FiniteDimensional K V
a : Module.End K V
ha : a.IsSemisimple
apply :
  Eq.{u_2 + 1} (α := Module.End K (Module.End K V))
    ((Polynomial.aeval (LinearMap.mulLeft K a) : (a : Polynomial K) → Module.End K (Module.End K V)) (minpoly K a) :
      Module.End K (Module.End K V))
    (0 : Module.End K (Module.End K V))
⊢ Module.End.IsSemisimple (LinearMap.mulLeft K a)

Tactic:
apply Module.End.isSemisimple_of_squarefree_aeval_eq_zero ha.minpoly_squarefree

Premises used: Module.End.isSemisimple_of_squarefree_aeval_eq_zero, Module.End.IsSemisimple.minpoly_squarefree
-- Module: Mathlib.Algebra.Lie.AdjointAction.Basic
Goal:
K : Type u_1
V : Type u_2
inst : Field K
inst_1 : PerfectField K
inst_2 : AddCommGroup V
inst_3 : Module K V
inst_4 : FiniteDimensional K V
a : Module.End K V
ha : a.IsSemisimple
rw :
  Eq.{u_2 + 1} (α := Module.End K (Module.End K V))
    ((Algebra.lmul K (Module.End K V) : (a : Module.End K V) → Module.End K (Module.End K V))
        ((Polynomial.aeval a : (a : Polynomial K) → Module.End K V) (minpoly K a) : Module.End K V) :
      Module.End K (Module.End K V))
    (0 : Module.End K (Module.End K V))
rw₁ :
  Eq.{u_2 + 1} (α := Module.End K (Module.End K V))
    ((Algebra.lmul K (Module.End K V) : (a : Module.End K V) → Module.End K (Module.End K V)) 0 :
      Module.End K (Module.End K V))
    (0 : Module.End K (Module.End K V))
rw₂ rw₃ : Eq.{u_2 + 1} (α := Module.End K (Module.End K V)) 0 0
⊢ Eq.{u_2 + 1} (α := Module.End K (Module.End K V))
    (((Polynomial.aeval ((Algebra.lmul K (Module.End K V) : (a : Module.End K V) → Module.End K (Module.End K V)) a) :
            AlgHom.{u_1, u_1, u_2} K (Polynomial K) (Module.End K (Module.End K V))) :
          (a : Polynomial K) → Module.End K (Module.End K V))
        (minpoly K a) :
      Module.End K (Module.End K V))
    (0 : Module.End K (Module.End K V))

Tactic:
rw [Polynomial.aeval_algHom_apply, minpoly.aeval, map_zero]

Premises used: map_zero, minpoly.aeval, Polynomial.aeval_algHom_apply
-- Module: Mathlib.Algebra.Lie.AdjointAction.Basic
Goal:
K : Type u_1
V : Type u_2
inst : Field K
inst_1 : PerfectField K
inst_2 : AddCommGroup V
inst_3 : Module K V
inst_4 : FiniteDimensional K V
a : Module.End K V
ha : a.IsSemisimple
⊢ Eq.{u_2 + 1} (α := Module.End K (Module.End K V))
    (((Polynomial.aeval ((Algebra.lmul K (Module.End K V) : (a : Module.End K V) → Module.End K (Module.End K V)) a) :
            AlgHom.{u_1, u_1, u_2} K (Polynomial K) (Module.End K (Module.End K V))) :
          (a : Polynomial K) → Module.End K (Module.End K V))
        (minpoly K a) :
      Module.End K (Module.End K V))
    (0 : Module.End K (Module.End K V))

Tactic:
have : Polynomial.aeval (Algebra.lmul K (Module.End K V) a) (minpoly K a) = 0 := by
      rw [Polynomial.aeval_algHom_apply, minpoly.aeval, map_zero]
-- Module: Mathlib.Algebra.Lie.AdjointAction.Basic
Goal:
K : Type u_1
V : Type u_2
inst : Field K
inst_1 : PerfectField K
inst_2 : AddCommGroup V
inst_3 : Module K V
inst_4 : FiniteDimensional K V
a : Module.End K V
ha : a.IsSemisimple
this :
  Eq.{u_2 + 1} (α := Module.End K (Module.End K V))
    (((Polynomial.aeval ((Algebra.lmul K (Module.End K V) : (a : Module.End K V) → Module.End K (Module.End K V)) a) :
            AlgHom.{u_1, u_1, u_2} K (Polynomial K) (Module.End K (Module.End K V))) :
          (a : Polynomial K) → Module.End K (Module.End K V))
        (minpoly K a) :
      Module.End K (Module.End K V))
    (0 : Module.End K (Module.End K V))
⊢ Eq.{u_2 + 1} (α := Module.End K (Module.End K V))
    ((Polynomial.aeval (LinearMap.mulLeft K a) : (a : Polynomial K) → Module.End K (Module.End K V)) (minpoly K a) :
      Module.End K (Module.End K V))
    (0 : Module.End K (Module.End K V))

Tactic:
simpa using this