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

case inr
α : Type u_1
inst✝ : LinearOrderedField α
a b : CauSeq α abs
h : b ≈ a
⊢ a ⊓ b ≈ b
α : Type u_1
inst✝ : LinearOrderedField α
a b : CauSeq α abs
h : b ≤ a
⊢ a ⊓ b ≈ b
obtain ⟨ε, ε0 : _ < _, i, h⟩ | h := h
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 → abs (↑(a ⊓ b - b) j) < ε✝
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
intro _ _
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
⊢ abs (↑(a ⊓ b - b) j) < ε✝
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 → abs (↑(a ⊓ b - b) j) < ε✝
refine' ⟨i, fun j hj => _⟩
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
⊢ abs (↑a j ⊓ ↑b j - ↑b j) < ε✝
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
⊢ abs (↑(a ⊓ b - b) j) < ε✝
dsimp
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
⊢ abs (min (↑a j - ↑b j) (↑b j - ↑b j)) < ε✝
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
⊢ abs (↑a j ⊓ ↑b j - ↑b j) < ε✝
erw [← min_sub_sub_right]
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
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
⊢ abs (min (↑a j - ↑b j) (↑b j - ↑b j)) < ε✝
rwa [sub_self, min_eq_right, abs_zero]
no goals
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
exact ε0.le.trans (h _ hj)
case inr
α : Type u_1
inst✝ : LinearOrderedField α
a b : CauSeq α abs
h : b ≈ a
⊢ b ⊓ b ≈ b
case inr
α : Type u_1
inst✝ : LinearOrderedField α
a b : CauSeq α abs
h : b ≈ a
⊢ a ⊓ b ≈ b
refine' Setoid.trans (inf_equiv_inf (Setoid.symm h) (Setoid.refl _)) _
no goals
case inr
α : Type u_1
inst✝ : LinearOrderedField α
a b : CauSeq α abs
h : b ≈ a
⊢ b ⊓ b ≈ b
rw [CauSeq.inf_idem]