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
f : CauSeq β abv
hf : ¬f.LimZero
ε : α
ε0 : ε > 0
nk : ∀ x > 0, ∀ (x_1 : ℕ), ∃ (x_2 : ℕ) (_ : x_2 ≥ x_1), abv ((↑f : ℕ → β) x_2) < x
obtain :
  ∀ (i : ℕ) (hi : ∀ j ≥ i, ∀ k ≥ j, abv ((↑f : ℕ → β) k - (↑f : ℕ → β) j) < ε / 2),
    ∃ (i : ℕ), ∀ j ≥ i, abv ((↑f : ℕ → β) j) < ε
⊢ ∃ (i : ℕ), ∀ j ≥ i, abv ((↑f : ℕ → β) j) < ε

Tactic:
obtain ⟨i, hi⟩ := f.cauchy₃ (half_pos ε0)

Premises used: half_pos, CauSeq.cauchy₃
-- 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
ε : α
ε0 : ε > 0
nk : ∀ x > 0, ∀ (x_1 : ℕ), ∃ (x_2 : ℕ) (_ : x_2 ≥ x_1), abv ((↑f : ℕ → β) x_2) < x
i : ℕ
hi : ∀ j ≥ i, ∀ k ≥ j, abv ((↑f : ℕ → β) k - (↑f : ℕ → β) j) < ε / 2
rcases : ∀ (j : ℕ) (ij : j ≥ i) (hj : abv ((↑f : ℕ → β) j) < ε / 2), ∃ (i : ℕ), ∀ j ≥ i, abv ((↑f : ℕ → β) j) < ε
⊢ ∃ (i : ℕ), ∀ j ≥ i, abv ((↑f : ℕ → β) j) < ε

Tactic:
rcases nk _ (half_pos ε0) i with ⟨j, ij, hj⟩

Premises used: half_pos
-- 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
ε : α
ε0 : ε > 0
nk : ∀ x > 0, ∀ (x_1 : ℕ), ∃ (x_2 : ℕ) (_ : x_2 ≥ x_1), abv ((↑f : ℕ → β) x_2) < x
i : ℕ
hi : ∀ j ≥ i, ∀ k ≥ j, abv ((↑f : ℕ → β) k - (↑f : ℕ → β) j) < ε / 2
j : ℕ
ij : j ≥ i
hj : abv ((↑f : ℕ → β) j) < ε / 2
⊢ ∃ (i : ℕ), ∀ j ≥ i, abv ((↑f : ℕ → β) j) < ε

Tactic:
⟨j, fun k jk => ?_⟩

Premises used: Exists.intro
-- 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
ε : α
ε0 : ε > 0
nk : ∀ x > 0, ∀ (x_1 : ℕ), ∃ (x_2 : ℕ) (_ : x_2 ≥ x_1), abv ((↑f : ℕ → β) x_2) < x
i : ℕ
hi : ∀ j ≥ i, ∀ k ≥ j, abv ((↑f : ℕ → β) k - (↑f : ℕ → β) j) < ε / 2
j : ℕ
ij : j ≥ i
hj : abv ((↑f : ℕ → β) j) < ε / 2
refine : ∀ (k : ℕ) (jk : k ≥ j), abv ((↑f : ℕ → β) k) < ε
⊢ ∃ (i : ℕ), ∀ j ≥ i, abv ((↑f : ℕ → β) j) < ε

Tactic:
refine ⟨j, fun k 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 : CauSeq β abv
hf : ¬f.LimZero
ε : α
ε0 : ε > 0
nk : ∀ x > 0, ∀ (x_1 : ℕ), ∃ (x_2 : ℕ) (_ : x_2 ≥ x_1), abv ((↑f : ℕ → β) x_2) < x
i : ℕ
hi : ∀ j ≥ i, ∀ k ≥ j, abv ((↑f : ℕ → β) k - (↑f : ℕ → β) j) < ε / 2
j : ℕ
ij : j ≥ i
hj : abv ((↑f : ℕ → β) j) < ε / 2
k : ℕ
jk : k ≥ j
⊢ abv ((↑f : ℕ → β) k - (↑f : ℕ → β) j + (↑f : ℕ → β) j) < ε / 2 + ε / 2

Tactic:
have := lt_of_le_of_lt (abv_add abv _ _) (add_lt_add (hi j ij k jk) hj)
-- 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
ε : α
ε0 : ε > 0
nk : ∀ x > 0, ∀ (x_1 : ℕ), ∃ (x_2 : ℕ) (_ : x_2 ≥ x_1), abv ((↑f : ℕ → β) x_2) < x
i : ℕ
hi : ∀ j ≥ i, ∀ k ≥ j, abv ((↑f : ℕ → β) k - (↑f : ℕ → β) j) < ε / 2
j : ℕ
ij : j ≥ i
hj : abv ((↑f : ℕ → β) j) < ε / 2
k : ℕ
jk : k ≥ j
this : abv ((↑f : ℕ → β) k - (↑f : ℕ → β) j + (↑f : ℕ → β) j) < ε / 2 + ε / 2
rwa : ∀ (this : abv ((↑f : ℕ → β) k) < ε / 2 + ε / 2), abv ((↑f : ℕ → β) k) < ε
rwa₁ rwa₂ rwa₃ rwa₄ : ∀ (this : abv ((↑f : ℕ → β) k) < ε), abv ((↑f : ℕ → β) k) < ε
⊢ abv ((↑f : ℕ → β) k) < ε

Tactic:
rwa [sub_add_cancel, add_halves] at this

Premises used: add_halves, sub_add_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 : ∀ ε > 0, ∃ (i : ℕ), ∀ j ≥ i, abv (f j - (↑g : ℕ → β) j) < ε
ε : α
ε0 : ε > 0
i : ℕ
hi : ∀ j ≥ i, abv (f j - (↑g : ℕ → β) j) < ε / 2 / 2 ∧ ∀ k ≥ j, abv ((↑g : ℕ → β) k - (↑g : ℕ → β) j) < ε / 2
j : ℕ
ij : j ≥ i
⊢ abv (f i - (↑g : ℕ → β) i) < ε / 2 / 2

Tactic:
obtain ⟨h₁, h₂⟩ := 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 : Ring β
abv : β → α
inst_4 : IsAbsoluteValue abv
f : ℕ → β
g : CauSeq β abv
h : ∀ ε > 0, ∃ (i : ℕ), ∀ j ≥ i, abv (f j - (↑g : ℕ → β) j) < ε
ε : α
ε0 : ε > 0
i : ℕ
hi : ∀ j ≥ i, abv (f j - (↑g : ℕ → β) j) < ε / 2 / 2 ∧ ∀ k ≥ j, abv ((↑g : ℕ → β) k - (↑g : ℕ → β) j) < ε / 2
j : ℕ
ij : j ≥ i
h₁ : abv (f i - (↑g : ℕ → β) i) < ε / 2 / 2
⊢ ∀ k ≥ i, abv ((↑g : ℕ → β) k - (↑g : ℕ → β) i) < ε / 2

Tactic:
obtain ⟨h₁, h₂⟩ := 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 : Ring β
abv : β → α
inst_4 : IsAbsoluteValue abv
f : ℕ → β
g : CauSeq β abv
h : ∀ ε > 0, ∃ (i : ℕ), ∀ j ≥ i, abv (f j - (↑g : ℕ → β) j) < ε
ε : α
ε0 : ε > 0
i : ℕ
hi : ∀ j ≥ i, abv (f j - (↑g : ℕ → β) j) < ε / 2 / 2 ∧ ∀ k ≥ j, abv ((↑g : ℕ → β) k - (↑g : ℕ → β) j) < ε / 2
j : ℕ
ij : j ≥ i
h₁ : abv (f i - (↑g : ℕ → β) i) < ε / 2 / 2
h₂ : ∀ k ≥ i, abv ((↑g : ℕ → β) k - (↑g : ℕ → β) i) < ε / 2
⊢ abv ((↑g : ℕ → β) i - f i) < ε / 2 / 2

Tactic:
rw [abv_sub abv] at h₁

Premises used: IsAbsoluteValue.abv_sub
-- 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 : ∀ ε > 0, ∃ (i : ℕ), ∀ j ≥ i, abv (f j - (↑g : ℕ → β) j) < ε
ε : α
ε0 : ε > 0
i : ℕ
hi : ∀ j ≥ i, abv (f j - (↑g : ℕ → β) j) < ε / 2 / 2 ∧ ∀ k ≥ j, abv ((↑g : ℕ → β) k - (↑g : ℕ → β) j) < ε / 2
j : ℕ
ij : j ≥ i
h₁ : abv (f i - (↑g : ℕ → β) i) < ε / 2 / 2
h₂ : ∀ k ≥ i, abv ((↑g : ℕ → β) k - (↑g : ℕ → β) i) < ε / 2
h₃ : abv ((↑g : ℕ → β) i - f i) < ε / 2 / 2
⊢ ∀ k ≥ i, abv ((↑g : ℕ → β) k - (↑g : ℕ → β) i) < ε / 2

Tactic:
rw [abv_sub abv] at h₁

Premises used: IsAbsoluteValue.abv_sub
-- 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 : ∀ ε > 0, ∃ (i : ℕ), ∀ j ≥ i, abv (f j - (↑g : ℕ → β) j) < ε
ε : α
ε0 : ε > 0
i : ℕ
hi : ∀ j ≥ i, abv (f j - (↑g : ℕ → β) j) < ε / 2 / 2 ∧ ∀ k ≥ j, abv ((↑g : ℕ → β) k - (↑g : ℕ → β) j) < ε / 2
j : ℕ
ij : j ≥ i
h₁ : abv ((↑g : ℕ → β) i - f i) < ε / 2 / 2
h₂ : ∀ k ≥ i, abv ((↑g : ℕ → β) k - (↑g : ℕ → β) i) < ε / 2
⊢ abv (f j - (↑g : ℕ → β) j + ((↑g : ℕ → β) i - f i)) < ε / 2 / 2 + ε / 2 / 2

Tactic:
have := lt_of_le_of_lt (abv_add abv _ _) (add_lt_add (hi _ ij).1 h₁)
-- 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 : ∀ ε > 0, ∃ (i : ℕ), ∀ j ≥ i, abv (f j - (↑g : ℕ → β) j) < ε
ε : α
ε0 : ε > 0
i : ℕ
hi : ∀ j ≥ i, abv (f j - (↑g : ℕ → β) j) < ε / 2 / 2 ∧ ∀ k ≥ j, abv ((↑g : ℕ → β) k - (↑g : ℕ → β) j) < ε / 2
j : ℕ
ij : j ≥ i
h₁ : abv ((↑g : ℕ → β) i - f i) < ε / 2 / 2
h₂ : ∀ k ≥ i, abv ((↑g : ℕ → β) k - (↑g : ℕ → β) i) < ε / 2
this : abv (f j - (↑g : ℕ → β) j + ((↑g : ℕ → β) i - f i)) < ε / 2 / 2 + ε / 2 / 2
⊢ abv (f j - (↑g : ℕ → β) j + ((↑g : ℕ → β) i - f i) + ((↑g : ℕ → β) j - (↑g : ℕ → β) i)) <
    ε / 2 / 2 + ε / 2 / 2 + ε / 2

Tactic:
have := lt_of_le_of_lt (abv_add abv _ _) (add_lt_add this (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 : ∀ ε > 0, ∃ (i : ℕ), ∀ j ≥ i, abv (f j - (↑g : ℕ → β) j) < ε
ε : α
ε0 : ε > 0
i : ℕ
hi : ∀ j ≥ i, abv (f j - (↑g : ℕ → β) j) < ε / 2 / 2 ∧ ∀ k ≥ j, abv ((↑g : ℕ → β) k - (↑g : ℕ → β) j) < ε / 2
j : ℕ
ij : j ≥ i
h₁ : abv ((↑g : ℕ → β) i - f i) < ε / 2 / 2
h₂ : ∀ k ≥ i, abv ((↑g : ℕ → β) k - (↑g : ℕ → β) i) < ε / 2
this_1 : abv (f j - (↑g : ℕ → β) j + ((↑g : ℕ → β) i - f i)) < ε / 2 / 2 + ε / 2 / 2
this :
  abv (f j - (↑g : ℕ → β) j + ((↑g : ℕ → β) i - f i) + ((↑g : ℕ → β) j - (↑g : ℕ → β) i)) <
    ε / 2 / 2 + ε / 2 / 2 + ε / 2
rwa :
  ∀ (this : abv (f j - (↑g : ℕ → β) j + ((↑g : ℕ → β) i - f i) + ((↑g : ℕ → β) j - (↑g : ℕ → β) i)) < ε / 2 + ε / 2),
    abv (f j - f i) < ε
rwa₁ :
  ∀ (this : abv (f j - (↑g : ℕ → β) j + ((↑g : ℕ → β) i - f i) + ((↑g : ℕ → β) j - (↑g : ℕ → β) i)) < ε),
    abv (f j - f i) < ε
rwa₂ :
  ∀ (this : abv (f j - (↑g : ℕ → β) j + ((↑g : ℕ → β) j - (↑g : ℕ → β) i) + ((↑g : ℕ → β) i - f i)) < ε),
    abv (f j - f i) < ε
rwa₃ : ∀ (this : abv (f j - (↑g : ℕ → β) i + ((↑g : ℕ → β) i - f i)) < ε), abv (f j - f i) < ε
rwa₄ rwa₅ rwa₆ rwa₇ : ∀ (this : abv (f j - f i) < ε), abv (f j - f i) < ε
⊢ abv (f j - f i) < ε

Tactic:
rwa [add_halves, add_halves, add_right_comm, sub_add_sub_cancel, sub_add_sub_cancel] at this

Premises used: sub_add_sub_cancel, add_halves, add_right_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 : CauSeq β abv
hf : ¬f ≈ 0
h : f.LimZero
⊢ (f - 0).LimZero

Tactic:
simp [h]
-- 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 ≈ 0
h : f.LimZero
⊢ (f - 0).LimZero

Tactic:
have : LimZero (f - 0) := by simp [h]
-- 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 ≈ 0
h : f.LimZero
this : (f - 0).LimZero
⊢ False

Tactic:
hf this
-- 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 ≈ 0
h : f.LimZero
this : (f - 0).LimZero
⊢ False

Tactic:
exact hf this
-- 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 f : CauSeq β abv
hf : f ≈ 0
this : (f - 0).LimZero
⊢ f.LimZero

Tactic:
simpa
-- 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 f : CauSeq β abv
hf : f ≈ 0
this_1 : (f - 0).LimZero
this : (g * f).LimZero
⊢ (g * f - 0).LimZero

Tactic:
simpa
-- 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 f : CauSeq β abv
hf : f ≈ 0
this_1 : (f - 0).LimZero
this : (f * g).LimZero
⊢ (f * g - 0).LimZero

Tactic:
simpa
-- 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 ≈ 0
hg : ¬g ≈ 0
this : (f * g - 0).LimZero
⊢ (f * g).LimZero

Tactic:
simpa
-- 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 ≈ 0
hg : ¬g ≈ 0
this : (f * g - 0).LimZero
⊢ (f * g).LimZero

Tactic:
have hlz : LimZero (f * g) := by simpa
-- 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 ≈ 0
hg : ¬g ≈ 0
this : (f * g - 0).LimZero
hlz : (f * g).LimZero
⊢ ¬f.LimZero

Tactic:
simpa using show ¬LimZero (f - 0) from hf
-- 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 ≈ 0
hg : ¬g ≈ 0
this : (f * g - 0).LimZero
hlz : (f * g).LimZero
⊢ ¬f.LimZero

Tactic:
have hf' : ¬LimZero f := by simpa using show ¬LimZero (f - 0) from hf
-- 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 ≈ 0
hg : ¬g ≈ 0
this : (f * g - 0).LimZero
hlz : (f * g).LimZero
hf' : ¬f.LimZero
⊢ ¬g.LimZero

Tactic:
simpa using show ¬LimZero (g - 0) from hg
-- 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 ≈ 0
hg : ¬g ≈ 0
this : (f * g - 0).LimZero
hlz : (f * g).LimZero
hf' : ¬f.LimZero
⊢ ¬g.LimZero

Tactic:
have hg' : ¬LimZero g := by simpa using show ¬LimZero (g - 0) from hg
-- 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 ≈ 0
hg : ¬g ≈ 0
this : (f * g - 0).LimZero
hlz : (f * g).LimZero
hf' : ¬f.LimZero
hg' : ¬g.LimZero
rcases : ∀ (a1 : α) (ha1 : a1 > 0) (N1 : ℕ) (hN1 : ∀ j ≥ N1, a1 ≤ abv ((↑f : ℕ → β) j)), False
⊢ False

Tactic:
rcases abv_pos_of_not_limZero hf' with ⟨a1, ha1, N1, hN1⟩

Premises used: CauSeq.abv_pos_of_not_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 ≈ 0
hg : ¬g ≈ 0
this : (f * g - 0).LimZero
hlz : (f * g).LimZero
hf' : ¬f.LimZero
hg' : ¬g.LimZero
a1 : α
ha1 : a1 > 0
N1 : ℕ
hN1 : ∀ j ≥ N1, a1 ≤ abv ((↑f : ℕ → β) j)
rcases : ∀ (a2 : α) (ha2 : a2 > 0) (N2 : ℕ) (hN2 : ∀ j ≥ N2, a2 ≤ abv ((↑g : ℕ → β) j)), False
⊢ False

Tactic:
rcases abv_pos_of_not_limZero hg' with ⟨a2, ha2, N2, hN2⟩

Premises used: CauSeq.abv_pos_of_not_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 ≈ 0
hg : ¬g ≈ 0
this : (f * g - 0).LimZero
hlz : (f * g).LimZero
hf' : ¬f.LimZero
hg' : ¬g.LimZero
a1 : α
ha1 : a1 > 0
N1 : ℕ
hN1 : ∀ j ≥ N1, a1 ≤ abv ((↑f : ℕ → β) j)
a2 : α
ha2 : a2 > 0
N2 : ℕ
hN2 : ∀ j ≥ N2, a2 ≤ abv ((↑g : ℕ → β) j)
⊢ 0 < a1 * a2

Tactic:
have : 0 < a1 * a2 := mul_pos ha1 ha2
-- 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 ≈ 0
hg : ¬g ≈ 0
this_1 : (f * g - 0).LimZero
hlz : (f * g).LimZero
hf' : ¬f.LimZero
hg' : ¬g.LimZero
a1 : α
ha1 : a1 > 0
N1 : ℕ
hN1 : ∀ j ≥ N1, a1 ≤ abv ((↑f : ℕ → β) j)
a2 : α
ha2 : a2 > 0
N2 : ℕ
hN2 : ∀ j ≥ N2, a2 ≤ abv ((↑g : ℕ → β) j)
this : 0 < a1 * a2
obtain : ∀ (N : ℕ) (hN : ∀ j ≥ N, abv ((↑(f * g) : ℕ → β) j) < a1 * a2), False
⊢ False

Tactic:
obtain ⟨N, hN⟩ := hlz _ this
-- 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 ≈ 0
hg : ¬g ≈ 0
this_1 : (f * g - 0).LimZero
hlz : (f * g).LimZero
hf' : ¬f.LimZero
hg' : ¬g.LimZero
a1 : α
ha1 : a1 > 0
N1 : ℕ
hN1 : ∀ j ≥ N1, a1 ≤ abv ((↑f : ℕ → β) j)
a2 : α
ha2 : a2 > 0
N2 : ℕ
hN2 : ∀ j ≥ N2, a2 ≤ abv ((↑g : ℕ → β) j)
this : 0 < a1 * a2
N : ℕ
hN : ∀ j ≥ N, abv ((↑(f * g) : ℕ → β) j) < a1 * a2
i : ℕ := max N (max N1 N2)
⊢ abv ((↑(f * g) : ℕ → β) i) < a1 * a2

Tactic:
have hN' := hN i (le_max_left _ _)
-- 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 ≈ 0
hg : ¬g ≈ 0
this_1 : (f * g - 0).LimZero
hlz : (f * g).LimZero
hf' : ¬f.LimZero
hg' : ¬g.LimZero
a1 : α
ha1 : a1 > 0
N1 : ℕ
hN1 : ∀ j ≥ N1, a1 ≤ abv ((↑f : ℕ → β) j)
a2 : α
ha2 : a2 > 0
N2 : ℕ
hN2 : ∀ j ≥ N2, a2 ≤ abv ((↑g : ℕ → β) j)
this : 0 < a1 * a2
N : ℕ
hN : ∀ j ≥ N, abv ((↑(f * g) : ℕ → β) j) < a1 * a2
i : ℕ := max N (max N1 N2)
hN' : abv ((↑(f * g) : ℕ → β) i) < a1 * a2
⊢ a1 ≤ abv ((↑f : ℕ → β) i)

Tactic:
have hN1' := hN1 i (le_trans (le_max_left _ _) (le_max_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 ≈ 0
hg : ¬g ≈ 0
this_1 : (f * g - 0).LimZero
hlz : (f * g).LimZero
hf' : ¬f.LimZero
hg' : ¬g.LimZero
a1 : α
ha1 : a1 > 0
N1 : ℕ
hN1 : ∀ j ≥ N1, a1 ≤ abv ((↑f : ℕ → β) j)
a2 : α
ha2 : a2 > 0
N2 : ℕ
hN2 : ∀ j ≥ N2, a2 ≤ abv ((↑g : ℕ → β) j)
this : 0 < a1 * a2
N : ℕ
hN : ∀ j ≥ N, abv ((↑(f * g) : ℕ → β) j) < a1 * a2
i : ℕ := max N (max N1 N2)
hN' : abv ((↑(f * g) : ℕ → β) i) < a1 * a2
hN1' : a1 ≤ abv ((↑f : ℕ → β) i)
⊢ a2 ≤ abv ((↑g : ℕ → β) i)

Tactic:
have hN1' := hN2 i (le_trans (le_max_right _ _) (le_max_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 ≈ 0
hg : ¬g ≈ 0
this_1 : (f * g - 0).LimZero
hlz : (f * g).LimZero
hf' : ¬f.LimZero
hg' : ¬g.LimZero
a1 : α
ha1 : a1 > 0
N1 : ℕ
hN1 : ∀ j ≥ N1, a1 ≤ abv ((↑f : ℕ → β) j)
a2 : α
ha2 : a2 > 0
N2 : ℕ
hN2 : ∀ j ≥ N2, a2 ≤ abv ((↑g : ℕ → β) j)
this : 0 < a1 * a2
N : ℕ
hN : ∀ j ≥ N, abv ((↑(f * g) : ℕ → β) j) < a1 * a2
i : ℕ := max N (max N1 N2)
hN' : abv ((↑(f * g) : ℕ → β) i) < a1 * a2
hN1'_1 : a1 ≤ abv ((↑f : ℕ → β) i)
hN1' : a2 ≤ abv ((↑g : ℕ → β) i)
apply : a1 * a2 ≤ abv ((↑(f * g) : ℕ → β) i)
⊢ False

Tactic:
apply not_le_of_gt hN'

Premises used: not_le_of_gt
-- 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 ≈ 0
hg : ¬g ≈ 0
this_1 : (f * g - 0).LimZero
hlz : (f * g).LimZero
hf' : ¬f.LimZero
hg' : ¬g.LimZero
a1 : α
ha1 : a1 > 0
N1 : ℕ
hN1 : ∀ j ≥ N1, a1 ≤ abv ((↑f : ℕ → β) j)
a2 : α
ha2 : a2 > 0
N2 : ℕ
hN2 : ∀ j ≥ N2, a2 ≤ abv ((↑g : ℕ → β) j)
this : 0 < a1 * a2
N : ℕ
hN : ∀ j ≥ N, abv ((↑(f * g) : ℕ → β) j) < a1 * a2
i : ℕ := max N (max N1 N2)
hN' : abv ((↑(f * g) : ℕ → β) i) < a1 * a2
hN1'_1 : a1 ≤ abv ((↑f : ℕ → β) i)
hN1' : a2 ≤ abv ((↑g : ℕ → β) i)
change : a1 * a2 ≤ abv ((↑f : ℕ → β) i * (↑g : ℕ → β) i)
⊢ a1 * a2 ≤ abv ((↑(f * g) : ℕ → β) i)

Tactic:
change _ ≤ abv (_ * _)

Premises used: HMul.hMul
-- 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 ≈ 0
hg : ¬g ≈ 0
this_1 : (f * g - 0).LimZero
hlz : (f * g).LimZero
hf' : ¬f.LimZero
hg' : ¬g.LimZero
a1 : α
ha1 : a1 > 0
N1 : ℕ
hN1 : ∀ j ≥ N1, a1 ≤ abv ((↑f : ℕ → β) j)
a2 : α
ha2 : a2 > 0
N2 : ℕ
hN2 : ∀ j ≥ N2, a2 ≤ abv ((↑g : ℕ → β) j)
this : 0 < a1 * a2
N : ℕ
hN : ∀ j ≥ N, abv ((↑(f * g) : ℕ → β) j) < a1 * a2
i : ℕ := max N (max N1 N2)
hN' : abv ((↑(f * g) : ℕ → β) i) < a1 * a2
hN1'_1 : a1 ≤ abv ((↑f : ℕ → β) i)
hN1' : a2 ≤ abv ((↑g : ℕ → β) i)
rw : a1 * a2 ≤ abv ((↑f : ℕ → β) i) * abv ((↑g : ℕ → β) i)
⊢ a1 * a2 ≤ abv ((↑f : ℕ → β) i * (↑g : ℕ → β) i)

Tactic:
rw [abv_mul abv]

Premises used: 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
hf : ¬f ≈ 0
hg : ¬g ≈ 0
this_1 : (f * g - 0).LimZero
hlz : (f * g).LimZero
hf' : ¬f.LimZero
hg' : ¬g.LimZero
a1 : α
ha1 : a1 > 0
N1 : ℕ
hN1 : ∀ j ≥ N1, a1 ≤ abv ((↑f : ℕ → β) j)
a2 : α
ha2 : a2 > 0
N2 : ℕ
hN2 : ∀ j ≥ N2, a2 ≤ abv ((↑g : ℕ → β) j)
this : 0 < a1 * a2
N : ℕ
hN : ∀ j ≥ N, abv ((↑(f * g) : ℕ → β) j) < a1 * a2
i : ℕ := max N (max N1 N2)
hN' : abv ((↑(f * g) : ℕ → β) i) < a1 * a2
hN1'_1 : a1 ≤ abv ((↑f : ℕ → β) i)
hN1' : a2 ≤ abv ((↑g : ℕ → β) i)
c0 : 0 ≤ a2
b0 : 0 ≤ abv ((↑f : ℕ → β) i)
⊢ a1 * a2 ≤ abv ((↑f : ℕ → β) i) * abv ((↑g : ℕ → β) i)

Tactic:
gcongr
-- 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 : β
rw : LimZero (const (x - y)) ↔ x = y
rw₁ : x - y = 0 ↔ x = y
rw₂ rw₃ : x = y ↔ x = y
⊢ (HSub.hSub (α := CauSeq β abv) (const x) (const y)).LimZero ↔ x = y

Tactic:
rw [← const_sub, const_limZero, sub_eq_zero]

Premises used: sub_eq_zero, CauSeq.const_limZero, CauSeq.const_sub
-- 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 [mul_sub, sub_mul, sub_add_sub_cancel]
    using add_limZero (mul_limZero_left g1 hf) (mul_limZero_right f2 hg)

Premises used: sub_add_sub_cancel, mul_sub, sub_mul, CauSeq.mul_limZero_right, CauSeq.mul_limZero_left, 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
G : Type u_3
inst_5 : SMul G β
inst_6 : IsScalarTower G β β
f1 f2 : CauSeq β abv
c : G
hf : f1 ≈ f2
⊢ c • f1 ≈ c • f2

Tactic:
simpa [const_smul, smul_one_mul _ _] using
    mul_equiv_mul (const_equiv.mpr <| Eq.refl <| c • (1 : β)) hf

Premises used: CauSeq.mul_equiv_mul, Iff.mpr, CauSeq.const_equiv, smul_one_mul, Eq.refl, HSMul.hSMul, OfNat.ofNat, CauSeq.const_smul
-- 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
⊢ HPow.hPow (β := ℕ) f1 0 ≈ HPow.hPow (β := ℕ) f2 0

Tactic:
simp only [pow_zero, Setoid.refl]

Premises used: pow_zero, Setoid.refl
-- 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 : ℕ
ih : f1 ^ n ≈ f2 ^ n
⊢ f1 ^ (n + 1) ≈ f2 ^ (n + 1)

Tactic:
simpa only [pow_succ'] using mul_equiv_mul hf ih

Premises used: CauSeq.mul_equiv_mul, pow_succ'