How to name the hypothesis resulting from the split tactic for if statements

Question

I am trying to prove the following theorem:

theorem list_take_take (n n: Nat) (xs: List α):
  take n (take m xs) = take (min n m) xs := by
  revert m xs
  induction n with
  | zero =>
    intro m xs
    rw [nat_min_zero]
    repeat rw [take]
  | succ n ihn =>
    intro m xs
    cases m with
    | zero =>
      rw [take, min]
      simp
      rw [take]
      apply list_take_nil
    | succ m =>
      unfold min
      split
      · -- case: succ n ≤ succ m
        -- how do I rewrite succ n ≤ succ m to n ≤ m
        -- using Nat.succ_le_succ or Nat.le_of_succ_le_succ?
        sorry
      · sorry

When I get to the split tactic, it splits the if statement that resulted from unfolding the min function, but the new hypothesis succ n ≤ succ m has no name, so I can't rewrite it to n ≤ m. Is there a way to name the hypothesis that will result from using the split tactic or is there another way to do cases on the comparison?

Note: this question is about Lean4 and not Lean3

Answer 1

In the tactic state you can see which case you are looking at

Tactic state
case succ.succ.inl
α: Type u_1
n✝n: Nat
ihn: ∀ {m : Nat} (xs : List α), take n (take m xs) = take (min n m) xs
xs: List α
m: Nat
: succ n ≤ succ m
⊢ take (succ n) (take (succ m) xs) = take (succ n) xs

You can use this to add a case clause after the split

unfold min
split
· case succ.succ.inl h =>

This will result in the comparison hypothesis being named as h:

α: Type u_1
n✝n: Nat
ihn: ∀ {m : Nat} (xs : List α), take n (take m xs) = take (min n m) xs
xs: List α
m: Nat
h: succ n ≤ succ m
⊢ take (succ n) (take (succ m) xs) = take (succ n) xs