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.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
⊢ 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)

Tactic:
isLeftDerivabilityStructure_iff_of_isLocalizedEquivalence iso'

Premises used: CategoryTheory.LocalizerMorphism.isLeftDerivabilityStructure_iff_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
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
⊢ 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)

Tactic:
exact isLeftDerivabilityStructure_iff_of_isLocalizedEquivalence iso'

Premises used: CategoryTheory.LocalizerMorphism.isLeftDerivabilityStructure_iff_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 : W₂'.RespectsIso
inst_6 : L.IsInduced (W₁ := W₁) (W₂ := W₁')
inst_7 : L.functor (W₁ := W₁) (W₂ := W₁').IsEquivalence
inst_8 : R.IsInduced (W₁ := W₂) (W₂ := W₂')
inst_9 : R.functor (W₁ := W₂) (W₂ := W₂').IsEquivalence
inst_10 : T.IsLeftDerivabilityStructure (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₂')
⊢ L.IsLocalizedEquivalence (W₁ := W₁) (W₂ := W₁')

Tactic:
have := L.isLocalizedEquivalence_of_isInduced
-- 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 : W₂'.RespectsIso
inst_6 : L.IsInduced (W₁ := W₁) (W₂ := W₁')
inst_7 : L.functor (W₁ := W₁) (W₂ := W₁').IsEquivalence
inst_8 : R.IsInduced (W₁ := W₂) (W₂ := W₂')
inst_9 : R.functor (W₁ := W₂) (W₂ := W₂').IsEquivalence
inst_10 : T.IsLeftDerivabilityStructure (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₂')
this : L.IsLocalizedEquivalence (W₁ := W₁) (W₂ := W₁')
⊢ R.IsLocalizedEquivalence (W₁ := W₂) (W₂ := W₂')

Tactic:
have := R.isLocalizedEquivalence_of_isInduced
-- 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 : W₂'.RespectsIso
inst_6 : L.IsInduced (W₁ := W₁) (W₂ := W₁')
inst_7 : L.functor (W₁ := W₁) (W₂ := W₁').IsEquivalence
inst_8 : R.IsInduced (W₁ := W₂) (W₂ := W₂')
inst_9 : R.functor (W₁ := W₂) (W₂ := W₂').IsEquivalence
inst_10 : T.IsLeftDerivabilityStructure (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₂')
this_1 : L.IsLocalizedEquivalence (W₁ := W₁) (W₂ := W₁')
this : R.IsLocalizedEquivalence (W₁ := W₂) (W₂ := W₂')
⊢ B.IsLeftDerivabilityStructure (W₁ := W₁') (W₂ := W₂')

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 : W₂'.RespectsIso
inst_6 : L.IsInduced (W₁ := W₁) (W₂ := W₁')
inst_7 : L.functor (W₁ := W₁) (W₂ := W₁').IsEquivalence
inst_8 : R.IsInduced (W₁ := W₂) (W₂ := W₂')
inst_9 : R.functor (W₁ := W₂) (W₂ := W₂').IsEquivalence
inst_10 : T.IsLeftDerivabilityStructure (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₂')
this_1 : L.IsLocalizedEquivalence (W₁ := W₁) (W₂ := W₁')
this : R.IsLocalizedEquivalence (W₁ := W₂) (W₂ := W₂')
⊢ B.IsLeftDerivabilityStructure (W₁ := W₁') (W₂ := W₂')

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 : W₂'.RespectsIso
inst_6 : L.IsInduced (W₁ := W₁) (W₂ := W₁')
inst_7 : L.functor (W₁ := W₁) (W₂ := W₁').IsEquivalence
inst_8 : R.IsInduced (W₁ := W₂) (W₂ := W₂')
inst_9 : R.functor (W₁ := W₂) (W₂ := W₂').IsEquivalence
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₂')
h : B.IsLeftDerivabilityStructure (W₁ := W₁') (W₂ := W₂')
e : B.functor (W₁ := W₁') (W₂ := W₂') ⋙ R.inv (W₁ := W₂) (W₂ := W₂').functor (W₁ := W₂') (W₂ := W₂) ≅
  L.inv (W₁ := W₁) (W₂ := W₁').functor (W₁ := W₁') (W₂ := W₁) ⋙ T.functor (W₁ := W₁) (W₂ := W₂) :=
  (B.functor (W₁ := W₁') (W₂ := W₂') ⋙ R.inv (W₁ := W₂) (W₂ := W₂').functor (W₁ := W₂') (W₂ := W₂)).leftUnitor.symm ≪≫
    isoWhiskerRight L.functor (W₁ := W₁) (W₂ := W₁').asEquivalence.counitIso.symm
        (B.functor (W₁ := W₁') (W₂ := W₂') ⋙ R.inv (W₁ := W₂) (W₂ := W₂').functor (W₁ := W₂') (W₂ := W₂)) ≪≫
      L.functor (W₁ := W₁) (W₂ := W₁').asEquivalence.inverse.associator
          L.functor (W₁ := W₁) (W₂ := W₁').asEquivalence.functor
          (B.functor (W₁ := W₁') (W₂ := W₂') ⋙ R.inv (W₁ := W₂) (W₂ := W₂').functor (W₁ := W₂') (W₂ := W₂)) ≪≫
        L.functor (W₁ := W₁) (W₂ := W₁').asEquivalence.inverse.isoWhiskerLeft
            (L.functor (W₁ := W₁) (W₂ := W₁').asEquivalence.functor.associator (B.functor (W₁ := W₁') (W₂ := W₂'))
                (R.inv (W₁ := W₂) (W₂ := W₂').functor (W₁ := W₂') (W₂ := W₂))).symm ≪≫
          L.functor (W₁ := W₁) (W₂ := W₁').asEquivalence.inverse.isoWhiskerLeft
              (isoWhiskerRight iso.symm (R.inv (W₁ := W₂) (W₂ := W₂').functor (W₁ := W₂') (W₂ := W₂))) ≪≫
            L.functor (W₁ := W₁) (W₂ := W₁').asEquivalence.inverse.isoWhiskerLeft
                (T.functor (W₁ := W₁) (W₂ := W₂).associator (R.functor (W₁ := W₂) (W₂ := W₂'))
                  (R.inv (W₁ := W₂) (W₂ := W₂').functor (W₁ := W₂') (W₂ := W₂))) ≪≫
              L.functor (W₁ := W₁) (W₂ := W₁').asEquivalence.inverse.isoWhiskerLeft
                  (T.functor (W₁ := W₁) (W₂ := W₂).isoWhiskerLeft
                    R.functor (W₁ := W₂) (W₂ := W₂').asEquivalence.unitIso.symm) ≪≫
                (L.functor (W₁ := W₁) (W₂ := W₁').asEquivalence.inverse.associator (T.functor (W₁ := W₁) (W₂ := W₂))
                      (𝟭 C₂)).symm ≪≫
                  (L.functor (W₁ := W₁) (W₂ := W₁').asEquivalence.inverse ⋙ T.functor (W₁ := W₁) (W₂ := W₂)).rightUnitor
rw : (W₁'.inverseImage (L.functor (W₁ := W₁) (W₂ := W₁'))).RespectsIso
⊢ W₁.RespectsIso

Tactic:
rw [← L.inverseImage_eq]

Premises used: CategoryTheory.LocalizerMorphism.IsInduced.inverseImage_eq
-- 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 : W₂'.RespectsIso
inst_6 : L.IsInduced (W₁ := W₁) (W₂ := W₁')
inst_7 : L.functor (W₁ := W₁) (W₂ := W₁').IsEquivalence
inst_8 : R.IsInduced (W₁ := W₂) (W₂ := W₂')
inst_9 : R.functor (W₁ := W₂) (W₂ := W₂').IsEquivalence
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₂')
h : B.IsLeftDerivabilityStructure (W₁ := W₁') (W₂ := W₂')
e : B.functor (W₁ := W₁') (W₂ := W₂') ⋙ R.inv (W₁ := W₂) (W₂ := W₂').functor (W₁ := W₂') (W₂ := W₂) ≅
  L.inv (W₁ := W₁) (W₂ := W₁').functor (W₁ := W₁') (W₂ := W₁) ⋙ T.functor (W₁ := W₁) (W₂ := W₂) :=
  (B.functor (W₁ := W₁') (W₂ := W₂') ⋙ R.inv (W₁ := W₂) (W₂ := W₂').functor (W₁ := W₂') (W₂ := W₂)).leftUnitor.symm ≪≫
    isoWhiskerRight L.functor (W₁ := W₁) (W₂ := W₁').asEquivalence.counitIso.symm
        (B.functor (W₁ := W₁') (W₂ := W₂') ⋙ R.inv (W₁ := W₂) (W₂ := W₂').functor (W₁ := W₂') (W₂ := W₂)) ≪≫
      L.functor (W₁ := W₁) (W₂ := W₁').asEquivalence.inverse.associator
          L.functor (W₁ := W₁) (W₂ := W₁').asEquivalence.functor
          (B.functor (W₁ := W₁') (W₂ := W₂') ⋙ R.inv (W₁ := W₂) (W₂ := W₂').functor (W₁ := W₂') (W₂ := W₂)) ≪≫
        L.functor (W₁ := W₁) (W₂ := W₁').asEquivalence.inverse.isoWhiskerLeft
            (L.functor (W₁ := W₁) (W₂ := W₁').asEquivalence.functor.associator (B.functor (W₁ := W₁') (W₂ := W₂'))
                (R.inv (W₁ := W₂) (W₂ := W₂').functor (W₁ := W₂') (W₂ := W₂))).symm ≪≫
          L.functor (W₁ := W₁) (W₂ := W₁').asEquivalence.inverse.isoWhiskerLeft
              (isoWhiskerRight iso.symm (R.inv (W₁ := W₂) (W₂ := W₂').functor (W₁ := W₂') (W₂ := W₂))) ≪≫
            L.functor (W₁ := W₁) (W₂ := W₁').asEquivalence.inverse.isoWhiskerLeft
                (T.functor (W₁ := W₁) (W₂ := W₂).associator (R.functor (W₁ := W₂) (W₂ := W₂'))
                  (R.inv (W₁ := W₂) (W₂ := W₂').functor (W₁ := W₂') (W₂ := W₂))) ≪≫
              L.functor (W₁ := W₁) (W₂ := W₁').asEquivalence.inverse.isoWhiskerLeft
                  (T.functor (W₁ := W₁) (W₂ := W₂).isoWhiskerLeft
                    R.functor (W₁ := W₂) (W₂ := W₂').asEquivalence.unitIso.symm) ≪≫
                (L.functor (W₁ := W₁) (W₂ := W₁').asEquivalence.inverse.associator (T.functor (W₁ := W₁) (W₂ := W₂))
                      (𝟭 C₂)).symm ≪≫
                  (L.functor (W₁ := W₁) (W₂ := W₁').asEquivalence.inverse ⋙ T.functor (W₁ := W₁) (W₂ := W₂)).rightUnitor
⊢ (W₁'.inverseImage (L.functor (W₁ := W₁) (W₂ := W₁'))).RespectsIso

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 : W₂'.RespectsIso
inst_6 : L.IsInduced (W₁ := W₁) (W₂ := W₁')
inst_7 : L.functor (W₁ := W₁) (W₂ := W₁').IsEquivalence
inst_8 : R.IsInduced (W₁ := W₂) (W₂ := W₂')
inst_9 : R.functor (W₁ := W₂) (W₂ := W₂').IsEquivalence
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₂')
h : B.IsLeftDerivabilityStructure (W₁ := W₁') (W₂ := W₂')
e : B.functor (W₁ := W₁') (W₂ := W₂') ⋙ R.inv (W₁ := W₂) (W₂ := W₂').functor (W₁ := W₂') (W₂ := W₂) ≅
  L.inv (W₁ := W₁) (W₂ := W₁').functor (W₁ := W₁') (W₂ := W₁) ⋙ T.functor (W₁ := W₁) (W₂ := W₂) :=
  (B.functor (W₁ := W₁') (W₂ := W₂') ⋙ R.inv (W₁ := W₂) (W₂ := W₂').functor (W₁ := W₂') (W₂ := W₂)).leftUnitor.symm ≪≫
    isoWhiskerRight L.functor (W₁ := W₁) (W₂ := W₁').asEquivalence.counitIso.symm
        (B.functor (W₁ := W₁') (W₂ := W₂') ⋙ R.inv (W₁ := W₂) (W₂ := W₂').functor (W₁ := W₂') (W₂ := W₂)) ≪≫
      L.functor (W₁ := W₁) (W₂ := W₁').asEquivalence.inverse.associator
          L.functor (W₁ := W₁) (W₂ := W₁').asEquivalence.functor
          (B.functor (W₁ := W₁') (W₂ := W₂') ⋙ R.inv (W₁ := W₂) (W₂ := W₂').functor (W₁ := W₂') (W₂ := W₂)) ≪≫
        L.functor (W₁ := W₁) (W₂ := W₁').asEquivalence.inverse.isoWhiskerLeft
            (L.functor (W₁ := W₁) (W₂ := W₁').asEquivalence.functor.associator (B.functor (W₁ := W₁') (W₂ := W₂'))
                (R.inv (W₁ := W₂) (W₂ := W₂').functor (W₁ := W₂') (W₂ := W₂))).symm ≪≫
          L.functor (W₁ := W₁) (W₂ := W₁').asEquivalence.inverse.isoWhiskerLeft
              (isoWhiskerRight iso.symm (R.inv (W₁ := W₂) (W₂ := W₂').functor (W₁ := W₂') (W₂ := W₂))) ≪≫
            L.functor (W₁ := W₁) (W₂ := W₁').asEquivalence.inverse.isoWhiskerLeft
                (T.functor (W₁ := W₁) (W₂ := W₂).associator (R.functor (W₁ := W₂) (W₂ := W₂'))
                  (R.inv (W₁ := W₂) (W₂ := W₂').functor (W₁ := W₂') (W₂ := W₂))) ≪≫
              L.functor (W₁ := W₁) (W₂ := W₁').asEquivalence.inverse.isoWhiskerLeft
                  (T.functor (W₁ := W₁) (W₂ := W₂).isoWhiskerLeft
                    R.functor (W₁ := W₂) (W₂ := W₂').asEquivalence.unitIso.symm) ≪≫
                (L.functor (W₁ := W₁) (W₂ := W₁').asEquivalence.inverse.associator (T.functor (W₁ := W₁) (W₂ := W₂))
                      (𝟭 C₂)).symm ≪≫
                  (L.functor (W₁ := W₁) (W₂ := W₁').asEquivalence.inverse ⋙ T.functor (W₁ := W₁) (W₂ := W₂)).rightUnitor
⊢ W₁.RespectsIso

Tactic:
have : W₁.RespectsIso := by rw [← L.inverseImage_eq]; 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 : W₂'.RespectsIso
inst_6 : L.IsInduced (W₁ := W₁) (W₂ := W₁')
inst_7 : L.functor (W₁ := W₁) (W₂ := W₁').IsEquivalence
inst_8 : R.IsInduced (W₁ := W₂) (W₂ := W₂')
inst_9 : R.functor (W₁ := W₂) (W₂ := W₂').IsEquivalence
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₂')
h : B.IsLeftDerivabilityStructure (W₁ := W₁') (W₂ := W₂')
e : B.functor (W₁ := W₁') (W₂ := W₂') ⋙ R.inv (W₁ := W₂) (W₂ := W₂').functor (W₁ := W₂') (W₂ := W₂) ≅
  L.inv (W₁ := W₁) (W₂ := W₁').functor (W₁ := W₁') (W₂ := W₁) ⋙ T.functor (W₁ := W₁) (W₂ := W₂) :=
  (B.functor (W₁ := W₁') (W₂ := W₂') ⋙ R.inv (W₁ := W₂) (W₂ := W₂').functor (W₁ := W₂') (W₂ := W₂)).leftUnitor.symm ≪≫
    isoWhiskerRight L.functor (W₁ := W₁) (W₂ := W₁').asEquivalence.counitIso.symm
        (B.functor (W₁ := W₁') (W₂ := W₂') ⋙ R.inv (W₁ := W₂) (W₂ := W₂').functor (W₁ := W₂') (W₂ := W₂)) ≪≫
      L.functor (W₁ := W₁) (W₂ := W₁').asEquivalence.inverse.associator
          L.functor (W₁ := W₁) (W₂ := W₁').asEquivalence.functor
          (B.functor (W₁ := W₁') (W₂ := W₂') ⋙ R.inv (W₁ := W₂) (W₂ := W₂').functor (W₁ := W₂') (W₂ := W₂)) ≪≫
        L.functor (W₁ := W₁) (W₂ := W₁').asEquivalence.inverse.isoWhiskerLeft
            (L.functor (W₁ := W₁) (W₂ := W₁').asEquivalence.functor.associator (B.functor (W₁ := W₁') (W₂ := W₂'))
                (R.inv (W₁ := W₂) (W₂ := W₂').functor (W₁ := W₂') (W₂ := W₂))).symm ≪≫
          L.functor (W₁ := W₁) (W₂ := W₁').asEquivalence.inverse.isoWhiskerLeft
              (isoWhiskerRight iso.symm (R.inv (W₁ := W₂) (W₂ := W₂').functor (W₁ := W₂') (W₂ := W₂))) ≪≫
            L.functor (W₁ := W₁) (W₂ := W₁').asEquivalence.inverse.isoWhiskerLeft
                (T.functor (W₁ := W₁) (W₂ := W₂).associator (R.functor (W₁ := W₂) (W₂ := W₂'))
                  (R.inv (W₁ := W₂) (W₂ := W₂').functor (W₁ := W₂') (W₂ := W₂))) ≪≫
              L.functor (W₁ := W₁) (W₂ := W₁').asEquivalence.inverse.isoWhiskerLeft
                  (T.functor (W₁ := W₁) (W₂ := W₂).isoWhiskerLeft
                    R.functor (W₁ := W₂) (W₂ := W₂').asEquivalence.unitIso.symm) ≪≫
                (L.functor (W₁ := W₁) (W₂ := W₁').asEquivalence.inverse.associator (T.functor (W₁ := W₁) (W₂ := W₂))
                      (𝟭 C₂)).symm ≪≫
                  (L.functor (W₁ := W₁) (W₂ := W₁').asEquivalence.inverse ⋙ T.functor (W₁ := W₁) (W₂ := W₂)).rightUnitor
this : W₁.RespectsIso
⊢ (W₂'.inverseImage (R.functor (W₁ := W₂) (W₂ := W₂'))).RespectsIso

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 : W₂'.RespectsIso
inst_6 : L.IsInduced (W₁ := W₁) (W₂ := W₁')
inst_7 : L.functor (W₁ := W₁) (W₂ := W₁').IsEquivalence
inst_8 : R.IsInduced (W₁ := W₂) (W₂ := W₂')
inst_9 : R.functor (W₁ := W₂) (W₂ := W₂').IsEquivalence
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₂')
h : B.IsLeftDerivabilityStructure (W₁ := W₁') (W₂ := W₂')
e : B.functor (W₁ := W₁') (W₂ := W₂') ⋙ R.inv (W₁ := W₂) (W₂ := W₂').functor (W₁ := W₂') (W₂ := W₂) ≅
  L.inv (W₁ := W₁) (W₂ := W₁').functor (W₁ := W₁') (W₂ := W₁) ⋙ T.functor (W₁ := W₁) (W₂ := W₂) :=
  (B.functor (W₁ := W₁') (W₂ := W₂') ⋙ R.inv (W₁ := W₂) (W₂ := W₂').functor (W₁ := W₂') (W₂ := W₂)).leftUnitor.symm ≪≫
    isoWhiskerRight L.functor (W₁ := W₁) (W₂ := W₁').asEquivalence.counitIso.symm
        (B.functor (W₁ := W₁') (W₂ := W₂') ⋙ R.inv (W₁ := W₂) (W₂ := W₂').functor (W₁ := W₂') (W₂ := W₂)) ≪≫
      L.functor (W₁ := W₁) (W₂ := W₁').asEquivalence.inverse.associator
          L.functor (W₁ := W₁) (W₂ := W₁').asEquivalence.functor
          (B.functor (W₁ := W₁') (W₂ := W₂') ⋙ R.inv (W₁ := W₂) (W₂ := W₂').functor (W₁ := W₂') (W₂ := W₂)) ≪≫
        L.functor (W₁ := W₁) (W₂ := W₁').asEquivalence.inverse.isoWhiskerLeft
            (L.functor (W₁ := W₁) (W₂ := W₁').asEquivalence.functor.associator (B.functor (W₁ := W₁') (W₂ := W₂'))
                (R.inv (W₁ := W₂) (W₂ := W₂').functor (W₁ := W₂') (W₂ := W₂))).symm ≪≫
          L.functor (W₁ := W₁) (W₂ := W₁').asEquivalence.inverse.isoWhiskerLeft
              (isoWhiskerRight iso.symm (R.inv (W₁ := W₂) (W₂ := W₂').functor (W₁ := W₂') (W₂ := W₂))) ≪≫
            L.functor (W₁ := W₁) (W₂ := W₁').asEquivalence.inverse.isoWhiskerLeft
                (T.functor (W₁ := W₁) (W₂ := W₂).associator (R.functor (W₁ := W₂) (W₂ := W₂'))
                  (R.inv (W₁ := W₂) (W₂ := W₂').functor (W₁ := W₂') (W₂ := W₂))) ≪≫
              L.functor (W₁ := W₁) (W₂ := W₁').asEquivalence.inverse.isoWhiskerLeft
                  (T.functor (W₁ := W₁) (W₂ := W₂).isoWhiskerLeft
                    R.functor (W₁ := W₂) (W₂ := W₂').asEquivalence.unitIso.symm) ≪≫
                (L.functor (W₁ := W₁) (W₂ := W₁').asEquivalence.inverse.associator (T.functor (W₁ := W₁) (W₂ := W₂))
                      (𝟭 C₂)).symm ≪≫
                  (L.functor (W₁ := W₁) (W₂ := W₁').asEquivalence.inverse ⋙ T.functor (W₁ := W₁) (W₂ := W₂)).rightUnitor
this : W₁.RespectsIso
⊢ W₂.RespectsIso

Tactic:
have : W₂.RespectsIso := by rw [← R.inverseImage_eq]; infer_instance