-- Mathlib/RingTheory/Localization/Ideal.lean
theorem isPrime_iff_isPrime_disjoint (J : Ideal S) :
    J.IsPrime ↔
      (Ideal.comap (algebraMap R S) J).IsPrime ∧
        Disjoint (M : Set R) ↑(Ideal.comap (algebraMap R S) J)

Proof state:
case mpr.refine_2.intro.intro.intro.intro
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
J : Ideal S
h : (Ideal.comap (algebraMap R S) J).IsPrime ∧ Disjoint ↑M ↑(Ideal.comap (algebraMap R S) J)
x y : S
hxy : x * y ∈ J
a : R
s : ↥M
ha : mk' S a s = x
b : R
t : ↥M
hb : mk' S b t = y
this : a * b ∈ Ideal.comap (algebraMap R S) J
this₂ : a ∈ Ideal.comap (algebraMap R S) J ∨ b ∈ Ideal.comap (algebraMap R S) J
⊢ x ∈ J ∨ y ∈ J

Tactic:
rw [Ideal.mem_comap, Ideal.mem_comap] at this₂

Result:
case mpr.refine_2.intro.intro.intro.intro
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
J : Ideal S
h : (Ideal.comap (algebraMap R S) J).IsPrime ∧ Disjoint ↑M ↑(Ideal.comap (algebraMap R S) J)
x y : S
hxy : x * y ∈ J
a : R
s : ↥M
ha : mk' S a s = x
b : R
t : ↥M
hb : mk' S b t = y
this : a * b ∈ Ideal.comap (algebraMap R S) J
this₂ : (algebraMap R S) a ∈ J ∨ (algebraMap R S) b ∈ J
⊢ x ∈ J ∨ y ∈ J

Proof state:
case mp.refine_2
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
J : Ideal S
h : J.IsPrime
x y : R
hxy : x * y ∈ Ideal.comap (algebraMap R S) J
⊢ x ∈ Ideal.comap (algebraMap R S) J ∨ y ∈ Ideal.comap (algebraMap R S) J

Tactic:
rw [Ideal.mem_comap, RingHom.map_mul] at hxy

Result:
case mp.refine_2
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
J : Ideal S
h : J.IsPrime
x y : R
hxy : (algebraMap R S) x * (algebraMap R S) y ∈ J
⊢ x ∈ Ideal.comap (algebraMap R S) J ∨ y ∈ Ideal.comap (algebraMap R S) J

Proof state:
case mpr.refine_2
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
J : Ideal S
h : (Ideal.comap (algebraMap R S) J).IsPrime ∧ Disjoint ↑M ↑(Ideal.comap (algebraMap R S) J)
x y : S
hxy : x * y ∈ J
⊢ x ∈ J ∨ y ∈ J

Tactic:
obtain ⟨a, s, ha⟩ := mk'_surjective M x

Result:
case mpr.refine_2.intro.intro
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
J : Ideal S
h : (Ideal.comap (algebraMap R S) J).IsPrime ∧ Disjoint ↑M ↑(Ideal.comap (algebraMap R S) J)
x y : S
hxy : x * y ∈ J
a : R
s : ↥M
ha : mk' S a s = x
⊢ x ∈ J ∨ y ∈ J

Proof state:
case mp.refine_1
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
J : Ideal S
h : J.IsPrime
⊢ Ideal.comap (algebraMap R S) J ≠ ⊤

Tactic:
refine fun hJ => h.ne_top ?_

Result:
case mp.refine_1
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
J : Ideal S
h : J.IsPrime
hJ : Ideal.comap (algebraMap R S) J = ⊤
⊢ J = ⊤

Proof state:
case mpr.refine_2.intro.intro.intro.intro
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
J : Ideal S
h : (Ideal.comap (algebraMap R S) J).IsPrime ∧ Disjoint ↑M ↑(Ideal.comap (algebraMap R S) J)
x y : S
hxy : x * y ∈ J
a : R
s : ↥M
ha : mk' S a s = x
b : R
t : ↥M
hb : mk' S b t = y
this : a * b ∈ Ideal.comap (algebraMap R S) J
⊢ x ∈ J ∨ y ∈ J

Tactic:
have this₂ := (h.1).mul_mem_iff_mem_or_mem.1 this

Result:
case mpr.refine_2.intro.intro.intro.intro
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
J : Ideal S
h : (Ideal.comap (algebraMap R S) J).IsPrime ∧ Disjoint ↑M ↑(Ideal.comap (algebraMap R S) J)
x y : S
hxy : x * y ∈ J
a : R
s : ↥M
ha : mk' S a s = x
b : R
t : ↥M
hb : mk' S b t = y
this : a * b ∈ Ideal.comap (algebraMap R S) J
this₂ : a ∈ Ideal.comap (algebraMap R S) J ∨ b ∈ Ideal.comap (algebraMap R S) J
⊢ x ∈ J ∨ y ∈ J

Proof state:
case mpr.refine_2.intro.intro.intro.intro
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
J : Ideal S
h : (Ideal.comap (algebraMap R S) J).IsPrime ∧ Disjoint ↑M ↑(Ideal.comap (algebraMap R S) J)
x y : S
hxy : x * y ∈ J
a : R
s : ↥M
ha : mk' S a s = x
b : R
t : ↥M
hb : mk' S b t = y
⊢ x ∈ J ∨ y ∈ J

Tactic:
have : mk' S (a * b) (s * t) ∈ J := by rwa [mk'_mul, ha, hb]

Result:
case mpr.refine_2.intro.intro.intro.intro
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
J : Ideal S
h : (Ideal.comap (algebraMap R S) J).IsPrime ∧ Disjoint ↑M ↑(Ideal.comap (algebraMap R S) J)
x y : S
hxy : x * y ∈ J
a : R
s : ↥M
ha : mk' S a s = x
b : R
t : ↥M
hb : mk' S b t = y
this : mk' S (a * b) (s * t) ∈ J
⊢ x ∈ J ∨ y ∈ J

Proof state:
case mp.refine_1
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
J : Ideal S
h : J.IsPrime
hJ : Ideal.comap (algebraMap R S) J = ⊤
⊢ J = ⊤

Tactic:
rw [eq_top_iff, ← (orderEmbedding M S).le_iff_le]

Result:
case mp.refine_1
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
J : Ideal S
h : J.IsPrime
hJ : Ideal.comap (algebraMap R S) J = ⊤
⊢ (orderEmbedding M S) ⊤ ≤ (orderEmbedding M S) J

Proof state:
case mp.refine_2
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
J : Ideal S
h : J.IsPrime
⊢ ∀ {x y : R},
    x * y ∈ Ideal.comap (algebraMap R S) J → x ∈ Ideal.comap (algebraMap R S) J ∨ y ∈ Ideal.comap (algebraMap R S) J

Tactic:
intro x y hxy

Result:
case mp.refine_2
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
J : Ideal S
h : J.IsPrime
x y : R
hxy : x * y ∈ Ideal.comap (algebraMap R S) J
⊢ x ∈ Ideal.comap (algebraMap R S) J ∨ y ∈ Ideal.comap (algebraMap R S) J