-- 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)
i : J
of :
  Eq (α :=
    (obj WithTerminal.liftFromOver c).obj (WithTerminal.of i) ⟶
      (WithTerminal.liftToTerminal c Over.mkIdTerminal ⋙ Over.forget F).obj WithTerminal.star)
    (CategoryStruct.comp (Y := (obj WithTerminal.liftFromOver c).obj WithTerminal.star)
      ((obj WithTerminal.liftFromOver c).map PUnit.unit)
      (Iso.hom
        ((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 WithTerminal.liftFromOver c).obj i ≅
                (WithTerminal.liftToTerminal c Over.mkIdTerminal ⋙ Over.forget F).obj i))
          WithTerminal.star)))
    (CategoryStruct.comp (Y :=
      (WithTerminal.liftToTerminal c Over.mkIdTerminal ⋙ Over.forget F).obj (WithTerminal.of i))
      (Iso.hom
        ((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 WithTerminal.liftFromOver c).obj i ≅
                (WithTerminal.liftToTerminal c Over.mkIdTerminal ⋙ Over.forget F).obj i))
          (WithTerminal.of i)))
      ((WithTerminal.liftToTerminal c Over.mkIdTerminal ⋙ Over.forget F).map PUnit.unit))
⊢ ∀ (f : WithTerminal.of i ⟶ WithTerminal.star),
    (obj WithTerminal.liftFromOver c).map f ≫
        Iso.hom
          ((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 WithTerminal.liftFromOver c).obj i ≅
                  (WithTerminal.liftToTerminal c Over.mkIdTerminal ⋙ Over.forget F).obj i))
            WithTerminal.star) =
      Iso.hom
          ((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 WithTerminal.liftFromOver c).obj i ≅
                  (WithTerminal.liftToTerminal c Over.mkIdTerminal ⋙ Over.forget F).obj i))
            (WithTerminal.of i)) ≫
        (WithTerminal.liftToTerminal c Over.mkIdTerminal ⋙ Over.forget F).map f

Tactic:
try rintro ⟨⟩