-- Module: Mathlib.RingTheory.Coalgebra.Basic
Goal:
R : Type u_1
n : Type u_2
inst : CommSemiring R
inst_1 : Fintype n
inst_2 : DecidableEq n
A : n → Type u_3
inst_3 : (i : n) → AddCommMonoid (A i)
inst_4 : (i : n) → Module.{u_1, u_3} R (A i)
inst_5 : (i : n) → Coalgebra.{u_1, u_3} R (A i)
i : n
h :
  Eq (α := A i →ₗ[R] R ⊗[R] ((i : n) → A i)) (rTensor ((i : n) → A i) counit ∘ₗ comul ∘ₗ LinearMap.single R A i)
    ((TensorProduct.mk R R ((i : n) → A i) : (a : R) → ((i : n) → A i) →ₗ[R] R ⊗[R] ((i : n) → A i)) 1 ∘ₗ
      LinearMap.single R A i)
h₁ :
  Eq (α := A i →ₗ[R] R ⊗[R] ((i : n) → A i))
    (rTensor ((i : n) → A i) counit ∘ₗ map (LinearMap.single R A i) (LinearMap.single R A i) ∘ₗ comul)
    ((TensorProduct.mk R R ((i : n) → A i) : (a : R) → ((i : n) → A i) →ₗ[R] R ⊗[R] ((i : n) → A i)) 1 ∘ₗ
      LinearMap.single R A i)
h₂ :
  Eq (α := A i →ₗ[R] R ⊗[R] ((i : n) → A i))
    ((rTensor ((i : n) → A i) counit ∘ₗ map (LinearMap.single R A i) (LinearMap.single R A i)) ∘ₗ comul)
    ((TensorProduct.mk R R ((i : n) → A i) : (a : R) → ((i : n) → A i) →ₗ[R] R ⊗[R] ((i : n) → A i)) 1 ∘ₗ
      LinearMap.single R A i)
h₃ :
  Eq (α := A i →ₗ[R] R ⊗[R] ((i : n) → A i)) (map (counit ∘ₗ LinearMap.single R A i) (LinearMap.single R A i) ∘ₗ comul)
    ((TensorProduct.mk R R ((i : n) → A i) : (a : R) → ((i : n) → A i) →ₗ[R] R ⊗[R] ((i : n) → A i)) 1 ∘ₗ
      LinearMap.single R A i)
h₄ :
  Eq (α := A i →ₗ[R] R ⊗[R] ((i : n) → A i)) (map counit (LinearMap.single R A i) ∘ₗ comul)
    ((TensorProduct.mk R R ((i : n) → A i) : (a : R) → ((i : n) → A i) →ₗ[R] R ⊗[R] ((i : n) → A i)) 1 ∘ₗ
      LinearMap.single R A i)
h₅ :
  Eq (α := A i →ₗ[R] R ⊗[R] ((i : n) → A i)) ((lTensor R (LinearMap.single R A i) ∘ₗ rTensor (A i) counit) ∘ₗ comul)
    ((TensorProduct.mk R R ((i : n) → A i) : (a : R) → ((i : n) → A i) →ₗ[R] R ⊗[R] ((i : n) → A i)) 1 ∘ₗ
      LinearMap.single R A i)
h₆ :
  Eq (α := A i →ₗ[R] R ⊗[R] ((i : n) → A i)) (lTensor R (LinearMap.single R A i) ∘ₗ rTensor (A i) counit ∘ₗ comul)
    ((TensorProduct.mk R R ((i : n) → A i) : (a : R) → ((i : n) → A i) →ₗ[R] R ⊗[R] ((i : n) → A i)) 1 ∘ₗ
      LinearMap.single R A i)
h₇ :
  Eq (α := A i →ₗ[R] R ⊗[R] ((i : n) → A i))
    (lTensor R (LinearMap.single R A i) ∘ₗ (TensorProduct.mk R R (A i) : (a : R) → A i →ₗ[R] R ⊗[R] A i) 1)
    ((TensorProduct.mk R R ((i : n) → A i) : (a : R) → ((i : n) → A i) →ₗ[R] R ⊗[R] ((i : n) → A i)) 1 ∘ₗ
      LinearMap.single R A i)
h₈ h₉ :
  Eq (α := A i →ₗ[R] R ⊗[R] ((i : n) → A i))
    ((TensorProduct.mk R R ((i : n) → A i) : (a : R) → ((i : n) → A i) →ₗ[R] R ⊗[R] ((i : n) → A i)) 1 ∘ₗ
      LinearMap.single R A i)
    ((TensorProduct.mk R R ((i : n) → A i) : (a : R) → ((i : n) → A i) →ₗ[R] R ⊗[R] ((i : n) → A i)) 1 ∘ₗ
      LinearMap.single R A i)
⊢ Eq (α := A i →ₗ[R] R ⊗[R] ((i : n) → A i)) ((rTensor ((i : n) → A i) counit ∘ₗ comul) ∘ₗ LinearMap.single R A i)
    ((TensorProduct.mk R R ((i : n) → A i) : (a : R) → ((i : n) → A i) →ₗ[R] R ⊗[R] ((i : n) → A i)) 1 ∘ₗ
      LinearMap.single R A i)

Tactic:
rw [comp_assoc, comul_comp_single, ← comp_assoc, rTensor_comp_map, counit_comp_single,
      ← lTensor_comp_rTensor, comp_assoc, rTensor_counit_comp_comul, lTensor_comp_mk]

Premises used: Pi.comul_comp_single, LinearMap.rTensor_comp_map, LinearMap.comp_assoc, Coalgebra.rTensor_counit_comp_comul, LinearMap.lTensor_comp_rTensor, LinearMap.lTensor_comp_mk, Pi.counit_comp_single