Theorem: IMOSL.IMO2015A1.final_solution (IMOSLLean4/IMO2015/A1/A1.lean)

State before:
F : Type u_1
inst✝ : LinearOrderedField F
a : ℕ → F
h : ∀ (k : ℕ), 0 < a k
h0 : ∀ (k : ℕ), ↑k.succ * a k / (a k ^ 2 + ↑k) ≤ a k.succ
⊢ ∀ (n : ℕ), 2 ≤ n → ↑n ≤ (range n).sum a
Tactic:
replace h0 (k : ℕ) : (k.succ : F) / a k.succ ≤ a k + k / a k := by
  rw [add_div' _ _ _ (h k).ne.symm, div_le_div_iff (h _) (h k), ← sq]
  exact (div_le_iff' <| add_pos_of_pos_of_nonneg
    (pow_pos (h k) 2) k.cast_nonneg).mp (h0 k)
State after:
F : Type u_1
inst✝ : LinearOrderedField F
a : ℕ → F
h : ∀ (k : ℕ), 0 < a k
h0 : ∀ (k : ℕ), ↑k.succ / a k.succ ≤ a k + ↑k / a k
⊢ ∀ (n : ℕ), 2 ≤ n → ↑n ≤ (range n).sum a

State before:
F : Type u_1
inst✝ : LinearOrderedField F
a : ℕ → F
h : ∀ (k : ℕ), 0 < a k
h0 : ∀ (k : ℕ), ↑k.succ / a k.succ ≤ a k + ↑k / a k
⊢ ∀ (n : ℕ), 2 ≤ n → ↑n ≤ (range n).sum a
Tactic:
refine Nat.le_induction ?_ ?_
State after:
case refine_1
F : Type u_1
inst✝ : LinearOrderedField F
a : ℕ → F
h : ∀ (k : ℕ), 0 < a k
h0 : ∀ (k : ℕ), ↑k.succ / a k.succ ≤ a k + ↑k / a k
⊢ ↑2 ≤ (range 2).sum a

case refine_2
F : Type u_1
inst✝ : LinearOrderedField F
a : ℕ → F
h : ∀ (k : ℕ), 0 < a k
h0 : ∀ (k : ℕ), ↑k.succ / a k.succ ≤ a k + ↑k / a k
⊢ ∀ (n : ℕ), 2 ≤ n → ↑n ≤ (range n).sum a → ↑(n + 1) ≤ (range (n + 1)).sum a

State before:
F : Type u_1
inst✝ : LinearOrderedField F
a : ℕ → F
h : ∀ (k : ℕ), 0 < a k
h0 : ∀ (k : ℕ), ↑k.succ * a k / (a k ^ 2 + ↑k) ≤ a k.succ
k : ℕ
⊢ ↑k.succ / a k.succ ≤ a k + ↑k / a k
Tactic:
rw [add_div' _ _ _ (h k).ne.symm, div_le_div_iff (h _) (h k), ← sq]
State after:
F : Type u_1
inst✝ : LinearOrderedField F
a : ℕ → F
h : ∀ (k : ℕ), 0 < a k
h0 : ∀ (k : ℕ), ↑k.succ * a k / (a k ^ 2 + ↑k) ≤ a k.succ
k : ℕ
⊢ ↑k.succ * a k ≤ (a k ^ 2 + ↑k) * a k.succ

State before:
F : Type u_1
inst✝ : LinearOrderedField F
a : ℕ → F
h : ∀ (k : ℕ), 0 < a k
h0 : ∀ (k : ℕ), ↑k.succ * a k / (a k ^ 2 + ↑k) ≤ a k.succ
k : ℕ
⊢ ↑k.succ * a k ≤ (a k ^ 2 + ↑k) * a k.succ
Tactic:
exact (div_le_iff' <| add_pos_of_pos_of_nonneg
  (pow_pos (h k) 2) k.cast_nonneg).mp (h0 k)
State after:
no goals

State before:
case refine_1
F : Type u_1
inst✝ : LinearOrderedField F
a : ℕ → F
h : ∀ (k : ℕ), 0 < a k
h0 : ∀ (k : ℕ), ↑k.succ / a k.succ ≤ a k + ↑k / a k
⊢ ↑2 ≤ (range 2).sum a
Tactic:
rw [Nat.cast_two, sum_range_succ, sum_range_one]
State after:
case refine_1
F : Type u_1
inst✝ : LinearOrderedField F
a : ℕ → F
h : ∀ (k : ℕ), 0 < a k
h0 : ∀ (k : ℕ), ↑k.succ / a k.succ ≤ a k + ↑k / a k
⊢ 2 ≤ a 0 + a 1

State before:
case refine_1
F : Type u_1
inst✝ : LinearOrderedField F
a : ℕ → F
h : ∀ (k : ℕ), 0 < a k
h0 : ∀ (k : ℕ), ↑k.succ / a k.succ ≤ a k + ↑k / a k
⊢ 2 ≤ a 0 + a 1
Tactic:
specialize h0 0
State after:
case refine_1
F : Type u_1
inst✝ : LinearOrderedField F
a : ℕ → F
h : ∀ (k : ℕ), 0 < a k
h0 : ↑(Nat.succ 0) / a (Nat.succ 0) ≤ a 0 + ↑0 / a 0
⊢ 2 ≤ a 0 + a 1

State before:
case refine_1
F : Type u_1
inst✝ : LinearOrderedField F
a : ℕ → F
h : ∀ (k : ℕ), 0 < a k
h0 : ↑(Nat.succ 0) / a (Nat.succ 0) ≤ a 0 + ↑0 / a 0
⊢ 2 ≤ a 0 + a 1
Tactic:
rw [Nat.cast_one, Nat.cast_zero, zero_div, add_zero] at h0
State after:
case refine_1
F : Type u_1
inst✝ : LinearOrderedField F
a : ℕ → F
h : ∀ (k : ℕ), 0 < a k
h0 : 1 / a (Nat.succ 0) ≤ a 0
⊢ 2 ≤ a 0 + a 1

State before:
case refine_1
F : Type u_1
inst✝ : LinearOrderedField F
a : ℕ → F
h : ∀ (k : ℕ), 0 < a k
h0 : 1 / a (Nat.succ 0) ≤ a 0
⊢ 2 ≤ a 0 + a 1
Tactic:
apply (add_le_add_right h0 _).trans'
State after:
case refine_1
F : Type u_1
inst✝ : LinearOrderedField F
a : ℕ → F
h : ∀ (k : ℕ), 0 < a k
h0 : 1 / a (Nat.succ 0) ≤ a 0
⊢ 2 ≤ 1 / a (Nat.succ 0) + a 1

State before:
case refine_1
F : Type u_1
inst✝ : LinearOrderedField F
a : ℕ → F
h : ∀ (k : ℕ), 0 < a k
h0 : 1 / a (Nat.succ 0) ≤ a 0
⊢ 2 ≤ 1 / a (Nat.succ 0) + a 1
Tactic:
rw [div_add' _ _ _ (h 1).ne.symm, le_div_iff (h 1), ← sq]
State after:
case refine_1
F : Type u_1
inst✝ : LinearOrderedField F
a : ℕ → F
h : ∀ (k : ℕ), 0 < a k
h0 : 1 / a (Nat.succ 0) ≤ a 0
⊢ 2 * a 1 ≤ 1 + a 1 ^ 2

State before:
case refine_1
F : Type u_1
inst✝ : LinearOrderedField F
a : ℕ → F
h : ∀ (k : ℕ), 0 < a k
h0 : 1 / a (Nat.succ 0) ≤ a 0
⊢ 2 * a 1 ≤ 1 + a 1 ^ 2
Tactic:
have h1 := two_mul_le_add_sq 1 (a 1)
State after:
case refine_1
F : Type u_1
inst✝ : LinearOrderedField F
a : ℕ → F
h : ∀ (k : ℕ), 0 < a k
h0 : 1 / a (Nat.succ 0) ≤ a 0
h1 : 2 * 1 * a 1 ≤ 1 ^ 2 + a 1 ^ 2
⊢ 2 * a 1 ≤ 1 + a 1 ^ 2

State before:
case refine_1
F : Type u_1
inst✝ : LinearOrderedField F
a : ℕ → F
h : ∀ (k : ℕ), 0 < a k
h0 : 1 / a (Nat.succ 0) ≤ a 0
h1 : 2 * 1 * a 1 ≤ 1 ^ 2 + a 1 ^ 2
⊢ 2 * a 1 ≤ 1 + a 1 ^ 2
Tactic:
rwa [mul_one, one_pow] at h1
State after:
no goals

State before:
case refine_2
F : Type u_1
inst✝ : LinearOrderedField F
a : ℕ → F
h : ∀ (k : ℕ), 0 < a k
h0 : ∀ (k : ℕ), ↑k.succ / a k.succ ≤ a k + ↑k / a k
⊢ ∀ (n : ℕ), 2 ≤ n → ↑n ≤ (range n).sum a → ↑(n + 1) ≤ (range (n + 1)).sum a
Tactic:
intro n h1 h2
State after:
case refine_2
F : Type u_1
inst✝ : LinearOrderedField F
a : ℕ → F
h : ∀ (k : ℕ), 0 < a k
h0 : ∀ (k : ℕ), ↑k.succ / a k.succ ≤ a k + ↑k / a k
n : ℕ
h1 : 2 ≤ n
h2 : ↑n ≤ (range n).sum a
⊢ ↑(n + 1) ≤ (range (n + 1)).sum a

State before:
case refine_2
F : Type u_1
inst✝ : LinearOrderedField F
a : ℕ → F
h : ∀ (k : ℕ), 0 < a k
h0 : ∀ (k : ℕ), ↑k.succ / a k.succ ≤ a k + ↑k / a k
n : ℕ
h1 : 2 ≤ n
h2 : ↑n ≤ (range n).sum a
⊢ ↑(n + 1) ≤ (range (n + 1)).sum a
Tactic:
rw [sum_range_succ, Nat.cast_succ]
State after:
case refine_2
F : Type u_1
inst✝ : LinearOrderedField F
a : ℕ → F
h : ∀ (k : ℕ), 0 < a k
h0 : ∀ (k : ℕ), ↑k.succ / a k.succ ≤ a k + ↑k / a k
n : ℕ
h1 : 2 ≤ n
h2 : ↑n ≤ (range n).sum a
⊢ ↑n + 1 ≤ ∑ x ∈ range n, a x + a n

State before:
case refine_2
F : Type u_1
inst✝ : LinearOrderedField F
a : ℕ → F
h : ∀ (k : ℕ), 0 < a k
h0 : ∀ (k : ℕ), ↑k.succ / a k.succ ≤ a k + ↑k / a k
n : ℕ
h1 : 2 ≤ n
h2 : ↑n ≤ (range n).sum a
⊢ ↑n + 1 ≤ ∑ x ∈ range n, a x + a n
Tactic:
rcases le_total 1 (a n) with h3 | h3
State after:
case refine_2.inl
F : Type u_1
inst✝ : LinearOrderedField F
a : ℕ → F
h : ∀ (k : ℕ), 0 < a k
h0 : ∀ (k : ℕ), ↑k.succ / a k.succ ≤ a k + ↑k / a k
n : ℕ
h1 : 2 ≤ n
h2 : ↑n ≤ (range n).sum a
h3 : 1 ≤ a n
⊢ ↑n + 1 ≤ ∑ x ∈ range n, a x + a n

case refine_2.inr
F : Type u_1
inst✝ : LinearOrderedField F
a : ℕ → F
h : ∀ (k : ℕ), 0 < a k
h0 : ∀ (k : ℕ), ↑k.succ / a k.succ ≤ a k + ↑k / a k
n : ℕ
h1 : 2 ≤ n
h2 : ↑n ≤ (range n).sum a
h3 : a n ≤ 1
⊢ ↑n + 1 ≤ ∑ x ∈ range n, a x + a n

State before:
case refine_2.inr
F : Type u_1
inst✝ : LinearOrderedField F
a : ℕ → F
h : ∀ (k : ℕ), 0 < a k
h0 : ∀ (k : ℕ), ↑k.succ / a k.succ ≤ a k + ↑k / a k
n : ℕ
h1 : 2 ≤ n
h2 : ↑n ≤ (range n).sum a
h3 : a n ≤ 1
⊢ ↑n + 1 ≤ ∑ x ∈ range n, a x + a n
Tactic:
refine le_trans ?_ (add_le_add_right (?_ : (n : F) / a n ≤ _) _)
State after:
case refine_2.inr.refine_1
F : Type u_1
inst✝ : LinearOrderedField F
a : ℕ → F
h : ∀ (k : ℕ), 0 < a k
h0 : ∀ (k : ℕ), ↑k.succ / a k.succ ≤ a k + ↑k / a k
n : ℕ
h1 : 2 ≤ n
h2 : ↑n ≤ (range n).sum a
h3 : a n ≤ 1
⊢ ↑n + 1 ≤ ↑n / a n + a n

case refine_2.inr.refine_2
F : Type u_1
inst✝ : LinearOrderedField F
a : ℕ → F
h : ∀ (k : ℕ), 0 < a k
h0 : ∀ (k : ℕ), ↑k.succ / a k.succ ≤ a k + ↑k / a k
n : ℕ
h1 : 2 ≤ n
h2 : ↑n ≤ (range n).sum a
h3 : a n ≤ 1
⊢ ↑n / a n ≤ ∑ x ∈ range n, a x

State before:
case refine_2.inr.refine_1
F : Type u_1
inst✝ : LinearOrderedField F
a : ℕ → F
h : ∀ (k : ℕ), 0 < a k
h0 : ∀ (k : ℕ), ↑k.succ / a k.succ ≤ a k + ↑k / a k
n : ℕ
h1 : 2 ≤ n
h2 : ↑n ≤ (range n).sum a
h3 : a n ≤ 1
⊢ ↑n + 1 ≤ ↑n / a n + a n

case refine_2.inr.refine_2
F : Type u_1
inst✝ : LinearOrderedField F
a : ℕ → F
h : ∀ (k : ℕ), 0 < a k
h0 : ∀ (k : ℕ), ↑k.succ / a k.succ ≤ a k + ↑k / a k
n : ℕ
h1 : 2 ≤ n
h2 : ↑n ≤ (range n).sum a
h3 : a n ≤ 1
⊢ ↑n / a n ≤ ∑ x ∈ range n, a x
Tactic:
rw [div_add' _ _ _ (h n).ne.symm, le_div_iff (h n), add_one_mul (α := F),
  ← sub_le_iff_le_add, add_sub_assoc, ← mul_one_sub,
  ← le_sub_iff_add_le', ← mul_one_sub, ← sub_nonneg, ← sub_mul]
State after:
case refine_2.inr.refine_1
F : Type u_1
inst✝ : LinearOrderedField F
a : ℕ → F
h : ∀ (k : ℕ), 0 < a k
h0 : ∀ (k : ℕ), ↑k.succ / a k.succ ≤ a k + ↑k / a k
n : ℕ
h1 : 2 ≤ n
h2 : ↑n ≤ (range n).sum a
h3 : a n ≤ 1
⊢ 0 ≤ (↑n - a n) * (1 - a n)

case refine_2.inr.refine_2
F : Type u_1
inst✝ : LinearOrderedField F
a : ℕ → F
h : ∀ (k : ℕ), 0 < a k
h0 : ∀ (k : ℕ), ↑k.succ / a k.succ ≤ a k + ↑k / a k
n : ℕ
h1 : 2 ≤ n
h2 : ↑n ≤ (range n).sum a
h3 : a n ≤ 1
⊢ ↑n / a n ≤ ∑ x ∈ range n, a x

State before:
case refine_2.inr.refine_1
F : Type u_1
inst✝ : LinearOrderedField F
a : ℕ → F
h : ∀ (k : ℕ), 0 < a k
h0 : ∀ (k : ℕ), ↑k.succ / a k.succ ≤ a k + ↑k / a k
n : ℕ
h1 : 2 ≤ n
h2 : ↑n ≤ (range n).sum a
h3 : a n ≤ 1
⊢ 0 ≤ (↑n - a n) * (1 - a n)

case refine_2.inr.refine_2
F : Type u_1
inst✝ : LinearOrderedField F
a : ℕ → F
h : ∀ (k : ℕ), 0 < a k
h0 : ∀ (k : ℕ), ↑k.succ / a k.succ ≤ a k + ↑k / a k
n : ℕ
h1 : 2 ≤ n
h2 : ↑n ≤ (range n).sum a
h3 : a n ≤ 1
⊢ ↑n / a n ≤ ∑ x ∈ range n, a x
Tactic:
refine mul_nonneg (sub_nonneg.mpr (h3.trans ?_)) (sub_nonneg.mpr h3)
State after:
case refine_2.inr.refine_1
F : Type u_1
inst✝ : LinearOrderedField F
a : ℕ → F
h : ∀ (k : ℕ), 0 < a k
h0 : ∀ (k : ℕ), ↑k.succ / a k.succ ≤ a k + ↑k / a k
n : ℕ
h1 : 2 ≤ n
h2 : ↑n ≤ (range n).sum a
h3 : a n ≤ 1
⊢ 1 ≤ ↑n

case refine_2.inr.refine_2
F : Type u_1
inst✝ : LinearOrderedField F
a : ℕ → F
h : ∀ (k : ℕ), 0 < a k
h0 : ∀ (k : ℕ), ↑k.succ / a k.succ ≤ a k + ↑k / a k
n : ℕ
h1 : 2 ≤ n
h2 : ↑n ≤ (range n).sum a
h3 : a n ≤ 1
⊢ ↑n / a n ≤ ∑ x ∈ range n, a x

State before:
case refine_2.inr.refine_1
F : Type u_1
inst✝ : LinearOrderedField F
a : ℕ → F
h : ∀ (k : ℕ), 0 < a k
h0 : ∀ (k : ℕ), ↑k.succ / a k.succ ≤ a k + ↑k / a k
n : ℕ
h1 : 2 ≤ n
h2 : ↑n ≤ (range n).sum a
h3 : a n ≤ 1
⊢ 1 ≤ ↑n

case refine_2.inr.refine_2
F : Type u_1
inst✝ : LinearOrderedField F
a : ℕ → F
h : ∀ (k : ℕ), 0 < a k
h0 : ∀ (k : ℕ), ↑k.succ / a k.succ ≤ a k + ↑k / a k
n : ℕ
h1 : 2 ≤ n
h2 : ↑n ≤ (range n).sum a
h3 : a n ≤ 1
⊢ ↑n / a n ≤ ∑ x ∈ range n, a x
Tactic:
rw [Nat.one_le_cast]
State after:
case refine_2.inr.refine_1
F : Type u_1
inst✝ : LinearOrderedField F
a : ℕ → F
h : ∀ (k : ℕ), 0 < a k
h0 : ∀ (k : ℕ), ↑k.succ / a k.succ ≤ a k + ↑k / a k
n : ℕ
h1 : 2 ≤ n
h2 : ↑n ≤ (range n).sum a
h3 : a n ≤ 1
⊢ 1 ≤ n

case refine_2.inr.refine_2
F : Type u_1
inst✝ : LinearOrderedField F
a : ℕ → F
h : ∀ (k : ℕ), 0 < a k
h0 : ∀ (k : ℕ), ↑k.succ / a k.succ ≤ a k + ↑k / a k
n : ℕ
h1 : 2 ≤ n
h2 : ↑n ≤ (range n).sum a
h3 : a n ≤ 1
⊢ ↑n / a n ≤ ∑ x ∈ range n, a x

State before:
case refine_2.inr.refine_1
F : Type u_1
inst✝ : LinearOrderedField F
a : ℕ → F
h : ∀ (k : ℕ), 0 < a k
h0 : ∀ (k : ℕ), ↑k.succ / a k.succ ≤ a k + ↑k / a k
n : ℕ
h1 : 2 ≤ n
h2 : ↑n ≤ (range n).sum a
h3 : a n ≤ 1
⊢ 1 ≤ n

case refine_2.inr.refine_2
F : Type u_1
inst✝ : LinearOrderedField F
a : ℕ → F
h : ∀ (k : ℕ), 0 < a k
h0 : ∀ (k : ℕ), ↑k.succ / a k.succ ≤ a k + ↑k / a k
n : ℕ
h1 : 2 ≤ n
h2 : ↑n ≤ (range n).sum a
h3 : a n ≤ 1
⊢ ↑n / a n ≤ ∑ x ∈ range n, a x
Tactic:
exact one_le_two.trans h1
State after:
case refine_2.inr.refine_2
F : Type u_1
inst✝ : LinearOrderedField F
a : ℕ → F
h : ∀ (k : ℕ), 0 < a k
h0 : ∀ (k : ℕ), ↑k.succ / a k.succ ≤ a k + ↑k / a k
n : ℕ
h1 : 2 ≤ n
h2 : ↑n ≤ (range n).sum a
h3 : a n ≤ 1
⊢ ↑n / a n ≤ ∑ x ∈ range n, a x

State before:
case refine_2.inr.refine_2
F : Type u_1
inst✝ : LinearOrderedField F
a : ℕ → F
h : ∀ (k : ℕ), 0 < a k
h0 : ∀ (k : ℕ), ↑k.succ / a k.succ ≤ a k + ↑k / a k
n : ℕ
h1 : 2 ≤ n
h2 : ↑n ≤ (range n).sum a
h3 : a n ≤ 1
⊢ ↑n / a n ≤ ∑ x ∈ range n, a x
Tactic:
clear h1 h2 h3
State after:
case refine_2.inr.refine_2
F : Type u_1
inst✝ : LinearOrderedField F
a : ℕ → F
h : ∀ (k : ℕ), 0 < a k
h0 : ∀ (k : ℕ), ↑k.succ / a k.succ ≤ a k + ↑k / a k
n : ℕ
⊢ ↑n / a n ≤ ∑ x ∈ range n, a x

State before:
case refine_2.inr.refine_2
F : Type u_1
inst✝ : LinearOrderedField F
a : ℕ → F
h : ∀ (k : ℕ), 0 < a k
h0 : ∀ (k : ℕ), ↑k.succ / a k.succ ≤ a k + ↑k / a k
n : ℕ
⊢ ↑n / a n ≤ ∑ x ∈ range n, a x
Tactic:
induction' n with n n_ih
State after:
case refine_2.inr.refine_2.zero
F : Type u_1
inst✝ : LinearOrderedField F
a : ℕ → F
h : ∀ (k : ℕ), 0 < a k
h0 : ∀ (k : ℕ), ↑k.succ / a k.succ ≤ a k + ↑k / a k
⊢ ↑0 / a 0 ≤ ∑ x ∈ range 0, a x

case refine_2.inr.refine_2.succ
F : Type u_1
inst✝ : LinearOrderedField F
a : ℕ → F
h : ∀ (k : ℕ), 0 < a k
h0 : ∀ (k : ℕ), ↑k.succ / a k.succ ≤ a k + ↑k / a k
n : ℕ
n_ih : ↑n / a n ≤ ∑ x ∈ range n, a x
⊢ ↑(n + 1) / a (n + 1) ≤ ∑ x ∈ range (n + 1), a x

State before:
case refine_2.inr.refine_2.zero
F : Type u_1
inst✝ : LinearOrderedField F
a : ℕ → F
h : ∀ (k : ℕ), 0 < a k
h0 : ∀ (k : ℕ), ↑k.succ / a k.succ ≤ a k + ↑k / a k
⊢ ↑0 / a 0 ≤ ∑ x ∈ range 0, a x

case refine_2.inr.refine_2.succ
F : Type u_1
inst✝ : LinearOrderedField F
a : ℕ → F
h : ∀ (k : ℕ), 0 < a k
h0 : ∀ (k : ℕ), ↑k.succ / a k.succ ≤ a k + ↑k / a k
n : ℕ
n_ih : ↑n / a n ≤ ∑ x ∈ range n, a x
⊢ ↑(n + 1) / a (n + 1) ≤ ∑ x ∈ range (n + 1), a x
Tactic:
rw [Nat.cast_zero, sum_range_zero, zero_div]
State after:
case refine_2.inr.refine_2.succ
F : Type u_1
inst✝ : LinearOrderedField F
a : ℕ → F
h : ∀ (k : ℕ), 0 < a k
h0 : ∀ (k : ℕ), ↑k.succ / a k.succ ≤ a k + ↑k / a k
n : ℕ
n_ih : ↑n / a n ≤ ∑ x ∈ range n, a x
⊢ ↑(n + 1) / a (n + 1) ≤ ∑ x ∈ range (n + 1), a x

State before:
case refine_2.inr.refine_2.succ
F : Type u_1
inst✝ : LinearOrderedField F
a : ℕ → F
h : ∀ (k : ℕ), 0 < a k
h0 : ∀ (k : ℕ), ↑k.succ / a k.succ ≤ a k + ↑k / a k
n : ℕ
n_ih : ↑n / a n ≤ ∑ x ∈ range n, a x
⊢ ↑(n + 1) / a (n + 1) ≤ ∑ x ∈ range (n + 1), a x
Tactic:
rw [sum_range_succ, add_comm _ (a n)]
State after:
case refine_2.inr.refine_2.succ
F : Type u_1
inst✝ : LinearOrderedField F
a : ℕ → F
h : ∀ (k : ℕ), 0 < a k
h0 : ∀ (k : ℕ), ↑k.succ / a k.succ ≤ a k + ↑k / a k
n : ℕ
n_ih : ↑n / a n ≤ ∑ x ∈ range n, a x
⊢ ↑(n + 1) / a (n + 1) ≤ a n + ∑ x ∈ range n, a x

State before:
case refine_2.inr.refine_2.succ
F : Type u_1
inst✝ : LinearOrderedField F
a : ℕ → F
h : ∀ (k : ℕ), 0 < a k
h0 : ∀ (k : ℕ), ↑k.succ / a k.succ ≤ a k + ↑k / a k
n : ℕ
n_ih : ↑n / a n ≤ ∑ x ∈ range n, a x
⊢ ↑(n + 1) / a (n + 1) ≤ a n + ∑ x ∈ range n, a x
Tactic:
refine (h0 n).trans (add_le_add_left n_ih (a n))
State after:
no goals

State before:
case refine_2.inl
F : Type u_1
inst✝ : LinearOrderedField F
a : ℕ → F
h : ∀ (k : ℕ), 0 < a k
h0 : ∀ (k : ℕ), ↑k.succ / a k.succ ≤ a k + ↑k / a k
n : ℕ
h1 : 2 ≤ n
h2 : ↑n ≤ (range n).sum a
h3 : 1 ≤ a n
⊢ ↑n + 1 ≤ ∑ x ∈ range n, a x + a n
Tactic:
exact add_le_add h2 h3
State after:
no goals