awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Construction (goal)
Goal:
C : Type uC
inst : Category.{uC', uC} C
W : MorphismProperty.{uC', uC} C
D : Type uD
inst_1 : Category.{uD', uD} D
G : Functor.{uC', uD', uC, uD} C D
hG : W.IsInvertedBy G
G₁ : Functor.{uC', uD', uC, uD} C D
hG₁ : W.IsInvertedBy G₁
G₂ : Functor.{uC', uD', uC, uD} C D
hG₂ : W.IsInvertedBy G₂
f :
  Quiver.Hom (V := MorphismProperty.FunctorsInverting.{uC', uC, uD', uD} W D)
    (ObjectProperty.FullSubcategory.mk (P := fun (F : Functor.{uC', uD', uC, uD} C D) ↦ W.IsInvertedBy F) G₁ hG₁)
    (ObjectProperty.FullSubcategory.mk (P := fun (F : Functor.{uC', uD', uC, uD} C D) ↦ W.IsInvertedBy F) G₂ hG₂)
x : C
⊢ Eq (α :=
    G₁.obj ((W.Q.obj x).as (r := relations W).obj (W := W)) ⟶ G₂.obj ((W.Q.obj x).as (r := relations W).obj (W := W)))
    (NatTransExtension.app (W := W) (eqToHom ⋯ ≫ f.hom ≫ eqToHom ⋯) (W.Q.obj x))
    (CategoryStruct.comp (Y := G₁.obj x) (NatTrans.app (InducedCategory.Hom.hom (eqToHom ⋯)) x)
      (f.hom.app x ≫ NatTrans.app (InducedCategory.Hom.hom (eqToHom ⋯)) x))
have refine_2 : (eqToHom sorry ≫ f.hom ≫ eqToHom sorry).app x = NatTrans.app (eqToHom sorry) x ≫ f.hom.app x ≫ NatTrans.app (eqToHom sorry) x
Tactic: rw [NatTransExtension.app_eq, InducedCategory.eqToHom_hom,
          InducedCategory.eqToHom_hom]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Construction (goal)
Goal:
C : Type uC
inst : Category.{uC', uC} C
W : MorphismProperty.{uC', uC} C
D : Type uD
inst_1 : Category.{uD', uD} D
G : Functor.{uC', uD', uC, uD} C D
hG : W.IsInvertedBy G
F : W.Localization ⥤ D
⊢ map (WhiskeringLeftEquivalence.functor W D) (NatTrans.app (Iso.hom (WhiskeringLeftEquivalence.unitIso W D)) F) ≫
      NatTrans.app (Iso.hom (WhiskeringLeftEquivalence.counitIso W D)) (obj (WhiskeringLeftEquivalence.functor W D) F) =
    𝟙 (obj (WhiskeringLeftEquivalence.functor W D) F)
have h : ∀ (x : C),
  NatTrans.app
      (InducedCategory.Hom.hom
        (map (WhiskeringLeftEquivalence.functor W D)
            (NatTrans.app (Iso.hom (WhiskeringLeftEquivalence.unitIso W D)) F) ≫
          NatTrans.app (Iso.hom (WhiskeringLeftEquivalence.counitIso W D))
            (obj (WhiskeringLeftEquivalence.functor W D) F)))
      x =
    (InducedCategory.Hom.hom (𝟙 (obj (WhiskeringLeftEquivalence.functor W D) F))).app x
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.DerivabilityStructure.Basic (hypothesis)
Goal:
C₁ : Type u₁
C₂ : Type u₂
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
Φ : LocalizerMorphism W₁ W₂
D₁ : Type u_1
D₂ : Type u_2
inst_2 : Category.{v_1, u_1} D₁
inst_3 : Category.{v_2, u_2} D₂
L₁ : Functor.{v₁, v_1, u₁, u_1} C₁ D₁
L₂ : Functor.{v₂, v_2, u₂, u_2} C₂ D₂
inst_4 : L₁.IsLocalization W₁
inst_5 : L₂.IsLocalization W₂
F : Functor.{v_1, v_2, u_1, u_2} D₁ D₂
inst_6 : Φ.HasRightResolutions (W₁ := W₁) (W₂ := W₂)
e : Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L₂ ≅ L₁ ⋙ F
⊢ Φ.IsRightDerivabilityStructure (W₁ := W₁) (W₂ := W₂) ↔ TwoSquare.GuitartExact e.hom
have this : Φ.IsRightDerivabilityStructure (W₁ := W₁) (W₂ := W₂) ↔
  TwoSquare.GuitartExact (B := Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q)
    (Iso.hom
      (CatCommSq.iso (Φ.functor (W₁ := W₁) (W₂ := W₂)) W₁.Q W₂.Q (Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q)))
Tactic: have : Φ.IsRightDerivabilityStructure ↔
      TwoSquare.GuitartExact ((Φ.catCommSq W₁.Q W₂.Q).iso).hom :=
    ⟨fun h => h.guitartExact', fun h => ⟨inferInstance, h⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.DerivabilityStructure.Basic (goal)
Goal:
C₁ : Type u₁
C₂ : Type u₂
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
Φ : LocalizerMorphism W₁ W₂
D₁ : Type u_1
D₂ : Type u_2
inst_2 : Category.{v_1, u_1} D₁
inst_3 : Category.{v_2, u_2} D₂
L₁ : Functor.{v₁, v_1, u₁, u_1} C₁ D₁
L₂ : Functor.{v₂, v_2, u₂, u_2} C₂ D₂
inst_4 : L₁.IsLocalization W₁
inst_5 : L₂.IsLocalization W₂
F : Functor.{v_1, v_2, u_1, u_2} D₁ D₂
inst_6 : Φ.HasRightResolutions (W₁ := W₁) (W₂ := W₂)
e : Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L₂ ≅ L₁ ⋙ F
this :
  Φ.IsRightDerivabilityStructure (W₁ := W₁) (W₂ := W₂) ↔
    TwoSquare.GuitartExact (B := Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q)
      (Iso.hom
        (CatCommSq.iso (Φ.functor (W₁ := W₁) (W₂ := W₂)) W₁.Q W₂.Q
          (Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q)))
⊢ Φ.IsRightDerivabilityStructure (W₁ := W₁) (W₂ := W₂) ↔ TwoSquare.GuitartExact e.hom
have rw : TwoSquare.GuitartExact (B := Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q)
    (Iso.hom
      (CatCommSq.iso (Φ.functor (W₁ := W₁) (W₂ := W₂)) W₁.Q W₂.Q
        (Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q))) ↔
  TwoSquare.GuitartExact e.hom
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.DerivabilityStructure.Basic (goal)
Goal:
C₁ : Type u₁
C₂ : Type u₂
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
Φ : LocalizerMorphism W₁ W₂
D₁ : Type u_1
D₂ : Type u_2
inst_2 : Category.{v_1, u_1} D₁
inst_3 : Category.{v_2, u_2} D₂
L₁ : Functor.{v₁, v_1, u₁, u_1} C₁ D₁
L₂ : Functor.{v₂, v_2, u₂, u_2} C₂ D₂
inst_4 : L₁.IsLocalization W₁
inst_5 : L₂.IsLocalization W₂
F : Functor.{v_1, v_2, u_1, u_2} D₁ D₂
inst_6 : Φ.HasRightResolutions (W₁ := W₁) (W₂ := W₂)
e : Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L₂ ≅ L₁ ⋙ F
this :
  Φ.IsRightDerivabilityStructure (W₁ := W₁) (W₂ := W₂) ↔
    TwoSquare.GuitartExact (B := Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q)
      (Iso.hom
        (CatCommSq.iso (Φ.functor (W₁ := W₁) (W₂ := W₂)) W₁.Q W₂.Q
          (Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q)))
e' : Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ W₂.Q ≅ W₁.Q ⋙ Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q :=
  CatCommSq.iso (Φ.functor (W₁ := W₁) (W₂ := W₂)) W₁.Q W₂.Q (Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q)
E₁ : W₁.Localization ≌ D₁ := uniq W₁.Q L₁ W₁
E₂ : W₂.Localization ≌ D₂ := uniq W₂.Q L₂ W₂
e₁ : W₁.Q ⋙ E₁.functor ≅ L₁ := compUniqFunctor W₁.Q L₁ W₁
e₂ : W₂.Q ⋙ E₂.functor ≅ L₂ := compUniqFunctor W₂.Q L₂ W₂
e'' : (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ W₂.Q) ⋙ E₂.functor ≅ (W₁.Q ⋙ E₁.functor) ⋙ F :=
  Φ.functor (W₁ := W₁) (W₂ := W₂).associator W₂.Q E₂.functor ≪≫
    Φ.functor (W₁ := W₁) (W₂ := W₂).isoWhiskerLeft e₂ ≪≫ e ≪≫ isoWhiskerRight e₁.symm F
e''' : Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q ⋙ E₂.functor ≅ E₁.functor ⋙ F :=
  liftNatIso W₁.Q W₁ ((Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ W₂.Q) ⋙ E₂.functor) ((W₁.Q ⋙ E₁.functor) ⋙ F)
    (Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q ⋙ E₂.functor) (E₁.functor ⋙ F) e''
⊢ TwoSquare.vComp' e'.hom e'''.hom e₁ e₂ = e.hom
have h : ∀ (X₁ : C₁), (TwoSquare.vComp' e'.hom e'''.hom e₁ e₂).natTrans.app X₁ = (TwoSquare.natTrans e.hom).app X₁
Tactic: ext X₁
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.DerivabilityStructure.Basic (goal)
Goal:
C₁ : Type u₁
C₂ : Type u₂
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
Φ : LocalizerMorphism W₁ W₂
D₁ : Type u_1
D₂ : Type u_2
inst_2 : Category.{v_1, u_1} D₁
inst_3 : Category.{v_2, u_2} D₂
L₁ : Functor.{v₁, v_1, u₁, u_1} C₁ D₁
L₂ : Functor.{v₂, v_2, u₂, u_2} C₂ D₂
inst_4 : L₁.IsLocalization W₁
inst_5 : L₂.IsLocalization W₂
F : Functor.{v_1, v_2, u_1, u_2} D₁ D₂
inst_6 : Φ.HasRightResolutions (W₁ := W₁) (W₂ := W₂)
e : Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L₂ ≅ L₁ ⋙ F
this :
  Φ.IsRightDerivabilityStructure (W₁ := W₁) (W₂ := W₂) ↔
    TwoSquare.GuitartExact (B := Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q)
      (Iso.hom
        (CatCommSq.iso (Φ.functor (W₁ := W₁) (W₂ := W₂)) W₁.Q W₂.Q
          (Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q)))
e' : Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ W₂.Q ≅ W₁.Q ⋙ Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q :=
  CatCommSq.iso (Φ.functor (W₁ := W₁) (W₂ := W₂)) W₁.Q W₂.Q (Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q)
E₁ : W₁.Localization ≌ D₁ := uniq W₁.Q L₁ W₁
E₂ : W₂.Localization ≌ D₂ := uniq W₂.Q L₂ W₂
e₁ : W₁.Q ⋙ E₁.functor ≅ L₁ := compUniqFunctor W₁.Q L₁ W₁
e₂ : W₂.Q ⋙ E₂.functor ≅ L₂ := compUniqFunctor W₂.Q L₂ W₂
e'' : (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ W₂.Q) ⋙ E₂.functor ≅ (W₁.Q ⋙ E₁.functor) ⋙ F :=
  Φ.functor (W₁ := W₁) (W₂ := W₂).associator W₂.Q E₂.functor ≪≫
    Φ.functor (W₁ := W₁) (W₂ := W₂).isoWhiskerLeft e₂ ≪≫ e ≪≫ isoWhiskerRight e₁.symm F
e''' : Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q ⋙ E₂.functor ≅ E₁.functor ⋙ F :=
  liftNatIso W₁.Q W₁ ((Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ W₂.Q) ⋙ E₂.functor) ((W₁.Q ⋙ E₁.functor) ⋙ F)
    (Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q ⋙ E₂.functor) (E₁.functor ⋙ F) e''
X₁ : C₁
⊢ (TwoSquare.vComp' e'.hom e'''.hom e₁ e₂).natTrans.app X₁ = (TwoSquare.natTrans e.hom).app X₁
have h : e₂.inv.app (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X₁) ≫
    E₂.functor.map ((TwoSquare.natTrans e'.hom).app X₁) ≫
      (NatTrans.app
            (Iso.hom
              (Lifting.iso W₁.Q W₁ ((Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ W₂.Q) ⋙ E₂.functor)
                (Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q ⋙ E₂.functor)))
            X₁ ≫
          e''.hom.app X₁ ≫ NatTrans.app (Iso.inv (Lifting.iso W₁.Q W₁ ((W₁.Q ⋙ E₁.functor) ⋙ F) (E₁.functor ⋙ F))) X₁) ≫
        F.map (e₁.hom.app X₁) =
  (TwoSquare.natTrans e.hom).app X₁
Tactic: rw [TwoSquare.vComp'_app, liftNatIso_hom, liftNatTrans_app]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.DerivabilityStructure.Basic (goal)
Goal:
C₁ : Type u₁
C₂ : Type u₂
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
Φ : LocalizerMorphism W₁ W₂
D₁ : Type u_1
D₂ : Type u_2
inst_2 : Category.{v_1, u_1} D₁
inst_3 : Category.{v_2, u_2} D₂
L₁ : Functor.{v₁, v_1, u₁, u_1} C₁ D₁
L₂ : Functor.{v₂, v_2, u₂, u_2} C₂ D₂
inst_4 : L₁.IsLocalization W₁
inst_5 : L₂.IsLocalization W₂
F : Functor.{v_1, v_2, u_1, u_2} D₁ D₂
inst_6 : Φ.HasRightResolutions (W₁ := W₁) (W₂ := W₂)
e : Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L₂ ≅ L₁ ⋙ F
this :
  Φ.IsRightDerivabilityStructure (W₁ := W₁) (W₂ := W₂) ↔
    TwoSquare.GuitartExact (B := Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q)
      (Iso.hom
        (CatCommSq.iso (Φ.functor (W₁ := W₁) (W₂ := W₂)) W₁.Q W₂.Q
          (Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q)))
e' : Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ W₂.Q ≅ W₁.Q ⋙ Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q :=
  CatCommSq.iso (Φ.functor (W₁ := W₁) (W₂ := W₂)) W₁.Q W₂.Q (Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q)
E₁ : W₁.Localization ≌ D₁ := uniq W₁.Q L₁ W₁
E₂ : W₂.Localization ≌ D₂ := uniq W₂.Q L₂ W₂
e₁ : W₁.Q ⋙ E₁.functor ≅ L₁ := compUniqFunctor W₁.Q L₁ W₁
e₂ : W₂.Q ⋙ E₂.functor ≅ L₂ := compUniqFunctor W₂.Q L₂ W₂
e'' : (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ W₂.Q) ⋙ E₂.functor ≅ (W₁.Q ⋙ E₁.functor) ⋙ F :=
  Φ.functor (W₁ := W₁) (W₂ := W₂).associator W₂.Q E₂.functor ≪≫
    Φ.functor (W₁ := W₁) (W₂ := W₂).isoWhiskerLeft e₂ ≪≫ e ≪≫ isoWhiskerRight e₁.symm F
e''' : Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q ⋙ E₂.functor ≅ E₁.functor ⋙ F :=
  liftNatIso W₁.Q W₁ ((Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ W₂.Q) ⋙ E₂.functor) ((W₁.Q ⋙ E₁.functor) ⋙ F)
    (Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q ⋙ E₂.functor) (E₁.functor ⋙ F) e''
X₁ : C₁
⊢ e₂.inv.app (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X₁) ≫
      E₂.functor.map ((TwoSquare.natTrans e'.hom).app X₁) ≫
        NatTrans.app
            (Iso.hom
              (Lifting.iso W₁.Q W₁ ((Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ W₂.Q) ⋙ E₂.functor)
                (Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q ⋙ E₂.functor)))
            X₁ ≫
          e₂.hom.app (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X₁) ≫
            e.hom.app X₁ ≫
              F.map (e₁.inv.app X₁) ≫
                NatTrans.app (Iso.inv (Lifting.iso W₁.Q W₁ ((W₁.Q ⋙ E₁.functor) ⋙ F) (E₁.functor ⋙ F))) X₁ ≫
                  F.map (e₁.hom.app X₁) =
    (TwoSquare.natTrans e.hom).app X₁
have h : e₂.inv.app (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X₁) ≫
    E₂.functor.map ((TwoSquare.natTrans e'.hom).app X₁) ≫
      E₂.functor.map (NatTrans.app (Iso.hom (liftingLocalizedFunctor._aux_1 (W₁ := W₁) (W₂ := W₂) Φ W₁.Q W₂.Q)) X₁) ≫
        e₂.hom.app (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X₁) ≫
          e.hom.app X₁ ≫ F.map (e₁.inv.app X₁) ≫ F.map (𝟙 (E₁.functor.obj (W₁.Q.obj X₁))) ≫ F.map (e₁.hom.app X₁) =
  (TwoSquare.natTrans e.hom).app X₁
Tactic: dsimp [Lifting.iso]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.DerivabilityStructure.Basic (goal)
Goal:
C₁ : Type u₁
C₂ : Type u₂
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
Φ : LocalizerMorphism W₁ W₂
D₁ : Type u_1
D₂ : Type u_2
inst_2 : Category.{v_1, u_1} D₁
inst_3 : Category.{v_2, u_2} D₂
L₁ : Functor.{v₁, v_1, u₁, u_1} C₁ D₁
L₂ : Functor.{v₂, v_2, u₂, u_2} C₂ D₂
inst_4 : L₁.IsLocalization W₁
inst_5 : L₂.IsLocalization W₂
F : Functor.{v_1, v_2, u_1, u_2} D₁ D₂
inst_6 : Φ.HasRightResolutions (W₁ := W₁) (W₂ := W₂)
e : Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L₂ ≅ L₁ ⋙ F
this :
  Φ.IsRightDerivabilityStructure (W₁ := W₁) (W₂ := W₂) ↔
    TwoSquare.GuitartExact (B := Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q)
      (Iso.hom
        (CatCommSq.iso (Φ.functor (W₁ := W₁) (W₂ := W₂)) W₁.Q W₂.Q
          (Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q)))
e' : Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ W₂.Q ≅ W₁.Q ⋙ Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q :=
  CatCommSq.iso (Φ.functor (W₁ := W₁) (W₂ := W₂)) W₁.Q W₂.Q (Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q)
E₁ : W₁.Localization ≌ D₁ := uniq W₁.Q L₁ W₁
E₂ : W₂.Localization ≌ D₂ := uniq W₂.Q L₂ W₂
e₁ : W₁.Q ⋙ E₁.functor ≅ L₁ := compUniqFunctor W₁.Q L₁ W₁
e₂ : W₂.Q ⋙ E₂.functor ≅ L₂ := compUniqFunctor W₂.Q L₂ W₂
e'' : (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ W₂.Q) ⋙ E₂.functor ≅ (W₁.Q ⋙ E₁.functor) ⋙ F :=
  Φ.functor (W₁ := W₁) (W₂ := W₂).associator W₂.Q E₂.functor ≪≫
    Φ.functor (W₁ := W₁) (W₂ := W₂).isoWhiskerLeft e₂ ≪≫ e ≪≫ isoWhiskerRight e₁.symm F
e''' : Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q ⋙ E₂.functor ≅ E₁.functor ⋙ F :=
  liftNatIso W₁.Q W₁ ((Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ W₂.Q) ⋙ E₂.functor) ((W₁.Q ⋙ E₁.functor) ⋙ F)
    (Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q ⋙ E₂.functor) (E₁.functor ⋙ F) e''
X₁ : C₁
⊢ e₂.inv.app (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X₁) ≫
      E₂.functor.map ((TwoSquare.natTrans e'.hom).app X₁) ≫
        E₂.functor.map (NatTrans.app (Iso.hom (liftingLocalizedFunctor._aux_1 (W₁ := W₁) (W₂ := W₂) Φ W₁.Q W₂.Q)) X₁) ≫
          e₂.hom.app (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X₁) ≫
            e.hom.app X₁ ≫ F.map (e₁.inv.app X₁) ≫ F.map (𝟙 (E₁.functor.obj (W₁.Q.obj X₁))) ≫ F.map (e₁.hom.app X₁) =
    (TwoSquare.natTrans e.hom).app X₁
have h : e₂.inv.app (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X₁) ≫
    E₂.functor.map
        ((TwoSquare.natTrans e'.hom).app X₁ ≫
          NatTrans.app (Iso.hom (liftingLocalizedFunctor._aux_1 (W₁ := W₁) (W₂ := W₂) Φ W₁.Q W₂.Q)) X₁) ≫
      e₂.hom.app (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X₁) ≫ e.hom.app X₁ =
  (TwoSquare.natTrans e.hom).app X₁
Tactic: rw [F.map_id, id_comp, ← F.map_comp, Iso.inv_hom_id_app, F.map_id, comp_id,
      ← Functor.map_comp_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.DerivabilityStructure.Basic (goal)
Goal:
C₁ : Type u₁
C₂ : Type u₂
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
Φ : LocalizerMorphism W₁ W₂
D₁ : Type u_1
D₂ : Type u_2
inst_2 : Category.{v_1, u_1} D₁
inst_3 : Category.{v_2, u_2} D₂
L₁ : Functor.{v₁, v_1, u₁, u_1} C₁ D₁
L₂ : Functor.{v₂, v_2, u₂, u_2} C₂ D₂
inst_4 : L₁.IsLocalization W₁
inst_5 : L₂.IsLocalization W₂
F : Functor.{v_1, v_2, u_1, u_2} D₁ D₂
inst_6 : Φ.HasRightResolutions (W₁ := W₁) (W₂ := W₂)
e : Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L₂ ≅ L₁ ⋙ F
this :
  Φ.IsRightDerivabilityStructure (W₁ := W₁) (W₂ := W₂) ↔
    TwoSquare.GuitartExact (B := Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q)
      (Iso.hom
        (CatCommSq.iso (Φ.functor (W₁ := W₁) (W₂ := W₂)) W₁.Q W₂.Q
          (Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q)))
e' : Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ W₂.Q ≅ W₁.Q ⋙ Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q :=
  CatCommSq.iso (Φ.functor (W₁ := W₁) (W₂ := W₂)) W₁.Q W₂.Q (Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q)
E₁ : W₁.Localization ≌ D₁ := uniq W₁.Q L₁ W₁
E₂ : W₂.Localization ≌ D₂ := uniq W₂.Q L₂ W₂
e₁ : W₁.Q ⋙ E₁.functor ≅ L₁ := compUniqFunctor W₁.Q L₁ W₁
e₂ : W₂.Q ⋙ E₂.functor ≅ L₂ := compUniqFunctor W₂.Q L₂ W₂
e'' : (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ W₂.Q) ⋙ E₂.functor ≅ (W₁.Q ⋙ E₁.functor) ⋙ F :=
  Φ.functor (W₁ := W₁) (W₂ := W₂).associator W₂.Q E₂.functor ≪≫
    Φ.functor (W₁ := W₁) (W₂ := W₂).isoWhiskerLeft e₂ ≪≫ e ≪≫ isoWhiskerRight e₁.symm F
e''' : Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q ⋙ E₂.functor ≅ E₁.functor ⋙ F :=
  liftNatIso W₁.Q W₁ ((Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ W₂.Q) ⋙ E₂.functor) ((W₁.Q ⋙ E₁.functor) ⋙ F)
    (Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q ⋙ E₂.functor) (E₁.functor ⋙ F) e''
X₁ : C₁
⊢ e₂.inv.app (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X₁) ≫
      E₂.functor.map
          ((TwoSquare.natTrans e'.hom).app X₁ ≫
            NatTrans.app (Iso.hom (liftingLocalizedFunctor._aux_1 (W₁ := W₁) (W₂ := W₂) Φ W₁.Q W₂.Q)) X₁) ≫
        e₂.hom.app (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X₁) ≫ e.hom.app X₁ =
    (TwoSquare.natTrans e.hom).app X₁
have h : e₂.inv.app (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X₁) ≫
    E₂.functor.map (𝟙 ((Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ W₂.Q).obj X₁)) ≫
      e₂.hom.app (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X₁) ≫ e.hom.app X₁ =
  (TwoSquare.natTrans e.hom).app X₁
Tactic: erw [show (CatCommSq.iso Φ.functor W₁.Q W₂.Q (localizedFunctor Φ W₁.Q W₂.Q)).hom =
      (Lifting.iso W₁.Q W₁ _ _).inv by rfl, Iso.inv_hom_id_app]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.DerivabilityStructure.Basic (hypothesis)
Goal:
C₁ : Type u₁
C₂ : Type u₂
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
Φ : LocalizerMorphism W₁ W₂
D₁ : Type u_1
D₂ : Type u_2
inst_2 : Category.{v_1, u_1} D₁
inst_3 : Category.{v_2, u_2} D₂
L₁ : Functor.{v₁, v_1, u₁, u_1} C₁ D₁
L₂ : Functor.{v₂, v_2, u₂, u_2} C₂ D₂
inst_4 : L₁.IsLocalization W₁
inst_5 : L₂.IsLocalization W₂
F : Functor.{v_1, v_2, u_1, u_2} D₁ D₂
inst_6 : Φ.HasRightResolutions (W₁ := W₁) (W₂ := W₂)
e : Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L₂ ≅ L₁ ⋙ F
this :
  Φ.IsRightDerivabilityStructure (W₁ := W₁) (W₂ := W₂) ↔
    TwoSquare.GuitartExact (B := Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q)
      (Iso.hom
        (CatCommSq.iso (Φ.functor (W₁ := W₁) (W₂ := W₂)) W₁.Q W₂.Q
          (Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q)))
e' : Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ W₂.Q ≅ W₁.Q ⋙ Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q :=
  CatCommSq.iso (Φ.functor (W₁ := W₁) (W₂ := W₂)) W₁.Q W₂.Q (Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q)
E₁ : W₁.Localization ≌ D₁ := uniq W₁.Q L₁ W₁
E₂ : W₂.Localization ≌ D₂ := uniq W₂.Q L₂ W₂
e₁ : W₁.Q ⋙ E₁.functor ≅ L₁ := compUniqFunctor W₁.Q L₁ W₁
e₂ : W₂.Q ⋙ E₂.functor ≅ L₂ := compUniqFunctor W₂.Q L₂ W₂
e'' : (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ W₂.Q) ⋙ E₂.functor ≅ (W₁.Q ⋙ E₁.functor) ⋙ F :=
  Φ.functor (W₁ := W₁) (W₂ := W₂).associator W₂.Q E₂.functor ≪≫
    Φ.functor (W₁ := W₁) (W₂ := W₂).isoWhiskerLeft e₂ ≪≫ e ≪≫ isoWhiskerRight e₁.symm F
e''' : Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q ⋙ E₂.functor ≅ E₁.functor ⋙ F :=
  liftNatIso W₁.Q W₁ ((Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ W₂.Q) ⋙ E₂.functor) ((W₁.Q ⋙ E₁.functor) ⋙ F)
    (Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q ⋙ E₂.functor) (E₁.functor ⋙ F) e''
⊢ TwoSquare.GuitartExact (B := Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q)
      (Iso.hom
        (CatCommSq.iso (Φ.functor (W₁ := W₁) (W₂ := W₂)) W₁.Q W₂.Q
          (Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q))) ↔
    TwoSquare.GuitartExact e.hom
have this₁ : TwoSquare.vComp' e'.hom e'''.hom e₁ e₂ = e.hom
Tactic: have : TwoSquare.vComp' e'.hom e'''.hom e₁ e₂ = e.hom := by
    ext X₁
    rw [TwoSquare.vComp'_app, liftNatIso_hom, liftNatTrans_app]
    simp only [Functor.comp_obj, Iso.trans_hom, isoWhiskerLeft_hom, isoWhiskerRight_hom,
      Iso.symm_hom, NatTrans.comp_app, Functor.associator_hom_app, whiskerLeft_app,
      whiskerRight_app, id_comp, assoc, e'']
    dsimp [Lifting.iso]
    rw [F.map_id, id_comp, ← F.map_comp, Iso.inv_hom_id_app, F.map_id, comp_id,
      ← Functor.map_comp_assoc]
    erw [show (CatCommSq.iso Φ.functor W₁.Q W₂.Q (localizedFunctor Φ W₁.Q W₂.Q)).hom =
      (Lifting.iso W₁.Q W₁ _ _).inv by rfl, Iso.inv_hom_id_app]
    simp
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.DerivabilityStructure.Basic (goal)
Goal:
C₁ : Type u₁
C₂ : Type u₂
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
Φ : LocalizerMorphism W₁ W₂
D₁ : Type u_1
D₂ : Type u_2
inst_2 : Category.{v_1, u_1} D₁
inst_3 : Category.{v_2, u_2} D₂
L₁ : Functor.{v₁, v_1, u₁, u_1} C₁ D₁
L₂ : Functor.{v₂, v_2, u₂, u_2} C₂ D₂
inst_4 : L₁.IsLocalization W₁
inst_5 : L₂.IsLocalization W₂
F : Functor.{v_1, v_2, u_1, u_2} D₁ D₂
inst_6 : Φ.HasRightResolutions (W₁ := W₁) (W₂ := W₂)
e : Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L₂ ≅ L₁ ⋙ F
this_1 :
  Φ.IsRightDerivabilityStructure (W₁ := W₁) (W₂ := W₂) ↔
    TwoSquare.GuitartExact (B := Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q)
      (Iso.hom
        (CatCommSq.iso (Φ.functor (W₁ := W₁) (W₂ := W₂)) W₁.Q W₂.Q
          (Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q)))
e' : Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ W₂.Q ≅ W₁.Q ⋙ Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q :=
  CatCommSq.iso (Φ.functor (W₁ := W₁) (W₂ := W₂)) W₁.Q W₂.Q (Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q)
E₁ : W₁.Localization ≌ D₁ := uniq W₁.Q L₁ W₁
E₂ : W₂.Localization ≌ D₂ := uniq W₂.Q L₂ W₂
e₁ : W₁.Q ⋙ E₁.functor ≅ L₁ := compUniqFunctor W₁.Q L₁ W₁
e₂ : W₂.Q ⋙ E₂.functor ≅ L₂ := compUniqFunctor W₂.Q L₂ W₂
e'' : (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ W₂.Q) ⋙ E₂.functor ≅ (W₁.Q ⋙ E₁.functor) ⋙ F :=
  Φ.functor (W₁ := W₁) (W₂ := W₂).associator W₂.Q E₂.functor ≪≫
    Φ.functor (W₁ := W₁) (W₂ := W₂).isoWhiskerLeft e₂ ≪≫ e ≪≫ isoWhiskerRight e₁.symm F
e''' : Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q ⋙ E₂.functor ≅ E₁.functor ⋙ F :=
  liftNatIso W₁.Q W₁ ((Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ W₂.Q) ⋙ E₂.functor) ((W₁.Q ⋙ E₁.functor) ⋙ F)
    (Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q ⋙ E₂.functor) (E₁.functor ⋙ F) e''
this : TwoSquare.vComp' e'.hom e'''.hom e₁ e₂ = e.hom
⊢ TwoSquare.GuitartExact (B := Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q)
      (Iso.hom
        (CatCommSq.iso (Φ.functor (W₁ := W₁) (W₂ := W₂)) W₁.Q W₂.Q
          (Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q))) ↔
    TwoSquare.GuitartExact e.hom
have rw : (TwoSquare.vComp' e'.hom e'''.hom e₁ e₂).GuitartExact ↔ TwoSquare.GuitartExact e.hom
Tactic: rw [← TwoSquare.GuitartExact.vComp'_iff_of_equivalences e'.hom E₁ E₂ e''' e₁ e₂, this]