# Zulip Chat Archive

## Stream: Is there code for X?

### Topic: Basic cardinality calculation

#### Bjørn Kjos-Hanssen (Oct 10 2020 at 21:38):

How would I prove that `{n:ℕ | n=5}.to_finset.card = 1`

? From the mathlib docs it didn't seem obvious what the definition of .card is

#### Pedro Minicz (Oct 10 2020 at 21:42):

`simp`

does the job:

```
example : {n : ℕ | n = 5}.to_finset.card = 1 :=
begin
simp
end
```

#### Heather Macbeth (Oct 10 2020 at 21:43):

By the way, did you know you can do `{5}`

rather than `{n : ℕ | n = 5}`

?

#### Pedro Minicz (Oct 10 2020 at 21:43):

By the way, you can use `squeeze_simp`

to see what lemmas `simp`

used to solve the goal:

```
example : {n : ℕ | n = 5}.to_finset.card = 1 :=
begin
--squeeze_simp,
simp only [set.card_singleton, set.set_of_eq_eq_singleton, set.to_finset_card]
end
```

#### Pedro Minicz (Oct 10 2020 at 21:45):

Heather Macbeth said:

By the way, did you know you can do

`{5}`

rather than`{n : ℕ | n = 5}`

?

Indeed, `simp`

was using `set_of_eq_eq_singleton {a : α} : {n | n = a} = {a}`

to turn `{n : ℕ | n = 5}`

into `{5}`

, as lemmas about singleton sets are defined using that notation.

#### Bjørn Kjos-Hanssen (Oct 10 2020 at 21:45):

OK thanks... `simp`

does that but how about `{n:ℕ | n=5 ∨ n=6}.to_finset.card = 2`

#### Heather Macbeth (Oct 10 2020 at 21:50):

Maybe docs#finset.card_eq_succ? (Not a library I know well, though.)

#### Pedro Minicz (Oct 10 2020 at 21:50):

`{n : ℕ | n = 5 ∨ n = 6}.to_finset`

won't work. If you see the definition of `set.to_finset`

the issue becomes clear:

```
#check set.to_finset -- set.to_finset : Π (s : set ?M_1) [_inst_1 : fintype ↥s], finset ?M_1
```

`set.to_finset`

needs an instance of `fintype ↥s`

which cannot be inferred in this case.

#### Pedro Minicz (Oct 10 2020 at 21:51):

In the first case the instance could be inferred because `{n : ℕ | n = 5} = {5}`

and there is an instance for `fintype ↥{x}`

.

#### Pedro Minicz (Oct 10 2020 at 21:55):

You could provide the instance:

```
instance : fintype ↥{n : ℕ | n = 5 ∨ n = 6} :=
sorry
```

but using a different notation is better (because Lean can then infer things):

```
example : ({5, 6} : set ℕ).to_finset.card = 2 :=
sorry
```

#### Pedro Minicz (Oct 10 2020 at 21:55):

`{5, 6} = {n : ℕ | n = 5 ∨ n = 6 ∨ false} = {n : ℕ | n = 5 ∨ n = 6}`

#### Pedro Minicz (Oct 10 2020 at 21:57):

```
example : ({5, 6} : set ℕ).to_finset.card = 2 :=
begin
simp,
refl
end
```

#### Pedro Minicz (Oct 10 2020 at 21:58):

Again, I'd recommend using `squeeze_simp`

and see which lemmas where used. In VSCode you can press F12 to jump to the definition.

#### Bjørn Kjos-Hanssen (Oct 10 2020 at 21:59):

That reduced the goal to `{6}.to_finset.val.card + 1 = 2`

it seems... so now if I prove `{6]}.to_finset.val.card = 1`

we may be getting somewhere

#### Pedro Minicz (Oct 10 2020 at 21:59):

This is true by reflexivity. `{6}.to_finset.val.card`

reduces to `1`

.

#### Pedro Minicz (Oct 10 2020 at 22:00):

I removed `change _ = 1 + 1`

, as it wasn't necessary. Then the goal becomes `{6}.to_finset.val.card + 1 = 2`

and again, `{6}.to_finset.val.card + 1`

reduces to `2`

. They are literally the same term!

#### Bjørn Kjos-Hanssen (Oct 10 2020 at 22:05):

Ah okay, this worked... `example : ({5, 6} : set ℕ).to_finset.card = 2 :=begin refl end`

Thanks @Pedro Minicz and @Heather Macbeth

#### Heather Macbeth (Oct 10 2020 at 22:10):

Also -- `example : ({5, 6} : set ℕ).to_finset.card = 2 := rfl`

:smiley:

#### Bjørn Kjos-Hanssen (Oct 10 2020 at 22:38):

I'd been wondering about the difference between `refl`

and `rfl`

... Also, this is a bit shorter: ```
example : ({5, 6} : finset ℕ).card = 2 :=
rfl
```

#### Heather Macbeth (Oct 10 2020 at 22:38):

`refl`

is a tactic and `rfl`

is a lemma, if you are in the mood for this kind of abstract nonsense.

#### Heather Macbeth (Oct 10 2020 at 22:39):

So `exact rfl`

is the same as `refl`

#### Heather Macbeth (Oct 10 2020 at 22:39):

and `by refl`

or `begin refl end`

are the same as `rfl`

#### Heather Macbeth (Oct 10 2020 at 22:40):

(modulo some subtleties that other people will probably jump in to explain!)

#### Kevin Buzzard (Oct 10 2020 at 22:47):

`refl`

(the tactic) is *slightly* stronger than `rfl`

(the term) because `rfl`

will only prove goals of the form `A = A`

, whereas `refl`

will close any goal of the form `R A A`

if `R`

is a binary relation such that there's a proof of "for all x, R x x" which has been tagged with the `refl`

tag (tactics can look through the library for lemmas and tags, term mode proofs can't). In practice most of the time `refl`

is used to prove `A = A`

(at least for me) but occasionally I use it to prove `x <= x`

or `P <-> P`

#### Kevin Buzzard (Oct 10 2020 at 22:50):

```
def R (a b : ℕ) : Prop := true
@[refl] lemma R.refl : ∀ a, R a a := λ a, trivial
example : R 37 37 :=
begin
refl
end
```

#### Kevin Buzzard (Oct 10 2020 at 22:52):

or even

```
def R (a b : ℕ) : Prop := sorry
@[refl] lemma R.refl : ∀ a, R a a := sorry
example : R 37 37 :=
begin
refl
end
```

#### Kyle Miller (Oct 10 2020 at 23:18):

Are the following instances already in mathlib?

```
instance emptyc.fintype (α : Type*) : fintype ({} : set α) :=
⟨∅, by simp⟩
instance insert.fintype (α : Type*) [decidable_eq α] (x : α) (s : set α) [fintype s] : fintype ↥(insert x s) :=
begin
fsplit,
let emb : s ↪ ↥(insert x s) :=
{ to_fun := λ ⟨a, h⟩, ⟨a, set.mem_insert_of_mem x h⟩,
inj' := λ ⟨a,ha⟩ ⟨b,hb⟩ h, by simpa [insert.fintype._match_1] using h },
have h : x ∈ insert x s := set.mem_insert x s,
exact {⟨x, h⟩} ∪ finset.map emb finset.univ,
rintro ⟨y, hy⟩,
simp only [set.mem_insert_iff] at hy,
rcases hy with ⟨rfl, _⟩,
simp,
simp [insert.fintype._match_1, hy_1],
end
```

#### Kyle Miller (Oct 10 2020 at 23:24):

This makes it so the following can find a `fintype`

instance:

```
example : ({1,2,3} : set ℕ).to_finset.card = 3 :=
begin
sorry,
end
```

#### Bryan Gin-ge Chen (Oct 11 2020 at 00:25):

Yeah, they're both in `data.set.finite`

as src#set.fintype_empty and src#set.fintype_insert:

```
import data.set.finite
example : ({1,2,3} : set ℕ).to_finset.card = 3 := rfl
```

(I found them by going to docs#fintype, expanding the "Instances" and scrolling down to `set.*`

.)

#### Bjørn Kjos-Hanssen (Oct 11 2020 at 02:16):

It seems that `rfl`

(and `begin refl end`

) can do some arithmetic too! For instance:

```
example : 2+2=4 :=
rfl
```

#### Kenny Lau (Oct 11 2020 at 04:27):

I might be wrong, but `rfl`

is a special term, as in it is specially interpreted by the parser / elaborator.

#### Kenny Lau (Oct 11 2020 at 04:28):

as seen from the fact that if you write `rfl`

for something that are not defeq, you get a special error message.

#### Mario Carneiro (Oct 11 2020 at 05:30):

For the most part it's just a term, but theorems of the form `theorem foo : A = B := rfl`

(where the rhs can only be the literal token `rfl`

) are used to mark definitional simp lemmas. It's a little restrictive but I think the idea is to substitute for some `computation foo : A ~> B`

that doesn't otherwise have syntax in lean

#### Bjørn Kjos-Hanssen (Oct 16 2020 at 20:14):

(deleted)

Last updated: May 19 2021 at 02:10 UTC