awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Spectrum.Prime.RingHom
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
hf : Surjective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
I : Ideal R
hI : ker f = I
p : Ideal R
isPrime : p.IsPrime
hp :
  Membership.mem (γ := Set (PrimeSpectrum R)) (zeroLocus (↑I : Set R))
    { asIdeal := p, isPrime := isPrime : PrimeSpectrum R }
simp : comap f (map f p) = p
⊢ (fun (p : PrimeSpectrum S) ↦
        (Subtype.mk (p := fun (x : PrimeSpectrum R) ↦
            Membership.mem (γ := Set (PrimeSpectrum R)) (zeroLocus (↑I : Set R)) x) (PrimeSpectrum.comap f p) ⋯ :
          { x : PrimeSpectrum R // Membership.mem (γ := Set (PrimeSpectrum R)) (zeroLocus (↑I : Set R)) x }))
      ((fun (x : (↑(zeroLocus (↑I : Set R)) : Type u)) ↦
          (match (motive := (↑(zeroLocus (↑I : Set R)) : Type u) → PrimeSpectrum S) x with
            | ⟨{ asIdeal := p, isPrime := isPrime }, hp⟩ => { asIdeal := map f p, isPrime := ⋯ } :
            PrimeSpectrum S))
        (Subtype.mk (p := fun (x : PrimeSpectrum R) ↦
          Membership.mem (γ := Set (PrimeSpectrum R)) (zeroLocus (↑I : Set R)) x) { asIdeal := p, isPrime := isPrime }
          hp)) =
    Subtype.mk (p := fun (x : PrimeSpectrum R) ↦ Membership.mem (γ := Set (PrimeSpectrum R)) (zeroLocus (↑I : Set R)) x)
      { asIdeal := p, isPrime := isPrime : PrimeSpectrum R } hp

Tactic:
simp only [Subtype.mk.injEq, PrimeSpectrum.ext_iff, comap_asIdeal]

Premises used: PrimeSpectrum.ext_iff, Subtype.mk.injEq, PrimeSpectrum.comap_asIdeal
-- Module: Mathlib.RingTheory.Spectrum.Prime.RingHom
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
hf : Surjective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
I : Ideal R
hI : ker f = I
p : Ideal R
isPrime : p.IsPrime
hp :
  Membership.mem (γ := Set (PrimeSpectrum R)) (zeroLocus (↑I : Set R))
    { asIdeal := p, isPrime := isPrime : PrimeSpectrum R }
⊢ comap f (map f p) = p

Tactic:
(p.comap_map_of_surjective f hf).trans <| sup_eq_left.mpr (hI.trans_le hp)

Premises used: Iff.mpr, sup_eq_left, Eq.trans_le, Ideal.comap_map_of_surjective, Eq.trans
-- Module: Mathlib.RingTheory.Spectrum.Prime.RingHom
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
hf : Surjective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
I : Ideal R
hI : ker f = I
p : Ideal R
isPrime : p.IsPrime
hp :
  Membership.mem (γ := Set (PrimeSpectrum R)) (zeroLocus (↑I : Set R))
    { asIdeal := p, isPrime := isPrime : PrimeSpectrum R }
⊢ comap f (map f p) = p

Tactic:
exact (p.comap_map_of_surjective f hf).trans <| sup_eq_left.mpr (hI.trans_le hp)

Premises used: Iff.mpr, sup_eq_left, Eq.trans_le, Ideal.comap_map_of_surjective, Eq.trans
-- Module: Mathlib.RingTheory.Spectrum.Prime.RingHom
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
hf : Surjective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
I : Ideal R
hI : ker f = I
a b : PrimeSpectrum S
rw : map f (comap f a.asIdeal) ≤ b.asIdeal ↔ a ≤ b
rw₁ : a.asIdeal ≤ b.asIdeal ↔ a ≤ b
rw₂ rw₃ : a ≤ b ↔ a ≤ b
⊢ LE.le (α := Ideal R) (comap f a.asIdeal) (comap f b.asIdeal) ↔ a ≤ b

Tactic:
rw [← Ideal.map_le_iff_le_comap, Ideal.map_comap_of_surjective f hf,
      PrimeSpectrum.asIdeal_le_asIdeal]

Premises used: Ideal.map_le_iff_le_comap, Ideal.map_comap_of_surjective, PrimeSpectrum.asIdeal_le_asIdeal
-- Module: Mathlib.RingTheory.Spectrum.Prime.RingHom
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
p : PrimeSpectrum R
h : p ∈ Set.range (comap f)
q : PrimeSpectrum S
hq : comap f q = p
⊢ Ideal.comap f (Ideal.map f p.asIdeal) = p.asIdeal

Tactic:
simp [← hq]
-- Module: Mathlib.RingTheory.Spectrum.Prime.RingHom
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
p : PrimeSpectrum R
refine : Ideal.comap f (Ideal.map f p.asIdeal) = p.asIdeal → p ∈ Set.range (comap f)
⊢ p ∈ Set.range (comap f) ↔ Ideal.comap f (Ideal.map f p.asIdeal) = p.asIdeal

Tactic:
refine ⟨fun ⟨q, hq⟩ ↦ by simp [← hq], ?_⟩
-- Module: Mathlib.RingTheory.Spectrum.Prime.RingHom
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
p : PrimeSpectrum R
rw : (∃ (q : Ideal S), q.IsPrime ∧ Ideal.comap f q = p.asIdeal) → p ∈ Set.range (comap f)
⊢ Ideal.comap f (Ideal.map f p.asIdeal) = p.asIdeal → p ∈ Set.range (comap f)

Tactic:
rw [Ideal.comap_map_eq_self_iff_of_isPrime]

Premises used: Ideal.comap_map_eq_self_iff_of_isPrime
-- Module: Mathlib.RingTheory.Spectrum.Prime.RingHom
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
p : PrimeSpectrum R
q : Ideal S
left : q.IsPrime
hq : Ideal.comap f q = p.asIdeal
⊢ p ∈ Set.range (comap f)

Tactic:
⟨⟨q, inferInstance⟩, PrimeSpectrum.ext hq⟩

Premises used: PrimeSpectrum.mk, PrimeSpectrum.ext, Set.Mem, setOf, inferInstance, Exists.intro, Set.range
-- Module: Mathlib.RingTheory.Spectrum.Prime.RingHom
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
p : PrimeSpectrum R
q : Ideal S
left : q.IsPrime
hq : Ideal.comap f q = p.asIdeal
⊢ p ∈ Set.range (comap f)

Tactic:
exact ⟨⟨q, inferInstance⟩, PrimeSpectrum.ext hq⟩
-- Module: Mathlib.RingTheory.Spectrum.Prime.RingHom
Goal:
R : Type u
inst : CommRing R
S : Type u_1
inst_1 : CommRing S
inst_2 : Algebra R S
p : PrimeSpectrum R
k : Type u := p.asIdeal.ResidueField
⊢ Nontrivial (p.asIdeal.ResidueField ⊗[R] S) ↔
    Membership.mem (γ := Set (PrimeSpectrum R)) (Set.range (ι := PrimeSpectrum S) (comap (algebraMap R S))) p

Tactic:
⟨fun h ↦ ?_, fun h ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.RingTheory.Spectrum.Prime.RingHom
Goal:
R : Type u
inst : CommRing R
S : Type u_1
inst_1 : CommRing S
inst_2 : Algebra R S
p : PrimeSpectrum R
k : Type u := p.asIdeal.ResidueField
refine_1 :
  ∀ (h : Nontrivial (p.asIdeal.ResidueField ⊗[R] S)),
    Membership.mem (γ := Set (PrimeSpectrum R)) (Set.range (ι := PrimeSpectrum S) (comap (algebraMap R S))) p
refine_2 :
  ∀ (h : Membership.mem (γ := Set (PrimeSpectrum R)) (Set.range (ι := PrimeSpectrum S) (comap (algebraMap R S))) p),
    Nontrivial (p.asIdeal.ResidueField ⊗[R] S)
⊢ Nontrivial (p.asIdeal.ResidueField ⊗[R] S) ↔
    Membership.mem (γ := Set (PrimeSpectrum R)) (Set.range (ι := PrimeSpectrum S) (comap (algebraMap R S))) p

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Module: Mathlib.RingTheory.Spectrum.Prime.RingHom
Goal:
R : Type u
inst : CommRing R
S : Type u_1
inst_1 : CommRing S
inst_2 : Algebra R S
p : PrimeSpectrum R
k : Type u := p.asIdeal.ResidueField
h : Nontrivial (p.asIdeal.ResidueField ⊗[R] S)
refine_1 :
  ∀ (m : Ideal (k ⊗[R] S)) (hm : m.IsMaximal),
    Membership.mem (γ := Set (PrimeSpectrum R)) (Set.range (ι := PrimeSpectrum S) (comap (algebraMap R S))) p
⊢ Membership.mem (γ := Set (PrimeSpectrum R)) (Set.range (ι := PrimeSpectrum S) (comap (algebraMap R S))) p

Tactic:
obtain ⟨m, hm⟩ := Ideal.exists_maximal (k ⊗[R] S)

Premises used: Ideal.exists_maximal, TensorProduct
-- Module: Mathlib.RingTheory.Spectrum.Prime.RingHom
Goal:
R : Type u
inst : CommRing R
S : Type u_1
inst_1 : CommRing S
inst_2 : Algebra R S
p : PrimeSpectrum R
k : Type u := p.asIdeal.ResidueField
h : Nontrivial (p.asIdeal.ResidueField ⊗[R] S)
m : Ideal (k ⊗[R] S)
hm : m.IsMaximal
h₁ :
  comap (algebraMap R S)
      (comap (S := k ⊗[R] S) (AlgHom.toRingHom Algebra.TensorProduct.includeRight) { asIdeal := m, isPrime := ⋯ }) =
    p
⊢ Membership.mem (γ := Set (PrimeSpectrum R)) (Set.range (ι := PrimeSpectrum S) (comap (algebraMap R S))) p

Tactic:
use PrimeSpectrum.comap (Algebra.TensorProduct.includeRight).toRingHom ⟨m, hm.isPrime⟩

Premises used: PrimeSpectrum.mk, Ideal.IsMaximal.isPrime, PrimeSpectrum.comap
-- Module: Mathlib.RingTheory.Spectrum.Prime.RingHom
Goal:
R : Type u
inst : CommRing R
S : Type u_1
inst_1 : CommRing S
inst_2 : Algebra R S
p : PrimeSpectrum R
k : Type u := p.asIdeal.ResidueField
h : Nontrivial (p.asIdeal.ResidueField ⊗[R] S)
m : Ideal (k ⊗[R] S)
hm : m.IsMaximal
h₁ :
  asIdeal
      (comap (algebraMap R S)
        (comap (S := k ⊗[R] S) (AlgHom.toRingHom Algebra.TensorProduct.includeRight) { asIdeal := m, isPrime := ⋯ })) =
    p.asIdeal
⊢ comap (algebraMap R S)
      (comap (S := k ⊗[R] S) (AlgHom.toRingHom Algebra.TensorProduct.includeRight) { asIdeal := m, isPrime := ⋯ }) =
    p

Tactic:
ext : 1
-- Module: Mathlib.RingTheory.Spectrum.Prime.RingHom
Goal:
R : Type u
inst : CommRing R
S : Type u_1
inst_1 : CommRing S
inst_2 : Algebra R S
p : PrimeSpectrum R
k : Type u := p.asIdeal.ResidueField
h : Nontrivial (p.asIdeal.ResidueField ⊗[R] S)
m : Ideal (k ⊗[R] S)
hm : m.IsMaximal
h₁ :
  asIdeal
      (comap (algebraMap R k)
        (comap (S := k ⊗[R] S) Algebra.TensorProduct.includeLeftRingHom { asIdeal := m, isPrime := ⋯ })) =
    p.asIdeal
⊢ asIdeal
      (comap (algebraMap R S)
        (comap (S := k ⊗[R] S) (AlgHom.toRingHom Algebra.TensorProduct.includeRight) { asIdeal := m, isPrime := ⋯ })) =
    p.asIdeal

Tactic:
rw [← PrimeSpectrum.comap_comp_apply,
      ← Algebra.TensorProduct.includeLeftRingHom_comp_algebraMap, comap_comp_apply]

Premises used: PrimeSpectrum.comap_comp_apply, Algebra.TensorProduct.includeLeftRingHom_comp_algebraMap
-- Module: Mathlib.RingTheory.Spectrum.Prime.RingHom
Goal:
R : Type u
inst : CommRing R
S : Type u_1
inst_1 : CommRing S
inst_2 : Algebra R S
p : PrimeSpectrum R
k : Type u := p.asIdeal.ResidueField
h : Nontrivial (p.asIdeal.ResidueField ⊗[R] S)
m : Ideal (k ⊗[R] S)
hm : m.IsMaximal
⊢ asIdeal
      (comap (algebraMap R k)
        (comap (S := k ⊗[R] S) Algebra.TensorProduct.includeLeftRingHom { asIdeal := m, isPrime := ⋯ })) =
    p.asIdeal

Tactic:
simp [Ideal.eq_bot_of_prime, k, ← RingHom.ker_eq_comap_bot]

Premises used: Ideal.eq_bot_of_prime, RingHom.ker_eq_comap_bot
-- Module: Mathlib.RingTheory.Spectrum.Prime.RingHom
Goal:
R : Type u
inst : CommRing R
S : Type u_1
inst_1 : CommRing S
inst_2 : Algebra R S
p : PrimeSpectrum R
k : Type u := p.asIdeal.ResidueField
h : Membership.mem (γ := Set (PrimeSpectrum R)) (Set.range (ι := PrimeSpectrum S) (comap (algebraMap R S))) p
refine_2 : ∀ (q : PrimeSpectrum S), Nontrivial (Ideal.ResidueField (asIdeal (comap (algebraMap R S) q)) ⊗[R] S)
⊢ Nontrivial (p.asIdeal.ResidueField ⊗[R] S)

Tactic:
obtain ⟨q, rfl⟩ := h

Premises used: rfl
-- Module: Mathlib.RingTheory.Spectrum.Prime.RingHom
Goal:
R : Type u
inst : CommRing R
S : Type u_1
inst_1 : CommRing S
inst_2 : Algebra R S
q : PrimeSpectrum S
k : Type u := Ideal.ResidueField (asIdeal (comap (algebraMap R S) q))
f : k ⊗[R] S →ₐ[R] q.asIdeal.ResidueField :=
  Algebra.TensorProduct.lift
    (Ideal.ResidueField.mapₐ (asIdeal (comap (algebraMap R S) q)) q.asIdeal (Algebra.ofId R S) ⋯)
    (IsScalarTower.toAlgHom R S q.asIdeal.ResidueField) ⋯
⊢ Nontrivial (Ideal.ResidueField (asIdeal (comap (algebraMap R S) q)) ⊗[R] S)

Tactic:
RingHom.domain_nontrivial f.toRingHom

Premises used: AlgHom.toRingHom, RingHom.domain_nontrivial
-- Module: Mathlib.RingTheory.Spectrum.Prime.RingHom
Goal:
R : Type u
inst : CommRing R
S : Type u_1
inst_1 : CommRing S
inst_2 : Algebra R S
q : PrimeSpectrum S
k : Type u := Ideal.ResidueField (asIdeal (comap (algebraMap R S) q))
f : k ⊗[R] S →ₐ[R] q.asIdeal.ResidueField :=
  Algebra.TensorProduct.lift
    (Ideal.ResidueField.mapₐ (asIdeal (comap (algebraMap R S) q)) q.asIdeal (Algebra.ofId R S) ⋯)
    (IsScalarTower.toAlgHom R S q.asIdeal.ResidueField) ⋯
⊢ Nontrivial (Ideal.ResidueField (asIdeal (comap (algebraMap R S) q)) ⊗[R] S)

Tactic:
exact RingHom.domain_nontrivial f.toRingHom

Premises used: AlgHom.toRingHom, RingHom.domain_nontrivial
-- Module: Mathlib.RingTheory.Spectrum.Prime.RingHom
Goal:
R : Type u
inst : CommRing R
S : Type u_1
inst_1 : CommRing S
f : R →+* S
hf : Surjective.{u + 1, u_1 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
⊢ StrictMono (comap f)

Tactic:
fun _ _ h ↦ (Ideal.relIsoOfSurjective _ hf).strictMono h

Premises used: StrictMono, OrderIso.strictMono, Ideal.relIsoOfSurjective
-- Module: Mathlib.RingTheory.Spectrum.Prime.RingHom
Goal:
R : Type u_1
inst : CommRing R
I : PrimeSpectrum R
rw : comap (S := I.asIdeal.ResidueField) (algebraMap R I.asIdeal.ResidueField) default = I
⊢ Eq (α := Set (PrimeSpectrum R))
    (Set.range (ι := PrimeSpectrum I.asIdeal.ResidueField) (comap (algebraMap R I.asIdeal.ResidueField))) {I}

Tactic:
rw [Set.range_unique, Set.singleton_eq_singleton_iff]

Premises used: Set.range_unique, Set.singleton_eq_singleton_iff
-- Module: Mathlib.RingTheory.Spectrum.Prime.RingHom
Goal:
R : Type u_1
inst : CommRing R
I : PrimeSpectrum R
⊢ comap (S := I.asIdeal.ResidueField) (algebraMap R I.asIdeal.ResidueField) default = I

Tactic:
PrimeSpectrum.ext (Ideal.ext fun x ↦ Ideal.algebraMap_residueField_eq_zero)

Premises used: PrimeSpectrum.ext, Ideal.ext, Ideal.algebraMap_residueField_eq_zero
-- Module: Mathlib.RingTheory.Spectrum.Prime.RingHom
Goal:
R : Type u_1
inst : CommRing R
I : PrimeSpectrum R
⊢ comap (S := I.asIdeal.ResidueField) (algebraMap R I.asIdeal.ResidueField) default = I

Tactic:
exact PrimeSpectrum.ext (Ideal.ext fun x ↦ Ideal.algebraMap_residueField_eq_zero)
-- 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 (comap f)
x : R
hfx : IsUnit.{v} (M := S) ((f : (a : R) → S) x : S)
by_contra : ∀ (hx : ¬IsUnit x), False
⊢ IsUnit x

Tactic:
by_contra hx
-- 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 (comap f)
x : R
hfx : IsUnit.{v} (M := S) ((f : (a : R) → S) x : S)
hx : ¬IsUnit x
obtain : ∀ (p : Ideal R) (hp : p.IsMaximal), x ∈ p → False
⊢ False

Tactic:
obtain ⟨p, hp, _⟩ := exists_max_ideal_of_mem_nonunits hx

Premises used: exists_max_ideal_of_mem_nonunits
-- 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 (comap f)
x : R
hfx : IsUnit.{v} (M := S) ((f : (a : R) → S) x : S)
hx : ¬IsUnit x
p : Ideal R
hp : p.IsMaximal
right : x ∈ p
obtain :
  ∀ (q : Ideal S) (hqp : q.IsPrime)
    (hq : comap f { asIdeal := q, isPrime := hqp : PrimeSpectrum S } = { asIdeal := p, isPrime := ⋯ }), False
⊢ False

Tactic:
obtain ⟨⟨q, hqp⟩, hq⟩ := hf ⟨p, hp.isPrime⟩

Premises used: PrimeSpectrum.mk, Ideal.IsMaximal.isPrime
-- 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 (comap f)
x : R
hfx : IsUnit.{v} (M := S) ((f : (a : R) → S) x : S)
hx : ¬IsUnit x
p : Ideal R
hp : p.IsMaximal
right : x ∈ p
q : Ideal S
hqp : q.IsPrime
hq : comap f { asIdeal := q, isPrime := hqp : PrimeSpectrum S } = { asIdeal := p, isPrime := ⋯ }
⊢ Ideal.comap f q = p

Tactic:
simp only [PrimeSpectrum.ext_iff, comap_asIdeal] at hq

Premises used: PrimeSpectrum.ext_iff, PrimeSpectrum.comap_asIdeal
-- 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 (comap f)
x : R
hfx : IsUnit.{v} (M := S) ((f : (a : R) → S) x : S)
hx : ¬IsUnit x
p : Ideal R
hp : p.IsMaximal
right : x ∈ p
q : Ideal S
hqp : q.IsPrime
hq : Ideal.comap f q = p
rwa rwa₁ rwa₂ rwa₃ : x ∈ p
⊢ Membership.mem (γ := Ideal R) (Ideal.comap f q) x

Tactic:
rwa [hq]
-- 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 (comap f)
x : R
hfx : IsUnit.{v} (M := S) ((f : (a : R) → S) x : S)
hx : ¬IsUnit x
p : Ideal R
hp : p.IsMaximal
right : x ∈ p
q : Ideal S
hqp : q.IsPrime
hq : Ideal.comap f q = p
⊢ False

Tactic:
exact hqp.ne_top (q.eq_top_of_isUnit_mem (q.mem_comap.mp (by rwa [hq])) hfx)

Premises used: Ideal.eq_top_of_isUnit_mem, Iff.mp, Ideal.IsPrime.ne_top, Ideal.mem_comap
-- Module: Mathlib.RingTheory.Spectrum.Prime.TensorProduct
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing T
inst_4 : Algebra R T
⊢ Continuous (X := PrimeSpectrum (S ⊗[R] T)) (tensorProductTo R S T)

Tactic:
(continuous_comap _).prodMk (continuous_comap _)

Premises used: PrimeSpectrum.continuous_comap, PrimeSpectrum.tensorProductTo, Continuous.prodMk
-- Module: Mathlib.RingTheory.Spectrum.Prime.TensorProduct
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing T
inst_4 : Algebra R T
hRT : RingHom.SurjectiveOnStalks (algebraMap R T)
p₁ p₂ : PrimeSpectrum (S ⊗[R] T)
h : tensorProductTo R S T p₁ = tensorProductTo R S T p₂
g : T →+* S ⊗[R] T := AlgHom.toRingHom Algebra.TensorProduct.includeRight
x : S ⊗[R] T
hxp₁ : x ∈ p₁.asIdeal
by_contra : ∀ (hxp₂ : x ∉ p₂.asIdeal), False
⊢ x ∈ p₂.asIdeal

Tactic:
by_contra hxp₂
-- Module: Mathlib.RingTheory.Spectrum.Prime.TensorProduct
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing T
inst_4 : Algebra R T
hRT : RingHom.SurjectiveOnStalks (algebraMap R T)
p₁ p₂ : PrimeSpectrum (S ⊗[R] T)
h : tensorProductTo R S T p₁ = tensorProductTo R S T p₂
g : T →+* S ⊗[R] T := AlgHom.toRingHom Algebra.TensorProduct.includeRight
x : S ⊗[R] T
hxp₁ : x ∈ p₁.asIdeal
hxp₂ : x ∉ p₂.asIdeal
obtain : ∀ (t : T) (r : R) (a : S) (ht : r • t ∉ Ideal.comap g p₂.asIdeal) (e : 1 ⊗ₜ[R] (r • t) * x = a ⊗ₜ[R] t), False
⊢ False

Tactic:
obtain ⟨t, r, a, ht, e⟩ := hRT.exists_mul_eq_tmul x
    (p₂.asIdeal.comap g) inferInstance

Premises used: RingHom.SurjectiveOnStalks.exists_mul_eq_tmul, inferInstance, Ideal.comap, PrimeSpectrum.asIdeal
-- Module: Mathlib.RingTheory.Spectrum.Prime.TensorProduct
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing T
inst_4 : Algebra R T
hRT : RingHom.SurjectiveOnStalks (algebraMap R T)
p₁ p₂ : PrimeSpectrum (S ⊗[R] T)
h : tensorProductTo R S T p₁ = tensorProductTo R S T p₂
g : T →+* S ⊗[R] T := AlgHom.toRingHom Algebra.TensorProduct.includeRight
x : S ⊗[R] T
hxp₁ : x ∈ p₁.asIdeal
hxp₂ : x ∉ p₂.asIdeal
t : T
r : R
a : S
ht : r • t ∉ Ideal.comap g p₂.asIdeal
e : 1 ⊗ₜ[R] (r • t) * x = a ⊗ₜ[R] t
⊢ a ⊗ₜ[R] t ∈ p₁.asIdeal

Tactic:
have h₁ : a ⊗ₜ[R] t ∈ p₁.asIdeal := e ▸ p₁.asIdeal.mul_mem_left (1 ⊗ₜ[R] (r • t)) hxp₁
-- Module: Mathlib.RingTheory.Spectrum.Prime.TensorProduct
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing T
inst_4 : Algebra R T
hRT : RingHom.SurjectiveOnStalks (algebraMap R T)
p₁ p₂ : PrimeSpectrum (S ⊗[R] T)
h : tensorProductTo R S T p₁ = tensorProductTo R S T p₂
g : T →+* S ⊗[R] T := AlgHom.toRingHom Algebra.TensorProduct.includeRight
x : S ⊗[R] T
hxp₁ : x ∈ p₁.asIdeal
hxp₂ : x ∉ p₂.asIdeal
t : T
r : R
a : S
ht : r • t ∉ Ideal.comap g p₂.asIdeal
e : 1 ⊗ₜ[R] (r • t) * x = a ⊗ₜ[R] t
h₁ : a ⊗ₜ[R] t ∈ p₁.asIdeal
⊢ a ⊗ₜ[R] t ∉ p₂.asIdeal

Tactic:
have h₂ : a ⊗ₜ[R] t ∉ p₂.asIdeal := e ▸ p₂.asIdeal.primeCompl.mul_mem ht hxp₂
-- Module: Mathlib.RingTheory.Spectrum.Prime.TensorProduct
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing T
inst_4 : Algebra R T
hRT : RingHom.SurjectiveOnStalks (algebraMap R T)
p₁ p₂ : PrimeSpectrum (S ⊗[R] T)
h : tensorProductTo R S T p₁ = tensorProductTo R S T p₂
g : T →+* S ⊗[R] T := AlgHom.toRingHom Algebra.TensorProduct.includeRight
x : S ⊗[R] T
hxp₁ : x ∈ p₁.asIdeal
hxp₂ : x ∉ p₂.asIdeal
t : T
r : R
a : S
ht : r • t ∉ Ideal.comap g p₂.asIdeal
e : 1 ⊗ₜ[R] (r • t) * x = a ⊗ₜ[R] t
h₁ : a ⊗ₜ[R] t ∈ p₁.asIdeal
h₂ : a ⊗ₜ[R] t ∉ p₂.asIdeal
⊢ HMul.hMul (α := S ⊗[R] T) (a ⊗ₜ[R] 1) (1 ⊗ₜ[R] t) ∈ p₁.asIdeal

Tactic:
rw [← mul_one a, ← one_mul t, ← Algebra.TensorProduct.tmul_mul_tmul] at h₁ h₂

Premises used: Algebra.TensorProduct.tmul_mul_tmul, mul_one, one_mul
-- Module: Mathlib.RingTheory.Spectrum.Prime.TensorProduct
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing T
inst_4 : Algebra R T
hRT : RingHom.SurjectiveOnStalks (algebraMap R T)
p₁ p₂ : PrimeSpectrum (S ⊗[R] T)
h : tensorProductTo R S T p₁ = tensorProductTo R S T p₂
g : T →+* S ⊗[R] T := AlgHom.toRingHom Algebra.TensorProduct.includeRight
x : S ⊗[R] T
hxp₁ : x ∈ p₁.asIdeal
hxp₂ : x ∉ p₂.asIdeal
t : T
r : R
a : S
ht : r • t ∉ Ideal.comap g p₂.asIdeal
e : 1 ⊗ₜ[R] (r • t) * x = a ⊗ₜ[R] t
h₁ : a ⊗ₜ[R] t ∈ p₁.asIdeal
h₂ : a ⊗ₜ[R] t ∉ p₂.asIdeal
h₃ : HMul.hMul (α := S ⊗[R] T) (a ⊗ₜ[R] 1) (1 ⊗ₜ[R] t) ∈ p₁.asIdeal
⊢ HMul.hMul (α := S ⊗[R] T) (a ⊗ₜ[R] 1) (1 ⊗ₜ[R] t) ∉ p₂.asIdeal

Tactic:
rw [← mul_one a, ← one_mul t, ← Algebra.TensorProduct.tmul_mul_tmul] at h₁ h₂

Premises used: Algebra.TensorProduct.tmul_mul_tmul, mul_one, one_mul
-- Module: Mathlib.RingTheory.Spectrum.Prime.TensorProduct
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing T
inst_4 : Algebra R T
hRT : RingHom.SurjectiveOnStalks (algebraMap R T)
p₁ p₂ : PrimeSpectrum (S ⊗[R] T)
h : tensorProductTo R S T p₁ = tensorProductTo R S T p₂
g : T →+* S ⊗[R] T := AlgHom.toRingHom Algebra.TensorProduct.includeRight
x : S ⊗[R] T
hxp₁ : x ∈ p₁.asIdeal
hxp₂ : x ∉ p₂.asIdeal
t : T
r : R
a : S
ht : r • t ∉ Ideal.comap g p₂.asIdeal
e : 1 ⊗ₜ[R] (r • t) * x = a ⊗ₜ[R] t
h₁ : HMul.hMul (α := S ⊗[R] T) (a ⊗ₜ[R] 1) (1 ⊗ₜ[R] t) ∈ p₁.asIdeal
h₂ : HMul.hMul (α := S ⊗[R] T) (a ⊗ₜ[R] 1) (1 ⊗ₜ[R] t) ∉ p₂.asIdeal
⊢ t ∉ Ideal.comap g p₂.asIdeal

Tactic:
have h₃ : t ∉ p₂.asIdeal.comap g := fun h ↦ h₂ (Ideal.mul_mem_left _ _ h)
-- Module: Mathlib.RingTheory.Spectrum.Prime.TensorProduct
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing T
inst_4 : Algebra R T
hRT : RingHom.SurjectiveOnStalks (algebraMap R T)
p₁ p₂ : PrimeSpectrum (S ⊗[R] T)
h : tensorProductTo R S T p₁ = tensorProductTo R S T p₂
g : T →+* S ⊗[R] T := AlgHom.toRingHom Algebra.TensorProduct.includeRight
x : S ⊗[R] T
hxp₁ : x ∈ p₁.asIdeal
hxp₂ : x ∉ p₂.asIdeal
t : T
r : R
a : S
ht : r • t ∉ Ideal.comap g p₂.asIdeal
e : 1 ⊗ₜ[R] (r • t) * x = a ⊗ₜ[R] t
h₁ : HMul.hMul (α := S ⊗[R] T) (a ⊗ₜ[R] 1) (1 ⊗ₜ[R] t) ∈ p₁.asIdeal
h₂ : HMul.hMul (α := S ⊗[R] T) (a ⊗ₜ[R] 1) (1 ⊗ₜ[R] t) ∉ p₂.asIdeal
h₃ : t ∉ Ideal.comap g p₂.asIdeal
⊢ a ∉ Ideal.comap (F := S →+* S ⊗[R] T) (algebraMap S (S ⊗[R] T)) p₂.asIdeal

Tactic:
have h₄ : a ∉ p₂.asIdeal.comap (algebraMap S (S ⊗[R] T)) :=
    fun h ↦ h₂ (Ideal.mul_mem_right _ _ h)
-- Module: Mathlib.RingTheory.Spectrum.Prime.TensorProduct
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing T
inst_4 : Algebra R T
hRT : RingHom.SurjectiveOnStalks (algebraMap R T)
p₁ p₂ : PrimeSpectrum (S ⊗[R] T)
h : tensorProductTo R S T p₁ = tensorProductTo R S T p₂
g : T →+* S ⊗[R] T := AlgHom.toRingHom Algebra.TensorProduct.includeRight
x : S ⊗[R] T
hxp₁ : x ∈ p₁.asIdeal
hxp₂ : x ∉ p₂.asIdeal
t : T
r : R
a : S
ht : r • t ∉ Ideal.comap g p₂.asIdeal
e : 1 ⊗ₜ[R] (r • t) * x = a ⊗ₜ[R] t
h₁ : HMul.hMul (α := S ⊗[R] T) (a ⊗ₜ[R] 1) (1 ⊗ₜ[R] t) ∈ p₁.asIdeal
h₂ : HMul.hMul (α := S ⊗[R] T) (a ⊗ₜ[R] 1) (1 ⊗ₜ[R] t) ∉ p₂.asIdeal
h₃ : t ∉ Ideal.comap g p₂.asIdeal
h₄ : a ∉ Ideal.comap (F := S →+* S ⊗[R] T) (algebraMap S (S ⊗[R] T)) p₂.asIdeal
rwa rwa₁ rwa₂ rwa₃ : t ∉ Ideal.comap g p₂.asIdeal
⊢ t ∉ Ideal.comap g p₁.asIdeal

Tactic:
rwa [show p₁.asIdeal.comap g = p₂.asIdeal.comap g from congr($h.2.1)]

Premises used: congrArg, id, Prod.snd, PrimeSpectrum.asIdeal