awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.Basic
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₂
F : W₁.Localization ⥤ W₂.Localization := Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q
e : Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ W₂.Q ≅ W₁.Q ⋙ F :=
  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₂).op ⋙ W₂.Q.op ≅ W₁.Q.op ⋙ F.op := NatIso.op e.symm
eq : TwoSquare.GuitartExact e'.inv ↔ TwoSquare.GuitartExact e.hom
h : Φ.op (W₁ := W₁) (W₂ := W₂).IsLeftDerivabilityStructure (W₁ := W₁.op) (W₂ := W₂.op)
this : Φ.HasRightResolutions (W₁ := W₁) (W₂ := W₂)
⊢ TwoSquare.GuitartExact e'.inv

Tactic:
Φ.op.guitartExact_of_isLeftDerivabilityStructure' _ _ _ e'

Premises used: CategoryTheory.Functor.op, CategoryTheory.LocalizerMorphism.guitartExact_of_isLeftDerivabilityStructure', CategoryTheory.LocalizerMorphism.op
-- Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.Basic
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₂
F : W₁.Localization ⥤ W₂.Localization := Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q
e : Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ W₂.Q ≅ W₁.Q ⋙ F :=
  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₂).op ⋙ W₂.Q.op ≅ W₁.Q.op ⋙ F.op := NatIso.op e.symm
eq : TwoSquare.GuitartExact e'.inv ↔ TwoSquare.GuitartExact e.hom
h : Φ.op (W₁ := W₁) (W₂ := W₂).IsLeftDerivabilityStructure (W₁ := W₁.op) (W₂ := W₂.op)
this : Φ.HasRightResolutions (W₁ := W₁) (W₂ := W₂)
⊢ TwoSquare.GuitartExact e'.inv

Tactic:
exact Φ.op.guitartExact_of_isLeftDerivabilityStructure' _ _ _ e'

Premises used: CategoryTheory.LocalizerMorphism.guitartExact_of_isLeftDerivabilityStructure', CategoryTheory.LocalizerMorphism.op
-- Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.Basic
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 rwa rwa₁ rwa₂ rwa₃ : Φ.IsLeftDerivabilityStructure (W₁ := W₁) (W₂ := W₂)
⊢ Φ.op (W₁ := W₁) (W₂ := W₂).IsRightDerivabilityStructure (W₁ := W₁.op) (W₂ := W₂.op)

Tactic:
rwa [← isLeftDerivabilityStructure_iff_op]

Premises used: CategoryTheory.LocalizerMorphism.isLeftDerivabilityStructure_iff_op
-- Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.Basic
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 rwa rwa₁ rwa₂ rwa₃ : Φ.IsRightDerivabilityStructure (W₁ := W₁) (W₂ := W₂)
⊢ Φ.op (W₁ := W₁) (W₂ := W₂).IsLeftDerivabilityStructure (W₁ := W₁.op) (W₂ := W₂.op)

Tactic:
rwa [← isRightDerivabilityStructure_iff_op]

Premises used: CategoryTheory.LocalizerMorphism.isRightDerivabilityStructure_iff_op
-- Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.Constructor
Goal:
C₁ : Type u_1
C₂ : Type u_2
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
W₁ : MorphismProperty.{v_1, u_1} C₁
W₂ : MorphismProperty.{v_2, u_2} C₂
Φ : LocalizerMorphism W₁ W₂
inst_2 : ∀ (X₂ : C₂), IsConnected (Φ.RightResolution (W₁ := W₁) (W₂ := W₂) X₂)
inst_3 : Φ.arrow (W₁ := W₁) (W₂ := W₂).HasRightResolutions (W₁ := W₁.arrow) (W₂ := W₂.arrow)
inst_4 : W₂.ContainsIdentities
D : Type u_3
inst_5 : Category.{v_3, u_3} D
L : Functor.{v_2, v_3, u_2, u_3} C₂ D
inst_6 : L.IsLocalization W₂
X₂ : C₂
X₃ : D
y : L.obj X₂ ⟶ X₃
R R' : Φ.RightResolution (W₁ := W₁) (W₂ := W₂) X₂
φ : R ⟶ R'
h :
  StructuredArrow.Hom.right
      (((TwoSquare.mk (Φ.functor (W₁ := W₁) (W₂ := W₂)) (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L) L (𝟭 D)
                  (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L).rightUnitor.inv).structuredArrowDownwards
              X₂).map
          (StructuredArrow.homMk (φ.f (W₁ := W₁) (W₂ := W₂)) ⋯) ≫
        (CostructuredArrow.mk (StructuredArrow.homMk ((isoOfHom L W₂ (R'.w (W₁ := W₁) (W₂ := W₂)) ⋯).inv ≫ y) ⋯)).hom) =
    StructuredArrow.Hom.right
      (CostructuredArrow.mk (StructuredArrow.homMk ((isoOfHom L W₂ (R.w (W₁ := W₁) (W₂ := W₂)) ⋯).inv ≫ y) ⋯)).hom
⊢ ((TwoSquare.mk (Φ.functor (W₁ := W₁) (W₂ := W₂)) (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L) L (𝟭 D)
                (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L).rightUnitor.inv).structuredArrowDownwards
            X₂).map
        (StructuredArrow.homMk (φ.f (W₁ := W₁) (W₂ := W₂)) ⋯) ≫
      (CostructuredArrow.mk (StructuredArrow.homMk ((isoOfHom L W₂ (R'.w (W₁ := W₁) (W₂ := W₂)) ⋯).inv ≫ y) ⋯)).hom =
    (CostructuredArrow.mk (StructuredArrow.homMk ((isoOfHom L W₂ (R.w (W₁ := W₁) (W₂ := W₂)) ⋯).inv ≫ y) ⋯)).hom

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.Constructor
Goal:
C₁ : Type u_1
C₂ : Type u_2
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
W₁ : MorphismProperty.{v_1, u_1} C₁
W₂ : MorphismProperty.{v_2, u_2} C₂
Φ : LocalizerMorphism W₁ W₂
inst_2 : ∀ (X₂ : C₂), IsConnected (Φ.RightResolution (W₁ := W₁) (W₂ := W₂) X₂)
inst_3 : Φ.arrow (W₁ := W₁) (W₂ := W₂).HasRightResolutions (W₁ := W₁.arrow) (W₂ := W₂.arrow)
inst_4 : W₂.ContainsIdentities
D : Type u_3
inst_5 : Category.{v_3, u_3} D
L : Functor.{v_2, v_3, u_2, u_3} C₂ D
inst_6 : L.IsLocalization W₂
X₂ : C₂
X₃ : D
y : L.obj X₂ ⟶ X₃
R R' : Φ.RightResolution (W₁ := W₁) (W₂ := W₂) X₂
φ : R ⟶ R'
h :
  L.map (Φ.functor (W₁ := W₁) (W₂ := W₂).map (φ.f (W₁ := W₁) (W₂ := W₂))) ≫
      (isoOfHom L W₂ (R'.w (W₁ := W₁) (W₂ := W₂)) ⋯).inv ≫ y =
    (isoOfHom L W₂ (R.w (W₁ := W₁) (W₂ := W₂)) ⋯).inv ≫ y
⊢ StructuredArrow.Hom.right
      (((TwoSquare.mk (Φ.functor (W₁ := W₁) (W₂ := W₂)) (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L) L (𝟭 D)
                  (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L).rightUnitor.inv).structuredArrowDownwards
              X₂).map
          (StructuredArrow.homMk (φ.f (W₁ := W₁) (W₂ := W₂)) ⋯) ≫
        (CostructuredArrow.mk (StructuredArrow.homMk ((isoOfHom L W₂ (R'.w (W₁ := W₁) (W₂ := W₂)) ⋯).inv ≫ y) ⋯)).hom) =
    StructuredArrow.Hom.right
      (CostructuredArrow.mk (StructuredArrow.homMk ((isoOfHom L W₂ (R.w (W₁ := W₁) (W₂ := W₂)) ⋯).inv ≫ y) ⋯)).hom

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.Constructor
Goal:
C₁ : Type u_1
C₂ : Type u_2
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
W₁ : MorphismProperty.{v_1, u_1} C₁
W₂ : MorphismProperty.{v_2, u_2} C₂
Φ : LocalizerMorphism W₁ W₂
inst_2 : ∀ (X₂ : C₂), IsConnected (Φ.RightResolution (W₁ := W₁) (W₂ := W₂) X₂)
inst_3 : Φ.arrow (W₁ := W₁) (W₂ := W₂).HasRightResolutions (W₁ := W₁.arrow) (W₂ := W₂.arrow)
inst_4 : W₂.ContainsIdentities
D : Type u_3
inst_5 : Category.{v_3, u_3} D
L : Functor.{v_2, v_3, u_2, u_3} C₂ D
inst_6 : L.IsLocalization W₂
X₂ : C₂
X₃ : D
y : L.obj X₂ ⟶ X₃
R R' : Φ.RightResolution (W₁ := W₁) (W₂ := W₂) X₂
φ : R ⟶ R'
h :
  (L.map (Φ.functor (W₁ := W₁) (W₂ := W₂).map (φ.f (W₁ := W₁) (W₂ := W₂))) ≫
        (isoOfHom L W₂ (R'.w (W₁ := W₁) (W₂ := W₂)) ⋯).inv) ≫
      y =
    (isoOfHom L W₂ (R.w (W₁ := W₁) (W₂ := W₂)) ⋯).inv ≫ y
h₁ :
  (isoOfHom L W₂ (R.w (W₁ := W₁) (W₂ := W₂)) ⋯).hom ≫
      (L.map (Φ.functor (W₁ := W₁) (W₂ := W₂).map (φ.f (W₁ := W₁) (W₂ := W₂))) ≫
          (isoOfHom L W₂ (R'.w (W₁ := W₁) (W₂ := W₂)) ⋯).inv) ≫
        y =
    (isoOfHom L W₂ (R.w (W₁ := W₁) (W₂ := W₂)) ⋯).hom ≫ (isoOfHom L W₂ (R.w (W₁ := W₁) (W₂ := W₂)) ⋯).inv ≫ y
h₂ :
  L.map (R.w (W₁ := W₁) (W₂ := W₂)) ≫
      (L.map (Φ.functor (W₁ := W₁) (W₂ := W₂).map (φ.f (W₁ := W₁) (W₂ := W₂))) ≫
          (isoOfHom L W₂ (R'.w (W₁ := W₁) (W₂ := W₂)) ⋯).inv) ≫
        y =
    L.map (R.w (W₁ := W₁) (W₂ := W₂)) ≫ (isoOfHom L W₂ (R.w (W₁ := W₁) (W₂ := W₂)) ⋯).inv ≫ y
h₃ :
  L.map (R.w (W₁ := W₁) (W₂ := W₂)) ≫
      (L.map (Φ.functor (W₁ := W₁) (W₂ := W₂).map (φ.f (W₁ := W₁) (W₂ := W₂))) ≫
          (isoOfHom L W₂ (R'.w (W₁ := W₁) (W₂ := W₂)) ⋯).inv) ≫
        y =
    y
h₄ :
  L.map (R.w (W₁ := W₁) (W₂ := W₂)) ≫
      L.map (Φ.functor (W₁ := W₁) (W₂ := W₂).map (φ.f (W₁ := W₁) (W₂ := W₂))) ≫
        (isoOfHom L W₂ (R'.w (W₁ := W₁) (W₂ := W₂)) ⋯).inv ≫ y =
    y
h₅ :
  L.map (R.w (W₁ := W₁) (W₂ := W₂) ≫ Φ.functor (W₁ := W₁) (W₂ := W₂).map (φ.f (W₁ := W₁) (W₂ := W₂))) ≫
      (isoOfHom L W₂ (R'.w (W₁ := W₁) (W₂ := W₂)) ⋯).inv ≫ y =
    y
h₆ : L.map (R'.w (W₁ := W₁) (W₂ := W₂)) ≫ (isoOfHom L W₂ (R'.w (W₁ := W₁) (W₂ := W₂)) ⋯).inv ≫ y = y
h₇ h₈ : y = y
⊢ L.map (Φ.functor (W₁ := W₁) (W₂ := W₂).map (φ.f (W₁ := W₁) (W₂ := W₂))) ≫
      (isoOfHom L W₂ (R'.w (W₁ := W₁) (W₂ := W₂)) ⋯).inv ≫ y =
    (isoOfHom L W₂ (R.w (W₁ := W₁) (W₂ := W₂)) ⋯).inv ≫ y

Tactic:
rw [← assoc, ← cancel_epi (isoOfHom L W₂ R.w R.hw).hom,
      isoOfHom_hom, isoOfHom_hom_inv_id_assoc, assoc, ← L.map_comp_assoc,
      φ.comm, isoOfHom_hom_inv_id_assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.LocalizerMorphism.RightResolution.w, CategoryTheory.Localization.isoOfHom_hom, CategoryTheory.Localization.isoOfHom, CategoryTheory.LocalizerMorphism.RightResolution.Hom.comm, CategoryTheory.Functor.map_comp_assoc, CategoryTheory.Localization.isoOfHom_hom_inv_id_assoc, CategoryTheory.LocalizerMorphism.RightResolution.hw, CategoryTheory.cancel_epi, CategoryTheory.Iso.hom
-- Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.Constructor
Goal:
C₁ : Type u_1
C₂ : Type u_2
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
W₁ : MorphismProperty.{v_1, u_1} C₁
W₂ : MorphismProperty.{v_2, u_2} C₂
Φ : LocalizerMorphism W₁ W₂
inst_2 : ∀ (X₂ : C₂), IsConnected (Φ.RightResolution (W₁ := W₁) (W₂ := W₂) X₂)
inst_3 : Φ.arrow (W₁ := W₁) (W₂ := W₂).HasRightResolutions (W₁ := W₁.arrow) (W₂ := W₂.arrow)
inst_4 : W₂.ContainsIdentities
D : Type u_3
inst_5 : Category.{v_3, u_3} D
L : Functor.{v_2, v_3, u_2, u_3} C₂ D
inst_6 : L.IsLocalization W₂
X₂ : C₂
X₃ : D
y : L.obj X₂ ⟶ X₃
w : TwoSquare (Φ.functor (W₁ := W₁) (W₂ := W₂)) (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L) L (𝟭 D) :=
  TwoSquare.mk (Φ.functor (W₁ := W₁) (W₂ := W₂)) (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L) L (𝟭 D)
    (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L).rightUnitor.inv
⊢ Nonempty (w.CostructuredArrowDownwards y)

Tactic:
have : Nonempty (w.CostructuredArrowDownwards y) :=
    ⟨(fromRightResolution Φ L y).obj (Classical.arbitrary _)⟩
-- Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.Constructor
Goal:
C₁ : Type u_1
C₂ : Type u_2
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
W₁ : MorphismProperty.{v_1, u_1} C₁
W₂ : MorphismProperty.{v_2, u_2} C₂
Φ : LocalizerMorphism W₁ W₂
inst_2 : ∀ (X₂ : C₂), IsConnected (Φ.RightResolution (W₁ := W₁) (W₂ := W₂) X₂)
inst_3 : Φ.arrow (W₁ := W₁) (W₂ := W₂).HasRightResolutions (W₁ := W₁.arrow) (W₂ := W₂.arrow)
inst_4 : W₂.ContainsIdentities
D : Type u_3
inst_5 : Category.{v_3, u_3} D
L : Functor.{v_2, v_3, u_2, u_3} C₂ D
inst_6 : L.IsLocalization W₂
X₂ : C₂
X₃ : D
y : L.obj X₂ ⟶ X₃
w : TwoSquare (Φ.functor (W₁ := W₁) (W₂ := W₂)) (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L) L (𝟭 D) :=
  TwoSquare.mk (Φ.functor (W₁ := W₁) (W₂ := W₂)) (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L) L (𝟭 D)
    (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L).rightUnitor.inv
this_1 : Nonempty (w.CostructuredArrowDownwards y)
this :
  ∀ (X : w.CostructuredArrowDownwards y),
    ∃ (Y : Φ.RightResolution (W₁ := W₁) (W₂ := W₂) X₂),
      Zigzag X ((fromRightResolution (W₁ := W₁) (W₂ := W₂) Φ L y).obj Y)
refine :
  ∀
    (X X' :
      (TwoSquare.mk (Φ.functor (W₁ := W₁) (W₂ := W₂)) (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L) L (𝟭 D)
            (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L).rightUnitor.inv).CostructuredArrowDownwards
        y),
    Zigzag X X'
⊢ IsConnected
    ((TwoSquare.mk (Φ.functor (W₁ := W₁) (W₂ := W₂)) (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L) L (𝟭 D)
          (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L).rightUnitor.inv).CostructuredArrowDownwards
      y)

Tactic:
refine zigzag_isConnected (fun X X' => ?_)

Premises used: CategoryTheory.zigzag_isConnected
-- Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.Constructor
Goal:
C₁ : Type u_1
C₂ : Type u_2
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
W₁ : MorphismProperty.{v_1, u_1} C₁
W₂ : MorphismProperty.{v_2, u_2} C₂
Φ : LocalizerMorphism W₁ W₂
inst_2 : ∀ (X₂ : C₂), IsConnected (Φ.RightResolution (W₁ := W₁) (W₂ := W₂) X₂)
inst_3 : Φ.arrow (W₁ := W₁) (W₂ := W₂).HasRightResolutions (W₁ := W₁.arrow) (W₂ := W₂.arrow)
inst_4 : W₂.ContainsIdentities
D : Type u_3
inst_5 : Category.{v_3, u_3} D
L : Functor.{v_2, v_3, u_2, u_3} C₂ D
inst_6 : L.IsLocalization W₂
X₂ : C₂
X₃ : D
y : L.obj X₂ ⟶ X₃
w : TwoSquare (Φ.functor (W₁ := W₁) (W₂ := W₂)) (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L) L (𝟭 D) :=
  TwoSquare.mk (Φ.functor (W₁ := W₁) (W₂ := W₂)) (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L) L (𝟭 D)
    (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L).rightUnitor.inv
this_1 : Nonempty (w.CostructuredArrowDownwards y)
this :
  ∀ (X : w.CostructuredArrowDownwards y),
    ∃ (Y : Φ.RightResolution (W₁ := W₁) (W₂ := W₂) X₂),
      Zigzag X ((fromRightResolution (W₁ := W₁) (W₂ := W₂) Φ L y).obj Y)
X X' :
  (TwoSquare.mk (Φ.functor (W₁ := W₁) (W₂ := W₂)) (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L) L (𝟭 D)
        (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L).rightUnitor.inv).CostructuredArrowDownwards
    y
obtain :
  ∀ (Y : Φ.RightResolution (W₁ := W₁) (W₂ := W₂) X₂)
    (hX : Zigzag X ((fromRightResolution (W₁ := W₁) (W₂ := W₂) Φ L y).obj Y)), Zigzag X X'
⊢ Zigzag X X'

Tactic:
obtain ⟨Y, hX⟩ := this X
-- Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.Constructor
Goal:
C₁ : Type u_1
C₂ : Type u_2
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
W₁ : MorphismProperty.{v_1, u_1} C₁
W₂ : MorphismProperty.{v_2, u_2} C₂
Φ : LocalizerMorphism W₁ W₂
inst_2 : ∀ (X₂ : C₂), IsConnected (Φ.RightResolution (W₁ := W₁) (W₂ := W₂) X₂)
inst_3 : Φ.arrow (W₁ := W₁) (W₂ := W₂).HasRightResolutions (W₁ := W₁.arrow) (W₂ := W₂.arrow)
inst_4 : W₂.ContainsIdentities
D : Type u_3
inst_5 : Category.{v_3, u_3} D
L : Functor.{v_2, v_3, u_2, u_3} C₂ D
inst_6 : L.IsLocalization W₂
X₂ : C₂
X₃ : D
y : L.obj X₂ ⟶ X₃
w : TwoSquare (Φ.functor (W₁ := W₁) (W₂ := W₂)) (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L) L (𝟭 D) :=
  TwoSquare.mk (Φ.functor (W₁ := W₁) (W₂ := W₂)) (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L) L (𝟭 D)
    (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L).rightUnitor.inv
this_1 : Nonempty (w.CostructuredArrowDownwards y)
this :
  ∀ (X : w.CostructuredArrowDownwards y),
    ∃ (Y : Φ.RightResolution (W₁ := W₁) (W₂ := W₂) X₂),
      Zigzag X ((fromRightResolution (W₁ := W₁) (W₂ := W₂) Φ L y).obj Y)
X X' :
  (TwoSquare.mk (Φ.functor (W₁ := W₁) (W₂ := W₂)) (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L) L (𝟭 D)
        (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L).rightUnitor.inv).CostructuredArrowDownwards
    y
Y : Φ.RightResolution (W₁ := W₁) (W₂ := W₂) X₂
hX : Zigzag X ((fromRightResolution (W₁ := W₁) (W₂ := W₂) Φ L y).obj Y)
obtain :
  ∀ (Y' : Φ.RightResolution (W₁ := W₁) (W₂ := W₂) X₂)
    (hX' : Zigzag X' ((fromRightResolution (W₁ := W₁) (W₂ := W₂) Φ L y).obj Y')), Zigzag X X'
⊢ Zigzag X X'

Tactic:
obtain ⟨Y', hX'⟩ := this X'
-- Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.Constructor
Goal:
C₁ : Type u_1
C₂ : Type u_2
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
W₁ : MorphismProperty.{v_1, u_1} C₁
W₂ : MorphismProperty.{v_2, u_2} C₂
Φ : LocalizerMorphism W₁ W₂
inst_2 : ∀ (X₂ : C₂), IsConnected (Φ.RightResolution (W₁ := W₁) (W₂ := W₂) X₂)
inst_3 : Φ.arrow (W₁ := W₁) (W₂ := W₂).HasRightResolutions (W₁ := W₁.arrow) (W₂ := W₂.arrow)
inst_4 : W₂.ContainsIdentities
D : Type u_3
inst_5 : Category.{v_3, u_3} D
L : Functor.{v_2, v_3, u_2, u_3} C₂ D
inst_6 : L.IsLocalization W₂
X₂ : C₂
X₃ : D
y : L.obj X₂ ⟶ X₃
w : TwoSquare (Φ.functor (W₁ := W₁) (W₂ := W₂)) (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L) L (𝟭 D) :=
  TwoSquare.mk (Φ.functor (W₁ := W₁) (W₂ := W₂)) (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L) L (𝟭 D)
    (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L).rightUnitor.inv
this_1 : Nonempty (w.CostructuredArrowDownwards y)
this :
  ∀ (X : w.CostructuredArrowDownwards y),
    ∃ (Y : Φ.RightResolution (W₁ := W₁) (W₂ := W₂) X₂),
      Zigzag X ((fromRightResolution (W₁ := W₁) (W₂ := W₂) Φ L y).obj Y)
X X' :
  (TwoSquare.mk (Φ.functor (W₁ := W₁) (W₂ := W₂)) (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L) L (𝟭 D)
        (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L).rightUnitor.inv).CostructuredArrowDownwards
    y
Y : Φ.RightResolution (W₁ := W₁) (W₂ := W₂) X₂
hX : Zigzag X ((fromRightResolution (W₁ := W₁) (W₂ := W₂) Φ L y).obj Y)
Y' : Φ.RightResolution (W₁ := W₁) (W₂ := W₂) X₂
hX' : Zigzag X' ((fromRightResolution (W₁ := W₁) (W₂ := W₂) Φ L y).obj Y')
⊢ Zigzag X X'

Tactic:
hX.trans ((zigzag_obj_of_zigzag _ (isPreconnected_zigzag Y Y')).trans hX'.symm)

Premises used: CategoryTheory.zigzag_obj_of_zigzag, CategoryTheory.isPreconnected_zigzag, CategoryTheory.Zigzag.trans, CategoryTheory.Zigzag.symm
-- Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.Constructor
Goal:
C₁ : Type u_1
C₂ : Type u_2
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
W₁ : MorphismProperty.{v_1, u_1} C₁
W₂ : MorphismProperty.{v_2, u_2} C₂
Φ : LocalizerMorphism W₁ W₂
inst_2 : ∀ (X₂ : C₂), IsConnected (Φ.RightResolution (W₁ := W₁) (W₂ := W₂) X₂)
inst_3 : Φ.arrow (W₁ := W₁) (W₂ := W₂).HasRightResolutions (W₁ := W₁.arrow) (W₂ := W₂.arrow)
inst_4 : W₂.ContainsIdentities
D : Type u_3
inst_5 : Category.{v_3, u_3} D
L : Functor.{v_2, v_3, u_2, u_3} C₂ D
inst_6 : L.IsLocalization W₂
X₂ : C₂
X₃ : D
y : L.obj X₂ ⟶ X₃
w : TwoSquare (Φ.functor (W₁ := W₁) (W₂ := W₂)) (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L) L (𝟭 D) :=
  TwoSquare.mk (Φ.functor (W₁ := W₁) (W₂ := W₂)) (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L) L (𝟭 D)
    (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L).rightUnitor.inv
this_1 : Nonempty (w.CostructuredArrowDownwards y)
this :
  ∀ (X : w.CostructuredArrowDownwards y),
    ∃ (Y : Φ.RightResolution (W₁ := W₁) (W₂ := W₂) X₂),
      Zigzag X ((fromRightResolution (W₁ := W₁) (W₂ := W₂) Φ L y).obj Y)
X X' :
  (TwoSquare.mk (Φ.functor (W₁ := W₁) (W₂ := W₂)) (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L) L (𝟭 D)
        (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L).rightUnitor.inv).CostructuredArrowDownwards
    y
Y : Φ.RightResolution (W₁ := W₁) (W₂ := W₂) X₂
hX : Zigzag X ((fromRightResolution (W₁ := W₁) (W₂ := W₂) Φ L y).obj Y)
Y' : Φ.RightResolution (W₁ := W₁) (W₂ := W₂) X₂
hX' : Zigzag X' ((fromRightResolution (W₁ := W₁) (W₂ := W₂) Φ L y).obj Y')
⊢ Zigzag X X'

Tactic:
exact hX.trans ((zigzag_obj_of_zigzag _ (isPreconnected_zigzag Y Y')).trans hX'.symm)

Premises used: CategoryTheory.zigzag_obj_of_zigzag, CategoryTheory.isPreconnected_zigzag, CategoryTheory.Zigzag.trans, CategoryTheory.Zigzag.symm
-- Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.Constructor
Goal:
C₁ : Type u_1
C₂ : Type u_2
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
W₁ : MorphismProperty.{v_1, u_1} C₁
W₂ : MorphismProperty.{v_2, u_2} C₂
Φ : LocalizerMorphism W₁ W₂
inst_2 : ∀ (X₂ : C₂), IsConnected (Φ.RightResolution (W₁ := W₁) (W₂ := W₂) X₂)
inst_3 : Φ.arrow (W₁ := W₁) (W₂ := W₂).HasRightResolutions (W₁ := W₁.arrow) (W₂ := W₂.arrow)
inst_4 : W₂.ContainsIdentities
D : Type u_3
inst_5 : Category.{v_3, u_3} D
L : Functor.{v_2, v_3, u_2, u_3} C₂ D
inst_6 : L.IsLocalization W₂
X₂ : C₂
X₃ : D
y : L.obj X₂ ⟶ X₃
w : TwoSquare (Φ.functor (W₁ := W₁) (W₂ := W₂)) (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L) L (𝟭 D) :=
  TwoSquare.mk (Φ.functor (W₁ := W₁) (W₂ := W₂)) (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L) L (𝟭 D)
    (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L).rightUnitor.inv
this : Nonempty (w.CostructuredArrowDownwards y)
suffices :
  ∀ (X : w.CostructuredArrowDownwards y),
    ∃ (Y : Φ.RightResolution (W₁ := W₁) (W₂ := W₂) X₂),
      Zigzag X ((fromRightResolution (W₁ := W₁) (W₂ := W₂) Φ L y).obj Y)
⊢ IsConnected
    ((TwoSquare.mk (Φ.functor (W₁ := W₁) (W₂ := W₂)) (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L) L (𝟭 D)
          (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L).rightUnitor.inv).CostructuredArrowDownwards
      y)

Tactic:
suffices ∀ (X : w.CostructuredArrowDownwards y),
      ∃ Y, Zigzag X ((fromRightResolution Φ L y).obj Y) by
    refine zigzag_isConnected (fun X X' => ?_)
    obtain ⟨Y, hX⟩ := this X
    obtain ⟨Y', hX'⟩ := this X'
    exact hX.trans ((zigzag_obj_of_zigzag _ (isPreconnected_zigzag Y Y')).trans hX'.symm)
-- Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.Constructor
Goal:
C₁ : Type u_1
C₂ : Type u_2
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
W₁ : MorphismProperty.{v_1, u_1} C₁
W₂ : MorphismProperty.{v_2, u_2} C₂
Φ : LocalizerMorphism W₁ W₂
inst_2 : ∀ (X₂ : C₂), IsConnected (Φ.RightResolution (W₁ := W₁) (W₂ := W₂) X₂)
inst_3 : Φ.arrow (W₁ := W₁) (W₂ := W₂).HasRightResolutions (W₁ := W₁.arrow) (W₂ := W₂.arrow)
inst_4 : W₂.ContainsIdentities
D : Type u_3
inst_5 : Category.{v_3, u_3} D
L : Functor.{v_2, v_3, u_2, u_3} C₂ D
inst_6 : L.IsLocalization W₂
X₂ : C₂
X₃ : D
y : L.obj X₂ ⟶ X₃
w : TwoSquare (Φ.functor (W₁ := W₁) (W₂ := W₂)) (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L) L (𝟭 D) :=
  TwoSquare.mk (Φ.functor (W₁ := W₁) (W₂ := W₂)) (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L) L (𝟭 D)
    (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L).rightUnitor.inv
this : Nonempty (w.CostructuredArrowDownwards y)
X : w.CostructuredArrowDownwards y
obtain :
  ∀ (c : C₁) (g : X₂ ⟶ Φ.functor (W₁ := W₁) (W₂ := W₂).obj c) (x : (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L).obj c ⟶ X₃)
    (fac : L.map g ≫ w.app c ≫ Functor.map (𝟭 D) x = y),
    ∃ (Y : Φ.RightResolution (W₁ := W₁) (W₂ := W₂) X₂),
      Zigzag (TwoSquare.CostructuredArrowDownwards.mk w y c g x fac)
        ((fromRightResolution (W₁ := W₁) (W₂ := W₂) Φ L y).obj Y)
⊢ ∃ (Y : Φ.RightResolution (W₁ := W₁) (W₂ := W₂) X₂), Zigzag X ((fromRightResolution (W₁ := W₁) (W₂ := W₂) Φ L y).obj Y)

Tactic:
obtain ⟨c, g, x, fac, rfl⟩ := TwoSquare.CostructuredArrowDownwards.mk_surjective X

Premises used: CategoryTheory.TwoSquare.CostructuredArrowDownwards.mk_surjective, CategoryTheory.Localization.fac, rfl
-- Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.Constructor
Goal:
C₁ : Type u_1
C₂ : Type u_2
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
W₁ : MorphismProperty.{v_1, u_1} C₁
W₂ : MorphismProperty.{v_2, u_2} C₂
Φ : LocalizerMorphism W₁ W₂
inst_2 : ∀ (X₂ : C₂), IsConnected (Φ.RightResolution (W₁ := W₁) (W₂ := W₂) X₂)
inst_3 : Φ.arrow (W₁ := W₁) (W₂ := W₂).HasRightResolutions (W₁ := W₁.arrow) (W₂ := W₂.arrow)
inst_4 : W₂.ContainsIdentities
D : Type u_3
inst_5 : Category.{v_3, u_3} D
L : Functor.{v_2, v_3, u_2, u_3} C₂ D
inst_6 : L.IsLocalization W₂
X₂ : C₂
X₃ : D
y : L.obj X₂ ⟶ X₃
w : TwoSquare (Φ.functor (W₁ := W₁) (W₂ := W₂)) (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L) L (𝟭 D) :=
  TwoSquare.mk (Φ.functor (W₁ := W₁) (W₂ := W₂)) (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L) L (𝟭 D)
    (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L).rightUnitor.inv
this : Nonempty (w.CostructuredArrowDownwards y)
c : C₁
g : X₂ ⟶ Φ.functor (W₁ := W₁) (W₂ := W₂).obj c
x : L.obj (Φ.functor (W₁ := W₁) (W₂ := W₂).obj c) ⟶ X₃
fac : L.map g ≫ 𝟙 (L.obj (Φ.functor (W₁ := W₁) (W₂ := W₂).obj c)) ≫ x = y
⊢ L.map g ≫ x = y

Tactic:
rw [id_comp] at fac

Premises used: CategoryTheory.Category.id_comp