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✝ : MonoidalRightAction C D
c✝ c'✝ : Cᵒᵖ
d✝ d'✝ : Dᵒᵖ
f : unop d'✝ ⟶ unop d✝
g : unop c'✝ ⟶ unop c✝
⊢ (Quiver.Hom.unop (op f) ⊙ᵣₘ Quiver.Hom.unop (op g)).op.unop =
    ((Quiver.Hom.unop (op f) ⊵ᵣ unop c✝).op ≫ (unop d'✝ ⊴ᵣ Quiver.Hom.unop (op g)).op).unop

Tactic:
simpa using

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 : unop d'✝ ⟶ unop d✝
g : unop c'✝ ⟶ unop c✝
⊢ f ⊙ᵣₘ g = f ⊵ᵣ unop c'✝ ≫ unop d✝ ⊴ᵣ g
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.op = ((f.op ⊵ᵣ op c✝).unop ≫ (op d'✝ ⊴ᵣ g.op).unop).op

Tactic:
simpa using

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 = f.op ⊵ᵣ op c'✝ ≫ op d✝ ⊴ᵣ g.op
Module: Mathlib.CategoryTheory.Monoidal.Internal.Limits

Goal state before:
pp: J : Type w
inst✝² : Category.{v_1, w} J
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
F : J ⥤ Mon C
c : Cone (F ⋙ forget C)
hc : IsLimit c
s : Cone F
m : s.pt ⟶ (limitCone F c hc).pt
w : ∀ (j : J), m ≫ (limitCone F c hc).π.app j = s.π.app j
j : J
⊢ m.hom ≫ c.π.app j = { hom := hc.lift ((forget C).mapCone s), isMonHom_hom := ⋯ }.hom ≫ c.π.app j

Tactic:
simpa using

Goal state after:
J : Type w
inst✝² : Category.{v_1, w} J
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
F : J ⥤ Mon C
c : Cone (F ⋙ forget C)
hc : IsLimit c
s : Cone F
m : s.pt ⟶ (limitCone F c hc).pt
w : ∀ (j : J), m ≫ (limitCone F c hc).π.app j = s.π.app j
j : J
⊢ m.hom ≫ c.π.app j = (s.π.app j).hom
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
A B : C
inst✝⁵ : MonObj A
inst✝⁴ : MonObj B
f : A ⟶ B
inst✝³ : IsMonHom f
M N : D
inst✝² : ModObj B M
inst✝¹ : ModObj B N
g : M ⟶ N
inst✝ : IsModHom B g
this✝ : ModObj A M := scalarRestriction f M
this : ModObj A N := scalarRestriction f N
⊢ γ ≫ g = A ⊴ₗ g ≫ γ

Tactic:
simpa using

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
A B : C
inst✝⁵ : MonObj A
inst✝⁴ : MonObj B
f : A ⟶ B
inst✝³ : IsMonHom f
M N : D
inst✝² : ModObj B M
inst✝¹ : ModObj B N
g : M ⟶ N
inst✝ : IsModHom B g
this✝ : ModObj A M := scalarRestriction f M
this : ModObj A N := scalarRestriction f N
⊢ f ⊵ₗ M ≫ B ⊴ₗ g ≫ γ = A ⊴ₗ g ≫ f ⊵ₗ N ≫ γ
Module: Mathlib.CategoryTheory.Monoidal.Ring

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : BraidedCategory C
R : C
inst✝ : RingObj R
X✝ X : C
a : X ⟶ R
⊢ 0 * a = 0

Tactic:
simpa using

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : BraidedCategory C
R : C
inst✝ : RingObj R
X✝ X : C
a : X ⟶ R
⊢ 0 * a = 0
Module: Mathlib.CategoryTheory.Monoidal.Ring

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : BraidedCategory C
R : C
inst✝ : RingObj R
X✝ X : C
a : X ⟶ R
⊢ a * 0 = 0

Tactic:
simpa using

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : BraidedCategory C
R : C
inst✝ : RingObj R
X✝ X : C
a : X ⟶ R
⊢ a * 0 = 0
Module: Mathlib.CategoryTheory.Subterminal

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
A : C
hA : IsSubterminal A
inst✝ : HasBinaryProduct A A
⊢ A ⨯ A ≅ A

Tactic:
letI := IsSubterminal.isIso_diag hA
  apply (asIso (diag A)).symm

Goal state after:
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 G : C ⥤ V
inst✝ : DayConvolution F G
ℌ : DayConvolutionInternalHom F (F ⊛ G) H
c c' : C
f : c ⟶ c'
⊢ G.map f ≫
      Wedge.IsLimit.lift (ℌ.isLimitWedge c')
        (fun c'_1 ↦ MonoidalClosed.curry ((DayConvolution.unit F G).app (c'_1, c'))) ⋯ =
    Wedge.IsLimit.lift (ℌ.isLimitWedge c) (fun c' ↦ MonoidalClosed.curry ((DayConvolution.unit F G).app (c', c))) ⋯ ≫
      H.map f

Tactic:
apply Wedge.IsLimit.hom_ext <| ℌ.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 G : C ⥤ V
inst✝ : DayConvolution F G
ℌ : DayConvolutionInternalHom F (F ⊛ G) H
c c' : C
f : c ⟶ c'
⊢ ∀ (j : (multicospanShapeEnd C).L),
    (G.map f ≫
          Wedge.IsLimit.lift (ℌ.isLimitWedge c')
            (fun c'_1 ↦ MonoidalClosed.curry ((DayConvolution.unit F G).app (c'_1, c'))) ⋯) ≫
        Multifork.ι (Wedge.mk (H.obj c') (ℌ.π c') ⋯) j =
      (Wedge.IsLimit.lift (ℌ.isLimitWedge c) (fun c' ↦ MonoidalClosed.curry ((DayConvolution.unit F G).app (c', c))) ⋯ ≫
          H.map f) ≫
        Multifork.ι (Wedge.mk (H.obj c') (ℌ.π c') ⋯) j
Module: Mathlib.CategoryTheory.Monoidal.Hopf_

Goal state before:
pp: case a
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 ◁ 𝒮 ≫ μ

pp: case a
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

Tactic:
antipode_right

Goal state after:
case a
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
| ε ≫ η

case a
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
Module: Mathlib.CategoryTheory.Monoidal.Hopf_

Goal state before:
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 ◁ 𝒮 ≫ μ) ▷ A

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 A).hom

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

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 A).inv

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

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

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

Tactic:
antipode_right

Goal state after:
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.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.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
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.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
| Δ

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

Goal state before:
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 ◁ 𝒮 ≫ μ) ▷ A

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 ◁ μ

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
| μ

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

pp: case 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
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 ◁ 𝒮

Tactic:
antipode_right

Goal state after:
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.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj 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
| μ

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

case 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
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 ◁ 𝒮
Module: Mathlib.CategoryTheory.Monoidal.Hopf_

Goal state before:
pp: case 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
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
| (ρ_ A).hom

Tactic:
antipode_right

Goal state after:
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.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
| (ρ_ A).hom
Module: Mathlib.CategoryTheory.Monoidal.DayConvolution

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
V : Type u₂
inst✝³ : Category.{v₂, u₂} V
inst✝² : MonoidalCategory C
inst✝¹ : MonoidalCategory V
F G : C ⥤ V
inst✝ : DayConvolution F G
x x' y y' : C
f : x ⟶ x'
g : y ⟶ y'
⊢ (F.map f ⊗ₘ G.map g) ≫ (unit F G).app (x', y') = (unit F G).app (x, y) ≫ (F ⊛ G).map (f ⊗ₘ g)

Tactic:
simpa using

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
F G : C ⥤ V
inst✝ : DayConvolution F G
x x' y y' : C
f : x ⟶ x'
g : y ⟶ y'
⊢ F.map f ▷ G.obj y ≫ F.obj x' ◁ G.map g ≫ (unit F G).app (x', y') =
    (unit F G).app (x, y) ≫ (F ⊛ G).map (f ▷ y) ≫ (F ⊛ G).map (x' ◁ g)
Module: Mathlib.CategoryTheory.Monoidal.DayConvolution

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
V : Type u₂
inst✝³ : Category.{v₂, u₂} V
inst✝² : MonoidalCategory C
inst✝¹ : MonoidalCategory V
F G : C ⥤ V
inst✝ : DayConvolution F G
x x' y : C
f : x ⟶ x'
⊢ F.map f ▷ G.obj y ≫ (unit F G).app (x', y) = (unit F G).app (x, y) ≫ (F ⊛ G).map (f ▷ y)

Tactic:
simpa using

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
F G : C ⥤ V
inst✝ : DayConvolution F G
x x' y : C
f : x ⟶ x'
⊢ F.map f ▷ G.obj y ≫ (unit F G).app (x', y) = (unit F G).app (x, y) ≫ (F ⊛ G).map (f ▷ y)
Module: Mathlib.CategoryTheory.Monoidal.DayConvolution

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
V : Type u₂
inst✝³ : Category.{v₂, u₂} V
inst✝² : MonoidalCategory C
inst✝¹ : MonoidalCategory V
F G : C ⥤ V
inst✝ : DayConvolution F G
x y y' : C
g : y ⟶ y'
⊢ F.obj x ◁ G.map g ≫ (unit F G).app (x, y') = (unit F G).app (x, y) ≫ (F ⊛ G).map (x ◁ g)

Tactic:
simpa using

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
F G : C ⥤ V
inst✝ : DayConvolution F G
x y y' : C
g : y ⟶ y'
⊢ F.obj x ◁ G.map g ≫ (unit F G).app (x, y') = (unit F G).app (x, y) ≫ (F ⊛ G).map (x ◁ g)
Module: Mathlib.CategoryTheory.Monoidal.DayConvolution

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
V : Type u₂
inst✝³ : Category.{v₂, u₂} V
inst✝² : MonoidalCategory C
inst✝¹ : MonoidalCategory V
F G : C ⥤ V
inst✝ : DayConvolution F G
c : C
v : V
f g : (F ⊛ G).obj c ⟶ v
h : ∀ {x y : C} (u : x ⊗ y ⟶ c), (unit F G).app (x, y) ≫ (F ⊛ G).map u ≫ f = (unit F G).app (x, y) ≫ (F ⊛ G).map u ≫ g
j : CostructuredArrow (tensor C) c
⊢ ((Functor.LeftExtension.mk (F ⊛ G) (unit F G)).coconeAt c).ι.app j ≫ f =
    ((Functor.LeftExtension.mk (F ⊛ G) (unit F G)).coconeAt c).ι.app j ≫ g

Tactic:
simpa using

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
F G : C ⥤ V
inst✝ : DayConvolution F G
c : C
v : V
f g : (F ⊛ G).obj c ⟶ v
h : ∀ {x y : C} (u : x ⊗ y ⟶ c), (unit F G).app (x, y) ≫ (F ⊛ G).map u ≫ f = (unit F G).app (x, y) ≫ (F ⊛ G).map u ≫ g
j : CostructuredArrow (tensor C) c
⊢ (unit F G).app j.left ≫ (F ⊛ G).map j.hom ≫ f = (unit F G).app j.left ≫ (F ⊛ G).map j.hom ≫ g
Module: Mathlib.CategoryTheory.Monoidal.Rigid.Braided

Goal state before:
pp: case e_g.e_f
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y : C
inst : ExactPairing X Y
⊢ ((((((α_ X Y X).inv ≫ (β_ X Y).hom ▷ X) ≫ inv (α_ Y X X).inv) ≫ inv (Y ◁ (β_ X X).inv)) ≫ inv (α_ Y X X).hom) ≫
        inv ((β_ Y X).inv ▷ X)) ≫
      inv (α_ X Y X).inv =
    (((inv (X ◁ (β_ Y X).inv) ≫ (α_ X X Y).inv) ≫ (β_ X X).hom ▷ Y) ≫ (α_ X X Y).hom) ≫ X ◁ (β_ X Y).hom

Tactic:
simpa using

Goal state after:
case e_g.e_f
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y : C
inst : ExactPairing X Y
⊢ (α_ X Y X).inv ≫
      (β_ X Y).hom ▷ X ≫ (α_ Y X X).hom ≫ Y ◁ (β_ X X).hom ≫ (α_ Y X X).inv ≫ (β_ Y X).hom ▷ X ≫ (α_ X Y X).hom =
    X ◁ (β_ Y X).hom ≫ (α_ X X Y).inv ≫ (β_ X X).hom ▷ Y ≫ (α_ X X Y).hom ≫ X ◁ (β_ X Y).hom
Module: Mathlib.CategoryTheory.Monoidal.Rigid.Braided

Goal state before:
pp: case e_g.e_a
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y : C
inst : ExactPairing X Y
⊢ (((Y ◁ (β_ X Y).hom ≫ inv (α_ Y Y X).hom) ≫ inv ((β_ Y Y).inv ▷ X)) ≫ inv (α_ Y Y X).inv) ≫ inv (Y ◁ (β_ Y X).inv) =
    (((((inv (α_ Y X Y).hom ≫ inv ((β_ Y X).inv ▷ Y)) ≫ (α_ X Y Y).hom) ≫ X ◁ (β_ Y Y).hom) ≫ (α_ X Y Y).inv) ≫
        (β_ X Y).hom ▷ Y) ≫
      (α_ Y X Y).hom

Tactic:
simpa using

Goal state after:
case e_g.e_a
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y : C
inst : ExactPairing X Y
⊢ Y ◁ (β_ X Y).hom ≫ (α_ Y Y X).inv ≫ (β_ Y Y).hom ▷ X ≫ (α_ Y Y X).hom ≫ Y ◁ (β_ Y X).hom =
    (α_ Y X Y).inv ≫
      (β_ Y X).hom ▷ Y ≫ (α_ X Y Y).hom ≫ X ◁ (β_ Y Y).hom ≫ (α_ X Y Y).inv ≫ (β_ X Y).hom ▷ Y ≫ (α_ Y X Y).hom
Module: Mathlib.CategoryTheory.Monoidal.DayConvolution

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
V : Type u₂
inst✝³ : Category.{v₂, u₂} V
inst✝² : MonoidalCategory C
inst✝¹ : MonoidalCategory V
U : C ⥤ V
inst✝ : DayConvolutionUnit U
c : C
v : V
g h : U.obj c ⟶ v
e : ∀ (f : 𝟙_ C ⟶ c), can ≫ U.map f ≫ g = can ≫ U.map f ≫ h
j : CostructuredArrow (fromPUnit (𝟙_ C)) c
⊢ ((LeftExtension.mk U { app := fun x ↦ can, naturality := ⋯ }).coconeAt c).ι.app j ≫ g =
    ((LeftExtension.mk U { app := fun x ↦ can, naturality := ⋯ }).coconeAt c).ι.app j ≫ h

Tactic:
simpa using

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
U : C ⥤ V
inst✝ : DayConvolutionUnit U
c : C
v : V
g h : U.obj c ⟶ v
e : ∀ (f : 𝟙_ C ⟶ c), can ≫ U.map f ≫ g = can ≫ U.map f ≫ h
j : CostructuredArrow (fromPUnit (𝟙_ C)) c
⊢ can ≫ U.map j.hom ≫ g = can ≫ U.map j.hom ≫ h
Module: Mathlib.CategoryTheory.Presentable.ColimitPresentation

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
J : Type u_1
I : J → Type u_2
inst✝¹ : Category.{v_1, u_1} J
inst✝ : (j : J) → Category.{?u.14, u_2} (I j)
D : J ⥤ C
P : (j : J) → ColimitPresentation (I j) (D.obj j)
k l m : Total P
f : k.Hom l
g : l.Hom m
⊢ (P k.fst).ι.app k.snd ≫ D.map (f.base ≫ g.base) = (f.hom ≫ g.hom) ≫ (P m.fst).ι.app m.snd

Tactic:
simp only [Functor.map_comp, Category.assoc]
    rw [f.w_assoc, g.w]

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 κ
P : ObjectProperty C
w✝ : ObjectProperty.EssentiallySmall.{w, v, u} P
hP : P.IsCardinalFilteredGenerator κ
⊢ P ≤ isCardinalPresentable C κ

Tactic:
exact hP.le_isCardinalPresentable

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

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
J✝ : Type u_1
I✝ : J✝ → Type u_2
inst✝⁵ : Category.{v_1, u_1} J✝
inst✝⁴ : (j : J✝) → Category.{?u.14, u_2} (I✝ j)
D✝ : J✝ ⥤ C
P✝¹ : (j : J✝) → ColimitPresentation (I✝ j) (D✝.obj j)
J : Type w
I : J → Type w
inst✝³ : SmallCategory J
inst✝² : (j : J) → SmallCategory (I j)
D : J ⥤ C
P✝ : (j : J) → ColimitPresentation (I j) (D.obj j)
X : C
P : ColimitPresentation J X
Q : (j : J) → ColimitPresentation (I j) (P.diag.obj j)
inst✝¹ : ∀ (j : J), IsFiltered (I j)
inst✝ : ∀ (j : J) (i : I j), IsFinitelyPresentable ((Q j).diag.obj i)
c : Cocone { obj := fun k ↦ (Q k.fst).diag.obj k.snd, map := fun {k l} f ↦ f.hom, map_id := ⋯, map_comp := ⋯ }
j : J
i i' : I j
u : i ⟶ i'
v : Total.mk Q j i ⟶ Total.mk Q j i' :=
  { base := 𝟙 (Total.mk Q j i).fst, hom := (Q (Total.mk Q j i).fst).diag.map u, w := ⋯ }
⊢ (Q j).diag.map u ≫ c.ι.app ⟨j, i'⟩ = c.ι.app ⟨j, i⟩ ≫ ((Functor.const (I j)).obj c.pt).map u

Tactic:
simpa using

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
J✝ : Type u_1
I✝ : J✝ → Type u_2
inst✝⁵ : Category.{v_1, u_1} J✝
inst✝⁴ : (j : J✝) → Category.{?u.14, u_2} (I✝ j)
D✝ : J✝ ⥤ C
P✝¹ : (j : J✝) → ColimitPresentation (I✝ j) (D✝.obj j)
J : Type w
I : J → Type w
inst✝³ : SmallCategory J
inst✝² : (j : J) → SmallCategory (I j)
D : J ⥤ C
P✝ : (j : J) → ColimitPresentation (I j) (D.obj j)
X : C
P : ColimitPresentation J X
Q : (j : J) → ColimitPresentation (I j) (P.diag.obj j)
inst✝¹ : ∀ (j : J), IsFiltered (I j)
inst✝ : ∀ (j : J) (i : I j), IsFinitelyPresentable ((Q j).diag.obj i)
c : Cocone { obj := fun k ↦ (Q k.fst).diag.obj k.snd, map := fun {k l} f ↦ f.hom, map_id := ⋯, map_comp := ⋯ }
j : J
i i' : I j
u : i ⟶ i'
v : Total.mk Q j i ⟶ Total.mk Q j i' :=
  { base := 𝟙 (Total.mk Q j i).fst, hom := (Q (Total.mk Q j i).fst).diag.map u, w := ⋯ }
⊢ (Q j).diag.map u ≫ c.ι.app ⟨j, i'⟩ = c.ι.app ⟨j, i⟩
Module: Mathlib.CategoryTheory.Presentable.ColimitPresentation

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
J✝ : Type u_1
I✝ : J✝ → Type u_2
inst✝⁵ : Category.{v_1, u_1} J✝
inst✝⁴ : (j : J✝) → Category.{?u.14, u_2} (I✝ j)
D✝ : J✝ ⥤ C
P✝¹ : (j : J✝) → ColimitPresentation (I✝ j) (D✝.obj j)
J : Type w
I : J → Type w
inst✝³ : SmallCategory J
inst✝² : (j : J) → SmallCategory (I j)
D : J ⥤ C
P✝ : (j : J) → ColimitPresentation (I j) (D.obj j)
X : C
P : ColimitPresentation J X
Q : (j : J) → ColimitPresentation (I j) (P.diag.obj j)
inst✝¹ : ∀ (j : J), IsFiltered (I j)
inst✝ : ∀ (j : J) (i : I j), IsFinitelyPresentable ((Q j).diag.obj i)
c : Cocone { obj := fun k ↦ (Q k.fst).diag.obj k.snd, map := fun {k l} f ↦ f.hom, map_id := ⋯, map_comp := ⋯ }
j j' : J
i : I j
i' : I j'
hom : Total.mk Q j i ⟶ Total.mk Q j' i'
⊢ hom.hom ≫ { pt := c.pt, ι := { app := fun i ↦ c.ι.app ⟨j', i⟩, naturality := ⋯ } }.ι.app i' = c.ι.app ⟨j, i⟩

Tactic:
simpa using

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
J✝ : Type u_1
I✝ : J✝ → Type u_2
inst✝⁵ : Category.{v_1, u_1} J✝
inst✝⁴ : (j : J✝) → Category.{?u.14, u_2} (I✝ j)
D✝ : J✝ ⥤ C
P✝¹ : (j : J✝) → ColimitPresentation (I✝ j) (D✝.obj j)
J : Type w
I : J → Type w
inst✝³ : SmallCategory J
inst✝² : (j : J) → SmallCategory (I j)
D : J ⥤ C
P✝ : (j : J) → ColimitPresentation (I j) (D.obj j)
X : C
P : ColimitPresentation J X
Q : (j : J) → ColimitPresentation (I j) (P.diag.obj j)
inst✝¹ : ∀ (j : J), IsFiltered (I j)
inst✝ : ∀ (j : J) (i : I j), IsFinitelyPresentable ((Q j).diag.obj i)
c : Cocone { obj := fun k ↦ (Q k.fst).diag.obj k.snd, map := fun {k l} f ↦ f.hom, map_id := ⋯, map_comp := ⋯ }
j j' : J
i : I j
i' : I j'
hom : Total.mk Q j i ⟶ Total.mk Q j' i'
⊢ hom.hom ≫ c.ι.app ⟨j', i'⟩ = c.ι.app ⟨j, i⟩