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
n : ℕ
f : Fin (n + 1) → C
c₁ : Cofan.{0, v, u} (C := C) fun (i : Fin n) ↦ f i.succ
c₂ : BinaryCofan.{v, u} (f 0) c₁.pt
t₁ : IsVanKampenColimit c₁
t₂ : IsVanKampenColimit c₂
inst_1 : ∀ {Z : C} (i : Z ⟶ c₂.pt), HasPullback c₂.inr i
inst_2 : HasFiniteCoproducts.{v, u} C
F : Functor.{0, v, 0, u} (Discrete (Fin (n + 1))) C
c : Cocone F
α : F ⟶ Discrete.functor f
i : c.pt ⟶ (extendCofan c₁ c₂).pt
e : α ≫ (extendCofan c₁ c₂).ι = c.ι ≫ map (const (Discrete (Fin (n + 1)))) i
hα : NatTrans.Equifibered α
Hc : IsColimit c
j : Fin (n + 1)
t₂' :
  ∀ (j : Discrete WalkingPair),
    IsPullback (P :=
      obj.{0, v, 0, u} (pair (F.obj { as := 0 }) (sigmaObj.{0, v, u} fun (j : Fin n) ↦ F.obj { as := j.succ })) j)
      (NatTrans.app
        (Cocone.ι
          (BinaryCofan.mk (c.ι.app { as := 0 : Discrete (Fin (n + 1)) })
            (Sigma.desc fun (b : Fin n) ↦ c.ι.app { as := b.succ })))
        j)
      (NatTrans.app (mapPair (α.app { as := 0 }) (Sigma.desc fun (b : Fin n) ↦ α.app { as := b.succ } ≫ c₁.inj b)) j) i
      (c₂.ι.app j)
⊢ IsPullback (P := F.obj { as := j }) (c.ι.app { as := j }) (α.app { as := j }) i
    ((extendCofan c₁ c₂).ι.app { as := j })
have refine_3 : IsPullback (P := F.obj { as := 0 }) (c.ι.app { as := 0 }) (α.app { as := 0 }) i ((extendCofan c₁ c₂).ι.app { as := 0 })
Tactic: induction j using Fin.inductionOn with
  | zero => exact t₂' ⟨WalkingPair.left⟩
  | succ j _ =>
    have t₁' := (@t₁ (Discrete.functor (fun j ↦ F.obj ⟨j.succ⟩)) (Cofan.mk _ _) (Discrete.natTrans
      fun i ↦ α.app _) (Sigma.desc (fun j ↦ α.app _ ≫ c₁.inj _)) ?_
      (.of_discrete _)).mp ⟨coproductIsCoproduct _⟩ ⟨j⟩
    rotate_left
    · ext ⟨j⟩
      dsimp
      rw [colimit.ι_desc]
      rfl
    simpa [Functor.const_obj_obj, Discrete.functor_obj, extendCofan_pt, extendCofan_ι_app,
      Fin.cases_succ, BinaryCofan.mk_pt, colimit.cocone_x, Cofan.mk_pt, Cofan.mk_ι_app,
      BinaryCofan.ι_app_right, BinaryCofan.mk_inr, colimit.ι_desc,
      Discrete.natTrans_app] using t₁'.paste_horiz (t₂' ⟨WalkingPair.right⟩)
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (goal)
Goal:
C : Type u
inst : Category.{v, u} C
n : ℕ
f : Fin (n + 1) → C
c₁ : Cofan.{0, v, u} (C := C) fun (i : Fin n) ↦ f i.succ
c₂ : BinaryCofan.{v, u} (f 0) c₁.pt
t₁ : IsVanKampenColimit c₁
t₂ : IsVanKampenColimit c₂
inst_1 : ∀ {Z : C} (i : Z ⟶ c₂.pt), HasPullback c₂.inr i
inst_2 : HasFiniteCoproducts.{v, u} C
F : Functor.{0, v, 0, u} (Discrete (Fin (n + 1))) C
c : Cocone F
α : F ⟶ Discrete.functor f
i : c.pt ⟶ (extendCofan c₁ c₂).pt
e : α ≫ (extendCofan c₁ c₂).ι = c.ι ≫ map (const (Discrete (Fin (n + 1)))) i
hα : NatTrans.Equifibered α
Hc : IsColimit c
j : Fin (n + 1)
t₂' :
  ∀ (j : Discrete WalkingPair),
    IsPullback (P :=
      obj.{0, v, 0, u} (pair (F.obj { as := 0 }) (sigmaObj.{0, v, u} fun (j : Fin n) ↦ F.obj { as := j.succ })) j)
      (NatTrans.app
        (Cocone.ι
          (BinaryCofan.mk (c.ι.app { as := 0 : Discrete (Fin (n + 1)) })
            (Sigma.desc fun (b : Fin n) ↦ c.ι.app { as := b.succ })))
        j)
      (NatTrans.app (mapPair (α.app { as := 0 }) (Sigma.desc fun (b : Fin n) ↦ α.app { as := b.succ } ≫ c₁.inj b)) j) i
      (c₂.ι.app j)
refine_3 :
  IsPullback (P := F.obj { as := 0 }) (c.ι.app { as := 0 }) (α.app { as := 0 }) i
    ((extendCofan c₁ c₂).ι.app { as := 0 })
⊢ IsPullback (P := F.obj { as := j }) (c.ι.app { as := j }) (α.app { as := j }) i
    ((extendCofan c₁ c₂).ι.app { as := j })
have refine_3₁ : ∀ (j : Fin n),
  IsPullback (P := F.obj { as := j.castSucc }) (c.ι.app { as := j.castSucc }) (α.app { as := j.castSucc }) i
      ((extendCofan c₁ c₂).ι.app { as := j.castSucc }) →
    IsPullback (P := F.obj { as := j.succ }) (c.ι.app { as := j.succ }) (α.app { as := j.succ }) i
      ((extendCofan c₁ c₂).ι.app { as := j.succ })
Tactic: induction j using Fin.inductionOn with
  | zero => exact t₂' ⟨WalkingPair.left⟩
  | succ j _ =>
    have t₁' := (@t₁ (Discrete.functor (fun j ↦ F.obj ⟨j.succ⟩)) (Cofan.mk _ _) (Discrete.natTrans
      fun i ↦ α.app _) (Sigma.desc (fun j ↦ α.app _ ≫ c₁.inj _)) ?_
      (.of_discrete _)).mp ⟨coproductIsCoproduct _⟩ ⟨j⟩
    rotate_left
    · ext ⟨j⟩
      dsimp
      rw [colimit.ι_desc]
      rfl
    simpa [Functor.const_obj_obj, Discrete.functor_obj, extendCofan_pt, extendCofan_ι_app,
      Fin.cases_succ, BinaryCofan.mk_pt, colimit.cocone_x, Cofan.mk_pt, Cofan.mk_ι_app,
      BinaryCofan.ι_app_right, BinaryCofan.mk_inr, colimit.ι_desc,
      Discrete.natTrans_app] using t₁'.paste_horiz (t₂' ⟨WalkingPair.right⟩)
Cleared hypotheses: j
-- 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
X : ι → C
c : Cofan.{u_3, v, u} X
hc : IsVanKampenColimit c
i j : ι
inst_2 : DecidableEq ι
⊢ IsPullback (P := if j = i then X i else initial.{v, u} C)
    (if h : j = i then eqToHom ⋯ else eqToHom ⋯ ≫ initial.to (X i))
    (if h : j = i then eqToHom ⋯ else eqToHom ⋯ ≫ initial.to (X j)) (c.inj i) (c.inj j)
have refine_1 : Eq (α :=
  Quiver.Hom (V := Functor.{u_3, v, u_3, u} (Discrete ι) C)
    (Discrete.functor fun (k : ι) ↦ if k = i then X i else initial.{v, u} C) (obj (const (Discrete ι)) c.pt))
  ((Discrete.natTrans fun (k : Discrete ι) ↦
      if h : k.as = i then eqToHom sorry else eqToHom sorry ≫ initial.to (obj.{u_3, v, u_3, u} (Discrete.functor X) k)) ≫
    c.ι)
  (CategoryStruct.comp (Y :=
    obj (const (Discrete ι))
      (Cocone.pt.{u_3, v, u_3, u} (J := Discrete ι) (F :=
        Discrete.functor fun (k : ι) ↦ if k = i then X i else initial.{v, u} C)
        (Cofan.mk (X i) fun (k : ι) ↦ if h : k = i then eqToHom sorry else eqToHom sorry ≫ initial.to (X i))))
    (Cocone.ι (Cofan.mk (X i) fun (k : ι) ↦ if h : k = i then eqToHom sorry else eqToHom sorry ≫ initial.to (X i)))
    (map (const (Discrete ι)) (c.inj i)))
Tactic: refine (hc (Cofan.mk (X i) (f := fun k ↦ if k = i then X i else ⊥_ C)
    (fun k ↦ if h : k = i then (eqToHom <| if_pos h) else (eqToHom <| if_neg h) ≫ initial.to _))
    (Discrete.natTrans (fun k ↦ if h : k.1 = i then (eqToHom <| (if_pos h).trans
      (congr_arg X h.symm)) else (eqToHom <| if_neg h) ≫ initial.to _))
    (c.inj i) ?_ (.of_discrete _)).mp ⟨?_⟩ ⟨j⟩
-- 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
X : ι → C
c : Cofan.{u_3, v, u} X
hc : IsVanKampenColimit c
i j : ι
inst_2 : DecidableEq ι
refine_1 :
  Eq (α :=
    Quiver.Hom (V := Functor.{u_3, v, u_3, u} (Discrete ι) C)
      (Discrete.functor fun (k : ι) ↦ if k = i then X i else initial.{v, u} C) (obj (const (Discrete ι)) c.pt))
    ((Discrete.natTrans fun (k : Discrete ι) ↦
        if h : k.as = i then eqToHom ⋯ else eqToHom ⋯ ≫ initial.to (obj.{u_3, v, u_3, u} (Discrete.functor X) k)) ≫
      c.ι)
    (CategoryStruct.comp (Y :=
      obj (const (Discrete ι))
        (Cocone.pt.{u_3, v, u_3, u} (J := Discrete ι) (F :=
          Discrete.functor fun (k : ι) ↦ if k = i then X i else initial.{v, u} C)
          (Cofan.mk (X i) fun (k : ι) ↦ if h : k = i then eqToHom ⋯ else eqToHom ⋯ ≫ initial.to (X i))))
      (Cocone.ι (Cofan.mk (X i) fun (k : ι) ↦ if h : k = i then eqToHom ⋯ else eqToHom ⋯ ≫ initial.to (X i)))
      (map (const (Discrete ι)) (c.inj i)))
⊢ IsPullback (P := if j = i then X i else initial.{v, u} C)
    (if h : j = i then eqToHom ⋯ else eqToHom ⋯ ≫ initial.to (X i))
    (if h : j = i then eqToHom ⋯ else eqToHom ⋯ ≫ initial.to (X j)) (c.inj i) (c.inj j)
have refine_2 : IsColimit.{u_3, v, u_3, u} (J := Discrete ι) (F :=
  Discrete.functor fun (k : ι) ↦ if k = i then X i else initial.{v, u} C)
  (Cofan.mk (X i) fun (k : ι) ↦ if h : k = i then eqToHom sorry else eqToHom sorry ≫ initial.to (X i))
Tactic: refine (hc (Cofan.mk (X i) (f := fun k ↦ if k = i then X i else ⊥_ C)
    (fun k ↦ if h : k = i then (eqToHom <| if_pos h) else (eqToHom <| if_neg h) ≫ initial.to _))
    (Discrete.natTrans (fun k ↦ if h : k.1 = i then (eqToHom <| (if_pos h).trans
      (congr_arg X h.symm)) else (eqToHom <| if_neg h) ≫ initial.to _))
    (c.inj i) ?_ (.of_discrete _)).mp ⟨?_⟩ ⟨j⟩
-- 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
X : ι → C
c : Cofan.{u_3, v, u} X
hc : IsVanKampenColimit c
i j : ι
inst_2 : DecidableEq ι
⊢ Eq (α :=
    Quiver.Hom (V := Functor.{u_3, v, u_3, u} (Discrete ι) C)
      (Discrete.functor fun (k : ι) ↦ if k = i then X i else initial.{v, u} C) (obj (const (Discrete ι)) c.pt))
    ((Discrete.natTrans fun (k : Discrete ι) ↦
        if h : k.as = i then eqToHom ⋯ else eqToHom ⋯ ≫ initial.to (obj.{u_3, v, u_3, u} (Discrete.functor X) k)) ≫
      c.ι)
    (CategoryStruct.comp (Y :=
      obj (const (Discrete ι))
        (Cocone.pt.{u_3, v, u_3, u} (J := Discrete ι) (F :=
          Discrete.functor fun (k : ι) ↦ if k = i then X i else initial.{v, u} C)
          (Cofan.mk (X i) fun (k : ι) ↦ if h : k = i then eqToHom ⋯ else eqToHom ⋯ ≫ initial.to (X i))))
      (Cocone.ι (Cofan.mk (X i) fun (k : ι) ↦ if h : k = i then eqToHom ⋯ else eqToHom ⋯ ≫ initial.to (X i)))
      (map (const (Discrete ι)) (c.inj i)))
have refine_1 : ∀ (k : ι),
  Eq (α :=
    obj.{u_3, v, u_3, u} (Discrete.functor fun (k : ι) ↦ if k = i then X i else initial.{v, u} C)
        { as := k : Discrete ι } ⟶
      obj.{u_3, v, u_3, u} (obj (const (Discrete ι)) c.pt) { as := k : Discrete ι })
    (NatTrans.app
      ((Discrete.natTrans fun (k : Discrete ι) ↦
          if h : k.as = i then eqToHom sorry else eqToHom sorry ≫ initial.to (obj.{u_3, v, u_3, u} (Discrete.functor X) k)) ≫
        c.ι)
      { as := k })
    (NatTrans.app
      (CategoryStruct.comp (Y :=
        obj (const (Discrete ι))
          (Cocone.pt.{u_3, v, u_3, u} (J := Discrete ι) (F :=
            Discrete.functor fun (k : ι) ↦ if k = i then X i else initial.{v, u} C)
            (Cofan.mk (X i) fun (k : ι) ↦ if h : k = i then eqToHom sorry else eqToHom sorry ≫ initial.to (X i))))
        (Cocone.ι (Cofan.mk (X i) fun (k : ι) ↦ if h : k = i then eqToHom sorry else eqToHom sorry ≫ initial.to (X i)))
        (map (const (Discrete ι)) (c.inj i)))
      { as := k })
Tactic: ext ⟨k⟩
-- 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
X : ι → C
c : Cofan.{u_3, v, u} X
hc : IsVanKampenColimit c
i j : ι
inst_2 : DecidableEq ι
k : ι
⊢ Eq (α :=
    obj.{u_3, v, u_3, u} (Discrete.functor fun (k : ι) ↦ if k = i then X i else initial.{v, u} C)
        { as := k : Discrete ι } ⟶
      obj.{u_3, v, u_3, u} (obj (const (Discrete ι)) c.pt) { as := k : Discrete ι })
    (NatTrans.app
      ((Discrete.natTrans fun (k : Discrete ι) ↦
          if h : k.as = i then eqToHom ⋯ else eqToHom ⋯ ≫ initial.to (obj.{u_3, v, u_3, u} (Discrete.functor X) k)) ≫
        c.ι)
      { as := k })
    (NatTrans.app
      (CategoryStruct.comp (Y :=
        obj (const (Discrete ι))
          (Cocone.pt.{u_3, v, u_3, u} (J := Discrete ι) (F :=
            Discrete.functor fun (k : ι) ↦ if k = i then X i else initial.{v, u} C)
            (Cofan.mk (X i) fun (k : ι) ↦ if h : k = i then eqToHom ⋯ else eqToHom ⋯ ≫ initial.to (X i))))
        (Cocone.ι (Cofan.mk (X i) fun (k : ι) ↦ if h : k = i then eqToHom ⋯ else eqToHom ⋯ ≫ initial.to (X i)))
        (map (const (Discrete ι)) (c.inj i)))
      { as := k })
have refine_1 : Eq (α := (if k = i then X i else initial.{v, u} C) ⟶ c.pt)
  (CategoryStruct.comp (Y := X k) (if h : k = i then eqToHom sorry else eqToHom sorry ≫ initial.to (X k))
      (c.ι.app { as := k }) :
    (if k = i then X i else initial.{v, u} C) ⟶ c.pt)
  ((if h : k = i then eqToHom sorry else eqToHom sorry ≫ initial.to (X i)) ≫ c.inj i :
    (if k = i then X i else initial.{v, u} C) ⟶ c.pt)
Tactic: simp only [Discrete.functor_obj, Functor.const_obj_obj, NatTrans.comp_app,
      Discrete.natTrans_app, Cofan.mk_pt, Cofan.mk_ι_app, Functor.const_map_app]
-- 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
X : ι → C
c : Cofan.{u_3, v, u} X
hc : IsVanKampenColimit c
i j : ι
inst_2 : DecidableEq ι
k : ι
⊢ Eq (α := (if k = i then X i else initial.{v, u} C) ⟶ c.pt)
    (CategoryStruct.comp (Y := X k) (if h : k = i then eqToHom ⋯ else eqToHom ⋯ ≫ initial.to (X k))
        (c.ι.app { as := k }) :
      (if k = i then X i else initial.{v, u} C) ⟶ c.pt)
    ((if h : k = i then eqToHom ⋯ else eqToHom ⋯ ≫ initial.to (X i)) ≫ c.inj i :
      (if k = i then X i else initial.{v, u} C) ⟶ c.pt)
have refine_1 : ∀ (h : k = i),
  Eq (α := (if k = i then X i else initial.{v, u} C) ⟶ c.pt) (eqToHom sorry ≫ c.ι.app { as := k }) (eqToHom sorry ≫ c.inj i)
Tactic: split
-- 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
X : ι → C
c : Cofan.{u_3, v, u} X
hc : IsVanKampenColimit c
i j : ι
inst_2 : DecidableEq ι
k : ι
refine_1 :
  ∀ (h : k = i),
    Eq (α := (if k = i then X i else initial.{v, u} C) ⟶ c.pt) (eqToHom ⋯ ≫ c.ι.app { as := k }) (eqToHom ⋯ ≫ c.inj i)
⊢ Eq (α := (if k = i then X i else initial.{v, u} C) ⟶ c.pt)
    (CategoryStruct.comp (Y := X k) (if h : k = i then eqToHom ⋯ else eqToHom ⋯ ≫ initial.to (X k))
        (c.ι.app { as := k }) :
      (if k = i then X i else initial.{v, u} C) ⟶ c.pt)
    ((if h : k = i then eqToHom ⋯ else eqToHom ⋯ ≫ initial.to (X i)) ≫ c.inj i :
      (if k = i then X i else initial.{v, u} C) ⟶ c.pt)
have refine_1₁ : ∀ (h : ¬k = i),
  Eq (α := (if k = i then X i else initial.{v, u} C) ⟶ c.pt) ((eqToHom sorry ≫ initial.to (X k)) ≫ c.ι.app { as := k })
    ((eqToHom sorry ≫ initial.to (X i)) ≫ c.inj i)
Tactic: split
-- 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
X : ι → C
c : Cofan.{u_3, v, u} X
hc : IsVanKampenColimit c
i j : ι
inst_2 : DecidableEq ι
k : ι
h : k = i
⊢ Eq (α := (if k = i then X i else initial.{v, u} C) ⟶ c.pt) (eqToHom ⋯ ≫ c.ι.app { as := k }) (eqToHom ⋯ ≫ c.inj i)
have refine_1 : Eq (α := (if k = k then X k else initial.{v, u} C) ⟶ c.pt) (eqToHom sorry ≫ c.ι.app { as := k }) (eqToHom sorry ≫ c.inj k)
Tactic: subst ‹k = i›
Cleared hypotheses: i, h
-- 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
X : ι → C
c : Cofan.{u_3, v, u} X
hc : IsVanKampenColimit c
i j : ι
inst_2 : DecidableEq ι
⊢ IsColimit.{u_3, v, u_3, u} (J := Discrete ι) (F :=
    Discrete.functor fun (k : ι) ↦ if k = i then X i else initial.{v, u} C)
    (Cofan.mk (X i) fun (k : ι) ↦ if h : k = i then eqToHom ⋯ else eqToHom ⋯ ≫ initial.to (X i))
have refine_2 : ∀ (t : Cofan.{u_3, v, u} (C := C) fun (k : ι) ↦ if k = i then X i else initial.{v, u} C) (j : ι),
  CategoryStruct.comp (Y :=
      Cocone.pt.{u_3, v, u_3, u} (J := Discrete ι) (F :=
        Discrete.functor fun (k : ι) ↦ if k = i then X i else initial.{v, u} C)
        (Cofan.mk (X i) fun (k : ι) ↦ if h : k = i then eqToHom sorry else eqToHom sorry ≫ initial.to (X i)))
      (Cofan.inj.{u_3, v, u} (f := fun (k : ι) ↦ if k = i then X i else initial.{v, u} C)
        (Cofan.mk (X i) fun (k : ι) ↦ if h : k = i then eqToHom sorry else eqToHom sorry ≫ initial.to (X i)) j)
      ((fun (t : Cofan.{u_3, v, u} (C := C) fun (k : ι) ↦ if k = i then X i else initial.{v, u} C) ↦
          eqToHom sorry ≫ t.inj i)
        t) =
    t.inj j
Tactic: refine Cofan.IsColimit.mk _ (fun t ↦ (eqToHom (if_pos rfl).symm) ≫ t.inj i) ?_ ?_
-- 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
X : ι → C
c : Cofan.{u_3, v, u} X
hc : IsVanKampenColimit c
i j : ι
inst_2 : DecidableEq ι
refine_2 :
  ∀ (t : Cofan.{u_3, v, u} (C := C) fun (k : ι) ↦ if k = i then X i else initial.{v, u} C) (j : ι),
    CategoryStruct.comp (Y :=
        Cocone.pt.{u_3, v, u_3, u} (J := Discrete ι) (F :=
          Discrete.functor fun (k : ι) ↦ if k = i then X i else initial.{v, u} C)
          (Cofan.mk (X i) fun (k : ι) ↦ if h : k = i then eqToHom ⋯ else eqToHom ⋯ ≫ initial.to (X i)))
        (Cofan.inj.{u_3, v, u} (f := fun (k : ι) ↦ if k = i then X i else initial.{v, u} C)
          (Cofan.mk (X i) fun (k : ι) ↦ if h : k = i then eqToHom ⋯ else eqToHom ⋯ ≫ initial.to (X i)) j)
        ((fun (t : Cofan.{u_3, v, u} (C := C) fun (k : ι) ↦ if k = i then X i else initial.{v, u} C) ↦
            eqToHom ⋯ ≫ t.inj i)
          t) =
      t.inj j
⊢ IsColimit.{u_3, v, u_3, u} (J := Discrete ι) (F :=
    Discrete.functor fun (k : ι) ↦ if k = i then X i else initial.{v, u} C)
    (Cofan.mk (X i) fun (k : ι) ↦ if h : k = i then eqToHom ⋯ else eqToHom ⋯ ≫ initial.to (X i))
have refine_2₁ : ∀ (t : Cofan.{u_3, v, u} (C := C) fun (k : ι) ↦ if k = i then X i else initial.{v, u} C)
  (m :
    Cocone.pt.{u_3, v, u_3, u} (J := Discrete ι) (F :=
        Discrete.functor fun (k : ι) ↦ if k = i then X i else initial.{v, u} C)
        (Cofan.mk (X i) fun (k : ι) ↦ if h : k = i then eqToHom sorry else eqToHom sorry ≫ initial.to (X i)) ⟶
      t.pt),
  (∀ (j : ι),
      Cofan.inj.{u_3, v, u} (f := fun (k : ι) ↦ if k = i then X i else initial.{v, u} C)
            (Cofan.mk (X i) fun (k : ι) ↦ if h : k = i then eqToHom sorry else eqToHom sorry ≫ initial.to (X i)) j ≫
          m =
        t.inj j) →
    m =
      (fun (t : Cofan.{u_3, v, u} (C := C) fun (k : ι) ↦ if k = i then X i else initial.{v, u} C) ↦ eqToHom sorry ≫ t.inj i)
        t
Tactic: refine Cofan.IsColimit.mk _ (fun t ↦ (eqToHom (if_pos rfl).symm) ≫ t.inj i) ?_ ?_
-- 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
X : ι → C
c : Cofan.{u_3, v, u} X
hc : IsVanKampenColimit c
i j_1 : ι
inst_2 : DecidableEq ι
t : Cofan.{u_3, v, u} (C := C) fun (k : ι) ↦ if k = i then X i else initial.{v, u} C
j : ι
⊢ CategoryStruct.comp (Y :=
      Cocone.pt.{u_3, v, u_3, u} (J := Discrete ι) (F :=
        Discrete.functor fun (k : ι) ↦ if k = i then X i else initial.{v, u} C)
        (Cofan.mk (X i) fun (k : ι) ↦ if h : k = i then eqToHom ⋯ else eqToHom ⋯ ≫ initial.to (X i)))
      (Cofan.inj.{u_3, v, u} (f := fun (k : ι) ↦ if k = i then X i else initial.{v, u} C)
        (Cofan.mk (X i) fun (k : ι) ↦ if h : k = i then eqToHom ⋯ else eqToHom ⋯ ≫ initial.to (X i)) j)
      ((fun (t : Cofan.{u_3, v, u} (C := C) fun (k : ι) ↦ if k = i then X i else initial.{v, u} C) ↦
          eqToHom ⋯ ≫ t.inj i)
        t) =
    t.inj j
have refine_2 : (if h : j = i then eqToHom sorry else eqToHom sorry ≫ initial.to (X i)) ≫ eqToHom sorry ≫ t.inj i = t.inj j
Tactic: simp only [Cofan.mk_pt, cofan_mk_inj]
-- 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
X : ι → C
c : Cofan.{u_3, v, u} X
hc : IsVanKampenColimit c
i j_1 : ι
inst_2 : DecidableEq ι
t : Cofan.{u_3, v, u} (C := C) fun (k : ι) ↦ if k = i then X i else initial.{v, u} C
j : ι
⊢ (if h : j = i then eqToHom ⋯ else eqToHom ⋯ ≫ initial.to (X i)) ≫ eqToHom ⋯ ≫ t.inj i = t.inj j
have refine_2 : ∀ (h : j = i), eqToHom sorry ≫ eqToHom sorry ≫ t.inj i = t.inj j
Tactic: split
-- 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
X : ι → C
c : Cofan.{u_3, v, u} X
hc : IsVanKampenColimit c
i j_1 : ι
inst_2 : DecidableEq ι
t : Cofan.{u_3, v, u} (C := C) fun (k : ι) ↦ if k = i then X i else initial.{v, u} C
j : ι
refine_2 : ∀ (h : j = i), eqToHom ⋯ ≫ eqToHom ⋯ ≫ t.inj i = t.inj j
⊢ (if h : j = i then eqToHom ⋯ else eqToHom ⋯ ≫ initial.to (X i)) ≫ eqToHom ⋯ ≫ t.inj i = t.inj j
have refine_2₁ : ∀ (h : ¬j = i), (eqToHom sorry ≫ initial.to (X i)) ≫ eqToHom sorry ≫ t.inj i = t.inj j
Tactic: split
-- 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
X : ι → C
c : Cofan.{u_3, v, u} X
hc : IsVanKampenColimit c
i j_1 : ι
inst_2 : DecidableEq ι
t : Cofan.{u_3, v, u} (C := C) fun (k : ι) ↦ if k = i then X i else initial.{v, u} C
j : ι
h : j = i
⊢ eqToHom ⋯ ≫ eqToHom ⋯ ≫ t.inj i = t.inj j
have refine_2 : ∀ (t : Cofan.{u_3, v, u} (C := C) fun (k : ι) ↦ if k = j then X j else initial.{v, u} C),
  eqToHom sorry ≫ eqToHom sorry ≫ t.inj j = t.inj j
Tactic: subst ‹j = i›
Cleared hypotheses: i, t, h
-- 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
X : ι → C
c : Cofan.{u_3, v, u} X
hc : IsVanKampenColimit c
i j_1 : ι
inst_2 : DecidableEq ι
t : Cofan.{u_3, v, u} (C := C) fun (k : ι) ↦ if k = i then X i else initial.{v, u} C
j : ι
h : ¬j = i
⊢ (eqToHom ⋯ ≫ initial.to (X i)) ≫ eqToHom ⋯ ≫ t.inj i = t.inj j
have refine_2 : initial.to (X i) ≫ eqToHom sorry ≫ t.inj i = inv (eqToHom sorry) ≫ t.inj j
Tactic: rw [Category.assoc, ← IsIso.eq_inv_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (hypothesis)
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 j : Discrete ι
hi : i ≠ j
f : ι → C := F.obj ∘ Discrete.mk
⊢ IsPullback (P := initial.{v, u} C) (initial.to (F.obj i)) (initial.to (F.obj j)) (c.ι.app i) (c.ι.app j)
have this : F = Discrete.functor f
Tactic: have : F = Discrete.functor f :=
    Functor.hext (fun i ↦ rfl) (by rintro ⟨i⟩ ⟨j⟩ ⟨⟨rfl : i = j⟩⟩; simp [f])
-- 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 j : Discrete ι
hi : i ≠ j
f : ι → C := F.obj ∘ Discrete.mk
this : F = Discrete.functor f
⊢ IsPullback (P := initial.{v, u} C) (initial.to (F.obj i)) (initial.to (F.obj j)) (c.ι.app i) (c.ι.app j)
have clear_value : ∀ (f : ι → C) (this : F = Discrete.functor f),
  IsPullback (P := initial.{v, u} C) (initial.to (F.obj i)) (initial.to (F.obj j)) (c.ι.app i) (c.ι.app j)
Tactic: clear_value f
Cleared hypotheses: f, this
-- 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 j : Discrete ι
hi : i ≠ j
f : ι → C
this : F = Discrete.functor f
⊢ IsPullback (P := initial.{v, u} C) (initial.to (F.obj i)) (initial.to (F.obj j)) (c.ι.app i) (c.ι.app j)
have subst : ∀ {c : Cocone.{u_3, v, u_3, u} (Discrete.functor f)} (hc : IsVanKampenColimit c),
  IsPullback (P := initial.{v, u} C) (initial.to (obj.{u_3, v, u_3, u} (Discrete.functor f) i))
    (initial.to (obj.{u_3, v, u_3, u} (Discrete.functor f) j)) (c.ι.app i) (c.ι.app j)
Tactic: subst this
Cleared hypotheses: F, c, hc, this
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasInitial.{v, u} C
ι : Type u_3
i j : Discrete ι
hi : i ≠ j
f : ι → C
c : Cocone.{u_3, v, u_3, u} (Discrete.functor f)
hc : IsVanKampenColimit c
⊢ IsPullback (P := initial.{v, u} C) (initial.to (obj.{u_3, v, u_3, u} (Discrete.functor f) i))
    (initial.to (obj.{u_3, v, u_3, u} (Discrete.functor f) j)) (c.ι.app i) (c.ι.app j)
have this : ∀ (i : Discrete ι), Subsingleton.{v + 1} (initial.{v, u} C ⟶ obj.{u_3, v, u_3, u} (Discrete.functor f) i)
Tactic: have : ∀ i, Subsingleton (⊥_ C ⟶ (Discrete.functor f).obj i) := inferInstance