mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.MarkovCategory.Positive

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : MonoidalCategory C
inst✝¹ : PositiveCategory C
X Y : C
f : X ⟶ Y
inst✝ : IsIso f
⊢ Deterministic (𝟙 X)

Tactic:
]

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : MonoidalCategory C
inst✝¹ : PositiveCategory C
X Y : C
f : X ⟶ Y
inst✝ : IsIso f
⊢ Deterministic (𝟙 X)
Module: Mathlib.CategoryTheory.MarkovCategory.Positive

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : MonoidalCategory C
inst✝¹ : PositiveCategory C
X Y : C
f : X ⟶ Y
inst✝ : IsIso f
⊢ (Δ ≫ (f ≫ inv f ⊗ₘ f)) ≫ (f ⊗ₘ 𝟙 Y) = (Δ ≫ (𝟙 X ⊗ₘ f)) ≫ (f ⊗ₘ 𝟙 Y)

Tactic:
]

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : MonoidalCategory C
inst✝¹ : PositiveCategory C
X Y : C
f : X ⟶ Y
inst✝ : IsIso f
⊢ (Δ ≫ (f ≫ inv f ⊗ₘ f)) ≫ (f ⊗ₘ 𝟙 Y) = (Δ ≫ (𝟙 X ⊗ₘ f)) ≫ (f ⊗ₘ 𝟙 Y)
Module: Mathlib.CategoryTheory.MarkovCategory.Positive

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : MonoidalCategory C
inst✝¹ : PositiveCategory C
X Y : C
f : X ⟶ Y
inst✝ : IsIso f
⊢ Δ ≫ (𝟙 X ≫ f ⊗ₘ f ≫ 𝟙 Y) = Δ ≫ (𝟙 X ≫ f ⊗ₘ f ≫ 𝟙 Y)

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.LocallyCartesianClosed.Sections

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : CartesianMonoidalCategory C
I : C
inst✝² : Closed I
inst✝¹ : ChosenPullbacksAlong (curryRightUnitorHom I)
inst✝ : BraidedCategory C
X : Over I
A : C
v : A ⟶ (sections I).obj X
v₂ : A ⟶ (ihom I).obj X.left := v ≫ ChosenPullbacksAlong.fst ((ihom I).map X.hom) (curryRightUnitorHom I)
comm : toUnit A ≫ curry (ρ_ I).hom = v₂ ≫ (ihom I).map X.hom
w' : I ◁ toUnit A ≫ (ρ_ I).hom = ((ihom.adjunction I).homEquiv A X.left).symm v₂ ≫ X.hom
⊢ SemiCartesianMonoidalCategory.snd A I = SemiCartesianMonoidalCategory.snd A I

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.LocallyCartesianClosed.Sections

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : CartesianMonoidalCategory C
I : C
inst✝² : Closed I
inst✝¹ : ChosenPullbacksAlong (curryRightUnitorHom I)
inst✝ : BraidedCategory C
A' A : C
X : Over I
g : A' ⟶ A
v : A ⟶ (sections I).obj X
⊢ homMk ((β_ A' I).hom ≫ uncurry ((g ≫ v) ≫ ChosenPullbacksAlong.fst ((ihom I).map X.hom) (curry (ρ_ I).hom))) ⋯ =
    homMk (g ▷ I ≫ (β_ A I).hom ≫ uncurry (v ≫ ChosenPullbacksAlong.fst ((ihom I).map X.hom) (curry (ρ_ I).hom))) ⋯

Tactic:
]

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : CartesianMonoidalCategory C
I : C
inst✝² : Closed I
inst✝¹ : ChosenPullbacksAlong (curryRightUnitorHom I)
inst✝ : BraidedCategory C
A' A : C
X : Over I
g : A' ⟶ A
v : A ⟶ (sections I).obj X
⊢ homMk ((β_ A' I).hom ≫ uncurry ((g ≫ v) ≫ ChosenPullbacksAlong.fst ((ihom I).map X.hom) (curry (ρ_ I).hom))) ⋯ =
    homMk (g ▷ I ≫ (β_ A I).hom ≫ uncurry (v ≫ ChosenPullbacksAlong.fst ((ihom I).map X.hom) (curry (ρ_ I).hom))) ⋯
Module: Mathlib.CategoryTheory.LocallyCartesianClosed.Over

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X : C
Y Z : Over X
inst✝ : ChosenPullbacksAlong Z.hom
T✝ : Over X
u : T✝ ⟶ Y
v : T✝ ⟶ Z
⊢ T✝.hom = T✝.hom

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.LocallyCartesianClosed.Over

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : CartesianMonoidalCategory C
X : C
Z : Over X
A : C
f : Z ⟶ (toOver X).obj A
⊢ (Over.forget X).map f ≫ SemiCartesianMonoidalCategory.fst A X =
    Over.Hom.left f ≫ SemiCartesianMonoidalCategory.fst A X

Tactic:
]

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : CartesianMonoidalCategory C
X : C
Z : Over X
A : C
f : Z ⟶ (toOver X).obj A
⊢ (Over.forget X).map f ≫ SemiCartesianMonoidalCategory.fst A X =
    Over.Hom.left f ≫ SemiCartesianMonoidalCategory.fst A X
Module: Mathlib.CategoryTheory.Monad.Kleisli

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
T : Monad C
X Y : Kleisli T
f : X.Hom Y
⊢ (𝟭 C).map f.of ≫ 𝟙 ((𝟭 C).obj (T.obj Y.of)) = f.of

Tactic:
]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
T : Monad C
X Y : Kleisli T
f : X.Hom Y
⊢ (𝟭 C).map f.of ≫ 𝟙 ((𝟭 C).obj (T.obj Y.of)) = f.of
Module: Mathlib.CategoryTheory.Monad.Monadicity

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₁, u₂} D
G : D ⥤ C
F : C ⥤ D
adj : F ⊣ G
A : adj.toMonad.Algebra
⊢ F.map (adj.unit.app A.A ≫ A.a) = F.map (𝟙 ((𝟭 C).obj A.A))

Tactic:
]

Goal state after:
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₁, u₂} D
G : D ⥤ C
F : C ⥤ D
adj : F ⊣ G
A : adj.toMonad.Algebra
⊢ F.map (adj.unit.app A.A ≫ A.a) = F.map (𝟙 ((𝟭 C).obj A.A))
Module: Mathlib.CategoryTheory.Monad.Monadicity

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₁, u₂} D
G : D ⥤ C
F : C ⥤ D
adj : F ⊣ G
A : adj.toMonad.Algebra
⊢ 𝟙 (F.obj A.A) = 𝟙 (F.obj A.A)

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Monad.Monadicity

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₁, u₂} D
G : D ⥤ C
F : C ⥤ D
adj : F ⊣ G
A : adj.toMonad.Algebra
B : D
inst✝ : HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))
f : F.obj A.A ⟶ B
⊢ A.a ≫ adj.unit.app A.A ≫ G.map f = adj.unit.app (adj.toMonad.obj A.A) ≫ G.map (adj.counit.app (F.obj A.A)) ≫ G.map f ↔
    G.map (F.map (adj.unit.app A.A ≫ G.map f)) ≫ G.map (adj.counit.app B) = A.a ≫ adj.unit.app A.A ≫ G.map f

Tactic:
]

Goal state after:
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₁, u₂} D
G : D ⥤ C
F : C ⥤ D
adj : F ⊣ G
A : adj.toMonad.Algebra
B : D
inst✝ : HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))
f : F.obj A.A ⟶ B
⊢ A.a ≫ adj.unit.app A.A ≫ G.map f = adj.unit.app (adj.toMonad.obj A.A) ≫ G.map (adj.counit.app (F.obj A.A)) ≫ G.map f ↔
    G.map (F.map (adj.unit.app A.A ≫ G.map f)) ≫ G.map (adj.counit.app B) = A.a ≫ adj.unit.app A.A ≫ G.map f
Module: Mathlib.CategoryTheory.Monad.Monadicity

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₁, u₂} D
G : D ⥤ C
F : C ⥤ D
adj : F ⊣ G
A : adj.toMonad.Algebra
B : D
inst✝ : HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))
f : F.obj A.A ⟶ B
⊢ A.a ≫ adj.unit.app A.A ≫ G.map f = G.map f ↔ G.map f = A.a ≫ adj.unit.app A.A ≫ G.map f

Tactic:
]

Goal state after:
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₁, u₂} D
G : D ⥤ C
F : C ⥤ D
adj : F ⊣ G
A : adj.toMonad.Algebra
B : D
inst✝ : HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))
f : F.obj A.A ⟶ B
⊢ A.a ≫ adj.unit.app A.A ≫ G.map f = G.map f ↔ G.map f = A.a ≫ adj.unit.app A.A ≫ G.map f
Module: Mathlib.CategoryTheory.Monad.Monadicity

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₁, u₂} D
G : D ⥤ C
F : C ⥤ D
adj : F ⊣ G
A : adj.toMonad.Algebra
inst✝ : HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))
⊢ G.map (adj.counit.app (F.obj A.A)) ≫ G.map (coequalizer.π (F.map A.a) (adj.counit.app (F.obj A.A))) =
    G.map (adj.counit.app (F.obj A.A)) ≫ G.map (coequalizer.π (F.map A.a) (adj.counit.app (F.obj A.A)))

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Monad.Monadicity

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₁, u₂} D
G : D ⥤ C
F : C ⥤ D
adj : F ⊣ G
inst✝ : ∀ (A : adj.toMonad.Algebra), HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))
A : adj.toMonad.Algebra
⊢ (beckCofork A).π ≫ ((comparisonAdjunction adj).unit.app A).f = (unitCofork A).π

Tactic:
]

Goal state after:
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₁, u₂} D
G : D ⥤ C
F : C ⥤ D
adj : F ⊣ G
inst✝ : ∀ (A : adj.toMonad.Algebra), HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))
A : adj.toMonad.Algebra
⊢ (beckCofork A).π ≫ ((comparisonAdjunction adj).unit.app A).f = (unitCofork A).π
Module: Mathlib.CategoryTheory.Monad.Monadicity

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₁, u₂} D
G : D ⥤ C
F : C ⥤ D
adj : F ⊣ G
inst✝ : ∀ (A : adj.toMonad.Algebra), HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))
A : adj.toMonad.Algebra
⊢ adj.unit.app (adj.toMonad.obj A.A) ≫
      G.map (adj.counit.app (F.obj A.A)) ≫ G.map (coequalizer.π (F.map A.a) (adj.counit.app (F.obj A.A))) =
    G.map (coequalizer.π (F.map A.a) (adj.counit.app (F.obj A.A)))

Tactic:
]

Goal state after:
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₁, u₂} D
G : D ⥤ C
F : C ⥤ D
adj : F ⊣ G
inst✝ : ∀ (A : adj.toMonad.Algebra), HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))
A : adj.toMonad.Algebra
⊢ adj.unit.app (adj.toMonad.obj A.A) ≫
      G.map (adj.counit.app (F.obj A.A)) ≫ G.map (coequalizer.π (F.map A.a) (adj.counit.app (F.obj A.A))) =
    G.map (coequalizer.π (F.map A.a) (adj.counit.app (F.obj A.A)))
Module: Mathlib.CategoryTheory.Monad.Monadicity

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Category.{v₁, u₂} D
G : D ⥤ C
F : C ⥤ D
adj : F ⊣ G
inst✝² : HasCoequalizerOfIsSplitPair G
inst✝¹ : PreservesColimitOfIsSplitPair G
inst✝ : ReflectsColimitOfIsSplitPair G
X : adj.toMonad.Algebra
⊢ IsIso ((beckCoequalizer X).desc (unitCofork X))

Tactic:
]

Goal state after:
C : Type u₁
D : Type u₂
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Category.{v₁, u₂} D
G : D ⥤ C
F : C ⥤ D
adj : F ⊣ G
inst✝² : HasCoequalizerOfIsSplitPair G
inst✝¹ : PreservesColimitOfIsSplitPair G
inst✝ : ReflectsColimitOfIsSplitPair G
X : adj.toMonad.Algebra
⊢ IsIso ((beckCoequalizer X).desc (unitCofork X))
Module: Mathlib.CategoryTheory.Monad.Monadicity

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Category.{v₁, u₂} D
G : D ⥤ C
F : C ⥤ D
adj : F ⊣ G
inst✝² : HasCoequalizerOfIsSplitPair G
inst✝¹ : PreservesColimitOfIsSplitPair G
inst✝ : ReflectsColimitOfIsSplitPair G
this : ∀ (X : adj.toMonad.Algebra), IsIso ((comparisonAdjunction adj).unit.app X)
Y : D
⊢ IsIso
    (colimit.desc (parallelPair (F.map (G.map (adj.counit.app Y))) (adj.counit.app (F.obj (G.obj Y))))
      (counitCofork adj Y))

Tactic:
]

Goal state after:
C : Type u₁
D : Type u₂
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Category.{v₁, u₂} D
G : D ⥤ C
F : C ⥤ D
adj : F ⊣ G
inst✝² : HasCoequalizerOfIsSplitPair G
inst✝¹ : PreservesColimitOfIsSplitPair G
inst✝ : ReflectsColimitOfIsSplitPair G
this : ∀ (X : adj.toMonad.Algebra), IsIso ((comparisonAdjunction adj).unit.app X)
Y : D
⊢ IsIso
    (colimit.desc (parallelPair (F.map (G.map (adj.counit.app Y))) (adj.counit.app (F.obj (G.obj Y))))
      (counitCofork adj Y))
Module: Mathlib.CategoryTheory.Monad.Monadicity

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₁, u₂} D
G : D ⥤ C
F : C ⥤ D
adj : F ⊣ G
inst✝¹ : CreatesColimitOfIsSplitPair G
A B : D
f g : A ⟶ B
inst✝ : G.IsSplitPair f g
⊢ HasColimit
    (parallelPair ((parallelPair f g ⋙ G).map WalkingParallelPairHom.left)
      ((parallelPair f g ⋙ G).map WalkingParallelPairHom.right))

Tactic:
]

Goal state after:
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₁, u₂} D
G : D ⥤ C
F : C ⥤ D
adj : F ⊣ G
inst✝¹ : CreatesColimitOfIsSplitPair G
A B : D
f g : A ⟶ B
inst✝ : G.IsSplitPair f g
⊢ HasColimit
    (parallelPair ((parallelPair f g ⋙ G).map WalkingParallelPairHom.left)
      ((parallelPair f g ⋙ G).map WalkingParallelPairHom.right))
Module: Mathlib.CategoryTheory.Monad.Monadicity

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Category.{v₁, u₂} D
G : D ⥤ C
F : C ⥤ D
adj : F ⊣ G
inst✝² : HasReflexiveCoequalizers D
inst✝¹ : G.ReflectsIsomorphisms
inst✝ : PreservesColimitOfIsReflexivePair G
X : adj.toMonad.Algebra
⊢ IsIso ((beckCoequalizer X).desc (unitCofork X))

Tactic:
]

Goal state after:
C : Type u₁
D : Type u₂
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Category.{v₁, u₂} D
G : D ⥤ C
F : C ⥤ D
adj : F ⊣ G
inst✝² : HasReflexiveCoequalizers D
inst✝¹ : G.ReflectsIsomorphisms
inst✝ : PreservesColimitOfIsReflexivePair G
X : adj.toMonad.Algebra
⊢ IsIso ((beckCoequalizer X).desc (unitCofork X))
Module: Mathlib.CategoryTheory.Monad.Monadicity

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Category.{v₁, u₂} D
G : D ⥤ C
F : C ⥤ D
adj : F ⊣ G
inst✝² : HasReflexiveCoequalizers D
inst✝¹ : G.ReflectsIsomorphisms
inst✝ : PreservesColimitOfIsReflexivePair G
this : ∀ (X : adj.toMonad.Algebra), IsIso ((comparisonAdjunction adj).unit.app X)
Y : D
⊢ IsIso
    (colimit.desc (parallelPair (F.map (G.map (adj.counit.app Y))) (adj.counit.app (F.obj (G.obj Y))))
      (counitCofork adj Y))

Tactic:
]

Goal state after:
C : Type u₁
D : Type u₂
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Category.{v₁, u₂} D
G : D ⥤ C
F : C ⥤ D
adj : F ⊣ G
inst✝² : HasReflexiveCoequalizers D
inst✝¹ : G.ReflectsIsomorphisms
inst✝ : PreservesColimitOfIsReflexivePair G
this : ∀ (X : adj.toMonad.Algebra), IsIso ((comparisonAdjunction adj).unit.app X)
Y : D
⊢ IsIso
    (colimit.desc (parallelPair (F.map (G.map (adj.counit.app Y))) (adj.counit.app (F.obj (G.obj Y))))
      (counitCofork adj Y))
Module: Mathlib.CategoryTheory.Monoidal.Action.Basic

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 C
inst✝ : MonoidalLeftAction C D
x y : D
f : x ⟶ y
⊢ 𝟙_ C ⊴ₗ f = (𝟙_ C ⊴ₗ f ≫ (λₗ y).hom) ≫ (λₗ y).inv

Tactic:
]

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 C
inst✝ : MonoidalLeftAction C D
x y : D
f : x ⟶ y
⊢ 𝟙_ C ⊴ₗ f = (𝟙_ C ⊴ₗ f ≫ (λₗ y).hom) ≫ (λₗ y).inv
Module: Mathlib.CategoryTheory.Monoidal.Action.Basic

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 C
inst✝ : MonoidalLeftAction C D
x y : C
z z' : D
f : z ⟶ z'
⊢ 𝟙 (x ⊗ y) ⊙ₗₘ f = (((𝟙 x ⊗ₘ 𝟙 y) ⊙ₗₘ f) ≫ (αₗ x y z').hom) ≫ (αₗ x y z').inv

Tactic:
]

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 C
inst✝ : MonoidalLeftAction C D
x y : C
z z' : D
f : z ⟶ z'
⊢ 𝟙 (x ⊗ y) ⊙ₗₘ f = (((𝟙 x ⊗ₘ 𝟙 y) ⊙ₗₘ f) ≫ (αₗ x y z').hom) ≫ (αₗ x y z').inv
Module: Mathlib.CategoryTheory.Monoidal.Action.Basic

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 C
inst✝ : MonoidalLeftAction C D
c₁ c₂ c₃ c₄ : C
d₁ d₂ : D
f : c₁ ⟶ c₂
g : c₃ ⟶ c₄
h : d₁ ⟶ d₂
⊢ (αₗ c₁ c₃ d₁).hom ≫ (f ⊙ₗₘ g ⊙ₗₘ h) = (αₗ c₁ c₃ d₁).hom ≫ (f ⊙ₗₘ g ⊙ₗₘ h)

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Action.Basic

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 C
inst✝ : MonoidalLeftAction C D
d d' : D
f : d ⟶ d'
⊢ 𝟙_ C ⊴ₗ f ≫ (λₗ d').hom = 𝟙_ C ⊴ₗ f ≫ (λₗ d').hom

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Action.Basic

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 C
inst✝ : MonoidalLeftAction C D
x : C
y z : D
f : y ≅ z
⊢ 𝟙 (x ⊙ₗ y) = 𝟙 (x ⊙ₗ y)

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Action.Basic

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 C
inst✝ : MonoidalLeftAction C D
x y : C
f : x ≅ y
z : D
⊢ 𝟙 (x ⊙ₗ z) = 𝟙 (x ⊙ₗ z)

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Action.Basic

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 C
inst✝ : MonoidalLeftAction C D
x : C
y z : D
f : y ≅ z
⊢ 𝟙 (x ⊙ₗ z) = 𝟙 (x ⊙ₗ z)

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Action.Basic

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 C
inst✝ : MonoidalLeftAction C D
x y : C
f : x ≅ y
z : D
⊢ 𝟙 (y ⊙ₗ z) = 𝟙 (y ⊙ₗ z)

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Action.Basic

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 C
inst✝¹ : MonoidalLeftAction C D
x : C
y z : D
f : y ⟶ z
inst✝ : IsIso f
⊢ 𝟙 (x ⊙ₗ y) = 𝟙 (x ⊙ₗ y)

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Action.Basic

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 C
inst✝¹ : MonoidalLeftAction C D
x y : C
f : x ⟶ y
inst✝ : IsIso f
z : D
⊢ 𝟙 (x ⊙ₗ z) = 𝟙 (x ⊙ₗ z)

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Action.Basic

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 C
inst✝¹ : MonoidalLeftAction C D
x : C
y z : D
f : y ⟶ z
inst✝ : IsIso f
⊢ 𝟙 (x ⊙ₗ z) = 𝟙 (x ⊙ₗ z)

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Action.Basic

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 C
inst✝¹ : MonoidalLeftAction C D
x y : C
f : x ⟶ y
inst✝ : IsIso f
z : D
⊢ 𝟙 (y ⊙ₗ z) = 𝟙 (y ⊙ₗ z)

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Action.Basic

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 C
inst✝ : MonoidalRightAction C D
x y : D
f : x ⟶ y
⊢ f ⊵ᵣ 𝟙_ C = (f ⊵ᵣ 𝟙_ C ≫ (ρᵣ y).hom) ≫ (ρᵣ y).inv

Tactic:
]

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 C
inst✝ : MonoidalRightAction C D
x y : D
f : x ⟶ y
⊢ f ⊵ᵣ 𝟙_ C = (f ⊵ᵣ 𝟙_ C ≫ (ρᵣ y).hom) ≫ (ρᵣ y).inv
Module: Mathlib.CategoryTheory.Monoidal.Action.Basic

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 C
inst✝ : MonoidalRightAction C D
z z' : D
f : z ⟶ z'
x y : C
⊢ f ⊙ᵣₘ 𝟙 (x ⊗ y) = ((f ⊙ᵣₘ 𝟙 x ⊗ₘ 𝟙 y) ≫ (αᵣ z' x y).hom) ≫ (αᵣ z' x y).inv

Tactic:
]

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 C
inst✝ : MonoidalRightAction C D
z z' : D
f : z ⟶ z'
x y : C
⊢ f ⊙ᵣₘ 𝟙 (x ⊗ y) = ((f ⊙ᵣₘ 𝟙 x ⊗ₘ 𝟙 y) ≫ (αᵣ z' x y).hom) ≫ (αᵣ z' x y).inv
Module: Mathlib.CategoryTheory.Monoidal.Action.Basic

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 C
inst✝ : MonoidalRightAction C D
d₁ d₂ : D
c₁ c₂ c₃ c₄ : C
f : d₁ ⟶ d₂
g : c₁ ⟶ c₂
h : c₃ ⟶ c₄
⊢ (αᵣ d₁ c₁ c₃).hom ≫ ((f ⊙ᵣₘ g) ⊙ᵣₘ h) = (αᵣ d₁ c₁ c₃).hom ≫ ((f ⊙ᵣₘ g) ⊙ᵣₘ h)

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Action.Basic

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 C
inst✝ : MonoidalRightAction C D
d d' : D
f : d ⟶ d'
⊢ f ⊵ᵣ 𝟙_ C ≫ (ρᵣ d').hom = f ⊵ᵣ 𝟙_ C ≫ (ρᵣ d').hom

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Action.Basic

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 C
inst✝ : MonoidalRightAction C D
x : D
y z : C
f : y ≅ z
⊢ 𝟙 (x ⊙ᵣ y) = 𝟙 (x ⊙ᵣ y)

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Action.Basic

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 C
inst✝ : MonoidalRightAction C D
x y : D
f : x ≅ y
z : C
⊢ 𝟙 (x ⊙ᵣ z) = 𝟙 (x ⊙ᵣ z)

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Action.Basic

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 C
inst✝ : MonoidalRightAction C D
x : D
y z : C
f : y ≅ z
⊢ 𝟙 (x ⊙ᵣ z) = 𝟙 (x ⊙ᵣ z)

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Action.Basic

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 C
inst✝ : MonoidalRightAction C D
x y : D
f : x ≅ y
z : C
⊢ 𝟙 (y ⊙ᵣ z) = 𝟙 (y ⊙ᵣ z)

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Action.Basic

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 C
inst✝¹ : MonoidalRightAction C D
x : D
y z : C
f : y ⟶ z
inst✝ : IsIso f
⊢ 𝟙 (x ⊙ᵣ y) = 𝟙 (x ⊙ᵣ y)

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Action.Basic

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 C
inst✝¹ : MonoidalRightAction C D
x y : D
f : x ⟶ y
inst✝ : IsIso f
z : C
⊢ 𝟙 (x ⊙ᵣ z) = 𝟙 (x ⊙ᵣ z)

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Action.Basic

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 C
inst✝¹ : MonoidalRightAction C D
x : D
y z : C
f : y ⟶ z
inst✝ : IsIso f
⊢ 𝟙 (x ⊙ᵣ z) = 𝟙 (x ⊙ᵣ z)

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Action.Basic

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 C
inst✝¹ : MonoidalRightAction C D
x y : D
f : x ⟶ y
inst✝ : IsIso f
z : C
⊢ 𝟙 (y ⊙ᵣ z) = 𝟙 (y ⊙ᵣ z)

Tactic:
]

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
M : Bimon C
⊢ (λ_ M.X.X).inv = (λ_ M.X.X).inv

Tactic:
]

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
M : Bimon C
⊢ (ρ_ M.X.X).inv = (ρ_ M.X.X).inv

Tactic:
]

Goal state after:
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
x✝ : ∀ (d d' : D), IsIso (L.map (adj.unit.app d ▷ d'))
h : ∀ (d d' : D), IsIso (L.map (adj.unit.app d ▷ d')) := x✝
d d' : D
this : d ◁ adj.unit.app d' = ((β_ d ((𝟭 D).obj d')).hom ≫ (adj.unit.app d' ⊗ₘ 𝟙 d)) ≫ (β_ d ((L ⋙ R).obj d')).inv
⊢ IsIso (L.map (d ◁ adj.unit.app d'))

Tactic:
]

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
x✝ : ∀ (d d' : D), IsIso (L.map (adj.unit.app d ▷ d'))
h : ∀ (d d' : D), IsIso (L.map (adj.unit.app d ▷ d')) := x✝
d d' : D
this : d ◁ adj.unit.app d' = ((β_ d ((𝟭 D).obj d')).hom ≫ (adj.unit.app d' ⊗ₘ 𝟙 d)) ≫ (β_ d ((L ⋙ R).obj d')).inv
⊢ IsIso (L.map (d ◁ adj.unit.app d'))