-- 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₁ : IsUniversalColimit c₁
t₂ : IsUniversalColimit c₂
inst_1 : ∀ {Z : C} (i : Z ⟶ c₂.pt), HasPullback c₂.inr i
F' : Fin (n + 1) → C
c : Cocone.{0, v, 0, u} (Discrete.functor F')
α : Quiver.Hom (V := Functor.{0, v, 0, u} (Discrete (Fin (n + 1))) C) (Discrete.functor 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 α
H : ∀ (j : Discrete (Fin (n + 1))), IsPullback (c.ι.app j) (α.app j) i ((extendCofan c₁ c₂).ι.app j)
H₁ :
  IsColimit.{0, v, 0, u} (J := Discrete (Fin n)) (F :=
    Discrete.functor fun (j : Fin n) ↦ obj.{0, v, 0, u} (Discrete.functor F') { as := j.succ : Discrete (Fin (n + 1)) })
    (Cofan.mk (pullback c₂.inr i) fun (j : Fin n) ↦
      pullback.lift (α.app { as := j.succ } ≫ c₁.inj j) (c.ι.app { as := j.succ }) ⋯)
H₂ :
  IsColimit (F := pair (obj.{0, v, 0, u} (Discrete.functor F') { as := 0 }) (pullback c₂.inr i))
    (BinaryCofan.mk (c.ι.app { as := 0 : Discrete (Fin (n + 1)) }) (pullback.snd c₂.inr i))
j : Fin (n + 1)
refine_4 :
  Eq.{v + 1} (α := F' 0 ⟶ c.pt)
    (Fin.cases (motive := fun (x : Fin (n + 1)) ↦ F' x ⟶ c.pt) (c.ι.app { as := 0 })
        (fun (i : Fin n) ↦ c.ι.app { as := i.succ }) 0 :
      F' 0 ⟶ c.pt)
    (c.ι.app { as := 0 } :
      obj.{0, v, 0, u} (C := Discrete (Fin (n + 1))) (Discrete.functor fun (i : Fin (n + 1)) ↦ F' i) { as := 0 } ⟶
        obj.{0, v, 0, u} (C := Discrete (Fin (n + 1))) (obj (const (Discrete (Fin (n + 1)))) c.pt)
          { as := 0 : Discrete (Fin (n + 1)) })
⊢ Eq.{v + 1} (α := F' j ⟶ c.pt)
    (Fin.cases (motive := fun (x : Fin (n + 1)) ↦ F' x ⟶ c.pt) (c.ι.app { as := 0 })
        (fun (i : Fin n) ↦ c.ι.app { as := i.succ }) j :
      F' j ⟶ c.pt)
    (c.ι.app { as := j } :
      obj.{0, v, 0, u} (Discrete.functor fun (i : Fin (n + 1)) ↦ F' i) { as := j : Discrete (Fin (n + 1)) } ⟶
        obj.{0, v, 0, u} (obj (const (Discrete (Fin (n + 1)))) c.pt) { as := j : Discrete (Fin (n + 1)) })
have refine_4₁ : ∀ (i : Fin n),
  Eq.{v + 1} (α := F' i.castSucc ⟶ c.pt)
      (Fin.cases (motive := fun (x : Fin (n + 1)) ↦ F' x ⟶ c.pt) (c.ι.app { as := 0 })
          (fun (i : Fin n) ↦ c.ι.app { as := i.succ }) i.castSucc :
        F' i.castSucc ⟶ c.pt)
      (c.ι.app { as := i.castSucc } :
        obj.{0, v, 0, u} (Discrete.functor fun (i : Fin (n + 1)) ↦ F' i) { as := i.castSucc : Discrete (Fin (n + 1)) } ⟶
          obj.{0, v, 0, u} (obj (const (Discrete (Fin (n + 1)))) c.pt) { as := i.castSucc : Discrete (Fin (n + 1)) }) →
    Eq.{v + 1} (α := F' i.succ ⟶ c.pt)
      (Fin.cases (motive := fun (x : Fin (n + 1)) ↦ F' x ⟶ c.pt) (c.ι.app { as := 0 })
          (fun (i : Fin n) ↦ c.ι.app { as := i.succ }) i.succ :
        F' i.succ ⟶ c.pt)
      (c.ι.app { as := i.succ } :
        obj.{0, v, 0, u} (Discrete.functor fun (i : Fin (n + 1)) ↦ F' i) { as := i.succ : Discrete (Fin (n + 1)) } ⟶
          obj.{0, v, 0, u} (obj (const (Discrete (Fin (n + 1)))) c.pt) { as := i.succ : Discrete (Fin (n + 1)) })
Tactic: induction j using Fin.inductionOn
Cleared hypotheses: j