awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ t ∉ Ideal.comap g p₁.asIdeal

Tactic:
replace h₃ : t ∉ p₁.asIdeal.comap g := by
    rwa [show p₁.asIdeal.comap g = p₂.asIdeal.comap g from congr($h.2.1)]
-- 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₄ : a ∉ Ideal.comap (F := S →+* S ⊗[R] T) (algebraMap S (S ⊗[R] T)) p₂.asIdeal
h₃ : t ∉ Ideal.comap g p₁.asIdeal
rwa rwa₁ rwa₂ rwa₃ : a ∉ Ideal.comap (F := S →+* S ⊗[R] T) (algebraMap S (S ⊗[R] T)) p₂.asIdeal
⊢ a ∉ Ideal.comap (F := S →+* S ⊗[R] T) (algebraMap S (S ⊗[R] T)) p₁.asIdeal

Tactic:
rwa [show p₁.asIdeal.comap (algebraMap S (S ⊗[R] T)) = p₂.asIdeal.comap _ from congr($h.1.1)]

Premises used: congrArg, id, Prod.fst, 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
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₄ : a ∉ Ideal.comap (F := S →+* S ⊗[R] T) (algebraMap S (S ⊗[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:
replace h₄ : a ∉ p₁.asIdeal.comap (algebraMap S (S ⊗[R] T)) := by
    rwa [show p₁.asIdeal.comap (algebraMap S (S ⊗[R] T)) = p₂.asIdeal.comap _ from congr($h.1.1)]
-- 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
⊢ False

Tactic:
p₁.asIdeal.primeCompl.mul_mem h₄ h₃ h₁

Premises used: Submonoid.mul_mem, Ideal.primeCompl, 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
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
⊢ False

Tactic:
exact p₁.asIdeal.primeCompl.mul_mem h₄ h₃ h₁

Premises used: Submonoid.mul_mem, Ideal.primeCompl, 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)
⊢ IsEmbedding (X := PrimeSpectrum (S ⊗[R] T)) (tensorProductTo R S T)

Tactic:
⟨?_, fun p₁ p₂ e ↦
    (isEmbedding_tensorProductTo_of_surjectiveOnStalks_aux R S T hRT p₁ p₂ e).antisymm
      (isEmbedding_tensorProductTo_of_surjectiveOnStalks_aux R S T hRT p₂ p₁ e.symm)⟩

Premises used: LE.le.antisymm, PrimeSpectrum.isEmbedding_tensorProductTo_of_surjectiveOnStalks_aux, Eq.symm, Topology.IsEmbedding.mk
-- 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)
refine : IsInducing (X := PrimeSpectrum (S ⊗[R] T)) (tensorProductTo R S T)
⊢ IsEmbedding (X := PrimeSpectrum (S ⊗[R] T)) (tensorProductTo R S T)

Tactic:
refine ⟨?_, fun p₁ p₂ e ↦
    (isEmbedding_tensorProductTo_of_surjectiveOnStalks_aux R S T hRT p₁ p₂ e).antisymm
      (isEmbedding_tensorProductTo_of_surjectiveOnStalks_aux R S T hRT p₂ p₁ e.symm)⟩
-- 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)
g : T →+* S ⊗[R] T := AlgHom.toRingHom Algebra.TensorProduct.includeRight
⊢ IsInducing (X := PrimeSpectrum (S ⊗[R] T)) (tensorProductTo R S T)

Tactic:
⟨(continuous_tensorProductTo ..).le_induced.antisymm (isBasis_basic_opens.le_iff.mpr ?_)⟩

Premises used: Iff.mpr, LE.le.antisymm, Topology.IsInducing.mk, Continuous.le_induced, PrimeSpectrum.continuous_tensorProductTo, PrimeSpectrum.isBasis_basic_opens, TopologicalSpace.Opens.IsBasis.le_iff
-- 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)
g : T →+* S ⊗[R] T := AlgHom.toRingHom Algebra.TensorProduct.includeRight
refine :
  ∀ (U : TopologicalSpace.Opens (PrimeSpectrum (S ⊗[R] T))),
    Membership.mem (γ := Set (TopologicalSpace.Opens (PrimeSpectrum (S ⊗[R] T)))) (Set.range basicOpen) U →
      IsOpen[TopologicalSpace.induced (tensorProductTo R S T) instTopologicalSpaceProd]
        (↑U : Set (PrimeSpectrum (S ⊗[R] T)))
⊢ IsInducing (X := PrimeSpectrum (S ⊗[R] T)) (tensorProductTo R S T)

Tactic:
refine ⟨(continuous_tensorProductTo ..).le_induced.antisymm (isBasis_basic_opens.le_iff.mpr ?_)⟩
-- 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)
g : T →+* S ⊗[R] T := AlgHom.toRingHom Algebra.TensorProduct.includeRight
f : S ⊗[R] T
rw :
  ∀ x ∈ (↑(basicOpen f) : Set (PrimeSpectrum (S ⊗[R] T))),
    ∃ t ⊆ (↑(basicOpen f) : Set (PrimeSpectrum (S ⊗[R] T))),
      IsOpen[TopologicalSpace.induced (tensorProductTo R S T) instTopologicalSpaceProd] t ∧ x ∈ t
⊢ IsOpen[TopologicalSpace.induced (tensorProductTo R S T) instTopologicalSpaceProd]
    (↑(basicOpen f) : Set (PrimeSpectrum (S ⊗[R] T)))

Tactic:
rw [@isOpen_iff_forall_mem_open]

Premises used: isOpen_iff_forall_mem_open
-- 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)
g : T →+* S ⊗[R] T := AlgHom.toRingHom Algebra.TensorProduct.includeRight
f : S ⊗[R] T
J : PrimeSpectrum (S ⊗[R] T)
hJ : f ∉ J.asIdeal
obtain :
  ∀ (t : T) (r : R) (a : S) (ht : r • t ∉ Ideal.comap g J.asIdeal) (e : 1 ⊗ₜ[R] (r • t) * f = a ⊗ₜ[R] t),
    ∃ t ⊆ (↑(basicOpen f) : Set (PrimeSpectrum (S ⊗[R] T))),
      IsOpen[TopologicalSpace.induced (tensorProductTo R S T) instTopologicalSpaceProd] t ∧ J ∈ t
⊢ ∃ t ⊆ (↑(basicOpen f) : Set (PrimeSpectrum (S ⊗[R] T))),
    IsOpen[TopologicalSpace.induced (tensorProductTo R S T) instTopologicalSpaceProd] t ∧ J ∈ t

Tactic:
obtain ⟨t, r, a, ht, e⟩ := hRT.exists_mul_eq_tmul f
    (J.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)
g : T →+* S ⊗[R] T := AlgHom.toRingHom Algebra.TensorProduct.includeRight
f : S ⊗[R] T
J : PrimeSpectrum (S ⊗[R] T)
hJ : f ∉ J.asIdeal
t : T
r : R
a : S
ht : r • t ∉ Ideal.comap g J.asIdeal
e : 1 ⊗ₜ[R] (r • t) * f = a ⊗ₜ[R] t
⊢ ∃ t ⊆ (↑(basicOpen f) : Set (PrimeSpectrum (S ⊗[R] T))),
    IsOpen[TopologicalSpace.induced (tensorProductTo R S T) instTopologicalSpaceProd] t ∧ J ∈ t

Tactic:
⟨_, ?_, ⟨_, (basicOpen a).2.prod (basicOpen t).2, rfl⟩, ?_⟩

Premises used: PrimeSpectrum.basicOpen, And.intro, Exists.intro, TopologicalSpace.Opens.is_open', rfl, IsOpen.prod
-- 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)
g : T →+* S ⊗[R] T := AlgHom.toRingHom Algebra.TensorProduct.includeRight
f : S ⊗[R] T
J : PrimeSpectrum (S ⊗[R] T)
hJ : f ∉ J.asIdeal
t : T
r : R
a : S
ht : r • t ∉ Ideal.comap g J.asIdeal
e : 1 ⊗ₜ[R] (r • t) * f = a ⊗ₜ[R] t
refine_1 :
  tensorProductTo R S T ⁻¹'
      SProd.sprod (α := Set (PrimeSpectrum S)) (β := Set (PrimeSpectrum T))
        (TopologicalSpace.Opens.carrier (basicOpen a)) (TopologicalSpace.Opens.carrier (basicOpen t)) ⊆
    (↑(basicOpen f) : Set (PrimeSpectrum (S ⊗[R] T)))
refine_2 :
  Membership.mem (γ := Set (PrimeSpectrum (S ⊗[R] T)))
    (tensorProductTo R S T ⁻¹'
      SProd.sprod (α := Set (PrimeSpectrum S)) (β := Set (PrimeSpectrum T))
        (TopologicalSpace.Opens.carrier (basicOpen a)) (TopologicalSpace.Opens.carrier (basicOpen t)))
    J
⊢ ∃ t ⊆ (↑(basicOpen f) : Set (PrimeSpectrum (S ⊗[R] T))),
    IsOpen[TopologicalSpace.induced (tensorProductTo R S T) instTopologicalSpaceProd] t ∧ J ∈ t

Tactic:
refine ⟨_, ?_, ⟨_, (basicOpen a).2.prod (basicOpen t).2, rfl⟩, ?_⟩
-- 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)
g : T →+* S ⊗[R] T := AlgHom.toRingHom Algebra.TensorProduct.includeRight
f : S ⊗[R] T
J : PrimeSpectrum (S ⊗[R] T)
hJ : f ∉ J.asIdeal
t : T
r : R
a : S
ht : r • t ∉ Ideal.comap g J.asIdeal
e : 1 ⊗ₜ[R] (r • t) * f = a ⊗ₜ[R] t
x : PrimeSpectrum (S ⊗[R] T)
hx₁ : a ⊗ₜ[R] 1 ∉ x.asIdeal
hx₂ : 1 ⊗ₜ[R] t ∉ x.asIdeal
hx₃ : f ∈ x.asIdeal
refine_1 : HMul.hMul (α := S ⊗[R] T) (a ⊗ₜ[R] 1) (1 ⊗ₜ[R] t) ∈ (↑x.asIdeal : Set (S ⊗[R] T))
⊢ False

Tactic:
apply x.asIdeal.primeCompl.mul_mem hx₁ hx₂

Premises used: Submonoid.mul_mem, Ideal.primeCompl, 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)
g : T →+* S ⊗[R] T := AlgHom.toRingHom Algebra.TensorProduct.includeRight
f : S ⊗[R] T
J : PrimeSpectrum (S ⊗[R] T)
hJ : f ∉ J.asIdeal
t : T
r : R
a : S
ht : r • t ∉ Ideal.comap g J.asIdeal
e : 1 ⊗ₜ[R] (r • t) * f = a ⊗ₜ[R] t
x : PrimeSpectrum (S ⊗[R] T)
hx₁ : a ⊗ₜ[R] 1 ∉ x.asIdeal
hx₂ : 1 ⊗ₜ[R] t ∉ x.asIdeal
hx₃ : f ∈ x.asIdeal
refine_1 : 1 ⊗ₜ[R] (r • t) * f ∈ (↑x.asIdeal : Set (S ⊗[R] T))
⊢ HMul.hMul (α := S ⊗[R] T) (a ⊗ₜ[R] 1) (1 ⊗ₜ[R] t) ∈ (↑x.asIdeal : Set (S ⊗[R] T))

Tactic:
rw [Algebra.TensorProduct.tmul_mul_tmul, mul_one, one_mul, ← e]

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)
g : T →+* S ⊗[R] T := AlgHom.toRingHom Algebra.TensorProduct.includeRight
f : S ⊗[R] T
J : PrimeSpectrum (S ⊗[R] T)
hJ : f ∉ J.asIdeal
t : T
r : R
a : S
ht : r • t ∉ Ideal.comap g J.asIdeal
e : 1 ⊗ₜ[R] (r • t) * f = a ⊗ₜ[R] t
x : PrimeSpectrum (S ⊗[R] T)
hx₁ : a ⊗ₜ[R] 1 ∉ x.asIdeal
hx₂ : 1 ⊗ₜ[R] t ∉ x.asIdeal
hx₃ : f ∈ x.asIdeal
⊢ 1 ⊗ₜ[R] (r • t) * f ∈ (↑x.asIdeal : Set (S ⊗[R] T))

Tactic:
x.asIdeal.mul_mem_left _ hx₃

Premises used: Set.Mem, Ideal.mul_mem_left, 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)
g : T →+* S ⊗[R] T := AlgHom.toRingHom Algebra.TensorProduct.includeRight
f : S ⊗[R] T
J : PrimeSpectrum (S ⊗[R] T)
hJ : f ∉ J.asIdeal
t : T
r : R
a : S
ht : r • t ∉ Ideal.comap g J.asIdeal
e : 1 ⊗ₜ[R] (r • t) * f = a ⊗ₜ[R] t
x : PrimeSpectrum (S ⊗[R] T)
hx₁ : a ⊗ₜ[R] 1 ∉ x.asIdeal
hx₂ : 1 ⊗ₜ[R] t ∉ x.asIdeal
hx₃ : f ∈ x.asIdeal
⊢ 1 ⊗ₜ[R] (r • t) * f ∈ (↑x.asIdeal : Set (S ⊗[R] T))

Tactic:
exact x.asIdeal.mul_mem_left _ hx₃

Premises used: Ideal.mul_mem_left, 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)
g : T →+* S ⊗[R] T := AlgHom.toRingHom Algebra.TensorProduct.includeRight
f : S ⊗[R] T
J : PrimeSpectrum (S ⊗[R] T)
hJ : f ∉ J.asIdeal
t : T
r : R
a : S
ht : r • t ∉ Ideal.comap g J.asIdeal
e : 1 ⊗ₜ[R] (r • t) * f = a ⊗ₜ[R] t
rw : 1 ⊗ₜ[R] (r • t) * f ∉ J.asIdeal
⊢ HMul.hMul (α := S ⊗[R] T) (a ⊗ₜ[R] 1) (1 ⊗ₜ[R] t) ∉ J.asIdeal

Tactic:
rw [Algebra.TensorProduct.tmul_mul_tmul, mul_one, one_mul, ← e]

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)
g : T →+* S ⊗[R] T := AlgHom.toRingHom Algebra.TensorProduct.includeRight
f : S ⊗[R] T
J : PrimeSpectrum (S ⊗[R] T)
hJ : f ∉ J.asIdeal
t : T
r : R
a : S
ht : r • t ∉ Ideal.comap g J.asIdeal
e : 1 ⊗ₜ[R] (r • t) * f = a ⊗ₜ[R] t
⊢ 1 ⊗ₜ[R] (r • t) * f ∉ J.asIdeal

Tactic:
J.asIdeal.primeCompl.mul_mem ht hJ

Premises used: Submonoid.mul_mem, Set.Mem, setOf, Ideal.primeCompl, PrimeSpectrum.asIdeal, Not
-- 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)
g : T →+* S ⊗[R] T := AlgHom.toRingHom Algebra.TensorProduct.includeRight
f : S ⊗[R] T
J : PrimeSpectrum (S ⊗[R] T)
hJ : f ∉ J.asIdeal
t : T
r : R
a : S
ht : r • t ∉ Ideal.comap g J.asIdeal
e : 1 ⊗ₜ[R] (r • t) * f = a ⊗ₜ[R] t
⊢ 1 ⊗ₜ[R] (r • t) * f ∉ J.asIdeal

Tactic:
exact J.asIdeal.primeCompl.mul_mem ht hJ

Premises used: Submonoid.mul_mem, Ideal.primeCompl, 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)
g : T →+* S ⊗[R] T := AlgHom.toRingHom Algebra.TensorProduct.includeRight
f : S ⊗[R] T
J : PrimeSpectrum (S ⊗[R] T)
hJ : f ∉ J.asIdeal
t : T
r : R
a : S
ht : r • t ∉ Ideal.comap g J.asIdeal
e : 1 ⊗ₜ[R] (r • t) * f = a ⊗ₜ[R] t
⊢ HMul.hMul (α := S ⊗[R] T) (a ⊗ₜ[R] 1) (1 ⊗ₜ[R] t) ∉ J.asIdeal

Tactic:
have : a ⊗ₜ[R] (1 : T) * (1 : S) ⊗ₜ[R] t ∉ J.asIdeal := by
      rw [Algebra.TensorProduct.tmul_mul_tmul, mul_one, one_mul, ← e]
      exact J.asIdeal.primeCompl.mul_mem ht hJ
-- 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)
g : T →+* S ⊗[R] T := AlgHom.toRingHom Algebra.TensorProduct.includeRight
f : S ⊗[R] T
J : PrimeSpectrum (S ⊗[R] T)
hJ : f ∉ J.asIdeal
t : T
r : R
a : S
ht : r • t ∉ Ideal.comap g J.asIdeal
e : 1 ⊗ₜ[R] (r • t) * f = a ⊗ₜ[R] t
this : HMul.hMul (α := S ⊗[R] T) (a ⊗ₜ[R] 1) (1 ⊗ₜ[R] t) ∉ J.asIdeal
refine_2 :
  ∀ (this : ¬(a ⊗ₜ[R] 1 ∈ J.asIdeal ∨ 1 ⊗ₜ[R] t ∈ J.asIdeal)),
    Membership.mem (γ := Set (PrimeSpectrum (S ⊗[R] T)))
      (tensorProductTo R S T ⁻¹'
        SProd.sprod (α := Set (PrimeSpectrum S)) (β := Set (PrimeSpectrum T))
          (TopologicalSpace.Opens.carrier (basicOpen a)) (TopologicalSpace.Opens.carrier (basicOpen t)))
      J
refine_2₁ refine_2₂ refine_2₃ refine_2₄ :
  ∀ (this : a ⊗ₜ[R] 1 ∉ J.asIdeal ∧ 1 ⊗ₜ[R] t ∉ J.asIdeal),
    Membership.mem (γ := Set (PrimeSpectrum (S ⊗[R] T)))
      (tensorProductTo R S T ⁻¹'
        SProd.sprod (α := Set (PrimeSpectrum S)) (β := Set (PrimeSpectrum T))
          (TopologicalSpace.Opens.carrier (basicOpen a)) (TopologicalSpace.Opens.carrier (basicOpen t)))
      J
⊢ Membership.mem (γ := Set (PrimeSpectrum (S ⊗[R] T)))
    (tensorProductTo R S T ⁻¹'
      SProd.sprod (α := Set (PrimeSpectrum S)) (β := Set (PrimeSpectrum T))
        (TopologicalSpace.Opens.carrier (basicOpen a)) (TopologicalSpace.Opens.carrier (basicOpen t)))
    J

Tactic:
rwa [J.isPrime.mul_mem_iff_mem_or_mem.not, not_or] at this

Premises used: PrimeSpectrum.isPrime, Iff.not, not_or, Ideal.IsPrime.mul_mem_iff_mem_or_mem
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
⊢ Eq.{u + 1} (α := Set (PrimeSpectrum R)) (zeroLocus Set.univ) ∅

Tactic:
simp
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
Zs : Set (Set (PrimeSpectrum R))
h : Zs ⊆ Set.range zeroLocus
rw :
  Membership.mem (γ := Set (Set (PrimeSpectrum R))) (Set.range zeroLocus)
    (⋂ (i : (↑Zs : Type u)), (↑i : Set (PrimeSpectrum R)))
⊢ Membership.mem (γ := Set (Set (PrimeSpectrum R))) (Set.range zeroLocus) (⋂₀ Zs)

Tactic:
rw [Set.sInter_eq_iInter]

Premises used: Set.sInter_eq_iInter
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
Zs : Set (Set (PrimeSpectrum R))
h : Zs ⊆ Set.range zeroLocus
choose :
  ∀ (f : (i : (↑Zs : Type u)) → Set R) (hf : ∀ (i : (↑Zs : Type u)), zeroLocus (f i) = (↑i : Set (PrimeSpectrum R))),
    Membership.mem (γ := Set (Set (PrimeSpectrum R))) (Set.range zeroLocus)
      (⋂ (i : (↑Zs : Type u)), (↑i : Set (PrimeSpectrum R)))
⊢ Membership.mem (γ := Set (Set (PrimeSpectrum R))) (Set.range zeroLocus)
    (⋂ (i : (↑Zs : Type u)), (↑i : Set (PrimeSpectrum R)))

Tactic:
choose f hf using fun i : Zs => h i.prop

Premises used: Subtype.prop
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
Zs : Set (Set (PrimeSpectrum R))
h : Zs ⊆ Set.range zeroLocus
f : (i : (↑Zs : Type u)) → Set R
hf : ∀ (i : (↑Zs : Type u)), zeroLocus (f i) = (↑i : Set (PrimeSpectrum R))
simp : Membership.mem (γ := Set (Set (PrimeSpectrum R))) (Set.range zeroLocus) (⋂ (i : (↑Zs : Type u)), zeroLocus (f i))
⊢ Membership.mem (γ := Set (Set (PrimeSpectrum R))) (Set.range zeroLocus)
    (⋂ (i : (↑Zs : Type u)), (↑i : Set (PrimeSpectrum R)))

Tactic:
simp only [← hf]
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
Zs : Set (Set (PrimeSpectrum R))
h : Zs ⊆ Set.range zeroLocus
f : (i : (↑Zs : Type u)) → Set R
hf : ∀ (i : (↑Zs : Type u)), zeroLocus (f i) = (↑i : Set (PrimeSpectrum R))
⊢ Membership.mem (γ := Set (Set (PrimeSpectrum R))) (Set.range zeroLocus) (⋂ (i : (↑Zs : Type u)), zeroLocus (f i))

Tactic:
⟨_, zeroLocus_iUnion _⟩

Premises used: Set.Mem, setOf, PrimeSpectrum.zeroLocus_iUnion, Exists.intro, Set.range
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
Zs : Set (Set (PrimeSpectrum R))
h : Zs ⊆ Set.range zeroLocus
f : (i : (↑Zs : Type u)) → Set R
hf : ∀ (i : (↑Zs : Type u)), zeroLocus (f i) = (↑i : Set (PrimeSpectrum R))
⊢ Membership.mem (γ := Set (Set (PrimeSpectrum R))) (Set.range zeroLocus) (⋂ (i : (↑Zs : Type u)), zeroLocus (f i))

Tactic:
exact ⟨_, zeroLocus_iUnion _⟩
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
s t : Set R
⊢ Membership.mem (γ := Set (Set (PrimeSpectrum R))) (Set.range zeroLocus) (zeroLocus s ∪ zeroLocus t)

Tactic:
⟨_, (union_zeroLocus s t).symm⟩

Premises used: Set.Mem, PrimeSpectrum.union_zeroLocus, setOf, Exists.intro, Set.range, Eq.symm
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
s t : Set R
⊢ Membership.mem (γ := Set (Set (PrimeSpectrum R))) (Set.range zeroLocus) (zeroLocus s ∪ zeroLocus t)

Tactic:
exact ⟨_, (union_zeroLocus s t).symm⟩
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
U : Set (PrimeSpectrum R)
simp : IsOpen U ↔ ∃ (s : Set R), zeroLocus s = Uᶜ
⊢ IsOpen U ↔ ∃ (s : Set R), Uᶜ = zeroLocus s

Tactic:
simp only [@eq_comm _ Uᶜ]

Premises used: eq_comm
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
U : Set (PrimeSpectrum R)
⊢ IsOpen U ↔ ∃ (s : Set R), zeroLocus s = Uᶜ

Tactic:
rfl
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
Z : Set (PrimeSpectrum R)
rw : IsOpen Zᶜ ↔ ∃ (s : Set R), Z = zeroLocus s
rw₁ : (∃ (s : Set R), Zᶜᶜ = zeroLocus s) ↔ ∃ (s : Set R), Z = zeroLocus s
rw₂ rw₃ : (∃ (s : Set R), Z = zeroLocus s) ↔ ∃ (s : Set R), Z = zeroLocus s
⊢ IsClosed Z ↔ ∃ (s : Set R), Z = zeroLocus s

Tactic:
rw [← isOpen_compl_iff, isOpen_iff, compl_compl]

Premises used: compl_compl, PrimeSpectrum.isOpen_iff, isOpen_compl_iff