Showing that a structure is `Fintype`

Stream: general

[Andrej Bauer]

What is the least painful way to show in Lean 4 that a structure whose components are Fintype is itself Fintype? A concrete example of interest:

structure Cow (n : ℕ) : Type :=
  fst : Fin n
  snd : Fin fst

[Kyle Miller]

Once mathlib4#3198 is merged, the answer will be

structure Cow (n : ℕ) : Type :=
  fst : Fin n
  snd : Fin fst
  deriving Fintype

That PR is fairly self-contained if you want to use it locally. It depends on some mathlib Fintype instances that are already in Mathlib.Data.Fintype.

[Kyle Miller]

Here's essentially what the derive handler is doing in this case:

import Mathlib.Data.Fintype.Sigma

structure Cow (n : ℕ) : Type :=
  fst : Fin n
  snd : Fin fst

def Cow.proxyEquiv (n : ℕ) : (fst : Fin n) × Fin fst ≃ Cow n where
  toFun z := ⟨z.1, z.2⟩
  invFun c := ⟨c.fst, c.snd⟩
  left_inv := fun _ => rfl
  right_inv := fun _ => rfl

instance : Fintype (Cow n) :=
  Fintype.ofEquiv _ (Cow.proxyEquiv n)

[Andrej Bauer]

Thanks. I spent some time looking for Fintype.ofEquiv but didn't find it.

[Eric Wieser]

library_search ought to have been able to find it if you set things up in the right generality first

[Kyle Miller]

@Eric Wieser What are you imagining would be the setup?

import Mathlib.Data.Fintype.Sigma
import Mathlib.Tactic.LibrarySearch

instance [Fintype α] (f : α ≃ β) : Fintype β := by library_search
-- suggestion: refine { elems := ?_ (id (Equiv.symm f)), complete := (_ : ∀ (x : β), x ∈ ?_) }

[Eric Wieser]

Yeah, I was hoping that would work...

[Eric Wieser]

It doesn't work in Lean 3 either :(

import data.fintype.basic
example {α β} [fintype α] (f : α ≃ β) : fintype β := by library_search

[Scott Morrison]

Noted the library_search failure at !4#3426.