case refine'_1
R : Type u_1
S : Type u_2
F : Type u_3
inst✝¹ : Ring R
inst✝ : Ring S
rc : RingHomClass F R S
f : F
hf : Function.Surjective ↑f
I : Ideal R
H : IsPrime I
hk : RingHom.ker f ≤ I
h : map f I = ⊤
⊢ ⊤ ≤ I

case refine'_2
R : Type u_1
S : Type u_2
F : Type u_3
inst✝¹ : Ring R
inst✝ : Ring S
rc : RingHomClass F R S
f : F
hf : Function.Surjective ↑f
I : Ideal R
H : IsPrime I
hk : RingHom.ker f ≤ I
x y : S
⊢ x * y ∈ map f I → x ∈ map f I ∨ y ∈ map f I
R : Type u_1
S : Type u_2
F : Type u_3
inst✝¹ : Ring R
inst✝ : Ring S
rc : RingHomClass F R S
f : F
hf : Function.Surjective ↑f
I : Ideal R
H : IsPrime I
hk : RingHom.ker f ≤ I
⊢ IsPrime (map f I)
refine' ⟨fun h => H.ne_top (eq_top_iff.2 _), fun {x y} => _⟩
case refine'_1
R : Type u_1
S : Type u_2
F : Type u_3
inst✝¹ : Ring R
inst✝ : Ring S
rc : RingHomClass F R S
f : F
hf : Function.Surjective ↑f
I : Ideal R
H : IsPrime I
hk : RingHom.ker f ≤ I
h : comap f (map f I) = comap f ⊤
⊢ ⊤ ≤ I
case refine'_1
R : Type u_1
S : Type u_2
F : Type u_3
inst✝¹ : Ring R
inst✝ : Ring S
rc : RingHomClass F R S
f : F
hf : Function.Surjective ↑f
I : Ideal R
H : IsPrime I
hk : RingHom.ker f ≤ I
h : map f I = ⊤
⊢ ⊤ ≤ I
replace h := congr_arg (comap f) h
case refine'_1
R : Type u_1
S : Type u_2
F : Type u_3
inst✝¹ : Ring R
inst✝ : Ring S
rc : RingHomClass F R S
f : F
hf : Function.Surjective ↑f
I : Ideal R
H : IsPrime I
hk : RingHom.ker f ≤ I
h : I ⊔ comap f ⊥ = ⊤
⊢ ⊤ ≤ I
case refine'_1
R : Type u_1
S : Type u_2
F : Type u_3
inst✝¹ : Ring R
inst✝ : Ring S
rc : RingHomClass F R S
f : F
hf : Function.Surjective ↑f
I : Ideal R
H : IsPrime I
hk : RingHom.ker f ≤ I
h : comap f (map f I) = comap f ⊤
⊢ ⊤ ≤ I
rw [comap_map_of_surjective _ hf, comap_top] at h
no goals
case refine'_1
R : Type u_1
S : Type u_2
F : Type u_3
inst✝¹ : Ring R
inst✝ : Ring S
rc : RingHomClass F R S
f : F
hf : Function.Surjective ↑f
I : Ideal R
H : IsPrime I
hk : RingHom.ker f ≤ I
h : I ⊔ comap f ⊥ = ⊤
⊢ ⊤ ≤ I
exact h ▸ sup_le (le_of_eq rfl) hk
case refine'_2
R : Type u_1
S : Type u_2
F : Type u_3
inst✝¹ : Ring R
inst✝ : Ring S
rc : RingHomClass F R S
f : F
hf : Function.Surjective ↑f
I : Ideal R
H : IsPrime I
hk : RingHom.ker f ≤ I
x y : S
hxy : x * y ∈ map f I
a : R
ha : ↑f a = x
b : R
hb : ↑f b = y
⊢ x ∈ map f I ∨ y ∈ map f I
case refine'_2
R : Type u_1
S : Type u_2
F : Type u_3
inst✝¹ : Ring R
inst✝ : Ring S
rc : RingHomClass F R S
f : F
hf : Function.Surjective ↑f
I : Ideal R
H : IsPrime I
hk : RingHom.ker f ≤ I
x y : S
⊢ x * y ∈ map f I → x ∈ map f I ∨ y ∈ map f I
refine' fun hxy => (hf x).recOn fun a ha => (hf y).recOn fun b hb => _
case refine'_2
R : Type u_1
S : Type u_2
F : Type u_3
inst✝¹ : Ring R
inst✝ : Ring S
rc : RingHomClass F R S
f : F
hf : Function.Surjective ↑f
I : Ideal R
H : IsPrime I
hk : RingHom.ker f ≤ I
x y : S
a : R
ha : ↑f a = x
b : R
hxy : ∃ x, x ∈ I ∧ ↑f x = ↑f (a * b)
hb : ↑f b = y
⊢ x ∈ map f I ∨ y ∈ map f I
case refine'_2
R : Type u_1
S : Type u_2
F : Type u_3
inst✝¹ : Ring R
inst✝ : Ring S
rc : RingHomClass F R S
f : F
hf : Function.Surjective ↑f
I : Ideal R
H : IsPrime I
hk : RingHom.ker f ≤ I
x y : S
hxy : x * y ∈ map f I
a : R
ha : ↑f a = x
b : R
hb : ↑f b = y
⊢ x ∈ map f I ∨ y ∈ map f I
rw [← ha, ← hb, ← _root_.map_mul f, mem_map_iff_of_surjective _ hf] at hxy
case refine'_2.intro.intro
R : Type u_1
S : Type u_2
F : Type u_3
inst✝¹ : Ring R
inst✝ : Ring S
rc : RingHomClass F R S
f : F
hf : Function.Surjective ↑f
I : Ideal R
H : IsPrime I
hk : RingHom.ker f ≤ I
x y : S
a : R
ha : ↑f a = x
b : R
hb : ↑f b = y
c : R
hc : c ∈ I
hc' : ↑f c = ↑f (a * b)
⊢ x ∈ map f I ∨ y ∈ map f I
case refine'_2
R : Type u_1
S : Type u_2
F : Type u_3
inst✝¹ : Ring R
inst✝ : Ring S
rc : RingHomClass F R S
f : F
hf : Function.Surjective ↑f
I : Ideal R
H : IsPrime I
hk : RingHom.ker f ≤ I
x y : S
a : R
ha : ↑f a = x
b : R
hxy : ∃ x, x ∈ I ∧ ↑f x = ↑f (a * b)
hb : ↑f b = y
⊢ x ∈ map f I ∨ y ∈ map f I
rcases hxy with ⟨c, hc, hc'⟩
case refine'_2.intro.intro
R : Type u_1
S : Type u_2
F : Type u_3
inst✝¹ : Ring R
inst✝ : Ring S
rc : RingHomClass F R S
f : F
hf : Function.Surjective ↑f
I : Ideal R
H : IsPrime I
hk : RingHom.ker f ≤ I
x y : S
a : R
ha : ↑f a = x
b : R
hb : ↑f b = y
c : R
hc : c ∈ I
hc'✝ : ↑f c = ↑f (a * b)
hc' : ↑f (c - a * b) = 0
⊢ x ∈ map f I ∨ y ∈ map f I
case refine'_2.intro.intro
R : Type u_1
S : Type u_2
F : Type u_3
inst✝¹ : Ring R
inst✝ : Ring S
rc : RingHomClass F R S
f : F
hf : Function.Surjective ↑f
I : Ideal R
H : IsPrime I
hk : RingHom.ker f ≤ I
x y : S
a : R
ha : ↑f a = x
b : R
hb : ↑f b = y
c : R
hc : c ∈ I
hc' : ↑f c = ↑f (a * b)
⊢ x ∈ map f I ∨ y ∈ map f I
rw [← sub_eq_zero, ← map_sub] at hc'
case refine'_2.intro.intro
R : Type u_1
S : Type u_2
F : Type u_3
inst✝¹ : Ring R
inst✝ : Ring S
rc : RingHomClass F R S
f : F
hf : Function.Surjective ↑f
I : Ideal R
H : IsPrime I
hk : RingHom.ker f ≤ I
x y : S
a : R
ha : ↑f a = x
b : R
hb : ↑f b = y
c : R
hc : c ∈ I
hc'✝ : ↑f c = ↑f (a * b)
hc' : ↑f (c - a * b) = 0
this : a * b ∈ I
⊢ x ∈ map f I ∨ y ∈ map f I
case refine'_2.intro.intro
R : Type u_1
S : Type u_2
F : Type u_3
inst✝¹ : Ring R
inst✝ : Ring S
rc : RingHomClass F R S
f : F
hf : Function.Surjective ↑f
I : Ideal R
H : IsPrime I
hk : RingHom.ker f ≤ I
x y : S
a : R
ha : ↑f a = x
b : R
hb : ↑f b = y
c : R
hc : c ∈ I
hc'✝ : ↑f c = ↑f (a * b)
hc' : ↑f (c - a * b) = 0
⊢ x ∈ map f I ∨ y ∈ map f I
have : a * b ∈ I := by
  convert I.sub_mem hc (hk (hc' : c - a * b ∈ RingHom.ker f)) using 1
  abel
no goals
case refine'_2.intro.intro
R : Type u_1
S : Type u_2
F : Type u_3
inst✝¹ : Ring R
inst✝ : Ring S
rc : RingHomClass F R S
f : F
hf : Function.Surjective ↑f
I : Ideal R
H : IsPrime I
hk : RingHom.ker f ≤ I
x y : S
a : R
ha : ↑f a = x
b : R
hb : ↑f b = y
c : R
hc : c ∈ I
hc'✝ : ↑f c = ↑f (a * b)
hc' : ↑f (c - a * b) = 0
this : a * b ∈ I
⊢ x ∈ map f I ∨ y ∈ map f I
exact
  (H.mem_or_mem this).imp (fun h => ha ▸ mem_map_of_mem f h) fun h => hb ▸ mem_map_of_mem f h
case h.e'_4
R : Type u_1
S : Type u_2
F : Type u_3
inst✝¹ : Ring R
inst✝ : Ring S
rc : RingHomClass F R S
f : F
hf : Function.Surjective ↑f
I : Ideal R
H : IsPrime I
hk : RingHom.ker f ≤ I
x y : S
a : R
ha : ↑f a = x
b : R
hb : ↑f b = y
c : R
hc : c ∈ I
hc'✝ : ↑f c = ↑f (a * b)
hc' : ↑f (c - a * b) = 0
⊢ a * b = c - (c - a * b)
R : Type u_1
S : Type u_2
F : Type u_3
inst✝¹ : Ring R
inst✝ : Ring S
rc : RingHomClass F R S
f : F
hf : Function.Surjective ↑f
I : Ideal R
H : IsPrime I
hk : RingHom.ker f ≤ I
x y : S
a : R
ha : ↑f a = x
b : R
hb : ↑f b = y
c : R
hc : c ∈ I
hc'✝ : ↑f c = ↑f (a * b)
hc' : ↑f (c - a * b) = 0
⊢ a * b ∈ I
convert I.sub_mem hc (hk (hc' : c - a * b ∈ RingHom.ker f)) using 1
no goals
case h.e'_4
R : Type u_1
S : Type u_2
F : Type u_3
inst✝¹ : Ring R
inst✝ : Ring S
rc : RingHomClass F R S
f : F
hf : Function.Surjective ↑f
I : Ideal R
H : IsPrime I
hk : RingHom.ker f ≤ I
x y : S
a : R
ha : ↑f a = x
b : R
hb : ↑f b = y
c : R
hc : c ∈ I
hc'✝ : ↑f c = ↑f (a * b)
hc' : ↑f (c - a * b) = 0
⊢ a * b = c - (c - a * b)
abel