Finding an operation that satisfies a specific requirement in "lean"

Question

I have already define four boolean operations:

def bnot : bool → bool 
| tt := ff
| ff := tt 

def band : bool → bool → bool 
| tt b := b
| ff b := ff

def bor : bool → bool → bool 
| tt b := tt
| ff b := b

def is_tt : bool → Prop 
| tt := true
| ff := false

and now I need to define an new operation:

def exb  (f : bool → bool) : bool
    :=sorry,

then use the operations above to computer and prove the existential quantification on booleans

exb_ok : ∀ f : bool → bool, is_tt (exb f) ↔ ∃ x : bool, is_tt (f x) :=
begin
  sorry,
end 

Now change the 'sorry' to the real answer.

I think may be it has

def exb  (f : bool → bool) : bool
    := f tt || f ff

theorem exb_ok : ∀ f : bool → bool, is_tt (exb f) ↔ ∃ x : bool, is_tt (f x) :=
begin
  assume f,
  constructor,
  dsimp[exb],
  assume h,
  existsi tt,
end

and I stop at this step, I do not know how to do next. And the goals now are

'f : bool → bool,
 h : is_tt (f tt||f ff)
 ⊢ is_tt (f tt)
 
 f : bool → bool
 ⊢ (∃ (x : bool), is_tt (f x)) → is_tt (exb f)'