awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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₁
⊢ Eq (α := Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ W₂.Q ⟶ W₁.Q ⋙ Φ.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)))
    (Iso.inv
      (Lifting.iso W₁.Q W₁ (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ W₂.Q)
        (Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q)))

Tactic:
rfl
-- 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 (𝟙 ((Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ W₂.Q).obj 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₁ ≫
            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₁

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]

Premises used: CategoryTheory.Iso.inv_hom_id_app
-- 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₁
⊢ e₂.inv.app (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X₁) ≫
      E₂.functor.map (𝟙 ((Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ W₂.Q).obj X₁)) ≫
        e₂.hom.app (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X₁) ≫ e.hom.app X₁ =
    (TwoSquare.natTrans e.hom).app X₁

Tactic:
simp
-- 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''
⊢ TwoSquare.vComp' e'.hom e'''.hom e₁ e₂ = e.hom

Tactic:
have : TwoSquare.vComp' e'.hom e'''.hom e₁ e₂ = e.hom := by
    ext X₁
    rw [TwoSquare.vComp'_app, liftNatIso_hom, liftNatTrans_app]
    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'']
    dsimp [Lifting.iso]
    rw [F.map_id, id_comp, ← F.map_comp, Iso.inv_hom_id_app, F.map_id, comp_id,
      ← Functor.map_comp_assoc]
    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]
    simp
-- 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_1 :
  Φ.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''
this : TwoSquare.vComp' e'.hom e'''.hom e₁ e₂ = e.hom
rw : (TwoSquare.vComp' e'.hom e'''.hom e₁ e₂).GuitartExact ↔ TwoSquare.GuitartExact e.hom
rw₁ rw₂ : TwoSquare.GuitartExact e.hom ↔ TwoSquare.GuitartExact e.hom
⊢ 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

Tactic:
rw [← TwoSquare.GuitartExact.vComp'_iff_of_equivalences e'.hom E₁ E₂ e''' e₁ e₂, this]

Premises used: CategoryTheory.TwoSquare.GuitartExact.vComp'_iff_of_equivalences, CategoryTheory.Iso.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₂
h : Φ.IsRightDerivabilityStructure (W₁ := W₁) (W₂ := W₂)
e : Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L₂ ≅ L₁ ⋙ F
⊢ TwoSquare.GuitartExact e.hom

Tactic:
simpa only [Φ.isRightDerivabilityStructure_iff L₁ L₂ F e] using h

Premises used: CategoryTheory.LocalizerMorphism.isRightDerivabilityStructure_iff
-- 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 : Φ.IsRightDerivabilityStructure (W₁ := W₁) (W₂ := W₂)
⊢ TwoSquare.GuitartExact (B := Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) L₁ L₂)
    (Iso.hom (CatCommSq.iso (Φ.functor (W₁ := W₁) (W₂ := W₂)) L₁ L₂ (Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) L₁ L₂)))

Tactic:
guitartExact_of_isRightDerivabilityStructure' _ _ _ _ _

Premises used: CategoryTheory.LocalizerMorphism.guitartExact_of_isRightDerivabilityStructure'
-- 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 : W₁.ContainsIdentities
⊢ (id W₁).HasRightResolutions (W₁ := W₁) (W₂ := W₁)

Tactic:
fun X₂ => ⟨RightResolution.mk (𝟙 X₂) (W₁.id_mem X₂)⟩

Premises used: CategoryTheory.CategoryStruct.id, CategoryTheory.LocalizerMorphism.RightResolution.mk, Nonempty.intro, CategoryTheory.MorphismProperty.id_mem
-- 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 : W₁.ContainsIdentities
rw :
  TwoSquare.GuitartExact (C₁ := C₁) (C₂ := C₁) (C₃ := W₁.Localization) (C₄ := W₁.Localization) (T :=
    (id W₁).functor (W₁ := W₁) (W₂ := W₁)) (L := W₁.Q) (R := W₁.Q) (B := 𝟭 W₁.Localization)
    (Iso.hom (Iso.refl ((id W₁).functor (W₁ := W₁) (W₂ := W₁) ⋙ W₁.Q)))
⊢ (id W₁).IsRightDerivabilityStructure (W₁ := W₁) (W₂ := W₁)

Tactic:
rw [(LocalizerMorphism.id W₁).isRightDerivabilityStructure_iff W₁.Q W₁.Q (𝟭 W₁.Localization)
    (Iso.refl _)]

Premises used: CategoryTheory.MorphismProperty.Q, CategoryTheory.Functor.id, CategoryTheory.Iso.refl, CategoryTheory.MorphismProperty.Localization, CategoryTheory.LocalizerMorphism.isRightDerivabilityStructure_iff, CategoryTheory.LocalizerMorphism.id
-- 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 : W₁.ContainsIdentities
⊢ TwoSquare.GuitartExact (C₁ := C₁) (C₂ := C₁) (C₃ := W₁.Localization) (C₄ := W₁.Localization) (T := 𝟭 C₁) (L := W₁.Q)
    (R := W₁.Q) (B := 𝟭 W₁.Localization) (𝟙 (𝟭 C₁ ⋙ W₁.Q))

Tactic:
TwoSquare.guitartExact_id W₁.Q

Premises used: CategoryTheory.MorphismProperty.Q, CategoryTheory.Functor.comp, CategoryTheory.TwoSquare.guitartExact_id
-- 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 : W₁.ContainsIdentities
⊢ TwoSquare.GuitartExact (C₁ := C₁) (C₂ := C₁) (C₃ := W₁.Localization) (C₄ := W₁.Localization) (T := 𝟭 C₁) (L := W₁.Q)
    (R := W₁.Q) (B := 𝟭 W₁.Localization) (𝟙 (𝟭 C₁ ⋙ W₁.Q))

Tactic:
exact TwoSquare.guitartExact_id W₁.Q

Premises used: CategoryTheory.MorphismProperty.Q, CategoryTheory.TwoSquare.guitartExact_id
-- 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₂
F : W₁.Localization ⥤ W₂.Localization := Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q
e : Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ W₂.Q ≅ W₁.Q ⋙ F :=
  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₂).op ⋙ W₂.Q.op ≅ W₁.Q.op ⋙ F.op := NatIso.op e.symm
⊢ TwoSquare.GuitartExact e'.hom ↔ TwoSquare.GuitartExact e.inv

Tactic:
have eq : TwoSquare.GuitartExact e'.hom ↔ TwoSquare.GuitartExact e.inv :=
    TwoSquare.guitartExact_op_iff _
-- 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₂
F : W₁.Localization ⥤ W₂.Localization := Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q
e : Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ W₂.Q ≅ W₁.Q ⋙ F :=
  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₂).op ⋙ W₂.Q.op ≅ W₁.Q.op ⋙ F.op := NatIso.op e.symm
eq : TwoSquare.GuitartExact e'.hom ↔ TwoSquare.GuitartExact e.inv
mp :
  Φ.IsLeftDerivabilityStructure (W₁ := W₁) (W₂ := W₂) →
    Φ.op (W₁ := W₁) (W₂ := W₂).IsRightDerivabilityStructure (W₁ := W₁.op) (W₂ := W₂.op)
mpr :
  Φ.op (W₁ := W₁) (W₂ := W₂).IsRightDerivabilityStructure (W₁ := W₁.op) (W₂ := W₂.op) →
    Φ.IsLeftDerivabilityStructure (W₁ := W₁) (W₂ := W₂)
⊢ Φ.IsLeftDerivabilityStructure (W₁ := W₁) (W₂ := W₂) ↔
    Φ.op (W₁ := W₁) (W₂ := W₂).IsRightDerivabilityStructure (W₁ := W₁.op) (W₂ := W₂.op)

Tactic:
constructor
-- 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₂
F : W₁.Localization ⥤ W₂.Localization := Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q
e : Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ W₂.Q ≅ W₁.Q ⋙ F :=
  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₂).op ⋙ W₂.Q.op ≅ W₁.Q.op ⋙ F.op := NatIso.op e.symm
eq : TwoSquare.GuitartExact e'.hom ↔ TwoSquare.GuitartExact e.inv
hasLeftResolutions : Φ.HasLeftResolutions (W₁ := W₁) (W₂ := W₂)
guitartExact' :
  TwoSquare.GuitartExact (R := Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q)
    (Iso.inv
      (CatCommSq.iso (Φ.functor (W₁ := W₁) (W₂ := W₂)) W₁.Q W₂.Q (Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q)))
mp : TwoSquare.GuitartExact e'.hom
mp₁ mp₂ mp₃ mp₄ : TwoSquare.GuitartExact e.inv
⊢ Φ.op (W₁ := W₁) (W₂ := W₂).IsRightDerivabilityStructure (W₁ := W₁.op) (W₂ := W₂.op)

Tactic:
rwa [Φ.op.isRightDerivabilityStructure_iff _ _ _ e', eq]

Premises used: CategoryTheory.LocalizerMorphism.isRightDerivabilityStructure_iff, CategoryTheory.LocalizerMorphism.op
-- 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₂
F : W₁.Localization ⥤ W₂.Localization := Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q
e : Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ W₂.Q ≅ W₁.Q ⋙ F :=
  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₂).op ⋙ W₂.Q.op ≅ W₁.Q.op ⋙ F.op := NatIso.op e.symm
eq : TwoSquare.GuitartExact e'.hom ↔ TwoSquare.GuitartExact e.inv
h : Φ.op (W₁ := W₁) (W₂ := W₂).IsRightDerivabilityStructure (W₁ := W₁.op) (W₂ := W₂.op)
rw : Φ.op (W₁ := W₁) (W₂ := W₂).HasRightResolutions (W₁ := W₁.op) (W₂ := W₂.op)
⊢ Φ.HasLeftResolutions (W₁ := W₁) (W₂ := W₂)

Tactic:
rw [hasLeftResolutions_iff_op]

Premises used: CategoryTheory.LocalizerMorphism.hasLeftResolutions_iff_op
-- 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₂
F : W₁.Localization ⥤ W₂.Localization := Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q
e : Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ W₂.Q ≅ W₁.Q ⋙ F :=
  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₂).op ⋙ W₂.Q.op ≅ W₁.Q.op ⋙ F.op := NatIso.op e.symm
eq : TwoSquare.GuitartExact e'.hom ↔ TwoSquare.GuitartExact e.inv
h : Φ.op (W₁ := W₁) (W₂ := W₂).IsRightDerivabilityStructure (W₁ := W₁.op) (W₂ := W₂.op)
⊢ Φ.op (W₁ := W₁) (W₂ := W₂).HasRightResolutions (W₁ := W₁.op) (W₂ := W₂.op)

Tactic:
infer_instance
-- 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₂
F : W₁.Localization ⥤ W₂.Localization := Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q
e : Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ W₂.Q ≅ W₁.Q ⋙ F :=
  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₂).op ⋙ W₂.Q.op ≅ W₁.Q.op ⋙ F.op := NatIso.op e.symm
eq : TwoSquare.GuitartExact e'.hom ↔ TwoSquare.GuitartExact e.inv
h : Φ.op (W₁ := W₁) (W₂ := W₂).IsRightDerivabilityStructure (W₁ := W₁.op) (W₂ := W₂.op)
⊢ Φ.HasLeftResolutions (W₁ := W₁) (W₂ := W₂)

Tactic:
have : Φ.HasLeftResolutions := by
      rw [hasLeftResolutions_iff_op]
      infer_instance