cases without losing previous ones

Stream: new members

[Filippo A. E. Nuccio]

Is there a way to perform by_cases (say, on hn : n =0) in a way that once the basic case has been proven, it stays in the local assumptions so that I can use it explicitly for the general case?

[Anne Baanen]

Could you explain what you want the goals to look like: from your description I understand that you want two goals, the first n = 0 → P and the other n ≠ 0 → (n = 0 → P) → P?

[Eric Wieser]

Use a have or suffices?

[Anne Baanen]

But n ≠ 0 implies n = 0 → P: this is just docs#absurd, no?

[Patrick Massot]

Filippo... why are you still posting in the new members stream?

[Filippo A. E. Nuccio]

OK, I try to explain myself better. I have a statement P n which I want to prove (say, for n : nat). I am (so far) unable to unify the proof of P 0 and P n for general n, so I thought about using by_cases to distinguish the two cases. But for my proof of P n I would like to use P 0, which has disappeared.

[Filippo A. E. Nuccio]

Patrick Massot said:

Filippo... why are you still posting in the new members stream?

Because I though that the question was very basic...

[Mario Carneiro]

I would suggest just doing have : P 0, { ...}, by_cases h : n = 0, { rw h, exact this }, ...

[Filippo A. E. Nuccio]

Yes, re-reading @Eric Wieser 's suggestion I understood he had this in mind. Thanks! Probably being at the 10th hour of Lean today is not helping...