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

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : MonoidalCategory C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : MonoidalLeftAction Cᵒᵖ Dᵒᵖ
x✝³ x✝² x✝¹ : C
x✝ : D
⊢ ((α_ x✝³ x✝² x✝¹).hom.op ⊵ₗ op x✝).unop ≫
      (αₗ (op x✝³) (op (x✝² ⊗ x✝¹)) (op x✝)).symm.unop.hom ≫
        (op x✝³ ⊴ₗ (αₗ (op x✝²) (op x✝¹) (op x✝)).symm.unop.hom.op).unop =
    (αₗ (op (x✝³ ⊗ x✝²)) (op x✝¹) (op x✝)).symm.unop.hom ≫
      (αₗ (op x✝³) (op x✝²) (op (unop (op x✝¹ ⊙ₗ op x✝)))).symm.unop.hom

Tactic:
apply Quiver.Hom.op_inj

Goal state after:
C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : MonoidalCategory C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : MonoidalLeftAction Cᵒᵖ Dᵒᵖ
x✝³ x✝² x✝¹ : C
x✝ : D
⊢ (((α_ x✝³ x✝² x✝¹).hom.op ⊵ₗ op x✝).unop ≫
        (αₗ (op x✝³) (op (x✝² ⊗ x✝¹)) (op x✝)).symm.unop.hom ≫
          (op x✝³ ⊴ₗ (αₗ (op x✝²) (op x✝¹) (op x✝)).symm.unop.hom.op).unop).op =
    ((αₗ (op (x✝³ ⊗ x✝²)) (op x✝¹) (op x✝)).symm.unop.hom ≫
        (αₗ (op x✝³) (op x✝²) (op (unop (op x✝¹ ⊙ₗ op x✝)))).symm.unop.hom).op
Module: Mathlib.CategoryTheory.Monoidal.Action.Opposites

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : MonoidalCategory C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : MonoidalLeftAction Cᵒᵖ Dᵒᵖ
x✝¹ : C
x✝ : D
⊢ ((λ_ x✝¹).hom.op ⊵ₗ op x✝).unop =
    (αₗ (op (𝟙_ C)) (op x✝¹) (op x✝)).symm.unop.hom ≫ (λₗ (op (unop (op x✝¹ ⊙ₗ op x✝)))).symm.unop.hom

Tactic:
apply Quiver.Hom.op_inj

Goal state after:
C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : MonoidalCategory C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : MonoidalLeftAction Cᵒᵖ Dᵒᵖ
x✝¹ : C
x✝ : D
⊢ ((λ_ x✝¹).hom.op ⊵ₗ op x✝).unop.op =
    ((αₗ (op (𝟙_ C)) (op x✝¹) (op x✝)).symm.unop.hom ≫ (λₗ (op (unop (op x✝¹ ⊙ₗ op x✝)))).symm.unop.hom).op
Module: Mathlib.CategoryTheory.Monoidal.Action.Opposites

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : MonoidalCategory C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : MonoidalLeftAction Cᵒᵖ Dᵒᵖ
x✝¹ : C
x✝ : D
⊢ ((ρ_ x✝¹).hom.op ⊵ₗ op x✝).unop =
    (αₗ (op x✝¹) (op (𝟙_ C)) (op x✝)).symm.unop.hom ≫ (op x✝¹ ⊴ₗ (λₗ (op x✝)).symm.unop.hom.op).unop

Tactic:
apply Quiver.Hom.op_inj

Goal state after:
C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : MonoidalCategory C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : MonoidalLeftAction Cᵒᵖ Dᵒᵖ
x✝¹ : C
x✝ : D
⊢ ((ρ_ x✝¹).hom.op ⊵ₗ op x✝).unop.op =
    ((αₗ (op x✝¹) (op (𝟙_ C)) (op x✝)).symm.unop.hom ≫ (op x✝¹ ⊴ₗ (λₗ (op x✝)).symm.unop.hom.op).unop).op
Module: Mathlib.CategoryTheory.Monoidal.Action.Opposites

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : MonoidalCategory C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : MonoidalRightAction Cᵒᵖ Dᵒᵖ
c✝ c'✝ : C
d✝ d'✝ : D
f : d✝ ⟶ d'✝
g : c✝ ⟶ c'✝
⊢ (f.op ⊙ᵣₘ g.op).unop = (f.op ⊵ᵣ op c✝).unop ≫ (op d'✝ ⊴ᵣ g.op).unop

Tactic:
apply Quiver.Hom.op_inj

Goal state after:
C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : MonoidalCategory C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : MonoidalRightAction Cᵒᵖ Dᵒᵖ
c✝ c'✝ : C
d✝ d'✝ : D
f : d✝ ⟶ d'✝
g : c✝ ⟶ c'✝
⊢ (f.op ⊙ᵣₘ g.op).unop.op = ((f.op ⊵ᵣ op c✝).unop ≫ (op d'✝ ⊴ᵣ g.op).unop).op
Module: Mathlib.CategoryTheory.Monoidal.Action.Opposites

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : MonoidalCategory C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : MonoidalRightAction Cᵒᵖ Dᵒᵖ
d₁✝ d₂✝ : D
c₁✝ c₂✝ c₃✝ c₄✝ : C
f : d₁✝ ⟶ d₂✝
g : c₁✝ ⟶ c₂✝
h : c₃✝ ⟶ c₄✝
⊢ (f.op ⊙ᵣₘ (g ⊗ₘ h).op).unop ≫ (αᵣ (op d₂✝) (op c₂✝) (op c₄✝)).symm.unop.hom =
    (αᵣ (op d₁✝) (op c₁✝) (op c₃✝)).symm.unop.hom ≫ ((f.op ⊙ᵣₘ g.op).unop.op ⊙ᵣₘ h.op).unop

Tactic:
apply Quiver.Hom.op_inj

Goal state after:
C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : MonoidalCategory C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : MonoidalRightAction Cᵒᵖ Dᵒᵖ
d₁✝ d₂✝ : D
c₁✝ c₂✝ c₃✝ c₄✝ : C
f : d₁✝ ⟶ d₂✝
g : c₁✝ ⟶ c₂✝
h : c₃✝ ⟶ c₄✝
⊢ ((f.op ⊙ᵣₘ (g ⊗ₘ h).op).unop ≫ (αᵣ (op d₂✝) (op c₂✝) (op c₄✝)).symm.unop.hom).op =
    ((αᵣ (op d₁✝) (op c₁✝) (op c₃✝)).symm.unop.hom ≫ ((f.op ⊙ᵣₘ g.op).unop.op ⊙ᵣₘ h.op).unop).op
Module: Mathlib.CategoryTheory.Monoidal.Action.Opposites

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : MonoidalCategory C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : MonoidalRightAction Cᵒᵖ Dᵒᵖ
d✝ d'✝ : D
x✝ : d✝ ⟶ d'✝
⊢ (ρᵣ (op d✝)).symm.unop.hom ≫ x✝ = (x✝.op ⊵ᵣ op (𝟙_ C)).unop ≫ (ρᵣ (op d'✝)).symm.unop.hom

Tactic:
apply Quiver.Hom.op_inj

Goal state after:
C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : MonoidalCategory C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : MonoidalRightAction Cᵒᵖ Dᵒᵖ
d✝ d'✝ : D
x✝ : d✝ ⟶ d'✝
⊢ ((ρᵣ (op d✝)).symm.unop.hom ≫ x✝).op = ((x✝.op ⊵ᵣ op (𝟙_ C)).unop ≫ (ρᵣ (op d'✝)).symm.unop.hom).op
Module: Mathlib.CategoryTheory.Monoidal.Action.Opposites

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : MonoidalCategory C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : MonoidalRightAction Cᵒᵖ Dᵒᵖ
x✝⁴ x✝³ x✝² : C
x✝¹ : x✝³ ⟶ x✝²
x✝ : D
⊢ (op x✝ ⊴ᵣ (x✝⁴ ◁ x✝¹).op).unop =
    (αᵣ (op x✝) (op x✝⁴) (op x✝³)).symm.unop.hom ≫
      (op (unop (op x✝ ⊙ᵣ op x✝⁴)) ⊴ᵣ x✝¹.op).unop ≫ (αᵣ (op x✝) (op x✝⁴) (op x✝²)).symm.unop.inv

Tactic:
apply Quiver.Hom.op_inj

Goal state after:
C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : MonoidalCategory C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : MonoidalRightAction Cᵒᵖ Dᵒᵖ
x✝⁴ x✝³ x✝² : C
x✝¹ : x✝³ ⟶ x✝²
x✝ : D
⊢ (op x✝ ⊴ᵣ (x✝⁴ ◁ x✝¹).op).unop.op =
    ((αᵣ (op x✝) (op x✝⁴) (op x✝³)).symm.unop.hom ≫
        (op (unop (op x✝ ⊙ᵣ op x✝⁴)) ⊴ᵣ x✝¹.op).unop ≫ (αᵣ (op x✝) (op x✝⁴) (op x✝²)).symm.unop.inv).op
Module: Mathlib.CategoryTheory.Monoidal.Action.Opposites

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : MonoidalCategory C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : MonoidalRightAction Cᵒᵖ Dᵒᵖ
x✝³ x✝² x✝¹ : C
x✝ : D
⊢ (op x✝ ⊴ᵣ (α_ x✝³ x✝² x✝¹).hom.op).unop ≫
      (αᵣ (op x✝) (op x✝³) (op (x✝² ⊗ x✝¹))).symm.unop.hom ≫
        (αᵣ (op (unop (op x✝ ⊙ᵣ op x✝³))) (op x✝²) (op x✝¹)).symm.unop.hom =
    (αᵣ (op x✝) (op (x✝³ ⊗ x✝²)) (op x✝¹)).symm.unop.hom ≫
      ((αᵣ (op x✝) (op x✝³) (op x✝²)).symm.unop.hom.op ⊵ᵣ op x✝¹).unop

Tactic:
apply Quiver.Hom.op_inj

Goal state after:
C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : MonoidalCategory C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : MonoidalRightAction Cᵒᵖ Dᵒᵖ
x✝³ x✝² x✝¹ : C
x✝ : D
⊢ ((op x✝ ⊴ᵣ (α_ x✝³ x✝² x✝¹).hom.op).unop ≫
        (αᵣ (op x✝) (op x✝³) (op (x✝² ⊗ x✝¹))).symm.unop.hom ≫
          (αᵣ (op (unop (op x✝ ⊙ᵣ op x✝³))) (op x✝²) (op x✝¹)).symm.unop.hom).op =
    ((αᵣ (op x✝) (op (x✝³ ⊗ x✝²)) (op x✝¹)).symm.unop.hom ≫
        ((αᵣ (op x✝) (op x✝³) (op x✝²)).symm.unop.hom.op ⊵ᵣ op x✝¹).unop).op
Module: Mathlib.CategoryTheory.Monoidal.Action.Opposites

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : MonoidalCategory C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : MonoidalRightAction Cᵒᵖ Dᵒᵖ
x✝¹ : C
x✝ : D
⊢ (op x✝ ⊴ᵣ (λ_ x✝¹).hom.op).unop =
    (αᵣ (op x✝) (op (𝟙_ C)) (op x✝¹)).symm.unop.hom ≫ ((ρᵣ (op x✝)).symm.unop.hom.op ⊵ᵣ op x✝¹).unop

Tactic:
apply Quiver.Hom.op_inj

Goal state after:
C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : MonoidalCategory C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : MonoidalRightAction Cᵒᵖ Dᵒᵖ
x✝¹ : C
x✝ : D
⊢ (op x✝ ⊴ᵣ (λ_ x✝¹).hom.op).unop.op =
    ((αᵣ (op x✝) (op (𝟙_ C)) (op x✝¹)).symm.unop.hom ≫ ((ρᵣ (op x✝)).symm.unop.hom.op ⊵ᵣ op x✝¹).unop).op
Module: Mathlib.CategoryTheory.Monoidal.Action.Opposites

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : MonoidalCategory C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : MonoidalRightAction Cᵒᵖ Dᵒᵖ
x✝¹ : C
x✝ : D
⊢ (op x✝ ⊴ᵣ (ρ_ x✝¹).hom.op).unop =
    (αᵣ (op x✝) (op x✝¹) (op (𝟙_ C))).symm.unop.hom ≫ (ρᵣ (op (unop (op x✝ ⊙ᵣ op x✝¹)))).symm.unop.hom

Tactic:
apply Quiver.Hom.op_inj

Goal state after:
C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : MonoidalCategory C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : MonoidalRightAction Cᵒᵖ Dᵒᵖ
x✝¹ : C
x✝ : D
⊢ (op x✝ ⊴ᵣ (ρ_ x✝¹).hom.op).unop.op =
    ((αᵣ (op x✝) (op x✝¹) (op (𝟙_ C))).symm.unop.hom ≫ (ρᵣ (op (unop (op x✝ ⊙ᵣ op x✝¹)))).symm.unop.hom).op
Module: Mathlib.CategoryTheory.Monoidal.Braided.Reflection

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Category.{v_2, u_2} D
inst✝⁴ : MonoidalCategory D
inst✝³ : SymmetricCategory D
inst✝² : MonoidalClosed D
R : C ⥤ D
inst✝¹ : R.Faithful
inst✝ : R.Full
L : D ⥤ C
adj : L ⊣ R
tfae_3_to_4 :
  (∀ (d d' : D), IsIso (L.map (adj.unit.app d ▷ d'))) → ∀ (d d' : D), IsIso (L.map (adj.unit.app d ⊗ₘ adj.unit.app d'))
tfae_4_to_1 :
  (∀ (d d' : D), IsIso (L.map (adj.unit.app d ⊗ₘ adj.unit.app d'))) →
    ∀ (c : C) (d : D), IsIso (adj.unit.app ((ihom d).obj (R.obj c)))
tfae_1_to_3 :
  (∀ (c : C) (d : D), IsIso (adj.unit.app ((ihom d).obj (R.obj c)))) → ∀ (d d' : D), IsIso (L.map (adj.unit.app d ▷ d'))
d d' : D
c : C
w₁ :
  ⇑(ConcreteCategory.hom ((coyoneda.map (L.map (adj.unit.app d ▷ d')).op).app c)) =
    ⇑(adj.homEquiv (Opposite.unop (Opposite.op ((𝟭 D).obj d ⊗ d'))) c).symm ∘
      ⇑(ConcreteCategory.hom ((coyoneda.map (adj.unit.app d ▷ d').op).app (R.obj c))) ∘
        ⇑(adj.homEquiv (Opposite.unop (Opposite.op ((L ⋙ R).obj d ⊗ d'))) c)
x✝ : (tensorLeft ((L ⋙ R).obj d)).obj (Opposite.unop (Opposite.op d')) ⟶ R.obj c
⊢ (ConcreteCategory.hom (↾fun g ↦ g ≫ (pre (adj.unit.app d)).app (R.obj c)))
      (((ihom.adjunction (R.obj (L.obj d))).homEquiv d' (R.obj c)) x✝) =
    ((ihom.adjunction d).homEquiv d' (R.obj c))
      ((ConcreteCategory.hom ((yoneda.obj (R.obj c)).map ((adj.unit.app d).op ▷ Opposite.op d'))) x✝)

Tactic:
Adjunction.homEquiv_unit,

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Category.{v_2, u_2} D
inst✝⁴ : MonoidalCategory D
inst✝³ : SymmetricCategory D
inst✝² : MonoidalClosed D
R : C ⥤ D
inst✝¹ : R.Faithful
inst✝ : R.Full
L : D ⥤ C
adj : L ⊣ R
tfae_3_to_4 :
  (∀ (d d' : D), IsIso (L.map (adj.unit.app d ▷ d'))) → ∀ (d d' : D), IsIso (L.map (adj.unit.app d ⊗ₘ adj.unit.app d'))
tfae_4_to_1 :
  (∀ (d d' : D), IsIso (L.map (adj.unit.app d ⊗ₘ adj.unit.app d'))) →
    ∀ (c : C) (d : D), IsIso (adj.unit.app ((ihom d).obj (R.obj c)))
tfae_1_to_3 :
  (∀ (c : C) (d : D), IsIso (adj.unit.app ((ihom d).obj (R.obj c)))) → ∀ (d d' : D), IsIso (L.map (adj.unit.app d ▷ d'))
d d' : D
c : C
w₁ :
  ⇑(ConcreteCategory.hom ((coyoneda.map (L.map (adj.unit.app d ▷ d')).op).app c)) =
    ⇑(adj.homEquiv (Opposite.unop (Opposite.op ((𝟭 D).obj d ⊗ d'))) c).symm ∘
      ⇑(ConcreteCategory.hom ((coyoneda.map (adj.unit.app d ▷ d').op).app (R.obj c))) ∘
        ⇑(adj.homEquiv (Opposite.unop (Opposite.op ((L ⋙ R).obj d ⊗ d'))) c)
x✝ : (tensorLeft ((L ⋙ R).obj d)).obj (Opposite.unop (Opposite.op d')) ⟶ R.obj c
⊢ (ConcreteCategory.hom (↾fun g ↦ g ≫ (pre (adj.unit.app d)).app (R.obj c)))
      ((ihom.adjunction (R.obj (L.obj d))).unit.app d' ≫ (ihom (R.obj (L.obj d))).map x✝) =
    ((ihom.adjunction d).homEquiv d' (R.obj c))
      ((ConcreteCategory.hom ((yoneda.obj (R.obj c)).map ((adj.unit.app d).op ▷ Opposite.op d'))) x✝)
Module: Mathlib.CategoryTheory.Monoidal.Closed.Enrichment

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
inst✝ : MonoidalClosed C
X Y₁ Y₂ : C
g : Y₁ ⟶ Y₂
⊢ (ρ_ ((ihom X).obj Y₁)).inv ≫ (ρ_ ((ihom X).obj Y₁)).hom ≫ (ihom X).map g = (ihom X).map g

Tactic:
Iso.inv_hom_id_assoc

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
inst✝ : MonoidalClosed C
X Y₁ Y₂ : C
g : Y₁ ⟶ Y₂
⊢ (ihom X).map g = (ihom X).map g
Module: Mathlib.CategoryTheory.Monoidal.Closed.Enrichment

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
inst✝ : MonoidalClosed C
X₁ X₂ : C
f : X₁ ⟶ X₂
Y : C
⊢ (λ_ ((ihom X₂).obj Y)).inv ≫ (λ_ ((ihom X₂).obj Y)).hom ≫ (pre f).app Y = (pre f).app Y

Tactic:
Iso.inv_hom_id_assoc

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
inst✝ : MonoidalClosed C
X₁ X₂ : C
f : X₁ ⟶ X₂
Y : C
⊢ (pre f).app Y = (pre f).app Y
Module: Mathlib.CategoryTheory.Monoidal.Closed.Ideal

Goal state before:
pp: case h_fst
C : Type u₁
D : Type u₂
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : Category.{v₁, u₂} D
i : D ⥤ C
inst✝⁵ : CartesianMonoidalCategory C
inst✝⁴ : Reflective i
inst✝³ : MonoidalClosed C
inst✝² : CartesianMonoidalCategory D
inst✝¹ : ExponentialIdeal i
inst✝ : BraidedCategory C
A B : C
⊢ fst A B ≫ (reflectorAdjunction i).unit.app A =
    (reflectorAdjunction i).unit.app (A ⊗ B) ≫
      i.map (prodComparison (reflector i) A B ≫ fst ((reflector i).obj A) ((reflector i).obj B))

Tactic:
prodComparison_fst

Goal state after:
case h_fst
C : Type u₁
D : Type u₂
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : Category.{v₁, u₂} D
i : D ⥤ C
inst✝⁵ : CartesianMonoidalCategory C
inst✝⁴ : Reflective i
inst✝³ : MonoidalClosed C
inst✝² : CartesianMonoidalCategory D
inst✝¹ : ExponentialIdeal i
inst✝ : BraidedCategory C
A B : C
⊢ fst A B ≫ (reflectorAdjunction i).unit.app A =
    (reflectorAdjunction i).unit.app (A ⊗ B) ≫ i.map ((reflector i).map (fst A B))
Module: Mathlib.CategoryTheory.Monoidal.Closed.Ideal

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : Category.{v₁, u₂} D
i : D ⥤ C
inst✝⁵ : CartesianMonoidalCategory C
inst✝⁴ : Reflective i
inst✝³ : MonoidalClosed C
inst✝² : CartesianMonoidalCategory D
inst✝¹ : ExponentialIdeal i
inst✝ : BraidedCategory C
A B : C
X X' : D
f : (reflector i).obj (A ⊗ B) ⟶ X
g : X ⟶ X'
⊢ prodComparison i ((reflector i).obj A) ((reflector i).obj B) ≫
      uncurry
          ((unitCompPartialBijective B ⋯)
            (curry
              ((β_ B (i.obj ((reflector i).obj A))).inv ≫
                uncurry
                    ((unitCompPartialBijective A ⋯)
                      (curry ((β_ A B).inv ≫ ((reflectorAdjunction i).homEquiv (A ⊗ B) X') (f ≫ g) ≫ 𝟙 (i.obj X')))) ≫
                  𝟙 (i.obj X')))) ≫
        𝟙 (i.obj X') =
    i.map
        (i.fullyFaithfulOfReflective.preimage
          (prodComparison i ((reflector i).obj A) ((reflector i).obj B) ≫
            uncurry
                ((unitCompPartialBijective B ⋯)
                  (curry
                    ((β_ B (i.obj ((reflector i).obj A))).inv ≫
                      uncurry
                          ((unitCompPartialBijective A ⋯)
                            (curry ((β_ A B).inv ≫ ((reflectorAdjunction i).homEquiv (A ⊗ B) X) f ≫ 𝟙 (i.obj X)))) ≫
                        𝟙 (i.obj X)))) ≫
              𝟙 (i.obj X))) ≫
      i.map g

Tactic:
Adjunction.homEquiv_unit,

Goal state after:
C : Type u₁
D : Type u₂
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : Category.{v₁, u₂} D
i : D ⥤ C
inst✝⁵ : CartesianMonoidalCategory C
inst✝⁴ : Reflective i
inst✝³ : MonoidalClosed C
inst✝² : CartesianMonoidalCategory D
inst✝¹ : ExponentialIdeal i
inst✝ : BraidedCategory C
A B : C
X X' : D
f : (reflector i).obj (A ⊗ B) ⟶ X
g : X ⟶ X'
⊢ prodComparison i ((reflector i).obj A) ((reflector i).obj B) ≫
      uncurry
          ((unitCompPartialBijective B ⋯)
            (curry
              ((β_ B (i.obj ((reflector i).obj A))).inv ≫
                uncurry
                    ((unitCompPartialBijective A ⋯)
                      (curry
                        ((β_ A B).inv ≫ ((reflectorAdjunction i).unit.app (A ⊗ B) ≫ i.map (f ≫ g)) ≫ 𝟙 (i.obj X')))) ≫
                  𝟙 (i.obj X')))) ≫
        𝟙 (i.obj X') =
    i.map
        (i.fullyFaithfulOfReflective.preimage
          (prodComparison i ((reflector i).obj A) ((reflector i).obj B) ≫
            uncurry
                ((unitCompPartialBijective B ⋯)
                  (curry
                    ((β_ B (i.obj ((reflector i).obj A))).inv ≫
                      uncurry
                          ((unitCompPartialBijective A ⋯)
                            (curry ((β_ A B).inv ≫ ((reflectorAdjunction i).homEquiv (A ⊗ B) X) f ≫ 𝟙 (i.obj X)))) ≫
                        𝟙 (i.obj X)))) ≫
              𝟙 (i.obj X))) ≫
      i.map g
Module: Mathlib.CategoryTheory.Monoidal.Closed.Ideal

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : Category.{v₁, u₂} D
i : D ⥤ C
inst✝⁵ : CartesianMonoidalCategory C
inst✝⁴ : Reflective i
inst✝³ : MonoidalClosed C
inst✝² : CartesianMonoidalCategory D
inst✝¹ : ExponentialIdeal i
inst✝ : BraidedCategory C
A B : C
⊢ prodComparison (reflector i) A B ≫ (bijection i A B ((reflector i).obj (A ⊗ B))) (𝟙 ((reflector i).obj (A ⊗ B))) =
    𝟙 ((reflector i).obj (A ⊗ B))

Tactic:
← (bijection i _ _ _).injective.eq_iff,

Goal state after:
C : Type u₁
D : Type u₂
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : Category.{v₁, u₂} D
i : D ⥤ C
inst✝⁵ : CartesianMonoidalCategory C
inst✝⁴ : Reflective i
inst✝³ : MonoidalClosed C
inst✝² : CartesianMonoidalCategory D
inst✝¹ : ExponentialIdeal i
inst✝ : BraidedCategory C
A B : C
⊢ (bijection i A B ((reflector i).obj (A ⊗ B)))
      (prodComparison (reflector i) A B ≫
        (bijection i A B ((reflector i).obj (A ⊗ B))) (𝟙 ((reflector i).obj (A ⊗ B)))) =
    (bijection i A B ((reflector i).obj (A ⊗ B))) (𝟙 ((reflector i).obj (A ⊗ B)))
Module: Mathlib.CategoryTheory.Monoidal.Free.Coherence

Goal state before:
pp: case mk
C : Type u
n : NormalMonoidalObject C
X Y : F C
f : X ⟶ Y
f' : X ⟶ᵐ Y
⊢ (fun n ↦ X.normalizeObj n) = Y.normalizeObj

Tactic:
clear n f

Goal state after:
case mk
C : Type u
X Y : F C
f' : X ⟶ᵐ Y
⊢ (fun n ↦ X.normalizeObj n) = Y.normalizeObj
Module: Mathlib.CategoryTheory.Monoidal.Hopf_

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
this : Δ ≫ 𝒮 ▷ A ≫ μ ≫ ε = ε ≫ η ≫ ε
⊢ 𝒮 ≫ ε = ε

Tactic:
rw [Bimon.mul_counit, tensorHom_def', Category.assoc, ← whisker_exchange_assoc] at this

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
this : Δ ≫ A ◁ ε ≫ 𝒮 ▷ 𝟙_ C ≫ ε ▷ 𝟙_ C ≫ (λ_ (𝟙_ C)).hom = ε ≫ η ≫ ε
⊢ 𝒮 ≫ ε = ε
Module: Mathlib.CategoryTheory.Monoidal.Hopf_

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
⊢ Δ ≫
      A ◁ Δ ≫
        (α_ A A A).inv ≫
          (α_ A A A).hom ≫
            A ◁ A ◁ Δ ≫
              A ◁ A ◁ 𝒮 ▷ A ≫
                (((A ◁ (α_ A A A).inv ≫ A ◁ μ ▷ A ≫ A ◁ (β_ A A).hom) ≫ A ◁ 𝒮 ▷ A) ≫ (α_ A A A).inv) ≫ μ ▷ A =
    ε ≫ (λ_ (𝟙_ C)).inv ≫ (η ⊗ₘ η)

Tactic:
Iso.inv_hom_id_assoc

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
⊢ Δ ≫
      A ◁ Δ ≫
        A ◁ A ◁ Δ ≫
          A ◁ A ◁ 𝒮 ▷ A ≫ (((A ◁ (α_ A A A).inv ≫ A ◁ μ ▷ A ≫ A ◁ (β_ A A).hom) ≫ A ◁ 𝒮 ▷ A) ≫ (α_ A A A).inv) ≫ μ ▷ A =
    ε ≫ (λ_ (𝟙_ C)).inv ≫ (η ⊗ₘ η)
Module: Mathlib.CategoryTheory.Monoidal.Hopf_

Goal state before:
pp: case a.a.a.a.a.a.a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| A ◁ Δ ≫ A ◁ A ◁ Δ

pp: case a.a.a.a.a.a.a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| A ◁ A ◁ 𝒮 ▷ A

pp: case a.a.a.a.a.a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| A ◁ (α_ A A A).inv

pp: case a.a.a.a.a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| A ◁ μ ▷ A

pp: case a.a.a.a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| A ◁ (β_ A A).hom

pp: case a.a.a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| A ◁ 𝒮 ▷ A

pp: case a.a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| (α_ A A A).inv

pp: case a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| μ ▷ A

pp: case a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| Δ

Tactic:
simp only [← whiskerLeft_comp]
    rw [ComonObj.comul_assoc]
    simp only [whiskerLeft_comp]

Goal state after:
case a.a.a.a.a.a.a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| A ◁ Δ ≫ A ◁ Δ ▷ A ≫ A ◁ (α_ A A A).hom

case a.a.a.a.a.a.a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| A ◁ A ◁ 𝒮 ▷ A

case a.a.a.a.a.a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| A ◁ (α_ A A A).inv

case a.a.a.a.a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| A ◁ μ ▷ A

case a.a.a.a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| A ◁ (β_ A A).hom

case a.a.a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| A ◁ 𝒮 ▷ A

case a.a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| (α_ A A A).inv

case a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| μ ▷ A

case a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| Δ
Module: Mathlib.CategoryTheory.Monoidal.Bimod

Goal state before:
pp: case a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
R S T U : Mon C
P : Bimod R S
Q : Bimod S T
L : Bimod T U
| (α_ P.X Q.X L.X).inv ≫
    (α_ P.X Q.X L.X).hom ≫ P.X ◁ coequalizer.π (Q.actRight ▷ L.X) ((α_ Q.X T.X L.X).hom ≫ Q.X ◁ L.actLeft)

pp: case a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
R S T U : Mon C
P : Bimod R S
Q : Bimod S T
L : Bimod T U
| coequalizer.π (P.actRight ▷ TensorBimod.X Q L) ((α_ P.X S.X (TensorBimod.X Q L)).hom ≫ P.X ◁ TensorBimod.actLeft Q L)

Tactic:
Iso.inv_hom_id_assoc

Goal state after:
case a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
R S T U : Mon C
P : Bimod R S
Q : Bimod S T
L : Bimod T U
| P.X ◁ coequalizer.π (Q.actRight ▷ L.X) ((α_ Q.X T.X L.X).hom ≫ Q.X ◁ L.actLeft)

case a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
R S T U : Mon C
P : Bimod R S
Q : Bimod S T
L : Bimod T U
| coequalizer.π (P.actRight ▷ TensorBimod.X Q L) ((α_ P.X S.X (TensorBimod.X Q L)).hom ≫ P.X ◁ TensorBimod.actLeft Q L)