awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Connected
Goal:
J : Type u'
inst : Category.{v', u'} J
C : Type u
inst_1 : Category.{v, u} C
D : Type u_1
inst_2 : Category.{v_1, u_1} D
K : Functor.{v, v_1, u, u_1} C D
X_1 : C
inst_3 : IsConnected.{v', u'} J
B : D
F : J ⥤ CostructuredArrow K B
c : Cone (F ⋙ proj K B)
X Y : J
f : X ⟶ Y
left :
  Eq (α :=
    (Functor.obj
          (Functor.obj (Functor.const J)
            (mk (K.map (c.π.app (Classical.arbitrary J)) ≫ (F.obj (Classical.arbitrary J)).hom)))
          X).left ⟶
      (F.obj Y).left)
    (CommaMorphism.left
      (Functor.map
          (Functor.obj (Functor.const J)
            (mk (K.map (c.π.app (Classical.arbitrary J)) ≫ (F.obj (Classical.arbitrary J)).hom)))
          f ≫
        homMk (c.π.app Y) ⋯))
    (CommaMorphism.left (homMk (c.π.app X) ⋯ ≫ F.map f))
right :
  Eq (α :=
    (Functor.obj
          (Functor.obj (Functor.const J)
            (mk (K.map (c.π.app (Classical.arbitrary J)) ≫ (F.obj (Classical.arbitrary J)).hom)))
          X).right ⟶
      (F.obj Y).right)
    (CommaMorphism.right
      (Functor.map
          (Functor.obj (Functor.const J)
            (mk (K.map (c.π.app (Classical.arbitrary J)) ≫ (F.obj (Classical.arbitrary J)).hom)))
          f ≫
        homMk (c.π.app Y) ⋯))
    (CommaMorphism.right (homMk (c.π.app X) ⋯ ≫ F.map f))
⊢ Eq (α :=
    Functor.obj
        (Functor.obj (Functor.const J)
          (mk (K.map (c.π.app (Classical.arbitrary J)) ≫ (F.obj (Classical.arbitrary J)).hom)))
        X ⟶
      F.obj Y)
    (Functor.map
        (Functor.obj (Functor.const J)
          (mk (K.map (c.π.app (Classical.arbitrary J)) ≫ (F.obj (Classical.arbitrary J)).hom)))
        f ≫
      homMk (c.π.app Y) ⋯)
    (homMk (c.π.app X) ⋯ ≫ F.map f)

Tactic:
apply CommaMorphism.ext

Premises used: CategoryTheory.CommaMorphism.ext
-- Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Connected
Goal:
J : Type u'
inst : Category.{v', u'} J
C : Type u
inst_1 : Category.{v, u} C
D : Type u_1
inst_2 : Category.{v_1, u_1} D
K : Functor.{v, v_1, u, u_1} C D
X_1 : C
inst_3 : IsConnected.{v', u'} J
B : D
F : J ⥤ CostructuredArrow K B
c : Cone (F ⋙ proj K B)
X Y : J
f : X ⟶ Y
⊢ Eq (α :=
    (Functor.obj
          (Functor.obj (Functor.const J)
            (mk (K.map (c.π.app (Classical.arbitrary J)) ≫ (F.obj (Classical.arbitrary J)).hom)))
          X).left ⟶
      (F.obj Y).left)
    (CommaMorphism.left
      (Functor.map
          (Functor.obj (Functor.const J)
            (mk (K.map (c.π.app (Classical.arbitrary J)) ≫ (F.obj (Classical.arbitrary J)).hom)))
          f ≫
        homMk (c.π.app Y) ⋯))
    (CommaMorphism.left (homMk (c.π.app X) ⋯ ≫ F.map f))

Tactic:
simpa using (c.w f).symm

Premises used: CategoryTheory.Limits.Cone.w, Eq.symm
-- Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Connected
Goal:
J : Type u'
inst : Category.{v', u'} J
C : Type u
inst_1 : Category.{v, u} C
D : Type u_1
inst_2 : Category.{v_1, u_1} D
K : Functor.{v, v_1, u, u_1} C D
X_1 : C
inst_3 : IsConnected.{v', u'} J
B : D
F : J ⥤ CostructuredArrow K B
c : Cone (F ⋙ proj K B)
X Y : J
f : X ⟶ Y
⊢ Eq (α :=
    (Functor.obj
          (Functor.obj (Functor.const J)
            (mk (K.map (c.π.app (Classical.arbitrary J)) ≫ (F.obj (Classical.arbitrary J)).hom)))
          X).right ⟶
      (F.obj Y).right)
    (CommaMorphism.right
      (Functor.map
          (Functor.obj (Functor.const J)
            (mk (K.map (c.π.app (Classical.arbitrary J)) ≫ (F.obj (Classical.arbitrary J)).hom)))
          f ≫
        homMk (c.π.app Y) ⋯))
    (CommaMorphism.right (homMk (c.π.app X) ⋯ ≫ F.map f))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Connected
Goal:
J : Type u'
inst : Category.{v', u'} J
C : Type u
inst_1 : Category.{v, u} C
D : Type u_1
inst_2 : Category.{v_1, u_1} D
K : Functor.{v, v_1, u, u_1} C D
inst_3 : IsConnected.{v', u'} J
B : D
F : J ⥤ CostructuredArrow K B
c : Cone (F ⋙ proj K B)
cat_disch cat_disch₁ cat_disch₂ cat_disch₃ : (proj K B).mapCone (raiseCone c) = c
⊢ (proj K B).mapCone (raiseCone c) = c

Tactic:
cat_disch
-- Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Connected
Goal:
J : Type u'
inst : Category.{v', u'} J
C : Type u
inst_1 : Category.{v, u} C
D : Type u_1
inst_2 : Category.{v_1, u_1} D
K : Functor.{v, v_1, u, u_1} C D
X : C
inst_3 : IsConnected.{v', u'} J
B : D
F : J ⥤ CostructuredArrow K B
c : Cone (F ⋙ proj K B)
t : IsLimit c
s : Cone F
⊢ K.map (t.lift ((proj K B).mapCone s)) ≫ (raiseCone c).pt.hom = s.pt.hom

Tactic:
simp [← Functor.map_comp_assoc]

Premises used: CategoryTheory.Functor.map_comp_assoc
-- Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Connected
Goal:
J : Type u'
inst : Category.{v', u'} J
C : Type u
inst_1 : Category.{v, u} C
D : Type u_1
inst_2 : Category.{v_1, u_1} D
K_1 : Functor.{v, v_1, u, u_1} C D
X : C
inst_3 : IsConnected.{v', u'} J
B : D
F : J ⥤ CostructuredArrow K_1 B
c : Cone (F ⋙ proj K_1 B)
t : IsLimit c
s : Cone F
m : s.pt ⟶ (raiseCone c).pt
K : ∀ (j : J), m ≫ (raiseCone c).π.app j = s.π.app j
h : m.left = CommaMorphism.left (homMk (t.lift ((proj K_1 B).mapCone s)) ⋯)
⊢ m = homMk (t.lift ((proj K_1 B).mapCone s)) ⋯

Tactic:
ext1
-- Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Connected
Goal:
J : Type u'
inst : Category.{v', u'} J
C : Type u
inst_1 : Category.{v, u} C
D : Type u_1
inst_2 : Category.{v_1, u_1} D
K_1 : Functor.{v, v_1, u, u_1} C D
X : C
inst_3 : IsConnected.{v', u'} J
B : D
F : J ⥤ CostructuredArrow K_1 B
c : Cone (F ⋙ proj K_1 B)
t : IsLimit c
s : Cone F
m : s.pt ⟶ (raiseCone c).pt
K : ∀ (j : J), m ≫ (raiseCone c).π.app j = s.π.app j
h : ∀ (j : J), m.left ≫ c.π.app j = CommaMorphism.left (homMk (t.lift ((proj K_1 B).mapCone s)) ⋯) ≫ c.π.app j
⊢ m.left = CommaMorphism.left (homMk (t.lift ((proj K_1 B).mapCone s)) ⋯)

Tactic:
apply t.hom_ext

Premises used: CategoryTheory.Limits.IsLimit.hom_ext
-- Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Connected
Goal:
J : Type u'
inst : Category.{v', u'} J
C : Type u
inst_1 : Category.{v, u} C
D : Type u_1
inst_2 : Category.{v_1, u_1} D
K_1 : Functor.{v, v_1, u, u_1} C D
X : C
inst_3 : IsConnected.{v', u'} J
B : D
F : J ⥤ CostructuredArrow K_1 B
c : Cone (F ⋙ proj K_1 B)
t : IsLimit c
s : Cone F
m : s.pt ⟶ (raiseCone c).pt
K : ∀ (j : J), m ≫ (raiseCone c).π.app j = s.π.app j
j : J
⊢ m.left ≫ c.π.app j = CommaMorphism.left (homMk (t.lift ((proj K_1 B).mapCone s)) ⋯) ≫ c.π.app j

Tactic:
simp [← K j]
-- Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Connected
Goal:
J : Type u'
inst : Category.{v', u'} J
C : Type u
inst_1 : Category.{v, u} C
D : Type u_1
inst_2 : Category.{v_1, u_1} D
K : Functor.{v, v_1, u, u_1} C D
X : C
inst_3 : IsConnected.{v', u'} J
B : D
K_1 : J ⥤ CostructuredArrow K B
c : Cone K_1
hc : IsLimit c
x : Cone (K_1 ⋙ proj K B)
x_1 : J
rw : (proj K B).map (hc.lift (CreatesConnected.raiseCone x)) ≫ (proj K B).map (c.π.app x_1) = x.π.app x_1
rw₁ : (proj K B).map (hc.lift (CreatesConnected.raiseCone x) ≫ c.π.app x_1) = x.π.app x_1
rw₂ : (proj K B).map ((CreatesConnected.raiseCone x).π.app x_1) = x.π.app x_1
rw₃ : (proj K B).map (homMk (x.π.app x_1) ⋯) = x.π.app x_1
rw₄ : CommaMorphism.left (homMk (x.π.app x_1) ⋯) = x.π.app x_1
rw₅ rw₆ : x.π.app x_1 = x.π.app x_1
⊢ (proj K B).map (hc.lift (CreatesConnected.raiseCone x)) ≫ ((proj K B).mapCone c).π.app x_1 = x.π.app x_1

Tactic:
rw [Functor.mapCone_π_app, ← Functor.map_comp, hc.fac,
        CreatesConnected.raiseCone_π_app, CostructuredArrow.proj_map,
        CostructuredArrow.homMk_left _ _]

Premises used: CategoryTheory.CostructuredArrow.proj_map, CategoryTheory.CostructuredArrow.homMk_left, CategoryTheory.Functor.mapCone_π_app, CategoryTheory.CostructuredArrow.CreatesConnected.raiseCone_π_app, CategoryTheory.Functor.map_comp, CategoryTheory.Limits.IsLimit.fac
-- Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Connected
Goal:
J : Type u'
inst : Category.{v', u'} J
C : Type u
inst_1 : Category.{v, u} C
D : Type u_1
inst_2 : Category.{v_1, u_1} D
K : Functor.{v, v_1, u, u_1} C D
X : C
inst_3 : IsConnected.{v', u'} J
B : D
K_1 : J ⥤ CostructuredArrow K B
c : Cone K_1
hc : IsLimit c
s : Cone (K_1 ⋙ proj K B)
m : s.pt ⟶ ((proj K B).mapCone c).pt
fac : ∀ (j : J), m ≫ ((proj K B).mapCone c).π.app j = s.π.app j
⊢ K.map m ≫ c.pt.hom = (CreatesConnected.raiseCone s).pt.hom

Tactic:
simp [← fac]
-- Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Connected
Goal:
J : Type u'
inst : Category.{v', u'} J
C : Type u
inst_1 : Category.{v, u} C
D : Type u_1
inst_2 : Category.{v_1, u_1} D
K : Functor.{v, v_1, u, u_1} C D
X : C
inst_3 : IsConnected.{v', u'} J
B : D
⊢ PreservesLimitsOfShape Jᵒᵖ (proj B K).op

Tactic:
have : PreservesLimitsOfShape Jᵒᵖ (proj B K).op :=
    inferInstanceAs <| PreservesLimitsOfShape Jᵒᵖ <|
      (structuredArrowOpEquivalence K B).functor ⋙ CostructuredArrow.proj K.op (.op B)
-- Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Connected
Goal:
J : Type u'
inst : Category.{v', u'} J
C : Type u
inst_1 : Category.{v, u} C
D : Type u_1
inst_2 : Category.{v_1, u_1} D
K : Functor.{v, v_1, u, u_1} C D
X : C
inst_3 : IsConnected.{v', u'} J
B : D
this : PreservesLimitsOfShape Jᵒᵖ (proj B K).op
⊢ PreservesColimitsOfShape J (proj B K)

Tactic:
apply preservesColimitsOfShape_of_op

Premises used: CategoryTheory.Limits.preservesColimitsOfShape_of_op
-- Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Connected
Goal:
J : Type u'
inst : Category.{v', u'} J
C : Type u
inst_1 : Category.{v, u} C
D : Type u_1
inst_2 : Category.{v_1, u_1} D
K : Functor.{v, v_1, u, u_1} C D
X : C
inst_3 : IsConnected.{v', u'} J
B : C
⊢ PreservesLimitsOfShape (C := Over.{v, u} B) J (forget B)

Tactic:
inferInstanceAs <| PreservesLimitsOfShape J (CostructuredArrow.proj _ _)

Premises used: _private.0.CategoryTheory.Over.preservesLimitsOfShape_forget_of_isConnected._proof_1
-- Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Connected
Goal:
J : Type u'
inst : Category.{v', u'} J
C : Type u
inst_1 : Category.{v, u} C
D_1 : Type u_1
inst_2 : Category.{v_1, u_1} D_1
K : Functor.{v, v_1, u, u_1} C D_1
X : C
B : D_1
inst_3 : IsConnected.{v', u'} J
inst_4 : HasLimitsOfShape.{v', u', v, u} J C
inst_5 : PreservesLimitsOfShape.{v', u', v, v_1, u, u_1} J K
D : J ⥤ CostructuredArrow K B
⊢ PreservesLimit D (CostructuredArrow.toOver K B ⋙ Over.forget B)

Tactic:
have : PreservesLimit D (CostructuredArrow.toOver K B ⋙ Over.forget B) :=
      inferInstanceAs <| PreservesLimit D (CostructuredArrow.proj K B ⋙ K)
-- Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Connected
Goal:
J : Type u'
inst : Category.{v', u'} J
C : Type u
inst_1 : Category.{v, u} C
D_1 : Type u_1
inst_2 : Category.{v_1, u_1} D_1
K : Functor.{v, v_1, u, u_1} C D_1
X : C
B : D_1
inst_3 : IsConnected.{v', u'} J
inst_4 : HasLimitsOfShape.{v', u', v, u} J C
inst_5 : PreservesLimitsOfShape.{v', u', v, v_1, u, u_1} J K
D : J ⥤ CostructuredArrow K B
this : PreservesLimit D (CostructuredArrow.toOver K B ⋙ Over.forget B)
⊢ PreservesLimit D (CostructuredArrow.toOver K B)

Tactic:
Limits.preservesLimit_of_reflects_of_preserves _ (Over.forget B)

Premises used: CategoryTheory.Over.forget, CategoryTheory.Limits.preservesLimit_of_reflects_of_preserves
-- Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Connected
Goal:
J : Type u'
inst : Category.{v', u'} J
C : Type u
inst_1 : Category.{v, u} C
D_1 : Type u_1
inst_2 : Category.{v_1, u_1} D_1
K : Functor.{v, v_1, u, u_1} C D_1
X : C
B : D_1
inst_3 : IsConnected.{v', u'} J
inst_4 : HasLimitsOfShape.{v', u', v, u} J C
inst_5 : PreservesLimitsOfShape.{v', u', v, v_1, u, u_1} J K
D : J ⥤ CostructuredArrow K B
this : PreservesLimit D (CostructuredArrow.toOver K B ⋙ Over.forget B)
⊢ PreservesLimit D (CostructuredArrow.toOver K B)

Tactic:
exact Limits.preservesLimit_of_reflects_of_preserves _ (Over.forget B)

Premises used: CategoryTheory.Over.forget, CategoryTheory.Limits.preservesLimit_of_reflects_of_preserves
-- Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Connected
Goal:
J : Type u'
inst : Category.{v', u'} J
C : Type u
inst_1 : Category.{v, u} C
D : Type u_1
inst_2 : Category.{v_1, u_1} D
K : Functor.{v, v_1, u, u_1} C D
X : C
inst_3 : IsConnected.{v', u'} J
B : C
⊢ PreservesColimitsOfShape (C := Under.{v, u} B) J (forget B)

Tactic:
inferInstanceAs <| PreservesColimitsOfShape J (StructuredArrow.proj _ _)

Premises used: _private.0.CategoryTheory.Under.preservesColimitsOfShape_forget_of_isConnected._proof_1
-- Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Connected
Goal:
J : Type u'
inst : Category.{v', u'} J
C : Type u
inst_1 : Category.{v, u} C
D_1 : Type u_1
inst_2 : Category.{v_1, u_1} D_1
K : Functor.{v, v_1, u, u_1} C D_1
X : C
B : D_1
inst_3 : IsConnected.{v', u'} J
inst_4 : HasColimitsOfShape.{v', u', v, u} J C
inst_5 : PreservesColimitsOfShape.{v', u', v, v_1, u, u_1} J K
D : J ⥤ StructuredArrow B K
⊢ PreservesColimit D (StructuredArrow.toUnder B K ⋙ Under.forget B)

Tactic:
have : PreservesColimit D (StructuredArrow.toUnder B K ⋙ Under.forget B) :=
      inferInstanceAs <| PreservesColimit D (StructuredArrow.proj B K ⋙ K)
-- Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Connected
Goal:
J : Type u'
inst : Category.{v', u'} J
C : Type u
inst_1 : Category.{v, u} C
D_1 : Type u_1
inst_2 : Category.{v_1, u_1} D_1
K : Functor.{v, v_1, u, u_1} C D_1
X : C
B : D_1
inst_3 : IsConnected.{v', u'} J
inst_4 : HasColimitsOfShape.{v', u', v, u} J C
inst_5 : PreservesColimitsOfShape.{v', u', v, v_1, u, u_1} J K
D : J ⥤ StructuredArrow B K
this : PreservesColimit D (StructuredArrow.toUnder B K ⋙ Under.forget B)
⊢ PreservesColimit D (StructuredArrow.toUnder B K)

Tactic:
Limits.preservesColimit_of_reflects_of_preserves _ (Under.forget B)

Premises used: CategoryTheory.Limits.preservesColimit_of_reflects_of_preserves, CategoryTheory.Under.forget
-- Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Connected
Goal:
J : Type u'
inst : Category.{v', u'} J
C : Type u
inst_1 : Category.{v, u} C
D_1 : Type u_1
inst_2 : Category.{v_1, u_1} D_1
K : Functor.{v, v_1, u, u_1} C D_1
X : C
B : D_1
inst_3 : IsConnected.{v', u'} J
inst_4 : HasColimitsOfShape.{v', u', v, u} J C
inst_5 : PreservesColimitsOfShape.{v', u', v, v_1, u, u_1} J K
D : J ⥤ StructuredArrow B K
this : PreservesColimit D (StructuredArrow.toUnder B K ⋙ Under.forget B)
⊢ PreservesColimit D (StructuredArrow.toUnder B K)

Tactic:
exact Limits.preservesColimit_of_reflects_of_preserves _ (Under.forget B)

Premises used: CategoryTheory.Limits.preservesColimit_of_reflects_of_preserves, CategoryTheory.Under.forget
-- Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Products
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : Y ⟶ X
g : Z ⟶ X
c₁ c₂ : BinaryFan (Over.mk f) (Over.mk g)
a : c₁ ⟶ c₂
⊢ Eq (α := (PullbackCone.mk (Over.Hom.left c₁.fst) (Over.Hom.left c₁.snd) ⋯).pt ⟶ (cospan f g).obj none)
    (Over.Hom.left a.hom ≫ (PullbackCone.mk (Over.Hom.left c₂.fst) (Over.Hom.left c₂.snd) ⋯).π.app none)
    ((PullbackCone.mk (Over.Hom.left c₁.fst) (Over.Hom.left c₁.snd) ⋯).π.app none)

Tactic:
simp [← Over.comp_left_assoc, ← Over.comp_left]

Premises used: CategoryTheory.Over.comp_left_assoc, CategoryTheory.Over.comp_left
-- Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Products
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : Y ⟶ X
g : Z ⟶ X
c₁ c₂ : BinaryFan (Over.mk f) (Over.mk g)
a : c₁ ⟶ c₂
⊢ Eq (α :=
    (PullbackCone.mk (Over.Hom.left c₁.fst) (Over.Hom.left c₁.snd) ⋯).pt ⟶ (cospan f g).obj (some WalkingPair.left))
    (Over.Hom.left a.hom ≫
      (PullbackCone.mk (Over.Hom.left c₂.fst) (Over.Hom.left c₂.snd) ⋯).π.app (some WalkingPair.left))
    ((PullbackCone.mk (Over.Hom.left c₁.fst) (Over.Hom.left c₁.snd) ⋯).π.app (some WalkingPair.left))

Tactic:
simp [← Over.comp_left_assoc, ← Over.comp_left]

Premises used: CategoryTheory.Over.comp_left_assoc, CategoryTheory.Over.comp_left
-- Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Products
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : Y ⟶ X
g : Z ⟶ X
c₁ c₂ : BinaryFan (Over.mk f) (Over.mk g)
a : c₁ ⟶ c₂
⊢ Eq (α :=
    (PullbackCone.mk (Over.Hom.left c₁.fst) (Over.Hom.left c₁.snd) ⋯).pt ⟶ (cospan f g).obj (some WalkingPair.right))
    (Over.Hom.left a.hom ≫
      (PullbackCone.mk (Over.Hom.left c₂.fst) (Over.Hom.left c₂.snd) ⋯).π.app (some WalkingPair.right))
    ((PullbackCone.mk (Over.Hom.left c₁.fst) (Over.Hom.left c₁.snd) ⋯).π.app (some WalkingPair.right))

Tactic:
simp [← Over.comp_left_assoc, ← Over.comp_left]

Premises used: CategoryTheory.Over.comp_left_assoc, CategoryTheory.Over.comp_left
-- Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Products
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : Y ⟶ X
g : Z ⟶ X
X_1 Y_1 : PullbackCone f g
f_1 : X_1 ⟶ Y_1
⊢ Eq (α :=
    (Functor.obj (𝟭 (PullbackCone f g)) X_1).pt ⟶
      Cone.pt.{0, v, 0, u} (J := WalkingCospan) (F := cospan f g)
        (Functor.obj
          (Functor.comp (D := BinaryFan (Over.mk f) (Over.mk g))
            {
              obj := fun (c : PullbackCone f g) ↦
                BinaryFan.mk (P := Over.mk (c.fst ≫ f)) (Over.homMk c.fst ⋯) (Over.homMk c.snd ⋯),
              map := fun {c₁ c₂ : PullbackCone f g} (a : c₁ ⟶ c₂) ↦ { hom := Over.homMk a.hom ⋯, w := ⋯ }, map_id := ⋯,
              map_comp := ⋯ }
            {
              obj := fun (c : BinaryFan (Over.mk f) (Over.mk g)) ↦
                PullbackCone.mk (Over.Hom.left c.fst) (Over.Hom.left c.snd) ⋯,
              map := fun {c₁ c₂ : BinaryFan (Over.mk f) (Over.mk g)} (a : c₁ ⟶ c₂) ↦
                { hom := Over.Hom.left a.hom, w := ⋯ },
              map_id := ⋯, map_comp := ⋯ })
          Y_1))
    (ConeMorphism.hom (Functor.map (𝟭 (PullbackCone f g)) f_1 ≫ Iso.hom ((fun (c : PullbackCone f g) ↦ c.eta) Y_1)))
    (ConeMorphism.hom
      (Iso.hom ((fun (c : PullbackCone f g) ↦ c.eta) X_1) ≫
        Functor.map
          (Functor.comp (D := BinaryFan (Over.mk f) (Over.mk g))
            {
              obj := fun (c : PullbackCone f g) ↦
                BinaryFan.mk (P := Over.mk (c.fst ≫ f)) (Over.homMk c.fst ⋯) (Over.homMk c.snd ⋯),
              map := fun {c₁ c₂ : PullbackCone f g} (a : c₁ ⟶ c₂) ↦
                { hom := Over.homMk a.hom ⋯, w := ⋯ :
                  ConeMorphism (C := Over.{v, u} X) (F := pair (Over.mk f) (Over.mk g))
                    (BinaryFan.mk (P := Over.mk (c₁.fst ≫ f)) (Over.homMk c₁.fst ⋯) (Over.homMk c₁.snd ⋯))
                    (BinaryFan.mk (P := Over.mk (c₂.fst ≫ f)) (Over.homMk c₂.fst ⋯) (Over.homMk c₂.snd ⋯)) },
              map_id := ⋯, map_comp := ⋯ : PullbackCone f g ⥤ BinaryFan (Over.mk f) (Over.mk g) }
            {
              obj := fun (c : BinaryFan (Over.mk f) (Over.mk g)) ↦
                PullbackCone.mk (Over.Hom.left c.fst) (Over.Hom.left c.snd) ⋯,
              map := fun {c₁ c₂ : BinaryFan (Over.mk f) (Over.mk g)} (a : c₁ ⟶ c₂) ↦
                { hom := Over.Hom.left a.hom, w := ⋯ :
                  ConeMorphism (PullbackCone.mk (Over.Hom.left c₁.fst) (Over.Hom.left c₁.snd) ⋯)
                    (PullbackCone.mk (Over.Hom.left c₂.fst) (Over.Hom.left c₂.snd) ⋯) },
              map_id := ⋯, map_comp := ⋯ : BinaryFan (Over.mk f) (Over.mk g) ⥤ PullbackCone f g })
          f_1))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Products
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
X_1 Y Z : C
f : Y ⟶ X_1
g : Z ⟶ X_1
X : BinaryFan (Over.mk f) (Over.mk g)
⊢ Iso.hom
        (Iso.refl
          (Over.left.{v, u} (X := X_1)
            (Cone.pt (J := Discrete WalkingPair) (F := pair (Over.mk f) (Over.mk g))
              (Functor.obj
                (Functor.comp (D := PullbackCone f g)
                  {
                    obj := fun (c : BinaryFan (Over.mk f) (Over.mk g)) ↦
                      PullbackCone.mk (Over.Hom.left c.fst) (Over.Hom.left c.snd) ⋯,
                    map := fun {c₁ c₂ : BinaryFan (Over.mk f) (Over.mk g)} (a : c₁ ⟶ c₂) ↦
                      { hom := Over.Hom.left a.hom, w := ⋯ :
                        ConeMorphism (PullbackCone.mk (Over.Hom.left c₁.fst) (Over.Hom.left c₁.snd) ⋯)
                          (PullbackCone.mk (Over.Hom.left c₂.fst) (Over.Hom.left c₂.snd) ⋯) },
                    map_id := ⋯, map_comp := ⋯ : BinaryFan (Over.mk f) (Over.mk g) ⥤ PullbackCone f g }
                  {
                    obj := fun (c : PullbackCone f g) ↦
                      BinaryFan.mk (P := Over.mk (c.fst ≫ f)) (Over.homMk c.fst ⋯) (Over.homMk c.snd ⋯),
                    map := fun {c₁ c₂ : PullbackCone f g} (a : c₁ ⟶ c₂) ↦
                      { hom := Over.homMk a.hom ⋯, w := ⋯ :
                        ConeMorphism (C := Over.{v, u} X_1) (F := pair (Over.mk f) (Over.mk g))
                          (BinaryFan.mk (P := Over.mk (c₁.fst ≫ f)) (Over.homMk c₁.fst ⋯) (Over.homMk c₁.snd ⋯))
                          (BinaryFan.mk (P := Over.mk (c₂.fst ≫ f)) (Over.homMk c₂.fst ⋯) (Over.homMk c₂.snd ⋯)) },
                    map_id := ⋯, map_comp := ⋯ : PullbackCone f g ⥤ BinaryFan (Over.mk f) (Over.mk g) })
                X)))) ≫
      (Functor.obj (𝟭 (BinaryFan (Over.mk f) (Over.mk g))) X).pt.hom =
    Over.hom
      (Cone.pt (J := Discrete WalkingPair) (F := pair (Over.mk f) (Over.mk g))
        (Functor.obj
          (Functor.comp (D := PullbackCone f g)
            {
              obj := fun (c : BinaryFan (Over.mk f) (Over.mk g)) ↦
                PullbackCone.mk (Over.Hom.left c.fst) (Over.Hom.left c.snd) ⋯,
              map := fun {c₁ c₂ : BinaryFan (Over.mk f) (Over.mk g)} (a : c₁ ⟶ c₂) ↦
                { hom := Over.Hom.left a.hom, w := ⋯ },
              map_id := ⋯, map_comp := ⋯ }
            {
              obj := fun (c : PullbackCone f g) ↦
                BinaryFan.mk (P := Over.mk (c.fst ≫ f)) (Over.homMk c.fst ⋯) (Over.homMk c.snd ⋯),
              map := fun {c₁ c₂ : PullbackCone f g} (a : c₁ ⟶ c₂) ↦ { hom := Over.homMk a.hom ⋯, w := ⋯ }, map_id := ⋯,
              map_comp := ⋯ })
          X))

Tactic:
simpa using X.fst.w.symm

Premises used: CategoryTheory.Limits.BinaryFan.fst, CategoryTheory.Over.Hom.w, Eq.symm