awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 ⋯
⊢ 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))

Tactic:
⟨Cofan.IsColimit.prod c (fun i ↦ Nonempty.some ?_) c' (Nonempty.some ?_)⟩

Premises used: Nonempty.some, Nonempty.intro, CategoryTheory.Limits.Cofan.IsColimit.prod
-- 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 ⋯
refine_1 : ∀ (i : ι), Nonempty (IsColimit (c i))
refine_2 : Nonempty (IsColimit c')
⊢ 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))

Tactic:
refine ⟨Cofan.IsColimit.prod c (fun i ↦ Nonempty.some ?_) c' (Nonempty.some ?_)⟩
-- 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 ⋯
i : ι
⊢ Nonempty (IsColimit (c i))

Tactic:
hbu.nonempty_isColimit_of_pullbackCone_left _ v _ _ (hs i) (pullback.cone _ _)
      (pullback.isLimit _ _) _ (Iso.refl _)

Premises used: CategoryTheory.Iso.refl, CategoryTheory.Limits.pullback.isLimit, CategoryTheory.IsUniversalColimit.nonempty_isColimit_of_pullbackCone_left, CategoryTheory.Limits.pullback.cone
-- 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 ⋯
i : ι
⊢ Nonempty (IsColimit (c i))

Tactic:
exact hbu.nonempty_isColimit_of_pullbackCone_left _ v _ _ (hs i) (pullback.cone _ _)
      (pullback.isLimit _ _) _ (Iso.refl _)

Premises used: CategoryTheory.Limits.pullback.isLimit, CategoryTheory.IsUniversalColimit.nonempty_isColimit_of_pullbackCone_left, CategoryTheory.Limits.pullback.cone
-- 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 ⋯
⊢ Nonempty (IsColimit c')

Tactic:
hau.nonempty_isColimit_of_pullbackCone_right _ u _ _ (fun _ ↦ pullback.isLimit _ _)
      t ht _ (Iso.refl _)

Premises used: CategoryTheory.Iso.refl, CategoryTheory.Limits.pullback.isLimit, CategoryTheory.Limits.limit, CategoryTheory.IsUniversalColimit.nonempty_isColimit_of_pullbackCone_right
-- 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 ⋯
⊢ Nonempty (IsColimit c')

Tactic:
exact hau.nonempty_isColimit_of_pullbackCone_right _ u _ _ (fun _ ↦ pullback.isLimit _ _)
      t ht _ (Iso.refl _)

Premises used: CategoryTheory.Limits.pullback.isLimit, CategoryTheory.IsUniversalColimit.nonempty_isColimit_of_pullbackCone_right
-- 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
P : ι × ι' → C
q₁ : (i : ι) → (j : ι') → P (i, j) ⟶ X i
q₂ : (i : ι) → (j : ι') → P (i, j) ⟶ Y j
hP : ∀ (i : ι) (j : ι'), IsPullback (q₁ i j) (q₂ i j) (f i) (g j)
Z : C
p₁ : Z ⟶ a.pt
p₂ : Z ⟶ b.pt
h : IsPullback p₁ p₂ u v
d : Cofan P
e : d.pt ≅ Z
hu : ∀ (i : ι), a.inj i ≫ u = f i
hv : ∀ (i : ι'), b.inj i ≫ v = g i
he₁ : ∀ (i : ι) (j : ι'), d.inj (i, j) ≫ e.hom ≫ p₁ = q₁ i j ≫ a.inj i
he₂ : ∀ (i : ι) (j : ι'), d.inj (i, j) ≫ e.hom ≫ p₂ = q₂ i j ≫ b.inj j
⊢ Nonempty (IsColimit d)

Tactic:
IsUniversalColimit.nonempty_isColimit_prod_of_pullbackCone hau hbu f g u v
    (fun i j ↦ (hP i j).cone) (fun i j ↦ (hP i j).isLimit) h.cone h.isLimit e

Premises used: CategoryTheory.IsUniversalColimit.nonempty_isColimit_prod_of_pullbackCone, CategoryTheory.IsPullback.cone, CategoryTheory.IsPullback.isLimit
-- 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
inst_2 : HasPullback u v
P : ι × ι' → C
q₁ : (i : ι) → (j : ι') → P (i, j) ⟶ X i
q₂ : (i : ι) → (j : ι') → P (i, j) ⟶ Y j
hP : ∀ (i : ι) (j : ι'), IsPullback (q₁ i j) (q₂ i j) (f i) (g j)
d : Cofan P
hd : IsColimit d
hu : ∀ (i : ι), a.inj i ≫ u = f i
hv : ∀ (i : ι'), b.inj i ≫ v = g i
p : ι × ι'
⊢ Eq (α := P p ⟶ S) ((q₁ p.1 p.2 ≫ a.inj p.1) ≫ u) ((q₂ p.1 p.2 ≫ b.inj p.2) ≫ v)

Tactic:
simp [(hP p.1 p.2).w, hu, hv]

Premises used: Prod.fst, CategoryTheory.IsPullback.toCommSq, CategoryTheory.CommSq.w, Prod.snd
-- 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
inst_2 : HasPullback u v
P : ι × ι' → C
q₁ : (i : ι) → (j : ι') → P (i, j) ⟶ X i
q₂ : (i : ι) → (j : ι') → P (i, j) ⟶ Y j
hP : ∀ (i : ι) (j : ι'), IsPullback (q₁ i j) (q₂ i j) (f i) (g j)
d : Cofan P
hd : IsColimit d
hu : ∀ (i : ι), a.inj i ≫ u = f i
hv : ∀ (i : ι'), b.inj i ≫ v = g i
c : Cofan P :=
  Cofan.mk (pullback u v) fun (p : ι × ι') ↦ pullback.lift (q₁ p.1 p.2 ≫ a.inj p.1) (q₂ p.1 p.2 ≫ b.inj p.2) ⋯
obtain :
  ∀ (hc : IsColimit c),
    IsPullback (Cofan.IsColimit.desc hd fun (p : ι × ι') ↦ q₁ p.1 p.2 ≫ a.inj p.1)
      (Cofan.IsColimit.desc hd fun (p : ι × ι') ↦ q₂ p.1 p.2 ≫ b.inj p.2) u v
⊢ IsPullback (Cofan.IsColimit.desc hd fun (p : ι × ι') ↦ q₁ p.1 p.2 ≫ a.inj p.1)
    (Cofan.IsColimit.desc hd fun (p : ι × ι') ↦ q₂ p.1 p.2 ≫ b.inj p.2) u v

Tactic:
obtain ⟨hc⟩ := hau.nonempty_isColimit_prod_of_isPullback hbu f g u
    v hP (IsPullback.of_hasPullback _ _) (d := c) (Iso.refl _)

Premises used: CategoryTheory.IsUniversalColimit.nonempty_isColimit_prod_of_isPullback, CategoryTheory.Iso.refl, CategoryTheory.IsPullback.of_hasPullback
-- 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
inst_2 : HasPullback u v
P : ι × ι' → C
q₁ : (i : ι) → (j : ι') → P (i, j) ⟶ X i
q₂ : (i : ι) → (j : ι') → P (i, j) ⟶ Y j
hP : ∀ (i : ι) (j : ι'), IsPullback (q₁ i j) (q₂ i j) (f i) (g j)
d : Cofan P
hd : IsColimit d
hu : ∀ (i : ι), a.inj i ≫ u = f i
hv : ∀ (i : ι'), b.inj i ≫ v = g i
c : Cofan P :=
  Cofan.mk (pullback u v) fun (p : ι × ι') ↦ pullback.lift (q₁ p.1 p.2 ≫ a.inj p.1) (q₂ p.1 p.2 ≫ b.inj p.2) ⋯
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
ι' : 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
inst_2 : HasPullback u v
P : ι × ι' → C
q₁ : (i : ι) → (j : ι') → P (i, j) ⟶ X i
q₂ : (i : ι) → (j : ι') → P (i, j) ⟶ Y j
hP : ∀ (i : ι) (j : ι'), IsPullback (q₁ i j) (q₂ i j) (f i) (g j)
d : Cofan P
hd : IsColimit d
hu : ∀ (i : ι), a.inj i ≫ u = f i
hv : ∀ (i : ι'), b.inj i ≫ v = g i
c : Cofan P :=
  Cofan.mk (pullback u v) fun (p : ι × ι') ↦ pullback.lift (q₁ p.1 p.2 ≫ a.inj p.1) (q₂ p.1 p.2 ≫ b.inj p.2) ⋯
hc : IsColimit c
⊢ v ≫ Iso.hom (Iso.refl S) = Iso.hom (Iso.refl b.pt) ≫ v

Tactic:
simp
-- 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
inst_2 : HasPullback u v
P : ι × ι' → C
q₁ : (i : ι) → (j : ι') → P (i, j) ⟶ X i
q₂ : (i : ι) → (j : ι') → P (i, j) ⟶ Y j
hP : ∀ (i : ι) (j : ι'), IsPullback (q₁ i j) (q₂ i j) (f i) (g j)
d : Cofan P
hd : IsColimit d
hu : ∀ (i : ι), a.inj i ≫ u = f i
hv : ∀ (i : ι'), b.inj i ≫ v = g i
c : Cofan P :=
  Cofan.mk (pullback u v) fun (p : ι × ι') ↦ pullback.lift (q₁ p.1 p.2 ≫ a.inj p.1) (q₂ p.1 p.2 ≫ b.inj p.2) ⋯
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 (p : ι × ι') ↦ q₁ p.1 p.2 ≫ a.inj p.1
refine_3 :
  pullback.snd u v ≫ Iso.hom (Iso.refl b.pt) =
    (hc.coconePointUniqueUpToIso hd).hom ≫ Cofan.IsColimit.desc hd fun (p : ι × ι') ↦ q₂ p.1 p.2 ≫ b.inj p.2
⊢ IsPullback (Cofan.IsColimit.desc hd fun (p : ι × ι') ↦ q₁ p.1 p.2 ≫ a.inj p.1)
    (Cofan.IsColimit.desc hd fun (p : ι × ι') ↦ q₂ p.1 p.2 ≫ b.inj p.2) 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
ι' : 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
inst_2 : HasPullback u v
P : ι × ι' → C
q₁ : (i : ι) → (j : ι') → P (i, j) ⟶ X i
q₂ : (i : ι) → (j : ι') → P (i, j) ⟶ Y j
hP : ∀ (i : ι) (j : ι'), IsPullback (q₁ i j) (q₂ i j) (f i) (g j)
d : Cofan P
hd : IsColimit d
hu : ∀ (i : ι), a.inj i ≫ u = f i
hv : ∀ (i : ι'), b.inj i ≫ v = g i
c : Cofan P :=
  Cofan.mk (pullback u v) fun (p : ι × ι') ↦ pullback.lift (q₁ p.1 p.2 ≫ a.inj p.1) (q₂ p.1 p.2 ≫ b.inj p.2) ⋯
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
ι' : 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
inst_2 : HasPullback u v
P : ι × ι' → C
q₁ : (i : ι) → (j : ι') → P (i, j) ⟶ X i
q₂ : (i : ι) → (j : ι') → P (i, j) ⟶ Y j
hP : ∀ (i : ι) (j : ι'), IsPullback (q₁ i j) (q₂ i j) (f i) (g j)
d : Cofan P
hd : IsColimit d
hu : ∀ (i : ι), a.inj i ≫ u = f i
hv : ∀ (i : ι'), b.inj i ≫ v = g i
c : Cofan P :=
  Cofan.mk (pullback u v) fun (p : ι × ι') ↦ pullback.lift (q₁ p.1 p.2 ≫ a.inj p.1) (q₂ p.1 p.2 ≫ b.inj p.2) ⋯
hc : IsColimit c
⊢ pullback.fst u v ≫ Iso.hom (Iso.refl a.pt) =
    (hc.coconePointUniqueUpToIso hd).hom ≫ Cofan.IsColimit.desc hd fun (p : ι × ι') ↦ q₁ p.1 p.2 ≫ a.inj p.1

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
ι' : 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
inst_2 : HasPullback u v
P : ι × ι' → C
q₁ : (i : ι) → (j : ι') → P (i, j) ⟶ X i
q₂ : (i : ι) → (j : ι') → P (i, j) ⟶ Y j
hP : ∀ (i : ι) (j : ι'), IsPullback (q₁ i j) (q₂ i j) (f i) (g j)
d : Cofan P
hd : IsColimit d
hu : ∀ (i : ι), a.inj i ≫ u = f i
hv : ∀ (i : ι'), b.inj i ≫ v = g i
c : Cofan P :=
  Cofan.mk (pullback u v) fun (p : ι × ι') ↦ pullback.lift (q₁ p.1 p.2 ≫ a.inj p.1) (q₂ p.1 p.2 ≫ b.inj p.2) ⋯
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 (p : ι × ι') ↦ q₁ p.1 p.2 ≫ a.inj p.1
⊢ pullback.fst u v ≫ Iso.hom (Iso.refl a.pt) =
    (hc.coconePointUniqueUpToIso hd).hom ≫ Cofan.IsColimit.desc hd fun (p : ι × ι') ↦ q₁ p.1 p.2 ≫ a.inj p.1

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
ι' : 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
inst_2 : HasPullback u v
P : ι × ι' → C
q₁ : (i : ι) → (j : ι') → P (i, j) ⟶ X i
q₂ : (i : ι) → (j : ι') → P (i, j) ⟶ Y j
hP : ∀ (i : ι) (j : ι'), IsPullback (q₁ i j) (q₂ i j) (f i) (g j)
d : Cofan P
hd : IsColimit d
hu : ∀ (i : ι), a.inj i ≫ u = f i
hv : ∀ (i : ι'), b.inj i ≫ v = g i
c : Cofan P :=
  Cofan.mk (pullback u v) fun (p : ι × ι') ↦ pullback.lift (q₁ p.1 p.2 ≫ a.inj p.1) (q₂ p.1 p.2 ≫ b.inj p.2) ⋯
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 (p : ι × ι') ↦ q₁ p.1 p.2 ≫ a.inj p.1

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