-- Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.Basic
Goal:
C₁ : Type u₁
C₂ : Type u₂
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
Φ : LocalizerMorphism W₁ W₂
D₁ : Type u_1
D₂ : Type u_2
inst_2 : Category.{v_1, u_1} D₁
inst_3 : Category.{v_2, u_2} D₂
L₁ : Functor.{v₁, v_1, u₁, u_1} C₁ D₁
L₂ : Functor.{v₂, v_2, u₂, u_2} C₂ D₂
inst_4 : L₁.IsLocalization W₁
inst_5 : L₂.IsLocalization W₂
F : Functor.{v_1, v_2, u_1, u_2} D₁ D₂
inst_6 : Φ.HasRightResolutions (W₁ := W₁) (W₂ := W₂)
e : Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L₂ ≅ L₁ ⋙ F
this :
  Φ.IsRightDerivabilityStructure (W₁ := W₁) (W₂ := W₂) ↔
    TwoSquare.GuitartExact (B := Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q)
      (Iso.hom
        (CatCommSq.iso (Φ.functor (W₁ := W₁) (W₂ := W₂)) W₁.Q W₂.Q
          (Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q)))
e' : Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ W₂.Q ≅ W₁.Q ⋙ Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q :=
  CatCommSq.iso (Φ.functor (W₁ := W₁) (W₂ := W₂)) W₁.Q W₂.Q (Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q)
E₁ : W₁.Localization ≌ D₁ := uniq W₁.Q L₁ W₁
E₂ : W₂.Localization ≌ D₂ := uniq W₂.Q L₂ W₂
e₁ : W₁.Q ⋙ E₁.functor ≅ L₁ := compUniqFunctor W₁.Q L₁ W₁
e₂ : W₂.Q ⋙ E₂.functor ≅ L₂ := compUniqFunctor W₂.Q L₂ W₂
e'' : (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ W₂.Q) ⋙ E₂.functor ≅ (W₁.Q ⋙ E₁.functor) ⋙ F :=
  Φ.functor (W₁ := W₁) (W₂ := W₂).associator W₂.Q E₂.functor ≪≫
    Φ.functor (W₁ := W₁) (W₂ := W₂).isoWhiskerLeft e₂ ≪≫ e ≪≫ isoWhiskerRight e₁.symm F
e''' : Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q ⋙ E₂.functor ≅ E₁.functor ⋙ F :=
  liftNatIso W₁.Q W₁ ((Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ W₂.Q) ⋙ E₂.functor) ((W₁.Q ⋙ E₁.functor) ⋙ F)
    (Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q ⋙ E₂.functor) (E₁.functor ⋙ F) e''
X₁ : C₁
h :
  e₂.inv.app (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X₁) ≫
      E₂.functor.map ((TwoSquare.natTrans e'.hom).app X₁) ≫
        NatTrans.app
            (Iso.hom
              (Lifting.iso W₁.Q W₁ ((Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ W₂.Q) ⋙ E₂.functor)
                (Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q ⋙ E₂.functor)))
            X₁ ≫
          e₂.hom.app (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X₁) ≫
            e.hom.app X₁ ≫
              F.map (e₁.inv.app X₁) ≫
                NatTrans.app (Iso.inv (Lifting.iso W₁.Q W₁ ((W₁.Q ⋙ E₁.functor) ⋙ F) (E₁.functor ⋙ F))) X₁ ≫
                  F.map (e₁.hom.app X₁) =
    (TwoSquare.natTrans e.hom).app X₁
⊢ e₂.inv.app (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X₁) ≫
      E₂.functor.map ((TwoSquare.natTrans e'.hom).app X₁) ≫
        (NatTrans.app
              (Iso.hom
                (Lifting.iso W₁.Q W₁ ((Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ W₂.Q) ⋙ E₂.functor)
                  (Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q ⋙ E₂.functor)))
              X₁ ≫
            e''.hom.app X₁ ≫
              NatTrans.app (Iso.inv (Lifting.iso W₁.Q W₁ ((W₁.Q ⋙ E₁.functor) ⋙ F) (E₁.functor ⋙ F))) X₁) ≫
          F.map (e₁.hom.app X₁) =
    (TwoSquare.natTrans e.hom).app X₁

Tactic:
simp only [Functor.comp_obj, Iso.trans_hom, isoWhiskerLeft_hom, isoWhiskerRight_hom,
      Iso.symm_hom, NatTrans.comp_app, Functor.associator_hom_app, whiskerLeft_app,
      whiskerRight_app, id_comp, assoc, e'']

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Category.assoc, CategoryTheory.Functor.associator_hom_app, CategoryTheory.Iso.symm_hom, CategoryTheory.Functor.whiskerLeft_app, CategoryTheory.Functor.isoWhiskerRight_hom, CategoryTheory.Iso.trans_hom, CategoryTheory.Functor.whiskerRight_app, CategoryTheory.NatTrans.comp_app, CategoryTheory.Functor.isoWhiskerLeft_hom, CategoryTheory.Category.id_comp