Theorem: Array.getElem_map' (Algdata/Data/Array/Lemmas.lean)

State before:
α : Type u
m : Type v → Type w
inst✝ : Monad m
β : Type u_1
f : α → β
arr : Array α
i : Nat
hi : i < size (map f arr)
⊢ (map f arr)[i] = f arr[i]
Tactic:
show (arr.map f).data[i] = f (arr[i]' _)
State after:
α : Type u
m : Type v → Type w
inst✝ : Monad m
β : Type u_1
f : α → β
arr : Array α
i : Nat
hi : i < size (map f arr)
⊢ (map f arr).data[i] = f arr[i]

State before:
α : Type u
m : Type v → Type w
inst✝ : Monad m
β : Type u_1
f : α → β
arr : Array α
i : Nat
hi : i < size (map f arr)
⊢ (map f arr).data[i] = f arr[i]
Tactic:
rw [getElem_eq (arr.map_data' f) (Eq.refl i)]
State after:
α : Type u
m : Type v → Type w
inst✝ : Monad m
β : Type u_1
f : α → β
arr : Array α
i : Nat
hi : i < size (map f arr)
⊢ (List.map f arr.data)[i] = f arr[i]

State before:
α : Type u
m : Type v → Type w
inst✝ : Monad m
β : Type u_1
f : α → β
arr : Array α
i : Nat
hi : i < size (map f arr)
⊢ (List.map f arr.data)[i] = f arr[i]
Tactic:
exact List.get_map f
State after:
no goals