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

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

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

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

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

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

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

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

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

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