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 : ℕ → β
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) < ε
⊢ abv (f j - f i) < ε
have rwa₁ : ∀ (this : abv (f j - (↑g : ℕ → β) j + ((↑g : ℕ → β) i - f i) + ((↑g : ℕ → β) j - (↑g : ℕ → β) 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
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 : ∀ ε > 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) < ε
⊢ abv (f j - f i) < ε
have rwa₂ : ∀ (this : abv (f j - (↑g : ℕ → β) j + ((↑g : ℕ → β) j - (↑g : ℕ → β) i) + ((↑g : ℕ → β) i - 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
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 : ∀ ε > 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) < ε
⊢ abv (f j - f i) < ε
have rwa₃ : ∀ (this : abv (f j - (↑g : ℕ → β) i + ((↑g : ℕ → β) i - 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
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 : ∀ ε > 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) < ε
⊢ abv (f j - f i) < ε
have rwa₄ : ∀ (this : 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
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 : CauSeq β abv
hf : ¬f ≈ 0
h : f.LimZero
⊢ False
have this : (f - 0).LimZero
Tactic: have : LimZero (f - 0) := by simp [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
hf : ¬f ≈ 0
hg : ¬g ≈ 0
this : (f * g - 0).LimZero
⊢ False
have hlz : (f * g).LimZero
Tactic: have hlz : LimZero (f * g) := by simpa
-- 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 ≈ 0
hg : ¬g ≈ 0
this : (f * g - 0).LimZero
hlz : (f * g).LimZero
⊢ False
have hf' : ¬f.LimZero
Tactic: have hf' : ¬LimZero f := by simpa using show ¬LimZero (f - 0) from hf
-- 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 ≈ 0
hg : ¬g ≈ 0
this : (f * g - 0).LimZero
hlz : (f * g).LimZero
hf' : ¬f.LimZero
⊢ False
have hg' : ¬g.LimZero
Tactic: have hg' : ¬LimZero g := by simpa using show ¬LimZero (g - 0) from hg
-- 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
hf : ¬f ≈ 0
hg : ¬g ≈ 0
this : (f * g - 0).LimZero
hlz : (f * g).LimZero
hf' : ¬f.LimZero
hg' : ¬g.LimZero
⊢ False
have rcases : ∀ (a1 : α) (ha1 : a1 > 0) (N1 : ℕ) (hN1 : ∀ j ≥ N1, a1 ≤ abv ((↑f : ℕ → β) j)), False
Tactic: rcases abv_pos_of_not_limZero hf' with ⟨a1, ha1, N1, hN1⟩
-- 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
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)
⊢ False
have rcases : ∀ (a2 : α) (ha2 : a2 > 0) (N2 : ℕ) (hN2 : ∀ j ≥ N2, a2 ≤ abv ((↑g : ℕ → β) j)), False
Tactic: rcases abv_pos_of_not_limZero hg' with ⟨a2, ha2, N2, hN2⟩
-- 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 ≈ 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)
⊢ False
have this₁ : 0 < a1 * a2
Tactic: have : 0 < a1 * a2 := mul_pos ha1 ha2
-- 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
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
⊢ False
have obtain : ∀ (N : ℕ) (hN : ∀ j ≥ N, abv ((↑(f * g) : ℕ → β) j) < a1 * a2), False
Tactic: obtain ⟨N, hN⟩ := hlz _ 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
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)
⊢ False
have hN' : abv ((↑(f * g) : ℕ → β) i) < a1 * a2
Tactic: have hN' := hN i (le_max_left _ _)
-- 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 ≈ 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
⊢ False
have hN1' : a1 ≤ abv ((↑f : ℕ → β) i)
Tactic: have hN1' := hN1 i (le_trans (le_max_left _ _) (le_max_right _ _))
-- 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 ≈ 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)
⊢ False
have hN1'₁ : a2 ≤ abv ((↑g : ℕ → β) i)
Tactic: have hN1' := hN2 i (le_trans (le_max_right _ _) (le_max_right _ _))
-- 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
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)
⊢ False
have apply : a1 * a2 ≤ abv ((↑(f * g) : ℕ → β) i)
Tactic: apply not_le_of_gt hN'
-- 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
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)
⊢ a1 * a2 ≤ abv ((↑(f * g) : ℕ → β) i)
have change : a1 * a2 ≤ abv ((↑f : ℕ → β) i * (↑g : ℕ → β) i)
Tactic: change _ ≤ 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
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)
⊢ a1 * a2 ≤ abv ((↑f : ℕ → β) i * (↑g : ℕ → β) i)
have rw : a1 * a2 ≤ abv ((↑f : ℕ → β) i) * abv ((↑g : ℕ → β) i)
Tactic: rw [abv_mul 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
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)
⊢ a1 * a2 ≤ abv ((↑f : ℕ → β) i) * abv ((↑g : ℕ → β) i)
have c0 : 0 ≤ a2
Tactic: gcongr
-- 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
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
⊢ a1 * a2 ≤ abv ((↑f : ℕ → β) i) * abv ((↑g : ℕ → β) i)
have b0 : 0 ≤ abv ((↑f : ℕ → β) i)
Tactic: gcongr
-- 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
x y : β
⊢ (HSub.hSub (α := CauSeq β abv) (const x) (const y)).LimZero ↔ x = y
have rw : LimZero (const (x - y)) ↔ x = y
Tactic: rw [← const_sub, const_limZero, sub_eq_zero]
-- 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
x y : β
rw : LimZero (const (x - y)) ↔ x = y
⊢ (HSub.hSub (α := CauSeq β abv) (const x) (const y)).LimZero ↔ x = y
have rw₁ : x - y = 0 ↔ x = y
Tactic: rw [← const_sub, const_limZero, sub_eq_zero]
-- 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
x y : β
rw : LimZero (const (x - y)) ↔ x = y
rw₁ : x - y = 0 ↔ x = y
⊢ (HSub.hSub (α := CauSeq β abv) (const x) (const y)).LimZero ↔ x = y
have rw₂ : x = y ↔ x = y
Tactic: rw [← const_sub, const_limZero, sub_eq_zero]
-- 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
f1 f2 : CauSeq β abv
hf : f1 ≈ f2
n : ℕ
⊢ f1 ^ n ≈ f2 ^ n
have zero : HPow.hPow (β := ℕ) f1 0 ≈ HPow.hPow (β := ℕ) f2 0
Tactic: induction n with
  | zero => simp only [pow_zero, Setoid.refl]
  | succ n ih => simpa only [pow_succ'] using mul_equiv_mul hf ih
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
f1 f2 : CauSeq β abv
hf : f1 ≈ f2
n : ℕ
zero : HPow.hPow (β := ℕ) f1 0 ≈ HPow.hPow (β := ℕ) f2 0
⊢ f1 ^ n ≈ f2 ^ n
have succ : ∀ (n : ℕ) (ih : f1 ^ n ≈ f2 ^ n), f1 ^ (n + 1) ≈ f2 ^ (n + 1)
Tactic: induction n with
  | zero => simp only [pow_zero, Setoid.refl]
  | succ n ih => simpa only [pow_succ'] using mul_equiv_mul hf ih
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 : DivisionRing β
abv : β → α
inst_4 : IsAbsoluteValue abv
x : β
hx : x ≠ 0
⊢ ¬LimZero (const abv x)
have rwa : ¬x = 0
Tactic: rwa [const_limZero]
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.Basic (hypothesis)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
f g : CauSeq α abs
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 / 2 ≤ (↑(f + g) : ℕ → α) j
have h₁ : F ≤ (↑f : ℕ → α) j
Tactic: obtain ⟨h₁, h₂⟩ := h j ij
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.Basic (hypothesis)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
f 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
⊢ F / 2 ≤ (↑(f + g) : ℕ → α) j
have h₂ : |(↑g : ℕ → α) j| < F / 2
Tactic: obtain ⟨h₁, h₂⟩ := h j ij
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.Basic (hypothesis)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
f 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 / 2 ≤ (↑(f + g) : ℕ → α) j
have this : F + -(F / 2) ≤ (↑f : ℕ → α) j + (↑g : ℕ → α) j
Tactic: have := add_le_add h₁ (le_of_lt (abs_lt.1 h₂).1)
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.Basic (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
f g : CauSeq α abs
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
⊢ F / 2 ≤ (↑(f + g) : ℕ → α) j
have rwa : ∀ (this : F - F / 2 ≤ (↑f : ℕ → α) j + (↑g : ℕ → α) j), F / 2 ≤ (↑(f + g) : ℕ → α) j
Tactic: rwa [← sub_eq_add_neg, sub_self_div_two] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.Basic (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
f g : 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
⊢ F / 2 ≤ (↑(f + g) : ℕ → α) j
have rwa₁ : ∀ (this : F / 2 ≤ (↑f : ℕ → α) j + (↑g : ℕ → α) j), F / 2 ≤ (↑(f + g) : ℕ → α) j
Tactic: rwa [← sub_eq_add_neg, sub_self_div_two] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.Basic (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
f : CauSeq α abs
⊢ f.Pos ∨ f.LimZero ∨ (-f).Pos
have inl : ∀ (h : f.LimZero), f.Pos ∨ f.LimZero ∨ (-f).Pos
Tactic: rcases Classical.em (LimZero f) with h | h
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.Basic (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
f : CauSeq α abs
inl : ∀ (h : f.LimZero), f.Pos ∨ f.LimZero ∨ (-f).Pos
⊢ f.Pos ∨ f.LimZero ∨ (-f).Pos
have inr : ∀ (h : ¬f.LimZero), f.Pos ∨ f.LimZero ∨ (-f).Pos
Tactic: rcases Classical.em (LimZero f) with h | h
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.Basic (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
f : CauSeq α abs
h : ¬f.LimZero
⊢ f.Pos ∨ f.LimZero ∨ (-f).Pos
have inr : f.Pos ∨ (-f).Pos
Tactic: simp only [false_or, h]
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.Basic (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
f : CauSeq α abs
h : ¬f.LimZero
⊢ f.Pos ∨ (-f).Pos
have inr : ∀ (K : α) (K0 : K > 0) (hK : ∃ (i : ℕ), ∀ j ≥ i, K ≤ |(↑f : ℕ → α) j|), f.Pos ∨ (-f).Pos
Tactic: rcases abv_pos_of_not_limZero h with ⟨K, K0, hK⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.Basic (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
f : CauSeq α abs
h : ¬f.LimZero
K : α
K0 : K > 0
hK : ∃ (i : ℕ), ∀ j ≥ i, K ≤ |(↑f : ℕ → α) j|
⊢ f.Pos ∨ (-f).Pos
have inr : ∀ (i : ℕ) (hi : ∀ j ≥ i, K ≤ |(↑f : ℕ → α) j| ∧ ∀ k ≥ j, |(↑f : ℕ → α) k - (↑f : ℕ → α) j| < K), f.Pos ∨ (-f).Pos
Tactic: rcases exists_forall_ge_and hK (f.cauchy₃ K0) with ⟨i, hi⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.Basic (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
f : CauSeq α abs
h : ¬f.LimZero
K : α
K0 : K > 0
hK : ∃ (i : ℕ), ∀ j ≥ i, K ≤ |(↑f : ℕ → α) j|
i : ℕ
hi : ∀ j ≥ i, K ≤ |(↑f : ℕ → α) j| ∧ ∀ k ≥ j, |(↑f : ℕ → α) k - (↑f : ℕ → α) j| < K
⊢ f.Pos ∨ (-f).Pos
have inr : 0 ≤ (↑f : ℕ → α) i → f.Pos
Tactic: refine (le_total 0 (f i)).imp ?_ ?_
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.Basic (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
f : CauSeq α abs
h : ¬f.LimZero
K : α
K0 : K > 0
hK : ∃ (i : ℕ), ∀ j ≥ i, K ≤ |(↑f : ℕ → α) j|
i : ℕ
hi : ∀ j ≥ i, K ≤ |(↑f : ℕ → α) j| ∧ ∀ k ≥ j, |(↑f : ℕ → α) k - (↑f : ℕ → α) j| < K
inr : 0 ≤ (↑f : ℕ → α) i → f.Pos
⊢ f.Pos ∨ (-f).Pos
have inr₁ : (↑f : ℕ → α) i ≤ 0 → (-f).Pos
Tactic: refine (le_total 0 (f i)).imp ?_ ?_