mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Monoidal.ExternalProduct.KanExtension

Goal state before:
pp: V : Type u₁
inst✝⁵ : Category.{v₁, u₁} V
inst✝⁴ : MonoidalCategory V
D : Type u₂
D' : Type u₃
E : Type u₄
inst✝³ : Category.{v₂, u₂} D
inst✝² : Category.{v₃, u₃} D'
inst✝¹ : Category.{v₄, u₄} E
H : D ⥤ V
L : D ⥤ D'
H' : D' ⥤ V
α : H ⟶ L ⋙ H'
K : E ⥤ V
d : D'
P : (Functor.LeftExtension.mk H' α).IsPointwiseLeftKanExtensionAt d
e : E
inst✝ : Limits.PreservesColimitsOfShape (CostructuredArrow L d) (tensorRight (K.obj e))
cone : Limits.Cocone (CostructuredArrow.proj (L.prod (𝟭 E)) (d, e) ⋙ H ⊠ K) :=
  (Functor.LeftExtension.mk (H' ⊠ K) (extensionUnitLeft H' α K)).coconeAt (d, e)
equiv : CostructuredArrow L d × CostructuredArrow (𝟭 E) e ≌ CostructuredArrow (L.prod (𝟭 E)) (d, e) :=
  (CostructuredArrow.prodEquivalence L (𝟭 E) d e).symm
I : CostructuredArrow L d ⥤ CostructuredArrow L d × CostructuredArrow (𝟭 E) e :=
  (prod.rightUnitorEquivalence (CostructuredArrow L d)).inverse ⋙
    (𝟭 (CostructuredArrow L d)).prod (Functor.fromPUnit (CostructuredArrow.mk (𝟙 ((𝟭 E).obj e))))
this : I.Final := isPointwiseLeftKanExtensionAtExtensionUnitLeft._proof_1 d e
⊢ Limits.IsColimit
    (Limits.Cocone.whisker equiv.functor
      ((Functor.LeftExtension.mk (H' ⊠ K) (extensionUnitLeft H' α K)).coconeAt (d, e)))

Tactic:
apply Functor.Final.isColimitWhiskerEquiv I (Limits.Cocone.whisker equiv.functor cone) |>.toFun

Goal state after:
V : Type u₁
inst✝⁵ : Category.{v₁, u₁} V
inst✝⁴ : MonoidalCategory V
D : Type u₂
D' : Type u₃
E : Type u₄
inst✝³ : Category.{v₂, u₂} D
inst✝² : Category.{v₃, u₃} D'
inst✝¹ : Category.{v₄, u₄} E
H : D ⥤ V
L : D ⥤ D'
H' : D' ⥤ V
α : H ⟶ L ⋙ H'
K : E ⥤ V
d : D'
P : (Functor.LeftExtension.mk H' α).IsPointwiseLeftKanExtensionAt d
e : E
inst✝ : Limits.PreservesColimitsOfShape (CostructuredArrow L d) (tensorRight (K.obj e))
cone : Limits.Cocone (CostructuredArrow.proj (L.prod (𝟭 E)) (d, e) ⋙ H ⊠ K) := ⋯
equiv : CostructuredArrow L d × CostructuredArrow (𝟭 E) e ≌ CostructuredArrow (L.prod (𝟭 E)) (d, e) := ⋯
I : CostructuredArrow L d ⥤ CostructuredArrow L d × CostructuredArrow (𝟭 E) e := ⋯
this : I.Final := ⋯
⊢ Limits.IsColimit (Limits.Cocone.whisker I (Limits.Cocone.whisker equiv.functor cone))
Module: Mathlib.CategoryTheory.Monoidal.ExternalProduct.KanExtension

Goal state before:
pp: V : Type u₁
inst✝⁵ : Category.{v₁, u₁} V
inst✝⁴ : MonoidalCategory V
D : Type u₂
D' : Type u₃
E : Type u₄
inst✝³ : Category.{v₂, u₂} D
inst✝² : Category.{v₃, u₃} D'
inst✝¹ : Category.{v₄, u₄} E
H : D ⥤ V
L : D ⥤ D'
H' : D' ⥤ V
α : H ⟶ L ⋙ H'
K : E ⥤ V
d : D'
P : (Functor.LeftExtension.mk H' α).IsPointwiseLeftKanExtensionAt d
e : E
inst✝ : Limits.PreservesColimitsOfShape (CostructuredArrow L d) (tensorLeft (K.obj e))
cone : Limits.Cocone (CostructuredArrow.proj ((𝟭 E).prod L) (e, d) ⋙ K ⊠ H) :=
  (Functor.LeftExtension.mk (K ⊠ H') (extensionUnitRight H' α K)).coconeAt (e, d)
equiv : CostructuredArrow (𝟭 E) e × CostructuredArrow L d ≌ CostructuredArrow ((𝟭 E).prod L) (e, d) :=
  (CostructuredArrow.prodEquivalence (𝟭 E) L e d).symm
I : CostructuredArrow L d ⥤ CostructuredArrow (𝟭 E) e × CostructuredArrow L d :=
  (prod.leftUnitorEquivalence (CostructuredArrow L d)).inverse ⋙
    (Functor.fromPUnit (CostructuredArrow.mk (𝟙 ((𝟭 E).obj e)))).prod (𝟭 (CostructuredArrow L d))
this : I.Final := isPointwiseLeftKanExtensionAtExtensionUnitRight._proof_1 d e
⊢ Limits.IsColimit
    (Limits.Cocone.whisker equiv.functor
      ((Functor.LeftExtension.mk (K ⊠ H') (extensionUnitRight H' α K)).coconeAt (e, d)))

Tactic:
apply Functor.Final.isColimitWhiskerEquiv I (Limits.Cocone.whisker equiv.functor cone) |>.toFun

Goal state after:
V : Type u₁
inst✝⁵ : Category.{v₁, u₁} V
inst✝⁴ : MonoidalCategory V
D : Type u₂
D' : Type u₃
E : Type u₄
inst✝³ : Category.{v₂, u₂} D
inst✝² : Category.{v₃, u₃} D'
inst✝¹ : Category.{v₄, u₄} E
H : D ⥤ V
L : D ⥤ D'
H' : D' ⥤ V
α : H ⟶ L ⋙ H'
K : E ⥤ V
d : D'
P : (Functor.LeftExtension.mk H' α).IsPointwiseLeftKanExtensionAt d
e : E
inst✝ : Limits.PreservesColimitsOfShape (CostructuredArrow L d) (tensorLeft (K.obj e))
cone : Limits.Cocone (CostructuredArrow.proj ((𝟭 E).prod L) (e, d) ⋙ K ⊠ H) := ⋯
equiv : CostructuredArrow (𝟭 E) e × CostructuredArrow L d ≌ CostructuredArrow ((𝟭 E).prod L) (e, d) := ⋯
I : CostructuredArrow L d ⥤ CostructuredArrow (𝟭 E) e × CostructuredArrow L d := ⋯
this : I.Final := ⋯
⊢ Limits.IsColimit (Limits.Cocone.whisker I (Limits.Cocone.whisker equiv.functor cone))
Module: Mathlib.CategoryTheory.Monoidal.Hopf_

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
⊢ 𝒮 ≫ ε = ε

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

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
this : Δ ≫ 𝒮 ▷ A ≫ μ ≫ ε = Δ ≫ 𝒮 ▷ A ≫ μ ≫ ε
⊢ 𝒮 ≫ ε = ε
Module: Mathlib.CategoryTheory.Monoidal.Hopf_

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
this : Δ ≫ 𝒮 ▷ A ≫ A ◁ ε ≫ ε ▷ 𝟙_ C ≫ (λ_ (𝟙_ C)).hom = ε ≫ η ≫ ε
⊢ 𝒮 ≫ ε = ε

Tactic:
← whisker_exchange_assoc

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
this : Δ ≫ A ◁ ε ≫ 𝒮 ▷ 𝟙_ C ≫ ε ▷ 𝟙_ C ≫ (λ_ (𝟙_ C)).hom = ε ≫ η ≫ ε
⊢ 𝒮 ≫ ε = ε
Module: Mathlib.CategoryTheory.Monoidal.Internal.Module

Goal state before:
pp: case e'_3
R : Type u
inst✝¹ : CommRing R
A : ModuleCat R
inst✝ : MonObj A
x : ↑A
⊢ x = (Hom.hom (MonoidalCategoryStruct.leftUnitor A).hom) (1 ⊗ₜ[R] x)

Tactic:
MonoidalCategory.leftUnitor_hom_apply,

Goal state after:
case e'_3
R : Type u
inst✝¹ : CommRing R
A : ModuleCat R
inst✝ : MonObj A
x : ↑A
⊢ x = 1 • x
Module: Mathlib.CategoryTheory.Monoidal.Internal.Module

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
A : ModuleCat R
inst✝ : MonObj A
x y : R
h :
  (Hom.hom (MonoidalCategoryStruct.leftUnitor A).hom) (x ⊗ₜ[R] (ConcreteCategory.hom η) y) =
    (Hom.hom (MonoidalCategoryStruct.whiskerRight η A ≫ μ)) (x ⊗ₜ[R] (ConcreteCategory.hom η) y)
⊢ (Hom.hom η).toFun (x * y) = (Hom.hom η).toFun x * (Hom.hom η).toFun y

Tactic:
MonoidalCategory.leftUnitor_hom_apply,

Goal state after:
R : Type u
inst✝¹ : CommRing R
A : ModuleCat R
inst✝ : MonObj A
x y : R
h :
  x • (ConcreteCategory.hom η) y =
    (Hom.hom (MonoidalCategoryStruct.whiskerRight η A ≫ μ)) (x ⊗ₜ[R] (ConcreteCategory.hom η) y)
⊢ (Hom.hom η).toFun (x * y) = (Hom.hom η).toFun x * (Hom.hom η).toFun y
Module: Mathlib.CategoryTheory.Monoidal.Internal.Module

Goal state before:
pp: R : Type u
inst✝ : CommRing R
A : AlgCat R
x : ↑(of R ↑A)
⊢ (Hom.hom (↟(Algebra.linearMap R ↑A))) (1, x).1 * LinearMap.id (1, x).2 =
    (Hom.hom (MonoidalCategoryStruct.leftUnitor (of R ↑A)).hom)
      (((TensorProduct.mk R ↑(MonoidalCategoryStruct.tensorUnit (ModuleCat R)) ↑A) 1) x)

Tactic:
MonoidalCategory.leftUnitor_hom_apply,

Goal state after:
R : Type u
inst✝ : CommRing R
A : AlgCat R
x : ↑(of R ↑A)
⊢ (Hom.hom (↟(Algebra.linearMap R ↑A))) (1, x).1 * LinearMap.id (1, x).2 = 1 • x
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
H : C ⥤ V
inst✝⁸ : DayConvolution G H
inst✝⁷ : DayConvolution F (G ⊛ H)
inst✝⁶ : DayConvolution (F ⊛ G) H
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)
F' G' H' : C ⥤ V
inst✝³ : DayConvolution F' G'
inst✝² : DayConvolution G' H'
inst✝¹ : DayConvolution F' (G' ⊛ H')
inst✝ : DayConvolution (F' ⊛ G') H'
f : F ⟶ F'
g : G ⟶ G'
h : H ⟶ H'
x✝ : (C × C) × C
⊢ ((unit F G).app x✝.1 ≫ (map f g).app (x✝.1.1 ⊗ x✝.1.2)) ▷ H.obj x✝.2 ≫
      (F' ⊛ G').obj (x✝.1.1 ⊗ x✝.1.2) ◁ h.app x✝.2 ≫
        (unit (F' ⊛ G') H').app (x✝.1.1 ⊗ x✝.1.2, x✝.2) ≫ (associator F' G' H').hom.app ((x✝.1.1 ⊗ x✝.1.2) ⊗ x✝.2) =
    (α_ (F.obj x✝.1.1) (G.obj x✝.1.2) (H.obj x✝.2)).hom ≫
      F.obj x✝.1.1 ◁ (unit G H).app (x✝.1.2, x✝.2) ≫
        f.app x✝.1.1 ▷ (G ⊛ H).obj (x✝.1.2 ⊗ x✝.2) ≫
          F'.obj x✝.1.1 ◁ (map g h).app (x✝.1.2 ⊗ x✝.2) ≫
            (unit F' (G' ⊛ H')).app (x✝.1.1, x✝.1.2 ⊗ x✝.2) ≫ (F' ⊛ G' ⊛ H').map (α_ x✝.1.1 x✝.1.2 x✝.2).inv

Tactic:
unit_app_map_app

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
H : C ⥤ V
inst✝⁸ : DayConvolution G H
inst✝⁷ : DayConvolution F (G ⊛ H)
inst✝⁶ : DayConvolution (F ⊛ G) H
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)
F' G' H' : C ⥤ V
inst✝³ : DayConvolution F' G'
inst✝² : DayConvolution G' H'
inst✝¹ : DayConvolution F' (G' ⊛ H')
inst✝ : DayConvolution (F' ⊛ G') H'
f : F ⟶ F'
g : G ⟶ G'
h : H ⟶ H'
x✝ : (C × C) × C
⊢ ((f.app x✝.1.1 ⊗ₘ g.app x✝.1.2) ≫ (unit F' G').app (x✝.1.1, x✝.1.2)) ▷ H.obj x✝.2 ≫
      (F' ⊛ G').obj (x✝.1.1 ⊗ x✝.1.2) ◁ h.app x✝.2 ≫
        (unit (F' ⊛ G') H').app (x✝.1.1 ⊗ x✝.1.2, x✝.2) ≫ (associator F' G' H').hom.app ((x✝.1.1 ⊗ x✝.1.2) ⊗ x✝.2) =
    (α_ (F.obj x✝.1.1) (G.obj x✝.1.2) (H.obj x✝.2)).hom ≫
      F.obj x✝.1.1 ◁ (unit G H).app (x✝.1.2, x✝.2) ≫
        f.app x✝.1.1 ▷ (G ⊛ H).obj (x✝.1.2 ⊗ x✝.2) ≫
          F'.obj x✝.1.1 ◁ (map g h).app (x✝.1.2 ⊗ x✝.2) ≫
            (unit F' (G' ⊛ H')).app (x✝.1.1, x✝.1.2 ⊗ x✝.2) ≫ (F' ⊛ G' ⊛ H').map (α_ x✝.1.1 x✝.1.2 x✝.2).inv
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
H : C ⥤ V
inst✝⁸ : DayConvolution G H
inst✝⁷ : DayConvolution F (G ⊛ H)
inst✝⁶ : DayConvolution (F ⊛ G) H
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)
F' G' H' : C ⥤ V
inst✝³ : DayConvolution F' G'
inst✝² : DayConvolution G' H'
inst✝¹ : DayConvolution F' (G' ⊛ H')
inst✝ : DayConvolution (F' ⊛ G') H'
f : F ⟶ F'
g : G ⟶ G'
h : H ⟶ H'
x✝ : (C × C) × C
⊢ (f.app x✝.1.1 ⊗ₘ g.app x✝.1.2) ▷ H.obj x✝.2 ≫
      (F'.obj x✝.1.1 ⊗ G'.obj x✝.1.2) ◁ h.app x✝.2 ≫
        (α_ (F'.obj x✝.1.1) ((G', H').1.obj (x✝.1.2, x✝.2).1) ((G', H').2.obj (x✝.1.2, x✝.2).2)).hom ≫
          F'.obj x✝.1.1 ◁ (unit G' H').app (x✝.1.2, x✝.2) ≫
            (unit F' (G' ⊛ H')).app (x✝.1.1, x✝.1.2 ⊗ x✝.2) ≫
              (F' ⊛ G' ⊛ H').map (α_ (x✝.1.1, x✝.1.2 ⊗ x✝.2).1 x✝.1.2 x✝.2).inv =
    (α_ (F.obj x✝.1.1) (G.obj x✝.1.2) (H.obj x✝.2)).hom ≫
      f.app x✝.1.1 ▷ (G.obj x✝.1.2 ⊗ H.obj x✝.2) ≫
        F'.obj x✝.1.1 ◁ ((unit G H).app (x✝.1.2, x✝.2) ≫ (map g h).app (x✝.1.2 ⊗ x✝.2)) ≫
          (unit F' (G' ⊛ H')).app (x✝.1.1, x✝.1.2 ⊗ x✝.2) ≫ (F' ⊛ G' ⊛ H').map (α_ x✝.1.1 x✝.1.2 x✝.2).inv

Tactic:
unit_app_map_app

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
H : C ⥤ V
inst✝⁸ : DayConvolution G H
inst✝⁷ : DayConvolution F (G ⊛ H)
inst✝⁶ : DayConvolution (F ⊛ G) H
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)
F' G' H' : C ⥤ V
inst✝³ : DayConvolution F' G'
inst✝² : DayConvolution G' H'
inst✝¹ : DayConvolution F' (G' ⊛ H')
inst✝ : DayConvolution (F' ⊛ G') H'
f : F ⟶ F'
g : G ⟶ G'
h : H ⟶ H'
x✝ : (C × C) × C
⊢ (f.app x✝.1.1 ⊗ₘ g.app x✝.1.2) ▷ H.obj x✝.2 ≫
      (F'.obj x✝.1.1 ⊗ G'.obj x✝.1.2) ◁ h.app x✝.2 ≫
        (α_ (F'.obj x✝.1.1) ((G', H').1.obj (x✝.1.2, x✝.2).1) ((G', H').2.obj (x✝.1.2, x✝.2).2)).hom ≫
          F'.obj x✝.1.1 ◁ (unit G' H').app (x✝.1.2, x✝.2) ≫
            (unit F' (G' ⊛ H')).app (x✝.1.1, x✝.1.2 ⊗ x✝.2) ≫
              (F' ⊛ G' ⊛ H').map (α_ (x✝.1.1, x✝.1.2 ⊗ x✝.2).1 x✝.1.2 x✝.2).inv =
    (α_ (F.obj x✝.1.1) (G.obj x✝.1.2) (H.obj x✝.2)).hom ≫
      f.app x✝.1.1 ▷ (G.obj x✝.1.2 ⊗ H.obj x✝.2) ≫
        F'.obj x✝.1.1 ◁ ((g.app x✝.1.2 ⊗ₘ h.app x✝.2) ≫ (unit G' H').app (x✝.1.2, x✝.2)) ≫
          (unit F' (G' ⊛ H')).app (x✝.1.1, x✝.1.2 ⊗ x✝.2) ≫ (F' ⊛ G' ⊛ H').map (α_ x✝.1.1 x✝.1.2 x✝.2).inv
Module: Mathlib.CategoryTheory.Monoidal.Bimod

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

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

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

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 S.X (𝟙_ C)).hom

Tactic:
MonObj.mul_one

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

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

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

case a.a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : HasCoequalizers C
R S : Mon C
P : Bimod R S
| (α_ P.X S.X (𝟙_ C)).hom
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 Z : Mon C
M : Bimod X Y
N : Bimod Y Z
⊢ coequalizer.π (M.actRight ▷ N.X) ((α_ M.X Y.X N.X).hom ≫ M.X ◁ N.actLeft) ≫ (M.whiskerLeft (𝟙 N)).hom =
    coequalizer.π (M.actRight ▷ N.X) ((α_ M.X Y.X N.X).hom ≫ M.X ◁ N.actLeft) ≫ (𝟙 (M.tensorBimod N)).hom

Tactic:
simp [TensorBimod.X]

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 Z : Mon C
M : Bimod X Y
N : Bimod Y Z
⊢ coequalizer.π (M.actRight ▷ N.X) ((α_ M.X Y.X N.X).hom ≫ M.X ◁ N.actLeft) ≫ (whiskerRight (𝟙 M) N).hom =
    coequalizer.π (M.actRight ▷ N.X) ((α_ M.X Y.X N.X).hom ≫ M.X ◁ N.actLeft) ≫ (𝟙 (M.tensorBimod N)).hom

Tactic:
simp [TensorBimod.X]

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

Goal state before:
pp: case of_presieve
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✝
R : Presieve X✝
hR : R ∈ K.coverings X✝
h✝ : ∀ (U : C) (g : U ⟶ X✝), R g → sourceLocalClosure K P (g ≫ f)
ih :
  ∀ (U : C) (g : U ⟶ X✝),
    R g →
      ∀ (W : C) (g_1 : Y ⟶ Y✝) (fst : W ⟶ U) (snd : W ⟶ Y), IsPullback fst snd (g ≫ f) g_1 → sourceLocalClosure K P snd
W : C
g : Y ⟶ Y✝
fst : W ⟶ X✝
snd : W ⟶ Y
h : IsPullback fst snd f g
U : C
⊢ ∀ (g : U ⟶ W), Presieve.pullbackArrows fst R g → sourceLocalClosure K P (g ≫ snd)

Tactic:
v

Goal state after:
case of_presieve
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✝
R : Presieve X✝
hR : R ∈ K.coverings X✝
h✝ : ∀ (U : C) (g : U ⟶ X✝), R g → sourceLocalClosure K P (g ≫ f)
ih :
  ∀ (U : C) (g : U ⟶ X✝),
    R g →
      ∀ (W : C) (g_1 : Y ⟶ Y✝) (fst : W ⟶ U) (snd : W ⟶ Y), IsPullback fst snd (g ≫ f) g_1 → sourceLocalClosure K P snd
W : C
g : Y ⟶ Y✝
fst : W ⟶ X✝
snd : W ⟶ Y
h : IsPullback fst snd f g
U : C
v : U ⟶ W
⊢ Presieve.pullbackArrows fst R v → sourceLocalClosure K P (v ≫ snd)
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
⊢ ∀ (g_1 : U ⟶ X'✝), (Precoverage.ZeroHypercover.pushforward (Arrow.Hom.left e.hom) ⋯ E).presieve₀ g_1 → P (g_1 ≫ g)

Tactic:
v

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'✝
⊢ (Precoverage.ZeroHypercover.pushforward (Arrow.Hom.left e.hom) ⋯ E).presieve₀ v → P (v ≫ g)
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 ((E.f i ≫ f) ≫ Arrow.Hom.right e.hom)

Tactic:
P.cancel_right_of_respectsIso

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 ≫ f)
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
⊢ ∀ (g_1 : U ⟶ U✝), (Precoverage.ZeroHypercover.pullback₁ g E).presieve₀ g_1 → P (g_1 ≫ g ≫ f)

Tactic:
v

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✝
⊢ (Precoverage.ZeroHypercover.pullback₁ g E).presieve₀ v → P (v ≫ 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✝
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)
this : MonoidalCategoryStruct D := mkMonoidalCategoryStruct C V D
⊢ ∀ {d₁ d₂ d₁' d₂' : D} (f₁ : d₁ ⟶ d₁') (f₂ : d₂ ⟶ d₂') (x y : C),
    (DayConvolution.unit ((ι C V D).obj d₁) ((ι C V D).obj d₂)).app (x, y) ≫ ((ι C V D).map (f₁ ⊗ₘ f₂)).app (x ⊗ y) =
      (((ι C V D).map f₁).app x ⊗ₘ ((ι C V D).map f₂).app y) ≫
        (DayConvolution.unit ((ι C V D).obj d₁') ((ι C V D).obj d₂')).app (x, y)

Tactic:
by
      intros d₁ d₁' d₂ d₂' f f' x y
      simp [ι_map_tensorHom_eq C V D f f']

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P : ObjectProperty C
X Y : C
f : X ⟶ Y
inst✝ : Epi f
Z : C
hZ : P Z
u : Y ⟶ Z
⊢ ∀ ⦃a₂ : Y ⟶ Z⦄, (fun g ↦ f ≫ g) u = (fun g ↦ f ≫ g) a₂ → u = a₂

Tactic:
v

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P : ObjectProperty C
X Y : C
f : X ⟶ Y
inst✝ : Epi f
Z : C
hZ : P Z
u v : Y ⟶ Z
⊢ (fun g ↦ f ≫ g) u = (fun g ↦ f ≫ g) v → u = v
Module: Mathlib.CategoryTheory.MorphismProperty.LocalEpi

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
P : ObjectProperty C
X Y : C
f : X ⟶ Y
hf : P.localEpi f
Z T : C
hT : P T
e : Z ≅ T
u : Y ⟶ Z
⊢ ∀ ⦃a₂ : Y ⟶ Z⦄, (fun g ↦ f ≫ g) u = (fun g ↦ f ≫ g) a₂ → u = a₂

Tactic:
v

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
P : ObjectProperty C
X Y : C
f : X ⟶ Y
hf : P.localEpi f
Z T : C
hT : P T
e : Z ≅ T
u v : Y ⟶ Z
⊢ (fun g ↦ f ≫ g) u = (fun g ↦ f ≫ g) v → u = v
Module: Mathlib.CategoryTheory.Preadditive.Comma

Goal state before:
pp: case h₁
A : Type u₁
inst✝⁷ : Category.{v₁, u₁} A
inst✝⁶ : Preadditive A
B : Type u₂
inst✝⁵ : Category.{v₂, u₂} B
inst✝⁴ : Preadditive B
T : Type u₃
inst✝³ : Category.{v₃, u₃} T
inst✝² : Preadditive T
L : A ⥤ T
inst✝¹ : L.Additive
R : B ⥤ T
inst✝ : R.Additive
u v : Comma L R
x✝¹ x✝ : u ⟶ v
⊢ (x✝¹ - x✝).left = (x✝¹ + -x✝).left

Tactic:
simp [sub_eq_add_neg]

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Comma

Goal state before:
pp: case h₂
A : Type u₁
inst✝⁷ : Category.{v₁, u₁} A
inst✝⁶ : Preadditive A
B : Type u₂
inst✝⁵ : Category.{v₂, u₂} B
inst✝⁴ : Preadditive B
T : Type u₃
inst✝³ : Category.{v₃, u₃} T
inst✝² : Preadditive T
L : A ⥤ T
inst✝¹ : L.Additive
R : B ⥤ T
inst✝ : R.Additive
u v : Comma L R
x✝¹ x✝ : u ⟶ v
⊢ (x✝¹ - x✝).right = (x✝¹ + -x✝).right

Tactic:
simp [sub_eq_add_neg]

Goal state after: