awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type u_3
S B : C
X : ι → C
a : Cofan.{u_3, v, u} X
hau : IsUniversalColimit a
f : (i : ι) → X i ⟶ S
u : a.pt ⟶ S
v : B ⟶ S
s : (i : ι) → PullbackCone (f i) v
hs : (i : ι) → IsLimit (s i)
t : PullbackCone u v
ht : IsLimit t
d : Cofan.{u_3, v, u} (C := C) fun (i : ι) ↦ (s i).pt
e : d.pt ≅ t.pt
hu : ∀ (i : ι), a.inj i ≫ u = f i
he₁ : ∀ (i : ι), d.inj i ≫ e.hom ≫ t.fst = (s i).fst ≫ a.inj i
he₂ : ∀ (i : ι), d.inj i ≫ e.hom ≫ t.snd = (s i).snd
iso : d ≅ Cofan.mk t.pt fun (i : ι) ↦ PullbackCone.IsLimit.lift ht ((s i).fst ≫ a.inj i) (s i).snd ⋯ := Cofan.ext e ⋯
j : Discrete ι
⊢ IsPullback (P := Cone.pt (F := cospan (X := X j.as) (f j.as) v) (s j.as))
    (PullbackCone.IsLimit.lift ht (PullbackCone.fst (s j.as) ≫ a.inj j.as) (PullbackCone.snd (s j.as)) ⋯ ≫ t.snd)
    (PullbackCone.fst (s j.as)) v (a.inj j.as ≫ u)

Tactic:
simpa [hu] using (IsPullback.of_isLimit (hs j.1)).flip

Premises used: CategoryTheory.IsPullback.of_isLimit, CategoryTheory.Discrete.as, CategoryTheory.IsPullback.flip
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type u_3
S B : C
X : ι → C
a : Cofan.{u_3, v, u} X
hau : IsUniversalColimit a
f : (i : ι) → X i ⟶ S
u : a.pt ⟶ S
v : B ⟶ S
P : ι → C
q₁ : (i : ι) → P i ⟶ X i
q₂ : (i : ι) → P i ⟶ B
hP : ∀ (i : ι), IsPullback (q₁ i) (q₂ i) (f i) v
Z : C
p₁ : Z ⟶ a.pt
p₂ : Z ⟶ B
h : IsPullback p₁ p₂ u v
d : Cofan.{u_3, v, u} P
e : d.pt ≅ Z
hu : ∀ (i : ι), a.inj i ≫ u = f i
he₁ : ∀ (i : ι), d.inj i ≫ e.hom ≫ p₁ = q₁ i ≫ a.inj i
he₂ : ∀ (i : ι), d.inj i ≫ e.hom ≫ p₂ = q₂ i
⊢ Nonempty (IsColimit d)

Tactic:
hau.nonempty_isColimit_of_pullbackCone_right f u v (fun i ↦ (hP i).cone)
    (fun i ↦ (hP i).isLimit) h.cone h.isLimit d e

Premises used: CategoryTheory.IsUniversalColimit.nonempty_isColimit_of_pullbackCone_right, CategoryTheory.IsPullback.cone, CategoryTheory.IsPullback.isLimit
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type u_3
S B : C
X : ι → C
a : Cofan.{u_3, v, u} X
hau : IsUniversalColimit a
f : (i : ι) → X i ⟶ S
u : a.pt ⟶ S
v : B ⟶ S
P : ι → C
q₁ : (i : ι) → P i ⟶ X i
q₂ : (i : ι) → P i ⟶ B
hP : ∀ (i : ι), IsPullback (q₁ i) (q₂ i) (f i) v
d : Cofan.{u_3, v, u} P
hd : IsColimit d
hu : ∀ (i : ι), a.inj i ≫ u = f i
inst_1 : HasPullback u v
i : ι
⊢ (q₁ i ≫ a.inj i) ≫ u = q₂ i ≫ v

Tactic:
simp [(hP i).w, hu]

Premises used: CategoryTheory.IsPullback.toCommSq, CategoryTheory.CommSq.w
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type u_3
S B : C
X : ι → C
a : Cofan.{u_3, v, u} X
hau : IsUniversalColimit a
f : (i : ι) → X i ⟶ S
u : a.pt ⟶ S
v : B ⟶ S
P : ι → C
q₁ : (i : ι) → P i ⟶ X i
q₂ : (i : ι) → P i ⟶ B
hP : ∀ (i : ι), IsPullback (q₁ i) (q₂ i) (f i) v
d : Cofan.{u_3, v, u} P
hd : IsColimit d
hu : ∀ (i : ι), a.inj i ≫ u = f i
inst_1 : HasPullback u v
c : Cofan.{u_3, v, u} P := Cofan.mk (pullback u v) fun (i : ι) ↦ pullback.lift (q₁ i ≫ a.inj i) (q₂ i) ⋯
obtain :
  ∀ (hc : IsColimit c),
    IsPullback (Cofan.IsColimit.desc hd fun (x : ι) ↦ q₁ x ≫ a.inj x) (Cofan.IsColimit.desc hd q₂) u v
⊢ IsPullback (Cofan.IsColimit.desc hd fun (x : ι) ↦ q₁ x ≫ a.inj x) (Cofan.IsColimit.desc hd q₂) u v

Tactic:
obtain ⟨hc⟩ := hau.nonempty_isColimit_of_isPullback_right f u
    v q₁ q₂ hP (IsPullback.of_hasPullback _ _) c (Iso.refl _)

Premises used: CategoryTheory.Iso.refl, CategoryTheory.IsPullback.of_hasPullback, CategoryTheory.IsUniversalColimit.nonempty_isColimit_of_isPullback_right
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type u_3
S B : C
X : ι → C
a : Cofan.{u_3, v, u} X
hau : IsUniversalColimit a
f : (i : ι) → X i ⟶ S
u : a.pt ⟶ S
v : B ⟶ S
P : ι → C
q₁ : (i : ι) → P i ⟶ X i
q₂ : (i : ι) → P i ⟶ B
hP : ∀ (i : ι), IsPullback (q₁ i) (q₂ i) (f i) v
d : Cofan.{u_3, v, u} P
hd : IsColimit d
hu : ∀ (i : ι), a.inj i ≫ u = f i
inst_1 : HasPullback u v
c : Cofan.{u_3, v, u} P := Cofan.mk (pullback u v) fun (i : ι) ↦ pullback.lift (q₁ i ≫ a.inj i) (q₂ i) ⋯
hc : IsColimit c
⊢ u ≫ Iso.hom (Iso.refl S) = Iso.hom (Iso.refl a.pt) ≫ u

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type u_3
S B : C
X : ι → C
a : Cofan.{u_3, v, u} X
hau : IsUniversalColimit a
f : (i : ι) → X i ⟶ S
u : a.pt ⟶ S
v : B ⟶ S
P : ι → C
q₁ : (i : ι) → P i ⟶ X i
q₂ : (i : ι) → P i ⟶ B
hP : ∀ (i : ι), IsPullback (q₁ i) (q₂ i) (f i) v
d : Cofan.{u_3, v, u} P
hd : IsColimit d
hu : ∀ (i : ι), a.inj i ≫ u = f i
inst_1 : HasPullback u v
c : Cofan.{u_3, v, u} P := Cofan.mk (pullback u v) fun (i : ι) ↦ pullback.lift (q₁ i ≫ a.inj i) (q₂ i) ⋯
hc : IsColimit c
⊢ v ≫ Iso.hom (Iso.refl S) = Iso.hom (Iso.refl B) ≫ v

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type u_3
S B : C
X : ι → C
a : Cofan.{u_3, v, u} X
hau : IsUniversalColimit a
f : (i : ι) → X i ⟶ S
u : a.pt ⟶ S
v : B ⟶ S
P : ι → C
q₁ : (i : ι) → P i ⟶ X i
q₂ : (i : ι) → P i ⟶ B
hP : ∀ (i : ι), IsPullback (q₁ i) (q₂ i) (f i) v
d : Cofan.{u_3, v, u} P
hd : IsColimit d
hu : ∀ (i : ι), a.inj i ≫ u = f i
inst_1 : HasPullback u v
c : Cofan.{u_3, v, u} P := Cofan.mk (pullback u v) fun (i : ι) ↦ pullback.lift (q₁ i ≫ a.inj i) (q₂ i) ⋯
hc : IsColimit c
refine_1 : pullback u v ≅ d.pt
refine_2 :
  pullback.fst u v ≫ Iso.hom (Iso.refl a.pt) =
    (hc.coconePointUniqueUpToIso hd).hom ≫ Cofan.IsColimit.desc hd fun (x : ι) ↦ q₁ x ≫ a.inj x
refine_3 : pullback.snd u v ≫ Iso.hom (Iso.refl B) = (hc.coconePointUniqueUpToIso hd).hom ≫ Cofan.IsColimit.desc hd q₂
⊢ IsPullback (Cofan.IsColimit.desc hd fun (x : ι) ↦ q₁ x ≫ a.inj x) (Cofan.IsColimit.desc hd q₂) u v

Tactic:
refine (IsPullback.of_hasPullback u v).of_iso
      ?_ (Iso.refl _) (Iso.refl _) (Iso.refl _) ?_ ?_ (by simp) (by simp)

Premises used: CategoryTheory.Iso.refl, CategoryTheory.IsPullback.of_iso, CategoryTheory.IsPullback.of_hasPullback
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type u_3
S B : C
X : ι → C
a : Cofan.{u_3, v, u} X
hau : IsUniversalColimit a
f : (i : ι) → X i ⟶ S
u : a.pt ⟶ S
v : B ⟶ S
P : ι → C
q₁ : (i : ι) → P i ⟶ X i
q₂ : (i : ι) → P i ⟶ B
hP : ∀ (i : ι), IsPullback (q₁ i) (q₂ i) (f i) v
d : Cofan.{u_3, v, u} P
hd : IsColimit d
hu : ∀ (i : ι), a.inj i ≫ u = f i
inst_1 : HasPullback u v
c : Cofan.{u_3, v, u} P := Cofan.mk (pullback u v) fun (i : ι) ↦ pullback.lift (q₁ i ≫ a.inj i) (q₂ i) ⋯
hc : IsColimit c
⊢ pullback u v ≅ d.pt

Tactic:
exact hc.coconePointUniqueUpToIso hd

Premises used: CategoryTheory.Limits.IsColimit.coconePointUniqueUpToIso
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type u_3
S B : C
X : ι → C
a : Cofan.{u_3, v, u} X
hau : IsUniversalColimit a
f : (i : ι) → X i ⟶ S
u : a.pt ⟶ S
v : B ⟶ S
P : ι → C
q₁ : (i : ι) → P i ⟶ X i
q₂ : (i : ι) → P i ⟶ B
hP : ∀ (i : ι), IsPullback (q₁ i) (q₂ i) (f i) v
d : Cofan.{u_3, v, u} P
hd : IsColimit d
hu : ∀ (i : ι), a.inj i ≫ u = f i
inst_1 : HasPullback u v
c : Cofan.{u_3, v, u} P := Cofan.mk (pullback u v) fun (i : ι) ↦ pullback.lift (q₁ i ≫ a.inj i) (q₂ i) ⋯
hc : IsColimit c
⊢ pullback.fst u v ≫ Iso.hom (Iso.refl a.pt) =
    (hc.coconePointUniqueUpToIso hd).hom ≫ Cofan.IsColimit.desc hd fun (x : ι) ↦ q₁ x ≫ a.inj x

Tactic:
Cofan.IsColimit.hom_ext hc _ _ fun i ↦ ?_

Premises used: CategoryTheory.Limits.Cofan.IsColimit.hom_ext, CategoryTheory.Limits.limit
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type u_3
S B : C
X : ι → C
a : Cofan.{u_3, v, u} X
hau : IsUniversalColimit a
f : (i : ι) → X i ⟶ S
u : a.pt ⟶ S
v : B ⟶ S
P : ι → C
q₁ : (i : ι) → P i ⟶ X i
q₂ : (i : ι) → P i ⟶ B
hP : ∀ (i : ι), IsPullback (q₁ i) (q₂ i) (f i) v
d : Cofan.{u_3, v, u} P
hd : IsColimit d
hu : ∀ (i : ι), a.inj i ≫ u = f i
inst_1 : HasPullback u v
c : Cofan.{u_3, v, u} P := Cofan.mk (pullback u v) fun (i : ι) ↦ pullback.lift (q₁ i ≫ a.inj i) (q₂ i) ⋯
hc : IsColimit c
refine_2 :
  ∀ (i : ι),
    c.inj i ≫ pullback.fst u v ≫ Iso.hom (Iso.refl a.pt) =
      c.inj i ≫ (hc.coconePointUniqueUpToIso hd).hom ≫ Cofan.IsColimit.desc hd fun (x : ι) ↦ q₁ x ≫ a.inj x
⊢ pullback.fst u v ≫ Iso.hom (Iso.refl a.pt) =
    (hc.coconePointUniqueUpToIso hd).hom ≫ Cofan.IsColimit.desc hd fun (x : ι) ↦ q₁ x ≫ a.inj x

Tactic:
refine Cofan.IsColimit.hom_ext hc _ _ fun i ↦ ?_

Premises used: CategoryTheory.Limits.Cofan.IsColimit.hom_ext
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type u_3
S B : C
X : ι → C
a : Cofan.{u_3, v, u} X
hau : IsUniversalColimit a
f : (i : ι) → X i ⟶ S
u : a.pt ⟶ S
v : B ⟶ S
P : ι → C
q₁ : (i : ι) → P i ⟶ X i
q₂ : (i : ι) → P i ⟶ B
hP : ∀ (i : ι), IsPullback (q₁ i) (q₂ i) (f i) v
d : Cofan.{u_3, v, u} P
hd : IsColimit d
hu : ∀ (i : ι), a.inj i ≫ u = f i
inst_1 : HasPullback u v
c : Cofan.{u_3, v, u} P := Cofan.mk (pullback u v) fun (i : ι) ↦ pullback.lift (q₁ i ≫ a.inj i) (q₂ i) ⋯
hc : IsColimit c
i : ι
⊢ c.inj i ≫ pullback.fst u v ≫ Iso.hom (Iso.refl a.pt) =
    c.inj i ≫ (hc.coconePointUniqueUpToIso hd).hom ≫ Cofan.IsColimit.desc hd fun (x : ι) ↦ q₁ x ≫ a.inj x

Tactic:
simpa [Cofan.inj, Cofan.IsColimit.desc] using pullback.lift_fst _ _ _

Premises used: CategoryTheory.Limits.Cofan.IsColimit.desc, CategoryTheory.Limits.Cofan.inj, CategoryTheory.Limits.pullback.lift_fst
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type u_3
S B : C
X : ι → C
a : Cofan.{u_3, v, u} X
hau : IsUniversalColimit a
f : (i : ι) → X i ⟶ S
u : a.pt ⟶ S
v : B ⟶ S
P : ι → C
q₁ : (i : ι) → P i ⟶ X i
q₂ : (i : ι) → P i ⟶ B
hP : ∀ (i : ι), IsPullback (q₁ i) (q₂ i) (f i) v
d : Cofan.{u_3, v, u} P
hd : IsColimit d
hu : ∀ (i : ι), a.inj i ≫ u = f i
inst_1 : HasPullback u v
c : Cofan.{u_3, v, u} P := Cofan.mk (pullback u v) fun (i : ι) ↦ pullback.lift (q₁ i ≫ a.inj i) (q₂ i) ⋯
hc : IsColimit c
⊢ pullback.snd u v ≫ Iso.hom (Iso.refl B) = (hc.coconePointUniqueUpToIso hd).hom ≫ Cofan.IsColimit.desc hd q₂

Tactic:
Cofan.IsColimit.hom_ext hc _ _ fun i ↦ ?_

Premises used: CategoryTheory.Limits.Cofan.IsColimit.hom_ext, CategoryTheory.Limits.limit
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type u_3
S B : C
X : ι → C
a : Cofan.{u_3, v, u} X
hau : IsUniversalColimit a
f : (i : ι) → X i ⟶ S
u : a.pt ⟶ S
v : B ⟶ S
P : ι → C
q₁ : (i : ι) → P i ⟶ X i
q₂ : (i : ι) → P i ⟶ B
hP : ∀ (i : ι), IsPullback (q₁ i) (q₂ i) (f i) v
d : Cofan.{u_3, v, u} P
hd : IsColimit d
hu : ∀ (i : ι), a.inj i ≫ u = f i
inst_1 : HasPullback u v
c : Cofan.{u_3, v, u} P := Cofan.mk (pullback u v) fun (i : ι) ↦ pullback.lift (q₁ i ≫ a.inj i) (q₂ i) ⋯
hc : IsColimit c
refine_3 :
  ∀ (i : ι),
    c.inj i ≫ pullback.snd u v ≫ Iso.hom (Iso.refl B) =
      c.inj i ≫ (hc.coconePointUniqueUpToIso hd).hom ≫ Cofan.IsColimit.desc hd q₂
⊢ pullback.snd u v ≫ Iso.hom (Iso.refl B) = (hc.coconePointUniqueUpToIso hd).hom ≫ Cofan.IsColimit.desc hd q₂

Tactic:
refine Cofan.IsColimit.hom_ext hc _ _ fun i ↦ ?_

Premises used: CategoryTheory.Limits.Cofan.IsColimit.hom_ext
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type u_3
S B : C
X : ι → C
a : Cofan.{u_3, v, u} X
hau : IsUniversalColimit a
f : (i : ι) → X i ⟶ S
u : a.pt ⟶ S
v : B ⟶ S
P : ι → C
q₁ : (i : ι) → P i ⟶ X i
q₂ : (i : ι) → P i ⟶ B
hP : ∀ (i : ι), IsPullback (q₁ i) (q₂ i) (f i) v
d : Cofan.{u_3, v, u} P
hd : IsColimit d
hu : ∀ (i : ι), a.inj i ≫ u = f i
inst_1 : HasPullback u v
c : Cofan.{u_3, v, u} P := Cofan.mk (pullback u v) fun (i : ι) ↦ pullback.lift (q₁ i ≫ a.inj i) (q₂ i) ⋯
hc : IsColimit c
i : ι
⊢ c.inj i ≫ pullback.snd u v ≫ Iso.hom (Iso.refl B) =
    c.inj i ≫ (hc.coconePointUniqueUpToIso hd).hom ≫ Cofan.IsColimit.desc hd q₂

Tactic:
simpa [Cofan.inj, Cofan.IsColimit.desc] using pullback.lift_snd _ _ _

Premises used: CategoryTheory.Limits.Cofan.IsColimit.desc, CategoryTheory.Limits.pullback.lift_snd, CategoryTheory.Limits.Cofan.inj
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type u_3
ι' : Type u_4
S : C
X : ι → C
a : Cofan.{u_3, v, u} X
hau : IsUniversalColimit a
Y : ι' → C
b : Cofan.{u_4, v, u} Y
hbu : IsUniversalColimit b
f : (i : ι) → X i ⟶ S
g : (i : ι') → Y i ⟶ S
u : a.pt ⟶ S
v : b.pt ⟶ S
inst_1 : ∀ (i : ι), HasPullback (f i) v
s : (i : ι) → (j : ι') → PullbackCone (f i) (g j)
hs : (i : ι) → (j : ι') → IsLimit (s i j)
t : PullbackCone u v
ht : IsLimit t
d : Cofan (C := C) fun (p : ι × ι') ↦ Cone.pt (F := cospan (X := X p.1) (Y := Y p.2) (f p.1) (g p.2)) (s p.1 p.2)
e : d.pt ≅ t.pt
hu : ∀ (i : ι), a.inj i ≫ u = f i
hv : ∀ (i : ι'), b.inj i ≫ v = g i
he₁ :
  ∀ (i : ι) (j : ι'),
    Eq (α :=
      Cone.pt (F := cospan (X := X (i, j).1) (Y := Y (i, j).2) (f (i, j).1) (g (i, j).2)) (s (i, j).1 (i, j).2) ⟶ a.pt)
      (d.inj (i, j) ≫ e.hom ≫ t.fst) (PullbackCone.fst (s (i, j).1 (i, j).2) ≫ a.inj (i, j).1)
he₂ :
  ∀ (i : ι) (j : ι'),
    Eq (α :=
      Cone.pt (F := cospan (X := X (i, j).1) (Y := Y (i, j).2) (f (i, j).1) (g (i, j).2)) (s (i, j).1 (i, j).2) ⟶ b.pt)
      (d.inj (i, j) ≫ e.hom ≫ t.snd) (PullbackCone.snd (s (i, j).1 (i, j).2) ≫ b.inj (i, j).2)
i : ι
j : ι'
⊢ (s i j).fst ≫ f i = ((s i j).snd ≫ b.inj j) ≫ v

Tactic:
simp [hv, (s i j).condition]

Premises used: CategoryTheory.Limits.PullbackCone.condition
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type u_3
ι' : Type u_4
S : C
X : ι → C
a : Cofan.{u_3, v, u} X
hau : IsUniversalColimit a
Y : ι' → C
b : Cofan.{u_4, v, u} Y
hbu : IsUniversalColimit b
f : (i : ι) → X i ⟶ S
g : (i : ι') → Y i ⟶ S
u : a.pt ⟶ S
v : b.pt ⟶ S
inst_1 : ∀ (i : ι), HasPullback (f i) v
s : (i : ι) → (j : ι') → PullbackCone (f i) (g j)
hs : (i : ι) → (j : ι') → IsLimit (s i j)
t : PullbackCone u v
ht : IsLimit t
d : Cofan (C := C) fun (p : ι × ι') ↦ Cone.pt (F := cospan (X := X p.1) (Y := Y p.2) (f p.1) (g p.2)) (s p.1 p.2)
e : d.pt ≅ t.pt
hu : ∀ (i : ι), a.inj i ≫ u = f i
hv : ∀ (i : ι'), b.inj i ≫ v = g i
he₁ :
  ∀ (i : ι) (j : ι'),
    Eq (α :=
      Cone.pt (F := cospan (X := X (i, j).1) (Y := Y (i, j).2) (f (i, j).1) (g (i, j).2)) (s (i, j).1 (i, j).2) ⟶ a.pt)
      (d.inj (i, j) ≫ e.hom ≫ t.fst) (PullbackCone.fst (s (i, j).1 (i, j).2) ≫ a.inj (i, j).1)
he₂ :
  ∀ (i : ι) (j : ι'),
    Eq (α :=
      Cone.pt (F := cospan (X := X (i, j).1) (Y := Y (i, j).2) (f (i, j).1) (g (i, j).2)) (s (i, j).1 (i, j).2) ⟶ b.pt)
      (d.inj (i, j) ≫ e.hom ≫ t.snd) (PullbackCone.snd (s (i, j).1 (i, j).2) ≫ b.inj (i, j).2)
c : (i : ι) → Cofan.{u_4, v, u} (C := C) fun (j : ι') ↦ (s i j).pt :=
  fun (i : ι) ↦ Cofan.mk (pullback (f i) v) fun (j : ι') ↦ pullback.lift (s i j).fst ((s i j).snd ≫ b.inj j) ⋯
i : ι
⊢ Eq (α := (c i).pt ⟶ S) ((pullback.fst (f i) v ≫ a.inj i) ≫ u) (pullback.snd (f i) v ≫ v)

Tactic:
simp [hu, pullback.condition]

Premises used: CategoryTheory.Limits.pullback.condition
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type u_3
ι' : Type u_4
S : C
X : ι → C
a : Cofan.{u_3, v, u} X
hau : IsUniversalColimit a
Y : ι' → C
b : Cofan.{u_4, v, u} Y
hbu : IsUniversalColimit b
f : (i : ι) → X i ⟶ S
g : (i : ι') → Y i ⟶ S
u : a.pt ⟶ S
v : b.pt ⟶ S
inst_1 : ∀ (i : ι), HasPullback (f i) v
s : (i : ι) → (j : ι') → PullbackCone (f i) (g j)
hs : (i : ι) → (j : ι') → IsLimit (s i j)
t : PullbackCone u v
ht : IsLimit t
d : Cofan (C := C) fun (p : ι × ι') ↦ Cone.pt (F := cospan (X := X p.1) (Y := Y p.2) (f p.1) (g p.2)) (s p.1 p.2)
e : d.pt ≅ t.pt
hu : ∀ (i : ι), a.inj i ≫ u = f i
hv : ∀ (i : ι'), b.inj i ≫ v = g i
he₁ :
  ∀ (i : ι) (j : ι'),
    Eq (α :=
      Cone.pt (F := cospan (X := X (i, j).1) (Y := Y (i, j).2) (f (i, j).1) (g (i, j).2)) (s (i, j).1 (i, j).2) ⟶ a.pt)
      (d.inj (i, j) ≫ e.hom ≫ t.fst) (PullbackCone.fst (s (i, j).1 (i, j).2) ≫ a.inj (i, j).1)
he₂ :
  ∀ (i : ι) (j : ι'),
    Eq (α :=
      Cone.pt (F := cospan (X := X (i, j).1) (Y := Y (i, j).2) (f (i, j).1) (g (i, j).2)) (s (i, j).1 (i, j).2) ⟶ b.pt)
      (d.inj (i, j) ≫ e.hom ≫ t.snd) (PullbackCone.snd (s (i, j).1 (i, j).2) ≫ b.inj (i, j).2)
c : (i : ι) → Cofan.{u_4, v, u} (C := C) fun (j : ι') ↦ (s i j).pt :=
  fun (i : ι) ↦ Cofan.mk (pullback (f i) v) fun (j : ι') ↦ pullback.lift (s i j).fst ((s i j).snd ≫ b.inj j) ⋯
c' : Cofan.{u_3, v, u} (C := C) fun (i : ι) ↦ (c i).pt :=
  Cofan.mk t.pt fun (i : ι) ↦ PullbackCone.IsLimit.lift ht (pullback.fst (f i) v ≫ a.inj i) (pullback.snd (f i) v) ⋯
refine_1 :
  ∀ (p : ι × ι'),
    (d.inj p ≫ e.hom) ≫ t.fst =
      Cofan.inj (f := fun (p : ι × ι') ↦ Cone.pt (F := cospan (X := X p.1) (Y := Y p.2) (f p.1) (g p.2)) (s p.1 p.2))
          (Cofan.mk c'.pt fun (p : ι × ι') ↦
            Cofan.inj (f := fun (j : ι') ↦ Cone.pt (F := cospan (X := X p.1) (f p.1) (g j)) (s p.1 j)) (c p.1) p.2 ≫
              c'.inj p.1)
          p ≫
        t.fst
refine_2 :
  ∀ (p : ι × ι'),
    (d.inj p ≫ e.hom) ≫ t.snd =
      Cofan.inj (f := fun (p : ι × ι') ↦ Cone.pt (F := cospan (X := X p.1) (Y := Y p.2) (f p.1) (g p.2)) (s p.1 p.2))
          (Cofan.mk c'.pt fun (p : ι × ι') ↦
            Cofan.inj (f := fun (j : ι') ↦ Cone.pt (F := cospan (X := X p.1) (f p.1) (g j)) (s p.1 j)) (c p.1) p.2 ≫
              c'.inj p.1)
          p ≫
        t.snd
⊢ d ≅
    Cofan.mk c'.pt fun (p : ι × ι') ↦
      Cofan.inj (f := fun (j : ι') ↦ Cone.pt (F := cospan (X := X p.1) (f p.1) (g j)) (s p.1 j)) (c p.1) p.2 ≫
        c'.inj p.1

Tactic:
refine Cofan.ext e <| fun p ↦ PullbackCone.IsLimit.hom_ext ht ?_ ?_

Premises used: CategoryTheory.Limits.PullbackCone.IsLimit.hom_ext, CategoryTheory.Limits.Cofan.ext
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type u_3
ι' : Type u_4
S : C
X : ι → C
a : Cofan.{u_3, v, u} X
hau : IsUniversalColimit a
Y : ι' → C
b : Cofan.{u_4, v, u} Y
hbu : IsUniversalColimit b
f : (i : ι) → X i ⟶ S
g : (i : ι') → Y i ⟶ S
u : a.pt ⟶ S
v : b.pt ⟶ S
inst_1 : ∀ (i : ι), HasPullback (f i) v
s : (i : ι) → (j : ι') → PullbackCone (f i) (g j)
hs : (i : ι) → (j : ι') → IsLimit (s i j)
t : PullbackCone u v
ht : IsLimit t
d : Cofan (C := C) fun (p : ι × ι') ↦ Cone.pt (F := cospan (X := X p.1) (Y := Y p.2) (f p.1) (g p.2)) (s p.1 p.2)
e : d.pt ≅ t.pt
hu : ∀ (i : ι), a.inj i ≫ u = f i
hv : ∀ (i : ι'), b.inj i ≫ v = g i
he₁ :
  ∀ (i : ι) (j : ι'),
    Eq (α :=
      Cone.pt (F := cospan (X := X (i, j).1) (Y := Y (i, j).2) (f (i, j).1) (g (i, j).2)) (s (i, j).1 (i, j).2) ⟶ a.pt)
      (d.inj (i, j) ≫ e.hom ≫ t.fst) (PullbackCone.fst (s (i, j).1 (i, j).2) ≫ a.inj (i, j).1)
he₂ :
  ∀ (i : ι) (j : ι'),
    Eq (α :=
      Cone.pt (F := cospan (X := X (i, j).1) (Y := Y (i, j).2) (f (i, j).1) (g (i, j).2)) (s (i, j).1 (i, j).2) ⟶ b.pt)
      (d.inj (i, j) ≫ e.hom ≫ t.snd) (PullbackCone.snd (s (i, j).1 (i, j).2) ≫ b.inj (i, j).2)
c : (i : ι) → Cofan.{u_4, v, u} (C := C) fun (j : ι') ↦ (s i j).pt :=
  fun (i : ι) ↦ Cofan.mk (pullback (f i) v) fun (j : ι') ↦ pullback.lift (s i j).fst ((s i j).snd ≫ b.inj j) ⋯
c' : Cofan.{u_3, v, u} (C := C) fun (i : ι) ↦ (c i).pt :=
  Cofan.mk t.pt fun (i : ι) ↦ PullbackCone.IsLimit.lift ht (pullback.fst (f i) v ≫ a.inj i) (pullback.snd (f i) v) ⋯
p : ι × ι'
⊢ (d.inj p ≫ e.hom) ≫ t.fst =
    Cofan.inj (f := fun (p : ι × ι') ↦ Cone.pt (F := cospan (X := X p.1) (Y := Y p.2) (f p.1) (g p.2)) (s p.1 p.2))
        (Cofan.mk c'.pt fun (p : ι × ι') ↦
          Cofan.inj (f := fun (j : ι') ↦ Cone.pt (F := cospan (X := X p.1) (f p.1) (g j)) (s p.1 j)) (c p.1) p.2 ≫
            c'.inj p.1)
        p ≫
      t.fst

Tactic:
simp [c', c, he₁]
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type u_3
ι' : Type u_4
S : C
X : ι → C
a : Cofan.{u_3, v, u} X
hau : IsUniversalColimit a
Y : ι' → C
b : Cofan.{u_4, v, u} Y
hbu : IsUniversalColimit b
f : (i : ι) → X i ⟶ S
g : (i : ι') → Y i ⟶ S
u : a.pt ⟶ S
v : b.pt ⟶ S
inst_1 : ∀ (i : ι), HasPullback (f i) v
s : (i : ι) → (j : ι') → PullbackCone (f i) (g j)
hs : (i : ι) → (j : ι') → IsLimit (s i j)
t : PullbackCone u v
ht : IsLimit t
d : Cofan (C := C) fun (p : ι × ι') ↦ Cone.pt (F := cospan (X := X p.1) (Y := Y p.2) (f p.1) (g p.2)) (s p.1 p.2)
e : d.pt ≅ t.pt
hu : ∀ (i : ι), a.inj i ≫ u = f i
hv : ∀ (i : ι'), b.inj i ≫ v = g i
he₁ :
  ∀ (i : ι) (j : ι'),
    Eq (α :=
      Cone.pt (F := cospan (X := X (i, j).1) (Y := Y (i, j).2) (f (i, j).1) (g (i, j).2)) (s (i, j).1 (i, j).2) ⟶ a.pt)
      (d.inj (i, j) ≫ e.hom ≫ t.fst) (PullbackCone.fst (s (i, j).1 (i, j).2) ≫ a.inj (i, j).1)
he₂ :
  ∀ (i : ι) (j : ι'),
    Eq (α :=
      Cone.pt (F := cospan (X := X (i, j).1) (Y := Y (i, j).2) (f (i, j).1) (g (i, j).2)) (s (i, j).1 (i, j).2) ⟶ b.pt)
      (d.inj (i, j) ≫ e.hom ≫ t.snd) (PullbackCone.snd (s (i, j).1 (i, j).2) ≫ b.inj (i, j).2)
c : (i : ι) → Cofan.{u_4, v, u} (C := C) fun (j : ι') ↦ (s i j).pt :=
  fun (i : ι) ↦ Cofan.mk (pullback (f i) v) fun (j : ι') ↦ pullback.lift (s i j).fst ((s i j).snd ≫ b.inj j) ⋯
c' : Cofan.{u_3, v, u} (C := C) fun (i : ι) ↦ (c i).pt :=
  Cofan.mk t.pt fun (i : ι) ↦ PullbackCone.IsLimit.lift ht (pullback.fst (f i) v ≫ a.inj i) (pullback.snd (f i) v) ⋯
p : ι × ι'
⊢ (d.inj p ≫ e.hom) ≫ t.snd =
    Cofan.inj (f := fun (p : ι × ι') ↦ Cone.pt (F := cospan (X := X p.1) (Y := Y p.2) (f p.1) (g p.2)) (s p.1 p.2))
        (Cofan.mk c'.pt fun (p : ι × ι') ↦
          Cofan.inj (f := fun (j : ι') ↦ Cone.pt (F := cospan (X := X p.1) (f p.1) (g j)) (s p.1 j)) (c p.1) p.2 ≫
            c'.inj p.1)
        p ≫
      t.snd

Tactic:
simp [c', c, he₂]
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type u_3
ι' : Type u_4
S : C
X : ι → C
a : Cofan.{u_3, v, u} X
hau : IsUniversalColimit a
Y : ι' → C
b : Cofan.{u_4, v, u} Y
hbu : IsUniversalColimit b
f : (i : ι) → X i ⟶ S
g : (i : ι') → Y i ⟶ S
u : a.pt ⟶ S
v : b.pt ⟶ S
inst_1 : ∀ (i : ι), HasPullback (f i) v
s : (i : ι) → (j : ι') → PullbackCone (f i) (g j)
hs : (i : ι) → (j : ι') → IsLimit (s i j)
t : PullbackCone u v
ht : IsLimit t
d : Cofan (C := C) fun (p : ι × ι') ↦ Cone.pt (F := cospan (X := X p.1) (Y := Y p.2) (f p.1) (g p.2)) (s p.1 p.2)
e : d.pt ≅ t.pt
hu : ∀ (i : ι), a.inj i ≫ u = f i
hv : ∀ (i : ι'), b.inj i ≫ v = g i
he₁ :
  ∀ (i : ι) (j : ι'),
    Eq (α :=
      Cone.pt (F := cospan (X := X (i, j).1) (Y := Y (i, j).2) (f (i, j).1) (g (i, j).2)) (s (i, j).1 (i, j).2) ⟶ a.pt)
      (d.inj (i, j) ≫ e.hom ≫ t.fst) (PullbackCone.fst (s (i, j).1 (i, j).2) ≫ a.inj (i, j).1)
he₂ :
  ∀ (i : ι) (j : ι'),
    Eq (α :=
      Cone.pt (F := cospan (X := X (i, j).1) (Y := Y (i, j).2) (f (i, j).1) (g (i, j).2)) (s (i, j).1 (i, j).2) ⟶ b.pt)
      (d.inj (i, j) ≫ e.hom ≫ t.snd) (PullbackCone.snd (s (i, j).1 (i, j).2) ≫ b.inj (i, j).2)
c : (i : ι) → Cofan.{u_4, v, u} (C := C) fun (j : ι') ↦ (s i j).pt :=
  fun (i : ι) ↦ Cofan.mk (pullback (f i) v) fun (j : ι') ↦ pullback.lift (s i j).fst ((s i j).snd ≫ b.inj j) ⋯
c' : Cofan.{u_3, v, u} (C := C) fun (i : ι) ↦ (c i).pt :=
  Cofan.mk t.pt fun (i : ι) ↦ PullbackCone.IsLimit.lift ht (pullback.fst (f i) v ≫ a.inj i) (pullback.snd (f i) v) ⋯
iso : d ≅
  Cofan.mk c'.pt fun (p : ι × ι') ↦
    Cofan.inj (f := fun (j : ι') ↦ Cone.pt (F := cospan (X := X p.1) (f p.1) (g j)) (s p.1 j)) (c p.1) p.2 ≫
      c'.inj p.1 :=
  Cofan.ext e ⋯
rw :
  Nonempty
    (IsColimit (J := Discrete (ι × ι')) (F :=
      Discrete.functor fun (p : ι × ι') ↦ Cone.pt (F := cospan (X := X p.1) (Y := Y p.2) (f p.1) (g p.2)) (s p.1 p.2))
      (Cofan.mk c'.pt fun (p : ι × ι') ↦
        Cofan.inj (f := fun (j : ι') ↦ Cone.pt (F := cospan (X := X p.1) (f p.1) (g j)) (s p.1 j)) (c p.1) p.2 ≫
          c'.inj p.1))
⊢ Nonempty (IsColimit d)

Tactic:
rw [(IsColimit.equivIsoColimit iso).nonempty_congr]

Premises used: CategoryTheory.Limits.IsColimit.equivIsoColimit, Equiv.nonempty_congr