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

State before:
α β α' β' : Type
inst✝¹ : Approx α α'
inst✝ : Approx β β'
c : Color ℚ
⊢ ↑c ∈ approx c.ofRat
Tactic:
simp only [coe, approx, ofRat, map]
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'

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

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 ⟨?_, ?_, ?_, ?_⟩
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)

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

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