internlm/Lean-Github huggingface dataset:
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, k.exp = u 1
Tactic:
use Real.log (u 1)
Proof 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
Theorem: Romania1998P12.exp_characterization
Proof 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)
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
⊢ ∀ (n : ℕ), u ↑n = (k * ↑n).exp
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
n : ℕ
⊢ u ↑n = (k * ↑n).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
n : ℕ
⊢ u ↑n = (k * ↑n).exp
Tactic:
have h10 := h4 n 1
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
n : ℕ
h10 : u (↑↑n * 1) = u 1 ^ ↑n
⊢ u ↑n = (k * ↑n).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
n : ℕ
h10 : u (↑↑n * 1) = u 1 ^ ↑n
⊢ u ↑n = (k * ↑n).exp
Tactic:
rw [←hk, mul_one] at h10
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
n : ℕ
h10 : u ↑↑n = k.exp ^ ↑n
⊢ u ↑n = (k * ↑n).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
n : ℕ
h10 : u ↑↑n = k.exp ^ ↑n
⊢ u ↑n = (k * ↑n).exp
Tactic:
norm_cast at h10
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
n : ℕ
h10 : u ↑n = k.exp ^ n
⊢ u ↑n = (k * ↑n).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
n : ℕ
h10 : u ↑n = k.exp ^ n
⊢ u ↑n = (k * ↑n).exp
Tactic:
rw [h10, mul_comm]
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
n : ℕ
h10 : u ↑n = k.exp ^ n
⊢ k.exp ^ n = (↑n * k).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
n : ℕ
h10 : u ↑n = k.exp ^ n
⊢ k.exp ^ n = (↑n * k).exp
Tactic:
exact (Real.exp_nat_mul _ _).symm
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
⊢ ∀ (z : ℤ), u ↑z = (k * ↑z).exp
Tactic:
intro z
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
z : ℤ
⊢ u ↑z = (k * ↑z).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
z : ℤ
⊢ u ↑z = (k * ↑z).exp
Tactic:
obtain ⟨n, hn⟩ := int_dichotomy z
Proof 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
Theorem: Romania1998P12.exp_characterization
Proof 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
Proof 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
Theorem: Romania1998P12.exp_characterization
Proof 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
Proof 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
Theorem: Romania1998P12.exp_characterization
Proof 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
Proof state after:
no goals
Theorem: Romania1998P12.exp_characterization
Proof 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
Proof 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
Theorem: Romania1998P12.exp_characterization
Proof 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
Proof 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
Theorem: Romania1998P12.exp_characterization
Proof 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]
Proof 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
Theorem: Romania1998P12.exp_characterization
Proof 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]
Proof 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)
Theorem: Romania1998P12.exp_characterization
Proof 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
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
⊢ ∀ (p : ℕ), 0 < p → ∀ (x : ℝ), u (x / ↑p) = u x ^ (1 / ↑p)
Tactic:
intro p hp x
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
p : ℕ
hp : 0 < p
x : ℝ
⊢ u (x / ↑p) = u x ^ (1 / ↑p)
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
p : ℕ
hp : 0 < p
x : ℝ
⊢ u (x / ↑p) = u x ^ (1 / ↑p)
Tactic:
cases' p with p p
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
⊢ 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))
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 : ∀ (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
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 * ↑p.succ / ↑p.succ)
⊢ u (x / ↑(p + 1)) = u x ^ (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 * ↑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 _ _
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 * ↑p.succ / ↑p.succ)
h13 : x * ↑p.succ / ↑p.succ = x
⊢ u (x / ↑(p + 1)) = u x ^ (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 * ↑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
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
⊢ u (x / ↑(p + 1)) = u x ^ (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
⊢ u (x / ↑(p + 1)) = u x ^ (1 / ↑(p + 1))
Tactic:
rw [← h12]
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
⊢ 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
⊢ 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
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
⊢ 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
⊢ u (x / ↑(p + 1)) = (u (x / ↑p.succ) ^ p.succ) ^ (1 / ↑(p + 1))
Tactic:
rw [h14]
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
⊢ u (x / ↑(p + 1)) = (u (x / ↑p.succ) ^ ↑p.succ) ^ (1 / ↑(p + 1))