next n ih =>
rcases Nat.lt_or_eq_of_le $ Nat.le_of_lt_succ h with x_lt_n | x_eq_n
. specialize ih x_lt_n
  simp only [Array.range, Nat.fold, flip, Array.get_push]
  simp only [Array.range, flip] at ih
  split
  . exact ih
  . next x_ge_n =>
    exfalso
    have h_range_size : (Array.range n).size = n := Array.range_size
    simp only [Array.mkEmpty_eq, Array.range, flip] at h_range_size
    simp only [Array.mkEmpty_eq, h_range_size] at x_ge_n
    exact x_ge_n x_lt_n
. simp only [Array.range, Nat.fold, flip, Array.get_push]
  split
  . next x_lt_n =>
    exfalso
    have h_range_size : (Array.range n).size = n := Array.range_size
    simp only [Array.range, Array.mkEmpty_eq] at h_range_size
    simp only [x_eq_n, Array.mkEmpty_eq, h_range_size, Nat.lt_irrefl] at x_lt_n
  . rw [x_eq_n]
case succ
x n✝ : Nat
a✝ : ∀ (h : x < n✝), (Array.range n✝)[x] = x
h : x < n✝ + 1
⊢ (Array.range (n✝ + 1))[x] = x
no goals