-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.EquifiberedLimits
Goal:
J_1 : Type u_1
K : Type u_2
C : Type u_3
D : Type u_4
ι : Type u_5
inst : Category.{v_1, u_1} J_1
inst_1 : Category.{v_2, u_3} C
inst_2 : Category.{v_3, u_2} K
inst_3 : Category.{v_4, u_4} D
F : Functor.{v_2, v_4, u_3, u_4} C D
inst_4 : ∀ (a b : C), HasCoproductsOfShape.{v_2, u_4, v_4} (a ⟶ b) D
J : Type u_1
inst_5 : Category.{v_1, u_1} J
hJ : IsConnected.{v_1, u_1} J
G : Over F
h : limitsOfShape (fun (f : Over F) ↦ Equifibered f.hom) J G
i j : C
f : i ⟶ j
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
s : PullbackCone (G.hom.app j) (F.map f)
hcᵢ : IsLimit ((Over.forget F ⋙ obj (evaluation C D) i).mapCone { pt := G, π := α : Cone c }) :=
  isLimitOfPreserves (Over.forget F ⋙ obj (evaluation C D) i) hc
hcⱼ : IsLimit ((Over.forget F ⋙ obj (evaluation C D) j).mapCone { pt := G, π := α : Cone c }) :=
  isLimitOfPreserves (Over.forget F ⋙ obj (evaluation C D) j) hc
l : s.pt ⟶ G.left.obj i :=
  hcᵢ.lift
    { pt := s.1,
      π := { app := fun (k : J) ↦ ⋯.lift (s.fst ≫ (Over.Hom.left (α.app k)).app j) s.snd ⋯, naturality := ⋯ } }
refine_1 :
  ∀ (k : J),
    (l ≫ (PullbackCone.mk (G.left.map f) (G.hom.app i) ⋯).fst) ≫
        ((Over.forget F ⋙ obj (evaluation C D) j).mapCone { pt := G, π := α : Cone c }).π.app k =
      s.fst ≫ ((Over.forget F ⋙ obj (evaluation C D) j).mapCone { pt := G, π := α }).π.app k
refine_2 : l ≫ (PullbackCone.mk (G.left.map f) (G.hom.app i) ⋯).snd = s.snd
refine_3 :
  ∀ {m : s.pt ⟶ (PullbackCone.mk (G.left.map f) (G.hom.app i) ⋯).pt}
    (hm₁ : m ≫ (PullbackCone.mk (G.left.map f) (G.hom.app i) ⋯).fst = s.fst)
    (hm₂ : m ≫ (PullbackCone.mk (G.left.map f) (G.hom.app i) ⋯).snd = s.snd) (k : J),
    (m ≫ ((Over.forget F ⋙ obj (evaluation C D) i).mapCone { pt := G, π := α : Cone c }).π.app k) ≫
        ({ diag := c, π := α, isLimit := hc : LimitPresentation J G }.diag.obj k).left.map f =
      app
          (Cone.π
            { pt := s.1,
              π := { app := fun (k : J) ↦ ⋯.lift (s.fst ≫ (Over.Hom.left (α.app k)).app j) s.snd ⋯, naturality := ⋯ } })
          k ≫
        ({ diag := c, π := α, isLimit := hc : LimitPresentation J G }.diag.obj k).left.map f
refine_4 :
  ∀ {m : s.pt ⟶ (PullbackCone.mk (G.left.map f) (G.hom.app i) ⋯).pt}
    (hm₁ : m ≫ (PullbackCone.mk (G.left.map f) (G.hom.app i) ⋯).fst = s.fst)
    (hm₂ : m ≫ (PullbackCone.mk (G.left.map f) (G.hom.app i) ⋯).snd = s.snd) (k : J),
    (m ≫ ((Over.forget F ⋙ obj (evaluation C D) i).mapCone { pt := G, π := α : Cone c }).π.app k) ≫
        ({ diag := c, π := α, isLimit := hc : LimitPresentation J G }.diag.obj k).hom.app i =
      app
          (Cone.π
            { pt := s.1,
              π := { app := fun (k : J) ↦ ⋯.lift (s.fst ≫ (Over.Hom.left (α.app k)).app j) s.snd ⋯, naturality := ⋯ } })
          k ≫
        ({ diag := c, π := α, isLimit := hc : LimitPresentation J G }.diag.obj k).hom.app i
⊢ { l : s.pt ⟶ (PullbackCone.mk (G.left.map f) (G.hom.app i) ⋯).pt //
    l ≫ (PullbackCone.mk (G.left.map f) (G.hom.app i) ⋯).fst = s.fst ∧
      l ≫ (PullbackCone.mk (G.left.map f) (G.hom.app i) ⋯).snd = s.snd ∧
        ∀ {m : s.pt ⟶ (PullbackCone.mk (G.left.map f) (G.hom.app i) ⋯).pt},
          m ≫ (PullbackCone.mk (G.left.map f) (G.hom.app i) ⋯).fst = s.fst →
            m ≫ (PullbackCone.mk (G.left.map f) (G.hom.app i) ⋯).snd = s.snd → m = l }

Tactic:
refine ⟨l, hcⱼ.hom_ext fun k ↦ ?_, ?_, fun {m} hm₁ hm₂ ↦ hcᵢ.hom_ext
    fun k ↦ ((H k f).hom_ext ?_ ?_).trans (hcᵢ.fac ⟨_, _⟩ k).symm⟩