-- Mathlib/RingTheory/Coalgebra/Basic.lean
theorem sum_map_tmul_tmul_eq {B : Type*} [AddCommMonoid B] [Module R B]
    {F : Type*} [FunLike F A B] [LinearMapClass F R A B] (f g h : F) (a : A) {repr : Repr R a}
    {a₁ : (i : repr.ι) → Repr R (repr.left i)} {a₂ : (i : repr.ι) → Repr R (repr.right i)} :
    ∑ i ∈ repr.index, ∑ j ∈ (a₂ i).index,
      f (repr.left i) ⊗ₜ (g ((a₂ i).left j) ⊗ₜ h ((a₂ i).right j)) =
    ∑ i ∈ repr.index, ∑ j ∈ (a₁ i).index,
      f ((a₁ i).left j) ⊗ₜ[R] (g ((a₁ i).right j) ⊗ₜ[R] h (repr.right i))

Proof state:
R : Type u
A : Type v
inst✝⁷ : CommSemiring R
inst✝⁶ : AddCommMonoid A
inst✝⁵ : Module R A
inst✝⁴ : Coalgebra R A
B : Type u_1
inst✝³ : AddCommMonoid B
inst✝² : Module R B
F : Type u_2
inst✝¹ : FunLike F A B
inst✝ : LinearMapClass F R A B
f g h : F
a : A
repr : Repr R a
a₁ : (i : repr.ι) → Repr R (repr.left i)
a₂ : (i : repr.ι) → Repr R (repr.right i)
this :
  ∑ i ∈ repr.index, ∑ j ∈ (a₁ i).index, (a₁ i).left j ⊗ₜ[R] (a₁ i).right j ⊗ₜ[R] repr.right i =
    ∑ i ∈ repr.index, ∑ j ∈ (a₂ i).index, repr.left i ⊗ₜ[R] (a₂ i).left j ⊗ₜ[R] (a₂ i).right j
⊢ ∑ i ∈ repr.index, ∑ j ∈ (a₂ i).index, f (repr.left i) ⊗ₜ[R] g ((a₂ i).left j) ⊗ₜ[R] h ((a₂ i).right j) =
    ∑ i ∈ repr.index, ∑ j ∈ (a₁ i).index, f ((a₁ i).left j) ⊗ₜ[R] g ((a₁ i).right j) ⊗ₜ[R] h (repr.right i)

Tactic:
apply_fun TensorProduct.map (f : A →ₗ[R] B)
  (TensorProduct.map (g : A →ₗ[R] B) (h : A →ₗ[R] B)) at this

Result:
R : Type u
A : Type v
inst✝⁷ : CommSemiring R
inst✝⁶ : AddCommMonoid A
inst✝⁵ : Module R A
inst✝⁴ : Coalgebra R A
B : Type u_1
inst✝³ : AddCommMonoid B
inst✝² : Module R B
F : Type u_2
inst✝¹ : FunLike F A B
inst✝ : LinearMapClass F R A B
f g h : F
a : A
repr : Repr R a
a₁ : (i : repr.ι) → Repr R (repr.left i)
a₂ : (i : repr.ι) → Repr R (repr.right i)
this :
  (TensorProduct.map (↑f) (TensorProduct.map ↑g ↑h))
      (∑ i ∈ repr.index, ∑ j ∈ (a₁ i).index, (a₁ i).left j ⊗ₜ[R] (a₁ i).right j ⊗ₜ[R] repr.right i) =
    (TensorProduct.map (↑f) (TensorProduct.map ↑g ↑h))
      (∑ i ∈ repr.index, ∑ j ∈ (a₂ i).index, repr.left i ⊗ₜ[R] (a₂ i).left j ⊗ₜ[R] (a₂ i).right j)
⊢ ∑ i ∈ repr.index, ∑ j ∈ (a₂ i).index, f (repr.left i) ⊗ₜ[R] g ((a₂ i).left j) ⊗ₜ[R] h ((a₂ i).right j) =
    ∑ i ∈ repr.index, ∑ j ∈ (a₁ i).index, f ((a₁ i).left j) ⊗ₜ[R] g ((a₁ i).right j) ⊗ₜ[R] h (repr.right i)

Proof state:
R : Type u
A : Type v
inst✝⁷ : CommSemiring R
inst✝⁶ : AddCommMonoid A
inst✝⁵ : Module R A
inst✝⁴ : Coalgebra R A
B : Type u_1
inst✝³ : AddCommMonoid B
inst✝² : Module R B
F : Type u_2
inst✝¹ : FunLike F A B
inst✝ : LinearMapClass F R A B
f g h : F
a : A
repr : Repr R a
a₁ : (i : repr.ι) → Repr R (repr.left i)
a₂ : (i : repr.ι) → Repr R (repr.right i)
⊢ ∑ i ∈ repr.index, ∑ j ∈ (a₂ i).index, f (repr.left i) ⊗ₜ[R] g ((a₂ i).left j) ⊗ₜ[R] h ((a₂ i).right j) =
    ∑ i ∈ repr.index, ∑ j ∈ (a₁ i).index, f ((a₁ i).left j) ⊗ₜ[R] g ((a₁ i).right j) ⊗ₜ[R] h (repr.right i)

Tactic:
have := sum_tmul_tmul_eq repr a₁ a₂

Result:
R : Type u
A : Type v
inst✝⁷ : CommSemiring R
inst✝⁶ : AddCommMonoid A
inst✝⁵ : Module R A
inst✝⁴ : Coalgebra R A
B : Type u_1
inst✝³ : AddCommMonoid B
inst✝² : Module R B
F : Type u_2
inst✝¹ : FunLike F A B
inst✝ : LinearMapClass F R A B
f g h : F
a : A
repr : Repr R a
a₁ : (i : repr.ι) → Repr R (repr.left i)
a₂ : (i : repr.ι) → Repr R (repr.right i)
this :
  ∑ i ∈ repr.index, ∑ j ∈ (a₁ i).index, (a₁ i).left j ⊗ₜ[R] (a₁ i).right j ⊗ₜ[R] repr.right i =
    ∑ i ∈ repr.index, ∑ j ∈ (a₂ i).index, repr.left i ⊗ₜ[R] (a₂ i).left j ⊗ₜ[R] (a₂ i).right j
⊢ ∑ i ∈ repr.index, ∑ j ∈ (a₂ i).index, f (repr.left i) ⊗ₜ[R] g ((a₂ i).left j) ⊗ₜ[R] h ((a₂ i).right j) =
    ∑ i ∈ repr.index, ∑ j ∈ (a₁ i).index, f ((a₁ i).left j) ⊗ₜ[R] g ((a₁ i).right j) ⊗ₜ[R] h (repr.right i)

Proof state:
R : Type u
A : Type v
inst✝⁷ : CommSemiring R
inst✝⁶ : AddCommMonoid A
inst✝⁵ : Module R A
inst✝⁴ : Coalgebra R A
B : Type u_1
inst✝³ : AddCommMonoid B
inst✝² : Module R B
F : Type u_2
inst✝¹ : FunLike F A B
inst✝ : LinearMapClass F R A B
f g h : F
a : A
repr : Repr R a
a₁ : (i : repr.ι) → Repr R (repr.left i)
a₂ : (i : repr.ι) → Repr R (repr.right i)
this :
  (TensorProduct.map (↑f) (TensorProduct.map ↑g ↑h))
      (∑ i ∈ repr.index, ∑ j ∈ (a₁ i).index, (a₁ i).left j ⊗ₜ[R] (a₁ i).right j ⊗ₜ[R] repr.right i) =
    (TensorProduct.map (↑f) (TensorProduct.map ↑g ↑h))
      (∑ i ∈ repr.index, ∑ j ∈ (a₂ i).index, repr.left i ⊗ₜ[R] (a₂ i).left j ⊗ₜ[R] (a₂ i).right j)
⊢ ∑ i ∈ repr.index, ∑ j ∈ (a₂ i).index, f (repr.left i) ⊗ₜ[R] g ((a₂ i).left j) ⊗ₜ[R] h ((a₂ i).right j) =
    ∑ i ∈ repr.index, ∑ j ∈ (a₁ i).index, f ((a₁ i).left j) ⊗ₜ[R] g ((a₁ i).right j) ⊗ₜ[R] h (repr.right i)

Tactic:
simp_all only [map_sum, TensorProduct.map_tmul, LinearMap.coe_coe]

Result:
no goals