awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.Basic (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b : CauSeq α abs
ε : α
ε0 : 0 < ε
i : ℕ
h : ∀ j ≥ i, ε ≤ (↑(a - b) : ℕ → α) j
ε_1 : α
h_1 : ε_1 > 0
⊢ ∃ (i : ℕ), ∀ j ≥ i, |(↑(a ⊓ b - b) : ℕ → α) j| < ε_1
have inl : ∀ (j : ℕ) (hj : j ≥ i), |(↑(a ⊓ b - b) : ℕ → α) j| < ε_1
Tactic: refine ⟨i, fun j hj => ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.Basic (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b : CauSeq α abs
ε : α
ε0 : 0 < ε
i : ℕ
h : ∀ j ≥ i, ε ≤ (↑(a - b) : ℕ → α) j
ε_1 : α
h_1 : ε_1 > 0
j : ℕ
hj : j ≥ i
⊢ |(↑(a ⊓ b - b) : ℕ → α) j| < ε_1
have inl : |min ((↑a : ℕ → α) j) ((↑b : ℕ → α) j) - (↑b : ℕ → α) j| < ε_1
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.Basic (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b : CauSeq α abs
ε : α
ε0 : 0 < ε
i : ℕ
h : ∀ j ≥ i, ε ≤ (↑(a - b) : ℕ → α) j
ε_1 : α
h_1 : ε_1 > 0
j : ℕ
hj : j ≥ i
⊢ |min ((↑a : ℕ → α) j) ((↑b : ℕ → α) j) - (↑b : ℕ → α) j| < ε_1
have inl : |min ((↑a : ℕ → α) j - (↑b : ℕ → α) j) ((↑b : ℕ → α) j - (↑b : ℕ → α) j)| < ε_1
Tactic: rw [← min_sub_sub_right]
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.Basic (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b : CauSeq α abs
ε : α
ε0 : 0 < ε
i : ℕ
h : ∀ j ≥ i, ε ≤ (↑(a - b) : ℕ → α) j
ε_1 : α
h_1 : ε_1 > 0
j : ℕ
hj : j ≥ i
⊢ |min ((↑a : ℕ → α) j - (↑b : ℕ → α) j) ((↑b : ℕ → α) j - (↑b : ℕ → α) j)| < ε_1
have inl : 0 ≤ (↑a : ℕ → α) j - (↑b : ℕ → α) j
Tactic: rwa [sub_self, min_eq_right, abs_zero]
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.Basic (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b : CauSeq α abs
h : b ≈ a
⊢ a ⊓ b ≈ b
have inr : b ⊓ b ≈ b
Tactic: refine Setoid.trans (inf_equiv_inf (Setoid.symm h) (Setoid.refl _)) ?_
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.Basic (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b : CauSeq α abs
h : b ≈ a
⊢ b ⊓ b ≈ b
have inr : (equiv : CauSeq α abs → CauSeq α abs → Prop) b b
Tactic: rw [CauSeq.inf_idem]
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.Basic (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b c : CauSeq α abs
ha : a ≤ c
hb : b ≤ c
⊢ a ⊔ b ≤ c
have inl : ∀ (ha : a < c), a ⊔ b ≤ c
Tactic: obtain ha | ha := ha
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.Basic (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b c : CauSeq α abs
ha : a ≤ c
hb : b ≤ c
inl : ∀ (ha : a < c), a ⊔ b ≤ c
⊢ a ⊔ b ≤ c
have inr : ∀ (ha : a ≈ c), a ⊔ b ≤ c
Tactic: obtain ha | ha := ha
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.Basic (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b c : CauSeq α abs
hb : b ≤ c
ha : a < c
⊢ a ⊔ b ≤ c
have inl : ∀ (hb : b < c), a ⊔ b ≤ c
Tactic: obtain hb | hb := hb
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.Basic (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b c : CauSeq α abs
hb : b ≤ c
ha : a < c
inl : ∀ (hb : b < c), a ⊔ b ≤ c
⊢ a ⊔ b ≤ c
have inl₁ : ∀ (hb : b ≈ c), a ⊔ b ≤ c
Tactic: obtain hb | hb := hb
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.Basic (hypothesis)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b c : CauSeq α abs
ha : a < c
hb : b ≈ c
⊢ a ⊔ b ≤ c
have ha₁ : a ≤ b
Tactic: replace ha := le_of_le_of_eq ha.le (Setoid.symm hb)
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.Basic (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b c : CauSeq α abs
hb : b ≈ c
ha : a ≤ b
⊢ a ⊔ b ≤ c
have inl : a ⊔ b ≈ b
Tactic: refine le_of_le_of_eq (Or.inr ?_) hb
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.Basic (hypothesis)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b c : CauSeq α abs
hb : b ≤ c
ha : a ≈ c
⊢ a ⊔ b ≤ c
have hb₁ : b ≤ a
Tactic: replace hb := le_of_le_of_eq hb (Setoid.symm ha)
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.Basic (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b c : CauSeq α abs
ha : a ≈ c
hb : b ≤ a
⊢ a ⊔ b ≤ c
have inr : a ⊔ b ≈ a
Tactic: refine le_of_le_of_eq (Or.inr ?_) ha
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.Basic (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b c : CauSeq α abs
hb : a ≤ b
hc : a ≤ c
⊢ a ≤ b ⊓ c
have inl : ∀ (hb : a < b), a ≤ b ⊓ c
Tactic: obtain hb | hb := hb
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.Basic (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b c : CauSeq α abs
hb : a ≤ b
hc : a ≤ c
inl : ∀ (hb : a < b), a ≤ b ⊓ c
⊢ a ≤ b ⊓ c
have inr : ∀ (hb : a ≈ b), a ≤ b ⊓ c
Tactic: obtain hb | hb := hb
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.Basic (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b c : CauSeq α abs
hc : a ≤ c
hb : a < b
⊢ a ≤ b ⊓ c
have inl : ∀ (hc : a < c), a ≤ b ⊓ c
Tactic: obtain hc | hc := hc
Cleared hypotheses: hc
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.Basic (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b c : CauSeq α abs
hc : a ≤ c
hb : a < b
inl : ∀ (hc : a < c), a ≤ b ⊓ c
⊢ a ≤ b ⊓ c
have inl₁ : ∀ (hc : a ≈ c), a ≤ b ⊓ c
Tactic: obtain hc | hc := hc
Cleared hypotheses: hc
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.Basic (hypothesis)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b c : CauSeq α abs
hb : a < b
hc : a ≈ c
⊢ a ≤ b ⊓ c
have hb₁ : c ≤ b
Tactic: replace hb := le_of_eq_of_le (Setoid.symm hc) hb.le
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.Basic (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b c : CauSeq α abs
hc : a ≈ c
hb : c ≤ b
⊢ a ≤ b ⊓ c
have inl : c ≈ b ⊓ c
Tactic: refine le_of_eq_of_le hc (Or.inr ?_)
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.Basic (hypothesis)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b c : CauSeq α abs
hc : a ≤ c
hb : a ≈ b
⊢ a ≤ b ⊓ c
have hc₁ : b ≤ c
Tactic: replace hc := le_of_eq_of_le (Setoid.symm hb) hc
Cleared hypotheses: hc
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.Basic (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b c : CauSeq α abs
hb : a ≈ b
hc : b ≤ c
⊢ a ≤ b ⊓ c
have inr : b ≈ b ⊓ c
Tactic: refine le_of_eq_of_le hb (Or.inr ?_)
-- 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
hg : IsCauSeq.{u_1, u_1} (α := α) abs fun (n : ℕ) ↦ ∑ i ∈ range n, a i
ε : α
ε0 : ε > 0
⊢ ∃ (i : ℕ),
    ∀ j ≥ i,
      abv
          (HSub.hSub (α := β) ((fun (n : ℕ) ↦ (∑ i ∈ range n, f i : β)) j)
            ((fun (n : ℕ) ↦ (∑ i ∈ range n, f i : β)) i)) <
        ε
have obtain : ∀ (i : ℕ)
  (hi :
    ∀ j ≥ i,
      |HSub.hSub (α := α) ((fun (n : ℕ) ↦ (∑ i ∈ range n, a i : α)) j) ((fun (n : ℕ) ↦ (∑ i ∈ range n, a i : α)) i)| <
        ε / 2),
  ∃ (i : ℕ),
    ∀ j ≥ i,
      abv
          (HSub.hSub (α := β) ((fun (n : ℕ) ↦ (∑ i ∈ range n, f i : β)) j)
            ((fun (n : ℕ) ↦ (∑ i ∈ range n, f i : β)) i)) <
        ε
Tactic: obtain ⟨i, hi⟩ := hg (ε / 2) (div_pos ε0 (by simp))
-- 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
hg : IsCauSeq.{u_1, u_1} (α := α) abs fun (n : ℕ) ↦ ∑ i ∈ range n, a i
ε : α
ε0 : ε > 0
i : ℕ
hi :
  ∀ j ≥ i,
    |HSub.hSub (α := α) ((fun (n : ℕ) ↦ (∑ i ∈ range n, a i : α)) j) ((fun (n : ℕ) ↦ (∑ i ∈ range n, a i : α)) i)| <
      ε / 2
⊢ ∃ (i : ℕ),
    ∀ j ≥ i,
      abv
          (HSub.hSub (α := β) ((fun (n : ℕ) ↦ (∑ i ∈ range n, f i : β)) j)
            ((fun (n : ℕ) ↦ (∑ i ∈ range n, f i : β)) i)) <
        ε
have exists : ∀ j ≥ max n i,
  abv
      (HSub.hSub (α := β) ((fun (n : ℕ) ↦ (∑ i ∈ range n, f i : β)) j)
        ((fun (n : ℕ) ↦ (∑ i ∈ range n, f i : β)) (max n i))) <
    ε
Tactic: exists max n i
-- 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 : ℕ → β
a : ℕ → α
n : ℕ
hm : ∀ (m : ℕ), n ≤ m → abv (f m) ≤ a m
hg : IsCauSeq.{u_1, u_1} (α := α) abs fun (n : ℕ) ↦ ∑ i ∈ range n, a i
ε : α
ε0 : ε > 0
i : ℕ
hi :
  ∀ j ≥ i,
    |HSub.hSub (α := α) ((fun (n : ℕ) ↦ (∑ i ∈ range n, a i : α)) j) ((fun (n : ℕ) ↦ (∑ i ∈ range n, a i : α)) i)| <
      ε / 2
j : ℕ
ji : j ≥ max n i
⊢ abv
      (HSub.hSub (α := β) ((fun (n : ℕ) ↦ (∑ i ∈ range n, f i : β)) j)
        ((fun (n : ℕ) ↦ (∑ i ∈ range n, f i : β)) (max n i))) <
    ε
have hi₁ : |HSub.hSub (α := α) ((fun (n : ℕ) ↦ (∑ i ∈ range n, a i : α)) j) ((fun (n : ℕ) ↦ (∑ i ∈ range n, a i : α)) i)| < ε / 2
Tactic: have hi₁ := hi j (le_trans (le_max_right n i) ji)
-- 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 : ℕ → β
a : ℕ → α
n : ℕ
hm : ∀ (m : ℕ), n ≤ m → abv (f m) ≤ a m
hg : IsCauSeq.{u_1, u_1} (α := α) abs fun (n : ℕ) ↦ ∑ i ∈ range n, a i
ε : α
ε0 : ε > 0
i : ℕ
hi :
  ∀ j ≥ i,
    |HSub.hSub (α := α) ((fun (n : ℕ) ↦ (∑ i ∈ range n, a i : α)) j) ((fun (n : ℕ) ↦ (∑ i ∈ range n, a i : α)) i)| <
      ε / 2
j : ℕ
ji : j ≥ max n i
hi₁ :
  |HSub.hSub (α := α) ((fun (n : ℕ) ↦ (∑ i ∈ range n, a i : α)) j) ((fun (n : ℕ) ↦ (∑ i ∈ range n, a i : α)) i)| < ε / 2
⊢ abv
      (HSub.hSub (α := β) ((fun (n : ℕ) ↦ (∑ i ∈ range n, f i : β)) j)
        ((fun (n : ℕ) ↦ (∑ i ∈ range n, f i : β)) (max n i))) <
    ε
have hi₂ : |HSub.hSub (α := α) ((fun (n : ℕ) ↦ (∑ i ∈ range n, a i : α)) (max n i)) ((fun (n : ℕ) ↦ (∑ i ∈ range n, a i : α)) i)| <
  ε / 2
Tactic: have hi₂ := hi (max n i) (le_max_right n i)
-- 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 : ℕ → β
a : ℕ → α
n : ℕ
hm : ∀ (m : ℕ), n ≤ m → abv (f m) ≤ a m
hg : IsCauSeq.{u_1, u_1} (α := α) abs fun (n : ℕ) ↦ ∑ i ∈ range n, a i
ε : α
ε0 : ε > 0
i : ℕ
hi :
  ∀ j ≥ i,
    |HSub.hSub (α := α) ((fun (n : ℕ) ↦ (∑ i ∈ range n, a i : α)) j) ((fun (n : ℕ) ↦ (∑ i ∈ range n, a i : α)) i)| <
      ε / 2
j : ℕ
ji : j ≥ max n i
hi₁ :
  |HSub.hSub (α := α) ((fun (n : ℕ) ↦ (∑ i ∈ range n, a i : α)) j) ((fun (n : ℕ) ↦ (∑ i ∈ range n, a i : α)) i)| < ε / 2
hi₂ :
  |HSub.hSub (α := α) ((fun (n : ℕ) ↦ (∑ i ∈ range n, a i : α)) (max n i))
        ((fun (n : ℕ) ↦ (∑ i ∈ range n, a i : α)) i)| <
    ε / 2
⊢ abv
      (HSub.hSub (α := β) ((fun (n : ℕ) ↦ (∑ i ∈ range n, f i : β)) j)
        ((fun (n : ℕ) ↦ (∑ i ∈ range n, f i : β)) (max n i))) <
    ε
have sub_le : |HSub.hSub (α := α) (∑ k ∈ range j, a k) (∑ k ∈ range (max n i), a k)| ≤
  |HSub.hSub (α := α) (∑ k ∈ range j, a k) (∑ k ∈ range i, a k)| +
    |HSub.hSub (α := α) (∑ k ∈ range i, a k) (∑ k ∈ range (max n i), a k)|
Tactic: have sub_le :=
    abs_sub_le (∑ k ∈ range j, a k) (∑ k ∈ range i, a k) (∑ k ∈ range (max n i), a k)
-- 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 : ℕ → β
a : ℕ → α
n : ℕ
hm : ∀ (m : ℕ), n ≤ m → abv (f m) ≤ a m
hg : IsCauSeq.{u_1, u_1} (α := α) abs fun (n : ℕ) ↦ ∑ i ∈ range n, a i
ε : α
ε0 : ε > 0
i : ℕ
hi :
  ∀ j ≥ i,
    |HSub.hSub (α := α) ((fun (n : ℕ) ↦ (∑ i ∈ range n, a i : α)) j) ((fun (n : ℕ) ↦ (∑ i ∈ range n, a i : α)) i)| <
      ε / 2
j : ℕ
ji : j ≥ max n i
hi₁ :
  |HSub.hSub (α := α) ((fun (n : ℕ) ↦ (∑ i ∈ range n, a i : α)) j) ((fun (n : ℕ) ↦ (∑ i ∈ range n, a i : α)) i)| < ε / 2
hi₂ :
  |HSub.hSub (α := α) ((fun (n : ℕ) ↦ (∑ i ∈ range n, a i : α)) (max n i))
        ((fun (n : ℕ) ↦ (∑ i ∈ range n, a i : α)) i)| <
    ε / 2
sub_le :
  |HSub.hSub (α := α) (∑ k ∈ range j, a k) (∑ k ∈ range (max n i), a k)| ≤
    |HSub.hSub (α := α) (∑ k ∈ range j, a k) (∑ k ∈ range i, a k)| +
      |HSub.hSub (α := α) (∑ k ∈ range i, a k) (∑ k ∈ range (max n i), a k)|
⊢ abv
      (HSub.hSub (α := β) ((fun (n : ℕ) ↦ (∑ i ∈ range n, f i : β)) j)
        ((fun (n : ℕ) ↦ (∑ i ∈ range n, f i : β)) (max n i))) <
    ε
have this : |HSub.hSub (α := α) ((fun (n : ℕ) ↦ (∑ i ∈ range n, a i : α)) j) ((fun (n : ℕ) ↦ (∑ i ∈ range n, a i : α)) i)| +
    |HSub.hSub (α := α) ((fun (n : ℕ) ↦ (∑ i ∈ range n, a i : α)) (max n i))
        ((fun (n : ℕ) ↦ (∑ i ∈ range n, a i : α)) i)| <
  ε / 2 + ε / 2
Tactic: have := add_lt_add hi₁ hi₂
-- 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 : ℕ → β
a : ℕ → α
n : ℕ
hm : ∀ (m : ℕ), n ≤ m → abv (f m) ≤ a m
hg : IsCauSeq.{u_1, u_1} (α := α) abs fun (n : ℕ) ↦ ∑ i ∈ range n, a i
ε : α
ε0 : ε > 0
i : ℕ
hi :
  ∀ j ≥ i,
    |HSub.hSub (α := α) ((fun (n : ℕ) ↦ (∑ i ∈ range n, a i : α)) j) ((fun (n : ℕ) ↦ (∑ i ∈ range n, a i : α)) i)| <
      ε / 2
j : ℕ
ji : j ≥ max n i
hi₁ :
  |HSub.hSub (α := α) ((fun (n : ℕ) ↦ (∑ i ∈ range n, a i : α)) j) ((fun (n : ℕ) ↦ (∑ i ∈ range n, a i : α)) i)| < ε / 2
hi₂ :
  |HSub.hSub (α := α) ((fun (n : ℕ) ↦ (∑ i ∈ range n, a i : α)) (max n i))
        ((fun (n : ℕ) ↦ (∑ i ∈ range n, a i : α)) i)| <
    ε / 2
sub_le :
  |HSub.hSub (α := α) (∑ k ∈ range j, a k) (∑ k ∈ range (max n i), a k)| ≤
    |HSub.hSub (α := α) (∑ k ∈ range j, a k) (∑ k ∈ range i, a k)| +
      |HSub.hSub (α := α) (∑ k ∈ range i, a k) (∑ k ∈ range (max n i), a k)|
this :
  |HSub.hSub (α := α) ((fun (n : ℕ) ↦ (∑ i ∈ range n, a i : α)) j) ((fun (n : ℕ) ↦ (∑ i ∈ range n, a i : α)) i)| +
      |HSub.hSub (α := α) ((fun (n : ℕ) ↦ (∑ i ∈ range n, a i : α)) (max n i))
          ((fun (n : ℕ) ↦ (∑ i ∈ range n, a i : α)) i)| <
    ε / 2 + ε / 2
⊢ abv
      (HSub.hSub (α := β) ((fun (n : ℕ) ↦ (∑ i ∈ range n, f i : β)) j)
        ((fun (n : ℕ) ↦ (∑ i ∈ range n, f i : β)) (max n i))) <
    ε
have this₁ : |HSub.hSub (α := α) ((fun (n : ℕ) ↦ (∑ i ∈ range n, a i : α)) j) ((fun (n : ℕ) ↦ (∑ i ∈ range n, a i : α)) i)| +
    |HSub.hSub (α := α) ((fun (n : ℕ) ↦ (∑ i ∈ range n, a i : α)) i) (∑ k ∈ range (max n i), a k)| <
  ε
Tactic: rw [abs_sub_comm (∑ k ∈ range (max n i), a k), add_halves ε] at this
Cleared hypotheses: this
-- 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
hg : IsCauSeq.{u_1, u_1} (α := α) abs fun (n : ℕ) ↦ ∑ i ∈ range n, a i
ε : α
ε0 : ε > 0
i : ℕ
hi :
  ∀ j ≥ i,
    |HSub.hSub (α := α) ((fun (n : ℕ) ↦ (∑ i ∈ range n, a i : α)) j) ((fun (n : ℕ) ↦ (∑ i ∈ range n, a i : α)) i)| <
      ε / 2
j : ℕ
ji : j ≥ max n i
hi₁ :
  |HSub.hSub (α := α) ((fun (n : ℕ) ↦ (∑ i ∈ range n, a i : α)) j) ((fun (n : ℕ) ↦ (∑ i ∈ range n, a i : α)) i)| < ε / 2
hi₂ :
  |HSub.hSub (α := α) ((fun (n : ℕ) ↦ (∑ i ∈ range n, a i : α)) (max n i))
        ((fun (n : ℕ) ↦ (∑ i ∈ range n, a i : α)) i)| <
    ε / 2
sub_le :
  |HSub.hSub (α := α) (∑ k ∈ range j, a k) (∑ k ∈ range (max n i), a k)| ≤
    |HSub.hSub (α := α) (∑ k ∈ range j, a k) (∑ k ∈ range i, a k)| +
      |HSub.hSub (α := α) (∑ k ∈ range i, a k) (∑ k ∈ range (max n i), a k)|
this :
  |HSub.hSub (α := α) ((fun (n : ℕ) ↦ (∑ i ∈ range n, a i : α)) j) ((fun (n : ℕ) ↦ (∑ i ∈ range n, a i : α)) i)| +
      |HSub.hSub (α := α) ((fun (n : ℕ) ↦ (∑ i ∈ range n, a i : α)) i) (∑ k ∈ range (max n i), a k)| <
    ε
⊢ abv
      (HSub.hSub (α := β) ((fun (n : ℕ) ↦ (∑ i ∈ range n, f i : β)) j)
        ((fun (n : ℕ) ↦ (∑ i ∈ range n, f i : β)) (max n i))) <
    ε
have refine : abv
    (HSub.hSub (α := β) ((fun (n : ℕ) ↦ (∑ i ∈ range n, f i : β)) j)
      ((fun (n : ℕ) ↦ (∑ i ∈ range n, f i : β)) (max n i))) ≤
  HSub.hSub (α := α) (∑ k ∈ range j, a k) (∑ k ∈ range (max n i), a k)
Tactic: refine lt_of_le_of_lt (le_trans (le_trans ?_ (le_abs_self _)) sub_le) this
-- 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
hg : IsCauSeq.{u_1, u_1} (α := α) abs fun (n : ℕ) ↦ ∑ i ∈ range n, a i
ε : α
ε0 : ε > 0
i : ℕ
hi :
  ∀ j ≥ i,
    |HSub.hSub (α := α) ((fun (n : ℕ) ↦ (∑ i ∈ range n, a i : α)) j) ((fun (n : ℕ) ↦ (∑ i ∈ range n, a i : α)) i)| <
      ε / 2
j : ℕ
ji : j ≥ max n i
hi₁ :
  |HSub.hSub (α := α) ((fun (n : ℕ) ↦ (∑ i ∈ range n, a i : α)) j) ((fun (n : ℕ) ↦ (∑ i ∈ range n, a i : α)) i)| < ε / 2
hi₂ :
  |HSub.hSub (α := α) ((fun (n : ℕ) ↦ (∑ i ∈ range n, a i : α)) (max n i))
        ((fun (n : ℕ) ↦ (∑ i ∈ range n, a i : α)) i)| <
    ε / 2
sub_le :
  |HSub.hSub (α := α) (∑ k ∈ range j, a k) (∑ k ∈ range (max n i), a k)| ≤
    |HSub.hSub (α := α) (∑ k ∈ range j, a k) (∑ k ∈ range i, a k)| +
      |HSub.hSub (α := α) (∑ k ∈ range i, a k) (∑ k ∈ range (max n i), a k)|
this :
  |HSub.hSub (α := α) ((fun (n : ℕ) ↦ (∑ i ∈ range n, a i : α)) j) ((fun (n : ℕ) ↦ (∑ i ∈ range n, a i : α)) i)| +
      |HSub.hSub (α := α) ((fun (n : ℕ) ↦ (∑ i ∈ range n, a i : α)) i) (∑ k ∈ range (max n i), a k)| <
    ε
⊢ abv
      (HSub.hSub (α := β) ((fun (n : ℕ) ↦ (∑ i ∈ range n, f i : β)) j)
        ((fun (n : ℕ) ↦ (∑ i ∈ range n, f i : β)) (max n i))) ≤
    HSub.hSub (α := α) (∑ k ∈ range j, a k) (∑ k ∈ range (max n i), a k)
have generalize : ∀ (k : ℕ) (hk : j - max n i = k),
  abv
      (HSub.hSub (α := β) ((fun (n : ℕ) ↦ (∑ i ∈ range n, f i : β)) j)
        ((fun (n : ℕ) ↦ (∑ i ∈ range n, f i : β)) (max n i))) ≤
    HSub.hSub (α := α) (∑ k ∈ range j, a k) (∑ k ∈ range (max n i), a k)
Tactic: generalize hk : j - max n i = k
-- 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 : ℕ → β
a : ℕ → α
n : ℕ
hm : ∀ (m : ℕ), n ≤ m → abv (f m) ≤ a m
i j : ℕ
ji : j ≥ max n i
k : ℕ
hk : j - max n i = k
⊢ abv
      (HSub.hSub (α := β) ((fun (n : ℕ) ↦ (∑ i ∈ range n, f i : β)) j)
        ((fun (n : ℕ) ↦ (∑ i ∈ range n, f i : β)) (max n i))) ≤
    HSub.hSub (α := α) (∑ k ∈ range j, a k) (∑ k ∈ range (max n i), a k)
have hk₁ : j = k + max n i
Tactic: rw [tsub_eq_iff_eq_add_of_le ji] at hk
Cleared hypotheses: hk
-- 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 j : ℕ
ji : j ≥ max n i
k : ℕ
hk : j = k + max n i
⊢ abv
      (HSub.hSub (α := β) ((fun (n : ℕ) ↦ (∑ i ∈ range n, f i : β)) j)
        ((fun (n : ℕ) ↦ (∑ i ∈ range n, f i : β)) (max n i))) ≤
    HSub.hSub (α := α) (∑ k ∈ range j, a k) (∑ k ∈ range (max n i), a k)
have rw : abv
    (HSub.hSub (α := β) ((fun (n : ℕ) ↦ (∑ i ∈ range n, f i : β)) (k + max n i))
      ((fun (n : ℕ) ↦ (∑ i ∈ range n, f i : β)) (max n i))) ≤
  HSub.hSub (α := α) (∑ k ∈ range (k + max n i), a k) (∑ k ∈ range (max n i), a k)
Tactic: rw [hk]
-- 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 (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)
have succ : abv (f (k + max n i) + ∑ x ∈ range (k + max n i), f x - ∑ x ∈ range (max n i), f x) ≤
  a (k + max n i) + ∑ x ∈ range (k + max n i), a x - ∑ x ∈ range (max n i), a x
Tactic: simp only [Nat.succ_add, Nat.succ_eq_add_one, Finset.sum_range_succ_comm]
-- 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 (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 (f (k + max n i) + ∑ x ∈ range (k + max n i), f x - ∑ x ∈ range (max n i), f x) ≤
    a (k + max n i) + ∑ x ∈ range (k + max n i), a x - ∑ x ∈ range (max n i), a x
have succ : 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)
Tactic: simp only [add_assoc, sub_eq_add_neg]
-- 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 : ℕ → β
a : ℕ → α
n : ℕ
hm : ∀ (m : ℕ), n ≤ m → abv (f m) ≤ a m
i 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 (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 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)
Tactic: simp only [sub_eq_add_neg] at hi
Cleared hypotheses: hi