card of subtype of fintype

Stream: Is there code for X?

[David Renshaw]

I'm having difficulty proving foo:

import Mathlib.Data.Fintype.Card
import Mathlib.Data.Finite.Basic

inductive Color : Type where
| red : Color
| blue : Color

theorem foo
    {α : Type} [DecidableEq α] [Fintype α] (n : ℕ) (hs : Fintype.card α = 0)
    : @Fintype.card
       { a : Finset α // (λ s ↦ Color.red) a = Color.red } (Fintype.ofFinite _) = 1 := by
  sorry

It seems like this should be easy -- given a type of cardinality 1, the trivial subtype that takes every element should also have cardinality 1.
But there seem to be issues about definitional equality among various typeclass instances.

[Eric Wieser]

What's the reason for the Fintype.ofFinite there?

[Eric Wieser]

Isn't the LHS 2 not 1, since there are $2^1$ sets?

[David Renshaw]

oops

[David Renshaw]

corrected -- I meant that Fintype.card α = 0.

[David Renshaw]

so there is $2^0 = 1$ set

[David Renshaw]

The Fintype.ofFinite is needed because if I don't explicitly provide an instance I get

failed to synthesize instance
  Fintype { a // (fun s => Color.red) a = Color.red }

[Kyle Miller]

You can derive a DecidableEq instance to clean up that Fintype.card:

inductive Color : Type where
  | red : Color
  | blue : Color
  deriving DecidableEq

theorem foo
    {α : Type} [DecidableEq α] [Fintype α] (n : ℕ) (hs : Fintype.card α = 0) :
    Fintype.card { a : Finset α // (λ s ↦ Color.red) a = Color.red } = 1 := by
  sorry

[David Renshaw]

ok, so simpler version:

import Mathlib.Data.Fintype.Card
import Mathlib.Data.Finite.Basic

inductive Color : Type where
| red : Color
| blue : Color
deriving DecidableEq

theorem foo'
    {α : Type} [DecidableEq α] [Fintype α] (hs : Fintype.card α = 1)
    : Fintype.card
       { a : α // (λ s ↦ Color.red) a = Color.red } = 1 := by
  sorry

[Kyle Miller]

Here's a horrible proof that's at least a proof:

theorem foo
    {α : Type} [DecidableEq α] [Fintype α] (n : ℕ) (hs : Fintype.card α = 0) :
    Fintype.card { a : Finset α // (λ s ↦ Color.red) a = Color.red } = 1 := by
  simp
  convert_to Fintype.card Set.univ = 1
  simp only [Fintype.card_ofFinset, Finset.mem_univ, forall_true_left, forall_const,
    Finset.filter_true_of_mem]
  convert_to Fintype.card (Finset α) = 1
  simp [hs]

[Eric Wieser]

For the simpler one:

theorem foo'
    {α : Type} [DecidableEq α] [Fintype α] (hs : Fintype.card α = 1)
    : Fintype.card
       { a : α // (λ s ↦ Color.red) a = Color.red } = 1 := by
  simpa [Fintype.card_subtype, Finset.card_univ]

[David Renshaw]

The big stumbling block for me here was the deriving DecidableEq.

[Kevin Buzzard]

(two $$ for LaTeX btw)