awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.SModEq.Basic (goal)
Goal:
A : Type u_3
inst : CommRing A
I : Ideal A
ι : Type u_6
s : Finset ι
x y : ι → A
hxy : ∀ i ∈ s, SModEq (R := A) I (x i) (y i)
⊢ SModEq.{u_3, u_3} (R := A) (M := A) I (∏ i ∈ s, x i) (∏ i ∈ s, y i)
have empty : ∀ (hxy : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → SModEq (R := A) I (x i) (y i)),
  SModEq.{u_3, u_3} (R := A) (M := A) I (∏ i ∈ ∅, x i) (∏ i ∈ ∅, y i)
Tactic: classical
  induction s using Finset.cons_induction with
  | empty => simp [SModEq.rfl]
  | cons i s _ ih =>
    grw [Finset.prod_cons, Finset.prod_cons, hxy i (Finset.mem_cons_self i s),
      ih (fun j hj ↦ hxy j (Finset.mem_cons_of_mem hj))]
Cleared hypotheses: s, hxy
-- Lean 4 proof step from Mathlib.LinearAlgebra.SModEq.Basic (goal)
Goal:
A : Type u_3
inst : CommRing A
I : Ideal A
ι : Type u_6
s : Finset ι
x y : ι → A
hxy : ∀ i ∈ s, SModEq (R := A) I (x i) (y i)
empty :
  ∀ (hxy : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → SModEq (R := A) I (x i) (y i)),
    SModEq.{u_3, u_3} (R := A) (M := A) I (∏ i ∈ ∅, x i) (∏ i ∈ ∅, y i)
⊢ SModEq.{u_3, u_3} (R := A) (M := A) I (∏ i ∈ s, x i) (∏ i ∈ s, y i)
have cons : ∀ (i : ι) (s : Finset ι) (h : i ∉ s)
  (ih :
    ∀ (hxy : ∀ i ∈ s, SModEq (R := A) I (x i) (y i)),
      SModEq.{u_3, u_3} (R := A) (M := A) I (∏ i ∈ s, x i) (∏ i ∈ s, y i))
  (hxy : ∀ i_1 ∈ Finset.cons i s h, SModEq (R := A) I (x i_1) (y i_1)),
  SModEq.{u_3, u_3} (R := A) (M := A) I (∏ i ∈ Finset.cons i s h, x i) (∏ i ∈ Finset.cons i s h, y i)
Tactic: classical
  induction s using Finset.cons_induction with
  | empty => simp [SModEq.rfl]
  | cons i s _ ih =>
    grw [Finset.prod_cons, Finset.prod_cons, hxy i (Finset.mem_cons_self i s),
      ih (fun j hj ↦ hxy j (Finset.mem_cons_of_mem hj))]
Cleared hypotheses: s, hxy
-- Lean 4 proof step from Mathlib.LinearAlgebra.SModEq.Basic (goal)
Goal:
A : Type u_3
inst : CommRing A
I : Ideal A
x y : A
n : ℕ
hxy : SModEq (R := A) I x y
⊢ SModEq (R := A) I (x ^ n) (y ^ n)
have simp : ∀
  (hxy :
    Eq (α := A ⧸ I) ((Ideal.Quotient.mk I : (a : A) → A ⧸ I) x : A ⧸ I)
      ((Ideal.Quotient.mk I : (a : A) → A ⧸ I) y : A ⧸ I)),
  HPow.hPow (α := A ⧸ I) ((Ideal.Quotient.mk I : (a : A) → A ⧸ I) x : A ⧸ I) n =
    HPow.hPow (α := A ⧸ I) ((Ideal.Quotient.mk I : (a : A) → A ⧸ I) y : A ⧸ I) n
Tactic: simp only [SModEq.def, Ideal.Quotient.mk_eq_mk, map_pow] at hxy ⊢
Cleared hypotheses: hxy
-- Lean 4 proof step from Mathlib.LinearAlgebra.SModEq.Basic (goal)
Goal:
A : Type u_3
inst : CommRing A
I : Ideal A
x y : A
n : ℕ
hxy :
  Eq (α := A ⧸ I) ((Ideal.Quotient.mk I : (a : A) → A ⧸ I) x : A ⧸ I)
    ((Ideal.Quotient.mk I : (a : A) → A ⧸ I) y : A ⧸ I)
⊢ HPow.hPow (α := A ⧸ I) ((Ideal.Quotient.mk I : (a : A) → A ⧸ I) x : A ⧸ I) n =
    HPow.hPow (α := A ⧸ I) ((Ideal.Quotient.mk I : (a : A) → A ⧸ I) y : A ⧸ I) n
have rw : HPow.hPow (α := A ⧸ I) ((Ideal.Quotient.mk I : (a : A) → A ⧸ I) y : A ⧸ I) n =
  HPow.hPow (α := A ⧸ I) ((Ideal.Quotient.mk I : (a : A) → A ⧸ I) y : A ⧸ I) n
Tactic: rw [hxy]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SModEq.Basic (hypothesis)
Goal:
R : Type u_1
inst : Ring R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
U : Submodule R M
x₁ x₂ y₁ y₂ : M
hxy₁ : x₁ ≡ y₁ [SMOD U]
hxy₂ : x₂ ≡ y₂ [SMOD U]
⊢ x₁ - x₂ ≡ y₁ - y₂ [SMOD U]
have hxy₃ : Eq (α := M ⧸ U) (Submodule.Quotient.mk x₁) (Submodule.Quotient.mk y₁)
Tactic: rw [SModEq.def] at hxy₁ hxy₂ ⊢
Cleared hypotheses: hxy₁, hxy₂
-- Lean 4 proof step from Mathlib.LinearAlgebra.SModEq.Basic (hypothesis)
Goal:
R : Type u_1
inst : Ring R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
U : Submodule R M
x₁ x₂ y₁ y₂ : M
hxy₁ : x₁ ≡ y₁ [SMOD U]
hxy₂ : x₂ ≡ y₂ [SMOD U]
hxy₃ : Eq (α := M ⧸ U) (Submodule.Quotient.mk x₁) (Submodule.Quotient.mk y₁)
⊢ x₁ - x₂ ≡ y₁ - y₂ [SMOD U]
have hxy₄ : Eq (α := M ⧸ U) (Submodule.Quotient.mk x₂) (Submodule.Quotient.mk y₂)
Tactic: rw [SModEq.def] at hxy₁ hxy₂ ⊢
Cleared hypotheses: hxy₁, hxy₂
-- Lean 4 proof step from Mathlib.LinearAlgebra.SModEq.Basic (goal)
Goal:
R : Type u_1
inst : Ring R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
U : Submodule R M
x₁ x₂ y₁ y₂ : M
hxy₁ : Eq (α := M ⧸ U) (Submodule.Quotient.mk x₁) (Submodule.Quotient.mk y₁)
hxy₂ : Eq (α := M ⧸ U) (Submodule.Quotient.mk x₂) (Submodule.Quotient.mk y₂)
⊢ Eq (α := M ⧸ U) (Submodule.Quotient.mk (x₁ - x₂)) (Submodule.Quotient.mk (y₁ - y₂))
have simp_rw : HSub.hSub (α := M ⧸ U) (Submodule.Quotient.mk x₁) (Submodule.Quotient.mk x₂) =
  HSub.hSub (α := M ⧸ U) (Submodule.Quotient.mk y₁) (Submodule.Quotient.mk y₂)
Tactic: simp_rw [Quotient.mk_sub, hxy₁, hxy₂]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SModEq.Basic (goal)
Goal:
R : Type u_1
inst : Ring R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
U : Submodule R M
x₁ x₂ y₁ y₂ : M
hxy₁ : Eq (α := M ⧸ U) (Submodule.Quotient.mk x₁) (Submodule.Quotient.mk y₁)
hxy₂ : Eq (α := M ⧸ U) (Submodule.Quotient.mk x₂) (Submodule.Quotient.mk y₂)
simp_rw :
  HSub.hSub (α := M ⧸ U) (Submodule.Quotient.mk x₁) (Submodule.Quotient.mk x₂) =
    HSub.hSub (α := M ⧸ U) (Submodule.Quotient.mk y₁) (Submodule.Quotient.mk y₂)
⊢ Eq (α := M ⧸ U) (Submodule.Quotient.mk (x₁ - x₂)) (Submodule.Quotient.mk (y₁ - y₂))
have simp_rw₁ : HSub.hSub (α := M ⧸ U) (Submodule.Quotient.mk y₁) (Submodule.Quotient.mk x₂) =
  HSub.hSub (α := M ⧸ U) (Submodule.Quotient.mk y₁) (Submodule.Quotient.mk y₂)
Tactic: simp_rw [Quotient.mk_sub, hxy₁, hxy₂]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SModEq.Basic (goal)
Goal:
R : Type u_1
inst : Ring R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
U : Submodule R M
x : M
⊢ x ≡ 0 [SMOD U] ↔ x ∈ U
have rw : Eq (α := M ⧸ U) (Submodule.Quotient.mk x) (Submodule.Quotient.mk 0) ↔ x ∈ U
Tactic: rw [SModEq.def, Submodule.Quotient.eq, sub_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SModEq.Basic (goal)
Goal:
R : Type u_1
inst : Ring R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
U : Submodule R M
x : M
rw : Eq (α := M ⧸ U) (Submodule.Quotient.mk x) (Submodule.Quotient.mk 0) ↔ x ∈ U
⊢ x ≡ 0 [SMOD U] ↔ x ∈ U
have rw₁ : x - 0 ∈ U ↔ x ∈ U
Tactic: rw [SModEq.def, Submodule.Quotient.eq, sub_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SModEq.Basic (goal)
Goal:
R : Type u_1
inst : Ring R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
U : Submodule R M
x : M
rw : Eq (α := M ⧸ U) (Submodule.Quotient.mk x) (Submodule.Quotient.mk 0) ↔ x ∈ U
rw₁ : x - 0 ∈ U ↔ x ∈ U
⊢ x ≡ 0 [SMOD U] ↔ x ∈ U
have rw₂ : x ∈ U ↔ x ∈ U
Tactic: rw [SModEq.def, Submodule.Quotient.eq, sub_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SModEq.Basic (goal)
Goal:
R : Type u_6
inst : CommRing R
I : Ideal R
x y : R
h : SModEq (R := R) I x y
f : R[X]
⊢ SModEq (R := R) I (Polynomial.eval x f) (Polynomial.eval y f)
have simp_rw : SModEq.{u_6, u_6} (R := R) (M := R) I (∑ x_1 ∈ f.support, f.coeff x_1 * x ^ x_1) (∑ x ∈ f.support, f.coeff x * y ^ x)
Tactic: simp_rw [Polynomial.eval_eq_sum, Polynomial.sum]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SModEq.Basic (goal)
Goal:
R : Type u_1
inst : Ring R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
U : Submodule R M
x y : M
⊢ x +ᵥ (↑U : Set M) ⊆ y +ᵥ (↑U : Set M) ↔ x ≡ y [SMOD U]
have rw : x +ᵥ (↑U : Set M) ⊆ y +ᵥ (↑U : Set M) ↔ x - y ∈ U
Tactic: rw [SModEq.sub_mem]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SModEq.Basic (goal)
Goal:
R : Type u_1
inst : Ring R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
U : Submodule R M
x y : M
⊢ x +ᵥ (↑U : Set M) ⊆ y +ᵥ (↑U : Set M) ↔ x - y ∈ U
have refine_1 : ∀ (h : x +ᵥ (↑U : Set M) ⊆ y +ᵥ (↑U : Set M)), x - y ∈ U
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.SModEq.Basic (goal)
Goal:
R : Type u_1
inst : Ring R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
U : Submodule R M
x y : M
refine_1 : ∀ (h : x +ᵥ (↑U : Set M) ⊆ y +ᵥ (↑U : Set M)), x - y ∈ U
⊢ x +ᵥ (↑U : Set M) ⊆ y +ᵥ (↑U : Set M) ↔ x - y ∈ U
have refine_2 : ∀ (h : x - y ∈ U), x +ᵥ (↑U : Set M) ⊆ y +ᵥ (↑U : Set M)
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.SModEq.Basic (hypothesis)
Goal:
R : Type u_1
inst : Ring R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
U : Submodule R M
x y : M
h : x +ᵥ (↑U : Set M) ⊆ y +ᵥ (↑U : Set M)
⊢ x - y ∈ U
have h₁ : (↑U : Set M) ⊆ (y - x) +ᵥ (↑U : Set M)
Tactic: rw [Set.vadd_set_subset_iff_subset_neg_vadd_set, vadd_vadd, neg_add_eq_sub] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.SModEq.Basic (goal)
Goal:
R : Type u_1
inst : Ring R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
U : Submodule R M
x y : M
h : x - y ∈ U
⊢ x +ᵥ (↑U : Set M) ⊆ y +ᵥ (↑U : Set M)
have refine_2 : (↑U : Set M) ⊆ (y - x) +ᵥ (↑U : Set M)
Tactic: rw [Set.vadd_set_subset_iff_subset_neg_vadd_set, vadd_vadd, neg_add_eq_sub]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SModEq.Pointwise (goal)
Goal:
R : Type u_1
inst : Ring R
I : Ideal R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
U : Submodule R M
x y : M
hxy : x ≡ y [SMOD U]
c : R
hc : c ∈ I
⊢ c • x ≡ c • y [SMOD I • U]
have rw : ∀ (hxy : x - y ∈ U) {c : R} (hc : c ∈ I), c • x - c • y ∈ I • U
Tactic: rw [SModEq.sub_mem] at hxy ⊢
Cleared hypotheses: hxy, c, hc
-- Lean 4 proof step from Mathlib.LinearAlgebra.SModEq.Pointwise (goal)
Goal:
R : Type u_1
inst : Ring R
I : Ideal R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
U : Submodule R M
x y : M
hxy : x - y ∈ U
c : R
hc : c ∈ I
⊢ c • x - c • y ∈ I • U
have rw : c • (x - y) ∈ I • U
Tactic: rw [← smul_sub]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SModEq.Pow (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
I J : Ideal R
p : ℕ
hpI : (↑p : R) ∈ I
x y : R
h : SModEq (R := R) J x y
hJI : J ≤ I
⊢ SModEq (R := R) (J * I) (x ^ p) (y ^ p)
have h₁ : Eq (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) x : R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) y : R ⧸ I)
Tactic: have h₁ := idealQuotientMk.mp <| h.mono hJI
-- Lean 4 proof step from Mathlib.LinearAlgebra.SModEq.Pow (goal)
Goal:
R : Type u_1
inst : CommRing R
I J : Ideal R
p : ℕ
hpI : (↑p : R) ∈ I
x y : R
h : SModEq (R := R) J x y
hJI : J ≤ I
h₁ :
  Eq (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) x : R ⧸ I)
    ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) y : R ⧸ I)
⊢ SModEq (R := R) (J * I) (x ^ p) (y ^ p)
have rw : ∀ (h : x - y ∈ J) (hJI : J ≤ I)
  (h₁ :
    Eq (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) x : R ⧸ I)
      ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) y : R ⧸ I)),
  x ^ p - y ^ p ∈ J * I
Tactic: rw [SModEq.sub_mem] at h ⊢
Cleared hypotheses: h, hJI, h₁
-- Lean 4 proof step from Mathlib.LinearAlgebra.SModEq.Pow (goal)
Goal:
R : Type u_1
inst : CommRing R
I J : Ideal R
p : ℕ
hpI : (↑p : R) ∈ I
x y : R
h : x - y ∈ J
hJI : J ≤ I
h₁ :
  Eq (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) x : R ⧸ I)
    ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) y : R ⧸ I)
⊢ x ^ p - y ^ p ∈ J * I
have rw : (x - y) * ∑ i ∈ Finset.range p, y ^ i * x ^ (p - 1 - i) ∈ J * I
Tactic: rw [← Commute.mul_neg_geom_sum₂ (.all _ _)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SModEq.Pow (goal)
Goal:
R : Type u_1
inst : CommRing R
I J : Ideal R
p : ℕ
hpI : (↑p : R) ∈ I
x y : R
h : x - y ∈ J
hJI : J ≤ I
h₁ :
  Eq (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) x : R ⧸ I)
    ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) y : R ⧸ I)
⊢ (x - y) * ∑ i ∈ Finset.range p, y ^ i * x ^ (p - 1 - i) ∈ J * I
have refine : ∑ i ∈ Finset.range p, y ^ i * x ^ (p - 1 - i) ∈ I
Tactic: refine Ideal.mul_mem_mul h ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.SModEq.Pow (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
I J : Ideal R
p : ℕ
hpI : (↑p : R) ∈ I
x y : R
h : x - y ∈ J
hJI : J ≤ I
h₁ :
  Eq (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) x : R ⧸ I)
    ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) y : R ⧸ I)
⊢ ∑ i ∈ Finset.range p, y ^ i * x ^ (p - 1 - i) ∈ I
have h₂ : Eq.{u_1 + 1} (α := R ⧸ I) (↑p : R ⧸ I) 0
Tactic: have h₂ : (p : R ⧸ I) = 0 := by simpa using Ideal.Quotient.eq_zero_iff_mem.mpr hpI
-- Lean 4 proof step from Mathlib.LinearAlgebra.SModEq.Pow (goal)
Goal:
R : Type u_1
inst : CommRing R
I J : Ideal R
p : ℕ
hpI : (↑p : R) ∈ I
x y : R
h : x - y ∈ J
hJI : J ≤ I
h₁ :
  Eq (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) x : R ⧸ I)
    ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) y : R ⧸ I)
h₂ : Eq.{u_1 + 1} (α := R ⧸ I) (↑p : R ⧸ I) 0
⊢ ∑ i ∈ Finset.range p, y ^ i * x ^ (p - 1 - i) ∈ I
have simp : Eq.{u_1 + 1} (α := R ⧸ I)
  (∑ x ∈ Finset.range p, HPow.hPow (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) y : R ⧸ I) (x + (p - 1 - x))) 0
Tactic: simp only [← Ideal.Quotient.eq_zero_iff_mem, map_sum, map_mul, map_pow, h₁, ← pow_add]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SModEq.Pow (goal)
Goal:
R : Type u_1
inst : CommRing R
I J : Ideal R
p : ℕ
hpI : (↑p : R) ∈ I
x y : R
h : x - y ∈ J
hJI : J ≤ I
h₁ :
  Eq (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) x : R ⧸ I)
    ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) y : R ⧸ I)
h₂ : Eq.{u_1 + 1} (α := R ⧸ I) (↑p : R ⧸ I) 0
⊢ Eq.{u_1 + 1} (α := R ⧸ I)
    (∑ x ∈ Finset.range p, HPow.hPow (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) y : R ⧸ I) (x + (p - 1 - x)))
    0
have trans : Eq.{u_1 + 1} (α := R ⧸ I)
  (∑ x ∈ Finset.range p, HPow.hPow (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) y : R ⧸ I) (x + (p - 1 - x)))
  (∑ x ∈ Finset.range p, HPow.hPow (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) y : R ⧸ I) (p - 1))
Tactic: trans ∑ x ∈ Finset.range p, Ideal.Quotient.mk I y ^ (p - 1)
-- Lean 4 proof step from Mathlib.LinearAlgebra.SModEq.Pow (goal)
Goal:
R : Type u_1
inst : CommRing R
I J : Ideal R
p : ℕ
hpI : (↑p : R) ∈ I
x y : R
h : x - y ∈ J
hJI : J ≤ I
h₁ :
  Eq (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) x : R ⧸ I)
    ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) y : R ⧸ I)
h₂ : Eq.{u_1 + 1} (α := R ⧸ I) (↑p : R ⧸ I) 0
trans :
  Eq.{u_1 + 1} (α := R ⧸ I)
    (∑ x ∈ Finset.range p, HPow.hPow (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) y : R ⧸ I) (x + (p - 1 - x)))
    (∑ x ∈ Finset.range p, HPow.hPow (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) y : R ⧸ I) (p - 1))
⊢ Eq.{u_1 + 1} (α := R ⧸ I)
    (∑ x ∈ Finset.range p, HPow.hPow (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) y : R ⧸ I) (x + (p - 1 - x)))
    0
have trans₁ : Eq.{u_1 + 1} (α := R ⧸ I)
  (∑ x ∈ Finset.range p, HPow.hPow (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) y : R ⧸ I) (p - 1)) 0
Tactic: trans ∑ x ∈ Finset.range p, Ideal.Quotient.mk I y ^ (p - 1)
-- Lean 4 proof step from Mathlib.LinearAlgebra.SModEq.Pow (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
p : ℕ
hpI : (↑p : R) ∈ I
x y : R
h : SModEq (R := R) I x y
m : ℕ
ih : SModEq (R := R) (I ^ (m + 1)) (x ^ p ^ m) (y ^ p ^ m)
⊢ SModEq (R := R) (I ^ (m + 1 + 1)) (x ^ p ^ (m + 1)) (y ^ p ^ (m + 1))
have succ : SModEq (R := R) (I ^ (m + 1 + 1)) ((x ^ p ^ m) ^ p) ((y ^ p ^ m) ^ p)
Tactic: simp_rw [pow_succ _ m, pow_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SModEq.Pow (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
p : ℕ
hpI : (↑p : R) ∈ I
x y : R
h : SModEq (R := R) I x y
m : ℕ
⊢ SModEq (R := R) (I ^ (m + 1)) (x ^ p ^ m) (y ^ p ^ m)
have zero : SModEq (R := R) (I ^ HAdd.hAdd (α := ℕ) 0 1) (x ^ HPow.hPow (β := ℕ) p 0) (y ^ HPow.hPow (β := ℕ) p 0)
Tactic: induction m with
  | zero => simpa
  | succ m ih =>
    simp_rw [pow_succ _ m, pow_mul]
    exact ih.pow_add_one hpI m.succ_ne_zero
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.LinearAlgebra.SModEq.Pow (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
p : ℕ
hpI : (↑p : R) ∈ I
x y : R
h : SModEq (R := R) I x y
m : ℕ
zero : SModEq (R := R) (I ^ HAdd.hAdd (α := ℕ) 0 1) (x ^ HPow.hPow (β := ℕ) p 0) (y ^ HPow.hPow (β := ℕ) p 0)
⊢ SModEq (R := R) (I ^ (m + 1)) (x ^ p ^ m) (y ^ p ^ m)
have succ : ∀ (m : ℕ) (ih : SModEq (R := R) (I ^ (m + 1)) (x ^ p ^ m) (y ^ p ^ m)),
  SModEq (R := R) (I ^ (m + 1 + 1)) (x ^ p ^ (m + 1)) (y ^ p ^ (m + 1))
Tactic: induction m with
  | zero => simpa
  | succ m ih =>
    simp_rw [pow_succ _ m, pow_mul]
    exact ih.pow_add_one hpI m.succ_ne_zero
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.LinearAlgebra.Semisimple (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
⊢ f.IsSemisimple ↔ ∀ (p : ↥f.invtSubmodule), ∃ (q : ↥f.invtSubmodule), IsCompl p q
have rw : (∀ (a : ↥(invtSubmodule ((Algebra.lsmul R R M : (a : End R M) → End R M) f))),
    ∃ (b : ↥(invtSubmodule ((Algebra.lsmul R R M : (a : End R M) → End R M) f))), IsCompl a b) ↔
  ∀ (p : ↥f.invtSubmodule), ∃ (q : ↥f.invtSubmodule), IsCompl p q
Tactic: rw [IsSemisimple, isSemisimpleModule_iff, (AEval.mapSubmodule R M f).symm.complementedLattice_iff,
    complementedLattice_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Semisimple (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
p : Submodule R M
hp : p ∈ f.invtSubmodule
e : Submodule.{u_1, u_2} R[X] (AEval' (LinearMap.restrict f hp)) ≃o
  (↑(Iic
          ((AEval.mapSubmodule R M f :
              (a : ↥((Algebra.lsmul R R M : (a : End R M) → End R M) f).invtSubmodule) → Submodule R[X] (AEval R M f))
            (Subtype.mk (p := fun (x : Submodule R M) ↦
              Membership.mem (γ := Sublattice (Submodule R M))
                (invtSubmodule ((Algebra.lsmul R R M : (a : End R M) → End R M) f)) x)
              p hp)) :
        Set (Submodule.{u_1, u_2} R[X] (AEval R M f))) :
    Type u_2) :=
  OrderIso.trans (Submodule.orderIsoMapComap (AEval.restrict_equiv_mapSubmodule f p hp))
    (Submodule.mapIic
      ((AEval.mapSubmodule R M f :
          (a : ↥((Algebra.lsmul R R M : (a : End R M) → End R M) f).invtSubmodule) → Submodule R[X] (AEval R M f))
        (Subtype.mk (p := fun (x : Submodule R M) ↦
          Membership.mem (γ := Sublattice (Submodule R M))
            (invtSubmodule ((Algebra.lsmul R R M : (a : End R M) → End R M) f)) x)
          p hp)))
⊢ IsSemisimple (LinearMap.restrict f hp) ↔
    ∀ q ∈ f.invtSubmodule, q ≤ p → ∃ r ≤ p, r ∈ f.invtSubmodule ∧ Disjoint q r ∧ q ⊔ r = p
have simp_rw : (∀ (a : Submodule R M)
    (b :
      Membership.mem (γ := Sublattice (Submodule R M))
        (invtSubmodule ((Algebra.lsmul R R M : (a : End R M) → End R M) f)) a),
    a ≤ p →
      ∃ a_2 ≤ p,
        Membership.mem (γ := Sublattice (Submodule R M))
            (invtSubmodule ((Algebra.lsmul R R M : (a : End R M) → End R M) f)) a_2 ∧
          a ⊓ a_2 = ⊥ ∧ a ⊔ a_2 = p) ↔
  ∀ q ∈ f.invtSubmodule, q ≤ p → ∃ r ≤ p, r ∈ f.invtSubmodule ∧ q ⊓ r = ⊥ ∧ q ⊔ r = p
Tactic: simp_rw [IsSemisimple, isSemisimpleModule_iff, e.complementedLattice_iff, disjoint_iff,
    ← (OrderIso.Iic _ _).complementedLattice_iff, Iic.complementedLattice_iff, Subtype.forall,
    Subtype.exists, Subtype.mk_le_mk, Sublattice.mk_inf_mk, Sublattice.mk_sup_mk, Subtype.mk.injEq,
    exists_and_left, exists_and_right, invtSubmodule.mk_eq_bot_iff, exists_prop, and_assoc]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Semisimple (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
M₂ : Type u_3
inst_3 : AddCommGroup M₂
inst_4 : Module R M₂
g : End R M₂
e_1 : M ≃ₗ[R] M₂
he : (↑e_1 : M →ₗ[R] M₂) ∘ₗ f = g ∘ₗ (↑e_1 : M →ₗ[R] M₂)
e : LinearEquiv.{u_1, u_1, u_2, u_3} (RingHom.id R[X]) (AEval' f) (AEval' g) :=
  LinearEquiv.ofAEval f (e_1 ≪≫ₗ AEval'.of g) ⋯
⊢ f.IsSemisimple ↔ g.IsSemisimple
have simp_rw : IsSemisimpleModule.{u_1, u_2} R[X] (AEval' f) ↔ IsSemisimpleModule.{u_1, u_3} R[X] (AEval' g)
Tactic: simp_rw [IsSemisimple, isSemisimpleModule_iff,
    (Submodule.orderIsoMapComap e).complementedLattice_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Semisimple (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
M₂ : Type u_3
inst_3 : AddCommGroup M₂
inst_4 : Module R M₂
g : End R M₂
e_1 : M ≃ₗ[R] M₂
he : (↑e_1 : M →ₗ[R] M₂) ∘ₗ f = g ∘ₗ (↑e_1 : M →ₗ[R] M₂)
e : LinearEquiv.{u_1, u_1, u_2, u_3} (RingHom.id R[X]) (AEval' f) (AEval' g) :=
  LinearEquiv.ofAEval f (e_1 ≪≫ₗ AEval'.of g) ⋯
simp_rw : IsSemisimpleModule.{u_1, u_2} R[X] (AEval' f) ↔ IsSemisimpleModule.{u_1, u_3} R[X] (AEval' g)
⊢ f.IsSemisimple ↔ g.IsSemisimple
have simp_rw₁ : ComplementedLattice.{u_2} (Submodule.{u_1, u_2} R[X] (AEval' f)) ↔
  ComplementedLattice.{u_3} (Submodule.{u_1, u_3} R[X] (AEval' g))
Tactic: simp_rw [IsSemisimple, isSemisimpleModule_iff,
    (Submodule.orderIsoMapComap e).complementedLattice_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Semisimple (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
hn : IsNilpotent f
hs : f.IsSemisimple
⊢ f = 0
have have : ∀ (n : ℕ) (h0 : f ^ n = 0), f = 0
Tactic: have ⟨n, h0⟩ := hn
-- Lean 4 proof step from Mathlib.LinearAlgebra.Semisimple (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
hn : IsNilpotent f
hs : f.IsSemisimple
n : ℕ
h0 : f ^ n = 0
⊢ f = 0
have rw : Eq.{u_2 + 1} (α := End R M) ((aeval f : (a : R[X]) → End R M) X : End R M) (0 : End R M)
Tactic: rw [← aeval_X (R := R) f]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Semisimple (hypothesis)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
hn : IsNilpotent f
hs : f.IsSemisimple
n : ℕ
h0 : f ^ n = 0
⊢ Eq.{u_2 + 1} (α := End R M) ((aeval f : (a : R[X]) → End R M) X : End R M) (0 : End R M)
have h0₁ : Eq.{u_2 + 1} (α := End R M) ((aeval f : (a : R[X]) → End R M) (HPow.hPow (α := R[X]) X n) : End R M) (0 : End R M)
Tactic: rw [← aeval_X_pow (R := R) f] at h0
Cleared hypotheses: h0
-- Lean 4 proof step from Mathlib.LinearAlgebra.Semisimple (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
hn : IsNilpotent f
hs : f.IsSemisimple
n : ℕ
h0 : Eq.{u_2 + 1} (α := End R M) ((aeval f : (a : R[X]) → End R M) (HPow.hPow (α := R[X]) X n) : End R M) (0 : End R M)
⊢ Eq.{u_2 + 1} (α := End R M) ((aeval f : (a : R[X]) → End R M) X : End R M) (0 : End R M)
have rw : ∀ (h0 : Membership.mem (γ := Ideal R[X]) (annihilator.{u_1, u_2} R[X] (AEval R M f)) (HPow.hPow (α := R[X]) X n)),
  Membership.mem (γ := Ideal R[X]) (annihilator.{u_1, u_2} R[X] (AEval R M f)) X
Tactic: rw [← RingHom.mem_ker, ← AEval.annihilator_eq_ker_aeval (M := M)] at h0 ⊢
Cleared hypotheses: h0
-- Lean 4 proof step from Mathlib.LinearAlgebra.Semisimple (hypothesis)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
hn : IsNilpotent f
hs : f.IsFinitelySemisimple
p : Submodule R M
hp₁ : p ∈ f.invtSubmodule
hp₂ : Module.Finite.{u_1, u_2} R ↥p
⊢ LinearMap.restrict f hp₁ = 0
have hs₁ : IsSemisimple (LinearMap.restrict f hp₁)
Tactic: specialize hs p hp₁ hp₂
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.LinearAlgebra.Semisimple (hypothesis)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
hn : IsNilpotent f
p : Submodule R M
hp₁ : p ∈ f.invtSubmodule
hp₂ : Module.Finite.{u_1, u_2} R ↥p
hs : IsSemisimple (LinearMap.restrict f hp₁)
⊢ LinearMap.restrict f hp₁ = 0
have hn₁ : IsNilpotent (LinearMap.restrict f hp₁)
Tactic: replace hn : IsNilpotent (f.restrict hp₁) := isNilpotent.restrict hp₁ hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.LinearAlgebra.Semisimple (hypothesis)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
hn : IsNilpotent f
hs : f.IsFinitelySemisimple
⊢ f = 0
have this : ∀ (p : Submodule R M) (hp₁ : p ∈ f.invtSubmodule) (hp₂ : Module.Finite.{u_1, u_2} R ↥p), LinearMap.restrict f hp₁ = 0
Tactic: have (p) (hp₁ : p ∈ f.invtSubmodule) (hp₂ : Module.Finite R p) : f.restrict hp₁ = 0 := by
    specialize hs p hp₁ hp₂
    replace hn : IsNilpotent (f.restrict hp₁) := isNilpotent.restrict hp₁ hn
    exact eq_zero_of_isNilpotent_isSemisimple hn hs