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
i : ℕ
⊢ Eq.{u_2 + 1} (α := β) ((↑1 : ℕ → β) i) 1

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 : Ring β
abv : β → α
inst_4 : IsAbsoluteValue abv
⊢ Eq (α := CauSeq β abv) (const 0) 0

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 : Ring β
abv : β → α
inst_4 : IsAbsoluteValue abv
⊢ Eq (α := CauSeq β abv) (const 1) 1

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 : Ring β
abv : β → α
inst_4 : IsAbsoluteValue abv
x y : β
⊢ const (x + y) = HAdd.hAdd (α := CauSeq β abv) (const x) (const y)

Tactic:
rfl

Premises used: CauSeq.const, rfl
-- 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
f g : CauSeq β abv
⊢ (↑(f * g) : ℕ → β) = (↑f : ℕ → β) * (↑g : ℕ → β)

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 : Ring β
abv : β → α
inst_4 : IsAbsoluteValue abv
f g : CauSeq β abv
i : ℕ
⊢ (↑(f * g) : ℕ → β) i = (↑f : ℕ → β) i * (↑g : ℕ → β) 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 : Ring β
abv : β → α
inst_4 : IsAbsoluteValue abv
x y : β
⊢ const (x * y) = HMul.hMul (α := CauSeq β abv) (const x) (const y)

Tactic:
rfl

Premises used: CauSeq.const, rfl
-- 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
f : CauSeq β abv
⊢ (↑(-f) : ℕ → β) = -(↑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 : Ring β
abv : β → α
inst_4 : IsAbsoluteValue abv
f : CauSeq β abv
i : ℕ
⊢ (↑(-f) : ℕ → β) 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 : Ring β
abv : β → α
inst_4 : IsAbsoluteValue abv
x : β
⊢ Eq (α := CauSeq β abv) (const (-x)) (-const x)

Tactic:
rfl

Premises used: CauSeq.const, rfl
-- 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
f g : CauSeq β abv
i : ℕ
⊢ (↑(f + -g) : ℕ → β) i = (fun (x : ℕ) ↦ (↑f : ℕ → β) x - (↑g : ℕ → β) x) i

Tactic:
simp [sub_eq_add_neg]

Premises used: sub_eq_add_neg
-- 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
f g : CauSeq β abv
⊢ (↑(f - g) : ℕ → β) = (↑f : ℕ → β) - (↑g : ℕ → β)

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 : Ring β
abv : β → α
inst_4 : IsAbsoluteValue abv
f g : CauSeq β abv
i : ℕ
⊢ (↑(f - g) : ℕ → β) i = (↑f : ℕ → β) i - (↑g : ℕ → β) 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 : Ring β
abv : β → α
inst_4 : IsAbsoluteValue abv
x y : β
⊢ const (x - y) = HSub.hSub (α := CauSeq β abv) (const x) (const y)

Tactic:
rfl

Premises used: CauSeq.ofEq, CauSeq.const, rfl
-- 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
G : Type u_3
inst_5 : SMul G β
inst_6 : IsScalarTower G β β
a : G
f : CauSeq β abv
⊢ (↑(a • f) : ℕ → β) = a • (↑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 : Ring β
abv : β → α
inst_4 : IsAbsoluteValue abv
G : Type u_3
inst_5 : SMul G β
inst_6 : IsScalarTower G β β
a : G
f : CauSeq β abv
i : ℕ
⊢ (↑(a • f) : ℕ → β) i = a • (↑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 : Ring β
abv : β → α
inst_4 : IsAbsoluteValue abv
G : Type u_3
inst_5 : SMul G β
inst_6 : IsScalarTower G β β
a : G
x : β
⊢ const (a • x) = HSMul.hSMul (β := CauSeq β abv) a (const x)

Tactic:
rfl

Premises used: CauSeq.ofEq, CauSeq.const, rfl
-- 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
G : Type u_3
inst_5 : SMul G β
inst_6 : IsScalarTower G β β
⊢ IsScalarTower.{u_3, u_2, u_2} G (CauSeq β abv) (CauSeq β abv)

Tactic:
⟨fun a f g => Subtype.ext <| smul_assoc a (f : ℕ → β) (g : ℕ → β)⟩

Premises used: smul_assoc, IsScalarTower.mk, Subtype.val, Subtype.ext
-- 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
n : ℕ
x : CauSeq β abv
⊢ (↑(n • x) : ℕ → β) = n • (↑x : ℕ → β)

Tactic:
rfl
-- 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
n : ℤ
x : CauSeq β abv
⊢ (↑(n • x) : ℕ → β) = n • (↑x : ℕ → β)

Tactic:
rfl
-- 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
n : ℕ
⊢ Eq.{u_2 + 1} (α := ℕ → β) (↑(↑n : CauSeq β abv) : ℕ → β) (↑n : ℕ → β)

Tactic:
rfl
-- 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
n : ℤ
⊢ Eq.{u_2 + 1} (α := ℕ → β) (↑(↑n : CauSeq β abv) : ℕ → β) (↑n : ℕ → β)

Tactic:
rfl
-- 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
f : CauSeq β abv
n : ℕ
zero : ∀ (i : ℕ), (↑(npowRec 0 f) : ℕ → β) i = HPow.hPow (β := ℕ) ((↑f : ℕ → β) i) 0
succ :
  ∀ (n : ℕ),
    (∀ (i : ℕ), (↑(npowRec n f) : ℕ → β) i = (↑f : ℕ → β) i ^ n) →
      ∀ (i : ℕ), (↑(npowRec (n + 1) f) : ℕ → β) i = (↑f : ℕ → β) i ^ (n + 1)
⊢ ∀ (i : ℕ), (↑(npowRec n f) : ℕ → β) i = (↑f : ℕ → β) i ^ n

Tactic:
induction n
-- 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
f : CauSeq β abv
⊢ ∀ (i : ℕ), (↑(npowRec 0 f) : ℕ → β) i = HPow.hPow (β := ℕ) ((↑f : ℕ → β) i) 0

Tactic:
simp [*, npowRec, pow_succ]

Premises used: pow_succ, npowRec
-- 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
f : CauSeq β abv
n : ℕ
h : ∀ (i : ℕ), (↑(npowRec n f) : ℕ → β) i = (↑f : ℕ → β) i ^ n
⊢ ∀ (i : ℕ), (↑(npowRec (n + 1) f) : ℕ → β) i = (↑f : ℕ → β) i ^ (n + 1)

Tactic:
simp [*, npowRec, pow_succ]

Premises used: pow_succ, npowRec
-- 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
f : CauSeq β abv
n : ℕ
⊢ (↑(f ^ n) : ℕ → β) = (↑f : ℕ → β) ^ n

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 : Ring β
abv : β → α
inst_4 : IsAbsoluteValue abv
f : CauSeq β abv
n i : ℕ
⊢ (↑(f ^ n) : ℕ → β) i = (↑f : ℕ → β) i ^ n

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 : Ring β
abv : β → α
inst_4 : IsAbsoluteValue abv
x : β
n : ℕ
⊢ const (x ^ n) = HPow.hPow (α := CauSeq β abv) (const x) n

Tactic:
rfl

Premises used: CauSeq.ofEq, CauSeq.const, rfl
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
Goal:
α : Type u_1
β_1 : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Ring β_1
abv_1 : β_1 → α
inst_4 : IsAbsoluteValue abv_1
β : Type u_3
inst_5 : CommRing β
abv : β → α
inst_6 : IsAbsoluteValue abv
a b : CauSeq β abv
n : ℕ
⊢ (↑(a * b) : ℕ → β) n = (↑(b * a) : ℕ → β) n

Tactic:
simp [mul_comm]

Premises used: mul_comm
-- 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
f g : CauSeq β abv
hf : f.LimZero
hg : g.LimZero
ε : α
ε0 : ε > 0
x : ℕ
H : ∀ j ≥ x, abv ((↑f : ℕ → β) j) < ε / 2 ∧ abv ((↑g : ℕ → β) j) < ε / 2
j : ℕ
ij : j ≥ x
⊢ abv ((↑f : ℕ → β) j) < ε / 2

Tactic:
let ⟨H₁, H₂⟩ := H _ ij
-- 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
f g : CauSeq β abv
hf : f.LimZero
hg : g.LimZero
ε : α
ε0 : ε > 0
x : ℕ
H : ∀ j ≥ x, abv ((↑f : ℕ → β) j) < ε / 2 ∧ abv ((↑g : ℕ → β) j) < ε / 2
j : ℕ
ij : j ≥ x
H₁ : abv ((↑f : ℕ → β) j) < ε / 2
⊢ abv ((↑g : ℕ → β) j) < ε / 2

Tactic:
let ⟨H₁, H₂⟩ := H _ ij
-- 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
f g : CauSeq β abv
hf : f.LimZero
hg : g.LimZero
ε : α
ε0 : ε > 0
x : ℕ
H : ∀ j ≥ x, abv ((↑f : ℕ → β) j) < ε / 2 ∧ abv ((↑g : ℕ → β) j) < ε / 2
j : ℕ
ij : j ≥ x
H₁ : abv ((↑f : ℕ → β) j) < ε / 2
H₂ : abv ((↑g : ℕ → β) j) < ε / 2
⊢ abv ((↑(f + g) : ℕ → β) j) < ε

Tactic:
simpa [add_halves ε] using lt_of_le_of_lt (abv_add abv _ _) (add_lt_add H₁ H₂)

Premises used: lt_of_le_of_lt, add_halves, add_lt_add, IsAbsoluteValue.abv_add
-- 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
f g : CauSeq β abv
hg : g.LimZero
ε : α
ε0 : ε > 0
F : α
F0 : F > 0
hF : ∀ (i : ℕ), abv ((↑f : ℕ → β) i) < F
x : ℕ
H : ∀ j ≥ x, abv ((↑g : ℕ → β) j) < ε / F
j : ℕ
ij : j ≥ x
⊢ abv ((↑f : ℕ → β) j) * abv ((↑g : ℕ → β) j) < F * (ε / F)

Tactic:
have := mul_lt_mul' (le_of_lt <| hF j) (H _ ij) (abv_nonneg abv _) F0
-- 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
f g : CauSeq β abv
hg : g.LimZero
ε : α
ε0 : ε > 0
F : α
F0 : F > 0
hF : ∀ (i : ℕ), abv ((↑f : ℕ → β) i) < F
x : ℕ
H : ∀ j ≥ x, abv ((↑g : ℕ → β) j) < ε / F
j : ℕ
ij : j ≥ x
this : abv ((↑f : ℕ → β) j) * abv ((↑g : ℕ → β) j) < F * (ε / F)
rwa : ∀ (this : abv ((↑f : ℕ → β) j) * abv ((↑g : ℕ → β) j) < ε / F * F), abv ((↑(f * g) : ℕ → β) j) < ε
rwa₁ : ∀ (this : abv ((↑f : ℕ → β) j) * abv ((↑g : ℕ → β) j) < ε), abv ((↑(f * g) : ℕ → β) j) < ε
rwa₂ rwa₃ rwa₄ rwa₅ : ∀ (this : abv ((↑f : ℕ → β) j * (↑g : ℕ → β) j) < ε), abv ((↑(f * g) : ℕ → β) j) < ε
⊢ abv ((↑(f * g) : ℕ → β) j) < ε

Tactic:
rwa [mul_comm F, div_mul_cancel₀ _ (ne_of_gt F0), ← abv_mul] at this

Premises used: div_mul_cancel₀, ne_of_gt, mul_comm, IsAbsoluteValue.abv_mul
-- 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
f g : CauSeq β abv
hg : f.LimZero
ε : α
ε0 : ε > 0
G : α
G0 : G > 0
hG : ∀ (i : ℕ), abv ((↑g : ℕ → β) i) < G
x : ℕ
H : ∀ j ≥ x, abv ((↑f : ℕ → β) j) < ε / G
j : ℕ
ij : j ≥ x
⊢ abv ((↑f : ℕ → β) j) * abv ((↑g : ℕ → β) j) < ε / G * G

Tactic:
have := mul_lt_mul'' (H _ ij) (hG j) (abv_nonneg abv _) (abv_nonneg abv _)
-- 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
f g : CauSeq β abv
hg : f.LimZero
ε : α
ε0 : ε > 0
G : α
G0 : G > 0
hG : ∀ (i : ℕ), abv ((↑g : ℕ → β) i) < G
x : ℕ
H : ∀ j ≥ x, abv ((↑f : ℕ → β) j) < ε / G
j : ℕ
ij : j ≥ x
this : abv ((↑f : ℕ → β) j) * abv ((↑g : ℕ → β) j) < ε / G * G
rwa : ∀ (this : abv ((↑f : ℕ → β) j) * abv ((↑g : ℕ → β) j) < ε), abv ((↑(f * g) : ℕ → β) j) < ε
rwa₁ rwa₂ rwa₃ rwa₄ : ∀ (this : abv ((↑f : ℕ → β) j * (↑g : ℕ → β) j) < ε), abv ((↑(f * g) : ℕ → β) j) < ε
⊢ abv ((↑(f * g) : ℕ → β) j) < ε

Tactic:
rwa [div_mul_cancel₀ _ (ne_of_gt G0), ← abv_mul] at this

Premises used: div_mul_cancel₀, ne_of_gt, IsAbsoluteValue.abv_mul
-- 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
f : CauSeq β abv
hf : f.LimZero
rw : (-1 * f).LimZero
⊢ (-f).LimZero

Tactic:
rw [← neg_one_mul f]

Premises used: neg_one_mul
-- 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
f : CauSeq β abv
hf : f.LimZero
⊢ (-1 * f).LimZero

Tactic:
mul_limZero_right _ hf

Premises used: CauSeq.mul_limZero_right
-- 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
f : CauSeq β abv
hf : f.LimZero
⊢ (-1 * f).LimZero

Tactic:
exact mul_limZero_right _ hf

Premises used: CauSeq.mul_limZero_right
-- 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
f g : CauSeq β abv
hf : f.LimZero
hg : g.LimZero
⊢ (f - g).LimZero

Tactic:
simpa only [sub_eq_add_neg] using add_limZero hf (neg_limZero hg)

Premises used: sub_eq_add_neg, CauSeq.neg_limZero, CauSeq.add_limZero
-- 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
f g : CauSeq β abv
hfg : (f - g).LimZero
⊢ (g - f).LimZero

Tactic:
simpa using neg_limZero hfg

Premises used: CauSeq.neg_limZero
-- 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
ε : α
ε0 : ε > 0
j : ℕ
h : j ≥ 0
⊢ abv ((↑0 : ℕ → β) j) < ε

Tactic:
simpa [abv_zero abv] using ε0

Premises used: IsAbsoluteValue.abv_zero
-- 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
x : β
⊢ LimZero (const x) ↔ x = 0

Tactic:
⟨fun H =>
    (abv_eq_zero abv).1 <|
      (eq_of_le_of_forall_lt_imp_le_of_dense (abv_nonneg abv _)) fun _ ε0 =>
        let ⟨_, hi⟩ := H _ ε0
        le_of_lt <| hi _ le_rfl,
    fun e => e.symm ▸ zero_limZero⟩

Premises used: le_rfl, IsAbsoluteValue.abv_nonneg, _private.0.CauSeq.const_limZero.match_1, le_of_lt, Eq.rec, LE.le, eq_of_le_of_forall_lt_imp_le_of_dense, Iff.intro, Iff.mp, Eq.symm, CauSeq.zero_limZero, IsAbsoluteValue.abv_eq_zero
-- 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
f : CauSeq β abv
⊢ (f - f).LimZero

Tactic:
simp [zero_limZero]

Premises used: CauSeq.zero_limZero
-- 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
x y : CauSeq β abv
f : (x - y).LimZero
ε : α
hε : ε > 0
⊢ ∃ (i : ℕ), ∀ j ≥ i, abv ((↑(y - x) : ℕ → β) j) < ε

Tactic:
simpa using neg_limZero f ε hε

Premises used: CauSeq.neg_limZero
-- 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
x y z : CauSeq β abv
fg : (x - y).LimZero
gh : (y - z).LimZero
⊢ (x - z).LimZero

Tactic:
simpa using add_limZero fg gh

Premises used: CauSeq.add_limZero
-- 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 g1 g2 : CauSeq β abv
hf : f1 ≈ f2
hg : g1 ≈ g2
⊢ f1 + g1 ≈ f2 + g2

Tactic:
simpa only [← add_sub_add_comm] using add_limZero hf hg

Premises used: add_sub_add_comm, CauSeq.add_limZero
-- 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
f g : CauSeq β abv
hf : f ≈ g
⊢ -f ≈ -g

Tactic:
simpa only [neg_sub'] using neg_limZero hf

Premises used: neg_sub', CauSeq.neg_limZero
-- 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 g1 g2 : CauSeq β abv
hf : f1 ≈ f2
hg : g1 ≈ g2
⊢ f1 - g1 ≈ f2 - g2

Tactic:
simpa only [sub_eq_add_neg] using add_equiv_add hf (neg_equiv_neg hg)

Premises used: sub_eq_add_neg, CauSeq.neg_equiv_neg, CauSeq.add_equiv_add
-- 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
f g : CauSeq β abv
h : f ≈ g
ε : α
ε0 : 0 < ε
x : ℕ
H : ∀ j ≥ x, abv ((↑(f - g) : ℕ → β) j) < ε / 2 ∧ ∀ k ≥ j, abv ((↑f : ℕ → β) k - (↑f : ℕ → β) j) < ε / 2
j : ℕ
ij : j ≥ x
k : ℕ
jk : k ≥ j
⊢ abv ((↑(f - g) : ℕ → β) j) < ε / 2

Tactic:
let ⟨h₁, h₂⟩ := H _ ij
-- 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
f g : CauSeq β abv
h : f ≈ g
ε : α
ε0 : 0 < ε
x : ℕ
H : ∀ j ≥ x, abv ((↑(f - g) : ℕ → β) j) < ε / 2 ∧ ∀ k ≥ j, abv ((↑f : ℕ → β) k - (↑f : ℕ → β) j) < ε / 2
j : ℕ
ij : j ≥ x
k : ℕ
jk : k ≥ j
h₁ : abv ((↑(f - g) : ℕ → β) j) < ε / 2
⊢ ∀ k ≥ j, abv ((↑f : ℕ → β) k - (↑f : ℕ → β) j) < ε / 2

Tactic:
let ⟨h₁, h₂⟩ := H _ ij
-- 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
f g : CauSeq β abv
h : f ≈ g
ε : α
ε0 : 0 < ε
x : ℕ
H : ∀ j ≥ x, abv ((↑(f - g) : ℕ → β) j) < ε / 2 ∧ ∀ k ≥ j, abv ((↑f : ℕ → β) k - (↑f : ℕ → β) j) < ε / 2
j : ℕ
ij : j ≥ x
k : ℕ
jk : k ≥ j
h₁ : abv ((↑(f - g) : ℕ → β) j) < ε / 2
h₂ : ∀ k ≥ j, abv ((↑f : ℕ → β) k - (↑f : ℕ → β) j) < ε / 2
⊢ abv ((↑f : ℕ → β) j - (↑g : ℕ → β) j + ((↑f : ℕ → β) k - (↑f : ℕ → β) j)) < ε / 2 + ε / 2

Tactic:
have := lt_of_le_of_lt (abv_add abv (f j - g j) _) (add_lt_add h₁ (h₂ _ jk))
-- 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
f g : CauSeq β abv
h : f ≈ g
ε : α
ε0 : 0 < ε
x : ℕ
H : ∀ j ≥ x, abv ((↑(f - g) : ℕ → β) j) < ε / 2 ∧ ∀ k ≥ j, abv ((↑f : ℕ → β) k - (↑f : ℕ → β) j) < ε / 2
j : ℕ
ij : j ≥ x
k : ℕ
jk : k ≥ j
h₁ : abv ((↑(f - g) : ℕ → β) j) < ε / 2
h₂ : ∀ k ≥ j, abv ((↑f : ℕ → β) k - (↑f : ℕ → β) j) < ε / 2
this : abv ((↑f : ℕ → β) j - (↑g : ℕ → β) j + ((↑f : ℕ → β) k - (↑f : ℕ → β) j)) < ε / 2 + ε / 2
rwa : ∀ (this : abv ((↑f : ℕ → β) k - (↑g : ℕ → β) j) < ε / 2 + ε / 2), abv ((↑f : ℕ → β) k - (↑g : ℕ → β) j) < ε
rwa₁ rwa₂ rwa₃ rwa₄ : ∀ (this : abv ((↑f : ℕ → β) k - (↑g : ℕ → β) j) < ε), abv ((↑f : ℕ → β) k - (↑g : ℕ → β) j) < ε
⊢ abv ((↑f : ℕ → β) k - (↑g : ℕ → β) j) < ε

Tactic:
rwa [sub_add_sub_cancel', add_halves] at this

Premises used: add_halves, sub_add_sub_cancel'
-- 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
f g : CauSeq β abv
h : f ≈ g
l : f.LimZero
⊢ g.LimZero

Tactic:
simpa using add_limZero (Setoid.symm h) l

Premises used: Setoid.symm, CauSeq.add_limZero
-- 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
f g : CauSeq β abv
h : f ≈ g
l : g.LimZero
⊢ f.LimZero

Tactic:
simpa using add_limZero h l

Premises used: CauSeq.add_limZero
-- 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
f : CauSeq β abv
hf : ¬f.LimZero
by_contra : ∀ (nk : ¬∃ K > 0, ∃ (i : ℕ), ∀ j ≥ i, K ≤ abv ((↑f : ℕ → β) j)), False
⊢ ∃ K > 0, ∃ (i : ℕ), ∀ j ≥ i, K ≤ abv ((↑f : ℕ → β) j)

Tactic:
by_contra nk
-- 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
f : CauSeq β abv
hf : ¬f.LimZero
nk : ¬∃ K > 0, ∃ (i : ℕ), ∀ j ≥ i, K ≤ abv ((↑f : ℕ → β) j)
⊢ False

Tactic:
hf fun ε ε0 => ?_
-- 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
f : CauSeq β abv
hf : ¬f.LimZero
nk : ¬∃ K > 0, ∃ (i : ℕ), ∀ j ≥ i, K ≤ abv ((↑f : ℕ → β) j)
refine : ∀ (ε : α) (ε0 : ε > 0), ∃ (i : ℕ), ∀ j ≥ i, abv ((↑f : ℕ → β) j) < ε
⊢ False

Tactic:
refine hf fun ε ε0 => ?_
-- 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
f : CauSeq β abv
hf : ¬f.LimZero
nk : ¬∃ K > 0, ∃ (i : ℕ), ∀ j ≥ i, K ≤ abv ((↑f : ℕ → β) j)
ε : α
ε0 : ε > 0
⊢ ∀ x > 0, ∀ (x_1 : ℕ), ∃ (x_2 : ℕ) (_ : x_2 ≥ x_1), abv ((↑f : ℕ → β) x_2) < x

Tactic:
simp only [not_exists, not_and, not_forall, not_le] at nk

Premises used: not_le, not_exists, not_and, Classical.not_forall