-- Mathlib/RingTheory/Localization/Ideal.lean
theorem surjective_quotientMap_of_maximal_of_localization {I : Ideal S} [I.IsPrime] {J : Ideal R}
    {H : J ≤ I.comap (algebraMap R S)} (hI : (I.comap (algebraMap R S)).IsMaximal) :
    Function.Surjective (Ideal.quotientMap I (algebraMap R S) H)

Proof state:
case pos
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
I : Ideal S
inst✝ : I.IsPrime
J : Ideal R
H : J ≤ Ideal.comap (algebraMap R S) I
hI : (Ideal.comap (algebraMap R S) I).IsMaximal
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 ⟨m, hm⟩)

Tactic:
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]

Result:
case pos
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
I : Ideal S
inst✝ : I.IsPrime
J : Ideal R
H : J ≤ Ideal.comap (algebraMap R S) I
hI : (Ideal.comap (algebraMap R S) I).IsMaximal
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 ⟨m, hm⟩)

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
I : Ideal S
inst✝ : I.IsPrime
J : Ideal R
H : J ≤ Ideal.comap (algebraMap R S) I
hI : (Ideal.comap (algebraMap R S) I).IsMaximal
r m : R
hm : m ∈ M
hM : (algebraMap R S) m ∈ I
⊢ 1 ∈ I

Tactic:
convert I.mul_mem_right (mk' S (1 : R) ⟨m, hm⟩) hM

Result:
case h.e'_5
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
I : Ideal S
inst✝ : I.IsPrime
J : Ideal R
H : J ≤ Ideal.comap (algebraMap R S) I
hI : (Ideal.comap (algebraMap R S) I).IsMaximal
r m : R
hm : m ∈ M
hM : (algebraMap R S) m ∈ I
⊢ 1 = (algebraMap R S) m * mk' S 1 ⟨m, hm⟩

Proof state:
case neg.intro
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
I : Ideal S
inst✝ : I.IsPrime
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 ⟨m, hm⟩)

Tactic:
obtain ⟨rn, rfl⟩ := Ideal.Quotient.mk_surjective n

Result:
case neg.intro.intro
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
I : Ideal S
inst✝ : I.IsPrime
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 ⟨m, hm⟩)

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
I : Ideal S
inst✝ : I.IsPrime
J : Ideal R
H : J ≤ Ideal.comap (algebraMap R S) I
hI : (Ideal.comap (algebraMap R S) I).IsMaximal
s : S ⧸ I
⊢ ∃ a, (Ideal.quotientMap I (algebraMap R S) H) a = s

Tactic:
obtain ⟨s, rfl⟩ := Ideal.Quotient.mk_surjective s

Result:
case intro
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
I : Ideal S
inst✝ : I.IsPrime
J : Ideal R
H : J ≤ Ideal.comap (algebraMap R S) I
hI : (Ideal.comap (algebraMap R S) I).IsMaximal
s : S
⊢ ∃ a, (Ideal.quotientMap I (algebraMap R S) H) a = (Ideal.Quotient.mk I) s

Proof state:
case neg
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
I : Ideal S
inst✝ : I.IsPrime
J : Ideal R
H : J ≤ Ideal.comap (algebraMap R S) I
hI : (Ideal.comap (algebraMap R S) I).IsMaximal
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 ⟨m, hm⟩)

Tactic:
rw [Ideal.Quotient.maximal_ideal_iff_isField_quotient] at hI

Result:
case neg
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
I : Ideal S
inst✝ : I.IsPrime
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 ⟨m, hm⟩)

Proof state:
case neg.intro.intro
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
I : Ideal S
inst✝ : I.IsPrime
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.Quotient.mk (Ideal.comap (algebraMap R S) I)) m) *
      (Ideal.quotientMap I (algebraMap R S) ⋯) ((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 ⟨m, hm⟩) ∨
    (Ideal.Quotient.mk I) ((algebraMap R S) r) = 0

Tactic:
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 ?_))

Result:
case neg.intro.intro
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
I : Ideal S
inst✝ : I.IsPrime
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.Quotient.mk (Ideal.comap (algebraMap R S) I)) m) *
      (Ideal.quotientMap I (algebraMap R S) ⋯) ((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 ⟨m, hm⟩)

Proof state:
case intro
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
I : Ideal S
inst✝ : I.IsPrime
J : Ideal R
H : J ≤ Ideal.comap (algebraMap R S) I
hI : (Ideal.comap (algebraMap R S) I).IsMaximal
s : S
⊢ ∃ a, (Ideal.quotientMap I (algebraMap R S) H) a = (Ideal.Quotient.mk I) s

Tactic:
obtain ⟨r, ⟨m, hm⟩, rfl⟩ := mk'_surjective M s

Result:
case intro.intro.intro.mk
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
I : Ideal S
inst✝ : I.IsPrime
J : Ideal R
H : J ≤ Ideal.comap (algebraMap R S) I
hI : (Ideal.comap (algebraMap R S) I).IsMaximal
r m : R
hm : m ∈ M
⊢ ∃ a, (Ideal.quotientMap I (algebraMap R S) H) a = (Ideal.Quotient.mk I) (mk' S r ⟨m, hm⟩)