mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic

Goal state before:
pp: case h_fst
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : CartesianMonoidalCategory C
X Y : C
⊢ lift (fst X Y) (snd X Y) ≫ fst X Y = 𝟙 (X ⊗ Y) ≫ fst X Y

pp: case h_snd
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : CartesianMonoidalCategory C
X Y : C
⊢ lift (fst X Y) (snd X Y) ≫ snd X Y = 𝟙 (X ⊗ Y) ≫ snd X Y

Tactic:
<;>

Goal state after:
case h_fst
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : CartesianMonoidalCategory C
X Y : C
⊢ lift (fst X Y) (snd X Y) ≫ fst X Y = 𝟙 (X ⊗ Y) ≫ fst X Y

case h_snd
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : CartesianMonoidalCategory C
X Y : C
⊢ lift (fst X Y) (snd X Y) ≫ snd X Y = 𝟙 (X ⊗ Y) ≫ snd X Y
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic

Goal state before:
pp: case h_fst
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : CartesianMonoidalCategory C
V W X Y Z : C
f : V ⟶ W
g : V ⟶ X
h : W ⟶ Y
k : X ⟶ Z
⊢ (lift f g ≫ (h ⊗ₘ k)) ≫ fst Y Z = lift (f ≫ h) (g ≫ k) ≫ fst Y Z

pp: case h_snd
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : CartesianMonoidalCategory C
V W X Y Z : C
f : V ⟶ W
g : V ⟶ X
h : W ⟶ Y
k : X ⟶ Z
⊢ (lift f g ≫ (h ⊗ₘ k)) ≫ snd Y Z = lift (f ≫ h) (g ≫ k) ≫ snd Y Z

Tactic:
<;>

Goal state after:
case h_fst
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : CartesianMonoidalCategory C
V W X Y Z : C
f : V ⟶ W
g : V ⟶ X
h : W ⟶ Y
k : X ⟶ Z
⊢ (lift f g ≫ (h ⊗ₘ k)) ≫ fst Y Z = lift (f ≫ h) (g ≫ k) ≫ fst Y Z

case h_snd
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : CartesianMonoidalCategory C
V W X Y Z : C
f : V ⟶ W
g : V ⟶ X
h : W ⟶ Y
k : X ⟶ Z
⊢ (lift f g ≫ (h ⊗ₘ k)) ≫ snd Y Z = lift (f ≫ h) (g ≫ k) ≫ snd Y Z
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic

Goal state before:
pp: case h_fst
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : CartesianMonoidalCategory C
W X Y Z : C
g : W ⟶ X
g' : Y ⟶ Z
⊢ lift (fst W Y ≫ g) (snd W Y ≫ g') ≫ fst X Z = (g ⊗ₘ g') ≫ fst X Z

pp: case h_snd
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : CartesianMonoidalCategory C
W X Y Z : C
g : W ⟶ X
g' : Y ⟶ Z
⊢ lift (fst W Y ≫ g) (snd W Y ≫ g') ≫ snd X Z = (g ⊗ₘ g') ≫ snd X Z

Tactic:
<;>

Goal state after:
case h_fst
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : CartesianMonoidalCategory C
W X Y Z : C
g : W ⟶ X
g' : Y ⟶ Z
⊢ lift (fst W Y ≫ g) (snd W Y ≫ g') ≫ fst X Z = (g ⊗ₘ g') ≫ fst X Z

case h_snd
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : CartesianMonoidalCategory C
W X Y Z : C
g : W ⟶ X
g' : Y ⟶ Z
⊢ lift (fst W Y ≫ g) (snd W Y ≫ g') ≫ snd X Z = (g ⊗ₘ g') ≫ snd X Z
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Mon

Goal state before:
pp: case e_a.e_a.h_fst
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v, u_1} C
inst✝⁵ : CartesianMonoidalCategory C
inst✝⁴ : Category.{w, u_2} D
inst✝³ : CartesianMonoidalCategory D
M N O X Y : C
inst✝² : MonObj M
inst✝¹ : MonObj N
inst✝ : MonObj O
f₁ f₂ f₃ : X ⟶ M
⊢ (lift (lift f₁ f₂) f₃ ≫ (α_ M M M).hom) ≫ fst M (M ⊗ M) = lift f₁ (lift f₂ f₃) ≫ fst M (M ⊗ M)

pp: case h_snd.h_fst
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v, u_1} C
inst✝⁵ : CartesianMonoidalCategory C
inst✝⁴ : Category.{w, u_2} D
inst✝³ : CartesianMonoidalCategory D
M N O X Y : C
inst✝² : MonObj M
inst✝¹ : MonObj N
inst✝ : MonObj O
f₁ f₂ f₃ : X ⟶ M
⊢ ((lift (lift f₁ f₂) f₃ ≫ (α_ M M M).hom) ≫ snd M (M ⊗ M)) ≫ fst M M = (lift f₁ (lift f₂ f₃) ≫ snd M (M ⊗ M)) ≫ fst M M

pp: case h_snd
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v, u_1} C
inst✝⁵ : CartesianMonoidalCategory C
inst✝⁴ : Category.{w, u_2} D
inst✝³ : CartesianMonoidalCategory D
M N O X Y : C
inst✝² : MonObj M
inst✝¹ : MonObj N
inst✝ : MonObj O
f₁ f₂ f₃ : X ⟶ M
⊢ ((lift (lift f₁ f₂) f₃ ≫ (α_ M M M).hom) ≫ snd M (M ⊗ M)) ≫ snd M M = (lift f₁ (lift f₂ f₃) ≫ snd M (M ⊗ M)) ≫ snd M M

Tactic:
<;>

Goal state after:
case e_a.e_a.h_fst
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v, u_1} C
inst✝⁵ : CartesianMonoidalCategory C
inst✝⁴ : Category.{w, u_2} D
inst✝³ : CartesianMonoidalCategory D
M N O X Y : C
inst✝² : MonObj M
inst✝¹ : MonObj N
inst✝ : MonObj O
f₁ f₂ f₃ : X ⟶ M
⊢ (lift (lift f₁ f₂) f₃ ≫ (α_ M M M).hom) ≫ fst M (M ⊗ M) = lift f₁ (lift f₂ f₃) ≫ fst M (M ⊗ M)

case h_snd.h_fst
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v, u_1} C
inst✝⁵ : CartesianMonoidalCategory C
inst✝⁴ : Category.{w, u_2} D
inst✝³ : CartesianMonoidalCategory D
M N O X Y : C
inst✝² : MonObj M
inst✝¹ : MonObj N
inst✝ : MonObj O
f₁ f₂ f₃ : X ⟶ M
⊢ ((lift (lift f₁ f₂) f₃ ≫ (α_ M M M).hom) ≫ snd M (M ⊗ M)) ≫ fst M M = (lift f₁ (lift f₂ f₃) ≫ snd M (M ⊗ M)) ≫ fst M M

case h_snd
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v, u_1} C
inst✝⁵ : CartesianMonoidalCategory C
inst✝⁴ : Category.{w, u_2} D
inst✝³ : CartesianMonoidalCategory D
M N O X Y : C
inst✝² : MonObj M
inst✝¹ : MonObj N
inst✝ : MonObj O
f₁ f₂ f₃ : X ⟶ M
⊢ ((lift (lift f₁ f₂) f₃ ≫ (α_ M M M).hom) ≫ snd M (M ⊗ M)) ≫ snd M M = (lift f₁ (lift f₂ f₃) ≫ snd M (M ⊗ M)) ≫ snd M M
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Mon

Goal state before:
pp: case zero
C : Type u_1
inst✝³ : Category.{v, u_1} C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : BraidedCategory C
M N : Mon C
inst✝ : IsCommMonObj N.X
f : M ⟶ N
⊢ (f ^ 0).hom = f.hom ^ 0

pp: case succ
C : Type u_1
inst✝³ : Category.{v, u_1} C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : BraidedCategory C
M N : Mon C
inst✝ : IsCommMonObj N.X
f : M ⟶ N
n✝ : ℕ
a✝ : (f ^ n✝).hom = f.hom ^ n✝
⊢ (f ^ (n✝ + 1)).hom = f.hom ^ (n✝ + 1)

Tactic:
<;>

Goal state after:
case zero
C : Type u_1
inst✝³ : Category.{v, u_1} C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : BraidedCategory C
M N : Mon C
inst✝ : IsCommMonObj N.X
f : M ⟶ N
⊢ (f ^ 0).hom = f.hom ^ 0

case succ
C : Type u_1
inst✝³ : Category.{v, u_1} C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : BraidedCategory C
M N : Mon C
inst✝ : IsCommMonObj N.X
f : M ⟶ N
n✝ : ℕ
a✝ : (f ^ n✝).hom = f.hom ^ n✝
⊢ (f ^ (n✝ + 1)).hom = f.hom ^ (n✝ + 1)
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic

Goal state before:
pp: case h_fst
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : BraidedCategory C
W X Y Z : C
⊢ (tensorμ W X Y Z ≫ fst (W ⊗ Y) (X ⊗ Z)) ≫ fst W Y = (fst W X ⊗ₘ fst Y Z) ≫ fst W Y

pp: case h_snd
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : BraidedCategory C
W X Y Z : C
⊢ (tensorμ W X Y Z ≫ fst (W ⊗ Y) (X ⊗ Z)) ≫ snd W Y = (fst W X ⊗ₘ fst Y Z) ≫ snd W Y

Tactic:
<;>

Goal state after:
case h_fst
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : BraidedCategory C
W X Y Z : C
⊢ (tensorμ W X Y Z ≫ fst (W ⊗ Y) (X ⊗ Z)) ≫ fst W Y = (fst W X ⊗ₘ fst Y Z) ≫ fst W Y

case h_snd
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : BraidedCategory C
W X Y Z : C
⊢ (tensorμ W X Y Z ≫ fst (W ⊗ Y) (X ⊗ Z)) ≫ snd W Y = (fst W X ⊗ₘ fst Y Z) ≫ snd W Y
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic

Goal state before:
pp: case h_fst
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : BraidedCategory C
W X Y Z : C
⊢ (tensorμ W X Y Z ≫ snd (W ⊗ Y) (X ⊗ Z)) ≫ fst X Z = (snd W X ⊗ₘ snd Y Z) ≫ fst X Z

pp: case h_snd
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : BraidedCategory C
W X Y Z : C
⊢ (tensorμ W X Y Z ≫ snd (W ⊗ Y) (X ⊗ Z)) ≫ snd X Z = (snd W X ⊗ₘ snd Y Z) ≫ snd X Z

Tactic:
<;>

Goal state after:
case h_fst
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : BraidedCategory C
W X Y Z : C
⊢ (tensorμ W X Y Z ≫ snd (W ⊗ Y) (X ⊗ Z)) ≫ fst X Z = (snd W X ⊗ₘ snd Y Z) ≫ fst X Z

case h_snd
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : BraidedCategory C
W X Y Z : C
⊢ (tensorμ W X Y Z ≫ snd (W ⊗ Y) (X ⊗ Z)) ≫ snd X Z = (snd W X ⊗ₘ snd Y Z) ≫ snd X Z
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic

Goal state before:
pp: case h_fst
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : BraidedCategory C
W X Y Z : C
⊢ (tensorδ W X Y Z ≫ fst (W ⊗ X) (Y ⊗ Z)) ≫ fst W X = (fst W Y ⊗ₘ fst X Z) ≫ fst W X

pp: case h_snd
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : BraidedCategory C
W X Y Z : C
⊢ (tensorδ W X Y Z ≫ fst (W ⊗ X) (Y ⊗ Z)) ≫ snd W X = (fst W Y ⊗ₘ fst X Z) ≫ snd W X

Tactic:
<;>

Goal state after:
case h_fst
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : BraidedCategory C
W X Y Z : C
⊢ (tensorδ W X Y Z ≫ fst (W ⊗ X) (Y ⊗ Z)) ≫ fst W X = (fst W Y ⊗ₘ fst X Z) ≫ fst W X

case h_snd
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : BraidedCategory C
W X Y Z : C
⊢ (tensorδ W X Y Z ≫ fst (W ⊗ X) (Y ⊗ Z)) ≫ snd W X = (fst W Y ⊗ₘ fst X Z) ≫ snd W X
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic

Goal state before:
pp: case h_fst
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : BraidedCategory C
W X Y Z : C
⊢ (tensorδ W X Y Z ≫ snd (W ⊗ X) (Y ⊗ Z)) ≫ fst Y Z = (snd W Y ⊗ₘ snd X Z) ≫ fst Y Z

pp: case h_snd
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : BraidedCategory C
W X Y Z : C
⊢ (tensorδ W X Y Z ≫ snd (W ⊗ X) (Y ⊗ Z)) ≫ snd Y Z = (snd W Y ⊗ₘ snd X Z) ≫ snd Y Z

Tactic:
<;>

Goal state after:
case h_fst
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : BraidedCategory C
W X Y Z : C
⊢ (tensorδ W X Y Z ≫ snd (W ⊗ X) (Y ⊗ Z)) ≫ fst Y Z = (snd W Y ⊗ₘ snd X Z) ≫ fst Y Z

case h_snd
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : BraidedCategory C
W X Y Z : C
⊢ (tensorδ W X Y Z ≫ snd (W ⊗ X) (Y ⊗ Z)) ≫ snd Y Z = (snd W Y ⊗ₘ snd X Z) ≫ snd Y Z
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Mon

Goal state before:
pp: case e_a.h_fst
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v, u_1} C
inst✝⁵ : CartesianMonoidalCategory C
inst✝⁴ : Category.{w, u_2} D
inst✝³ : CartesianMonoidalCategory D
M✝ N✝ O X Y : C
inst✝² : MonObj M✝
inst✝¹ : MonObj N✝
inst✝ : MonObj O
M N : Mon C
α : yonedaMonObj M.X ⟶ yonedaMonObj N.X
⊢ lift ((MonCat.Hom.hom (α.app (op (M.X ⊗ M.X)))) (fst M.X M.X))
        ((MonCat.Hom.hom (α.app (op (M.X ⊗ M.X)))) (snd M.X M.X)) ≫
      fst N.X N.X =
    ((ConcreteCategory.hom (α.app (op M.X))) (𝟙 M.X) ⊗ₘ (ConcreteCategory.hom (α.app (op M.X))) (𝟙 M.X)) ≫ fst N.X N.X

pp: case h_snd
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v, u_1} C
inst✝⁵ : CartesianMonoidalCategory C
inst✝⁴ : Category.{w, u_2} D
inst✝³ : CartesianMonoidalCategory D
M✝ N✝ O X Y : C
inst✝² : MonObj M✝
inst✝¹ : MonObj N✝
inst✝ : MonObj O
M N : Mon C
α : yonedaMonObj M.X ⟶ yonedaMonObj N.X
⊢ lift ((MonCat.Hom.hom (α.app (op (M.X ⊗ M.X)))) (fst M.X M.X))
        ((MonCat.Hom.hom (α.app (op (M.X ⊗ M.X)))) (snd M.X M.X)) ≫
      snd N.X N.X =
    ((ConcreteCategory.hom (α.app (op M.X))) (𝟙 M.X) ⊗ₘ (ConcreteCategory.hom (α.app (op M.X))) (𝟙 M.X)) ≫ snd N.X N.X

Tactic:
<;>

Goal state after:
case e_a.h_fst
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v, u_1} C
inst✝⁵ : CartesianMonoidalCategory C
inst✝⁴ : Category.{w, u_2} D
inst✝³ : CartesianMonoidalCategory D
M✝ N✝ O X Y : C
inst✝² : MonObj M✝
inst✝¹ : MonObj N✝
inst✝ : MonObj O
M N : Mon C
α : yonedaMonObj M.X ⟶ yonedaMonObj N.X
⊢ lift ((MonCat.Hom.hom (α.app (op (M.X ⊗ M.X)))) (fst M.X M.X))
        ((MonCat.Hom.hom (α.app (op (M.X ⊗ M.X)))) (snd M.X M.X)) ≫
      fst N.X N.X =
    ((ConcreteCategory.hom (α.app (op M.X))) (𝟙 M.X) ⊗ₘ (ConcreteCategory.hom (α.app (op M.X))) (𝟙 M.X)) ≫ fst N.X N.X

case h_snd
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v, u_1} C
inst✝⁵ : CartesianMonoidalCategory C
inst✝⁴ : Category.{w, u_2} D
inst✝³ : CartesianMonoidalCategory D
M✝ N✝ O X Y : C
inst✝² : MonObj M✝
inst✝¹ : MonObj N✝
inst✝ : MonObj O
M N : Mon C
α : yonedaMonObj M.X ⟶ yonedaMonObj N.X
⊢ lift ((MonCat.Hom.hom (α.app (op (M.X ⊗ M.X)))) (fst M.X M.X))
        ((MonCat.Hom.hom (α.app (op (M.X ⊗ M.X)))) (snd M.X M.X)) ≫
      snd N.X N.X =
    ((ConcreteCategory.hom (α.app (op M.X))) (𝟙 M.X) ⊗ₘ (ConcreteCategory.hom (α.app (op M.X))) (𝟙 M.X)) ≫ snd N.X N.X
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Mon

Goal state before:
pp: case zero
C : Type u_1
inst✝⁴ : Category.{v, u_1} C
inst✝³ : CartesianMonoidalCategory C
M N X : C
inst✝² : MonObj M
inst✝¹ : MonObj N
f : X ⟶ M
g : M ⟶ N
inst✝ : IsMonHom g
⊢ (f ^ 0) ≫ g = (f ≫ g) ^ 0

pp: case succ
C : Type u_1
inst✝⁴ : Category.{v, u_1} C
inst✝³ : CartesianMonoidalCategory C
M N X : C
inst✝² : MonObj M
inst✝¹ : MonObj N
f : X ⟶ M
g : M ⟶ N
inst✝ : IsMonHom g
n✝ : ℕ
a✝ : (f ^ n✝) ≫ g = (f ≫ g) ^ n✝
⊢ (f ^ (n✝ + 1)) ≫ g = (f ≫ g) ^ (n✝ + 1)

Tactic:
<;>

Goal state after:
case zero
C : Type u_1
inst✝⁴ : Category.{v, u_1} C
inst✝³ : CartesianMonoidalCategory C
M N X : C
inst✝² : MonObj M
inst✝¹ : MonObj N
f : X ⟶ M
g : M ⟶ N
inst✝ : IsMonHom g
⊢ (f ^ 0) ≫ g = (f ≫ g) ^ 0

case succ
C : Type u_1
inst✝⁴ : Category.{v, u_1} C
inst✝³ : CartesianMonoidalCategory C
M N X : C
inst✝² : MonObj M
inst✝¹ : MonObj N
f : X ⟶ M
g : M ⟶ N
inst✝ : IsMonHom g
n✝ : ℕ
a✝ : (f ^ n✝) ≫ g = (f ≫ g) ^ n✝
⊢ (f ^ (n✝ + 1)) ≫ g = (f ≫ g) ^ (n✝ + 1)
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Mon

Goal state before:
pp: case zero
C : Type u_1
inst✝² : Category.{v, u_1} C
inst✝¹ : CartesianMonoidalCategory C
M X Y : C
inst✝ : MonObj M
f : X ⟶ M
h : Y ⟶ X
⊢ h ≫ f ^ 0 = (h ≫ f) ^ 0

pp: case succ
C : Type u_1
inst✝² : Category.{v, u_1} C
inst✝¹ : CartesianMonoidalCategory C
M X Y : C
inst✝ : MonObj M
f : X ⟶ M
h : Y ⟶ X
n✝ : ℕ
a✝ : h ≫ f ^ n✝ = (h ≫ f) ^ n✝
⊢ h ≫ f ^ (n✝ + 1) = (h ≫ f) ^ (n✝ + 1)

Tactic:
<;>

Goal state after:
case zero
C : Type u_1
inst✝² : Category.{v, u_1} C
inst✝¹ : CartesianMonoidalCategory C
M X Y : C
inst✝ : MonObj M
f : X ⟶ M
h : Y ⟶ X
⊢ h ≫ f ^ 0 = (h ≫ f) ^ 0

case succ
C : Type u_1
inst✝² : Category.{v, u_1} C
inst✝¹ : CartesianMonoidalCategory C
M X Y : C
inst✝ : MonObj M
f : X ⟶ M
h : Y ⟶ X
n✝ : ℕ
a✝ : h ≫ f ^ n✝ = (h ≫ f) ^ n✝
⊢ h ≫ f ^ (n✝ + 1) = (h ≫ f) ^ (n✝ + 1)
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic

Goal state before:
pp: case h_fst
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
A B A' B' : C
f : A ⟶ A'
g : B ⟶ B'
⊢ (F.map (f ⊗ₘ g) ≫ prodComparison F A' B') ≫ fst (F.obj A') (F.obj B') =
    (prodComparison F A B ≫ (F.map f ⊗ₘ F.map g)) ≫ fst (F.obj A') (F.obj B')

pp: case h_snd
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
A B A' B' : C
f : A ⟶ A'
g : B ⟶ B'
⊢ (F.map (f ⊗ₘ g) ≫ prodComparison F A' B') ≫ snd (F.obj A') (F.obj B') =
    (prodComparison F A B ≫ (F.map f ⊗ₘ F.map g)) ≫ snd (F.obj A') (F.obj B')

Tactic:
<;>

Goal state after:
case h_fst
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
A B A' B' : C
f : A ⟶ A'
g : B ⟶ B'
⊢ (F.map (f ⊗ₘ g) ≫ prodComparison F A' B') ≫ fst (F.obj A') (F.obj B') =
    (prodComparison F A B ≫ (F.map f ⊗ₘ F.map g)) ≫ fst (F.obj A') (F.obj B')

case h_snd
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
A B A' B' : C
f : A ⟶ A'
g : B ⟶ B'
⊢ (F.map (f ⊗ₘ g) ≫ prodComparison F A' B') ≫ snd (F.obj A') (F.obj B') =
    (prodComparison F A B ≫ (F.map f ⊗ₘ F.map g)) ≫ snd (F.obj A') (F.obj B')
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic

Goal state before:
pp: case h_fst
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
A B B' : C
g : B ⟶ B'
⊢ (F.map (A ◁ g) ≫ prodComparison F A B') ≫ fst (F.obj A) (F.obj B') =
    (prodComparison F A B ≫ F.obj A ◁ F.map g) ≫ fst (F.obj A) (F.obj B')

pp: case h_snd
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
A B B' : C
g : B ⟶ B'
⊢ (F.map (A ◁ g) ≫ prodComparison F A B') ≫ snd (F.obj A) (F.obj B') =
    (prodComparison F A B ≫ F.obj A ◁ F.map g) ≫ snd (F.obj A) (F.obj B')

Tactic:
<;>

Goal state after:
case h_fst
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
A B B' : C
g : B ⟶ B'
⊢ (F.map (A ◁ g) ≫ prodComparison F A B') ≫ fst (F.obj A) (F.obj B') =
    (prodComparison F A B ≫ F.obj A ◁ F.map g) ≫ fst (F.obj A) (F.obj B')

case h_snd
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
A B B' : C
g : B ⟶ B'
⊢ (F.map (A ◁ g) ≫ prodComparison F A B') ≫ snd (F.obj A) (F.obj B') =
    (prodComparison F A B ≫ F.obj A ◁ F.map g) ≫ snd (F.obj A) (F.obj B')
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic

Goal state before:
pp: case h_fst
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
A B A' : C
f : A ⟶ A'
⊢ (F.map (f ▷ B) ≫ prodComparison F A' B) ≫ fst (F.obj A') (F.obj B) =
    (prodComparison F A B ≫ F.map f ▷ F.obj B) ≫ fst (F.obj A') (F.obj B)

pp: case h_snd
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
A B A' : C
f : A ⟶ A'
⊢ (F.map (f ▷ B) ≫ prodComparison F A' B) ≫ snd (F.obj A') (F.obj B) =
    (prodComparison F A B ≫ F.map f ▷ F.obj B) ≫ snd (F.obj A') (F.obj B)

Tactic:
<;>

Goal state after:
case h_fst
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
A B A' : C
f : A ⟶ A'
⊢ (F.map (f ▷ B) ≫ prodComparison F A' B) ≫ fst (F.obj A') (F.obj B) =
    (prodComparison F A B ≫ F.map f ▷ F.obj B) ≫ fst (F.obj A') (F.obj B)

case h_snd
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
A B A' : C
f : A ⟶ A'
⊢ (F.map (f ▷ B) ≫ prodComparison F A' B) ≫ snd (F.obj A') (F.obj B) =
    (prodComparison F A B ≫ F.map f ▷ F.obj B) ≫ snd (F.obj A') (F.obj B)
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic

Goal state before:
pp: 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
A B B' : C
inst✝¹ : IsIso (prodComparison F A B)
g : B ⟶ B'
inst✝ : IsIso (prodComparison F A B')
⊢ inv (prodComparison F A B) ≫ F.map (A ◁ g) = F.obj A ◁ F.map g ≫ inv (prodComparison F A B')

Tactic:
by
  rw [IsIso.eq_comp_inv, Category.assoc, IsIso.inv_comp_eq, prodComparison_natural_whiskerLeft]

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

Goal state before:
pp: case h_fst
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 : C
⊢ lift ((F ⋙ G).map (fst A B)) ((F ⋙ G).map (snd A B)) ≫ fst ((F ⋙ G).obj A) ((F ⋙ G).obj B) =
    (G.map (lift (F.map (fst A B)) (F.map (snd A B))) ≫
        lift (G.map (fst (F.obj A) (F.obj B))) (G.map (snd (F.obj A) (F.obj B)))) ≫
      fst ((F ⋙ G).obj A) ((F ⋙ G).obj B)

pp: case h_snd
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 : C
⊢ lift ((F ⋙ G).map (fst A B)) ((F ⋙ G).map (snd A B)) ≫ snd ((F ⋙ G).obj A) ((F ⋙ G).obj B) =
    (G.map (lift (F.map (fst A B)) (F.map (snd A B))) ≫
        lift (G.map (fst (F.obj A) (F.obj B))) (G.map (snd (F.obj A) (F.obj B)))) ≫
      snd ((F ⋙ G).obj A) ((F ⋙ G).obj B)

Tactic:
<;>

Goal state after:
case h_fst
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 : C
⊢ lift ((F ⋙ G).map (fst A B)) ((F ⋙ G).map (snd A B)) ≫ fst ((F ⋙ G).obj A) ((F ⋙ G).obj B) =
    (G.map (lift (F.map (fst A B)) (F.map (snd A B))) ≫
        lift (G.map (fst (F.obj A) (F.obj B))) (G.map (snd (F.obj A) (F.obj B)))) ≫
      fst ((F ⋙ G).obj A) ((F ⋙ G).obj B)

case h_snd
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 : C
⊢ lift ((F ⋙ G).map (fst A B)) ((F ⋙ G).map (snd A B)) ≫ snd ((F ⋙ G).obj A) ((F ⋙ G).obj B) =
    (G.map (lift (F.map (fst A B)) (F.map (snd A B))) ≫
        lift (G.map (fst (F.obj A) (F.obj B))) (G.map (snd (F.obj A) (F.obj B)))) ≫
      snd ((F ⋙ G).obj A) ((F ⋙ G).obj B)
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic

Goal state before:
pp: case h_fst
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' A x y : C
f : x ⟶ y
⊢ (((curriedTensor C).obj A ⋙ F).map f ≫ prodComparison F A y) ≫ fst (F.obj A) (F.obj y) =
    (prodComparison F A x ≫ (F ⋙ (curriedTensor D).obj (F.obj A)).map f) ≫ fst (F.obj A) (F.obj y)

pp: case h_snd
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' A x y : C
f : x ⟶ y
⊢ (((curriedTensor C).obj A ⋙ F).map f ≫ prodComparison F A y) ≫ snd (F.obj A) (F.obj y) =
    (prodComparison F A x ≫ (F ⋙ (curriedTensor D).obj (F.obj A)).map f) ≫ snd (F.obj A) (F.obj y)

Tactic:
<;>

Goal state after:
case h_fst
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' A x y : C
f : x ⟶ y
⊢ (((curriedTensor C).obj A ⋙ F).map f ≫ prodComparison F A y) ≫ fst (F.obj A) (F.obj y) =
    (prodComparison F A x ≫ (F ⋙ (curriedTensor D).obj (F.obj A)).map f) ≫ fst (F.obj A) (F.obj y)

case h_snd
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' A x y : C
f : x ⟶ y
⊢ (((curriedTensor C).obj A ⋙ F).map f ≫ prodComparison F A y) ≫ snd (F.obj A) (F.obj y) =
    (prodComparison F A x ≫ (F ⋙ (curriedTensor D).obj (F.obj A)).map f) ≫ snd (F.obj A) (F.obj y)