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)
this : IsPrime p
⊢ ∃ p', IsPrime p' ∧ I ≤ p' ∧ 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', IsPrime p' ∧ I ≤ p' ∧ comap f p' = p
have := H.1.1
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)
this : IsPrime p
f' : R →+* S ⧸ I := RingHom.comp (Quotient.mk I) f
⊢ ∃ p', IsPrime p' ∧ I ≤ p' ∧ 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)
this : IsPrime p
⊢ ∃ p', IsPrime p' ∧ I ≤ p' ∧ comap f p' = p
let f' := (Ideal.Quotient.mk I).comp f
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)
this : IsPrime p
f' : R →+* S ⧸ I := RingHom.comp (Quotient.mk I) f
e : RingHom.ker f' = comap f I
⊢ ∃ p', IsPrime p' ∧ I ≤ p' ∧ 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)
this : IsPrime p
f' : R →+* S ⧸ I := RingHom.comp (Quotient.mk I) f
⊢ ∃ p', IsPrime p' ∧ I ≤ p' ∧ comap f p' = p
have e : RingHom.ker f' = I.comap f := by
  ext1
  exact Submodule.Quotient.mk_eq_zero _
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)
this✝ : IsPrime p
f' : R →+* S ⧸ I := RingHom.comp (Quotient.mk I) f
e : RingHom.ker f' = comap f I
this : RingHom.ker (Quotient.mk (RingHom.ker f')) ≤ p
⊢ ∃ p', IsPrime p' ∧ I ≤ p' ∧ 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)
this : IsPrime p
f' : R →+* S ⧸ I := RingHom.comp (Quotient.mk I) f
e : RingHom.ker f' = comap f I
⊢ ∃ p', IsPrime p' ∧ I ≤ p' ∧ comap f p' = p
have : RingHom.ker (Ideal.Quotient.mk <| RingHom.ker f') ≤ p := by
  rw [Ideal.mk_ker, e]
  exact H.1.2
case refine'_1
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)
this✝ : IsPrime p
f' : R →+* S ⧸ I := RingHom.comp (Quotient.mk I) f
e : RingHom.ker f' = comap f I
this : RingHom.ker (Quotient.mk (RingHom.ker f')) ≤ p
⊢ IsPrime (map (Quotient.mk (RingHom.ker f')) p)

case refine'_2
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)
this✝ : IsPrime p
f' : R →+* S ⧸ I := RingHom.comp (Quotient.mk I) f
e : RingHom.ker f' = comap f I
this : RingHom.ker (Quotient.mk (RingHom.ker f')) ≤ p
⊢ ∀ ⦃b : Ideal (R ⧸ RingHom.ker f')⦄,
    b ∈ {p | IsPrime p ∧ ⊥ ≤ p} →
      (fun x x_1 => x ≤ x_1) b (map (Quotient.mk (RingHom.ker f')) p) →
        (fun x x_1 => x ≤ x_1) (map (Quotient.mk (RingHom.ker f')) p) b
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)
this✝ : IsPrime p
f' : R →+* S ⧸ I := RingHom.comp (Quotient.mk I) 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')
refine' ⟨⟨_, bot_le⟩, _⟩
case h
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)
this : IsPrime p
f' : R →+* S ⧸ I := RingHom.comp (Quotient.mk I) f
x✝ : R
⊢ x✝ ∈ RingHom.ker f' ↔ x✝ ∈ comap f I
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)
this : IsPrime p
f' : R →+* S ⧸ I := RingHom.comp (Quotient.mk I) f
⊢ RingHom.ker f' = comap f I
ext1
no goals
case h
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)
this : IsPrime p
f' : R →+* S ⧸ I := RingHom.comp (Quotient.mk I) f
x✝ : R
⊢ x✝ ∈ RingHom.ker f' ↔ x✝ ∈ comap f I
exact Submodule.Quotient.mk_eq_zero _
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)
this : IsPrime p
f' : R →+* S ⧸ I := RingHom.comp (Quotient.mk I) f
e : RingHom.ker f' = comap f I
⊢ comap f I ≤ 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)
this : IsPrime p
f' : R →+* S ⧸ I := RingHom.comp (Quotient.mk I) f
e : RingHom.ker f' = comap f I
⊢ RingHom.ker (Quotient.mk (RingHom.ker f')) ≤ p
rw [Ideal.mk_ker, e]
no goals
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)
this : IsPrime p
f' : R →+* S ⧸ I := RingHom.comp (Quotient.mk I) f
e : RingHom.ker f' = comap f I
⊢ comap f I ≤ p
exact H.1.2
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)
this✝¹ : IsPrime p
f' : R →+* S ⧸ I := RingHom.comp (Quotient.mk I) 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₁ : IsPrime p'
hp₂ : comap (RingHom.kerLift f') p' = map (Quotient.mk (RingHom.ker f')) p
⊢ ∃ p', IsPrime p' ∧ I ≤ p' ∧ 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)
this✝¹ : IsPrime p
f' : R →+* S ⧸ I := RingHom.comp (Quotient.mk I) f
e : RingHom.ker f' = comap f I
this✝ : RingHom.ker (Quotient.mk (RingHom.ker f')) ≤ p
this : ?m.52004
⊢ ∃ p', IsPrime p' ∧ I ≤ p' ∧ comap f p' = p
have ⟨p', hp₁, hp₂⟩ := Ideal.exists_comap_eq_of_mem_minimalPrimes_of_injective
  (RingHom.kerLift_injective f') (p.map <| Ideal.Quotient.mk <| RingHom.ker f') this
case refine'_1
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)
this✝¹ : IsPrime p
f' : R →+* S ⧸ I := RingHom.comp (Quotient.mk I) 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₁ : IsPrime p'
hp₂ : comap (RingHom.kerLift f') p' = map (Quotient.mk (RingHom.ker f')) p
⊢ I ≤ comap (Quotient.mk I) p'

case refine'_2
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)
this✝¹ : IsPrime p
f' : R →+* S ⧸ I := RingHom.comp (Quotient.mk I) 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₁ : IsPrime p'
hp₂ : comap (RingHom.kerLift f') p' = map (Quotient.mk (RingHom.ker f')) p
⊢ comap f (comap (Quotient.mk I) 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)
this✝¹ : IsPrime p
f' : R →+* S ⧸ I := RingHom.comp (Quotient.mk I) 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₁ : IsPrime p'
hp₂ : comap (RingHom.kerLift f') p' = map (Quotient.mk (RingHom.ker f')) p
⊢ ∃ p', IsPrime p' ∧ I ≤ p' ∧ comap f p' = p
refine' ⟨p'.comap <| Ideal.Quotient.mk I, Ideal.IsPrime.comap _, _, _⟩
no goals
case refine'_2
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)
this✝¹ : IsPrime p
f' : R →+* S ⧸ I := RingHom.comp (Quotient.mk I) 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₁ : IsPrime p'
hp₂ : comap (RingHom.kerLift f') p' = map (Quotient.mk (RingHom.ker f')) p
⊢ comap f (comap (Quotient.mk I) p') = p
. convert congr_arg (Ideal.comap <| Ideal.Quotient.mk <| RingHom.ker f') hp₂
  rwa [Ideal.comap_map_of_surjective (Ideal.Quotient.mk <| RingHom.ker f')
    Ideal.Quotient.mk_surjective, eq_comm, sup_eq_left]
no goals
case refine'_1
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)
this✝¹ : IsPrime p
f' : R →+* S ⧸ I := RingHom.comp (Quotient.mk I) 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₁ : IsPrime p'
hp₂ : comap (RingHom.kerLift f') p' = map (Quotient.mk (RingHom.ker f')) p
⊢ I ≤ comap (Quotient.mk I) p'
exact Ideal.mk_ker.symm.trans_le (Ideal.comap_mono bot_le)
case h.e'_3
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)
this✝¹ : IsPrime p
f' : R →+* S ⧸ I := RingHom.comp (Quotient.mk I) 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₁ : IsPrime p'
hp₂ : comap (RingHom.kerLift f') p' = map (Quotient.mk (RingHom.ker f')) p
⊢ p = comap (Quotient.mk (RingHom.ker f')) (map (Quotient.mk (RingHom.ker f')) p)
case refine'_2
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)
this✝¹ : IsPrime p
f' : R →+* S ⧸ I := RingHom.comp (Quotient.mk I) 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₁ : IsPrime p'
hp₂ : comap (RingHom.kerLift f') p' = map (Quotient.mk (RingHom.ker f')) p
⊢ comap f (comap (Quotient.mk I) p') = p
convert congr_arg (Ideal.comap <| Ideal.Quotient.mk <| RingHom.ker f') hp₂
no goals
case h.e'_3
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)
this✝¹ : IsPrime p
f' : R →+* S ⧸ I := RingHom.comp (Quotient.mk I) 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₁ : IsPrime p'
hp₂ : comap (RingHom.kerLift f') p' = map (Quotient.mk (RingHom.ker f')) p
⊢ p = comap (Quotient.mk (RingHom.ker f')) (map (Quotient.mk (RingHom.ker f')) p)
rwa [Ideal.comap_map_of_surjective (Ideal.Quotient.mk <| RingHom.ker f')
  Ideal.Quotient.mk_surjective, eq_comm, sup_eq_left]
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)
this✝ : IsPrime p
f' : R →+* S ⧸ I := RingHom.comp (Quotient.mk I) f
e : RingHom.ker f' = comap f I
this : RingHom.ker (Quotient.mk (RingHom.ker f')) ≤ p
⊢ Function.Surjective ↑(Quotient.mk (RingHom.ker f'))
case refine'_1
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)
this✝ : IsPrime p
f' : R →+* S ⧸ I := RingHom.comp (Quotient.mk I) f
e : RingHom.ker f' = comap f I
this : RingHom.ker (Quotient.mk (RingHom.ker f')) ≤ p
⊢ IsPrime (map (Quotient.mk (RingHom.ker f')) p)
apply Ideal.map_isPrime_of_surjective _ this
no goals
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)
this✝ : IsPrime p
f' : R →+* S ⧸ I := RingHom.comp (Quotient.mk I) f
e : RingHom.ker f' = comap f I
this : RingHom.ker (Quotient.mk (RingHom.ker f')) ≤ p
⊢ Function.Surjective ↑(Quotient.mk (RingHom.ker f'))
exact Ideal.Quotient.mk_surjective
case refine'_2.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)
this✝ : IsPrime p
f' : R →+* S ⧸ I := RingHom.comp (Quotient.mk I) f
e : RingHom.ker f' = comap f I
this : RingHom.ker (Quotient.mk (RingHom.ker f')) ≤ p
q : Ideal (R ⧸ RingHom.ker f')
hq : IsPrime q
hq' : q ≤ map (Quotient.mk (RingHom.ker f')) p
⊢ map (Quotient.mk (RingHom.ker f')) p ≤ q
case refine'_2
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)
this✝ : IsPrime p
f' : R →+* S ⧸ I := RingHom.comp (Quotient.mk I) f
e : RingHom.ker f' = comap f I
this : RingHom.ker (Quotient.mk (RingHom.ker f')) ≤ p
⊢ ∀ ⦃b : Ideal (R ⧸ RingHom.ker f')⦄,
    b ∈ {p | IsPrime p ∧ ⊥ ≤ p} →
      (fun x x_1 => x ≤ x_1) b (map (Quotient.mk (RingHom.ker f')) p) →
        (fun x x_1 => x ≤ x_1) (map (Quotient.mk (RingHom.ker f')) p) b
rintro q ⟨hq, -⟩ hq'
case refine'_2.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)
this✝ : IsPrime p
f' : R →+* S ⧸ I := RingHom.comp (Quotient.mk I) f
e : RingHom.ker f' = comap f I
this : RingHom.ker (Quotient.mk (RingHom.ker f')) ≤ p
q : Ideal (R ⧸ RingHom.ker f')
hq : IsPrime q
hq' : q ≤ map (Quotient.mk (RingHom.ker f')) p
⊢ map (Quotient.mk (RingHom.ker f')) p ≤
    map (Quotient.mk (RingHom.ker (RingHom.comp (Quotient.mk I) f)))
      (comap (Quotient.mk (RingHom.ker (RingHom.comp (Quotient.mk I) f))) q)
case refine'_2.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)
this✝ : IsPrime p
f' : R →+* S ⧸ I := RingHom.comp (Quotient.mk I) f
e : RingHom.ker f' = comap f I
this : RingHom.ker (Quotient.mk (RingHom.ker f')) ≤ p
q : Ideal (R ⧸ RingHom.ker f')
hq : IsPrime q
hq' : q ≤ map (Quotient.mk (RingHom.ker f')) p
⊢ map (Quotient.mk (RingHom.ker f')) p ≤ q
rw [← Ideal.map_comap_of_surjective
    (Ideal.Quotient.mk (RingHom.ker ((Ideal.Quotient.mk I).comp f)))
    Ideal.Quotient.mk_surjective q]
case refine'_2.intro.h
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)
this✝ : IsPrime p
f' : R →+* S ⧸ I := RingHom.comp (Quotient.mk I) f
e : RingHom.ker f' = comap f I
this : RingHom.ker (Quotient.mk (RingHom.ker f')) ≤ p
q : Ideal (R ⧸ RingHom.ker f')
hq : IsPrime q
hq' : q ≤ map (Quotient.mk (RingHom.ker f')) p
⊢ p ≤ comap (Quotient.mk (RingHom.ker (RingHom.comp (Quotient.mk I) f))) q
case refine'_2.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)
this✝ : IsPrime p
f' : R →+* S ⧸ I := RingHom.comp (Quotient.mk I) f
e : RingHom.ker f' = comap f I
this : RingHom.ker (Quotient.mk (RingHom.ker f')) ≤ p
q : Ideal (R ⧸ RingHom.ker f')
hq : IsPrime q
hq' : q ≤ map (Quotient.mk (RingHom.ker f')) p
⊢ map (Quotient.mk (RingHom.ker f')) p ≤
    map (Quotient.mk (RingHom.ker (RingHom.comp (Quotient.mk I) f)))
      (comap (Quotient.mk (RingHom.ker (RingHom.comp (Quotient.mk I) f))) q)
apply Ideal.map_mono
case refine'_2.intro.h.a
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)
this✝ : IsPrime p
f' : R →+* S ⧸ I := RingHom.comp (Quotient.mk I) f
e : RingHom.ker f' = comap f I
this : RingHom.ker (Quotient.mk (RingHom.ker f')) ≤ p
q : Ideal (R ⧸ RingHom.ker f')
hq : IsPrime q
hq' : q ≤ map (Quotient.mk (RingHom.ker f')) p
⊢ comap (Quotient.mk (RingHom.ker (RingHom.comp (Quotient.mk I) f))) q ∈ {p | IsPrime p ∧ comap f I ≤ p}

case refine'_2.intro.h.a
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)
this✝ : IsPrime p
f' : R →+* S ⧸ I := RingHom.comp (Quotient.mk I) f
e : RingHom.ker f' = comap f I
this : RingHom.ker (Quotient.mk (RingHom.ker f')) ≤ p
q : Ideal (R ⧸ RingHom.ker f')
hq : IsPrime q
hq' : q ≤ map (Quotient.mk (RingHom.ker f')) p
⊢ comap (Quotient.mk (RingHom.ker (RingHom.comp (Quotient.mk I) f))) q ≤ p
case refine'_2.intro.h
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)
this✝ : IsPrime p
f' : R →+* S ⧸ I := RingHom.comp (Quotient.mk I) f
e : RingHom.ker f' = comap f I
this : RingHom.ker (Quotient.mk (RingHom.ker f')) ≤ p
q : Ideal (R ⧸ RingHom.ker f')
hq : IsPrime q
hq' : q ≤ map (Quotient.mk (RingHom.ker f')) p
⊢ p ≤ comap (Quotient.mk (RingHom.ker (RingHom.comp (Quotient.mk I) f))) q
apply H.2
no goals
case refine'_2.intro.h.a
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)
this✝ : IsPrime p
f' : R →+* S ⧸ I := RingHom.comp (Quotient.mk I) f
e : RingHom.ker f' = comap f I
this : RingHom.ker (Quotient.mk (RingHom.ker f')) ≤ p
q : Ideal (R ⧸ RingHom.ker f')
hq : IsPrime q
hq' : q ≤ map (Quotient.mk (RingHom.ker f')) p
⊢ comap (Quotient.mk (RingHom.ker (RingHom.comp (Quotient.mk I) f))) q ∈ {p | IsPrime p ∧ comap f I ≤ p}
refine' ⟨inferInstance, (Ideal.mk_ker.trans e).symm.trans_le (Ideal.comap_mono bot_le)⟩
case refine'_2.intro.h.a
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)
this✝ : IsPrime p
f' : R →+* S ⧸ I := RingHom.comp (Quotient.mk I) f
e : RingHom.ker f' = comap f I
this : RingHom.ker (Quotient.mk (RingHom.ker f')) ≤ p
q : Ideal (R ⧸ RingHom.ker f')
hq : IsPrime q
hq' : q ≤ map (Quotient.mk (RingHom.ker f')) p
⊢ comap (Quotient.mk (RingHom.ker (RingHom.comp (Quotient.mk I) f))) (map (Quotient.mk (RingHom.ker f')) p) ≤ p
case refine'_2.intro.h.a
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)
this✝ : IsPrime p
f' : R →+* S ⧸ I := RingHom.comp (Quotient.mk I) f
e : RingHom.ker f' = comap f I
this : RingHom.ker (Quotient.mk (RingHom.ker f')) ≤ p
q : Ideal (R ⧸ RingHom.ker f')
hq : IsPrime q
hq' : q ≤ map (Quotient.mk (RingHom.ker f')) p
⊢ comap (Quotient.mk (RingHom.ker (RingHom.comp (Quotient.mk I) f))) q ≤ p
refine' (Ideal.comap_mono hq').trans _
case refine'_2.intro.h.a
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)
this✝ : IsPrime p
f' : R →+* S ⧸ I := RingHom.comp (Quotient.mk I) f
e : RingHom.ker f' = comap f I
this : RingHom.ker (Quotient.mk (RingHom.ker f')) ≤ p
q : Ideal (R ⧸ RingHom.ker f')
hq : IsPrime q
hq' : q ≤ map (Quotient.mk (RingHom.ker f')) p
⊢ p ⊔ comap (Quotient.mk (RingHom.ker (RingHom.comp (Quotient.mk I) f))) ⊥ ≤ p

case refine'_2.intro.h.a.hf
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)
this✝ : IsPrime p
f' : R →+* S ⧸ I := RingHom.comp (Quotient.mk I) f
e : RingHom.ker f' = comap f I
this : RingHom.ker (Quotient.mk (RingHom.ker f')) ≤ p
q : Ideal (R ⧸ RingHom.ker f')
hq : IsPrime q
hq' : q ≤ map (Quotient.mk (RingHom.ker f')) p
⊢ Function.Surjective ↑(Quotient.mk (RingHom.ker (RingHom.comp (Quotient.mk I) f)))
case refine'_2.intro.h.a
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)
this✝ : IsPrime p
f' : R →+* S ⧸ I := RingHom.comp (Quotient.mk I) f
e : RingHom.ker f' = comap f I
this : RingHom.ker (Quotient.mk (RingHom.ker f')) ≤ p
q : Ideal (R ⧸ RingHom.ker f')
hq : IsPrime q
hq' : q ≤ map (Quotient.mk (RingHom.ker f')) p
⊢ comap (Quotient.mk (RingHom.ker (RingHom.comp (Quotient.mk I) f))) (map (Quotient.mk (RingHom.ker f')) p) ≤ p
rw [Ideal.comap_map_of_surjective]
no goals
case refine'_2.intro.h.a
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)
this✝ : IsPrime p
f' : R →+* S ⧸ I := RingHom.comp (Quotient.mk I) f
e : RingHom.ker f' = comap f I
this : RingHom.ker (Quotient.mk (RingHom.ker f')) ≤ p
q : Ideal (R ⧸ RingHom.ker f')
hq : IsPrime q
hq' : q ≤ map (Quotient.mk (RingHom.ker f')) p
⊢ p ⊔ comap (Quotient.mk (RingHom.ker (RingHom.comp (Quotient.mk I) f))) ⊥ ≤ p

case refine'_2.intro.h.a.hf
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)
this✝ : IsPrime p
f' : R →+* S ⧸ I := RingHom.comp (Quotient.mk I) f
e : RingHom.ker f' = comap f I
this : RingHom.ker (Quotient.mk (RingHom.ker f')) ≤ p
q : Ideal (R ⧸ RingHom.ker f')
hq : IsPrime q
hq' : q ≤ map (Quotient.mk (RingHom.ker f')) p
⊢ Function.Surjective ↑(Quotient.mk (RingHom.ker (RingHom.comp (Quotient.mk I) f)))
exacts [sup_le rfl.le this, Ideal.Quotient.mk_surjective]