mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Final

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : D ⥤ Cat
G : C ⥤ D
d : D
f : ↑(F.obj d)
X : StructuredArrow d G
⊢ (F.map X.hom).toFunctor.obj { base := d, fiber := f }.fiber ⟶
    ((pre F G).obj { base := X.right, fiber := (F.map X.hom).toFunctor.obj f }).fiber

Tactic:
dsimp

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : D ⥤ Cat
G : C ⥤ D
d : D
f : ↑(F.obj d)
X : StructuredArrow d G
⊢ (F.map X.hom).toFunctor.obj f ⟶ (F.map X.hom).toFunctor.obj f
Module: Mathlib.CategoryTheory.Limits.Final

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : D ⥤ Cat
G : C ⥤ D
hG : G.Final
d : D
f : ↑(F.obj d)
u : Discrete PUnit.{1}
c : C
g : (fromPUnit d).obj u ⟶ G.obj c
this : Nonempty (StructuredArrow { base := d, fiber := f } (pre F G)) :=
  Nonempty.intro
    { left := u, right := { base := c, fiber := (F.map g).toFunctor.obj f },
      hom := { base := g, fiber := 𝟙 ((F.map g).toFunctor.obj ((fromPUnit { base := d, fiber := f }).obj u).fiber) } }
bi : C
fi : ↑(F.obj (G.obj bi))
gbi : d ⟶ G.obj bi
gfi : (F.map gbi).toFunctor.obj f ⟶ fi
bj : C
fj : ↑(F.obj (G.obj bj))
gbj : d ⟶ G.obj bj
gfj : (F.map gbj).toFunctor.obj f ⟶ fj
⊢ (StructuredArrow.mk
          { base := gbi, fiber := 𝟙 ((F.map gbi).toFunctor.obj { base := d, fiber := f }.fiber) }).right.base ⟶
    (StructuredArrow.right
        { left := { as := PUnit.unit }, right := { base := bi, fiber := fi },
          hom := { base := gbi, fiber := gfi } }).base

Tactic:
dsimp

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : D ⥤ Cat
G : C ⥤ D
hG : G.Final
d : D
f : ↑(F.obj d)
u : Discrete PUnit.{1}
c : C
g : (fromPUnit d).obj u ⟶ G.obj c
this : Nonempty (StructuredArrow { base := d, fiber := f } (pre F G)) :=
  Nonempty.intro
    { left := u, right := { base := c, fiber := (F.map g).toFunctor.obj f },
      hom := { base := g, fiber := 𝟙 ((F.map g).toFunctor.obj ((fromPUnit { base := d, fiber := f }).obj u).fiber) } }
bi : C
fi : ↑(F.obj (G.obj bi))
gbi : d ⟶ G.obj bi
gfi : (F.map gbi).toFunctor.obj f ⟶ fi
bj : C
fj : ↑(F.obj (G.obj bj))
gbj : d ⟶ G.obj bj
gfj : (F.map gbj).toFunctor.obj f ⟶ fj
⊢ bi ⟶ bi
Module: Mathlib.CategoryTheory.Limits.Final

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : D ⥤ Cat
G : C ⥤ D
hG : G.Final
d : D
f : ↑(F.obj d)
u : Discrete PUnit.{1}
c : C
g : (fromPUnit d).obj u ⟶ G.obj c
this : Nonempty (StructuredArrow { base := d, fiber := f } (pre F G)) :=
  Nonempty.intro
    { left := u, right := { base := c, fiber := (F.map g).toFunctor.obj f },
      hom := { base := g, fiber := 𝟙 ((F.map g).toFunctor.obj ((fromPUnit { base := d, fiber := f }).obj u).fiber) } }
bi : C
fi : ↑(F.obj (G.obj bi))
gbi : d ⟶ G.obj bi
gfi : (F.map gbi).toFunctor.obj f ⟶ fi
bj : C
fj : ↑(F.obj (G.obj bj))
gbj : d ⟶ G.obj bj
gfj : (F.map gbj).toFunctor.obj f ⟶ fj
⊢ (StructuredArrow.mk
          { base := gbj, fiber := 𝟙 ((F.map gbj).toFunctor.obj { base := d, fiber := f }.fiber) }).right.base ⟶
    (StructuredArrow.right
        { left := { as := PUnit.unit }, right := { base := bj, fiber := fj },
          hom := { base := gbj, fiber := gfj } }).base

Tactic:
dsimp

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : D ⥤ Cat
G : C ⥤ D
hG : G.Final
d : D
f : ↑(F.obj d)
u : Discrete PUnit.{1}
c : C
g : (fromPUnit d).obj u ⟶ G.obj c
this : Nonempty (StructuredArrow { base := d, fiber := f } (pre F G)) :=
  Nonempty.intro
    { left := u, right := { base := c, fiber := (F.map g).toFunctor.obj f },
      hom := { base := g, fiber := 𝟙 ((F.map g).toFunctor.obj ((fromPUnit { base := d, fiber := f }).obj u).fiber) } }
bi : C
fi : ↑(F.obj (G.obj bi))
gbi : d ⟶ G.obj bi
gfi : (F.map gbi).toFunctor.obj f ⟶ fi
bj : C
fj : ↑(F.obj (G.obj bj))
gbj : d ⟶ G.obj bj
gfj : (F.map gbj).toFunctor.obj f ⟶ fj
⊢ bj ⟶ bj
Module: Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
J : Type u'
inst✝¹ : Category.{v', u'} J
inst✝ : Nonempty J
⊢ ⊥.strictLimitsOfShape J = ⊥

Tactic:
by
  rw [eq_bot_iff]
  rintro _ ⟨_, h⟩
  exact h (Classical.arbitrary J)

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
P : ObjectProperty C
J : Type u'
inst✝¹ : Category.{v', u'} J
J' : Type u''
inst✝ : Category.{v'', u''} J'
X : C
p : P.LimitOfShape J X
X✝ Y✝ : J
f : X✝ ⟶ Y✝
⊢ (StructuredArrow.mk (p.π.app X✝)).right.obj ⟶ (StructuredArrow.mk (p.π.app Y✝)).right.obj

Tactic:
by exact p.diag.map f

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
W : MorphismProperty C
J : Type u_2
inst✝¹ : Preorder J
inst✝ : OrderBot J
F : J ⥤ C
c : Cocone F
hc : IsColimit c
h : ∀ (j : J), W (F.map (homOfLE ⋯))
x✝² x✝¹ : J
x✝ : x✝² ⟶ x✝¹
⊢ ((Functor.const J).obj (F.obj ⊥)).map x✝ ≫ F.map (homOfLE ⋯) = F.map (homOfLE ⋯) ≫ F.map x✝

Tactic:
dsimp

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
W : MorphismProperty C
J : Type u_2
inst✝¹ : Preorder J
inst✝ : OrderBot J
F : J ⥤ C
c : Cocone F
hc : IsColimit c
h : ∀ (j : J), W (F.map (homOfLE ⋯))
x✝² x✝¹ : J
x✝ : x✝² ⟶ x✝¹
⊢ 𝟙 (F.obj ⊥) ≫ F.map (homOfLE ⋯) = F.map (homOfLE ⋯) ≫ F.map x✝
Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
J : Type u'
inst✝¹ : Category.{v', u'} J
inst✝ : Nonempty J
⊢ ⊥.strictColimitsOfShape J = ⊥

Tactic:
by
  rw [eq_bot_iff]
  rintro _ ⟨_, h⟩
  exact h (Classical.arbitrary J)

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
P : ObjectProperty C
J : Type u'
inst✝¹ : Category.{v', u'} J
J' : Type u''
inst✝ : Category.{v'', u''} J'
X : C
p : P.ColimitOfShape J X
X✝ Y✝ : J
f : X✝ ⟶ Y✝
⊢ (CostructuredArrow.mk (p.ι.app X✝)).left.obj ⟶ (CostructuredArrow.mk (p.ι.app Y✝)).left.obj

Tactic:
by exact p.diag.map f

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
ℬ : (X Y : C) → LimitCone (pair X Y)
W X Y Z : C
⊢ ↑(BinaryFan.IsLimit.lift' (ℬ (ℬ W (ℬ X Y).cone.pt).cone.pt Z).isLimit
          ((ℬ (ℬ (ℬ W X).cone.pt Y).cone.pt Z).cone.π.app { as := WalkingPair.left } ≫
            (BinaryFan.associatorOfLimitCone ℬ W X Y).hom)
          ((ℬ (ℬ (ℬ W X).cone.pt Y).cone.pt Z).cone.π.app { as := WalkingPair.right } ≫ 𝟙 Z)) ≫
      (BinaryFan.associatorOfLimitCone ℬ W (tensorObj ℬ X Y) Z).hom ≫
        ↑(BinaryFan.IsLimit.lift' (ℬ W (ℬ X (ℬ Y Z).cone.pt).cone.pt).isLimit
            ((ℬ W (ℬ (tensorObj ℬ X Y) Z).cone.pt).cone.π.app { as := WalkingPair.left } ≫ 𝟙 W)
            ((ℬ W (ℬ (tensorObj ℬ X Y) Z).cone.pt).cone.π.app { as := WalkingPair.right } ≫
              (BinaryFan.associatorOfLimitCone ℬ X Y Z).hom)) =
    (BinaryFan.associatorOfLimitCone ℬ (tensorObj ℬ W X) Y Z).hom ≫
      (BinaryFan.associatorOfLimitCone ℬ W X (tensorObj ℬ Y Z)).hom

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

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
ℬ : (X Y : C) → LimitCone (pair X Y)
W X Y Z : C
⊢ ∀ (j : Discrete WalkingPair),
    (↑(BinaryFan.IsLimit.lift' (ℬ (ℬ W (ℬ X Y).cone.pt).cone.pt Z).isLimit
              ((ℬ (ℬ (ℬ W X).cone.pt Y).cone.pt Z).cone.π.app { as := WalkingPair.left } ≫
                (BinaryFan.associatorOfLimitCone ℬ W X Y).hom)
              ((ℬ (ℬ (ℬ W X).cone.pt Y).cone.pt Z).cone.π.app { as := WalkingPair.right } ≫ 𝟙 Z)) ≫
          (BinaryFan.associatorOfLimitCone ℬ W (tensorObj ℬ X Y) Z).hom ≫
            ↑(BinaryFan.IsLimit.lift' (ℬ W (ℬ X (ℬ Y Z).cone.pt).cone.pt).isLimit
                ((ℬ W (ℬ (tensorObj ℬ X Y) Z).cone.pt).cone.π.app { as := WalkingPair.left } ≫ 𝟙 W)
                ((ℬ W (ℬ (tensorObj ℬ X Y) Z).cone.pt).cone.π.app { as := WalkingPair.right } ≫
                  (BinaryFan.associatorOfLimitCone ℬ X Y Z).hom))) ≫
        (ℬ W (ℬ X (ℬ Y Z).cone.pt).cone.pt).cone.π.app j =
      ((BinaryFan.associatorOfLimitCone ℬ (tensorObj ℬ W X) Y Z).hom ≫
          (BinaryFan.associatorOfLimitCone ℬ W X (tensorObj ℬ Y Z)).hom) ≫
        (ℬ W (ℬ X (ℬ Y Z).cone.pt).cone.pt).cone.π.app j
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic

Goal state before:
pp: case right
C : Type u
inst✝ : Category.{v, u} C
ℬ : (X Y : C) → LimitCone (pair X Y)
W X Y Z : C
⊢ (↑(BinaryFan.IsLimit.lift' (ℬ (ℬ W (ℬ X Y).cone.pt).cone.pt Z).isLimit
            ((ℬ (ℬ (ℬ W X).cone.pt Y).cone.pt Z).cone.π.app { as := WalkingPair.left } ≫
              (BinaryFan.associatorOfLimitCone ℬ W X Y).hom)
            ((ℬ (ℬ (ℬ W X).cone.pt Y).cone.pt Z).cone.π.app { as := WalkingPair.right } ≫ 𝟙 Z)) ≫
        (BinaryFan.associatorOfLimitCone ℬ W (tensorObj ℬ X Y) Z).hom ≫
          ↑(BinaryFan.IsLimit.lift' (ℬ W (ℬ X (ℬ Y Z).cone.pt).cone.pt).isLimit
              ((ℬ W (ℬ (tensorObj ℬ X Y) Z).cone.pt).cone.π.app { as := WalkingPair.left } ≫ 𝟙 W)
              ((ℬ W (ℬ (tensorObj ℬ X Y) Z).cone.pt).cone.π.app { as := WalkingPair.right } ≫
                (BinaryFan.associatorOfLimitCone ℬ X Y Z).hom))) ≫
      (ℬ W (ℬ X (ℬ Y Z).cone.pt).cone.pt).cone.π.app { as := WalkingPair.right } =
    ((BinaryFan.associatorOfLimitCone ℬ (tensorObj ℬ W X) Y Z).hom ≫
        (BinaryFan.associatorOfLimitCone ℬ W X (tensorObj ℬ Y Z)).hom) ≫
      (ℬ W (ℬ X (ℬ Y Z).cone.pt).cone.pt).cone.π.app { as := WalkingPair.right }

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

Goal state after:
case right
C : Type u
inst✝ : Category.{v, u} C
ℬ : (X Y : C) → LimitCone (pair X Y)
W X Y Z : C
⊢ ∀ (j : Discrete WalkingPair),
    ((↑(BinaryFan.IsLimit.lift' (ℬ (ℬ W (ℬ X Y).cone.pt).cone.pt Z).isLimit
                ((ℬ (ℬ (ℬ W X).cone.pt Y).cone.pt Z).cone.π.app { as := WalkingPair.left } ≫
                  (BinaryFan.associatorOfLimitCone ℬ W X Y).hom)
                ((ℬ (ℬ (ℬ W X).cone.pt Y).cone.pt Z).cone.π.app { as := WalkingPair.right } ≫ 𝟙 Z)) ≫
            (BinaryFan.associatorOfLimitCone ℬ W (tensorObj ℬ X Y) Z).hom ≫
              ↑(BinaryFan.IsLimit.lift' (ℬ W (ℬ X (ℬ Y Z).cone.pt).cone.pt).isLimit
                  ((ℬ W (ℬ (tensorObj ℬ X Y) Z).cone.pt).cone.π.app { as := WalkingPair.left } ≫ 𝟙 W)
                  ((ℬ W (ℬ (tensorObj ℬ X Y) Z).cone.pt).cone.π.app { as := WalkingPair.right } ≫
                    (BinaryFan.associatorOfLimitCone ℬ X Y Z).hom))) ≫
          (ℬ W (ℬ X (ℬ Y Z).cone.pt).cone.pt).cone.π.app { as := WalkingPair.right }) ≫
        (ℬ X (ℬ Y Z).cone.pt).cone.π.app j =
      (((BinaryFan.associatorOfLimitCone ℬ (tensorObj ℬ W X) Y Z).hom ≫
            (BinaryFan.associatorOfLimitCone ℬ W X (tensorObj ℬ Y Z)).hom) ≫
          (ℬ W (ℬ X (ℬ Y Z).cone.pt).cone.pt).cone.π.app { as := WalkingPair.right }) ≫
        (ℬ X (ℬ Y Z).cone.pt).cone.π.app j
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic

Goal state before:
pp: case right.right
C : Type u
inst✝ : Category.{v, u} C
ℬ : (X Y : C) → LimitCone (pair X Y)
W X Y Z : C
⊢ ((↑(BinaryFan.IsLimit.lift' (ℬ (ℬ W (ℬ X Y).cone.pt).cone.pt Z).isLimit
              ((ℬ (ℬ (ℬ W X).cone.pt Y).cone.pt Z).cone.π.app { as := WalkingPair.left } ≫
                (BinaryFan.associatorOfLimitCone ℬ W X Y).hom)
              ((ℬ (ℬ (ℬ W X).cone.pt Y).cone.pt Z).cone.π.app { as := WalkingPair.right } ≫ 𝟙 Z)) ≫
          (BinaryFan.associatorOfLimitCone ℬ W (tensorObj ℬ X Y) Z).hom ≫
            ↑(BinaryFan.IsLimit.lift' (ℬ W (ℬ X (ℬ Y Z).cone.pt).cone.pt).isLimit
                ((ℬ W (ℬ (tensorObj ℬ X Y) Z).cone.pt).cone.π.app { as := WalkingPair.left } ≫ 𝟙 W)
                ((ℬ W (ℬ (tensorObj ℬ X Y) Z).cone.pt).cone.π.app { as := WalkingPair.right } ≫
                  (BinaryFan.associatorOfLimitCone ℬ X Y Z).hom))) ≫
        (ℬ W (ℬ X (ℬ Y Z).cone.pt).cone.pt).cone.π.app { as := WalkingPair.right }) ≫
      (ℬ X (ℬ Y Z).cone.pt).cone.π.app { as := WalkingPair.right } =
    (((BinaryFan.associatorOfLimitCone ℬ (tensorObj ℬ W X) Y Z).hom ≫
          (BinaryFan.associatorOfLimitCone ℬ W X (tensorObj ℬ Y Z)).hom) ≫
        (ℬ W (ℬ X (ℬ Y Z).cone.pt).cone.pt).cone.π.app { as := WalkingPair.right }) ≫
      (ℬ X (ℬ Y Z).cone.pt).cone.π.app { as := WalkingPair.right }

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

Goal state after:
case right.right
C : Type u
inst✝ : Category.{v, u} C
ℬ : (X Y : C) → LimitCone (pair X Y)
W X Y Z : C
⊢ ∀ (j : Discrete WalkingPair),
    (((↑(BinaryFan.IsLimit.lift' (ℬ (ℬ W (ℬ X Y).cone.pt).cone.pt Z).isLimit
                  ((ℬ (ℬ (ℬ W X).cone.pt Y).cone.pt Z).cone.π.app { as := WalkingPair.left } ≫
                    (BinaryFan.associatorOfLimitCone ℬ W X Y).hom)
                  ((ℬ (ℬ (ℬ W X).cone.pt Y).cone.pt Z).cone.π.app { as := WalkingPair.right } ≫ 𝟙 Z)) ≫
              (BinaryFan.associatorOfLimitCone ℬ W (tensorObj ℬ X Y) Z).hom ≫
                ↑(BinaryFan.IsLimit.lift' (ℬ W (ℬ X (ℬ Y Z).cone.pt).cone.pt).isLimit
                    ((ℬ W (ℬ (tensorObj ℬ X Y) Z).cone.pt).cone.π.app { as := WalkingPair.left } ≫ 𝟙 W)
                    ((ℬ W (ℬ (tensorObj ℬ X Y) Z).cone.pt).cone.π.app { as := WalkingPair.right } ≫
                      (BinaryFan.associatorOfLimitCone ℬ X Y Z).hom))) ≫
            (ℬ W (ℬ X (ℬ Y Z).cone.pt).cone.pt).cone.π.app { as := WalkingPair.right }) ≫
          (ℬ X (ℬ Y Z).cone.pt).cone.π.app { as := WalkingPair.right }) ≫
        (ℬ Y Z).cone.π.app j =
      ((((BinaryFan.associatorOfLimitCone ℬ (tensorObj ℬ W X) Y Z).hom ≫
              (BinaryFan.associatorOfLimitCone ℬ W X (tensorObj ℬ Y Z)).hom) ≫
            (ℬ W (ℬ X (ℬ Y Z).cone.pt).cone.pt).cone.π.app { as := WalkingPair.right }) ≫
          (ℬ X (ℬ Y Z).cone.pt).cone.π.app { as := WalkingPair.right }) ≫
        (ℬ Y Z).cone.π.app j
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
ℬ : (X Y : C) → LimitCone (pair X Y)
X₁ X₂ X₃ Y₁ Y₂ Y₃ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
f₃ : X₃ ⟶ Y₃
⊢ ↑(BinaryFan.IsLimit.lift' (ℬ (tensorObj ℬ Y₁ Y₂) Y₃).isLimit
          ((ℬ (tensorObj ℬ X₁ X₂) X₃).cone.π.app { as := WalkingPair.left } ≫
            ↑(BinaryFan.IsLimit.lift' (ℬ Y₁ Y₂).isLimit ((ℬ X₁ X₂).cone.π.app { as := WalkingPair.left } ≫ f₁)
                ((ℬ X₁ X₂).cone.π.app { as := WalkingPair.right } ≫ f₂)))
          ((ℬ (tensorObj ℬ X₁ X₂) X₃).cone.π.app { as := WalkingPair.right } ≫ f₃)) ≫
      (BinaryFan.associatorOfLimitCone ℬ Y₁ Y₂ Y₃).hom =
    (BinaryFan.associatorOfLimitCone ℬ X₁ X₂ X₃).hom ≫
      ↑(BinaryFan.IsLimit.lift' (ℬ Y₁ (tensorObj ℬ Y₂ Y₃)).isLimit
          ((ℬ X₁ (ℬ X₂ X₃).cone.pt).cone.π.app { as := WalkingPair.left } ≫ f₁)
          ((ℬ X₁ (ℬ X₂ X₃).cone.pt).cone.π.app { as := WalkingPair.right } ≫
            ↑(BinaryFan.IsLimit.lift' (ℬ Y₂ Y₃).isLimit ((ℬ X₂ X₃).cone.π.app { as := WalkingPair.left } ≫ f₂)
                ((ℬ X₂ X₃).cone.π.app { as := WalkingPair.right } ≫ f₃))))

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

Goal state after:
C : Type u
inst✝ : Category.{v, u} 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),
    (↑(BinaryFan.IsLimit.lift' (ℬ (tensorObj ℬ Y₁ Y₂) Y₃).isLimit
              ((ℬ (tensorObj ℬ X₁ X₂) X₃).cone.π.app { as := WalkingPair.left } ≫
                ↑(BinaryFan.IsLimit.lift' (ℬ Y₁ Y₂).isLimit ((ℬ X₁ X₂).cone.π.app { as := WalkingPair.left } ≫ f₁)
                    ((ℬ X₁ X₂).cone.π.app { as := WalkingPair.right } ≫ f₂)))
              ((ℬ (tensorObj ℬ X₁ X₂) X₃).cone.π.app { as := WalkingPair.right } ≫ f₃)) ≫
          (BinaryFan.associatorOfLimitCone ℬ Y₁ Y₂ Y₃).hom) ≫
        (ℬ Y₁ (ℬ Y₂ Y₃).cone.pt).cone.π.app j =
      ((BinaryFan.associatorOfLimitCone ℬ X₁ X₂ X₃).hom ≫
          ↑(BinaryFan.IsLimit.lift' (ℬ Y₁ (tensorObj ℬ Y₂ Y₃)).isLimit
              ((ℬ X₁ (ℬ X₂ X₃).cone.pt).cone.π.app { as := WalkingPair.left } ≫ f₁)
              ((ℬ X₁ (ℬ X₂ X₃).cone.pt).cone.π.app { as := WalkingPair.right } ≫
                ↑(BinaryFan.IsLimit.lift' (ℬ Y₂ Y₃).isLimit ((ℬ X₂ X₃).cone.π.app { as := WalkingPair.left } ≫ f₂)
                    ((ℬ X₂ X₃).cone.π.app { as := WalkingPair.right } ≫ f₃))))) ≫
        (ℬ Y₁ (ℬ Y₂ Y₃).cone.pt).cone.π.app j
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic

Goal state before:
pp: case right
C : Type u
inst✝ : Category.{v, u} C
ℬ : (X Y : C) → LimitCone (pair X Y)
X₁ X₂ X₃ Y₁ Y₂ Y₃ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
f₃ : X₃ ⟶ Y₃
⊢ (↑(BinaryFan.IsLimit.lift' (ℬ (tensorObj ℬ Y₁ Y₂) Y₃).isLimit
            ((ℬ (tensorObj ℬ X₁ X₂) X₃).cone.π.app { as := WalkingPair.left } ≫
              ↑(BinaryFan.IsLimit.lift' (ℬ Y₁ Y₂).isLimit ((ℬ X₁ X₂).cone.π.app { as := WalkingPair.left } ≫ f₁)
                  ((ℬ X₁ X₂).cone.π.app { as := WalkingPair.right } ≫ f₂)))
            ((ℬ (tensorObj ℬ X₁ X₂) X₃).cone.π.app { as := WalkingPair.right } ≫ f₃)) ≫
        (BinaryFan.associatorOfLimitCone ℬ Y₁ Y₂ Y₃).hom) ≫
      (ℬ Y₁ (ℬ Y₂ Y₃).cone.pt).cone.π.app { as := WalkingPair.right } =
    ((BinaryFan.associatorOfLimitCone ℬ X₁ X₂ X₃).hom ≫
        ↑(BinaryFan.IsLimit.lift' (ℬ Y₁ (tensorObj ℬ Y₂ Y₃)).isLimit
            ((ℬ X₁ (ℬ X₂ X₃).cone.pt).cone.π.app { as := WalkingPair.left } ≫ f₁)
            ((ℬ X₁ (ℬ X₂ X₃).cone.pt).cone.π.app { as := WalkingPair.right } ≫
              ↑(BinaryFan.IsLimit.lift' (ℬ Y₂ Y₃).isLimit ((ℬ X₂ X₃).cone.π.app { as := WalkingPair.left } ≫ f₂)
                  ((ℬ X₂ X₃).cone.π.app { as := WalkingPair.right } ≫ f₃))))) ≫
      (ℬ Y₁ (ℬ Y₂ Y₃).cone.pt).cone.π.app { as := WalkingPair.right }

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

Goal state after:
case right
C : Type u
inst✝ : Category.{v, u} 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),
    ((↑(BinaryFan.IsLimit.lift' (ℬ (tensorObj ℬ Y₁ Y₂) Y₃).isLimit
                ((ℬ (tensorObj ℬ X₁ X₂) X₃).cone.π.app { as := WalkingPair.left } ≫
                  ↑(BinaryFan.IsLimit.lift' (ℬ Y₁ Y₂).isLimit ((ℬ X₁ X₂).cone.π.app { as := WalkingPair.left } ≫ f₁)
                      ((ℬ X₁ X₂).cone.π.app { as := WalkingPair.right } ≫ f₂)))
                ((ℬ (tensorObj ℬ X₁ X₂) X₃).cone.π.app { as := WalkingPair.right } ≫ f₃)) ≫
            (BinaryFan.associatorOfLimitCone ℬ Y₁ Y₂ Y₃).hom) ≫
          (ℬ Y₁ (ℬ Y₂ Y₃).cone.pt).cone.π.app { as := WalkingPair.right }) ≫
        (ℬ Y₂ Y₃).cone.π.app j =
      (((BinaryFan.associatorOfLimitCone ℬ X₁ X₂ X₃).hom ≫
            ↑(BinaryFan.IsLimit.lift' (ℬ Y₁ (tensorObj ℬ Y₂ Y₃)).isLimit
                ((ℬ X₁ (ℬ X₂ X₃).cone.pt).cone.π.app { as := WalkingPair.left } ≫ f₁)
                ((ℬ X₁ (ℬ X₂ X₃).cone.pt).cone.π.app { as := WalkingPair.right } ≫
                  ↑(BinaryFan.IsLimit.lift' (ℬ Y₂ Y₃).isLimit ((ℬ X₂ X₃).cone.π.app { as := WalkingPair.left } ≫ f₂)
                      ((ℬ X₂ X₃).cone.π.app { as := WalkingPair.right } ≫ f₃))))) ≫
          (ℬ Y₁ (ℬ Y₂ Y₃).cone.pt).cone.π.app { as := WalkingPair.right }) ≫
        (ℬ Y₂ Y₃).cone.π.app j
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Mon

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v, u_1} C
inst✝¹ : CartesianMonoidalCategory C
A B : C
inst✝ : MonObj B
f : A ⟶ 𝟙_ C
g : A ⟶ B
this : lift (f ≫ η) g ≫ μ = lift f g ≫ (λ_ B).hom
⊢ lift (f ≫ η) g ≫ μ = g

Tactic:
lift_leftUnitor_hom

Goal state after:
C : Type u_1
inst✝² : Category.{v, u_1} C
inst✝¹ : CartesianMonoidalCategory C
A B : C
inst✝ : MonObj B
f : A ⟶ 𝟙_ C
g : A ⟶ B
this : lift (f ≫ η) g ≫ μ = g
⊢ lift (f ≫ η) g ≫ μ = g
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic

Goal state before:
pp: C✝ : Type u
inst✝⁹ : Category.{v, u} C✝
C : Type u
inst✝⁸ : Category.{v, u} C
inst✝⁷ : CartesianMonoidalCategory C
D : Type u₁
inst✝⁶ : Category.{v₁, u₁} D
inst✝⁵ : CartesianMonoidalCategory D
F : C ⥤ D
E✝ : Type u₂
inst✝⁴ : Category.{v₂, u₂} E✝
inst✝³ : CartesianMonoidalCategory E✝
G✝ : D ⥤ E✝
A B A' B' : C
E : Type u₂
inst✝² : Category.{v₂, u₂} E
inst✝¹ : CartesianMonoidalCategory E
G : D ⥤ E
inst✝ : ∀ (A B : C), IsIso (prodComparison F A B)
x✝ : C
⊢ IsIso ((prodComparisonBifunctorNatTrans F).app x✝)

Tactic:
dsimp

Goal state after:
C✝ : Type u
inst✝⁹ : Category.{v, u} C✝
C : Type u
inst✝⁸ : Category.{v, u} C
inst✝⁷ : CartesianMonoidalCategory C
D : Type u₁
inst✝⁶ : Category.{v₁, u₁} D
inst✝⁵ : CartesianMonoidalCategory D
F : C ⥤ D
E✝ : Type u₂
inst✝⁴ : Category.{v₂, u₂} E✝
inst✝³ : CartesianMonoidalCategory E✝
G✝ : D ⥤ E✝
A B A' B' : C
E : Type u₂
inst✝² : Category.{v₂, u₂} E
inst✝¹ : CartesianMonoidalCategory E
G : D ⥤ E
inst✝ : ∀ (A B : C), IsIso (prodComparison F A B)
x✝ : C
⊢ IsIso (prodComparisonNatTrans F x✝)
Module: Mathlib.Algebra.Category.CommAlgCat.Monoidal

Goal state before:
pp: R : Type u
inst✝ : CommRing R
A B C D X✝ Y✝ Z✝ : CommAlgCat R
f✝ : Y✝ ⟶ Z✝
⊢ Hom.hom (X✝ ◁ f✝ ≫ (isoMk (Algebra.TensorProduct.comm R ↑X✝ ↑Z✝)).hom) =
    Hom.hom ((isoMk (Algebra.TensorProduct.comm R ↑X✝ ↑Y✝)).hom ≫ f✝ ▷ X✝)

Tactic:
dsimp

Goal state after:
R : Type u
inst✝ : CommRing R
A B C D X✝ Y✝ Z✝ : CommAlgCat R
f✝ : Y✝ ⟶ Z✝
⊢ (Hom.hom (isoMk (Algebra.TensorProduct.comm R ↑X✝ ↑Z✝)).hom).comp
      (Algebra.TensorProduct.map (AlgHom.id R ↑X✝) (Hom.hom f✝)) =
    (Algebra.TensorProduct.map (Hom.hom f✝) (AlgHom.id R ↑X✝)).comp
      (Hom.hom (isoMk (Algebra.TensorProduct.comm R ↑X✝ ↑Y✝)).hom)
Module: Mathlib.Algebra.Category.CommAlgCat.Monoidal

Goal state before:
pp: R : Type u
inst✝ : CommRing R
A B C D X✝ Y✝ : CommAlgCat R
f✝ : X✝ ⟶ Y✝
Z✝ : CommAlgCat R
⊢ Hom.hom (f✝ ▷ Z✝ ≫ (isoMk (Algebra.TensorProduct.comm R ↑Y✝ ↑Z✝)).hom) =
    Hom.hom ((isoMk (Algebra.TensorProduct.comm R ↑X✝ ↑Z✝)).hom ≫ Z✝ ◁ f✝)

Tactic:
dsimp

Goal state after:
R : Type u
inst✝ : CommRing R
A B C D X✝ Y✝ : CommAlgCat R
f✝ : X✝ ⟶ Y✝
Z✝ : CommAlgCat R
⊢ (Hom.hom (isoMk (Algebra.TensorProduct.comm R ↑Y✝ ↑Z✝)).hom).comp
      (Algebra.TensorProduct.map (Hom.hom f✝) (AlgHom.id R ↑Z✝)) =
    (Algebra.TensorProduct.map (AlgHom.id R ↑Z✝) (Hom.hom f✝)).comp
      (Hom.hom (isoMk (Algebra.TensorProduct.comm R ↑X✝ ↑Z✝)).hom)
Module: Mathlib.Algebra.Category.CommAlgCat.Monoidal

Goal state before:
pp: R : Type u
inst✝ : CommRing R
A B C D S T U : CommAlgCat R
⊢ Hom.hom ((α_ S T U).hom ≫ (isoMk (Algebra.TensorProduct.comm R ↑S ↑(T ⊗ U))).hom ≫ (α_ T U S).hom) =
    Hom.hom
      ((isoMk (Algebra.TensorProduct.comm R ↑S ↑T)).hom ▷ U ≫
        (α_ T S U).hom ≫ T ◁ (isoMk (Algebra.TensorProduct.comm R ↑S ↑U)).hom)

Tactic:
dsimp

Goal state after:
R : Type u
inst✝ : CommRing R
A B C D S T U : CommAlgCat R
⊢ ((↑(assoc R R R ↑T ↑U ↑S)).comp (Hom.hom (isoMk (Algebra.TensorProduct.comm R (↑S) (↑T ⊗[R] ↑U))).hom)).comp
      ↑(assoc R R R ↑S ↑T ↑U) =
    ((Algebra.TensorProduct.map (AlgHom.id R ↑T) (Hom.hom (isoMk (Algebra.TensorProduct.comm R ↑S ↑U)).hom)).comp
          ↑(assoc R R R ↑T ↑S ↑U)).comp
      (Algebra.TensorProduct.map (Hom.hom (isoMk (Algebra.TensorProduct.comm R ↑S ↑T)).hom) (AlgHom.id R ↑U))
Module: Mathlib.Algebra.Category.CommAlgCat.Monoidal

Goal state before:
pp: R : Type u
inst✝ : CommRing R
A B C D S T U : CommAlgCat R
⊢ Hom.hom ((α_ S T U).inv ≫ (isoMk (Algebra.TensorProduct.comm R ↑(S ⊗ T) ↑U)).hom ≫ (α_ U S T).inv) =
    Hom.hom
      (S ◁ (isoMk (Algebra.TensorProduct.comm R ↑T ↑U)).hom ≫
        (α_ S U T).inv ≫ (isoMk (Algebra.TensorProduct.comm R ↑S ↑U)).hom ▷ T)

Tactic:
dsimp

Goal state after:
R : Type u
inst✝ : CommRing R
A B C D S T U : CommAlgCat R
⊢ ((↑(assoc R R R ↑U ↑S ↑T).symm).comp (Hom.hom (isoMk (Algebra.TensorProduct.comm R (↑S ⊗[R] ↑T) ↑U)).hom)).comp
      ↑(assoc R R R ↑S ↑T ↑U).symm =
    ((Algebra.TensorProduct.map (Hom.hom (isoMk (Algebra.TensorProduct.comm R ↑S ↑U)).hom) (AlgHom.id R ↑T)).comp
          ↑(assoc R R R ↑S ↑U ↑T).symm).comp
      (Algebra.TensorProduct.map (AlgHom.id R ↑S) (Hom.hom (isoMk (Algebra.TensorProduct.comm R ↑T ↑U)).hom))