mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Bialgebra.Convolution

Goal state before:
pp: case ha
R : Type u_1
A : Type u_2
C : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring A
inst✝² : Semiring C
inst✝¹ : Bialgebra R C
inst✝ : Algebra R A
f g : WithConv (C →ₐ[R] A)
c x✝ : C
⊢ (((lmul' R).comp (Algebra.TensorProduct.map f.ofConv g.ofConv)).comp includeLeft) x✝ =
    ((Algebra.TensorProduct.lift f.ofConv g.ofConv ⋯).comp includeLeft) x✝

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Bialgebra.Convolution

Goal state before:
pp: case hb
R : Type u_1
A : Type u_2
C : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring A
inst✝² : Semiring C
inst✝¹ : Bialgebra R C
inst✝ : Algebra R A
f g : WithConv (C →ₐ[R] A)
c x✝ : C
⊢ ((restrictScalars R ((lmul' R).comp (Algebra.TensorProduct.map f.ofConv g.ofConv))).comp includeRight) x✝ =
    ((restrictScalars R (Algebra.TensorProduct.lift f.ofConv g.ofConv ⋯)).comp includeRight) x✝

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Bialgebra.Convolution

Goal state before:
pp: R : Type u_1
A : Type u_2
C : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring A
inst✝² : Semiring C
inst✝¹ : Bialgebra R C
inst✝ : Algebra R A
f : WithConv (C →ₐ[R] A)
n : ℕ
⊢ toConv (f ^ (n + 1)).ofConv.toLinearMap = toConv f.ofConv.toLinearMap ^ (n + 1)

Tactic:
by simp only [convPow_succ, toLinearMap_convMul, toLinearMap_convPow, pow_succ]

Goal state after:
Module: Mathlib.Algebra.Category.CommAlgCat.Monoidal

Goal state before:
pp: R : Type u
inst✝ : CommRing R
A B C D : CommAlgCat R
S T : (CommAlgCat R)ᵒᵖ
x : ↑(unop (op ((pair (unop S) (unop T)).obj { as := WalkingPair.right })))
⊢ 1 ⊗ₜ[R] x = (algebraMap R ↑(unop S)) 1 ⊗ₜ[R] x

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : CartesianMonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : CartesianMonoidalCategory D
F : C ⥤ D
X Y Z : C
inst✝ : F.Monoidal
f : X ⟶ Y
g : X ⟶ Z
⊢ (lift (F.map f) (F.map g) ≫ μ F Y Z) ≫ (μIso F Y Z).inv = F.map (lift f g) ≫ (μIso F Y Z).inv

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : CartesianMonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : CartesianMonoidalCategory D
F : C ⥤ D
inst✝ : F.Monoidal
X Y : C
⊢ (μIso F X Y).inv ≫ μ F X Y ≫ F.map (fst X Y) = (μIso F X Y).inv ≫ fst (F.obj X) (F.obj Y)

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : CartesianMonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : CartesianMonoidalCategory D
F : C ⥤ D
inst✝ : F.Monoidal
X Y : C
⊢ (μIso F X Y).inv ≫ μ F X Y ≫ F.map (snd X Y) = (μIso F X Y).inv ≫ snd (F.obj X) (F.obj Y)

Tactic:
simp

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

Goal state before:
pp: case h_fst
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : CartesianMonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : CartesianMonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : CartesianMonoidalCategory E
F✝ : C ⥤ D
G✝ : D ⥤ E
X✝ Y✝ Z : C
F G : C ⥤ D
inst✝¹ : F.Monoidal
inst✝ : G.Monoidal
α : F ⟶ G
X Y : C
⊢ ((Functor.Monoidal.μIso F X Y).inv ≫ (μ F X Y ≫ α.app (X ⊗ Y)) ≫ (Functor.Monoidal.μIso G X Y).inv) ≫
      fst (G.obj X) (G.obj Y) =
    ((Functor.Monoidal.μIso F X Y).inv ≫ ((α.app X ⊗ₘ α.app Y) ≫ μ G X Y) ≫ (Functor.Monoidal.μIso G X Y).inv) ≫
      fst (G.obj X) (G.obj Y)

Tactic:
simp

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

Goal state before:
pp: case h_snd
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : CartesianMonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : CartesianMonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : CartesianMonoidalCategory E
F✝ : C ⥤ D
G✝ : D ⥤ E
X✝ Y✝ Z : C
F G : C ⥤ D
inst✝¹ : F.Monoidal
inst✝ : G.Monoidal
α : F ⟶ G
X Y : C
⊢ ((Functor.Monoidal.μIso F X Y).inv ≫ (μ F X Y ≫ α.app (X ⊗ Y)) ≫ (Functor.Monoidal.μIso G X Y).inv) ≫
      snd (G.obj X) (G.obj Y) =
    ((Functor.Monoidal.μIso F X Y).inv ≫ ((α.app X ⊗ₘ α.app Y) ≫ μ G X Y) ≫ (Functor.Monoidal.μIso G X Y).inv) ≫
      snd (G.obj X) (G.obj Y)

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.HopfAlgebra.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
⊢ (LinearMap.mul' R R ∘ₗ LinearMap.rTensor R LinearMap.id ∘ₗ CoalgebraStruct.comul) 1 =
    (Algebra.linearMap R R ∘ₗ CoalgebraStruct.counit) 1

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.HopfAlgebra.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
⊢ (LinearMap.mul' R R ∘ₗ LinearMap.lTensor R LinearMap.id ∘ₗ CoalgebraStruct.comul) 1 =
    (Algebra.linearMap R R ∘ₗ CoalgebraStruct.counit) 1

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.HopfAlgebra.TensorProduct

Goal state before:
pp: case e'_2.tmul.tmul
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Semiring A
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R S
inst✝³ : HopfAlgebra R A
inst✝² : HopfAlgebra S B
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R S B
x : B
y : A
x₁ x₂ : B
y₁ y₂ : A
⊢ (LinearMap.mul' S (B ⊗[R] A))
      ((LinearMap.rTensor (B ⊗[R] A) (AlgebraTensorModule.map (antipode S) (antipode R)))
        ((AlgebraTensorModule.tensorTensorTensorComm R S R S B B A A) (x₁ ⊗ₜ[S] x₂ ⊗ₜ[R] (y₁ ⊗ₜ[R] y₂)))) =
    (LinearMap.mul' S B) ((LinearMap.rTensor B (antipode S)) (x₁ ⊗ₜ[S] x₂)) ⊗ₜ[R]
      (LinearMap.mul' R A) ((LinearMap.rTensor A (antipode R)) (y₁ ⊗ₜ[R] y₂))

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.HopfAlgebra.TensorProduct

Goal state before:
pp: case e'_2.tmul.tmul
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Semiring A
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R S
inst✝³ : HopfAlgebra R A
inst✝² : HopfAlgebra S B
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R S B
x : B
y : A
x₁ x₂ : B
y₁ y₂ : A
⊢ (LinearMap.mul' S (B ⊗[R] A))
      ((LinearMap.lTensor (B ⊗[R] A) (AlgebraTensorModule.map (antipode S) (antipode R)))
        ((AlgebraTensorModule.tensorTensorTensorComm R S R S B B A A) (x₁ ⊗ₜ[S] x₂ ⊗ₜ[R] (y₁ ⊗ₜ[R] y₂)))) =
    (LinearMap.mul' S B) ((LinearMap.lTensor B (antipode S)) (x₁ ⊗ₜ[S] x₂)) ⊗ₜ[R]
      (LinearMap.mul' R A) ((LinearMap.lTensor A (antipode R)) (y₁ ⊗ₜ[R] y₂))

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : CartesianMonoidalCategory C
G X : C
inst✝¹ : GrpObj G
A✝ B A : C
inst✝ : GrpObj A
⊢ ι ≫ ι = 𝟙 A

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : CartesianMonoidalCategory C
A : C
inst✝ : GrpObj A
⊢ (mulRight η).hom = (Iso.refl A).hom

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : CartesianMonoidalCategory C
A : C
inst✝ : GrpObj A
⊢ μ ▷ A ≫ μ = ((α_ A A A).hom ≫ A ◁ μ) ≫ μ

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : CartesianMonoidalCategory C
A : C
inst✝ : GrpObj A
s : PullbackCone μ μ
⊢ (lift (lift (s.snd ≫ fst A A) (lift (s.snd ≫ fst A A ≫ ι) (s.fst ≫ fst A A) ≫ μ)) (s.fst ≫ snd A A) ≫ μ ▷ A) ≫
      snd A A =
    s.fst ≫ snd A A

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : CartesianMonoidalCategory C
A : C
inst✝ : GrpObj A
s : PullbackCone μ μ
⊢ (lift (lift (s.snd ≫ fst A A) (lift (s.snd ≫ fst A A ≫ ι) (s.fst ≫ fst A A) ≫ μ)) (s.fst ≫ snd A A) ≫
        (α_ A A A).hom ≫ A ◁ μ) ≫
      fst A A =
    s.snd ≫ fst A A

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.HopfAlgebra.Convolution

Goal state before:
pp: R : Type u_1
A : Type u_2
C : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : HopfAlgebra R A
⊢ MulOpposite.op ((↑(MulOpposite.opLinearEquiv R) ∘ₗ antipode R) 1) = MulOpposite.op 1

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.HopfAlgebra.Convolution

Goal state before:
pp: R : Type u_1
C : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring C
inst✝ : HopfAlgebra R C
x✝¹ x✝ : C
⊢ ((AlgebraTensorModule.curry (mul' R (C ⊗[R] C) ∘ₗ (δ ⊗ₘ δ))) x✝¹) x✝ =
    ((AlgebraTensorModule.curry (δ ∘ₗ mul' R C)) x✝¹) x✝

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.HopfAlgebra.Convolution

Goal state before:
pp: R : Type u_1
C : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring C
inst✝ : HopfAlgebra R C
⊢ (δ ∘ₗ Algebra.linearMap R C) 1 = (Algebra.linearMap R (C ⊗[R] C)) 1

Tactic:
simp

Goal state after:
R : Type u_1
C : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring C
inst✝ : HopfAlgebra R C
⊢ 1 = 1 ⊗ₜ[R] 1
Module: Mathlib.RingTheory.HopfAlgebra.Convolution

Goal state before:
pp: case ha
R : Type u_1
A : Type u_2
C : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring A
inst✝² : CommSemiring C
inst✝¹ : Bialgebra R C
inst✝ : HopfAlgebra R A
f : WithConv (A →ₐ[R] C)
x✝ : A
⊢ (((lmul' R).comp (Algebra.TensorProduct.map f.ofConv f.ofConv)).comp includeLeft) x✝ =
    ((f.ofConv.comp (lmul' R)).comp includeLeft) x✝

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.HopfAlgebra.Convolution

Goal state before:
pp: case hb
R : Type u_1
A : Type u_2
C : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring A
inst✝² : CommSemiring C
inst✝¹ : Bialgebra R C
inst✝ : HopfAlgebra R A
f : WithConv (A →ₐ[R] C)
x✝ : A
⊢ ((restrictScalars R ((lmul' R).comp (Algebra.TensorProduct.map f.ofConv f.ofConv))).comp includeRight) x✝ =
    ((restrictScalars R (f.ofConv.comp (lmul' R))).comp includeRight) x✝

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.HopfAlgebra.Convolution

Goal state before:
pp: R : Type u_1
A : Type u_2
C : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring A
inst✝² : CommSemiring C
inst✝¹ : Bialgebra R C
inst✝ : HopfAlgebra R A
f : WithConv (A →ₐ[R] C)
H : (lmul' R).comp (Algebra.TensorProduct.map f.ofConv f.ofConv) = f.ofConv.comp (lmul' R)
x✝ : A
⊢ (f.ofConv.toLinearMap ∘ₗ ofConv 1) x✝ = (ofConv 1) x✝

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.HopfAlgebra.Convolution

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : HopfAlgebra R A
⊢ ((counitAlgHom R A).comp (antipodeAlgHom R A)).toLinearMap = (counitAlgHom R A).toLinearMap

Tactic:
simp

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

Goal state before:
pp: case refine_1
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : CartesianMonoidalCategory C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : CartesianMonoidalCategory D
F : C ⥤ D
inst✝² : F.Monoidal
inst✝¹ : F.Full
inst✝ : F.Faithful
G : Grp D
H : C
e : F.obj H ≅ G.X
this✝ : GrpObj (F.obj H) := GrpObj.ofIso e.symm
this : GrpObj H := (FullyFaithful.ofFullyFaithful F).grpObj H
⊢ η ≫ e.hom = η

Tactic:
simp

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

Goal state before:
pp: case refine_2
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : CartesianMonoidalCategory C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : CartesianMonoidalCategory D
F : C ⥤ D
inst✝² : F.Monoidal
inst✝¹ : F.Full
inst✝ : F.Faithful
G : Grp D
H : C
e : F.obj H ≅ G.X
this✝ : GrpObj (F.obj H) := GrpObj.ofIso e.symm
this : GrpObj H := (FullyFaithful.ofFullyFaithful F).grpObj H
⊢ μ ≫ e.hom = (e.hom ⊗ₘ e.hom) ≫ μ

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : MonoidalCategory C
W X Y Z : C
inst✝¹ : Closed W
inst✝ : Closed X
f : W ⟶ X
g : Y ⟶ Z
⊢ (pre f).app Y ≫ (ihom W).map g = (ihom X).map g ≫ (pre f).app Z

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
x y : C
inst✝ : Closed x
⊢ x ◁ (λ_ ((ihom x).obj y)).inv ≫ x ◁ id x ▷ (ihom x).obj y ≫ uncurry (comp x x y) = uncurry (𝟙 ((ihom x).obj y))

Tactic:
comp_eq,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
x y : C
inst✝ : Closed x
⊢ x ◁ (λ_ ((ihom x).obj y)).inv ≫ x ◁ id x ▷ (ihom x).obj y ≫ uncurry (curry (compTranspose x x y)) =
    uncurry (𝟙 ((ihom x).obj y))
Module: Mathlib.CategoryTheory.Monoidal.Closed.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : MonoidalCategory C
x y : C
inst✝¹ : Closed x
inst✝ : Closed y
⊢ x ◁ (ρ_ ((ihom x).obj y)).inv ≫ x ◁ (ihom x).obj y ◁ id y ≫ uncurry (comp x y y) = uncurry (𝟙 ((ihom x).obj y))

Tactic:
comp_eq,

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : MonoidalCategory C
x y : C
inst✝¹ : Closed x
inst✝ : Closed y
⊢ x ◁ (ρ_ ((ihom x).obj y)).inv ≫ x ◁ (ihom x).obj y ◁ id y ≫ uncurry (curry (compTranspose x y y)) =
    uncurry (𝟙 ((ihom x).obj y))
Module: Mathlib.CategoryTheory.Monoidal.Closed.Basic

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : MonoidalCategory C
w x y z : C
inst✝² : Closed w
inst✝¹ : Closed x
inst✝ : Closed y
⊢ w ◁ (α_ ((ihom w).obj x) ((ihom x).obj y) ((ihom y).obj z)).inv ≫
      (α_ w ((ihom w).obj x ⊗ (ihom x).obj y) ((ihom y).obj z)).inv ≫
        ((α_ w ((ihom w).obj x) ((ihom x).obj y)).inv ≫ (ihom.ev w).app x ▷ (ihom x).obj y ≫ (ihom.ev x).app y) ▷
            (ihom y).obj z ≫
          (ihom.ev y).app z =
    (α_ w ((ihom w).obj x) ((ihom x).obj y ⊗ (ihom y).obj z)).inv ≫
      (ihom.ev w).app x ▷ ((ihom x).obj y ⊗ (ihom y).obj z) ≫
        (α_ x ((ihom x).obj y) ((ihom y).obj z)).inv ≫ (ihom.ev x).app y ▷ (ihom y).obj z ≫ (ihom.ev y).app z

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : MonoidalCategory C
A B X✝ X' Y✝ Y' Z : C
inst✝¹ : Closed A
X Y : C
inst✝ : Closed X
x✝ : X ⟶ Y
⊢ uncurry' (curry' x✝) = x✝

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : MonoidalCategory C
A B X✝ X' Y✝ Y' Z : C
inst✝¹ : Closed A
X Y : C
inst✝ : Closed X
x✝ : 𝟙_ C ⟶ (ihom X).obj Y
⊢ curry' (uncurry' x✝) = x✝

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : MonoidalCategory C
X Y Z : C
inst✝¹ : Closed X
inst✝ : Closed Y
f : X ⟶ Y
⊢ uncurry ((λ_ ((ihom Y).obj Z)).inv ≫ curry' f ▷ (ihom Y).obj Z ≫ comp X Y Z) = f ▷ (ihom Y).obj Z ≫ (ihom.ev Y).app Z

Tactic:
comp_eq,

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : MonoidalCategory C
X Y Z : C
inst✝¹ : Closed X
inst✝ : Closed Y
f : X ⟶ Y
⊢ uncurry ((λ_ ((ihom Y).obj Z)).inv ≫ curry' f ▷ (ihom Y).obj Z ≫ curry (compTranspose X Y Z)) =
    f ▷ (ihom Y).obj Z ≫ (ihom.ev Y).app Z
Module: Mathlib.CategoryTheory.Monoidal.Closed.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : MonoidalCategory C
X Y Z : C
inst✝¹ : Closed X
inst✝ : Closed Y
f : Y ⟶ Z
⊢ uncurry ((ρ_ ((ihom X).obj Y)).inv ≫ (ihom X).obj Y ◁ curry' f ≫ comp X Y Z) = (ihom.ev X).app Y ≫ f

Tactic:
comp_eq,

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : MonoidalCategory C
X Y Z : C
inst✝¹ : Closed X
inst✝ : Closed Y
f : Y ⟶ Z
⊢ uncurry ((ρ_ ((ihom X).obj Y)).inv ≫ (ihom X).obj Y ◁ curry' f ≫ curry (compTranspose X Y Z)) = (ihom.ev X).app Y ≫ f
Module: Mathlib.Data.W.Cardinal

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : ∀ (a : α), Finite (β a)
x✝ : IsEmpty α
⊢ #(WType β) ≤ max (lift.{v, u} #α) ℵ₀

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.Dual.Basis

Goal state before:
pp: R : Type uR
M : Type uM
ι : Type uι
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq ι
b : Basis ι R M
inst✝ : Finite ι
f : Dual R M
i : ι
⊢ (b.toDual ((Finsupp.linearCombination R ⇑b) (Finsupp.equivFunOnFinite.symm fun i ↦ f (b i)))) (b i) = f (b i)

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.Dual.Basis

Goal state before:
pp: case h₁
R : Type u_1
M : Type u_2
ι : Type u_3
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
e : ι → M
ε : ι → Dual R M
h : DualBases e ε
l : ι →₀ R
i : ι
⊢ l i = 0 → (ε i) (0 • e i) = 0

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.Dual.Basis

Goal state before:
pp: R : Type u_1
M : Type u_2
ι : Type u_3
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
e : ι → M
ε : ι → Dual R M
h : DualBases e ε
H : Set ι
x : M
hmem : x ∈ span R (e '' H)
⊢ ∀ (i : ι), (ε i) x ≠ 0 → i ∈ H

Tactic:
by
  intro i hi
  rcases (Finsupp.mem_span_image_iff_linearCombination _).mp hmem with ⟨l, supp_l, rfl⟩
  apply not_imp_comm.mp ((Finsupp.mem_supported' _ _).mp supp_l i)
  rwa [← lc_def, h.dual_lc] at hi

Goal state after:
Module: Mathlib.LinearAlgebra.Dual.Basis

Goal state before:
pp: R : Type u_1
M : Type u_2
ι : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
e : ι → M
ε : ι → Dual R M
h : DualBases e ε
inst✝¹ : DecidableEq ι
inst✝ : Finite ι
i j : ι
⊢ (h.basis.dualBasis i) (h.basis j) = (ε i) (h.basis j)

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Category.CommHopfAlgCat

Goal state before:
pp: R : Type u
inst✝ : CommRing R
A : CommHopfAlgCat R
a : ↑A
⊢ (ConcreteCategory.hom (𝟙 A)) a = a

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Category.CommHopfAlgCat

Goal state before:
pp: R : Type u
inst✝ : CommRing R
A B C : CommHopfAlgCat R
f : A ⟶ B
g : B ⟶ C
a : ↑A
⊢ (ConcreteCategory.hom (f ≫ g)) a = (ConcreteCategory.hom g) ((ConcreteCategory.hom f) a)

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Category.CommHopfAlgCat

Goal state before:
pp: R : Type u
inst✝ : CommRing R
A B : CommHopfAlgCat R
e : A ≅ B
x : ↑A
⊢ (ConcreteCategory.hom e.inv) ((ConcreteCategory.hom e.hom) x) = x

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Category.CommHopfAlgCat

Goal state before:
pp: R : Type u
inst✝ : CommRing R
A B : CommHopfAlgCat R
e : A ≅ B
x : ↑B
⊢ (ConcreteCategory.hom e.hom) ((ConcreteCategory.hom e.inv) x) = x

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Category.CommHopfAlgCat

Goal state before:
pp: R : Type u
inst✝⁶ : CommRing R
A B C : CommHopfAlgCat R
X Y Z : Type v
inst✝⁵ : CommRing X
inst✝⁴ : HopfAlgebra R X
inst✝³ : CommRing Y
inst✝² : HopfAlgebra R Y
inst✝¹ : CommRing Z
inst✝ : HopfAlgebra R Z
i : A ≅ B
x : ↑A
⊢ (ConcreteCategory.hom i.inv) ((ConcreteCategory.hom i.hom) x) = x

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Category.CommHopfAlgCat

Goal state before:
pp: R : Type u
inst✝⁶ : CommRing R
A B C : CommHopfAlgCat R
X Y Z : Type v
inst✝⁵ : CommRing X
inst✝⁴ : HopfAlgebra R X
inst✝³ : CommRing Y
inst✝² : HopfAlgebra R Y
inst✝¹ : CommRing Z
inst✝ : HopfAlgebra R Z
i : A ≅ B
x : ↑B
⊢ (ConcreteCategory.hom i.hom) ((ConcreteCategory.hom i.inv) x) = x

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.Dimension.RankNullity

Goal state before:
pp: R : Type u_1
M : Type u
M' : Type v
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup M'
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : HasRankNullity.{v, u_1} R
f : M →ₗ[R] M'
p : Submodule R M
f' : M ⧸ p →ₗ[R] ↥f.range ⧸ Submodule.map f.rangeRestrict p :=
  p.mapQ (Submodule.map f.rangeRestrict p) f.rangeRestrict ⋯
⊢ Submodule.map (Submodule.map f.rangeRestrict p).mkQ f.rangeRestrict.range = ⊤

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.Dimension.RankNullity

Goal state before:
pp: R : Type u_1
M : Type u
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : HasRankNullity.{u, u_1} R
inst✝² : IsDomain R
inst✝¹ : StrongRankCondition R
inst✝ : IsTorsionFree R M
h : 1 < Module.rank R M
x : M
hx : x ≠ 0
y : M
hy : LinearIndependent R (Fin.snoc ![x] y)
⊢ Fin.snoc ![x] y = ![x, y]

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.Dimension.RankNullity

Goal state before:
pp: R : Type u_1
M : Type u
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : HasRankNullity.{u, u_1} R
s t : Submodule R M
⊢ t = (s ⊔ t) ⊓ t

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.InvariantBasisNumber

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
n m : ℕ
f : Matrix (Fin m) (Fin n) R
g : Matrix (Fin n) (Fin m) R
⊢ opEquiv.mapMatrix.symm (opEquiv.mapMatrix f * opEquiv.mapMatrix g) = opEquiv.mapMatrix.symm 1 → m ≤ n ↔
    (transposeAddEquiv (Fin n) (Fin m) R).toEquiv g * (transposeAddEquiv (Fin m) (Fin n) R).toEquiv f = 1 → m ≤ n

Tactic:
rw [← (transposeAddEquiv ..).injective.eq_iff]

Goal state after:
R : Type u_1
inst✝ : Semiring R
n m : ℕ
f : Matrix (Fin m) (Fin n) R
g : Matrix (Fin n) (Fin m) R
⊢ (transposeAddEquiv (Fin m) (Fin m) R) (opEquiv.mapMatrix.symm (opEquiv.mapMatrix f * opEquiv.mapMatrix g)) =
        (transposeAddEquiv (Fin m) (Fin m) R) (opEquiv.mapMatrix.symm 1) →
      m ≤ n ↔
    (transposeAddEquiv (Fin n) (Fin m) R).toEquiv g * (transposeAddEquiv (Fin m) (Fin n) R).toEquiv f = 1 → m ≤ n
Module: Mathlib.LinearAlgebra.Matrix.InvariantBasisNumber

Goal state before:
pp: case refine_2
R : Type u_1
inst✝ : Semiring R
n m : ℕ
f : Matrix (Fin m) (Fin n) R
g : Matrix (Fin n) (Fin m) R
⊢ (transposeAddEquiv (Fin m) (Fin m) R) (opEquiv.mapMatrix.symm 1) = 1

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.InvariantBasisNumber

Goal state before:
pp: case refine_2
R : Type u_1
inst✝ : Semiring R
n m : ℕ
f : Matrix (Fin m) (Fin n) R
g : Matrix (Fin n) (Fin m) R
⊢ (transposeAddEquiv (Fin n) (Fin n) R) (opEquiv.mapMatrix.symm 1) = 1

pp: case refine_3
R : Type u_1
inst✝ : Semiring R
n m : ℕ
f : Matrix (Fin m) (Fin n) R
g : Matrix (Fin n) (Fin m) R
⊢ (transposeAddEquiv (Fin m) (Fin m) R) (opEquiv.mapMatrix.symm (opEquiv.mapMatrix f * opEquiv.mapMatrix g)) =
    (transposeAddEquiv (Fin n) (Fin m) R).toEquiv g * (transposeAddEquiv (Fin m) (Fin n) R).toEquiv f

pp: case refine_4
R : Type u_1
inst✝ : Semiring R
n m : ℕ
f : Matrix (Fin m) (Fin n) R
g : Matrix (Fin n) (Fin m) R
⊢ (transposeAddEquiv (Fin m) (Fin m) R) (opEquiv.mapMatrix.symm 1) = 1

Tactic:
simp

Goal state after:
case refine_3
R : Type u_1
inst✝ : Semiring R
n m : ℕ
f : Matrix (Fin m) (Fin n) R
g : Matrix (Fin n) (Fin m) R
⊢ (transposeAddEquiv (Fin m) (Fin m) R) (opEquiv.mapMatrix.symm (opEquiv.mapMatrix f * opEquiv.mapMatrix g)) =
    (transposeAddEquiv (Fin n) (Fin m) R).toEquiv g * (transposeAddEquiv (Fin m) (Fin n) R).toEquiv f

case refine_4
R : Type u_1
inst✝ : Semiring R
n m : ℕ
f : Matrix (Fin m) (Fin n) R
g : Matrix (Fin n) (Fin m) R
⊢ (transposeAddEquiv (Fin m) (Fin m) R) (opEquiv.mapMatrix.symm 1) = 1
Module: Mathlib.LinearAlgebra.Matrix.InvariantBasisNumber

Goal state before:
pp: case refine_4
R : Type u_1
inst✝ : Semiring R
n m : ℕ
f : Matrix (Fin m) (Fin n) R
g : Matrix (Fin n) (Fin m) R
⊢ (transposeAddEquiv (Fin m) (Fin m) R) (opEquiv.mapMatrix.symm 1) = 1

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas

Goal state before:
pp: case refine_1.inl
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Module.Finite K V
W : Submodule K V
v : V
hv : v ∉ W
hW : W ⊔ K ∙ v = ⊤
hw : 0 • v ∈ W ⊓ K ∙ v
ht : 0 • v ∈ W
⊢ 0 • v = 0

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
X Y : C
inst✝¹ : HasRightDual X
inst✝ : HasRightDual Y
f : X ⟶ Y
⊢ Yᘁ ◁ (η_ X Xᘁ ≫ f ▷ Xᘁ) ≫ (α_ Yᘁ Y Xᘁ).inv ≫ ε_ Y Yᘁ ▷ Xᘁ ≫ (λ_ Xᘁ).hom =
    (ρ_ Yᘁ).hom ≫ (ρ_ Yᘁ).inv ≫ Yᘁ ◁ η_ X Xᘁ ≫ Yᘁ ◁ f ▷ Xᘁ ≫ (α_ Yᘁ Y Xᘁ).inv ≫ ε_ Y Yᘁ ▷ Xᘁ ≫ (λ_ Xᘁ).hom

Tactic:
simp

Goal state after: