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
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)))
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 ⋯ else eqToHom ⋯ ≫ initial.to (X 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)

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⟩

Premises used: CategoryTheory.eqToHom, CategoryTheory.Discrete.functor, CategoryTheory.Limits.initial.to, CategoryTheory.NatTrans.Equifibered.of_discrete, if_pos, Nonempty.intro, CategoryTheory.Discrete.natTrans, dite, CategoryTheory.Discrete.mk, congr_arg, CategoryTheory.Discrete.as, CategoryTheory.Limits.Cofan.inj, CategoryTheory.CategoryStruct.comp, Iff.mp, CategoryTheory.Limits.Cofan.mk, Eq.symm, Eq, if_neg, CategoryTheory.Functor.obj, Eq.trans
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
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 :
  ∀ (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 })
⊢ 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)))

Tactic:
ext ⟨k⟩
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
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 :
  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)
⊢ 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 })

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]

Premises used: CategoryTheory.Discrete.functor_obj, CategoryTheory.Limits.Cofan.mk_ι_app, CategoryTheory.Limits.Cofan.mk_pt, CategoryTheory.Functor.const_map_app, CategoryTheory.Functor.const_obj_obj, CategoryTheory.NatTrans.comp_app, CategoryTheory.Discrete.natTrans_app
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
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)
refine_1₁ :
  ∀ (h : ¬k = i),
    Eq (α := (if k = i then X i else initial.{v, u} C) ⟶ c.pt) ((eqToHom ⋯ ≫ initial.to (X k)) ≫ c.ι.app { as := k })
      ((eqToHom ⋯ ≫ initial.to (X i)) ≫ 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)

Tactic:
split
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
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
refine_1 :
  Eq (α := (if k = k then X k else initial.{v, u} C) ⟶ c.pt) (eqToHom ⋯ ≫ c.ι.app { as := k }) (eqToHom ⋯ ≫ c.inj k)
⊢ Eq (α := (if k = i then X i else initial.{v, u} C) ⟶ c.pt) (eqToHom ⋯ ≫ c.ι.app { as := k }) (eqToHom ⋯ ≫ c.inj i)

Tactic:
subst ‹k = i›
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
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
j : ι
inst_2 : DecidableEq ι
k : ι
⊢ Eq (α := (if k = k then X k else initial.{v, u} C) ⟶ c.pt) (eqToHom ⋯ ≫ c.ι.app { as := k }) (eqToHom ⋯ ≫ c.inj k)

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
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 ⋯ ≫ initial.to (X k)) ≫ c.ι.app { as := k })
    ((eqToHom ⋯ ≫ initial.to (X i)) ≫ c.inj i)

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
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
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 ⋯ else eqToHom ⋯ ≫ 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 ⋯ else eqToHom ⋯ ≫ 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 ⋯ ≫ t.inj i)
          t
⊢ 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))

Tactic:
refine Cofan.IsColimit.mk _ (fun t ↦ (eqToHom (if_pos rfl).symm) ≫ t.inj i) ?_ ?_

Premises used: CategoryTheory.Limits.Cofan.IsColimit.mk, CategoryTheory.eqToHom, if_pos, CategoryTheory.CategoryStruct.comp, 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
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 : (if h : j = i then eqToHom ⋯ else eqToHom ⋯ ≫ initial.to (X i)) ≫ eqToHom ⋯ ≫ t.inj i = t.inj 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

Tactic:
simp only [Cofan.mk_pt, cofan_mk_inj]

Premises used: CategoryTheory.Limits.Cofan.mk_pt, CategoryTheory.Limits.cofan_mk_inj
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
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
refine_2₁ : ∀ (h : ¬j = i), (eqToHom ⋯ ≫ initial.to (X i)) ≫ 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

Tactic:
split
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
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
refine_2 :
  ∀ (t : Cofan.{u_3, v, u} (C := C) fun (k : ι) ↦ if k = j then X j else initial.{v, u} C),
    eqToHom ⋯ ≫ eqToHom ⋯ ≫ t.inj j = t.inj j
⊢ eqToHom ⋯ ≫ eqToHom ⋯ ≫ t.inj i = t.inj j

Tactic:
subst ‹j = i›
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
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
j_1 : ι
inst_2 : DecidableEq ι
j : ι
t : Cofan.{u_3, v, u} (C := C) fun (k : ι) ↦ if k = j then X j else initial.{v, u} C
⊢ eqToHom ⋯ ≫ eqToHom ⋯ ≫ t.inj j = t.inj j

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
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
refine_2 : initial.to (X i) ≫ eqToHom ⋯ ≫ t.inj i = inv (eqToHom ⋯) ≫ t.inj j
⊢ (eqToHom ⋯ ≫ initial.to (X i)) ≫ eqToHom ⋯ ≫ t.inj i = t.inj j

Tactic:
rw [Category.assoc, ← IsIso.eq_inv_comp]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.IsIso.eq_inv_comp
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
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
⊢ initial.to (X i) ≫ eqToHom ⋯ ≫ t.inj i = inv (eqToHom ⋯) ≫ t.inj j

Tactic:
initialIsInitial.hom_ext _ _

Premises used: CategoryTheory.Limits.IsInitial.hom_ext, CategoryTheory.Limits.initialIsInitial
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
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
⊢ initial.to (X i) ≫ eqToHom ⋯ ≫ t.inj i = inv (eqToHom ⋯) ≫ t.inj j

Tactic:
exact initialIsInitial.hom_ext _ _

Premises used: CategoryTheory.Limits.IsInitial.hom_ext, CategoryTheory.Limits.initialIsInitial
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
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 ι
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 ⋯ else eqToHom ⋯ ≫ initial.to (X i)) ⟶
    t.pt
hm :
  ∀ (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 ⋯ else eqToHom ⋯ ≫ 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 ⋯ ≫ t.inj i) t

Tactic:
simp [← hm i]
-- 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 j : Discrete ι
hi : i_1 ≠ j
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 j : Discrete ι
hi : i ≠ j
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 j : Discrete ι
hi : i ≠ j
f : ι → C := F.obj ∘ Discrete.mk
this : F = Discrete.functor f
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)
⊢ 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
-- 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 j : Discrete ι
hi : i ≠ j
f : ι → C
this : F = Discrete.functor f
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)
⊢ IsPullback (P := initial.{v, u} C) (initial.to (F.obj i)) (initial.to (F.obj j)) (c.ι.app i) (c.ι.app j)

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 j : Discrete ι
hi : i ≠ j
f : ι → C
c : Cocone.{u_3, v, u_3, u} (Discrete.functor f)
hc : IsVanKampenColimit c
⊢ ∀ (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
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
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
this : ∀ (i : Discrete ι), Subsingleton.{v + 1} (initial.{v, u} C ⟶ obj.{u_3, v, u_3, u} (Discrete.functor f) i)
⊢ IsPullback (P := if j.as = i.as then f i.as else initial.{v, u} C) (X := f i.as) (Y := f j.as)
    (if h : j.as = i.as then eqToHom ⋯ else eqToHom ⋯ ≫ initial.to (f i.as))
    (if h : j.as = i.as then eqToHom ⋯ else eqToHom ⋯ ≫ initial.to (f j.as)) (Cofan.inj c i.as) (Cofan.inj c j.as)

Tactic:
isPullback_of_cofan_isVanKampen hc i.as j.as

Premises used: CategoryTheory.isPullback_of_cofan_isVanKampen, CategoryTheory.Discrete.as
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
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
this : ∀ (i : Discrete ι), Subsingleton.{v + 1} (initial.{v, u} C ⟶ obj.{u_3, v, u_3, u} (Discrete.functor f) i)
h : initial.{v, u} C = if j.as = i.as then f i.as else initial.{v, u} 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:
convert! isPullback_of_cofan_isVanKampen hc i.as j.as

Premises used: CategoryTheory.isPullback_of_cofan_isVanKampen, CategoryTheory.Discrete.as
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
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
this : ∀ (i : Discrete ι), Subsingleton.{v + 1} (initial.{v, u} C ⟶ obj.{u_3, v, u_3, u} (Discrete.functor f) i)
⊢ initial.{v, u} C = if j.as = i.as then f i.as else initial.{v, u} C

Tactic:
(if_neg (mt Discrete.ext hi.symm)).symm

Premises used: mt, Ne.symm, CategoryTheory.Discrete.ext, Eq.symm, if_neg
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
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
this : ∀ (i : Discrete ι), Subsingleton.{v + 1} (initial.{v, u} C ⟶ obj.{u_3, v, u_3, u} (Discrete.functor f) i)
⊢ initial.{v, u} C = if j.as = i.as then f i.as else initial.{v, u} C

Tactic:
exact (if_neg (mt Discrete.ext hi.symm)).symm

Premises used: mt, Ne.symm, CategoryTheory.Discrete.ext, Eq.symm, if_neg
-- 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 j : Discrete ι
hi : i ≠ j
let let₁ let₂ : IsPullback (P := initial.{v, u} C) (initial.to (F.obj i)) (initial.to (F.obj j)) (c.ι.app i) (c.ι.app j)
let₃ :
  let f := 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)
let₄ :
  ∀ (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)
let₅ :
  ∀ (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)
let₆ :
  ∀ (f : ι → C) {c : Cocone.{u_3, v, u_3, u} (Discrete.functor f)} (hc : IsVanKampenColimit c)
    (this : ∀ (i : Discrete ι), Subsingleton.{v + 1} (initial.{v, u} C ⟶ obj.{u_3, v, u_3, u} (Discrete.functor f) i)),
    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)
h :
  ∀ (f : ι → C) {c : Cocone.{u_3, v, u_3, u} (Discrete.functor f)} (hc : IsVanKampenColimit c)
    (this : ∀ (i : Discrete ι), Subsingleton.{v + 1} (initial.{v, u} C ⟶ obj.{u_3, v, u_3, u} (Discrete.functor f) i)),
    initial.{v, u} C = if j.as = i.as then f i.as else initial.{v, u} C
⊢ IsPullback (P := initial.{v, u} C) (initial.to (F.obj i)) (initial.to (F.obj j)) (c.ι.app i) (c.ι.app j)

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
  have : ∀ i, Subsingleton (⊥_ C ⟶ (Discrete.functor f).obj i) := inferInstance
  convert! isPullback_of_cofan_isVanKampen hc i.as j.as
  exact (if_neg (mt Discrete.ext hi.symm)).symm

Premises used: mt, Ne.symm, CategoryTheory.Discrete.ext, Eq.symm, if_neg