## Stream: new members

### Topic: sets with two elements

#### Damiano Testa (Sep 01 2020 at 14:53):

Dear All,

I have managed to find a very convoluted proof of what I think of as a very simple fact. Can anyone suggest a proof of the lemma below?

I am happy to be embarrassed by showing my proof, although I am not doing it right away, in order not to lead anyone astray... I will post it, if you ask, though!

Thank you very much!

import tactic

lemma card_two {sup : finset ℕ} {H : 2 ≤ sup.card} : finset.min' sup ≠ finset.max' sup :=
begin
sorry,
end


#### Damiano Testa (Sep 01 2020 at 14:54):

(The reason that I would like a shorter proof is that at the moment, Lean times out every time I try to continue with my proofs...)

#### Reid Barton (Sep 01 2020 at 14:59):

I was going to say your lemma doesn't look like it would type check but I guess it actually does.

#### Reid Barton (Sep 01 2020 at 14:59):

Did you really prove it as a top-level lemma in this form?

#### Damiano Testa (Sep 01 2020 at 15:00):

Reid Barton said:

Did you really prove it as a top-level lemma in this form?

I did prove it, but I am not really proud of my proof:

#### Damiano Testa (Sep 01 2020 at 15:00):

lemma card_two {sup : finset ℕ} {H : 2 ≤ sup.card} : finset.min' sup ≠ finset.max' sup :=
begin
intro,
have sne : sup.nonempty,
{
refine finset.card_pos.mp _,
refine lt_of_lt_of_le _ H,
exact two_pos,
},
have ineq : {c : ℕ | ∃ d ∈ sup , d = c} ⊆ {c : ℕ | (finset.min' sup sne) ≤ c ∧ c ≤ (finset.max' sup sne)},
{
intros c chip,
have cinsup : c ∈ sup,
simp only [*, exists_prop, exists_eq_right, finset.set_of_mem, finset.mem_coe] at *,
have clemax : c ≤ finset.max' sup sne,
exact finset.le_max' sup sne c cinsup,
have minlec : finset.min' sup sne ≤ c,
exact finset.min'_le sup sne c cinsup,
simp only [*, and_self, set.mem_set_of_eq] at *,
},
rw a at ineq,
have : {c : ℕ | (finset.max' sup sne) ≤ c ∧ c ≤ (finset.max' sup sne)} = {c : ℕ | c = (finset.max' sup sne)},
{
simp only [exists_prop, set.set_of_eq_eq_singleton, exists_eq_right, finset.set_of_mem] at *,
ext,
split;{simp only [and_imp, set.mem_singleton_iff, set.mem_set_of_eq] at *,omega},
},
rw this at ineq,
simp only [*, exists_prop, set.set_of_eq_eq_singleton, exists_eq_right, finset.set_of_mem] at *,
have consingle : {c : ℕ | ∃ d ∈ sup , d = c} ⊆ {finset.max' sup sne},
simp only [*, exists_prop, exists_eq_right, finset.set_of_mem] at *,
have supfintype : fintype {c : ℕ | ∃ d ∈ sup , d = c},
{
refine set.finite.fintype _,
refine set.finite.subset _ _,
exact {dd : ℕ | ∃ d ∈ sup , d = dd},
simp only [*, exists_prop, exists_eq_right, finset.set_of_mem] at *,
exact finset.finite_to_set sup,
simp only [exists_prop] at *,
},
have supfinite : {c : ℕ | ∃ d ∈ sup , d = c}.finite,
refine set.finite.subset _ _,
exact {dd : ℕ | ∃ d ∈ sup , d = dd},
simp only [*, exists_prop, exists_eq_right, finset.set_of_mem] at *,
exact finset.finite_to_set sup,
simp only [exists_prop] at *,
have supins : sup = supfinite.to_finset,
simp only [exists_prop, finset.finite_to_set_to_finset, exists_eq_right, finset.set_of_mem] at *,
have singlefinite: {d : ℕ | d = sup.max' sne}.finite,
exact set.finite_pure (finset.max' sup sne),
have le : supfinite.to_finset.card ≤ singlefinite.to_finset.card,
{
apply finset.card_le_of_subset,
intros a ah,
refine set.mem_def.mpr _,
refine multiset.mem_map.mpr _,
tidy,
},
let singsing : set ℕ := {finset.max' sup sne},
have singsingfinite : singsing.finite,
exact set.finite_singleton (finset.max' sup sne),
have eq1 : singlefinite.to_finset.card = 1,
{
apply finset.card_eq_one.mpr,
use (finset.max' sup sne),
ext1,
split;
{intros xx,finish,},
},
rw eq1 at le,
have careq : sup.card = supfinite.to_finset.card,
exact congr_arg finset.card supins,
rw ← careq at le,
linarith,
end


#### Damiano Testa (Sep 01 2020 at 15:01):

(I am not sure whether I need more imports for the proof to go through: I produced the mwe with only the statement)
I just checked that there is the need for no other imports.

#### Damiano Testa (Sep 01 2020 at 15:03):

Reid Barton said:

Did you really prove it as a top-level lemma in this form?

Btw, what does "top-level lemma" means?

#### Reid Barton (Sep 01 2020 at 15:04):

Not part of another proof

#### Damiano Testa (Sep 01 2020 at 15:04):

well, this lemma is supposed to be part of another proof... ahahah! so I guess that it is a "bottom-level lemma"!

#### Reid Barton (Sep 01 2020 at 15:11):

Here's a more efficient proof

lemma card_two {α : Type*} {s : finset α} [decidable_linear_order α] {H : 2 ≤ s.card} : finset.min' s ≠ finset.max' s :=
begin
intro h,
have sne : s.nonempty,
{ rw ←finset.card_pos, linarith },
let min := finset.min' s sne,
let max := finset.max' s sne,
have : min = max,
{ dsimp only [min, max], rw h },
have : ∀ x ∈ s, x = min,
{ intros x hx,
apply le_antisymm,
{ rw this,
exact finset.le_max' s sne x hx },
{ exact finset.min'_le s sne x hx } },
have : s.card ≤ 1,
{ rw finset.card_le_one_iff,
intros x y hx hy,
rw [this x hx, this y hy] },
linarith
end


#### Johan Commelin (Sep 01 2020 at 15:12):

finset.le_max' seems to have spurious assumptions.

#### Damiano Testa (Sep 01 2020 at 15:12):

Reid Barton said:

Here's a more efficient proof

Thank you so much!!!

#### Damiano Testa (Sep 01 2020 at 15:12):

I will try to understand why your proof works, but for the moment, I will continue with what I was doing!

#### Reid Barton (Sep 01 2020 at 15:13):

The main step is to guess that something like docs#finset.card_le_one_iff already exists

#### Johan Commelin (Sep 01 2020 at 15:14):

Here is my proof, without looking at the one by Reid. I haven't made golfing attempts yet.

open_locale classical

lemma card_two (sup : finset ℕ) (H : 2 ≤ sup.card) :
finset.min' sup ≠ finset.max' sup :=
begin
contrapose! H,
suffices : sup.card = 0 ∨ sup.card = 1,
{ cases this with h h; rw h; linarith, },
rw or_iff_not_imp_left,
intro h0,
rw finset.card_eq_one,
rw [← ne.def, ← nat.pos_iff_ne_zero, finset.card_pos] at h0,
obtain ⟨x, hx⟩ := h0,
use x,
rw finset.eq_singleton_iff_unique_mem,
refine ⟨hx, _⟩,
rintro i hi,
suffices : ∀ a b, a ∈ sup → b ∈ sup → a ≤ b,
{ apply le_antisymm; solve_by_elim },
rintro a b ha hb,
apply le_trans (sup.le_max' ⟨x, hx⟩ a ha),
rw ← H,
apply sup.min'_le ⟨x, hx⟩ b hb,
end


#### Damiano Testa (Sep 01 2020 at 15:15):

Reid Barton said:

The main step is to guess that something like docs#finset.card_le_one_iff already exists

It always seems to simple, when someone else points it out to me...

#### Sebastien Gouezel (Sep 01 2020 at 15:15):

The assumption is calling to be formulated in terms of nontrivial (which is equivalent to your assumption thanks to docs#fintype.one_lt_card_iff_nontrivial )

#### Damiano Testa (Sep 01 2020 at 15:15):

Reid Barton said:

The main step is to guess that something like docs#finset.card_le_one_iff already exists

What does Type* mean?

#### Johan Commelin (Sep 01 2020 at 15:15):

Golfed

open_locale classical

lemma card_two (sup : finset ℕ) (H : 2 ≤ sup.card) :
finset.min' sup ≠ finset.max' sup :=
begin
contrapose! H,
suffices : sup.card ≤ 1, by linarith,
rw finset.card_le_one_iff,
suffices : ∀ a b, a ∈ sup → b ∈ sup → a ≤ b,
{ intros, apply le_antisymm; solve_by_elim },
rintro a b ha hb,
apply le_trans (sup.le_max' ⟨a, ha⟩ a ha),
rw ← H,
apply sup.min'_le ⟨a, ha⟩ b hb,
end


#### Reid Barton (Sep 01 2020 at 15:16):

Oh, now I understand what you mean about extraneous assumptions

#### Johan Commelin (Sep 01 2020 at 15:16):

Damiano Testa said:

What does Type* mean?

Type _, in other words: "Hey lean, figure out the universe yourself"

#### Damiano Testa (Sep 01 2020 at 15:16):

Johan Commelin said:

Golfed

Wow! This proof is also very short!

#### Damiano Testa (Sep 01 2020 at 15:17):

Johan Commelin said:

Damiano Testa said:

What does Type* mean?

Type _, in other words: "Hey lean, figure out the universe yourself"

Ah, so I can skip introducing universes and go directly to never think about them anymore!

#### Sebastien Gouezel (Sep 01 2020 at 15:17):

No, sorry, nontrivial is for (fin)types, but you're working with a finset.

#### Johan Commelin (Sep 01 2020 at 15:18):

Yup... until you start doing fpqc cohomology (-;

#### Johan Commelin (Sep 01 2020 at 15:19):

@Reid Barton Are you PRing a fix? Otherwise I will do it

#4020

#### Johan Commelin (Sep 01 2020 at 15:26):

@Reid Barton I also finally understand why you were so surprised that this lemma typechecked :face_palm:

#### Damiano Testa (Sep 01 2020 at 15:27):

Reid Barton said:

Here's a more efficient proof

I really like your proof! I see that you went for the minimum, rather than the maximum! Anyway, it was very instructive for me, thanks!

#### Johan Commelin (Sep 01 2020 at 15:31):

@Damiano Testa Here is an evil proof that might satisfy Reid:

lemma card_two (sup : finset ℕ) (H : 2 ≤ sup.card) :
finset.min' sup ≠ finset.max' sup :=
begin
have h0 : 0 < sup.card, by linarith,
rw finset.card_pos at h0,
rw [ne.def, function.funext_iff, not_forall],
use h0,
apply ne_of_lt,
apply finset.min'_lt_max'_of_card,
linarith,
end


#### Damiano Testa (Sep 01 2020 at 15:32):

Johan Commelin said:

Damiano Testa Here is an evil proof that might satisfy Reid:

Ahaha an evil proof!

I was going over your previous one and I find it very clean!

#### Johan Commelin (Sep 01 2020 at 15:33):

lemma card_two (sup : finset ℕ) (H : 2 ≤ sup.card) :
finset.min' sup ≠ finset.max' sup :=
begin
have h0 : sup.nonempty, by { rw ← finset.card_pos, linarith },
rw [ne.def, function.funext_iff, not_forall],
use h0,
apply ne_of_lt,
apply finset.min'_lt_max'_of_card _ _ H,
end


#### Reid Barton (Sep 01 2020 at 15:34):

Johan Commelin said:

Damiano Testa Here is an evil proof that might satisfy Reid:

  apply finset.min'_lt_max'_of_card,


Oh nice

#### Reid Barton (Sep 01 2020 at 15:34):

Presumably this is the statement one actually wants anyways (the inequality of functions is not very convenient)

#### Yakov Pechersky (Sep 01 2020 at 15:58):

If you look at the definition of finset.min'_lt_max'_of_card, you'll see the closely related finset.min'_lt_max', which might be more convenient. Not sure how you showed that the cardinality is 2 or more. Could be that if you're still proving things about disjoint elements, the card-free lemma is simpler to utilize, instead of generating a hypothesis about card that is just for this lemma.

#### Damiano Testa (Sep 01 2020 at 16:19):

Thank you all for the useful lemmas that you found!

#### Bhavik Mehta (Sep 21 2020 at 00:08):

Perhaps I'm missing something, but to me the obvious thing to do here would be:

lemma card_two {sup : finset ℕ} {H : 2 ≤ sup.card} : finset.min' sup ≠ finset.max' sup :=
mt (λ h, congr_fun h _) (ne_of_lt (finset.min'_lt_max'_of_card sup H))


#### Damiano Testa (Sep 21 2020 at 07:49):

@Bhavik Mehta I would like this to be easy, but using your approach, I get the following error:

expected type:
sup: finset ℕ
H: 2 ≤ sup.card
⊢ sup.min' ≠ sup.max'
Messages (2)
mwe.lean:4:21
don't know how to synthesize placeholder
context:
sup : finset ℕ,
H : 2 ≤ sup.card
⊢ sup.nonempty
mwe.lean:4:35
type mismatch at application
sup.min'_lt_max'_of_card H
term
H
has type
2 ≤ sup.card
but is expected to have type
sup.nonempty
/home/damiano/Matematica/Lean/Chevalley01/mwe.lean:4:35: context: switched to simple application elaboration procedure because failed to use expected type to elaborate it, error message
type mismatch, term
?m_3.min'_lt_max'_of_card ?m_4
has type
1 < ?m_2.card → ?m_2.min' ?m_4 < ?m_2.max' ?m_4
but is expected to have type
sup.min' ?m_1 < sup.max' ?m_1


(the underlined bits are the underscore in congr_fun h _and finset)

(deleted)

(deleted)

#### Shing Tak Lam (Sep 21 2020 at 08:00):

@Damiano Testa What Bhavik posted works for me. finset.min'_lt_max'_of_card was changed 15 days ago (#4020), so maybe you need to update mathlib?

#### Kyle Miller (Sep 21 2020 at 08:03):

(Scratch what I said. I wasn't paying attention to what was going on.)

#### Damiano Testa (Sep 21 2020 at 10:09):

Shing Tak Lam said:

Damiano Testa What Bhavik posted works for me. finset.min'_lt_max'_of_card was changed 15 days ago (#4020), so maybe you need to update mathlib?

Thanks: after downloading the new version of mathlib, it works!

Last updated: May 10 2021 at 00:31 UTC