Theorem: Array.modify_stable_size (Advent/Array.lean)

State before:
α : Type u_1
arr : Array α
f : α → α
n : Nat
⊢ size arr = size (modify arr n f)
Tactic:
simp [modify, modifyM, dite]
State after:
α : Type u_1
arr : Array α
f : α → α
n : Nat
⊢ size arr =
    size
      (Id.run
        (Decidable.rec (fun h => arr) (fun h => set arr { val := n, isLt := h } (f arr[n])) (Nat.decLt n (size arr))))

State before:
α : Type u_1
arr : Array α
f : α → α
n : Nat
⊢ size arr =
    size
      (Id.run
        (Decidable.rec (fun h => arr) (fun h => set arr { val := n, isLt := h } (f arr[n])) (Nat.decLt n (size arr))))
Tactic:
generalize Nat.decLt n (size arr) = q
State after:
α : Type u_1
arr : Array α
f : α → α
n : Nat
q : Decidable (n < size arr)
⊢ size arr = size (Id.run (Decidable.rec (fun h => arr) (fun h => set arr { val := n, isLt := h } (f arr[n])) q))

State before:
α : Type u_1
arr : Array α
f : α → α
n : Nat
q : Decidable (n < size arr)
⊢ size arr = size (Id.run (Decidable.rec (fun h => arr) (fun h => set arr { val := n, isLt := h } (f arr[n])) q))
Tactic:
cases q <;> simp [Id.run]
State after:
no goals