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

Tactic:
rw [← map_mul, ← mk'_eq_mul_mk'_one, mk'_self, RingHom.map_one]

Result:
no goals

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
⊢ Function.Surjective ⇑(Ideal.quotientMap I (algebraMap R S) H)

Tactic:
intro s

Result:
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

Proof state:
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⟩)

Tactic:
by_cases hM : (Ideal.Quotient.mk (I.comap (algebraMap R S))) m = 0

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
⊢ ∃ a, (Ideal.quotientMap I (algebraMap R S) H) a = (Ideal.Quotient.mk I) (mk' S r ⟨m, hm⟩)

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

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.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 ⟨m, hm⟩)

Tactic:
replace hn := congr_arg (Ideal.quotientMap I (algebraMap R S) le_rfl) 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.Quotient.mk (Ideal.comap (algebraMap R S) I)) rn) =
    (Ideal.quotientMap I (algebraMap R S) ⋯) 1
⊢ (Ideal.quotientMap I (algebraMap R S) H) ((Ideal.Quotient.mk J) (r * rn)) = (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 : (Ideal.Quotient.mk (Ideal.comap (algebraMap R S) I)) m = 0
⊢ I = ⊤

Tactic:
rw [Ideal.eq_top_iff_one]

Result:
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
⊢ 1 ∈ I

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.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⟩)

Tactic:
refine ⟨(Ideal.Quotient.mk J) (r * rn), ?_⟩

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
⊢ (Ideal.quotientMap I (algebraMap R S) H) ((Ideal.Quotient.mk J) (r * rn)) = (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 : (Ideal.Quotient.mk (Ideal.comap (algebraMap R S) I)) m = 0
⊢ 1 ∈ I

Tactic:
rw [Ideal.Quotient.eq_zero_iff_mem, Ideal.mem_comap] at hM

Result:
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