-- Mathlib/RingTheory/Ideal/MinimalPrime/Localization.lean
theorem Ideal.exists_comap_eq_of_mem_minimalPrimes {I : Ideal S} (f : R →+* S) (p)
    (H : p ∈ (I.comap f).minimalPrimes) : ∃ p' : Ideal S, p'.IsPrime ∧ I ≤ p' ∧ p'.comap f = p

Proof state:
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal S
f : R →+* S
p : Ideal R
H : p ∈ (comap f I).minimalPrimes
this✝¹ : p.IsPrime
f' : R →+* S ⧸ I := (Quotient.mk I).comp f
e : RingHom.ker f' = comap f I
this✝ : RingHom.ker (Quotient.mk (RingHom.ker f')) ≤ p
this : map (Quotient.mk (RingHom.ker f')) p ∈ minimalPrimes (R ⧸ RingHom.ker f')
p' : Ideal (S ⧸ I)
hp₁ : p'.IsPrime
hp₂ : comap f'.kerLift p' = map (Quotient.mk (RingHom.ker f')) p
⊢ ∃ p', p'.IsPrime ∧ I ≤ p' ∧ comap f p' = p

Tactic:
refine ⟨p'.comap <| Ideal.Quotient.mk I, Ideal.IsPrime.comap _, ?_, ?_⟩

Result:
case refine_1
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal S
f : R →+* S
p : Ideal R
H : p ∈ (comap f I).minimalPrimes
this✝¹ : p.IsPrime
f' : R →+* S ⧸ I := (Quotient.mk I).comp f
e : RingHom.ker f' = comap f I
this✝ : RingHom.ker (Quotient.mk (RingHom.ker f')) ≤ p
this : map (Quotient.mk (RingHom.ker f')) p ∈ minimalPrimes (R ⧸ RingHom.ker f')
p' : Ideal (S ⧸ I)
hp₁ : p'.IsPrime
hp₂ : comap f'.kerLift p' = map (Quotient.mk (RingHom.ker f')) p
⊢ I ≤ comap (Quotient.mk I) p'

case refine_2
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal S
f : R →+* S
p : Ideal R
H : p ∈ (comap f I).minimalPrimes
this✝¹ : p.IsPrime
f' : R →+* S ⧸ I := (Quotient.mk I).comp f
e : RingHom.ker f' = comap f I
this✝ : RingHom.ker (Quotient.mk (RingHom.ker f')) ≤ p
this : map (Quotient.mk (RingHom.ker f')) p ∈ minimalPrimes (R ⧸ RingHom.ker f')
p' : Ideal (S ⧸ I)
hp₁ : p'.IsPrime
hp₂ : comap f'.kerLift p' = map (Quotient.mk (RingHom.ker f')) p
⊢ comap f (comap (Quotient.mk I) p') = p

Proof state:
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal S
f : R →+* S
p : Ideal R
H : p ∈ (comap f I).minimalPrimes
this✝¹ : p.IsPrime
f' : R →+* S ⧸ I := (Quotient.mk I).comp f
e : RingHom.ker f' = comap f I
this✝ : RingHom.ker (Quotient.mk (RingHom.ker f')) ≤ p
this : ?m.43443
⊢ ∃ p', p'.IsPrime ∧ I ≤ p' ∧ comap f p' = p

Tactic:
have ⟨p', hp₁, hp₂⟩ := Ideal.exists_comap_eq_of_mem_minimalPrimes_of_injective
  (RingHom.kerLift_injective f') (p.map <| Ideal.Quotient.mk <| RingHom.ker f') this

Result:
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal S
f : R →+* S
p : Ideal R
H : p ∈ (comap f I).minimalPrimes
this✝¹ : p.IsPrime
f' : R →+* S ⧸ I := (Quotient.mk I).comp f
e : RingHom.ker f' = comap f I
this✝ : RingHom.ker (Quotient.mk (RingHom.ker f')) ≤ p
this : map (Quotient.mk (RingHom.ker f')) p ∈ minimalPrimes (R ⧸ RingHom.ker f')
p' : Ideal (S ⧸ I)
hp₁ : p'.IsPrime
hp₂ : comap f'.kerLift p' = map (Quotient.mk (RingHom.ker f')) p
⊢ ∃ p', p'.IsPrime ∧ I ≤ p' ∧ comap f p' = p

Proof state:
case refine_2
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal S
f : R →+* S
p : Ideal R
H : p ∈ (comap f I).minimalPrimes
this✝ : p.IsPrime
f' : R →+* S ⧸ I := (Quotient.mk I).comp f
e : RingHom.ker f' = comap f I
this : RingHom.ker (Quotient.mk (RingHom.ker f')) ≤ p
⊢ ∀ ⦃y : Ideal (R ⧸ RingHom.ker f')⦄,
    (fun q => q.IsPrime ∧ ⊥ ≤ q) y → y ≤ map (Quotient.mk (RingHom.ker f')) p → map (Quotient.mk (RingHom.ker f')) p ≤ y

Tactic:
rintro q ⟨hq, -⟩ hq'

Result:
case refine_2.intro
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal S
f : R →+* S
p : Ideal R
H : p ∈ (comap f I).minimalPrimes
this✝ : p.IsPrime
f' : R →+* S ⧸ I := (Quotient.mk I).comp f
e : RingHom.ker f' = comap f I
this : RingHom.ker (Quotient.mk (RingHom.ker f')) ≤ p
q : Ideal (R ⧸ RingHom.ker f')
hq : q.IsPrime
hq' : q ≤ map (Quotient.mk (RingHom.ker f')) p
⊢ map (Quotient.mk (RingHom.ker f')) p ≤ q

Proof state:
case refine_2.intro
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal S
f : R →+* S
p : Ideal R
H : p ∈ (comap f I).minimalPrimes
this✝ : p.IsPrime
f' : R →+* S ⧸ I := (Quotient.mk I).comp f
e : RingHom.ker f' = comap f I
this : RingHom.ker (Quotient.mk (RingHom.ker f')) ≤ p
q : Ideal (R ⧸ RingHom.ker f')
hq : q.IsPrime
hq' : q ≤ map (Quotient.mk (RingHom.ker f')) p
⊢ map (Quotient.mk (RingHom.ker f')) p ≤
    map (Quotient.mk (RingHom.ker ((Quotient.mk I).comp f)))
      (comap (Quotient.mk (RingHom.ker ((Quotient.mk I).comp f))) q)

Tactic:
apply Ideal.map_mono

Result:
case refine_2.intro.h
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal S
f : R →+* S
p : Ideal R
H : p ∈ (comap f I).minimalPrimes
this✝ : p.IsPrime
f' : R →+* S ⧸ I := (Quotient.mk I).comp f
e : RingHom.ker f' = comap f I
this : RingHom.ker (Quotient.mk (RingHom.ker f')) ≤ p
q : Ideal (R ⧸ RingHom.ker f')
hq : q.IsPrime
hq' : q ≤ map (Quotient.mk (RingHom.ker f')) p
⊢ p ≤ comap (Quotient.mk (RingHom.ker ((Quotient.mk I).comp f))) q

Proof state:
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal S
f : R →+* S
p : Ideal R
H : p ∈ (comap f I).minimalPrimes
this✝ : p.IsPrime
f' : R →+* S ⧸ I := (Quotient.mk I).comp f
e : RingHom.ker f' = comap f I
this : RingHom.ker (Quotient.mk (RingHom.ker f')) ≤ p
⊢ Function.Surjective ⇑(Quotient.mk (RingHom.ker f'))

Tactic:
exact Ideal.Quotient.mk_surjective

Result:
no goals

Proof state:
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal S
f : R →+* S
p : Ideal R
H : p ∈ (comap f I).minimalPrimes
this : p.IsPrime
f' : R →+* S ⧸ I := (Quotient.mk I).comp f
e : RingHom.ker f' = comap f I
⊢ comap f I ≤ p

Tactic:
exact H.1.2

Result:
no goals

Proof state:
case refine_2.intro.h.a
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal S
f : R →+* S
p : Ideal R
H : p ∈ (comap f I).minimalPrimes
this✝ : p.IsPrime
f' : R →+* S ⧸ I := (Quotient.mk I).comp f
e : RingHom.ker f' = comap f I
this : RingHom.ker (Quotient.mk (RingHom.ker f')) ≤ p
q : Ideal (R ⧸ RingHom.ker f')
hq : q.IsPrime
hq' : q ≤ map (Quotient.mk (RingHom.ker f')) p
⊢ comap (Quotient.mk (RingHom.ker ((Quotient.mk I).comp f))) q ≤ p

Tactic:
refine (Ideal.comap_mono hq').trans ?_

Result:
case refine_2.intro.h.a
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal S
f : R →+* S
p : Ideal R
H : p ∈ (comap f I).minimalPrimes
this✝ : p.IsPrime
f' : R →+* S ⧸ I := (Quotient.mk I).comp f
e : RingHom.ker f' = comap f I
this : RingHom.ker (Quotient.mk (RingHom.ker f')) ≤ p
q : Ideal (R ⧸ RingHom.ker f')
hq : q.IsPrime
hq' : q ≤ map (Quotient.mk (RingHom.ker f')) p
⊢ comap (Quotient.mk (RingHom.ker ((Quotient.mk I).comp f))) (map (Quotient.mk (RingHom.ker f')) p) ≤ p

Proof state:
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal S
f : R →+* S
p : Ideal R
H : p ∈ (comap f I).minimalPrimes
this : p.IsPrime
f' : R →+* S ⧸ I := (Quotient.mk I).comp f
⊢ ∃ p', p'.IsPrime ∧ I ≤ p' ∧ comap f p' = p

Tactic:
have e : RingHom.ker f' = I.comap f := by
  ext1
  exact Submodule.Quotient.mk_eq_zero _

Result:
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal S
f : R →+* S
p : Ideal R
H : p ∈ (comap f I).minimalPrimes
this : p.IsPrime
f' : R →+* S ⧸ I := (Quotient.mk I).comp f
e : RingHom.ker f' = comap f I
⊢ ∃ p', p'.IsPrime ∧ I ≤ p' ∧ comap f p' = p