-- Mathlib/RingTheory/Ideal/MinimalPrime/Localization.lean
theorem Ideal.comap_minimalPrimes_eq_of_surjective {f : R →+* S} (hf : Function.Surjective f)
    (I : Ideal S) : (I.comap f).minimalPrimes = Ideal.comap f '' I.minimalPrimes

Proof state:
case h.mp
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Function.Surjective ⇑f
I : Ideal S
J : Ideal R
⊢ J ∈ (comap f I).minimalPrimes → J ∈ comap f '' I.minimalPrimes

Tactic:
intro H

Result:
case h.mp
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Function.Surjective ⇑f
I : Ideal S
J : Ideal R
H : J ∈ (comap f I).minimalPrimes
⊢ J ∈ comap f '' I.minimalPrimes

Proof state:
case h.mpr.intro.intro
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Function.Surjective ⇑f
I J : Ideal S
hJ : J ∈ I.minimalPrimes
⊢ comap f J ∈ (comap f I).minimalPrimes

Tactic:
exact Ideal.minimal_primes_comap_of_surjective hf hJ

Result:
no goals

Proof state:
case h.mp
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Function.Surjective ⇑f
I : Ideal S
J : Ideal R
H : J ∈ (comap f I).minimalPrimes
⊢ J ∈ comap f '' I.minimalPrimes

Tactic:
obtain ⟨p, h, rfl⟩ := Ideal.exists_minimalPrimes_comap_eq f J H

Result:
case h.mp.intro.intro
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Function.Surjective ⇑f
I p : Ideal S
h : p ∈ I.minimalPrimes
H : comap f p ∈ (comap f I).minimalPrimes
⊢ comap f p ∈ comap f '' I.minimalPrimes

Proof state:
case h
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Function.Surjective ⇑f
I : Ideal S
J : Ideal R
⊢ J ∈ (comap f I).minimalPrimes ↔ J ∈ comap f '' I.minimalPrimes

Tactic:
constructor

Result:
case h.mp
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Function.Surjective ⇑f
I : Ideal S
J : Ideal R
⊢ J ∈ (comap f I).minimalPrimes → J ∈ comap f '' I.minimalPrimes

case h.mpr
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Function.Surjective ⇑f
I : Ideal S
J : Ideal R
⊢ J ∈ comap f '' I.minimalPrimes → J ∈ (comap f I).minimalPrimes

Proof state:
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Function.Surjective ⇑f
I : Ideal S
⊢ (comap f I).minimalPrimes = comap f '' I.minimalPrimes

Tactic:
ext J

Result:
case h
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Function.Surjective ⇑f
I : Ideal S
J : Ideal R
⊢ J ∈ (comap f I).minimalPrimes ↔ J ∈ comap f '' I.minimalPrimes

Proof state:
case h.mp.intro.intro
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Function.Surjective ⇑f
I p : Ideal S
h : p ∈ I.minimalPrimes
H : comap f p ∈ (comap f I).minimalPrimes
⊢ comap f p ∈ comap f '' I.minimalPrimes

Tactic:
exact ⟨p, h, rfl⟩

Result:
no goals

Proof state:
case h.mpr
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Function.Surjective ⇑f
I : Ideal S
J : Ideal R
⊢ J ∈ comap f '' I.minimalPrimes → J ∈ (comap f I).minimalPrimes

Tactic:
rintro ⟨J, hJ, rfl⟩

Result:
case h.mpr.intro.intro
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Function.Surjective ⇑f
I J : Ideal S
hJ : J ∈ I.minimalPrimes
⊢ comap f J ∈ (comap f I).minimalPrimes