-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.EquifiberedLimits (goal)
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)
⊢ ∀ (f : Quiver.Hom.{v_1, u_1} (V := WithTerminal J) WithTerminal.star 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.star) ≫
        (WithTerminal.liftToTerminal c Over.mkIdTerminal ⋙ Over.forget F).map f
have star : Eq (α :=
  (obj WithTerminal.liftFromOver c).obj WithTerminal.star ⟶
    (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.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.star))
    ((WithTerminal.liftToTerminal c Over.mkIdTerminal ⋙ Over.forget F).map PUnit.unit))
Tactic: try rintro ⟨⟩