mathlib-initiative/mathlib-tactics huggingface dataset:
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
A : C ⥤ D
inst✝ : ComonObj A
X✝ Y✝ : C
f : X✝ ⟶ Y✝
⊢ ε.app X✝ ≫ 𝟙 (𝟙_ D) = ε.app X✝

Tactic:
]

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
A : C ⥤ D
inst✝ : ComonObj A
X✝ Y✝ : C
f : X✝ ⟶ Y✝
⊢ ε.app X✝ ≫ 𝟙 (𝟙_ D) = ε.app X✝
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
A : C ⥤ D
inst✝ : ComonObj A
X✝ Y✝ : C
f : X✝ ⟶ Y✝
⊢ ε.app X✝ = ε.app X✝

Tactic:
]

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
U : C ⥤ V
inst✝² : DayConvolutionUnit U
F : C ⥤ V
inst✝¹ : ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (fromPUnit (𝟙_ C)) d) (tensorRight v)
inst✝ : DayConvolution U F
x : C
⊢ (λ_ (F.obj x)).inv ≫
      ((prod.leftInverseUnitor C).whiskerLeft
              (((U ⊠ F).homEquivOfIsLeftKanExtension (extensionUnitLeft U (φ U) F) (tensor C ⋙ U ⊛ F))
                (((U ⊛ F).homEquivOfIsLeftKanExtension (DayConvolution.unit U F) (U ⊛ F)) (𝟙 (U ⊛ F))))).app
          x ≫
        (U ⊛ F).map (λ_ x).hom =
    (λ_ (F.obj x)).inv ≫ can ▷ F.obj x ≫ (DayConvolution.unit U F).app (𝟙_ C, x) ≫ (U ⊛ F).map (λ_ x).hom

Tactic:
]

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) (tensorRight v)
inst✝ : DayConvolution U F
x : C
⊢ (λ_ (F.obj x)).inv ≫
      ((prod.leftInverseUnitor C).whiskerLeft
              (((U ⊠ F).homEquivOfIsLeftKanExtension (extensionUnitLeft U (φ U) F) (tensor C ⋙ U ⊛ F))
                (((U ⊛ F).homEquivOfIsLeftKanExtension (DayConvolution.unit U F) (U ⊛ F)) (𝟙 (U ⊛ F))))).app
          x ≫
        (U ⊛ F).map (λ_ x).hom =
    (λ_ (F.obj x)).inv ≫ can ▷ F.obj x ≫ (DayConvolution.unit U F).app (𝟙_ C, x) ≫ (U ⊛ F).map (λ_ x).hom
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
A : C ⥤ D
inst✝ : ComonObj A
X✝ Y✝ : C
f : X✝ ⟶ Y✝
⊢ Δ.app X✝ ≫ (A.map f ⊗ₘ A.map f) = Δ.app X✝ ≫ (A.map f ⊗ₘ A.map f)

Tactic:
]

Goal state after:
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
A : C ⥤ D
inst✝ : ComonObj A
X : C
⊢ 𝟙 (A.obj X) = 𝟙 (A.obj X)

Tactic:
]

Goal state after:
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
A : C ⥤ D
inst✝ : ComonObj A
X✝ Y✝ Z✝ : C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ A.map f ≫ A.map g = A.map f ≫ A.map g

Tactic:
]

Goal state after:
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
⊢ ε = ε

Tactic:
]

Goal state after:
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 ⊗ₘ (α.app x).hom)

Tactic:
]

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)
k l m : Total P
f : k.Hom l
g : l.Hom m
⊢ f.hom ≫ g.hom ≫ (P m.fst).ι.app m.snd = f.hom ≫ g.hom ≫ (P m.fst).ι.app m.snd

Tactic:
]

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
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 ≫
      ((prod.rightInverseUnitor C).whiskerLeft
              (((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

Tactic:
]

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 ≫
      ((prod.rightInverseUnitor C).whiskerLeft
              (((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.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:
]

Goal state after:
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 κ
Module: Mathlib.CategoryTheory.Presentable.Dense

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
κ : Cardinal.{w}
inst✝³ : Fact κ.IsRegular
J : Type u'
inst✝² : Category.{v', u'} J
inst✝¹ : EssentiallySmall.{w, v', u'} J
inst✝ : IsCardinalFiltered J κ
X : C
p : (isCardinalPresentable C κ).ColimitOfShape J X
this : IsFiltered J
⊢ (∀ (d : CostructuredArrow (isCardinalPresentable C κ).ι X), ∃ c, Nonempty (d ⟶ p.toCostructuredArrow.obj c)) ∧
    ∀ {d : CostructuredArrow (isCardinalPresentable C κ).ι X} {c : J} (s s' : d ⟶ p.toCostructuredArrow.obj c),
      ∃ c' t, s ≫ p.toCostructuredArrow.map t = s' ≫ p.toCostructuredArrow.map t

Tactic:
]

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
κ : Cardinal.{w}
inst✝³ : Fact κ.IsRegular
J : Type u'
inst✝² : Category.{v', u'} J
inst✝¹ : EssentiallySmall.{w, v', u'} J
inst✝ : IsCardinalFiltered J κ
X : C
p : (isCardinalPresentable C κ).ColimitOfShape J X
this : IsFiltered J
⊢ (∀ (d : CostructuredArrow (isCardinalPresentable C κ).ι X), ∃ c, Nonempty (d ⟶ p.toCostructuredArrow.obj c)) ∧
    ∀ {d : CostructuredArrow (isCardinalPresentable C κ).ι X} {c : J} (s s' : d ⟶ p.toCostructuredArrow.obj c),
      ∃ c' t, s ≫ p.toCostructuredArrow.map t = s' ≫ p.toCostructuredArrow.map t
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)
inst✝² : IsFiltered J
inst✝¹ : ∀ (j : J), IsFiltered (I j)
inst✝ : ∀ (j : J) (i : I j), IsFinitelyPresentable ((P j).diag.obj i)
k l : Total P
f g : k ⟶ l
a : J := IsFiltered.coeq f.base g.base
a' : I (IsFiltered.coeq f.base g.base)
u : Total.mk P l.fst l.snd ⟶ Total.mk P (IsFiltered.coeq f.base g.base) a'
hu : u.base = IsFiltered.coeqHom f.base g.base
⊢ (P k.fst).ι.app k.snd ≫ D.map (g.base ≫ IsFiltered.coeqHom f.base g.base) =
    (P k.fst).ι.app k.snd ≫ D.map g.base ≫ D.map (IsFiltered.coeqHom f.base g.base)

Tactic:
]

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)
inst✝² : IsFiltered J
inst✝¹ : ∀ (j : J), IsFiltered (I j)
inst✝ : ∀ (j : J) (i : I j), IsFinitelyPresentable ((P j).diag.obj i)
k l : Total P
f g : k ⟶ l
a : J := IsFiltered.coeq f.base g.base
a' : I (IsFiltered.coeq f.base g.base)
u : Total.mk P l.fst l.snd ⟶ Total.mk P (IsFiltered.coeq f.base g.base) a'
hu : u.base = IsFiltered.coeqHom f.base g.base
⊢ (P k.fst).ι.app k.snd ≫ D.map (g.base ≫ IsFiltered.coeqHom f.base g.base) =
    (P k.fst).ι.app k.snd ≫ D.map g.base ≫ D.map (IsFiltered.coeqHom f.base g.base)
Module: Mathlib.CategoryTheory.Presentable.Dense

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

Tactic:
]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsFinitelyAccessibleCategory C
X : C
⊢ IsCardinalFiltered (CostructuredArrow (isCardinalPresentable C Cardinal.aleph0).ι X) Cardinal.aleph0
Module: Mathlib.CategoryTheory.Presentable.Dense

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

Tactic:
]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsFinitelyAccessibleCategory C
⊢ (isCardinalPresentable C Cardinal.aleph0).ι.IsDense
Module: Mathlib.CategoryTheory.Presentable.Dense

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsFinitelyAccessibleCategory C
⊢ ObjectProperty.EssentiallySmall.{w, v, u} (isCardinalPresentable C Cardinal.aleph0)

Tactic:
]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsFinitelyAccessibleCategory C
⊢ ObjectProperty.EssentiallySmall.{w, v, u} (isCardinalPresentable C Cardinal.aleph0)
Module: Mathlib.CategoryTheory.ObjectProperty.Ind

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
P : ObjectProperty C
ι : Type u_1
inst✝³ : Small.{w, u_1} ι
inst✝² : P.IsClosedUnderLimitsOfShape (Discrete ι)
inst✝¹ : HasProductsOfShape ι C
inst✝ : IsIPCOfShape.{w, u_1, v, u} ι C
X : C
x✝ : P.ind.strictLimitsOfShape (Discrete ι) X
Y : Discrete ι ⥤ C
h : ∀ (j : Discrete ι), P.ind (Y.obj j)
e : ι ≃ Shrink.{w, u_1} ι := equivShrink ι
this✝¹ : HasProductsOfShape (Shrink.{w, u_1} ι) C
this✝ : IsIPCOfShape.{w, w, v, u} (Shrink.{w, u_1} ι) C
this : P.IsClosedUnderLimitsOfShape (Discrete (Shrink.{w, u_1} ι))
iso : limit Y ≅ ∏ᶜ fun i ↦ Y.obj { as := e.symm i } :=
  (Pi.isoLimit Y).symm ≪≫ (Pi.reindex e.symm fun j ↦ Y.obj { as := j }).symm
⊢ P.ind (∏ᶜ fun i ↦ Y.obj { as := e.symm i })

Tactic:
]

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
P : ObjectProperty C
ι : Type u_1
inst✝³ : Small.{w, u_1} ι
inst✝² : P.IsClosedUnderLimitsOfShape (Discrete ι)
inst✝¹ : HasProductsOfShape ι C
inst✝ : IsIPCOfShape.{w, u_1, v, u} ι C
X : C
x✝ : P.ind.strictLimitsOfShape (Discrete ι) X
Y : Discrete ι ⥤ C
h : ∀ (j : Discrete ι), P.ind (Y.obj j)
e : ι ≃ Shrink.{w, u_1} ι := equivShrink ι
this✝¹ : HasProductsOfShape (Shrink.{w, u_1} ι) C
this✝ : IsIPCOfShape.{w, w, v, u} (Shrink.{w, u_1} ι) C
this : P.IsClosedUnderLimitsOfShape (Discrete (Shrink.{w, u_1} ι))
iso : limit Y ≅ ∏ᶜ fun i ↦ Y.obj { as := e.symm i } :=
  (Pi.isoLimit Y).symm ≪≫ (Pi.reindex e.symm fun j ↦ Y.obj { as := j }).symm
⊢ P.ind (∏ᶜ fun i ↦ Y.obj { as := e.symm 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:
]

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 ≫ { pt := c.pt, ι := { app := fun i ↦ c.ι.app ⟨j', i⟩, naturality := ⋯ } }.ι.app i' = c.ι.app ⟨j, i⟩
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
⊢ ((ι C V D).obj x✝).obj x ◁ ((ι C V D).map f).app y ≫ (convolutionExtensionUnit C V x✝ y₂).app (x, y) =
    ((ι C V D).obj x✝).obj x ◁ ((ι C V D).map f).app y ≫ (convolutionExtensionUnit C V x✝ y₂).app (x, y)

Tactic:
]

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

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.LocalClosure

Goal state before:
pp: case of_iso
C : Type u
inst✝¹ : Category.{v, u} C
K : Precoverage C
P Q : MorphismProperty C
h : P ≤ Q
inst✝ : Q.IsLocalAtSource K
X Y : C
f✝ : X ⟶ Y
X✝ Y✝ X'✝ Y'✝ : C
f : X✝ ⟶ Y✝
g : X'✝ ⟶ Y'✝
e : Arrow.mk f ≅ Arrow.mk g
a✝ : sourceLocalClosure K P f
hf : Q f
⊢ Q f

Tactic:
]

Goal state after:
case of_iso
C : Type u
inst✝¹ : Category.{v, u} C
K : Precoverage C
P Q : MorphismProperty C
h : P ≤ Q
inst✝ : Q.IsLocalAtSource K
X Y : C
f✝ : X ⟶ Y
X✝ Y✝ X'✝ Y'✝ : C
f : X✝ ⟶ Y✝
g : X'✝ ⟶ Y'✝
e : Arrow.mk f ≅ Arrow.mk g
a✝ : sourceLocalClosure K P f
hf : Q f
⊢ Q f
Module: Mathlib.CategoryTheory.MorphismProperty.LocalClosure

Goal state before:
pp: case comp
C : Type u
inst✝³ : Category.{v, u} C
K : Precoverage C
P Q : MorphismProperty C
X✝¹ Y✝¹ : C
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : K.IsStableUnderBaseChange
inst✝ : HasPullbacks C
Y X Z : C
f : X ⟶ Z
X✝ Y✝ : C
f' : X✝ ⟶ Y✝
hf' : sourceLocalClosure K P f'
R : Presieve X✝
hR : R ∈ K.coverings X✝
U✝ : C
g' : U✝ ⟶ X✝
hg' : R g'
ih : ∀ (W : C) (g : Y ⟶ Y✝) (fst : W ⟶ X✝) (snd : W ⟶ Y), IsPullback fst snd f' g → sourceLocalClosure K P snd
W : C
g : Y ⟶ Y✝
fst : W ⟶ U✝
snd : W ⟶ Y
h✝ : IsPullback fst snd (g' ≫ f') g
u : W ⟶ pullback g f' := pullback.lift snd (fst ≫ g') ⋯
h : IsPullback fst (u ≫ pullback.fst g f') (g' ≫ f') g
this : snd = u ≫ pullback.fst g f'
⊢ sourceLocalClosure K P (u ≫ pullback.fst g f')

Tactic:
]

Goal state after:
case comp
C : Type u
inst✝³ : Category.{v, u} C
K : Precoverage C
P Q : MorphismProperty C
X✝¹ Y✝¹ : C
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : K.IsStableUnderBaseChange
inst✝ : HasPullbacks C
Y X Z : C
f : X ⟶ Z
X✝ Y✝ : C
f' : X✝ ⟶ Y✝
hf' : sourceLocalClosure K P f'
R : Presieve X✝
hR : R ∈ K.coverings X✝
U✝ : C
g' : U✝ ⟶ X✝
hg' : R g'
ih : ∀ (W : C) (g : Y ⟶ Y✝) (fst : W ⟶ X✝) (snd : W ⟶ Y), IsPullback fst snd f' g → sourceLocalClosure K P snd
W : C
g : Y ⟶ Y✝
fst : W ⟶ U✝
snd : W ⟶ Y
h✝ : IsPullback fst snd (g' ≫ f') g
u : W ⟶ pullback g f' := pullback.lift snd (fst ≫ g') ⋯
h : IsPullback fst (u ≫ pullback.fst g f') (g' ≫ f') g
this : snd = u ≫ pullback.fst g f'
⊢ sourceLocalClosure K P (u ≫ pullback.fst g f')
Module: Mathlib.CategoryTheory.MorphismProperty.LocalClosure

Goal state before:
pp: case comp
C : Type u
inst✝³ : Category.{v, u} C
K : Precoverage C
P Q : MorphismProperty C
X✝¹ Y✝¹ : C
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : K.IsStableUnderBaseChange
inst✝ : HasPullbacks C
Y X Z : C
f : X ⟶ Z
X✝ Y✝ : C
f' : X✝ ⟶ Y✝
hf' : sourceLocalClosure K P f'
R : Presieve X✝
hR : R ∈ K.coverings X✝
U✝ : C
g' : U✝ ⟶ X✝
hg' : R g'
ih : ∀ (W : C) (g : Y ⟶ Y✝) (fst : W ⟶ X✝) (snd : W ⟶ Y), IsPullback fst snd f' g → sourceLocalClosure K P snd
W : C
g : Y ⟶ Y✝
fst : W ⟶ U✝
snd : W ⟶ Y
h✝ : IsPullback fst snd (g' ≫ f') g
u : W ⟶ pullback g f' := pullback.lift snd (fst ≫ g') ⋯
h : IsPullback fst (u ≫ pullback.fst g f') (g' ≫ f') g
this : snd = u ≫ pullback.fst g f'
e : W ≅ pullback g' (pullback.snd g f') := ⋯.isoPullback
⊢ sourceLocalClosure K P ((e.inv ≫ u) ≫ pullback.fst g f')

Tactic:
]

Goal state after:
case comp
C : Type u
inst✝³ : Category.{v, u} C
K : Precoverage C
P Q : MorphismProperty C
X✝¹ Y✝¹ : C
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : K.IsStableUnderBaseChange
inst✝ : HasPullbacks C
Y X Z : C
f : X ⟶ Z
X✝ Y✝ : C
f' : X✝ ⟶ Y✝
hf' : sourceLocalClosure K P f'
R : Presieve X✝
hR : R ∈ K.coverings X✝
U✝ : C
g' : U✝ ⟶ X✝
hg' : R g'
ih : ∀ (W : C) (g : Y ⟶ Y✝) (fst : W ⟶ X✝) (snd : W ⟶ Y), IsPullback fst snd f' g → sourceLocalClosure K P snd
W : C
g : Y ⟶ Y✝
fst : W ⟶ U✝
snd : W ⟶ Y
h✝ : IsPullback fst snd (g' ≫ f') g
u : W ⟶ pullback g f' := pullback.lift snd (fst ≫ g') ⋯
h : IsPullback fst (u ≫ pullback.fst g f') (g' ≫ f') g
this : snd = u ≫ pullback.fst g f'
e : W ≅ pullback g' (pullback.snd g f') := ⋯.isoPullback
⊢ sourceLocalClosure K P ((e.inv ≫ u) ≫ pullback.fst g f')