internlm/Lean-Github huggingface dataset:
Theorem: Romania1998P12.exp_characterization
Proof 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)))
Proof 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))
Theorem: Romania1998P12.exp_characterization
Proof 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 _]
Proof 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)))
Theorem: Romania1998P12.exp_characterization
Proof 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
Proof state after:
no goals
Theorem: Romania1998P12.exp_characterization
Proof 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
Proof 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
Theorem: Romania1998P12.exp_characterization
Proof 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
Proof state after:
no goals
Theorem: Romania1998P12.exp_characterization
Proof 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
Proof 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)
Theorem: Romania1998P12.exp_characterization
Proof 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
Proof 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)
Theorem: Romania1998P12.exp_characterization
Proof 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]
Proof state after:
no goals
Theorem: Romania1998P12.exp_characterization
Proof 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
Proof 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)
Theorem: Romania1998P12.exp_characterization
Proof 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]
Proof 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)
Theorem: Romania1998P12.exp_characterization
Proof 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))
Proof 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)
Theorem: Romania1998P12.exp_characterization
Proof 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]
Proof 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)
Theorem: Romania1998P12.exp_characterization
Proof 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
Proof state after:
no goals
Theorem: Romania1998P12.exp_characterization
Proof 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
Proof 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
Theorem: Romania1998P12.exp_characterization
Proof 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
Proof state after:
no goals
Theorem: Romania1998P12.exp_characterization
Proof 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
Proof state after:
no goals
Theorem: Romania1998P12.exp_characterization
Proof 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]
Proof 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
Theorem: Romania1998P12.exp_characterization
Proof 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
Proof state after:
no goals
Theorem: Romania1998P12.exp_characterization
Proof 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
Proof state after:
no goals
Theorem: Romania1998P12.exp_characterization
Proof 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
Proof 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
Theorem: Romania1998P12.exp_characterization
Proof 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
Proof state after:
no goals
Theorem: Romania1998P12.exp_characterization
Proof 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
Proof 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
Theorem: Romania1998P12.exp_characterization
Proof 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
Proof state after:
no goals
Theorem: Romania1998P12.romania1998_p12_mp
Proof state before:
u : ℝ → ℝ
⊢ (∃ f, (StrictMono f ∨ StrictAnti f) ∧ ∀ (x y : ℝ), f (x + y) = f x * u y + f y) → ∃ k, ∀ (x : ℝ), u x = (k * x).exp
Tactic:
intro h
Proof state after:
u : ℝ → ℝ
h : ∃ f, (StrictMono f ∨ StrictAnti f) ∧ ∀ (x y : ℝ), f (x + y) = f x * u y + f y
⊢ ∃ k, ∀ (x : ℝ), u x = (k * x).exp
Theorem: Romania1998P12.romania1998_p12_mp
Proof state before:
u : ℝ → ℝ
h : ∃ f, (StrictMono f ∨ StrictAnti f) ∧ ∀ (x y : ℝ), f (x + y) = f x * u y + f y
⊢ ∃ k, ∀ (x : ℝ), u x = (k * x).exp
Tactic:
obtain ⟨f, hm, hf⟩ := h
Proof state after:
case intro.intro
u f : ℝ → ℝ
hm : StrictMono f ∨ StrictAnti f
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
⊢ ∃ k, ∀ (x : ℝ), u x = (k * x).exp