Theorem: Imo2013P5.pow_f_le_f_pow (Compfiles/Imo2013P5.lean)

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'
State after:
no goals

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
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

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
State after:
no goals

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'
State after:
no goals

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]
State after:
no goals

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
State after:
no goals

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
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)

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)]
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

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
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

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'
State after:
no goals