-- Module: Mathlib.RingTheory.Coalgebra.Basic
Goal:
R : Type u
ι : Type v
A : ι → Type w
inst : DecidableEq ι
inst_1 : CommSemiring R
inst_2 : (i : ι) → AddCommMonoid (A i)
inst_3 : (i : ι) → Module.{u, w} R (A i)
inst_4 : (i : ι) → Coalgebra.{u, w} R (A i)
i : ι
h :
  Eq (α := A i →ₗ[R] R ⊗[R] Π₀ (i : ι), A i) (rTensor (Π₀ (i : ι), A i) counit ∘ₗ comul ∘ₗ lsingle (M := A) i)
    ((TensorProduct.mk R R (Π₀ (i : ι), A i) : (a : R) → (Π₀ (i : ι), A i) →ₗ[R] R ⊗[R] Π₀ (i : ι), A i) 1 ∘ₗ
      lsingle (M := A) i)
h₁ :
  Eq (α := A i →ₗ[R] R ⊗[R] Π₀ (i : ι), A i)
    (rTensor (Π₀ (i : ι), A i) counit ∘ₗ TensorProduct.map (lsingle (M := A) i) (lsingle (M := A) i) ∘ₗ comul)
    ((TensorProduct.mk R R (Π₀ (i : ι), A i) : (a : R) → (Π₀ (i : ι), A i) →ₗ[R] R ⊗[R] Π₀ (i : ι), A i) 1 ∘ₗ
      lsingle (M := A) i)
h₂ :
  Eq (α := A i →ₗ[R] R ⊗[R] Π₀ (i : ι), A i)
    ((rTensor (Π₀ (i : ι), A i) counit ∘ₗ TensorProduct.map (lsingle (M := A) i) (lsingle (M := A) i)) ∘ₗ comul)
    ((TensorProduct.mk R R (Π₀ (i : ι), A i) : (a : R) → (Π₀ (i : ι), A i) →ₗ[R] R ⊗[R] Π₀ (i : ι), A i) 1 ∘ₗ
      lsingle (M := A) i)
h₃ :
  Eq (α := A i →ₗ[R] R ⊗[R] Π₀ (i : ι), A i)
    (TensorProduct.map (counit ∘ₗ lsingle (M := A) i) (lsingle (M := A) i) ∘ₗ comul)
    ((TensorProduct.mk R R (Π₀ (i : ι), A i) : (a : R) → (Π₀ (i : ι), A i) →ₗ[R] R ⊗[R] Π₀ (i : ι), A i) 1 ∘ₗ
      lsingle (M := A) i)
h₄ :
  Eq (α := A i →ₗ[R] R ⊗[R] Π₀ (i : ι), A i) (TensorProduct.map counit (lsingle (M := A) i) ∘ₗ comul)
    ((TensorProduct.mk R R (Π₀ (i : ι), A i) : (a : R) → (Π₀ (i : ι), A i) →ₗ[R] R ⊗[R] Π₀ (i : ι), A i) 1 ∘ₗ
      lsingle (M := A) i)
h₅ :
  Eq (α := A i →ₗ[R] R ⊗[R] Π₀ (i : ι), A i) ((lTensor R (lsingle (M := A) i) ∘ₗ rTensor (A i) counit) ∘ₗ comul)
    ((TensorProduct.mk R R (Π₀ (i : ι), A i) : (a : R) → (Π₀ (i : ι), A i) →ₗ[R] R ⊗[R] Π₀ (i : ι), A i) 1 ∘ₗ
      lsingle (M := A) i)
h₆ :
  Eq (α := A i →ₗ[R] R ⊗[R] Π₀ (i : ι), A i) (lTensor R (lsingle (M := A) i) ∘ₗ rTensor (A i) counit ∘ₗ comul)
    ((TensorProduct.mk R R (Π₀ (i : ι), A i) : (a : R) → (Π₀ (i : ι), A i) →ₗ[R] R ⊗[R] Π₀ (i : ι), A i) 1 ∘ₗ
      lsingle (M := A) i)
h₇ :
  Eq (α := A i →ₗ[R] R ⊗[R] Π₀ (i : ι), A i)
    (lTensor R (lsingle (M := A) i) ∘ₗ (TensorProduct.mk R R (A i) : (a : R) → A i →ₗ[R] R ⊗[R] A i) 1)
    ((TensorProduct.mk R R (Π₀ (i : ι), A i) : (a : R) → (Π₀ (i : ι), A i) →ₗ[R] R ⊗[R] Π₀ (i : ι), A i) 1 ∘ₗ
      lsingle (M := A) i)
h₈ h₉ :
  Eq (α := A i →ₗ[R] R ⊗[R] Π₀ (i : ι), A i)
    ((TensorProduct.mk R R (Π₀ (i : ι), A i) : (a : R) → (Π₀ (i : ι), A i) →ₗ[R] R ⊗[R] Π₀ (i : ι), A i) 1 ∘ₗ
      lsingle (M := A) i)
    ((TensorProduct.mk R R (Π₀ (i : ι), A i) : (a : R) → (Π₀ (i : ι), A i) →ₗ[R] R ⊗[R] Π₀ (i : ι), A i) 1 ∘ₗ
      lsingle (M := A) i)
⊢ Eq (α := A i →ₗ[R] R ⊗[R] Π₀ (i : ι), A i) ((rTensor (Π₀ (i : ι), A i) counit ∘ₗ comul) ∘ₗ lsingle (M := A) i)
    ((TensorProduct.mk R R (Π₀ (i : ι), A i) : (a : R) → (Π₀ (i : ι), A i) →ₗ[R] R ⊗[R] Π₀ (i : ι), A i) 1 ∘ₗ
      lsingle (M := A) i)

Tactic:
rw [comp_assoc, comul_comp_lsingle, ← comp_assoc, rTensor_comp_map, counit_comp_lsingle,
      ← lTensor_comp_rTensor, comp_assoc, rTensor_counit_comp_comul, lTensor_comp_mk]

Premises used: LinearMap.rTensor_comp_map, LinearMap.comp_assoc, DFinsupp.counit_comp_lsingle, Coalgebra.rTensor_counit_comp_comul, LinearMap.lTensor_comp_rTensor, DFinsupp.comul_comp_lsingle, LinearMap.lTensor_comp_mk