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

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

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

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

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