-- 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] ((i : n) → A i) ⊗[R] R) (lTensor ((i : n) → A i) counit ∘ₗ comul ∘ₗ LinearMap.single R A i)
    ((LinearMap.flip (TensorProduct.mk R ((i : n) → A i) R) : (a : R) → ((i : n) → A i) →ₗ[R] ((i : n) → A i) ⊗[R] R)
        1 ∘ₗ
      LinearMap.single R A i)
h₁ :
  Eq (α := A i →ₗ[R] ((i : n) → A i) ⊗[R] R)
    (lTensor ((i : n) → A i) counit ∘ₗ map (LinearMap.single R A i) (LinearMap.single R A i) ∘ₗ comul)
    ((LinearMap.flip (TensorProduct.mk R ((i : n) → A i) R) : (a : R) → ((i : n) → A i) →ₗ[R] ((i : n) → A i) ⊗[R] R)
        1 ∘ₗ
      LinearMap.single R A i)
h₂ :
  Eq (α := A i →ₗ[R] ((i : n) → A i) ⊗[R] R)
    ((lTensor ((i : n) → A i) counit ∘ₗ map (LinearMap.single R A i) (LinearMap.single R A i)) ∘ₗ comul)
    ((LinearMap.flip (TensorProduct.mk R ((i : n) → A i) R) : (a : R) → ((i : n) → A i) →ₗ[R] ((i : n) → A i) ⊗[R] R)
        1 ∘ₗ
      LinearMap.single R A i)
h₃ :
  Eq (α := A i →ₗ[R] ((i : n) → A i) ⊗[R] R) (map (LinearMap.single R A i) (counit ∘ₗ LinearMap.single R A i) ∘ₗ comul)
    ((LinearMap.flip (TensorProduct.mk R ((i : n) → A i) R) : (a : R) → ((i : n) → A i) →ₗ[R] ((i : n) → A i) ⊗[R] R)
        1 ∘ₗ
      LinearMap.single R A i)
h₄ :
  Eq (α := A i →ₗ[R] ((i : n) → A i) ⊗[R] R) (map (LinearMap.single R A i) counit ∘ₗ comul)
    ((LinearMap.flip (TensorProduct.mk R ((i : n) → A i) R) : (a : R) → ((i : n) → A i) →ₗ[R] ((i : n) → A i) ⊗[R] R)
        1 ∘ₗ
      LinearMap.single R A i)
h₅ :
  Eq (α := A i →ₗ[R] ((i : n) → A i) ⊗[R] R) ((rTensor R (LinearMap.single R A i) ∘ₗ lTensor (A i) counit) ∘ₗ comul)
    ((LinearMap.flip (TensorProduct.mk R ((i : n) → A i) R) : (a : R) → ((i : n) → A i) →ₗ[R] ((i : n) → A i) ⊗[R] R)
        1 ∘ₗ
      LinearMap.single R A i)
h₆ :
  Eq (α := A i →ₗ[R] ((i : n) → A i) ⊗[R] R) (rTensor R (LinearMap.single R A i) ∘ₗ lTensor (A i) counit ∘ₗ comul)
    ((LinearMap.flip (TensorProduct.mk R ((i : n) → A i) R) : (a : R) → ((i : n) → A i) →ₗ[R] ((i : n) → A i) ⊗[R] R)
        1 ∘ₗ
      LinearMap.single R A i)
h₇ :
  Eq (α := A i →ₗ[R] ((i : n) → A i) ⊗[R] R)
    (rTensor R (LinearMap.single R A i) ∘ₗ
      (LinearMap.flip (TensorProduct.mk R (A i) R) : (a : R) → A i →ₗ[R] A i ⊗[R] R) 1)
    ((LinearMap.flip (TensorProduct.mk R ((i : n) → A i) R) : (a : R) → ((i : n) → A i) →ₗ[R] ((i : n) → A i) ⊗[R] R)
        1 ∘ₗ
      LinearMap.single R A i)
h₈ h₉ :
  Eq (α := A i →ₗ[R] ((i : n) → A i) ⊗[R] R)
    ((LinearMap.flip (TensorProduct.mk R ((i : n) → A i) R) : (a : R) → ((i : n) → A i) →ₗ[R] ((i : n) → A i) ⊗[R] R)
        1 ∘ₗ
      LinearMap.single R A i)
    ((LinearMap.flip (TensorProduct.mk R ((i : n) → A i) R) : (a : R) → ((i : n) → A i) →ₗ[R] ((i : n) → A i) ⊗[R] R)
        1 ∘ₗ
      LinearMap.single R A i)
⊢ Eq (α := A i →ₗ[R] ((i : n) → A i) ⊗[R] R) ((lTensor ((i : n) → A i) counit ∘ₗ comul) ∘ₗ LinearMap.single R A i)
    ((LinearMap.flip (TensorProduct.mk R ((i : n) → A i) R) : (a : R) → ((i : n) → A i) →ₗ[R] ((i : n) → A i) ⊗[R] R)
        1 ∘ₗ
      LinearMap.single R A i)

Tactic:
rw [comp_assoc, comul_comp_single, ← comp_assoc, lTensor_comp_map, counit_comp_single,
      ← rTensor_comp_lTensor, comp_assoc, lTensor_counit_comp_comul, rTensor_comp_flip_mk]

Premises used: Pi.comul_comp_single, LinearMap.rTensor_comp_lTensor, LinearMap.rTensor_comp_flip_mk, LinearMap.comp_assoc, Coalgebra.lTensor_counit_comp_comul, LinearMap.lTensor_comp_map, Pi.counit_comp_single