-- Mathlib/CategoryTheory/Limits/VanKampen.lean
theorem isPullback_of_cofan_isVanKampen [HasInitial C] {ι : Type*} {X : ι → C}
    {c : Cofan X} (hc : IsVanKampenColimit c) (i j : ι) [DecidableEq ι] :
    IsPullback (P := (if j = i then X i else ⊥_ C))
      (if h : j = i then eqToHom (if_pos h) else eqToHom (if_neg h) ≫ initial.to (X i))
      (if h : j = i then eqToHom ((if_pos h).trans (congr_arg X h.symm))
        else eqToHom (if_neg h) ≫ initial.to (X j))
      (Cofan.inj c i) (Cofan.inj c j)

Proof state:
case refine_2.refine_1
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasInitial C
ι : Type u_3
X : ι → C
c : Cofan X
hc : IsVanKampenColimit c
i j : ι
inst✝ : DecidableEq ι
⊢ ∀ (t : Cofan fun k => if k = i then X i else ⊥_ C) (j : ι),
    (Cofan.mk (X i) fun k => if h : k = i then eqToHom ⋯ else eqToHom ⋯ ≫ initial.to (X i)).inj j ≫
        (fun t => eqToHom ⋯ ≫ t.inj i) t =
      t.inj j

Tactic:
intro t j

Result:
case refine_2.refine_1
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasInitial C
ι : Type u_3
X : ι → C
c : Cofan X
hc : IsVanKampenColimit c
i j✝ : ι
inst✝ : DecidableEq ι
t : Cofan fun k => if k = i then X i else ⊥_ C
j : ι
⊢ (Cofan.mk (X i) fun k => if h : k = i then eqToHom ⋯ else eqToHom ⋯ ≫ initial.to (X i)).inj j ≫
      (fun t => eqToHom ⋯ ≫ t.inj i) t =
    t.inj j

Proof state:
case refine_2.refine_1
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasInitial C
ι : Type u_3
X : ι → C
c : Cofan X
hc : IsVanKampenColimit c
i j✝ : ι
inst✝ : DecidableEq ι
t : Cofan fun k => if k = i then X i else ⊥_ C
j : ι
⊢ (Cofan.mk (X i) fun k => if h : k = i then eqToHom ⋯ else eqToHom ⋯ ≫ initial.to (X i)).inj j ≫
      (fun t => eqToHom ⋯ ≫ t.inj i) t =
    t.inj j

Tactic:
simp only [Cofan.mk_pt, cofan_mk_inj]

Result:
case refine_2.refine_1
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasInitial C
ι : Type u_3
X : ι → C
c : Cofan X
hc : IsVanKampenColimit c
i j✝ : ι
inst✝ : DecidableEq ι
t : Cofan fun k => if k = i then X i else ⊥_ C
j : ι
⊢ (if h : j = i then eqToHom ⋯ else eqToHom ⋯ ≫ initial.to (X i)) ≫ eqToHom ⋯ ≫ t.inj i = t.inj j

Proof state:
case refine_2.refine_1.isFalse
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasInitial C
ι : Type u_3
X : ι → C
c : Cofan X
hc : IsVanKampenColimit c
i j✝ : ι
inst✝ : DecidableEq ι
t : Cofan fun k => if k = i then X i else ⊥_ C
j : ι
h✝ : ¬j = i
⊢ initial.to (X i) ≫ eqToHom ⋯ ≫ t.inj i = inv (eqToHom ⋯) ≫ t.inj j

Tactic:
exact initialIsInitial.hom_ext _ _

Result:
no goals

Proof state:
case refine_1.w.h.mk.isTrue
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasInitial C
ι : Type u_3
X : ι → C
c : Cofan X
hc : IsVanKampenColimit c
j : ι
inst✝ : DecidableEq ι
k : ι
⊢ eqToHom ⋯ ≫ c.ι.app { as := k } = eqToHom ⋯ ≫ c.inj k

Tactic:
rfl

Result:
no goals

Proof state:
case refine_2.refine_2
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasInitial C
ι : Type u_3
X : ι → C
c : Cofan X
hc : IsVanKampenColimit c
i j : ι
inst✝ : DecidableEq ι
⊢ ∀ (t : Cofan fun k => if k = i then X i else ⊥_ C)
    (m : (Cofan.mk (X i) fun k => if h : k = i then eqToHom ⋯ else eqToHom ⋯ ≫ initial.to (X i)).pt ⟶ t.pt),
    (∀ (j : ι),
        (Cofan.mk (X i) fun k => if h : k = i then eqToHom ⋯ else eqToHom ⋯ ≫ initial.to (X i)).inj j ≫ m = t.inj j) →
      m = (fun t => eqToHom ⋯ ≫ t.inj i) t

Tactic:
intro t m hm

Result:
case refine_2.refine_2
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasInitial C
ι : Type u_3
X : ι → C
c : Cofan X
hc : IsVanKampenColimit c
i j : ι
inst✝ : DecidableEq ι
t : Cofan fun k => if k = i then X i else ⊥_ C
m : (Cofan.mk (X i) fun k => if h : k = i then eqToHom ⋯ else eqToHom ⋯ ≫ initial.to (X i)).pt ⟶ t.pt
hm :
  ∀ (j : ι), (Cofan.mk (X i) fun k => if h : k = i then eqToHom ⋯ else eqToHom ⋯ ≫ initial.to (X i)).inj j ≫ m = t.inj j
⊢ m = (fun t => eqToHom ⋯ ≫ t.inj i) t

Proof state:
case refine_2.refine_2
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasInitial C
ι : Type u_3
X : ι → C
c : Cofan X
hc : IsVanKampenColimit c
i j : ι
inst✝ : DecidableEq ι
t : Cofan fun k => if k = i then X i else ⊥_ C
m : (Cofan.mk (X i) fun k => if h : k = i then eqToHom ⋯ else eqToHom ⋯ ≫ initial.to (X i)).pt ⟶ t.pt
hm :
  ∀ (j : ι), (Cofan.mk (X i) fun k => if h : k = i then eqToHom ⋯ else eqToHom ⋯ ≫ initial.to (X i)).inj j ≫ m = t.inj j
⊢ m = (fun t => eqToHom ⋯ ≫ t.inj i) t

Tactic:
simp [← hm i]

Result:
no goals

Proof state:
case refine_2
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasInitial C
ι : Type u_3
X : ι → C
c : Cofan X
hc : IsVanKampenColimit c
i j : ι
inst✝ : DecidableEq ι
⊢ IsColimit (Cofan.mk (X i) fun k => if h : k = i then eqToHom ⋯ else eqToHom ⋯ ≫ initial.to (X i))

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

Result:
case refine_2.refine_1
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasInitial C
ι : Type u_3
X : ι → C
c : Cofan X
hc : IsVanKampenColimit c
i j : ι
inst✝ : DecidableEq ι
⊢ ∀ (t : Cofan fun k => if k = i then X i else ⊥_ C) (j : ι),
    (Cofan.mk (X i) fun k => if h : k = i then eqToHom ⋯ else eqToHom ⋯ ≫ initial.to (X i)).inj j ≫
        (fun t => eqToHom ⋯ ≫ t.inj i) t =
      t.inj j

case refine_2.refine_2
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasInitial C
ι : Type u_3
X : ι → C
c : Cofan X
hc : IsVanKampenColimit c
i j : ι
inst✝ : DecidableEq ι
⊢ ∀ (t : Cofan fun k => if k = i then X i else ⊥_ C)
    (m : (Cofan.mk (X i) fun k => if h : k = i then eqToHom ⋯ else eqToHom ⋯ ≫ initial.to (X i)).pt ⟶ t.pt),
    (∀ (j : ι),
        (Cofan.mk (X i) fun k => if h : k = i then eqToHom ⋯ else eqToHom ⋯ ≫ initial.to (X i)).inj j ≫ m = t.inj j) →
      m = (fun t => eqToHom ⋯ ≫ t.inj i) t

Proof state:
case refine_2.refine_1
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasInitial C
ι : Type u_3
X : ι → C
c : Cofan X
hc : IsVanKampenColimit c
i j✝ : ι
inst✝ : DecidableEq ι
t : Cofan fun k => if k = i then X i else ⊥_ C
j : ι
⊢ (if h : j = i then eqToHom ⋯ else eqToHom ⋯ ≫ initial.to (X i)) ≫ eqToHom ⋯ ≫ t.inj i = t.inj j

Tactic:
split

Result:
case refine_2.refine_1.isTrue
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasInitial C
ι : Type u_3
X : ι → C
c : Cofan X
hc : IsVanKampenColimit c
i j✝ : ι
inst✝ : DecidableEq ι
t : Cofan fun k => if k = i then X i else ⊥_ C
j : ι
h✝ : j = i
⊢ eqToHom ⋯ ≫ eqToHom ⋯ ≫ t.inj i = t.inj j

case refine_2.refine_1.isFalse
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasInitial C
ι : Type u_3
X : ι → C
c : Cofan X
hc : IsVanKampenColimit c
i j✝ : ι
inst✝ : DecidableEq ι
t : Cofan fun k => if k = i then X i else ⊥_ C
j : ι
h✝ : ¬j = i
⊢ (eqToHom ⋯ ≫ initial.to (X i)) ≫ eqToHom ⋯ ≫ t.inj i = t.inj j

Proof state:
case refine_2.refine_1.isTrue
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasInitial C
ι : Type u_3
X : ι → C
c : Cofan X
hc : IsVanKampenColimit c
j✝ : ι
inst✝ : DecidableEq ι
j : ι
t : Cofan fun k => if k = j then X j else ⊥_ C
⊢ eqToHom ⋯ ≫ eqToHom ⋯ ≫ t.inj j = t.inj j

Tactic:
simp

Result:
no goals

Proof state:
case refine_1.w.h.mk
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasInitial C
ι : Type u_3
X : ι → C
c : Cofan X
hc : IsVanKampenColimit c
i j : ι
inst✝ : DecidableEq ι
k : ι
⊢ ((Discrete.natTrans fun k =>
            if h : k.as = i then eqToHom ⋯ else eqToHom ⋯ ≫ initial.to ((Discrete.functor X).obj k)) ≫
          c.ι).app
      { as := k } =
    ((Cofan.mk (X i) fun k => if h : k = i then eqToHom ⋯ else eqToHom ⋯ ≫ initial.to (X i)).ι ≫
          (Functor.const (Discrete ι)).map (c.inj i)).app
      { 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]

Result:
case refine_1.w.h.mk
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasInitial C
ι : Type u_3
X : ι → C
c : Cofan X
hc : IsVanKampenColimit c
i j : ι
inst✝ : DecidableEq ι
k : ι
⊢ (if h : k = i then eqToHom ⋯ else eqToHom ⋯ ≫ initial.to (X k)) ≫ c.ι.app { as := k } =
    (if h : k = i then eqToHom ⋯ else eqToHom ⋯ ≫ initial.to (X i)) ≫ c.inj i