α : Type u_1
β : Type ?u.15452
inst✝³ : Ring β
inst✝² : LinearOrderedField α
inst✝¹ : Archimedean α
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → α
a : α
m : ℕ
ham : ∀ (n : ℕ), n ≥ m → abs' (f n) ≤ a
hnm : ∀ (n : ℕ), n ≥ m → f n ≤ f (Nat.succ n)
⊢ ↑(-{ val := fun n => -f n, property := (_ : IsCauSeq abs' fun n => -f n) }) = f
α : Type u_1
β : Type ?u.15452
inst✝³ : Ring β
inst✝² : LinearOrderedField α
inst✝¹ : Archimedean α
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → α
a : α
m : ℕ
ham : ∀ (n : ℕ), n ≥ m → abs' (f n) ≤ a
hnm : ∀ (n : ℕ), n ≥ m → f n ≤ f (Nat.succ n)
⊢ IsCauSeq abs' f
refine'
  @Eq.ndrecOn (ℕ → α) _ (IsCauSeq abs) _ _
    (-⟨_, @isCauSeq_of_decreasing_bounded _ _ _ (fun n => -f n) a m (by simpa) (by simpa)⟩ :
        CauSeq α abs).2
case h
α : Type u_1
β : Type ?u.15452
inst✝³ : Ring β
inst✝² : LinearOrderedField α
inst✝¹ : Archimedean α
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → α
a : α
m : ℕ
ham : ∀ (n : ℕ), n ≥ m → abs' (f n) ≤ a
hnm : ∀ (n : ℕ), n ≥ m → f n ≤ f (Nat.succ n)
x✝ : ℕ
⊢ ↑(-{ val := fun n => -f n, property := (_ : IsCauSeq abs' fun n => -f n) }) x✝ = f x✝
α : Type u_1
β : Type ?u.15452
inst✝³ : Ring β
inst✝² : LinearOrderedField α
inst✝¹ : Archimedean α
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → α
a : α
m : ℕ
ham : ∀ (n : ℕ), n ≥ m → abs' (f n) ≤ a
hnm : ∀ (n : ℕ), n ≥ m → f n ≤ f (Nat.succ n)
⊢ ↑(-{ val := fun n => -f n, property := (_ : IsCauSeq abs' fun n => -f n) }) = f
ext
no goals
case h
α : Type u_1
β : Type ?u.15452
inst✝³ : Ring β
inst✝² : LinearOrderedField α
inst✝¹ : Archimedean α
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → α
a : α
m : ℕ
ham : ∀ (n : ℕ), n ≥ m → abs' (f n) ≤ a
hnm : ∀ (n : ℕ), n ≥ m → f n ≤ f (Nat.succ n)
x✝ : ℕ
⊢ ↑(-{ val := fun n => -f n, property := (_ : IsCauSeq abs' fun n => -f n) }) x✝ = f x✝
exact neg_neg _
no goals
α : Type u_1
β : Type ?u.15452
inst✝³ : Ring β
inst✝² : LinearOrderedField α
inst✝¹ : Archimedean α
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → α
a : α
m : ℕ
ham : ∀ (n : ℕ), n ≥ m → abs' (f n) ≤ a
hnm : ∀ (n : ℕ), n ≥ m → f n ≤ f (Nat.succ n)
⊢ ∀ (n : ℕ), n ≥ m → abs' ((fun n => -f n) n) ≤ a
simpa
no goals
α : Type u_1
β : Type ?u.15452
inst✝³ : Ring β
inst✝² : LinearOrderedField α
inst✝¹ : Archimedean α
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → α
a : α
m : ℕ
ham : ∀ (n : ℕ), n ≥ m → abs' (f n) ≤ a
hnm : ∀ (n : ℕ), n ≥ m → f n ≤ f (Nat.succ n)
⊢ ∀ (n : ℕ), n ≥ m → (fun n => -f n) (Nat.succ n) ≤ (fun n => -f n) n
simpa