awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Order.CauSeq.BigOperators
Goal:
α : Type u_1
β : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Ring β
abv : β → α
inst_4 : IsAbsoluteValue abv
inst_5 : Archimedean α
inst_6 : Nontrivial β
x : β
hx1 : abv x < 1
hx1' : abv x ≠ 1
this : 0 < 1 - abv x
n : ℕ
h : n ≥ 0
refine_1 : 1 - abv x ^ n ≤ 1
⊢ (1 - abv x ^ n) / (1 - abv x) ≤ 1 / (1 - abv x)

Tactic:
gcongr
-- Module: Mathlib.Algebra.Order.CauSeq.BigOperators
Goal:
α : Type u_1
β : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Ring β
abv : β → α
inst_4 : IsAbsoluteValue abv
inst_5 : Archimedean α
inst_6 : Nontrivial β
x : β
hx1 : abv x < 1
hx1' : abv x ≠ 1
this : 0 < 1 - abv x
n : ℕ
h : n ≥ 0
⊢ 1 - abv x ^ n ≤ 1

Tactic:
sub_le_self _ (abv_pow abv x n ▸ abv_nonneg _ _)

Premises used: IsAbsoluteValue.abv_nonneg, Eq.rec, IsAbsoluteValue.abv_pow, sub_le_self
-- Module: Mathlib.Algebra.Order.CauSeq.BigOperators
Goal:
α : Type u_1
β : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Ring β
abv : β → α
inst_4 : IsAbsoluteValue abv
inst_5 : Archimedean α
inst_6 : Nontrivial β
x : β
hx1 : abv x < 1
hx1' : abv x ≠ 1
this : 0 < 1 - abv x
n : ℕ
h : n ≥ 0
⊢ 1 - abv x ^ n ≤ 1

Tactic:
exact sub_le_self _ (abv_pow abv x n ▸ abv_nonneg _ _)

Premises used: sub_le_self
-- Module: Mathlib.Algebra.Order.CauSeq.BigOperators
Goal:
α : Type u_1
β : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Ring β
abv : β → α
inst_4 : IsAbsoluteValue abv
inst_5 : Archimedean α
inst_6 : Nontrivial β
x : β
hx1 : abv x < 1
hx1' : abv x ≠ 1
this : 0 < 1 - abv x
n : ℕ
h : n ≥ 0
⊢ 0 ≤ (1 - abv x ^ n) / (1 - abv x)

Tactic:
div_nonneg (sub_nonneg.2 ?_) (sub_nonneg.2 <| le_of_lt hx1)

Premises used: Iff.mpr, le_of_lt, div_nonneg, sub_nonneg
-- Module: Mathlib.Algebra.Order.CauSeq.BigOperators
Goal:
α : Type u_1
β : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Ring β
abv : β → α
inst_4 : IsAbsoluteValue abv
inst_5 : Archimedean α
inst_6 : Nontrivial β
x : β
hx1 : abv x < 1
hx1' : abv x ≠ 1
this : 0 < 1 - abv x
n : ℕ
h : n ≥ 0
refine_1 : abv x ^ n ≤ 1
⊢ 0 ≤ (1 - abv x ^ n) / (1 - abv x)

Tactic:
refine div_nonneg (sub_nonneg.2 ?_) (sub_nonneg.2 <| le_of_lt hx1)

Premises used: Iff.mpr, le_of_lt, div_nonneg, sub_nonneg
-- Module: Mathlib.Algebra.Order.CauSeq.BigOperators
Goal:
α : Type u_1
β : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Ring β
abv : β → α
inst_4 : IsAbsoluteValue abv
inst_5 : Archimedean α
inst_6 : Nontrivial β
x : β
hx1 : abv x < 1
hx1' : abv x ≠ 1
this : 0 < 1 - abv x
n : ℕ
h : n ≥ 0
⊢ 0 ≤ abv x

Tactic:
positivity
-- Module: Mathlib.Algebra.Order.CauSeq.BigOperators
Goal:
α : Type u_1
β : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Ring β
abv : β → α
inst_4 : IsAbsoluteValue abv
inst_5 : Archimedean α
inst_6 : Nontrivial β
x : β
hx1 : abv x < 1
hx1' : abv x ≠ 1
this : 0 < 1 - abv x
n : ℕ
h : n ≥ 0
⊢ abv x ^ n ≤ 1

Tactic:
exact pow_le_one₀ (by positivity) hx1.le

Premises used: LT.lt.le, pow_le_one₀
-- Module: Mathlib.Algebra.Order.CauSeq.BigOperators
Goal:
α : Type u_1
β : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Ring β
abv : β → α
inst_4 : IsAbsoluteValue abv
inst_5 : Archimedean α
inst_6 : Nontrivial β
x : β
hx1 : abv x < 1
hx1' : abv x ≠ 1
this : 0 < 1 - abv x
n : ℕ
refine_2 : n ≥ 0 → (1 - abv x ^ n) / (1 - abv x) ≤ (1 - abv x ^ n.succ) / (1 - abv x)
⊢ n ≥ 0 → (1 - abv x ^ n) / (1 - abv x) ≤ (1 - abv x ^ n.succ) / (1 - abv x)

Tactic:
_
-- Module: Mathlib.Algebra.Order.CauSeq.BigOperators
Goal:
α : Type u_1
β : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Ring β
abv : β → α
inst_4 : IsAbsoluteValue abv
inst_5 : Archimedean α
inst_6 : Nontrivial β
x : β
hx1 : abv x < 1
hx1' : abv x ≠ 1
this : 0 < 1 - abv x
n : ℕ
h : n ≥ 0
refine_2 : (1 - 1 * abv x ^ n) / (1 - abv x) ≤ (1 - abv x * abv x ^ n) / (1 - abv x)
⊢ (1 - abv x ^ n) / (1 - abv x) ≤ (1 - abv x ^ n.succ) / (1 - abv x)

Tactic:
rw [← one_mul (abv x ^ n), pow_succ']

Premises used: HPow.hPow, pow_succ', one_mul
-- Module: Mathlib.Algebra.Order.CauSeq.BigOperators
Goal:
α : Type u_1
β : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Ring β
abv : β → α
inst_4 : IsAbsoluteValue abv
inst_5 : Archimedean α
inst_6 : Nontrivial β
x : β
hx1 : abv x < 1
hx1' : abv x ≠ 1
this : 0 < 1 - abv x
n : ℕ
h : n ≥ 0
refine_2 : 0 ≤ 1 - abv x
refine_2₁ : 0 ≤ abv x ^ n
⊢ (1 - 1 * abv x ^ n) / (1 - abv x) ≤ (1 - abv x * abv x ^ n) / (1 - abv x)

Tactic:
gcongr
-- Module: Mathlib.Algebra.Order.CauSeq.BigOperators
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Archimedean α
a x : α
hx1 : |x| < 1
⊢ IsCauSeq.{u_1, u_1} (α := α) abs fun (m : ℕ) ↦ ∑ n ∈ range m, a * x ^ n

Tactic:
simpa [mul_sum, Pi.mul_def] using (const a).mul (geo_series x hx1)

Premises used: Finset.mul_sum, IsCauSeq.const, IsCauSeq.geo_series, Pi.mul_def, IsCauSeq.mul
-- Module: Mathlib.Algebra.Order.CauSeq.BigOperators
Goal:
α : Type u_1
β : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Ring β
abv : β → α
inst_4 : IsAbsoluteValue abv
inst_5 : Archimedean α
f : ℕ → β
n : ℕ
r : α
hr0 : 0 ≤ r
hr1 : r < 1
h : ∀ (m : ℕ), n ≤ m → abv (f m.succ) ≤ r * abv (f m)
rwa rwa₁ rwa₂ rwa₃ : r < 1
⊢ |r| < 1

Tactic:
rwa [abs_of_nonneg hr0]

Premises used: abs_of_nonneg
-- Module: Mathlib.Algebra.Order.CauSeq.BigOperators
Goal:
α : Type u_1
β : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Ring β
abv : β → α
inst_4 : IsAbsoluteValue abv
inst_5 : Archimedean α
f : ℕ → β
n : ℕ
r : α
hr0 : 0 ≤ r
hr1 : r < 1
h : ∀ (m : ℕ), n ≤ m → abv (f m.succ) ≤ r * abv (f m)
⊢ |r| < 1

Tactic:
have har1 : |r| < 1 := by rwa [abs_of_nonneg hr0]
-- Module: Mathlib.Algebra.Order.CauSeq.BigOperators
Goal:
α : Type u_1
β : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Ring β
abv : β → α
inst_4 : IsAbsoluteValue abv
inst_5 : Archimedean α
f : ℕ → β
n : ℕ
r : α
hr0 : 0 ≤ r
hr1 : r < 1
h : ∀ (m : ℕ), n ≤ m → abv (f m.succ) ≤ r * abv (f m)
har1 : |r| < 1
⊢ IsCauSeq abv fun (m : ℕ) ↦ ∑ n ∈ range m, f n

Tactic:
(geo_series_const (abv (f n.succ) * r⁻¹ ^ n.succ) har1).of_abv_le n.succ fun m hmn ↦ ?_

Premises used: HMul.hMul, IsCauSeq.of_abv_le, Inv.inv, HPow.hPow, IsCauSeq.geo_series_const, Nat.succ
-- Module: Mathlib.Algebra.Order.CauSeq.BigOperators
Goal:
α : Type u_1
β : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Ring β
abv : β → α
inst_4 : IsAbsoluteValue abv
inst_5 : Archimedean α
f : ℕ → β
n : ℕ
r : α
hr0 : 0 ≤ r
hr1 : r < 1
h : ∀ (m : ℕ), n ≤ m → abv (f m.succ) ≤ r * abv (f m)
har1 : |r| < 1
refine : ∀ (m : ℕ) (hmn : n.succ ≤ m), abv (f m) ≤ abv (f n.succ) * r⁻¹ ^ n.succ * r ^ m
⊢ IsCauSeq abv fun (m : ℕ) ↦ ∑ n ∈ range m, f n

Tactic:
refine (geo_series_const (abv (f n.succ) * r⁻¹ ^ n.succ) har1).of_abv_le n.succ fun m hmn ↦ ?_

Premises used: HMul.hMul, IsCauSeq.of_abv_le, Inv.inv, HPow.hPow, IsCauSeq.geo_series_const, Nat.succ
-- Module: Mathlib.Algebra.Order.CauSeq.BigOperators
Goal:
α : Type u_1
β : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Ring β
abv : β → α
inst_4 : IsAbsoluteValue abv
inst_5 : Archimedean α
f : ℕ → β
n : ℕ
r : α
hr0 : 0 ≤ r
hr1 : r < 1
h : ∀ (m : ℕ), n ≤ m → abv (f m.succ) ≤ r * abv (f m)
har1 : |r| < 1
m : ℕ
hmn : n.succ ≤ m
inl :
  ∀ (hr0 : LE.le.{u_1} (α := α) 0 0) (hr1 : LT.lt.{u_1} (α := α) 0 1)
    (h : ∀ (m : ℕ), n ≤ m → abv (f m.succ) ≤ 0 * abv (f m)) (har1 : LT.lt.{u_1} (α := α) |0| 1),
    abv (f m) ≤ abv (f n.succ) * HPow.hPow (α := α) 0⁻¹ n.succ * HPow.hPow (α := α) 0 m
inr : ∀ (hr : 0 < r), abv (f m) ≤ abv (f n.succ) * r⁻¹ ^ n.succ * r ^ m
⊢ abv (f m) ≤ abv (f n.succ) * r⁻¹ ^ n.succ * r ^ m

Tactic:
obtain rfl | hr := hr0.eq_or_lt

Premises used: LE.le.eq_or_lt, rfl
-- Module: Mathlib.Algebra.Order.CauSeq.BigOperators
Goal:
α : Type u_1
β : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Ring β
abv : β → α
inst_4 : IsAbsoluteValue abv
inst_5 : Archimedean α
f : ℕ → β
n m : ℕ
hmn : n.succ ≤ m
hr0 : LE.le.{u_1} (α := α) 0 0
hr1 : LT.lt.{u_1} (α := α) 0 1
h : ∀ (m : ℕ), n ≤ m → abv (f m.succ) ≤ 0 * abv (f m)
har1 : LT.lt.{u_1} (α := α) |0| 1
⊢ 0 < m

Tactic:
have m_pos := lt_of_lt_of_le (Nat.succ_pos n) hmn
-- Module: Mathlib.Algebra.Order.CauSeq.BigOperators
Goal:
α : Type u_1
β : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Ring β
abv : β → α
inst_4 : IsAbsoluteValue abv
inst_5 : Archimedean α
f : ℕ → β
n m : ℕ
hmn : n.succ ≤ m
hr0 : LE.le.{u_1} (α := α) 0 0
hr1 : LT.lt.{u_1} (α := α) 0 1
h : ∀ (m : ℕ), n ≤ m → abv (f m.succ) ≤ 0 * abv (f m)
har1 : LT.lt.{u_1} (α := α) |0| 1
m_pos : 0 < m
rwa rwa₁ rwa₂ rwa₃ : n.succ ≤ m
⊢ n.succ ≤ m.pred.succ

Tactic:
rwa [Nat.succ_pred_eq_of_pos m_pos]

Premises used: Nat.succ_pred_eq_of_pos
-- Module: Mathlib.Algebra.Order.CauSeq.BigOperators
Goal:
α : Type u_1
β : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Ring β
abv : β → α
inst_4 : IsAbsoluteValue abv
inst_5 : Archimedean α
f : ℕ → β
n m : ℕ
hmn : n.succ ≤ m
hr0 : LE.le.{u_1} (α := α) 0 0
hr1 : LT.lt.{u_1} (α := α) 0 1
h : ∀ (m : ℕ), n ≤ m → abv (f m.succ) ≤ 0 * abv (f m)
har1 : LT.lt.{u_1} (α := α) |0| 1
m_pos : 0 < m
⊢ abv (f m.pred.succ) ≤ 0 * abv (f m.pred)

Tactic:
have := h m.pred (Nat.le_of_succ_le_succ (by rwa [Nat.succ_pred_eq_of_pos m_pos]))
-- Module: Mathlib.Algebra.Order.CauSeq.BigOperators
Goal:
α : Type u_1
β : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Ring β
abv : β → α
inst_4 : IsAbsoluteValue abv
inst_5 : Archimedean α
f : ℕ → β
n m : ℕ
hmn : n.succ ≤ m
hr0 : LE.le.{u_1} (α := α) 0 0
hr1 : LT.lt.{u_1} (α := α) 0 1
h : ∀ (m : ℕ), n ≤ m → abv (f m.succ) ≤ 0 * abv (f m)
har1 : LT.lt.{u_1} (α := α) |0| 1
m_pos : 0 < m
this : abv (f m.pred.succ) ≤ 0 * abv (f m.pred)
⊢ abv (f m) ≤ abv (f n.succ) * HPow.hPow (α := α) 0⁻¹ n.succ * HPow.hPow (α := α) 0 m

Tactic:
simpa [Nat.sub_add_cancel m_pos, pow_succ] using this

Premises used: pow_succ, Nat.sub_add_cancel
-- Module: Mathlib.Algebra.Order.CauSeq.BigOperators
Goal:
α : Type u_1
β : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Ring β
abv : β → α
inst_4 : IsAbsoluteValue abv
inst_5 : Archimedean α
f : ℕ → β
n : ℕ
r : α
hr0 : 0 ≤ r
hr1 : r < 1
h : ∀ (m : ℕ), n ≤ m → abv (f m.succ) ≤ r * abv (f m)
har1 : |r| < 1
m : ℕ
hmn : n.succ ≤ m
hr : 0 < r
inr : ∀ (k : ℕ) (hk : m - n.succ = k), abv (f m) ≤ abv (f n.succ) * r⁻¹ ^ n.succ * r ^ m
⊢ abv (f m) ≤ abv (f n.succ) * r⁻¹ ^ n.succ * r ^ m

Tactic:
generalize hk : m - n.succ = k

Premises used: Nat.succ
-- Module: Mathlib.Algebra.Order.CauSeq.BigOperators
Goal:
α : Type u_1
β : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Ring β
abv : β → α
inst_4 : IsAbsoluteValue abv
inst_5 : Archimedean α
f : ℕ → β
n : ℕ
r : α
hr0 : 0 ≤ r
hr1 : r < 1
h : ∀ (m : ℕ), n ≤ m → abv (f m.succ) ≤ r * abv (f m)
har1 : |r| < 1
m : ℕ
hmn : n.succ ≤ m
hr : 0 < r
k : ℕ
hk : m - n.succ = k
⊢ m = k + n.succ

Tactic:
replace hk : m = k + n.succ := (tsub_eq_iff_eq_add_of_le hmn).1 hk
-- Module: Mathlib.Algebra.Order.CauSeq.BigOperators
Goal:
α : Type u_1
β : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Ring β
abv : β → α
inst_4 : IsAbsoluteValue abv
inst_5 : Archimedean α
f : ℕ → β
r : α
hr0 : 0 ≤ r
hr1 : r < 1
har1 : |r| < 1
hr : 0 < r
n : ℕ
h : ∀ (m : ℕ), n ≤ m → abv (f m.succ) ≤ r * abv (f m)
m : ℕ
hmn : n.succ ≤ m
hk : m = 0 + n.succ
inr : r ^ n.succ ≠ 0
⊢ abv (f m) ≤ abv (f n.succ) * r⁻¹ ^ n.succ * r ^ m

Tactic:
rw [hk, Nat.zero_add, mul_right_comm, inv_pow _ _, ← div_eq_mul_inv, mul_div_cancel_right₀]

Premises used: inv_pow, div_eq_mul_inv, mul_div_cancel_right₀, mul_right_comm, Nat.zero_add
-- Module: Mathlib.Algebra.Order.CauSeq.BigOperators
Goal:
α : Type u_1
β : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Ring β
abv : β → α
inst_4 : IsAbsoluteValue abv
inst_5 : Archimedean α
f : ℕ → β
r : α
hr0 : 0 ≤ r
hr1 : r < 1
har1 : |r| < 1
hr : 0 < r
n : ℕ
h : ∀ (m : ℕ), n ≤ m → abv (f m.succ) ≤ r * abv (f m)
m : ℕ
hmn : n.succ ≤ m
hk : m = 0 + n.succ
⊢ r ^ n.succ ≠ 0

Tactic:
positivity
-- Module: Mathlib.Algebra.Order.CauSeq.BigOperators
Goal:
α : Type u_1
β : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Ring β
abv : β → α
inst_4 : IsAbsoluteValue abv
inst_5 : Archimedean α
f : ℕ → β
r : α
hr0 : 0 ≤ r
hr1 : r < 1
har1 : |r| < 1
hr : 0 < r
k : ℕ
ih :
  ∀ (n : ℕ) (h : ∀ (m : ℕ), n ≤ m → abv (f m.succ) ≤ r * abv (f m)) (m : ℕ) (hmn : n.succ ≤ m) (hk : m = k + n.succ),
    abv (f m) ≤ abv (f n.succ) * r⁻¹ ^ n.succ * r ^ m
n : ℕ
h : ∀ (m : ℕ), n ≤ m → abv (f m.succ) ≤ r * abv (f m)
m : ℕ
hmn : n.succ ≤ m
hk : m = k + 1 + n.succ
rw : k + (0 + n.succ) ≥ 0 + n.succ
⊢ k + n.succ ≥ n.succ

Tactic:
rw [← zero_add n.succ]

Premises used: zero_add, Nat.succ
-- Module: Mathlib.Algebra.Order.CauSeq.BigOperators
Goal:
α : Type u_1
β : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Ring β
abv : β → α
inst_4 : IsAbsoluteValue abv
inst_5 : Archimedean α
f : ℕ → β
r : α
hr0 : 0 ≤ r
hr1 : r < 1
har1 : |r| < 1
hr : 0 < r
k : ℕ
ih :
  ∀ (n : ℕ) (h : ∀ (m : ℕ), n ≤ m → abv (f m.succ) ≤ r * abv (f m)) (m : ℕ) (hmn : n.succ ≤ m) (hk : m = k + n.succ),
    abv (f m) ≤ abv (f n.succ) * r⁻¹ ^ n.succ * r ^ m
n : ℕ
h : ∀ (m : ℕ), n ≤ m → abv (f m.succ) ≤ r * abv (f m)
m : ℕ
hmn : n.succ ≤ m
hk : m = k + 1 + n.succ
⊢ n.succ ≤ 0 + n.succ

Tactic:
simp
-- Module: Mathlib.Algebra.Order.CauSeq.BigOperators
Goal:
α : Type u_1
β : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Ring β
abv : β → α
inst_4 : IsAbsoluteValue abv
inst_5 : Archimedean α
f : ℕ → β
r : α
hr0 : 0 ≤ r
hr1 : r < 1
har1 : |r| < 1
hr : 0 < r
k : ℕ
ih :
  ∀ (n : ℕ) (h : ∀ (m : ℕ), n ≤ m → abv (f m.succ) ≤ r * abv (f m)) (m : ℕ) (hmn : n.succ ≤ m) (hk : m = k + n.succ),
    abv (f m) ≤ abv (f n.succ) * r⁻¹ ^ n.succ * r ^ m
n : ℕ
h : ∀ (m : ℕ), n ≤ m → abv (f m.succ) ≤ r * abv (f m)
m : ℕ
hmn : n.succ ≤ m
hk : m = k + 1 + n.succ
⊢ k + (0 + n.succ) ≥ 0 + n.succ

Tactic:
exact add_le_add (Nat.zero_le _) (by simp)

Premises used: Nat.zero_le, add_le_add
-- Module: Mathlib.Algebra.Order.CauSeq.BigOperators
Goal:
α : Type u_1
β : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Ring β
abv : β → α
inst_4 : IsAbsoluteValue abv
inst_5 : Archimedean α
f : ℕ → β
r : α
hr0 : 0 ≤ r
hr1 : r < 1
har1 : |r| < 1
hr : 0 < r
k : ℕ
ih :
  ∀ (n : ℕ) (h : ∀ (m : ℕ), n ≤ m → abv (f m.succ) ≤ r * abv (f m)) (m : ℕ) (hmn : n.succ ≤ m) (hk : m = k + n.succ),
    abv (f m) ≤ abv (f n.succ) * r⁻¹ ^ n.succ * r ^ m
n : ℕ
h : ∀ (m : ℕ), n ≤ m → abv (f m.succ) ≤ r * abv (f m)
m : ℕ
hmn : n.succ ≤ m
hk : m = k + 1 + n.succ
⊢ k + n.succ ≥ n.succ

Tactic:
have kn : k + n.succ ≥ n.succ := by
      rw [← zero_add n.succ]; exact add_le_add (Nat.zero_le _) (by simp)
-- Module: Mathlib.Algebra.Order.CauSeq.BigOperators
Goal:
α : Type u_1
β : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Ring β
abv : β → α
inst_4 : IsAbsoluteValue abv
inst_5 : Archimedean α
f : ℕ → β
r : α
hr0 : 0 ≤ r
hr1 : r < 1
har1 : |r| < 1
hr : 0 < r
k : ℕ
ih :
  ∀ (n : ℕ) (h : ∀ (m : ℕ), n ≤ m → abv (f m.succ) ≤ r * abv (f m)) (m : ℕ) (hmn : n.succ ≤ m) (hk : m = k + n.succ),
    abv (f m) ≤ abv (f n.succ) * r⁻¹ ^ n.succ * r ^ m
n : ℕ
h : ∀ (m : ℕ), n ≤ m → abv (f m.succ) ≤ r * abv (f m)
m : ℕ
hmn : n.succ ≤ m
hk : m = k + 1 + n.succ
kn : k + n.succ ≥ n.succ
inr : abv (f (k + n.succ).succ) ≤ abv (f n.succ) * r⁻¹ ^ n.succ * r ^ (k + n.succ) * r
⊢ abv (f m) ≤ abv (f n.succ) * r⁻¹ ^ n.succ * r ^ m

Tactic:
rw [hk, Nat.succ_add, pow_succ r, ← mul_assoc]

Premises used: pow_succ, mul_assoc, Nat.succ_add
-- Module: Mathlib.Algebra.Order.CauSeq.BigOperators
Goal:
α : Type u_1
β : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Ring β
abv : β → α
inst_4 : IsAbsoluteValue abv
inst_5 : Archimedean α
f : ℕ → β
r : α
hr0 : 0 ≤ r
hr1 : r < 1
har1 : |r| < 1
hr : 0 < r
k : ℕ
ih :
  ∀ (n : ℕ) (h : ∀ (m : ℕ), n ≤ m → abv (f m.succ) ≤ r * abv (f m)) (m : ℕ) (hmn : n.succ ≤ m) (hk : m = k + n.succ),
    abv (f m) ≤ abv (f n.succ) * r⁻¹ ^ n.succ * r ^ m
n : ℕ
h : ∀ (m : ℕ), n ≤ m → abv (f m.succ) ≤ r * abv (f m)
m : ℕ
hmn : n.succ ≤ m
hk : m = k + 1 + n.succ
kn : k + n.succ ≥ n.succ
rw : abv (f (k + n.succ).succ) ≤ r * abv (f (k + n.succ))
a : α
⊢ abv (f (k + n.succ).succ) ≤ abv (f (k + n.succ)) * r

Tactic:
rw [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.Algebra.Order.CauSeq.BigOperators
Goal:
α : Type u_1
β : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Ring β
abv : β → α
inst_4 : IsAbsoluteValue abv
inst_5 : Archimedean α
f : ℕ → β
r : α
hr0 : 0 ≤ r
hr1 : r < 1
har1 : |r| < 1
hr : 0 < r
k : ℕ
ih :
  ∀ (n : ℕ) (h : ∀ (m : ℕ), n ≤ m → abv (f m.succ) ≤ r * abv (f m)) (m : ℕ) (hmn : n.succ ≤ m) (hk : m = k + n.succ),
    abv (f m) ≤ abv (f n.succ) * r⁻¹ ^ n.succ * r ^ m
n : ℕ
h : ∀ (m : ℕ), n ≤ m → abv (f m.succ) ≤ r * abv (f m)
m : ℕ
hmn : n.succ ≤ m
hk : m = k + 1 + n.succ
kn : k + n.succ ≥ n.succ
⊢ abv (f (k + n.succ).succ) ≤ r * abv (f (k + n.succ))

Tactic:
h _ (Nat.le_of_succ_le kn)

Premises used: Nat.le_of_succ_le
-- Module: Mathlib.Algebra.Order.CauSeq.BigOperators
Goal:
α : Type u_1
β : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Ring β
abv : β → α
inst_4 : IsAbsoluteValue abv
inst_5 : Archimedean α
f : ℕ → β
r : α
hr0 : 0 ≤ r
hr1 : r < 1
har1 : |r| < 1
hr : 0 < r
k : ℕ
ih :
  ∀ (n : ℕ) (h : ∀ (m : ℕ), n ≤ m → abv (f m.succ) ≤ r * abv (f m)) (m : ℕ) (hmn : n.succ ≤ m) (hk : m = k + n.succ),
    abv (f m) ≤ abv (f n.succ) * r⁻¹ ^ n.succ * r ^ m
n : ℕ
h : ∀ (m : ℕ), n ≤ m → abv (f m.succ) ≤ r * abv (f m)
m : ℕ
hmn : n.succ ≤ m
hk : m = k + 1 + n.succ
kn : k + n.succ ≥ n.succ
⊢ abv (f (k + n.succ).succ) ≤ r * abv (f (k + n.succ))

Tactic:
exact h _ (Nat.le_of_succ_le kn)

Premises used: Nat.le_of_succ_le
-- Module: Mathlib.Algebra.Order.CauSeq.BigOperators
Goal:
α : Type u_1
β : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Ring β
abv : β → α
inst_4 : IsAbsoluteValue abv
inst_5 : Archimedean α
f : ℕ → β
r : α
hr0 : 0 ≤ r
hr1 : r < 1
har1 : |r| < 1
hr : 0 < r
k : ℕ
ih :
  ∀ (n : ℕ) (h : ∀ (m : ℕ), n ≤ m → abv (f m.succ) ≤ r * abv (f m)) (m : ℕ) (hmn : n.succ ≤ m) (hk : m = k + n.succ),
    abv (f m) ≤ abv (f n.succ) * r⁻¹ ^ n.succ * r ^ m
n : ℕ
h : ∀ (m : ℕ), n ≤ m → abv (f m.succ) ≤ r * abv (f m)
m : ℕ
hmn : n.succ ≤ m
hk : m = k + 1 + n.succ
kn : k + n.succ ≥ n.succ
inr : abv (f (k + n.succ)) ≤ abv (f n.succ) * r⁻¹ ^ n.succ * r ^ (k + n.succ)
⊢ abv (f (k + n.succ).succ) ≤ abv (f n.succ) * r⁻¹ ^ n.succ * r ^ (k + n.succ) * r

Tactic:
refine
      le_trans (by rw [mul_comm] <;> exact h _ (Nat.le_of_succ_le kn))
        (mul_le_mul_of_nonneg_right ?_ hr0)

Premises used: mul_le_mul_of_nonneg_right, le_trans
-- Module: Mathlib.Algebra.Order.CauSeq.BigOperators
Goal:
α : Type u_1
β : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Ring β
abv : β → α
inst_4 : IsAbsoluteValue abv
inst_5 : Archimedean α
f : ℕ → β
r : α
hr0 : 0 ≤ r
hr1 : r < 1
har1 : |r| < 1
hr : 0 < r
k : ℕ
ih :
  ∀ (n : ℕ) (h : ∀ (m : ℕ), n ≤ m → abv (f m.succ) ≤ r * abv (f m)) (m : ℕ) (hmn : n.succ ≤ m) (hk : m = k + n.succ),
    abv (f m) ≤ abv (f n.succ) * r⁻¹ ^ n.succ * r ^ m
n : ℕ
h : ∀ (m : ℕ), n ≤ m → abv (f m.succ) ≤ r * abv (f m)
m : ℕ
hmn : n.succ ≤ m
hk : m = k + 1 + n.succ
kn : k + n.succ ≥ n.succ
⊢ n.succ ≤ k + n.succ

Tactic:
simp
-- Module: Mathlib.Algebra.Order.CauSeq.BigOperators
Goal:
α : Type u_1
β : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Ring β
abv : β → α
inst_4 : IsAbsoluteValue abv
inst_5 : Archimedean α
f : ℕ → β
r : α
hr0 : 0 ≤ r
hr1 : r < 1
har1 : |r| < 1
hr : 0 < r
k : ℕ
ih :
  ∀ (n : ℕ) (h : ∀ (m : ℕ), n ≤ m → abv (f m.succ) ≤ r * abv (f m)) (m : ℕ) (hmn : n.succ ≤ m) (hk : m = k + n.succ),
    abv (f m) ≤ abv (f n.succ) * r⁻¹ ^ n.succ * r ^ m
n : ℕ
h : ∀ (m : ℕ), n ≤ m → abv (f m.succ) ≤ r * abv (f m)
m : ℕ
hmn : n.succ ≤ m
hk : m = k + 1 + n.succ
kn : k + n.succ ≥ n.succ
⊢ abv (f (k + n.succ)) ≤ abv (f n.succ) * r⁻¹ ^ n.succ * r ^ (k + n.succ)

Tactic:
exact ih _ h _ (by simp) rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.CauSeq.BigOperators
Goal:
α : Type u_1
β : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Ring β
abv : β → α
inst_4 : IsAbsoluteValue abv
inst_5 : Archimedean α
f : ℕ → β
n : ℕ
r : α
hr0 : 0 ≤ r
hr1 : r < 1
h : ∀ (m : ℕ), n ≤ m → abv (f m.succ) ≤ r * abv (f m)
har1 : |r| < 1
m : ℕ
hmn : n.succ ≤ m
hr : 0 < r
k : ℕ
hk : m = k + n.succ
inr :
  ∀ (n : ℕ) (h : ∀ (m : ℕ), n ≤ m → abv (f m.succ) ≤ r * abv (f m)) (m : ℕ) (hmn : n.succ ≤ m) (hk : m = 0 + n.succ),
    abv (f m) ≤ abv (f n.succ) * r⁻¹ ^ n.succ * r ^ m
inr₁ :
  ∀ (k : ℕ)
    (ih :
      ∀ (n : ℕ) (h : ∀ (m : ℕ), n ≤ m → abv (f m.succ) ≤ r * abv (f m)) (m : ℕ) (hmn : n.succ ≤ m)
        (hk : m = k + n.succ), abv (f m) ≤ abv (f n.succ) * r⁻¹ ^ n.succ * r ^ m)
    (n : ℕ) (h : ∀ (m : ℕ), n ≤ m → abv (f m.succ) ≤ r * abv (f m)) (m : ℕ) (hmn : n.succ ≤ m)
    (hk : m = k + 1 + n.succ), abv (f m) ≤ abv (f n.succ) * r⁻¹ ^ n.succ * r ^ m
⊢ abv (f m) ≤ abv (f n.succ) * r⁻¹ ^ n.succ * r ^ m

Tactic:
induction k generalizing m n with
  | zero =>
    rw [hk, Nat.zero_add, mul_right_comm, inv_pow _ _, ← div_eq_mul_inv, mul_div_cancel_right₀]
    positivity
  | succ k ih =>
    have kn : k + n.succ ≥ n.succ := by
      rw [← zero_add n.succ]; exact add_le_add (Nat.zero_le _) (by simp)
    rw [hk, Nat.succ_add, pow_succ r, ← mul_assoc]
    refine
      le_trans (by rw [mul_comm] <;> exact h _ (Nat.le_of_succ_le kn))
        (mul_le_mul_of_nonneg_right ?_ hr0)
    exact ih _ h _ (by simp) rfl

Premises used: pow_succ, mul_assoc, inv_pow, div_eq_mul_inv, mul_div_cancel_right₀, mul_le_mul_of_nonneg_right, mul_right_comm, Nat.zero_add, Nat.succ_add, le_trans
-- Module: Mathlib.Algebra.Order.CauSeq.Completion
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
β : Type u_2
inst_3 : Ring β
abv : β → α
inst_4 : IsAbsoluteValue abv
f : CauSeq β abv
⊢ Eq (α := Cauchy abv) ⟦f⟧ (mk f)

Tactic:
rfl

Premises used: CauSeq.Completion.mk, rfl
-- Module: Mathlib.Algebra.Order.CauSeq.Completion
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
β : Type u_2
inst_3 : Ring β
abv : β → α
inst_4 : IsAbsoluteValue abv
f g : CauSeq β abv
⊢ Eq (α := Cauchy abv) (mk f) (mk g) ↔ (f - g).LimZero

Tactic:
Quotient.eq

Premises used: CauSeq.Completion.Cauchy, CauSeq.Completion.mk, Quotient.eq
-- Module: Mathlib.Algebra.Order.CauSeq.Completion
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
β : Type u_2
inst_3 : Ring β
abv : β → α
inst_4 : IsAbsoluteValue abv
⊢ Eq.{u_2 + 1} (α := Cauchy abv) (ofRat 0) 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.CauSeq.Completion
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
β : Type u_2
inst_3 : Ring β
abv : β → α
inst_4 : IsAbsoluteValue abv
⊢ Eq.{u_2 + 1} (α := Cauchy abv) (ofRat 1) 1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.CauSeq.Completion
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
β : Type u_2
inst_3 : Ring β
abv : β → α
inst_4 : IsAbsoluteValue abv
f : CauSeq β abv
⊢ Eq (α := Cauchy abv) (mk f) 0 ↔ (f - 0).LimZero

Tactic:
have : mk f = 0 ↔ LimZero (f - 0) := Quotient.eq