case intro
α : Type u
β : Type v
γ : Type ?u.8099
inst✝ : OmegaCompletePartialOrder α
c₀ c₁ : Chain α
h✝ : c₀ ≤ c₁
i w✝ : ℕ
h : ↑c₀ i ≤ ↑c₁ w✝
⊢ ↑c₀ i ≤ ωSup c₁
α : Type u
β : Type v
γ : Type ?u.8099
inst✝ : OmegaCompletePartialOrder α
c₀ c₁ : Chain α
h : c₀ ≤ c₁
i : ℕ
⊢ ↑c₀ i ≤ ωSup c₁
obtain ⟨_, h⟩ := h i
no goals
case intro
α : Type u
β : Type v
γ : Type ?u.8099
inst✝ : OmegaCompletePartialOrder α
c₀ c₁ : Chain α
h✝ : c₀ ≤ c₁
i w✝ : ℕ
h : ↑c₀ i ≤ ↑c₁ w✝
⊢ ↑c₀ i ≤ ωSup c₁
exact le_trans h (le_ωSup _ _)