rcases option unit

Stream: general

[Johan Commelin]

Which pattern should I use to completely destroy a term of type option unit?

import tactic

example (i : option unit) : true :=
begin
  rcases i with (_|i), -- how do I get rid of the `i` in the second goal?
  -- rcases i with (_|⟨)⟩, -- doesn't help, I still have an `i` in the second goal
  all_goals { trivial },
end

cc @Mario Carneiro

[Jujian Zhang]

How about this

example (i : option unit) : true :=
begin
/-
2 goals
⊢ true

⊢ true
-/

  rcases i with (_|_|_),
end

[Eric Rodriguez]

rcases i with _ | ⟨⟨⟩⟩

[Eric Rodriguez]

gotten from rcases? i

[Eric Rodriguez]

which is a very underrated extension to rcases

[Kevin Buzzard]

I use it a lot :-) It was really helpful for doing "reshuffling" proofs in my undergraduate course.

[Eric Wieser]

Use match instead?

[Eric Rodriguez]

how does match help here?

[Eric Wieser]

Sorry, I guess I mean the equation compiler:

example : Π (i : option unit), true
| none := trivial
| (some ()) := trivial

[Eric Wieser]

Indeed, match doesn't eliminate the variable

[Mario Carneiro]

Eric Rodriguez said:

rcases i with _ | ⟨⟨⟩⟩

gotten from rcases? i

@Johan Commelin ^ I wrote this bot to speak on my behalf :grinning:

[Mario Carneiro]

Although in this particular case there is an even shorter alternative: rcases i with _|-, which clears i instead of destructuring it