-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.DerivabilityStructure.OfLocalizedEquivalences (hypothesis)
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
⊢ T.IsLeftDerivabilityStructure (W₁ := W₁) (W₂ := W₂)
have this₁ : W₂.RespectsIso
Tactic: have : W₂.RespectsIso := by rw [← R.inverseImage_eq]; infer_instance