keyword_tactics.lean:34:2: error: unify tactic failed, failed to unify
  bool : Type
and
  ℕ : Type
state:
⊢ ℕ → ℕ → ℕ
keyword_tactics.lean:52:0: error: tactic failed, there are unsolved goals
state:
f : ℕ → ℕ,
this : ℕ
⊢ bool
keyword_tactics.lean:57:0: error: tactic failed, there are unsolved goals
state:
f : ℕ → ℕ
⊢ ℕ → bool
