-- Mathlib/CategoryTheory/Monoidal/OfChosenFiniteProducts/Symmetric.lean
theorem braiding_naturality {X X' Y Y' : C} (f : X ⟶ Y) (g : X' ⟶ Y') :
    tensorHom ℬ f g ≫ (Limits.BinaryFan.braiding (ℬ Y Y').isLimit (ℬ Y' Y).isLimit).hom =
      (Limits.BinaryFan.braiding (ℬ X X').isLimit (ℬ X' X).isLimit).hom ≫ tensorHom ℬ g f

Proof state:
C : Type u
inst✝ : Category.{v, u} C
ℬ : (X Y : C) → LimitCone (pair X Y)
X X' Y Y' : C
f : X ⟶ Y
g : X' ⟶ Y'
⊢ tensorHom ℬ f g ≫ (BinaryFan.braiding (ℬ Y Y').isLimit (ℬ Y' Y).isLimit).hom =
    (BinaryFan.braiding (ℬ X X').isLimit (ℬ X' X).isLimit).hom ≫ tensorHom ℬ g f

Tactic:
dsimp [tensorHom, Limits.BinaryFan.braiding]

Result:
C : Type u
inst✝ : Category.{v, u} C
ℬ : (X Y : C) → LimitCone (pair X Y)
X X' Y Y' : C
f : X ⟶ Y
g : X' ⟶ Y'
⊢ (ℬ Y Y').isLimit.lift (BinaryFan.mk (BinaryFan.fst (ℬ X X').cone ≫ f) (BinaryFan.snd (ℬ X X').cone ≫ g)) ≫
      ((ℬ Y Y').isLimit.conePointUniqueUpToIso (ℬ Y' Y).isLimit.swapBinaryFan).hom =
    ((ℬ X X').isLimit.conePointUniqueUpToIso (ℬ X' X).isLimit.swapBinaryFan).hom ≫
      (ℬ Y' Y).isLimit.lift (BinaryFan.mk (BinaryFan.fst (ℬ X' X).cone ≫ g) (BinaryFan.snd (ℬ X' X).cone ≫ f))

Proof state:
C : Type u
inst✝ : Category.{v, u} C
ℬ : (X Y : C) → LimitCone (pair X Y)
X X' Y Y' : C
f : X ⟶ Y
g : X' ⟶ Y'
⊢ (ℬ Y Y').isLimit.lift (BinaryFan.mk (BinaryFan.fst (ℬ X X').cone ≫ f) (BinaryFan.snd (ℬ X X').cone ≫ g)) ≫
      ((ℬ Y Y').isLimit.conePointUniqueUpToIso (ℬ Y' Y).isLimit.swapBinaryFan).hom =
    ((ℬ X X').isLimit.conePointUniqueUpToIso (ℬ X' X).isLimit.swapBinaryFan).hom ≫
      (ℬ Y' Y).isLimit.lift (BinaryFan.mk (BinaryFan.fst (ℬ X' X).cone ≫ g) (BinaryFan.snd (ℬ X' X).cone ≫ f))

Tactic:
apply (ℬ _ _).isLimit.hom_ext

Result:
C : Type u
inst✝ : Category.{v, u} C
ℬ : (X Y : C) → LimitCone (pair X Y)
X X' Y Y' : C
f : X ⟶ Y
g : X' ⟶ Y'
⊢ ∀ (j : Discrete WalkingPair),
    ((ℬ Y Y').isLimit.lift (BinaryFan.mk (BinaryFan.fst (ℬ X X').cone ≫ f) (BinaryFan.snd (ℬ X X').cone ≫ g)) ≫
          ((ℬ Y Y').isLimit.conePointUniqueUpToIso (ℬ Y' Y).isLimit.swapBinaryFan).hom) ≫
        (ℬ Y' Y).cone.π.app j =
      (((ℬ X X').isLimit.conePointUniqueUpToIso (ℬ X' X).isLimit.swapBinaryFan).hom ≫
          (ℬ Y' Y).isLimit.lift (BinaryFan.mk (BinaryFan.fst (ℬ X' X).cone ≫ g) (BinaryFan.snd (ℬ X' X).cone ≫ f))) ≫
        (ℬ Y' Y).cone.π.app j

Proof state:
case mk.right
C : Type u
inst✝ : Category.{v, u} C
ℬ : (X Y : C) → LimitCone (pair X Y)
X X' Y Y' : C
f : X ⟶ Y
g : X' ⟶ Y'
⊢ ((ℬ Y Y').isLimit.lift (BinaryFan.mk (BinaryFan.fst (ℬ X X').cone ≫ f) (BinaryFan.snd (ℬ X X').cone ≫ g)) ≫
        (ℬ Y' Y).isLimit.lift (BinaryFan.swap (ℬ Y Y').cone)) ≫
      BinaryFan.snd (ℬ Y' Y).cone =
    ((ℬ X' X).isLimit.lift (BinaryFan.swap (ℬ X X').cone) ≫
        (ℬ Y' Y).isLimit.lift (BinaryFan.mk (BinaryFan.fst (ℬ X' X).cone ≫ g) (BinaryFan.snd (ℬ X' X).cone ≫ f))) ≫
      BinaryFan.snd (ℬ Y' Y).cone

Tactic:
simp

Result:
no goals

Proof state:
case mk.right
C : Type u
inst✝ : Category.{v, u} C
ℬ : (X Y : C) → LimitCone (pair X Y)
X X' Y Y' : C
f : X ⟶ Y
g : X' ⟶ Y'
⊢ ((ℬ Y Y').isLimit.lift (BinaryFan.mk (BinaryFan.fst (ℬ X X').cone ≫ f) (BinaryFan.snd (ℬ X X').cone ≫ g)) ≫
        ((ℬ Y Y').isLimit.conePointUniqueUpToIso (ℬ Y' Y).isLimit.swapBinaryFan).hom) ≫
      (ℬ Y' Y).cone.π.app { as := WalkingPair.right } =
    (((ℬ X X').isLimit.conePointUniqueUpToIso (ℬ X' X).isLimit.swapBinaryFan).hom ≫
        (ℬ Y' Y).isLimit.lift (BinaryFan.mk (BinaryFan.fst (ℬ X' X).cone ≫ g) (BinaryFan.snd (ℬ X' X).cone ≫ f))) ≫
      (ℬ Y' Y).cone.π.app { as := WalkingPair.right }

Tactic:
dsimp [Limits.IsLimit.conePointUniqueUpToIso]

Result:
case mk.right
C : Type u
inst✝ : Category.{v, u} C
ℬ : (X Y : C) → LimitCone (pair X Y)
X X' Y Y' : C
f : X ⟶ Y
g : X' ⟶ Y'
⊢ ((ℬ Y Y').isLimit.lift (BinaryFan.mk (BinaryFan.fst (ℬ X X').cone ≫ f) (BinaryFan.snd (ℬ X X').cone ≫ g)) ≫
        (ℬ Y' Y).isLimit.lift (BinaryFan.swap (ℬ Y Y').cone)) ≫
      BinaryFan.snd (ℬ Y' Y).cone =
    ((ℬ X' X).isLimit.lift (BinaryFan.swap (ℬ X X').cone) ≫
        (ℬ Y' Y).isLimit.lift (BinaryFan.mk (BinaryFan.fst (ℬ X' X).cone ≫ g) (BinaryFan.snd (ℬ X' X).cone ≫ f))) ≫
      BinaryFan.snd (ℬ Y' Y).cone