In lean 4, how do I give names to variables when using `split`?

Question

Sort of related to In lean 4, how do I refer to variables with names like `a✝`

When I use split to pull apart a match, I get a huge influx of variables. How do I name them so I can refer to them? (Should I be using split to pull apart match?)

import Mathlib

example
  (a : Int)
  (b c : Nat)
  (ha : 0 <= a)
  (hb : 1 <= b)
  : (Int.div a (Nat.succ b) ≤ Int.div a b)
  := by
  induction' b with d hd
  absurd hb
  simp
  induction d
  simp
  induction' a with a2 ha2
  simp
  simp [Int.div]
  split  -- adds variables "x✝¹", "x✝", "m✝", "n✝", "heq✝¹", "heq✝"
  sorry
  sorry
  sorry
  sorry
  sorry
  sorry
```

Answer 1

You can use case (or next) tactic to specify the subgoal and name the variables. See the doc string for split for more information. Here I used case with induction as well.

example
  (a : Int)
  (b c : Nat)
  (ha : 0 <= a)
  (hb : 1 <= b)
  : (Int.div a (Nat.succ b) ≤ Int.div a b)
  := by
  induction b
  case zero =>
    absurd hb
    simp
  case succ d hd =>
    induction d
    case zero =>
      simp
      induction a
      case ofNat a =>
        simp
        simp [Int.div] -- I don't think this is a good idea, but to illustrate how to do it...
        split
        case h_1 a b c d e f => sorry
        case h_2 a b c d e f => sorry
        case h_3 a b c d e f => sorry
        case h_4 a b c d e f => sorry
      case negSucc a => sorry