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

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

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

• · is an anonymous case, you don't need both Mar 7 at 10:50
• Even better, thank you :)  unfold min split case succ.succ.inl h => rw [nat_succ_le_succ_iff] at h  Mar 7 at 15:30