-- Module: Mathlib.CategoryTheory.Limits.Shapes.StrictInitial
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasStrictTerminalObjects.{v, u} C
J : Type v
inst_2 : SmallCategory J
F : J ⥤ C
inst_3 : HasLimit F
i : J
H : (j : J) → j ≠ i → IsTerminal.{v, u} (F.obj j)
inst_4 : Subsingleton.{v + 1} (i ⟶ i)
refine_1 : (X : J) → Functor.obj (Functor.obj (Functor.const J) (F.1 i)) X ⟶ F.obj X
refine_2 :
  ∀ ⦃X Y : J⦄ (f : X ⟶ Y),
    Eq (α := Functor.obj (Functor.obj (Functor.const J) (F.1 i)) X ⟶ F.obj Y)
      (Functor.map (Functor.obj (Functor.const J) (F.1 i)) f ≫
        if h : Y = i then eqToHom ⋯ else (H Y h).from (Functor.obj (Functor.obj (Functor.const J) (F.1 i)) Y))
      ((if h : X = i then eqToHom ⋯ else (H X h).from (Functor.obj (Functor.obj (Functor.const J) (F.1 i)) X)) ≫
        F.map f)
refine_3 :
  limit.π F i ≫
      limit.lift F
        { pt := F.1 i,
          π :=
            {
              app := fun (j : J) ↦
                if h : j = i then eqToHom ⋯ else (H j h).from (Functor.obj (Functor.obj (Functor.const J) (F.1 i)) j),
              naturality := ⋯ } } =
    𝟙 (limit F)
refine_4 :
  Eq (α := F.obj i ⟶ F.obj i)
    (CategoryStruct.comp (Y := limit F)
        (limit.lift F
          { pt := F.1 i,
            π :=
              {
                app := fun (j : J) ↦
                  if h : j = i then eqToHom ⋯ else (H j h).from (Functor.obj (Functor.obj (Functor.const J) (F.1 i)) j),
                naturality := ⋯ } })
        (limit.π F i) :
      F.obj i ⟶ F.obj i)
    (𝟙 (F.obj i) : F.obj i ⟶ F.obj i)
refine_2₁ :
  ∀ ⦃X Y : J⦄ (f : X ⟶ Y),
    Eq (α := Functor.obj (Functor.obj (Functor.const J) (F.1 i)) X ⟶ F.obj Y)
      (Functor.map (Functor.obj (Functor.const J) (F.1 i)) f ≫
        if h : Y = i then eqToHom ⋯ else (H Y h).from (Functor.obj (Functor.obj (Functor.const J) (F.1 i)) Y))
      ((if h : X = i then eqToHom ⋯ else (H X h).from (Functor.obj (Functor.obj (Functor.const J) (F.1 i)) X)) ≫
        F.map f)
refine_3₁ :
  limit.π F i ≫
      limit.lift F
        { pt := F.1 i,
          π :=
            {
              app := fun (j : J) ↦
                if h : j = i then eqToHom ⋯ else (H j h).from (Functor.obj (Functor.obj (Functor.const J) (F.1 i)) j),
              naturality := ⋯ } } =
    𝟙 (limit F)
refine_4₁ :
  Eq (α := F.obj i ⟶ F.obj i)
    (CategoryStruct.comp (Y := limit F)
        (limit.lift F
          { pt := F.1 i,
            π :=
              {
                app := fun (j : J) ↦
                  if h : j = i then eqToHom ⋯ else (H j h).from (Functor.obj (Functor.obj (Functor.const J) (F.1 i)) j),
                naturality := ⋯ } })
        (limit.π F i) :
      F.obj i ⟶ F.obj i)
    (𝟙 (F.obj i) : F.obj i ⟶ F.obj i)
refine_3₂ :
  limit.π F i ≫
      limit.lift F
        { pt := F.1 i,
          π :=
            {
              app := fun (j : J) ↦
                if h : j = i then eqToHom ⋯ else (H j h).from (Functor.obj (Functor.obj (Functor.const J) (F.1 i)) j),
              naturality := ⋯ } } =
    𝟙 (limit F)
refine_4₂ refine_4₃ :
  Eq (α := F.obj i ⟶ F.obj i)
    (CategoryStruct.comp (Y := limit F)
        (limit.lift F
          { pt := F.1 i,
            π :=
              {
                app := fun (j : J) ↦
                  if h : j = i then eqToHom ⋯ else (H j h).from (Functor.obj (Functor.obj (Functor.const J) (F.1 i)) j),
                naturality := ⋯ } })
        (limit.π F i) :
      F.obj i ⟶ F.obj i)
    (𝟙 (F.obj i) : F.obj i ⟶ F.obj i)
⊢ IsIso (X := limit F) (limit.π F i)

Tactic:
classical
    refine ⟨⟨limit.lift _ ⟨_, ⟨?_, ?_⟩⟩, ?_, ?_⟩⟩
    · exact fun j =>
        dite (j = i)
          (fun h => eqToHom (by cases h; rfl))
          fun h => (H _ h).from _
    · intro j k f
      split_ifs with h h_1 h_1
      · cases h
        cases h_1
        obtain rfl : f = 𝟙 _ := Subsingleton.elim _ _
        simp
      · cases h
        haveI : IsIso (F.map f) := (H _ h_1).isIso_from _
        rw [← IsIso.comp_inv_eq]
        apply (H _ h_1).hom_ext
      · cases h_1
        apply (H _ h).hom_ext
      · apply (H _ h).hom_ext
    · ext
      rw [assoc, limit.lift_π]
      dsimp only
      split_ifs with h
      · cases h
        rw [id_comp, eqToHom_refl]
        exact comp_id _
      · apply (H _ h).hom_ext
    · simp

Premises used: CategoryTheory.Category.assoc, CategoryTheory.CategoryStruct.id, CategoryTheory.eqToHom_refl, CategoryTheory.Category.comp_id, CategoryTheory.IsIso.comp_inv_eq, Subsingleton.elim, CategoryTheory.Limits.limit.lift_π, rfl, CategoryTheory.Category.id_comp