## Stream: new members

### Topic: teaching simp about my structure

#### Jesse Selover (Sep 25 2020 at 20:18):

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 (Sep 25 2020 at 21:36):

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

#### Reid Barton (Sep 26 2020 at 00:14):

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 (Sep 26 2020 at 01:50):

thank you! I will try that

#### Jesse Selover (Sep 26 2020 at 02:31):

Stating the iff in reverse worked!

Last updated: May 15 2021 at 00:39 UTC