-- Mathlib/CategoryTheory/Limits/Final.lean
theorem final_of_colimit_comp_coyoneda_iso_pUnit
    (I : ∀ d, colimit (F ⋙ coyoneda.obj (op d)) ≅ PUnit) : Final F :=
  ⟨fun d => by
    have : Nonempty (StructuredArrow d F)

Proof state:
C : Type v
inst✝¹ : Category.{v, v} C
D : Type u₁
inst✝ : Category.{v, u₁} D
F : C ⥤ D
I : (d : D) → colimit (F ⋙ coyoneda.obj (op d)) ≅ PUnit.{v + 1}
d : D
this : Nonempty (StructuredArrow d F)
⊢ IsConnected (StructuredArrow d F)

Tactic:
apply zigzag_isConnected

Result:
case h
C : Type v
inst✝¹ : Category.{v, v} C
D : Type u₁
inst✝ : Category.{v, u₁} D
F : C ⥤ D
I : (d : D) → colimit (F ⋙ coyoneda.obj (op d)) ≅ PUnit.{v + 1}
d : D
this : Nonempty (StructuredArrow d F)
⊢ ∀ (j₁ j₂ : StructuredArrow d F), Zigzag j₁ j₂

Proof state:
case h.mk.mk.unit.mk.mk.unit
C : Type v
inst✝¹ : Category.{v, v} C
D : Type u₁
inst✝ : Category.{v, u₁} D
F : C ⥤ D
I : (d : D) → colimit (F ⋙ coyoneda.obj (op d)) ≅ PUnit.{v + 1}
d : D
this : Nonempty (StructuredArrow d F)
X₁ : C
f₁ : (fromPUnit d).obj { as := PUnit.unit } ⟶ F.obj X₁
X₂ : C
f₂ : (fromPUnit d).obj { as := PUnit.unit } ⟶ F.obj X₂
y₁ : colimit (F ⋙ coyoneda.obj (op d)) := colimit.ι (F ⋙ coyoneda.obj (op d)) X₁ f₁
y₂ : colimit (F ⋙ coyoneda.obj (op d)) := colimit.ι (F ⋙ coyoneda.obj (op d)) X₂ f₂
e : y₁ = y₂
t : Relation.EqvGen (Types.Quot.Rel (F ⋙ coyoneda.obj (op d))) ⟨X₁, f₁⟩ ⟨X₂, f₂⟩
⊢ Zigzag { left := { as := PUnit.unit }, right := X₁, hom := f₁ }
    { left := { as := PUnit.unit }, right := X₂, hom := f₂ }

Tactic:
clear e y₁ y₂

Result:
case h.mk.mk.unit.mk.mk.unit
C : Type v
inst✝¹ : Category.{v, v} C
D : Type u₁
inst✝ : Category.{v, u₁} D
F : C ⥤ D
I : (d : D) → colimit (F ⋙ coyoneda.obj (op d)) ≅ PUnit.{v + 1}
d : D
this : Nonempty (StructuredArrow d F)
X₁ : C
f₁ : (fromPUnit d).obj { as := PUnit.unit } ⟶ F.obj X₁
X₂ : C
f₂ : (fromPUnit d).obj { as := PUnit.unit } ⟶ F.obj X₂
t : Relation.EqvGen (Types.Quot.Rel (F ⋙ coyoneda.obj (op d))) ⟨X₁, f₁⟩ ⟨X₂, f₂⟩
⊢ Zigzag { left := { as := PUnit.unit }, right := X₁, hom := f₁ }
    { left := { as := PUnit.unit }, right := X₂, hom := f₂ }

Proof state:
case intro.intro
C : Type v
inst✝¹ : Category.{v, v} C
D : Type u₁
inst✝ : Category.{v, u₁} D
F : C ⥤ D
I : (d : D) → colimit (F ⋙ coyoneda.obj (op d)) ≅ PUnit.{v + 1}
d : D
j : C
y : (F ⋙ coyoneda.obj (op d)).obj j
⊢ Nonempty (StructuredArrow d F)

Tactic:
exact ⟨StructuredArrow.mk y⟩

Result:
no goals

Proof state:
C : Type v
inst✝¹ : Category.{v, v} C
D : Type u₁
inst✝ : Category.{v, u₁} D
F : C ⥤ D
I : (d : D) → colimit (F ⋙ coyoneda.obj (op d)) ≅ PUnit.{v + 1}
d : D
⊢ Nonempty (StructuredArrow d F)

Tactic:
have := (I d).inv PUnit.unit

Result:
C : Type v
inst✝¹ : Category.{v, v} C
D : Type u₁
inst✝ : Category.{v, u₁} D
F : C ⥤ D
I : (d : D) → colimit (F ⋙ coyoneda.obj (op d)) ≅ PUnit.{v + 1}
d : D
this : colimit (F ⋙ coyoneda.obj (op d))
⊢ Nonempty (StructuredArrow d F)

Proof state:
case h.mk.mk.unit.mk.mk.unit
C : Type v
inst✝¹ : Category.{v, v} C
D : Type u₁
inst✝ : Category.{v, u₁} D
F : C ⥤ D
I : (d : D) → colimit (F ⋙ coyoneda.obj (op d)) ≅ PUnit.{v + 1}
d : D
this : Nonempty (StructuredArrow d F)
X₁ : C
f₁ : (fromPUnit d).obj { as := PUnit.unit } ⟶ F.obj X₁
X₂ : C
f₂ : (fromPUnit d).obj { as := PUnit.unit } ⟶ F.obj X₂
t : Relation.EqvGen (Types.Quot.Rel (F ⋙ coyoneda.obj (op d))) ⟨X₁, f₁⟩ ⟨X₂, f₂⟩
⊢ Zigzag { left := { as := PUnit.unit }, right := X₁, hom := f₁ }
    { left := { as := PUnit.unit }, right := X₂, hom := f₂ }

Tactic:
exact Final.zigzag_of_eqvGen_quot_rel t

Result:
no goals

Proof state:
case h
C : Type v
inst✝¹ : Category.{v, v} C
D : Type u₁
inst✝ : Category.{v, u₁} D
F : C ⥤ D
I : (d : D) → colimit (F ⋙ coyoneda.obj (op d)) ≅ PUnit.{v + 1}
d : D
this : Nonempty (StructuredArrow d F)
⊢ ∀ (j₁ j₂ : StructuredArrow d F), Zigzag j₁ j₂

Tactic:
rintro ⟨⟨⟨⟩⟩, X₁, f₁⟩ ⟨⟨⟨⟩⟩, X₂, f₂⟩

Result:
case h.mk.mk.unit.mk.mk.unit
C : Type v
inst✝¹ : Category.{v, v} C
D : Type u₁
inst✝ : Category.{v, u₁} D
F : C ⥤ D
I : (d : D) → colimit (F ⋙ coyoneda.obj (op d)) ≅ PUnit.{v + 1}
d : D
this : Nonempty (StructuredArrow d F)
X₁ : C
f₁ : (fromPUnit d).obj { as := PUnit.unit } ⟶ F.obj X₁
X₂ : C
f₂ : (fromPUnit d).obj { as := PUnit.unit } ⟶ F.obj X₂
⊢ Zigzag { left := { as := PUnit.unit }, right := X₁, hom := f₁ }
    { left := { as := PUnit.unit }, right := X₂, hom := f₂ }

Proof state:
C : Type v
inst✝¹ : Category.{v, v} C
D : Type u₁
inst✝ : Category.{v, u₁} D
F : C ⥤ D
I : (d : D) → colimit (F ⋙ coyoneda.obj (op d)) ≅ PUnit.{v + 1}
d : D
this : Nonempty (StructuredArrow d F)
X₁ : C
f₁ : (fromPUnit d).obj { as := PUnit.unit } ⟶ F.obj X₁
X₂ : C
f₂ : (fromPUnit d).obj { as := PUnit.unit } ⟶ F.obj X₂
y₁ : colimit (F ⋙ coyoneda.obj (op d)) := colimit.ι (F ⋙ coyoneda.obj (op d)) X₁ f₁
y₂ : colimit (F ⋙ coyoneda.obj (op d)) := colimit.ι (F ⋙ coyoneda.obj (op d)) X₂ f₂
⊢ y₁ = y₂

Tactic:
apply (I d).toEquiv.injective

Result:
case a
C : Type v
inst✝¹ : Category.{v, v} C
D : Type u₁
inst✝ : Category.{v, u₁} D
F : C ⥤ D
I : (d : D) → colimit (F ⋙ coyoneda.obj (op d)) ≅ PUnit.{v + 1}
d : D
this : Nonempty (StructuredArrow d F)
X₁ : C
f₁ : (fromPUnit d).obj { as := PUnit.unit } ⟶ F.obj X₁
X₂ : C
f₂ : (fromPUnit d).obj { as := PUnit.unit } ⟶ F.obj X₂
y₁ : colimit (F ⋙ coyoneda.obj (op d)) := colimit.ι (F ⋙ coyoneda.obj (op d)) X₁ f₁
y₂ : colimit (F ⋙ coyoneda.obj (op d)) := colimit.ι (F ⋙ coyoneda.obj (op d)) X₂ f₂
⊢ (I d).toEquiv y₁ = (I d).toEquiv y₂

Proof state:
case h.mk.mk.unit.mk.mk.unit
C : Type v
inst✝¹ : Category.{v, v} C
D : Type u₁
inst✝ : Category.{v, u₁} D
F : C ⥤ D
I : (d : D) → colimit (F ⋙ coyoneda.obj (op d)) ≅ PUnit.{v + 1}
d : D
this : Nonempty (StructuredArrow d F)
X₁ : C
f₁ : (fromPUnit d).obj { as := PUnit.unit } ⟶ F.obj X₁
X₂ : C
f₂ : (fromPUnit d).obj { as := PUnit.unit } ⟶ F.obj X₂
y₁ : colimit (F ⋙ coyoneda.obj (op d)) := colimit.ι (F ⋙ coyoneda.obj (op d)) X₁ f₁
y₂ : colimit (F ⋙ coyoneda.obj (op d)) := colimit.ι (F ⋙ coyoneda.obj (op d)) X₂ f₂
e : y₁ = y₂
⊢ Zigzag { left := { as := PUnit.unit }, right := X₁, hom := f₁ }
    { left := { as := PUnit.unit }, right := X₂, hom := f₂ }

Tactic:
have t := Types.colimit_eq.{v, v} e

Result:
case h.mk.mk.unit.mk.mk.unit
C : Type v
inst✝¹ : Category.{v, v} C
D : Type u₁
inst✝ : Category.{v, u₁} D
F : C ⥤ D
I : (d : D) → colimit (F ⋙ coyoneda.obj (op d)) ≅ PUnit.{v + 1}
d : D
this : Nonempty (StructuredArrow d F)
X₁ : C
f₁ : (fromPUnit d).obj { as := PUnit.unit } ⟶ F.obj X₁
X₂ : C
f₂ : (fromPUnit d).obj { as := PUnit.unit } ⟶ F.obj X₂
y₁ : colimit (F ⋙ coyoneda.obj (op d)) := colimit.ι (F ⋙ coyoneda.obj (op d)) X₁ f₁
y₂ : colimit (F ⋙ coyoneda.obj (op d)) := colimit.ι (F ⋙ coyoneda.obj (op d)) X₂ f₂
e : y₁ = y₂
t : Relation.EqvGen (Types.Quot.Rel (F ⋙ coyoneda.obj (op d))) ⟨X₁, f₁⟩ ⟨X₂, f₂⟩
⊢ Zigzag { left := { as := PUnit.unit }, right := X₁, hom := f₁ }
    { left := { as := PUnit.unit }, right := X₂, hom := f₂ }

Proof state:
C : Type v
inst✝¹ : Category.{v, v} C
D : Type u₁
inst✝ : Category.{v, u₁} D
F : C ⥤ D
I : (d : D) → colimit (F ⋙ coyoneda.obj (op d)) ≅ PUnit.{v + 1}
d : D
this : colimit (F ⋙ coyoneda.obj (op d))
⊢ Nonempty (StructuredArrow d F)

Tactic:
obtain ⟨j, y, rfl⟩ := Limits.Types.jointly_surjective'.{v, v} this

Result:
case intro.intro
C : Type v
inst✝¹ : Category.{v, v} C
D : Type u₁
inst✝ : Category.{v, u₁} D
F : C ⥤ D
I : (d : D) → colimit (F ⋙ coyoneda.obj (op d)) ≅ PUnit.{v + 1}
d : D
j : C
y : (F ⋙ coyoneda.obj (op d)).obj j
⊢ Nonempty (StructuredArrow d F)