Theorem: Romania1998P12.exp_characterization (Compfiles/Romania1998P12.lean)

State before:
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
h1 : ∀ (n : ℕ) (x : ℝ), u (↑n * x) = u x ^ n
⊢ ∃ k, ∀ (x : ℝ), u x = (k * x).exp
Tactic:
have h2 : ∀ x, (u x) * u (-x) = 1 := by
  intro x
  have := hu x (-x)
  rw [add_right_neg] at this
  rw [←this]
  exact hu0
State after:
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
h1 : ∀ (n : ℕ) (x : ℝ), u (↑n * x) = u x ^ n
h2 : ∀ (x : ℝ), u x * u (-x) = 1
⊢ ∃ k, ∀ (x : ℝ), u x = (k * x).exp

State before:
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
h1 : ∀ (n : ℕ) (x : ℝ), u (↑n * x) = u x ^ n
h2 : ∀ (x : ℝ), u x * u (-x) = 1
hunz : ∀ (x : ℝ), 0 < u x
⊢ ∃ k, ∀ (x : ℝ), u x = (k * x).exp
Tactic:
have h3 : ∀ x, u (-x) = 1 / (u x) :=
  fun x ↦ eq_one_div_of_mul_eq_one_right (h2 x)
State after:
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
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
⊢ ∃ k, ∀ (x : ℝ), u x = (k * x).exp

State before:
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
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, ∀ (x : ℝ), u x = (k * x).exp
Tactic:
obtain ⟨k, hk⟩ : ∃ k, Real.exp k = u 1 := by
  use Real.log (u 1); exact Real.exp_log (hunz 1)
State after:
case intro
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
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
⊢ ∃ k, ∀ (x : ℝ), u x = (k * x).exp

State before:
case intro
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
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
⊢ ∃ k, ∀ (x : ℝ), u x = (k * x).exp
Tactic:
have hnexp : ∀ n : ℕ, u n = Real.exp (k * n) := by
  intro n
  have h10 := h4 n 1
  rw [←hk, mul_one] at h10
  norm_cast at h10
  rw [h10, mul_comm]
  exact (Real.exp_nat_mul _ _).symm
State after:
case intro
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
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
⊢ ∃ k, ∀ (x : ℝ), u x = (k * x).exp

State before:
case intro
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
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)
⊢ ∃ k, ∀ (x : ℝ), u x = (k * x).exp
Tactic:
have hq : ∀ q : ℚ, u q = Real.exp (k * q) := fun q ↦ by
  rw [Rat.cast_def q, hp q.den q.pos q.num, hzexp q.num, ←Real.exp_mul]
  ring_nf
State after:
case intro
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
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
⊢ ∃ k, ∀ (x : ℝ), u x = (k * x).exp

State before:
case intro
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
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
⊢ ∃ k, ∀ (x : ℝ), u x = (k * x).exp
Tactic:
use k
State after:
case h
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
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
⊢ ∀ (x : ℝ), u x = (k * x).exp

State before:
case h
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
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
⊢ ∀ (x : ℝ), u x = (k * x).exp
Tactic:
let f := λ x ↦ Real.exp (k * x)
State after:
case h
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
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
⊢ ∀ (x : ℝ), u x = (k * x).exp

State before:
case h
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
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
⊢ ∀ (x : ℝ), u x = (k * x).exp
Tactic:
have hf : ∀ q : ℚ, u q = f q := λ q ↦ hq q
State after:
case h
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
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
⊢ ∀ (x : ℝ), u x = (k * x).exp

State before:
case h
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
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
⊢ ∀ (x : ℝ), u x = (k * x).exp
Tactic:
have hfm : Continuous f := by continuity
State after:
case h
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
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
⊢ ∀ (x : ℝ), u x = (k * x).exp

State before:
case h
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
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
⊢ ∀ (x : ℝ), u x = (k * x).exp
Tactic:
cases' hm with hm hm
State after:
case h.inl
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 : StrictMono 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
⊢ ∀ (x : ℝ), u x = (k * x).exp

State before:
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
⊢ ∀ (n : ℕ) (x : ℝ), u (↑n * x) = u x ^ n
Tactic:
intro n
State after:
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
n : ℕ
⊢ ∀ (x : ℝ), u (↑n * x) = u x ^ n

State before:
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
n : ℕ
⊢ ∀ (x : ℝ), u (↑n * x) = u x ^ n
Tactic:
induction' n with pn hpn
State after:
case zero
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
⊢ ∀ (x : ℝ), u (↑0 * x) = u x ^ 0

case succ
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
pn : ℕ
hpn : ∀ (x : ℝ), u (↑pn * x) = u x ^ pn
⊢ ∀ (x : ℝ), u (↑(pn + 1) * x) = u x ^ (pn + 1)

State before:
case zero
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
⊢ ∀ (x : ℝ), u (↑0 * x) = u x ^ 0
Tactic:
intro x
State after:
case zero
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
x : ℝ
⊢ u (↑0 * x) = u x ^ 0

State before:
case zero
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
x : ℝ
⊢ u (↑0 * x) = u x ^ 0
Tactic:
simp only [Nat.zero_eq, CharP.cast_eq_zero, zero_mul, Real.rpow_zero]
State after:
case zero
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
x : ℝ
⊢ u 0 = u x ^ 0

State before:
case zero
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
x : ℝ
⊢ u 0 = u x ^ 0
Tactic:
exact hu0
State after:
no goals

State before:
case succ
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
pn : ℕ
hpn : ∀ (x : ℝ), u (↑pn * x) = u x ^ pn
⊢ ∀ (x : ℝ), u (↑(pn + 1) * x) = u x ^ (pn + 1)
Tactic:
intro x
State after:
case succ
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
pn : ℕ
hpn : ∀ (x : ℝ), u (↑pn * x) = u x ^ pn
x : ℝ
⊢ u (↑(pn + 1) * x) = u x ^ (pn + 1)

State before:
case succ
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
pn : ℕ
hpn : ∀ (x : ℝ), u (↑pn * x) = u x ^ pn
x : ℝ
⊢ u (↑(pn + 1) * x) = u x ^ (pn + 1)
Tactic:
have hp1: ↑(pn.succ) * x = ↑pn * x + x := by
  have : ↑pn * x + x = (↑pn + 1) * x := by ring
  rw[this, Nat.cast_succ]
State after:
case succ
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
pn : ℕ
hpn : ∀ (x : ℝ), u (↑pn * x) = u x ^ pn
x : ℝ
hp1 : ↑pn.succ * x = ↑pn * x + x
⊢ u (↑(pn + 1) * x) = u x ^ (pn + 1)

State before:
case succ
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
pn : ℕ
hpn : ∀ (x : ℝ), u (↑pn * x) = u x ^ pn
x : ℝ
hp1 : ↑pn.succ * x = ↑pn * x + x
⊢ u (↑(pn + 1) * x) = u x ^ (pn + 1)
Tactic:
rw[hp1, hu (↑pn * x) x, hpn x, mul_comm]
State after:
case succ
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
pn : ℕ
hpn : ∀ (x : ℝ), u (↑pn * x) = u x ^ pn
x : ℝ
hp1 : ↑pn.succ * x = ↑pn * x + x
⊢ u x * u x ^ pn = u x ^ (pn + 1)

State before:
case succ
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
pn : ℕ
hpn : ∀ (x : ℝ), u (↑pn * x) = u x ^ pn
x : ℝ
hp1 : ↑pn.succ * x = ↑pn * x + x
⊢ u x * u x ^ pn = u x ^ (pn + 1)
Tactic:
exact (pow_succ' (u x) pn).symm
State after:
no goals

State before:
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
pn : ℕ
hpn : ∀ (x : ℝ), u (↑pn * x) = u x ^ pn
x : ℝ
⊢ ↑pn.succ * x = ↑pn * x + x
Tactic:
have : ↑pn * x + x = (↑pn + 1) * x := by ring
State after:
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
pn : ℕ
hpn : ∀ (x : ℝ), u (↑pn * x) = u x ^ pn
x : ℝ
this : ↑pn * x + x = (↑pn + 1) * x
⊢ ↑pn.succ * x = ↑pn * x + x

State before:
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
pn : ℕ
hpn : ∀ (x : ℝ), u (↑pn * x) = u x ^ pn
x : ℝ
this : ↑pn * x + x = (↑pn + 1) * x
⊢ ↑pn.succ * x = ↑pn * x + x
Tactic:
rw[this, Nat.cast_succ]
State after:
no goals

State before:
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
pn : ℕ
hpn : ∀ (x : ℝ), u (↑pn * x) = u x ^ pn
x : ℝ
⊢ ↑pn * x + x = (↑pn + 1) * x
Tactic:
ring
State after:
no goals

State before:
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
h1 : ∀ (n : ℕ) (x : ℝ), u (↑n * x) = u x ^ n
⊢ ∀ (x : ℝ), u x * u (-x) = 1
Tactic:
intro x
State after:
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
h1 : ∀ (n : ℕ) (x : ℝ), u (↑n * x) = u x ^ n
x : ℝ
⊢ u x * u (-x) = 1

State before:
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
h1 : ∀ (n : ℕ) (x : ℝ), u (↑n * x) = u x ^ n
x : ℝ
⊢ u x * u (-x) = 1
Tactic:
have := hu x (-x)
State after:
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
h1 : ∀ (n : ℕ) (x : ℝ), u (↑n * x) = u x ^ n
x : ℝ
this : u (x + -x) = u x * u (-x)
⊢ u x * u (-x) = 1

State before:
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
h1 : ∀ (n : ℕ) (x : ℝ), u (↑n * x) = u x ^ n
x : ℝ
this : u (x + -x) = u x * u (-x)
⊢ u x * u (-x) = 1
Tactic:
rw [add_right_neg] at this
State after:
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
h1 : ∀ (n : ℕ) (x : ℝ), u (↑n * x) = u x ^ n
x : ℝ
this : u 0 = u x * u (-x)
⊢ u x * u (-x) = 1

State before:
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
h1 : ∀ (n : ℕ) (x : ℝ), u (↑n * x) = u x ^ n
x : ℝ
this : u 0 = u x * u (-x)
⊢ u x * u (-x) = 1
Tactic:
rw [←this]
State after:
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
h1 : ∀ (n : ℕ) (x : ℝ), u (↑n * x) = u x ^ n
x : ℝ
this : u 0 = u x * u (-x)
⊢ u 0 = 1

State before:
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
h1 : ∀ (n : ℕ) (x : ℝ), u (↑n * x) = u x ^ n
x : ℝ
this : u 0 = u x * u (-x)
⊢ u 0 = 1
Tactic:
exact hu0
State after:
no goals

State before:
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
h1 : ∀ (n : ℕ) (x : ℝ), u (↑n * x) = u x ^ n
h2 : ∀ (x : ℝ), u x * u (-x) = 1
x : ℝ
⊢ 0 < u x
Tactic:
by_contra! H
State after:
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
h1 : ∀ (n : ℕ) (x : ℝ), u (↑n * x) = u x ^ n
h2 : ∀ (x : ℝ), u x * u (-x) = 1
x : ℝ
H : u x ≤ 0
⊢ False

State before:
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
h1 : ∀ (n : ℕ) (x : ℝ), u (↑n * x) = u x ^ n
h2 : ∀ (x : ℝ), u x * u (-x) = 1
x : ℝ
H : u x ≤ 0
⊢ False
Tactic:
obtain hlt | heq | hgt := lt_trichotomy x 0
State after:
case inl
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
h1 : ∀ (n : ℕ) (x : ℝ), u (↑n * x) = u x ^ n
h2 : ∀ (x : ℝ), u x * u (-x) = 1
x : ℝ
H : u x ≤ 0
hlt : x < 0
⊢ False

case inr.inl
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
h1 : ∀ (n : ℕ) (x : ℝ), u (↑n * x) = u x ^ n
h2 : ∀ (x : ℝ), u x * u (-x) = 1
x : ℝ
H : u x ≤ 0
heq : x = 0
⊢ False

case inr.inr
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
h1 : ∀ (n : ℕ) (x : ℝ), u (↑n * x) = u x ^ n
h2 : ∀ (x : ℝ), u x * u (-x) = 1
x : ℝ
H : u x ≤ 0
hgt : 0 < x
⊢ False

State before:
case inl
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
h1 : ∀ (n : ℕ) (x : ℝ), u (↑n * x) = u x ^ n
h2 : ∀ (x : ℝ), u x * u (-x) = 1
x : ℝ
H : u x ≤ 0
hlt : x < 0
⊢ False
Tactic:
have h10 := h2 x
State after:
case inl
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
h1 : ∀ (n : ℕ) (x : ℝ), u (↑n * x) = u x ^ n
h2 : ∀ (x : ℝ), u x * u (-x) = 1
x : ℝ
H : u x ≤ 0
hlt : x < 0
h10 : u x * u (-x) = 1
⊢ False

State before:
case inl
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
h1 : ∀ (n : ℕ) (x : ℝ), u (↑n * x) = u x ^ n
h2 : ∀ (x : ℝ), u x * u (-x) = 1
x : ℝ
H : u x ≤ 0
hlt : x < 0
h10 : u x * u (-x) = 1
⊢ False
Tactic:
have hx0 : 0 < -x := neg_pos.mpr hlt
State after:
case inl
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
h1 : ∀ (n : ℕ) (x : ℝ), u (↑n * x) = u x ^ n
h2 : ∀ (x : ℝ), u x * u (-x) = 1
x : ℝ
H : u x ≤ 0
hlt : x < 0
h10 : u x * u (-x) = 1
hx0 : 0 < -x
⊢ False

State before:
case inl
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
h1 : ∀ (n : ℕ) (x : ℝ), u (↑n * x) = u x ^ n
h2 : ∀ (x : ℝ), u x * u (-x) = 1
x : ℝ
H : u x ≤ 0
hlt : x < 0
h10 : u x * u (-x) = 1
hx0 : 0 < -x
⊢ False
Tactic:
cases' hm with hm hm <;> nlinarith[hm hx0, hm hlt]
State after:
no goals

State before:
case inr.inl
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
h1 : ∀ (n : ℕ) (x : ℝ), u (↑n * x) = u x ^ n
h2 : ∀ (x : ℝ), u x * u (-x) = 1
x : ℝ
H : u x ≤ 0
heq : x = 0
⊢ False
Tactic:
rw [heq, hu0] at H
State after:
case inr.inl
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
h1 : ∀ (n : ℕ) (x : ℝ), u (↑n * x) = u x ^ n
h2 : ∀ (x : ℝ), u x * u (-x) = 1
x : ℝ
H : 1 ≤ 0
heq : x = 0
⊢ False

State before:
case inr.inl
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
h1 : ∀ (n : ℕ) (x : ℝ), u (↑n * x) = u x ^ n
h2 : ∀ (x : ℝ), u x * u (-x) = 1
x : ℝ
H : 1 ≤ 0
heq : x = 0
⊢ False
Tactic:
linarith
State after:
no goals

State before:
case inr.inr
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
h1 : ∀ (n : ℕ) (x : ℝ), u (↑n * x) = u x ^ n
h2 : ∀ (x : ℝ), u x * u (-x) = 1
x : ℝ
H : u x ≤ 0
hgt : 0 < x
⊢ False
Tactic:
have h10 := h2 x
State after:
case inr.inr
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
h1 : ∀ (n : ℕ) (x : ℝ), u (↑n * x) = u x ^ n
h2 : ∀ (x : ℝ), u x * u (-x) = 1
x : ℝ
H : u x ≤ 0
hgt : 0 < x
h10 : u x * u (-x) = 1
⊢ False

State before:
case inr.inr
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
h1 : ∀ (n : ℕ) (x : ℝ), u (↑n * x) = u x ^ n
h2 : ∀ (x : ℝ), u x * u (-x) = 1
x : ℝ
H : u x ≤ 0
hgt : 0 < x
h10 : u x * u (-x) = 1
⊢ False
Tactic:
have hx0 : -x < 0 := neg_lt_zero.mpr hgt
State after:
case inr.inr
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
h1 : ∀ (n : ℕ) (x : ℝ), u (↑n * x) = u x ^ n
h2 : ∀ (x : ℝ), u x * u (-x) = 1
x : ℝ
H : u x ≤ 0
hgt : 0 < x
h10 : u x * u (-x) = 1
hx0 : -x < 0
⊢ False

State before:
case inr.inr
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
h1 : ∀ (n : ℕ) (x : ℝ), u (↑n * x) = u x ^ n
h2 : ∀ (x : ℝ), u x * u (-x) = 1
x : ℝ
H : u x ≤ 0
hgt : 0 < x
h10 : u x * u (-x) = 1
hx0 : -x < 0
⊢ False
Tactic:
cases' hm with hm hm <;> nlinarith [hm hx0, hm hgt]
State after:
no goals

State before:
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
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
⊢ ∀ (z : ℤ) (x : ℝ), u (↑z * x) = u x ^ z
Tactic:
intro z x
State after:
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
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
z : ℤ
x : ℝ
⊢ u (↑z * x) = u x ^ z

State before:
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
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
z : ℤ
x : ℝ
⊢ u (↑z * x) = u x ^ z
Tactic:
obtain ⟨n, hn⟩ := int_dichotomy z
State after:
case intro
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
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
z : ℤ
x : ℝ
n : ℕ
hn : ↑n = z ∨ -↑n = z
⊢ u (↑z * x) = u x ^ z

State before:
case intro
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
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
z : ℤ
x : ℝ
n : ℕ
hn : ↑n = z ∨ -↑n = z
⊢ u (↑z * x) = u x ^ z
Tactic:
rcases hn with rfl | hn
State after:
case intro.inl
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
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
x : ℝ
n : ℕ
⊢ u (↑↑n * x) = u x ^ ↑n

case intro.inr
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
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
z : ℤ
x : ℝ
n : ℕ
hn : -↑n = z
⊢ u (↑z * x) = u x ^ z

State before:
case intro.inl
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
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
x : ℝ
n : ℕ
⊢ u (↑↑n * x) = u x ^ ↑n
Tactic:
have := h1 n x
State after:
case intro.inl
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
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
x : ℝ
n : ℕ
this : u (↑n * x) = u x ^ n
⊢ u (↑↑n * x) = u x ^ ↑n

State before:
case intro.inl
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
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
x : ℝ
n : ℕ
this : u (↑n * x) = u x ^ n
⊢ u (↑↑n * x) = u x ^ ↑n
Tactic:
norm_cast at this
State after:
no goals

State before:
case intro.inr
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
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
z : ℤ
x : ℝ
n : ℕ
hn : -↑n = z
⊢ u (↑z * x) = u x ^ z
Tactic:
have h10 := h1 n x
State after:
case intro.inr
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
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
z : ℤ
x : ℝ
n : ℕ
hn : -↑n = z
h10 : u (↑n * x) = u x ^ n
⊢ u (↑z * x) = u x ^ z

State before:
case intro.inr
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
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
z : ℤ
x : ℝ
n : ℕ
hn : -↑n = z
h10 : u (↑n * x) = u x ^ n
⊢ u (↑z * x) = u x ^ z
Tactic:
rw [←hn]
State after:
case intro.inr
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
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
z : ℤ
x : ℝ
n : ℕ
hn : -↑n = z
h10 : u (↑n * x) = u x ^ n
⊢ u (↑(-↑n) * x) = u x ^ (-↑n)

State before:
case intro.inr
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
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
z : ℤ
x : ℝ
n : ℕ
hn : -↑n = z
h10 : u (↑n * x) = u x ^ n
⊢ u (↑(-↑n) * x) = u x ^ (-↑n)
Tactic:
have h11: ↑(-((↑n):ℤ)) * x = - (n * x) := by norm_num
State after:
case intro.inr
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
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
z : ℤ
x : ℝ
n : ℕ
hn : -↑n = z
h10 : u (↑n * x) = u x ^ n
h11 : ↑(-↑n) * x = -(↑n * x)
⊢ u (↑(-↑n) * x) = u x ^ (-↑n)

State before:
case intro.inr
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
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
z : ℤ
x : ℝ
n : ℕ
hn : -↑n = z
h10 : u (↑n * x) = u x ^ n
h11 : ↑(-↑n) * x = -(↑n * x)
⊢ u (↑(-↑n) * x) = u x ^ (-↑n)
Tactic:
rw [h11, h3 _]
State after:
case intro.inr
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
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
z : ℤ
x : ℝ
n : ℕ
hn : -↑n = z
h10 : u (↑n * x) = u x ^ n
h11 : ↑(-↑n) * x = -(↑n * x)
⊢ 1 / u (↑n * x) = u x ^ (-↑n)

State before:
case intro.inr
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
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
z : ℤ
x : ℝ
n : ℕ
hn : -↑n = z
h10 : u (↑n * x) = u x ^ n
h11 : ↑(-↑n) * x = -(↑n * x)
⊢ 1 / u (↑n * x) = u x ^ (-↑n)
Tactic:
rw [h10, one_div]
State after:
case intro.inr
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
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
z : ℤ
x : ℝ
n : ℕ
hn : -↑n = z
h10 : u (↑n * x) = u x ^ n
h11 : ↑(-↑n) * x = -(↑n * x)
⊢ (u x ^ n)⁻¹ = u x ^ (-↑n)

State before:
case intro.inr
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
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
z : ℤ
x : ℝ
n : ℕ
hn : -↑n = z
h10 : u (↑n * x) = u x ^ n
h11 : ↑(-↑n) * x = -(↑n * x)
⊢ (u x ^ n)⁻¹ = u x ^ (-↑n)
Tactic:
rw [hn, inv_eq_iff_eq_inv, ←hn, zpow_neg, inv_inv]
State after:
case intro.inr
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
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
z : ℤ
x : ℝ
n : ℕ
hn : -↑n = z
h10 : u (↑n * x) = u x ^ n
h11 : ↑(-↑n) * x = -(↑n * x)
⊢ u x ^ n = u x ^ ↑n

State before:
case intro.inr
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
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
z : ℤ
x : ℝ
n : ℕ
hn : -↑n = z
h10 : u (↑n * x) = u x ^ n
h11 : ↑(-↑n) * x = -(↑n * x)
⊢ u x ^ n = u x ^ ↑n
Tactic:
rfl
State after:
no goals

State before:
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
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
z : ℤ
x : ℝ
n : ℕ
hn : -↑n = z
h10 : u (↑n * x) = u x ^ n
⊢ ↑(-↑n) * x = -(↑n * x)
Tactic:
norm_num
State after:
no goals

State before:
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
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, k.exp = u 1
Tactic:
use Real.log (u 1)
State after:
case h
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
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
⊢ (u 1).log.exp = u 1

State before:
case h
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
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
⊢ (u 1).log.exp = u 1
Tactic:
exact Real.exp_log (hunz 1)
State after:
no goals

State before:
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
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
⊢ ∀ (n : ℕ), u ↑n = (k * ↑n).exp
Tactic:
intro n
State after:
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
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
n : ℕ
⊢ u ↑n = (k * ↑n).exp

State before:
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
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
n : ℕ
⊢ u ↑n = (k * ↑n).exp
Tactic:
have h10 := h4 n 1
State after:
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
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
n : ℕ
h10 : u (↑↑n * 1) = u 1 ^ ↑n
⊢ u ↑n = (k * ↑n).exp

State before:
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
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
n : ℕ
h10 : u (↑↑n * 1) = u 1 ^ ↑n
⊢ u ↑n = (k * ↑n).exp
Tactic:
rw [←hk, mul_one] at h10
State after:
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
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
n : ℕ
h10 : u ↑↑n = k.exp ^ ↑n
⊢ u ↑n = (k * ↑n).exp

State before:
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
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
n : ℕ
h10 : u ↑↑n = k.exp ^ ↑n
⊢ u ↑n = (k * ↑n).exp
Tactic:
norm_cast at h10
State after:
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
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
n : ℕ
h10 : u ↑n = k.exp ^ n
⊢ u ↑n = (k * ↑n).exp

State before:
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
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
n : ℕ
h10 : u ↑n = k.exp ^ n
⊢ u ↑n = (k * ↑n).exp
Tactic:
rw [h10, mul_comm]
State after:
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
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
n : ℕ
h10 : u ↑n = k.exp ^ n
⊢ k.exp ^ n = (↑n * k).exp

State before:
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
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
n : ℕ
h10 : u ↑n = k.exp ^ n
⊢ k.exp ^ n = (↑n * k).exp
Tactic:
exact (Real.exp_nat_mul _ _).symm
State after:
no goals

State before:
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
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
⊢ ∀ (z : ℤ), u ↑z = (k * ↑z).exp
Tactic:
intro z
State after:
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
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
z : ℤ
⊢ u ↑z = (k * ↑z).exp

State before:
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
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
z : ℤ
⊢ u ↑z = (k * ↑z).exp
Tactic:
obtain ⟨n, hn⟩ := int_dichotomy z
State after:
case intro
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
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
z : ℤ
n : ℕ
hn : ↑n = z ∨ -↑n = z
⊢ u ↑z = (k * ↑z).exp

State before:
case intro
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
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
z : ℤ
n : ℕ
hn : ↑n = z ∨ -↑n = z
⊢ u ↑z = (k * ↑z).exp
Tactic:
rcases hn with rfl | rfl
State after:
case intro.inl
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
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
n : ℕ
⊢ u ↑↑n = (k * ↑↑n).exp

case intro.inr
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
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
n : ℕ
⊢ u ↑(-↑n) = (k * ↑(-↑n)).exp

State before:
case intro.inl
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
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
n : ℕ
⊢ u ↑↑n = (k * ↑↑n).exp
Tactic:
norm_cast
State after:
case intro.inl
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
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
n : ℕ
⊢ u ↑n = (k * ↑n).exp

State before:
case intro.inl
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
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
n : ℕ
⊢ u ↑n = (k * ↑n).exp
Tactic:
exact hnexp n
State after:
no goals

State before:
case intro.inr
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
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
n : ℕ
⊢ u ↑(-↑n) = (k * ↑(-↑n)).exp
Tactic:
have := h4 (-↑n) 1
State after:
case intro.inr
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
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
n : ℕ
this : u (↑(-↑n) * 1) = u 1 ^ (-↑n)
⊢ u ↑(-↑n) = (k * ↑(-↑n)).exp

State before:
case intro.inr
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
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
n : ℕ
this : u (↑(-↑n) * 1) = u 1 ^ (-↑n)
⊢ u ↑(-↑n) = (k * ↑(-↑n)).exp
Tactic:
rw[mul_one] at this
State after:
case intro.inr
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
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
n : ℕ
this : u ↑(-↑n) = u 1 ^ (-↑n)
⊢ u ↑(-↑n) = (k * ↑(-↑n)).exp

State before:
case intro.inr
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
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
n : ℕ
this : u ↑(-↑n) = u 1 ^ (-↑n)
⊢ u ↑(-↑n) = (k * ↑(-↑n)).exp
Tactic:
rw[this, ←hk]
State after:
case intro.inr
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
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
n : ℕ
this : u ↑(-↑n) = u 1 ^ (-↑n)
⊢ k.exp ^ (-↑n) = (k * ↑(-↑n)).exp

State before:
case intro.inr
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
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
n : ℕ
this : u ↑(-↑n) = u 1 ^ (-↑n)
⊢ k.exp ^ (-↑n) = (k * ↑(-↑n)).exp
Tactic:
rw [Real.exp_mul]
State after:
case intro.inr
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
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
n : ℕ
this : u ↑(-↑n) = u 1 ^ (-↑n)
⊢ k.exp ^ (-↑n) = k.exp ^ ↑(-↑n)

State before:
case intro.inr
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
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
n : ℕ
this : u ↑(-↑n) = u 1 ^ (-↑n)
⊢ k.exp ^ (-↑n) = k.exp ^ ↑(-↑n)
Tactic:
exact (Real.rpow_intCast _ _).symm
State after:
no goals

State before:
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
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
⊢ ∀ (p : ℕ), 0 < p → ∀ (x : ℝ), u (x / ↑p) = u x ^ (1 / ↑p)
Tactic:
intro p hp x
State after:
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
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
p : ℕ
hp : 0 < p
x : ℝ
⊢ u (x / ↑p) = u x ^ (1 / ↑p)

State before:
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
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
p : ℕ
hp : 0 < p
x : ℝ
⊢ u (x / ↑p) = u x ^ (1 / ↑p)
Tactic:
cases' p with p p
State after:
case zero
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
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
x : ℝ
hp : 0 < 0
⊢ u (x / ↑0) = u x ^ (1 / ↑0)

case succ
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
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
x : ℝ
p : ℕ
hp : 0 < p + 1
⊢ u (x / ↑(p + 1)) = u x ^ (1 / ↑(p + 1))

State before:
case succ
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
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
x : ℝ
p : ℕ
hp : 0 < p + 1
h12 : ∀ (n : ℕ), u (x / ↑p.succ) ^ n = u (x * ↑n / ↑p.succ)
⊢ u (x / ↑(p + 1)) = u x ^ (1 / ↑(p + 1))
Tactic:
replace h12 := h12 p.succ
State after:
case succ
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
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
x : ℝ
p : ℕ
hp : 0 < p + 1
h12 : u (x / ↑p.succ) ^ p.succ = u (x * ↑p.succ / ↑p.succ)
⊢ u (x / ↑(p + 1)) = u x ^ (1 / ↑(p + 1))

State before:
case succ
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
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
x : ℝ
p : ℕ
hp : 0 < p + 1
h12 : u (x / ↑p.succ) ^ p.succ = u (x * ↑p.succ / ↑p.succ)
⊢ u (x / ↑(p + 1)) = u x ^ (1 / ↑(p + 1))
Tactic:
have h13 : x * ↑(p.succ) / ↑(p.succ) = x := mul_div_cancel_of_invertible _ _
State after:
case succ
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
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
x : ℝ
p : ℕ
hp : 0 < p + 1
h12 : u (x / ↑p.succ) ^ p.succ = u (x * ↑p.succ / ↑p.succ)
h13 : x * ↑p.succ / ↑p.succ = x
⊢ u (x / ↑(p + 1)) = u x ^ (1 / ↑(p + 1))

State before:
case succ
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
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
x : ℝ
p : ℕ
hp : 0 < p + 1
h12 : u (x / ↑p.succ) ^ p.succ = u (x * ↑p.succ / ↑p.succ)
h13 : x * ↑p.succ / ↑p.succ = x
⊢ u (x / ↑(p + 1)) = u x ^ (1 / ↑(p + 1))
Tactic:
rw [h13] at h12
State after:
case succ
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
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
x : ℝ
p : ℕ
hp : 0 < p + 1
h12 : u (x / ↑p.succ) ^ p.succ = u x
h13 : x * ↑p.succ / ↑p.succ = x
⊢ u (x / ↑(p + 1)) = u x ^ (1 / ↑(p + 1))

State before:
case succ
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
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
x : ℝ
p : ℕ
hp : 0 < p + 1
h12 : u (x / ↑p.succ) ^ p.succ = u x
h13 : x * ↑p.succ / ↑p.succ = x
⊢ u (x / ↑(p + 1)) = u x ^ (1 / ↑(p + 1))
Tactic:
rw [← h12]
State after:
case succ
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
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
x : ℝ
p : ℕ
hp : 0 < p + 1
h12 : u (x / ↑p.succ) ^ p.succ = u x
h13 : x * ↑p.succ / ↑p.succ = x
⊢ u (x / ↑(p + 1)) = (u (x / ↑p.succ) ^ p.succ) ^ (1 / ↑(p + 1))

State before:
case succ
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
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
x : ℝ
p : ℕ
hp : 0 < p + 1
h12 : u (x / ↑p.succ) ^ p.succ = u x
h13 : x * ↑p.succ / ↑p.succ = x
⊢ u (x / ↑(p + 1)) = (u (x / ↑p.succ) ^ p.succ) ^ (1 / ↑(p + 1))
Tactic:
have h14: u (x / ↑(p.succ)) ^ p.succ = u (x / ↑(p.succ)) ^ (p.succ:ℝ) := by norm_cast
State after:
case succ
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
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
x : ℝ
p : ℕ
hp : 0 < p + 1
h12 : u (x / ↑p.succ) ^ p.succ = u x
h13 : x * ↑p.succ / ↑p.succ = x
h14 : u (x / ↑p.succ) ^ p.succ = u (x / ↑p.succ) ^ ↑p.succ
⊢ u (x / ↑(p + 1)) = (u (x / ↑p.succ) ^ p.succ) ^ (1 / ↑(p + 1))

State before:
case succ
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
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
x : ℝ
p : ℕ
hp : 0 < p + 1
h12 : u (x / ↑p.succ) ^ p.succ = u x
h13 : x * ↑p.succ / ↑p.succ = x
h14 : u (x / ↑p.succ) ^ p.succ = u (x / ↑p.succ) ^ ↑p.succ
⊢ u (x / ↑(p + 1)) = (u (x / ↑p.succ) ^ p.succ) ^ (1 / ↑(p + 1))
Tactic:
rw [h14]
State after:
case succ
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
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
x : ℝ
p : ℕ
hp : 0 < p + 1
h12 : u (x / ↑p.succ) ^ p.succ = u x
h13 : x * ↑p.succ / ↑p.succ = x
h14 : u (x / ↑p.succ) ^ p.succ = u (x / ↑p.succ) ^ ↑p.succ
⊢ u (x / ↑(p + 1)) = (u (x / ↑p.succ) ^ ↑p.succ) ^ (1 / ↑(p + 1))

State before:
case succ
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
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
x : ℝ
p : ℕ
hp : 0 < p + 1
h12 : u (x / ↑p.succ) ^ p.succ = u x
h13 : x * ↑p.succ / ↑p.succ = x
h14 : u (x / ↑p.succ) ^ p.succ = u (x / ↑p.succ) ^ ↑p.succ
⊢ u (x / ↑(p + 1)) = (u (x / ↑p.succ) ^ ↑p.succ) ^ (1 / ↑(p + 1))
Tactic:
have h15 := le_of_lt (hunz (x / ↑(p.succ)))
State after:
case succ
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
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
x : ℝ
p : ℕ
hp : 0 < p + 1
h12 : u (x / ↑p.succ) ^ p.succ = u x
h13 : x * ↑p.succ / ↑p.succ = x
h14 : u (x / ↑p.succ) ^ p.succ = u (x / ↑p.succ) ^ ↑p.succ
h15 : 0 ≤ u (x / ↑p.succ)
⊢ u (x / ↑(p + 1)) = (u (x / ↑p.succ) ^ ↑p.succ) ^ (1 / ↑(p + 1))

State before:
case succ
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
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
x : ℝ
p : ℕ
hp : 0 < p + 1
h12 : u (x / ↑p.succ) ^ p.succ = u x
h13 : x * ↑p.succ / ↑p.succ = x
h14 : u (x / ↑p.succ) ^ p.succ = u (x / ↑p.succ) ^ ↑p.succ
h15 : 0 ≤ u (x / ↑p.succ)
⊢ u (x / ↑(p + 1)) = (u (x / ↑p.succ) ^ ↑p.succ) ^ (1 / ↑(p + 1))
Tactic:
rw [←Real.rpow_mul h15 _]
State after:
case succ
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
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
x : ℝ
p : ℕ
hp : 0 < p + 1
h12 : u (x / ↑p.succ) ^ p.succ = u x
h13 : x * ↑p.succ / ↑p.succ = x
h14 : u (x / ↑p.succ) ^ p.succ = u (x / ↑p.succ) ^ ↑p.succ
h15 : 0 ≤ u (x / ↑p.succ)
⊢ u (x / ↑(p + 1)) = u (x / ↑p.succ) ^ (↑p.succ * (1 / ↑(p + 1)))

State before:
case succ
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
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
x : ℝ
p : ℕ
hp : 0 < p + 1
h12 : u (x / ↑p.succ) ^ p.succ = u x
h13 : x * ↑p.succ / ↑p.succ = x
h14 : u (x / ↑p.succ) ^ p.succ = u (x / ↑p.succ) ^ ↑p.succ
h15 : 0 ≤ u (x / ↑p.succ)
⊢ u (x / ↑(p + 1)) = u (x / ↑p.succ) ^ (↑p.succ * (1 / ↑(p + 1)))
Tactic:
field_simp
State after:
no goals

State before:
case zero
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
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
x : ℝ
hp : 0 < 0
⊢ u (x / ↑0) = u x ^ (1 / ↑0)
Tactic:
exfalso
State after:
case zero
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
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
x : ℝ
hp : 0 < 0
⊢ False

State before:
case zero
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
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
x : ℝ
hp : 0 < 0
⊢ False
Tactic:
exact Nat.lt_asymm hp hp
State after:
no goals

State before:
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
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
x : ℝ
p : ℕ
hp : 0 < p + 1
⊢ ∀ (n : ℕ), u (x / ↑p.succ) ^ n = u (x * ↑n / ↑p.succ)
Tactic:
intro n
State after:
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
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
x : ℝ
p : ℕ
hp : 0 < p + 1
n : ℕ
⊢ u (x / ↑p.succ) ^ n = u (x * ↑n / ↑p.succ)

State before:
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
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
x : ℝ
p : ℕ
hp : 0 < p + 1
n : ℕ
⊢ u (x / ↑p.succ) ^ n = u (x * ↑n / ↑p.succ)
Tactic:
induction' n with pn hpn
State after:
case zero
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
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
x : ℝ
p : ℕ
hp : 0 < p + 1
⊢ u (x / ↑p.succ) ^ 0 = u (x * ↑0 / ↑p.succ)

case succ
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
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
x : ℝ
p : ℕ
hp : 0 < p + 1
pn : ℕ
hpn : u (x / ↑p.succ) ^ pn = u (x * ↑pn / ↑p.succ)
⊢ u (x / ↑p.succ) ^ (pn + 1) = u (x * ↑(pn + 1) / ↑p.succ)

State before:
case zero
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
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
x : ℝ
p : ℕ
hp : 0 < p + 1
⊢ u (x / ↑p.succ) ^ 0 = u (x * ↑0 / ↑p.succ)
Tactic:
simp [hu0.symm]
State after:
no goals

State before:
case succ
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
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
x : ℝ
p : ℕ
hp : 0 < p + 1
pn : ℕ
hpn : u (x / ↑p.succ) ^ pn = u (x * ↑pn / ↑p.succ)
⊢ u (x / ↑p.succ) ^ (pn + 1) = u (x * ↑(pn + 1) / ↑p.succ)
Tactic:
have h10: x * ↑(pn.succ) / ↑(p.succ) = x * ↑pn / ↑(p.succ) + x / ↑(p.succ) := by
  field_simp; ring
State after:
case succ
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
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
x : ℝ
p : ℕ
hp : 0 < p + 1
pn : ℕ
hpn : u (x / ↑p.succ) ^ pn = u (x * ↑pn / ↑p.succ)
h10 : x * ↑pn.succ / ↑p.succ = x * ↑pn / ↑p.succ + x / ↑p.succ
⊢ u (x / ↑p.succ) ^ (pn + 1) = u (x * ↑(pn + 1) / ↑p.succ)

State before:
case succ
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
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
x : ℝ
p : ℕ
hp : 0 < p + 1
pn : ℕ
hpn : u (x / ↑p.succ) ^ pn = u (x * ↑pn / ↑p.succ)
h10 : x * ↑pn.succ / ↑p.succ = x * ↑pn / ↑p.succ + x / ↑p.succ
⊢ u (x / ↑p.succ) ^ (pn + 1) = u (x * ↑(pn + 1) / ↑p.succ)
Tactic:
rw [h10]
State after:
case succ
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
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
x : ℝ
p : ℕ
hp : 0 < p + 1
pn : ℕ
hpn : u (x / ↑p.succ) ^ pn = u (x * ↑pn / ↑p.succ)
h10 : x * ↑pn.succ / ↑p.succ = x * ↑pn / ↑p.succ + x / ↑p.succ
⊢ u (x / ↑p.succ) ^ (pn + 1) = u (x * ↑pn / ↑p.succ + x / ↑p.succ)

State before:
case succ
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
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
x : ℝ
p : ℕ
hp : 0 < p + 1
pn : ℕ
hpn : u (x / ↑p.succ) ^ pn = u (x * ↑pn / ↑p.succ)
h10 : x * ↑pn.succ / ↑p.succ = x * ↑pn / ↑p.succ + x / ↑p.succ
⊢ u (x / ↑p.succ) ^ (pn + 1) = u (x * ↑pn / ↑p.succ + x / ↑p.succ)
Tactic:
have h11 := hu (x * ↑pn / ↑(p.succ)) (x / ↑(p.succ))
State after:
case succ
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
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
x : ℝ
p : ℕ
hp : 0 < p + 1
pn : ℕ
hpn : u (x / ↑p.succ) ^ pn = u (x * ↑pn / ↑p.succ)
h10 : x * ↑pn.succ / ↑p.succ = x * ↑pn / ↑p.succ + x / ↑p.succ
h11 : u (x * ↑pn / ↑p.succ + x / ↑p.succ) = u (x * ↑pn / ↑p.succ) * u (x / ↑p.succ)
⊢ u (x / ↑p.succ) ^ (pn + 1) = u (x * ↑pn / ↑p.succ + x / ↑p.succ)

State before:
case succ
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
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
x : ℝ
p : ℕ
hp : 0 < p + 1
pn : ℕ
hpn : u (x / ↑p.succ) ^ pn = u (x * ↑pn / ↑p.succ)
h10 : x * ↑pn.succ / ↑p.succ = x * ↑pn / ↑p.succ + x / ↑p.succ
h11 : u (x * ↑pn / ↑p.succ + x / ↑p.succ) = u (x * ↑pn / ↑p.succ) * u (x / ↑p.succ)
⊢ u (x / ↑p.succ) ^ (pn + 1) = u (x * ↑pn / ↑p.succ + x / ↑p.succ)
Tactic:
rw [h11, ← hpn]
State after:
case succ
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
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
x : ℝ
p : ℕ
hp : 0 < p + 1
pn : ℕ
hpn : u (x / ↑p.succ) ^ pn = u (x * ↑pn / ↑p.succ)
h10 : x * ↑pn.succ / ↑p.succ = x * ↑pn / ↑p.succ + x / ↑p.succ
h11 : u (x * ↑pn / ↑p.succ + x / ↑p.succ) = u (x * ↑pn / ↑p.succ) * u (x / ↑p.succ)
⊢ u (x / ↑p.succ) ^ (pn + 1) = u (x / ↑p.succ) ^ pn * u (x / ↑p.succ)

State before:
case succ
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
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
x : ℝ
p : ℕ
hp : 0 < p + 1
pn : ℕ
hpn : u (x / ↑p.succ) ^ pn = u (x * ↑pn / ↑p.succ)
h10 : x * ↑pn.succ / ↑p.succ = x * ↑pn / ↑p.succ + x / ↑p.succ
h11 : u (x * ↑pn / ↑p.succ + x / ↑p.succ) = u (x * ↑pn / ↑p.succ) * u (x / ↑p.succ)
⊢ u (x / ↑p.succ) ^ (pn + 1) = u (x / ↑p.succ) ^ pn * u (x / ↑p.succ)
Tactic:
norm_cast
State after:
no goals

State before:
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
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
x : ℝ
p : ℕ
hp : 0 < p + 1
pn : ℕ
hpn : u (x / ↑p.succ) ^ pn = u (x * ↑pn / ↑p.succ)
⊢ x * ↑pn.succ / ↑p.succ = x * ↑pn / ↑p.succ + x / ↑p.succ
Tactic:
field_simp
State after:
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
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
x : ℝ
p : ℕ
hp : 0 < p + 1
pn : ℕ
hpn : u (x / ↑p.succ) ^ pn = u (x * ↑pn / ↑p.succ)
⊢ x * (↑pn + 1) = x * ↑pn + x

State before:
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
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
x : ℝ
p : ℕ
hp : 0 < p + 1
pn : ℕ
hpn : u (x / ↑p.succ) ^ pn = u (x * ↑pn / ↑p.succ)
⊢ x * (↑pn + 1) = x * ↑pn + x
Tactic:
ring
State after:
no goals

State before:
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
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
x : ℝ
p : ℕ
hp : 0 < p + 1
h12 : u (x / ↑p.succ) ^ p.succ = u x
h13 : x * ↑p.succ / ↑p.succ = x
⊢ u (x / ↑p.succ) ^ p.succ = u (x / ↑p.succ) ^ ↑p.succ
Tactic:
norm_cast
State after:
no goals

State before:
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
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)
q : ℚ
⊢ u ↑q = (k * ↑q).exp
Tactic:
rw [Rat.cast_def q, hp q.den q.pos q.num, hzexp q.num, ←Real.exp_mul]
State after:
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
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)
q : ℚ
⊢ (k * ↑q.num * (1 / ↑q.den)).exp = (k * (↑q.num / ↑q.den)).exp

State before:
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
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)
q : ℚ
⊢ (k * ↑q.num * (1 / ↑q.den)).exp = (k * (↑q.num / ↑q.den)).exp
Tactic:
ring_nf
State after:
no goals

State before:
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
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
⊢ Continuous f
Tactic:
continuity
State after:
no goals

State before:
case h.inl
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 : StrictMono u
⊢ ∀ (x : ℝ), u x = (k * x).exp
Tactic:
have hmu : Monotone u := StrictMono.monotone hm
State after:
case h.inl
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 : StrictMono u
hmu : Monotone u
⊢ ∀ (x : ℝ), u x = (k * x).exp

State before:
case h.inl
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 : StrictMono u
hmu : Monotone u
⊢ ∀ (x : ℝ), u x = (k * x).exp
Tactic:
exact extend_function_mono u f hmu hfm hf
State after:
no goals

State before:
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
Tactic:
have hau : Antitone u := StrictAnti.antitone hm
State after:
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

State before:
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
Tactic:
exact extend_function_anti u f hau hfm hf
State after:
no goals