simplifying card proof

Stream: new members

[Shimon Cohen]

I want to prove the theorem about the number of graphs over some fintype, To get familliar with this kind of proofs I started with simplified version.
Assuming the folowing definitions

import tactic
import data.fintype.big_operators

variables {V : Type*}

@[ext]
structure func (V : Type*) :=
  (f : V → Prop)

open fintype

@[instance]
noncomputable def func.fintype [fintype V] : fintype (func V) :=
begin
   classical,
   exact of_injective func.f func.ext,
end

prove that
theorem my_card_func [fintype V] : card (func V) = 2 ^ card V := sorry

I did it with isomerphism as follow

theorem on_f [fintype V] : card (V -> Prop) = 2 ^ card V := card_fun

@[simp] theorem func_def (fu : V → Prop) : (func.mk fu).f = fu := rfl

theorem left_inv : function.left_inverse (@func.mk V) (@func.f V) :=
begin
  intros funcV,
  apply func.ext,
  simp,
end

theorem right_inv : function.right_inverse (@func.mk V) (@func.f V) :=
begin
  intros funcV,
  simp,
end

def func_iso_f : func V ≃ (V → Prop) :=
  {to_fun := func.f, inv_fun := func.mk, left_inv := left_inv, right_inv := right_inv}

theorem my_card_func [fintype V] : card (func V) = 2 ^ card V :=
begin
  rw [(fintype.card_congr func_iso_f)],
  exact on_f,
end

There is a way to simplify the proof?

[Eric Wieser]

I would recommend using func_iso_f to define the : fintype (func V) instance in the first place (via docs#fintype.of_equiv)