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