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 : 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₂')
inst_9 : TwoSquare.GuitartExact iso.inv
this_1 : B.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
iso' : CatCommSq (T.functor (W₁ := W₁) (W₂ := W₂)) (L.functor (W₁ := W₁) (W₂ := W₁')) (R.functor (W₁ := W₂) (W₂ := W₂'))
  (B.functor (W₁ := W₁') (W₂ := W₂')) :=
  { iso := iso }
this : CatCommSq (T.functor (W₁ := W₁) (W₂ := W₂)) (L.functor (W₁ := W₁) (W₂ := W₁') ⋙ W₁'.Q)
  (R.functor (W₁ := W₂) (W₂ := W₂') ⋙ W₂'.Q) F :=
  CatCommSq.vComp (L.functor (W₁ := W₁) (W₂ := W₁')) W₁'.Q (T.functor (W₁ := W₁) (W₂ := W₂))
    (B.functor (W₁ := W₁') (W₂ := W₂')) F (R.functor (W₁ := W₂) (W₂ := W₂')) W₂'.Q
h :
  ∀ (X : C₁),
    (TwoSquare.hComp iso.inv e'.inv).natTrans.app X =
      (TwoSquare.natTrans
            (CatCommSq.iso (T.functor (W₁ := W₁) (W₂ := W₂)) (L.functor (W₁ := W₁) (W₂ := W₁') ⋙ W₁'.Q)
                (R.functor (W₁ := W₂) (W₂ := W₂') ⋙ W₂'.Q) F).inv).app
        X
⊢ TwoSquare.hComp iso.inv e'.inv =
    (CatCommSq.iso (T.functor (W₁ := W₁) (W₂ := W₂)) (L.functor (W₁ := W₁) (W₂ := W₁') ⋙ W₁'.Q)
        (R.functor (W₁ := W₂) (W₂ := W₂') ⋙ W₂'.Q) F).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 : 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₂')
inst_9 : TwoSquare.GuitartExact iso.inv
this_1 : B.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
iso' : CatCommSq (T.functor (W₁ := W₁) (W₂ := W₂)) (L.functor (W₁ := W₁) (W₂ := W₁')) (R.functor (W₁ := W₂) (W₂ := W₂'))
  (B.functor (W₁ := W₁') (W₂ := W₂')) :=
  { iso := iso }
this : CatCommSq (T.functor (W₁ := W₁) (W₂ := W₂)) (L.functor (W₁ := W₁) (W₂ := W₁') ⋙ W₁'.Q)
  (R.functor (W₁ := W₂) (W₂ := W₂') ⋙ W₂'.Q) F :=
  CatCommSq.vComp (L.functor (W₁ := W₁) (W₂ := W₁')) W₁'.Q (T.functor (W₁ := W₁) (W₂ := W₂))
    (B.functor (W₁ := W₁') (W₂ := W₂')) F (R.functor (W₁ := W₂) (W₂ := W₂')) W₂'.Q
X : C₁
⊢ (TwoSquare.hComp iso.inv e'.inv).natTrans.app X =
    (TwoSquare.natTrans
          (CatCommSq.iso (T.functor (W₁ := W₁) (W₂ := W₂)) (L.functor (W₁ := W₁) (W₂ := W₁') ⋙ W₁'.Q)
              (R.functor (W₁ := W₂) (W₂ := W₂') ⋙ W₂'.Q) F).inv).app
      X

Tactic:
simp [e', CatCommSq.iso, iso']

Premises used: CategoryTheory.CatCommSq.iso
-- 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.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₂')
inst_9 : TwoSquare.GuitartExact iso.inv
this_1 : B.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
iso' : CatCommSq (T.functor (W₁ := W₁) (W₂ := W₂)) (L.functor (W₁ := W₁) (W₂ := W₁')) (R.functor (W₁ := W₂) (W₂ := W₂'))
  (B.functor (W₁ := W₁') (W₂ := W₂')) :=
  { iso := iso }
this : CatCommSq (T.functor (W₁ := W₁) (W₂ := W₂)) (L.functor (W₁ := W₁) (W₂ := W₁') ⋙ W₁'.Q)
  (R.functor (W₁ := W₂) (W₂ := W₂') ⋙ W₂'.Q) F :=
  CatCommSq.vComp (L.functor (W₁ := W₁) (W₂ := W₁')) W₁'.Q (T.functor (W₁ := W₁) (W₂ := W₂))
    (B.functor (W₁ := W₁') (W₂ := W₂')) F (R.functor (W₁ := W₂) (W₂ := W₂')) W₂'.Q
⊢ (TwoSquare.hComp iso.inv e'.inv).GuitartExact

Tactic:
have : (TwoSquare.hComp iso.inv e'.inv).GuitartExact := by
    convert!
      T.guitartExact_of_isLeftDerivabilityStructure' (L.functor ⋙ W₁'.Q) (R.functor ⋙ W₂'.Q) F
        (CatCommSq.iso _ _ _ _)
    ext
    simp [e', CatCommSq.iso, iso']
-- 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.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₂')
inst_9 : TwoSquare.GuitartExact iso.inv
this_1 : B.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
iso' : CatCommSq (T.functor (W₁ := W₁) (W₂ := W₂)) (L.functor (W₁ := W₁) (W₂ := W₁')) (R.functor (W₁ := W₂) (W₂ := W₂'))
  (B.functor (W₁ := W₁') (W₂ := W₂')) :=
  { iso := iso }
this_2 : CatCommSq (T.functor (W₁ := W₁) (W₂ := W₂)) (L.functor (W₁ := W₁) (W₂ := W₁') ⋙ W₁'.Q)
  (R.functor (W₁ := W₂) (W₂ := W₂') ⋙ W₂'.Q) F :=
  CatCommSq.vComp (L.functor (W₁ := W₁) (W₂ := W₁')) W₁'.Q (T.functor (W₁ := W₁) (W₂ := W₂))
    (B.functor (W₁ := W₁') (W₂ := W₂')) F (R.functor (W₁ := W₂) (W₂ := W₂')) W₂'.Q
this : (TwoSquare.hComp iso.inv e'.inv).GuitartExact
rw : TwoSquare.GuitartExact e'.inv
⊢ B.IsLeftDerivabilityStructure (W₁ := W₁') (W₂ := W₂')

Tactic:
rw [B.isLeftDerivabilityStructure_iff W₁'.Q W₂'.Q F e']

Premises used: CategoryTheory.MorphismProperty.Q, 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 : 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₂')
inst_9 : TwoSquare.GuitartExact iso.inv
this_1 : B.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
iso' : CatCommSq (T.functor (W₁ := W₁) (W₂ := W₂)) (L.functor (W₁ := W₁) (W₂ := W₁')) (R.functor (W₁ := W₂) (W₂ := W₂'))
  (B.functor (W₁ := W₁') (W₂ := W₂')) :=
  { iso := iso }
this_2 : CatCommSq (T.functor (W₁ := W₁) (W₂ := W₂)) (L.functor (W₁ := W₁) (W₂ := W₁') ⋙ W₁'.Q)
  (R.functor (W₁ := W₂) (W₂ := W₂') ⋙ W₂'.Q) F :=
  CatCommSq.vComp (L.functor (W₁ := W₁) (W₂ := W₁')) W₁'.Q (T.functor (W₁ := W₁) (W₂ := W₂))
    (B.functor (W₁ := W₁') (W₂ := W₂')) F (R.functor (W₁ := W₂) (W₂ := W₂')) W₂'.Q
this : (TwoSquare.hComp iso.inv e'.inv).GuitartExact
⊢ TwoSquare.GuitartExact e'.inv

Tactic:
apply TwoSquare.GuitartExact.of_hComp iso.inv

Premises used: CategoryTheory.TwoSquare.GuitartExact.of_hComp, CategoryTheory.Iso.inv
-- 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
⊢ T.IsLeftDerivabilityStructure (W₁ := W₁) (W₂ := W₂) ↔ B.IsLeftDerivabilityStructure (W₁ := W₁') (W₂ := W₂')

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

Premises used: CategoryTheory.LocalizerMorphism.isLeftDerivabilityStructure_of_isLocalizedEquivalence, Iff.intro
-- 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
refine : B.IsLeftDerivabilityStructure (W₁ := W₁') (W₂ := W₂') → T.IsLeftDerivabilityStructure (W₁ := W₁) (W₂ := W₂)
⊢ T.IsLeftDerivabilityStructure (W₁ := W₁) (W₂ := W₂) ↔ B.IsLeftDerivabilityStructure (W₁ := W₁') (W₂ := W₂')

Tactic:
refine ⟨fun _ ↦ isLeftDerivabilityStructure_of_isLocalizedEquivalence iso, fun _ ↦ ?_⟩
-- 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₂')
X₂ : C₂
ρ : B.LeftResolution (W₁ := W₁') (W₂ := W₂') (R.functor (W₁ := W₂) (W₂ := W₂').obj X₂) :=
  Classical.arbitrary (B.LeftResolution (W₁ := W₁') (W₂ := W₂') (R.functor (W₁ := W₂) (W₂ := W₂').obj X₂))
simp :
  W₂' (X :=
    R.functor (W₁ := W₂) (W₂ := W₂').obj
      (T.functor (W₁ := W₁) (W₂ := W₂).obj
        (L.functor (W₁ := W₁) (W₂ := W₁').objPreimage (ρ.X₁ (W₁ := W₁') (W₂ := W₂')))))
    (iso.hom.app (L.functor (W₁ := W₁) (W₂ := W₁').objPreimage (ρ.X₁ (W₁ := W₁') (W₂ := W₂'))) ≫
      B.functor (W₁ := W₁') (W₂ := W₂').map
          (Iso.hom (L.functor (W₁ := W₁) (W₂ := W₁').objObjPreimageIso (ρ.X₁ (W₁ := W₁') (W₂ := W₂')))) ≫
        ρ.w (W₁ := W₁') (W₂ := W₂'))
⊢ W₂ (X :=
    T.functor (W₁ := W₁) (W₂ := W₂).obj (L.functor (W₁ := W₁) (W₂ := W₁').objPreimage (ρ.X₁ (W₁ := W₁') (W₂ := W₂'))))
    (R.functor (W₁ := W₂) (W₂ := W₂').preimage
      (iso.hom.app (L.functor (W₁ := W₁) (W₂ := W₁').objPreimage (ρ.X₁ (W₁ := W₁') (W₂ := W₂'))) ≫
        B.functor (W₁ := W₁') (W₂ := W₂').map
            (Iso.hom (L.functor (W₁ := W₁) (W₂ := W₁').objObjPreimageIso (ρ.X₁ (W₁ := W₁') (W₂ := W₂')))) ≫
          ρ.w (W₁ := W₁') (W₂ := W₂')))

Tactic:
simp only [← R.inverseImage_eq, Functor.comp_obj,
          MorphismProperty.inverseImage_iff, Functor.map_preimage]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.MorphismProperty.inverseImage_iff, CategoryTheory.LocalizerMorphism.IsInduced.inverseImage_eq, CategoryTheory.Functor.map_preimage
-- 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₂')
X₂ : C₂
ρ : B.LeftResolution (W₁ := W₁') (W₂ := W₂') (R.functor (W₁ := W₂) (W₂ := W₂').obj X₂) :=
  Classical.arbitrary (B.LeftResolution (W₁ := W₁') (W₂ := W₂') (R.functor (W₁ := W₂) (W₂ := W₂').obj X₂))
⊢ W₂' (X :=
    R.functor (W₁ := W₂) (W₂ := W₂').obj
      (T.functor (W₁ := W₁) (W₂ := W₂).obj
        (L.functor (W₁ := W₁) (W₂ := W₁').objPreimage (ρ.X₁ (W₁ := W₁') (W₂ := W₂')))))
    (iso.hom.app (L.functor (W₁ := W₁) (W₂ := W₁').objPreimage (ρ.X₁ (W₁ := W₁') (W₂ := W₂'))) ≫
      B.functor (W₁ := W₁') (W₂ := W₂').map
          (Iso.hom (L.functor (W₁ := W₁) (W₂ := W₁').objObjPreimageIso (ρ.X₁ (W₁ := W₁') (W₂ := W₂')))) ≫
        ρ.w (W₁ := W₁') (W₂ := W₂'))

Tactic:
(W₂'.arrow_mk_iso_iff ?_).2 ρ.hw

Premises used: Iff.mpr, CategoryTheory.MorphismProperty.arrow_mk_iso_iff, CategoryTheory.LocalizerMorphism.LeftResolution.hw
-- 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₂')
X₂ : C₂
ρ : B.LeftResolution (W₁ := W₁') (W₂ := W₂') (R.functor (W₁ := W₂) (W₂ := W₂').obj X₂) :=
  Classical.arbitrary (B.LeftResolution (W₁ := W₁') (W₂ := W₂') (R.functor (W₁ := W₂) (W₂ := W₂').obj X₂))
refine :
  Arrow.mk (X :=
      R.functor (W₁ := W₂) (W₂ := W₂').obj
        (T.functor (W₁ := W₁) (W₂ := W₂).obj
          (L.functor (W₁ := W₁) (W₂ := W₁').objPreimage (ρ.X₁ (W₁ := W₁') (W₂ := W₂')))))
      (iso.hom.app (L.functor (W₁ := W₁) (W₂ := W₁').objPreimage (ρ.X₁ (W₁ := W₁') (W₂ := W₂'))) ≫
        B.functor (W₁ := W₁') (W₂ := W₂').map
            (Iso.hom (L.functor (W₁ := W₁) (W₂ := W₁').objObjPreimageIso (ρ.X₁ (W₁ := W₁') (W₂ := W₂')))) ≫
          ρ.w (W₁ := W₁') (W₂ := W₂')) ≅
    Arrow.mk (ρ.w (W₁ := W₁') (W₂ := W₂'))
⊢ W₂' (X :=
    R.functor (W₁ := W₂) (W₂ := W₂').obj
      (T.functor (W₁ := W₁) (W₂ := W₂).obj
        (L.functor (W₁ := W₁) (W₂ := W₁').objPreimage (ρ.X₁ (W₁ := W₁') (W₂ := W₂')))))
    (iso.hom.app (L.functor (W₁ := W₁) (W₂ := W₁').objPreimage (ρ.X₁ (W₁ := W₁') (W₂ := W₂'))) ≫
      B.functor (W₁ := W₁') (W₂ := W₂').map
          (Iso.hom (L.functor (W₁ := W₁) (W₂ := W₁').objObjPreimageIso (ρ.X₁ (W₁ := W₁') (W₂ := W₂')))) ≫
        ρ.w (W₁ := W₁') (W₂ := W₂'))

Tactic:
refine (W₂'.arrow_mk_iso_iff ?_).2 ρ.hw

Premises used: Iff.mpr, CategoryTheory.MorphismProperty.arrow_mk_iso_iff, CategoryTheory.LocalizerMorphism.LeftResolution.hw
-- 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₂')
X₂ : C₂
ρ : B.LeftResolution (W₁ := W₁') (W₂ := W₂') (R.functor (W₁ := W₂) (W₂ := W₂').obj X₂) :=
  Classical.arbitrary (B.LeftResolution (W₁ := W₁') (W₂ := W₂') (R.functor (W₁ := W₂) (W₂ := W₂').obj X₂))
⊢ Arrow.mk (X :=
      R.functor (W₁ := W₂) (W₂ := W₂').obj
        (T.functor (W₁ := W₁) (W₂ := W₂).obj
          (L.functor (W₁ := W₁) (W₂ := W₁').objPreimage (ρ.X₁ (W₁ := W₁') (W₂ := W₂')))))
      (iso.hom.app (L.functor (W₁ := W₁) (W₂ := W₁').objPreimage (ρ.X₁ (W₁ := W₁') (W₂ := W₂'))) ≫
        B.functor (W₁ := W₁') (W₂ := W₂').map
            (Iso.hom (L.functor (W₁ := W₁) (W₂ := W₁').objObjPreimageIso (ρ.X₁ (W₁ := W₁') (W₂ := W₂')))) ≫
          ρ.w (W₁ := W₁') (W₂ := W₂')) ≅
    Arrow.mk (ρ.w (W₁ := W₁') (W₂ := W₂'))

Tactic:
exact Arrow.isoMk (iso.app _ ≪≫ B.functor.mapIso (L.functor.objObjPreimageIso ρ.X₁))
          (Iso.refl _)

Premises used: CategoryTheory.Iso.refl, CategoryTheory.Iso.trans, CategoryTheory.Arrow.isoMk
-- 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₂')
X₂ : C₂
ρ : B.LeftResolution (W₁ := W₁') (W₂ := W₂') (R.functor (W₁ := W₂) (W₂ := W₂').obj X₂) :=
  Classical.arbitrary (B.LeftResolution (W₁ := W₁') (W₂ := W₂') (R.functor (W₁ := W₂) (W₂ := W₂').obj X₂))
⊢ Nonempty (T.LeftResolution (W₁ := W₁) (W₂ := W₂) X₂)

Tactic:
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 _) }⟩