mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Preserves.BifunctorCokernel

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C : Type u_3
inst✝¹¹ : Category.{v_1, u_1} C₁
inst✝¹⁰ : Category.{v_2, u_2} C₂
inst✝⁹ : Category.{v_3, u_3} C
inst✝⁸ : HasZeroMorphisms C₁
inst✝⁷ : HasZeroMorphisms C₂
inst✝⁶ : HasZeroMorphisms C
X₁ Y₁ : C₁
f₁ : X₁ ⟶ Y₁
c₁ : CokernelCofork f₁
hc₁ : IsColimit c₁
X₂ Y₂ : C₂
f₂ : X₂ ⟶ Y₂
c₂ : CokernelCofork f₂
hc₂ : IsColimit c₂
F : C₁ ⥤ C₂ ⥤ C
inst✝⁵ : (F.obj c₁.pt).PreservesZeroMorphisms
inst✝⁴ : F.PreservesZeroMorphisms
inst✝³ : PreservesColimit (parallelPair f₂ 0) (F.obj c₁.pt)
inst✝² : PreservesColimit (parallelPair f₁ 0) (F.flip.obj Y₂)
inst✝¹ : HasBinaryCoproduct ((F.obj X₁).obj Y₂) ((F.obj Y₁).obj X₂)
inst✝ : PreservesColimit (parallelPair f₁ 0) (F.flip.obj X₂)
s : Cofork (coprod.desc ((F.map f₁).app Y₂) ((F.obj Y₁).map f₂)) 0
m : (c₁.mapBifunctor c₂ F).pt ⟶ s.pt
hm : Cofork.π (c₁.mapBifunctor c₂ F) ≫ m = s.π
⊢ (F.map (Cofork.π c₁)).app Y₂ ≫ (F.obj c₁.pt).map (Cofork.π c₂) ≫ m =
    ((F.map (Cofork.π c₁)).app Y₂ ≫ (F.obj c₁.pt).map (Cofork.π c₂)) ≫ m

Tactic:
Category.assoc

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
C : Type u_3
inst✝¹¹ : Category.{v_1, u_1} C₁
inst✝¹⁰ : Category.{v_2, u_2} C₂
inst✝⁹ : Category.{v_3, u_3} C
inst✝⁸ : HasZeroMorphisms C₁
inst✝⁷ : HasZeroMorphisms C₂
inst✝⁶ : HasZeroMorphisms C
X₁ Y₁ : C₁
f₁ : X₁ ⟶ Y₁
c₁ : CokernelCofork f₁
hc₁ : IsColimit c₁
X₂ Y₂ : C₂
f₂ : X₂ ⟶ Y₂
c₂ : CokernelCofork f₂
hc₂ : IsColimit c₂
F : C₁ ⥤ C₂ ⥤ C
inst✝⁵ : (F.obj c₁.pt).PreservesZeroMorphisms
inst✝⁴ : F.PreservesZeroMorphisms
inst✝³ : PreservesColimit (parallelPair f₂ 0) (F.obj c₁.pt)
inst✝² : PreservesColimit (parallelPair f₁ 0) (F.flip.obj Y₂)
inst✝¹ : HasBinaryCoproduct ((F.obj X₁).obj Y₂) ((F.obj Y₁).obj X₂)
inst✝ : PreservesColimit (parallelPair f₁ 0) (F.flip.obj X₂)
s : Cofork (coprod.desc ((F.map f₁).app Y₂) ((F.obj Y₁).map f₂)) 0
m : (c₁.mapBifunctor c₂ F).pt ⟶ s.pt
hm : Cofork.π (c₁.mapBifunctor c₂ F) ≫ m = s.π
⊢ (F.map (Cofork.π c₁)).app Y₂ ≫ (F.obj c₁.pt).map (Cofork.π c₂) ≫ m =
    (F.map (Cofork.π c₁)).app Y₂ ≫ (F.obj c₁.pt).map (Cofork.π c₂) ≫ m
Module: Mathlib.CategoryTheory.Limits.Shapes.PiProd

Goal state before:
pp: C : Type u_1
I : Type u_2
inst✝⁷ : Category.{v_1, u_1} C
X Y : I → C
f : (i : I) → X i ⟶ Y i
P : I → Prop
inst✝⁶ : HasProduct X
inst✝⁵ : HasProduct Y
inst✝⁴ : HasProduct fun i ↦ X ↑i
inst✝³ : HasProduct fun i ↦ X ↑i
inst✝² : HasProduct fun i ↦ Y ↑i
inst✝¹ : HasProduct fun i ↦ Y ↑i
inst✝ : (i : I) → Decidable (P i)
x✝¹ : BinaryFan (∏ᶜ fun i ↦ X ↑i) (∏ᶜ fun i ↦ X ↑i)
x✝ : x✝¹.pt ⟶ ∏ᶜ X
h₁ : (x✝ ≫ map' Subtype.val fun x ↦ 𝟙 (X ↑x)) = x✝¹.fst
h₂ : (x✝ ≫ map' Subtype.val fun x ↦ 𝟙 (X ↑x)) = x✝¹.snd
b : I
⊢ x✝ ≫ π X b =
    (lift fun b ↦
        if h : P b then x✝¹.π.app { as := WalkingPair.left } ≫ π (fun i ↦ X ↑i) ⟨b, h⟩
        else x✝¹.π.app { as := WalkingPair.right } ≫ π (fun i ↦ X ↑i) ⟨b, h⟩) ≫
      π X b

Tactic:
by_cases h : P b
      · simp [← h₁, dif_pos h]
      · simp [← h₂, dif_neg h]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X₁ X₂ X₃ S : C
f₁ : X₁ ⟶ S
f₂ : X₂ ⟶ S
f₃ : X₃ ⟶ S
h₁₂ : ChosenPullback f₁ f₂
h₂₃ : ChosenPullback f₂ f₃
h₁₃ : ChosenPullback f₁ f₃
h : ChosenPullback₃ h₁₂ h₂₃ h₁₃
Y : C
g₁ : Y ⟶ X₁
g₂ : Y ⟶ X₂
g₃ : Y ⟶ X₃
b : Y ⟶ S
hg₁ : g₁ ≫ f₁ = b
hg₂ : g₂ ≫ f₂ = b
hg₃ : g₃ ≫ f₃ = b
⊢ ∃ φ, φ ≫ h.p₁ = g₁ ∧ φ ≫ h.p₂ = g₂ ∧ φ ≫ h.p₃ = g₃

Tactic:
obtain ⟨φ₁₂, w₁, w₂⟩ := h₁₂.isPullback.exists_lift g₁ g₂ (by cat_disch)

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X₁ X₂ X₃ S : C
f₁ : X₁ ⟶ S
f₂ : X₂ ⟶ S
f₃ : X₃ ⟶ S
h₁₂ : ChosenPullback f₁ f₂
h₂₃ : ChosenPullback f₂ f₃
h₁₃ : ChosenPullback f₁ f₃
h : ChosenPullback₃ h₁₂ h₂₃ h₁₃
Y : C
g₁ : Y ⟶ X₁
g₂ : Y ⟶ X₂
g₃ : Y ⟶ X₃
b : Y ⟶ S
hg₁ : g₁ ≫ f₁ = b
hg₂ : g₂ ≫ f₂ = b
hg₃ : g₃ ≫ f₃ = b
φ₁₂ : Y ⟶ h₁₂.pullback
w₁ : φ₁₂ ≫ h₁₂.p₁ = g₁
w₂ : φ₁₂ ≫ h₁₂.p₂ = g₂
⊢ ∃ φ, φ ≫ h.p₁ = g₁ ∧ φ ≫ h.p₂ = g₂ ∧ φ ≫ h.p₃ = g₃
Module: Mathlib.CategoryTheory.Limits.Types.PreservesLimit

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
J : Type u'
inst✝¹ : Category.{v', u'} J
inst✝ : LocallySmall.{w, v, u} C
F : J ⥤ Cᵒᵖ
c : Cone F
c' : Cocone (F.leftOp ⋙ shrinkYoneda.{w, v, u})
hc : IsLimit c
hc' : IsColimit c'
P : Cᵒᵖ ⥤ Type w
f : c'.pt ⟶ P
X X' : J
g : X ⟶ X'
⊢ (ConcreteCategory.hom (P.map (F.map g))) (shrinkYonedaEquiv (c'.ι.app (op X) ≫ f)) =
    shrinkYonedaEquiv ((shrinkYoneda.{w, v, u}.map (F.map g).unop ≫ c'.ι.app (op X)) ≫ f)

Tactic:
Category.assoc

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
J : Type u'
inst✝¹ : Category.{v', u'} J
inst✝ : LocallySmall.{w, v, u} C
F : J ⥤ Cᵒᵖ
c : Cone F
c' : Cocone (F.leftOp ⋙ shrinkYoneda.{w, v, u})
hc : IsLimit c
hc' : IsColimit c'
P : Cᵒᵖ ⥤ Type w
f : c'.pt ⟶ P
X X' : J
g : X ⟶ X'
⊢ (ConcreteCategory.hom (P.map (F.map g))) (shrinkYonedaEquiv (c'.ι.app (op X) ≫ f)) =
    shrinkYonedaEquiv (shrinkYoneda.{w, v, u}.map (F.map g).unop ≫ c'.ι.app (op X) ≫ f)
Module: Mathlib.CategoryTheory.Monoidal.Free.Basic

Goal state before:
pp: case assoc
C : Type u
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : MonoidalCategory D
f✝¹ : C → D
X Y : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
f g : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
X✝ Y✝ U✝ V✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
f✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
g✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
h✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ (projectMapAux f✝¹ f✝ ≫ projectMapAux f✝¹ g✝) ≫ projectMapAux f✝¹ h✝ =
    projectMapAux f✝¹ f✝ ≫ projectMapAux f✝¹ g✝ ≫ projectMapAux f✝¹ h✝

Tactic:
Category.assoc

Goal state after:
case assoc
C : Type u
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : MonoidalCategory D
f✝¹ : C → D
X Y : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
f g : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
X✝ Y✝ U✝ V✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
f✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
g✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
h✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ projectMapAux f✝¹ f✝ ≫ projectMapAux f✝¹ g✝ ≫ projectMapAux f✝¹ h✝ =
    projectMapAux f✝¹ f✝ ≫ projectMapAux f✝¹ g✝ ≫ projectMapAux f✝¹ h✝
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 ⊗ₘ 𝟙 Y)) ≫ (f ⊗ₘ 𝟙 Y) = (Δ ≫ (𝟙 X ⊗ₘ f)) ≫ (f ⊗ₘ 𝟙 Y)

Tactic:
by
      rw [copy_comp_natural (h := by rw [IsIso.hom_inv_id]; infer_instance)]
      simp

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
⊢ (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:
Category.assoc

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: case inst
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✝¹ : MonadicRightAdjoint G
A B : D
f g : A ⟶ B
inst✝ : G.IsSplitPair f g
⊢ PreservesColimit (parallelPair f g ⋙ G) (monadicLeftAdjoint G ⋙ G)

pp: case inst
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✝¹ : MonadicRightAdjoint G
A B : D
f g : A ⟶ B
inst✝ : G.IsSplitPair f g
⊢ PreservesColimit ((parallelPair f g ⋙ G) ⋙ monadicLeftAdjoint G ⋙ G) (monadicLeftAdjoint G ⋙ G)

Tactic:
all_goals
    apply @preservesColimit_of_iso_diagram _ _ _ _ _ _ _ _ _ (diagramIsoParallelPair.{v₁} _).symm ?_
    dsimp
    infer_instance

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
⊢ Δ.hom ≫ ε ▷ M.X.X = (λ_ M.X.X).inv

Tactic:
← BimonObjAux_comul,

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
M : Bimon C
⊢ Δ ≫ ε ▷ M.X.X = (λ_ M.X.X).inv
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
⊢ Δ.hom ≫ M.X.X ◁ ε = (ρ_ M.X.X).inv

Tactic:
← BimonObjAux_comul,

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
M : Bimon C
⊢ Δ ≫ M.X.X ◁ ε = (ρ_ M.X.X).inv
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
⊢ Δ.hom ≫ M.X.X ◁ Δ.hom = Δ.hom ≫ Δ.hom ▷ M.X.X ≫ (α_ M.X.X M.X.X M.X.X).hom

Tactic:
← BimonObjAux_comul,

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
M : Bimon C
⊢ Δ ≫ M.X.X ◁ Δ = Δ ≫ Δ ▷ M.X.X ≫ (α_ M.X.X M.X.X M.X.X).hom
Module: Mathlib.CategoryTheory.Monoidal.Bimod

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

pp: case a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : HasCoequalizers C
R S T : Mon C
P : Bimod R S
Q : Bimod S T
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
| R.X ◁ actLeft P Q

pp: case a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : HasCoequalizers C
R S T : Mon C
P : Bimod R S
Q : Bimod S T
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
| actLeft P Q

Tactic:
associator_naturality_right

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

case a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : HasCoequalizers C
R S T : Mon C
P : Bimod R S
Q : Bimod S T
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
| R.X ◁ actLeft P Q

case a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : HasCoequalizers C
R S T : Mon C
P : Bimod R S
Q : Bimod S T
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
| actLeft P Q
Module: Mathlib.CategoryTheory.Monoidal.Mod

Goal state before:
pp: C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalLeftAction C D
M : C
inst✝³ : MonObj M
X : D
N : C
inst✝² : MonObj N
e₁ : M ≅ N
inst✝¹ : IsMonHom e₁.hom
Y : D
e₂ : X ≅ Y
inst✝ : ModObj M X
⊢ (e₁.inv ⊗ₘ e₁.inv) ⊵ₗ Y ≫ (M ⊗ M) ⊴ₗ e₂.inv ≫ μ ⊵ₗ X = ((e₁.inv ⊗ₘ e₁.inv) ⊵ₗ Y ≫ (M ⊗ M) ⊴ₗ e₂.inv) ≫ μ ⊵ₗ X

Tactic:
Category.assoc

Goal state after:
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalLeftAction C D
M : C
inst✝³ : MonObj M
X : D
N : C
inst✝² : MonObj N
e₁ : M ≅ N
inst✝¹ : IsMonHom e₁.hom
Y : D
e₂ : X ≅ Y
inst✝ : ModObj M X
⊢ (e₁.inv ⊗ₘ e₁.inv) ⊵ₗ Y ≫ (M ⊗ M) ⊴ₗ e₂.inv ≫ μ ⊵ₗ X = (e₁.inv ⊗ₘ e₁.inv) ⊵ₗ Y ≫ (M ⊗ M) ⊴ₗ e₂.inv ≫ μ ⊵ₗ X
Module: Mathlib.CategoryTheory.Monoidal.Mod

Goal state before:
pp: C : Type u₁
inst✝¹² : Category.{v₁, u₁} C
inst✝¹¹ : MonoidalCategory C
D : Type u₂
inst✝¹⁰ : Category.{v₂, u₂} D
inst✝⁹ : MonoidalLeftAction C D
M' N' O' : D
A✝¹ : C
inst✝⁸ : MonObj A✝¹
M✝¹ N O : D
inst✝⁷ : ModObj A✝¹ M✝¹
inst✝⁶ : ModObj A✝¹ N
inst✝⁵ : ModObj A✝¹ O
A✝ : C
inst✝⁴ : MonObj A✝
M✝ : Mod D A✝
A B : C
inst✝³ : MonObj A
inst✝² : MonObj B
f : A ⟶ B
inst✝¹ : IsMonHom f
M : D
inst✝ : ModObj B M
⊢ ((f ▷ A ≫ B ◁ f) ≫ μ) ⊵ₗ M ≫ γ = (f ▷ A ≫ B ◁ f ≫ μ) ⊵ₗ M ≫ γ

Tactic:
Category.assoc

Goal state after:
C : Type u₁
inst✝¹² : Category.{v₁, u₁} C
inst✝¹¹ : MonoidalCategory C
D : Type u₂
inst✝¹⁰ : Category.{v₂, u₂} D
inst✝⁹ : MonoidalLeftAction C D
M' N' O' : D
A✝¹ : C
inst✝⁸ : MonObj A✝¹
M✝¹ N O : D
inst✝⁷ : ModObj A✝¹ M✝¹
inst✝⁶ : ModObj A✝¹ N
inst✝⁵ : ModObj A✝¹ O
A✝ : C
inst✝⁴ : MonObj A✝
M✝ : Mod D A✝
A B : C
inst✝³ : MonObj A
inst✝² : MonObj B
f : A ⟶ B
inst✝¹ : IsMonHom f
M : D
inst✝ : ModObj B M
⊢ (f ▷ A ≫ B ◁ f ≫ μ) ⊵ₗ M ≫ γ = (f ▷ A ≫ B ◁ f ≫ μ) ⊵ₗ M ≫ γ
Module: Mathlib.CategoryTheory.Monoidal.Bimod

Goal state before:
pp: case a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : HasCoequalizers C
R S T : Mon C
P : Bimod R S
Q : Bimod S T
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
| (P.X ⊗ Q.X) ◁ η ≫ (α_ P.X Q.X T.X).hom

pp: case a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : HasCoequalizers C
R S T : Mon C
P : Bimod R S
Q : Bimod S T
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
| P.X ◁ Q.actRight

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

Tactic:
associator_naturality_right

Goal state after:
case a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : HasCoequalizers C
R S T : Mon C
P : Bimod R S
Q : Bimod S T
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
| (α_ P.X Q.X (𝟙_ C)).hom ≫ P.X ◁ Q.X ◁ η

case a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : HasCoequalizers C
R S T : Mon C
P : Bimod R S
Q : Bimod S T
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
| P.X ◁ Q.actRight

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

Goal state before:
pp: case a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : HasCoequalizers C
R S T : Mon C
P : Bimod R S
Q : Bimod S T
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
| (P.X ⊗ Q.X) ◁ μ ≫ (α_ P.X Q.X T.X).hom

pp: case a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : HasCoequalizers C
R S T : Mon C
P : Bimod R S
Q : Bimod S T
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
| P.X ◁ Q.actRight

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

Tactic:
associator_naturality_right

Goal state after:
case a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : HasCoequalizers C
R S T : Mon C
P : Bimod R S
Q : Bimod S T
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
| (α_ P.X Q.X (T.X ⊗ T.X)).hom ≫ P.X ◁ Q.X ◁ μ

case a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : HasCoequalizers C
R S T : Mon C
P : Bimod R S
Q : Bimod S T
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
| P.X ◁ Q.actRight

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

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
inst✝ : MonoidalClosed V
F G H : C ⥤ V
ℌ : DayConvolutionInternalHom F G H
G' H' : C ⥤ V
f✝ : G ⟶ G'
ℌ' : DayConvolutionInternalHom F G' H'
c c' : C
f : c ⟶ c'
j : (multicospanShapeEnd C).L
⊢ H.map f ≫ ℌ.π c' j ≫ (ihom (F.obj j)).map (f✝.app (j ⊗ c')) =
    Wedge.IsLimit.lift (ℌ'.isLimitWedge c) (fun j ↦ ℌ.π c j ≫ (ihom (F.obj j)).map (f✝.app (j ⊗ c))) ⋯ ≫
      Multifork.ι (Wedge.mk (H'.obj c) (ℌ'.π c) ⋯) j ≫ (ihom (F.obj j)).map (G'.map (j ◁ f))

Tactic:
Wedge.IsLimit.lift_ι_assoc (ℌ'.isLimitWedge c)

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
inst✝ : MonoidalClosed V
F G H : C ⥤ V
ℌ : DayConvolutionInternalHom F G H
G' H' : C ⥤ V
f✝ : G ⟶ G'
ℌ' : DayConvolutionInternalHom F G' H'
c c' : C
f : c ⟶ c'
j : (multicospanShapeEnd C).L
⊢ H.map f ≫ ℌ.π c' j ≫ (ihom (F.obj j)).map (f✝.app (j ⊗ c')) =
    (ℌ.π c j ≫ (ihom (F.obj j)).map (f✝.app (j ⊗ c))) ≫ (ihom (F.obj j)).map (G'.map (j ◁ f))
Module: Mathlib.CategoryTheory.Monoidal.Hopf_

Goal state before:
pp: case hac
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
inst✝³ : BraidedCategory C
A B : C
inst✝² : HopfObj A
inst✝¹ : HopfObj B
f : A ⟶ B
inst✝ : IsBimonHom f
⊢ Δ ≫ f ▷ A ≫ B ◁ 𝒮 ≫ B ◁ f ≫ μ = ε ≫ η

Tactic:
slice_lhs 2 3 =>
      rw [← whisker_exchange]

Goal state after:
case hac
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
inst✝³ : BraidedCategory C
A B : C
inst✝² : HopfObj A
inst✝¹ : HopfObj B
f : A ⟶ B
inst✝ : IsBimonHom f
⊢ Δ ≫ ((A ◁ 𝒮 ≫ f ▷ A) ≫ B ◁ f) ≫ μ = ε ≫ η
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
⊢ η ≫ 𝒮 = η

Tactic:
have := (rfl : η[A] ≫ Δ[A] ≫ (𝒮[A] ▷ A) ≫ μ[A] = _)

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
this : η ≫ Δ ≫ 𝒮 ▷ A ≫ μ = η ≫ Δ ≫ 𝒮 ▷ A ≫ μ
⊢ η ≫ 𝒮 = η
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
comm : (β_ A A).hom ≫ μ = μ
⊢ 𝒮 ≫ 𝒮 = 𝟙 A

Tactic:
by
  -- Again, it is a "left inverse equals right inverse" argument in the convolution monoid.
  apply left_inv_eq_right_inv
    (M := Conv A A)
    (a := 𝒮[A])
  · -- Unfold the algebra structure in the convolution monoid,
    -- then `simp?`.
    rw [Conv.mul_eq, Conv.one_eq]
    simp only [comp_whiskerRight, Category.assoc]
    rw [← comm, ← tensorHom_def_assoc, ← mul_antipode]
    simp
  · rw [Conv.mul_eq, Conv.one_eq]
    simp

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

Goal state before:
pp: case a.a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : HasCoequalizers C
R S : Mon C
P : Bimod R S
| P.actRight ≫ (ρ_ P.X).inv

pp: case a.a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : HasCoequalizers C
R S : Mon C
P : Bimod R S
| P.X ◁ η

pp: case a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : HasCoequalizers C
R S : Mon C
P : Bimod R S
| coequalizer.π (P.actRight ▷ S.X) ((α_ P.X S.X S.X).hom ≫ P.X ◁ μ)

Tactic:
rw [rightUnitor_inv_naturality]

Goal state after:
case a.a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : HasCoequalizers C
R S : Mon C
P : Bimod R S
| (ρ_ (P.X ⊗ S.X)).inv ≫ P.actRight ▷ 𝟙_ C

case a.a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : HasCoequalizers C
R S : Mon C
P : Bimod R S
| P.X ◁ η

case a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : HasCoequalizers C
R S : Mon C
P : Bimod R S
| coequalizer.π (P.actRight ▷ S.X) ((α_ P.X S.X S.X).hom ≫ P.X ◁ μ)
Module: Mathlib.CategoryTheory.Monoidal.Bimod

Goal state before:
pp: case a.a.a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : HasCoequalizers C
R S : Mon C
P : Bimod R S
| (P.X ⊗ S.X) ◁ η ≫ (α_ P.X S.X S.X).hom

pp: case a.a.a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : HasCoequalizers C
R S : Mon C
P : Bimod R S
| P.X ◁ μ

pp: case a.a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : HasCoequalizers C
R S : Mon C
P : Bimod R S
| coequalizer.π (P.actRight ▷ S.X) ((α_ P.X S.X S.X).hom ≫ P.X ◁ μ)

pp: case a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : HasCoequalizers C
R S : Mon C
P : Bimod R S
| (ρ_ (P.X ⊗ S.X)).inv

Tactic:
associator_naturality_right

Goal state after:
case a.a.a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : HasCoequalizers C
R S : Mon C
P : Bimod R S
| (α_ P.X S.X (𝟙_ C)).hom ≫ P.X ◁ S.X ◁ η

case a.a.a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : HasCoequalizers C
R S : Mon C
P : Bimod R S
| P.X ◁ μ

case a.a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : HasCoequalizers C
R S : Mon C
P : Bimod R S
| coequalizer.π (P.actRight ▷ S.X) ((α_ P.X S.X S.X).hom ≫ P.X ◁ μ)

case a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : HasCoequalizers C
R S : Mon C
P : Bimod R S
| (ρ_ (P.X ⊗ S.X)).inv
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:
rw [IsComonHom.hom_comul (α.app x).hom]

Goal state after:
Module: Mathlib.CategoryTheory.Presentable.Dense

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalAccessibleCategory C κ
X : C
⊢ IsCardinalFiltered (CostructuredArrow (isCardinalPresentable C κ).ι X) κ

Tactic:
obtain ⟨J, _, _, ⟨p⟩⟩ :=
    (isCardinalFilteredGenerator_isCardinalPresentable C κ).exists_colimitsOfShape X

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalAccessibleCategory C κ
X : C
J : Type w
w✝¹ : SmallCategory J
w✝ : IsCardinalFiltered J κ
p : (isCardinalPresentable C κ).ColimitOfShape J X
⊢ IsCardinalFiltered (CostructuredArrow (isCardinalPresentable C κ).ι X) κ