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

Tactic:
exact Ideal.mk_ker.symm.trans_le (Ideal.comap_mono bot_le)

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
⊢ RingHom.ker f' = comap f I

Tactic:
ext1

Result:
case 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
x✝ : R
⊢ x✝ ∈ RingHom.ker f' ↔ x✝ ∈ comap f I

Proof state:
case 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
x✝ : R
⊢ x✝ ∈ RingHom.ker f' ↔ x✝ ∈ comap f I

Tactic:
exact Submodule.Quotient.mk_eq_zero _

Result:
no goals

Proof state:
case h.e'_3
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 = comap (Quotient.mk (RingHom.ker f')) (map (Quotient.mk (RingHom.ker f')) p)

Tactic:
rwa [Ideal.comap_map_of_surjective (Ideal.Quotient.mk <| RingHom.ker f')
  Ideal.Quotient.mk_surjective, eq_comm, sup_eq_left]

Result:
no goals

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

Tactic:
apply H.2

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))) q).IsPrime ∧
    comap f I ≤ comap (Quotient.mk (RingHom.ker ((Quotient.mk I).comp f))) q

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

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
⊢ map (Quotient.mk (RingHom.ker f')) p ∈ minimalPrimes (R ⧸ RingHom.ker f')

Tactic:
refine ⟨⟨?_, bot_le⟩, ?_⟩

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
⊢ (map (Quotient.mk (RingHom.ker f')) p).IsPrime

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

Proof state:
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
⊢ (map (Quotient.mk (RingHom.ker f')) p).IsPrime

Tactic:
apply Ideal.map_isPrime_of_surjective _ 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
⊢ Function.Surjective ⇑(Quotient.mk (RingHom.ker f'))

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
⊢ RingHom.ker (Quotient.mk (RingHom.ker f')) ≤ p

Tactic:
rw [Ideal.mk_ker, e]

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
⊢ comap f I ≤ p