Prove equality in a record type

Question

I am trying to prove something about monoids an categories. This results in the following (partial) proof:

Require Import UniMath.Algebra.Monoids.
Require Import UniMath.CategoryTheory.Core.Categories.

Unset Universe Checking.

Theorem exercise18 (M: monoid) : category.
Proof.
    destruct M as [[[M misaset] mul] [assoc [e [lunit runit]]]].

    use makecategory.
        exact M.
        exact (λ x z, (hfiber (λ y: M, (mul x y)) z)).
        {
            intros.
            apply (isaset_hfiber _ _ misaset misaset).
        }
        {
            intros x.
            refine (e ,, (runit x)).
        }
        {
            simpl.
            intros x y z [f hf] [g hg].
            refine ((mul f g) ,, _).
            rewrite <- assoc, <- hg, <- hf.
            reflexivity.
        }
        {
            simpl.
            intros x y [f hf].
            assert (heq: mul e f = f).
                {exact (lunit f). }
            rewrite heq.

At the end, the goal is

mul e f,,
internal_paths_rew M (mul (mul x e) f) (λ p : M, p = y)
  (internal_paths_rew M (mul x f) (λ z : M, mul (mul x e) f = z)
     (internal_paths_rew M (mul x e)
        (λ y0 : M, mul (mul x e) f = mul y0 f)
        (idpath (mul (mul x e) f)) x (runit x)) y hf)
  (mul x (mul e f)) (assoc x e f) = f,, hf

Which leads me to ask a couple of questions (tell me if I should ask them separately):

• Is there a tactic which turns a goal about equality of a record type (such as tpair, with notation _ ,, _) into a set of goals, one for each property of the record? Or is there another nice way to show equality?
• What is the internal_paths_rew here?
• The last line, rewrite heq gives an elaborate error:

Abstracting over the term "mul e f" leads to a term
λ p : M,, misaset,
p,,
internal_paths_rew M (mul (mul x e) f) (λ p0 : M, p0 = y)
  (internal_paths_rew M (mul x f) (λ z : M, mul (mul x e) f = z)
     (internal_paths_rew M (mul x e)
        (λ y0 : M, mul (mul x e) f = mul y0 f)
        (idpath (mul (mul x e) f)) x (runit x)) y hf) 
  (mul x p) (assoc x e f) = f,, hf
which is ill-typed.
Reason is: Illegal application: 
The term "internal_paths_rew" of type
 "∏ (A : UU) (a : A) (P : A → Type), P a → ∏ y : A, a = y → P y"
cannot be applied to the terms
 "M" : "UU"
 "mul (mul x e) f" : "pr1hSet (M,, misaset)"
 "λ p : M, p = y" : "M → UU"
 "internal_paths_rew M (mul x f) (λ z : M, mul (mul x e) f = z)
    (internal_paths_rew M (mul x e)
       (λ y : M, mul (mul x e) f = mul y f)
       (idpath (mul (mul x e) f)) x (runit x)) y hf"
   : "mul (mul x e) f = y"
 "mul x p" : "pr1hSet (M,, misaset)"
 "assoc x e f"
   : "(x * e * f)%multmonoid = (x * (e * f))%multmonoid"
The 6th term has type
 "(x * e * f)%multmonoid = (x * (e * f))%multmonoid"
which should be coercible to "mul (mul x e) f = mul x p".

What is happening here? I would expect I'd be able to perform arbitrary rewrites based on equality.