Showing t.card < s.card

Stream: general

[Daniel Garcia]

I am having some trouble finding a relevant theorem in Mathlib to establish that the cardinality of a finite set t is less than a finite set s. I would appreciate any suggestions! Thank you in advance.

import Mathlib.Tactic
open Finset
def s : Finset ℤ  := {1, -2, 2}
def t: Finset ℤ := {1, 4}
example: t.card < s.card := by sorry

[Riccardo Brasca]

by decide should work.

[Riccardo Brasca]

In general such completely explicitly results, where the math proof is "just look", can be proved using decide.

[Daniel Garcia]

Thank you! I appreciate the math analogy. Do you have any suggestions for how I would show this for when the result is less obvious? I am doing this smaller example to prepare for a bigger proof

Riccardo Brasca said:

by decide should work.

[Riccardo Brasca]

In general you should try to follow the math proof you have.

[Riccardo Brasca]

It's difficult to give an advice without knowing what makes your theorem not obvious but doable.

[Daniel Garcia]

Fair enough! I appreciate the guidance

[Riccardo Brasca]

For example in your case you can compute the cardinality by hand, using docs#Finset.card_insert_of_not_mem

[Yaël Dillies]

You can also try by simp [s, t] for a proof that's more robust to the decidability of the ground set (here ℤ)

[Kevin Buzzard]

I think there is no quick and easy explanation for what to do in lean when "it's obvious" in maths. The reason is that there are so many different ways that a thing can be obvious. There is an art to understanding all these various reasons and knowing exactly which algorithm will prove your obvious thing. For example I bet decide won't work if the numbers in question were the same numbers but real. And to a mathematician the questions look identical.

[Riccardo Brasca]

With real numbers Lean would probably complain already in the definition of the two sets...

[Riccardo Brasca]

Here is the proof with real numbers, to give an idea of what can be done.

import Mathlib
open Finset
noncomputable
def s : Finset ℝ  := {1, -2, 2}
noncomputable
def t: Finset ℝ := {1, 4}

example: t.card < s.card := by
  simp [s, t]
  convert_to 2 < 3
  · rw [Finset.card_insert_of_not_mem]
    · simp
    · simp; norm_num
  · norm_num

[Riccardo Brasca]

Note that simp is smart enough to compute the cardinality of {1,4}, but not of the other set.