awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Spectrum.Maximal.Localization
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
f_1 : R →+* S
hf : Function.Bijective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f_1 : (a : R) → S)
f : R ≃+* S := RingEquiv.ofBijective f_1 hf
e : RingEquiv.{u_1, u_2} (PiLocalization R) (PiLocalization S) :=
  RingEquiv.ofRingHom (mapPiLocalization (↑f : R →+* S)) (mapPiLocalization (↑f.symm : S →+* R)) ⋯ ⋯
⊢ Function.Bijective.{u_1 + 1, u_2 + 1} (α := PiLocalization R) (β := PiLocalization S)
    (⇑(mapPiLocalization f_1) : (a : PiLocalization R) → PiLocalization S)

Tactic:
e.bijective

Premises used: Set.Mem, setOf, MonoidHomClass.toMonoidHom, RingHomClass.toRingHom, RingEquiv.bijective
-- Module: Mathlib.RingTheory.Spectrum.Maximal.Localization
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
f_1 : R →+* S
hf : Function.Bijective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f_1 : (a : R) → S)
f : R ≃+* S := RingEquiv.ofBijective f_1 hf
e : RingEquiv.{u_1, u_2} (PiLocalization R) (PiLocalization S) :=
  RingEquiv.ofRingHom (mapPiLocalization (↑f : R →+* S)) (mapPiLocalization (↑f.symm : S →+* R)) ⋯ ⋯
⊢ Function.Bijective.{u_1 + 1, u_2 + 1} (α := PiLocalization R) (β := PiLocalization S)
    (⇑(mapPiLocalization f_1) : (a : PiLocalization R) → PiLocalization S)

Tactic:
exact e.bijective

Premises used: RingEquiv.bijective
-- Module: Mathlib.RingTheory.Spectrum.Maximal.Localization
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
f_1 : R →+* S
hf : Function.Bijective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f_1 : (a : R) → S)
f : R ≃+* S := RingEquiv.ofBijective f_1 hf
refine_1 :
  Eq (α := PiLocalization S →+* PiLocalization S)
    (mapPiLocalization (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑f : R →+* S) (↑f.symm : S →+* R)))
    (RingHom.id (PiLocalization S))
refine_1₁ :
  Eq (α := PiLocalization S →+* PiLocalization S) (mapPiLocalization (RingHom.id S)) (RingHom.id (PiLocalization S))
refine_1₂ refine_1₃ :
  Eq.{u_2 + 1} (α := PiLocalization S →+* PiLocalization S) (RingHom.id (PiLocalization S))
    (RingHom.id (PiLocalization S))
⊢ Eq (α := PiLocalization S →+* PiLocalization S)
    (RingHom.comp (β := PiLocalization R) (mapPiLocalization (↑f : R →+* S)) (mapPiLocalization (↑f.symm : S →+* R)))
    (RingHom.id (PiLocalization S))

Tactic:
rw [← mapPiLocalization_comp, RingEquiv.comp_symm, mapPiLocalization_id]

Premises used: PrimeSpectrum.mapPiLocalization_id, PrimeSpectrum.mapPiLocalization_comp, RingEquiv.comp_symm
-- Module: Mathlib.RingTheory.Spectrum.Maximal.Localization
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
f_1 : R →+* S
hf : Function.Bijective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f_1 : (a : R) → S)
f : R ≃+* S := RingEquiv.ofBijective f_1 hf
refine_2 :
  Eq (α := PiLocalization R →+* PiLocalization R)
    (mapPiLocalization (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑f.symm : S →+* R) (↑f : R →+* S)))
    (RingHom.id (PiLocalization R))
refine_2₁ :
  Eq (α := PiLocalization R →+* PiLocalization R) (mapPiLocalization (RingHom.id R)) (RingHom.id (PiLocalization R))
refine_2₂ refine_2₃ :
  Eq.{u_1 + 1} (α := PiLocalization R →+* PiLocalization R) (RingHom.id (PiLocalization R))
    (RingHom.id (PiLocalization R))
⊢ Eq (α := PiLocalization R →+* PiLocalization R)
    (RingHom.comp (β := PiLocalization S) (mapPiLocalization (↑f.symm : S →+* R)) (mapPiLocalization (↑f : R →+* S)))
    (RingHom.id (PiLocalization R))

Tactic:
rw [← mapPiLocalization_comp, RingEquiv.symm_comp, mapPiLocalization_id]

Premises used: PrimeSpectrum.mapPiLocalization_id, PrimeSpectrum.mapPiLocalization_comp, RingEquiv.symm_comp
-- Module: Mathlib.RingTheory.Spectrum.Maximal.Localization
Goal:
ι : Type u_5
R : ι → Type u_4
inst : (i : ι) → CommSemiring (R i)
inst_1 : ∀ (i : ι), Nontrivial.{u_4} (R i)
inst_2 : Infinite ι
surj :
  Function.Surjective (α := (i : ι) → R i) (β := PiLocalization ((i : ι) → R i))
    (⇑(toPiLocalization ((i : ι) → R i)) : (a : (i : ι) → R i) → PiLocalization ((i : ι) → R i))
rw :
  Function.Surjective (α := (i : ι) → R i) (β := MaximalSpectrum.PiLocalization ((i : ι) → R i))
    (⇑(↑(AlgHom.comp (piLocalizationToMaximal ((i : ι) → R i)) (toPiLocalization ((i : ι) → R i))) :
          ((i : ι) → R i) →+* MaximalSpectrum.PiLocalization ((i : ι) → R i)) :
      (a : (i : ι) → R i) → MaximalSpectrum.PiLocalization ((i : ι) → R i))
⊢ Function.Surjective (α := (i : ι) → R i) (β := MaximalSpectrum.PiLocalization ((i : ι) → R i))
    (⇑(MaximalSpectrum.toPiLocalization ((i : ι) → R i)) :
      (a : (i : ι) → R i) → MaximalSpectrum.PiLocalization ((i : ι) → R i))

Tactic:
rw [← AlgHom.coe_toRingHom, ← piLocalizationToMaximal_comp_toPiLocalization]

Premises used: AlgHom.coe_toRingHom, PrimeSpectrum.piLocalizationToMaximal_comp_toPiLocalization
-- Module: Mathlib.RingTheory.Spectrum.Maximal.Localization
Goal:
ι : Type u_5
R : ι → Type u_4
inst : (i : ι) → CommSemiring (R i)
inst_1 : ∀ (i : ι), Nontrivial.{u_4} (R i)
inst_2 : Infinite ι
surj :
  Function.Surjective (α := (i : ι) → R i) (β := PiLocalization ((i : ι) → R i))
    (⇑(toPiLocalization ((i : ι) → R i)) : (a : (i : ι) → R i) → PiLocalization ((i : ι) → R i))
⊢ Function.Surjective (α := (i : ι) → R i) (β := MaximalSpectrum.PiLocalization ((i : ι) → R i))
    (⇑(↑(AlgHom.comp (piLocalizationToMaximal ((i : ι) → R i)) (toPiLocalization ((i : ι) → R i))) :
          ((i : ι) → R i) →+* MaximalSpectrum.PiLocalization ((i : ι) → R i)) :
      (a : (i : ι) → R i) → MaximalSpectrum.PiLocalization ((i : ι) → R i))

Tactic:
(piLocalizationToMaximal_surjective _).comp surj

Premises used: PrimeSpectrum.piLocalizationToMaximal_surjective, Quotient.mk', Function.Surjective.comp, OreLocalization.oreDiv
-- Module: Mathlib.RingTheory.Spectrum.Maximal.Localization
Goal:
ι : Type u_5
R : ι → Type u_4
inst : (i : ι) → CommSemiring (R i)
inst_1 : ∀ (i : ι), Nontrivial.{u_4} (R i)
inst_2 : Infinite ι
surj :
  Function.Surjective (α := (i : ι) → R i) (β := PiLocalization ((i : ι) → R i))
    (⇑(toPiLocalization ((i : ι) → R i)) : (a : (i : ι) → R i) → PiLocalization ((i : ι) → R i))
⊢ Function.Surjective (α := (i : ι) → R i) (β := MaximalSpectrum.PiLocalization ((i : ι) → R i))
    (⇑(↑(AlgHom.comp (piLocalizationToMaximal ((i : ι) → R i)) (toPiLocalization ((i : ι) → R i))) :
          ((i : ι) → R i) →+* MaximalSpectrum.PiLocalization ((i : ι) → R i)) :
      (a : (i : ι) → R i) → MaximalSpectrum.PiLocalization ((i : ι) → R i))

Tactic:
exact (piLocalizationToMaximal_surjective _).comp surj

Premises used: PrimeSpectrum.piLocalizationToMaximal_surjective, Function.Surjective.comp
-- Module: Mathlib.RingTheory.Spectrum.Maximal.Localization
Goal:
ι : Type u_5
R : ι → Type u_4
inst : (i : ι) → CommSemiring (R i)
inst_1 : ∀ (i : ι), Nontrivial.{u_4} (R i)
h : Infinite ι
⊢ ¬Function.Surjective (α := (i : ι) → R i) (β := PiLocalization ((i : ι) → R i))
      (⇑(toPiLocalization ((i : ι) → R i)) : (a : (i : ι) → R i) → PiLocalization ((i : ι) → R i))

Tactic:
toPiLocalization_not_surjective_of_infinite _

Premises used: PrimeSpectrum.toPiLocalization_not_surjective_of_infinite
-- Module: Mathlib.RingTheory.Spectrum.Maximal.Localization
Goal:
ι : Type u_5
R : ι → Type u_4
inst : (i : ι) → CommSemiring (R i)
inst_1 : ∀ (i : ι), Nontrivial.{u_4} (R i)
h : Infinite ι
⊢ ¬Function.Surjective (α := (i : ι) → R i) (β := PiLocalization ((i : ι) → R i))
      (⇑(toPiLocalization ((i : ι) → R i)) : (a : (i : ι) → R i) → PiLocalization ((i : ι) → R i))

Tactic:
exact toPiLocalization_not_surjective_of_infinite _

Premises used: PrimeSpectrum.toPiLocalization_not_surjective_of_infinite
-- Module: Mathlib.RingTheory.Spectrum.Maximal.Localization
Goal:
R : Type u_1
inst : CommSemiring R
surj : Function.Surjective (α := R) (β := PiLocalization R) (⇑(toPiLocalization R) : (a : R) → PiLocalization R)
⊢ Function.Surjective (α := R) (β := PiLocalization (PiLocalization R))
    (Function.comp (β := PiLocalization R)
      (⇑(mapPiLocalization (AlgHom.toRingHom (toPiLocalization R))) :
        (a : PiLocalization R) → PiLocalization (PiLocalization R))
      (⇑(toPiLocalization R) : (a : R) → PiLocalization R))

Tactic:
replace surj := (mapPiLocalization_bijective _ ⟨toPiLocalization_injective R, surj⟩).2.comp surj
-- Module: Mathlib.RingTheory.Spectrum.Maximal.Localization
Goal:
R : Type u_1
inst : CommSemiring R
surj :
  Function.Surjective (α := R) (β := PiLocalization (PiLocalization R))
    (Function.comp (β := PiLocalization R)
      (⇑(mapPiLocalization (AlgHom.toRingHom (toPiLocalization R))) :
        (a : PiLocalization R) → PiLocalization (PiLocalization R))
      (⇑(toPiLocalization R) : (a : R) → PiLocalization R))
⊢ Function.Surjective (α := R) (β := PiLocalization (PiLocalization R))
    (Function.comp (β := PiLocalization R)
      (⇑(AlgHom.toRingHom (toPiLocalization (PiLocalization R))) :
        (a : PiLocalization R) → PiLocalization (PiLocalization R))
      (⇑(AlgHom.toRingHom (toPiLocalization R)) : (a : R) → PiLocalization R))

Tactic:
rw [← AlgHom.coe_toRingHom,
    ← RingHom.coe_comp, mapPiLocalization_naturality, RingHom.coe_comp] at surj

Premises used: AlgHom.coe_toRingHom, PrimeSpectrum.mapPiLocalization_naturality, RingHom.coe_comp
-- Module: Mathlib.RingTheory.Spectrum.Maximal.Localization
Goal:
R : Type u_1
inst : CommSemiring R
surj :
  Function.Surjective (α := R) (β := PiLocalization (PiLocalization R))
    (Function.comp (β := PiLocalization R)
      (⇑(AlgHom.toRingHom (toPiLocalization (PiLocalization R))) :
        (a : PiLocalization R) → PiLocalization (PiLocalization R))
      (⇑(AlgHom.toRingHom (toPiLocalization R)) : (a : R) → PiLocalization R))
⊢ Finite.{u_1 + 1} (PrimeSpectrum R)

Tactic:
finite_of_toPiLocalization_pi_surjective surj.of_comp

Premises used: Function.Surjective.of_comp, PrimeSpectrum.finite_of_toPiLocalization_pi_surjective
-- Module: Mathlib.RingTheory.Spectrum.Maximal.Localization
Goal:
R : Type u_1
inst : CommSemiring R
surj :
  Function.Surjective (α := R) (β := PiLocalization (PiLocalization R))
    (Function.comp (β := PiLocalization R)
      (⇑(AlgHom.toRingHom (toPiLocalization (PiLocalization R))) :
        (a : PiLocalization R) → PiLocalization (PiLocalization R))
      (⇑(AlgHom.toRingHom (toPiLocalization R)) : (a : R) → PiLocalization R))
⊢ Finite.{u_1 + 1} (PrimeSpectrum R)

Tactic:
exact finite_of_toPiLocalization_pi_surjective surj.of_comp

Premises used: Function.Surjective.of_comp, PrimeSpectrum.finite_of_toPiLocalization_pi_surjective
-- Module: Mathlib.RingTheory.Spectrum.Maximal.Topology
Goal:
R : Type u
inst : CommRing R
simp : Eq.{u + 1} (α := Set (PrimeSpectrum R)) (range toPrimeSpectrum) {x : PrimeSpectrum R | x.asIdeal.IsMaximal}
⊢ Eq.{u + 1} (α := Set (PrimeSpectrum R)) (range toPrimeSpectrum)
    {x : PrimeSpectrum R | IsClosed (X := PrimeSpectrum R) {x}}

Tactic:
simp only [isClosed_singleton_iff_isMaximal]

Premises used: PrimeSpectrum.isClosed_singleton_iff_isMaximal
-- Module: Mathlib.RingTheory.Spectrum.Maximal.Topology
Goal:
R : Type u
inst : CommRing R
h :
  ∀ (x : Ideal R) (isPrime : x.IsPrime),
    Membership.mem (γ := Set (PrimeSpectrum R)) (range toPrimeSpectrum)
        { asIdeal := x, isPrime := isPrime : PrimeSpectrum R } ↔
      Membership.mem (γ := Set (PrimeSpectrum R)) {x : PrimeSpectrum R | x.asIdeal.IsMaximal}
        { asIdeal := x, isPrime := isPrime : PrimeSpectrum R }
⊢ Eq.{u + 1} (α := Set (PrimeSpectrum R)) (range toPrimeSpectrum) {x : PrimeSpectrum R | x.asIdeal.IsMaximal}

Tactic:
ext ⟨x, _⟩
-- Module: Mathlib.RingTheory.Spectrum.Maximal.Topology
Goal:
R : Type u
inst : CommRing R
x : Ideal R
isPrime : x.IsPrime
⊢ Membership.mem (γ := Set (PrimeSpectrum R)) (range toPrimeSpectrum)
      { asIdeal := x, isPrime := isPrime : PrimeSpectrum R } ↔
    Membership.mem (γ := Set (PrimeSpectrum R)) {x : PrimeSpectrum R | x.asIdeal.IsMaximal}
      { asIdeal := x, isPrime := isPrime : PrimeSpectrum R }

Tactic:
⟨fun ⟨y, hy⟩ => hy ▸ y.isMaximal, fun hx => ⟨⟨x, hx⟩, rfl⟩⟩

Premises used: PrimeSpectrum.mk, MaximalSpectrum.isMaximal, MaximalSpectrum.mk, setOf, Membership.mem, Eq.rec, Iff.intro, Exists.intro, _private.0.MaximalSpectrum.toPrimeSpectrum_range.match_1, Ideal.IsMaximal, PrimeSpectrum.asIdeal, rfl
-- Module: Mathlib.RingTheory.Spectrum.Maximal.Topology
Goal:
R : Type u
inst : CommRing R
x : Ideal R
isPrime : x.IsPrime
⊢ Membership.mem (γ := Set (PrimeSpectrum R)) (range toPrimeSpectrum)
      { asIdeal := x, isPrime := isPrime : PrimeSpectrum R } ↔
    Membership.mem (γ := Set (PrimeSpectrum R)) {x : PrimeSpectrum R | x.asIdeal.IsMaximal}
      { asIdeal := x, isPrime := isPrime : PrimeSpectrum R }

Tactic:
exact ⟨fun ⟨y, hy⟩ => hy ▸ y.isMaximal, fun hx => ⟨⟨x, hx⟩, rfl⟩⟩
-- Module: Mathlib.RingTheory.Spectrum.Maximal.Topology
Goal:
R : Type u
inst : CommRing R
x : MaximalSpectrum R
⊢ Eq (α := Set (MaximalSpectrum R)) (toPrimeSpectrum ⁻¹' {x.toPrimeSpectrum}) {x}

Tactic:
simpa only [← image_singleton] using preimage_image_eq {x} toPrimeSpectrum_injective

Premises used: Set.image_singleton, MaximalSpectrum.toPrimeSpectrum_injective, Set.preimage_image_eq, Singleton.singleton
-- Module: Mathlib.RingTheory.Spectrum.Maximal.Topology
Goal:
R : Type u
inst : CommRing R
⊢ Continuous.{u, u} (X := MaximalSpectrum R) toPrimeSpectrum

Tactic:
continuous_induced_dom

Premises used: continuous_induced_dom
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
Goal:
R : Type u
inst : CommSemiring R
⊢ Nonempty.{u + 1} (PrimeSpectrum R) ↔ Nontrivial R

Tactic:
⟨fun ⟨p⟩ ↦ ⟨0, 1, fun h ↦ p.2.ne_top ?_⟩, fun h ↦ ?_⟩

Premises used: Nontrivial, PrimeSpectrum.isPrime, _private.0.PrimeSpectrum.nonempty_iff_nontrivial.match_1, Nontrivial.mk, Iff.intro, Exists.intro, OfNat.ofNat, Ideal.IsPrime.ne_top
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
Goal:
R : Type u
inst : CommSemiring R
refine_1 : Nonempty.{u + 1} (PrimeSpectrum R) → ∀ (p : PrimeSpectrum R) (h : Eq.{u + 1} (α := R) 0 1), p.asIdeal = ⊤
refine_2 : ∀ (h : Nontrivial R), Nonempty.{u + 1} (PrimeSpectrum R)
⊢ Nonempty.{u + 1} (PrimeSpectrum R) ↔ Nontrivial R

Tactic:
refine ⟨fun ⟨p⟩ ↦ ⟨0, 1, fun h ↦ p.2.ne_top ?_⟩, fun h ↦ ?_⟩
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
Goal:
R : Type u
inst : CommSemiring R
h_1 : Nonempty.{u + 1} (PrimeSpectrum R)
p : PrimeSpectrum R
h : Eq.{u + 1} (α := R) 0 1
⊢ p.asIdeal = ⊤

Tactic:
simp [Ideal.eq_top_iff_one p.asIdeal, ← h]

Premises used: Ideal.eq_top_iff_one, PrimeSpectrum.asIdeal
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
Goal:
R : Type u
inst : CommSemiring R
h : Nontrivial R
refine_2 : ∀ (I : Ideal R) (hI : I.IsMaximal), Nonempty.{u + 1} (PrimeSpectrum R)
⊢ Nonempty.{u + 1} (PrimeSpectrum R)

Tactic:
obtain ⟨I, hI⟩ := Ideal.exists_maximal R

Premises used: Ideal.exists_maximal
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
Goal:
R : Type u
inst : CommSemiring R
h : Nontrivial R
I : Ideal R
hI : I.IsMaximal
⊢ Nonempty.{u + 1} (PrimeSpectrum R)

Tactic:
⟨⟨I, hI.isPrime⟩⟩

Premises used: PrimeSpectrum.mk, Ideal.IsMaximal.isPrime, Nonempty.intro
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
Goal:
R : Type u
inst : CommSemiring R
h : Nontrivial R
I : Ideal R
hI : I.IsMaximal
⊢ Nonempty.{u + 1} (PrimeSpectrum R)

Tactic:
exact ⟨⟨I, hI.isPrime⟩⟩
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
Goal:
R : Type u
inst : CommSemiring R
contrapose! : Nonempty.{u + 1} (PrimeSpectrum R) ↔ Nontrivial R
⊢ IsEmpty.{u + 1} (PrimeSpectrum R) ↔ Subsingleton R

Tactic:
contrapose!
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
Goal:
R : Type u
inst : CommSemiring R
⊢ Nonempty.{u + 1} (PrimeSpectrum R) ↔ Nontrivial R

Tactic:
nonempty_iff_nontrivial

Premises used: PrimeSpectrum.nonempty_iff_nontrivial
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
Goal:
R : Type u
inst : CommSemiring R
⊢ Nonempty.{u + 1} (PrimeSpectrum R) ↔ Nontrivial R

Tactic:
exact nonempty_iff_nontrivial

Premises used: PrimeSpectrum.nonempty_iff_nontrivial
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Nontrivial R
⊢ Nonempty.{u + 1} (PrimeSpectrum R)

Tactic:
nonempty_iff_nontrivial.mpr inferInstance

Premises used: Iff.mpr, inferInstance, PrimeSpectrum.nonempty_iff_nontrivial
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Subsingleton R
⊢ IsEmpty.{u + 1} (PrimeSpectrum R)

Tactic:
isEmpty_iff_subsingleton.mpr inferInstance

Premises used: Iff.mpr, inferInstance, PrimeSpectrum.isEmpty_iff_subsingleton
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
Goal:
R : Type u
inst : CommSemiring R
p : PrimeSpectrum R
⊢ Nontrivial R

Tactic:
nonempty_iff_nontrivial.mp ⟨p⟩

Premises used: Nonempty.intro, PrimeSpectrum.nonempty_iff_nontrivial, Iff.mp
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
Goal:
R : Type u
inst : CommSemiring R
⊢ Eq.{u + 1} (α := Set (Ideal R)) (Set.range asIdeal) {J : Ideal R | J.IsPrime}

Tactic:
Set.ext fun J ↦
    ⟨fun hJ ↦ let ⟨j, hj⟩ := Set.mem_range.mp hJ; Set.mem_setOf.mpr <| hj ▸ j.isPrime,
      fun hJ ↦ Set.mem_range.mpr ⟨⟨J, Set.mem_setOf.mp hJ⟩, rfl⟩⟩

Premises used: Iff.mpr, Set.ext, PrimeSpectrum.mk, Set.mem_range, PrimeSpectrum.isPrime, _private.0.PrimeSpectrum.range_asIdeal.match_1, setOf, Membership.mem, Eq.rec, Set.mem_setOf, Iff.intro, Ideal.IsPrime, Exists.intro, Iff.mp, rfl
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
left : Function.Injective (α := Sum.{u, v} (PrimeSpectrum R) (PrimeSpectrum S)) (primeSpectrumProdOfSum R S)
right : Function.Surjective (α := Sum.{u, v} (PrimeSpectrum R) (PrimeSpectrum S)) (primeSpectrumProdOfSum R S)
⊢ Function.Bijective (α := Sum.{u, v} (PrimeSpectrum R) (PrimeSpectrum S)) (primeSpectrumProdOfSum R S)

Tactic:
constructor
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
I : Ideal R
hI : I.IsPrime
I' : Ideal R
hI' : I'.IsPrime
h :
  Eq (α := PrimeSpectrum (R × S)) (primeSpectrumProdOfSum R S (Sum.inl { asIdeal := I, isPrime := hI }))
    (primeSpectrumProdOfSum R S (Sum.inl { asIdeal := I', isPrime := hI' }))
⊢ I = I' ∧ True

Tactic:
simp only [mk.injEq, Ideal.prod_inj, primeSpectrumProdOfSum] at h

Premises used: Ideal.prod_inj, PrimeSpectrum.mk.injEq, PrimeSpectrum.primeSpectrumProdOfSum
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
I : Ideal R
hI : I.IsPrime
J' : Ideal S
hJ' : J'.IsPrime
h :
  primeSpectrumProdOfSum R S (Sum.inl { asIdeal := I, isPrime := hI }) =
    primeSpectrumProdOfSum R S (Sum.inr { asIdeal := J', isPrime := hJ' : PrimeSpectrum S })
⊢ I = ⊤ ∧ ⊤ = J'

Tactic:
simp only [mk.injEq, Ideal.prod_inj, primeSpectrumProdOfSum] at h

Premises used: Ideal.prod_inj, PrimeSpectrum.mk.injEq, PrimeSpectrum.primeSpectrumProdOfSum
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
J : Ideal S
hJ : J.IsPrime
I' : Ideal R
hI' : I'.IsPrime
h :
  primeSpectrumProdOfSum R S (Sum.inr { asIdeal := J, isPrime := hJ }) =
    primeSpectrumProdOfSum R S (Sum.inl { asIdeal := I', isPrime := hI' : PrimeSpectrum R })
⊢ ⊤ = I' ∧ J = ⊤

Tactic:
simp only [mk.injEq, Ideal.prod_inj, primeSpectrumProdOfSum] at h

Premises used: Ideal.prod_inj, PrimeSpectrum.mk.injEq, PrimeSpectrum.primeSpectrumProdOfSum
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
J : Ideal S
hJ : J.IsPrime
J' : Ideal S
hJ' : J'.IsPrime
h :
  Eq (α := PrimeSpectrum (R × S)) (primeSpectrumProdOfSum R S (Sum.inr { asIdeal := J, isPrime := hJ }))
    (primeSpectrumProdOfSum R S (Sum.inr { asIdeal := J', isPrime := hJ' }))
⊢ True ∧ J = J'

Tactic:
simp only [mk.injEq, Ideal.prod_inj, primeSpectrumProdOfSum] at h

Premises used: Ideal.prod_inj, PrimeSpectrum.mk.injEq, PrimeSpectrum.primeSpectrumProdOfSum
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
I : Ideal R
hI : I.IsPrime
I' : Ideal R
hI' : I'.IsPrime
h : I = I' ∧ True
⊢ Eq (α := Sum.{u, v} (PrimeSpectrum R) (PrimeSpectrum S)) (Sum.inl { asIdeal := I, isPrime := hI })
    (Sum.inl { asIdeal := I', isPrime := hI' })

Tactic:
simp only [h]
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
I : Ideal R
hI : I.IsPrime
J' : Ideal S
hJ' : J'.IsPrime
h : I = ⊤ ∧ ⊤ = J'
⊢ Sum.inl { asIdeal := I, isPrime := hI } = Sum.inr { asIdeal := J', isPrime := hJ' : PrimeSpectrum S }

Tactic:
False.elim (hI.ne_top h.left)

Premises used: False.elim, And.left, Ideal.IsPrime.ne_top
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
I : Ideal R
hI : I.IsPrime
J' : Ideal S
hJ' : J'.IsPrime
h : I = ⊤ ∧ ⊤ = J'
⊢ Sum.inl { asIdeal := I, isPrime := hI } = Sum.inr { asIdeal := J', isPrime := hJ' : PrimeSpectrum S }

Tactic:
exact False.elim (hI.ne_top h.left)

Premises used: False.elim, And.left, Ideal.IsPrime.ne_top
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
J : Ideal S
hJ : J.IsPrime
I' : Ideal R
hI' : I'.IsPrime
h : ⊤ = I' ∧ J = ⊤
⊢ Sum.inr { asIdeal := J, isPrime := hJ } = Sum.inl { asIdeal := I', isPrime := hI' : PrimeSpectrum R }

Tactic:
False.elim (hJ.ne_top h.right)

Premises used: False.elim, And.right, Ideal.IsPrime.ne_top
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
J : Ideal S
hJ : J.IsPrime
I' : Ideal R
hI' : I'.IsPrime
h : ⊤ = I' ∧ J = ⊤
⊢ Sum.inr { asIdeal := J, isPrime := hJ } = Sum.inl { asIdeal := I', isPrime := hI' : PrimeSpectrum R }

Tactic:
exact False.elim (hJ.ne_top h.right)

Premises used: False.elim, And.right, Ideal.IsPrime.ne_top
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
J : Ideal S
hJ : J.IsPrime
J' : Ideal S
hJ' : J'.IsPrime
h : True ∧ J = J'
⊢ Eq (α := Sum.{u, v} (PrimeSpectrum R) (PrimeSpectrum S)) (Sum.inr { asIdeal := J, isPrime := hJ })
    (Sum.inr { asIdeal := J', isPrime := hJ' })

Tactic:
simp only [h]
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
I : Ideal (R × S)
hI : I.IsPrime
right :
  ∀ (p : Ideal R) (hp : p.IsPrime) (hI : Ideal.IsPrime (α := R × S) (p.prod ⊤)),
    ∃ (a : Sum.{u, v} (PrimeSpectrum R) (PrimeSpectrum S)),
      primeSpectrumProdOfSum R S a = { asIdeal := p.prod ⊤, isPrime := hI }
right₁ :
  ∀ (p : Ideal S) (hp : p.IsPrime) (hI : Ideal.IsPrime (α := R × S) (Ideal.prod ⊤ p)),
    ∃ (a : Sum.{u, v} (PrimeSpectrum R) (PrimeSpectrum S)),
      primeSpectrumProdOfSum R S a = { asIdeal := Ideal.prod ⊤ p, isPrime := hI }
⊢ ∃ (a : Sum.{u, v} (PrimeSpectrum R) (PrimeSpectrum S)), primeSpectrumProdOfSum R S a = { asIdeal := I, isPrime := hI }

Tactic:
rcases (Ideal.ideal_prod_prime I).mp hI with (⟨p, ⟨hp, rfl⟩⟩ | ⟨p, ⟨hp, rfl⟩⟩)

Premises used: Ideal.ideal_prod_prime, Iff.mp, rfl
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
p : Ideal R
hp : p.IsPrime
hI : Ideal.IsPrime (α := R × S) (p.prod ⊤)
⊢ ∃ (a : Sum.{u, v} (PrimeSpectrum R) (PrimeSpectrum S)),
    primeSpectrumProdOfSum R S a = { asIdeal := p.prod ⊤, isPrime := hI }

Tactic:
⟨Sum.inl ⟨p, hp⟩, rfl⟩

Premises used: PrimeSpectrum.mk, Sum.inl, Exists.intro, rfl
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
p : Ideal R
hp : p.IsPrime
hI : Ideal.IsPrime (α := R × S) (p.prod ⊤)
⊢ ∃ (a : Sum.{u, v} (PrimeSpectrum R) (PrimeSpectrum S)),
    primeSpectrumProdOfSum R S a = { asIdeal := p.prod ⊤, isPrime := hI }

Tactic:
exact ⟨Sum.inl ⟨p, hp⟩, rfl⟩