# Zulip Chat Archive

## Stream: new members

### Topic: cases and rcases won't eliminate hypothesis

#### Robin Carlier (May 30 2020 at 15:16):

Hey, I'm in a situation that I suspect that is a bug, but It may be as well that I'm missing something obvious. Unfortunately, this is part of some bigger code chunk, with a few dependencies, so I can't post a MWE. Also I don't even know how to reproduce this behaviour.

I am writing a proof and I have some hypothesis with an existential quantifier, When I try to `cases`

or `rcases`

this hypothesis, I get the following error message: `induction tactic failed, recursor 'Exists.dcases_on' can only eliminate into Prop`

. Now what is really weird is that in an earlier proof, with exactly *the same* hypothesis (when I say exactly, I mean I compared the two hypothesis with `set_option pp.all true`

and they were really exactly the same) , and cases worked just fine.

Now even weirder: if I `tidy?`

in my proof, and follow the first few instructions (a few `fsplit`

and `work_on_goal`

), tidy then suggests some `cases`

is done on this hypothesis, and it works. I tried a bunch of things: if I open some subgoal, then it starts working as well.

here is what my exists statement looks like with pprint.all :

```
@Exists.{u+1} (set.{u} (@category_theory.over.{u u} C 𝒞 X))
(λ (R : set.{u} (@category_theory.over.{u u} C 𝒞 X)),
@Exists.{0}
(@has_mem.mem.{u u} (set.{u} (@category_theory.over.{u u} C 𝒞 X))
(set.{u} (set.{u} (@category_theory.over.{u u} C 𝒞 X)))
(@set.has_mem.{u} (set.{u} (@category_theory.over.{u u} C 𝒞 X)))
R
(K X))
(λ
(H :
@has_mem.mem.{u u} (set.{u} (@category_theory.over.{u u} C 𝒞 X))
(set.{u} (set.{u} (@category_theory.over.{u u} C 𝒞 X)))
(@set.has_mem.{u} (set.{u} (@category_theory.over.{u u} C 𝒞 X)))
R
(K X)),
@has_subset.subset.{u} (set.{u} (@category_theory.over.{u u} C 𝒞 X))
(@set.has_subset.{u} (@category_theory.over.{u u} C 𝒞 X))
R
(@category_theory.sieve.arrows.{u u} C 𝒞 X S)))
```

Any idea how one would find a work-around for this kind of things? I can `classical.some`

one the hypothesis but I'd rather avoid. Also, what kind of debug options (further than pp.print_all) would be usefull there to try to understand what's going on?

#### Johan Commelin (May 30 2020 at 15:19):

It means that your goal is not a `Prop`

#### Johan Commelin (May 30 2020 at 15:19):

So even though the hypothesis is the same, the rest of your context isn't

#### Robin Carlier (May 30 2020 at 15:19):

Oh well that explains everything

#### Johan Commelin (May 30 2020 at 15:21):

You'll have to either work your way around it (by doing stuff that makes your goal a `Prop`

) or use `choose`

.

#### Johan Commelin (May 30 2020 at 15:21):

For example, if you want to use `exfalso`

, do that first, and afterwards the `cases`

will work.

#### Robin Carlier (May 30 2020 at 15:22):

Well I guess I'll just use choose. Makes sense since the goal is to give some object.

#### Robin Carlier (May 30 2020 at 15:26):

Well thank you a lot, I was going mad over this!

#### Johan Commelin (May 30 2020 at 15:27):

No worries

#### Johan Commelin (May 30 2020 at 15:27):

Asking questions here is an encouraged method of solving problems

#### Kevin Buzzard (May 30 2020 at 16:20):

If you're using tactic mode to make something that isn't a proof, you might be doing it wrong.

Sometimes you can get around things not eliminating to Type by using `classical. some`

Last updated: May 11 2021 at 23:11 UTC