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

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

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