-- 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
⊢ IsConnected (StructuredArrow d F)

Tactic:
have : Nonempty (StructuredArrow d F) := by
  have := (I d).inv PUnit.unit
  obtain ⟨j, y, rfl⟩ := Limits.Types.jointly_surjective'.{v, v} this
  exact ⟨StructuredArrow.mk y⟩

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 : Nonempty (StructuredArrow d F)
⊢ IsConnected (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₂
⊢ Zigzag { left := { as := PUnit.unit }, right := X₁, hom := f₁ }
    { left := { as := PUnit.unit }, right := X₂, hom := f₂ }

Tactic:
let y₁ := colimit.ι (F ⋙ coyoneda.obj (op d)) 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₂
y₁ : colimit (F ⋙ coyoneda.obj (op d)) := colimit.ι (F ⋙ coyoneda.obj (op d)) X₁ f₁
⊢ Zigzag { left := { as := PUnit.unit }, right := X₁, hom := f₁ }
    { left := { as := PUnit.unit }, right := X₂, hom := f₂ }

Proof state:
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₂

Tactic:
ext

Result:
no goals

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₂
⊢ Zigzag { left := { as := PUnit.unit }, right := X₁, hom := f₁ }
    { left := { as := PUnit.unit }, right := X₂, hom := f₂ }

Tactic:
have e : y₁ = y₂ := by
  apply (I d).toEquiv.injective
  ext

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₂
⊢ Zigzag { left := { as := PUnit.unit }, right := X₁, hom := f₁ }
    { left := { as := PUnit.unit }, right := X₂, hom := 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₂
y₁ : colimit (F ⋙ coyoneda.obj (op d)) := colimit.ι (F ⋙ coyoneda.obj (op d)) X₁ f₁
⊢ Zigzag { left := { as := PUnit.unit }, right := X₁, hom := f₁ }
    { left := { as := PUnit.unit }, right := X₂, hom := f₂ }

Tactic:
let y₂ := colimit.ι (F ⋙ coyoneda.obj (op d)) 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₂
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₂
⊢ Zigzag { left := { as := PUnit.unit }, right := X₁, hom := f₁ }
    { left := { as := PUnit.unit }, right := X₂, hom := f₂ }