sq_abs

Stream: new members

[Julia Ramos Alves]

I have another simple problem but I don't know how to solve it. For this following lemma:

lemma rhs (x: ℝ): (2 * real.pi)⁻¹ * ∫ x in 0 .. (2 * real.pi), (|x|) ^ 2 =
 (real.pi)^2 / 3 :=

I'm trying to use rw sq_abs, so that I can solve it with rw integral_pow,

But I'm getting the following error:

  |?m_3| ^ 2````

Can someone help me identify what's wrong?

[Julia Ramos Alves]

Excuse me for the mistake, the error is "rewrite tactic failed, did not find instance of the pattern in the target expression
|?m_3| ^ 2"

[Anne Baanen]

Looks like this is because rw isn't always able to rewrite under a binder (i.e. inside an expression like ∫ x that introduces a new variable). You could try tactic#simp_rw or simp only instead of rw.

[Yaël Dillies]

It's under a "binder", namely ∫, so rw is not quite powerful enough. Try simp_rw sq_abs.