calc Real.exp (k * (x + y)) - 1
         = Real.exp (k * x + k * y) - 1 := by rw [mul_add]
       _ = Real.exp (k * x) * Real.exp (k * y) - 1 := by rw [Real.exp_add]
       _ = (Real.exp (k * x) - 1) * Real.exp (k * y) +
              (Real.exp (k * y) - 1) := by ring
case right
u : ℝ → ℝ
k : ℝ
hk : ∀ (x : ℝ), u x = (k * x).exp
hknz : k ≠ 0
f : ℝ → ℝ := fun x => (k * x).exp - 1
hfm : StrictMono f ∨ StrictAnti f
x y : ℝ
⊢ f (x + y) = f x * (k * y).exp + f y
no goals