chore(order/galois_connection): golf (#9236)

* add `galois_insertion.is_lub_of_u_image`,
  `galois_insertion.is_glb_of_u_image`,
  `galois_coinsertion.is_glb_of_l_image`, and
  `galois_coinsertion.is_lub_of_l_image`;
* get some proofs in `lift_*` from `order_dual` instances;
* this changes definitional equalities for `Inf` and `Sup` so that we can reuse the same `Inf`/`Sup` for a `conditionally_complete_lattice` later.

src/algebra/algebra/subalgebra.lean

@@ -521,9 +521,10 @@ lemma mem_inf {S T : subalgebra R A} {x : A} : x ∈ S ⊓ T ↔ x ∈ S ∧ x 
   (S ⊓ T).to_subsemiring = S.to_subsemiring ⊓ T.to_subsemiring := rfl
 
 @[simp, norm_cast]
-lemma coe_Inf (S : set (subalgebra R A)) : (↑(Inf S) : set A) = ⋂ s ∈ S, ↑s := rfl
+lemma coe_Inf (S : set (subalgebra R A)) : (↑(Inf S) : set A) = ⋂ s ∈ S, ↑s := Inf_image
 
-lemma mem_Inf {S : set (subalgebra R A)} {x : A} : x ∈ Inf S ↔ ∀ p ∈ S, x ∈ p := set.mem_bInter_iff
+lemma mem_Inf {S : set (subalgebra R A)} {x : A} : x ∈ Inf S ↔ ∀ p ∈ S, x ∈ p :=
+by simp only [← set_like.mem_coe, coe_Inf, set.mem_bInter_iff]
 
 @[simp] lemma Inf_to_submodule (S : set (subalgebra R A)) :
   (Inf S).to_submodule = Inf (subalgebra.to_submodule '' S) :=
@@ -535,7 +536,7 @@ set_like.coe_injective $ by simp
 
 @[simp, norm_cast]
 lemma coe_infi {ι : Sort*} {S : ι → subalgebra R A} : (↑(⨅ i, S i) : set A) = ⋂ i, S i :=
-set.bInter_range
+by simp [infi]
 
 lemma mem_infi {ι : Sort*} {S : ι → subalgebra R A} {x : A} : (x ∈ ⨅ i, S i) ↔ ∀ i, x ∈ S i :=
 by simp only [infi, mem_Inf, set.forall_range_iff]

src/measure_theory/measurable_space_def.lean

@@ -363,12 +363,11 @@ iff.rfl
 
 @[simp] theorem measurable_set_Inf {ms : set (measurable_space α)} {s : set α} :
   @measurable_set _ (Inf ms) s ↔ ∀ m ∈ ms, @measurable_set _ m s :=
-show s ∈ (⋂ m ∈ ms, {t | @measurable_set _ m t }) ↔ _, by simp
+show s ∈ (⋂₀ _) ↔ _, by simp
 
 @[simp] theorem measurable_set_infi {ι} {m : ι → measurable_space α} {s : set α} :
   @measurable_set _ (infi m) s ↔ ∀ i, @measurable_set _ (m i) s :=
-show s ∈ (λ m, {s | @measurable_set _ m s }) (infi m) ↔ _,
-by { rw (@gi_generate_from α).gc.u_infi, simp }
+by rw [infi, measurable_set_Inf, forall_range_iff]
 
 theorem measurable_set_sup {m₁ m₂ : measurable_space α} {s : set α} :
   @measurable_set _ (m₁ ⊔ m₂) s ↔ generate_measurable (m₁.measurable_set' ∪ m₂.measurable_set') s :=
@@ -378,17 +377,14 @@ theorem measurable_set_Sup {ms : set (measurable_space α)} {s : set α} :
   @measurable_set _ (Sup ms) s ↔
     generate_measurable {s : set α | ∃ m ∈ ms, @measurable_set _ m s} s :=
 begin
-  change @measurable_set' _ (generate_from $ ⋃ m ∈ ms, _) _ ↔ _,
+  change @measurable_set' _ (generate_from $ ⋃₀ _) _ ↔ _,
   simp [generate_from, ← set_of_exists]
 end
 
 theorem measurable_set_supr {ι} {m : ι → measurable_space α} {s : set α} :
   @measurable_set _ (supr m) s ↔
     generate_measurable {s : set α | ∃ i, @measurable_set _ (m i) s} s :=
-begin
-  convert @measurable_set_Sup _ (range m) s,
-  simp,
-end
+by simp only [supr, measurable_set_Sup, exists_range_iff]
 
 end complete_lattice
 

src/order/filter/basic.lean

@@ -401,7 +401,8 @@ instance : complete_lattice (filter α) := original_complete_lattice.copy
                            (@inf_le_right (filter α) _ _ _ _ hb)
        end)
   end
-  /- Sup -/ (join ∘ 𝓟) (by ext s x; exact (@mem_bInter_iff _ _ s filter.sets x).symm)
+  /- Sup -/ (join ∘ 𝓟) (by { ext s x, exact (@mem_bInter_iff _ _ s filter.sets x).symm.trans
+    (set.ext_iff.1 (sInter_image _ _) x).symm})
   /- Inf -/ _ rfl
 
 end complete_lattice
@@ -476,7 +477,7 @@ by simp only [← filter.mem_sets, supr_sets_eq, iff_self, mem_Inter]
 by simp [ne_bot_iff]
 
 lemma infi_eq_generate (s : ι → filter α) : infi s = generate (⋃ i, (s i).sets) :=
-show generate _ = generate _, from congr_arg _ supr_range
+show generate _ = generate _, from congr_arg _ $ congr_arg Sup $ (range_comp _ _).symm
 
 lemma mem_infi_of_mem {f : ι → filter α} (i : ι) : ∀ {s}, s ∈ f i → s ∈ ⨅ i, f i :=
 show (⨅ i, f i) ≤ f i, from infi_le _ _

src/order/galois_connection.lean

@@ -354,6 +354,17 @@ lemma u_le_u_iff [preorder α] [preorder β] (gi : galois_insertion l u) {a b} :
 lemma strict_mono_u [preorder α] [preorder β] (gi : galois_insertion l u) : strict_mono u :=
 strict_mono_of_le_iff_le $ λ _ _, gi.u_le_u_iff.symm
 
+lemma is_lub_of_u_image [preorder α] [preorder β] (gi : galois_insertion l u) {s : set β} {a : α}
+  (hs : is_lub (u '' s) a) : is_lub s (l a) :=
+⟨λ x hx, (gi.le_l_u x).trans $ gi.gc.monotone_l $ hs.1 $ mem_image_of_mem _ hx,
+  λ x hx, gi.gc.l_le $ hs.2 $ gi.gc.monotone_u.mem_upper_bounds_image hx⟩
+
+lemma is_glb_of_u_image [preorder α] [preorder β] (gi : galois_insertion l u) {s : set β} {a : α}
+  (hs : is_glb (u '' s) a) : is_glb s (l a) :=
+⟨λ x hx, gi.gc.l_le $ hs.1 $ mem_image_of_mem _ hx,
+  λ x hx, (gi.le_l_u x).trans $ gi.gc.monotone_l $ hs.2 $
+    gi.gc.monotone_u.mem_lower_bounds_image hx⟩
+
 section lift
 
 variables [partial_order β]
@@ -394,17 +405,13 @@ def lift_bounded_lattice [bounded_lattice α] (gi : galois_insertion l u) : boun
 
 /-- Lift all suprema and infima along a Galois insertion -/
 def lift_complete_lattice [complete_lattice α] (gi : galois_insertion l u) : complete_lattice β :=
-{ Sup := λ s, l (⨆ b ∈ s, u b),
-  Sup_le := λ s a hs, gi.gc.l_le $ supr_le $ λ b, supr_le $ λ hb, gi.gc.monotone_u $ hs _ hb,
-  le_Sup := λ s a ha, (gi.le_l_u a).trans $
-    gi.gc.monotone_l $ le_supr_of_le a $ le_supr_of_le ha $ le_refl _,
-  Inf := λ s, gi.choice (⨅ b ∈ s, u b) $ le_infi $ λ b, le_infi $ λ hb,
-    gi.gc.monotone_u $ gi.gc.l_le $ infi_le_of_le b $ infi_le_of_le hb $ le_refl _,
-  Inf_le := by simp only [gi.choice_eq]; exact
-    λ s a ha, gi.gc.l_le $ infi_le_of_le a $ infi_le_of_le ha $ le_refl _,
-  le_Inf := by simp only [gi.choice_eq]; exact
-    λ s a hs, (gi.le_l_u a).trans $ gi.gc.monotone_l $ le_infi $ λ b,
-    show u a ≤ ⨅ (H : b ∈ s), u b, from le_infi $ λ hb, gi.gc.monotone_u $ hs _ hb,
+{ Sup := λ s, l (Sup (u '' s)),
+  Sup_le := λ s, (gi.is_lub_of_u_image (is_lub_Sup _)).2,
+  le_Sup := λ s, (gi.is_lub_of_u_image (is_lub_Sup _)).1,
+  Inf := λ s, gi.choice (Inf (u '' s)) $ gi.gc.monotone_u.le_is_glb_image
+    (gi.is_glb_of_u_image $ is_glb_Inf _) (is_glb_Inf _),
+  Inf_le := λ s, by { rw gi.choice_eq, exact (gi.is_glb_of_u_image (is_glb_Inf _)).1 },
+  le_Inf := λ s, by { rw gi.choice_eq, exact (gi.is_glb_of_u_image (is_glb_Inf _)).2 },
   .. gi.lift_bounded_lattice }
 
 end lift
@@ -523,29 +530,30 @@ gi.dual.u_le_u_iff
 lemma strict_mono_l [partial_order α] [preorder β] (gi : galois_coinsertion l u) : strict_mono l :=
 λ a b h, gi.dual.strict_mono_u h
 
+lemma is_glb_of_l_image [preorder α] [preorder β] (gi : galois_coinsertion l u) {s : set α} {a : β}
+  (hs : is_glb (l '' s) a) : is_glb s (u a) :=
+gi.dual.is_lub_of_u_image hs
+
+lemma is_lub_of_l_image [preorder α] [preorder β] (gi : galois_coinsertion l u) {s : set α} {a : β}
+  (hs : is_lub (l '' s) a) : is_lub s (u a) :=
+gi.dual.is_glb_of_u_image hs
+
+
 section lift
 
 variables [partial_order α]
 
 /-- Lift the infima along a Galois coinsertion -/
 def lift_semilattice_inf [semilattice_inf β] (gi : galois_coinsertion l u) : semilattice_inf α :=
 { inf := λ a b, u (l a ⊓ l b),
-  inf_le_left  := λ a b, (gi.gc.monotone_u $ inf_le_left).trans (gi.u_l_le a),
-  inf_le_right := λ a b, (gi.gc.monotone_u $ inf_le_right).trans (gi.u_l_le b),
-  le_inf       := λ a b c hac hbc, gi.gc.le_u $ le_inf (gi.gc.monotone_l hac)
-    (gi.gc.monotone_l hbc),
-  .. ‹partial_order α› }
+  .. ‹partial_order α›, .. @order_dual.semilattice_inf _ gi.dual.lift_semilattice_sup }
 
 /-- Lift the suprema along a Galois coinsertion -/
 def lift_semilattice_sup [semilattice_sup β] (gi : galois_coinsertion l u) : semilattice_sup α :=
 { sup := λ a b, gi.choice (l a ⊔ l b) $
     (sup_le (gi.gc.monotone_l $ gi.gc.le_u $ le_sup_left)
       (gi.gc.monotone_l $ gi.gc.le_u $ le_sup_right)),
-  le_sup_left  := by simp only [gi.choice_eq]; exact λ a b, gi.gc.le_u le_sup_left,
-  le_sup_right := by simp only [gi.choice_eq]; exact λ a b, gi.gc.le_u le_sup_right,
-  sup_le       := by simp only [gi.choice_eq]; exact λ a b c hac hbc,
-    (gi.gc.monotone_u $ sup_le (gi.gc.monotone_l hac) (gi.gc.monotone_l hbc)).trans (gi.u_l_le c),
-  .. ‹partial_order α› }
+  .. ‹partial_order α›, .. @order_dual.semilattice_sup _ gi.dual.lift_semilattice_inf }
 
 /-- Lift the suprema and infima along a Galois coinsertion -/
 def lift_lattice [lattice β] (gi : galois_coinsertion l u) : lattice α :=
@@ -554,30 +562,17 @@ def lift_lattice [lattice β] (gi : galois_coinsertion l u) : lattice α :=
 /-- Lift the bot along a Galois coinsertion -/
 def lift_order_bot [order_bot β] (gi : galois_coinsertion l u) : order_bot α :=
 { bot    := gi.choice ⊥ $ bot_le,
-  bot_le := by simp only [gi.choice_eq];
-    exact λ b, (gi.gc.monotone_u bot_le).trans (gi.u_l_le b),
-  .. ‹partial_order α› }
+  .. ‹partial_order α›, .. @order_dual.order_bot _ gi.dual.lift_order_top }
 
 /-- Lift the top, bottom, suprema, and infima along a Galois coinsertion -/
 def lift_bounded_lattice [bounded_lattice β] (gi : galois_coinsertion l u) : bounded_lattice α :=
 { .. gi.lift_lattice, .. gi.lift_order_bot, .. gi.gc.lift_order_top }
 
 /-- Lift all suprema and infima along a Galois coinsertion -/
 def lift_complete_lattice [complete_lattice β] (gi : galois_coinsertion l u) : complete_lattice α :=
-{ Inf := λ s, u (⨅ a ∈ s, l a),
-  le_Inf := λ s a hs, gi.gc.le_u $ le_infi $ λ b, le_infi $
-    λ hb, gi.gc.monotone_l $ hs _ hb,
-  Inf_le := λ s a ha, (gi.gc.monotone_u $ infi_le_of_le a $
-    infi_le_of_le ha $ le_refl (l a)).trans (gi.u_l_le a),
-  Sup := λ s, gi.choice (⨆ a ∈ s, l a) $ supr_le $ λ b, supr_le $ λ hb,
-    gi.gc.monotone_l $ gi.gc.le_u $ le_supr_of_le b $ le_supr_of_le hb $ le_refl _,
-  le_Sup := by simp only [gi.choice_eq]; exact
-    λ s a ha, gi.gc.le_u $ le_supr_of_le a $ le_supr_of_le ha $ le_refl _,
-  Sup_le := by simp only [gi.choice_eq]; exact
-    λ s a hs, (gi.gc.monotone_u $ supr_le $ λ b,
-        show (⨆ (hb : b ∈ s), l b) ≤ l a, from supr_le $ λ hb, gi.gc.monotone_l $ hs b hb).trans
-      (gi.u_l_le a),
-  .. gi.lift_bounded_lattice }
+{ Inf := λ s, u (Inf (l '' s)),
+  Sup := λ s, gi.choice (Sup (l '' s)) _,
+  .. gi.lift_bounded_lattice, .. @order_dual.complete_lattice _ gi.dual.lift_complete_lattice }
 
 end lift
 

src/topology/opens.lean

@@ -83,14 +83,7 @@ begin
   apply subtype.ext_iff_val.mpr,
   exact (is_open.inter U.2 V.2).interior_eq.symm,
 end
-/- Sup -/ (λ Us, ⟨⋃₀ (coe '' Us), is_open_sUnion $ λ U hU,
-by { rcases hU with ⟨⟨V, hV⟩, h, h'⟩, dsimp at h', subst h', exact hV}⟩)
-begin
-  funext,
-  apply subtype.ext_iff_val.mpr,
-  simp [Sup_range],
-  refl,
-end
+/- Sup -/ _ rfl
 /- Inf -/ _ rfl
 
 lemma le_def {U V : opens α} : U ≤ V ↔ (U : set α) ≤ (V : set α) :=
@@ -139,6 +132,7 @@ lemma open_embedding_of_le {U V : opens α} (i : U ≤ V) :
     exact U.property.preimage continuous_subtype_val
   end, }
 
+/-- A set of `opens α` is a basis if the set of corresponding sets is a topological basis. -/
 def is_basis (B : set (opens α)) : Prop := is_topological_basis ((coe : _ → set α) '' B)
 
 lemma is_basis_iff_nbhd {B : set (opens α)} :