internlm/Lean-Github huggingface dataset:
Theorem: IMOSL.Extra.Infinitesimal.FloorRing_mul_right
Proof state before:
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
ε : R
hε : Infinitesimal ε
r : R
k : ℕ
⊢ k • |ε * r| < 1
Tactic:
apply (hε (k * ⌈|r|⌉.natAbs)).trans_le'
Proof state after:
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
ε : R
hε : Infinitesimal ε
r : R
k : ℕ
⊢ k • |ε * r| ≤ (k * ⌈|r|⌉.natAbs) • |ε|
Theorem: IMOSL.Extra.Infinitesimal.FloorRing_mul_right
Proof state before:
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
ε : R
hε : Infinitesimal ε
r : R
k : ℕ
⊢ k • |ε * r| ≤ (k * ⌈|r|⌉.natAbs) • |ε|
Tactic:
rw [abs_mul, mul_nsmul', nsmul_eq_mul' |ε|]
Proof state after:
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
ε : R
hε : Infinitesimal ε
r : R
k : ℕ
⊢ k • (|ε| * |r|) ≤ k • (|ε| * ↑⌈|r|⌉.natAbs)
Theorem: IMOSL.Extra.Infinitesimal.FloorRing_mul_right
Proof state before:
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
ε : R
hε : Infinitesimal ε
r : R
k : ℕ
⊢ k • (|ε| * |r|) ≤ k • (|ε| * ↑⌈|r|⌉.natAbs)
Tactic:
refine nsmul_le_nsmul_right (mul_le_mul_of_nonneg_left ?_ (abs_nonneg ε)) k
Proof state after:
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
ε : R
hε : Infinitesimal ε
r : R
k : ℕ
⊢ |r| ≤ ↑⌈|r|⌉.natAbs
Theorem: IMOSL.Extra.Infinitesimal.FloorRing_mul_right
Proof state before:
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
ε : R
hε : Infinitesimal ε
r : R
k : ℕ
⊢ |r| ≤ ↑⌈|r|⌉.natAbs
Tactic:
rw [← Int.cast_natCast ⌈|r|⌉.natAbs, ← Int.ceil_le]
Proof state after:
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
ε : R
hε : Infinitesimal ε
r : R
k : ℕ
⊢ ⌈|r|⌉ ≤ ↑⌈|r|⌉.natAbs
Theorem: IMOSL.Extra.Infinitesimal.FloorRing_mul_right
Proof state before:
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
ε : R
hε : Infinitesimal ε
r : R
k : ℕ
⊢ ⌈|r|⌉ ≤ ↑⌈|r|⌉.natAbs
Tactic:
exact Int.le_natAbs
Proof state after:
no goals
Theorem: IMOSL.Extra.Infinitesimal.FloorRing_iff_mul_left₁
Proof state before:
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
ε : R
h : ∀ (r : R), r * ε < 1
k : ℕ
⊢ k • |ε| < 1
Tactic:
rcases le_total 0 ε with h0 | h0
Proof state after:
case inl
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
ε : R
h : ∀ (r : R), r * ε < 1
k : ℕ
h0 : 0 ≤ ε
⊢ k • |ε| < 1

case inr
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
ε : R
h : ∀ (r : R), r * ε < 1
k : ℕ
h0 : ε ≤ 0
⊢ k • |ε| < 1
Theorem: IMOSL.Extra.Infinitesimal.FloorRing_iff_mul_left₁
Proof state before:
case inl
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
ε : R
h : ∀ (r : R), r * ε < 1
k : ℕ
h0 : 0 ≤ ε
⊢ k • |ε| < 1
Tactic:
rw [abs_eq_self.mpr h0, nsmul_eq_mul]
Proof state after:
case inl
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
ε : R
h : ∀ (r : R), r * ε < 1
k : ℕ
h0 : 0 ≤ ε
⊢ ↑k * ε < 1
Theorem: IMOSL.Extra.Infinitesimal.FloorRing_iff_mul_left₁
Proof state before:
case inl
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
ε : R
h : ∀ (r : R), r * ε < 1
k : ℕ
h0 : 0 ≤ ε
⊢ ↑k * ε < 1
Tactic:
exact h _
Proof state after:
no goals
Theorem: IMOSL.Extra.Infinitesimal.FloorRing_iff_mul_left₁
Proof state before:
case inr
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
ε : R
h : ∀ (r : R), r * ε < 1
k : ℕ
h0 : ε ≤ 0
⊢ k • |ε| < 1
Tactic:
rw [abs_eq_neg_self.mpr h0, nsmul_eq_mul, mul_neg, ← neg_mul]
Proof state after:
case inr
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
ε : R
h : ∀ (r : R), r * ε < 1
k : ℕ
h0 : ε ≤ 0
⊢ -↑k * ε < 1
Theorem: IMOSL.Extra.Infinitesimal.FloorRing_iff_mul_left₁
Proof state before:
case inr
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
ε : R
h : ∀ (r : R), r * ε < 1
k : ℕ
h0 : ε ≤ 0
⊢ -↑k * ε < 1
Tactic:
exact h _
Proof state after:
no goals
Theorem: IMOSL.Extra.Infinitesimal.FloorRing_iff_mul_right₁
Proof state before:
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
ε : R
h : ∀ (r : R), ε * r < 1
k : ℕ
⊢ k • |ε| < 1
Tactic:
rcases le_total 0 ε with h0 | h0
Proof state after:
case inl
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
ε : R
h : ∀ (r : R), ε * r < 1
k : ℕ
h0 : 0 ≤ ε
⊢ k • |ε| < 1

case inr
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
ε : R
h : ∀ (r : R), ε * r < 1
k : ℕ
h0 : ε ≤ 0
⊢ k • |ε| < 1
Theorem: IMOSL.Extra.Infinitesimal.FloorRing_iff_mul_right₁
Proof state before:
case inl
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
ε : R
h : ∀ (r : R), ε * r < 1
k : ℕ
h0 : 0 ≤ ε
⊢ k • |ε| < 1
Tactic:
rw [abs_eq_self.mpr h0, nsmul_eq_mul']
Proof state after:
case inl
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
ε : R
h : ∀ (r : R), ε * r < 1
k : ℕ
h0 : 0 ≤ ε
⊢ ε * ↑k < 1
Theorem: IMOSL.Extra.Infinitesimal.FloorRing_iff_mul_right₁
Proof state before:
case inl
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
ε : R
h : ∀ (r : R), ε * r < 1
k : ℕ
h0 : 0 ≤ ε
⊢ ε * ↑k < 1
Tactic:
exact h _
Proof state after:
no goals
Theorem: IMOSL.Extra.Infinitesimal.FloorRing_iff_mul_right₁
Proof state before:
case inr
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
ε : R
h : ∀ (r : R), ε * r < 1
k : ℕ
h0 : ε ≤ 0
⊢ k • |ε| < 1
Tactic:
rw [abs_eq_neg_self.mpr h0, nsmul_eq_mul', neg_mul, ← mul_neg]
Proof state after:
case inr
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
ε : R
h : ∀ (r : R), ε * r < 1
k : ℕ
h0 : ε ≤ 0
⊢ ε * -↑k < 1
Theorem: IMOSL.Extra.Infinitesimal.FloorRing_iff_mul_right₁
Proof state before:
case inr
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
ε : R
h : ∀ (r : R), ε * r < 1
k : ℕ
h0 : ε ≤ 0
⊢ ε * -↑k < 1
Tactic:
exact h _
Proof state after:
no goals
Theorem: IMOSL.Extra.Infinitesimal.FloorRing_iff_mul_left₂
Proof state before:
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
ε : R
⊢ Infinitesimal ε ↔ ∃ α, ∀ (r : R), r * ε < α
Tactic:
refine FloorRing_iff_mul_left₁.trans ⟨λ h ↦ ⟨1, h⟩, λ ⟨α, h⟩ r ↦ ?_⟩
Proof state after:
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
ε : R
x✝ : ∃ α, ∀ (r : R), r * ε < α
r α : R
h : ∀ (r : R), r * ε < α
⊢ r * ε < 1
Theorem: IMOSL.Extra.Infinitesimal.FloorRing_iff_mul_left₂
Proof state before:
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
ε : R
x✝ : ∃ α, ∀ (r : R), r * ε < α
r α : R
h : ∀ (r : R), r * ε < α
⊢ r * ε < 1
Tactic:
have h0 : 0 < α := (zero_mul ε).symm.trans_lt (h 0)
Proof state after:
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
ε : R
x✝ : ∃ α, ∀ (r : R), r * ε < α
r α : R
h : ∀ (r : R), r * ε < α
h0 : 0 < α
⊢ r * ε < 1
Theorem: IMOSL.Extra.Infinitesimal.FloorRing_iff_mul_left₂
Proof state before:
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
ε : R
x✝ : ∃ α, ∀ (r : R), r * ε < α
r α : R
h : ∀ (r : R), r * ε < α
h0 : 0 < α
⊢ r * ε < 1
Tactic:
specialize h (α * r)
Proof state after:
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
ε : R
x✝ : ∃ α, ∀ (r : R), r * ε < α
r α : R
h0 : 0 < α
h : α * r * ε < α
⊢ r * ε < 1
Theorem: IMOSL.Extra.Infinitesimal.FloorRing_iff_mul_left₂
Proof state before:
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
ε : R
x✝ : ∃ α, ∀ (r : R), r * ε < α
r α : R
h0 : 0 < α
h : α * r * ε < α
⊢ r * ε < 1
Tactic:
rwa [mul_assoc, mul_lt_iff_lt_one_right h0] at h
Proof state after:
no goals
Theorem: IMOSL.Extra.Infinitesimal.FloorRing_iff_mul_right₂
Proof state before:
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
ε : R
⊢ Infinitesimal ε ↔ ∃ α, ∀ (r : R), ε * r < α
Tactic:
refine FloorRing_iff_mul_right₁.trans ⟨λ h ↦ ⟨1, h⟩, λ ⟨α, h⟩ r ↦ ?_⟩
Proof state after:
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
ε : R
x✝ : ∃ α, ∀ (r : R), ε * r < α
r α : R
h : ∀ (r : R), ε * r < α
⊢ ε * r < 1
Theorem: IMOSL.Extra.Infinitesimal.FloorRing_iff_mul_right₂
Proof state before:
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
ε : R
x✝ : ∃ α, ∀ (r : R), ε * r < α
r α : R
h : ∀ (r : R), ε * r < α
⊢ ε * r < 1
Tactic:
have h0 : 0 < α := (mul_zero ε).symm.trans_lt (h 0)
Proof state after:
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
ε : R
x✝ : ∃ α, ∀ (r : R), ε * r < α
r α : R
h : ∀ (r : R), ε * r < α
h0 : 0 < α
⊢ ε * r < 1
Theorem: IMOSL.Extra.Infinitesimal.FloorRing_iff_mul_right₂
Proof state before:
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
ε : R
x✝ : ∃ α, ∀ (r : R), ε * r < α
r α : R
h : ∀ (r : R), ε * r < α
h0 : 0 < α
⊢ ε * r < 1
Tactic:
specialize h (r * α)
Proof state after:
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
ε : R
x✝ : ∃ α, ∀ (r : R), ε * r < α
r α : R
h0 : 0 < α
h : ε * (r * α) < α
⊢ ε * r < 1
Theorem: IMOSL.Extra.Infinitesimal.FloorRing_iff_mul_right₂
Proof state before:
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
ε : R
x✝ : ∃ α, ∀ (r : R), ε * r < α
r α : R
h0 : 0 < α
h : ε * (r * α) < α
⊢ ε * r < 1
Tactic:
rwa [← mul_assoc, mul_lt_iff_lt_one_left h0] at h
Proof state after:
no goals
Theorem: IMOSL.IMO2015A1.final_solution
Proof 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)
Proof 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
Theorem: IMOSL.IMO2015A1.final_solution
Proof 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 ?_ ?_
Proof 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
Theorem: IMOSL.IMO2015A1.final_solution
Proof 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]
Proof 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
Theorem: IMOSL.IMO2015A1.final_solution
Proof 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)
Proof state after:
no goals
Theorem: IMOSL.IMO2015A1.final_solution
Proof 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]
Proof 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
Theorem: IMOSL.IMO2015A1.final_solution
Proof 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
Proof 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
Theorem: IMOSL.IMO2015A1.final_solution
Proof 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
Proof 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
Theorem: IMOSL.IMO2015A1.final_solution
Proof 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'
Proof 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
Theorem: IMOSL.IMO2015A1.final_solution
Proof 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]
Proof 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
Theorem: IMOSL.IMO2015A1.final_solution
Proof 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)
Proof 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
Theorem: IMOSL.IMO2015A1.final_solution
Proof 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
Proof state after:
no goals
Theorem: IMOSL.IMO2015A1.final_solution
Proof 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
Proof 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
Theorem: IMOSL.IMO2015A1.final_solution
Proof 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]
Proof 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
Theorem: IMOSL.IMO2015A1.final_solution
Proof 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
Proof 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
Theorem: IMOSL.IMO2015A1.final_solution
Proof 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 ≤ _) _)
Proof 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
Theorem: IMOSL.IMO2015A1.final_solution
Proof 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]
Proof 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
Theorem: IMOSL.IMO2015A1.final_solution
Proof 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)
Proof 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
Theorem: IMOSL.IMO2015A1.final_solution
Proof 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]
Proof 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
Theorem: IMOSL.IMO2015A1.final_solution
Proof 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
Proof 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
Theorem: IMOSL.IMO2015A1.final_solution
Proof 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
Proof 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
Theorem: IMOSL.IMO2015A1.final_solution
Proof 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
Proof 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
Theorem: IMOSL.IMO2015A1.final_solution
Proof 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]
Proof 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
Theorem: IMOSL.IMO2015A1.final_solution
Proof 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)]
Proof 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
Theorem: IMOSL.IMO2015A1.final_solution
Proof 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))
Proof state after:
no goals