-- 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)
a : J
⊢ Eq (α :=
    obj
        (obj (const (WithTerminal J))
          (Cone.pt (F := 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 }))))
        (WithTerminal.of a) ⟶
      (WithTerminal.liftToTerminal c Over.mkIdTerminal ⋙ Over.forget F).obj (WithTerminal.of a))
    (app
      (Cone.π
        (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 })))
      (WithTerminal.of a))
    (Iso.hom
        (Iso.refl
          (Cone.pt (F := 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 })))) ≫
      app
        (Cone.π
          (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 := ⋯ } }))
        (WithTerminal.of a))

Tactic:
simp