# Zulip Chat Archive

## 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

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

adding

```
local attribute [irreducible] Set.mem
```

makes it instant

Last updated: Dec 20 2023 at 11:08 UTC