awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
⊢ Over.Hom.left
      (BinaryFan.fst
        (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)) =
    Over.Hom.left
      (Iso.hom
          (Over.isoMk
            (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).fst)

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)
⊢ Over.Hom.left
      (BinaryFan.snd
        (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)) =
    Over.Hom.left
      (Iso.hom
          (Over.isoMk
            (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).snd)

Tactic:
simp
-- 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 : PullbackCone f g
hc : IsLimit c
s : BinaryFan (Over.mk f) (Over.mk g)
⊢ hc.lift (Functor.obj (Equivalence.inverse pullbackConeEquivBinaryFan) s) ≫ (Over.mk (c.fst ≫ f)).hom = s.pt.hom

Tactic:
simpa using s.fst.w

Premises used: CategoryTheory.Limits.BinaryFan.fst, CategoryTheory.Over.Hom.w
-- 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 : PullbackCone f g
hc : IsLimit c
s : BinaryFan (Over.mk f) (Over.mk g)
m : s.pt ⟶ Over.mk (c.fst ≫ f)
e₁ : m ≫ Over.homMk c.fst ⋯ = s.fst
e₂ : m ≫ Over.homMk c.snd ⋯ = s.snd
h :
  Over.Hom.left m =
    Over.Hom.left
      ((fun (s : BinaryFan (Over.mk f) (Over.mk g)) ↦
          (Over.homMk (hc.lift (Functor.obj (Equivalence.inverse pullbackConeEquivBinaryFan) s)) ⋯ :
            s.pt ⟶ Over.mk (c.fst ≫ f)))
        s)
⊢ m =
    (fun (s : BinaryFan (Over.mk f) (Over.mk g)) ↦
        (Over.homMk (hc.lift (Functor.obj (Equivalence.inverse pullbackConeEquivBinaryFan) s)) ⋯ :
          s.pt ⟶ Over.mk (c.fst ≫ f)))
      s

Tactic:
ext1
-- 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 : PullbackCone f g
hc : IsLimit c
s : BinaryFan (Over.mk f) (Over.mk g)
m : s.pt ⟶ Over.mk (c.fst ≫ f)
e₁ : m ≫ Over.homMk c.fst ⋯ = s.fst
e₂ : m ≫ Over.homMk c.snd ⋯ = s.snd
h :
  Over.Hom.left m ≫ c.fst =
    Over.Hom.left
        ((fun (s : BinaryFan (Over.mk f) (Over.mk g)) ↦
            (Over.homMk (hc.lift (Functor.obj (Equivalence.inverse pullbackConeEquivBinaryFan) s)) ⋯ :
              s.pt ⟶ Over.mk (c.fst ≫ f)))
          s) ≫
      c.fst
h₁ :
  Over.Hom.left m ≫ c.snd =
    Over.Hom.left
        ((fun (s : BinaryFan (Over.mk f) (Over.mk g)) ↦
            (Over.homMk (hc.lift (Functor.obj (Equivalence.inverse pullbackConeEquivBinaryFan) s)) ⋯ :
              s.pt ⟶ Over.mk (c.fst ≫ f)))
          s) ≫
      c.snd
⊢ Over.Hom.left m =
    Over.Hom.left
      ((fun (s : BinaryFan (Over.mk f) (Over.mk g)) ↦
          (Over.homMk (hc.lift (Functor.obj (Equivalence.inverse pullbackConeEquivBinaryFan) s)) ⋯ :
            s.pt ⟶ Over.mk (c.fst ≫ f)))
        s)

Tactic:
apply PullbackCone.IsLimit.hom_ext hc

Premises used: CategoryTheory.Limits.PullbackCone.IsLimit.hom_ext
-- 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 : PullbackCone f g
hc : IsLimit c
s : BinaryFan (Over.mk f) (Over.mk g)
m : s.pt ⟶ Over.mk (c.fst ≫ f)
e₁ : m ≫ Over.homMk c.fst ⋯ = s.fst
e₂ : m ≫ Over.homMk c.snd ⋯ = s.snd
⊢ Over.Hom.left m ≫ c.fst =
    Over.Hom.left
        ((fun (s : BinaryFan (Over.mk f) (Over.mk g)) ↦
            (Over.homMk (hc.lift (Functor.obj (Equivalence.inverse pullbackConeEquivBinaryFan) s)) ⋯ :
              s.pt ⟶ Over.mk (c.fst ≫ f)))
          s) ≫
      c.fst

Tactic:
simpa using congr(($e₁).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 : PullbackCone f g
hc : IsLimit c
s : BinaryFan (Over.mk f) (Over.mk g)
m : s.pt ⟶ Over.mk (c.fst ≫ f)
e₁ : m ≫ Over.homMk c.fst ⋯ = s.fst
e₂ : m ≫ Over.homMk c.snd ⋯ = s.snd
⊢ Over.Hom.left m ≫ c.snd =
    Over.Hom.left
        ((fun (s : BinaryFan (Over.mk f) (Over.mk g)) ↦
            (Over.homMk (hc.lift (Functor.obj (Equivalence.inverse pullbackConeEquivBinaryFan) s)) ⋯ :
              s.pt ⟶ Over.mk (c.fst ≫ f)))
          s) ≫
      c.snd

Tactic:
simpa using congr(($e₂).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 : BinaryFan (Over.mk f) (Over.mk g)
hc : IsLimit c
s :
  PullbackCone (Functor.obj (pair (Over.mk f) (Over.mk g)) { as := WalkingPair.left : Discrete WalkingPair }).hom
    (Functor.obj (pair (Over.mk f) (Over.mk g)) { as := WalkingPair.right : Discrete WalkingPair }).hom
⊢ (fun
            (s :
              PullbackCone
                (Functor.obj (pair (Over.mk f) (Over.mk g)) { as := WalkingPair.left : Discrete WalkingPair }).hom
                (Functor.obj (pair (Over.mk f) (Over.mk g)) { as := WalkingPair.right : Discrete WalkingPair }).hom) ↦
          (Over.Hom.left (hc.lift (Functor.obj (Equivalence.functor pullbackConeEquivBinaryFan) s)) :
            (Functor.obj (Equivalence.functor pullbackConeEquivBinaryFan) s).pt.left ⟶ c.pt.left))
        s ≫
      Over.Hom.left c.fst =
    s.fst

Tactic:
simpa only using congr($(hc.fac _ _).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 : BinaryFan (Over.mk f) (Over.mk g)
hc : IsLimit c
s :
  PullbackCone (Functor.obj (pair (Over.mk f) (Over.mk g)) { as := WalkingPair.left : Discrete WalkingPair }).hom
    (Functor.obj (pair (Over.mk f) (Over.mk g)) { as := WalkingPair.right : Discrete WalkingPair }).hom
⊢ (fun
            (s :
              PullbackCone
                (Functor.obj (pair (Over.mk f) (Over.mk g)) { as := WalkingPair.left : Discrete WalkingPair }).hom
                (Functor.obj (pair (Over.mk f) (Over.mk g)) { as := WalkingPair.right : Discrete WalkingPair }).hom) ↦
          (Over.Hom.left (hc.lift (Functor.obj (Equivalence.functor pullbackConeEquivBinaryFan) s)) :
            (Functor.obj (Equivalence.functor pullbackConeEquivBinaryFan) s).pt.left ⟶ c.pt.left))
        s ≫
      Over.Hom.left c.snd =
    s.snd

Tactic:
simpa only using congr($(hc.fac _ _).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 : BinaryFan (Over.mk f) (Over.mk g)
hc : IsLimit c
s :
  PullbackCone (Functor.obj (pair (Over.mk f) (Over.mk g)) { as := WalkingPair.left : Discrete WalkingPair }).hom
    (Functor.obj (pair (Over.mk f) (Over.mk g)) { as := WalkingPair.right : Discrete WalkingPair }).hom
m :
  s.pt ⟶
    (Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) c.pt)
        { as := WalkingPair.left : Discrete WalkingPair }).left
hm₁ : m ≫ Over.Hom.left c.fst = s.fst
hm₂ : m ≫ Over.Hom.left c.snd = s.snd
change :
  ∀ (s : PullbackCone f g)
    (m :
      s.pt ⟶
        (Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) c.pt)
            { as := WalkingPair.left : Discrete WalkingPair }).left)
    (hm₁ : m ≫ Over.Hom.left c.fst = s.fst) (hm₂ : m ≫ Over.Hom.left c.snd = s.snd),
    m =
      (fun
            (s :
              PullbackCone
                (Functor.obj (pair (Over.mk f) (Over.mk g)) { as := WalkingPair.left : Discrete WalkingPair }).hom
                (Functor.obj (pair (Over.mk f) (Over.mk g)) { as := WalkingPair.right : Discrete WalkingPair }).hom) ↦
          (Over.Hom.left (hc.lift (Functor.obj (Equivalence.functor pullbackConeEquivBinaryFan) s)) :
            (Functor.obj (Equivalence.functor pullbackConeEquivBinaryFan) s).pt.left ⟶ c.pt.left))
        s
⊢ m =
    (fun
          (s :
            PullbackCone
              (Functor.obj (pair (Over.mk f) (Over.mk g)) { as := WalkingPair.left : Discrete WalkingPair }).hom
              (Functor.obj (pair (Over.mk f) (Over.mk g)) { as := WalkingPair.right : Discrete WalkingPair }).hom) ↦
        (Over.Hom.left (hc.lift (Functor.obj (Equivalence.functor pullbackConeEquivBinaryFan) s)) :
          (Functor.obj (Equivalence.functor pullbackConeEquivBinaryFan) s).pt.left ⟶ c.pt.left))
      s

Tactic:
change PullbackCone f g at s

Premises used: CategoryTheory.Limits.PullbackCone
-- 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 : BinaryFan (Over.mk f) (Over.mk g)
hc : IsLimit c
s : PullbackCone f g
m :
  s.pt ⟶
    (Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) c.pt)
        { as := WalkingPair.left : Discrete WalkingPair }).left
hm₁ : m ≫ Over.Hom.left c.fst = s.fst
hm₂ : m ≫ Over.Hom.left c.snd = s.snd
⊢ m ≫ c.pt.hom = (Functor.obj (Equivalence.functor pullbackConeEquivBinaryFan) s).pt.hom

Tactic:
simp [← hm₁, dsimp% c.fst.w]

Premises used: CategoryTheory.Limits.BinaryFan.fst, CategoryTheory.Over.Hom.w
-- 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 : BinaryFan (Over.mk f) (Over.mk g)
hc : IsLimit c
s : PullbackCone f g
m :
  s.pt ⟶
    (Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) c.pt)
        { as := WalkingPair.left : Discrete WalkingPair }).left
hm₁ : m ≫ Over.Hom.left c.fst = s.fst
hm₂ : m ≫ Over.Hom.left c.snd = s.snd
left :
  Eq (α :=
    (Functor.obj (Equivalence.functor pullbackConeEquivBinaryFan) s).pt.left ⟶
      (Functor.obj (pair (Over.mk f) (Over.mk g)) { as := WalkingPair.left : Discrete WalkingPair }).left)
    (Over.Hom.left (Over.homMk m ⋯ ≫ c.π.app { as := WalkingPair.left : Discrete WalkingPair }))
    (Over.Hom.left ((Functor.obj (Equivalence.functor pullbackConeEquivBinaryFan) s).π.app { as := WalkingPair.left }))
⊢ Eq (α :=
    (Functor.obj (Equivalence.functor pullbackConeEquivBinaryFan) s).pt ⟶
      Functor.obj (pair (Over.mk f) (Over.mk g)) { as := WalkingPair.left : Discrete WalkingPair })
    (Over.homMk m ⋯ ≫ c.π.app { as := WalkingPair.left : Discrete WalkingPair })
    ((Functor.obj (Equivalence.functor pullbackConeEquivBinaryFan) s).π.app { as := WalkingPair.left })

Tactic:
ext
-- 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 : BinaryFan (Over.mk f) (Over.mk g)
hc : IsLimit c
s : PullbackCone f g
m :
  s.pt ⟶
    (Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) c.pt)
        { as := WalkingPair.left : Discrete WalkingPair }).left
hm₁ : m ≫ Over.Hom.left c.fst = s.fst
hm₂ : m ≫ Over.Hom.left c.snd = s.snd
right :
  Eq (α :=
    (Functor.obj (Equivalence.functor pullbackConeEquivBinaryFan) s).pt.left ⟶
      (Functor.obj (pair (Over.mk f) (Over.mk g)) { as := WalkingPair.right : Discrete WalkingPair }).left)
    (Over.Hom.left (Over.homMk m ⋯ ≫ c.π.app { as := WalkingPair.right : Discrete WalkingPair }))
    (Over.Hom.left ((Functor.obj (Equivalence.functor pullbackConeEquivBinaryFan) s).π.app { as := WalkingPair.right }))
⊢ Eq (α :=
    (Functor.obj (Equivalence.functor pullbackConeEquivBinaryFan) s).pt ⟶
      Functor.obj (pair (Over.mk f) (Over.mk g)) { as := WalkingPair.right : Discrete WalkingPair })
    (Over.homMk m ⋯ ≫ c.π.app { as := WalkingPair.right : Discrete WalkingPair })
    ((Functor.obj (Equivalence.functor pullbackConeEquivBinaryFan) s).π.app { as := WalkingPair.right })

Tactic:
ext
-- 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 : BinaryFan (Over.mk f) (Over.mk g)
hc : IsLimit c
s : PullbackCone f g
m :
  s.pt ⟶
    (Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) c.pt)
        { as := WalkingPair.left : Discrete WalkingPair }).left
hm₁ : m ≫ Over.Hom.left c.fst = s.fst
hm₂ : m ≫ Over.Hom.left c.snd = s.snd
⊢ Eq (α :=
    (Functor.obj (Equivalence.functor pullbackConeEquivBinaryFan) s).pt.left ⟶
      (Functor.obj (pair (Over.mk f) (Over.mk g)) { as := WalkingPair.left : Discrete WalkingPair }).left)
    (Over.Hom.left (Over.homMk m ⋯ ≫ c.π.app { as := WalkingPair.left : Discrete WalkingPair }))
    (Over.Hom.left ((Functor.obj (Equivalence.functor pullbackConeEquivBinaryFan) s).π.app { as := WalkingPair.left }))

Tactic:
simpa
-- 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 : BinaryFan (Over.mk f) (Over.mk g)
hc : IsLimit c
s : PullbackCone f g
m :
  s.pt ⟶
    (Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) c.pt)
        { as := WalkingPair.left : Discrete WalkingPair }).left
hm₁ : m ≫ Over.Hom.left c.fst = s.fst
hm₂ : m ≫ Over.Hom.left c.snd = s.snd
⊢ Eq (α :=
    (Functor.obj (Equivalence.functor pullbackConeEquivBinaryFan) s).pt.left ⟶
      (Functor.obj (pair (Over.mk f) (Over.mk g)) { as := WalkingPair.right : Discrete WalkingPair }).left)
    (Over.Hom.left (Over.homMk m ⋯ ≫ c.π.app { as := WalkingPair.right : Discrete WalkingPair }))
    (Over.Hom.left ((Functor.obj (Equivalence.functor pullbackConeEquivBinaryFan) s).π.app { as := WalkingPair.right }))

Tactic:
simpa
-- 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 : BinaryFan (Over.mk f) (Over.mk g)
hc : IsLimit c
s : PullbackCone f g
m :
  s.pt ⟶
    (Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) c.pt)
        { as := WalkingPair.left : Discrete WalkingPair }).left
hm₁ : m ≫ Over.Hom.left c.fst = s.fst
hm₂ : m ≫ Over.Hom.left c.snd = s.snd
⊢ Eq (α := (Functor.obj (Equivalence.functor pullbackConeEquivBinaryFan) s).pt ⟶ c.pt) (Over.homMk m ⋯)
    (hc.lift (Functor.obj (Equivalence.functor pullbackConeEquivBinaryFan) s))

Tactic:
have := hc.uniq (pullbackConeEquivBinaryFan.functor.obj s) (Over.homMk m <| by
        simp [← hm₁, dsimp% c.fst.w])
        (by rintro (_ | _) <;> ext <;> simpa)
-- 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 : BinaryFan (Over.mk f) (Over.mk g)
hc : IsLimit c
s : PullbackCone f g
m :
  s.pt ⟶
    (Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) c.pt)
        { as := WalkingPair.left : Discrete WalkingPair }).left
hm₁ : m ≫ Over.Hom.left c.fst = s.fst
hm₂ : m ≫ Over.Hom.left c.snd = s.snd
this :
  Eq (α := (Functor.obj (Equivalence.functor pullbackConeEquivBinaryFan) s).pt ⟶ c.pt) (Over.homMk m ⋯)
    (hc.lift (Functor.obj (Equivalence.functor pullbackConeEquivBinaryFan) s))
⊢ m =
    (fun
          (s :
            PullbackCone
              (Functor.obj (pair (Over.mk f) (Over.mk g)) { as := WalkingPair.left : Discrete WalkingPair }).hom
              (Functor.obj (pair (Over.mk f) (Over.mk g)) { as := WalkingPair.right : Discrete WalkingPair }).hom) ↦
        (Over.Hom.left (hc.lift (Functor.obj (Equivalence.functor pullbackConeEquivBinaryFan) s)) :
          (Functor.obj (Equivalence.functor pullbackConeEquivBinaryFan) s).pt.left ⟶ c.pt.left))
      s

Tactic:
congr(($this).left)

Premises used: congrArg, CategoryTheory.Over.Hom.left, id
-- 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 : BinaryFan (Over.mk f) (Over.mk g)
hc : IsLimit c
s : PullbackCone f g
m :
  s.pt ⟶
    (Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) c.pt)
        { as := WalkingPair.left : Discrete WalkingPair }).left
hm₁ : m ≫ Over.Hom.left c.fst = s.fst
hm₂ : m ≫ Over.Hom.left c.snd = s.snd
this :
  Eq (α := (Functor.obj (Equivalence.functor pullbackConeEquivBinaryFan) s).pt ⟶ c.pt) (Over.homMk m ⋯)
    (hc.lift (Functor.obj (Equivalence.functor pullbackConeEquivBinaryFan) s))
⊢ m =
    (fun
          (s :
            PullbackCone
              (Functor.obj (pair (Over.mk f) (Over.mk g)) { as := WalkingPair.left : Discrete WalkingPair }).hom
              (Functor.obj (pair (Over.mk f) (Over.mk g)) { as := WalkingPair.right : Discrete WalkingPair }).hom) ↦
        (Over.Hom.left (hc.lift (Functor.obj (Equivalence.functor pullbackConeEquivBinaryFan) s)) :
          (Functor.obj (Equivalence.functor pullbackConeEquivBinaryFan) s).pt.left ⟶ c.pt.left))
      s

Tactic:
exact congr(($this).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 : X ⟶ Y
g : X ⟶ Z
c₁ c₂ : BinaryCofan (Under.mk f) (Under.mk g)
a : c₁ ⟶ c₂
⊢ Eq (α := (span f g).obj none ⟶ (PushoutCocone.mk (Under.Hom.right c₂.inl) (Under.Hom.right c₂.inr) ⋯).pt)
    ((PushoutCocone.mk (Under.Hom.right c₁.inl) (Under.Hom.right c₁.inr) ⋯).ι.app none ≫ Under.Hom.right a.hom)
    ((PushoutCocone.mk (Under.Hom.right c₂.inl) (Under.Hom.right c₂.inr) ⋯).ι.app none)

Tactic:
simp [← Under.comp_right]

Premises used: CategoryTheory.Under.comp_right
-- Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Products
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
c₁ c₂ : BinaryCofan (Under.mk f) (Under.mk g)
a : c₁ ⟶ c₂
⊢ Eq (α :=
    (span f g).obj (some WalkingPair.left) ⟶ (PushoutCocone.mk (Under.Hom.right c₂.inl) (Under.Hom.right c₂.inr) ⋯).pt)
    ((PushoutCocone.mk (Under.Hom.right c₁.inl) (Under.Hom.right c₁.inr) ⋯).ι.app (some WalkingPair.left) ≫
      Under.Hom.right a.hom)
    ((PushoutCocone.mk (Under.Hom.right c₂.inl) (Under.Hom.right c₂.inr) ⋯).ι.app (some WalkingPair.left))

Tactic:
simp [← Under.comp_right]

Premises used: CategoryTheory.Under.comp_right
-- Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Products
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
c₁ c₂ : BinaryCofan (Under.mk f) (Under.mk g)
a : c₁ ⟶ c₂
⊢ Eq (α :=
    (span f g).obj (some WalkingPair.right) ⟶ (PushoutCocone.mk (Under.Hom.right c₂.inl) (Under.Hom.right c₂.inr) ⋯).pt)
    ((PushoutCocone.mk (Under.Hom.right c₁.inl) (Under.Hom.right c₁.inr) ⋯).ι.app (some WalkingPair.right) ≫
      Under.Hom.right a.hom)
    ((PushoutCocone.mk (Under.Hom.right c₂.inl) (Under.Hom.right c₂.inr) ⋯).ι.app (some WalkingPair.right))

Tactic:
simp [← Under.comp_right]

Premises used: CategoryTheory.Under.comp_right