internlm/Lean-Github huggingface dataset:
Theorem: Interval.mem_approx_quantize
Proof 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]
Proof 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))
Theorem: Interval.mem_approx_quantize
Proof 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]
Proof 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))
Theorem: Interval.mem_approx_quantize
Proof 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
Proof state after:
no goals
Theorem: Interval.mem_approx_quantize
Proof 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
Proof state after:
no goals
Theorem: Interval.mem_approx_quantize
Proof 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]
Proof state after:
no goals
Theorem: Interval.mem_approx_quantize
Proof 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
Proof state after:
no goals
Theorem: Interval.mem_approx_quantize
Proof 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
Proof state after:
no goals
Theorem: Interval.mem_approx_quantize
Proof 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]
Proof state after:
no goals
Theorem: Color.mem_approx_quantize
Proof state before:
α β : Type
c' : Color ℝ
c : Color Interval
cm : c' ∈ approx c
⊢ c' ∈ approx c.quantize
Tactic:
rw [quantize]
Proof state after:
α β : Type
c' : Color ℝ
c : Color Interval
cm : c' ∈ approx c
⊢ c' ∈
    approx
      (match (c.r.quantize, c.g.quantize, c.b.quantize, c.a.quantize) with
      | (some r, some g, some b, some a) => { r := r, g := g, b := b, a := a }
      | x => nan)
Theorem: Color.mem_approx_quantize
Proof state before:
α β : Type
c' : Color ℝ
c : Color Interval
cm : c' ∈ approx c
⊢ c' ∈
    approx
      (match (c.r.quantize, c.g.quantize, c.b.quantize, c.a.quantize) with
      | (some r, some g, some b, some a) => { r := r, g := g, b := b, a := a }
      | x => nan)
Tactic:
generalize hr : c.r.quantize = r
Proof state after:
α β : Type
c' : Color ℝ
c : Color Interval
cm : c' ∈ approx c
r : Option UInt8
hr : c.r.quantize = r
⊢ c' ∈
    approx
      (match (r, c.g.quantize, c.b.quantize, c.a.quantize) with
      | (some r, some g, some b, some a) => { r := r, g := g, b := b, a := a }
      | x => nan)
Theorem: Color.mem_approx_quantize
Proof state before:
α β : Type
c' : Color ℝ
c : Color Interval
cm : c' ∈ approx c
r : Option UInt8
hr : c.r.quantize = r
⊢ c' ∈
    approx
      (match (r, c.g.quantize, c.b.quantize, c.a.quantize) with
      | (some r, some g, some b, some a) => { r := r, g := g, b := b, a := a }
      | x => nan)
Tactic:
generalize hg : c.g.quantize = g
Proof state after:
α β : Type
c' : Color ℝ
c : Color Interval
cm : c' ∈ approx c
r : Option UInt8
hr : c.r.quantize = r
g : Option UInt8
hg : c.g.quantize = g
⊢ c' ∈
    approx
      (match (r, g, c.b.quantize, c.a.quantize) with
      | (some r, some g, some b, some a) => { r := r, g := g, b := b, a := a }
      | x => nan)
Theorem: Color.mem_approx_quantize
Proof state before:
α β : Type
c' : Color ℝ
c : Color Interval
cm : c' ∈ approx c
r : Option UInt8
hr : c.r.quantize = r
g : Option UInt8
hg : c.g.quantize = g
⊢ c' ∈
    approx
      (match (r, g, c.b.quantize, c.a.quantize) with
      | (some r, some g, some b, some a) => { r := r, g := g, b := b, a := a }
      | x => nan)
Tactic:
generalize hb : c.b.quantize = b
Proof state after:
α β : Type
c' : Color ℝ
c : Color Interval
cm : c' ∈ approx c
r : Option UInt8
hr : c.r.quantize = r
g : Option UInt8
hg : c.g.quantize = g
b : Option UInt8
hb : c.b.quantize = b
⊢ c' ∈
    approx
      (match (r, g, b, c.a.quantize) with
      | (some r, some g, some b, some a) => { r := r, g := g, b := b, a := a }
      | x => nan)
Theorem: Color.mem_approx_quantize
Proof state before:
α β : Type
c' : Color ℝ
c : Color Interval
cm : c' ∈ approx c
r : Option UInt8
hr : c.r.quantize = r
g : Option UInt8
hg : c.g.quantize = g
b : Option UInt8
hb : c.b.quantize = b
⊢ c' ∈
    approx
      (match (r, g, b, c.a.quantize) with
      | (some r, some g, some b, some a) => { r := r, g := g, b := b, a := a }
      | x => nan)
Tactic:
generalize ha : c.a.quantize = a
Proof state after:
α β : Type
c' : Color ℝ
c : Color Interval
cm : c' ∈ approx c
r : Option UInt8
hr : c.r.quantize = r
g : Option UInt8
hg : c.g.quantize = g
b : Option UInt8
hb : c.b.quantize = b
a : Option UInt8
ha : c.a.quantize = a
⊢ c' ∈
    approx
      (match (r, g, b, a) with
      | (some r, some g, some b, some a) => { r := r, g := g, b := b, a := a }
      | x => nan)
Theorem: Color.mem_approx_quantize
Proof state before:
α β : Type
c' : Color ℝ
c : Color Interval
cm : c' ∈ approx c
r : Option UInt8
hr : c.r.quantize = r
g : Option UInt8
hg : c.g.quantize = g
b : Option UInt8
hb : c.b.quantize = b
a : Option UInt8
ha : c.a.quantize = a
⊢ c' ∈
    approx
      (match (r, g, b, a) with
      | (some r, some g, some b, some a) => { r := r, g := g, b := b, a := a }
      | x => nan)
Tactic:
match r with
| none => simp only [approx_nan, mem_univ]
| some r =>
  match g with
  | none => simp only [approx_nan, mem_univ]
  | some g =>
  match b with
  | none => simp only [approx_nan, mem_univ]
  | some b =>
    match a with
    | none => simp only [approx_nan, mem_univ]
    | some a =>
      simp only [approx, mem_ite_univ_left]
      intro _
      simp only [approx] at cm; simp only [approx', mem_setOf_eq] at cm
      rcases cm with ⟨m0, m1, m2, m3⟩
      simp only [approx', mem_setOf_eq, ←approx_some, ←hr, ←hg, ←hb, ←ha,
        Interval.mem_approx_quantize, m0, m1, m2, m3, true_and]
Proof state after:
no goals
Theorem: Color.mem_approx_quantize
Proof state before:
α β : Type
c' : Color ℝ
c : Color Interval
cm : c' ∈ approx c
r g : Option UInt8
hg : c.g.quantize = g
b : Option UInt8
hb : c.b.quantize = b
a : Option UInt8
ha : c.a.quantize = a
hr : c.r.quantize = none
⊢ c' ∈
    approx
      (match (none, g, b, a) with
      | (some r, some g, some b, some a) => { r := r, g := g, b := b, a := a }
      | x => nan)
Tactic:
simp only [approx_nan, mem_univ]
Proof state after:
no goals
Theorem: Color.mem_approx_quantize
Proof state before:
α β : Type
c' : Color ℝ
c : Color Interval
cm : c' ∈ approx c
r✝ g : Option UInt8
hg : c.g.quantize = g
b : Option UInt8
hb : c.b.quantize = b
a : Option UInt8
ha : c.a.quantize = a
r : UInt8
hr : c.r.quantize = some r
⊢ c' ∈
    approx
      (match (some r, g, b, a) with
      | (some r, some g, some b, some a) => { r := r, g := g, b := b, a := a }
      | x => nan)
Tactic:
match g with
| none => simp only [approx_nan, mem_univ]
| some g =>
match b with
| none => simp only [approx_nan, mem_univ]
| some b =>
  match a with
  | none => simp only [approx_nan, mem_univ]
  | some a =>
    simp only [approx, mem_ite_univ_left]
    intro _
    simp only [approx] at cm; simp only [approx', mem_setOf_eq] at cm
    rcases cm with ⟨m0, m1, m2, m3⟩
    simp only [approx', mem_setOf_eq, ←approx_some, ←hr, ←hg, ←hb, ←ha,
      Interval.mem_approx_quantize, m0, m1, m2, m3, true_and]
Proof state after:
no goals
Theorem: Color.mem_approx_quantize
Proof state before:
α β : Type
c' : Color ℝ
c : Color Interval
cm : c' ∈ approx c
r✝ g b : Option UInt8
hb : c.b.quantize = b
a : Option UInt8
ha : c.a.quantize = a
r : UInt8
hr : c.r.quantize = some r
hg : c.g.quantize = none
⊢ c' ∈
    approx
      (match (some r, none, b, a) with
      | (some r, some g, some b, some a) => { r := r, g := g, b := b, a := a }
      | x => nan)
Tactic:
simp only [approx_nan, mem_univ]
Proof state after:
no goals
Theorem: Color.mem_approx_quantize
Proof state before:
α β : Type
c' : Color ℝ
c : Color Interval
cm : c' ∈ approx c
r✝ g✝ b : Option UInt8
hb : c.b.quantize = b
a : Option UInt8
ha : c.a.quantize = a
r : UInt8
hr : c.r.quantize = some r
g : UInt8
hg : c.g.quantize = some g
⊢ c' ∈
    approx
      (match (some r, some g, b, a) with
      | (some r, some g, some b, some a) => { r := r, g := g, b := b, a := a }
      | x => nan)
Tactic:
match b with
| none => simp only [approx_nan, mem_univ]
| some b =>
  match a with
  | none => simp only [approx_nan, mem_univ]
  | some a =>
    simp only [approx, mem_ite_univ_left]
    intro _
    simp only [approx] at cm; simp only [approx', mem_setOf_eq] at cm
    rcases cm with ⟨m0, m1, m2, m3⟩
    simp only [approx', mem_setOf_eq, ←approx_some, ←hr, ←hg, ←hb, ←ha,
      Interval.mem_approx_quantize, m0, m1, m2, m3, true_and]
Proof state after:
no goals
Theorem: Color.mem_approx_quantize
Proof state before:
α β : Type
c' : Color ℝ
c : Color Interval
cm : c' ∈ approx c
r✝ g✝ b a : Option UInt8
ha : c.a.quantize = a
r : UInt8
hr : c.r.quantize = some r
g : UInt8
hg : c.g.quantize = some g
hb : c.b.quantize = none
⊢ c' ∈
    approx
      (match (some r, some g, none, a) with
      | (some r, some g, some b, some a) => { r := r, g := g, b := b, a := a }
      | x => nan)
Tactic:
simp only [approx_nan, mem_univ]
Proof state after:
no goals
Theorem: Color.mem_approx_quantize
Proof state before:
α β : Type
c' : Color ℝ
c : Color Interval
cm : c' ∈ approx c
r✝ g✝ b✝ a : Option UInt8
ha : c.a.quantize = a
r : UInt8
hr : c.r.quantize = some r
g : UInt8
hg : c.g.quantize = some g
b : UInt8
hb : c.b.quantize = some b
⊢ c' ∈
    approx
      (match (some r, some g, some b, a) with
      | (some r, some g, some b, some a) => { r := r, g := g, b := b, a := a }
      | x => nan)
Tactic:
match a with
| none => simp only [approx_nan, mem_univ]
| some a =>
  simp only [approx, mem_ite_univ_left]
  intro _
  simp only [approx] at cm; simp only [approx', mem_setOf_eq] at cm
  rcases cm with ⟨m0, m1, m2, m3⟩
  simp only [approx', mem_setOf_eq, ←approx_some, ←hr, ←hg, ←hb, ←ha,
    Interval.mem_approx_quantize, m0, m1, m2, m3, true_and]
Proof state after:
no goals
Theorem: Color.mem_approx_quantize
Proof state before:
α β : Type
c' : Color ℝ
c : Color Interval
cm : c' ∈ approx c
r✝ g✝ b✝ a : Option UInt8
r : UInt8
hr : c.r.quantize = some r
g : UInt8
hg : c.g.quantize = some g
b : UInt8
hb : c.b.quantize = some b
ha : c.a.quantize = none
⊢ c' ∈
    approx
      (match (some r, some g, some b, none) with
      | (some r, some g, some b, some a) => { r := r, g := g, b := b, a := a }
      | x => nan)
Tactic:
simp only [approx_nan, mem_univ]
Proof state after:
no goals
Theorem: Color.mem_approx_quantize
Proof state before:
α β : Type
c' : Color ℝ
c : Color Interval
cm : c' ∈ approx c
r✝ g✝ b✝ a✝ : Option UInt8
r : UInt8
hr : c.r.quantize = some r
g : UInt8
hg : c.g.quantize = some g
b : UInt8
hb : c.b.quantize = some b
a : UInt8
ha : c.a.quantize = some a
⊢ c' ∈
    approx
      (match (some r, some g, some b, some a) with
      | (some r, some g, some b, some a) => { r := r, g := g, b := b, a := a }
      | x => nan)
Tactic:
simp only [approx, mem_ite_univ_left]
Proof state after:
α β : Type
c' : Color ℝ
c : Color Interval
cm : c' ∈ approx c
r✝ g✝ b✝ a✝ : Option UInt8
r : UInt8
hr : c.r.quantize = some r
g : UInt8
hg : c.g.quantize = some g
b : UInt8
hb : c.b.quantize = some b
a : UInt8
ha : c.a.quantize = some a
⊢ ¬{ r := r, g := g, b := b, a := a } = nan → c' ∈ { r := r, g := g, b := b, a := a }.approx'
Theorem: Color.mem_approx_quantize
Proof state before:
α β : Type
c' : Color ℝ
c : Color Interval
cm : c' ∈ approx c
r✝ g✝ b✝ a✝ : Option UInt8
r : UInt8
hr : c.r.quantize = some r
g : UInt8
hg : c.g.quantize = some g
b : UInt8
hb : c.b.quantize = some b
a : UInt8
ha : c.a.quantize = some a
⊢ ¬{ r := r, g := g, b := b, a := a } = nan → c' ∈ { r := r, g := g, b := b, a := a }.approx'
Tactic:
intro _
Proof state after:
α β : Type
c' : Color ℝ
c : Color Interval
cm : c' ∈ approx c
r✝ g✝ b✝ a✝¹ : Option UInt8
r : UInt8
hr : c.r.quantize = some r
g : UInt8
hg : c.g.quantize = some g
b : UInt8
hb : c.b.quantize = some b
a : UInt8
ha : c.a.quantize = some a
a✝ : ¬{ r := r, g := g, b := b, a := a } = nan
⊢ c' ∈ { r := r, g := g, b := b, a := a }.approx'
Theorem: Color.mem_approx_quantize
Proof state before:
α β : Type
c' : Color ℝ
c : Color Interval
cm : c' ∈ approx c
r✝ g✝ b✝ a✝¹ : Option UInt8
r : UInt8
hr : c.r.quantize = some r
g : UInt8
hg : c.g.quantize = some g
b : UInt8
hb : c.b.quantize = some b
a : UInt8
ha : c.a.quantize = some a
a✝ : ¬{ r := r, g := g, b := b, a := a } = nan
⊢ c' ∈ { r := r, g := g, b := b, a := a }.approx'
Tactic:
simp only [approx] at cm
Proof state after:
α β : Type
c' : Color ℝ
c : Color Interval
cm : c' ∈ c.approx'
r✝ g✝ b✝ a✝¹ : Option UInt8
r : UInt8
hr : c.r.quantize = some r
g : UInt8
hg : c.g.quantize = some g
b : UInt8
hb : c.b.quantize = some b
a : UInt8
ha : c.a.quantize = some a
a✝ : ¬{ r := r, g := g, b := b, a := a } = nan
⊢ c' ∈ { r := r, g := g, b := b, a := a }.approx'
Theorem: Color.mem_approx_quantize
Proof state before:
α β : Type
c' : Color ℝ
c : Color Interval
cm : c' ∈ c.approx'
r✝ g✝ b✝ a✝¹ : Option UInt8
r : UInt8
hr : c.r.quantize = some r
g : UInt8
hg : c.g.quantize = some g
b : UInt8
hb : c.b.quantize = some b
a : UInt8
ha : c.a.quantize = some a
a✝ : ¬{ r := r, g := g, b := b, a := a } = nan
⊢ c' ∈ { r := r, g := g, b := b, a := a }.approx'
Tactic:
simp only [approx', mem_setOf_eq] at cm
Proof state after:
α β : Type
c' : Color ℝ
c : Color Interval
cm : c'.r ∈ approx c.r ∧ c'.g ∈ approx c.g ∧ c'.b ∈ approx c.b ∧ c'.a ∈ approx c.a
r✝ g✝ b✝ a✝¹ : Option UInt8
r : UInt8
hr : c.r.quantize = some r
g : UInt8
hg : c.g.quantize = some g
b : UInt8
hb : c.b.quantize = some b
a : UInt8
ha : c.a.quantize = some a
a✝ : ¬{ r := r, g := g, b := b, a := a } = nan
⊢ c' ∈ { r := r, g := g, b := b, a := a }.approx'
Theorem: Color.mem_approx_quantize
Proof state before:
α β : Type
c' : Color ℝ
c : Color Interval
cm : c'.r ∈ approx c.r ∧ c'.g ∈ approx c.g ∧ c'.b ∈ approx c.b ∧ c'.a ∈ approx c.a
r✝ g✝ b✝ a✝¹ : Option UInt8
r : UInt8
hr : c.r.quantize = some r
g : UInt8
hg : c.g.quantize = some g
b : UInt8
hb : c.b.quantize = some b
a : UInt8
ha : c.a.quantize = some a
a✝ : ¬{ r := r, g := g, b := b, a := a } = nan
⊢ c' ∈ { r := r, g := g, b := b, a := a }.approx'
Tactic:
rcases cm with ⟨m0, m1, m2, m3⟩
Proof state after:
case intro.intro.intro
α β : Type
c' : Color ℝ
c : Color Interval
r✝ g✝ b✝ a✝¹ : Option UInt8
r : UInt8
hr : c.r.quantize = some r
g : UInt8
hg : c.g.quantize = some g
b : UInt8
hb : c.b.quantize = some b
a : UInt8
ha : c.a.quantize = some a
a✝ : ¬{ r := r, g := g, b := b, a := a } = nan
m0 : c'.r ∈ approx c.r
m1 : c'.g ∈ approx c.g
m2 : c'.b ∈ approx c.b
m3 : c'.a ∈ approx c.a
⊢ c' ∈ { r := r, g := g, b := b, a := a }.approx'
Theorem: Color.mem_approx_quantize
Proof state before:
case intro.intro.intro
α β : Type
c' : Color ℝ
c : Color Interval
r✝ g✝ b✝ a✝¹ : Option UInt8
r : UInt8
hr : c.r.quantize = some r
g : UInt8
hg : c.g.quantize = some g
b : UInt8
hb : c.b.quantize = some b
a : UInt8
ha : c.a.quantize = some a
a✝ : ¬{ r := r, g := g, b := b, a := a } = nan
m0 : c'.r ∈ approx c.r
m1 : c'.g ∈ approx c.g
m2 : c'.b ∈ approx c.b
m3 : c'.a ∈ approx c.a
⊢ c' ∈ { r := r, g := g, b := b, a := a }.approx'
Tactic:
simp only [approx', mem_setOf_eq, ←approx_some, ←hr, ←hg, ←hb, ←ha,
  Interval.mem_approx_quantize, m0, m1, m2, m3, true_and]
Proof state after:
no goals
Theorem: mem_approx_lerp
Proof state before:
α β α' β' : Type
inst✝⁹ : Approx α α'
inst✝⁸ : Approx β β'
inst✝⁷ : Add β
inst✝⁶ : Sub β
inst✝⁵ : AddGroup β'
inst✝⁴ : SMul α β
inst✝³ : SMul α' β'
inst✝² : ApproxAdd β β'
inst✝¹ : ApproxSub β β'
inst✝ : ApproxSMul α β α' β'
t' : α'
x' y' : β'
t : α
x y : β
tm : t' ∈ approx t
xm : x' ∈ approx x
ym : y' ∈ approx y
⊢ lerp t' x' y' ∈ approx (lerp t x y)
Tactic:
rw [lerp, lerp]
Proof state after:
α β α' β' : Type
inst✝⁹ : Approx α α'
inst✝⁸ : Approx β β'
inst✝⁷ : Add β
inst✝⁶ : Sub β
inst✝⁵ : AddGroup β'
inst✝⁴ : SMul α β
inst✝³ : SMul α' β'
inst✝² : ApproxAdd β β'
inst✝¹ : ApproxSub β β'
inst✝ : ApproxSMul α β α' β'
t' : α'
x' y' : β'
t : α
x y : β
tm : t' ∈ approx t
xm : x' ∈ approx x
ym : y' ∈ approx y
⊢ x' + t' • (y' - x') ∈ approx (x + t • (y - x))
Theorem: mem_approx_lerp
Proof state before:
α β α' β' : Type
inst✝⁹ : Approx α α'
inst✝⁸ : Approx β β'
inst✝⁷ : Add β
inst✝⁶ : Sub β
inst✝⁵ : AddGroup β'
inst✝⁴ : SMul α β
inst✝³ : SMul α' β'
inst✝² : ApproxAdd β β'
inst✝¹ : ApproxSub β β'
inst✝ : ApproxSMul α β α' β'
t' : α'
x' y' : β'
t : α
x y : β
tm : t' ∈ approx t
xm : x' ∈ approx x
ym : y' ∈ approx y
⊢ x' + t' • (y' - x') ∈ approx (x + t • (y - x))
Tactic:
mono
Proof state after:
no goals
Theorem: Color.mem_approx_ofRat
Proof state before:
α β α' β' : Type
inst✝¹ : Approx α α'
inst✝ : Approx β β'
c : Color ℚ
⊢ ↑c ∈ approx c.ofRat
Tactic:
simp only [coe, approx, ofRat, map]
Proof state after:
α β α' β' : Type
inst✝¹ : Approx α α'
inst✝ : Approx β β'
c : Color ℚ
⊢ { r := ↑c.r, g := ↑c.g, b := ↑c.b, a := ↑c.a } ∈
    { r := Interval.ofRat c.r, g := Interval.ofRat c.g, b := Interval.ofRat c.b, a := Interval.ofRat c.a }.approx'
Theorem: Color.mem_approx_ofRat
Proof state before:
α β α' β' : Type
inst✝¹ : Approx α α'
inst✝ : Approx β β'
c : Color ℚ
⊢ { r := ↑c.r, g := ↑c.g, b := ↑c.b, a := ↑c.a } ∈
    { r := Interval.ofRat c.r, g := Interval.ofRat c.g, b := Interval.ofRat c.b, a := Interval.ofRat c.a }.approx'
Tactic:
simp only [approx', mem_setOf_eq]
Proof state after:
α β α' β' : Type
inst✝¹ : Approx α α'
inst✝ : Approx β β'
c : Color ℚ
⊢ ↑c.r ∈ approx (Interval.ofRat c.r) ∧
    ↑c.g ∈ approx (Interval.ofRat c.g) ∧ ↑c.b ∈ approx (Interval.ofRat c.b) ∧ ↑c.a ∈ approx (Interval.ofRat c.a)
Theorem: Color.mem_approx_ofRat
Proof state before:
α β α' β' : Type
inst✝¹ : Approx α α'
inst✝ : Approx β β'
c : Color ℚ
⊢ ↑c.r ∈ approx (Interval.ofRat c.r) ∧
    ↑c.g ∈ approx (Interval.ofRat c.g) ∧ ↑c.b ∈ approx (Interval.ofRat c.b) ∧ ↑c.a ∈ approx (Interval.ofRat c.a)
Tactic:
refine ⟨?_, ?_, ?_, ?_⟩
Proof state after:
case refine_1
α β α' β' : Type
inst✝¹ : Approx α α'
inst✝ : Approx β β'
c : Color ℚ
⊢ ↑c.r ∈ approx (Interval.ofRat c.r)

case refine_2
α β α' β' : Type
inst✝¹ : Approx α α'
inst✝ : Approx β β'
c : Color ℚ
⊢ ↑c.g ∈ approx (Interval.ofRat c.g)

case refine_3
α β α' β' : Type
inst✝¹ : Approx α α'
inst✝ : Approx β β'
c : Color ℚ
⊢ ↑c.b ∈ approx (Interval.ofRat c.b)

case refine_4
α β α' β' : Type
inst✝¹ : Approx α α'
inst✝ : Approx β β'
c : Color ℚ
⊢ ↑c.a ∈ approx (Interval.ofRat c.a)
Theorem: Color.mem_approx_ofRat
Proof state before:
case refine_1
α β α' β' : Type
inst✝¹ : Approx α α'
inst✝ : Approx β β'
c : Color ℚ
⊢ ↑c.r ∈ approx (Interval.ofRat c.r)

case refine_2
α β α' β' : Type
inst✝¹ : Approx α α'
inst✝ : Approx β β'
c : Color ℚ
⊢ ↑c.g ∈ approx (Interval.ofRat c.g)

case refine_3
α β α' β' : Type
inst✝¹ : Approx α α'
inst✝ : Approx β β'
c : Color ℚ
⊢ ↑c.b ∈ approx (Interval.ofRat c.b)

case refine_4
α β α' β' : Type
inst✝¹ : Approx α α'
inst✝ : Approx β β'
c : Color ℚ
⊢ ↑c.a ∈ approx (Interval.ofRat c.a)
Tactic:
all_goals apply Interval.approx_ofRat
Proof state after:
no goals
Theorem: Color.mem_approx_ofRat
Proof state before:
case refine_4
α β α' β' : Type
inst✝¹ : Approx α α'
inst✝ : Approx β β'
c : Color ℚ
⊢ ↑c.a ∈ approx (Interval.ofRat c.a)
Tactic:
apply Interval.approx_ofRat
Proof state after:
no goals