awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Semisimple (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
hn : IsNilpotent f
hs : f.IsFinitelySemisimple
this :
  ∀ (p : Submodule R M) (hp₁ : p ∈ f.invtSubmodule) (hp₂ : Module.Finite.{u_1, u_2} R ↥p), LinearMap.restrict f hp₁ = 0
⊢ f = 0
have h : ∀ (x : M), Eq (α := M) ((f : (a : M) → M) x : M) ((0 : (a : M) → M) x : M)
Tactic: ext x
-- Lean 4 proof step from Mathlib.LinearAlgebra.Semisimple (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
hn : IsNilpotent f
hs : f.IsFinitelySemisimple
this :
  ∀ (p : Submodule R M) (hp₁ : p ∈ f.invtSubmodule) (hp₂ : Module.Finite.{u_1, u_2} R ↥p), LinearMap.restrict f hp₁ = 0
x : M
⊢ Eq (α := M) ((f : (a : M) → M) x : M) ((0 : (a : M) → M) x : M)
have h : ∀ (k : ℕ) (hk : f ^ k = 0), Eq (α := M) ((f : (a : M) → M) x : M) ((0 : (a : M) → M) x : M)
Tactic: obtain ⟨k : ℕ, hk : f ^ k = 0⟩ := hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.LinearAlgebra.Semisimple (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
hs : f.IsFinitelySemisimple
this :
  ∀ (p : Submodule R M) (hp₁ : p ∈ f.invtSubmodule) (hp₂ : Module.Finite.{u_1, u_2} R ↥p), LinearMap.restrict f hp₁ = 0
x : M
k : ℕ
hk : f ^ k = 0
p : Submodule R M := Submodule.span R {x_1 : M | ∃ (i : ℕ) (_ : i ≤ k), (f ^ i : (a : M) → M) x = x_1}
⊢ p ∈ f.invtSubmodule
have simp : {x_1 : M | ∃ (i : ℕ) (_ : i ≤ k), (f ^ i : (a : M) → M) x = x_1} ⊆
  (↑(Submodule.comap f (Submodule.span R {x_1 : M | ∃ (i : ℕ) (_ : i ≤ k), (f ^ i : (a : M) → M) x = x_1})) : Set M)
Tactic: simp only [mem_invtSubmodule, p, Submodule.span_le]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Semisimple (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
hs : f.IsFinitelySemisimple
this :
  ∀ (p : Submodule R M) (hp₁ : p ∈ f.invtSubmodule) (hp₂ : Module.Finite.{u_1, u_2} R ↥p), LinearMap.restrict f hp₁ = 0
x : M
k : ℕ
hk : f ^ k = 0
p : Submodule R M := Submodule.span R {x_1 : M | ∃ (i : ℕ) (_ : i ≤ k), (f ^ i : (a : M) → M) x = x_1}
i : ℕ
hi : i ≤ k
⊢ Membership.mem (α := M)
    (↑(Submodule.comap f (Submodule.span R {x_1 : M | ∃ (i : ℕ) (_ : i ≤ k), (f ^ i : (a : M) → M) x = x_1})) : Set M)
    ((f ^ i : (a : M) → M) x : M)
have a : Membership.mem (α := M) (γ := Set M) {x_1 : M | ∃ (i : ℕ) (_ : i ≤ k), (f ^ i : (a : M) → M) x = x_1}
  ((f : (a : M) → M) ((f ^ i : (a : M) → M) x : M) : M)
Tactic: apply Submodule.subset_span
-- Lean 4 proof step from Mathlib.LinearAlgebra.Semisimple (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
hs : f.IsFinitelySemisimple
this :
  ∀ (p : Submodule R M) (hp₁ : p ∈ f.invtSubmodule) (hp₂ : Module.Finite.{u_1, u_2} R ↥p), LinearMap.restrict f hp₁ = 0
x : M
k : ℕ
hk : f ^ k = 0
p : Submodule R M := Submodule.span R {x_1 : M | ∃ (i : ℕ) (_ : i ≤ k), (f ^ i : (a : M) → M) x = x_1}
i : ℕ
hi : i ≤ k
⊢ Membership.mem (α := M) (γ := Set M) {x_1 : M | ∃ (i : ℕ) (_ : i ≤ k), (f ^ i : (a : M) → M) x = x_1}
    ((f : (a : M) → M) ((f ^ i : (a : M) → M) x : M) : M)
have a : ∀ (hik : i < k),
  Membership.mem (α := M) (γ := Set M) {x_1 : M | ∃ (i : ℕ) (_ : i ≤ k), (f ^ i : (a : M) → M) x = x_1}
    ((f : (a : M) → M) ((f ^ i : (a : M) → M) x : M) : M)
Tactic: rcases lt_or_eq_of_le hi with hik | rfl
-- Lean 4 proof step from Mathlib.LinearAlgebra.Semisimple (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
hs : f.IsFinitelySemisimple
this :
  ∀ (p : Submodule R M) (hp₁ : p ∈ f.invtSubmodule) (hp₂ : Module.Finite.{u_1, u_2} R ↥p), LinearMap.restrict f hp₁ = 0
x : M
k : ℕ
hk : f ^ k = 0
p : Submodule R M := Submodule.span R {x_1 : M | ∃ (i : ℕ) (_ : i ≤ k), (f ^ i : (a : M) → M) x = x_1}
i : ℕ
hi : i ≤ k
a :
  ∀ (hik : i < k),
    Membership.mem (α := M) (γ := Set M) {x_1 : M | ∃ (i : ℕ) (_ : i ≤ k), (f ^ i : (a : M) → M) x = x_1}
      ((f : (a : M) → M) ((f ^ i : (a : M) → M) x : M) : M)
⊢ Membership.mem (α := M) (γ := Set M) {x_1 : M | ∃ (i : ℕ) (_ : i ≤ k), (f ^ i : (a : M) → M) x = x_1}
    ((f : (a : M) → M) ((f ^ i : (a : M) → M) x : M) : M)
have a₁ : ∀ (hk : f ^ i = 0) (hi : i ≤ i),
  Membership.mem (α := M) (γ := Set M) {x_1 : M | ∃ (i_1 : ℕ) (_ : i_1 ≤ i), (f ^ i_1 : (a : M) → M) x = x_1}
    ((f : (a : M) → M) ((f ^ i : (a : M) → M) x : M) : M)
Tactic: rcases lt_or_eq_of_le hi with hik | rfl
Cleared hypotheses: k, hk, p, hi
-- Lean 4 proof step from Mathlib.LinearAlgebra.Semisimple (hypothesis)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
hs : f.IsFinitelySemisimple
this :
  ∀ (p : Submodule R M) (hp₁ : p ∈ f.invtSubmodule) (hp₂ : Module.Finite.{u_1, u_2} R ↥p), LinearMap.restrict f hp₁ = 0
x : M
k : ℕ
hk : f ^ k = 0
p : Submodule R M := Submodule.span R {x_1 : M | ∃ (i : ℕ) (_ : i ≤ k), (f ^ i : (a : M) → M) x = x_1}
⊢ Eq (α := M) ((f : (a : M) → M) x : M) ((0 : (a : M) → M) x : M)
have hp₁ : p ∈ f.invtSubmodule
Tactic: have hp₁ : p ∈ f.invtSubmodule := by
    simp only [mem_invtSubmodule, p, Submodule.span_le]
    rintro - ⟨i, hi, rfl⟩
    apply Submodule.subset_span
    rcases lt_or_eq_of_le hi with hik | rfl
    · exact ⟨i + 1, hik, by simpa [Module.End.pow_apply] using iterate_succ_apply' f i x⟩
    · exact ⟨i, by simp [hk]⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Semisimple (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
hs : f.IsFinitelySemisimple
this :
  ∀ (p : Submodule R M) (hp₁ : p ∈ f.invtSubmodule) (hp₂ : Module.Finite.{u_1, u_2} R ↥p), LinearMap.restrict f hp₁ = 0
x : M
k : ℕ
hk : f ^ k = 0
p : Submodule R M := Submodule.span R {x_1 : M | ∃ (i : ℕ) (_ : i ≤ k), (f ^ i : (a : M) → M) x = x_1}
hp₁ : p ∈ f.invtSubmodule
g : ℕ → M := fun (i : ℕ) ↦ (f ^ i : (a : M) → M) x
⊢ {x_1 : M | ∃ (i : ℕ) (_ : i ≤ k), (f ^ i : (a : M) → M) x = x_1} = g '' Iic k
have h : ∀ (x_1 : M),
  Membership.mem (γ := Set M) {x_2 : M | ∃ (i : ℕ) (_ : i ≤ k), (f ^ i : (a : M) → M) x = x_2} x_1 ↔ x_1 ∈ g '' Iic k
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Semisimple (hypothesis)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
hs : f.IsFinitelySemisimple
this :
  ∀ (p : Submodule R M) (hp₁ : p ∈ f.invtSubmodule) (hp₂ : Module.Finite.{u_1, u_2} R ↥p), LinearMap.restrict f hp₁ = 0
x : M
k : ℕ
hk : f ^ k = 0
p : Submodule R M := Submodule.span R {x_1 : M | ∃ (i : ℕ) (_ : i ≤ k), (f ^ i : (a : M) → M) x = x_1}
hp₁ : p ∈ f.invtSubmodule
g : ℕ → M := fun (i : ℕ) ↦ (f ^ i : (a : M) → M) x
⊢ Module.Finite.{u_1, u_2} R ↥p
have hg : {x_1 : M | ∃ (i : ℕ) (_ : i ≤ k), (f ^ i : (a : M) → M) x = x_1} = g '' Iic k
Tactic: have hg : {(f ^ i) x | (i : ℕ) (_ : i ≤ k)} = g '' Iic k := by ext; simp [g]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Semisimple (hypothesis)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
hs : f.IsFinitelySemisimple
this :
  ∀ (p : Submodule R M) (hp₁ : p ∈ f.invtSubmodule) (hp₂ : Module.Finite.{u_1, u_2} R ↥p), LinearMap.restrict f hp₁ = 0
x : M
k : ℕ
hk : f ^ k = 0
p : Submodule R M := Submodule.span R {x_1 : M | ∃ (i : ℕ) (_ : i ≤ k), (f ^ i : (a : M) → M) x = x_1}
hp₁ : p ∈ f.invtSubmodule
⊢ Eq (α := M) ((f : (a : M) → M) x : M) ((0 : (a : M) → M) x : M)
have hp₂ : Module.Finite.{u_1, u_2} R ↥p
Tactic: have hp₂ : Module.Finite R p := by
    let g : ℕ → M := fun i ↦ (f ^ i) x
    have hg : {(f ^ i) x | (i : ℕ) (_ : i ≤ k)} = g '' Iic k := by ext; simp [g]
    exact Module.Finite.span_of_finite _ <| hg ▸ toFinite (g '' Iic k)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Semisimple (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
μ : R
⊢ (HSub.hSub (β := End R M) f ((algebraMap R (End R M) : (a : R) → End R M) μ : End R M)).IsSemisimple ↔ f.IsSemisimple
have suffices : ∀ (p : Submodule R M),
  p ≤ Submodule.comap (HSub.hSub (β := End R M) f ((algebraMap R (End R M) : (a : R) → End R M) μ : End R M)) p ↔
    p ≤ Submodule.comap f p
Tactic: suffices ∀ p : Submodule R M, p ≤ p.comap (f - algebraMap R (Module.End R M) μ) ↔ p ≤ p.comap f by
    simp [mem_invtSubmodule, isSemisimple_iff, this]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Semisimple (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
μ : R
⊢ ∀ (p : Submodule R M),
    p ≤ Submodule.comap (HSub.hSub (β := End R M) f ((algebraMap R (End R M) : (a : R) → End R M) μ : End R M)) p ↔
      p ≤ Submodule.comap f p
have refine : ∀ (p : Submodule R M)
  (h : p ≤ Submodule.comap (HSub.hSub (β := End R M) f ((algebraMap R (End R M) : (a : R) → End R M) μ : End R M)) p)
  (x : M) (hx : x ∈ p), x ∈ Submodule.comap f p
Tactic: refine fun p ↦ ⟨fun h x hx ↦ ?_, fun h x hx ↦ p.sub_mem (h hx) (p.smul_mem μ hx)⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Semisimple (hypothesis)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
p : Submodule R M
hp : p ∈ f.invtSubmodule
hf : f.IsSemisimple
⊢ IsSemisimple (LinearMap.restrict f hp)
have hf₁ : IsSemisimpleModule.{u_1, u_2} R[X] (AEval' f)
Tactic: rw [IsSemisimple] at hf ⊢
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.LinearAlgebra.Semisimple (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
inst_3 : Module.Finite R M
⊢ f.IsFinitelySemisimple ↔ f.IsSemisimple
have refine : ∀ (hf : f.IsFinitelySemisimple) (p : Submodule R M) (hp : p ∈ f.invtSubmodule), ∃ q ∈ f.invtSubmodule, IsCompl p q
Tactic: refine ⟨fun hf ↦ isSemisimple_iff.mpr fun p hp ↦ ?_, IsSemisimple.isFinitelySemisimple⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Semisimple (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
inst_3 : Module.Finite R M
hf : f.IsFinitelySemisimple
p : Submodule R M
hp : p ∈ f.invtSubmodule
⊢ ∃ q ∈ f.invtSubmodule, IsCompl p q
have obtain : ∀ (q : Submodule R M) (hq₁ : q ∈ f.invtSubmodule) (hq₂ : Disjoint p q) (hq₃ : p ⊔ q = ⊤),
  ∃ q ∈ f.invtSubmodule, IsCompl p q
Tactic: obtain ⟨q, -, hq₁, hq₂, hq₃⟩ :=
    isFinitelySemisimple_iff.mp hf ⊤ (invtSubmodule.top_mem f) inferInstance p hp le_top
-- Lean 4 proof step from Mathlib.LinearAlgebra.Semisimple (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
μ : R
this :
  ∀ (p : Submodule R M),
    p ≤ Submodule.comap (HSub.hSub (β := End R M) f ((algebraMap R (End R M) : (a : R) → End R M) μ : End R M)) p ↔
      p ≤ Submodule.comap f p
⊢ (HSub.hSub (β := End R M) f ((algebraMap R (End R M) : (a : R) → End R M) μ : End R M)).IsFinitelySemisimple ↔
    f.IsFinitelySemisimple
have simp_rw : (∀ p ∈ (HSub.hSub (β := End R M) f ((algebraMap R (End R M) : (a : R) → End R M) μ : End R M)).invtSubmodule,
    Module.Finite.{u_1, u_2} R ↥p →
      ∀ q ∈ (HSub.hSub (β := End R M) f ((algebraMap R (End R M) : (a : R) → End R M) μ : End R M)).invtSubmodule,
        q ≤ p →
          ∃ r ≤ p,
            r ∈ (HSub.hSub (β := End R M) f ((algebraMap R (End R M) : (a : R) → End R M) μ : End R M)).invtSubmodule ∧
              Disjoint q r ∧ q ⊔ r = p) ↔
  ∀ p ∈ f.invtSubmodule,
    Module.Finite.{u_1, u_2} R ↥p →
      ∀ q ∈ f.invtSubmodule, q ≤ p → ∃ r ≤ p, r ∈ f.invtSubmodule ∧ Disjoint q r ∧ q ⊔ r = p
Tactic: simp_rw [isFinitelySemisimple_iff, mem_invtSubmodule, this]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Semisimple (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
μ : R
this :
  ∀ (p : Submodule R M),
    p ≤ Submodule.comap (HSub.hSub (β := End R M) f ((algebraMap R (End R M) : (a : R) → End R M) μ : End R M)) p ↔
      p ≤ Submodule.comap f p
simp_rw :
  (∀ p ∈ (HSub.hSub (β := End R M) f ((algebraMap R (End R M) : (a : R) → End R M) μ : End R M)).invtSubmodule,
      Module.Finite.{u_1, u_2} R ↥p →
        ∀ q ∈ (HSub.hSub (β := End R M) f ((algebraMap R (End R M) : (a : R) → End R M) μ : End R M)).invtSubmodule,
          q ≤ p →
            ∃ r ≤ p,
              r ∈
                  (HSub.hSub (β := End R M) f
                      ((algebraMap R (End R M) : (a : R) → End R M) μ : End R M)).invtSubmodule ∧
                Disjoint q r ∧ q ⊔ r = p) ↔
    ∀ p ∈ f.invtSubmodule,
      Module.Finite.{u_1, u_2} R ↥p →
        ∀ q ∈ f.invtSubmodule, q ≤ p → ∃ r ≤ p, r ∈ f.invtSubmodule ∧ Disjoint q r ∧ q ⊔ r = p
⊢ (HSub.hSub (β := End R M) f ((algebraMap R (End R M) : (a : R) → End R M) μ : End R M)).IsFinitelySemisimple ↔
    f.IsFinitelySemisimple
have simp_rw₁ : (∀ p ≤ Submodule.comap (HSub.hSub (β := End R M) f ((algebraMap R (End R M) : (a : R) → End R M) μ : End R M)) p,
    Module.Finite.{u_1, u_2} R ↥p →
      ∀ q ≤ Submodule.comap (HSub.hSub (β := End R M) f ((algebraMap R (End R M) : (a : R) → End R M) μ : End R M)) q,
        q ≤ p →
          ∃ r ≤ p,
            r ≤
                Submodule.comap (HSub.hSub (β := End R M) f ((algebraMap R (End R M) : (a : R) → End R M) μ : End R M))
                  r ∧
              Disjoint q r ∧ q ⊔ r = p) ↔
  ∀ p ≤ Submodule.comap f p,
    Module.Finite.{u_1, u_2} R ↥p →
      ∀ q ≤ Submodule.comap f q, q ≤ p → ∃ r ≤ p, r ≤ Submodule.comap f r ∧ Disjoint q r ∧ q ⊔ r = p
Tactic: simp_rw [isFinitelySemisimple_iff, mem_invtSubmodule, this]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Semisimple (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
μ : R
⊢ (HSub.hSub (β := End R M) f ((algebraMap R (End R M) : (a : R) → End R M) μ : End R M)).IsFinitelySemisimple ↔
    f.IsFinitelySemisimple
have suffices : ∀ (p : Submodule R M),
  p ≤ Submodule.comap (HSub.hSub (β := End R M) f ((algebraMap R (End R M) : (a : R) → End R M) μ : End R M)) p ↔
    p ≤ Submodule.comap f p
Tactic: suffices ∀ p : Submodule R M, p ≤ p.comap (f - algebraMap R (Module.End R M) μ) ↔ p ≤ p.comap f by
    simp_rw [isFinitelySemisimple_iff, mem_invtSubmodule, this]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Semisimple (hypothesis)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
p : Submodule R M
hp : p ∈ f.invtSubmodule
hf : f.IsFinitelySemisimple
q : Submodule R ↥p
hq₁ : q ∈ invtSubmodule (LinearMap.restrict f hp)
hq₂ : Module.Finite.{u_1, u_2} R ↥q
⊢ IsSemisimple ((LinearMap.restrict f hp).restrict hq₁)
have this : Submodule.map p.subtype q ∈ f.invtSubmodule
Tactic: have := invtSubmodule.map_subtype_mem_of_mem_invtSubmodule f hp hq₁
-- Lean 4 proof step from Mathlib.LinearAlgebra.Semisimple (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
p : Submodule R M
hp : p ∈ f.invtSubmodule
hf : f.IsFinitelySemisimple
q : Submodule R ↥p
hq₁ : q ∈ invtSubmodule (LinearMap.restrict f hp)
hq₂ : Module.Finite.{u_1, u_2} R ↥q
this : Submodule.map p.subtype q ∈ f.invtSubmodule
e : ↥q ≃ₗ[R] ↥(Submodule.map p.subtype q) := p.equivSubtypeMap q
⊢ IsSemisimple ((LinearMap.restrict f hp).restrict hq₁)
have rw : IsSemisimple (M := ↥(Submodule.map p.subtype q)) (LinearMap.restrict f this)
Tactic: rw [e.isSemisimple_iff ((LinearMap.restrict f hp).restrict hq₁) (LinearMap.restrict f this) rfl]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Semisimple (goal)
Goal:
M : Type u_2
inst : AddCommGroup M
K : Type u_3
inst_1 : Field K
inst_2 : Module K M
f : End K M
t : K
h : f.IsSemisimple
⊢ (t • f).IsSemisimple
have inr : ∀
  (this :
    ∀ {M : Type u_2} [inst : AddCommGroup M] {K : Type u_3} [inst_3 : Field K] [inst_4 : Module K M] {f : End K M}
      (t : K) (h : f.IsSemisimple) (ht : t ≠ 0), (t • f).IsSemisimple)
  (ht : ¬t ≠ 0), (t • f).IsSemisimple
Tactic: wlog ht : t ≠ 0
-- Lean 4 proof step from Mathlib.LinearAlgebra.Semisimple (goal)
Goal:
M : Type u_2
inst : AddCommGroup M
K : Type u_3
inst_1 : Field K
inst_2 : Module K M
f : End K M
t : K
h : f.IsSemisimple
inr :
  ∀
    (this :
      ∀ {M : Type u_2} [inst : AddCommGroup M] {K : Type u_3} [inst_3 : Field K] [inst_4 : Module K M] {f : End K M}
        (t : K) (h : f.IsSemisimple) (ht : t ≠ 0), (t • f).IsSemisimple)
    (ht : ¬t ≠ 0), (t • f).IsSemisimple
⊢ (t • f).IsSemisimple
have wlog : ∀ {M : Type u_2} [inst : AddCommGroup M] {K : Type u_3} [inst_3 : Field K] [inst_4 : Module K M] {f : End K M} (t : K)
  (h : f.IsSemisimple) (ht : t ≠ 0), (t • f).IsSemisimple
Tactic: wlog ht : t ≠ 0
Cleared hypotheses: t, h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Semisimple (hypothesis)
Goal:
M : Type u_2
inst : AddCommGroup M
K : Type u_3
inst_1 : Field K
inst_2 : Module K M
f : End K M
p : K[X]
hp : Squarefree p
hpf : Eq.{u_2 + 1} (α := End K M) ((aeval f : (a : K[X]) → End K M) p : End K M) (0 : End K M)
⊢ f.IsSemisimple
have hpf₁ : IsTorsionBySet.{u_3, u_2} K[X] (AEval K M f) (↑(Ideal.span {p}) : Set K[X])
Tactic: rw [← RingHom.mem_ker, ← AEval.annihilator_eq_ker_aeval (M := M), mem_annihilator,
      ← IsTorsionBy, ← isTorsionBySet_singleton_iff, isTorsionBySet_iff_is_torsion_by_span] at hpf
Cleared hypotheses: hpf
-- Lean 4 proof step from Mathlib.LinearAlgebra.Semisimple (hypothesis)
Goal:
M : Type u_2
inst : AddCommGroup M
K : Type u_3
inst_1 : Field K
inst_2 : Module K M
f : End K M
p : K[X]
hp : Squarefree p
hpf : IsTorsionBySet.{u_3, u_2} K[X] (AEval K M f) (↑(Ideal.span {p}) : Set K[X])
R : Type u_3 := HasQuotient.Quotient K[X] (B := Ideal K[X]) (Ideal.span {p})
⊢ f.IsSemisimple
have this : IsReduced R
Tactic: have : IsReduced R :=
    (Ideal.isRadical_iff_quotient_reduced _).mp (isRadical_iff_span_singleton.mp hp.isRadical)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Semisimple (hypothesis)
Goal:
M : Type u_2
inst : AddCommGroup M
K : Type u_3
inst_1 : Field K
inst_2 : Module K M
f : End K M
p : K[X]
hp : Squarefree p
hpf : IsTorsionBySet.{u_3, u_2} K[X] (AEval K M f) (↑(Ideal.span {p}) : Set K[X])
R : Type u_3 := HasQuotient.Quotient K[X] (B := Ideal K[X]) (Ideal.span {p})
this : IsReduced R
⊢ f.IsSemisimple
have this₁ : FiniteDimensional K R
Tactic: have : FiniteDimensional K R := (AdjoinRoot.powerBasis hp.ne_zero).finite
-- Lean 4 proof step from Mathlib.LinearAlgebra.Semisimple (hypothesis)
Goal:
M : Type u_2
inst : AddCommGroup M
K : Type u_3
inst_1 : Field K
inst_2 : Module K M
f : End K M
p : K[X]
hp : Squarefree p
hpf : IsTorsionBySet.{u_3, u_2} K[X] (AEval K M f) (↑(Ideal.span {p}) : Set K[X])
R : Type u_3 := HasQuotient.Quotient K[X] (B := Ideal K[X]) (Ideal.span {p})
this_1 : IsReduced R
this : FiniteDimensional K R
⊢ f.IsSemisimple
have this₁ : IsArtinianRing R
Tactic: have : IsArtinianRing R := .of_finite K R
-- Lean 4 proof step from Mathlib.LinearAlgebra.Semisimple (hypothesis)
Goal:
M : Type u_2
inst : AddCommGroup M
K : Type u_3
inst_1 : Field K
inst_2 : Module K M
f : End K M
p : K[X]
hp : Squarefree p
hpf : IsTorsionBySet.{u_3, u_2} K[X] (AEval K M f) (↑(Ideal.span {p}) : Set K[X])
R : Type u_3 := HasQuotient.Quotient K[X] (B := Ideal K[X]) (Ideal.span {p})
this_1 : IsReduced R
this_2 : FiniteDimensional K R
this : IsArtinianRing R
⊢ f.IsSemisimple
have this₁ : IsSemisimpleRing R
Tactic: have : IsSemisimpleRing R := IsArtinianRing.isSemisimpleRing_of_isReduced R
-- Lean 4 proof step from Mathlib.LinearAlgebra.Semisimple (goal)
Goal:
M : Type u_2
inst : AddCommGroup M
K : Type u_3
inst_1 : Field K
inst_2 : Module K M
f : End K M
inst_3 : FiniteDimensional K M
hf : f.IsSemisimple
⊢ IsRadical (R := K[X]) (minpoly K f)
have rw : Ideal.IsRadical.{u_3} (R := K[X]) (annihilator.{u_3, u_2} K[X] (AEval' f))
Tactic: rw [isRadical_iff_span_singleton, span_minpoly_eq_annihilator]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Semisimple (goal)
Goal:
M : Type u_2
inst : AddCommGroup M
K : Type u_3
inst_1 : Field K
inst_2 : Module K M
f : End K M
inst_3 : FiniteDimensional K M
hf : f.IsSemisimple
p : K[X]
R : Type u_3 := HasQuotient.Quotient K[X] (B := Ideal K[X]) (Ideal.span {minpoly K f})
this_1 : Module.Finite K R
this : IsReduced R
a : K[X]
h : Membership.mem (γ := Ideal K[X]) (Ideal.span {minpoly K f}) a
⊢ Eq.{u_2 + 1} (α := End K M) ((aeval f : (a : K[X]) → End K M) a : End K M) (0 : End K M)
have rwa : ∀ (h : Membership.mem (γ := Ideal K[X]) (K[X] ∙ minpoly K f) a),
  Eq.{u_2 + 1} (α := End K M) ((aeval f : (a : K[X]) → End K M) a : End K M) (0 : End K M)
Tactic: rwa [Ideal.span, ← minpoly.ker_aeval_eq_span_minpoly] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Semisimple (goal)
Goal:
M : Type u_2
inst : AddCommGroup M
K : Type u_3
inst_1 : Field K
inst_2 : Module K M
f : End K M
inst_3 : FiniteDimensional K M
hf : f.IsSemisimple
p : K[X]
R : Type u_3 := HasQuotient.Quotient K[X] (B := Ideal K[X]) (Ideal.span {minpoly K f})
this_1 : Module.Finite K R
this : IsReduced R
a : K[X]
h : Membership.mem (γ := Ideal K[X]) (Ideal.span {minpoly K f}) a
rwa :
  ∀ (h : Membership.mem (γ := Ideal K[X]) (K[X] ∙ minpoly K f) a),
    Eq.{u_2 + 1} (α := End K M) ((aeval f : (a : K[X]) → End K M) a : End K M) (0 : End K M)
⊢ Eq.{u_2 + 1} (α := End K M) ((aeval f : (a : K[X]) → End K M) a : End K M) (0 : End K M)
have rwa₁ : ∀ (h : Membership.mem (γ := Ideal K[X]) (RingHom.ker (F := AlgHom.{u_3, u_3, u_2} K K[X] (End K M)) (aeval f)) a),
  Eq.{u_2 + 1} (α := End K M) ((aeval f : (a : K[X]) → End K M) a : End K M) (0 : End K M)
Tactic: rwa [Ideal.span, ← minpoly.ker_aeval_eq_span_minpoly] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Semisimple (goal)
Goal:
M : Type u_2
inst : AddCommGroup M
K : Type u_3
inst_1 : Field K
inst_2 : Module K M
f : End K M
inst_3 : FiniteDimensional K M
hf : f.IsSemisimple
p : K[X]
R : Type u_3 := HasQuotient.Quotient K[X] (B := Ideal K[X]) (Ideal.span {minpoly K f})
this_1 : Module.Finite K R
this : IsReduced R
⊢ Eq.{u_2 + 1} (α := End K M)
    (((aeval ((aeval f : (a : K[X]) → End K M) p) : AlgHom.{u_3, u_3, u_2} K K[X] (End K M)) : (a : K[X]) → End K M)
        (minpoly K (B := HasQuotient.Quotient K[X] (B := Ideal K[X]) (Ideal.span {minpoly K f}))
          ((Ideal.Quotient.mkₐ K (Ideal.span {minpoly K f}) : (a : K[X]) → K[X] ⧸ Ideal.span {minpoly K f}) p :
            HasQuotient.Quotient K[X] (B := Ideal K[X]) (Ideal.span {minpoly K f}))) :
      End K M)
    (0 : End K M)
have rw : Eq.{u_2 + 1} (α := End K M)
  (((aeval
            ((AlgHom.comp (B := HasQuotient.Quotient K[X] (B := Ideal K[X]) (Ideal.span {minpoly K f}))
                  (Ideal.Quotient.liftₐ (Ideal.span {minpoly K f}) (aeval f) sorry)
                  (Ideal.Quotient.mkₐ K (Ideal.span {minpoly K f})) :
                (a : K[X]) → End K M)
              p) :
          AlgHom.{u_3, u_3, u_2} K K[X] (End K M)) :
        (a : K[X]) → End K M)
      (minpoly K (B := HasQuotient.Quotient K[X] (B := Ideal K[X]) (Ideal.span {minpoly K f}))
        ((Ideal.Quotient.mkₐ K (Ideal.span {minpoly K f}) : (a : K[X]) → K[X] ⧸ Ideal.span {minpoly K f}) p :
          HasQuotient.Quotient K[X] (B := Ideal K[X]) (Ideal.span {minpoly K f}))) :
    End K M)
  (0 : End K M)
Tactic: rw [← Ideal.Quotient.liftₐ_comp (.span {minpoly K f}) (aeval f)
        fun a h ↦ by rwa [Ideal.span, ← minpoly.ker_aeval_eq_span_minpoly] at h, aeval_algHom,
        AlgHom.comp_apply, AlgHom.comp_apply, ← aeval_algHom_apply, minpoly.aeval, map_zero]