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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
A : C ⥤ D
inst✝ : MonObj A
X✝ Y✝ Z✝ : C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ { hom := A.map (f ≫ g), isMonHom_hom := ⋯ }.hom =
    ({ hom := A.map f, isMonHom_hom := ⋯ } ≫ { hom := A.map g, isMonHom_hom := ⋯ }).hom

Tactic:
;

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
A : C ⥤ D
inst✝ : MonObj A
X✝ Y✝ Z✝ : C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ { hom := A.map (f ≫ g), isMonHom_hom := ⋯ }.hom =
    ({ hom := A.map f, isMonHom_hom := ⋯ } ≫ { hom := A.map g, isMonHom_hom := ⋯ }).hom
Module: Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
A : C ⥤ D
inst✝ : MonObj A
X✝ Y✝ Z✝ : C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ A.map (f ≫ g) = A.map f ≫ A.map g

Tactic:
;

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
A : C ⥤ D
inst✝ : MonObj A
X✝ Y✝ Z✝ : C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ A.map (f ≫ g) = A.map f ≫ A.map g
Module: Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
A : C ⥤ D
inst✝ : ComonObj A
X✝ Y✝ : C
f : X✝ ⟶ Y✝
⊢ A.map f ≫ ε.app Y✝ = ε.app X✝

Tactic:
;

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
A : C ⥤ D
inst✝ : ComonObj A
X✝ Y✝ : C
f : X✝ ⟶ Y✝
⊢ A.map f ≫ ε.app Y✝ = ε.app X✝
Module: Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
A : C ⥤ D
inst✝ : ComonObj A
X✝ Y✝ : C
f : X✝ ⟶ Y✝
⊢ ε.app X✝ ≫ 𝟙 (𝟙_ D) = ε.app X✝

Tactic:
;

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
A : C ⥤ D
inst✝ : ComonObj A
X✝ Y✝ : C
f : X✝ ⟶ Y✝
⊢ ε.app X✝ ≫ 𝟙 (𝟙_ D) = ε.app X✝
Module: Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
A : C ⥤ D
inst✝ : ComonObj A
X✝ Y✝ : C
f : X✝ ⟶ Y✝
⊢ A.map f ≫ Δ.app Y✝ = Δ.app X✝ ≫ (A.map f ⊗ₘ A.map f)

Tactic:
;

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
A : C ⥤ D
inst✝ : ComonObj A
X✝ Y✝ : C
f : X✝ ⟶ Y✝
⊢ A.map f ≫ Δ.app Y✝ = Δ.app X✝ ≫ (A.map f ⊗ₘ A.map f)
Module: Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
A : C ⥤ D
inst✝ : ComonObj A
X : C
⊢ { hom := A.map (𝟙 X), isComonHom_hom := ⋯ }.hom = (𝟙 (functorObjObj A X)).hom

Tactic:
;

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
A : C ⥤ D
inst✝ : ComonObj A
X : C
⊢ { hom := A.map (𝟙 X), isComonHom_hom := ⋯ }.hom = (𝟙 (functorObjObj A X)).hom
Module: Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
A : C ⥤ D
inst✝ : ComonObj A
X : C
⊢ A.map (𝟙 X) = 𝟙 (A.obj X)

Tactic:
;

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
A : C ⥤ D
inst✝ : ComonObj A
X : C
⊢ A.map (𝟙 X) = 𝟙 (A.obj X)
Module: Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
A : C ⥤ D
inst✝ : ComonObj A
X✝ Y✝ Z✝ : C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ { hom := A.map (f ≫ g), isComonHom_hom := ⋯ }.hom =
    ({ hom := A.map f, isComonHom_hom := ⋯ } ≫ { hom := A.map g, isComonHom_hom := ⋯ }).hom

Tactic:
;

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
A : C ⥤ D
inst✝ : ComonObj A
X✝ Y✝ Z✝ : C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ { hom := A.map (f ≫ g), isComonHom_hom := ⋯ }.hom =
    ({ hom := A.map f, isComonHom_hom := ⋯ } ≫ { hom := A.map g, isComonHom_hom := ⋯ }).hom
Module: Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
A : C ⥤ D
inst✝ : ComonObj A
X✝ Y✝ Z✝ : C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ A.map (f ≫ g) = A.map f ≫ A.map g

Tactic:
;

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
A : C ⥤ D
inst✝ : ComonObj A
X✝ Y✝ Z✝ : C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ A.map (f ≫ g) = A.map f ≫ A.map g
Module: Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : MonoidalCategory D
X✝ Y✝ : C ⥤ Comon D
α : X✝ ⟶ Y✝
x : C
⊢ ({ app := fun X ↦ (α.app X).hom, naturality := ⋯ } ≫ ε).app x = ε.app x

Tactic:
;

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : MonoidalCategory D
X✝ Y✝ : C ⥤ Comon D
α : X✝ ⟶ Y✝
x : C
⊢ ({ app := fun X ↦ (α.app X).hom, naturality := ⋯ } ≫ ε).app x = ε.app x
Module: Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : MonoidalCategory D
X✝ Y✝ : C ⥤ Comon D
α : X✝ ⟶ Y✝
x : C
⊢ (α.app x).hom ≫ ε = ε

Tactic:
;

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : MonoidalCategory D
X✝ Y✝ : C ⥤ Comon D
α : X✝ ⟶ Y✝
x : C
⊢ (α.app x).hom ≫ ε = ε
Module: Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : MonoidalCategory D
X✝ Y✝ : C ⥤ Comon D
α : X✝ ⟶ Y✝
x : C
⊢ ({ app := fun X ↦ (α.app X).hom, naturality := ⋯ } ≫ Δ).app x =
    (Δ ≫ ({ app := fun X ↦ (α.app X).hom, naturality := ⋯ } ⊗ₘ { app := fun X ↦ (α.app X).hom, naturality := ⋯ })).app x

Tactic:
;

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : MonoidalCategory D
X✝ Y✝ : C ⥤ Comon D
α : X✝ ⟶ Y✝
x : C
⊢ ({ app := fun X ↦ (α.app X).hom, naturality := ⋯ } ≫ Δ).app x =
    (Δ ≫ ({ app := fun X ↦ (α.app X).hom, naturality := ⋯ } ⊗ₘ { app := fun X ↦ (α.app X).hom, naturality := ⋯ })).app x
Module: Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : MonoidalCategory D
X✝ Y✝ : C ⥤ Comon D
α : X✝ ⟶ Y✝
x : C
⊢ (α.app x).hom ≫ Δ = Δ ≫ ((α.app x).hom ⊗ₘ (α.app x).hom)

Tactic:
;

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : MonoidalCategory D
X✝ Y✝ : C ⥤ Comon D
α : X✝ ⟶ Y✝
x : C
⊢ (α.app x).hom ≫ Δ = Δ ≫ ((α.app x).hom ⊗ₘ (α.app x).hom)
Module: Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
inst✝ : BraidedCategory D
F : C ⥤ CommMon D
X : C
⊢ ((β_ ((monFunctorCategoryEquivalence C D).inverse.obj (F ⋙ CommMon.forget₂Mon D)).X
              ((monFunctorCategoryEquivalence C D).inverse.obj (F ⋙ CommMon.forget₂Mon D)).X).hom ≫
          μ).app
      X =
    μ.app X

Tactic:
;

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
inst✝ : BraidedCategory D
F : C ⥤ CommMon D
X : C
⊢ ((β_ ((monFunctorCategoryEquivalence C D).inverse.obj (F ⋙ CommMon.forget₂Mon D)).X
              ((monFunctorCategoryEquivalence C D).inverse.obj (F ⋙ CommMon.forget₂Mon D)).X).hom ≫
          μ).app
      X =
    μ.app X
Module: Mathlib.CategoryTheory.Presentable.ColimitPresentation

Goal state before:
pp: case refine_1
C : Type u
inst✝⁷ : Category.{v, u} C
J✝ : Type u_1
I✝ : J✝ → Type u_2
inst✝⁶ : Category.{v_1, u_1} J✝
inst✝⁵ : (j : J✝) → Category.{?u.14, u_2} (I✝ j)
D✝ : J✝ ⥤ C
P✝ : (j : J✝) → ColimitPresentation (I✝ j) (D✝.obj j)
J : Type w
I : J → Type w
inst✝⁴ : SmallCategory J
inst✝³ : (j : J) → SmallCategory (I j)
D : J ⥤ C
P : (j : J) → ColimitPresentation (I j) (D.obj j)
inst✝² : IsFiltered J
inst✝¹ : ∀ (j : J), IsFiltered (I j)
inst✝ : ∀ (j : J) (i : I j), IsFinitelyPresentable ((P j).diag.obj i)
k l : Total P
a : J := IsFiltered.max k.fst l.fst
a' : I (IsFiltered.max k.fst l.fst)
f : Total.mk P k.fst k.snd ⟶ Total.mk P (IsFiltered.max k.fst l.fst) a'
hf : f.base = IsFiltered.leftToMax k.fst l.fst
b' : I (IsFiltered.max k.fst l.fst)
g : Total.mk P l.fst l.snd ⟶ Total.mk P (IsFiltered.max k.fst l.fst) b'
hg : g.base = IsFiltered.rightToMax k.fst l.fst
⊢ k ⟶ ⟨a, IsFiltered.max a' b'⟩

Tactic:
exact f ≫ { base := 𝟙 _, hom := (P _).diag.map (IsFiltered.leftToMax _ _) }

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

Goal state before:
pp: C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
V : Type u₂
inst✝⁵ : Category.{v₂, u₂} V
inst✝⁴ : MonoidalCategory C
inst✝³ : MonoidalCategory V
D : Type u₃
inst✝² : Category.{v₃, u₃} D
inst✝¹ : MonoidalCategoryStruct D
inst✝ : LawfulDayConvolutionMonoidalCategoryStruct C V D
d₁ d₂ d₁' d₂' : D
f : d₁ ⟶ d₂
f' : d₁' ⟶ d₂'
⊢ (ι C V D).map (f ⊗ₘ f') = DayConvolution.map ((ι C V D).map f) ((ι C V D).map f')

Tactic:
apply DayConvolution.corepresentableBy
    (ι C V D |>.obj d₁) (ι C V D |>.obj d₁') |>.homEquiv.injective

Goal state after:
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
V : Type u₂
inst✝⁵ : Category.{v₂, u₂} V
inst✝⁴ : MonoidalCategory C
inst✝³ : MonoidalCategory V
D : Type u₃
inst✝² : Category.{v₃, u₃} D
inst✝¹ : MonoidalCategoryStruct D
inst✝ : LawfulDayConvolutionMonoidalCategoryStruct C V D
d₁ d₂ d₁' d₂' : D
f : d₁ ⟶ d₂
f' : d₁' ⟶ d₂'
⊢ (DayConvolution.corepresentableBy ((ι C V D).obj d₁) ((ι C V D).obj d₁')).homEquiv ((ι C V D).map (f ⊗ₘ f')) =
    (DayConvolution.corepresentableBy ((ι C V D).obj d₁) ((ι C V D).obj d₁')).homEquiv
      (DayConvolution.map ((ι C V D).map f) ((ι C V D).map f'))
Module: Mathlib.CategoryTheory.MorphismProperty.Ind

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : MorphismProperty C
H✝ : P ≤ isFinitelyPresentable C
X Y : C
f : X ⟶ Y
inst✝ : IsFinitelyAccessibleCategory (Under X)
H : ∀ {Z : C} (p : X ⟶ Z) (g : Z ⟶ Y), isFinitelyPresentable C p → p ≫ g = f → ∃ W u v, u ≫ v = g ∧ P (p ≫ u)
Z : Under X
g : Z ⟶ CategoryTheory.Under.mk f
hZ : IsFinitelyPresentable Z
W : C
u : Z.right ⟶ W
v : W ⟶ Y
huv : u ≫ v = Under.Hom.right g
hW : P (Z.hom ≫ u)
⊢ Under.Hom.right (CategoryTheory.Under.homMk u ⋯ ≫ CategoryTheory.Under.homMk v ⋯) = Under.Hom.right g

Tactic:
;

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
P : MorphismProperty C
H✝ : P ≤ isFinitelyPresentable C
X Y : C
f : X ⟶ Y
inst✝ : IsFinitelyAccessibleCategory (Under X)
H : ∀ {Z : C} (p : X ⟶ Z) (g : Z ⟶ Y), isFinitelyPresentable C p → p ≫ g = f → ∃ W u v, u ≫ v = g ∧ P (p ≫ u)
Z : Under X
g : Z ⟶ CategoryTheory.Under.mk f
hZ : IsFinitelyPresentable Z
W : C
u : Z.right ⟶ W
v : W ⟶ Y
huv : u ≫ v = Under.Hom.right g
hW : P (Z.hom ≫ u)
⊢ Under.Hom.right (CategoryTheory.Under.homMk u ⋯ ≫ CategoryTheory.Under.homMk v ⋯) = Under.Hom.right g
Module: Mathlib.CategoryTheory.Monoidal.DayConvolution

Goal state before:
pp: C✝ : Type u₁
inst✝¹³ : Category.{v₁, u₁} C✝
V✝ : Type u₂
inst✝¹² : Category.{v₂, u₂} V✝
inst✝¹¹ : MonoidalCategory C✝
inst✝¹⁰ : MonoidalCategory V✝
C : Type u₁
inst✝⁹ : Category.{v₁, u₁} C
V : Type u₂
inst✝⁸ : Category.{v₂, u₂} V
inst✝⁷ : MonoidalCategory C
inst✝⁶ : MonoidalCategory V
D : Type u₃
inst✝⁵ : Category.{v₃, u₃} D
inst✝⁴ : InducedLawfulDayConvolutionMonoidalCategoryStructCore C V D
inst✝³ : ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorLeft v)
inst✝² : ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorRight v)
inst✝¹ :
  ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (𝟙_ C)) d) (tensorRight v)
inst✝ :
  ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (𝟙_ C)) d) (tensorLeft v)
this : MonoidalCategoryStruct D := mkMonoidalCategoryStruct C V D
x✝¹ : D
x✝ : C
⊢ ((ι C V D).obj x✝¹).obj x✝ ◁ DayConvolutionUnit.can ≫
      (DayConvolution.unit ((ι C V D).obj x✝¹) ((ι C V D).obj (𝟙_ D))).app (x✝, 𝟙_ C) ≫
        ((ι C V D).map (ρ_ x✝¹).hom).app (x✝ ⊗ 𝟙_ C) =
    (ρ_ (((ι C V D).obj x✝¹).obj x✝)).hom ≫ ((ι C V D).obj x✝¹).map (ρ_ x✝).inv

Tactic:
simp only [Functor.comp_obj, tensor_obj, rightUnitor,
        Functor.FullyFaithful.preimageIso_hom, Functor.FullyFaithful.map_preimage]
      apply DayConvolutionUnit.rightUnitor_hom_unit_app

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
P : ObjectProperty C
⊢ P.isoClosure.localEpi = P.localEpi

Tactic:
refine le_antisymm (localEpi_antitone <| le_isoClosure P) ?_
  intro X Y f hf Z ⟨T, hT, ⟨e⟩⟩ u v huv
  rw [← cancel_mono e.hom]
  apply hf hT
  simpa

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
ι : Type u_1
X : ι → C
κ : Cardinal.{w}
h : HasCardinalLT ι κ
i : ι
⊢ ∃ a, (fun i ↦ ⟨X i, ⋯⟩) a = ⟨X i, ⋯⟩

Tactic:
;

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
ι : Type u_1
X : ι → C
κ : Cardinal.{w}
h : HasCardinalLT ι κ
i : ι
⊢ ∃ a, (fun i ↦ ⟨X i, ⋯⟩) a = ⟨X i, ⋯⟩
Module: Mathlib.CategoryTheory.Preadditive.FreydCategory.RightFreyd

Goal state before:
pp: V : Type u_1
inst✝² : Category.{v_1, u_1} V
inst✝¹ : Preadditive V
u v : Arrow V
f g : u ⟶ v
inst✝ : HasZeroObject V
⊢ (rightFunctor V ⋙ quotient V).Additive

Tactic:
;

Goal state after:
V : Type u_1
inst✝² : Category.{v_1, u_1} V
inst✝¹ : Preadditive V
u v : Arrow V
f g : u ⟶ v
inst✝ : HasZeroObject V
⊢ (rightFunctor V ⋙ quotient V).Additive
Module: Mathlib.CategoryTheory.Pi.Monoidal

Goal state before:
pp: I : Type w₁
C : I → Type u₁
inst✝¹ : (i : I) → Category.{v₁, u₁} (C i)
inst✝ : (i : I) → MonoidalCategory (C i)
A B X Y : (i : I) → C i
f : A ⟶ B
g : X ⟶ Y
i : I
⊢ (f ⊗ₘ g) i = (f ▷ X ≫ B ◁ g) i

Tactic:
;

Goal state after:
I : Type w₁
C : I → Type u₁
inst✝¹ : (i : I) → Category.{v₁, u₁} (C i)
inst✝ : (i : I) → MonoidalCategory (C i)
A B X Y : (i : I) → C i
f : A ⟶ B
g : X ⟶ Y
i : I
⊢ (f ⊗ₘ g) i = (f ▷ X ≫ B ◁ g) i
Module: Mathlib.CategoryTheory.Pi.Monoidal

Goal state before:
pp: I : Type w₁
C : I → Type u₁
inst✝² : (i : I) → Category.{v₁, u₁} (C i)
inst✝¹ : (i : I) → MonoidalCategory (C i)
inst✝ : (i : I) → BraidedCategory (C i)
X Y Z : (i : I) → C i
i : I
⊢ ((α_ X Y Z).hom ≫ (isoMk fun i ↦ β_ (X i) ((Y ⊗ Z) i)).hom ≫ (α_ Y Z X).hom) i =
    ((isoMk fun i ↦ β_ (X i) (Y i)).hom ▷ Z ≫ (α_ Y X Z).hom ≫ Y ◁ (isoMk fun i ↦ β_ (X i) (Z i)).hom) i

Tactic:
;

Goal state after:
I : Type w₁
C : I → Type u₁
inst✝² : (i : I) → Category.{v₁, u₁} (C i)
inst✝¹ : (i : I) → MonoidalCategory (C i)
inst✝ : (i : I) → BraidedCategory (C i)
X Y Z : (i : I) → C i
i : I
⊢ ((α_ X Y Z).hom ≫ (isoMk fun i ↦ β_ (X i) ((Y ⊗ Z) i)).hom ≫ (α_ Y Z X).hom) i =
    ((isoMk fun i ↦ β_ (X i) (Y i)).hom ▷ Z ≫ (α_ Y X Z).hom ≫ Y ◁ (isoMk fun i ↦ β_ (X i) (Z i)).hom) i
Module: Mathlib.CategoryTheory.Preadditive.FreydCategory.RightFreyd

Goal state before:
pp: V : Type u_1
inst✝² : Category.{v_1, u_1} V
inst✝¹ : Preadditive V
u✝ v✝ : Arrow V
f✝ g : u✝ ⟶ v✝
inst✝ : HasBinaryBiproducts V
u v : Arrow V
f : u ⟶ v
⊢ IsIso (𝟙 v.right)

Tactic:
;

Goal state after:
V : Type u_1
inst✝² : Category.{v_1, u_1} V
inst✝¹ : Preadditive V
u✝ v✝ : Arrow V
f✝ g : u✝ ⟶ v✝
inst✝ : HasBinaryBiproducts V
u v : Arrow V
f : u ⟶ v
⊢ IsIso (𝟙 v.right)
Module: Mathlib.CategoryTheory.Pi.Monoidal

Goal state before:
pp: I : Type w₁
C : I → Type u₁
inst✝² : (i : I) → Category.{v₁, u₁} (C i)
inst✝¹ : (i : I) → MonoidalCategory (C i)
inst✝ : (i : I) → BraidedCategory (C i)
X Y Z : (i : I) → C i
i : I
⊢ ((α_ X Y Z).inv ≫ (isoMk fun i ↦ β_ ((X ⊗ Y) i) (Z i)).hom ≫ (α_ Z X Y).inv) i =
    (X ◁ (isoMk fun i ↦ β_ (Y i) (Z i)).hom ≫ (α_ X Z Y).inv ≫ (isoMk fun i ↦ β_ (X i) (Z i)).hom ▷ Y) i

Tactic:
;

Goal state after:
I : Type w₁
C : I → Type u₁
inst✝² : (i : I) → Category.{v₁, u₁} (C i)
inst✝¹ : (i : I) → MonoidalCategory (C i)
inst✝ : (i : I) → BraidedCategory (C i)
X Y Z : (i : I) → C i
i : I
⊢ ((α_ X Y Z).inv ≫ (isoMk fun i ↦ β_ ((X ⊗ Y) i) (Z i)).hom ≫ (α_ Z X Y).inv) i =
    (X ◁ (isoMk fun i ↦ β_ (Y i) (Z i)).hom ≫ (α_ X Z Y).inv ≫ (isoMk fun i ↦ β_ (X i) (Z i)).hom ▷ Y) i
Module: Mathlib.CategoryTheory.Pi.Monoidal

Goal state before:
pp: I : Type w₁
C : I → Type u₁
inst✝² : (i : I) → Category.{v₁, u₁} (C i)
inst✝¹ : (i : I) → MonoidalCategory (C i)
inst✝ : (i : I) → SymmetricCategory (C i)
X Y : (i : I) → C i
i : I
⊢ ((β_ X Y).hom ≫ (β_ Y X).hom) i = 𝟙 (X ⊗ Y) i

Tactic:
;

Goal state after:
I : Type w₁
C : I → Type u₁
inst✝² : (i : I) → Category.{v₁, u₁} (C i)
inst✝¹ : (i : I) → MonoidalCategory (C i)
inst✝ : (i : I) → SymmetricCategory (C i)
X Y : (i : I) → C i
i : I
⊢ ((β_ X Y).hom ≫ (β_ Y X).hom) i = 𝟙 (X ⊗ Y) i
Module: Mathlib.CategoryTheory.Pi.Monoidal

Goal state before:
pp: I : Type w₁
C : I → Type u₁
inst✝⁴ : (i : I) → Category.{v₁, u₁} (C i)
inst✝³ : (i : I) → MonoidalCategory (C i)
D : Type u_1
inst✝² : Category.{v_1, u_1} D
inst✝¹ : MonoidalCategory D
F : (i : I) → D ⥤ C i
inst✝ : (i : I) → (F i).OplaxMonoidal
X : D
i✝ : I
⊢ (λ_ ((Functor.pi' F).obj X)).inv i✝ =
    ((Functor.pi' F).map (λ_ X).inv ≫
        (fun i ↦ Functor.OplaxMonoidal.δ (F i) (𝟙_ D) X) ≫
          (fun i ↦ Functor.OplaxMonoidal.η (F i)) ▷ (Functor.pi' F).obj X)
      i✝

Tactic:
;

Goal state after:
I : Type w₁
C : I → Type u₁
inst✝⁴ : (i : I) → Category.{v₁, u₁} (C i)
inst✝³ : (i : I) → MonoidalCategory (C i)
D : Type u_1
inst✝² : Category.{v_1, u_1} D
inst✝¹ : MonoidalCategory D
F : (i : I) → D ⥤ C i
inst✝ : (i : I) → (F i).OplaxMonoidal
X : D
i✝ : I
⊢ (λ_ ((Functor.pi' F).obj X)).inv i✝ =
    ((Functor.pi' F).map (λ_ X).inv ≫
        (fun i ↦ Functor.OplaxMonoidal.δ (F i) (𝟙_ D) X) ≫
          (fun i ↦ Functor.OplaxMonoidal.η (F i)) ▷ (Functor.pi' F).obj X)
      i✝
Module: Mathlib.CategoryTheory.Pi.Monoidal

Goal state before:
pp: I : Type w₁
C : I → Type u₁
inst✝⁴ : (i : I) → Category.{v₁, u₁} (C i)
inst✝³ : (i : I) → MonoidalCategory (C i)
D : Type u_1
inst✝² : Category.{v_1, u_1} D
inst✝¹ : MonoidalCategory D
F : (i : I) → D ⥤ C i
inst✝ : (i : I) → (F i).OplaxMonoidal
X : D
i✝ : I
⊢ (ρ_ ((Functor.pi' F).obj X)).inv i✝ =
    ((Functor.pi' F).map (ρ_ X).inv ≫
        (fun i ↦ Functor.OplaxMonoidal.δ (F i) X (𝟙_ D)) ≫
          (Functor.pi' F).obj X ◁ fun i ↦ Functor.OplaxMonoidal.η (F i))
      i✝

Tactic:
;

Goal state after:
I : Type w₁
C : I → Type u₁
inst✝⁴ : (i : I) → Category.{v₁, u₁} (C i)
inst✝³ : (i : I) → MonoidalCategory (C i)
D : Type u_1
inst✝² : Category.{v_1, u_1} D
inst✝¹ : MonoidalCategory D
F : (i : I) → D ⥤ C i
inst✝ : (i : I) → (F i).OplaxMonoidal
X : D
i✝ : I
⊢ (ρ_ ((Functor.pi' F).obj X)).inv i✝ =
    ((Functor.pi' F).map (ρ_ X).inv ≫
        (fun i ↦ Functor.OplaxMonoidal.δ (F i) X (𝟙_ D)) ≫
          (Functor.pi' F).obj X ◁ fun i ↦ Functor.OplaxMonoidal.η (F i))
      i✝
Module: Mathlib.CategoryTheory.Pi.Monoidal

Goal state before:
pp: I : Type w₁
C : I → Type u₁
inst✝⁶ : (i : I) → Category.{v₁, u₁} (C i)
inst✝⁵ : (i : I) → MonoidalCategory (C i)
inst✝⁴ : (i : I) → BraidedCategory (C i)
D : Type u_1
inst✝³ : Category.{v_1, u_1} D
inst✝² : MonoidalCategory D
inst✝¹ : BraidedCategory D
F : (i : I) → D ⥤ C i
inst✝ : (i : I) → (F i).LaxBraided
X✝ Y✝ : D
⊢ Functor.LaxMonoidal.μ (Functor.pi' F) X✝ Y✝ ≫ (Functor.pi' F).map (β_ X✝ Y✝).hom =
    (β_ ((Functor.pi' F).obj X✝) ((Functor.pi' F).obj Y✝)).hom ≫ Functor.LaxMonoidal.μ (Functor.pi' F) Y✝ X✝

Tactic:
;

Goal state after:
I : Type w₁
C : I → Type u₁
inst✝⁶ : (i : I) → Category.{v₁, u₁} (C i)
inst✝⁵ : (i : I) → MonoidalCategory (C i)
inst✝⁴ : (i : I) → BraidedCategory (C i)
D : Type u_1
inst✝³ : Category.{v_1, u_1} D
inst✝² : MonoidalCategory D
inst✝¹ : BraidedCategory D
F : (i : I) → D ⥤ C i
inst✝ : (i : I) → (F i).LaxBraided
X✝ Y✝ : D
⊢ Functor.LaxMonoidal.μ (Functor.pi' F) X✝ Y✝ ≫ (Functor.pi' F).map (β_ X✝ Y✝).hom =
    (β_ ((Functor.pi' F).obj X✝) ((Functor.pi' F).obj Y✝)).hom ≫ Functor.LaxMonoidal.μ (Functor.pi' F) Y✝ X✝
Module: Mathlib.CategoryTheory.Pi.Monoidal

Goal state before:
pp: I : Type w₁
C : I → Type u₁
inst✝⁶ : (i : I) → Category.{v₁, u₁} (C i)
inst✝⁵ : (i : I) → MonoidalCategory (C i)
inst✝⁴ : (i : I) → BraidedCategory (C i)
D : Type u_1
inst✝³ : Category.{v_1, u_1} D
inst✝² : MonoidalCategory D
inst✝¹ : BraidedCategory D
F : (i : I) → D ⥤ C i
inst✝ : (i : I) → (F i).LaxBraided
X✝ Y✝ : D
i : I
⊢ (Functor.LaxMonoidal.μ (Functor.pi' F) X✝ Y✝ ≫ (Functor.pi' F).map (β_ X✝ Y✝).hom) i =
    ((β_ ((Functor.pi' F).obj X✝) ((Functor.pi' F).obj Y✝)).hom ≫ Functor.LaxMonoidal.μ (Functor.pi' F) Y✝ X✝) i

Tactic:
;

Goal state after:
I : Type w₁
C : I → Type u₁
inst✝⁶ : (i : I) → Category.{v₁, u₁} (C i)
inst✝⁵ : (i : I) → MonoidalCategory (C i)
inst✝⁴ : (i : I) → BraidedCategory (C i)
D : Type u_1
inst✝³ : Category.{v_1, u_1} D
inst✝² : MonoidalCategory D
inst✝¹ : BraidedCategory D
F : (i : I) → D ⥤ C i
inst✝ : (i : I) → (F i).LaxBraided
X✝ Y✝ : D
i : I
⊢ (Functor.LaxMonoidal.μ (Functor.pi' F) X✝ Y✝ ≫ (Functor.pi' F).map (β_ X✝ Y✝).hom) i =
    ((β_ ((Functor.pi' F).obj X✝) ((Functor.pi' F).obj Y✝)).hom ≫ Functor.LaxMonoidal.μ (Functor.pi' F) Y✝ X✝) i
Module: Mathlib.CategoryTheory.Pi.Monoidal

Goal state before:
pp: I : Type w₁
C : I → Type u₁
inst✝⁴ : (i : I) → Category.{v₁, u₁} (C i)
inst✝³ : (i : I) → MonoidalCategory (C i)
D : I → Type u₂
inst✝² : (i : I) → Category.{v₂, u₂} (D i)
inst✝¹ : (i : I) → MonoidalCategory (D i)
F : (i : I) → D i ⥤ C i
inst✝ : (i : I) → (F i).OplaxMonoidal
X : (i : I) → D i
i✝ : I
⊢ (λ_ ((Functor.pi F).obj X)).inv i✝ =
    ((Functor.pi F).map (λ_ X).inv ≫
        (fun i ↦ Functor.OplaxMonoidal.δ (F i) ((𝟙_ ((i : I) → D i)) i) (X i)) ≫
          (fun i ↦ Functor.OplaxMonoidal.η (F i)) ▷ (Functor.pi F).obj X)
      i✝

Tactic:
;

Goal state after:
I : Type w₁
C : I → Type u₁
inst✝⁴ : (i : I) → Category.{v₁, u₁} (C i)
inst✝³ : (i : I) → MonoidalCategory (C i)
D : I → Type u₂
inst✝² : (i : I) → Category.{v₂, u₂} (D i)
inst✝¹ : (i : I) → MonoidalCategory (D i)
F : (i : I) → D i ⥤ C i
inst✝ : (i : I) → (F i).OplaxMonoidal
X : (i : I) → D i
i✝ : I
⊢ (λ_ ((Functor.pi F).obj X)).inv i✝ =
    ((Functor.pi F).map (λ_ X).inv ≫
        (fun i ↦ Functor.OplaxMonoidal.δ (F i) ((𝟙_ ((i : I) → D i)) i) (X i)) ≫
          (fun i ↦ Functor.OplaxMonoidal.η (F i)) ▷ (Functor.pi F).obj X)
      i✝