mathlib-initiative/mathlib-tactics huggingface dataset:
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 ((comparisonAdjunction adj).counit.app Y)

Tactic:
comparisonAdjunction_counit_app

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✝² : HasReflexiveCoequalizers D
inst✝¹ : G.ReflectsIsomorphisms
inst✝ : PreservesColimitOfIsReflexivePair G
this : ∀ (X : adj.toMonad.Algebra), IsIso ((comparisonAdjunction adj).unit.app X)
Y : D
⊢ IsIso ((comparisonAdjunction adj).counit.app Y)

Tactic:
comparisonAdjunction_counit_app

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.Bimod

Goal state before:
pp: 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).inv ≫ μ ▷ P.X ▷ Q.X) ≫ P.actLeft ▷ Q.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) ≫
      (α_ R.X R.X (coequalizer (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft))).hom ≫
        R.X ◁ actLeft P Q ≫ actLeft P Q

Tactic:
slice_lhs 2 3 => rw [← comp_whiskerRight, left_assoc, comp_whiskerRight, comp_whiskerRight]

Goal state after:
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).inv ≫
      ((α_ R.X R.X P.X).hom ▷ Q.X ≫ (R.X ◁ P.actLeft) ▷ Q.X ≫ P.actLeft ▷ Q.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) ≫
      (α_ R.X R.X (coequalizer (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft))).hom ≫
        R.X ◁ actLeft P Q ≫ actLeft P Q
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Mod

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : CartesianMonoidalCategory C
M : C
inst✝¹ : MonObj M
X : C
inst✝ : ModObj M X
Z : C
m n : Z ⟶ M
x : Z ⟶ X
⊢ (m * n) • x = m • n • x

Tactic:
by simp [mul_def, smul_def, ← lift_whiskerRight]

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

Goal state before:
pp: 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) ▷ T.X ≫ actRight P Q =
    (α_ P.X Q.X T.X).hom ≫ P.X ◁ Q.actRight ≫ coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft)

Tactic:
by
  erw [map_π_preserves_coequalizer_inv_colimMap (tensorRight _)]
  simp only [Category.assoc]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Normal

Goal state before:
pp: case refine_1
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : CartesianMonoidalCategory C
G H : C
inst✝³ : GrpObj G
inst✝² : GrpObj H
φ : H ⟶ G
inst✝¹ : IsMonHom φ
inst✝ : Mono φ
ψ : G ⊗ H ⟶ H
hψ : ψ ≫ φ = G ◁ φ ≫ conj G
X : C
x : X ⟶ H
z : X ⟶ G
⊢ z * (monoidHom φ X) x * z⁻¹ ∈ (monoidHom φ X).range

Tactic:
exact ⟨lift z x ≫ ψ, by simp [hψ]⟩

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

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v, u'} D
inst✝⁴ : CartesianMonoidalCategory C
inst✝³ : CartesianMonoidalCategory D
F : C ⥤ D
inst✝² : MonoidalClosed C
inst✝¹ : MonoidalClosed D
inst✝ : Limits.PreservesLimitsOfShape (Discrete Limits.WalkingPair) F
A B : C
⊢ F.map ((ihom.coev A).app B) ≫ (expComparison F A).natTrans.app (A ⊗ B) =
    (ihom.coev (F.obj A)).app (F.obj B) ≫ (ihom (F.obj A)).map (inv (prodComparison F A B))

Tactic:
convert! unit_mateEquiv _ _ (prodComparisonNatIso F A).inv B using 3
  apply IsIso.inv_eq_of_hom_inv_id -- Porting note (https://github.com/leanprover-community/mathlib4/issues/11041): was `ext`
  simp

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
A B : Mon C
M : Bimod A B
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)
X Y Z : Mon C
M₁ M₂ : Bimod X Y
f : M₁ ⟶ M₂
N : Bimod Y Z
⊢ (α_ M₁.X N.X Z.X).hom ≫
      (f.hom ▷ (N.X ⊗ Z.X) ≫ M₂.X ◁ N.actRight) ≫
        colimit.ι (parallelPair (M₂.actRight ▷ N.X) ((α_ M₂.X Y.X N.X).hom ≫ M₂.X ◁ N.actLeft))
          WalkingParallelPair.one =
    coequalizer.π (M₁.actRight ▷ N.X) ((α_ M₁.X Y.X N.X).hom ≫ M₁.X ◁ N.actLeft) ▷ Z.X ≫
      colimMap
            (parallelPairHom (M₁.actRight ▷ N.X) ((α_ M₁.X Y.X N.X).hom ≫ M₁.X ◁ N.actLeft) (M₂.actRight ▷ N.X)
              ((α_ M₂.X Y.X N.X).hom ≫ M₂.X ◁ N.actLeft) (f.hom ▷ Y.X ▷ N.X) (f.hom ▷ N.X) ⋯ ⋯) ▷
          Z.X ≫
        TensorBimod.actRight M₂ N

Tactic:
slice_rhs 1 2 => rw [← comp_whiskerRight, ι_colimMap, parallelPairHom_app_one,
      comp_whiskerRight]

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
A B : Mon C
M : Bimod A B
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)
X Y Z : Mon C
M₁ M₂ : Bimod X Y
f : M₁ ⟶ M₂
N : Bimod Y Z
⊢ (α_ M₁.X N.X Z.X).hom ≫
      (f.hom ▷ (N.X ⊗ Z.X) ≫ M₂.X ◁ N.actRight) ≫
        colimit.ι (parallelPair (M₂.actRight ▷ N.X) ((α_ M₂.X Y.X N.X).hom ≫ M₂.X ◁ N.actLeft))
          WalkingParallelPair.one =
    (f.hom ▷ N.X ▷ Z.X ≫
        colimit.ι (parallelPair (M₂.actRight ▷ N.X) ((α_ M₂.X Y.X N.X).hom ≫ M₂.X ◁ N.actLeft))
            WalkingParallelPair.one ▷
          Z.X) ≫
      TensorBimod.actRight M₂ N
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'
⊢ H.map f ≫
      Wedge.IsLimit.lift (ℌ'.isLimitWedge c')
        (fun j ↦ ℌ.π c' j ≫ ((((dayConvolutionInternalHomDiagramFunctor F).map f✝).app c').app (op j)).app j) ⋯ =
    Wedge.IsLimit.lift (ℌ'.isLimitWedge c)
        (fun j ↦ ℌ.π c j ≫ ((((dayConvolutionInternalHomDiagramFunctor F).map f✝).app c).app (op j)).app j) ⋯ ≫
      H'.map f

Tactic:
apply Wedge.IsLimit.hom_ext (ℌ'.isLimitWedge c')
    intro j
    dsimp
    simp only [Category.assoc, map_comp_π]
    rw [← Wedge.mk_ι
        (F := dayConvolutionInternalHomDiagramFunctor F |>.obj _ |>.obj c')
        (H'.obj c') (ℌ'.π c') (ℌ'.hπ c'),
      ← Wedge.mk_ι
        (F := dayConvolutionInternalHomDiagramFunctor F |>.obj _ |>.obj c)
        (H'.obj c) (ℌ'.π c) (ℌ'.hπ c),
      Wedge.IsLimit.lift_ι (ℌ'.isLimitWedge c'),
      Wedge.IsLimit.lift_ι_assoc (ℌ'.isLimitWedge c)]
    simp [← Functor.map_comp]

Goal state after:
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 : (λ_ (𝟙_ C)).inv ≫ η ▷ 𝟙_ C ≫ A ◁ η ≫ 𝒮 ▷ A ≫ μ = η ≫ ε ≫ η
⊢ η ≫ 𝒮 = η

Tactic:
unitors_inv_equal,

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
this : (ρ_ (𝟙_ C)).inv ≫ η ▷ 𝟙_ C ≫ 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:
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.actLeft ≫ (λ_ 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.X) ((α_ R.X R.X P.X).hom ≫ R.X ◁ P.actLeft)

Tactic:
leftUnitor_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
| (λ_ (R.X ⊗ P.X)).inv ≫ 𝟙_ C ◁ P.actLeft

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.X) ((α_ R.X R.X P.X).hom ≫ R.X ◁ P.actLeft)
Module: Mathlib.CategoryTheory.Monoidal.OfHasFiniteProducts

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X✝ Y✝ : C
inst✝¹ : HasInitial C
inst✝ : HasBinaryCoproducts C
X Y Z : C
⊢ (α_ X Y Z).hom ≫ (coprod.braiding X (Y ⊗ Z)).hom ≫ (α_ Y Z X).hom =
    (coprod.braiding X Y).hom ▷ Z ≫ (α_ Y X Z).hom ≫ Y ◁ (coprod.braiding X Z).hom

Tactic:
dsimp [monoidalOfHasFiniteCoproducts.associator_hom]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
X✝ Y✝ : C
inst✝¹ : HasInitial C
inst✝ : HasBinaryCoproducts C
X Y Z : C
⊢ coprod.desc (coprod.desc coprod.inl (coprod.inl ≫ coprod.inr)) (coprod.inr ≫ coprod.inr) ≫
      (coprod.braiding X (Y ⨿ Z)).hom ≫
        coprod.desc (coprod.desc coprod.inl (coprod.inl ≫ coprod.inr)) (coprod.inr ≫ coprod.inr) =
    coprod.map (coprod.braiding X Y).hom (𝟙 Z) ≫
      coprod.desc (coprod.desc coprod.inl (coprod.inl ≫ coprod.inr)) (coprod.inr ≫ coprod.inr) ≫
        coprod.map (𝟙 Y) (coprod.braiding X Z).hom
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
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
X Y : Mon C
M N : Bimod X Y
f : M ⟶ N
| N.actLeft ≫ (λ_ N.X).inv

pp: case a.a.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)
X Y : Mon C
M N : Bimod X Y
f : M ⟶ N
| η ▷ N.X

pp: case a.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)
X Y : Mon C
M N : Bimod X Y
f : M ⟶ N
| coequalizer.π (μ ▷ N.X) ((α_ X.X X.X N.X).hom ≫ X.X ◁ N.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)
X Y : Mon C
M N : Bimod X Y
f : M ⟶ N
| X.X ◁ f.hom

Tactic:
leftUnitor_inv_naturality

Goal state after:
case a.a.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)
X Y : Mon C
M N : Bimod X Y
f : M ⟶ N
| (λ_ (X.X ⊗ N.X)).inv ≫ 𝟙_ C ◁ N.actLeft

case a.a.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)
X Y : Mon C
M N : Bimod X Y
f : M ⟶ N
| η ▷ N.X

case a.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)
X Y : Mon C
M N : Bimod X Y
f : M ⟶ N
| coequalizer.π (μ ▷ N.X) ((α_ X.X X.X N.X).hom ≫ X.X ◁ N.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)
X Y : Mon C
M N : Bimod X Y
f : M ⟶ N
| X.X ◁ f.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
F : C ⥤ V
inst✝¹ : ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (fromPUnit (𝟙_ C)) d) (tensorLeft v)
inst✝ : DayConvolution F U
x : C
⊢ (rightUnitor U F).inv.app x =
    (ρ_ (F.obj x)).inv ≫ F.obj x ◁ can ≫ (DayConvolution.unit F U).app (x, 𝟙_ C) ≫ (F ⊛ U).map (ρ_ x).hom

Tactic:
dsimp [rightUnitor, Coyoneda.fullyFaithful, corepresentableByRight,
    rightUnitorCorepresentingIso, Functor.CorepresentableBy.ofIso,
    Functor.corepresentableByEquiv, Iso.toEquiv, Equiv.toIso]

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
F : C ⥤ V
inst✝¹ : ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (fromPUnit (𝟙_ C)) d) (tensorLeft v)
inst✝ : DayConvolution F U
x : C
⊢ (ρ_ (F.obj x)).inv ≫
      ((ConcreteCategory.hom
                (𝟙
                  (prod.rightInverseUnitor C ⋙ F ⊠ fromPUnit (𝟙_ V) ⟶
                    prod.rightInverseUnitor C ⋙ (𝟭 C).prod (fromPUnit (𝟙_ C)) ⋙ tensor C ⋙ F ⊛ U)))
              ((prod.rightUnitorEquivalence C).congrLeft.fullyFaithfulFunctor.homEquiv
                (((F ⊠ U).homEquivOfIsLeftKanExtension (extensionUnitRight U (φ U) F) (tensor C ⋙ F ⊛ U))
                  (((F ⊛ U).homEquivOfIsLeftKanExtension (DayConvolution.unit F U) (F ⊛ U)) (𝟙 (F ⊛ U)))))).app
          x ≫
        (F ⊛ U).map (ρ_ x).hom =
    (ρ_ (F.obj x)).inv ≫ F.obj x ◁ can ≫ (DayConvolution.unit F U).app (x, 𝟙_ C) ≫ (F ⊛ U).map (ρ_ x).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
F : C ⥤ V
inst✝² : ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (fromPUnit (𝟙_ C)) d) (tensorLeft v)
inst✝¹ : DayConvolution F U
G : C ⥤ V
inst✝ : DayConvolution G U
f : F ⟶ G
⊢ DayConvolution.map f (𝟙 U) ≫ (rightUnitor U G).hom = (rightUnitor U F).hom ≫ f

Tactic:
by
  apply Functor.hom_ext_of_isLeftKanExtension _ (DayConvolution.unit _ _) _
  apply Functor.hom_ext_of_isLeftKanExtension _ (extensionUnitRight U (φ U) F) _
  ext
  simp [whisker_exchange_assoc]

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)
k l : Total Q
u : k ⟶ l
⊢ { obj := fun k ↦ (Q k.fst).diag.obj k.snd, map := fun {k l} f ↦ f.hom, map_id := ⋯, map_comp := ⋯ }.map u ≫
      (Q l.fst).ι.app l.snd ≫ P.ι.app l.fst =
    ((Q k.fst).ι.app k.snd ≫ P.ι.app k.fst) ≫ ((Functor.const (Total Q)).obj X).map u

Tactic:
by simp [← u.w_assoc]

Goal state after:
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✝
C : Type u₁
inst✝¹² : Category.{v₁, u₁} C
V : Type u₂
inst✝¹¹ : Category.{v₂, u₂} V
inst✝¹⁰ : MonoidalCategory C
inst✝⁹ : MonoidalCategory V
D : Type u₃
inst✝⁸ : Category.{v₃, u₃} D
inst✝⁷ : MonoidalCategoryStruct D
inst✝⁶ : LawfulDayConvolutionMonoidalCategoryStruct C V D
inst✝⁵ : ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorLeft v)
inst✝⁴ : ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorRight v)
inst✝³ :
  ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (𝟙_ C)) d) (tensorLeft v)
inst✝² :
  ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (𝟙_ C)) d) (tensorRight v)
inst✝¹ :
  ∀ (v : V) (d : C × C),
    Limits.PreservesColimitsOfShape (CostructuredArrow ((𝟭 C).prod (Functor.fromPUnit (𝟙_ C))) d) (tensorRight v)
inst✝ :
  ∀ (v : V) (d : C × C), Limits.PreservesColimitsOfShape (CostructuredArrow ((tensor C).prod (𝟭 C)) d) (tensorRight v)
X₁✝ X₂✝ X₃✝ Y₁✝ Y₂✝ Y₃✝ : D
f₁ : X₁✝ ⟶ Y₁✝
f₂ : X₂✝ ⟶ Y₂✝
f₃ : X₃✝ ⟶ Y₃✝
⊢ (ι C V D).map (((f₁ ⊗ₘ f₂) ⊗ₘ f₃) ≫ (α_ Y₁✝ Y₂✝ Y₃✝).hom) = (ι C V D).map ((α_ X₁✝ X₂✝ X₃✝).hom ≫ (f₁ ⊗ₘ f₂ ⊗ₘ f₃))

Tactic:
simp only [Functor.map_comp, ι_map_associator_hom_eq_associator_hom,
        ι_map_tensorHom_hom_eq_tensorHom]

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✝
C : Type u₁
inst✝¹² : Category.{v₁, u₁} C
V : Type u₂
inst✝¹¹ : Category.{v₂, u₂} V
inst✝¹⁰ : MonoidalCategory C
inst✝⁹ : MonoidalCategory V
D : Type u₃
inst✝⁸ : Category.{v₃, u₃} D
inst✝⁷ : MonoidalCategoryStruct D
inst✝⁶ : LawfulDayConvolutionMonoidalCategoryStruct C V D
inst✝⁵ : ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorLeft v)
inst✝⁴ : ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorRight v)
inst✝³ :
  ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (𝟙_ C)) d) (tensorLeft v)
inst✝² :
  ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (𝟙_ C)) d) (tensorRight v)
inst✝¹ :
  ∀ (v : V) (d : C × C),
    Limits.PreservesColimitsOfShape (CostructuredArrow ((𝟭 C).prod (Functor.fromPUnit (𝟙_ C))) d) (tensorRight v)
inst✝ :
  ∀ (v : V) (d : C × C), Limits.PreservesColimitsOfShape (CostructuredArrow ((tensor C).prod (𝟭 C)) d) (tensorRight v)
X₁✝ X₂✝ X₃✝ Y₁✝ Y₂✝ Y₃✝ : D
f₁ : X₁✝ ⟶ Y₁✝
f₂ : X₂✝ ⟶ Y₂✝
f₃ : X₃✝ ⟶ Y₃✝
⊢ map (map ((ι C V D).map f₁) ((ι C V D).map f₂)) ((ι C V D).map f₃) ≫
      (DayConvolution.associator ((ι C V D).obj Y₁✝) ((ι C V D).obj Y₂✝) ((ι C V D).obj Y₃✝)).hom =
    (DayConvolution.associator ((ι C V D).obj X₁✝) ((ι C V D).obj X₂✝) ((ι C V D).obj X₃✝)).hom ≫
      map ((ι C V D).map f₁) (map ((ι C V D).map f₂) ((ι C V D).map f₃))
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
D : Type u₃
inst✝⁵ : Category.{v₃, u₃} D
inst✝⁴ : InducedLawfulDayConvolutionMonoidalCategoryStructCore C V D
inst✝³ : ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorLeft v)
inst✝² : ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorRight v)
inst✝¹ :
  ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (𝟙_ C)) d) (tensorRight v)
inst✝ :
  ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (𝟙_ C)) d) (tensorLeft v)
d₁ d₁' d₂ d₂' : D
f : d₁ ⟶ d₂
f' : d₁' ⟶ d₂'
⊢ (DayConvolution.corepresentableBy ((ι C V D).obj d₁) ((ι C V D).obj d₁')).homEquiv
      ((tensorObjIsoConvolution C V d₁ d₁').hom ≫
        DayConvolution.map ((ι C V D).map f) ((ι C V D).map f') ≫ (tensorObjIsoConvolution C V d₂ d₂').inv) =
    (DayConvolution.corepresentableBy ((ι C V D).obj d₁) ((ι C V D).obj d₁')).homEquiv
      (DayConvolution.map ((ι C V D).map f) ((ι C V D).map f'))

Tactic:
ext ⟨u₁, u₂⟩

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
D : Type u₃
inst✝⁵ : Category.{v₃, u₃} D
inst✝⁴ : InducedLawfulDayConvolutionMonoidalCategoryStructCore C V D
inst✝³ : ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorLeft v)
inst✝² : ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorRight v)
inst✝¹ :
  ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (𝟙_ C)) d) (tensorRight v)
inst✝ :
  ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (𝟙_ C)) d) (tensorLeft v)
d₁ d₁' d₂ d₂' : D
f : d₁ ⟶ d₂
f' : d₁' ⟶ d₂'
u₁ u₂ : C
⊢ ((DayConvolution.corepresentableBy ((ι C V D).obj d₁) ((ι C V D).obj d₁')).homEquiv
          ((tensorObjIsoConvolution C V d₁ d₁').hom ≫
            DayConvolution.map ((ι C V D).map f) ((ι C V D).map f') ≫ (tensorObjIsoConvolution C V d₂ d₂').inv)).app
      (u₁, u₂) =
    ((DayConvolution.corepresentableBy ((ι C V D).obj d₁) ((ι C V D).obj d₁')).homEquiv
          (DayConvolution.map ((ι C V D).map f) ((ι C V D).map f'))).app
      (u₁, u₂)