-- Mathlib/LinearAlgebra/Semisimple.lean
theorem isSemisimple_of_squarefree_aeval_eq_zero {p : K[X]}
    (hp : Squarefree p) (hpf : aeval f p = 0) : f.IsSemisimple

Proof state:
M : Type u_2
inst✝² : AddCommGroup M
K : Type u_3
inst✝¹ : Field K
inst✝ : Module K M
f : End K M
p : K[X]
hp : Squarefree p
hpf : IsTorsionBySet K[X] (AEval K M f) ↑(Ideal.span {p})
R : Type u_3 := K[X] ⧸ Ideal.span {p}
this : IsReduced R
⊢ f.IsSemisimple

Tactic:
have : FiniteDimensional K R := (AdjoinRoot.powerBasis hp.ne_zero).finite

Result:
M : Type u_2
inst✝² : AddCommGroup M
K : Type u_3
inst✝¹ : Field K
inst✝ : Module K M
f : End K M
p : K[X]
hp : Squarefree p
hpf : IsTorsionBySet K[X] (AEval K M f) ↑(Ideal.span {p})
R : Type u_3 := K[X] ⧸ Ideal.span {p}
this✝ : IsReduced R
this : FiniteDimensional K R
⊢ f.IsSemisimple

Proof state:
M : Type u_2
inst✝² : AddCommGroup M
K : Type u_3
inst✝¹ : Field K
inst✝ : Module K M
f : End K M
p : K[X]
hp : Squarefree p
hpf : IsTorsionBySet K[X] (AEval K M f) ↑(Ideal.span {p})
R : Type u_3 := K[X] ⧸ Ideal.span {p}
this✝ : IsReduced R
this : FiniteDimensional K R
⊢ f.IsSemisimple

Tactic:
have : IsArtinianRing R := .of_finite K R

Result:
M : Type u_2
inst✝² : AddCommGroup M
K : Type u_3
inst✝¹ : Field K
inst✝ : Module K M
f : End K M
p : K[X]
hp : Squarefree p
hpf : IsTorsionBySet K[X] (AEval K M f) ↑(Ideal.span {p})
R : Type u_3 := K[X] ⧸ Ideal.span {p}
this✝¹ : IsReduced R
this✝ : FiniteDimensional K R
this : IsArtinianRing R
⊢ f.IsSemisimple

Proof state:
M : Type u_2
inst✝² : AddCommGroup M
K : Type u_3
inst✝¹ : Field K
inst✝ : Module K M
f : End K M
p : K[X]
hp : Squarefree p
hpf : IsTorsionBySet K[X] (AEval K M f) ↑(Ideal.span {p})
R : Type u_3 := K[X] ⧸ Ideal.span {p}
this✝³ : IsReduced R
this✝² : FiniteDimensional K R
this✝¹ : IsArtinianRing R
this✝ : IsSemisimpleRing R
this : Module R (AEval' f) := hpf.module
⊢ f.IsSemisimple

Tactic:
let e : AEval' f →ₛₗ[Ideal.Quotient.mk (Ideal.span {p})] AEval' f :=
  { AddMonoidHom.id _ with map_smul' := fun _ _ ↦ rfl }

Result:
M : Type u_2
inst✝² : AddCommGroup M
K : Type u_3
inst✝¹ : Field K
inst✝ : Module K M
f : End K M
p : K[X]
hp : Squarefree p
hpf : IsTorsionBySet K[X] (AEval K M f) ↑(Ideal.span {p})
R : Type u_3 := K[X] ⧸ Ideal.span {p}
this✝³ : IsReduced R
this✝² : FiniteDimensional K R
this✝¹ : IsArtinianRing R
this✝ : IsSemisimpleRing R
this : Module R (AEval' f) := hpf.module
e : AEval' f →ₛₗ[Ideal.Quotient.mk (Ideal.span {p})] AEval' f :=
  let __src := AddMonoidHom.id (AEval' f);
  { toFun := (↑__src).toFun, map_add' := ⋯, map_smul' := ⋯ }
⊢ f.IsSemisimple

Proof state:
M : Type u_2
inst✝² : AddCommGroup M
K : Type u_3
inst✝¹ : Field K
inst✝ : Module K M
f : End K M
p : K[X]
hp : Squarefree p
hpf : IsTorsionBySet K[X] (AEval K M f) ↑(Ideal.span {p})
R : Type u_3 := K[X] ⧸ Ideal.span {p}
this✝² : IsReduced R
this✝¹ : FiniteDimensional K R
this✝ : IsArtinianRing R
this : IsSemisimpleRing R
⊢ f.IsSemisimple

Tactic:
letI : Module R (AEval' f) := Module.IsTorsionBySet.module hpf

Result:
M : Type u_2
inst✝² : AddCommGroup M
K : Type u_3
inst✝¹ : Field K
inst✝ : Module K M
f : End K M
p : K[X]
hp : Squarefree p
hpf : IsTorsionBySet K[X] (AEval K M f) ↑(Ideal.span {p})
R : Type u_3 := K[X] ⧸ Ideal.span {p}
this✝³ : IsReduced R
this✝² : FiniteDimensional K R
this✝¹ : IsArtinianRing R
this✝ : IsSemisimpleRing R
this : Module R (AEval' f) := hpf.module
⊢ f.IsSemisimple

Proof state:
M : Type u_2
inst✝² : AddCommGroup M
K : Type u_3
inst✝¹ : Field K
inst✝ : Module K M
f : End K M
p : K[X]
hp : Squarefree p
hpf : IsTorsionBySet K[X] (AEval K M f) ↑(Ideal.span {p})
R : Type u_3 := K[X] ⧸ Ideal.span {p}
⊢ f.IsSemisimple

Tactic:
have : IsReduced R :=
  (Ideal.isRadical_iff_quotient_reduced _).mp (isRadical_iff_span_singleton.mp hp.isRadical)

Result:
M : Type u_2
inst✝² : AddCommGroup M
K : Type u_3
inst✝¹ : Field K
inst✝ : Module K M
f : End K M
p : K[X]
hp : Squarefree p
hpf : IsTorsionBySet K[X] (AEval K M f) ↑(Ideal.span {p})
R : Type u_3 := K[X] ⧸ Ideal.span {p}
this : IsReduced R
⊢ f.IsSemisimple

Proof state:
M : Type u_2
inst✝² : AddCommGroup M
K : Type u_3
inst✝¹ : Field K
inst✝ : Module K M
f : End K M
p : K[X]
hp : Squarefree p
hpf : IsTorsionBySet K[X] (AEval K M f) ↑(Ideal.span {p})
⊢ f.IsSemisimple

Tactic:
let R := K[X] ⧸ Ideal.span {p}

Result:
M : Type u_2
inst✝² : AddCommGroup M
K : Type u_3
inst✝¹ : Field K
inst✝ : Module K M
f : End K M
p : K[X]
hp : Squarefree p
hpf : IsTorsionBySet K[X] (AEval K M f) ↑(Ideal.span {p})
R : Type u_3 := K[X] ⧸ Ideal.span {p}
⊢ f.IsSemisimple

Proof state:
M : Type u_2
inst✝² : AddCommGroup M
K : Type u_3
inst✝¹ : Field K
inst✝ : Module K M
f : End K M
p : K[X]
hp : Squarefree p
hpf : IsTorsionBySet K[X] (AEval K M f) ↑(Ideal.span {p})
R : Type u_3 := K[X] ⧸ Ideal.span {p}
this✝¹ : IsReduced R
this✝ : FiniteDimensional K R
this : IsArtinianRing R
⊢ f.IsSemisimple

Tactic:
have : IsSemisimpleRing R := IsArtinianRing.isSemisimpleRing_of_isReduced R

Result:
M : Type u_2
inst✝² : AddCommGroup M
K : Type u_3
inst✝¹ : Field K
inst✝ : Module K M
f : End K M
p : K[X]
hp : Squarefree p
hpf : IsTorsionBySet K[X] (AEval K M f) ↑(Ideal.span {p})
R : Type u_3 := K[X] ⧸ Ideal.span {p}
this✝² : IsReduced R
this✝¹ : FiniteDimensional K R
this✝ : IsArtinianRing R
this : IsSemisimpleRing R
⊢ f.IsSemisimple

Proof state:
M : Type u_2
inst✝² : AddCommGroup M
K : Type u_3
inst✝¹ : Field K
inst✝ : Module K M
f : End K M
p : K[X]
hp : Squarefree p
hpf : (aeval f) p = 0
⊢ f.IsSemisimple

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

Result:
M : Type u_2
inst✝² : AddCommGroup M
K : Type u_3
inst✝¹ : Field K
inst✝ : Module K M
f : End K M
p : K[X]
hp : Squarefree p
hpf : IsTorsionBySet K[X] (AEval K M f) ↑(Ideal.span {p})
⊢ f.IsSemisimple

Proof state:
M : Type u_2
inst✝² : AddCommGroup M
K : Type u_3
inst✝¹ : Field K
inst✝ : Module K M
f : End K M
p : K[X]
hp : Squarefree p
hpf : IsTorsionBySet K[X] (AEval K M f) ↑(Ideal.span {p})
R : Type u_3 := K[X] ⧸ Ideal.span {p}
this✝³ : IsReduced R
this✝² : FiniteDimensional K R
this✝¹ : IsArtinianRing R
this✝ : IsSemisimpleRing R
this : Module R (AEval' f) := hpf.module
e : AEval' f →ₛₗ[Ideal.Quotient.mk (Ideal.span {p})] AEval' f :=
  let __src := AddMonoidHom.id (AEval' f);
  { toFun := (↑__src).toFun, map_add' := ⋯, map_smul' := ⋯ }
⊢ f.IsSemisimple

Tactic:
exact (e.isSemisimpleModule_iff_of_bijective bijective_id).mpr inferInstance

Result:
no goals