-- Mathlib/CategoryTheory/Limits/Shapes/Terminal.lean
theorem isIso_ι_of_isInitial {j : J} (I : IsInitial j) (F : J ⥤ C) [HasColimit F]
    [∀ (i j : J) (f : i ⟶ j), IsIso (F.map f)] : IsIso (colimit.ι F j) :=
  ⟨⟨colimit.desc _ (coconeOfDiagramInitial I F), by
    refine ⟨?_, by ext; simp⟩
    dsimp; simp only [colimit.ι_desc, coconeOfDiagramInitial_pt, coconeOfDiagramInitial_ι_app,
      Functor.const_obj_obj, IsInitial.to_self, Functor.map_id]
    dsimp [inv]; simp only [Category.id_comp, Category.comp_id, and_self]
    apply @Classical.choose_spec _ (fun x => x = 𝟙 F.obj j) _
  ⟩⟩

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
J : Type u
inst✝² : Category.{v, u} J
j : J
I : IsInitial j
F : J ⥤ C
inst✝¹ : HasColimit F
inst✝ : ∀ (i j : J) (f : i ⟶ j), IsIso (F.map f)
⊢ inv (𝟙 (F.obj j)) = 𝟙 (F.obj j)

Tactic:
dsimp [inv]

Result:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
J : Type u
inst✝² : Category.{v, u} J
j : J
I : IsInitial j
F : J ⥤ C
inst✝¹ : HasColimit F
inst✝ : ∀ (i j : J) (f : i ⟶ j), IsIso (F.map f)
⊢ Classical.choose ⋯ = 𝟙 (F.obj j)

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
J : Type u
inst✝² : Category.{v, u} J
j : J
I : IsInitial j
F : J ⥤ C
inst✝¹ : HasColimit F
inst✝ : ∀ (i j : J) (f : i ⟶ j), IsIso (F.map f)
⊢ Classical.choose ⋯ = 𝟙 (F.obj j)

Tactic:
apply @Classical.choose_spec _ (fun x => x = 𝟙 F.obj j) _

Result:
no goals

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
J : Type u
inst✝² : Category.{v, u} J
j : J
I : IsInitial j
F : J ⥤ C
inst✝¹ : HasColimit F
inst✝ : ∀ (i j : J) (f : i ⟶ j), IsIso (F.map f)
⊢ colimit.ι F j ≫ colimit.desc F (coconeOfDiagramInitial I F) = 𝟙 (F.obj j) ∧
    colimit.desc F (coconeOfDiagramInitial I F) ≫ colimit.ι F j = 𝟙 (colimit F)

Tactic:
refine ⟨?_, by ext; simp⟩

Result:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
J : Type u
inst✝² : Category.{v, u} J
j : J
I : IsInitial j
F : J ⥤ C
inst✝¹ : HasColimit F
inst✝ : ∀ (i j : J) (f : i ⟶ j), IsIso (F.map f)
⊢ colimit.ι F j ≫ colimit.desc F (coconeOfDiagramInitial I F) = 𝟙 (F.obj j)

Proof state:
case w
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
J : Type u
inst✝² : Category.{v, u} J
j : J
I : IsInitial j
F : J ⥤ C
inst✝¹ : HasColimit F
inst✝ : ∀ (i j : J) (f : i ⟶ j), IsIso (F.map f)
j✝ : J
⊢ colimit.ι F j✝ ≫ colimit.desc F (coconeOfDiagramInitial I F) ≫ colimit.ι F j = colimit.ι F j✝ ≫ 𝟙 (colimit F)

Tactic:
simp

Result:
no goals

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
J : Type u
inst✝² : Category.{v, u} J
j : J
I : IsInitial j
F : J ⥤ C
inst✝¹ : HasColimit F
inst✝ : ∀ (i j : J) (f : i ⟶ j), IsIso (F.map f)
⊢ colimit.desc F (coconeOfDiagramInitial I F) ≫ colimit.ι F j = 𝟙 (colimit F)

Tactic:
ext

Result:
case w
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
J : Type u
inst✝² : Category.{v, u} J
j : J
I : IsInitial j
F : J ⥤ C
inst✝¹ : HasColimit F
inst✝ : ∀ (i j : J) (f : i ⟶ j), IsIso (F.map f)
j✝ : J
⊢ colimit.ι F j✝ ≫ colimit.desc F (coconeOfDiagramInitial I F) ≫ colimit.ι F j = colimit.ι F j✝ ≫ 𝟙 (colimit F)

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
J : Type u
inst✝² : Category.{v, u} J
j : J
I : IsInitial j
F : J ⥤ C
inst✝¹ : HasColimit F
inst✝ : ∀ (i j : J) (f : i ⟶ j), IsIso (F.map f)
⊢ colimit.ι F j ≫ colimit.desc F (coconeOfDiagramInitial I F) = 𝟙 (F.obj j)

Tactic:
simp only [colimit.ι_desc, coconeOfDiagramInitial_pt, coconeOfDiagramInitial_ι_app,
Functor.const_obj_obj, IsInitial.to_self, Functor.map_id]

Result:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
J : Type u
inst✝² : Category.{v, u} J
j : J
I : IsInitial j
F : J ⥤ C
inst✝¹ : HasColimit F
inst✝ : ∀ (i j : J) (f : i ⟶ j), IsIso (F.map f)
⊢ inv (𝟙 (F.obj j)) = 𝟙 (F.obj j)