internlm/Lean-Github huggingface dataset:
Theorem: Imo2013P5.le_of_all_pow_lt_succ'
Proof state before:
x y : ℝ
hx : 1 < x
hy : 0 < y
h : ∀ (n : ℕ), 0 < n → x ^ n - 1 < y ^ n
hy'' : y ≤ 1
y' : ℝ
h1_lt_y' : 1 < y'
h_y'_lt_x : y' < x
h_y_lt_y' : y < y'
n : ℕ
hn : 0 < n
⊢ x ^ n - 1 < y' ^ n
Tactic:
calc x^n - 1 < y^n  := h n hn
     _  ≤ y'^n := pow_le_pow_left hy.le h_y_lt_y'.le n
Proof state after:
no goals
Theorem: Imo2013P5.f_pos_of_pos
Proof state before:
f : ℚ → ℝ
q : ℚ
hq : 0 < q
H1 : ∀ (x y : ℚ), 0 < x → 0 < y → f (x * y) ≤ f x * f y
H4 : ∀ (n : ℕ), 0 < n → ↑n ≤ f ↑n
⊢ 0 < f q
Tactic:
have hfqn := calc f q.num = f (q * q.den) := by rw [←Rat.mul_den_eq_num]
                  _ ≤ f q * f q.den := H1 q q.den hq (Nat.cast_pos.mpr q.pos)
Proof state after:
f : ℚ → ℝ
q : ℚ
hq : 0 < q
H1 : ∀ (x y : ℚ), 0 < x → 0 < y → f (x * y) ≤ f x * f y
H4 : ∀ (n : ℕ), 0 < n → ↑n ≤ f ↑n
hfqn : f ↑q.num ≤ f q * f ↑q.den
⊢ 0 < f q
Theorem: Imo2013P5.f_pos_of_pos
Proof state before:
f : ℚ → ℝ
q : ℚ
hq : 0 < q
H1 : ∀ (x y : ℚ), 0 < x → 0 < y → f (x * y) ≤ f x * f y
H4 : ∀ (n : ℕ), 0 < n → ↑n ≤ f ↑n
hfqn : f ↑q.num ≤ f q * f ↑q.den
⊢ 0 < f q
Tactic:
have num_pos : 0 < q.num := Rat.num_pos.mpr hq
Proof state after:
f : ℚ → ℝ
q : ℚ
hq : 0 < q
H1 : ∀ (x y : ℚ), 0 < x → 0 < y → f (x * y) ≤ f x * f y
H4 : ∀ (n : ℕ), 0 < n → ↑n ≤ f ↑n
hfqn : f ↑q.num ≤ f q * f ↑q.den
num_pos : 0 < q.num
⊢ 0 < f q
Theorem: Imo2013P5.f_pos_of_pos
Proof state before:
f : ℚ → ℝ
q : ℚ
hq : 0 < q
H1 : ∀ (x y : ℚ), 0 < x → 0 < y → f (x * y) ≤ f x * f y
H4 : ∀ (n : ℕ), 0 < n → ↑n ≤ f ↑n
hfqn : f ↑q.num ≤ f q * f ↑q.den
num_pos : 0 < q.num
⊢ 0 < f q
Tactic:
have hqna : (q.num.natAbs : ℤ) = q.num := Int.natAbs_of_nonneg num_pos.le
Proof state after:
f : ℚ → ℝ
q : ℚ
hq : 0 < q
H1 : ∀ (x y : ℚ), 0 < x → 0 < y → f (x * y) ≤ f x * f y
H4 : ∀ (n : ℕ), 0 < n → ↑n ≤ f ↑n
hfqn : f ↑q.num ≤ f q * f ↑q.den
num_pos : 0 < q.num
hqna : ↑q.num.natAbs = q.num
⊢ 0 < f q
Theorem: Imo2013P5.f_pos_of_pos
Proof state before:
f : ℚ → ℝ
q : ℚ
hq : 0 < q
H1 : ∀ (x y : ℚ), 0 < x → 0 < y → f (x * y) ≤ f x * f y
H4 : ∀ (n : ℕ), 0 < n → ↑n ≤ f ↑n
hfqn : f ↑q.num ≤ f q * f ↑q.den
num_pos : 0 < q.num
hqna : ↑q.num.natAbs = q.num
⊢ 0 < f q
Tactic:
have hqfn' := calc (q.num : ℝ)
       = ((q.num.natAbs : ℤ) : ℝ) := congr_arg Int.cast (Eq.symm hqna)
     _ ≤ f q.num.natAbs           := H4 q.num.natAbs
                                          (Int.natAbs_pos.mpr (ne_of_gt num_pos))
     _ = f q.num                   := by rw [Nat.cast_natAbs, abs_of_nonneg num_pos.le]
Proof state after:
f : ℚ → ℝ
q : ℚ
hq : 0 < q
H1 : ∀ (x y : ℚ), 0 < x → 0 < y → f (x * y) ≤ f x * f y
H4 : ∀ (n : ℕ), 0 < n → ↑n ≤ f ↑n
hfqn : f ↑q.num ≤ f q * f ↑q.den
num_pos : 0 < q.num
hqna : ↑q.num.natAbs = q.num
hqfn' : ↑q.num ≤ f ↑q.num
⊢ 0 < f q
Theorem: Imo2013P5.f_pos_of_pos
Proof state before:
f : ℚ → ℝ
q : ℚ
hq : 0 < q
H1 : ∀ (x y : ℚ), 0 < x → 0 < y → f (x * y) ≤ f x * f y
H4 : ∀ (n : ℕ), 0 < n → ↑n ≤ f ↑n
hfqn : f ↑q.num ≤ f q * f ↑q.den
num_pos : 0 < q.num
hqna : ↑q.num.natAbs = q.num
hqfn' : ↑q.num ≤ f ↑q.num
⊢ 0 < f q
Tactic:
have f_num_pos := calc (0 : ℝ) < q.num := Int.cast_pos.mpr num_pos
                       _ ≤ f q.num     := hqfn'
Proof state after:
f : ℚ → ℝ
q : ℚ
hq : 0 < q
H1 : ∀ (x y : ℚ), 0 < x → 0 < y → f (x * y) ≤ f x * f y
H4 : ∀ (n : ℕ), 0 < n → ↑n ≤ f ↑n
hfqn : f ↑q.num ≤ f q * f ↑q.den
num_pos : 0 < q.num
hqna : ↑q.num.natAbs = q.num
hqfn' : ↑q.num ≤ f ↑q.num
f_num_pos : 0 < f ↑q.num
⊢ 0 < f q
Theorem: Imo2013P5.f_pos_of_pos
Proof state before:
f : ℚ → ℝ
q : ℚ
hq : 0 < q
H1 : ∀ (x y : ℚ), 0 < x → 0 < y → f (x * y) ≤ f x * f y
H4 : ∀ (n : ℕ), 0 < n → ↑n ≤ f ↑n
hfqn : f ↑q.num ≤ f q * f ↑q.den
num_pos : 0 < q.num
hqna : ↑q.num.natAbs = q.num
hqfn' : ↑q.num ≤ f ↑q.num
f_num_pos : 0 < f ↑q.num
⊢ 0 < f q
Tactic:
have f_den_pos := calc (0 : ℝ) < q.den := Nat.cast_pos.mpr q.pos
                       _ ≤ f q.den     := H4 q.den q.pos
Proof state after:
f : ℚ → ℝ
q : ℚ
hq : 0 < q
H1 : ∀ (x y : ℚ), 0 < x → 0 < y → f (x * y) ≤ f x * f y
H4 : ∀ (n : ℕ), 0 < n → ↑n ≤ f ↑n
hfqn : f ↑q.num ≤ f q * f ↑q.den
num_pos : 0 < q.num
hqna : ↑q.num.natAbs = q.num
hqfn' : ↑q.num ≤ f ↑q.num
f_num_pos : 0 < f ↑q.num
f_den_pos : 0 < f ↑q.den
⊢ 0 < f q
Theorem: Imo2013P5.f_pos_of_pos
Proof state before:
f : ℚ → ℝ
q : ℚ
hq : 0 < q
H1 : ∀ (x y : ℚ), 0 < x → 0 < y → f (x * y) ≤ f x * f y
H4 : ∀ (n : ℕ), 0 < n → ↑n ≤ f ↑n
hfqn : f ↑q.num ≤ f q * f ↑q.den
num_pos : 0 < q.num
hqna : ↑q.num.natAbs = q.num
hqfn' : ↑q.num ≤ f ↑q.num
f_num_pos : 0 < f ↑q.num
f_den_pos : 0 < f ↑q.den
⊢ 0 < f q
Tactic:
nlinarith
Proof state after:
no goals
Theorem: Imo2013P5.f_pos_of_pos
Proof state before:
f : ℚ → ℝ
q : ℚ
hq : 0 < q
H1 : ∀ (x y : ℚ), 0 < x → 0 < y → f (x * y) ≤ f x * f y
H4 : ∀ (n : ℕ), 0 < n → ↑n ≤ f ↑n
⊢ f ↑q.num = f (q * ↑q.den)
Tactic:
rw [←Rat.mul_den_eq_num]
Proof state after:
no goals
Theorem: Imo2013P5.f_pos_of_pos
Proof state before:
f : ℚ → ℝ
q : ℚ
hq : 0 < q
H1 : ∀ (x y : ℚ), 0 < x → 0 < y → f (x * y) ≤ f x * f y
H4 : ∀ (n : ℕ), 0 < n → ↑n ≤ f ↑n
hfqn : f ↑q.num ≤ f q * f ↑q.den
num_pos : 0 < q.num
hqna : ↑q.num.natAbs = q.num
⊢ f ↑q.num.natAbs = f ↑q.num
Tactic:
rw [Nat.cast_natAbs, abs_of_nonneg num_pos.le]
Proof state after:
no goals
Theorem: Imo2013P5.fx_gt_xm1
Proof state before:
f : ℚ → ℝ
x : ℚ
hx : 1 ≤ x
H1 : ∀ (x y : ℚ), 0 < x → 0 < y → f (x * y) ≤ f x * f y
H2 : ∀ (x y : ℚ), 0 < x → 0 < y → f x + f y ≤ f (x + y)
H4 : ∀ (n : ℕ), 0 < n → ↑n ≤ f ↑n
⊢ ↑x - 1 < f x
Tactic:
have hx0 :=
  calc (x - 1 : ℝ)
        < ⌊x⌋₊   := by exact_mod_cast Nat.sub_one_lt_floor x
      _ ≤ f ⌊x⌋₊ := H4 _ (Nat.floor_pos.2 hx)
Proof state after:
f : ℚ → ℝ
x : ℚ
hx : 1 ≤ x
H1 : ∀ (x y : ℚ), 0 < x → 0 < y → f (x * y) ≤ f x * f y
H2 : ∀ (x y : ℚ), 0 < x → 0 < y → f x + f y ≤ f (x + y)
H4 : ∀ (n : ℕ), 0 < n → ↑n ≤ f ↑n
hx0 : ↑x - 1 < f ↑⌊x⌋₊
⊢ ↑x - 1 < f x
Theorem: Imo2013P5.fx_gt_xm1
Proof state before:
f : ℚ → ℝ
x : ℚ
hx : 1 ≤ x
H1 : ∀ (x y : ℚ), 0 < x → 0 < y → f (x * y) ≤ f x * f y
H2 : ∀ (x y : ℚ), 0 < x → 0 < y → f x + f y ≤ f (x + y)
H4 : ∀ (n : ℕ), 0 < n → ↑n ≤ f ↑n
hx0 : ↑x - 1 < f ↑⌊x⌋₊
⊢ ↑x - 1 < f x
Tactic:
obtain h_eq | h_lt := (Nat.floor_le $ zero_le_one.trans hx).eq_or_lt
Proof state after:
case inl
f : ℚ → ℝ
x : ℚ
hx : 1 ≤ x
H1 : ∀ (x y : ℚ), 0 < x → 0 < y → f (x * y) ≤ f x * f y
H2 : ∀ (x y : ℚ), 0 < x → 0 < y → f x + f y ≤ f (x + y)
H4 : ∀ (n : ℕ), 0 < n → ↑n ≤ f ↑n
hx0 : ↑x - 1 < f ↑⌊x⌋₊
h_eq : ↑⌊x⌋₊ = x
⊢ ↑x - 1 < f x

case inr
f : ℚ → ℝ
x : ℚ
hx : 1 ≤ x
H1 : ∀ (x y : ℚ), 0 < x → 0 < y → f (x * y) ≤ f x * f y
H2 : ∀ (x y : ℚ), 0 < x → 0 < y → f x + f y ≤ f (x + y)
H4 : ∀ (n : ℕ), 0 < n → ↑n ≤ f ↑n
hx0 : ↑x - 1 < f ↑⌊x⌋₊
h_lt : ↑⌊x⌋₊ < x
⊢ ↑x - 1 < f x
Theorem: Imo2013P5.fx_gt_xm1
Proof state before:
case inr
f : ℚ → ℝ
x : ℚ
hx : 1 ≤ x
H1 : ∀ (x y : ℚ), 0 < x → 0 < y → f (x * y) ≤ f x * f y
H2 : ∀ (x y : ℚ), 0 < x → 0 < y → f x + f y ≤ f (x + y)
H4 : ∀ (n : ℕ), 0 < n → ↑n ≤ f ↑n
hx0 : ↑x - 1 < f ↑⌊x⌋₊
h_lt : ↑⌊x⌋₊ < x
⊢ ↑x - 1 < f x
Tactic:
calc (x - 1 : ℝ) < f ⌊x⌋₊ := hx0
  _ < f (x - ⌊x⌋₊) + f ⌊x⌋₊ := lt_add_of_pos_left _ (f_pos_of_pos (sub_pos.mpr h_lt) H1 H4)
  _ ≤ f (x - ⌊x⌋₊ + ⌊x⌋₊)   := H2 _ _ (sub_pos.mpr h_lt) (Nat.cast_pos.2 (Nat.floor_pos.2 hx))
  _ = f x                   := by rw [sub_add_cancel]
Proof state after:
no goals
Theorem: Imo2013P5.fx_gt_xm1
Proof state before:
f : ℚ → ℝ
x : ℚ
hx : 1 ≤ x
H1 : ∀ (x y : ℚ), 0 < x → 0 < y → f (x * y) ≤ f x * f y
H2 : ∀ (x y : ℚ), 0 < x → 0 < y → f x + f y ≤ f (x + y)
H4 : ∀ (n : ℕ), 0 < n → ↑n ≤ f ↑n
⊢ ↑x - 1 < ↑⌊x⌋₊
Tactic:
exact_mod_cast Nat.sub_one_lt_floor x
Proof state after:
no goals
Theorem: Imo2013P5.fx_gt_xm1
Proof state before:
case inl
f : ℚ → ℝ
x : ℚ
hx : 1 ≤ x
H1 : ∀ (x y : ℚ), 0 < x → 0 < y → f (x * y) ≤ f x * f y
H2 : ∀ (x y : ℚ), 0 < x → 0 < y → f x + f y ≤ f (x + y)
H4 : ∀ (n : ℕ), 0 < n → ↑n ≤ f ↑n
hx0 : ↑x - 1 < f ↑⌊x⌋₊
h_eq : ↑⌊x⌋₊ = x
⊢ ↑x - 1 < f x
Tactic:
rwa [h_eq] at hx0
Proof state after:
no goals
Theorem: Imo2013P5.fx_gt_xm1
Proof state before:
f : ℚ → ℝ
x : ℚ
hx : 1 ≤ x
H1 : ∀ (x y : ℚ), 0 < x → 0 < y → f (x * y) ≤ f x * f y
H2 : ∀ (x y : ℚ), 0 < x → 0 < y → f x + f y ≤ f (x + y)
H4 : ∀ (n : ℕ), 0 < n → ↑n ≤ f ↑n
hx0 : ↑x - 1 < f ↑⌊x⌋₊
h_lt : ↑⌊x⌋₊ < x
⊢ f (x - ↑⌊x⌋₊ + ↑⌊x⌋₊) = f x
Tactic:
rw [sub_add_cancel]
Proof state after:
no goals
Theorem: Imo2013P5.pow_f_le_f_pow
Proof state before:
f : ℚ → ℝ
n : ℕ
hn : 0 < n
x : ℚ
hx : 1 < x
H1 : ∀ (x y : ℚ), 0 < x → 0 < y → f (x * y) ≤ f x * f y
H4 : ∀ (n : ℕ), 0 < n → ↑n ≤ f ↑n
⊢ f (x ^ n) ≤ f x ^ n
Tactic:
induction n with
| zero => exfalso; exact Nat.lt_asymm hn hn
| succ pn hpn =>
  cases pn with
  | zero => simp [show Nat.succ 0 = 1 by rfl, pow_one]
  | succ pn =>
    have hpn' := hpn pn.succ_pos
    rw [pow_succ x (pn + 1), pow_succ (f x) (pn + 1)]
    have hxp : 0 < x := zero_lt_one.trans hx
    calc f ((x ^ (pn+1)) * x)
        ≤ f (x ^ (pn+1)) * f x := H1 (x ^ (pn+1)) x (pow_pos hxp (pn+1)) hxp
      _ ≤ (f x) ^ (pn+1) * f x := (mul_le_mul_right (f_pos_of_pos hxp H1 H4)).mpr hpn'
Proof state after:
no goals
Theorem: Imo2013P5.pow_f_le_f_pow
Proof state before:
case zero
f : ℚ → ℝ
x : ℚ
hx : 1 < x
H1 : ∀ (x y : ℚ), 0 < x → 0 < y → f (x * y) ≤ f x * f y
H4 : ∀ (n : ℕ), 0 < n → ↑n ≤ f ↑n
hn : 0 < 0
⊢ f (x ^ 0) ≤ f x ^ 0
Tactic:
exfalso
Proof state after:
case zero
f : ℚ → ℝ
x : ℚ
hx : 1 < x
H1 : ∀ (x y : ℚ), 0 < x → 0 < y → f (x * y) ≤ f x * f y
H4 : ∀ (n : ℕ), 0 < n → ↑n ≤ f ↑n
hn : 0 < 0
⊢ False
Theorem: Imo2013P5.pow_f_le_f_pow
Proof state before:
case zero
f : ℚ → ℝ
x : ℚ
hx : 1 < x
H1 : ∀ (x y : ℚ), 0 < x → 0 < y → f (x * y) ≤ f x * f y
H4 : ∀ (n : ℕ), 0 < n → ↑n ≤ f ↑n
hn : 0 < 0
⊢ False
Tactic:
exact Nat.lt_asymm hn hn
Proof state after:
no goals
Theorem: Imo2013P5.pow_f_le_f_pow
Proof state before:
case succ
f : ℚ → ℝ
x : ℚ
hx : 1 < x
H1 : ∀ (x y : ℚ), 0 < x → 0 < y → f (x * y) ≤ f x * f y
H4 : ∀ (n : ℕ), 0 < n → ↑n ≤ f ↑n
pn : ℕ
hpn : 0 < pn → f (x ^ pn) ≤ f x ^ pn
hn : 0 < pn + 1
⊢ f (x ^ (pn + 1)) ≤ f x ^ (pn + 1)
Tactic:
cases pn with
| zero => simp [show Nat.succ 0 = 1 by rfl, pow_one]
| succ pn =>
  have hpn' := hpn pn.succ_pos
  rw [pow_succ x (pn + 1), pow_succ (f x) (pn + 1)]
  have hxp : 0 < x := zero_lt_one.trans hx
  calc f ((x ^ (pn+1)) * x)
      ≤ f (x ^ (pn+1)) * f x := H1 (x ^ (pn+1)) x (pow_pos hxp (pn+1)) hxp
    _ ≤ (f x) ^ (pn+1) * f x := (mul_le_mul_right (f_pos_of_pos hxp H1 H4)).mpr hpn'
Proof state after:
no goals
Theorem: Imo2013P5.pow_f_le_f_pow
Proof state before:
case succ.zero
f : ℚ → ℝ
x : ℚ
hx : 1 < x
H1 : ∀ (x y : ℚ), 0 < x → 0 < y → f (x * y) ≤ f x * f y
H4 : ∀ (n : ℕ), 0 < n → ↑n ≤ f ↑n
hpn : 0 < 0 → f (x ^ 0) ≤ f x ^ 0
hn : 0 < 0 + 1
⊢ f (x ^ (0 + 1)) ≤ f x ^ (0 + 1)
Tactic:
simp [show Nat.succ 0 = 1 by rfl, pow_one]
Proof state after:
no goals
Theorem: Imo2013P5.pow_f_le_f_pow
Proof state before:
f : ℚ → ℝ
x : ℚ
hx : 1 < x
H1 : ∀ (x y : ℚ), 0 < x → 0 < y → f (x * y) ≤ f x * f y
H4 : ∀ (n : ℕ), 0 < n → ↑n ≤ f ↑n
hpn : 0 < 0 → f (x ^ 0) ≤ f x ^ 0
hn : 0 < 0 + 1
⊢ Nat.succ 0 = 1
Tactic:
rfl
Proof state after:
no goals
Theorem: Imo2013P5.pow_f_le_f_pow
Proof state before:
case succ.succ
f : ℚ → ℝ
x : ℚ
hx : 1 < x
H1 : ∀ (x y : ℚ), 0 < x → 0 < y → f (x * y) ≤ f x * f y
H4 : ∀ (n : ℕ), 0 < n → ↑n ≤ f ↑n
pn : ℕ
hpn : 0 < pn + 1 → f (x ^ (pn + 1)) ≤ f x ^ (pn + 1)
hn : 0 < pn + 1 + 1
⊢ f (x ^ (pn + 1 + 1)) ≤ f x ^ (pn + 1 + 1)
Tactic:
have hpn' := hpn pn.succ_pos
Proof state after:
case succ.succ
f : ℚ → ℝ
x : ℚ
hx : 1 < x
H1 : ∀ (x y : ℚ), 0 < x → 0 < y → f (x * y) ≤ f x * f y
H4 : ∀ (n : ℕ), 0 < n → ↑n ≤ f ↑n
pn : ℕ
hpn : 0 < pn + 1 → f (x ^ (pn + 1)) ≤ f x ^ (pn + 1)
hn : 0 < pn + 1 + 1
hpn' : f (x ^ (pn + 1)) ≤ f x ^ (pn + 1)
⊢ f (x ^ (pn + 1 + 1)) ≤ f x ^ (pn + 1 + 1)
Theorem: Imo2013P5.pow_f_le_f_pow
Proof state before:
case succ.succ
f : ℚ → ℝ
x : ℚ
hx : 1 < x
H1 : ∀ (x y : ℚ), 0 < x → 0 < y → f (x * y) ≤ f x * f y
H4 : ∀ (n : ℕ), 0 < n → ↑n ≤ f ↑n
pn : ℕ
hpn : 0 < pn + 1 → f (x ^ (pn + 1)) ≤ f x ^ (pn + 1)
hn : 0 < pn + 1 + 1
hpn' : f (x ^ (pn + 1)) ≤ f x ^ (pn + 1)
⊢ f (x ^ (pn + 1 + 1)) ≤ f x ^ (pn + 1 + 1)
Tactic:
rw [pow_succ x (pn + 1), pow_succ (f x) (pn + 1)]
Proof state after:
case succ.succ
f : ℚ → ℝ
x : ℚ
hx : 1 < x
H1 : ∀ (x y : ℚ), 0 < x → 0 < y → f (x * y) ≤ f x * f y
H4 : ∀ (n : ℕ), 0 < n → ↑n ≤ f ↑n
pn : ℕ
hpn : 0 < pn + 1 → f (x ^ (pn + 1)) ≤ f x ^ (pn + 1)
hn : 0 < pn + 1 + 1
hpn' : f (x ^ (pn + 1)) ≤ f x ^ (pn + 1)
⊢ f (x ^ (pn + 1) * x) ≤ f x ^ (pn + 1) * f x
Theorem: Imo2013P5.pow_f_le_f_pow
Proof state before:
case succ.succ
f : ℚ → ℝ
x : ℚ
hx : 1 < x
H1 : ∀ (x y : ℚ), 0 < x → 0 < y → f (x * y) ≤ f x * f y
H4 : ∀ (n : ℕ), 0 < n → ↑n ≤ f ↑n
pn : ℕ
hpn : 0 < pn + 1 → f (x ^ (pn + 1)) ≤ f x ^ (pn + 1)
hn : 0 < pn + 1 + 1
hpn' : f (x ^ (pn + 1)) ≤ f x ^ (pn + 1)
⊢ f (x ^ (pn + 1) * x) ≤ f x ^ (pn + 1) * f x
Tactic:
have hxp : 0 < x := zero_lt_one.trans hx
Proof state after:
case succ.succ
f : ℚ → ℝ
x : ℚ
hx : 1 < x
H1 : ∀ (x y : ℚ), 0 < x → 0 < y → f (x * y) ≤ f x * f y
H4 : ∀ (n : ℕ), 0 < n → ↑n ≤ f ↑n
pn : ℕ
hpn : 0 < pn + 1 → f (x ^ (pn + 1)) ≤ f x ^ (pn + 1)
hn : 0 < pn + 1 + 1
hpn' : f (x ^ (pn + 1)) ≤ f x ^ (pn + 1)
hxp : 0 < x
⊢ f (x ^ (pn + 1) * x) ≤ f x ^ (pn + 1) * f x
Theorem: Imo2013P5.pow_f_le_f_pow
Proof state before:
case succ.succ
f : ℚ → ℝ
x : ℚ
hx : 1 < x
H1 : ∀ (x y : ℚ), 0 < x → 0 < y → f (x * y) ≤ f x * f y
H4 : ∀ (n : ℕ), 0 < n → ↑n ≤ f ↑n
pn : ℕ
hpn : 0 < pn + 1 → f (x ^ (pn + 1)) ≤ f x ^ (pn + 1)
hn : 0 < pn + 1 + 1
hpn' : f (x ^ (pn + 1)) ≤ f x ^ (pn + 1)
hxp : 0 < x
⊢ f (x ^ (pn + 1) * x) ≤ f x ^ (pn + 1) * f x
Tactic:
calc f ((x ^ (pn+1)) * x)
    ≤ f (x ^ (pn+1)) * f x := H1 (x ^ (pn+1)) x (pow_pos hxp (pn+1)) hxp
  _ ≤ (f x) ^ (pn+1) * f x := (mul_le_mul_right (f_pos_of_pos hxp H1 H4)).mpr hpn'
Proof state after:
no goals
Theorem: Imo2013P5.fixed_point_of_pos_nat_pow
Proof state before:
f : ℚ → ℝ
n : ℕ
hn : 0 < n
H1 : ∀ (x y : ℚ), 0 < x → 0 < y → f (x * y) ≤ f x * f y
H4 : ∀ (n : ℕ), 0 < n → ↑n ≤ f ↑n
H5 : ∀ (x : ℚ), 1 < x → ↑x ≤ f x
a : ℚ
ha1 : 1 < a
hae : f a = ↑a
⊢ f (a ^ n) = ↑a ^ n
Tactic:
have hh0 : (a : ℝ) ^ n ≤ f (a ^ n) := by
  exact_mod_cast H5 (a ^ n) (one_lt_pow ha1 hn.ne')
Proof state after:
f : ℚ → ℝ
n : ℕ
hn : 0 < n
H1 : ∀ (x y : ℚ), 0 < x → 0 < y → f (x * y) ≤ f x * f y
H4 : ∀ (n : ℕ), 0 < n → ↑n ≤ f ↑n
H5 : ∀ (x : ℚ), 1 < x → ↑x ≤ f x
a : ℚ
ha1 : 1 < a
hae : f a = ↑a
hh0 : ↑a ^ n ≤ f (a ^ n)
⊢ f (a ^ n) = ↑a ^ n
Theorem: Imo2013P5.fixed_point_of_pos_nat_pow
Proof state before:
f : ℚ → ℝ
n : ℕ
hn : 0 < n
H1 : ∀ (x y : ℚ), 0 < x → 0 < y → f (x * y) ≤ f x * f y
H4 : ∀ (n : ℕ), 0 < n → ↑n ≤ f ↑n
H5 : ∀ (x : ℚ), 1 < x → ↑x ≤ f x
a : ℚ
ha1 : 1 < a
hae : f a = ↑a
hh0 : ↑a ^ n ≤ f (a ^ n)
⊢ f (a ^ n) = ↑a ^ n
Tactic:
have hh1 := calc f (a^n) ≤ (f a)^n := pow_f_le_f_pow hn ha1 H1 H4
                 _ = (a : ℝ)^n     := by rw [←hae]
Proof state after:
f : ℚ → ℝ
n : ℕ
hn : 0 < n
H1 : ∀ (x y : ℚ), 0 < x → 0 < y → f (x * y) ≤ f x * f y
H4 : ∀ (n : ℕ), 0 < n → ↑n ≤ f ↑n
H5 : ∀ (x : ℚ), 1 < x → ↑x ≤ f x
a : ℚ
ha1 : 1 < a
hae : f a = ↑a
hh0 : ↑a ^ n ≤ f (a ^ n)
hh1 : f (a ^ n) ≤ ↑a ^ n
⊢ f (a ^ n) = ↑a ^ n
Theorem: Imo2013P5.fixed_point_of_pos_nat_pow
Proof state before:
f : ℚ → ℝ
n : ℕ
hn : 0 < n
H1 : ∀ (x y : ℚ), 0 < x → 0 < y → f (x * y) ≤ f x * f y
H4 : ∀ (n : ℕ), 0 < n → ↑n ≤ f ↑n
H5 : ∀ (x : ℚ), 1 < x → ↑x ≤ f x
a : ℚ
ha1 : 1 < a
hae : f a = ↑a
hh0 : ↑a ^ n ≤ f (a ^ n)
hh1 : f (a ^ n) ≤ ↑a ^ n
⊢ f (a ^ n) = ↑a ^ n
Tactic:
exact_mod_cast hh1.antisymm hh0
Proof state after:
no goals
Theorem: Imo2013P5.fixed_point_of_pos_nat_pow
Proof state before:
f : ℚ → ℝ
n : ℕ
hn : 0 < n
H1 : ∀ (x y : ℚ), 0 < x → 0 < y → f (x * y) ≤ f x * f y
H4 : ∀ (n : ℕ), 0 < n → ↑n ≤ f ↑n
H5 : ∀ (x : ℚ), 1 < x → ↑x ≤ f x
a : ℚ
ha1 : 1 < a
hae : f a = ↑a
⊢ ↑a ^ n ≤ f (a ^ n)
Tactic:
exact_mod_cast H5 (a ^ n) (one_lt_pow ha1 hn.ne')
Proof state after:
no goals
Theorem: Imo2013P5.fixed_point_of_pos_nat_pow
Proof state before:
f : ℚ → ℝ
n : ℕ
hn : 0 < n
H1 : ∀ (x y : ℚ), 0 < x → 0 < y → f (x * y) ≤ f x * f y
H4 : ∀ (n : ℕ), 0 < n → ↑n ≤ f ↑n
H5 : ∀ (x : ℚ), 1 < x → ↑x ≤ f x
a : ℚ
ha1 : 1 < a
hae : f a = ↑a
hh0 : ↑a ^ n ≤ f (a ^ n)
⊢ f a ^ n = ↑a ^ n
Tactic:
rw [←hae]
Proof state after:
no goals
Theorem: Imo2013P5.fixed_point_of_gt_1
Proof state before:
f : ℚ → ℝ
x : ℚ
hx : 1 < x
H1 : ∀ (x y : ℚ), 0 < x → 0 < y → f (x * y) ≤ f x * f y
H2 : ∀ (x y : ℚ), 0 < x → 0 < y → f x + f y ≤ f (x + y)
H4 : ∀ (n : ℕ), 0 < n → ↑n ≤ f ↑n
H5 : ∀ (x : ℚ), 1 < x → ↑x ≤ f x
a : ℚ
ha1 : 1 < a
hae : f a = ↑a
⊢ f x = ↑x
Tactic:
obtain ⟨N, hN⟩ := pow_unbounded_of_one_lt (1 + x) ha1
Proof state after:
case intro
f : ℚ → ℝ
x : ℚ
hx : 1 < x
H1 : ∀ (x y : ℚ), 0 < x → 0 < y → f (x * y) ≤ f x * f y
H2 : ∀ (x y : ℚ), 0 < x → 0 < y → f x + f y ≤ f (x + y)
H4 : ∀ (n : ℕ), 0 < n → ↑n ≤ f ↑n
H5 : ∀ (x : ℚ), 1 < x → ↑x ≤ f x
a : ℚ
ha1 : 1 < a
hae : f a = ↑a
N : ℕ
hN : 1 + x < a ^ N
⊢ f x = ↑x
Theorem: Imo2013P5.fixed_point_of_gt_1
Proof state before:
case intro
f : ℚ → ℝ
x : ℚ
hx : 1 < x
H1 : ∀ (x y : ℚ), 0 < x → 0 < y → f (x * y) ≤ f x * f y
H2 : ∀ (x y : ℚ), 0 < x → 0 < y → f x + f y ≤ f (x + y)
H4 : ∀ (n : ℕ), 0 < n → ↑n ≤ f ↑n
H5 : ∀ (x : ℚ), 1 < x → ↑x ≤ f x
a : ℚ
ha1 : 1 < a
hae : f a = ↑a
N : ℕ
hN : 1 + x < a ^ N
⊢ f x = ↑x
Tactic:
have h_big_enough : (1:ℚ) < a^N - x := lt_sub_iff_add_lt.mpr hN
Proof state after:
case intro
f : ℚ → ℝ
x : ℚ
hx : 1 < x
H1 : ∀ (x y : ℚ), 0 < x → 0 < y → f (x * y) ≤ f x * f y
H2 : ∀ (x y : ℚ), 0 < x → 0 < y → f x + f y ≤ f (x + y)
H4 : ∀ (n : ℕ), 0 < n → ↑n ≤ f ↑n
H5 : ∀ (x : ℚ), 1 < x → ↑x ≤ f x
a : ℚ
ha1 : 1 < a
hae : f a = ↑a
N : ℕ
hN : 1 + x < a ^ N
h_big_enough : 1 < a ^ N - x
⊢ f x = ↑x
Theorem: Imo2013P5.fixed_point_of_gt_1
Proof state before:
case intro
f : ℚ → ℝ
x : ℚ
hx : 1 < x
H1 : ∀ (x y : ℚ), 0 < x → 0 < y → f (x * y) ≤ f x * f y
H2 : ∀ (x y : ℚ), 0 < x → 0 < y → f x + f y ≤ f (x + y)
H4 : ∀ (n : ℕ), 0 < n → ↑n ≤ f ↑n
H5 : ∀ (x : ℚ), 1 < x → ↑x ≤ f x
a : ℚ
ha1 : 1 < a
hae : f a = ↑a
N : ℕ
hN : 1 + x < a ^ N
h_big_enough : 1 < a ^ N - x
⊢ f x = ↑x
Tactic:
have h1 := calc (x : ℝ) + ((a^N - x) : ℚ)
              ≤ f x + ((a^N - x) : ℚ) := add_le_add_right (H5 x hx) _
            _ ≤ f x + f (a^N - x)     := add_le_add_left (H5 _ h_big_enough) _
Proof state after:
case intro
f : ℚ → ℝ
x : ℚ
hx : 1 < x
H1 : ∀ (x y : ℚ), 0 < x → 0 < y → f (x * y) ≤ f x * f y
H2 : ∀ (x y : ℚ), 0 < x → 0 < y → f x + f y ≤ f (x + y)
H4 : ∀ (n : ℕ), 0 < n → ↑n ≤ f ↑n
H5 : ∀ (x : ℚ), 1 < x → ↑x ≤ f x
a : ℚ
ha1 : 1 < a
hae : f a = ↑a
N : ℕ
hN : 1 + x < a ^ N
h_big_enough : 1 < a ^ N - x
h1 : ↑x + ↑(a ^ N - x) ≤ f x + f (a ^ N - x)
⊢ f x = ↑x
Theorem: Imo2013P5.fixed_point_of_gt_1
Proof state before:
case intro
f : ℚ → ℝ
x : ℚ
hx : 1 < x
H1 : ∀ (x y : ℚ), 0 < x → 0 < y → f (x * y) ≤ f x * f y
H2 : ∀ (x y : ℚ), 0 < x → 0 < y → f x + f y ≤ f (x + y)
H4 : ∀ (n : ℕ), 0 < n → ↑n ≤ f ↑n
H5 : ∀ (x : ℚ), 1 < x → ↑x ≤ f x
a : ℚ
ha1 : 1 < a
hae : f a = ↑a
N : ℕ
hN : 1 + x < a ^ N
h_big_enough : 1 < a ^ N - x
h1 : ↑x + ↑(a ^ N - x) ≤ f x + f (a ^ N - x)
⊢ f x = ↑x
Tactic:
have hxp : 0 < x := zero_lt_one.trans hx
Proof state after:
case intro
f : ℚ → ℝ
x : ℚ
hx : 1 < x
H1 : ∀ (x y : ℚ), 0 < x → 0 < y → f (x * y) ≤ f x * f y
H2 : ∀ (x y : ℚ), 0 < x → 0 < y → f x + f y ≤ f (x + y)
H4 : ∀ (n : ℕ), 0 < n → ↑n ≤ f ↑n
H5 : ∀ (x : ℚ), 1 < x → ↑x ≤ f x
a : ℚ
ha1 : 1 < a
hae : f a = ↑a
N : ℕ
hN : 1 + x < a ^ N
h_big_enough : 1 < a ^ N - x
h1 : ↑x + ↑(a ^ N - x) ≤ f x + f (a ^ N - x)
hxp : 0 < x
⊢ f x = ↑x
Theorem: Imo2013P5.fixed_point_of_gt_1
Proof state before:
case intro
f : ℚ → ℝ
x : ℚ
hx : 1 < x
H1 : ∀ (x y : ℚ), 0 < x → 0 < y → f (x * y) ≤ f x * f y
H2 : ∀ (x y : ℚ), 0 < x → 0 < y → f x + f y ≤ f (x + y)
H4 : ∀ (n : ℕ), 0 < n → ↑n ≤ f ↑n
H5 : ∀ (x : ℚ), 1 < x → ↑x ≤ f x
a : ℚ
ha1 : 1 < a
hae : f a = ↑a
N : ℕ
hN : 1 + x < a ^ N
h_big_enough : 1 < a ^ N - x
h1 : ↑x + ↑(a ^ N - x) ≤ f x + f (a ^ N - x)
hxp : 0 < x
⊢ f x = ↑x
Tactic:
have hNp : 0 < N := by
  by_contra H; push_neg at H; rw [le_zero_iff.mp H] at hN; linarith
Proof state after:
case intro
f : ℚ → ℝ
x : ℚ
hx : 1 < x
H1 : ∀ (x y : ℚ), 0 < x → 0 < y → f (x * y) ≤ f x * f y
H2 : ∀ (x y : ℚ), 0 < x → 0 < y → f x + f y ≤ f (x + y)
H4 : ∀ (n : ℕ), 0 < n → ↑n ≤ f ↑n
H5 : ∀ (x : ℚ), 1 < x → ↑x ≤ f x
a : ℚ
ha1 : 1 < a
hae : f a = ↑a
N : ℕ
hN : 1 + x < a ^ N
h_big_enough : 1 < a ^ N - x
h1 : ↑x + ↑(a ^ N - x) ≤ f x + f (a ^ N - x)
hxp : 0 < x
hNp : 0 < N
⊢ f x = ↑x
Theorem: Imo2013P5.fixed_point_of_gt_1
Proof state before:
case intro
f : ℚ → ℝ
x : ℚ
hx : 1 < x
H1 : ∀ (x y : ℚ), 0 < x → 0 < y → f (x * y) ≤ f x * f y
H2 : ∀ (x y : ℚ), 0 < x → 0 < y → f x + f y ≤ f (x + y)
H4 : ∀ (n : ℕ), 0 < n → ↑n ≤ f ↑n
H5 : ∀ (x : ℚ), 1 < x → ↑x ≤ f x
a : ℚ
ha1 : 1 < a
hae : f a = ↑a
N : ℕ
hN : 1 + x < a ^ N
h_big_enough : 1 < a ^ N - x
h1 : ↑x + ↑(a ^ N - x) ≤ f x + f (a ^ N - x)
hxp : 0 < x
hNp : 0 < N
⊢ f x = ↑x
Tactic:
have h2 := calc f x + f (a^N - x)
              ≤ f (x + (a^N - x)) := H2 x (a^N - x) hxp (zero_lt_one.trans h_big_enough)
            _ = f (a^N)           := by ring_nf
            _ = (a^N : ℝ)         := fixed_point_of_pos_nat_pow hNp H1 H4 H5 ha1 hae
            _ = (x:ℝ) + ((a^N:ℝ) - (x:ℝ))     := by ring
Proof state after:
case intro
f : ℚ → ℝ
x : ℚ
hx : 1 < x
H1 : ∀ (x y : ℚ), 0 < x → 0 < y → f (x * y) ≤ f x * f y
H2 : ∀ (x y : ℚ), 0 < x → 0 < y → f x + f y ≤ f (x + y)
H4 : ∀ (n : ℕ), 0 < n → ↑n ≤ f ↑n
H5 : ∀ (x : ℚ), 1 < x → ↑x ≤ f x
a : ℚ
ha1 : 1 < a
hae : f a = ↑a
N : ℕ
hN : 1 + x < a ^ N
h_big_enough : 1 < a ^ N - x
h1 : ↑x + ↑(a ^ N - x) ≤ f x + f (a ^ N - x)
hxp : 0 < x
hNp : 0 < N
h2 : f x + f (a ^ N - x) ≤ ↑x + (↑a ^ N - ↑x)
⊢ f x = ↑x
Theorem: Imo2013P5.fixed_point_of_gt_1
Proof state before:
case intro
f : ℚ → ℝ
x : ℚ
hx : 1 < x
H1 : ∀ (x y : ℚ), 0 < x → 0 < y → f (x * y) ≤ f x * f y
H2 : ∀ (x y : ℚ), 0 < x → 0 < y → f x + f y ≤ f (x + y)
H4 : ∀ (n : ℕ), 0 < n → ↑n ≤ f ↑n
H5 : ∀ (x : ℚ), 1 < x → ↑x ≤ f x
a : ℚ
ha1 : 1 < a
hae : f a = ↑a
N : ℕ
hN : 1 + x < a ^ N
h_big_enough : 1 < a ^ N - x
h1 : ↑x + ↑(a ^ N - x) ≤ f x + f (a ^ N - x)
hxp : 0 < x
hNp : 0 < N
h2 : f x + f (a ^ N - x) ≤ ↑x + (↑a ^ N - ↑x)
⊢ f x = ↑x
Tactic:
have heq := h1.antisymm (by exact_mod_cast h2)
Proof state after:
case intro
f : ℚ → ℝ
x : ℚ
hx : 1 < x
H1 : ∀ (x y : ℚ), 0 < x → 0 < y → f (x * y) ≤ f x * f y
H2 : ∀ (x y : ℚ), 0 < x → 0 < y → f x + f y ≤ f (x + y)
H4 : ∀ (n : ℕ), 0 < n → ↑n ≤ f ↑n
H5 : ∀ (x : ℚ), 1 < x → ↑x ≤ f x
a : ℚ
ha1 : 1 < a
hae : f a = ↑a
N : ℕ
hN : 1 + x < a ^ N
h_big_enough : 1 < a ^ N - x
h1 : ↑x + ↑(a ^ N - x) ≤ f x + f (a ^ N - x)
hxp : 0 < x
hNp : 0 < N
h2 : f x + f (a ^ N - x) ≤ ↑x + (↑a ^ N - ↑x)
heq : ↑x + ↑(a ^ N - x) = f x + f (a ^ N - x)
⊢ f x = ↑x
Theorem: Imo2013P5.fixed_point_of_gt_1
Proof state before:
case intro
f : ℚ → ℝ
x : ℚ
hx : 1 < x
H1 : ∀ (x y : ℚ), 0 < x → 0 < y → f (x * y) ≤ f x * f y
H2 : ∀ (x y : ℚ), 0 < x → 0 < y → f x + f y ≤ f (x + y)
H4 : ∀ (n : ℕ), 0 < n → ↑n ≤ f ↑n
H5 : ∀ (x : ℚ), 1 < x → ↑x ≤ f x
a : ℚ
ha1 : 1 < a
hae : f a = ↑a
N : ℕ
hN : 1 + x < a ^ N
h_big_enough : 1 < a ^ N - x
h1 : ↑x + ↑(a ^ N - x) ≤ f x + f (a ^ N - x)
hxp : 0 < x
hNp : 0 < N
h2 : f x + f (a ^ N - x) ≤ ↑x + (↑a ^ N - ↑x)
heq : ↑x + ↑(a ^ N - x) = f x + f (a ^ N - x)
⊢ f x = ↑x
Tactic:
linarith [H5 x hx, H5 _ h_big_enough]
Proof state after:
no goals
Theorem: Imo2013P5.fixed_point_of_gt_1
Proof state before:
f : ℚ → ℝ
x : ℚ
hx : 1 < x
H1 : ∀ (x y : ℚ), 0 < x → 0 < y → f (x * y) ≤ f x * f y
H2 : ∀ (x y : ℚ), 0 < x → 0 < y → f x + f y ≤ f (x + y)
H4 : ∀ (n : ℕ), 0 < n → ↑n ≤ f ↑n
H5 : ∀ (x : ℚ), 1 < x → ↑x ≤ f x
a : ℚ
ha1 : 1 < a
hae : f a = ↑a
N : ℕ
hN : 1 + x < a ^ N
h_big_enough : 1 < a ^ N - x
h1 : ↑x + ↑(a ^ N - x) ≤ f x + f (a ^ N - x)
hxp : 0 < x
⊢ 0 < N
Tactic:
by_contra H
Proof state after:
f : ℚ → ℝ
x : ℚ
hx : 1 < x
H1 : ∀ (x y : ℚ), 0 < x → 0 < y → f (x * y) ≤ f x * f y
H2 : ∀ (x y : ℚ), 0 < x → 0 < y → f x + f y ≤ f (x + y)
H4 : ∀ (n : ℕ), 0 < n → ↑n ≤ f ↑n
H5 : ∀ (x : ℚ), 1 < x → ↑x ≤ f x
a : ℚ
ha1 : 1 < a
hae : f a = ↑a
N : ℕ
hN : 1 + x < a ^ N
h_big_enough : 1 < a ^ N - x
h1 : ↑x + ↑(a ^ N - x) ≤ f x + f (a ^ N - x)
hxp : 0 < x
H : ¬0 < N
⊢ False