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)
⊢ 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:
simp [Finset.mul_sum]

Premises used: Finset.mul_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)
⊢ 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]
-- 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
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))
⊢ ∑ 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:
rw [← sum_add_distrib]

Premises used: Finset.sum_add_distrib
-- 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
⊢ 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:
simp [(mul_add _ _ _).symm]

Premises used: mul_add, Eq.symm
-- 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
⊢ ∑ 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]
-- 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)
⊢ 4 = HMul.hMul (α := α) 2 2

Tactic:
norm_num
-- 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)
⊢ 4 = HMul.hMul (α := α) 2 2

Tactic:
have two_mul_two : (4 : α) = 2 * 2 := by norm_num
-- 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
h : Q = 0
⊢ False

Tactic:
simp [h] at hQε0
-- 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
⊢ Q ≠ 0

Tactic:
have hQ0 : Q ≠ 0 := fun h ↦ by simp [h] at hQε0
-- 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
⊢ 2 * Q ≠ 0

Tactic:
have h2Q0 : 2 * Q ≠ 0 := mul_ne_zero two_ne_zero hQ0
-- 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
rw : ε / 2 / P * P + ε / (4 * Q) * (2 * Q) = ε
rw₁ : ε / 2 + ε / (4 * Q) * (2 * Q) = ε
rw₂ : ε / 2 + ε / (HMul.hMul (α := α) 2 2 * Q) * (2 * Q) = ε
rw₃ : ε / 2 + ε / (2 * (2 * Q)) * (2 * Q) = ε
rw₄ : ε / 2 + ε / 2 / (2 * Q) * (2 * Q) = ε
rw₅ : ε / 2 + ε / 2 = ε
rw₆ rw₇ : ε = ε
⊢ ε / (2 * P) * P + ε / (4 * Q) * (2 * Q) = ε

Tactic:
rw [← div_div, div_mul_cancel₀ _ (Ne.symm (ne_of_lt hP0)), two_mul_two, mul_assoc, ← div_div,
      div_mul_cancel₀ _ h2Q0, add_halves]

Premises used: div_mul_cancel₀, add_halves, mul_assoc, Ne.symm, div_div, ne_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
⊢ ε / (2 * P) * P + ε / (4 * Q) * (2 * Q) = ε

Tactic:
have hε : ε / (2 * P) * P + ε / (4 * Q) * (2 * Q) = ε := by
    rw [← div_div, div_mul_cancel₀ _ (Ne.symm (ne_of_lt hP0)), two_mul_two, mul_assoc, ← div_div,
      div_mul_cancel₀ _ h2Q0, add_halves]
-- 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) = ε
rw : max N M + 1 < max N M + 1 + (max N M + 1)
⊢ max N M + 1 < 2 * (max N M + 1)

Tactic:
rw [two_mul]

Premises used: two_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) = ε
⊢ max N M + 1 < max N M + 1 + (max N M + 1)

Tactic:
lt_add_of_pos_left _ (Nat.succ_pos _)

Premises used: Nat.succ_pos, lt_add_of_pos_left
-- 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) = ε
⊢ max N M + 1 < max N M + 1 + (max N M + 1)

Tactic:
exact lt_add_of_pos_left _ (Nat.succ_pos _)

Premises used: Nat.succ_pos, lt_add_of_pos_left
-- 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) = ε
⊢ max N M + 1 < K

Tactic:
have hNMK : max N M + 1 < K :=
    lt_of_lt_of_le (by rw [two_mul]; exact lt_add_of_pos_left _ (Nat.succ_pos _)) hK