mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.GradedObject.Braiding

Goal state before:
pp: I : Type u_1
inst✝²⁰ : AddCommMonoid I
C : Type u_2
inst✝¹⁹ : Category.{v_1, u_2} C
inst✝¹⁸ : MonoidalCategory C
X Y Z : GradedObject I C
inst✝¹⁷ : BraidedCategory C
inst✝¹⁶ : X.HasTensor Y
inst✝¹⁵ : Y.HasTensor Z
inst✝¹⁴ : Z.HasTensor X
inst✝¹³ : Z.HasTensor Y
inst✝¹² : X.HasTensor Z
inst✝¹¹ : (tensorObj X Y).HasTensor Z
inst✝¹⁰ : X.HasTensor (tensorObj Y Z)
inst✝⁹ : Z.HasTensor (tensorObj X Y)
inst✝⁸ : (tensorObj Z X).HasTensor Y
inst✝⁷ : X.HasTensor (tensorObj Z Y)
inst✝⁶ : (tensorObj X Z).HasTensor Y
inst✝⁵ : X.HasGoodTensor₁₂Tensor Y Z
inst✝⁴ : X.HasGoodTensorTensor₂₃ Y Z
inst✝³ : Z.HasGoodTensor₁₂Tensor X Y
inst✝² : Z.HasGoodTensorTensor₂₃ X Y
inst✝¹ : X.HasGoodTensor₁₂Tensor Z Y
inst✝ : X.HasGoodTensorTensor₂₃ Z Y
⊢ (associator X Y Z).inv ≫ (braiding (tensorObj X Y) Z).hom ≫ (associator Z X Y).inv =
    whiskerLeft X (braiding Y Z).hom ≫ (associator X Z Y).inv ≫ whiskerRight (braiding X Z).hom Y

Tactic:
ext k i₁ i₂ i₃ h

Goal state after:
I : Type u_1
inst✝²⁰ : AddCommMonoid I
C : Type u_2
inst✝¹⁹ : Category.{v_1, u_2} C
inst✝¹⁸ : MonoidalCategory C
X Y Z : GradedObject I C
inst✝¹⁷ : BraidedCategory C
inst✝¹⁶ : X.HasTensor Y
inst✝¹⁵ : Y.HasTensor Z
inst✝¹⁴ : Z.HasTensor X
inst✝¹³ : Z.HasTensor Y
inst✝¹² : X.HasTensor Z
inst✝¹¹ : (tensorObj X Y).HasTensor Z
inst✝¹⁰ : X.HasTensor (tensorObj Y Z)
inst✝⁹ : Z.HasTensor (tensorObj X Y)
inst✝⁸ : (tensorObj Z X).HasTensor Y
inst✝⁷ : X.HasTensor (tensorObj Z Y)
inst✝⁶ : (tensorObj X Z).HasTensor Y
inst✝⁵ : X.HasGoodTensor₁₂Tensor Y Z
inst✝⁴ : X.HasGoodTensorTensor₂₃ Y Z
inst✝³ : Z.HasGoodTensor₁₂Tensor X Y
inst✝² : Z.HasGoodTensorTensor₂₃ X Y
inst✝¹ : X.HasGoodTensor₁₂Tensor Z Y
inst✝ : X.HasGoodTensorTensor₂₃ Z Y
k i₁ i₂ i₃ : I
h : i₁ + i₂ + i₃ = k
⊢ ιTensorObj₃ X Y Z i₁ i₂ i₃ k h ≫
      ((associator X Y Z).inv ≫ (braiding (tensorObj X Y) Z).hom ≫ (associator Z X Y).inv) k =
    ιTensorObj₃ X Y Z i₁ i₂ i₃ k h ≫
      (whiskerLeft X (braiding Y Z).hom ≫ (associator X Z Y).inv ≫ whiskerRight (braiding X Z).hom Y) k
Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid

Goal state before:
pp: C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
c✝ d : C
⊢ Groupoid.inv (𝟙 c✝) ∈ {p | Discrete.Arrows c✝ c✝ p}

Tactic:
simp only [inv_eq_inv, IsIso.inv_id]

Goal state after:
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
c✝ d : C
⊢ 𝟙 c✝ ∈ {p | Discrete.Arrows c✝ c✝ p}
Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid

Goal state before:
pp: C : Type u
inst✝¹ : Groupoid C
S✝ : Subgroupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
S : Subgroupoid D
c✝ d✝ : C
p✝ : c✝ ⟶ d✝
hp : p✝ ∈ {f | φ.map f ∈ S.arrows (φ.obj c✝) (φ.obj d✝)}
⊢ Groupoid.inv p✝ ∈ {f | φ.map f ∈ S.arrows (φ.obj d✝) (φ.obj c✝)}

Tactic:
rw [mem_ofPred, inv_eq_inv, φ.map_inv, ← inv_eq_inv]; exact S.inv hp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.ConcreteCategory.WithAlgebraicStructures

Goal state before:
pp: R : Type u_1
inst✝⁴ : Ring R
J : Type w
inst✝³ : Category.{r, w} J
F : J ⥤ ModuleCat R
inst✝² : PreservesColimit F (forget (ModuleCat R))
inst✝¹ : IsFiltered J
inst✝ : HasColimit F
r : R
H : ∃ j', ∀ (j : J) (x : j' ⟶ j) (c : ↑(F.obj j)), r • c = 0 → c = 0
x : ToType (colimit F)
hx : r • x = 0
⊢ x = 0

Tactic:
obtain ⟨j, x, rfl⟩ := Concrete.colimit_exists_rep F x

Goal state after:
R : Type u_1
inst✝⁴ : Ring R
J : Type w
inst✝³ : Category.{r, w} J
F : J ⥤ ModuleCat R
inst✝² : PreservesColimit F (forget (ModuleCat R))
inst✝¹ : IsFiltered J
inst✝ : HasColimit F
r : R
H : ∃ j', ∀ (j : J) (x : j' ⟶ j) (c : ↑(F.obj j)), r • c = 0 → c = 0
j : J
x : ToType (F.obj j)
hx : r • (ConcreteCategory.hom (colimit.ι F j)) x = 0
⊢ (ConcreteCategory.hom (colimit.ι F j)) x = 0
Module: Mathlib.CategoryTheory.Join.Basic

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
E' : Type u₄
inst✝ : Category.{v₄, u₄} E'
H : C ⥤ E
Fᵣ Gᵣ : D ⥤ E'
α : Fᵣ ≅ Gᵣ
⊢ (mapIsoWhiskerLeft H α).inv = mapWhiskerLeft H α.inv

Tactic:
ext x
  cases x <;> simp [mapIsoWhiskerLeft]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F G : C ⥤ Type w
a : C
x : F.obj a
y : G.obj a
⊢ (hom (Limits.prod.fst.app a)) (prodMk x y) = x

Tactic:
by
  simp [prodMk]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F G : C ⥤ Type w
a : C
x : F.obj a
y : G.obj a
⊢ (hom (Limits.prod.snd.app a)) (prodMk x y) = y

Tactic:
by
  simp [prodMk]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Free.Basic

Goal state before:
pp: C : Type u
X₁ X₂ X₃ Y₁ Y₂ Y₃ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ ∀ (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (f₃ : X₃ ⟶ Y₃),
    Quotient.map₂ Hom.tensor ⋯ (Quotient.map₂ Hom.tensor ⋯ f₁ f₂) f₃ ≫
        { hom := ⟦Hom.α_hom Y₁ Y₂ Y₃⟧, inv := ⟦Hom.α_inv Y₁ Y₂ Y₃⟧, hom_inv_id := ⋯, inv_hom_id := ⋯ }.hom =
      { hom := ⟦Hom.α_hom X₁ X₂ X₃⟧, inv := ⟦Hom.α_inv X₁ X₂ X₃⟧, hom_inv_id := ⋯, inv_hom_id := ⋯ }.hom ≫
        Quotient.map₂ Hom.tensor ⋯ f₁ (Quotient.map₂ Hom.tensor ⋯ f₂ f₃)

Tactic:
rintro ⟨f₁⟩ ⟨f₂⟩ ⟨f₃⟩

Goal state after:
case mk.mk.mk
C : Type u
X₁ X₂ X₃ Y₁ Y₂ Y₃ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
f₁✝ : X₁ ⟶ Y₁
f₁ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
f₂✝ : X₂ ⟶ Y₂
f₂ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
f₃✝ : X₃ ⟶ Y₃
f₃ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ Quotient.map₂ Hom.tensor ⋯
        (Quotient.map₂ Hom.tensor ⋯ (Quot.mk (⇑(X₁.setoidHom Y₁)) f₁) (Quot.mk (⇑(X₂.setoidHom Y₂)) f₂))
        (Quot.mk (⇑(X₃.setoidHom Y₃)) f₃) ≫
      { hom := ⟦Hom.α_hom Y₁ Y₂ Y₃⟧, inv := ⟦Hom.α_inv Y₁ Y₂ Y₃⟧, hom_inv_id := ⋯, inv_hom_id := ⋯ }.hom =
    { hom := ⟦Hom.α_hom X₁ X₂ X₃⟧, inv := ⟦Hom.α_inv X₁ X₂ X₃⟧, hom_inv_id := ⋯, inv_hom_id := ⋯ }.hom ≫
      Quotient.map₂ Hom.tensor ⋯ (Quot.mk (⇑(X₁.setoidHom Y₁)) f₁)
        (Quotient.map₂ Hom.tensor ⋯ (Quot.mk (⇑(X₂.setoidHom Y₂)) f₂) (Quot.mk (⇑(X₃.setoidHom Y₃)) f₃))
Module: Mathlib.CategoryTheory.Monoidal.Free.Basic

Goal state before:
pp: case h.comp
C : Type u
motive : {X Y : F C} → (X ⟶ Y) → Prop
X Y : F C
id : ∀ (X : F C), motive (𝟙 X)
α_hom : ∀ (X Y Z : F C), motive (α_ X Y Z).hom
α_inv : ∀ (X Y Z : F C), motive (α_ X Y Z).inv
l_hom : ∀ (X : F C), motive (λ_ X).hom
l_inv : ∀ (X : F C), motive (λ_ X).inv
ρ_hom : ∀ (X : F C), motive (ρ_ X).hom
ρ_inv : ∀ (X : F C), motive (ρ_ X).inv
comp : ∀ {X Y Z : F C} (f : X ⟶ Y) (g : Y ⟶ Z), motive f → motive g → motive (f ≫ g)
whiskerLeft : ∀ (X : F C) {Y Z : F C} (f : Y ⟶ Z), motive f → motive (X ◁ f)
whiskerRight : ∀ {X Y : F C} (f : X ⟶ Y) (Z : F C), motive f → motive (f ▷ Z)
X✝ Y✝ Z✝ : F C
f : X✝ ⟶ᵐ Y✝
g : Y✝ ⟶ᵐ Z✝
hf : motive ⟦f⟧
hg : motive ⟦g⟧
⊢ motive ⟦f.comp g⟧

Tactic:
exact comp _ _ hf hg

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

Goal state before:
pp: case refine_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : CartesianMonoidalCategory C
R : C
inst✝¹ : MonObj R
inst✝ : AddMonObj R
h : R ◁ σ ≫ μ = lift (R ◁ fst R R ≫ μ) (R ◁ snd R R ≫ μ) ≫ σ
x✝ : C
a b c : x✝ ⟶ R
this : lift a (lift b c ≫ σ) ≫ μ = lift a (lift b c) ≫ lift (R ◁ fst R R ≫ μ) (R ◁ snd R R ≫ μ) ≫ σ
⊢ a * (b + c) = a * b + a * c

Tactic:
simp only [Hom.add_def, Hom.mul_def, this, ← Category.assoc]

Goal state after:
case refine_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : CartesianMonoidalCategory C
R : C
inst✝¹ : MonObj R
inst✝ : AddMonObj R
h : R ◁ σ ≫ μ = lift (R ◁ fst R R ≫ μ) (R ◁ snd R R ≫ μ) ≫ σ
x✝ : C
a b c : x✝ ⟶ R
this : lift a (lift b c ≫ σ) ≫ μ = lift a (lift b c) ≫ lift (R ◁ fst R R ≫ μ) (R ◁ snd R R ≫ μ) ≫ σ
⊢ (lift a (lift b c) ≫ lift (R ◁ fst R R ≫ μ) (R ◁ snd R R ≫ μ)) ≫ σ = lift (lift a b ≫ μ) (lift a c ≫ μ) ≫ σ
Module: Mathlib.CategoryTheory.Monoidal.Ring

Goal state before:
pp: case refine_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : CartesianMonoidalCategory C
R : C
inst✝¹ : MonObj R
inst✝ : AddMonObj R
h : σ ▷ R ≫ μ = lift (fst R R ▷ R ≫ μ) (snd R R ▷ R ≫ μ) ≫ σ
x✝ : C
a b c : x✝ ⟶ R
this : lift (lift a b ≫ σ) c ≫ μ = lift (lift a b) c ≫ lift (fst R R ▷ R ≫ μ) (snd R R ▷ R ≫ μ) ≫ σ
⊢ (a + b) * c = a * c + b * c

Tactic:
simp only [Hom.add_def, Hom.mul_def, this, ← Category.assoc]

Goal state after:
case refine_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : CartesianMonoidalCategory C
R : C
inst✝¹ : MonObj R
inst✝ : AddMonObj R
h : σ ▷ R ≫ μ = lift (fst R R ▷ R ≫ μ) (snd R R ▷ R ≫ μ) ≫ σ
x✝ : C
a b c : x✝ ⟶ R
this : lift (lift a b ≫ σ) c ≫ μ = lift (lift a b) c ≫ lift (fst R R ▷ R ≫ μ) (snd R R ▷ R ≫ μ) ≫ σ
⊢ (lift (lift a b) c ≫ lift (fst R R ▷ R ≫ μ) (snd R R ▷ R ≫ μ)) ≫ σ = lift (lift a c ≫ μ) (lift b c ≫ μ) ≫ σ
Module: Mathlib.CategoryTheory.Monoidal.Closed.FunctorCategory.Basic

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalClosed C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
inst✝ : ∀ (F₁ F₂ : J ⥤ C), HasFunctorEnrichedHom C F₁ F₂
F₁ F₂ F₂' F₃ F₃' : J ⥤ C
f : F₁ ⊗ F₂ ⟶ F₃
j : J
k₁ k₂ : Under j
φ : k₁ ⟶ k₂
⊢ curry
      (F₁.obj k₁.right ◁ F₂.map k₁.hom ≫
        F₁.map (Under.Hom.right φ) ▷ F₂.obj k₁.right ≫ F₁.obj k₂.right ◁ F₂.map (Under.Hom.right φ) ≫ f.app k₂.right) =
    curry
      (F₁.map (Under.Hom.right φ) ▷ F₂.obj j ≫
        F₁.obj k₂.right ◁ (F₂.map k₁.hom ≫ F₂.map (Under.Hom.right φ)) ≫ f.app k₂.right)

Tactic:
MonoidalCategory.whiskerLeft_comp_assoc,

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalClosed C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
inst✝ : ∀ (F₁ F₂ : J ⥤ C), HasFunctorEnrichedHom C F₁ F₂
F₁ F₂ F₂' F₃ F₃' : J ⥤ C
f : F₁ ⊗ F₂ ⟶ F₃
j : J
k₁ k₂ : Under j
φ : k₁ ⟶ k₂
⊢ curry
      (F₁.obj k₁.right ◁ F₂.map k₁.hom ≫
        F₁.map (Under.Hom.right φ) ▷ F₂.obj k₁.right ≫ F₁.obj k₂.right ◁ F₂.map (Under.Hom.right φ) ≫ f.app k₂.right) =
    curry
      (F₁.map (Under.Hom.right φ) ▷ F₂.obj j ≫
        F₁.obj k₂.right ◁ F₂.map k₁.hom ≫ F₁.obj k₂.right ◁ F₂.map (Under.Hom.right φ) ≫ f.app k₂.right)
Module: Mathlib.CategoryTheory.Monoidal.Closed.Functor

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v, u'} D
inst✝⁴ : CartesianMonoidalCategory C
inst✝³ : CartesianMonoidalCategory D
F : C ⥤ D
L : D ⥤ C
inst✝² : MonoidalClosed C
inst✝¹ : MonoidalClosed D
inst✝ : Limits.PreservesLimitsOfShape (Discrete Limits.WalkingPair) F
h : L ⊣ F
A : C
conjeq :
  ((mateEquiv (ihom.adjunction A) (ihom.adjunction (F.obj A)))
        ((mateEquiv h h)
          (prodComparisonNatTrans L (F.obj A) ≫ L.whiskerLeft ((curriedTensor C).map (h.counit.app A))))).natTrans =
    (conjugateEquiv (h.comp (ihom.adjunction A)) ((ihom.adjunction (F.obj A)).comp h))
      (prodComparisonNatTrans L (F.obj A) ≫ L.whiskerLeft ((curriedTensor C).map (h.counit.app A)))
B : C
⊢ h.unit.app (F.obj A ⊗ F.obj B) ≫
      F.map (prodComparison L (F.obj A) (F.obj B)) ≫
        F.map (h.counit.app A ▷ L.obj (F.obj B)) ≫ F.map (A ◁ h.counit.app B) =
    inv (prodComparison F A B)

Tactic:
rw [← F.map_comp, ← F.map_comp]

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v, u'} D
inst✝⁴ : CartesianMonoidalCategory C
inst✝³ : CartesianMonoidalCategory D
F : C ⥤ D
L : D ⥤ C
inst✝² : MonoidalClosed C
inst✝¹ : MonoidalClosed D
inst✝ : Limits.PreservesLimitsOfShape (Discrete Limits.WalkingPair) F
h : L ⊣ F
A : C
conjeq :
  ((mateEquiv (ihom.adjunction A) (ihom.adjunction (F.obj A)))
        ((mateEquiv h h)
          (prodComparisonNatTrans L (F.obj A) ≫ L.whiskerLeft ((curriedTensor C).map (h.counit.app A))))).natTrans =
    (conjugateEquiv (h.comp (ihom.adjunction A)) ((ihom.adjunction (F.obj A)).comp h))
      (prodComparisonNatTrans L (F.obj A) ≫ L.whiskerLeft ((curriedTensor C).map (h.counit.app A)))
B : C
⊢ h.unit.app (F.obj A ⊗ F.obj B) ≫
      F.map (prodComparison L (F.obj A) (F.obj B) ≫ h.counit.app A ▷ L.obj (F.obj B) ≫ A ◁ h.counit.app B) =
    inv (prodComparison F A B)
Module: Mathlib.CategoryTheory.Monoidal.Closed.FunctorCategory.Basic

Goal state before:
pp: case e_a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalClosed C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
inst✝ : ∀ (F₁ F₂ : J ⥤ C), HasFunctorEnrichedHom C F₁ F₂
F₁ F₂ F₂' F₃ F₃' : J ⥤ C
g : F₂ ⟶ functorEnrichedHom C F₁ F₃
j j' : J
φ : j ⟶ j'
⊢ enrichedHomπ C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃) ((Under.map φ).obj (Under.mk (𝟙 j'))) ≫
      (pre (F₁.map φ)).app (F₃.obj j') =
    enrichedHomπ C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃) (Under.mk (𝟙 j)) ≫ (ihom (F₁.obj j)).map (F₃.map φ)

Tactic:
← enrichedOrdinaryCategorySelf_eHomWhiskerRight,

Goal state after:
case e_a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalClosed C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
inst✝ : ∀ (F₁ F₂ : J ⥤ C), HasFunctorEnrichedHom C F₁ F₂
F₁ F₂ F₂' F₃ F₃' : J ⥤ C
g : F₂ ⟶ functorEnrichedHom C F₁ F₃
j j' : J
φ : j ⟶ j'
⊢ enrichedHomπ C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃) ((Under.map φ).obj (Under.mk (𝟙 j'))) ≫
      eHomWhiskerRight C (F₁.map φ) (F₃.obj j') =
    enrichedHomπ C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃) (Under.mk (𝟙 j)) ≫ (ihom (F₁.obj j)).map (F₃.map φ)
Module: Mathlib.CategoryTheory.Monoidal.Bimod

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

pp: case a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
A B : Mon C
M✝ : Bimod A B
inst✝² : HasCoequalizers C
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
X Y Z : Mon C
M : Bimod X Y
N₁ N₂ : Bimod Y Z
f : N₁ ⟶ N₂
| TensorBimod.actRight M N₂

Tactic:
rw [← comp_whiskerRight, ι_colimMap, parallelPairHom_app_one, comp_whiskerRight]

Goal state after:
case a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
A B : Mon C
M✝ : Bimod A B
inst✝² : HasCoequalizers C
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
X Y Z : Mon C
M : Bimod X Y
N₁ N₂ : Bimod Y Z
f : N₁ ⟶ N₂
| (M.X ◁ f.hom) ▷ Z.X ≫
    colimit.ι (parallelPair (M.actRight ▷ N₂.X) ((α_ M.X Y.X N₂.X).hom ≫ M.X ◁ N₂.actLeft)) WalkingParallelPair.one ▷
      Z.X

case a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
A B : Mon C
M✝ : Bimod A B
inst✝² : HasCoequalizers C
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
X Y Z : Mon C
M : Bimod X Y
N₁ N₂ : Bimod Y Z
f : N₁ ⟶ N₂
| TensorBimod.actRight M N₂
Module: Mathlib.CategoryTheory.Monoidal.Free.Coherence

Goal state before:
pp: C : Type u
X : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ ∀ {X_1 Y : (Discrete ∘ NormalMonoidalObject) C} (f : X_1 ⟶ Y),
    ((tensorFunc C).obj X).map f ≫ (normalizeIsoApp C X Y).hom =
      (normalizeIsoApp C X X_1).hom ≫ ((normalize' C).obj X).map f

Tactic:
rintro ⟨X⟩ ⟨Y⟩ ⟨⟨f⟩⟩
      dsimp at f
      subst f
      dsimp
      simp

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

Goal state before:
pp: case a
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
| Δ ≫ 𝒮 ▷ B ≫ μ

pp: case a
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

Tactic:
rw [antipode_left]

Goal state after:
case a
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
| ε ≫ η

case a
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
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 B : C
inst✝² : HopfObj A
inst✝¹ : HopfObj B
f : A ⟶ B
inst✝ : IsBimonHom f
⊢ f ≫ 𝒮 * f = 1

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:
· rw [Conv.mul_eq, Conv.one_eq]
    simp only [comp_whiskerRight, Category.assoc]
    slice_lhs 3 4 =>
      rw [← whisker_exchange]
    slice_lhs 2 3 =>
      rw [← tensorHom_def]
    slice_lhs 1 2 =>
      rw [← IsComonHom.hom_comul f]
    slice_lhs 2 4 =>
      rw [antipode_left]
    slice_lhs 1 2 =>
      rw [IsComonHom.hom_counit]

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 * 𝒮 ≫ f = 1
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 ≫ μ
| η ≫ Δ ≫ 𝒮 ▷ A ≫ μ

Tactic:
rw [antipode_left]

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: case a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| Δ ≫ 𝒮 ▷ A ≫ μ

pp: case a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| Δ

Tactic:
rw [antipode_left]

Goal state after:
case a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| ε ≫ η

case a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| Δ
Module: Mathlib.CategoryTheory.Monoidal.Bimod

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
R S : Mon C
P : Bimod R S
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
⊢ ((regular R).tensorBimod P).actLeft ≫ hom P = R.X ◁ hom P ≫ P.actLeft

Tactic:
by
  dsimp; dsimp [hom, TensorBimod.actLeft, regular]
  refine (cancel_epi ((tensorLeft _).map (coequalizer.π _ _))).1 ?_
  dsimp
  slice_lhs 1 4 => rw [id_tensor_π_preserves_coequalizer_inv_colimMap_desc]
  slice_lhs 2 3 => rw [left_assoc]
  slice_rhs 1 2 => rw [← whiskerLeft_comp, coequalizer.π_desc]
  rw [Iso.inv_hom_id_assoc]

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

Goal state before:
pp: C : Type u₁
inst✝¹³ : Category.{v₁, u₁} C
V : Type u₂
inst✝¹² : Category.{v₂, u₂} V
inst✝¹¹ : MonoidalCategory C
inst✝¹⁰ : MonoidalCategory V
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 ≫
        (unit F' G').app (x✝.1.1, x✝.1.2) ▷ H'.obj 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:
associator_hom_unit_unit,

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.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.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✝ : MonObj A
X✝ Y✝ : C
f : X✝ ⟶ Y✝
⊢ η.app X✝ ≫ A.map f = η.app Y✝

Tactic:
rw [← η[A].naturality, tensorUnit_map]

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✝ : MonObj A
X✝ Y✝ : C
f : X✝ ⟶ Y✝
⊢ 𝟙 (𝟙_ D) ≫ η.app Y✝ = η.app Y✝
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 κ
X : C
⊢ (isCardinalPresentable C κ).ι.isDenseAt X

Tactic:
by
    obtain ⟨J, _, _, ⟨p⟩⟩ :=
      (isCardinalFilteredGenerator_isCardinalPresentable C κ).exists_colimitsOfShape X
    exact ⟨(Functor.Final.isColimitWhiskerEquiv (F := p.toCostructuredArrow) _).1
      (IsColimit.ofIsoColimit p.isColimit (Cocone.ext (Iso.refl _)))⟩

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

Goal state before:
pp: case refine_3
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
X Y : C
f : X ⟶ Y
hf : P f
⊢ ∀ (j : PUnit.{w + 1}),
    P ({ app := fun x ↦ f, naturality := ⋯ }.app j) ∧
      { app := fun x ↦ f, naturality := ⋯ }.app j ≫ (𝟙 ((Functor.const PUnit.{w + 1}).obj Y)).app j = f

Tactic:
· simpa

Goal state after: