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?

$\endgroup$

1 Answer 1

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
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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