-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.EquifiberedLimits
Goal:
J : Type u_1
K : Type u_2
C : Type u_3
D : Type u_4
ι : Type u_5
inst_1 : Category.{v_1, u_1} J
inst_2 : Category.{v_2, u_3} C
inst_3 : Category.{v_3, u_2} K
inst_4 : Category.{v_4, u_4} D
F : Functor.{v_2, v_4, u_3, u_4} C D
inst_5 : ∀ (a b : C), HasCoproductsOfShape.{v_2, u_4, v_4} (a ⟶ b) D
this :
  ∀ {J : Type u_1} [inst : Category.{v_1, u_1} J] (hJ : IsConnected.{v_1, u_1} J),
    IsClosedUnderLimitsOfShape (C := Over F) (fun (f : Over F) ↦ Equifibered f.hom) J
hJ : ¬IsConnected.{v_1, u_1} J
G : Over F
h : limitsOfShape (fun (f : Over F) ↦ Equifibered f.hom) J G
U V : C
f : U ⟶ V
c : J ⥤ Over F
α : obj (const J) G ⟶ c
hc : IsLimit { pt := G, π := α : Cone c }
H : ∀ (j : J), Equifibered ({ diag := c, π := α, isLimit := hc : LimitPresentation J G }.diag.obj j).hom
hα : ∀ (i j : J) (f : i ⟶ j), α.app i ≫ c.map f = α.app j
hc' : IsLimit (obj (Equivalence.functor WithTerminal.coneEquiv) { pt := G, π := α : Cone c })
inst : IsConnected.{v_1, u_1} (WithTerminal J)
refine_1 : obj WithTerminal.liftFromOver c ≅ WithTerminal.liftToTerminal c Over.mkIdTerminal ⋙ Over.forget F
refine_2 :
  Iso (C := Cone (WithTerminal.liftToTerminal c Over.mkIdTerminal ⋙ Over.forget F))
    (obj
      (Cone.postcompose
        (Iso.hom
          (NatIso.ofComponents
            (fun (i : WithTerminal J) ↦
              WithTerminal.casesOn (motive := fun (x : WithTerminal J) ↦
                (obj WithTerminal.liftFromOver c).obj x ≅
                  (WithTerminal.liftToTerminal c Over.mkIdTerminal ⋙ Over.forget F).obj x)
                i (fun (x : J) ↦ Iso.refl ((obj WithTerminal.liftFromOver c).obj (WithTerminal.of x)))
                (Iso.refl ((obj WithTerminal.liftFromOver c).obj WithTerminal.star)))
            ⋯)))
      (obj (Equivalence.functor WithTerminal.coneEquiv) { pt := G, π := α : Cone c }))
    (mapCone (Over.forget F)
      { pt := G,
        π :=
          {
            app := fun (i : WithTerminal J) ↦
              WithTerminal.casesOn (motive := fun (x : WithTerminal J) ↦
                obj (obj (const (WithTerminal J)) G) x ⟶ (WithTerminal.liftToTerminal c Over.mkIdTerminal).obj x) i
                α.app
                (IsTerminal.from Over.mkIdTerminal
                  (obj (C := WithTerminal J) (obj (const (WithTerminal J)) G) WithTerminal.star)),
            naturality := ⋯ } })
⊢ IsLimit (J := WithTerminal J) (F := WithTerminal.liftToTerminal c Over.mkIdTerminal ⋙ Over.forget F)
    (mapCone (Over.forget F)
      { pt := G,
        π :=
          {
            app := fun (i : WithTerminal J) ↦
              WithTerminal.casesOn (motive := fun (x : WithTerminal J) ↦
                obj (obj (const (WithTerminal J)) G) x ⟶ (WithTerminal.liftToTerminal c Over.mkIdTerminal).obj x) i
                α.app
                (IsTerminal.from Over.mkIdTerminal
                  (obj (C := WithTerminal J) (obj (const (WithTerminal J)) G) WithTerminal.star)),
            naturality := ⋯ } })

Tactic:
refine IsLimit.equivOfNatIsoOfIso ?_ _ _ ?_ (WithTerminal.isLimitEquiv.symm hc)

Premises used: CategoryTheory.WithTerminal.isLimitEquiv, Equiv.symm, DFunLike.coe, CategoryTheory.Limits.IsLimit.equivOfNatIsoOfIso