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

Proof state:
case intro.intro.intro.intro.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
p' : Ideal S
h₁ : p'.IsPrime
h₂ : I ≤ p'
h₃ : comap f p' = p
q : Ideal S
hq : q ∈ I.minimalPrimes
hq' : q ≤ p'
this✝ : q.IsPrime
this : comap f q ≤ p
⊢ p = comap f q

Tactic:
exact (H.2 ⟨inferInstance, Ideal.comap_mono hq.1.2⟩ this).antisymm this

Result:
no goals

Proof state:
case intro.intro.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
p' : Ideal S
h₁ : p'.IsPrime
h₂ : I ≤ p'
h₃ : comap f p' = p
⊢ ∃ p' ∈ I.minimalPrimes, comap f p' = p

Tactic:
obtain ⟨q, hq, hq'⟩ := Ideal.exists_minimalPrimes_le h₂

Result:
case intro.intro.intro.intro.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
p' : Ideal S
h₁ : p'.IsPrime
h₂ : I ≤ p'
h₃ : comap f p' = p
q : Ideal S
hq : q ∈ I.minimalPrimes
hq' : q ≤ p'
⊢ ∃ p' ∈ I.minimalPrimes, comap f p' = p

Proof state:
case intro.intro.intro.intro.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
p' : Ideal S
h₁ : p'.IsPrime
h₂ : I ≤ p'
h₃ : comap f p' = p
q : Ideal S
hq : q ∈ I.minimalPrimes
hq' : q ≤ p'
this : q.IsPrime
⊢ p = comap f q

Tactic:
have := (Ideal.comap_mono hq').trans_eq h₃

Result:
case intro.intro.intro.intro.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
p' : Ideal S
h₁ : p'.IsPrime
h₂ : I ≤ p'
h₃ : comap f p' = p
q : Ideal S
hq : q ∈ I.minimalPrimes
hq' : q ≤ p'
this✝ : q.IsPrime
this : comap f q ≤ p
⊢ p = comap f q

Proof state:
case intro.intro.intro.intro.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
p' : Ideal S
h₁ : p'.IsPrime
h₂ : I ≤ p'
h₃ : comap f p' = p
q : Ideal S
hq : q ∈ I.minimalPrimes
hq' : q ≤ p'
⊢ ∃ p' ∈ I.minimalPrimes, comap f p' = p

Tactic:
refine ⟨q, hq, Eq.symm ?_⟩

Result:
case intro.intro.intro.intro.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
p' : Ideal S
h₁ : p'.IsPrime
h₂ : I ≤ p'
h₃ : comap f p' = p
q : Ideal S
hq : q ∈ I.minimalPrimes
hq' : q ≤ p'
⊢ p = comap f q

Proof state:
case intro.intro.intro.intro.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
p' : Ideal S
h₁ : p'.IsPrime
h₂ : I ≤ p'
h₃ : comap f p' = p
q : Ideal S
hq : q ∈ I.minimalPrimes
hq' : q ≤ p'
⊢ p = comap f q

Tactic:
have := hq.1.1

Result:
case intro.intro.intro.intro.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
p' : Ideal S
h₁ : p'.IsPrime
h₂ : I ≤ p'
h₃ : comap f p' = p
q : Ideal S
hq : q ∈ I.minimalPrimes
hq' : q ≤ p'
this : q.IsPrime
⊢ p = comap 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
⊢ ∃ p' ∈ I.minimalPrimes, comap f p' = p

Tactic:
obtain ⟨p', h₁, h₂, h₃⟩ := Ideal.exists_comap_eq_of_mem_minimalPrimes f p H

Result:
case intro.intro.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
p' : Ideal S
h₁ : p'.IsPrime
h₂ : I ≤ p'
h₃ : comap f p' = p
⊢ ∃ p' ∈ I.minimalPrimes, comap f p' = p