sets with two elements

Stream: new members

[Damiano Testa]

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]

(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]

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

[Reid Barton]

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

[Damiano Testa]

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]

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]

(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]

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]

Not part of another proof

[Damiano Testa]

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

[Reid Barton]

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]

finset.le_max' seems to have spurious assumptions.

[Damiano Testa]

Reid Barton said:

Here's a more efficient proof

Thank you so much!!!

[Damiano Testa]

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

[Reid Barton]

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

[Johan Commelin]

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]

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]

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]

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]

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]

Oh, now I understand what you mean about extraneous assumptions

[Johan Commelin]

Damiano Testa said:

What does Type* mean?

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

[Damiano Testa]

Johan Commelin said:

Golfed

Wow! This proof is also very short!

[Damiano Testa]

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]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Reid Barton]

Go ahead

[Johan Commelin]

#4020

[Johan Commelin]

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

[Damiano Testa]

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]

@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]

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]

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]

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]

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

[Yakov Pechersky]

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]

Thank you all for the useful lemmas that you found!

[Bhavik Mehta]

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]

@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
Additional information:
/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)

[Kyle Miller]

(deleted)

[Kyle Miller]

(deleted)

[Shing Tak Lam]

@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]

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

[Damiano Testa]

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!