awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (goal)
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 ⋯
refine_1 :
  Eq (α :=
    Quiver.Hom (V := Functor.{u_3, v, u_3, u} (Discrete ι) C) (Discrete.functor fun (i : ι) ↦ (s i).pt)
      (obj (const (Discrete ι)) a.pt))
    ((Discrete.natTrans fun (i : Discrete ι) ↦ PullbackCone.fst (s i.as)) ≫ a.ι)
    (CategoryStruct.comp (Y :=
      obj (const (Discrete ι))
        (Cocone.pt.{u_3, v, u_3, u} (J := Discrete ι) (F := Discrete.functor fun (i : ι) ↦ (s i).pt)
          (Cofan.mk t.pt fun (i : ι) ↦ PullbackCone.IsLimit.lift ht ((s i).fst ≫ a.inj i) (s i).snd ⋯)))
      (Cocone.ι (Cofan.mk t.pt fun (i : ι) ↦ PullbackCone.IsLimit.lift ht ((s i).fst ≫ a.inj i) (s i).snd ⋯))
      (map (const (Discrete ι)) t.fst))
⊢ Nonempty
    (IsColimit.{u_3, v, u_3, u} (J := Discrete ι) (F := Discrete.functor fun (i : ι) ↦ (s i).pt)
      (Cofan.mk t.pt fun (i : ι) ↦ PullbackCone.IsLimit.lift ht ((s i).fst ≫ a.inj i) (s i).snd ⋯))
have refine_2 : ∀ (j : Discrete ι),
  IsPullback (P := obj.{u_3, v, u_3, u} (Discrete.functor fun (i : ι) ↦ (s i).pt) j)
    (NatTrans.app
      (Cocone.ι (Cofan.mk t.pt fun (i : ι) ↦ PullbackCone.IsLimit.lift ht ((s i).fst ≫ a.inj i) (s i).snd sorry)) j)
    (NatTrans.app (Discrete.natTrans fun (i : Discrete ι) ↦ PullbackCone.fst (s i.as)) j) t.fst (a.ι.app j)
Tactic: refine hau _ (Discrete.natTrans fun i ↦ (s i.as).fst) t.fst ?_ (.of_discrete _) fun j ↦ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (goal)
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 := obj.{u_3, v, u_3, u} (Discrete.functor fun (i : ι) ↦ (s i).pt) j)
    (NatTrans.app
      (Cocone.ι (Cofan.mk t.pt fun (i : ι) ↦ PullbackCone.IsLimit.lift ht ((s i).fst ≫ a.inj i) (s i).snd ⋯)) j)
    (NatTrans.app (Discrete.natTrans fun (i : Discrete ι) ↦ PullbackCone.fst (s i.as)) j) t.fst (a.ι.app j)
have refine_2 : 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)) sorry)
  (PullbackCone.fst (s j.as)) t.fst (a.ι.app j)
Tactic: simp only [Discrete.functor_obj_eq_as, Cofan.mk_pt, Functor.const_obj_obj, Cofan.mk_ι_app,
      Discrete.natTrans_app]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (goal)
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)) ⋯)
    (PullbackCone.fst (s j.as)) t.fst (a.ι.app j)
have refine_2 : 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)) sorry)
  (PullbackCone.fst (s j.as)) t.fst (a.inj j.as)
Tactic: rw [← Cofan.inj]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (goal)
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)) ⋯)
    (PullbackCone.fst (s j.as)) t.fst (a.inj j.as)
have refine_2 : 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)) sorry ≫ t.snd)
  (PullbackCone.fst (s j.as)) v (a.inj j.as ≫ u)
Tactic: refine IsPullback.of_right ?_ (by simp) (IsPullback.of_isLimit ht).flip
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (goal)
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) ⋯
⊢ IsPullback (Cofan.IsColimit.desc hd fun (x : ι) ↦ q₁ x ≫ a.inj x) (Cofan.IsColimit.desc hd q₂) u v
have obtain : ∀ (hc : IsColimit c), 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 _)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (goal)
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
⊢ IsPullback (Cofan.IsColimit.desc hd fun (x : ι) ↦ q₁ x ≫ a.inj x) (Cofan.IsColimit.desc hd q₂) u v
have refine_1 : pullback u v ≅ d.pt
Tactic: refine (IsPullback.of_hasPullback u v).of_iso
      ?_ (Iso.refl _) (Iso.refl _) (Iso.refl _) ?_ ?_ (by simp) (by simp)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (goal)
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
⊢ IsPullback (Cofan.IsColimit.desc hd fun (x : ι) ↦ q₁ x ≫ a.inj x) (Cofan.IsColimit.desc hd q₂) u v
have 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
Tactic: refine (IsPullback.of_hasPullback u v).of_iso
      ?_ (Iso.refl _) (Iso.refl _) (Iso.refl _) ?_ ?_ (by simp) (by simp)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (goal)
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
⊢ IsPullback (Cofan.IsColimit.desc hd fun (x : ι) ↦ q₁ x ≫ a.inj x) (Cofan.IsColimit.desc hd q₂) u v
have refine_3 : pullback.snd u v ≫ Iso.hom (Iso.refl B) = (hc.coconePointUniqueUpToIso hd).hom ≫ Cofan.IsColimit.desc hd q₂
Tactic: refine (IsPullback.of_hasPullback u v).of_iso
      ?_ (Iso.refl _) (Iso.refl _) (Iso.refl _) ?_ ?_ (by simp) (by simp)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (goal)
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
have 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
Tactic: refine Cofan.IsColimit.hom_ext hc _ _ fun i ↦ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (goal)
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₂
have 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₂
Tactic: refine Cofan.IsColimit.hom_ext hc _ _ fun i ↦ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (goal)
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) ⋯
⊢ 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
have 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
Tactic: refine Cofan.ext e <| fun p ↦ PullbackCone.IsLimit.hom_ext ht ?_ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (goal)
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
⊢ 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
have 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
Tactic: refine Cofan.ext e <| fun p ↦ PullbackCone.IsLimit.hom_ext ht ?_ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (goal)
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 d)
have 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))
Tactic: rw [(IsColimit.equivIsoColimit iso).nonempty_congr]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (goal)
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))
have refine_1 : ∀ (i : ι), Nonempty (IsColimit (c i))
Tactic: refine ⟨Cofan.IsColimit.prod c (fun i ↦ Nonempty.some ?_) c' (Nonempty.some ?_)⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (goal)
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))
⊢ 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))
have refine_2 : Nonempty (IsColimit c')
Tactic: refine ⟨Cofan.IsColimit.prod c (fun i ↦ Nonempty.some ?_) c' (Nonempty.some ?_)⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (goal)
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) ⋯
⊢ 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
have 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
Tactic: obtain ⟨hc⟩ := hau.nonempty_isColimit_prod_of_isPullback hbu f g u
    v hP (IsPullback.of_hasPullback _ _) (d := c) (Iso.refl _)