awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.AssociatedPrime.Localization (goal)
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
R' : Type u_2
inst_1 : CommRing R'
inst_2 : Algebra R R'
hSR' : IsLocalization S R'
M : Type u_3
M' : Type u_4
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup M'
inst_6 : Module R M'
f : M →ₗ[R] M'
inst_7 : IsLocalizedModule S f
inst_8 : Module R' M'
inst_9 : IsScalarTower R R' M'
p : Ideal R'
hp : p.IsPrime
T : Finset R
hT : Eq (α := Ideal R) (Ideal.span (↑T : Set R)) (Ideal.comap (F := R →+* R') (algebraMap R R') p)
m : M
s : ↥S
hx : p = Ideal.radical (colon (M := M') ⊥ {IsLocalizedModule.mk' f m s})
e : (a : ↥T) → ℕ
g : (a : ↥T) → ↥S
hg : ∀ (a : ↥T), g a • (↑a : R) ^ e a • m = 0
r : R
k : ℕ
hk : (r ^ k * (↑(∏ a : ↥T, g a) : R)) • m = 0
h :
  Membership.mem.{u_2, u_2} (α := R') (γ := Ideal R') (colon (M := M') ⊥ {IsLocalizedModule.mk' f m s})
    ((algebraMap R R' : (a : R) → R') (r ^ k * (↑(∏ a : ↥T, g a) : R)) : R')
h₁ :
  Membership.mem (γ := Submodule R' M') ⊥
    (HSMul.hSMul.{u_2, u_4, u_4} (α := R') ((algebraMap R R' : (a : R) → R') (r ^ k * (↑(∏ a : ↥T, g a) : R)) : R')
      (IsLocalizedModule.mk' f m s))
h₂ : Membership.mem (γ := Submodule R' M') ⊥ ((r ^ k * (↑(∏ a : ↥T, g a) : R)) • IsLocalizedModule.mk' f m s)
h₃ : Membership.mem (γ := Submodule R' M') ⊥ (IsLocalizedModule.mk' f ((r ^ k * (↑(∏ a : ↥T, g a) : R)) • m) s)
h₄ : Membership.mem (γ := Submodule R' M') ⊥ (IsLocalizedModule.mk' f 0 s)
⊢ Membership.mem (γ := Ideal R') (colon (M := M') ⊥ {IsLocalizedModule.mk' f m s})
    (HPow.hPow (α := R') (β := ℕ) ((algebraMap R R' : (a : R) → R') (r ^ k * (↑(∏ a : ↥T, g a) : R)) : R') 1)
have h₅ : Membership.mem (γ := Submodule R' M') ⊥ 0
Tactic: simp_rw [pow_one, mem_colon_singleton, algebraMap_smul, ← IsLocalizedModule.mk'_smul,
        hk, IsLocalizedModule.mk'_zero, mem_bot]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.AssociatedPrime.Localization (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
R' : Type u_2
inst_1 : CommRing R'
inst_2 : Algebra R R'
hSR' : IsLocalization S R'
M : Type u_3
M' : Type u_4
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup M'
inst_6 : Module R M'
f : M →ₗ[R] M'
inst_7 : IsLocalizedModule S f
inst_8 : Module R' M'
inst_9 : IsScalarTower R R' M'
p : Ideal R'
hp : p.IsPrime
T : Finset R
hT : Eq (α := Ideal R) (Ideal.span (↑T : Set R)) (Ideal.comap (F := R →+* R') (algebraMap R R') p)
m : M
s : ↥S
hx : p = Ideal.radical (colon (M := M') ⊥ {IsLocalizedModule.mk' f m s})
e : (a : ↥T) → ℕ
g : (a : ↥T) → ↥S
hg : ∀ (a : ↥T), g a • (↑a : R) ^ e a • m = 0
r : R
k : ℕ
hk : (r ^ k * (↑(∏ a : ↥T, g a) : R)) • m = 0
⊢ Membership.mem (γ := Submodule R R) (Ideal.comap (F := R →+* R') (algebraMap R R') p) r
have mem : Membership.mem (γ := Ideal R) (Ideal.comap (F := R →+* R') (algebraMap R R') p) (r ^ k * (↑(∏ a : ↥T, g a) : R))
Tactic: have mem : r ^ k * (∏ a, g a).1 ∈ Ideal.comap (algebraMap R R') p := by
      rw [hx]
      use 1
      simp_rw [pow_one, mem_colon_singleton, algebraMap_smul, ← IsLocalizedModule.mk'_smul,
        hk, IsLocalizedModule.mk'_zero, mem_bot]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.AssociatedPrime.Localization (goal)
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
R' : Type u_2
inst_1 : CommRing R'
inst_2 : Algebra R R'
hSR' : IsLocalization S R'
M : Type u_3
M' : Type u_4
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup M'
inst_6 : Module R M'
f : M →ₗ[R] M'
inst_7 : IsLocalizedModule S f
inst_8 : Module R' M'
inst_9 : IsScalarTower R R' M'
p : Ideal R'
hp : p.IsPrime
T : Finset R
hT : Eq (α := Ideal R) (Ideal.span (↑T : Set R)) (Ideal.comap (F := R →+* R') (algebraMap R R') p)
m : M
s : ↥S
hx : p = Ideal.radical (colon (M := M') ⊥ {IsLocalizedModule.mk' f m s})
e : (a : ↥T) → ℕ
g : (a : ↥T) → ↥S
hg : ∀ (a : ↥T), g a • (↑a : R) ^ e a • m = 0
r : R
k : ℕ
hk : (r ^ k * (↑(∏ a : ↥T, g a) : R)) • m = 0
mem : Membership.mem (γ := Ideal R) (Ideal.comap (F := R →+* R') (algebraMap R R') p) (r ^ k * (↑(∏ a : ↥T, g a) : R))
⊢ Membership.mem (γ := Submodule R R) (Ideal.comap (F := R →+* R') (algebraMap R R') p) r
have refine_2 : HPow.hPow (α := R') ((algebraMap R R' : (a : R) → R') r : R') k ∈ p
Tactic: apply hp.mem_of_pow_mem k
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.AssociatedPrime.Localization (goal)
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
R' : Type u_2
inst_1 : CommRing R'
inst_2 : Algebra R R'
hSR' : IsLocalization S R'
M : Type u_3
M' : Type u_4
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup M'
inst_6 : Module R M'
f : M →ₗ[R] M'
inst_7 : IsLocalizedModule S f
inst_8 : Module R' M'
inst_9 : IsScalarTower R R' M'
p : Ideal R'
hp : p.IsPrime
T : Finset R
hT : Eq (α := Ideal R) (Ideal.span (↑T : Set R)) (Ideal.comap (F := R →+* R') (algebraMap R R') p)
m : M
s : ↥S
hx : p = Ideal.radical (colon (M := M') ⊥ {IsLocalizedModule.mk' f m s})
e : (a : ↥T) → ℕ
g : (a : ↥T) → ↥S
hg : ∀ (a : ↥T), g a • (↑a : R) ^ e a • m = 0
r : R
k : ℕ
hk : (r ^ k * (↑(∏ a : ↥T, g a) : R)) • m = 0
mem : Membership.mem (γ := Ideal R) (Ideal.comap (F := R →+* R') (algebraMap R R') p) (r ^ k * (↑(∏ a : ↥T, g a) : R))
⊢ HPow.hPow (α := R') ((algebraMap R R' : (a : R) → R') r : R') k ∈ p
have refine_2 : Membership.mem (α := R') p ((algebraMap R R' : (a : R) → R') (r ^ k) : R')
Tactic: rw [← map_pow]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.AssociatedPrime.Localization (goal)
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
R' : Type u_2
inst_1 : CommRing R'
inst_2 : Algebra R R'
hSR' : IsLocalization S R'
M : Type u_3
M' : Type u_4
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup M'
inst_6 : Module R M'
f : M →ₗ[R] M'
inst_7 : IsLocalizedModule S f
inst_8 : Module R' M'
inst_9 : IsScalarTower R R' M'
inst_10 : IsNoetherianRing R
⊢ Eq (α := Set (Ideal R'))
    (preimage (β := Ideal R) (Ideal.comap (F := R →+* R') (algebraMap R R')) (associatedPrimes R M))
    (associatedPrimes R' M')
have h : ∀ (p : Ideal R'),
  Membership.mem (γ := Set (Ideal R'))
      (preimage (β := Ideal R) (Ideal.comap (F := R →+* R') (algebraMap R R')) (associatedPrimes R M)) p ↔
    Membership.mem (γ := Set (Ideal R')) (associatedPrimes R' M') p
Tactic: ext p
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.AssociatedPrime.Localization (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsNoetherianRing R
inst_4 : Module.Finite R M
p : Ideal R
hp : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (annihilator R M)) p
⊢ Membership.mem (γ := Set (Ideal R)) (associatedPrimes R M) p
have prime : p.IsPrime
Tactic: have prime := hp.isPrime
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.AssociatedPrime.Localization (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsNoetherianRing R
inst_4 : Module.Finite R M
p : Ideal R
hp : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (annihilator R M)) p
prime : p.IsPrime
Rₚ : Type u_1 := Localization.AtPrime p
⊢ Membership.mem (γ := Set (Ideal R)) (associatedPrimes R M) p
have this : Nontrivial (LocalizedModule p.primeCompl M)
Tactic: have : Nontrivial (LocalizedModule p.primeCompl M) := by
    simpa [← Module.mem_support_iff (p := ⟨p, prime⟩), Module.support_eq_zeroLocus] using hp.le
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.AssociatedPrime.Localization (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsNoetherianRing R
inst_4 : Module.Finite R M
p : Ideal R
hp : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (annihilator R M)) p
prime : p.IsPrime
Rₚ : Type u_1 := Localization.AtPrime p
this : Nontrivial (LocalizedModule p.primeCompl M)
⊢ Membership.mem (γ := Set (Ideal R)) (associatedPrimes R M) p
have rcases : ∀ (q : Ideal Rₚ) (hq : Membership.mem (γ := Set (Ideal Rₚ)) (associatedPrimes Rₚ (LocalizedModule p.primeCompl M)) q),
  Membership.mem (γ := Set (Ideal R)) (associatedPrimes R M) p
Tactic: rcases associatedPrimes.nonempty Rₚ (LocalizedModule p.primeCompl M) with ⟨q, hq⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.AssociatedPrime.Localization (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsNoetherianRing R
inst_4 : Module.Finite R M
p : Ideal R
hp : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (annihilator R M)) p
prime : p.IsPrime
Rₚ : Type u_1 := Localization.AtPrime p
this : Nontrivial (LocalizedModule p.primeCompl M)
q : Ideal Rₚ
hq : Membership.mem (γ := Set (Ideal Rₚ)) (associatedPrimes Rₚ (LocalizedModule p.primeCompl M)) q
⊢ Membership.mem (γ := Set (Ideal R)) (associatedPrimes R M) p
have q_prime : q.IsPrime
Tactic: have q_prime : q.IsPrime := IsAssociatedPrime.isPrime hq
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.AssociatedPrime.Localization (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsNoetherianRing R
inst_4 : Module.Finite R M
p : Ideal R
hp : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (annihilator R M)) p
prime : p.IsPrime
Rₚ : Type u_1 := Localization.AtPrime p
this : Nontrivial (LocalizedModule p.primeCompl M)
q : Ideal Rₚ
hq : Membership.mem (γ := Set (Ideal Rₚ)) (associatedPrimes Rₚ (LocalizedModule p.primeCompl M)) q
q_prime : q.IsPrime
⊢ Membership.mem (γ := Set (Ideal R)) (associatedPrimes R M) p
have hq₁ : Membership.mem (γ := Set (Ideal R)) (associatedPrimes R M) (Ideal.comap (F := R →+* Rₚ) (algebraMap R Rₚ) q)
Tactic: simp only [← preimage_comap_associatedPrimes_eq_associatedPrimes_of_isLocalizedModule p.primeCompl
    Rₚ (LocalizedModule.mkLinearMap p.primeCompl M), Set.mem_preimage] at hq
Cleared hypotheses: hq
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.AssociatedPrime.Localization (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsNoetherianRing R
inst_4 : Module.Finite R M
p : Ideal R
hp : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (annihilator R M)) p
prime : p.IsPrime
Rₚ : Type u_1 := Localization.AtPrime p
this : Nontrivial (LocalizedModule p.primeCompl M)
q : Ideal Rₚ
q_prime : q.IsPrime
hq : Membership.mem (γ := Set (Ideal R)) (associatedPrimes R M) (Ideal.comap (F := R →+* Rₚ) (algebraMap R Rₚ) q)
⊢ Membership.mem (γ := Set (Ideal R)) (associatedPrimes R M) p
have ann_le : LE.le (α := Ideal R) (annihilator R M) (Ideal.comap (F := R →+* Rₚ) (algebraMap R Rₚ) q)
Tactic: have ann_le : Module.annihilator R M ≤ Ideal.comap (algebraMap R Rₚ) q :=
    le_of_eq_of_le Submodule.annihilator_top.symm (IsAssociatedPrime.annihilator_le hq)
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.AssociatedPrime.Localization (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsNoetherianRing R
inst_4 : Module.Finite R M
p : Ideal R
hp : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (annihilator R M)) p
prime : p.IsPrime
Rₚ : Type u_1 := Localization.AtPrime p
this : Nontrivial (LocalizedModule p.primeCompl M)
q : Ideal Rₚ
q_prime : q.IsPrime
hq : Membership.mem (γ := Set (Ideal R)) (associatedPrimes R M) (Ideal.comap (F := R →+* Rₚ) (algebraMap R Rₚ) q)
ann_le : LE.le (α := Ideal R) (annihilator R M) (Ideal.comap (F := R →+* Rₚ) (algebraMap R Rₚ) q)
⊢ Ideal.comap (F := R →+* Rₚ) (algebraMap R Rₚ) q ≤ p
have this₁ : Disjoint (↑p.primeCompl : Set R) (↑(Ideal.under R q) : Set R)
Tactic: have := (IsLocalization.disjoint_under_iff p.primeCompl Rₚ q).mpr q_prime.ne_top
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.AssociatedPrime.Localization (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsNoetherianRing R
inst_4 : Module.Finite R M
p : Ideal R
hp : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (annihilator R M)) p
prime : p.IsPrime
Rₚ : Type u_1 := Localization.AtPrime p
this : Nontrivial (LocalizedModule p.primeCompl M)
q : Ideal Rₚ
q_prime : q.IsPrime
hq : Membership.mem (γ := Set (Ideal R)) (associatedPrimes R M) (Ideal.comap (F := R →+* Rₚ) (algebraMap R Rₚ) q)
ann_le : LE.le (α := Ideal R) (annihilator R M) (Ideal.comap (F := R →+* Rₚ) (algebraMap R Rₚ) q)
⊢ Membership.mem (γ := Set (Ideal R)) (associatedPrimes R M) p
have le : Ideal.comap (F := R →+* Rₚ) (algebraMap R Rₚ) q ≤ p
Tactic: have le : Ideal.comap (algebraMap R Rₚ) q ≤ p := by
    have := (IsLocalization.disjoint_under_iff p.primeCompl Rₚ q).mpr q_prime.ne_top
    simpa only [Ideal.primeCompl, Submonoid.coe_set_mk, Subsemigroup.coe_set_mk,
      Set.disjoint_compl_left_iff_subset] using this
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Basic (goal)
Goal:
ι : Type u_1
R : ι → Type u_5
inst : (i : ι) → Semiring (R i)
r : (i : ι) → R i
⊢ Eq (α := Ideal ((i : ι) → R i)) (pi (R := R) fun (x : ι) ↦ span {r x}) (span {r})
have h : ∀ (x : (i : ι) → R i),
  Membership.mem (γ := Ideal ((i : ι) → R i)) (pi (R := R) fun (x : ι) ↦ span {r x}) x ↔
    Membership.mem (γ := Ideal ((i : ι) → R i)) (span {r}) x
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Basic (goal)
Goal:
ι : Type u_1
R : ι → Type u_5
inst : (i : ι) → Semiring (R i)
r x : (i : ι) → R i
⊢ Membership.mem (γ := Ideal ((i : ι) → R i)) (pi (R := R) fun (x : ι) ↦ span {r x}) x ↔
    Membership.mem (γ := Ideal ((i : ι) → R i)) (span {r}) x
have h : (∀ (i : ι), Membership.mem (γ := Ideal (R i)) (span {r i}) (x i)) ↔
  Membership.mem (γ := Ideal ((i : ι) → R i)) (span {r}) x
Tactic: simp_rw [mem_pi, mem_span_singleton', funext_iff, Classical.skolem, Pi.mul_def]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Basic (goal)
Goal:
ι : Type u_1
R : ι → Type u_5
inst : (i : ι) → Semiring (R i)
r x : (i : ι) → R i
h :
  (∀ (i : ι), Membership.mem (γ := Ideal (R i)) (span {r i}) (x i)) ↔
    Membership.mem (γ := Ideal ((i : ι) → R i)) (span {r}) x
⊢ Membership.mem (γ := Ideal ((i : ι) → R i)) (pi (R := R) fun (x : ι) ↦ span {r x}) x ↔
    Membership.mem (γ := Ideal ((i : ι) → R i)) (span {r}) x
have h₁ : (∀ (i : ι), ∃ (a : R i), a * r i = x i) ↔ ∃ (a : (i : ι) → R i), a * r = x
Tactic: simp_rw [mem_pi, mem_span_singleton', funext_iff, Classical.skolem, Pi.mul_def]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Basic (goal)
Goal:
ι : Type u_1
R : ι → Type u_5
inst : (i : ι) → Semiring (R i)
r x : (i : ι) → R i
h :
  (∀ (i : ι), Membership.mem (γ := Ideal (R i)) (span {r i}) (x i)) ↔
    Membership.mem (γ := Ideal ((i : ι) → R i)) (span {r}) x
h₁ : (∀ (i : ι), ∃ (a : R i), a * r i = x i) ↔ ∃ (a : (i : ι) → R i), a * r = x
⊢ Membership.mem (γ := Ideal ((i : ι) → R i)) (pi (R := R) fun (x : ι) ↦ span {r x}) x ↔
    Membership.mem (γ := Ideal ((i : ι) → R i)) (span {r}) x
have h₂ : (∀ (i : ι), ∃ (a : R i), a * r i = x i) ↔ ∃ (a : (i : ι) → R i), ∀ (x_1 : ι), (a * r) x_1 = x x_1
Tactic: simp_rw [mem_pi, mem_span_singleton', funext_iff, Classical.skolem, Pi.mul_def]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Basic (goal)
Goal:
ι : Type u_1
R : ι → Type u_5
inst : (i : ι) → Semiring (R i)
r x : (i : ι) → R i
h :
  (∀ (i : ι), Membership.mem (γ := Ideal (R i)) (span {r i}) (x i)) ↔
    Membership.mem (γ := Ideal ((i : ι) → R i)) (span {r}) x
h₁ : (∀ (i : ι), ∃ (a : R i), a * r i = x i) ↔ ∃ (a : (i : ι) → R i), a * r = x
h₂ : (∀ (i : ι), ∃ (a : R i), a * r i = x i) ↔ ∃ (a : (i : ι) → R i), ∀ (x_1 : ι), (a * r) x_1 = x x_1
⊢ Membership.mem (γ := Ideal ((i : ι) → R i)) (pi (R := R) fun (x : ι) ↦ span {r x}) x ↔
    Membership.mem (γ := Ideal ((i : ι) → R i)) (span {r}) x
have h₃ : (∃ (f : (x : ι) → R x), ∀ (x_1 : ι), f x_1 * r x_1 = x x_1) ↔ ∃ (a : (i : ι) → R i), ∀ (x_1 : ι), (a * r) x_1 = x x_1
Tactic: simp_rw [mem_pi, mem_span_singleton', funext_iff, Classical.skolem, Pi.mul_def]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Basic (goal)
Goal:
ι : Type u_1
R : ι → Type u_5
inst : (i : ι) → Semiring (R i)
I : (i : ι) → Ideal (R i)
inst_1 : DecidableEq ι
i : ι
r : R i
hr : r ∈ I i
j : ι
⊢ Pi.single (M := R) i r j ∈ I j
have inl : Pi.single (M := R) i r i ∈ I i
Tactic: obtain rfl | ne := eq_or_ne i j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Basic (goal)
Goal:
ι : Type u_1
R : ι → Type u_5
inst : (i : ι) → Semiring (R i)
I : (i : ι) → Ideal (R i)
inst_1 : DecidableEq ι
i : ι
r : R i
hr : r ∈ I i
j : ι
inl : Pi.single (M := R) i r i ∈ I i
⊢ Pi.single (M := R) i r j ∈ I j
have inr : ∀ (ne : i ≠ j), Pi.single (M := R) i r j ∈ I j
Tactic: obtain rfl | ne := eq_or_ne i j
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Basic (goal)
Goal:
α : Type u_6
inst : Semiring α
I : Ideal α
a b : α
m n k : ℕ
ha : a ^ m ∈ I
hb : b ^ n ∈ I
hk : m + n ≤ k + 1
hab : Commute a b
⊢ (a + b) ^ k ∈ I
have simp_rw : ∑ x ∈ Finset.range (k + 1), (↑(k.choose x) : α) * (a ^ x * b ^ (k - x)) ∈ I
Tactic: simp_rw [hab.add_pow, ← Nat.cast_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Basic (goal)
Goal:
α : Type u_6
inst : Semiring α
I : Ideal α
a b : α
m n k : ℕ
ha : a ^ m ∈ I
hb : b ^ n ∈ I
hk : m + n ≤ k + 1
hab : Commute a b
⊢ ∑ x ∈ Finset.range (k + 1), (↑(k.choose x) : α) * (a ^ x * b ^ (k - x)) ∈ I
have apply : ∀ c ∈ Finset.range (k + 1), (↑(k.choose c) : α) * (a ^ c * b ^ (k - c)) ∈ I
Tactic: apply I.sum_mem
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Basic (goal)
Goal:
α : Type u_6
inst : Semiring α
I : Ideal α
a b : α
m n k : ℕ
ha : a ^ m ∈ I
hb : b ^ n ∈ I
hk : m + n ≤ k + 1
hab : Commute a b
c : ℕ
h : c ∈ Finset.range (k + 1)
⊢ (↑(k.choose c) : α) * (a ^ c * b ^ (k - c)) ∈ I
have a₁ : a ^ c * b ^ (k - c) ∈ I
Tactic: apply mul_mem_left
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Basic (goal)
Goal:
α : Type u_6
inst : Semiring α
I : Ideal α
a b : α
m n k : ℕ
ha : a ^ m ∈ I
hb : b ^ n ∈ I
hk : m + n ≤ k + 1
hab : Commute a b
c : ℕ
h : c ∈ Finset.range (k + 1)
⊢ a ^ c * b ^ (k - c) ∈ I
have pos : ∀ (h : m ≤ c), a ^ c * b ^ (k - c) ∈ I
Tactic: by_cases h : m ≤ c
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Basic (goal)
Goal:
α : Type u_6
inst : Semiring α
I : Ideal α
a b : α
m n k : ℕ
ha : a ^ m ∈ I
hb : b ^ n ∈ I
hk : m + n ≤ k + 1
hab : Commute a b
c : ℕ
h : c ∈ Finset.range (k + 1)
pos : ∀ (h : m ≤ c), a ^ c * b ^ (k - c) ∈ I
⊢ a ^ c * b ^ (k - c) ∈ I
have neg : ∀ (h : ¬m ≤ c), a ^ c * b ^ (k - c) ∈ I
Tactic: by_cases h : m ≤ c
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Basic (goal)
Goal:
α : Type u_6
inst : Semiring α
I : Ideal α
a b : α
m n k : ℕ
ha : a ^ m ∈ I
hb : b ^ n ∈ I
hk : m + n ≤ k + 1
hab : Commute a b
c : ℕ
h_1 : c ∈ Finset.range (k + 1)
h : m ≤ c
⊢ a ^ c * b ^ (k - c) ∈ I
have pos : b ^ (k - c) * a ^ c ∈ I
Tactic: rw [hab.pow_pow]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Basic (goal)
Goal:
α : Type u_6
inst : Semiring α
I : Ideal α
a b : α
m n k : ℕ
ha : a ^ m ∈ I
hb : b ^ n ∈ I
hk : m + n ≤ k + 1
hab : Commute a b
c : ℕ
h_1 : c ∈ Finset.range (k + 1)
h : ¬m ≤ c
⊢ a ^ c * b ^ (k - c) ∈ I
have neg : n ≤ k - c
Tactic: refine I.mul_mem_left _ (I.pow_mem_of_pow_mem hb ?_)
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Basic (goal)
Goal:
α : Type u_6
inst : Semiring α
I : Ideal α
a b : α
m n : ℕ
ha : a ^ m ∈ I
hb : b ^ n ∈ I
hab : Commute a b
⊢ m + n ≤ m + n - 1 + 1
have rw : m + n - 1 ≤ m + n - 1
Tactic: rw [← Nat.sub_le_iff_le_add]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Basic (goal)
Goal:
α : Type u_2
inst : CommSemiring α
inst_1 : DecidableEq α
s : Multiset α
n : ℕ
⊢ Membership.mem (γ := Ideal α) (span (↑(Multiset.toFinset (Multiset.map (fun (x : α) ↦ x ^ (n + 1)) s)) : Set α))
    (s.sum ^ (s.card * n + 1))
have cons : ∀ (a : α) (s : Multiset α)
  (hs :
    Membership.mem (γ := Ideal α) (span (↑(Multiset.toFinset (Multiset.map (fun (x : α) ↦ x ^ (n + 1)) s)) : Set α))
      (s.sum ^ (s.card * n + 1))),
  Membership.mem (γ := Ideal α)
    (span (↑(Multiset.toFinset (Multiset.map (fun (x : α) ↦ x ^ (n + 1)) (a ::ₘ s))) : Set α))
    ((a ::ₘ s).sum ^ ((a ::ₘ s).card * n + 1))
Tactic: induction s using Multiset.induction_on with
  | empty => simp
  | cons a s hs => ?_
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Basic (goal)
Goal:
α : Type u_2
inst : CommSemiring α
inst_1 : DecidableEq α
n : ℕ
a : α
s : Multiset α
hs :
  Membership.mem (γ := Ideal α) (span (↑(Multiset.toFinset (Multiset.map (fun (x : α) ↦ x ^ (n + 1)) s)) : Set α))
    (s.sum ^ (s.card * n + 1))
⊢ Membership.mem (γ := Ideal α)
    (span (↑(Multiset.toFinset (Multiset.map (fun (x : α) ↦ x ^ (n + 1)) (a ::ₘ s))) : Set α))
    ((a ::ₘ s).sum ^ ((a ::ₘ s).card * n + 1))
have cons : Membership.mem (γ := Ideal α)
  (span (insert (a ^ (n + 1)) (↑(Multiset.toFinset (Multiset.map (fun (x : α) ↦ x ^ (n + 1)) s)) : Set α)))
  (∑ m ∈ Finset.range ((s.card + 1) * n + 1 + 1),
    a ^ m * s.sum ^ ((s.card + 1) * n + 1 - m) * (↑(((s.card + 1) * n + 1).choose m) : α))
Tactic: simp only [Finset.coe_insert, Multiset.map_cons, Multiset.toFinset_cons, Multiset.sum_cons,
    Multiset.card_cons, add_pow]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Basic (goal)
Goal:
α : Type u_2
inst : CommSemiring α
inst_1 : DecidableEq α
n : ℕ
a : α
s : Multiset α
hs :
  Membership.mem (γ := Ideal α) (span (↑(Multiset.toFinset (Multiset.map (fun (x : α) ↦ x ^ (n + 1)) s)) : Set α))
    (s.sum ^ (s.card * n + 1))
⊢ Membership.mem (γ := Ideal α)
    (span (insert (a ^ (n + 1)) (↑(Multiset.toFinset (Multiset.map (fun (x : α) ↦ x ^ (n + 1)) s)) : Set α)))
    (∑ m ∈ Finset.range ((s.card + 1) * n + 1 + 1),
      a ^ m * s.sum ^ ((s.card + 1) * n + 1 - m) * (↑(((s.card + 1) * n + 1).choose m) : α))
have cons : ∀ c ∈ Finset.range ((s.card + 1) * n + 1 + 1),
  Membership.mem (γ := Submodule α α)
    (span (insert (a ^ (n + 1)) (↑(Multiset.toFinset (Multiset.map (fun (x : α) ↦ x ^ (n + 1)) s)) : Set α)))
    (a ^ c * s.sum ^ ((s.card + 1) * n + 1 - c) * (↑(((s.card + 1) * n + 1).choose c) : α))
Tactic: refine Submodule.sum_mem _ ?_
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Basic (goal)
Goal:
α : Type u_2
inst : CommSemiring α
inst_1 : DecidableEq α
n : ℕ
a : α
s : Multiset α
hs :
  Membership.mem (γ := Ideal α) (span (↑(Multiset.toFinset (Multiset.map (fun (x : α) ↦ x ^ (n + 1)) s)) : Set α))
    (s.sum ^ (s.card * n + 1))
c : ℕ
_hc : c ∈ Finset.range ((s.card + 1) * n + 1 + 1)
⊢ Membership.mem (γ := Submodule α α)
    (span (insert (a ^ (n + 1)) (↑(Multiset.toFinset (Multiset.map (fun (x : α) ↦ x ^ (n + 1)) s)) : Set α)))
    (a ^ c * s.sum ^ ((s.card + 1) * n + 1 - c) * (↑(((s.card + 1) * n + 1).choose c) : α))
have cons : ∃ (a_1 : α) (z : α),
  Membership.mem (γ := Ideal α) (span (↑(Multiset.toFinset (Multiset.map (fun (x : α) ↦ x ^ (n + 1)) s)) : Set α)) z ∧
    a ^ c * s.sum ^ ((s.card + 1) * n + 1 - c) * (↑(((s.card + 1) * n + 1).choose c) : α) = a_1 * a ^ (n + 1) + z
Tactic: rw [mem_span_insert]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Basic (goal)
Goal:
α : Type u_2
inst : CommSemiring α
inst_1 : DecidableEq α
n : ℕ
a : α
s : Multiset α
hs :
  Membership.mem (γ := Ideal α) (span (↑(Multiset.toFinset (Multiset.map (fun (x : α) ↦ x ^ (n + 1)) s)) : Set α))
    (s.sum ^ (s.card * n + 1))
c : ℕ
_hc : c ∈ Finset.range ((s.card + 1) * n + 1 + 1)
⊢ ∃ (a_1 : α) (z : α),
    Membership.mem (γ := Ideal α) (span (↑(Multiset.toFinset (Multiset.map (fun (x : α) ↦ x ^ (n + 1)) s)) : Set α)) z ∧
      a ^ c * s.sum ^ ((s.card + 1) * n + 1 - c) * (↑(((s.card + 1) * n + 1).choose c) : α) = a_1 * a ^ (n + 1) + z
have pos : ∀ (h : n + 1 ≤ c),
  ∃ (a_1 : α) (z : α),
    Membership.mem (γ := Ideal α) (span (↑(Multiset.toFinset (Multiset.map (fun (x : α) ↦ x ^ (n + 1)) s)) : Set α)) z ∧
      a ^ c * s.sum ^ ((s.card + 1) * n + 1 - c) * (↑(((s.card + 1) * n + 1).choose c) : α) = a_1 * a ^ (n + 1) + z
Tactic: by_cases! h : n + 1 ≤ c