awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equifibered
Goal:
J : Type u_1
K : Type u_2
C : Type u_3
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_3} C
inst_2 : Category.{v_3, u_2} K
F G : Functor.{v_1, v_2, u_1, u_3} J C
α : F ⟶ G
hα : Coequifibered α
H : Functor.{v_3, v_1, u_2, u_1} K J
⊢ Coequifibered (H.whiskerLeft α)

Tactic:
fun _ _ f => hα (H.map f)

Premises used: CategoryTheory.Functor.map, CategoryTheory.NatTrans.Coequifibered
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equifibered
Goal:
C : Type u_3
inst : Category.{v_2, u_3} C
ι : Type u_6
F G : Functor.{u_6, v_2, u_6, u_3} (Discrete ι) C
α : F ⟶ G
i : ι
simp :
  IsPullback (𝟙 (F.obj { as := i })) (α.app { as := i : Discrete ι }) (α.app { as := i : Discrete ι })
    (𝟙 (G.obj { as := i }))
⊢ IsPullback
    (F.map
      { down := { down := ⋯ : PLift ({ as := i : Discrete ι }.as = { as := i : Discrete ι }.as) } :
        ULift.{u_6, 0} (PLift ({ as := i : Discrete ι }.as = { as := i : Discrete ι }.as)) })
    (α.app { as := i }) (α.app { as := i })
    (G.map
      { down := { down := ⋯ : PLift ({ as := i : Discrete ι }.as = { as := i : Discrete ι }.as) } :
        ULift.{u_6, 0} (PLift ({ as := i : Discrete ι }.as = { as := i : Discrete ι }.as)) })

Tactic:
simp only [Discrete.functor_map_id]

Premises used: CategoryTheory.Discrete.functor_map_id
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equifibered
Goal:
C : Type u_3
inst : Category.{v_2, u_3} C
ι : Type u_6
F G : Functor.{u_6, v_2, u_6, u_3} (Discrete ι) C
α : F ⟶ G
i : ι
rw : α.app { as := i } = α.app { as := i : Discrete ι } ≫ 𝟙 (G.obj { as := i : Discrete ι })
rw₁ rw₂ : Eq (α := F.obj { as := i : Discrete ι } ⟶ G.obj { as := i }) (α.app { as := i }) (α.app { as := i })
⊢ 𝟙 (F.obj { as := i : Discrete ι }) ≫ α.app { as := i : Discrete ι } =
    α.app { as := i : Discrete ι } ≫ 𝟙 (G.obj { as := i })

Tactic:
rw [Category.id_comp, Category.comp_id]

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equifibered
Goal:
C : Type u_3
inst : Category.{v_2, u_3} C
ι : Type u_6
F G : Functor.{u_6, v_2, u_6, u_3} (Discrete ι) C
α : F ⟶ G
i : ι
⊢ IsPullback (𝟙 (F.obj { as := i })) (α.app { as := i : Discrete ι }) (α.app { as := i : Discrete ι })
    (𝟙 (G.obj { as := i }))

Tactic:
exact IsPullback.of_horiz_isIso ⟨by rw [Category.id_comp, Category.comp_id]⟩

Premises used: CategoryTheory.CommSq.mk, CategoryTheory.IsPullback.of_horiz_isIso
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equifibered
Goal:
J : Type u_1
C : Type u_3
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_3} C
F G : Functor.{v_1, v_2, u_1, u_3} J C
α : F ⟶ G
hα : Coequifibered α
⊢ Equifibered (NatTrans.op α)

Tactic:
fun _ _ f ↦ (hα f.unop).op

Premises used: Quiver.Hom.op, Quiver.Hom.unop, CategoryTheory.NatTrans.Equifibered, CategoryTheory.IsPushout.op
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equifibered
Goal:
J : Type u_1
C : Type u_3
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_3} C
F G : Functor.{v_1, v_2, u_1, u_3} J C
α : F ⟶ G
hα : Equifibered α
⊢ Coequifibered (NatTrans.op α)

Tactic:
fun _ _ f ↦ (hα f.unop).op

Premises used: CategoryTheory.IsPullback.op, Quiver.Hom.op, Quiver.Hom.unop, CategoryTheory.NatTrans.Coequifibered
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equifibered
Goal:
J : Type u_1
C : Type u_3
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_3} C
F G : Functor.{v_1, v_2, u_1, u_3} Jᵒᵖ Cᵒᵖ
α : F ⟶ G
hα : Coequifibered α
⊢ Equifibered (NatTrans.unop α)

Tactic:
fun _ _ f ↦ (hα f.op).unop

Premises used: Quiver.Hom.op, Quiver.Hom.unop, CategoryTheory.IsPushout.unop, CategoryTheory.NatTrans.Equifibered
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equifibered
Goal:
J : Type u_1
C : Type u_3
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_3} C
F G : Functor.{v_1, v_2, u_1, u_3} Jᵒᵖ Cᵒᵖ
α : F ⟶ G
hα : Equifibered α
⊢ Coequifibered (NatTrans.unop α)

Tactic:
fun _ _ f ↦ (hα f.op).unop

Premises used: Quiver.Hom.op, Quiver.Hom.unop, CategoryTheory.IsPullback.unop, CategoryTheory.NatTrans.Coequifibered
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equifibered
Goal:
J : Type u_1
C : Type u_3
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_3} C
F G : Functor.{v_1, v_2, u_1, u_3} Jᵒᵖ C
α : F ⟶ G
hα : Equifibered α
⊢ Coequifibered (NatTrans.rightOp α)

Tactic:
fun _ _ f ↦ (hα f.op).op

Premises used: CategoryTheory.IsPullback.op, Quiver.Hom.op, CategoryTheory.NatTrans.Coequifibered
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equifibered
Goal:
J : Type u_1
C : Type u_3
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_3} C
F G : Functor.{v_1, v_2, u_1, u_3} Jᵒᵖ C
α : F ⟶ G
hα : Coequifibered α
⊢ Equifibered (NatTrans.rightOp α)

Tactic:
fun _ _ f ↦ (hα f.op).op

Premises used: Quiver.Hom.op, CategoryTheory.NatTrans.Equifibered, CategoryTheory.IsPushout.op
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equifibered
Goal:
J : Type u_1
C : Type u_3
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_3} C
F G : Functor.{v_1, v_2, u_1, u_3} J C
α : F ⟶ G
⊢ Coequifibered (NatTrans.op α) ↔ Equifibered α

Tactic:
⟨Coequifibered.unop, Equifibered.op⟩

Premises used: Iff.intro, CategoryTheory.NatTrans.Coequifibered.unop, CategoryTheory.NatTrans.Equifibered.op
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equifibered
Goal:
J : Type u_1
C : Type u_3
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_3} C
F G : Functor.{v_1, v_2, u_1, u_3} J C
α : F ⟶ G
⊢ Equifibered (NatTrans.op α) ↔ Coequifibered α

Tactic:
⟨Equifibered.unop, Coequifibered.op⟩

Premises used: CategoryTheory.NatTrans.Coequifibered.op, Iff.intro, CategoryTheory.NatTrans.Equifibered.unop
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equifibered
Goal:
J : Type u_1
C : Type u_3
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_3} C
F G : Functor.{v_1, v_2, u_1, u_3} Jᵒᵖ Cᵒᵖ
α : F ⟶ G
⊢ Coequifibered (NatTrans.unop α) ↔ Equifibered α

Tactic:
⟨Coequifibered.op, Equifibered.unop⟩

Premises used: CategoryTheory.NatTrans.Coequifibered.op, Iff.intro, CategoryTheory.NatTrans.Equifibered.unop
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equifibered
Goal:
J : Type u_1
C : Type u_3
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_3} C
F G : Functor.{v_1, v_2, u_1, u_3} Jᵒᵖ Cᵒᵖ
α : F ⟶ G
⊢ Equifibered (NatTrans.unop α) ↔ Coequifibered α

Tactic:
⟨Equifibered.op, Coequifibered.unop⟩

Premises used: Iff.intro, CategoryTheory.NatTrans.Coequifibered.unop, CategoryTheory.NatTrans.Equifibered.op
-- 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 : Category.{v_1, u_1} J
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
inr :
  ∀
    (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), IsClosedUnderLimitsOfShape (C := Over F) (fun (f : Over F) ↦ Equifibered f.hom) J
wlog :
  ∀ {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
⊢ IsClosedUnderLimitsOfShape (C := Over F) (fun (f : Over F) ↦ Equifibered f.hom) J

Tactic:
wlog hJ : IsConnected J generalizing J

Premises used: CategoryTheory.IsConnected
-- 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 : Category.{v_1, u_1} J
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
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
⊢ IsClosedUnderLimitsOfShape (C := Over F) (fun (f : Over F) ↦ Equifibered f.hom) J

Tactic:
⟨fun G ⟨⟨c, α, hc⟩, H⟩ U V f ↦ ?_⟩

Premises used: _private.0.CategoryTheory.NatTrans.instIsClosedUnderLimitsOfShapeOverFunctorEquifiberedHomOfHasCoproductsOfShapeHom.match_1, CategoryTheory.IsPullback, CategoryTheory.Functor.map, CategoryTheory.Over.left, CategoryTheory.ObjectProperty.IsClosedUnderLimitsOfShape.mk, CategoryTheory.Over.hom, CategoryTheory.NatTrans.app
-- 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 : Category.{v_1, u_1} J
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
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
inr :
  ∀ (G : Over F),
    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),
        IsPullback (G.left.map f) (G.hom.app U) (G.hom.app V) (F.map f)
⊢ IsClosedUnderLimitsOfShape (C := Over F) (fun (f : Over F) ↦ Equifibered f.hom) J

Tactic:
refine ⟨fun G ⟨⟨c, α, hc⟩, H⟩ U V f ↦ ?_⟩
-- 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 : Category.{v_1, u_1} J
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
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_1 : 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
i j : J
f : i ⟶ j
⊢ α.app i ≫ c.map f = α.app j

Tactic:
simp [← NatTrans.naturality]

Premises used: CategoryTheory.NatTrans.naturality
-- 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 : Category.{v_1, u_1} J
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
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
⊢ ∀ (i j : J) (f : i ⟶ j), α.app i ≫ c.map f = α.app j

Tactic:
have hα (i j) (f : i ⟶ j) : α.app i ≫ c.map f = α.app j := by simp [← NatTrans.naturality]
-- 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 : Category.{v_1, u_1} J
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
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
inr :
  ∀ (hc' : IsLimit (obj (Equivalence.functor WithTerminal.coneEquiv) { pt := G, π := α : Cone c })),
    IsPullback (G.left.map f) (G.hom.app U) (G.hom.app V) (F.map f)
⊢ IsPullback (G.left.map f) (G.hom.app U) (G.hom.app V) (F.map f)

Tactic:
have hc' := WithTerminal.isLimitEquiv.symm hc
-- 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 : Category.{v_1, u_1} J
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
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 })
⊢ IsConnected.{v_1, u_1} (WithTerminal J)

Tactic:
have inst : IsConnected (WithTerminal J) := isConnected_of_hasTerminal _
-- 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)
j : J
⊢ ∀ (f : WithTerminal.star ⟶ WithTerminal.of j),
    (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.of j)) =
      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

Tactic:
try rintro ⟨⟩
-- 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 : J
⊢ ∀ (f : WithTerminal.of i ⟶ WithTerminal.of j),
    (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.of j)) =
      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:
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)
i : J
⊢ 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))

Tactic:
simp