internlm/Lean-Github huggingface dataset:
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
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
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
⊢ ∀ (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
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
⊢ ∀ (n : ℕ) (x : ℝ), u (↑n * x) = u x ^ n
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
n : ℕ
⊢ ∀ (x : ℝ), u (↑n * x) = u x ^ n
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
n : ℕ
⊢ ∀ (x : ℝ), u (↑n * x) = u x ^ n
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
⊢ ∀ (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)
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
⊢ ∀ (x : ℝ), u (↑0 * x) = u x ^ 0
Tactic:
intro x
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
x : ℝ
⊢ u (↑0 * x) = u x ^ 0
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
x : ℝ
⊢ u (↑0 * x) = u x ^ 0
Tactic:
simp only [Nat.zero_eq, CharP.cast_eq_zero, zero_mul, Real.rpow_zero]
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
x : ℝ
⊢ u 0 = u x ^ 0
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
x : ℝ
⊢ u 0 = u x ^ 0
Tactic:
exact hu0
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
pn : ℕ
hpn : ∀ (x : ℝ), u (↑pn * x) = u x ^ pn
⊢ ∀ (x : ℝ), u (↑(pn + 1) * x) = u x ^ (pn + 1)
Tactic:
intro x
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
pn : ℕ
hpn : ∀ (x : ℝ), u (↑pn * x) = u x ^ pn
x : ℝ
⊢ u (↑(pn + 1) * x) = u x ^ (pn + 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
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]
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
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)
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
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]
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
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)
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
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
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
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
Proof 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
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
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]
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
pn : ℕ
hpn : ∀ (x : ℝ), u (↑pn * x) = u x ^ pn
x : ℝ
⊢ ↑pn * x + x = (↑pn + 1) * 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
⊢ ∀ (x : ℝ), u x * u (-x) = 1
Tactic:
intro 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
x : ℝ
⊢ u x * u (-x) = 1
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
x : ℝ
⊢ u x * u (-x) = 1
Tactic:
have := hu x (-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
x : ℝ
this : u (x + -x) = u x * u (-x)
⊢ u x * u (-x) = 1
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
x : ℝ
this : u (x + -x) = u x * u (-x)
⊢ u x * u (-x) = 1
Tactic:
rw [add_right_neg] at this
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
x : ℝ
this : u 0 = u x * u (-x)
⊢ u x * u (-x) = 1
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
x : ℝ
this : u 0 = u x * u (-x)
⊢ u x * u (-x) = 1
Tactic:
rw [←this]
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
x : ℝ
this : u 0 = u x * u (-x)
⊢ u 0 = 1
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
x : ℝ
this : u 0 = u x * u (-x)
⊢ u 0 = 1
Tactic:
exact hu0
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
x : ℝ
⊢ 0 < u x
Tactic:
by_contra! H
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
x : ℝ
H : u x ≤ 0
⊢ False
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
x : ℝ
H : u x ≤ 0
⊢ False
Tactic:
obtain hlt | heq | hgt := lt_trichotomy x 0
Proof 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
Theorem: Romania1998P12.exp_characterization
Proof 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
Proof 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
Theorem: Romania1998P12.exp_characterization
Proof 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
Proof 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
Theorem: Romania1998P12.exp_characterization
Proof 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]
Proof state after:
no goals
Theorem: Romania1998P12.exp_characterization
Proof 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
Proof 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
Theorem: Romania1998P12.exp_characterization
Proof 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
Proof state after:
no goals
Theorem: Romania1998P12.exp_characterization
Proof 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
Proof 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
Theorem: Romania1998P12.exp_characterization
Proof 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
Proof 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
Theorem: Romania1998P12.exp_characterization
Proof 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]
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
⊢ ∀ (z : ℤ) (x : ℝ), u (↑z * x) = u x ^ z
Tactic:
intro z 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
z : ℤ
x : ℝ
⊢ u (↑z * x) = u x ^ z
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
z : ℤ
x : ℝ
⊢ u (↑z * x) = u x ^ z
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
z : ℤ
x : ℝ
n : ℕ
hn : ↑n = z ∨ -↑n = z
⊢ u (↑z * x) = u x ^ z
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
z : ℤ
x : ℝ
n : ℕ
hn : ↑n = z ∨ -↑n = z
⊢ u (↑z * x) = u x ^ z
Tactic:
rcases hn with rfl | hn
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
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
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
x : ℝ
n : ℕ
⊢ u (↑↑n * x) = u x ^ ↑n
Tactic:
have := h1 n x
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
x : ℝ
n : ℕ
this : u (↑n * x) = u x ^ n
⊢ u (↑↑n * x) = u x ^ ↑n
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
x : ℝ
n : ℕ
this : u (↑n * x) = u x ^ n
⊢ u (↑↑n * x) = u x ^ ↑n
Tactic:
norm_cast at this
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
z : ℤ
x : ℝ
n : ℕ
hn : -↑n = z
⊢ u (↑z * x) = u x ^ z
Tactic:
have h10 := h1 n x
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
z : ℤ
x : ℝ
n : ℕ
hn : -↑n = z
h10 : u (↑n * x) = u x ^ n
⊢ u (↑z * x) = u x ^ z
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
z : ℤ
x : ℝ
n : ℕ
hn : -↑n = z
h10 : u (↑n * x) = u x ^ n
⊢ u (↑z * x) = u x ^ z
Tactic:
rw [←hn]
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
z : ℤ
x : ℝ
n : ℕ
hn : -↑n = z
h10 : u (↑n * x) = u x ^ n
⊢ u (↑(-↑n) * x) = u x ^ (-↑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
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
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
z : ℤ
x : ℝ
n : ℕ
hn : -↑n = z
h10 : u (↑n * x) = u x ^ n
h11 : ↑(-↑n) * x = -(↑n * x)
⊢ u (↑(-↑n) * x) = u x ^ (-↑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
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 _]
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
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)
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
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]
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
z : ℤ
x : ℝ
n : ℕ
hn : -↑n = z
h10 : u (↑n * x) = u x ^ n
h11 : ↑(-↑n) * x = -(↑n * x)
⊢ (u x ^ n)⁻¹ = u x ^ (-↑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
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]
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
z : ℤ
x : ℝ
n : ℕ
hn : -↑n = z
h10 : u (↑n * x) = u x ^ n
h11 : ↑(-↑n) * x = -(↑n * x)
⊢ u x ^ n = u x ^ ↑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
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
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
z : ℤ
x : ℝ
n : ℕ
hn : -↑n = z
h10 : u (↑n * x) = u x ^ n
⊢ ↑(-↑n) * x = -(↑n * x)
Tactic:
norm_num
Proof state after:
no goals