feat(order/complete_lattice): add sup_eq_supr and inf_eq_infi (#8573

)

* add `bool.injective_iff`, `bool.univ_eq`, and `bool.range_eq`;
* add `sup_eq_supr` and `inf_eq_infi`;
* golf `filter.comap_sup`.

src/data/bool.lean

@@ -195,4 +195,8 @@ by cases h; subst h; [cases b₁, cases b₀]; simp [to_nat,nat.zero_le]
 lemma of_nat_to_nat (b : bool) : of_nat (to_nat b) = b :=
 by cases b; simp only [of_nat,to_nat]; exact dec_trivial
 
+@[simp] lemma injective_iff {α : Sort*} {f : bool → α} : function.injective f ↔ f ff ≠ f tt :=
+⟨λ Hinj Heq, ff_ne_tt (Hinj Heq),
+  λ H x y hxy, by { cases x; cases y, exacts [rfl, (H hxy).elim, (H hxy.symm).elim, rfl] }⟩
+
 end bool

src/data/set/bool.lean

@@ -0,0 +1,25 @@
+/-
+Copyright (c) 2021 Yury G. Kudryashov. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yury G. Kudryashov
+-/
+import data.set.basic
+import data.bool
+
+/-!
+# Booleans and set operations
+
+This file contains two trivial lemmas about `bool`, `set.univ`, and `set.range`.
+-/
+
+open set
+
+namespace bool
+
+@[simp] lemma univ_eq : (univ : set bool) = {ff, tt} :=
+(eq_univ_of_forall bool.dichotomy).symm
+
+@[simp] lemma range_eq {α : Type*} (f : bool → α) : range f = {f ff, f tt} :=
+by rw [← image_univ, univ_eq, image_pair]
+
+end bool

src/data/set/lattice.lean

@@ -768,10 +768,10 @@ lemma sInter_eq_Inter {s : set (set α)} : (⋂₀ s) = (⋂ (i : s), i) :=
 by simp only [←sInter_range, subtype.range_coe]
 
 lemma union_eq_Union {s₁ s₂ : set α} : s₁ ∪ s₂ = ⋃ b : bool, cond b s₁ s₂ :=
-(@supr_bool_eq _ _ (λ b, cond b s₁ s₂)).symm
+sup_eq_supr s₁ s₂
 
 lemma inter_eq_Inter {s₁ s₂ : set α} : s₁ ∩ s₂ = ⋂ b : bool, cond b s₁ s₂ :=
-(@infi_bool_eq _ _ (λ b, cond b s₁ s₂)).symm
+inf_eq_infi s₁ s₂
 
 lemma sInter_union_sInter {S T : set (set α)} :
   (⋂₀S) ∪ (⋂₀T) = (⋂p ∈ S.prod T, (p : (set α) × (set α)).1 ∪ p.2) :=

src/order/complete_lattice.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl
 -/
 import order.bounds
+import data.set.bool
 
 /-!
 # Theory of complete lattices
@@ -973,13 +974,17 @@ infi_of_empty nonempty_empty
 supr_of_empty nonempty_empty
 
 lemma supr_bool_eq {f : bool → α} : (⨆b:bool, f b) = f tt ⊔ f ff :=
-le_antisymm
-  (supr_le $ assume b, match b with tt := le_sup_left | ff := le_sup_right end)
-  (sup_le (le_supr _ _) (le_supr _ _))
+by rw [supr, bool.range_eq, Sup_pair, sup_comm]
 
 lemma infi_bool_eq {f : bool → α} : (⨅b:bool, f b) = f tt ⊓ f ff :=
 @supr_bool_eq (order_dual α) _ _
 
+lemma sup_eq_supr (x y : α) : x ⊔ y = ⨆ b : bool, cond b x y :=
+by rw [supr_bool_eq, bool.cond_tt, bool.cond_ff]
+
+lemma inf_eq_infi (x y : α) : x ⊓ y = ⨅ b : bool, cond b x y :=
+@sup_eq_supr (order_dual α) _ _ _
+
 lemma is_glb_binfi {s : set β} {f : β → α} : is_glb (f '' s) (⨅ x ∈ s, f x) :=
 by simpa only [range_comp, subtype.range_coe, infi_subtype'] using @is_glb_infi α s _ (f ∘ coe)
 

src/order/filter/basic.lean

@@ -1623,13 +1623,7 @@ lemma comap_Sup {s : set (filter β)} {m : α → β} : comap m (Sup s) = (⨆f
 by simp only [Sup_eq_supr, comap_supr, eq_self_iff_true]
 
 lemma comap_sup : comap m (g₁ ⊔ g₂) = comap m g₁ ⊔ comap m g₂ :=
-le_antisymm
-  (assume s ⟨⟨t₁, ht₁, hs₁⟩, ⟨t₂, ht₂, hs₂⟩⟩,
-    ⟨t₁ ∪ t₂,
-      ⟨mem_sets_of_superset ht₁ (subset_union_left _ _),
-        mem_sets_of_superset ht₂ (subset_union_right _ _)⟩,
-      union_subset hs₁ hs₂⟩)
-  ((@comap_mono _ _ m).le_map_sup _ _)
+by rw [sup_eq_supr, comap_supr, supr_bool_eq, bool.cond_tt, bool.cond_ff]
 
 lemma map_comap (f : filter β) (m : α → β) : (f.comap m).map m = f ⊓ 𝓟 (range m) :=
 begin