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