[GOAL]
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
ε : α
ε0 : 0 < ε
a₁ a₂ b₁ b₂ : β
h₁ : abv (a₁ - b₁) < ε / 2
h₂ : abv (a₂ - b₂) < ε / 2
⊢ abv (a₁ + a₂ - (b₁ + b₂)) < ε
[PROOFSTEP]
simpa [add_halves, sub_eq_add_neg, add_comm, add_left_comm, add_assoc] using
  lt_of_le_of_lt (abv_add abv _ _) (add_lt_add h₁ h₂)
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
ε K₁ K₂ : α
ε0 : 0 < ε
⊢ ∃ δ,
    δ > 0 ∧
      ∀ {a₁ a₂ b₁ b₂ : β},
        abv a₁ < K₁ → abv b₂ < K₂ → abv (a₁ - b₁) < δ → abv (a₂ - b₂) < δ → abv (a₁ * a₂ - b₁ * b₂) < ε
[PROOFSTEP]
have K0 : (0 : α) < max 1 (max K₁ K₂) := lt_of_lt_of_le zero_lt_one (le_max_left _ _)
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
ε K₁ K₂ : α
ε0 : 0 < ε
K0 : 0 < max 1 (max K₁ K₂)
⊢ ∃ δ,
    δ > 0 ∧
      ∀ {a₁ a₂ b₁ b₂ : β},
        abv a₁ < K₁ → abv b₂ < K₂ → abv (a₁ - b₁) < δ → abv (a₂ - b₂) < δ → abv (a₁ * a₂ - b₁ * b₂) < ε
[PROOFSTEP]
have εK := div_pos (half_pos ε0) K0
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
ε K₁ K₂ : α
ε0 : 0 < ε
K0 : 0 < max 1 (max K₁ K₂)
εK : 0 < ε / 2 / max 1 (max K₁ K₂)
⊢ ∃ δ,
    δ > 0 ∧
      ∀ {a₁ a₂ b₁ b₂ : β},
        abv a₁ < K₁ → abv b₂ < K₂ → abv (a₁ - b₁) < δ → abv (a₂ - b₂) < δ → abv (a₁ * a₂ - b₁ * b₂) < ε
[PROOFSTEP]
refine' ⟨_, εK, fun {a₁ a₂ b₁ b₂} ha₁ hb₂ h₁ h₂ => _⟩
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
ε K₁ K₂ : α
ε0 : 0 < ε
K0 : 0 < max 1 (max K₁ K₂)
εK : 0 < ε / 2 / max 1 (max K₁ K₂)
a₁ a₂ b₁ b₂ : β
ha₁ : abv a₁ < K₁
hb₂ : abv b₂ < K₂
h₁ : abv (a₁ - b₁) < ε / 2 / max 1 (max K₁ K₂)
h₂ : abv (a₂ - b₂) < ε / 2 / max 1 (max K₁ K₂)
⊢ abv (a₁ * a₂ - b₁ * b₂) < ε
[PROOFSTEP]
replace ha₁ := lt_of_lt_of_le ha₁ (le_trans (le_max_left _ K₂) (le_max_right 1 _))
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
ε K₁ K₂ : α
ε0 : 0 < ε
K0 : 0 < max 1 (max K₁ K₂)
εK : 0 < ε / 2 / max 1 (max K₁ K₂)
a₁ a₂ b₁ b₂ : β
hb₂ : abv b₂ < K₂
h₁ : abv (a₁ - b₁) < ε / 2 / max 1 (max K₁ K₂)
h₂ : abv (a₂ - b₂) < ε / 2 / max 1 (max K₁ K₂)
ha₁ : abv a₁ < max 1 (max K₁ K₂)
⊢ abv (a₁ * a₂ - b₁ * b₂) < ε
[PROOFSTEP]
replace hb₂ := lt_of_lt_of_le hb₂ (le_trans (le_max_right K₁ _) (le_max_right 1 _))
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
ε K₁ K₂ : α
ε0 : 0 < ε
K0 : 0 < max 1 (max K₁ K₂)
εK : 0 < ε / 2 / max 1 (max K₁ K₂)
a₁ a₂ b₁ b₂ : β
h₁ : abv (a₁ - b₁) < ε / 2 / max 1 (max K₁ K₂)
h₂ : abv (a₂ - b₂) < ε / 2 / max 1 (max K₁ K₂)
ha₁ : abv a₁ < max 1 (max K₁ K₂)
hb₂ : abv b₂ < max 1 (max K₁ K₂)
⊢ abv (a₁ * a₂ - b₁ * b₂) < ε
[PROOFSTEP]
set M := max 1 (max K₁ K₂)
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
ε K₁ K₂ : α
ε0 : 0 < ε
a₁ a₂ b₁ b₂ : β
M : α := max 1 (max K₁ K₂)
K0 : 0 < M
εK : 0 < ε / 2 / M
h₁ : abv (a₁ - b₁) < ε / 2 / M
h₂ : abv (a₂ - b₂) < ε / 2 / M
ha₁ : abv a₁ < M
hb₂ : abv b₂ < M
⊢ abv (a₁ * a₂ - b₁ * b₂) < ε
[PROOFSTEP]
have : abv (a₁ - b₁) * abv b₂ + abv (a₂ - b₂) * abv a₁ < ε / 2 / M * M + ε / 2 / M * M
[GOAL]
case this
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
ε K₁ K₂ : α
ε0 : 0 < ε
a₁ a₂ b₁ b₂ : β
M : α := max 1 (max K₁ K₂)
K0 : 0 < M
εK : 0 < ε / 2 / M
h₁ : abv (a₁ - b₁) < ε / 2 / M
h₂ : abv (a₂ - b₂) < ε / 2 / M
ha₁ : abv a₁ < M
hb₂ : abv b₂ < M
⊢ abv (a₁ - b₁) * abv b₂ + abv (a₂ - b₂) * abv a₁ < ε / 2 / M * M + ε / 2 / M * M
[PROOFSTEP]
gcongr
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
ε K₁ K₂ : α
ε0 : 0 < ε
a₁ a₂ b₁ b₂ : β
M : α := max 1 (max K₁ K₂)
K0 : 0 < M
εK : 0 < ε / 2 / M
h₁ : abv (a₁ - b₁) < ε / 2 / M
h₂ : abv (a₂ - b₂) < ε / 2 / M
ha₁ : abv a₁ < M
hb₂ : abv b₂ < M
this : abv (a₁ - b₁) * abv b₂ + abv (a₂ - b₂) * abv a₁ < ε / 2 / M * M + ε / 2 / M * M
⊢ abv (a₁ * a₂ - b₁ * b₂) < ε
[PROOFSTEP]
rw [← abv_mul abv, mul_comm, div_mul_cancel _ (ne_of_gt K0), ← abv_mul abv, add_halves] at this 
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
ε K₁ K₂ : α
ε0 : 0 < ε
a₁ a₂ b₁ b₂ : β
M : α := max 1 (max K₁ K₂)
K0 : 0 < M
εK : 0 < ε / 2 / M
h₁ : abv (a₁ - b₁) < ε / 2 / M
h₂ : abv (a₂ - b₂) < ε / 2 / M
ha₁ : abv a₁ < M
hb₂ : abv b₂ < M
this : abv ((a₁ - b₁) * b₂) + abv (a₁ * (a₂ - b₂)) < ε
⊢ abv (a₁ * a₂ - b₁ * b₂) < ε
[PROOFSTEP]
simpa [sub_eq_add_neg, mul_add, add_mul, add_left_comm] using lt_of_le_of_lt (abv_add abv _ _) this
[GOAL]
α : Type u_2
β✝ : Type ?u.21207
inst✝⁴ : LinearOrderedField α
inst✝³ : Ring β✝
abv✝ : β✝ → α
inst✝² : IsAbsoluteValue abv✝
β : Type u_1
inst✝¹ : DivisionRing β
abv : β → α
inst✝ : IsAbsoluteValue abv
ε K : α
ε0 : 0 < ε
K0 : 0 < K
⊢ ∃ δ, δ > 0 ∧ ∀ {a b : β}, K ≤ abv a → K ≤ abv b → abv (a - b) < δ → abv (a⁻¹ - b⁻¹) < ε
[PROOFSTEP]
refine' ⟨K * ε * K, mul_pos (mul_pos K0 ε0) K0, fun {a b} ha hb h => _⟩
[GOAL]
α : Type u_2
β✝ : Type ?u.21207
inst✝⁴ : LinearOrderedField α
inst✝³ : Ring β✝
abv✝ : β✝ → α
inst✝² : IsAbsoluteValue abv✝
β : Type u_1
inst✝¹ : DivisionRing β
abv : β → α
inst✝ : IsAbsoluteValue abv
ε K : α
ε0 : 0 < ε
K0 : 0 < K
a b : β
ha : K ≤ abv a
hb : K ≤ abv b
h : abv (a - b) < K * ε * K
⊢ abv (a⁻¹ - b⁻¹) < ε
[PROOFSTEP]
have a0 := K0.trans_le ha
[GOAL]
α : Type u_2
β✝ : Type ?u.21207
inst✝⁴ : LinearOrderedField α
inst✝³ : Ring β✝
abv✝ : β✝ → α
inst✝² : IsAbsoluteValue abv✝
β : Type u_1
inst✝¹ : DivisionRing β
abv : β → α
inst✝ : IsAbsoluteValue abv
ε K : α
ε0 : 0 < ε
K0 : 0 < K
a b : β
ha : K ≤ abv a
hb : K ≤ abv b
h : abv (a - b) < K * ε * K
a0 : 0 < abv a
⊢ abv (a⁻¹ - b⁻¹) < ε
[PROOFSTEP]
have b0 := K0.trans_le hb
[GOAL]
α : Type u_2
β✝ : Type ?u.21207
inst✝⁴ : LinearOrderedField α
inst✝³ : Ring β✝
abv✝ : β✝ → α
inst✝² : IsAbsoluteValue abv✝
β : Type u_1
inst✝¹ : DivisionRing β
abv : β → α
inst✝ : IsAbsoluteValue abv
ε K : α
ε0 : 0 < ε
K0 : 0 < K
a b : β
ha : K ≤ abv a
hb : K ≤ abv b
h : abv (a - b) < K * ε * K
a0 : 0 < abv a
b0 : 0 < abv b
⊢ abv (a⁻¹ - b⁻¹) < ε
[PROOFSTEP]
rw [inv_sub_inv' ((abv_pos abv).1 a0) ((abv_pos abv).1 b0), abv_mul abv, abv_mul abv, abv_inv abv, abv_inv abv,
  abv_sub abv]
[GOAL]
α : Type u_2
β✝ : Type ?u.21207
inst✝⁴ : LinearOrderedField α
inst✝³ : Ring β✝
abv✝ : β✝ → α
inst✝² : IsAbsoluteValue abv✝
β : Type u_1
inst✝¹ : DivisionRing β
abv : β → α
inst✝ : IsAbsoluteValue abv
ε K : α
ε0 : 0 < ε
K0 : 0 < K
a b : β
ha : K ≤ abv a
hb : K ≤ abv b
h : abv (a - b) < K * ε * K
a0 : 0 < abv a
b0 : 0 < abv b
⊢ (abv a)⁻¹ * abv (a - b) * (abv b)⁻¹ < ε
[PROOFSTEP]
refine' lt_of_mul_lt_mul_left (lt_of_mul_lt_mul_right _ b0.le) a0.le
[GOAL]
α : Type u_2
β✝ : Type ?u.21207
inst✝⁴ : LinearOrderedField α
inst✝³ : Ring β✝
abv✝ : β✝ → α
inst✝² : IsAbsoluteValue abv✝
β : Type u_1
inst✝¹ : DivisionRing β
abv : β → α
inst✝ : IsAbsoluteValue abv
ε K : α
ε0 : 0 < ε
K0 : 0 < K
a b : β
ha : K ≤ abv a
hb : K ≤ abv b
h : abv (a - b) < K * ε * K
a0 : 0 < abv a
b0 : 0 < abv b
⊢ abv a * ((abv a)⁻¹ * abv (a - b) * (abv b)⁻¹) * abv b < abv a * ε * abv b
[PROOFSTEP]
rw [mul_assoc, inv_mul_cancel_right₀ b0.ne', ← mul_assoc, mul_inv_cancel a0.ne', one_mul]
[GOAL]
α : Type u_2
β✝ : Type ?u.21207
inst✝⁴ : LinearOrderedField α
inst✝³ : Ring β✝
abv✝ : β✝ → α
inst✝² : IsAbsoluteValue abv✝
β : Type u_1
inst✝¹ : DivisionRing β
abv : β → α
inst✝ : IsAbsoluteValue abv
ε K : α
ε0 : 0 < ε
K0 : 0 < K
a b : β
ha : K ≤ abv a
hb : K ≤ abv b
h : abv (a - b) < K * ε * K
a0 : 0 < abv a
b0 : 0 < abv b
⊢ abv (a - b) < abv a * ε * abv b
[PROOFSTEP]
refine' h.trans_le _
[GOAL]
α : Type u_2
β✝ : Type ?u.21207
inst✝⁴ : LinearOrderedField α
inst✝³ : Ring β✝
abv✝ : β✝ → α
inst✝² : IsAbsoluteValue abv✝
β : Type u_1
inst✝¹ : DivisionRing β
abv : β → α
inst✝ : IsAbsoluteValue abv
ε K : α
ε0 : 0 < ε
K0 : 0 < K
a b : β
ha : K ≤ abv a
hb : K ≤ abv b
h : abv (a - b) < K * ε * K
a0 : 0 < abv a
b0 : 0 < abv b
⊢ K * ε * K ≤ abv a * ε * abv b
[PROOFSTEP]
gcongr
[GOAL]
α : Type u_2
β : Type u_1
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f g : ℕ → β
hf : IsCauSeq abv f
ε : α
ε0 : 0 < ε
⊢ ∃ i, ∀ (j : ℕ), j ≥ i → ∀ (k : ℕ), k ≥ i → abv (f j - f k) < ε
[PROOFSTEP]
refine' (hf _ (half_pos ε0)).imp fun i hi j ij k ik => _
[GOAL]
α : Type u_2
β : Type u_1
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f g : ℕ → β
hf : IsCauSeq abv f
ε : α
ε0 : 0 < ε
i : ℕ
hi : ∀ (j : ℕ), j ≥ i → abv (f j - f i) < ε / 2
j : ℕ
ij : j ≥ i
k : ℕ
ik : k ≥ i
⊢ abv (f j - f k) < ε
[PROOFSTEP]
rw [← add_halves ε]
[GOAL]
α : Type u_2
β : Type u_1
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f g : ℕ → β
hf : IsCauSeq abv f
ε : α
ε0 : 0 < ε
i : ℕ
hi : ∀ (j : ℕ), j ≥ i → abv (f j - f i) < ε / 2
j : ℕ
ij : j ≥ i
k : ℕ
ik : k ≥ i
⊢ abv (f j - f k) < ε / 2 + ε / 2
[PROOFSTEP]
refine' lt_of_le_of_lt (abv_sub_le abv _ _ _) (add_lt_add (hi _ ij) _)
[GOAL]
α : Type u_2
β : Type u_1
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f g : ℕ → β
hf : IsCauSeq abv f
ε : α
ε0 : 0 < ε
i : ℕ
hi : ∀ (j : ℕ), j ≥ i → abv (f j - f i) < ε / 2
j : ℕ
ij : j ≥ i
k : ℕ
ik : k ≥ i
⊢ abv (f i - f k) < ε / 2
[PROOFSTEP]
rw [abv_sub abv]
[GOAL]
α : Type u_2
β : Type u_1
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f g : ℕ → β
hf : IsCauSeq abv f
ε : α
ε0 : 0 < ε
i : ℕ
hi : ∀ (j : ℕ), j ≥ i → abv (f j - f i) < ε / 2
j : ℕ
ij : j ≥ i
k : ℕ
ik : k ≥ i
⊢ abv (f k - f i) < ε / 2
[PROOFSTEP]
exact hi _ ik
[GOAL]
α : Type ?u.36935
β : Type ?u.36938
inst✝¹ : LinearOrderedField α
inst✝ : Ring β
abv : β → α
f : CauSeq β abv
g : ℕ → β
e : ∀ (i : ℕ), ↑f i = g i
ε : α
⊢ ε > 0 → ∃ i, ∀ (j : ℕ), j ≥ i → abv (g j - g i) < ε
[PROOFSTEP]
rw [show g = f from (funext e).symm]
[GOAL]
α : Type ?u.36935
β : Type ?u.36938
inst✝¹ : LinearOrderedField α
inst✝ : Ring β
abv : β → α
f : CauSeq β abv
g : ℕ → β
e : ∀ (i : ℕ), ↑f i = g i
ε : α
⊢ ε > 0 → ∃ i, ∀ (j : ℕ), j ≥ i → abv (↑f j - ↑f i) < ε
[PROOFSTEP]
exact f.cauchy
[GOAL]
α : Type u_2
β : Type u_1
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : CauSeq β abv
⊢ ∃ r, ∀ (i : ℕ), abv (↑f i) < r
[PROOFSTEP]
cases' f.cauchy zero_lt_one with i h
[GOAL]
case intro
α : Type u_2
β : Type u_1
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
[PROOFSTEP]
set R : ℕ → α := @Nat.rec (fun _ => α) (abv (f 0)) fun i c => max c (abv (f i.succ)) with hR
[GOAL]
case intro
α : Type u_2
β : Type u_1
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
[PROOFSTEP]
have : ∀ i, ∀ j ≤ i, abv (f j) ≤ R i := by
  refine' Nat.rec (by simp [hR]) _
  rintro i hi j (rfl | hj)
  · simp
  exact (hi j hj).trans (le_max_left _ _)
[GOAL]
α : Type u_2
β : Type u_1
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
[PROOFSTEP]
refine' Nat.rec (by simp [hR]) _
[GOAL]
α : Type u_2
β : Type u_1
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
[PROOFSTEP]
simp [hR]
[GOAL]
α : Type u_2
β : Type u_1
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)
[PROOFSTEP]
rintro i hi j (rfl | hj)
[GOAL]
case refl
α : Type u_2
β : Type u_1
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)
[PROOFSTEP]
simp
[GOAL]
case step
α : Type u_2
β : Type u_1
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)
[PROOFSTEP]
exact (hi j hj).trans (le_max_left _ _)
[GOAL]
case intro
α : Type u_2
β : Type u_1
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
[PROOFSTEP]
refine' ⟨R i + 1, fun j => _⟩
[GOAL]
case intro
α : Type u_2
β : Type u_1
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
[PROOFSTEP]
cases' lt_or_le j i with ij ij
[GOAL]
case intro.inl
α : Type u_2
β : Type u_1
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
[PROOFSTEP]
exact lt_of_le_of_lt (this i _ (le_of_lt ij)) (lt_add_one _)
[GOAL]
case intro.inr
α : Type u_2
β : Type u_1
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
[PROOFSTEP]
have := lt_of_le_of_lt (abv_add abv _ _) (add_lt_add_of_le_of_lt (this i _ le_rfl) (h _ ij))
[GOAL]
case intro.inr
α : Type u_2
β : Type u_1
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
[PROOFSTEP]
rw [add_sub, add_comm] at this 
[GOAL]
case intro.inr
α : Type u_2
β : Type u_1
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
[PROOFSTEP]
simpa using this
[GOAL]
α : Type ?u.58870
β : Type ?u.58873
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
x : β
ε : α
ε0 : ε > 0
j : ℕ
x✝ : j ≥ 0
⊢ abv ((fun x_1 => x) j - (fun x_1 => x) 0) < ε
[PROOFSTEP]
simpa [abv_zero] using ε0
[GOAL]
α : Type ?u.84925
β : Type ?u.84928
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : CauSeq β abv
i : ℕ
⊢ ↑(const (-1) * f) i = (fun x => -↑f x) i
[PROOFSTEP]
simp
[GOAL]
α : Type ?u.88209
β : Type ?u.88212
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f g : CauSeq β abv
i : ℕ
⊢ ↑(f + -g) i = (fun x => ↑f x - ↑g x) i
[PROOFSTEP]
simp [sub_eq_add_neg]
[GOAL]
α : Type ?u.110288
β : Type ?u.110291
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
⊢ ∀ (x : CauSeq β abv) (n : ℕ), ↑(n • x) = n • ↑x
[PROOFSTEP]
intros
[GOAL]
α : Type ?u.110288
β : Type ?u.110291
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
x✝ : CauSeq β abv
n✝ : ℕ
⊢ ↑(n✝ • x✝) = n✝ • ↑x✝
[PROOFSTEP]
rfl
[GOAL]
α : Type ?u.110288
β : Type ?u.110291
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
⊢ ∀ (x : CauSeq β abv) (n : ℤ), ↑(n • x) = n • ↑x
[PROOFSTEP]
intros
[GOAL]
α : Type ?u.110288
β : Type ?u.110291
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
x✝ : CauSeq β abv
n✝ : ℤ
⊢ ↑(n✝ • x✝) = n✝ • ↑x✝
[PROOFSTEP]
rfl
[GOAL]
α : Type ?u.110288
β : Type ?u.110291
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
⊢ ∀ (n : ℕ), ↑↑n = ↑n
[PROOFSTEP]
intros
[GOAL]
α : Type ?u.110288
β : Type ?u.110291
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
n✝ : ℕ
⊢ ↑↑n✝ = ↑n✝
[PROOFSTEP]
rfl
[GOAL]
α : Type ?u.110288
β : Type ?u.110291
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
⊢ ∀ (n : ℤ), ↑↑n = ↑n
[PROOFSTEP]
intros
[GOAL]
α : Type ?u.110288
β : Type ?u.110291
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
n✝ : ℤ
⊢ ↑↑n✝ = ↑n✝
[PROOFSTEP]
rfl
[GOAL]
α : Type ?u.112041
β : Type ?u.112044
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : CauSeq β abv
n : ℕ
⊢ ∀ (i : ℕ), ↑(npowRec n f) i = ↑f i ^ n
[PROOFSTEP]
induction n
[GOAL]
case zero
α : Type ?u.112041
β : Type ?u.112044
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : CauSeq β abv
⊢ ∀ (i : ℕ), ↑(npowRec Nat.zero f) i = ↑f i ^ Nat.zero
[PROOFSTEP]
simp [*, npowRec, pow_succ]
[GOAL]
case succ
α : Type ?u.112041
β : Type ?u.112044
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : CauSeq β abv
n✝ : ℕ
n_ih✝ : ∀ (i : ℕ), ↑(npowRec n✝ f) i = ↑f i ^ n✝
⊢ ∀ (i : ℕ), ↑(npowRec (Nat.succ n✝) f) i = ↑f i ^ Nat.succ n✝
[PROOFSTEP]
simp [*, npowRec, pow_succ]
[GOAL]
α : Type ?u.120684
β✝ : Type ?u.120687
inst✝⁴ : LinearOrderedField α
inst✝³ : Ring β✝
abv✝ : β✝ → α
inst✝² : IsAbsoluteValue abv✝
β : Type u_1
inst✝¹ : CommRing β
abv : β → α
inst✝ : IsAbsoluteValue abv
src✝ : Ring (CauSeq β abv) := ring
a b : CauSeq β abv
n : ℕ
⊢ ↑(a * b) n = ↑(b * a) n
[PROOFSTEP]
simp [mul_left_comm, mul_comm]
[GOAL]
α : Type u_2
β : Type u_1
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f g : CauSeq β abv
hf : LimZero f
hg : LimZero g
ε : α
ε0 : ε > 0
i : ℕ
H : ∀ (j : ℕ), j ≥ i → abv (↑f j) < ε / 2 ∧ abv (↑g j) < ε / 2
j : ℕ
ij : j ≥ i
⊢ abv (↑(f + g) j) < ε
[PROOFSTEP]
let ⟨H₁, H₂⟩ := H _ ij
[GOAL]
α : Type u_2
β : Type u_1
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f g : CauSeq β abv
hf : LimZero f
hg : LimZero g
ε : α
ε0 : ε > 0
i : ℕ
H : ∀ (j : ℕ), j ≥ i → abv (↑f j) < ε / 2 ∧ abv (↑g j) < ε / 2
j : ℕ
ij : j ≥ i
H₁ : abv (↑f j) < ε / 2
H₂ : abv (↑g j) < ε / 2
⊢ abv (↑(f + g) j) < ε
[PROOFSTEP]
simpa [add_halves ε] using lt_of_le_of_lt (abv_add abv _ _) (add_lt_add H₁ H₂)
[GOAL]
α : Type u_2
β : Type u_1
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f g : CauSeq β abv
hg : LimZero g
ε : α
ε0 : ε > 0
F : α
F0 : F > 0
hF : ∀ (i : ℕ), abv (↑f i) < F
i : ℕ
H : ∀ (j : ℕ), j ≥ i → abv (↑g j) < ε / F
j : ℕ
ij : j ≥ i
⊢ abv (↑(f * g) j) < ε
[PROOFSTEP]
have := mul_lt_mul' (le_of_lt <| hF j) (H _ ij) (abv_nonneg abv _) F0
[GOAL]
α : Type u_2
β : Type u_1
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f g : CauSeq β abv
hg : LimZero g
ε : α
ε0 : ε > 0
F : α
F0 : F > 0
hF : ∀ (i : ℕ), abv (↑f i) < F
i : ℕ
H : ∀ (j : ℕ), j ≥ i → abv (↑g j) < ε / F
j : ℕ
ij : j ≥ i
this : abv (↑f j) * abv (↑g j) < F * (ε / F)
⊢ abv (↑(f * g) j) < ε
[PROOFSTEP]
rwa [mul_comm F, div_mul_cancel _ (ne_of_gt F0), ← abv_mul] at this 
[GOAL]
α : Type u_2
β : Type u_1
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f g : CauSeq β abv
hg : LimZero f
ε : α
ε0 : ε > 0
G : α
G0 : G > 0
hG : ∀ (i : ℕ), abv (↑g i) < G
i : ℕ
H : ∀ (j : ℕ), j ≥ i → abv (↑f j) < ε / G
j : ℕ
ij : j ≥ i
⊢ abv (↑(f * g) j) < ε
[PROOFSTEP]
have := mul_lt_mul'' (H _ ij) (hG j) (abv_nonneg abv _) (abv_nonneg abv _)
[GOAL]
α : Type u_2
β : Type u_1
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f g : CauSeq β abv
hg : LimZero f
ε : α
ε0 : ε > 0
G : α
G0 : G > 0
hG : ∀ (i : ℕ), abv (↑g i) < G
i : ℕ
H : ∀ (j : ℕ), j ≥ i → abv (↑f j) < ε / G
j : ℕ
ij : j ≥ i
this : abv (↑f j) * abv (↑g j) < ε / G * G
⊢ abv (↑(f * g) j) < ε
[PROOFSTEP]
rwa [div_mul_cancel _ (ne_of_gt G0), ← abv_mul] at this 
[GOAL]
α : Type u_2
β : Type u_1
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : CauSeq β abv
hf : LimZero f
⊢ LimZero (-f)
[PROOFSTEP]
rw [← neg_one_mul f]
[GOAL]
α : Type u_2
β : Type u_1
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : CauSeq β abv
hf : LimZero f
⊢ LimZero (-1 * f)
[PROOFSTEP]
exact mul_limZero_right _ hf
[GOAL]
α : Type u_2
β : Type u_1
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f g : CauSeq β abv
hf : LimZero f
hg : LimZero g
⊢ LimZero (f - g)
[PROOFSTEP]
simpa only [sub_eq_add_neg] using add_limZero hf (neg_limZero hg)
[GOAL]
α : Type u_2
β : Type u_1
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f g : CauSeq β abv
hfg : LimZero (f - g)
⊢ LimZero (g - f)
[PROOFSTEP]
simpa using neg_limZero hfg
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
ε : α
ε0 : ε > 0
j : ℕ
x✝ : j ≥ 0
⊢ abv (↑0 j) < ε
[PROOFSTEP]
simpa [abv_zero abv] using ε0
[GOAL]
α : Type ?u.134602
β : Type ?u.134605
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : CauSeq β abv
⊢ LimZero (f - f)
[PROOFSTEP]
simp [zero_limZero]
[GOAL]
α : Type ?u.134602
β : Type ?u.134605
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
x✝ y✝ : CauSeq β abv
f : LimZero (x✝ - y✝)
ε : α
hε : ε > 0
⊢ ∃ i, ∀ (j : ℕ), j ≥ i → abv (↑(y✝ - x✝) j) < ε
[PROOFSTEP]
simpa using neg_limZero f ε hε
[GOAL]
α : Type ?u.134602
β : Type ?u.134605
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
x✝ y✝ z✝ : CauSeq β abv
fg : LimZero (x✝ - y✝)
gh : LimZero (y✝ - z✝)
⊢ LimZero (x✝ - z✝)
[PROOFSTEP]
simpa using add_limZero fg gh
[GOAL]
α : Type u_2
β : Type u_1
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f1 f2 g1 g2 : CauSeq β abv
hf : f1 ≈ f2
hg : g1 ≈ g2
⊢ f1 + g1 ≈ f2 + g2
[PROOFSTEP]
simpa only [← add_sub_add_comm] using add_limZero hf hg
[GOAL]
α : Type u_2
β : Type u_1
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f g : CauSeq β abv
hf : f ≈ g
⊢ -f ≈ -g
[PROOFSTEP]
simpa only [neg_sub'] using neg_limZero hf
[GOAL]
α : Type u_2
β : Type u_1
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f1 f2 g1 g2 : CauSeq β abv
hf : f1 ≈ f2
hg : g1 ≈ g2
⊢ f1 - g1 ≈ f2 - g2
[PROOFSTEP]
simpa only [sub_eq_add_neg] using add_equiv_add hf (neg_equiv_neg hg)
[GOAL]
α : Type u_2
β : Type u_1
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f g : CauSeq β abv
h : f ≈ g
ε : α
ε0 : 0 < ε
i : ℕ
H : ∀ (j : ℕ), j ≥ i → abv (↑(f - g) j) < ε / 2 ∧ ∀ (k : ℕ), k ≥ j → abv (↑f k - ↑f j) < ε / 2
j : ℕ
ij : j ≥ i
k : ℕ
jk : k ≥ j
⊢ abv (↑f k - ↑g j) < ε
[PROOFSTEP]
let ⟨h₁, h₂⟩ := H _ ij
[GOAL]
α : Type u_2
β : Type u_1
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f g : CauSeq β abv
h : f ≈ g
ε : α
ε0 : 0 < ε
i : ℕ
H : ∀ (j : ℕ), j ≥ i → abv (↑(f - g) j) < ε / 2 ∧ ∀ (k : ℕ), k ≥ j → abv (↑f k - ↑f j) < ε / 2
j : ℕ
ij : j ≥ i
k : ℕ
jk : k ≥ j
h₁ : abv (↑(f - g) j) < ε / 2
h₂ : ∀ (k : ℕ), k ≥ j → abv (↑f k - ↑f j) < ε / 2
⊢ abv (↑f k - ↑g j) < ε
[PROOFSTEP]
have := lt_of_le_of_lt (abv_add abv (f j - g j) _) (add_lt_add h₁ (h₂ _ jk))
[GOAL]
α : Type u_2
β : Type u_1
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f g : CauSeq β abv
h : f ≈ g
ε : α
ε0 : 0 < ε
i : ℕ
H : ∀ (j : ℕ), j ≥ i → abv (↑(f - g) j) < ε / 2 ∧ ∀ (k : ℕ), k ≥ j → abv (↑f k - ↑f j) < ε / 2
j : ℕ
ij : j ≥ i
k : ℕ
jk : k ≥ j
h₁ : abv (↑(f - g) j) < ε / 2
h₂ : ∀ (k : ℕ), k ≥ j → abv (↑f k - ↑f j) < ε / 2
this : abv (↑f j - ↑g j + (↑f k - ↑f j)) < ε / 2 + ε / 2
⊢ abv (↑f k - ↑g j) < ε
[PROOFSTEP]
rwa [sub_add_sub_cancel', add_halves] at this 
[GOAL]
α : Type u_2
β : Type u_1
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f g : CauSeq β abv
h : f ≈ g
l : LimZero f
⊢ LimZero g
[PROOFSTEP]
simpa using add_limZero (Setoid.symm h) l
[GOAL]
α : Type u_2
β : Type u_1
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f g : CauSeq β abv
h : f ≈ g
l : LimZero g
⊢ LimZero f
[PROOFSTEP]
simpa using add_limZero h l
[GOAL]
α : Type u_2
β : Type u_1
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : CauSeq β abv
hf : ¬LimZero f
⊢ ∃ K, K > 0 ∧ ∃ i, ∀ (j : ℕ), j ≥ i → K ≤ abv (↑f j)
[PROOFSTEP]
haveI := Classical.propDecidable
[GOAL]
α : Type u_2
β : Type u_1
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : CauSeq β abv
hf : ¬LimZero f
this : (a : Prop) → Decidable a
⊢ ∃ K, K > 0 ∧ ∃ i, ∀ (j : ℕ), j ≥ i → K ≤ abv (↑f j)
[PROOFSTEP]
by_contra nk
[GOAL]
α : Type u_2
β : Type u_1
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : CauSeq β abv
hf : ¬LimZero f
this : (a : Prop) → Decidable a
nk : ¬∃ K, K > 0 ∧ ∃ i, ∀ (j : ℕ), j ≥ i → K ≤ abv (↑f j)
⊢ False
[PROOFSTEP]
refine' hf fun ε ε0 => _
[GOAL]
α : Type u_2
β : Type u_1
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : CauSeq β abv
hf : ¬LimZero f
this : (a : Prop) → Decidable a
nk : ¬∃ K, K > 0 ∧ ∃ i, ∀ (j : ℕ), j ≥ i → K ≤ abv (↑f j)
ε : α
ε0 : ε > 0
⊢ ∃ i, ∀ (j : ℕ), j ≥ i → abv (↑f j) < ε
[PROOFSTEP]
simp [not_forall] at nk 
[GOAL]
α : Type u_2
β : Type u_1
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : CauSeq β abv
hf : ¬LimZero f
this : (a : Prop) → Decidable a
ε : α
ε0 : ε > 0
nk : ∀ (x : α), 0 < x → ∀ (x_1 : ℕ), ∃ x_2, x_1 ≤ x_2 ∧ abv (↑f x_2) < x
⊢ ∃ i, ∀ (j : ℕ), j ≥ i → abv (↑f j) < ε
[PROOFSTEP]
cases' f.cauchy₃ (half_pos ε0) with i hi
[GOAL]
case intro
α : Type u_2
β : Type u_1
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : CauSeq β abv
hf : ¬LimZero f
this : (a : Prop) → Decidable a
ε : α
ε0 : ε > 0
nk : ∀ (x : α), 0 < x → ∀ (x_1 : ℕ), ∃ x_2, x_1 ≤ x_2 ∧ abv (↑f x_2) < x
i : ℕ
hi : ∀ (j : ℕ), j ≥ i → ∀ (k : ℕ), k ≥ j → abv (↑f k - ↑f j) < ε / 2
⊢ ∃ i, ∀ (j : ℕ), j ≥ i → abv (↑f j) < ε
[PROOFSTEP]
rcases nk _ (half_pos ε0) i with ⟨j, ij, hj⟩
[GOAL]
case intro.intro.intro
α : Type u_2
β : Type u_1
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : CauSeq β abv
hf : ¬LimZero f
this : (a : Prop) → Decidable a
ε : α
ε0 : ε > 0
nk : ∀ (x : α), 0 < x → ∀ (x_1 : ℕ), ∃ x_2, x_1 ≤ x_2 ∧ abv (↑f x_2) < x
i : ℕ
hi : ∀ (j : ℕ), j ≥ i → ∀ (k : ℕ), k ≥ j → abv (↑f k - ↑f j) < ε / 2
j : ℕ
ij : i ≤ j
hj : abv (↑f j) < ε / 2
⊢ ∃ i, ∀ (j : ℕ), j ≥ i → abv (↑f j) < ε
[PROOFSTEP]
refine' ⟨j, fun k jk => _⟩
[GOAL]
case intro.intro.intro
α : Type u_2
β : Type u_1
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : CauSeq β abv
hf : ¬LimZero f
this : (a : Prop) → Decidable a
ε : α
ε0 : ε > 0
nk : ∀ (x : α), 0 < x → ∀ (x_1 : ℕ), ∃ x_2, x_1 ≤ x_2 ∧ abv (↑f x_2) < x
i : ℕ
hi : ∀ (j : ℕ), j ≥ i → ∀ (k : ℕ), k ≥ j → abv (↑f k - ↑f j) < ε / 2
j : ℕ
ij : i ≤ j
hj : abv (↑f j) < ε / 2
k : ℕ
jk : k ≥ j
⊢ abv (↑f k) < ε
[PROOFSTEP]
have := lt_of_le_of_lt (abv_add abv _ _) (add_lt_add (hi j ij k jk) hj)
[GOAL]
case intro.intro.intro
α : Type u_2
β : Type u_1
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : CauSeq β abv
hf : ¬LimZero f
this✝ : (a : Prop) → Decidable a
ε : α
ε0 : ε > 0
nk : ∀ (x : α), 0 < x → ∀ (x_1 : ℕ), ∃ x_2, x_1 ≤ x_2 ∧ abv (↑f x_2) < x
i : ℕ
hi : ∀ (j : ℕ), j ≥ i → ∀ (k : ℕ), k ≥ j → abv (↑f k - ↑f j) < ε / 2
j : ℕ
ij : i ≤ j
hj : abv (↑f j) < ε / 2
k : ℕ
jk : k ≥ j
this : abv (↑f k - ↑f j + ↑f j) < ε / 2 + ε / 2
⊢ abv (↑f k) < ε
[PROOFSTEP]
rwa [sub_add_cancel, add_halves] at this 
[GOAL]
α : Type u_2
β : Type u_1
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → β
g : CauSeq β abv
h : ∀ (ε : α), ε > 0 → ∃ i, ∀ (j : ℕ), j ≥ i → abv (f j - ↑g j) < ε
ε : α
ε0 : ε > 0
i : ℕ
hi : ∀ (j : ℕ), j ≥ i → abv (f j - ↑g j) < ε / 2 / 2 ∧ ∀ (k : ℕ), k ≥ j → abv (↑g k - ↑g j) < ε / 2
j : ℕ
ij : j ≥ i
⊢ abv (f j - f i) < ε
[PROOFSTEP]
cases' hi _ le_rfl with h₁ h₂
[GOAL]
case intro
α : Type u_2
β : Type u_1
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → β
g : CauSeq β abv
h : ∀ (ε : α), ε > 0 → ∃ i, ∀ (j : ℕ), j ≥ i → abv (f j - ↑g j) < ε
ε : α
ε0 : ε > 0
i : ℕ
hi : ∀ (j : ℕ), j ≥ i → abv (f j - ↑g j) < ε / 2 / 2 ∧ ∀ (k : ℕ), k ≥ j → abv (↑g k - ↑g j) < ε / 2
j : ℕ
ij : j ≥ i
h₁ : abv (f i - ↑g i) < ε / 2 / 2
h₂ : ∀ (k : ℕ), k ≥ i → abv (↑g k - ↑g i) < ε / 2
⊢ abv (f j - f i) < ε
[PROOFSTEP]
rw [abv_sub abv] at h₁ 
[GOAL]
case intro
α : Type u_2
β : Type u_1
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → β
g : CauSeq β abv
h : ∀ (ε : α), ε > 0 → ∃ i, ∀ (j : ℕ), j ≥ i → abv (f j - ↑g j) < ε
ε : α
ε0 : ε > 0
i : ℕ
hi : ∀ (j : ℕ), j ≥ i → abv (f j - ↑g j) < ε / 2 / 2 ∧ ∀ (k : ℕ), k ≥ j → abv (↑g k - ↑g j) < ε / 2
j : ℕ
ij : j ≥ i
h₁ : abv (↑g i - f i) < ε / 2 / 2
h₂ : ∀ (k : ℕ), k ≥ i → abv (↑g k - ↑g i) < ε / 2
⊢ abv (f j - f i) < ε
[PROOFSTEP]
have := lt_of_le_of_lt (abv_add abv _ _) (add_lt_add (hi _ ij).1 h₁)
[GOAL]
case intro
α : Type u_2
β : Type u_1
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → β
g : CauSeq β abv
h : ∀ (ε : α), ε > 0 → ∃ i, ∀ (j : ℕ), j ≥ i → abv (f j - ↑g j) < ε
ε : α
ε0 : ε > 0
i : ℕ
hi : ∀ (j : ℕ), j ≥ i → abv (f j - ↑g j) < ε / 2 / 2 ∧ ∀ (k : ℕ), k ≥ j → abv (↑g k - ↑g j) < ε / 2
j : ℕ
ij : j ≥ i
h₁ : abv (↑g i - f i) < ε / 2 / 2
h₂ : ∀ (k : ℕ), k ≥ i → abv (↑g k - ↑g i) < ε / 2
this : abv (f j - ↑g j + (↑g i - f i)) < ε / 2 / 2 + ε / 2 / 2
⊢ abv (f j - f i) < ε
[PROOFSTEP]
have := lt_of_le_of_lt (abv_add abv _ _) (add_lt_add this (h₂ _ ij))
[GOAL]
case intro
α : Type u_2
β : Type u_1
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → β
g : CauSeq β abv
h : ∀ (ε : α), ε > 0 → ∃ i, ∀ (j : ℕ), j ≥ i → abv (f j - ↑g j) < ε
ε : α
ε0 : ε > 0
i : ℕ
hi : ∀ (j : ℕ), j ≥ i → abv (f j - ↑g j) < ε / 2 / 2 ∧ ∀ (k : ℕ), k ≥ j → abv (↑g k - ↑g j) < ε / 2
j : ℕ
ij : j ≥ i
h₁ : abv (↑g i - f i) < ε / 2 / 2
h₂ : ∀ (k : ℕ), k ≥ i → abv (↑g k - ↑g i) < ε / 2
this✝ : abv (f j - ↑g j + (↑g i - f i)) < ε / 2 / 2 + ε / 2 / 2
this : abv (f j - ↑g j + (↑g i - f i) + (↑g j - ↑g i)) < ε / 2 / 2 + ε / 2 / 2 + ε / 2
⊢ abv (f j - f i) < ε
[PROOFSTEP]
rwa [add_halves, add_halves, add_right_comm, sub_add_sub_cancel, sub_add_sub_cancel] at this 
[GOAL]
α : Type u_2
β : Type u_1
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : CauSeq β abv
hf : ¬f ≈ 0
⊢ ¬LimZero f
[PROOFSTEP]
intro h
[GOAL]
α : Type u_2
β : Type u_1
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : CauSeq β abv
hf : ¬f ≈ 0
h : LimZero f
⊢ False
[PROOFSTEP]
have : LimZero (f - 0) := by simp [h]
[GOAL]
α : Type u_2
β : Type u_1
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : CauSeq β abv
hf : ¬f ≈ 0
h : LimZero f
⊢ LimZero (f - 0)
[PROOFSTEP]
simp [h]
[GOAL]
α : Type u_2
β : Type u_1
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : CauSeq β abv
hf : ¬f ≈ 0
h : LimZero f
this : LimZero (f - 0)
⊢ False
[PROOFSTEP]
exact hf this
[GOAL]
α : Type u_2
β : Type u_1
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
g f : CauSeq β abv
hf : f ≈ 0
this : LimZero (f - 0)
⊢ LimZero f
[PROOFSTEP]
simpa
[GOAL]
α : Type u_2
β : Type u_1
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
g f : CauSeq β abv
hf : f ≈ 0
this✝ : LimZero (f - 0)
this : LimZero (g * f)
⊢ LimZero (g * f - 0)
[PROOFSTEP]
simpa
[GOAL]
α : Type u_2
β : Type u_1
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
g f : CauSeq β abv
hf : f ≈ 0
this : LimZero (f - 0)
⊢ LimZero f
[PROOFSTEP]
simpa
[GOAL]
α : Type u_2
β : Type u_1
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
g f : CauSeq β abv
hf : f ≈ 0
this✝ : LimZero (f - 0)
this : LimZero (f * g)
⊢ LimZero (f * g - 0)
[PROOFSTEP]
simpa
[GOAL]
α : Type u_2
β : Type u_1
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f g : CauSeq β abv
hf : ¬f ≈ 0
hg : ¬g ≈ 0
this : LimZero (f * g - 0)
⊢ False
[PROOFSTEP]
have hlz : LimZero (f * g) := by simpa
[GOAL]
α : Type u_2
β : Type u_1
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f g : CauSeq β abv
hf : ¬f ≈ 0
hg : ¬g ≈ 0
this : LimZero (f * g - 0)
⊢ LimZero (f * g)
[PROOFSTEP]
simpa
[GOAL]
α : Type u_2
β : Type u_1
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f g : CauSeq β abv
hf : ¬f ≈ 0
hg : ¬g ≈ 0
this : LimZero (f * g - 0)
hlz : LimZero (f * g)
⊢ False
[PROOFSTEP]
have hf' : ¬LimZero f := by simpa using show ¬LimZero (f - 0) from hf
[GOAL]
α : Type u_2
β : Type u_1
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f g : CauSeq β abv
hf : ¬f ≈ 0
hg : ¬g ≈ 0
this : LimZero (f * g - 0)
hlz : LimZero (f * g)
⊢ ¬LimZero f
[PROOFSTEP]
simpa using show ¬LimZero (f - 0) from hf
[GOAL]
α : Type u_2
β : Type u_1
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f g : CauSeq β abv
hf : ¬f ≈ 0
hg : ¬g ≈ 0
this : LimZero (f * g - 0)
hlz : LimZero (f * g)
hf' : ¬LimZero f
⊢ False
[PROOFSTEP]
have hg' : ¬LimZero g := by simpa using show ¬LimZero (g - 0) from hg
[GOAL]
α : Type u_2
β : Type u_1
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f g : CauSeq β abv
hf : ¬f ≈ 0
hg : ¬g ≈ 0
this : LimZero (f * g - 0)
hlz : LimZero (f * g)
hf' : ¬LimZero f
⊢ ¬LimZero g
[PROOFSTEP]
simpa using show ¬LimZero (g - 0) from hg
[GOAL]
α : Type u_2
β : Type u_1
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f g : CauSeq β abv
hf : ¬f ≈ 0
hg : ¬g ≈ 0
this : LimZero (f * g - 0)
hlz : LimZero (f * g)
hf' : ¬LimZero f
hg' : ¬LimZero g
⊢ False
[PROOFSTEP]
rcases abv_pos_of_not_limZero hf' with ⟨a1, ha1, N1, hN1⟩
[GOAL]
case intro.intro.intro
α : Type u_2
β : Type u_1
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f g : CauSeq β abv
hf : ¬f ≈ 0
hg : ¬g ≈ 0
this : LimZero (f * g - 0)
hlz : LimZero (f * g)
hf' : ¬LimZero f
hg' : ¬LimZero g
a1 : α
ha1 : a1 > 0
N1 : ℕ
hN1 : ∀ (j : ℕ), j ≥ N1 → a1 ≤ abv (↑f j)
⊢ False
[PROOFSTEP]
rcases abv_pos_of_not_limZero hg' with ⟨a2, ha2, N2, hN2⟩
[GOAL]
case intro.intro.intro.intro.intro.intro
α : Type u_2
β : Type u_1
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f g : CauSeq β abv
hf : ¬f ≈ 0
hg : ¬g ≈ 0
this : LimZero (f * g - 0)
hlz : LimZero (f * g)
hf' : ¬LimZero f
hg' : ¬LimZero g
a1 : α
ha1 : a1 > 0
N1 : ℕ
hN1 : ∀ (j : ℕ), j ≥ N1 → a1 ≤ abv (↑f j)
a2 : α
ha2 : a2 > 0
N2 : ℕ
hN2 : ∀ (j : ℕ), j ≥ N2 → a2 ≤ abv (↑g j)
⊢ False
[PROOFSTEP]
have : 0 < a1 * a2 := mul_pos ha1 ha2
[GOAL]
case intro.intro.intro.intro.intro.intro
α : Type u_2
β : Type u_1
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f g : CauSeq β abv
hf : ¬f ≈ 0
hg : ¬g ≈ 0
this✝ : LimZero (f * g - 0)
hlz : LimZero (f * g)
hf' : ¬LimZero f
hg' : ¬LimZero g
a1 : α
ha1 : a1 > 0
N1 : ℕ
hN1 : ∀ (j : ℕ), j ≥ N1 → a1 ≤ abv (↑f j)
a2 : α
ha2 : a2 > 0
N2 : ℕ
hN2 : ∀ (j : ℕ), j ≥ N2 → a2 ≤ abv (↑g j)
this : 0 < a1 * a2
⊢ False
[PROOFSTEP]
cases' hlz _ this with N hN
[GOAL]
case intro.intro.intro.intro.intro.intro.intro
α : Type u_2
β : Type u_1
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f g : CauSeq β abv
hf : ¬f ≈ 0
hg : ¬g ≈ 0
this✝ : LimZero (f * g - 0)
hlz : LimZero (f * g)
hf' : ¬LimZero f
hg' : ¬LimZero g
a1 : α
ha1 : a1 > 0
N1 : ℕ
hN1 : ∀ (j : ℕ), j ≥ N1 → a1 ≤ abv (↑f j)
a2 : α
ha2 : a2 > 0
N2 : ℕ
hN2 : ∀ (j : ℕ), j ≥ N2 → a2 ≤ abv (↑g j)
this : 0 < a1 * a2
N : ℕ
hN : ∀ (j : ℕ), j ≥ N → abv (↑(f * g) j) < a1 * a2
⊢ False
[PROOFSTEP]
let i := max N (max N1 N2)
[GOAL]
case intro.intro.intro.intro.intro.intro.intro
α : Type u_2
β : Type u_1
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f g : CauSeq β abv
hf : ¬f ≈ 0
hg : ¬g ≈ 0
this✝ : LimZero (f * g - 0)
hlz : LimZero (f * g)
hf' : ¬LimZero f
hg' : ¬LimZero g
a1 : α
ha1 : a1 > 0
N1 : ℕ
hN1 : ∀ (j : ℕ), j ≥ N1 → a1 ≤ abv (↑f j)
a2 : α
ha2 : a2 > 0
N2 : ℕ
hN2 : ∀ (j : ℕ), j ≥ N2 → a2 ≤ abv (↑g j)
this : 0 < a1 * a2
N : ℕ
hN : ∀ (j : ℕ), j ≥ N → abv (↑(f * g) j) < a1 * a2
i : ℕ := max N (max N1 N2)
⊢ False
[PROOFSTEP]
have hN' := hN i (le_max_left _ _)
[GOAL]
case intro.intro.intro.intro.intro.intro.intro
α : Type u_2
β : Type u_1
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f g : CauSeq β abv
hf : ¬f ≈ 0
hg : ¬g ≈ 0
this✝ : LimZero (f * g - 0)
hlz : LimZero (f * g)
hf' : ¬LimZero f
hg' : ¬LimZero g
a1 : α
ha1 : a1 > 0
N1 : ℕ
hN1 : ∀ (j : ℕ), j ≥ N1 → a1 ≤ abv (↑f j)
a2 : α
ha2 : a2 > 0
N2 : ℕ
hN2 : ∀ (j : ℕ), j ≥ N2 → a2 ≤ abv (↑g j)
this : 0 < a1 * a2
N : ℕ
hN : ∀ (j : ℕ), j ≥ N → abv (↑(f * g) j) < a1 * a2
i : ℕ := max N (max N1 N2)
hN' : abv (↑(f * g) i) < a1 * a2
⊢ False
[PROOFSTEP]
have hN1' := hN1 i (le_trans (le_max_left _ _) (le_max_right _ _))
[GOAL]
case intro.intro.intro.intro.intro.intro.intro
α : Type u_2
β : Type u_1
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f g : CauSeq β abv
hf : ¬f ≈ 0
hg : ¬g ≈ 0
this✝ : LimZero (f * g - 0)
hlz : LimZero (f * g)
hf' : ¬LimZero f
hg' : ¬LimZero g
a1 : α
ha1 : a1 > 0
N1 : ℕ
hN1 : ∀ (j : ℕ), j ≥ N1 → a1 ≤ abv (↑f j)
a2 : α
ha2 : a2 > 0
N2 : ℕ
hN2 : ∀ (j : ℕ), j ≥ N2 → a2 ≤ abv (↑g j)
this : 0 < a1 * a2
N : ℕ
hN : ∀ (j : ℕ), j ≥ N → abv (↑(f * g) j) < a1 * a2
i : ℕ := max N (max N1 N2)
hN' : abv (↑(f * g) i) < a1 * a2
hN1' : a1 ≤ abv (↑f i)
⊢ False
[PROOFSTEP]
have hN1' := hN2 i (le_trans (le_max_right _ _) (le_max_right _ _))
[GOAL]
case intro.intro.intro.intro.intro.intro.intro
α : Type u_2
β : Type u_1
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f g : CauSeq β abv
hf : ¬f ≈ 0
hg : ¬g ≈ 0
this✝ : LimZero (f * g - 0)
hlz : LimZero (f * g)
hf' : ¬LimZero f
hg' : ¬LimZero g
a1 : α
ha1 : a1 > 0
N1 : ℕ
hN1 : ∀ (j : ℕ), j ≥ N1 → a1 ≤ abv (↑f j)
a2 : α
ha2 : a2 > 0
N2 : ℕ
hN2 : ∀ (j : ℕ), j ≥ N2 → a2 ≤ abv (↑g j)
this : 0 < a1 * a2
N : ℕ
hN : ∀ (j : ℕ), j ≥ N → abv (↑(f * g) j) < a1 * a2
i : ℕ := max N (max N1 N2)
hN' : abv (↑(f * g) i) < a1 * a2
hN1'✝ : a1 ≤ abv (↑f i)
hN1' : a2 ≤ abv (↑g i)
⊢ False
[PROOFSTEP]
apply not_le_of_lt hN'
[GOAL]
case intro.intro.intro.intro.intro.intro.intro
α : Type u_2
β : Type u_1
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f g : CauSeq β abv
hf : ¬f ≈ 0
hg : ¬g ≈ 0
this✝ : LimZero (f * g - 0)
hlz : LimZero (f * g)
hf' : ¬LimZero f
hg' : ¬LimZero g
a1 : α
ha1 : a1 > 0
N1 : ℕ
hN1 : ∀ (j : ℕ), j ≥ N1 → a1 ≤ abv (↑f j)
a2 : α
ha2 : a2 > 0
N2 : ℕ
hN2 : ∀ (j : ℕ), j ≥ N2 → a2 ≤ abv (↑g j)
this : 0 < a1 * a2
N : ℕ
hN : ∀ (j : ℕ), j ≥ N → abv (↑(f * g) j) < a1 * a2
i : ℕ := max N (max N1 N2)
hN' : abv (↑(f * g) i) < a1 * a2
hN1'✝ : a1 ≤ abv (↑f i)
hN1' : a2 ≤ abv (↑g i)
⊢ a1 * a2 ≤ abv (↑(f * g) i)
[PROOFSTEP]
change _ ≤ abv (_ * _)
[GOAL]
case intro.intro.intro.intro.intro.intro.intro
α : Type u_2
β : Type u_1
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f g : CauSeq β abv
hf : ¬f ≈ 0
hg : ¬g ≈ 0
this✝ : LimZero (f * g - 0)
hlz : LimZero (f * g)
hf' : ¬LimZero f
hg' : ¬LimZero g
a1 : α
ha1 : a1 > 0
N1 : ℕ
hN1 : ∀ (j : ℕ), j ≥ N1 → a1 ≤ abv (↑f j)
a2 : α
ha2 : a2 > 0
N2 : ℕ
hN2 : ∀ (j : ℕ), j ≥ N2 → a2 ≤ abv (↑g j)
this : 0 < a1 * a2
N : ℕ
hN : ∀ (j : ℕ), j ≥ N → abv (↑(f * g) j) < a1 * a2
i : ℕ := max N (max N1 N2)
hN' : abv (↑(f * g) i) < a1 * a2
hN1'✝ : a1 ≤ abv (↑f i)
hN1' : a2 ≤ abv (↑g i)
⊢ a1 * a2 ≤ abv (↑f i * ↑g i)
[PROOFSTEP]
rw [abv_mul abv]
[GOAL]
case intro.intro.intro.intro.intro.intro.intro
α : Type u_2
β : Type u_1
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f g : CauSeq β abv
hf : ¬f ≈ 0
hg : ¬g ≈ 0
this✝ : LimZero (f * g - 0)
hlz : LimZero (f * g)
hf' : ¬LimZero f
hg' : ¬LimZero g
a1 : α
ha1 : a1 > 0
N1 : ℕ
hN1 : ∀ (j : ℕ), j ≥ N1 → a1 ≤ abv (↑f j)
a2 : α
ha2 : a2 > 0
N2 : ℕ
hN2 : ∀ (j : ℕ), j ≥ N2 → a2 ≤ abv (↑g j)
this : 0 < a1 * a2
N : ℕ
hN : ∀ (j : ℕ), j ≥ N → abv (↑(f * g) j) < a1 * a2
i : ℕ := max N (max N1 N2)
hN' : abv (↑(f * g) i) < a1 * a2
hN1'✝ : a1 ≤ abv (↑f i)
hN1' : a2 ≤ abv (↑g i)
⊢ a1 * a2 ≤ abv (↑f i) * abv (↑g i)
[PROOFSTEP]
gcongr
[GOAL]
α : Type u_2
β : Type u_1
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
x y : β
⊢ LimZero (const x - const y) ↔ x = y
[PROOFSTEP]
rw [← const_sub, const_limZero, sub_eq_zero]
[GOAL]
α : Type u_2
β : Type u_1
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f1 f2 g1 g2 : CauSeq β abv
hf : f1 ≈ f2
hg : g1 ≈ g2
⊢ f1 * g1 ≈ f2 * g2
[PROOFSTEP]
change LimZero (f1 * g1 - f2 * g2)
[GOAL]
α : Type u_2
β : Type u_1
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f1 f2 g1 g2 : CauSeq β abv
hf : f1 ≈ f2
hg : g1 ≈ g2
⊢ LimZero (f1 * g1 - f2 * g2)
[PROOFSTEP]
convert add_limZero (mul_limZero_left g1 hf) (mul_limZero_right f2 hg) using 1
[GOAL]
case h.e'_6
α : Type u_2
β : Type u_1
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f1 f2 g1 g2 : CauSeq β abv
hf : f1 ≈ f2
hg : g1 ≈ g2
⊢ f1 * g1 - f2 * g2 = (f1 - f2) * g1 + f2 * (g1 - g2)
[PROOFSTEP]
rw [mul_sub, sub_mul]
  -- Porting note: doesn't work with `rw`, but did in Lean 3
[GOAL]
case h.e'_6
α : Type u_2
β : Type u_1
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f1 f2 g1 g2 : CauSeq β abv
hf : f1 ≈ f2
hg : g1 ≈ g2
⊢ f1 * g1 - f2 * g2 = f1 * g1 - f2 * g1 + (f2 * g1 - f2 * g2)
[PROOFSTEP]
exact (sub_add_sub_cancel (f1 * g1) (f2 * g1) (f2 * g2)).symm
[GOAL]
α : Type u_3
β : Type u_2
inst✝⁴ : LinearOrderedField α
inst✝³ : Ring β
abv : β → α
inst✝² : IsAbsoluteValue abv
G : Type u_1
inst✝¹ : SMul G β
inst✝ : IsScalarTower G β β
f1 f2 : CauSeq β abv
c : G
hf : f1 ≈ f2
⊢ c • f1 ≈ c • f2
[PROOFSTEP]
simpa [const_smul, smul_one_mul _ _] using mul_equiv_mul (const_equiv.mpr <| Eq.refl <| c • (1 : β)) hf
[GOAL]
α : Type u_2
β : Type u_1
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f1 f2 : CauSeq β abv
hf : f1 ≈ f2
n : ℕ
⊢ f1 ^ n ≈ f2 ^ n
[PROOFSTEP]
induction' n with n ih
[GOAL]
case zero
α : Type u_2
β : Type u_1
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f1 f2 : CauSeq β abv
hf : f1 ≈ f2
⊢ f1 ^ Nat.zero ≈ f2 ^ Nat.zero
[PROOFSTEP]
simp only [Nat.zero_eq, pow_zero, Setoid.refl]
[GOAL]
case succ
α : Type u_2
β : Type u_1
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f1 f2 : CauSeq β abv
hf : f1 ≈ f2
n : ℕ
ih : f1 ^ n ≈ f2 ^ n
⊢ f1 ^ Nat.succ n ≈ f2 ^ Nat.succ n
[PROOFSTEP]
simpa only [pow_succ] using mul_equiv_mul hf ih
[GOAL]
α : Type u_2
β : Type u_1
inst✝³ : LinearOrderedField α
inst✝² : Ring β
inst✝¹ : IsDomain β
abv : β → α
inst✝ : IsAbsoluteValue abv
h : const abv 1 ≈ const abv 0
this : ∀ (ε : α), ε > 0 → ∃ i, ∀ (k : ℕ), i ≤ k → abv (1 - 0) < ε
h2 : 0 < abv 1
i : ℕ
hi : ∀ (k : ℕ), i ≤ k → abv (1 - 0) < abv 1
⊢ abv 1 < abv 1
[PROOFSTEP]
simpa using hi _ le_rfl
[GOAL]
α : Type u_2
β : Type u_1
inst✝² : LinearOrderedField α
inst✝¹ : DivisionRing β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : CauSeq β abv
hf : ¬LimZero f
ε : α
ε0 : ε > 0
K : α
K0 : K > 0
i : ℕ
H : ∀ (j : ℕ), j ≥ i → K ≤ abv (↑f j)
j : ℕ
ij : j ≥ i
⊢ abv (↑(inv f hf * f - 1) j) < ε
[PROOFSTEP]
simpa [(abv_pos abv).1 (lt_of_lt_of_le K0 (H _ ij)), abv_zero abv] using ε0
[GOAL]
α : Type u_2
β : Type u_1
inst✝² : LinearOrderedField α
inst✝¹ : DivisionRing β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : CauSeq β abv
hf : ¬LimZero f
ε : α
ε0 : ε > 0
K : α
K0 : K > 0
i : ℕ
H : ∀ (j : ℕ), j ≥ i → K ≤ abv (↑f j)
j : ℕ
ij : j ≥ i
⊢ abv (↑(f * inv f hf - 1) j) < ε
[PROOFSTEP]
simpa [(abv_pos abv).1 (lt_of_lt_of_le K0 (H _ ij)), abv_zero abv] using ε0
[GOAL]
α : Type ?u.200476
β : Type ?u.200479
inst✝² : LinearOrderedField α
inst✝¹ : DivisionRing β
abv : β → α
inst✝ : IsAbsoluteValue abv
x : β
hx : x ≠ 0
⊢ ¬LimZero (const abv x)
[PROOFSTEP]
rwa [const_limZero]
[GOAL]
α : Type u_1
inst✝ : LinearOrderedField α
f g : CauSeq α abs
F : α
F0 : F > 0
hF : ∃ i, ∀ (j : ℕ), j ≥ i → F ≤ ↑f j
H : LimZero g
i : ℕ
h : ∀ (j : ℕ), j ≥ i → F ≤ ↑f j ∧ |↑g j| < F / 2
j : ℕ
ij : j ≥ i
⊢ F / 2 ≤ ↑(f + g) j
[PROOFSTEP]
cases' h j ij with h₁ h₂
[GOAL]
case intro
α : Type u_1
inst✝ : LinearOrderedField α
f g : CauSeq α abs
F : α
F0 : F > 0
hF : ∃ i, ∀ (j : ℕ), j ≥ i → F ≤ ↑f j
H : LimZero g
i : ℕ
h : ∀ (j : ℕ), j ≥ i → F ≤ ↑f j ∧ |↑g j| < F / 2
j : ℕ
ij : j ≥ i
h₁ : F ≤ ↑f j
h₂ : |↑g j| < F / 2
⊢ F / 2 ≤ ↑(f + g) j
[PROOFSTEP]
have := add_le_add h₁ (le_of_lt (abs_lt.1 h₂).1)
[GOAL]
case intro
α : Type u_1
inst✝ : LinearOrderedField α
f g : CauSeq α abs
F : α
F0 : F > 0
hF : ∃ i, ∀ (j : ℕ), j ≥ i → F ≤ ↑f j
H : LimZero g
i : ℕ
h : ∀ (j : ℕ), j ≥ i → F ≤ ↑f j ∧ |↑g j| < F / 2
j : ℕ
ij : j ≥ i
h₁ : F ≤ ↑f j
h₂ : |↑g j| < F / 2
this : F + -(F / 2) ≤ ↑f j + ↑g j
⊢ F / 2 ≤ ↑(f + g) j
[PROOFSTEP]
rwa [← sub_eq_add_neg, sub_self_div_two] at this 
[GOAL]
α : Type u_1
inst✝ : LinearOrderedField α
f : CauSeq α abs
⊢ Pos f ∨ LimZero f ∨ Pos (-f)
[PROOFSTEP]
cases' Classical.em (LimZero f) with h h
[GOAL]
case inl
α : Type u_1
inst✝ : LinearOrderedField α
f : CauSeq α abs
h : LimZero f
⊢ Pos f ∨ LimZero f ∨ Pos (-f)
[PROOFSTEP]
simp [*]
[GOAL]
case inr
α : Type u_1
inst✝ : LinearOrderedField α
f : CauSeq α abs
h : ¬LimZero f
⊢ Pos f ∨ LimZero f ∨ Pos (-f)
[PROOFSTEP]
simp [*]
[GOAL]
case inr
α : Type u_1
inst✝ : LinearOrderedField α
f : CauSeq α abs
h : ¬LimZero f
⊢ Pos f ∨ Pos (-f)
[PROOFSTEP]
rcases abv_pos_of_not_limZero h with ⟨K, K0, hK⟩
[GOAL]
case inr.intro.intro
α : Type u_1
inst✝ : LinearOrderedField α
f : CauSeq α abs
h : ¬LimZero f
K : α
K0 : K > 0
hK : ∃ i, ∀ (j : ℕ), j ≥ i → K ≤ |↑f j|
⊢ Pos f ∨ Pos (-f)
[PROOFSTEP]
rcases exists_forall_ge_and hK (f.cauchy₃ K0) with ⟨i, hi⟩
[GOAL]
case inr.intro.intro.intro
α : Type u_1
inst✝ : LinearOrderedField α
f : CauSeq α abs
h : ¬LimZero f
K : α
K0 : K > 0
hK : ∃ i, ∀ (j : ℕ), j ≥ i → K ≤ |↑f j|
i : ℕ
hi : ∀ (j : ℕ), j ≥ i → K ≤ |↑f j| ∧ ∀ (k : ℕ), k ≥ j → |↑f k - ↑f j| < K
⊢ Pos f ∨ Pos (-f)
[PROOFSTEP]
refine' (le_total 0 (f i)).imp _ _
[GOAL]
case inr.intro.intro.intro.refine'_1
α : Type u_1
inst✝ : LinearOrderedField α
f : CauSeq α abs
h : ¬LimZero f
K : α
K0 : K > 0
hK : ∃ i, ∀ (j : ℕ), j ≥ i → K ≤ |↑f j|
i : ℕ
hi : ∀ (j : ℕ), j ≥ i → K ≤ |↑f j| ∧ ∀ (k : ℕ), k ≥ j → |↑f k - ↑f j| < K
⊢ 0 ≤ ↑f i → Pos f
[PROOFSTEP]
refine' fun h => ⟨K, K0, i, fun j ij => _⟩
[GOAL]
case inr.intro.intro.intro.refine'_2
α : Type u_1
inst✝ : LinearOrderedField α
f : CauSeq α abs
h : ¬LimZero f
K : α
K0 : K > 0
hK : ∃ i, ∀ (j : ℕ), j ≥ i → K ≤ |↑f j|
i : ℕ
hi : ∀ (j : ℕ), j ≥ i → K ≤ |↑f j| ∧ ∀ (k : ℕ), k ≥ j → |↑f k - ↑f j| < K
⊢ ↑f i ≤ 0 → Pos (-f)
[PROOFSTEP]
refine' fun h => ⟨K, K0, i, fun j ij => _⟩
[GOAL]
case inr.intro.intro.intro.refine'_1
α : Type u_1
inst✝ : LinearOrderedField α
f : CauSeq α abs
h✝ : ¬LimZero f
K : α
K0 : K > 0
hK : ∃ i, ∀ (j : ℕ), j ≥ i → K ≤ |↑f j|
i : ℕ
hi : ∀ (j : ℕ), j ≥ i → K ≤ |↑f j| ∧ ∀ (k : ℕ), k ≥ j → |↑f k - ↑f j| < K
h : 0 ≤ ↑f i
j : ℕ
ij : j ≥ i
⊢ K ≤ ↑f j
[PROOFSTEP]
have := (hi _ ij).1
[GOAL]
case inr.intro.intro.intro.refine'_2
α : Type u_1
inst✝ : LinearOrderedField α
f : CauSeq α abs
h✝ : ¬LimZero f
K : α
K0 : K > 0
hK : ∃ i, ∀ (j : ℕ), j ≥ i → K ≤ |↑f j|
i : ℕ
hi : ∀ (j : ℕ), j ≥ i → K ≤ |↑f j| ∧ ∀ (k : ℕ), k ≥ j → |↑f k - ↑f j| < K
h : ↑f i ≤ 0
j : ℕ
ij : j ≥ i
⊢ K ≤ ↑(-f) j
[PROOFSTEP]
have := (hi _ ij).1
[GOAL]
case inr.intro.intro.intro.refine'_1
α : Type u_1
inst✝ : LinearOrderedField α
f : CauSeq α abs
h✝ : ¬LimZero f
K : α
K0 : K > 0
hK : ∃ i, ∀ (j : ℕ), j ≥ i → K ≤ |↑f j|
i : ℕ
hi : ∀ (j : ℕ), j ≥ i → K ≤ |↑f j| ∧ ∀ (k : ℕ), k ≥ j → |↑f k - ↑f j| < K
h : 0 ≤ ↑f i
j : ℕ
ij : j ≥ i
this : K ≤ |↑f j|
⊢ K ≤ ↑f j
[PROOFSTEP]
cases' hi _ le_rfl with h₁ h₂
[GOAL]
case inr.intro.intro.intro.refine'_2
α : Type u_1
inst✝ : LinearOrderedField α
f : CauSeq α abs
h✝ : ¬LimZero f
K : α
K0 : K > 0
hK : ∃ i, ∀ (j : ℕ), j ≥ i → K ≤ |↑f j|
i : ℕ
hi : ∀ (j : ℕ), j ≥ i → K ≤ |↑f j| ∧ ∀ (k : ℕ), k ≥ j → |↑f k - ↑f j| < K
h : ↑f i ≤ 0
j : ℕ
ij : j ≥ i
this : K ≤ |↑f j|
⊢ K ≤ ↑(-f) j
[PROOFSTEP]
cases' hi _ le_rfl with h₁ h₂
[GOAL]
case inr.intro.intro.intro.refine'_1.intro
α : Type u_1
inst✝ : LinearOrderedField α
f : CauSeq α abs
h✝ : ¬LimZero f
K : α
K0 : K > 0
hK : ∃ i, ∀ (j : ℕ), j ≥ i → K ≤ |↑f j|
i : ℕ
hi : ∀ (j : ℕ), j ≥ i → K ≤ |↑f j| ∧ ∀ (k : ℕ), k ≥ j → |↑f k - ↑f j| < K
h : 0 ≤ ↑f i
j : ℕ
ij : j ≥ i
this : K ≤ |↑f j|
h₁ : K ≤ |↑f i|
h₂ : ∀ (k : ℕ), k ≥ i → |↑f k - ↑f i| < K
⊢ K ≤ ↑f j
[PROOFSTEP]
rwa [abs_of_nonneg] at this 
[GOAL]
case inr.intro.intro.intro.refine'_1.intro
α : Type u_1
inst✝ : LinearOrderedField α
f : CauSeq α abs
h✝ : ¬LimZero f
K : α
K0 : K > 0
hK : ∃ i, ∀ (j : ℕ), j ≥ i → K ≤ |↑f j|
i : ℕ
hi : ∀ (j : ℕ), j ≥ i → K ≤ |↑f j| ∧ ∀ (k : ℕ), k ≥ j → |↑f k - ↑f j| < K
h : 0 ≤ ↑f i
j : ℕ
ij : j ≥ i
this : K ≤ |↑f j|
h₁ : K ≤ |↑f i|
h₂ : ∀ (k : ℕ), k ≥ i → |↑f k - ↑f i| < K
⊢ 0 ≤ ↑f j
[PROOFSTEP]
rw [abs_of_nonneg h] at h₁ 
[GOAL]
case inr.intro.intro.intro.refine'_1.intro
α : Type u_1
inst✝ : LinearOrderedField α
f : CauSeq α abs
h✝ : ¬LimZero f
K : α
K0 : K > 0
hK : ∃ i, ∀ (j : ℕ), j ≥ i → K ≤ |↑f j|
i : ℕ
hi : ∀ (j : ℕ), j ≥ i → K ≤ |↑f j| ∧ ∀ (k : ℕ), k ≥ j → |↑f k - ↑f j| < K
h : 0 ≤ ↑f i
j : ℕ
ij : j ≥ i
this : K ≤ |↑f j|
h₁ : K ≤ ↑f i
h₂ : ∀ (k : ℕ), k ≥ i → |↑f k - ↑f i| < K
⊢ 0 ≤ ↑f j
[PROOFSTEP]
exact (le_add_iff_nonneg_right _).1 (le_trans h₁ <| neg_le_sub_iff_le_add'.1 <| le_of_lt (abs_lt.1 <| h₂ _ ij).1)
[GOAL]
case inr.intro.intro.intro.refine'_2.intro
α : Type u_1
inst✝ : LinearOrderedField α
f : CauSeq α abs
h✝ : ¬LimZero f
K : α
K0 : K > 0
hK : ∃ i, ∀ (j : ℕ), j ≥ i → K ≤ |↑f j|
i : ℕ
hi : ∀ (j : ℕ), j ≥ i → K ≤ |↑f j| ∧ ∀ (k : ℕ), k ≥ j → |↑f k - ↑f j| < K
h : ↑f i ≤ 0
j : ℕ
ij : j ≥ i
this : K ≤ |↑f j|
h₁ : K ≤ |↑f i|
h₂ : ∀ (k : ℕ), k ≥ i → |↑f k - ↑f i| < K
⊢ K ≤ ↑(-f) j
[PROOFSTEP]
rwa [abs_of_nonpos] at this 
[GOAL]
case inr.intro.intro.intro.refine'_2.intro
α : Type u_1
inst✝ : LinearOrderedField α
f : CauSeq α abs
h✝ : ¬LimZero f
K : α
K0 : K > 0
hK : ∃ i, ∀ (j : ℕ), j ≥ i → K ≤ |↑f j|
i : ℕ
hi : ∀ (j : ℕ), j ≥ i → K ≤ |↑f j| ∧ ∀ (k : ℕ), k ≥ j → |↑f k - ↑f j| < K
h : ↑f i ≤ 0
j : ℕ
ij : j ≥ i
this : K ≤ |↑f j|
h₁ : K ≤ |↑f i|
h₂ : ∀ (k : ℕ), k ≥ i → |↑f k - ↑f i| < K
⊢ ↑f j ≤ 0
[PROOFSTEP]
rw [abs_of_nonpos h] at h₁ 
[GOAL]
case inr.intro.intro.intro.refine'_2.intro
α : Type u_1
inst✝ : LinearOrderedField α
f : CauSeq α abs
h✝ : ¬LimZero f
K : α
K0 : K > 0
hK : ∃ i, ∀ (j : ℕ), j ≥ i → K ≤ |↑f j|
i : ℕ
hi : ∀ (j : ℕ), j ≥ i → K ≤ |↑f j| ∧ ∀ (k : ℕ), k ≥ j → |↑f k - ↑f j| < K
h : ↑f i ≤ 0
j : ℕ
ij : j ≥ i
this : K ≤ |↑f j|
h₁ : K ≤ -↑f i
h₂ : ∀ (k : ℕ), k ≥ i → |↑f k - ↑f i| < K
⊢ ↑f j ≤ 0
[PROOFSTEP]
rw [← sub_le_sub_iff_right, zero_sub]
[GOAL]
case inr.intro.intro.intro.refine'_2.intro
α : Type u_1
inst✝ : LinearOrderedField α
f : CauSeq α abs
h✝ : ¬LimZero f
K : α
K0 : K > 0
hK : ∃ i, ∀ (j : ℕ), j ≥ i → K ≤ |↑f j|
i : ℕ
hi : ∀ (j : ℕ), j ≥ i → K ≤ |↑f j| ∧ ∀ (k : ℕ), k ≥ j → |↑f k - ↑f j| < K
h : ↑f i ≤ 0
j : ℕ
ij : j ≥ i
this : K ≤ |↑f j|
h₁ : K ≤ -↑f i
h₂ : ∀ (k : ℕ), k ≥ i → |↑f k - ↑f i| < K
⊢ ↑f j - ?inr.intro.intro.intro.refine'_2.intro ≤ -?inr.intro.intro.intro.refine'_2.intro
case inr.intro.intro.intro.refine'_2.intro
α : Type u_1
inst✝ : LinearOrderedField α
f : CauSeq α abs
h✝ : ¬LimZero f
K : α
K0 : K > 0
hK : ∃ i, ∀ (j : ℕ), j ≥ i → K ≤ |↑f j|
i : ℕ
hi : ∀ (j : ℕ), j ≥ i → K ≤ |↑f j| ∧ ∀ (k : ℕ), k ≥ j → |↑f k - ↑f j| < K
h : ↑f i ≤ 0
j : ℕ
ij : j ≥ i
this : K ≤ |↑f j|
h₁ : K ≤ -↑f i
h₂ : ∀ (k : ℕ), k ≥ i → |↑f k - ↑f i| < K
⊢ α
[PROOFSTEP]
exact le_trans (le_of_lt (abs_lt.1 <| h₂ _ ij).2) h₁
[GOAL]
α : Type u_1
inst✝ : LinearOrderedField α
f g h : CauSeq α abs
fg : f < g
gh : g ≈ h
⊢ Pos (h - f)
[PROOFSTEP]
convert pos_add_limZero fg (neg_limZero gh) using 1
[GOAL]
case h.e'_3
α : Type u_1
inst✝ : LinearOrderedField α
f g h : CauSeq α abs
fg : f < g
gh : g ≈ h
⊢ h - f = g - f + -(g - h)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝ : LinearOrderedField α
f g h : CauSeq α abs
fg : f ≈ g
gh : g < h
⊢ f < h
[PROOFSTEP]
have := pos_add_limZero gh (neg_limZero fg)
[GOAL]
α : Type u_1
inst✝ : LinearOrderedField α
f g h : CauSeq α abs
fg : f ≈ g
gh : g < h
this : Pos (h - g + -(f - g))
⊢ f < h
[PROOFSTEP]
rwa [← sub_eq_add_neg, sub_sub_sub_cancel_right] at this 
[GOAL]
α : Type u_1
inst✝ : LinearOrderedField α
f g h : CauSeq α abs
fg : f < g
gh : g < h
⊢ Pos (h - f)
[PROOFSTEP]
convert add_pos fg gh using 1
[GOAL]
case h.e'_3
α : Type u_1
inst✝ : LinearOrderedField α
f g h : CauSeq α abs
fg : f < g
gh : g < h
⊢ h - f = g - f + (h - g)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝ : LinearOrderedField α
f : CauSeq α abs
x✝ : f < f
h : f < f := x✝
⊢ LimZero (f - f)
[PROOFSTEP]
simp [zero_limZero]
[GOAL]
α : Type u_1
inst✝ : LinearOrderedField α
f g : CauSeq α abs
h✝ : LimZero (g - f) ∨ Pos (-(g - f))
h : Pos (-(g - f))
⊢ g < f
[PROOFSTEP]
rwa [neg_sub] at h 
[GOAL]
α : Type u_1
inst✝ : LinearOrderedField α
x y : α
⊢ Pos (const y - const x) ↔ x < y
[PROOFSTEP]
rw [← const_sub, const_pos, sub_pos]
[GOAL]
α : Type u_1
inst✝ : LinearOrderedField α
x y : α
⊢ const x ≤ const y ↔ x ≤ y
[PROOFSTEP]
rw [le_iff_lt_or_eq]
[GOAL]
α : Type u_1
inst✝ : LinearOrderedField α
x y : α
⊢ const x ≤ const y ↔ x < y ∨ x = y
[PROOFSTEP]
exact or_congr const_lt const_equiv
[GOAL]
α : Type u_1
inst✝ : LinearOrderedField α
f : CauSeq α abs
K : α
H : ∀ (i : ℕ), |↑f i| < K
i : ℕ
x✝ : i ≥ 0
⊢ 1 ≤ ↑(const (K + 1) - f) i
[PROOFSTEP]
rw [sub_apply, const_apply, le_sub_iff_add_le', add_le_add_iff_right]
[GOAL]
α : Type u_1
inst✝ : LinearOrderedField α
f : CauSeq α abs
K : α
H : ∀ (i : ℕ), |↑f i| < K
i : ℕ
x✝ : i ≥ 0
⊢ ↑f i ≤ K
[PROOFSTEP]
exact le_of_lt (abs_lt.1 (H _)).2
[GOAL]
α : Type u_1
inst✝ : LinearOrderedField α
f : CauSeq α abs
a : α
h : -f < const a
⊢ Pos (f - const (-a))
[PROOFSTEP]
rwa [const_neg, sub_neg_eq_add, add_comm, ← sub_neg_eq_add]
[GOAL]
α : Type u_1
inst✝ : LinearOrderedField α
f g : CauSeq α abs
hf : LimZero f
hg : LimZero g
ε : α
ε0 : ε > 0
i : ℕ
H : ∀ (j : ℕ), j ≥ i → |↑f j| < ε ∧ |↑g j| < ε
j : ℕ
ij : j ≥ i
⊢ |↑(f ⊔ g) j| < ε
[PROOFSTEP]
let ⟨H₁, H₂⟩ := H _ ij
[GOAL]
α : Type u_1
inst✝ : LinearOrderedField α
f g : CauSeq α abs
hf : LimZero f
hg : LimZero g
ε : α
ε0 : ε > 0
i : ℕ
H : ∀ (j : ℕ), j ≥ i → |↑f j| < ε ∧ |↑g j| < ε
j : ℕ
ij : j ≥ i
H₁ : |↑f j| < ε
H₂ : |↑g j| < ε
⊢ |↑(f ⊔ g) j| < ε
[PROOFSTEP]
rw [abs_lt] at H₁ H₂ ⊢
[GOAL]
α : Type u_1
inst✝ : LinearOrderedField α
f g : CauSeq α abs
hf : LimZero f
hg : LimZero g
ε : α
ε0 : ε > 0
i : ℕ
H : ∀ (j : ℕ), j ≥ i → |↑f j| < ε ∧ |↑g j| < ε
j : ℕ
ij : j ≥ i
H₁ : -ε < ↑f j ∧ ↑f j < ε
H₂ : -ε < ↑g j ∧ ↑g j < ε
⊢ -ε < ↑(f ⊔ g) j ∧ ↑(f ⊔ g) j < ε
[PROOFSTEP]
exact ⟨lt_sup_iff.mpr (Or.inl H₁.1), sup_lt_iff.mpr ⟨H₁.2, H₂.2⟩⟩
[GOAL]
α : Type u_1
inst✝ : LinearOrderedField α
f g : CauSeq α abs
hf : LimZero f
hg : LimZero g
ε : α
ε0 : ε > 0
i : ℕ
H : ∀ (j : ℕ), j ≥ i → |↑f j| < ε ∧ |↑g j| < ε
j : ℕ
ij : j ≥ i
⊢ |↑(f ⊓ g) j| < ε
[PROOFSTEP]
let ⟨H₁, H₂⟩ := H _ ij
[GOAL]
α : Type u_1
inst✝ : LinearOrderedField α
f g : CauSeq α abs
hf : LimZero f
hg : LimZero g
ε : α
ε0 : ε > 0
i : ℕ
H : ∀ (j : ℕ), j ≥ i → |↑f j| < ε ∧ |↑g j| < ε
j : ℕ
ij : j ≥ i
H₁ : |↑f j| < ε
H₂ : |↑g j| < ε
⊢ |↑(f ⊓ g) j| < ε
[PROOFSTEP]
rw [abs_lt] at H₁ H₂ ⊢
[GOAL]
α : Type u_1
inst✝ : LinearOrderedField α
f g : CauSeq α abs
hf : LimZero f
hg : LimZero g
ε : α
ε0 : ε > 0
i : ℕ
H : ∀ (j : ℕ), j ≥ i → |↑f j| < ε ∧ |↑g j| < ε
j : ℕ
ij : j ≥ i
H₁ : -ε < ↑f j ∧ ↑f j < ε
H₂ : -ε < ↑g j ∧ ↑g j < ε
⊢ -ε < ↑(f ⊓ g) j ∧ ↑(f ⊓ g) j < ε
[PROOFSTEP]
exact ⟨lt_inf_iff.mpr ⟨H₁.1, H₂.1⟩, inf_lt_iff.mpr (Or.inl H₁.2)⟩
[GOAL]
α : Type u_1
inst✝ : LinearOrderedField α
a₁ b₁ a₂ b₂ : CauSeq α abs
ha : a₁ ≈ a₂
hb : b₁ ≈ b₂
⊢ a₁ ⊔ b₁ ≈ a₂ ⊔ b₂
[PROOFSTEP]
intro ε ε0
[GOAL]
α : Type u_1
inst✝ : LinearOrderedField α
a₁ b₁ a₂ b₂ : CauSeq α abs
ha : a₁ ≈ a₂
hb : b₁ ≈ b₂
ε : α
ε0 : ε > 0
⊢ ∃ i, ∀ (j : ℕ), j ≥ i → |↑(a₁ ⊔ b₁ - a₂ ⊔ b₂) j| < ε
[PROOFSTEP]
obtain ⟨ai, hai⟩ := ha ε ε0
[GOAL]
case intro
α : Type u_1
inst✝ : LinearOrderedField α
a₁ b₁ a₂ b₂ : CauSeq α abs
ha : a₁ ≈ a₂
hb : b₁ ≈ b₂
ε : α
ε0 : ε > 0
ai : ℕ
hai : ∀ (j : ℕ), j ≥ ai → |↑(a₁ - a₂) j| < ε
⊢ ∃ i, ∀ (j : ℕ), j ≥ i → |↑(a₁ ⊔ b₁ - a₂ ⊔ b₂) j| < ε
[PROOFSTEP]
obtain ⟨bi, hbi⟩ := hb ε ε0
[GOAL]
case intro.intro
α : Type u_1
inst✝ : LinearOrderedField α
a₁ b₁ a₂ b₂ : CauSeq α abs
ha : a₁ ≈ a₂
hb : b₁ ≈ b₂
ε : α
ε0 : ε > 0
ai : ℕ
hai : ∀ (j : ℕ), j ≥ ai → |↑(a₁ - a₂) j| < ε
bi : ℕ
hbi : ∀ (j : ℕ), j ≥ bi → |↑(b₁ - b₂) j| < ε
⊢ ∃ i, ∀ (j : ℕ), j ≥ i → |↑(a₁ ⊔ b₁ - a₂ ⊔ b₂) j| < ε
[PROOFSTEP]
exact
  ⟨ai ⊔ bi, fun i hi =>
    (abs_max_sub_max_le_max (a₁ i) (b₁ i) (a₂ i) (b₂ i)).trans_lt
      (max_lt (hai i (sup_le_iff.mp hi).1) (hbi i (sup_le_iff.mp hi).2))⟩
[GOAL]
α : Type u_1
inst✝ : LinearOrderedField α
a₁ b₁ a₂ b₂ : CauSeq α abs
ha : a₁ ≈ a₂
hb : b₁ ≈ b₂
⊢ a₁ ⊓ b₁ ≈ a₂ ⊓ b₂
[PROOFSTEP]
intro ε ε0
[GOAL]
α : Type u_1
inst✝ : LinearOrderedField α
a₁ b₁ a₂ b₂ : CauSeq α abs
ha : a₁ ≈ a₂
hb : b₁ ≈ b₂
ε : α
ε0 : ε > 0
⊢ ∃ i, ∀ (j : ℕ), j ≥ i → |↑(a₁ ⊓ b₁ - a₂ ⊓ b₂) j| < ε
[PROOFSTEP]
obtain ⟨ai, hai⟩ := ha ε ε0
[GOAL]
case intro
α : Type u_1
inst✝ : LinearOrderedField α
a₁ b₁ a₂ b₂ : CauSeq α abs
ha : a₁ ≈ a₂
hb : b₁ ≈ b₂
ε : α
ε0 : ε > 0
ai : ℕ
hai : ∀ (j : ℕ), j ≥ ai → |↑(a₁ - a₂) j| < ε
⊢ ∃ i, ∀ (j : ℕ), j ≥ i → |↑(a₁ ⊓ b₁ - a₂ ⊓ b₂) j| < ε
[PROOFSTEP]
obtain ⟨bi, hbi⟩ := hb ε ε0
[GOAL]
case intro.intro
α : Type u_1
inst✝ : LinearOrderedField α
a₁ b₁ a₂ b₂ : CauSeq α abs
ha : a₁ ≈ a₂
hb : b₁ ≈ b₂
ε : α
ε0 : ε > 0
ai : ℕ
hai : ∀ (j : ℕ), j ≥ ai → |↑(a₁ - a₂) j| < ε
bi : ℕ
hbi : ∀ (j : ℕ), j ≥ bi → |↑(b₁ - b₂) j| < ε
⊢ ∃ i, ∀ (j : ℕ), j ≥ i → |↑(a₁ ⊓ b₁ - a₂ ⊓ b₂) j| < ε
[PROOFSTEP]
exact
  ⟨ai ⊔ bi, fun i hi =>
    (abs_min_sub_min_le_max (a₁ i) (b₁ i) (a₂ i) (b₂ i)).trans_lt
      (max_lt (hai i (sup_le_iff.mp hi).1) (hbi i (sup_le_iff.mp hi).2))⟩
[GOAL]
α : Type u_1
inst✝ : LinearOrderedField α
a b c : CauSeq α abs
ha : a < c
hb : b < c
⊢ a ⊔ b < c
[PROOFSTEP]
obtain ⟨⟨εa, εa0, ia, ha⟩, ⟨εb, εb0, ib, hb⟩⟩ := ha, hb
[GOAL]
case intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝ : LinearOrderedField α
a b c : CauSeq α abs
εa : α
εa0 : εa > 0
ia : ℕ
ha : ∀ (j : ℕ), j ≥ ia → εa ≤ ↑(c - a) j
εb : α
εb0 : εb > 0
ib : ℕ
hb : ∀ (j : ℕ), j ≥ ib → εb ≤ ↑(c - b) j
⊢ a ⊔ b < c
[PROOFSTEP]
refine' ⟨εa ⊓ εb, lt_inf_iff.mpr ⟨εa0, εb0⟩, ia ⊔ ib, fun i hi => _⟩
[GOAL]
case intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝ : LinearOrderedField α
a b c : CauSeq α abs
εa : α
εa0 : εa > 0
ia : ℕ
ha : ∀ (j : ℕ), j ≥ ia → εa ≤ ↑(c - a) j
εb : α
εb0 : εb > 0
ib : ℕ
hb : ∀ (j : ℕ), j ≥ ib → εb ≤ ↑(c - b) j
i : ℕ
hi : i ≥ ia ⊔ ib
⊢ εa ⊓ εb ≤ ↑(c - a ⊔ b) i
[PROOFSTEP]
have := min_le_min (ha _ (sup_le_iff.mp hi).1) (hb _ (sup_le_iff.mp hi).2)
[GOAL]
case intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝ : LinearOrderedField α
a b c : CauSeq α abs
εa : α
εa0 : εa > 0
ia : ℕ
ha : ∀ (j : ℕ), j ≥ ia → εa ≤ ↑(c - a) j
εb : α
εb0 : εb > 0
ib : ℕ
hb : ∀ (j : ℕ), j ≥ ib → εb ≤ ↑(c - b) j
i : ℕ
hi : i ≥ ia ⊔ ib
this : min εa εb ≤ min (↑(c - a) i) (↑(c - b) i)
⊢ εa ⊓ εb ≤ ↑(c - a ⊔ b) i
[PROOFSTEP]
exact this.trans_eq (min_sub_sub_left _ _ _)
[GOAL]
α : Type u_1
inst✝ : LinearOrderedField α
a b c : CauSeq α abs
hb : a < b
hc : a < c
⊢ a < b ⊓ c
[PROOFSTEP]
obtain ⟨⟨εb, εb0, ib, hb⟩, ⟨εc, εc0, ic, hc⟩⟩ := hb, hc
[GOAL]
case intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝ : LinearOrderedField α
a b c : CauSeq α abs
εb : α
εb0 : εb > 0
ib : ℕ
hb : ∀ (j : ℕ), j ≥ ib → εb ≤ ↑(b - a) j
εc : α
εc0 : εc > 0
ic : ℕ
hc : ∀ (j : ℕ), j ≥ ic → εc ≤ ↑(c - a) j
⊢ a < b ⊓ c
[PROOFSTEP]
refine' ⟨εb ⊓ εc, lt_inf_iff.mpr ⟨εb0, εc0⟩, ib ⊔ ic, fun i hi => _⟩
[GOAL]
case intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝ : LinearOrderedField α
a b c : CauSeq α abs
εb : α
εb0 : εb > 0
ib : ℕ
hb : ∀ (j : ℕ), j ≥ ib → εb ≤ ↑(b - a) j
εc : α
εc0 : εc > 0
ic : ℕ
hc : ∀ (j : ℕ), j ≥ ic → εc ≤ ↑(c - a) j
i : ℕ
hi : i ≥ ib ⊔ ic
⊢ εb ⊓ εc ≤ ↑(b ⊓ c - a) i
[PROOFSTEP]
have := min_le_min (hb _ (sup_le_iff.mp hi).1) (hc _ (sup_le_iff.mp hi).2)
[GOAL]
case intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝ : LinearOrderedField α
a b c : CauSeq α abs
εb : α
εb0 : εb > 0
ib : ℕ
hb : ∀ (j : ℕ), j ≥ ib → εb ≤ ↑(b - a) j
εc : α
εc0 : εc > 0
ic : ℕ
hc : ∀ (j : ℕ), j ≥ ic → εc ≤ ↑(c - a) j
i : ℕ
hi : i ≥ ib ⊔ ic
this : min εb εc ≤ min (↑(b - a) i) (↑(c - a) i)
⊢ εb ⊓ εc ≤ ↑(b ⊓ c - a) i
[PROOFSTEP]
exact this.trans_eq (min_sub_sub_right _ _ _)
[GOAL]
α : Type u_1
inst✝ : LinearOrderedField α
a b : CauSeq α abs
h : a ≤ b
⊢ a ⊔ b ≈ b
[PROOFSTEP]
obtain ⟨ε, ε0 : _ < _, i, h⟩ | h := h
[GOAL]
case inl.intro.intro.intro
α : Type u_1
inst✝ : LinearOrderedField α
a b : CauSeq α abs
ε : α
ε0 : 0 < ε
i : ℕ
h : ∀ (j : ℕ), j ≥ i → ε ≤ ↑(b - a) j
⊢ a ⊔ b ≈ b
[PROOFSTEP]
intro _ _
[GOAL]
case inl.intro.intro.intro
α : Type u_1
inst✝ : LinearOrderedField α
a b : CauSeq α abs
ε : α
ε0 : 0 < ε
i : ℕ
h : ∀ (j : ℕ), j ≥ i → ε ≤ ↑(b - a) j
ε✝ : α
a✝ : ε✝ > 0
⊢ ∃ i, ∀ (j : ℕ), j ≥ i → |↑(a ⊔ b - b) j| < ε✝
[PROOFSTEP]
refine' ⟨i, fun j hj => _⟩
[GOAL]
case inl.intro.intro.intro
α : Type u_1
inst✝ : LinearOrderedField α
a b : CauSeq α abs
ε : α
ε0 : 0 < ε
i : ℕ
h : ∀ (j : ℕ), j ≥ i → ε ≤ ↑(b - a) j
ε✝ : α
a✝ : ε✝ > 0
j : ℕ
hj : j ≥ i
⊢ |↑(a ⊔ b - b) j| < ε✝
[PROOFSTEP]
dsimp
[GOAL]
case inl.intro.intro.intro
α : Type u_1
inst✝ : LinearOrderedField α
a b : CauSeq α abs
ε : α
ε0 : 0 < ε
i : ℕ
h : ∀ (j : ℕ), j ≥ i → ε ≤ ↑(b - a) j
ε✝ : α
a✝ : ε✝ > 0
j : ℕ
hj : j ≥ i
⊢ |↑a j ⊔ ↑b j - ↑b j| < ε✝
[PROOFSTEP]
erw [← max_sub_sub_right]
[GOAL]
case inl.intro.intro.intro
α : Type u_1
inst✝ : LinearOrderedField α
a b : CauSeq α abs
ε : α
ε0 : 0 < ε
i : ℕ
h : ∀ (j : ℕ), j ≥ i → ε ≤ ↑(b - a) j
ε✝ : α
a✝ : ε✝ > 0
j : ℕ
hj : j ≥ i
⊢ |max (↑a j - ↑b j) (↑b j - ↑b j)| < ε✝
[PROOFSTEP]
rwa [sub_self, max_eq_right, abs_zero]
[GOAL]
case inl.intro.intro.intro
α : Type u_1
inst✝ : LinearOrderedField α
a b : CauSeq α abs
ε : α
ε0 : 0 < ε
i : ℕ
h : ∀ (j : ℕ), j ≥ i → ε ≤ ↑(b - a) j
ε✝ : α
a✝ : ε✝ > 0
j : ℕ
hj : j ≥ i
⊢ ↑a j - ↑b j ≤ 0
[PROOFSTEP]
rw [sub_nonpos, ← sub_nonneg]
[GOAL]
case inl.intro.intro.intro
α : Type u_1
inst✝ : LinearOrderedField α
a b : CauSeq α abs
ε : α
ε0 : 0 < ε
i : ℕ
h : ∀ (j : ℕ), j ≥ i → ε ≤ ↑(b - a) j
ε✝ : α
a✝ : ε✝ > 0
j : ℕ
hj : j ≥ i
⊢ 0 ≤ ↑b j - ↑a j
[PROOFSTEP]
exact ε0.le.trans (h _ hj)
[GOAL]
case inr
α : Type u_1
inst✝ : LinearOrderedField α
a b : CauSeq α abs
h : a ≈ b
⊢ a ⊔ b ≈ b
[PROOFSTEP]
refine' Setoid.trans (sup_equiv_sup h (Setoid.refl _)) _
[GOAL]
case inr
α : Type u_1
inst✝ : LinearOrderedField α
a b : CauSeq α abs
h : a ≈ b
⊢ b ⊔ b ≈ b
[PROOFSTEP]
rw [CauSeq.sup_idem]
[GOAL]
α : Type u_1
inst✝ : LinearOrderedField α
a b : CauSeq α abs
h : b ≤ a
⊢ a ⊓ b ≈ b
[PROOFSTEP]
obtain ⟨ε, ε0 : _ < _, i, h⟩ | h := h
[GOAL]
case inl.intro.intro.intro
α : Type u_1
inst✝ : LinearOrderedField α
a b : CauSeq α abs
ε : α
ε0 : 0 < ε
i : ℕ
h : ∀ (j : ℕ), j ≥ i → ε ≤ ↑(a - b) j
⊢ a ⊓ b ≈ b
[PROOFSTEP]
intro _ _
[GOAL]
case inl.intro.intro.intro
α : Type u_1
inst✝ : LinearOrderedField α
a b : CauSeq α abs
ε : α
ε0 : 0 < ε
i : ℕ
h : ∀ (j : ℕ), j ≥ i → ε ≤ ↑(a - b) j
ε✝ : α
a✝ : ε✝ > 0
⊢ ∃ i, ∀ (j : ℕ), j ≥ i → |↑(a ⊓ b - b) j| < ε✝
[PROOFSTEP]
refine' ⟨i, fun j hj => _⟩
[GOAL]
case inl.intro.intro.intro
α : Type u_1
inst✝ : LinearOrderedField α
a b : CauSeq α abs
ε : α
ε0 : 0 < ε
i : ℕ
h : ∀ (j : ℕ), j ≥ i → ε ≤ ↑(a - b) j
ε✝ : α
a✝ : ε✝ > 0
j : ℕ
hj : j ≥ i
⊢ |↑(a ⊓ b - b) j| < ε✝
[PROOFSTEP]
dsimp
[GOAL]
case inl.intro.intro.intro
α : Type u_1
inst✝ : LinearOrderedField α
a b : CauSeq α abs
ε : α
ε0 : 0 < ε
i : ℕ
h : ∀ (j : ℕ), j ≥ i → ε ≤ ↑(a - b) j
ε✝ : α
a✝ : ε✝ > 0
j : ℕ
hj : j ≥ i
⊢ |↑a j ⊓ ↑b j - ↑b j| < ε✝
[PROOFSTEP]
erw [← min_sub_sub_right]
[GOAL]
case inl.intro.intro.intro
α : Type u_1
inst✝ : LinearOrderedField α
a b : CauSeq α abs
ε : α
ε0 : 0 < ε
i : ℕ
h : ∀ (j : ℕ), j ≥ i → ε ≤ ↑(a - b) j
ε✝ : α
a✝ : ε✝ > 0
j : ℕ
hj : j ≥ i
⊢ |min (↑a j - ↑b j) (↑b j - ↑b j)| < ε✝
[PROOFSTEP]
rwa [sub_self, min_eq_right, abs_zero]
[GOAL]
case inl.intro.intro.intro
α : Type u_1
inst✝ : LinearOrderedField α
a b : CauSeq α abs
ε : α
ε0 : 0 < ε
i : ℕ
h : ∀ (j : ℕ), j ≥ i → ε ≤ ↑(a - b) j
ε✝ : α
a✝ : ε✝ > 0
j : ℕ
hj : j ≥ i
⊢ 0 ≤ ↑a j - ↑b j
[PROOFSTEP]
exact ε0.le.trans (h _ hj)
[GOAL]
case inr
α : Type u_1
inst✝ : LinearOrderedField α
a b : CauSeq α abs
h : b ≈ a
⊢ a ⊓ b ≈ b
[PROOFSTEP]
refine' Setoid.trans (inf_equiv_inf (Setoid.symm h) (Setoid.refl _)) _
[GOAL]
case inr
α : Type u_1
inst✝ : LinearOrderedField α
a b : CauSeq α abs
h : b ≈ a
⊢ b ⊓ b ≈ b
[PROOFSTEP]
rw [CauSeq.inf_idem]
[GOAL]
α : Type u_1
inst✝ : LinearOrderedField α
a b : CauSeq α abs
h : b ≤ a
⊢ a ⊔ b ≈ a
[PROOFSTEP]
simpa only [CauSeq.sup_comm] using CauSeq.sup_eq_right h
[GOAL]
α : Type u_1
inst✝ : LinearOrderedField α
a b : CauSeq α abs
h : a ≤ b
⊢ a ⊓ b ≈ a
[PROOFSTEP]
simpa only [CauSeq.inf_comm] using CauSeq.inf_eq_right h
[GOAL]
α : Type u_1
inst✝ : LinearOrderedField α
a b c : CauSeq α abs
ha : a ≤ c
hb : b ≤ c
⊢ a ⊔ b ≤ c
[PROOFSTEP]
cases' ha with ha ha
[GOAL]
case inl
α : Type u_1
inst✝ : LinearOrderedField α
a b c : CauSeq α abs
hb : b ≤ c
ha : a < c
⊢ a ⊔ b ≤ c
[PROOFSTEP]
cases' hb with hb hb
[GOAL]
case inl.inl
α : Type u_1
inst✝ : LinearOrderedField α
a b c : CauSeq α abs
ha : a < c
hb : b < c
⊢ a ⊔ b ≤ c
[PROOFSTEP]
exact Or.inl (CauSeq.sup_lt ha hb)
[GOAL]
case inl.inr
α : Type u_1
inst✝ : LinearOrderedField α
a b c : CauSeq α abs
ha : a < c
hb : b ≈ c
⊢ a ⊔ b ≤ c
[PROOFSTEP]
replace ha := le_of_le_of_eq ha.le (Setoid.symm hb)
[GOAL]
case inl.inr
α : Type u_1
inst✝ : LinearOrderedField α
a b c : CauSeq α abs
hb : b ≈ c
ha : a ≤ b
⊢ a ⊔ b ≤ c
[PROOFSTEP]
refine' le_of_le_of_eq (Or.inr _) hb
[GOAL]
case inl.inr
α : Type u_1
inst✝ : LinearOrderedField α
a b c : CauSeq α abs
hb : b ≈ c
ha : a ≤ b
⊢ a ⊔ b ≈ b
[PROOFSTEP]
exact CauSeq.sup_eq_right ha
[GOAL]
case inr
α : Type u_1
inst✝ : LinearOrderedField α
a b c : CauSeq α abs
hb : b ≤ c
ha : a ≈ c
⊢ a ⊔ b ≤ c
[PROOFSTEP]
replace hb := le_of_le_of_eq hb (Setoid.symm ha)
[GOAL]
case inr
α : Type u_1
inst✝ : LinearOrderedField α
a b c : CauSeq α abs
ha : a ≈ c
hb : b ≤ a
⊢ a ⊔ b ≤ c
[PROOFSTEP]
refine' le_of_le_of_eq (Or.inr _) ha
[GOAL]
case inr
α : Type u_1
inst✝ : LinearOrderedField α
a b c : CauSeq α abs
ha : a ≈ c
hb : b ≤ a
⊢ a ⊔ b ≈ a
[PROOFSTEP]
exact CauSeq.sup_eq_left hb
[GOAL]
α : Type u_1
inst✝ : LinearOrderedField α
a b c : CauSeq α abs
hb : a ≤ b
hc : a ≤ c
⊢ a ≤ b ⊓ c
[PROOFSTEP]
cases' hb with hb hb
[GOAL]
case inl
α : Type u_1
inst✝ : LinearOrderedField α
a b c : CauSeq α abs
hc : a ≤ c
hb : a < b
⊢ a ≤ b ⊓ c
[PROOFSTEP]
cases' hc with hc hc
[GOAL]
case inl.inl
α : Type u_1
inst✝ : LinearOrderedField α
a b c : CauSeq α abs
hb : a < b
hc : a < c
⊢ a ≤ b ⊓ c
[PROOFSTEP]
exact Or.inl (CauSeq.lt_inf hb hc)
[GOAL]
case inl.inr
α : Type u_1
inst✝ : LinearOrderedField α
a b c : CauSeq α abs
hb : a < b
hc : a ≈ c
⊢ a ≤ b ⊓ c
[PROOFSTEP]
replace hb := le_of_eq_of_le (Setoid.symm hc) hb.le
[GOAL]
case inl.inr
α : Type u_1
inst✝ : LinearOrderedField α
a b c : CauSeq α abs
hc : a ≈ c
hb : c ≤ b
⊢ a ≤ b ⊓ c
[PROOFSTEP]
refine' le_of_eq_of_le hc (Or.inr _)
[GOAL]
case inl.inr
α : Type u_1
inst✝ : LinearOrderedField α
a b c : CauSeq α abs
hc : a ≈ c
hb : c ≤ b
⊢ c ≈ b ⊓ c
[PROOFSTEP]
exact Setoid.symm (CauSeq.inf_eq_right hb)
[GOAL]
case inr
α : Type u_1
inst✝ : LinearOrderedField α
a b c : CauSeq α abs
hc : a ≤ c
hb : a ≈ b
⊢ a ≤ b ⊓ c
[PROOFSTEP]
replace hc := le_of_eq_of_le (Setoid.symm hb) hc
[GOAL]
case inr
α : Type u_1
inst✝ : LinearOrderedField α
a b c : CauSeq α abs
hb : a ≈ b
hc : b ≤ c
⊢ a ≤ b ⊓ c
[PROOFSTEP]
refine' le_of_eq_of_le hb (Or.inr _)
[GOAL]
case inr
α : Type u_1
inst✝ : LinearOrderedField α
a b c : CauSeq α abs
hb : a ≈ b
hc : b ≤ c
⊢ b ≈ b ⊓ c
[PROOFSTEP]
exact Setoid.symm (CauSeq.inf_eq_left hc)
