## Stream: new members

### Topic: Finsets and fintypes

#### Donald Sebastian Leung (Apr 29 2020 at 04:29):

Is there a mathlib lemma that says if I can construct a finset α with cardinality n then fintype.card α ≥ n?

#### Reid Barton (Apr 29 2020 at 04:30):

I doubt it, but I am sure there are lemmas that say things like every finset is a subset of finset.univ and finset.card preserves order and finset.univ.card equals fintype.card.

#### Jalex Stark (Apr 29 2020 at 14:05):

example
{α : Type*} {X : finset α} {n : ℕ} [fintype α] (hX : finset.card X = n)
:  fintype.card α ≥ n := begin
rw ← hX,
apply finset.card_le_of_subset,
refine finset.subset_univ X,
end


#### Kenny Lau (Apr 29 2020 at 14:06):

example {α : Type*} {X : finset α} {n : ℕ} [fintype α] (hX : finset.card X = n) :  fintype.card α ≥ n :=
hX ▸ finset.card_le_of_subset $finset.subset_univ X  #### Jalex Stark (Apr 29 2020 at 14:08): just to check my understanding, your proof is more-or-less a mechanical translation of my tactic script into a single term? (do you think it runs noticeably faster?) #### Kenny Lau (Apr 29 2020 at 14:08): yes; no #### Kevin Buzzard (Apr 29 2020 at 14:42): I think that there is some overhead for entering tactic mode and some more overhead by using the rewrite command; I've noticed slowdown in scripts which use a lot of rewrites. I would be interested to know how much faster term mode is; in some sense the best argument for writing stuff in term mode is that it's faster (because it's also less readable, harder to debug, harder to write...) #### Kevin Buzzard (Apr 29 2020 at 15:16): I created files which were just 10,000 copies of the term proof and the tactic proof: import data.fintype.basic example {α : Type*} {X : finset α} {n : ℕ} [fintype α] (hX : finset.card X = n) : fintype.card α ≥ n := hX ▸ finset.card_le_of_subset$ finset.subset_univ X
example {α : Type*} {X : finset α} {n : ℕ} [fintype α] (hX : finset.card X = n) :  fintype.card α ≥ n :=
hX ▸ finset.card_le_of_subset $finset.subset_univ X example {α : Type*} {X : finset α} {n : ℕ} [fintype α] (hX : finset.card X = n) : fintype.card α ≥ n := hX ▸ finset.card_le_of_subset$ finset.subset_univ X
...


and

import data.fintype.basic

example
{α : Type*} {X : finset α} {n : ℕ} [fintype α] (hX : finset.card X = n)
:  fintype.card α ≥ n := begin
rw ← hX,
apply finset.card_le_of_subset,
refine finset.subset_univ X,
end
example
{α : Type*} {X : finset α} {n : ℕ} [fintype α] (hX : finset.card X = n)
:  fintype.card α ≥ n := begin
rw ← hX,
apply finset.card_le_of_subset,
refine finset.subset_univ X,
end
...


and here are the timings:

buzzard@bob:~/lean-projects/xena/src/term_v_tactic$date; lean --make tactic10000.lean; date Wed 29 Apr 16:13:54 BST 2020 Wed 29 Apr 16:14:58 BST 2020 buzzard@bob:~/lean-projects/xena/src/term_v_tactic$ date; lean --make term10000.lean; date
Wed 29 Apr 16:15:05 BST 2020
Wed 29 Apr 16:15:11 BST 2020

#### Kevin Buzzard (Apr 29 2020 at 15:56):

Boy that's a lot of errors

Somehow after exact you can't use $. I never understood why not. You seem to be able to use everything else. #### Kevin Buzzard (Apr 29 2020 at 15:58): $ date; lean --make byexactterm10000.lean; date
Wed 29 Apr 16:58:00 BST 2020
Wed 29 Apr 16:58:20 BST 2020


#### Reid Barton (Apr 29 2020 at 16:02):

So by exact already incurs 1/3 the cost

#### Reid Barton (Apr 29 2020 at 16:02):

and you have three tactics :thinking:

#### Reid Barton (May 03 2020 at 10:52):

Donald Sebastian Leung said:

Is there a mathlib lemma that says if I can construct a finset α with cardinality n then fintype.card α ≥ n?

Also I just found out why you asked this :upside_down:

#### Reid Barton (May 03 2020 at 10:52):

I think a more naturally-phrased form of this lemma would be good for mathlib

Last updated: May 12 2021 at 22:15 UTC