-- Mathlib/CategoryTheory/Limits/VanKampen.lean
theorem isVanKampenColimit_extendCofan {n : ℕ} (f : Fin (n + 1) → C)
    {c₁ : Cofan fun i : Fin n ↦ f i.succ} {c₂ : BinaryCofan (f 0) c₁.pt}
    (t₁ : IsVanKampenColimit c₁) (t₂ : IsVanKampenColimit c₂)
    [∀ {Z} (i : Z ⟶ c₂.pt), HasPullback c₂.inr i]
    [HasFiniteCoproducts C] :
    IsVanKampenColimit (extendCofan c₁ c₂)

Proof state:
case refine_3.succ
C : Type u
inst✝² : Category.{v, u} C
n : ℕ
f : Fin (n + 1) → C
c₁ : Cofan fun i => f i.succ
c₂ : BinaryCofan (f 0) c₁.pt
t₁ : IsVanKampenColimit c₁
t₂ : IsVanKampenColimit c₂
inst✝¹ : ∀ {Z : C} (i : Z ⟶ c₂.pt), HasPullback c₂.inr i
inst✝ : HasFiniteCoproducts C
F : Discrete (Fin (n + 1)) ⥤ C
c : Cocone F
α : F ⟶ Discrete.functor f
i : c.pt ⟶ (extendCofan c₁ c₂).pt
e : α ≫ (extendCofan c₁ c₂).ι = c.ι ≫ (Functor.const (Discrete (Fin (n + 1)))).map i
hα : NatTrans.Equifibered α
Hc : IsColimit c
t₂' :
  ∀ (j : Discrete WalkingPair),
    IsPullback ((BinaryCofan.mk (c.ι.app { as := 0 }) (Sigma.desc fun b => c.ι.app { as := b.succ })).ι.app j)
      ((mapPair (α.app { as := 0 }) (Sigma.desc fun b => α.app { as := b.succ } ≫ c₁.inj b)).app j) i (c₂.ι.app j)
j : Fin n
a✝ :
  IsPullback (c.ι.app { as := j.castSucc }) (α.app { as := j.castSucc }) i
    ((extendCofan c₁ c₂).ι.app { as := j.castSucc })
⊢ IsPullback (c.ι.app { as := j.succ }) (α.app { as := j.succ }) i ((extendCofan c₁ c₂).ι.app { as := j.succ })

Tactic:
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 _)) ?_
  (NatTrans.equifibered_of_discrete _)).mp ⟨coproductIsCoproduct _⟩ ⟨j⟩

Result:
case refine_3.succ.refine_2
C : Type u
inst✝² : Category.{v, u} C
n : ℕ
f : Fin (n + 1) → C
c₁ : Cofan fun i => f i.succ
c₂ : BinaryCofan (f 0) c₁.pt
t₁ : IsVanKampenColimit c₁
t₂ : IsVanKampenColimit c₂
inst✝¹ : ∀ {Z : C} (i : Z ⟶ c₂.pt), HasPullback c₂.inr i
inst✝ : HasFiniteCoproducts C
F : Discrete (Fin (n + 1)) ⥤ C
c : Cocone F
α : F ⟶ Discrete.functor f
i : c.pt ⟶ (extendCofan c₁ c₂).pt
e : α ≫ (extendCofan c₁ c₂).ι = c.ι ≫ (Functor.const (Discrete (Fin (n + 1)))).map i
hα : NatTrans.Equifibered α
Hc : IsColimit c
t₂' :
  ∀ (j : Discrete WalkingPair),
    IsPullback ((BinaryCofan.mk (c.ι.app { as := 0 }) (Sigma.desc fun b => c.ι.app { as := b.succ })).ι.app j)
      ((mapPair (α.app { as := 0 }) (Sigma.desc fun b => α.app { as := b.succ } ≫ c₁.inj b)).app j) i (c₂.ι.app j)
j : Fin n
a✝ :
  IsPullback (c.ι.app { as := j.castSucc }) (α.app { as := j.castSucc }) i
    ((extendCofan c₁ c₂).ι.app { as := j.castSucc })
t₁' :
  IsPullback
    ((Cofan.mk (colimit.cocone (Discrete.functor fun j => F.obj { as := j.succ })).1
            (Sigma.ι fun j => F.obj { as := j.succ })).ι.app
      { as := j })
    ((Discrete.natTrans fun i => α.app { as := i.as.succ }).app { as := j })
    (Sigma.desc fun j => α.app { as := j.succ } ≫ c₁.inj j) (c₁.ι.app { as := j })
⊢ IsPullback (c.ι.app { as := j.succ }) (α.app { as := j.succ }) i ((extendCofan c₁ c₂).ι.app { as := j.succ })

case refine_3.succ.refine_1
C : Type u
inst✝² : Category.{v, u} C
n : ℕ
f : Fin (n + 1) → C
c₁ : Cofan fun i => f i.succ
c₂ : BinaryCofan (f 0) c₁.pt
t₁ : IsVanKampenColimit c₁
t₂ : IsVanKampenColimit c₂
inst✝¹ : ∀ {Z : C} (i : Z ⟶ c₂.pt), HasPullback c₂.inr i
inst✝ : HasFiniteCoproducts C
F : Discrete (Fin (n + 1)) ⥤ C
c : Cocone F
α : F ⟶ Discrete.functor f
i : c.pt ⟶ (extendCofan c₁ c₂).pt
e : α ≫ (extendCofan c₁ c₂).ι = c.ι ≫ (Functor.const (Discrete (Fin (n + 1)))).map i
hα : NatTrans.Equifibered α
Hc : IsColimit c
t₂' :
  ∀ (j : Discrete WalkingPair),
    IsPullback ((BinaryCofan.mk (c.ι.app { as := 0 }) (Sigma.desc fun b => c.ι.app { as := b.succ })).ι.app j)
      ((mapPair (α.app { as := 0 }) (Sigma.desc fun b => α.app { as := b.succ } ≫ c₁.inj b)).app j) i (c₂.ι.app j)
j : Fin n
a✝ :
  IsPullback (c.ι.app { as := j.castSucc }) (α.app { as := j.castSucc }) i
    ((extendCofan c₁ c₂).ι.app { as := j.castSucc })
⊢ (Discrete.natTrans fun i => α.app { as := i.as.succ }) ≫ c₁.ι =
    (Cofan.mk (colimit.cocone (Discrete.functor fun j => F.obj { as := j.succ })).1
          (Sigma.ι fun j => F.obj { as := j.succ })).ι ≫
      (Functor.const (Discrete (Fin n))).map (Sigma.desc fun j => α.app { as := j.succ } ≫ c₁.inj j)

Proof state:
case refine_2.uniq.zero
C : Type u
inst✝² : Category.{v, u} C
n : ℕ
f : Fin (n + 1) → C
c₁ : Cofan fun i => f i.succ
c₂ : BinaryCofan (f 0) c₁.pt
t₁ : IsVanKampenColimit c₁
t₂ : IsVanKampenColimit c₂
inst✝¹ : ∀ {Z : C} (i : Z ⟶ c₂.pt), HasPullback c₂.inr i
inst✝ : HasFiniteCoproducts C
j : Fin (n + 1)
F' : Fin (n + 1) → C
c : Cocone (Discrete.functor F')
α : Discrete.functor F' ⟶ Discrete.functor f
i : c.pt ⟶ (extendCofan c₁ c₂).pt
e : α ≫ (extendCofan c₁ c₂).ι = c.ι ≫ (Functor.const (Discrete (Fin (n + 1)))).map i
hα : NatTrans.Equifibered α
Hc : IsColimit c
T : C
f₁ : F' 0 ⟶ T
f₂ : (∐ fun j => (Discrete.functor F').obj { as := j.succ }) ⟶ T
f₃ : (BinaryCofan.mk (c.ι.app { as := 0 }) (Sigma.desc fun b => c.ι.app { as := b.succ })).pt ⟶ T
m₁ : c.ι.app { as := 0 } ≫ f₃ = f₁
m₂ : (Sigma.desc fun b => c.ι.app { as := b.succ }) ≫ f₃ = f₂
⊢ c.ι.app { as := 0 } ≫ f₃ = Fin.cases f₁ (fun i => Sigma.ι (fun j => F' j.succ) i ≫ f₂) 0

Tactic:
simp only [Fin.cases_zero, m₁]

Result:
no goals

Proof state:
case refine_1.w.h.mk.left
C : Type u
inst✝² : Category.{v, u} C
n : ℕ
f : Fin (n + 1) → C
c₁ : Cofan fun i => f i.succ
c₂ : BinaryCofan (f 0) c₁.pt
t₁ : IsVanKampenColimit c₁
t₂ : IsVanKampenColimit c₂
inst✝¹ : ∀ {Z : C} (i : Z ⟶ c₂.pt), HasPullback c₂.inr i
inst✝ : HasFiniteCoproducts C
F : Discrete (Fin (n + 1)) ⥤ C
c : Cocone F
α : F ⟶ Discrete.functor f
i : c.pt ⟶ (extendCofan c₁ c₂).pt
e : α ≫ (extendCofan c₁ c₂).ι = c.ι ≫ (Functor.const (Discrete (Fin (n + 1)))).map i
hα : NatTrans.Equifibered α
Hc : IsColimit c
j : Fin (n + 1)
⊢ (mapPair (α.app { as := 0 }) (Sigma.desc fun b => α.app { as := b.succ } ≫ c₁.inj b) ≫ c₂.ι).app
      { as := WalkingPair.left } =
    ((BinaryCofan.mk (c.ι.app { as := 0 }) (Sigma.desc fun b => c.ι.app { as := b.succ })).ι ≫
          (Functor.const (Discrete WalkingPair)).map i).app
      { as := WalkingPair.left }

Tactic:
simpa only [pair_obj_left, Functor.const_obj_obj, pair_obj_right, Discrete.functor_obj,
  NatTrans.comp_app, mapPair_left, BinaryCofan.ι_app_left, BinaryCofan.mk_pt,
  BinaryCofan.mk_inl, Functor.const_map_app, extendCofan_pt,
  extendCofan_ι_app, Fin.cases_zero] using congr_app e ⟨0⟩

Result:
no goals