## Stream: new members

### Topic: simplifying card proof

#### Shimon Cohen (May 30 2023 at 11:38):

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 (May 30 2023 at 11:41):

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

Last updated: Dec 20 2023 at 11:08 UTC