Hi. How would you prove `[fset x | x in A & x \in B] = B`

where `B = A `\` C`

and A, B and C are mathcomp.finmap sets?

I imagine one way would be to transform `[fset x | x in A & x \in B]`

into `[fset x | x in B]`

and then use `imfset_id`

.

There must be many ways to do so, but this one seems straightforward enough. Note that `inE`

accomplishes a lot but for some reason prints `k \in mem_fin (fset_finpred A)`

instead of `k \in A`

, which hides the fact that the goal is a simple consequence of the properties of `&&`

at that point (or case analysis, as you prefer).

```
From mathcomp Require Import all_ssreflect finmap.
Open Scope fset.
Lemma foo (K : choiceType) (A C : {fset K}) :
[fset x | x in A & x \in A `\` C] = A `\` C.
Proof.
apply/fsetP => k.
rewrite !inE.
rewrite -[_ \in mem_fin (fset_finpred _)]/(k \in A).
by case: (k \in A); rewrite ?andbF.
Qed.
```

Thank you @Ana de Almeida Borges. After understanding your code I feel like I'm starting to get an intuion on how to bring the goal to a state where `inE`

can be most useful.

You can "shake" the predicate notation down by refolding it, also you can use the idempotency of `&&`

instead of `case`

, rolling the last 3 lines into

`by rewrite !inE /= unfold_in topredE andbCA andbb.`

Last updated: Jul 23 2024 at 21:01 UTC