## Stream: maths

### Topic: proving size at least 3

#### Kevin Buzzard (Aug 13 2018 at 10:35):

I would be interested in a relatively slick proof of either of the below examples:

import data.fintype
import set_theory.cardinal

-- fintype
open fintype
example (α : Type) [fintype α] (a b c : α) (Hab : a ≠ b) (Hbc : b ≠ c) (Hac : a ≠ c) :
card α ≥ 3 := sorry

-- general
example (α : Type) (a b c : α) (Hab : a ≠ b) (Hbc : b ≠ c) (Hac : a ≠ c) :
cardinal.mk α ≥ 3 := sorry


This is for pedagogical purposes and I don't really mind if we stick to fintypes or not.

As a side issue, is cardinal.mk really the way to talk about the cardinality of a type? Is there not some interface function?

#### Mario Carneiro (Aug 13 2018 at 10:38):

cardinal.mk is the interface function

#### Kenny Lau (Aug 13 2018 at 10:58):

import data.fintype
import set_theory.cardinal

@[derive decidable_eq]
inductive three : Type
| A : three
| B : three
| C : three

open three

instance : fintype three :=
{ elems := {A, B, C},
complete := λ x, by cases x; simp }

theorem three.cardinal : cardinal.mk three = 3 :=
(cardinal.fintype_card three).trans $show ((3 : nat) : cardinal) = 3, by simp -- fintype open fintype example (α : Type) [fintype α] (a b c : α) (Hab : a ≠ b) (Hbc : b ≠ c) (Hac : a ≠ c) : card α ≥ 3 := show card three ≤ card α, from card_le_of_injective (λ n, three.rec_on n a b c)$
λ x y h, by cases x; cases y; dsimp at h; cc

-- general
example (α : Type) (a b c : α) (Hab : a ≠ b) (Hbc : b ≠ c) (Hac : a ≠ c) :
cardinal.mk α ≥ 3 :=
three.cardinal ▸ nonempty.intro ⟨λ n, three.rec_on n a b c,
λ x y h, by cases x; cases y; dsimp at h; cc⟩


#### Mario Carneiro (Aug 13 2018 at 10:58):

hm, I needed some additional library functions for this, attached. The main proof is not so hard:

@[simp] lemma fintype.card_coe (s : finset α) :
fintype.card (↑s : set α) = s.card := card_attach

theorem card_le_of_finset {α} (s : finset α) :
(s.card : cardinal) ≤ cardinal.mk α :=
begin
rw (_ : (s.card : cardinal) = cardinal.mk (↑s : set α)),
{ exact ⟨function.embedding.subtype _⟩ },
rw [cardinal.fintype_card, fintype.card_coe]
end

-- fintype
open fintype
example (α : Type) [fintype α] (a b c : α) (Hab : a ≠ b) (Hbc : b ≠ c) (Hac : a ≠ c) :
card α ≥ 3 :=
finset.card_le_of_subset (finset.subset_univ ⟨a::b::c::0, by simp *⟩)

-- general
example (α : Type) (a b c : α) (Hab : a ≠ b) (Hbc : b ≠ c) (Hac : a ≠ c) :
cardinal.mk α ≥ 3 :=
begin
suffices : ((3:ℕ) : cardinal) ≤ cardinal.mk α, {simpa},
exact card_le_of_finset ⟨a::b::c::0, by simp *⟩
end


#### Kenny Lau (Aug 13 2018 at 10:58):

just 3 seconds apart!

#### Kevin Buzzard (Aug 13 2018 at 18:33):

Thanks to both of you! [I've only just seen these].

#### Kevin Buzzard (Aug 13 2018 at 22:15):

This is one of those "easy in maths, hard in Lean" moments :-/ I am going to need stuff like "card X = 3 iff there exists a,b,c all distinct and every element of X must be a, b or c" [but I've gotta scoot]. I think I can take it from here but this is all a bit ugly. Mathematicians are so good at 3 :-/

#### Mario Carneiro (Aug 14 2018 at 02:04):

that latter fact is essentially exactly the definition of a fintype instance where the underlying multiset has three elements

#### Kevin Buzzard (Aug 14 2018 at 19:36):

Here's a proof for the cardinal case:

import set_theory.cardinal

lemma three (α : Type) (Hthree : cardinal.mk α = 3) :
∃ a b c : α, a ≠ b ∧ b ≠ c ∧ c ≠ a ∧ ∀ d : α, d = a ∨ d = b ∨ d = c :=
begin
rw ←(show cardinal.mk (fin 3) = 3, by simp) at Hthree,
cases (quotient.exact Hthree) with Hequiv,
let a := Hequiv.symm 0,let b := Hequiv.symm 1,let c := Hequiv.symm 2,
have H12 : a ≠ b := by simp [Hequiv];exact dec_trivial,
have H23 : b ≠ c := by simp [Hequiv];exact dec_trivial,
have H31 : c ≠ a := by simp [Hequiv];exact dec_trivial,
existsi a,existsi b,existsi c,
refine ⟨H12,H23,H31,λ d,_⟩,
cases H : (Hequiv d) with n Hn,
cases n with e He,
left,show d = Hequiv.symm ⟨0,Hn⟩,rw ←H,simp,
cases e with e He,
right,left,show d = Hequiv.symm ⟨1,Hn⟩,rw ←H,simp,
cases e with e He,
right,right,show d = Hequiv.symm ⟨2,Hn⟩,rw ←H,simp,
exfalso,apply not_le_of_gt Hn,exact dec_trivial,
end


Now I need to do four :cry: (but that's the last one)

#### Mario Carneiro (Aug 14 2018 at 19:37):

noo... my heart, it hurts

#### Mario Carneiro (Aug 14 2018 at 19:38):

n is easier than 3

#### Kevin Buzzard (Aug 14 2018 at 19:39):

So 4 is easier than 3? :-)

#### Mario Carneiro (Aug 14 2018 at 19:39):

3 is easier than 3

#### Kevin Buzzard (Aug 14 2018 at 19:41):

I did think about doing the general case but at the end of the day I want to extract exactly those things in the conclusion, and I wasn't entirely sure how easy it would be if I had a list of size n or whatever, so I decided to bite the bullet now rather than later.

#### Mario Carneiro (Aug 14 2018 at 19:41):

trust me, it's way easier to conclude from the general statement, even if the final goal is exactly the statement you wrote

#### Mario Carneiro (Aug 14 2018 at 19:42):

hint: if you have a list of length 3, then you can match it against [a, b, c]

#### Kevin Buzzard (Aug 14 2018 at 19:42):

I was a bit surprised to see simp leave me with a goal not 0 = 1 in the H12 proof.

#### Mario Carneiro (Aug 14 2018 at 19:43):

and d \in [a, b, c] and list.nodup [a, b, c] will simplify to the disjunctions you wrote

#### Kevin Buzzard (Aug 14 2018 at 19:43):

This is the stupid cardinal version, because Richard Thomas complained that I was assuming unnecessary finiteness hypotheses.

#### Mario Carneiro (Aug 14 2018 at 19:44):

there are theorems showing equivalence to the finite versions in cardinal

#### Kevin Buzzard (Aug 14 2018 at 19:44):

Oh OK, maybe I'll take it from here. Thanks!

#### Kevin Buzzard (Aug 14 2018 at 19:45):

It's just my lack of experience which made me do the 3 case explicitly. I could see I could try for the n case, but I figured that doing the 3 case directly would be less painful. I guess your instincts immediately told you otherwise.

#### Mario Carneiro (Aug 14 2018 at 19:46):

even 2 is sometimes tricky, but certainly 2 < n < 3

Last updated: May 12 2021 at 07:17 UTC