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