case H
α : Type u_1
β : Type u_2
γ : Type ?u.22086
inst✝² : OmegaCompletePartialOrder α
inst✝¹ : OmegaCompletePartialOrder β
inst✝ : OmegaCompletePartialOrder γ
c₀ : Chain α
c₁ : Chain β
⊢ ∀ (c : α × β), ωSup (Chain.zip c₀ c₁) ≤ c ↔ (ωSup c₀, ωSup c₁) ≤ c
α : Type u_1
β : Type u_2
γ : Type ?u.22086
inst✝² : OmegaCompletePartialOrder α
inst✝¹ : OmegaCompletePartialOrder β
inst✝ : OmegaCompletePartialOrder γ
c₀ : Chain α
c₁ : Chain β
⊢ ωSup (Chain.zip c₀ c₁) = (ωSup c₀, ωSup c₁)
apply eq_of_forall_ge_iff
case H.mk
α : Type u_1
β : Type u_2
γ : Type ?u.22086
inst✝² : OmegaCompletePartialOrder α
inst✝¹ : OmegaCompletePartialOrder β
inst✝ : OmegaCompletePartialOrder γ
c₀ : Chain α
c₁ : Chain β
z₁ : α
z₂ : β
⊢ ωSup (Chain.zip c₀ c₁) ≤ (z₁, z₂) ↔ (ωSup c₀, ωSup c₁) ≤ (z₁, z₂)
case H
α : Type u_1
β : Type u_2
γ : Type ?u.22086
inst✝² : OmegaCompletePartialOrder α
inst✝¹ : OmegaCompletePartialOrder β
inst✝ : OmegaCompletePartialOrder γ
c₀ : Chain α
c₁ : Chain β
⊢ ∀ (c : α × β), ωSup (Chain.zip c₀ c₁) ≤ c ↔ (ωSup c₀, ωSup c₁) ≤ c
rintro ⟨z₁, z₂⟩
no goals
case H.mk
α : Type u_1
β : Type u_2
γ : Type ?u.22086
inst✝² : OmegaCompletePartialOrder α
inst✝¹ : OmegaCompletePartialOrder β
inst✝ : OmegaCompletePartialOrder γ
c₀ : Chain α
c₁ : Chain β
z₁ : α
z₂ : β
⊢ ωSup (Chain.zip c₀ c₁) ≤ (z₁, z₂) ↔ (ωSup c₀, ωSup c₁) ≤ (z₁, z₂)
simp [ωSup_le_iff, forall_and]