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

State before:
α : Type ?u.30674
l : List α
f : ℕ → ℕ
h_f : ∀ (n : ℕ), n < length l → f n < length l
n : ℕ
h_n : n < length (remap l f h_f)
⊢ f n < length l
Tactic:
apply h_f
State after:
case a
α : Type ?u.30674
l : List α
f : ℕ → ℕ
h_f : ∀ (n : ℕ), n < length l → f n < length l
n : ℕ
h_n : n < length (remap l f h_f)
⊢ n < length l

State before:
case a
α : Type ?u.30674
l : List α
f : ℕ → ℕ
h_f : ∀ (n : ℕ), n < length l → f n < length l
n : ℕ
h_n : n < length (remap l f h_f)
⊢ n < length l
Tactic:
simp at h_n
State after:
case a
α : Type ?u.30674
l : List α
f : ℕ → ℕ
h_f : ∀ (n : ℕ), n < length l → f n < length l
n : ℕ
h_n : n < length l
⊢ n < length l

State before:
case a
α : Type ?u.30674
l : List α
f : ℕ → ℕ
h_f : ∀ (n : ℕ), n < length l → f n < length l
n : ℕ
h_n : n < length l
⊢ n < length l
Tactic:
apply h_n
State after:
no goals

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