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 X
inst✝¹⁴ : Y.HasTensor Z
inst✝¹³ : Z.HasTensor X
inst✝¹² : X.HasTensor Z
inst✝¹¹ : (tensorObj X Y).HasTensor Z
inst✝¹⁰ : X.HasTensor (tensorObj Y Z)
inst✝⁹ : (tensorObj Y Z).HasTensor X
inst✝⁸ : Y.HasTensor (tensorObj Z X)
inst✝⁷ : (tensorObj Y X).HasTensor Z
inst✝⁶ : Y.HasTensor (tensorObj X Z)
inst✝⁵ : X.HasGoodTensor₁₂Tensor Y Z
inst✝⁴ : X.HasGoodTensorTensor₂₃ Y Z
inst✝³ : Y.HasGoodTensor₁₂Tensor Z X
inst✝² : Y.HasGoodTensorTensor₂₃ Z X
inst✝¹ : Y.HasGoodTensor₁₂Tensor X Z
inst✝ : Y.HasGoodTensorTensor₂₃ X Z
k i₁ i₂ i₃ : I
h : i₁ + i₂ + i₃ = k
| MonoidalCategoryStruct.tensorHom
      (ιTensorObj X Y i₁ i₂ (i₁ + i₂) ⋯ ≫
        tensorObjDesc fun i j hij ↦ (β_ (X i) (Y j)).hom ≫ ιTensorObj Y X j i (i₁ + i₂) ⋯)
      (𝟙 (Z i₃) ≫ 𝟙 Z i₃) ≫
    ιTensorObj (tensorObj Y X) Z (i₁ + i₂) i₃ k ⋯ ≫
      (associator Y X Z).hom k ≫
        whiskerLeft Y (fun k ↦ tensorObjDesc fun i j hij ↦ (β_ (X i) (Z j)).hom ≫ ιTensorObj Z X j i k ⋯) k

Tactic:
id_comp,

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 X
inst✝¹⁴ : Y.HasTensor Z
inst✝¹³ : Z.HasTensor X
inst✝¹² : X.HasTensor Z
inst✝¹¹ : (tensorObj X Y).HasTensor Z
inst✝¹⁰ : X.HasTensor (tensorObj Y Z)
inst✝⁹ : (tensorObj Y Z).HasTensor X
inst✝⁸ : Y.HasTensor (tensorObj Z X)
inst✝⁷ : (tensorObj Y X).HasTensor Z
inst✝⁶ : Y.HasTensor (tensorObj X Z)
inst✝⁵ : X.HasGoodTensor₁₂Tensor Y Z
inst✝⁴ : X.HasGoodTensorTensor₂₃ Y Z
inst✝³ : Y.HasGoodTensor₁₂Tensor Z X
inst✝² : Y.HasGoodTensorTensor₂₃ Z X
inst✝¹ : Y.HasGoodTensor₁₂Tensor X Z
inst✝ : Y.HasGoodTensorTensor₂₃ X Z
k i₁ i₂ i₃ : I
h : i₁ + i₂ + i₃ = k
| MonoidalCategoryStruct.tensorHom
      (ιTensorObj X Y i₁ i₂ (i₁ + i₂) ⋯ ≫
        tensorObjDesc fun i j hij ↦ (β_ (X i) (Y j)).hom ≫ ιTensorObj Y X j i (i₁ + i₂) ⋯)
      (𝟙 Z i₃) ≫
    ιTensorObj (tensorObj Y X) Z (i₁ + i₂) i₃ k ⋯ ≫
      (associator Y X Z).hom k ≫
        whiskerLeft Y (fun k ↦ tensorObjDesc fun i j hij ↦ (β_ (X i) (Z j)).hom ≫ ιTensorObj Z X j i k ⋯) k
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 X
inst✝¹⁴ : Y.HasTensor Z
inst✝¹³ : Z.HasTensor X
inst✝¹² : X.HasTensor Z
inst✝¹¹ : (tensorObj X Y).HasTensor Z
inst✝¹⁰ : X.HasTensor (tensorObj Y Z)
inst✝⁹ : (tensorObj Y Z).HasTensor X
inst✝⁸ : Y.HasTensor (tensorObj Z X)
inst✝⁷ : (tensorObj Y X).HasTensor Z
inst✝⁶ : Y.HasTensor (tensorObj X Z)
inst✝⁵ : X.HasGoodTensor₁₂Tensor Y Z
inst✝⁴ : X.HasGoodTensorTensor₂₃ Y Z
inst✝³ : Y.HasGoodTensor₁₂Tensor Z X
inst✝² : Y.HasGoodTensorTensor₂₃ Z X
inst✝¹ : Y.HasGoodTensor₁₂Tensor X Z
inst✝ : Y.HasGoodTensorTensor₂₃ X Z
k i₁ i₂ i₃ : I
h : i₁ + i₂ + i₃ = k
| MonoidalCategoryStruct.tensorHom (β_ (X i₁) (Y i₂)).hom (𝟙 (Z i₃)) ≫
    (MonoidalCategoryStruct.associator (Y i₂) (X i₁) (Z i₃)).hom ≫
      MonoidalCategoryStruct.tensorHom (𝟙 (Y i₂)) ((β_ (X i₁) (Z i₃)).hom ≫ ιTensorObj Z X i₃ i₁ (i₁ + i₃) ⋯) ≫
        ιTensorObj Y (tensorObj Z X) i₂ (i₁ + i₃) k ⋯

Tactic:
MonoidalCategory.id_tensor_comp,

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 X
inst✝¹⁴ : Y.HasTensor Z
inst✝¹³ : Z.HasTensor X
inst✝¹² : X.HasTensor Z
inst✝¹¹ : (tensorObj X Y).HasTensor Z
inst✝¹⁰ : X.HasTensor (tensorObj Y Z)
inst✝⁹ : (tensorObj Y Z).HasTensor X
inst✝⁸ : Y.HasTensor (tensorObj Z X)
inst✝⁷ : (tensorObj Y X).HasTensor Z
inst✝⁶ : Y.HasTensor (tensorObj X Z)
inst✝⁵ : X.HasGoodTensor₁₂Tensor Y Z
inst✝⁴ : X.HasGoodTensorTensor₂₃ Y Z
inst✝³ : Y.HasGoodTensor₁₂Tensor Z X
inst✝² : Y.HasGoodTensorTensor₂₃ Z X
inst✝¹ : Y.HasGoodTensor₁₂Tensor X Z
inst✝ : Y.HasGoodTensorTensor₂₃ X Z
k i₁ i₂ i₃ : I
h : i₁ + i₂ + i₃ = k
| MonoidalCategoryStruct.tensorHom (β_ (X i₁) (Y i₂)).hom (𝟙 (Z i₃)) ≫
    (MonoidalCategoryStruct.associator (Y i₂) (X i₁) (Z i₃)).hom ≫
      (MonoidalCategoryStruct.tensorHom (𝟙 (Y i₂)) (β_ (X i₁) (Z i₃)).hom ≫
          MonoidalCategoryStruct.tensorHom (𝟙 (Y i₂)) (ιTensorObj Z X i₃ i₁ (i₁ + i₃) ⋯)) ≫
        ιTensorObj Y (tensorObj Z X) i₂ (i₁ + i₃) k ⋯
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
k i₁ i₂ i₃ : I
h : i₁ + i₂ + i₃ = k
| MonoidalCategoryStruct.tensorHom (𝟙 (X i₁) ≫ 𝟙 X i₁)
      (ιTensorObj Y Z i₂ i₃ (i₂ + i₃) ⋯ ≫
        tensorObjDesc fun i j hij ↦ (β_ (Y i) (Z j)).hom ≫ ιTensorObj Z Y j i (i₂ + i₃) ⋯) ≫
    ιTensorObj X (tensorObj Z Y) i₁ (i₂ + i₃) k ⋯ ≫
      (associator X Z Y).inv k ≫
        whiskerRight (fun k ↦ tensorObjDesc fun i j hij ↦ (β_ (X i) (Z j)).hom ≫ ιTensorObj Z X j i k ⋯) Y k

Tactic:
id_comp,

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
| MonoidalCategoryStruct.tensorHom (𝟙 X i₁)
      (ιTensorObj Y Z i₂ i₃ (i₂ + i₃) ⋯ ≫
        tensorObjDesc fun i j hij ↦ (β_ (Y i) (Z j)).hom ≫ ιTensorObj Z Y j i (i₂ + i₃) ⋯) ≫
    ιTensorObj X (tensorObj Z Y) i₁ (i₂ + i₃) k ⋯ ≫
      (associator X Z Y).inv k ≫
        whiskerRight (fun k ↦ tensorObjDesc fun i j hij ↦ (β_ (X i) (Z j)).hom ≫ ιTensorObj Z X j i k ⋯) Y k
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
k i₁ i₂ i₃ : I
h : i₁ + i₂ + i₃ = k
| MonoidalCategoryStruct.tensorHom (𝟙 (X i₁)) ((β_ (Y i₂) (Z i₃)).hom ≫ ιTensorObj Z Y i₃ i₂ (i₂ + i₃) ⋯) ≫
    ιTensorObj X (tensorObj Z Y) i₁ (i₂ + i₃) k ⋯ ≫
      (associator X Z Y).inv k ≫
        whiskerRight (fun k ↦ tensorObjDesc fun i j hij ↦ (β_ (X i) (Z j)).hom ≫ ιTensorObj Z X j i k ⋯) Y k

Tactic:
MonoidalCategory.id_tensor_comp,

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
| (MonoidalCategoryStruct.tensorHom (𝟙 (X i₁)) (β_ (Y i₂) (Z i₃)).hom ≫
      MonoidalCategoryStruct.tensorHom (𝟙 (X i₁)) (ιTensorObj Z Y i₃ i₂ (i₂ + i₃) ⋯)) ≫
    ιTensorObj X (tensorObj Z Y) i₁ (i₂ + i₃) k ⋯ ≫
      (associator X Z Y).inv k ≫
        whiskerRight (fun k ↦ tensorObjDesc fun i j hij ↦ (β_ (X i) (Z j)).hom ≫ ιTensorObj Z X j i k ⋯) Y k
Module: Mathlib.CategoryTheory.Join.Sum

Goal state before:
pp: case inl.inl
C : Type u_1
D : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
x✝ y✝ : C
f✝¹ f✝ : x✝ ⟶ y✝
heq : (fromSum C D).map ((Sum.inl_ C D).map f✝¹) = (fromSum C D).map ((Sum.inl_ C D).map f✝)
⊢ (Sum.inl_ C D).map f✝¹ = (Sum.inl_ C D).map f✝

Tactic:
simp only [fromSum_map_inl, fromSum_map_inr] at heq
      simp [Functor.map_injective _ heq]

Goal state after:
Module: Mathlib.CategoryTheory.Join.Sum

Goal state before:
pp: case inr.inr
C : Type u_1
D : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
x✝ y✝ : D
f✝¹ f✝ : x✝ ⟶ y✝
heq : (fromSum C D).map ((Sum.inr_ C D).map f✝¹) = (fromSum C D).map ((Sum.inr_ C D).map f✝)
⊢ (Sum.inr_ C D).map f✝¹ = (Sum.inr_ C D).map f✝

Tactic:
simp only [fromSum_map_inl, fromSum_map_inr] at heq
      simp [Functor.map_injective _ heq]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Images

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
F G : C ⥤ Type u
f : F ⟶ G
H : MonoFactorisation f
⊢ {
        app := fun X ↦
          ↾fun x ↦
            match x with
            | ⟨x, hx⟩ => (ConcreteCategory.hom (H.e.app X)) (Exists.choose hx),
        naturality := ⋯ } ≫
      H.m =
    (monoFactorisation f).m

Tactic:
by
    ext
    simp
    grind

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback

Goal state before:
pp: case refine_3
C : Type u
inst✝ : Category.{v, u} C
X₁ X₂ X₃ S : C
f₁ : X₁ ⟶ S
f₂ : X₂ ⟶ S
f₃ : X₃ ⟶ S
h₁₂ : ChosenPullback f₁ f₂
h₂₃ : ChosenPullback f₂ f₃
h₁₃ : ChosenPullback f₁ f₃
h : ChosenPullback₃ h₁₂ h₂₃ h₁₃
Y : C
g₁ : Y ⟶ X₁
g₂ : Y ⟶ X₂
g₃ : Y ⟶ X₃
b : Y ⟶ S
hg₁ : g₁ ≫ f₁ = b
hg₂ : g₂ ≫ f₂ = b
hg₃ : g₃ ≫ f₃ = b
φ₁₂ : Y ⟶ h₁₂.pullback
w₁ : φ₁₂ ≫ h₁₂.p₁ = g₁
w₂ : φ₁₂ ≫ h₁₂.p₂ = g₂
φ₂₃ : Y ⟶ h₂₃.pullback
w₂' : φ₂₃ ≫ h₂₃.p₁ = g₂
w₃ : φ₂₃ ≫ h₂₃.p₂ = g₃
φ : Y ⟶ h.chosenPullback.pullback
w₁₂ : φ ≫ h.chosenPullback.p₁ = φ₁₂
w₂₃ : φ ≫ h.chosenPullback.p₂ = φ₂₃
⊢ φ ≫ h.p₃ = φ ≫ h.p₂₃ ≫ h₂₃.p₂

Tactic:
p₂₃_p₃

Goal state after:
case refine_3
C : Type u
inst✝ : Category.{v, u} C
X₁ X₂ X₃ S : C
f₁ : X₁ ⟶ S
f₂ : X₂ ⟶ S
f₃ : X₃ ⟶ S
h₁₂ : ChosenPullback f₁ f₂
h₂₃ : ChosenPullback f₂ f₃
h₁₃ : ChosenPullback f₁ f₃
h : ChosenPullback₃ h₁₂ h₂₃ h₁₃
Y : C
g₁ : Y ⟶ X₁
g₂ : Y ⟶ X₂
g₃ : Y ⟶ X₃
b : Y ⟶ S
hg₁ : g₁ ≫ f₁ = b
hg₂ : g₂ ≫ f₂ = b
hg₃ : g₃ ≫ f₃ = b
φ₁₂ : Y ⟶ h₁₂.pullback
w₁ : φ₁₂ ≫ h₁₂.p₁ = g₁
w₂ : φ₁₂ ≫ h₁₂.p₂ = g₂
φ₂₃ : Y ⟶ h₂₃.pullback
w₂' : φ₂₃ ≫ h₂₃.p₁ = g₂
w₃ : φ₂₃ ≫ h₂₃.p₂ = g₃
φ : Y ⟶ h.chosenPullback.pullback
w₁₂ : φ ≫ h.chosenPullback.p₁ = φ₁₂
w₂₃ : φ ≫ h.chosenPullback.p₂ = φ₂₃
⊢ φ ≫ h.p₃ = φ ≫ h.p₃
Module: Mathlib.CategoryTheory.Limits.Shapes.SequentialProduct

Goal state before:
pp: case neg
C : Type u_1
M N : ℕ → C
inst✝¹ : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst✝ : HasCountableProducts C
s : Cone (Functor.ofOpSequence (functorMap f))
n m : ℕ
h : ¬m < n
⊢ (Pi.lift fun m ↦ s.π.app (Opposite.op (m + 1)) ≫ Pi.π (fun i ↦ if x : i < m + 1 then M i else N i) m ≫ eqToHom ⋯) ≫
      (cone f).π.app (Opposite.op n) ≫ Pi.π (fun m ↦ if x : m < n then M m else N m) m =
    s.π.app (Opposite.op n) ≫ Pi.π (fun m ↦ if x : m < n then M m else N m) m

Tactic:
cone_π_app_comp_Pi_π_neg f _ _ h

Goal state after:
case neg
C : Type u_1
M N : ℕ → C
inst✝¹ : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst✝ : HasCountableProducts C
s : Cone (Functor.ofOpSequence (functorMap f))
n m : ℕ
h : ¬m < n
⊢ (Pi.lift fun m ↦ s.π.app (Opposite.op (m + 1)) ≫ Pi.π (fun i ↦ if x : i < m + 1 then M i else N i) m ≫ eqToHom ⋯) ≫
      Pi.π M m ≫ f m ≫ eqToHom ⋯ =
    s.π.app (Opposite.op n) ≫ Pi.π (fun m ↦ if x : m < n then M m else N m) m
Module: Mathlib.CategoryTheory.Limits.WeakLimits.Basic

Goal state before:
pp: J : Type u_1
inst✝³ : Category.{v_1, u_1} J
K : Type u_2
inst✝² : Category.{v_2, u_2} K
C : Type u_3
inst✝¹ : Category.{v_3, u_3} C
F : J ⥤ C
D : Type u_4
inst✝ : Category.{v_4, u_4} D
G : K ⥤ D
t t' : Cone F
l : IsLimit t
l' : IsWeakLimit t'
x✝ : J
⊢ l'.lift t ≫ l.lift t' ≫ t.π.app x✝ = 𝟙 t.pt ≫ t.π.app x✝

Tactic:
id_comp,

Goal state after:
J : Type u_1
inst✝³ : Category.{v_1, u_1} J
K : Type u_2
inst✝² : Category.{v_2, u_2} K
C : Type u_3
inst✝¹ : Category.{v_3, u_3} C
F : J ⥤ C
D : Type u_4
inst✝ : Category.{v_4, u_4} D
G : K ⥤ D
t t' : Cone F
l : IsLimit t
l' : IsWeakLimit t'
x✝ : J
⊢ l'.lift t ≫ l.lift t' ≫ t.π.app x✝ = t.π.app x✝
Module: Mathlib.CategoryTheory.Monoidal.Free.Basic

Goal state before:
pp: case ρ_hom_inv
C : Type u
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : MonoidalCategory D
f✝ : C → D
X Y : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
f g : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
X✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ projectMapAux f✝ ((ρ_hom X✝).comp (ρ_inv X✝)) = projectMapAux f✝ (Hom.id (X✝.tensor unit))

Tactic:
| ρ_hom_inv =>

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

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasPushouts C
inst✝³ : HasInitial C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : MonoidalClosed C
inst✝ : BraidedCategory C
X Y : Arrow C
⊢ IsInitial (((curriedTensor C).obj X.right).obj (𝟙_ (Arrow C)).left)

Tactic:
exact initialIsInitial.ofIso (zeroMul initialIsInitial).symm

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

Goal state before:
pp: C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalLeftAction C D
M : C
inst✝³ : MonObj M
X : D
N : C
inst✝² : MonObj N
e₁ : M ≅ N
inst✝¹ : IsMonHom e₁.hom
Y : D
e₂ : X ≅ Y
inst✝ : ModObj M X
⊢ (μ ≫ e₁.inv) ⊵ₗ Y ≫ M ⊴ₗ e₂.inv = ((e₁.inv ⊗ₘ e₁.inv) ⊙ₗₘ e₂.inv) ≫ μ ⊵ₗ X

Tactic:
IsMonHom.mul_hom,

Goal state after:
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalLeftAction C D
M : C
inst✝³ : MonObj M
X : D
N : C
inst✝² : MonObj N
e₁ : M ≅ N
inst✝¹ : IsMonHom e₁.hom
Y : D
e₂ : X ≅ Y
inst✝ : ModObj M X
⊢ ((e₁.inv ⊗ₘ e₁.inv) ≫ μ) ⊵ₗ Y ≫ M ⊴ₗ e₂.inv = ((e₁.inv ⊗ₘ e₁.inv) ⊙ₗₘ e₂.inv) ≫ μ ⊵ₗ X
Module: Mathlib.CategoryTheory.Monoidal.Mod

Goal state before:
pp: C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalLeftAction C D
M : C
inst✝³ : MonObj M
X : D
N : C
inst✝² : MonObj N
e₁ : M ≅ N
inst✝¹ : IsMonHom e₁.hom
Y : D
e₂ : X ≅ Y
inst✝ : ModObj M X
this✝ : μ ⊵ₗ Y ≫ (e₁.inv ⊙ₗₘ e₂.inv) = ((e₁.inv ⊗ₘ e₁.inv) ⊙ₗₘ e₂.inv) ≫ μ ⊵ₗ X
this : (αₗ N M X).inv ≫ (e₁.inv ▷ M) ⊵ₗ X ≫ (αₗ M M X).hom ≫ M ⊴ₗ γ = N ⊴ₗ γ ≫ e₁.inv ⊵ₗ X
⊢ ((e₁.inv ⊗ₘ e₁.inv) ⊙ₗₘ e₂.inv) ≫ μ ⊵ₗ X ≫ γ ≫ e₂.hom =
    (αₗ N N Y).hom ≫ N ⊴ₗ ((e₁.inv ⊙ₗₘ e₂.inv) ≫ γ ≫ e₂.hom) ≫ (e₁.inv ⊙ₗₘ e₂.inv) ≫ γ ≫ e₂.hom

Tactic:
simp [tensorHom_def', actionHom_def', mul_smul_assoc, reassoc_of% this]

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

Goal state before:
pp: C : Type u₁
inst✝¹² : Category.{v₁, u₁} C
inst✝¹¹ : MonoidalCategory C
D : Type u₂
inst✝¹⁰ : Category.{v₂, u₂} D
inst✝⁹ : MonoidalLeftAction C D
M' N' O' : D
A✝¹ : C
inst✝⁸ : MonObj A✝¹
M✝¹ N O : D
inst✝⁷ : ModObj A✝¹ M✝¹
inst✝⁶ : ModObj A✝¹ N
inst✝⁵ : ModObj A✝¹ O
A✝ : C
inst✝⁴ : MonObj A✝
M✝ : Mod D A✝
A B : C
inst✝³ : MonObj A
inst✝² : MonObj B
f : A ⟶ B
inst✝¹ : IsMonHom f
M : D
inst✝ : ModObj B M
⊢ (μ ≫ f) ⊵ₗ M ≫ γ = (f ▷ A ≫ B ◁ f ≫ μ) ⊵ₗ M ≫ γ

Tactic:
IsMonHom.mul_hom,

Goal state after:
C : Type u₁
inst✝¹² : Category.{v₁, u₁} C
inst✝¹¹ : MonoidalCategory C
D : Type u₂
inst✝¹⁰ : Category.{v₂, u₂} D
inst✝⁹ : MonoidalLeftAction C D
M' N' O' : D
A✝¹ : C
inst✝⁸ : MonObj A✝¹
M✝¹ N O : D
inst✝⁷ : ModObj A✝¹ M✝¹
inst✝⁶ : ModObj A✝¹ N
inst✝⁵ : ModObj A✝¹ O
A✝ : C
inst✝⁴ : MonObj A✝
M✝ : Mod D A✝
A B : C
inst✝³ : MonObj A
inst✝² : MonObj B
f : A ⟶ B
inst✝¹ : IsMonHom f
M : D
inst✝ : ModObj B M
⊢ ((f ⊗ₘ f) ≫ μ) ⊵ₗ M ≫ γ = (f ▷ A ≫ B ◁ f ≫ μ) ⊵ₗ M ≫ γ
Module: Mathlib.CategoryTheory.Monoidal.Closed.Ideal

Goal state before:
pp: case h_snd
C : Type u₁
D : Type u₂
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : Category.{v₁, u₂} D
i : D ⥤ C
inst✝⁵ : CartesianMonoidalCategory C
inst✝⁴ : Reflective i
inst✝³ : MonoidalClosed C
inst✝² : CartesianMonoidalCategory D
inst✝¹ : ExponentialIdeal i
inst✝ : BraidedCategory C
A B : C
⊢ snd A B ≫ (reflectorAdjunction i).unit.app B =
    (reflectorAdjunction i).unit.app (A ⊗ B) ≫
      i.map (prodComparison (reflector i) A B) ≫
        prodComparison i ((reflector i).obj A) ((reflector i).obj B) ≫
          snd (i.obj ((reflector i).obj A)) (i.obj ((reflector i).obj B))

Tactic:
prodComparison_snd,

Goal state after:
case h_snd
C : Type u₁
D : Type u₂
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : Category.{v₁, u₂} D
i : D ⥤ C
inst✝⁵ : CartesianMonoidalCategory C
inst✝⁴ : Reflective i
inst✝³ : MonoidalClosed C
inst✝² : CartesianMonoidalCategory D
inst✝¹ : ExponentialIdeal i
inst✝ : BraidedCategory C
A B : C
⊢ snd A B ≫ (reflectorAdjunction i).unit.app B =
    (reflectorAdjunction i).unit.app (A ⊗ B) ≫
      i.map (prodComparison (reflector i) A B) ≫ i.map (snd ((reflector i).obj A) ((reflector i).obj B))
Module: Mathlib.CategoryTheory.Monoidal.DayConvolution.Braided

Goal state before:
pp: C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
V : Type u₂
inst✝⁶ : Category.{v₂, u₂} V
inst✝⁵ : MonoidalCategory C
inst✝⁴ : BraidedCategory C
inst✝³ : MonoidalCategory V
inst✝² : BraidedCategory V
F G : C ⥤ V
inst✝¹ : DayConvolution F G
inst✝ : DayConvolution G F
⊢ (corepresentableBy F G).homEquiv.symm (braidingHomCorepresenting F G) ≫
      (corepresentableBy G F).homEquiv.symm (braidingInvCorepresenting F G) =
    𝟙 (F ⊛ G)

Tactic:
apply Functor.hom_ext_of_isLeftKanExtension (F ⊛ G) (unit F G)

Goal state after:
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
V : Type u₂
inst✝⁶ : Category.{v₂, u₂} V
inst✝⁵ : MonoidalCategory C
inst✝⁴ : BraidedCategory C
inst✝³ : MonoidalCategory V
inst✝² : BraidedCategory V
F G : C ⥤ V
inst✝¹ : DayConvolution F G
inst✝ : DayConvolution G F
⊢ unit F G ≫
      (tensor C).whiskerLeft
        ((corepresentableBy F G).homEquiv.symm (braidingHomCorepresenting F G) ≫
          (corepresentableBy G F).homEquiv.symm (braidingInvCorepresenting F G)) =
    unit F G ≫ (tensor C).whiskerLeft (𝟙 (F ⊛ G))
Module: Mathlib.CategoryTheory.Monoidal.DayConvolution.Braided

Goal state before:
pp: C : Type u₁
inst✝¹⁸ : Category.{v₁, u₁} C
V : Type u₂
inst✝¹⁷ : Category.{v₂, u₂} V
inst✝¹⁶ : MonoidalCategory C
inst✝¹⁵ : BraidedCategory C
inst✝¹⁴ : MonoidalCategory V
inst✝¹³ : BraidedCategory V
F G : C ⥤ V
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)
H : C ⥤ V
inst✝¹⁰ : DayConvolution F G
inst✝⁹ : DayConvolution G H
inst✝⁸ : DayConvolution F (G ⊛ H)
inst✝⁷ : DayConvolution (F ⊛ G) H
inst✝⁶ : DayConvolution H F
inst✝⁵ : DayConvolution G (H ⊛ F)
inst✝⁴ : DayConvolution (G ⊛ H) F
inst✝³ : DayConvolution G F
inst✝² : DayConvolution (G ⊛ F) H
inst✝¹ : DayConvolution F H
inst✝ : DayConvolution G (F ⊛ H)
⊢ (associator F G H).hom ≫ (braiding F (G ⊛ H)).hom ≫ (associator G H F).hom =
    map (braiding F G).hom (𝟙 H) ≫ (associator G F H).hom ≫ map (𝟙 G) (braiding F H).hom

Tactic:
apply Functor.hom_ext_of_isLeftKanExtension ((F ⊛ G) ⊛ H) (unit _ H)

Goal state after:
C : Type u₁
inst✝¹⁸ : Category.{v₁, u₁} C
V : Type u₂
inst✝¹⁷ : Category.{v₂, u₂} V
inst✝¹⁶ : MonoidalCategory C
inst✝¹⁵ : BraidedCategory C
inst✝¹⁴ : MonoidalCategory V
inst✝¹³ : BraidedCategory V
F G : C ⥤ V
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)
H : C ⥤ V
inst✝¹⁰ : DayConvolution F G
inst✝⁹ : DayConvolution G H
inst✝⁸ : DayConvolution F (G ⊛ H)
inst✝⁷ : DayConvolution (F ⊛ G) H
inst✝⁶ : DayConvolution H F
inst✝⁵ : DayConvolution G (H ⊛ F)
inst✝⁴ : DayConvolution (G ⊛ H) F
inst✝³ : DayConvolution G F
inst✝² : DayConvolution (G ⊛ F) H
inst✝¹ : DayConvolution F H
inst✝ : DayConvolution G (F ⊛ H)
⊢ unit (F ⊛ G) H ≫ (tensor C).whiskerLeft ((associator F G H).hom ≫ (braiding F (G ⊛ H)).hom ≫ (associator G H F).hom) =
    unit (F ⊛ G) H ≫
      (tensor C).whiskerLeft (map (braiding F G).hom (𝟙 H) ≫ (associator G F H).hom ≫ map (𝟙 G) (braiding F H).hom)
Module: Mathlib.CategoryTheory.Monoidal.DayConvolution.Closed

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
inst✝ : MonoidalClosed V
F G H : C ⥤ V
ℌ : DayConvolutionInternalHom F G H
G' H' : C ⥤ V
f : G ⟶ G'
ℌ' : DayConvolutionInternalHom F G' H'
c j : C
⊢ (ℌ.map f ℌ').app c ≫ ℌ'.π c j = ℌ.π c j ≫ (ihom (F.obj j)).map (f.app (j ⊗ c))

Tactic:
dsimp [map]
  rw [← Wedge.mk_ι
      (F := dayConvolutionInternalHomDiagramFunctor F |>.obj _ |>.obj c)
      (H'.obj c) (ℌ'.π c) (ℌ'.hπ c),
    Wedge.IsLimit.lift_ι (ℌ'.isLimitWedge c)]

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

Goal state before:
pp: C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
V : Type u₂
inst✝⁶ : Category.{v₂, u₂} V
inst✝⁵ : MonoidalCategory C
inst✝⁴ : SymmetricCategory C
inst✝³ : MonoidalCategory V
inst✝² : SymmetricCategory V
F G : C ⥤ V
inst✝¹ : DayConvolution F G
inst✝ : DayConvolution G F
⊢ (braiding F G).hom ≫ (braiding G F).hom = 𝟙 (F ⊛ G)

Tactic:
apply Functor.hom_ext_of_isLeftKanExtension (F ⊛ G) (unit F G)

Goal state after:
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
V : Type u₂
inst✝⁶ : Category.{v₂, u₂} V
inst✝⁵ : MonoidalCategory C
inst✝⁴ : SymmetricCategory C
inst✝³ : MonoidalCategory V
inst✝² : SymmetricCategory V
F G : C ⥤ V
inst✝¹ : DayConvolution F G
inst✝ : DayConvolution G F
⊢ unit F G ≫ (tensor C).whiskerLeft ((braiding F G).hom ≫ (braiding G F).hom) =
    unit F G ≫ (tensor C).whiskerLeft (𝟙 (F ⊛ G))
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:
by
  have := (rfl : η[A] ≫ Δ[A] ≫ (𝒮[A] ▷ A) ≫ μ[A] = _)
  conv at this =>
    rhs
    rw [antipode_left]
  rw [Bimon.one_comul_assoc, tensorHom_def_assoc, unitors_inv_equal,
    ← rightUnitor_inv_naturality_assoc, whisker_exchange_assoc, ← rightUnitor_inv_naturality_assoc,
    rightUnitor_inv_naturality_assoc] at this
  simpa

Goal state after: