Cardinality of a concrete set

Stream: Is there code for X?

[Janitha]

How do I prove

{13, 17, 35, 45, 63, 65, 85, 91, 15, 21, 39, 51}.ncard = 12

?

[Yaël Dillies]

That would be a good job for a simproc. Unfortunately for you, no one has written that one yet :smile:

[Yakov Pechersky]

import Mathlib

example : Set.ncard {13, 17, 35, 45, 63, 65, 85, 91, 15, 21, 39, 51} = 12 := by
  convert Set.ncard_eq_toFinset_card _ _
  · simp
  · repeat first | apply Set.Finite.insert | simp

[Bhavik Mehta]

import Mathlib

example : Set.ncard {13, 17, 35, 45, 63, 65, 85, 91, 15, 21, 39, 51} = 12 := by
  rw [Set.ncard_eq_toFinset_card']
  rfl

[Bhavik Mehta]

or even more simply,

import Mathlib

example : Set.ncard {13, 17, 35, 45, 63, 65, 85, 91, 15, 21, 39, 51} = 12 := by
  simp [Set.ncard_eq_toFinset_card']

since simp already has all the pieces to do this

[Janitha]

Thank you!