proof golfing

Stream: lean4

[Siddharth Bhat]

theorem h (m : BitVec 64) (P : BitVec 64 → Bool)
    (h : m ≤ 0x00000006 ∧
         P 0x00000000 ∧
         P 0x00000001 ∧
         P 0x00000002 ∧
         P 0x00000003 ∧
         P 0x00000004 ∧
         P 0x00000005 ∧
         P 0x00000006) :
    P m := by
  obtain ⟨m, hm⟩ := m
  simp_all [BitVec.le_def]
  -- this proof is unfortunate, it's surely golfable,
  -- and one would hope that the automation would do better.
  obtain hm | hm | hm | hm | hm | hm | hm : m = 0 ∨ m = 1 ∨ m = 2 ∨ m = 3 ∨
    m = 4 ∨ m = 5 ∨ m = 6 := by omega
  repeat (simp [hm] at h ⊢; simp [h])

Using only core Lean (no mathlib / batteries), is this proof golfable?

[Kyle Miller]

The only thing I can see is replacing the last line with all_goals subst_vars; simp_all.

[Kyle Miller]

You said no mathlib, but mathlib does have a tactic for that obtain.

theorem h (m : BitVec 64) (P : BitVec 64 → Bool)
    (h : m ≤ 0x00000006 ∧
         P 0x00000000 ∧
         P 0x00000001 ∧
         P 0x00000002 ∧
         P 0x00000003 ∧
         P 0x00000004 ∧
         P 0x00000005 ∧
         P 0x00000006) :
    P m := by
  obtain ⟨m, hm⟩ := m
  simp_all [BitVec.le_def]
  have := h.1
  -- Mathlib.Tactic.IntervalCases
  interval_cases m <;> simp_all