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 : ℕ → β
a : ℕ → α
n : ℕ
hm : ∀ (m : ℕ), n ≤ m → abv (f m) ≤ a m
i k : ℕ
hi :
  abv (HAdd.hAdd (α := β) (∑ i ∈ range (k + max n i), f i) (-∑ i ∈ range (max n i), f i)) ≤
    HAdd.hAdd (α := α) (∑ k ∈ range (k + max n i), a k) (-∑ k ∈ range (max n i), a k)
⊢ abv (f (k + max n i) + HAdd.hAdd (α := β) (∑ x ∈ range (k + max n i), f x) (-∑ x ∈ range (max n i), f x)) ≤
    a (k + max n i) + HAdd.hAdd (α := α) (∑ x ∈ range (k + max n i), a x) (-∑ x ∈ range (max n i), a x)
have succ : abv (f (k + max n i)) + abv (HAdd.hAdd (α := β) (∑ x ∈ range (k + max n i), f x) (-∑ x ∈ range (max n i), f x)) ≤
  a (k + max n i) + HAdd.hAdd (α := α) (∑ x ∈ range (k + max n i), a x) (-∑ x ∈ range (max n i), a x)
Tactic: grw [abv_add abv, hm _ (by omega), hi]
-- 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 : ℕ → β
a : ℕ → α
n : ℕ
hm : ∀ (m : ℕ), n ≤ m → abv (f m) ≤ a m
i k : ℕ
hi :
  abv (HAdd.hAdd (α := β) (∑ i ∈ range (k + max n i), f i) (-∑ i ∈ range (max n i), f i)) ≤
    HAdd.hAdd (α := α) (∑ k ∈ range (k + max n i), a k) (-∑ k ∈ range (max n i), a k)
succ :
  abv (f (k + max n i)) + abv (HAdd.hAdd (α := β) (∑ x ∈ range (k + max n i), f x) (-∑ x ∈ range (max n i), f x)) ≤
    a (k + max n i) + HAdd.hAdd (α := α) (∑ x ∈ range (k + max n i), a x) (-∑ x ∈ range (max n i), a x)
⊢ abv (f (k + max n i) + HAdd.hAdd (α := β) (∑ x ∈ range (k + max n i), f x) (-∑ x ∈ range (max n i), f x)) ≤
    a (k + max n i) + HAdd.hAdd (α := α) (∑ x ∈ range (k + max n i), a x) (-∑ x ∈ range (max n i), a x)
have succ₁ : a (k + max n i) + abv (HAdd.hAdd (α := β) (∑ x ∈ range (k + max n i), f x) (-∑ x ∈ range (max n i), f x)) ≤
  a (k + max n i) + HAdd.hAdd (α := α) (∑ x ∈ range (k + max n i), a x) (-∑ x ∈ range (max n i), a x)
Tactic: grw [abv_add abv, hm _ (by omega), hi]
-- 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 : ℕ → β
a : ℕ → α
n : ℕ
hm : ∀ (m : ℕ), n ≤ m → abv (f m) ≤ a m
i k : ℕ
hi :
  abv (HAdd.hAdd (α := β) (∑ i ∈ range (k + max n i), f i) (-∑ i ∈ range (max n i), f i)) ≤
    HAdd.hAdd (α := α) (∑ k ∈ range (k + max n i), a k) (-∑ k ∈ range (max n i), a k)
succ :
  abv (f (k + max n i)) + abv (HAdd.hAdd (α := β) (∑ x ∈ range (k + max n i), f x) (-∑ x ∈ range (max n i), f x)) ≤
    a (k + max n i) + HAdd.hAdd (α := α) (∑ x ∈ range (k + max n i), a x) (-∑ x ∈ range (max n i), a x)
succ₁ :
  a (k + max n i) + abv (HAdd.hAdd (α := β) (∑ x ∈ range (k + max n i), f x) (-∑ x ∈ range (max n i), f x)) ≤
    a (k + max n i) + HAdd.hAdd (α := α) (∑ x ∈ range (k + max n i), a x) (-∑ x ∈ range (max n i), a x)
⊢ abv (f (k + max n i) + HAdd.hAdd (α := β) (∑ x ∈ range (k + max n i), f x) (-∑ x ∈ range (max n i), f x)) ≤
    a (k + max n i) + HAdd.hAdd (α := α) (∑ x ∈ range (k + max n i), a x) (-∑ x ∈ range (max n i), a x)
have succ₂ : a (k + max n i) + HAdd.hAdd (α := α) (∑ k ∈ range (k + max n i), a k) (-∑ k ∈ range (max n i), a k) ≤
  a (k + max n i) + HAdd.hAdd (α := α) (∑ k ∈ range (k + max n i), a k) (-∑ k ∈ range (max n i), a k)
Tactic: grw [abv_add abv, hm _ (by omega), hi]
-- 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 : ℕ → β
a : ℕ → α
n : ℕ
hm : ∀ (m : ℕ), n ≤ m → abv (f m) ≤ a m
i k : ℕ
⊢ abv (HSub.hSub (α := β) (∑ i ∈ range (k + max n i), f i) (∑ i ∈ range (max n i), f i)) ≤
    HSub.hSub (α := α) (∑ k ∈ range (k + max n i), a k) (∑ k ∈ range (max n i), a k)
have zero : abv (HSub.hSub (α := β) (∑ i ∈ range (0 + max n i), f i) (∑ i ∈ range (max n i), f i)) ≤
  HSub.hSub (α := α) (∑ k ∈ range (0 + max n i), a k) (∑ k ∈ range (max n i), a k)
Tactic: induction k with
  | zero => simp [abv_zero abv]
  | succ k hi =>
    simp only [Nat.succ_add, Nat.succ_eq_add_one, Finset.sum_range_succ_comm]
    simp only [add_assoc, sub_eq_add_neg]
    simp only [sub_eq_add_neg] at hi
    grw [abv_add abv, hm _ (by omega), hi]
Cleared hypotheses: k
-- 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 : ℕ → β
a : ℕ → α
n : ℕ
hm : ∀ (m : ℕ), n ≤ m → abv (f m) ≤ a m
i k : ℕ
zero :
  abv (HSub.hSub (α := β) (∑ i ∈ range (0 + max n i), f i) (∑ i ∈ range (max n i), f i)) ≤
    HSub.hSub (α := α) (∑ k ∈ range (0 + max n i), a k) (∑ k ∈ range (max n i), a k)
⊢ abv (HSub.hSub (α := β) (∑ i ∈ range (k + max n i), f i) (∑ i ∈ range (max n i), f i)) ≤
    HSub.hSub (α := α) (∑ k ∈ range (k + max n i), a k) (∑ k ∈ range (max n i), a k)
have succ : ∀ (k : ℕ)
  (hi :
    abv (HSub.hSub (α := β) (∑ i ∈ range (k + max n i), f i) (∑ i ∈ range (max n i), f i)) ≤
      HSub.hSub (α := α) (∑ k ∈ range (k + max n i), a k) (∑ k ∈ range (max n i), a k)),
  abv (HSub.hSub (α := β) (∑ i ∈ range (k + 1 + max n i), f i) (∑ i ∈ range (max n i), f i)) ≤
    HSub.hSub (α := α) (∑ k ∈ range (k + 1 + max n i), a k) (∑ k ∈ range (max n i), a k)
Tactic: induction k with
  | zero => simp [abv_zero abv]
  | succ k hi =>
    simp only [Nat.succ_add, Nat.succ_eq_add_one, Finset.sum_range_succ_comm]
    simp only [add_assoc, sub_eq_add_neg]
    simp only [sub_eq_add_neg] at hi
    grw [abv_add abv, hm _ (by omega), hi]
Cleared hypotheses: k
-- 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 < ε
⊢ ∃ (i : ℕ),
    ∀ j ≥ i,
      abv
          (HMul.hMul (α := β) (∑ k ∈ range j, f k) (∑ k ∈ range j, g k) -
            ∑ n ∈ range j, ∑ m ∈ range (n + 1), f m * g (n - m)) <
        ε
have let : ∀ (P : α) (hP : ∀ (i : ℕ), |∑ n ∈ range i, abv (f n)| < P),
  ∃ (i : ℕ),
    ∀ j ≥ i,
      abv
          (HMul.hMul (α := β) (∑ k ∈ range j, f k) (∑ k ∈ range j, g k) -
            ∑ n ∈ range j, ∑ m ∈ range (n + 1), f m * g (n - m)) <
        ε
Tactic: let ⟨P, hP⟩ := ha.bounded
-- 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
⊢ ∃ (i : ℕ),
    ∀ j ≥ i,
      abv
          (HMul.hMul (α := β) (∑ k ∈ range j, f k) (∑ k ∈ range j, g k) -
            ∑ n ∈ range j, ∑ m ∈ range (n + 1), f m * g (n - m)) <
        ε
have let : ∀ (Q : α) (hQ : ∀ (i : ℕ), abv (∑ n ∈ range i, g n) < Q),
  ∃ (i : ℕ),
    ∀ j ≥ i,
      abv
          (HMul.hMul (α := β) (∑ k ∈ range j, f k) (∑ k ∈ range j, g k) -
            ∑ n ∈ range j, ∑ m ∈ range (n + 1), f m * g (n - m)) <
        ε
Tactic: let ⟨Q, hQ⟩ := hb.bounded
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.BigOperators (hypothesis)
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
⊢ ∃ (i : ℕ),
    ∀ j ≥ i,
      abv
          (HMul.hMul (α := β) (∑ k ∈ range j, f k) (∑ k ∈ range j, g k) -
            ∑ n ∈ range j, ∑ m ∈ range (n + 1), f m * g (n - m)) <
        ε
have hP0 : 0 < P
Tactic: have hP0 : 0 < P := lt_of_le_of_lt (abs_nonneg _) (hP 0)
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.BigOperators (hypothesis)
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
⊢ ∃ (i : ℕ),
    ∀ j ≥ i,
      abv
          (HMul.hMul (α := β) (∑ k ∈ range j, f k) (∑ k ∈ range j, g k) -
            ∑ n ∈ range j, ∑ m ∈ range (n + 1), f m * g (n - m)) <
        ε
have hPε0 : 0 < ε / (2 * P)
Tactic: have hPε0 : 0 < ε / (2 * P) := div_pos ε0 (mul_pos (show (2 : α) > 0 by simp) hP0)
-- 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)
⊢ ∃ (i : ℕ),
    ∀ j ≥ i,
      abv
          (HMul.hMul (α := β) (∑ k ∈ range j, f k) (∑ k ∈ range j, g k) -
            ∑ n ∈ range j, ∑ m ∈ range (n + 1), f m * g (n - m)) <
        ε
have let : ∀ (N : ℕ) (hN : ∀ j ≥ N, ∀ k ≥ N, abv (HSub.hSub (α := β) (∑ n ∈ range j, g n) (∑ n ∈ range k, g n)) < ε / (2 * P)),
  ∃ (i : ℕ),
    ∀ j ≥ i,
      abv
          (HMul.hMul (α := β) (∑ k ∈ range j, f k) (∑ k ∈ range j, g k) -
            ∑ n ∈ range j, ∑ m ∈ range (n + 1), f m * g (n - m)) <
        ε
Tactic: let ⟨N, hN⟩ := hb.cauchy₂ hPε0
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.BigOperators (hypothesis)
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)
⊢ ∃ (i : ℕ),
    ∀ j ≥ i,
      abv
          (HMul.hMul (α := β) (∑ k ∈ range j, f k) (∑ k ∈ range j, g k) -
            ∑ n ∈ range j, ∑ m ∈ range (n + 1), f m * g (n - m)) <
        ε
have hQε0 : 0 < ε / (4 * Q)
Tactic: have hQε0 : 0 < ε / (4 * Q) :=
    div_pos ε0 (mul_pos (show (0 : α) < 4 by simp) (lt_of_le_of_lt (abv_nonneg _ _) (hQ 0)))
-- 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)
⊢ ∃ (i : ℕ),
    ∀ j ≥ i,
      abv
          (HMul.hMul (α := β) (∑ k ∈ range j, f k) (∑ k ∈ range j, g k) -
            ∑ n ∈ range j, ∑ m ∈ range (n + 1), f m * g (n - m)) <
        ε
have let : ∀ (M : ℕ)
  (hM : ∀ j ≥ M, ∀ k ≥ M, |HSub.hSub (α := α) (∑ n ∈ range j, abv (f n)) (∑ n ∈ range k, abv (f n))| < ε / (4 * Q)),
  ∃ (i : ℕ),
    ∀ j ≥ i,
      abv
          (HMul.hMul (α := β) (∑ k ∈ range j, f k) (∑ k ∈ range j, g k) -
            ∑ n ∈ range j, ∑ m ∈ range (n + 1), f m * g (n - m)) <
        ε
Tactic: let ⟨M, hM⟩ := ha.cauchy₂ hQε0
-- 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)
⊢ ∃ (i : ℕ),
    ∀ j ≥ i,
      abv
          (HMul.hMul (α := β) (∑ k ∈ range j, f k) (∑ k ∈ range j, g k) -
            ∑ n ∈ range j, ∑ m ∈ range (n + 1), f m * g (n - m)) <
        ε
have refine : ∀ (K : ℕ) (hK : K ≥ 2 * (max N M + 1)),
  abv
      (HMul.hMul (α := β) (∑ k ∈ range K, f k) (∑ k ∈ range K, g k) -
        ∑ n ∈ range K, ∑ m ∈ range (n + 1), f m * g (n - m)) <
    ε
Tactic: refine ⟨2 * (max N M + 1), fun K hK ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.BigOperators (hypothesis)
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)
⊢ abv
      (HMul.hMul (α := β) (∑ k ∈ range K, f k) (∑ k ∈ range K, g k) -
        ∑ n ∈ range K, ∑ m ∈ range (n + 1), f m * g (n - m)) <
    ε
have 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)
Tactic: have h₁ :
    (∑ m ∈ range K, ∑ k ∈ range (m + 1), f k * g (m - k)) =
      ∑ m ∈ range K, ∑ n ∈ range (K - m), f m * g n := by
    simpa using sum_range_diag_flip K fun m n ↦ f m * g n
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.BigOperators (hypothesis)
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)
⊢ abv
      (HMul.hMul (α := β) (∑ k ∈ range K, f k) (∑ k ∈ range K, g k) -
        ∑ n ∈ range K, ∑ m ∈ range (n + 1), f m * g (n - m)) <
    ε
have 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
Tactic: have h₂ :
    (fun i ↦ ∑ k ∈ range (K - i), f i * g k) = fun i ↦ f i * ∑ k ∈ range (K - i), g k := by
    simp [Finset.mul_sum]
-- 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
⊢ ∑ 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)
have rw : Eq.{u_2 + 1} (α := β) (∑ i ∈ range K, f i * ∑ k ∈ range (K - i), g k)
  (∑ x ∈ range K, (f x * HSub.hSub (α := β) (∑ k ∈ range (K - x), g k) (∑ k ∈ range K, g k) + f x * ∑ k ∈ range K, g k))
Tactic: rw [← sum_add_distrib]
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.BigOperators (hypothesis)
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
⊢ abv
      (HMul.hMul (α := β) (∑ k ∈ range K, f k) (∑ k ∈ range K, g k) -
        ∑ n ∈ range K, ∑ m ∈ range (n + 1), f m * g (n - m)) <
    ε
have 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)
Tactic: have h₃ :
    ∑ i ∈ range K, f i * ∑ k ∈ range (K - i), g k =
      ∑ i ∈ range K, f i * (∑ k ∈ range (K - i), g k - ∑ k ∈ range K, g k) +
        ∑ i ∈ range K, f i * ∑ k ∈ range K, g k := by
    rw [← sum_add_distrib]; simp [(mul_add _ _ _).symm]
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.BigOperators (hypothesis)
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)
⊢ abv
      (HMul.hMul (α := β) (∑ k ∈ range K, f k) (∑ k ∈ range K, g k) -
        ∑ n ∈ range K, ∑ m ∈ range (n + 1), f m * g (n - m)) <
    ε
have two_mul_two : 4 = HMul.hMul (α := α) 2 2
Tactic: have two_mul_two : (4 : α) = 2 * 2 := by norm_num
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.BigOperators (hypothesis)
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
⊢ abv
      (HMul.hMul (α := β) (∑ k ∈ range K, f k) (∑ k ∈ range K, g k) -
        ∑ n ∈ range K, ∑ m ∈ range (n + 1), f m * g (n - m)) <
    ε
have hQ0 : Q ≠ 0
Tactic: have hQ0 : Q ≠ 0 := fun h ↦ by simp [h] at hQε0
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.BigOperators (hypothesis)
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
⊢ abv
      (HMul.hMul (α := β) (∑ k ∈ range K, f k) (∑ k ∈ range K, g k) -
        ∑ n ∈ range K, ∑ m ∈ range (n + 1), f m * g (n - m)) <
    ε
have h2Q0 : 2 * Q ≠ 0
Tactic: have h2Q0 : 2 * Q ≠ 0 := mul_ne_zero two_ne_zero hQ0