-- 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_2.uniq
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₂
j : Fin (n + 1)
⊢ c.ι.app { as := j } ≫ f₃ = Fin.cases f₁ (fun i => Sigma.ι (fun j => F' j.succ) i ≫ f₂) j

Tactic:
induction' j using Fin.inductionOn with j _

Result:
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

case refine_2.uniq.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
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₂
j : Fin n
a✝ : c.ι.app { as := j.castSucc } ≫ f₃ = Fin.cases f₁ (fun i => Sigma.ι (fun j => F' j.succ) i ≫ f₂) j.castSucc
⊢ c.ι.app { as := j.succ } ≫ f₃ = Fin.cases f₁ (fun i => Sigma.ι (fun j => F' j.succ) i ≫ f₂) j.succ

Proof state:
case h_obj
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)
F' : Fin (n + 1) → C := F.obj ∘ Discrete.mk
⊢ ∀ (X : Discrete (Fin (n + 1))), F.obj X = (Discrete.functor F').obj X

Tactic:
exact fun i ↦ rfl

Result:
no goals

Proof state:
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)
F' : Fin (n + 1) → C := F.obj ∘ Discrete.mk
⊢ F = Discrete.functor F'

Tactic:
apply Functor.hext

Result:
case h_obj
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)
F' : Fin (n + 1) → C := F.obj ∘ Discrete.mk
⊢ ∀ (X : Discrete (Fin (n + 1))), F.obj X = (Discrete.functor F').obj X

case h_map
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)
F' : Fin (n + 1) → C := F.obj ∘ Discrete.mk
⊢ ∀ (X Y : Discrete (Fin (n + 1))) (f : X ⟶ Y), HEq (F.map f) ((Discrete.functor F').map f)

Proof state:
case h_map.mk.mk.up.up
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)
F' : Fin (n + 1) → C := F.obj ∘ Discrete.mk
i : Fin (n + 1)
⊢ HEq (F.map { down := { down := ⋯ } }) ((Discrete.functor F').map { down := { down := ⋯ } })

Tactic:
simp [F']

Result:
no goals