have hau : Antitone u := StrictAnti.antitone hm
case h.inr
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
h1 : ∀ (n : ℕ) (x : ℝ), u (↑n * x) = u x ^ n
h2 : ∀ (x : ℝ), u x * u (-x) = 1
hunz : ∀ (x : ℝ), 0 < u x
h3 : ∀ (x : ℝ), u (-x) = 1 / u x
h4 : ∀ (z : ℤ) (x : ℝ), u (↑z * x) = u x ^ z
k : ℝ
hk : k.exp = u 1
hnexp : ∀ (n : ℕ), u ↑n = (k * ↑n).exp
hzexp : ∀ (z : ℤ), u ↑z = (k * ↑z).exp
hp : ∀ (p : ℕ), 0 < p → ∀ (x : ℝ), u (x / ↑p) = u x ^ (1 / ↑p)
hq : ∀ (q : ℚ), u ↑q = (k * ↑q).exp
f : ℝ → ℝ := fun x => (k * x).exp
hf : ∀ (q : ℚ), u ↑q = f ↑q
hfm : Continuous f
hm : StrictAnti u
⊢ ∀ (x : ℝ), u x = (k * x).exp
case h.inr
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
h1 : ∀ (n : ℕ) (x : ℝ), u (↑n * x) = u x ^ n
h2 : ∀ (x : ℝ), u x * u (-x) = 1
hunz : ∀ (x : ℝ), 0 < u x
h3 : ∀ (x : ℝ), u (-x) = 1 / u x
h4 : ∀ (z : ℤ) (x : ℝ), u (↑z * x) = u x ^ z
k : ℝ
hk : k.exp = u 1
hnexp : ∀ (n : ℕ), u ↑n = (k * ↑n).exp
hzexp : ∀ (z : ℤ), u ↑z = (k * ↑z).exp
hp : ∀ (p : ℕ), 0 < p → ∀ (x : ℝ), u (x / ↑p) = u x ^ (1 / ↑p)
hq : ∀ (q : ℚ), u ↑q = (k * ↑q).exp
f : ℝ → ℝ := fun x => (k * x).exp
hf : ∀ (q : ℚ), u ↑q = f ↑q
hfm : Continuous f
hm : StrictAnti u
hau : Antitone u
⊢ ∀ (x : ℝ), u x = (k * x).exp