[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y P Q : C
t : BinaryFan P Q
I : IsLimit t
s : Cone (pair Q P)
⊢ ∀ (j : Discrete WalkingPair),
    (fun s => lift I (BinaryFan.swap s)) s ≫ NatTrans.app (BinaryFan.swap t).π j = NatTrans.app s.π j
[PROOFSTEP]
rintro ⟨⟨⟩⟩
[GOAL]
case mk.left
C : Type u
inst✝ : Category.{v, u} C
X Y P Q : C
t : BinaryFan P Q
I : IsLimit t
s : Cone (pair Q P)
⊢ (fun s => lift I (BinaryFan.swap s)) s ≫ NatTrans.app (BinaryFan.swap t).π { as := WalkingPair.left } =
    NatTrans.app s.π { as := WalkingPair.left }
[PROOFSTEP]
simp
[GOAL]
case mk.right
C : Type u
inst✝ : Category.{v, u} C
X Y P Q : C
t : BinaryFan P Q
I : IsLimit t
s : Cone (pair Q P)
⊢ (fun s => lift I (BinaryFan.swap s)) s ≫ NatTrans.app (BinaryFan.swap t).π { as := WalkingPair.right } =
    NatTrans.app s.π { as := WalkingPair.right }
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y P Q : C
t : BinaryFan P Q
I : IsLimit t
s : Cone (pair Q P)
m : s.pt ⟶ (BinaryFan.swap t).pt
w : ∀ (j : Discrete WalkingPair), m ≫ NatTrans.app (BinaryFan.swap t).π j = NatTrans.app s.π j
⊢ m = (fun s => lift I (BinaryFan.swap s)) s
[PROOFSTEP]
have h := I.uniq (BinaryFan.swap s) m
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y P Q : C
t : BinaryFan P Q
I : IsLimit t
s : Cone (pair Q P)
m : s.pt ⟶ (BinaryFan.swap t).pt
w : ∀ (j : Discrete WalkingPair), m ≫ NatTrans.app (BinaryFan.swap t).π j = NatTrans.app s.π j
h :
  (∀ (j : Discrete WalkingPair), m ≫ NatTrans.app t.π j = NatTrans.app (BinaryFan.swap s).π j) →
    m = lift I (BinaryFan.swap s)
⊢ m = (fun s => lift I (BinaryFan.swap s)) s
[PROOFSTEP]
rw [h]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y P Q : C
t : BinaryFan P Q
I : IsLimit t
s : Cone (pair Q P)
m : s.pt ⟶ (BinaryFan.swap t).pt
w : ∀ (j : Discrete WalkingPair), m ≫ NatTrans.app (BinaryFan.swap t).π j = NatTrans.app s.π j
h :
  (∀ (j : Discrete WalkingPair), m ≫ NatTrans.app t.π j = NatTrans.app (BinaryFan.swap s).π j) →
    m = lift I (BinaryFan.swap s)
⊢ ∀ (j : Discrete WalkingPair), m ≫ NatTrans.app t.π j = NatTrans.app (BinaryFan.swap s).π j
[PROOFSTEP]
rintro ⟨j⟩
[GOAL]
case mk
C : Type u
inst✝ : Category.{v, u} C
X Y P Q : C
t : BinaryFan P Q
I : IsLimit t
s : Cone (pair Q P)
m : s.pt ⟶ (BinaryFan.swap t).pt
w : ∀ (j : Discrete WalkingPair), m ≫ NatTrans.app (BinaryFan.swap t).π j = NatTrans.app s.π j
h :
  (∀ (j : Discrete WalkingPair), m ≫ NatTrans.app t.π j = NatTrans.app (BinaryFan.swap s).π j) →
    m = lift I (BinaryFan.swap s)
j : WalkingPair
⊢ m ≫ NatTrans.app t.π { as := j } = NatTrans.app (BinaryFan.swap s).π { as := j }
[PROOFSTEP]
specialize w ⟨WalkingPair.swap j⟩
[GOAL]
case mk
C : Type u
inst✝ : Category.{v, u} C
X Y P Q : C
t : BinaryFan P Q
I : IsLimit t
s : Cone (pair Q P)
m : s.pt ⟶ (BinaryFan.swap t).pt
h :
  (∀ (j : Discrete WalkingPair), m ≫ NatTrans.app t.π j = NatTrans.app (BinaryFan.swap s).π j) →
    m = lift I (BinaryFan.swap s)
j : WalkingPair
w : m ≫ NatTrans.app (BinaryFan.swap t).π { as := ↑WalkingPair.swap j } = NatTrans.app s.π { as := ↑WalkingPair.swap j }
⊢ m ≫ NatTrans.app t.π { as := j } = NatTrans.app (BinaryFan.swap s).π { as := j }
[PROOFSTEP]
cases j
[GOAL]
case mk.left
C : Type u
inst✝ : Category.{v, u} C
X Y P Q : C
t : BinaryFan P Q
I : IsLimit t
s : Cone (pair Q P)
m : s.pt ⟶ (BinaryFan.swap t).pt
h :
  (∀ (j : Discrete WalkingPair), m ≫ NatTrans.app t.π j = NatTrans.app (BinaryFan.swap s).π j) →
    m = lift I (BinaryFan.swap s)
w :
  m ≫ NatTrans.app (BinaryFan.swap t).π { as := ↑WalkingPair.swap WalkingPair.left } =
    NatTrans.app s.π { as := ↑WalkingPair.swap WalkingPair.left }
⊢ m ≫ NatTrans.app t.π { as := WalkingPair.left } = NatTrans.app (BinaryFan.swap s).π { as := WalkingPair.left }
[PROOFSTEP]
exact w
[GOAL]
case mk.right
C : Type u
inst✝ : Category.{v, u} C
X Y P Q : C
t : BinaryFan P Q
I : IsLimit t
s : Cone (pair Q P)
m : s.pt ⟶ (BinaryFan.swap t).pt
h :
  (∀ (j : Discrete WalkingPair), m ≫ NatTrans.app t.π j = NatTrans.app (BinaryFan.swap s).π j) →
    m = lift I (BinaryFan.swap s)
w :
  m ≫ NatTrans.app (BinaryFan.swap t).π { as := ↑WalkingPair.swap WalkingPair.right } =
    NatTrans.app s.π { as := ↑WalkingPair.swap WalkingPair.right }
⊢ m ≫ NatTrans.app t.π { as := WalkingPair.right } = NatTrans.app (BinaryFan.swap s).π { as := WalkingPair.right }
[PROOFSTEP]
exact w
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ X Y Z : C
sXY : BinaryFan X Y
P : IsLimit sXY
sYZ : BinaryFan Y Z
Q : IsLimit sYZ
s : BinaryFan sXY.pt Z
R : IsLimit s
t : Cone (pair X sYZ.pt)
⊢ ∀ (j : Discrete WalkingPair),
    (fun t => lift R (BinaryFan.assocInv P t)) t ≫ NatTrans.app (BinaryFan.assoc Q s).π j = NatTrans.app t.π j
[PROOFSTEP]
rintro ⟨⟨⟩⟩
[GOAL]
case mk.left
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ X Y Z : C
sXY : BinaryFan X Y
P : IsLimit sXY
sYZ : BinaryFan Y Z
Q : IsLimit sYZ
s : BinaryFan sXY.pt Z
R : IsLimit s
t : Cone (pair X sYZ.pt)
⊢ (fun t => lift R (BinaryFan.assocInv P t)) t ≫ NatTrans.app (BinaryFan.assoc Q s).π { as := WalkingPair.left } =
    NatTrans.app t.π { as := WalkingPair.left }
[PROOFSTEP]
simp
[GOAL]
case mk.right
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ X Y Z : C
sXY : BinaryFan X Y
P : IsLimit sXY
sYZ : BinaryFan Y Z
Q : IsLimit sYZ
s : BinaryFan sXY.pt Z
R : IsLimit s
t : Cone (pair X sYZ.pt)
⊢ (fun t => lift R (BinaryFan.assocInv P t)) t ≫ NatTrans.app (BinaryFan.assoc Q s).π { as := WalkingPair.right } =
    NatTrans.app t.π { as := WalkingPair.right }
[PROOFSTEP]
simp
[GOAL]
case mk.right
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ X Y Z : C
sXY : BinaryFan X Y
P : IsLimit sXY
sYZ : BinaryFan Y Z
Q : IsLimit sYZ
s : BinaryFan sXY.pt Z
R : IsLimit s
t : Cone (pair X sYZ.pt)
⊢ lift R (BinaryFan.assocInv P t) ≫ lift Q (BinaryFan.mk (BinaryFan.fst s ≫ BinaryFan.snd sXY) (BinaryFan.snd s)) =
    BinaryFan.snd t
[PROOFSTEP]
apply Q.hom_ext
[GOAL]
case mk.right
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ X Y Z : C
sXY : BinaryFan X Y
P : IsLimit sXY
sYZ : BinaryFan Y Z
Q : IsLimit sYZ
s : BinaryFan sXY.pt Z
R : IsLimit s
t : Cone (pair X sYZ.pt)
⊢ ∀ (j : Discrete WalkingPair),
    (lift R (BinaryFan.assocInv P t) ≫ lift Q (BinaryFan.mk (BinaryFan.fst s ≫ BinaryFan.snd sXY) (BinaryFan.snd s))) ≫
        NatTrans.app sYZ.π j =
      BinaryFan.snd t ≫ NatTrans.app sYZ.π j
[PROOFSTEP]
rintro ⟨⟨⟩⟩
[GOAL]
case mk.right.mk.left
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ X Y Z : C
sXY : BinaryFan X Y
P : IsLimit sXY
sYZ : BinaryFan Y Z
Q : IsLimit sYZ
s : BinaryFan sXY.pt Z
R : IsLimit s
t : Cone (pair X sYZ.pt)
⊢ (lift R (BinaryFan.assocInv P t) ≫ lift Q (BinaryFan.mk (BinaryFan.fst s ≫ BinaryFan.snd sXY) (BinaryFan.snd s))) ≫
      NatTrans.app sYZ.π { as := WalkingPair.left } =
    BinaryFan.snd t ≫ NatTrans.app sYZ.π { as := WalkingPair.left }
[PROOFSTEP]
simp
[GOAL]
case mk.right.mk.right
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ X Y Z : C
sXY : BinaryFan X Y
P : IsLimit sXY
sYZ : BinaryFan Y Z
Q : IsLimit sYZ
s : BinaryFan sXY.pt Z
R : IsLimit s
t : Cone (pair X sYZ.pt)
⊢ (lift R (BinaryFan.assocInv P t) ≫ lift Q (BinaryFan.mk (BinaryFan.fst s ≫ BinaryFan.snd sXY) (BinaryFan.snd s))) ≫
      NatTrans.app sYZ.π { as := WalkingPair.right } =
    BinaryFan.snd t ≫ NatTrans.app sYZ.π { as := WalkingPair.right }
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ X Y Z : C
sXY : BinaryFan X Y
P : IsLimit sXY
sYZ : BinaryFan Y Z
Q : IsLimit sYZ
s : BinaryFan sXY.pt Z
R : IsLimit s
t : Cone (pair X sYZ.pt)
m : t.pt ⟶ (BinaryFan.assoc Q s).pt
w : ∀ (j : Discrete WalkingPair), m ≫ NatTrans.app (BinaryFan.assoc Q s).π j = NatTrans.app t.π j
⊢ m = (fun t => lift R (BinaryFan.assocInv P t)) t
[PROOFSTEP]
have h := R.uniq (BinaryFan.assocInv P t) m
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ X Y Z : C
sXY : BinaryFan X Y
P : IsLimit sXY
sYZ : BinaryFan Y Z
Q : IsLimit sYZ
s : BinaryFan sXY.pt Z
R : IsLimit s
t : Cone (pair X sYZ.pt)
m : t.pt ⟶ (BinaryFan.assoc Q s).pt
w : ∀ (j : Discrete WalkingPair), m ≫ NatTrans.app (BinaryFan.assoc Q s).π j = NatTrans.app t.π j
h :
  (∀ (j : Discrete WalkingPair), m ≫ NatTrans.app s.π j = NatTrans.app (BinaryFan.assocInv P t).π j) →
    m = lift R (BinaryFan.assocInv P t)
⊢ m = (fun t => lift R (BinaryFan.assocInv P t)) t
[PROOFSTEP]
rw [h]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ X Y Z : C
sXY : BinaryFan X Y
P : IsLimit sXY
sYZ : BinaryFan Y Z
Q : IsLimit sYZ
s : BinaryFan sXY.pt Z
R : IsLimit s
t : Cone (pair X sYZ.pt)
m : t.pt ⟶ (BinaryFan.assoc Q s).pt
w : ∀ (j : Discrete WalkingPair), m ≫ NatTrans.app (BinaryFan.assoc Q s).π j = NatTrans.app t.π j
h :
  (∀ (j : Discrete WalkingPair), m ≫ NatTrans.app s.π j = NatTrans.app (BinaryFan.assocInv P t).π j) →
    m = lift R (BinaryFan.assocInv P t)
⊢ ∀ (j : Discrete WalkingPair), m ≫ NatTrans.app s.π j = NatTrans.app (BinaryFan.assocInv P t).π j
[PROOFSTEP]
rintro ⟨⟨⟩⟩
[GOAL]
case mk.left
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ X Y Z : C
sXY : BinaryFan X Y
P : IsLimit sXY
sYZ : BinaryFan Y Z
Q : IsLimit sYZ
s : BinaryFan sXY.pt Z
R : IsLimit s
t : Cone (pair X sYZ.pt)
m : t.pt ⟶ (BinaryFan.assoc Q s).pt
w : ∀ (j : Discrete WalkingPair), m ≫ NatTrans.app (BinaryFan.assoc Q s).π j = NatTrans.app t.π j
h :
  (∀ (j : Discrete WalkingPair), m ≫ NatTrans.app s.π j = NatTrans.app (BinaryFan.assocInv P t).π j) →
    m = lift R (BinaryFan.assocInv P t)
⊢ m ≫ NatTrans.app s.π { as := WalkingPair.left } = NatTrans.app (BinaryFan.assocInv P t).π { as := WalkingPair.left }
[PROOFSTEP]
simp
[GOAL]
case mk.right
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ X Y Z : C
sXY : BinaryFan X Y
P : IsLimit sXY
sYZ : BinaryFan Y Z
Q : IsLimit sYZ
s : BinaryFan sXY.pt Z
R : IsLimit s
t : Cone (pair X sYZ.pt)
m : t.pt ⟶ (BinaryFan.assoc Q s).pt
w : ∀ (j : Discrete WalkingPair), m ≫ NatTrans.app (BinaryFan.assoc Q s).π j = NatTrans.app t.π j
h :
  (∀ (j : Discrete WalkingPair), m ≫ NatTrans.app s.π j = NatTrans.app (BinaryFan.assocInv P t).π j) →
    m = lift R (BinaryFan.assocInv P t)
⊢ m ≫ NatTrans.app s.π { as := WalkingPair.right } = NatTrans.app (BinaryFan.assocInv P t).π { as := WalkingPair.right }
[PROOFSTEP]
simp
[GOAL]
case mk.left
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ X Y Z : C
sXY : BinaryFan X Y
P : IsLimit sXY
sYZ : BinaryFan Y Z
Q : IsLimit sYZ
s : BinaryFan sXY.pt Z
R : IsLimit s
t : Cone (pair X sYZ.pt)
m : t.pt ⟶ (BinaryFan.assoc Q s).pt
w : ∀ (j : Discrete WalkingPair), m ≫ NatTrans.app (BinaryFan.assoc Q s).π j = NatTrans.app t.π j
h :
  (∀ (j : Discrete WalkingPair), m ≫ NatTrans.app s.π j = NatTrans.app (BinaryFan.assocInv P t).π j) →
    m = lift R (BinaryFan.assocInv P t)
⊢ m ≫ BinaryFan.fst s = lift P (BinaryFan.mk (BinaryFan.fst t) (BinaryFan.snd t ≫ BinaryFan.fst sYZ))
case mk.right
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ X Y Z : C
sXY : BinaryFan X Y
P : IsLimit sXY
sYZ : BinaryFan Y Z
Q : IsLimit sYZ
s : BinaryFan sXY.pt Z
R : IsLimit s
t : Cone (pair X sYZ.pt)
m : t.pt ⟶ (BinaryFan.assoc Q s).pt
w : ∀ (j : Discrete WalkingPair), m ≫ NatTrans.app (BinaryFan.assoc Q s).π j = NatTrans.app t.π j
h :
  (∀ (j : Discrete WalkingPair), m ≫ NatTrans.app s.π j = NatTrans.app (BinaryFan.assocInv P t).π j) →
    m = lift R (BinaryFan.assocInv P t)
⊢ m ≫ BinaryFan.snd s = BinaryFan.snd t ≫ BinaryFan.snd sYZ
[PROOFSTEP]
apply P.hom_ext
[GOAL]
case mk.left
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ X Y Z : C
sXY : BinaryFan X Y
P : IsLimit sXY
sYZ : BinaryFan Y Z
Q : IsLimit sYZ
s : BinaryFan sXY.pt Z
R : IsLimit s
t : Cone (pair X sYZ.pt)
m : t.pt ⟶ (BinaryFan.assoc Q s).pt
w : ∀ (j : Discrete WalkingPair), m ≫ NatTrans.app (BinaryFan.assoc Q s).π j = NatTrans.app t.π j
h :
  (∀ (j : Discrete WalkingPair), m ≫ NatTrans.app s.π j = NatTrans.app (BinaryFan.assocInv P t).π j) →
    m = lift R (BinaryFan.assocInv P t)
⊢ ∀ (j : Discrete WalkingPair),
    (m ≫ BinaryFan.fst s) ≫ NatTrans.app sXY.π j =
      lift P (BinaryFan.mk (BinaryFan.fst t) (BinaryFan.snd t ≫ BinaryFan.fst sYZ)) ≫ NatTrans.app sXY.π j
[PROOFSTEP]
rintro ⟨⟨⟩⟩
[GOAL]
case mk.left.mk.left
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ X Y Z : C
sXY : BinaryFan X Y
P : IsLimit sXY
sYZ : BinaryFan Y Z
Q : IsLimit sYZ
s : BinaryFan sXY.pt Z
R : IsLimit s
t : Cone (pair X sYZ.pt)
m : t.pt ⟶ (BinaryFan.assoc Q s).pt
w : ∀ (j : Discrete WalkingPair), m ≫ NatTrans.app (BinaryFan.assoc Q s).π j = NatTrans.app t.π j
h :
  (∀ (j : Discrete WalkingPair), m ≫ NatTrans.app s.π j = NatTrans.app (BinaryFan.assocInv P t).π j) →
    m = lift R (BinaryFan.assocInv P t)
⊢ (m ≫ BinaryFan.fst s) ≫ NatTrans.app sXY.π { as := WalkingPair.left } =
    lift P (BinaryFan.mk (BinaryFan.fst t) (BinaryFan.snd t ≫ BinaryFan.fst sYZ)) ≫
      NatTrans.app sXY.π { as := WalkingPair.left }
[PROOFSTEP]
simp
[GOAL]
case mk.left.mk.right
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ X Y Z : C
sXY : BinaryFan X Y
P : IsLimit sXY
sYZ : BinaryFan Y Z
Q : IsLimit sYZ
s : BinaryFan sXY.pt Z
R : IsLimit s
t : Cone (pair X sYZ.pt)
m : t.pt ⟶ (BinaryFan.assoc Q s).pt
w : ∀ (j : Discrete WalkingPair), m ≫ NatTrans.app (BinaryFan.assoc Q s).π j = NatTrans.app t.π j
h :
  (∀ (j : Discrete WalkingPair), m ≫ NatTrans.app s.π j = NatTrans.app (BinaryFan.assocInv P t).π j) →
    m = lift R (BinaryFan.assocInv P t)
⊢ (m ≫ BinaryFan.fst s) ≫ NatTrans.app sXY.π { as := WalkingPair.right } =
    lift P (BinaryFan.mk (BinaryFan.fst t) (BinaryFan.snd t ≫ BinaryFan.fst sYZ)) ≫
      NatTrans.app sXY.π { as := WalkingPair.right }
[PROOFSTEP]
simp
[GOAL]
case mk.left.mk.left
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ X Y Z : C
sXY : BinaryFan X Y
P : IsLimit sXY
sYZ : BinaryFan Y Z
Q : IsLimit sYZ
s : BinaryFan sXY.pt Z
R : IsLimit s
t : Cone (pair X sYZ.pt)
m : t.pt ⟶ (BinaryFan.assoc Q s).pt
w : ∀ (j : Discrete WalkingPair), m ≫ NatTrans.app (BinaryFan.assoc Q s).π j = NatTrans.app t.π j
h :
  (∀ (j : Discrete WalkingPair), m ≫ NatTrans.app s.π j = NatTrans.app (BinaryFan.assocInv P t).π j) →
    m = lift R (BinaryFan.assocInv P t)
⊢ m ≫ BinaryFan.fst s ≫ BinaryFan.fst sXY = BinaryFan.fst t
[PROOFSTEP]
exact w ⟨WalkingPair.left⟩
[GOAL]
case mk.left.mk.right
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ X Y Z : C
sXY : BinaryFan X Y
P : IsLimit sXY
sYZ : BinaryFan Y Z
Q : IsLimit sYZ
s : BinaryFan sXY.pt Z
R : IsLimit s
t : Cone (pair X sYZ.pt)
m : t.pt ⟶ (BinaryFan.assoc Q s).pt
w : ∀ (j : Discrete WalkingPair), m ≫ NatTrans.app (BinaryFan.assoc Q s).π j = NatTrans.app t.π j
h :
  (∀ (j : Discrete WalkingPair), m ≫ NatTrans.app s.π j = NatTrans.app (BinaryFan.assocInv P t).π j) →
    m = lift R (BinaryFan.assocInv P t)
⊢ m ≫ BinaryFan.fst s ≫ BinaryFan.snd sXY = BinaryFan.snd t ≫ BinaryFan.fst sYZ
[PROOFSTEP]
specialize w ⟨WalkingPair.right⟩
[GOAL]
case mk.left.mk.right
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ X Y Z : C
sXY : BinaryFan X Y
P : IsLimit sXY
sYZ : BinaryFan Y Z
Q : IsLimit sYZ
s : BinaryFan sXY.pt Z
R : IsLimit s
t : Cone (pair X sYZ.pt)
m : t.pt ⟶ (BinaryFan.assoc Q s).pt
h :
  (∀ (j : Discrete WalkingPair), m ≫ NatTrans.app s.π j = NatTrans.app (BinaryFan.assocInv P t).π j) →
    m = lift R (BinaryFan.assocInv P t)
w : m ≫ NatTrans.app (BinaryFan.assoc Q s).π { as := WalkingPair.right } = NatTrans.app t.π { as := WalkingPair.right }
⊢ m ≫ BinaryFan.fst s ≫ BinaryFan.snd sXY = BinaryFan.snd t ≫ BinaryFan.fst sYZ
[PROOFSTEP]
simp at w 
[GOAL]
case mk.left.mk.right
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ X Y Z : C
sXY : BinaryFan X Y
P : IsLimit sXY
sYZ : BinaryFan Y Z
Q : IsLimit sYZ
s : BinaryFan sXY.pt Z
R : IsLimit s
t : Cone (pair X sYZ.pt)
m : t.pt ⟶ (BinaryFan.assoc Q s).pt
h :
  (∀ (j : Discrete WalkingPair), m ≫ NatTrans.app s.π j = NatTrans.app (BinaryFan.assocInv P t).π j) →
    m = lift R (BinaryFan.assocInv P t)
w : m ≫ lift Q (BinaryFan.mk (BinaryFan.fst s ≫ BinaryFan.snd sXY) (BinaryFan.snd s)) = BinaryFan.snd t
⊢ m ≫ BinaryFan.fst s ≫ BinaryFan.snd sXY = BinaryFan.snd t ≫ BinaryFan.fst sYZ
[PROOFSTEP]
rw [← w]
[GOAL]
case mk.left.mk.right
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ X Y Z : C
sXY : BinaryFan X Y
P : IsLimit sXY
sYZ : BinaryFan Y Z
Q : IsLimit sYZ
s : BinaryFan sXY.pt Z
R : IsLimit s
t : Cone (pair X sYZ.pt)
m : t.pt ⟶ (BinaryFan.assoc Q s).pt
h :
  (∀ (j : Discrete WalkingPair), m ≫ NatTrans.app s.π j = NatTrans.app (BinaryFan.assocInv P t).π j) →
    m = lift R (BinaryFan.assocInv P t)
w : m ≫ lift Q (BinaryFan.mk (BinaryFan.fst s ≫ BinaryFan.snd sXY) (BinaryFan.snd s)) = BinaryFan.snd t
⊢ m ≫ BinaryFan.fst s ≫ BinaryFan.snd sXY =
    (m ≫ lift Q (BinaryFan.mk (BinaryFan.fst s ≫ BinaryFan.snd sXY) (BinaryFan.snd s))) ≫ BinaryFan.fst sYZ
[PROOFSTEP]
simp
[GOAL]
case mk.right
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ X Y Z : C
sXY : BinaryFan X Y
P : IsLimit sXY
sYZ : BinaryFan Y Z
Q : IsLimit sYZ
s : BinaryFan sXY.pt Z
R : IsLimit s
t : Cone (pair X sYZ.pt)
m : t.pt ⟶ (BinaryFan.assoc Q s).pt
w : ∀ (j : Discrete WalkingPair), m ≫ NatTrans.app (BinaryFan.assoc Q s).π j = NatTrans.app t.π j
h :
  (∀ (j : Discrete WalkingPair), m ≫ NatTrans.app s.π j = NatTrans.app (BinaryFan.assocInv P t).π j) →
    m = lift R (BinaryFan.assocInv P t)
⊢ m ≫ BinaryFan.snd s = BinaryFan.snd t ≫ BinaryFan.snd sYZ
[PROOFSTEP]
specialize w ⟨WalkingPair.right⟩
[GOAL]
case mk.right
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ X Y Z : C
sXY : BinaryFan X Y
P : IsLimit sXY
sYZ : BinaryFan Y Z
Q : IsLimit sYZ
s : BinaryFan sXY.pt Z
R : IsLimit s
t : Cone (pair X sYZ.pt)
m : t.pt ⟶ (BinaryFan.assoc Q s).pt
h :
  (∀ (j : Discrete WalkingPair), m ≫ NatTrans.app s.π j = NatTrans.app (BinaryFan.assocInv P t).π j) →
    m = lift R (BinaryFan.assocInv P t)
w : m ≫ NatTrans.app (BinaryFan.assoc Q s).π { as := WalkingPair.right } = NatTrans.app t.π { as := WalkingPair.right }
⊢ m ≫ BinaryFan.snd s = BinaryFan.snd t ≫ BinaryFan.snd sYZ
[PROOFSTEP]
simp at w 
[GOAL]
case mk.right
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ X Y Z : C
sXY : BinaryFan X Y
P : IsLimit sXY
sYZ : BinaryFan Y Z
Q : IsLimit sYZ
s : BinaryFan sXY.pt Z
R : IsLimit s
t : Cone (pair X sYZ.pt)
m : t.pt ⟶ (BinaryFan.assoc Q s).pt
h :
  (∀ (j : Discrete WalkingPair), m ≫ NatTrans.app s.π j = NatTrans.app (BinaryFan.assocInv P t).π j) →
    m = lift R (BinaryFan.assocInv P t)
w : m ≫ lift Q (BinaryFan.mk (BinaryFan.fst s ≫ BinaryFan.snd sXY) (BinaryFan.snd s)) = BinaryFan.snd t
⊢ m ≫ BinaryFan.snd s = BinaryFan.snd t ≫ BinaryFan.snd sYZ
[PROOFSTEP]
rw [← w]
[GOAL]
case mk.right
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ X Y Z : C
sXY : BinaryFan X Y
P : IsLimit sXY
sYZ : BinaryFan Y Z
Q : IsLimit sYZ
s : BinaryFan sXY.pt Z
R : IsLimit s
t : Cone (pair X sYZ.pt)
m : t.pt ⟶ (BinaryFan.assoc Q s).pt
h :
  (∀ (j : Discrete WalkingPair), m ≫ NatTrans.app s.π j = NatTrans.app (BinaryFan.assocInv P t).π j) →
    m = lift R (BinaryFan.assocInv P t)
w : m ≫ lift Q (BinaryFan.mk (BinaryFan.fst s ≫ BinaryFan.snd sXY) (BinaryFan.snd s)) = BinaryFan.snd t
⊢ m ≫ BinaryFan.snd s =
    (m ≫ lift Q (BinaryFan.mk (BinaryFan.fst s ≫ BinaryFan.snd sXY) (BinaryFan.snd s))) ≫ BinaryFan.snd sYZ
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X✝ Y X : C
s : Cone (Functor.empty C)
P : IsLimit s
t : BinaryFan s.pt X
Q : IsLimit t
⊢ snd t ≫
      IsLimit.lift Q
        (mk
          (IsLimit.lift P
            { pt := X,
              π :=
                NatTrans.mk fun x =>
                  Discrete.rec
                    (fun x =>
                      PEmpty.rec
                        (fun x =>
                          (x : PEmpty) →
                            ((Functor.const (Discrete PEmpty)).obj X).obj { as := x } ⟶
                              (Functor.empty C).obj { as := x })
                        x x)
                    x })
          (𝟙 X)) =
    𝟙 t.pt
[PROOFSTEP]
apply Q.hom_ext
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X✝ Y X : C
s : Cone (Functor.empty C)
P : IsLimit s
t : BinaryFan s.pt X
Q : IsLimit t
⊢ ∀ (j : Discrete WalkingPair),
    (snd t ≫
          IsLimit.lift Q
            (mk
              (IsLimit.lift P
                { pt := X,
                  π :=
                    NatTrans.mk fun x =>
                      Discrete.rec
                        (fun x =>
                          PEmpty.rec
                            (fun x =>
                              (x : PEmpty) →
                                ((Functor.const (Discrete PEmpty)).obj X).obj { as := x } ⟶
                                  (Functor.empty C).obj { as := x })
                            x x)
                        x })
              (𝟙 X))) ≫
        NatTrans.app t.π j =
      𝟙 t.pt ≫ NatTrans.app t.π j
[PROOFSTEP]
rintro ⟨⟨⟩⟩
[GOAL]
case mk.left
C : Type u
inst✝ : Category.{v, u} C
X✝ Y X : C
s : Cone (Functor.empty C)
P : IsLimit s
t : BinaryFan s.pt X
Q : IsLimit t
⊢ (snd t ≫
        IsLimit.lift Q
          (mk
            (IsLimit.lift P
              { pt := X,
                π :=
                  NatTrans.mk fun x =>
                    Discrete.rec
                      (fun x =>
                        PEmpty.rec
                          (fun x =>
                            (x : PEmpty) →
                              ((Functor.const (Discrete PEmpty)).obj X).obj { as := x } ⟶
                                (Functor.empty C).obj { as := x })
                          x x)
                      x })
            (𝟙 X))) ≫
      NatTrans.app t.π { as := WalkingPair.left } =
    𝟙 t.pt ≫ NatTrans.app t.π { as := WalkingPair.left }
[PROOFSTEP]
apply P.hom_ext
[GOAL]
case mk.left
C : Type u
inst✝ : Category.{v, u} C
X✝ Y X : C
s : Cone (Functor.empty C)
P : IsLimit s
t : BinaryFan s.pt X
Q : IsLimit t
⊢ ∀ (j : Discrete PEmpty),
    ((snd t ≫
            IsLimit.lift Q
              (mk
                (IsLimit.lift P
                  { pt := X,
                    π :=
                      NatTrans.mk fun x =>
                        Discrete.rec
                          (fun x =>
                            PEmpty.rec
                              (fun x =>
                                (x : PEmpty) →
                                  ((Functor.const (Discrete PEmpty)).obj X).obj { as := x } ⟶
                                    (Functor.empty C).obj { as := x })
                              x x)
                          x })
                (𝟙 X))) ≫
          NatTrans.app t.π { as := WalkingPair.left }) ≫
        NatTrans.app s.π j =
      (𝟙 t.pt ≫ NatTrans.app t.π { as := WalkingPair.left }) ≫ NatTrans.app s.π j
[PROOFSTEP]
rintro ⟨⟨⟩⟩
[GOAL]
case mk.right
C : Type u
inst✝ : Category.{v, u} C
X✝ Y X : C
s : Cone (Functor.empty C)
P : IsLimit s
t : BinaryFan s.pt X
Q : IsLimit t
⊢ (snd t ≫
        IsLimit.lift Q
          (mk
            (IsLimit.lift P
              { pt := X,
                π :=
                  NatTrans.mk fun x =>
                    Discrete.rec
                      (fun x =>
                        PEmpty.rec
                          (fun x =>
                            (x : PEmpty) →
                              ((Functor.const (Discrete PEmpty)).obj X).obj { as := x } ⟶
                                (Functor.empty C).obj { as := x })
                          x x)
                      x })
            (𝟙 X))) ≫
      NatTrans.app t.π { as := WalkingPair.right } =
    𝟙 t.pt ≫ NatTrans.app t.π { as := WalkingPair.right }
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X✝ Y X : C
s : Cone (Functor.empty C)
P : IsLimit s
t : BinaryFan X s.pt
Q : IsLimit t
⊢ fst t ≫
      IsLimit.lift Q
        (mk (𝟙 X)
          (IsLimit.lift P
            { pt := X,
              π :=
                NatTrans.mk fun x =>
                  Discrete.rec
                    (fun x =>
                      PEmpty.rec
                        (fun x =>
                          (x : PEmpty) →
                            ((Functor.const (Discrete PEmpty)).obj X).obj { as := x } ⟶
                              (Functor.empty C).obj { as := x })
                        x x)
                    x })) =
    𝟙 t.pt
[PROOFSTEP]
apply Q.hom_ext
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X✝ Y X : C
s : Cone (Functor.empty C)
P : IsLimit s
t : BinaryFan X s.pt
Q : IsLimit t
⊢ ∀ (j : Discrete WalkingPair),
    (fst t ≫
          IsLimit.lift Q
            (mk (𝟙 X)
              (IsLimit.lift P
                { pt := X,
                  π :=
                    NatTrans.mk fun x =>
                      Discrete.rec
                        (fun x =>
                          PEmpty.rec
                            (fun x =>
                              (x : PEmpty) →
                                ((Functor.const (Discrete PEmpty)).obj X).obj { as := x } ⟶
                                  (Functor.empty C).obj { as := x })
                            x x)
                        x }))) ≫
        NatTrans.app t.π j =
      𝟙 t.pt ≫ NatTrans.app t.π j
[PROOFSTEP]
rintro ⟨⟨⟩⟩
[GOAL]
case mk.left
C : Type u
inst✝ : Category.{v, u} C
X✝ Y X : C
s : Cone (Functor.empty C)
P : IsLimit s
t : BinaryFan X s.pt
Q : IsLimit t
⊢ (fst t ≫
        IsLimit.lift Q
          (mk (𝟙 X)
            (IsLimit.lift P
              { pt := X,
                π :=
                  NatTrans.mk fun x =>
                    Discrete.rec
                      (fun x =>
                        PEmpty.rec
                          (fun x =>
                            (x : PEmpty) →
                              ((Functor.const (Discrete PEmpty)).obj X).obj { as := x } ⟶
                                (Functor.empty C).obj { as := x })
                          x x)
                      x }))) ≫
      NatTrans.app t.π { as := WalkingPair.left } =
    𝟙 t.pt ≫ NatTrans.app t.π { as := WalkingPair.left }
[PROOFSTEP]
simp
[GOAL]
case mk.right
C : Type u
inst✝ : Category.{v, u} C
X✝ Y X : C
s : Cone (Functor.empty C)
P : IsLimit s
t : BinaryFan X s.pt
Q : IsLimit t
⊢ (fst t ≫
        IsLimit.lift Q
          (mk (𝟙 X)
            (IsLimit.lift P
              { pt := X,
                π :=
                  NatTrans.mk fun x =>
                    Discrete.rec
                      (fun x =>
                        PEmpty.rec
                          (fun x =>
                            (x : PEmpty) →
                              ((Functor.const (Discrete PEmpty)).obj X).obj { as := x } ⟶
                                (Functor.empty C).obj { as := x })
                          x x)
                      x }))) ≫
      NatTrans.app t.π { as := WalkingPair.right } =
    𝟙 t.pt ≫ NatTrans.app t.π { as := WalkingPair.right }
[PROOFSTEP]
apply P.hom_ext
[GOAL]
case mk.right
C : Type u
inst✝ : Category.{v, u} C
X✝ Y X : C
s : Cone (Functor.empty C)
P : IsLimit s
t : BinaryFan X s.pt
Q : IsLimit t
⊢ ∀ (j : Discrete PEmpty),
    ((fst t ≫
            IsLimit.lift Q
              (mk (𝟙 X)
                (IsLimit.lift P
                  { pt := X,
                    π :=
                      NatTrans.mk fun x =>
                        Discrete.rec
                          (fun x =>
                            PEmpty.rec
                              (fun x =>
                                (x : PEmpty) →
                                  ((Functor.const (Discrete PEmpty)).obj X).obj { as := x } ⟶
                                    (Functor.empty C).obj { as := x })
                              x x)
                          x }))) ≫
          NatTrans.app t.π { as := WalkingPair.right }) ≫
        NatTrans.app s.π j =
      (𝟙 t.pt ≫ NatTrans.app t.π { as := WalkingPair.right }) ≫ NatTrans.app s.π j
[PROOFSTEP]
rintro ⟨⟨⟩⟩
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y : C
𝒯 : LimitCone (Functor.empty C)
ℬ : (X Y : C) → LimitCone (pair X Y)
X₁ X₂ : C
⊢ tensorHom ℬ (𝟙 X₁) (𝟙 X₂) = 𝟙 (tensorObj ℬ X₁ X₂)
[PROOFSTEP]
apply IsLimit.hom_ext (ℬ _ _).isLimit
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y : C
𝒯 : LimitCone (Functor.empty C)
ℬ : (X Y : C) → LimitCone (pair X Y)
X₁ X₂ : C
⊢ ∀ (j : Discrete WalkingPair),
    tensorHom ℬ (𝟙 X₁) (𝟙 X₂) ≫ NatTrans.app (ℬ X₁ X₂).cone.π j =
      𝟙 (tensorObj ℬ X₁ X₂) ≫ NatTrans.app (ℬ X₁ X₂).cone.π j
[PROOFSTEP]
rintro ⟨⟨⟩⟩
[GOAL]
case mk.left
C : Type u
inst✝ : Category.{v, u} C
X Y : C
𝒯 : LimitCone (Functor.empty C)
ℬ : (X Y : C) → LimitCone (pair X Y)
X₁ X₂ : C
⊢ tensorHom ℬ (𝟙 X₁) (𝟙 X₂) ≫ NatTrans.app (ℬ X₁ X₂).cone.π { as := WalkingPair.left } =
    𝟙 (tensorObj ℬ X₁ X₂) ≫ NatTrans.app (ℬ X₁ X₂).cone.π { as := WalkingPair.left }
[PROOFSTEP]
dsimp [tensorHom]
[GOAL]
case mk.left
C : Type u
inst✝ : Category.{v, u} C
X Y : C
𝒯 : LimitCone (Functor.empty C)
ℬ : (X Y : C) → LimitCone (pair X Y)
X₁ X₂ : C
⊢ IsLimit.lift (ℬ X₁ X₂).isLimit
        (BinaryFan.mk (BinaryFan.fst (ℬ X₁ X₂).cone ≫ 𝟙 X₁) (BinaryFan.snd (ℬ X₁ X₂).cone ≫ 𝟙 X₂)) ≫
      BinaryFan.fst (ℬ X₁ X₂).cone =
    𝟙 (tensorObj ℬ X₁ X₂) ≫ BinaryFan.fst (ℬ X₁ X₂).cone
[PROOFSTEP]
simp
[GOAL]
case mk.right
C : Type u
inst✝ : Category.{v, u} C
X Y : C
𝒯 : LimitCone (Functor.empty C)
ℬ : (X Y : C) → LimitCone (pair X Y)
X₁ X₂ : C
⊢ tensorHom ℬ (𝟙 X₁) (𝟙 X₂) ≫ NatTrans.app (ℬ X₁ X₂).cone.π { as := WalkingPair.right } =
    𝟙 (tensorObj ℬ X₁ X₂) ≫ NatTrans.app (ℬ X₁ X₂).cone.π { as := WalkingPair.right }
[PROOFSTEP]
dsimp [tensorHom]
[GOAL]
case mk.right
C : Type u
inst✝ : Category.{v, u} C
X Y : C
𝒯 : LimitCone (Functor.empty C)
ℬ : (X Y : C) → LimitCone (pair X Y)
X₁ X₂ : C
⊢ IsLimit.lift (ℬ X₁ X₂).isLimit
        (BinaryFan.mk (BinaryFan.fst (ℬ X₁ X₂).cone ≫ 𝟙 X₁) (BinaryFan.snd (ℬ X₁ X₂).cone ≫ 𝟙 X₂)) ≫
      BinaryFan.snd (ℬ X₁ X₂).cone =
    𝟙 (tensorObj ℬ X₁ X₂) ≫ BinaryFan.snd (ℬ X₁ X₂).cone
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y : C
𝒯 : LimitCone (Functor.empty C)
ℬ : (X Y : C) → LimitCone (pair X Y)
X₁ Y₁ Z₁ X₂ Y₂ Z₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : Y₁ ⟶ Z₁
g₂ : Y₂ ⟶ Z₂
⊢ tensorHom ℬ (f₁ ≫ g₁) (f₂ ≫ g₂) = tensorHom ℬ f₁ f₂ ≫ tensorHom ℬ g₁ g₂
[PROOFSTEP]
apply IsLimit.hom_ext (ℬ _ _).isLimit
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y : C
𝒯 : LimitCone (Functor.empty C)
ℬ : (X Y : C) → LimitCone (pair X Y)
X₁ Y₁ Z₁ X₂ Y₂ Z₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : Y₁ ⟶ Z₁
g₂ : Y₂ ⟶ Z₂
⊢ ∀ (j : Discrete WalkingPair),
    tensorHom ℬ (f₁ ≫ g₁) (f₂ ≫ g₂) ≫ NatTrans.app (ℬ Z₁ Z₂).cone.π j =
      (tensorHom ℬ f₁ f₂ ≫ tensorHom ℬ g₁ g₂) ≫ NatTrans.app (ℬ Z₁ Z₂).cone.π j
[PROOFSTEP]
rintro ⟨⟨⟩⟩
[GOAL]
case mk.left
C : Type u
inst✝ : Category.{v, u} C
X Y : C
𝒯 : LimitCone (Functor.empty C)
ℬ : (X Y : C) → LimitCone (pair X Y)
X₁ Y₁ Z₁ X₂ Y₂ Z₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : Y₁ ⟶ Z₁
g₂ : Y₂ ⟶ Z₂
⊢ tensorHom ℬ (f₁ ≫ g₁) (f₂ ≫ g₂) ≫ NatTrans.app (ℬ Z₁ Z₂).cone.π { as := WalkingPair.left } =
    (tensorHom ℬ f₁ f₂ ≫ tensorHom ℬ g₁ g₂) ≫ NatTrans.app (ℬ Z₁ Z₂).cone.π { as := WalkingPair.left }
[PROOFSTEP]
dsimp [tensorHom]
[GOAL]
case mk.left
C : Type u
inst✝ : Category.{v, u} C
X Y : C
𝒯 : LimitCone (Functor.empty C)
ℬ : (X Y : C) → LimitCone (pair X Y)
X₁ Y₁ Z₁ X₂ Y₂ Z₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : Y₁ ⟶ Z₁
g₂ : Y₂ ⟶ Z₂
⊢ IsLimit.lift (ℬ Z₁ Z₂).isLimit
        (BinaryFan.mk (BinaryFan.fst (ℬ X₁ X₂).cone ≫ f₁ ≫ g₁) (BinaryFan.snd (ℬ X₁ X₂).cone ≫ f₂ ≫ g₂)) ≫
      BinaryFan.fst (ℬ Z₁ Z₂).cone =
    (IsLimit.lift (ℬ Y₁ Y₂).isLimit
          (BinaryFan.mk (BinaryFan.fst (ℬ X₁ X₂).cone ≫ f₁) (BinaryFan.snd (ℬ X₁ X₂).cone ≫ f₂)) ≫
        IsLimit.lift (ℬ Z₁ Z₂).isLimit
          (BinaryFan.mk (BinaryFan.fst (ℬ Y₁ Y₂).cone ≫ g₁) (BinaryFan.snd (ℬ Y₁ Y₂).cone ≫ g₂))) ≫
      BinaryFan.fst (ℬ Z₁ Z₂).cone
[PROOFSTEP]
simp
[GOAL]
case mk.right
C : Type u
inst✝ : Category.{v, u} C
X Y : C
𝒯 : LimitCone (Functor.empty C)
ℬ : (X Y : C) → LimitCone (pair X Y)
X₁ Y₁ Z₁ X₂ Y₂ Z₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : Y₁ ⟶ Z₁
g₂ : Y₂ ⟶ Z₂
⊢ tensorHom ℬ (f₁ ≫ g₁) (f₂ ≫ g₂) ≫ NatTrans.app (ℬ Z₁ Z₂).cone.π { as := WalkingPair.right } =
    (tensorHom ℬ f₁ f₂ ≫ tensorHom ℬ g₁ g₂) ≫ NatTrans.app (ℬ Z₁ Z₂).cone.π { as := WalkingPair.right }
[PROOFSTEP]
dsimp [tensorHom]
[GOAL]
case mk.right
C : Type u
inst✝ : Category.{v, u} C
X Y : C
𝒯 : LimitCone (Functor.empty C)
ℬ : (X Y : C) → LimitCone (pair X Y)
X₁ Y₁ Z₁ X₂ Y₂ Z₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : Y₁ ⟶ Z₁
g₂ : Y₂ ⟶ Z₂
⊢ IsLimit.lift (ℬ Z₁ Z₂).isLimit
        (BinaryFan.mk (BinaryFan.fst (ℬ X₁ X₂).cone ≫ f₁ ≫ g₁) (BinaryFan.snd (ℬ X₁ X₂).cone ≫ f₂ ≫ g₂)) ≫
      BinaryFan.snd (ℬ Z₁ Z₂).cone =
    (IsLimit.lift (ℬ Y₁ Y₂).isLimit
          (BinaryFan.mk (BinaryFan.fst (ℬ X₁ X₂).cone ≫ f₁) (BinaryFan.snd (ℬ X₁ X₂).cone ≫ f₂)) ≫
        IsLimit.lift (ℬ Z₁ Z₂).isLimit
          (BinaryFan.mk (BinaryFan.fst (ℬ Y₁ Y₂).cone ≫ g₁) (BinaryFan.snd (ℬ Y₁ Y₂).cone ≫ g₂))) ≫
      BinaryFan.snd (ℬ Z₁ Z₂).cone
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : C
𝒯 : LimitCone (Functor.empty C)
ℬ : (X Y : C) → LimitCone (pair X Y)
W X Y Z : C
⊢ tensorHom ℬ (BinaryFan.associatorOfLimitCone ℬ W X Y).hom (𝟙 Z) ≫
      (BinaryFan.associatorOfLimitCone ℬ W (tensorObj ℬ X Y) Z).hom ≫
        tensorHom ℬ (𝟙 W) (BinaryFan.associatorOfLimitCone ℬ X Y Z).hom =
    (BinaryFan.associatorOfLimitCone ℬ (tensorObj ℬ W X) Y Z).hom ≫
      (BinaryFan.associatorOfLimitCone ℬ W X (tensorObj ℬ Y Z)).hom
[PROOFSTEP]
dsimp [tensorHom]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : C
𝒯 : LimitCone (Functor.empty C)
ℬ : (X Y : C) → LimitCone (pair X Y)
W X Y Z : C
⊢ IsLimit.lift (ℬ (ℬ W (ℬ X Y).cone.pt).cone.pt Z).isLimit
        (BinaryFan.mk
          (BinaryFan.fst (ℬ (ℬ (ℬ W X).cone.pt Y).cone.pt Z).cone ≫ (BinaryFan.associatorOfLimitCone ℬ W X Y).hom)
          (BinaryFan.snd (ℬ (ℬ (ℬ W X).cone.pt Y).cone.pt Z).cone ≫ 𝟙 Z)) ≫
      (BinaryFan.associatorOfLimitCone ℬ W (tensorObj ℬ X Y) Z).hom ≫
        IsLimit.lift (ℬ W (ℬ X (ℬ Y Z).cone.pt).cone.pt).isLimit
          (BinaryFan.mk (BinaryFan.fst (ℬ W (ℬ (tensorObj ℬ X Y) Z).cone.pt).cone ≫ 𝟙 W)
            (BinaryFan.snd (ℬ W (ℬ (tensorObj ℬ X Y) Z).cone.pt).cone ≫
              (BinaryFan.associatorOfLimitCone ℬ X Y Z).hom)) =
    (BinaryFan.associatorOfLimitCone ℬ (tensorObj ℬ W X) Y Z).hom ≫
      (BinaryFan.associatorOfLimitCone ℬ W X (tensorObj ℬ Y Z)).hom
[PROOFSTEP]
apply IsLimit.hom_ext (ℬ _ _).isLimit
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : C
𝒯 : LimitCone (Functor.empty C)
ℬ : (X Y : C) → LimitCone (pair X Y)
W X Y Z : C
⊢ ∀ (j : Discrete WalkingPair),
    (IsLimit.lift (ℬ (ℬ W (ℬ X Y).cone.pt).cone.pt Z).isLimit
            (BinaryFan.mk
              (BinaryFan.fst (ℬ (ℬ (ℬ W X).cone.pt Y).cone.pt Z).cone ≫ (BinaryFan.associatorOfLimitCone ℬ W X Y).hom)
              (BinaryFan.snd (ℬ (ℬ (ℬ W X).cone.pt Y).cone.pt Z).cone ≫ 𝟙 Z)) ≫
          (BinaryFan.associatorOfLimitCone ℬ W (tensorObj ℬ X Y) Z).hom ≫
            IsLimit.lift (ℬ W (ℬ X (ℬ Y Z).cone.pt).cone.pt).isLimit
              (BinaryFan.mk (BinaryFan.fst (ℬ W (ℬ (tensorObj ℬ X Y) Z).cone.pt).cone ≫ 𝟙 W)
                (BinaryFan.snd (ℬ W (ℬ (tensorObj ℬ X Y) Z).cone.pt).cone ≫
                  (BinaryFan.associatorOfLimitCone ℬ X Y Z).hom))) ≫
        NatTrans.app (ℬ W (ℬ X (ℬ Y Z).cone.pt).cone.pt).cone.π j =
      ((BinaryFan.associatorOfLimitCone ℬ (tensorObj ℬ W X) Y Z).hom ≫
          (BinaryFan.associatorOfLimitCone ℬ W X (tensorObj ℬ Y Z)).hom) ≫
        NatTrans.app (ℬ W (ℬ X (ℬ Y Z).cone.pt).cone.pt).cone.π j
[PROOFSTEP]
rintro ⟨⟨⟩⟩
[GOAL]
case mk.left
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : C
𝒯 : LimitCone (Functor.empty C)
ℬ : (X Y : C) → LimitCone (pair X Y)
W X Y Z : C
⊢ (IsLimit.lift (ℬ (ℬ W (ℬ X Y).cone.pt).cone.pt Z).isLimit
          (BinaryFan.mk
            (BinaryFan.fst (ℬ (ℬ (ℬ W X).cone.pt Y).cone.pt Z).cone ≫ (BinaryFan.associatorOfLimitCone ℬ W X Y).hom)
            (BinaryFan.snd (ℬ (ℬ (ℬ W X).cone.pt Y).cone.pt Z).cone ≫ 𝟙 Z)) ≫
        (BinaryFan.associatorOfLimitCone ℬ W (tensorObj ℬ X Y) Z).hom ≫
          IsLimit.lift (ℬ W (ℬ X (ℬ Y Z).cone.pt).cone.pt).isLimit
            (BinaryFan.mk (BinaryFan.fst (ℬ W (ℬ (tensorObj ℬ X Y) Z).cone.pt).cone ≫ 𝟙 W)
              (BinaryFan.snd (ℬ W (ℬ (tensorObj ℬ X Y) Z).cone.pt).cone ≫
                (BinaryFan.associatorOfLimitCone ℬ X Y Z).hom))) ≫
      NatTrans.app (ℬ W (ℬ X (ℬ Y Z).cone.pt).cone.pt).cone.π { as := WalkingPair.left } =
    ((BinaryFan.associatorOfLimitCone ℬ (tensorObj ℬ W X) Y Z).hom ≫
        (BinaryFan.associatorOfLimitCone ℬ W X (tensorObj ℬ Y Z)).hom) ≫
      NatTrans.app (ℬ W (ℬ X (ℬ Y Z).cone.pt).cone.pt).cone.π { as := WalkingPair.left }
[PROOFSTEP]
simp
[GOAL]
case mk.right
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : C
𝒯 : LimitCone (Functor.empty C)
ℬ : (X Y : C) → LimitCone (pair X Y)
W X Y Z : C
⊢ (IsLimit.lift (ℬ (ℬ W (ℬ X Y).cone.pt).cone.pt Z).isLimit
          (BinaryFan.mk
            (BinaryFan.fst (ℬ (ℬ (ℬ W X).cone.pt Y).cone.pt Z).cone ≫ (BinaryFan.associatorOfLimitCone ℬ W X Y).hom)
            (BinaryFan.snd (ℬ (ℬ (ℬ W X).cone.pt Y).cone.pt Z).cone ≫ 𝟙 Z)) ≫
        (BinaryFan.associatorOfLimitCone ℬ W (tensorObj ℬ X Y) Z).hom ≫
          IsLimit.lift (ℬ W (ℬ X (ℬ Y Z).cone.pt).cone.pt).isLimit
            (BinaryFan.mk (BinaryFan.fst (ℬ W (ℬ (tensorObj ℬ X Y) Z).cone.pt).cone ≫ 𝟙 W)
              (BinaryFan.snd (ℬ W (ℬ (tensorObj ℬ X Y) Z).cone.pt).cone ≫
                (BinaryFan.associatorOfLimitCone ℬ X Y Z).hom))) ≫
      NatTrans.app (ℬ W (ℬ X (ℬ Y Z).cone.pt).cone.pt).cone.π { as := WalkingPair.right } =
    ((BinaryFan.associatorOfLimitCone ℬ (tensorObj ℬ W X) Y Z).hom ≫
        (BinaryFan.associatorOfLimitCone ℬ W X (tensorObj ℬ Y Z)).hom) ≫
      NatTrans.app (ℬ W (ℬ X (ℬ Y Z).cone.pt).cone.pt).cone.π { as := WalkingPair.right }
[PROOFSTEP]
apply IsLimit.hom_ext (ℬ _ _).isLimit
[GOAL]
case mk.right
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : C
𝒯 : LimitCone (Functor.empty C)
ℬ : (X Y : C) → LimitCone (pair X Y)
W X Y Z : C
⊢ ∀ (j : Discrete WalkingPair),
    ((IsLimit.lift (ℬ (ℬ W (ℬ X Y).cone.pt).cone.pt Z).isLimit
              (BinaryFan.mk
                (BinaryFan.fst (ℬ (ℬ (ℬ W X).cone.pt Y).cone.pt Z).cone ≫ (BinaryFan.associatorOfLimitCone ℬ W X Y).hom)
                (BinaryFan.snd (ℬ (ℬ (ℬ W X).cone.pt Y).cone.pt Z).cone ≫ 𝟙 Z)) ≫
            (BinaryFan.associatorOfLimitCone ℬ W (tensorObj ℬ X Y) Z).hom ≫
              IsLimit.lift (ℬ W (ℬ X (ℬ Y Z).cone.pt).cone.pt).isLimit
                (BinaryFan.mk (BinaryFan.fst (ℬ W (ℬ (tensorObj ℬ X Y) Z).cone.pt).cone ≫ 𝟙 W)
                  (BinaryFan.snd (ℬ W (ℬ (tensorObj ℬ X Y) Z).cone.pt).cone ≫
                    (BinaryFan.associatorOfLimitCone ℬ X Y Z).hom))) ≫
          NatTrans.app (ℬ W (ℬ X (ℬ Y Z).cone.pt).cone.pt).cone.π { as := WalkingPair.right }) ≫
        NatTrans.app (ℬ X (ℬ Y Z).cone.pt).cone.π j =
      (((BinaryFan.associatorOfLimitCone ℬ (tensorObj ℬ W X) Y Z).hom ≫
            (BinaryFan.associatorOfLimitCone ℬ W X (tensorObj ℬ Y Z)).hom) ≫
          NatTrans.app (ℬ W (ℬ X (ℬ Y Z).cone.pt).cone.pt).cone.π { as := WalkingPair.right }) ≫
        NatTrans.app (ℬ X (ℬ Y Z).cone.pt).cone.π j
[PROOFSTEP]
rintro ⟨⟨⟩⟩
[GOAL]
case mk.right.mk.left
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : C
𝒯 : LimitCone (Functor.empty C)
ℬ : (X Y : C) → LimitCone (pair X Y)
W X Y Z : C
⊢ ((IsLimit.lift (ℬ (ℬ W (ℬ X Y).cone.pt).cone.pt Z).isLimit
            (BinaryFan.mk
              (BinaryFan.fst (ℬ (ℬ (ℬ W X).cone.pt Y).cone.pt Z).cone ≫ (BinaryFan.associatorOfLimitCone ℬ W X Y).hom)
              (BinaryFan.snd (ℬ (ℬ (ℬ W X).cone.pt Y).cone.pt Z).cone ≫ 𝟙 Z)) ≫
          (BinaryFan.associatorOfLimitCone ℬ W (tensorObj ℬ X Y) Z).hom ≫
            IsLimit.lift (ℬ W (ℬ X (ℬ Y Z).cone.pt).cone.pt).isLimit
              (BinaryFan.mk (BinaryFan.fst (ℬ W (ℬ (tensorObj ℬ X Y) Z).cone.pt).cone ≫ 𝟙 W)
                (BinaryFan.snd (ℬ W (ℬ (tensorObj ℬ X Y) Z).cone.pt).cone ≫
                  (BinaryFan.associatorOfLimitCone ℬ X Y Z).hom))) ≫
        NatTrans.app (ℬ W (ℬ X (ℬ Y Z).cone.pt).cone.pt).cone.π { as := WalkingPair.right }) ≫
      NatTrans.app (ℬ X (ℬ Y Z).cone.pt).cone.π { as := WalkingPair.left } =
    (((BinaryFan.associatorOfLimitCone ℬ (tensorObj ℬ W X) Y Z).hom ≫
          (BinaryFan.associatorOfLimitCone ℬ W X (tensorObj ℬ Y Z)).hom) ≫
        NatTrans.app (ℬ W (ℬ X (ℬ Y Z).cone.pt).cone.pt).cone.π { as := WalkingPair.right }) ≫
      NatTrans.app (ℬ X (ℬ Y Z).cone.pt).cone.π { as := WalkingPair.left }
[PROOFSTEP]
simp
[GOAL]
case mk.right.mk.right
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : C
𝒯 : LimitCone (Functor.empty C)
ℬ : (X Y : C) → LimitCone (pair X Y)
W X Y Z : C
⊢ ((IsLimit.lift (ℬ (ℬ W (ℬ X Y).cone.pt).cone.pt Z).isLimit
            (BinaryFan.mk
              (BinaryFan.fst (ℬ (ℬ (ℬ W X).cone.pt Y).cone.pt Z).cone ≫ (BinaryFan.associatorOfLimitCone ℬ W X Y).hom)
              (BinaryFan.snd (ℬ (ℬ (ℬ W X).cone.pt Y).cone.pt Z).cone ≫ 𝟙 Z)) ≫
          (BinaryFan.associatorOfLimitCone ℬ W (tensorObj ℬ X Y) Z).hom ≫
            IsLimit.lift (ℬ W (ℬ X (ℬ Y Z).cone.pt).cone.pt).isLimit
              (BinaryFan.mk (BinaryFan.fst (ℬ W (ℬ (tensorObj ℬ X Y) Z).cone.pt).cone ≫ 𝟙 W)
                (BinaryFan.snd (ℬ W (ℬ (tensorObj ℬ X Y) Z).cone.pt).cone ≫
                  (BinaryFan.associatorOfLimitCone ℬ X Y Z).hom))) ≫
        NatTrans.app (ℬ W (ℬ X (ℬ Y Z).cone.pt).cone.pt).cone.π { as := WalkingPair.right }) ≫
      NatTrans.app (ℬ X (ℬ Y Z).cone.pt).cone.π { as := WalkingPair.right } =
    (((BinaryFan.associatorOfLimitCone ℬ (tensorObj ℬ W X) Y Z).hom ≫
          (BinaryFan.associatorOfLimitCone ℬ W X (tensorObj ℬ Y Z)).hom) ≫
        NatTrans.app (ℬ W (ℬ X (ℬ Y Z).cone.pt).cone.pt).cone.π { as := WalkingPair.right }) ≫
      NatTrans.app (ℬ X (ℬ Y Z).cone.pt).cone.π { as := WalkingPair.right }
[PROOFSTEP]
apply IsLimit.hom_ext (ℬ _ _).isLimit
[GOAL]
case mk.right.mk.right
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : C
𝒯 : LimitCone (Functor.empty C)
ℬ : (X Y : C) → LimitCone (pair X Y)
W X Y Z : C
⊢ ∀ (j : Discrete WalkingPair),
    (((IsLimit.lift (ℬ (ℬ W (ℬ X Y).cone.pt).cone.pt Z).isLimit
                (BinaryFan.mk
                  (BinaryFan.fst (ℬ (ℬ (ℬ W X).cone.pt Y).cone.pt Z).cone ≫
                    (BinaryFan.associatorOfLimitCone ℬ W X Y).hom)
                  (BinaryFan.snd (ℬ (ℬ (ℬ W X).cone.pt Y).cone.pt Z).cone ≫ 𝟙 Z)) ≫
              (BinaryFan.associatorOfLimitCone ℬ W (tensorObj ℬ X Y) Z).hom ≫
                IsLimit.lift (ℬ W (ℬ X (ℬ Y Z).cone.pt).cone.pt).isLimit
                  (BinaryFan.mk (BinaryFan.fst (ℬ W (ℬ (tensorObj ℬ X Y) Z).cone.pt).cone ≫ 𝟙 W)
                    (BinaryFan.snd (ℬ W (ℬ (tensorObj ℬ X Y) Z).cone.pt).cone ≫
                      (BinaryFan.associatorOfLimitCone ℬ X Y Z).hom))) ≫
            NatTrans.app (ℬ W (ℬ X (ℬ Y Z).cone.pt).cone.pt).cone.π { as := WalkingPair.right }) ≫
          NatTrans.app (ℬ X (ℬ Y Z).cone.pt).cone.π { as := WalkingPair.right }) ≫
        NatTrans.app (ℬ Y Z).cone.π j =
      ((((BinaryFan.associatorOfLimitCone ℬ (tensorObj ℬ W X) Y Z).hom ≫
              (BinaryFan.associatorOfLimitCone ℬ W X (tensorObj ℬ Y Z)).hom) ≫
            NatTrans.app (ℬ W (ℬ X (ℬ Y Z).cone.pt).cone.pt).cone.π { as := WalkingPair.right }) ≫
          NatTrans.app (ℬ X (ℬ Y Z).cone.pt).cone.π { as := WalkingPair.right }) ≫
        NatTrans.app (ℬ Y Z).cone.π j
[PROOFSTEP]
rintro ⟨⟨⟩⟩
[GOAL]
case mk.right.mk.right.mk.left
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : C
𝒯 : LimitCone (Functor.empty C)
ℬ : (X Y : C) → LimitCone (pair X Y)
W X Y Z : C
⊢ (((IsLimit.lift (ℬ (ℬ W (ℬ X Y).cone.pt).cone.pt Z).isLimit
              (BinaryFan.mk
                (BinaryFan.fst (ℬ (ℬ (ℬ W X).cone.pt Y).cone.pt Z).cone ≫ (BinaryFan.associatorOfLimitCone ℬ W X Y).hom)
                (BinaryFan.snd (ℬ (ℬ (ℬ W X).cone.pt Y).cone.pt Z).cone ≫ 𝟙 Z)) ≫
            (BinaryFan.associatorOfLimitCone ℬ W (tensorObj ℬ X Y) Z).hom ≫
              IsLimit.lift (ℬ W (ℬ X (ℬ Y Z).cone.pt).cone.pt).isLimit
                (BinaryFan.mk (BinaryFan.fst (ℬ W (ℬ (tensorObj ℬ X Y) Z).cone.pt).cone ≫ 𝟙 W)
                  (BinaryFan.snd (ℬ W (ℬ (tensorObj ℬ X Y) Z).cone.pt).cone ≫
                    (BinaryFan.associatorOfLimitCone ℬ X Y Z).hom))) ≫
          NatTrans.app (ℬ W (ℬ X (ℬ Y Z).cone.pt).cone.pt).cone.π { as := WalkingPair.right }) ≫
        NatTrans.app (ℬ X (ℬ Y Z).cone.pt).cone.π { as := WalkingPair.right }) ≫
      NatTrans.app (ℬ Y Z).cone.π { as := WalkingPair.left } =
    ((((BinaryFan.associatorOfLimitCone ℬ (tensorObj ℬ W X) Y Z).hom ≫
            (BinaryFan.associatorOfLimitCone ℬ W X (tensorObj ℬ Y Z)).hom) ≫
          NatTrans.app (ℬ W (ℬ X (ℬ Y Z).cone.pt).cone.pt).cone.π { as := WalkingPair.right }) ≫
        NatTrans.app (ℬ X (ℬ Y Z).cone.pt).cone.π { as := WalkingPair.right }) ≫
      NatTrans.app (ℬ Y Z).cone.π { as := WalkingPair.left }
[PROOFSTEP]
simp
[GOAL]
case mk.right.mk.right.mk.right
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : C
𝒯 : LimitCone (Functor.empty C)
ℬ : (X Y : C) → LimitCone (pair X Y)
W X Y Z : C
⊢ (((IsLimit.lift (ℬ (ℬ W (ℬ X Y).cone.pt).cone.pt Z).isLimit
              (BinaryFan.mk
                (BinaryFan.fst (ℬ (ℬ (ℬ W X).cone.pt Y).cone.pt Z).cone ≫ (BinaryFan.associatorOfLimitCone ℬ W X Y).hom)
                (BinaryFan.snd (ℬ (ℬ (ℬ W X).cone.pt Y).cone.pt Z).cone ≫ 𝟙 Z)) ≫
            (BinaryFan.associatorOfLimitCone ℬ W (tensorObj ℬ X Y) Z).hom ≫
              IsLimit.lift (ℬ W (ℬ X (ℬ Y Z).cone.pt).cone.pt).isLimit
                (BinaryFan.mk (BinaryFan.fst (ℬ W (ℬ (tensorObj ℬ X Y) Z).cone.pt).cone ≫ 𝟙 W)
                  (BinaryFan.snd (ℬ W (ℬ (tensorObj ℬ X Y) Z).cone.pt).cone ≫
                    (BinaryFan.associatorOfLimitCone ℬ X Y Z).hom))) ≫
          NatTrans.app (ℬ W (ℬ X (ℬ Y Z).cone.pt).cone.pt).cone.π { as := WalkingPair.right }) ≫
        NatTrans.app (ℬ X (ℬ Y Z).cone.pt).cone.π { as := WalkingPair.right }) ≫
      NatTrans.app (ℬ Y Z).cone.π { as := WalkingPair.right } =
    ((((BinaryFan.associatorOfLimitCone ℬ (tensorObj ℬ W X) Y Z).hom ≫
            (BinaryFan.associatorOfLimitCone ℬ W X (tensorObj ℬ Y Z)).hom) ≫
          NatTrans.app (ℬ W (ℬ X (ℬ Y Z).cone.pt).cone.pt).cone.π { as := WalkingPair.right }) ≫
        NatTrans.app (ℬ X (ℬ Y Z).cone.pt).cone.π { as := WalkingPair.right }) ≫
      NatTrans.app (ℬ Y Z).cone.π { as := WalkingPair.right }
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : C
𝒯 : LimitCone (Functor.empty C)
ℬ : (X Y : C) → LimitCone (pair X Y)
X Y : C
⊢ (BinaryFan.associatorOfLimitCone ℬ X 𝒯.cone.pt Y).hom ≫
      tensorHom ℬ (𝟙 X) (BinaryFan.leftUnitor 𝒯.isLimit (ℬ 𝒯.cone.pt Y).isLimit).hom =
    tensorHom ℬ (BinaryFan.rightUnitor 𝒯.isLimit (ℬ X 𝒯.cone.pt).isLimit).hom (𝟙 Y)
[PROOFSTEP]
dsimp [tensorHom]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : C
𝒯 : LimitCone (Functor.empty C)
ℬ : (X Y : C) → LimitCone (pair X Y)
X Y : C
⊢ (BinaryFan.associatorOfLimitCone ℬ X 𝒯.cone.pt Y).hom ≫
      IsLimit.lift (ℬ X Y).isLimit
        (BinaryFan.mk (BinaryFan.fst (ℬ X (ℬ 𝒯.cone.pt Y).cone.pt).cone ≫ 𝟙 X)
          (BinaryFan.snd (ℬ X (ℬ 𝒯.cone.pt Y).cone.pt).cone ≫ BinaryFan.snd (ℬ 𝒯.cone.pt Y).cone)) =
    IsLimit.lift (ℬ X Y).isLimit
      (BinaryFan.mk (BinaryFan.fst (ℬ (ℬ X 𝒯.cone.pt).cone.pt Y).cone ≫ BinaryFan.fst (ℬ X 𝒯.cone.pt).cone)
        (BinaryFan.snd (ℬ (ℬ X 𝒯.cone.pt).cone.pt Y).cone ≫ 𝟙 Y))
[PROOFSTEP]
apply IsLimit.hom_ext (ℬ _ _).isLimit
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : C
𝒯 : LimitCone (Functor.empty C)
ℬ : (X Y : C) → LimitCone (pair X Y)
X Y : C
⊢ ∀ (j : Discrete WalkingPair),
    ((BinaryFan.associatorOfLimitCone ℬ X 𝒯.cone.pt Y).hom ≫
          IsLimit.lift (ℬ X Y).isLimit
            (BinaryFan.mk (BinaryFan.fst (ℬ X (ℬ 𝒯.cone.pt Y).cone.pt).cone ≫ 𝟙 X)
              (BinaryFan.snd (ℬ X (ℬ 𝒯.cone.pt Y).cone.pt).cone ≫ BinaryFan.snd (ℬ 𝒯.cone.pt Y).cone))) ≫
        NatTrans.app (ℬ X Y).cone.π j =
      IsLimit.lift (ℬ X Y).isLimit
          (BinaryFan.mk (BinaryFan.fst (ℬ (ℬ X 𝒯.cone.pt).cone.pt Y).cone ≫ BinaryFan.fst (ℬ X 𝒯.cone.pt).cone)
            (BinaryFan.snd (ℬ (ℬ X 𝒯.cone.pt).cone.pt Y).cone ≫ 𝟙 Y)) ≫
        NatTrans.app (ℬ X Y).cone.π j
[PROOFSTEP]
rintro ⟨⟨⟩⟩
[GOAL]
case mk.left
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : C
𝒯 : LimitCone (Functor.empty C)
ℬ : (X Y : C) → LimitCone (pair X Y)
X Y : C
⊢ ((BinaryFan.associatorOfLimitCone ℬ X 𝒯.cone.pt Y).hom ≫
        IsLimit.lift (ℬ X Y).isLimit
          (BinaryFan.mk (BinaryFan.fst (ℬ X (ℬ 𝒯.cone.pt Y).cone.pt).cone ≫ 𝟙 X)
            (BinaryFan.snd (ℬ X (ℬ 𝒯.cone.pt Y).cone.pt).cone ≫ BinaryFan.snd (ℬ 𝒯.cone.pt Y).cone))) ≫
      NatTrans.app (ℬ X Y).cone.π { as := WalkingPair.left } =
    IsLimit.lift (ℬ X Y).isLimit
        (BinaryFan.mk (BinaryFan.fst (ℬ (ℬ X 𝒯.cone.pt).cone.pt Y).cone ≫ BinaryFan.fst (ℬ X 𝒯.cone.pt).cone)
          (BinaryFan.snd (ℬ (ℬ X 𝒯.cone.pt).cone.pt Y).cone ≫ 𝟙 Y)) ≫
      NatTrans.app (ℬ X Y).cone.π { as := WalkingPair.left }
[PROOFSTEP]
simp
[GOAL]
case mk.right
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : C
𝒯 : LimitCone (Functor.empty C)
ℬ : (X Y : C) → LimitCone (pair X Y)
X Y : C
⊢ ((BinaryFan.associatorOfLimitCone ℬ X 𝒯.cone.pt Y).hom ≫
        IsLimit.lift (ℬ X Y).isLimit
          (BinaryFan.mk (BinaryFan.fst (ℬ X (ℬ 𝒯.cone.pt Y).cone.pt).cone ≫ 𝟙 X)
            (BinaryFan.snd (ℬ X (ℬ 𝒯.cone.pt Y).cone.pt).cone ≫ BinaryFan.snd (ℬ 𝒯.cone.pt Y).cone))) ≫
      NatTrans.app (ℬ X Y).cone.π { as := WalkingPair.right } =
    IsLimit.lift (ℬ X Y).isLimit
        (BinaryFan.mk (BinaryFan.fst (ℬ (ℬ X 𝒯.cone.pt).cone.pt Y).cone ≫ BinaryFan.fst (ℬ X 𝒯.cone.pt).cone)
          (BinaryFan.snd (ℬ (ℬ X 𝒯.cone.pt).cone.pt Y).cone ≫ 𝟙 Y)) ≫
      NatTrans.app (ℬ X Y).cone.π { as := WalkingPair.right }
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y : C
𝒯 : LimitCone (Functor.empty C)
ℬ : (X Y : C) → LimitCone (pair X Y)
X₁ X₂ : C
f : X₁ ⟶ X₂
⊢ tensorHom ℬ (𝟙 𝒯.cone.pt) f ≫ (BinaryFan.leftUnitor 𝒯.isLimit (ℬ 𝒯.cone.pt X₂).isLimit).hom =
    (BinaryFan.leftUnitor 𝒯.isLimit (ℬ 𝒯.cone.pt X₁).isLimit).hom ≫ f
[PROOFSTEP]
dsimp [tensorHom]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y : C
𝒯 : LimitCone (Functor.empty C)
ℬ : (X Y : C) → LimitCone (pair X Y)
X₁ X₂ : C
f : X₁ ⟶ X₂
⊢ IsLimit.lift (ℬ 𝒯.cone.pt X₂).isLimit
        (BinaryFan.mk (BinaryFan.fst (ℬ 𝒯.cone.pt X₁).cone ≫ 𝟙 𝒯.cone.pt) (BinaryFan.snd (ℬ 𝒯.cone.pt X₁).cone ≫ f)) ≫
      BinaryFan.snd (ℬ 𝒯.cone.pt X₂).cone =
    BinaryFan.snd (ℬ 𝒯.cone.pt X₁).cone ≫ f
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y : C
𝒯 : LimitCone (Functor.empty C)
ℬ : (X Y : C) → LimitCone (pair X Y)
X₁ X₂ : C
f : X₁ ⟶ X₂
⊢ tensorHom ℬ f (𝟙 𝒯.cone.pt) ≫ (BinaryFan.rightUnitor 𝒯.isLimit (ℬ X₂ 𝒯.cone.pt).isLimit).hom =
    (BinaryFan.rightUnitor 𝒯.isLimit (ℬ X₁ 𝒯.cone.pt).isLimit).hom ≫ f
[PROOFSTEP]
dsimp [tensorHom]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y : C
𝒯 : LimitCone (Functor.empty C)
ℬ : (X Y : C) → LimitCone (pair X Y)
X₁ X₂ : C
f : X₁ ⟶ X₂
⊢ IsLimit.lift (ℬ X₂ 𝒯.cone.pt).isLimit
        (BinaryFan.mk (BinaryFan.fst (ℬ X₁ 𝒯.cone.pt).cone ≫ f) (BinaryFan.snd (ℬ X₁ 𝒯.cone.pt).cone ≫ 𝟙 𝒯.cone.pt)) ≫
      BinaryFan.fst (ℬ X₂ 𝒯.cone.pt).cone =
    BinaryFan.fst (ℬ X₁ 𝒯.cone.pt).cone ≫ f
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y : C
𝒯 : LimitCone (Functor.empty C)
ℬ : (X Y : C) → LimitCone (pair X Y)
X₁ X₂ X₃ Y₁ Y₂ Y₃ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
f₃ : X₃ ⟶ Y₃
⊢ tensorHom ℬ (tensorHom ℬ f₁ f₂) f₃ ≫ (BinaryFan.associatorOfLimitCone ℬ Y₁ Y₂ Y₃).hom =
    (BinaryFan.associatorOfLimitCone ℬ X₁ X₂ X₃).hom ≫ tensorHom ℬ f₁ (tensorHom ℬ f₂ f₃)
[PROOFSTEP]
dsimp [tensorHom]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y : C
𝒯 : LimitCone (Functor.empty C)
ℬ : (X Y : C) → LimitCone (pair X Y)
X₁ X₂ X₃ Y₁ Y₂ Y₃ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
f₃ : X₃ ⟶ Y₃
⊢ IsLimit.lift (ℬ (tensorObj ℬ Y₁ Y₂) Y₃).isLimit
        (BinaryFan.mk
          (BinaryFan.fst (ℬ (tensorObj ℬ X₁ X₂) X₃).cone ≫
            IsLimit.lift (ℬ Y₁ Y₂).isLimit
              (BinaryFan.mk (BinaryFan.fst (ℬ X₁ X₂).cone ≫ f₁) (BinaryFan.snd (ℬ X₁ X₂).cone ≫ f₂)))
          (BinaryFan.snd (ℬ (tensorObj ℬ X₁ X₂) X₃).cone ≫ f₃)) ≫
      (BinaryFan.associatorOfLimitCone ℬ Y₁ Y₂ Y₃).hom =
    (BinaryFan.associatorOfLimitCone ℬ X₁ X₂ X₃).hom ≫
      IsLimit.lift (ℬ Y₁ (tensorObj ℬ Y₂ Y₃)).isLimit
        (BinaryFan.mk (BinaryFan.fst (ℬ X₁ (ℬ X₂ X₃).cone.pt).cone ≫ f₁)
          (BinaryFan.snd (ℬ X₁ (ℬ X₂ X₃).cone.pt).cone ≫
            IsLimit.lift (ℬ Y₂ Y₃).isLimit
              (BinaryFan.mk (BinaryFan.fst (ℬ X₂ X₃).cone ≫ f₂) (BinaryFan.snd (ℬ X₂ X₃).cone ≫ f₃))))
[PROOFSTEP]
apply IsLimit.hom_ext (ℬ _ _).isLimit
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y : C
𝒯 : LimitCone (Functor.empty C)
ℬ : (X Y : C) → LimitCone (pair X Y)
X₁ X₂ X₃ Y₁ Y₂ Y₃ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
f₃ : X₃ ⟶ Y₃
⊢ ∀ (j : Discrete WalkingPair),
    (IsLimit.lift (ℬ (tensorObj ℬ Y₁ Y₂) Y₃).isLimit
            (BinaryFan.mk
              (BinaryFan.fst (ℬ (tensorObj ℬ X₁ X₂) X₃).cone ≫
                IsLimit.lift (ℬ Y₁ Y₂).isLimit
                  (BinaryFan.mk (BinaryFan.fst (ℬ X₁ X₂).cone ≫ f₁) (BinaryFan.snd (ℬ X₁ X₂).cone ≫ f₂)))
              (BinaryFan.snd (ℬ (tensorObj ℬ X₁ X₂) X₃).cone ≫ f₃)) ≫
          (BinaryFan.associatorOfLimitCone ℬ Y₁ Y₂ Y₃).hom) ≫
        NatTrans.app (ℬ Y₁ (ℬ Y₂ Y₃).cone.pt).cone.π j =
      ((BinaryFan.associatorOfLimitCone ℬ X₁ X₂ X₃).hom ≫
          IsLimit.lift (ℬ Y₁ (tensorObj ℬ Y₂ Y₃)).isLimit
            (BinaryFan.mk (BinaryFan.fst (ℬ X₁ (ℬ X₂ X₃).cone.pt).cone ≫ f₁)
              (BinaryFan.snd (ℬ X₁ (ℬ X₂ X₃).cone.pt).cone ≫
                IsLimit.lift (ℬ Y₂ Y₃).isLimit
                  (BinaryFan.mk (BinaryFan.fst (ℬ X₂ X₃).cone ≫ f₂) (BinaryFan.snd (ℬ X₂ X₃).cone ≫ f₃))))) ≫
        NatTrans.app (ℬ Y₁ (ℬ Y₂ Y₃).cone.pt).cone.π j
[PROOFSTEP]
rintro ⟨⟨⟩⟩
[GOAL]
case mk.left
C : Type u
inst✝ : Category.{v, u} C
X Y : C
𝒯 : LimitCone (Functor.empty C)
ℬ : (X Y : C) → LimitCone (pair X Y)
X₁ X₂ X₃ Y₁ Y₂ Y₃ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
f₃ : X₃ ⟶ Y₃
⊢ (IsLimit.lift (ℬ (tensorObj ℬ Y₁ Y₂) Y₃).isLimit
          (BinaryFan.mk
            (BinaryFan.fst (ℬ (tensorObj ℬ X₁ X₂) X₃).cone ≫
              IsLimit.lift (ℬ Y₁ Y₂).isLimit
                (BinaryFan.mk (BinaryFan.fst (ℬ X₁ X₂).cone ≫ f₁) (BinaryFan.snd (ℬ X₁ X₂).cone ≫ f₂)))
            (BinaryFan.snd (ℬ (tensorObj ℬ X₁ X₂) X₃).cone ≫ f₃)) ≫
        (BinaryFan.associatorOfLimitCone ℬ Y₁ Y₂ Y₃).hom) ≫
      NatTrans.app (ℬ Y₁ (ℬ Y₂ Y₃).cone.pt).cone.π { as := WalkingPair.left } =
    ((BinaryFan.associatorOfLimitCone ℬ X₁ X₂ X₃).hom ≫
        IsLimit.lift (ℬ Y₁ (tensorObj ℬ Y₂ Y₃)).isLimit
          (BinaryFan.mk (BinaryFan.fst (ℬ X₁ (ℬ X₂ X₃).cone.pt).cone ≫ f₁)
            (BinaryFan.snd (ℬ X₁ (ℬ X₂ X₃).cone.pt).cone ≫
              IsLimit.lift (ℬ Y₂ Y₃).isLimit
                (BinaryFan.mk (BinaryFan.fst (ℬ X₂ X₃).cone ≫ f₂) (BinaryFan.snd (ℬ X₂ X₃).cone ≫ f₃))))) ≫
      NatTrans.app (ℬ Y₁ (ℬ Y₂ Y₃).cone.pt).cone.π { as := WalkingPair.left }
[PROOFSTEP]
simp
[GOAL]
case mk.right
C : Type u
inst✝ : Category.{v, u} C
X Y : C
𝒯 : LimitCone (Functor.empty C)
ℬ : (X Y : C) → LimitCone (pair X Y)
X₁ X₂ X₃ Y₁ Y₂ Y₃ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
f₃ : X₃ ⟶ Y₃
⊢ (IsLimit.lift (ℬ (tensorObj ℬ Y₁ Y₂) Y₃).isLimit
          (BinaryFan.mk
            (BinaryFan.fst (ℬ (tensorObj ℬ X₁ X₂) X₃).cone ≫
              IsLimit.lift (ℬ Y₁ Y₂).isLimit
                (BinaryFan.mk (BinaryFan.fst (ℬ X₁ X₂).cone ≫ f₁) (BinaryFan.snd (ℬ X₁ X₂).cone ≫ f₂)))
            (BinaryFan.snd (ℬ (tensorObj ℬ X₁ X₂) X₃).cone ≫ f₃)) ≫
        (BinaryFan.associatorOfLimitCone ℬ Y₁ Y₂ Y₃).hom) ≫
      NatTrans.app (ℬ Y₁ (ℬ Y₂ Y₃).cone.pt).cone.π { as := WalkingPair.right } =
    ((BinaryFan.associatorOfLimitCone ℬ X₁ X₂ X₃).hom ≫
        IsLimit.lift (ℬ Y₁ (tensorObj ℬ Y₂ Y₃)).isLimit
          (BinaryFan.mk (BinaryFan.fst (ℬ X₁ (ℬ X₂ X₃).cone.pt).cone ≫ f₁)
            (BinaryFan.snd (ℬ X₁ (ℬ X₂ X₃).cone.pt).cone ≫
              IsLimit.lift (ℬ Y₂ Y₃).isLimit
                (BinaryFan.mk (BinaryFan.fst (ℬ X₂ X₃).cone ≫ f₂) (BinaryFan.snd (ℬ X₂ X₃).cone ≫ f₃))))) ≫
      NatTrans.app (ℬ Y₁ (ℬ Y₂ Y₃).cone.pt).cone.π { as := WalkingPair.right }
[PROOFSTEP]
apply IsLimit.hom_ext (ℬ _ _).isLimit
[GOAL]
case mk.right
C : Type u
inst✝ : Category.{v, u} C
X Y : C
𝒯 : LimitCone (Functor.empty C)
ℬ : (X Y : C) → LimitCone (pair X Y)
X₁ X₂ X₃ Y₁ Y₂ Y₃ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
f₃ : X₃ ⟶ Y₃
⊢ ∀ (j : Discrete WalkingPair),
    ((IsLimit.lift (ℬ (tensorObj ℬ Y₁ Y₂) Y₃).isLimit
              (BinaryFan.mk
                (BinaryFan.fst (ℬ (tensorObj ℬ X₁ X₂) X₃).cone ≫
                  IsLimit.lift (ℬ Y₁ Y₂).isLimit
                    (BinaryFan.mk (BinaryFan.fst (ℬ X₁ X₂).cone ≫ f₁) (BinaryFan.snd (ℬ X₁ X₂).cone ≫ f₂)))
                (BinaryFan.snd (ℬ (tensorObj ℬ X₁ X₂) X₃).cone ≫ f₃)) ≫
            (BinaryFan.associatorOfLimitCone ℬ Y₁ Y₂ Y₃).hom) ≫
          NatTrans.app (ℬ Y₁ (ℬ Y₂ Y₃).cone.pt).cone.π { as := WalkingPair.right }) ≫
        NatTrans.app (ℬ Y₂ Y₃).cone.π j =
      (((BinaryFan.associatorOfLimitCone ℬ X₁ X₂ X₃).hom ≫
            IsLimit.lift (ℬ Y₁ (tensorObj ℬ Y₂ Y₃)).isLimit
              (BinaryFan.mk (BinaryFan.fst (ℬ X₁ (ℬ X₂ X₃).cone.pt).cone ≫ f₁)
                (BinaryFan.snd (ℬ X₁ (ℬ X₂ X₃).cone.pt).cone ≫
                  IsLimit.lift (ℬ Y₂ Y₃).isLimit
                    (BinaryFan.mk (BinaryFan.fst (ℬ X₂ X₃).cone ≫ f₂) (BinaryFan.snd (ℬ X₂ X₃).cone ≫ f₃))))) ≫
          NatTrans.app (ℬ Y₁ (ℬ Y₂ Y₃).cone.pt).cone.π { as := WalkingPair.right }) ≫
        NatTrans.app (ℬ Y₂ Y₃).cone.π j
[PROOFSTEP]
rintro ⟨⟨⟩⟩
[GOAL]
case mk.right.mk.left
C : Type u
inst✝ : Category.{v, u} C
X Y : C
𝒯 : LimitCone (Functor.empty C)
ℬ : (X Y : C) → LimitCone (pair X Y)
X₁ X₂ X₃ Y₁ Y₂ Y₃ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
f₃ : X₃ ⟶ Y₃
⊢ ((IsLimit.lift (ℬ (tensorObj ℬ Y₁ Y₂) Y₃).isLimit
            (BinaryFan.mk
              (BinaryFan.fst (ℬ (tensorObj ℬ X₁ X₂) X₃).cone ≫
                IsLimit.lift (ℬ Y₁ Y₂).isLimit
                  (BinaryFan.mk (BinaryFan.fst (ℬ X₁ X₂).cone ≫ f₁) (BinaryFan.snd (ℬ X₁ X₂).cone ≫ f₂)))
              (BinaryFan.snd (ℬ (tensorObj ℬ X₁ X₂) X₃).cone ≫ f₃)) ≫
          (BinaryFan.associatorOfLimitCone ℬ Y₁ Y₂ Y₃).hom) ≫
        NatTrans.app (ℬ Y₁ (ℬ Y₂ Y₃).cone.pt).cone.π { as := WalkingPair.right }) ≫
      NatTrans.app (ℬ Y₂ Y₃).cone.π { as := WalkingPair.left } =
    (((BinaryFan.associatorOfLimitCone ℬ X₁ X₂ X₃).hom ≫
          IsLimit.lift (ℬ Y₁ (tensorObj ℬ Y₂ Y₃)).isLimit
            (BinaryFan.mk (BinaryFan.fst (ℬ X₁ (ℬ X₂ X₃).cone.pt).cone ≫ f₁)
              (BinaryFan.snd (ℬ X₁ (ℬ X₂ X₃).cone.pt).cone ≫
                IsLimit.lift (ℬ Y₂ Y₃).isLimit
                  (BinaryFan.mk (BinaryFan.fst (ℬ X₂ X₃).cone ≫ f₂) (BinaryFan.snd (ℬ X₂ X₃).cone ≫ f₃))))) ≫
        NatTrans.app (ℬ Y₁ (ℬ Y₂ Y₃).cone.pt).cone.π { as := WalkingPair.right }) ≫
      NatTrans.app (ℬ Y₂ Y₃).cone.π { as := WalkingPair.left }
[PROOFSTEP]
simp
[GOAL]
case mk.right.mk.right
C : Type u
inst✝ : Category.{v, u} C
X Y : C
𝒯 : LimitCone (Functor.empty C)
ℬ : (X Y : C) → LimitCone (pair X Y)
X₁ X₂ X₃ Y₁ Y₂ Y₃ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
f₃ : X₃ ⟶ Y₃
⊢ ((IsLimit.lift (ℬ (tensorObj ℬ Y₁ Y₂) Y₃).isLimit
            (BinaryFan.mk
              (BinaryFan.fst (ℬ (tensorObj ℬ X₁ X₂) X₃).cone ≫
                IsLimit.lift (ℬ Y₁ Y₂).isLimit
                  (BinaryFan.mk (BinaryFan.fst (ℬ X₁ X₂).cone ≫ f₁) (BinaryFan.snd (ℬ X₁ X₂).cone ≫ f₂)))
              (BinaryFan.snd (ℬ (tensorObj ℬ X₁ X₂) X₃).cone ≫ f₃)) ≫
          (BinaryFan.associatorOfLimitCone ℬ Y₁ Y₂ Y₃).hom) ≫
        NatTrans.app (ℬ Y₁ (ℬ Y₂ Y₃).cone.pt).cone.π { as := WalkingPair.right }) ≫
      NatTrans.app (ℬ Y₂ Y₃).cone.π { as := WalkingPair.right } =
    (((BinaryFan.associatorOfLimitCone ℬ X₁ X₂ X₃).hom ≫
          IsLimit.lift (ℬ Y₁ (tensorObj ℬ Y₂ Y₃)).isLimit
            (BinaryFan.mk (BinaryFan.fst (ℬ X₁ (ℬ X₂ X₃).cone.pt).cone ≫ f₁)
              (BinaryFan.snd (ℬ X₁ (ℬ X₂ X₃).cone.pt).cone ≫
                IsLimit.lift (ℬ Y₂ Y₃).isLimit
                  (BinaryFan.mk (BinaryFan.fst (ℬ X₂ X₃).cone ≫ f₂) (BinaryFan.snd (ℬ X₂ X₃).cone ≫ f₃))))) ≫
        NatTrans.app (ℬ Y₁ (ℬ Y₂ Y₃).cone.pt).cone.π { as := WalkingPair.right }) ≫
      NatTrans.app (ℬ Y₂ Y₃).cone.π { as := WalkingPair.right }
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y : C
𝒯 : LimitCone (Functor.empty C)
ℬ : (X Y : C) → LimitCone (pair X Y)
⊢ Category.{?u.82278, u} (MonoidalOfChosenFiniteProductsSynonym 𝒯 ℬ)
[PROOFSTEP]
dsimp [MonoidalOfChosenFiniteProductsSynonym]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y : C
𝒯 : LimitCone (Functor.empty C)
ℬ : (X Y : C) → LimitCone (pair X Y)
⊢ Category.{?u.82278, u} C
[PROOFSTEP]
infer_instance
