-- Mathlib/RingTheory/Ideal/Quotient/PowTransition.lean
lemma Ideal.map_mk_comap_factor [J.IsTwoSided] [K.IsTwoSided] (hIJ : J ≤ I) (hJK : K ≤ J) :
    (I.map (mk J)).comap (factor hJK) = I.map (mk K)

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

Tactic:
simpa only [← eq] using mem_map_of_mem (mk J) hr

Result:
no goals

Proof state:
case h.refine_1.intro.intro.intro.intro
R : Type u_1
inst✝² : Ring R
I J K : Ideal R
inst✝¹ : J.IsTwoSided
inst✝ : K.IsTwoSided
hIJ : J ≤ I
hJK : K ≤ J
x : R ⧸ K
h : x ∈ comap (factor hJK) (map (mk J) I)
r : R
hr : r ∈ ↑I
eq : (mk J) r = (factor hJK) x
this : x - (mk K) r ∈ map (mk K) J
s : R
hs : s ∈ ↑J
eq' : (mk K) s = x - (mk K) r
⊢ (mk K) (r + s) ∈ map (mk K) I

Tactic:
exact mem_map_of_mem (mk K) (Submodule.add_mem _ hr (hIJ hs))

Result:
no goals

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

Tactic:
rcases mem_image_of_mem_map_of_surjective (mk J) Quotient.mk_surjective h with ⟨r, hr, eq⟩

Result:
case h.refine_1.intro.intro
R : Type u_1
inst✝² : Ring R
I J K : Ideal R
inst✝¹ : J.IsTwoSided
inst✝ : K.IsTwoSided
hIJ : J ≤ I
hJK : K ≤ J
x : R ⧸ K
h : x ∈ comap (factor hJK) (map (mk J) I)
r : R
hr : r ∈ ↑I
eq : (mk J) r = (factor hJK) x
⊢ x ∈ map (mk K) I

Proof state:
case h.refine_1.intro.intro.intro.intro
R : Type u_1
inst✝² : Ring R
I J K : Ideal R
inst✝¹ : J.IsTwoSided
inst✝ : K.IsTwoSided
hIJ : J ≤ I
hJK : K ≤ J
x : R ⧸ K
h : x ∈ comap (factor hJK) (map (mk J) I)
r : R
hr : r ∈ ↑I
eq : (mk J) r = (factor hJK) x
this : x - (mk K) r ∈ map (mk K) J
s : R
hs : s ∈ ↑J
eq' : (mk K) s = x - (mk K) r
⊢ x ∈ map (mk K) I

Tactic:
rw [← add_sub_cancel ((mk K) r) x, ← eq', ← map_add]

Result:
case h.refine_1.intro.intro.intro.intro
R : Type u_1
inst✝² : Ring R
I J K : Ideal R
inst✝¹ : J.IsTwoSided
inst✝ : K.IsTwoSided
hIJ : J ≤ I
hJK : K ≤ J
x : R ⧸ K
h : x ∈ comap (factor hJK) (map (mk J) I)
r : R
hr : r ∈ ↑I
eq : (mk J) r = (factor hJK) x
this : x - (mk K) r ∈ map (mk K) J
s : R
hs : s ∈ ↑J
eq' : (mk K) s = x - (mk K) r
⊢ (mk K) (r + s) ∈ map (mk K) I

Proof state:
R : Type u_1
inst✝² : Ring R
I J K : Ideal R
inst✝¹ : J.IsTwoSided
inst✝ : K.IsTwoSided
hIJ : J ≤ I
hJK : K ≤ J
⊢ comap (factor hJK) (map (mk J) I) = map (mk K) I

Tactic:
ext x

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

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

Tactic:
rcases mem_image_of_mem_map_of_surjective (mk K) Quotient.mk_surjective h with ⟨r, hr, eq⟩

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

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

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

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

case h.refine_2
R : Type u_1
inst✝² : Ring R
I J K : Ideal R
inst✝¹ : J.IsTwoSided
inst✝ : K.IsTwoSided
hIJ : J ≤ I
hJK : K ≤ J
x : R ⧸ K
h : x ∈ map (mk K) I
⊢ x ∈ comap (factor hJK) (map (mk J) I)

Proof state:
case h.refine_1.intro.intro
R : Type u_1
inst✝² : Ring R
I J K : Ideal R
inst✝¹ : J.IsTwoSided
inst✝ : K.IsTwoSided
hIJ : J ≤ I
hJK : K ≤ J
x : R ⧸ K
h : x ∈ comap (factor hJK) (map (mk J) I)
r : R
hr : r ∈ ↑I
eq : (mk J) r = (factor hJK) x
this : x - (mk K) r ∈ map (mk K) J
⊢ x ∈ map (mk K) I

Tactic:
rcases mem_image_of_mem_map_of_surjective (mk K) Quotient.mk_surjective this with ⟨s, hs, eq'⟩

Result:
case h.refine_1.intro.intro.intro.intro
R : Type u_1
inst✝² : Ring R
I J K : Ideal R
inst✝¹ : J.IsTwoSided
inst✝ : K.IsTwoSided
hIJ : J ≤ I
hJK : K ≤ J
x : R ⧸ K
h : x ∈ comap (factor hJK) (map (mk J) I)
r : R
hr : r ∈ ↑I
eq : (mk J) r = (factor hJK) x
this : x - (mk K) r ∈ map (mk K) J
s : R
hs : s ∈ ↑J
eq' : (mk K) s = x - (mk K) r
⊢ x ∈ map (mk K) I

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

Tactic:
have : x - ((mk K) r) ∈ J.map (mk K) := by
  simp [← factor_ker hJK, ← eq]

Result:
case h.refine_1.intro.intro
R : Type u_1
inst✝² : Ring R
I J K : Ideal R
inst✝¹ : J.IsTwoSided
inst✝ : K.IsTwoSided
hIJ : J ≤ I
hJK : K ≤ J
x : R ⧸ K
h : x ∈ comap (factor hJK) (map (mk J) I)
r : R
hr : r ∈ ↑I
eq : (mk J) r = (factor hJK) x
this : x - (mk K) r ∈ map (mk K) J
⊢ x ∈ map (mk K) I

Proof state:
R : Type u_1
inst✝² : Ring R
I J K : Ideal R
inst✝¹ : J.IsTwoSided
inst✝ : K.IsTwoSided
hIJ : J ≤ I
hJK : K ≤ J
x : R ⧸ K
h : x ∈ comap (factor hJK) (map (mk J) I)
r : R
hr : r ∈ ↑I
eq : (mk J) r = (factor hJK) x
⊢ x - (mk K) r ∈ map (mk K) J

Tactic:
simp [← factor_ker hJK, ← eq]

Result:
no goals