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

Goal state before:
pp: case hac
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
inst✝³ : BraidedCategory C
A B : C
inst✝² : HopfObj A
inst✝¹ : HopfObj B
f : A ⟶ B
inst✝ : IsBimonHom f
⊢ f * 𝒮 ≫ f = 1

Tactic:
Conv.mul_eq,

Goal state after:
case hac
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
inst✝³ : BraidedCategory C
A B : C
inst✝² : HopfObj A
inst✝¹ : HopfObj B
f : A ⟶ B
inst✝ : IsBimonHom f
⊢ Δ ≫ f ▷ A ≫ B ◁ (𝒮 ≫ f) ≫ μ = 1
Module: Mathlib.CategoryTheory.Monoidal.Hopf_

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

Tactic:
Conv.mul_eq,

Goal state after:
case hba
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
⊢ Δ ≫ (𝒮 ≫ Δ) ▷ A ≫ (A ⊗ A) ◁ Δ ≫ μ = 1
Module: Mathlib.CategoryTheory.Monoidal.Hopf_

Goal state before:
pp: case hac
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
⊢ Δ * Δ ≫ (β_ A A).hom ≫ (𝒮 ⊗ₘ 𝒮) = 1

Tactic:
Conv.mul_eq,

Goal state after:
case hac
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
⊢ Δ ≫ Δ ▷ A ≫ (A ⊗ A) ◁ (Δ ≫ (β_ A A).hom ≫ (𝒮 ⊗ₘ 𝒮)) ≫ μ = 1
Module: Mathlib.CategoryTheory.Monoidal.Hopf_

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

Tactic:
Conv.mul_eq,

Goal state after:
case hba
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
⊢ Δ ≫ (μ ≫ 𝒮) ▷ (A ⊗ A) ≫ A ◁ μ ≫ μ = 1
Module: Mathlib.CategoryTheory.Monoidal.Hopf_

Goal state before:
pp: case hac
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
⊢ μ * (𝒮 ⊗ₘ 𝒮) ≫ (β_ A A).hom ≫ μ = 1

Tactic:
Conv.mul_eq,

Goal state after:
case hac
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
⊢ Δ ≫ μ ▷ (A ⊗ A) ≫ A ◁ ((𝒮 ⊗ₘ 𝒮) ≫ (β_ A A).hom ≫ μ) ≫ μ = 1
Module: Mathlib.CategoryTheory.Monoidal.Hopf_

Goal state before:
pp: case hba
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
comm : (β_ A A).hom ≫ μ = μ
⊢ 𝒮 ≫ 𝒮 * 𝒮 = 1

Tactic:
Conv.mul_eq,

Goal state after:
case hba
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
comm : (β_ A A).hom ≫ μ = μ
⊢ Δ ≫ (𝒮 ≫ 𝒮) ▷ A ≫ A ◁ 𝒮 ≫ μ = 1
Module: Mathlib.CategoryTheory.Monoidal.Hopf_

Goal state before:
pp: case hac
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
comm : (β_ A A).hom ≫ μ = μ
⊢ 𝒮 * 𝟙 A = 1

Tactic:
Conv.mul_eq,

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
A : ModuleCat R
inst✝ : MonObj A
x : ↑A
⊢ (ConcreteCategory.hom μ) (x ⊗ₜ[R] 0) = 0

Tactic:
TensorProduct.tmul_zero,

Goal state after:
R : Type u
inst✝¹ : CommRing R
A : ModuleCat R
inst✝ : MonObj A
x : ↑A
⊢ (ConcreteCategory.hom μ) 0 = 0
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
⊢ ∀ {Y Y' : C ⥤ V} (g : Y ⟶ Y') (f : F ⊛ G ⟶ Y),
    ((F ⊛ G).homEquivOfIsLeftKanExtension (unit F G) Y') (f ≫ g) =
      (ConcreteCategory.hom
          (((Functor.whiskeringLeft (C × C) C V).obj (tensor C) ⋙ coyoneda.obj (Opposite.op (F ⊠ G))).map g))
        (((F ⊛ G).homEquivOfIsLeftKanExtension (unit F G) Y) f)

Tactic:
by aesop

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
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)
⊢ ∀ {Y Y' : C ⥤ V} (g : Y ⟶ Y') (f : F ⊛ G ⊛ H ⟶ Y),
    ((corepresentableBy F (G ⊛ H)).homEquiv.trans
          ((F ⊠ G ⊛ H).homEquivOfIsLeftKanExtension (extensionUnitRight (G ⊛ H) (unit G H) F)
            (((whiskeringLeft (C × C) C V).obj (tensor C)).obj Y')))
        (f ≫ g) =
      (ConcreteCategory.hom
          (((whiskeringLeft (C × C) C V).obj (tensor C) ⋙
                (whiskeringLeft (C × C × C) (C × C) V).obj ((𝟭 C).prod (tensor C)) ⋙
                  coyoneda.obj (Opposite.op (F ⊠ G ⊠ H))).map
            g))
        (((corepresentableBy F (G ⊛ H)).homEquiv.trans
            ((F ⊠ G ⊛ H).homEquivOfIsLeftKanExtension (extensionUnitRight (G ⊛ H) (unit G H) F)
              (((whiskeringLeft (C × C) C V).obj (tensor C)).obj Y)))
          f)

Tactic:
by aesop

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
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)
⊢ ∀ {Y Y' : C ⥤ V} (g : Y ⟶ Y') (f : (F ⊛ G) ⊛ H ⟶ Y),
    ((corepresentableBy (F ⊛ G) H).homEquiv.trans
          (((F ⊛ G) ⊠ H).homEquivOfIsLeftKanExtension (extensionUnitLeft (F ⊛ G) (unit F G) H)
            (((whiskeringLeft (C × C) C V).obj (tensor C)).obj Y')))
        (f ≫ g) =
      (ConcreteCategory.hom
          (((whiskeringLeft (C × C) C V).obj (tensor C) ⋙
                (whiskeringLeft ((C × C) × C) (C × C) V).obj ((tensor C).prod (𝟭 C)) ⋙
                  coyoneda.obj (Opposite.op ((F ⊠ G) ⊠ H))).map
            g))
        (((corepresentableBy (F ⊛ G) H).homEquiv.trans
            (((F ⊛ G) ⊠ H).homEquivOfIsLeftKanExtension (extensionUnitLeft (F ⊛ G) (unit F G) H)
              (((whiskeringLeft (C × C) C V).obj (tensor C)).obj Y)))
          f)

Tactic:
by aesop

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✝¹ : ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (fromPUnit (𝟙_ C)) d) (tensorRight v)
inst✝ : DayConvolution U F
⊢ ∀ {Y Y' : C ⥤ V} (g : Y ⟶ Y') (f : U ⊛ F ⟶ Y),
    (((U ⊛ F).homEquivOfIsLeftKanExtension (DayConvolution.unit U F) Y').trans
          ((U ⊠ F).homEquivOfIsLeftKanExtension (extensionUnitLeft U (φ U) F) (tensor C ⋙ Y')))
        (f ≫ g) =
      (ConcreteCategory.hom
          (((whiskeringLeft (C × C) C V).obj (tensor C) ⋙
                (whiskeringLeft (Discrete PUnit.{1} × C) (C × C) V).obj ((fromPUnit (𝟙_ C)).prod (𝟭 C)) ⋙
                  coyoneda.obj (Opposite.op (fromPUnit (𝟙_ V) ⊠ F))).map
            g))
        ((((U ⊛ F).homEquivOfIsLeftKanExtension (DayConvolution.unit U F) Y).trans
            ((U ⊠ F).homEquivOfIsLeftKanExtension (extensionUnitLeft U (φ U) F) (tensor C ⋙ Y)))
          f)

Tactic:
by aesop

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✝¹ : ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (fromPUnit (𝟙_ C)) d) (tensorRight v)
inst✝ : DayConvolution F U
⊢ ∀ {Y Y' : C ⥤ V} (g : Y ⟶ Y') (f : F ⊛ U ⟶ Y),
    (((F ⊛ U).homEquivOfIsLeftKanExtension (DayConvolution.unit F U) Y').trans
          ((F ⊠ U).homEquivOfIsLeftKanExtension (extensionUnitRight U (φ U) F) (tensor C ⋙ Y')))
        (f ≫ g) =
      (ConcreteCategory.hom
          (((whiskeringLeft (C × C) C V).obj (tensor C) ⋙
                (whiskeringLeft (C × Discrete PUnit.{1}) (C × C) V).obj ((𝟭 C).prod (fromPUnit (𝟙_ C))) ⋙
                  coyoneda.obj (Opposite.op (F ⊠ fromPUnit (𝟙_ V)))).map
            g))
        ((((F ⊛ U).homEquivOfIsLeftKanExtension (DayConvolution.unit F U) Y).trans
            ((F ⊠ U).homEquivOfIsLeftKanExtension (extensionUnitRight U (φ U) F) (tensor C ⋙ Y)))
          f)

Tactic:
by aesop

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
D : Type u₃
inst✝³ : Category.{v₃, u₃} D
inst✝² : MonoidalCategoryStruct D
inst✝¹ : LawfulDayConvolutionMonoidalCategoryStruct C V D
d : D
inst✝ :
  ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (𝟙_ C)) d) (tensorRight v)
⊢ (((ι C V D).obj (𝟙_ D) ⊠ (ι C V D).obj d).homEquivOfIsLeftKanExtension
        (ExternalProduct.extensionUnitLeft ((ι C V D).obj (𝟙_ D)) (φ ((ι C V D).obj (𝟙_ D))) ((ι C V D).obj d))
        (tensor C ⋙ (ι C V D).obj d))
      ((((ι C V D).obj (𝟙_ D) ⊛ (ι C V D).obj d).homEquivOfIsLeftKanExtension
          (DayConvolution.unit ((ι C V D).obj (𝟙_ D)) ((ι C V D).obj d)) ((ι C V D).obj d))
        ((ι C V D).map (λ_ d).hom)) =
    (((ι C V D).obj (𝟙_ D) ⊠ (ι C V D).obj d).homEquivOfIsLeftKanExtension
        (ExternalProduct.extensionUnitLeft ((ι C V D).obj (𝟙_ D)) (φ ((ι C V D).obj (𝟙_ D))) ((ι C V D).obj d))
        (tensor C ⋙ (ι C V D).obj d))
      ((((ι C V D).obj (𝟙_ D) ⊛ (ι C V D).obj d).homEquivOfIsLeftKanExtension
          (DayConvolution.unit ((ι C V D).obj (𝟙_ D)) ((ι C V D).obj d)) ((ι C V D).obj d))
        (DayConvolutionUnit.leftUnitor ((ι C V D).obj (𝟙_ D)) ((ι C V D).obj d)).hom)

Tactic:
ext ⟨_, x⟩

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✝² : MonoidalCategoryStruct D
inst✝¹ : LawfulDayConvolutionMonoidalCategoryStruct C V D
d : D
inst✝ :
  ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (𝟙_ C)) d) (tensorRight v)
fst✝ : Discrete PUnit.{1}
x : C
⊢ ((((ι C V D).obj (𝟙_ D) ⊠ (ι C V D).obj d).homEquivOfIsLeftKanExtension
            (ExternalProduct.extensionUnitLeft ((ι C V D).obj (𝟙_ D)) (φ ((ι C V D).obj (𝟙_ D))) ((ι C V D).obj d))
            (tensor C ⋙ (ι C V D).obj d))
          ((((ι C V D).obj (𝟙_ D) ⊛ (ι C V D).obj d).homEquivOfIsLeftKanExtension
              (DayConvolution.unit ((ι C V D).obj (𝟙_ D)) ((ι C V D).obj d)) ((ι C V D).obj d))
            ((ι C V D).map (λ_ d).hom))).app
      (fst✝, x) =
    ((((ι C V D).obj (𝟙_ D) ⊠ (ι C V D).obj d).homEquivOfIsLeftKanExtension
            (ExternalProduct.extensionUnitLeft ((ι C V D).obj (𝟙_ D)) (φ ((ι C V D).obj (𝟙_ D))) ((ι C V D).obj d))
            (tensor C ⋙ (ι C V D).obj d))
          ((((ι C V D).obj (𝟙_ D) ⊛ (ι C V D).obj d).homEquivOfIsLeftKanExtension
              (DayConvolution.unit ((ι C V D).obj (𝟙_ D)) ((ι C V D).obj d)) ((ι C V D).obj d))
            (DayConvolutionUnit.leftUnitor ((ι C V D).obj (𝟙_ D)) ((ι C V D).obj d)).hom)).app
      (fst✝, x)
Module: Mathlib.CategoryTheory.MorphismProperty.Ind

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
X Y : C
f : X ⟶ Y
x✝ : P.ind f
J : Type w
w✝¹ : SmallCategory J
w✝ : IsFiltered J
D : J ⥤ C
t : (Functor.const J).obj X ⟶ D
s : D ⟶ (Functor.const J).obj Y
hs : IsColimit { pt := Y, ι := s }
hst : ∀ (j : J), P (t.app j) ∧ t.app j ≫ s.app j = f
j : J
⊢ ((Under.lift D t).obj j).hom ≫ s.app j = (((Functor.const J).obj (CategoryTheory.Under.mk f)).obj j).hom

Tactic:
by simp [hst]

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
X Y : C
f : X ⟶ Y
x✝ : P.ind f
J : Type w
w✝¹ : SmallCategory J
w✝ : IsFiltered J
D : J ⥤ C
t : (Functor.const J).obj X ⟶ D
s : D ⟶ (Functor.const J).obj Y
hs : IsColimit { pt := Y, ι := s }
hst : ∀ (j : J), P (t.app j) ∧ t.app j ≫ s.app j = f
this : Nonempty J
⊢ ∀ (j : J), t.app j ≫ { pt := Y, ι := s }.ι.app j = f

Tactic:
by simp [hst]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P Q : MorphismProperty C
inst✝ : P.RespectsLeft Q
X Y Z : C
i : X ⟶ Y
hi : Q i
f : Y ⟶ Z
x✝ : P.ind f
J : Type u_1
w✝¹ : SmallCategory J
w✝ : IsFiltered J
D : J ⥤ C
t : (Functor.const J).obj Y ⟶ D
s : D ⟶ (Functor.const J).obj Z
hs : IsColimit { pt := Z, ι := s }
hst : ∀ (j : J), P (t.app j) ∧ t.app j ≫ s.app j = f
j : J
⊢ ((Functor.const J).map i ≫ t).app j ≫ s.app j = i ≫ f

Tactic:
by simp [hst]

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

Goal state before:
pp: case refine_2
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝¹ : G.Faithful
inst✝ : G.Full
X Y : C
f : X ⟶ Y
h : Epi (F.map f)
Z : D
u v : G.obj (F.obj Y) ⟶ G.obj Z
huv : (fun g ↦ G.map (F.map f) ≫ g) u = (fun g ↦ G.map (F.map f) ≫ g) v
⊢ u = v

Tactic:
obtain ⟨u, rfl⟩ := G.map_surjective u

Goal state after:
case refine_2
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝¹ : G.Faithful
inst✝ : G.Full
X Y : C
f : X ⟶ Y
h : Epi (F.map f)
Z : D
v : G.obj (F.obj Y) ⟶ G.obj Z
u : F.obj Y ⟶ Z
huv : (fun g ↦ G.map (F.map f) ≫ g) (G.map u) = (fun g ↦ G.map (F.map f) ≫ g) v
⊢ G.map u = v
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
⊢ f.hom ▷ Y.X ≫ colimit.ι (parallelPair (N.actRight ▷ Y.X) ((α_ N.X Y.X Y.X).hom ≫ N.X ◁ μ)) WalkingParallelPair.one =
    (M.actRight ≫ f.hom) ≫ RightUnitorBimod.inv N

Tactic:
dsimp [RightUnitorBimod.inv]

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
⊢ f.hom ▷ Y.X ≫ colimit.ι (parallelPair (N.actRight ▷ Y.X) ((α_ N.X Y.X Y.X).hom ≫ N.X ◁ μ)) WalkingParallelPair.one =
    (M.actRight ≫ f.hom) ≫ (ρ_ N.X).inv ≫ N.X ◁ η ≫ coequalizer.π (N.actRight ▷ Y.X) ((α_ N.X Y.X Y.X).hom ≫ N.X ◁ μ)
Module: Mathlib.CategoryTheory.Preadditive.FreydCategory.RightFreyd

Goal state before:
pp: V : Type u_1
inst✝² : Category.{v_1, u_1} V
inst✝¹ : Preadditive V
u v : Arrow V
f : u ⟶ v
inst✝ : IsIso (Hom.right f)
Z✝ : RightFreyd V
g₂ : (quotient V).obj v ⟶ Z✝
g₁ : v ⟶ Z✝.as
eq : (quotient V).map f ≫ (quotient V).map g₁ = (quotient V).map f ≫ g₂
⊢ (quotient V).map g₁ = g₂

Tactic:
obtain ⟨g₂, rfl⟩ := (quotient V).map_surjective g₂

Goal state after:
V : Type u_1
inst✝² : Category.{v_1, u_1} V
inst✝¹ : Preadditive V
u v : Arrow V
f : u ⟶ v
inst✝ : IsIso (Hom.right f)
Z✝ : RightFreyd V
g₁ g₂ : v ⟶ Z✝.as
eq : (quotient V).map f ≫ (quotient V).map g₁ = (quotient V).map f ≫ (quotient V).map g₂
⊢ (quotient V).map g₁ = (quotient V).map g₂
Module: Mathlib.CategoryTheory.Preadditive.Comma

Goal state before:
pp: 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✝¹ + 1) • x✝ = x✝¹ • x✝ + x✝

Tactic:
simp_rw [HSMul.hSMul, SMul.smul]; ext <;> dsimp <;> simp [add_nsmul]

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

Goal state before:
pp: case refine_1.refine_2
κ : Cardinal.{u}
inst✝¹ : Fact κ.IsRegular
J : CardinalDirectedPoset κ
κ' : Cardinal.{u}
inst✝ : Fact κ'.IsRegular
hJ : HasCardinalLT (↑J.obj) κ'
h : κ ≤ κ'
A : Type u
x✝¹ : SmallCategory A
x✝ : IsCardinalFiltered A κ'
F : A ⥤ CardinalDirectedPoset κ
c : Cocone F
this✝ : IsFiltered A
this : IsCardinalFiltered A κ
hc : IsColimit ((forget (CardinalDirectedPoset κ)).mapCocone c)
f : J ⟶ c.pt
j : ↑J.obj → A
g : (x : ↑J.obj) → (fun X ↦ X) ((F ⋙ forget (CardinalDirectedPoset κ)).obj (j x))
hg :
  ∀ (x : ↑J.obj),
    (ConcreteCategory.hom (((forget (CardinalDirectedPoset κ)).mapCocone c).ι.app (j x))) (g x) =
      (ConcreteCategory.hom f) x
m : A := IsCardinalFiltered.max j hJ
φ : ↑J.obj → ↑(F.obj m).obj := fun x ↦ (ConcreteCategory.hom (F.map (IsCardinalFiltered.toMax j hJ x))) (g x)
hφ : ∀ (x : ↑J.obj), (ConcreteCategory.hom f) x = (ConcreteCategory.hom (c.ι.app m)) (φ x)
⊢ f =
    (ConcreteCategory.hom (((coyoneda.obj (Opposite.op J)).mapCocone c).ι.app m))
      (ObjectProperty.homMk (PartOrdEmb.ofHom { toFun := φ, inj' := ⋯, map_rel_iff' := ⋯ }))

Tactic:
· dsimp
        ext x
        trans c.ι.app (j x) (g x)
        · exact (hg x).symm
        · exact (ConcreteCategory.congr_hom (c.w (IsCardinalFiltered.toMax j hJ x)).symm (g x))

Goal state after:
Module: Mathlib.Order.Category.PartOrdEmb

Goal state before:
pp: α : PartOrdEmb
P : Set ↑α → Prop
X✝ Y✝ : Subtype P
f : X✝ ⟶ Y✝
x✝² x✝¹ : ↑↑X✝
x✝ : (fun x ↦ ⟨↑x, ⋯⟩) x✝² = (fun x ↦ ⟨↑x, ⋯⟩) x✝¹
⊢ x✝² = x✝¹

Tactic:
by aesop

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

Goal state before:
pp: J : Type w
inst✝ : SmallCategory J
κ : Cardinal.{w}
D₁ : Diagram J κ
top : J
h₁ : D₁.IsTerminal top
h₁' : ∀ (j : J) (hj : D₁.IsTerminal j), j = top
D₂ : Diagram J κ
top' : J
h₂ : D₂.IsTerminal top'
h₂' : ∀ (j : J) (hj : D₂.IsTerminal j), j = top'
hW :
  { toDiagram := D₁, top := top, isTerminal := h₁, uniq_terminal := h₁' }.W =
    { toDiagram := D₂, top := top', isTerminal := h₂, uniq_terminal := h₂' }.W
hP :
  { toDiagram := D₁, top := top, isTerminal := h₁, uniq_terminal := h₁' }.P =
    { toDiagram := D₂, top := top', isTerminal := h₂, uniq_terminal := h₂' }.P
⊢ D₁ = D₂

Tactic:
by aesop

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

Goal state before:
pp: κ : Cardinal.{u}
inst✝¹ : Fact κ.IsRegular
J : CardinalDirectedPoset κ
κ' : Cardinal.{u}
inst✝ : Fact κ'.IsRegular
a : ↑J.obj
⊢ some a ∈ {↑a, ⊤}

Tactic:
by aesop

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

Goal state before:
pp: J : Type w
inst✝¹ : SmallCategory J
κ : Cardinal.{w}
inst✝ : Fact κ.IsRegular
j : J
x✝ : Subtype (ObjectProperty.ofObj fun x ↦ j)
k : J
hk : ObjectProperty.ofObj (fun x ↦ j) k
⊢ (fun x ↦ ⟨j, ⋯⟩) PUnit.unit = ⟨k, hk⟩

Tactic:
by aesop

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

Goal state before:
pp: κ : Cardinal.{u}
inst✝¹ : Fact κ.IsRegular
J : CardinalDirectedPoset κ
κ' : Cardinal.{u}
inst✝ : Fact κ'.IsRegular
⊢ none ∈ {↑(Classical.arbitrary ↑J.obj), ⊤}

Tactic:
by aesop

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

Goal state before:
pp: case refine_2
J : Type w
inst✝¹ : SmallCategory J
κ : Cardinal.{w}
inst✝ : Fact κ.IsRegular
j x✝² : J
h₁ : __Diagram✝.P x✝²
x✝¹ x✝ : x✝² ⟶ j
h₂ : __Diagram✝.W x✝¹
h₃ : __Diagram✝.W x✝
⊢ x✝¹ = x✝

pp: case refine_3
J : Type w
inst✝¹ : SmallCategory J
κ : Cardinal.{w}
inst✝ : Fact κ.IsRegular
j x✝² x✝¹ : J
x✝ : x✝² ⟶ x✝¹
h : __Diagram✝.W x✝
⊢ ∃ li lj, __Diagram✝.W li ∧ __Diagram✝.W lj ∧ x✝ ≫ lj = li

Tactic:
· simp only [Diagram.single_P, ObjectProperty.singleton_iff] at h₁
      subst h₁
      obtain ⟨⟨⟩⟩ := h₂
      obtain ⟨⟨⟩⟩ := h₃
      simp

Goal state after:
case refine_3
J : Type w
inst✝¹ : SmallCategory J
κ : Cardinal.{w}
inst✝ : Fact κ.IsRegular
j x✝² x✝¹ : J
x✝ : x✝² ⟶ x✝¹
h : __Diagram✝.W x✝
⊢ ∃ li lj, __Diagram✝.W li ∧ __Diagram✝.W lj ∧ x✝ ≫ lj = li
Module: Mathlib.CategoryTheory.Presentable.OrthogonalReflection

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
W : MorphismProperty C
Z : C
inst✝³ : HasCoproduct D₁.obj₁
inst✝² : HasCoproduct D₁.obj₂
inst✝¹ : HasPushouts C
inst✝ : HasMulticoequalizer (D₂.multispanIndex W Z)
X Y : C
f : X ⟶ Y
hf : W f
g₁ g₂ : Y ⟶ Z
hg : f ≫ g₁ = f ≫ g₂
⊢ g₁ ≫ toSucc W Z = g₂ ≫ toSucc W Z

Tactic:
simpa using D₂.condition f hf (g₁ := g₁ ≫ toStep W Z) (g₂ := g₂ ≫ toStep W Z)
    (by simp [reassoc_of% hg])

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

Goal state before:
pp: J : Type w
inst✝² : SmallCategory J
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
hJ : ∀ (e : J), ∃ m x, IsEmpty (m ⟶ e)
ι : Type w
D : ι → DiagramWithUniqueTerminal J κ
hι : HasCardinalLT ι κ
m₀ : ι → J
t₀ : (i : ι) → (D i).top ⟶ m₀ i
hm₀ : ∀ (i : ι), IsEmpty (m₀ i ⟶ (D i).top)
m₁ : J := max m₀ hι
t₁ : (i : ι) → m₀ i ⟶ m₁ := fun i ↦ toMax m₀ hι i
u : (i : ι) → (D i).top ⟶ m₁ := fun i ↦ t₀ i ≫ t₁ i
⊢ ∃ m u,
    (∀ (i : ι), IsEmpty (m ⟶ (D i).top)) ∧
      ∀ (i₁ i₂ : ι) (j : J) (hj₁ : (D i₁).P j) (hj₂ : (D i₂).P j),
        (D i₁).isTerminal.lift hj₁ ≫ u i₁ = (D i₂).isTerminal.lift hj₂ ≫ u i₂

Tactic:
let S := { x : ι × ι × J // (D x.1).P x.2.2 ∧ (D x.2.1).P x.2.2 }

Goal state after:
J : Type w
inst✝² : SmallCategory J
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
hJ : ∀ (e : J), ∃ m x, IsEmpty (m ⟶ e)
ι : Type w
D : ι → DiagramWithUniqueTerminal J κ
hι : HasCardinalLT ι κ
m₀ : ι → J
t₀ : (i : ι) → (D i).top ⟶ m₀ i
hm₀ : ∀ (i : ι), IsEmpty (m₀ i ⟶ (D i).top)
m₁ : J := max m₀ hι
t₁ : (i : ι) → m₀ i ⟶ m₁ := fun i ↦ toMax m₀ hι i
u : (i : ι) → (D i).top ⟶ m₁ := fun i ↦ t₀ i ≫ t₁ i
S : Type (max 0 w) := { x // (D x.1).P x.2.2 ∧ (D x.2.1).P x.2.2 }
⊢ ∃ m u,
    (∀ (i : ι), IsEmpty (m ⟶ (D i).top)) ∧
      ∀ (i₁ i₂ : ι) (j : J) (hj₁ : (D i₁).P j) (hj₂ : (D i₂).P j),
        (D i₁).isTerminal.lift hj₁ ≫ u i₁ = (D i₂).isTerminal.lift hj₂ ≫ u i₂
Module: Mathlib.CategoryTheory.Presentable.OrthogonalReflection

Goal state before:
pp: case refine_2
C : Type u
inst✝⁴ : Category.{v, u} C
W : MorphismProperty C
Z : C
inst✝³ : HasCoproduct D₁.obj₁
inst✝² : HasCoproduct D₁.obj₂
inst✝¹ : HasPushouts C
inst✝ : HasMulticoequalizer (D₂.multispanIndex W Z)
T : C
hT : W.isLocal T
g : Z ⟶ T
⊢ ∃ a, (fun g ↦ toSucc W Z ≫ g) a = g

Tactic:
choose f hf using fun (d : D₁ W Z) ↦ (hT d.1.1.hom d.1.2).2 (d.2 ≫ g)
    exact ⟨Multicoequalizer.desc _ _ (fun ⟨⟩ ↦ pushout.desc (Sigma.desc f) g)
      (fun d ↦ (hT d.1.1.hom d.1.2).1 (by simp [reassoc_of% d.2.2])), by simp⟩

Goal state after: