Theorem: Image.size_push_colors (Ray/Render/Image.lean)

State before:
f : ℕ → Color UInt8
n o : ℕ
d : ByteArray
⊢ (push_colors f n o d).size = d.size + n * 4
Tactic:
induction' n with n h generalizing d o
State after:
case zero
f : ℕ → Color UInt8
o : ℕ
d : ByteArray
⊢ (push_colors f 0 o d).size = d.size + 0 * 4

case succ
f : ℕ → Color UInt8
n : ℕ
h : ∀ (o : ℕ) (d : ByteArray), (push_colors f n o d).size = d.size + n * 4
o : ℕ
d : ByteArray
⊢ (push_colors f (n + 1) o d).size = d.size + (n + 1) * 4

State before:
case zero
f : ℕ → Color UInt8
o : ℕ
d : ByteArray
⊢ (push_colors f 0 o d).size = d.size + 0 * 4
Tactic:
simp only [Nat.zero_eq, push_colors, ↓reduceIte, zero_mul, add_zero]
State after:
no goals

State before:
case succ
f : ℕ → Color UInt8
n : ℕ
h : ∀ (o : ℕ) (d : ByteArray), (push_colors f n o d).size = d.size + n * 4
o : ℕ
d : ByteArray
⊢ (push_colors f (n + 1) o d).size = d.size + (n + 1) * 4
Tactic:
rw [push_colors]
State after:
case succ
f : ℕ → Color UInt8
n : ℕ
h : ∀ (o : ℕ) (d : ByteArray), (push_colors f n o d).size = d.size + n * 4
o : ℕ
d : ByteArray
⊢ (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)).size =
    d.size + (n + 1) * 4

State before:
case succ
f : ℕ → Color UInt8
n : ℕ
h : ∀ (o : ℕ) (d : ByteArray), (push_colors f n o d).size = d.size + n * 4
o : ℕ
d : ByteArray
⊢ (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)).size =
    d.size + (n + 1) * 4
Tactic:
simp only [Nat.succ_eq_add_one, add_eq_zero, one_ne_zero, and_false, ↓reduceIte,
  add_tsub_cancel_right, h, ByteArray.size_push]
State after:
case succ
f : ℕ → Color UInt8
n : ℕ
h : ∀ (o : ℕ) (d : ByteArray), (push_colors f n o d).size = d.size + n * 4
o : ℕ
d : ByteArray
⊢ d.size + 1 + 1 + 1 + 1 + n * 4 = d.size + (n + 1) * 4

State before:
case succ
f : ℕ → Color UInt8
n : ℕ
h : ∀ (o : ℕ) (d : ByteArray), (push_colors f n o d).size = d.size + n * 4
o : ℕ
d : ByteArray
⊢ d.size + 1 + 1 + 1 + 1 + n * 4 = d.size + (n + 1) * 4
Tactic:
omega
State after:
no goals