-- Mathlib/CategoryTheory/Localization/HomEquiv.lean
@[reassoc]
lemma homMap_apply (G : D₁ ⥤ D₂) (e : Φ.functor ⋙ L₂ ≅ L₁ ⋙ G) (f : L₁.obj X ⟶ L₁.obj Y) :
    Φ.homMap L₁ L₂ f = e.hom.app X ≫ G.map f ≫ e.inv.app Y

Proof state:
C₁ : Type u_2
C₂ : Type u_3
D₁ : Type u_5
D₂ : Type u_6
inst✝⁵ : Category.{u_10, u_2} C₁
inst✝⁴ : Category.{u_11, u_3} C₂
inst✝³ : Category.{u_8, u_5} D₁
inst✝² : Category.{u_9, u_6} D₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
L₁ : C₁ ⥤ D₁
inst✝¹ : L₁.IsLocalization W₁
L₂ : C₂ ⥤ D₂
inst✝ : L₂.IsLocalization W₂
X Y : C₁
G : D₁ ⥤ D₂
e : Φ.functor ⋙ L₂ ≅ L₁ ⋙ G
f : L₁.obj X ⟶ L₁.obj Y
G' : D₁ ⥤ D₂ := Φ.localizedFunctor L₁ L₂
e' : Φ.functor ⋙ L₂ ≅ L₁ ⋙ G' := CatCommSq.iso Φ.functor L₁ L₂ G'
⊢ e'.hom.app X ≫ G'.map f ≫ e'.inv.app Y = e.hom.app X ≫ G.map f ≫ e.inv.app Y

Tactic:
letI : Localization.Lifting L₁ W₁ (Φ.functor ⋙ L₂) G := ⟨e.symm⟩

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

Proof state:
C₁ : Type u_2
C₂ : Type u_3
D₁ : Type u_5
D₂ : Type u_6
inst✝⁵ : Category.{u_10, u_2} C₁
inst✝⁴ : Category.{u_11, u_3} C₂
inst✝³ : Category.{u_8, u_5} D₁
inst✝² : Category.{u_9, u_6} D₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
L₁ : C₁ ⥤ D₁
inst✝¹ : L₁.IsLocalization W₁
L₂ : C₂ ⥤ D₂
inst✝ : L₂.IsLocalization W₂
X Y : C₁
G : D₁ ⥤ D₂
e : Φ.functor ⋙ L₂ ≅ L₁ ⋙ G
f : L₁.obj X ⟶ L₁.obj Y
G' : D₁ ⥤ D₂ := Φ.localizedFunctor L₁ L₂
e' : Φ.functor ⋙ L₂ ≅ L₁ ⋙ G' := CatCommSq.iso Φ.functor L₁ L₂ G'
this✝ : Localization.Lifting L₁ W₁ (Φ.functor ⋙ L₂) G := { iso' := e.symm }
α : G' ≅ G := Localization.liftNatIso L₁ W₁ (L₁ ⋙ G') (Φ.functor ⋙ L₂) G' G e'.symm
this : e = e' ≪≫ isoWhiskerLeft L₁ α
⊢ e'.hom.app X ≫ G'.map f ≫ e'.inv.app Y = e.hom.app X ≫ G.map f ≫ e.inv.app Y

Tactic:
simp [this]

Result:
no goals

Proof state:
C₁ : Type u_2
C₂ : Type u_3
D₁ : Type u_5
D₂ : Type u_6
inst✝⁵ : Category.{u_10, u_2} C₁
inst✝⁴ : Category.{u_11, u_3} C₂
inst✝³ : Category.{u_8, u_5} D₁
inst✝² : Category.{u_9, u_6} D₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
L₁ : C₁ ⥤ D₁
inst✝¹ : L₁.IsLocalization W₁
L₂ : C₂ ⥤ D₂
inst✝ : L₂.IsLocalization W₂
X Y : C₁
G : D₁ ⥤ D₂
e : Φ.functor ⋙ L₂ ≅ L₁ ⋙ G
f : L₁.obj X ⟶ L₁.obj Y
G' : D₁ ⥤ D₂ := Φ.localizedFunctor L₁ L₂
e' : Φ.functor ⋙ L₂ ≅ L₁ ⋙ G' := CatCommSq.iso Φ.functor L₁ L₂ G'
this : Localization.Lifting L₁ W₁ (Φ.functor ⋙ L₂) G := { iso' := e.symm }
⊢ e'.hom.app X ≫ G'.map f ≫ e'.inv.app Y = e.hom.app X ≫ G.map f ≫ e.inv.app Y

Tactic:
let α : G' ≅ G := Localization.liftNatIso L₁ W₁ (L₁ ⋙ G') (Φ.functor ⋙ L₂) _ _ e'.symm

Result:
C₁ : Type u_2
C₂ : Type u_3
D₁ : Type u_5
D₂ : Type u_6
inst✝⁵ : Category.{u_10, u_2} C₁
inst✝⁴ : Category.{u_11, u_3} C₂
inst✝³ : Category.{u_8, u_5} D₁
inst✝² : Category.{u_9, u_6} D₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
L₁ : C₁ ⥤ D₁
inst✝¹ : L₁.IsLocalization W₁
L₂ : C₂ ⥤ D₂
inst✝ : L₂.IsLocalization W₂
X Y : C₁
G : D₁ ⥤ D₂
e : Φ.functor ⋙ L₂ ≅ L₁ ⋙ G
f : L₁.obj X ⟶ L₁.obj Y
G' : D₁ ⥤ D₂ := Φ.localizedFunctor L₁ L₂
e' : Φ.functor ⋙ L₂ ≅ L₁ ⋙ G' := CatCommSq.iso Φ.functor L₁ L₂ G'
this : Localization.Lifting L₁ W₁ (Φ.functor ⋙ L₂) G := { iso' := e.symm }
α : G' ≅ G := Localization.liftNatIso L₁ W₁ (L₁ ⋙ G') (Φ.functor ⋙ L₂) G' G e'.symm
⊢ e'.hom.app X ≫ G'.map f ≫ e'.inv.app Y = e.hom.app X ≫ G.map f ≫ e.inv.app Y