awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
⊢ 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:
simp
-- 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)
⊢ obj WithTerminal.liftFromOver c ≅ WithTerminal.liftToTerminal c Over.mkIdTerminal ⋙ Over.forget F

Tactic:
exact NatIso.ofComponents (fun i ↦ i.casesOn (fun _ ↦ .refl _) (.refl _)) <| by
          rintro (i | _) (j | _) <;> (try rintro ⟨⟩) <;> simp

Premises used: CategoryTheory.NatIso.ofComponents
-- 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)
⊢ 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 := ⋯ } })

Tactic:
exact Cone.ext (.refl _) (by rintro ⟨⟩ <;> simp)

Premises used: CategoryTheory.Iso.refl, CategoryTheory.Limits.Cone.ext
-- 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)
⊢ IsPullback (G.left.map f) (G.hom.app U) (G.hom.app V) (F.map f)

Tactic:
exact (this (J := WithTerminal J) inst).1 G ⟨⟨WithTerminal.liftToTerminal c Over.mkIdTerminal,
      { app i := i.casesOn α.app (Over.mkIdTerminal.from _) }, isLimitOfReflects (Over.forget _) (by
      refine IsLimit.equivOfNatIsoOfIso ?_ _ _ ?_ (WithTerminal.isLimitEquiv.symm hc)
      · exact NatIso.ofComponents (fun i ↦ i.casesOn (fun _ ↦ .refl _) (.refl _)) <| by
          rintro (i | _) (j | _) <;> (try rintro ⟨⟩) <;> simp
      · exact Cone.ext (.refl _) (by rintro ⟨⟩ <;> simp))⟩, fun i ↦
        i.casesOn H (.of_isIso (𝟙 F))⟩ f

Premises used: CategoryTheory.Limits.isLimitOfReflects, CategoryTheory.Over.forget, CategoryTheory.Limits.LimitPresentation.mk, CategoryTheory.WithTerminal.liftToTerminal, Nonempty.intro, CategoryTheory.NatTrans.mk, CategoryTheory.ObjectProperty.LimitOfShape.mk, CategoryTheory.Over.mkIdTerminal, CategoryTheory.WithTerminal.casesOn, CategoryTheory.ObjectProperty.IsClosedUnderLimitsOfShape.limitsOfShape_le
-- 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
⊢ G.left.map f ≫ G.hom.app j = G.hom.app i ≫ F.map f

Tactic:
simp
-- 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
refine :
  (G : Over F) →
    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)) →
                    { 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 }
⊢ IsClosedUnderLimitsOfShape (C := Over F) (fun (f : Over F) ↦ Equifibered f.hom) J

Tactic:
refine ⟨fun G ⟨⟨c, α, hc⟩, H⟩ i j f ↦ ⟨⟨by simp⟩, ⟨Limits.PullbackCone.isLimitAux' _ fun s ↦ ?_⟩⟩⟩
-- 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
k : J
⊢ (s.fst ≫ (Over.Hom.left (α.app k)).app j) ≫
      ({ diag := c, π := α, isLimit := hc : LimitPresentation J G }.diag.obj k).hom.app j =
    s.snd ≫ F.map f

Tactic:
simp [← s.condition, ← NatTrans.comp_app]

Premises used: CategoryTheory.Limits.PullbackCone.condition, CategoryTheory.NatTrans.comp_app
-- 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
k₁ k₂ : J
fk₁k₂ : k₁ ⟶ k₂
⊢ Eq (α :=
    obj.{v_1, v_4, u_1, u_4} (obj (const J) s.1) k₁ ⟶
      ({ diag := c, π := α, isLimit := hc : LimitPresentation J G }.diag.obj k₂).left.obj j)
    ((Functor.map (obj (const J) s.1) fk₁k₂ ≫
        (fun (k : J) ↦ ⋯.lift (s.fst ≫ (Over.Hom.left (α.app k)).app j) s.snd ⋯) k₂) ≫
      ({ diag := c, π := α, isLimit := hc : LimitPresentation J G }.diag.obj k₂).left.map f)
    (((fun (k : J) ↦ ⋯.lift (s.fst ≫ (Over.Hom.left (α.app k)).app j) s.snd ⋯) k₁ ≫
        (c ⋙ Over.forget F ⋙ obj (evaluation C D) i).map fk₁k₂) ≫
      ({ diag := c, π := α, isLimit := hc : LimitPresentation J G }.diag.obj k₂).left.map f)

Tactic:
simp [← NatTrans.naturality, ← NatTrans.comp_app, ← Over.comp_left]

Premises used: CategoryTheory.Over.comp_left, CategoryTheory.NatTrans.naturality, CategoryTheory.NatTrans.comp_app
-- 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
k₁ k₂ : J
fk₁k₂ : k₁ ⟶ k₂
⊢ Eq (α := obj.{v_1, v_4, u_1, u_4} (obj (const J) s.1) k₁ ⟶ F.obj i)
    ((Functor.map (obj (const J) s.1) fk₁k₂ ≫
        (fun (k : J) ↦ ⋯.lift (s.fst ≫ (Over.Hom.left (α.app k)).app j) s.snd ⋯) k₂) ≫
      ({ diag := c, π := α, isLimit := hc : LimitPresentation J G }.diag.obj k₂).hom.app i)
    (((fun (k : J) ↦ ⋯.lift (s.fst ≫ (Over.Hom.left (α.app k)).app j) s.snd ⋯) k₁ ≫
        (c ⋙ Over.forget F ⋙ obj (evaluation C D) i).map fk₁k₂) ≫
      ({ diag := c, π := α, isLimit := hc : LimitPresentation J G }.diag.obj k₂).hom.app i)

Tactic:
simp [← NatTrans.comp_app]

Premises used: CategoryTheory.NatTrans.comp_app
-- 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 := ⋯ } }
k : J
⊢ app
        (Cone.π
          { pt := s.1,
            π := { app := fun (k : J) ↦ ⋯.lift (s.fst ≫ (Over.Hom.left (α.app k)).app j) s.snd ⋯, naturality := ⋯ } })
        k ≫
      (c.obj k).left.map f =
    s.fst ≫ (Over.Hom.left (α.app k)).app j

Tactic:
simp
-- 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 := ⋯ } }
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

Tactic:
simpa [Category.assoc, NatTrans.naturality] using (hcᵢ.fac_assoc _ _ _).trans (by simp)

Premises used: CategoryTheory.Category.assoc, CategoryTheory.NatTrans.naturality, CategoryTheory.Limits.IsLimit.fac_assoc, Eq.trans
-- 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_2 : l ≫ G.hom.app i = s.snd
⊢ l ≫ (PullbackCone.mk (G.left.map f) (G.hom.app i) ⋯).snd = s.snd

Tactic:
dsimp
-- 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 := ⋯ } }
⊢ Nonempty J

Tactic:
inferInstance

Premises used: inferInstance
-- 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_2 : ∀ (k : J), l ≫ G.hom.app i = s.snd
⊢ l ≫ G.hom.app i = s.snd

Tactic:
obtain ⟨k⟩ : Nonempty J := inferInstance

Premises used: Nonempty