awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Coalgebra.CoassocSimps
Goal:
R : Type u_1
M : Type u_3
P : Type u_5
M' : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid P
inst_4 : Module R P
inst_5 : AddCommMonoid M'
inst_6 : Module R M'
inst_7 : Coalgebra R M
f : M →ₗ[R] M'
g : P →ₗ[R] M
simp_rw : (f ⊗ₘ ε ∘ₗ δ) ∘ₗ g = (f ⊗ₘ LinearMap.id ∘ₗ ρ⁻¹) ∘ₗ g
⊢ f ⊗ₘ ε ∘ₗ δ ∘ₗ g = f ⊗ₘ LinearMap.id ∘ₗ ρ⁻¹ ∘ₗ g

Tactic:
simp_rw [← LinearMap.comp_assoc, map_counit_comp_comul_right]

Premises used: CoassocSimps.map_counit_comp_comul_right, LinearMap.comp_assoc
-- Module: Mathlib.RingTheory.Coalgebra.CoassocSimps
Goal:
R : Type u_1
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : Coalgebra R M
f : M →ₗ[R] N
rw :
  α ∘ₗ (β ⊗ₘ f ∘ₗ LinearMap.rTensor M δ) ∘ₗ δ =
    LinearMap.lTensor M (LinearMap.lTensor M (f ∘ₗ LinearMap.id) ∘ₗ β) ∘ₗ α ∘ₗ β ∘ₗ α ∘ₗ LinearMap.rTensor M δ ∘ₗ δ
⊢ α ∘ₗ (β ∘ₗ δ) ⊗ₘ f ∘ₗ δ = LinearMap.id ⊗ₘ (LinearMap.id ⊗ₘ f ∘ₗ β) ∘ₗ α ∘ₗ δ ⊗ₘ LinearMap.id ∘ₗ β ∘ₗ δ

Tactic:
rw [← symm_comp_map_assoc, ← LinearMap.lTensor_def, ← LinearMap.lTensor_def,
    ← LinearMap.lTensor_def, ← Coalgebra.coassoc, ← f.comp_id,
    TensorProduct.map_comp, ← LinearMap.rTensor_def]

Premises used: CoassocSimps.symm_comp_map_assoc, Coalgebra.coassoc, TensorProduct.map_comp, LinearMap.rTensor_def, LinearMap.comp_id, LinearMap.lTensor_def
-- Module: Mathlib.RingTheory.Coalgebra.CoassocSimps
Goal:
R : Type u_1
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : Coalgebra R M
f : M →ₗ[R] N
simp :
  ((α ∘ₗ β ⊗ₘ f) ∘ₗ LinearMap.rTensor M δ) ∘ₗ δ =
    ((((LinearMap.lTensor M (LinearMap.lTensor M (f ∘ₗ LinearMap.id) ∘ₗ β) ∘ₗ α) ∘ₗ β) ∘ₗ α) ∘ₗ
        LinearMap.rTensor M δ) ∘ₗ
      δ
⊢ α ∘ₗ (β ⊗ₘ f ∘ₗ LinearMap.rTensor M δ) ∘ₗ δ =
    LinearMap.lTensor M (LinearMap.lTensor M (f ∘ₗ LinearMap.id) ∘ₗ β) ∘ₗ α ∘ₗ β ∘ₗ α ∘ₗ LinearMap.rTensor M δ ∘ₗ δ

Tactic:
simp only [← LinearMap.comp_assoc]

Premises used: LinearMap.comp_assoc
-- Module: Mathlib.RingTheory.Coalgebra.CoassocSimps
Goal:
R : Type u_1
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : Coalgebra R M
f : M →ₗ[R] N
e_f :
  Eq («α» := M ⊗[R] M ⊗[R] M →ₗ[R] M ⊗[R] (M ⊗[R] N)) (α ∘ₗ β ⊗ₘ f)
    (((LinearMap.lTensor M (LinearMap.lTensor M (f ∘ₗ LinearMap.id) ∘ₗ β) ∘ₗ α) ∘ₗ β) ∘ₗ α)
⊢ ((α ∘ₗ β ⊗ₘ f) ∘ₗ LinearMap.rTensor M δ) ∘ₗ δ =
    ((((LinearMap.lTensor M (LinearMap.lTensor M (f ∘ₗ LinearMap.id) ∘ₗ β) ∘ₗ α) ∘ₗ β) ∘ₗ α) ∘ₗ
        LinearMap.rTensor M δ) ∘ₗ
      δ

Tactic:
congr 2
-- Module: Mathlib.RingTheory.Coalgebra.CoassocSimps
Goal:
R : Type u_1
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : Coalgebra R M
f : M →ₗ[R] N
e_f :
  ∀ (x x_1 x_2 : M),
    Eq («α» := M ⊗[R] (M ⊗[R] N))
      (((((((AlgebraTensorModule.curry (AlgebraTensorModule.curry (α ∘ₗ β ⊗ₘ f)) :
                          M →ₗ[R] M →ₗ[R] M →ₗ[R] M ⊗[R] (M ⊗[R] N)) :
                        (a : M) → M →ₗ[R] M →ₗ[R] M ⊗[R] (M ⊗[R] N))
                      x :
                    M →ₗ[R] M →ₗ[R] M ⊗[R] (M ⊗[R] N)) :
                  (a : M) → M →ₗ[R] M ⊗[R] (M ⊗[R] N))
                x_1 :
              M →ₗ[R] M ⊗[R] (M ⊗[R] N)) :
            (a : M) → M ⊗[R] (M ⊗[R] N))
          x_2 :
        M ⊗[R] (M ⊗[R] N))
      (((((((AlgebraTensorModule.curry
                            (AlgebraTensorModule.curry
                              (((LinearMap.lTensor M (LinearMap.lTensor M (f ∘ₗ LinearMap.id) ∘ₗ β) ∘ₗ α) ∘ₗ β) ∘ₗ α)) :
                          M →ₗ[R] M →ₗ[R] M →ₗ[R] M ⊗[R] (M ⊗[R] N)) :
                        (a : M) → M →ₗ[R] M →ₗ[R] M ⊗[R] (M ⊗[R] N))
                      x :
                    M →ₗ[R] M →ₗ[R] M ⊗[R] (M ⊗[R] N)) :
                  (a : M) → M →ₗ[R] M ⊗[R] (M ⊗[R] N))
                x_1 :
              M →ₗ[R] M ⊗[R] (M ⊗[R] N)) :
            (a : M) → M ⊗[R] (M ⊗[R] N))
          x_2 :
        M ⊗[R] (M ⊗[R] N))
⊢ Eq («α» := M ⊗[R] M ⊗[R] M →ₗ[R] M ⊗[R] (M ⊗[R] N)) (α ∘ₗ β ⊗ₘ f)
    (((LinearMap.lTensor M (LinearMap.lTensor M (f ∘ₗ LinearMap.id) ∘ₗ β) ∘ₗ α) ∘ₗ β) ∘ₗ α)

Tactic:
ext
-- Module: Mathlib.RingTheory.Coalgebra.CoassocSimps
Goal:
R : Type u_1
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : Coalgebra R M
f : M →ₗ[R] N
x x_1 x_2 : M
⊢ Eq («α» := M ⊗[R] (M ⊗[R] N))
    (((((((AlgebraTensorModule.curry (AlgebraTensorModule.curry (α ∘ₗ β ⊗ₘ f)) :
                        M →ₗ[R] M →ₗ[R] M →ₗ[R] M ⊗[R] (M ⊗[R] N)) :
                      (a : M) → M →ₗ[R] M →ₗ[R] M ⊗[R] (M ⊗[R] N))
                    x :
                  M →ₗ[R] M →ₗ[R] M ⊗[R] (M ⊗[R] N)) :
                (a : M) → M →ₗ[R] M ⊗[R] (M ⊗[R] N))
              x_1 :
            M →ₗ[R] M ⊗[R] (M ⊗[R] N)) :
          (a : M) → M ⊗[R] (M ⊗[R] N))
        x_2 :
      M ⊗[R] (M ⊗[R] N))
    (((((((AlgebraTensorModule.curry
                          (AlgebraTensorModule.curry
                            (((LinearMap.lTensor M (LinearMap.lTensor M (f ∘ₗ LinearMap.id) ∘ₗ β) ∘ₗ α) ∘ₗ β) ∘ₗ α)) :
                        M →ₗ[R] M →ₗ[R] M →ₗ[R] M ⊗[R] (M ⊗[R] N)) :
                      (a : M) → M →ₗ[R] M →ₗ[R] M ⊗[R] (M ⊗[R] N))
                    x :
                  M →ₗ[R] M →ₗ[R] M ⊗[R] (M ⊗[R] N)) :
                (a : M) → M →ₗ[R] M ⊗[R] (M ⊗[R] N))
              x_1 :
            M →ₗ[R] M ⊗[R] (M ⊗[R] N)) :
          (a : M) → M ⊗[R] (M ⊗[R] N))
        x_2 :
      M ⊗[R] (M ⊗[R] N))

Tactic:
rfl
-- Module: Mathlib.RingTheory.Coalgebra.CoassocSimps
Goal:
R : Type u_1
M : Type u_3
N : Type u_4
Q : Type u_9
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : AddCommMonoid Q
inst_6 : Module R Q
inst_7 : Coalgebra R M
f : M →ₗ[R] N
h : Q →ₗ[R] M
simp_rw :
  ((α ∘ₗ (β ∘ₗ δ) ⊗ₘ f) ∘ₗ δ) ∘ₗ h =
    ((((LinearMap.id ⊗ₘ (LinearMap.id ⊗ₘ f ∘ₗ β) ∘ₗ α) ∘ₗ δ ⊗ₘ LinearMap.id) ∘ₗ β) ∘ₗ δ) ∘ₗ h
⊢ α ∘ₗ (β ∘ₗ δ) ⊗ₘ f ∘ₗ δ ∘ₗ h = LinearMap.id ⊗ₘ (LinearMap.id ⊗ₘ f ∘ₗ β) ∘ₗ α ∘ₗ δ ⊗ₘ LinearMap.id ∘ₗ β ∘ₗ δ ∘ₗ h

Tactic:
simp_rw [← LinearMap.comp_assoc]

Premises used: LinearMap.comp_assoc
-- Module: Mathlib.RingTheory.Coalgebra.CoassocSimps
Goal:
R : Type u_1
M : Type u_3
N : Type u_4
Q : Type u_9
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : AddCommMonoid Q
inst_6 : Module R Q
inst_7 : Coalgebra R M
f : M →ₗ[R] N
h : Q →ₗ[R] M
e_f : (α ∘ₗ (β ∘ₗ δ) ⊗ₘ f) ∘ₗ δ = (((LinearMap.id ⊗ₘ (LinearMap.id ⊗ₘ f ∘ₗ β) ∘ₗ α) ∘ₗ δ ⊗ₘ LinearMap.id) ∘ₗ β) ∘ₗ δ
⊢ ((α ∘ₗ (β ∘ₗ δ) ⊗ₘ f) ∘ₗ δ) ∘ₗ h =
    ((((LinearMap.id ⊗ₘ (LinearMap.id ⊗ₘ f ∘ₗ β) ∘ₗ α) ∘ₗ δ ⊗ₘ LinearMap.id) ∘ₗ β) ∘ₗ δ) ∘ₗ h

Tactic:
congr 1
-- Module: Mathlib.RingTheory.Coalgebra.CoassocSimps
Goal:
R : Type u_1
M : Type u_3
N : Type u_4
Q : Type u_9
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : AddCommMonoid Q
inst_6 : Module R Q
inst_7 : Coalgebra R M
f : M →ₗ[R] N
h : Q →ₗ[R] M
⊢ (α ∘ₗ (β ∘ₗ δ) ⊗ₘ f) ∘ₗ δ = (((LinearMap.id ⊗ₘ (LinearMap.id ⊗ₘ f ∘ₗ β) ∘ₗ α) ∘ₗ δ ⊗ₘ LinearMap.id) ∘ₗ β) ∘ₗ δ

Tactic:
simp only [coassoc_simps]
-- Module: Mathlib.RingTheory.Coalgebra.Convolution
Goal:
R : Type u_1
A : Type u_2
C : Type u_4
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : SMulCommClass R A A
inst_4 : IsScalarTower R A A
inst_5 : AddCommMonoid C
inst_6 : Module R C
inst_7 : CoalgebraStruct R C
f g : WithConv (C →ₗ[R] A)
⊢ f * g = toConv (mul' R A ∘ₗ (f.ofConv ⊗ₘ g.ofConv) ∘ₗ δ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Coalgebra.Convolution
Goal:
R : Type u_1
A : Type u_2
C : Type u_4
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : SMulCommClass R A A
inst_4 : IsScalarTower R A A
inst_5 : AddCommMonoid C
inst_6 : Module R C
inst_7 : CoalgebraStruct R C
f g : WithConv (C →ₗ[R] A)
c : C
⊢ Eq.{u_2 + 1} (α := A) (((f * g).ofConv : (a : C) → A) c : A)
    ((mul' R A : (a : A ⊗[R] A) → A)
        ((f.ofConv ⊗ₘ g.ofConv : (a : C ⊗[R] C) → A ⊗[R] A) ((δ : (a : C) → C ⊗[R] C) c) : A ⊗[R] A) :
      A)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, rfl
-- Module: Mathlib.RingTheory.Coalgebra.Convolution
Goal:
R : Type u_1
A : Type u_2
C : Type u_4
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : SMulCommClass R A A
inst_4 : IsScalarTower R A A
inst_5 : AddCommMonoid C
inst_6 : Module R C
inst_7 : CoalgebraStruct R C
a : C
𝓡 : Coalgebra.Repr.{u_1, u_4, u_5} R a
f g : WithConv (C →ₗ[R] A)
⊢ Eq.{u_2 + 1} (α := A) (((f * g).ofConv : (a : C) → A) a : A)
    (∑ i ∈ 𝓡.index,
        HMul.hMul (α := A) (β := A) ((f.ofConv : (a : C) → A) (𝓡.left i) : A)
          ((g.ofConv : (a : C) → A) (𝓡.right i) : A) :
      A)

Tactic:
simp [convMul_def, ← 𝓡.eq]

Premises used: LinearMap.convMul_def, Coalgebra.Repr.eq
-- Module: Mathlib.RingTheory.Coalgebra.Convolution
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : SMulCommClass R A A
inst_4 : IsScalarTower R A A
inst_5 : AddCommMonoid C
inst_6 : Module R C
inst_7 : CoalgebraStruct R C
f g h : WithConv (C →ₗ[R] A)
h₁ :
  ∀ (x : C),
    Eq.{u_2 + 1} (α := A) (((f * (g + h)).ofConv : (a : C) → A) x : A) (((f * g + f * h).ofConv : (a : C) → A) x : A)
⊢ f * (g + h) = f * g + f * h

Tactic:
ext
-- Module: Mathlib.RingTheory.Coalgebra.Convolution
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : SMulCommClass R A A
inst_4 : IsScalarTower R A A
inst_5 : AddCommMonoid C
inst_6 : Module R C
inst_7 : CoalgebraStruct R C
f g h : WithConv (C →ₗ[R] A)
x : C
⊢ Eq.{u_2 + 1} (α := A) (((f * (g + h)).ofConv : (a : C) → A) x : A) (((f * g + f * h).ofConv : (a : C) → A) x : A)

Tactic:
simp [map_add_right]

Premises used: TensorProduct.map_add_right
-- Module: Mathlib.RingTheory.Coalgebra.Convolution
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : SMulCommClass R A A
inst_4 : IsScalarTower R A A
inst_5 : AddCommMonoid C
inst_6 : Module R C
inst_7 : CoalgebraStruct R C
f g h : WithConv (C →ₗ[R] A)
h₁ :
  ∀ (x : C),
    Eq.{u_2 + 1} (α := A) ((((f + g) * h).ofConv : (a : C) → A) x : A) (((f * h + g * h).ofConv : (a : C) → A) x : A)
⊢ (f + g) * h = f * h + g * h

Tactic:
ext
-- Module: Mathlib.RingTheory.Coalgebra.Convolution
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : SMulCommClass R A A
inst_4 : IsScalarTower R A A
inst_5 : AddCommMonoid C
inst_6 : Module R C
inst_7 : CoalgebraStruct R C
f g h : WithConv (C →ₗ[R] A)
x : C
⊢ Eq.{u_2 + 1} (α := A) ((((f + g) * h).ofConv : (a : C) → A) x : A) (((f * h + g * h).ofConv : (a : C) → A) x : A)

Tactic:
simp [map_add_left]

Premises used: TensorProduct.map_add_left
-- Module: Mathlib.RingTheory.Coalgebra.Convolution
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : SMulCommClass R A A
inst_4 : IsScalarTower R A A
inst_5 : AddCommMonoid C
inst_6 : Module R C
inst_7 : CoalgebraStruct R C
f : WithConv (C →ₗ[R] A)
h : ∀ (x : C), Eq.{u_2 + 1} (α := A) (((0 * f).ofConv : (a : C) → A) x : A) ((ofConv 0 : (a : C) → A) x : A)
⊢ 0 * f = 0

Tactic:
ext
-- Module: Mathlib.RingTheory.Coalgebra.Convolution
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : SMulCommClass R A A
inst_4 : IsScalarTower R A A
inst_5 : AddCommMonoid C
inst_6 : Module R C
inst_7 : CoalgebraStruct R C
f : WithConv (C →ₗ[R] A)
x : C
⊢ Eq.{u_2 + 1} (α := A) (((0 * f).ofConv : (a : C) → A) x : A) ((ofConv 0 : (a : C) → A) x : A)

Tactic:
simp
-- Module: Mathlib.RingTheory.Coalgebra.Convolution
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : SMulCommClass R A A
inst_4 : IsScalarTower R A A
inst_5 : AddCommMonoid C
inst_6 : Module R C
inst_7 : CoalgebraStruct R C
f : WithConv (C →ₗ[R] A)
h : ∀ (x : C), Eq.{u_2 + 1} (α := A) (((f * 0).ofConv : (a : C) → A) x : A) ((ofConv 0 : (a : C) → A) x : A)
⊢ f * 0 = 0

Tactic:
ext
-- Module: Mathlib.RingTheory.Coalgebra.Convolution
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : SMulCommClass R A A
inst_4 : IsScalarTower R A A
inst_5 : AddCommMonoid C
inst_6 : Module R C
inst_7 : CoalgebraStruct R C
f : WithConv (C →ₗ[R] A)
x : C
⊢ Eq.{u_2 + 1} (α := A) (((f * 0).ofConv : (a : C) → A) x : A) ((ofConv 0 : (a : C) → A) x : A)

Tactic:
simp
-- Module: Mathlib.RingTheory.Coalgebra.Convolution
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : SMulCommClass R A A
inst_4 : IsScalarTower R A A
x y : A
h :
  Eq.{u_2 + 1} (α := A)
    (((HMul.hMul (α := WithConv (R →ₗ[R] A)) (toConv (toSpanSingleton R A x)) (toConv (toSpanSingleton R A y))).ofConv :
          (a : R) → A)
        1 :
      A)
    ((ofConv (toConv (toSpanSingleton R A (x * y))) : (a : R) → A) 1 : A)
⊢ HMul.hMul (α := WithConv (R →ₗ[R] A)) (toConv (toSpanSingleton R A x)) (toConv (toSpanSingleton R A y)) =
    toConv (toSpanSingleton R A (x * y))

Tactic:
ext
-- Module: Mathlib.RingTheory.Coalgebra.Convolution
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : SMulCommClass R A A
inst_4 : IsScalarTower R A A
x y : A
⊢ Eq.{u_2 + 1} (α := A)
    (((HMul.hMul (α := WithConv (R →ₗ[R] A)) (toConv (toSpanSingleton R A x)) (toConv (toSpanSingleton R A y))).ofConv :
          (a : R) → A)
        1 :
      A)
    ((ofConv (toConv (toSpanSingleton R A (x * y))) : (a : R) → A) 1 : A)

Tactic:
simp
-- Module: Mathlib.RingTheory.Coalgebra.Convolution
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : SMulCommClass R A A
inst_4 : IsScalarTower R A A
inst_5 : AddCommMonoid C
inst_6 : Module R C
inst_7 : CoalgebraStruct R C
D : Type u_5
inst_8 : AddCommMonoid B
inst_9 : Module R B
inst_10 : CoalgebraStruct R B
inst_11 : NonUnitalNonAssocSemiring D
inst_12 : Module R D
inst_13 : SMulCommClass R D D
inst_14 : IsScalarTower R D D
f h : WithConv (C →ₗ[R] A)
g k : WithConv (B →ₗ[R] D)
simp_rw :
  toConv
      ((mul' R A ⊗ₘ mul' R D) ∘ₗ
        ((↑(tensorTensorTensorComm R A D A D) : A ⊗[R] D ⊗[R] (A ⊗[R] D) →ₗ[R] A ⊗[R] A ⊗[R] (D ⊗[R] D)) ∘ₗ
            ((f.ofConv ⊗ₘ g.ofConv) ⊗ₘ (h.ofConv ⊗ₘ k.ofConv))) ∘ₗ
          ((↑(AlgebraTensorModule.tensorTensorTensorComm R R R R C C B B) :
                TensorProduct.{u_1, u_4, u_3} R (C ⊗[R] C) (B ⊗[R] B) →ₗ[R] C ⊗[R] B ⊗[R] (C ⊗[R] B)) :
              TensorProduct.{u_1, u_4, u_3} R (C ⊗[R] C) (B ⊗[R] B) →ₗ[R] C ⊗[R] B ⊗[R] (C ⊗[R] B)) ∘ₗ
            (δ ⊗ₘ δ : C ⊗[R] B →ₗ[R] TensorProduct.{u_1, u_4, u_3} R (C ⊗[R] C) (B ⊗[R] B))) =
    toConv (mul' R A ∘ₗ (f.ofConv ⊗ₘ h.ofConv) ∘ₗ δ ⊗ₘ mul' R D ∘ₗ (g.ofConv ⊗ₘ k.ofConv) ∘ₗ δ)
⊢ toConv (f.ofConv ⊗ₘ g.ofConv) * toConv (h.ofConv ⊗ₘ k.ofConv) = toConv ((f * h).ofConv ⊗ₘ (g * k).ofConv)

Tactic:
simp_rw [convMul_def, comul_def, mul'_tensor, comp_assoc, AlgebraTensorModule.map_eq,
    ← comp_assoc _ _ (tensorTensorTensorComm R _ _ _ _).toLinearMap]

Premises used: LinearMap.convMul_def, LinearMap.comp_assoc, TensorProduct.AlgebraTensorModule.map_eq, TensorProduct.tensorTensorTensorComm, LinearEquiv.toLinearMap, TensorProduct.comul_def, LinearMap.mul'_tensor
-- Module: Mathlib.RingTheory.Coalgebra.Convolution
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : SMulCommClass R A A
inst_4 : IsScalarTower R A A
inst_5 : AddCommMonoid C
inst_6 : Module R C
inst_7 : CoalgebraStruct R C
D : Type u_5
inst_8 : AddCommMonoid B
inst_9 : Module R B
inst_10 : CoalgebraStruct R B
inst_11 : NonUnitalNonAssocSemiring D
inst_12 : Module R D
inst_13 : SMulCommClass R D D
inst_14 : IsScalarTower R D D
f h : WithConv (C →ₗ[R] A)
g k : WithConv (B →ₗ[R] D)
nth_rw :
  toConv
      ((mul' R A ⊗ₘ mul' R D) ∘ₗ
        ((↑(tensorTensorTensorComm R A D A D) : A ⊗[R] D ⊗[R] (A ⊗[R] D) →ₗ[R] A ⊗[R] A ⊗[R] (D ⊗[R] D)) ∘ₗ
              ((f.ofConv ⊗ₘ g.ofConv) ⊗ₘ (h.ofConv ⊗ₘ k.ofConv)) ∘ₗ
                (↑(AlgebraTensorModule.tensorTensorTensorComm R R R R C C B B) :
                  C ⊗[R] C ⊗[R] (B ⊗[R] B) →ₗ[R] C ⊗[R] B ⊗[R] (C ⊗[R] B)) :
            TensorProduct.{u_1, u_4, u_3} R (C ⊗[R] C) (B ⊗[R] B) →ₗ[R]
              TensorProduct.{u_1, u_2, u_5} R (A ⊗[R] A) (D ⊗[R] D)) ∘ₗ
          (δ ⊗ₘ δ : C ⊗[R] B →ₗ[R] TensorProduct.{u_1, u_4, u_3} R (C ⊗[R] C) (B ⊗[R] B))) =
    toConv (mul' R A ∘ₗ (f.ofConv ⊗ₘ h.ofConv) ∘ₗ δ ⊗ₘ mul' R D ∘ₗ (g.ofConv ⊗ₘ k.ofConv) ∘ₗ δ)
⊢ toConv
      ((mul' R A ⊗ₘ mul' R D) ∘ₗ
        ((↑(tensorTensorTensorComm R A D A D) : A ⊗[R] D ⊗[R] (A ⊗[R] D) →ₗ[R] A ⊗[R] A ⊗[R] (D ⊗[R] D)) ∘ₗ
            ((f.ofConv ⊗ₘ g.ofConv) ⊗ₘ (h.ofConv ⊗ₘ k.ofConv))) ∘ₗ
          ((↑(AlgebraTensorModule.tensorTensorTensorComm R R R R C C B B) :
                TensorProduct.{u_1, u_4, u_3} R (C ⊗[R] C) (B ⊗[R] B) →ₗ[R] C ⊗[R] B ⊗[R] (C ⊗[R] B)) :
              TensorProduct.{u_1, u_4, u_3} R (C ⊗[R] C) (B ⊗[R] B) →ₗ[R] C ⊗[R] B ⊗[R] (C ⊗[R] B)) ∘ₗ
            (δ ⊗ₘ δ : C ⊗[R] B →ₗ[R] TensorProduct.{u_1, u_4, u_3} R (C ⊗[R] C) (B ⊗[R] B))) =
    toConv (mul' R A ∘ₗ (f.ofConv ⊗ₘ h.ofConv) ∘ₗ δ ⊗ₘ mul' R D ∘ₗ (g.ofConv ⊗ₘ k.ofConv) ∘ₗ δ)

Tactic:
nth_rw 2 [← comp_assoc, comp_assoc]

Premises used: LinearMap.comp_assoc
-- Module: Mathlib.RingTheory.Coalgebra.Convolution
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : SMulCommClass R A A
inst_4 : IsScalarTower R A A
inst_5 : AddCommMonoid C
inst_6 : Module R C
inst_7 : CoalgebraStruct R C
D : Type u_5
inst_8 : AddCommMonoid B
inst_9 : Module R B
inst_10 : CoalgebraStruct R B
inst_11 : NonUnitalNonAssocSemiring D
inst_12 : Module R D
inst_13 : SMulCommClass R D D
inst_14 : IsScalarTower R D D
f h : WithConv (C →ₗ[R] A)
g k : WithConv (B →ₗ[R] D)
⊢ toConv
      ((mul' R A ⊗ₘ mul' R D) ∘ₗ
        ((↑(tensorTensorTensorComm R A D A D) : A ⊗[R] D ⊗[R] (A ⊗[R] D) →ₗ[R] A ⊗[R] A ⊗[R] (D ⊗[R] D)) ∘ₗ
              ((f.ofConv ⊗ₘ g.ofConv) ⊗ₘ (h.ofConv ⊗ₘ k.ofConv)) ∘ₗ
                (↑(AlgebraTensorModule.tensorTensorTensorComm R R R R C C B B) :
                  C ⊗[R] C ⊗[R] (B ⊗[R] B) →ₗ[R] C ⊗[R] B ⊗[R] (C ⊗[R] B)) :
            TensorProduct.{u_1, u_4, u_3} R (C ⊗[R] C) (B ⊗[R] B) →ₗ[R]
              TensorProduct.{u_1, u_2, u_5} R (A ⊗[R] A) (D ⊗[R] D)) ∘ₗ
          (δ ⊗ₘ δ : C ⊗[R] B →ₗ[R] TensorProduct.{u_1, u_4, u_3} R (C ⊗[R] C) (B ⊗[R] B))) =
    toConv (mul' R A ∘ₗ (f.ofConv ⊗ₘ h.ofConv) ∘ₗ δ ⊗ₘ mul' R D ∘ₗ (g.ofConv ⊗ₘ k.ofConv) ∘ₗ δ)

Tactic:
simp [AlgebraTensorModule.tensorTensorTensorComm_eq, ← tensorTensorTensorComm_comp_map,
    ← comp_assoc, map_comp]

Premises used: TensorProduct.tensorTensorTensorComm_comp_map, LinearMap.comp_assoc, TensorProduct.AlgebraTensorModule.tensorTensorTensorComm_eq, TensorProduct.map_comp
-- Module: Mathlib.RingTheory.Coalgebra.Convolution
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst : CommSemiring R
inst_1 : NonUnitalSemiring A
inst_2 : Module R A
inst_3 : SMulCommClass R A A
inst_4 : IsScalarTower R A A
inst_5 : AddCommMonoid C
inst_6 : Module R C
inst_7 : Coalgebra R C
inst_8 : NonUnitalNonAssocSemiring B
inst_9 : Module R B
inst_10 : SMulCommClass R B B
inst_11 : IsScalarTower R B B
h : A →ₙₐ[R] B
f g : WithConv (C →ₗ[R] A)
⊢ (↑h : [inst_12 : FunLike (A →ₙₐ[R] B) A B] → [SemilinearMapClass (A →ₙₐ[R] B) (RingHom.id R) A B] → A →ₗ[R] B) ∘ₗ
      (f * g).ofConv =
    (HMul.hMul (α := WithConv (C →ₗ[R] B))
        (toConv
          ((↑h :
              [inst_12 : FunLike (A →ₙₐ[R] B) A B] →
                [SemilinearMapClass (A →ₙₐ[R] B) (RingHom.id R) A B] → A →ₗ[R] B) ∘ₗ
            f.ofConv))
        (toConv
          ((↑h :
              [inst_12 : FunLike (A →ₙₐ[R] B) A B] →
                [SemilinearMapClass (A →ₙₐ[R] B) (RingHom.id R) A B] → A →ₗ[R] B) ∘ₗ
            g.ofConv))).ofConv

Tactic:
simp [convMul_def, map_comp, ← comp_assoc, NonUnitalAlgHom.comp_mul']

Premises used: LinearMap.convMul_def, LinearMap.comp_assoc, TensorProduct.map_comp, NonUnitalAlgHom.comp_mul'
-- Module: Mathlib.RingTheory.Coalgebra.Convolution
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst : CommSemiring R
inst_1 : NonUnitalSemiring A
inst_2 : Module R A
inst_3 : SMulCommClass R A A
inst_4 : IsScalarTower R A A
inst_5 : AddCommMonoid C
inst_6 : Module R C
inst_7 : Coalgebra R C
inst_8 : AddCommMonoid B
inst_9 : Module R B
inst_10 : CoalgebraStruct R B
f g : WithConv (C →ₗ[R] A)
h : B →ₗc[R] C
⊢ (f * g).ofConv ∘ₗ h.toLinearMap = (toConv (f.ofConv ∘ₗ h.toLinearMap) * toConv (g.ofConv ∘ₗ h.toLinearMap)).ofConv

Tactic:
simp [convMul_def, map_comp, comp_assoc]

Premises used: LinearMap.convMul_def, LinearMap.comp_assoc, TensorProduct.map_comp
-- Module: Mathlib.RingTheory.Coalgebra.Convolution
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst : CommSemiring R
inst_1 : NonUnitalSemiring A
inst_2 : Module R A
inst_3 : SMulCommClass R A A
inst_4 : IsScalarTower R A A
inst_5 : AddCommMonoid C
inst_6 : Module R C
inst_7 : Coalgebra R C
f g h : WithConv (C →ₗ[R] A)
h₁ :
  ∀ (x : C),
    Eq.{u_2 + 1} (α := A) ((mul' R A ∘ₗ ((f * g).ofConv ⊗ₘ h.ofConv) ∘ₗ δ : (a : C) → A) x : A)
      (((mul' R A ∘ₗ rTensor A (mul' R A)) ∘ₗ
              (((f.ofConv ⊗ₘ g.ofConv) ⊗ₘ h.ofConv) ∘ₗ
                  (↑(LinearEquiv.symm (TensorProduct.assoc R C C C)) : C ⊗[R] (C ⊗[R] C) →ₗ[R] C ⊗[R] C ⊗[R] C)) ∘ₗ
                lTensor C δ ∘ₗ δ :
            (a : C) → A)
          x :
        A)
⊢ mul' R A ∘ₗ ((f * g).ofConv ⊗ₘ h.ofConv) ∘ₗ δ =
    (mul' R A ∘ₗ rTensor A (mul' R A)) ∘ₗ
      (((f.ofConv ⊗ₘ g.ofConv) ⊗ₘ h.ofConv) ∘ₗ
          (↑(LinearEquiv.symm (TensorProduct.assoc R C C C)) : C ⊗[R] (C ⊗[R] C) →ₗ[R] C ⊗[R] C ⊗[R] C)) ∘ₗ
        lTensor C δ ∘ₗ δ

Tactic:
ext
-- Module: Mathlib.RingTheory.Coalgebra.Convolution
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst : CommSemiring R
inst_1 : NonUnitalSemiring A
inst_2 : Module R A
inst_3 : SMulCommClass R A A
inst_4 : IsScalarTower R A A
inst_5 : AddCommMonoid C
inst_6 : Module R C
inst_7 : Coalgebra R C
f g h : WithConv (C →ₗ[R] A)
x : C
⊢ Eq.{u_2 + 1} (α := A) ((mul' R A ∘ₗ ((f * g).ofConv ⊗ₘ h.ofConv) ∘ₗ δ : (a : C) → A) x : A)
    (((mul' R A ∘ₗ rTensor A (mul' R A)) ∘ₗ
            (((f.ofConv ⊗ₘ g.ofConv) ⊗ₘ h.ofConv) ∘ₗ
                (↑(LinearEquiv.symm (TensorProduct.assoc R C C C)) : C ⊗[R] (C ⊗[R] C) →ₗ[R] C ⊗[R] C ⊗[R] C)) ∘ₗ
              lTensor C δ ∘ₗ δ :
          (a : C) → A)
        x :
      A)

Tactic:
simp [comp_assoc, coassoc_symm, convMul_def]

Premises used: LinearMap.convMul_def, LinearMap.comp_assoc, Coalgebra.coassoc_symm