-- Mathlib/CategoryTheory/Limits/Final.lean
theorem zigzag_of_eqvGen_quot_rel {F : C ⥤ D} {d : D} {f₁ f₂ : ΣX, d ⟶ F.obj X}
    (t : Relation.EqvGen (Types.Quot.Rel.{v, v} (F ⋙ coyoneda.obj (op d))) f₁ f₂) :
    Zigzag (StructuredArrow.mk f₁.2) (StructuredArrow.mk f₂.2)

Proof state:
case refl
C : Type v
inst✝¹ : Category.{v, v} C
D : Type u₁
inst✝ : Category.{v, u₁} D
F : C ⥤ D
d : D
f₁ f₂ x✝ : (X : C) × (d ⟶ F.obj X)
⊢ Zigzag (StructuredArrow.mk x✝.snd) (StructuredArrow.mk x✝.snd)

Tactic:
fconstructor

Result:
no goals

Proof state:
case trans
C : Type v
inst✝¹ : Category.{v, v} C
D : Type u₁
inst✝ : Category.{v, u₁} D
F : C ⥤ D
d : D
f₁ f₂ x y z : (X : C) × (d ⟶ F.obj X)
a✝¹ : Relation.EqvGen (Types.Quot.Rel (F ⋙ coyoneda.obj (op d))) x y
a✝ : Relation.EqvGen (Types.Quot.Rel (F ⋙ coyoneda.obj (op d))) y z
ih₁ : Zigzag (StructuredArrow.mk x.snd) (StructuredArrow.mk y.snd)
ih₂ : Zigzag (StructuredArrow.mk y.snd) (StructuredArrow.mk z.snd)
⊢ Zigzag (StructuredArrow.mk x.snd) (StructuredArrow.mk z.snd)

Tactic:
apply Relation.ReflTransGen.trans

Result:
case trans.hab
C : Type v
inst✝¹ : Category.{v, v} C
D : Type u₁
inst✝ : Category.{v, u₁} D
F : C ⥤ D
d : D
f₁ f₂ x y z : (X : C) × (d ⟶ F.obj X)
a✝¹ : Relation.EqvGen (Types.Quot.Rel (F ⋙ coyoneda.obj (op d))) x y
a✝ : Relation.EqvGen (Types.Quot.Rel (F ⋙ coyoneda.obj (op d))) y z
ih₁ : Zigzag (StructuredArrow.mk x.snd) (StructuredArrow.mk y.snd)
ih₂ : Zigzag (StructuredArrow.mk y.snd) (StructuredArrow.mk z.snd)
⊢ Relation.ReflTransGen Zag (StructuredArrow.mk x.snd) ?trans.b

case trans.hbc
C : Type v
inst✝¹ : Category.{v, v} C
D : Type u₁
inst✝ : Category.{v, u₁} D
F : C ⥤ D
d : D
f₁ f₂ x y z : (X : C) × (d ⟶ F.obj X)
a✝¹ : Relation.EqvGen (Types.Quot.Rel (F ⋙ coyoneda.obj (op d))) x y
a✝ : Relation.EqvGen (Types.Quot.Rel (F ⋙ coyoneda.obj (op d))) y z
ih₁ : Zigzag (StructuredArrow.mk x.snd) (StructuredArrow.mk y.snd)
ih₂ : Zigzag (StructuredArrow.mk y.snd) (StructuredArrow.mk z.snd)
⊢ Relation.ReflTransGen Zag ?trans.b (StructuredArrow.mk z.snd)

case trans.b
C : Type v
inst✝¹ : Category.{v, v} C
D : Type u₁
inst✝ : Category.{v, u₁} D
F : C ⥤ D
d : D
f₁ f₂ x y z : (X : C) × (d ⟶ F.obj X)
a✝¹ : Relation.EqvGen (Types.Quot.Rel (F ⋙ coyoneda.obj (op d))) x y
a✝ : Relation.EqvGen (Types.Quot.Rel (F ⋙ coyoneda.obj (op d))) y z
ih₁ : Zigzag (StructuredArrow.mk x.snd) (StructuredArrow.mk y.snd)
ih₂ : Zigzag (StructuredArrow.mk y.snd) (StructuredArrow.mk z.snd)
⊢ StructuredArrow d F

Proof state:
case rel.intro
C : Type v
inst✝¹ : Category.{v, v} C
D : Type u₁
inst✝ : Category.{v, u₁} D
F : C ⥤ D
d : D
f₁ f₂ x y : (X : C) × (d ⟶ F.obj X)
f : x.fst ⟶ y.fst
w : y.snd = (F ⋙ coyoneda.obj (op d)).map f x.snd
⊢ Zigzag (StructuredArrow.mk x.snd) (StructuredArrow.mk y.snd)

Tactic:
fconstructor

Result:
case rel.intro.b
C : Type v
inst✝¹ : Category.{v, v} C
D : Type u₁
inst✝ : Category.{v, u₁} D
F : C ⥤ D
d : D
f₁ f₂ x y : (X : C) × (d ⟶ F.obj X)
f : x.fst ⟶ y.fst
w : y.snd = (F ⋙ coyoneda.obj (op d)).map f x.snd
⊢ StructuredArrow d F

case rel.intro.a
C : Type v
inst✝¹ : Category.{v, v} C
D : Type u₁
inst✝ : Category.{v, u₁} D
F : C ⥤ D
d : D
f₁ f₂ x y : (X : C) × (d ⟶ F.obj X)
f : x.fst ⟶ y.fst
w : y.snd = (F ⋙ coyoneda.obj (op d)).map f x.snd
⊢ Relation.ReflTransGen Zag (StructuredArrow.mk x.snd) ?rel.intro.b

case rel.intro.a
C : Type v
inst✝¹ : Category.{v, v} C
D : Type u₁
inst✝ : Category.{v, u₁} D
F : C ⥤ D
d : D
f₁ f₂ x y : (X : C) × (d ⟶ F.obj X)
f : x.fst ⟶ y.fst
w : y.snd = (F ⋙ coyoneda.obj (op d)).map f x.snd
⊢ Zag ?rel.intro.b (StructuredArrow.mk y.snd)

Proof state:
case rel.intro.a.h.val
C : Type v
inst✝¹ : Category.{v, v} C
D : Type u₁
inst✝ : Category.{v, u₁} D
F : C ⥤ D
d : D
f₁ f₂ x y : (X : C) × (d ⟶ F.obj X)
f : x.fst ⟶ y.fst
w : y.snd = (F ⋙ coyoneda.obj (op d)).map f x.snd
⊢ StructuredArrow.mk x.snd ⟶ StructuredArrow.mk y.snd

Tactic:
exact StructuredArrow.homMk f

Result:
no goals

Proof state:
case rel.intro.a
C : Type v
inst✝¹ : Category.{v, v} C
D : Type u₁
inst✝ : Category.{v, u₁} D
F : C ⥤ D
d : D
f₁ f₂ x y : (X : C) × (d ⟶ F.obj X)
f : x.fst ⟶ y.fst
w : y.snd = (F ⋙ coyoneda.obj (op d)).map f x.snd
⊢ Relation.ReflTransGen Zag (StructuredArrow.mk x.snd) ?rel.intro.b

Tactic:
fconstructor

Result:
no goals

Proof state:
case rel.intro.a.h
C : Type v
inst✝¹ : Category.{v, v} C
D : Type u₁
inst✝ : Category.{v, u₁} D
F : C ⥤ D
d : D
f₁ f₂ x y : (X : C) × (d ⟶ F.obj X)
f : x.fst ⟶ y.fst
w : y.snd = (F ⋙ coyoneda.obj (op d)).map f x.snd
⊢ Nonempty (StructuredArrow.mk x.snd ⟶ StructuredArrow.mk y.snd)

Tactic:
fconstructor

Result:
case rel.intro.a.h.val
C : Type v
inst✝¹ : Category.{v, v} C
D : Type u₁
inst✝ : Category.{v, u₁} D
F : C ⥤ D
d : D
f₁ f₂ x y : (X : C) × (d ⟶ F.obj X)
f : x.fst ⟶ y.fst
w : y.snd = (F ⋙ coyoneda.obj (op d)).map f x.snd
⊢ StructuredArrow.mk x.snd ⟶ StructuredArrow.mk y.snd

Proof state:
case symm.a
C : Type v
inst✝¹ : Category.{v, v} C
D : Type u₁
inst✝ : Category.{v, u₁} D
F : C ⥤ D
d : D
f₁ f₂ x y : (X : C) × (d ⟶ F.obj X)
a✝ : Relation.EqvGen (Types.Quot.Rel (F ⋙ coyoneda.obj (op d))) x y
ih : Zigzag (StructuredArrow.mk x.snd) (StructuredArrow.mk y.snd)
⊢ Zigzag (StructuredArrow.mk x.snd) (StructuredArrow.mk y.snd)

Tactic:
exact ih

Result:
no goals

Proof state:
case symm
C : Type v
inst✝¹ : Category.{v, v} C
D : Type u₁
inst✝ : Category.{v, u₁} D
F : C ⥤ D
d : D
f₁ f₂ x y : (X : C) × (d ⟶ F.obj X)
a✝ : Relation.EqvGen (Types.Quot.Rel (F ⋙ coyoneda.obj (op d))) x y
ih : Zigzag (StructuredArrow.mk x.snd) (StructuredArrow.mk y.snd)
⊢ Zigzag (StructuredArrow.mk y.snd) (StructuredArrow.mk x.snd)

Tactic:
apply zigzag_symmetric

Result:
case symm.a
C : Type v
inst✝¹ : Category.{v, v} C
D : Type u₁
inst✝ : Category.{v, u₁} D
F : C ⥤ D
d : D
f₁ f₂ x y : (X : C) × (d ⟶ F.obj X)
a✝ : Relation.EqvGen (Types.Quot.Rel (F ⋙ coyoneda.obj (op d))) x y
ih : Zigzag (StructuredArrow.mk x.snd) (StructuredArrow.mk y.snd)
⊢ Zigzag (StructuredArrow.mk x.snd) (StructuredArrow.mk y.snd)

Proof state:
case rel.intro.b
C : Type v
inst✝¹ : Category.{v, v} C
D : Type u₁
inst✝ : Category.{v, u₁} D
F : C ⥤ D
d : D
f₁ f₂ x y : (X : C) × (d ⟶ F.obj X)
f : x.fst ⟶ y.fst
w : y.snd = (F ⋙ coyoneda.obj (op d)).map f x.snd
⊢ StructuredArrow d F

case rel.intro.a
C : Type v
inst✝¹ : Category.{v, v} C
D : Type u₁
inst✝ : Category.{v, u₁} D
F : C ⥤ D
d : D
f₁ f₂ x y : (X : C) × (d ⟶ F.obj X)
f : x.fst ⟶ y.fst
w : y.snd = (F ⋙ coyoneda.obj (op d)).map f x.snd
⊢ Relation.ReflTransGen Zag (StructuredArrow.mk x.snd) ?rel.intro.b

case rel.intro.a
C : Type v
inst✝¹ : Category.{v, v} C
D : Type u₁
inst✝ : Category.{v, u₁} D
F : C ⥤ D
d : D
f₁ f₂ x y : (X : C) × (d ⟶ F.obj X)
f : x.fst ⟶ y.fst
w : y.snd = (F ⋙ coyoneda.obj (op d)).map f x.snd
⊢ Zag ?rel.intro.b (StructuredArrow.mk y.snd)

Tactic:
swap

Result:
case rel.intro.a
C : Type v
inst✝¹ : Category.{v, v} C
D : Type u₁
inst✝ : Category.{v, u₁} D
F : C ⥤ D
d : D
f₁ f₂ x y : (X : C) × (d ⟶ F.obj X)
f : x.fst ⟶ y.fst
w : y.snd = (F ⋙ coyoneda.obj (op d)).map f x.snd
⊢ Relation.ReflTransGen Zag (StructuredArrow.mk x.snd) ?rel.intro.b

case rel.intro.b
C : Type v
inst✝¹ : Category.{v, v} C
D : Type u₁
inst✝ : Category.{v, u₁} D
F : C ⥤ D
d : D
f₁ f₂ x y : (X : C) × (d ⟶ F.obj X)
f : x.fst ⟶ y.fst
w : y.snd = (F ⋙ coyoneda.obj (op d)).map f x.snd
⊢ StructuredArrow d F

case rel.intro.a
C : Type v
inst✝¹ : Category.{v, v} C
D : Type u₁
inst✝ : Category.{v, u₁} D
F : C ⥤ D
d : D
f₁ f₂ x y : (X : C) × (d ⟶ F.obj X)
f : x.fst ⟶ y.fst
w : y.snd = (F ⋙ coyoneda.obj (op d)).map f x.snd
⊢ Zag ?rel.intro.b (StructuredArrow.mk y.snd)