Does `classical` break `interval_cases`?

Stream: maths

[Kevin Buzzard]

import tactic

example (n : ℕ) (hn : n ≤ 4) : false :=
begin
  classical,
  interval_cases n,
  repeat {sorry}
end

/-
cases tactic failed, it is not applicable to the given hypothesis
state:
n : ℕ,
hn : n ≤ 4,
_inst : Π (a : Prop), decidable a,
lh : n ∈ tactic.interval_cases.set_elems (set.Ico ⊥ (4 + 1))
⊢ false
-/

If you comment out classical it works fine.

[Kevin Buzzard]

Another interval_cases issue:

import tactic group_theory.order_of_element

example (G : Type) [fintype G] [group G] [decidable_eq G]
  (g : G) (h : order_of g ≤ 2) : false :=
begin
  interval_cases (order_of g),
  repeat {sorry}
end

You would expect to get three cases order_of g = 0,1,2. But I think simp or something got to the middle case:

3 goals
G : Type,
_inst_1 : fintype G,
_inst_2 : group G,
_inst_3 : decidable_eq G,
g : G,
h : order_of g ≤ 2,
lh : order_of g = 0
⊢ false

G : Type,
_inst_1 : fintype G,
_inst_2 : group G,
_inst_3 : decidable_eq G,
h : order_of 1 ≤ 2
⊢ false

G : Type,
_inst_1 : fintype G,
_inst_2 : group G,
_inst_3 : decidable_eq G,
g : G,
h : order_of g ≤ 2,
lh : order_of g = 2
⊢ false

Lean has eliminated the hypothesis that the order of g is 1, and replaced g with the identity. Which is fine, I guess, but perhaps not what I expected.

[Scott Morrison]

This is probably my fault in some way. :-) I'm not sure I'll have time to look at it today. If no one else jumps in, creating and assigning an issue to me would be great. interval_cases is built on top of fin_cases, and both are pretty simple tactics (which can be "decompiled" by hand into a string of other tactic invocations), so it's probably not too hard to find where we're over simplifying.

[Kevin Buzzard]

#2367