case intro
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : CauSeq β abv
i : ℕ
h : ∀ (j : ℕ), j ≥ i → abv (↑f j - ↑f i) < 1
⊢ ∃ r, ∀ (i : ℕ), abv (↑f i) < r
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : CauSeq β abv
⊢ ∃ r, ∀ (i : ℕ), abv (↑f i) < r
cases' f.cauchy zero_lt_one with i h
case intro
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : CauSeq β abv
i : ℕ
h : ∀ (j : ℕ), j ≥ i → abv (↑f j - ↑f i) < 1
R : ℕ → α := Nat.rec (abv (↑f 0)) fun i c => max c (abv (↑f (Nat.succ i)))
hR : R = Nat.rec (abv (↑f 0)) fun i c => max c (abv (↑f (Nat.succ i)))
⊢ ∃ r, ∀ (i : ℕ), abv (↑f i) < r
case intro
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : CauSeq β abv
i : ℕ
h : ∀ (j : ℕ), j ≥ i → abv (↑f j - ↑f i) < 1
⊢ ∃ r, ∀ (i : ℕ), abv (↑f i) < r
set R : ℕ → α := @Nat.rec (fun _ => α) (abv (f 0)) fun i c => max c (abv (f i.succ)) with hR
case intro
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : CauSeq β abv
i : ℕ
h : ∀ (j : ℕ), j ≥ i → abv (↑f j - ↑f i) < 1
R : ℕ → α := Nat.rec (abv (↑f 0)) fun i c => max c (abv (↑f (Nat.succ i)))
hR : R = Nat.rec (abv (↑f 0)) fun i c => max c (abv (↑f (Nat.succ i)))
this : ∀ (i j : ℕ), j ≤ i → abv (↑f j) ≤ R i
j : ℕ
⊢ abv (↑f j) < R i + 1
case intro
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : CauSeq β abv
i : ℕ
h : ∀ (j : ℕ), j ≥ i → abv (↑f j - ↑f i) < 1
R : ℕ → α := Nat.rec (abv (↑f 0)) fun i c => max c (abv (↑f (Nat.succ i)))
hR : R = Nat.rec (abv (↑f 0)) fun i c => max c (abv (↑f (Nat.succ i)))
this : ∀ (i j : ℕ), j ≤ i → abv (↑f j) ≤ R i
⊢ ∃ r, ∀ (i : ℕ), abv (↑f i) < r
refine' ⟨R i + 1, fun j => _⟩
case intro.inl
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : CauSeq β abv
i : ℕ
h : ∀ (j : ℕ), j ≥ i → abv (↑f j - ↑f i) < 1
R : ℕ → α := Nat.rec (abv (↑f 0)) fun i c => max c (abv (↑f (Nat.succ i)))
hR : R = Nat.rec (abv (↑f 0)) fun i c => max c (abv (↑f (Nat.succ i)))
this : ∀ (i j : ℕ), j ≤ i → abv (↑f j) ≤ R i
j : ℕ
ij : j < i
⊢ abv (↑f j) < R i + 1

case intro.inr
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : CauSeq β abv
i : ℕ
h : ∀ (j : ℕ), j ≥ i → abv (↑f j - ↑f i) < 1
R : ℕ → α := Nat.rec (abv (↑f 0)) fun i c => max c (abv (↑f (Nat.succ i)))
hR : R = Nat.rec (abv (↑f 0)) fun i c => max c (abv (↑f (Nat.succ i)))
this : ∀ (i j : ℕ), j ≤ i → abv (↑f j) ≤ R i
j : ℕ
ij : i ≤ j
⊢ abv (↑f j) < R i + 1
case intro
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : CauSeq β abv
i : ℕ
h : ∀ (j : ℕ), j ≥ i → abv (↑f j - ↑f i) < 1
R : ℕ → α := Nat.rec (abv (↑f 0)) fun i c => max c (abv (↑f (Nat.succ i)))
hR : R = Nat.rec (abv (↑f 0)) fun i c => max c (abv (↑f (Nat.succ i)))
this : ∀ (i j : ℕ), j ≤ i → abv (↑f j) ≤ R i
j : ℕ
⊢ abv (↑f j) < R i + 1
cases' lt_or_le j i with ij ij
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : CauSeq β abv
i : ℕ
h : ∀ (j : ℕ), j ≥ i → abv (↑f j - ↑f i) < 1
R : ℕ → α := Nat.rec (abv (↑f 0)) fun i c => max c (abv (↑f (Nat.succ i)))
hR : R = Nat.rec (abv (↑f 0)) fun i c => max c (abv (↑f (Nat.succ i)))
⊢ ∀ (n : ℕ), (∀ (j : ℕ), j ≤ n → abv (↑f j) ≤ R n) → ∀ (j : ℕ), j ≤ Nat.succ n → abv (↑f j) ≤ R (Nat.succ n)
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : CauSeq β abv
i : ℕ
h : ∀ (j : ℕ), j ≥ i → abv (↑f j - ↑f i) < 1
R : ℕ → α := Nat.rec (abv (↑f 0)) fun i c => max c (abv (↑f (Nat.succ i)))
hR : R = Nat.rec (abv (↑f 0)) fun i c => max c (abv (↑f (Nat.succ i)))
⊢ ∀ (i j : ℕ), j ≤ i → abv (↑f j) ≤ R i
refine' Nat.rec (by simp [hR]) _
case refl
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : CauSeq β abv
i✝ : ℕ
h : ∀ (j : ℕ), j ≥ i✝ → abv (↑f j - ↑f i✝) < 1
R : ℕ → α := Nat.rec (abv (↑f 0)) fun i c => max c (abv (↑f (Nat.succ i)))
hR : R = Nat.rec (abv (↑f 0)) fun i c => max c (abv (↑f (Nat.succ i)))
i : ℕ
hi : ∀ (j : ℕ), j ≤ i → abv (↑f j) ≤ R i
⊢ abv (↑f (Nat.succ i)) ≤ R (Nat.succ i)

case step
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : CauSeq β abv
i✝ : ℕ
h : ∀ (j : ℕ), j ≥ i✝ → abv (↑f j - ↑f i✝) < 1
R : ℕ → α := Nat.rec (abv (↑f 0)) fun i c => max c (abv (↑f (Nat.succ i)))
hR : R = Nat.rec (abv (↑f 0)) fun i c => max c (abv (↑f (Nat.succ i)))
i : ℕ
hi : ∀ (j : ℕ), j ≤ i → abv (↑f j) ≤ R i
j : ℕ
hj : Nat.le j i
⊢ abv (↑f j) ≤ R (Nat.succ i)
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : CauSeq β abv
i : ℕ
h : ∀ (j : ℕ), j ≥ i → abv (↑f j - ↑f i) < 1
R : ℕ → α := Nat.rec (abv (↑f 0)) fun i c => max c (abv (↑f (Nat.succ i)))
hR : R = Nat.rec (abv (↑f 0)) fun i c => max c (abv (↑f (Nat.succ i)))
⊢ ∀ (n : ℕ), (∀ (j : ℕ), j ≤ n → abv (↑f j) ≤ R n) → ∀ (j : ℕ), j ≤ Nat.succ n → abv (↑f j) ≤ R (Nat.succ n)
rintro i hi j (rfl | hj)
no goals
case step
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : CauSeq β abv
i✝ : ℕ
h : ∀ (j : ℕ), j ≥ i✝ → abv (↑f j - ↑f i✝) < 1
R : ℕ → α := Nat.rec (abv (↑f 0)) fun i c => max c (abv (↑f (Nat.succ i)))
hR : R = Nat.rec (abv (↑f 0)) fun i c => max c (abv (↑f (Nat.succ i)))
i : ℕ
hi : ∀ (j : ℕ), j ≤ i → abv (↑f j) ≤ R i
j : ℕ
hj : Nat.le j i
⊢ abv (↑f j) ≤ R (Nat.succ i)
exact (hi j hj).trans (le_max_left _ _)
no goals
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : CauSeq β abv
i : ℕ
h : ∀ (j : ℕ), j ≥ i → abv (↑f j - ↑f i) < 1
R : ℕ → α := Nat.rec (abv (↑f 0)) fun i c => max c (abv (↑f (Nat.succ i)))
hR : R = Nat.rec (abv (↑f 0)) fun i c => max c (abv (↑f (Nat.succ i)))
⊢ ∀ (j : ℕ), j ≤ Nat.zero → abv (↑f j) ≤ R Nat.zero
simp [hR]
no goals
case refl
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : CauSeq β abv
i✝ : ℕ
h : ∀ (j : ℕ), j ≥ i✝ → abv (↑f j - ↑f i✝) < 1
R : ℕ → α := Nat.rec (abv (↑f 0)) fun i c => max c (abv (↑f (Nat.succ i)))
hR : R = Nat.rec (abv (↑f 0)) fun i c => max c (abv (↑f (Nat.succ i)))
i : ℕ
hi : ∀ (j : ℕ), j ≤ i → abv (↑f j) ≤ R i
⊢ abv (↑f (Nat.succ i)) ≤ R (Nat.succ i)
simp
no goals
case intro.inl
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : CauSeq β abv
i : ℕ
h : ∀ (j : ℕ), j ≥ i → abv (↑f j - ↑f i) < 1
R : ℕ → α := Nat.rec (abv (↑f 0)) fun i c => max c (abv (↑f (Nat.succ i)))
hR : R = Nat.rec (abv (↑f 0)) fun i c => max c (abv (↑f (Nat.succ i)))
this : ∀ (i j : ℕ), j ≤ i → abv (↑f j) ≤ R i
j : ℕ
ij : j < i
⊢ abv (↑f j) < R i + 1
exact lt_of_le_of_lt (this i _ (le_of_lt ij)) (lt_add_one _)
case intro.inr
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : CauSeq β abv
i : ℕ
h : ∀ (j : ℕ), j ≥ i → abv (↑f j - ↑f i) < 1
R : ℕ → α := Nat.rec (abv (↑f 0)) fun i c => max c (abv (↑f (Nat.succ i)))
hR : R = Nat.rec (abv (↑f 0)) fun i c => max c (abv (↑f (Nat.succ i)))
this✝ : ∀ (i j : ℕ), j ≤ i → abv (↑f j) ≤ R i
j : ℕ
ij : i ≤ j
this : abv (↑f i + (↑f j - ↑f i)) < R i + 1
⊢ abv (↑f j) < R i + 1
case intro.inr
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : CauSeq β abv
i : ℕ
h : ∀ (j : ℕ), j ≥ i → abv (↑f j - ↑f i) < 1
R : ℕ → α := Nat.rec (abv (↑f 0)) fun i c => max c (abv (↑f (Nat.succ i)))
hR : R = Nat.rec (abv (↑f 0)) fun i c => max c (abv (↑f (Nat.succ i)))
this : ∀ (i j : ℕ), j ≤ i → abv (↑f j) ≤ R i
j : ℕ
ij : i ≤ j
⊢ abv (↑f j) < R i + 1
have := lt_of_le_of_lt (abv_add abv _ _) (add_lt_add_of_le_of_lt (this i _ le_rfl) (h _ ij))
case intro.inr
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : CauSeq β abv
i : ℕ
h : ∀ (j : ℕ), j ≥ i → abv (↑f j - ↑f i) < 1
R : ℕ → α := Nat.rec (abv (↑f 0)) fun i c => max c (abv (↑f (Nat.succ i)))
hR : R = Nat.rec (abv (↑f 0)) fun i c => max c (abv (↑f (Nat.succ i)))
this✝ : ∀ (i j : ℕ), j ≤ i → abv (↑f j) ≤ R i
j : ℕ
ij : i ≤ j
this : abv (↑f j + ↑f i - ↑f i) < R i + 1
⊢ abv (↑f j) < R i + 1
case intro.inr
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : CauSeq β abv
i : ℕ
h : ∀ (j : ℕ), j ≥ i → abv (↑f j - ↑f i) < 1
R : ℕ → α := Nat.rec (abv (↑f 0)) fun i c => max c (abv (↑f (Nat.succ i)))
hR : R = Nat.rec (abv (↑f 0)) fun i c => max c (abv (↑f (Nat.succ i)))
this✝ : ∀ (i j : ℕ), j ≤ i → abv (↑f j) ≤ R i
j : ℕ
ij : i ≤ j
this : abv (↑f i + (↑f j - ↑f i)) < R i + 1
⊢ abv (↑f j) < R i + 1
rw [add_sub, add_comm] at this
no goals
case intro.inr
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : CauSeq β abv
i : ℕ
h : ∀ (j : ℕ), j ≥ i → abv (↑f j - ↑f i) < 1
R : ℕ → α := Nat.rec (abv (↑f 0)) fun i c => max c (abv (↑f (Nat.succ i)))
hR : R = Nat.rec (abv (↑f 0)) fun i c => max c (abv (↑f (Nat.succ i)))
this✝ : ∀ (i j : ℕ), j ≤ i → abv (↑f j) ≤ R i
j : ℕ
ij : i ≤ j
this : abv (↑f j + ↑f i - ↑f i) < R i + 1
⊢ abv (↑f j) < R i + 1
simpa using this