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

State before:
α β : Type
c' : Color ℝ
c : Color Interval
cm : c' ∈ approx c
⊢ c' ∈ approx c.quantize
Tactic:
rw [quantize]
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)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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