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 : HasPullbacks.{v_2, u_2} D
inst_4 : HasColimitsOfShape.{u', v', v_2, u_2} J D
F : J ⥤ Functor.{v, v_2, u, u_2} C D
c : Cocone F
hc : ∀ (x : C), IsVanKampenColimit (F := F ⋙ obj (evaluation C D) x) (mapCocone (obj (evaluation C D) x) c)
F' : J ⥤ Functor.{v, v_2, u, u_2} C D
c' : Cocone F'
α : F' ⟶ F
f : c'.pt ⟶ c.pt
e : α ≫ c.ι = c'.ι ≫ map (const J) f
hα : NatTrans.Equifibered α
⊢ ∀ (x : C),
    Nonempty (IsColimit (F := F' ⋙ obj (evaluation C D) x) (mapCocone (obj (evaluation C D) x) c')) ↔
      ∀ (j : J),
        IsPullback (X :=
          obj.{u', v_2, v', u_2}
            (obj (const J) (Cocone.pt (F := F' ⋙ obj (evaluation C D) x) (mapCocone (obj (evaluation C D) x) c'))) j)
          (Z := Cocone.pt (F := F ⋙ obj (evaluation C D) x) (mapCocone (obj (evaluation C D) x) c))
          (NatTrans.app (Cocone.ι (mapCocone (obj (evaluation C D) x) c')) j)
          ((whiskerRight α (obj (evaluation C D) x)).app j)
          (map (obj (evaluation C D) x) f : obj (obj (evaluation C D) x) c'.pt ⟶ obj (obj (evaluation C D) x) c.pt)
          (NatTrans.app (Cocone.ι (mapCocone (obj (evaluation C D) x) c)) j :
            (F ⋙ obj (evaluation C D) x).obj j ⟶
              obj.{u', v_2, v', u_2}
                (obj (const J) (Cocone.pt (F := F ⋙ obj (evaluation C D) x) (mapCocone (obj (evaluation C D) x) c))) j)

Tactic:
have := fun x => hc x (((evaluation C D).obj x).mapCocone c') (whiskerRight α _)
      (((evaluation C D).obj x).map f)
      (by
        ext y
        dsimp
        exact NatTrans.congr_app (NatTrans.congr_app e y) x)
      (hα.whiskerRight _)
-- 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 : HasPullbacks.{v_2, u_2} D
inst_4 : HasColimitsOfShape.{u', v', v_2, u_2} J D
F : J ⥤ Functor.{v, v_2, u, u_2} C D
c : Cocone F
hc : ∀ (x : C), IsVanKampenColimit (F := F ⋙ obj (evaluation C D) x) (mapCocone (obj (evaluation C D) x) c)
F' : J ⥤ Functor.{v, v_2, u, u_2} C D
c' : Cocone F'
α : F' ⟶ F
f : c'.pt ⟶ c.pt
e : α ≫ c.ι = c'.ι ≫ map (const J) f
hα : NatTrans.Equifibered α
this :
  ∀ (x : C),
    Nonempty (IsColimit (F := F' ⋙ obj (evaluation C D) x) (mapCocone (obj (evaluation C D) x) c')) ↔
      ∀ (j : J),
        IsPullback (X :=
          obj.{u', v_2, v', u_2}
            (obj (const J) (Cocone.pt (F := F' ⋙ obj (evaluation C D) x) (mapCocone (obj (evaluation C D) x) c'))) j)
          (Z := Cocone.pt (F := F ⋙ obj (evaluation C D) x) (mapCocone (obj (evaluation C D) x) c))
          (NatTrans.app (Cocone.ι (mapCocone (obj (evaluation C D) x) c')) j)
          ((whiskerRight α (obj (evaluation C D) x)).app j)
          (map (obj (evaluation C D) x) f : obj (obj (evaluation C D) x) c'.pt ⟶ obj (obj (evaluation C D) x) c.pt)
          (NatTrans.app (Cocone.ι (mapCocone (obj (evaluation C D) x) c)) j :
            (F ⋙ obj (evaluation C D) x).obj j ⟶
              obj.{u', v_2, v', u_2}
                (obj (const J) (Cocone.pt (F := F ⋙ obj (evaluation C D) x) (mapCocone (obj (evaluation C D) x) c))) j)
mp : Nonempty (IsColimit c') → ∀ (j : J), IsPullback (c'.ι.app j) (α.app j) f (c.ι.app j)
mpr : (∀ (j : J), IsPullback (c'.ι.app j) (α.app j) f (c.ι.app j)) → Nonempty (IsColimit c')
⊢ Nonempty (IsColimit c') ↔ ∀ (j : J), IsPullback (c'.ι.app j) (α.app j) f (c.ι.app j)

Tactic:
constructor
-- 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 : HasPullbacks.{v_2, u_2} D
inst_4 : HasColimitsOfShape.{u', v', v_2, u_2} J D
F : J ⥤ Functor.{v, v_2, u, u_2} C D
c : Cocone F
hc : ∀ (x : C), IsVanKampenColimit (F := F ⋙ obj (evaluation C D) x) (mapCocone (obj (evaluation C D) x) c)
F' : J ⥤ Functor.{v, v_2, u, u_2} C D
c' : Cocone F'
α : F' ⟶ F
f : c'.pt ⟶ c.pt
e : α ≫ c.ι = c'.ι ≫ map (const J) f
hα : NatTrans.Equifibered α
this :
  ∀ (x : C),
    Nonempty (IsColimit (F := F' ⋙ obj (evaluation C D) x) (mapCocone (obj (evaluation C D) x) c')) ↔
      ∀ (j : J),
        IsPullback (X :=
          obj.{u', v_2, v', u_2}
            (obj (const J) (Cocone.pt (F := F' ⋙ obj (evaluation C D) x) (mapCocone (obj (evaluation C D) x) c'))) j)
          (Z := Cocone.pt (F := F ⋙ obj (evaluation C D) x) (mapCocone (obj (evaluation C D) x) c))
          (NatTrans.app (Cocone.ι (mapCocone (obj (evaluation C D) x) c')) j)
          ((whiskerRight α (obj (evaluation C D) x)).app j)
          (map (obj (evaluation C D) x) f : obj (obj (evaluation C D) x) c'.pt ⟶ obj (obj (evaluation C D) x) c.pt)
          (NatTrans.app (Cocone.ι (mapCocone (obj (evaluation C D) x) c)) j :
            (F ⋙ obj (evaluation C D) x).obj j ⟶
              obj.{u', v_2, v', u_2}
                (obj (const J) (Cocone.pt (F := F ⋙ obj (evaluation C D) x) (mapCocone (obj (evaluation C D) x) c))) j)
hc' : IsColimit c'
j : J
⊢ IsPullback (c'.ι.app j) (α.app j) f (c.ι.app j)

Tactic:
⟨⟨(NatTrans.congr_app e j).symm⟩, ⟨evaluationJointlyReflectsLimits _ ?_⟩⟩

Premises used: CategoryTheory.Limits.evaluationJointlyReflectsLimits, CategoryTheory.IsPullback.mk, CategoryTheory.CommSq.mk, Nonempty.intro, CategoryTheory.NatTrans.congr_app, Eq.symm
-- 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 : HasPullbacks.{v_2, u_2} D
inst_4 : HasColimitsOfShape.{u', v', v_2, u_2} J D
F : J ⥤ Functor.{v, v_2, u, u_2} C D
c : Cocone F
hc : ∀ (x : C), IsVanKampenColimit (F := F ⋙ obj (evaluation C D) x) (mapCocone (obj (evaluation C D) x) c)
F' : J ⥤ Functor.{v, v_2, u, u_2} C D
c' : Cocone F'
α : F' ⟶ F
f : c'.pt ⟶ c.pt
e : α ≫ c.ι = c'.ι ≫ map (const J) f
hα : NatTrans.Equifibered α
this :
  ∀ (x : C),
    Nonempty (IsColimit (F := F' ⋙ obj (evaluation C D) x) (mapCocone (obj (evaluation C D) x) c')) ↔
      ∀ (j : J),
        IsPullback (X :=
          obj.{u', v_2, v', u_2}
            (obj (const J) (Cocone.pt (F := F' ⋙ obj (evaluation C D) x) (mapCocone (obj (evaluation C D) x) c'))) j)
          (Z := Cocone.pt (F := F ⋙ obj (evaluation C D) x) (mapCocone (obj (evaluation C D) x) c))
          (NatTrans.app (Cocone.ι (mapCocone (obj (evaluation C D) x) c')) j)
          ((whiskerRight α (obj (evaluation C D) x)).app j)
          (map (obj (evaluation C D) x) f : obj (obj (evaluation C D) x) c'.pt ⟶ obj (obj (evaluation C D) x) c.pt)
          (NatTrans.app (Cocone.ι (mapCocone (obj (evaluation C D) x) c)) j :
            (F ⋙ obj (evaluation C D) x).obj j ⟶
              obj.{u', v_2, v', u_2}
                (obj (const J) (Cocone.pt (F := F ⋙ obj (evaluation C D) x) (mapCocone (obj (evaluation C D) x) c))) j)
hc' : IsColimit c'
j : J
mp :
  (k : C) →
    IsLimit (F := cospan f (c.ι.app j) ⋙ obj (evaluation C D) k)
      (mapCone (obj (evaluation C D) k) (PullbackCone.mk (c'.ι.app j) (α.app j) ⋯))
⊢ IsPullback (c'.ι.app j) (α.app j) f (c.ι.app j)

Tactic:
refine ⟨⟨(NatTrans.congr_app e j).symm⟩, ⟨evaluationJointlyReflectsLimits _ ?_⟩⟩
-- 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 : HasPullbacks.{v_2, u_2} D
inst_4 : HasColimitsOfShape.{u', v', v_2, u_2} J D
F : J ⥤ Functor.{v, v_2, u, u_2} C D
c : Cocone F
hc : ∀ (x : C), IsVanKampenColimit (F := F ⋙ obj (evaluation C D) x) (mapCocone (obj (evaluation C D) x) c)
F' : J ⥤ Functor.{v, v_2, u, u_2} C D
c' : Cocone F'
α : F' ⟶ F
f : c'.pt ⟶ c.pt
e : α ≫ c.ι = c'.ι ≫ map (const J) f
hα : NatTrans.Equifibered α
this :
  ∀ (x : C),
    Nonempty (IsColimit (F := F' ⋙ obj (evaluation C D) x) (mapCocone (obj (evaluation C D) x) c')) ↔
      ∀ (j : J),
        IsPullback (X :=
          obj.{u', v_2, v', u_2}
            (obj (const J) (Cocone.pt (F := F' ⋙ obj (evaluation C D) x) (mapCocone (obj (evaluation C D) x) c'))) j)
          (Z := Cocone.pt (F := F ⋙ obj (evaluation C D) x) (mapCocone (obj (evaluation C D) x) c))
          (NatTrans.app (Cocone.ι (mapCocone (obj (evaluation C D) x) c')) j)
          ((whiskerRight α (obj (evaluation C D) x)).app j)
          (map (obj (evaluation C D) x) f : obj (obj (evaluation C D) x) c'.pt ⟶ obj (obj (evaluation C D) x) c.pt)
          (NatTrans.app (Cocone.ι (mapCocone (obj (evaluation C D) x) c)) j :
            (F ⋙ obj (evaluation C D) x).obj j ⟶
              obj.{u', v_2, v', u_2}
                (obj (const J) (Cocone.pt (F := F ⋙ obj (evaluation C D) x) (mapCocone (obj (evaluation C D) x) c))) j)
hc' : IsColimit c'
j : J
mp :
  (x : C) →
    IsLimit (F :=
      cospan (X := obj (obj (evaluation C D) x) (obj (obj (const J) c'.pt) j)) (map (obj (evaluation C D) x) f)
        (map (obj (evaluation C D) x) (c.ι.app j)))
      (PullbackCone.mk (map (obj (evaluation C D) x) (c'.ι.app j)) (map (obj (evaluation C D) x) (α.app j)) ⋯)
⊢ (k : C) →
    IsLimit (F := cospan f (c.ι.app j) ⋙ obj (evaluation C D) k)
      (mapCone (obj (evaluation C D) k) (PullbackCone.mk (c'.ι.app j) (α.app j) ⋯))

Tactic:
refine fun x => (isLimitMapConePullbackConeEquiv _ _).symm ?_

Premises used: CategoryTheory.Limits.isLimitMapConePullbackConeEquiv, Equiv.symm, DFunLike.coe
-- 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 : HasPullbacks.{v_2, u_2} D
inst_4 : HasColimitsOfShape.{u', v', v_2, u_2} J D
F : J ⥤ Functor.{v, v_2, u, u_2} C D
c : Cocone F
hc : ∀ (x : C), IsVanKampenColimit (F := F ⋙ obj (evaluation C D) x) (mapCocone (obj (evaluation C D) x) c)
F' : J ⥤ Functor.{v, v_2, u, u_2} C D
c' : Cocone F'
α : F' ⟶ F
f : c'.pt ⟶ c.pt
e : α ≫ c.ι = c'.ι ≫ map (const J) f
hα : NatTrans.Equifibered α
this :
  ∀ (x : C),
    Nonempty (IsColimit (F := F' ⋙ obj (evaluation C D) x) (mapCocone (obj (evaluation C D) x) c')) ↔
      ∀ (j : J),
        IsPullback (X :=
          obj.{u', v_2, v', u_2}
            (obj (const J) (Cocone.pt (F := F' ⋙ obj (evaluation C D) x) (mapCocone (obj (evaluation C D) x) c'))) j)
          (Z := Cocone.pt (F := F ⋙ obj (evaluation C D) x) (mapCocone (obj (evaluation C D) x) c))
          (NatTrans.app (Cocone.ι (mapCocone (obj (evaluation C D) x) c')) j)
          ((whiskerRight α (obj (evaluation C D) x)).app j)
          (map (obj (evaluation C D) x) f : obj (obj (evaluation C D) x) c'.pt ⟶ obj (obj (evaluation C D) x) c.pt)
          (NatTrans.app (Cocone.ι (mapCocone (obj (evaluation C D) x) c)) j :
            (F ⋙ obj (evaluation C D) x).obj j ⟶
              obj.{u', v_2, v', u_2}
                (obj (const J) (Cocone.pt (F := F ⋙ obj (evaluation C D) x) (mapCocone (obj (evaluation C D) x) c))) j)
hc' : IsColimit c'
j : J
x : C
⊢ IsLimit (F :=
    cospan (X := obj (obj (evaluation C D) x) (obj (obj (const J) c'.pt) j)) (map (obj (evaluation C D) x) f)
      (map (obj (evaluation C D) x) (c.ι.app j)))
    (PullbackCone.mk (map (obj (evaluation C D) x) (c'.ι.app j)) (map (obj (evaluation C D) x) (α.app j)) ⋯)

Tactic:
exact ((this x).mp ⟨isColimitOfPreserves _ hc'⟩ _).isLimit

Premises used: Nonempty.intro, Iff.mp, CategoryTheory.Limits.isColimitOfPreserves, CategoryTheory.IsPullback.isLimit
-- 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 : HasPullbacks.{v_2, u_2} D
inst_4 : HasColimitsOfShape.{u', v', v_2, u_2} J D
F : J ⥤ Functor.{v, v_2, u, u_2} C D
c : Cocone F
hc : ∀ (x : C), IsVanKampenColimit (F := F ⋙ obj (evaluation C D) x) (mapCocone (obj (evaluation C D) x) c)
F' : J ⥤ Functor.{v, v_2, u, u_2} C D
c' : Cocone F'
α : F' ⟶ F
f : c'.pt ⟶ c.pt
e : α ≫ c.ι = c'.ι ≫ map (const J) f
hα : NatTrans.Equifibered α
this :
  ∀ (x : C),
    Nonempty (IsColimit (F := F' ⋙ obj (evaluation C D) x) (mapCocone (obj (evaluation C D) x) c')) ↔
      ∀ (j : J),
        IsPullback (X :=
          obj.{u', v_2, v', u_2}
            (obj (const J) (Cocone.pt (F := F' ⋙ obj (evaluation C D) x) (mapCocone (obj (evaluation C D) x) c'))) j)
          (Z := Cocone.pt (F := F ⋙ obj (evaluation C D) x) (mapCocone (obj (evaluation C D) x) c))
          (NatTrans.app (Cocone.ι (mapCocone (obj (evaluation C D) x) c')) j)
          ((whiskerRight α (obj (evaluation C D) x)).app j)
          (map (obj (evaluation C D) x) f : obj (obj (evaluation C D) x) c'.pt ⟶ obj (obj (evaluation C D) x) c.pt)
          (NatTrans.app (Cocone.ι (mapCocone (obj (evaluation C D) x) c)) j :
            (F ⋙ obj (evaluation C D) x).obj j ⟶
              obj.{u', v_2, v', u_2}
                (obj (const J) (Cocone.pt (F := F ⋙ obj (evaluation C D) x) (mapCocone (obj (evaluation C D) x) c))) j)
⊢ (∀ (j : J), IsPullback (c'.ι.app j) (α.app j) f (c.ι.app j)) → Nonempty (IsColimit c')

Tactic:
fun H => ⟨evaluationJointlyReflectsColimits _ fun x =>
      ((this x).mpr fun j => (H j).map ((evaluation C D).obj x)).some⟩

Premises used: Iff.mpr, CategoryTheory.Limits.evaluationJointlyReflectsColimits, Nonempty.some, Nonempty.intro, CategoryTheory.evaluation, CategoryTheory.IsPullback.map, CategoryTheory.Functor.obj
-- 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 : HasPullbacks.{v_2, u_2} D
inst_4 : HasColimitsOfShape.{u', v', v_2, u_2} J D
F : J ⥤ Functor.{v, v_2, u, u_2} C D
c : Cocone F
hc : ∀ (x : C), IsVanKampenColimit (F := F ⋙ obj (evaluation C D) x) (mapCocone (obj (evaluation C D) x) c)
F' : J ⥤ Functor.{v, v_2, u, u_2} C D
c' : Cocone F'
α : F' ⟶ F
f : c'.pt ⟶ c.pt
e : α ≫ c.ι = c'.ι ≫ map (const J) f
hα : NatTrans.Equifibered α
this :
  ∀ (x : C),
    Nonempty (IsColimit (F := F' ⋙ obj (evaluation C D) x) (mapCocone (obj (evaluation C D) x) c')) ↔
      ∀ (j : J),
        IsPullback (X :=
          obj.{u', v_2, v', u_2}
            (obj (const J) (Cocone.pt (F := F' ⋙ obj (evaluation C D) x) (mapCocone (obj (evaluation C D) x) c'))) j)
          (Z := Cocone.pt (F := F ⋙ obj (evaluation C D) x) (mapCocone (obj (evaluation C D) x) c))
          (NatTrans.app (Cocone.ι (mapCocone (obj (evaluation C D) x) c')) j)
          ((whiskerRight α (obj (evaluation C D) x)).app j)
          (map (obj (evaluation C D) x) f : obj (obj (evaluation C D) x) c'.pt ⟶ obj (obj (evaluation C D) x) c.pt)
          (NatTrans.app (Cocone.ι (mapCocone (obj (evaluation C D) x) c)) j :
            (F ⋙ obj (evaluation C D) x).obj j ⟶
              obj.{u', v_2, v', u_2}
                (obj (const J) (Cocone.pt (F := F ⋙ obj (evaluation C D) x) (mapCocone (obj (evaluation C D) x) c))) j)
⊢ (∀ (j : J), IsPullback (c'.ι.app j) (α.app j) f (c.ι.app j)) → Nonempty (IsColimit c')

Tactic:
exact fun H => ⟨evaluationJointlyReflectsColimits _ fun x =>
      ((this x).mpr fun j => (H j).map ((evaluation C D).obj x)).some⟩
-- 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
⊢ PreservesLimitsOfSize.{v, v, v_2, v, u_2, u} Gr

Tactic:
have := adj.rightAdjoint_preservesLimits
-- 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 : PreservesLimitsOfSize.{v, v, v_2, v, u_2, u} Gr
⊢ PreservesColimitsOfSize.{u', v', v, v_2, u, u_2} Gl

Tactic:
have : PreservesColimitsOfSize.{u', v'} Gl := adj.leftAdjoint_preservesColimits
-- 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 : 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 α
⊢ Nonempty (IsColimit c') ↔ ∀ (j : J), IsPullback (c'.ι.app j) (α.app j) f ((Gl.mapCocone c).ι.app j)

Tactic:
⟨?_, H.isUniversal.map_reflective adj c' α f h hα⟩

Premises used: CategoryTheory.IsUniversalColimit.map_reflective, CategoryTheory.IsVanKampenColimit.isUniversal, Iff.intro
-- 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 : 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 α
refine : Nonempty (IsColimit c') → ∀ (j : J), IsPullback (c'.ι.app j) (α.app j) f ((Gl.mapCocone c).ι.app j)
⊢ Nonempty (IsColimit c') ↔ ∀ (j : J), IsPullback (c'.ι.app j) (α.app j) f ((Gl.mapCocone c).ι.app j)

Tactic:
refine ⟨?_, H.isUniversal.map_reflective adj c' α f h hα⟩
-- 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 : 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
⊢ NatTrans.Equifibered α'

Tactic:
have hα' : NatTrans.Equifibered α' := hα.comp (.of_isIso _)
-- 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 : 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 := α ≫ (F.associator Gr Gl).hom ≫ F.whiskerLeft adj.counit ≫ F.rightUnitor.hom
hα' : NatTrans.Equifibered α'
j : J
rw :
  Gl.map (Gr.map (α'.app j)) ≫ adj.counit.app (F.obj j) = (adj.counit.app (F'.1 j) ≫ α.app j) ≫ adj.counit.app (F.obj j)
⊢ Gl.map (Gr.map (α'.app j)) = adj.counit.app (F'.1 j) ≫ α.app j

Tactic:
rw [← cancel_mono (adj.counit.app <| F.obj j)]

Premises used: CategoryTheory.cancel_mono, CategoryTheory.Adjunction.counit, CategoryTheory.Functor.obj, CategoryTheory.NatTrans.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 : 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 := α ≫ (F.associator Gr Gl).hom ≫ F.whiskerLeft adj.counit ≫ F.rightUnitor.hom
hα' : NatTrans.Equifibered α'
j : J
dsimp :
  Gl.map (Gr.map (α.app j ≫ 𝟙 (Gl.obj (Gr.obj (F.obj j))) ≫ adj.counit.app (F.obj j) ≫ 𝟙 (F.obj j))) ≫
      adj.counit.app (F.obj j) =
    (adj.counit.app (F'.1 j) ≫ α.app j) ≫ adj.counit.app (F.obj j)
⊢ Gl.map (Gr.map (α'.app j)) ≫ adj.counit.app (F.obj j) = (adj.counit.app (F'.1 j) ≫ α.app j) ≫ adj.counit.app (F.obj j)

Tactic:
dsimp [α']