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₂
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)
this : Φ.HasLeftResolutions (W₁ := W₁) (W₂ := W₂)
⊢ Φ.IsLeftDerivabilityStructure (W₁ := W₁) (W₂ := W₂)

Tactic:
⟨inferInstance, ?_⟩

Premises used: inferInstance, CategoryTheory.LocalizerMorphism.IsLeftDerivabilityStructure.mk
-- 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)
this : Φ.HasLeftResolutions (W₁ := W₁) (W₂ := W₂)
mpr :
  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)))
⊢ Φ.IsLeftDerivabilityStructure (W₁ := W₁) (W₂ := W₂)

Tactic:
refine ⟨inferInstance, ?_⟩
-- 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)
this : Φ.HasLeftResolutions (W₁ := W₁) (W₂ := W₂)
mpr : TwoSquare.GuitartExact e'.hom
⊢ 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)))

Tactic:
rw [← eq]
-- 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)
this : Φ.HasLeftResolutions (W₁ := W₁) (W₂ := W₂)
⊢ TwoSquare.GuitartExact e'.hom

Tactic:
Φ.op.guitartExact_of_isRightDerivabilityStructure' _ _ _ e'

Premises used: CategoryTheory.Functor.op, CategoryTheory.LocalizerMorphism.guitartExact_of_isRightDerivabilityStructure', 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)
this : Φ.HasLeftResolutions (W₁ := W₁) (W₂ := W₂)
⊢ TwoSquare.GuitartExact e'.hom

Tactic:
exact Φ.op.guitartExact_of_isRightDerivabilityStructure' _ _ _ e'

Premises used: CategoryTheory.LocalizerMorphism.guitartExact_of_isRightDerivabilityStructure', 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₂
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 : Φ.HasLeftResolutions (W₁ := W₁) (W₂ := W₂)
e : Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L₂ ≅ L₁ ⋙ F
rw : TwoSquare.GuitartExact (NatIso.op e.symm).hom ↔ (TwoSquare.op e.inv).GuitartExact
⊢ Φ.IsLeftDerivabilityStructure (W₁ := W₁) (W₂ := W₂) ↔ TwoSquare.GuitartExact e.inv

Tactic:
rw [isLeftDerivabilityStructure_iff_op,
    Φ.op.isRightDerivabilityStructure_iff L₁.op L₂.op F.op (NatIso.op e.symm),
    ← TwoSquare.guitartExact_op_iff e.inv]

Premises used: CategoryTheory.Functor.op, CategoryTheory.TwoSquare.guitartExact_op_iff, CategoryTheory.LocalizerMorphism.isRightDerivabilityStructure_iff, CategoryTheory.Iso.symm, CategoryTheory.NatIso.op, CategoryTheory.Iso.inv, CategoryTheory.LocalizerMorphism.op, CategoryTheory.LocalizerMorphism.isLeftDerivabilityStructure_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₂
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 : Φ.HasLeftResolutions (W₁ := W₁) (W₂ := W₂)
e : Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L₂ ≅ L₁ ⋙ F
⊢ TwoSquare.GuitartExact (NatIso.op e.symm).hom ↔ (TwoSquare.op e.inv).GuitartExact

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₂
h : Φ.IsLeftDerivabilityStructure (W₁ := W₁) (W₂ := W₂)
e : Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L₂ ≅ L₁ ⋙ F
⊢ TwoSquare.GuitartExact e.inv

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

Premises used: CategoryTheory.LocalizerMorphism.isLeftDerivabilityStructure_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 : Φ.IsLeftDerivabilityStructure (W₁ := W₁) (W₂ := W₂)
⊢ TwoSquare.GuitartExact (R := Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) L₁ L₂)
    (Iso.inv (CatCommSq.iso (Φ.functor (W₁ := W₁) (W₂ := W₂)) L₁ L₂ (Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) L₁ L₂)))

Tactic:
guitartExact_of_isLeftDerivabilityStructure' _ _ _ _ _

Premises used: CategoryTheory.LocalizerMorphism.guitartExact_of_isLeftDerivabilityStructure'
-- 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₁).HasLeftResolutions (W₁ := W₁) (W₂ := W₁)

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

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

Tactic:
rw [(LocalizerMorphism.id W₁).isLeftDerivabilityStructure_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.id, CategoryTheory.LocalizerMorphism.isLeftDerivabilityStructure_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 : W₁.ContainsIdentities
⊢ TwoSquare.GuitartExact (C₁ := C₁) (C₂ := W₁.Localization) (C₃ := C₁) (C₄ := W₁.Localization) (T := W₁.Q) (L := 𝟭 C₁)
    (R := 𝟭 W₁.Localization) (B := W₁.Q) (𝟙 (𝟭 C₁ ⋙ W₁.Q))

Tactic:
TwoSquare.guitartExact_id' W₁.Q

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

Tactic:
exact TwoSquare.guitartExact_id' W₁.Q

Premises used: CategoryTheory.TwoSquare.guitartExact_id', CategoryTheory.MorphismProperty.Q
-- 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'.inv ↔ TwoSquare.GuitartExact e.hom

Tactic:
have eq : TwoSquare.GuitartExact e'.inv ↔ TwoSquare.GuitartExact e.hom :=
    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'.inv ↔ TwoSquare.GuitartExact e.hom
⊢ Φ.IsRightDerivabilityStructure (W₁ := W₁) (W₂ := W₂) ↔
    Φ.op (W₁ := W₁) (W₂ := W₂).IsLeftDerivabilityStructure (W₁ := W₁.op) (W₂ := W₂.op)

Tactic:
⟨fun ⟨_, _⟩ ↦ ?_, fun _ ↦ ?_⟩

Premises used: CategoryTheory.LocalizerMorphism.IsLeftDerivabilityStructure, _private.0.CategoryTheory.LocalizerMorphism.isRightDerivabilityStructure_iff_op.match_1, Iff.intro, 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'.inv ↔ TwoSquare.GuitartExact e.hom
refine_1 :
  Φ.IsRightDerivabilityStructure (W₁ := W₁) (W₂ := W₂) →
    Φ.HasRightResolutions (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))) →
        Φ.op (W₁ := W₁) (W₂ := W₂).IsLeftDerivabilityStructure (W₁ := W₁.op) (W₂ := W₂.op)
refine_2 :
  Φ.op (W₁ := W₁) (W₂ := W₂).IsLeftDerivabilityStructure (W₁ := W₁.op) (W₂ := W₂.op) →
    Φ.IsRightDerivabilityStructure (W₁ := W₁) (W₂ := W₂)
⊢ Φ.IsRightDerivabilityStructure (W₁ := W₁) (W₂ := W₂) ↔
    Φ.op (W₁ := W₁) (W₂ := W₂).IsLeftDerivabilityStructure (W₁ := W₁.op) (W₂ := W₂.op)

Tactic:
refine ⟨fun ⟨_, _⟩ ↦ ?_, fun _ ↦ ?_⟩
-- 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'.inv ↔ TwoSquare.GuitartExact e.hom
h : Φ.IsRightDerivabilityStructure (W₁ := W₁) (W₂ := W₂)
hasRightResolutions : Φ.HasRightResolutions (W₁ := W₁) (W₂ := W₂)
guitartExact' :
  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)))
⊢ Φ.op (W₁ := W₁) (W₂ := W₂).IsLeftDerivabilityStructure (W₁ := W₁.op) (W₂ := W₂.op)

Tactic:
simpa only [Φ.op.isLeftDerivabilityStructure_iff _ _ _ e', eq]

Premises used: CategoryTheory.LocalizerMorphism.isLeftDerivabilityStructure_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'.inv ↔ TwoSquare.GuitartExact e.hom
h : Φ.op (W₁ := W₁) (W₂ := W₂).IsLeftDerivabilityStructure (W₁ := W₁.op) (W₂ := W₂.op)
rw : Φ.op (W₁ := W₁) (W₂ := W₂).HasLeftResolutions (W₁ := W₁.op) (W₂ := W₂.op)
⊢ Φ.HasRightResolutions (W₁ := W₁) (W₂ := W₂)

Tactic:
rw [hasRightResolutions_iff_op]

Premises used: CategoryTheory.LocalizerMorphism.hasRightResolutions_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'.inv ↔ TwoSquare.GuitartExact e.hom
h : Φ.op (W₁ := W₁) (W₂ := W₂).IsLeftDerivabilityStructure (W₁ := W₁.op) (W₂ := W₂.op)
⊢ Φ.op (W₁ := W₁) (W₂ := W₂).HasLeftResolutions (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'.inv ↔ TwoSquare.GuitartExact e.hom
h : Φ.op (W₁ := W₁) (W₂ := W₂).IsLeftDerivabilityStructure (W₁ := W₁.op) (W₂ := W₂.op)
⊢ Φ.HasRightResolutions (W₁ := W₁) (W₂ := W₂)

Tactic:
have : Φ.HasRightResolutions := by
      rw [hasRightResolutions_iff_op]
      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'.inv ↔ TwoSquare.GuitartExact e.hom
h : Φ.op (W₁ := W₁) (W₂ := W₂).IsLeftDerivabilityStructure (W₁ := W₁.op) (W₂ := W₂.op)
this : Φ.HasRightResolutions (W₁ := W₁) (W₂ := W₂)
⊢ Φ.IsRightDerivabilityStructure (W₁ := W₁) (W₂ := W₂)

Tactic:
⟨inferInstance, ?_⟩

Premises used: inferInstance, CategoryTheory.LocalizerMorphism.IsRightDerivabilityStructure.mk
-- 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'.inv ↔ TwoSquare.GuitartExact e.hom
h : Φ.op (W₁ := W₁) (W₂ := W₂).IsLeftDerivabilityStructure (W₁ := W₁.op) (W₂ := W₂.op)
this : Φ.HasRightResolutions (W₁ := W₁) (W₂ := W₂)
refine_2 :
  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)))
⊢ Φ.IsRightDerivabilityStructure (W₁ := W₁) (W₂ := W₂)

Tactic:
refine ⟨inferInstance, ?_⟩
-- 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'.inv ↔ TwoSquare.GuitartExact e.hom
h : Φ.op (W₁ := W₁) (W₂ := W₂).IsLeftDerivabilityStructure (W₁ := W₁.op) (W₂ := W₂.op)
this : Φ.HasRightResolutions (W₁ := W₁) (W₂ := W₂)
refine_2 : TwoSquare.GuitartExact e'.inv
⊢ 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:
rw [← eq]