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 α
f : CauSeq α abs
h : ¬f.LimZero
K : α
K0 : K > 0
hK : ∃ (i : ℕ), ∀ j ≥ i, K ≤ |(↑f : ℕ → α) j|
i : ℕ
hi : ∀ j ≥ i, K ≤ |(↑f : ℕ → α) j| ∧ ∀ k ≥ j, |(↑f : ℕ → α) k - (↑f : ℕ → α) j| < K
⊢ 0 ≤ (↑f : ℕ → α) i → f.Pos
have inr : ∀ (h : 0 ≤ (↑f : ℕ → α) i) (j : ℕ) (ij : j ≥ i), K ≤ (↑f : ℕ → α) j
Tactic: refine fun h => ⟨K, K0, i, fun j ij => ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.Basic (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
f : CauSeq α abs
h : ¬f.LimZero
K : α
K0 : K > 0
hK : ∃ (i : ℕ), ∀ j ≥ i, K ≤ |(↑f : ℕ → α) j|
i : ℕ
hi : ∀ j ≥ i, K ≤ |(↑f : ℕ → α) j| ∧ ∀ k ≥ j, |(↑f : ℕ → α) k - (↑f : ℕ → α) j| < K
⊢ (↑f : ℕ → α) i ≤ 0 → (-f).Pos
have inr : ∀ (h : (↑f : ℕ → α) i ≤ 0) (j : ℕ) (ij : j ≥ i), K ≤ (↑(-f) : ℕ → α) j
Tactic: refine fun h => ⟨K, K0, i, fun j ij => ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.Basic (hypothesis)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
f : CauSeq α abs
h_1 : ¬f.LimZero
K : α
K0 : K > 0
hK : ∃ (i : ℕ), ∀ j ≥ i, K ≤ |(↑f : ℕ → α) j|
i : ℕ
hi : ∀ j ≥ i, K ≤ |(↑f : ℕ → α) j| ∧ ∀ k ≥ j, |(↑f : ℕ → α) k - (↑f : ℕ → α) j| < K
h : 0 ≤ (↑f : ℕ → α) i
j : ℕ
ij : j ≥ i
⊢ K ≤ (↑f : ℕ → α) j
have this : K ≤ |(↑f : ℕ → α) j|
Tactic: have := (hi _ ij).1
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.Basic (hypothesis)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
f : CauSeq α abs
h_1 : ¬f.LimZero
K : α
K0 : K > 0
hK : ∃ (i : ℕ), ∀ j ≥ i, K ≤ |(↑f : ℕ → α) j|
i : ℕ
hi : ∀ j ≥ i, K ≤ |(↑f : ℕ → α) j| ∧ ∀ k ≥ j, |(↑f : ℕ → α) k - (↑f : ℕ → α) j| < K
h : (↑f : ℕ → α) i ≤ 0
j : ℕ
ij : j ≥ i
⊢ K ≤ (↑(-f) : ℕ → α) j
have this : K ≤ |(↑f : ℕ → α) j|
Tactic: have := (hi _ ij).1
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.Basic (hypothesis)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
f : CauSeq α abs
h_1 : ¬f.LimZero
K : α
K0 : K > 0
hK : ∃ (i : ℕ), ∀ j ≥ i, K ≤ |(↑f : ℕ → α) j|
i : ℕ
hi : ∀ j ≥ i, K ≤ |(↑f : ℕ → α) j| ∧ ∀ k ≥ j, |(↑f : ℕ → α) k - (↑f : ℕ → α) j| < K
h : 0 ≤ (↑f : ℕ → α) i
j : ℕ
ij : j ≥ i
this : K ≤ |(↑f : ℕ → α) j|
⊢ K ≤ (↑f : ℕ → α) j
have h₁ : K ≤ |(↑f : ℕ → α) i|
Tactic: obtain ⟨h₁, h₂⟩ := hi _ le_rfl
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.Basic (hypothesis)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
f : CauSeq α abs
h_1 : ¬f.LimZero
K : α
K0 : K > 0
hK : ∃ (i : ℕ), ∀ j ≥ i, K ≤ |(↑f : ℕ → α) j|
i : ℕ
hi : ∀ j ≥ i, K ≤ |(↑f : ℕ → α) j| ∧ ∀ k ≥ j, |(↑f : ℕ → α) k - (↑f : ℕ → α) j| < K
h : 0 ≤ (↑f : ℕ → α) i
j : ℕ
ij : j ≥ i
this : K ≤ |(↑f : ℕ → α) j|
h₁ : K ≤ |(↑f : ℕ → α) i|
⊢ K ≤ (↑f : ℕ → α) j
have h₂ : ∀ k ≥ i, |(↑f : ℕ → α) k - (↑f : ℕ → α) i| < K
Tactic: obtain ⟨h₁, h₂⟩ := hi _ le_rfl
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.Basic (hypothesis)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
f : CauSeq α abs
h_1 : ¬f.LimZero
K : α
K0 : K > 0
hK : ∃ (i : ℕ), ∀ j ≥ i, K ≤ |(↑f : ℕ → α) j|
i : ℕ
hi : ∀ j ≥ i, K ≤ |(↑f : ℕ → α) j| ∧ ∀ k ≥ j, |(↑f : ℕ → α) k - (↑f : ℕ → α) j| < K
h : (↑f : ℕ → α) i ≤ 0
j : ℕ
ij : j ≥ i
this : K ≤ |(↑f : ℕ → α) j|
⊢ K ≤ (↑(-f) : ℕ → α) j
have h₁ : K ≤ |(↑f : ℕ → α) i|
Tactic: obtain ⟨h₁, h₂⟩ := hi _ le_rfl
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.Basic (hypothesis)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
f : CauSeq α abs
h_1 : ¬f.LimZero
K : α
K0 : K > 0
hK : ∃ (i : ℕ), ∀ j ≥ i, K ≤ |(↑f : ℕ → α) j|
i : ℕ
hi : ∀ j ≥ i, K ≤ |(↑f : ℕ → α) j| ∧ ∀ k ≥ j, |(↑f : ℕ → α) k - (↑f : ℕ → α) j| < K
h : (↑f : ℕ → α) i ≤ 0
j : ℕ
ij : j ≥ i
this : K ≤ |(↑f : ℕ → α) j|
h₁ : K ≤ |(↑f : ℕ → α) i|
⊢ K ≤ (↑(-f) : ℕ → α) j
have h₂ : ∀ k ≥ i, |(↑f : ℕ → α) k - (↑f : ℕ → α) i| < K
Tactic: obtain ⟨h₁, h₂⟩ := hi _ le_rfl
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.Basic (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
f : CauSeq α abs
h_1 : ¬f.LimZero
K : α
K0 : K > 0
hK : ∃ (i : ℕ), ∀ j ≥ i, K ≤ |(↑f : ℕ → α) j|
i : ℕ
hi : ∀ j ≥ i, K ≤ |(↑f : ℕ → α) j| ∧ ∀ k ≥ j, |(↑f : ℕ → α) k - (↑f : ℕ → α) j| < K
h : 0 ≤ (↑f : ℕ → α) i
j : ℕ
ij : j ≥ i
this : K ≤ |(↑f : ℕ → α) j|
h₁ : K ≤ |(↑f : ℕ → α) i|
h₂ : ∀ k ≥ i, |(↑f : ℕ → α) k - (↑f : ℕ → α) i| < K
⊢ K ≤ (↑f : ℕ → α) j
have inr : 0 ≤ (↑f : ℕ → α) j
Tactic: rwa [abs_of_nonneg] at this
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.Basic (hypothesis)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
f : CauSeq α abs
h_1 : ¬f.LimZero
K : α
K0 : K > 0
hK : ∃ (i : ℕ), ∀ j ≥ i, K ≤ |(↑f : ℕ → α) j|
i : ℕ
hi : ∀ j ≥ i, K ≤ |(↑f : ℕ → α) j| ∧ ∀ k ≥ j, |(↑f : ℕ → α) k - (↑f : ℕ → α) j| < K
h : 0 ≤ (↑f : ℕ → α) i
j : ℕ
ij : j ≥ i
this : K ≤ |(↑f : ℕ → α) j|
h₁ : K ≤ |(↑f : ℕ → α) i|
h₂ : ∀ k ≥ i, |(↑f : ℕ → α) k - (↑f : ℕ → α) i| < K
⊢ 0 ≤ (↑f : ℕ → α) j
have h₃ : K ≤ (↑f : ℕ → α) i
Tactic: rw [abs_of_nonneg h] at h₁
Cleared hypotheses: h₁, h₂
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.Basic (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
f : CauSeq α abs
h_1 : ¬f.LimZero
K : α
K0 : K > 0
hK : ∃ (i : ℕ), ∀ j ≥ i, K ≤ |(↑f : ℕ → α) j|
i : ℕ
hi : ∀ j ≥ i, K ≤ |(↑f : ℕ → α) j| ∧ ∀ k ≥ j, |(↑f : ℕ → α) k - (↑f : ℕ → α) j| < K
h : (↑f : ℕ → α) i ≤ 0
j : ℕ
ij : j ≥ i
this : K ≤ |(↑f : ℕ → α) j|
h₁ : K ≤ |(↑f : ℕ → α) i|
h₂ : ∀ k ≥ i, |(↑f : ℕ → α) k - (↑f : ℕ → α) i| < K
⊢ K ≤ (↑(-f) : ℕ → α) j
have inr : (↑f : ℕ → α) j ≤ 0
Tactic: rwa [abs_of_nonpos] at this
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.Basic (hypothesis)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
f : CauSeq α abs
h_1 : ¬f.LimZero
K : α
K0 : K > 0
hK : ∃ (i : ℕ), ∀ j ≥ i, K ≤ |(↑f : ℕ → α) j|
i : ℕ
hi : ∀ j ≥ i, K ≤ |(↑f : ℕ → α) j| ∧ ∀ k ≥ j, |(↑f : ℕ → α) k - (↑f : ℕ → α) j| < K
h : (↑f : ℕ → α) i ≤ 0
j : ℕ
ij : j ≥ i
this : K ≤ |(↑f : ℕ → α) j|
h₁ : K ≤ |(↑f : ℕ → α) i|
h₂ : ∀ k ≥ i, |(↑f : ℕ → α) k - (↑f : ℕ → α) i| < K
⊢ (↑f : ℕ → α) j ≤ 0
have h₃ : K ≤ -(↑f : ℕ → α) i
Tactic: rw [abs_of_nonpos h] at h₁
Cleared hypotheses: h₁, h₂
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.Basic (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
f : CauSeq α abs
h_1 : ¬f.LimZero
K : α
K0 : K > 0
hK : ∃ (i : ℕ), ∀ j ≥ i, K ≤ |(↑f : ℕ → α) j|
i : ℕ
hi : ∀ j ≥ i, K ≤ |(↑f : ℕ → α) j| ∧ ∀ k ≥ j, |(↑f : ℕ → α) k - (↑f : ℕ → α) j| < K
h : (↑f : ℕ → α) i ≤ 0
j : ℕ
ij : j ≥ i
this : K ≤ |(↑f : ℕ → α) j|
h₁ : K ≤ -(↑f : ℕ → α) i
h₂ : ∀ k ≥ i, |(↑f : ℕ → α) k - (↑f : ℕ → α) i| < K
⊢ (↑f : ℕ → α) j ≤ 0
have inr : (↑f : ℕ → α) j - (↑f : ℕ → α) i ≤ -(↑f : ℕ → α) i
Tactic: rw [← sub_le_sub_iff_right, zero_sub]
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.Basic (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
f g h : CauSeq α abs
fg : f < g
gh : g ≈ h
⊢ (h - f).Pos
have h₁ : h - f = g - f + -(g - h)
Tactic: convert! pos_add_limZero fg (neg_limZero gh) using 1
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.Basic (hypothesis)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
f g h : CauSeq α abs
fg : f ≈ g
gh : g < h
⊢ f < h
have this : (h - g + -(f - g)).Pos
Tactic: have := pos_add_limZero gh (neg_limZero fg)
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.Basic (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
f g h : CauSeq α abs
fg : f ≈ g
gh : g < h
this : (h - g + -(f - g)).Pos
⊢ f < h
have rwa : ∀ (this : (h - g - (f - g)).Pos), f < h
Tactic: rwa [← sub_eq_add_neg, sub_sub_sub_cancel_right] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.Basic (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
f g h : CauSeq α abs
fg : f ≈ g
gh : g < h
this : (h - g + -(f - g)).Pos
rwa : ∀ (this : (h - g - (f - g)).Pos), f < h
⊢ f < h
have rwa₁ : ∀ (this : (h - f).Pos), f < h
Tactic: rwa [← sub_eq_add_neg, sub_sub_sub_cancel_right] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.Basic (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
f g h : CauSeq α abs
fg : f < g
gh : g < h
⊢ (h - f).Pos
have h₁ : h - f = g - f + (h - g)
Tactic: convert! add_pos fg gh using 1
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.Basic (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
f g : CauSeq α abs
h_1 : (g - f).LimZero ∨ (-(g - f)).Pos
h : (-(g - f)).Pos
⊢ g < f
have rwa : ∀ (h : (f - g).Pos), g < f
Tactic: rwa [neg_sub] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.Basic (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
x y : α
⊢ (HSub.hSub (α := CauSeq α abs) (const y) (const x)).Pos ↔ x < y
have rw : Pos (const (y - x)) ↔ x < y
Tactic: rw [← const_sub, const_pos, sub_pos]
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.Basic (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
x y : α
rw : Pos (const (y - x)) ↔ x < y
⊢ (HSub.hSub (α := CauSeq α abs) (const y) (const x)).Pos ↔ x < y
have rw₁ : 0 < y - x ↔ x < y
Tactic: rw [← const_sub, const_pos, sub_pos]
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.Basic (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
x y : α
rw : Pos (const (y - x)) ↔ x < y
rw₁ : 0 < y - x ↔ x < y
⊢ (HSub.hSub (α := CauSeq α abs) (const y) (const x)).Pos ↔ x < y
have rw₂ : x < y ↔ x < y
Tactic: rw [← const_sub, const_pos, sub_pos]
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.Basic (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
x y : α
⊢ LE.le (α := CauSeq α abs) (const x) (const y) ↔ x ≤ y
have rw : LE.le (α := CauSeq α abs) (const x) (const y) ↔ x < y ∨ x = y
Tactic: rw [le_iff_lt_or_eq]
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.Basic (goal)
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
⊢ 1 ≤ (↑(const (K + 1) - f) : ℕ → α) i
have rw : (↑f : ℕ → α) i ≤ K
Tactic: rw [sub_apply, const_apply, le_sub_iff_add_le', add_le_add_iff_right]
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.Basic (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
f : CauSeq α abs
a : α
h : -f < const a
⊢ (f - const (-a)).Pos
have rwa : (f - -const a).Pos
Tactic: rwa [const_neg, sub_neg_eq_add, add_comm, ← sub_neg_eq_add]
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.Basic (goal)
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
⊢ (f - const (-a)).Pos
have rwa₁ : (f + const a).Pos
Tactic: rwa [const_neg, sub_neg_eq_add, add_comm, ← sub_neg_eq_add]
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.Basic (goal)
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
⊢ (f - const (-a)).Pos
have rwa₂ : (const a + f).Pos
Tactic: rwa [const_neg, sub_neg_eq_add, add_comm, ← sub_neg_eq_add]
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.Basic (goal)
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
⊢ (f - const (-a)).Pos
have rwa₃ : (const a - -f).Pos
Tactic: rwa [const_neg, sub_neg_eq_add, add_comm, ← sub_neg_eq_add]
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.Basic (hypothesis)
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 ⊔ g) : ℕ → α) j| < ε
have H₁ : |(↑f : ℕ → α) j| < ε
Tactic: let ⟨H₁, H₂⟩ := H _ ij
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.Basic (hypothesis)
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 ⊔ g) : ℕ → α) j| < ε
have H₂ : |(↑g : ℕ → α) j| < ε
Tactic: let ⟨H₁, H₂⟩ := H _ ij
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.Basic (goal)
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| < ε
⊢ |(↑(f ⊔ g) : ℕ → α) j| < ε
have rw : ∀ (H₁ : -ε < (↑f : ℕ → α) j ∧ (↑f : ℕ → α) j < ε) (H₂ : -ε < (↑g : ℕ → α) j ∧ (↑g : ℕ → α) j < ε),
  -ε < (↑(f ⊔ g) : ℕ → α) j ∧ (↑(f ⊔ g) : ℕ → α) j < ε
Tactic: rw [abs_lt] at H₁ H₂ ⊢
Cleared hypotheses: H₁, H₂
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.Basic (hypothesis)
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 ⊓ g) : ℕ → α) j| < ε
have H₁ : |(↑f : ℕ → α) j| < ε
Tactic: let ⟨H₁, H₂⟩ := H _ ij
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.Basic (hypothesis)
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 ⊓ g) : ℕ → α) j| < ε
have H₂ : |(↑g : ℕ → α) j| < ε
Tactic: let ⟨H₁, H₂⟩ := H _ ij
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.Basic (goal)
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| < ε
⊢ |(↑(f ⊓ g) : ℕ → α) j| < ε
have rw : ∀ (H₁ : -ε < (↑f : ℕ → α) j ∧ (↑f : ℕ → α) j < ε) (H₂ : -ε < (↑g : ℕ → α) j ∧ (↑g : ℕ → α) j < ε),
  -ε < (↑(f ⊓ g) : ℕ → α) j ∧ (↑(f ⊓ g) : ℕ → α) j < ε
Tactic: rw [abs_lt] at H₁ H₂ ⊢
Cleared hypotheses: H₁, H₂
-- 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₁ a₂ b₂ : CauSeq α abs
ha : a₁ ≈ a₂
hb : b₁ ≈ b₂
ε : α
ε0 : ε > 0
⊢ ∃ (i : ℕ), ∀ j ≥ i, |(↑(a₁ ⊔ b₁ - a₂ ⊔ b₂) : ℕ → α) j| < ε
have obtain : ∀ (ai : ℕ) (hai : ∀ j ≥ ai, |(↑(a₁ - a₂) : ℕ → α) j| < ε), ∃ (i : ℕ), ∀ j ≥ i, |(↑(a₁ ⊔ b₁ - a₂ ⊔ b₂) : ℕ → α) j| < ε
Tactic: obtain ⟨ai, hai⟩ := ha ε ε0
-- 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₁ a₂ b₂ : CauSeq α abs
ha : a₁ ≈ a₂
hb : b₁ ≈ b₂
ε : α
ε0 : ε > 0
ai : ℕ
hai : ∀ j ≥ ai, |(↑(a₁ - a₂) : ℕ → α) j| < ε
⊢ ∃ (i : ℕ), ∀ j ≥ i, |(↑(a₁ ⊔ b₁ - a₂ ⊔ b₂) : ℕ → α) j| < ε
have obtain : ∀ (bi : ℕ) (hbi : ∀ j ≥ bi, |(↑(b₁ - b₂) : ℕ → α) j| < ε), ∃ (i : ℕ), ∀ j ≥ i, |(↑(a₁ ⊔ b₁ - a₂ ⊔ b₂) : ℕ → α) j| < ε
Tactic: obtain ⟨bi, hbi⟩ := hb ε ε0
-- 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₁ a₂ b₂ : CauSeq α abs
ha : a₁ ≈ a₂
hb : b₁ ≈ b₂
ε : α
ε0 : ε > 0
⊢ ∃ (i : ℕ), ∀ j ≥ i, |(↑(a₁ ⊓ b₁ - a₂ ⊓ b₂) : ℕ → α) j| < ε
have obtain : ∀ (ai : ℕ) (hai : ∀ j ≥ ai, |(↑(a₁ - a₂) : ℕ → α) j| < ε), ∃ (i : ℕ), ∀ j ≥ i, |(↑(a₁ ⊓ b₁ - a₂ ⊓ b₂) : ℕ → α) j| < ε
Tactic: obtain ⟨ai, hai⟩ := ha ε ε0
-- 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₁ a₂ b₂ : CauSeq α abs
ha : a₁ ≈ a₂
hb : b₁ ≈ b₂
ε : α
ε0 : ε > 0
ai : ℕ
hai : ∀ j ≥ ai, |(↑(a₁ - a₂) : ℕ → α) j| < ε
⊢ ∃ (i : ℕ), ∀ j ≥ i, |(↑(a₁ ⊓ b₁ - a₂ ⊓ b₂) : ℕ → α) j| < ε
have obtain : ∀ (bi : ℕ) (hbi : ∀ j ≥ bi, |(↑(b₁ - b₂) : ℕ → α) j| < ε), ∃ (i : ℕ), ∀ j ≥ i, |(↑(a₁ ⊓ b₁ - a₂ ⊓ b₂) : ℕ → α) j| < ε
Tactic: obtain ⟨bi, hbi⟩ := hb ε ε0
-- 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 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
Tactic: obtain ⟨⟨εa, εa0, ia, ha⟩, ⟨εb, εb0, ib, hb⟩⟩ := ha, hb
Cleared hypotheses: ha, 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
ε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
have refine : ∀ (i : ℕ) (hi : i ≥ max ia ib), min εa εb ≤ (↑(c - a ⊔ b) : ℕ → α) i
Tactic: refine ⟨εa ⊓ εb, lt_inf_iff.mpr ⟨εa0, εb0⟩, ia ⊔ ib, fun i hi => ?_⟩
-- 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
ε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 ≤ (↑(c - a ⊔ b) : ℕ → α) i
have this : 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)
-- 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 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
Tactic: obtain ⟨⟨εb, εb0, ib, hb⟩, ⟨εc, εc0, ic, hc⟩⟩ := hb, hc
Cleared hypotheses: hb, 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
ε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
have refine : ∀ (i : ℕ) (hi : i ≥ max ib ic), min εb εc ≤ (↑(b ⊓ c - a) : ℕ → α) i
Tactic: refine ⟨εb ⊓ εc, lt_inf_iff.mpr ⟨εb0, εc0⟩, ib ⊔ ic, fun i hi => ?_⟩
-- 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
ε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 ≤ (↑(b ⊓ c - a) : ℕ → α) i
have this : 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)
-- 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 : a ≤ b
⊢ a ⊔ b ≈ b
have inl : ∀ (ε : α) (ε0 : 0 < ε) (i : ℕ) (h : ∀ j ≥ i, ε ≤ (↑(b - a) : ℕ → α) j), a ⊔ b ≈ b
Tactic: obtain ⟨ε, ε0 : _ < _, i, h⟩ | h := h
Cleared hypotheses: h
-- 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 : a ≤ b
inl : ∀ (ε : α) (ε0 : 0 < ε) (i : ℕ) (h : ∀ j ≥ i, ε ≤ (↑(b - a) : ℕ → α) j), a ⊔ b ≈ b
⊢ a ⊔ b ≈ b
have inr : ∀ (h : a ≈ b), a ⊔ b ≈ b
Tactic: obtain ⟨ε, ε0 : _ < _, i, h⟩ | h := h
Cleared hypotheses: h
-- 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, ε ≤ (↑(b - a) : ℕ → α) 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, ε ≤ (↑(b - a) : ℕ → α) j
ε_1 : α
h_1 : ε_1 > 0
j : ℕ
hj : j ≥ i
⊢ |(↑(a ⊔ b - b) : ℕ → α) j| < ε_1
have inl : |max ((↑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, ε ≤ (↑(b - a) : ℕ → α) j
ε_1 : α
h_1 : ε_1 > 0
j : ℕ
hj : j ≥ i
⊢ |max ((↑a : ℕ → α) j) ((↑b : ℕ → α) j) - (↑b : ℕ → α) j| < ε_1
have inl : |max ((↑a : ℕ → α) j - (↑b : ℕ → α) j) ((↑b : ℕ → α) j - (↑b : ℕ → α) j)| < ε_1
Tactic: rw [← max_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, ε ≤ (↑(b - a) : ℕ → α) j
ε_1 : α
h_1 : ε_1 > 0
j : ℕ
hj : j ≥ i
⊢ |max ((↑a : ℕ → α) j - (↑b : ℕ → α) j) ((↑b : ℕ → α) j - (↑b : ℕ → α) j)| < ε_1
have inl : (↑a : ℕ → α) j - (↑b : ℕ → α) j ≤ 0
Tactic: rwa [sub_self, max_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
ε : α
ε0 : 0 < ε
i : ℕ
h : ∀ j ≥ i, ε ≤ (↑(b - a) : ℕ → α) j
ε_1 : α
h_1 : ε_1 > 0
j : ℕ
hj : j ≥ i
⊢ (↑a : ℕ → α) j - (↑b : ℕ → α) j ≤ 0
have inl : 0 ≤ (↑b : ℕ → α) j - (↑a : ℕ → α) j
Tactic: rw [sub_nonpos, ← sub_nonneg]
-- 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 : a ≈ b
⊢ a ⊔ b ≈ b
have inr : b ⊔ b ≈ b
Tactic: refine Setoid.trans (sup_equiv_sup 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 : a ≈ b
⊢ b ⊔ b ≈ b
have inr : (equiv : CauSeq α abs → CauSeq α abs → Prop) b b
Tactic: rw [CauSeq.sup_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 : CauSeq α abs
h : b ≤ a
⊢ a ⊓ b ≈ b
have inl : ∀ (ε : α) (ε0 : 0 < ε) (i : ℕ) (h : ∀ j ≥ i, ε ≤ (↑(a - b) : ℕ → α) j), a ⊓ b ≈ b
Tactic: obtain ⟨ε, ε0 : _ < _, i, h⟩ | h := h
Cleared hypotheses: h
-- 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
inl : ∀ (ε : α) (ε0 : 0 < ε) (i : ℕ) (h : ∀ j ≥ i, ε ≤ (↑(a - b) : ℕ → α) j), a ⊓ b ≈ b
⊢ a ⊓ b ≈ b
have inr : ∀ (h : b ≈ a), a ⊓ b ≈ b
Tactic: obtain ⟨ε, ε0 : _ < _, i, h⟩ | h := h
Cleared hypotheses: h