Showing s.card is bounded

Stream: general

[Daniel Garcia]

Hey all, I am wondering how to proceed in the following proof to show that the cardinality of a finite set is bounded. Thanks in advance for the help!

import Mathlib.Tactic
open Finset
example (s : Finset ℕ) (h : ∀ x ∈ s, x < 100) : s.card < 101 := by sorry

[Damiano Testa]

example (s : Finset ℕ) (h : ∀ x ∈ s, x < 100) : s.card < 101 := by
  apply Nat.lt_succ.mpr
  have : 100 = Finset.card (Finset.range 100) := rfl
  rw [this]
  apply Finset.card_mono
  exact fun x hx => mem_range.mpr (h x hx)

[Daniel Garcia]

Thank you so much! That worked! :)

Damiano Testa said:

example (s : Finset ℕ) (h : ∀ x ∈ s, x < 100) : s.card < 101 := by
  apply Nat.lt_succ.mpr
  have : 100 = Finset.card (Finset.range 100) := rfl
  rw [this]
  apply Finset.card_mono
  exact fun x hx => mem_range.mpr (h x hx)

[Kyle Miller]

Here's another way to write it, but it's the same idea.

example (s : Finset ℕ) (h : ∀ x ∈ s, x < 100) : s.card < 101 := by
  have : s ⊆ Finset.range 100 := by
    intro x hx
    simpa using h x hx
  rw [Nat.lt_succ]
  exact Finset.card_mono this

[Damiano Testa]

You can also go the opposite way and hide all possibility of understanding:

example (s : Finset ℕ) (h : ∀ x ∈ s, x < 100) : s.card < 101 :=
  (card_mono fun _ _ => mem_range.mpr (h _ ‹_›)).trans_lt <| Nat.lt_succ.mpr le_rfl