-- Mathlib/RingTheory/Ideal/Quotient/PowTransition.lean
lemma Ideal.Quotient.factor_ker (H : I ≤ J) [I.IsTwoSided] [J.IsTwoSided] :
    RingHom.ker (factor H) = J.map (Ideal.Quotient.mk I)

Proof state:
case h.refine_1.intro
R : Type u_1
inst✝² : Ring R
I J : Ideal R
H : I ≤ J
inst✝¹ : I.IsTwoSided
inst✝ : J.IsTwoSided
x : R ⧸ I
r : R
h : (mk I) r ∈ RingHom.ker (factor H)
hr : (mk I) r = x
⊢ (mk I) r ∈ map (mk I) J

Tactic:
simp only [factor, RingHom.mem_ker, lift_mk, eq_zero_iff_mem] at h

Result:
case h.refine_1.intro
R : Type u_1
inst✝² : Ring R
I J : Ideal R
H : I ≤ J
inst✝¹ : I.IsTwoSided
inst✝ : J.IsTwoSided
x : R ⧸ I
r : R
hr : (mk I) r = x
h : r ∈ J
⊢ (mk I) r ∈ map (mk I) J

Proof state:
case h.refine_1
R : Type u_1
inst✝² : Ring R
I J : Ideal R
H : I ≤ J
inst✝¹ : I.IsTwoSided
inst✝ : J.IsTwoSided
x : R ⧸ I
h : x ∈ RingHom.ker (factor H)
⊢ x ∈ map (mk I) J

Tactic:
rcases Ideal.Quotient.mk_surjective x with ⟨r, hr⟩

Result:
case h.refine_1.intro
R : Type u_1
inst✝² : Ring R
I J : Ideal R
H : I ≤ J
inst✝¹ : I.IsTwoSided
inst✝ : J.IsTwoSided
x : R ⧸ I
h : x ∈ RingHom.ker (factor H)
r : R
hr : (mk I) r = x
⊢ x ∈ map (mk I) J

Proof state:
case h.refine_2
R : Type u_1
inst✝² : Ring R
I J : Ideal R
H : I ≤ J
inst✝¹ : I.IsTwoSided
inst✝ : J.IsTwoSided
x : R ⧸ I
h : x ∈ map (mk I) J
⊢ x ∈ RingHom.ker (factor H)

Tactic:
rcases mem_image_of_mem_map_of_surjective _ Ideal.Quotient.mk_surjective h with ⟨r, hr, eq⟩

Result:
case h.refine_2.intro.intro
R : Type u_1
inst✝² : Ring R
I J : Ideal R
H : I ≤ J
inst✝¹ : I.IsTwoSided
inst✝ : J.IsTwoSided
x : R ⧸ I
h : x ∈ map (mk I) J
r : R
hr : r ∈ ↑J
eq : (mk I) r = x
⊢ x ∈ RingHom.ker (factor H)

Proof state:
case h.refine_1.intro
R : Type u_1
inst✝² : Ring R
I J : Ideal R
H : I ≤ J
inst✝¹ : I.IsTwoSided
inst✝ : J.IsTwoSided
x : R ⧸ I
r : R
hr : (mk I) r = x
h : r ∈ J
⊢ (mk I) r ∈ map (mk I) J

Tactic:
exact Ideal.mem_map_of_mem _ h

Result:
no goals

Proof state:
case h.refine_2.intro.intro
R : Type u_1
inst✝² : Ring R
I J : Ideal R
H : I ≤ J
inst✝¹ : I.IsTwoSided
inst✝ : J.IsTwoSided
x : R ⧸ I
h : x ∈ map (mk I) J
r : R
hr : r ∈ ↑J
eq : (mk I) r = x
⊢ x ∈ RingHom.ker (factor H)

Tactic:
simpa [← eq, Ideal.Quotient.eq_zero_iff_mem] using hr

Result:
no goals

Proof state:
R : Type u_1
inst✝² : Ring R
I J : Ideal R
H : I ≤ J
inst✝¹ : I.IsTwoSided
inst✝ : J.IsTwoSided
⊢ RingHom.ker (factor H) = map (mk I) J

Tactic:
ext x

Result:
case h
R : Type u_1
inst✝² : Ring R
I J : Ideal R
H : I ≤ J
inst✝¹ : I.IsTwoSided
inst✝ : J.IsTwoSided
x : R ⧸ I
⊢ x ∈ RingHom.ker (factor H) ↔ x ∈ map (mk I) J

Proof state:
case h.refine_1.intro
R : Type u_1
inst✝² : Ring R
I J : Ideal R
H : I ≤ J
inst✝¹ : I.IsTwoSided
inst✝ : J.IsTwoSided
x : R ⧸ I
h : x ∈ RingHom.ker (factor H)
r : R
hr : (mk I) r = x
⊢ x ∈ map (mk I) J

Tactic:
rw [← hr] at h ⊢

Result:
case h.refine_1.intro
R : Type u_1
inst✝² : Ring R
I J : Ideal R
H : I ≤ J
inst✝¹ : I.IsTwoSided
inst✝ : J.IsTwoSided
x : R ⧸ I
r : R
h : (mk I) r ∈ RingHom.ker (factor H)
hr : (mk I) r = x
⊢ (mk I) r ∈ map (mk I) J

Proof state:
case h
R : Type u_1
inst✝² : Ring R
I J : Ideal R
H : I ≤ J
inst✝¹ : I.IsTwoSided
inst✝ : J.IsTwoSided
x : R ⧸ I
⊢ x ∈ RingHom.ker (factor H) ↔ x ∈ map (mk I) J

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩

Result:
case h.refine_1
R : Type u_1
inst✝² : Ring R
I J : Ideal R
H : I ≤ J
inst✝¹ : I.IsTwoSided
inst✝ : J.IsTwoSided
x : R ⧸ I
h : x ∈ RingHom.ker (factor H)
⊢ x ∈ map (mk I) J

case h.refine_2
R : Type u_1
inst✝² : Ring R
I J : Ideal R
H : I ≤ J
inst✝¹ : I.IsTwoSided
inst✝ : J.IsTwoSided
x : R ⧸ I
h : x ∈ map (mk I) J
⊢ x ∈ RingHom.ker (factor H)