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

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Finite J
f : J → C
X Y : C
⊢ (rightDistributor f X ⊗ᵢ asIso (𝟙 Y)) ≪≫ rightDistributor (fun j ↦ f j ⊗ X) Y =
    α_ (⨁ f) X Y ≪≫ rightDistributor f (X ⊗ Y) ≪≫ biproduct.mapIso fun x ↦ (α_ (f x) X Y).symm

Tactic:
cases nonempty_fintype J
  ext
  simp only [Category.comp_id, Category.assoc, eqToHom_refl, Iso.symm_hom, Iso.trans_hom,
    asIso_hom, comp_zero, comp_dite, Preadditive.sum_comp, Preadditive.comp_sum, sum_tensor,
    comp_tensor_id, tensorIso_hom, rightDistributor_hom, biproduct.mapIso_hom, biproduct.ι_map,
    biproduct.ι_π, Finset.sum_dite_irrel, Finset.sum_dite_eq', Finset.sum_const_zero,
    Finset.mem_univ, if_true]
  simp_rw [← tensorHom_id]
  simp only [← comp_tensor_id, biproduct.ι_π, dite_tensor, comp_dite]
  simp

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

Goal state before:
pp: C : Type u₁
inst✝⁸ : Category.{v₁, u₁} C
inst✝⁷ : MonoidalCategory C
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : MonoidalCategory D
E : Type u₃
inst✝⁴ : Category.{v₃, u₃} E
inst✝³ : MonoidalCategory E
C' : Type u₁'
inst✝² : Category.{v₁', u₁'} C'
F✝ F : C ⥤ D
G : C ⥤ E
inst✝¹ : F.Monoidal
inst✝ : G.Monoidal
x✝¹ x✝ : C
⊢ δ (F.prod' G) x✝¹ x✝ ≫ μ (F.prod' G) x✝¹ x✝ = 𝟙 ((F.prod' G).obj (x✝¹ ⊗ x✝))

Tactic:
by
    ext
    · simp only [CategoryTheory.prod_comp_fst, prod'_μ_fst, prod'_δ_fst, δ_μ,
        prod'_obj, prod_id]
    · simp only [CategoryTheory.prod_comp_snd, prod'_μ_snd, prod'_δ_snd, δ_μ,
        prod'_obj, prod_id]

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

Goal state before:
pp: case e'_2
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y Z : C
⊢ ((α_ X Y Z).inv ≫ (β_ X Y).hom ▷ Z ⊗≫ Y ◁ (β_ X Z).hom ⊗≫ (β_ Y Z).hom ▷ X) ≫ (α_ Z Y X).hom =
    (α_ X Y Z).inv ≫
      (β_ X Y).hom ▷ Z ≫ (α_ Y X Z).hom ≫ Y ◁ (β_ X Z).hom ≫ (α_ Y Z X).inv ≫ (β_ Y Z).hom ▷ X ≫ (α_ Z Y X).hom

Tactic:
monoidal

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

Goal state before:
pp: case e'_3
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y Z : C
⊢ ((α_ X Y Z).inv ≫ 𝟙 ((X ⊗ Y) ⊗ Z) ⊗≫ (X ◁ (β_ Y Z).hom ⊗≫ (β_ X Z).hom ▷ Y ⊗≫ Z ◁ (β_ X Y).hom) ⊗≫ 𝟙 ((Z ⊗ Y) ⊗ X)) ≫
      (α_ Z Y X).hom =
    X ◁ (β_ Y Z).hom ≫ (α_ X Z Y).inv ≫ (β_ X Z).hom ▷ Y ≫ (α_ Z X Y).hom ≫ Z ◁ (β_ X Y).hom

Tactic:
monoidal

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

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Category.{v_2, u_2} D
inst✝⁴ : MonoidalCategory C
inst✝³ : MonoidalCategory D
F : C ⥤ D
inst✝² : F.Monoidal
inst✝¹ : F.Faithful
inst✝ : BraidedCategory D
β : (X Y : C) → X ⊗ Y ≅ Y ⊗ X
w : ∀ (X Y : C), μ F X Y ≫ F.map (β X Y).hom = (β_ (F.obj X) (F.obj Y)).hom ≫ μ F Y X
X✝ Y✝ Z✝ : C
f✝ : Y✝ ⟶ Z✝
⊢ F.obj X✝ ◁ F.map f✝ ≫ μ F X✝ Z✝ ≫ F.map (β X✝ Z✝).hom = μ F X✝ Y✝ ≫ F.map ((β X✝ Y✝).hom ≫ f✝ ▷ X✝)

Tactic:
w,

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Category.{v_2, u_2} D
inst✝⁴ : MonoidalCategory C
inst✝³ : MonoidalCategory D
F : C ⥤ D
inst✝² : F.Monoidal
inst✝¹ : F.Faithful
inst✝ : BraidedCategory D
β : (X Y : C) → X ⊗ Y ≅ Y ⊗ X
w : ∀ (X Y : C), μ F X Y ≫ F.map (β X Y).hom = (β_ (F.obj X) (F.obj Y)).hom ≫ μ F Y X
X✝ Y✝ Z✝ : C
f✝ : Y✝ ⟶ Z✝
⊢ F.obj X✝ ◁ F.map f✝ ≫ (β_ (F.obj X✝) (F.obj Z✝)).hom ≫ μ F Z✝ X✝ = μ F X✝ Y✝ ≫ F.map ((β X✝ Y✝).hom ≫ f✝ ▷ X✝)
Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Category.{v_2, u_2} D
inst✝⁴ : MonoidalCategory C
inst✝³ : MonoidalCategory D
F : C ⥤ D
inst✝² : F.Monoidal
inst✝¹ : F.Faithful
inst✝ : BraidedCategory D
β : (X Y : C) → X ⊗ Y ≅ Y ⊗ X
w : ∀ (X Y : C), μ F X Y ≫ F.map (β X Y).hom = (β_ (F.obj X) (F.obj Y)).hom ≫ μ F Y X
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
Z✝ : C
⊢ F.map f✝ ▷ F.obj Z✝ ≫ μ F Y✝ Z✝ ≫ F.map (β Y✝ Z✝).hom = μ F X✝ Z✝ ≫ F.map ((β X✝ Z✝).hom ≫ Z✝ ◁ f✝)

Tactic:
w,

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Category.{v_2, u_2} D
inst✝⁴ : MonoidalCategory C
inst✝³ : MonoidalCategory D
F : C ⥤ D
inst✝² : F.Monoidal
inst✝¹ : F.Faithful
inst✝ : BraidedCategory D
β : (X Y : C) → X ⊗ Y ≅ Y ⊗ X
w : ∀ (X Y : C), μ F X Y ≫ F.map (β X Y).hom = (β_ (F.obj X) (F.obj Y)).hom ≫ μ F Y X
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
Z✝ : C
⊢ F.map f✝ ▷ F.obj Z✝ ≫ (β_ (F.obj Y✝) (F.obj Z✝)).hom ≫ μ F Z✝ Y✝ = μ F X✝ Z✝ ≫ F.map ((β X✝ Z✝).hom ≫ Z✝ ◁ f✝)
Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Category.{v_2, u_2} D
inst✝⁴ : MonoidalCategory C
inst✝³ : MonoidalCategory D
F : C ⥤ D
inst✝² : F.Monoidal
inst✝¹ : F.Faithful
inst✝ : BraidedCategory D
β : (X Y : C) → X ⊗ Y ≅ Y ⊗ X
w : ∀ (X Y : C), μ F X Y ≫ F.map (β X Y).hom = (β_ (F.obj X) (F.obj Y)).hom ≫ μ F Y X
⊢ ∀ {X Y : C} (f : X ⟶ Y) (Z : C), f ▷ Z ≫ (β Y Z).hom = (β X Z).hom ≫ Z ◁ f

Tactic:
intros
    apply F.map_injective
    refine (cancel_epi (μ F ?_ ?_)).1 ?_
    rw [Functor.map_comp, ← μ_natural_left_assoc, w, Functor.map_comp,
      reassoc_of% w, braiding_naturality_left_assoc, μ_natural_right]

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

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Category.{v_2, u_2} D
inst✝⁴ : MonoidalCategory C
inst✝³ : MonoidalCategory D
F : C ⥤ D
inst✝² : F.Monoidal
inst✝¹ : F.Faithful
inst✝ : BraidedCategory D
β : (X Y : C) → X ⊗ Y ≅ Y ⊗ X
w : ∀ (X Y : C), μ F X Y ≫ F.map (β X Y).hom = (β_ (F.obj X) (F.obj Y)).hom ≫ μ F Y X
X✝ Y✝ Z✝ : C
⊢ μ F X✝ Y✝ ▷ F.obj Z✝ ≫
      μ F (X✝ ⊗ Y✝) Z✝ ≫ F.map (α_ X✝ Y✝ Z✝).hom ≫ F.map (β X✝ (Y✝ ⊗ Z✝)).hom ≫ F.map (α_ Y✝ Z✝ X✝).hom =
    (μ F X✝ Y✝ ≫ F.map (β X✝ Y✝).hom) ▷ F.obj Z✝ ≫
      μ F (Y✝ ⊗ X✝) Z✝ ≫ F.map (α_ Y✝ X✝ Z✝).hom ≫ F.map (Y✝ ◁ (β X✝ Z✝).hom)

Tactic:
w,

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Category.{v_2, u_2} D
inst✝⁴ : MonoidalCategory C
inst✝³ : MonoidalCategory D
F : C ⥤ D
inst✝² : F.Monoidal
inst✝¹ : F.Faithful
inst✝ : BraidedCategory D
β : (X Y : C) → X ⊗ Y ≅ Y ⊗ X
w : ∀ (X Y : C), μ F X Y ≫ F.map (β X Y).hom = (β_ (F.obj X) (F.obj Y)).hom ≫ μ F Y X
X✝ Y✝ Z✝ : C
⊢ μ F X✝ Y✝ ▷ F.obj Z✝ ≫
      μ F (X✝ ⊗ Y✝) Z✝ ≫ F.map (α_ X✝ Y✝ Z✝).hom ≫ F.map (β X✝ (Y✝ ⊗ Z✝)).hom ≫ F.map (α_ Y✝ Z✝ X✝).hom =
    ((β_ (F.obj X✝) (F.obj Y✝)).hom ≫ μ F Y✝ X✝) ▷ F.obj Z✝ ≫
      μ F (Y✝ ⊗ X✝) Z✝ ≫ F.map (α_ Y✝ X✝ Z✝).hom ≫ F.map (Y✝ ◁ (β X✝ Z✝).hom)
Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Category.{v_2, u_2} D
inst✝⁴ : MonoidalCategory C
inst✝³ : MonoidalCategory D
F : C ⥤ D
inst✝² : F.Monoidal
inst✝¹ : F.Faithful
inst✝ : BraidedCategory D
β : (X Y : C) → X ⊗ Y ≅ Y ⊗ X
w : ∀ (X Y : C), μ F X Y ≫ F.map (β X Y).hom = (β_ (F.obj X) (F.obj Y)).hom ≫ μ F Y X
X✝ Y✝ Z✝ : C
⊢ (α_ (F.obj X✝) (F.obj Y✝) (F.obj Z✝)).hom ≫
      F.obj X✝ ◁ μ F Y✝ Z✝ ≫ μ F X✝ (Y✝ ⊗ Z✝) ≫ F.map (β X✝ (Y✝ ⊗ Z✝)).hom ≫ F.map (α_ Y✝ Z✝ X✝).hom =
    (β_ (F.obj X✝) (F.obj Y✝)).hom ▷ F.obj Z✝ ≫
      (α_ (F.obj Y✝) (F.obj X✝) (F.obj Z✝)).hom ≫ F.obj Y✝ ◁ (μ F X✝ Z✝ ≫ F.map (β X✝ Z✝).hom) ≫ μ F Y✝ (Z✝ ⊗ X✝)

Tactic:
w,

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Category.{v_2, u_2} D
inst✝⁴ : MonoidalCategory C
inst✝³ : MonoidalCategory D
F : C ⥤ D
inst✝² : F.Monoidal
inst✝¹ : F.Faithful
inst✝ : BraidedCategory D
β : (X Y : C) → X ⊗ Y ≅ Y ⊗ X
w : ∀ (X Y : C), μ F X Y ≫ F.map (β X Y).hom = (β_ (F.obj X) (F.obj Y)).hom ≫ μ F Y X
X✝ Y✝ Z✝ : C
⊢ (α_ (F.obj X✝) (F.obj Y✝) (F.obj Z✝)).hom ≫
      F.obj X✝ ◁ μ F Y✝ Z✝ ≫ μ F X✝ (Y✝ ⊗ Z✝) ≫ F.map (β X✝ (Y✝ ⊗ Z✝)).hom ≫ F.map (α_ Y✝ Z✝ X✝).hom =
    (β_ (F.obj X✝) (F.obj Y✝)).hom ▷ F.obj Z✝ ≫
      (α_ (F.obj Y✝) (F.obj X✝) (F.obj Z✝)).hom ≫
        F.obj Y✝ ◁ ((β_ (F.obj X✝) (F.obj Z✝)).hom ≫ μ F Z✝ X✝) ≫ μ F Y✝ (Z✝ ⊗ X✝)
Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Category.{v_2, u_2} D
inst✝⁴ : MonoidalCategory C
inst✝³ : MonoidalCategory D
F : C ⥤ D
inst✝² : F.Monoidal
inst✝¹ : F.Faithful
inst✝ : BraidedCategory D
β : (X Y : C) → X ⊗ Y ≅ Y ⊗ X
w : ∀ (X Y : C), μ F X Y ≫ F.map (β X Y).hom = (β_ (F.obj X) (F.obj Y)).hom ≫ μ F Y X
X✝ Y✝ Z✝ : C
⊢ F.obj X✝ ◁ μ F Y✝ Z✝ ≫
      μ F X✝ (Y✝ ⊗ Z✝) ≫ F.map (α_ X✝ Y✝ Z✝).inv ≫ F.map (β (X✝ ⊗ Y✝) Z✝).hom ≫ F.map (α_ Z✝ X✝ Y✝).inv =
    F.obj X✝ ◁ (μ F Y✝ Z✝ ≫ F.map (β Y✝ Z✝).hom) ≫
      μ F X✝ (Z✝ ⊗ Y✝) ≫ F.map (α_ X✝ Z✝ Y✝).inv ≫ F.map ((β X✝ Z✝).hom ▷ Y✝)

Tactic:
w,

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Category.{v_2, u_2} D
inst✝⁴ : MonoidalCategory C
inst✝³ : MonoidalCategory D
F : C ⥤ D
inst✝² : F.Monoidal
inst✝¹ : F.Faithful
inst✝ : BraidedCategory D
β : (X Y : C) → X ⊗ Y ≅ Y ⊗ X
w : ∀ (X Y : C), μ F X Y ≫ F.map (β X Y).hom = (β_ (F.obj X) (F.obj Y)).hom ≫ μ F Y X
X✝ Y✝ Z✝ : C
⊢ F.obj X✝ ◁ μ F Y✝ Z✝ ≫
      μ F X✝ (Y✝ ⊗ Z✝) ≫ F.map (α_ X✝ Y✝ Z✝).inv ≫ F.map (β (X✝ ⊗ Y✝) Z✝).hom ≫ F.map (α_ Z✝ X✝ Y✝).inv =
    F.obj X✝ ◁ ((β_ (F.obj Y✝) (F.obj Z✝)).hom ≫ μ F Z✝ Y✝) ≫
      μ F X✝ (Z✝ ⊗ Y✝) ≫ F.map (α_ X✝ Z✝ Y✝).inv ≫ F.map ((β X✝ Z✝).hom ▷ Y✝)
Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Category.{v_2, u_2} D
inst✝⁴ : MonoidalCategory C
inst✝³ : MonoidalCategory D
F : C ⥤ D
inst✝² : F.Monoidal
inst✝¹ : F.Faithful
inst✝ : BraidedCategory D
β : (X Y : C) → X ⊗ Y ≅ Y ⊗ X
w : ∀ (X Y : C), μ F X Y ≫ F.map (β X Y).hom = (β_ (F.obj X) (F.obj Y)).hom ≫ μ F Y X
X✝ Y✝ Z✝ : C
⊢ (α_ (F.obj X✝) (F.obj Y✝) (F.obj Z✝)).inv ≫
      μ F X✝ Y✝ ▷ F.obj Z✝ ≫ μ F (X✝ ⊗ Y✝) Z✝ ≫ F.map (β (X✝ ⊗ Y✝) Z✝).hom ≫ F.map (α_ Z✝ X✝ Y✝).inv =
    F.obj X✝ ◁ (β_ (F.obj Y✝) (F.obj Z✝)).hom ≫
      (α_ (F.obj X✝) (F.obj Z✝) (F.obj Y✝)).inv ≫ (μ F X✝ Z✝ ≫ F.map (β X✝ Z✝).hom) ▷ F.obj Y✝ ≫ μ F (Z✝ ⊗ X✝) Y✝

Tactic:
w,

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Category.{v_2, u_2} D
inst✝⁴ : MonoidalCategory C
inst✝³ : MonoidalCategory D
F : C ⥤ D
inst✝² : F.Monoidal
inst✝¹ : F.Faithful
inst✝ : BraidedCategory D
β : (X Y : C) → X ⊗ Y ≅ Y ⊗ X
w : ∀ (X Y : C), μ F X Y ≫ F.map (β X Y).hom = (β_ (F.obj X) (F.obj Y)).hom ≫ μ F Y X
X✝ Y✝ Z✝ : C
⊢ (α_ (F.obj X✝) (F.obj Y✝) (F.obj Z✝)).inv ≫
      μ F X✝ Y✝ ▷ F.obj Z✝ ≫ μ F (X✝ ⊗ Y✝) Z✝ ≫ F.map (β (X✝ ⊗ Y✝) Z✝).hom ≫ F.map (α_ Z✝ X✝ Y✝).inv =
    F.obj X✝ ◁ (β_ (F.obj Y✝) (F.obj Z✝)).hom ≫
      (α_ (F.obj X✝) (F.obj Z✝) (F.obj Y✝)).inv ≫
        ((β_ (F.obj X✝) (F.obj Z✝)).hom ≫ μ F Z✝ X✝) ▷ F.obj Y✝ ≫ μ F (Z✝ ⊗ X✝) Y✝
Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X : C
⊢ (α_ (𝟙_ C) (𝟙_ C) X).hom ≫ 𝟙_ C ◁ (β_ X (𝟙_ C)).inv ≫ (α_ (𝟙_ C) X (𝟙_ C)).inv ≫ (λ_ X).hom ▷ 𝟙_ C =
    (λ_ (𝟙_ C)).hom ▷ X ≫ (β_ X (𝟙_ C)).inv

Tactic:
monoidal

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X : C
⊢ (α_ (𝟙_ C) (𝟙_ C) X).inv ≫ (ρ_ (𝟙_ C)).hom ▷ X = 𝟙_ C ◁ (λ_ X).hom

Tactic:
triangle_assoc_comp_right

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X : C
⊢ 𝟙_ C ◁ (λ_ X).hom = 𝟙_ C ◁ (λ_ X).hom
Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X : C
⊢ ((λ_ X).hom ≫ (ρ_ X).inv) ≫ (ρ_ X).hom ≫ (λ_ X).inv = 𝟙 (𝟙_ C ⊗ X)

Tactic:
monoidal

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X : C
⊢ ((ρ_ X).hom ≫ (λ_ X).inv) ≫ (λ_ X).hom ≫ (ρ_ X).inv = 𝟙 (X ⊗ 𝟙_ C)

Tactic:
monoidal

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X₁ X₂ : C
⊢ (X₁ ⊗ X₂) ◁ (λ_ (𝟙_ C)).inv ≫ (α_ X₁ X₂ (𝟙_ C ⊗ 𝟙_ C)).hom ≫ X₁ ◁ (α_ X₂ (𝟙_ C) (𝟙_ C)).inv =
    (α_ X₁ X₂ (𝟙_ C)).hom ≫ X₁ ◁ (ρ_ X₂).inv ▷ 𝟙_ C

Tactic:
monoidal

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X₁ X₂ Y₁ Y₂ Z₁ Z₂ : C
⊢ ((α_ X₁ X₂ (Y₁ ⊗ Y₂)).hom ≫
          X₁ ◁ (α_ X₂ Y₁ Y₂).inv ≫ X₁ ◁ (β_ X₂ Y₁).hom ▷ Y₂ ≫ X₁ ◁ (α_ Y₁ X₂ Y₂).hom ≫ (α_ X₁ Y₁ (X₂ ⊗ Y₂)).inv) ▷
        (Z₁ ⊗ Z₂) ≫
      ((α_ (X₁ ⊗ Y₁) (X₂ ⊗ Y₂) (Z₁ ⊗ Z₂)).hom ≫
          (X₁ ⊗ Y₁) ◁ (α_ (X₂ ⊗ Y₂) Z₁ Z₂).inv ≫
            (X₁ ⊗ Y₁) ◁
                ((α_ X₂ Y₂ Z₁).hom ≫
                    X₂ ◁ (β_ Y₂ Z₁).hom ≫ (α_ X₂ Z₁ Y₂).inv ≫ (β_ X₂ Z₁).hom ▷ Y₂ ≫ (α_ Z₁ X₂ Y₂).hom) ▷
                  Z₂ ≫
              (X₁ ⊗ Y₁) ◁ (α_ Z₁ (X₂ ⊗ Y₂) Z₂).hom ≫ (α_ (X₁ ⊗ Y₁) Z₁ ((X₂ ⊗ Y₂) ⊗ Z₂)).inv) ≫
        ((α_ X₁ Y₁ Z₁).hom ⊗ₘ (α_ X₂ Y₂ Z₂).hom) =
    𝟙 (((X₁ ⊗ X₂) ⊗ Y₁ ⊗ Y₂) ⊗ Z₁ ⊗ Z₂) ⊗≫
      X₁ ◁ ((β_ X₂ Y₁).hom ▷ (Y₂ ⊗ Z₁) ≫ (Y₁ ⊗ X₂) ◁ (β_ Y₂ Z₁).hom) ▷ Z₂ ⊗≫
        X₁ ◁ Y₁ ◁ (β_ X₂ Z₁).hom ▷ Y₂ ▷ Z₂ ⊗≫ 𝟙 ((X₁ ⊗ Y₁ ⊗ Z₁) ⊗ X₂ ⊗ Y₂ ⊗ Z₂)

Tactic:
monoidal

Goal state after:
Module: Mathlib.Algebra.Category.Grp.Colimits

Goal state before:
pp: J : Type u
inst✝² : Category.{v, u} J
F : J ⥤ AddCommGrpCat
c : Cocone F
inst✝¹ : DecidableEq J
A : Type w
inst✝ : AddCommGroup A
f : Quot F →+ A
hc : IsColimit c
j : J
x : ↑(F.obj j)
⊢ (ConcreteCategory.hom (c.ι.app j ≫ hc.desc (toCocone F f))) x = f ((ι F j) x)

Tactic:
hc.fac

Goal state after:
J : Type u
inst✝² : Category.{v, u} J
F : J ⥤ AddCommGrpCat
c : Cocone F
inst✝¹ : DecidableEq J
A : Type w
inst✝ : AddCommGroup A
f : Quot F →+ A
hc : IsColimit c
j : J
x : ↑(F.obj j)
⊢ (ConcreteCategory.hom ((toCocone F f).ι.app j)) x = f ((ι F j) x)
Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X₁ X₂ Y₁ Y₂ Z₁ Z₂ : C
⊢ 𝟙 (((X₁ ⊗ X₂) ⊗ Y₁ ⊗ Y₂) ⊗ Z₁ ⊗ Z₂) ⊗≫
      X₁ ◁ ((X₂ ⊗ Y₁) ◁ (β_ Y₂ Z₁).hom ≫ (β_ X₂ Y₁).hom ▷ (Z₁ ⊗ Y₂)) ▷ Z₂ ⊗≫
        X₁ ◁ Y₁ ◁ (β_ X₂ Z₁).hom ▷ Y₂ ▷ Z₂ ⊗≫ 𝟙 ((X₁ ⊗ Y₁ ⊗ Z₁) ⊗ X₂ ⊗ Y₂ ⊗ Z₂) =
    (α_ (X₁ ⊗ X₂) (Y₁ ⊗ Y₂) (Z₁ ⊗ Z₂)).hom ≫
      (X₁ ⊗ X₂) ◁
          ((α_ Y₁ Y₂ (Z₁ ⊗ Z₂)).hom ≫
            Y₁ ◁ (α_ Y₂ Z₁ Z₂).inv ≫ Y₁ ◁ (β_ Y₂ Z₁).hom ▷ Z₂ ≫ Y₁ ◁ (α_ Z₁ Y₂ Z₂).hom ≫ (α_ Y₁ Z₁ (Y₂ ⊗ Z₂)).inv) ≫
        (α_ X₁ X₂ ((Y₁ ⊗ Z₁) ⊗ Y₂ ⊗ Z₂)).hom ≫
          X₁ ◁ (α_ X₂ (Y₁ ⊗ Z₁) (Y₂ ⊗ Z₂)).inv ≫
            X₁ ◁
                ((α_ X₂ Y₁ Z₁).inv ≫
                    (β_ X₂ Y₁).hom ▷ Z₁ ≫ (α_ Y₁ X₂ Z₁).hom ≫ Y₁ ◁ (β_ X₂ Z₁).hom ≫ (α_ Y₁ Z₁ X₂).inv) ▷
                  (Y₂ ⊗ Z₂) ≫
              X₁ ◁ (α_ (Y₁ ⊗ Z₁) X₂ (Y₂ ⊗ Z₂)).hom ≫ (α_ X₁ (Y₁ ⊗ Z₁) (X₂ ⊗ Y₂ ⊗ Z₂)).inv

Tactic:
monoidal

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.Mates

Goal state before:
pp: case a.a
C : Type u₁
D : Type u₂
E : Type u₃
F : Type u₄
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
inst✝¹ : Category.{v₃, u₃} E
inst✝ : Category.{v₄, u₄} F
G : C ⥤ E
H : D ⥤ F
L₁ : C ⥤ D
R₁ : D ⥤ C
L₂ : E ⥤ F
R₂ : F ⥤ E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
α : TwoSquare G L₁ L₂ H
c : C
| R₂.map ((G ⋙ L₂).map (adj₁.unit.app c) ≫ α.natTrans.app (R₁.obj (L₁.obj c)))

pp: case a.a
C : Type u₁
D : Type u₂
E : Type u₃
F : Type u₄
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
inst✝¹ : Category.{v₃, u₃} E
inst✝ : Category.{v₄, u₄} F
G : C ⥤ E
H : D ⥤ F
L₁ : C ⥤ D
R₁ : D ⥤ C
L₂ : E ⥤ F
R₂ : F ⥤ E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
α : TwoSquare G L₁ L₂ H
c : C
| R₂.map (H.map (adj₁.counit.app (L₁.obj c)))

pp: case a
C : Type u₁
D : Type u₂
E : Type u₃
F : Type u₄
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
inst✝¹ : Category.{v₃, u₃} E
inst✝ : Category.{v₄, u₄} F
G : C ⥤ E
H : D ⥤ F
L₁ : C ⥤ D
R₁ : D ⥤ C
L₂ : E ⥤ F
R₂ : F ⥤ E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
α : TwoSquare G L₁ L₂ H
c : C
| adj₂.unit.app (G.obj c)

Tactic:
α.naturality

Goal state after:
case a.a
C : Type u₁
D : Type u₂
E : Type u₃
F : Type u₄
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
inst✝¹ : Category.{v₃, u₃} E
inst✝ : Category.{v₄, u₄} F
G : C ⥤ E
H : D ⥤ F
L₁ : C ⥤ D
R₁ : D ⥤ C
L₂ : E ⥤ F
R₂ : F ⥤ E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
α : TwoSquare G L₁ L₂ H
c : C
| R₂.map (α.app c ≫ (L₁ ⋙ H).map (adj₁.unit.app c))

case a.a
C : Type u₁
D : Type u₂
E : Type u₃
F : Type u₄
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
inst✝¹ : Category.{v₃, u₃} E
inst✝ : Category.{v₄, u₄} F
G : C ⥤ E
H : D ⥤ F
L₁ : C ⥤ D
R₁ : D ⥤ C
L₂ : E ⥤ F
R₂ : F ⥤ E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
α : TwoSquare G L₁ L₂ H
c : C
| R₂.map (H.map (adj₁.counit.app (L₁.obj c)))

case a
C : Type u₁
D : Type u₂
E : Type u₃
F : Type u₄
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
inst✝¹ : Category.{v₃, u₃} E
inst✝ : Category.{v₄, u₄} F
G : C ⥤ E
H : D ⥤ F
L₁ : C ⥤ D
R₁ : D ⥤ C
L₂ : E ⥤ F
R₂ : F ⥤ E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
α : TwoSquare G L₁ L₂ H
c : C
| adj₂.unit.app (G.obj c)
Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X₁ X₂ : C
⊢ (λ_ X₁).hom ⊗ₘ (λ_ X₂).hom =
    (α_ (𝟙_ C) X₁ (𝟙_ C ⊗ X₂)).hom ≫ 𝟙_ C ◁ (α_ X₁ (𝟙_ C) X₂).inv ≫ (λ_ ((X₁ ⊗ 𝟙_ C) ⊗ X₂)).hom ≫ (ρ_ X₁).hom ▷ X₂

Tactic:
monoidal

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X₁ X₂ : C
⊢ (ρ_ X₁).hom ⊗ₘ (ρ_ X₂).hom =
    (α_ X₁ (𝟙_ C) (X₂ ⊗ 𝟙_ C)).hom ≫ X₁ ◁ (α_ (𝟙_ C) X₂ (𝟙_ C)).inv ≫ X₁ ◁ (ρ_ (𝟙_ C ⊗ X₂)).hom ≫ X₁ ◁ (λ_ X₂).hom

Tactic:
monoidal

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X₁ X₂ : C
⊢ (α_ X₁ (𝟙_ C) (X₂ ⊗ 𝟙_ C)).hom ≫
      X₁ ◁ (α_ (𝟙_ C) X₂ (𝟙_ C)).inv ≫ X₁ ◁ (ρ_ (𝟙_ C ⊗ X₂)).hom ≫ X₁ ◁ ((β_ (𝟙_ C) X₂).hom ≫ (ρ_ X₂).hom) =
    ((α_ X₁ (𝟙_ C) (X₂ ⊗ 𝟙_ C)).hom ≫
        X₁ ◁ (α_ (𝟙_ C) X₂ (𝟙_ C)).inv ≫
          X₁ ◁ (β_ (𝟙_ C) X₂).hom ▷ 𝟙_ C ≫ X₁ ◁ (α_ X₂ (𝟙_ C) (𝟙_ C)).hom ≫ (α_ X₁ X₂ (𝟙_ C ⊗ 𝟙_ C)).inv) ≫
      (X₁ ⊗ X₂) ◁ (λ_ (𝟙_ C)).hom ≫ (ρ_ (X₁ ⊗ X₂)).hom

Tactic:
monoidal

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X₁ X₂ X₃ Y₁ Y₂ Y₃ : C
⊢ ((α_ (X₁ ⊗ X₂) X₃ ((Y₁ ⊗ Y₂) ⊗ Y₃)).hom ≫
        (X₁ ⊗ X₂) ◁ (α_ X₃ (Y₁ ⊗ Y₂) Y₃).inv ≫
          (X₁ ⊗ X₂) ◁
              ((α_ X₃ Y₁ Y₂).inv ≫ (β_ X₃ Y₁).hom ▷ Y₂ ≫ (α_ Y₁ X₃ Y₂).hom ≫ Y₁ ◁ (β_ X₃ Y₂).hom ≫ (α_ Y₁ Y₂ X₃).inv) ▷
                Y₃ ≫
            (X₁ ⊗ X₂) ◁ (α_ (Y₁ ⊗ Y₂) X₃ Y₃).hom ≫ (α_ (X₁ ⊗ X₂) (Y₁ ⊗ Y₂) (X₃ ⊗ Y₃)).inv) ≫
      ((α_ X₁ X₂ (Y₁ ⊗ Y₂)).hom ≫
            X₁ ◁ (α_ X₂ Y₁ Y₂).inv ≫ X₁ ◁ (β_ X₂ Y₁).hom ▷ Y₂ ≫ X₁ ◁ (α_ Y₁ X₂ Y₂).hom ≫ (α_ X₁ Y₁ (X₂ ⊗ Y₂)).inv) ▷
          (X₃ ⊗ Y₃) ≫
        (α_ (X₁ ⊗ Y₁) (X₂ ⊗ Y₂) (X₃ ⊗ Y₃)).hom =
    𝟙 (((X₁ ⊗ X₂) ⊗ X₃) ⊗ (Y₁ ⊗ Y₂) ⊗ Y₃) ⊗≫
      X₁ ◁ X₂ ◁ (β_ X₃ Y₁).hom ▷ Y₂ ▷ Y₃ ⊗≫
        X₁ ◁ ((X₂ ⊗ Y₁) ◁ (β_ X₃ Y₂).hom ≫ (β_ X₂ Y₁).hom ▷ (Y₂ ⊗ X₃)) ▷ Y₃ ⊗≫ 𝟙 ((X₁ ⊗ Y₁) ⊗ (X₂ ⊗ Y₂) ⊗ X₃ ⊗ Y₃)

Tactic:
monoidal

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X₁ X₂ X₃ Y₁ Y₂ Y₃ : C
⊢ 𝟙 (((X₁ ⊗ X₂) ⊗ X₃) ⊗ (Y₁ ⊗ Y₂) ⊗ Y₃) ⊗≫
      X₁ ◁ X₂ ◁ (β_ X₃ Y₁).hom ▷ Y₂ ▷ Y₃ ⊗≫
        X₁ ◁ ((β_ X₂ Y₁).hom ▷ (X₃ ⊗ Y₂) ≫ (Y₁ ⊗ X₂) ◁ (β_ X₃ Y₂).hom) ▷ Y₃ ⊗≫ 𝟙 ((X₁ ⊗ Y₁) ⊗ (X₂ ⊗ Y₂) ⊗ X₃ ⊗ Y₃) =
    ((α_ X₁ X₂ X₃).hom ⊗ₘ (α_ Y₁ Y₂ Y₃).hom) ≫
      ((α_ X₁ (X₂ ⊗ X₃) (Y₁ ⊗ Y₂ ⊗ Y₃)).hom ≫
          X₁ ◁ (α_ (X₂ ⊗ X₃) Y₁ (Y₂ ⊗ Y₃)).inv ≫
            X₁ ◁
                ((α_ X₂ X₃ Y₁).hom ≫
                    X₂ ◁ (β_ X₃ Y₁).hom ≫ (α_ X₂ Y₁ X₃).inv ≫ (β_ X₂ Y₁).hom ▷ X₃ ≫ (α_ Y₁ X₂ X₃).hom) ▷
                  (Y₂ ⊗ Y₃) ≫
              X₁ ◁ (α_ Y₁ (X₂ ⊗ X₃) (Y₂ ⊗ Y₃)).hom ≫ (α_ X₁ Y₁ ((X₂ ⊗ X₃) ⊗ Y₂ ⊗ Y₃)).inv) ≫
        (X₁ ⊗ Y₁) ◁
          ((α_ X₂ X₃ (Y₂ ⊗ Y₃)).hom ≫
            X₂ ◁ (α_ X₃ Y₂ Y₃).inv ≫ X₂ ◁ (β_ X₃ Y₂).hom ▷ Y₃ ≫ X₂ ◁ (α_ Y₂ X₃ Y₃).hom ≫ (α_ X₂ Y₂ (X₃ ⊗ Y₃)).inv)

Tactic:
monoidal

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.Mates

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
L₁ L₂ : C ⥤ D
R₁ R₂ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
α : R₁ ⟶ R₂
inst✝ : IsIso ((conjugateEquiv adj₁ adj₂).symm α)
⊢ IsIso α

Tactic:
suffices IsIso ((conjugateEquiv adj₁ adj₂) ((conjugateEquiv adj₁ adj₂).symm α))
    by simpa using this

Goal state after:
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
L₁ L₂ : C ⥤ D
R₁ R₂ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
α : R₁ ⟶ R₂
inst✝ : IsIso ((conjugateEquiv adj₁ adj₂).symm α)
⊢ IsIso ((conjugateEquiv adj₁ adj₂) ((conjugateEquiv adj₁ adj₂).symm α))
Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

Goal state before:
pp: R✝ : Type u₁
S✝ : Type u₂
inst✝⁵ : CommRing R✝
inst✝⁴ : CommRing S✝
f✝ : R✝ →+* S✝
R : Type u₁
S : Type u₂
inst✝³ : Ring R
inst✝² : Ring S
f : R →+* S
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : S
g : ↑((restrictScalars f).obj (of S S)) →ₗ[R] M
r : R
t : S
⊢ g (r • t * s) = (RingHom.id R) r • g (t * s)

Tactic:
by
        simp [← map_smul, ModuleCat.restrictScalars.smul_def (M := ModuleCat.of _ S), mul_assoc]

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

Goal state before:
pp: R : Type u₁
inst✝ : CommRing R
M : ModuleCat R
m : ↑M
⊢ (ConcreteCategory.hom ((extendScalarsId R).hom.app M)) ((ConcreteCategory.hom ((extendScalarsId R).inv.app M)) m) =
    (Hom.hom ((restrictScalarsId R).inv.app M)) m

Tactic:
← comp_apply

Goal state after:
R : Type u₁
inst✝ : CommRing R
M : ModuleCat R
m : ↑M
⊢ (ConcreteCategory.hom ((extendScalarsId R).inv.app M ≫ (extendScalarsId R).hom.app M)) m =
    (Hom.hom ((restrictScalarsId R).inv.app M)) m
Module: Mathlib.CategoryTheory.Category.Bipointed

Goal state before:
pp: X Y Z : Bipointed
f : X.Hom Y
g : Y.Hom Z
⊢ (g.toFun ∘ f.toFun) X.toProd.1 = Z.toProd.1

Tactic:
by rw [Function.comp_apply, f.map_fst, g.map_fst]

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

Goal state before:
pp: C : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} C
inst✝⁹ : MonoidalCategory C
M N O : C
inst✝⁸ : ComonObj M
inst✝⁷ : ComonObj N
inst✝⁶ : ComonObj O
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
F : C ⥤ D
inst✝³ : F.OplaxMonoidal
X Y : C
inst✝² : ComonObj X
inst✝¹ : ComonObj Y
f : X ⟶ Y
inst✝ : IsComonHom f
⊢ F.map f ≫ F.map Δ ≫ δ F Y Y = (F.map Δ ≫ δ F X X) ≫ (F.map f ⊗ₘ F.map f)

Tactic:
rw [Category.assoc, δ_natural, ← F.map_comp_assoc, ← F.map_comp_assoc, hom_comul]

Goal state after:
Module: Mathlib.RingTheory.TwoSidedIdeal.Operations

Goal state before:
pp: case refine_2
R : Type u_1
inst✝ : NonUnitalRing R
s : Set R
z : R
⊢ ∀ (y x : R), y ∈ s ∪ s * univ ∪ univ * s ∪ univ * s * univ → y * x ∈ s ∪ s * univ ∪ univ * s ∪ univ * s * univ

Tactic:
· rintro y x (((hy | ⟨y, hy, r, -, rfl⟩) | ⟨r, -, y, hy, rfl⟩) |
        ⟨-, ⟨r', -, y, hy, rfl⟩, r, -, rfl⟩)
      · exact .inl <| .inl <| .inr ⟨y, hy, x, mem_univ _, rfl⟩
      · exact .inl <| .inl <| .inr ⟨y, hy, r * x, mem_univ _, (mul_assoc ..).symm⟩
      · exact .inr <| ⟨r * y, ⟨r, mem_univ _, y, hy, rfl⟩, x, mem_univ _, rfl⟩
      · refine .inr <| ⟨r' * y, ⟨r', mem_univ _, y, hy, rfl⟩, r * x, mem_univ _, ?_⟩
        simp [mul_assoc]

Goal state after: