rw[hy0x1]
u f : ℝ → ℝ
hm : StrictMono f ∨ StrictAnti f
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * u 0 + f 0
hu0 : u 0 ≠ 1
x : ℝ
hy0x1 : f 0 = f x * (1 - u 0)
⊢ f x = f 0 / (1 - u 0)
u f : ℝ → ℝ
hm : StrictMono f ∨ StrictAnti f
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * u 0 + f 0
hu0 : u 0 ≠ 1
x : ℝ
hy0x1 : f 0 = f x * (1 - u 0)
⊢ f x = f x * (1 - u 0) / (1 - u 0)