awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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_1 : L.map g ≫ 𝟙 (L.obj (Φ.functor (W₁ := W₁) (W₂ := W₂).obj c)) ≫ x = y
fac : L.map g ≫ x = y
ρ : Φ.arrow (W₁ := W₁) (W₂ := W₂).RightResolution (W₁ := W₁.arrow) (W₂ := W₂.arrow) (Arrow.mk g) :=
  Classical.arbitrary (Φ.arrow (W₁ := W₁) (W₂ := W₂).RightResolution (W₁ := W₁.arrow) (W₂ := W₂.arrow) (Arrow.mk g))
⊢ ∃ (Y : Φ.RightResolution (W₁ := W₁) (W₂ := W₂) X₂),
    Zigzag (TwoSquare.CostructuredArrowDownwards.mk w y c g x fac_1)
      ((fromRightResolution (W₁ := W₁) (W₂ := W₂) Φ L y).obj Y)

Tactic:
⟨RightResolution.mk ρ.w.left ρ.hw.1, ?_⟩

Premises used: CategoryTheory.LocalizerMorphism.RightResolution.w, CategoryTheory.LocalizerMorphism.RightResolution.mk, And.left, CategoryTheory.LocalizerMorphism.RightResolution.hw, Exists.intro, CategoryTheory.Arrow.Hom.left
-- 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_1 : L.map g ≫ 𝟙 (L.obj (Φ.functor (W₁ := W₁) (W₂ := W₂).obj c)) ≫ x = y
fac : L.map g ≫ x = y
ρ : Φ.arrow (W₁ := W₁) (W₂ := W₂).RightResolution (W₁ := W₁.arrow) (W₂ := W₂.arrow) (Arrow.mk g) :=
  Classical.arbitrary (Φ.arrow (W₁ := W₁) (W₂ := W₂).RightResolution (W₁ := W₁.arrow) (W₂ := W₂.arrow) (Arrow.mk g))
refine :
  Zigzag (TwoSquare.CostructuredArrowDownwards.mk w y c g x fac_1)
    ((fromRightResolution (W₁ := W₁) (W₂ := W₂) Φ L y).obj
      (RightResolution.mk (W₁ := W₁) (W₂ := W₂) (Arrow.Hom.left (ρ.w (W₁ := W₁.arrow) (W₂ := W₂.arrow))) ⋯))
⊢ ∃ (Y : Φ.RightResolution (W₁ := W₁) (W₂ := W₂) X₂),
    Zigzag (TwoSquare.CostructuredArrowDownwards.mk w y c g x fac_1)
      ((fromRightResolution (W₁ := W₁) (W₂ := W₂) Φ L y).obj Y)

Tactic:
refine ⟨RightResolution.mk ρ.w.left ρ.hw.1, ?_⟩
-- 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_1 : L.map g ≫ 𝟙 (L.obj (Φ.functor (W₁ := W₁) (W₂ := W₂).obj c)) ≫ x = y
fac : L.map g ≫ x = y
ρ : Φ.arrow (W₁ := W₁) (W₂ := W₂).RightResolution (W₁ := W₁.arrow) (W₂ := W₂.arrow) (Arrow.mk g) :=
  Classical.arbitrary (Φ.arrow (W₁ := W₁) (W₂ := W₂).RightResolution (W₁ := W₁.arrow) (W₂ := W₂.arrow) (Arrow.mk g))
⊢ Zigzag
    ((fromRightResolution (W₁ := W₁) (W₂ := W₂) Φ L x ⋙ w.costructuredArrowDownwardsPrecomp x y g fac).obj
      (RightResolution.mk (W₁ := W₁) (W₂ := W₂) (𝟙 (Φ.functor (W₁ := W₁) (W₂ := W₂).obj c)) ⋯))
    ((fromRightResolution (W₁ := W₁) (W₂ := W₂) Φ L x ⋙ w.costructuredArrowDownwardsPrecomp x y g fac).obj
      (RightResolution.mk (W₁ := W₁) (W₂ := W₂) (Arrow.Hom.right (ρ.w (W₁ := W₁.arrow) (W₂ := W₂.arrow))) ⋯))

Tactic:
have := zigzag_obj_of_zigzag
    (fromRightResolution Φ L x ⋙ w.costructuredArrowDownwardsPrecomp x y g fac)
      (isPreconnected_zigzag (RightResolution.mk (𝟙 _) (W₂.id_mem _))
        (RightResolution.mk ρ.w.right ρ.hw.2))
-- 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)
c : C₁
g : X₂ ⟶ Φ.functor (W₁ := W₁) (W₂ := W₂).obj c
x : L.obj (Φ.functor (W₁ := W₁) (W₂ := W₂).obj c) ⟶ X₃
fac_1 : L.map g ≫ 𝟙 (L.obj (Φ.functor (W₁ := W₁) (W₂ := W₂).obj c)) ≫ x = y
fac : L.map g ≫ x = y
ρ : Φ.arrow (W₁ := W₁) (W₂ := W₂).RightResolution (W₁ := W₁.arrow) (W₂ := W₂.arrow) (Arrow.mk g) :=
  Classical.arbitrary (Φ.arrow (W₁ := W₁) (W₂ := W₂).RightResolution (W₁ := W₁.arrow) (W₂ := W₂.arrow) (Arrow.mk g))
this :
  Zigzag
    ((fromRightResolution (W₁ := W₁) (W₂ := W₂) Φ L x ⋙ w.costructuredArrowDownwardsPrecomp x y g fac).obj
      (RightResolution.mk (W₁ := W₁) (W₂ := W₂) (𝟙 (Φ.functor (W₁ := W₁) (W₂ := W₂).obj c)) ⋯))
    ((fromRightResolution (W₁ := W₁) (W₂ := W₂) Φ L x ⋙ w.costructuredArrowDownwardsPrecomp x y g fac).obj
      (RightResolution.mk (W₁ := W₁) (W₂ := W₂) (Arrow.Hom.right (ρ.w (W₁ := W₁.arrow) (W₂ := W₂.arrow))) ⋯))
⊢ Zigzag (TwoSquare.CostructuredArrowDownwards.mk w y c g x fac_1)
    ((fromRightResolution (W₁ := W₁) (W₂ := W₂) Φ L y).obj
      (RightResolution.mk (W₁ := W₁) (W₂ := W₂) (Arrow.Hom.left (ρ.w (W₁ := W₁.arrow) (W₂ := W₂.arrow))) ⋯))

Tactic:
Zigzag.trans ?_ (Zigzag.trans this ?_)

Premises used: CategoryTheory.Zigzag.trans
-- 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)
c : C₁
g : X₂ ⟶ Φ.functor (W₁ := W₁) (W₂ := W₂).obj c
x : L.obj (Φ.functor (W₁ := W₁) (W₂ := W₂).obj c) ⟶ X₃
fac_1 : L.map g ≫ 𝟙 (L.obj (Φ.functor (W₁ := W₁) (W₂ := W₂).obj c)) ≫ x = y
fac : L.map g ≫ x = y
ρ : Φ.arrow (W₁ := W₁) (W₂ := W₂).RightResolution (W₁ := W₁.arrow) (W₂ := W₂.arrow) (Arrow.mk g) :=
  Classical.arbitrary (Φ.arrow (W₁ := W₁) (W₂ := W₂).RightResolution (W₁ := W₁.arrow) (W₂ := W₂.arrow) (Arrow.mk g))
this :
  Zigzag
    ((fromRightResolution (W₁ := W₁) (W₂ := W₂) Φ L x ⋙ w.costructuredArrowDownwardsPrecomp x y g fac).obj
      (RightResolution.mk (W₁ := W₁) (W₂ := W₂) (𝟙 (Φ.functor (W₁ := W₁) (W₂ := W₂).obj c)) ⋯))
    ((fromRightResolution (W₁ := W₁) (W₂ := W₂) Φ L x ⋙ w.costructuredArrowDownwardsPrecomp x y g fac).obj
      (RightResolution.mk (W₁ := W₁) (W₂ := W₂) (Arrow.Hom.right (ρ.w (W₁ := W₁.arrow) (W₂ := W₂.arrow))) ⋯))
refine_1 :
  Zigzag (TwoSquare.CostructuredArrowDownwards.mk w y c g x fac_1)
    ((fromRightResolution (W₁ := W₁) (W₂ := W₂) Φ L x ⋙ w.costructuredArrowDownwardsPrecomp x y g fac).obj
      (RightResolution.mk (W₁ := W₁) (W₂ := W₂) (𝟙 (Φ.functor (W₁ := W₁) (W₂ := W₂).obj c)) ⋯))
refine_2 :
  Zigzag
    ((fromRightResolution (W₁ := W₁) (W₂ := W₂) Φ L x ⋙ w.costructuredArrowDownwardsPrecomp x y g fac).obj
      (RightResolution.mk (W₁ := W₁) (W₂ := W₂) (Arrow.Hom.right (ρ.w (W₁ := W₁.arrow) (W₂ := W₂.arrow))) ⋯))
    ((fromRightResolution (W₁ := W₁) (W₂ := W₂) Φ L y).obj
      (RightResolution.mk (W₁ := W₁) (W₂ := W₂) (Arrow.Hom.left (ρ.w (W₁ := W₁.arrow) (W₂ := W₂.arrow))) ⋯))
⊢ Zigzag (TwoSquare.CostructuredArrowDownwards.mk w y c g x fac_1)
    ((fromRightResolution (W₁ := W₁) (W₂ := W₂) Φ L y).obj
      (RightResolution.mk (W₁ := W₁) (W₂ := W₂) (Arrow.Hom.left (ρ.w (W₁ := W₁.arrow) (W₂ := W₂.arrow))) ⋯))

Tactic:
refine Zigzag.trans ?_ (Zigzag.trans this ?_)

Premises used: CategoryTheory.Zigzag.trans
-- 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)
c : C₁
g : X₂ ⟶ Φ.functor (W₁ := W₁) (W₂ := W₂).obj c
x : L.obj (Φ.functor (W₁ := W₁) (W₂ := W₂).obj c) ⟶ X₃
fac_1 : L.map g ≫ 𝟙 (L.obj (Φ.functor (W₁ := W₁) (W₂ := W₂).obj c)) ≫ x = y
fac : L.map g ≫ x = y
ρ : Φ.arrow (W₁ := W₁) (W₂ := W₂).RightResolution (W₁ := W₁.arrow) (W₂ := W₂.arrow) (Arrow.mk g) :=
  Classical.arbitrary (Φ.arrow (W₁ := W₁) (W₂ := W₂).RightResolution (W₁ := W₁.arrow) (W₂ := W₂.arrow) (Arrow.mk g))
this :
  Zigzag
    ((fromRightResolution (W₁ := W₁) (W₂ := W₂) Φ L x ⋙ w.costructuredArrowDownwardsPrecomp x y g fac).obj
      (RightResolution.mk (W₁ := W₁) (W₂ := W₂) (𝟙 (Φ.functor (W₁ := W₁) (W₂ := W₂).obj c)) ⋯))
    ((fromRightResolution (W₁ := W₁) (W₂ := W₂) Φ L x ⋙ w.costructuredArrowDownwardsPrecomp x y g fac).obj
      (RightResolution.mk (W₁ := W₁) (W₂ := W₂) (Arrow.Hom.right (ρ.w (W₁ := W₁.arrow) (W₂ := W₂.arrow))) ⋯))
⊢ TwoSquare.CostructuredArrowDownwards.mk w y c g x fac_1 =
    (fromRightResolution (W₁ := W₁) (W₂ := W₂) Φ L x ⋙ w.costructuredArrowDownwardsPrecomp x y g fac).obj
      (RightResolution.mk (W₁ := W₁) (W₂ := W₂) (𝟙 (Φ.functor (W₁ := W₁) (W₂ := W₂).obj c)) ⋯)

Tactic:
simp
-- 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)
c : C₁
g : X₂ ⟶ Φ.functor (W₁ := W₁) (W₂ := W₂).obj c
x : L.obj (Φ.functor (W₁ := W₁) (W₂ := W₂).obj c) ⟶ X₃
fac_1 : L.map g ≫ 𝟙 (L.obj (Φ.functor (W₁ := W₁) (W₂ := W₂).obj c)) ≫ x = y
fac : L.map g ≫ x = y
ρ : Φ.arrow (W₁ := W₁) (W₂ := W₂).RightResolution (W₁ := W₁.arrow) (W₂ := W₂.arrow) (Arrow.mk g) :=
  Classical.arbitrary (Φ.arrow (W₁ := W₁) (W₂ := W₂).RightResolution (W₁ := W₁.arrow) (W₂ := W₂.arrow) (Arrow.mk g))
this :
  Zigzag
    ((fromRightResolution (W₁ := W₁) (W₂ := W₂) Φ L x ⋙ w.costructuredArrowDownwardsPrecomp x y g fac).obj
      (RightResolution.mk (W₁ := W₁) (W₂ := W₂) (𝟙 (Φ.functor (W₁ := W₁) (W₂ := W₂).obj c)) ⋯))
    ((fromRightResolution (W₁ := W₁) (W₂ := W₂) Φ L x ⋙ w.costructuredArrowDownwardsPrecomp x y g fac).obj
      (RightResolution.mk (W₁ := W₁) (W₂ := W₂) (Arrow.Hom.right (ρ.w (W₁ := W₁.arrow) (W₂ := W₂.arrow))) ⋯))
⊢ Zigzag (TwoSquare.CostructuredArrowDownwards.mk w y c g x fac_1)
    ((fromRightResolution (W₁ := W₁) (W₂ := W₂) Φ L x ⋙ w.costructuredArrowDownwardsPrecomp x y g fac).obj
      (RightResolution.mk (W₁ := W₁) (W₂ := W₂) (𝟙 (Φ.functor (W₁ := W₁) (W₂ := W₂).obj c)) ⋯))

Tactic:
exact Zigzag.of_hom (eqToHom (by simp))

Premises used: CategoryTheory.eqToHom, CategoryTheory.Zigzag.of_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
this_1 : 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_1 : L.map g ≫ 𝟙 (L.obj (Φ.functor (W₁ := W₁) (W₂ := W₂).obj c)) ≫ x = y
fac : L.map g ≫ x = y
ρ : Φ.arrow (W₁ := W₁) (W₂ := W₂).RightResolution (W₁ := W₁.arrow) (W₂ := W₂.arrow) (Arrow.mk g) :=
  Classical.arbitrary (Φ.arrow (W₁ := W₁) (W₂ := W₂).RightResolution (W₁ := W₁.arrow) (W₂ := W₂.arrow) (Arrow.mk g))
this :
  Zigzag
    ((fromRightResolution (W₁ := W₁) (W₂ := W₂) Φ L x ⋙ w.costructuredArrowDownwardsPrecomp x y g fac).obj
      (RightResolution.mk (W₁ := W₁) (W₂ := W₂) (𝟙 (Φ.functor (W₁ := W₁) (W₂ := W₂).obj c)) ⋯))
    ((fromRightResolution (W₁ := W₁) (W₂ := W₂) Φ L x ⋙ w.costructuredArrowDownwardsPrecomp x y g fac).obj
      (RightResolution.mk (W₁ := W₁) (W₂ := W₂) (Arrow.Hom.right (ρ.w (W₁ := W₁.arrow) (W₂ := W₂.arrow))) ⋯))
refine_2 :
  (fromRightResolution (W₁ := W₁) (W₂ := W₂) Φ L y).obj
      (RightResolution.mk (W₁ := W₁) (W₂ := W₂) (Arrow.Hom.left (ρ.w (W₁ := W₁.arrow) (W₂ := W₂.arrow))) ⋯) ⟶
    (fromRightResolution (W₁ := W₁) (W₂ := W₂) Φ L x ⋙ w.costructuredArrowDownwardsPrecomp x y g fac).obj
      (RightResolution.mk (W₁ := W₁) (W₂ := W₂) (Arrow.Hom.right (ρ.w (W₁ := W₁.arrow) (W₂ := W₂.arrow))) ⋯)
⊢ Zigzag
    ((fromRightResolution (W₁ := W₁) (W₂ := W₂) Φ L x ⋙ w.costructuredArrowDownwardsPrecomp x y g fac).obj
      (RightResolution.mk (W₁ := W₁) (W₂ := W₂) (Arrow.Hom.right (ρ.w (W₁ := W₁.arrow) (W₂ := W₂.arrow))) ⋯))
    ((fromRightResolution (W₁ := W₁) (W₂ := W₂) Φ L y).obj
      (RightResolution.mk (W₁ := W₁) (W₂ := W₂) (Arrow.Hom.left (ρ.w (W₁ := W₁.arrow) (W₂ := W₂.arrow))) ⋯))

Tactic:
apply Zigzag.of_inv

Premises used: CategoryTheory.Zigzag.of_inv
-- 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)
c : C₁
g : X₂ ⟶ Φ.functor (W₁ := W₁) (W₂ := W₂).obj c
x : L.obj (Φ.functor (W₁ := W₁) (W₂ := W₂).obj c) ⟶ X₃
fac_1 : L.map g ≫ 𝟙 (L.obj (Φ.functor (W₁ := W₁) (W₂ := W₂).obj c)) ≫ x = y
fac : L.map g ≫ x = y
ρ : Φ.arrow (W₁ := W₁) (W₂ := W₂).RightResolution (W₁ := W₁.arrow) (W₂ := W₂.arrow) (Arrow.mk g) :=
  Classical.arbitrary (Φ.arrow (W₁ := W₁) (W₂ := W₂).RightResolution (W₁ := W₁.arrow) (W₂ := W₂.arrow) (Arrow.mk g))
this :
  Zigzag
    ((fromRightResolution (W₁ := W₁) (W₂ := W₂) Φ L x ⋙ w.costructuredArrowDownwardsPrecomp x y g fac).obj
      (RightResolution.mk (W₁ := W₁) (W₂ := W₂) (𝟙 (Φ.functor (W₁ := W₁) (W₂ := W₂).obj c)) ⋯))
    ((fromRightResolution (W₁ := W₁) (W₂ := W₂) Φ L x ⋙ w.costructuredArrowDownwardsPrecomp x y g fac).obj
      (RightResolution.mk (W₁ := W₁) (W₂ := W₂) (Arrow.Hom.right (ρ.w (W₁ := W₁.arrow) (W₂ := W₂.arrow))) ⋯))
⊢ (CostructuredArrow.left
          ((fromRightResolution (W₁ := W₁) (W₂ := W₂) Φ L y).obj
            (RightResolution.mk (W₁ := W₁) (W₂ := W₂) (Arrow.Hom.left (ρ.w (W₁ := W₁.arrow) (W₂ := W₂.arrow)))
              ⋯))).hom ≫
      Φ.functor (W₁ := W₁) (W₂ := W₂).map ρ.X₁ (W₁ := W₁.arrow) (W₂ := W₂.arrow).hom =
    (CostructuredArrow.left
        ((fromRightResolution (W₁ := W₁) (W₂ := W₂) Φ L x ⋙ w.costructuredArrowDownwardsPrecomp x y g fac).obj
          (RightResolution.mk (W₁ := W₁) (W₂ := W₂) (Arrow.Hom.right (ρ.w (W₁ := W₁.arrow) (W₂ := W₂.arrow))) ⋯))).hom

Tactic:
simp
-- 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)
c : C₁
g : X₂ ⟶ Φ.functor (W₁ := W₁) (W₂ := W₂).obj c
x : L.obj (Φ.functor (W₁ := W₁) (W₂ := W₂).obj c) ⟶ X₃
fac_1 : L.map g ≫ 𝟙 (L.obj (Φ.functor (W₁ := W₁) (W₂ := W₂).obj c)) ≫ x = y
fac : L.map g ≫ x = y
ρ : Φ.arrow (W₁ := W₁) (W₂ := W₂).RightResolution (W₁ := W₁.arrow) (W₂ := W₂.arrow) (Arrow.mk g) :=
  Classical.arbitrary (Φ.arrow (W₁ := W₁) (W₂ := W₂).RightResolution (W₁ := W₁.arrow) (W₂ := W₂.arrow) (Arrow.mk g))
this :
  Zigzag
    ((fromRightResolution (W₁ := W₁) (W₂ := W₂) Φ L x ⋙ w.costructuredArrowDownwardsPrecomp x y g fac).obj
      (RightResolution.mk (W₁ := W₁) (W₂ := W₂) (𝟙 (Φ.functor (W₁ := W₁) (W₂ := W₂).obj c)) ⋯))
    ((fromRightResolution (W₁ := W₁) (W₂ := W₂) Φ L x ⋙ w.costructuredArrowDownwardsPrecomp x y g fac).obj
      (RightResolution.mk (W₁ := W₁) (W₂ := W₂) (Arrow.Hom.right (ρ.w (W₁ := W₁.arrow) (W₂ := W₂.arrow))) ⋯))
refine_2 :
  ((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 ρ.X₁ (W₁ := W₁.arrow) (W₂ := W₂.arrow).hom ⋯) ≫
      CostructuredArrow.hom
        ((fromRightResolution (W₁ := W₁) (W₂ := W₂) Φ L x ⋙ w.costructuredArrowDownwardsPrecomp x y g fac).obj
          (RightResolution.mk (W₁ := W₁) (W₂ := W₂) (Arrow.Hom.right (ρ.w (W₁ := W₁.arrow) (W₂ := W₂.arrow))) ⋯)) =
    CostructuredArrow.hom
      ((fromRightResolution (W₁ := W₁) (W₂ := W₂) Φ L y).obj
        (RightResolution.mk (W₁ := W₁) (W₂ := W₂) (Arrow.Hom.left (ρ.w (W₁ := W₁.arrow) (W₂ := W₂.arrow))) ⋯))
⊢ (fromRightResolution (W₁ := W₁) (W₂ := W₂) Φ L y).obj
      (RightResolution.mk (W₁ := W₁) (W₂ := W₂) (Arrow.Hom.left (ρ.w (W₁ := W₁.arrow) (W₂ := W₂.arrow))) ⋯) ⟶
    (fromRightResolution (W₁ := W₁) (W₂ := W₂) Φ L x ⋙ w.costructuredArrowDownwardsPrecomp x y g fac).obj
      (RightResolution.mk (W₁ := W₁) (W₂ := W₂) (Arrow.Hom.right (ρ.w (W₁ := W₁.arrow) (W₂ := W₂.arrow))) ⋯)

Tactic:
refine CostructuredArrow.homMk (StructuredArrow.homMk ρ.X₁.hom (by simp)) ?_

Premises used: CategoryTheory.StructuredArrow.homMk, CategoryTheory.CostructuredArrow.homMk