confusing behavior with interval_cases

Stream: new members

[Patrick Lutz]

I'm not sure the issue is actually with interval_cases. After doing the following

import tactic data.nat.basic

example (n : ℕ) (h : n % 5 = 3) : n ≥ 3 :=
begin
    by_contradiction h',
    push_neg at h',
    interval_cases n,
end

the goal state looks like this:

3 goals
h : 0 % 5 = 3,
h' : 0 < 3
⊢ false

h : 1 % 5 = 3,
h' : 1 < 3
⊢ false

h : 2 % 5 = 3,
h' : 2 < 3
⊢ false

I think tauto should be able to take care of all three goals. But this

example (n : ℕ) (h : n % 5 = 3) : n ≥ 3 :=
begin
    by_contradiction h',
    push_neg at h',
    interval_cases n;
    tauto,
end

results in this goal state

done tactic failed, there are unsolved goals
state:
h : 1 % 5 = 3,
h' : 1 < 3
⊢ false

Using finish in place of tauto has the same effect. And the same thing happens if I use tauto on each goal separately.

Why is this happening? Why would tauto work on the first and third goals but not the second goal? They all look pretty much the same to me.

[Reid Barton]

It doesn't work on the third goal

[Reid Barton]

tauto would not occur to me. Try norm_num at h.

[Rob Lewis]

Or cases h

[Patrick Lutz]

Oh, I think I just got confused by the message in the goal state

[Patrick Lutz]

I just tried tauto because hintsuggested it

[Patrick Lutz]

Okay, thanks for the advice. I do know how to prove this kind of thing but I was just confused that I thought tauto worked on the first and third goals but not the second. Now I see it only works on the first, which makes much more sense