awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Lie.Abelian (goal)
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)
⊢ 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)
have 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
Tactic: rw [Commute.symm_iff, commute_iff_lie_eq, ← LieHom.map_lie, hx y, map_zero]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Abelian (goal)
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
⊢ 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)
have rw₄ : Eq.{w + 1} (α := Module.End R M) 0 0
Tactic: rw [Commute.symm_iff, commute_iff_lie_eq, ← LieHom.map_lie, hx y, map_zero]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Abelian (goal)
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
⊢ ⁅I, N⁆ = ⊥
have suffices : ⁅I, N⁆ ≤ ⊥
Tactic: suffices ⁅I, N⁆ ≤ ⊥ from le_bot_iff.mp this
-- Lean 4 proof step from Mathlib.Algebra.Lie.Abelian (goal)
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
⊢ ⁅I, N⁆ ≤ ⊥
have rw : {x : M | ∃ (x_1 : ↥I) (n : ↥N), ⁅(↑x_1 : L), (↑n : M)⁆ = x} ⊆ (↑⊥ : Set M)
Tactic: rw [lieIdeal_oper_eq_span, LieSubmodule.lieSpan_le]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Abelian (hypothesis)
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
⊢ m ∈ (↑⊥ : Set M)
have h₁ : 0 = m
Tactic: rw [trivial_lie_zero] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Lie.Abelian (goal)
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 ↔ ⁅I, I⁆ = ⊥
have simp : IsLieAbelian.{v} ↥I ↔ ∀ (y : L) (x : ↥I) (x_1 : ↥I), ⁅(↑x : L), (↑x_1 : L)⁆ = y → y = 0
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]
-- Lean 4 proof step from Mathlib.Algebra.Lie.AdjointAction.Basic (goal)
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
⊢ 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)
have 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)
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]
-- Lean 4 proof step from Mathlib.Algebra.Lie.AdjointAction.Basic (goal)
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)
⊢ 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)
have 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)
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]
-- Lean 4 proof step from Mathlib.Algebra.Lie.AdjointAction.Basic (goal)
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)
⊢ 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)
have 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
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]
-- Lean 4 proof step from Mathlib.Algebra.Lie.AdjointAction.Basic (goal)
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
⊢ 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)
have 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)
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]
-- Lean 4 proof step from Mathlib.Algebra.Lie.AdjointAction.Basic (goal)
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)
⊢ 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)
have 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)
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]
-- Lean 4 proof step from Mathlib.Algebra.Lie.AdjointAction.Basic (goal)
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)
⊢ 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)
have 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)
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]
-- Lean 4 proof step from Mathlib.Algebra.Lie.AdjointAction.Basic (goal)
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)
⊢ 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)
have 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)
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]
-- Lean 4 proof step from Mathlib.Algebra.Lie.AdjointAction.Basic (goal)
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)
⊢ 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)
have rw₇ : Eq.{u_2 + 1} (α := Module.End R A) 0 0
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]
-- Lean 4 proof step from Mathlib.Algebra.Lie.AdjointAction.Basic (goal)
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 := Module.End R A) ((ad R A : (a : A) → Module.End R A) a : Module.End R A)
have rw : IsNilpotent
  (HSub.hSub (α := (a : A) → A →ₗ[R] A) (β := (b : A) → A →ₗ[R] A) (LinearMap.mulLeft R) (LinearMap.mulRight R) a)
Tactic: rw [LieAlgebra.ad_eq_lmul_left_sub_lmul_right]
-- Lean 4 proof step from Mathlib.Algebra.Lie.AdjointAction.Basic (hypothesis)
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
    (HSub.hSub (α := (a : A) → A →ₗ[R] A) (β := (b : A) → A →ₗ[R] A) (LinearMap.mulLeft R) (LinearMap.mulRight R) a)
have hl : IsNilpotent (R := A →ₗ[R] A) (LinearMap.mulLeft R a)
Tactic: have hl : IsNilpotent (LinearMap.mulLeft R a) := by rwa [LinearMap.isNilpotent_mulLeft_iff]
-- Lean 4 proof step from Mathlib.Algebra.Lie.AdjointAction.Basic (hypothesis)
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
    (HSub.hSub (α := (a : A) → A →ₗ[R] A) (β := (b : A) → A →ₗ[R] A) (LinearMap.mulLeft R) (LinearMap.mulRight R) a)
have hr : IsNilpotent (R := A →ₗ[R] A) (LinearMap.mulRight R a)
Tactic: have hr : IsNilpotent (LinearMap.mulRight R a) := by rwa [LinearMap.isNilpotent_mulRight_iff]
-- Lean 4 proof step from Mathlib.Algebra.Lie.AdjointAction.Basic (goal)
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)
⊢ IsNilpotent (R := Module.End R ↥K) ((LieAlgebra.ad R ↥K : (a : ↥K) → Module.End R ↥K) x : Module.End R ↥K)
have 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)
Tactic: obtain ⟨n, hn⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Lie.AdjointAction.Basic (goal)
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
⊢ IsNilpotent (R := Module.End R ↥K) ((LieAlgebra.ad R ↥K : (a : ↥K) → Module.End R ↥K) x : Module.End R ↥K)
have h : HPow.hPow (α := Module.End R ↥K) ((LieAlgebra.ad R ↥K : (a : ↥K) → Module.End R ↥K) x : Module.End R ↥K) n = 0
Tactic: use n
-- Lean 4 proof step from Mathlib.Algebra.Lie.AdjointAction.Basic (goal)
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
⊢ 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)
have 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
Tactic: rw [LieAlgebra.ad_eq_lmul_left_sub_lmul_right]
-- Lean 4 proof step from Mathlib.Algebra.Lie.AdjointAction.Basic (goal)
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
⊢ Module.End.IsSemisimple (LinearMap.mulLeft K a)
have 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))
Tactic: apply Module.End.isSemisimple_of_squarefree_aeval_eq_zero ha.minpoly_squarefree
-- Lean 4 proof step from Mathlib.Algebra.Lie.AdjointAction.Basic (goal)
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))
have 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))
Tactic: rw [Polynomial.aeval_algHom_apply, minpoly.aeval, map_zero]
-- Lean 4 proof step from Mathlib.Algebra.Lie.AdjointAction.Basic (goal)
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))
⊢ 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))
have 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))
Tactic: rw [Polynomial.aeval_algHom_apply, minpoly.aeval, map_zero]