awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Types.Pushouts
Goal:
X₁ X₂ X₃ X₄ : Type u
t : X₁ ⟶ X₂
r : X₂ ⟶ X₄
l : X₁ ⟶ X₃
b : X₃ ⟶ X₄
h₁ : IsPullback t l r b
inst : Mono r
h₂ :
  Eq (α := Set ((fun (X : Type u) ↦ X) X₄))
    (Set.range (ι := (fun (X : Type u) ↦ X) X₂)
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) r) : (a : (fun (X : Type u) ↦ X) X₂) → (fun (X : Type u) ↦ X) X₄) ⊔
      Set.range (ι := (fun (X : Type u) ↦ X) X₃)
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) b) : (a : (fun (X : Type u) ↦ X) X₃) → (fun (X : Type u) ↦ X) X₄))
    Set.univ
H :
  ∀ (x₃ y₃ : X₃),
    x₃ ∉
        Set.range (ι := (fun (X : Type u) ↦ X) X₁)
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) l) :
            (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) X₃) →
      y₃ ∉
          Set.range (ι := (fun (X : Type u) ↦ X) X₁)
            (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) l) :
              (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) X₃) →
        Eq (α := (fun (X : Type u) ↦ X) X₄)
            ((ConcreteCategory.hom (FC := TypeCat.Fun) b : (a : (fun (X : Type u) ↦ X) X₃) → (fun (X : Type u) ↦ X) X₄)
                x₃ :
              (fun (X : Type u) ↦ X) X₄)
            ((ConcreteCategory.hom (FC := TypeCat.Fun) b : (a : (fun (X : Type u) ↦ X) X₃) → (fun (X : Type u) ↦ X) X₄)
                y₃ :
              (fun (X : Type u) ↦ X) X₄) →
          x₃ = y₃
⊢ b ≫ 𝟙 X₄ = b

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Types.Yoneda
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
F : Functor.{v_1, v_2, u_1, u_2} J C
X : C
s : (↑(F ⋙ obj coyoneda (op X)).sections : Type (max u_1 v_2))
j j' : J
f : j ⟶ j'
dsimp : 𝟙 X ≫ (↑s : (j : J) → X ⟶ F.obj j) j' = (↑s : (j : J) → X ⟶ F.obj j) j ≫ F.map f
⊢ map (obj (const J) X) f ≫ (↑s : (j : J) → (F ⋙ coyoneda.obj (op X)).obj j) j' =
    (↑s : (j : J) → (F ⋙ coyoneda.obj (op X)).obj j) j ≫ F.map f

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Limits.Types.Yoneda
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
F : Functor.{v_1, v_2, u_1, u_2} J C
X : C
s : (↑(F ⋙ obj coyoneda (op X)).sections : Type (max u_1 v_2))
j j' : J
f : j ⟶ j'
rw : (↑s : (j : J) → X ⟶ F.obj j) j' = (↑s : (j : J) → X ⟶ F.obj j) j ≫ F.map f
⊢ 𝟙 X ≫ (↑s : (j : J) → X ⟶ F.obj j) j' = (↑s : (j : J) → X ⟶ F.obj j) j ≫ F.map f

Tactic:
rw [Category.id_comp]

Premises used: CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Limits.Types.Yoneda
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
F : Functor.{v_1, v_2, u_1, u_2} J C
X : C
s : (↑(F ⋙ obj coyoneda (op X)).sections : Type (max u_1 v_2))
j j' : J
f : j ⟶ j'
⊢ (↑s : (j : J) → X ⟶ F.obj j) j' = (↑s : (j : J) → X ⟶ F.obj j) j ≫ F.map f

Tactic:
(s.property f).symm

Premises used: Eq.symm, Subtype.property
-- Module: Mathlib.CategoryTheory.Limits.Types.Yoneda
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
F : Functor.{v_1, v_2, u_1, u_2} J C
X : C
s : (↑(F ⋙ obj coyoneda (op X)).sections : Type (max u_1 v_2))
j j' : J
f : j ⟶ j'
⊢ (↑s : (j : J) → X ⟶ F.obj j) j' = (↑s : (j : J) → X ⟶ F.obj j) j ≫ F.map f

Tactic:
exact (s.property f).symm

Premises used: Eq.symm, Subtype.property
-- Module: Mathlib.CategoryTheory.Limits.Types.Yoneda
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
F : Functor.{v_1, v_2, u_1, u_2} J C
X : C
τ : obj (const J) X ⟶ F
j j' : J
f : j ⟶ j'
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) ((F ⋙ obj coyoneda (op X)).map f) :
        (a : (fun (X : Type v_2) ↦ X) ((F ⋙ coyoneda.obj (op X)).obj j)) →
          (fun (X : Type v_2) ↦ X) ((F ⋙ coyoneda.obj (op X)).obj j'))
      (τ.app j) =
    τ.app j'

Tactic:
simpa using (τ.naturality f).symm

Premises used: CategoryTheory.NatTrans.naturality, Eq.symm
-- Module: Mathlib.CategoryTheory.Limits.Types.Yoneda
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
F : Functor.{v_1, v_2, u_1, u_2} J C
X : C
s : (↑(F.op ⋙ obj yoneda X).sections : Type (max u_1 v_2))
j j' : J
f : j ⟶ j'
dsimp : F.map f ≫ (↑s : (j : Jᵒᵖ) → F.obj (unop j) ⟶ X) (op j') = (↑s : (j : Jᵒᵖ) → F.obj (unop j) ⟶ X) (op j) ≫ 𝟙 X
⊢ F.map f ≫ (↑s : (j : Jᵒᵖ) → (F.op ⋙ yoneda.obj X).obj j) (op j') =
    (↑s : (j : Jᵒᵖ) → (F.op ⋙ yoneda.obj X).obj j) (op j) ≫ map (obj (const J) X) f

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Limits.Types.Yoneda
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
F : Functor.{v_1, v_2, u_1, u_2} J C
X : C
s : (↑(F.op ⋙ obj yoneda X).sections : Type (max u_1 v_2))
j j' : J
f : j ⟶ j'
rw : F.map f ≫ (↑s : (j : Jᵒᵖ) → F.obj (unop j) ⟶ X) (op j') = (↑s : (j : Jᵒᵖ) → F.obj (unop j) ⟶ X) (op j)
⊢ F.map f ≫ (↑s : (j : Jᵒᵖ) → F.obj (unop j) ⟶ X) (op j') = (↑s : (j : Jᵒᵖ) → F.obj (unop j) ⟶ X) (op j) ≫ 𝟙 X

Tactic:
rw [Category.comp_id]

Premises used: CategoryTheory.Category.comp_id
-- Module: Mathlib.CategoryTheory.Limits.Types.Yoneda
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
F : Functor.{v_1, v_2, u_1, u_2} J C
X : C
s : (↑(F.op ⋙ obj yoneda X).sections : Type (max u_1 v_2))
j j' : J
f : j ⟶ j'
⊢ F.map f ≫ (↑s : (j : Jᵒᵖ) → F.obj (unop j) ⟶ X) (op j') = (↑s : (j : Jᵒᵖ) → F.obj (unop j) ⟶ X) (op j)

Tactic:
(s.property f.op)

Premises used: Quiver.Hom.op, Quiver.Hom.unop, Subtype.property
-- Module: Mathlib.CategoryTheory.Limits.Types.Yoneda
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
F : Functor.{v_1, v_2, u_1, u_2} J C
X : C
s : (↑(F.op ⋙ obj yoneda X).sections : Type (max u_1 v_2))
j j' : J
f : j ⟶ j'
⊢ F.map f ≫ (↑s : (j : Jᵒᵖ) → F.obj (unop j) ⟶ X) (op j') = (↑s : (j : Jᵒᵖ) → F.obj (unop j) ⟶ X) (op j)

Tactic:
exact (s.property f.op)

Premises used: Quiver.Hom.op, Subtype.property
-- Module: Mathlib.CategoryTheory.Limits.Types.Yoneda
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
F : Functor.{v_1, v_2, u_1, u_2} J C
X : C
τ : F ⟶ obj (const J) X
j j' : Jᵒᵖ
f : j ⟶ j'
⊢ Eq (α := (fun (X : Type v_2) ↦ X) ((F.op ⋙ obj yoneda X).obj j'))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((F.op ⋙ obj yoneda X).map f) :
          (a : (fun (X : Type v_2) ↦ X) ((F.op ⋙ yoneda.obj X).obj j)) →
            (fun (X : Type v_2) ↦ X) ((F.op ⋙ yoneda.obj X).obj j'))
        ((fun (j : Jᵒᵖ) ↦ (τ.app (unop j) : F.obj (unop j) ⟶ obj.{v_1, v_2, u_1, u_2} (obj (const J) X) (unop j))) j) :
      (fun (X : Type v_2) ↦ X) ((F.op ⋙ obj yoneda X).obj j'))
    ((fun (j : Jᵒᵖ) ↦ (τ.app (unop j) : F.obj (unop j) ⟶ obj.{v_1, v_2, u_1, u_2} (obj (const J) X) (unop j))) j' :
      F.obj (unop j') ⟶ obj.{v_1, v_2, u_1, u_2} (obj (const J) X) (unop j'))

Tactic:
simp [τ.naturality f.unop]

Premises used: Quiver.Hom.unop, CategoryTheory.NatTrans.naturality
-- Module: Mathlib.CategoryTheory.Limits.Types.Yoneda
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
F : Functor.{v_1, v_2, u_1, u_2} J Cᵒᵖ
X : C
s : (↑(F ⋙ obj yoneda X).sections : Type (max u_1 v_2))
j j' : J
f : j ⟶ j'
dsimp : 𝟙 (op X) ≫ ((↑s : (j : J) → unop (F.obj j) ⟶ X) j').op = ((↑s : (j : J) → unop (F.obj j) ⟶ X) j).op ≫ F.map f
⊢ Eq (α := obj.{v_1, v_2, u_1, u_2} (obj (const J) (op X)) j ⟶ F.obj j')
    (map (obj (const J) (op X)) f ≫ Quiver.Hom.op ((↑s : (j : J) → (F ⋙ yoneda.obj X).obj j) j'))
    (Quiver.Hom.op ((↑s : (j : J) → (F ⋙ yoneda.obj X).obj j) j) ≫ F.map f)

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Limits.Types.Yoneda
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
F : Functor.{v_1, v_2, u_1, u_2} J Cᵒᵖ
X : C
s : (↑(F ⋙ obj yoneda X).sections : Type (max u_1 v_2))
j j' : J
f : j ⟶ j'
rw : ((↑s : (j : J) → unop (F.obj j) ⟶ X) j').op = ((↑s : (j : J) → unop (F.obj j) ⟶ X) j).op ≫ F.map f
⊢ 𝟙 (op X) ≫ ((↑s : (j : J) → unop (F.obj j) ⟶ X) j').op = ((↑s : (j : J) → unop (F.obj j) ⟶ X) j).op ≫ F.map f

Tactic:
rw [Category.id_comp]

Premises used: CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Limits.Types.Yoneda
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
F : Functor.{v_1, v_2, u_1, u_2} J Cᵒᵖ
X : C
s : (↑(F ⋙ obj yoneda X).sections : Type (max u_1 v_2))
j j' : J
f : j ⟶ j'
⊢ ((↑s : (j : J) → unop (F.obj j) ⟶ X) j').op = ((↑s : (j : J) → unop (F.obj j) ⟶ X) j).op ≫ F.map f

Tactic:
Quiver.Hom.unop_inj (s.property f).symm

Premises used: Quiver.Hom.unop_inj, Eq.symm, Subtype.property
-- Module: Mathlib.CategoryTheory.Limits.Types.Yoneda
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
F : Functor.{v_1, v_2, u_1, u_2} J Cᵒᵖ
X : C
s : (↑(F ⋙ obj yoneda X).sections : Type (max u_1 v_2))
j j' : J
f : j ⟶ j'
⊢ ((↑s : (j : J) → unop (F.obj j) ⟶ X) j').op = ((↑s : (j : J) → unop (F.obj j) ⟶ X) j).op ≫ F.map f

Tactic:
exact Quiver.Hom.unop_inj (s.property f).symm

Premises used: Quiver.Hom.unop_inj, Eq.symm, Subtype.property
-- Module: Mathlib.CategoryTheory.Limits.Types.Yoneda
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
F : Functor.{v_1, v_2, u_1, u_2} J Cᵒᵖ
X : C
τ : obj (const J) (op X) ⟶ F
j j' : J
f : j ⟶ j'
⊢ Eq (α := op X ⟶ op (unop (F.obj j')))
    (Quiver.Hom.op
        ((ConcreteCategory.hom (FC := TypeCat.Fun) ((F ⋙ obj yoneda X).map f) :
            (a : (fun (X : Type v_2) ↦ X) ((F ⋙ yoneda.obj X).obj j)) →
              (fun (X : Type v_2) ↦ X) ((F ⋙ yoneda.obj X).obj j'))
          ((fun (j : J) ↦ (τ.app j).unop) j)) :
      op X ⟶ op (unop (F.obj j')))
    (Quiver.Hom.op ((fun (j : J) ↦ (τ.app j).unop) j') : op X ⟶ op (unop (F.obj j')))

Tactic:
simpa using (τ.naturality f).symm

Premises used: CategoryTheory.NatTrans.naturality, Eq.symm
-- Module: Mathlib.CategoryTheory.Limits.Types.Yoneda
Goal:
J : Type v
inst : SmallCategory J
C : Type u
inst_1 : Category.{v, u} C
F : J ⥤ C
X : C
a : limit (F ⋙ obj coyoneda (op X))
x x_1 : J
x_2 : x ⟶ x_1
⊢ Eq (α := obj (obj (const J) X) x ⟶ F.obj x_1)
    (map (obj (const J) X) x_2 ≫
      (ConcreteCategory.hom (FC := TypeCat.Fun) (limit.π (F ⋙ obj coyoneda (op X)) x_1) :
          (a : (fun (X : Type v) ↦ X) (limit (F ⋙ coyoneda.obj (op X)))) →
            (fun (X : Type v) ↦ X) ((F ⋙ coyoneda.obj (op X)).obj x_1))
        a)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (limit.π (F ⋙ obj coyoneda (op X)) x) :
          (a : (fun (X : Type v) ↦ X) (limit (F ⋙ coyoneda.obj (op X)))) →
            (fun (X : Type v) ↦ X) ((F ⋙ coyoneda.obj (op X)).obj x))
        a ≫
      F.map x_2)

Tactic:
simpa using (limit.w_apply _ _ _).symm

Premises used: Eq.symm, CategoryTheory.Limits.limit.w_apply
-- Module: Mathlib.CategoryTheory.Limits.Types.Yoneda
Goal:
J : Type v
inst : SmallCategory J
C : Type u
inst_1 : Category.{v, u} C
F : J ⥤ C
X : C
t : obj (const J) X ⟶ F
⊢ t.app ∈ (F ⋙ obj coyoneda (op X)).sections

Tactic:
simp [Functor.sections, ← t.naturality]

Premises used: CategoryTheory.NatTrans.naturality, CategoryTheory.Functor.sections
-- Module: Mathlib.CategoryTheory.Limits.Types.Yoneda
Goal:
J : Type v
inst : SmallCategory J
C : Type u
inst_1 : Category.{v, u} C
F : J ⥤ C
X : C
a : limit (F.op ⋙ obj yoneda X)
x x_1 : J
f : x ⟶ x_1
⊢ Eq (α := F.obj x ⟶ obj (obj (const J) X) x_1)
    (F.map f ≫
      (ConcreteCategory.hom (FC := TypeCat.Fun) (limit.π (F.op ⋙ obj yoneda X) (op x_1)) :
          (a : (fun (X : Type v) ↦ X) (limit (F.op ⋙ yoneda.obj X))) →
            (fun (X : Type v) ↦ X) ((F.op ⋙ yoneda.obj X).obj (op x_1)))
        a)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (limit.π (F.op ⋙ obj yoneda X) (op x)) :
          (a : (fun (X : Type v) ↦ X) (limit (F.op ⋙ yoneda.obj X))) →
            (fun (X : Type v) ↦ X) ((F.op ⋙ yoneda.obj X).obj (op x)))
        a ≫
      map (obj (const J) X) f)

Tactic:
simpa using (limit.w_apply (F.op ⋙ yoneda.obj X) f.op a)

Premises used: CategoryTheory.Functor.op, Quiver.Hom.op, CategoryTheory.Functor.comp, CategoryTheory.yoneda, CategoryTheory.Functor.obj, CategoryTheory.Limits.limit.w_apply
-- Module: Mathlib.CategoryTheory.Limits.Types.Yoneda
Goal:
J : Type v
inst : SmallCategory J
C : Type u
inst_1 : Category.{v, u} C
F : J ⥤ C
X : C
t : F ⟶ obj (const J) X
⊢ (fun (j : Jᵒᵖ) ↦ t.app (unop j)) ∈ (F.op ⋙ obj yoneda X).sections

Tactic:
simp [Functor.sections]

Premises used: CategoryTheory.Functor.sections
-- Module: Mathlib.CategoryTheory.Limits.Unit
Goal:
J : Type v
inst : Category.{v', v} J
F : Functor.{v', u_1, v, u_1} J (Discrete PUnit.{u_1 + 1})
c s : Cone F
⊢ s.pt = c.pt

Tactic:
simp [eq_iff_true_of_subsingleton]

Premises used: eq_iff_true_of_subsingleton
-- Module: Mathlib.CategoryTheory.Limits.Unit
Goal:
J : Type v
inst : Category.{v', v} J
F : Functor.{v', u_1, v, u_1} J (Discrete PUnit.{u_1 + 1})
c s : Cocone F
⊢ c.pt = s.pt

Tactic:
simp [eq_iff_true_of_subsingleton]

Premises used: eq_iff_true_of_subsingleton
-- Module: Mathlib.CategoryTheory.Limits.Unit
Goal:
J : Type v
inst : Category.{v', v} J
F : Functor.{v', ?u.5339, v, ?u.5339} J (Discrete PUnit.{?u.5339 + 1})
⊢ HasLimitsOfSize.{v', v, u_1, u_1} (Discrete PUnit.{u_1 + 1})

Tactic:
⟨fun _ _ => ⟨fun _ => ⟨punitCone, punitConeIsLimit⟩⟩⟩

Premises used: CategoryTheory.Limits.punitCone, CategoryTheory.Limits.HasLimitsOfShape.mk, CategoryTheory.Limits.punitConeIsLimit, CategoryTheory.Limits.HasLimitsOfSize.mk, Nonempty.intro, CategoryTheory.Limits.HasLimit.mk', CategoryTheory.Limits.LimitCone.mk
-- Module: Mathlib.CategoryTheory.Limits.Unit
Goal:
J : Type v
inst : Category.{v', v} J
F : Functor.{v', ?u.6329, v, ?u.6329} J (Discrete PUnit.{?u.6329 + 1})
⊢ HasColimitsOfSize.{v', v, u_1, u_1} (Discrete PUnit.{u_1 + 1})

Tactic:
⟨fun _ _ => ⟨fun _ => ⟨punitCocone, punitCoconeIsColimit⟩⟩⟩

Premises used: CategoryTheory.Limits.HasColimitsOfShape.mk, CategoryTheory.Limits.punitCoconeIsColimit, Nonempty.intro, CategoryTheory.Limits.HasColimit.mk', CategoryTheory.Limits.ColimitCocone.mk, CategoryTheory.Limits.HasColimitsOfSize.mk, CategoryTheory.Limits.punitCocone
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
F : Functor.{u', v, v', u} J C
c : Cocone F
H : IsVanKampenColimit c
⊢ IsUniversalColimit c

Tactic:
fun _ c' α f h hα => (H c' α f h hα).mpr

Premises used: Iff.mpr, CategoryTheory.IsUniversalColimit
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
K : Type u_1
inst_2 : Category.{v_1, u_1} K
D : Type u_2
inst_3 : Category.{v_2, u_2} D
F : Functor.{u', v, v', u} J C
c : Cocone F
h : IsUniversalColimit c
rw : 𝟙 F ≫ c.ι = c.ι ≫ 𝟙 (obj (const J) c.pt)
rw₁ : 𝟙 F ≫ c.ι = c.ι
rw₂ rw₃ : c.ι = c.ι
⊢ 𝟙 F ≫ c.ι = c.ι ≫ map (const J) (𝟙 c.pt)

Tactic:
rw [Functor.map_id, Category.comp_id, Category.id_comp]

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.Functor.map_id, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
K : Type u_1
inst_2 : Category.{v_1, u_1} K
D : Type u_2
inst_3 : Category.{v_2, u_2} D
F : Functor.{u', v, v', u} J C
c : Cocone F
h : IsUniversalColimit c
refine : ∀ (j : J), IsPullback (c.ι.app j) (NatTrans.app (𝟙 F) j) (𝟙 c.pt) (c.ι.app j)
⊢ IsColimit c

Tactic:
refine ((h c (𝟙 F) (𝟙 c.pt :) (by rw [Functor.map_id, Category.comp_id, Category.id_comp])
    (.of_isIso _)) fun j => ?_).some

Premises used: CategoryTheory.NatTrans.Equifibered.of_isIso, CategoryTheory.CategoryStruct.id, Nonempty.some, CategoryTheory.Limits.Cocone.pt
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
K : Type u_1
inst_2 : Category.{v_1, u_1} K
D : Type u_2
inst_3 : Category.{v_2, u_2} D
F : Functor.{u', v, v', u} J C
c : Cocone F
h : IsUniversalColimit c
j : J
⊢ IsIso.{v, u} (𝟙 c.pt)

Tactic:
haveI : IsIso (𝟙 c.pt) := inferInstance
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
K : Type u_1
inst_2 : Category.{v_1, u_1} K
D : Type u_2
inst_3 : Category.{v_2, u_2} D
F : Functor.{u', v, v', u} J C
c : Cocone F
h : IsUniversalColimit c
j : J
this : IsIso.{v, u} (𝟙 c.pt)
⊢ c.ι.app j ≫ 𝟙 c.pt = NatTrans.app (𝟙 F) j ≫ c.ι.app j

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
K : Type u_1
inst_2 : Category.{v_1, u_1} K
D : Type u_2
inst_3 : Category.{v_2, u_2} D
F : Functor.{u', v, v', u} J C
c : Cocone F
h : IsUniversalColimit c
j : J
this : IsIso.{v, u} (𝟙 c.pt)
⊢ IsPullback (c.ι.app j) (NatTrans.app (𝟙 F) j) (𝟙 c.pt) (c.ι.app j)

Tactic:
exact IsPullback.of_vert_isIso ⟨by simp⟩

Premises used: CategoryTheory.IsPullback.of_vert_isIso, CategoryTheory.CommSq.mk
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasStrictInitialObjects.{v, u} C
X : C
h : IsInitial.{v, u} X
F' : Functor.{0, v, 0, u} (Discrete PEmpty.{1}) C
c' : Cocone F'
α : F' ⟶ empty C
f : c'.pt ⟶ Cocone.pt.{0, v, 0, u} (asEmptyCocone X)
hf : α ≫ Cocone.ι (asEmptyCocone X) = c'.ι ≫ map (const (Discrete PEmpty.{1})) f
hα : NatTrans.Equifibered α
h_obj : ∀ (X : Discrete PEmpty.{1}), F'.obj X = obj.{0, v, 0, u} (empty C) X
h_map :
  ∀ (X Y : Discrete PEmpty.{1}) (f : X ⟶ Y),
    HEq (F'.map f) (β := obj.{0, v, 0, u} (empty C) X ⟶ obj.{0, v, 0, u} (empty C) Y) (map (empty C) f)
⊢ F' = empty C

Tactic:
apply Functor.hext

Premises used: CategoryTheory.Functor.hext
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasStrictInitialObjects.{v, u} C
X : C
h : IsInitial.{v, u} X
F' : Functor.{0, v, 0, u} (Discrete PEmpty.{1}) C
c' : Cocone F'
α : F' ⟶ empty C
f : c'.pt ⟶ Cocone.pt.{0, v, 0, u} (asEmptyCocone X)
hf : α ≫ Cocone.ι (asEmptyCocone X) = c'.ι ≫ map (const (Discrete PEmpty.{1})) f
hα : NatTrans.Equifibered α
⊢ F' = empty C

Tactic:
have : F' = Functor.empty C := by apply Functor.hext <;> rintro ⟨⟨⟩⟩
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasStrictInitialObjects.{v, u} C
X : C
h : IsInitial.{v, u} X
F' : Functor.{0, v, 0, u} (Discrete PEmpty.{1}) C
c' : Cocone F'
α : F' ⟶ empty C
f : c'.pt ⟶ Cocone.pt.{0, v, 0, u} (asEmptyCocone X)
hf : α ≫ Cocone.ι (asEmptyCocone X) = c'.ι ≫ map (const (Discrete PEmpty.{1})) f
hα : NatTrans.Equifibered α
this : F' = empty C
subst :
  ∀ (c' : Cocone.{0, v, 0, u} (empty C))
    (α : Quiver.Hom (V := Functor.{0, v, 0, u} (Discrete PEmpty.{1}) C) (empty C) (empty C))
    (f : c'.pt ⟶ Cocone.pt.{0, v, 0, u} (asEmptyCocone X))
    (hf : α ≫ Cocone.ι (asEmptyCocone X) = c'.ι ≫ map (const (Discrete PEmpty.{1})) f) (hα : NatTrans.Equifibered α),
    Nonempty (IsColimit c') ↔
      ∀ (j : Discrete PEmpty.{1}), IsPullback (c'.ι.app j) (α.app j) f (NatTrans.app (Cocone.ι (asEmptyCocone X)) j)
⊢ Nonempty (IsColimit c') ↔
    ∀ (j : Discrete PEmpty.{1}), IsPullback (c'.ι.app j) (α.app j) f (NatTrans.app (Cocone.ι (asEmptyCocone X)) j)

Tactic:
subst this
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasStrictInitialObjects.{v, u} C
X : C
h : IsInitial.{v, u} X
c' : Cocone.{0, v, 0, u} (empty C)
α : Quiver.Hom (V := Functor.{0, v, 0, u} (Discrete PEmpty.{1}) C) (empty C) (empty C)
f : c'.pt ⟶ Cocone.pt.{0, v, 0, u} (asEmptyCocone X)
hf : α ≫ Cocone.ι (asEmptyCocone X) = c'.ι ≫ map (const (Discrete PEmpty.{1})) f
hα : NatTrans.Equifibered α
⊢ IsIso f

Tactic:
haveI := h.isIso_to f
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasStrictInitialObjects.{v, u} C
X : C
h : IsInitial.{v, u} X
c' : Cocone.{0, v, 0, u} (empty C)
α : Quiver.Hom (V := Functor.{0, v, 0, u} (Discrete PEmpty.{1}) C) (empty C) (empty C)
f : c'.pt ⟶ Cocone.pt.{0, v, 0, u} (asEmptyCocone X)
hf : α ≫ Cocone.ι (asEmptyCocone X) = c'.ι ≫ map (const (Discrete PEmpty.{1})) f
hα : NatTrans.Equifibered α
this : IsIso f
⊢ Nonempty (IsColimit c') ↔
    ∀ (j : Discrete PEmpty.{1}), IsPullback (c'.ι.app j) (α.app j) f (NatTrans.app (Cocone.ι (asEmptyCocone X)) j)

Tactic:
refine ⟨by rintro _ ⟨⟨⟩⟩,
    fun _ => ⟨IsColimit.ofIsoColimit h (Cocone.ext (asIso f).symm <| by rintro ⟨⟨⟩⟩)⟩⟩
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
F : Functor.{u', v, v', u} J C
c c' : Cocone F
hc : IsUniversalColimit c
e : c ≅ c'
F' : Functor.{u', v, v', u} J C
c'' : Cocone F'
α : F' ⟶ F
f : c''.pt ⟶ c'.pt
h : α ≫ c'.ι = c''.ι ≫ map (const J) f
hα : NatTrans.Equifibered α
H : ∀ (j : J), IsPullback (c''.ι.app j) (α.app j) f (c'.ι.app j)
w : ∀ (j : J), (c'.ι ≫ map (const J) e.inv.hom).app j = c.ι.app j
⊢ c'.ι ≫ map (const J) e.inv.hom = 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
F : Functor.{u', v, v', u} J C
c c' : Cocone F
hc : IsUniversalColimit c
e : c ≅ c'
F' : Functor.{u', v, v', u} J C
c'' : Cocone F'
α : F' ⟶ F
f : c''.pt ⟶ c'.pt
h : α ≫ c'.ι = c''.ι ≫ map (const J) f
hα : NatTrans.Equifibered α
H : ∀ (j : J), IsPullback (c''.ι.app j) (α.app j) f (c'.ι.app j)
j : J
⊢ (c'.ι ≫ map (const J) e.inv.hom).app j = c.ι.app j

Tactic:
e.inv.2 j

Premises used: CategoryTheory.Limits.CoconeMorphism.w, CategoryTheory.Iso.inv
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
F : Functor.{u', v, v', u} J C
c c' : Cocone F
hc : IsUniversalColimit c
e : c ≅ c'
F' : Functor.{u', v, v', u} J C
c'' : Cocone F'
α : F' ⟶ F
f : c''.pt ⟶ c'.pt
h : α ≫ c'.ι = c''.ι ≫ map (const J) f
hα : NatTrans.Equifibered α
H : ∀ (j : J), IsPullback (c''.ι.app j) (α.app j) f (c'.ι.app j)
j : J
⊢ (c'.ι ≫ map (const J) e.inv.hom).app j = c.ι.app j

Tactic:
exact e.inv.2 j

Premises used: CategoryTheory.Limits.CoconeMorphism.w, CategoryTheory.Iso.inv
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
F : Functor.{u', v, v', u} J C
c c' : Cocone F
hc : IsUniversalColimit c
e : c ≅ c'
F' : Functor.{u', v, v', u} J C
c'' : Cocone F'
α : F' ⟶ F
f : c''.pt ⟶ c'.pt
h : α ≫ c'.ι = c''.ι ≫ map (const J) f
hα : NatTrans.Equifibered α
H : ∀ (j : J), IsPullback (c''.ι.app j) (α.app j) f (c'.ι.app j)
⊢ c'.ι ≫ map (const J) e.inv.hom = c.ι

Tactic:
have : c'.ι ≫ (Functor.const J).map e.inv.hom = c.ι := by
    ext j
    exact e.inv.2 j
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
F : Functor.{u', v, v', u} J C
c c' : Cocone F
hc : IsUniversalColimit c
e : c ≅ c'
F' : Functor.{u', v, v', u} J C
c'' : Cocone F'
α : F' ⟶ F
f : c''.pt ⟶ c'.pt
h : α ≫ c'.ι = c''.ι ≫ map (const J) f
hα : NatTrans.Equifibered α
H : ∀ (j : J), IsPullback (c''.ι.app j) (α.app j) f (c'.ι.app j)
this : c'.ι ≫ map (const J) e.inv.hom = c.ι
rw : α ≫ c.ι = c''.ι ≫ map (const J) f ≫ map (const J) e.inv.hom
rw₁ : α ≫ c.ι = α ≫ c'.ι ≫ map (const J) e.inv.hom
rw₂ rw₃ : α ≫ c.ι = α ≫ c.ι
⊢ α ≫ c.ι = c''.ι ≫ map (const J) (f ≫ e.inv.hom)

Tactic:
rw [Functor.map_comp, ← reassoc_of% h, this]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
F : Functor.{u', v, v', u} J C
c c' : Cocone F
hc : IsUniversalColimit c
e : c ≅ c'
F' : Functor.{u', v, v', u} J C
c'' : Cocone F'
α : F' ⟶ F
f : c''.pt ⟶ c'.pt
h : α ≫ c'.ι = c''.ι ≫ map (const J) f
hα : NatTrans.Equifibered α
H : ∀ (j : J), IsPullback (c''.ι.app j) (α.app j) f (c'.ι.app j)
this : c'.ι ≫ map (const J) e.inv.hom = c.ι
apply : ∀ (j : J), IsPullback (c''.ι.app j) (α.app j) (f ≫ e.inv.hom) (c.ι.app j)
⊢ Nonempty (IsColimit c'')

Tactic:
apply hc c'' α (f ≫ e.inv.1) (by rw [Functor.map_comp, ← reassoc_of% h, this]) hα

Premises used: CategoryTheory.Limits.CoconeMorphism.hom, CategoryTheory.CategoryStruct.comp, CategoryTheory.Iso.inv