-- Mathlib/CategoryTheory/Limits/Final/ParallelPair.lean
lemma parallelPair_initial_mk' {X Y : C} (f g : X ⟶ Y)
    (h₁ : ∀ Z, Nonempty (X ⟶ Z))
    (h₂ : ∀ ⦃Z : C⦄ (i j : X ⟶ Z),
      Zigzag (J := CostructuredArrow (parallelPair f g) Z)
        (mk (Y := zero) i) (mk (Y := zero) j)) :
    (parallelPair f g).Initial where
  out Z

Proof state:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y : C
f g : X ⟶ Y
h₁ : ∀ (Z : C), Nonempty (X ⟶ Z)
h₂ : ∀ ⦃Z : C⦄ (i j : X ⟶ Z), Zigzag (mk i) (mk j)
Z : C
this✝ : Nonempty (CostructuredArrow (parallelPair f g) Z)
this : ∀ (x : CostructuredArrow (parallelPair f g) Z), Zigzag x (mk ⋯.some)
⊢ IsConnected (CostructuredArrow (parallelPair f g) Z)

Tactic:
exact zigzag_isConnected (fun x y => (this x).trans (this y).symm)

Result:
no goals

Proof state:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y : C
f g : X ⟶ Y
h₁ : ∀ (Z : C), Nonempty (X ⟶ Z)
h₂ : ∀ ⦃Z : C⦄ (i j : X ⟶ Z), Zigzag (mk i) (mk j)
Z : C
⊢ IsConnected (CostructuredArrow (parallelPair f g) Z)

Tactic:
have : Nonempty (CostructuredArrow (parallelPair f g) Z) :=
  ⟨mk (Y := zero) (h₁ Z).some⟩

Result:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y : C
f g : X ⟶ Y
h₁ : ∀ (Z : C), Nonempty (X ⟶ Z)
h₂ : ∀ ⦃Z : C⦄ (i j : X ⟶ Z), Zigzag (mk i) (mk j)
Z : C
this : Nonempty (CostructuredArrow (parallelPair f g) Z)
⊢ IsConnected (CostructuredArrow (parallelPair f g) Z)

Proof state:
case mk.zero.mk
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y : C
f g : X ⟶ Y
h₁ : ∀ (Z : C), Nonempty (X ⟶ Z)
h₂ : ∀ ⦃Z : C⦄ (i j : X ⟶ Z), Zigzag (mk i) (mk j)
Z : C
this : Nonempty (CostructuredArrow (parallelPair f g) Z)
as✝ : PUnit.{1}
φ : (parallelPair f g).obj zero ⟶ (Functor.fromPUnit Z).obj { as := as✝ }
⊢ Zigzag { left := zero, right := { as := as✝ }, hom := φ } (mk ⋯.some)

Tactic:
apply h₂

Result:
no goals

Proof state:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y : C
f g : X ⟶ Y
h₁ : ∀ (Z : C), Nonempty (X ⟶ Z)
h₂ : ∀ ⦃Z : C⦄ (i j : X ⟶ Z), Zigzag (mk i) (mk j)
Z : C
this : Nonempty (CostructuredArrow (parallelPair f g) Z)
⊢ ∀ (x : CostructuredArrow (parallelPair f g) Z), Zigzag x (mk ⋯.some)

Tactic:
rintro ⟨(_|_), ⟨⟩, φ⟩

Result:
case mk.zero.mk
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y : C
f g : X ⟶ Y
h₁ : ∀ (Z : C), Nonempty (X ⟶ Z)
h₂ : ∀ ⦃Z : C⦄ (i j : X ⟶ Z), Zigzag (mk i) (mk j)
Z : C
this : Nonempty (CostructuredArrow (parallelPair f g) Z)
as✝ : PUnit.{1}
φ : (parallelPair f g).obj zero ⟶ (Functor.fromPUnit Z).obj { as := as✝ }
⊢ Zigzag { left := zero, right := { as := as✝ }, hom := φ } (mk ⋯.some)

case mk.one.mk
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y : C
f g : X ⟶ Y
h₁ : ∀ (Z : C), Nonempty (X ⟶ Z)
h₂ : ∀ ⦃Z : C⦄ (i j : X ⟶ Z), Zigzag (mk i) (mk j)
Z : C
this : Nonempty (CostructuredArrow (parallelPair f g) Z)
as✝ : PUnit.{1}
φ : (parallelPair f g).obj one ⟶ (Functor.fromPUnit Z).obj { as := as✝ }
⊢ Zigzag { left := one, right := { as := as✝ }, hom := φ } (mk ⋯.some)

Proof state:
case mk.one.mk
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y : C
f g : X ⟶ Y
h₁ : ∀ (Z : C), Nonempty (X ⟶ Z)
h₂ : ∀ ⦃Z : C⦄ (i j : X ⟶ Z), Zigzag (mk i) (mk j)
Z : C
this : Nonempty (CostructuredArrow (parallelPair f g) Z)
as✝ : PUnit.{1}
φ : (parallelPair f g).obj one ⟶ (Functor.fromPUnit Z).obj { as := as✝ }
⊢ Zigzag { left := one, right := { as := as✝ }, hom := φ } (mk (f ≫ φ))

Tactic:
exact Zigzag.of_inv (homMk left)

Result:
no goals

Proof state:
case mk.one.mk
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y : C
f g : X ⟶ Y
h₁ : ∀ (Z : C), Nonempty (X ⟶ Z)
h₂ : ∀ ⦃Z : C⦄ (i j : X ⟶ Z), Zigzag (mk i) (mk j)
Z : C
this : Nonempty (CostructuredArrow (parallelPair f g) Z)
as✝ : PUnit.{1}
φ : (parallelPair f g).obj one ⟶ (Functor.fromPUnit Z).obj { as := as✝ }
⊢ Zigzag { left := one, right := { as := as✝ }, hom := φ } (mk ⋯.some)

Tactic:
refine Zigzag.trans ?_ (h₂ (f ≫ φ) _)

Result:
case mk.one.mk
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y : C
f g : X ⟶ Y
h₁ : ∀ (Z : C), Nonempty (X ⟶ Z)
h₂ : ∀ ⦃Z : C⦄ (i j : X ⟶ Z), Zigzag (mk i) (mk j)
Z : C
this : Nonempty (CostructuredArrow (parallelPair f g) Z)
as✝ : PUnit.{1}
φ : (parallelPair f g).obj one ⟶ (Functor.fromPUnit Z).obj { as := as✝ }
⊢ Zigzag { left := one, right := { as := as✝ }, hom := φ } (mk (f ≫ φ))