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

Tactic:
rw [comp_assoc, comul_comp_lsingle, ← comp_assoc, lTensor_comp_map, counit_comp_lsingle,
      ← rTensor_comp_lTensor, comp_assoc, lTensor_counit_comp_comul, rTensor_comp_flip_mk]

Premises used: LinearMap.rTensor_comp_lTensor, LinearMap.rTensor_comp_flip_mk, LinearMap.comp_assoc, DFinsupp.counit_comp_lsingle, DFinsupp.comul_comp_lsingle, Coalgebra.lTensor_counit_comp_comul, LinearMap.lTensor_comp_map