-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.Basic (goal)
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : AddCommMonoid B
inst_3 : Module R A
inst_4 : Module R B
inst_5 : Coalgebra R A
inst_6 : Coalgebra R B
hl :
  ∀ (x : A),
    Eq (α := (A × B) ⊗[R] ((A × B) ⊗[R] (A × B)))
      ((((↑(TensorProduct.assoc R (A × B) (A × B) (A × B)) :
                  (A × B) ⊗[R] (A × B) ⊗[R] (A × B) →ₗ[R] (A × B) ⊗[R] ((A × B) ⊗[R] (A × B))) ∘ₗ
                rTensor (A × B)
                    (coprod (TensorProduct.map (inl R A B) (inl R A B) ∘ₗ comul)
                      (TensorProduct.map (inr R A B) (inr R A B) ∘ₗ comul)) ∘ₗ
                  coprod (TensorProduct.map (inl R A B) (inl R A B) ∘ₗ comul)
                    (TensorProduct.map (inr R A B) (inr R A B) ∘ₗ comul)) ∘ₗ
              inl R A B :
            (a : A) → (A × B) ⊗[R] ((A × B) ⊗[R] (A × B)))
          x :
        (A × B) ⊗[R] ((A × B) ⊗[R] (A × B)))
      (((lTensor (A × B)
                  (coprod (TensorProduct.map (inl R A B) (inl R A B) ∘ₗ comul)
                    (TensorProduct.map (inr R A B) (inr R A B) ∘ₗ comul)) ∘ₗ
                coprod (TensorProduct.map (inl R A B) (inl R A B) ∘ₗ comul)
                  (TensorProduct.map (inr R A B) (inr R A B) ∘ₗ comul)) ∘ₗ
              inl R A B :
            (a : A) → (A × B) ⊗[R] ((A × B) ⊗[R] (A × B)))
          x :
        (A × B) ⊗[R] ((A × B) ⊗[R] (A × B)))
⊢ Eq (α := A × B →ₗ[R] (A × B) ⊗[R] ((A × B) ⊗[R] (A × B)))
    ((↑(TensorProduct.assoc R (A × B) (A × B) (A × B)) :
        (A × B) ⊗[R] (A × B) ⊗[R] (A × B) →ₗ[R] (A × B) ⊗[R] ((A × B) ⊗[R] (A × B))) ∘ₗ
      rTensor (A × B)
          (coprod (TensorProduct.map (inl R A B) (inl R A B) ∘ₗ comul)
            (TensorProduct.map (inr R A B) (inr R A B) ∘ₗ comul)) ∘ₗ
        coprod (TensorProduct.map (inl R A B) (inl R A B) ∘ₗ comul)
          (TensorProduct.map (inr R A B) (inr R A B) ∘ₗ comul))
    (lTensor (A × B)
        (coprod (TensorProduct.map (inl R A B) (inl R A B) ∘ₗ comul)
          (TensorProduct.map (inr R A B) (inr R A B) ∘ₗ comul)) ∘ₗ
      coprod (TensorProduct.map (inl R A B) (inl R A B) ∘ₗ comul) (TensorProduct.map (inr R A B) (inr R A B) ∘ₗ comul))
have hr : ∀ (x : B),
  Eq (α := (A × B) ⊗[R] ((A × B) ⊗[R] (A × B)))
    ((((↑(TensorProduct.assoc R (A × B) (A × B) (A × B)) :
                (A × B) ⊗[R] (A × B) ⊗[R] (A × B) →ₗ[R] (A × B) ⊗[R] ((A × B) ⊗[R] (A × B))) ∘ₗ
              rTensor (A × B)
                  (coprod (TensorProduct.map (inl R A B) (inl R A B) ∘ₗ comul)
                    (TensorProduct.map (inr R A B) (inr R A B) ∘ₗ comul)) ∘ₗ
                coprod (TensorProduct.map (inl R A B) (inl R A B) ∘ₗ comul)
                  (TensorProduct.map (inr R A B) (inr R A B) ∘ₗ comul)) ∘ₗ
            inr R A B :
          (a : B) → (A × B) ⊗[R] ((A × B) ⊗[R] (A × B)))
        x :
      (A × B) ⊗[R] ((A × B) ⊗[R] (A × B)))
    (((lTensor (A × B)
                (coprod (TensorProduct.map (inl R A B) (inl R A B) ∘ₗ comul)
                  (TensorProduct.map (inr R A B) (inr R A B) ∘ₗ comul)) ∘ₗ
              coprod (TensorProduct.map (inl R A B) (inl R A B) ∘ₗ comul)
                (TensorProduct.map (inr R A B) (inr R A B) ∘ₗ comul)) ∘ₗ
            inr R A B :
          (a : B) → (A × B) ⊗[R] ((A × B) ⊗[R] (A × B)))
        x :
      (A × B) ⊗[R] ((A × B) ⊗[R] (A × B)))
Tactic: ext x : 2