Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.OfLocalizedEquivalences

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝⁹ : Category.{v_1, u_1} C₁
inst✝⁸ : Category.{v_2, u_2} C₂
inst✝⁷ : Category.{v_3, u_3} D₁
inst✝⁶ : Category.{v_4, u_4} D₂
W₁ : MorphismProperty C₁
W₁' : MorphismProperty D₁
W₂ : MorphismProperty C₂
W₂' : MorphismProperty D₂
T : LocalizerMorphism W₁ W₂
L : LocalizerMorphism W₁ W₁'
R : LocalizerMorphism W₂ W₂'
B : LocalizerMorphism W₁' W₂'
inst✝⁵ : W₁'.RespectsIso
inst✝⁴ : W₂'.RespectsIso
inst✝³ : L.IsInduced
inst✝² : L.functor.IsEquivalence
inst✝¹ : R.IsInduced
inst✝ : R.functor.IsEquivalence
iso : T.functor ⋙ R.functor ≅ L.functor ⋙ B.functor
x✝ : B.IsLeftDerivabilityStructure
e : B.functor ⋙ R.inv.functor ≅ L.inv.functor ⋙ T.functor :=
  (B.functor ⋙ R.inv.functor).leftUnitor.symm ≪≫
    isoWhiskerRight L.functor.asEquivalence.counitIso.symm (B.functor ⋙ R.inv.functor) ≪≫
      L.functor.asEquivalence.inverse.associator L.functor.asEquivalence.functor (B.functor ⋙ R.inv.functor) ≪≫
        L.functor.asEquivalence.inverse.isoWhiskerLeft
            (L.functor.asEquivalence.functor.associator B.functor R.inv.functor).symm ≪≫
          L.functor.asEquivalence.inverse.isoWhiskerLeft (isoWhiskerRight iso.symm R.inv.functor) ≪≫
            L.functor.asEquivalence.inverse.isoWhiskerLeft (T.functor.associator R.functor R.inv.functor) ≪≫
              L.functor.asEquivalence.inverse.isoWhiskerLeft
                  (T.functor.isoWhiskerLeft R.functor.asEquivalence.unitIso.symm) ≪≫
                (L.functor.asEquivalence.inverse.associator T.functor (𝟭 C₂)).symm ≪≫
                  (L.functor.asEquivalence.inverse ⋙ T.functor).rightUnitor
this : W₁.RespectsIso
⊢ T.IsLeftDerivabilityStructure

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

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝⁹ : Category.{v_1, u_1} C₁
inst✝⁸ : Category.{v_2, u_2} C₂
inst✝⁷ : Category.{v_3, u_3} D₁
inst✝⁶ : Category.{v_4, u_4} D₂
W₁ : MorphismProperty C₁
W₁' : MorphismProperty D₁
W₂ : MorphismProperty C₂
W₂' : MorphismProperty D₂
T : LocalizerMorphism W₁ W₂
L : LocalizerMorphism W₁ W₁'
R : LocalizerMorphism W₂ W₂'
B : LocalizerMorphism W₁' W₂'
inst✝⁵ : W₁'.RespectsIso
inst✝⁴ : W₂'.RespectsIso
inst✝³ : L.IsInduced
inst✝² : L.functor.IsEquivalence
inst✝¹ : R.IsInduced
inst✝ : R.functor.IsEquivalence
iso : T.functor ⋙ R.functor ≅ L.functor ⋙ B.functor
x✝ : B.IsLeftDerivabilityStructure
e : B.functor ⋙ R.inv.functor ≅ L.inv.functor ⋙ T.functor :=
  (B.functor ⋙ R.inv.functor).leftUnitor.symm ≪≫
    isoWhiskerRight L.functor.asEquivalence.counitIso.symm (B.functor ⋙ R.inv.functor) ≪≫
      L.functor.asEquivalence.inverse.associator L.functor.asEquivalence.functor (B.functor ⋙ R.inv.functor) ≪≫
        L.functor.asEquivalence.inverse.isoWhiskerLeft
            (L.functor.asEquivalence.functor.associator B.functor R.inv.functor).symm ≪≫
          L.functor.asEquivalence.inverse.isoWhiskerLeft (isoWhiskerRight iso.symm R.inv.functor) ≪≫
            L.functor.asEquivalence.inverse.isoWhiskerLeft (T.functor.associator R.functor R.inv.functor) ≪≫
              L.functor.asEquivalence.inverse.isoWhiskerLeft
                  (T.functor.isoWhiskerLeft R.functor.asEquivalence.unitIso.symm) ≪≫
                (L.functor.asEquivalence.inverse.associator T.functor (𝟭 C₂)).symm ≪≫
                  (L.functor.asEquivalence.inverse ⋙ T.functor).rightUnitor
this✝ : W₁.RespectsIso
this : W₂.RespectsIso
⊢ T.IsLeftDerivabilityStructure