R : Type u_2
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_1
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
I : Ideal S
inst✝ : Ideal.IsPrime I
J : Ideal R
H : J ≤ Ideal.comap (algebraMap R S) I
hI : Ideal.IsMaximal (Ideal.comap (algebraMap R S) I)
s : S ⧸ I
⊢ ∃ a, ↑(Ideal.quotientMap I (algebraMap R S) H) a = s
R : Type u_2
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_1
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
I : Ideal S
inst✝ : Ideal.IsPrime I
J : Ideal R
H : J ≤ Ideal.comap (algebraMap R S) I
hI : Ideal.IsMaximal (Ideal.comap (algebraMap R S) I)
⊢ Function.Surjective ↑(Ideal.quotientMap I (algebraMap R S) H)
intro s
case intro
R : Type u_2
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_1
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
I : Ideal S
inst✝ : Ideal.IsPrime I
J : Ideal R
H : J ≤ Ideal.comap (algebraMap R S) I
hI : Ideal.IsMaximal (Ideal.comap (algebraMap R S) I)
s : S
⊢ ∃ a, ↑(Ideal.quotientMap I (algebraMap R S) H) a = ↑(Ideal.Quotient.mk I) s
R : Type u_2
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_1
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
I : Ideal S
inst✝ : Ideal.IsPrime I
J : Ideal R
H : J ≤ Ideal.comap (algebraMap R S) I
hI : Ideal.IsMaximal (Ideal.comap (algebraMap R S) I)
s : S ⧸ I
⊢ ∃ a, ↑(Ideal.quotientMap I (algebraMap R S) H) a = s
obtain ⟨s, rfl⟩ := Ideal.Quotient.mk_surjective s
case intro.intro.intro.mk
R : Type u_2
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_1
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
I : Ideal S
inst✝ : Ideal.IsPrime I
J : Ideal R
H : J ≤ Ideal.comap (algebraMap R S) I
hI : Ideal.IsMaximal (Ideal.comap (algebraMap R S) I)
r m : R
hm : m ∈ M
⊢ ∃ a, ↑(Ideal.quotientMap I (algebraMap R S) H) a = ↑(Ideal.Quotient.mk I) (mk' S r { val := m, property := hm })
case intro
R : Type u_2
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_1
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
I : Ideal S
inst✝ : Ideal.IsPrime I
J : Ideal R
H : J ≤ Ideal.comap (algebraMap R S) I
hI : Ideal.IsMaximal (Ideal.comap (algebraMap R S) I)
s : S
⊢ ∃ a, ↑(Ideal.quotientMap I (algebraMap R S) H) a = ↑(Ideal.Quotient.mk I) s
obtain ⟨r, ⟨m, hm⟩, rfl⟩ := mk'_surjective M s
case pos
R : Type u_2
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_1
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
I : Ideal S
inst✝ : Ideal.IsPrime I
J : Ideal R
H : J ≤ Ideal.comap (algebraMap R S) I
hI : Ideal.IsMaximal (Ideal.comap (algebraMap R S) I)
r m : R
hm : m ∈ M
hM : ↑(Ideal.Quotient.mk (Ideal.comap (algebraMap R S) I)) m = 0
⊢ ∃ a, ↑(Ideal.quotientMap I (algebraMap R S) H) a = ↑(Ideal.Quotient.mk I) (mk' S r { val := m, property := hm })

case neg
R : Type u_2
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_1
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
I : Ideal S
inst✝ : Ideal.IsPrime I
J : Ideal R
H : J ≤ Ideal.comap (algebraMap R S) I
hI : Ideal.IsMaximal (Ideal.comap (algebraMap R S) I)
r m : R
hm : m ∈ M
hM : ¬↑(Ideal.Quotient.mk (Ideal.comap (algebraMap R S) I)) m = 0
⊢ ∃ a, ↑(Ideal.quotientMap I (algebraMap R S) H) a = ↑(Ideal.Quotient.mk I) (mk' S r { val := m, property := hm })
case intro.intro.intro.mk
R : Type u_2
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_1
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
I : Ideal S
inst✝ : Ideal.IsPrime I
J : Ideal R
H : J ≤ Ideal.comap (algebraMap R S) I
hI : Ideal.IsMaximal (Ideal.comap (algebraMap R S) I)
r m : R
hm : m ∈ M
⊢ ∃ a, ↑(Ideal.quotientMap I (algebraMap R S) H) a = ↑(Ideal.Quotient.mk I) (mk' S r { val := m, property := hm })
by_cases hM : (Ideal.Quotient.mk (I.comap (algebraMap R S))) m = 0
case pos
R : Type u_2
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_1
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
I : Ideal S
inst✝ : Ideal.IsPrime I
J : Ideal R
H : J ≤ Ideal.comap (algebraMap R S) I
hI : Ideal.IsMaximal (Ideal.comap (algebraMap R S) I)
r m : R
hm : m ∈ M
hM : ↑(Ideal.Quotient.mk (Ideal.comap (algebraMap R S) I)) m = 0
this : I = ⊤
⊢ ∃ a, ↑(Ideal.quotientMap I (algebraMap R S) H) a = ↑(Ideal.Quotient.mk I) (mk' S r { val := m, property := hm })
case pos
R : Type u_2
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_1
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
I : Ideal S
inst✝ : Ideal.IsPrime I
J : Ideal R
H : J ≤ Ideal.comap (algebraMap R S) I
hI : Ideal.IsMaximal (Ideal.comap (algebraMap R S) I)
r m : R
hm : m ∈ M
hM : ↑(Ideal.Quotient.mk (Ideal.comap (algebraMap R S) I)) m = 0
⊢ ∃ a, ↑(Ideal.quotientMap I (algebraMap R S) H) a = ↑(Ideal.Quotient.mk I) (mk' S r { val := m, property := hm })
have : I = ⊤ := by
  rw [Ideal.eq_top_iff_one]
  rw [Ideal.Quotient.eq_zero_iff_mem, Ideal.mem_comap] at hM
  convert I.mul_mem_right (mk' S (1 : R) ⟨m, hm⟩) hM
  rw [← mk'_eq_mul_mk'_one, mk'_self]
no goals
case pos
R : Type u_2
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_1
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
I : Ideal S
inst✝ : Ideal.IsPrime I
J : Ideal R
H : J ≤ Ideal.comap (algebraMap R S) I
hI : Ideal.IsMaximal (Ideal.comap (algebraMap R S) I)
r m : R
hm : m ∈ M
hM : ↑(Ideal.Quotient.mk (Ideal.comap (algebraMap R S) I)) m = 0
this : I = ⊤
⊢ ∃ a, ↑(Ideal.quotientMap I (algebraMap R S) H) a = ↑(Ideal.Quotient.mk I) (mk' S r { val := m, property := hm })
exact ⟨0, eq_comm.1 (by simp [Ideal.Quotient.eq_zero_iff_mem, this])⟩
R : Type u_2
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_1
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
I : Ideal S
inst✝ : Ideal.IsPrime I
J : Ideal R
H : J ≤ Ideal.comap (algebraMap R S) I
hI : Ideal.IsMaximal (Ideal.comap (algebraMap R S) I)
r m : R
hm : m ∈ M
hM : ↑(Ideal.Quotient.mk (Ideal.comap (algebraMap R S) I)) m = 0
⊢ 1 ∈ I
R : Type u_2
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_1
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
I : Ideal S
inst✝ : Ideal.IsPrime I
J : Ideal R
H : J ≤ Ideal.comap (algebraMap R S) I
hI : Ideal.IsMaximal (Ideal.comap (algebraMap R S) I)
r m : R
hm : m ∈ M
hM : ↑(Ideal.Quotient.mk (Ideal.comap (algebraMap R S) I)) m = 0
⊢ I = ⊤
rw [Ideal.eq_top_iff_one]
R : Type u_2
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_1
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
I : Ideal S
inst✝ : Ideal.IsPrime I
J : Ideal R
H : J ≤ Ideal.comap (algebraMap R S) I
hI : Ideal.IsMaximal (Ideal.comap (algebraMap R S) I)
r m : R
hm : m ∈ M
hM : ↑(algebraMap R S) m ∈ I
⊢ 1 ∈ I
R : Type u_2
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_1
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
I : Ideal S
inst✝ : Ideal.IsPrime I
J : Ideal R
H : J ≤ Ideal.comap (algebraMap R S) I
hI : Ideal.IsMaximal (Ideal.comap (algebraMap R S) I)
r m : R
hm : m ∈ M
hM : ↑(Ideal.Quotient.mk (Ideal.comap (algebraMap R S) I)) m = 0
⊢ 1 ∈ I
rw [Ideal.Quotient.eq_zero_iff_mem, Ideal.mem_comap] at hM
case h.e'_4
R : Type u_2
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_1
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
I : Ideal S
inst✝ : Ideal.IsPrime I
J : Ideal R
H : J ≤ Ideal.comap (algebraMap R S) I
hI : Ideal.IsMaximal (Ideal.comap (algebraMap R S) I)
r m : R
hm : m ∈ M
hM : ↑(algebraMap R S) m ∈ I
⊢ 1 = ↑(algebraMap R S) m * mk' S 1 { val := m, property := hm }
R : Type u_2
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_1
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
I : Ideal S
inst✝ : Ideal.IsPrime I
J : Ideal R
H : J ≤ Ideal.comap (algebraMap R S) I
hI : Ideal.IsMaximal (Ideal.comap (algebraMap R S) I)
r m : R
hm : m ∈ M
hM : ↑(algebraMap R S) m ∈ I
⊢ 1 ∈ I
convert I.mul_mem_right (mk' S (1 : R) ⟨m, hm⟩) hM
no goals
case h.e'_4
R : Type u_2
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_1
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
I : Ideal S
inst✝ : Ideal.IsPrime I
J : Ideal R
H : J ≤ Ideal.comap (algebraMap R S) I
hI : Ideal.IsMaximal (Ideal.comap (algebraMap R S) I)
r m : R
hm : m ∈ M
hM : ↑(algebraMap R S) m ∈ I
⊢ 1 = ↑(algebraMap R S) m * mk' S 1 { val := m, property := hm }
rw [← mk'_eq_mul_mk'_one, mk'_self]
no goals
R : Type u_2
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_1
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
I : Ideal S
inst✝ : Ideal.IsPrime I
J : Ideal R
H : J ≤ Ideal.comap (algebraMap R S) I
hI : Ideal.IsMaximal (Ideal.comap (algebraMap R S) I)
r m : R
hm : m ∈ M
hM : ↑(Ideal.Quotient.mk (Ideal.comap (algebraMap R S) I)) m = 0
this : I = ⊤
⊢ ↑(Ideal.Quotient.mk I) (mk' S r { val := m, property := hm }) = ↑(Ideal.quotientMap I (algebraMap R S) H) 0
simp [Ideal.Quotient.eq_zero_iff_mem, this]
case neg
R : Type u_2
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_1
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
I : Ideal S
inst✝ : Ideal.IsPrime I
J : Ideal R
H : J ≤ Ideal.comap (algebraMap R S) I
hI : IsField (R ⧸ Ideal.comap (algebraMap R S) I)
r m : R
hm : m ∈ M
hM : ¬↑(Ideal.Quotient.mk (Ideal.comap (algebraMap R S) I)) m = 0
⊢ ∃ a, ↑(Ideal.quotientMap I (algebraMap R S) H) a = ↑(Ideal.Quotient.mk I) (mk' S r { val := m, property := hm })
case neg
R : Type u_2
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_1
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
I : Ideal S
inst✝ : Ideal.IsPrime I
J : Ideal R
H : J ≤ Ideal.comap (algebraMap R S) I
hI : Ideal.IsMaximal (Ideal.comap (algebraMap R S) I)
r m : R
hm : m ∈ M
hM : ¬↑(Ideal.Quotient.mk (Ideal.comap (algebraMap R S) I)) m = 0
⊢ ∃ a, ↑(Ideal.quotientMap I (algebraMap R S) H) a = ↑(Ideal.Quotient.mk I) (mk' S r { val := m, property := hm })
rw [Ideal.Quotient.maximal_ideal_iff_isField_quotient] at hI
case neg.intro
R : Type u_2
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_1
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
I : Ideal S
inst✝ : Ideal.IsPrime I
J : Ideal R
H : J ≤ Ideal.comap (algebraMap R S) I
hI : IsField (R ⧸ Ideal.comap (algebraMap R S) I)
r m : R
hm : m ∈ M
hM : ¬↑(Ideal.Quotient.mk (Ideal.comap (algebraMap R S) I)) m = 0
n : R ⧸ Ideal.comap (algebraMap R S) I
hn : ↑(Ideal.Quotient.mk (Ideal.comap (algebraMap R S) I)) m * n = 1
⊢ ∃ a, ↑(Ideal.quotientMap I (algebraMap R S) H) a = ↑(Ideal.Quotient.mk I) (mk' S r { val := m, property := hm })
case neg
R : Type u_2
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_1
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
I : Ideal S
inst✝ : Ideal.IsPrime I
J : Ideal R
H : J ≤ Ideal.comap (algebraMap R S) I
hI : IsField (R ⧸ Ideal.comap (algebraMap R S) I)
r m : R
hm : m ∈ M
hM : ¬↑(Ideal.Quotient.mk (Ideal.comap (algebraMap R S) I)) m = 0
⊢ ∃ a, ↑(Ideal.quotientMap I (algebraMap R S) H) a = ↑(Ideal.Quotient.mk I) (mk' S r { val := m, property := hm })
obtain ⟨n, hn⟩ := hI.3 hM
case neg.intro.intro
R : Type u_2
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_1
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
I : Ideal S
inst✝ : Ideal.IsPrime I
J : Ideal R
H : J ≤ Ideal.comap (algebraMap R S) I
hI : IsField (R ⧸ Ideal.comap (algebraMap R S) I)
r m : R
hm : m ∈ M
hM : ¬↑(Ideal.Quotient.mk (Ideal.comap (algebraMap R S) I)) m = 0
rn : R
hn :
  ↑(Ideal.Quotient.mk (Ideal.comap (algebraMap R S) I)) m * ↑(Ideal.Quotient.mk (Ideal.comap (algebraMap R S) I)) rn = 1
⊢ ∃ a, ↑(Ideal.quotientMap I (algebraMap R S) H) a = ↑(Ideal.Quotient.mk I) (mk' S r { val := m, property := hm })
case neg.intro
R : Type u_2
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_1
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
I : Ideal S
inst✝ : Ideal.IsPrime I
J : Ideal R
H : J ≤ Ideal.comap (algebraMap R S) I
hI : IsField (R ⧸ Ideal.comap (algebraMap R S) I)
r m : R
hm : m ∈ M
hM : ¬↑(Ideal.Quotient.mk (Ideal.comap (algebraMap R S) I)) m = 0
n : R ⧸ Ideal.comap (algebraMap R S) I
hn : ↑(Ideal.Quotient.mk (Ideal.comap (algebraMap R S) I)) m * n = 1
⊢ ∃ a, ↑(Ideal.quotientMap I (algebraMap R S) H) a = ↑(Ideal.Quotient.mk I) (mk' S r { val := m, property := hm })
obtain ⟨rn, rfl⟩ := Ideal.Quotient.mk_surjective n
case neg.intro.intro
R : Type u_2
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_1
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
I : Ideal S
inst✝ : Ideal.IsPrime I
J : Ideal R
H : J ≤ Ideal.comap (algebraMap R S) I
hI : IsField (R ⧸ Ideal.comap (algebraMap R S) I)
r m : R
hm : m ∈ M
hM : ¬↑(Ideal.Quotient.mk (Ideal.comap (algebraMap R S) I)) m = 0
rn : R
hn :
  ↑(Ideal.Quotient.mk (Ideal.comap (algebraMap R S) I)) m * ↑(Ideal.Quotient.mk (Ideal.comap (algebraMap R S) I)) rn = 1
⊢ ↑(Ideal.quotientMap I (algebraMap R S) H) (↑(Ideal.Quotient.mk J) (r * rn)) =
    ↑(Ideal.Quotient.mk I) (mk' S r { val := m, property := hm })
case neg.intro.intro
R : Type u_2
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_1
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
I : Ideal S
inst✝ : Ideal.IsPrime I
J : Ideal R
H : J ≤ Ideal.comap (algebraMap R S) I
hI : IsField (R ⧸ Ideal.comap (algebraMap R S) I)
r m : R
hm : m ∈ M
hM : ¬↑(Ideal.Quotient.mk (Ideal.comap (algebraMap R S) I)) m = 0
rn : R
hn :
  ↑(Ideal.Quotient.mk (Ideal.comap (algebraMap R S) I)) m * ↑(Ideal.Quotient.mk (Ideal.comap (algebraMap R S) I)) rn = 1
⊢ ∃ a, ↑(Ideal.quotientMap I (algebraMap R S) H) a = ↑(Ideal.Quotient.mk I) (mk' S r { val := m, property := hm })
refine' ⟨(Ideal.Quotient.mk J) (r * rn), _⟩
case neg.intro.intro
R : Type u_2
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_1
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
I : Ideal S
inst✝ : Ideal.IsPrime I
J : Ideal R
H : J ≤ Ideal.comap (algebraMap R S) I
hI : IsField (R ⧸ Ideal.comap (algebraMap R S) I)
r m : R
hm : m ∈ M
hM : ¬↑(Ideal.Quotient.mk (Ideal.comap (algebraMap R S) I)) m = 0
rn : R
hn :
  ↑(Ideal.quotientMap I (algebraMap R S) (_ : Ideal.comap (algebraMap R S) I ≤ Ideal.comap (algebraMap R S) I))
      (↑(Ideal.Quotient.mk (Ideal.comap (algebraMap R S) I)) m *
        ↑(Ideal.Quotient.mk (Ideal.comap (algebraMap R S) I)) rn) =
    ↑(Ideal.quotientMap I (algebraMap R S) (_ : Ideal.comap (algebraMap R S) I ≤ Ideal.comap (algebraMap R S) I)) 1
⊢ ↑(Ideal.quotientMap I (algebraMap R S) H) (↑(Ideal.Quotient.mk J) (r * rn)) =
    ↑(Ideal.Quotient.mk I) (mk' S r { val := m, property := hm })
case neg.intro.intro
R : Type u_2
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_1
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
I : Ideal S
inst✝ : Ideal.IsPrime I
J : Ideal R
H : J ≤ Ideal.comap (algebraMap R S) I
hI : IsField (R ⧸ Ideal.comap (algebraMap R S) I)
r m : R
hm : m ∈ M
hM : ¬↑(Ideal.Quotient.mk (Ideal.comap (algebraMap R S) I)) m = 0
rn : R
hn :
  ↑(Ideal.Quotient.mk (Ideal.comap (algebraMap R S) I)) m * ↑(Ideal.Quotient.mk (Ideal.comap (algebraMap R S) I)) rn = 1
⊢ ↑(Ideal.quotientMap I (algebraMap R S) H) (↑(Ideal.Quotient.mk J) (r * rn)) =
    ↑(Ideal.Quotient.mk I) (mk' S r { val := m, property := hm })
replace hn := congr_arg (Ideal.quotientMap I (algebraMap R S) le_rfl) hn
case neg.intro.intro
R : Type u_2
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_1
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
I : Ideal S
inst✝ : Ideal.IsPrime I
J : Ideal R
H : J ≤ Ideal.comap (algebraMap R S) I
hI : IsField (R ⧸ Ideal.comap (algebraMap R S) I)
r m : R
hm : m ∈ M
hM : ¬↑(Ideal.Quotient.mk (Ideal.comap (algebraMap R S) I)) m = 0
rn : R
hn :
  ↑(Ideal.quotientMap I (algebraMap R S) (_ : Ideal.comap (algebraMap R S) I ≤ Ideal.comap (algebraMap R S) I))
        (↑(Ideal.Quotient.mk (Ideal.comap (algebraMap R S) I)) m) *
      ↑(Ideal.quotientMap I (algebraMap R S) (_ : Ideal.comap (algebraMap R S) I ≤ Ideal.comap (algebraMap R S) I))
        (↑(Ideal.Quotient.mk (Ideal.comap (algebraMap R S) I)) rn) =
    1
⊢ ↑(Ideal.quotientMap I (algebraMap R S) H) (↑(Ideal.Quotient.mk J) (r * rn)) =
    ↑(Ideal.Quotient.mk I) (mk' S r { val := m, property := hm })
case neg.intro.intro
R : Type u_2
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_1
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
I : Ideal S
inst✝ : Ideal.IsPrime I
J : Ideal R
H : J ≤ Ideal.comap (algebraMap R S) I
hI : IsField (R ⧸ Ideal.comap (algebraMap R S) I)
r m : R
hm : m ∈ M
hM : ¬↑(Ideal.Quotient.mk (Ideal.comap (algebraMap R S) I)) m = 0
rn : R
hn :
  ↑(Ideal.quotientMap I (algebraMap R S) (_ : Ideal.comap (algebraMap R S) I ≤ Ideal.comap (algebraMap R S) I))
      (↑(Ideal.Quotient.mk (Ideal.comap (algebraMap R S) I)) m *
        ↑(Ideal.Quotient.mk (Ideal.comap (algebraMap R S) I)) rn) =
    ↑(Ideal.quotientMap I (algebraMap R S) (_ : Ideal.comap (algebraMap R S) I ≤ Ideal.comap (algebraMap R S) I)) 1
⊢ ↑(Ideal.quotientMap I (algebraMap R S) H) (↑(Ideal.Quotient.mk J) (r * rn)) =
    ↑(Ideal.Quotient.mk I) (mk' S r { val := m, property := hm })
rw [RingHom.map_one, RingHom.map_mul] at hn
case neg.intro.intro
R : Type u_2
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_1
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
I : Ideal S
inst✝ : Ideal.IsPrime I
J : Ideal R
H : J ≤ Ideal.comap (algebraMap R S) I
hI : IsField (R ⧸ Ideal.comap (algebraMap R S) I)
r m : R
hm : m ∈ M
hM : ¬↑(Ideal.Quotient.mk (Ideal.comap (algebraMap R S) I)) m = 0
rn : R
hn :
  ↑(Ideal.quotientMap I (algebraMap R S) (_ : Ideal.comap (algebraMap R S) I ≤ Ideal.comap (algebraMap R S) I))
        (↑(Ideal.Quotient.mk (Ideal.comap (algebraMap R S) I)) m) *
      ↑(Ideal.quotientMap I (algebraMap R S) (_ : Ideal.comap (algebraMap R S) I ≤ Ideal.comap (algebraMap R S) I))
        (↑(Ideal.Quotient.mk (Ideal.comap (algebraMap R S) I)) rn) =
    1
⊢ ↑(Ideal.Quotient.mk I) (↑(algebraMap R S) (r * rn)) =
    ↑(Ideal.Quotient.mk I) (↑(algebraMap R S) r * mk' S 1 { val := m, property := hm })
case neg.intro.intro
R : Type u_2
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_1
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
I : Ideal S
inst✝ : Ideal.IsPrime I
J : Ideal R
H : J ≤ Ideal.comap (algebraMap R S) I
hI : IsField (R ⧸ Ideal.comap (algebraMap R S) I)
r m : R
hm : m ∈ M
hM : ¬↑(Ideal.Quotient.mk (Ideal.comap (algebraMap R S) I)) m = 0
rn : R
hn :
  ↑(Ideal.quotientMap I (algebraMap R S) (_ : Ideal.comap (algebraMap R S) I ≤ Ideal.comap (algebraMap R S) I))
        (↑(Ideal.Quotient.mk (Ideal.comap (algebraMap R S) I)) m) *
      ↑(Ideal.quotientMap I (algebraMap R S) (_ : Ideal.comap (algebraMap R S) I ≤ Ideal.comap (algebraMap R S) I))
        (↑(Ideal.Quotient.mk (Ideal.comap (algebraMap R S) I)) rn) =
    1
⊢ ↑(Ideal.quotientMap I (algebraMap R S) H) (↑(Ideal.Quotient.mk J) (r * rn)) =
    ↑(Ideal.Quotient.mk I) (mk' S r { val := m, property := hm })
rw [Ideal.quotientMap_mk, ← sub_eq_zero, ← RingHom.map_sub, Ideal.Quotient.eq_zero_iff_mem, ←
  Ideal.Quotient.eq_zero_iff_mem, RingHom.map_sub, sub_eq_zero, mk'_eq_mul_mk'_one]
case neg.intro.intro
R : Type u_2
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_1
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
I : Ideal S
inst✝ : Ideal.IsPrime I
J : Ideal R
H : J ≤ Ideal.comap (algebraMap R S) I
hI : IsField (R ⧸ Ideal.comap (algebraMap R S) I)
r m : R
hm : m ∈ M
hM : ¬↑(Ideal.Quotient.mk (Ideal.comap (algebraMap R S) I)) m = 0
rn : R
hn :
  ↑(Ideal.quotientMap I (algebraMap R S) (_ : Ideal.comap (algebraMap R S) I ≤ Ideal.comap (algebraMap R S) I))
        (↑(Ideal.Quotient.mk (Ideal.comap (algebraMap R S) I)) m) *
      ↑(Ideal.quotientMap I (algebraMap R S) (_ : Ideal.comap (algebraMap R S) I ≤ Ideal.comap (algebraMap R S) I))
        (↑(Ideal.Quotient.mk (Ideal.comap (algebraMap R S) I)) rn) =
    1
⊢ ↑(Ideal.Quotient.mk I) (↑(algebraMap R S) rn) = ↑(Ideal.Quotient.mk I) (mk' S 1 { val := m, property := hm }) ∨
    ↑(Ideal.Quotient.mk I) (↑(algebraMap R S) r) = 0
case neg.intro.intro
R : Type u_2
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_1
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
I : Ideal S
inst✝ : Ideal.IsPrime I
J : Ideal R
H : J ≤ Ideal.comap (algebraMap R S) I
hI : IsField (R ⧸ Ideal.comap (algebraMap R S) I)
r m : R
hm : m ∈ M
hM : ¬↑(Ideal.Quotient.mk (Ideal.comap (algebraMap R S) I)) m = 0
rn : R
hn :
  ↑(Ideal.quotientMap I (algebraMap R S) (_ : Ideal.comap (algebraMap R S) I ≤ Ideal.comap (algebraMap R S) I))
        (↑(Ideal.Quotient.mk (Ideal.comap (algebraMap R S) I)) m) *
      ↑(Ideal.quotientMap I (algebraMap R S) (_ : Ideal.comap (algebraMap R S) I ≤ Ideal.comap (algebraMap R S) I))
        (↑(Ideal.Quotient.mk (Ideal.comap (algebraMap R S) I)) rn) =
    1
⊢ ↑(Ideal.Quotient.mk I) (↑(algebraMap R S) (r * rn)) =
    ↑(Ideal.Quotient.mk I) (↑(algebraMap R S) r * mk' S 1 { val := m, property := hm })
simp only [mul_eq_mul_left_iff, RingHom.map_mul]
case neg.intro.intro
R : Type u_2
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_1
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
I : Ideal S
inst✝ : Ideal.IsPrime I
J : Ideal R
H : J ≤ Ideal.comap (algebraMap R S) I
hI : IsField (R ⧸ Ideal.comap (algebraMap R S) I)
r m : R
hm : m ∈ M
hM : ¬↑(Ideal.Quotient.mk (Ideal.comap (algebraMap R S) I)) m = 0
rn : R
hn :
  ↑(Ideal.quotientMap I (algebraMap R S) (_ : Ideal.comap (algebraMap R S) I ≤ Ideal.comap (algebraMap R S) I))
        (↑(Ideal.Quotient.mk (Ideal.comap (algebraMap R S) I)) m) *
      ↑(Ideal.quotientMap I (algebraMap R S) (_ : Ideal.comap (algebraMap R S) I ≤ Ideal.comap (algebraMap R S) I))
        (↑(Ideal.Quotient.mk (Ideal.comap (algebraMap R S) I)) rn) =
    1
⊢ 1 = ↑(Ideal.Quotient.mk I) (↑(algebraMap R S) m) * ↑(Ideal.Quotient.mk I) (mk' S 1 { val := m, property := hm })
case neg.intro.intro
R : Type u_2
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_1
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
I : Ideal S
inst✝ : Ideal.IsPrime I
J : Ideal R
H : J ≤ Ideal.comap (algebraMap R S) I
hI : IsField (R ⧸ Ideal.comap (algebraMap R S) I)
r m : R
hm : m ∈ M
hM : ¬↑(Ideal.Quotient.mk (Ideal.comap (algebraMap R S) I)) m = 0
rn : R
hn :
  ↑(Ideal.quotientMap I (algebraMap R S) (_ : Ideal.comap (algebraMap R S) I ≤ Ideal.comap (algebraMap R S) I))
        (↑(Ideal.Quotient.mk (Ideal.comap (algebraMap R S) I)) m) *
      ↑(Ideal.quotientMap I (algebraMap R S) (_ : Ideal.comap (algebraMap R S) I ≤ Ideal.comap (algebraMap R S) I))
        (↑(Ideal.Quotient.mk (Ideal.comap (algebraMap R S) I)) rn) =
    1
⊢ ↑(Ideal.Quotient.mk I) (↑(algebraMap R S) rn) = ↑(Ideal.Quotient.mk I) (mk' S 1 { val := m, property := hm }) ∨
    ↑(Ideal.Quotient.mk I) (↑(algebraMap R S) r) = 0
refine
  Or.inl
    (mul_left_cancel₀ (M₀ := S ⧸ I)
      (fun hn =>
        hM
          (Ideal.Quotient.eq_zero_iff_mem.2
            (Ideal.mem_comap.2 (Ideal.Quotient.eq_zero_iff_mem.1 hn))))
      (_root_.trans hn ?_))
case neg.intro.intro
R : Type u_2
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_1
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
I : Ideal S
inst✝ : Ideal.IsPrime I
J : Ideal R
H : J ≤ Ideal.comap (algebraMap R S) I
hI : IsField (R ⧸ Ideal.comap (algebraMap R S) I)
r m : R
hm : m ∈ M
hM : ¬↑(Ideal.Quotient.mk (Ideal.comap (algebraMap R S) I)) m = 0
rn : R
hn :
  ↑(Ideal.quotientMap I (algebraMap R S) (_ : Ideal.comap (algebraMap R S) I ≤ Ideal.comap (algebraMap R S) I))
        (↑(Ideal.Quotient.mk (Ideal.comap (algebraMap R S) I)) m) *
      ↑(Ideal.quotientMap I (algebraMap R S) (_ : Ideal.comap (algebraMap R S) I ≤ Ideal.comap (algebraMap R S) I))
        (↑(Ideal.Quotient.mk (Ideal.comap (algebraMap R S) I)) rn) =
    1
⊢ 1 = ↑(Ideal.Quotient.mk I) (↑(algebraMap R S) m * mk' S 1 { val := m, property := hm })
case neg.intro.intro
R : Type u_2
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_1
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
I : Ideal S
inst✝ : Ideal.IsPrime I
J : Ideal R
H : J ≤ Ideal.comap (algebraMap R S) I
hI : IsField (R ⧸ Ideal.comap (algebraMap R S) I)
r m : R
hm : m ∈ M
hM : ¬↑(Ideal.Quotient.mk (Ideal.comap (algebraMap R S) I)) m = 0
rn : R
hn :
  ↑(Ideal.quotientMap I (algebraMap R S) (_ : Ideal.comap (algebraMap R S) I ≤ Ideal.comap (algebraMap R S) I))
        (↑(Ideal.Quotient.mk (Ideal.comap (algebraMap R S) I)) m) *
      ↑(Ideal.quotientMap I (algebraMap R S) (_ : Ideal.comap (algebraMap R S) I ≤ Ideal.comap (algebraMap R S) I))
        (↑(Ideal.Quotient.mk (Ideal.comap (algebraMap R S) I)) rn) =
    1
⊢ 1 = ↑(Ideal.Quotient.mk I) (↑(algebraMap R S) m) * ↑(Ideal.Quotient.mk I) (mk' S 1 { val := m, property := hm })
refine Eq.trans ?_ (RingHom.map_mul (Ideal.Quotient.mk I) (algebraMap R S m) (mk' S 1 ⟨m, hm⟩))
no goals
case neg.intro.intro
R : Type u_2
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_1
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
I : Ideal S
inst✝ : Ideal.IsPrime I
J : Ideal R
H : J ≤ Ideal.comap (algebraMap R S) I
hI : IsField (R ⧸ Ideal.comap (algebraMap R S) I)
r m : R
hm : m ∈ M
hM : ¬↑(Ideal.Quotient.mk (Ideal.comap (algebraMap R S) I)) m = 0
rn : R
hn :
  ↑(Ideal.quotientMap I (algebraMap R S) (_ : Ideal.comap (algebraMap R S) I ≤ Ideal.comap (algebraMap R S) I))
        (↑(Ideal.Quotient.mk (Ideal.comap (algebraMap R S) I)) m) *
      ↑(Ideal.quotientMap I (algebraMap R S) (_ : Ideal.comap (algebraMap R S) I ≤ Ideal.comap (algebraMap R S) I))
        (↑(Ideal.Quotient.mk (Ideal.comap (algebraMap R S) I)) rn) =
    1
⊢ 1 = ↑(Ideal.Quotient.mk I) (↑(algebraMap R S) m * mk' S 1 { val := m, property := hm })
rw [← mk'_eq_mul_mk'_one, mk'_self, RingHom.map_one]