awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.BigOperators (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Ring β
abv : β → α
inst_4 : IsAbsoluteValue abv
f g : ℕ → β
ha : IsCauSeq.{u_1, u_1} (α := α) abs fun (m : ℕ) ↦ ∑ n ∈ range m, abv (f n)
hb : IsCauSeq abv fun (m : ℕ) ↦ ∑ n ∈ range m, g n
ε : α
ε0 : 0 < ε
P : α
hP : ∀ (i : ℕ), |∑ n ∈ range i, abv (f n)| < P
Q : α
hQ : ∀ (i : ℕ), abv (∑ n ∈ range i, g n) < Q
hP0 : 0 < P
hPε0 : 0 < ε / (2 * P)
N : ℕ
hN : ∀ j ≥ N, ∀ k ≥ N, abv (HSub.hSub (α := β) (∑ n ∈ range j, g n) (∑ n ∈ range k, g n)) < ε / (2 * P)
hQε0 : 0 < ε / (4 * Q)
M : ℕ
hM : ∀ j ≥ M, ∀ k ≥ M, |HSub.hSub (α := α) (∑ n ∈ range j, abv (f n)) (∑ n ∈ range k, abv (f n))| < ε / (4 * Q)
K : ℕ
hK : K ≥ 2 * (max N M + 1)
h₁ :
  Eq.{u_2 + 1} (α := β) (∑ m ∈ range K, ∑ k ∈ range (m + 1), f k * g (m - k))
    (∑ m ∈ range K, ∑ n ∈ range (K - m), f m * g n)
h₂ :
  Eq.{u_2 + 1} (α := (i : ℕ) → β) (fun (i : ℕ) ↦ ∑ k ∈ range (K - i), f i * g k) fun (i : ℕ) ↦
    f i * ∑ k ∈ range (K - i), g k
h₃ :
  ∑ i ∈ range K, f i * ∑ k ∈ range (K - i), g k =
    HAdd.hAdd (α := β) (∑ i ∈ range K, f i * HSub.hSub (α := β) (∑ k ∈ range (K - i), g k) (∑ k ∈ range K, g k))
      (∑ i ∈ range K, f i * ∑ k ∈ range K, g k)
two_mul_two : 4 = HMul.hMul (α := α) 2 2
hQ0 : Q ≠ 0
h2Q0 : 2 * Q ≠ 0
hε : ε / (2 * P) * P + ε / (4 * Q) * (2 * Q) = ε
hNMK : max N M + 1 < K
hKN : N < K
hsumlesum :
  LE.le.{u_1} (α := α)
    (∑ i ∈ range (max N M + 1), abv (f i) * abv (HSub.hSub (α := β) (∑ k ∈ range (K - i), g k) (∑ k ∈ range K, g k)))
    (∑ i ∈ range (max N M + 1), abv (f i) * (ε / (2 * P)))
hsumltP : ∑ n ∈ range (max N M + 1), abv (f n) < P
i :
  LE.le.{u_1} (α := α)
    (∑ i ∈ range K with max N M + 1 ≤ i,
      abv (f i) * abv (HSub.hSub (α := β) (∑ k ∈ range (K - i), g k) (∑ k ∈ range K, g k)))
    (∑ i ∈ range K with max N M + 1 ≤ i, abv (f i) * (2 * Q))
⊢ ∑ k ∈ range K with max N M + 1 ≤ k,
      abv (f k) * abv (HSub.hSub (α := β) (∑ k ∈ range (K - k), g k) (∑ k ∈ range K, g k)) <
    ε / (4 * Q) * (2 * Q)
have i₁ : ∑ i ∈ range K with max N M + 1 ≤ i, abv (f i) * (2 * Q) < ε / (4 * Q) * (2 * Q)
Tactic: calc
    (∑ i ∈ range K with max N M + 1 ≤ i,
          abv (f i) * abv ((∑ k ∈ range (K - i), g k) - ∑ k ∈ range K, g k)) ≤
        ∑ i ∈ range K with max N M + 1 ≤ i, abv (f i) * (2 * Q) := by
        gcongr
        rw [sub_eq_add_neg]
        grw [abv_add abv]
        rw [two_mul, abv_neg abv]
        gcongr <;> exact le_of_lt (hQ _)
    _ < ε / (4 * Q) * (2 * Q) := by
        rw [← sum_mul, ← sum_range_sub_sum_range (le_of_lt hNMK)]
        have := lt_of_le_of_lt (abv_nonneg _ _) (hQ 0)
        gcongr
        exact (le_abs_self _).trans_lt <|
          hM _ ((Nat.le_succ_of_le (le_max_right _ _)).trans hNMK.le) _ <|
            Nat.le_succ_of_le <| le_max_right _ _
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.BigOperators (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Archimedean α
f : ℕ → α
a : α
m : ℕ
ham : ∀ n ≥ m, |f n| ≤ a
hnm : ∀ n ≥ m, f n.succ ≤ f n
ε : α
ε0 : ε > 0
⊢ ∃ (i : ℕ), ∀ j ≥ i, |f j - f i| < ε
have let : ∀ (k : ℕ) (hk : a ≤ k • ε), ∃ (i : ℕ), ∀ j ≥ i, |f j - f i| < ε
Tactic: let ⟨k, hk⟩ := Archimedean.arch a ε0
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.BigOperators (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Archimedean α
f : ℕ → α
a : α
m : ℕ
ham : ∀ n ≥ m, |f n| ≤ a
hnm_1 : ∀ n ≥ m, f n.succ ≤ f n
ε : α
ε0 : ε > 0
k : ℕ
hk : a ≤ k • ε
n : ℕ
hnm : n ≥ m
⊢ a < -(a - (k + (k + 1)) • ε)
have rw : a + a < k • ε + (k • ε + ε)
Tactic: rw [neg_sub, lt_sub_iff_add_lt, add_nsmul, add_nsmul, one_nsmul]
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.BigOperators (hypothesis)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Archimedean α
f : ℕ → α
a : α
m : ℕ
ham : ∀ n ≥ m, |f n| ≤ a
hnm : ∀ n ≥ m, f n.succ ≤ f n
ε : α
ε0 : ε > 0
k : ℕ
hk : a ≤ k • ε
⊢ ∃ (i : ℕ), ∀ j ≥ i, |f j - f i| < ε
have h : ∃ (l : ℕ), ∀ n ≥ m, a - l • ε < f n
Tactic: have h : ∃ l, ∀ n ≥ m, a - l • ε < f n :=
    ⟨k + k + 1, fun n hnm ↦
      lt_of_lt_of_le (show a - (k + (k + 1)) • ε < -|f n| from
          lt_neg.1 <| (ham n hnm).trans_lt
              (by
                rw [neg_sub, lt_sub_iff_add_lt, add_nsmul, add_nsmul, one_nsmul]
                exact add_lt_add_of_le_of_lt hk (lt_of_le_of_lt hk (lt_add_of_pos_right _ ε0))))
        (neg_le.2 <| abs_neg (f n) ▸ le_abs_self _)⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.BigOperators (hypothesis)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Archimedean α
f : ℕ → α
a : α
m : ℕ
ham : ∀ n ≥ m, |f n| ≤ a
hnm : ∀ n ≥ m, f n.succ ≤ f n
ε : α
ε0 : ε > 0
k : ℕ
hk : a ≤ k • ε
h : ∃ (l : ℕ), ∀ n ≥ m, a - l • ε < f n
l : ℕ := Nat.find (p := fun (n : ℕ) ↦ ∀ n_1 ≥ m, a - n • ε < f n_1) h
⊢ ∃ (i : ℕ), ∀ j ≥ i, |f j - f i| < ε
have hl : ∀ n ≥ m, f n > a - l • ε
Tactic: have hl : ∀ n : ℕ, n ≥ m → f n > a - l • ε := Nat.find_spec h
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.BigOperators (hypothesis)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Archimedean α
f : ℕ → α
a : α
m : ℕ
ham : ∀ n ≥ m, |f n| ≤ a
hnm : ∀ n ≥ m, f n.succ ≤ f n
ε : α
ε0 : ε > 0
k : ℕ
hk : a ≤ k • ε
h : ∃ (l : ℕ), ∀ n ≥ m, a - l • ε < f n
l : ℕ := Nat.find (p := fun (n : ℕ) ↦ ∀ n_1 ≥ m, a - n • ε < f n_1) h
hl : ∀ n ≥ m, f n > a - l • ε
hl0 : l = 0
⊢ a < f m
have this : f m > a - l • ε
Tactic: have := hl m (le_refl m)
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.BigOperators (hypothesis)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Archimedean α
f : ℕ → α
a : α
m : ℕ
ham : ∀ n ≥ m, |f n| ≤ a
hnm : ∀ n ≥ m, f n.succ ≤ f n
ε : α
ε0 : ε > 0
k : ℕ
hk : a ≤ k • ε
h : ∃ (l : ℕ), ∀ n ≥ m, a - l • ε < f n
l : ℕ := Nat.find (p := fun (n : ℕ) ↦ ∀ n_1 ≥ m, a - n • ε < f n_1) h
hl : ∀ n ≥ m, f n > a - l • ε
⊢ ∃ (i : ℕ), ∀ j ≥ i, |f j - f i| < ε
have hl0 : l ≠ 0
Tactic: have hl0 : l ≠ 0 := fun hl0 ↦
    not_lt_of_ge (ham m le_rfl)
      (lt_of_lt_of_le (by have := hl m (le_refl m); simpa [hl0] using this) (le_abs_self (f m)))
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.BigOperators (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Archimedean α
f : ℕ → α
a : α
m : ℕ
ham : ∀ n ≥ m, |f n| ≤ a
hnm : ∀ n ≥ m, f n.succ ≤ f n
ε : α
ε0 : ε > 0
k : ℕ
hk : a ≤ k • ε
h : ∃ (l : ℕ), ∀ n ≥ m, a - l • ε < f n
l : ℕ := Nat.find (p := fun (n : ℕ) ↦ ∀ n_1 ≥ m, a - n • ε < f n_1) h
hl : ∀ n ≥ m, f n > a - l • ε
hl0 : l ≠ 0
⊢ ∃ (i : ℕ), ∀ j ≥ i, |f j - f i| < ε
have obtain : ∀ (i : ℕ) (hi : ¬(i ≥ m → a - (Nat.find (p := fun (n : ℕ) ↦ ∀ n_1 ≥ m, a - n • ε < f n_1) h).pred • ε < f i)),
  ∃ (i : ℕ), ∀ j ≥ i, |f j - f i| < ε
Tactic: obtain ⟨i, hi⟩ := not_forall.1 (Nat.find_min h (Nat.pred_lt hl0))
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.BigOperators (hypothesis)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Archimedean α
f : ℕ → α
a : α
m : ℕ
ham : ∀ n ≥ m, |f n| ≤ a
hnm : ∀ n ≥ m, f n.succ ≤ f n
ε : α
ε0 : ε > 0
k : ℕ
hk : a ≤ k • ε
h : ∃ (l : ℕ), ∀ n ≥ m, a - l • ε < f n
l : ℕ := Nat.find (p := fun (n : ℕ) ↦ ∀ n_1 ≥ m, a - n • ε < f n_1) h
hl : ∀ n ≥ m, f n > a - l • ε
hl0 : l ≠ 0
i : ℕ
hi : ¬(i ≥ m → a - (Nat.find (p := fun (n : ℕ) ↦ ∀ n_1 ≥ m, a - n • ε < f n_1) h).pred • ε < f i)
⊢ ∃ (i : ℕ), ∀ j ≥ i, |f j - f i| < ε
have hi₁ : i ≥ m ∧ f i ≤ a - (Nat.find (p := fun (n : ℕ) ↦ ∀ n_1 ≥ m, a - n • ε < f n_1) h).pred • ε
Tactic: rw [Classical.not_imp, not_lt] at hi
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.BigOperators (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Archimedean α
f : ℕ → α
a : α
m : ℕ
ham : ∀ n ≥ m, |f n| ≤ a
hnm : ∀ n ≥ m, f n.succ ≤ f n
ε : α
ε0 : ε > 0
k : ℕ
hk : a ≤ k • ε
h : ∃ (l : ℕ), ∀ n ≥ m, a - l • ε < f n
l : ℕ := Nat.find (p := fun (n : ℕ) ↦ ∀ n_1 ≥ m, a - n • ε < f n_1) h
hl : ∀ n ≥ m, f n > a - l • ε
hl0 : l ≠ 0
i : ℕ
hi : i ≥ m ∧ f i ≤ a - (Nat.find (p := fun (n : ℕ) ↦ ∀ n_1 ≥ m, a - n • ε < f n_1) h).pred • ε
⊢ ∃ (i : ℕ), ∀ j ≥ i, |f j - f i| < ε
have exists : ∀ j ≥ i, |f j - f i| < ε
Tactic: exists i
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.BigOperators (hypothesis)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Archimedean α
f : ℕ → α
a : α
m : ℕ
ham : ∀ n ≥ m, |f n| ≤ a
hnm : ∀ n ≥ m, f n.succ ≤ f n
ε : α
ε0 : ε > 0
k : ℕ
hk : a ≤ k • ε
h : ∃ (l : ℕ), ∀ n ≥ m, a - l • ε < f n
l : ℕ := Nat.find (p := fun (n : ℕ) ↦ ∀ n_1 ≥ m, a - n • ε < f n_1) h
hl : ∀ n ≥ m, f n > a - l • ε
hl0 : l ≠ 0
i : ℕ
hi : i ≥ m ∧ f i ≤ a - (Nat.find (p := fun (n : ℕ) ↦ ∀ n_1 ≥ m, a - n • ε < f n_1) h).pred • ε
j : ℕ
hj : j ≥ i
⊢ |f j - f i| < ε
have hfij : f j ≤ f i
Tactic: have hfij : f j ≤ f i := (Nat.rel_of_forall_rel_succ_of_le_of_le (· ≥ ·) hnm hi.1 hj).le
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.BigOperators (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Archimedean α
f : ℕ → α
a : α
m : ℕ
ham : ∀ n ≥ m, |f n| ≤ a
hnm : ∀ n ≥ m, f n.succ ≤ f n
ε : α
ε0 : ε > 0
k : ℕ
hk : a ≤ k • ε
h : ∃ (l : ℕ), ∀ n ≥ m, a - l • ε < f n
l : ℕ := Nat.find (p := fun (n : ℕ) ↦ ∀ n_1 ≥ m, a - n • ε < f n_1) h
hl : ∀ n ≥ m, f n > a - l • ε
hl0 : l ≠ 0
i : ℕ
hi : i ≥ m ∧ f i ≤ a - (Nat.find (p := fun (n : ℕ) ↦ ∀ n_1 ≥ m, a - n • ε < f n_1) h).pred • ε
j : ℕ
hj : j ≥ i
hfij : f j ≤ f i
⊢ |f j - f i| < ε
have rw : f i < f j + ε
Tactic: rw [abs_of_nonpos (sub_nonpos.2 hfij), neg_sub, sub_lt_iff_lt_add']
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.BigOperators (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Archimedean α
f : ℕ → α
a : α
m : ℕ
ham : ∀ n ≥ m, |f n| ≤ a
hnm : ∀ n ≥ m, f n.succ ≤ f n
ε : α
ε0 : ε > 0
k : ℕ
hk : a ≤ k • ε
h : ∃ (l : ℕ), ∀ n ≥ m, a - l • ε < f n
l : ℕ := Nat.find (p := fun (n : ℕ) ↦ ∀ n_1 ≥ m, a - n • ε < f n_1) h
hl : ∀ n ≥ m, f n > a - l • ε
hl0 : l ≠ 0
i : ℕ
hi : i ≥ m ∧ f i ≤ a - (Nat.find (p := fun (n : ℕ) ↦ ∀ n_1 ≥ m, a - n • ε < f n_1) h).pred • ε
j : ℕ
hj : j ≥ i
hfij : f j ≤ f i
| a - l.pred • ε = a - l • ε + ε
have rhs : a - l • ε + ε
Tactic: rhs
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.BigOperators (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Archimedean α
f : ℕ → α
a : α
m : ℕ
ham : ∀ n ≥ m, |f n| ≤ a
hnm : ∀ n ≥ m, f n.succ ≤ f n
ε : α
ε0 : ε > 0
k : ℕ
hk : a ≤ k • ε
h : ∃ (l : ℕ), ∀ n ≥ m, a - l • ε < f n
l : ℕ := Nat.find (p := fun (n : ℕ) ↦ ∀ n_1 ≥ m, a - n • ε < f n_1) h
hl : ∀ n ≥ m, f n > a - l • ε
hl0 : l ≠ 0
i : ℕ
hi : i ≥ m ∧ f i ≤ a - (Nat.find (p := fun (n : ℕ) ↦ ∀ n_1 ≥ m, a - n • ε < f n_1) h).pred • ε
j : ℕ
hj : j ≥ i
hfij : f j ≤ f i
| a - l • ε + ε
have rw : a - l.pred • ε
Tactic: rw [← Nat.succ_pred_eq_of_pos (Nat.pos_of_ne_zero hl0), succ_nsmul, sub_add,
          add_sub_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.BigOperators (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Archimedean α
f : ℕ → α
a : α
m : ℕ
ham : ∀ n ≥ m, |f n| ≤ a
hnm : ∀ n ≥ m, f n.succ ≤ f n
ε : α
ε0 : ε > 0
k : ℕ
hk : a ≤ k • ε
h : ∃ (l : ℕ), ∀ n ≥ m, a - l • ε < f n
l : ℕ := Nat.find (p := fun (n : ℕ) ↦ ∀ n_1 ≥ m, a - n • ε < f n_1) h
hl : ∀ n ≥ m, f n > a - l • ε
hl0 : l ≠ 0
i : ℕ
hi : i ≥ m ∧ f i ≤ a - (Nat.find (p := fun (n : ℕ) ↦ ∀ n_1 ≥ m, a - n • ε < f n_1) h).pred • ε
j : ℕ
hj : j ≥ i
hfij : f j ≤ f i
| a - l.pred • ε = a - l • ε + ε
have rw : a - l.pred • ε
Tactic: rhs
        rw [← Nat.succ_pred_eq_of_pos (Nat.pos_of_ne_zero hl0), succ_nsmul, sub_add,
          add_sub_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.BigOperators (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Archimedean α
f : ℕ → α
a : α
m : ℕ
ham : ∀ n ≥ m, |f n| ≤ a
hnm : ∀ n ≥ m, f n.succ ≤ f n
ε : α
ε0 : ε > 0
k : ℕ
hk : a ≤ k • ε
h : ∃ (l : ℕ), ∀ n ≥ m, a - l • ε < f n
l : ℕ := Nat.find (p := fun (n : ℕ) ↦ ∀ n_1 ≥ m, a - n • ε < f n_1) h
hl : ∀ n ≥ m, f n > a - l • ε
hl0 : l ≠ 0
i : ℕ
hi : i ≥ m ∧ f i ≤ a - (Nat.find (p := fun (n : ℕ) ↦ ∀ n_1 ≥ m, a - n • ε < f n_1) h).pred • ε
j : ℕ
hj : j ≥ i
hfij : f j ≤ f i
⊢ a - l.pred • ε = a - l • ε + ε
have conv : a - l.pred • ε = a - l • ε + ε
Tactic: conv =>
        rhs
        rw [← Nat.succ_pred_eq_of_pos (Nat.pos_of_ne_zero hl0), succ_nsmul, sub_add,
          add_sub_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.BigOperators (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Archimedean α
f : ℕ → α
a : α
m : ℕ
ham : ∀ n ≥ m, |f n| ≤ a
hnm : ∀ n ≥ m, f n.succ ≤ f n
ε : α
ε0 : ε > 0
k : ℕ
hk : a ≤ k • ε
h : ∃ (l : ℕ), ∀ n ≥ m, a - l • ε < f n
l : ℕ := Nat.find (p := fun (n : ℕ) ↦ ∀ n_1 ≥ m, a - n • ε < f n_1) h
hl : ∀ n ≥ m, f n > a - l • ε
hl0 : l ≠ 0
i : ℕ
hi : i ≥ m ∧ f i ≤ a - (Nat.find (p := fun (n : ℕ) ↦ ∀ n_1 ≥ m, a - n • ε < f n_1) h).pred • ε
j : ℕ
hj : j ≥ i
hfij : f j ≤ f i
conv : a - l.pred • ε = a - l • ε + ε
⊢ a - l.pred • ε = a - l • ε + ε
have conv₁ : a - l.pred • ε = a - l.pred • ε
Tactic: conv =>
        rhs
        rw [← Nat.succ_pred_eq_of_pos (Nat.pos_of_ne_zero hl0), succ_nsmul, sub_add,
          add_sub_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.BigOperators (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Archimedean α
f : ℕ → α
a : α
m : ℕ
ham : ∀ n ≥ m, |f n| ≤ a
hnm : ∀ n ≥ m, f n.succ ≤ f n
ε : α
ε0 : ε > 0
k : ℕ
hk : a ≤ k • ε
h : ∃ (l : ℕ), ∀ n ≥ m, a - l • ε < f n
l : ℕ := Nat.find (p := fun (n : ℕ) ↦ ∀ n_1 ≥ m, a - n • ε < f n_1) h
hl : ∀ n ≥ m, f n > a - l • ε
hl0 : l ≠ 0
i : ℕ
hi : i ≥ m ∧ f i ≤ a - (Nat.find (p := fun (n : ℕ) ↦ ∀ n_1 ≥ m, a - n • ε < f n_1) h).pred • ε
j : ℕ
hj : j ≥ i
hfij : f j ≤ f i
⊢ a - l • ε + ε < f j + ε
have bc : a - l • ε < f j
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.BigOperators (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Archimedean α
f : ℕ → α
a : α
m : ℕ
ham : ∀ n ≥ m, |f n| ≤ a
hnm : ∀ n ≥ m, f n.succ ≤ f n
ε : α
ε0 : ε > 0
k : ℕ
hk : a ≤ k • ε
h : ∃ (l : ℕ), ∀ n ≥ m, a - l • ε < f n
l : ℕ := Nat.find (p := fun (n : ℕ) ↦ ∀ n_1 ≥ m, a - n • ε < f n_1) h
hl : ∀ n ≥ m, f n > a - l • ε
hl0 : l ≠ 0
i : ℕ
hi : i ≥ m ∧ f i ≤ a - (Nat.find (p := fun (n : ℕ) ↦ ∀ n_1 ≥ m, a - n • ε < f n_1) h).pred • ε
j : ℕ
hj : j ≥ i
hfij : f j ≤ f i
⊢ f i < f j + ε
have f₁ : a - l.pred • ε = a - l • ε + ε
Tactic: calc
    f i ≤ a - Nat.pred l • ε := hi.2
    _ = a - l • ε + ε := by
      conv =>
        rhs
        rw [← Nat.succ_pred_eq_of_pos (Nat.pos_of_ne_zero hl0), succ_nsmul, sub_add,
          add_sub_cancel_right]
    _ < f j + ε := by gcongr; exact hl _ <| hi.1.trans hj
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.BigOperators (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Archimedean α
f : ℕ → α
a : α
m : ℕ
ham : ∀ n ≥ m, |f n| ≤ a
hnm : ∀ n ≥ m, f n.succ ≤ f n
ε : α
ε0 : ε > 0
k : ℕ
hk : a ≤ k • ε
h : ∃ (l : ℕ), ∀ n ≥ m, a - l • ε < f n
l : ℕ := Nat.find (p := fun (n : ℕ) ↦ ∀ n_1 ≥ m, a - n • ε < f n_1) h
hl : ∀ n ≥ m, f n > a - l • ε
hl0 : l ≠ 0
i : ℕ
hi : i ≥ m ∧ f i ≤ a - (Nat.find (p := fun (n : ℕ) ↦ ∀ n_1 ≥ m, a - n • ε < f n_1) h).pred • ε
j : ℕ
hj : j ≥ i
hfij : f j ≤ f i
f₁ : a - l.pred • ε = a - l • ε + ε
⊢ f i < f j + ε
have f₂ : a - l • ε + ε < f j + ε
Tactic: calc
    f i ≤ a - Nat.pred l • ε := hi.2
    _ = a - l • ε + ε := by
      conv =>
        rhs
        rw [← Nat.succ_pred_eq_of_pos (Nat.pos_of_ne_zero hl0), succ_nsmul, sub_add,
          add_sub_cancel_right]
    _ < f j + ε := by gcongr; exact hl _ <| hi.1.trans hj
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.BigOperators (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Archimedean α
f : ℕ → α
a : α
m : ℕ
ham : ∀ n ≥ m, |f n| ≤ a
hnm : ∀ n ≥ m, f n.succ ≤ f n
ε : α
ε0 : ε > 0
⊢ ∃ (i : ℕ), ∀ j ≥ i, |f j - f i| < ε
have let : ∀ (k : ℕ) (hk : a ≤ k • ε), ∃ (i : ℕ), ∀ j ≥ i, |f j - f i| < ε
Tactic: classical
  let ⟨k, hk⟩ := Archimedean.arch a ε0
  have h : ∃ l, ∀ n ≥ m, a - l • ε < f n :=
    ⟨k + k + 1, fun n hnm ↦
      lt_of_lt_of_le (show a - (k + (k + 1)) • ε < -|f n| from
          lt_neg.1 <| (ham n hnm).trans_lt
              (by
                rw [neg_sub, lt_sub_iff_add_lt, add_nsmul, add_nsmul, one_nsmul]
                exact add_lt_add_of_le_of_lt hk (lt_of_le_of_lt hk (lt_add_of_pos_right _ ε0))))
        (neg_le.2 <| abs_neg (f n) ▸ le_abs_self _)⟩
  let l := Nat.find h
  have hl : ∀ n : ℕ, n ≥ m → f n > a - l • ε := Nat.find_spec h
  have hl0 : l ≠ 0 := fun hl0 ↦
    not_lt_of_ge (ham m le_rfl)
      (lt_of_lt_of_le (by have := hl m (le_refl m); simpa [hl0] using this) (le_abs_self (f m)))
  obtain ⟨i, hi⟩ := not_forall.1 (Nat.find_min h (Nat.pred_lt hl0))
  rw [Classical.not_imp, not_lt] at hi
  exists i
  intro j hj
  have hfij : f j ≤ f i := (Nat.rel_of_forall_rel_succ_of_le_of_le (· ≥ ·) hnm hi.1 hj).le
  rw [abs_of_nonpos (sub_nonpos.2 hfij), neg_sub, sub_lt_iff_lt_add']
  calc
    f i ≤ a - Nat.pred l • ε := hi.2
    _ = a - l • ε + ε := by
      conv =>
        rhs
        rw [← Nat.succ_pred_eq_of_pos (Nat.pos_of_ne_zero hl0), succ_nsmul, sub_add,
          add_sub_cancel_right]
    _ < f j + ε := by gcongr; exact hl _ <| hi.1.trans hj
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.BigOperators (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Archimedean α
f : ℕ → α
a : α
m : ℕ
ham : ∀ n ≥ m, |f n| ≤ a
hnm : ∀ n ≥ m, f n.succ ≤ f n
ε : α
ε0 : ε > 0
let let₁ let₂ : ∀ (k : ℕ) (hk : a ≤ k • ε), ∃ (i : ℕ), ∀ j ≥ i, |f j - f i| < ε
⊢ ∃ (i : ℕ), ∀ j ≥ i, |f j - f i| < ε
have let₃ : ∀ (k : ℕ) (hk : a ≤ k • ε) (h : ∃ (l : ℕ), ∀ n ≥ m, a - l • ε < f n), ∃ (i : ℕ), ∀ j ≥ i, |f j - f i| < ε
Tactic: classical
  let ⟨k, hk⟩ := Archimedean.arch a ε0
  have h : ∃ l, ∀ n ≥ m, a - l • ε < f n :=
    ⟨k + k + 1, fun n hnm ↦
      lt_of_lt_of_le (show a - (k + (k + 1)) • ε < -|f n| from
          lt_neg.1 <| (ham n hnm).trans_lt
              (by
                rw [neg_sub, lt_sub_iff_add_lt, add_nsmul, add_nsmul, one_nsmul]
                exact add_lt_add_of_le_of_lt hk (lt_of_le_of_lt hk (lt_add_of_pos_right _ ε0))))
        (neg_le.2 <| abs_neg (f n) ▸ le_abs_self _)⟩
  let l := Nat.find h
  have hl : ∀ n : ℕ, n ≥ m → f n > a - l • ε := Nat.find_spec h
  have hl0 : l ≠ 0 := fun hl0 ↦
    not_lt_of_ge (ham m le_rfl)
      (lt_of_lt_of_le (by have := hl m (le_refl m); simpa [hl0] using this) (le_abs_self (f m)))
  obtain ⟨i, hi⟩ := not_forall.1 (Nat.find_min h (Nat.pred_lt hl0))
  rw [Classical.not_imp, not_lt] at hi
  exists i
  intro j hj
  have hfij : f j ≤ f i := (Nat.rel_of_forall_rel_succ_of_le_of_le (· ≥ ·) hnm hi.1 hj).le
  rw [abs_of_nonpos (sub_nonpos.2 hfij), neg_sub, sub_lt_iff_lt_add']
  calc
    f i ≤ a - Nat.pred l • ε := hi.2
    _ = a - l • ε + ε := by
      conv =>
        rhs
        rw [← Nat.succ_pred_eq_of_pos (Nat.pos_of_ne_zero hl0), succ_nsmul, sub_add,
          add_sub_cancel_right]
    _ < f j + ε := by gcongr; exact hl _ <| hi.1.trans hj
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.BigOperators (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Archimedean α
f : ℕ → α
a : α
m : ℕ
ham : ∀ n ≥ m, |f n| ≤ a
hnm : ∀ n ≥ m, f n.succ ≤ f n
ε : α
ε0 : ε > 0
let let₁ let₂ : ∀ (k : ℕ) (hk : a ≤ k • ε), ∃ (i : ℕ), ∀ j ≥ i, |f j - f i| < ε
let₃ let₄ : ∀ (k : ℕ) (hk : a ≤ k • ε) (h : ∃ (l : ℕ), ∀ n ≥ m, a - l • ε < f n), ∃ (i : ℕ), ∀ j ≥ i, |f j - f i| < ε
⊢ ∃ (i : ℕ), ∀ j ≥ i, |f j - f i| < ε
have let₅ : ∀ (k : ℕ) (hk : a ≤ k • ε) (h : ∃ (l : ℕ), ∀ n ≥ m, a - l • ε < f n),
  let l := Nat.find (p := fun (n : ℕ) ↦ ∀ n_1 ≥ m, a - n • ε < f n_1) h;
  ∀ (hl : ∀ n ≥ m, f n > a - l • ε), ∃ (i : ℕ), ∀ j ≥ i, |f j - f i| < ε
Tactic: classical
  let ⟨k, hk⟩ := Archimedean.arch a ε0
  have h : ∃ l, ∀ n ≥ m, a - l • ε < f n :=
    ⟨k + k + 1, fun n hnm ↦
      lt_of_lt_of_le (show a - (k + (k + 1)) • ε < -|f n| from
          lt_neg.1 <| (ham n hnm).trans_lt
              (by
                rw [neg_sub, lt_sub_iff_add_lt, add_nsmul, add_nsmul, one_nsmul]
                exact add_lt_add_of_le_of_lt hk (lt_of_le_of_lt hk (lt_add_of_pos_right _ ε0))))
        (neg_le.2 <| abs_neg (f n) ▸ le_abs_self _)⟩
  let l := Nat.find h
  have hl : ∀ n : ℕ, n ≥ m → f n > a - l • ε := Nat.find_spec h
  have hl0 : l ≠ 0 := fun hl0 ↦
    not_lt_of_ge (ham m le_rfl)
      (lt_of_lt_of_le (by have := hl m (le_refl m); simpa [hl0] using this) (le_abs_self (f m)))
  obtain ⟨i, hi⟩ := not_forall.1 (Nat.find_min h (Nat.pred_lt hl0))
  rw [Classical.not_imp, not_lt] at hi
  exists i
  intro j hj
  have hfij : f j ≤ f i := (Nat.rel_of_forall_rel_succ_of_le_of_le (· ≥ ·) hnm hi.1 hj).le
  rw [abs_of_nonpos (sub_nonpos.2 hfij), neg_sub, sub_lt_iff_lt_add']
  calc
    f i ≤ a - Nat.pred l • ε := hi.2
    _ = a - l • ε + ε := by
      conv =>
        rhs
        rw [← Nat.succ_pred_eq_of_pos (Nat.pos_of_ne_zero hl0), succ_nsmul, sub_add,
          add_sub_cancel_right]
    _ < f j + ε := by gcongr; exact hl _ <| hi.1.trans hj
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.BigOperators (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Archimedean α
f : ℕ → α
a : α
m : ℕ
ham : ∀ n ≥ m, |f n| ≤ a
hnm : ∀ n ≥ m, f n.succ ≤ f n
ε : α
ε0 : ε > 0
let let₁ let₂ : ∀ (k : ℕ) (hk : a ≤ k • ε), ∃ (i : ℕ), ∀ j ≥ i, |f j - f i| < ε
let₃ let₄ : ∀ (k : ℕ) (hk : a ≤ k • ε) (h : ∃ (l : ℕ), ∀ n ≥ m, a - l • ε < f n), ∃ (i : ℕ), ∀ j ≥ i, |f j - f i| < ε
let₅ :
  ∀ (k : ℕ) (hk : a ≤ k • ε) (h : ∃ (l : ℕ), ∀ n ≥ m, a - l • ε < f n),
    let l := Nat.find (p := fun (n : ℕ) ↦ ∀ n_1 ≥ m, a - n • ε < f n_1) h;
    ∀ (hl : ∀ n ≥ m, f n > a - l • ε), ∃ (i : ℕ), ∀ j ≥ i, |f j - f i| < ε
⊢ ∃ (i : ℕ), ∀ j ≥ i, |f j - f i| < ε
have let₆ : ∀ (k : ℕ) (hk : a ≤ k • ε) (h : ∃ (l : ℕ), ∀ n ≥ m, a - l • ε < f n),
  let l := Nat.find (p := fun (n : ℕ) ↦ ∀ n_1 ≥ m, a - n • ε < f n_1) h;
  ∀ (hl : ∀ n ≥ m, f n > a - l • ε) (hl0 : l ≠ 0), ∃ (i : ℕ), ∀ j ≥ i, |f j - f i| < ε
Tactic: classical
  let ⟨k, hk⟩ := Archimedean.arch a ε0
  have h : ∃ l, ∀ n ≥ m, a - l • ε < f n :=
    ⟨k + k + 1, fun n hnm ↦
      lt_of_lt_of_le (show a - (k + (k + 1)) • ε < -|f n| from
          lt_neg.1 <| (ham n hnm).trans_lt
              (by
                rw [neg_sub, lt_sub_iff_add_lt, add_nsmul, add_nsmul, one_nsmul]
                exact add_lt_add_of_le_of_lt hk (lt_of_le_of_lt hk (lt_add_of_pos_right _ ε0))))
        (neg_le.2 <| abs_neg (f n) ▸ le_abs_self _)⟩
  let l := Nat.find h
  have hl : ∀ n : ℕ, n ≥ m → f n > a - l • ε := Nat.find_spec h
  have hl0 : l ≠ 0 := fun hl0 ↦
    not_lt_of_ge (ham m le_rfl)
      (lt_of_lt_of_le (by have := hl m (le_refl m); simpa [hl0] using this) (le_abs_self (f m)))
  obtain ⟨i, hi⟩ := not_forall.1 (Nat.find_min h (Nat.pred_lt hl0))
  rw [Classical.not_imp, not_lt] at hi
  exists i
  intro j hj
  have hfij : f j ≤ f i := (Nat.rel_of_forall_rel_succ_of_le_of_le (· ≥ ·) hnm hi.1 hj).le
  rw [abs_of_nonpos (sub_nonpos.2 hfij), neg_sub, sub_lt_iff_lt_add']
  calc
    f i ≤ a - Nat.pred l • ε := hi.2
    _ = a - l • ε + ε := by
      conv =>
        rhs
        rw [← Nat.succ_pred_eq_of_pos (Nat.pos_of_ne_zero hl0), succ_nsmul, sub_add,
          add_sub_cancel_right]
    _ < f j + ε := by gcongr; exact hl _ <| hi.1.trans hj