intro x y
case h.right
u : ℝ → ℝ
hk : ∀ (x : ℝ), u x = (0 * x).exp
⊢ ∀ (x y : ℝ), id (x + y) = id x * u y + id y
case h.right
u : ℝ → ℝ
hk : ∀ (x : ℝ), u x = (0 * x).exp
x y : ℝ
⊢ id (x + y) = id x * u y + id y