awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Semisimple
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 (M := ↥(Submodule.map p.subtype q)) (LinearMap.restrict f this)

Tactic:
hf _ this (Finite.map q p.subtype)

Premises used: Submodule.subtype, Module.Finite.map
-- Module: Mathlib.LinearAlgebra.Semisimple
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 (M := ↥(Submodule.map p.subtype q)) (LinearMap.restrict f this)

Tactic:
exact hf _ this (Finite.map q p.subtype)

Premises used: Submodule.subtype, Module.Finite.map
-- Module: Mathlib.LinearAlgebra.Semisimple
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
ht : t ≠ 0
⊢ (t • f).IsSemisimple ↔ f.IsSemisimple

Tactic:
simp [isSemisimple_iff, mem_invtSubmodule, Submodule.comap_smul f (h := ht)]

Premises used: Module.End.mem_invtSubmodule, Submodule.comap_smul, Module.End.isSemisimple_iff
-- Module: Mathlib.LinearAlgebra.Semisimple
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
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
⊢ (t • f).IsSemisimple

Tactic:
wlog ht : t ≠ 0
-- Module: Mathlib.LinearAlgebra.Semisimple
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
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:
simp [not_not.mp ht]

Premises used: Classical.not_not, Iff.mp
-- Module: Mathlib.LinearAlgebra.Semisimple
Goal:
M_1 : Type u_2
inst : AddCommGroup M_1
K_1 : Type u_3
inst_1 : Field K_1
inst_2 : Module K_1 M_1
f_1 : End K_1 M_1
M : Type u_2
inst_3 : AddCommGroup M
K : Type u_3
inst_4 : Field K
inst_5 : Module K M
f : End K M
t : K
h : f.IsSemisimple
ht : t ≠ 0
rwa rwa₁ rwa₂ rwa₃ : f.IsSemisimple
⊢ (t • f).IsSemisimple

Tactic:
rwa [IsSemisimple_smul_iff ht]

Premises used: Module.End.IsSemisimple_smul_iff
-- Module: Mathlib.LinearAlgebra.Semisimple
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)
⊢ 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

Premises used: Module.mem_annihilator, Module.IsTorsionBy, RingHom.mem_ker, Module.isTorsionBySet_singleton_iff, Module.isTorsionBySet_iff_is_torsion_by_span, Module.AEval.annihilator_eq_ker_aeval
-- Module: Mathlib.LinearAlgebra.Semisimple
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})
⊢ IsReduced R

Tactic:
have : IsReduced R :=
    (Ideal.isRadical_iff_quotient_reduced _).mp (isRadical_iff_span_singleton.mp hp.isRadical)
-- Module: Mathlib.LinearAlgebra.Semisimple
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
⊢ FiniteDimensional K R

Tactic:
have : FiniteDimensional K R := (AdjoinRoot.powerBasis hp.ne_zero).finite
-- Module: Mathlib.LinearAlgebra.Semisimple
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
⊢ IsArtinianRing R

Tactic:
have : IsArtinianRing R := .of_finite K R
-- Module: Mathlib.LinearAlgebra.Semisimple
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
⊢ IsSemisimpleRing R

Tactic:
have : IsSemisimpleRing R := IsArtinianRing.isSemisimpleRing_of_isReduced R
-- Module: Mathlib.LinearAlgebra.Semisimple
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_3 : IsArtinianRing R
this_4 : IsSemisimpleRing R
this : Module.{u_3, u_2} R (AEval' f) := hpf.module
e : LinearMap (R := K[X]) (S := HasQuotient.Quotient K[X] (B := Ideal K[X]) (Ideal.span {p}))
  (Ideal.Quotient.mk (Ideal.span {p})) (AEval' f) (AEval' f) :=
  let __src : AEval' f →+ AEval' f := AddMonoidHom.id (AEval' f);
  { toFun := (↑__src : ZeroHom (AEval' f) (AEval' f)).toFun, map_add' := ⋯, map_smul' := ⋯ }
⊢ f.IsSemisimple

Tactic:
(e.isSemisimpleModule_iff_of_bijective bijective_id).mpr inferInstance

Premises used: Iff.mpr, Function.bijective_id, Module.AEval, inferInstance, LinearMap.isSemisimpleModule_iff_of_bijective, Module.End.IsSemisimple
-- Module: Mathlib.LinearAlgebra.Semisimple
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_3 : IsArtinianRing R
this_4 : IsSemisimpleRing R
this : Module.{u_3, u_2} R (AEval' f) := hpf.module
e : LinearMap (R := K[X]) (S := HasQuotient.Quotient K[X] (B := Ideal K[X]) (Ideal.span {p}))
  (Ideal.Quotient.mk (Ideal.span {p})) (AEval' f) (AEval' f) :=
  let __src : AEval' f →+ AEval' f := AddMonoidHom.id (AEval' f);
  { toFun := (↑__src : ZeroHom (AEval' f) (AEval' f)).toFun, map_add' := ⋯, map_smul' := ⋯ }
⊢ f.IsSemisimple

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

Premises used: Iff.mpr, Function.bijective_id, inferInstance, LinearMap.isSemisimpleModule_iff_of_bijective
-- Module: Mathlib.LinearAlgebra.Semisimple
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
rw : Ideal.IsRadical.{u_3} (R := K[X]) (annihilator.{u_3, u_2} K[X] (AEval' f))
⊢ IsRadical (R := K[X]) (minpoly K f)

Tactic:
rw [isRadical_iff_span_singleton, span_minpoly_eq_annihilator]

Premises used: isRadical_iff_span_singleton, Polynomial.span_minpoly_eq_annihilator
-- Module: Mathlib.LinearAlgebra.Semisimple
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
⊢ Ideal.IsRadical.{u_3} (R := K[X]) (annihilator.{u_3, u_2} K[X] (AEval' f))

Tactic:
hf.annihilator_isRadical

Premises used: Module.AEval.instAddCommMonoid._aux_4, IsSemisimpleModule.annihilator_isRadical, Module.AEval, Module.AEval.instAddCommMonoid._aux_1
-- Module: Mathlib.LinearAlgebra.Semisimple
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
⊢ Ideal.IsRadical.{u_3} (R := K[X]) (annihilator.{u_3, u_2} K[X] (AEval' f))

Tactic:
exact hf.annihilator_isRadical

Premises used: IsSemisimpleModule.annihilator_isRadical
-- Module: Mathlib.LinearAlgebra.Semisimple
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)
rwa₁ rwa₂ rwa₃ 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)
⊢ 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

Premises used: minpoly.ker_aeval_eq_span_minpoly, Ideal.span
-- Module: Mathlib.LinearAlgebra.Semisimple
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
a : End K M
ha : Membership.mem (γ := Subalgebra K (End K M)) K[f] a
⊢ Membership.mem (γ := Subalgebra K (End K M)) (AlgHom.range (aeval f)) a

Tactic:
rw [adjoin_singleton_eq_range_aeval] at ha

Premises used: Algebra.adjoin_singleton_eq_range_aeval
-- Module: Mathlib.LinearAlgebra.Semisimple
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
a : End K M
ha : Membership.mem (γ := Subalgebra K (End K M)) (AlgHom.range (aeval f)) a
obtain : ∀ (p : K[X]), IsSemisimple.{u_3, u_2} (R := K) (M := M) ((AlgHom.toRingHom (aeval f) : (a : K[X]) → End K M) p)
⊢ a.IsSemisimple

Tactic:
obtain ⟨p, rfl⟩ := ha

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.Semisimple
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]
⊢ IsSemisimple.{u_3, u_2} (R := K) (M := M) ((AlgHom.toRingHom (aeval f) : (a : K[X]) → End K M) p)

Tactic:
.aeval hf _

Premises used: Module.End.IsSemisimple.aeval
-- Module: Mathlib.LinearAlgebra.Semisimple
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]
⊢ IsSemisimple.{u_3, u_2} (R := K) (M := M) ((AlgHom.toRingHom (aeval f) : (a : K[X]) → End K M) p)

Tactic:
exact .aeval hf _
-- Module: Mathlib.LinearAlgebra.Semisimple
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
n : ℕ
⊢ (f ^ n).IsSemisimple

Tactic:
.of_mem_adjoin_singleton hf (pow_mem (self_mem_adjoin_singleton _ _) _)

Premises used: Module.End.IsSemisimple.of_mem_adjoin_singleton, pow_mem, Algebra.self_mem_adjoin_singleton
-- Module: Mathlib.LinearAlgebra.Semisimple
Goal:
M : Type u_2
inst : AddCommGroup M
K : Type u_3
inst_1 : Field K
inst_2 : Module K M
f g : End K M
inst_3 : FiniteDimensional K M
inst_4 : PerfectField K
comm : Commute f g
hf : f.IsSemisimple
hg : g.IsSemisimple
a : End K M
ha : Membership.mem (γ := Subalgebra K (End K M)) K[f, g] a
R : Type u_3 := HasQuotient.Quotient K[X] (B := Ideal K[X]) (Ideal.span {minpoly K f})
S : Type u_3 := AdjoinRoot (map (algebraMap K R) (minpoly K g))
⊢ Module.Finite K R

Tactic:
have : Module.Finite K R :=
    (AdjoinRoot.powerBasis' <| minpoly.monic <| IsIntegral.isIntegral f).finite
-- Module: Mathlib.LinearAlgebra.Semisimple
Goal:
M : Type u_2
inst : AddCommGroup M
K : Type u_3
inst_1 : Field K
inst_2 : Module K M
f g : End K M
inst_3 : FiniteDimensional K M
inst_4 : PerfectField K
comm : Commute f g
hf : f.IsSemisimple
hg : g.IsSemisimple
a : End K M
ha : Membership.mem (γ := Subalgebra K (End K M)) K[f, g] a
R : Type u_3 := HasQuotient.Quotient K[X] (B := Ideal K[X]) (Ideal.span {minpoly K f})
S : Type u_3 := AdjoinRoot (map (algebraMap K R) (minpoly K g))
this : Module.Finite K R
⊢ Module.Finite R S

Tactic:
have : Module.Finite R S :=
    (AdjoinRoot.powerBasis' <| (minpoly.monic <| IsIntegral.isIntegral g).map _).finite
-- Module: Mathlib.LinearAlgebra.Semisimple
Goal:
M : Type u_2
inst : AddCommGroup M
K : Type u_3
inst_1 : Field K
inst_2 : Module K M
f g : End K M
inst_3 : FiniteDimensional K M
inst_4 : PerfectField K
comm : Commute f g
hf : f.IsSemisimple
hg : g.IsSemisimple
a : End K M
ha : Membership.mem (γ := Subalgebra K (End K M)) K[f, g] a
R : Type u_3 := HasQuotient.Quotient K[X] (B := Ideal K[X]) (Ideal.span {minpoly K f})
S : Type u_3 := AdjoinRoot (map (algebraMap K R) (minpoly K g))
this_1 : Module.Finite K R
this : Module.Finite R S
⊢ Module.Finite K S

Tactic:
have : Module.Finite K S := .trans R S
-- Module: Mathlib.LinearAlgebra.Semisimple
Goal:
M : Type u_2
inst : AddCommGroup M
K : Type u_3
inst_1 : Field K
inst_2 : Module K M
f g : End K M
inst_3 : FiniteDimensional K M
inst_4 : PerfectField K
comm : Commute f g
hf : f.IsSemisimple
hg : g.IsSemisimple
a : End K M
ha : Membership.mem (γ := Subalgebra K (End K M)) K[f, g] a
R : Type u_3 := HasQuotient.Quotient K[X] (B := Ideal K[X]) (Ideal.span {minpoly K f})
S : Type u_3 := AdjoinRoot (map (algebraMap K R) (minpoly K g))
this_1 : Module.Finite K R
this_2 : Module.Finite R S
this : Module.Finite K S
⊢ IsArtinianRing R

Tactic:
have : IsArtinianRing R := .of_finite K R
-- Module: Mathlib.LinearAlgebra.Semisimple
Goal:
M : Type u_2
inst : AddCommGroup M
K : Type u_3
inst_1 : Field K
inst_2 : Module K M
f g : End K M
inst_3 : FiniteDimensional K M
inst_4 : PerfectField K
comm : Commute f g
hf : f.IsSemisimple
hg : g.IsSemisimple
a : End K M
ha : Membership.mem (γ := Subalgebra K (End K M)) K[f, g] a
R : Type u_3 := HasQuotient.Quotient K[X] (B := Ideal K[X]) (Ideal.span {minpoly K f})
S : Type u_3 := AdjoinRoot (map (algebraMap K R) (minpoly K g))
this_1 : Module.Finite K R
this_2 : Module.Finite R S
this_3 : Module.Finite K S
this : IsArtinianRing R
⊢ IsReduced R

Tactic:
have : IsReduced R := (Ideal.isRadical_iff_quotient_reduced _).mp <|
    span_minpoly_eq_annihilator K f ▸ hf.annihilator_isRadical
-- Module: Mathlib.LinearAlgebra.Semisimple
Goal:
M : Type u_2
inst : AddCommGroup M
K : Type u_3
inst_1 : Field K
inst_2 : Module K M
f g : End K M
inst_3 : FiniteDimensional K M
inst_4 : PerfectField K
comm : Commute f g
hf : f.IsSemisimple
hg : g.IsSemisimple
a : End K M
ha : Membership.mem (γ := Subalgebra K (End K M)) K[f, g] a
R : Type u_3 := HasQuotient.Quotient K[X] (B := Ideal K[X]) (Ideal.span {minpoly K f})
S : Type u_3 := AdjoinRoot (map (algebraMap K R) (minpoly K g))
this_1 : Module.Finite K R
this_2 : Module.Finite R S
this_3 : Module.Finite K S
this_4 : IsArtinianRing R
this : IsReduced R
simp_rw : IsRadical (map (algebraMap K R) (minpoly K g))
⊢ IsReduced S

Tactic:
simp_rw [S, AdjoinRoot, ← Ideal.isRadical_iff_quotient_reduced, ← isRadical_iff_span_singleton]

Premises used: AdjoinRoot, isRadical_iff_span_singleton, Ideal.isRadical_iff_quotient_reduced
-- Module: Mathlib.LinearAlgebra.Semisimple
Goal:
M : Type u_2
inst : AddCommGroup M
K : Type u_3
inst_1 : Field K
inst_2 : Module K M
f g : End K M
inst_3 : FiniteDimensional K M
inst_4 : PerfectField K
comm : Commute f g
hf : f.IsSemisimple
hg : g.IsSemisimple
a : End K M
ha : Membership.mem (γ := Subalgebra K (End K M)) K[f, g] a
R : Type u_3 := HasQuotient.Quotient K[X] (B := Ideal K[X]) (Ideal.span {minpoly K f})
S : Type u_3 := AdjoinRoot (map (algebraMap K R) (minpoly K g))
this_1 : Module.Finite K R
this_2 : Module.Finite R S
this_3 : Module.Finite K S
this_4 : IsArtinianRing R
this : IsReduced R
⊢ IsRadical (map (algebraMap K R) (minpoly K g))

Tactic:
(PerfectField.separable_iff_squarefree.mpr hg.minpoly_squarefree).map.squarefree.isRadical

Premises used: Iff.mpr, Squarefree.isRadical, Polynomial.Separable.map, PerfectField.separable_iff_squarefree, Polynomial.Separable.squarefree, Module.End.IsSemisimple.minpoly_squarefree
-- Module: Mathlib.LinearAlgebra.Semisimple
Goal:
M : Type u_2
inst : AddCommGroup M
K : Type u_3
inst_1 : Field K
inst_2 : Module K M
f g : End K M
inst_3 : FiniteDimensional K M
inst_4 : PerfectField K
comm : Commute f g
hf : f.IsSemisimple
hg : g.IsSemisimple
a : End K M
ha : Membership.mem (γ := Subalgebra K (End K M)) K[f, g] a
R : Type u_3 := HasQuotient.Quotient K[X] (B := Ideal K[X]) (Ideal.span {minpoly K f})
S : Type u_3 := AdjoinRoot (map (algebraMap K R) (minpoly K g))
this_1 : Module.Finite K R
this_2 : Module.Finite R S
this_3 : Module.Finite K S
this_4 : IsArtinianRing R
this : IsReduced R
⊢ IsRadical (map (algebraMap K R) (minpoly K g))

Tactic:
exact (PerfectField.separable_iff_squarefree.mpr hg.minpoly_squarefree).map.squarefree.isRadical

Premises used: Iff.mpr, Squarefree.isRadical, Polynomial.Separable.map, PerfectField.separable_iff_squarefree, Polynomial.Separable.squarefree, Module.End.IsSemisimple.minpoly_squarefree
-- Module: Mathlib.LinearAlgebra.Semisimple
Goal:
M : Type u_2
inst : AddCommGroup M
K : Type u_3
inst_1 : Field K
inst_2 : Module K M
f g : End K M
inst_3 : FiniteDimensional K M
inst_4 : PerfectField K
comm : Commute f g
hf : f.IsSemisimple
hg : g.IsSemisimple
a : End K M
ha : Membership.mem (γ := Subalgebra K (End K M)) K[f, g] a
R : Type u_3 := HasQuotient.Quotient K[X] (B := Ideal K[X]) (Ideal.span {minpoly K f})
S : Type u_3 := AdjoinRoot (map (algebraMap K R) (minpoly K g))
this_1 : Module.Finite K R
this_2 : Module.Finite R S
this_3 : Module.Finite K S
this_4 : IsArtinianRing R
this : IsReduced R
⊢ IsReduced S

Tactic:
have : IsReduced S := by
    simp_rw [S, AdjoinRoot, ← Ideal.isRadical_iff_quotient_reduced, ← isRadical_iff_span_singleton]
    exact (PerfectField.separable_iff_squarefree.mpr hg.minpoly_squarefree).map.squarefree.isRadical
-- Module: Mathlib.LinearAlgebra.Semisimple
Goal:
M : Type u_2
inst : AddCommGroup M
K : Type u_3
inst_1 : Field K
inst_2 : Module K M
f g : End K M
inst_3 : FiniteDimensional K M
inst_4 : PerfectField K
comm : Commute f g
hf : f.IsSemisimple
hg : g.IsSemisimple
a : End K M
ha : Membership.mem (γ := Subalgebra K (End K M)) K[f, g] a
R : Type u_3 := HasQuotient.Quotient K[X] (B := Ideal K[X]) (Ideal.span {minpoly K f})
S : Type u_3 := AdjoinRoot (map (algebraMap K R) (minpoly K g))
this_1 : Module.Finite K R
this_2 : Module.Finite R S
this_3 : Module.Finite K S
this_4 : IsArtinianRing R
this_5 : IsReduced R
this : IsReduced S
refine_4 : a.IsSemisimple
refine_1 :
  ∀ (a : K[X]),
    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)
refine_2 : ∀ (a : R), Commute ((Ideal.Quotient.liftₐ (Ideal.span {minpoly K f}) (aeval f) ⋯ : (a : R) → End K M) a) g
refine_3 :
  Membership.mem (γ := Ideal R[X])
    (RingHom.ker (F := AlgHom.{u_3, u_3, u_2} K R[X] (End K M))
      (eval₂AlgHom (Ideal.Quotient.liftₐ (Ideal.span {minpoly K f}) (aeval f) ⋯) g ⋯))
    (map (algebraMap K R) (minpoly K g))
⊢ a.IsSemisimple

Tactic:
let φ : S →ₐ[K] End K M := Ideal.Quotient.liftₐ _ (eval₂AlgHom (Ideal.Quotient.liftₐ _ (aeval f)
    fun a ↦ ?_) g ?_) ((Ideal.span_singleton_le_iff_mem _).mpr ?_ : _ ≤ RingHom.ker _)
-- Module: Mathlib.LinearAlgebra.Semisimple
Goal:
M : Type u_2
inst : AddCommGroup M
K : Type u_3
inst_1 : Field K
inst_2 : Module K M
f g : End K M
inst_3 : FiniteDimensional K M
inst_4 : PerfectField K
comm : Commute f g
hf : f.IsSemisimple
hg : g.IsSemisimple
a_1 : End K M
ha : Membership.mem (γ := Subalgebra K (End K M)) K[f, g] a_1
R : Type u_3 := HasQuotient.Quotient K[X] (B := Ideal K[X]) (Ideal.span {minpoly K f})
S : Type u_3 := AdjoinRoot (map (algebraMap K R) (minpoly K g))
this_1 : Module.Finite K R
this_2 : Module.Finite R S
this_3 : Module.Finite K S
this_4 : IsArtinianRing R
this_5 : IsReduced R
this : IsReduced S
a : K[X]
refine_1 :
  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)
⊢ 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)

Tactic:
rw [Ideal.span, ← minpoly.ker_aeval_eq_span_minpoly]

Premises used: minpoly.ker_aeval_eq_span_minpoly, Ideal.span
-- Module: Mathlib.LinearAlgebra.Semisimple
Goal:
M : Type u_2
inst : AddCommGroup M
K : Type u_3
inst_1 : Field K
inst_2 : Module K M
f g : End K M
inst_3 : FiniteDimensional K M
inst_4 : PerfectField K
comm : Commute f g
hf : f.IsSemisimple
hg : g.IsSemisimple
a_1 : End K M
ha : Membership.mem (γ := Subalgebra K (End K M)) K[f, g] a_1
R : Type u_3 := HasQuotient.Quotient K[X] (B := Ideal K[X]) (Ideal.span {minpoly K f})
S : Type u_3 := AdjoinRoot (map (algebraMap K R) (minpoly K g))
this_1 : Module.Finite K R
this_2 : Module.Finite R S
this_3 : Module.Finite K S
this_4 : IsArtinianRing R
this_5 : IsReduced R
this : IsReduced S
a : K[X]
⊢ 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:
id

Premises used: Set.Mem, setOf, id, Set.preimage, Set.singleton
-- Module: Mathlib.LinearAlgebra.Semisimple
Goal:
M : Type u_2
inst : AddCommGroup M
K : Type u_3
inst_1 : Field K
inst_2 : Module K M
f g : End K M
inst_3 : FiniteDimensional K M
inst_4 : PerfectField K
comm : Commute f g
hf : f.IsSemisimple
hg : g.IsSemisimple
a_1 : End K M
ha : Membership.mem (γ := Subalgebra K (End K M)) K[f, g] a_1
R : Type u_3 := HasQuotient.Quotient K[X] (B := Ideal K[X]) (Ideal.span {minpoly K f})
S : Type u_3 := AdjoinRoot (map (algebraMap K R) (minpoly K g))
this_1 : Module.Finite K R
this_2 : Module.Finite R S
this_3 : Module.Finite K S
this_4 : IsArtinianRing R
this_5 : IsReduced R
this : IsReduced S
a : K[X]
⊢ 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:
exact id