Module: Mathlib.CategoryTheory.Limits.VanKampen

Goal state before:
pp: case e'_3
J : Type v'
inst✝⁸ : Category.{u', v'} J
C : Type u
inst✝⁷ : Category.{v, u} C
D : Type u_2
inst✝⁶ : Category.{v_2, u_2} D
inst✝⁵ : HasColimitsOfShape J C
Gl : C ⥤ D
Gr : D ⥤ C
adj : Gl ⊣ Gr
inst✝⁴ : Gr.Full
inst✝³ : Gr.Faithful
F : J ⥤ D
c : Cocone (F ⋙ Gr)
H : IsVanKampenColimit c
inst✝² : ∀ (X : D) (f : X ⟶ Gl.obj c.pt), HasPullback (Gr.map f) (adj.unit.app c.pt)
inst✝¹ : ∀ (X : D) (f : X ⟶ Gl.obj c.pt), PreservesLimit (cospan (Gr.map f) (adj.unit.app c.pt)) Gl
inst✝ : ∀ (X : C) (i : J) (f : X ⟶ c.pt), PreservesLimit (cospan f (c.ι.app i)) Gl
this✝¹ : PreservesLimitsOfSize.{?u.178, ?u.177, v_2, v, u_2, u} Gr
this✝ : PreservesColimitsOfSize.{u', v', v, v_2, u, u_2} Gl
F' : J ⥤ D
c' : Cocone F'
α : F' ⟶ (F ⋙ Gr) ⋙ Gl
f : c'.pt ⟶ (Gl.mapCocone c).pt
h : α ≫ (Gl.mapCocone c).ι = c'.ι ≫ (const J).map f
hα : NatTrans.Equifibered α
hc' : IsColimit c'
j : J
α' : F' ⟶ F
hα' : NatTrans.Equifibered α'
hα'' : ∀ (j : J), Gl.map (Gr.map (α'.app j)) = adj.counit.app (F'.1 j) ≫ α.app j
β : F' ⋙ Gr ⋙ Gl ≅ F' := F'.isoWhiskerLeft (asIso adj.counit) ≪≫ F'.rightUnitor
hl : IsColimit ((Cocone.precompose β.hom).obj c') := (IsColimit.precomposeHomEquiv β c').symm hc'
hr : IsColimit (Gl.mapCocone (colimit.cocone (F' ⋙ Gr))) := isColimitOfPreserves Gl (colimit.isColimit (F' ⋙ Gr))
this : α.app j = β.inv.app j ≫ Gl.map (Gr.map (α'.app j))
e_1✝ :
  (c'.pt ⟶ (Gl.mapCocone c).pt) =
    (((Cocone.precompose β.hom).obj c').pt ⟶ (Gl.mapCocone { pt := c.pt, ι := whiskerRight α' Gr ≫ c.ι }).pt)
⊢ f = hl.desc (Gl.mapCocone { pt := c.pt, ι := whiskerRight α' Gr ≫ c.ι })

Tactic:
apply hl.hom_ext

Goal state after:
case e'_3
J : Type v'
inst✝⁸ : Category.{u', v'} J
C : Type u
inst✝⁷ : Category.{v, u} C
D : Type u_2
inst✝⁶ : Category.{v_2, u_2} D
inst✝⁵ : HasColimitsOfShape J C
Gl : C ⥤ D
Gr : D ⥤ C
adj : Gl ⊣ Gr
inst✝⁴ : Gr.Full
inst✝³ : Gr.Faithful
F : J ⥤ D
c : Cocone (F ⋙ Gr)
H : IsVanKampenColimit c
inst✝² : ∀ (X : D) (f : X ⟶ Gl.obj c.pt), HasPullback (Gr.map f) (adj.unit.app c.pt)
inst✝¹ : ∀ (X : D) (f : X ⟶ Gl.obj c.pt), PreservesLimit (cospan (Gr.map f) (adj.unit.app c.pt)) Gl
inst✝ : ∀ (X : C) (i : J) (f : X ⟶ c.pt), PreservesLimit (cospan f (c.ι.app i)) Gl
this✝¹ : PreservesLimitsOfSize.{?u.178, ?u.177, v_2, v, u_2, u} Gr
this✝ : PreservesColimitsOfSize.{u', v', v, v_2, u, u_2} Gl
F' : J ⥤ D
c' : Cocone F'
α : F' ⟶ (F ⋙ Gr) ⋙ Gl
f : c'.pt ⟶ (Gl.mapCocone c).pt
h : α ≫ (Gl.mapCocone c).ι = c'.ι ≫ (const J).map f
hα : NatTrans.Equifibered α
hc' : IsColimit c'
j : J
α' : F' ⟶ F
hα' : NatTrans.Equifibered α'
hα'' : ∀ (j : J), Gl.map (Gr.map (α'.app j)) = adj.counit.app (F'.1 j) ≫ α.app j
β : F' ⋙ Gr ⋙ Gl ≅ F' := ⋯
hl : IsColimit ((Cocone.precompose β.hom).obj c') := ⋯
hr : IsColimit (Gl.mapCocone (colimit.cocone (F' ⋙ Gr))) := ⋯
this : α.app j = β.inv.app j ≫ Gl.map (Gr.map (α'.app j))
e_1✝ :
  (c'.pt ⟶ (Gl.mapCocone c).pt) =
    (((Cocone.precompose β.hom).obj c').pt ⟶ (Gl.mapCocone { pt := c.pt, ι := whiskerRight α' Gr ≫ c.ι }).pt)
⊢ ∀ (j : J),
    ((Cocone.precompose β.hom).obj c').ι.app j ≫ f =
      ((Cocone.precompose β.hom).obj c').ι.app j ≫ hl.desc (Gl.mapCocone { pt := c.pt, ι := whiskerRight α' Gr ≫ c.ι })