Theorem: Image.get!_push_colors (Ray/Render/Image.lean)

State before:
f : ℕ → Color UInt8
n o : ℕ
d : ByteArray
k : ℕ
lt : k < d.size + n * 4
⊢ (push_colors f n o d).get! k = if k < d.size then d.get! k else (f (o + (k - d.size) / 4))[↑(k - d.size)]
Tactic:
induction' n with n h generalizing d o
State after:
case zero
f : ℕ → Color UInt8
k o : ℕ
d : ByteArray
lt : k < d.size + 0 * 4
⊢ (push_colors f 0 o d).get! k = if k < d.size then d.get! k else (f (o + (k - d.size) / 4))[↑(k - d.size)]

case succ
f : ℕ → Color UInt8
k n : ℕ
h :
  ∀ (o : ℕ) (d : ByteArray),
    k < d.size + n * 4 →
      (push_colors f n o d).get! k = if k < d.size then d.get! k else (f (o + (k - d.size) / 4))[↑(k - d.size)]
o : ℕ
d : ByteArray
lt : k < d.size + (n + 1) * 4
⊢ (push_colors f (n + 1) o d).get! k = if k < d.size then d.get! k else (f (o + (k - d.size) / 4))[↑(k - d.size)]

State before:
case zero
f : ℕ → Color UInt8
k o : ℕ
d : ByteArray
lt : k < d.size + 0 * 4
⊢ (push_colors f 0 o d).get! k = if k < d.size then d.get! k else (f (o + (k - d.size) / 4))[↑(k - d.size)]
Tactic:
simp only [Nat.zero_eq, zero_mul, add_zero] at lt
State after:
case zero
f : ℕ → Color UInt8
k o : ℕ
d : ByteArray
lt : k < d.size
⊢ (push_colors f 0 o d).get! k = if k < d.size then d.get! k else (f (o + (k - d.size) / 4))[↑(k - d.size)]

State before:
case zero
f : ℕ → Color UInt8
k o : ℕ
d : ByteArray
lt : k < d.size
⊢ (push_colors f 0 o d).get! k = if k < d.size then d.get! k else (f (o + (k - d.size) / 4))[↑(k - d.size)]
Tactic:
simp only [Nat.zero_eq, push_colors, ↓reduceIte, lt, ↓reduceDite]
State after:
no goals

State before:
case succ
f : ℕ → Color UInt8
k n : ℕ
h :
  ∀ (o : ℕ) (d : ByteArray),
    k < d.size + n * 4 →
      (push_colors f n o d).get! k = if k < d.size then d.get! k else (f (o + (k - d.size) / 4))[↑(k - d.size)]
o : ℕ
d : ByteArray
lt : k < d.size + (n + 1) * 4
⊢ (push_colors f (n + 1) o d).get! k = if k < d.size then d.get! k else (f (o + (k - d.size) / 4))[↑(k - d.size)]
Tactic:
rw [push_colors]
State after:
case succ
f : ℕ → Color UInt8
k n : ℕ
h :
  ∀ (o : ℕ) (d : ByteArray),
    k < d.size + n * 4 →
      (push_colors f n o d).get! k = if k < d.size then d.get! k else (f (o + (k - d.size) / 4))[↑(k - d.size)]
o : ℕ
d : ByteArray
lt : k < d.size + (n + 1) * 4
⊢ (if n + 1 = 0 then d
        else
          let c := f o;
          push_colors f (n + 1 - 1) (o + 1) ((((d.push c.r).push c.g).push c.b).push c.a)).get!
      k =
    if k < d.size then d.get! k else (f (o + (k - d.size) / 4))[↑(k - d.size)]

State before:
case succ
f : ℕ → Color UInt8
k n : ℕ
h :
  ∀ (o : ℕ) (d : ByteArray),
    k < d.size + n * 4 →
      (push_colors f n o d).get! k = if k < d.size then d.get! k else (f (o + (k - d.size) / 4))[↑(k - d.size)]
o : ℕ
d : ByteArray
lt : k < d.size + (n + 1) * 4
⊢ (if n + 1 = 0 then d
        else
          let c := f o;
          push_colors f (n + 1 - 1) (o + 1) ((((d.push c.r).push c.g).push c.b).push c.a)).get!
      k =
    if k < d.size then d.get! k else (f (o + (k - d.size) / 4))[↑(k - d.size)]
Tactic:
simp only [Nat.succ_ne_zero, ↓reduceIte, Nat.succ_sub_succ_eq_sub, tsub_zero, dite_eq_ite]
State after:
case succ
f : ℕ → Color UInt8
k n : ℕ
h :
  ∀ (o : ℕ) (d : ByteArray),
    k < d.size + n * 4 →
      (push_colors f n o d).get! k = if k < d.size then d.get! k else (f (o + (k - d.size) / 4))[↑(k - d.size)]
o : ℕ
d : ByteArray
lt : k < d.size + (n + 1) * 4
⊢ (push_colors f n (o + 1) ((((d.push (f o).r).push (f o).g).push (f o).b).push (f o).a)).get! k =
    if k < d.size then d.get! k else (f (o + (k - d.size) / 4))[↑(k - d.size)]

State before:
case succ
f : ℕ → Color UInt8
k n : ℕ
h :
  ∀ (o : ℕ) (d : ByteArray),
    k < d.size + n * 4 →
      (push_colors f n o d).get! k = if k < d.size then d.get! k else (f (o + (k - d.size) / 4))[↑(k - d.size)]
o : ℕ
d : ByteArray
lt : k < d.size + (n + 1) * 4
⊢ (push_colors f n (o + 1) ((((d.push (f o).r).push (f o).g).push (f o).b).push (f o).a)).get! k =
    if k < d.size then d.get! k else (f (o + (k - d.size) / 4))[↑(k - d.size)]
Tactic:
simp only [Nat.succ_eq_add_one, add_one_mul, ← add_assoc] at lt
State after:
case succ
f : ℕ → Color UInt8
k n : ℕ
h :
  ∀ (o : ℕ) (d : ByteArray),
    k < d.size + n * 4 →
      (push_colors f n o d).get! k = if k < d.size then d.get! k else (f (o + (k - d.size) / 4))[↑(k - d.size)]
o : ℕ
d : ByteArray
lt : k < d.size + n * 4 + 4
⊢ (push_colors f n (o + 1) ((((d.push (f o).r).push (f o).g).push (f o).b).push (f o).a)).get! k =
    if k < d.size then d.get! k else (f (o + (k - d.size) / 4))[↑(k - d.size)]

State before:
case succ
f : ℕ → Color UInt8
k n : ℕ
h :
  ∀ (o : ℕ) (d : ByteArray),
    k < d.size + n * 4 →
      (push_colors f n o d).get! k = if k < d.size then d.get! k else (f (o + (k - d.size) / 4))[↑(k - d.size)]
o : ℕ
d : ByteArray
lt : k < d.size + n * 4 + 4
⊢ (push_colors f n (o + 1) ((((d.push (f o).r).push (f o).g).push (f o).b).push (f o).a)).get! k =
    if k < d.size then d.get! k else (f (o + (k - d.size) / 4))[↑(k - d.size)]
Tactic:
rw [h]
State after:
case succ
f : ℕ → Color UInt8
k n : ℕ
h :
  ∀ (o : ℕ) (d : ByteArray),
    k < d.size + n * 4 →
      (push_colors f n o d).get! k = if k < d.size then d.get! k else (f (o + (k - d.size) / 4))[↑(k - d.size)]
o : ℕ
d : ByteArray
lt : k < d.size + n * 4 + 4
⊢ (if k < ((((d.push (f o).r).push (f o).g).push (f o).b).push (f o).a).size then
      ((((d.push (f o).r).push (f o).g).push (f o).b).push (f o).a).get! k
    else
      (f
          (o + 1 +
            (k - ((((d.push (f o).r).push (f o).g).push (f o).b).push (f o).a).size) /
              4))[↑(k - ((((d.push (f o).r).push (f o).g).push (f o).b).push (f o).a).size)]) =
    if k < d.size then d.get! k else (f (o + (k - d.size) / 4))[↑(k - d.size)]

case succ.lt
f : ℕ → Color UInt8
k n : ℕ
h :
  ∀ (o : ℕ) (d : ByteArray),
    k < d.size + n * 4 →
      (push_colors f n o d).get! k = if k < d.size then d.get! k else (f (o + (k - d.size) / 4))[↑(k - d.size)]
o : ℕ
d : ByteArray
lt : k < d.size + n * 4 + 4
⊢ k < ((((d.push (f o).r).push (f o).g).push (f o).b).push (f o).a).size + n * 4

State before:
case succ
f : ℕ → Color UInt8
k n : ℕ
h :
  ∀ (o : ℕ) (d : ByteArray),
    k < d.size + n * 4 →
      (push_colors f n o d).get! k = if k < d.size then d.get! k else (f (o + (k - d.size) / 4))[↑(k - d.size)]
o : ℕ
d : ByteArray
lt : k < d.size + n * 4 + 4
⊢ (if k < ((((d.push (f o).r).push (f o).g).push (f o).b).push (f o).a).size then
      ((((d.push (f o).r).push (f o).g).push (f o).b).push (f o).a).get! k
    else
      (f
          (o + 1 +
            (k - ((((d.push (f o).r).push (f o).g).push (f o).b).push (f o).a).size) /
              4))[↑(k - ((((d.push (f o).r).push (f o).g).push (f o).b).push (f o).a).size)]) =
    if k < d.size then d.get! k else (f (o + (k - d.size) / 4))[↑(k - d.size)]
Tactic:
simp only [ByteArray.size_push, dite_eq_ite, ByteArray.get!_push, add_assoc]
State after:
case succ
f : ℕ → Color UInt8
k n : ℕ
h :
  ∀ (o : ℕ) (d : ByteArray),
    k < d.size + n * 4 →
      (push_colors f n o d).get! k = if k < d.size then d.get! k else (f (o + (k - d.size) / 4))[↑(k - d.size)]
o : ℕ
d : ByteArray
lt : k < d.size + n * 4 + 4
⊢ (if k < d.size + (1 + (1 + (1 + 1))) then
      if k < d.size + (1 + (1 + 1)) then
        if k < d.size + (1 + 1) then
          if k < d.size + 1 then if k < d.size then d.get! k else if k = d.size then (f o).r else default
          else if k = d.size + 1 then (f o).g else default
        else if k = d.size + (1 + 1) then (f o).b else default
      else if k = d.size + (1 + (1 + 1)) then (f o).a else default
    else (f (o + (1 + (k - (d.size + (1 + (1 + (1 + 1))))) / 4)))[↑(k - (d.size + (1 + (1 + (1 + 1)))))]) =
    if k < d.size then d.get! k else (f (o + (k - d.size) / 4))[↑(k - d.size)]

State before:
case succ
f : ℕ → Color UInt8
k n : ℕ
h :
  ∀ (o : ℕ) (d : ByteArray),
    k < d.size + n * 4 →
      (push_colors f n o d).get! k = if k < d.size then d.get! k else (f (o + (k - d.size) / 4))[↑(k - d.size)]
o : ℕ
d : ByteArray
lt : k < d.size + n * 4 + 4
⊢ (if k < d.size + (1 + (1 + (1 + 1))) then
      if k < d.size + (1 + (1 + 1)) then
        if k < d.size + (1 + 1) then
          if k < d.size + 1 then if k < d.size then d.get! k else if k = d.size then (f o).r else default
          else if k = d.size + 1 then (f o).g else default
        else if k = d.size + (1 + 1) then (f o).b else default
      else if k = d.size + (1 + (1 + 1)) then (f o).a else default
    else (f (o + (1 + (k - (d.size + (1 + (1 + (1 + 1))))) / 4)))[↑(k - (d.size + (1 + (1 + (1 + 1)))))]) =
    if k < d.size then d.get! k else (f (o + (k - d.size) / 4))[↑(k - d.size)]
Tactic:
norm_num
State after:
case succ
f : ℕ → Color UInt8
k n : ℕ
h :
  ∀ (o : ℕ) (d : ByteArray),
    k < d.size + n * 4 →
      (push_colors f n o d).get! k = if k < d.size then d.get! k else (f (o + (k - d.size) / 4))[↑(k - d.size)]
o : ℕ
d : ByteArray
lt : k < d.size + n * 4 + 4
⊢ (if k < d.size + 4 then
      if k < d.size + 3 then
        if k < d.size + 2 then
          if k < d.size + 1 then if k < d.size then d.get! k else if k = d.size then (f o).r else default
          else if k = d.size + 1 then (f o).g else default
        else if k = d.size + 2 then (f o).b else default
      else if k = d.size + 3 then (f o).a else default
    else (f (o + (1 + (k - (d.size + 4)) / 4)))[↑(k - (d.size + 4))]) =
    if k < d.size then d.get! k else (f (o + (k - d.size) / 4))[↑(k - d.size)]

State before:
case succ
f : ℕ → Color UInt8
k n : ℕ
h :
  ∀ (o : ℕ) (d : ByteArray),
    k < d.size + n * 4 →
      (push_colors f n o d).get! k = if k < d.size then d.get! k else (f (o + (k - d.size) / 4))[↑(k - d.size)]
o : ℕ
d : ByteArray
lt : k < d.size + n * 4 + 4
⊢ (if k < d.size + 4 then
      if k < d.size + 3 then
        if k < d.size + 2 then
          if k < d.size + 1 then if k < d.size then d.get! k else if k = d.size then (f o).r else default
          else if k = d.size + 1 then (f o).g else default
        else if k = d.size + 2 then (f o).b else default
      else if k = d.size + 3 then (f o).a else default
    else (f (o + (1 + (k - (d.size + 4)) / 4)))[↑(k - (d.size + 4))]) =
    if k < d.size then d.get! k else (f (o + (k - d.size) / 4))[↑(k - d.size)]
Tactic:
by_cases e0 : k = d.size
State after:
case pos
f : ℕ → Color UInt8
k n : ℕ
h :
  ∀ (o : ℕ) (d : ByteArray),
    k < d.size + n * 4 →
      (push_colors f n o d).get! k = if k < d.size then d.get! k else (f (o + (k - d.size) / 4))[↑(k - d.size)]
o : ℕ
d : ByteArray
lt : k < d.size + n * 4 + 4
e0 : k = d.size
⊢ (if k < d.size + 4 then
      if k < d.size + 3 then
        if k < d.size + 2 then
          if k < d.size + 1 then if k < d.size then d.get! k else if k = d.size then (f o).r else default
          else if k = d.size + 1 then (f o).g else default
        else if k = d.size + 2 then (f o).b else default
      else if k = d.size + 3 then (f o).a else default
    else (f (o + (1 + (k - (d.size + 4)) / 4)))[↑(k - (d.size + 4))]) =
    if k < d.size then d.get! k else (f (o + (k - d.size) / 4))[↑(k - d.size)]

case neg
f : ℕ → Color UInt8
k n : ℕ
h :
  ∀ (o : ℕ) (d : ByteArray),
    k < d.size + n * 4 →
      (push_colors f n o d).get! k = if k < d.size then d.get! k else (f (o + (k - d.size) / 4))[↑(k - d.size)]
o : ℕ
d : ByteArray
lt : k < d.size + n * 4 + 4
e0 : ¬k = d.size
⊢ (if k < d.size + 4 then
      if k < d.size + 3 then
        if k < d.size + 2 then
          if k < d.size + 1 then if k < d.size then d.get! k else if k = d.size then (f o).r else default
          else if k = d.size + 1 then (f o).g else default
        else if k = d.size + 2 then (f o).b else default
      else if k = d.size + 3 then (f o).a else default
    else (f (o + (1 + (k - (d.size + 4)) / 4)))[↑(k - (d.size + 4))]) =
    if k < d.size then d.get! k else (f (o + (k - d.size) / 4))[↑(k - d.size)]

State before:
case neg
f : ℕ → Color UInt8
k n : ℕ
h :
  ∀ (o : ℕ) (d : ByteArray),
    k < d.size + n * 4 →
      (push_colors f n o d).get! k = if k < d.size then d.get! k else (f (o + (k - d.size) / 4))[↑(k - d.size)]
o : ℕ
d : ByteArray
lt : k < d.size + n * 4 + 4
e0 : ¬k = d.size
⊢ (if k < d.size + 4 then
      if k < d.size + 3 then
        if k < d.size + 2 then
          if k < d.size + 1 then if k < d.size then d.get! k else if k = d.size then (f o).r else default
          else if k = d.size + 1 then (f o).g else default
        else if k = d.size + 2 then (f o).b else default
      else if k = d.size + 3 then (f o).a else default
    else (f (o + (1 + (k - (d.size + 4)) / 4)))[↑(k - (d.size + 4))]) =
    if k < d.size then d.get! k else (f (o + (k - d.size) / 4))[↑(k - d.size)]
Tactic:
by_cases e1 : k = d.size + 1
State after:
case pos
f : ℕ → Color UInt8
k n : ℕ
h :
  ∀ (o : ℕ) (d : ByteArray),
    k < d.size + n * 4 →
      (push_colors f n o d).get! k = if k < d.size then d.get! k else (f (o + (k - d.size) / 4))[↑(k - d.size)]
o : ℕ
d : ByteArray
lt : k < d.size + n * 4 + 4
e0 : ¬k = d.size
e1 : k = d.size + 1
⊢ (if k < d.size + 4 then
      if k < d.size + 3 then
        if k < d.size + 2 then
          if k < d.size + 1 then if k < d.size then d.get! k else if k = d.size then (f o).r else default
          else if k = d.size + 1 then (f o).g else default
        else if k = d.size + 2 then (f o).b else default
      else if k = d.size + 3 then (f o).a else default
    else (f (o + (1 + (k - (d.size + 4)) / 4)))[↑(k - (d.size + 4))]) =
    if k < d.size then d.get! k else (f (o + (k - d.size) / 4))[↑(k - d.size)]

case neg
f : ℕ → Color UInt8
k n : ℕ
h :
  ∀ (o : ℕ) (d : ByteArray),
    k < d.size + n * 4 →
      (push_colors f n o d).get! k = if k < d.size then d.get! k else (f (o + (k - d.size) / 4))[↑(k - d.size)]
o : ℕ
d : ByteArray
lt : k < d.size + n * 4 + 4
e0 : ¬k = d.size
e1 : ¬k = d.size + 1
⊢ (if k < d.size + 4 then
      if k < d.size + 3 then
        if k < d.size + 2 then
          if k < d.size + 1 then if k < d.size then d.get! k else if k = d.size then (f o).r else default
          else if k = d.size + 1 then (f o).g else default
        else if k = d.size + 2 then (f o).b else default
      else if k = d.size + 3 then (f o).a else default
    else (f (o + (1 + (k - (d.size + 4)) / 4)))[↑(k - (d.size + 4))]) =
    if k < d.size then d.get! k else (f (o + (k - d.size) / 4))[↑(k - d.size)]

State before:
case neg
f : ℕ → Color UInt8
k n : ℕ
h :
  ∀ (o : ℕ) (d : ByteArray),
    k < d.size + n * 4 →
      (push_colors f n o d).get! k = if k < d.size then d.get! k else (f (o + (k - d.size) / 4))[↑(k - d.size)]
o : ℕ
d : ByteArray
lt : k < d.size + n * 4 + 4
e0 : ¬k = d.size
e1 : ¬k = d.size + 1
⊢ (if k < d.size + 4 then
      if k < d.size + 3 then
        if k < d.size + 2 then
          if k < d.size + 1 then if k < d.size then d.get! k else if k = d.size then (f o).r else default
          else if k = d.size + 1 then (f o).g else default
        else if k = d.size + 2 then (f o).b else default
      else if k = d.size + 3 then (f o).a else default
    else (f (o + (1 + (k - (d.size + 4)) / 4)))[↑(k - (d.size + 4))]) =
    if k < d.size then d.get! k else (f (o + (k - d.size) / 4))[↑(k - d.size)]
Tactic:
by_cases e2 : k = d.size + 2
State after:
case pos
f : ℕ → Color UInt8
k n : ℕ
h :
  ∀ (o : ℕ) (d : ByteArray),
    k < d.size + n * 4 →
      (push_colors f n o d).get! k = if k < d.size then d.get! k else (f (o + (k - d.size) / 4))[↑(k - d.size)]
o : ℕ
d : ByteArray
lt : k < d.size + n * 4 + 4
e0 : ¬k = d.size
e1 : ¬k = d.size + 1
e2 : k = d.size + 2
⊢ (if k < d.size + 4 then
      if k < d.size + 3 then
        if k < d.size + 2 then
          if k < d.size + 1 then if k < d.size then d.get! k else if k = d.size then (f o).r else default
          else if k = d.size + 1 then (f o).g else default
        else if k = d.size + 2 then (f o).b else default
      else if k = d.size + 3 then (f o).a else default
    else (f (o + (1 + (k - (d.size + 4)) / 4)))[↑(k - (d.size + 4))]) =
    if k < d.size then d.get! k else (f (o + (k - d.size) / 4))[↑(k - d.size)]

case neg
f : ℕ → Color UInt8
k n : ℕ
h :
  ∀ (o : ℕ) (d : ByteArray),
    k < d.size + n * 4 →
      (push_colors f n o d).get! k = if k < d.size then d.get! k else (f (o + (k - d.size) / 4))[↑(k - d.size)]
o : ℕ
d : ByteArray
lt : k < d.size + n * 4 + 4
e0 : ¬k = d.size
e1 : ¬k = d.size + 1
e2 : ¬k = d.size + 2
⊢ (if k < d.size + 4 then
      if k < d.size + 3 then
        if k < d.size + 2 then
          if k < d.size + 1 then if k < d.size then d.get! k else if k = d.size then (f o).r else default
          else if k = d.size + 1 then (f o).g else default
        else if k = d.size + 2 then (f o).b else default
      else if k = d.size + 3 then (f o).a else default
    else (f (o + (1 + (k - (d.size + 4)) / 4)))[↑(k - (d.size + 4))]) =
    if k < d.size then d.get! k else (f (o + (k - d.size) / 4))[↑(k - d.size)]

State before:
case neg
f : ℕ → Color UInt8
k n : ℕ
h :
  ∀ (o : ℕ) (d : ByteArray),
    k < d.size + n * 4 →
      (push_colors f n o d).get! k = if k < d.size then d.get! k else (f (o + (k - d.size) / 4))[↑(k - d.size)]
o : ℕ
d : ByteArray
lt : k < d.size + n * 4 + 4
e0 : ¬k = d.size
e1 : ¬k = d.size + 1
e2 : ¬k = d.size + 2
⊢ (if k < d.size + 4 then
      if k < d.size + 3 then
        if k < d.size + 2 then
          if k < d.size + 1 then if k < d.size then d.get! k else if k = d.size then (f o).r else default
          else if k = d.size + 1 then (f o).g else default
        else if k = d.size + 2 then (f o).b else default
      else if k = d.size + 3 then (f o).a else default
    else (f (o + (1 + (k - (d.size + 4)) / 4)))[↑(k - (d.size + 4))]) =
    if k < d.size then d.get! k else (f (o + (k - d.size) / 4))[↑(k - d.size)]
Tactic:
by_cases e3 : k = d.size + 3
State after:
case pos
f : ℕ → Color UInt8
k n : ℕ
h :
  ∀ (o : ℕ) (d : ByteArray),
    k < d.size + n * 4 →
      (push_colors f n o d).get! k = if k < d.size then d.get! k else (f (o + (k - d.size) / 4))[↑(k - d.size)]
o : ℕ
d : ByteArray
lt : k < d.size + n * 4 + 4
e0 : ¬k = d.size
e1 : ¬k = d.size + 1
e2 : ¬k = d.size + 2
e3 : k = d.size + 3
⊢ (if k < d.size + 4 then
      if k < d.size + 3 then
        if k < d.size + 2 then
          if k < d.size + 1 then if k < d.size then d.get! k else if k = d.size then (f o).r else default
          else if k = d.size + 1 then (f o).g else default
        else if k = d.size + 2 then (f o).b else default
      else if k = d.size + 3 then (f o).a else default
    else (f (o + (1 + (k - (d.size + 4)) / 4)))[↑(k - (d.size + 4))]) =
    if k < d.size then d.get! k else (f (o + (k - d.size) / 4))[↑(k - d.size)]

case neg
f : ℕ → Color UInt8
k n : ℕ
h :
  ∀ (o : ℕ) (d : ByteArray),
    k < d.size + n * 4 →
      (push_colors f n o d).get! k = if k < d.size then d.get! k else (f (o + (k - d.size) / 4))[↑(k - d.size)]
o : ℕ
d : ByteArray
lt : k < d.size + n * 4 + 4
e0 : ¬k = d.size
e1 : ¬k = d.size + 1
e2 : ¬k = d.size + 2
e3 : ¬k = d.size + 3
⊢ (if k < d.size + 4 then
      if k < d.size + 3 then
        if k < d.size + 2 then
          if k < d.size + 1 then if k < d.size then d.get! k else if k = d.size then (f o).r else default
          else if k = d.size + 1 then (f o).g else default
        else if k = d.size + 2 then (f o).b else default
      else if k = d.size + 3 then (f o).a else default
    else (f (o + (1 + (k - (d.size + 4)) / 4)))[↑(k - (d.size + 4))]) =
    if k < d.size then d.get! k else (f (o + (k - d.size) / 4))[↑(k - d.size)]

State before:
case neg
f : ℕ → Color UInt8
k n : ℕ
h :
  ∀ (o : ℕ) (d : ByteArray),
    k < d.size + n * 4 →
      (push_colors f n o d).get! k = if k < d.size then d.get! k else (f (o + (k - d.size) / 4))[↑(k - d.size)]
o : ℕ
d : ByteArray
lt : k < d.size + n * 4 + 4
e0 : ¬k = d.size
e1 : ¬k = d.size + 1
e2 : ¬k = d.size + 2
e3 : ¬k = d.size + 3
⊢ (if k < d.size + 4 then
      if k < d.size + 3 then
        if k < d.size + 2 then
          if k < d.size + 1 then if k < d.size then d.get! k else if k = d.size then (f o).r else default
          else if k = d.size + 1 then (f o).g else default
        else if k = d.size + 2 then (f o).b else default
      else if k = d.size + 3 then (f o).a else default
    else (f (o + (1 + (k - (d.size + 4)) / 4)))[↑(k - (d.size + 4))]) =
    if k < d.size then d.get! k else (f (o + (k - d.size) / 4))[↑(k - d.size)]
Tactic:
simp only [← ne_eq] at e0 e1 e2 e3
State after:
case neg
f : ℕ → Color UInt8
k n : ℕ
h :
  ∀ (o : ℕ) (d : ByteArray),
    k < d.size + n * 4 →
      (push_colors f n o d).get! k = if k < d.size then d.get! k else (f (o + (k - d.size) / 4))[↑(k - d.size)]
o : ℕ
d : ByteArray
lt : k < d.size + n * 4 + 4
e0 : k ≠ d.size
e1 : k ≠ d.size + 1
e2 : k ≠ d.size + 2
e3 : k ≠ d.size + 3
⊢ (if k < d.size + 4 then
      if k < d.size + 3 then
        if k < d.size + 2 then
          if k < d.size + 1 then if k < d.size then d.get! k else if k = d.size then (f o).r else default
          else if k = d.size + 1 then (f o).g else default
        else if k = d.size + 2 then (f o).b else default
      else if k = d.size + 3 then (f o).a else default
    else (f (o + (1 + (k - (d.size + 4)) / 4)))[↑(k - (d.size + 4))]) =
    if k < d.size then d.get! k else (f (o + (k - d.size) / 4))[↑(k - d.size)]

State before:
case neg
f : ℕ → Color UInt8
k n : ℕ
h :
  ∀ (o : ℕ) (d : ByteArray),
    k < d.size + n * 4 →
      (push_colors f n o d).get! k = if k < d.size then d.get! k else (f (o + (k - d.size) / 4))[↑(k - d.size)]
o : ℕ
d : ByteArray
lt : k < d.size + n * 4 + 4
e0 : k ≠ d.size
e1 : k ≠ d.size + 1
e2 : k ≠ d.size + 2
e3 : k ≠ d.size + 3
⊢ (if k < d.size + 4 then
      if k < d.size + 3 then
        if k < d.size + 2 then
          if k < d.size + 1 then if k < d.size then d.get! k else if k = d.size then (f o).r else default
          else if k = d.size + 1 then (f o).g else default
        else if k = d.size + 2 then (f o).b else default
      else if k = d.size + 3 then (f o).a else default
    else (f (o + (1 + (k - (d.size + 4)) / 4)))[↑(k - (d.size + 4))]) =
    if k < d.size then d.get! k else (f (o + (k - d.size) / 4))[↑(k - d.size)]
Tactic:
by_cases lt0 : k < d.size
State after:
case pos
f : ℕ → Color UInt8
k n : ℕ
h :
  ∀ (o : ℕ) (d : ByteArray),
    k < d.size + n * 4 →
      (push_colors f n o d).get! k = if k < d.size then d.get! k else (f (o + (k - d.size) / 4))[↑(k - d.size)]
o : ℕ
d : ByteArray
lt : k < d.size + n * 4 + 4
e0 : k ≠ d.size
e1 : k ≠ d.size + 1
e2 : k ≠ d.size + 2
e3 : k ≠ d.size + 3
lt0 : k < d.size
⊢ (if k < d.size + 4 then
      if k < d.size + 3 then
        if k < d.size + 2 then
          if k < d.size + 1 then if k < d.size then d.get! k else if k = d.size then (f o).r else default
          else if k = d.size + 1 then (f o).g else default
        else if k = d.size + 2 then (f o).b else default
      else if k = d.size + 3 then (f o).a else default
    else (f (o + (1 + (k - (d.size + 4)) / 4)))[↑(k - (d.size + 4))]) =
    if k < d.size then d.get! k else (f (o + (k - d.size) / 4))[↑(k - d.size)]

case neg
f : ℕ → Color UInt8
k n : ℕ
h :
  ∀ (o : ℕ) (d : ByteArray),
    k < d.size + n * 4 →
      (push_colors f n o d).get! k = if k < d.size then d.get! k else (f (o + (k - d.size) / 4))[↑(k - d.size)]
o : ℕ
d : ByteArray
lt : k < d.size + n * 4 + 4
e0 : k ≠ d.size
e1 : k ≠ d.size + 1
e2 : k ≠ d.size + 2
e3 : k ≠ d.size + 3
lt0 : ¬k < d.size
⊢ (if k < d.size + 4 then
      if k < d.size + 3 then
        if k < d.size + 2 then
          if k < d.size + 1 then if k < d.size then d.get! k else if k = d.size then (f o).r else default
          else if k = d.size + 1 then (f o).g else default
        else if k = d.size + 2 then (f o).b else default
      else if k = d.size + 3 then (f o).a else default
    else (f (o + (1 + (k - (d.size + 4)) / 4)))[↑(k - (d.size + 4))]) =
    if k < d.size then d.get! k else (f (o + (k - d.size) / 4))[↑(k - d.size)]

State before:
case pos
f : ℕ → Color UInt8
k n : ℕ
h :
  ∀ (o : ℕ) (d : ByteArray),
    k < d.size + n * 4 →
      (push_colors f n o d).get! k = if k < d.size then d.get! k else (f (o + (k - d.size) / 4))[↑(k - d.size)]
o : ℕ
d : ByteArray
lt : k < d.size + n * 4 + 4
e0 : k = d.size
⊢ (if k < d.size + 4 then
      if k < d.size + 3 then
        if k < d.size + 2 then
          if k < d.size + 1 then if k < d.size then d.get! k else if k = d.size then (f o).r else default
          else if k = d.size + 1 then (f o).g else default
        else if k = d.size + 2 then (f o).b else default
      else if k = d.size + 3 then (f o).a else default
    else (f (o + (1 + (k - (d.size + 4)) / 4)))[↑(k - (d.size + 4))]) =
    if k < d.size then d.get! k else (f (o + (k - d.size) / 4))[↑(k - d.size)]
Tactic:
simp [e0]
State after:
no goals

State before:
case pos
f : ℕ → Color UInt8
k n : ℕ
h :
  ∀ (o : ℕ) (d : ByteArray),
    k < d.size + n * 4 →
      (push_colors f n o d).get! k = if k < d.size then d.get! k else (f (o + (k - d.size) / 4))[↑(k - d.size)]
o : ℕ
d : ByteArray
lt : k < d.size + n * 4 + 4
e0 : ¬k = d.size
e1 : k = d.size + 1
⊢ (if k < d.size + 4 then
      if k < d.size + 3 then
        if k < d.size + 2 then
          if k < d.size + 1 then if k < d.size then d.get! k else if k = d.size then (f o).r else default
          else if k = d.size + 1 then (f o).g else default
        else if k = d.size + 2 then (f o).b else default
      else if k = d.size + 3 then (f o).a else default
    else (f (o + (1 + (k - (d.size + 4)) / 4)))[↑(k - (d.size + 4))]) =
    if k < d.size then d.get! k else (f (o + (k - d.size) / 4))[↑(k - d.size)]
Tactic:
simp [e1]
State after:
no goals

State before:
case pos
f : ℕ → Color UInt8
k n : ℕ
h :
  ∀ (o : ℕ) (d : ByteArray),
    k < d.size + n * 4 →
      (push_colors f n o d).get! k = if k < d.size then d.get! k else (f (o + (k - d.size) / 4))[↑(k - d.size)]
o : ℕ
d : ByteArray
lt : k < d.size + n * 4 + 4
e0 : ¬k = d.size
e1 : ¬k = d.size + 1
e2 : k = d.size + 2
⊢ (if k < d.size + 4 then
      if k < d.size + 3 then
        if k < d.size + 2 then
          if k < d.size + 1 then if k < d.size then d.get! k else if k = d.size then (f o).r else default
          else if k = d.size + 1 then (f o).g else default
        else if k = d.size + 2 then (f o).b else default
      else if k = d.size + 3 then (f o).a else default
    else (f (o + (1 + (k - (d.size + 4)) / 4)))[↑(k - (d.size + 4))]) =
    if k < d.size then d.get! k else (f (o + (k - d.size) / 4))[↑(k - d.size)]
Tactic:
simp [e2]
State after:
no goals

State before:
case pos
f : ℕ → Color UInt8
k n : ℕ
h :
  ∀ (o : ℕ) (d : ByteArray),
    k < d.size + n * 4 →
      (push_colors f n o d).get! k = if k < d.size then d.get! k else (f (o + (k - d.size) / 4))[↑(k - d.size)]
o : ℕ
d : ByteArray
lt : k < d.size + n * 4 + 4
e0 : ¬k = d.size
e1 : ¬k = d.size + 1
e2 : ¬k = d.size + 2
e3 : k = d.size + 3
⊢ (if k < d.size + 4 then
      if k < d.size + 3 then
        if k < d.size + 2 then
          if k < d.size + 1 then if k < d.size then d.get! k else if k = d.size then (f o).r else default
          else if k = d.size + 1 then (f o).g else default
        else if k = d.size + 2 then (f o).b else default
      else if k = d.size + 3 then (f o).a else default
    else (f (o + (1 + (k - (d.size + 4)) / 4)))[↑(k - (d.size + 4))]) =
    if k < d.size then d.get! k else (f (o + (k - d.size) / 4))[↑(k - d.size)]
Tactic:
simp [e3]
State after:
no goals

State before:
case pos
f : ℕ → Color UInt8
k n : ℕ
h :
  ∀ (o : ℕ) (d : ByteArray),
    k < d.size + n * 4 →
      (push_colors f n o d).get! k = if k < d.size then d.get! k else (f (o + (k - d.size) / 4))[↑(k - d.size)]
o : ℕ
d : ByteArray
lt : k < d.size + n * 4 + 4
e0 : k ≠ d.size
e1 : k ≠ d.size + 1
e2 : k ≠ d.size + 2
e3 : k ≠ d.size + 3
lt0 : k < d.size
⊢ (if k < d.size + 4 then
      if k < d.size + 3 then
        if k < d.size + 2 then
          if k < d.size + 1 then if k < d.size then d.get! k else if k = d.size then (f o).r else default
          else if k = d.size + 1 then (f o).g else default
        else if k = d.size + 2 then (f o).b else default
      else if k = d.size + 3 then (f o).a else default
    else (f (o + (1 + (k - (d.size + 4)) / 4)))[↑(k - (d.size + 4))]) =
    if k < d.size then d.get! k else (f (o + (k - d.size) / 4))[↑(k - d.size)]
Tactic:
have lt1 : k < d.size + 1 := by omega
State after:
case pos
f : ℕ → Color UInt8
k n : ℕ
h :
  ∀ (o : ℕ) (d : ByteArray),
    k < d.size + n * 4 →
      (push_colors f n o d).get! k = if k < d.size then d.get! k else (f (o + (k - d.size) / 4))[↑(k - d.size)]
o : ℕ
d : ByteArray
lt : k < d.size + n * 4 + 4
e0 : k ≠ d.size
e1 : k ≠ d.size + 1
e2 : k ≠ d.size + 2
e3 : k ≠ d.size + 3
lt0 : k < d.size
lt1 : k < d.size + 1
⊢ (if k < d.size + 4 then
      if k < d.size + 3 then
        if k < d.size + 2 then
          if k < d.size + 1 then if k < d.size then d.get! k else if k = d.size then (f o).r else default
          else if k = d.size + 1 then (f o).g else default
        else if k = d.size + 2 then (f o).b else default
      else if k = d.size + 3 then (f o).a else default
    else (f (o + (1 + (k - (d.size + 4)) / 4)))[↑(k - (d.size + 4))]) =
    if k < d.size then d.get! k else (f (o + (k - d.size) / 4))[↑(k - d.size)]

State before:
case pos
f : ℕ → Color UInt8
k n : ℕ
h :
  ∀ (o : ℕ) (d : ByteArray),
    k < d.size + n * 4 →
      (push_colors f n o d).get! k = if k < d.size then d.get! k else (f (o + (k - d.size) / 4))[↑(k - d.size)]
o : ℕ
d : ByteArray
lt : k < d.size + n * 4 + 4
e0 : k ≠ d.size
e1 : k ≠ d.size + 1
e2 : k ≠ d.size + 2
e3 : k ≠ d.size + 3
lt0 : k < d.size
lt1 : k < d.size + 1
⊢ (if k < d.size + 4 then
      if k < d.size + 3 then
        if k < d.size + 2 then
          if k < d.size + 1 then if k < d.size then d.get! k else if k = d.size then (f o).r else default
          else if k = d.size + 1 then (f o).g else default
        else if k = d.size + 2 then (f o).b else default
      else if k = d.size + 3 then (f o).a else default
    else (f (o + (1 + (k - (d.size + 4)) / 4)))[↑(k - (d.size + 4))]) =
    if k < d.size then d.get! k else (f (o + (k - d.size) / 4))[↑(k - d.size)]
Tactic:
have lt2 : k < d.size + 2 := by omega
State after:
case pos
f : ℕ → Color UInt8
k n : ℕ
h :
  ∀ (o : ℕ) (d : ByteArray),
    k < d.size + n * 4 →
      (push_colors f n o d).get! k = if k < d.size then d.get! k else (f (o + (k - d.size) / 4))[↑(k - d.size)]
o : ℕ
d : ByteArray
lt : k < d.size + n * 4 + 4
e0 : k ≠ d.size
e1 : k ≠ d.size + 1
e2 : k ≠ d.size + 2
e3 : k ≠ d.size + 3
lt0 : k < d.size
lt1 : k < d.size + 1
lt2 : k < d.size + 2
⊢ (if k < d.size + 4 then
      if k < d.size + 3 then
        if k < d.size + 2 then
          if k < d.size + 1 then if k < d.size then d.get! k else if k = d.size then (f o).r else default
          else if k = d.size + 1 then (f o).g else default
        else if k = d.size + 2 then (f o).b else default
      else if k = d.size + 3 then (f o).a else default
    else (f (o + (1 + (k - (d.size + 4)) / 4)))[↑(k - (d.size + 4))]) =
    if k < d.size then d.get! k else (f (o + (k - d.size) / 4))[↑(k - d.size)]

State before:
case pos
f : ℕ → Color UInt8
k n : ℕ
h :
  ∀ (o : ℕ) (d : ByteArray),
    k < d.size + n * 4 →
      (push_colors f n o d).get! k = if k < d.size then d.get! k else (f (o + (k - d.size) / 4))[↑(k - d.size)]
o : ℕ
d : ByteArray
lt : k < d.size + n * 4 + 4
e0 : k ≠ d.size
e1 : k ≠ d.size + 1
e2 : k ≠ d.size + 2
e3 : k ≠ d.size + 3
lt0 : k < d.size
lt1 : k < d.size + 1
lt2 : k < d.size + 2
⊢ (if k < d.size + 4 then
      if k < d.size + 3 then
        if k < d.size + 2 then
          if k < d.size + 1 then if k < d.size then d.get! k else if k = d.size then (f o).r else default
          else if k = d.size + 1 then (f o).g else default
        else if k = d.size + 2 then (f o).b else default
      else if k = d.size + 3 then (f o).a else default
    else (f (o + (1 + (k - (d.size + 4)) / 4)))[↑(k - (d.size + 4))]) =
    if k < d.size then d.get! k else (f (o + (k - d.size) / 4))[↑(k - d.size)]
Tactic:
have lt3 : k < d.size + 3 := by omega
State after:
case pos
f : ℕ → Color UInt8
k n : ℕ
h :
  ∀ (o : ℕ) (d : ByteArray),
    k < d.size + n * 4 →
      (push_colors f n o d).get! k = if k < d.size then d.get! k else (f (o + (k - d.size) / 4))[↑(k - d.size)]
o : ℕ
d : ByteArray
lt : k < d.size + n * 4 + 4
e0 : k ≠ d.size
e1 : k ≠ d.size + 1
e2 : k ≠ d.size + 2
e3 : k ≠ d.size + 3
lt0 : k < d.size
lt1 : k < d.size + 1
lt2 : k < d.size + 2
lt3 : k < d.size + 3
⊢ (if k < d.size + 4 then
      if k < d.size + 3 then
        if k < d.size + 2 then
          if k < d.size + 1 then if k < d.size then d.get! k else if k = d.size then (f o).r else default
          else if k = d.size + 1 then (f o).g else default
        else if k = d.size + 2 then (f o).b else default
      else if k = d.size + 3 then (f o).a else default
    else (f (o + (1 + (k - (d.size + 4)) / 4)))[↑(k - (d.size + 4))]) =
    if k < d.size then d.get! k else (f (o + (k - d.size) / 4))[↑(k - d.size)]

State before:
case pos
f : ℕ → Color UInt8
k n : ℕ
h :
  ∀ (o : ℕ) (d : ByteArray),
    k < d.size + n * 4 →
      (push_colors f n o d).get! k = if k < d.size then d.get! k else (f (o + (k - d.size) / 4))[↑(k - d.size)]
o : ℕ
d : ByteArray
lt : k < d.size + n * 4 + 4
e0 : k ≠ d.size
e1 : k ≠ d.size + 1
e2 : k ≠ d.size + 2
e3 : k ≠ d.size + 3
lt0 : k < d.size
lt1 : k < d.size + 1
lt2 : k < d.size + 2
lt3 : k < d.size + 3
⊢ (if k < d.size + 4 then
      if k < d.size + 3 then
        if k < d.size + 2 then
          if k < d.size + 1 then if k < d.size then d.get! k else if k = d.size then (f o).r else default
          else if k = d.size + 1 then (f o).g else default
        else if k = d.size + 2 then (f o).b else default
      else if k = d.size + 3 then (f o).a else default
    else (f (o + (1 + (k - (d.size + 4)) / 4)))[↑(k - (d.size + 4))]) =
    if k < d.size then d.get! k else (f (o + (k - d.size) / 4))[↑(k - d.size)]
Tactic:
have lt4 : k < d.size + 4 := by omega
State after:
case pos
f : ℕ → Color UInt8
k n : ℕ
h :
  ∀ (o : ℕ) (d : ByteArray),
    k < d.size + n * 4 →
      (push_colors f n o d).get! k = if k < d.size then d.get! k else (f (o + (k - d.size) / 4))[↑(k - d.size)]
o : ℕ
d : ByteArray
lt : k < d.size + n * 4 + 4
e0 : k ≠ d.size
e1 : k ≠ d.size + 1
e2 : k ≠ d.size + 2
e3 : k ≠ d.size + 3
lt0 : k < d.size
lt1 : k < d.size + 1
lt2 : k < d.size + 2
lt3 : k < d.size + 3
lt4 : k < d.size + 4
⊢ (if k < d.size + 4 then
      if k < d.size + 3 then
        if k < d.size + 2 then
          if k < d.size + 1 then if k < d.size then d.get! k else if k = d.size then (f o).r else default
          else if k = d.size + 1 then (f o).g else default
        else if k = d.size + 2 then (f o).b else default
      else if k = d.size + 3 then (f o).a else default
    else (f (o + (1 + (k - (d.size + 4)) / 4)))[↑(k - (d.size + 4))]) =
    if k < d.size then d.get! k else (f (o + (k - d.size) / 4))[↑(k - d.size)]

State before:
case pos
f : ℕ → Color UInt8
k n : ℕ
h :
  ∀ (o : ℕ) (d : ByteArray),
    k < d.size + n * 4 →
      (push_colors f n o d).get! k = if k < d.size then d.get! k else (f (o + (k - d.size) / 4))[↑(k - d.size)]
o : ℕ
d : ByteArray
lt : k < d.size + n * 4 + 4
e0 : k ≠ d.size
e1 : k ≠ d.size + 1
e2 : k ≠ d.size + 2
e3 : k ≠ d.size + 3
lt0 : k < d.size
lt1 : k < d.size + 1
lt2 : k < d.size + 2
lt3 : k < d.size + 3
lt4 : k < d.size + 4
⊢ (if k < d.size + 4 then
      if k < d.size + 3 then
        if k < d.size + 2 then
          if k < d.size + 1 then if k < d.size then d.get! k else if k = d.size then (f o).r else default
          else if k = d.size + 1 then (f o).g else default
        else if k = d.size + 2 then (f o).b else default
      else if k = d.size + 3 then (f o).a else default
    else (f (o + (1 + (k - (d.size + 4)) / 4)))[↑(k - (d.size + 4))]) =
    if k < d.size then d.get! k else (f (o + (k - d.size) / 4))[↑(k - d.size)]
Tactic:
simp only [lt0, lt1, lt2, lt3, lt4, if_true]
State after:
no goals

State before:
f : ℕ → Color UInt8
k n : ℕ
h :
  ∀ (o : ℕ) (d : ByteArray),
    k < d.size + n * 4 →
      (push_colors f n o d).get! k = if k < d.size then d.get! k else (f (o + (k - d.size) / 4))[↑(k - d.size)]
o : ℕ
d : ByteArray
lt : k < d.size + n * 4 + 4
e0 : k ≠ d.size
e1 : k ≠ d.size + 1
e2 : k ≠ d.size + 2
e3 : k ≠ d.size + 3
lt0 : k < d.size
⊢ k < d.size + 1
Tactic:
omega
State after:
no goals

State before:
f : ℕ → Color UInt8
k n : ℕ
h :
  ∀ (o : ℕ) (d : ByteArray),
    k < d.size + n * 4 →
      (push_colors f n o d).get! k = if k < d.size then d.get! k else (f (o + (k - d.size) / 4))[↑(k - d.size)]
o : ℕ
d : ByteArray
lt : k < d.size + n * 4 + 4
e0 : k ≠ d.size
e1 : k ≠ d.size + 1
e2 : k ≠ d.size + 2
e3 : k ≠ d.size + 3
lt0 : k < d.size
lt1 : k < d.size + 1
⊢ k < d.size + 2
Tactic:
omega
State after:
no goals

State before:
f : ℕ → Color UInt8
k n : ℕ
h :
  ∀ (o : ℕ) (d : ByteArray),
    k < d.size + n * 4 →
      (push_colors f n o d).get! k = if k < d.size then d.get! k else (f (o + (k - d.size) / 4))[↑(k - d.size)]
o : ℕ
d : ByteArray
lt : k < d.size + n * 4 + 4
e0 : k ≠ d.size
e1 : k ≠ d.size + 1
e2 : k ≠ d.size + 2
e3 : k ≠ d.size + 3
lt0 : k < d.size
lt1 : k < d.size + 1
lt2 : k < d.size + 2
⊢ k < d.size + 3
Tactic:
omega
State after:
no goals

State before:
f : ℕ → Color UInt8
k n : ℕ
h :
  ∀ (o : ℕ) (d : ByteArray),
    k < d.size + n * 4 →
      (push_colors f n o d).get! k = if k < d.size then d.get! k else (f (o + (k - d.size) / 4))[↑(k - d.size)]
o : ℕ
d : ByteArray
lt : k < d.size + n * 4 + 4
e0 : k ≠ d.size
e1 : k ≠ d.size + 1
e2 : k ≠ d.size + 2
e3 : k ≠ d.size + 3
lt0 : k < d.size
lt1 : k < d.size + 1
lt2 : k < d.size + 2
lt3 : k < d.size + 3
⊢ k < d.size + 4
Tactic:
omega
State after:
no goals

State before:
case neg
f : ℕ → Color UInt8
k n : ℕ
h :
  ∀ (o : ℕ) (d : ByteArray),
    k < d.size + n * 4 →
      (push_colors f n o d).get! k = if k < d.size then d.get! k else (f (o + (k - d.size) / 4))[↑(k - d.size)]
o : ℕ
d : ByteArray
lt : k < d.size + n * 4 + 4
e0 : k ≠ d.size
e1 : k ≠ d.size + 1
e2 : k ≠ d.size + 2
e3 : k ≠ d.size + 3
lt0 : ¬k < d.size
⊢ (if k < d.size + 4 then
      if k < d.size + 3 then
        if k < d.size + 2 then
          if k < d.size + 1 then if k < d.size then d.get! k else if k = d.size then (f o).r else default
          else if k = d.size + 1 then (f o).g else default
        else if k = d.size + 2 then (f o).b else default
      else if k = d.size + 3 then (f o).a else default
    else (f (o + (1 + (k - (d.size + 4)) / 4)))[↑(k - (d.size + 4))]) =
    if k < d.size then d.get! k else (f (o + (k - d.size) / 4))[↑(k - d.size)]
Tactic:
have ge : d.size + 4 ≤ k := by omega
State after:
case neg
f : ℕ → Color UInt8
k n : ℕ
h :
  ∀ (o : ℕ) (d : ByteArray),
    k < d.size + n * 4 →
      (push_colors f n o d).get! k = if k < d.size then d.get! k else (f (o + (k - d.size) / 4))[↑(k - d.size)]
o : ℕ
d : ByteArray
lt : k < d.size + n * 4 + 4
e0 : k ≠ d.size
e1 : k ≠ d.size + 1
e2 : k ≠ d.size + 2
e3 : k ≠ d.size + 3
lt0 : ¬k < d.size
ge : d.size + 4 ≤ k
⊢ (if k < d.size + 4 then
      if k < d.size + 3 then
        if k < d.size + 2 then
          if k < d.size + 1 then if k < d.size then d.get! k else if k = d.size then (f o).r else default
          else if k = d.size + 1 then (f o).g else default
        else if k = d.size + 2 then (f o).b else default
      else if k = d.size + 3 then (f o).a else default
    else (f (o + (1 + (k - (d.size + 4)) / 4)))[↑(k - (d.size + 4))]) =
    if k < d.size then d.get! k else (f (o + (k - d.size) / 4))[↑(k - d.size)]

State before:
case neg
f : ℕ → Color UInt8
k n : ℕ
h :
  ∀ (o : ℕ) (d : ByteArray),
    k < d.size + n * 4 →
      (push_colors f n o d).get! k = if k < d.size then d.get! k else (f (o + (k - d.size) / 4))[↑(k - d.size)]
o : ℕ
d : ByteArray
lt : k < d.size + n * 4 + 4
e0 : k ≠ d.size
e1 : k ≠ d.size + 1
e2 : k ≠ d.size + 2
e3 : k ≠ d.size + 3
lt0 : ¬k < d.size
ge : d.size + 4 ≤ k
⊢ (if k < d.size + 4 then
      if k < d.size + 3 then
        if k < d.size + 2 then
          if k < d.size + 1 then if k < d.size then d.get! k else if k = d.size then (f o).r else default
          else if k = d.size + 1 then (f o).g else default
        else if k = d.size + 2 then (f o).b else default
      else if k = d.size + 3 then (f o).a else default
    else (f (o + (1 + (k - (d.size + 4)) / 4)))[↑(k - (d.size + 4))]) =
    if k < d.size then d.get! k else (f (o + (k - d.size) / 4))[↑(k - d.size)]
Tactic:
have e0 : o + (1 + (k - (d.size + 4)) / 4) = o + (k - d.size) / 4 := by omega
State after:
case neg
f : ℕ → Color UInt8
k n : ℕ
h :
  ∀ (o : ℕ) (d : ByteArray),
    k < d.size + n * 4 →
      (push_colors f n o d).get! k = if k < d.size then d.get! k else (f (o + (k - d.size) / 4))[↑(k - d.size)]
o : ℕ
d : ByteArray
lt : k < d.size + n * 4 + 4
e0✝ : k ≠ d.size
e1 : k ≠ d.size + 1
e2 : k ≠ d.size + 2
e3 : k ≠ d.size + 3
lt0 : ¬k < d.size
ge : d.size + 4 ≤ k
e0 : o + (1 + (k - (d.size + 4)) / 4) = o + (k - d.size) / 4
⊢ (if k < d.size + 4 then
      if k < d.size + 3 then
        if k < d.size + 2 then
          if k < d.size + 1 then if k < d.size then d.get! k else if k = d.size then (f o).r else default
          else if k = d.size + 1 then (f o).g else default
        else if k = d.size + 2 then (f o).b else default
      else if k = d.size + 3 then (f o).a else default
    else (f (o + (1 + (k - (d.size + 4)) / 4)))[↑(k - (d.size + 4))]) =
    if k < d.size then d.get! k else (f (o + (k - d.size) / 4))[↑(k - d.size)]

State before:
case neg
f : ℕ → Color UInt8
k n : ℕ
h :
  ∀ (o : ℕ) (d : ByteArray),
    k < d.size + n * 4 →
      (push_colors f n o d).get! k = if k < d.size then d.get! k else (f (o + (k - d.size) / 4))[↑(k - d.size)]
o : ℕ
d : ByteArray
lt : k < d.size + n * 4 + 4
e0✝ : k ≠ d.size
e1 : k ≠ d.size + 1
e2 : k ≠ d.size + 2
e3 : k ≠ d.size + 3
lt0 : ¬k < d.size
ge : d.size + 4 ≤ k
e0 : o + (1 + (k - (d.size + 4)) / 4) = o + (k - d.size) / 4
⊢ (if k < d.size + 4 then
      if k < d.size + 3 then
        if k < d.size + 2 then
          if k < d.size + 1 then if k < d.size then d.get! k else if k = d.size then (f o).r else default
          else if k = d.size + 1 then (f o).g else default
        else if k = d.size + 2 then (f o).b else default
      else if k = d.size + 3 then (f o).a else default
    else (f (o + (1 + (k - (d.size + 4)) / 4)))[↑(k - (d.size + 4))]) =
    if k < d.size then d.get! k else (f (o + (k - d.size) / 4))[↑(k - d.size)]
Tactic:
have e1 : k - d.size = k - (d.size + 4) + 4 := by omega
State after:
case neg
f : ℕ → Color UInt8
k n : ℕ
h :
  ∀ (o : ℕ) (d : ByteArray),
    k < d.size + n * 4 →
      (push_colors f n o d).get! k = if k < d.size then d.get! k else (f (o + (k - d.size) / 4))[↑(k - d.size)]
o : ℕ
d : ByteArray
lt : k < d.size + n * 4 + 4
e0✝ : k ≠ d.size
e1✝ : k ≠ d.size + 1
e2 : k ≠ d.size + 2
e3 : k ≠ d.size + 3
lt0 : ¬k < d.size
ge : d.size + 4 ≤ k
e0 : o + (1 + (k - (d.size + 4)) / 4) = o + (k - d.size) / 4
e1 : k - d.size = k - (d.size + 4) + 4
⊢ (if k < d.size + 4 then
      if k < d.size + 3 then
        if k < d.size + 2 then
          if k < d.size + 1 then if k < d.size then d.get! k else if k = d.size then (f o).r else default
          else if k = d.size + 1 then (f o).g else default
        else if k = d.size + 2 then (f o).b else default
      else if k = d.size + 3 then (f o).a else default
    else (f (o + (1 + (k - (d.size + 4)) / 4)))[↑(k - (d.size + 4))]) =
    if k < d.size then d.get! k else (f (o + (k - d.size) / 4))[↑(k - d.size)]

State before:
case neg
f : ℕ → Color UInt8
k n : ℕ
h :
  ∀ (o : ℕ) (d : ByteArray),
    k < d.size + n * 4 →
      (push_colors f n o d).get! k = if k < d.size then d.get! k else (f (o + (k - d.size) / 4))[↑(k - d.size)]
o : ℕ
d : ByteArray
lt : k < d.size + n * 4 + 4
e0✝ : k ≠ d.size
e1✝ : k ≠ d.size + 1
e2 : k ≠ d.size + 2
e3 : k ≠ d.size + 3
lt0 : ¬k < d.size
ge : d.size + 4 ≤ k
e0 : o + (1 + (k - (d.size + 4)) / 4) = o + (k - d.size) / 4
e1 : k - d.size = k - (d.size + 4) + 4
⊢ (if k < d.size + 4 then
      if k < d.size + 3 then
        if k < d.size + 2 then
          if k < d.size + 1 then if k < d.size then d.get! k else if k = d.size then (f o).r else default
          else if k = d.size + 1 then (f o).g else default
        else if k = d.size + 2 then (f o).b else default
      else if k = d.size + 3 then (f o).a else default
    else (f (o + (1 + (k - (d.size + 4)) / 4)))[↑(k - (d.size + 4))]) =
    if k < d.size then d.get! k else (f (o + (k - d.size) / 4))[↑(k - d.size)]
Tactic:
simp only [not_lt.mpr ge, ↓reduceIte, Nat.succ_eq_add_one, e0, e1, lt0, Nat.cast_add,
  Fin.natCast_self, add_zero]
State after:
no goals

State before:
f : ℕ → Color UInt8
k n : ℕ
h :
  ∀ (o : ℕ) (d : ByteArray),
    k < d.size + n * 4 →
      (push_colors f n o d).get! k = if k < d.size then d.get! k else (f (o + (k - d.size) / 4))[↑(k - d.size)]
o : ℕ
d : ByteArray
lt : k < d.size + n * 4 + 4
e0 : k ≠ d.size
e1 : k ≠ d.size + 1
e2 : k ≠ d.size + 2
e3 : k ≠ d.size + 3
lt0 : ¬k < d.size
⊢ d.size + 4 ≤ k
Tactic:
omega
State after:
no goals

State before:
f : ℕ → Color UInt8
k n : ℕ
h :
  ∀ (o : ℕ) (d : ByteArray),
    k < d.size + n * 4 →
      (push_colors f n o d).get! k = if k < d.size then d.get! k else (f (o + (k - d.size) / 4))[↑(k - d.size)]
o : ℕ
d : ByteArray
lt : k < d.size + n * 4 + 4
e0 : k ≠ d.size
e1 : k ≠ d.size + 1
e2 : k ≠ d.size + 2
e3 : k ≠ d.size + 3
lt0 : ¬k < d.size
ge : d.size + 4 ≤ k
⊢ o + (1 + (k - (d.size + 4)) / 4) = o + (k - d.size) / 4
Tactic:
omega
State after:
no goals

State before:
f : ℕ → Color UInt8
k n : ℕ
h :
  ∀ (o : ℕ) (d : ByteArray),
    k < d.size + n * 4 →
      (push_colors f n o d).get! k = if k < d.size then d.get! k else (f (o + (k - d.size) / 4))[↑(k - d.size)]
o : ℕ
d : ByteArray
lt : k < d.size + n * 4 + 4
e0✝ : k ≠ d.size
e1 : k ≠ d.size + 1
e2 : k ≠ d.size + 2
e3 : k ≠ d.size + 3
lt0 : ¬k < d.size
ge : d.size + 4 ≤ k
e0 : o + (1 + (k - (d.size + 4)) / 4) = o + (k - d.size) / 4
⊢ k - d.size = k - (d.size + 4) + 4
Tactic:
omega
State after:
no goals

State before:
case succ.lt
f : ℕ → Color UInt8
k n : ℕ
h :
  ∀ (o : ℕ) (d : ByteArray),
    k < d.size + n * 4 →
      (push_colors f n o d).get! k = if k < d.size then d.get! k else (f (o + (k - d.size) / 4))[↑(k - d.size)]
o : ℕ
d : ByteArray
lt : k < d.size + n * 4 + 4
⊢ k < ((((d.push (f o).r).push (f o).g).push (f o).b).push (f o).a).size + n * 4
Tactic:
simp only [ByteArray.size_push]
State after:
case succ.lt
f : ℕ → Color UInt8
k n : ℕ
h :
  ∀ (o : ℕ) (d : ByteArray),
    k < d.size + n * 4 →
      (push_colors f n o d).get! k = if k < d.size then d.get! k else (f (o + (k - d.size) / 4))[↑(k - d.size)]
o : ℕ
d : ByteArray
lt : k < d.size + n * 4 + 4
⊢ k < d.size + 1 + 1 + 1 + 1 + n * 4

State before:
case succ.lt
f : ℕ → Color UInt8
k n : ℕ
h :
  ∀ (o : ℕ) (d : ByteArray),
    k < d.size + n * 4 →
      (push_colors f n o d).get! k = if k < d.size then d.get! k else (f (o + (k - d.size) / 4))[↑(k - d.size)]
o : ℕ
d : ByteArray
lt : k < d.size + n * 4 + 4
⊢ k < d.size + 1 + 1 + 1 + 1 + n * 4
Tactic:
omega
State after:
no goals