diff --git a/Mathlib/CategoryTheory/Limits/VanKampen.lean b/Mathlib/CategoryTheory/Limits/VanKampen.lean
index 2c47495e645aa1..a89f2cf53055ae 100644
--- a/Mathlib/CategoryTheory/Limits/VanKampen.lean
+++ b/Mathlib/CategoryTheory/Limits/VanKampen.lean
@@ -686,9 +686,10 @@ theorem isVanKampenColimit_extendCofan {n : ℕ} (f : Fin (n + 1) → C)
       · simp only [Fin.cases_zero, m₁]
       · simp only [← m₂, colimit.ι_desc_assoc, Discrete.functor_obj,
           Cofan.mk_pt, Cofan.mk_ι_app, Fin.cases_succ]
-  induction' j using Fin.inductionOn with j _
-  · exact t₂' ⟨WalkingPair.left⟩
-  · have t₁' := (t₁ (Cofan.mk _ (Sigma.ι fun (j : Fin n) ↦ F.obj ⟨j.succ⟩)) (Discrete.natTrans
+  induction j using Fin.inductionOn with
+  | zero => exact t₂' ⟨WalkingPair.left⟩
+  | succ j _ =>
+    have t₁' := (t₁ (Cofan.mk _ (Sigma.ι fun (j : Fin n) ↦ F.obj ⟨j.succ⟩)) (Discrete.natTrans
       fun i ↦ α.app _) (Sigma.desc (fun j ↦ α.app _ ≫ c₁.inj _)) ?_
       (NatTrans.equifibered_of_discrete _)).mp ⟨coproductIsCoproduct _⟩ ⟨j⟩
     rotate_left