-- Mathlib/Algebra/Order/CauSeq/BigOperators.lean
lemma geo_series [Nontrivial β] (x : β) (hx1 : abv x < 1) :
    IsCauSeq abv fun n ↦ ∑ m ∈ range n, x ^ m

Proof state:
α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrderedField α
inst✝³ : Ring β
abv : β → α
inst✝² : IsAbsoluteValue abv
inst✝¹ : Archimedean α
inst✝ : Nontrivial β
x : β
hx1 : abv x < 1
⊢ IsCauSeq abv fun n => ∑ m ∈ range n, x ^ m

Tactic:
have hx1' : abv x ≠ 1 := fun h ↦ by simp [h, lt_irrefl] at hx1

Result:
α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrderedField α
inst✝³ : Ring β
abv : β → α
inst✝² : IsAbsoluteValue abv
inst✝¹ : Archimedean α
inst✝ : Nontrivial β
x : β
hx1 : abv x < 1
hx1' : abv x ≠ 1
⊢ IsCauSeq abv fun n => ∑ m ∈ range n, x ^ m

Proof state:
α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrderedField α
inst✝³ : Ring β
abv : β → α
inst✝² : IsAbsoluteValue abv
inst✝¹ : Archimedean α
inst✝ : Nontrivial β
x : β
hx1 : abv x < 1
hx1' : abv x ≠ 1
⊢ IsCauSeq abs fun m => (abv x ^ m - 1) / (abv x - 1)

Tactic:
conv in _ / _ => rw [← neg_div_neg_eq, neg_sub, neg_sub]

Result:
α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrderedField α
inst✝³ : Ring β
abv : β → α
inst✝² : IsAbsoluteValue abv
inst✝¹ : Archimedean α
inst✝ : Nontrivial β
x : β
hx1 : abv x < 1
hx1' : abv x ≠ 1
⊢ IsCauSeq abs fun m => (1 - abv x ^ m) / (1 - abv x)

Proof state:
α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrderedField α
inst✝³ : Ring β
abv : β → α
inst✝² : IsAbsoluteValue abv
inst✝¹ : Archimedean α
inst✝ : Nontrivial β
x : β
hx1 : abv x < 1
hx1' : abv x ≠ 1
this : 0 < 1 - abv x
n : ℕ
a✝ : n ≥ 0
⊢ 0 ≤ abv x

Tactic:
positivity

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrderedField α
inst✝³ : Ring β
abv : β → α
inst✝² : IsAbsoluteValue abv
inst✝¹ : Archimedean α
inst✝ : Nontrivial β
x : β
hx1 : abv x < 1
h : abv x = 1
⊢ False

Tactic:
simp [h, lt_irrefl] at hx1

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrderedField α
inst✝³ : Ring β
abv : β → α
inst✝² : IsAbsoluteValue abv
inst✝¹ : Archimedean α
inst✝ : Nontrivial β
x : β
hx1 : abv x < 1
hx1' : abv x ≠ 1
⊢ IsCauSeq abv fun n => ∑ m ∈ range n, x ^ m

Tactic:
refine of_abv ?_

Result:
α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrderedField α
inst✝³ : Ring β
abv : β → α
inst✝² : IsAbsoluteValue abv
inst✝¹ : Archimedean α
inst✝ : Nontrivial β
x : β
hx1 : abv x < 1
hx1' : abv x ≠ 1
⊢ IsCauSeq abs fun m => ∑ n ∈ range m, abv (x ^ n)

Proof state:
α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrderedField α
inst✝³ : Ring β
abv : β → α
inst✝² : IsAbsoluteValue abv
inst✝¹ : Archimedean α
inst✝ : Nontrivial β
x : β
hx1 : abv x < 1
hx1' : abv x ≠ 1
this : 0 < 1 - abv x
⊢ IsCauSeq abs fun m => (1 - abv x ^ m) / (1 - abv x)

Tactic:
refine @of_mono_bounded _ _ _ _ ((1 : α) / (1 - abv x)) 0 ?_ ?_

Result:
case refine_1
α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrderedField α
inst✝³ : Ring β
abv : β → α
inst✝² : IsAbsoluteValue abv
inst✝¹ : Archimedean α
inst✝ : Nontrivial β
x : β
hx1 : abv x < 1
hx1' : abv x ≠ 1
this : 0 < 1 - abv x
⊢ ∀ n ≥ 0, |(1 - abv x ^ n) / (1 - abv x)| ≤ 1 / (1 - abv x)

case refine_2
α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrderedField α
inst✝³ : Ring β
abv : β → α
inst✝² : IsAbsoluteValue abv
inst✝¹ : Archimedean α
inst✝ : Nontrivial β
x : β
hx1 : abv x < 1
hx1' : abv x ≠ 1
this : 0 < 1 - abv x
⊢ ∀ n ≥ 0, (1 - abv x ^ n) / (1 - abv x) ≤ (1 - abv x ^ n.succ) / (1 - abv x)

Proof state:
case refine_2
α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrderedField α
inst✝³ : Ring β
abv : β → α
inst✝² : IsAbsoluteValue abv
inst✝¹ : Archimedean α
inst✝ : Nontrivial β
x : β
hx1 : abv x < 1
hx1' : abv x ≠ 1
this : 0 < 1 - abv x
n : ℕ
a✝ : n ≥ 0
⊢ (1 - 1 * abv x ^ n) / (1 - abv x) ≤ (1 - abv x * abv x ^ n) / (1 - abv x)

Tactic:
gcongr

Result:
no goals

Proof state:
case refine_2
α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrderedField α
inst✝³ : Ring β
abv : β → α
inst✝² : IsAbsoluteValue abv
inst✝¹ : Archimedean α
inst✝ : Nontrivial β
x : β
hx1 : abv x < 1
hx1' : abv x ≠ 1
this : 0 < 1 - abv x
n : ℕ
a✝ : n ≥ 0
⊢ (1 - abv x ^ n) / (1 - abv x) ≤ (1 - abv x ^ n.succ) / (1 - abv x)

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

Result:
case refine_2
α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrderedField α
inst✝³ : Ring β
abv : β → α
inst✝² : IsAbsoluteValue abv
inst✝¹ : Archimedean α
inst✝ : Nontrivial β
x : β
hx1 : abv x < 1
hx1' : abv x ≠ 1
this : 0 < 1 - abv x
n : ℕ
a✝ : n ≥ 0
⊢ (1 - 1 * abv x ^ n) / (1 - abv x) ≤ (1 - abv x * abv x ^ n) / (1 - abv x)

Proof state:
case refine_1
α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrderedField α
inst✝³ : Ring β
abv : β → α
inst✝² : IsAbsoluteValue abv
inst✝¹ : Archimedean α
inst✝ : Nontrivial β
x : β
hx1 : abv x < 1
hx1' : abv x ≠ 1
this : 0 < 1 - abv x
n : ℕ
a✝ : n ≥ 0
⊢ |(1 - abv x ^ n) / (1 - abv x)| ≤ 1 / (1 - abv x)

Tactic:
rw [abs_of_nonneg]

Result:
case refine_1
α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrderedField α
inst✝³ : Ring β
abv : β → α
inst✝² : IsAbsoluteValue abv
inst✝¹ : Archimedean α
inst✝ : Nontrivial β
x : β
hx1 : abv x < 1
hx1' : abv x ≠ 1
this : 0 < 1 - abv x
n : ℕ
a✝ : n ≥ 0
⊢ (1 - abv x ^ n) / (1 - abv x) ≤ 1 / (1 - abv x)

case refine_1
α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrderedField α
inst✝³ : Ring β
abv : β → α
inst✝² : IsAbsoluteValue abv
inst✝¹ : Archimedean α
inst✝ : Nontrivial β
x : β
hx1 : abv x < 1
hx1' : abv x ≠ 1
this : 0 < 1 - abv x
n : ℕ
a✝ : n ≥ 0
⊢ 0 ≤ (1 - abv x ^ n) / (1 - abv x)

Proof state:
case refine_1.hab
α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrderedField α
inst✝³ : Ring β
abv : β → α
inst✝² : IsAbsoluteValue abv
inst✝¹ : Archimedean α
inst✝ : Nontrivial β
x : β
hx1 : abv x < 1
hx1' : abv x ≠ 1
this : 0 < 1 - abv x
n : ℕ
a✝ : n ≥ 0
⊢ 1 - abv x ^ n ≤ 1

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

Result:
no goals

Proof state:
case refine_1
α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrderedField α
inst✝³ : Ring β
abv : β → α
inst✝² : IsAbsoluteValue abv
inst✝¹ : Archimedean α
inst✝ : Nontrivial β
x : β
hx1 : abv x < 1
hx1' : abv x ≠ 1
this : 0 < 1 - abv x
n : ℕ
a✝ : n ≥ 0
⊢ 0 ≤ (1 - abv x ^ n) / (1 - abv x)

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

Result:
case refine_1
α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrderedField α
inst✝³ : Ring β
abv : β → α
inst✝² : IsAbsoluteValue abv
inst✝¹ : Archimedean α
inst✝ : Nontrivial β
x : β
hx1 : abv x < 1
hx1' : abv x ≠ 1
this : 0 < 1 - abv x
n : ℕ
a✝ : n ≥ 0
⊢ abv x ^ n ≤ 1

Proof state:
case refine_2
α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrderedField α
inst✝³ : Ring β
abv : β → α
inst✝² : IsAbsoluteValue abv
inst✝¹ : Archimedean α
inst✝ : Nontrivial β
x : β
hx1 : abv x < 1
hx1' : abv x ≠ 1
this : 0 < 1 - abv x
⊢ ∀ n ≥ 0, (1 - abv x ^ n) / (1 - abv x) ≤ (1 - abv x ^ n.succ) / (1 - abv x)

Tactic:
intro n _

Result:
case refine_2
α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrderedField α
inst✝³ : Ring β
abv : β → α
inst✝² : IsAbsoluteValue abv
inst✝¹ : Archimedean α
inst✝ : Nontrivial β
x : β
hx1 : abv x < 1
hx1' : abv x ≠ 1
this : 0 < 1 - abv x
n : ℕ
a✝ : n ≥ 0
⊢ (1 - abv x ^ n) / (1 - abv x) ≤ (1 - abv x ^ n.succ) / (1 - abv x)

Proof state:
α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrderedField α
inst✝³ : Ring β
abv : β → α
inst✝² : IsAbsoluteValue abv
inst✝¹ : Archimedean α
inst✝ : Nontrivial β
x : β
hx1 : abv x < 1
hx1' : abv x ≠ 1
⊢ IsCauSeq abs fun m => (1 - abv x ^ m) / (1 - abv x)

Tactic:
have : 0 < 1 - abv x := sub_pos.2 hx1

Result:
α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrderedField α
inst✝³ : Ring β
abv : β → α
inst✝² : IsAbsoluteValue abv
inst✝¹ : Archimedean α
inst✝ : Nontrivial β
x : β
hx1 : abv x < 1
hx1' : abv x ≠ 1
this : 0 < 1 - abv x
⊢ IsCauSeq abs fun m => (1 - abv x ^ m) / (1 - abv x)