opening the square

Stream: Is there code for X?

[Alex Kontorovich]

Any idea why this isn't working?... Thanks!

import algebra.group.defs
import data.finset.basic
import algebra.big_operators.ring

universes u v

open_locale big_operators

lemma open_square {α : Type u} {β : Type v} [add_comm_monoid β] [has_mul β] [has_pow β ℕ] [monoid β]
  (s : finset α) (f : α → β) :
(∑ i in s, f i)^2 = ∑ i in s, ∑ j in s, (f i) * (f j) :=
begin
  rw pow_two (∑ i in s, f i),
  sorry,
end

[Yaël Dillies]

Not solving your problem, but I'll let you know about docs#finset.sum_mul_sum

[Adam Topaz]

What are your imports?

[Adam Topaz]

The issue is probably the rewrite under a binder... try simp_rw instead of rw

[Adam Topaz]

Oh maybe not

[Alex Kontorovich]

Sorry, added imports

[Eric Rodriguez]

oh! why do you give has_pow b nat?

[Eric Rodriguez]

there's two instances of has_pow on b, one from that and one from the monoid

[Alex Kontorovich]

I thought it wanted that..?

[Alex Kontorovich]

Ah, maybe that's my problem...?

[Alex Kontorovich]

Yep, that did it. Thanks!

[Eric Rodriguez]

(the has_mul instance will also cause you issues - most structures like rings and stuff are bundled, meaning you don't require a pre-existing has_mul/has_add etc instance)

[Alex Kontorovich]

I see, thanks; I was adding them in the order that Lean seemed to want them, not knowing which to remove after adding the next...

[Adam Topaz]

Probably!