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
X : C
f : J → C
Y : C
⊢ (leftDistributor X f ⊗ᵢ asIso (𝟙 Y)) ≪≫ rightDistributor (fun j ↦ X ⊗ f j) Y =
    α_ X (⨁ f) Y ≪≫
      (asIso (𝟙 X) ⊗ᵢ rightDistributor f Y) ≪≫
        (leftDistributor X fun j ↦ f j ⊗ Y) ≪≫ biproduct.mapIso fun x ↦ (α_ X (f x) Y).symm

Tactic:
cases nonempty_fintype J

Goal state after:
case intro
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
X : C
f : J → C
Y : C
val✝ : Fintype J
⊢ (leftDistributor X f ⊗ᵢ asIso (𝟙 Y)) ≪≫ rightDistributor (fun j ↦ X ⊗ f j) Y =
    α_ X (⨁ f) Y ≪≫
      (asIso (𝟙 X) ⊗ᵢ rightDistributor f Y) ≪≫
        (leftDistributor X fun j ↦ f j ⊗ Y) ≪≫ biproduct.mapIso fun x ↦ (α_ X (f x) Y).symm
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
X Y : C
f : J → C
g h : X ⊗ ⨁ f ⟶ Y
w : ∀ (j : J), X ◁ biproduct.ι f j ≫ g = X ◁ biproduct.ι f j ≫ h
⊢ g = h

Tactic:
cases nonempty_fintype J

Goal state after:
case intro
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
X Y : C
f : J → C
g h : X ⊗ ⨁ f ⟶ Y
w : ∀ (j : J), X ◁ biproduct.ι f j ≫ g = X ◁ biproduct.ι f j ≫ h
val✝ : Fintype J
⊢ g = h
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
X Y : C
f : J → C
g h : X ⟶ Y ⊗ ⨁ f
w : ∀ (j : J), g ≫ Y ◁ biproduct.π f j = h ≫ Y ◁ biproduct.π f j
⊢ g = h

Tactic:
cases nonempty_fintype J

Goal state after:
case intro
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
X Y : C
f : J → C
g h : X ⟶ Y ⊗ ⨁ f
w : ∀ (j : J), g ≫ Y ◁ biproduct.π f j = h ≫ Y ◁ biproduct.π f j
val✝ : Fintype J
⊢ g = h
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
g h : (⨁ f) ⊗ X ⟶ Y
w : ∀ (j : J), biproduct.ι f j ▷ X ≫ g = biproduct.ι f j ▷ X ≫ h
⊢ g = h

Tactic:
cases nonempty_fintype J

Goal state after:
case intro
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
g h : (⨁ f) ⊗ X ⟶ Y
w : ∀ (j : J), biproduct.ι f j ▷ X ≫ g = biproduct.ι f j ▷ X ≫ h
val✝ : Fintype J
⊢ g = h
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
g h : X ⟶ (⨁ f) ⊗ Y
w : ∀ (j : J), g ≫ biproduct.π f j ▷ Y = h ≫ biproduct.π f j ▷ Y
⊢ g = h

Tactic:
cases nonempty_fintype J

Goal state after:
case intro
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
g h : X ⟶ (⨁ f) ⊗ Y
w : ∀ (j : J), g ≫ biproduct.π f j ▷ Y = h ≫ biproduct.π f j ▷ Y
val✝ : Fintype J
⊢ g = h
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
F : C ⥤ D
inst✝ : F.LaxMonoidal
X : C
⊢ ε F ▷ F.obj X ≫ μ F (𝟙_ C) X = ε F ▷ F.obj X ≫ μ F (𝟙_ C) X ≫ F.map (𝟙 (𝟙_ C ⊗ X))

Tactic:
F.map_id,

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
F : C ⥤ D
inst✝ : F.LaxMonoidal
X : C
⊢ ε F ▷ F.obj X ≫ μ F (𝟙_ C) X = ε F ▷ F.obj X ≫ μ F (𝟙_ C) X ≫ 𝟙 (F.obj (𝟙_ C ⊗ X))
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
F : C ⥤ D
inst✝ : F.LaxMonoidal
X : C
⊢ F.obj X ◁ ε F ≫ μ F X (𝟙_ C) = F.obj X ◁ ε F ≫ μ F X (𝟙_ C) ≫ F.map (𝟙 (X ⊗ 𝟙_ C))

Tactic:
F.map_id,

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
F : C ⥤ D
inst✝ : F.LaxMonoidal
X : C
⊢ F.obj X ◁ ε F ≫ μ F X (𝟙_ C) = F.obj X ◁ ε F ≫ μ F X (𝟙_ C) ≫ 𝟙 (F.obj (X ⊗ 𝟙_ C))
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
F : C ⥤ D
inst✝ : F.LaxMonoidal
X Y Z : C
⊢ μ F X Y ▷ F.obj Z ≫ μ F (X ⊗ Y) Z ≫ F.map (𝟙 ((X ⊗ Y) ⊗ Z)) = μ F X Y ▷ F.obj Z ≫ μ F (X ⊗ Y) Z

Tactic:
F.map_id,

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
F : C ⥤ D
inst✝ : F.LaxMonoidal
X Y Z : C
⊢ μ F X Y ▷ F.obj Z ≫ μ F (X ⊗ Y) Z ≫ 𝟙 (F.obj ((X ⊗ Y) ⊗ Z)) = μ F X Y ▷ F.obj Z ≫ μ F (X ⊗ Y) Z
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
F : C ⥤ D
inst✝ : F.OplaxMonoidal
X : C
⊢ δ F (𝟙_ C) X ≫ η F ▷ F.obj X = F.map (𝟙 (𝟙_ C ⊗ X)) ≫ δ F (𝟙_ C) X ≫ η F ▷ F.obj X

Tactic:
F.map_id,

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
F : C ⥤ D
inst✝ : F.OplaxMonoidal
X : C
⊢ δ F (𝟙_ C) X ≫ η F ▷ F.obj X = 𝟙 (F.obj (𝟙_ C ⊗ X)) ≫ δ F (𝟙_ C) X ≫ η F ▷ F.obj X
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
F : C ⥤ D
inst✝ : F.OplaxMonoidal
X : C
⊢ δ F X (𝟙_ C) ≫ F.obj X ◁ η F = F.map (𝟙 (X ⊗ 𝟙_ C)) ≫ δ F X (𝟙_ C) ≫ F.obj X ◁ η F

Tactic:
F.map_id,

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
F : C ⥤ D
inst✝ : F.OplaxMonoidal
X : C
⊢ δ F X (𝟙_ C) ≫ F.obj X ◁ η F = 𝟙 (F.obj (X ⊗ 𝟙_ C)) ≫ δ F X (𝟙_ C) ≫ F.obj X ◁ η F
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
F : C ⥤ D
inst✝ : F.OplaxMonoidal
X Y Z : C
⊢ δ F X (Y ⊗ Z) ≫ F.obj X ◁ δ F Y Z = F.map (𝟙 (X ⊗ Y ⊗ Z)) ≫ δ F X (Y ⊗ Z) ≫ F.obj X ◁ δ F Y Z

Tactic:
F.map_id,

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
F : C ⥤ D
inst✝ : F.OplaxMonoidal
X Y Z : C
⊢ δ F X (Y ⊗ Z) ≫ F.obj X ◁ δ F Y Z = 𝟙 (F.obj (X ⊗ Y ⊗ Z)) ≫ δ F X (Y ⊗ Z) ≫ F.obj X ◁ δ F Y Z
Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
M N : SemimoduleCat R
f : M ⟶ N
⊢ tensorHom f (𝟙 (of R R)) ≫ (rightUnitor N).hom = (rightUnitor M).hom ≫ f

Tactic:
by
  ext : 1
  -- Porting note (https://github.com/leanprover-community/mathlib4/issues/11041): broken ext
  apply TensorProduct.ext
  ext
  simp [tensorHom, tensorObj, rightUnitor]

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic

Goal state before:
pp: R : Type u
inst✝ : CommRing R
⊢ MonoidalLinear R (ModuleCat R)

Tactic:
by
  refine ⟨?_, ?_⟩
  · intros
    ext : 1
    refine TensorProduct.ext (LinearMap.ext fun x => LinearMap.ext fun y => ?_)
    simp [ModuleCat.hom_whiskerLeft]
  · intros
    ext : 1
    refine TensorProduct.ext (LinearMap.ext fun x => LinearMap.ext fun y => ?_)
    simp [ModuleCat.hom_whiskerRight]

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
⊢ ε (opOpEquivalence C).inverse =
    (opOpEquivalence C).toAdjunction.unit.app (𝟙_ Cᵒᵖᵒᵖ) ≫
      (opOpEquivalence C).inverse.map (η (opOpEquivalence C).functor)

Tactic:
by simp [opOpEquivalence]

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
⊢ ∀ (X Y : C),
    μ (opOpEquivalence C).inverse X Y =
      (opOpEquivalence C).toAdjunction.unit.app
          ((opOpEquivalence C).inverse.obj X ⊗ (opOpEquivalence C).inverse.obj Y) ≫
        (opOpEquivalence C).inverse.map
          (δ (opOpEquivalence C).functor ((opOpEquivalence C).inverse.obj X) ((opOpEquivalence C).inverse.obj Y) ≫
            ((opOpEquivalence C).toAdjunction.counit.app X ⊗ₘ (opOpEquivalence C).toAdjunction.counit.app Y))

Tactic:
by simp [opOpEquivalence]

Goal state after:
Module: Mathlib.Tactic.CategoryTheory.Monoidal.Normalize

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
f g : C
η : f ⟶ g
η₁ : f ⟶ 𝟙_ C ⊗ g
η₂ : 𝟙_ C ⊗ f ⟶ 𝟙_ C ⊗ g
e_η₁ : η ≫ (λ_ g).inv = η₁
e_η₂ : (λ_ f).hom ≫ η₁ = η₂
⊢ 𝟙_ C ◁ η = η₂

Tactic:
simp [e_η₁, e_η₂]

Goal state after:
Module: Mathlib.Tactic.CategoryTheory.Monoidal.Normalize

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
f g : C
η : f ⟶ g
η₁ : f ⟶ g ⊗ 𝟙_ C
η₂ : f ⊗ 𝟙_ C ⟶ g ⊗ 𝟙_ C
e_η₁ : η ≫ (ρ_ g).inv = η₁
e_η₂ : (ρ_ f).hom ≫ η₁ = η₂
⊢ η ▷ 𝟙_ C = η₂

Tactic:
simp [e_η₁, e_η₂]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
G : C ⥤ D
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : PreservesLimit (cospan f g) G
c : Cone (cospan g f)
hc : IsLimit c
⊢ IsLimit (G.mapCone c)

Tactic:
apply (IsLimit.postcomposeHomEquiv (diagramIsoCospan.{v₂} _) _).toFun
    apply IsLimit.ofIsoLimit _ (PullbackCone.isoMk _).symm
    apply PullbackCone.isLimitOfFlip
    apply (isLimitMapConePullbackConeEquiv _ _).toFun
    · refine @isLimitOfPreserves _ _ _ _ _ _ _ _ _ ?_ ?_
      · apply PullbackCone.isLimitOfFlip
        apply IsLimit.ofIsoLimit _ (PullbackCone.isoMk _)
        exact (IsLimit.postcomposeHomEquiv (diagramIsoCospan.{v₁} _) _).invFun hc
      · dsimp
        infer_instance
    · exact
        (c.π.naturality WalkingCospan.Hom.inr).symm.trans
          (c.π.naturality WalkingCospan.Hom.inl :)

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
inst✝ : W.ContainsIdentities
x : C
⊢ W (CategoryTheory.eqToHom ⋯)

Tactic:
eqToHom_refl

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
inst✝ : W.ContainsIdentities
x : C
⊢ W (𝟙 x)
Module: Mathlib.CategoryTheory.MorphismProperty.Composition

Goal state before:
pp: case a
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F₁ F₂ : C ⥤ D
app : (X : C) → F₁.obj X ⟶ F₂.obj X
X Y : C
e : X ≅ Y
he : F₁.map e.hom ≫ app Y = app X ≫ F₂.map e.hom
| F₁.map e.hom ≫ app Y

pp: case a
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F₁ F₂ : C ⥤ D
app : (X : C) → F₁.obj X ⟶ F₂.obj X
X Y : C
e : X ≅ Y
he : F₁.map e.hom ≫ app Y = app X ≫ F₂.map e.hom
| F₂.map e.inv

Tactic:
he

Goal state after:
case a
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F₁ F₂ : C ⥤ D
app : (X : C) → F₁.obj X ⟶ F₂.obj X
X Y : C
e : X ≅ Y
he : F₁.map e.hom ≫ app Y = app X ≫ F₂.map e.hom
| app X ≫ F₂.map e.hom

case a
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F₁ F₂ : C ⥤ D
app : (X : C) → F₁.obj X ⟶ F₂.obj X
X Y : C
e : X ≅ Y
he : F₁.map e.hom ≫ app Y = app X ≫ F₂.map e.hom
| F₂.map e.inv
Module: Mathlib.CategoryTheory.ConcreteCategory.EpiMono

Goal state before:
pp: case mp
C : Type u
inst✝² : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
h : MorphismProperty.injective C = monomorphisms C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
hf : monomorphisms C f
⊢ Mono ((forget C).map f)

Tactic:
mono_iff_injective

Goal state after:
case mp
C : Type u
inst✝² : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
h : MorphismProperty.injective C = monomorphisms C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
hf : monomorphisms C f
⊢ Function.Injective ⇑(hom ((forget C).map f))
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 : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : G.LaxMonoidal
x✝ : C
⊢ (adj.homEquiv x✝ (F.obj x✝ ⊗ 𝟙_ D)) (ρ_ (F.obj x✝)).inv =
    (adj.homEquiv x✝ (F.obj x✝ ⊗ 𝟙_ D))
      (F.map (ρ_ x✝).inv ≫
        (adj.homEquiv (x✝ ⊗ 𝟙_ C) (F.obj x✝ ⊗ F.obj (𝟙_ C))).symm
            ((adj.unit.app x✝ ⊗ₘ adj.unit.app (𝟙_ C)) ≫ μ G (F.obj x✝) (F.obj (𝟙_ C))) ≫
          F.obj x✝ ◁ (adj.homEquiv (𝟙_ C) (𝟙_ D)).symm (ε G))

Tactic:
rw [Adjunction.homEquiv_naturality_left, Adjunction.homEquiv_naturality_right,
      Equiv.apply_symm_apply, assoc, ← μ_natural_right, ← id_tensorHom,
      tensorHom_comp_tensorHom_assoc]
    simp [tensorHom_def, homEquiv_unit, homEquiv_counit]

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) X).inv = (ρ_ X).hom ≫ (λ_ X).inv

Tactic:
rw [Iso.inv_ext]
  rw [braiding_tensorUnit_left]
  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
D : Type u₂
inst✝⁸ : Category.{v₂, u₂} D
inst✝⁷ : MonoidalCategory D
inst✝⁶ : BraidedCategory D
E : Type u₃
inst✝⁵ : Category.{v₃, u₃} E
inst✝⁴ : MonoidalCategory E
inst✝³ : BraidedCategory E
F G : C ⥤ D
i : F ≅ G
inst✝² : F.LaxBraided
inst✝¹ : G.LaxMonoidal
inst✝ : NatTrans.IsMonoidal i.hom
X Y : C
⊢ μ G X Y ≫ G.map (β_ X Y).hom = (β_ (G.obj X) (G.obj Y)).hom ≫ μ G Y X

Tactic:
have (X Y : C) : μ G X Y = (i.inv.app X ⊗ₘ i.inv.app Y) ≫ μ F X Y ≫ i.hom.app _ := by
      simp [NatTrans.IsMonoidal.tensor X Y, tensorHom_comp_tensorHom_assoc]
    rw [this X Y, this Y X, ← braiding_naturality_assoc, ← Functor.LaxBraided.braided_assoc]
    simp

Goal state after:
Module: Mathlib.LinearAlgebra.TensorAlgebra.Basic

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : M →ₗ[R] A
⊢ Subalgebra.map ((lift R) f) (Algebra.adjoin R (Set.range ⇑(ι R))) = Algebra.adjoin R (Set.range ⇑f)

Tactic:
AlgHom.map_adjoin,

Goal state after:
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : M →ₗ[R] A
⊢ Algebra.adjoin R (⇑((lift R) f) '' Set.range ⇑(ι R)) = Algebra.adjoin R (Set.range ⇑f)
Module: Mathlib.Algebra.TrivSqZeroExt.Basic

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Module Rᵐᵒᵖ M
m₁ m₂ : M
⊢ 0 •> m₂ + m₁ <• 0 = 0

Tactic:
rw [zero_smul, zero_add, op_zero, zero_smul]

Goal state after:
Module: Mathlib.Algebra.TrivSqZeroExt.Basic

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Module Rᵐᵒᵖ M
x : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ x.1 •> 0 + 0 •> x.2 = 0

Tactic:
rw [smul_zero, zero_add, zero_smul]

Goal state after:
Module: Mathlib.Algebra.TrivSqZeroExt.Basic

Goal state before:
pp: R : Type u
M : Type v
inst✝⁴ : Monoid R
inst✝³ : AddMonoid M
inst✝² : DistribMulAction R M
inst✝¹ : DistribMulAction Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
n : ℕ
h : x.snd <• x.fst = x.fst •> x.snd
⊢ (List.map (fun i ↦ x.fst ^ (0 - i + i) •> x.snd) []).sum = 0

Tactic:
List.map_nil,

Goal state after:
R : Type u
M : Type v
inst✝⁴ : Monoid R
inst✝³ : AddMonoid M
inst✝² : DistribMulAction R M
inst✝¹ : DistribMulAction Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
n : ℕ
h : x.snd <• x.fst = x.fst •> x.snd
⊢ [].sum = 0
Module: Mathlib.RingTheory.Coalgebra.Basic

Goal state before:
pp: R : Type u
A : Type v
ι : Type u_1
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid A
inst✝¹ : Module R A
inst✝ : Coalgebra R A
a : A
𝓡 : Repr R a ι
⊢ ∑ x ∈ 𝓡.index, counit (𝓡.left x) • 𝓡.right x = a

Tactic:
by
  simpa only [map_sum, TensorProduct.lift.tmul, LinearMap.lsmul_apply, one_smul]
    using congr(TensorProduct.lift (LinearMap.lsmul R A) $(sum_counit_tmul_eq (R := R) 𝓡))

Goal state after:
Module: Mathlib.Algebra.TrivSqZeroExt.Basic

Goal state before:
pp: R : Type u
M : Type v
inst✝⁴ : AddCommGroup M
inst✝³ : Semiring R
inst✝² : Module Rᵐᵒᵖ M
inst✝¹ : Module R M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
m : M
⊢ IsUnit (inr m) ↔ Subsingleton R

Tactic:
by
  simp_rw [isUnit_iff_isUnit_fst, fst_inr, isUnit_zero_iff, subsingleton_iff_zero_eq_one]

Goal state after:
Module: Mathlib.Algebra.TrivSqZeroExt.Basic

Goal state before:
pp: S : Type u_1
R R' : Type u
M : Type v
inst✝¹⁶ : CommSemiring S
inst✝¹⁵ : Semiring R
inst✝¹⁴ : CommSemiring R'
inst✝¹³ : AddCommMonoid M
inst✝¹² : Algebra S R
inst✝¹¹ : Module S M
inst✝¹⁰ : Module R M
inst✝⁹ : Module Rᵐᵒᵖ M
inst✝⁸ : SMulCommClass R Rᵐᵒᵖ M
inst✝⁷ : IsScalarTower S R M
inst✝⁶ : IsScalarTower S Rᵐᵒᵖ M
inst✝⁵ : Module R' M
inst✝⁴ : Module R'ᵐᵒᵖ M
inst✝³ : IsCentralScalar R' M
A : Type u_2
inst✝² : Semiring A
inst✝¹ : Algebra S A
inst✝ : Algebra R' A
f : R →ₐ[S] A
g : M →ₗ[S] A
hg : ∀ (x y : M), g x * g y = 0
hfg : ∀ (r : R) (x : M), g (r •> x) = f r * g x
hgf : ∀ (r : R) (x : M), g (x <• r) = g x * f r
r₁ : R
m₁ : M
r₂ : R
m₂ : M
⊢ ((f.comp (fstHom S R M)).toLinearMap + g ∘ₗ ↑S (sndHom R M)) ((inl r₁ + inr m₁) * (inl r₂ + inr m₂)) =
    ((f.comp (fstHom S R M)).toLinearMap + g ∘ₗ ↑S (sndHom R M)) (inl r₁ + inr m₁) *
      ((f.comp (fstHom S R M)).toLinearMap + g ∘ₗ ↑S (sndHom R M)) (inl r₂ + inr m₂)

Tactic:
dsimp
        simp only [add_zero, zero_add, add_mul, mul_add, hg]
        rw [← map_mul, map_add, add_comm (g _), add_assoc, hfg, hgf]

Goal state after:
Module: Mathlib.Algebra.TrivSqZeroExt.Basic

Goal state before:
pp: S : Type u_1
R : Type u
M : Type v
inst✝¹¹ : CommSemiring S
inst✝¹⁰ : Semiring R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Algebra S R
inst✝⁷ : Module S M
inst✝⁶ : Module R M
inst✝⁵ : Module Rᵐᵒᵖ M
inst✝⁴ : SMulCommClass R Rᵐᵒᵖ M
inst✝³ : IsScalarTower S R M
inst✝² : IsScalarTower S Rᵐᵒᵖ M
A : Type u_2
inst✝¹ : Semiring A
inst✝ : Algebra S A
f : R →ₐ[S] A
g : M →ₗ[S] A
hg : ∀ (x y : M), g x * g y = 0
hfg : ∀ (r : R) (x : M), g (r •> x) = f r * g x
hgf : ∀ (r : R) (x : M), g (x <• r) = g x * f r
⊢ Subalgebra.map (lift f g hg hfg hgf) (inlAlgHom S R M).range ⊔
      Subalgebra.map (lift f g hg hfg hgf) (Algebra.adjoin S (Set.range inr)) =
    Subalgebra.map f ⊤ ⊔ Algebra.adjoin S (Set.range ⇑g)

Tactic:
AlgHom.map_adjoin,

Goal state after:
S : Type u_1
R : Type u
M : Type v
inst✝¹¹ : CommSemiring S
inst✝¹⁰ : Semiring R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Algebra S R
inst✝⁷ : Module S M
inst✝⁶ : Module R M
inst✝⁵ : Module Rᵐᵒᵖ M
inst✝⁴ : SMulCommClass R Rᵐᵒᵖ M
inst✝³ : IsScalarTower S R M
inst✝² : IsScalarTower S Rᵐᵒᵖ M
A : Type u_2
inst✝¹ : Semiring A
inst✝ : Algebra S A
f : R →ₐ[S] A
g : M →ₗ[S] A
hg : ∀ (x y : M), g x * g y = 0
hfg : ∀ (r : R) (x : M), g (r •> x) = f r * g x
hgf : ∀ (r : R) (x : M), g (x <• r) = g x * f r
⊢ Subalgebra.map (lift f g hg hfg hgf) (inlAlgHom S R M).range ⊔
      Algebra.adjoin S (⇑(lift f g hg hfg hgf) '' Set.range inr) =
    Subalgebra.map f ⊤ ⊔ Algebra.adjoin S (Set.range ⇑g)
Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

Goal state before:
pp: R : Type u₁
S : Type u₂
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
X✝ Y✝ : ModuleCat S
x✝ : X✝ ⟶ Y✝
h : Mono x✝
⊢ Mono ((restrictScalars f).map x✝)

Tactic:
mono_iff_injective

Goal state after:
R : Type u₁
S : Type u₂
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
X✝ Y✝ : ModuleCat S
x✝ : X✝ ⟶ Y✝
h : Function.Injective ⇑(ConcreteCategory.hom x✝)
⊢ Function.Injective ⇑(ConcreteCategory.hom ((restrictScalars f).map x✝))
Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

Goal state before:
pp: case refine_1.refine_2
R✝ : Type u₁
S✝ : Type u₂
inst✝³ : CommRing R✝
inst✝² : CommRing S✝
f✝ : R✝ →+* S✝
R : Type u₁
S : Type u₂
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
X : ModuleCat R
Y : ModuleCat S
g : X ⟶ (restrictScalars f).obj Y
m1 : Module R S := Module.compHom S f
m2 : Module R ↑Y := Module.compHom (↑Y) f
z : ↑((restrictScalars f).obj (of S S)) ⊗[R] ↑X
r : R
s : S
x : ↑X
⊢ (evalAt f (r • s) g) x = ((RingHom.id R) r • evalAt f s g) x

Tactic:
apply mul_smul (f r) s (g x)

Goal state after:
Module: Mathlib.Algebra.Ring.BooleanRing

Goal state before:
pp: α : Type u_1
inst✝ : BooleanRing α
a : α
⊢ -a + -a + a = a

Tactic:
by rw [add_self, zero_add]

Goal state after:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity

Goal state before:
pp: case a
R : Type u_2
inst✝³ : CommMonoidWithZero R
inst✝² : UniqueFactorizationMonoid R
inst✝¹ : NormalizationMonoid R
inst✝ : DecidableEq R
a b : R
ha : Irreducible a
hb : b ≠ 0
⊢ ¬↑(count (normalize a) (normalizedFactors b) + 1) ≤ emultiplicity a b

Tactic:
le_emultiplicity_iff_replicate_le_normalizedFactors ha hb,

Goal state after:
case a
R : Type u_2
inst✝³ : CommMonoidWithZero R
inst✝² : UniqueFactorizationMonoid R
inst✝¹ : NormalizationMonoid R
inst✝ : DecidableEq R
a b : R
ha : Irreducible a
hb : b ≠ 0
⊢ ¬replicate (count (normalize a) (normalizedFactors b) + 1) (normalize a) ≤ normalizedFactors b
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity

Goal state before:
pp: case a
R : Type u_2
inst✝³ : CommMonoidWithZero R
inst✝² : UniqueFactorizationMonoid R
inst✝¹ : NormalizationMonoid R
inst✝ : DecidableEq R
a b : R
ha : Irreducible a
hb : b ≠ 0
⊢ ↑(count (normalize a) (normalizedFactors b)) ≤ emultiplicity a b

Tactic:
le_emultiplicity_iff_replicate_le_normalizedFactors ha hb,

Goal state after:
case a
R : Type u_2
inst✝³ : CommMonoidWithZero R
inst✝² : UniqueFactorizationMonoid R
inst✝¹ : NormalizationMonoid R
inst✝ : DecidableEq R
a b : R
ha : Irreducible a
hb : b ≠ 0
⊢ replicate (count (normalize a) (normalizedFactors b)) (normalize a) ≤ normalizedFactors b