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
α : Type u_1
inst✝ : LinearOrderedField α
a b c : CauSeq α abs
hb : a < b
hc : a < c
⊢ a < b ⊓ c
obtain ⟨⟨εb, εb0, ib, hb⟩, ⟨εc, εc0, ic, hc⟩⟩ := hb, hc
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
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
refine' ⟨εb ⊓ εc, lt_inf_iff.mpr ⟨εb0, εc0⟩, ib ⊔ ic, fun i hi => _⟩
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
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
have := min_le_min (hb _ (sup_le_iff.mp hi).1) (hc _ (sup_le_iff.mp hi).2)
no goals
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
exact this.trans_eq (min_sub_sub_right _ _ _)