awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.JordanChevalley
Goal:
K : Type u_1
V : Type u_2
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
f : End K V
P : K[X]
k : ℕ
sep : P.Separable
nil : minpoly K f ∣ P ^ k
ff : ↥K[f] := Subtype.mk (p := fun (x : End K V) ↦ Membership.mem (γ := Subalgebra K (End K V)) K[f] x) f ⋯
P' : K[X] := (derivative : (a : K[X]) → K[X]) P
nil' : IsNilpotent.{u_2} (R := ↥K[f]) ((aeval ff : (a : K[X]) → ↥K[f]) P : ↥K[f])
a b : K[X]
h : a * P ^ k + b * P' = 1
⊢ HMul.hMul (α := End K V) (β := End K V) ((aeval f : (a : K[X]) → End K V) b : End K V)
      ((aeval f : (a : K[X]) → End K V) P' : End K V) =
    1

Tactic:
simpa only [map_add, map_mul, map_one, minpoly.dvd_iff.mp nil, mul_zero, zero_add]
        using (aeval f).congr_arg h

Premises used: minpoly.dvd_iff, map_add, zero_add, MulZeroClass.mul_zero, map_mul, AlgHom.congr_arg, map_one, Iff.mp, Polynomial.aeval
-- Module: Mathlib.LinearAlgebra.JordanChevalley
Goal:
K : Type u_1
V : Type u_2
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
f : End K V
P : K[X]
k : ℕ
sep : P.Separable
nil : minpoly K f ∣ P ^ k
ff : ↥K[f] := Subtype.mk (p := fun (x : End K V) ↦ Membership.mem (γ := Subalgebra K (End K V)) K[f] x) f ⋯
P' : K[X] := (derivative : (a : K[X]) → K[X]) P
nil' : IsNilpotent.{u_2} (R := ↥K[f]) ((aeval ff : (a : K[X]) → ↥K[f]) P : ↥K[f])
a b : K[X]
h : a * P ^ k + b * P' = 1
⊢ HMul.hMul (α := End K V) (β := End K V) ((aeval f : (a : K[X]) → End K V) b : End K V)
      ((aeval f : (a : K[X]) → End K V) P' : End K V) =
    1

Tactic:
replace h : (aeval f b) * (aeval f P') = 1 := by
      simpa only [map_add, map_mul, map_one, minpoly.dvd_iff.mp nil, mul_zero, zero_add]
        using (aeval f).congr_arg h
-- Module: Mathlib.LinearAlgebra.JordanChevalley
Goal:
K : Type u_1
V : Type u_2
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
f : End K V
P : K[X]
k : ℕ
sep : P.Separable
nil : minpoly K f ∣ P ^ k
ff : ↥K[f] := Subtype.mk (p := fun (x : End K V) ↦ Membership.mem (γ := Subalgebra K (End K V)) K[f] x) f ⋯
P' : K[X] := (derivative : (a : K[X]) → K[X]) P
nil' : IsNilpotent.{u_2} (R := ↥K[f]) ((aeval ff : (a : K[X]) → ↥K[f]) P : ↥K[f])
a b : K[X]
h :
  HMul.hMul (α := End K V) (β := End K V) ((aeval f : (a : K[X]) → End K V) b : End K V)
      ((aeval f : (a : K[X]) → End K V) P' : End K V) =
    1
⊢ IsUnit.{u_2} (M := ↥K[f]) ((aeval ff : (a : K[X]) → ↥K[f]) P' : ↥K[f])

Tactic:
.of_mul_eq_one_right (aeval ff b) (Subtype.ext_iff.mpr ?_)

Premises used: Iff.mpr, IsUnit.of_mul_eq_one_right, Subtype.ext_iff, Polynomial.aeval, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.JordanChevalley
Goal:
K : Type u_1
V : Type u_2
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
f : End K V
P : K[X]
k : ℕ
sep : P.Separable
nil : minpoly K f ∣ P ^ k
ff : ↥K[f] := Subtype.mk (p := fun (x : End K V) ↦ Membership.mem (γ := Subalgebra K (End K V)) K[f] x) f ⋯
P' : K[X] := (derivative : (a : K[X]) → K[X]) P
nil' : IsNilpotent.{u_2} (R := ↥K[f]) ((aeval ff : (a : K[X]) → ↥K[f]) P : ↥K[f])
a b : K[X]
h :
  HMul.hMul (α := End K V) (β := End K V) ((aeval f : (a : K[X]) → End K V) b : End K V)
      ((aeval f : (a : K[X]) → End K V) P' : End K V) =
    1
refine :
  (↑(HMul.hMul (α := ↥K[f]) (β := ↥K[f]) ((aeval ff : (a : K[X]) → ↥K[f]) b : ↥K[f])
          ((aeval ff : (a : K[X]) → ↥K[f]) P' : ↥K[f])) :
      End K V) =
    (↑1 : End K V)
⊢ IsUnit.{u_2} (M := ↥K[f]) ((aeval ff : (a : K[X]) → ↥K[f]) P' : ↥K[f])

Tactic:
refine .of_mul_eq_one_right (aeval ff b) (Subtype.ext_iff.mpr ?_)
-- Module: Mathlib.LinearAlgebra.JordanChevalley
Goal:
K : Type u_1
V : Type u_2
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
f : End K V
P : K[X]
k : ℕ
sep : P.Separable
nil : minpoly K f ∣ P ^ k
ff : ↥K[f] := Subtype.mk (p := fun (x : End K V) ↦ Membership.mem (γ := Subalgebra K (End K V)) K[f] x) f ⋯
P' : K[X] := (derivative : (a : K[X]) → K[X]) P
nil' : IsNilpotent.{u_2} (R := ↥K[f]) ((aeval ff : (a : K[X]) → ↥K[f]) P : ↥K[f])
a b : K[X]
h :
  HMul.hMul (α := End K V) (β := End K V) ((aeval f : (a : K[X]) → End K V) b : End K V)
      ((aeval f : (a : K[X]) → End K V) P' : End K V) =
    1
⊢ (↑(HMul.hMul (α := ↥K[f]) (β := ↥K[f]) ((aeval ff : (a : K[X]) → ↥K[f]) b : ↥K[f])
          ((aeval ff : (a : K[X]) → ↥K[f]) P' : ↥K[f])) :
      End K V) =
    (↑1 : End K V)

Tactic:
simpa [ff, coe_aeval_mk_apply] using h

Premises used: Polynomial.coe_aeval_mk_apply
-- Module: Mathlib.LinearAlgebra.JordanChevalley
Goal:
K : Type u_1
V : Type u_2
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
f : End K V
P : K[X]
k : ℕ
sep : P.Separable
nil : minpoly K f ∣ P ^ k
ff : ↥K[f] := Subtype.mk (p := fun (x : End K V) ↦ Membership.mem (γ := Subalgebra K (End K V)) K[f] x) f ⋯
P' : K[X] := (derivative : (a : K[X]) → K[X]) P
nil' : IsNilpotent.{u_2} (R := ↥K[f]) ((aeval ff : (a : K[X]) → ↥K[f]) P : ↥K[f])
⊢ IsUnit.{u_2} (M := ↥K[f]) ((aeval ff : (a : K[X]) → ↥K[f]) P' : ↥K[f])

Tactic:
have sep' : IsUnit (aeval ff P') := by
    obtain ⟨a, b, h⟩ : IsCoprime (P ^ k) P' := sep.pow_left
    replace h : (aeval f b) * (aeval f P') = 1 := by
      simpa only [map_add, map_mul, map_one, minpoly.dvd_iff.mp nil, mul_zero, zero_add]
        using (aeval f).congr_arg h
    refine .of_mul_eq_one_right (aeval ff b) (Subtype.ext_iff.mpr ?_)
    simpa [ff, coe_aeval_mk_apply] using h
-- Module: Mathlib.LinearAlgebra.JordanChevalley
Goal:
K : Type u_1
V : Type u_2
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
f : End K V
P : K[X]
k : ℕ
sep : P.Separable
nil : minpoly K f ∣ P ^ k
ff : ↥K[f] := Subtype.mk (p := fun (x : End K V) ↦ Membership.mem (γ := Subalgebra K (End K V)) K[f] x) f ⋯
P' : K[X] := (derivative : (a : K[X]) → K[X]) P
nil' : IsNilpotent.{u_2} (R := ↥K[f]) ((aeval ff : (a : K[X]) → ↥K[f]) P : ↥K[f])
sep' : IsUnit.{u_2} (M := ↥K[f]) ((aeval ff : (a : K[X]) → ↥K[f]) P' : ↥K[f])
obtain :
  ∀ (s : End K V) (mem : Membership.mem (γ := Subalgebra K (End K V)) K[f] s)
    (hss :
      Eq.{u_2 + 1} (α := ↥K[f])
        ((aeval (Subtype.mk (p := fun (x : End K V) ↦ Membership.mem (γ := Subalgebra K (End K V)) K[f] x) s mem) :
              (a : K[X]) → ↥K[f])
            P :
          ↥K[f])
        (0 : ↥K[f]))
    (k : ℕ)
    (hk :
      (ff - Subtype.mk (p := fun (x : End K V) ↦ Membership.mem (γ := Subalgebra K (End K V)) K[f] x) s mem) ^ k = 0),
    ∃ (n : End K V),
      Membership.mem (γ := Subalgebra K (End K V)) K[f] n ∧
        ∃ (s : End K V),
          Membership.mem (γ := Subalgebra K (End K V)) K[f] s ∧ IsNilpotent n ∧ s.IsSemisimple ∧ f = n + s
⊢ ∃ (n : End K V),
    Membership.mem (γ := Subalgebra K (End K V)) K[f] n ∧
      ∃ (s : End K V), Membership.mem (γ := Subalgebra K (End K V)) K[f] s ∧ IsNilpotent n ∧ s.IsSemisimple ∧ f = n + s

Tactic:
obtain ⟨⟨s, mem⟩, ⟨⟨k, hk⟩, hss⟩, -⟩ := existsUnique_nilpotent_sub_and_aeval_eq_zero nil' sep'

Premises used: Polynomial.existsUnique_nilpotent_sub_and_aeval_eq_zero
-- Module: Mathlib.LinearAlgebra.JordanChevalley
Goal:
K : Type u_1
V : Type u_2
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
f : End K V
P : K[X]
k_1 : ℕ
sep : P.Separable
nil : minpoly K f ∣ P ^ k_1
ff : ↥K[f] := Subtype.mk (p := fun (x : End K V) ↦ Membership.mem (γ := Subalgebra K (End K V)) K[f] x) f ⋯
P' : K[X] := (derivative : (a : K[X]) → K[X]) P
nil' : IsNilpotent.{u_2} (R := ↥K[f]) ((aeval ff : (a : K[X]) → ↥K[f]) P : ↥K[f])
sep' : IsUnit.{u_2} (M := ↥K[f]) ((aeval ff : (a : K[X]) → ↥K[f]) P' : ↥K[f])
s : End K V
mem : Membership.mem (γ := Subalgebra K (End K V)) K[f] s
hss :
  Eq.{u_2 + 1} (α := ↥K[f])
    ((aeval (Subtype.mk (p := fun (x : End K V) ↦ Membership.mem (γ := Subalgebra K (End K V)) K[f] x) s mem) :
          (a : K[X]) → ↥K[f])
        P :
      ↥K[f])
    (0 : ↥K[f])
k : ℕ
hk : (ff - Subtype.mk (p := fun (x : End K V) ↦ Membership.mem (γ := Subalgebra K (End K V)) K[f] x) s mem) ^ k = 0
⊢ ∃ (n : End K V),
    Membership.mem (γ := Subalgebra K (End K V)) K[f] n ∧
      ∃ (s : End K V), Membership.mem (γ := Subalgebra K (End K V)) K[f] s ∧ IsNilpotent n ∧ s.IsSemisimple ∧ f = n + s

Tactic:
⟨f - s, ?_, s, mem, ⟨k, ?_⟩, ?_, (sub_add_cancel f s).symm⟩

Premises used: HSub.hSub, And.intro, Exists.intro, Eq.symm, sub_add_cancel
-- Module: Mathlib.LinearAlgebra.JordanChevalley
Goal:
K : Type u_1
V : Type u_2
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
f : End K V
P : K[X]
k_1 : ℕ
sep : P.Separable
nil : minpoly K f ∣ P ^ k_1
ff : ↥K[f] := Subtype.mk (p := fun (x : End K V) ↦ Membership.mem (γ := Subalgebra K (End K V)) K[f] x) f ⋯
P' : K[X] := (derivative : (a : K[X]) → K[X]) P
nil' : IsNilpotent.{u_2} (R := ↥K[f]) ((aeval ff : (a : K[X]) → ↥K[f]) P : ↥K[f])
sep' : IsUnit.{u_2} (M := ↥K[f]) ((aeval ff : (a : K[X]) → ↥K[f]) P' : ↥K[f])
s : End K V
mem : Membership.mem (γ := Subalgebra K (End K V)) K[f] s
hss :
  Eq.{u_2 + 1} (α := ↥K[f])
    ((aeval (Subtype.mk (p := fun (x : End K V) ↦ Membership.mem (γ := Subalgebra K (End K V)) K[f] x) s mem) :
          (a : K[X]) → ↥K[f])
        P :
      ↥K[f])
    (0 : ↥K[f])
k : ℕ
hk : (ff - Subtype.mk (p := fun (x : End K V) ↦ Membership.mem (γ := Subalgebra K (End K V)) K[f] x) s mem) ^ k = 0
refine_1 : Membership.mem (γ := Subalgebra K (End K V)) K[f] (f - s)
refine_2 : (f - s) ^ k = 0
refine_3 : s.IsSemisimple
⊢ ∃ (n : End K V),
    Membership.mem (γ := Subalgebra K (End K V)) K[f] n ∧
      ∃ (s : End K V), Membership.mem (γ := Subalgebra K (End K V)) K[f] s ∧ IsNilpotent n ∧ s.IsSemisimple ∧ f = n + s

Tactic:
refine ⟨f - s, ?_, s, mem, ⟨k, ?_⟩, ?_, (sub_add_cancel f s).symm⟩
-- Module: Mathlib.LinearAlgebra.JordanChevalley
Goal:
K : Type u_1
V : Type u_2
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
f : End K V
P : K[X]
k_1 : ℕ
sep : P.Separable
nil : minpoly K f ∣ P ^ k_1
ff : ↥K[f] := Subtype.mk (p := fun (x : End K V) ↦ Membership.mem (γ := Subalgebra K (End K V)) K[f] x) f ⋯
P' : K[X] := (derivative : (a : K[X]) → K[X]) P
nil' : IsNilpotent.{u_2} (R := ↥K[f]) ((aeval ff : (a : K[X]) → ↥K[f]) P : ↥K[f])
sep' : IsUnit.{u_2} (M := ↥K[f]) ((aeval ff : (a : K[X]) → ↥K[f]) P' : ↥K[f])
s : End K V
mem : Membership.mem (γ := Subalgebra K (End K V)) K[f] s
hss :
  Eq.{u_2 + 1} (α := ↥K[f])
    ((aeval (Subtype.mk (p := fun (x : End K V) ↦ Membership.mem (γ := Subalgebra K (End K V)) K[f] x) s mem) :
          (a : K[X]) → ↥K[f])
        P :
      ↥K[f])
    (0 : ↥K[f])
k : ℕ
hk : (ff - Subtype.mk (p := fun (x : End K V) ↦ Membership.mem (γ := Subalgebra K (End K V)) K[f] x) s mem) ^ k = 0
⊢ Membership.mem (γ := Subalgebra K (End K V)) K[f] (f - s)

Tactic:
sub_mem (self_mem_adjoin_singleton K f) mem

Premises used: Set.Mem, sub_mem, Algebra.self_mem_adjoin_singleton
-- Module: Mathlib.LinearAlgebra.JordanChevalley
Goal:
K : Type u_1
V : Type u_2
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
f : End K V
P : K[X]
k_1 : ℕ
sep : P.Separable
nil : minpoly K f ∣ P ^ k_1
ff : ↥K[f] := Subtype.mk (p := fun (x : End K V) ↦ Membership.mem (γ := Subalgebra K (End K V)) K[f] x) f ⋯
P' : K[X] := (derivative : (a : K[X]) → K[X]) P
nil' : IsNilpotent.{u_2} (R := ↥K[f]) ((aeval ff : (a : K[X]) → ↥K[f]) P : ↥K[f])
sep' : IsUnit.{u_2} (M := ↥K[f]) ((aeval ff : (a : K[X]) → ↥K[f]) P' : ↥K[f])
s : End K V
mem : Membership.mem (γ := Subalgebra K (End K V)) K[f] s
hss :
  Eq.{u_2 + 1} (α := ↥K[f])
    ((aeval (Subtype.mk (p := fun (x : End K V) ↦ Membership.mem (γ := Subalgebra K (End K V)) K[f] x) s mem) :
          (a : K[X]) → ↥K[f])
        P :
      ↥K[f])
    (0 : ↥K[f])
k : ℕ
hk : (ff - Subtype.mk (p := fun (x : End K V) ↦ Membership.mem (γ := Subalgebra K (End K V)) K[f] x) s mem) ^ k = 0
⊢ Membership.mem (γ := Subalgebra K (End K V)) K[f] (f - s)

Tactic:
exact sub_mem (self_mem_adjoin_singleton K f) mem

Premises used: sub_mem, Algebra.self_mem_adjoin_singleton
-- Module: Mathlib.LinearAlgebra.JordanChevalley
Goal:
K : Type u_1
V : Type u_2
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
f : End K V
P : K[X]
k_1 : ℕ
sep : P.Separable
nil : minpoly K f ∣ P ^ k_1
ff : ↥K[f] := Subtype.mk (p := fun (x : End K V) ↦ Membership.mem (γ := Subalgebra K (End K V)) K[f] x) f ⋯
P' : K[X] := (derivative : (a : K[X]) → K[X]) P
nil' : IsNilpotent.{u_2} (R := ↥K[f]) ((aeval ff : (a : K[X]) → ↥K[f]) P : ↥K[f])
sep' : IsUnit.{u_2} (M := ↥K[f]) ((aeval ff : (a : K[X]) → ↥K[f]) P' : ↥K[f])
s : End K V
mem : Membership.mem (γ := Subalgebra K (End K V)) K[f] s
hss :
  Eq.{u_2 + 1} (α := ↥K[f])
    ((aeval (Subtype.mk (p := fun (x : End K V) ↦ Membership.mem (γ := Subalgebra K (End K V)) K[f] x) s mem) :
          (a : K[X]) → ↥K[f])
        P :
      ↥K[f])
    (0 : ↥K[f])
k : ℕ
hk : (ff - Subtype.mk (p := fun (x : End K V) ↦ Membership.mem (γ := Subalgebra K (End K V)) K[f] x) s mem) ^ k = 0
⊢ (↑((ff - Subtype.mk (p := fun (x : End K V) ↦ Membership.mem (γ := Subalgebra K (End K V)) K[f] x) s mem) ^ k) :
      End K V) =
    (↑0 : End K V)

Tactic:
rw [Subtype.ext_iff] at hk

Premises used: Subtype.ext_iff
-- Module: Mathlib.LinearAlgebra.JordanChevalley
Goal:
K : Type u_1
V : Type u_2
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
f : End K V
P : K[X]
k_1 : ℕ
sep : P.Separable
nil : minpoly K f ∣ P ^ k_1
ff : ↥K[f] := Subtype.mk (p := fun (x : End K V) ↦ Membership.mem (γ := Subalgebra K (End K V)) K[f] x) f ⋯
P' : K[X] := (derivative : (a : K[X]) → K[X]) P
nil' : IsNilpotent.{u_2} (R := ↥K[f]) ((aeval ff : (a : K[X]) → ↥K[f]) P : ↥K[f])
sep' : IsUnit.{u_2} (M := ↥K[f]) ((aeval ff : (a : K[X]) → ↥K[f]) P' : ↥K[f])
s : End K V
mem : Membership.mem (γ := Subalgebra K (End K V)) K[f] s
hss :
  Eq.{u_2 + 1} (α := ↥K[f])
    ((aeval (Subtype.mk (p := fun (x : End K V) ↦ Membership.mem (γ := Subalgebra K (End K V)) K[f] x) s mem) :
          (a : K[X]) → ↥K[f])
        P :
      ↥K[f])
    (0 : ↥K[f])
k : ℕ
hk :
  (↑((ff - Subtype.mk (p := fun (x : End K V) ↦ Membership.mem (γ := Subalgebra K (End K V)) K[f] x) s mem) ^ k) :
      End K V) =
    (↑0 : End K V)
⊢ (f - s) ^ k = 0

Tactic:
simpa using hk
-- Module: Mathlib.LinearAlgebra.JordanChevalley
Goal:
K : Type u_1
V : Type u_2
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
f : End K V
P : K[X]
k_1 : ℕ
sep : P.Separable
nil : minpoly K f ∣ P ^ k_1
ff : ↥K[f] := Subtype.mk (p := fun (x : End K V) ↦ Membership.mem (γ := Subalgebra K (End K V)) K[f] x) f ⋯
P' : K[X] := (derivative : (a : K[X]) → K[X]) P
nil' : IsNilpotent.{u_2} (R := ↥K[f]) ((aeval ff : (a : K[X]) → ↥K[f]) P : ↥K[f])
sep' : IsUnit.{u_2} (M := ↥K[f]) ((aeval ff : (a : K[X]) → ↥K[f]) P' : ↥K[f])
s : End K V
mem : Membership.mem (γ := Subalgebra K (End K V)) K[f] s
hss :
  Eq.{u_2 + 1} (α := ↥K[f])
    ((aeval (Subtype.mk (p := fun (x : End K V) ↦ Membership.mem (γ := Subalgebra K (End K V)) K[f] x) s mem) :
          (a : K[X]) → ↥K[f])
        P :
      ↥K[f])
    (0 : ↥K[f])
k : ℕ
hk : (ff - Subtype.mk (p := fun (x : End K V) ↦ Membership.mem (γ := Subalgebra K (End K V)) K[f] x) s mem) ^ k = 0
rwa :
  ∀
    (hss :
      Eq.{u_2 + 1} (α := End K V)
        (↑((aeval (Subtype.mk (p := fun (x : End K V) ↦ Membership.mem (γ := Subalgebra K (End K V)) K[f] x) s mem) :
                (a : K[X]) → ↥K[f])
              P) :
          End K V)
        (↑0 : End K V))
    (k : ℕ)
    (hk :
      (ff - Subtype.mk (p := fun (x : End K V) ↦ Membership.mem (γ := Subalgebra K (End K V)) K[f] x) s mem) ^ k = 0),
    Eq.{u_2 + 1} (α := End K V) ((aeval s : (a : K[X]) → End K V) P : End K V) (0 : End K V)
rwa₁ rwa₂ rwa₃ rwa₄ :
  ∀ (hss : Eq.{u_2 + 1} (α := End K V) ((aeval s : (a : K[X]) → End K V) P : End K V) ((↑0 : End K V) : End K V))
    (k : ℕ)
    (hk :
      (ff - Subtype.mk (p := fun (x : End K V) ↦ Membership.mem (γ := Subalgebra K (End K V)) K[f] x) s mem) ^ k = 0),
    Eq.{u_2 + 1} (α := End K V) ((aeval s : (a : K[X]) → End K V) P : End K V) (0 : End K V)
⊢ Eq.{u_2 + 1} (α := End K V) ((aeval s : (a : K[X]) → End K V) P : End K V) (0 : End K V)

Tactic:
rwa [Subtype.ext_iff, coe_aeval_mk_apply] at hss

Premises used: Subtype.ext_iff, Polynomial.coe_aeval_mk_apply
-- Module: Mathlib.LinearAlgebra.JordanChevalley
Goal:
K : Type u_1
V : Type u_2
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
f : End K V
P : K[X]
k_1 : ℕ
sep : P.Separable
nil : minpoly K f ∣ P ^ k_1
ff : ↥K[f] := Subtype.mk (p := fun (x : End K V) ↦ Membership.mem (γ := Subalgebra K (End K V)) K[f] x) f ⋯
P' : K[X] := (derivative : (a : K[X]) → K[X]) P
nil' : IsNilpotent.{u_2} (R := ↥K[f]) ((aeval ff : (a : K[X]) → ↥K[f]) P : ↥K[f])
sep' : IsUnit.{u_2} (M := ↥K[f]) ((aeval ff : (a : K[X]) → ↥K[f]) P' : ↥K[f])
s : End K V
mem : Membership.mem (γ := Subalgebra K (End K V)) K[f] s
hss :
  Eq.{u_2 + 1} (α := ↥K[f])
    ((aeval (Subtype.mk (p := fun (x : End K V) ↦ Membership.mem (γ := Subalgebra K (End K V)) K[f] x) s mem) :
          (a : K[X]) → ↥K[f])
        P :
      ↥K[f])
    (0 : ↥K[f])
k : ℕ
hk : (ff - Subtype.mk (p := fun (x : End K V) ↦ Membership.mem (γ := Subalgebra K (End K V)) K[f] x) s mem) ^ k = 0
⊢ Eq.{u_2 + 1} (α := End K V) ((aeval s : (a : K[X]) → End K V) P : End K V) (0 : End K V)

Tactic:
replace hss : aeval s P = 0 := by rwa [Subtype.ext_iff, coe_aeval_mk_apply] at hss
-- Module: Mathlib.LinearAlgebra.JordanChevalley
Goal:
K : Type u_1
V : Type u_2
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
f : End K V
P : K[X]
k_1 : ℕ
sep : P.Separable
nil : minpoly K f ∣ P ^ k_1
ff : ↥K[f] := Subtype.mk (p := fun (x : End K V) ↦ Membership.mem (γ := Subalgebra K (End K V)) K[f] x) f ⋯
P' : K[X] := (derivative : (a : K[X]) → K[X]) P
nil' : IsNilpotent.{u_2} (R := ↥K[f]) ((aeval ff : (a : K[X]) → ↥K[f]) P : ↥K[f])
sep' : IsUnit.{u_2} (M := ↥K[f]) ((aeval ff : (a : K[X]) → ↥K[f]) P' : ↥K[f])
s : End K V
mem : Membership.mem (γ := Subalgebra K (End K V)) K[f] s
k : ℕ
hk : (ff - Subtype.mk (p := fun (x : End K V) ↦ Membership.mem (γ := Subalgebra K (End K V)) K[f] x) s mem) ^ k = 0
hss : Eq.{u_2 + 1} (α := End K V) ((aeval s : (a : K[X]) → End K V) P : End K V) (0 : End K V)
⊢ s.IsSemisimple

Tactic:
isSemisimple_of_squarefree_aeval_eq_zero sep.squarefree hss

Premises used: Module.End.isSemisimple_of_squarefree_aeval_eq_zero, Polynomial.Separable.squarefree
-- Module: Mathlib.LinearAlgebra.JordanChevalley
Goal:
K : Type u_1
V : Type u_2
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
f : End K V
P : K[X]
k_1 : ℕ
sep : P.Separable
nil : minpoly K f ∣ P ^ k_1
ff : ↥K[f] := Subtype.mk (p := fun (x : End K V) ↦ Membership.mem (γ := Subalgebra K (End K V)) K[f] x) f ⋯
P' : K[X] := (derivative : (a : K[X]) → K[X]) P
nil' : IsNilpotent.{u_2} (R := ↥K[f]) ((aeval ff : (a : K[X]) → ↥K[f]) P : ↥K[f])
sep' : IsUnit.{u_2} (M := ↥K[f]) ((aeval ff : (a : K[X]) → ↥K[f]) P' : ↥K[f])
s : End K V
mem : Membership.mem (γ := Subalgebra K (End K V)) K[f] s
k : ℕ
hk : (ff - Subtype.mk (p := fun (x : End K V) ↦ Membership.mem (γ := Subalgebra K (End K V)) K[f] x) s mem) ^ k = 0
hss : Eq.{u_2 + 1} (α := End K V) ((aeval s : (a : K[X]) → End K V) P : End K V) (0 : End K V)
⊢ s.IsSemisimple

Tactic:
exact isSemisimple_of_squarefree_aeval_eq_zero sep.squarefree hss

Premises used: Module.End.isSemisimple_of_squarefree_aeval_eq_zero, Polynomial.Separable.squarefree
-- Module: Mathlib.LinearAlgebra.JordanChevalley
Goal:
K : Type u_1
V : Type u_2
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
f : End K V
inst_3 : FiniteDimensional K V
inst_4 : PerfectField K
obtain :
  ∀ (g : K[X]) (k : ℕ) (sep : Squarefree g) (nil : minpoly K f ∣ g ^ k),
    ∃ (n : End K V),
      Membership.mem (γ := Subalgebra K (End K V)) K[f] n ∧
        ∃ (s : End K V),
          Membership.mem (γ := Subalgebra K (End K V)) K[f] s ∧ IsNilpotent n ∧ s.IsSemisimple ∧ f = n + s
⊢ ∃ (n : End K V),
    Membership.mem (γ := Subalgebra K (End K V)) K[f] n ∧
      ∃ (s : End K V), Membership.mem (γ := Subalgebra K (End K V)) K[f] s ∧ IsNilpotent n ∧ s.IsSemisimple ∧ f = n + s

Tactic:
obtain ⟨g, k, sep, -, nil⟩ := exists_squarefree_dvd_pow_of_ne_zero (minpoly.ne_zero_of_finite K f)

Premises used: minpoly.ne_zero_of_finite, exists_squarefree_dvd_pow_of_ne_zero
-- Module: Mathlib.LinearAlgebra.JordanChevalley
Goal:
K : Type u_1
V : Type u_2
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
f : End K V
inst_3 : FiniteDimensional K V
inst_4 : PerfectField K
g : K[X]
k : ℕ
sep : Squarefree g
nil : minpoly K f ∣ g ^ k
⊢ g.Separable

Tactic:
rw [← PerfectField.separable_iff_squarefree] at sep

Premises used: PerfectField.separable_iff_squarefree
-- Module: Mathlib.LinearAlgebra.JordanChevalley
Goal:
K : Type u_1
V : Type u_2
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
f : End K V
inst_3 : FiniteDimensional K V
inst_4 : PerfectField K
g : K[X]
k : ℕ
sep : Squarefree g
nil : minpoly K f ∣ g ^ k
sep₁ : g.Separable
⊢ minpoly K f ∣ g ^ k

Tactic:
rw [← PerfectField.separable_iff_squarefree] at sep

Premises used: PerfectField.separable_iff_squarefree
-- Module: Mathlib.LinearAlgebra.JordanChevalley
Goal:
K : Type u_1
V : Type u_2
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
f : End K V
inst_3 : FiniteDimensional K V
inst_4 : PerfectField K
g : K[X]
k : ℕ
sep : g.Separable
nil : minpoly K f ∣ g ^ k
⊢ ∃ (n : End K V),
    Membership.mem (γ := Subalgebra K (End K V)) K[f] n ∧
      ∃ (s : End K V), Membership.mem (γ := Subalgebra K (End K V)) K[f] s ∧ IsNilpotent n ∧ s.IsSemisimple ∧ f = n + s

Tactic:
exists_isNilpotent_isSemisimple_of_separable_of_dvd_pow sep nil

Premises used: Module.End.exists_isNilpotent_isSemisimple_of_separable_of_dvd_pow
-- Module: Mathlib.LinearAlgebra.JordanChevalley
Goal:
K : Type u_1
V : Type u_2
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
f : End K V
inst_3 : FiniteDimensional K V
inst_4 : PerfectField K
g : K[X]
k : ℕ
sep : g.Separable
nil : minpoly K f ∣ g ^ k
⊢ ∃ (n : End K V),
    Membership.mem (γ := Subalgebra K (End K V)) K[f] n ∧
      ∃ (s : End K V), Membership.mem (γ := Subalgebra K (End K V)) K[f] s ∧ IsNilpotent n ∧ s.IsSemisimple ∧ f = n + s

Tactic:
exact exists_isNilpotent_isSemisimple_of_separable_of_dvd_pow sep nil

Premises used: Module.End.exists_isNilpotent_isSemisimple_of_separable_of_dvd_pow
-- Module: Mathlib.LinearAlgebra.JordanChevalley
Goal:
K : Type u_1
V : Type u_2
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
inst_4 : PerfectField K
n₁ s₁ n₂ s₂ : End K V
hn₁ : IsNilpotent n₁
hs₁ : s₁.IsSemisimple
hn₂ : IsNilpotent n₂
hs₂ : s₂.IsSemisimple
hc₁ : Commute n₁ s₁
hc₂ : Commute n₂ s₂
h : n₁ + s₁ = n₂ + s₂
obtain :
  ∀ (n₀ : End K V) (hn₀ : Membership.mem (γ := Subalgebra K (End K V)) K[n₁ + s₁] n₀) (s₀ : End K V)
    (hs₀ : Membership.mem (γ := Subalgebra K (End K V)) K[n₁ + s₁] s₀) (hn₀_nil : IsNilpotent n₀)
    (hs₀_ss : s₀.IsSemisimple) (h₀ : n₁ + s₁ = n₀ + s₀), n₁ = n₂ ∧ s₁ = s₂
⊢ n₁ = n₂ ∧ s₁ = s₂

Tactic:
obtain ⟨n₀, hn₀, s₀, hs₀, hn₀_nil, hs₀_ss, h₀⟩ := (n₁ + s₁).exists_isNilpotent_isSemisimple

Premises used: Module.End.exists_isNilpotent_isSemisimple
-- Module: Mathlib.LinearAlgebra.JordanChevalley
Goal:
K : Type u_1
V : Type u_2
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
inst_4 : PerfectField K
n₁ s₁ n₂ s₂ : End K V
hn₁ : IsNilpotent n₁
hs₁ : s₁.IsSemisimple
hn₂ : IsNilpotent n₂
hs₂ : s₂.IsSemisimple
hc₁ : Commute n₁ s₁
hc₂ : Commute n₂ s₂
h : n₁ + s₁ = n₂ + s₂
n₀ : End K V
hn₀ : Membership.mem (γ := Subalgebra K (End K V)) K[n₁ + s₁] n₀
s₀ : End K V
hs₀ : Membership.mem (γ := Subalgebra K (End K V)) K[n₁ + s₁] s₀
hn₀_nil : IsNilpotent n₀
hs₀_ss : s₀.IsSemisimple
h₀ : n₁ + s₁ = n₀ + s₀
this : ∀ {n s : End K V}, IsNilpotent n → s.IsSemisimple → Commute n s → n₁ + s₁ = n + s → s = s₀
⊢ n₁ = n₂ ∧ s₁ = s₂

Tactic:
grind
-- Module: Mathlib.LinearAlgebra.JordanChevalley
Goal:
K : Type u_1
V : Type u_2
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
inst_4 : PerfectField K
n₁ s₁ n₂ s₂ : End K V
hn₁ : IsNilpotent n₁
hs₁ : s₁.IsSemisimple
hn₂ : IsNilpotent n₂
hs₂ : s₂.IsSemisimple
hc₁ : Commute n₁ s₁
hc₂ : Commute n₂ s₂
h : n₁ + s₁ = n₂ + s₂
n₀ : End K V
hn₀ : Membership.mem (γ := Subalgebra K (End K V)) K[n₁ + s₁] n₀
s₀ : End K V
hs₀ : Membership.mem (γ := Subalgebra K (End K V)) K[n₁ + s₁] s₀
hn₀_nil : IsNilpotent n₀
hs₀_ss : s₀.IsSemisimple
h₀ : n₁ + s₁ = n₀ + s₀
suffices : ∀ {n s : End K V}, IsNilpotent n → s.IsSemisimple → Commute n s → n₁ + s₁ = n + s → s = s₀
⊢ n₁ = n₂ ∧ s₁ = s₂

Tactic:
suffices ∀ {n s}, IsNilpotent n → s.IsSemisimple → Commute n s → n₁ + s₁ = n + s → s = s₀ by grind