case intro.intro.intro
R : Type u_2
S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
I✝ J : Ideal R
I : Ideal S
f : R →+* S
p : Ideal R
H : p ∈ Ideal.minimalPrimes (comap f I)
p' : Ideal S
h₁ : IsPrime p'
h₂ : I ≤ p'
h₃ : comap f p' = p
⊢ ∃ p', p' ∈ Ideal.minimalPrimes I ∧ comap f p' = p
R : Type u_2
S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
I✝ J : Ideal R
I : Ideal S
f : R →+* S
p : Ideal R
H : p ∈ Ideal.minimalPrimes (comap f I)
⊢ ∃ p', p' ∈ Ideal.minimalPrimes I ∧ comap f p' = p
obtain ⟨p', h₁, h₂, h₃⟩ := Ideal.exists_comap_eq_of_mem_minimalPrimes f p H
case intro.intro.intro.intro.intro
R : Type u_2
S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
I✝ J : Ideal R
I : Ideal S
f : R →+* S
p : Ideal R
H : p ∈ Ideal.minimalPrimes (comap f I)
p' : Ideal S
h₁ : IsPrime p'
h₂ : I ≤ p'
h₃ : comap f p' = p
q : Ideal S
hq : q ∈ Ideal.minimalPrimes I
hq' : q ≤ p'
⊢ ∃ p', p' ∈ Ideal.minimalPrimes I ∧ comap f p' = p
case intro.intro.intro
R : Type u_2
S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
I✝ J : Ideal R
I : Ideal S
f : R →+* S
p : Ideal R
H : p ∈ Ideal.minimalPrimes (comap f I)
p' : Ideal S
h₁ : IsPrime p'
h₂ : I ≤ p'
h₃ : comap f p' = p
⊢ ∃ p', p' ∈ Ideal.minimalPrimes I ∧ comap f p' = p
obtain ⟨q, hq, hq'⟩ := Ideal.exists_minimalPrimes_le h₂
case intro.intro.intro.intro.intro
R : Type u_2
S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
I✝ J : Ideal R
I : Ideal S
f : R →+* S
p : Ideal R
H : p ∈ Ideal.minimalPrimes (comap f I)
p' : Ideal S
h₁ : IsPrime p'
h₂ : I ≤ p'
h₃ : comap f p' = p
q : Ideal S
hq : q ∈ Ideal.minimalPrimes I
hq' : q ≤ p'
⊢ p = comap f q
case intro.intro.intro.intro.intro
R : Type u_2
S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
I✝ J : Ideal R
I : Ideal S
f : R →+* S
p : Ideal R
H : p ∈ Ideal.minimalPrimes (comap f I)
p' : Ideal S
h₁ : IsPrime p'
h₂ : I ≤ p'
h₃ : comap f p' = p
q : Ideal S
hq : q ∈ Ideal.minimalPrimes I
hq' : q ≤ p'
⊢ ∃ p', p' ∈ Ideal.minimalPrimes I ∧ comap f p' = p
refine' ⟨q, hq, Eq.symm _⟩
case intro.intro.intro.intro.intro
R : Type u_2
S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
I✝ J : Ideal R
I : Ideal S
f : R →+* S
p : Ideal R
H : p ∈ Ideal.minimalPrimes (comap f I)
p' : Ideal S
h₁ : IsPrime p'
h₂ : I ≤ p'
h₃ : comap f p' = p
q : Ideal S
hq : q ∈ Ideal.minimalPrimes I
hq' : q ≤ p'
this : IsPrime q
⊢ p = comap f q
case intro.intro.intro.intro.intro
R : Type u_2
S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
I✝ J : Ideal R
I : Ideal S
f : R →+* S
p : Ideal R
H : p ∈ Ideal.minimalPrimes (comap f I)
p' : Ideal S
h₁ : IsPrime p'
h₂ : I ≤ p'
h₃ : comap f p' = p
q : Ideal S
hq : q ∈ Ideal.minimalPrimes I
hq' : q ≤ p'
⊢ p = comap f q
have := hq.1.1
case intro.intro.intro.intro.intro
R : Type u_2
S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
I✝ J : Ideal R
I : Ideal S
f : R →+* S
p : Ideal R
H : p ∈ Ideal.minimalPrimes (comap f I)
p' : Ideal S
h₁ : IsPrime p'
h₂ : I ≤ p'
h₃ : comap f p' = p
q : Ideal S
hq : q ∈ Ideal.minimalPrimes I
hq' : q ≤ p'
this✝ : IsPrime q
this : comap f q ≤ p
⊢ p = comap f q
case intro.intro.intro.intro.intro
R : Type u_2
S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
I✝ J : Ideal R
I : Ideal S
f : R →+* S
p : Ideal R
H : p ∈ Ideal.minimalPrimes (comap f I)
p' : Ideal S
h₁ : IsPrime p'
h₂ : I ≤ p'
h₃ : comap f p' = p
q : Ideal S
hq : q ∈ Ideal.minimalPrimes I
hq' : q ≤ p'
this : IsPrime q
⊢ p = comap f q
have := (Ideal.comap_mono hq').trans_eq h₃
no goals
case intro.intro.intro.intro.intro
R : Type u_2
S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
I✝ J : Ideal R
I : Ideal S
f : R →+* S
p : Ideal R
H : p ∈ Ideal.minimalPrimes (comap f I)
p' : Ideal S
h₁ : IsPrime p'
h₂ : I ≤ p'
h₃ : comap f p' = p
q : Ideal S
hq : q ∈ Ideal.minimalPrimes I
hq' : q ≤ p'
this✝ : IsPrime q
this : comap f q ≤ p
⊢ p = comap f q
exact (H.2 ⟨inferInstance, Ideal.comap_mono hq.1.2⟩ this).antisymm this