awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
D : Type u_2
inst_2 : Category.{v_2, u_2} D
inst_3 : HasColimitsOfShape.{u', v', v, u} J C
Gl : Functor.{v, v_2, u, u_2} C D
Gr : Functor.{v_2, v, u_2, u} D C
adj : Gl ⊣ Gr
inst_4 : Gr.Full
inst_5 : Gr.Faithful
F : Functor.{u', v_2, v', u_2} J D
c : Cocone (F ⋙ Gr)
H : IsVanKampenColimit c
inst_6 : ∀ (X : D) (f : X ⟶ Gl.obj c.pt), HasPullback (Gr.map f) (adj.unit.app c.pt)
inst_7 : ∀ (X : D) (f : X ⟶ Gl.obj c.pt), PreservesLimit (cospan (Gr.map f) (adj.unit.app c.pt)) Gl
inst_8 : ∀ (X : C) (i : J) (f : X ⟶ c.pt), PreservesLimit (cospan f (c.ι.app i)) Gl
this_1 : PreservesLimitsOfSize.{v, v, v_2, v, u_2, u} Gr
this_2 : PreservesColimitsOfSize.{u', v', v, v_2, u, u_2} Gl
F' : Functor.{u', v_2, v', u_2} J D
c' : Cocone F'
α : F' ⟶ (F ⋙ Gr) ⋙ Gl
f : c'.pt ⟶ (Gl.mapCocone c).pt
h : α ≫ (Gl.mapCocone c).ι = c'.ι ≫ map (const J) f
hα : NatTrans.Equifibered α
hc' : IsColimit c'
j : J
α' : F' ⟶ F := α ≫ (F.associator Gr Gl).hom ≫ F.whiskerLeft adj.counit ≫ F.rightUnitor.hom
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 : (a : IsColimit c') → IsColimit ((Cocone.precompose β.hom).obj c')) hc'
hr : IsColimit (Gl.mapCocone (colimit.cocone (F' ⋙ Gr))) := isColimitOfPreserves Gl (colimit.isColimit (F' ⋙ Gr))
this_3 : α.app j = β.inv.app j ≫ Gl.map (Gr.map (α'.app j))
this_4 :
  f =
    (hl.coconePointUniqueUpToIso hr).hom ≫ Gl.map (colimit.desc (F' ⋙ Gr) { pt := c.pt, ι := whiskerRight α' Gr ≫ c.ι })
this :
  IsPullback (Gl.map ((colimit.cocone (F' ⋙ Gr)).ι.app j)) (Gl.map ((whiskerRight α' Gr).app j))
    (Gl.map (colimit.desc (F' ⋙ Gr) { pt := c.pt, ι := whiskerRight α' Gr ≫ c.ι })) (Gl.map (c.ι.app j))
refine_2 :
  IsPullback (c'.ι.app j) (β.inv.app j) (hl.coconePointUniqueUpToIso hr).hom
    (Gl.map ((colimit.cocone (F' ⋙ Gr)).ι.app j))
⊢ IsPullback (c'.ι.app j) (β.inv.app j ≫ Gl.map (Gr.map (α'.app j)))
    ((hl.coconePointUniqueUpToIso hr).hom ≫
      Gl.map (colimit.desc (F' ⋙ Gr) { pt := c.pt, ι := whiskerRight α' Gr ≫ c.ι }))
    ((Gl.mapCocone c).ι.app j)

Tactic:
convert! IsPullback.paste_vert _ this

Premises used: CategoryTheory.IsPullback.paste_vert
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
D : Type u_2
inst_2 : Category.{v_2, u_2} D
inst_3 : HasColimitsOfShape.{u', v', v, u} J C
Gl : Functor.{v, v_2, u, u_2} C D
Gr : Functor.{v_2, v, u_2, u} D C
adj : Gl ⊣ Gr
inst_4 : Gr.Full
inst_5 : Gr.Faithful
F : Functor.{u', v_2, v', u_2} J D
c : Cocone (F ⋙ Gr)
H : IsVanKampenColimit c
inst_6 : ∀ (X : D) (f : X ⟶ Gl.obj c.pt), HasPullback (Gr.map f) (adj.unit.app c.pt)
inst_7 : ∀ (X : D) (f : X ⟶ Gl.obj c.pt), PreservesLimit (cospan (Gr.map f) (adj.unit.app c.pt)) Gl
inst_8 : ∀ (X : C) (i : J) (f : X ⟶ c.pt), PreservesLimit (cospan f (c.ι.app i)) Gl
this_1 : PreservesLimitsOfSize.{v, v, v_2, v, u_2, u} Gr
this_2 : PreservesColimitsOfSize.{u', v', v, v_2, u, u_2} Gl
F' : Functor.{u', v_2, v', u_2} J D
c' : Cocone F'
α : F' ⟶ (F ⋙ Gr) ⋙ Gl
f : c'.pt ⟶ (Gl.mapCocone c).pt
h : α ≫ (Gl.mapCocone c).ι = c'.ι ≫ map (const J) f
hα : NatTrans.Equifibered α
hc' : IsColimit c'
j : J
α' : F' ⟶ F := α ≫ (F.associator Gr Gl).hom ≫ F.whiskerLeft adj.counit ≫ F.rightUnitor.hom
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 : (a : IsColimit c') → IsColimit ((Cocone.precompose β.hom).obj c')) hc'
hr : IsColimit (Gl.mapCocone (colimit.cocone (F' ⋙ Gr))) := isColimitOfPreserves Gl (colimit.isColimit (F' ⋙ Gr))
this_3 : α.app j = β.inv.app j ≫ Gl.map (Gr.map (α'.app j))
this_4 :
  f =
    (hl.coconePointUniqueUpToIso hr).hom ≫ Gl.map (colimit.desc (F' ⋙ Gr) { pt := c.pt, ι := whiskerRight α' Gr ≫ c.ι })
this :
  IsPullback (Gl.map ((colimit.cocone (F' ⋙ Gr)).ι.app j)) (Gl.map ((whiskerRight α' Gr).app j))
    (Gl.map (colimit.desc (F' ⋙ Gr) { pt := c.pt, ι := whiskerRight α' Gr ≫ c.ι })) (Gl.map (c.ι.app j))
⊢ IsPullback (c'.ι.app j) (β.inv.app j) (hl.coconePointUniqueUpToIso hr).hom
    (Gl.map ((colimit.cocone (F' ⋙ Gr)).ι.app j))

Tactic:
IsPullback.of_vert_isIso ⟨?_⟩

Premises used: CategoryTheory.IsPullback.of_vert_isIso, CategoryTheory.CommSq.mk
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
D : Type u_2
inst_2 : Category.{v_2, u_2} D
inst_3 : HasColimitsOfShape.{u', v', v, u} J C
Gl : Functor.{v, v_2, u, u_2} C D
Gr : Functor.{v_2, v, u_2, u} D C
adj : Gl ⊣ Gr
inst_4 : Gr.Full
inst_5 : Gr.Faithful
F : Functor.{u', v_2, v', u_2} J D
c : Cocone (F ⋙ Gr)
H : IsVanKampenColimit c
inst_6 : ∀ (X : D) (f : X ⟶ Gl.obj c.pt), HasPullback (Gr.map f) (adj.unit.app c.pt)
inst_7 : ∀ (X : D) (f : X ⟶ Gl.obj c.pt), PreservesLimit (cospan (Gr.map f) (adj.unit.app c.pt)) Gl
inst_8 : ∀ (X : C) (i : J) (f : X ⟶ c.pt), PreservesLimit (cospan f (c.ι.app i)) Gl
this_1 : PreservesLimitsOfSize.{v, v, v_2, v, u_2, u} Gr
this_2 : PreservesColimitsOfSize.{u', v', v, v_2, u, u_2} Gl
F' : Functor.{u', v_2, v', u_2} J D
c' : Cocone F'
α : F' ⟶ (F ⋙ Gr) ⋙ Gl
f : c'.pt ⟶ (Gl.mapCocone c).pt
h : α ≫ (Gl.mapCocone c).ι = c'.ι ≫ map (const J) f
hα : NatTrans.Equifibered α
hc' : IsColimit c'
j : J
α' : F' ⟶ F := α ≫ (F.associator Gr Gl).hom ≫ F.whiskerLeft adj.counit ≫ F.rightUnitor.hom
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 : (a : IsColimit c') → IsColimit ((Cocone.precompose β.hom).obj c')) hc'
hr : IsColimit (Gl.mapCocone (colimit.cocone (F' ⋙ Gr))) := isColimitOfPreserves Gl (colimit.isColimit (F' ⋙ Gr))
this_3 : α.app j = β.inv.app j ≫ Gl.map (Gr.map (α'.app j))
this_4 :
  f =
    (hl.coconePointUniqueUpToIso hr).hom ≫ Gl.map (colimit.desc (F' ⋙ Gr) { pt := c.pt, ι := whiskerRight α' Gr ≫ c.ι })
this :
  IsPullback (Gl.map ((colimit.cocone (F' ⋙ Gr)).ι.app j)) (Gl.map ((whiskerRight α' Gr).app j))
    (Gl.map (colimit.desc (F' ⋙ Gr) { pt := c.pt, ι := whiskerRight α' Gr ≫ c.ι })) (Gl.map (c.ι.app j))
refine_2 : c'.ι.app j ≫ (hl.coconePointUniqueUpToIso hr).hom = β.inv.app j ≫ Gl.map ((colimit.cocone (F' ⋙ Gr)).ι.app j)
⊢ IsPullback (c'.ι.app j) (β.inv.app j) (hl.coconePointUniqueUpToIso hr).hom
    (Gl.map ((colimit.cocone (F' ⋙ Gr)).ι.app j))

Tactic:
refine IsPullback.of_vert_isIso ⟨?_⟩

Premises used: CategoryTheory.IsPullback.of_vert_isIso, CategoryTheory.CommSq.mk
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
D : Type u_2
inst_2 : Category.{v_2, u_2} D
inst_3 : HasColimitsOfShape.{u', v', v, u} J C
Gl : Functor.{v, v_2, u, u_2} C D
Gr : Functor.{v_2, v, u_2, u} D C
adj : Gl ⊣ Gr
inst_4 : Gr.Full
inst_5 : Gr.Faithful
F : Functor.{u', v_2, v', u_2} J D
c : Cocone (F ⋙ Gr)
H : IsVanKampenColimit c
inst_6 : ∀ (X : D) (f : X ⟶ Gl.obj c.pt), HasPullback (Gr.map f) (adj.unit.app c.pt)
inst_7 : ∀ (X : D) (f : X ⟶ Gl.obj c.pt), PreservesLimit (cospan (Gr.map f) (adj.unit.app c.pt)) Gl
inst_8 : ∀ (X : C) (i : J) (f : X ⟶ c.pt), PreservesLimit (cospan f (c.ι.app i)) Gl
this_1 : PreservesLimitsOfSize.{v, v, v_2, v, u_2, u} Gr
this_2 : PreservesColimitsOfSize.{u', v', v, v_2, u, u_2} Gl
F' : Functor.{u', v_2, v', u_2} J D
c' : Cocone F'
α : F' ⟶ (F ⋙ Gr) ⋙ Gl
f : c'.pt ⟶ (Gl.mapCocone c).pt
h : α ≫ (Gl.mapCocone c).ι = c'.ι ≫ map (const J) f
hα : NatTrans.Equifibered α
hc' : IsColimit c'
j : J
α' : F' ⟶ F := α ≫ (F.associator Gr Gl).hom ≫ F.whiskerLeft adj.counit ≫ F.rightUnitor.hom
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 : (a : IsColimit c') → IsColimit ((Cocone.precompose β.hom).obj c')) hc'
hr : IsColimit (Gl.mapCocone (colimit.cocone (F' ⋙ Gr))) := isColimitOfPreserves Gl (colimit.isColimit (F' ⋙ Gr))
this_3 : α.app j = β.inv.app j ≫ Gl.map (Gr.map (α'.app j))
this_4 :
  f =
    (hl.coconePointUniqueUpToIso hr).hom ≫ Gl.map (colimit.desc (F' ⋙ Gr) { pt := c.pt, ι := whiskerRight α' Gr ≫ c.ι })
this :
  IsPullback (Gl.map ((colimit.cocone (F' ⋙ Gr)).ι.app j)) (Gl.map ((whiskerRight α' Gr).app j))
    (Gl.map (colimit.desc (F' ⋙ Gr) { pt := c.pt, ι := whiskerRight α' Gr ≫ c.ι })) (Gl.map (c.ι.app j))
refine_2 :
  (β.hom.app j ≫ c'.ι.app j) ≫ (hl.coconePointUniqueUpToIso hr).hom = Gl.map ((colimit.cocone (F' ⋙ Gr)).ι.app j)
⊢ c'.ι.app j ≫ (hl.coconePointUniqueUpToIso hr).hom = β.inv.app j ≫ Gl.map ((colimit.cocone (F' ⋙ Gr)).ι.app j)

Tactic:
rw [← IsIso.inv_comp_eq, ← Category.assoc, NatIso.inv_inv_app]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.IsIso.inv_comp_eq, CategoryTheory.NatIso.inv_inv_app
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
D : Type u_2
inst_2 : Category.{v_2, u_2} D
inst_3 : HasColimitsOfShape.{u', v', v, u} J C
Gl : Functor.{v, v_2, u, u_2} C D
Gr : Functor.{v_2, v, u_2, u} D C
adj : Gl ⊣ Gr
inst_4 : Gr.Full
inst_5 : Gr.Faithful
F : Functor.{u', v_2, v', u_2} J D
c : Cocone (F ⋙ Gr)
H : IsVanKampenColimit c
inst_6 : ∀ (X : D) (f : X ⟶ Gl.obj c.pt), HasPullback (Gr.map f) (adj.unit.app c.pt)
inst_7 : ∀ (X : D) (f : X ⟶ Gl.obj c.pt), PreservesLimit (cospan (Gr.map f) (adj.unit.app c.pt)) Gl
inst_8 : ∀ (X : C) (i : J) (f : X ⟶ c.pt), PreservesLimit (cospan f (c.ι.app i)) Gl
this_1 : PreservesLimitsOfSize.{v, v, v_2, v, u_2, u} Gr
this_2 : PreservesColimitsOfSize.{u', v', v, v_2, u, u_2} Gl
F' : Functor.{u', v_2, v', u_2} J D
c' : Cocone F'
α : F' ⟶ (F ⋙ Gr) ⋙ Gl
f : c'.pt ⟶ (Gl.mapCocone c).pt
h : α ≫ (Gl.mapCocone c).ι = c'.ι ≫ map (const J) f
hα : NatTrans.Equifibered α
hc' : IsColimit c'
j : J
α' : F' ⟶ F := α ≫ (F.associator Gr Gl).hom ≫ F.whiskerLeft adj.counit ≫ F.rightUnitor.hom
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 : (a : IsColimit c') → IsColimit ((Cocone.precompose β.hom).obj c')) hc'
hr : IsColimit (Gl.mapCocone (colimit.cocone (F' ⋙ Gr))) := isColimitOfPreserves Gl (colimit.isColimit (F' ⋙ Gr))
this_3 : α.app j = β.inv.app j ≫ Gl.map (Gr.map (α'.app j))
this_4 :
  f =
    (hl.coconePointUniqueUpToIso hr).hom ≫ Gl.map (colimit.desc (F' ⋙ Gr) { pt := c.pt, ι := whiskerRight α' Gr ≫ c.ι })
this :
  IsPullback (Gl.map ((colimit.cocone (F' ⋙ Gr)).ι.app j)) (Gl.map ((whiskerRight α' Gr).app j))
    (Gl.map (colimit.desc (F' ⋙ Gr) { pt := c.pt, ι := whiskerRight α' Gr ≫ c.ι })) (Gl.map (c.ι.app j))
⊢ (β.hom.app j ≫ c'.ι.app j) ≫ (hl.coconePointUniqueUpToIso hr).hom = Gl.map ((colimit.cocone (F' ⋙ Gr)).ι.app j)

Tactic:
IsColimit.comp_coconePointUniqueUpToIso_hom hl hr _

Premises used: CategoryTheory.Functor.comp, CategoryTheory.Limits.IsColimit.comp_coconePointUniqueUpToIso_hom
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
D : Type u_2
inst_2 : Category.{v_2, u_2} D
inst_3 : HasColimitsOfShape.{u', v', v, u} J C
Gl : Functor.{v, v_2, u, u_2} C D
Gr : Functor.{v_2, v, u_2, u} D C
adj : Gl ⊣ Gr
inst_4 : Gr.Full
inst_5 : Gr.Faithful
F : Functor.{u', v_2, v', u_2} J D
c : Cocone (F ⋙ Gr)
H : IsVanKampenColimit c
inst_6 : ∀ (X : D) (f : X ⟶ Gl.obj c.pt), HasPullback (Gr.map f) (adj.unit.app c.pt)
inst_7 : ∀ (X : D) (f : X ⟶ Gl.obj c.pt), PreservesLimit (cospan (Gr.map f) (adj.unit.app c.pt)) Gl
inst_8 : ∀ (X : C) (i : J) (f : X ⟶ c.pt), PreservesLimit (cospan f (c.ι.app i)) Gl
this_1 : PreservesLimitsOfSize.{v, v, v_2, v, u_2, u} Gr
this_2 : PreservesColimitsOfSize.{u', v', v, v_2, u, u_2} Gl
F' : Functor.{u', v_2, v', u_2} J D
c' : Cocone F'
α : F' ⟶ (F ⋙ Gr) ⋙ Gl
f : c'.pt ⟶ (Gl.mapCocone c).pt
h : α ≫ (Gl.mapCocone c).ι = c'.ι ≫ map (const J) f
hα : NatTrans.Equifibered α
hc' : IsColimit c'
j : J
α' : F' ⟶ F := α ≫ (F.associator Gr Gl).hom ≫ F.whiskerLeft adj.counit ≫ F.rightUnitor.hom
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 : (a : IsColimit c') → IsColimit ((Cocone.precompose β.hom).obj c')) hc'
hr : IsColimit (Gl.mapCocone (colimit.cocone (F' ⋙ Gr))) := isColimitOfPreserves Gl (colimit.isColimit (F' ⋙ Gr))
this_3 : α.app j = β.inv.app j ≫ Gl.map (Gr.map (α'.app j))
this_4 :
  f =
    (hl.coconePointUniqueUpToIso hr).hom ≫ Gl.map (colimit.desc (F' ⋙ Gr) { pt := c.pt, ι := whiskerRight α' Gr ≫ c.ι })
this :
  IsPullback (Gl.map ((colimit.cocone (F' ⋙ Gr)).ι.app j)) (Gl.map ((whiskerRight α' Gr).app j))
    (Gl.map (colimit.desc (F' ⋙ Gr) { pt := c.pt, ι := whiskerRight α' Gr ≫ c.ι })) (Gl.map (c.ι.app j))
⊢ (β.hom.app j ≫ c'.ι.app j) ≫ (hl.coconePointUniqueUpToIso hr).hom = Gl.map ((colimit.cocone (F' ⋙ Gr)).ι.app j)

Tactic:
exact IsColimit.comp_coconePointUniqueUpToIso_hom hl hr _

Premises used: CategoryTheory.Limits.IsColimit.comp_coconePointUniqueUpToIso_hom
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
D : Type u_2
inst_2 : Category.{v_2, u_2} D
inst_3 : HasColimitsOfShape.{u', v', v, u} J C
Gl : Functor.{v, v_2, u, u_2} C D
Gr : Functor.{v_2, v, u_2, u} D C
adj : Gl ⊣ Gr
inst_4 : Gr.Full
inst_5 : Gr.Faithful
F : Functor.{u', v_2, v', u_2} J D
c : Cocone (F ⋙ Gr)
H : IsVanKampenColimit c
inst_6 : ∀ (X : D) (f : X ⟶ Gl.obj c.pt), HasPullback (Gr.map f) (adj.unit.app c.pt)
inst_7 : ∀ (X : D) (f : X ⟶ Gl.obj c.pt), PreservesLimit (cospan (Gr.map f) (adj.unit.app c.pt)) Gl
inst_8 : ∀ (X : C) (i : J) (f : X ⟶ c.pt), PreservesLimit (cospan f (c.ι.app i)) Gl
this_1 : PreservesLimitsOfSize.{v, v, v_2, v, u_2, u} Gr
this_2 : PreservesColimitsOfSize.{u', v', v, v_2, u, u_2} Gl
F' : Functor.{u', v_2, v', u_2} J D
c' : Cocone F'
α : F' ⟶ (F ⋙ Gr) ⋙ Gl
f : c'.pt ⟶ (Gl.mapCocone c).pt
h : α ≫ (Gl.mapCocone c).ι = c'.ι ≫ map (const J) f
hα : NatTrans.Equifibered α
hc' : IsColimit c'
j : J
α' : F' ⟶ F := α ≫ (F.associator Gr Gl).hom ≫ F.whiskerLeft adj.counit ≫ F.rightUnitor.hom
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 : (a : IsColimit c') → IsColimit ((Cocone.precompose β.hom).obj c')) hc'
hr : IsColimit (Gl.mapCocone (colimit.cocone (F' ⋙ Gr))) := isColimitOfPreserves Gl (colimit.isColimit (F' ⋙ Gr))
this_3 : α.app j = β.inv.app j ≫ Gl.map (Gr.map (α'.app j))
this :
  f =
    (hl.coconePointUniqueUpToIso hr).hom ≫ Gl.map (colimit.desc (F' ⋙ Gr) { pt := c.pt, ι := whiskerRight α' Gr ≫ c.ι })
refine_1 :
  ∀ (α' : F' ⟶ F) (hα' : NatTrans.Equifibered α')
    (hα'' : ∀ (j : J), Gl.map (Gr.map (α'.app j)) = adj.counit.app (F'.1 j) ≫ α.app j),
    let β := F'.isoWhiskerLeft (asIso adj.counit) ≪≫ F'.rightUnitor;
    let hl : IsColimit ((Cocone.precompose β.hom).obj c') :=
      ((IsColimit.precomposeHomEquiv β c').symm : (a : IsColimit c') → IsColimit ((Cocone.precompose β.hom).obj c'))
        hc';
    let 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)))
      (this :
        f =
          (hl.coconePointUniqueUpToIso hr).hom ≫
            Gl.map (colimit.desc (F' ⋙ Gr) { pt := c.pt, ι := whiskerRight α' Gr ≫ c.ι })),
      whiskerRight α' Gr ≫ c.ι =
        (colimit.cocone (F' ⋙ Gr)).ι ≫
          map (const J) (colimit.desc (F' ⋙ Gr) { pt := c.pt, ι := whiskerRight α' Gr ≫ c.ι })
⊢ whiskerRight α' Gr ≫ c.ι =
    (colimit.cocone (F' ⋙ Gr)).ι ≫ map (const J) (colimit.desc (F' ⋙ Gr) { pt := c.pt, ι := whiskerRight α' Gr ≫ c.ι })

Tactic:
clear_value α'
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
D : Type u_2
inst_2 : Category.{v_2, u_2} D
inst_3 : HasColimitsOfShape.{u', v', v, u} J C
Gl : Functor.{v, v_2, u, u_2} C D
Gr : Functor.{v_2, v, u_2, u} D C
adj : Gl ⊣ Gr
inst_4 : Gr.Full
inst_5 : Gr.Faithful
F : Functor.{u', v_2, v', u_2} J D
c : Cocone (F ⋙ Gr)
H : IsVanKampenColimit c
inst_6 : ∀ (X : D) (f : X ⟶ Gl.obj c.pt), HasPullback (Gr.map f) (adj.unit.app c.pt)
inst_7 : ∀ (X : D) (f : X ⟶ Gl.obj c.pt), PreservesLimit (cospan (Gr.map f) (adj.unit.app c.pt)) Gl
inst_8 : ∀ (X : C) (i : J) (f : X ⟶ c.pt), PreservesLimit (cospan f (c.ι.app i)) Gl
this_1 : PreservesLimitsOfSize.{v, v, v_2, v, u_2, u} Gr
this_2 : PreservesColimitsOfSize.{u', v', v, v_2, u, u_2} Gl
F' : Functor.{u', v_2, v', u_2} J D
c' : Cocone F'
α : F' ⟶ (F ⋙ Gr) ⋙ Gl
f : c'.pt ⟶ (Gl.mapCocone c).pt
h : α ≫ (Gl.mapCocone c).ι = c'.ι ≫ map (const J) 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 : (a : IsColimit c') → IsColimit ((Cocone.precompose β.hom).obj c')) hc'
hr : IsColimit (Gl.mapCocone (colimit.cocone (F' ⋙ Gr))) := isColimitOfPreserves Gl (colimit.isColimit (F' ⋙ Gr))
this_3 : α.app j = β.inv.app j ≫ Gl.map (Gr.map (α'.app j))
this :
  f =
    (hl.coconePointUniqueUpToIso hr).hom ≫ Gl.map (colimit.desc (F' ⋙ Gr) { pt := c.pt, ι := whiskerRight α' Gr ≫ c.ι })
refine_1 :
  ∀ (j : J),
    (whiskerRight α' Gr ≫ c.ι).app j =
      NatTrans.app
        ((colimit.cocone (F' ⋙ Gr)).ι ≫
          map (const J) (colimit.desc (F' ⋙ Gr) { pt := c.pt, ι := whiskerRight α' Gr ≫ c.ι }))
        j
⊢ whiskerRight α' Gr ≫ c.ι =
    (colimit.cocone (F' ⋙ Gr)).ι ≫ map (const J) (colimit.desc (F' ⋙ Gr) { pt := c.pt, ι := whiskerRight α' Gr ≫ c.ι })

Tactic:
ext j
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
D : Type u_2
inst_2 : Category.{v_2, u_2} D
inst_3 : HasColimitsOfShape.{u', v', v, u} J C
Gl : Functor.{v, v_2, u, u_2} C D
Gr : Functor.{v_2, v, u_2, u} D C
adj : Gl ⊣ Gr
inst_4 : Gr.Full
inst_5 : Gr.Faithful
F : Functor.{u', v_2, v', u_2} J D
c : Cocone (F ⋙ Gr)
H : IsVanKampenColimit c
inst_6 : ∀ (X : D) (f : X ⟶ Gl.obj c.pt), HasPullback (Gr.map f) (adj.unit.app c.pt)
inst_7 : ∀ (X : D) (f : X ⟶ Gl.obj c.pt), PreservesLimit (cospan (Gr.map f) (adj.unit.app c.pt)) Gl
inst_8 : ∀ (X : C) (i : J) (f : X ⟶ c.pt), PreservesLimit (cospan f (c.ι.app i)) Gl
this_1 : PreservesLimitsOfSize.{v, v, v_2, v, u_2, u} Gr
this_2 : PreservesColimitsOfSize.{u', v', v, v_2, u, u_2} Gl
F' : Functor.{u', v_2, v', u_2} J D
c' : Cocone F'
α : F' ⟶ (F ⋙ Gr) ⋙ Gl
f : c'.pt ⟶ (Gl.mapCocone c).pt
h : α ≫ (Gl.mapCocone c).ι = c'.ι ≫ map (const J) f
hα : NatTrans.Equifibered α
hc' : IsColimit c'
j_1 : 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 : (a : IsColimit c') → IsColimit ((Cocone.precompose β.hom).obj c')) hc'
hr : IsColimit (Gl.mapCocone (colimit.cocone (F' ⋙ Gr))) := isColimitOfPreserves Gl (colimit.isColimit (F' ⋙ Gr))
this_3 : α.app j_1 = β.inv.app j_1 ≫ Gl.map (Gr.map (α'.app j_1))
this :
  f =
    (hl.coconePointUniqueUpToIso hr).hom ≫ Gl.map (colimit.desc (F' ⋙ Gr) { pt := c.pt, ι := whiskerRight α' Gr ≫ c.ι })
j : J
⊢ (whiskerRight α' Gr ≫ c.ι).app j =
    NatTrans.app
      ((colimit.cocone (F' ⋙ Gr)).ι ≫
        map (const J) (colimit.desc (F' ⋙ Gr) { pt := c.pt, ι := whiskerRight α' Gr ≫ c.ι }))
      j

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasInitial.{v, u} C
H : IsUniversalColimit.{0, 0, v, u} (BinaryCofan.mk (𝟙 (initial.{v, u} C)) (𝟙 (initial.{v, u} C)))
A : C
f : A ⟶ initial.{v, u} C
this : IsColimit.{0, v, 0, u} (BinaryCofan.mk (𝟙 A) (𝟙 A))
obtain :
  ∀ (l : Cocone.pt.{0, v, 0, u} (BinaryCofan.mk (𝟙 A) (𝟙 A)) ⟶ A)
    (h₁ : BinaryCofan.inl (BinaryCofan.mk (𝟙 A) (𝟙 A)) ≫ l = f ≫ initial.to A)
    (h₂ :
      Eq.{v + 1} (α := obj.{0, v, 0, u} (pair A A) { as := WalkingPair.right : Discrete WalkingPair } ⟶ A)
        (BinaryCofan.inr (BinaryCofan.mk (𝟙 A) (𝟙 A)) ≫ l) (𝟙 A)),
    IsIso f
⊢ IsIso f

Tactic:
obtain ⟨l, h₁, h₂⟩ := Limits.BinaryCofan.IsColimit.desc' this (f ≫ initial.to A) (𝟙 A)

Premises used: CategoryTheory.CategoryStruct.id, CategoryTheory.Limits.initial.to, CategoryTheory.CategoryStruct.comp, CategoryTheory.Limits.BinaryCofan.IsColimit.desc'
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasInitial.{v, u} C
H : IsUniversalColimit.{0, 0, v, u} (BinaryCofan.mk (𝟙 (initial.{v, u} C)) (𝟙 (initial.{v, u} C)))
A : C
f : A ⟶ initial.{v, u} C
this : IsColimit.{0, v, 0, u} (BinaryCofan.mk (𝟙 A) (𝟙 A))
l : Cocone.pt.{0, v, 0, u} (BinaryCofan.mk (𝟙 A) (𝟙 A)) ⟶ A
h₁ : BinaryCofan.inl (BinaryCofan.mk (𝟙 A) (𝟙 A)) ≫ l = f ≫ initial.to A
h₂ :
  Eq.{v + 1} (α := obj.{0, v, 0, u} (pair A A) { as := WalkingPair.right : Discrete WalkingPair } ⟶ A)
    (BinaryCofan.inr (BinaryCofan.mk (𝟙 A) (𝟙 A)) ≫ l) (𝟙 A)
⊢ CategoryStruct.comp (Y :=
      obj.{0, v, 0, u} (obj (const (Discrete WalkingPair)) (Cocone.pt.{0, v, 0, u} (BinaryCofan.mk (𝟙 A) (𝟙 A))))
        { as := WalkingPair.left : Discrete WalkingPair })
      (BinaryCofan.inl (BinaryCofan.mk (𝟙 A) (𝟙 A))) (𝟙 A) =
    f ≫ initial.to A

Tactic:
rcases (Category.id_comp _).symm.trans h₂ with rfl

Premises used: Eq.symm, rfl, Eq.trans, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasInitial.{v, u} C
H : IsUniversalColimit.{0, 0, v, u} (BinaryCofan.mk (𝟙 (initial.{v, u} C)) (𝟙 (initial.{v, u} C)))
A : C
f : A ⟶ initial.{v, u} C
this : IsColimit.{0, v, 0, u} (BinaryCofan.mk (𝟙 A) (𝟙 A))
l : Cocone.pt.{0, v, 0, u} (BinaryCofan.mk (𝟙 A) (𝟙 A)) ⟶ A
h₁ : BinaryCofan.inl (BinaryCofan.mk (𝟙 A) (𝟙 A)) ≫ l = f ≫ initial.to A
h₂ :
  Eq.{v + 1} (α := obj.{0, v, 0, u} (pair A A) { as := WalkingPair.right : Discrete WalkingPair } ⟶ A)
    (BinaryCofan.inr (BinaryCofan.mk (𝟙 A) (𝟙 A)) ≫ l) (𝟙 A)
h₃ :
  CategoryStruct.comp (Y :=
      obj.{0, v, 0, u} (obj (const (Discrete WalkingPair)) (Cocone.pt.{0, v, 0, u} (BinaryCofan.mk (𝟙 A) (𝟙 A))))
        { as := WalkingPair.left : Discrete WalkingPair })
      (BinaryCofan.inl (BinaryCofan.mk (𝟙 A) (𝟙 A))) (𝟙 A) =
    f ≫ initial.to A
⊢ Eq.{v + 1} (α := obj.{0, v, 0, u} (pair A A) { as := WalkingPair.right : Discrete WalkingPair } ⟶ A)
    (CategoryStruct.comp (Y :=
      obj.{0, v, 0, u} (obj (const (Discrete WalkingPair)) (Cocone.pt.{0, v, 0, u} (BinaryCofan.mk (𝟙 A) (𝟙 A))))
        { as := WalkingPair.right : Discrete WalkingPair })
      (BinaryCofan.inr (BinaryCofan.mk (𝟙 A) (𝟙 A))) (𝟙 A))
    (𝟙 A)

Tactic:
rcases (Category.id_comp _).symm.trans h₂ with rfl

Premises used: Eq.symm, rfl, Eq.trans, CategoryTheory.Category.id_comp