Theorem: List.length_rangeF (MLIR/Util/List.lean)

State before:
n : ℕ
⊢ length (rangeF n) = n
Tactic:
induction n with
| zero => simp
| succ m ih => simp [rangeF, ih]
State after:
no goals

State before:
case zero

⊢ length (rangeF Nat.zero) = Nat.zero
Tactic:
simp
State after:
no goals

State before:
case succ
m : ℕ
ih : length (rangeF m) = m
⊢ length (rangeF (Nat.succ m)) = Nat.succ m
Tactic:
simp [rangeF, ih]
State after:
no goals