awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
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 : α
inl : ε_1 > 0 → ∃ (i : ℕ), ∀ j ≥ i, |(↑(a ⊓ b - b) : ℕ → α) j| < ε_1
⊢ ε_1 > 0 → ∃ (i : ℕ), ∀ j ≥ i, |(↑(a ⊓ b - b) : ℕ → α) j| < ε_1

Tactic:
_
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
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

Tactic:
⟨i, fun j hj => ?_⟩

Premises used: Exists.intro
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
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
inl : ∀ (j : ℕ) (hj : j ≥ i), |(↑(a ⊓ b - b) : ℕ → α) j| < ε_1
⊢ ∃ (i : ℕ), ∀ j ≥ i, |(↑(a ⊓ b - b) : ℕ → α) j| < ε_1

Tactic:
refine ⟨i, fun j hj => ?_⟩
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
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
inl : |min ((↑a : ℕ → α) j) ((↑b : ℕ → α) j) - (↑b : ℕ → α) j| < ε_1
⊢ |(↑(a ⊓ b - b) : ℕ → α) j| < ε_1

Tactic:
dsimp
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
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
inl : |min ((↑a : ℕ → α) j - (↑b : ℕ → α) j) ((↑b : ℕ → α) j - (↑b : ℕ → α) j)| < ε_1
⊢ |min ((↑a : ℕ → α) j) ((↑b : ℕ → α) j) - (↑b : ℕ → α) j| < ε_1

Tactic:
rw [← min_sub_sub_right]

Premises used: min_sub_sub_right
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
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
inl : 0 ≤ (↑a : ℕ → α) j - (↑b : ℕ → α) j
⊢ |min ((↑a : ℕ → α) j - (↑b : ℕ → α) j) ((↑b : ℕ → α) j - (↑b : ℕ → α) j)| < ε_1

Tactic:
rwa [sub_self, min_eq_right, abs_zero]

Premises used: sub_self, min_eq_right, abs_zero
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
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
⊢ 0 ≤ (↑a : ℕ → α) j - (↑b : ℕ → α) j

Tactic:
ε0.le.trans (h _ hj)

Premises used: LT.lt.le, LE.le.trans
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
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
⊢ 0 ≤ (↑a : ℕ → α) j - (↑b : ℕ → α) j

Tactic:
exact ε0.le.trans (h _ hj)

Premises used: LT.lt.le, LE.le.trans
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b : CauSeq α abs
h : b ≈ a
⊢ a ⊓ b ≈ b

Tactic:
Setoid.trans (inf_equiv_inf (Setoid.symm h) (Setoid.refl _)) ?_

Premises used: CauSeq.inf_equiv_inf, Setoid.symm, Setoid.trans, Setoid.refl
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b : CauSeq α abs
h : b ≈ a
inr : b ⊓ b ≈ b
⊢ a ⊓ b ≈ b

Tactic:
refine Setoid.trans (inf_equiv_inf (Setoid.symm h) (Setoid.refl _)) ?_

Premises used: CauSeq.inf_equiv_inf, Setoid.symm, Setoid.trans, Setoid.refl
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b : CauSeq α abs
h : b ≈ a
inr inr₁ : (equiv : CauSeq α abs → CauSeq α abs → Prop) b b
⊢ b ⊓ b ≈ b

Tactic:
rw [CauSeq.inf_idem]

Premises used: CauSeq.inf_idem
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b : CauSeq α abs
h : b ≤ a
⊢ a ⊔ b ≈ a

Tactic:
simpa only [CauSeq.sup_comm] using CauSeq.sup_eq_right h

Premises used: CauSeq.sup_eq_right, CauSeq.sup_comm
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b : CauSeq α abs
h : a ≤ b
⊢ a ⊓ b ≈ a

Tactic:
simpa only [CauSeq.inf_comm] using CauSeq.inf_eq_right h

Premises used: CauSeq.inf_comm, CauSeq.inf_eq_right
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b : CauSeq α abs
⊢ a ≤ a ⊔ b

Tactic:
le_of_exists ⟨0, fun _ _ => le_sup_left⟩

Premises used: le_sup_left, CauSeq.le_of_exists, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b : CauSeq α abs
⊢ a ⊓ b ≤ a

Tactic:
le_of_exists ⟨0, fun _ _ => inf_le_left⟩

Premises used: CauSeq.le_of_exists, Exists.intro, inf_le_left, OfNat.ofNat
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b : CauSeq α abs
⊢ b ≤ a ⊔ b

Tactic:
le_of_exists ⟨0, fun _ _ => le_sup_right⟩

Premises used: le_sup_right, CauSeq.le_of_exists, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b : CauSeq α abs
⊢ a ⊓ b ≤ b

Tactic:
le_of_exists ⟨0, fun _ _ => inf_le_right⟩

Premises used: inf_le_right, CauSeq.le_of_exists, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
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
inr : ∀ (ha : a ≈ c), a ⊔ b ≤ c
⊢ a ⊔ b ≤ c

Tactic:
obtain ha | ha := ha
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
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
inl₁ : ∀ (hb : b ≈ c), a ⊔ b ≤ c
⊢ a ⊔ b ≤ c

Tactic:
obtain hb | hb := hb
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
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

Tactic:
Or.inl (CauSeq.sup_lt ha hb)

Premises used: CauSeq.sup_lt, Or.inl
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
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

Tactic:
exact Or.inl (CauSeq.sup_lt ha hb)

Premises used: CauSeq.sup_lt, Or.inl
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
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

Tactic:
replace ha := le_of_le_of_eq ha.le (Setoid.symm hb)
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
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

Tactic:
le_of_le_of_eq (Or.inr ?_) hb

Premises used: CauSeq.le_of_le_of_eq, Or.inr
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b c : CauSeq α abs
hb : b ≈ c
ha : a ≤ b
inl : a ⊔ b ≈ b
⊢ a ⊔ b ≤ c

Tactic:
refine le_of_le_of_eq (Or.inr ?_) hb

Premises used: CauSeq.le_of_le_of_eq, Or.inr
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
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 ≈ b

Tactic:
CauSeq.sup_eq_right ha

Premises used: CauSeq.sup_eq_right
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
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 ≈ b

Tactic:
exact CauSeq.sup_eq_right ha

Premises used: CauSeq.sup_eq_right
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b c : CauSeq α abs
hb : b ≤ c
ha : a ≈ c
⊢ b ≤ a

Tactic:
replace hb := le_of_le_of_eq hb (Setoid.symm ha)
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
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

Tactic:
le_of_le_of_eq (Or.inr ?_) ha

Premises used: CauSeq.le_of_le_of_eq, Or.inr
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b c : CauSeq α abs
ha : a ≈ c
hb : b ≤ a
inr : a ⊔ b ≈ a
⊢ a ⊔ b ≤ c

Tactic:
refine le_of_le_of_eq (Or.inr ?_) ha

Premises used: CauSeq.le_of_le_of_eq, Or.inr
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
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 ≈ a

Tactic:
CauSeq.sup_eq_left hb

Premises used: CauSeq.sup_eq_left
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
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 ≈ a

Tactic:
exact CauSeq.sup_eq_left hb

Premises used: CauSeq.sup_eq_left
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
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
inr : ∀ (hb : a ≈ b), a ≤ b ⊓ c
⊢ a ≤ b ⊓ c

Tactic:
obtain hb | hb := hb
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
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
inl₁ : ∀ (hc : a ≈ c), a ≤ b ⊓ c
⊢ a ≤ b ⊓ c

Tactic:
obtain hc | hc := hc
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
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

Tactic:
Or.inl (CauSeq.lt_inf hb hc)

Premises used: CauSeq.lt_inf, Or.inl
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
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

Tactic:
exact Or.inl (CauSeq.lt_inf hb hc)

Premises used: CauSeq.lt_inf, Or.inl
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b c : CauSeq α abs
hb : a < b
hc : a ≈ c
⊢ c ≤ b

Tactic:
replace hb := le_of_eq_of_le (Setoid.symm hc) hb.le
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
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

Tactic:
le_of_eq_of_le hc (Or.inr ?_)

Premises used: CauSeq.le_of_eq_of_le, Or.inr
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b c : CauSeq α abs
hc : a ≈ c
hb : c ≤ b
inl : c ≈ b ⊓ c
⊢ a ≤ b ⊓ c

Tactic:
refine le_of_eq_of_le hc (Or.inr ?_)

Premises used: CauSeq.le_of_eq_of_le, Or.inr
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b c : CauSeq α abs
hc : a ≈ c
hb : c ≤ b
⊢ c ≈ b ⊓ c

Tactic:
Setoid.symm (CauSeq.inf_eq_right hb)

Premises used: CauSeq.inf_eq_right, Setoid.symm
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b c : CauSeq α abs
hc : a ≈ c
hb : c ≤ b
⊢ c ≈ b ⊓ c

Tactic:
exact Setoid.symm (CauSeq.inf_eq_right hb)

Premises used: CauSeq.inf_eq_right, Setoid.symm
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b c : CauSeq α abs
hc : a ≤ c
hb : a ≈ b
⊢ b ≤ c

Tactic:
replace hc := le_of_eq_of_le (Setoid.symm hb) hc
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
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

Tactic:
le_of_eq_of_le hb (Or.inr ?_)

Premises used: CauSeq.le_of_eq_of_le, Or.inr
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b c : CauSeq α abs
hb : a ≈ b
hc : b ≤ c
inr : b ≈ b ⊓ c
⊢ a ≤ b ⊓ c

Tactic:
refine le_of_eq_of_le hb (Or.inr ?_)

Premises used: CauSeq.le_of_eq_of_le, Or.inr
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b c : CauSeq α abs
hb : a ≈ b
hc : b ≤ c
⊢ b ≈ b ⊓ c

Tactic:
Setoid.symm (CauSeq.inf_eq_left hc)

Premises used: Setoid.symm, CauSeq.inf_eq_left
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b c : CauSeq α abs
hb : a ≈ b
hc : b ≤ c
⊢ b ≈ b ⊓ c

Tactic:
exact Setoid.symm (CauSeq.inf_eq_left hc)

Premises used: Setoid.symm, CauSeq.inf_eq_left
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b c : CauSeq α abs
⊢ a ⊔ b ⊓ c = (a ⊔ b) ⊓ (a ⊔ c)

Tactic:
ext fun _ ↦ max_min_distrib_left _ _ _

Premises used: max_min_distrib_left, CauSeq.ext, Subtype.val
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b c : CauSeq α abs
⊢ a ⊓ b ⊔ c = (a ⊔ c) ⊓ (b ⊔ c)

Tactic:
ext fun _ ↦ max_min_distrib_right _ _ _

Premises used: max_min_distrib_right, CauSeq.ext, Subtype.val
-- 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 : ℕ → β
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
⊢ LT.lt.{u_1} (α := α) 0 2

Tactic:
simp
-- 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 : ℕ → β
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
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)) <
          ε
⊢ ∃ (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))

Premises used: HDiv.hDiv, div_pos, OfNat.ofNat
-- 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 : ℕ → β
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
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))) <
      ε
⊢ ∃ (i : ℕ),
    ∀ j ≥ i,
      abv
          (HSub.hSub (α := β) ((fun (n : ℕ) ↦ (∑ i ∈ range n, f i : β)) j)
            ((fun (n : ℕ) ↦ (∑ i ∈ range n, f i : β)) i)) <
        ε

Tactic:
exists max n i

Premises used: Max.max
-- 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 : ℕ → β
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
⊢ |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)
-- 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 : ℕ → β
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
⊢ |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)
-- 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 : ℕ → β
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
⊢ |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)
-- 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 : ℕ → β
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)|
⊢ |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₂
-- 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 : ℕ → β
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
⊢ |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

Premises used: add_halves, Finset.range, Max.max, abs_sub_comm, Finset.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 : ℕ → β
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))) <
    ε

Tactic:
lt_of_le_of_lt (le_trans (le_trans ?_ (le_abs_self _)) sub_le) this

Premises used: lt_of_le_of_lt, le_abs_self, le_trans