J : Type u₁
inst✝³ : Category J
K : Type u₂
inst✝² : Category K
C : Type u
inst✝¹ : Category C
F✝ F G : J ⥤ C
inst✝ : HasColimit F
α : G ≅ F
s : Cocone G
j : J
⊢ (α.hom.app j ≫ colimit.ι F j) ≫ (fun s => colimit.desc F ((Cocones.precompose α.inv).obj s)) s = s.ι.app j
J : Type u₁
inst✝³ : Category J
K : Type u₂
inst✝² : Category K
C : Type u
inst✝¹ : Category C
F✝ F G : J ⥤ C
inst✝ : HasColimit F
α : G ≅ F
s : Cocone G
j : J
⊢ ((Cocones.precompose α.hom).obj (colimit.cocone F)).ι.app j ≫
      (fun s => colimit.desc F ((Cocones.precompose α.inv).obj s)) s =
    s.ι.app j
rw [Cocones.precompose_obj_ι, NatTrans.comp_app, colimit.cocone_ι]
J : Type u₁
inst✝³ : Category J
K : Type u₂
inst✝² : Category K
C : Type u
inst✝¹ : Category C
F✝ F G : J ⥤ C
inst✝ : HasColimit F
α : G ≅ F
s : Cocone G
j : J
⊢ ((Cocones.precompose α.inv).obj s).ι.app j = (α.app j).inv ≫ s.ι.app j
J : Type u₁
inst✝³ : Category J
K : Type u₂
inst✝² : Category K
C : Type u
inst✝¹ : Category C
F✝ F G : J ⥤ C
inst✝ : HasColimit F
α : G ≅ F
s : Cocone G
j : J
⊢ (α.hom.app j ≫ colimit.ι F j) ≫ (fun s => colimit.desc F ((Cocones.precompose α.inv).obj s)) s = s.ι.app j
rw [Category.assoc, colimit.ι_desc, ← NatIso.app_hom, ← Iso.eq_inv_comp]
no goals
J : Type u₁
inst✝³ : Category J
K : Type u₂
inst✝² : Category K
C : Type u
inst✝¹ : Category C
F✝ F G : J ⥤ C
inst✝ : HasColimit F
α : G ≅ F
s : Cocone G
j : J
⊢ ((Cocones.precompose α.inv).obj s).ι.app j = (α.app j).inv ≫ s.ι.app j
rfl
case w
J : Type u₁
inst✝³ : Category J
K : Type u₂
inst✝² : Category K
C : Type u
inst✝¹ : Category C
F✝ F G : J ⥤ C
inst✝ : HasColimit F
α : G ≅ F
s : Cocone G
m : ((Cocones.precompose α.hom).obj (colimit.cocone F)).pt ⟶ s.pt
w : ∀ (j : J), ((Cocones.precompose α.hom).obj (colimit.cocone F)).ι.app j ≫ m = s.ι.app j
⊢ ∀ (j : J), colimit.ι F j ≫ m = colimit.ι F j ≫ (fun s => colimit.desc F ((Cocones.precompose α.inv).obj s)) s
J : Type u₁
inst✝³ : Category J
K : Type u₂
inst✝² : Category K
C : Type u
inst✝¹ : Category C
F✝ F G : J ⥤ C
inst✝ : HasColimit F
α : G ≅ F
s : Cocone G
m : ((Cocones.precompose α.hom).obj (colimit.cocone F)).pt ⟶ s.pt
w : ∀ (j : J), ((Cocones.precompose α.hom).obj (colimit.cocone F)).ι.app j ≫ m = s.ι.app j
⊢ m = (fun s => colimit.desc F ((Cocones.precompose α.inv).obj s)) s
apply colimit.hom_ext
case w
J : Type u₁
inst✝³ : Category J
K : Type u₂
inst✝² : Category K
C : Type u
inst✝¹ : Category C
F✝ F G : J ⥤ C
inst✝ : HasColimit F
α : G ≅ F
s : Cocone G
m : ((Cocones.precompose α.hom).obj (colimit.cocone F)).pt ⟶ s.pt
w : ∀ (j : J), ((Cocones.precompose α.hom).obj (colimit.cocone F)).ι.app j ≫ m = s.ι.app j
j : J
⊢ colimit.ι F j ≫ m = colimit.ι F j ≫ (fun s => colimit.desc F ((Cocones.precompose α.inv).obj s)) s
case w
J : Type u₁
inst✝³ : Category J
K : Type u₂
inst✝² : Category K
C : Type u
inst✝¹ : Category C
F✝ F G : J ⥤ C
inst✝ : HasColimit F
α : G ≅ F
s : Cocone G
m : ((Cocones.precompose α.hom).obj (colimit.cocone F)).pt ⟶ s.pt
w : ∀ (j : J), ((Cocones.precompose α.hom).obj (colimit.cocone F)).ι.app j ≫ m = s.ι.app j
⊢ ∀ (j : J), colimit.ι F j ≫ m = colimit.ι F j ≫ (fun s => colimit.desc F ((Cocones.precompose α.inv).obj s)) s
intro j
case w
J : Type u₁
inst✝³ : Category J
K : Type u₂
inst✝² : Category K
C : Type u
inst✝¹ : Category C
F✝ F G : J ⥤ C
inst✝ : HasColimit F
α : G ≅ F
s : Cocone G
m : ((Cocones.precompose α.hom).obj (colimit.cocone F)).pt ⟶ s.pt
w : ∀ (j : J), ((Cocones.precompose α.hom).obj (colimit.cocone F)).ι.app j ≫ m = s.ι.app j
j : J
⊢ (α.app j).hom ≫ colimit.ι F j ≫ m = s.ι.app j
case w
J : Type u₁
inst✝³ : Category J
K : Type u₂
inst✝² : Category K
C : Type u
inst✝¹ : Category C
F✝ F G : J ⥤ C
inst✝ : HasColimit F
α : G ≅ F
s : Cocone G
m : ((Cocones.precompose α.hom).obj (colimit.cocone F)).pt ⟶ s.pt
w : ∀ (j : J), ((Cocones.precompose α.hom).obj (colimit.cocone F)).ι.app j ≫ m = s.ι.app j
j : J
⊢ colimit.ι F j ≫ m = colimit.ι F j ≫ (fun s => colimit.desc F ((Cocones.precompose α.inv).obj s)) s
rw [colimit.ι_desc, Cocones.precompose_obj_ι, NatTrans.comp_app, ← NatIso.app_inv,
  Iso.eq_inv_comp]
no goals
case w
J : Type u₁
inst✝³ : Category J
K : Type u₂
inst✝² : Category K
C : Type u
inst✝¹ : Category C
F✝ F G : J ⥤ C
inst✝ : HasColimit F
α : G ≅ F
s : Cocone G
m : ((Cocones.precompose α.hom).obj (colimit.cocone F)).pt ⟶ s.pt
w : ∀ (j : J), ((Cocones.precompose α.hom).obj (colimit.cocone F)).ι.app j ≫ m = s.ι.app j
j : J
⊢ (α.app j).hom ≫ colimit.ι F j ≫ m = s.ι.app j
simpa using w j