awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.CoassocSimps (goal)
Goal:
R : Type u_1
M : Type u_3
N : Type u_4
M' : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : AddCommMonoid M'
inst_6 : Module R M'
inst_7 : Coalgebra R M
f : M →ₗ[R] M'
g : N →ₗ[R] M
⊢ α⁻¹ ∘ₗ f ⊗ₘ δ ∘ₗ δ ∘ₗ g = (f ⊗ₘ LinearMap.id) ⊗ₘ LinearMap.id ∘ₗ δ ⊗ₘ LinearMap.id ∘ₗ δ ∘ₗ g
have simp : ((α⁻¹ ∘ₗ f ⊗ₘ δ) ∘ₗ δ) ∘ₗ g = (((f ⊗ₘ LinearMap.id) ⊗ₘ LinearMap.id ∘ₗ δ ⊗ₘ LinearMap.id) ∘ₗ δ) ∘ₗ g
Tactic: simp only [← LinearMap.comp_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.CoassocSimps (goal)
Goal:
R : Type u_1
M : Type u_3
N : Type u_4
M' : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : AddCommMonoid M'
inst_6 : Module R M'
inst_7 : Coalgebra R M
f : M →ₗ[R] M'
g : N →ₗ[R] M
⊢ ((α⁻¹ ∘ₗ f ⊗ₘ δ) ∘ₗ δ) ∘ₗ g = (((f ⊗ₘ LinearMap.id) ⊗ₘ LinearMap.id ∘ₗ δ ⊗ₘ LinearMap.id) ∘ₗ δ) ∘ₗ g
have e_f : (α⁻¹ ∘ₗ f ⊗ₘ δ) ∘ₗ δ = ((f ⊗ₘ LinearMap.id) ⊗ₘ LinearMap.id ∘ₗ δ ⊗ₘ LinearMap.id) ∘ₗ δ
Tactic: congr 1
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.CoassocSimps (goal)
Goal:
R : Type u_1
M : Type u_3
M' : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
inst_5 : Coalgebra R M
f : M →ₗ[R] M'
⊢ ε ⊗ₘ f ∘ₗ δ = LinearMap.id ⊗ₘ f ∘ₗ λ⁻¹
have rw : LinearMap.lTensor R f ∘ₗ (TensorProduct.mk R R M : (a : R) → M →ₗ[R] R ⊗[R] M) 1 = LinearMap.id ⊗ₘ f ∘ₗ λ⁻¹
Tactic: rw [← LinearMap.lTensor_comp_rTensor, LinearMap.comp_assoc, Coalgebra.rTensor_counit_comp_comul]
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.CoassocSimps (goal)
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
⊢ ε ⊗ₘ f ∘ₗ δ ∘ₗ g = LinearMap.id ⊗ₘ f ∘ₗ λ⁻¹ ∘ₗ g
have simp_rw : (ε ⊗ₘ f ∘ₗ δ) ∘ₗ g = (LinearMap.id ⊗ₘ f ∘ₗ λ⁻¹) ∘ₗ g
Tactic: simp_rw [← LinearMap.comp_assoc, map_counit_comp_comul_left]
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.CoassocSimps (goal)
Goal:
R : Type u_1
M : Type u_3
M' : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
inst_5 : Coalgebra R M
f : M →ₗ[R] M'
⊢ f ⊗ₘ ε ∘ₗ δ = f ⊗ₘ LinearMap.id ∘ₗ ρ⁻¹
have rw : LinearMap.rTensor R f ∘ₗ (LinearMap.flip (TensorProduct.mk R M R) : (a : R) → M →ₗ[R] M ⊗[R] R) 1 =
  f ⊗ₘ LinearMap.id ∘ₗ ρ⁻¹
Tactic: rw [← LinearMap.rTensor_comp_lTensor, LinearMap.comp_assoc, Coalgebra.lTensor_counit_comp_comul]
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.CoassocSimps (goal)
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
⊢ f ⊗ₘ ε ∘ₗ δ ∘ₗ g = f ⊗ₘ LinearMap.id ∘ₗ ρ⁻¹ ∘ₗ g
have simp_rw : (f ⊗ₘ ε ∘ₗ δ) ∘ₗ g = (f ⊗ₘ LinearMap.id ∘ₗ ρ⁻¹) ∘ₗ g
Tactic: simp_rw [← LinearMap.comp_assoc, map_counit_comp_comul_right]
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.CoassocSimps (goal)
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
⊢ α ∘ₗ (β ∘ₗ δ) ⊗ₘ f ∘ₗ δ = LinearMap.id ⊗ₘ (LinearMap.id ⊗ₘ f ∘ₗ β) ∘ₗ α ∘ₗ δ ⊗ₘ LinearMap.id ∘ₗ β ∘ₗ δ
have rw : α ∘ₗ (β ⊗ₘ f ∘ₗ LinearMap.rTensor M δ) ∘ₗ δ =
  LinearMap.lTensor M (LinearMap.lTensor M (f ∘ₗ LinearMap.id) ∘ₗ β) ∘ₗ α ∘ₗ β ∘ₗ α ∘ₗ LinearMap.rTensor M δ ∘ₗ δ
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]
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.CoassocSimps (goal)
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
⊢ α ∘ₗ (β ⊗ₘ f ∘ₗ LinearMap.rTensor M δ) ∘ₗ δ =
    LinearMap.lTensor M (LinearMap.lTensor M (f ∘ₗ LinearMap.id) ∘ₗ β) ∘ₗ α ∘ₗ β ∘ₗ α ∘ₗ LinearMap.rTensor M δ ∘ₗ δ
have simp : ((α ∘ₗ β ⊗ₘ f) ∘ₗ LinearMap.rTensor M δ) ∘ₗ δ =
  ((((LinearMap.lTensor M (LinearMap.lTensor M (f ∘ₗ LinearMap.id) ∘ₗ β) ∘ₗ α) ∘ₗ β) ∘ₗ α) ∘ₗ LinearMap.rTensor M δ) ∘ₗ
    δ
Tactic: simp only [← LinearMap.comp_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.CoassocSimps (goal)
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
⊢ ((α ∘ₗ β ⊗ₘ f) ∘ₗ LinearMap.rTensor M δ) ∘ₗ δ =
    ((((LinearMap.lTensor M (LinearMap.lTensor M (f ∘ₗ LinearMap.id) ∘ₗ β) ∘ₗ α) ∘ₗ β) ∘ₗ α) ∘ₗ
        LinearMap.rTensor M δ) ∘ₗ
      δ
have e_f : Eq («α» := M ⊗[R] M ⊗[R] M →ₗ[R] M ⊗[R] (M ⊗[R] N)) (α ∘ₗ β ⊗ₘ f)
  (((LinearMap.lTensor M (LinearMap.lTensor M (f ∘ₗ LinearMap.id) ∘ₗ β) ∘ₗ α) ∘ₗ β) ∘ₗ α)
Tactic: congr 2
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.CoassocSimps (goal)
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
⊢ Eq («α» := M ⊗[R] M ⊗[R] M →ₗ[R] M ⊗[R] (M ⊗[R] N)) (α ∘ₗ β ⊗ₘ f)
    (((LinearMap.lTensor M (LinearMap.lTensor M (f ∘ₗ LinearMap.id) ∘ₗ β) ∘ₗ α) ∘ₗ β) ∘ₗ α)
have 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))
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.CoassocSimps (goal)
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 ∘ₗ δ ∘ₗ h = LinearMap.id ⊗ₘ (LinearMap.id ⊗ₘ f ∘ₗ β) ∘ₗ α ∘ₗ δ ⊗ₘ LinearMap.id ∘ₗ β ∘ₗ δ ∘ₗ h
have simp_rw : ((α ∘ₗ (β ∘ₗ δ) ⊗ₘ f) ∘ₗ δ) ∘ₗ h =
  ((((LinearMap.id ⊗ₘ (LinearMap.id ⊗ₘ f ∘ₗ β) ∘ₗ α) ∘ₗ δ ⊗ₘ LinearMap.id) ∘ₗ β) ∘ₗ δ) ∘ₗ h
Tactic: simp_rw [← LinearMap.comp_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.CoassocSimps (goal)
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) ∘ₗ δ) ∘ₗ h =
    ((((LinearMap.id ⊗ₘ (LinearMap.id ⊗ₘ f ∘ₗ β) ∘ₗ α) ∘ₗ δ ⊗ₘ LinearMap.id) ∘ₗ β) ∘ₗ δ) ∘ₗ h
have e_f : (α ∘ₗ (β ∘ₗ δ) ⊗ₘ f) ∘ₗ δ = (((LinearMap.id ⊗ₘ (LinearMap.id ⊗ₘ f ∘ₗ β) ∘ₗ α) ∘ₗ δ ⊗ₘ LinearMap.id) ∘ₗ β) ∘ₗ δ
Tactic: congr 1
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.Convolution (goal)
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)
⊢ f * (g + h) = f * g + f * h
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.Convolution (goal)
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)
⊢ (f + g) * h = f * h + g * h
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.Convolution (goal)
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)
⊢ 0 * f = 0
have h : ∀ (x : C), Eq.{u_2 + 1} (α := A) (((0 * f).ofConv : (a : C) → A) x : A) ((ofConv 0 : (a : C) → A) x : A)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.Convolution (goal)
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)
⊢ f * 0 = 0
have h : ∀ (x : C), Eq.{u_2 + 1} (α := A) (((f * 0).ofConv : (a : C) → A) x : A) ((ofConv 0 : (a : C) → A) x : A)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.Convolution (goal)
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
⊢ HMul.hMul (α := WithConv (R →ₗ[R] A)) (toConv (toSpanSingleton R A x)) (toConv (toSpanSingleton R A y)) =
    toConv (toSpanSingleton R A (x * y))
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.Convolution (goal)
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 (f.ofConv ⊗ₘ g.ofConv) * toConv (h.ofConv ⊗ₘ k.ofConv) = toConv ((f * h).ofConv ⊗ₘ (g * k).ofConv)
have 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) ∘ₗ δ)
Tactic: simp_rw [convMul_def, comul_def, mul'_tensor, comp_assoc, AlgebraTensorModule.map_eq,
    ← comp_assoc _ _ (tensorTensorTensorComm R _ _ _ _).toLinearMap]
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.Convolution (goal)
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) :
                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) ∘ₗ δ)
have 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) ∘ₗ δ)
Tactic: nth_rw 2 [← comp_assoc, comp_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.Convolution (goal)
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)
⊢ 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 δ ∘ₗ δ
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.Convolution (goal)
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)
⊢ (mul' R A ∘ₗ
        rTensor A (mul' R A) ∘ₗ
          (↑(LinearEquiv.symm (TensorProduct.assoc R A A A)) : A ⊗[R] (A ⊗[R] A) →ₗ[R] A ⊗[R] A ⊗[R] A)) ∘ₗ
      (f.ofConv ⊗ₘ (g.ofConv ⊗ₘ h.ofConv)) ∘ₗ lTensor C δ ∘ₗ δ =
    (mul' R A ∘ₗ lTensor A (mul' R A)) ∘ₗ (f.ofConv ⊗ₘ (g.ofConv ⊗ₘ h.ofConv)) ∘ₗ lTensor C δ ∘ₗ δ
have e_f : Eq (α := A ⊗[R] (A ⊗[R] A) →ₗ[R] A)
  (mul' R A ∘ₗ
    rTensor A (mul' R A) ∘ₗ
      (↑(LinearEquiv.symm (TensorProduct.assoc R A A A)) : A ⊗[R] (A ⊗[R] A) →ₗ[R] A ⊗[R] A ⊗[R] A))
  (mul' R A ∘ₗ lTensor A (mul' R A))
Tactic: congr 1
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.Convolution (goal)
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)
⊢ Eq (α := A ⊗[R] (A ⊗[R] A) →ₗ[R] A)
    (mul' R A ∘ₗ
      rTensor A (mul' R A) ∘ₗ
        (↑(LinearEquiv.symm (TensorProduct.assoc R A A A)) : A ⊗[R] (A ⊗[R] A) →ₗ[R] A ⊗[R] A ⊗[R] A))
    (mul' R A ∘ₗ lTensor A (mul' R A))
have e_f : ∀ (x x_1 x_2 : A),
  Eq (α := A)
    (((((AlgebraTensorModule.curry
                    (((AlgebraTensorModule.curry
                            (mul' R A ∘ₗ
                              rTensor A (mul' R A) ∘ₗ
                                (↑(LinearEquiv.symm (TensorProduct.assoc R A A A)) :
                                  A ⊗[R] (A ⊗[R] A) →ₗ[R] A ⊗[R] A ⊗[R] A)) :
                          A →ₗ[R] A ⊗[R] A →ₗ[R] A) :
                        (a : A) → A ⊗[R] A →ₗ[R] A)
                      x) :
                  A →ₗ[R] A →ₗ[R] A) :
                (a : A) → A →ₗ[R] A)
              x_1 :
            A →ₗ[R] A) :
          (a : A) → A)
        x_2 :
      A)
    (((((AlgebraTensorModule.curry
                    (((AlgebraTensorModule.curry (mul' R A ∘ₗ lTensor A (mul' R A)) : A →ₗ[R] A ⊗[R] A →ₗ[R] A) :
                        (a : A) → A ⊗[R] A →ₗ[R] A)
                      x) :
                  A →ₗ[R] A →ₗ[R] A) :
                (a : A) → A →ₗ[R] A)
              x_1 :
            A →ₗ[R] A) :
          (a : A) → A)
        x_2 :
      A)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.Convolution (goal)
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)
⊢ (mul' R A ∘ₗ lTensor A (mul' R A)) ∘ₗ (f.ofConv ⊗ₘ (g.ofConv ⊗ₘ h.ofConv)) ∘ₗ lTensor C δ ∘ₗ δ =
    mul' R A ∘ₗ (f.ofConv ⊗ₘ mul' R A ∘ₗ (g.ofConv ⊗ₘ h.ofConv) ∘ₗ δ) ∘ₗ δ
have h₁ : ∀ (x : C),
  Eq.{u_2 + 1} (α := A)
    (((mul' R A ∘ₗ lTensor A (mul' R A)) ∘ₗ (f.ofConv ⊗ₘ (g.ofConv ⊗ₘ h.ofConv)) ∘ₗ lTensor C δ ∘ₗ δ : (a : C) → A) x :
      A)
    ((mul' R A ∘ₗ (f.ofConv ⊗ₘ mul' R A ∘ₗ (g.ofConv ⊗ₘ h.ofConv) ∘ₗ δ) ∘ₗ δ : (a : C) → A) x : A)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.Convolution (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
inst_5 : AddCommMonoid C
inst_6 : Module R C
inst_7 : Coalgebra R C
f : WithConv (C →ₗ[R] A)
⊢ 1 * f = f
have h : ∀ (x : C), Eq.{u_2 + 1} (α := A) (((1 * f).ofConv : (a : C) → A) x : A) ((f.ofConv : (a : C) → A) x : A)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.Convolution (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
inst_5 : AddCommMonoid C
inst_6 : Module R C
inst_7 : Coalgebra R C
f : WithConv (C →ₗ[R] A)
⊢ f * 1 = f
have h : ∀ (x : C), Eq.{u_2 + 1} (α := A) (((f * 1).ofConv : (a : C) → A) x : A) ((f.ofConv : (a : C) → A) x : A)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.Convolution (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : AddCommMonoid C
inst_3 : Algebra R A
inst_4 : Module R C
inst_5 : Coalgebra R C
inst_6 : IsCocomm R C
f g : WithConv (C →ₗ[R] A)
⊢ f * g = g * f
have h : ∀ (x : C), Eq.{u_2 + 1} (α := A) (((f * g).ofConv : (a : C) → A) x : A) (((g * f).ofConv : (a : C) → A) x : A)
Tactic: ext x
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.Convolution (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : AddCommMonoid C
inst_3 : Algebra R A
inst_4 : Module R C
inst_5 : Coalgebra R C
inst_6 : IsCocomm R C
f g : WithConv (C →ₗ[R] A)
x : C
⊢ Eq.{u_2 + 1} (α := A) (((f * g).ofConv : (a : C) → A) x : A) (((g * f).ofConv : (a : C) → A) x : A)
have h : Eq (α := 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) x) : A ⊗[R] A) :
    A)
  (((g * f).ofConv : (a : C) → A) x : A)
Tactic: rw [convMul_apply, ← comm_comul R x, map_comm, mul'_comm, convMul_apply]
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.Convolution (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : AddCommMonoid C
inst_3 : Algebra R A
inst_4 : Module R C
inst_5 : Coalgebra R C
inst_6 : IsCocomm R C
f g : WithConv (C →ₗ[R] A)
x : C
h :
  Eq (α := 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) x) : A ⊗[R] A) :
      A)
    (((g * f).ofConv : (a : C) → A) x : A)
⊢ Eq.{u_2 + 1} (α := A) (((f * g).ofConv : (a : C) → A) x : A) (((g * f).ofConv : (a : C) → A) x : A)
have h₁ : Eq (α := A)
  ((mul' R A : (a : A ⊗[R] A) → A)
      ((f.ofConv ⊗ₘ g.ofConv : (a : C ⊗[R] C) → A ⊗[R] A)
          ((TensorProduct.comm R C C : (a : C ⊗[R] C) → C ⊗[R] C) ((δ : (a : C) → C ⊗[R] C) x)) :
        A ⊗[R] A) :
    A)
  (((g * f).ofConv : (a : C) → A) x : A)
Tactic: rw [convMul_apply, ← comm_comul R x, map_comm, mul'_comm, convMul_apply]
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.Convolution (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : AddCommMonoid C
inst_3 : Algebra R A
inst_4 : Module R C
inst_5 : Coalgebra R C
inst_6 : IsCocomm R C
f g : WithConv (C →ₗ[R] A)
x : C
h :
  Eq (α := 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) x) : A ⊗[R] A) :
      A)
    (((g * f).ofConv : (a : C) → A) x : A)
h₁ :
  Eq (α := A)
    ((mul' R A : (a : A ⊗[R] A) → A)
        ((f.ofConv ⊗ₘ g.ofConv : (a : C ⊗[R] C) → A ⊗[R] A)
            ((TensorProduct.comm R C C : (a : C ⊗[R] C) → C ⊗[R] C) ((δ : (a : C) → C ⊗[R] C) x)) :
          A ⊗[R] A) :
      A)
    (((g * f).ofConv : (a : C) → A) x : A)
⊢ Eq.{u_2 + 1} (α := A) (((f * g).ofConv : (a : C) → A) x : A) (((g * f).ofConv : (a : C) → A) x : A)
have h₂ : Eq (α := A)
  ((mul' R A : (a : A ⊗[R] A) → A)
      ((TensorProduct.comm R A A : (a : A ⊗[R] A) → A ⊗[R] A)
          ((g.ofConv ⊗ₘ f.ofConv : (a : C ⊗[R] C) → A ⊗[R] A) ((δ : (a : C) → C ⊗[R] C) x)) :
        A ⊗[R] A) :
    A)
  (((g * f).ofConv : (a : C) → A) x : A)
Tactic: rw [convMul_apply, ← comm_comul R x, map_comm, mul'_comm, convMul_apply]