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
P : ι → C
q₁ : (i : ι) → P i ⟶ B
q₂ : (i : ι) → P i ⟶ X i
hP : ∀ (i : ι), IsPullback (q₁ i) (q₂ i) v (f i)
Z : C
p₁ : Z ⟶ B
p₂ : Z ⟶ a.pt
h : IsPullback p₁ p₂ v u
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
he₂ : ∀ (i : ι), d.inj i ≫ e.hom ≫ p₂ = q₂ i ≫ a.inj i
⊢ Nonempty (IsColimit d)

Tactic:
hau.nonempty_isColimit_of_pullbackCone_left 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_left, 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 ⟶ B
q₂ : (i : ι) → P i ⟶ X i
hP : ∀ (i : ι), IsPullback (q₁ i) (q₂ i) v (f i)
d : Cofan.{u_3, v, u} P
hd : IsColimit d
hu : ∀ (i : ι), a.inj i ≫ u = f i
inst_1 : HasPullback v u
i : ι
⊢ q₁ i ≫ v = (q₂ i ≫ a.inj i) ≫ u

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 ⟶ B
q₂ : (i : ι) → P i ⟶ X i
hP : ∀ (i : ι), IsPullback (q₁ i) (q₂ i) v (f i)
d : Cofan.{u_3, v, u} P
hd : IsColimit d
hu : ∀ (i : ι), a.inj i ≫ u = f i
inst_1 : HasPullback v u
c : Cofan.{u_3, v, u} P := Cofan.mk (pullback v u) fun (i : ι) ↦ pullback.lift (q₁ i) (q₂ i ≫ a.inj i) ⋯
obtain :
  ∀ (hc : IsColimit c),
    IsPullback (Cofan.IsColimit.desc hd q₁) (Cofan.IsColimit.desc hd fun (x : ι) ↦ q₂ x ≫ a.inj x) v u
⊢ IsPullback (Cofan.IsColimit.desc hd q₁) (Cofan.IsColimit.desc hd fun (x : ι) ↦ q₂ x ≫ a.inj x) v u

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

Premises used: CategoryTheory.IsUniversalColimit.nonempty_isColimit_of_isPullback_left, CategoryTheory.Iso.refl, 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 ⟶ B
q₂ : (i : ι) → P i ⟶ X i
hP : ∀ (i : ι), IsPullback (q₁ i) (q₂ i) v (f i)
d : Cofan.{u_3, v, u} P
hd : IsColimit d
hu : ∀ (i : ι), a.inj i ≫ u = f i
inst_1 : HasPullback v u
c : Cofan.{u_3, v, u} P := Cofan.mk (pullback v u) fun (i : ι) ↦ pullback.lift (q₁ i) (q₂ i ≫ a.inj 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 ⟶ B
q₂ : (i : ι) → P i ⟶ X i
hP : ∀ (i : ι), IsPullback (q₁ i) (q₂ i) v (f i)
d : Cofan.{u_3, v, u} P
hd : IsColimit d
hu : ∀ (i : ι), a.inj i ≫ u = f i
inst_1 : HasPullback v u
c : Cofan.{u_3, v, u} P := Cofan.mk (pullback v u) fun (i : ι) ↦ pullback.lift (q₁ i) (q₂ i ≫ a.inj 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 ⟶ B
q₂ : (i : ι) → P i ⟶ X i
hP : ∀ (i : ι), IsPullback (q₁ i) (q₂ i) v (f i)
d : Cofan.{u_3, v, u} P
hd : IsColimit d
hu : ∀ (i : ι), a.inj i ≫ u = f i
inst_1 : HasPullback v u
c : Cofan.{u_3, v, u} P := Cofan.mk (pullback v u) fun (i : ι) ↦ pullback.lift (q₁ i) (q₂ i ≫ a.inj i) ⋯
hc : IsColimit c
refine_1 : pullback v u ≅ d.pt
refine_2 : pullback.fst v u ≫ Iso.hom (Iso.refl B) = (hc.coconePointUniqueUpToIso hd).hom ≫ Cofan.IsColimit.desc hd q₁
refine_3 :
  pullback.snd v u ≫ 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 q₁) (Cofan.IsColimit.desc hd fun (x : ι) ↦ q₂ x ≫ a.inj x) v u

Tactic:
refine (IsPullback.of_hasPullback v u).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 ⟶ B
q₂ : (i : ι) → P i ⟶ X i
hP : ∀ (i : ι), IsPullback (q₁ i) (q₂ i) v (f i)
d : Cofan.{u_3, v, u} P
hd : IsColimit d
hu : ∀ (i : ι), a.inj i ≫ u = f i
inst_1 : HasPullback v u
c : Cofan.{u_3, v, u} P := Cofan.mk (pullback v u) fun (i : ι) ↦ pullback.lift (q₁ i) (q₂ i ≫ a.inj i) ⋯
hc : IsColimit c
⊢ pullback v u ≅ 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 ⟶ B
q₂ : (i : ι) → P i ⟶ X i
hP : ∀ (i : ι), IsPullback (q₁ i) (q₂ i) v (f i)
d : Cofan.{u_3, v, u} P
hd : IsColimit d
hu : ∀ (i : ι), a.inj i ≫ u = f i
inst_1 : HasPullback v u
c : Cofan.{u_3, v, u} P := Cofan.mk (pullback v u) fun (i : ι) ↦ pullback.lift (q₁ i) (q₂ i ≫ a.inj i) ⋯
hc : IsColimit c
⊢ pullback.fst v u ≫ 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 ⟶ B
q₂ : (i : ι) → P i ⟶ X i
hP : ∀ (i : ι), IsPullback (q₁ i) (q₂ i) v (f i)
d : Cofan.{u_3, v, u} P
hd : IsColimit d
hu : ∀ (i : ι), a.inj i ≫ u = f i
inst_1 : HasPullback v u
c : Cofan.{u_3, v, u} P := Cofan.mk (pullback v u) fun (i : ι) ↦ pullback.lift (q₁ i) (q₂ i ≫ a.inj i) ⋯
hc : IsColimit c
refine_2 :
  ∀ (i : ι),
    c.inj i ≫ pullback.fst v u ≫ Iso.hom (Iso.refl B) =
      c.inj i ≫ (hc.coconePointUniqueUpToIso hd).hom ≫ Cofan.IsColimit.desc hd q₁
⊢ pullback.fst v u ≫ 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 ⟶ B
q₂ : (i : ι) → P i ⟶ X i
hP : ∀ (i : ι), IsPullback (q₁ i) (q₂ i) v (f i)
d : Cofan.{u_3, v, u} P
hd : IsColimit d
hu : ∀ (i : ι), a.inj i ≫ u = f i
inst_1 : HasPullback v u
c : Cofan.{u_3, v, u} P := Cofan.mk (pullback v u) fun (i : ι) ↦ pullback.lift (q₁ i) (q₂ i ≫ a.inj i) ⋯
hc : IsColimit c
i : ι
⊢ c.inj i ≫ pullback.fst v u ≫ 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_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 ⟶ B
q₂ : (i : ι) → P i ⟶ X i
hP : ∀ (i : ι), IsPullback (q₁ i) (q₂ i) v (f i)
d : Cofan.{u_3, v, u} P
hd : IsColimit d
hu : ∀ (i : ι), a.inj i ≫ u = f i
inst_1 : HasPullback v u
c : Cofan.{u_3, v, u} P := Cofan.mk (pullback v u) fun (i : ι) ↦ pullback.lift (q₁ i) (q₂ i ≫ a.inj i) ⋯
hc : IsColimit c
⊢ pullback.snd v u ≫ 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 ⟶ B
q₂ : (i : ι) → P i ⟶ X i
hP : ∀ (i : ι), IsPullback (q₁ i) (q₂ i) v (f i)
d : Cofan.{u_3, v, u} P
hd : IsColimit d
hu : ∀ (i : ι), a.inj i ≫ u = f i
inst_1 : HasPullback v u
c : Cofan.{u_3, v, u} P := Cofan.mk (pullback v u) fun (i : ι) ↦ pullback.lift (q₁ i) (q₂ i ≫ a.inj i) ⋯
hc : IsColimit c
refine_3 :
  ∀ (i : ι),
    c.inj i ≫ pullback.snd v u ≫ 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.snd v u ≫ 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 ⟶ B
q₂ : (i : ι) → P i ⟶ X i
hP : ∀ (i : ι), IsPullback (q₁ i) (q₂ i) v (f i)
d : Cofan.{u_3, v, u} P
hd : IsColimit d
hu : ∀ (i : ι), a.inj i ≫ u = f i
inst_1 : HasPullback v u
c : Cofan.{u_3, v, u} P := Cofan.mk (pullback v u) fun (i : ι) ↦ pullback.lift (q₁ i) (q₂ i ≫ a.inj i) ⋯
hc : IsColimit c
i : ι
⊢ c.inj i ≫ pullback.snd v u ≫ 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_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
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
i : ι
⊢ ((s i).fst ≫ a.inj i) ≫ u = (s i).snd ≫ v

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

Premises used: CategoryTheory.Limits.PullbackCone.condition
-- 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
p : ι
⊢ (d.inj p ≫ e.hom) ≫ t.fst =
    Cofan.inj.{u_3, v, u} (f := fun (i : ι) ↦ (s i).pt)
        (Cofan.mk t.pt fun (i : ι) ↦ PullbackCone.IsLimit.lift ht ((s i).fst ≫ a.inj i) (s i).snd ⋯) p ≫
      t.fst

Tactic:
simp [he₁]
-- 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
p : ι
⊢ (d.inj p ≫ e.hom) ≫ t.snd =
    Cofan.inj.{u_3, v, u} (f := fun (i : ι) ↦ (s i).pt)
        (Cofan.mk t.pt fun (i : ι) ↦ PullbackCone.IsLimit.lift ht ((s i).fst ≫ a.inj i) (s i).snd ⋯) p ≫
      t.snd

Tactic:
simp [he₂]
-- 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 ⋯
rw :
  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 ⋯))
⊢ Nonempty (IsColimit d)

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

Premises used: CategoryTheory.Limits.IsColimit.equivIsoColimit, Equiv.nonempty_congr
-- 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 ⋯
⊢ 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 ⋯))

Tactic:
hau _ (Discrete.natTrans fun i ↦ (s i.as).fst) t.fst ?_ (.of_discrete _) fun j ↦ ?_

Premises used: CategoryTheory.Limits.PullbackCone.fst, CategoryTheory.NatTrans.Equifibered.of_discrete, CategoryTheory.Discrete.natTrans, CategoryTheory.Discrete.as
-- 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 ⋯
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))
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 ⋯)) j)
      (NatTrans.app (Discrete.natTrans fun (i : Discrete ι) ↦ PullbackCone.fst (s i.as)) j) t.fst (a.ι.app j)
⊢ 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 ⋯))

Tactic:
refine hau _ (Discrete.natTrans fun i ↦ (s i.as).fst) t.fst ?_ (.of_discrete _) fun j ↦ ?_

Premises used: CategoryTheory.NatTrans.Equifibered.of_discrete, CategoryTheory.Discrete.natTrans
-- 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 ⋯
x : Discrete ι
⊢ Eq (α :=
    obj.{u_3, v, u_3, u} (Discrete.functor fun (i : ι) ↦ (s i).pt) x ⟶
      obj.{u_3, v, u_3, u} (obj (const (Discrete ι)) a.pt) x)
    (NatTrans.app ((Discrete.natTrans fun (i : Discrete ι) ↦ PullbackCone.fst (s i.as)) ≫ a.ι) x)
    (NatTrans.app
      (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))
      x)

Tactic:
simp [Cofan.inj]

Premises used: CategoryTheory.Limits.Cofan.inj
-- 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 ι
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)) ⋯)
    (PullbackCone.fst (s j.as)) t.fst (a.ι.app j)
⊢ 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)

Tactic:
simp only [Discrete.functor_obj_eq_as, Cofan.mk_pt, Functor.const_obj_obj, Cofan.mk_ι_app,
      Discrete.natTrans_app]

Premises used: CategoryTheory.Limits.Cofan.mk_ι_app, CategoryTheory.Limits.Cofan.mk_pt, CategoryTheory.Discrete.functor_obj_eq_as, CategoryTheory.Functor.const_obj_obj, CategoryTheory.Discrete.natTrans_app
-- 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 ι
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)) ⋯)
    (PullbackCone.fst (s j.as)) t.fst (a.inj j.as)
⊢ 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)

Tactic:
rw [← Cofan.inj]

Premises used: CategoryTheory.Limits.Cofan.inj
-- 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 ι
⊢ Eq (α := Cone.pt (F := cospan (X := X j.as) (f j.as) v) (s j.as) ⟶ a.pt)
    (PullbackCone.IsLimit.lift ht (PullbackCone.fst (s j.as) ≫ a.inj j.as) (PullbackCone.snd (s j.as)) ⋯ ≫ t.fst)
    (PullbackCone.fst (s j.as) ≫ a.inj j.as)

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
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 ι
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)) ⋯ ≫ t.snd)
    (PullbackCone.fst (s j.as)) v (a.inj j.as ≫ u)
⊢ 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)

Tactic:
refine IsPullback.of_right ?_ (by simp) (IsPullback.of_isLimit ht).flip

Premises used: CategoryTheory.IsPullback.of_isLimit, CategoryTheory.IsPullback.flip, CategoryTheory.IsPullback.of_right