-- Mathlib/RingTheory/Ideal/Quotient/Operations.lean
theorem comp_quotientMap_eq_of_comp_eq {R' S' : Type*} [Ring R'] [Ring S'] {f : R →+* S}
    {f' : R' →+* S'} {g : R →+* R'} {g' : S →+* S'} (hfg : f'.comp g = g'.comp f)
    (I : Ideal S') [I.IsTwoSided] :
    -- Porting note: was losing track of I
    let leq := le_of_eq (_root_.trans (comap_comap (I := I) f g') (hfg ▸ comap_comap (I := I) g f'))
    (quotientMap I g' le_rfl).comp (quotientMap (I.comap g') f le_rfl) =
    (quotientMap I f' le_rfl).comp (quotientMap (I.comap f') g leq)

Proof state:
case intro
R : Type u
inst✝⁴ : Ring R
S : Type v
inst✝³ : Ring S
R' : Type u_5
S' : Type u_6
inst✝² : Ring R'
inst✝¹ : Ring S'
f : R →+* S
f' : R' →+* S'
g : R →+* R'
g' : S →+* S'
hfg : f'.comp g = g'.comp f
I : Ideal S'
inst✝ : I.IsTwoSided
r : R
⊢ (Quotient.mk I) (g' (f r)) = (Quotient.mk I) (f' (g r))

Tactic:
exact (Ideal.Quotient.mk I).congr_arg (_root_.trans (g'.comp_apply f r).symm
  (hfg ▸ f'.comp_apply g r))

Result:
no goals

Proof state:
R : Type u
inst✝⁴ : Ring R
S : Type v
inst✝³ : Ring S
R' : Type u_5
S' : Type u_6
inst✝² : Ring R'
inst✝¹ : Ring S'
f : R →+* S
f' : R' →+* S'
g : R →+* R'
g' : S →+* S'
hfg : f'.comp g = g'.comp f
I : Ideal S'
inst✝ : I.IsTwoSided
a : R ⧸ comap f (comap g' I)
⊢ ((quotientMap I g' ⋯).comp (quotientMap (comap g' I) f ⋯)) a =
    ((quotientMap I f' ⋯).comp (quotientMap (comap f' I) g ⋯)) a

Tactic:
obtain ⟨r, rfl⟩ := Quotient.mk_surjective a

Result:
case intro
R : Type u
inst✝⁴ : Ring R
S : Type v
inst✝³ : Ring S
R' : Type u_5
S' : Type u_6
inst✝² : Ring R'
inst✝¹ : Ring S'
f : R →+* S
f' : R' →+* S'
g : R →+* R'
g' : S →+* S'
hfg : f'.comp g = g'.comp f
I : Ideal S'
inst✝ : I.IsTwoSided
r : R
⊢ ((quotientMap I g' ⋯).comp (quotientMap (comap g' I) f ⋯)) ((Quotient.mk (comap f (comap g' I))) r) =
    ((quotientMap I f' ⋯).comp (quotientMap (comap f' I) g ⋯)) ((Quotient.mk (comap f (comap g' I))) r)

Proof state:
case intro
R : Type u
inst✝⁴ : Ring R
S : Type v
inst✝³ : Ring S
R' : Type u_5
S' : Type u_6
inst✝² : Ring R'
inst✝¹ : Ring S'
f : R →+* S
f' : R' →+* S'
g : R →+* R'
g' : S →+* S'
hfg : f'.comp g = g'.comp f
I : Ideal S'
inst✝ : I.IsTwoSided
r : R
⊢ ((quotientMap I g' ⋯).comp (quotientMap (comap g' I) f ⋯)) ((Quotient.mk (comap f (comap g' I))) r) =
    ((quotientMap I f' ⋯).comp (quotientMap (comap f' I) g ⋯)) ((Quotient.mk (comap f (comap g' I))) r)

Tactic:
simp only [RingHom.comp_apply, quotientMap_mk]

Result:
case intro
R : Type u
inst✝⁴ : Ring R
S : Type v
inst✝³ : Ring S
R' : Type u_5
S' : Type u_6
inst✝² : Ring R'
inst✝¹ : Ring S'
f : R →+* S
f' : R' →+* S'
g : R →+* R'
g' : S →+* S'
hfg : f'.comp g = g'.comp f
I : Ideal S'
inst✝ : I.IsTwoSided
r : R
⊢ (Quotient.mk I) (g' (f r)) = (Quotient.mk I) (f' (g r))

Proof state:
R : Type u
inst✝⁴ : Ring R
S : Type v
inst✝³ : Ring S
R' : Type u_5
S' : Type u_6
inst✝² : Ring R'
inst✝¹ : Ring S'
f : R →+* S
f' : R' →+* S'
g : R →+* R'
g' : S →+* S'
hfg : f'.comp g = g'.comp f
I : Ideal S'
inst✝ : I.IsTwoSided
⊢ let leq := ⋯;
  (quotientMap I g' ⋯).comp (quotientMap (comap g' I) f ⋯) = (quotientMap I f' ⋯).comp (quotientMap (comap f' I) g leq)

Tactic:
refine RingHom.ext fun a => ?_

Result:
R : Type u
inst✝⁴ : Ring R
S : Type v
inst✝³ : Ring S
R' : Type u_5
S' : Type u_6
inst✝² : Ring R'
inst✝¹ : Ring S'
f : R →+* S
f' : R' →+* S'
g : R →+* R'
g' : S →+* S'
hfg : f'.comp g = g'.comp f
I : Ideal S'
inst✝ : I.IsTwoSided
a : R ⧸ comap f (comap g' I)
⊢ ((quotientMap I g' ⋯).comp (quotientMap (comap g' I) f ⋯)) a =
    ((quotientMap I f' ⋯).comp (quotientMap (comap f' I) g ⋯)) a