Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.Basic

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
inst✝⁶ : Category.{v₁, u₁} C₁
inst✝⁵ : Category.{v₂, u₂} C₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
D₁ : Type u_1
D₂ : Type u_2
inst✝⁴ : Category.{v_1, u_1} D₁
inst✝³ : Category.{v_2, u_2} D₂
L₁ : C₁ ⥤ D₁
L₂ : C₂ ⥤ D₂
inst✝² : L₁.IsLocalization W₁
inst✝¹ : L₂.IsLocalization W₂
F : D₁ ⥤ D₂
inst✝ : Φ.HasRightResolutions
e : Φ.functor ⋙ L₂ ≅ L₁ ⋙ F
this :
  Φ.IsRightDerivabilityStructure ↔
    TwoSquare.GuitartExact (CatCommSq.iso Φ.functor W₁.Q W₂.Q (Φ.localizedFunctor W₁.Q W₂.Q)).hom
e' : Φ.functor ⋙ W₂.Q ≅ W₁.Q ⋙ Φ.localizedFunctor W₁.Q W₂.Q :=
  CatCommSq.iso Φ.functor W₁.Q W₂.Q (Φ.localizedFunctor 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₂.Q) ⋙ E₂.functor ≅ (W₁.Q ⋙ E₁.functor) ⋙ F :=
  Φ.functor.associator W₂.Q E₂.functor ≪≫ Φ.functor.isoWhiskerLeft e₂ ≪≫ e ≪≫ isoWhiskerRight e₁.symm F
e''' : Φ.localizedFunctor W₁.Q W₂.Q ⋙ E₂.functor ≅ E₁.functor ⋙ F :=
  liftNatIso W₁.Q W₁ ((Φ.functor ⋙ W₂.Q) ⋙ E₂.functor) ((W₁.Q ⋙ E₁.functor) ⋙ F)
    (Φ.localizedFunctor W₁.Q W₂.Q ⋙ E₂.functor) (E₁.functor ⋙ F) e''
X₁ : C₁
⊢ e₂.inv.app (Φ.functor.obj X₁) ≫
      E₂.functor.map ((TwoSquare.natTrans e'.hom).app X₁ ≫ (liftingLocalizedFunctor._aux_1 Φ W₁.Q W₂.Q).hom.app X₁) ≫
        e₂.hom.app (Φ.functor.obj X₁) ≫ e.hom.app X₁ =
    (TwoSquare.natTrans e.hom).app X₁

Tactic:
erw [show (CatCommSq.iso Φ.functor W₁.Q W₂.Q (localizedFunctor Φ W₁.Q W₂.Q)).hom =
      (Lifting.iso W₁.Q W₁ _ _).inv by rfl, Iso.inv_hom_id_app]

Goal state after:
C₁ : Type u₁
C₂ : Type u₂
inst✝⁶ : Category.{v₁, u₁} C₁
inst✝⁵ : Category.{v₂, u₂} C₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
D₁ : Type u_1
D₂ : Type u_2
inst✝⁴ : Category.{v_1, u_1} D₁
inst✝³ : Category.{v_2, u_2} D₂
L₁ : C₁ ⥤ D₁
L₂ : C₂ ⥤ D₂
inst✝² : L₁.IsLocalization W₁
inst✝¹ : L₂.IsLocalization W₂
F : D₁ ⥤ D₂
inst✝ : Φ.HasRightResolutions
e : Φ.functor ⋙ L₂ ≅ L₁ ⋙ F
this :
  Φ.IsRightDerivabilityStructure ↔
    TwoSquare.GuitartExact (CatCommSq.iso Φ.functor W₁.Q W₂.Q (Φ.localizedFunctor W₁.Q W₂.Q)).hom
e' : Φ.functor ⋙ W₂.Q ≅ W₁.Q ⋙ Φ.localizedFunctor W₁.Q W₂.Q :=
  CatCommSq.iso Φ.functor W₁.Q W₂.Q (Φ.localizedFunctor 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₂.Q) ⋙ E₂.functor ≅ (W₁.Q ⋙ E₁.functor) ⋙ F :=
  Φ.functor.associator W₂.Q E₂.functor ≪≫ Φ.functor.isoWhiskerLeft e₂ ≪≫ e ≪≫ isoWhiskerRight e₁.symm F
e''' : Φ.localizedFunctor W₁.Q W₂.Q ⋙ E₂.functor ≅ E₁.functor ⋙ F :=
  liftNatIso W₁.Q W₁ ((Φ.functor ⋙ W₂.Q) ⋙ E₂.functor) ((W₁.Q ⋙ E₁.functor) ⋙ F)
    (Φ.localizedFunctor W₁.Q W₂.Q ⋙ E₂.functor) (E₁.functor ⋙ F) e''
X₁ : C₁
⊢ e₂.inv.app (Φ.functor.obj X₁) ≫
      E₂.functor.map (𝟙 ((Φ.functor ⋙ W₂.Q).obj X₁)) ≫ e₂.hom.app (Φ.functor.obj X₁) ≫ e.hom.app X₁ =
    (TwoSquare.natTrans e.hom).app X₁