Theorem: UInt8.val_unquantize (Ray/Render/Color.lean)

State before:
α β : Type
v : UInt8
n : v.unquantize ≠ nan
⊢ v.unquantize.val = ↑v.toNat / 256 + 1 / 512
Tactic:
rw [unquantize] at n ⊢
State after:
α β : Type
v : UInt8
n : (Floating.ofNat (2 * v.toNat + 1) false).scaleB (-9) ≠ nan
⊢ ((Floating.ofNat (2 * v.toNat + 1) false).scaleB (-9)).val = ↑v.toNat / 256 + 1 / 512

State before:
α β : Type
v : UInt8
n : (Floating.ofNat (2 * v.toNat + 1) false).scaleB (-9) ≠ nan
⊢ ((Floating.ofNat (2 * v.toNat + 1) false).scaleB (-9)).val = ↑v.toNat / 256 + 1 / 512
Tactic:
have lt : 2 * v.toNat + 1 < 2^63 := by have h := v.toNat_lt; norm_num only at h ⊢; omega
State after:
α β : Type
v : UInt8
n : (Floating.ofNat (2 * v.toNat + 1) false).scaleB (-9) ≠ nan
lt : 2 * v.toNat + 1 < 2 ^ 63
⊢ ((Floating.ofNat (2 * v.toNat + 1) false).scaleB (-9)).val = ↑v.toNat / 256 + 1 / 512

State before:
α β : Type
v : UInt8
n : (Floating.ofNat (2 * v.toNat + 1) false).scaleB (-9) ≠ nan
lt : 2 * v.toNat + 1 < 2 ^ 63
⊢ ((Floating.ofNat (2 * v.toNat + 1) false).scaleB (-9)).val = ↑v.toNat / 256 + 1 / 512
Tactic:
have e9 : ((-9 : Int64) : ℤ) = -9 := by decide
State after:
α β : Type
v : UInt8
n : (Floating.ofNat (2 * v.toNat + 1) false).scaleB (-9) ≠ nan
lt : 2 * v.toNat + 1 < 2 ^ 63
e9 : ↑(-9) = -9
⊢ ((Floating.ofNat (2 * v.toNat + 1) false).scaleB (-9)).val = ↑v.toNat / 256 + 1 / 512

State before:
α β : Type
v : UInt8
n : (Floating.ofNat (2 * v.toNat + 1) false).scaleB (-9) ≠ nan
lt : 2 * v.toNat + 1 < 2 ^ 63
e9 : ↑(-9) = -9
⊢ ((Floating.ofNat (2 * v.toNat + 1) false).scaleB (-9)).val = ↑v.toNat / 256 + 1 / 512
Tactic:
simp only [Floating.val_scaleB n, Floating.val_ofNat' lt, e9, Nat.cast_add, Nat.cast_mul,
  Nat.cast_ofNat, Nat.cast_one, Int.reduceNeg, zpow_neg, add_mul, one_mul, one_div]
State after:
α β : Type
v : UInt8
n : (Floating.ofNat (2 * v.toNat + 1) false).scaleB (-9) ≠ nan
lt : 2 * v.toNat + 1 < 2 ^ 63
e9 : ↑(-9) = -9
⊢ 2 * ↑v.toNat * (2 ^ 9)⁻¹ + (2 ^ 9)⁻¹ = ↑v.toNat / 256 + 512⁻¹

State before:
α β : Type
v : UInt8
n : (Floating.ofNat (2 * v.toNat + 1) false).scaleB (-9) ≠ nan
lt : 2 * v.toNat + 1 < 2 ^ 63
e9 : ↑(-9) = -9
⊢ 2 * ↑v.toNat * (2 ^ 9)⁻¹ + (2 ^ 9)⁻¹ = ↑v.toNat / 256 + 512⁻¹
Tactic:
ring_nf
State after:
no goals

State before:
α β : Type
v : UInt8
n : (Floating.ofNat (2 * v.toNat + 1) false).scaleB (-9) ≠ nan
⊢ 2 * v.toNat + 1 < 2 ^ 63
Tactic:
have h := v.toNat_lt
State after:
α β : Type
v : UInt8
n : (Floating.ofNat (2 * v.toNat + 1) false).scaleB (-9) ≠ nan
h : v.toNat < 2 ^ 8
⊢ 2 * v.toNat + 1 < 2 ^ 63

State before:
α β : Type
v : UInt8
n : (Floating.ofNat (2 * v.toNat + 1) false).scaleB (-9) ≠ nan
h : v.toNat < 2 ^ 8
⊢ 2 * v.toNat + 1 < 2 ^ 63
Tactic:
norm_num only at h ⊢
State after:
α β : Type
v : UInt8
n : (Floating.ofNat (2 * v.toNat + 1) false).scaleB (-9) ≠ nan
h : v.toNat < 256
⊢ 2 * v.toNat + 1 < 9223372036854775808

State before:
α β : Type
v : UInt8
n : (Floating.ofNat (2 * v.toNat + 1) false).scaleB (-9) ≠ nan
h : v.toNat < 256
⊢ 2 * v.toNat + 1 < 9223372036854775808
Tactic:
omega
State after:
no goals

State before:
α β : Type
v : UInt8
n : (Floating.ofNat (2 * v.toNat + 1) false).scaleB (-9) ≠ nan
lt : 2 * v.toNat + 1 < 2 ^ 63
⊢ ↑(-9) = -9
Tactic:
decide
State after:
no goals