no goals
C : Type u_3
D : Type u_6
inst✝³ : Category C
inst✝² : Category D
L : C ⥤ D
W : MorphismProperty C
E : Type u_4
inst✝¹ : Category E
inst✝ : Functor.IsLocalization L W
F₁ F₂ F₃ : C ⥤ E
F₁' F₂' F₃' : D ⥤ E
h₁ : Lifting L W F₁ F₁'
h₂ : Lifting L W F₂ F₂'
h₃ : Lifting L W F₃ F₃'
τ : F₁ ⟶ F₂
τ' : F₂ ⟶ F₃
X : C
⊢ (liftNatTrans L W F₁ F₂ F₁' F₂' τ ≫ liftNatTrans L W F₂ F₃ F₂' F₃' τ').app (L.obj X) =
    (liftNatTrans L W F₁ F₃ F₁' F₃' (τ ≫ τ')).app (L.obj X)
simp only [NatTrans.comp_app, liftNatTrans_app, assoc, Iso.inv_hom_id_app_assoc]