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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
f g h i j : C
α : g ≅ h
η : h ⟶ i
ηs : i ⟶ j
θ : f ⊗ i ⟶ f ⊗ j
e_θ : f ◁ ηs = θ
⊢ f ◁ (α.hom ≫ η ≫ ηs) = (f ◁ᵢ α).hom ≫ f ◁ η ≫ θ

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.CategoryTheory.Monoidal.Normalize

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
f g h i : C
η : h ⟶ i
η₁ : g ⊗ h ⟶ g ⊗ i
η₂ : f ⊗ g ⊗ h ⟶ f ⊗ g ⊗ i
η₃ : f ⊗ g ⊗ h ⟶ (f ⊗ g) ⊗ i
η₄ : (f ⊗ g) ⊗ h ⟶ (f ⊗ g) ⊗ i
e_η₁ : g ◁ η = η₁
e_η₂ : f ◁ η₁ = η₂
e_η₃ : η₂ ≫ (α_ f g i).inv = η₃
e_η₄ : (α_ f g h).hom ≫ η₃ = η₄
⊢ (f ⊗ g) ◁ η = η₄

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.CategoryTheory.Monoidal.Normalize

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
f g : C
η : f ⟶ g
η₁ : f ⟶ 𝟙_ C ⊗ g
η₂ : 𝟙_ C ⊗ f ⟶ 𝟙_ C ⊗ g
e_η₁ : η ≫ (λ_ g).inv = η₁
e_η₂ : (λ_ f).hom ≫ η₁ = η₂
⊢ 𝟙_ C ◁ η = η₂

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.CategoryTheory.Monoidal.Normalize

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
f g h : C
η η' : g ⟶ h
θ : f ⊗ g ⟶ f ⊗ h
e_η : η = η'
e_θ : f ◁ η' = θ
⊢ f ◁ η = θ

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.CategoryTheory.Monoidal.Normalize

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
f g h : C
η η' : f ⟶ g
θ : f ⊗ h ⟶ g ⊗ h
e_η : η = η'
e_θ : η' ▷ h = θ
⊢ η ▷ h = θ

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.CategoryTheory.Monoidal.Normalize

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
f g h i : C
η η' : f ⟶ g
θ θ' : h ⟶ i
ι : f ⊗ h ⟶ g ⊗ i
e_η : η = η'
e_θ : θ = θ'
e_ι : η' ⊗ₘ θ' = ι
⊢ η ⊗ₘ θ = ι

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.CategoryTheory.Monoidal.Normalize

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
f g : C
α : f ≅ g
h : C
⊢ (α ▷ᵢ h).hom = (α ▷ᵢ h).hom

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.CategoryTheory.Monoidal.Normalize

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
f g h i j : C
α : f ≅ g
η : g ⟶ h
ηs : h ⟶ i
ηs₁ : h ⊗ j ⟶ i ⊗ j
η₁ : g ⊗ j ⟶ h ⊗ j
η₂ : g ⊗ j ⟶ i ⊗ j
η₃ : f ⊗ j ⟶ i ⊗ j
e_ηs₁ : ηs ▷ j = ηs₁
e_η₁ : η ▷ j = η₁
e_η₂ : η₁ ≫ ηs₁ = η₂
e_η₃ : (α ▷ᵢ j).hom ≫ η₂ = η₃
⊢ (α.hom ≫ η ≫ ηs) ▷ j = η₃

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.CategoryTheory.Monoidal.Normalize

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
f g h i j k : C
α : g ≅ f ⊗ h
η : h ⟶ i
ηs : f ⊗ i ⟶ j
η₁ : h ⊗ k ⟶ i ⊗ k
η₂ : f ⊗ h ⊗ k ⟶ f ⊗ i ⊗ k
ηs₁ : (f ⊗ i) ⊗ k ⟶ j ⊗ k
ηs₂ : f ⊗ i ⊗ k ⟶ j ⊗ k
η₃ : f ⊗ h ⊗ k ⟶ j ⊗ k
η₄ : (f ⊗ h) ⊗ k ⟶ j ⊗ k
η₅ : g ⊗ k ⟶ j ⊗ k
e_η₁ : ((Iso.refl h).hom ≫ η ≫ (Iso.refl i).hom) ▷ k = η₁
e_η₂ : f ◁ η₁ = η₂
e_ηs₁ : ηs ▷ k = ηs₁
e_ηs₂ : (α_ f i k).inv ≫ ηs₁ = ηs₂
e_η₃ : η₂ ≫ ηs₂ = η₃
e_η₄ : (α_ f h k).hom ≫ η₃ = η₄
e_η₅ : (α ▷ᵢ k).hom ≫ η₄ = η₅
⊢ (α.hom ≫ f ◁ η ≫ ηs) ▷ k = η₅

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.CategoryTheory.Monoidal.Normalize

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
f f' g h : C
η : f ⟶ f'
η₁ : f ⊗ g ⟶ f' ⊗ g
η₂ : (f ⊗ g) ⊗ h ⟶ (f' ⊗ g) ⊗ h
η₃ : (f ⊗ g) ⊗ h ⟶ f' ⊗ g ⊗ h
η₄ : f ⊗ g ⊗ h ⟶ f' ⊗ g ⊗ h
e_η₁ : η ▷ g = η₁
e_η₂ : η₁ ▷ h = η₂
e_η₃ : η₂ ≫ (α_ f' g h).hom = η₃
e_η₄ : (α_ f g h).inv ≫ η₃ = η₄
⊢ η ▷ (g ⊗ h) = η₄

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.CategoryTheory.Monoidal.Normalize

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
f g : C
η : f ⟶ g
η₁ : f ⟶ g ⊗ 𝟙_ C
η₂ : f ⊗ 𝟙_ C ⟶ g ⊗ 𝟙_ C
e_η₁ : η ≫ (ρ_ g).inv = η₁
e_η₂ : (ρ_ f).hom ≫ η₁ = η₂
⊢ η ▷ 𝟙_ C = η₂

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.CategoryTheory.Monoidal.Normalize

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
f g : C
η : f ⟶ g
h : C
⊢ η ▷ h = (Iso.refl (f ⊗ h)).hom ≫ η ▷ h ≫ (Iso.refl (g ⊗ h)).hom

Tactic:
by

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

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
C' : Type u₁'
inst✝ : Category.{v₁', u₁'} C'
F : C ⥤ D
εIso : 𝟙_ D ≅ F.obj (𝟙_ C)
μIso : (X Y : C) → F.obj X ⊗ F.obj Y ≅ F.obj (X ⊗ Y)
μIso_inv_natural_left :
  ∀ {X Y : C} (f : X ⟶ Y) (X' : C), (μIso X X').inv ≫ F.map f ▷ F.obj X' = F.map (f ▷ X') ≫ (μIso Y X').inv
μIso_inv_natural_right :
  ∀ {X Y : C} (X' : C) (f : X ⟶ Y), (μIso X' X).inv ≫ F.obj X' ◁ F.map f = F.map (X' ◁ f) ≫ (μIso X' Y).inv
oplax_associativity :
  ∀ (X Y Z : C),
    (μIso (X ⊗ Y) Z).inv ≫ (μIso X Y).inv ▷ F.obj Z ≫ (α_ (F.obj X) (F.obj Y) (F.obj Z)).hom =
      F.map (α_ X Y Z).hom ≫ (μIso X (Y ⊗ Z)).inv ≫ F.obj X ◁ (μIso Y Z).inv
oplax_left_unitality : ∀ (X : C), (λ_ (F.obj X)).inv = F.map (λ_ X).inv ≫ (μIso (𝟙_ C) X).inv ≫ εIso.inv ▷ F.obj X
oplax_right_unitality : ∀ (X : C), (ρ_ (F.obj X)).inv = F.map (ρ_ X).inv ≫ (μIso X (𝟙_ C)).inv ≫ F.obj X ◁ εIso.inv
X : C
⊢ (ρ_ (F.obj X)).hom = F.obj X ◁ εIso.hom ≫ (μIso X (𝟙_ C)).hom ≫ F.map (ρ_ X).hom

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.CategoryTheory.Monoidal.Normalize

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
f g h i j : C
η : g ⟶ h
ηs : i ⟶ j
ηs' : i ⊗ f ⟶ j ⊗ f
η₁ : g ⊗ i ⊗ f ⟶ h ⊗ j ⊗ f
η₂ : g ⊗ i ⊗ f ⟶ (h ⊗ j) ⊗ f
η₃ : (g ⊗ i) ⊗ f ⟶ (h ⊗ j) ⊗ f
e_ηs' : ηs ▷ f = ηs'
e_η₁ : (Iso.refl g).hom ≫ η ≫ (Iso.refl h).hom ⊗ₘ ηs' = η₁
e_η₂ : η₁ ≫ (α_ h j f).inv = η₂
e_η₃ : (α_ g i f).hom ≫ η₂ = η₃
⊢ (η ⊗ₘ ηs) ▷ f = η₃

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.CategoryTheory.Monoidal.Normalize

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
f f' g h i : C
α : f' ≅ g
η : g ⟶ h
ηs : h ⟶ i
ηs₁ : h ⊗ f ⟶ i ⊗ f
η₁ : g ⊗ f ⟶ h ⊗ f
η₂ : g ⊗ f ⟶ i ⊗ f
η₃ : f' ⊗ f ⟶ i ⊗ f
e_ηs₁ : ηs ▷ f = ηs₁
e_η₁ : η ▷ f = η₁
e_η₂ : η₁ ≫ ηs₁ = η₂
e_η₃ : (α ▷ᵢ f).hom ≫ η₂ = η₃
⊢ (α.hom ≫ η ≫ ηs) ▷ f = η₃

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.CategoryTheory.Monoidal.Normalize

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
f g h i : C
η : f ⟶ g
θ : h ⟶ i
⊢ η ⊗ₘ θ = (Iso.refl (f ⊗ h)).hom ≫ (η ⊗ₘ θ) ≫ (Iso.refl (g ⊗ i)).hom

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.CategoryTheory.Monoidal.Normalize

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
f f' g g' h i : C
η : f ⟶ g
ηs : f' ⟶ g'
θ : h ⟶ i
ηθ : f' ⊗ h ⟶ g' ⊗ i
η₁ : f ⊗ f' ⊗ h ⟶ g ⊗ g' ⊗ i
ηθ₁ : f ⊗ f' ⊗ h ⟶ (g ⊗ g') ⊗ i
ηθ₂ : (f ⊗ f') ⊗ h ⟶ (g ⊗ g') ⊗ i
e_ηθ : ηs ⊗ₘ θ = ηθ
e_η₁ : (Iso.refl f).hom ≫ η ≫ (Iso.refl g).hom ⊗ₘ ηθ = η₁
e_ηθ₁ : η₁ ≫ (α_ g g' i).inv = ηθ₁
e_ηθ₂ : (α_ f f' h).hom ≫ ηθ₁ = ηθ₂
⊢ (η ⊗ₘ ηs) ⊗ₘ θ = ηθ₂

Tactic:
by

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

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
C' : Type u₁'
inst✝ : Category.{v₁', u₁'} C'
F : C ⥤ D
h : F.CoreMonoidal
X✝ Y✝ : C
x✝¹ : X✝ ⟶ Y✝
x✝ : C
⊢ (h.μIso X✝ x✝).inv ≫ F.map x✝¹ ▷ F.obj x✝ = F.map (x✝¹ ▷ x✝) ≫ (h.μIso Y✝ x✝).inv

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.CategoryTheory.Monoidal.Normalize

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
f f' g g' h : C
η : g ⟶ h
θ : f' ⟶ g'
ηθ : g ⊗ f' ⟶ h ⊗ g'
η₁ : f ⊗ g ⊗ f' ⟶ f ⊗ h ⊗ g'
η₂ : f ⊗ g ⊗ f' ⟶ (f ⊗ h) ⊗ g'
η₃ : (f ⊗ g) ⊗ f' ⟶ (f ⊗ h) ⊗ g'
e_ηθ : η ⊗ₘ θ = ηθ
e_η₁ : f ◁ ηθ = η₁
e_η₂ : η₁ ≫ (α_ f h g').inv = η₂
e_η₃ : (α_ f g f').hom ≫ η₂ = η₃
⊢ f ◁ η ⊗ₘ θ = η₃

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.CategoryTheory.Monoidal.Normalize

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
f f' g g' h : C
η : g ⟶ h
θ : f' ⟶ g'
η₁ : g ⊗ f ⟶ h ⊗ f
ηθ : (g ⊗ f) ⊗ f' ⟶ (h ⊗ f) ⊗ g'
ηθ₁ : (g ⊗ f) ⊗ f' ⟶ h ⊗ f ⊗ g'
ηθ₂ : g ⊗ f ⊗ f' ⟶ h ⊗ f ⊗ g'
e_η₁ : η ▷ f = η₁
e_ηθ : η₁ ⊗ₘ (Iso.refl f').hom ≫ θ ≫ (Iso.refl g').hom = ηθ
e_ηθ₁ : ηθ ≫ (α_ h f g').hom = ηθ₁
e_ηθ₂ : (α_ g f f').inv ≫ ηθ₁ = ηθ₂
⊢ η ⊗ₘ f ◁ θ = ηθ₂

Tactic:
by

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

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
C' : Type u₁'
inst✝ : Category.{v₁', u₁'} C'
F : C ⥤ D
h : F.CoreMonoidal
X✝ Y✝ x✝¹ : C
x✝ : X✝ ⟶ Y✝
⊢ (h.μIso x✝¹ X✝).inv ≫ F.obj x✝¹ ◁ F.map x✝ = F.map (x✝¹ ◁ x✝) ≫ (h.μIso x✝¹ Y✝).inv

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.CategoryTheory.Monoidal.Normalize

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
f g h i : C
α : f ≅ g
β : h ≅ i
⊢ (α ⊗ᵢ β).hom = (α ⊗ᵢ β).hom

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.CategoryTheory.Monoidal.Normalize

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
f f' g g' h i : C
α : f ≅ g
β : f' ≅ g'
η : g' ⟶ h
ηs : h ⟶ i
η₁ : g ⊗ g' ⟶ g ⊗ h
ηs₁ : g ⊗ h ⟶ g ⊗ i
η₂ : g ⊗ g' ⟶ g ⊗ i
η₃ : f ⊗ f' ⟶ g ⊗ i
e_η₁ : g ◁ ((Iso.refl g').hom ≫ η ≫ (Iso.refl h).hom) = η₁
e_ηs₁ : g ◁ ηs = ηs₁
e_η₂ : η₁ ≫ ηs₁ = η₂
e_η₃ : (α ⊗ᵢ β).hom ≫ η₂ = η₃
⊢ α.hom ⊗ₘ β.hom ≫ η ≫ ηs = η₃

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.CategoryTheory.Monoidal.Normalize

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
f f' g g' h i : C
α : f ≅ g
η : g ⟶ h
ηs : h ⟶ i
β : f' ≅ g'
η₁ : g ⊗ g' ⟶ h ⊗ g'
ηs₁ : h ⊗ g' ⟶ i ⊗ g'
η₂ : g ⊗ g' ⟶ i ⊗ g'
η₃ : f ⊗ f' ⟶ i ⊗ g'
e_η₁ : ((Iso.refl g).hom ≫ η ≫ (Iso.refl h).hom) ▷ g' = η₁
e_ηs₁ : ηs ▷ g' = ηs₁
e_η₂ : η₁ ≫ ηs₁ = η₂
e_η₃ : (α ⊗ᵢ β).hom ≫ η₂ = η₃
⊢ α.hom ≫ η ≫ ηs ⊗ₘ β.hom = η₃

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.CategoryTheory.Monoidal.Normalize

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
f f' g g' h h' i i' : C
α : f ≅ g
η : g ⟶ h
ηs : h ⟶ i
β : f' ≅ g'
θ : g' ⟶ h'
θs : h' ⟶ i'
ηθ : g ⊗ g' ⟶ h ⊗ h'
ηθs : h ⊗ h' ⟶ i ⊗ i'
ηθ₁ : g ⊗ g' ⟶ i ⊗ i'
ηθ₂ : f ⊗ f' ⟶ i ⊗ i'
e_ηθ : η ⊗ₘ θ = ηθ
e_ηθs : ηs ⊗ₘ θs = ηθs
e_ηθ₁ : ηθ ≫ ηθs = ηθ₁
e_ηθ₂ : (α ⊗ᵢ β).hom ≫ ηθ₁ = ηθ₂
⊢ α.hom ≫ η ≫ ηs ⊗ₘ β.hom ≫ θ ≫ θs = ηθ₂

Tactic:
by

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

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
C' : Type u₁'
inst✝ : Category.{v₁', u₁'} C'
F : C ⥤ D
h : F.CoreMonoidal
X Y Z : C
⊢ (h.μIso (X ⊗ Y) Z).inv ≫ (h.μIso X Y).inv ▷ F.obj Z ≫ (α_ (F.obj X) (F.obj Y) (F.obj Z)).hom =
    F.map (α_ X Y Z).hom ≫ (h.μIso X (Y ⊗ Z)).inv ≫ F.obj X ◁ (h.μIso Y Z).inv

Tactic:
by

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

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
C' : Type u₁'
inst✝ : Category.{v₁', u₁'} C'
F : C ⥤ D
h : F.CoreMonoidal
x✝ : C
⊢ (λ_ (F.obj x✝)).inv = F.map (λ_ x✝).inv ≫ (h.μIso (𝟙_ C) x✝).inv ≫ h.εIso.inv ▷ F.obj x✝

Tactic:
by

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

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
C' : Type u₁'
inst✝ : Category.{v₁', u₁'} C'
F : C ⥤ D
h : F.CoreMonoidal
x✝ : C
⊢ (ρ_ (F.obj x✝)).inv = F.map (ρ_ x✝).inv ≫ (h.μIso x✝ (𝟙_ C)).inv ≫ F.obj x✝ ◁ h.εIso.inv

Tactic:
by

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

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
C' : Type u₁'
inst✝³ : Category.{v₁', u₁'} C'
F : C ⥤ D
h : F.CoreMonoidal
inst✝² : F.OplaxMonoidal
inst✝¹ : IsIso (η F)
inst✝ : ∀ (X Y : C), IsIso (δ F X Y)
X Y Z : C
⊢ (asIso (δ F X Y)).symm.hom ▷ F.obj Z ≫ (asIso (δ F (X ⊗ Y) Z)).symm.hom ≫ F.map (α_ X Y Z).hom =
    (α_ (F.obj X) (F.obj Y) (F.obj Z)).hom ≫ F.obj X ◁ (asIso (δ F Y Z)).symm.hom ≫ (asIso (δ F X (Y ⊗ Z))).symm.hom

Tactic:
by

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

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
C' : Type u₁'
inst✝³ : Category.{v₁', u₁'} C'
F : C ⥤ D
h : F.CoreMonoidal
inst✝² : F.OplaxMonoidal
inst✝¹ : IsIso (η F)
inst✝ : ∀ (X Y : C), IsIso (δ F X Y)
X : C
⊢ (λ_ (F.obj X)).hom = (asIso (η F)).symm.hom ▷ F.obj X ≫ (asIso (δ F (𝟙_ C) X)).symm.hom ≫ F.map (λ_ X).hom

Tactic:
by

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

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
C' : Type u₁'
inst✝³ : Category.{v₁', u₁'} C'
F : C ⥤ D
h : F.CoreMonoidal
inst✝² : F.OplaxMonoidal
inst✝¹ : IsIso (η F)
inst✝ : ∀ (X Y : C), IsIso (δ F X Y)
X : C
⊢ (ρ_ (F.obj X)).hom = F.obj X ◁ (asIso (η F)).symm.hom ≫ (asIso (δ F X (𝟙_ C))).symm.hom ≫ F.map (ρ_ X).hom

Tactic:
by

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

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
C' : Type u₁'
inst✝³ : Category.{v₁', u₁'} C'
F✝ F : C ⥤ D
G : E ⥤ C'
inst✝² : MonoidalCategory C'
inst✝¹ : F.Monoidal
inst✝ : G.Monoidal
⊢ ε (F.prod G) ≫ η (F.prod G) = 𝟙 (𝟙_ (D × C'))

Tactic:
by

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

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
C' : Type u₁'
inst✝³ : Category.{v₁', u₁'} C'
F✝ F : C ⥤ D
G : E ⥤ C'
inst✝² : MonoidalCategory C'
inst✝¹ : F.Monoidal
inst✝ : G.Monoidal
⊢ η (F.prod G) ≫ ε (F.prod G) = 𝟙 ((F.prod G).obj (𝟙_ (C × E)))

Tactic:
by

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

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
C' : Type u₁'
inst✝³ : Category.{v₁', u₁'} C'
F✝ F : C ⥤ D
G : E ⥤ C'
inst✝² : MonoidalCategory C'
inst✝¹ : F.Monoidal
inst✝ : G.Monoidal
x✝¹ x✝ : C × E
⊢ μ (F.prod G) x✝¹ x✝ ≫ δ (F.prod G) x✝¹ x✝ = 𝟙 ((F.prod G).obj x✝¹ ⊗ (F.prod G).obj x✝)

Tactic:
by

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

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
C' : Type u₁'
inst✝³ : Category.{v₁', u₁'} C'
F✝ F : C ⥤ D
G : E ⥤ C'
inst✝² : MonoidalCategory C'
inst✝¹ : F.Monoidal
inst✝ : G.Monoidal
x✝¹ x✝ : C × E
⊢ δ (F.prod G) x✝¹ x✝ ≫ μ (F.prod G) x✝¹ x✝ = 𝟙 ((F.prod G).obj (x✝¹ ⊗ x✝))

Tactic:
by

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

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
F : C ⥤ D
G : C ⥤ E
inst✝¹ : F.LaxMonoidal
inst✝ : G.LaxMonoidal
⊢ (ε (F.prod' G)).1 = ε F

Tactic:
by

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

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
F : C ⥤ D
G : C ⥤ E
inst✝¹ : F.LaxMonoidal
inst✝ : G.LaxMonoidal
⊢ (ε (F.prod' G)).2 = ε G

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
F : J ⥤ Cᵒᵖ
c : Cocone F
hc : IsColimit c
s : Cone F.leftOp
j : Jᵒᵖ
⊢ ((hc.desc (coconeOfConeLeftOp s)).unop ≫ (coneLeftOpOfCocone c).π.app j).op = (s.π.app j).op

Tactic:
by

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

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
F : C ⥤ D
G : C ⥤ E
inst✝¹ : F.LaxMonoidal
inst✝ : G.LaxMonoidal
X Y : C
⊢ (μ (F.prod' G) X Y).1 = μ F X Y

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
F : J ⥤ Cᵒᵖ
c : Cocone F
hc : IsColimit c
s : Cone F.leftOp
m : s.pt ⟶ (coneLeftOpOfCocone c).pt
w : ∀ (j : Jᵒᵖ), m ≫ (coneLeftOpOfCocone c).π.app j = s.π.app j
⊢ m = (hc.desc (coconeOfConeLeftOp s)).unop

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
F : J ⥤ Cᵒᵖ
c : Cone F
hc : IsLimit c
s : Cocone F.leftOp
j : Jᵒᵖ
⊢ ((coconeLeftOpOfCone c).ι.app j ≫ (hc.lift (coneOfCoconeLeftOp s)).unop).op = (s.ι.app j).op

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
F : J ⥤ Cᵒᵖ
c : Cone F
hc : IsLimit c
s : Cocone F.leftOp
m : (coconeLeftOpOfCone c).pt ⟶ s.pt
w : ∀ (j : Jᵒᵖ), (coconeLeftOpOfCone c).ι.app j ≫ m = s.ι.app j
⊢ m = (hc.lift (coneOfCoconeLeftOp s)).unop

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
F : Jᵒᵖ ⥤ C
c : Cocone F
hc : IsColimit c
s : Cone F.rightOp
j : J
⊢ ((hc.desc (coconeOfConeRightOp s)).op ≫ (coneRightOpOfCocone c).π.app j).unop = (s.π.app j).unop

Tactic:
by

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

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
F : C ⥤ D
G : C ⥤ E
inst✝¹ : F.LaxMonoidal
inst✝ : G.LaxMonoidal
X Y : C
⊢ (μ (F.prod' G) X Y).2 = μ G X Y

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
F : Jᵒᵖ ⥤ C
c : Cocone F
hc : IsColimit c
s : Cone F.rightOp
m : s.pt ⟶ (coneRightOpOfCocone c).pt
w : ∀ (j : J), m ≫ (coneRightOpOfCocone c).π.app j = s.π.app j
⊢ m = (hc.desc (coconeOfConeRightOp s)).op

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
F : Jᵒᵖ ⥤ C
c : Cone F
hc : IsLimit c
s : Cocone F.rightOp
j : J
⊢ ((coconeRightOpOfCone c).ι.app j ≫ (hc.lift (coneOfCoconeRightOp s)).op).unop = (s.ι.app j).unop

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
F : Jᵒᵖ ⥤ C
c : Cone F
hc : IsLimit c
s : Cocone F.rightOp
m : (coconeRightOpOfCone c).pt ⟶ s.pt
w : ∀ (j : J), (coconeRightOpOfCone c).ι.app j ≫ m = s.ι.app j
⊢ m = (hc.lift (coneOfCoconeRightOp s)).op

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
F : Jᵒᵖ ⥤ Cᵒᵖ
c : Cocone F
hc : IsColimit c
s : Cone F.unop
j : J
⊢ ((hc.desc (coconeOfConeUnop s)).unop ≫ (coneUnopOfCocone c).π.app j).op = (s.π.app j).op

Tactic:
by

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

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
F : C ⥤ D
G : C ⥤ E
inst✝¹ : F.OplaxMonoidal
inst✝ : G.OplaxMonoidal
⊢ (η (F.prod' G)).1 = η F

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
F : Jᵒᵖ ⥤ Cᵒᵖ
c : Cocone F
hc : IsColimit c
s : Cone F.unop
m : s.pt ⟶ (coneUnopOfCocone c).pt
w : ∀ (j : J), m ≫ (coneUnopOfCocone c).π.app j = s.π.app j
⊢ m = (hc.desc (coconeOfConeUnop s)).unop

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
F : Jᵒᵖ ⥤ Cᵒᵖ
c : Cone F
hc : IsLimit c
s : Cocone F.unop
j : J
⊢ ((coconeUnopOfCone c).ι.app j ≫ (hc.lift (coneOfCoconeUnop s)).unop).op = (s.ι.app j).op

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
F : Jᵒᵖ ⥤ Cᵒᵖ
c : Cone F
hc : IsLimit c
s : Cocone F.unop
m : (coconeUnopOfCone c).pt ⟶ s.pt
w : ∀ (j : J), (coconeUnopOfCone c).ι.app j ≫ m = s.ι.app j
⊢ m = (hc.lift (coneOfCoconeUnop s)).unop

Tactic:
by

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

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
F : C ⥤ D
G : C ⥤ E
inst✝¹ : F.OplaxMonoidal
inst✝ : G.OplaxMonoidal
⊢ (η (F.prod' G)).2 = η G

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
F : J ⥤ Cᵒᵖ
c : Cocone F.leftOp
hc : IsColimit c
s : Cone F
j : J
⊢ ((hc.desc (coconeLeftOpOfCone s)).op ≫ (coneOfCoconeLeftOp c).π.app j).unop = (s.π.app j).unop

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
F : J ⥤ Cᵒᵖ
c : Cocone F.leftOp
hc : IsColimit c
s : Cone F
m : s.pt ⟶ (coneOfCoconeLeftOp c).pt
w : ∀ (j : J), m ≫ (coneOfCoconeLeftOp c).π.app j = s.π.app j
⊢ m = (hc.desc (coconeLeftOpOfCone s)).op

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
F : J ⥤ Cᵒᵖ
c : Cone F.leftOp
hc : IsLimit c
s : Cocone F
j : J
⊢ ((coconeOfConeLeftOp c).ι.app j ≫ (hc.lift (coneLeftOpOfCocone s)).op).unop = (s.ι.app j).unop

Tactic:
by

Goal state after: