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

State before:
α : Type u_1
l : List α
f : ℕ → ℕ
h : ∀ (n : ℕ), n < length l → f n < length l
⊢ length (remap l f h) = length l
Tactic:
simp [remap]
State after:
no goals