Theorem: Array.getElem_modify_eq (Algdata/Data/Array/Lemmas.lean)

State before:
α✝ : Type u
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
x : Array α
i : Nat
f : α → α
hi : i < size x
⊢ (modify x i f)[i] = f x[i]
Tactic:
dsimp [modify, modifyM, Id.run]
State after:
α✝ : Type u
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
x : Array α
i : Nat
f : α → α
hi : i < size x
⊢ (if h : i < size x then set x { val := i, isLt := h } (f x[i]) else x)[i] = f x[i]

State before:
α✝ : Type u
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
x : Array α
i : Nat
f : α → α
hi : i < size x
⊢ (if h : i < size x then set x { val := i, isLt := h } (f x[i]) else x)[i] = f x[i]
Tactic:
simp only [dif_pos hi]
State after:
α✝ : Type u
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
x : Array α
i : Nat
f : α → α
hi : i < size x
⊢ (set x { val := i, isLt := hi } (f x[i]))[i] = f x[i]

State before:
α✝ : Type u
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
x : Array α
i : Nat
f : α → α
hi : i < size x
⊢ (set x { val := i, isLt := hi } (f x[i]))[i] = f x[i]
Tactic:
rw [Array.get_set_eq]
State after:
no goals