awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Ring β
abv : β → α
inst_4 : IsAbsoluteValue abv
f : ℕ → β
hf : IsCauSeq abv f
i : ℕ
h : ∀ j ≥ i, abv (f j - f i) < 1
R : ℕ → α :=
  Nat.rec (motive := fun (x : ℕ) ↦ α) (abv (f 0)) fun (i : ℕ) (c : (fun (x : ℕ) ↦ α) i) ↦ max c (abv (f i.succ))
hR : R = Nat.rec (motive := fun (x : ℕ) ↦ α) (abv (f 0)) fun (i : ℕ) (c : (fun (x : ℕ) ↦ α) i) ↦ max c (abv (f i.succ))
this : ∀ (i j : ℕ), j ≤ i → abv (f j) ≤ R i
⊢ ∃ (r : α), ∀ (i : ℕ), abv (f i) < r
have refine : ∀ (j : ℕ), abv (f j) < R i + 1
Tactic: refine ⟨R i + 1, fun j ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Ring β
abv : β → α
inst_4 : IsAbsoluteValue abv
f : ℕ → β
hf : IsCauSeq abv f
i : ℕ
h : ∀ j ≥ i, abv (f j - f i) < 1
R : ℕ → α :=
  Nat.rec (motive := fun (x : ℕ) ↦ α) (abv (f 0)) fun (i : ℕ) (c : (fun (x : ℕ) ↦ α) i) ↦ max c (abv (f i.succ))
hR : R = Nat.rec (motive := fun (x : ℕ) ↦ α) (abv (f 0)) fun (i : ℕ) (c : (fun (x : ℕ) ↦ α) i) ↦ max c (abv (f i.succ))
this : ∀ (i j : ℕ), j ≤ i → abv (f j) ≤ R i
j : ℕ
⊢ abv (f j) < R i + 1
have inl : ∀ (hji : j ≤ i), abv (f j) < R i + 1
Tactic: obtain hji | hij := le_total j i
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Ring β
abv : β → α
inst_4 : IsAbsoluteValue abv
f : ℕ → β
hf : IsCauSeq abv f
i : ℕ
h : ∀ j ≥ i, abv (f j - f i) < 1
R : ℕ → α :=
  Nat.rec (motive := fun (x : ℕ) ↦ α) (abv (f 0)) fun (i : ℕ) (c : (fun (x : ℕ) ↦ α) i) ↦ max c (abv (f i.succ))
hR : R = Nat.rec (motive := fun (x : ℕ) ↦ α) (abv (f 0)) fun (i : ℕ) (c : (fun (x : ℕ) ↦ α) i) ↦ max c (abv (f i.succ))
this : ∀ (i j : ℕ), j ≤ i → abv (f j) ≤ R i
j : ℕ
inl : ∀ (hji : j ≤ i), abv (f j) < R i + 1
⊢ abv (f j) < R i + 1
have inr : ∀ (hij : i ≤ j), abv (f j) < R i + 1
Tactic: obtain hji | hij := le_total j i
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Ring β
abv : β → α
f : CauSeq β abv
g : ℕ → β
e : ∀ (i : ℕ), (↑f : ℕ → β) i = g i
ε : α
⊢ ε > 0 → ∃ (i : ℕ), ∀ j ≥ i, abv (g j - g i) < ε
have rw : ε > 0 → ∃ (i : ℕ), ∀ j ≥ i, abv ((↑f : ℕ → β) j - (↑f : ℕ → β) i) < ε
Tactic: rw [show g = f from (funext e).symm]
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.Basic (goal)
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 : ℕ), (↑(npowRec n f) : ℕ → β) i = (↑f : ℕ → β) i ^ n
have zero : ∀ (i : ℕ), (↑(npowRec 0 f) : ℕ → β) i = HPow.hPow (β := ℕ) ((↑f : ℕ → β) i) 0
Tactic: induction n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.Basic (goal)
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
⊢ ∀ (i : ℕ), (↑(npowRec n f) : ℕ → β) i = (↑f : ℕ → β) i ^ n
have succ : ∀ (n : ℕ),
  (∀ (i : ℕ), (↑(npowRec n f) : ℕ → β) i = (↑f : ℕ → β) i ^ n) →
    ∀ (i : ℕ), (↑(npowRec (n + 1) f) : ℕ → β) i = (↑f : ℕ → β) i ^ (n + 1)
Tactic: induction n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.Basic (hypothesis)
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 + g) : ℕ → β) j) < ε
have H₁ : abv ((↑f : ℕ → β) j) < ε / 2
Tactic: let ⟨H₁, H₂⟩ := H _ ij
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.Basic (hypothesis)
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 ((↑(f + g) : ℕ → β) j) < ε
have H₂ : abv ((↑g : ℕ → β) j) < ε / 2
Tactic: let ⟨H₁, H₂⟩ := H _ ij
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.Basic (hypothesis)
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 * g) : ℕ → β) j) < ε
have this : abv ((↑f : ℕ → β) j) * abv ((↑g : ℕ → β) j) < F * (ε / F)
Tactic: have := mul_lt_mul' (le_of_lt <| hF j) (H _ ij) (abv_nonneg abv _) F0
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.Basic (goal)
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)
⊢ abv ((↑(f * g) : ℕ → β) j) < ε
have rwa : ∀ (this : abv ((↑f : ℕ → β) j) * abv ((↑g : ℕ → β) j) < ε / F * F), abv ((↑(f * g) : ℕ → β) j) < ε
Tactic: rwa [mul_comm F, div_mul_cancel₀ _ (ne_of_gt F0), ← abv_mul] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.Basic (goal)
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) < ε
⊢ abv ((↑(f * g) : ℕ → β) j) < ε
have rwa₁ : ∀ (this : abv ((↑f : ℕ → β) j) * abv ((↑g : ℕ → β) j) < ε), abv ((↑(f * g) : ℕ → β) j) < ε
Tactic: rwa [mul_comm F, div_mul_cancel₀ _ (ne_of_gt F0), ← abv_mul] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.Basic (goal)
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) < ε
⊢ abv ((↑(f * g) : ℕ → β) j) < ε
have rwa₂ : ∀ (this : abv ((↑f : ℕ → β) j * (↑g : ℕ → β) j) < ε), abv ((↑(f * g) : ℕ → β) j) < ε
Tactic: rwa [mul_comm F, div_mul_cancel₀ _ (ne_of_gt F0), ← abv_mul] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.Basic (hypothesis)
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 * g) : ℕ → β) j) < ε
have this : abv ((↑f : ℕ → β) j) * abv ((↑g : ℕ → β) j) < ε / G * G
Tactic: have := mul_lt_mul'' (H _ ij) (hG j) (abv_nonneg abv _) (abv_nonneg abv _)
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.Basic (goal)
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
⊢ abv ((↑(f * g) : ℕ → β) j) < ε
have rwa : ∀ (this : abv ((↑f : ℕ → β) j) * abv ((↑g : ℕ → β) j) < ε), abv ((↑(f * g) : ℕ → β) j) < ε
Tactic: rwa [div_mul_cancel₀ _ (ne_of_gt G0), ← abv_mul] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.Basic (goal)
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) < ε
⊢ abv ((↑(f * g) : ℕ → β) j) < ε
have rwa₁ : ∀ (this : abv ((↑f : ℕ → β) j * (↑g : ℕ → β) j) < ε), abv ((↑(f * g) : ℕ → β) j) < ε
Tactic: rwa [div_mul_cancel₀ _ (ne_of_gt G0), ← abv_mul] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.Basic (goal)
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
⊢ (-f).LimZero
have rw : (-1 * f).LimZero
Tactic: rw [← neg_one_mul f]
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.Basic (hypothesis)
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 : ℕ → β) k - (↑g : ℕ → β) j) < ε
have h₁ : abv ((↑(f - g) : ℕ → β) j) < ε / 2
Tactic: let ⟨h₁, h₂⟩ := H _ ij
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.Basic (hypothesis)
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
⊢ abv ((↑f : ℕ → β) k - (↑g : ℕ → β) j) < ε
have h₂ : ∀ k ≥ j, abv ((↑f : ℕ → β) k - (↑f : ℕ → β) j) < ε / 2
Tactic: let ⟨h₁, h₂⟩ := H _ ij
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.Basic (hypothesis)
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 : ℕ → β) k - (↑g : ℕ → β) j) < ε
have this : 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))
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.Basic (goal)
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
⊢ abv ((↑f : ℕ → β) k - (↑g : ℕ → β) j) < ε
have rwa : ∀ (this : abv ((↑f : ℕ → β) k - (↑g : ℕ → β) j) < ε / 2 + ε / 2), abv ((↑f : ℕ → β) k - (↑g : ℕ → β) j) < ε
Tactic: rwa [sub_add_sub_cancel', add_halves] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.Basic (goal)
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) < ε
⊢ abv ((↑f : ℕ → β) k - (↑g : ℕ → β) j) < ε
have rwa₁ : ∀ (this : abv ((↑f : ℕ → β) k - (↑g : ℕ → β) j) < ε), abv ((↑f : ℕ → β) k - (↑g : ℕ → β) j) < ε
Tactic: rwa [sub_add_sub_cancel', add_halves] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.Basic (goal)
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
⊢ ∃ K > 0, ∃ (i : ℕ), ∀ j ≥ i, K ≤ abv ((↑f : ℕ → β) j)
have by_contra : ∀ (nk : ¬∃ K > 0, ∃ (i : ℕ), ∀ j ≥ i, K ≤ abv ((↑f : ℕ → β) j)), False
Tactic: by_contra nk
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.Basic (goal)
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
have refine : ∀ (ε : α) (ε0 : ε > 0), ∃ (i : ℕ), ∀ j ≥ i, abv ((↑f : ℕ → β) j) < ε
Tactic: refine hf fun ε ε0 => ?_
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.Basic (hypothesis)
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
⊢ ∃ (i : ℕ), ∀ j ≥ i, abv ((↑f : ℕ → β) j) < ε
have nk₁ : ∀ 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
Cleared hypotheses: nk
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.Basic (goal)
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 : ℕ), ∀ j ≥ i, abv ((↑f : ℕ → β) j) < ε
have obtain : ∀ (i : ℕ) (hi : ∀ j ≥ i, ∀ k ≥ j, abv ((↑f : ℕ → β) k - (↑f : ℕ → β) j) < ε / 2),
  ∃ (i : ℕ), ∀ j ≥ i, abv ((↑f : ℕ → β) j) < ε
Tactic: obtain ⟨i, hi⟩ := f.cauchy₃ (half_pos ε0)
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.Basic (goal)
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
⊢ ∃ (i : ℕ), ∀ j ≥ i, abv ((↑f : ℕ → β) j) < ε
have rcases : ∀ (j : ℕ) (ij : j ≥ i) (hj : abv ((↑f : ℕ → β) j) < ε / 2), ∃ (i : ℕ), ∀ j ≥ i, abv ((↑f : ℕ → β) j) < ε
Tactic: rcases nk _ (half_pos ε0) i with ⟨j, ij, hj⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.Basic (goal)
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) < ε
have refine : ∀ (k : ℕ) (jk : k ≥ j), abv ((↑f : ℕ → β) k) < ε
Tactic: refine ⟨j, fun k jk => ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.Basic (hypothesis)
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) < ε
have this : 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)
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.Basic (goal)
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
⊢ abv ((↑f : ℕ → β) k) < ε
have rwa : ∀ (this : abv ((↑f : ℕ → β) k) < ε / 2 + ε / 2), abv ((↑f : ℕ → β) k) < ε
Tactic: rwa [sub_add_cancel, add_halves] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.Basic (goal)
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) < ε
⊢ abv ((↑f : ℕ → β) k) < ε
have rwa₁ : ∀ (this : abv ((↑f : ℕ → β) k) < ε), abv ((↑f : ℕ → β) k) < ε
Tactic: rwa [sub_add_cancel, add_halves] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.Basic (hypothesis)
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 j - f i) < ε
have h₁ : abv (f i - (↑g : ℕ → β) i) < ε / 2 / 2
Tactic: obtain ⟨h₁, h₂⟩ := hi _ le_rfl
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.Basic (hypothesis)
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
⊢ abv (f j - f i) < ε
have h₂ : ∀ k ≥ i, abv ((↑g : ℕ → β) k - (↑g : ℕ → β) i) < ε / 2
Tactic: obtain ⟨h₁, h₂⟩ := hi _ le_rfl
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.Basic (hypothesis)
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 (f j - f i) < ε
have h₃ : abv ((↑g : ℕ → β) i - f i) < ε / 2 / 2
Tactic: rw [abv_sub abv] at h₁
Cleared hypotheses: h₁, h₂
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.Basic (hypothesis)
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 - f i) < ε
have this : 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₁)
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.Basic (hypothesis)
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 - f i) < ε
have this₁ : 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))
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.Basic (goal)
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
⊢ abv (f j - f i) < ε
have rwa : ∀ (this : abv (f j - (↑g : ℕ → β) j + ((↑g : ℕ → β) i - f i) + ((↑g : ℕ → β) j - (↑g : ℕ → β) i)) < ε / 2 + ε / 2),
  abv (f j - f i) < ε
Tactic: rwa [add_halves, add_halves, add_right_comm, sub_add_sub_cancel, sub_add_sub_cancel] at this
Cleared hypotheses: this