awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasInitial.{v, u} C
ι : Type u_3
F : Functor.{u_3, v, u_3, u} (Discrete ι) C
c : Cocone F
hc : IsVanKampenColimit c
i_1 : Discrete ι
f : ι → C := F.obj ∘ Discrete.mk
i : ι
⊢ HEq
    (F.map
      { down := { down := ⋯ : PLift ({ as := i : Discrete ι }.as = { as := i : Discrete ι }.as) } :
        ULift.{u_3, 0} (PLift ({ as := i : Discrete ι }.as = { as := i : Discrete ι }.as)) })
    (β :=
    obj.{u_3, v, u_3, u} (Discrete.functor f) { as := i : Discrete ι } ⟶
      obj.{u_3, v, u_3, u} (Discrete.functor f) { as := i : Discrete ι })
    (map (Discrete.functor f) { down := { down := ⋯ } })

Tactic:
simp [f]
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasInitial.{v, u} C
ι : Type u_3
F : Functor.{u_3, v, u_3, u} (Discrete ι) C
c : Cocone F
hc : IsVanKampenColimit c
i : Discrete ι
f : ι → C := F.obj ∘ Discrete.mk
⊢ F = Discrete.functor f

Tactic:
have : F = Discrete.functor f :=
    Functor.hext (fun i ↦ rfl) (by rintro ⟨i⟩ ⟨j⟩ ⟨⟨rfl : i = j⟩⟩; simp [f])
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasInitial.{v, u} C
ι : Type u_3
F : Functor.{u_3, v, u_3, u} (Discrete ι) C
c : Cocone F
hc : IsVanKampenColimit c
i : Discrete ι
f : ι → C := F.obj ∘ Discrete.mk
this : F = Discrete.functor f
clear_value : ∀ (f : ι → C) (this : F = Discrete.functor f), Mono (c.ι.app i)
⊢ Mono (c.ι.app i)

Tactic:
clear_value f
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasInitial.{v, u} C
ι : Type u_3
F : Functor.{u_3, v, u_3, u} (Discrete ι) C
c : Cocone F
hc : IsVanKampenColimit c
i : Discrete ι
f : ι → C
this : F = Discrete.functor f
subst : ∀ {c : Cocone.{u_3, v, u_3, u} (Discrete.functor f)} (hc : IsVanKampenColimit c), Mono (c.ι.app i)
⊢ Mono (c.ι.app i)

Tactic:
subst this
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasInitial.{v, u} C
ι : Type u_3
i : Discrete ι
f : ι → C
c : Cocone.{u_3, v, u_3, u} (Discrete.functor f)
hc : IsVanKampenColimit c
⊢ Mono (c.ι.app i)

Tactic:
PullbackCone.mono_of_isLimitMkIdId _ (IsPullback.isLimit ?_)

Premises used: CategoryTheory.Limits.PullbackCone.mono_of_isLimitMkIdId, CategoryTheory.IsPullback.isLimit
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasInitial.{v, u} C
ι : Type u_3
i : Discrete ι
f : ι → C
c : Cocone.{u_3, v, u_3, u} (Discrete.functor f)
hc : IsVanKampenColimit c
refine :
  IsPullback (𝟙 (obj.{u_3, v, u_3, u} (Discrete.functor f) i)) (𝟙 (obj.{u_3, v, u_3, u} (Discrete.functor f) i))
    (c.ι.app i) (c.ι.app i)
⊢ Mono (c.ι.app i)

Tactic:
refine PullbackCone.mono_of_isLimitMkIdId _ (IsPullback.isLimit ?_)

Premises used: CategoryTheory.Limits.PullbackCone.mono_of_isLimitMkIdId, CategoryTheory.IsPullback.isLimit
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasInitial.{v, u} C
ι : Type u_3
i : Discrete ι
f : ι → C
c : Cocone.{u_3, v, u_3, u} (Discrete.functor f)
hc : IsVanKampenColimit c
nth_rw :
  IsPullback (𝟙 (obj.{u_3, v, u_3, u} (Discrete.functor f) i)) (𝟙 (obj.{u_3, v, u_3, u} (Discrete.functor f) i))
    (𝟙 (obj.{u_3, v, u_3, u} (Discrete.functor f) i) ≫ c.ι.app i) (c.ι.app i)
⊢ IsPullback (𝟙 (obj.{u_3, v, u_3, u} (Discrete.functor f) i)) (𝟙 (obj.{u_3, v, u_3, u} (Discrete.functor f) i))
    (c.ι.app i) (c.ι.app i)

Tactic:
nth_rw 1 [← Category.id_comp (c.ι.app i)]

Premises used: CategoryTheory.Limits.Cocone.ι, CategoryTheory.NatTrans.app, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasInitial.{v, u} C
ι : Type u_3
i : Discrete ι
f : ι → C
c : Cocone.{u_3, v, u_3, u} (Discrete.functor f)
hc : IsVanKampenColimit c
⊢ IsPullback (Y := f i.as) (𝟙 (obj.{u_3, v, u_3, u} (Discrete.functor f) i))
    (CategoryStruct.comp (Y := if i.as = i.as then f i.as else initial.{v, u} C) (eqToHom ⋯)
      (if h : i.as = i.as then eqToHom ⋯ else eqToHom ⋯ ≫ initial.to (f i.as)))
    (𝟙 (obj.{u_3, v, u_3, u} (Discrete.functor f) i) ≫ Cofan.inj c i.as) (Cofan.inj c i.as)

Tactic:
IsPullback.paste_vert _ (isPullback_of_cofan_isVanKampen hc i.as i.as)

Premises used: CategoryTheory.isPullback_of_cofan_isVanKampen, CategoryTheory.Discrete.as, CategoryTheory.IsPullback.paste_vert
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasInitial.{v, u} C
ι : Type u_3
i : Discrete ι
f : ι → C
c : Cocone.{u_3, v, u_3, u} (Discrete.functor f)
hc : IsVanKampenColimit c
h :
  obj.{u_3, v, u_3, u} (Discrete.functor f) i = f i.as →
    Eq.{v + 1} (α := obj.{u_3, v, u_3, u} (Discrete.functor f) i ⟶ obj.{u_3, v, u_3, u} (Discrete.functor f) i)
      (𝟙 (obj.{u_3, v, u_3, u} (Discrete.functor f) i))
      (CategoryStruct.comp (Y := if i.as = i.as then f i.as else initial.{v, u} C) (eqToHom ⋯)
        (if h : i.as = i.as then eqToHom ⋯ else eqToHom ⋯ ≫ initial.to (f i.as)))
convert_4 : obj.{u_3, v, u_3, u} (Discrete.functor f) i ⟶ if i.as = i.as then f i.as else initial.{v, u} C
convert_6 :
  IsPullback.{v, u} (Y := if i.as = i.as then f i.as else initial.{v, u} C)
    (𝟙 (obj.{u_3, v, u_3, u} (Discrete.functor f) i)) (eqToHom ⋯) (𝟙 (obj.{u_3, v, u_3, u} (Discrete.functor f) i))
    (if h : i.as = i.as then eqToHom ⋯ else eqToHom ⋯ ≫ initial.to (f i.as))
⊢ IsPullback (𝟙 (obj.{u_3, v, u_3, u} (Discrete.functor f) i)) (𝟙 (obj.{u_3, v, u_3, u} (Discrete.functor f) i))
    (𝟙 (obj.{u_3, v, u_3, u} (Discrete.functor f) i) ≫ c.ι.app i) (c.ι.app i)

Tactic:
convert! IsPullback.paste_vert _ (isPullback_of_cofan_isVanKampen hc i.as i.as)

Premises used: CategoryTheory.isPullback_of_cofan_isVanKampen, CategoryTheory.Discrete.as, CategoryTheory.IsPullback.paste_vert
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasInitial.{v, u} C
ι : Type u_3
i : Discrete ι
f : ι → C
c : Cocone.{u_3, v, u_3, u} (Discrete.functor f)
hc : IsVanKampenColimit c
⊢ obj.{u_3, v, u_3, u} (Discrete.functor f) i ⟶ if i.as = i.as then f i.as else initial.{v, u} C

Tactic:
exact (eqToHom (if_pos rfl).symm)

Premises used: CategoryTheory.eqToHom, if_pos, Eq.symm, rfl
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasInitial.{v, u} C
ι : Type u_3
i : Discrete ι
f : ι → C
c : Cocone.{u_3, v, u_3, u} (Discrete.functor f)
hc : IsVanKampenColimit c
e_5 : obj.{u_3, v, u_3, u} (Discrete.functor f) i = f i.as
⊢ Eq.{v + 1} (α := obj.{u_3, v, u_3, u} (Discrete.functor f) i ⟶ obj.{u_3, v, u_3, u} (Discrete.functor f) i)
    (𝟙 (obj.{u_3, v, u_3, u} (Discrete.functor f) i))
    (CategoryStruct.comp (Y := if i.as = i.as then f i.as else initial.{v, u} C) (eqToHom ⋯)
      (if h : i.as = i.as then eqToHom ⋯ else eqToHom ⋯ ≫ initial.to (f i.as)))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasInitial.{v, u} C
ι : Type u_3
i : Discrete ι
f : ι → C
c : Cocone.{u_3, v, u_3, u} (Discrete.functor f)
hc : IsVanKampenColimit c
⊢ Eq.{v + 1} (α := obj.{u_3, v, u_3, u} (Discrete.functor f) i ⟶ f i.as)
    (𝟙 (obj.{u_3, v, u_3, u} (Discrete.functor f) i) ≫ 𝟙 (obj.{u_3, v, u_3, u} (Discrete.functor f) i))
    (CategoryStruct.comp (Y := if i.as = i.as then f i.as else initial.{v, u} C) (eqToHom ⋯)
      (if h : i.as = i.as then eqToHom ⋯ else eqToHom ⋯ ≫ initial.to (f i.as)))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasInitial.{v, u} C
ι : Type u_3
i : Discrete ι
f : ι → C
c : Cocone.{u_3, v, u_3, u} (Discrete.functor f)
hc : IsVanKampenColimit c
⊢ IsPullback.{v, u} (Y := if i.as = i.as then f i.as else initial.{v, u} C)
    (𝟙 (obj.{u_3, v, u_3, u} (Discrete.functor f) i)) (eqToHom ⋯) (𝟙 (obj.{u_3, v, u_3, u} (Discrete.functor f) i))
    (if h : i.as = i.as then eqToHom ⋯ else eqToHom ⋯ ≫ initial.to (f i.as))

Tactic:
exact IsPullback.of_vert_isIso ⟨by simp⟩

Premises used: CategoryTheory.IsPullback.of_vert_isIso, CategoryTheory.CommSq.mk
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
Goal:
C : Type u
inst : Category.{v, u} C
ι : 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 v (f i)
hs : (i : ι) → IsLimit (s i)
t : PullbackCone v u
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
he₂ : ∀ (i : ι), d.inj i ≫ e.hom ≫ t.snd = (s i).snd ≫ a.inj i
i : ι
⊢ (s i).fst ≫ v = ((s i).snd ≫ a.inj i) ≫ u

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 v (f i)
hs : (i : ι) → IsLimit (s i)
t : PullbackCone v u
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
he₂ : ∀ (i : ι), d.inj i ≫ e.hom ≫ t.snd = (s i).snd ≫ a.inj i
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 ((s i).snd ≫ a.inj i) ⋯) 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 v (f i)
hs : (i : ι) → IsLimit (s i)
t : PullbackCone v u
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
he₂ : ∀ (i : ι), d.inj i ≫ e.hom ≫ t.snd = (s i).snd ≫ a.inj i
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 ((s i).snd ≫ a.inj i) ⋯) 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 v (f i)
hs : (i : ι) → IsLimit (s i)
t : PullbackCone v u
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
he₂ : ∀ (i : ι), d.inj i ≫ e.hom ≫ t.snd = (s i).snd ≫ a.inj i
iso : d ≅ Cofan.mk t.pt fun (i : ι) ↦ PullbackCone.IsLimit.lift ht (s i).fst ((s i).snd ≫ a.inj i) ⋯ := 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 ((s i).snd ≫ a.inj i) ⋯))
⊢ 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 v (f i)
hs : (i : ι) → IsLimit (s i)
t : PullbackCone v u
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
he₂ : ∀ (i : ι), d.inj i ≫ e.hom ≫ t.snd = (s i).snd ≫ a.inj i
iso : d ≅ Cofan.mk t.pt fun (i : ι) ↦ PullbackCone.IsLimit.lift ht (s i).fst ((s i).snd ≫ a.inj i) ⋯ := 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 ((s i).snd ≫ a.inj i) ⋯))

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

Premises used: CategoryTheory.NatTrans.Equifibered.of_discrete, CategoryTheory.Discrete.natTrans, CategoryTheory.Discrete.as, CategoryTheory.Limits.PullbackCone.snd
-- 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 v (f i)
hs : (i : ι) → IsLimit (s i)
t : PullbackCone v u
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
he₂ : ∀ (i : ι), d.inj i ≫ e.hom ≫ t.snd = (s i).snd ≫ a.inj i
iso : d ≅ Cofan.mk t.pt fun (i : ι) ↦ PullbackCone.IsLimit.lift ht (s i).fst ((s i).snd ≫ a.inj i) ⋯ := 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.snd (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 ((s i).snd ≫ a.inj i) ⋯)))
      (Cocone.ι (Cofan.mk t.pt fun (i : ι) ↦ PullbackCone.IsLimit.lift ht (s i).fst ((s i).snd ≫ a.inj i) ⋯))
      (map (const (Discrete ι)) t.snd))
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 ((s i).snd ≫ a.inj i) ⋯)) j)
      (NatTrans.app (Discrete.natTrans fun (i : Discrete ι) ↦ PullbackCone.snd (s i.as)) j) t.snd (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 ((s i).snd ≫ a.inj i) ⋯))

Tactic:
refine hau _ (Discrete.natTrans fun i ↦ (s i.as).snd) t.snd ?_ (.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 v (f i)
hs : (i : ι) → IsLimit (s i)
t : PullbackCone v u
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
he₂ : ∀ (i : ι), d.inj i ≫ e.hom ≫ t.snd = (s i).snd ≫ a.inj i
iso : d ≅ Cofan.mk t.pt fun (i : ι) ↦ PullbackCone.IsLimit.lift ht (s i).fst ((s i).snd ≫ a.inj i) ⋯ := Cofan.ext e ⋯
refine_1 :
  ∀ (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.snd (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 ((s i).snd ≫ a.inj i) ⋯)))
          (Cocone.ι (Cofan.mk t.pt fun (i : ι) ↦ PullbackCone.IsLimit.lift ht (s i).fst ((s i).snd ≫ a.inj i) ⋯))
          (map (const (Discrete ι)) t.snd))
        x)
⊢ 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.snd (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 ((s i).snd ≫ a.inj i) ⋯)))
      (Cocone.ι (Cofan.mk t.pt fun (i : ι) ↦ PullbackCone.IsLimit.lift ht (s i).fst ((s i).snd ≫ a.inj i) ⋯))
      (map (const (Discrete ι)) t.snd))

Tactic:
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
s : (i : ι) → PullbackCone v (f i)
hs : (i : ι) → IsLimit (s i)
t : PullbackCone v u
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
he₂ : ∀ (i : ι), d.inj i ≫ e.hom ≫ t.snd = (s i).snd ≫ a.inj i
iso : d ≅ Cofan.mk t.pt fun (i : ι) ↦ PullbackCone.IsLimit.lift ht (s i).fst ((s i).snd ≫ a.inj i) ⋯ := 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.snd (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 ((s i).snd ≫ a.inj i) ⋯)))
        (Cocone.ι (Cofan.mk t.pt fun (i : ι) ↦ PullbackCone.IsLimit.lift ht (s i).fst ((s i).snd ≫ a.inj i) ⋯))
        (map (const (Discrete ι)) t.snd))
      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 v (f i)
hs : (i : ι) → IsLimit (s i)
t : PullbackCone v u
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
he₂ : ∀ (i : ι), d.inj i ≫ e.hom ≫ t.snd = (s i).snd ≫ a.inj i
iso : d ≅ Cofan.mk t.pt fun (i : ι) ↦ PullbackCone.IsLimit.lift ht (s i).fst ((s i).snd ≫ a.inj i) ⋯ := Cofan.ext e ⋯
j : Discrete ι
refine_2 :
  IsPullback (P := Cone.pt (F := cospan (Y := X j.as) v (f j.as)) (s j.as))
    (PullbackCone.IsLimit.lift ht (PullbackCone.fst (s j.as)) (PullbackCone.snd (s j.as) ≫ a.inj j.as) ⋯)
    (PullbackCone.snd (s j.as)) t.snd (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 ((s i).snd ≫ a.inj i) ⋯)) j)
    (NatTrans.app (Discrete.natTrans fun (i : Discrete ι) ↦ PullbackCone.snd (s i.as)) j) t.snd (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 v (f i)
hs : (i : ι) → IsLimit (s i)
t : PullbackCone v u
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
he₂ : ∀ (i : ι), d.inj i ≫ e.hom ≫ t.snd = (s i).snd ≫ a.inj i
iso : d ≅ Cofan.mk t.pt fun (i : ι) ↦ PullbackCone.IsLimit.lift ht (s i).fst ((s i).snd ≫ a.inj i) ⋯ := Cofan.ext e ⋯
j : Discrete ι
refine_2 :
  IsPullback (P := Cone.pt (F := cospan (Y := X j.as) v (f j.as)) (s j.as))
    (PullbackCone.IsLimit.lift ht (PullbackCone.fst (s j.as)) (PullbackCone.snd (s j.as) ≫ a.inj j.as) ⋯)
    (PullbackCone.snd (s j.as)) t.snd (a.inj j.as)
⊢ IsPullback (P := Cone.pt (F := cospan (Y := X j.as) v (f j.as)) (s j.as))
    (PullbackCone.IsLimit.lift ht (PullbackCone.fst (s j.as)) (PullbackCone.snd (s j.as) ≫ a.inj j.as) ⋯)
    (PullbackCone.snd (s j.as)) t.snd (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 v (f i)
hs : (i : ι) → IsLimit (s i)
t : PullbackCone v u
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
he₂ : ∀ (i : ι), d.inj i ≫ e.hom ≫ t.snd = (s i).snd ≫ a.inj i
iso : d ≅ Cofan.mk t.pt fun (i : ι) ↦ PullbackCone.IsLimit.lift ht (s i).fst ((s i).snd ≫ a.inj i) ⋯ := Cofan.ext e ⋯
j : Discrete ι
⊢ Eq (α := Cone.pt (F := cospan (Y := X j.as) v (f j.as)) (s j.as) ⟶ a.pt)
    (PullbackCone.IsLimit.lift ht (PullbackCone.fst (s j.as)) (PullbackCone.snd (s j.as) ≫ a.inj j.as) ⋯ ≫ t.snd)
    (PullbackCone.snd (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 v (f i)
hs : (i : ι) → IsLimit (s i)
t : PullbackCone v u
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
he₂ : ∀ (i : ι), d.inj i ≫ e.hom ≫ t.snd = (s i).snd ≫ a.inj i
iso : d ≅ Cofan.mk t.pt fun (i : ι) ↦ PullbackCone.IsLimit.lift ht (s i).fst ((s i).snd ≫ a.inj i) ⋯ := Cofan.ext e ⋯
j : Discrete ι
refine_2 :
  IsPullback (P := Cone.pt (F := cospan (Y := X j.as) v (f j.as)) (s j.as))
    (PullbackCone.IsLimit.lift ht (PullbackCone.fst (s j.as)) (PullbackCone.snd (s j.as) ≫ a.inj j.as) ⋯ ≫ t.fst)
    (PullbackCone.snd (s j.as)) v (a.inj j.as ≫ u)
⊢ IsPullback (P := Cone.pt (F := cospan (Y := X j.as) v (f j.as)) (s j.as))
    (PullbackCone.IsLimit.lift ht (PullbackCone.fst (s j.as)) (PullbackCone.snd (s j.as) ≫ a.inj j.as) ⋯)
    (PullbackCone.snd (s j.as)) t.snd (a.inj j.as)

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

Premises used: CategoryTheory.IsPullback.of_isLimit, CategoryTheory.IsPullback.of_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
s : (i : ι) → PullbackCone v (f i)
hs : (i : ι) → IsLimit (s i)
t : PullbackCone v u
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
he₂ : ∀ (i : ι), d.inj i ≫ e.hom ≫ t.snd = (s i).snd ≫ a.inj i
iso : d ≅ Cofan.mk t.pt fun (i : ι) ↦ PullbackCone.IsLimit.lift ht (s i).fst ((s i).snd ≫ a.inj i) ⋯ := Cofan.ext e ⋯
j : Discrete ι
⊢ IsPullback (P := Cone.pt (F := cospan (Y := X j.as) v (f j.as)) (s j.as))
    (PullbackCone.IsLimit.lift ht (PullbackCone.fst (s j.as)) (PullbackCone.snd (s j.as) ≫ a.inj j.as) ⋯ ≫ t.fst)
    (PullbackCone.snd (s j.as)) v (a.inj j.as ≫ u)

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

Premises used: CategoryTheory.IsPullback.of_isLimit, CategoryTheory.Discrete.as