I got a goal like this which says given a set `{set A+B}`

in which all elements are value like `inr _`

, the set given by `inl @^-1`

would be empty.

```
From mathcomp Require Import all_ssreflect.
Goal forall {A B: finType} (b: {set B}),
(* inl @^-1: ((inr (A:=A)) @: b) = set0. *)
inl @^-1: [set (inr (A:=A)) x | x in b] = set0.
Proof.
move => A B b.
(*
1 subgoal
A, B : finType
b : {set B}
========================= (1 / 1)
inl @^-1: [set inr x | x in b] = set0
*)
Search (_ @^-1: _).
```

How can we proceed from here?

Couldn't figure out a suitable lemma with the `Search`

.

to show that two sets are equal, you can use `apply/setP`

.

Thanks. Made some progress with it:

```
Lemma foo1: forall {A B: finType} (b: {set B}),
inl @^-1: ((inr (A:=A)) @: b) = set0.
(* inl @^-1: [set (inr (A:=A)) x | x in b] = set0. *)
Proof.
move => A B b.
apply/setP => //= x.
rewrite !in_set.
(*
1 subgoal
A, B : finType
b : {set B}
x : A
========================= (1 / 1)
(inl x \in [set inr x | x in b]) = false
*)
Search (_ \in _).
```

Rewriting with `unfold_in`

reduces it to `[set inr x | x in b] (inl x) = false`

but was not sure if that's the way to go..

apply/negbTE changes the goal with better notations

and then you want to look at `imsetP`

because you are dealing with the image of a set

Could do it!

Not sure if I'm doing it in a proper way, though..

```
Lemma bar: forall {A B: Type} (a: A) (b: B),
inl (B:=B) a = inr (A:=A) b -> False.
Proof.
move => A B a b.
move => H.
inversion H.
Qed.
Lemma foo1: forall {A B: finType} (b: {set B}),
inl @^-1: ((inr (A:=A)) @: b) = set0.
Proof.
move => A B b.
apply/setP => //= x.
rewrite !in_set.
apply/negbTE/imsetP => [[eb]] => _.
by apply: bar.
Qed.
```

Is use of `inversion`

more of a non-ssreflect style?

```
From mathcomp Require Import all_ssreflect.
Goal forall {A B: finType} (b: {set B}),
(* inl @^-1: ((inr (A:=A)) @: b) = set0. *)
inl @^-1: [set (inr (A:=A)) x | x in b] = set0.
Proof.
move => A B b.
apply/setP => x.
rewrite !inE.
apply/negbTE.
apply/imsetP.
by case.
Qed.
```

you don't need no inversion because the "inl = inr" hypo is already contradictory

Thanks!. Hadn't realized it can figure out the `inl _ = inr _`

being a contradiction by itself.

Did it separately because once I need to derive `a=b`

from `inl a = inl b`

. It didn't seem able to figure it out by itself then (or more likely, I didn't use some ssreflect feature).

I had also been trying to prove this:

```
Lemma foo2: forall {A B: finType} (a: {set B}),
(* a = inl @^-1: ((inl (B:=B)) @: a). *)
a = inl @^-1: [set (inl (B:=B)) x | x in a].
Proof.
move => A B a.
apply/setP => //= x.
rewrite inE.
(*
1 subgoal
A, B : finType
a : {set B}
x : B
========================= (1 / 1)
(x \in a) = (inl x \in [set inl x0 | x0 in a])
*)
```

Is there some lemma that can help? I did a few `Search`

-es, but couldn't spot any.

Maybe `mem_imset`

(found with `Search imset mem`

, or more easily with `Search (_ _ \in imset _ _)`

but that requires knowing what the notation hides).

`mem_imset`

helped!

But I kind of ended up doing things a bit 'manually'..

```
Lemma inl_inj {A B: Type}: injective (rT:=A+B) inl.
Proof. by rewrite /injective => ? ?; case. Qed.
Lemma foo2: forall {A B: finType} (a: {set A}),
a = inl @^-1: [set (inl (B:=B)) x | x in a].
Proof.
move => A B a.
apply/setP => //= x.
rewrite finset.inE.
symmetry.
exact: (mem_imset (aT:=A) (rT:=A+B)%type inl a x inl_inj).
Qed.
```

Could there be a better way to do this?

You should not have to write `finset.`

, and you should be able to rewrite `mem_imset`

just after `inE`

.

Last updated: Jul 25 2024 at 15:02 UTC