awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Localization.Construction
Goal:
C : Type uC
inst : Category.{uC', uC} C
W : MorphismProperty.{uC', uC} C
D : Type uD
inst_1 : Category.{uD', uD} D
G : Functor.{uC', uD', uC, uD} C D
hG : W.IsInvertedBy G
G₁ : Functor.{uC', uD', uC, uD} C D
hG₁ : W.IsInvertedBy G₁
G₂ : Functor.{uC', uD', uC, uD} C D
hG₂ : W.IsInvertedBy G₂
f :
  Quiver.Hom (V := MorphismProperty.FunctorsInverting.{uC', uC, uD', uD} W D)
    (ObjectProperty.FullSubcategory.mk (P := fun (F : Functor.{uC', uD', uC, uD} C D) ↦ W.IsInvertedBy F) G₁ hG₁)
    (ObjectProperty.FullSubcategory.mk (P := fun (F : Functor.{uC', uD', uC, uD} C D) ↦ W.IsInvertedBy F) G₂ hG₂)
refine_2 :
  ∀ (x : C),
    Eq (α :=
      (obj (inverse W D ⋙ functor W D)
                  (ObjectProperty.FullSubcategory.mk (P := fun (F : Functor.{uC', uD', uC, uD} C D) ↦ W.IsInvertedBy F)
                    G₁ hG₁)).obj
              (P := fun (F : Functor.{uC', uD', uC, uD} C D) ↦ W.IsInvertedBy F).obj
          x ⟶
        (obj (inverse W D ⋙ functor W D)
                  (ObjectProperty.FullSubcategory.mk (P := fun (F : Functor.{uC', uD', uC, uD} C D) ↦ W.IsInvertedBy F)
                    G₂ hG₂)).obj
              (P := fun (F : Functor.{uC', uD', uC, uD} C D) ↦ W.IsInvertedBy F).obj
          x)
      (NatTrans.app (InducedCategory.Hom.hom (map (inverse W D ⋙ functor W D) f)) x)
      (NatTrans.app
        (InducedCategory.Hom.hom
          (CategoryStruct.comp (Y :=
            obj (𝟭 (MorphismProperty.FunctorsInverting.{uC', uC, uD', uD} W D))
              (ObjectProperty.FullSubcategory.mk (P := fun (F : Functor.{uC', uD', uC, uD} C D) ↦ W.IsInvertedBy F) G₁
                hG₁))
            (eqToHom ⋯) (map (𝟭 (MorphismProperty.FunctorsInverting.{uC', uC, uD', uD} W D)) f ≫ eqToHom ⋯)))
        x)
⊢ Eq (α :=
    obj (inverse W D ⋙ functor W D)
        (ObjectProperty.FullSubcategory.mk (P := fun (F : Functor.{uC', uD', uC, uD} C D) ↦ W.IsInvertedBy F) G₁ hG₁) ⟶
      obj (inverse W D ⋙ functor W D)
        (ObjectProperty.FullSubcategory.mk (P := fun (F : Functor.{uC', uD', uC, uD} C D) ↦ W.IsInvertedBy F) G₂ hG₂))
    (map (inverse W D ⋙ functor W D) f)
    (CategoryStruct.comp (Y :=
      obj (𝟭 (MorphismProperty.FunctorsInverting.{uC', uC, uD', uD} W D))
        (ObjectProperty.FullSubcategory.mk (P := fun (F : Functor.{uC', uD', uC, uD} C D) ↦ W.IsInvertedBy F) G₁ hG₁))
      (eqToHom ⋯) (map (𝟭 (MorphismProperty.FunctorsInverting.{uC', uC, uD', uD} W D)) f ≫ eqToHom ⋯))

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Localization.Construction
Goal:
C : Type uC
inst : Category.{uC', uC} C
W : MorphismProperty.{uC', uC} C
D : Type uD
inst_1 : Category.{uD', uD} D
G : Functor.{uC', uD', uC, uD} C D
hG : W.IsInvertedBy G
G₁ : Functor.{uC', uD', uC, uD} C D
hG₁ : W.IsInvertedBy G₁
G₂ : Functor.{uC', uD', uC, uD} C D
hG₂ : W.IsInvertedBy G₂
f :
  Quiver.Hom (V := MorphismProperty.FunctorsInverting.{uC', uC, uD', uD} W D)
    (ObjectProperty.FullSubcategory.mk (P := fun (F : Functor.{uC', uD', uC, uD} C D) ↦ W.IsInvertedBy F) G₁ hG₁)
    (ObjectProperty.FullSubcategory.mk (P := fun (F : Functor.{uC', uD', uC, uD} C D) ↦ W.IsInvertedBy F) G₂ hG₂)
x : C
refine_2 :
  Eq (α :=
    G₁.obj ((W.Q.obj x).as (r := relations W).obj (W := W)) ⟶ G₂.obj ((W.Q.obj x).as (r := relations W).obj (W := W)))
    (NatTransExtension.app (W := W) (eqToHom ⋯ ≫ f.hom ≫ eqToHom ⋯) (W.Q.obj x))
    (CategoryStruct.comp (Y := G₁.obj x) (NatTrans.app (InducedCategory.Hom.hom (eqToHom ⋯)) x)
      (f.hom.app x ≫ NatTrans.app (InducedCategory.Hom.hom (eqToHom ⋯)) x))
⊢ Eq (α :=
    (obj (inverse W D ⋙ functor W D)
                (ObjectProperty.FullSubcategory.mk (P := fun (F : Functor.{uC', uD', uC, uD} C D) ↦ W.IsInvertedBy F) G₁
                  hG₁)).obj
            (P := fun (F : Functor.{uC', uD', uC, uD} C D) ↦ W.IsInvertedBy F).obj
        x ⟶
      (obj (inverse W D ⋙ functor W D)
                (ObjectProperty.FullSubcategory.mk (P := fun (F : Functor.{uC', uD', uC, uD} C D) ↦ W.IsInvertedBy F) G₂
                  hG₂)).obj
            (P := fun (F : Functor.{uC', uD', uC, uD} C D) ↦ W.IsInvertedBy F).obj
        x)
    (NatTrans.app (InducedCategory.Hom.hom (map (inverse W D ⋙ functor W D) f)) x)
    (NatTrans.app
      (InducedCategory.Hom.hom
        (CategoryStruct.comp (Y :=
          obj (𝟭 (MorphismProperty.FunctorsInverting.{uC', uC, uD', uD} W D))
            (ObjectProperty.FullSubcategory.mk (P := fun (F : Functor.{uC', uD', uC, uD} C D) ↦ W.IsInvertedBy F) G₁
              hG₁))
          (eqToHom ⋯) (map (𝟭 (MorphismProperty.FunctorsInverting.{uC', uC, uD', uD} W D)) f ≫ eqToHom ⋯)))
      x)

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Localization.Construction
Goal:
C : Type uC
inst : Category.{uC', uC} C
W : MorphismProperty.{uC', uC} C
D : Type uD
inst_1 : Category.{uD', uD} D
G : Functor.{uC', uD', uC, uD} C D
hG : W.IsInvertedBy G
G₁ : Functor.{uC', uD', uC, uD} C D
hG₁ : W.IsInvertedBy G₁
G₂ : Functor.{uC', uD', uC, uD} C D
hG₂ : W.IsInvertedBy G₂
f :
  Quiver.Hom (V := MorphismProperty.FunctorsInverting.{uC', uC, uD', uD} W D)
    (ObjectProperty.FullSubcategory.mk (P := fun (F : Functor.{uC', uD', uC, uD} C D) ↦ W.IsInvertedBy F) G₁ hG₁)
    (ObjectProperty.FullSubcategory.mk (P := fun (F : Functor.{uC', uD', uC, uD} C D) ↦ W.IsInvertedBy F) G₂ hG₂)
x : C
refine_2 : (eqToHom ⋯ ≫ f.hom ≫ eqToHom ⋯).app x = NatTrans.app (eqToHom ⋯) x ≫ f.hom.app x ≫ NatTrans.app (eqToHom ⋯) x
⊢ Eq (α :=
    G₁.obj ((W.Q.obj x).as (r := relations W).obj (W := W)) ⟶ G₂.obj ((W.Q.obj x).as (r := relations W).obj (W := W)))
    (NatTransExtension.app (W := W) (eqToHom ⋯ ≫ f.hom ≫ eqToHom ⋯) (W.Q.obj x))
    (CategoryStruct.comp (Y := G₁.obj x) (NatTrans.app (InducedCategory.Hom.hom (eqToHom ⋯)) x)
      (f.hom.app x ≫ NatTrans.app (InducedCategory.Hom.hom (eqToHom ⋯)) x))

Tactic:
rw [NatTransExtension.app_eq, InducedCategory.eqToHom_hom,
          InducedCategory.eqToHom_hom]

Premises used: CategoryTheory.Localization.Construction.NatTransExtension.app_eq, CategoryTheory.InducedCategory.eqToHom_hom
-- Module: Mathlib.CategoryTheory.Localization.Construction
Goal:
C : Type uC
inst : Category.{uC', uC} C
W : MorphismProperty.{uC', uC} C
D : Type uD
inst_1 : Category.{uD', uD} D
G : Functor.{uC', uD', uC, uD} C D
hG : W.IsInvertedBy G
G₁ : Functor.{uC', uD', uC, uD} C D
hG₁ : W.IsInvertedBy G₁
G₂ : Functor.{uC', uD', uC, uD} C D
hG₂ : W.IsInvertedBy G₂
f :
  Quiver.Hom (V := MorphismProperty.FunctorsInverting.{uC', uC, uD', uD} W D)
    (ObjectProperty.FullSubcategory.mk (P := fun (F : Functor.{uC', uD', uC, uD} C D) ↦ W.IsInvertedBy F) G₁ hG₁)
    (ObjectProperty.FullSubcategory.mk (P := fun (F : Functor.{uC', uD', uC, uD} C D) ↦ W.IsInvertedBy F) G₂ hG₂)
x : C
⊢ (eqToHom ⋯ ≫ f.hom ≫ eqToHom ⋯).app x = NatTrans.app (eqToHom ⋯) x ≫ f.hom.app x ≫ NatTrans.app (eqToHom ⋯) x

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Localization.Construction
Goal:
C : Type uC
inst : Category.{uC', uC} C
W : MorphismProperty.{uC', uC} C
D : Type uD
inst_1 : Category.{uD', uD} D
G : Functor.{uC', uD', uC, uD} C D
hG : W.IsInvertedBy G
F : W.Localization ⥤ D
h :
  ∀ (x : C),
    NatTrans.app
        (InducedCategory.Hom.hom
          (map (WhiskeringLeftEquivalence.functor W D)
              (NatTrans.app (Iso.hom (WhiskeringLeftEquivalence.unitIso W D)) F) ≫
            NatTrans.app (Iso.hom (WhiskeringLeftEquivalence.counitIso W D))
              (obj (WhiskeringLeftEquivalence.functor W D) F)))
        x =
      (InducedCategory.Hom.hom (𝟙 (obj (WhiskeringLeftEquivalence.functor W D) F))).app x
⊢ map (WhiskeringLeftEquivalence.functor W D) (NatTrans.app (Iso.hom (WhiskeringLeftEquivalence.unitIso W D)) F) ≫
      NatTrans.app (Iso.hom (WhiskeringLeftEquivalence.counitIso W D)) (obj (WhiskeringLeftEquivalence.functor W D) F) =
    𝟙 (obj (WhiskeringLeftEquivalence.functor W D) F)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Localization.Construction
Goal:
C : Type uC
inst : Category.{uC', uC} C
W : MorphismProperty.{uC', uC} C
D : Type uD
inst_1 : Category.{uD', uD} D
G : Functor.{uC', uD', uC, uD} C D
hG : W.IsInvertedBy G
F : W.Localization ⥤ D
x : C
⊢ NatTrans.app
      (InducedCategory.Hom.hom
        (map (WhiskeringLeftEquivalence.functor W D)
            (NatTrans.app (Iso.hom (WhiskeringLeftEquivalence.unitIso W D)) F) ≫
          NatTrans.app (Iso.hom (WhiskeringLeftEquivalence.counitIso W D))
            (obj (WhiskeringLeftEquivalence.functor W D) F)))
      x =
    (InducedCategory.Hom.hom (𝟙 (obj (WhiskeringLeftEquivalence.functor W D) F))).app x

Tactic:
simp only [WhiskeringLeftEquivalence.unitIso_hom, eqToHom_app, eqToHom_refl,
      WhiskeringLeftEquivalence.counitIso_hom, eqToHom_map, eqToHom_trans]

Premises used: CategoryTheory.eqToHom_map, CategoryTheory.eqToHom_app, CategoryTheory.eqToHom_refl, CategoryTheory.Localization.Construction.WhiskeringLeftEquivalence.unitIso_hom, CategoryTheory.Localization.Construction.WhiskeringLeftEquivalence.counitIso_hom, CategoryTheory.eqToHom_trans
-- 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
⊢ Φ.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)))

Tactic:
have : Φ.IsRightDerivabilityStructure ↔
      TwoSquare.GuitartExact ((Φ.catCommSq W₁.Q W₂.Q).iso).hom :=
    ⟨fun h => h.guitartExact', fun h => ⟨inferInstance, h⟩⟩
-- 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)))
rw :
  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))) ↔
    TwoSquare.GuitartExact e.hom
⊢ Φ.IsRightDerivabilityStructure (W₁ := W₁) (W₂ := W₂) ↔ TwoSquare.GuitartExact e.hom

Tactic:
rw [this]
-- 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''
h : ∀ (X₁ : C₁), (TwoSquare.vComp' e'.hom e'''.hom e₁ e₂).natTrans.app X₁ = (TwoSquare.natTrans e.hom).app X₁
⊢ TwoSquare.vComp' e'.hom e'''.hom e₁ e₂ = e.hom

Tactic:
ext X₁
-- 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 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₁
⊢ (TwoSquare.vComp' e'.hom e'''.hom e₁ e₂).natTrans.app X₁ = (TwoSquare.natTrans e.hom).app X₁

Tactic:
rw [TwoSquare.vComp'_app, liftNatIso_hom, liftNatTrans_app]

Premises used: CategoryTheory.Localization.liftNatTrans_app, CategoryTheory.TwoSquare.vComp'_app, CategoryTheory.Localization.liftNatIso_hom
-- 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₁) ≫
        E₂.functor.map (NatTrans.app (Iso.hom (liftingLocalizedFunctor._aux_1 (W₁ := W₁) (W₂ := W₂) Φ W₁.Q W₂.Q)) X₁) ≫
          e₂.hom.app (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X₁) ≫
            e.hom.app X₁ ≫ F.map (e₁.inv.app X₁) ≫ F.map (𝟙 (E₁.functor.obj (W₁.Q.obj 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 (Φ.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₁

Tactic:
dsimp [Lifting.iso]

Premises used: CategoryTheory.Localization.Lifting.iso
-- 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 (liftingLocalizedFunctor._aux_1 (W₁ := W₁) (W₂ := W₂) Φ W₁.Q W₂.Q)) X₁) ≫
        e₂.hom.app (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X₁) ≫ 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₁) ≫
        E₂.functor.map (NatTrans.app (Iso.hom (liftingLocalizedFunctor._aux_1 (W₁ := W₁) (W₂ := W₂) Φ W₁.Q W₂.Q)) X₁) ≫
          e₂.hom.app (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X₁) ≫
            e.hom.app X₁ ≫ F.map (e₁.inv.app X₁) ≫ F.map (𝟙 (E₁.functor.obj (W₁.Q.obj X₁))) ≫ F.map (e₁.hom.app X₁) =
    (TwoSquare.natTrans e.hom).app X₁

Tactic:
rw [F.map_id, id_comp, ← F.map_comp, Iso.inv_hom_id_app, F.map_id, comp_id,
      ← Functor.map_comp_assoc]

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.Functor.map_comp_assoc, CategoryTheory.Functor.map_id, CategoryTheory.Functor.map_comp, CategoryTheory.Iso.inv_hom_id_app, CategoryTheory.Category.id_comp