-- Module: Mathlib.RingTheory.HopfAlgebra.Basic
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : HopfAlgebra R A
a b x y : A
ℛx : Coalgebra.Repr R x := ℛ R x
ℛy : Coalgebra.Repr R y := ℛ R y
calc :
  Eq (α := A)
    (∑ i ∈ ℛx.index,
      ∑ j ∈ ℛy.index,
        ℛx.left i * ℛy.left j *
          HMul.hMul (α := A) (β := A) ((antipode R : (a : A) → A) (ℛy.right j) : A)
            ((antipode R : (a : A) → A) (ℛx.right i) : A))
    (∑ i ∈ ℛx.index,
      ∑ j ∈ ℛy.index,
        ℛx.left i *
          HMul.hMul (β := A) (HMul.hMul (β := A) (ℛy.left j) ((antipode R : (a : A) → A) (ℛy.right j) : A))
            ((antipode R : (a : A) → A) (ℛx.right i) : A))
calc₁ :
  Eq (α := A)
    (∑ i ∈ ℛx.index,
      ∑ j ∈ ℛy.index,
        ℛx.left i *
          HMul.hMul (β := A) (HMul.hMul (β := A) (ℛy.left j) ((antipode R : (a : A) → A) (ℛy.right j) : A))
            ((antipode R : (a : A) → A) (ℛx.right i) : A))
    (∑ i ∈ ℛx.index,
      ℛx.left i *
        HMul.hMul (α := A) (β := A)
          (∑ j ∈ ℛy.index, HMul.hMul (β := A) (ℛy.left j) ((antipode R : (a : A) → A) (ℛy.right j) : A) : A)
          ((antipode R : (a : A) → A) (ℛx.right i) : A))
calc₂ :
  Eq (α := A)
    (∑ i ∈ ℛx.index,
      ℛx.left i *
        HMul.hMul (α := A) (β := A)
          (∑ j ∈ ℛy.index, HMul.hMul (β := A) (ℛy.left j) ((antipode R : (a : A) → A) (ℛy.right j) : A) : A)
          ((antipode R : (a : A) → A) (ℛx.right i) : A))
    (∑ i ∈ ℛx.index,
      ℛx.left i *
        HMul.hMul (β := A) (HSMul.hSMul.{u, v, v} (α := R) (β := A) ((counit : (a : A) → R) y : R) 1)
          ((antipode R : (a : A) → A) (ℛx.right i) : A))
calc₃ :
  Eq (α := A)
    (∑ i ∈ ℛx.index,
      ℛx.left i *
        HMul.hMul (β := A) (HSMul.hSMul.{u, v, v} (α := R) (β := A) ((counit : (a : A) → R) y : R) 1)
          ((antipode R : (a : A) → A) (ℛx.right i) : A))
    (∑ i ∈ ℛx.index,
      ℛx.left i *
        HMul.hMul (α := A) (β := A) ((algebraMap R A : (a : R) → A) ((counit : (a : A) → R) y : R) : A)
          ((antipode R : (a : A) → A) (ℛx.right i) : A))
calc₄ :
  Eq (α := A)
    (∑ i ∈ ℛx.index,
      ℛx.left i *
        HMul.hMul (α := A) (β := A) ((algebraMap R A : (a : R) → A) ((counit : (a : A) → R) y : R) : A)
          ((antipode R : (a : A) → A) (ℛx.right i) : A))
    (∑ i ∈ ℛx.index,
      HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) ((counit : (a : A) → R) y : R) : A)
        (HMul.hMul (β := A) (ℛx.left i) ((antipode R : (a : A) → A) (ℛx.right i) : A)))
calc₅ :
  ∑ i ∈ ℛx.index,
      HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) ((counit : (a : A) → R) y : R) : A)
        (HMul.hMul (β := A) (ℛx.left i) ((antipode R : (a : A) → A) (ℛx.right i) : A)) =
    HMul.hMul (α := A) (β := A) ((algebraMap R A : (a : R) → A) ((counit : (a : A) → R) y : R) : A)
      (∑ i ∈ ℛx.index, HMul.hMul (β := A) (ℛx.left i) ((antipode R : (a : A) → A) (ℛx.right i) : A) : A)
calc₆ :
  HMul.hMul (α := A) (β := A) ((algebraMap R A : (a : R) → A) ((counit : (a : A) → R) y : R) : A)
      (∑ i ∈ ℛx.index, HMul.hMul (β := A) (ℛx.left i) ((antipode R : (a : A) → A) (ℛx.right i) : A) : A) =
    HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) ((counit : (a : A) → R) y : R) : A)
      (HSMul.hSMul.{u, v, v} (α := R) (β := A) ((counit : (a : A) → R) x : R) 1)
calc₇ :
  HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) ((counit : (a : A) → R) y : R) : A)
      (HSMul.hSMul.{u, v, v} (α := R) (β := A) ((counit : (a : A) → R) x : R) 1) =
    HSMul.hSMul (β := A) (HMul.hMul (α := R) (β := R) ((counit : (a : A) → R) x : R) ((counit : (a : A) → R) y : R)) 1
calc₈ :
  HSMul.hSMul (β := A) (HMul.hMul (α := R) (β := R) ((counit : (a : A) → R) x : R) ((counit : (a : A) → R) y : R)) 1 =
    HSMul.hSMul (β := A) (HSMul.hSMul (α := R) (β := R) ((counit : (a : A) → R) y : R) ((counit : (a : A) → R) x : R)) 1
⊢ ∑ y_1 ∈ ℛx.index,
      ∑ x_1 ∈ ℛy.index,
        HMul.hMul (β := A) (ℛx.left y_1 * ℛy.left x_1)
          ((LinearMap.mul' R A : (a : A ⊗[R] A) → A)
              ((TensorProduct.map (antipode R) (antipode R) : (a : A ⊗[R] A) → A ⊗[R] A)
                  (((↑(TensorProduct.comm R A A) : A ⊗[R] A →ₗ[R] A ⊗[R] A) : (a : A ⊗[R] A) → A ⊗[R] A)
                    (ℛx.right y_1 ⊗ₜ[R] ℛy.right x_1)) :
                A ⊗[R] A) :
            A) =
    HSMul.hSMul (β := A) (HSMul.hSMul (α := R) (β := R) ((counit : (a : A) → R) y : R) ((counit : (a : A) → R) x : R)) 1

Tactic:
calc ∑ i ∈ ℛx.index, ∑ j ∈ ℛy.index,
        (ℛx.left i * ℛy.left j) * (antipode R (ℛy.right j) * antipode R (ℛx.right i))
      _ = ∑ i ∈ ℛx.index, ∑ j ∈ ℛy.index,
          ℛx.left i * (ℛy.left j * antipode R (ℛy.right j) * antipode R (ℛx.right i)) := by
        simp [mul_assoc]
      _ = ∑ i ∈ ℛx.index, ℛx.left i *
          ((∑ j ∈ ℛy.index, ℛy.left j * antipode R (ℛy.right j)) * antipode R (ℛx.right i)) := by
        simp [Finset.sum_mul, Finset.mul_sum]
      _ = ∑ i ∈ ℛx.index, ℛx.left i *
          (counit y • 1 * antipode R (ℛx.right i)) := by
        rw [sum_mul_antipode_eq_smul ℛy]
      _ = ∑ i ∈ ℛx.index, ℛx.left i *
          (algebraMap R A (counit y) * antipode R (ℛx.right i)) := by
        simp [Algebra.smul_def]
      _ = ∑ i ∈ ℛx.index, algebraMap R A (counit y) * (ℛx.left i * antipode R (ℛx.right i)) := by
        congr 1; ext i; rw [← mul_assoc, ← mul_assoc, Algebra.commutes]
      _ = algebraMap R A (counit y) * ∑ i ∈ ℛx.index, ℛx.left i * antipode R (ℛx.right i) := by
        rw [← Finset.mul_sum]
      _ = algebraMap R A (counit y) * (counit (R := R) x • (1 : A)) := by
        rw [sum_mul_antipode_eq_smul ℛx]
      _ = (counit (R := R) x * counit y) • (1 : A) := by
        simp only [Algebra.smul_def, mul_one, ← map_mul, mul_comm (counit x)]
      _ = (counit (R := R) y • counit x) • (1 : A) := by
        simp only [smul_eq_mul, mul_comm (counit y)]

Premises used: HMul.hMul, Algebra.algebraMap, CoalgebraStruct.counit, Coalgebra.Repr.index, HSMul.hSMul, OfNat.ofNat, DFunLike.coe