awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial
Goal:
R : Type u_2
inst : CommRing R
σ : Type u_1
U : Set (PrimeSpectrum (MvPolynomial σ R))
hU : IsOpen U
obtain :
  ∀ (S : Set (Set (PrimeSpectrum (MvPolynomial σ R))))
    (hS : S ⊆ Set.range fun (r : MvPolynomial σ R) ↦ (↑(basicOpen r) : Set (PrimeSpectrum (MvPolynomial σ R))))
    (hU : IsOpen (⋃₀ S)), IsOpen (comap C '' ⋃₀ S)
⊢ IsOpen (comap C '' U)

Tactic:
obtain ⟨S, hS, rfl⟩ := isTopologicalBasis_basic_opens.open_eq_sUnion hU

Premises used: TopologicalSpace.IsTopologicalBasis.open_eq_sUnion, PrimeSpectrum.isTopologicalBasis_basic_opens, rfl
-- Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial
Goal:
R : Type u_2
inst : CommRing R
σ : Type u_1
S : Set (Set (PrimeSpectrum (MvPolynomial σ R)))
hS : S ⊆ Set.range fun (r : MvPolynomial σ R) ↦ (↑(basicOpen r) : Set (PrimeSpectrum (MvPolynomial σ R)))
hU : IsOpen (⋃₀ S)
rw : IsOpen (⋃₀ (Set.image (comap C) '' S))
⊢ IsOpen (comap C '' ⋃₀ S)

Tactic:
rw [Set.image_sUnion]

Premises used: Set.image_sUnion
-- Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial
Goal:
R : Type u_2
inst : CommRing R
σ : Type u_1
S : Set (Set (PrimeSpectrum (MvPolynomial σ R)))
hS : S ⊆ Set.range fun (r : MvPolynomial σ R) ↦ (↑(basicOpen r) : Set (PrimeSpectrum (MvPolynomial σ R)))
hU : IsOpen (⋃₀ S)
h : ∀ t ∈ Set.image (comap C) '' S, IsOpen t
⊢ IsOpen (⋃₀ (Set.image (comap C) '' S))

Tactic:
apply isOpen_sUnion

Premises used: isOpen_sUnion
-- Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial
Goal:
R : Type u_2
inst : CommRing R
σ : Type u_1
S : Set (Set (PrimeSpectrum (MvPolynomial σ R)))
hS : S ⊆ Set.range fun (r : MvPolynomial σ R) ↦ (↑(basicOpen r) : Set (PrimeSpectrum (MvPolynomial σ R)))
hU : IsOpen (⋃₀ S)
t : Set (PrimeSpectrum (MvPolynomial σ R))
ht : t ∈ S
h :
  ∀ (r : MvPolynomial σ R)
    (ht : (fun (r : MvPolynomial σ R) ↦ (↑(basicOpen r) : Set (PrimeSpectrum (MvPolynomial σ R)))) r ∈ S),
    IsOpen.{u_2} (X := PrimeSpectrum R)
      (Set.image (α := PrimeSpectrum (MvPolynomial σ R)) (comap C)
        ((fun (r : MvPolynomial σ R) ↦ (↑(basicOpen r) : Set (PrimeSpectrum (MvPolynomial σ R)))) r))
⊢ IsOpen (comap C '' t)

Tactic:
obtain ⟨r, rfl⟩ := hS ht

Premises used: rfl
-- Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial
Goal:
R : Type u_2
inst : CommRing R
σ : Type u_1
S : Set (Set (PrimeSpectrum (MvPolynomial σ R)))
hS : S ⊆ Set.range fun (r : MvPolynomial σ R) ↦ (↑(basicOpen r) : Set (PrimeSpectrum (MvPolynomial σ R)))
hU : IsOpen (⋃₀ S)
r : MvPolynomial σ R
ht : (fun (r : MvPolynomial σ R) ↦ (↑(basicOpen r) : Set (PrimeSpectrum (MvPolynomial σ R)))) r ∈ S
h : IsOpen.{u_2} (X := PrimeSpectrum R) (zeroLocus (Set.range fun (m : σ →₀ ℕ) ↦ coeff m r))ᶜ
⊢ IsOpen.{u_2} (X := PrimeSpectrum R)
    (Set.image (α := PrimeSpectrum (MvPolynomial σ R)) (comap C)
      ((fun (r : MvPolynomial σ R) ↦ (↑(basicOpen r) : Set (PrimeSpectrum (MvPolynomial σ R)))) r))

Tactic:
simp only [image_comap_C_basicOpen]

Premises used: MvPolynomial.image_comap_C_basicOpen
-- Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial
Goal:
R : Type u_2
inst : CommRing R
σ : Type u_1
S : Set (Set (PrimeSpectrum (MvPolynomial σ R)))
hS : S ⊆ Set.range fun (r : MvPolynomial σ R) ↦ (↑(basicOpen r) : Set (PrimeSpectrum (MvPolynomial σ R)))
hU : IsOpen (⋃₀ S)
r : MvPolynomial σ R
ht : (fun (r : MvPolynomial σ R) ↦ (↑(basicOpen r) : Set (PrimeSpectrum (MvPolynomial σ R)))) r ∈ S
⊢ IsOpen.{u_2} (X := PrimeSpectrum R) (zeroLocus (Set.range fun (m : σ →₀ ℕ) ↦ coeff m r))ᶜ

Tactic:
(isClosed_zeroLocus _).isOpen_compl

Premises used: IsClosed.isOpen_compl
-- Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial
Goal:
R : Type u_2
inst : CommRing R
σ : Type u_1
S : Set (Set (PrimeSpectrum (MvPolynomial σ R)))
hS : S ⊆ Set.range fun (r : MvPolynomial σ R) ↦ (↑(basicOpen r) : Set (PrimeSpectrum (MvPolynomial σ R)))
hU : IsOpen (⋃₀ S)
r : MvPolynomial σ R
ht : (fun (r : MvPolynomial σ R) ↦ (↑(basicOpen r) : Set (PrimeSpectrum (MvPolynomial σ R)))) r ∈ S
⊢ IsOpen.{u_2} (X := PrimeSpectrum R) (zeroLocus (Set.range fun (m : σ →₀ ℕ) ↦ coeff m r))ᶜ

Tactic:
exact (isClosed_zeroLocus _).isOpen_compl

Premises used: IsClosed.isOpen_compl
-- Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial
Goal:
R : Type u_2
inst : CommRing R
σ : Type u_1
x : PrimeSpectrum R
⊢ ∃ (a : PrimeSpectrum (MvPolynomial σ R)), comap C a = x

Tactic:
⟨comap (eval₂Hom (.id _) 0) x, ?_⟩

Premises used: MvPolynomial.eval₂Hom, Exists.intro, PrimeSpectrum.comap, OfNat.ofNat, RingHom.id
-- Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial
Goal:
R : Type u_2
inst : CommRing R
σ : Type u_1
x : PrimeSpectrum R
refine : comap (S := MvPolynomial σ R) C (comap (eval₂Hom (RingHom.id R) 0) x) = x
⊢ ∃ (a : PrimeSpectrum (MvPolynomial σ R)), comap C a = x

Tactic:
refine ⟨comap (eval₂Hom (.id _) 0) x, ?_⟩
-- Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial
Goal:
R : Type u_2
inst : CommRing R
σ : Type u_1
x : PrimeSpectrum R
a :
  ∀ (x : R),
    Eq (α := R) ((RingHom.comp (β := MvPolynomial σ R) (eval₂Hom (RingHom.id R) 0) C : (a : R) → R) x : R)
      ((RingHom.id R : (a : R) → R) x : R)
⊢ Eq (α := R →+* R) (RingHom.comp (β := MvPolynomial σ R) (eval₂Hom (RingHom.id R) 0) C) (RingHom.id R)

Tactic:
ext
-- Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial
Goal:
R : Type u_2
inst : CommRing R
σ : Type u_1
x : PrimeSpectrum R
x_1 : R
⊢ Eq (α := R) ((RingHom.comp (β := MvPolynomial σ R) (eval₂Hom (RingHom.id R) 0) C : (a : R) → R) x_1 : R)
    ((RingHom.id R : (a : R) → R) x_1 : R)

Tactic:
simp
-- Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial
Goal:
R : Type u_2
inst : CommRing R
σ : Type u_1
x : PrimeSpectrum R
rw : comap (RingHom.comp (β := MvPolynomial σ R) (eval₂Hom (RingHom.id R) 0) C) x = x
rw₁ : comap (RingHom.id R) x = x
rw₂ rw₃ : (fun (x : PrimeSpectrum R) ↦ x) x = x
⊢ comap (S := MvPolynomial σ R) C (comap (eval₂Hom (RingHom.id R) 0) x) = x

Tactic:
rw [← comap_comp_apply, (show (eval₂Hom (.id _) 0).comp C = .id R by ext; simp),
    comap_id]

Premises used: PrimeSpectrum.comap_comp_apply, PrimeSpectrum.comap_id
-- Module: Mathlib.RingTheory.Spectrum.Prime.RingHom
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
y : PrimeSpectrum S
⊢ (comap f y).asIdeal = Ideal.comap f y.asIdeal

Tactic:
rfl

Premises used: Ideal.comap, rfl
-- Module: Mathlib.RingTheory.Spectrum.Prime.RingHom
Goal:
R : Type u
inst : CommSemiring R
⊢ Eq (α := (p : PrimeSpectrum R) → PrimeSpectrum R) (comap (RingHom.id R)) fun (x : PrimeSpectrum R) ↦ x

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.preimage, Ideal.comap, PrimeSpectrum.comap, rfl
-- Module: Mathlib.RingTheory.Spectrum.Prime.RingHom
Goal:
R : Type u
S : Type v
S' : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : CommSemiring S'
f : R →+* S
g : S →+* S'
⊢ comap (g.comp f) = comap f ∘ comap g

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.preimage, Ideal.comap, PrimeSpectrum.comap, rfl
-- Module: Mathlib.RingTheory.Spectrum.Prime.RingHom
Goal:
R : Type u
S : Type v
S' : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : CommSemiring S'
f : R →+* S
g : S →+* S'
x : PrimeSpectrum S'
⊢ comap (g.comp f) x = comap f (comap g x)

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.preimage, Ideal.comap, PrimeSpectrum.comap, rfl
-- Module: Mathlib.RingTheory.Spectrum.Prime.RingHom
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
s : Set R
h :
  ∀ (x : PrimeSpectrum S),
    x ∈ comap f ⁻¹' zeroLocus s ↔ Membership.mem (γ := Set (PrimeSpectrum S)) (zeroLocus ((⇑f : (a : R) → S) '' s)) x
⊢ comap f ⁻¹' zeroLocus s = zeroLocus ((⇑f : (a : R) → S) '' s)

Tactic:
ext x
-- Module: Mathlib.RingTheory.Spectrum.Prime.RingHom
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
s : Set R
x : PrimeSpectrum S
⊢ x ∈ comap f ⁻¹' zeroLocus s ↔ Membership.mem (γ := Set (PrimeSpectrum S)) (zeroLocus ((⇑f : (a : R) → S) '' s)) x

Tactic:
simp [mem_zeroLocus, Set.image_subset_iff, Set.mem_preimage, mem_zeroLocus]

Premises used: PrimeSpectrum.mem_zeroLocus, Set.image_subset_iff, Set.mem_preimage
-- Module: Mathlib.RingTheory.Spectrum.Prime.RingHom
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
s : Set R
⊢ comap f ⁻¹' zeroLocus s = zeroLocus ((⇑f : (a : R) → S) '' s)

Tactic:
preimage_comap_zeroLocus_aux f s

Premises used: PrimeSpectrum.preimage_comap_zeroLocus_aux
-- Module: Mathlib.RingTheory.Spectrum.Prime.RingHom
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
hf : Function.Surjective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
⊢ Function.Injective (comap f)

Tactic:
fun x y h =>
  PrimeSpectrum.ext
    (Ideal.comap_injective_of_surjective f hf
      (congr_arg PrimeSpectrum.asIdeal h : (comap f x).asIdeal = (comap f y).asIdeal))

Premises used: PrimeSpectrum.ext, congr_arg, Function.Injective, PrimeSpectrum.asIdeal, Ideal.comap_injective_of_surjective
-- Module: Mathlib.RingTheory.Spectrum.Prime.RingHom
Goal:
R : Type u
S : Type v
S' : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : CommSemiring S'
f : R →+* S
e : R ≃+* S
x : PrimeSpectrum R
rw : comap (RingHom.id R) x = x
⊢ comap e.toRingHom (comap e.symm.toRingHom x) = x

Tactic:
rw [← comap_comp_apply, RingEquiv.toRingHom_eq_coe,
      RingEquiv.toRingHom_eq_coe, RingEquiv.symm_comp]

Premises used: PrimeSpectrum.comap_comp_apply, RingEquiv.toRingHom_eq_coe, RingEquiv.symm_comp
-- Module: Mathlib.RingTheory.Spectrum.Prime.RingHom
Goal:
R : Type u
S : Type v
S' : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : CommSemiring S'
f : R →+* S
e : R ≃+* S
x : PrimeSpectrum R
⊢ comap (RingHom.id R) x = x

Tactic:
rfl
-- Module: Mathlib.RingTheory.Spectrum.Prime.RingHom
Goal:
R : Type u
S : Type v
S' : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : CommSemiring S'
f : R →+* S
e : R ≃+* S
x : PrimeSpectrum S
⊢ comap (RingHom.id S) x = x

Tactic:
rfl
-- Module: Mathlib.RingTheory.Spectrum.Prime.RingHom
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
e : R ≃+* S
⊢ (comapEquiv e).symm = comapEquiv e.symm

Tactic:
rfl

Premises used: PrimeSpectrum.comapEquiv, RelIso.symm, OrderIso.symm, PrimeSpectrum.comap, Equiv.symm, RingEquiv.symm, rfl
-- Module: Mathlib.RingTheory.Spectrum.Prime.RingHom
Goal:
ι : Type u_3
R : ι → Type u_2
inst : (i : ι) → CommSemiring (R i)
i : ι
p : PrimeSpectrum (R i)
⊢ Eq (α := PrimeSpectrum ((i : ι) → R i)) (sigmaToPi R (Sigma.mk (β := fun (i : ι) ↦ PrimeSpectrum (R i)) i p))
    (comap (Pi.evalRingHom R i) p)

Tactic:
rfl

Premises used: PrimeSpectrum.sigmaToPi, rfl
-- Module: Mathlib.RingTheory.Spectrum.Prime.RingHom
Goal:
ι : Type u_3
R : ι → Type u_2
inst : (i : ι) → CommSemiring (R i)
x x_1 : (i : ι) × PrimeSpectrum (R i)
i : ι
p : PrimeSpectrum (R i)
j : ι
q : PrimeSpectrum (R j)
eq :
  Eq (α := PrimeSpectrum ((i : ι) → R i)) (sigmaToPi R (Sigma.mk (β := fun (i : ι) ↦ PrimeSpectrum (R i)) i p))
    (sigmaToPi R (Sigma.mk (β := fun (i : ι) ↦ PrimeSpectrum (R i)) j q))
inl :
  ∀ (q : PrimeSpectrum (R i))
    (eq :
      Eq (α := PrimeSpectrum ((i : ι) → R i)) (sigmaToPi R (Sigma.mk (β := fun (i : ι) ↦ PrimeSpectrum (R i)) i p))
        (sigmaToPi R (Sigma.mk (β := fun (i : ι) ↦ PrimeSpectrum (R i)) i q))),
    Eq (α := (i : ι) × PrimeSpectrum (R i)) (Sigma.mk (β := fun (i : ι) ↦ PrimeSpectrum (R i)) i p)
      (Sigma.mk (β := fun (i : ι) ↦ PrimeSpectrum (R i)) i q)
inr :
  ∀ (ne : i ≠ j),
    Eq (α := (i : ι) × PrimeSpectrum (R i)) (Sigma.mk (β := fun (i : ι) ↦ PrimeSpectrum (R i)) i p)
      (Sigma.mk (β := fun (i : ι) ↦ PrimeSpectrum (R i)) j q)
⊢ Eq (α := (i : ι) × PrimeSpectrum (R i)) (Sigma.mk (β := fun (i : ι) ↦ PrimeSpectrum (R i)) i p)
    (Sigma.mk (β := fun (i : ι) ↦ PrimeSpectrum (R i)) j q)

Tactic:
obtain rfl | ne := eq_or_ne i j

Premises used: eq_or_ne, rfl
-- Module: Mathlib.RingTheory.Spectrum.Prime.RingHom
Goal:
ι : Type u_3
R : ι → Type u_2
inst : (i : ι) → CommSemiring (R i)
x x_1 : (i : ι) × PrimeSpectrum (R i)
i : ι
p q : PrimeSpectrum (R i)
eq :
  Eq (α := PrimeSpectrum ((i : ι) → R i)) (sigmaToPi R (Sigma.mk (β := fun (i : ι) ↦ PrimeSpectrum (R i)) i p))
    (sigmaToPi R (Sigma.mk (β := fun (i : ι) ↦ PrimeSpectrum (R i)) i q))
inl : p = q
⊢ Eq (α := (i : ι) × PrimeSpectrum (R i)) (Sigma.mk (β := fun (i : ι) ↦ PrimeSpectrum (R i)) i p)
    (Sigma.mk (β := fun (i : ι) ↦ PrimeSpectrum (R i)) i q)

Tactic:
congr
-- Module: Mathlib.RingTheory.Spectrum.Prime.RingHom
Goal:
ι : Type u_3
R : ι → Type u_2
inst : (i : ι) → CommSemiring (R i)
x x_1 : (i : ι) × PrimeSpectrum (R i)
i : ι
p q : PrimeSpectrum (R i)
eq :
  Eq (α := PrimeSpectrum ((i : ι) → R i)) (sigmaToPi R (Sigma.mk (β := fun (i : ι) ↦ PrimeSpectrum (R i)) i p))
    (sigmaToPi R (Sigma.mk (β := fun (i : ι) ↦ PrimeSpectrum (R i)) i q))
inl : ∀ (x : R i), x ∈ p.asIdeal ↔ x ∈ q.asIdeal
⊢ p = q

Tactic:
ext x
-- Module: Mathlib.RingTheory.Spectrum.Prime.RingHom
Goal:
ι : Type u_3
R : ι → Type u_2
inst : (i : ι) → CommSemiring (R i)
x_1 x_2 : (i : ι) × PrimeSpectrum (R i)
i : ι
p q : PrimeSpectrum (R i)
eq :
  Eq (α := PrimeSpectrum ((i : ι) → R i)) (sigmaToPi R (Sigma.mk (β := fun (i : ι) ↦ PrimeSpectrum (R i)) i p))
    (sigmaToPi R (Sigma.mk (β := fun (i : ι) ↦ PrimeSpectrum (R i)) i q))
x : R i
⊢ x ∈ p.asIdeal ↔ x ∈ q.asIdeal

Tactic:
simpa using congr_arg (Function.update (0 : ∀ i, R i) i x ∈ ·.asIdeal) eq

Premises used: Function.update, Membership.mem, congr_arg, OfNat.ofNat
-- Module: Mathlib.RingTheory.Spectrum.Prime.RingHom
Goal:
ι : Type u_3
R : ι → Type u_2
inst : (i : ι) → CommSemiring (R i)
x x_1 : (i : ι) × PrimeSpectrum (R i)
i : ι
p : PrimeSpectrum (R i)
j : ι
q : PrimeSpectrum (R j)
eq :
  Eq (α := PrimeSpectrum ((i : ι) → R i)) (sigmaToPi R (Sigma.mk (β := fun (i : ι) ↦ PrimeSpectrum (R i)) i p))
    (sigmaToPi R (Sigma.mk (β := fun (i : ι) ↦ PrimeSpectrum (R i)) j q))
ne : i ≠ j
⊢ Eq (α := (i : ι) × PrimeSpectrum (R i)) (Sigma.mk (β := fun (i : ι) ↦ PrimeSpectrum (R i)) i p)
    (Sigma.mk (β := fun (i : ι) ↦ PrimeSpectrum (R i)) j q)

Tactic:
(p.1.ne_top_iff_one.mp p.2.ne_top ?_).elim

Premises used: Ideal.ne_top_iff_one, PrimeSpectrum.isPrime, False.elim, Iff.mp, Ideal.IsPrime.ne_top, PrimeSpectrum.asIdeal
-- Module: Mathlib.RingTheory.Spectrum.Prime.RingHom
Goal:
ι : Type u_3
R : ι → Type u_2
inst : (i : ι) → CommSemiring (R i)
x x_1 : (i : ι) × PrimeSpectrum (R i)
i : ι
p : PrimeSpectrum (R i)
j : ι
q : PrimeSpectrum (R j)
eq :
  Eq (α := PrimeSpectrum ((i : ι) → R i)) (sigmaToPi R (Sigma.mk (β := fun (i : ι) ↦ PrimeSpectrum (R i)) i p))
    (sigmaToPi R (Sigma.mk (β := fun (i : ι) ↦ PrimeSpectrum (R i)) j q))
ne : i ≠ j
inr : 1 ∈ p.asIdeal
⊢ Eq (α := (i : ι) × PrimeSpectrum (R i)) (Sigma.mk (β := fun (i : ι) ↦ PrimeSpectrum (R i)) i p)
    (Sigma.mk (β := fun (i : ι) ↦ PrimeSpectrum (R i)) j q)

Tactic:
refine (p.1.ne_top_iff_one.mp p.2.ne_top ?_).elim

Premises used: Ideal.ne_top_iff_one, PrimeSpectrum.isPrime, False.elim, Iff.mp, Ideal.IsPrime.ne_top, PrimeSpectrum.asIdeal
-- Module: Mathlib.RingTheory.Spectrum.Prime.RingHom
Goal:
ι : Type u_3
R : ι → Type u_2
inst : (i : ι) → CommSemiring (R i)
x x_1 : (i : ι) × PrimeSpectrum (R i)
i : ι
p : PrimeSpectrum (R i)
j : ι
q : PrimeSpectrum (R j)
eq :
  Eq (α := PrimeSpectrum ((i : ι) → R i)) (sigmaToPi R (Sigma.mk (β := fun (i : ι) ↦ PrimeSpectrum (R i)) i p))
    (sigmaToPi R (Sigma.mk (β := fun (i : ι) ↦ PrimeSpectrum (R i)) j q))
ne : i ≠ j
⊢ Membership.mem (γ := Ideal ((i : ι) → R i))
    (asIdeal (sigmaToPi R (Sigma.mk (β := fun (i : ι) ↦ PrimeSpectrum (R i)) j q))) (Function.update (β := R) 1 j 0)

Tactic:
simp
-- Module: Mathlib.RingTheory.Spectrum.Prime.RingHom
Goal:
ι : Type u_3
R : ι → Type u_2
inst : (i : ι) → CommSemiring (R i)
x x_1 : (i : ι) × PrimeSpectrum (R i)
i : ι
p : PrimeSpectrum (R i)
j : ι
q : PrimeSpectrum (R j)
eq :
  Eq (α := PrimeSpectrum ((i : ι) → R i)) (sigmaToPi R (Sigma.mk (β := fun (i : ι) ↦ PrimeSpectrum (R i)) i p))
    (sigmaToPi R (Sigma.mk (β := fun (i : ι) ↦ PrimeSpectrum (R i)) j q))
ne : i ≠ j
⊢ Membership.mem (γ := Ideal ((i : ι) → R i))
    (asIdeal (sigmaToPi R (Sigma.mk (β := fun (i : ι) ↦ PrimeSpectrum (R i)) j q))) (Function.update (β := R) 1 j 0)

Tactic:
have : Function.update (1 : ∀ i, R i) j 0 ∈ (sigmaToPi R ⟨j, q⟩).asIdeal := by simp
-- Module: Mathlib.RingTheory.Spectrum.Prime.RingHom
Goal:
ι : Type u_3
R : ι → Type u_2
inst : (i : ι) → CommSemiring (R i)
x x_1 : (i : ι) × PrimeSpectrum (R i)
i : ι
p : PrimeSpectrum (R i)
j : ι
q : PrimeSpectrum (R j)
eq :
  Eq (α := PrimeSpectrum ((i : ι) → R i)) (sigmaToPi R (Sigma.mk (β := fun (i : ι) ↦ PrimeSpectrum (R i)) i p))
    (sigmaToPi R (Sigma.mk (β := fun (i : ι) ↦ PrimeSpectrum (R i)) j q))
ne : i ≠ j
this :
  Membership.mem (γ := Ideal ((i : ι) → R i))
    (asIdeal (sigmaToPi R (Sigma.mk (β := fun (i : ι) ↦ PrimeSpectrum (R i)) j q))) (Function.update (β := R) 1 j 0)
⊢ 1 ∈ p.asIdeal

Tactic:
simpa [← eq, Function.update_of_ne ne]

Premises used: Function.update_of_ne
-- Module: Mathlib.RingTheory.Spectrum.Prime.RingHom
Goal:
ι : Type u_3
R : ι → Type u_2
inst : (i : ι) → CommSemiring (R i)
x x_1 : (i : ι) × PrimeSpectrum (R i)
i : ι
p : PrimeSpectrum (R i)
j : ι
q : PrimeSpectrum (R j)
eq :
  Eq (α := PrimeSpectrum ((i : ι) → R i)) (sigmaToPi R (Sigma.mk (β := fun (i : ι) ↦ PrimeSpectrum (R i)) i p))
    (sigmaToPi R (Sigma.mk (β := fun (i : ι) ↦ PrimeSpectrum (R i)) j q))
inl :
  ∀ (q : PrimeSpectrum (R i))
    (eq :
      Eq (α := PrimeSpectrum ((i : ι) → R i)) (sigmaToPi R (Sigma.mk (β := fun (i : ι) ↦ PrimeSpectrum (R i)) i p))
        (sigmaToPi R (Sigma.mk (β := fun (i : ι) ↦ PrimeSpectrum (R i)) i q))),
    Eq (α := (i : ι) × PrimeSpectrum (R i)) (Sigma.mk (β := fun (i : ι) ↦ PrimeSpectrum (R i)) i p)
      (Sigma.mk (β := fun (i : ι) ↦ PrimeSpectrum (R i)) i q)
inr inr₁ :
  ∀ (ne : i ≠ j),
    Eq (α := (i : ι) × PrimeSpectrum (R i)) (Sigma.mk (β := fun (i : ι) ↦ PrimeSpectrum (R i)) i p)
      (Sigma.mk (β := fun (i : ι) ↦ PrimeSpectrum (R i)) j q)
⊢ Eq (α := (i : ι) × PrimeSpectrum (R i)) (Sigma.mk (β := fun (i : ι) ↦ PrimeSpectrum (R i)) i p)
    (Sigma.mk (β := fun (i : ι) ↦ PrimeSpectrum (R i)) j q)

Tactic:
classical
  obtain rfl | ne := eq_or_ne i j
  · congr; ext x
    simpa using congr_arg (Function.update (0 : ∀ i, R i) i x ∈ ·.asIdeal) eq
  · refine (p.1.ne_top_iff_one.mp p.2.ne_top ?_).elim
    have : Function.update (1 : ∀ i, R i) j 0 ∈ (sigmaToPi R ⟨j, q⟩).asIdeal := by simp
    simpa [← eq, Function.update_of_ne ne]

Premises used: Ideal.ne_top_iff_one, PrimeSpectrum.isPrime, False.elim, Iff.mp, eq_or_ne, Ideal.IsPrime.ne_top, PrimeSpectrum.asIdeal, rfl
-- Module: Mathlib.RingTheory.Spectrum.Prime.RingHom
Goal:
ι : Type u_3
R : ι → Type u_2
inst : (i : ι) → CommSemiring (R i)
inst_1 : Infinite ι
inst_2 : ∀ (i : ι), Nontrivial.{u_2} (R i)
r : (i : ι) → R i
x : Π₀ (i : ι), R i
⊢ HSMul.hSMul (β := (i : ι) → R i) r
      ((DFinsupp.coeFnAddMonoidHom (β := R) : (a : Π₀ (i : ι), R i) → (i : ι) → R i) x : (i : ι) → R i) ∈
    AddSubsemigroup.carrier
      (AddSubmonoid.toAddSubsemigroup
        (AddMonoidHom.mrange (F := (Π₀ (i : ι), R i) →+ (i : ι) → R i) (DFinsupp.coeFnAddMonoidHom (β := R))))

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

Premises used: DFinsupp.mk, HMul.hMul, Set.Mem, setOf, DFinsupp.support, funext, Exists.intro, Set.range, Subtype.val, DFunLike.coe
-- Module: Mathlib.RingTheory.Spectrum.Prime.RingHom
Goal:
ι : Type u_3
R : ι → Type u_2
inst : (i : ι) → CommSemiring (R i)
inst_1 : Infinite ι
inst_2 : ∀ (i : ι), Nontrivial.{u_2} (R i)
r : (i : ι) → R i
x : Π₀ (i : ι), R i
refine :
  ∀ (i : ι),
    (if H : i ∈ x.support (β := R) then
        (fun (i : (↑(↑(x.support (β := R)) : Set ι) : Type u_3)) ↦
            HMul.hMul (α := R (↑i : ι)) (r (↑i : ι)) ((x : (a : ι) → R a) (↑i : ι)))
          (Subtype.mk (p := fun (x_1 : ι) ↦ x_1 ∈ (↑(x.support (β := R)) : Set ι)) i H)
      else 0) =
      HSMul.hSMul (β := (i : ι) → R i) r
        ((DFinsupp.coeFnAddMonoidHom (β := R) : (a : Π₀ (i : ι), R i) → (i : ι) → R i) x : (i : ι) → R i) i
⊢ HSMul.hSMul (β := (i : ι) → R i) r
      ((DFinsupp.coeFnAddMonoidHom (β := R) : (a : Π₀ (i : ι), R i) → (i : ι) → R i) x : (i : ι) → R i) ∈
    AddSubsemigroup.carrier
      (AddSubmonoid.toAddSubsemigroup
        (AddMonoidHom.mrange (F := (Π₀ (i : ι), R i) →+ (i : ι) → R i) (DFinsupp.coeFnAddMonoidHom (β := R))))

Tactic:
refine ⟨.mk x.support fun i ↦ r i * x i, funext fun i ↦ show dite _ _ _ = _ from ?_⟩
-- Module: Mathlib.RingTheory.Spectrum.Prime.RingHom
Goal:
ι : Type u_3
R : ι → Type u_2
inst : (i : ι) → CommSemiring (R i)
inst_1 : Infinite ι
inst_2 : ∀ (i : ι), Nontrivial.{u_2} (R i)
r : (i : ι) → R i
x : Π₀ (i : ι), R i
i : ι
simp_rw :
  (if h : i ∈ x.support (β := R) then r i * (x : (a : ι) → R a) i else 0) =
    HSMul.hSMul (β := (i : ι) → R i) r
      (({ toFun := DFunLike.coe (β := R), map_zero' := ⋯, map_add' := ⋯ : (Π₀ (i : ι), R i) →+ (i : ι) → R i } :
            (a : Π₀ (i : ι), R i) → (i : ι) → R i)
          x :
        (i : ι) → R i)
      i
⊢ (if H : i ∈ x.support (β := R) then
      (fun (i : (↑(↑(x.support (β := R)) : Set ι) : Type u_3)) ↦
          HMul.hMul (α := R (↑i : ι)) (r (↑i : ι)) ((x : (a : ι) → R a) (↑i : ι)))
        (Subtype.mk (p := fun (x_1 : ι) ↦ x_1 ∈ (↑(x.support (β := R)) : Set ι)) i H)
    else 0) =
    HSMul.hSMul (β := (i : ι) → R i) r
      ((DFinsupp.coeFnAddMonoidHom (β := R) : (a : Π₀ (i : ι), R i) → (i : ι) → R i) x : (i : ι) → R i) i

Tactic:
simp_rw +instances [DFinsupp.coeFnAddMonoidHom]

Premises used: DFinsupp.coeFnAddMonoidHom
-- Module: Mathlib.RingTheory.Spectrum.Prime.RingHom
Goal:
ι : Type u_3
R : ι → Type u_2
inst : (i : ι) → CommSemiring (R i)
inst_1 : Infinite ι
inst_2 : ∀ (i : ι), Nontrivial.{u_2} (R i)
r : (i : ι) → R i
x : Π₀ (i : ι), R i
i : ι
⊢ (if h : i ∈ x.support (β := R) then r i * (x : (a : ι) → R a) i else 0) =
    HSMul.hSMul (β := (i : ι) → R i) r
      (({ toFun := DFunLike.coe (β := R), map_zero' := ⋯, map_add' := ⋯ : (Π₀ (i : ι), R i) →+ (i : ι) → R i } :
            (a : Π₀ (i : ι), R i) → (i : ι) → R i)
          x :
        (i : ι) → R i)
      i

Tactic:
dite_eq_left_iff.mpr fun h ↦ ?_

Premises used: Iff.mpr, dite_eq_left_iff
-- Module: Mathlib.RingTheory.Spectrum.Prime.RingHom
Goal:
ι : Type u_3
R : ι → Type u_2
inst : (i : ι) → CommSemiring (R i)
inst_1 : Infinite ι
inst_2 : ∀ (i : ι), Nontrivial.{u_2} (R i)
r : (i : ι) → R i
x : Π₀ (i : ι), R i
i : ι
refine : ∀ (h : i ∉ x.support (β := R)), 0 = r i * (x : (a : ι) → R a) i
⊢ (if h : i ∈ x.support (β := R) then r i * (x : (a : ι) → R a) i else 0) =
    HSMul.hSMul (β := (i : ι) → R i) r
      (({ toFun := DFunLike.coe (β := R), map_zero' := ⋯, map_add' := ⋯ : (Π₀ (i : ι), R i) →+ (i : ι) → R i } :
            (a : Π₀ (i : ι), R i) → (i : ι) → R i)
          x :
        (i : ι) → R i)
      i

Tactic:
refine dite_eq_left_iff.mpr fun h ↦ ?_

Premises used: Iff.mpr, dite_eq_left_iff
-- Module: Mathlib.RingTheory.Spectrum.Prime.RingHom
Goal:
ι : Type u_3
R : ι → Type u_2
inst : (i : ι) → CommSemiring (R i)
inst_1 : Infinite ι
inst_2 : ∀ (i : ι), Nontrivial.{u_2} (R i)
r : (i : ι) → R i
x : Π₀ (i : ι), R i
i : ι
h : i ∉ x.support (β := R)
rw : 0 = r i * 0
rw₁ rw₂ : Eq.{u_2 + 1} (α := R i) 0 0
⊢ 0 = r i * (x : (a : ι) → R a) i

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

Premises used: DFinsupp.notMem_support_iff, MulZeroClass.mul_zero, Iff.mp
-- Module: Mathlib.RingTheory.Spectrum.Prime.RingHom
Goal:
ι : Type u_3
R : ι → Type u_2
inst : (i : ι) → CommSemiring (R i)
inst_1 : Infinite ι
inst_2 : ∀ (i : ι), Nontrivial.{u_2} (R i)
J : Ideal ((i : ι) → R i) :=
  let __spread.0 : AddSubmonoid ((i : ι) → R i) :=
    AddMonoidHom.mrange (F := (Π₀ (i : ι), R i) →+ (i : ι) → R i) (DFinsupp.coeFnAddMonoidHom (β := R));
  { toAddSubmonoid := __spread.0, smul_mem' := ⋯ }
x : Π₀ (i : ι), R i
hx :
  Eq (α := (i : ι) → R i)
    ((DFinsupp.coeFnAddMonoidHom (β := R) : (a : Π₀ (i : ι), R i) → (i : ι) → R i) x : (i : ι) → R i)
    (1 : (i : ι) → R i)
have : ∀ (i : ι) (hi : i ∉ x.support (β := R)), False
⊢ False

Tactic:
have ⟨i, hi⟩ := x.support.exists_notMem