awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Isomorphisms (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
p p' : Submodule R M
x : ↥(p ⊔ p')
hx : (↑x : M) ∈ p
⊢ Eq (α := ↥(p ⊔ p') ⧸ comap (p ⊔ p').subtype p') (Submodule.Quotient.mk x)
    ((quotientInfEquivSupQuotient p p' :
        (a : ↥p ⧸ comap p.subtype p ⊓ comap p.subtype p') → ↥(p ⊔ p') ⧸ comap (p ⊔ p').subtype p')
      (Submodule.Quotient.mk (Subtype.mk (p := fun (x : M) ↦ x ∈ p) (↑x : M) hx)))
have rw : Eq (α := ↥(p ⊔ p') ⧸ comap (p ⊔ p').subtype p') (Submodule.Quotient.mk x)
  (Submodule.Quotient.mk ((inclusion sorry : (a : ↥p) → ↥(p ⊔ p')) (Subtype.mk (p := fun (x : M) ↦ x ∈ p) (↑x : M) hx)))
Tactic: rw [quotientInfEquivSupQuotient_apply_mk, inclusion_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Isomorphisms (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
p p' : Submodule R M
x : ↥(p ⊔ p')
hx : (↑x : M) ∈ p
rw :
  Eq (α := ↥(p ⊔ p') ⧸ comap (p ⊔ p').subtype p') (Submodule.Quotient.mk x)
    (Submodule.Quotient.mk ((inclusion ⋯ : (a : ↥p) → ↥(p ⊔ p')) (Subtype.mk (p := fun (x : M) ↦ x ∈ p) (↑x : M) hx)))
⊢ Eq (α := ↥(p ⊔ p') ⧸ comap (p ⊔ p').subtype p') (Submodule.Quotient.mk x)
    ((quotientInfEquivSupQuotient p p' :
        (a : ↥p ⧸ comap p.subtype p ⊓ comap p.subtype p') → ↥(p ⊔ p') ⧸ comap (p ⊔ p').subtype p')
      (Submodule.Quotient.mk (Subtype.mk (p := fun (x : M) ↦ x ∈ p) (↑x : M) hx)))
have rw₁ : Eq (α := ↥(p ⊔ p') ⧸ comap (p ⊔ p').subtype p') (Submodule.Quotient.mk x)
  (Submodule.Quotient.mk
    (Subtype.mk (p := fun (x : M) ↦ x ∈ p ⊔ p') (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ p) (↑x : M) hx) : M) sorry))
Tactic: rw [quotientInfEquivSupQuotient_apply_mk, inclusion_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Isomorphisms (goal)
Goal:
R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup M₂
inst_3 : AddCommGroup M₃
inst_4 : Module R M
inst_5 : Module R M₂
inst_6 : Module R M₃
f : M →ₗ[R] M₂
S T : Submodule R M
h : S ≤ T
⊢ map S.mkQ T = map S.mkQ (S ⊔ T)
have rw : map S.mkQ T = map S.mkQ S ⊔ map S.mkQ T
Tactic: rw [map_sup, mkQ_map_self, bot_sup_eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Isomorphisms (goal)
Goal:
R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup M₂
inst_3 : AddCommGroup M₃
inst_4 : Module R M
inst_5 : Module R M₂
inst_6 : Module R M₃
f : M →ₗ[R] M₂
S T : Submodule R M
h : S ≤ T
rw : map S.mkQ T = map S.mkQ S ⊔ map S.mkQ T
⊢ map S.mkQ T = map S.mkQ (S ⊔ T)
have rw₁ : map S.mkQ T = ⊥ ⊔ map S.mkQ T
Tactic: rw [map_sup, mkQ_map_self, bot_sup_eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Isomorphisms (goal)
Goal:
R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup M₂
inst_3 : AddCommGroup M₃
inst_4 : Module R M
inst_5 : Module R M₂
inst_6 : Module R M₃
f : M →ₗ[R] M₂
S T : Submodule R M
h : S ≤ T
rw : map S.mkQ T = map S.mkQ S ⊔ map S.mkQ T
rw₁ : map S.mkQ T = ⊥ ⊔ map S.mkQ T
⊢ map S.mkQ T = map S.mkQ (S ⊔ T)
have rw₂ : map S.mkQ T = map S.mkQ T
Tactic: rw [map_sup, mkQ_map_self, bot_sup_eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Isomorphisms (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
S T : Submodule R M
hST : T ≤ S
⊢ Nat.card.{u_2} ↥(map T.mkQ S) * Nat.card.{u_2} (M ⧸ S) = Nat.card.{u_2} (M ⧸ T)
have rw : Nat.card.{u_2} ↥(map T.mkQ S) * Nat.card.{u_2} (M ⧸ S) =
  Nat.card.{u_2} ↥(map T.mkQ S) * Nat.card.{u_2} ((M ⧸ T) ⧸ map T.mkQ S)
Tactic: rw [Submodule.card_eq_card_quotient_mul_card (map T.mkQ S),
    Nat.card_congr (quotientQuotientEquivQuotient T S hST).toEquiv]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Isomorphisms (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
S T : Submodule R M
hST : T ≤ S
rw :
  Nat.card.{u_2} ↥(map T.mkQ S) * Nat.card.{u_2} (M ⧸ S) =
    Nat.card.{u_2} ↥(map T.mkQ S) * Nat.card.{u_2} ((M ⧸ T) ⧸ map T.mkQ S)
⊢ Nat.card.{u_2} ↥(map T.mkQ S) * Nat.card.{u_2} (M ⧸ S) = Nat.card.{u_2} (M ⧸ T)
have rw₁ : Nat.card.{u_2} ↥(map T.mkQ S) * Nat.card.{u_2} (M ⧸ S) = Nat.card.{u_2} ↥(map T.mkQ S) * Nat.card.{u_2} (M ⧸ S)
Tactic: rw [Submodule.card_eq_card_quotient_mul_card (map T.mkQ S),
    Nat.card_congr (quotientQuotientEquivQuotient T S hST).toEquiv]
-- Lean 4 proof step from Mathlib.LinearAlgebra.JordanChevalley (goal)
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
⊢ IsNilpotent.{u_2} (R := ↥K[f]) ((aeval ff : (a : K[X]) → ↥K[f]) P : ↥K[f])
have h : HPow.hPow (α := ↥K[f]) ((aeval ff : (a : K[X]) → ↥K[f]) P : ↥K[f]) k = 0
Tactic: use k
-- Lean 4 proof step from Mathlib.LinearAlgebra.JordanChevalley (goal)
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
⊢ HPow.hPow (α := ↥K[f]) ((aeval ff : (a : K[X]) → ↥K[f]) P : ↥K[f]) k = 0
have h : ∀ (q : K[X]) (hq : P ^ k = minpoly K f * q), HPow.hPow (α := ↥K[f]) ((aeval ff : (a : K[X]) → ↥K[f]) P : ↥K[f]) k = 0
Tactic: obtain ⟨q, hq⟩ := nil
Cleared hypotheses: nil
-- Lean 4 proof step from Mathlib.LinearAlgebra.JordanChevalley (goal)
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
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
q : K[X]
hq : P ^ k = minpoly K f * q
⊢ HPow.hPow (α := ↥K[f]) ((aeval ff : (a : K[X]) → ↥K[f]) P : ↥K[f]) k = 0
have h : Eq.{u_2 + 1} (α := End K V) (↑((aeval ff : (a : K[X]) → ↥K[f]) (P ^ k)) : End K V) (↑0 : End K V)
Tactic: rw [← map_pow, Subtype.ext_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.JordanChevalley (hypothesis)
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
⊢ ∃ (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
have nil' : IsNilpotent.{u_2} (R := ↥K[f]) ((aeval ff : (a : K[X]) → ↥K[f]) P : ↥K[f])
Tactic: have nil' : IsNilpotent (aeval ff P) := by
    use k
    obtain ⟨q, hq⟩ := nil
    rw [← map_pow, Subtype.ext_iff]
    simp [ff, hq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.JordanChevalley (goal)
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])
have obtain : ∀ (a b : K[X]) (h : a * P ^ k + b * P' = 1), IsUnit.{u_2} (M := ↥K[f]) ((aeval ff : (a : K[X]) → ↥K[f]) P' : ↥K[f])
Tactic: obtain ⟨a, b, h⟩ : IsCoprime (P ^ k) P' := sep.pow_left
-- Lean 4 proof step from Mathlib.LinearAlgebra.JordanChevalley (hypothesis)
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
⊢ IsUnit.{u_2} (M := ↥K[f]) ((aeval ff : (a : K[X]) → ↥K[f]) P' : ↥K[f])
have 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
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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.JordanChevalley (goal)
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])
have 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)
Tactic: refine .of_mul_eq_one_right (aeval ff b) (Subtype.ext_iff.mpr ?_)
-- Lean 4 proof step from Mathlib.LinearAlgebra.JordanChevalley (hypothesis)
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])
⊢ ∃ (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
have sep' : 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
-- Lean 4 proof step from Mathlib.LinearAlgebra.JordanChevalley (goal)
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])
⊢ ∃ (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
have 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
Tactic: obtain ⟨⟨s, mem⟩, ⟨⟨k, hk⟩, hss⟩, -⟩ := existsUnique_nilpotent_sub_and_aeval_eq_zero nil' sep'
-- Lean 4 proof step from Mathlib.LinearAlgebra.JordanChevalley (goal)
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
have refine_1 : Membership.mem (γ := Subalgebra K (End K V)) K[f] (f - s)
Tactic: refine ⟨f - s, ?_, s, mem, ⟨k, ?_⟩, ?_, (sub_add_cancel f s).symm⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.JordanChevalley (goal)
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)
⊢ ∃ (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
have refine_2 : (f - s) ^ k = 0
Tactic: refine ⟨f - s, ?_, s, mem, ⟨k, ?_⟩, ?_, (sub_add_cancel f s).symm⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.JordanChevalley (goal)
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
⊢ ∃ (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
have refine_3 : s.IsSemisimple
Tactic: refine ⟨f - s, ?_, s, mem, ⟨k, ?_⟩, ?_, (sub_add_cancel f s).symm⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.JordanChevalley (hypothesis)
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
⊢ (f - s) ^ k = 0
have 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)
Tactic: rw [Subtype.ext_iff] at hk
Cleared hypotheses: hk
-- Lean 4 proof step from Mathlib.LinearAlgebra.JordanChevalley (goal)
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)
have 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)
Tactic: rwa [Subtype.ext_iff, coe_aeval_mk_apply] at hss
Cleared hypotheses: hss, k, hk
-- Lean 4 proof step from Mathlib.LinearAlgebra.JordanChevalley (goal)
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)
⊢ Eq.{u_2 + 1} (α := End K V) ((aeval s : (a : K[X]) → End K V) P : End K V) (0 : End K V)
have 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)
Tactic: rwa [Subtype.ext_iff, coe_aeval_mk_apply] at hss
Cleared hypotheses: hss, k, hk
-- Lean 4 proof step from Mathlib.LinearAlgebra.JordanChevalley (hypothesis)
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
⊢ s.IsSemisimple
have hss₁ : 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
Cleared hypotheses: hss
-- Lean 4 proof step from Mathlib.LinearAlgebra.JordanChevalley (goal)
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
⊢ ∃ (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
have 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
Tactic: obtain ⟨g, k, sep, -, nil⟩ := exists_squarefree_dvd_pow_of_ne_zero (minpoly.ne_zero_of_finite K f)
-- Lean 4 proof step from Mathlib.LinearAlgebra.JordanChevalley (hypothesis)
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
⊢ ∃ (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
have sep₁ : g.Separable
Tactic: rw [← PerfectField.separable_iff_squarefree] at sep
Cleared hypotheses: sep, nil