Theorem: Misc.Array.modify_preserves_size (LeanSAT/Util/Misc.lean)

State before:
α : Type u_1
a : Array α
i : Nat
f : α → α
⊢ (a.modify i f).size = a.size
Tactic:
simp only [Array.modify, Array.modifyM, Id.bind_eq, Id.pure_eq, Id.run]
State after:
α : Type u_1
a : Array α
i : Nat
f : α → α
⊢ Array.size (if h : i < a.size then a.set ⟨i, ⋯⟩ (f (a.get ⟨i, ⋯⟩)) else a) = a.size

State before:
α : Type u_1
a : Array α
i : Nat
f : α → α
⊢ Array.size (if h : i < a.size then a.set ⟨i, ⋯⟩ (f (a.get ⟨i, ⋯⟩)) else a) = a.size
Tactic:
split
State after:
case isTrue
α : Type u_1
a : Array α
i : Nat
f : α → α
h✝ : i < a.size
⊢ (a.set ⟨i, ⋯⟩ (f (a.get ⟨i, ⋯⟩))).size = a.size

case isFalse
α : Type u_1
a : Array α
i : Nat
f : α → α
h✝ : ¬i < a.size
⊢ a.size = a.size

State before:
case isTrue
α : Type u_1
a : Array α
i : Nat
f : α → α
h✝ : i < a.size
⊢ (a.set ⟨i, ⋯⟩ (f (a.get ⟨i, ⋯⟩))).size = a.size

case isFalse
α : Type u_1
a : Array α
i : Nat
f : α → α
h✝ : ¬i < a.size
⊢ a.size = a.size
Tactic:
. simp only [Array.size_set]
State after:
case isFalse
α : Type u_1
a : Array α
i : Nat
f : α → α
h✝ : ¬i < a.size
⊢ a.size = a.size

State before:
case isFalse
α : Type u_1
a : Array α
i : Nat
f : α → α
h✝ : ¬i < a.size
⊢ a.size = a.size
Tactic:
. rfl
State after:
no goals

State before:
case isTrue
α : Type u_1
a : Array α
i : Nat
f : α → α
h✝ : i < a.size
⊢ (a.set ⟨i, ⋯⟩ (f (a.get ⟨i, ⋯⟩))).size = a.size
Tactic:
simp only [Array.size_set]
State after:
no goals

State before:
case isFalse
α : Type u_1
a : Array α
i : Nat
f : α → α
h✝ : ¬i < a.size
⊢ a.size = a.size
Tactic:
rfl
State after:
no goals