internlm/Lean-Github huggingface dataset:
Theorem: Image.get!_push_colors
Proof 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
Proof 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)]
Theorem: Image.get!_push_colors
Proof 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
Proof 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)]
Theorem: Image.get!_push_colors
Proof 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]
Proof state after:
no goals
Theorem: Image.get!_push_colors
Proof 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]
Proof 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)]
Theorem: Image.get!_push_colors
Proof 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]
Proof 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)]
Theorem: Image.get!_push_colors
Proof 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
Proof 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)]
Theorem: Image.get!_push_colors
Proof 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]
Proof 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
Theorem: Image.get!_push_colors
Proof 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]
Proof 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)]
Theorem: Image.get!_push_colors
Proof 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
Proof 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)]
Theorem: Image.get!_push_colors
Proof 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
Proof 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)]
Theorem: Image.get!_push_colors
Proof 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
Proof 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)]
Theorem: Image.get!_push_colors
Proof 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
Proof 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)]
Theorem: Image.get!_push_colors
Proof 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
Proof 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)]
Theorem: Image.get!_push_colors
Proof 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
Proof 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)]
Theorem: Image.get!_push_colors
Proof 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
Proof 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)]