awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Ring β
abv : β → α
inst_4 : IsAbsoluteValue abv
f1 f2 : CauSeq β abv
hf : f1 ≈ f2
n : ℕ
zero : HPow.hPow (β := ℕ) f1 0 ≈ HPow.hPow (β := ℕ) f2 0
succ : ∀ (n : ℕ) (ih : f1 ^ n ≈ f2 ^ n), f1 ^ (n + 1) ≈ f2 ^ (n + 1)
⊢ f1 ^ n ≈ f2 ^ n

Tactic:
induction n with
  | zero => simp only [pow_zero, Setoid.refl]
  | succ n ih => simpa only [pow_succ'] using mul_equiv_mul hf ih

Premises used: pow_zero, Setoid.refl, pow_succ'
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Ring β
inst_4 : IsDomain β
abv : β → α
inst_5 : IsAbsoluteValue abv
h : HasEquiv.Equiv (α := CauSeq β abv) (const abv 1) (const abv 0)
this : ∀ ε > 0, ∃ (i : ℕ), ∀ (k : ℕ), i ≤ k → abv (HSub.hSub (α := β) 1 0) < ε
h2 : 0 < abv 1
i : ℕ
hi : ∀ (k : ℕ), i ≤ k → abv (HSub.hSub (α := β) 1 0) < abv 1
⊢ abv 1 < abv 1

Tactic:
simpa using hi _ le_rfl

Premises used: le_rfl
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : DivisionRing β
abv : β → α
inst_4 : IsAbsoluteValue abv
f : CauSeq β abv
hf : ¬f.LimZero
⊢ (↑(f.inv hf) : ℕ → β) = (↑f : ℕ → β)⁻¹

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : DivisionRing β
abv : β → α
inst_4 : IsAbsoluteValue abv
f : CauSeq β abv
hf : ¬f.LimZero
i : ℕ
⊢ (↑(f.inv hf) : ℕ → β) i = ((↑f : ℕ → β) i)⁻¹

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : DivisionRing β
abv : β → α
inst_4 : IsAbsoluteValue abv
f : CauSeq β abv
hf : ¬f.LimZero
ε : α
ε0 : ε > 0
K : α
K0 : K > 0
i : ℕ
H : ∀ j ≥ i, K ≤ abv ((↑f : ℕ → β) j)
j : ℕ
ij : j ≥ i
⊢ abv ((↑(f.inv hf * f - 1) : ℕ → β) j) < ε

Tactic:
simpa [(abv_pos abv).1 (lt_of_lt_of_le K0 (H _ ij)), abv_zero abv] using ε0

Premises used: IsAbsoluteValue.abv_zero, Iff.mp, lt_of_lt_of_le, IsAbsoluteValue.abv_pos
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : DivisionRing β
abv : β → α
inst_4 : IsAbsoluteValue abv
f : CauSeq β abv
hf : ¬f.LimZero
ε : α
ε0 : ε > 0
K : α
K0 : K > 0
i : ℕ
H : ∀ j ≥ i, K ≤ abv ((↑f : ℕ → β) j)
j : ℕ
ij : j ≥ i
⊢ abv ((↑(f * f.inv hf - 1) : ℕ → β) j) < ε

Tactic:
simpa [(abv_pos abv).1 (lt_of_lt_of_le K0 (H _ ij)), abv_zero abv] using ε0

Premises used: IsAbsoluteValue.abv_zero, Iff.mp, lt_of_lt_of_le, IsAbsoluteValue.abv_pos
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : DivisionRing β
abv : β → α
inst_4 : IsAbsoluteValue abv
x : β
hx : x ≠ 0
rwa rwa₁ rwa₂ rwa₃ : ¬x = 0
⊢ ¬LimZero (const abv x)

Tactic:
rwa [const_limZero]

Premises used: CauSeq.const_limZero
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : DivisionRing β
abv : β → α
inst_4 : IsAbsoluteValue abv
x : β
hx : x ≠ 0
⊢ Eq (α := CauSeq β abv) (const abv x⁻¹) (inv (const abv x) ⋯)

Tactic:
rfl

Premises used: CauSeq.inv, CauSeq.const, rfl
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
x : α
⊢ Pos (const x) ↔ 0 < x

Tactic:
⟨fun ⟨_, K0, _, h⟩ => lt_of_lt_of_le K0 (h _ le_rfl), fun h => ⟨x, h, 0, fun _ _ => le_rfl⟩⟩

Premises used: le_rfl, And.intro, LT.lt, Iff.intro, Exists.intro, OfNat.ofNat, _private.0.CauSeq.const_pos.match_1, lt_of_lt_of_le
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
f g : CauSeq α abs
F : α
F0 : F > 0
hF : ∃ (i : ℕ), ∀ j ≥ i, F ≤ (↑f : ℕ → α) j
H : g.LimZero
i : ℕ
h : ∀ j ≥ i, F ≤ (↑f : ℕ → α) j ∧ |(↑g : ℕ → α) j| < F / 2
j : ℕ
ij : j ≥ i
⊢ F ≤ (↑f : ℕ → α) j

Tactic:
obtain ⟨h₁, h₂⟩ := h j ij
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
f g : CauSeq α abs
F : α
F0 : F > 0
hF : ∃ (i : ℕ), ∀ j ≥ i, F ≤ (↑f : ℕ → α) j
H : g.LimZero
i : ℕ
h : ∀ j ≥ i, F ≤ (↑f : ℕ → α) j ∧ |(↑g : ℕ → α) j| < F / 2
j : ℕ
ij : j ≥ i
h₁ : F ≤ (↑f : ℕ → α) j
⊢ |(↑g : ℕ → α) j| < F / 2

Tactic:
obtain ⟨h₁, h₂⟩ := h j ij
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
f g : CauSeq α abs
F : α
F0 : F > 0
hF : ∃ (i : ℕ), ∀ j ≥ i, F ≤ (↑f : ℕ → α) j
H : g.LimZero
i : ℕ
h : ∀ j ≥ i, F ≤ (↑f : ℕ → α) j ∧ |(↑g : ℕ → α) j| < F / 2
j : ℕ
ij : j ≥ i
h₁ : F ≤ (↑f : ℕ → α) j
h₂ : |(↑g : ℕ → α) j| < F / 2
⊢ F + -(F / 2) ≤ (↑f : ℕ → α) j + (↑g : ℕ → α) j

Tactic:
have := add_le_add h₁ (le_of_lt (abs_lt.1 h₂).1)
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
f g : CauSeq α abs
F : α
F0 : F > 0
hF : ∃ (i : ℕ), ∀ j ≥ i, F ≤ (↑f : ℕ → α) j
H : g.LimZero
i : ℕ
h : ∀ j ≥ i, F ≤ (↑f : ℕ → α) j ∧ |(↑g : ℕ → α) j| < F / 2
j : ℕ
ij : j ≥ i
h₁ : F ≤ (↑f : ℕ → α) j
h₂ : |(↑g : ℕ → α) j| < F / 2
this : F + -(F / 2) ≤ (↑f : ℕ → α) j + (↑g : ℕ → α) j
rwa : ∀ (this : F - F / 2 ≤ (↑f : ℕ → α) j + (↑g : ℕ → α) j), F / 2 ≤ (↑(f + g) : ℕ → α) j
rwa₁ rwa₂ rwa₃ rwa₄ : ∀ (this : F / 2 ≤ (↑f : ℕ → α) j + (↑g : ℕ → α) j), F / 2 ≤ (↑(f + g) : ℕ → α) j
⊢ F / 2 ≤ (↑(f + g) : ℕ → α) j

Tactic:
rwa [← sub_eq_add_neg, sub_self_div_two] at this

Premises used: sub_eq_add_neg, sub_self_div_two
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
f : CauSeq α abs
inl : ∀ (h : f.LimZero), f.Pos ∨ f.LimZero ∨ (-f).Pos
inr : ∀ (h : ¬f.LimZero), f.Pos ∨ f.LimZero ∨ (-f).Pos
⊢ f.Pos ∨ f.LimZero ∨ (-f).Pos

Tactic:
rcases Classical.em (LimZero f) with h | h

Premises used: Classical.em, CauSeq.LimZero
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
f : CauSeq α abs
h : f.LimZero
⊢ f.Pos ∨ f.LimZero ∨ (-f).Pos

Tactic:
simp [*]
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
f : CauSeq α abs
h : ¬f.LimZero
inr : f.Pos ∨ (-f).Pos
⊢ f.Pos ∨ f.LimZero ∨ (-f).Pos

Tactic:
simp only [false_or, h]

Premises used: false_or
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
f : CauSeq α abs
h : ¬f.LimZero
inr : ∀ (K : α) (K0 : K > 0) (hK : ∃ (i : ℕ), ∀ j ≥ i, K ≤ |(↑f : ℕ → α) j|), f.Pos ∨ (-f).Pos
⊢ f.Pos ∨ (-f).Pos

Tactic:
rcases abv_pos_of_not_limZero h with ⟨K, K0, hK⟩

Premises used: CauSeq.abv_pos_of_not_limZero
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
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|
inr : ∀ (i : ℕ) (hi : ∀ j ≥ i, K ≤ |(↑f : ℕ → α) j| ∧ ∀ k ≥ j, |(↑f : ℕ → α) k - (↑f : ℕ → α) j| < K), f.Pos ∨ (-f).Pos
⊢ f.Pos ∨ (-f).Pos

Tactic:
rcases exists_forall_ge_and hK (f.cauchy₃ K0) with ⟨i, hi⟩

Premises used: exists_forall_ge_and, CauSeq.cauchy₃
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
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.Pos ∨ (-f).Pos

Tactic:
(le_total 0 (f i)).imp ?_ ?_

Premises used: le_total, Or.imp, OfNat.ofNat, Subtype.val
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
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
inr : 0 ≤ (↑f : ℕ → α) i → f.Pos
inr₁ : (↑f : ℕ → α) i ≤ 0 → (-f).Pos
⊢ f.Pos ∨ (-f).Pos

Tactic:
refine (le_total 0 (f i)).imp ?_ ?_

Premises used: le_total, Or.imp, OfNat.ofNat, Subtype.val
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
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

Tactic:
fun h => ⟨K, K0, i, fun j ij => ?_⟩

Premises used: CauSeq.Pos, And.intro, Exists.intro
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
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
inr : ∀ (h : 0 ≤ (↑f : ℕ → α) i) (j : ℕ) (ij : j ≥ i), K ≤ (↑f : ℕ → α) j
⊢ 0 ≤ (↑f : ℕ → α) i → f.Pos

Tactic:
refine fun h => ⟨K, K0, i, fun j ij => ?_⟩
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
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

Tactic:
fun h => ⟨K, K0, i, fun j ij => ?_⟩

Premises used: CauSeq.Pos, And.intro, Exists.intro
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
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
inr : ∀ (h : (↑f : ℕ → α) i ≤ 0) (j : ℕ) (ij : j ≥ i), K ≤ (↑(-f) : ℕ → α) j
⊢ (↑f : ℕ → α) i ≤ 0 → (-f).Pos

Tactic:
refine fun h => ⟨K, K0, i, fun j ij => ?_⟩
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
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|

Tactic:
have := (hi _ ij).1
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
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|

Tactic:
have := (hi _ ij).1
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
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 : ℕ → α) i|

Tactic:
obtain ⟨h₁, h₂⟩ := hi _ le_rfl

Premises used: le_rfl
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
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 ≥ i, |(↑f : ℕ → α) k - (↑f : ℕ → α) i| < K

Tactic:
obtain ⟨h₁, h₂⟩ := hi _ le_rfl

Premises used: le_rfl
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
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 : ℕ → α) i|

Tactic:
obtain ⟨h₁, h₂⟩ := hi _ le_rfl

Premises used: le_rfl
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
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 ≥ i, |(↑f : ℕ → α) k - (↑f : ℕ → α) i| < K

Tactic:
obtain ⟨h₁, h₂⟩ := hi _ le_rfl

Premises used: le_rfl
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
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
inr : 0 ≤ (↑f : ℕ → α) j
⊢ K ≤ (↑f : ℕ → α) j

Tactic:
rwa [abs_of_nonneg] at this

Premises used: abs_of_nonneg
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
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 : ℕ → α) i

Tactic:
rw [abs_of_nonneg h] at h₁

Premises used: abs_of_nonneg
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
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
h₃ : K ≤ (↑f : ℕ → α) i
⊢ ∀ k ≥ i, |(↑f : ℕ → α) k - (↑f : ℕ → α) i| < K

Tactic:
rw [abs_of_nonneg h] at h₁

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

Tactic:
(le_add_iff_nonneg_right _).1
        (le_trans h₁ <| neg_le_sub_iff_le_add'.1 <| le_of_lt (abs_lt.1 <| h₂ _ ij).1)

Premises used: le_add_iff_nonneg_right, le_of_lt, neg_le_sub_iff_le_add', And.left, Iff.mp, abs_lt, le_trans
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
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

Tactic:
exact
      (le_add_iff_nonneg_right _).1
        (le_trans h₁ <| neg_le_sub_iff_le_add'.1 <| le_of_lt (abs_lt.1 <| h₂ _ ij).1)

Premises used: le_add_iff_nonneg_right, le_of_lt, neg_le_sub_iff_le_add', And.left, Iff.mp, abs_lt, le_trans
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
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
inr : (↑f : ℕ → α) j ≤ 0
⊢ K ≤ (↑(-f) : ℕ → α) j

Tactic:
rwa [abs_of_nonpos] at this

Premises used: abs_of_nonpos
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
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 : ℕ → α) i

Tactic:
rw [abs_of_nonpos h] at h₁

Premises used: abs_of_nonpos
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
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
h₃ : K ≤ -(↑f : ℕ → α) i
⊢ ∀ k ≥ i, |(↑f : ℕ → α) k - (↑f : ℕ → α) i| < K

Tactic:
rw [abs_of_nonpos h] at h₁

Premises used: abs_of_nonpos
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
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
inr : (↑f : ℕ → α) j - (↑f : ℕ → α) i ≤ -(↑f : ℕ → α) i
inr₁ : α
⊢ (↑f : ℕ → α) j ≤ 0

Tactic:
rw [← sub_le_sub_iff_right, zero_sub]

Premises used: sub_le_sub_iff_right, zero_sub
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
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 - (↑f : ℕ → α) i ≤ -(↑f : ℕ → α) i

Tactic:
le_trans (le_of_lt (abs_lt.1 <| h₂ _ ij).2) h₁

Premises used: le_of_lt, And.right, Iff.mp, abs_lt, le_trans
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
f g h : CauSeq α abs
fg : f < g
gh : g ≈ h
⊢ (g - f + -(g - h)).Pos

Tactic:
pos_add_limZero fg (neg_limZero gh)

Premises used: CauSeq.pos_add_limZero, CauSeq.neg_limZero
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
f g h : CauSeq α abs
fg : f < g
gh : g ≈ h
h₁ : h - f = g - f + -(g - h)
⊢ (h - f).Pos

Tactic:
convert! pos_add_limZero fg (neg_limZero gh) using 1

Premises used: CauSeq.pos_add_limZero, CauSeq.neg_limZero
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
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 = g - f + -(g - h)

Tactic:
simp
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
f g h : CauSeq α abs
fg : f ≈ g
gh : g < h
⊢ (h - g + -(f - g)).Pos

Tactic:
have := pos_add_limZero gh (neg_limZero fg)
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
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
rwa₁ rwa₂ rwa₃ rwa₄ : ∀ (this : (h - f).Pos), f < h
⊢ f < h

Tactic:
rwa [← sub_eq_add_neg, sub_sub_sub_cancel_right] at this

Premises used: sub_sub_sub_cancel_right, sub_eq_add_neg
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
f g h : CauSeq α abs
fg : f < g
gh : g < h
⊢ (g - f + (h - g)).Pos

Tactic:
add_pos fg gh

Premises used: CauSeq.add_pos
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
f g h : CauSeq α abs
fg : f < g
gh : g < h
h₁ : h - f = g - f + (h - g)
⊢ (h - f).Pos

Tactic:
convert! add_pos fg gh using 1

Premises used: CauSeq.add_pos
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
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 = g - f + (h - g)

Tactic:
simp
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
f : CauSeq α abs
h_1 : f < f
h : f < f := h_1
⊢ (f - f).LimZero

Tactic:
simp [zero_limZero]

Premises used: CauSeq.zero_limZero
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
f g h : CauSeq α abs
hfg : f ≈ g
hgh : g ≤ h
⊢ f ≤ h

Tactic:
hgh.elim (Or.inl ∘ CauSeq.lt_of_eq_of_lt hfg) (Or.inr ∘ Setoid.trans hfg)

Premises used: CauSeq.lt_of_eq_of_lt, Function.comp, Setoid.trans, Or.inl, Or.elim, Or.inr
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
f g h : CauSeq α abs
hfg : f ≤ g
hgh : g ≈ h
⊢ f ≤ h

Tactic:
hfg.elim (fun h => Or.inl (CauSeq.lt_of_lt_of_eq h hgh)) fun h => Or.inr (Setoid.trans h hgh)

Premises used: Setoid.trans, CauSeq.lt_of_lt_of_eq, Or.inl, Or.elim, Or.inr
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
f g : CauSeq α abs
fg : f ≤ g
gf : g ≤ f
⊢ f ≈ g

Tactic:
fg.resolve_left (not_lt_of_ge gf)

Premises used: Or.resolve_left, not_lt_of_ge
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
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
rwa rwa₁ rwa₂ rwa₃ : ∀ (h : (f - g).Pos), g < f
⊢ g < f

Tactic:
rwa [neg_sub] at h

Premises used: neg_sub
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
f g : CauSeq α abs
⊢ f ≤ g ∨ g ≤ f

Tactic:
(or_assoc.2 (lt_total f g)).imp_right Or.inl

Premises used: Iff.mpr, Or.inl, CauSeq.lt_total, Or.imp_right, or_assoc
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
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
rw₂ rw₃ : x < y ↔ x < y
⊢ (HSub.hSub (α := CauSeq α abs) (const y) (const x)).Pos ↔ x < y

Tactic:
rw [← const_sub, const_pos, sub_pos]

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

Tactic:
rw [le_iff_lt_or_eq]

Premises used: le_iff_lt_or_eq