# Zulip Chat Archive

## Stream: new members

### Topic: intersection as a set of subtype

#### Antoine Chambert-Loir (Mar 12 2022 at 18:05):

Under `variables {α : Type*} (s t : set α)`

, what is the proper way to have `s ∩ t`

as a `set ?

I am stuck in proving these 3 lemmas that should be obvious.

```
import data.set.basic
import data.finset.basic
import data.fintype.basic
open_locale classical
variables (α: Type*) [fintype α]
example {s t : set α} : coe '' (coe ⁻¹' t : set s) = t ∩ s :=
subtype.image_preimage_coe s t
example {s t : set α} :
(t ∩ s).to_finset.card = (coe ⁻¹' t : set s).to_finset.card := sorry
example {s : set α} {t : set s} :
t.to_finset.card = ((coe '' t) : set α).to_finset.card := sorry
```

(The first example does not rewrite if I want to apply it to the second one, I get a “motive is not type correct”…)

#### Johan Commelin (Mar 12 2022 at 18:07):

Antoine Chambert-Loir said:

Under

`variables {α : Type*} (s t : set α)`

, what is the proper way to have`s ∩ t`

as a `set ?

Something seems to be missing at the end of this sentence...

#### Antoine Chambert-Loir (Mar 13 2022 at 09:48):

I meant `set s`

.

#### Riccardo Brasca (Mar 13 2022 at 09:57):

If you write

```
import data.set.basic
import data.finset.basic
import data.fintype.basic
open_locale classical
variables (α: Type*) [fintype α]
lemma foo (s t : set α) : coe '' (coe ⁻¹' t : set s) = t ∩ s :=
subtype.image_preimage_coe s t
example {s t : set α} :
(t ∩ s).to_finset.card = (coe ⁻¹' t : set s).to_finset.card :=
begin
rw ← foo s t,
end
example {s : set α} {t : set s} :
t.to_finset.card = ((coe '' t) : set α).to_finset.card := sorry
```

you get a more precise error

```
type mismatch at application
foo ↥s t
term
t
has type
set α
but is expected to have type
set ↥s
```

#### Riccardo Brasca (Mar 13 2022 at 09:58):

In any case you can use `simp_rw`

, that works.

#### Riccardo Brasca (Mar 13 2022 at 10:07):

Ah sorry, `α`

is explicit, so what I wrote doesn't make sense.

#### Riccardo Brasca (Mar 13 2022 at 10:11):

but `simp_rw`

seems to work anyway.

#### Antoine Chambert-Loir (Mar 13 2022 at 10:50):

I update my initial question, since I now can prove these examples,.

However, I found it difficult, and it must be because I missed something.

```
import data.set.basic
import data.finset.basic
import data.fintype.basic
open_locale classical
variables {α: Type*} [fintype α]
example {s t : set α} : coe '' (coe ⁻¹' t : set s) = t ∩ s :=
subtype.image_preimage_coe s t
lemma finset.coe_inj' (ft : finset α) : (ft : set α).to_finset = ft :=
by rw [← finset.coe_inj, set.coe_to_finset]
example {s : set α} {ft : finset s} :
(finset.image coe ft : finset α).card = ft.card :=
finset.card_image_of_inj_on (function.injective.inj_on (subtype.coe_injective) ↑ft)
lemma finset.card_coe {s : set α} {t : set s} :
((coe '' t) : set α).to_finset.card = t.to_finset.card :=
begin
conv_lhs { rw [← set.coe_to_finset t, ← finset.coe_image] },
change (↑(finset.image coe _) : set α).to_finset.card = _,
rw ← finset.card_image_of_inj_on (function.injective.inj_on (subtype.coe_injective) _),
apply congr_arg,
rw ← finset.coe_inj, rw set.coe_to_finset,
end
example {s t : set α} :
(t ∩ s).to_finset.card = (coe ⁻¹' t : set s).to_finset.card :=
begin
suffices : (coe ⁻¹' t : set s).to_finset.card = (coe '' (coe ⁻¹' t : set s)).to_finset.card,
{ rw this,
apply congr_arg,
rw set.to_finset_inj,
rw subtype.image_preimage_coe s t },
rw finset.card_coe,
end
```
```

#### Antoine Chambert-Loir (Mar 13 2022 at 10:51):

Riccardo Brasca said:

You can use

`simp_rw`

, that seems to work.

What do you mean? (I found docs#simp_rw. I need to understand how it can be used here…)

#### Riccardo Brasca (Mar 13 2022 at 10:57):

If `rw [foo]`

gives you "motive is not type correct", you can try `simp_rw [foo]`

. Sometimes it works, meaning that it does what you wanted from `rw`

.

#### Riccardo Brasca (Mar 13 2022 at 11:05):

#### Antoine Chambert-Loir (Mar 13 2022 at 11:26):

Thanks to you, I have a much simpler proof !

```
example {s t : set α} :
(t ∩ s).to_finset.card = (coe ⁻¹' t : set s).to_finset.card :=
begin
simp_rw [← subtype.image_preimage_coe s t],
rw ← finset.card_image_of_inj_on (function.injective.inj_on (subtype.coe_injective) _),
apply congr_arg,
rw [← finset.coe_inj, set.coe_to_finset, finset.coe_image, set.coe_to_finset],
exact classical.dec_eq α,
end
```

A new question arises: why do I now need to appeal explicitly to `classical.dec_eq α`

?…

#### Riccardo Brasca (Mar 13 2022 at 12:12):

I don't understand all the details of `decidable_eq`

, but I noticed that using `open_locale classical`

is often not as good as a "classical" mathematician thinks. I usually write `[decidable_eq α]`

if I need it in the *statements*. If I need it in proof I just use `classical`

. The point is that if you have `open_locale classical`

and you need `decidable_eq α`

in a statement, than the theorem will apply to the `decidable_eq α`

instance provided by choice, and it will not work if there is another instance of `decidable_eq α`

(for example `ℕ`

has its own `decidable_eq`

instance, that is not the one given by choice).

#### Riccardo Brasca (Mar 13 2022 at 12:13):

In your case adding `[decidable_eq α]`

does not suffice, it seems that Lean is then missing some `fintype`

instances, but I am not sure why.

#### Riccardo Brasca (Mar 13 2022 at 12:16):

Ah, it's because Lean wants some `decidable_pred (∈ _)`

.

#### Riccardo Brasca (Mar 13 2022 at 12:25):

I think this proof is better

```
import data.set.basic
import data.finset.basic
import data.fintype.basic
variables {α: Type*} [fintype α] [decidable_eq α]
example {s t : set α} [decidable_pred (∈ t ∩ s)] [decidable_pred (∈ s)]
[decidable_pred (∈ (coe ⁻¹' t : set s))] :
(t ∩ s).to_finset.card = (coe ⁻¹' t : set s).to_finset.card :=
begin
classical,
simp_rw [← subtype.image_preimage_coe s t],
rw ← finset.card_image_of_inj_on (function.injective.inj_on (subtype.coe_injective) _),
apply congr_arg,
rw [← finset.coe_inj, set.coe_to_finset, finset.coe_image, set.coe_to_finset],
apply_instance
end
```

I don't know exactly why we need the last `apply_instance`

, but it must be something related to the order of the elaboration.

#### Antoine Chambert-Loir (Mar 13 2022 at 13:10):

Thanks !

Riccardo Brasca said:

I don't know exactly why we need the last

`apply_instance`

, but it must be something related to the order of the elaboration.

Indeed, my impression is that Lean has less material to guess, it sometimes find such instances by itself.

#### Kevin Buzzard (Mar 13 2022 at 13:17):

`apply`

is normally the guilty party when you end up with random goals which are instances; try changing it to `refine X _ _`

with appropriate number of underscores

#### Antoine Chambert-Loir (Mar 13 2022 at 13:41):

It indeed appeared after `apply congr_arg`

, but `refine congr_arg _ _`

does not help.

(It is on line 1099 of https://github.com/leanprover-community/mathlib/blob/cbfab7e23b9a594a477809e2cae58e9685413c68/acl-sandbox/group_theory/wielandt.lean )

#### Riccardo Brasca (Mar 13 2022 at 13:43):

You can try to write down the fist argument explicitly, but I wouldn't bother too much about it.

#### Antoine Chambert-Loir (Mar 13 2022 at 13:44):

I am so happy that this files now work that I will have some rest!

(This is a formalization of Wielandt's book on Finite permutation groups. I am close to proving a theorem of Jordan.)

Last updated: Dec 20 2023 at 11:08 UTC