teaching simp about my structure

Stream: new members

[Jesse Selover]

Apologies for a rather vague question, but I'm wondering if there is a way to teach lean that only certain parts of my structure matter for equality?
I have a structure which is a combination of another structure and a proof, like:

structure sym_fn (σ : Type*) (α : Type*) :=
(series : mv_power_series σ α)
(series_sym : ∀ (i j : σ) (f : σ →₀ ℕ), series f = series (swap i j f))

And because different proofs of the same thing are equal, I've proved a helper lemma like

lemma series_part (x y : sym_fn σ α) : x.series = y.series ↔ x = y := ...

Is that the appropriate thing to do? Is there a way to teach simp about that? I basically want to be able to infer that sym_fn addition is associative from the fact that mv_power_series addition is...

[Yakov Pechersky]

Try stating the iff in reverse, and supplying that to simp

[Reid Barton]

You can put the ext attribute on your structure, and it will prove your lemma under the name sym_fn.ext and mark it with the ext attribute so that the ext tactic will automatically use it.

[Jesse Selover]

thank you! I will try that

[Jesse Selover]

Stating the iff in reverse worked!