Cases tactic fails

Stream: new members

[Nicolò Cavalleri]

Suppose I am trying to prove something is a commutative group, and for this I need to build a function add. There is a lemma that tells me that under some hypotheses, that are satisfied in my case, there exists a map with certain properties. I need to use that map to build my add function, however in order to get the map I need to give this lemma the hypotheses it wants and in order to do it I switch into tactic mode. After I give it the hypotheses I get an hypothesis of the forms \esists f, ... and I need to get that f. However, I cannot use cases as my goal is not a prop. What can I do? It is really hard for me to create a mwe now as there's a lot of code in between what I am doing and the current version of Mathlib I think

[Yakov Pechersky]

obtain ⟨f, hf⟩ := hyp

[Yakov Pechersky]

where hyp is the hypothesis of the form \ex f, p f, and f will be the function that satisfies hf : p f

[Nicolò Cavalleri]

It still tells me

induction tactic failed, recursor 'Exists.dcases_on' can only eliminate into Prop

with obtain, I guess you'd need to see the code?

[Alex J. Best]

Sounds like docs#classical.some is what you want? You can use that to get something from an exists, and docs#classical.some_spec to show that that term has the right property.

[Reid Barton]

It also sounds like maybe the lemma you use should not have been a lemma at all, but rather a def

[Nicolò Cavalleri]

It is actually a definition but it there is still an exists in it. It is analogous to the definition of topological fiber bundle:

def is_topological_fiber_bundle : Prop :=
∀ x : Z, ∃e : bundle_trivialization F proj, x ∈ e.source

I have my x where I want to get my trivialization and I need to use e but I can't manage to extract it. I will try Alex's suggestion

[Reid Barton]

Perhaps you could explain what it is you want to do?

[Nicolò Cavalleri]

Reid Barton said:

Perhaps you could explain what it is you want to do?

Actually what I was trying to do was stupid and I changed everything but thanks a lot for the help!