awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.OfLocalizedEquivalences
Goal:
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} D₁
inst_3 : Category.{v_4, u_4} D₂
W₁ : MorphismProperty.{v_1, u_1} C₁
W₁' : MorphismProperty.{v_3, u_3} D₁
W₂ : MorphismProperty.{v_2, u_2} C₂
W₂' : MorphismProperty.{v_4, u_4} D₂
T : LocalizerMorphism W₁ W₂
L : LocalizerMorphism W₁ W₁'
R : LocalizerMorphism W₂ W₂'
B : LocalizerMorphism W₁' W₂'
inst_4 : W₂'.RespectsIso
inst_5 : L.IsLocalizedEquivalence (W₁ := W₁) (W₂ := W₁')
inst_6 : R.IsLocalizedEquivalence (W₁ := W₂) (W₂ := W₂')
inst_7 : R.functor (W₁ := W₂) (W₂ := W₂').EssSurj
inst_8 : L.functor (W₁ := W₁) (W₂ := W₁').EssSurj
inst_9 : R.functor (W₁ := W₂) (W₂ := W₂').Full
inst_10 : R.IsInduced (W₁ := W₂) (W₂ := W₂')
iso :
  T.functor (W₁ := W₁) (W₂ := W₂) ⋙ R.functor (W₁ := W₂) (W₂ := W₂') ≅
    L.functor (W₁ := W₁) (W₂ := W₁') ⋙ B.functor (W₁ := W₁') (W₂ := W₂')
inst_11 : TwoSquare.GuitartExact iso.inv
h : B.IsLeftDerivabilityStructure (W₁ := W₁') (W₂ := W₂')
⊢ T.HasLeftResolutions (W₁ := W₁) (W₂ := W₂)

Tactic:
have : T.HasLeftResolutions := fun X₂ ↦ by
    let ρ : B.LeftResolution (R.functor.obj X₂) := Classical.arbitrary _
    exact ⟨{
      X₁ := L.functor.objPreimage ρ.X₁
      w :=
        R.functor.preimage (iso.hom.app _ ≫
          B.functor.map (L.functor.objObjPreimageIso ρ.X₁).hom ≫ ρ.w)
      hw := by
        simp only [← R.inverseImage_eq, Functor.comp_obj,
          MorphismProperty.inverseImage_iff, Functor.map_preimage]
        refine (W₂'.arrow_mk_iso_iff ?_).2 ρ.hw
        exact Arrow.isoMk (iso.app _ ≪≫ B.functor.mapIso (L.functor.objObjPreimageIso ρ.X₁))
          (Iso.refl _) }⟩
-- Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.OfLocalizedEquivalences
Goal:
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} D₁
inst_3 : Category.{v_4, u_4} D₂
W₁ : MorphismProperty.{v_1, u_1} C₁
W₁' : MorphismProperty.{v_3, u_3} D₁
W₂ : MorphismProperty.{v_2, u_2} C₂
W₂' : MorphismProperty.{v_4, u_4} D₂
T : LocalizerMorphism W₁ W₂
L : LocalizerMorphism W₁ W₁'
R : LocalizerMorphism W₂ W₂'
B : LocalizerMorphism W₁' W₂'
inst_4 : W₂'.RespectsIso
inst_5 : L.IsLocalizedEquivalence (W₁ := W₁) (W₂ := W₁')
inst_6 : R.IsLocalizedEquivalence (W₁ := W₂) (W₂ := W₂')
inst_7 : R.functor (W₁ := W₂) (W₂ := W₂').EssSurj
inst_8 : L.functor (W₁ := W₁) (W₂ := W₁').EssSurj
inst_9 : R.functor (W₁ := W₂) (W₂ := W₂').Full
inst_10 : R.IsInduced (W₁ := W₂) (W₂ := W₂')
iso :
  T.functor (W₁ := W₁) (W₂ := W₂) ⋙ R.functor (W₁ := W₂) (W₂ := W₂') ≅
    L.functor (W₁ := W₁) (W₂ := W₁') ⋙ B.functor (W₁ := W₁') (W₂ := W₂')
inst_11 : TwoSquare.GuitartExact iso.inv
h : B.IsLeftDerivabilityStructure (W₁ := W₁') (W₂ := W₂')
this : T.HasLeftResolutions (W₁ := W₁) (W₂ := W₂)
F : W₁'.Localization ⥤ W₂'.Localization := B.localizedFunctor (W₁ := W₁') (W₂ := W₂') W₁'.Q W₂'.Q
e' : B.functor (W₁ := W₁') (W₂ := W₂') ⋙ W₂'.Q ≅ W₁'.Q ⋙ F :=
  CatCommSq.iso (B.functor (W₁ := W₁') (W₂ := W₂')) W₁'.Q W₂'.Q F
e : T.functor (W₁ := W₁) (W₂ := W₂) ⋙ R.functor (W₁ := W₂) (W₂ := W₂') ⋙ W₂'.Q ≅
  (L.functor (W₁ := W₁) (W₂ := W₁') ⋙ W₁'.Q) ⋙ F :=
  (T.functor (W₁ := W₁) (W₂ := W₂).associator (R.functor (W₁ := W₂) (W₂ := W₂')) W₂'.Q).symm ≪≫
    Functor.isoWhiskerRight iso W₂'.Q ≪≫
      L.functor (W₁ := W₁) (W₂ := W₁').associator (B.functor (W₁ := W₁') (W₂ := W₂')) W₂'.Q ≪≫
        L.functor (W₁ := W₁) (W₂ := W₁').isoWhiskerLeft e' ≪≫ (L.functor (W₁ := W₁) (W₂ := W₁').associator W₁'.Q F).symm
⊢ TwoSquare.GuitartExact e'.inv

Tactic:
have he' : TwoSquare.GuitartExact e'.inv := inferInstance
-- Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.OfLocalizedEquivalences
Goal:
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} D₁
inst_3 : Category.{v_4, u_4} D₂
W₁ : MorphismProperty.{v_1, u_1} C₁
W₁' : MorphismProperty.{v_3, u_3} D₁
W₂ : MorphismProperty.{v_2, u_2} C₂
W₂' : MorphismProperty.{v_4, u_4} D₂
T : LocalizerMorphism W₁ W₂
L : LocalizerMorphism W₁ W₁'
R : LocalizerMorphism W₂ W₂'
B : LocalizerMorphism W₁' W₂'
inst_4 : W₂'.RespectsIso
inst_5 : L.IsLocalizedEquivalence (W₁ := W₁) (W₂ := W₁')
inst_6 : R.IsLocalizedEquivalence (W₁ := W₂) (W₂ := W₂')
inst_7 : R.functor (W₁ := W₂) (W₂ := W₂').EssSurj
inst_8 : L.functor (W₁ := W₁) (W₂ := W₁').EssSurj
inst_9 : R.functor (W₁ := W₂) (W₂ := W₂').Full
inst_10 : R.IsInduced (W₁ := W₂) (W₂ := W₂')
iso :
  T.functor (W₁ := W₁) (W₂ := W₂) ⋙ R.functor (W₁ := W₂) (W₂ := W₂') ≅
    L.functor (W₁ := W₁) (W₂ := W₁') ⋙ B.functor (W₁ := W₁') (W₂ := W₂')
inst_11 : TwoSquare.GuitartExact iso.inv
h_1 : B.IsLeftDerivabilityStructure (W₁ := W₁') (W₂ := W₂')
this : T.HasLeftResolutions (W₁ := W₁) (W₂ := W₂)
F : W₁'.Localization ⥤ W₂'.Localization := B.localizedFunctor (W₁ := W₁') (W₂ := W₂') W₁'.Q W₂'.Q
e' : B.functor (W₁ := W₁') (W₂ := W₂') ⋙ W₂'.Q ≅ W₁'.Q ⋙ F :=
  CatCommSq.iso (B.functor (W₁ := W₁') (W₂ := W₂')) W₁'.Q W₂'.Q F
e : T.functor (W₁ := W₁) (W₂ := W₂) ⋙ R.functor (W₁ := W₂) (W₂ := W₂') ⋙ W₂'.Q ≅
  (L.functor (W₁ := W₁) (W₂ := W₁') ⋙ W₁'.Q) ⋙ F :=
  (T.functor (W₁ := W₁) (W₂ := W₂).associator (R.functor (W₁ := W₂) (W₂ := W₂')) W₂'.Q).symm ≪≫
    Functor.isoWhiskerRight iso W₂'.Q ≪≫
      L.functor (W₁ := W₁) (W₂ := W₁').associator (B.functor (W₁ := W₁') (W₂ := W₂')) W₂'.Q ≪≫
        L.functor (W₁ := W₁) (W₂ := W₁').isoWhiskerLeft e' ≪≫ (L.functor (W₁ := W₁) (W₂ := W₁').associator W₁'.Q F).symm
he' : TwoSquare.GuitartExact e'.inv
h : ∀ (X : C₁), (TwoSquare.hComp iso.inv e'.inv).natTrans.app X = (TwoSquare.natTrans e.inv).app X
⊢ TwoSquare.hComp iso.inv e'.inv = e.inv

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.OfLocalizedEquivalences
Goal:
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} D₁
inst_3 : Category.{v_4, u_4} D₂
W₁ : MorphismProperty.{v_1, u_1} C₁
W₁' : MorphismProperty.{v_3, u_3} D₁
W₂ : MorphismProperty.{v_2, u_2} C₂
W₂' : MorphismProperty.{v_4, u_4} D₂
T : LocalizerMorphism W₁ W₂
L : LocalizerMorphism W₁ W₁'
R : LocalizerMorphism W₂ W₂'
B : LocalizerMorphism W₁' W₂'
inst_4 : W₂'.RespectsIso
inst_5 : L.IsLocalizedEquivalence (W₁ := W₁) (W₂ := W₁')
inst_6 : R.IsLocalizedEquivalence (W₁ := W₂) (W₂ := W₂')
inst_7 : R.functor (W₁ := W₂) (W₂ := W₂').EssSurj
inst_8 : L.functor (W₁ := W₁) (W₂ := W₁').EssSurj
inst_9 : R.functor (W₁ := W₂) (W₂ := W₂').Full
inst_10 : R.IsInduced (W₁ := W₂) (W₂ := W₂')
iso :
  T.functor (W₁ := W₁) (W₂ := W₂) ⋙ R.functor (W₁ := W₂) (W₂ := W₂') ≅
    L.functor (W₁ := W₁) (W₂ := W₁') ⋙ B.functor (W₁ := W₁') (W₂ := W₂')
inst_11 : TwoSquare.GuitartExact iso.inv
h : B.IsLeftDerivabilityStructure (W₁ := W₁') (W₂ := W₂')
this : T.HasLeftResolutions (W₁ := W₁) (W₂ := W₂)
F : W₁'.Localization ⥤ W₂'.Localization := B.localizedFunctor (W₁ := W₁') (W₂ := W₂') W₁'.Q W₂'.Q
e' : B.functor (W₁ := W₁') (W₂ := W₂') ⋙ W₂'.Q ≅ W₁'.Q ⋙ F :=
  CatCommSq.iso (B.functor (W₁ := W₁') (W₂ := W₂')) W₁'.Q W₂'.Q F
e : T.functor (W₁ := W₁) (W₂ := W₂) ⋙ R.functor (W₁ := W₂) (W₂ := W₂') ⋙ W₂'.Q ≅
  (L.functor (W₁ := W₁) (W₂ := W₁') ⋙ W₁'.Q) ⋙ F :=
  (T.functor (W₁ := W₁) (W₂ := W₂).associator (R.functor (W₁ := W₂) (W₂ := W₂')) W₂'.Q).symm ≪≫
    Functor.isoWhiskerRight iso W₂'.Q ≪≫
      L.functor (W₁ := W₁) (W₂ := W₁').associator (B.functor (W₁ := W₁') (W₂ := W₂')) W₂'.Q ≪≫
        L.functor (W₁ := W₁) (W₂ := W₁').isoWhiskerLeft e' ≪≫ (L.functor (W₁ := W₁) (W₂ := W₁').associator W₁'.Q F).symm
he' : TwoSquare.GuitartExact e'.inv
X : C₁
⊢ (TwoSquare.hComp iso.inv e'.inv).natTrans.app X = (TwoSquare.natTrans e.inv).app X

Tactic:
simp [e]
-- Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.OfLocalizedEquivalences
Goal:
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} D₁
inst_3 : Category.{v_4, u_4} D₂
W₁ : MorphismProperty.{v_1, u_1} C₁
W₁' : MorphismProperty.{v_3, u_3} D₁
W₂ : MorphismProperty.{v_2, u_2} C₂
W₂' : MorphismProperty.{v_4, u_4} D₂
T : LocalizerMorphism W₁ W₂
L : LocalizerMorphism W₁ W₁'
R : LocalizerMorphism W₂ W₂'
B : LocalizerMorphism W₁' W₂'
inst_4 : W₂'.RespectsIso
inst_5 : L.IsLocalizedEquivalence (W₁ := W₁) (W₂ := W₁')
inst_6 : R.IsLocalizedEquivalence (W₁ := W₂) (W₂ := W₂')
inst_7 : R.functor (W₁ := W₂) (W₂ := W₂').EssSurj
inst_8 : L.functor (W₁ := W₁) (W₂ := W₁').EssSurj
inst_9 : R.functor (W₁ := W₂) (W₂ := W₂').Full
inst_10 : R.IsInduced (W₁ := W₂) (W₂ := W₂')
iso :
  T.functor (W₁ := W₁) (W₂ := W₂) ⋙ R.functor (W₁ := W₂) (W₂ := W₂') ≅
    L.functor (W₁ := W₁) (W₂ := W₁') ⋙ B.functor (W₁ := W₁') (W₂ := W₂')
inst_11 : TwoSquare.GuitartExact iso.inv
h : B.IsLeftDerivabilityStructure (W₁ := W₁') (W₂ := W₂')
this : T.HasLeftResolutions (W₁ := W₁) (W₂ := W₂)
F : W₁'.Localization ⥤ W₂'.Localization := B.localizedFunctor (W₁ := W₁') (W₂ := W₂') W₁'.Q W₂'.Q
e' : B.functor (W₁ := W₁') (W₂ := W₂') ⋙ W₂'.Q ≅ W₁'.Q ⋙ F :=
  CatCommSq.iso (B.functor (W₁ := W₁') (W₂ := W₂')) W₁'.Q W₂'.Q F
e : T.functor (W₁ := W₁) (W₂ := W₂) ⋙ R.functor (W₁ := W₂) (W₂ := W₂') ⋙ W₂'.Q ≅
  (L.functor (W₁ := W₁) (W₂ := W₁') ⋙ W₁'.Q) ⋙ F :=
  (T.functor (W₁ := W₁) (W₂ := W₂).associator (R.functor (W₁ := W₂) (W₂ := W₂')) W₂'.Q).symm ≪≫
    Functor.isoWhiskerRight iso W₂'.Q ≪≫
      L.functor (W₁ := W₁) (W₂ := W₁').associator (B.functor (W₁ := W₁') (W₂ := W₂')) W₂'.Q ≪≫
        L.functor (W₁ := W₁) (W₂ := W₁').isoWhiskerLeft e' ≪≫ (L.functor (W₁ := W₁) (W₂ := W₁').associator W₁'.Q F).symm
he' : TwoSquare.GuitartExact e'.inv
⊢ TwoSquare.hComp iso.inv e'.inv = e.inv

Tactic:
have : TwoSquare.hComp iso.inv e'.inv = e.inv := by ext; simp [e]
-- Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.OfLocalizedEquivalences
Goal:
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} D₁
inst_3 : Category.{v_4, u_4} D₂
W₁ : MorphismProperty.{v_1, u_1} C₁
W₁' : MorphismProperty.{v_3, u_3} D₁
W₂ : MorphismProperty.{v_2, u_2} C₂
W₂' : MorphismProperty.{v_4, u_4} D₂
T : LocalizerMorphism W₁ W₂
L : LocalizerMorphism W₁ W₁'
R : LocalizerMorphism W₂ W₂'
B : LocalizerMorphism W₁' W₂'
inst_4 : W₂'.RespectsIso
inst_5 : L.IsLocalizedEquivalence (W₁ := W₁) (W₂ := W₁')
inst_6 : R.IsLocalizedEquivalence (W₁ := W₂) (W₂ := W₂')
inst_7 : R.functor (W₁ := W₂) (W₂ := W₂').EssSurj
inst_8 : L.functor (W₁ := W₁) (W₂ := W₁').EssSurj
inst_9 : R.functor (W₁ := W₂) (W₂ := W₂').Full
inst_10 : R.IsInduced (W₁ := W₂) (W₂ := W₂')
iso :
  T.functor (W₁ := W₁) (W₂ := W₂) ⋙ R.functor (W₁ := W₂) (W₂ := W₂') ≅
    L.functor (W₁ := W₁) (W₂ := W₁') ⋙ B.functor (W₁ := W₁') (W₂ := W₂')
inst_11 : TwoSquare.GuitartExact iso.inv
h : B.IsLeftDerivabilityStructure (W₁ := W₁') (W₂ := W₂')
this_1 : T.HasLeftResolutions (W₁ := W₁) (W₂ := W₂)
F : W₁'.Localization ⥤ W₂'.Localization := B.localizedFunctor (W₁ := W₁') (W₂ := W₂') W₁'.Q W₂'.Q
e' : B.functor (W₁ := W₁') (W₂ := W₂') ⋙ W₂'.Q ≅ W₁'.Q ⋙ F :=
  CatCommSq.iso (B.functor (W₁ := W₁') (W₂ := W₂')) W₁'.Q W₂'.Q F
e : T.functor (W₁ := W₁) (W₂ := W₂) ⋙ R.functor (W₁ := W₂) (W₂ := W₂') ⋙ W₂'.Q ≅
  (L.functor (W₁ := W₁) (W₂ := W₁') ⋙ W₁'.Q) ⋙ F :=
  (T.functor (W₁ := W₁) (W₂ := W₂).associator (R.functor (W₁ := W₂) (W₂ := W₂')) W₂'.Q).symm ≪≫
    Functor.isoWhiskerRight iso W₂'.Q ≪≫
      L.functor (W₁ := W₁) (W₂ := W₁').associator (B.functor (W₁ := W₁') (W₂ := W₂')) W₂'.Q ≪≫
        L.functor (W₁ := W₁) (W₂ := W₁').isoWhiskerLeft e' ≪≫ (L.functor (W₁ := W₁) (W₂ := W₁').associator W₁'.Q F).symm
he' : TwoSquare.GuitartExact e'.inv
this : TwoSquare.hComp iso.inv e'.inv = e.inv
rw : (TwoSquare.hComp iso.inv e'.inv).GuitartExact
⊢ T.IsLeftDerivabilityStructure (W₁ := W₁) (W₂ := W₂)

Tactic:
rw [T.isLeftDerivabilityStructure_iff (L.functor ⋙ W₁'.Q)
    (R.functor ⋙ W₂'.Q) F e, ← this]

Premises used: CategoryTheory.MorphismProperty.Q, CategoryTheory.Functor.comp, CategoryTheory.LocalizerMorphism.functor, CategoryTheory.LocalizerMorphism.isLeftDerivabilityStructure_iff
-- Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.OfLocalizedEquivalences
Goal:
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} D₁
inst_3 : Category.{v_4, u_4} D₂
W₁ : MorphismProperty.{v_1, u_1} C₁
W₁' : MorphismProperty.{v_3, u_3} D₁
W₂ : MorphismProperty.{v_2, u_2} C₂
W₂' : MorphismProperty.{v_4, u_4} D₂
T : LocalizerMorphism W₁ W₂
L : LocalizerMorphism W₁ W₁'
R : LocalizerMorphism W₂ W₂'
B : LocalizerMorphism W₁' W₂'
inst_4 : W₂'.RespectsIso
inst_5 : L.IsLocalizedEquivalence (W₁ := W₁) (W₂ := W₁')
inst_6 : R.IsLocalizedEquivalence (W₁ := W₂) (W₂ := W₂')
inst_7 : R.functor (W₁ := W₂) (W₂ := W₂').EssSurj
inst_8 : L.functor (W₁ := W₁) (W₂ := W₁').EssSurj
inst_9 : R.functor (W₁ := W₂) (W₂ := W₂').Full
inst_10 : R.IsInduced (W₁ := W₂) (W₂ := W₂')
iso :
  T.functor (W₁ := W₁) (W₂ := W₂) ⋙ R.functor (W₁ := W₂) (W₂ := W₂') ≅
    L.functor (W₁ := W₁) (W₂ := W₁') ⋙ B.functor (W₁ := W₁') (W₂ := W₂')
inst_11 : TwoSquare.GuitartExact iso.inv
h : B.IsLeftDerivabilityStructure (W₁ := W₁') (W₂ := W₂')
this_1 : T.HasLeftResolutions (W₁ := W₁) (W₂ := W₂)
F : W₁'.Localization ⥤ W₂'.Localization := B.localizedFunctor (W₁ := W₁') (W₂ := W₂') W₁'.Q W₂'.Q
e' : B.functor (W₁ := W₁') (W₂ := W₂') ⋙ W₂'.Q ≅ W₁'.Q ⋙ F :=
  CatCommSq.iso (B.functor (W₁ := W₁') (W₂ := W₂')) W₁'.Q W₂'.Q F
e : T.functor (W₁ := W₁) (W₂ := W₂) ⋙ R.functor (W₁ := W₂) (W₂ := W₂') ⋙ W₂'.Q ≅
  (L.functor (W₁ := W₁) (W₂ := W₁') ⋙ W₁'.Q) ⋙ F :=
  (T.functor (W₁ := W₁) (W₂ := W₂).associator (R.functor (W₁ := W₂) (W₂ := W₂')) W₂'.Q).symm ≪≫
    Functor.isoWhiskerRight iso W₂'.Q ≪≫
      L.functor (W₁ := W₁) (W₂ := W₁').associator (B.functor (W₁ := W₁') (W₂ := W₂')) W₂'.Q ≪≫
        L.functor (W₁ := W₁) (W₂ := W₁').isoWhiskerLeft e' ≪≫ (L.functor (W₁ := W₁) (W₂ := W₁').associator W₁'.Q F).symm
he' : TwoSquare.GuitartExact e'.inv
this : TwoSquare.hComp iso.inv e'.inv = e.inv
⊢ (TwoSquare.hComp iso.inv e'.inv).GuitartExact

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.OfLocalizedEquivalences
Goal:
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} D₁
inst_3 : Category.{v_4, u_4} D₂
W₁ : MorphismProperty.{v_1, u_1} C₁
W₁' : MorphismProperty.{v_3, u_3} D₁
W₂ : MorphismProperty.{v_2, u_2} C₂
W₂' : MorphismProperty.{v_4, u_4} D₂
T : LocalizerMorphism W₁ W₂
L : LocalizerMorphism W₁ W₁'
R : LocalizerMorphism W₂ W₂'
B : LocalizerMorphism W₁' W₂'
inst_4 : W₂'.RespectsIso
inst_5 : L.IsLocalizedEquivalence (W₁ := W₁) (W₂ := W₁')
inst_6 : R.IsLocalizedEquivalence (W₁ := W₂) (W₂ := W₂')
inst_7 : R.functor (W₁ := W₂) (W₂ := W₂').EssSurj
inst_8 : T.IsRightDerivabilityStructure (W₁ := W₁) (W₂ := W₂)
iso :
  T.functor (W₁ := W₁) (W₂ := W₂) ⋙ R.functor (W₁ := W₂) (W₂ := W₂') ≅
    L.functor (W₁ := W₁) (W₂ := W₁') ⋙ B.functor (W₁ := W₁') (W₂ := W₂')
inst_9 : TwoSquare.GuitartExact iso.hom
rw : B.op (W₁ := W₁') (W₂ := W₂').IsLeftDerivabilityStructure (W₁ := W₁'.op) (W₂ := W₂'.op)
⊢ B.IsRightDerivabilityStructure (W₁ := W₁') (W₂ := W₂')

Tactic:
rw [isRightDerivabilityStructure_iff_op]

Premises used: CategoryTheory.LocalizerMorphism.isRightDerivabilityStructure_iff_op
-- Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.OfLocalizedEquivalences
Goal:
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} D₁
inst_3 : Category.{v_4, u_4} D₂
W₁ : MorphismProperty.{v_1, u_1} C₁
W₁' : MorphismProperty.{v_3, u_3} D₁
W₂ : MorphismProperty.{v_2, u_2} C₂
W₂' : MorphismProperty.{v_4, u_4} D₂
T : LocalizerMorphism W₁ W₂
L : LocalizerMorphism W₁ W₁'
R : LocalizerMorphism W₂ W₂'
B : LocalizerMorphism W₁' W₂'
inst_4 : W₂'.RespectsIso
inst_5 : L.IsLocalizedEquivalence (W₁ := W₁) (W₂ := W₁')
inst_6 : R.IsLocalizedEquivalence (W₁ := W₂) (W₂ := W₂')
inst_7 : R.functor (W₁ := W₂) (W₂ := W₂').EssSurj
inst_8 : T.IsRightDerivabilityStructure (W₁ := W₁) (W₂ := W₂)
iso :
  T.functor (W₁ := W₁) (W₂ := W₂) ⋙ R.functor (W₁ := W₂) (W₂ := W₂') ≅
    L.functor (W₁ := W₁) (W₂ := W₁') ⋙ B.functor (W₁ := W₁') (W₂ := W₂')
inst_9 : TwoSquare.GuitartExact iso.hom
iso' : T.op (W₁ := W₁) (W₂ := W₂).functor (W₁ := W₁.op) (W₂ := W₂.op) ⋙
    R.op (W₁ := W₂) (W₂ := W₂').functor (W₁ := W₂.op) (W₂ := W₂'.op) ≅
  L.op (W₁ := W₁) (W₂ := W₁').functor (W₁ := W₁.op) (W₂ := W₁'.op) ⋙
    B.op (W₁ := W₁') (W₂ := W₂').functor (W₁ := W₁'.op) (W₂ := W₂'.op) :=
  NatIso.op iso.symm
⊢ TwoSquare.GuitartExact iso'.inv

Tactic:
have : TwoSquare.GuitartExact iso'.inv :=
    inferInstanceAs (TwoSquare.op iso.hom).GuitartExact
-- Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.OfLocalizedEquivalences
Goal:
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} D₁
inst_3 : Category.{v_4, u_4} D₂
W₁ : MorphismProperty.{v_1, u_1} C₁
W₁' : MorphismProperty.{v_3, u_3} D₁
W₂ : MorphismProperty.{v_2, u_2} C₂
W₂' : MorphismProperty.{v_4, u_4} D₂
T : LocalizerMorphism W₁ W₂
L : LocalizerMorphism W₁ W₁'
R : LocalizerMorphism W₂ W₂'
B : LocalizerMorphism W₁' W₂'
inst_4 : W₂'.RespectsIso
inst_5 : L.IsLocalizedEquivalence (W₁ := W₁) (W₂ := W₁')
inst_6 : R.IsLocalizedEquivalence (W₁ := W₂) (W₂ := W₂')
inst_7 : R.functor (W₁ := W₂) (W₂ := W₂').EssSurj
inst_8 : T.IsRightDerivabilityStructure (W₁ := W₁) (W₂ := W₂)
iso :
  T.functor (W₁ := W₁) (W₂ := W₂) ⋙ R.functor (W₁ := W₂) (W₂ := W₂') ≅
    L.functor (W₁ := W₁) (W₂ := W₁') ⋙ B.functor (W₁ := W₁') (W₂ := W₂')
inst_9 : TwoSquare.GuitartExact iso.hom
iso' : T.op (W₁ := W₁) (W₂ := W₂).functor (W₁ := W₁.op) (W₂ := W₂.op) ⋙
    R.op (W₁ := W₂) (W₂ := W₂').functor (W₁ := W₂.op) (W₂ := W₂'.op) ≅
  L.op (W₁ := W₁) (W₂ := W₁').functor (W₁ := W₁.op) (W₂ := W₁'.op) ⋙
    B.op (W₁ := W₁') (W₂ := W₂').functor (W₁ := W₁'.op) (W₂ := W₂'.op) :=
  NatIso.op iso.symm
this : TwoSquare.GuitartExact iso'.inv
⊢ B.op (W₁ := W₁') (W₂ := W₂').IsLeftDerivabilityStructure (W₁ := W₁'.op) (W₂ := W₂'.op)

Tactic:
isLeftDerivabilityStructure_of_isLocalizedEquivalence iso'

Premises used: CategoryTheory.LocalizerMorphism.isLeftDerivabilityStructure_of_isLocalizedEquivalence
-- Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.OfLocalizedEquivalences
Goal:
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} D₁
inst_3 : Category.{v_4, u_4} D₂
W₁ : MorphismProperty.{v_1, u_1} C₁
W₁' : MorphismProperty.{v_3, u_3} D₁
W₂ : MorphismProperty.{v_2, u_2} C₂
W₂' : MorphismProperty.{v_4, u_4} D₂
T : LocalizerMorphism W₁ W₂
L : LocalizerMorphism W₁ W₁'
R : LocalizerMorphism W₂ W₂'
B : LocalizerMorphism W₁' W₂'
inst_4 : W₂'.RespectsIso
inst_5 : L.IsLocalizedEquivalence (W₁ := W₁) (W₂ := W₁')
inst_6 : R.IsLocalizedEquivalence (W₁ := W₂) (W₂ := W₂')
inst_7 : R.functor (W₁ := W₂) (W₂ := W₂').EssSurj
inst_8 : T.IsRightDerivabilityStructure (W₁ := W₁) (W₂ := W₂)
iso :
  T.functor (W₁ := W₁) (W₂ := W₂) ⋙ R.functor (W₁ := W₂) (W₂ := W₂') ≅
    L.functor (W₁ := W₁) (W₂ := W₁') ⋙ B.functor (W₁ := W₁') (W₂ := W₂')
inst_9 : TwoSquare.GuitartExact iso.hom
iso' : T.op (W₁ := W₁) (W₂ := W₂).functor (W₁ := W₁.op) (W₂ := W₂.op) ⋙
    R.op (W₁ := W₂) (W₂ := W₂').functor (W₁ := W₂.op) (W₂ := W₂'.op) ≅
  L.op (W₁ := W₁) (W₂ := W₁').functor (W₁ := W₁.op) (W₂ := W₁'.op) ⋙
    B.op (W₁ := W₁') (W₂ := W₂').functor (W₁ := W₁'.op) (W₂ := W₂'.op) :=
  NatIso.op iso.symm
this : TwoSquare.GuitartExact iso'.inv
⊢ B.op (W₁ := W₁') (W₂ := W₂').IsLeftDerivabilityStructure (W₁ := W₁'.op) (W₂ := W₂'.op)

Tactic:
exact isLeftDerivabilityStructure_of_isLocalizedEquivalence iso'

Premises used: CategoryTheory.LocalizerMorphism.isLeftDerivabilityStructure_of_isLocalizedEquivalence
-- Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.OfLocalizedEquivalences
Goal:
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} D₁
inst_3 : Category.{v_4, u_4} D₂
W₁ : MorphismProperty.{v_1, u_1} C₁
W₁' : MorphismProperty.{v_3, u_3} D₁
W₂ : MorphismProperty.{v_2, u_2} C₂
W₂' : MorphismProperty.{v_4, u_4} D₂
T : LocalizerMorphism W₁ W₂
L : LocalizerMorphism W₁ W₁'
R : LocalizerMorphism W₂ W₂'
B : LocalizerMorphism W₁' W₂'
inst_4 : W₂'.RespectsIso
inst_5 : L.IsLocalizedEquivalence (W₁ := W₁) (W₂ := W₁')
inst_6 : R.IsLocalizedEquivalence (W₁ := W₂) (W₂ := W₂')
inst_7 : R.functor (W₁ := W₂) (W₂ := W₂').EssSurj
inst_8 : L.functor (W₁ := W₁) (W₂ := W₁').EssSurj
inst_9 : R.functor (W₁ := W₂) (W₂ := W₂').Full
inst_10 : R.IsInduced (W₁ := W₂) (W₂ := W₂')
iso :
  T.functor (W₁ := W₁) (W₂ := W₂) ⋙ R.functor (W₁ := W₂) (W₂ := W₂') ≅
    L.functor (W₁ := W₁) (W₂ := W₁') ⋙ B.functor (W₁ := W₁') (W₂ := W₂')
inst_11 : TwoSquare.GuitartExact iso.hom
simp :
  T.op (W₁ := W₁) (W₂ := W₂).IsLeftDerivabilityStructure (W₁ := W₁.op) (W₂ := W₂.op) ↔
    B.op (W₁ := W₁') (W₂ := W₂').IsLeftDerivabilityStructure (W₁ := W₁'.op) (W₂ := W₂'.op)
⊢ T.IsRightDerivabilityStructure (W₁ := W₁) (W₂ := W₂) ↔ B.IsRightDerivabilityStructure (W₁ := W₁') (W₂ := W₂')

Tactic:
simp only [isRightDerivabilityStructure_iff_op]

Premises used: CategoryTheory.LocalizerMorphism.isRightDerivabilityStructure_iff_op
-- Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.OfLocalizedEquivalences
Goal:
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} D₁
inst_3 : Category.{v_4, u_4} D₂
W₁ : MorphismProperty.{v_1, u_1} C₁
W₁' : MorphismProperty.{v_3, u_3} D₁
W₂ : MorphismProperty.{v_2, u_2} C₂
W₂' : MorphismProperty.{v_4, u_4} D₂
T : LocalizerMorphism W₁ W₂
L : LocalizerMorphism W₁ W₁'
R : LocalizerMorphism W₂ W₂'
B : LocalizerMorphism W₁' W₂'
inst_4 : W₂'.RespectsIso
inst_5 : L.IsLocalizedEquivalence (W₁ := W₁) (W₂ := W₁')
inst_6 : R.IsLocalizedEquivalence (W₁ := W₂) (W₂ := W₂')
inst_7 : R.functor (W₁ := W₂) (W₂ := W₂').EssSurj
inst_8 : L.functor (W₁ := W₁) (W₂ := W₁').EssSurj
inst_9 : R.functor (W₁ := W₂) (W₂ := W₂').Full
inst_10 : R.IsInduced (W₁ := W₂) (W₂ := W₂')
iso :
  T.functor (W₁ := W₁) (W₂ := W₂) ⋙ R.functor (W₁ := W₂) (W₂ := W₂') ≅
    L.functor (W₁ := W₁) (W₂ := W₁') ⋙ B.functor (W₁ := W₁') (W₂ := W₂')
inst_11 : TwoSquare.GuitartExact iso.hom
iso' : T.op (W₁ := W₁) (W₂ := W₂).functor (W₁ := W₁.op) (W₂ := W₂.op) ⋙
    R.op (W₁ := W₂) (W₂ := W₂').functor (W₁ := W₂.op) (W₂ := W₂'.op) ≅
  L.op (W₁ := W₁) (W₂ := W₁').functor (W₁ := W₁.op) (W₂ := W₁'.op) ⋙
    B.op (W₁ := W₁') (W₂ := W₂').functor (W₁ := W₁'.op) (W₂ := W₂'.op) :=
  NatIso.op iso.symm
⊢ TwoSquare.GuitartExact iso'.inv

Tactic:
have : TwoSquare.GuitartExact iso'.inv :=
    inferInstanceAs (TwoSquare.op iso.hom).GuitartExact