case mp
R : Type u_2
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_1
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
J : Ideal S
⊢ Ideal.IsPrime J → Ideal.IsPrime (Ideal.comap (algebraMap R S) J) ∧ Disjoint ↑M ↑(Ideal.comap (algebraMap R S) J)

case mpr
R : Type u_2
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_1
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
J : Ideal S
⊢ Ideal.IsPrime (Ideal.comap (algebraMap R S) J) ∧ Disjoint ↑M ↑(Ideal.comap (algebraMap R S) J) → Ideal.IsPrime J
R : Type u_2
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_1
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
J : Ideal S
⊢ Ideal.IsPrime J ↔ Ideal.IsPrime (Ideal.comap (algebraMap R S) J) ∧ Disjoint ↑M ↑(Ideal.comap (algebraMap R S) J)
constructor
case mp.refine'_1
R : Type u_2
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_1
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
J : Ideal S
h : Ideal.IsPrime J
⊢ Ideal.comap (algebraMap R S) J ≠ ⊤

case mp.refine'_2
R : Type u_2
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_1
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
J : Ideal S
h : Ideal.IsPrime J
⊢ ∀ {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
case mp
R : Type u_2
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_1
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
J : Ideal S
⊢ Ideal.IsPrime J → Ideal.IsPrime (Ideal.comap (algebraMap R S) J) ∧ Disjoint ↑M ↑(Ideal.comap (algebraMap R S) J)
refine' fun h =>
  ⟨⟨_, _⟩,
    Set.disjoint_left.mpr fun m hm1 hm2 =>
      h.ne_top (Ideal.eq_top_of_isUnit_mem _ hm2 (map_units S ⟨m, hm1⟩))⟩
case mp.refine'_1
R : Type u_2
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_1
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
J : Ideal S
h : Ideal.IsPrime J
hJ : Ideal.comap (algebraMap R S) J = ⊤
⊢ J = ⊤
case mp.refine'_1
R : Type u_2
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_1
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
J : Ideal S
h : Ideal.IsPrime J
⊢ Ideal.comap (algebraMap R S) J ≠ ⊤
refine' fun hJ => h.ne_top _
case mp.refine'_1
R : Type u_2
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_1
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
J : Ideal S
h : Ideal.IsPrime J
hJ : Ideal.comap (algebraMap R S) J = ⊤
⊢ ↑(orderEmbedding M S) ⊤ ≤ ↑(orderEmbedding M S) J
case mp.refine'_1
R : Type u_2
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_1
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
J : Ideal S
h : Ideal.IsPrime J
hJ : Ideal.comap (algebraMap R S) J = ⊤
⊢ J = ⊤
rw [eq_top_iff, ← (orderEmbedding M S).le_iff_le]
no goals
case mp.refine'_1
R : Type u_2
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_1
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
J : Ideal S
h : Ideal.IsPrime J
hJ : Ideal.comap (algebraMap R S) J = ⊤
⊢ ↑(orderEmbedding M S) ⊤ ≤ ↑(orderEmbedding M S) J
exact le_of_eq hJ.symm
case mp.refine'_2
R : Type u_2
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_1
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
J : Ideal S
h : Ideal.IsPrime J
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
case mp.refine'_2
R : Type u_2
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_1
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
J : Ideal S
h : Ideal.IsPrime J
⊢ ∀ {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
intro x y hxy
case mp.refine'_2
R : Type u_2
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_1
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
J : Ideal S
h : Ideal.IsPrime J
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
case mp.refine'_2
R : Type u_2
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_1
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
J : Ideal S
h : Ideal.IsPrime J
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
rw [Ideal.mem_comap, RingHom.map_mul] at hxy
no goals
case mp.refine'_2
R : Type u_2
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_1
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
J : Ideal S
h : Ideal.IsPrime J
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
exact h.mem_or_mem hxy
case mpr.refine'_1
R : Type u_2
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_1
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
J : Ideal S
h : Ideal.IsPrime (Ideal.comap (algebraMap R S) J) ∧ Disjoint ↑M ↑(Ideal.comap (algebraMap R S) J)
hJ : J = ⊤
⊢ ⊤ ≤ Ideal.comap (algebraMap R S) J

case mpr.refine'_2
R : Type u_2
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_1
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
J : Ideal S
h : Ideal.IsPrime (Ideal.comap (algebraMap R S) J) ∧ Disjoint ↑M ↑(Ideal.comap (algebraMap R S) J)
⊢ ∀ {x y : S}, x * y ∈ J → x ∈ J ∨ y ∈ J
case mpr
R : Type u_2
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_1
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
J : Ideal S
⊢ Ideal.IsPrime (Ideal.comap (algebraMap R S) J) ∧ Disjoint ↑M ↑(Ideal.comap (algebraMap R S) J) → Ideal.IsPrime J
refine' fun h => ⟨fun hJ => h.left.ne_top (eq_top_iff.2 _), _⟩
no goals
case mpr.refine'_1
R : Type u_2
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_1
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
J : Ideal S
h : Ideal.IsPrime (Ideal.comap (algebraMap R S) J) ∧ Disjoint ↑M ↑(Ideal.comap (algebraMap R S) J)
hJ : J = ⊤
⊢ ⊤ ≤ Ideal.comap (algebraMap R S) J
rwa [eq_top_iff, ← (orderEmbedding M S).le_iff_le] at hJ
case mpr.refine'_2
R : Type u_2
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_1
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
J : Ideal S
h : Ideal.IsPrime (Ideal.comap (algebraMap R S) J) ∧ Disjoint ↑M ↑(Ideal.comap (algebraMap R S) J)
x y : S
hxy : x * y ∈ J
⊢ x ∈ J ∨ y ∈ J
case mpr.refine'_2
R : Type u_2
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_1
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
J : Ideal S
h : Ideal.IsPrime (Ideal.comap (algebraMap R S) J) ∧ Disjoint ↑M ↑(Ideal.comap (algebraMap R S) J)
⊢ ∀ {x y : S}, x * y ∈ J → x ∈ J ∨ y ∈ J
intro x y hxy
case mpr.refine'_2.intro.intro
R : Type u_2
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_1
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
J : Ideal S
h : Ideal.IsPrime (Ideal.comap (algebraMap R S) J) ∧ Disjoint ↑M ↑(Ideal.comap (algebraMap R S) J)
x y : S
hxy : x * y ∈ J
a : R
s : { x // x ∈ M }
ha : mk' S a s = x
⊢ x ∈ J ∨ y ∈ J
case mpr.refine'_2
R : Type u_2
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_1
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
J : Ideal S
h : Ideal.IsPrime (Ideal.comap (algebraMap R S) J) ∧ Disjoint ↑M ↑(Ideal.comap (algebraMap R S) J)
x y : S
hxy : x * y ∈ J
⊢ x ∈ J ∨ y ∈ J
obtain ⟨a, s, ha⟩ := mk'_surjective M x
case mpr.refine'_2.intro.intro.intro.intro
R : Type u_2
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_1
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
J : Ideal S
h : Ideal.IsPrime (Ideal.comap (algebraMap R S) J) ∧ Disjoint ↑M ↑(Ideal.comap (algebraMap R S) J)
x y : S
hxy : x * y ∈ J
a : R
s : { x // x ∈ M }
ha : mk' S a s = x
b : R
t : { x // x ∈ M }
hb : mk' S b t = y
⊢ x ∈ J ∨ y ∈ J
case mpr.refine'_2.intro.intro
R : Type u_2
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_1
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
J : Ideal S
h : Ideal.IsPrime (Ideal.comap (algebraMap R S) J) ∧ Disjoint ↑M ↑(Ideal.comap (algebraMap R S) J)
x y : S
hxy : x * y ∈ J
a : R
s : { x // x ∈ M }
ha : mk' S a s = x
⊢ x ∈ J ∨ y ∈ J
obtain ⟨b, t, hb⟩ := mk'_surjective M y
case mpr.refine'_2.intro.intro.intro.intro
R : Type u_2
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_1
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
J : Ideal S
h : Ideal.IsPrime (Ideal.comap (algebraMap R S) J) ∧ Disjoint ↑M ↑(Ideal.comap (algebraMap R S) J)
x y : S
hxy : x * y ∈ J
a : R
s : { x // x ∈ M }
ha : mk' S a s = x
b : R
t : { x // x ∈ M }
hb : mk' S b t = y
this : mk' S (a * b) (s * t) ∈ J
⊢ x ∈ J ∨ y ∈ J
case mpr.refine'_2.intro.intro.intro.intro
R : Type u_2
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_1
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
J : Ideal S
h : Ideal.IsPrime (Ideal.comap (algebraMap R S) J) ∧ Disjoint ↑M ↑(Ideal.comap (algebraMap R S) J)
x y : S
hxy : x * y ∈ J
a : R
s : { x // x ∈ M }
ha : mk' S a s = x
b : R
t : { x // x ∈ M }
hb : mk' S b t = y
⊢ x ∈ J ∨ y ∈ J
have : mk' S (a * b) (s * t) ∈ J := by rwa [mk'_mul, ha, hb]
case mpr.refine'_2.intro.intro.intro.intro
R : Type u_2
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_1
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
J : Ideal S
h : Ideal.IsPrime (Ideal.comap (algebraMap R S) J) ∧ Disjoint ↑M ↑(Ideal.comap (algebraMap R S) J)
x y : S
hxy : x * y ∈ J
a : R
s : { x // x ∈ M }
ha : mk' S a s = x
b : R
t : { x // x ∈ M }
hb : mk' S b t = y
this : a * b ∈ Ideal.comap (algebraMap R S) J
⊢ x ∈ J ∨ y ∈ J
case mpr.refine'_2.intro.intro.intro.intro
R : Type u_2
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_1
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
J : Ideal S
h : Ideal.IsPrime (Ideal.comap (algebraMap R S) J) ∧ Disjoint ↑M ↑(Ideal.comap (algebraMap R S) J)
x y : S
hxy : x * y ∈ J
a : R
s : { x // x ∈ M }
ha : mk' S a s = x
b : R
t : { x // x ∈ M }
hb : mk' S b t = y
this : mk' S (a * b) (s * t) ∈ J
⊢ x ∈ J ∨ y ∈ J
rw [mk'_mem_iff, ← Ideal.mem_comap] at this
case mpr.refine'_2.intro.intro.intro.intro
R : Type u_2
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_1
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
J : Ideal S
h : Ideal.IsPrime (Ideal.comap (algebraMap R S) J) ∧ Disjoint ↑M ↑(Ideal.comap (algebraMap R S) J)
x y : S
hxy : x * y ∈ J
a : R
s : { x // x ∈ M }
ha : mk' S a s = x
b : R
t : { x // x ∈ 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
case mpr.refine'_2.intro.intro.intro.intro
R : Type u_2
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_1
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
J : Ideal S
h : Ideal.IsPrime (Ideal.comap (algebraMap R S) J) ∧ Disjoint ↑M ↑(Ideal.comap (algebraMap R S) J)
x y : S
hxy : x * y ∈ J
a : R
s : { x // x ∈ M }
ha : mk' S a s = x
b : R
t : { x // x ∈ M }
hb : mk' S b t = y
this : a * b ∈ Ideal.comap (algebraMap R S) J
⊢ x ∈ J ∨ y ∈ J
have this₂ := (h.1).mul_mem_iff_mem_or_mem.1 this
case mpr.refine'_2.intro.intro.intro.intro
R : Type u_2
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_1
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
J : Ideal S
h : Ideal.IsPrime (Ideal.comap (algebraMap R S) J) ∧ Disjoint ↑M ↑(Ideal.comap (algebraMap R S) J)
x y : S
hxy : x * y ∈ J
a : R
s : { x // x ∈ M }
ha : mk' S a s = x
b : R
t : { x // x ∈ 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
case mpr.refine'_2.intro.intro.intro.intro
R : Type u_2
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_1
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
J : Ideal S
h : Ideal.IsPrime (Ideal.comap (algebraMap R S) J) ∧ Disjoint ↑M ↑(Ideal.comap (algebraMap R S) J)
x y : S
hxy : x * y ∈ J
a : R
s : { x // x ∈ M }
ha : mk' S a s = x
b : R
t : { x // x ∈ 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
rw [Ideal.mem_comap, Ideal.mem_comap] at this₂
no goals
case mpr.refine'_2.intro.intro.intro.intro
R : Type u_2
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_1
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
J : Ideal S
h : Ideal.IsPrime (Ideal.comap (algebraMap R S) J) ∧ Disjoint ↑M ↑(Ideal.comap (algebraMap R S) J)
x y : S
hxy : x * y ∈ J
a : R
s : { x // x ∈ M }
ha : mk' S a s = x
b : R
t : { x // x ∈ 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
rwa [← ha, ← hb, mk'_mem_iff, mk'_mem_iff]
no goals
R : Type u_2
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_1
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
J : Ideal S
h : Ideal.IsPrime (Ideal.comap (algebraMap R S) J) ∧ Disjoint ↑M ↑(Ideal.comap (algebraMap R S) J)
x y : S
hxy : x * y ∈ J
a : R
s : { x // x ∈ M }
ha : mk' S a s = x
b : R
t : { x // x ∈ M }
hb : mk' S b t = y
⊢ mk' S (a * b) (s * t) ∈ J
rwa [mk'_mul, ha, hb]