chore(Order): golf entire IsBoundedUnder.eventually_le and ωSup_zip using tauto and rfl (#28568)

Co-authored-by: euprunin <euprunin@users.noreply.github.com>

Author: euprunin

Mathlib/Order/Filter/IsBounded.lean

@@ -91,9 +91,7 @@ variable [Preorder α] {f : Filter β} {u : β → α} {s : Set β}
 
 lemma IsBoundedUnder.eventually_le (h : IsBoundedUnder (· ≤ ·) f u) :
     ∃ a, ∀ᶠ x in f, u x ≤ a := by
-  obtain ⟨a, ha⟩ := h
-  use a
-  exact eventually_map.1 ha
+  tauto
 
 lemma IsBoundedUnder.eventually_ge (h : IsBoundedUnder (· ≥ ·) f u) :
     ∃ a, ∀ᶠ x in f, a ≤ u x :=

Mathlib/Order/OmegaCompletePartialOrder.lean

@@ -424,9 +424,7 @@ instance : OmegaCompletePartialOrder (α × β) where
   ωSup_le := fun _ _ h => ⟨ωSup_le _ _ fun i => (h i).1, ωSup_le _ _ fun i => (h i).2⟩
   le_ωSup c i := ⟨le_ωSup (c.map OrderHom.fst) i, le_ωSup (c.map OrderHom.snd) i⟩
 
-theorem ωSup_zip (c₀ : Chain α) (c₁ : Chain β) : ωSup (c₀.zip c₁) = (ωSup c₀, ωSup c₁) := by
-  apply eq_of_forall_ge_iff; rintro ⟨z₁, z₂⟩
-  simp [ωSup_le_iff, forall_and]
+theorem ωSup_zip (c₀ : Chain α) (c₁ : Chain β) : ωSup (c₀.zip c₁) = (ωSup c₀, ωSup c₁) := rfl
 
 end Prod