no goals
α : Type u_2
inst✝⁴ : LinearOrderedField α
inst✝³ : Archimedean α
β : Type u_1
inst✝² : Ring β
inst✝¹ : Nontrivial β
abv : β → α
inst✝ : IsAbsoluteValue abv
x : β
hx1 : abv x < 1
h : abv x = 1
⊢ False
simp [h, lt_irrefl] at hx1
α : Type u_2
inst✝⁴ : LinearOrderedField α
inst✝³ : Archimedean α
β : Type u_1
inst✝² : Ring β
inst✝¹ : Nontrivial β
abv : β → α
inst✝ : IsAbsoluteValue abv
x : β
hx1 : abv x < 1
hx1' : abv x ≠ 1
⊢ IsCauSeq abs' fun m => (abv x ^ m - 1) / (abv x - 1)
α : Type u_2
inst✝⁴ : LinearOrderedField α
inst✝³ : Archimedean α
β : Type u_1
inst✝² : Ring β
inst✝¹ : Nontrivial β
abv : β → α
inst✝ : IsAbsoluteValue abv
x : β
hx1 : abv x < 1
hx1' : abv x ≠ 1
⊢ IsCauSeq abs' fun m => ∑ n in range m, abv (x ^ n)
simp only [abv_pow abv, geom_sum_eq hx1']
α : Type u_2
inst✝⁴ : LinearOrderedField α
inst✝³ : Archimedean α
β : Type u_1
inst✝² : Ring β
inst✝¹ : Nontrivial β
abv : β → α
inst✝ : IsAbsoluteValue abv
x : β
hx1 : abv x < 1
hx1' : abv x ≠ 1
⊢ IsCauSeq abs' fun m => (1 - abv x ^ m) / (1 - abv x)
α : Type u_2
inst✝⁴ : LinearOrderedField α
inst✝³ : Archimedean α
β : Type u_1
inst✝² : Ring β
inst✝¹ : Nontrivial β
abv : β → α
inst✝ : IsAbsoluteValue abv
x : β
hx1 : abv x < 1
hx1' : abv x ≠ 1
⊢ IsCauSeq abs' fun m => (abv x ^ m - 1) / (abv x - 1)
conv in _ / _ => rw [← neg_div_neg_eq, neg_sub, neg_sub]
α : Type u_2
inst✝⁴ : LinearOrderedField α
inst✝³ : Archimedean α
β : Type u_1
inst✝² : Ring β
inst✝¹ : Nontrivial β
abv : β → α
inst✝ : IsAbsoluteValue abv
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)
α : Type u_2
inst✝⁴ : LinearOrderedField α
inst✝³ : Archimedean α
β : Type u_1
inst✝² : Ring β
inst✝¹ : Nontrivial β
abv : β → α
inst✝ : IsAbsoluteValue abv
x : β
hx1 : abv x < 1
hx1' : abv x ≠ 1
⊢ IsCauSeq abs' fun m => (1 - abv x ^ m) / (1 - abv x)
have : 0 < 1 - abv x := sub_pos.2 hx1
case refine'_1
α : Type u_2
inst✝⁴ : LinearOrderedField α
inst✝³ : Archimedean α
β : Type u_1
inst✝² : Ring β
inst✝¹ : Nontrivial β
abv : β → α
inst✝ : IsAbsoluteValue abv
x : β
hx1 : abv x < 1
hx1' : abv x ≠ 1
this : 0 < 1 - abv x
⊢ ∀ (n : ℕ), n ≥ 0 → abs' ((1 - abv x ^ n) / (1 - abv x)) ≤ 1 / (1 - abv x)

case refine'_2
α : Type u_2
inst✝⁴ : LinearOrderedField α
inst✝³ : Archimedean α
β : Type u_1
inst✝² : Ring β
inst✝¹ : Nontrivial β
abv : β → α
inst✝ : IsAbsoluteValue abv
x : β
hx1 : abv x < 1
hx1' : abv x ≠ 1
this : 0 < 1 - abv x
⊢ ∀ (n : ℕ), n ≥ 0 → (1 - abv x ^ n) / (1 - abv x) ≤ (1 - abv x ^ Nat.succ n) / (1 - abv x)
α : Type u_2
inst✝⁴ : LinearOrderedField α
inst✝³ : Archimedean α
β : Type u_1
inst✝² : Ring β
inst✝¹ : Nontrivial β
abv : β → α
inst✝ : IsAbsoluteValue abv
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)
refine' @isCauSeq_of_mono_bounded _ _ _ _ ((1 : α) / (1 - abv x)) 0 _ _
case refine'_1
α : Type u_2
inst✝⁴ : LinearOrderedField α
inst✝³ : Archimedean α
β : Type u_1
inst✝² : Ring β
inst✝¹ : Nontrivial β
abv : β → α
inst✝ : IsAbsoluteValue abv
x : β
hx1 : abv x < 1
hx1' : abv x ≠ 1
this : 0 < 1 - abv x
n : ℕ
a✝ : n ≥ 0
⊢ abs' ((1 - abv x ^ n) / (1 - abv x)) ≤ 1 / (1 - abv x)
case refine'_1
α : Type u_2
inst✝⁴ : LinearOrderedField α
inst✝³ : Archimedean α
β : Type u_1
inst✝² : Ring β
inst✝¹ : Nontrivial β
abv : β → α
inst✝ : IsAbsoluteValue abv
x : β
hx1 : abv x < 1
hx1' : abv x ≠ 1
this : 0 < 1 - abv x
⊢ ∀ (n : ℕ), n ≥ 0 → abs' ((1 - abv x ^ n) / (1 - abv x)) ≤ 1 / (1 - abv x)
intro n _
case refine'_1
α : Type u_2
inst✝⁴ : LinearOrderedField α
inst✝³ : Archimedean α
β : Type u_1
inst✝² : Ring β
inst✝¹ : Nontrivial β
abv : β → α
inst✝ : IsAbsoluteValue abv
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_2
inst✝⁴ : LinearOrderedField α
inst✝³ : Archimedean α
β : Type u_1
inst✝² : Ring β
inst✝¹ : Nontrivial β
abv : β → α
inst✝ : IsAbsoluteValue abv
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)
case refine'_1
α : Type u_2
inst✝⁴ : LinearOrderedField α
inst✝³ : Archimedean α
β : Type u_1
inst✝² : Ring β
inst✝¹ : Nontrivial β
abv : β → α
inst✝ : IsAbsoluteValue abv
x : β
hx1 : abv x < 1
hx1' : abv x ≠ 1
this : 0 < 1 - abv x
n : ℕ
a✝ : n ≥ 0
⊢ abs' ((1 - abv x ^ n) / (1 - abv x)) ≤ 1 / (1 - abv x)
rw [abs_of_nonneg]
case refine'_1.h
α : Type u_2
inst✝⁴ : LinearOrderedField α
inst✝³ : Archimedean α
β : Type u_1
inst✝² : Ring β
inst✝¹ : Nontrivial β
abv : β → α
inst✝ : IsAbsoluteValue abv
x : β
hx1 : abv x < 1
hx1' : abv x ≠ 1
this : 0 < 1 - abv x
n : ℕ
a✝ : n ≥ 0
⊢ 1 - abv x ^ n ≤ 1

case refine'_1
α : Type u_2
inst✝⁴ : LinearOrderedField α
inst✝³ : Archimedean α
β : Type u_1
inst✝² : Ring β
inst✝¹ : Nontrivial β
abv : β → α
inst✝ : IsAbsoluteValue abv
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)
case refine'_1
α : Type u_2
inst✝⁴ : LinearOrderedField α
inst✝³ : Archimedean α
β : Type u_1
inst✝² : Ring β
inst✝¹ : Nontrivial β
abv : β → α
inst✝ : IsAbsoluteValue abv
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_2
inst✝⁴ : LinearOrderedField α
inst✝³ : Archimedean α
β : Type u_1
inst✝² : Ring β
inst✝¹ : Nontrivial β
abv : β → α
inst✝ : IsAbsoluteValue abv
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)
gcongr
case refine'_1
α : Type u_2
inst✝⁴ : LinearOrderedField α
inst✝³ : Archimedean α
β : Type u_1
inst✝² : Ring β
inst✝¹ : Nontrivial β
abv : β → α
inst✝ : IsAbsoluteValue abv
x : β
hx1 : abv x < 1
hx1' : abv x ≠ 1
this : 0 < 1 - abv x
n : ℕ
a✝ : n ≥ 0
⊢ abv x ^ n ≤ 1
case refine'_1
α : Type u_2
inst✝⁴ : LinearOrderedField α
inst✝³ : Archimedean α
β : Type u_1
inst✝² : Ring β
inst✝¹ : Nontrivial β
abv : β → α
inst✝ : IsAbsoluteValue abv
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)
refine' div_nonneg (sub_nonneg.2 _) (sub_nonneg.2 <| le_of_lt hx1)
no goals
case refine'_1
α : Type u_2
inst✝⁴ : LinearOrderedField α
inst✝³ : Archimedean α
β : Type u_1
inst✝² : Ring β
inst✝¹ : Nontrivial β
abv : β → α
inst✝ : IsAbsoluteValue abv
x : β
hx1 : abv x < 1
hx1' : abv x ≠ 1
this : 0 < 1 - abv x
n : ℕ
a✝ : n ≥ 0
⊢ abv x ^ n ≤ 1
exact pow_le_one _ (by positivity) hx1.le
no goals
case refine'_1.h
α : Type u_2
inst✝⁴ : LinearOrderedField α
inst✝³ : Archimedean α
β : Type u_1
inst✝² : Ring β
inst✝¹ : Nontrivial β
abv : β → α
inst✝ : IsAbsoluteValue abv
x : β
hx1 : abv x < 1
hx1' : abv x ≠ 1
this : 0 < 1 - abv x
n : ℕ
a✝ : n ≥ 0
⊢ 1 - abv x ^ n ≤ 1
exact sub_le_self _ (abv_pow abv x n ▸ abv_nonneg _ _)
no goals
α : Type u_2
inst✝⁴ : LinearOrderedField α
inst✝³ : Archimedean α
β : Type u_1
inst✝² : Ring β
inst✝¹ : Nontrivial β
abv : β → α
inst✝ : IsAbsoluteValue abv
x : β
hx1 : abv x < 1
hx1' : abv x ≠ 1
this : 0 < 1 - abv x
n : ℕ
a✝ : n ≥ 0
⊢ 0 ≤ abv x
positivity
case refine'_2
α : Type u_2
inst✝⁴ : LinearOrderedField α
inst✝³ : Archimedean α
β : Type u_1
inst✝² : Ring β
inst✝¹ : Nontrivial β
abv : β → α
inst✝ : IsAbsoluteValue abv
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 ^ Nat.succ n) / (1 - abv x)
case refine'_2
α : Type u_2
inst✝⁴ : LinearOrderedField α
inst✝³ : Archimedean α
β : Type u_1
inst✝² : Ring β
inst✝¹ : Nontrivial β
abv : β → α
inst✝ : IsAbsoluteValue abv
x : β
hx1 : abv x < 1
hx1' : abv x ≠ 1
this : 0 < 1 - abv x
⊢ ∀ (n : ℕ), n ≥ 0 → (1 - abv x ^ n) / (1 - abv x) ≤ (1 - abv x ^ Nat.succ n) / (1 - abv x)
intro n _
case refine'_2
α : Type u_2
inst✝⁴ : LinearOrderedField α
inst✝³ : Archimedean α
β : Type u_1
inst✝² : Ring β
inst✝¹ : Nontrivial β
abv : β → α
inst✝ : IsAbsoluteValue abv
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)
case refine'_2
α : Type u_2
inst✝⁴ : LinearOrderedField α
inst✝³ : Archimedean α
β : Type u_1
inst✝² : Ring β
inst✝¹ : Nontrivial β
abv : β → α
inst✝ : IsAbsoluteValue abv
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 ^ Nat.succ n) / (1 - abv x)
rw [←one_mul (abv x ^ n), pow_succ]
no goals
case refine'_2
α : Type u_2
inst✝⁴ : LinearOrderedField α
inst✝³ : Archimedean α
β : Type u_1
inst✝² : Ring β
inst✝¹ : Nontrivial β
abv : β → α
inst✝ : IsAbsoluteValue abv
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)
gcongr