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 α
x y : α
⊢ LE.le (α := CauSeq α abs) (const x) (const y) ↔ x < y ∨ x = y

Tactic:
or_congr const_lt const_equiv

Premises used: or_congr, CauSeq.const_lt, CauSeq.const_equiv
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
x y : α
⊢ LE.le (α := CauSeq α abs) (const x) (const y) ↔ x < y ∨ x = y

Tactic:
exact or_congr const_lt const_equiv

Premises used: or_congr, CauSeq.const_lt, CauSeq.const_equiv
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
f g : CauSeq α abs
h : ∃ (i : ℕ), ∀ j ≥ i, (↑f : ℕ → α) j ≤ (↑g : ℕ → α) j
⊢ f ≤ g

Tactic:
let ⟨i, hi⟩ := h
  (or_assoc.2 (CauSeq.lt_total f g)).elim id fun hgf =>
    False.elim
      (let ⟨_, hK0, j, hKj⟩ := hgf
      not_lt_of_ge (hi (max i j) (le_max_left _ _))
        (sub_pos.1 (lt_of_lt_of_le hK0 (hKj _ (le_max_right _ _)))))

Premises used: le_max_right, Iff.mpr, sub_pos, False, False.elim, _private.0.CauSeq.le_of_exists.match_2, id, LE.le, _private.0.CauSeq.le_of_exists.match_1, Max.max, Iff.mp, CauSeq.lt_total, Or.elim, le_max_left, or_assoc, lt_of_lt_of_le, not_lt_of_ge
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
f : CauSeq α abs
K : α
H : ∀ (i : ℕ), |(↑f : ℕ → α) i| < K
i : ℕ
h : i ≥ 0
rw : (↑f : ℕ → α) i ≤ K
⊢ 1 ≤ (↑(const (K + 1) - f) : ℕ → α) i

Tactic:
rw [sub_apply, const_apply, le_sub_iff_add_le', add_le_add_iff_right]

Premises used: CauSeq.sub_apply, le_sub_iff_add_le', CauSeq.const_apply, add_le_add_iff_right
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
f : CauSeq α abs
K : α
H : ∀ (i : ℕ), |(↑f : ℕ → α) i| < K
i : ℕ
h : i ≥ 0
⊢ (↑f : ℕ → α) i ≤ K

Tactic:
le_of_lt (abs_lt.1 (H _)).2

Premises used: le_of_lt, And.right, Iff.mp, abs_lt
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
f : CauSeq α abs
K : α
H : ∀ (i : ℕ), |(↑f : ℕ → α) i| < K
i : ℕ
h : i ≥ 0
⊢ (↑f : ℕ → α) i ≤ K

Tactic:
exact le_of_lt (abs_lt.1 (H _)).2

Premises used: le_of_lt, And.right, Iff.mp, abs_lt
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
f : CauSeq α abs
a : α
h : -f < const a
rwa : (f - -const a).Pos
rwa₁ : (f + const a).Pos
rwa₂ : (const a + f).Pos
rwa₃ rwa₄ rwa₅ rwa₆ : (const a - -f).Pos
⊢ (f - const (-a)).Pos

Tactic:
rwa [const_neg, sub_neg_eq_add, add_comm, ← sub_neg_eq_add]

Premises used: CauSeq.const_neg, add_comm, sub_neg_eq_add
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
ε a₁ a₂ b₁ b₂ : α
⊢ |a₁ - b₁| < ε → |a₂ - b₂| < ε → |max a₁ a₂ - max b₁ b₂| < ε

Tactic:
fun h₁ h₂ =>
  (abs_max_sub_max_le_max _ _ _ _).trans_lt (max_lt h₁ h₂)

Premises used: abs_max_sub_max_le_max, max_lt, LE.le.trans_lt
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
ε a₁ a₂ b₁ b₂ : α
⊢ |a₁ - b₁| < ε → |a₂ - b₂| < ε → |min a₁ a₂ - min b₁ b₂| < ε

Tactic:
fun h₁ h₂ =>
  (abs_min_sub_min_le_max _ _ _ _).trans_lt (max_lt h₁ h₂)

Premises used: max_lt, abs_min_sub_min_le_max, LE.le.trans_lt
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
f g : CauSeq α abs
⊢ (↑(f ⊔ g) : ℕ → α) = (↑f : ℕ → α) ⊔ (↑g : ℕ → α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
f g : CauSeq α abs
⊢ (↑(f ⊓ g) : ℕ → α) = (↑f : ℕ → α) ⊓ (↑g : ℕ → α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
f g : CauSeq α abs
hf : f.LimZero
hg : g.LimZero
ε : α
ε0 : ε > 0
x : ℕ
H : ∀ j ≥ x, |(↑f : ℕ → α) j| < ε ∧ |(↑g : ℕ → α) j| < ε
j : ℕ
ij : j ≥ x
⊢ |(↑f : ℕ → α) j| < ε

Tactic:
let ⟨H₁, H₂⟩ := H _ ij
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
f g : CauSeq α abs
hf : f.LimZero
hg : g.LimZero
ε : α
ε0 : ε > 0
x : ℕ
H : ∀ j ≥ x, |(↑f : ℕ → α) j| < ε ∧ |(↑g : ℕ → α) j| < ε
j : ℕ
ij : j ≥ x
H₁ : |(↑f : ℕ → α) j| < ε
⊢ |(↑g : ℕ → α) j| < ε

Tactic:
let ⟨H₁, H₂⟩ := H _ ij
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
f g : CauSeq α abs
hf : f.LimZero
hg : g.LimZero
ε : α
ε0 : ε > 0
x : ℕ
H : ∀ j ≥ x, |(↑f : ℕ → α) j| < ε ∧ |(↑g : ℕ → α) j| < ε
j : ℕ
ij : j ≥ x
H₁ : |(↑f : ℕ → α) j| < ε
H₂ : |(↑g : ℕ → α) j| < ε
rw :
  ∀ (H₁ : -ε < (↑f : ℕ → α) j ∧ (↑f : ℕ → α) j < ε) (H₂ : -ε < (↑g : ℕ → α) j ∧ (↑g : ℕ → α) j < ε),
    -ε < (↑(f ⊔ g) : ℕ → α) j ∧ (↑(f ⊔ g) : ℕ → α) j < ε
⊢ |(↑(f ⊔ g) : ℕ → α) j| < ε

Tactic:
rw [abs_lt] at H₁ H₂ ⊢

Premises used: abs_lt
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
f g : CauSeq α abs
hf : f.LimZero
hg : g.LimZero
ε : α
ε0 : ε > 0
x : ℕ
H : ∀ j ≥ x, |(↑f : ℕ → α) j| < ε ∧ |(↑g : ℕ → α) j| < ε
j : ℕ
ij : j ≥ x
H₁ : -ε < (↑f : ℕ → α) j ∧ (↑f : ℕ → α) j < ε
H₂ : -ε < (↑g : ℕ → α) j ∧ (↑g : ℕ → α) j < ε
⊢ -ε < (↑(f ⊔ g) : ℕ → α) j ∧ (↑(f ⊔ g) : ℕ → α) j < ε

Tactic:
⟨lt_sup_iff.mpr (Or.inl H₁.1), sup_lt_iff.mpr ⟨H₁.2, H₂.2⟩⟩

Premises used: Iff.mpr, lt_sup_iff, And.right, And.left, sup_lt_iff, And.intro, Or.inl
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
f g : CauSeq α abs
hf : f.LimZero
hg : g.LimZero
ε : α
ε0 : ε > 0
x : ℕ
H : ∀ j ≥ x, |(↑f : ℕ → α) j| < ε ∧ |(↑g : ℕ → α) j| < ε
j : ℕ
ij : j ≥ x
H₁ : -ε < (↑f : ℕ → α) j ∧ (↑f : ℕ → α) j < ε
H₂ : -ε < (↑g : ℕ → α) j ∧ (↑g : ℕ → α) j < ε
⊢ -ε < (↑(f ⊔ g) : ℕ → α) j ∧ (↑(f ⊔ g) : ℕ → α) j < ε

Tactic:
exact ⟨lt_sup_iff.mpr (Or.inl H₁.1), sup_lt_iff.mpr ⟨H₁.2, H₂.2⟩⟩
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
f g : CauSeq α abs
hf : f.LimZero
hg : g.LimZero
ε : α
ε0 : ε > 0
x : ℕ
H : ∀ j ≥ x, |(↑f : ℕ → α) j| < ε ∧ |(↑g : ℕ → α) j| < ε
j : ℕ
ij : j ≥ x
H₁ : |(↑f : ℕ → α) j| < ε
H₂ : |(↑g : ℕ → α) j| < ε
rw :
  ∀ (H₁ : -ε < (↑f : ℕ → α) j ∧ (↑f : ℕ → α) j < ε) (H₂ : -ε < (↑g : ℕ → α) j ∧ (↑g : ℕ → α) j < ε),
    -ε < (↑(f ⊓ g) : ℕ → α) j ∧ (↑(f ⊓ g) : ℕ → α) j < ε
⊢ |(↑(f ⊓ g) : ℕ → α) j| < ε

Tactic:
rw [abs_lt] at H₁ H₂ ⊢

Premises used: abs_lt
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
f g : CauSeq α abs
hf : f.LimZero
hg : g.LimZero
ε : α
ε0 : ε > 0
x : ℕ
H : ∀ j ≥ x, |(↑f : ℕ → α) j| < ε ∧ |(↑g : ℕ → α) j| < ε
j : ℕ
ij : j ≥ x
H₁ : -ε < (↑f : ℕ → α) j ∧ (↑f : ℕ → α) j < ε
H₂ : -ε < (↑g : ℕ → α) j ∧ (↑g : ℕ → α) j < ε
⊢ -ε < (↑(f ⊓ g) : ℕ → α) j ∧ (↑(f ⊓ g) : ℕ → α) j < ε

Tactic:
⟨lt_inf_iff.mpr ⟨H₁.1, H₂.1⟩, inf_lt_iff.mpr (Or.inl H₁.2)⟩

Premises used: Iff.mpr, lt_inf_iff, And.right, And.left, And.intro, inf_lt_iff, Or.inl
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
f g : CauSeq α abs
hf : f.LimZero
hg : g.LimZero
ε : α
ε0 : ε > 0
x : ℕ
H : ∀ j ≥ x, |(↑f : ℕ → α) j| < ε ∧ |(↑g : ℕ → α) j| < ε
j : ℕ
ij : j ≥ x
H₁ : -ε < (↑f : ℕ → α) j ∧ (↑f : ℕ → α) j < ε
H₂ : -ε < (↑g : ℕ → α) j ∧ (↑g : ℕ → α) j < ε
⊢ -ε < (↑(f ⊓ g) : ℕ → α) j ∧ (↑(f ⊓ g) : ℕ → α) j < ε

Tactic:
exact ⟨lt_inf_iff.mpr ⟨H₁.1, H₂.1⟩, inf_lt_iff.mpr (Or.inl H₁.2)⟩
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a₁ b₁ a₂ b₂ : CauSeq α abs
ha : a₁ ≈ a₂
hb : b₁ ≈ b₂
ε : α
ε0 : ε > 0
obtain :
  ∀ (ai : ℕ) (hai : ∀ j ≥ ai, |(↑(a₁ - a₂) : ℕ → α) j| < ε), ∃ (i : ℕ), ∀ j ≥ i, |(↑(a₁ ⊔ b₁ - a₂ ⊔ b₂) : ℕ → α) j| < ε
⊢ ∃ (i : ℕ), ∀ j ≥ i, |(↑(a₁ ⊔ b₁ - a₂ ⊔ b₂) : ℕ → α) j| < ε

Tactic:
obtain ⟨ai, hai⟩ := ha ε ε0
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a₁ b₁ a₂ b₂ : CauSeq α abs
ha : a₁ ≈ a₂
hb : b₁ ≈ b₂
ε : α
ε0 : ε > 0
ai : ℕ
hai : ∀ j ≥ ai, |(↑(a₁ - a₂) : ℕ → α) j| < ε
obtain :
  ∀ (bi : ℕ) (hbi : ∀ j ≥ bi, |(↑(b₁ - b₂) : ℕ → α) j| < ε), ∃ (i : ℕ), ∀ j ≥ i, |(↑(a₁ ⊔ b₁ - a₂ ⊔ b₂) : ℕ → α) j| < ε
⊢ ∃ (i : ℕ), ∀ j ≥ i, |(↑(a₁ ⊔ b₁ - a₂ ⊔ b₂) : ℕ → α) j| < ε

Tactic:
obtain ⟨bi, hbi⟩ := hb ε ε0
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a₁ b₁ a₂ b₂ : CauSeq α abs
ha : a₁ ≈ a₂
hb : b₁ ≈ b₂
ε : α
ε0 : ε > 0
ai : ℕ
hai : ∀ j ≥ ai, |(↑(a₁ - a₂) : ℕ → α) j| < ε
bi : ℕ
hbi : ∀ j ≥ bi, |(↑(b₁ - b₂) : ℕ → α) j| < ε
⊢ ∃ (i : ℕ), ∀ j ≥ i, |(↑(a₁ ⊔ b₁ - a₂ ⊔ b₂) : ℕ → α) j| < ε

Tactic:
⟨ai ⊔ bi, fun i hi =>
      (abs_max_sub_max_le_max (a₁ i) (b₁ i) (a₂ i) (b₂ i)).trans_lt
        (max_lt (hai i (sup_le_iff.mp hi).1) (hbi i (sup_le_iff.mp hi).2))⟩

Premises used: abs_max_sub_max_le_max, max_lt, sup_le_iff, And.right, And.left, Max.max, Exists.intro, Iff.mp, Subtype.val, LE.le.trans_lt
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a₁ b₁ a₂ b₂ : CauSeq α abs
ha : a₁ ≈ a₂
hb : b₁ ≈ b₂
ε : α
ε0 : ε > 0
ai : ℕ
hai : ∀ j ≥ ai, |(↑(a₁ - a₂) : ℕ → α) j| < ε
bi : ℕ
hbi : ∀ j ≥ bi, |(↑(b₁ - b₂) : ℕ → α) j| < ε
⊢ ∃ (i : ℕ), ∀ j ≥ i, |(↑(a₁ ⊔ b₁ - a₂ ⊔ b₂) : ℕ → α) j| < ε

Tactic:
exact
    ⟨ai ⊔ bi, fun i hi =>
      (abs_max_sub_max_le_max (a₁ i) (b₁ i) (a₂ i) (b₂ i)).trans_lt
        (max_lt (hai i (sup_le_iff.mp hi).1) (hbi i (sup_le_iff.mp hi).2))⟩
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a₁ b₁ a₂ b₂ : CauSeq α abs
ha : a₁ ≈ a₂
hb : b₁ ≈ b₂
ε : α
ε0 : ε > 0
obtain :
  ∀ (ai : ℕ) (hai : ∀ j ≥ ai, |(↑(a₁ - a₂) : ℕ → α) j| < ε), ∃ (i : ℕ), ∀ j ≥ i, |(↑(a₁ ⊓ b₁ - a₂ ⊓ b₂) : ℕ → α) j| < ε
⊢ ∃ (i : ℕ), ∀ j ≥ i, |(↑(a₁ ⊓ b₁ - a₂ ⊓ b₂) : ℕ → α) j| < ε

Tactic:
obtain ⟨ai, hai⟩ := ha ε ε0
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a₁ b₁ a₂ b₂ : CauSeq α abs
ha : a₁ ≈ a₂
hb : b₁ ≈ b₂
ε : α
ε0 : ε > 0
ai : ℕ
hai : ∀ j ≥ ai, |(↑(a₁ - a₂) : ℕ → α) j| < ε
obtain :
  ∀ (bi : ℕ) (hbi : ∀ j ≥ bi, |(↑(b₁ - b₂) : ℕ → α) j| < ε), ∃ (i : ℕ), ∀ j ≥ i, |(↑(a₁ ⊓ b₁ - a₂ ⊓ b₂) : ℕ → α) j| < ε
⊢ ∃ (i : ℕ), ∀ j ≥ i, |(↑(a₁ ⊓ b₁ - a₂ ⊓ b₂) : ℕ → α) j| < ε

Tactic:
obtain ⟨bi, hbi⟩ := hb ε ε0
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a₁ b₁ a₂ b₂ : CauSeq α abs
ha : a₁ ≈ a₂
hb : b₁ ≈ b₂
ε : α
ε0 : ε > 0
ai : ℕ
hai : ∀ j ≥ ai, |(↑(a₁ - a₂) : ℕ → α) j| < ε
bi : ℕ
hbi : ∀ j ≥ bi, |(↑(b₁ - b₂) : ℕ → α) j| < ε
⊢ ∃ (i : ℕ), ∀ j ≥ i, |(↑(a₁ ⊓ b₁ - a₂ ⊓ b₂) : ℕ → α) j| < ε

Tactic:
⟨ai ⊔ bi, fun i hi =>
      (abs_min_sub_min_le_max (a₁ i) (b₁ i) (a₂ i) (b₂ i)).trans_lt
        (max_lt (hai i (sup_le_iff.mp hi).1) (hbi i (sup_le_iff.mp hi).2))⟩

Premises used: max_lt, sup_le_iff, And.right, And.left, Max.max, Exists.intro, Iff.mp, abs_min_sub_min_le_max, Subtype.val, LE.le.trans_lt
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a₁ b₁ a₂ b₂ : CauSeq α abs
ha : a₁ ≈ a₂
hb : b₁ ≈ b₂
ε : α
ε0 : ε > 0
ai : ℕ
hai : ∀ j ≥ ai, |(↑(a₁ - a₂) : ℕ → α) j| < ε
bi : ℕ
hbi : ∀ j ≥ bi, |(↑(b₁ - b₂) : ℕ → α) j| < ε
⊢ ∃ (i : ℕ), ∀ j ≥ i, |(↑(a₁ ⊓ b₁ - a₂ ⊓ b₂) : ℕ → α) j| < ε

Tactic:
exact
    ⟨ai ⊔ bi, fun i hi =>
      (abs_min_sub_min_le_max (a₁ i) (b₁ i) (a₂ i) (b₂ i)).trans_lt
        (max_lt (hai i (sup_le_iff.mp hi).1) (hbi i (sup_le_iff.mp hi).2))⟩
-- 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
obtain :
  ∀ (εa : α) (εa0 : εa > 0) (ia : ℕ) (ha : ∀ j ≥ ia, εa ≤ (↑(c - a) : ℕ → α) j) (εb : α) (εb0 : εb > 0) (ib : ℕ)
    (hb : ∀ j ≥ ib, εb ≤ (↑(c - b) : ℕ → α) j), a ⊔ b < c
⊢ a ⊔ b < c

Tactic:
obtain ⟨⟨εa, εa0, ia, ha⟩, ⟨εb, εb0, ib, hb⟩⟩ := ha, hb
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b c : CauSeq α abs
εa : α
εa0 : εa > 0
ia : ℕ
ha : ∀ j ≥ ia, εa ≤ (↑(c - a) : ℕ → α) j
εb : α
εb0 : εb > 0
ib : ℕ
hb : ∀ j ≥ ib, εb ≤ (↑(c - b) : ℕ → α) j
⊢ a ⊔ b < c

Tactic:
⟨εa ⊓ εb, lt_inf_iff.mpr ⟨εa0, εb0⟩, ia ⊔ ib, fun i hi => ?_⟩

Premises used: Iff.mpr, CauSeq.Pos, lt_inf_iff, Max.max, And.intro, Exists.intro, Min.min
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b c : CauSeq α abs
εa : α
εa0 : εa > 0
ia : ℕ
ha : ∀ j ≥ ia, εa ≤ (↑(c - a) : ℕ → α) j
εb : α
εb0 : εb > 0
ib : ℕ
hb : ∀ j ≥ ib, εb ≤ (↑(c - b) : ℕ → α) j
refine : ∀ (i : ℕ) (hi : i ≥ max ia ib), min εa εb ≤ (↑(c - a ⊔ b) : ℕ → α) i
⊢ a ⊔ b < c

Tactic:
refine ⟨εa ⊓ εb, lt_inf_iff.mpr ⟨εa0, εb0⟩, ia ⊔ ib, fun i hi => ?_⟩
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b c : CauSeq α abs
εa : α
εa0 : εa > 0
ia : ℕ
ha : ∀ j ≥ ia, εa ≤ (↑(c - a) : ℕ → α) j
εb : α
εb0 : εb > 0
ib : ℕ
hb : ∀ j ≥ ib, εb ≤ (↑(c - b) : ℕ → α) j
i : ℕ
hi : i ≥ max ia ib
⊢ min εa εb ≤ min ((↑(c - a) : ℕ → α) i) ((↑(c - b) : ℕ → α) i)

Tactic:
have := min_le_min (ha _ (sup_le_iff.mp hi).1) (hb _ (sup_le_iff.mp hi).2)
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b c : CauSeq α abs
εa : α
εa0 : εa > 0
ia : ℕ
ha : ∀ j ≥ ia, εa ≤ (↑(c - a) : ℕ → α) j
εb : α
εb0 : εb > 0
ib : ℕ
hb : ∀ j ≥ ib, εb ≤ (↑(c - b) : ℕ → α) j
i : ℕ
hi : i ≥ max ia ib
this : min εa εb ≤ min ((↑(c - a) : ℕ → α) i) ((↑(c - b) : ℕ → α) i)
⊢ min εa εb ≤ (↑(c - a ⊔ b) : ℕ → α) i

Tactic:
this.trans_eq (min_sub_sub_left _ _ _)

Premises used: min_sub_sub_left, LE.le.trans_eq
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b c : CauSeq α abs
εa : α
εa0 : εa > 0
ia : ℕ
ha : ∀ j ≥ ia, εa ≤ (↑(c - a) : ℕ → α) j
εb : α
εb0 : εb > 0
ib : ℕ
hb : ∀ j ≥ ib, εb ≤ (↑(c - b) : ℕ → α) j
i : ℕ
hi : i ≥ max ia ib
this : min εa εb ≤ min ((↑(c - a) : ℕ → α) i) ((↑(c - b) : ℕ → α) i)
⊢ min εa εb ≤ (↑(c - a ⊔ b) : ℕ → α) i

Tactic:
exact this.trans_eq (min_sub_sub_left _ _ _)

Premises used: min_sub_sub_left, LE.le.trans_eq
-- 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
obtain :
  ∀ (εb : α) (εb0 : εb > 0) (ib : ℕ) (hb : ∀ j ≥ ib, εb ≤ (↑(b - a) : ℕ → α) j) (εc : α) (εc0 : εc > 0) (ic : ℕ)
    (hc : ∀ j ≥ ic, εc ≤ (↑(c - a) : ℕ → α) j), a < b ⊓ c
⊢ a < b ⊓ c

Tactic:
obtain ⟨⟨εb, εb0, ib, hb⟩, ⟨εc, εc0, ic, hc⟩⟩ := 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
εb : α
εb0 : εb > 0
ib : ℕ
hb : ∀ j ≥ ib, εb ≤ (↑(b - a) : ℕ → α) j
εc : α
εc0 : εc > 0
ic : ℕ
hc : ∀ j ≥ ic, εc ≤ (↑(c - a) : ℕ → α) j
⊢ a < b ⊓ c

Tactic:
⟨εb ⊓ εc, lt_inf_iff.mpr ⟨εb0, εc0⟩, ib ⊔ ic, fun i hi => ?_⟩

Premises used: Iff.mpr, CauSeq.Pos, lt_inf_iff, Max.max, And.intro, Exists.intro, Min.min
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b c : CauSeq α abs
εb : α
εb0 : εb > 0
ib : ℕ
hb : ∀ j ≥ ib, εb ≤ (↑(b - a) : ℕ → α) j
εc : α
εc0 : εc > 0
ic : ℕ
hc : ∀ j ≥ ic, εc ≤ (↑(c - a) : ℕ → α) j
refine : ∀ (i : ℕ) (hi : i ≥ max ib ic), min εb εc ≤ (↑(b ⊓ c - a) : ℕ → α) i
⊢ a < b ⊓ c

Tactic:
refine ⟨εb ⊓ εc, lt_inf_iff.mpr ⟨εb0, εc0⟩, ib ⊔ ic, fun i hi => ?_⟩
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b c : CauSeq α abs
εb : α
εb0 : εb > 0
ib : ℕ
hb : ∀ j ≥ ib, εb ≤ (↑(b - a) : ℕ → α) j
εc : α
εc0 : εc > 0
ic : ℕ
hc : ∀ j ≥ ic, εc ≤ (↑(c - a) : ℕ → α) j
i : ℕ
hi : i ≥ max ib ic
⊢ min εb εc ≤ min ((↑(b - a) : ℕ → α) i) ((↑(c - a) : ℕ → α) i)

Tactic:
have := min_le_min (hb _ (sup_le_iff.mp hi).1) (hc _ (sup_le_iff.mp hi).2)
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b c : CauSeq α abs
εb : α
εb0 : εb > 0
ib : ℕ
hb : ∀ j ≥ ib, εb ≤ (↑(b - a) : ℕ → α) j
εc : α
εc0 : εc > 0
ic : ℕ
hc : ∀ j ≥ ic, εc ≤ (↑(c - a) : ℕ → α) j
i : ℕ
hi : i ≥ max ib ic
this : min εb εc ≤ min ((↑(b - a) : ℕ → α) i) ((↑(c - a) : ℕ → α) i)
⊢ min εb εc ≤ (↑(b ⊓ c - a) : ℕ → α) i

Tactic:
this.trans_eq (min_sub_sub_right _ _ _)

Premises used: LE.le.trans_eq, min_sub_sub_right
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b c : CauSeq α abs
εb : α
εb0 : εb > 0
ib : ℕ
hb : ∀ j ≥ ib, εb ≤ (↑(b - a) : ℕ → α) j
εc : α
εc0 : εc > 0
ic : ℕ
hc : ∀ j ≥ ic, εc ≤ (↑(c - a) : ℕ → α) j
i : ℕ
hi : i ≥ max ib ic
this : min εb εc ≤ min ((↑(b - a) : ℕ → α) i) ((↑(c - a) : ℕ → α) i)
⊢ min εb εc ≤ (↑(b ⊓ c - a) : ℕ → α) i

Tactic:
exact this.trans_eq (min_sub_sub_right _ _ _)

Premises used: LE.le.trans_eq, min_sub_sub_right
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a : CauSeq α abs
⊢ a ⊔ a = a

Tactic:
Subtype.ext (sup_idem _)

Premises used: sup_idem, CauSeq, Subtype.ext
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a : CauSeq α abs
⊢ a ⊓ a = a

Tactic:
Subtype.ext (inf_idem _)

Premises used: CauSeq, inf_idem, Subtype.ext
-- 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 ⊔ a

Tactic:
Subtype.ext (sup_comm _ _)

Premises used: sup_comm, CauSeq, Subtype.ext
-- 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 ⊓ a

Tactic:
Subtype.ext (inf_comm _ _)

Premises used: inf_comm, CauSeq, Subtype.ext
-- 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
inl : ∀ (ε : α) (ε0 : 0 < ε) (i : ℕ) (h : ∀ j ≥ i, ε ≤ (↑(b - a) : ℕ → α) j), a ⊔ b ≈ b
inr : ∀ (h : a ≈ b), a ⊔ b ≈ b
⊢ a ⊔ b ≈ b

Tactic:
obtain ⟨ε, ε0 : _ < _, i, h⟩ | h := h
-- 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, ε ≤ (↑(b - a) : ℕ → α) 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, ε ≤ (↑(b - a) : ℕ → α) 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, ε ≤ (↑(b - a) : ℕ → α) 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, ε ≤ (↑(b - a) : ℕ → α) j
ε_1 : α
h_1 : ε_1 > 0
j : ℕ
hj : j ≥ i
inl : |max ((↑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, ε ≤ (↑(b - a) : ℕ → α) j
ε_1 : α
h_1 : ε_1 > 0
j : ℕ
hj : j ≥ i
inl : |max ((↑a : ℕ → α) j - (↑b : ℕ → α) j) ((↑b : ℕ → α) j - (↑b : ℕ → α) j)| < ε_1
⊢ |max ((↑a : ℕ → α) j) ((↑b : ℕ → α) j) - (↑b : ℕ → α) j| < ε_1

Tactic:
rw [← max_sub_sub_right]

Premises used: max_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, ε ≤ (↑(b - a) : ℕ → α) j
ε_1 : α
h_1 : ε_1 > 0
j : ℕ
hj : j ≥ i
inl : (↑a : ℕ → α) j - (↑b : ℕ → α) j ≤ 0
⊢ |max ((↑a : ℕ → α) j - (↑b : ℕ → α) j) ((↑b : ℕ → α) j - (↑b : ℕ → α) j)| < ε_1

Tactic:
rwa [sub_self, max_eq_right, abs_zero]

Premises used: sub_self, max_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, ε ≤ (↑(b - a) : ℕ → α) j
ε_1 : α
h_1 : ε_1 > 0
j : ℕ
hj : j ≥ i
inl : 0 ≤ (↑b : ℕ → α) j - (↑a : ℕ → α) j
⊢ (↑a : ℕ → α) j - (↑b : ℕ → α) j ≤ 0

Tactic:
rw [sub_nonpos, ← sub_nonneg]

Premises used: sub_nonpos, sub_nonneg
-- 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, ε ≤ (↑(b - a) : ℕ → α) j
ε_1 : α
h_1 : ε_1 > 0
j : ℕ
hj : j ≥ i
⊢ 0 ≤ (↑b : ℕ → α) j - (↑a : ℕ → α) 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, ε ≤ (↑(b - a) : ℕ → α) j
ε_1 : α
h_1 : ε_1 > 0
j : ℕ
hj : j ≥ i
⊢ 0 ≤ (↑b : ℕ → α) j - (↑a : ℕ → α) 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 : a ≈ b
⊢ a ⊔ b ≈ b

Tactic:
Setoid.trans (sup_equiv_sup h (Setoid.refl _)) ?_

Premises used: CauSeq.sup_equiv_sup, 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 : a ≈ b
inr : b ⊔ b ≈ b
⊢ a ⊔ b ≈ b

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

Premises used: CauSeq.sup_equiv_sup, 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 : a ≈ b
inr inr₁ : (equiv : CauSeq α abs → CauSeq α abs → Prop) b b
⊢ b ⊔ b ≈ b

Tactic:
rw [CauSeq.sup_idem]

Premises used: CauSeq.sup_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
inl : ∀ (ε : α) (ε0 : 0 < ε) (i : ℕ) (h : ∀ j ≥ i, ε ≤ (↑(a - b) : ℕ → α) j), a ⊓ b ≈ b
inr : ∀ (h : b ≈ a), a ⊓ b ≈ b
⊢ a ⊓ b ≈ b

Tactic:
obtain ⟨ε, ε0 : _ < _, i, h⟩ | h := h