Theorem: Array.modifyLast_data (One.lean)

State before:
α✝ : Type u_1
f : α✝ → α✝
a : Array α✝
⊢ (modifyLast f a).data = List.modifyLast f a.data
Tactic:
unfold modifyLast
State after:
α✝ : Type u_1
f : α✝ → α✝
a : Array α✝
⊢ (modify a (size a - 1) f).data = List.modifyLast f a.data

State before:
α✝ : Type u_1
f : α✝ → α✝
a : Array α✝
⊢ (modify a (size a - 1) f).data = List.modifyLast f a.data
Tactic:
rw [List.modifyLast_eq_modifyNth]
State after:
α✝ : Type u_1
f : α✝ → α✝
a : Array α✝
⊢ (modify a (size a - 1) f).data = List.modifyNth f (List.length a.data - 1) a.data

State before:
α✝ : Type u_1
f : α✝ → α✝
a : Array α✝
⊢ (modify a (size a - 1) f).data = List.modifyNth f (List.length a.data - 1) a.data
Tactic:
simp only [tsub_le_iff_right, ge_iff_le, modify_data]
State after:
no goals