-- Mathlib/RingTheory/Spectrum/Prime/TensorProduct.lean
lemma PrimeSpectrum.isEmbedding_tensorProductTo_of_surjectiveOnStalks_aux
    (p₁ p₂ : PrimeSpectrum (S ⊗[R] T))
    (h : tensorProductTo R S T p₁ = tensorProductTo R S T p₂) :
    p₁ ≤ p₂

Proof state:
case intro.intro.intro.intro
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : CommRing T
inst✝ : Algebra R T
hRT : (algebraMap R T).SurjectiveOnStalks
p₁ p₂ : PrimeSpectrum (S ⊗[R] T)
h : tensorProductTo R S T p₁ = tensorProductTo R S T p₂
g : T →+* S ⊗[R] T := Algebra.TensorProduct.includeRight.toRingHom
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] 1 * 1 ⊗ₜ[R] t ∈ p₁.asIdeal
h₂ : a ⊗ₜ[R] 1 * 1 ⊗ₜ[R] t ∉ p₂.asIdeal
h₃ : t ∉ Ideal.comap g p₂.asIdeal
⊢ False

Tactic:
have h₄ : a ∉ p₂.asIdeal.comap (algebraMap S (S ⊗[R] T)) :=
  fun h ↦ h₂ (Ideal.mul_mem_right _ _ h)

Result:
case intro.intro.intro.intro
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : CommRing T
inst✝ : Algebra R T
hRT : (algebraMap R T).SurjectiveOnStalks
p₁ p₂ : PrimeSpectrum (S ⊗[R] T)
h : tensorProductTo R S T p₁ = tensorProductTo R S T p₂
g : T →+* S ⊗[R] T := Algebra.TensorProduct.includeRight.toRingHom
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] 1 * 1 ⊗ₜ[R] t ∈ p₁.asIdeal
h₂ : a ⊗ₜ[R] 1 * 1 ⊗ₜ[R] t ∉ p₂.asIdeal
h₃ : t ∉ Ideal.comap g p₂.asIdeal
h₄ : a ∉ Ideal.comap (algebraMap S (S ⊗[R] T)) p₂.asIdeal
⊢ False

Proof state:
case intro.intro.intro.intro
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : CommRing T
inst✝ : Algebra R T
hRT : (algebraMap R T).SurjectiveOnStalks
p₁ p₂ : PrimeSpectrum (S ⊗[R] T)
h : tensorProductTo R S T p₁ = tensorProductTo R S T p₂
g : T →+* S ⊗[R] T := Algebra.TensorProduct.includeRight.toRingHom
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] 1 * 1 ⊗ₜ[R] t ∈ p₁.asIdeal
h₂ : a ⊗ₜ[R] 1 * 1 ⊗ₜ[R] t ∉ p₂.asIdeal
h₄ : a ∉ Ideal.comap (algebraMap S (S ⊗[R] T)) p₂.asIdeal
h₃ : t ∉ Ideal.comap g p₁.asIdeal
⊢ False

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)]

Result:
case intro.intro.intro.intro
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : CommRing T
inst✝ : Algebra R T
hRT : (algebraMap R T).SurjectiveOnStalks
p₁ p₂ : PrimeSpectrum (S ⊗[R] T)
h : tensorProductTo R S T p₁ = tensorProductTo R S T p₂
g : T →+* S ⊗[R] T := Algebra.TensorProduct.includeRight.toRingHom
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] 1 * 1 ⊗ₜ[R] t ∈ p₁.asIdeal
h₂ : a ⊗ₜ[R] 1 * 1 ⊗ₜ[R] t ∉ p₂.asIdeal
h₃ : t ∉ Ideal.comap g p₁.asIdeal
h₄ : a ∉ Ideal.comap (algebraMap S (S ⊗[R] T)) p₁.asIdeal
⊢ False

Proof state:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : CommRing T
inst✝ : Algebra R T
hRT : (algebraMap R T).SurjectiveOnStalks
p₁ p₂ : PrimeSpectrum (S ⊗[R] T)
h : tensorProductTo R S T p₁ = tensorProductTo R S T p₂
g : T →+* S ⊗[R] T := Algebra.TensorProduct.includeRight.toRingHom
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] 1 * 1 ⊗ₜ[R] t ∈ p₁.asIdeal
h₂ : a ⊗ₜ[R] 1 * 1 ⊗ₜ[R] t ∉ p₂.asIdeal
h₃ : t ∉ Ideal.comap g p₂.asIdeal
h₄ : a ∉ Ideal.comap (algebraMap S (S ⊗[R] T)) p₂.asIdeal
⊢ t ∉ Ideal.comap g p₁.asIdeal

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

Result:
no goals

Proof state:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : CommRing T
inst✝ : Algebra R T
hRT : (algebraMap R T).SurjectiveOnStalks
p₁ p₂ : PrimeSpectrum (S ⊗[R] T)
h : tensorProductTo R S T p₁ = tensorProductTo R S T p₂
g : T →+* S ⊗[R] T := Algebra.TensorProduct.includeRight.toRingHom
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] 1 * 1 ⊗ₜ[R] t ∈ p₁.asIdeal
h₂ : a ⊗ₜ[R] 1 * 1 ⊗ₜ[R] t ∉ p₂.asIdeal
h₄ : a ∉ Ideal.comap (algebraMap S (S ⊗[R] T)) p₂.asIdeal
h₃ : t ∉ Ideal.comap g p₁.asIdeal
⊢ a ∉ Ideal.comap (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)]

Result:
no goals

Proof state:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : CommRing T
inst✝ : Algebra R T
hRT : (algebraMap R T).SurjectiveOnStalks
p₁ p₂ : PrimeSpectrum (S ⊗[R] T)
h : tensorProductTo R S T p₁ = tensorProductTo R S T p₂
g : T →+* S ⊗[R] T := Algebra.TensorProduct.includeRight.toRingHom
⊢ p₁ ≤ p₂

Tactic:
intros x hxp₁

Result:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : CommRing T
inst✝ : Algebra R T
hRT : (algebraMap R T).SurjectiveOnStalks
p₁ p₂ : PrimeSpectrum (S ⊗[R] T)
h : tensorProductTo R S T p₁ = tensorProductTo R S T p₂
g : T →+* S ⊗[R] T := Algebra.TensorProduct.includeRight.toRingHom
x : S ⊗[R] T
hxp₁ : x ∈ p₁.asIdeal
⊢ x ∈ p₂.asIdeal

Proof state:
case intro.intro.intro.intro
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : CommRing T
inst✝ : Algebra R T
hRT : (algebraMap R T).SurjectiveOnStalks
p₁ p₂ : PrimeSpectrum (S ⊗[R] T)
h : tensorProductTo R S T p₁ = tensorProductTo R S T p₂
g : T →+* S ⊗[R] T := Algebra.TensorProduct.includeRight.toRingHom
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
⊢ False

Tactic:
have h₂ : a ⊗ₜ[R] t ∉ p₂.asIdeal := e ▸ p₂.asIdeal.primeCompl.mul_mem ht hxp₂

Result:
case intro.intro.intro.intro
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : CommRing T
inst✝ : Algebra R T
hRT : (algebraMap R T).SurjectiveOnStalks
p₁ p₂ : PrimeSpectrum (S ⊗[R] T)
h : tensorProductTo R S T p₁ = tensorProductTo R S T p₂
g : T →+* S ⊗[R] T := Algebra.TensorProduct.includeRight.toRingHom
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
⊢ False

Proof state:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : CommRing T
inst✝ : Algebra R T
hRT : (algebraMap R T).SurjectiveOnStalks
p₁ p₂ : PrimeSpectrum (S ⊗[R] T)
h : tensorProductTo R S T p₁ = tensorProductTo R S T p₂
g : T →+* S ⊗[R] T := Algebra.TensorProduct.includeRight.toRingHom
x : S ⊗[R] T
hxp₁ : x ∈ p₁.asIdeal
⊢ x ∈ p₂.asIdeal

Tactic:
by_contra hxp₂

Result:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : CommRing T
inst✝ : Algebra R T
hRT : (algebraMap R T).SurjectiveOnStalks
p₁ p₂ : PrimeSpectrum (S ⊗[R] T)
h : tensorProductTo R S T p₁ = tensorProductTo R S T p₂
g : T →+* S ⊗[R] T := Algebra.TensorProduct.includeRight.toRingHom
x : S ⊗[R] T
hxp₁ : x ∈ p₁.asIdeal
hxp₂ : x ∉ p₂.asIdeal
⊢ False