awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z P : C
c : BinaryFan.{v, u} X Y
hc : IsLimit c
s : BinaryCofan.{v, u} (op X) (op Y)
m :
  op
      (Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const (Discrete WalkingPair)) c.pt)
        { as := WalkingPair.left : Discrete WalkingPair }) ⟶
    s.pt
h₁ : c.fst.op ≫ m = s.inl
h₂ : c.snd.op ≫ m = s.inr
⊢ m.unop ≫ c.fst =
    Quiver.Hom.unop
        ((fun (s : BinaryCofan.{v, u} (op X) (op Y)) ↦ (Quiver.Hom.op (hc.lift s.unop) : op c.pt ⟶ op s.unop.pt)) s) ≫
      c.fst

Tactic:
simp [← h₁]
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z P : C
c : BinaryFan.{v, u} X Y
hc : IsLimit c
s : BinaryCofan.{v, u} (op X) (op Y)
m :
  op
      (Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const (Discrete WalkingPair)) c.pt)
        { as := WalkingPair.left : Discrete WalkingPair }) ⟶
    s.pt
h₁ : c.fst.op ≫ m = s.inl
h₂ : c.snd.op ≫ m = s.inr
⊢ m.unop ≫ c.snd =
    Quiver.Hom.unop
        ((fun (s : BinaryCofan.{v, u} (op X) (op Y)) ↦ (Quiver.Hom.op (hc.lift s.unop) : op c.pt ⟶ op s.unop.pt)) s) ≫
      c.snd

Tactic:
simp [← h₂]
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z P : C
c : BinaryCofan.{v, u} X Y
hc : IsColimit c
x : BinaryFan.{v, u} (op X) (op Y)
⊢ Quiver.Hom.unop
      ((fun (s : BinaryFan.{v, u} (op X) (op Y)) ↦ (Quiver.Hom.op (hc.desc s.unop) : op s.unop.pt ⟶ op c.pt)) x ≫
        c.inl.op) =
    x.fst.unop

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z P : C
c : BinaryCofan.{v, u} X Y
hc : IsColimit c
x : BinaryFan.{v, u} (op X) (op Y)
⊢ Quiver.Hom.unop
      ((fun (s : BinaryFan.{v, u} (op X) (op Y)) ↦ (Quiver.Hom.op (hc.desc s.unop) : op s.unop.pt ⟶ op c.pt)) x ≫
        c.inr.op) =
    x.snd.unop

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z P : C
c : BinaryCofan.{v, u} X Y
hc : IsColimit c
s : BinaryFan.{v, u} (op X) (op Y)
m :
  s.pt ⟶
    op
      (Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const (Discrete WalkingPair)) c.pt)
        { as := WalkingPair.left : Discrete WalkingPair })
h₁ : m ≫ c.inl.op = s.fst
h₂ : m ≫ c.inr.op = s.snd
⊢ c.inl ≫ m.unop =
    c.inl ≫
      Quiver.Hom.unop
        ((fun (s : BinaryFan.{v, u} (op X) (op Y)) ↦ (Quiver.Hom.op (hc.desc s.unop) : op s.unop.pt ⟶ op c.pt)) s)

Tactic:
simp [← h₁]
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z P : C
c : BinaryCofan.{v, u} X Y
hc : IsColimit c
s : BinaryFan.{v, u} (op X) (op Y)
m :
  s.pt ⟶
    op
      (Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const (Discrete WalkingPair)) c.pt)
        { as := WalkingPair.left : Discrete WalkingPair })
h₁ : m ≫ c.inl.op = s.fst
h₂ : m ≫ c.inr.op = s.snd
⊢ c.inr ≫ m.unop =
    c.inr ≫
      Quiver.Hom.unop
        ((fun (s : BinaryFan.{v, u} (op X) (op Y)) ↦ (Quiver.Hom.op (hc.desc s.unop) : op s.unop.pt ⟶ op c.pt)) s)

Tactic:
simp [← h₂]
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z P : C
c : BinaryFan.{v, u} (op X) (op Y)
hc : IsLimit c
x : BinaryCofan.{v, u} X Y
⊢ Quiver.Hom.op
      (c.fst.unop ≫
        (fun (s : BinaryCofan.{v, u} X Y) ↦ (Quiver.Hom.unop (hc.lift s.op) : unop c.pt ⟶ unop s.op.pt)) x) =
    x.inl.op

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z P : C
c : BinaryFan.{v, u} (op X) (op Y)
hc : IsLimit c
x : BinaryCofan.{v, u} X Y
⊢ Quiver.Hom.op
      (c.snd.unop ≫
        (fun (s : BinaryCofan.{v, u} X Y) ↦ (Quiver.Hom.unop (hc.lift s.op) : unop c.pt ⟶ unop s.op.pt)) x) =
    x.inr.op

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z P : C
c : BinaryFan.{v, u} (op X) (op Y)
hc : IsLimit c
s : BinaryCofan.{v, u} X Y
m :
  unop
      (Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const (Discrete WalkingPair)) c.pt)
        { as := WalkingPair.left : Discrete WalkingPair }) ⟶
    s.pt
h₁ : c.fst.unop ≫ m = s.inl
h₂ : c.snd.unop ≫ m = s.inr
⊢ Eq (α := op s.pt ⟶ Functor.obj.{0, v, 0, u} (pair (op X) (op Y)) { as := WalkingPair.left : Discrete WalkingPair })
    (m.op ≫ c.fst)
    (Quiver.Hom.op
        ((fun (s : BinaryCofan.{v, u} X Y) ↦ (Quiver.Hom.unop (hc.lift s.op) : unop c.pt ⟶ unop s.op.pt)) s) ≫
      c.fst)

Tactic:
simp [← h₁]
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z P : C
c : BinaryFan.{v, u} (op X) (op Y)
hc : IsLimit c
s : BinaryCofan.{v, u} X Y
m :
  unop
      (Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const (Discrete WalkingPair)) c.pt)
        { as := WalkingPair.left : Discrete WalkingPair }) ⟶
    s.pt
h₁ : c.fst.unop ≫ m = s.inl
h₂ : c.snd.unop ≫ m = s.inr
⊢ Eq (α := op s.pt ⟶ Functor.obj.{0, v, 0, u} (pair (op X) (op Y)) { as := WalkingPair.right : Discrete WalkingPair })
    (m.op ≫ c.snd)
    (Quiver.Hom.op
        ((fun (s : BinaryCofan.{v, u} X Y) ↦ (Quiver.Hom.unop (hc.lift s.op) : unop c.pt ⟶ unop s.op.pt)) s) ≫
      c.snd)

Tactic:
simp [← h₂]
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z P : C
c : BinaryCofan.{v, u} (op X) (op Y)
hc : IsColimit c
x : BinaryFan.{v, u} X Y
⊢ Quiver.Hom.op
      ((fun (s : BinaryFan.{v, u} X Y) ↦ (Quiver.Hom.unop (hc.desc s.op) : unop s.op.pt ⟶ unop c.pt)) x ≫ c.inl.unop) =
    x.fst.op

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z P : C
c : BinaryCofan.{v, u} (op X) (op Y)
hc : IsColimit c
x : BinaryFan.{v, u} X Y
⊢ Quiver.Hom.op
      ((fun (s : BinaryFan.{v, u} X Y) ↦ (Quiver.Hom.unop (hc.desc s.op) : unop s.op.pt ⟶ unop c.pt)) x ≫ c.inr.unop) =
    x.snd.op

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z P : C
c : BinaryCofan.{v, u} (op X) (op Y)
hc : IsColimit c
s : BinaryFan.{v, u} X Y
m :
  s.pt ⟶
    unop
      (Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const (Discrete WalkingPair)) c.pt)
        { as := WalkingPair.left : Discrete WalkingPair })
h₁ : m ≫ c.inl.unop = s.fst
h₂ : m ≫ c.inr.unop = s.snd
⊢ c.inl ≫ m.op =
    c.inl ≫
      Quiver.Hom.op ((fun (s : BinaryFan.{v, u} X Y) ↦ (Quiver.Hom.unop (hc.desc s.op) : unop s.op.pt ⟶ unop c.pt)) s)

Tactic:
simp [← h₁]
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z P : C
c : BinaryCofan.{v, u} (op X) (op Y)
hc : IsColimit c
s : BinaryFan.{v, u} X Y
m :
  s.pt ⟶
    unop
      (Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const (Discrete WalkingPair)) c.pt)
        { as := WalkingPair.left : Discrete WalkingPair })
h₁ : m ≫ c.inl.unop = s.fst
h₂ : m ≫ c.inr.unop = s.snd
⊢ c.inr ≫ m.op =
    c.inr ≫
      Quiver.Hom.op ((fun (s : BinaryFan.{v, u} X Y) ↦ (Quiver.Hom.unop (hc.desc s.op) : unop s.op.pt ⟶ unop c.pt)) s)

Tactic:
simp [← h₂]
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
s : BinaryFan.{v, u} X Y
⊢ s.swap.fst = s.snd

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
s : BinaryFan.{v, u} X Y
⊢ s.swap.snd = s.fst

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z P : C
s : BinaryFan.{v, u} X Y
t_1 : BinaryFan.{v, u} Y X
I : IsLimit s
t : Cone.{0, v, 0, u} (pair Y X)
⊢ Eq (α := t.pt ⟶ Functor.obj.{0, v, 0, u} (pair Y X) { as := WalkingPair.left : Discrete WalkingPair })
    (I.lift (BinaryFan.swap t) ≫ s.swap.π.app { as := WalkingPair.left : Discrete WalkingPair } :
      t.pt ⟶ Functor.obj.{0, v, 0, u} (pair Y X) { as := WalkingPair.left : Discrete WalkingPair })
    (t.π.app { as := WalkingPair.left } :
      Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const (Discrete WalkingPair)) t.pt)
          { as := WalkingPair.left : Discrete WalkingPair } ⟶
        Functor.obj.{0, v, 0, u} (pair Y X) { as := WalkingPair.left : Discrete WalkingPair })

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z P : C
s : BinaryFan.{v, u} X Y
t_1 : BinaryFan.{v, u} Y X
I : IsLimit s
t : Cone.{0, v, 0, u} (pair Y X)
⊢ Eq (α := t.pt ⟶ Functor.obj.{0, v, 0, u} (pair Y X) { as := WalkingPair.right : Discrete WalkingPair })
    (I.lift (BinaryFan.swap t) ≫ s.swap.π.app { as := WalkingPair.right : Discrete WalkingPair } :
      t.pt ⟶ Functor.obj.{0, v, 0, u} (pair Y X) { as := WalkingPair.right : Discrete WalkingPair })
    (t.π.app { as := WalkingPair.right } :
      Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const (Discrete WalkingPair)) t.pt)
          { as := WalkingPair.right : Discrete WalkingPair } ⟶
        Functor.obj.{0, v, 0, u} (pair Y X) { as := WalkingPair.right : Discrete WalkingPair })

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z P : C
s : BinaryFan.{v, u} X Y
t_1 : BinaryFan.{v, u} Y X
I : IsLimit s
t : Cone.{0, v, 0, u} (pair Y X)
m : t.pt ⟶ s.swap.pt
w : ∀ (j : Discrete WalkingPair), m ≫ s.swap.π.app j = t.π.app j
⊢ (∀ (j : Discrete WalkingPair), m ≫ s.π.app j = (BinaryFan.swap t).π.app j) → m = I.lift (BinaryFan.swap t)

Tactic:
have h := I.uniq (BinaryFan.swap t) m
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z P : C
s : BinaryFan.{v, u} X Y
t_1 : BinaryFan.{v, u} Y X
I : IsLimit s
t : Cone.{0, v, 0, u} (pair Y X)
m : t.pt ⟶ s.swap.pt
w : ∀ (j : Discrete WalkingPair), m ≫ s.swap.π.app j = t.π.app j
h : (∀ (j : Discrete WalkingPair), m ≫ s.π.app j = (BinaryFan.swap t).π.app j) → m = I.lift (BinaryFan.swap t)
rw : ∀ (j : Discrete WalkingPair), m ≫ s.π.app j = (BinaryFan.swap t).π.app j
⊢ m = I.lift (BinaryFan.swap t)

Tactic:
rw [h]
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z P : C
s : BinaryFan.{v, u} X Y
t_1 : BinaryFan.{v, u} Y X
I : IsLimit s
t : Cone.{0, v, 0, u} (pair Y X)
m : t.pt ⟶ s.swap.pt
w : ∀ (j : Discrete WalkingPair), m ≫ s.swap.π.app j = t.π.app j
h : (∀ (j : Discrete WalkingPair), m ≫ s.π.app j = (BinaryFan.swap t).π.app j) → m = I.lift (BinaryFan.swap t)
j : WalkingPair
⊢ Eq (α := t.pt ⟶ Functor.obj.{0, v, 0, u} (pair Y X) { as := (WalkingPair.swap : (a : WalkingPair) → WalkingPair) j })
    (m ≫ s.swap.π.app { as := (WalkingPair.swap : (a : WalkingPair) → WalkingPair) j })
    (t.π.app { as := (WalkingPair.swap : (a : WalkingPair) → WalkingPair) j })

Tactic:
specialize w ⟨WalkingPair.swap j⟩

Premises used: CategoryTheory.Limits.WalkingPair.swap, CategoryTheory.Discrete.mk, DFunLike.coe
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z P : C
s : BinaryFan.{v, u} X Y
t_1 : BinaryFan.{v, u} Y X
I : IsLimit s
t : Cone.{0, v, 0, u} (pair Y X)
m : t.pt ⟶ s.swap.pt
h : (∀ (j : Discrete WalkingPair), m ≫ s.π.app j = (BinaryFan.swap t).π.app j) → m = I.lift (BinaryFan.swap t)
j : WalkingPair
w :
  Eq (α := t.pt ⟶ Functor.obj.{0, v, 0, u} (pair Y X) { as := (WalkingPair.swap : (a : WalkingPair) → WalkingPair) j })
    (m ≫ s.swap.π.app { as := (WalkingPair.swap : (a : WalkingPair) → WalkingPair) j })
    (t.π.app { as := (WalkingPair.swap : (a : WalkingPair) → WalkingPair) j })
left :
  ∀
    (w :
      Eq (α :=
        t.pt ⟶
          Functor.obj.{0, v, 0, u} (pair Y X)
            { as := (WalkingPair.swap : (a : WalkingPair) → WalkingPair) WalkingPair.left })
        (m ≫ s.swap.π.app { as := (WalkingPair.swap : (a : WalkingPair) → WalkingPair) WalkingPair.left })
        (t.π.app { as := (WalkingPair.swap : (a : WalkingPair) → WalkingPair) WalkingPair.left })),
    Eq (α :=
      (BinaryFan.swap t).pt ⟶ Functor.obj.{0, v, 0, u} (pair X Y) { as := WalkingPair.left : Discrete WalkingPair })
      (m ≫ s.π.app { as := WalkingPair.left }) ((BinaryFan.swap t).π.app { as := WalkingPair.left })
right :
  ∀
    (w :
      Eq (α :=
        t.pt ⟶
          Functor.obj.{0, v, 0, u} (pair Y X)
            { as := (WalkingPair.swap : (a : WalkingPair) → WalkingPair) WalkingPair.right })
        (m ≫ s.swap.π.app { as := (WalkingPair.swap : (a : WalkingPair) → WalkingPair) WalkingPair.right })
        (t.π.app { as := (WalkingPair.swap : (a : WalkingPair) → WalkingPair) WalkingPair.right })),
    Eq (α :=
      (BinaryFan.swap t).pt ⟶ Functor.obj.{0, v, 0, u} (pair X Y) { as := WalkingPair.right : Discrete WalkingPair })
      (m ≫ s.π.app { as := WalkingPair.right }) ((BinaryFan.swap t).π.app { as := WalkingPair.right })
⊢ Eq (α := (BinaryFan.swap t).pt ⟶ Functor.obj.{0, v, 0, u} (pair X Y) { as := j : Discrete WalkingPair })
    (m ≫ s.π.app { as := j }) ((BinaryFan.swap t).π.app { as := j })

Tactic:
cases j
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z P : C
s : BinaryFan.{v, u} X Y
t_1 : BinaryFan.{v, u} Y X
I : IsLimit s
t : Cone.{0, v, 0, u} (pair Y X)
m : t.pt ⟶ s.swap.pt
h : (∀ (j : Discrete WalkingPair), m ≫ s.π.app j = (BinaryFan.swap t).π.app j) → m = I.lift (BinaryFan.swap t)
w :
  Eq (α :=
    t.pt ⟶
      Functor.obj.{0, v, 0, u} (pair Y X)
        { as := (WalkingPair.swap : (a : WalkingPair) → WalkingPair) WalkingPair.left })
    (m ≫ s.swap.π.app { as := (WalkingPair.swap : (a : WalkingPair) → WalkingPair) WalkingPair.left })
    (t.π.app { as := (WalkingPair.swap : (a : WalkingPair) → WalkingPair) WalkingPair.left })
⊢ Eq (α :=
    (BinaryFan.swap t).pt ⟶ Functor.obj.{0, v, 0, u} (pair X Y) { as := WalkingPair.left : Discrete WalkingPair })
    (m ≫ s.π.app { as := WalkingPair.left }) ((BinaryFan.swap t).π.app { as := WalkingPair.left })

Tactic:
w

Premises used: CategoryTheory.Discrete.functor, CategoryTheory.Limits.pair
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z P : C
s : BinaryFan.{v, u} X Y
t_1 : BinaryFan.{v, u} Y X
I : IsLimit s
t : Cone.{0, v, 0, u} (pair Y X)
m : t.pt ⟶ s.swap.pt
h : (∀ (j : Discrete WalkingPair), m ≫ s.π.app j = (BinaryFan.swap t).π.app j) → m = I.lift (BinaryFan.swap t)
w :
  Eq (α :=
    t.pt ⟶
      Functor.obj.{0, v, 0, u} (pair Y X)
        { as := (WalkingPair.swap : (a : WalkingPair) → WalkingPair) WalkingPair.left })
    (m ≫ s.swap.π.app { as := (WalkingPair.swap : (a : WalkingPair) → WalkingPair) WalkingPair.left })
    (t.π.app { as := (WalkingPair.swap : (a : WalkingPair) → WalkingPair) WalkingPair.left })
⊢ Eq (α :=
    (BinaryFan.swap t).pt ⟶ Functor.obj.{0, v, 0, u} (pair X Y) { as := WalkingPair.left : Discrete WalkingPair })
    (m ≫ s.π.app { as := WalkingPair.left }) ((BinaryFan.swap t).π.app { as := WalkingPair.left })

Tactic:
exact w
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z P : C
s : BinaryFan.{v, u} X Y
t_1 : BinaryFan.{v, u} Y X
I : IsLimit s
t : Cone.{0, v, 0, u} (pair Y X)
m : t.pt ⟶ s.swap.pt
h : (∀ (j : Discrete WalkingPair), m ≫ s.π.app j = (BinaryFan.swap t).π.app j) → m = I.lift (BinaryFan.swap t)
w :
  Eq (α :=
    t.pt ⟶
      Functor.obj.{0, v, 0, u} (pair Y X)
        { as := (WalkingPair.swap : (a : WalkingPair) → WalkingPair) WalkingPair.right })
    (m ≫ s.swap.π.app { as := (WalkingPair.swap : (a : WalkingPair) → WalkingPair) WalkingPair.right })
    (t.π.app { as := (WalkingPair.swap : (a : WalkingPair) → WalkingPair) WalkingPair.right })
⊢ Eq (α :=
    (BinaryFan.swap t).pt ⟶ Functor.obj.{0, v, 0, u} (pair X Y) { as := WalkingPair.right : Discrete WalkingPair })
    (m ≫ s.π.app { as := WalkingPair.right }) ((BinaryFan.swap t).π.app { as := WalkingPair.right })

Tactic:
w

Premises used: CategoryTheory.Discrete.functor, CategoryTheory.Limits.pair
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z P : C
s : BinaryFan.{v, u} X Y
t_1 : BinaryFan.{v, u} Y X
I : IsLimit s
t : Cone.{0, v, 0, u} (pair Y X)
m : t.pt ⟶ s.swap.pt
h : (∀ (j : Discrete WalkingPair), m ≫ s.π.app j = (BinaryFan.swap t).π.app j) → m = I.lift (BinaryFan.swap t)
w :
  Eq (α :=
    t.pt ⟶
      Functor.obj.{0, v, 0, u} (pair Y X)
        { as := (WalkingPair.swap : (a : WalkingPair) → WalkingPair) WalkingPair.right })
    (m ≫ s.swap.π.app { as := (WalkingPair.swap : (a : WalkingPair) → WalkingPair) WalkingPair.right })
    (t.π.app { as := (WalkingPair.swap : (a : WalkingPair) → WalkingPair) WalkingPair.right })
⊢ Eq (α :=
    (BinaryFan.swap t).pt ⟶ Functor.obj.{0, v, 0, u} (pair X Y) { as := WalkingPair.right : Discrete WalkingPair })
    (m ≫ s.π.app { as := WalkingPair.right }) ((BinaryFan.swap t).π.app { as := WalkingPair.right })

Tactic:
exact w
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
inst_1 : HasBinaryProduct.{v, u} X Y
⊢ HasBinaryProduct.{v, u} Y X

Tactic:
.mk ⟨BinaryFan.swap (limit.cone (pair X Y)), (limit.isLimit (pair X Y)).binaryFanSwap⟩

Premises used: CategoryTheory.Limits.BinaryFan.swap, CategoryTheory.Limits.limit.cone, CategoryTheory.Limits.limit.isLimit, CategoryTheory.Limits.HasLimit.mk, CategoryTheory.Limits.pair, CategoryTheory.Limits.IsLimit.binaryFanSwap, CategoryTheory.Limits.LimitCone.mk
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
s : BinaryFan.{v, u} X Y
P : IsLimit s
t : BinaryFan.{v, u} Y X
Q : IsLimit t
⊢ (braiding P Q).hom ≫ t.fst = s.snd

Tactic:
P.conePointUniqueUpToIso_hom_comp _ ⟨.right⟩

Premises used: CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso_hom_comp, CategoryTheory.Discrete.functor, CategoryTheory.Limits.WalkingPair.right, CategoryTheory.Discrete.mk, CategoryTheory.Limits.pair
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
s : BinaryFan.{v, u} X Y
P : IsLimit s
t : BinaryFan.{v, u} Y X
Q : IsLimit t
⊢ (braiding P Q).hom ≫ t.snd = s.fst

Tactic:
P.conePointUniqueUpToIso_hom_comp _ ⟨.left⟩

Premises used: CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso_hom_comp, CategoryTheory.Discrete.functor, CategoryTheory.Discrete.mk, CategoryTheory.Limits.pair, CategoryTheory.Limits.WalkingPair.left
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
s : BinaryFan.{v, u} X Y
P : IsLimit s
t : BinaryFan.{v, u} Y X
Q : IsLimit t
⊢ (braiding P Q).inv ≫ s.fst = t.snd

Tactic:
P.conePointUniqueUpToIso_inv_comp _ ⟨.left⟩

Premises used: CategoryTheory.Discrete.functor, CategoryTheory.Discrete.mk, CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso_inv_comp, CategoryTheory.Limits.pair, CategoryTheory.Limits.WalkingPair.left
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
s : BinaryFan.{v, u} X Y
P : IsLimit s
t : BinaryFan.{v, u} Y X
Q : IsLimit t
⊢ (braiding P Q).inv ≫ s.snd = t.fst

Tactic:
P.conePointUniqueUpToIso_inv_comp _ ⟨.right⟩

Premises used: CategoryTheory.Discrete.functor, CategoryTheory.Limits.WalkingPair.right, CategoryTheory.Discrete.mk, CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso_inv_comp, CategoryTheory.Limits.pair
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
sXY : BinaryFan.{v, u} X Y
sYZ : BinaryFan.{v, u} Y Z
Q : IsLimit sYZ
s : BinaryFan.{v, u} sXY.pt Z
⊢ (assoc Q s).fst = s.fst ≫ sXY.fst

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
sXY : BinaryFan.{v, u} X Y
sYZ : BinaryFan.{v, u} Y Z
Q : IsLimit sYZ
s : BinaryFan.{v, u} sXY.pt Z
⊢ (assoc Q s).snd = Q.lift (mk (s.fst ≫ sXY.snd) s.snd)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
sXY : BinaryFan.{v, u} X Y
sYZ : BinaryFan.{v, u} Y Z
P : IsLimit sXY
s : BinaryFan.{v, u} X sYZ.pt
⊢ (assocInv P s).fst = IsLimit.lift P s.fst (s.snd ≫ sYZ.fst)

Tactic:
rfl

Premises used: CategoryTheory.Limits.BinaryFan.IsLimit.lift, rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
sXY : BinaryFan.{v, u} X Y
sYZ : BinaryFan.{v, u} Y Z
P : IsLimit sXY
s : BinaryFan.{v, u} X sYZ.pt
⊢ (assocInv P s).snd = s.snd ≫ sYZ.snd

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z P_1 : C
sXY : BinaryFan.{v, u} X Y
sYZ : BinaryFan.{v, u} Y Z
P : IsLimit sXY
Q : IsLimit sYZ
s : BinaryFan.{v, u} sXY.pt Z
R : IsLimit s
t : Cone.{0, v, 0, u} (pair X sYZ.pt)
⊢ Eq (α := t.pt ⟶ Functor.obj.{0, v, 0, u} (pair X sYZ.pt) { as := WalkingPair.left : Discrete WalkingPair })
    (R.lift (BinaryFan.assocInv P t) ≫ (BinaryFan.assoc Q s).π.app { as := WalkingPair.left : Discrete WalkingPair } :
      t.pt ⟶ Functor.obj.{0, v, 0, u} (pair X sYZ.pt) { as := WalkingPair.left : Discrete WalkingPair })
    (t.π.app { as := WalkingPair.left } :
      Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const (Discrete WalkingPair)) t.pt)
          { as := WalkingPair.left : Discrete WalkingPair } ⟶
        Functor.obj.{0, v, 0, u} (pair X sYZ.pt) { as := WalkingPair.left : Discrete WalkingPair })

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z P_1 : C
sXY : BinaryFan.{v, u} X Y
sYZ : BinaryFan.{v, u} Y Z
P : IsLimit sXY
Q : IsLimit sYZ
s : BinaryFan.{v, u} sXY.pt Z
R : IsLimit s
t : Cone.{0, v, 0, u} (pair X sYZ.pt)
right :
  ∀ (j : Discrete WalkingPair),
    Eq (α := t.pt ⟶ Functor.obj.{0, v, 0, u} (pair Y Z) j)
      ((R.lift (BinaryFan.assocInv P t) ≫
            (BinaryFan.assoc Q s).π.app { as := WalkingPair.right : Discrete WalkingPair }) ≫
          sYZ.π.app j :
        t.pt ⟶ Functor.obj.{0, v, 0, u} (pair Y Z) j)
      (t.π.app { as := WalkingPair.right } ≫ sYZ.π.app j : t.pt ⟶ Functor.obj.{0, v, 0, u} (pair Y Z) j)
⊢ Eq (α := t.pt ⟶ Functor.obj.{0, v, 0, u} (pair X sYZ.pt) { as := WalkingPair.right : Discrete WalkingPair })
    (R.lift (BinaryFan.assocInv P t) ≫ (BinaryFan.assoc Q s).π.app { as := WalkingPair.right : Discrete WalkingPair } :
      t.pt ⟶ Functor.obj.{0, v, 0, u} (pair X sYZ.pt) { as := WalkingPair.right : Discrete WalkingPair })
    (t.π.app { as := WalkingPair.right } :
      Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const (Discrete WalkingPair)) t.pt)
          { as := WalkingPair.right : Discrete WalkingPair } ⟶
        Functor.obj.{0, v, 0, u} (pair X sYZ.pt) { as := WalkingPair.right : Discrete WalkingPair })

Tactic:
apply Q.hom_ext

Premises used: CategoryTheory.Limits.IsLimit.hom_ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z P_1 : C
sXY : BinaryFan.{v, u} X Y
sYZ : BinaryFan.{v, u} Y Z
P : IsLimit sXY
Q : IsLimit sYZ
s : BinaryFan.{v, u} sXY.pt Z
R : IsLimit s
t : Cone.{0, v, 0, u} (pair X sYZ.pt)
⊢ Eq (α := t.pt ⟶ Functor.obj.{0, v, 0, u} (pair Y Z) { as := WalkingPair.left : Discrete WalkingPair })
    ((R.lift (BinaryFan.assocInv P t) ≫
          (BinaryFan.assoc Q s).π.app { as := WalkingPair.right : Discrete WalkingPair }) ≫
        sYZ.π.app { as := WalkingPair.left : Discrete WalkingPair } :
      t.pt ⟶ Functor.obj.{0, v, 0, u} (pair Y Z) { as := WalkingPair.left : Discrete WalkingPair })
    (CategoryStruct.comp (Y := sYZ.pt)
        (t.π.app { as := WalkingPair.right } :
          Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const (Discrete WalkingPair)) t.pt)
              { as := WalkingPair.right : Discrete WalkingPair } ⟶
            Functor.obj.{0, v, 0, u} (pair X sYZ.pt) { as := WalkingPair.right : Discrete WalkingPair })
        (sYZ.π.app { as := WalkingPair.left }) :
      t.pt ⟶ Functor.obj.{0, v, 0, u} (pair Y Z) { as := WalkingPair.left : Discrete WalkingPair })

Tactic:
simp