Prove Finset has cardinality 1

Stream: new members

[Nathan]

example (s : Finset ℕ) (a : ℕ) (h : a ∈ s) : {x ∈ s | x = a}.card = 1 := sorry

How do you prove this? I tried proving {x ∈ s | x = a} = {a}, but no luck

[Yongxi Lin (Aaron)]

If you can prove {x ∈ s | x = a} = {a}, then I believe simp should give you result. To prove {x ∈ s | x = a} = {a}, you can use the ext tactic.

[Kyle Miller]

I guessed that there would be a Finset.card_filter lemma, then simp turned out to basically prove it.

import Mathlib

example (s : Finset ℕ) (a : ℕ) (h : a ∈ s) : {x ∈ s | x = a}.card = 1 := by
  rw [Finset.card_filter]
  simp
  assumption

The proof can be compressed to simp [Finset.card_filter, h].

[Nathan]

thanks!

[Nathan]

Why does this work though? Finset.card_filter changes it to a sum, why is that better?

[Ruben Van de Velde]

If you replace simp by simp?, it shows what lemmas were used:

simp only [Finset.sum_ite_eq', ite_eq_left_iff, zero_ne_one, imp_false, Decidable.not_not]

[Ruben Van de Velde]

So notably docs#Finset.sum_ite_eq' shows there's at most one term that contributes to the sum

[Nathan]

oh yeah that would do it

[Nathan]

it should be possible with ext too, right? i was struggling to show a ∈ {a}. maybe i'll take another look

[Matt Diamond]

i was struggling to show a ∈ {a}

you can use docs#Finset.mem_singleton_self if you're talking about Finset singletons (there's a separate lemma for sets)

[Nathan]

thanks!

[Nathan]

can simp and rw be used on the constants in the context, or only on the goal?

[Robin Arnez]

simp ... at <hypothesis>, rw ... at <hypothesis> for hypothesis in the context.

[Nathan]

oh awesome

[Nathan]

example (s : Finset ℕ) (a : ℕ) (h : a ∈ s) : {x ∈ s | x = a}.card = 1 :=
  have : {x ∈ s | x = a} = {a} := by
    ext t
    apply Iff.intro
    · intro ts
      simp at ts
      rw [ts.right]
      exact Finset.mem_singleton_self a
    · intro ta
      simp at ta
      simp
      sorry
  sorry

getting there... am i on the right track?

[Aaron Liu]

you can just simp it

import Mathlib

example (s : Finset ℕ) (a : ℕ) (h : a ∈ s) : {x ∈ s | x = a}.card = 1 := by
  have : {x ∈ s | x = a} = {a} := by
    simp [Finset.ext_iff, h]
  rw [this]
  rfl

[Nathan]

:astonished:

[Ruben Van de Velde]

rfl there is not great, especially given that docs#Finset.card_singleton is right there

[Nathan]

the thing i've been thinking about regarding tactics is, when changes are made it could break people's code

[Nathan]

why do you have to open classical to use excluded middle, but not for Nat.lt_trichotomy?

[Nathan]

i'm working on a proof that's currently 241 lines, which i fully expect to be reduced to like 20 lines if someone takes a look at it :joy:

[Nathan]

thanks for the tip earlier, Aaron

[Matt Diamond]

I don't think you have to open classical to use excluded middle

[Matt Diamond]

you can just use docs#em ... it uses choice under the hood, but you don't have to open classical to take advantage of that

[Kenny Lau]

Nathan said:

why do you have to open classical to use excluded middle, but not for Nat.lt_trichotomy?

the first part is not true, but the second part is because you can prove that particular instance of excluded middle without using the axiom

[Kenny Lau]

when we say choiceless lean rejects excluded middle, it doesn't mean every instance of excluded middle is literally false; some instances can still be proved

[Kenny Lau]

what open Classical does is enable if then else for any condition