-- Mathlib/RingTheory/Spectrum/Prime/RingHom.lean
theorem exists_maximal_nmem_range_sigmaToPi_of_infinite :
    ∃ (I : Ideal (Π i, R i)) (_ : I.IsMaximal), ⟨I, inferInstance⟩ ∉ Set.range (sigmaToPi R)

Proof state:
ι : Type u_3
R : ι → Type u_2
inst✝² : (i : ι) → CommSemiring (R i)
inst✝¹ : Infinite ι
inst✝ : ∀ (i : ι), Nontrivial (R i)
J : Ideal ((i : ι) → R i) :=
  let __spread.0 := AddMonoidHom.mrange DFinsupp.coeFnAddMonoidHom;
  { toAddSubmonoid := __spread.0, smul_mem' := ⋯ }
I : Ideal ((i : ι) → R i)
max : I.IsMaximal
le : J ≤ I
x✝ : { asIdeal := I, isPrime := ⋯ } ∈ Set.range (sigmaToPi R)
i : ι
p : PrimeSpectrum (R i)
eq : sigmaToPi R ⟨i, p⟩ = { asIdeal := I, isPrime := ⋯ }
this : ⇑(DFinsupp.single i 1) ∉ (sigmaToPi R ⟨i, p⟩).asIdeal
⊢ False

Tactic:
rw [eq] at this

Result:
ι : Type u_3
R : ι → Type u_2
inst✝² : (i : ι) → CommSemiring (R i)
inst✝¹ : Infinite ι
inst✝ : ∀ (i : ι), Nontrivial (R i)
J : Ideal ((i : ι) → R i) :=
  let __spread.0 := AddMonoidHom.mrange DFinsupp.coeFnAddMonoidHom;
  { toAddSubmonoid := __spread.0, smul_mem' := ⋯ }
I : Ideal ((i : ι) → R i)
max : I.IsMaximal
le : J ≤ I
x✝ : { asIdeal := I, isPrime := ⋯ } ∈ Set.range (sigmaToPi R)
i : ι
p : PrimeSpectrum (R i)
eq : sigmaToPi R ⟨i, p⟩ = { asIdeal := I, isPrime := ⋯ }
this : ⇑(DFinsupp.single i 1) ∉ { asIdeal := I, isPrime := ⋯ }.asIdeal
⊢ False

Proof state:
ι : Type u_3
R : ι → Type u_2
inst✝² : (i : ι) → CommSemiring (R i)
inst✝¹ : Infinite ι
inst✝ : ∀ (i : ι), Nontrivial (R i)
⊢ ∃ I, ∃ (x : I.IsMaximal), { asIdeal := I, isPrime := ⋯ } ∉ Set.range (sigmaToPi R)

Tactic:
let J : Ideal (Π i, R i) := { __ := AddMonoidHom.mrange DFinsupp.coeFnAddMonoidHom
  smul_mem' := by
    rintro r _ ⟨x, rfl⟩
    refine ⟨.mk x.support fun i ↦ r i * x i, funext fun i ↦ show dite _ _ _ = _ from ?_⟩
    simp_rw [DFinsupp.coeFnAddMonoidHom]
    refine dite_eq_left_iff.mpr fun h ↦ ?_
    rw [DFinsupp.not_mem_support_iff.mp h, mul_zero] }

Result:
ι : Type u_3
R : ι → Type u_2
inst✝² : (i : ι) → CommSemiring (R i)
inst✝¹ : Infinite ι
inst✝ : ∀ (i : ι), Nontrivial (R i)
J : Ideal ((i : ι) → R i) :=
  let __spread.0 := AddMonoidHom.mrange DFinsupp.coeFnAddMonoidHom;
  { toAddSubmonoid := __spread.0, smul_mem' := ⋯ }
⊢ ∃ I, ∃ (x : I.IsMaximal), { asIdeal := I, isPrime := ⋯ } ∉ Set.range (sigmaToPi R)

Proof state:
case intro
ι : Type u_3
R : ι → Type u_2
inst✝² : (i : ι) → CommSemiring (R i)
inst✝¹ : Infinite ι
inst✝ : ∀ (i : ι), Nontrivial (R i)
r : (i : ι) → R i
x : Π₀ (i : ι), R i
i : ι
h : i ∉ x.support
⊢ 0 = r i * x i

Tactic:
rw [DFinsupp.not_mem_support_iff.mp h, mul_zero]

Result:
no goals

Proof state:
ι : Type u_3
R : ι → Type u_2
inst✝² : (i : ι) → CommSemiring (R i)
inst✝¹ : Infinite ι
inst✝ : ∀ (i : ι), Nontrivial (R i)
J : Ideal ((i : ι) → R i) :=
  let __spread.0 := AddMonoidHom.mrange DFinsupp.coeFnAddMonoidHom;
  { toAddSubmonoid := __spread.0, smul_mem' := ⋯ }
I : Ideal ((i : ι) → R i)
max : I.IsMaximal
le : J ≤ I
x✝ : { asIdeal := I, isPrime := ⋯ } ∈ Set.range (sigmaToPi R)
i : ι
p : PrimeSpectrum (R i)
eq : sigmaToPi R ⟨i, p⟩ = { asIdeal := I, isPrime := ⋯ }
⊢ False

Tactic:
have : ⇑(DFinsupp.single i 1) ∉ (sigmaToPi R ⟨i, p⟩).asIdeal := by
  simpa using p.1.ne_top_iff_one.mp p.2.ne_top

Result:
ι : Type u_3
R : ι → Type u_2
inst✝² : (i : ι) → CommSemiring (R i)
inst✝¹ : Infinite ι
inst✝ : ∀ (i : ι), Nontrivial (R i)
J : Ideal ((i : ι) → R i) :=
  let __spread.0 := AddMonoidHom.mrange DFinsupp.coeFnAddMonoidHom;
  { toAddSubmonoid := __spread.0, smul_mem' := ⋯ }
I : Ideal ((i : ι) → R i)
max : I.IsMaximal
le : J ≤ I
x✝ : { asIdeal := I, isPrime := ⋯ } ∈ Set.range (sigmaToPi R)
i : ι
p : PrimeSpectrum (R i)
eq : sigmaToPi R ⟨i, p⟩ = { asIdeal := I, isPrime := ⋯ }
this : ⇑(DFinsupp.single i 1) ∉ (sigmaToPi R ⟨i, p⟩).asIdeal
⊢ False

Proof state:
ι : Type u_3
R : ι → Type u_2
inst✝² : (i : ι) → CommSemiring (R i)
inst✝¹ : Infinite ι
inst✝ : ∀ (i : ι), Nontrivial (R i)
⊢ ∀ (c : (i : ι) → R i) {x : (i : ι) → R i}, x ∈ __spread✝⁻⁰.carrier → c • x ∈ __spread✝⁻⁰.carrier

Tactic:
rintro r _ ⟨x, rfl⟩

Result:
case intro
ι : Type u_3
R : ι → Type u_2
inst✝² : (i : ι) → CommSemiring (R i)
inst✝¹ : Infinite ι
inst✝ : ∀ (i : ι), Nontrivial (R i)
r : (i : ι) → R i
x : Π₀ (i : ι), R i
⊢ r • DFinsupp.coeFnAddMonoidHom x ∈ __spread✝⁻⁰.carrier

Proof state:
case intro
ι : Type u_3
R : ι → Type u_2
inst✝² : (i : ι) → CommSemiring (R i)
inst✝¹ : Infinite ι
inst✝ : ∀ (i : ι), Nontrivial (R i)
r : (i : ι) → R i
x : Π₀ (i : ι), R i
⊢ r • DFinsupp.coeFnAddMonoidHom x ∈ __spread✝⁻⁰.carrier

Tactic:
refine ⟨.mk x.support fun i ↦ r i * x i, funext fun i ↦ show dite _ _ _ = _ from ?_⟩

Result:
case intro
ι : Type u_3
R : ι → Type u_2
inst✝² : (i : ι) → CommSemiring (R i)
inst✝¹ : Infinite ι
inst✝ : ∀ (i : ι), Nontrivial (R i)
r : (i : ι) → R i
x : Π₀ (i : ι), R i
i : ι
⊢ (if H : i ∈ x.support then (fun i => r ↑i * x ↑i) ⟨i, H⟩ else 0) = (r • DFinsupp.coeFnAddMonoidHom x) i