C : Type u₁
inst✝³ : Category C
J : Type u
inst✝² : Category 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)
C : Type u₁
inst✝³ : Category C
J : Type u
inst✝² : Category 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)
refine ⟨?_, by ext; simp⟩
C : Type u₁
inst✝³ : Category C
J : Type u
inst✝² : Category 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)
C : Type u₁
inst✝³ : Category C
J : Type u
inst✝² : Category 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)
dsimp
C : Type u₁
inst✝³ : Category C
J : Type u
inst✝² : Category 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)
C : Type u₁
inst✝³ : Category C
J : Type u
inst✝² : Category 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)
simp only [colimit.ι_desc, coconeOfDiagramInitial_pt, coconeOfDiagramInitial_ι_app,
Functor.const_obj_obj, IsInitial.to_self, Functor.map_id]
C : Type u₁
inst✝³ : Category C
J : Type u
inst✝² : Category 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 (_ : ∃ inv, 𝟙 (F.obj j) ≫ inv = 𝟙 (F.obj j) ∧ inv ≫ 𝟙 (F.obj j) = 𝟙 (F.obj j)) = 𝟙 (F.obj j)
C : Type u₁
inst✝³ : Category C
J : Type u
inst✝² : Category 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)
dsimp [inv]
C : Type u₁
inst✝³ : Category C
J : Type u
inst✝² : Category 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 (_ : ∃ x, (fun x => x = 𝟙 (F.obj j)) x) = 𝟙 (F.obj j)
C : Type u₁
inst✝³ : Category C
J : Type u
inst✝² : Category 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 (_ : ∃ inv, 𝟙 (F.obj j) ≫ inv = 𝟙 (F.obj j) ∧ inv ≫ 𝟙 (F.obj j) = 𝟙 (F.obj j)) = 𝟙 (F.obj j)
simp only [Category.id_comp, Category.comp_id, and_self]
no goals
C : Type u₁
inst✝³ : Category C
J : Type u
inst✝² : Category 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 (_ : ∃ x, (fun x => x = 𝟙 (F.obj j)) x) = 𝟙 (F.obj j)
apply @Classical.choose_spec _ (fun x => x = 𝟙 F.obj j) _
case w
C : Type u₁
inst✝³ : Category C
J : Type u
inst✝² : Category 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)
C : Type u₁
inst✝³ : Category C
J : Type u
inst✝² : Category 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)
ext
no goals
case w
C : Type u₁
inst✝³ : Category C
J : Type u
inst✝² : Category 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)
simp