Theorem: Misc.Array.set!_preserves_size (LeanSAT/Util/Misc.lean)

State before:
α : Type u_1
a : Array α
i : Nat
x : α
⊢ (a.set! i x).size = a.size
Tactic:
rw [Array.set!, Array.setD]
State after:
α : Type u_1
a : Array α
i : Nat
x : α
⊢ (if h : i < a.size then a.set ⟨i, h⟩ x else a).size = a.size

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

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

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

case isFalse
α : Type u_1
a : Array α
i : Nat
x : α
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
x : α
h✝ : ¬i < a.size
⊢ a.size = a.size

State before:
case isFalse
α : Type u_1
a : Array α
i : Nat
x : α
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
x : α
h✝ : i < a.size
⊢ (a.set ⟨i, h✝⟩ x).size = a.size
Tactic:
simp only [Array.size_set]
State after:
no goals

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