-- Mathlib/RingTheory/Ideal/Maps.lean
theorem map_isPrime_of_surjective {f : F} (hf : Function.Surjective f) {I : Ideal R} [H : IsPrime I]
    (hk : RingHom.ker f ≤ I) : IsPrime (map f I)

Proof state:
case h.e'_5
R : Type u_1
S : Type u_2
F : Type u_3
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : FunLike F R S
rc : RingHomClass F R S
f : F
hf : Function.Surjective ⇑f
I : Ideal R
H : I.IsPrime
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 - a * b) = 0
⊢ a * b = c - (c - a * b)

Tactic:
abel

Result:
no goals

Proof state:
case refine_2.intro.intro
R : Type u_1
S : Type u_2
F : Type u_3
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : FunLike F R S
rc : RingHomClass F R S
f : F
hf : Function.Surjective ⇑f
I : Ideal R
H : I.IsPrime
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 - a * b) = 0
⊢ x ∈ map f I ∨ y ∈ map f I

Tactic:
have : a * b ∈ I := by
  convert I.sub_mem hc (hk (hc' : c - a * b ∈ RingHom.ker f)) using 1
  abel

Result:
case refine_2.intro.intro
R : Type u_1
S : Type u_2
F : Type u_3
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : FunLike F R S
rc : RingHomClass F R S
f : F
hf : Function.Surjective ⇑f
I : Ideal R
H : I.IsPrime
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 - a * b) = 0
this : a * b ∈ I
⊢ x ∈ map f I ∨ y ∈ map f I

Proof state:
case refine_2
R : Type u_1
S : Type u_2
F : Type u_3
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : FunLike F R S
rc : RingHomClass F R S
f : F
hf : Function.Surjective ⇑f
I : Ideal R
H : I.IsPrime
hk : RingHom.ker f ≤ I
x y : S
⊢ x * y ∈ map f I → x ∈ map f I ∨ y ∈ map f I

Tactic:
refine fun hxy => (hf x).recOn fun a ha => (hf y).recOn fun b hb => ?_

Result:
case refine_2
R : Type u_1
S : Type u_2
F : Type u_3
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : FunLike F R S
rc : RingHomClass F R S
f : F
hf : Function.Surjective ⇑f
I : Ideal R
H : I.IsPrime
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

Proof state:
case refine_1
R : Type u_1
S : Type u_2
F : Type u_3
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : FunLike F R S
rc : RingHomClass F R S
f : F
hf : Function.Surjective ⇑f
I : Ideal R
H : I.IsPrime
hk : RingHom.ker f ≤ I
h : comap f (map f I) = comap f ⊤
⊢ ⊤ ≤ I

Tactic:
rw [comap_map_of_surjective _ hf, comap_top] at h

Result:
case refine_1
R : Type u_1
S : Type u_2
F : Type u_3
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : FunLike F R S
rc : RingHomClass F R S
f : F
hf : Function.Surjective ⇑f
I : Ideal R
H : I.IsPrime
hk : RingHom.ker f ≤ I
h : I ⊔ comap f ⊥ = ⊤
⊢ ⊤ ≤ I

Proof state:
R : Type u_1
S : Type u_2
F : Type u_3
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : FunLike F R S
rc : RingHomClass F R S
f : F
hf : Function.Surjective ⇑f
I : Ideal R
H : I.IsPrime
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 - a * b) = 0
⊢ a * b ∈ I

Tactic:
convert I.sub_mem hc (hk (hc' : c - a * b ∈ RingHom.ker f)) using 1

Result:
case h.e'_5
R : Type u_1
S : Type u_2
F : Type u_3
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : FunLike F R S
rc : RingHomClass F R S
f : F
hf : Function.Surjective ⇑f
I : Ideal R
H : I.IsPrime
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 - a * b) = 0
⊢ a * b = c - (c - a * b)

Proof state:
case refine_2
R : Type u_1
S : Type u_2
F : Type u_3
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : FunLike F R S
rc : RingHomClass F R S
f : F
hf : Function.Surjective ⇑f
I : Ideal R
H : I.IsPrime
hk : RingHom.ker f ≤ I
x y : S
a : R
ha : f a = x
b : R
hxy : ∃ x ∈ I, f x = f (a * b)
hb : f b = y
⊢ x ∈ map f I ∨ y ∈ map f I

Tactic:
rcases hxy with ⟨c, hc, hc'⟩

Result:
case refine_2.intro.intro
R : Type u_1
S : Type u_2
F : Type u_3
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : FunLike F R S
rc : RingHomClass F R S
f : F
hf : Function.Surjective ⇑f
I : Ideal R
H : I.IsPrime
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

Proof state:
case refine_2.intro.intro
R : Type u_1
S : Type u_2
F : Type u_3
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : FunLike F R S
rc : RingHomClass F R S
f : F
hf : Function.Surjective ⇑f
I : Ideal R
H : I.IsPrime
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 - a * b) = 0
this : a * b ∈ I
⊢ x ∈ map f I ∨ y ∈ map f I

Tactic:
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

Result:
no goals

Proof state:
R : Type u_1
S : Type u_2
F : Type u_3
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : FunLike F R S
rc : RingHomClass F R S
f : F
hf : Function.Surjective ⇑f
I : Ideal R
H : I.IsPrime
hk : RingHom.ker f ≤ I
⊢ (map f I).IsPrime

Tactic:
refine ⟨fun h => H.ne_top (eq_top_iff.2 ?_), fun {x y} => ?_⟩

Result:
case refine_1
R : Type u_1
S : Type u_2
F : Type u_3
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : FunLike F R S
rc : RingHomClass F R S
f : F
hf : Function.Surjective ⇑f
I : Ideal R
H : I.IsPrime
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
inst✝ : FunLike F R S
rc : RingHomClass F R S
f : F
hf : Function.Surjective ⇑f
I : Ideal R
H : I.IsPrime
hk : RingHom.ker f ≤ I
x y : S
⊢ x * y ∈ map f I → x ∈ map f I ∨ y ∈ map f I

Proof state:
case refine_1
R : Type u_1
S : Type u_2
F : Type u_3
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : FunLike F R S
rc : RingHomClass F R S
f : F
hf : Function.Surjective ⇑f
I : Ideal R
H : I.IsPrime
hk : RingHom.ker f ≤ I
h : map f I = ⊤
⊢ ⊤ ≤ I

Tactic:
replace h := congr_arg (comap f) h

Result:
case refine_1
R : Type u_1
S : Type u_2
F : Type u_3
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : FunLike F R S
rc : RingHomClass F R S
f : F
hf : Function.Surjective ⇑f
I : Ideal R
H : I.IsPrime
hk : RingHom.ker f ≤ I
h : comap f (map f I) = comap f ⊤
⊢ ⊤ ≤ I

Proof state:
case refine_2.intro.intro
R : Type u_1
S : Type u_2
F : Type u_3
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : FunLike F R S
rc : RingHomClass F R S
f : F
hf : Function.Surjective ⇑f
I : Ideal R
H : I.IsPrime
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

Tactic:
rw [← sub_eq_zero, ← map_sub] at hc'

Result:
case refine_2.intro.intro
R : Type u_1
S : Type u_2
F : Type u_3
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : FunLike F R S
rc : RingHomClass F R S
f : F
hf : Function.Surjective ⇑f
I : Ideal R
H : I.IsPrime
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 - a * b) = 0
⊢ x ∈ map f I ∨ y ∈ map f I

Proof state:
case refine_1
R : Type u_1
S : Type u_2
F : Type u_3
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : FunLike F R S
rc : RingHomClass F R S
f : F
hf : Function.Surjective ⇑f
I : Ideal R
H : I.IsPrime
hk : RingHom.ker f ≤ I
h : I ⊔ comap f ⊥ = ⊤
⊢ ⊤ ≤ I

Tactic:
exact h ▸ sup_le (le_of_eq rfl) hk

Result:
no goals

Proof state:
case refine_2
R : Type u_1
S : Type u_2
F : Type u_3
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : FunLike F R S
rc : RingHomClass F R S
f : F
hf : Function.Surjective ⇑f
I : Ideal R
H : I.IsPrime
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

Tactic:
rw [← ha, ← hb, ← _root_.map_mul f, mem_map_iff_of_surjective _ hf] at hxy

Result:
case refine_2
R : Type u_1
S : Type u_2
F : Type u_3
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : FunLike F R S
rc : RingHomClass F R S
f : F
hf : Function.Surjective ⇑f
I : Ideal R
H : I.IsPrime
hk : RingHom.ker f ≤ I
x y : S
a : R
ha : f a = x
b : R
hxy : ∃ x ∈ I, f x = f (a * b)
hb : f b = y
⊢ x ∈ map f I ∨ y ∈ map f I