-- 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_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

Tactic:
refine ⟨inferInstance, (Ideal.mk_ker.trans e).symm.trans_le (Ideal.comap_mono bot_le)⟩

Result:
no goals

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

Tactic:
convert congr_arg (Ideal.comap <| Ideal.Quotient.mk <| RingHom.ker f') hp₂

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

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
⊢ ∃ p', p'.IsPrime ∧ I ≤ p' ∧ comap f p' = p

Tactic:
let f' := (Ideal.Quotient.mk I).comp f

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
⊢ ∃ p', p'.IsPrime ∧ I ≤ p' ∧ comap f p' = p

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

Tactic:
rw [Ideal.comap_map_of_surjective]

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
⊢ p ⊔ comap (Quotient.mk (RingHom.ker ((Quotient.mk I).comp f))) ⊥ ≤ p

case refine_2.intro.h.a.hf
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
⊢ Function.Surjective ⇑(Quotient.mk (RingHom.ker ((Quotient.mk I).comp 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
⊢ ∃ p', p'.IsPrime ∧ I ≤ p' ∧ comap f p' = p

Tactic:
have := H.1.1

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
⊢ ∃ p', p'.IsPrime ∧ I ≤ p' ∧ comap 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
e : RingHom.ker f' = comap f I
⊢ ∃ p', p'.IsPrime ∧ I ≤ p' ∧ comap f p' = p

Tactic:
have : RingHom.ker (Ideal.Quotient.mk <| RingHom.ker f') ≤ p := by
  rw [Ideal.mk_ker, e]
  exact H.1.2

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
⊢ ∃ p', p'.IsPrime ∧ I ≤ p' ∧ comap f p' = p

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
⊢ p ⊔ comap (Quotient.mk (RingHom.ker ((Quotient.mk I).comp f))) ⊥ ≤ p

case refine_2.intro.h.a.hf
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
⊢ Function.Surjective ⇑(Quotient.mk (RingHom.ker ((Quotient.mk I).comp f)))

Tactic:
exacts [sup_le rfl.le this, Ideal.Quotient.mk_surjective]

Result:
no goals

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 ≤ q

Tactic:
rw [← Ideal.map_comap_of_surjective
    (Ideal.Quotient.mk (RingHom.ker ((Ideal.Quotient.mk I).comp f)))
    Ideal.Quotient.mk_surjective q]

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