mathlib-initiative/mathlib-tactics huggingface dataset:
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✝ y₁ y₂ : D
f : y₁ ⟶ y₂
x y : C
⊢ ((corepresentableBy ((ι C V D).obj x✝) ((ι C V D).obj y₁)).homEquiv
          (map ((ι C V D).map (𝟙 x✝)) ((ι C V D).map f))).app
      (x, y) =
    ((corepresentableBy ((ι C V D).obj x✝) ((ι C V D).obj y₁)).homEquiv ((ι C V D).map (x✝ ◁ f))).app (x, y)

Tactic:
dsimp

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✝ y₁ y₂ : D
f : y₁ ⟶ y₂
x y : C
⊢ (unit ((ι C V D).obj x✝) ((ι C V D).obj y₁)).app (x, y) ≫ (map ((ι C V D).map (𝟙 x✝)) ((ι C V D).map f)).app (x ⊗ y) =
    (unit ((ι C V D).obj x✝) ((ι C V D).obj y₁)).app (x, y) ≫ ((ι C V D).map (x✝ ◁ f)).app (x ⊗ 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✝
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 y₁ : D
y₂ : x ⟶ y₁
f : D
⊢ (corepresentableBy ((ι C V D).obj x) ((ι C V D).obj f)).homEquiv (map ((ι C V D).map y₂) ((ι C V D).map (𝟙 f))) =
    (corepresentableBy ((ι C V D).obj x) ((ι C V D).obj f)).homEquiv ((ι C V D).map (y₂ ▷ f))

Tactic:
dsimp

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 y₁ : D
y₂ : x ⟶ y₁
f : D
⊢ (corepresentableBy ((ι C V D).obj x) ((ι C V D).obj f)).homEquiv (map ((ι C V D).map y₂) ((ι C V D).map (𝟙 f))) =
    (corepresentableBy ((ι C V D).obj x) ((ι C V D).obj f)).homEquiv ((ι C V D).map (y₂ ▷ 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✝
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✝ y₁ : D
y₂ : x✝ ⟶ y₁
f : D
x y : C
⊢ ((corepresentableBy ((ι C V D).obj x✝) ((ι C V D).obj f)).homEquiv (map ((ι C V D).map y₂) ((ι C V D).map (𝟙 f)))).app
      (x, y) =
    ((corepresentableBy ((ι C V D).obj x✝) ((ι C V D).obj f)).homEquiv ((ι C V D).map (y₂ ▷ f))).app (x, y)

Tactic:
dsimp

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✝ y₁ : D
y₂ : x✝ ⟶ y₁
f : D
x y : C
⊢ (unit ((ι C V D).obj x✝) ((ι C V D).obj f)).app (x, y) ≫ (map ((ι C V D).map y₂) ((ι C V D).map (𝟙 f))).app (x ⊗ y) =
    (unit ((ι C V D).obj x✝) ((ι C V D).obj f)).app (x, y) ≫ ((ι C V D).map (y₂ ▷ f)).app (x ⊗ y)
Module: Mathlib.CategoryTheory.MorphismProperty.LocalClosure

Goal state before:
pp: case refine_1.of_iso
C : Type u
inst✝⁶ : Category.{v, u} C
K : Precoverage C
P : MorphismProperty C
inst✝⁵ : P.RespectsIso
inst✝⁴ : P.RespectsLeft K.morphismProperty
inst✝³ : K.HasIsos
inst✝² : K.IsStableUnderBaseChange
inst✝¹ : K.IsStableUnderComposition
inst✝ : K.HasPullbacks
X Y : C
f✝ : X ⟶ Y
X✝ Y✝ X'✝ Y'✝ : C
f : X✝ ⟶ Y✝
g : X'✝ ⟶ Y'✝
e : Arrow.mk f ≅ Arrow.mk g
hf : sourceLocalClosure K P f
E : K.ZeroHypercover X✝
h : ∀ (U : C) (g : U ⟶ X✝), Presieve.ofArrows E.X E.f g → P (g ≫ f)
U : C
v : U ⟶ X'✝
i : (Precoverage.ZeroHypercover.pushforward (Arrow.Hom.left e.hom) ⋯ E).I₀
⊢ P ((Precoverage.ZeroHypercover.pushforward (Arrow.Hom.left e.hom) ⋯ E).f i ≫ g)

Tactic:
dsimp

Goal state after:
case refine_1.of_iso
C : Type u
inst✝⁶ : Category.{v, u} C
K : Precoverage C
P : MorphismProperty C
inst✝⁵ : P.RespectsIso
inst✝⁴ : P.RespectsLeft K.morphismProperty
inst✝³ : K.HasIsos
inst✝² : K.IsStableUnderBaseChange
inst✝¹ : K.IsStableUnderComposition
inst✝ : K.HasPullbacks
X Y : C
f✝ : X ⟶ Y
X✝ Y✝ X'✝ Y'✝ : C
f : X✝ ⟶ Y✝
g : X'✝ ⟶ Y'✝
e : Arrow.mk f ≅ Arrow.mk g
hf : sourceLocalClosure K P f
E : K.ZeroHypercover X✝
h : ∀ (U : C) (g : U ⟶ X✝), Presieve.ofArrows E.X E.f g → P (g ≫ f)
U : C
v : U ⟶ X'✝
i : (Precoverage.ZeroHypercover.pushforward (Arrow.Hom.left e.hom) ⋯ E).I₀
⊢ P ((E.f i ≫ Arrow.Hom.left e.hom) ≫ g)
Module: Mathlib.CategoryTheory.MorphismProperty.LocalClosure

Goal state before:
pp: case refine_1.comp
C : Type u
inst✝⁶ : Category.{v, u} C
K : Precoverage C
P : MorphismProperty C
inst✝⁵ : P.RespectsIso
inst✝⁴ : P.RespectsLeft K.morphismProperty
inst✝³ : K.HasIsos
inst✝² : K.IsStableUnderBaseChange
inst✝¹ : K.IsStableUnderComposition
inst✝ : K.HasPullbacks
X Y : C
f✝ : X ⟶ Y
X✝ Y✝ : C
f : X✝ ⟶ Y✝
hf : sourceLocalClosure K P f
U✝ : C
g : U✝ ⟶ X✝
E : K.ZeroHypercover X✝
h : ∀ (U : C) (g : U ⟶ X✝), Presieve.ofArrows E.X E.f g → P (g ≫ f)
F : K.ZeroHypercover X✝
hg : Presieve.ofArrows F.X F.f g
U : C
v : U ⟶ U✝
i : (Precoverage.ZeroHypercover.pullback₁ g E).I₀
⊢ P ((Precoverage.ZeroHypercover.pullback₁ g E).f i ≫ g ≫ f)

Tactic:
dsimp

Goal state after:
case refine_1.comp
C : Type u
inst✝⁶ : Category.{v, u} C
K : Precoverage C
P : MorphismProperty C
inst✝⁵ : P.RespectsIso
inst✝⁴ : P.RespectsLeft K.morphismProperty
inst✝³ : K.HasIsos
inst✝² : K.IsStableUnderBaseChange
inst✝¹ : K.IsStableUnderComposition
inst✝ : K.HasPullbacks
X Y : C
f✝ : X ⟶ Y
X✝ Y✝ : C
f : X✝ ⟶ Y✝
hf : sourceLocalClosure K P f
U✝ : C
g : U✝ ⟶ X✝
E : K.ZeroHypercover X✝
h : ∀ (U : C) (g : U ⟶ X✝), Presieve.ofArrows E.X E.f g → P (g ≫ f)
F : K.ZeroHypercover X✝
hg : Presieve.ofArrows F.X F.f g
U : C
v : U ⟶ U✝
i : (Precoverage.ZeroHypercover.pullback₁ g E).I₀
⊢ P (pullback.fst g (E.f i) ≫ g ≫ 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:
dsimp

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₂'
⊢ (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'))
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₂'
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₂)

Tactic:
dsimp

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.unit ((ι C V D).obj d₁) ((ι C V D).obj d₁')).app (u₁, u₂) ≫
      (tensorObjIsoConvolution C V d₁ d₁').hom.app (u₁ ⊗ u₂) ≫
        (DayConvolution.map ((ι C V D).map f) ((ι C V D).map f')).app (u₁ ⊗ u₂) ≫
          (tensorObjIsoConvolution C V d₂ d₂').inv.app (u₁ ⊗ u₂) =
    (DayConvolution.unit ((ι C V D).obj d₁) ((ι C V D).obj d₁')).app (u₁, u₂) ≫
      (DayConvolution.map ((ι C V D).map f) ((ι C V D).map f')).app (u₁ ⊗ u₂)
Module: Mathlib.CategoryTheory.MorphismProperty.LocalClosure

Goal state before:
pp: case refine_1.of_presieve
C : Type u
inst✝⁶ : Category.{v, u} C
K : Precoverage C
P : MorphismProperty C
inst✝⁵ : P.RespectsIso
inst✝⁴ : P.RespectsLeft K.morphismProperty
inst✝³ : K.HasIsos
inst✝² : K.IsStableUnderBaseChange
inst✝¹ : K.IsStableUnderComposition
inst✝ : K.HasPullbacks
X Y : C
f✝ : X ⟶ Y
X✝ Y✝ : C
f : X✝ ⟶ Y✝
E : K.ZeroHypercover X✝
h : ∀ (U : C) (g : U ⟶ X✝), Presieve.ofArrows E.X E.f g → sourceLocalClosure K P (g ≫ f)
ih :
  ∀ (U : C) (g : U ⟶ X✝),
    Presieve.ofArrows E.X E.f g → ∃ R ∈ K.coverings U, ∀ (U_1 : C) (g_1 : U_1 ⟶ U), R g_1 → P (g_1 ≫ g ≫ f)
S : (i : E.I₀) → Presieve (E.X i)
h' : ∀ (i : E.I₀) (U : C) (g : U ⟶ E.X i), S i g → P (g ≫ E.f i ≫ f)
F : (i : E.I₀) → K.ZeroHypercover (E.X i)
hF : ∀ (i : E.I₀), S i = Presieve.ofArrows (F i).X (F i).f
U : C
g : U ⟶ X✝
x✝ : (E.bind F).presieve₀ g
j : (E.bind F).I₀
⊢ P ((E.bind F).f j ≫ f)

Tactic:
dsimp

Goal state after:
case refine_1.of_presieve
C : Type u
inst✝⁶ : Category.{v, u} C
K : Precoverage C
P : MorphismProperty C
inst✝⁵ : P.RespectsIso
inst✝⁴ : P.RespectsLeft K.morphismProperty
inst✝³ : K.HasIsos
inst✝² : K.IsStableUnderBaseChange
inst✝¹ : K.IsStableUnderComposition
inst✝ : K.HasPullbacks
X Y : C
f✝ : X ⟶ Y
X✝ Y✝ : C
f : X✝ ⟶ Y✝
E : K.ZeroHypercover X✝
h : ∀ (U : C) (g : U ⟶ X✝), Presieve.ofArrows E.X E.f g → sourceLocalClosure K P (g ≫ f)
ih :
  ∀ (U : C) (g : U ⟶ X✝),
    Presieve.ofArrows E.X E.f g → ∃ R ∈ K.coverings U, ∀ (U_1 : C) (g_1 : U_1 ⟶ U), R g_1 → P (g_1 ≫ g ≫ f)
S : (i : E.I₀) → Presieve (E.X i)
h' : ∀ (i : E.I₀) (U : C) (g : U ⟶ E.X i), S i g → P (g ≫ E.f i ≫ f)
F : (i : E.I₀) → K.ZeroHypercover (E.X i)
hF : ∀ (i : E.I₀), S i = Presieve.ofArrows (F i).X (F i).f
U : C
g : U ⟶ X✝
x✝ : (E.bind F).presieve₀ g
j : (E.bind F).I₀
⊢ P (((F j.fst).f j.snd ≫ E.f j.fst) ≫ f)
Module: Mathlib.CategoryTheory.Monoidal.Bimod

Goal state before:
pp: case a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
W X Y Z : Mon C
M : Bimod W X
N : Bimod X Y
P P' : Bimod Y Z
f : P ⟶ P'
| coequalizer.π (M.actRight ▷ N.X) ((α_ M.X X.X N.X).hom ≫ M.X ◁ N.actLeft) ▷ P.X ≫
    coequalizer (M.actRight ▷ N.X) ((α_ M.X X.X N.X).hom ≫ M.X ◁ N.actLeft) ◁ f.hom

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)
W X Y Z : Mon C
M : Bimod W X
N : Bimod X Y
P P' : Bimod Y Z
f : P ⟶ P'
| colimit.ι
    (parallelPair (TensorBimod.actRight M N ▷ P'.X)
      ((α_ (coequalizer (M.actRight ▷ N.X) ((α_ M.X X.X N.X).hom ≫ M.X ◁ N.actLeft)) Y.X P'.X).hom ≫
        coequalizer (M.actRight ▷ N.X) ((α_ M.X X.X N.X).hom ≫ M.X ◁ N.actLeft) ◁ P'.actLeft))
    WalkingParallelPair.one

Tactic:
← whisker_exchange

Goal state after:
case a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
W X Y Z : Mon C
M : Bimod W X
N : Bimod X Y
P P' : Bimod Y Z
f : P ⟶ P'
| (M.X ⊗ N.X) ◁ f.hom ≫ coequalizer.π (M.actRight ▷ N.X) ((α_ M.X X.X N.X).hom ≫ M.X ◁ N.actLeft) ▷ P'.X

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)
W X Y Z : Mon C
M : Bimod W X
N : Bimod X Y
P P' : Bimod Y Z
f : P ⟶ P'
| colimit.ι
    (parallelPair (TensorBimod.actRight M N ▷ P'.X)
      ((α_ (coequalizer (M.actRight ▷ N.X) ((α_ M.X X.X N.X).hom ≫ M.X ◁ N.actLeft)) Y.X P'.X).hom ≫
        coequalizer (M.actRight ▷ N.X) ((α_ M.X X.X N.X).hom ≫ M.X ◁ N.actLeft) ◁ P'.actLeft))
    WalkingParallelPair.one
Module: Mathlib.CategoryTheory.Subobject.NoetherianObject

Goal state before:
pp: case refine_2
C : Type u
inst✝ : Category.{v, u} C
X : C
h : ∀ (F : ℕ ⥤ MonoOver X), IsFiltered.IsEventuallyConstant F
F : ℕ →o Subobject X
n : ℕ
hn : (⋯.functor ⋙ Subobject.representative).IsEventuallyConstantFrom n
m : ℕ
hm : n ≤ m
⊢ F n = F m

Tactic:
simpa [← MonoOver.isIso_iff_isIso_hom_left, isIso_iff_of_reflects_iso,
      PartialOrder.isIso_iff_eq] using hn (homOfLE hm)

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
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.π
        (M.actRight ▷
          { X := Y.X, actLeft := μ, one_actLeft := ⋯, left_assoc := ⋯, actRight := μ, actRight_one := ⋯,
              right_assoc := ⋯, middle_assoc := ⋯ }.X)
        ((α_ M.X Y.X
              { X := Y.X, actLeft := μ, one_actLeft := ⋯, left_assoc := ⋯, actRight := μ, actRight_one := ⋯,
                  right_assoc := ⋯, middle_assoc := ⋯ }.X).hom ≫
          M.X ◁
            { X := Y.X, actLeft := μ, one_actLeft := ⋯, left_assoc := ⋯, actRight := μ, actRight_one := ⋯,
                right_assoc := ⋯, middle_assoc := ⋯ }.actLeft) ≫
      (whiskerRight f
          { X := Y.X, actLeft := μ, one_actLeft := ⋯, left_assoc := ⋯, actRight := μ, actRight_one := ⋯,
            right_assoc := ⋯, middle_assoc := ⋯ }).hom =
    coequalizer.π
        (M.actRight ▷
          { X := Y.X, actLeft := μ, one_actLeft := ⋯, left_assoc := ⋯, actRight := μ, actRight_one := ⋯,
              right_assoc := ⋯, middle_assoc := ⋯ }.X)
        ((α_ M.X Y.X
              { X := Y.X, actLeft := μ, one_actLeft := ⋯, left_assoc := ⋯, actRight := μ, actRight_one := ⋯,
                  right_assoc := ⋯, middle_assoc := ⋯ }.X).hom ≫
          M.X ◁
            { X := Y.X, actLeft := μ, one_actLeft := ⋯, left_assoc := ⋯, actRight := μ, actRight_one := ⋯,
                right_assoc := ⋯, middle_assoc := ⋯ }.actLeft) ≫
      ((isoOfIso { hom := RightUnitorBimod.hom M, inv := RightUnitorBimod.inv M, hom_inv_id := ⋯, inv_hom_id := ⋯ } ⋯
              ⋯).hom ≫
          f ≫
            (isoOfIso { hom := RightUnitorBimod.hom N, inv := RightUnitorBimod.inv N, hom_inv_id := ⋯, inv_hom_id := ⋯ }
                ⋯ ⋯).inv).hom

Tactic:
dsimp

Goal state after:
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.π (M.actRight ▷ Y.X) ((α_ M.X Y.X Y.X).hom ≫ M.X ◁ μ) ≫
      colimMap
        (parallelPairHom (M.actRight ▷ Y.X) ((α_ M.X Y.X Y.X).hom ≫ M.X ◁ μ) (N.actRight ▷ Y.X)
          ((α_ N.X Y.X Y.X).hom ≫ N.X ◁ μ) (f.hom ▷ Y.X ▷ Y.X) (f.hom ▷ Y.X) ⋯ ⋯) =
    coequalizer.π (M.actRight ▷ Y.X) ((α_ M.X Y.X Y.X).hom ≫ M.X ◁ μ) ≫
      RightUnitorBimod.hom M ≫ f.hom ≫ RightUnitorBimod.inv N