conv in sum

Stream: general

[Morenikeji Neri]

I would like to show

finset.sum finset.univ  (λ (μ : S n), e (ρ.to_fun) * e (μ.to_fun) * finset.prod finset.univ (λ (i : fin n), A (μ.to_fun i) i)) = finset.sum finset.univ
      (λ (μ : S n), e (ρ.to_fun) * (e (μ.to_fun) * finset.prod finset.univ (λ (i : fin n), A (μ.to_fun i) i)))

where multiplication is in a comm_ring hence is associative, however I cannot use conv as it cannot synthesis μ.to_fun as it is a function. Any tips?

[Morenikeji Neri]

all sorted

[Simon Hudon]

I recommend you make a minimal working example so that people can have a look inside of a Lean session.

I think congr' 1, ext, rw mul_assoc could help.