Theorem: Interval.mem_approx_quantize (Ray/Render/Color.lean)

State before:
α β : Type
x' : ℝ
x : Interval
xm : x' ∈ approx x
⊢ x' ∈ approx x.quantize
Tactic:
rw [quantize]
State after:
α β : Type
x' : ℝ
x : Interval
xm : x' ∈ approx x
⊢ x' ∈
    approx
      (let c := x.untrusted_quantize;
      let m := c.unquantize;
      let lo := m.sub half_color_error.lo true;
      let hi := m.add half_color_error.lo false;
      if lo ≠ nan ∧ hi ≠ nan ∧ lo ≤ x.lo ∧ x.hi ≤ hi then some c else none)

State before:
α β : Type
x' : ℝ
x : Interval
xm : x' ∈ approx x
⊢ x' ∈
    approx
      (let c := x.untrusted_quantize;
      let m := c.unquantize;
      let lo := m.sub half_color_error.lo true;
      let hi := m.add half_color_error.lo false;
      if lo ≠ nan ∧ hi ≠ nan ∧ lo ≤ x.lo ∧ x.hi ≤ hi then some c else none)
Tactic:
generalize hc : x.untrusted_quantize = c
State after:
α β : Type
x' : ℝ
x : Interval
xm : x' ∈ approx x
c : UInt8
hc : x.untrusted_quantize = c
⊢ x' ∈
    approx
      (let c := c;
      let m := c.unquantize;
      let lo := m.sub half_color_error.lo true;
      let hi := m.add half_color_error.lo false;
      if lo ≠ nan ∧ hi ≠ nan ∧ lo ≤ x.lo ∧ x.hi ≤ hi then some c else none)

State before:
α β : Type
x' : ℝ
x : Interval
xm : x' ∈ approx x
c : UInt8
hc : x.untrusted_quantize = c
⊢ x' ∈
    approx
      (let c := c;
      let m := c.unquantize;
      let lo := m.sub half_color_error.lo true;
      let hi := m.add half_color_error.lo false;
      if lo ≠ nan ∧ hi ≠ nan ∧ lo ≤ x.lo ∧ x.hi ≤ hi then some c else none)
Tactic:
generalize hl : c.unquantize.sub half_color_error.lo true = lo
State after:
α β : Type
x' : ℝ
x : Interval
xm : x' ∈ approx x
c : UInt8
hc : x.untrusted_quantize = c
lo : Floating
hl : c.unquantize.sub half_color_error.lo true = lo
⊢ x' ∈
    approx
      (let c := c;
      let m := c.unquantize;
      let lo := m.sub half_color_error.lo true;
      let hi := m.add half_color_error.lo false;
      if lo ≠ nan ∧ hi ≠ nan ∧ lo ≤ x.lo ∧ x.hi ≤ hi then some c else none)

State before:
α β : Type
x' : ℝ
x : Interval
xm : x' ∈ approx x
c : UInt8
hc : x.untrusted_quantize = c
lo : Floating
hl : c.unquantize.sub half_color_error.lo true = lo
⊢ x' ∈
    approx
      (let c := c;
      let m := c.unquantize;
      let lo := m.sub half_color_error.lo true;
      let hi := m.add half_color_error.lo false;
      if lo ≠ nan ∧ hi ≠ nan ∧ lo ≤ x.lo ∧ x.hi ≤ hi then some c else none)
Tactic:
generalize hh : c.unquantize.add half_color_error.lo false = hi
State after:
α β : Type
x' : ℝ
x : Interval
xm : x' ∈ approx x
c : UInt8
hc : x.untrusted_quantize = c
lo : Floating
hl : c.unquantize.sub half_color_error.lo true = lo
hi : Floating
hh : c.unquantize.add half_color_error.lo false = hi
⊢ x' ∈
    approx
      (let c := c;
      let m := c.unquantize;
      let lo := m.sub half_color_error.lo true;
      let hi := m.add half_color_error.lo false;
      if lo ≠ nan ∧ hi ≠ nan ∧ lo ≤ x.lo ∧ x.hi ≤ hi then some c else none)

State before:
α β : Type
x' : ℝ
x : Interval
xm : x' ∈ approx x
c : UInt8
hc : x.untrusted_quantize = c
lo : Floating
hl : c.unquantize.sub half_color_error.lo true = lo
hi : Floating
hh : c.unquantize.add half_color_error.lo false = hi
⊢ x' ∈
    approx
      (let c := c;
      let m := c.unquantize;
      let lo := m.sub half_color_error.lo true;
      let hi := m.add half_color_error.lo false;
      if lo ≠ nan ∧ hi ≠ nan ∧ lo ≤ x.lo ∧ x.hi ≤ hi then some c else none)
Tactic:
simp only [hl, hh, ne_eq, Floating.val_le_val]
State after:
α β : Type
x' : ℝ
x : Interval
xm : x' ∈ approx x
c : UInt8
hc : x.untrusted_quantize = c
lo : Floating
hl : c.unquantize.sub half_color_error.lo true = lo
hi : Floating
hh : c.unquantize.add half_color_error.lo false = hi
⊢ x' ∈ approx (if ¬lo = nan ∧ ¬hi = nan ∧ lo.val ≤ x.lo.val ∧ x.hi.val ≤ hi.val then some c else none)

State before:
α β : Type
x' : ℝ
x : Interval
xm : x' ∈ approx x
c : UInt8
hc : x.untrusted_quantize = c
lo : Floating
hl : c.unquantize.sub half_color_error.lo true = lo
hi : Floating
hh : c.unquantize.add half_color_error.lo false = hi
⊢ x' ∈ approx (if ¬lo = nan ∧ ¬hi = nan ∧ lo.val ≤ x.lo.val ∧ x.hi.val ≤ hi.val then some c else none)
Tactic:
by_cases n : lo = nan ∨ hi = nan
State after:
case pos
α β : Type
x' : ℝ
x : Interval
xm : x' ∈ approx x
c : UInt8
hc : x.untrusted_quantize = c
lo : Floating
hl : c.unquantize.sub half_color_error.lo true = lo
hi : Floating
hh : c.unquantize.add half_color_error.lo false = hi
n : lo = nan ∨ hi = nan
⊢ x' ∈ approx (if ¬lo = nan ∧ ¬hi = nan ∧ lo.val ≤ x.lo.val ∧ x.hi.val ≤ hi.val then some c else none)

case neg
α β : Type
x' : ℝ
x : Interval
xm : x' ∈ approx x
c : UInt8
hc : x.untrusted_quantize = c
lo : Floating
hl : c.unquantize.sub half_color_error.lo true = lo
hi : Floating
hh : c.unquantize.add half_color_error.lo false = hi
n : ¬(lo = nan ∨ hi = nan)
⊢ x' ∈ approx (if ¬lo = nan ∧ ¬hi = nan ∧ lo.val ≤ x.lo.val ∧ x.hi.val ≤ hi.val then some c else none)

State before:
case neg
α β : Type
x' : ℝ
x : Interval
xm : x' ∈ approx x
c : UInt8
hc : x.untrusted_quantize = c
lo : Floating
hl : c.unquantize.sub half_color_error.lo true = lo
hi : Floating
hh : c.unquantize.add half_color_error.lo false = hi
n : ¬(lo = nan ∨ hi = nan)
⊢ x' ∈ approx (if ¬lo = nan ∧ ¬hi = nan ∧ lo.val ≤ x.lo.val ∧ x.hi.val ≤ hi.val then some c else none)
Tactic:
rcases not_or.mp n with ⟨n0,n1⟩
State after:
case neg.intro
α β : Type
x' : ℝ
x : Interval
xm : x' ∈ approx x
c : UInt8
hc : x.untrusted_quantize = c
lo : Floating
hl : c.unquantize.sub half_color_error.lo true = lo
hi : Floating
hh : c.unquantize.add half_color_error.lo false = hi
n : ¬(lo = nan ∨ hi = nan)
n0 : ¬lo = nan
n1 : ¬hi = nan
⊢ x' ∈ approx (if ¬lo = nan ∧ ¬hi = nan ∧ lo.val ≤ x.lo.val ∧ x.hi.val ≤ hi.val then some c else none)

State before:
case neg.intro
α β : Type
x' : ℝ
x : Interval
xm : x' ∈ approx x
c : UInt8
hc : x.untrusted_quantize = c
lo : Floating
hl : c.unquantize.sub half_color_error.lo true = lo
hi : Floating
hh : c.unquantize.add half_color_error.lo false = hi
n : ¬(lo = nan ∨ hi = nan)
n0 : ¬lo = nan
n1 : ¬hi = nan
⊢ x' ∈ approx (if ¬lo = nan ∧ ¬hi = nan ∧ lo.val ≤ x.lo.val ∧ x.hi.val ≤ hi.val then some c else none)
Tactic:
simp only [n0, not_false_eq_true, n1, true_and]
State after:
case neg.intro
α β : Type
x' : ℝ
x : Interval
xm : x' ∈ approx x
c : UInt8
hc : x.untrusted_quantize = c
lo : Floating
hl : c.unquantize.sub half_color_error.lo true = lo
hi : Floating
hh : c.unquantize.add half_color_error.lo false = hi
n : ¬(lo = nan ∨ hi = nan)
n0 : ¬lo = nan
n1 : ¬hi = nan
⊢ x' ∈ approx (if lo.val ≤ x.lo.val ∧ x.hi.val ≤ hi.val then some c else none)

State before:
case neg.intro
α β : Type
x' : ℝ
x : Interval
xm : x' ∈ approx x
c : UInt8
hc : x.untrusted_quantize = c
lo : Floating
hl : c.unquantize.sub half_color_error.lo true = lo
hi : Floating
hh : c.unquantize.add half_color_error.lo false = hi
n : ¬(lo = nan ∨ hi = nan)
n0 : ¬lo = nan
n1 : ¬hi = nan
⊢ x' ∈ approx (if lo.val ≤ x.lo.val ∧ x.hi.val ≤ hi.val then some c else none)
Tactic:
have mn : c.unquantize ≠ nan := by rw [←hl] at n0; exact (Floating.ne_nan_of_sub n0).1
State after:
case neg.intro
α β : Type
x' : ℝ
x : Interval
xm : x' ∈ approx x
c : UInt8
hc : x.untrusted_quantize = c
lo : Floating
hl : c.unquantize.sub half_color_error.lo true = lo
hi : Floating
hh : c.unquantize.add half_color_error.lo false = hi
n : ¬(lo = nan ∨ hi = nan)
n0 : ¬lo = nan
n1 : ¬hi = nan
mn : c.unquantize ≠ nan
⊢ x' ∈ approx (if lo.val ≤ x.lo.val ∧ x.hi.val ≤ hi.val then some c else none)

State before:
case neg.intro
α β : Type
x' : ℝ
x : Interval
xm : x' ∈ approx x
c : UInt8
hc : x.untrusted_quantize = c
lo : Floating
hl : c.unquantize.sub half_color_error.lo true = lo
hi : Floating
hh : c.unquantize.add half_color_error.lo false = hi
n : ¬(lo = nan ∨ hi = nan)
n0 : ¬lo = nan
n1 : ¬hi = nan
mn : c.unquantize ≠ nan
⊢ x' ∈ approx (if lo.val ≤ x.lo.val ∧ x.hi.val ≤ hi.val then some c else none)
Tactic:
by_cases g : lo.val ≤ x.lo.val ∧ x.hi.val ≤ hi.val
State after:
case pos
α β : Type
x' : ℝ
x : Interval
xm : x' ∈ approx x
c : UInt8
hc : x.untrusted_quantize = c
lo : Floating
hl : c.unquantize.sub half_color_error.lo true = lo
hi : Floating
hh : c.unquantize.add half_color_error.lo false = hi
n : ¬(lo = nan ∨ hi = nan)
n0 : ¬lo = nan
n1 : ¬hi = nan
mn : c.unquantize ≠ nan
g : lo.val ≤ x.lo.val ∧ x.hi.val ≤ hi.val
⊢ x' ∈ approx (if lo.val ≤ x.lo.val ∧ x.hi.val ≤ hi.val then some c else none)

case neg
α β : Type
x' : ℝ
x : Interval
xm : x' ∈ approx x
c : UInt8
hc : x.untrusted_quantize = c
lo : Floating
hl : c.unquantize.sub half_color_error.lo true = lo
hi : Floating
hh : c.unquantize.add half_color_error.lo false = hi
n : ¬(lo = nan ∨ hi = nan)
n0 : ¬lo = nan
n1 : ¬hi = nan
mn : c.unquantize ≠ nan
g : ¬(lo.val ≤ x.lo.val ∧ x.hi.val ≤ hi.val)
⊢ x' ∈ approx (if lo.val ≤ x.lo.val ∧ x.hi.val ≤ hi.val then some c else none)

State before:
case pos
α β : Type
x' : ℝ
x : Interval
xm : x' ∈ approx x
c : UInt8
hc : x.untrusted_quantize = c
lo : Floating
hl : c.unquantize.sub half_color_error.lo true = lo
hi : Floating
hh : c.unquantize.add half_color_error.lo false = hi
n : lo = nan ∨ hi = nan
⊢ x' ∈ approx (if ¬lo = nan ∧ ¬hi = nan ∧ lo.val ≤ x.lo.val ∧ x.hi.val ≤ hi.val then some c else none)
Tactic:
rcases n with n | n
State after:
case pos.inl
α β : Type
x' : ℝ
x : Interval
xm : x' ∈ approx x
c : UInt8
hc : x.untrusted_quantize = c
lo : Floating
hl : c.unquantize.sub half_color_error.lo true = lo
hi : Floating
hh : c.unquantize.add half_color_error.lo false = hi
n : lo = nan
⊢ x' ∈ approx (if ¬lo = nan ∧ ¬hi = nan ∧ lo.val ≤ x.lo.val ∧ x.hi.val ≤ hi.val then some c else none)

case pos.inr
α β : Type
x' : ℝ
x : Interval
xm : x' ∈ approx x
c : UInt8
hc : x.untrusted_quantize = c
lo : Floating
hl : c.unquantize.sub half_color_error.lo true = lo
hi : Floating
hh : c.unquantize.add half_color_error.lo false = hi
n : hi = nan
⊢ x' ∈ approx (if ¬lo = nan ∧ ¬hi = nan ∧ lo.val ≤ x.lo.val ∧ x.hi.val ≤ hi.val then some c else none)

State before:
case pos.inl
α β : Type
x' : ℝ
x : Interval
xm : x' ∈ approx x
c : UInt8
hc : x.untrusted_quantize = c
lo : Floating
hl : c.unquantize.sub half_color_error.lo true = lo
hi : Floating
hh : c.unquantize.add half_color_error.lo false = hi
n : lo = nan
⊢ x' ∈ approx (if ¬lo = nan ∧ ¬hi = nan ∧ lo.val ≤ x.lo.val ∧ x.hi.val ≤ hi.val then some c else none)

case pos.inr
α β : Type
x' : ℝ
x : Interval
xm : x' ∈ approx x
c : UInt8
hc : x.untrusted_quantize = c
lo : Floating
hl : c.unquantize.sub half_color_error.lo true = lo
hi : Floating
hh : c.unquantize.add half_color_error.lo false = hi
n : hi = nan
⊢ x' ∈ approx (if ¬lo = nan ∧ ¬hi = nan ∧ lo.val ≤ x.lo.val ∧ x.hi.val ≤ hi.val then some c else none)
Tactic:
all_goals simp [n]
State after:
no goals

State before:
case pos.inr
α β : Type
x' : ℝ
x : Interval
xm : x' ∈ approx x
c : UInt8
hc : x.untrusted_quantize = c
lo : Floating
hl : c.unquantize.sub half_color_error.lo true = lo
hi : Floating
hh : c.unquantize.add half_color_error.lo false = hi
n : hi = nan
⊢ x' ∈ approx (if ¬lo = nan ∧ ¬hi = nan ∧ lo.val ≤ x.lo.val ∧ x.hi.val ≤ hi.val then some c else none)
Tactic:
simp [n]
State after:
no goals

State before:
α β : Type
x' : ℝ
x : Interval
xm : x' ∈ approx x
c : UInt8
hc : x.untrusted_quantize = c
lo : Floating
hl : c.unquantize.sub half_color_error.lo true = lo
hi : Floating
hh : c.unquantize.add half_color_error.lo false = hi
n : ¬(lo = nan ∨ hi = nan)
n0 : ¬lo = nan
n1 : ¬hi = nan
⊢ c.unquantize ≠ nan
Tactic:
rw [←hl] at n0
State after:
α β : Type
x' : ℝ
x : Interval
xm : x' ∈ approx x
c : UInt8
hc : x.untrusted_quantize = c
lo : Floating
hl : c.unquantize.sub half_color_error.lo true = lo
hi : Floating
hh : c.unquantize.add half_color_error.lo false = hi
n : ¬(lo = nan ∨ hi = nan)
n0 : ¬c.unquantize.sub half_color_error.lo true = nan
n1 : ¬hi = nan
⊢ c.unquantize ≠ nan

State before:
α β : Type
x' : ℝ
x : Interval
xm : x' ∈ approx x
c : UInt8
hc : x.untrusted_quantize = c
lo : Floating
hl : c.unquantize.sub half_color_error.lo true = lo
hi : Floating
hh : c.unquantize.add half_color_error.lo false = hi
n : ¬(lo = nan ∨ hi = nan)
n0 : ¬c.unquantize.sub half_color_error.lo true = nan
n1 : ¬hi = nan
⊢ c.unquantize ≠ nan
Tactic:
exact (Floating.ne_nan_of_sub n0).1
State after:
no goals

State before:
case pos
α β : Type
x' : ℝ
x : Interval
xm : x' ∈ approx x
c : UInt8
hc : x.untrusted_quantize = c
lo : Floating
hl : c.unquantize.sub half_color_error.lo true = lo
hi : Floating
hh : c.unquantize.add half_color_error.lo false = hi
n : ¬(lo = nan ∨ hi = nan)
n0 : ¬lo = nan
n1 : ¬hi = nan
mn : c.unquantize ≠ nan
g : lo.val ≤ x.lo.val ∧ x.hi.val ≤ hi.val
⊢ x' ∈ approx (if lo.val ≤ x.lo.val ∧ x.hi.val ≤ hi.val then some c else none)
Tactic:
have xn : x ≠ nan := by
  contrapose g
  simp only [ne_eq, not_not] at g
  simp only [g, lo_nan, hi_nan, Floating.val_nan_le, and_true, not_le, ←Floating.val_lt_val]
  exact Floating.nan_lt n0
State after:
case pos
α β : Type
x' : ℝ
x : Interval
xm : x' ∈ approx x
c : UInt8
hc : x.untrusted_quantize = c
lo : Floating
hl : c.unquantize.sub half_color_error.lo true = lo
hi : Floating
hh : c.unquantize.add half_color_error.lo false = hi
n : ¬(lo = nan ∨ hi = nan)
n0 : ¬lo = nan
n1 : ¬hi = nan
mn : c.unquantize ≠ nan
g : lo.val ≤ x.lo.val ∧ x.hi.val ≤ hi.val
xn : x ≠ nan
⊢ x' ∈ approx (if lo.val ≤ x.lo.val ∧ x.hi.val ≤ hi.val then some c else none)

State before:
case pos
α β : Type
x' : ℝ
x : Interval
xm : x' ∈ approx x
c : UInt8
hc : x.untrusted_quantize = c
lo : Floating
hl : c.unquantize.sub half_color_error.lo true = lo
hi : Floating
hh : c.unquantize.add half_color_error.lo false = hi
n : ¬(lo = nan ∨ hi = nan)
n0 : ¬lo = nan
n1 : ¬hi = nan
mn : c.unquantize ≠ nan
g : lo.val ≤ x.lo.val ∧ x.hi.val ≤ hi.val
xn : x ≠ nan
⊢ x' ∈ approx (if lo.val ≤ x.lo.val ∧ x.hi.val ≤ hi.val then some c else none)
Tactic:
simp only [g, and_self, ↓reduceIte, approx_some, approx, Rat.cast_div, Rat.cast_ofNat, mem_Icc,
  tsub_le_iff_right, UInt8.color, add_div]
State after:
case pos
α β : Type
x' : ℝ
x : Interval
xm : x' ∈ approx x
c : UInt8
hc : x.untrusted_quantize = c
lo : Floating
hl : c.unquantize.sub half_color_error.lo true = lo
hi : Floating
hh : c.unquantize.add half_color_error.lo false = hi
n : ¬(lo = nan ∨ hi = nan)
n0 : ¬lo = nan
n1 : ¬hi = nan
mn : c.unquantize ≠ nan
g : lo.val ≤ x.lo.val ∧ x.hi.val ≤ hi.val
xn : x ≠ nan
⊢ ↑c.toNat / 256 + 1 / 2 / 256 ≤ x' + ↑color_error / 2 ∧ x' ≤ ↑c.toNat / 256 + 1 / 2 / 256 + ↑color_error / 2

State before:
case pos
α β : Type
x' : ℝ
x : Interval
xm : x' ∈ approx x
c : UInt8
hc : x.untrusted_quantize = c
lo : Floating
hl : c.unquantize.sub half_color_error.lo true = lo
hi : Floating
hh : c.unquantize.add half_color_error.lo false = hi
n : ¬(lo = nan ∨ hi = nan)
n0 : ¬lo = nan
n1 : ¬hi = nan
mn : c.unquantize ≠ nan
g : lo.val ≤ x.lo.val ∧ x.hi.val ≤ hi.val
xn : x ≠ nan
⊢ ↑c.toNat / 256 + 1 / 2 / 256 ≤ x' + ↑color_error / 2 ∧ x' ≤ ↑c.toNat / 256 + 1 / 2 / 256 + ↑color_error / 2
Tactic:
simp only [approx, lo_eq_nan, xn, ↓reduceIte, mem_Icc] at xm
State after:
case pos
α β : Type
x' : ℝ
x : Interval
c : UInt8
hc : x.untrusted_quantize = c
lo : Floating
hl : c.unquantize.sub half_color_error.lo true = lo
hi : Floating
hh : c.unquantize.add half_color_error.lo false = hi
n : ¬(lo = nan ∨ hi = nan)
n0 : ¬lo = nan
n1 : ¬hi = nan
mn : c.unquantize ≠ nan
g : lo.val ≤ x.lo.val ∧ x.hi.val ≤ hi.val
xn : x ≠ nan
xm : x.lo.val ≤ x' ∧ x' ≤ x.hi.val
⊢ ↑c.toNat / 256 + 1 / 2 / 256 ≤ x' + ↑color_error / 2 ∧ x' ≤ ↑c.toNat / 256 + 1 / 2 / 256 + ↑color_error / 2

State before:
case pos
α β : Type
x' : ℝ
x : Interval
c : UInt8
hc : x.untrusted_quantize = c
lo : Floating
hl : c.unquantize.sub half_color_error.lo true = lo
hi : Floating
hh : c.unquantize.add half_color_error.lo false = hi
n : ¬(lo = nan ∨ hi = nan)
n0 : ¬lo = nan
n1 : ¬hi = nan
mn : c.unquantize ≠ nan
g : lo.val ≤ x.lo.val ∧ x.hi.val ≤ hi.val
xn : x ≠ nan
xm : x.lo.val ≤ x' ∧ x' ≤ x.hi.val
⊢ ↑c.toNat / 256 + 1 / 2 / 256 ≤ x' + ↑color_error / 2 ∧ x' ≤ ↑c.toNat / 256 + 1 / 2 / 256 + ↑color_error / 2
Tactic:
have e : half_color_error.lo.val ≤ color_error / 2 := by
  rw [half_color_error]
  apply lo_le (by native_decide)
  have e : (color_error : ℝ) / 2 = (color_error / 2 : ℚ) := by
    simp only [Rat.cast_div, Rat.cast_ofNat]
  rw [e]; mono
State after:
case pos
α β : Type
x' : ℝ
x : Interval
c : UInt8
hc : x.untrusted_quantize = c
lo : Floating
hl : c.unquantize.sub half_color_error.lo true = lo
hi : Floating
hh : c.unquantize.add half_color_error.lo false = hi
n : ¬(lo = nan ∨ hi = nan)
n0 : ¬lo = nan
n1 : ¬hi = nan
mn : c.unquantize ≠ nan
g : lo.val ≤ x.lo.val ∧ x.hi.val ≤ hi.val
xn : x ≠ nan
xm : x.lo.val ≤ x' ∧ x' ≤ x.hi.val
e : half_color_error.lo.val ≤ ↑color_error / 2
⊢ ↑c.toNat / 256 + 1 / 2 / 256 ≤ x' + ↑color_error / 2 ∧ x' ≤ ↑c.toNat / 256 + 1 / 2 / 256 + ↑color_error / 2

State before:
case pos
α β : Type
x' : ℝ
x : Interval
c : UInt8
hc : x.untrusted_quantize = c
lo : Floating
hl : c.unquantize.sub half_color_error.lo true = lo
hi : Floating
hh : c.unquantize.add half_color_error.lo false = hi
n : ¬(lo = nan ∨ hi = nan)
n0 : ¬lo = nan
n1 : ¬hi = nan
mn : c.unquantize ≠ nan
g : lo.val ≤ x.lo.val ∧ x.hi.val ≤ hi.val
xn : x ≠ nan
xm : x.lo.val ≤ x' ∧ x' ≤ x.hi.val
e : half_color_error.lo.val ≤ ↑color_error / 2
⊢ ↑c.toNat / 256 + 1 / 2 / 256 ≤ x' + ↑color_error / 2 ∧ x' ≤ ↑c.toNat / 256 + 1 / 2 / 256 + ↑color_error / 2
Tactic:
simp only [←hl, ←hh] at n0 n1 mn g
State after:
case pos
α β : Type
x' : ℝ
x : Interval
c : UInt8
hc : x.untrusted_quantize = c
lo : Floating
hl : c.unquantize.sub half_color_error.lo true = lo
hi : Floating
hh : c.unquantize.add half_color_error.lo false = hi
n : ¬(lo = nan ∨ hi = nan)
mn : c.unquantize ≠ nan
xn : x ≠ nan
xm : x.lo.val ≤ x' ∧ x' ≤ x.hi.val
e : half_color_error.lo.val ≤ ↑color_error / 2
n0 : ¬c.unquantize.sub half_color_error.lo true = nan
n1 : ¬c.unquantize.add half_color_error.lo false = nan
g :
  (c.unquantize.sub half_color_error.lo true).val ≤ x.lo.val ∧
    x.hi.val ≤ (c.unquantize.add half_color_error.lo false).val
⊢ ↑c.toNat / 256 + 1 / 2 / 256 ≤ x' + ↑color_error / 2 ∧ x' ≤ ↑c.toNat / 256 + 1 / 2 / 256 + ↑color_error / 2

State before:
case pos
α β : Type
x' : ℝ
x : Interval
c : UInt8
hc : x.untrusted_quantize = c
lo : Floating
hl : c.unquantize.sub half_color_error.lo true = lo
hi : Floating
hh : c.unquantize.add half_color_error.lo false = hi
n : ¬(lo = nan ∨ hi = nan)
mn : c.unquantize ≠ nan
xn : x ≠ nan
xm : x.lo.val ≤ x' ∧ x' ≤ x.hi.val
e : half_color_error.lo.val ≤ ↑color_error / 2
n0 : ¬c.unquantize.sub half_color_error.lo true = nan
n1 : ¬c.unquantize.add half_color_error.lo false = nan
g :
  (c.unquantize.sub half_color_error.lo true).val ≤ x.lo.val ∧
    x.hi.val ≤ (c.unquantize.add half_color_error.lo false).val
⊢ ↑c.toNat / 256 + 1 / 2 / 256 ≤ x' + ↑color_error / 2 ∧ x' ≤ ↑c.toNat / 256 + 1 / 2 / 256 + ↑color_error / 2
Tactic:
have le_lo := Floating.le_sub n0
State after:
case pos
α β : Type
x' : ℝ
x : Interval
c : UInt8
hc : x.untrusted_quantize = c
lo : Floating
hl : c.unquantize.sub half_color_error.lo true = lo
hi : Floating
hh : c.unquantize.add half_color_error.lo false = hi
n : ¬(lo = nan ∨ hi = nan)
mn : c.unquantize ≠ nan
xn : x ≠ nan
xm : x.lo.val ≤ x' ∧ x' ≤ x.hi.val
e : half_color_error.lo.val ≤ ↑color_error / 2
n0 : ¬c.unquantize.sub half_color_error.lo true = nan
n1 : ¬c.unquantize.add half_color_error.lo false = nan
g :
  (c.unquantize.sub half_color_error.lo true).val ≤ x.lo.val ∧
    x.hi.val ≤ (c.unquantize.add half_color_error.lo false).val
le_lo : c.unquantize.val - half_color_error.lo.val ≤ (c.unquantize.sub half_color_error.lo true).val
⊢ ↑c.toNat / 256 + 1 / 2 / 256 ≤ x' + ↑color_error / 2 ∧ x' ≤ ↑c.toNat / 256 + 1 / 2 / 256 + ↑color_error / 2

State before:
case pos
α β : Type
x' : ℝ
x : Interval
c : UInt8
hc : x.untrusted_quantize = c
lo : Floating
hl : c.unquantize.sub half_color_error.lo true = lo
hi : Floating
hh : c.unquantize.add half_color_error.lo false = hi
n : ¬(lo = nan ∨ hi = nan)
mn : c.unquantize ≠ nan
xn : x ≠ nan
xm : x.lo.val ≤ x' ∧ x' ≤ x.hi.val
e : half_color_error.lo.val ≤ ↑color_error / 2
n0 : ¬c.unquantize.sub half_color_error.lo true = nan
n1 : ¬c.unquantize.add half_color_error.lo false = nan
g :
  (c.unquantize.sub half_color_error.lo true).val ≤ x.lo.val ∧
    x.hi.val ≤ (c.unquantize.add half_color_error.lo false).val
le_lo : c.unquantize.val - half_color_error.lo.val ≤ (c.unquantize.sub half_color_error.lo true).val
⊢ ↑c.toNat / 256 + 1 / 2 / 256 ≤ x' + ↑color_error / 2 ∧ x' ≤ ↑c.toNat / 256 + 1 / 2 / 256 + ↑color_error / 2
Tactic:
have le_hi := Floating.add_le n1
State after:
case pos
α β : Type
x' : ℝ
x : Interval
c : UInt8
hc : x.untrusted_quantize = c
lo : Floating
hl : c.unquantize.sub half_color_error.lo true = lo
hi : Floating
hh : c.unquantize.add half_color_error.lo false = hi
n : ¬(lo = nan ∨ hi = nan)
mn : c.unquantize ≠ nan
xn : x ≠ nan
xm : x.lo.val ≤ x' ∧ x' ≤ x.hi.val
e : half_color_error.lo.val ≤ ↑color_error / 2
n0 : ¬c.unquantize.sub half_color_error.lo true = nan
n1 : ¬c.unquantize.add half_color_error.lo false = nan
g :
  (c.unquantize.sub half_color_error.lo true).val ≤ x.lo.val ∧
    x.hi.val ≤ (c.unquantize.add half_color_error.lo false).val
le_lo : c.unquantize.val - half_color_error.lo.val ≤ (c.unquantize.sub half_color_error.lo true).val
le_hi : (c.unquantize.add half_color_error.lo false).val ≤ c.unquantize.val + half_color_error.lo.val
⊢ ↑c.toNat / 256 + 1 / 2 / 256 ≤ x' + ↑color_error / 2 ∧ x' ≤ ↑c.toNat / 256 + 1 / 2 / 256 + ↑color_error / 2

State before:
case pos
α β : Type
x' : ℝ
x : Interval
c : UInt8
hc : x.untrusted_quantize = c
lo : Floating
hl : c.unquantize.sub half_color_error.lo true = lo
hi : Floating
hh : c.unquantize.add half_color_error.lo false = hi
n : ¬(lo = nan ∨ hi = nan)
mn : c.unquantize ≠ nan
xn : x ≠ nan
xm : x.lo.val ≤ x' ∧ x' ≤ x.hi.val
e : half_color_error.lo.val ≤ ↑color_error / 2
n0 : ¬c.unquantize.sub half_color_error.lo true = nan
n1 : ¬c.unquantize.add half_color_error.lo false = nan
g :
  (c.unquantize.sub half_color_error.lo true).val ≤ x.lo.val ∧
    x.hi.val ≤ (c.unquantize.add half_color_error.lo false).val
le_lo : c.unquantize.val - half_color_error.lo.val ≤ (c.unquantize.sub half_color_error.lo true).val
le_hi : (c.unquantize.add half_color_error.lo false).val ≤ c.unquantize.val + half_color_error.lo.val
⊢ ↑c.toNat / 256 + 1 / 2 / 256 ≤ x' + ↑color_error / 2 ∧ x' ≤ ↑c.toNat / 256 + 1 / 2 / 256 + ↑color_error / 2
Tactic:
simp only [UInt8.val_unquantize mn, hl, tsub_le_iff_right, hh, hl, hh] at le_lo le_hi g ⊢
State after:
case pos
α β : Type
x' : ℝ
x : Interval
c : UInt8
hc : x.untrusted_quantize = c
lo : Floating
hl : c.unquantize.sub half_color_error.lo true = lo
hi : Floating
hh : c.unquantize.add half_color_error.lo false = hi
n : ¬(lo = nan ∨ hi = nan)
mn : c.unquantize ≠ nan
xn : x ≠ nan
xm : x.lo.val ≤ x' ∧ x' ≤ x.hi.val
e : half_color_error.lo.val ≤ ↑color_error / 2
n0 : ¬c.unquantize.sub half_color_error.lo true = nan
n1 : ¬c.unquantize.add half_color_error.lo false = nan
le_lo : ↑c.toNat / 256 + 1 / 512 ≤ lo.val + half_color_error.lo.val
le_hi : hi.val ≤ ↑c.toNat / 256 + 1 / 512 + half_color_error.lo.val
g : lo.val ≤ x.lo.val ∧ x.hi.val ≤ hi.val
⊢ ↑c.toNat / 256 + 1 / 2 / 256 ≤ x' + ↑color_error / 2 ∧ x' ≤ ↑c.toNat / 256 + 1 / 2 / 256 + ↑color_error / 2

State before:
case pos
α β : Type
x' : ℝ
x : Interval
c : UInt8
hc : x.untrusted_quantize = c
lo : Floating
hl : c.unquantize.sub half_color_error.lo true = lo
hi : Floating
hh : c.unquantize.add half_color_error.lo false = hi
n : ¬(lo = nan ∨ hi = nan)
mn : c.unquantize ≠ nan
xn : x ≠ nan
xm : x.lo.val ≤ x' ∧ x' ≤ x.hi.val
e : half_color_error.lo.val ≤ ↑color_error / 2
n0 : ¬c.unquantize.sub half_color_error.lo true = nan
n1 : ¬c.unquantize.add half_color_error.lo false = nan
le_lo : ↑c.toNat / 256 + 1 / 512 ≤ lo.val + half_color_error.lo.val
le_hi : hi.val ≤ ↑c.toNat / 256 + 1 / 512 + half_color_error.lo.val
g : lo.val ≤ x.lo.val ∧ x.hi.val ≤ hi.val
⊢ ↑c.toNat / 256 + 1 / 2 / 256 ≤ x' + ↑color_error / 2 ∧ x' ≤ ↑c.toNat / 256 + 1 / 2 / 256 + ↑color_error / 2
Tactic:
exact ⟨by linarith, by linarith⟩
State after:
no goals

State before:
α β : Type
x' : ℝ
x : Interval
xm : x' ∈ approx x
c : UInt8
hc : x.untrusted_quantize = c
lo : Floating
hl : c.unquantize.sub half_color_error.lo true = lo
hi : Floating
hh : c.unquantize.add half_color_error.lo false = hi
n : ¬(lo = nan ∨ hi = nan)
n0 : ¬lo = nan
n1 : ¬hi = nan
mn : c.unquantize ≠ nan
g : lo.val ≤ x.lo.val ∧ x.hi.val ≤ hi.val
⊢ x ≠ nan
Tactic:
contrapose g
State after:
α β : Type
x' : ℝ
x : Interval
xm : x' ∈ approx x
c : UInt8
hc : x.untrusted_quantize = c
lo : Floating
hl : c.unquantize.sub half_color_error.lo true = lo
hi : Floating
hh : c.unquantize.add half_color_error.lo false = hi
n : ¬(lo = nan ∨ hi = nan)
n0 : ¬lo = nan
n1 : ¬hi = nan
mn : c.unquantize ≠ nan
g : ¬x ≠ nan
⊢ ¬(lo.val ≤ x.lo.val ∧ x.hi.val ≤ hi.val)

State before:
α β : Type
x' : ℝ
x : Interval
xm : x' ∈ approx x
c : UInt8
hc : x.untrusted_quantize = c
lo : Floating
hl : c.unquantize.sub half_color_error.lo true = lo
hi : Floating
hh : c.unquantize.add half_color_error.lo false = hi
n : ¬(lo = nan ∨ hi = nan)
n0 : ¬lo = nan
n1 : ¬hi = nan
mn : c.unquantize ≠ nan
g : ¬x ≠ nan
⊢ ¬(lo.val ≤ x.lo.val ∧ x.hi.val ≤ hi.val)
Tactic:
simp only [ne_eq, not_not] at g
State after:
α β : Type
x' : ℝ
x : Interval
xm : x' ∈ approx x
c : UInt8
hc : x.untrusted_quantize = c
lo : Floating
hl : c.unquantize.sub half_color_error.lo true = lo
hi : Floating
hh : c.unquantize.add half_color_error.lo false = hi
n : ¬(lo = nan ∨ hi = nan)
n0 : ¬lo = nan
n1 : ¬hi = nan
mn : c.unquantize ≠ nan
g : x = nan
⊢ ¬(lo.val ≤ x.lo.val ∧ x.hi.val ≤ hi.val)

State before:
α β : Type
x' : ℝ
x : Interval
xm : x' ∈ approx x
c : UInt8
hc : x.untrusted_quantize = c
lo : Floating
hl : c.unquantize.sub half_color_error.lo true = lo
hi : Floating
hh : c.unquantize.add half_color_error.lo false = hi
n : ¬(lo = nan ∨ hi = nan)
n0 : ¬lo = nan
n1 : ¬hi = nan
mn : c.unquantize ≠ nan
g : x = nan
⊢ ¬(lo.val ≤ x.lo.val ∧ x.hi.val ≤ hi.val)
Tactic:
simp only [g, lo_nan, hi_nan, Floating.val_nan_le, and_true, not_le, ←Floating.val_lt_val]
State after:
α β : Type
x' : ℝ
x : Interval
xm : x' ∈ approx x
c : UInt8
hc : x.untrusted_quantize = c
lo : Floating
hl : c.unquantize.sub half_color_error.lo true = lo
hi : Floating
hh : c.unquantize.add half_color_error.lo false = hi
n : ¬(lo = nan ∨ hi = nan)
n0 : ¬lo = nan
n1 : ¬hi = nan
mn : c.unquantize ≠ nan
g : x = nan
⊢ nan < lo

State before:
α β : Type
x' : ℝ
x : Interval
xm : x' ∈ approx x
c : UInt8
hc : x.untrusted_quantize = c
lo : Floating
hl : c.unquantize.sub half_color_error.lo true = lo
hi : Floating
hh : c.unquantize.add half_color_error.lo false = hi
n : ¬(lo = nan ∨ hi = nan)
n0 : ¬lo = nan
n1 : ¬hi = nan
mn : c.unquantize ≠ nan
g : x = nan
⊢ nan < lo
Tactic:
exact Floating.nan_lt n0
State after:
no goals

State before:
α β : Type
x' : ℝ
x : Interval
c : UInt8
hc : x.untrusted_quantize = c
lo : Floating
hl : c.unquantize.sub half_color_error.lo true = lo
hi : Floating
hh : c.unquantize.add half_color_error.lo false = hi
n : ¬(lo = nan ∨ hi = nan)
n0 : ¬lo = nan
n1 : ¬hi = nan
mn : c.unquantize ≠ nan
g : lo.val ≤ x.lo.val ∧ x.hi.val ≤ hi.val
xn : x ≠ nan
xm : x.lo.val ≤ x' ∧ x' ≤ x.hi.val
⊢ half_color_error.lo.val ≤ ↑color_error / 2
Tactic:
rw [half_color_error]
State after:
α β : Type
x' : ℝ
x : Interval
c : UInt8
hc : x.untrusted_quantize = c
lo : Floating
hl : c.unquantize.sub half_color_error.lo true = lo
hi : Floating
hh : c.unquantize.add half_color_error.lo false = hi
n : ¬(lo = nan ∨ hi = nan)
n0 : ¬lo = nan
n1 : ¬hi = nan
mn : c.unquantize ≠ nan
g : lo.val ≤ x.lo.val ∧ x.hi.val ≤ hi.val
xn : x ≠ nan
xm : x.lo.val ≤ x' ∧ x' ≤ x.hi.val
⊢ (ofRat (color_error / 2)).lo.val ≤ ↑color_error / 2

State before:
α β : Type
x' : ℝ
x : Interval
c : UInt8
hc : x.untrusted_quantize = c
lo : Floating
hl : c.unquantize.sub half_color_error.lo true = lo
hi : Floating
hh : c.unquantize.add half_color_error.lo false = hi
n : ¬(lo = nan ∨ hi = nan)
n0 : ¬lo = nan
n1 : ¬hi = nan
mn : c.unquantize ≠ nan
g : lo.val ≤ x.lo.val ∧ x.hi.val ≤ hi.val
xn : x ≠ nan
xm : x.lo.val ≤ x' ∧ x' ≤ x.hi.val
⊢ (ofRat (color_error / 2)).lo.val ≤ ↑color_error / 2
Tactic:
apply lo_le (by native_decide)
State after:
α β : Type
x' : ℝ
x : Interval
c : UInt8
hc : x.untrusted_quantize = c
lo : Floating
hl : c.unquantize.sub half_color_error.lo true = lo
hi : Floating
hh : c.unquantize.add half_color_error.lo false = hi
n : ¬(lo = nan ∨ hi = nan)
n0 : ¬lo = nan
n1 : ¬hi = nan
mn : c.unquantize ≠ nan
g : lo.val ≤ x.lo.val ∧ x.hi.val ≤ hi.val
xn : x ≠ nan
xm : x.lo.val ≤ x' ∧ x' ≤ x.hi.val
⊢ ↑color_error / 2 ∈ approx (ofRat (color_error / 2))

State before:
α β : Type
x' : ℝ
x : Interval
c : UInt8
hc : x.untrusted_quantize = c
lo : Floating
hl : c.unquantize.sub half_color_error.lo true = lo
hi : Floating
hh : c.unquantize.add half_color_error.lo false = hi
n : ¬(lo = nan ∨ hi = nan)
n0 : ¬lo = nan
n1 : ¬hi = nan
mn : c.unquantize ≠ nan
g : lo.val ≤ x.lo.val ∧ x.hi.val ≤ hi.val
xn : x ≠ nan
xm : x.lo.val ≤ x' ∧ x' ≤ x.hi.val
⊢ ↑color_error / 2 ∈ approx (ofRat (color_error / 2))
Tactic:
have e : (color_error : ℝ) / 2 = (color_error / 2 : ℚ) := by
  simp only [Rat.cast_div, Rat.cast_ofNat]
State after:
α β : Type
x' : ℝ
x : Interval
c : UInt8
hc : x.untrusted_quantize = c
lo : Floating
hl : c.unquantize.sub half_color_error.lo true = lo
hi : Floating
hh : c.unquantize.add half_color_error.lo false = hi
n : ¬(lo = nan ∨ hi = nan)
n0 : ¬lo = nan
n1 : ¬hi = nan
mn : c.unquantize ≠ nan
g : lo.val ≤ x.lo.val ∧ x.hi.val ≤ hi.val
xn : x ≠ nan
xm : x.lo.val ≤ x' ∧ x' ≤ x.hi.val
e : ↑color_error / 2 = ↑(color_error / 2)
⊢ ↑color_error / 2 ∈ approx (ofRat (color_error / 2))

State before:
α β : Type
x' : ℝ
x : Interval
c : UInt8
hc : x.untrusted_quantize = c
lo : Floating
hl : c.unquantize.sub half_color_error.lo true = lo
hi : Floating
hh : c.unquantize.add half_color_error.lo false = hi
n : ¬(lo = nan ∨ hi = nan)
n0 : ¬lo = nan
n1 : ¬hi = nan
mn : c.unquantize ≠ nan
g : lo.val ≤ x.lo.val ∧ x.hi.val ≤ hi.val
xn : x ≠ nan
xm : x.lo.val ≤ x' ∧ x' ≤ x.hi.val
e : ↑color_error / 2 = ↑(color_error / 2)
⊢ ↑color_error / 2 ∈ approx (ofRat (color_error / 2))
Tactic:
rw [e]
State after:
α β : Type
x' : ℝ
x : Interval
c : UInt8
hc : x.untrusted_quantize = c
lo : Floating
hl : c.unquantize.sub half_color_error.lo true = lo
hi : Floating
hh : c.unquantize.add half_color_error.lo false = hi
n : ¬(lo = nan ∨ hi = nan)
n0 : ¬lo = nan
n1 : ¬hi = nan
mn : c.unquantize ≠ nan
g : lo.val ≤ x.lo.val ∧ x.hi.val ≤ hi.val
xn : x ≠ nan
xm : x.lo.val ≤ x' ∧ x' ≤ x.hi.val
e : ↑color_error / 2 = ↑(color_error / 2)
⊢ ↑(color_error / 2) ∈ approx (ofRat (color_error / 2))

State before:
α β : Type
x' : ℝ
x : Interval
c : UInt8
hc : x.untrusted_quantize = c
lo : Floating
hl : c.unquantize.sub half_color_error.lo true = lo
hi : Floating
hh : c.unquantize.add half_color_error.lo false = hi
n : ¬(lo = nan ∨ hi = nan)
n0 : ¬lo = nan
n1 : ¬hi = nan
mn : c.unquantize ≠ nan
g : lo.val ≤ x.lo.val ∧ x.hi.val ≤ hi.val
xn : x ≠ nan
xm : x.lo.val ≤ x' ∧ x' ≤ x.hi.val
e : ↑color_error / 2 = ↑(color_error / 2)
⊢ ↑(color_error / 2) ∈ approx (ofRat (color_error / 2))
Tactic:
mono
State after:
no goals

State before:
α β : Type
x' : ℝ
x : Interval
c : UInt8
hc : x.untrusted_quantize = c
lo : Floating
hl : c.unquantize.sub half_color_error.lo true = lo
hi : Floating
hh : c.unquantize.add half_color_error.lo false = hi
n : ¬(lo = nan ∨ hi = nan)
n0 : ¬lo = nan
n1 : ¬hi = nan
mn : c.unquantize ≠ nan
g : lo.val ≤ x.lo.val ∧ x.hi.val ≤ hi.val
xn : x ≠ nan
xm : x.lo.val ≤ x' ∧ x' ≤ x.hi.val
⊢ ofRat (color_error / 2) ≠ nan
Tactic:
native_decide
State after:
no goals

State before:
α β : Type
x' : ℝ
x : Interval
c : UInt8
hc : x.untrusted_quantize = c
lo : Floating
hl : c.unquantize.sub half_color_error.lo true = lo
hi : Floating
hh : c.unquantize.add half_color_error.lo false = hi
n : ¬(lo = nan ∨ hi = nan)
n0 : ¬lo = nan
n1 : ¬hi = nan
mn : c.unquantize ≠ nan
g : lo.val ≤ x.lo.val ∧ x.hi.val ≤ hi.val
xn : x ≠ nan
xm : x.lo.val ≤ x' ∧ x' ≤ x.hi.val
⊢ ↑color_error / 2 = ↑(color_error / 2)
Tactic:
simp only [Rat.cast_div, Rat.cast_ofNat]
State after:
no goals

State before:
α β : Type
x' : ℝ
x : Interval
c : UInt8
hc : x.untrusted_quantize = c
lo : Floating
hl : c.unquantize.sub half_color_error.lo true = lo
hi : Floating
hh : c.unquantize.add half_color_error.lo false = hi
n : ¬(lo = nan ∨ hi = nan)
mn : c.unquantize ≠ nan
xn : x ≠ nan
xm : x.lo.val ≤ x' ∧ x' ≤ x.hi.val
e : half_color_error.lo.val ≤ ↑color_error / 2
n0 : ¬c.unquantize.sub half_color_error.lo true = nan
n1 : ¬c.unquantize.add half_color_error.lo false = nan
le_lo : ↑c.toNat / 256 + 1 / 512 ≤ lo.val + half_color_error.lo.val
le_hi : hi.val ≤ ↑c.toNat / 256 + 1 / 512 + half_color_error.lo.val
g : lo.val ≤ x.lo.val ∧ x.hi.val ≤ hi.val
⊢ ↑c.toNat / 256 + 1 / 2 / 256 ≤ x' + ↑color_error / 2
Tactic:
linarith
State after:
no goals

State before:
α β : Type
x' : ℝ
x : Interval
c : UInt8
hc : x.untrusted_quantize = c
lo : Floating
hl : c.unquantize.sub half_color_error.lo true = lo
hi : Floating
hh : c.unquantize.add half_color_error.lo false = hi
n : ¬(lo = nan ∨ hi = nan)
mn : c.unquantize ≠ nan
xn : x ≠ nan
xm : x.lo.val ≤ x' ∧ x' ≤ x.hi.val
e : half_color_error.lo.val ≤ ↑color_error / 2
n0 : ¬c.unquantize.sub half_color_error.lo true = nan
n1 : ¬c.unquantize.add half_color_error.lo false = nan
le_lo : ↑c.toNat / 256 + 1 / 512 ≤ lo.val + half_color_error.lo.val
le_hi : hi.val ≤ ↑c.toNat / 256 + 1 / 512 + half_color_error.lo.val
g : lo.val ≤ x.lo.val ∧ x.hi.val ≤ hi.val
⊢ x' ≤ ↑c.toNat / 256 + 1 / 2 / 256 + ↑color_error / 2
Tactic:
linarith
State after:
no goals

State before:
case neg
α β : Type
x' : ℝ
x : Interval
xm : x' ∈ approx x
c : UInt8
hc : x.untrusted_quantize = c
lo : Floating
hl : c.unquantize.sub half_color_error.lo true = lo
hi : Floating
hh : c.unquantize.add half_color_error.lo false = hi
n : ¬(lo = nan ∨ hi = nan)
n0 : ¬lo = nan
n1 : ¬hi = nan
mn : c.unquantize ≠ nan
g : ¬(lo.val ≤ x.lo.val ∧ x.hi.val ≤ hi.val)
⊢ x' ∈ approx (if lo.val ≤ x.lo.val ∧ x.hi.val ≤ hi.val then some c else none)
Tactic:
simp only [g, ↓reduceIte, approx_none, mem_univ]
State after:
no goals