Theorem: Image.size_parallel_colors' (Ray/Render/Image.lean)

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
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

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']
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

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
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

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]
State after:
no goals

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)]
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

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
State after:
no goals