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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategoryStruct C
id_tensorHom_id : ∀ (X₁ X₂ : C), 𝟙 X₁ ⊗ₘ 𝟙 X₂ = 𝟙 (X₁ ⊗ X₂)
id_tensorHom : ∀ (X : C) {Y₁ Y₂ : C} (f : Y₁ ⟶ Y₂), 𝟙 X ⊗ₘ f = X ◁ f
tensorHom_id : ∀ {X₁ X₂ : C} (f : X₁ ⟶ X₂) (Y : C), f ⊗ₘ 𝟙 Y = f ▷ Y
tensorHom_comp_tensorHom :
  ∀ {X₁ Y₁ Z₁ X₂ Y₂ Z₂ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (g₁ : Y₁ ⟶ Z₁) (g₂ : Y₂ ⟶ Z₂),
    (f₁ ⊗ₘ f₂) ≫ (g₁ ⊗ₘ g₂) = f₁ ≫ g₁ ⊗ₘ f₂ ≫ g₂
associator_naturality :
  ∀ {X₁ X₂ X₃ Y₁ Y₂ Y₃ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (f₃ : X₃ ⟶ Y₃),
    ((f₁ ⊗ₘ f₂) ⊗ₘ f₃) ≫ (α_ Y₁ Y₂ Y₃).hom = (α_ X₁ X₂ X₃).hom ≫ (f₁ ⊗ₘ f₂ ⊗ₘ f₃)
leftUnitor_naturality : ∀ {X Y : C} (f : X ⟶ Y), (𝟙 (𝟙_ C) ⊗ₘ f) ≫ (λ_ Y).hom = (λ_ X).hom ≫ f
rightUnitor_naturality : ∀ {X Y : C} (f : X ⟶ Y), (f ⊗ₘ 𝟙 (𝟙_ C)) ≫ (ρ_ Y).hom = (ρ_ X).hom ≫ f
pentagon :
  ∀ (W X Y Z : C),
    ((α_ W X Y).hom ⊗ₘ 𝟙 Z) ≫ (α_ W (X ⊗ Y) Z).hom ≫ (𝟙 W ⊗ₘ (α_ X Y Z).hom) =
      (α_ (W ⊗ X) Y Z).hom ≫ (α_ W X (Y ⊗ Z)).hom
triangle : ∀ (X Y : C), (α_ X (𝟙_ C) Y).hom ≫ (𝟙 X ⊗ₘ (λ_ Y).hom) = (ρ_ X).hom ⊗ₘ 𝟙 Y
X✝ Y✝ : C
⊢ 𝟙 X✝ ▷ Y✝ = 𝟙 (X✝ ⊗ Y✝)

Tactic:
;

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategoryStruct C
id_tensorHom_id : ∀ (X₁ X₂ : C), 𝟙 X₁ ⊗ₘ 𝟙 X₂ = 𝟙 (X₁ ⊗ X₂)
id_tensorHom : ∀ (X : C) {Y₁ Y₂ : C} (f : Y₁ ⟶ Y₂), 𝟙 X ⊗ₘ f = X ◁ f
tensorHom_id : ∀ {X₁ X₂ : C} (f : X₁ ⟶ X₂) (Y : C), f ⊗ₘ 𝟙 Y = f ▷ Y
tensorHom_comp_tensorHom :
  ∀ {X₁ Y₁ Z₁ X₂ Y₂ Z₂ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (g₁ : Y₁ ⟶ Z₁) (g₂ : Y₂ ⟶ Z₂),
    (f₁ ⊗ₘ f₂) ≫ (g₁ ⊗ₘ g₂) = f₁ ≫ g₁ ⊗ₘ f₂ ≫ g₂
associator_naturality :
  ∀ {X₁ X₂ X₃ Y₁ Y₂ Y₃ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (f₃ : X₃ ⟶ Y₃),
    ((f₁ ⊗ₘ f₂) ⊗ₘ f₃) ≫ (α_ Y₁ Y₂ Y₃).hom = (α_ X₁ X₂ X₃).hom ≫ (f₁ ⊗ₘ f₂ ⊗ₘ f₃)
leftUnitor_naturality : ∀ {X Y : C} (f : X ⟶ Y), (𝟙 (𝟙_ C) ⊗ₘ f) ≫ (λ_ Y).hom = (λ_ X).hom ≫ f
rightUnitor_naturality : ∀ {X Y : C} (f : X ⟶ Y), (f ⊗ₘ 𝟙 (𝟙_ C)) ≫ (ρ_ Y).hom = (ρ_ X).hom ≫ f
pentagon :
  ∀ (W X Y Z : C),
    ((α_ W X Y).hom ⊗ₘ 𝟙 Z) ≫ (α_ W (X ⊗ Y) Z).hom ≫ (𝟙 W ⊗ₘ (α_ X Y Z).hom) =
      (α_ (W ⊗ X) Y Z).hom ≫ (α_ W X (Y ⊗ Z)).hom
triangle : ∀ (X Y : C), (α_ X (𝟙_ C) Y).hom ≫ (𝟙 X ⊗ₘ (λ_ Y).hom) = (ρ_ X).hom ⊗ₘ 𝟙 Y
X✝ Y✝ : C
⊢ 𝟙 X✝ ▷ Y✝ = 𝟙 (X✝ ⊗ Y✝)
Module: Mathlib.CategoryTheory.Adjunction.FullyFaithful

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝¹ : L.Faithful
inst✝ : L.Full
X : D
⊢ IsIso (h.counit.app X) ↔ L.essImage X

Tactic:
by
  constructor
  · intro
    exact ⟨R.obj X, ⟨asIso (h.counit.app X)⟩⟩
  · rintro ⟨_, ⟨i⟩⟩
    rw [NatTrans.isIso_app_iff_of_iso _ i.symm]
    infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Category

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategoryStruct C
id_tensorHom_id : ∀ (X₁ X₂ : C), 𝟙 X₁ ⊗ₘ 𝟙 X₂ = 𝟙 (X₁ ⊗ X₂)
id_tensorHom : ∀ (X : C) {Y₁ Y₂ : C} (f : Y₁ ⟶ Y₂), 𝟙 X ⊗ₘ f = X ◁ f
tensorHom_id : ∀ {X₁ X₂ : C} (f : X₁ ⟶ X₂) (Y : C), f ⊗ₘ 𝟙 Y = f ▷ Y
tensorHom_comp_tensorHom :
  ∀ {X₁ Y₁ Z₁ X₂ Y₂ Z₂ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (g₁ : Y₁ ⟶ Z₁) (g₂ : Y₂ ⟶ Z₂),
    (f₁ ⊗ₘ f₂) ≫ (g₁ ⊗ₘ g₂) = f₁ ≫ g₁ ⊗ₘ f₂ ≫ g₂
associator_naturality :
  ∀ {X₁ X₂ X₃ Y₁ Y₂ Y₃ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (f₃ : X₃ ⟶ Y₃),
    ((f₁ ⊗ₘ f₂) ⊗ₘ f₃) ≫ (α_ Y₁ Y₂ Y₃).hom = (α_ X₁ X₂ X₃).hom ≫ (f₁ ⊗ₘ f₂ ⊗ₘ f₃)
leftUnitor_naturality : ∀ {X Y : C} (f : X ⟶ Y), (𝟙 (𝟙_ C) ⊗ₘ f) ≫ (λ_ Y).hom = (λ_ X).hom ≫ f
rightUnitor_naturality : ∀ {X Y : C} (f : X ⟶ Y), (f ⊗ₘ 𝟙 (𝟙_ C)) ≫ (ρ_ Y).hom = (ρ_ X).hom ≫ f
pentagon :
  ∀ (W X Y Z : C),
    ((α_ W X Y).hom ⊗ₘ 𝟙 Z) ≫ (α_ W (X ⊗ Y) Z).hom ≫ (𝟙 W ⊗ₘ (α_ X Y Z).hom) =
      (α_ (W ⊗ X) Y Z).hom ≫ (α_ W X (Y ⊗ Z)).hom
triangle : ∀ (X Y : C), (α_ X (𝟙_ C) Y).hom ≫ (𝟙 X ⊗ₘ (λ_ Y).hom) = (ρ_ X).hom ⊗ₘ 𝟙 Y
W✝ X✝ Y✝ Z✝ : C
⊢ (α_ W✝ X✝ Y✝).hom ▷ Z✝ ≫ (α_ W✝ (X✝ ⊗ Y✝) Z✝).hom ≫ W✝ ◁ (α_ X✝ Y✝ Z✝).hom =
    (α_ (W✝ ⊗ X✝) Y✝ Z✝).hom ≫ (α_ W✝ X✝ (Y✝ ⊗ Z✝)).hom

Tactic:
;

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategoryStruct C
id_tensorHom_id : ∀ (X₁ X₂ : C), 𝟙 X₁ ⊗ₘ 𝟙 X₂ = 𝟙 (X₁ ⊗ X₂)
id_tensorHom : ∀ (X : C) {Y₁ Y₂ : C} (f : Y₁ ⟶ Y₂), 𝟙 X ⊗ₘ f = X ◁ f
tensorHom_id : ∀ {X₁ X₂ : C} (f : X₁ ⟶ X₂) (Y : C), f ⊗ₘ 𝟙 Y = f ▷ Y
tensorHom_comp_tensorHom :
  ∀ {X₁ Y₁ Z₁ X₂ Y₂ Z₂ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (g₁ : Y₁ ⟶ Z₁) (g₂ : Y₂ ⟶ Z₂),
    (f₁ ⊗ₘ f₂) ≫ (g₁ ⊗ₘ g₂) = f₁ ≫ g₁ ⊗ₘ f₂ ≫ g₂
associator_naturality :
  ∀ {X₁ X₂ X₃ Y₁ Y₂ Y₃ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (f₃ : X₃ ⟶ Y₃),
    ((f₁ ⊗ₘ f₂) ⊗ₘ f₃) ≫ (α_ Y₁ Y₂ Y₃).hom = (α_ X₁ X₂ X₃).hom ≫ (f₁ ⊗ₘ f₂ ⊗ₘ f₃)
leftUnitor_naturality : ∀ {X Y : C} (f : X ⟶ Y), (𝟙 (𝟙_ C) ⊗ₘ f) ≫ (λ_ Y).hom = (λ_ X).hom ≫ f
rightUnitor_naturality : ∀ {X Y : C} (f : X ⟶ Y), (f ⊗ₘ 𝟙 (𝟙_ C)) ≫ (ρ_ Y).hom = (ρ_ X).hom ≫ f
pentagon :
  ∀ (W X Y Z : C),
    ((α_ W X Y).hom ⊗ₘ 𝟙 Z) ≫ (α_ W (X ⊗ Y) Z).hom ≫ (𝟙 W ⊗ₘ (α_ X Y Z).hom) =
      (α_ (W ⊗ X) Y Z).hom ≫ (α_ W X (Y ⊗ Z)).hom
triangle : ∀ (X Y : C), (α_ X (𝟙_ C) Y).hom ≫ (𝟙 X ⊗ₘ (λ_ Y).hom) = (ρ_ X).hom ⊗ₘ 𝟙 Y
W✝ X✝ Y✝ Z✝ : C
⊢ (α_ W✝ X✝ Y✝).hom ▷ Z✝ ≫ (α_ W✝ (X✝ ⊗ Y✝) Z✝).hom ≫ W✝ ◁ (α_ X✝ Y✝ Z✝).hom =
    (α_ (W✝ ⊗ X✝) Y✝ Z✝).hom ≫ (α_ W✝ X✝ (Y✝ ⊗ Z✝)).hom
Module: Mathlib.CategoryTheory.Monoidal.Category

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategoryStruct C
id_tensorHom_id : ∀ (X₁ X₂ : C), 𝟙 X₁ ⊗ₘ 𝟙 X₂ = 𝟙 (X₁ ⊗ X₂)
id_tensorHom : ∀ (X : C) {Y₁ Y₂ : C} (f : Y₁ ⟶ Y₂), 𝟙 X ⊗ₘ f = X ◁ f
tensorHom_id : ∀ {X₁ X₂ : C} (f : X₁ ⟶ X₂) (Y : C), f ⊗ₘ 𝟙 Y = f ▷ Y
tensorHom_comp_tensorHom :
  ∀ {X₁ Y₁ Z₁ X₂ Y₂ Z₂ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (g₁ : Y₁ ⟶ Z₁) (g₂ : Y₂ ⟶ Z₂),
    (f₁ ⊗ₘ f₂) ≫ (g₁ ⊗ₘ g₂) = f₁ ≫ g₁ ⊗ₘ f₂ ≫ g₂
associator_naturality :
  ∀ {X₁ X₂ X₃ Y₁ Y₂ Y₃ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (f₃ : X₃ ⟶ Y₃),
    ((f₁ ⊗ₘ f₂) ⊗ₘ f₃) ≫ (α_ Y₁ Y₂ Y₃).hom = (α_ X₁ X₂ X₃).hom ≫ (f₁ ⊗ₘ f₂ ⊗ₘ f₃)
leftUnitor_naturality : ∀ {X Y : C} (f : X ⟶ Y), (𝟙 (𝟙_ C) ⊗ₘ f) ≫ (λ_ Y).hom = (λ_ X).hom ≫ f
rightUnitor_naturality : ∀ {X Y : C} (f : X ⟶ Y), (f ⊗ₘ 𝟙 (𝟙_ C)) ≫ (ρ_ Y).hom = (ρ_ X).hom ≫ f
pentagon :
  ∀ (W X Y Z : C),
    ((α_ W X Y).hom ⊗ₘ 𝟙 Z) ≫ (α_ W (X ⊗ Y) Z).hom ≫ (𝟙 W ⊗ₘ (α_ X Y Z).hom) =
      (α_ (W ⊗ X) Y Z).hom ≫ (α_ W X (Y ⊗ Z)).hom
triangle : ∀ (X Y : C), (α_ X (𝟙_ C) Y).hom ≫ (𝟙 X ⊗ₘ (λ_ Y).hom) = (ρ_ X).hom ⊗ₘ 𝟙 Y
X✝ Y✝ : C
⊢ (α_ X✝ (𝟙_ C) Y✝).hom ≫ X✝ ◁ (λ_ Y✝).hom = (ρ_ X✝).hom ▷ Y✝

Tactic:
;

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategoryStruct C
id_tensorHom_id : ∀ (X₁ X₂ : C), 𝟙 X₁ ⊗ₘ 𝟙 X₂ = 𝟙 (X₁ ⊗ X₂)
id_tensorHom : ∀ (X : C) {Y₁ Y₂ : C} (f : Y₁ ⟶ Y₂), 𝟙 X ⊗ₘ f = X ◁ f
tensorHom_id : ∀ {X₁ X₂ : C} (f : X₁ ⟶ X₂) (Y : C), f ⊗ₘ 𝟙 Y = f ▷ Y
tensorHom_comp_tensorHom :
  ∀ {X₁ Y₁ Z₁ X₂ Y₂ Z₂ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (g₁ : Y₁ ⟶ Z₁) (g₂ : Y₂ ⟶ Z₂),
    (f₁ ⊗ₘ f₂) ≫ (g₁ ⊗ₘ g₂) = f₁ ≫ g₁ ⊗ₘ f₂ ≫ g₂
associator_naturality :
  ∀ {X₁ X₂ X₃ Y₁ Y₂ Y₃ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (f₃ : X₃ ⟶ Y₃),
    ((f₁ ⊗ₘ f₂) ⊗ₘ f₃) ≫ (α_ Y₁ Y₂ Y₃).hom = (α_ X₁ X₂ X₃).hom ≫ (f₁ ⊗ₘ f₂ ⊗ₘ f₃)
leftUnitor_naturality : ∀ {X Y : C} (f : X ⟶ Y), (𝟙 (𝟙_ C) ⊗ₘ f) ≫ (λ_ Y).hom = (λ_ X).hom ≫ f
rightUnitor_naturality : ∀ {X Y : C} (f : X ⟶ Y), (f ⊗ₘ 𝟙 (𝟙_ C)) ≫ (ρ_ Y).hom = (ρ_ X).hom ≫ f
pentagon :
  ∀ (W X Y Z : C),
    ((α_ W X Y).hom ⊗ₘ 𝟙 Z) ≫ (α_ W (X ⊗ Y) Z).hom ≫ (𝟙 W ⊗ₘ (α_ X Y Z).hom) =
      (α_ (W ⊗ X) Y Z).hom ≫ (α_ W X (Y ⊗ Z)).hom
triangle : ∀ (X Y : C), (α_ X (𝟙_ C) Y).hom ≫ (𝟙 X ⊗ₘ (λ_ Y).hom) = (ρ_ X).hom ⊗ₘ 𝟙 Y
X✝ Y✝ : C
⊢ (α_ X✝ (𝟙_ C) Y✝).hom ≫ X✝ ◁ (λ_ Y✝).hom = (ρ_ X✝).hom ▷ Y✝
Module: Mathlib.CategoryTheory.Monoidal.Category

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y : C
f : X ⟶ Y
⊢ 𝟙_ C ◁ f = (𝟙_ C ◁ f ≫ (λ_ Y).hom) ≫ (λ_ Y).inv

Tactic:
;

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y : C
f : X ⟶ Y
⊢ 𝟙_ C ◁ f = (𝟙_ C ◁ f ≫ (λ_ Y).hom) ≫ (λ_ Y).inv
Module: Mathlib.CategoryTheory.Monoidal.Category

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y : C
f : X ⟶ Y
⊢ f ▷ 𝟙_ C = (f ▷ 𝟙_ C ≫ (ρ_ Y).hom) ≫ (ρ_ Y).inv

Tactic:
;

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y : C
f : X ⟶ Y
⊢ f ▷ 𝟙_ C = (f ▷ 𝟙_ C ≫ (ρ_ Y).hom) ≫ (ρ_ Y).inv
Module: Mathlib.CategoryTheory.Monoidal.Category

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
P : ObjectProperty C
tensorUnit : P (𝟙_ C)
tensorObj : ∀ (X Y : C), P X → P Y → P (X ⊗ Y)
X₁✝ Y₁✝ X₂✝ Y₂✝ : P.FullSubcategory
x✝¹ : X₁✝ ⟶ Y₁✝
x✝ : X₂✝ ⟶ Y₂✝
⊢ (homMk (x✝¹.hom ⊗ₘ x✝.hom)).hom = (homMk (x✝¹.hom ▷ X₂✝.obj) ≫ homMk (Y₁✝.obj ◁ x✝.hom)).hom

Tactic:
;

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
P : ObjectProperty C
tensorUnit : P (𝟙_ C)
tensorObj : ∀ (X Y : C), P X → P Y → P (X ⊗ Y)
X₁✝ Y₁✝ X₂✝ Y₂✝ : P.FullSubcategory
x✝¹ : X₁✝ ⟶ Y₁✝
x✝ : X₂✝ ⟶ Y₂✝
⊢ (homMk (x✝¹.hom ⊗ₘ x✝.hom)).hom = (homMk (x✝¹.hom ▷ X₂✝.obj) ≫ homMk (Y₁✝.obj ◁ x✝.hom)).hom
Module: Mathlib.CategoryTheory.Monoidal.Category

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
P : ObjectProperty C
tensorUnit : P (𝟙_ C)
tensorObj : ∀ (X Y : C), P X → P Y → P (X ⊗ Y)
X₁✝ Y₁✝ X₂✝ Y₂✝ : P.FullSubcategory
x✝¹ : X₁✝ ⟶ Y₁✝
x✝ : X₂✝ ⟶ Y₂✝
⊢ homMk (x✝¹.hom ⊗ₘ x✝.hom) = homMk (x✝¹.hom ▷ X₂✝.obj) ≫ homMk (Y₁✝.obj ◁ x✝.hom)

Tactic:
by ext; apply tensorHom_def

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Transport

Goal state before:
pp: case mk
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategoryStruct D
F : D ⥤ C
inst✝ : F.Faithful
X₁ X₂ : D
μIso✝ : (X Y : D) → F.obj X ⊗ F.obj Y ≅ F.obj (X ⊗ Y)
whiskerLeft_eq✝ :
  ∀ (X : D) {Y₁ Y₂ : D} (f : Y₁ ⟶ Y₂), F.map (X ◁ f) = (μIso✝ X Y₁).inv ≫ F.obj X ◁ F.map f ≫ (μIso✝ X Y₂).hom
whiskerRight_eq✝ :
  ∀ {X₁ X₂ : D} (f : X₁ ⟶ X₂) (Y : D), F.map (f ▷ Y) = (μIso✝ X₁ Y).inv ≫ F.map f ▷ F.obj Y ≫ (μIso✝ X₂ Y).hom
tensorHom_eq✝ :
  ∀ {X₁ Y₁ X₂ Y₂ : D} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂),
    F.map (f ⊗ₘ g) = (μIso✝ X₁ X₂).inv ≫ (F.map f ⊗ₘ F.map g) ≫ (μIso✝ Y₁ Y₂).hom
εIso✝ : 𝟙_ C ≅ F.obj (𝟙_ D)
associator_eq✝ :
  ∀ (X Y Z : D),
    F.map (α_ X Y Z).hom =
      (((μIso✝ (X ⊗ Y) Z).symm ≪≫ ((μIso✝ X Y).symm ⊗ᵢ Iso.refl (F.obj Z))) ≪≫
          α_ (F.obj X) (F.obj Y) (F.obj Z) ≪≫ (Iso.refl (F.obj X) ⊗ᵢ μIso✝ Y Z) ≪≫ μIso✝ X (Y ⊗ Z)).hom
leftUnitor_eq✝ :
  ∀ (X : D), F.map (λ_ X).hom = (((μIso✝ (𝟙_ D) X).symm ≪≫ (εIso✝.symm ⊗ᵢ Iso.refl (F.obj X))) ≪≫ λ_ (F.obj X)).hom
rightUnitor_eq✝ :
  ∀ (X : D), F.map (ρ_ X).hom = (((μIso✝ X (𝟙_ D)).symm ≪≫ (Iso.refl (F.obj X) ⊗ᵢ εIso✝.symm)) ≪≫ ρ_ (F.obj X)).hom
⊢ F.map (𝟙 X₁ ⊗ₘ 𝟙 X₂) = F.map (𝟙 (X₁ ⊗ X₂))

Tactic:
;

Goal state after:
case mk
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategoryStruct D
F : D ⥤ C
inst✝ : F.Faithful
X₁ X₂ : D
μIso✝ : (X Y : D) → F.obj X ⊗ F.obj Y ≅ F.obj (X ⊗ Y)
whiskerLeft_eq✝ :
  ∀ (X : D) {Y₁ Y₂ : D} (f : Y₁ ⟶ Y₂), F.map (X ◁ f) = (μIso✝ X Y₁).inv ≫ F.obj X ◁ F.map f ≫ (μIso✝ X Y₂).hom
whiskerRight_eq✝ :
  ∀ {X₁ X₂ : D} (f : X₁ ⟶ X₂) (Y : D), F.map (f ▷ Y) = (μIso✝ X₁ Y).inv ≫ F.map f ▷ F.obj Y ≫ (μIso✝ X₂ Y).hom
tensorHom_eq✝ :
  ∀ {X₁ Y₁ X₂ Y₂ : D} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂),
    F.map (f ⊗ₘ g) = (μIso✝ X₁ X₂).inv ≫ (F.map f ⊗ₘ F.map g) ≫ (μIso✝ Y₁ Y₂).hom
εIso✝ : 𝟙_ C ≅ F.obj (𝟙_ D)
associator_eq✝ :
  ∀ (X Y Z : D),
    F.map (α_ X Y Z).hom =
      (((μIso✝ (X ⊗ Y) Z).symm ≪≫ ((μIso✝ X Y).symm ⊗ᵢ Iso.refl (F.obj Z))) ≪≫
          α_ (F.obj X) (F.obj Y) (F.obj Z) ≪≫ (Iso.refl (F.obj X) ⊗ᵢ μIso✝ Y Z) ≪≫ μIso✝ X (Y ⊗ Z)).hom
leftUnitor_eq✝ :
  ∀ (X : D), F.map (λ_ X).hom = (((μIso✝ (𝟙_ D) X).symm ≪≫ (εIso✝.symm ⊗ᵢ Iso.refl (F.obj X))) ≪≫ λ_ (F.obj X)).hom
rightUnitor_eq✝ :
  ∀ (X : D), F.map (ρ_ X).hom = (((μIso✝ X (𝟙_ D)).symm ≪≫ (Iso.refl (F.obj X) ⊗ᵢ εIso✝.symm)) ≪≫ ρ_ (F.obj X)).hom
⊢ F.map (𝟙 X₁ ⊗ₘ 𝟙 X₂) = F.map (𝟙 (X₁ ⊗ X₂))
Module: Mathlib.CategoryTheory.Monoidal.Transport

Goal state before:
pp: case mk
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategoryStruct D
F : D ⥤ C
inst✝ : F.Faithful
X₁✝ Y₁✝ Z₁✝ X₂✝ Y₂✝ Z₂✝ : D
f₁ : X₁✝ ⟶ Y₁✝
f₂ : X₂✝ ⟶ Y₂✝
g₁ : Y₁✝ ⟶ Z₁✝
g₂ : Y₂✝ ⟶ Z₂✝
μIso✝ : (X Y : D) → F.obj X ⊗ F.obj Y ≅ F.obj (X ⊗ Y)
whiskerLeft_eq✝ :
  ∀ (X : D) {Y₁ Y₂ : D} (f : Y₁ ⟶ Y₂), F.map (X ◁ f) = (μIso✝ X Y₁).inv ≫ F.obj X ◁ F.map f ≫ (μIso✝ X Y₂).hom
whiskerRight_eq✝ :
  ∀ {X₁ X₂ : D} (f : X₁ ⟶ X₂) (Y : D), F.map (f ▷ Y) = (μIso✝ X₁ Y).inv ≫ F.map f ▷ F.obj Y ≫ (μIso✝ X₂ Y).hom
tensorHom_eq✝ :
  ∀ {X₁ Y₁ X₂ Y₂ : D} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂),
    F.map (f ⊗ₘ g) = (μIso✝ X₁ X₂).inv ≫ (F.map f ⊗ₘ F.map g) ≫ (μIso✝ Y₁ Y₂).hom
εIso✝ : 𝟙_ C ≅ F.obj (𝟙_ D)
associator_eq✝ :
  ∀ (X Y Z : D),
    F.map (α_ X Y Z).hom =
      (((μIso✝ (X ⊗ Y) Z).symm ≪≫ ((μIso✝ X Y).symm ⊗ᵢ Iso.refl (F.obj Z))) ≪≫
          α_ (F.obj X) (F.obj Y) (F.obj Z) ≪≫ (Iso.refl (F.obj X) ⊗ᵢ μIso✝ Y Z) ≪≫ μIso✝ X (Y ⊗ Z)).hom
leftUnitor_eq✝ :
  ∀ (X : D), F.map (λ_ X).hom = (((μIso✝ (𝟙_ D) X).symm ≪≫ (εIso✝.symm ⊗ᵢ Iso.refl (F.obj X))) ≪≫ λ_ (F.obj X)).hom
rightUnitor_eq✝ :
  ∀ (X : D), F.map (ρ_ X).hom = (((μIso✝ X (𝟙_ D)).symm ≪≫ (Iso.refl (F.obj X) ⊗ᵢ εIso✝.symm)) ≪≫ ρ_ (F.obj X)).hom
⊢ F.map ((f₁ ⊗ₘ f₂) ≫ (g₁ ⊗ₘ g₂)) = F.map (f₁ ≫ g₁ ⊗ₘ f₂ ≫ g₂)

Tactic:
;

Goal state after:
case mk
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategoryStruct D
F : D ⥤ C
inst✝ : F.Faithful
X₁✝ Y₁✝ Z₁✝ X₂✝ Y₂✝ Z₂✝ : D
f₁ : X₁✝ ⟶ Y₁✝
f₂ : X₂✝ ⟶ Y₂✝
g₁ : Y₁✝ ⟶ Z₁✝
g₂ : Y₂✝ ⟶ Z₂✝
μIso✝ : (X Y : D) → F.obj X ⊗ F.obj Y ≅ F.obj (X ⊗ Y)
whiskerLeft_eq✝ :
  ∀ (X : D) {Y₁ Y₂ : D} (f : Y₁ ⟶ Y₂), F.map (X ◁ f) = (μIso✝ X Y₁).inv ≫ F.obj X ◁ F.map f ≫ (μIso✝ X Y₂).hom
whiskerRight_eq✝ :
  ∀ {X₁ X₂ : D} (f : X₁ ⟶ X₂) (Y : D), F.map (f ▷ Y) = (μIso✝ X₁ Y).inv ≫ F.map f ▷ F.obj Y ≫ (μIso✝ X₂ Y).hom
tensorHom_eq✝ :
  ∀ {X₁ Y₁ X₂ Y₂ : D} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂),
    F.map (f ⊗ₘ g) = (μIso✝ X₁ X₂).inv ≫ (F.map f ⊗ₘ F.map g) ≫ (μIso✝ Y₁ Y₂).hom
εIso✝ : 𝟙_ C ≅ F.obj (𝟙_ D)
associator_eq✝ :
  ∀ (X Y Z : D),
    F.map (α_ X Y Z).hom =
      (((μIso✝ (X ⊗ Y) Z).symm ≪≫ ((μIso✝ X Y).symm ⊗ᵢ Iso.refl (F.obj Z))) ≪≫
          α_ (F.obj X) (F.obj Y) (F.obj Z) ≪≫ (Iso.refl (F.obj X) ⊗ᵢ μIso✝ Y Z) ≪≫ μIso✝ X (Y ⊗ Z)).hom
leftUnitor_eq✝ :
  ∀ (X : D), F.map (λ_ X).hom = (((μIso✝ (𝟙_ D) X).symm ≪≫ (εIso✝.symm ⊗ᵢ Iso.refl (F.obj X))) ≪≫ λ_ (F.obj X)).hom
rightUnitor_eq✝ :
  ∀ (X : D), F.map (ρ_ X).hom = (((μIso✝ X (𝟙_ D)).symm ≪≫ (Iso.refl (F.obj X) ⊗ᵢ εIso✝.symm)) ≪≫ ρ_ (F.obj X)).hom
⊢ F.map ((f₁ ⊗ₘ f₂) ≫ (g₁ ⊗ₘ g₂)) = F.map (f₁ ≫ g₁ ⊗ₘ f₂ ≫ g₂)
Module: Mathlib.CategoryTheory.Monoidal.Transport

Goal state before:
pp: case mk
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategoryStruct D
F : D ⥤ C
inst✝ : F.Faithful
X Y : D
μIso✝ : (X Y : D) → F.obj X ⊗ F.obj Y ≅ F.obj (X ⊗ Y)
whiskerLeft_eq✝ :
  ∀ (X : D) {Y₁ Y₂ : D} (f : Y₁ ⟶ Y₂), F.map (X ◁ f) = (μIso✝ X Y₁).inv ≫ F.obj X ◁ F.map f ≫ (μIso✝ X Y₂).hom
whiskerRight_eq✝ :
  ∀ {X₁ X₂ : D} (f : X₁ ⟶ X₂) (Y : D), F.map (f ▷ Y) = (μIso✝ X₁ Y).inv ≫ F.map f ▷ F.obj Y ≫ (μIso✝ X₂ Y).hom
tensorHom_eq✝ :
  ∀ {X₁ Y₁ X₂ Y₂ : D} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂),
    F.map (f ⊗ₘ g) = (μIso✝ X₁ X₂).inv ≫ (F.map f ⊗ₘ F.map g) ≫ (μIso✝ Y₁ Y₂).hom
εIso✝ : 𝟙_ C ≅ F.obj (𝟙_ D)
associator_eq✝ :
  ∀ (X Y Z : D),
    F.map (α_ X Y Z).hom =
      (((μIso✝ (X ⊗ Y) Z).symm ≪≫ ((μIso✝ X Y).symm ⊗ᵢ Iso.refl (F.obj Z))) ≪≫
          α_ (F.obj X) (F.obj Y) (F.obj Z) ≪≫ (Iso.refl (F.obj X) ⊗ᵢ μIso✝ Y Z) ≪≫ μIso✝ X (Y ⊗ Z)).hom
leftUnitor_eq✝ :
  ∀ (X : D), F.map (λ_ X).hom = (((μIso✝ (𝟙_ D) X).symm ≪≫ (εIso✝.symm ⊗ᵢ Iso.refl (F.obj X))) ≪≫ λ_ (F.obj X)).hom
rightUnitor_eq✝ :
  ∀ (X : D), F.map (ρ_ X).hom = (((μIso✝ X (𝟙_ D)).symm ≪≫ (Iso.refl (F.obj X) ⊗ᵢ εIso✝.symm)) ≪≫ ρ_ (F.obj X)).hom
⊢ F.map ((α_ X (𝟙_ D) Y).hom ≫ X ◁ (λ_ Y).hom) = F.map ((ρ_ X).hom ▷ Y)

Tactic:
;

Goal state after:
case mk
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategoryStruct D
F : D ⥤ C
inst✝ : F.Faithful
X Y : D
μIso✝ : (X Y : D) → F.obj X ⊗ F.obj Y ≅ F.obj (X ⊗ Y)
whiskerLeft_eq✝ :
  ∀ (X : D) {Y₁ Y₂ : D} (f : Y₁ ⟶ Y₂), F.map (X ◁ f) = (μIso✝ X Y₁).inv ≫ F.obj X ◁ F.map f ≫ (μIso✝ X Y₂).hom
whiskerRight_eq✝ :
  ∀ {X₁ X₂ : D} (f : X₁ ⟶ X₂) (Y : D), F.map (f ▷ Y) = (μIso✝ X₁ Y).inv ≫ F.map f ▷ F.obj Y ≫ (μIso✝ X₂ Y).hom
tensorHom_eq✝ :
  ∀ {X₁ Y₁ X₂ Y₂ : D} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂),
    F.map (f ⊗ₘ g) = (μIso✝ X₁ X₂).inv ≫ (F.map f ⊗ₘ F.map g) ≫ (μIso✝ Y₁ Y₂).hom
εIso✝ : 𝟙_ C ≅ F.obj (𝟙_ D)
associator_eq✝ :
  ∀ (X Y Z : D),
    F.map (α_ X Y Z).hom =
      (((μIso✝ (X ⊗ Y) Z).symm ≪≫ ((μIso✝ X Y).symm ⊗ᵢ Iso.refl (F.obj Z))) ≪≫
          α_ (F.obj X) (F.obj Y) (F.obj Z) ≪≫ (Iso.refl (F.obj X) ⊗ᵢ μIso✝ Y Z) ≪≫ μIso✝ X (Y ⊗ Z)).hom
leftUnitor_eq✝ :
  ∀ (X : D), F.map (λ_ X).hom = (((μIso✝ (𝟙_ D) X).symm ≪≫ (εIso✝.symm ⊗ᵢ Iso.refl (F.obj X))) ≪≫ λ_ (F.obj X)).hom
rightUnitor_eq✝ :
  ∀ (X : D), F.map (ρ_ X).hom = (((μIso✝ X (𝟙_ D)).symm ≪≫ (Iso.refl (F.obj X) ⊗ᵢ εIso✝.symm)) ≪≫ ρ_ (F.obj X)).hom
⊢ F.map ((α_ X (𝟙_ D) Y).hom ≫ X ◁ (λ_ Y).hom) = F.map ((ρ_ X).hom ▷ Y)
Module: Mathlib.CategoryTheory.Monoidal.NaturalTransformation

Goal state before:
pp: C : Type u₁
inst✝¹³ : Category.{v₁, u₁} C
inst✝¹² : MonoidalCategory C
D : Type u₂
inst✝¹¹ : Category.{v₂, u₂} D
inst✝¹⁰ : MonoidalCategory D
E : Type u₃
inst✝⁹ : Category.{v₃, u₃} E
inst✝⁸ : MonoidalCategory E
E' : Type u₄
inst✝⁷ : Category.{v₄, u₄} E'
inst✝⁶ : MonoidalCategory E'
F₁ F₂ F₃ : C ⥤ D
τ : F₁ ⟶ F₂
inst✝⁵ : F₁.LaxMonoidal
inst✝⁴ : F₂.LaxMonoidal
inst✝³ : F₃.LaxMonoidal
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝² : F.Monoidal
inst✝¹ : G.LaxMonoidal
inst✝ : adj.IsMonoidal
X Y : D
⊢ μ (G ⋙ F) X Y ≫ adj.counit.app (X ⊗ Y) = (adj.counit.app X ⊗ₘ adj.counit.app Y) ≫ μ (𝟭 D) X Y

Tactic:
by
    dsimp
    rw [assoc, map_μ_comp_counit_app_tensor, μ_δ_assoc, comp_id]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.NaturalTransformation

Goal state before:
pp: C : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} C
inst✝⁹ : MonoidalCategory C
D : Type u₂
inst✝⁸ : Category.{v₂, u₂} D
inst✝⁷ : MonoidalCategory D
E : Type u₃
inst✝⁶ : Category.{v₃, u₃} E
inst✝⁵ : MonoidalCategory E
E' : Type u₄
inst✝⁴ : Category.{v₄, u₄} E'
inst✝³ : MonoidalCategory E'
F₁ F₂ F₃ : C ⥤ D
τ : F₁ ⟶ F₂
inst✝² : F₁.LaxMonoidal
inst✝¹ : F₂.LaxMonoidal
inst✝ : F₃.LaxMonoidal
X✝ Y✝ Z✝ : LaxMonoidalFunctor C D
α : X✝.Hom Y✝
β : Y✝.Hom Z✝
this : NatTrans.IsMonoidal α.hom
⊢ NatTrans.IsMonoidal (α.hom ≫ β.hom)

Tactic:
;

Goal state after:
C : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} C
inst✝⁹ : MonoidalCategory C
D : Type u₂
inst✝⁸ : Category.{v₂, u₂} D
inst✝⁷ : MonoidalCategory D
E : Type u₃
inst✝⁶ : Category.{v₃, u₃} E
inst✝⁵ : MonoidalCategory E
E' : Type u₄
inst✝⁴ : Category.{v₄, u₄} E'
inst✝³ : MonoidalCategory E'
F₁ F₂ F₃ : C ⥤ D
τ : F₁ ⟶ F₂
inst✝² : F₁.LaxMonoidal
inst✝¹ : F₂.LaxMonoidal
inst✝ : F₃.LaxMonoidal
X✝ Y✝ Z✝ : LaxMonoidalFunctor C D
α : X✝.Hom Y✝
β : Y✝.Hom Z✝
this : NatTrans.IsMonoidal α.hom
⊢ NatTrans.IsMonoidal (α.hom ≫ β.hom)
Module: Mathlib.CategoryTheory.Monoidal.NaturalTransformation

Goal state before:
pp: C : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} C
inst✝⁹ : MonoidalCategory C
D : Type u₂
inst✝⁸ : Category.{v₂, u₂} D
inst✝⁷ : MonoidalCategory D
E : Type u₃
inst✝⁶ : Category.{v₃, u₃} E
inst✝⁵ : MonoidalCategory E
E' : Type u₄
inst✝⁴ : Category.{v₄, u₄} E'
inst✝³ : MonoidalCategory E'
F₁ F₂ F₃ : C ⥤ D
τ : F₁ ⟶ F₂
inst✝² : F₁.LaxMonoidal
inst✝¹ : F₂.LaxMonoidal
inst✝ : F₃.LaxMonoidal
X✝ Y✝ Z✝ : LaxMonoidalFunctor C D
α : X✝.Hom Y✝
β : Y✝.Hom Z✝
this✝ : NatTrans.IsMonoidal α.hom
this : NatTrans.IsMonoidal β.hom
⊢ NatTrans.IsMonoidal (α.hom ≫ β.hom)

Tactic:
;

Goal state after:
C : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} C
inst✝⁹ : MonoidalCategory C
D : Type u₂
inst✝⁸ : Category.{v₂, u₂} D
inst✝⁷ : MonoidalCategory D
E : Type u₃
inst✝⁶ : Category.{v₃, u₃} E
inst✝⁵ : MonoidalCategory E
E' : Type u₄
inst✝⁴ : Category.{v₄, u₄} E'
inst✝³ : MonoidalCategory E'
F₁ F₂ F₃ : C ⥤ D
τ : F₁ ⟶ F₂
inst✝² : F₁.LaxMonoidal
inst✝¹ : F₂.LaxMonoidal
inst✝ : F₃.LaxMonoidal
X✝ Y✝ Z✝ : LaxMonoidalFunctor C D
α : X✝.Hom Y✝
β : Y✝.Hom Z✝
this✝ : NatTrans.IsMonoidal α.hom
this : NatTrans.IsMonoidal β.hom
⊢ NatTrans.IsMonoidal (α.hom ≫ β.hom)
Module: Mathlib.CategoryTheory.Monoidal.NaturalTransformation

Goal state before:
pp: case mk
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : MonoidalCategory D
F G : LaxMonoidalFunctor C D
β : F ⟶ G
hom✝ : F.toFunctor ⟶ G.toFunctor
isMonoidal✝ : NatTrans.IsMonoidal hom✝
h : { hom := hom✝, isMonoidal := isMonoidal✝ }.hom = β.hom
⊢ { hom := hom✝, isMonoidal := isMonoidal✝ } = β

Tactic:
;

Goal state after:
case mk
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : MonoidalCategory D
F G : LaxMonoidalFunctor C D
β : F ⟶ G
hom✝ : F.toFunctor ⟶ G.toFunctor
isMonoidal✝ : NatTrans.IsMonoidal hom✝
h : { hom := hom✝, isMonoidal := isMonoidal✝ }.hom = β.hom
⊢ { hom := hom✝, isMonoidal := isMonoidal✝ } = β
Module: Mathlib.CategoryTheory.Monoidal.NaturalTransformation

Goal state before:
pp: case mk.mk
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : MonoidalCategory D
F G : LaxMonoidalFunctor C D
hom✝¹ : F.toFunctor ⟶ G.toFunctor
isMonoidal✝¹ : NatTrans.IsMonoidal hom✝¹
hom✝ : F.toFunctor ⟶ G.toFunctor
isMonoidal✝ : NatTrans.IsMonoidal hom✝
h : { hom := hom✝¹, isMonoidal := isMonoidal✝¹ }.hom = { hom := hom✝, isMonoidal := isMonoidal✝ }.hom
⊢ { hom := hom✝¹, isMonoidal := isMonoidal✝¹ } = { hom := hom✝, isMonoidal := isMonoidal✝ }

Tactic:
;

Goal state after:
case mk.mk
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : MonoidalCategory D
F G : LaxMonoidalFunctor C D
hom✝¹ : F.toFunctor ⟶ G.toFunctor
isMonoidal✝¹ : NatTrans.IsMonoidal hom✝¹
hom✝ : F.toFunctor ⟶ G.toFunctor
isMonoidal✝ : NatTrans.IsMonoidal hom✝
h : { hom := hom✝¹, isMonoidal := isMonoidal✝¹ }.hom = { hom := hom✝, isMonoidal := isMonoidal✝ }.hom
⊢ { hom := hom✝¹, isMonoidal := isMonoidal✝¹ } = { hom := hom✝, isMonoidal := isMonoidal✝ }
Module: Mathlib.CategoryTheory.Monoidal.NaturalTransformation

Goal state before:
pp: case mk.mk
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : MonoidalCategory D
F G : LaxMonoidalFunctor C D
hom✝ : F.toFunctor ⟶ G.toFunctor
isMonoidal✝¹ : NatTrans.IsMonoidal hom✝
isMonoidal✝ : NatTrans.IsMonoidal { hom := hom✝, isMonoidal := isMonoidal✝¹ }.hom
⊢ { hom := hom✝, isMonoidal := isMonoidal✝¹ } =
    { hom := { hom := hom✝, isMonoidal := isMonoidal✝¹ }.hom, isMonoidal := isMonoidal✝ }

Tactic:
;

Goal state after:
case mk.mk
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : MonoidalCategory D
F G : LaxMonoidalFunctor C D
hom✝ : F.toFunctor ⟶ G.toFunctor
isMonoidal✝¹ : NatTrans.IsMonoidal hom✝
isMonoidal✝ : NatTrans.IsMonoidal { hom := hom✝, isMonoidal := isMonoidal✝¹ }.hom
⊢ { hom := hom✝, isMonoidal := isMonoidal✝¹ } =
    { hom := { hom := hom✝, isMonoidal := isMonoidal✝¹ }.hom, isMonoidal := isMonoidal✝ }
Module: Mathlib.CategoryTheory.Monoidal.Preadditive

Goal state before:
pp: C : Type u_1
inst✝⁹ : Category.{v_1, u_1} C
inst✝⁸ : Preadditive C
inst✝⁷ : MonoidalCategory C
inst✝⁶ : MonoidalPreadditive C
D : Type u_2
inst✝⁵ : Category.{v_2, u_2} D
inst✝⁴ : Preadditive D
inst✝³ : MonoidalCategory D
F : D ⥤ C
inst✝² : F.Monoidal
inst✝¹ : F.Faithful
inst✝ : F.Additive
X✝ Y✝ Z✝ : D
⊢ F.map (0 ▷ X✝) = F.map 0

Tactic:
simp [Functor.Monoidal.map_whiskerRight]

Goal state after: