Array property using induction

Stream: lean4

[Muqsit Azeem]

I am using induction to prove the property that updating all the values of an array will not change the size of the array.

import Std.Data.Array

def set_elements (arr: Array Int) (index: Nat) : Array Int := Id.run do
  let mut arr : Array Int := arr
  let mut index : Nat := index
  if index >= arr.size then
    return arr
  else
    arr := arr.set! index 1
    index := index+1
    return set_elements arr index
termination_by _ => arr.size - index
decreasing_by simp_wf; sorry


def set_one (arr: Array Int) : Array Int := Id.run do
  return set_elements arr 0


theorem set_elements_size (arr : Array Int) (index : Nat) : (set_elements arr index).size = arr.size := by
  unfold set_elements Id.run
  simp_all
  induction arr.size - index
  case zero =>
    have h₁: arr.size = index := by sorry -- assuming case zero => arr.size - index = 0
    simp_all
  case succ =>
    have h₂: arr.size > index := by sorry -- assuming case zero => arr.size - index > 0
    simp_all



theorem size_same_set_1 (arr: Array Int) : (set_one arr).size = arr.size := by
  unfold set_one Id.run
  simp_all
  apply set_elements_size

Applying induction on arr.size - index splits it into two goals given below but no constraints on the induction variables.

case zero
arr: Array Int
index: Nat
⊢ Array.size (if index ≥ Array.size arr then arr else set_elements (Array.set! arr index 1) (index + 1)) = Array.size arr

and

case succ
arr: Array Int
indexn✝: Nat
n_ih✝: Array.size (if index ≥ Array.size arr then arr else set_elements (Array.set! arr index 1) (index + 1)) = Array.size arr
⊢ Array.size (if index ≥ Array.size arr then arr else set_elements (Array.set! arr index 1) (index + 1)) = Array.size arr

Therefore I added h1 and h2 in these two cases respectively.
How do I get rid of sorry for h1 and h2?
I am using Lean version 4.5.0-rc1