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

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

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

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

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

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