## 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.

simp_rw

#### 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