awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
β : Type u_3
inst_3 : DivisionRing β
abv : β → α
inst_4 : IsAbsoluteValue abv
ε K : α
ε0 : 0 < ε
K0 : 0 < K
a b : β
ha : K ≤ abv a
hb : K ≤ abv b
h : abv (a - b) < K * ε * K
a0 : 0 < abv a
b0 : 0 < abv b
refine : K * ε * K ≤ abv a * ε * abv b
⊢ abv (a - b) < abv a * ε * abv b

Tactic:
refine h.trans_le ?_

Premises used: LT.lt.trans_le
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
β : Type u_3
inst_3 : DivisionRing β
abv : β → α
inst_4 : IsAbsoluteValue abv
ε K : α
ε0 : 0 < ε
K0 : 0 < K
a b : β
ha : K ≤ abv a
hb : K ≤ abv b
h : abv (a - b) < K * ε * K
a0 : 0 < abv a
b0 : 0 < abv b
b0₁ : 0 ≤ abv a * ε
⊢ K * ε * K ≤ abv a * ε * abv b

Tactic:
gcongr
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
β : Type u_3
inst_3 : DivisionRing β
abv : β → α
inst_4 : IsAbsoluteValue abv
ε K : α
ε0 : 0 < ε
K0 : 0 < K
a b : β
ha : K ≤ abv a
hb : K ≤ abv b
h : abv (a - b) < K * ε * K
a0 : 0 < abv a
b0 : 0 < abv b
⊢ 0 ≤ abv a * ε

Tactic:
mul_nonneg a0.le ε0.le

Premises used: mul_nonneg, LT.lt.le
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
β : Type u_3
inst_3 : DivisionRing β
abv : β → α
inst_4 : IsAbsoluteValue abv
ε K : α
ε0 : 0 < ε
K0 : 0 < K
a b : β
ha : K ≤ abv a
hb : K ≤ abv b
h : abv (a - b) < K * ε * K
a0 : 0 < abv a
b0 : 0 < abv b
⊢ 0 ≤ abv a * ε

Tactic:
exact mul_nonneg a0.le ε0.le

Premises used: mul_nonneg, LT.lt.le
-- 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 : ℕ → β
hf : IsCauSeq abv f
ε : α
ε0 : 0 < ε
⊢ ∃ (i : ℕ), ∀ j ≥ i, ∀ k ≥ i, abv (f j - f k) < ε

Tactic:
(hf _ (half_pos ε0)).imp fun i hi j ij k ik => ?_

Premises used: half_pos, Exists.imp
-- 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 : ℕ → β
hf : IsCauSeq abv f
ε : α
ε0 : 0 < ε
refine :
  ∀ (i : ℕ) (hi : ∀ j ≥ i, abv (f j - f i) < ε / 2) (j : ℕ) (ij : j ≥ i) (k : ℕ) (ik : k ≥ i), abv (f j - f k) < ε
⊢ ∃ (i : ℕ), ∀ j ≥ i, ∀ k ≥ i, abv (f j - f k) < ε

Tactic:
refine (hf _ (half_pos ε0)).imp fun i hi j ij k ik => ?_

Premises used: half_pos, Exists.imp
-- 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 : ℕ → β
hf : IsCauSeq abv f
ε : α
ε0 : 0 < ε
i : ℕ
hi : ∀ j ≥ i, abv (f j - f i) < ε / 2
j : ℕ
ij : j ≥ i
k : ℕ
ik : k ≥ i
rw : abv (f j - f k) < ε / 2 + ε / 2
⊢ abv (f j - f k) < ε

Tactic:
rw [← add_halves ε]

Premises used: add_halves
-- 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 : ℕ → β
hf : IsCauSeq abv f
ε : α
ε0 : 0 < ε
i : ℕ
hi : ∀ j ≥ i, abv (f j - f i) < ε / 2
j : ℕ
ij : j ≥ i
k : ℕ
ik : k ≥ i
⊢ abv (f j - f k) < ε / 2 + ε / 2

Tactic:
lt_of_le_of_lt (abv_sub_le abv _ _ _) (add_lt_add (hi _ ij) ?_)

Premises used: lt_of_le_of_lt, add_lt_add, IsAbsoluteValue.abv_sub_le
-- 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 : ℕ → β
hf : IsCauSeq abv f
ε : α
ε0 : 0 < ε
i : ℕ
hi : ∀ j ≥ i, abv (f j - f i) < ε / 2
j : ℕ
ij : j ≥ i
k : ℕ
ik : k ≥ i
refine : abv (f i - f k) < ε / 2
⊢ abv (f j - f k) < ε / 2 + ε / 2

Tactic:
refine lt_of_le_of_lt (abv_sub_le abv _ _ _) (add_lt_add (hi _ ij) ?_)

Premises used: lt_of_le_of_lt, add_lt_add, IsAbsoluteValue.abv_sub_le
-- 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 : ℕ → β
hf : IsCauSeq abv f
ε : α
ε0 : 0 < ε
i : ℕ
hi : ∀ j ≥ i, abv (f j - f i) < ε / 2
j : ℕ
ij : j ≥ i
k : ℕ
ik : k ≥ i
rw : abv (f k - f i) < ε / 2
⊢ abv (f i - f k) < ε / 2

Tactic:
rw [abv_sub abv]

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 : ℕ → β
hf : IsCauSeq abv f
ε : α
ε0 : 0 < ε
i : ℕ
hi : ∀ j ≥ i, abv (f j - f i) < ε / 2
j : ℕ
ij : j ≥ i
k : ℕ
ik : k ≥ i
⊢ abv (f k - f i) < ε / 2

Tactic:
hi _ ik
-- 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 : ℕ → β
hf : IsCauSeq abv f
ε : α
ε0 : 0 < ε
i : ℕ
hi : ∀ j ≥ i, abv (f j - f i) < ε / 2
j : ℕ
ij : j ≥ i
k : ℕ
ik : k ≥ i
⊢ abv (f k - f i) < ε / 2

Tactic:
exact hi _ ik
-- 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 : ℕ → β
hf : IsCauSeq abv f
ε : α
ε0 : 0 < ε
⊢ ∃ (i : ℕ), ∀ j ≥ i, ∀ k ≥ j, abv (f k - f j) < ε

Tactic:
let ⟨i, H⟩ := hf.cauchy₂ ε0
  ⟨i, fun _ ij _ jk => H _ (le_trans ij jk) _ ij⟩

Premises used: Exists, IsCauSeq.cauchy₂, Exists.intro, _private.0.IsCauSeq.cauchy₃.match_1, le_trans
-- 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 : ℕ → β
hf : IsCauSeq abv f
obtain : ∀ (i : ℕ) (h : ∀ j ≥ i, abv (f j - f i) < 1), ∃ (r : α), ∀ (i : ℕ), abv (f i) < r
⊢ ∃ (r : α), ∀ (i : ℕ), abv (f i) < r

Tactic:
obtain ⟨i, h⟩ := hf _ zero_lt_one

Premises used: zero_lt_one
-- 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 : ℕ → β
hf : IsCauSeq abv f
i : ℕ
h : ∀ j ≥ i, abv (f j - f i) < 1
⊢ let R : ℕ → α :=
    Nat.rec (motive := fun (x : ℕ) ↦ α) (abv (f 0)) fun (i : ℕ) (c : (fun (x : ℕ) ↦ α) i) ↦ max c (abv (f i.succ));
  R = Nat.rec (motive := fun (x : ℕ) ↦ α) (abv (f 0)) fun (i : ℕ) (c : (fun (x : ℕ) ↦ α) i) ↦ max c (abv (f i.succ))

Tactic:
set R : ℕ → α := @Nat.rec (fun _ => α) (abv (f 0)) fun i c => max c (abv (f i.succ)) with hR

Premises used: Nat.rec, Max.max, OfNat.ofNat, Nat.succ
-- Module: Mathlib.Algebra.Order.CauSeq.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Ring β
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))
⊢ ∀ j ≤ Nat.zero, abv (f j) ≤ R Nat.zero

Tactic:
simp [hR]
-- 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 : ℕ → β
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))
refine : ∀ (n : ℕ) (n_ih : ∀ j ≤ n, abv (f j) ≤ R n), ∀ j ≤ n.succ, abv (f j) ≤ R n.succ
⊢ ∀ (i j : ℕ), j ≤ i → abv (f j) ≤ R i

Tactic:
refine Nat.rec (by simp [hR]) ?_
-- 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 : ℕ → β
hf : IsCauSeq abv f
i_1 : ℕ
h : ∀ j ≥ i_1, abv (f j - f i_1) < 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))
i : ℕ
hi : ∀ j ≤ i, abv (f j) ≤ R i
⊢ abv (f i.succ) ≤ R i.succ

Tactic:
simp [R]
-- 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 : ℕ → β
hf : IsCauSeq abv f
i_1 : ℕ
h : ∀ j ≥ i_1, abv (f j - f i_1) < 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))
i : ℕ
hi : ∀ j ≤ i, abv (f j) ≤ R i
j : ℕ
hj : j.le i
⊢ abv (f j) ≤ R i.succ

Tactic:
(hi j hj).trans (le_max_left _ _)

Premises used: LE.le.trans, 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 : ℕ → β
hf : IsCauSeq abv f
i_1 : ℕ
h : ∀ j ≥ i_1, abv (f j - f i_1) < 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))
i : ℕ
hi : ∀ j ≤ i, abv (f j) ≤ R i
j : ℕ
hj : j.le i
⊢ abv (f j) ≤ R i.succ

Tactic:
exact (hi j hj).trans (le_max_left _ _)

Premises used: LE.le.trans, 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 : ℕ → β
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))
⊢ ∀ (i j : ℕ), j ≤ i → abv (f j) ≤ R i

Tactic:
have : ∀ i, ∀ j ≤ i, abv (f j) ≤ R i := by
    refine Nat.rec (by simp [hR]) ?_
    rintro i hi j (rfl | hj)
    · simp [R]
    · exact (hi j hj).trans (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 : ℕ → β
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

Tactic:
⟨R i + 1, fun j ↦ ?_⟩

Premises used: HAdd.hAdd, Exists.intro, OfNat.ofNat
-- 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 : ℕ → β
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
refine : ∀ (j : ℕ), abv (f j) < R i + 1
⊢ ∃ (r : α), ∀ (i : ℕ), abv (f i) < r

Tactic:
refine ⟨R i + 1, fun j ↦ ?_⟩
-- 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 : ℕ → β
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
inr : ∀ (hij : i ≤ j), abv (f j) < R i + 1
⊢ abv (f j) < R i + 1

Tactic:
obtain hji | hij := le_total j i

Premises used: le_total
-- 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 : ℕ → β
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 : ℕ
hji : j ≤ i
⊢ abv (f j) < R i + 1

Tactic:
(this i _ hji).trans_lt (lt_add_one _)

Premises used: lt_add_one, LE.le.trans_lt
-- 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 : ℕ → β
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 : ℕ
hji : j ≤ i
⊢ abv (f j) < R i + 1

Tactic:
exact (this i _ hji).trans_lt (lt_add_one _)

Premises used: lt_add_one, LE.le.trans_lt
-- 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 : ℕ → β
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 : ℕ
hij : i ≤ j
⊢ abv (f j) < R i + 1

Tactic:
simpa using (abv_add abv _ _).trans_lt <| add_lt_add_of_le_of_lt (this i _ le_rfl) (h _ hij)

Premises used: add_lt_add_of_le_of_lt, le_rfl, IsAbsoluteValue.abv_add, LE.le.trans_lt
-- 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 : ℕ → β
hf : IsCauSeq abv f
x : α
⊢ ∃ r > x, ∀ (i : ℕ), abv (f i) < r

Tactic:
let ⟨r, h⟩ := hf.bounded
  ⟨max r (x + 1), (lt_add_one x).trans_le (le_max_right _ _),
    fun i ↦ (h i).trans_le (le_max_left _ _)⟩

Premises used: le_max_right, lt_add_one, Exists, IsCauSeq.bounded, _private.0.IsCauSeq.bounded'.match_1, GT.gt, And, HAdd.hAdd, Max.max, LT.lt.trans_le, And.intro, Exists.intro, OfNat.ofNat, 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
x : β
ε : α
ε0 : ε > 0
j : ℕ
h : j ≥ 0
⊢ abv (HSub.hSub (α := β) ((fun (x_1 : ℕ) ↦ x) j) ((fun (x_1 : ℕ) ↦ x) 0)) < ε

Tactic:
simpa [abv_zero] 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
f g : ℕ → β
hf : IsCauSeq abv f
hg : IsCauSeq abv g
⊢ IsCauSeq abv (f + g)

Tactic:
fun _ ε0 =>
  let ⟨_, δ0, Hδ⟩ := rat_add_continuous_lemma abv ε0
  let ⟨i, H⟩ := exists_forall_ge_and (hf.cauchy₃ δ0) (hg.cauchy₃ δ0)
  ⟨i, fun _ ij =>
    let ⟨H₁, H₂⟩ := H _ le_rfl
    Hδ (H₁ _ ij) (H₂ _ ij)⟩

Premises used: _private.0.IsCauSeq.add.match_2, le_rfl, HSub.hSub, _private.0.IsCauSeq.add.match_1, Exists, IsCauSeq.cauchy₃, HAdd.hAdd, LT.lt, Exists.intro, exists_forall_ge_and, _private.0.IsCauSeq.add.match_3, IsCauSeq, rat_add_continuous_lemma
-- 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 : ℕ → β
hf : IsCauSeq abv f
hg : IsCauSeq abv g
⊢ IsCauSeq abv (f * g)

Tactic:
fun _ ε0 =>
  let ⟨_, _, hF⟩ := hf.bounded' 0
  let ⟨_, _, hG⟩ := hg.bounded' 0
  let ⟨_, δ0, Hδ⟩ := rat_mul_continuous_lemma abv ε0
  let ⟨i, H⟩ := exists_forall_ge_and (hf.cauchy₃ δ0) (hg.cauchy₃ δ0)
  ⟨i, fun j ij =>
    let ⟨H₁, H₂⟩ := H _ le_rfl
    Hδ (hF j) (hG i) (H₁ _ ij) (H₂ _ ij)⟩

Premises used: _private.0.IsCauSeq.add.match_2, IsCauSeq.bounded', le_rfl, HMul.hMul, HSub.hSub, _private.0.IsCauSeq.add.match_1, Exists, _private.0.IsCauSeq.mul.match_2, IsCauSeq.cauchy₃, rat_mul_continuous_lemma, LT.lt, Exists.intro, exists_forall_ge_and, OfNat.ofNat, IsCauSeq, _private.0.IsCauSeq.mul.match_1
-- 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 : ℕ → β
⊢ IsCauSeq abv (-f) ↔ IsCauSeq abv f

Tactic:
simp only [IsCauSeq, Pi.neg_apply, ← neg_sub', abv_neg]

Premises used: neg_sub', IsCauSeq, Pi.neg_apply, IsAbsoluteValue.abv_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 : β → α
f g : CauSeq β abv
h : ∀ (i : ℕ), (↑f : ℕ → β) i = (↑g : ℕ → β) i
⊢ f = g

Tactic:
Subtype.ext (funext h)

Premises used: funext, CauSeq, 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 : β → α
f : CauSeq β abv
⊢ IsCauSeq abv (↑f : ℕ → β)

Tactic:
f.2

Premises used: Subtype.property
-- 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 : β → α
f : CauSeq β abv
⊢ ∀ {ε : α}, 0 < ε → ∃ (i : ℕ), ∀ j ≥ i, abv ((↑f : ℕ → β) j - (↑f : ℕ → β) i) < ε

Tactic:
@f.2

Premises used: IsCauSeq, Subtype.property
-- 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 : β → α
f : CauSeq β abv
g : ℕ → β
e : ∀ (i : ℕ), (↑f : ℕ → β) i = g i
ε : α
rw : ε > 0 → ∃ (i : ℕ), ∀ j ≥ i, abv ((↑f : ℕ → β) j - (↑f : ℕ → β) i) < ε
⊢ ε > 0 → ∃ (i : ℕ), ∀ j ≥ i, abv (g j - g i) < ε

Tactic:
rw [show g = f from (funext e).symm]

Premises used: funext, Eq.symm
-- 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 : β → α
f : CauSeq β abv
g : ℕ → β
e : ∀ (i : ℕ), (↑f : ℕ → β) i = g i
ε : α
⊢ ε > 0 → ∃ (i : ℕ), ∀ j ≥ i, abv ((↑f : ℕ → β) j - (↑f : ℕ → β) i) < ε

Tactic:
f.cauchy

Premises used: 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 : β → α
f : CauSeq β abv
g : ℕ → β
e : ∀ (i : ℕ), (↑f : ℕ → β) i = g i
ε : α
⊢ ε > 0 → ∃ (i : ℕ), ∀ j ≥ i, abv ((↑f : ℕ → β) j - (↑f : ℕ → β) i) < ε

Tactic:
exact f.cauchy

Premises used: 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
ε : α
⊢ 0 < ε → ∃ (i : ℕ), ∀ j ≥ i, ∀ k ≥ i, abv ((↑f : ℕ → β) j - (↑f : ℕ → β) k) < ε

Tactic:
f.2.cauchy₂

Premises used: IsCauSeq.cauchy₂, Subtype.property
-- 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
ε : α
⊢ 0 < ε → ∃ (i : ℕ), ∀ j ≥ i, ∀ k ≥ j, abv ((↑f : ℕ → β) k - (↑f : ℕ → β) j) < ε

Tactic:
f.2.cauchy₃

Premises used: IsCauSeq.cauchy₃, Subtype.property
-- 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
⊢ ∃ (r : α), ∀ (i : ℕ), abv ((↑f : ℕ → β) i) < r

Tactic:
f.2.bounded

Premises used: IsCauSeq.bounded, Subtype.property
-- 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
x : α
⊢ ∃ r > x, ∀ (i : ℕ), abv ((↑f : ℕ → β) i) < r

Tactic:
f.2.bounded' x

Premises used: IsCauSeq.bounded', Subtype.property
-- 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 : β
⊢ (↑(const x) : ℕ → β) = Function.const ℕ x

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 : β
i : ℕ
⊢ (↑(const x) : ℕ → β) i = x

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 : β
⊢ Eq (α := CauSeq β abv) (const x) (const y) ↔ x = y

Tactic:
⟨fun h => congr_arg (fun f : CauSeq β abv => (f : ℕ → β) 0) h, congr_arg _⟩

Premises used: congr_arg, Iff.intro, OfNat.ofNat, Subtype.val
-- 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.{u_2 + 1} (α := ℕ → β) (↑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.{u_2 + 1} (α := ℕ → β) (↑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
i : ℕ
⊢ Eq.{u_2 + 1} (α := β) ((↑0 : ℕ → β) i) 0

Tactic:
rfl

Premises used: rfl