awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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) ⋯)
                    (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)
⊢ 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)
  ((AlgHom.comp
          (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})))
          (aeval p) :
        (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]
-- 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
inst_3 : FiniteDimensional K M
hf : f.IsSemisimple
a : End K M
ha : Membership.mem (γ := Subalgebra K (End K M)) K[f] a
⊢ a.IsSemisimple
have ha₁ : Membership.mem (γ := Subalgebra K (End K M)) (AlgHom.range (aeval f)) a
Tactic: rw [adjoin_singleton_eq_range_aeval] at ha
Cleared hypotheses: ha
-- 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
a : End K M
ha : Membership.mem (γ := Subalgebra K (End K M)) (AlgHom.range (aeval f)) a
⊢ a.IsSemisimple
have obtain : ∀ (p : K[X]), IsSemisimple.{u_3, u_2} (R := K) (M := M) ((AlgHom.toRingHom (aeval f) : (a : K[X]) → End K M) p)
Tactic: obtain ⟨p, rfl⟩ := ha
Cleared hypotheses: a, ha
-- 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 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))
⊢ a.IsSemisimple
have this : Module.Finite K R
Tactic: have : Module.Finite K R :=
    (AdjoinRoot.powerBasis' <| minpoly.monic <| IsIntegral.isIntegral f).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 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
⊢ a.IsSemisimple
have this₁ : Module.Finite R S
Tactic: have : Module.Finite R S :=
    (AdjoinRoot.powerBasis' <| (minpoly.monic <| IsIntegral.isIntegral g).map _).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 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
⊢ a.IsSemisimple
have this₁ : Module.Finite K S
Tactic: have : Module.Finite K S := .trans R S
-- 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 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
⊢ a.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 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
⊢ a.IsSemisimple
have this₁ : IsReduced R
Tactic: have : IsReduced R := (Ideal.isRadical_iff_quotient_reduced _).mp <|
    span_minpoly_eq_annihilator K f ▸ hf.annihilator_isRadical
-- 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 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
have simp_rw : IsRadical (map (algebraMap K R) (minpoly K g))
Tactic: simp_rw [S, AdjoinRoot, ← Ideal.isRadical_iff_quotient_reduced, ← isRadical_iff_span_singleton]
-- 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 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
⊢ a.IsSemisimple
have this₁ : 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
-- 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 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
⊢ a.IsSemisimple
have 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)
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 _)
-- 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 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)
⊢ a.IsSemisimple
have refine_2 : ∀ (a : R), Commute ((Ideal.Quotient.liftₐ (Ideal.span {minpoly K f}) (aeval f) sorry : (a : R) → End K M) a) g
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 _)
-- 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 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
⊢ a.IsSemisimple
have 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) sorry) g sorry))
  (map (algebraMap K R) (minpoly K g))
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 _)
-- 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 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]) (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 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)
Tactic: rw [Ideal.span, ← minpoly.ker_aeval_eq_span_minpoly]
-- 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 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
φ : AlgHom.{u_3, u_3, u_2} K S (End K M) :=
  Ideal.Quotient.liftₐ (Ideal.span {map (algebraMap K R) (minpoly K g)})
    (eval₂AlgHom (Ideal.Quotient.liftₐ (Ideal.span {minpoly K f}) (aeval f) ⋯) g ⋯) ⋯
x : End K M
hx : x = f
⊢ x ∈ (↑φ.range : Set (End K M))
have inl : f ∈ (↑φ.range : Set (End K M))
Tactic: rw [hx]
-- 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 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
φ : AlgHom.{u_3, u_3, u_2} K S (End K M) :=
  Ideal.Quotient.liftₐ (Ideal.span {map (algebraMap K R) (minpoly K g)})
    (eval₂AlgHom (Ideal.Quotient.liftₐ (Ideal.span {minpoly K f}) (aeval f) ⋯) g ⋯) ⋯
x : End K M
hx : Membership.mem (γ := Set (End K M)) {g} x
⊢ x ∈ (↑φ.range : Set (End K M))
have inr : g ∈ (↑φ.range : Set (End K M))
Tactic: rw [hx]
-- 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 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
φ : AlgHom.{u_3, u_3, u_2} K S (End K M) :=
  Ideal.Quotient.liftₐ (Ideal.span {map (algebraMap K R) (minpoly K g)})
    (eval₂AlgHom (Ideal.Quotient.liftₐ (Ideal.span {minpoly K f}) (aeval f) ⋯) g ⋯) ⋯
⊢ a.IsSemisimple
have this₁ : K[f, g] ≤ φ.range
Tactic: have : K[f, g] ≤ φ.range := adjoin_le fun x ↦ by
    rintro (hx | hx) <;> rw [hx]
    · exact ⟨AdjoinRoot.of _ (AdjoinRoot.root _), (eval₂_C _ _).trans (aeval_X f)⟩
    · exact ⟨AdjoinRoot.root _, eval₂_X _ _⟩
-- 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 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_6 : IsReduced S
φ : AlgHom.{u_3, u_3, u_2} K S (End K M) :=
  Ideal.Quotient.liftₐ (Ideal.span {map (algebraMap K R) (minpoly K g)})
    (eval₂AlgHom (Ideal.Quotient.liftₐ (Ideal.span {minpoly K f}) (aeval f) ⋯) g ⋯) ⋯
this : K[f, g] ≤ φ.range
⊢ a.IsSemisimple
have refine_4 : ∀ (p : S)
  (ha : Membership.mem (α := End K M) (γ := Subalgebra K (End K M)) K[f, g] ((φ : (a : S) → End K M) p : End K M)),
  IsSemisimple.{u_3, u_2} (R := K) (M := M) ((φ : (a : S) → End K M) p)
Tactic: obtain ⟨p, rfl⟩ := (AlgHom.mem_range _).mp (this ha)
Cleared hypotheses: a, ha
-- 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 g : End K M
inst_3 : FiniteDimensional K M
inst_4 : PerfectField K
comm : Commute f g
hf : f.IsSemisimple
hg : g.IsSemisimple
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_6 : IsReduced S
φ : AlgHom.{u_3, u_3, u_2} K S (End K M) :=
  Ideal.Quotient.liftₐ (Ideal.span {map (algebraMap K R) (minpoly K g)})
    (eval₂AlgHom (Ideal.Quotient.liftₐ (Ideal.span {minpoly K f}) (aeval f) ⋯) g ⋯) ⋯
this : K[f, g] ≤ φ.range
p : S
ha : Membership.mem (α := End K M) (γ := Subalgebra K (End K M)) K[f, g] ((φ : (a : S) → End K M) p : End K M)
⊢ IsSemisimple.{u_3, u_2} (R := K) (M := M) ((φ : (a : S) → End K M) p)
have refine_4 : Eq.{u_2 + 1} (α := End K M)
  (((aeval ((φ : (a : S) → 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 p) :
    End K M)
  (0 : End K M)
Tactic: refine isSemisimple_of_squarefree_aeval_eq_zero
    ((minpoly.isRadical K p).squarefree <| minpoly.ne_zero <| .of_finite K p) ?_
-- 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 g : End K M
inst_3 : FiniteDimensional K M
inst_4 : PerfectField K
comm : Commute f g
hf : f.IsSemisimple
hg : g.IsSemisimple
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_6 : IsReduced S
φ : AlgHom.{u_3, u_3, u_2} K S (End K M) :=
  Ideal.Quotient.liftₐ (Ideal.span {map (algebraMap K R) (minpoly K g)})
    (eval₂AlgHom (Ideal.Quotient.liftₐ (Ideal.span {minpoly K f}) (aeval f) ⋯) g ⋯) ⋯
this : K[f, g] ≤ φ.range
p : S
ha : Membership.mem (α := End K M) (γ := Subalgebra K (End K M)) K[f, g] ((φ : (a : S) → End K M) p : End K M)
⊢ Eq.{u_2 + 1} (α := End K M)
    (((aeval ((φ : (a : S) → 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 p) :
      End K M)
    (0 : End K M)
have refine_4 : Eq.{u_2 + 1} (α := End K M) ((φ.comp (aeval p) : (a : K[X]) → End K M) (minpoly K p) : End K M) (0 : End K M)
Tactic: rw [aeval_algHom, φ.comp_apply, minpoly.aeval, map_zero]
-- 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 g : End K M
inst_3 : FiniteDimensional K M
inst_4 : PerfectField K
comm : Commute f g
hf : f.IsSemisimple
hg : g.IsSemisimple
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_6 : IsReduced S
φ : AlgHom.{u_3, u_3, u_2} K S (End K M) :=
  Ideal.Quotient.liftₐ (Ideal.span {map (algebraMap K R) (minpoly K g)})
    (eval₂AlgHom (Ideal.Quotient.liftₐ (Ideal.span {minpoly K f}) (aeval f) ⋯) g ⋯) ⋯
this : K[f, g] ≤ φ.range
p : S
ha : Membership.mem (α := End K M) (γ := Subalgebra K (End K M)) K[f, g] ((φ : (a : S) → End K M) p : End K M)
refine_4 : Eq.{u_2 + 1} (α := End K M) ((φ.comp (aeval p) : (a : K[X]) → End K M) (minpoly K p) : End K M) (0 : End K M)
⊢ Eq.{u_2 + 1} (α := End K M)
    (((aeval ((φ : (a : S) → 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 p) :
      End K M)
    (0 : End K M)
have refine_4₁ : Eq.{u_2 + 1} (α := End K M) ((φ : (a : S) → End K M) ((aeval p : (a : K[X]) → S) (minpoly K p)) : End K M) (0 : End K M)
Tactic: rw [aeval_algHom, φ.comp_apply, minpoly.aeval, map_zero]
-- 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 g : End K M
inst_3 : FiniteDimensional K M
inst_4 : PerfectField K
comm : Commute f g
hf : f.IsSemisimple
hg : g.IsSemisimple
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_6 : IsReduced S
φ : AlgHom.{u_3, u_3, u_2} K S (End K M) :=
  Ideal.Quotient.liftₐ (Ideal.span {map (algebraMap K R) (minpoly K g)})
    (eval₂AlgHom (Ideal.Quotient.liftₐ (Ideal.span {minpoly K f}) (aeval f) ⋯) g ⋯) ⋯
this : K[f, g] ≤ φ.range
p : S
ha : Membership.mem (α := End K M) (γ := Subalgebra K (End K M)) K[f, g] ((φ : (a : S) → End K M) p : End K M)
refine_4 : Eq.{u_2 + 1} (α := End K M) ((φ.comp (aeval p) : (a : K[X]) → End K M) (minpoly K p) : End K M) (0 : End K M)
refine_4₁ :
  Eq.{u_2 + 1} (α := End K M) ((φ : (a : S) → End K M) ((aeval p : (a : K[X]) → S) (minpoly K p)) : End K M)
    (0 : End K M)
⊢ Eq.{u_2 + 1} (α := End K M)
    (((aeval ((φ : (a : S) → 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 p) :
      End K M)
    (0 : End K M)
have refine_4₂ : Eq.{u_2 + 1} (α := End K M) ((φ : (a : S) → End K M) 0) 0
Tactic: rw [aeval_algHom, φ.comp_apply, minpoly.aeval, map_zero]