awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.BigOperators (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Archimedean α
f : ℕ → α
a : α
m : ℕ
ham : ∀ n ≥ m, |f n| ≤ a
hnm : ∀ n ≥ m, f n.succ ≤ f n
ε : α
ε0 : ε > 0
let let₁ let₂ : ∀ (k : ℕ) (hk : a ≤ k • ε), ∃ (i : ℕ), ∀ j ≥ i, |f j - f i| < ε
let₃ let₄ : ∀ (k : ℕ) (hk : a ≤ k • ε) (h : ∃ (l : ℕ), ∀ n ≥ m, a - l • ε < f n), ∃ (i : ℕ), ∀ j ≥ i, |f j - f i| < ε
let₅ :
  ∀ (k : ℕ) (hk : a ≤ k • ε) (h : ∃ (l : ℕ), ∀ n ≥ m, a - l • ε < f n),
    let l := Nat.find (p := fun (n : ℕ) ↦ ∀ n_1 ≥ m, a - n • ε < f n_1) h;
    ∀ (hl : ∀ n ≥ m, f n > a - l • ε), ∃ (i : ℕ), ∀ j ≥ i, |f j - f i| < ε
let₆ :
  ∀ (k : ℕ) (hk : a ≤ k • ε) (h : ∃ (l : ℕ), ∀ n ≥ m, a - l • ε < f n),
    let l := Nat.find (p := fun (n : ℕ) ↦ ∀ n_1 ≥ m, a - n • ε < f n_1) h;
    ∀ (hl : ∀ n ≥ m, f n > a - l • ε) (hl0 : l ≠ 0), ∃ (i : ℕ), ∀ j ≥ i, |f j - f i| < ε
⊢ ∃ (i : ℕ), ∀ j ≥ i, |f j - f i| < ε
have let₇ : ∀ (k : ℕ) (hk : a ≤ k • ε) (h : ∃ (l : ℕ), ∀ n ≥ m, a - l • ε < f n),
  let l := Nat.find (p := fun (n : ℕ) ↦ ∀ n_1 ≥ m, a - n • ε < f n_1) h;
  ∀ (hl : ∀ n ≥ m, f n > a - l • ε) (hl0 : l ≠ 0) (i : ℕ)
    (hi : ¬(i ≥ m → a - (Nat.find (p := fun (n : ℕ) ↦ ∀ n_1 ≥ m, a - n • ε < f n_1) h).pred • ε < f i)),
    ∃ (i : ℕ), ∀ j ≥ i, |f j - f i| < ε
Tactic: classical
  let ⟨k, hk⟩ := Archimedean.arch a ε0
  have h : ∃ l, ∀ n ≥ m, a - l • ε < f n :=
    ⟨k + k + 1, fun n hnm ↦
      lt_of_lt_of_le (show a - (k + (k + 1)) • ε < -|f n| from
          lt_neg.1 <| (ham n hnm).trans_lt
              (by
                rw [neg_sub, lt_sub_iff_add_lt, add_nsmul, add_nsmul, one_nsmul]
                exact add_lt_add_of_le_of_lt hk (lt_of_le_of_lt hk (lt_add_of_pos_right _ ε0))))
        (neg_le.2 <| abs_neg (f n) ▸ le_abs_self _)⟩
  let l := Nat.find h
  have hl : ∀ n : ℕ, n ≥ m → f n > a - l • ε := Nat.find_spec h
  have hl0 : l ≠ 0 := fun hl0 ↦
    not_lt_of_ge (ham m le_rfl)
      (lt_of_lt_of_le (by have := hl m (le_refl m); simpa [hl0] using this) (le_abs_self (f m)))
  obtain ⟨i, hi⟩ := not_forall.1 (Nat.find_min h (Nat.pred_lt hl0))
  rw [Classical.not_imp, not_lt] at hi
  exists i
  intro j hj
  have hfij : f j ≤ f i := (Nat.rel_of_forall_rel_succ_of_le_of_le (· ≥ ·) hnm hi.1 hj).le
  rw [abs_of_nonpos (sub_nonpos.2 hfij), neg_sub, sub_lt_iff_lt_add']
  calc
    f i ≤ a - Nat.pred l • ε := hi.2
    _ = a - l • ε + ε := by
      conv =>
        rhs
        rw [← Nat.succ_pred_eq_of_pos (Nat.pos_of_ne_zero hl0), succ_nsmul, sub_add,
          add_sub_cancel_right]
    _ < f j + ε := by gcongr; exact hl _ <| hi.1.trans hj
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.BigOperators (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Archimedean α
f : ℕ → α
a : α
m : ℕ
ham : ∀ n ≥ m, |f n| ≤ a
hnm : ∀ n ≥ m, f n.succ ≤ f n
ε : α
ε0 : ε > 0
let let₁ let₂ : ∀ (k : ℕ) (hk : a ≤ k • ε), ∃ (i : ℕ), ∀ j ≥ i, |f j - f i| < ε
let₃ let₄ : ∀ (k : ℕ) (hk : a ≤ k • ε) (h : ∃ (l : ℕ), ∀ n ≥ m, a - l • ε < f n), ∃ (i : ℕ), ∀ j ≥ i, |f j - f i| < ε
let₅ :
  ∀ (k : ℕ) (hk : a ≤ k • ε) (h : ∃ (l : ℕ), ∀ n ≥ m, a - l • ε < f n),
    let l := Nat.find (p := fun (n : ℕ) ↦ ∀ n_1 ≥ m, a - n • ε < f n_1) h;
    ∀ (hl : ∀ n ≥ m, f n > a - l • ε), ∃ (i : ℕ), ∀ j ≥ i, |f j - f i| < ε
let₆ :
  ∀ (k : ℕ) (hk : a ≤ k • ε) (h : ∃ (l : ℕ), ∀ n ≥ m, a - l • ε < f n),
    let l := Nat.find (p := fun (n : ℕ) ↦ ∀ n_1 ≥ m, a - n • ε < f n_1) h;
    ∀ (hl : ∀ n ≥ m, f n > a - l • ε) (hl0 : l ≠ 0), ∃ (i : ℕ), ∀ j ≥ i, |f j - f i| < ε
let₇ :
  ∀ (k : ℕ) (hk : a ≤ k • ε) (h : ∃ (l : ℕ), ∀ n ≥ m, a - l • ε < f n),
    let l := Nat.find (p := fun (n : ℕ) ↦ ∀ n_1 ≥ m, a - n • ε < f n_1) h;
    ∀ (hl : ∀ n ≥ m, f n > a - l • ε) (hl0 : l ≠ 0) (i : ℕ)
      (hi : ¬(i ≥ m → a - (Nat.find (p := fun (n : ℕ) ↦ ∀ n_1 ≥ m, a - n • ε < f n_1) h).pred • ε < f i)),
      ∃ (i : ℕ), ∀ j ≥ i, |f j - f i| < ε
⊢ ∃ (i : ℕ), ∀ j ≥ i, |f j - f i| < ε
have let₈ : ∀ (k : ℕ) (hk : a ≤ k • ε) (h : ∃ (l : ℕ), ∀ n ≥ m, a - l • ε < f n),
  let l := Nat.find (p := fun (n : ℕ) ↦ ∀ n_1 ≥ m, a - n • ε < f n_1) h;
  ∀ (hl : ∀ n ≥ m, f n > a - l • ε) (hl0 : l ≠ 0) (i : ℕ)
    (hi : i ≥ m ∧ f i ≤ a - (Nat.find (p := fun (n : ℕ) ↦ ∀ n_1 ≥ m, a - n • ε < f n_1) h).pred • ε),
    ∃ (i : ℕ), ∀ j ≥ i, |f j - f i| < ε
Tactic: classical
  let ⟨k, hk⟩ := Archimedean.arch a ε0
  have h : ∃ l, ∀ n ≥ m, a - l • ε < f n :=
    ⟨k + k + 1, fun n hnm ↦
      lt_of_lt_of_le (show a - (k + (k + 1)) • ε < -|f n| from
          lt_neg.1 <| (ham n hnm).trans_lt
              (by
                rw [neg_sub, lt_sub_iff_add_lt, add_nsmul, add_nsmul, one_nsmul]
                exact add_lt_add_of_le_of_lt hk (lt_of_le_of_lt hk (lt_add_of_pos_right _ ε0))))
        (neg_le.2 <| abs_neg (f n) ▸ le_abs_self _)⟩
  let l := Nat.find h
  have hl : ∀ n : ℕ, n ≥ m → f n > a - l • ε := Nat.find_spec h
  have hl0 : l ≠ 0 := fun hl0 ↦
    not_lt_of_ge (ham m le_rfl)
      (lt_of_lt_of_le (by have := hl m (le_refl m); simpa [hl0] using this) (le_abs_self (f m)))
  obtain ⟨i, hi⟩ := not_forall.1 (Nat.find_min h (Nat.pred_lt hl0))
  rw [Classical.not_imp, not_lt] at hi
  exists i
  intro j hj
  have hfij : f j ≤ f i := (Nat.rel_of_forall_rel_succ_of_le_of_le (· ≥ ·) hnm hi.1 hj).le
  rw [abs_of_nonpos (sub_nonpos.2 hfij), neg_sub, sub_lt_iff_lt_add']
  calc
    f i ≤ a - Nat.pred l • ε := hi.2
    _ = a - l • ε + ε := by
      conv =>
        rhs
        rw [← Nat.succ_pred_eq_of_pos (Nat.pos_of_ne_zero hl0), succ_nsmul, sub_add,
          add_sub_cancel_right]
    _ < f j + ε := by gcongr; exact hl _ <| hi.1.trans hj
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.BigOperators (hypothesis)
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
⊢ IsCauSeq abv fun (n : ℕ) ↦ ∑ m ∈ range n, x ^ m
have hx1' : abv x ≠ 1
Tactic: have hx1' : abv x ≠ 1 := fun h ↦ by simp [h] at hx1
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.BigOperators (goal)
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
⊢ IsCauSeq abv fun (n : ℕ) ↦ ∑ m ∈ range n, x ^ m
have refine : IsCauSeq.{u_1, u_1} (α := α) abs fun (m : ℕ) ↦ ∑ n ∈ range m, abv (x ^ n)
Tactic: refine of_abv ?_
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.BigOperators (goal)
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
⊢ IsCauSeq.{u_1, u_1} (α := α) abs fun (m : ℕ) ↦ ∑ n ∈ range m, abv (x ^ n)
have simp : IsCauSeq.{u_1, u_1} (α := α) abs fun (m : ℕ) ↦ (abv x ^ m - 1) / (abv x - 1)
Tactic: simp only [abv_pow abv, geom_sum_eq hx1']
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.BigOperators (goal)
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
m : ℕ
| (abv x ^ m - 1) / (abv x - 1)
have rw : (1 - abv x ^ m) / (1 - abv x)
Tactic: rw [← neg_div_neg_eq, neg_sub, neg_sub]
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.BigOperators (goal)
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
⊢ IsCauSeq.{u_1, u_1} (α := α) abs fun (m : ℕ) ↦ (abv x ^ m - 1) / (abv x - 1)
have conv : IsCauSeq.{u_1, u_1} (α := α) abs fun (m : ℕ) ↦ (1 - abv x ^ m) / (1 - abv x)
Tactic: conv in _ / _ => rw [← neg_div_neg_eq, neg_sub, neg_sub]
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.BigOperators (hypothesis)
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
⊢ IsCauSeq.{u_1, u_1} (α := α) abs fun (m : ℕ) ↦ (1 - abv x ^ m) / (1 - abv x)
have this : 0 < 1 - abv x
Tactic: have : 0 < 1 - abv x := sub_pos.2 hx1
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.BigOperators (goal)
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
⊢ IsCauSeq.{u_1, u_1} (α := α) abs fun (m : ℕ) ↦ (1 - abv x ^ m) / (1 - abv x)
have refine_1 : ∀ n ≥ 0, |(1 - abv x ^ n) / (1 - abv x)| ≤ 1 / (1 - abv x)
Tactic: refine of_mono_bounded _ (a := (1 : α) / (1 - abv x)) (m := 0) ?_ ?_
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.BigOperators (goal)
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
refine_1 : ∀ n ≥ 0, |(1 - abv x ^ n) / (1 - abv x)| ≤ 1 / (1 - abv x)
⊢ IsCauSeq.{u_1, u_1} (α := α) abs fun (m : ℕ) ↦ (1 - abv x ^ m) / (1 - abv x)
have refine_2 : ∀ n ≥ 0, (1 - abv x ^ n) / (1 - abv x) ≤ (1 - abv x ^ n.succ) / (1 - abv x)
Tactic: refine of_mono_bounded _ (a := (1 : α) / (1 - abv x)) (m := 0) ?_ ?_
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.BigOperators (goal)
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 - abv x)| ≤ 1 / (1 - abv x)
have refine_1 : (1 - abv x ^ n) / (1 - abv x) ≤ 1 / (1 - abv x)
Tactic: rw [abs_of_nonneg]
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.BigOperators (goal)
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 - abv x) ≤ 1 / (1 - abv x)
⊢ |(1 - abv x ^ n) / (1 - abv x)| ≤ 1 / (1 - abv x)
have refine_1₁ : 0 ≤ (1 - abv x ^ n) / (1 - abv x)
Tactic: rw [abs_of_nonneg]
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.BigOperators (goal)
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 - abv x) ≤ 1 / (1 - abv x)
have refine_1 : 1 - abv x ^ n ≤ 1
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.BigOperators (goal)
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)
have refine_1 : abv x ^ n ≤ 1
Tactic: refine div_nonneg (sub_nonneg.2 ?_) (sub_nonneg.2 <| le_of_lt hx1)
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.BigOperators (goal)
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 - abv x) ≤ (1 - abv x ^ n.succ) / (1 - abv x)
have refine_2 : (1 - 1 * abv x ^ n) / (1 - abv x) ≤ (1 - abv x * abv x ^ n) / (1 - abv x)
Tactic: rw [← one_mul (abv x ^ n), pow_succ']
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.BigOperators (goal)
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 - 1 * abv x ^ n) / (1 - abv x) ≤ (1 - abv x * abv x ^ n) / (1 - abv x)
have refine_2 : 0 ≤ 1 - abv x
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.BigOperators (goal)
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
⊢ (1 - 1 * abv x ^ n) / (1 - abv x) ≤ (1 - abv x * abv x ^ n) / (1 - abv x)
have refine_2₁ : 0 ≤ abv x ^ n
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.BigOperators (hypothesis)
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)
⊢ IsCauSeq abv fun (m : ℕ) ↦ ∑ n ∈ range m, f n
have har1 : |r| < 1
Tactic: have har1 : |r| < 1 := by rwa [abs_of_nonneg hr0]
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.BigOperators (goal)
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
have refine : ∀ (m : ℕ) (hmn : n.succ ≤ m), abv (f m) ≤ abv (f n.succ) * r⁻¹ ^ n.succ * r ^ m
Tactic: refine (geo_series_const (abv (f n.succ) * r⁻¹ ^ n.succ) har1).of_abv_le n.succ fun m hmn ↦ ?_
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.BigOperators (goal)
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
⊢ abv (f m) ≤ abv (f n.succ) * r⁻¹ ^ n.succ * r ^ m
have 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
Tactic: obtain rfl | hr := hr0.eq_or_lt
Cleared hypotheses: r, hr0, hr1, h, har1
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.BigOperators (goal)
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
⊢ abv (f m) ≤ abv (f n.succ) * r⁻¹ ^ n.succ * r ^ m
have inr : ∀ (hr : 0 < r), abv (f m) ≤ abv (f n.succ) * r⁻¹ ^ n.succ * r ^ m
Tactic: obtain rfl | hr := hr0.eq_or_lt
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.BigOperators (hypothesis)
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
⊢ abv (f m) ≤ abv (f n.succ) * HPow.hPow (α := α) 0⁻¹ n.succ * HPow.hPow (α := α) 0 m
have m_pos : 0 < m
Tactic: have m_pos := lt_of_lt_of_le (Nat.succ_pos n) hmn
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.BigOperators (hypothesis)
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) ≤ abv (f n.succ) * HPow.hPow (α := α) 0⁻¹ n.succ * HPow.hPow (α := α) 0 m
have this : 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]))
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.BigOperators (goal)
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
⊢ abv (f m) ≤ abv (f n.succ) * r⁻¹ ^ n.succ * r ^ m
have inr : ∀ (k : ℕ) (hk : m - n.succ = k), abv (f m) ≤ abv (f n.succ) * r⁻¹ ^ n.succ * r ^ m
Tactic: generalize hk : m - n.succ = k
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.BigOperators (hypothesis)
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
⊢ abv (f m) ≤ abv (f n.succ) * r⁻¹ ^ n.succ * r ^ m
have hk₁ : m = k + n.succ
Tactic: replace hk : m = k + n.succ := (tsub_eq_iff_eq_add_of_le hmn).1 hk
Cleared hypotheses: hk
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.BigOperators (goal)
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
⊢ abv (f m) ≤ abv (f n.succ) * r⁻¹ ^ n.succ * r ^ m
have inr : r ^ n.succ ≠ 0
Tactic: rw [hk, Nat.zero_add, mul_right_comm, inv_pow _ _, ← div_eq_mul_inv, mul_div_cancel_right₀]
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.BigOperators (goal)
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
have rw : k + (0 + n.succ) ≥ 0 + n.succ
Tactic: rw [← zero_add n.succ]
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.BigOperators (hypothesis)
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
⊢ abv (f m) ≤ abv (f n.succ) * r⁻¹ ^ n.succ * r ^ m
have kn : 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)
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.BigOperators (goal)
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 m) ≤ abv (f n.succ) * r⁻¹ ^ n.succ * r ^ m
have inr : abv (f (k + n.succ).succ) ≤ abv (f n.succ) * r⁻¹ ^ n.succ * r ^ (k + n.succ) * r
Tactic: rw [hk, Nat.succ_add, pow_succ r, ← mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.BigOperators (goal)
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) ≤ abv (f (k + n.succ)) * r
have rw : abv (f (k + n.succ).succ) ≤ r * abv (f (k + n.succ))
Tactic: rw [mul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.BigOperators (goal)
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) ≤ abv (f n.succ) * r⁻¹ ^ n.succ * r ^ (k + n.succ) * r
have inr : abv (f (k + n.succ)) ≤ abv (f n.succ) * r⁻¹ ^ n.succ * r ^ (k + n.succ)
Tactic: refine
      le_trans (by rw [mul_comm] <;> exact h _ (Nat.le_of_succ_le kn))
        (mul_le_mul_of_nonneg_right ?_ hr0)
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.BigOperators (goal)
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
⊢ abv (f m) ≤ abv (f n.succ) * r⁻¹ ^ n.succ * r ^ m
have 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
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
Cleared hypotheses: n, h, m, hmn, k, hk