1
$\begingroup$

I'm trying to prove a <= max(a, b) by case. I have this:

example (a b : Nat) : a <= (max a b) := by
  cases decide (a <= b) with
  | true =>
    sorry
  | false =>
    sorry

When I put my cursor before the first sorry, I see the following tactic state:

enter image description here

The thing that's confusing me is I don't see "decide (a <= b)" as one of the available terms anywhere in the state. I need that in order to complete the case. How do I get access to the case assumption in order to finish the case?

Improve this question
$\endgroup$

1 Answer 1

Reset to default
1
$\begingroup$

Use cases h : decide(a <= b) with. You can read more about it in the doc string for cases.

example (a b : Nat) : a <= (max a b) := by
  cases h : decide (a <= b) with
  | true =>
    sorry
    /-
    case true
    a b : Nat
    h : decide (a ≤ b) = true
    ⊢ a ≤ max a b
    -/
  | false =>
    sorry
Improve this answer
$\endgroup$

Not the answer you're looking for? Browse other questions tagged or ask your own question.