awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
a_1 : R
p : K[X]
k : K
⊢ Commute
    ((Ideal.Quotient.liftₐ (Ideal.span {minpoly K f}) (aeval f) ⋯ : (a : R) → End K M)
      (Quot.mk (⇑(Submodule.quotientRel (Ideal.span {minpoly K f})) : K[X] → K[X] → Prop) ((C : (a : K) → K[X]) k)))
    g

Tactic:
simp [R, commute_algebraMap_left]

Premises used: Algebra.commute_algebraMap_left
-- 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
a_1 : R
p_1 p q : K[X]
hp :
  Commute
    ((Ideal.Quotient.liftₐ (Ideal.span {minpoly K f}) (aeval f) ⋯ : (a : R) → End K M)
      (Quot.mk (⇑(Submodule.quotientRel (Ideal.span {minpoly K f})) : K[X] → K[X] → Prop) p))
    g
hq :
  Commute
    ((Ideal.Quotient.liftₐ (Ideal.span {minpoly K f}) (aeval f) ⋯ : (a : R) → End K M)
      (Quot.mk (⇑(Submodule.quotientRel (Ideal.span {minpoly K f})) : K[X] → K[X] → Prop) q))
    g
⊢ Commute
    ((Ideal.Quotient.liftₐ (Ideal.span {minpoly K f}) (aeval f) ⋯ : (a : R) → End K M)
      (Quot.mk (⇑(Submodule.quotientRel (Ideal.span {minpoly K f})) : K[X] → K[X] → Prop) (p + q)))
    g

Tactic:
simpa [R] using hp.add_left hq

Premises used: Commute.add_left
-- 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
a_1 : R
p : K[X]
n : ℕ
k : K
⊢ Commute
      ((Ideal.Quotient.liftₐ (Ideal.span {minpoly K f}) (aeval f) ⋯ : (a : R) → End K M)
        (Quot.mk (⇑(Submodule.quotientRel (Ideal.span {minpoly K f})) : K[X] → K[X] → Prop)
          (HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) k : K[X]) (HPow.hPow (α := K[X]) X n))))
      g →
    Commute
      ((Ideal.Quotient.liftₐ (Ideal.span {minpoly K f}) (aeval f) ⋯ : (a : R) → End K M)
        (Quot.mk (⇑(Submodule.quotientRel (Ideal.span {minpoly K f})) : K[X] → K[X] → Prop)
          (HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) k : K[X]) (HPow.hPow (α := K[X]) X (n + 1)))))
      g

Tactic:
simpa [R, pow_succ, ← mul_assoc _ _ X] using (·.mul_left comm)

Premises used: pow_succ, mul_assoc, Polynomial.X
-- 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
a_1 : R
p : K[X]
⊢ Commute
    ((Ideal.Quotient.liftₐ (Ideal.span {minpoly K f}) (aeval f) ⋯ : (a : R) → End K M)
      (Quot.mk (⇑(Submodule.quotientRel (Ideal.span {minpoly K f})) : K[X] → K[X] → Prop) p))
    g

Tactic:
exact p.induction_on (fun k ↦ by simp [R, commute_algebraMap_left])
      (fun p q hp hq ↦ by simpa [R] using hp.add_left hq)
      fun n k ↦ by simpa [R, pow_succ, ← mul_assoc _ _ X] using (·.mul_left comm)
-- 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
⊢ 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))

Tactic:
simpa only [RingHom.mem_ker, eval₂AlgHom_apply, eval₂_map, AlgHom.comp_algebraMap_of_tower]
      using minpoly.aeval K g

Premises used: RingHom.mem_ker, Polynomial.eval₂AlgHom_apply, AlgHom.comp_algebraMap_of_tower, Polynomial.eval₂_map, minpoly.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 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
inl : f ∈ (↑φ.range : Set (End K M))
⊢ x ∈ (↑φ.range : Set (End K M))

Tactic:
rw [hx]
-- 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
φ : 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
inr : g ∈ (↑φ.range : Set (End K M))
⊢ x ∈ (↑φ.range : Set (End K M))

Tactic:
rw [hx]
-- 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
φ : 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
⊢ f ∈ (↑φ.range : Set (End K M))

Tactic:
⟨AdjoinRoot.of _ (AdjoinRoot.root _), (eval₂_C _ _).trans (aeval_X f)⟩

Premises used: Set.Mem, setOf, AdjoinRoot.root, Exists.intro, Polynomial.eval₂_C, Set.range, AdjoinRoot.of, DFunLike.coe, Polynomial.aeval_X, Eq.trans
-- 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
φ : 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
⊢ f ∈ (↑φ.range : Set (End K M))

Tactic:
exact ⟨AdjoinRoot.of _ (AdjoinRoot.root _), (eval₂_C _ _).trans (aeval_X f)⟩
-- 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
φ : 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
⊢ g ∈ (↑φ.range : Set (End K M))

Tactic:
⟨AdjoinRoot.root _, eval₂_X _ _⟩

Premises used: Set.Mem, setOf, Polynomial.eval₂_X, AdjoinRoot.root, Exists.intro, Set.range
-- 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
φ : 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
⊢ g ∈ (↑φ.range : Set (End K M))

Tactic:
exact ⟨AdjoinRoot.root _, eval₂_X _ _⟩
-- 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
φ : 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 ⋯) ⋯
⊢ 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 _ _⟩
-- 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_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
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)
⊢ a.IsSemisimple

Tactic:
obtain ⟨p, rfl⟩ := (AlgHom.mem_range _).mp (this ha)

Premises used: AlgHom.mem_range, Iff.mp, 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 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)

Tactic:
isSemisimple_of_squarefree_aeval_eq_zero
    ((minpoly.isRadical K p).squarefree <| minpoly.ne_zero <| .of_finite K p) ?_

Premises used: minpoly.isRadical, IsRadical.squarefree, Module.End.isSemisimple_of_squarefree_aeval_eq_zero, IsIntegral.of_finite, minpoly.ne_zero
-- 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
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)
    (((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)
⊢ IsSemisimple.{u_3, u_2} (R := K) (M := M) ((φ : (a : S) → End K M) p)

Tactic:
refine isSemisimple_of_squarefree_aeval_eq_zero
    ((minpoly.isRadical K p).squarefree <| minpoly.ne_zero <| .of_finite K p) ?_

Premises used: minpoly.isRadical, IsRadical.squarefree, Module.End.isSemisimple_of_squarefree_aeval_eq_zero, IsIntegral.of_finite, minpoly.ne_zero
-- 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
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)
refine_4₂ : Eq.{u_2 + 1} (α := End K M) ((φ : (a : S) → End K M) 0) 0
refine_4₃ refine_4₄ : Eq.{u_2 + 1} (α := End K M) 0 0
⊢ 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:
rw [aeval_algHom, φ.comp_apply, minpoly.aeval, map_zero]

Premises used: AlgHom.comp_apply, map_zero, minpoly.aeval, Polynomial.aeval_algHom
-- 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
⊢ (f + g).IsSemisimple

Tactic:
.of_mem_adjoin_pair
  comm hf hg <| add_mem (Algebra.subset_adjoin <| .inl rfl) (Algebra.subset_adjoin <| .inr rfl)

Premises used: Algebra.subset_adjoin, Module.End.IsSemisimple.of_mem_adjoin_pair, AddMemClass.add_mem, Or.inl, Or.inr, 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 g : End K M
inst_3 : FiniteDimensional K M
inst_4 : PerfectField K
comm : Commute f g
hf : f.IsSemisimple
hg : g.IsSemisimple
⊢ (f - g).IsSemisimple

Tactic:
.of_mem_adjoin_pair
  comm hf hg <| sub_mem (subset_adjoin <| .inl rfl) (subset_adjoin <| .inr rfl)

Premises used: Algebra.subset_adjoin, sub_mem, Module.End.IsSemisimple.of_mem_adjoin_pair, Or.inl, Or.inr, 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 g : End K M
inst_3 : FiniteDimensional K M
inst_4 : PerfectField K
comm : Commute f g
hf : f.IsSemisimple
hg : g.IsSemisimple
⊢ (f * g).IsSemisimple

Tactic:
.of_mem_adjoin_pair
  comm hf hg <| mul_mem (subset_adjoin <| .inl rfl) (subset_adjoin <| .inr rfl)

Premises used: Algebra.subset_adjoin, Module.End.IsSemisimple.of_mem_adjoin_pair, Or.inl, Or.inr, rfl, MulMemClass.mul_mem
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
inst : CommSemiring R
inst_1 : CommSemiring R₁
inst_2 : AddCommMonoid M₁
inst_3 : Module R₁ M₁
inst_4 : CommSemiring R₂
inst_5 : AddCommMonoid M₂
inst_6 : Module R₂ M₂
inst_7 : AddCommMonoid M
inst_8 : Module R M
I₁ : R₁ →+* R
I₂ : R₂ →+* R
B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] M
x : M₁
y : M₂
⊢ B.IsOrtho x y ↔
    Eq.{u_5 + 1} (α := M) ((((B : (a : M₁) → M₂ →ₛₗ[I₂] M) x : M₂ →ₛₗ[I₂] M) : (a : M₂) → M) y : M) (0 : M)

Tactic:
Iff.rfl

Premises used: Iff.rfl, LinearMap.IsOrtho
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
inst : CommSemiring R
inst_1 : CommSemiring R₁
inst_2 : AddCommMonoid M₁
inst_3 : Module R₁ M₁
inst_4 : CommSemiring R₂
inst_5 : AddCommMonoid M₂
inst_6 : Module R₂ M₂
inst_7 : AddCommMonoid M
inst_8 : Module R M
I₁ : R₁ →+* R
I₂ : R₂ →+* R
B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] M
x : M₂
rw : Eq.{u_5 + 1} (α := M) ((0 : (a : M₂) → M) x : M) (0 : M)
rw₁ rw₂ : Eq.{u_5 + 1} (α := M) 0 0
⊢ Eq.{u_5 + 1} (α := M) (((B : (a : M₁) → M₂ →ₛₗ[I₂] M) 0 : (a : M₂) → M) x : M) (0 : M)

Tactic:
rw [map_zero B, zero_apply]

Premises used: LinearMap.zero_apply, map_zero
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
inst : CommSemiring R
inst_1 : CommSemiring R₁
inst_2 : AddCommMonoid M₁
inst_3 : Module R₁ M₁
inst_4 : CommSemiring R₂
inst_5 : AddCommMonoid M₂
inst_6 : Module R₂ M₂
inst_7 : AddCommMonoid M
inst_8 : Module R M
I₁ : R₁ →+* R
I₂ : R₂ →+* R
B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] M
x : M₁
⊢ B.IsOrtho x 0

Tactic:
map_zero (B x)

Premises used: map_zero, LinearMap.IsOrtho, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
R : Type u_1
R₁ : Type u_2
M : Type u_5
M₁ : Type u_6
inst : CommSemiring R
inst_1 : CommSemiring R₁
inst_2 : AddCommMonoid M₁
inst_3 : Module R₁ M₁
inst_4 : AddCommMonoid M
inst_5 : Module R M
I₁ I₁' : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₁'] M
x y : M₁
simp_rw :
  Eq.{u_5 + 1} (α := M) ((((B : (a : M₁) → M₁ →ₛₗ[I₁'] M) x : M₁ →ₛₗ[I₁'] M) : (a : M₁) → M) y : M) (0 : M) ↔
    Eq.{u_5 + 1} (α := M) ((((B.flip : (a : M₁) → M₁ →ₛₗ[I₁] M) y : M₁ →ₛₗ[I₁] M) : (a : M₁) → M) x : M) (0 : M)
⊢ B.IsOrtho x y ↔ B.flip.IsOrtho y x

Tactic:
simp_rw [isOrtho_def, flip_apply]

Premises used: LinearMap.flip_apply, LinearMap.isOrtho_def
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
R : Type u_1
R₁ : Type u_2
M : Type u_5
M₁ : Type u_6
n : Type u_19
inst : CommSemiring R
inst_1 : CommSemiring R₁
inst_2 : AddCommMonoid M₁
inst_3 : Module R₁ M₁
inst_4 : AddCommMonoid M
inst_5 : Module R M
I₁ I₁' : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₁'] M
v : n → M₁
⊢ B.IsOrthoᵢ v ↔
    ∀ (i j : n),
      i ≠ j →
        Eq.{u_5 + 1} (α := M) ((((B : (a : M₁) → M₁ →ₛₗ[I₁'] M) (v i) : M₁ →ₛₗ[I₁'] M) : (a : M₁) → M) (v j) : M)
          (0 : M)

Tactic:
Iff.rfl

Premises used: Iff.rfl, LinearMap.IsOrtho, Pairwise, LinearMap.IsOrthoᵢ
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
R : Type u_1
R₁ : Type u_2
M : Type u_5
M₁ : Type u_6
n : Type u_19
inst : CommSemiring R
inst_1 : CommSemiring R₁
inst_2 : AddCommMonoid M₁
inst_3 : Module R₁ M₁
inst_4 : AddCommMonoid M
inst_5 : Module R M
I₁ I₁' : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₁'] M
v : n → M₁
simp_rw :
  (∀ (i j : n),
      i ≠ j →
        Eq.{u_5 + 1} (α := M) ((((B : (a : M₁) → M₁ →ₛₗ[I₁'] M) (v i) : M₁ →ₛₗ[I₁'] M) : (a : M₁) → M) (v j) : M)
          (0 : M)) ↔
    ∀ (i j : n),
      i ≠ j →
        Eq.{u_5 + 1} (α := M) ((((B.flip : (a : M₁) → M₁ →ₛₗ[I₁] M) (v i) : M₁ →ₛₗ[I₁] M) : (a : M₁) → M) (v j) : M)
          (0 : M)
⊢ B.IsOrthoᵢ v ↔ B.flip.IsOrthoᵢ v

Tactic:
simp_rw [isOrthoᵢ_def]

Premises used: LinearMap.isOrthoᵢ_def