intersection as a set of subtype

Stream: new members

[Antoine Chambert-Loir]

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]

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]

I meant set s.

[Riccardo Brasca]

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]

In any case you can use simp_rw, that works.

[Riccardo Brasca]

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

[Riccardo Brasca]

but simp_rw seems to work anyway.

[Antoine Chambert-Loir]

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]

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]

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]

simp_rw

[Antoine Chambert-Loir]

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]

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]

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]

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

[Riccardo Brasca]

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]

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]

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]

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]

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

[Antoine Chambert-Loir]

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