Theorem: Array.get_modify (Lean4Lean/Std/Basic.lean)

State before:
α : Type ?u.21452
f : α → α
arr : Array α
x i : Nat
h : i < size arr
⊢ i < size (modify arr x f)
Tactic:
simp [h]
State after:
no goals

State before:
α : Type u_1
f : α → α
arr : Array α
x i : Nat
h : i < size arr
⊢ get (modify arr x f) { val := i, isLt := ⋯ } =
    if x = i then f (get arr { val := i, isLt := h }) else get arr { val := i, isLt := h }
Tactic:
simp [modify, modifyM, Id.run]
State after:
α : Type u_1
f : α → α
arr : Array α
x i : Nat
h : i < size arr
⊢ (if h : x < size arr then set arr { val := x, isLt := h } (f arr[x]) else arr)[i] = if x = i then f arr[i] else arr[i]

State before:
α : Type u_1
f : α → α
arr : Array α
x i : Nat
h : i < size arr
⊢ (if h : x < size arr then set arr { val := x, isLt := h } (f arr[x]) else arr)[i] = if x = i then f arr[i] else arr[i]
Tactic:
split
State after:
case inl
α : Type u_1
f : α → α
arr : Array α
x i : Nat
h : i < size arr
h✝ : x < size arr
⊢ (set arr { val := x, isLt := h✝ } (f arr[x]))[i] = if x = i then f arr[i] else arr[i]

case inr
α : Type u_1
f : α → α
arr : Array α
x i : Nat
h : i < size arr
h✝ : ¬x < size arr
⊢ arr[i] = if x = i then f arr[i] else arr[i]

State before:
case inl
α : Type u_1
f : α → α
arr : Array α
x i : Nat
h : i < size arr
h✝ : x < size arr
⊢ (set arr { val := x, isLt := h✝ } (f arr[x]))[i] = if x = i then f arr[i] else arr[i]
Tactic:
simp [get_set _ _ _ h]
State after:
case inl
α : Type u_1
f : α → α
arr : Array α
x i : Nat
h : i < size arr
h✝ : x < size arr
⊢ (if x = i then f arr[x] else arr[i]) = if x = i then f arr[i] else arr[i]

State before:
case inl
α : Type u_1
f : α → α
arr : Array α
x i : Nat
h : i < size arr
h✝ : x < size arr
⊢ (if x = i then f arr[x] else arr[i]) = if x = i then f arr[i] else arr[i]
Tactic:
split <;> simp [*]
State after:
no goals

State before:
case inr
α : Type u_1
f : α → α
arr : Array α
x i : Nat
h : i < size arr
h✝ : ¬x < size arr
⊢ arr[i] = if x = i then f arr[i] else arr[i]
Tactic:
rw [if_neg (mt (by rintro rfl; exact h) ‹_›)]
State after:
no goals

State before:
α : Type u_1
f : α → α
arr : Array α
x i : Nat
h : i < size arr
h✝ : ¬x < size arr
⊢ x = i → ?m.24309
Tactic:
rintro rfl
State after:
α : Type u_1
f : α → α
arr : Array α
x : Nat
h✝ : ¬x < size arr
h : x < size arr
⊢ ?m.24496 h

State before:
α : Type u_1
f : α → α
arr : Array α
x : Nat
h✝ : ¬x < size arr
h : x < size arr
⊢ ?m.24496 h
Tactic:
exact h
State after:
no goals