awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Order.CauSeq.BigOperators
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
refine : ∑ i ∈ range K, abv (f i * HSub.hSub (α := β) (∑ k ∈ range (K - i), g k) (∑ k ∈ range K, g k)) < ε
⊢ abv (∑ i ∈ range K, f i * HSub.hSub (α := β) (∑ k ∈ range (K - i), g k) (∑ k ∈ range K, g k)) < ε

Tactic:
refine lt_of_le_of_lt (IsAbsoluteValue.abv_sum _ _ _) ?_

Premises used: lt_of_le_of_lt, IsAbsoluteValue.abv_sum
-- Module: Mathlib.Algebra.Order.CauSeq.BigOperators
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
this :
  ∑ i ∈ range (max N M + 1), abv (f i) * abv (HSub.hSub (α := β) (∑ k ∈ range (K - i), g k) (∑ k ∈ range K, g k)) +
      HSub.hSub (α := α)
        (∑ i ∈ range K, 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) * abv (HSub.hSub (α := β) (∑ k ∈ range (K - i), g k) (∑ k ∈ range K, g k))) <
    ε / (2 * P) * P + ε / (4 * Q) * (2 * Q)
⊢ ∑ i ∈ range (max N M + 1), abv (f i) * abv (HSub.hSub (α := β) (∑ k ∈ range (K - i), g k) (∑ k ∈ range K, g k)) +
      HSub.hSub (α := α)
        (∑ i ∈ range K, 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) * abv (HSub.hSub (α := β) (∑ k ∈ range (K - i), g k) (∑ k ∈ range K, g k))) <
    ε

Tactic:
rw [hε] at this
-- Module: Mathlib.Algebra.Order.CauSeq.BigOperators
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
this :
  ∑ i ∈ range (max N M + 1), abv (f i) * abv (HSub.hSub (α := β) (∑ k ∈ range (K - i), g k) (∑ k ∈ range K, g k)) +
      HSub.hSub (α := α)
        (∑ i ∈ range K, 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) * abv (HSub.hSub (α := β) (∑ k ∈ range (K - i), g k) (∑ k ∈ range K, g k))) <
    ε
⊢ ∑ i ∈ range K, abv (f i * HSub.hSub (α := β) (∑ k ∈ range (K - i), g k) (∑ k ∈ range K, g k)) < ε

Tactic:
simpa [abv_mul abv] using this

Premises used: IsAbsoluteValue.abv_mul
-- Module: Mathlib.Algebra.Order.CauSeq.BigOperators
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 :
  ∑ i ∈ range (max N M + 1), abv (f i) * abv (HSub.hSub (α := β) (∑ k ∈ range (K - i), g k) (∑ k ∈ range K, g k)) +
      HSub.hSub (α := α)
        (∑ i ∈ range K, 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) * abv (HSub.hSub (α := β) (∑ k ∈ range (K - i), g k) (∑ k ∈ range K, g k))) <
    ε / (2 * P) * P + ε / (4 * Q) * (2 * Q)
⊢ ∑ i ∈ range K, abv (f i * HSub.hSub (α := β) (∑ k ∈ range (K - i), g k) (∑ k ∈ range K, g k)) < ε

Tactic:
suffices
    (∑ i ∈ range (max N M + 1),
          abv (f i) * abv ((∑ k ∈ range (K - i), g k) - ∑ k ∈ range K, g k)) +
        ((∑ i ∈ range K, abv (f i) * abv ((∑ k ∈ range (K - i), g k) - ∑ k ∈ range K, g k)) -
          ∑ i ∈ range (max N M + 1),
            abv (f i) * abv ((∑ k ∈ range (K - i), g k) - ∑ k ∈ range K, g k)) <
      ε / (2 * P) * P + ε / (4 * Q) * (2 * Q) by
    rw [hε] at this
    simpa [abv_mul abv] using this
-- Module: Mathlib.Algebra.Order.CauSeq.BigOperators
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
h₄ :
  ∑ i ∈ range (max N M + 1), abv (f i) * abv (HSub.hSub (α := β) (∑ k ∈ range (K - i), g k) (∑ k ∈ range K, g k)) <
    ε / (2 * P) * P
h₅ :
  HSub.hSub (α := α)
      (∑ i ∈ range K, 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) * abv (HSub.hSub (α := β) (∑ k ∈ range (K - i), g k) (∑ k ∈ range K, g k))) <
    ε / (4 * Q) * (2 * Q)
⊢ ∑ i ∈ range (max N M + 1), abv (f i) * abv (HSub.hSub (α := β) (∑ k ∈ range (K - i), g k) (∑ k ∈ range K, g k)) +
      HSub.hSub (α := α)
        (∑ i ∈ range K, 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) * abv (HSub.hSub (α := β) (∑ k ∈ range (K - i), g k) (∑ k ∈ range K, g k))) <
    ε / (2 * P) * P + ε / (4 * Q) * (2 * Q)

Tactic:
gcongr
-- Module: Mathlib.Algebra.Order.CauSeq.BigOperators
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
rw : ε / (2 * P) * ∑ i ∈ range (max N M + 1), abv (f i) < ε / (2 * P) * P
⊢ ∑ i ∈ range (max N M + 1), abv (f i) * (ε / (2 * P)) < ε / (2 * P) * P

Tactic:
rw [← sum_mul, mul_comm]

Premises used: mul_comm, Finset.sum_mul
-- Module: Mathlib.Algebra.Order.CauSeq.BigOperators
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
ha₁ : 0 < ε / (2 * P)
⊢ ε / (2 * P) * ∑ i ∈ range (max N M + 1), abv (f i) < ε / (2 * P) * P

Tactic:
gcongr
-- Module: Mathlib.Algebra.Order.CauSeq.BigOperators
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 ∈ range (max N M + 1), abv (f i) * abv (HSub.hSub (α := β) (∑ k ∈ range (K - i), g k) (∑ k ∈ range K, g k)) <
    ε / (2 * P) * P

Tactic:
exact lt_of_le_of_lt hsumlesum
        (by rw [← sum_mul, mul_comm]; gcongr)

Premises used: lt_of_le_of_lt
-- Module: Mathlib.Algebra.Order.CauSeq.BigOperators
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
h₄ :
  ∑ 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)
⊢ HSub.hSub (α := α)
      (∑ i ∈ range K, 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) * abv (HSub.hSub (α := β) (∑ k ∈ range (K - i), g k) (∑ k ∈ range K, g k))) <
    ε / (4 * Q) * (2 * Q)

Tactic:
rw [sum_range_sub_sum_range (le_of_lt hNMK)]

Premises used: le_of_lt, Finset.sum_range_sub_sum_range
-- Module: Mathlib.Algebra.Order.CauSeq.BigOperators
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
h :
  ∀ i ∈ {i ∈ range K | max N M + 1 ≤ i},
    abv (HSub.hSub (α := β) (∑ k ∈ range (K - i), g k) (∑ k ∈ range K, g k)) ≤ 2 * Q
⊢ 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))

Tactic:
gcongr
-- Module: Mathlib.Algebra.Order.CauSeq.BigOperators
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 : ℕ
h_1 : i ∈ {i ∈ range K | max N M + 1 ≤ i}
h : abv (HAdd.hAdd (α := β) (∑ k ∈ range (K - i), g k) (-∑ k ∈ range K, g k)) ≤ 2 * Q
⊢ abv (HSub.hSub (α := β) (∑ k ∈ range (K - i), g k) (∑ k ∈ range K, g k)) ≤ 2 * Q

Tactic:
rw [sub_eq_add_neg]

Premises used: sub_eq_add_neg