-- 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₂
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)))

Tactic:
simp only [Functor.map_comp, assoc, comp_id, id_comp]

Result:
no goals

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₃
⊢ Ψ.homMap L₂ L₃ (Φ.homMap L₁ L₂ f) = (Φ.comp Ψ).homMap L₁ L₃ f

Tactic:
let e : Φ.functor ⋙ L₂ ≅ L₁ ⋙ G := CatCommSq.iso _ _ _ _

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
⊢ Ψ.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
⊢ Ψ.homMap L₂ L₃ (Φ.homMap L₁ L₂ f) = (Φ.comp Ψ).homMap L₁ L₃ f

Tactic:
let e' : Ψ.functor ⋙ L₃ ≅ L₂ ⋙ G' := CatCommSq.iso _ _ _ _

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'
⊢ Ψ.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
⊢ Ψ.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₂
⊢ Ψ.homMap L₂ L₃ (Φ.homMap L₁ L₂ f) = (Φ.comp Ψ).homMap L₁ L₃ f