## Stream: new members

### Topic: cases timeout; using zfc sets

#### Evan Haskell (May 26 2021 at 01:07):

I've been working through a book on axiomatic set theory and have been proving much of it in lean for fun using the constructions in set_theory.zfc. But I've run into a deterministic timeout on a few occasions. Here's a MWE.

import set_theory.zfc

namespace Set

def dom (R : Set) : Set := {x  R.Union.Union |  y, x.pair y  R}
def ran (R : Set) : Set := {y  R.Union.Union |  x : Set, x.pair y  R}
def fun_value (F x : Set) : Set := {y  F.Union.Union | x.pair y  F}.Union
def inv (R : Set) : Set := pair_sep (λ a b, b.pair a  R) R.ran R.dom

theorem ttt {F : Set} : F.inv.fun_value   F :=
begin
cases 0, -- deterministic timeout in vscode
end

end Set

The lean command returns after ~10 seconds. cases and related tactics timeout regardless of the arguments. It doesn't timeout if I remove .inv or .fun_value ∅ or replace with = in the goal. Is the goal just too complicated? What's going on? Can I increase the timeout threshold?

The strange thing is I can do nat.cases_on without issue:

apply @nat.cases_on (λ n, F.inv.fun_value   F) 0,
sorry,
intro n, sorry,

#### Mario Carneiro (May 26 2021 at 02:18):

I would guess that cases is trying to find the weak head normal form of the goal and this is particularly expensive for the example goal