[Merged by Bors] - chore(*): some monotonicity lemmas

src/data/set/lattice.lean

@@ -267,6 +267,14 @@ begin
   exact ⟨c, c_in, hc ha⟩
 end
 
+theorem bInter_mono {s : set α} {t t' : α → set β} (h : ∀ x ∈ s, t x ⊆ t' x) :
+  (⋂ x ∈ s, t x) ⊆ (⋂ x ∈ s, t' x) :=
+begin
+  intros x x_in,
+  simp only [mem_Inter] at *,
+  exact λ a a_in, h a a_in (x_in a a_in),
+end
+
 theorem bUnion_mono {s : set α} {t t' : α → set β} (h : ∀ x ∈ s, t x ⊆ t' x) :
   (⋃ x ∈ s, t x) ⊆ (⋃ x ∈ s, t' x) :=
 bUnion_subset_bUnion (λ x x_in, ⟨x, x_in, h x x_in⟩)
@@ -279,7 +287,7 @@ theorem bInter_eq_Inter (s : set α) (t : Π x ∈ s, set β) :
   (⋂ x ∈ s, t x ‹_›) = (⋂ x : s, t x x.2) :=
 infi_subtype'
 
-theorem bInter_empty (u : α → set β) : (⋂ x ∈ (∅ : set α), u x) = univ :=
+@[simp] theorem bInter_empty (u : α → set β) : (⋂ x ∈ (∅ : set α), u x) = univ :=
 show (⨅x ∈ (∅ : set α), u x) = ⊤, -- simplifier should be able to rewrite x ∈ ∅ to false.
   from infi_emptyset
 

src/order/filter/basic.lean

@@ -6,6 +6,7 @@ Authors: Johannes Hölzl, Jeremy Avigad
 import order.zorn
 import order.copy
 import data.set.finite
+import tactic.monotonicity
 
 /-!
 # Theory of filters on sets
@@ -442,7 +443,7 @@ show (∀{t}, s ⊆ t → t ∈ f) ↔ s ∈ f,
 lemma principal_mono {s t : set α} : 𝓟 s ≤ 𝓟 t ↔ s ⊆ t :=
 by simp only [le_principal_iff, iff_self, mem_principal_sets]
 
-lemma monotone_principal : monotone (𝓟 : set α → filter α) :=
+@[mono] lemma monotone_principal : monotone (𝓟 : set α → filter α) :=
 λ _ _, principal_mono.2
 
 @[simp] lemma principal_eq_iff_eq {s t : set α} : 𝓟 s = 𝓟 t ↔ s = t :=
@@ -1403,8 +1404,8 @@ lemma map_le_iff_le_comap : map m f ≤ g ↔ f ≤ comap m g :=
 lemma gc_map_comap (m : α → β) : galois_connection (map m) (comap m) :=
 assume f g, map_le_iff_le_comap
 
-lemma map_mono : monotone (map m) := (gc_map_comap m).monotone_l
-lemma comap_mono : monotone (comap m) := (gc_map_comap m).monotone_u
+@[mono] lemma map_mono : monotone (map m) := (gc_map_comap m).monotone_l
+@[mono] lemma comap_mono : monotone (comap m) := (gc_map_comap m).monotone_u
 
 @[simp] lemma map_bot : map m ⊥ = ⊥ := (gc_map_comap m).l_bot
 @[simp] lemma map_sup : map m (f₁ ⊔ f₂) = map m f₁ ⊔ map m f₂ := (gc_map_comap m).l_sup
@@ -1717,7 +1718,7 @@ lemma le_seq {f : filter (α → β)} {g : filter α} {h : filter β}
 assume s ⟨t, ht, u, hu, hs⟩, mem_sets_of_superset (hh _ ht _ hu) $
   assume b ⟨m, hm, a, ha, eq⟩, eq ▸ hs _ hm _ ha
 
-lemma seq_mono {f₁ f₂ : filter (α → β)} {g₁ g₂ : filter α}
+@[mono] lemma seq_mono {f₁ f₂ : filter (α → β)} {g₁ g₂ : filter α}
   (hf : f₁ ≤ f₂) (hg : g₁ ≤ g₂) : f₁.seq g₁ ≤ f₂.seq g₂ :=
 le_seq $ assume s hs t ht, seq_mem_seq_sets (hf hs) (hg ht)
 
@@ -2141,7 +2142,7 @@ lemma prod_infi_right {f : filter α} {g : ι → filter β} (i : ι) :
   f ×ᶠ (⨅i, g i) = (⨅i, f ×ᶠ (g i)) :=
 by rw [filter.prod, comap_infi, inf_infi i]; simp only [filter.prod, eq_self_iff_true]
 
-lemma prod_mono {f₁ f₂ : filter α} {g₁ g₂ : filter β} (hf : f₁ ≤ f₂) (hg : g₁ ≤ g₂) :
+@[mono] lemma prod_mono {f₁ f₂ : filter α} {g₁ g₂ : filter β} (hf : f₁ ≤ f₂) (hg : g₁ ≤ g₂) :
   f₁ ×ᶠ g₁ ≤ f₂ ×ᶠ g₂ :=
 inf_le_inf (comap_mono hf) (comap_mono hg)
 

src/tactic/monotonicity/lemmas.lean

@@ -5,6 +5,7 @@ Author: Simon Hudon
 -/
 import tactic.monotonicity.basic
 import data.set.lattice
+import order.bounds
 
 variables {α : Type*}
 
@@ -69,4 +70,10 @@ end
 
 open set
 
-attribute [mono] monotone_inter monotone_union bUnion_mono sUnion_mono seq_mono monotone_prod
+attribute [mono] monotone_inter monotone_union
+                 sUnion_mono bUnion_mono sInter_subset_sInter bInter_mono
+                 image_subset preimage_mono prod_mono monotone_prod seq_mono
+attribute [mono] upper_bounds_mono_set lower_bounds_mono_set
+                 upper_bounds_mono_mem  lower_bounds_mono_mem
+                 upper_bounds_mono  lower_bounds_mono
+                 bdd_above.mono bdd_below.mono