-- Mathlib/CategoryTheory/Localization/HomEquiv.lean
@[simp]
lemma homMap_homMap (f : L₁.obj X ⟶ L₁.obj Y) :
    Ψ.homMap L₂ L₃ (Φ.homMap L₁ L₂ f) = (Φ.comp Ψ).homMap L₁ L₃ f

Proof state:
C₁ : Type u_2
C₂ : Type u_3
C₃ : Type u_4
D₁ : Type u_5
D₂ : Type u_6
D₃ : Type u_7
inst✝⁸ : Category.{u_9, u_2} C₁
inst✝⁷ : Category.{u_12, u_3} C₂
inst✝⁶ : Category.{u_11, u_4} C₃
inst✝⁵ : Category.{u_8, u_5} D₁
inst✝⁴ : Category.{u_13, u_6} D₂
inst✝³ : Category.{u_10, u_7} D₃
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
W₃ : MorphismProperty C₃
Φ : LocalizerMorphism W₁ W₂
Ψ : LocalizerMorphism W₂ W₃
L₁ : C₁ ⥤ D₁
inst✝² : L₁.IsLocalization W₁
L₂ : C₂ ⥤ D₂
inst✝¹ : L₂.IsLocalization W₂
L₃ : C₃ ⥤ D₃
inst✝ : L₃.IsLocalization W₃
X Y : C₁
f : L₁.obj X ⟶ L₁.obj Y
G : D₁ ⥤ D₂ := Φ.localizedFunctor L₁ L₂
⊢ Ψ.homMap L₂ L₃ (Φ.homMap L₁ L₂ f) = (Φ.comp Ψ).homMap L₁ L₃ f

Tactic:
let G' := Ψ.localizedFunctor L₂ L₃

Result:
C₁ : Type u_2
C₂ : Type u_3
C₃ : Type u_4
D₁ : Type u_5
D₂ : Type u_6
D₃ : Type u_7
inst✝⁸ : Category.{u_9, u_2} C₁
inst✝⁷ : Category.{u_12, u_3} C₂
inst✝⁶ : Category.{u_11, u_4} C₃
inst✝⁵ : Category.{u_8, u_5} D₁
inst✝⁴ : Category.{u_13, u_6} D₂
inst✝³ : Category.{u_10, u_7} D₃
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
W₃ : MorphismProperty C₃
Φ : LocalizerMorphism W₁ W₂
Ψ : LocalizerMorphism W₂ W₃
L₁ : C₁ ⥤ D₁
inst✝² : L₁.IsLocalization W₁
L₂ : C₂ ⥤ D₂
inst✝¹ : L₂.IsLocalization W₂
L₃ : C₃ ⥤ D₃
inst✝ : L₃.IsLocalization W₃
X Y : C₁
f : L₁.obj X ⟶ L₁.obj Y
G : D₁ ⥤ D₂ := Φ.localizedFunctor L₁ L₂
G' : D₂ ⥤ D₃ := Ψ.localizedFunctor L₂ L₃
⊢ Ψ.homMap L₂ L₃ (Φ.homMap L₁ L₂ f) = (Φ.comp Ψ).homMap L₁ L₃ f

Proof state:
C₁ : Type u_2
C₂ : Type u_3
C₃ : Type u_4
D₁ : Type u_5
D₂ : Type u_6
D₃ : Type u_7
inst✝⁸ : Category.{u_9, u_2} C₁
inst✝⁷ : Category.{u_12, u_3} C₂
inst✝⁶ : Category.{u_11, u_4} C₃
inst✝⁵ : Category.{u_8, u_5} D₁
inst✝⁴ : Category.{u_13, u_6} D₂
inst✝³ : Category.{u_10, u_7} D₃
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
W₃ : MorphismProperty C₃
Φ : LocalizerMorphism W₁ W₂
Ψ : LocalizerMorphism W₂ W₃
L₁ : C₁ ⥤ D₁
inst✝² : L₁.IsLocalization W₁
L₂ : C₂ ⥤ D₂
inst✝¹ : L₂.IsLocalization W₂
L₃ : C₃ ⥤ D₃
inst✝ : L₃.IsLocalization W₃
X Y : C₁
f : L₁.obj X ⟶ L₁.obj Y
G : D₁ ⥤ D₂ := Φ.localizedFunctor L₁ L₂
G' : D₂ ⥤ D₃ := Ψ.localizedFunctor L₂ L₃
e : Φ.functor ⋙ L₂ ≅ L₁ ⋙ G := CatCommSq.iso Φ.functor L₁ L₂ G
e' : Ψ.functor ⋙ L₃ ≅ L₂ ⋙ G' := CatCommSq.iso Ψ.functor L₂ L₃ G'
⊢ Ψ.homMap L₂ L₃ (Φ.homMap L₁ L₂ f) = (Φ.comp Ψ).homMap L₁ L₃ f

Tactic:
rw [Φ.homMap_apply L₁ L₂ G e, Ψ.homMap_apply L₂ L₃ G' e',
  (Φ.comp Ψ).homMap_apply L₁ L₃ (G ⋙ G')
    (Functor.associator _ _ _ ≪≫ isoWhiskerLeft _ e' ≪≫
    (Functor.associator _ _ _).symm ≪≫ isoWhiskerRight e _ ≪≫
    Functor.associator _ _ _)]

Result:
C₁ : Type u_2
C₂ : Type u_3
C₃ : Type u_4
D₁ : Type u_5
D₂ : Type u_6
D₃ : Type u_7
inst✝⁸ : Category.{u_9, u_2} C₁
inst✝⁷ : Category.{u_12, u_3} C₂
inst✝⁶ : Category.{u_11, u_4} C₃
inst✝⁵ : Category.{u_8, u_5} D₁
inst✝⁴ : Category.{u_13, u_6} D₂
inst✝³ : Category.{u_10, u_7} D₃
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
W₃ : MorphismProperty C₃
Φ : LocalizerMorphism W₁ W₂
Ψ : LocalizerMorphism W₂ W₃
L₁ : C₁ ⥤ D₁
inst✝² : L₁.IsLocalization W₁
L₂ : C₂ ⥤ D₂
inst✝¹ : L₂.IsLocalization W₂
L₃ : C₃ ⥤ D₃
inst✝ : L₃.IsLocalization W₃
X Y : C₁
f : L₁.obj X ⟶ L₁.obj Y
G : D₁ ⥤ D₂ := Φ.localizedFunctor L₁ L₂
G' : D₂ ⥤ D₃ := Ψ.localizedFunctor L₂ L₃
e : Φ.functor ⋙ L₂ ≅ L₁ ⋙ G := CatCommSq.iso Φ.functor L₁ L₂ G
e' : Ψ.functor ⋙ L₃ ≅ L₂ ⋙ G' := CatCommSq.iso Ψ.functor L₂ L₃ G'
⊢ e'.hom.app (Φ.functor.obj X) ≫ G'.map (e.hom.app X ≫ G.map f ≫ e.inv.app Y) ≫ e'.inv.app (Φ.functor.obj Y) =
    (Φ.functor.associator Ψ.functor L₃ ≪≫
              isoWhiskerLeft Φ.functor e' ≪≫
                (Φ.functor.associator L₂ G').symm ≪≫ isoWhiskerRight e G' ≪≫ L₁.associator G G').hom.app
        X ≫
      (G ⋙ G').map f ≫
        (Φ.functor.associator Ψ.functor L₃ ≪≫
                isoWhiskerLeft Φ.functor e' ≪≫
                  (Φ.functor.associator L₂ G').symm ≪≫ isoWhiskerRight e G' ≪≫ L₁.associator G G').inv.app
          Y

Proof state:
C₁ : Type u_2
C₂ : Type u_3
C₃ : Type u_4
D₁ : Type u_5
D₂ : Type u_6
D₃ : Type u_7
inst✝⁸ : Category.{u_9, u_2} C₁
inst✝⁷ : Category.{u_12, u_3} C₂
inst✝⁶ : Category.{u_11, u_4} C₃
inst✝⁵ : Category.{u_8, u_5} D₁
inst✝⁴ : Category.{u_13, u_6} D₂
inst✝³ : Category.{u_10, u_7} D₃
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
W₃ : MorphismProperty C₃
Φ : LocalizerMorphism W₁ W₂
Ψ : LocalizerMorphism W₂ W₃
L₁ : C₁ ⥤ D₁
inst✝² : L₁.IsLocalization W₁
L₂ : C₂ ⥤ D₂
inst✝¹ : L₂.IsLocalization W₂
L₃ : C₃ ⥤ D₃
inst✝ : L₃.IsLocalization W₃
X Y : C₁
f : L₁.obj X ⟶ L₁.obj Y
G : D₁ ⥤ D₂ := Φ.localizedFunctor L₁ L₂
G' : D₂ ⥤ D₃ := Ψ.localizedFunctor L₂ L₃
e : Φ.functor ⋙ L₂ ≅ L₁ ⋙ G := CatCommSq.iso Φ.functor L₁ L₂ G
e' : Ψ.functor ⋙ L₃ ≅ L₂ ⋙ G' := CatCommSq.iso Ψ.functor L₂ L₃ G'
⊢ e'.hom.app (Φ.functor.obj X) ≫ G'.map (e.hom.app X ≫ G.map f ≫ e.inv.app Y) ≫ e'.inv.app (Φ.functor.obj Y) =
    (Φ.functor.associator Ψ.functor L₃ ≪≫
              isoWhiskerLeft Φ.functor e' ≪≫
                (Φ.functor.associator L₂ G').symm ≪≫ isoWhiskerRight e G' ≪≫ L₁.associator G G').hom.app
        X ≫
      (G ⋙ G').map f ≫
        (Φ.functor.associator Ψ.functor L₃ ≪≫
                isoWhiskerLeft Φ.functor e' ≪≫
                  (Φ.functor.associator L₂ G').symm ≪≫ isoWhiskerRight e G' ≪≫ L₁.associator G G').inv.app
          Y

Tactic:
dsimp

Result:
C₁ : Type u_2
C₂ : Type u_3
C₃ : Type u_4
D₁ : Type u_5
D₂ : Type u_6
D₃ : Type u_7
inst✝⁸ : Category.{u_9, u_2} C₁
inst✝⁷ : Category.{u_12, u_3} C₂
inst✝⁶ : Category.{u_11, u_4} C₃
inst✝⁵ : Category.{u_8, u_5} D₁
inst✝⁴ : Category.{u_13, u_6} D₂
inst✝³ : Category.{u_10, u_7} D₃
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
W₃ : MorphismProperty C₃
Φ : LocalizerMorphism W₁ W₂
Ψ : LocalizerMorphism W₂ W₃
L₁ : C₁ ⥤ D₁
inst✝² : L₁.IsLocalization W₁
L₂ : C₂ ⥤ D₂
inst✝¹ : L₂.IsLocalization W₂
L₃ : C₃ ⥤ D₃
inst✝ : L₃.IsLocalization W₃
X Y : C₁
f : L₁.obj X ⟶ L₁.obj Y
G : D₁ ⥤ D₂ := Φ.localizedFunctor L₁ L₂
G' : D₂ ⥤ D₃ := Ψ.localizedFunctor L₂ L₃
e : Φ.functor ⋙ L₂ ≅ L₁ ⋙ G := CatCommSq.iso Φ.functor L₁ L₂ G
e' : Ψ.functor ⋙ L₃ ≅ L₂ ⋙ G' := CatCommSq.iso Ψ.functor L₂ L₃ G'
⊢ e'.hom.app (Φ.functor.obj X) ≫ G'.map (e.hom.app X ≫ G.map f ≫ e.inv.app Y) ≫ e'.inv.app (Φ.functor.obj Y) =
    (𝟙 (L₃.obj (Ψ.functor.obj (Φ.functor.obj X))) ≫
        e'.hom.app (Φ.functor.obj X) ≫
          𝟙 (G'.obj (L₂.obj (Φ.functor.obj X))) ≫ G'.map (e.hom.app X) ≫ 𝟙 (G'.obj (G.obj (L₁.obj X)))) ≫
      G'.map (G.map f) ≫
        (((𝟙 (G'.obj (G.obj (L₁.obj Y))) ≫ G'.map (e.inv.app Y)) ≫ 𝟙 (G'.obj (L₂.obj (Φ.functor.obj Y)))) ≫
            e'.inv.app (Φ.functor.obj Y)) ≫
          𝟙 (L₃.obj (Ψ.functor.obj (Φ.functor.obj Y)))