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
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 ι
let let₁ let₂ : Mono (c.ι.app i)
let₃ :
  let f := F.obj ∘ Discrete.mk;
  ∀ (this : F = Discrete.functor f), Mono (c.ι.app i)
let₄ : ∀ (f : ι → C) (this : F = Discrete.functor f), Mono (c.ι.app i)
let₅ : ∀ (f : ι → C) {c : Cocone.{u_3, v, u_3, u} (Discrete.functor f)} (hc : IsVanKampenColimit c), Mono (c.ι.app i)
let₆ :
  ∀ (f : ι → C) {c : Cocone.{u_3, v, u_3, u} (Discrete.functor f)} (hc : IsVanKampenColimit c),
    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)
let₇ :
  ∀ (f : ι → C) {c : Cocone.{u_3, v, u_3, u} (Discrete.functor f)} (hc : IsVanKampenColimit c),
    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)
h :
  ∀ (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 = 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)))
⊢ Mono (c.ι.app i)
have convert_4 : (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: classical
  let f : ι → C := F.obj ∘ Discrete.mk
  have : F = Discrete.functor f :=
    Functor.hext (fun i ↦ rfl) (by rintro ⟨i⟩ ⟨j⟩ ⟨⟨rfl : i = j⟩⟩; simp [f])
  clear_value f
  subst this
  refine PullbackCone.mono_of_isLimitMkIdId _ (IsPullback.isLimit ?_)
  nth_rw 1 [← Category.id_comp (c.ι.app i)]
  convert! IsPullback.paste_vert _ (isPullback_of_cofan_isVanKampen hc i.as i.as)
  swap
  · exact (eqToHom (if_pos rfl).symm)
  · simp
  · exact IsPullback.of_vert_isIso ⟨by simp⟩
Cleared hypotheses: F, c, hc
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (goal)
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 ι
let let₁ let₂ : Mono (c.ι.app i)
let₃ :
  let f := F.obj ∘ Discrete.mk;
  ∀ (this : F = Discrete.functor f), Mono (c.ι.app i)
let₄ : ∀ (f : ι → C) (this : F = Discrete.functor f), Mono (c.ι.app i)
let₅ : ∀ (f : ι → C) {c : Cocone.{u_3, v, u_3, u} (Discrete.functor f)} (hc : IsVanKampenColimit c), Mono (c.ι.app i)
let₆ :
  ∀ (f : ι → C) {c : Cocone.{u_3, v, u_3, u} (Discrete.functor f)} (hc : IsVanKampenColimit c),
    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)
let₇ :
  ∀ (f : ι → C) {c : Cocone.{u_3, v, u_3, u} (Discrete.functor f)} (hc : IsVanKampenColimit c),
    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)
h :
  ∀ (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 = 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 :
  (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
⊢ Mono (c.ι.app i)
have convert_6 : ∀ (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 sorry) (𝟙 (obj.{u_3, v, u_3, u} (Discrete.functor f) i))
    (if h : i.as = i.as then eqToHom sorry else eqToHom sorry ≫ initial.to (f i.as))
Tactic: classical
  let f : ι → C := F.obj ∘ Discrete.mk
  have : F = Discrete.functor f :=
    Functor.hext (fun i ↦ rfl) (by rintro ⟨i⟩ ⟨j⟩ ⟨⟨rfl : i = j⟩⟩; simp [f])
  clear_value f
  subst this
  refine PullbackCone.mono_of_isLimitMkIdId _ (IsPullback.isLimit ?_)
  nth_rw 1 [← Category.id_comp (c.ι.app i)]
  convert! IsPullback.paste_vert _ (isPullback_of_cofan_isVanKampen hc i.as i.as)
  swap
  · exact (eqToHom (if_pos rfl).symm)
  · simp
  · exact IsPullback.of_vert_isIso ⟨by simp⟩
Cleared hypotheses: F, c, hc
-- 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 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 d)
have 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) sorry))
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
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) ⋯))
have 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) sorry)))
    (Cocone.ι (Cofan.mk t.pt fun (i : ι) ↦ PullbackCone.IsLimit.lift ht (s i).fst ((s i).snd ≫ a.inj i) sorry))
    (map (const (Discrete ι)) t.snd))
Tactic: refine hau _ (Discrete.natTrans fun i ↦ (s i.as).snd) t.snd ?_ (.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 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))
⊢ 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) ⋯))
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 ((s i).snd ≫ a.inj i) sorry)) j)
    (NatTrans.app (Discrete.natTrans fun (i : Discrete ι) ↦ PullbackCone.snd (s i.as)) j) t.snd (a.ι.app j)
Tactic: refine hau _ (Discrete.natTrans fun i ↦ (s i.as).snd) t.snd ?_ (.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 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 ⋯
⊢ 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))
have 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) sorry)))
        (Cocone.ι (Cofan.mk t.pt fun (i : ι) ↦ PullbackCone.IsLimit.lift ht (s i).fst ((s i).snd ≫ a.inj i) sorry))
        (map (const (Discrete ι)) t.snd))
      x)
Tactic: ext
-- 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 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 := 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)
have 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) sorry)
  (PullbackCone.snd (s j.as)) 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]
-- 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 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) ⋯)
    (PullbackCone.snd (s j.as)) t.snd (a.ι.app j)
have 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) sorry)
  (PullbackCone.snd (s j.as)) t.snd (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 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) ⋯)
    (PullbackCone.snd (s j.as)) t.snd (a.inj j.as)
have 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) sorry ≫ t.fst)
  (PullbackCone.snd (s j.as)) v (a.inj j.as ≫ u)
Tactic: refine IsPullback.of_right ?_ (by simp) (IsPullback.of_isLimit ht)
-- 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 ⟶ 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) ⋯
⊢ IsPullback (Cofan.IsColimit.desc hd q₁) (Cofan.IsColimit.desc hd fun (x : ι) ↦ q₂ x ≫ a.inj x) v u
have obtain : ∀ (hc : IsColimit c), 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 _)
-- 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 ⟶ 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
⊢ IsPullback (Cofan.IsColimit.desc hd q₁) (Cofan.IsColimit.desc hd fun (x : ι) ↦ q₂ x ≫ a.inj x) v u
have refine_1 : pullback v u ≅ d.pt
Tactic: refine (IsPullback.of_hasPullback v u).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 ⟶ 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
⊢ IsPullback (Cofan.IsColimit.desc hd q₁) (Cofan.IsColimit.desc hd fun (x : ι) ↦ q₂ x ≫ a.inj x) v u
have refine_2 : pullback.fst v u ≫ Iso.hom (Iso.refl B) = (hc.coconePointUniqueUpToIso hd).hom ≫ Cofan.IsColimit.desc hd q₁
Tactic: refine (IsPullback.of_hasPullback v u).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 ⟶ 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₁
⊢ IsPullback (Cofan.IsColimit.desc hd q₁) (Cofan.IsColimit.desc hd fun (x : ι) ↦ q₂ x ≫ a.inj x) v u
have 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
Tactic: refine (IsPullback.of_hasPullback v u).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 ⟶ 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₁
have 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₁
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 ⟶ 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
have 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
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
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 d)
have 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 sorry))
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
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 ⋯))
have 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 sorry)))
    (Cocone.ι (Cofan.mk t.pt fun (i : ι) ↦ PullbackCone.IsLimit.lift ht ((s i).fst ≫ a.inj i) (s i).snd sorry))
    (map (const (Discrete ι)) t.fst))
Tactic: refine hau _ (Discrete.natTrans fun i ↦ (s i.as).fst) t.fst ?_ (.of_discrete _) fun j ↦ ?_