awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.DerivabilityStructure.OfLocalizedEquivalences (goal)
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 :=
    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₂')))
have 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₂'))
Tactic: simp only [← R.inverseImage_eq, Functor.comp_obj,
          MorphismProperty.inverseImage_iff, Functor.map_preimage]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.DerivabilityStructure.OfLocalizedEquivalences (goal)
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₂'))
have 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₂'))
Tactic: refine (W₂'.arrow_mk_iso_iff ?_).2 ρ.hw
-- 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 : 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.IsLeftDerivabilityStructure (W₁ := W₁) (W₂ := W₂)
have this : 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 _) }⟩
-- 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 : 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
⊢ T.IsLeftDerivabilityStructure (W₁ := W₁) (W₂ := W₂)
have he' : TwoSquare.GuitartExact e'.inv
Tactic: have he' : TwoSquare.GuitartExact e'.inv := inferInstance
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.DerivabilityStructure.OfLocalizedEquivalences (goal)
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
have h : ∀ (X : C₁), (TwoSquare.hComp iso.inv e'.inv).natTrans.app X = (TwoSquare.natTrans e.inv).app X
Tactic: ext
-- 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 : 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
⊢ T.IsLeftDerivabilityStructure (W₁ := W₁) (W₂ := W₂)
have this₁ : TwoSquare.hComp iso.inv e'.inv = e.inv
Tactic: have : TwoSquare.hComp iso.inv e'.inv = e.inv := by ext; simp [e]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.DerivabilityStructure.OfLocalizedEquivalences (goal)
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
⊢ T.IsLeftDerivabilityStructure (W₁ := W₁) (W₂ := W₂)
have rw : (TwoSquare.hComp iso.inv e'.inv).GuitartExact
Tactic: rw [T.isLeftDerivabilityStructure_iff (L.functor ⋙ W₁'.Q)
    (R.functor ⋙ W₂'.Q) F e, ← this]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.DerivabilityStructure.OfLocalizedEquivalences (goal)
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
⊢ B.IsRightDerivabilityStructure (W₁ := W₁') (W₂ := W₂')
have rw : B.op (W₁ := W₁') (W₂ := W₂').IsLeftDerivabilityStructure (W₁ := W₁'.op) (W₂ := W₂'.op)
Tactic: rw [isRightDerivabilityStructure_iff_op]
-- 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 : 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
⊢ B.op (W₁ := W₁') (W₂ := W₂').IsLeftDerivabilityStructure (W₁ := W₁'.op) (W₂ := W₂'.op)
have this : TwoSquare.GuitartExact iso'.inv
Tactic: have : TwoSquare.GuitartExact iso'.inv :=
    inferInstanceAs (TwoSquare.op iso.hom).GuitartExact
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.DerivabilityStructure.OfLocalizedEquivalences (goal)
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
⊢ T.IsRightDerivabilityStructure (W₁ := W₁) (W₂ := W₂) ↔ B.IsRightDerivabilityStructure (W₁ := W₁') (W₂ := W₂')
have 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)
Tactic: simp only [isRightDerivabilityStructure_iff_op]
-- 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 : 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
⊢ 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)
have this : TwoSquare.GuitartExact iso'.inv
Tactic: have : TwoSquare.GuitartExact iso'.inv :=
    inferInstanceAs (TwoSquare.op iso.hom).GuitartExact
-- 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
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₂')
⊢ B.IsLeftDerivabilityStructure (W₁ := W₁') (W₂ := W₂')
have this : L.IsLocalizedEquivalence (W₁ := W₁) (W₂ := W₁')
Tactic: have := L.isLocalizedEquivalence_of_isInduced
-- 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
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₁')
⊢ B.IsLeftDerivabilityStructure (W₁ := W₁') (W₂ := W₂')
have this₁ : R.IsLocalizedEquivalence (W₁ := W₂) (W₂ := W₂')
Tactic: have := R.isLocalizedEquivalence_of_isInduced