internlm/Lean-Github huggingface dataset:
Theorem: Image.get_push_colors
Proof state before:
f : ℕ → Color UInt8
n o : ℕ
d : ByteArray
k : Fin (push_colors f n o d).size
⊢ (push_colors f n o d)[k] = if h : ↑k < d.size then d[k] else (f (o + (↑k - d.size) / 4))[↑(↑k - d.size)]
Tactic:
simp only [getElem_fin, ByteArray.getElemNat_eq_get!, dite_eq_ite]
Proof state after:
f : ℕ → Color UInt8
n o : ℕ
d : ByteArray
k : Fin (push_colors f n o d).size
⊢ (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)]
Theorem: Image.get_push_colors
Proof state before:
f : ℕ → Color UInt8
n o : ℕ
d : ByteArray
k : Fin (push_colors f n o d).size
⊢ (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:
apply get!_push_colors
Proof state after:
case lt
f : ℕ → Color UInt8
n o : ℕ
d : ByteArray
k : Fin (push_colors f n o d).size
⊢ ↑k < d.size + n * 4
Theorem: Image.get_push_colors
Proof state before:
case lt
f : ℕ → Color UInt8
n o : ℕ
d : ByteArray
k : Fin (push_colors f n o d).size
⊢ ↑k < d.size + n * 4
Tactic:
convert k.prop
Proof state after:
case h.e'_4
f : ℕ → Color UInt8
n o : ℕ
d : ByteArray
k : Fin (push_colors f n o d).size
⊢ d.size + n * 4 = (push_colors f n o d).size
Theorem: Image.get_push_colors
Proof state before:
case h.e'_4
f : ℕ → Color UInt8
n o : ℕ
d : ByteArray
k : Fin (push_colors f n o d).size
⊢ d.size + n * 4 = (push_colors f n o d).size
Tactic:
simp only [size_push_colors]
Proof state after:
no goals
Theorem: Image.n0_lt_n
Proof state before:
n chunk : ℕ
h : ¬n ≤ max 1 chunk
⊢ n / 2 < n
Tactic:
simp only [le_max_iff] at h
Proof state after:
n chunk : ℕ
h : ¬(n ≤ 1 ∨ n ≤ chunk)
⊢ n / 2 < n
Theorem: Image.n0_lt_n
Proof state before:
n chunk : ℕ
h : ¬(n ≤ 1 ∨ n ≤ chunk)
⊢ n / 2 < n
Tactic:
omega
Proof state after:
no goals
Theorem: Image.n1_lt_n
Proof state before:
n chunk : ℕ
h : ¬n ≤ max 1 chunk
⊢ n - n / 2 < n
Tactic:
simp only [le_max_iff] at h
Proof state after:
n chunk : ℕ
h : ¬(n ≤ 1 ∨ n ≤ chunk)
⊢ n - n / 2 < n
Theorem: Image.n1_lt_n
Proof state before:
n chunk : ℕ
h : ¬(n ≤ 1 ∨ n ≤ chunk)
⊢ n - n / 2 < n
Tactic:
omega
Proof state after:
no goals
Theorem: Image.size_parallel_colors'
Proof state before:
f : ℕ → Color UInt8
n o chunk : ℕ
⊢ (parallel_colors' f n o chunk).size = n * 4
Tactic:
induction' n using Nat.strong_induction_on with n i generalizing o
Proof state after:
case h
f : ℕ → Color UInt8
chunk n : ℕ
i : ∀ m < n, ∀ (o : ℕ), (parallel_colors' f m o chunk).size = m * 4
o : ℕ
⊢ (parallel_colors' f n o chunk).size = n * 4
Theorem: Image.size_parallel_colors'
Proof state before:
case h
f : ℕ → Color UInt8
chunk n : ℕ
i : ∀ m < n, ∀ (o : ℕ), (parallel_colors' f m o chunk).size = m * 4
o : ℕ
⊢ (parallel_colors' f n o chunk).size = n * 4
Tactic:
rw [parallel_colors']
Proof state after:
case h
f : ℕ → Color UInt8
chunk n : ℕ
i : ∀ m < n, ∀ (o : ℕ), (parallel_colors' f m o chunk).size = m * 4
o : ℕ
⊢ (if n ≤ max 1 chunk then push_colors f n o (ByteArray.mkEmpty n)
      else
        let n0 := n / 2;
        let t0 := Task.spawn fun x => parallel_colors' f n0 o chunk;
        let t1 := Task.spawn fun x => parallel_colors' f (n - n0) (o + n0) chunk;
        t0.get ++ t1.get).size =
    n * 4
Theorem: Image.size_parallel_colors'
Proof state before:
case h
f : ℕ → Color UInt8
chunk n : ℕ
i : ∀ m < n, ∀ (o : ℕ), (parallel_colors' f m o chunk).size = m * 4
o : ℕ
⊢ (if n ≤ max 1 chunk then push_colors f n o (ByteArray.mkEmpty n)
      else
        let n0 := n / 2;
        let t0 := Task.spawn fun x => parallel_colors' f n0 o chunk;
        let t1 := Task.spawn fun x => parallel_colors' f (n - n0) (o + n0) chunk;
        t0.get ++ t1.get).size =
    n * 4
Tactic:
by_cases h : n ≤ max 1 chunk
Proof state after:
case pos
f : ℕ → Color UInt8
chunk n : ℕ
i : ∀ m < n, ∀ (o : ℕ), (parallel_colors' f m o chunk).size = m * 4
o : ℕ
h : n ≤ max 1 chunk
⊢ (if n ≤ max 1 chunk then push_colors f n o (ByteArray.mkEmpty n)
      else
        let n0 := n / 2;
        let t0 := Task.spawn fun x => parallel_colors' f n0 o chunk;
        let t1 := Task.spawn fun x => parallel_colors' f (n - n0) (o + n0) chunk;
        t0.get ++ t1.get).size =
    n * 4

case neg
f : ℕ → Color UInt8
chunk n : ℕ
i : ∀ m < n, ∀ (o : ℕ), (parallel_colors' f m o chunk).size = m * 4
o : ℕ
h : ¬n ≤ max 1 chunk
⊢ (if n ≤ max 1 chunk then push_colors f n o (ByteArray.mkEmpty n)
      else
        let n0 := n / 2;
        let t0 := Task.spawn fun x => parallel_colors' f n0 o chunk;
        let t1 := Task.spawn fun x => parallel_colors' f (n - n0) (o + n0) chunk;
        t0.get ++ t1.get).size =
    n * 4
Theorem: Image.size_parallel_colors'
Proof state before:
case pos
f : ℕ → Color UInt8
chunk n : ℕ
i : ∀ m < n, ∀ (o : ℕ), (parallel_colors' f m o chunk).size = m * 4
o : ℕ
h : n ≤ max 1 chunk
⊢ (if n ≤ max 1 chunk then push_colors f n o (ByteArray.mkEmpty n)
      else
        let n0 := n / 2;
        let t0 := Task.spawn fun x => parallel_colors' f n0 o chunk;
        let t1 := Task.spawn fun x => parallel_colors' f (n - n0) (o + n0) chunk;
        t0.get ++ t1.get).size =
    n * 4
Tactic:
simp only [h, if_true, size_push_colors, ByteArray.size_mkEmpty, zero_add]
Proof state after:
no goals
Theorem: Image.size_parallel_colors'
Proof state before:
case neg
f : ℕ → Color UInt8
chunk n : ℕ
i : ∀ m < n, ∀ (o : ℕ), (parallel_colors' f m o chunk).size = m * 4
o : ℕ
h : ¬n ≤ max 1 chunk
⊢ (if n ≤ max 1 chunk then push_colors f n o (ByteArray.mkEmpty n)
      else
        let n0 := n / 2;
        let t0 := Task.spawn fun x => parallel_colors' f n0 o chunk;
        let t1 := Task.spawn fun x => parallel_colors' f (n - n0) (o + n0) chunk;
        t0.get ++ t1.get).size =
    n * 4
Tactic:
simp only [h, if_false, Task.spawn, ByteArray.size_append, i _ (n0_lt_n h), i _ (n1_lt_n h)]
Proof state after:
case neg
f : ℕ → Color UInt8
chunk n : ℕ
i : ∀ m < n, ∀ (o : ℕ), (parallel_colors' f m o chunk).size = m * 4
o : ℕ
h : ¬n ≤ max 1 chunk
⊢ n / 2 * 4 + (n - n / 2) * 4 = n * 4
Theorem: Image.size_parallel_colors'
Proof state before:
case neg
f : ℕ → Color UInt8
chunk n : ℕ
i : ∀ m < n, ∀ (o : ℕ), (parallel_colors' f m o chunk).size = m * 4
o : ℕ
h : ¬n ≤ max 1 chunk
⊢ n / 2 * 4 + (n - n / 2) * 4 = n * 4
Tactic:
omega
Proof state after:
no goals
Theorem: Image.get!_parallel_colors'
Proof state before:
f : ℕ → Color UInt8
n o chunk k : ℕ
lt : k < n * 4
⊢ (parallel_colors' f n o chunk).get! k = (f (o + k / 4))[↑k]
Tactic:
have four : ((4 : ℕ) : Fin 4) = 0 := by decide
Proof state after:
f : ℕ → Color UInt8
n o chunk k : ℕ
lt : k < n * 4
four : ↑4 = 0
⊢ (parallel_colors' f n o chunk).get! k = (f (o + k / 4))[↑k]
Theorem: Image.get!_parallel_colors'
Proof state before:
f : ℕ → Color UInt8
n o chunk k : ℕ
lt : k < n * 4
four : ↑4 = 0
⊢ (parallel_colors' f n o chunk).get! k = (f (o + k / 4))[↑k]
Tactic:
induction' n using Nat.strong_induction_on with n i generalizing o k
Proof state after:
case h
f : ℕ → Color UInt8
chunk : ℕ
four : ↑4 = 0
n : ℕ
i : ∀ m < n, ∀ (o k : ℕ), k < m * 4 → (parallel_colors' f m o chunk).get! k = (f (o + k / 4))[↑k]
o k : ℕ
lt : k < n * 4
⊢ (parallel_colors' f n o chunk).get! k = (f (o + k / 4))[↑k]
Theorem: Image.get!_parallel_colors'
Proof state before:
case h
f : ℕ → Color UInt8
chunk : ℕ
four : ↑4 = 0
n : ℕ
i : ∀ m < n, ∀ (o k : ℕ), k < m * 4 → (parallel_colors' f m o chunk).get! k = (f (o + k / 4))[↑k]
o k : ℕ
lt : k < n * 4
⊢ (parallel_colors' f n o chunk).get! k = (f (o + k / 4))[↑k]
Tactic:
rw [parallel_colors']
Proof state after:
case h
f : ℕ → Color UInt8
chunk : ℕ
four : ↑4 = 0
n : ℕ
i : ∀ m < n, ∀ (o k : ℕ), k < m * 4 → (parallel_colors' f m o chunk).get! k = (f (o + k / 4))[↑k]
o k : ℕ
lt : k < n * 4
⊢ (if n ≤ max 1 chunk then push_colors f n o (ByteArray.mkEmpty n)
        else
          let n0 := n / 2;
          let t0 := Task.spawn fun x => parallel_colors' f n0 o chunk;
          let t1 := Task.spawn fun x => parallel_colors' f (n - n0) (o + n0) chunk;
          t0.get ++ t1.get).get!
      k =
    (f (o + k / 4))[↑k]
Theorem: Image.get!_parallel_colors'
Proof state before:
case h
f : ℕ → Color UInt8
chunk : ℕ
four : ↑4 = 0
n : ℕ
i : ∀ m < n, ∀ (o k : ℕ), k < m * 4 → (parallel_colors' f m o chunk).get! k = (f (o + k / 4))[↑k]
o k : ℕ
lt : k < n * 4
⊢ (if n ≤ max 1 chunk then push_colors f n o (ByteArray.mkEmpty n)
        else
          let n0 := n / 2;
          let t0 := Task.spawn fun x => parallel_colors' f n0 o chunk;
          let t1 := Task.spawn fun x => parallel_colors' f (n - n0) (o + n0) chunk;
          t0.get ++ t1.get).get!
      k =
    (f (o + k / 4))[↑k]
Tactic:
by_cases h : n ≤ max 1 chunk
Proof state after:
case pos
f : ℕ → Color UInt8
chunk : ℕ
four : ↑4 = 0
n : ℕ
i : ∀ m < n, ∀ (o k : ℕ), k < m * 4 → (parallel_colors' f m o chunk).get! k = (f (o + k / 4))[↑k]
o k : ℕ
lt : k < n * 4
h : n ≤ max 1 chunk
⊢ (if n ≤ max 1 chunk then push_colors f n o (ByteArray.mkEmpty n)
        else
          let n0 := n / 2;
          let t0 := Task.spawn fun x => parallel_colors' f n0 o chunk;
          let t1 := Task.spawn fun x => parallel_colors' f (n - n0) (o + n0) chunk;
          t0.get ++ t1.get).get!
      k =
    (f (o + k / 4))[↑k]

case neg
f : ℕ → Color UInt8
chunk : ℕ
four : ↑4 = 0
n : ℕ
i : ∀ m < n, ∀ (o k : ℕ), k < m * 4 → (parallel_colors' f m o chunk).get! k = (f (o + k / 4))[↑k]
o k : ℕ
lt : k < n * 4
h : ¬n ≤ max 1 chunk
⊢ (if n ≤ max 1 chunk then push_colors f n o (ByteArray.mkEmpty n)
        else
          let n0 := n / 2;
          let t0 := Task.spawn fun x => parallel_colors' f n0 o chunk;
          let t1 := Task.spawn fun x => parallel_colors' f (n - n0) (o + n0) chunk;
          t0.get ++ t1.get).get!
      k =
    (f (o + k / 4))[↑k]
Theorem: Image.get!_parallel_colors'
Proof state before:
f : ℕ → Color UInt8
n o chunk k : ℕ
lt : k < n * 4
⊢ ↑4 = 0
Tactic:
decide
Proof state after:
no goals
Theorem: Image.get!_parallel_colors'
Proof state before:
case pos
f : ℕ → Color UInt8
chunk : ℕ
four : ↑4 = 0
n : ℕ
i : ∀ m < n, ∀ (o k : ℕ), k < m * 4 → (parallel_colors' f m o chunk).get! k = (f (o + k / 4))[↑k]
o k : ℕ
lt : k < n * 4
h : n ≤ max 1 chunk
⊢ (if n ≤ max 1 chunk then push_colors f n o (ByteArray.mkEmpty n)
        else
          let n0 := n / 2;
          let t0 := Task.spawn fun x => parallel_colors' f n0 o chunk;
          let t1 := Task.spawn fun x => parallel_colors' f (n - n0) (o + n0) chunk;
          t0.get ++ t1.get).get!
      k =
    (f (o + k / 4))[↑k]
Tactic:
simp only [h, if_true, Task.spawn]
Proof state after:
case pos
f : ℕ → Color UInt8
chunk : ℕ
four : ↑4 = 0
n : ℕ
i : ∀ m < n, ∀ (o k : ℕ), k < m * 4 → (parallel_colors' f m o chunk).get! k = (f (o + k / 4))[↑k]
o k : ℕ
lt : k < n * 4
h : n ≤ max 1 chunk
⊢ (push_colors f n o (ByteArray.mkEmpty n)).get! k = (f (o + k / 4))[↑k]
Theorem: Image.get!_parallel_colors'
Proof state before:
case pos
f : ℕ → Color UInt8
chunk : ℕ
four : ↑4 = 0
n : ℕ
i : ∀ m < n, ∀ (o k : ℕ), k < m * 4 → (parallel_colors' f m o chunk).get! k = (f (o + k / 4))[↑k]
o k : ℕ
lt : k < n * 4
h : n ≤ max 1 chunk
⊢ (push_colors f n o (ByteArray.mkEmpty n)).get! k = (f (o + k / 4))[↑k]
Tactic:
rw [get!_push_colors]
Proof state after:
case pos
f : ℕ → Color UInt8
chunk : ℕ
four : ↑4 = 0
n : ℕ
i : ∀ m < n, ∀ (o k : ℕ), k < m * 4 → (parallel_colors' f m o chunk).get! k = (f (o + k / 4))[↑k]
o k : ℕ
lt : k < n * 4
h : n ≤ max 1 chunk
⊢ (if k < (ByteArray.mkEmpty n).size then (ByteArray.mkEmpty n).get! k
    else (f (o + (k - (ByteArray.mkEmpty n).size) / 4))[↑(k - (ByteArray.mkEmpty n).size)]) =
    (f (o + k / 4))[↑k]

case pos.lt
f : ℕ → Color UInt8
chunk : ℕ
four : ↑4 = 0
n : ℕ
i : ∀ m < n, ∀ (o k : ℕ), k < m * 4 → (parallel_colors' f m o chunk).get! k = (f (o + k / 4))[↑k]
o k : ℕ
lt : k < n * 4
h : n ≤ max 1 chunk
⊢ k < (ByteArray.mkEmpty n).size + n * 4
Theorem: Image.get!_parallel_colors'
Proof state before:
case pos
f : ℕ → Color UInt8
chunk : ℕ
four : ↑4 = 0
n : ℕ
i : ∀ m < n, ∀ (o k : ℕ), k < m * 4 → (parallel_colors' f m o chunk).get! k = (f (o + k / 4))[↑k]
o k : ℕ
lt : k < n * 4
h : n ≤ max 1 chunk
⊢ (if k < (ByteArray.mkEmpty n).size then (ByteArray.mkEmpty n).get! k
    else (f (o + (k - (ByteArray.mkEmpty n).size) / 4))[↑(k - (ByteArray.mkEmpty n).size)]) =
    (f (o + k / 4))[↑k]
Tactic:
simp only [ByteArray.size_mkEmpty, not_lt_zero', ↓reduceIte, tsub_zero]
Proof state after:
no goals
Theorem: Image.get!_parallel_colors'
Proof state before:
case pos.lt
f : ℕ → Color UInt8
chunk : ℕ
four : ↑4 = 0
n : ℕ
i : ∀ m < n, ∀ (o k : ℕ), k < m * 4 → (parallel_colors' f m o chunk).get! k = (f (o + k / 4))[↑k]
o k : ℕ
lt : k < n * 4
h : n ≤ max 1 chunk
⊢ k < (ByteArray.mkEmpty n).size + n * 4
Tactic:
simpa only [ByteArray.size_mkEmpty, zero_add]
Proof state after:
no goals
Theorem: Image.get!_parallel_colors'
Proof state before:
case neg
f : ℕ → Color UInt8
chunk : ℕ
four : ↑4 = 0
n : ℕ
i : ∀ m < n, ∀ (o k : ℕ), k < m * 4 → (parallel_colors' f m o chunk).get! k = (f (o + k / 4))[↑k]
o k : ℕ
lt : k < n * 4
h : ¬n ≤ max 1 chunk
⊢ (if n ≤ max 1 chunk then push_colors f n o (ByteArray.mkEmpty n)
        else
          let n0 := n / 2;
          let t0 := Task.spawn fun x => parallel_colors' f n0 o chunk;
          let t1 := Task.spawn fun x => parallel_colors' f (n - n0) (o + n0) chunk;
          t0.get ++ t1.get).get!
      k =
    (f (o + k / 4))[↑k]
Tactic:
simp only [h, if_false, Task.spawn, ByteArray.get!_append, size_parallel_colors']
Proof state after:
case neg
f : ℕ → Color UInt8
chunk : ℕ
four : ↑4 = 0
n : ℕ
i : ∀ m < n, ∀ (o k : ℕ), k < m * 4 → (parallel_colors' f m o chunk).get! k = (f (o + k / 4))[↑k]
o k : ℕ
lt : k < n * 4
h : ¬n ≤ max 1 chunk
⊢ (if k < n / 2 * 4 then (parallel_colors' f (n / 2) o chunk).get! k
    else (parallel_colors' f (n - n / 2) (o + n / 2) chunk).get! (k - n / 2 * 4)) =
    (f (o + k / 4))[↑k]
Theorem: Image.get!_parallel_colors'
Proof state before:
case neg
f : ℕ → Color UInt8
chunk : ℕ
four : ↑4 = 0
n : ℕ
i : ∀ m < n, ∀ (o k : ℕ), k < m * 4 → (parallel_colors' f m o chunk).get! k = (f (o + k / 4))[↑k]
o k : ℕ
lt : k < n * 4
h : ¬n ≤ max 1 chunk
⊢ (if k < n / 2 * 4 then (parallel_colors' f (n / 2) o chunk).get! k
    else (parallel_colors' f (n - n / 2) (o + n / 2) chunk).get! (k - n / 2 * 4)) =
    (f (o + k / 4))[↑k]
Tactic:
simp only [le_max_iff, not_or, not_le] at h
Proof state after:
case neg
f : ℕ → Color UInt8
chunk : ℕ
four : ↑4 = 0
n : ℕ
i : ∀ m < n, ∀ (o k : ℕ), k < m * 4 → (parallel_colors' f m o chunk).get! k = (f (o + k / 4))[↑k]
o k : ℕ
lt : k < n * 4
h : 1 < n ∧ chunk < n
⊢ (if k < n / 2 * 4 then (parallel_colors' f (n / 2) o chunk).get! k
    else (parallel_colors' f (n - n / 2) (o + n / 2) chunk).get! (k - n / 2 * 4)) =
    (f (o + k / 4))[↑k]
Theorem: Image.get!_parallel_colors'
Proof state before:
case neg
f : ℕ → Color UInt8
chunk : ℕ
four : ↑4 = 0
n : ℕ
i : ∀ m < n, ∀ (o k : ℕ), k < m * 4 → (parallel_colors' f m o chunk).get! k = (f (o + k / 4))[↑k]
o k : ℕ
lt : k < n * 4
h : 1 < n ∧ chunk < n
⊢ (if k < n / 2 * 4 then (parallel_colors' f (n / 2) o chunk).get! k
    else (parallel_colors' f (n - n / 2) (o + n / 2) chunk).get! (k - n / 2 * 4)) =
    (f (o + k / 4))[↑k]
Tactic:
by_cases c : k < n/2 * 4
Proof state after:
case pos
f : ℕ → Color UInt8
chunk : ℕ
four : ↑4 = 0
n : ℕ
i : ∀ m < n, ∀ (o k : ℕ), k < m * 4 → (parallel_colors' f m o chunk).get! k = (f (o + k / 4))[↑k]
o k : ℕ
lt : k < n * 4
h : 1 < n ∧ chunk < n
c : k < n / 2 * 4
⊢ (if k < n / 2 * 4 then (parallel_colors' f (n / 2) o chunk).get! k
    else (parallel_colors' f (n - n / 2) (o + n / 2) chunk).get! (k - n / 2 * 4)) =
    (f (o + k / 4))[↑k]

case neg
f : ℕ → Color UInt8
chunk : ℕ
four : ↑4 = 0
n : ℕ
i : ∀ m < n, ∀ (o k : ℕ), k < m * 4 → (parallel_colors' f m o chunk).get! k = (f (o + k / 4))[↑k]
o k : ℕ
lt : k < n * 4
h : 1 < n ∧ chunk < n
c : ¬k < n / 2 * 4
⊢ (if k < n / 2 * 4 then (parallel_colors' f (n / 2) o chunk).get! k
    else (parallel_colors' f (n - n / 2) (o + n / 2) chunk).get! (k - n / 2 * 4)) =
    (f (o + k / 4))[↑k]
Theorem: Image.get!_parallel_colors'
Proof state before:
case pos
f : ℕ → Color UInt8
chunk : ℕ
four : ↑4 = 0
n : ℕ
i : ∀ m < n, ∀ (o k : ℕ), k < m * 4 → (parallel_colors' f m o chunk).get! k = (f (o + k / 4))[↑k]
o k : ℕ
lt : k < n * 4
h : 1 < n ∧ chunk < n
c : k < n / 2 * 4
⊢ (if k < n / 2 * 4 then (parallel_colors' f (n / 2) o chunk).get! k
    else (parallel_colors' f (n - n / 2) (o + n / 2) chunk).get! (k - n / 2 * 4)) =
    (f (o + k / 4))[↑k]
Tactic:
simp only [c, ↓reduceIte]
Proof state after:
case pos
f : ℕ → Color UInt8
chunk : ℕ
four : ↑4 = 0
n : ℕ
i : ∀ m < n, ∀ (o k : ℕ), k < m * 4 → (parallel_colors' f m o chunk).get! k = (f (o + k / 4))[↑k]
o k : ℕ
lt : k < n * 4
h : 1 < n ∧ chunk < n
c : k < n / 2 * 4
⊢ (parallel_colors' f (n / 2) o chunk).get! k = (f (o + k / 4))[↑k]
Theorem: Image.get!_parallel_colors'
Proof state before:
case pos
f : ℕ → Color UInt8
chunk : ℕ
four : ↑4 = 0
n : ℕ
i : ∀ m < n, ∀ (o k : ℕ), k < m * 4 → (parallel_colors' f m o chunk).get! k = (f (o + k / 4))[↑k]
o k : ℕ
lt : k < n * 4
h : 1 < n ∧ chunk < n
c : k < n / 2 * 4
⊢ (parallel_colors' f (n / 2) o chunk).get! k = (f (o + k / 4))[↑k]
Tactic:
rw [i _ (by omega) _ _ (by omega)]
Proof state after:
no goals
Theorem: Image.get!_parallel_colors'
Proof state before:
f : ℕ → Color UInt8
chunk : ℕ
four : ↑4 = 0
n : ℕ
i : ∀ m < n, ∀ (o k : ℕ), k < m * 4 → (parallel_colors' f m o chunk).get! k = (f (o + k / 4))[↑k]
o k : ℕ
lt : k < n * 4
h : 1 < n ∧ chunk < n
c : k < n / 2 * 4
⊢ n / 2 < n
Tactic:
omega
Proof state after:
no goals
Theorem: Image.get!_parallel_colors'
Proof state before:
f : ℕ → Color UInt8
chunk : ℕ
four : ↑4 = 0
n : ℕ
i : ∀ m < n, ∀ (o k : ℕ), k < m * 4 → (parallel_colors' f m o chunk).get! k = (f (o + k / 4))[↑k]
o k : ℕ
lt : k < n * 4
h : 1 < n ∧ chunk < n
c : k < n / 2 * 4
⊢ k < n / 2 * 4
Tactic:
omega
Proof state after:
no goals
Theorem: Image.get!_parallel_colors'
Proof state before:
case neg
f : ℕ → Color UInt8
chunk : ℕ
four : ↑4 = 0
n : ℕ
i : ∀ m < n, ∀ (o k : ℕ), k < m * 4 → (parallel_colors' f m o chunk).get! k = (f (o + k / 4))[↑k]
o k : ℕ
lt : k < n * 4
h : 1 < n ∧ chunk < n
c : ¬k < n / 2 * 4
⊢ (if k < n / 2 * 4 then (parallel_colors' f (n / 2) o chunk).get! k
    else (parallel_colors' f (n - n / 2) (o + n / 2) chunk).get! (k - n / 2 * 4)) =
    (f (o + k / 4))[↑k]
Tactic:
simp only [c, ↓reduceIte]
Proof state after:
case neg
f : ℕ → Color UInt8
chunk : ℕ
four : ↑4 = 0
n : ℕ
i : ∀ m < n, ∀ (o k : ℕ), k < m * 4 → (parallel_colors' f m o chunk).get! k = (f (o + k / 4))[↑k]
o k : ℕ
lt : k < n * 4
h : 1 < n ∧ chunk < n
c : ¬k < n / 2 * 4
⊢ (parallel_colors' f (n - n / 2) (o + n / 2) chunk).get! (k - n / 2 * 4) = (f (o + k / 4))[↑k]
Theorem: Image.get!_parallel_colors'
Proof state before:
case neg
f : ℕ → Color UInt8
chunk : ℕ
four : ↑4 = 0
n : ℕ
i : ∀ m < n, ∀ (o k : ℕ), k < m * 4 → (parallel_colors' f m o chunk).get! k = (f (o + k / 4))[↑k]
o k : ℕ
lt : k < n * 4
h : 1 < n ∧ chunk < n
c : ¬k < n / 2 * 4
⊢ (parallel_colors' f (n - n / 2) (o + n / 2) chunk).get! (k - n / 2 * 4) = (f (o + k / 4))[↑k]
Tactic:
rw [i]
Proof state after:
case neg
f : ℕ → Color UInt8
chunk : ℕ
four : ↑4 = 0
n : ℕ
i : ∀ m < n, ∀ (o k : ℕ), k < m * 4 → (parallel_colors' f m o chunk).get! k = (f (o + k / 4))[↑k]
o k : ℕ
lt : k < n * 4
h : 1 < n ∧ chunk < n
c : ¬k < n / 2 * 4
⊢ (f (o + n / 2 + (k - n / 2 * 4) / 4))[↑(k - n / 2 * 4)] = (f (o + k / 4))[↑k]

case neg.a
f : ℕ → Color UInt8
chunk : ℕ
four : ↑4 = 0
n : ℕ
i : ∀ m < n, ∀ (o k : ℕ), k < m * 4 → (parallel_colors' f m o chunk).get! k = (f (o + k / 4))[↑k]
o k : ℕ
lt : k < n * 4
h : 1 < n ∧ chunk < n
c : ¬k < n / 2 * 4
⊢ n - n / 2 < n

case neg.lt
f : ℕ → Color UInt8
chunk : ℕ
four : ↑4 = 0
n : ℕ
i : ∀ m < n, ∀ (o k : ℕ), k < m * 4 → (parallel_colors' f m o chunk).get! k = (f (o + k / 4))[↑k]
o k : ℕ
lt : k < n * 4
h : 1 < n ∧ chunk < n
c : ¬k < n / 2 * 4
⊢ k - n / 2 * 4 < (n - n / 2) * 4
Theorem: Image.get!_parallel_colors'
Proof state before:
case neg
f : ℕ → Color UInt8
chunk : ℕ
four : ↑4 = 0
n : ℕ
i : ∀ m < n, ∀ (o k : ℕ), k < m * 4 → (parallel_colors' f m o chunk).get! k = (f (o + k / 4))[↑k]
o k : ℕ
lt : k < n * 4
h : 1 < n ∧ chunk < n
c : ¬k < n / 2 * 4
⊢ (f (o + n / 2 + (k - n / 2 * 4) / 4))[↑(k - n / 2 * 4)] = (f (o + k / 4))[↑k]
Tactic:
have ke : o + n / 2 + (k - n / 2 * 4) / 4 = o + k / 4 := by omega
Proof state after:
case neg
f : ℕ → Color UInt8
chunk : ℕ
four : ↑4 = 0
n : ℕ
i : ∀ m < n, ∀ (o k : ℕ), k < m * 4 → (parallel_colors' f m o chunk).get! k = (f (o + k / 4))[↑k]
o k : ℕ
lt : k < n * 4
h : 1 < n ∧ chunk < n
c : ¬k < n / 2 * 4
ke : o + n / 2 + (k - n / 2 * 4) / 4 = o + k / 4
⊢ (f (o + n / 2 + (k - n / 2 * 4) / 4))[↑(k - n / 2 * 4)] = (f (o + k / 4))[↑k]
Theorem: Image.get!_parallel_colors'
Proof state before:
case neg
f : ℕ → Color UInt8
chunk : ℕ
four : ↑4 = 0
n : ℕ
i : ∀ m < n, ∀ (o k : ℕ), k < m * 4 → (parallel_colors' f m o chunk).get! k = (f (o + k / 4))[↑k]
o k : ℕ
lt : k < n * 4
h : 1 < n ∧ chunk < n
c : ¬k < n / 2 * 4
ke : o + n / 2 + (k - n / 2 * 4) / 4 = o + k / 4
⊢ (f (o + n / 2 + (k - n / 2 * 4) / 4))[↑(k - n / 2 * 4)] = (f (o + k / 4))[↑k]
Tactic:
rw [Nat.cast_sub (by omega), Nat.cast_mul, four, mul_zero, sub_zero, ke]
Proof state after:
no goals
Theorem: Image.get!_parallel_colors'
Proof state before:
f : ℕ → Color UInt8
chunk : ℕ
four : ↑4 = 0
n : ℕ
i : ∀ m < n, ∀ (o k : ℕ), k < m * 4 → (parallel_colors' f m o chunk).get! k = (f (o + k / 4))[↑k]
o k : ℕ
lt : k < n * 4
h : 1 < n ∧ chunk < n
c : ¬k < n / 2 * 4
⊢ o + n / 2 + (k - n / 2 * 4) / 4 = o + k / 4
Tactic:
omega
Proof state after:
no goals
Theorem: Image.get!_parallel_colors'
Proof state before:
f : ℕ → Color UInt8
chunk : ℕ
four : ↑4 = 0
n : ℕ
i : ∀ m < n, ∀ (o k : ℕ), k < m * 4 → (parallel_colors' f m o chunk).get! k = (f (o + k / 4))[↑k]
o k : ℕ
lt : k < n * 4
h : 1 < n ∧ chunk < n
c : ¬k < n / 2 * 4
ke : o + n / 2 + (k - n / 2 * 4) / 4 = o + k / 4
⊢ n / 2 * 4 ≤ k
Tactic:
omega
Proof state after:
no goals
Theorem: Image.get!_parallel_colors'
Proof state before:
case neg.a
f : ℕ → Color UInt8
chunk : ℕ
four : ↑4 = 0
n : ℕ
i : ∀ m < n, ∀ (o k : ℕ), k < m * 4 → (parallel_colors' f m o chunk).get! k = (f (o + k / 4))[↑k]
o k : ℕ
lt : k < n * 4
h : 1 < n ∧ chunk < n
c : ¬k < n / 2 * 4
⊢ n - n / 2 < n
Tactic:
omega
Proof state after:
no goals
Theorem: Image.get!_parallel_colors'
Proof state before:
case neg.lt
f : ℕ → Color UInt8
chunk : ℕ
four : ↑4 = 0
n : ℕ
i : ∀ m < n, ∀ (o k : ℕ), k < m * 4 → (parallel_colors' f m o chunk).get! k = (f (o + k / 4))[↑k]
o k : ℕ
lt : k < n * 4
h : 1 < n ∧ chunk < n
c : ¬k < n / 2 * 4
⊢ k - n / 2 * 4 < (n - n / 2) * 4
Tactic:
omega
Proof state after:
no goals
Theorem: Image.size_parallel_colors
Proof state before:
f : ℕ → Color UInt8
n chunk : ℕ
⊢ (parallel_colors f n chunk).size = n * 4
Tactic:
simp only [parallel_colors, size_parallel_colors']
Proof state after:
no goals
Theorem: Image.get!_parallel_colors
Proof state before:
f : ℕ → Color UInt8
n chunk k : ℕ
lt : k < n * 4
⊢ (parallel_colors f n chunk).get! k = (f (k / 4))[↑k]
Tactic:
simp only [parallel_colors, zero_add, get!_parallel_colors' f n 0 chunk k lt]
Proof state after:
no goals
Theorem: Image.width_ofFn
Proof state before:
f : ℕ → ℕ → Color UInt8
w h chunk : ℕ
⊢ (ofFn w h chunk f).width = w
Tactic:
rw [ofFn]
Proof state after:
no goals
Theorem: Image.height_ofFn
Proof state before:
f : ℕ → ℕ → Color UInt8
w h chunk : ℕ
⊢ (ofFn w h chunk f).height = h
Tactic:
rw [ofFn]
Proof state after:
no goals
Theorem: Image.get_ofFn
Proof state before:
f : ℕ → ℕ → Color UInt8
w h chunk : ℕ
x : Fin (ofFn w h chunk f).width
y : Fin (ofFn w h chunk f).height
⊢ (ofFn w h chunk f).get x y = f ↑x ↑y
Tactic:
rw [get]
Proof state after:
f : ℕ → ℕ → Color UInt8
w h chunk : ℕ
x : Fin (ofFn w h chunk f).width
y : Fin (ofFn w h chunk f).height
⊢ (let b := base (ofFn w h chunk f).width (ofFn w h chunk f).height ↑x ↑y;
    let_fun lt := ⋯;
    { r := (ofFn w h chunk f).data[b], g := (ofFn w h chunk f).data[b + 1], b := (ofFn w h chunk f).data[b + 2],
      a := (ofFn w h chunk f).data[b + 3] }) =
    f ↑x ↑y