Module: Mathlib.CategoryTheory.Monoidal.NaturalTransformation

Goal state before:
pp: case unit
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 G : LaxMonoidalFunctor C D
e : (X : C) → F.obj X ≅ G.obj X
naturality : ∀ {X Y : C} (f : X ⟶ Y), F.map f ≫ (e Y).hom = (e X).hom ≫ G.map f
unit : ε F.toFunctor ≫ (e (𝟙_ C)).hom = ε G.toFunctor
tensor : ∀ (X Y : C), μ F.toFunctor X Y ≫ (e (X ⊗ Y)).hom = ((e X).hom ⊗ₘ (e Y).hom) ≫ μ G.toFunctor X Y
⊢ autoParam (ε F.toFunctor ≫ (NatIso.ofComponents e ⋯).hom.app (𝟙_ C) = ε G.toFunctor)
    NatTrans.IsMonoidal.unit._autoParam

pp: case tensor
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 G : LaxMonoidalFunctor C D
e : (X : C) → F.obj X ≅ G.obj X
naturality : ∀ {X Y : C} (f : X ⟶ Y), F.map f ≫ (e Y).hom = (e X).hom ≫ G.map f
unit : ε F.toFunctor ≫ (e (𝟙_ C)).hom = ε G.toFunctor
tensor : ∀ (X Y : C), μ F.toFunctor X Y ≫ (e (X ⊗ Y)).hom = ((e X).hom ⊗ₘ (e Y).hom) ≫ μ G.toFunctor X Y
⊢ autoParam
    (∀ (X Y : C),
      μ F.toFunctor X Y ≫ (NatIso.ofComponents e ⋯).hom.app (X ⊗ Y) =
        ((NatIso.ofComponents e ⋯).hom.app X ⊗ₘ (NatIso.ofComponents e ⋯).hom.app Y) ≫ μ G.toFunctor X Y)
    NatTrans.IsMonoidal.tensor._autoParam

Tactic:
<;>

Goal state after:
case unit
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 G : LaxMonoidalFunctor C D
e : (X : C) → F.obj X ≅ G.obj X
naturality : ∀ {X Y : C} (f : X ⟶ Y), F.map f ≫ (e Y).hom = (e X).hom ≫ G.map f
unit : ε F.toFunctor ≫ (e (𝟙_ C)).hom = ε G.toFunctor
tensor : ∀ (X Y : C), μ F.toFunctor X Y ≫ (e (X ⊗ Y)).hom = ((e X).hom ⊗ₘ (e Y).hom) ≫ μ G.toFunctor X Y
⊢ autoParam (ε F.toFunctor ≫ (NatIso.ofComponents e ⋯).hom.app (𝟙_ C) = ε G.toFunctor)
    NatTrans.IsMonoidal.unit._autoParam

case tensor
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 G : LaxMonoidalFunctor C D
e : (X : C) → F.obj X ≅ G.obj X
naturality : ∀ {X Y : C} (f : X ⟶ Y), F.map f ≫ (e Y).hom = (e X).hom ≫ G.map f
unit : ε F.toFunctor ≫ (e (𝟙_ C)).hom = ε G.toFunctor
tensor : ∀ (X Y : C), μ F.toFunctor X Y ≫ (e (X ⊗ Y)).hom = ((e X).hom ⊗ₘ (e Y).hom) ≫ μ G.toFunctor X Y
⊢ autoParam
    (∀ (X Y : C),
      μ F.toFunctor X Y ≫ (NatIso.ofComponents e ⋯).hom.app (X ⊗ Y) =
        ((NatIso.ofComponents e ⋯).hom.app X ⊗ₘ (NatIso.ofComponents e ⋯).hom.app Y) ≫ μ G.toFunctor X Y)
    NatTrans.IsMonoidal.tensor._autoParam