feat(data/set): two simple lemmas (#11531)

src/data/set/lattice.lean

@@ -1035,6 +1035,18 @@ by { rw sInter_eq_bInter, apply image_bInter_subset }
 
 /-! ### `inj_on` -/
 
+lemma inj_on.image_inter {f : α → β} {s t u : set α} (hf : inj_on f u) (hs : s ⊆ u) (ht : t ⊆ u) :
+  f '' (s ∩ t) = f '' s ∩ f '' t :=
+begin
+  apply subset.antisymm (image_inter_subset _ _ _),
+  rintros x ⟨⟨y, ys, hy⟩, ⟨z, zt, hz⟩⟩,
+  have : y = z,
+  { apply hf (hs ys) (ht zt),
+    rwa ← hz at hy },
+  rw ← this at zt,
+  exact ⟨y, ⟨ys, zt⟩, hy⟩,
+end
+
 lemma inj_on.image_Inter_eq [nonempty ι] {s : ι → set α} {f : α → β} (h : inj_on f (⋃ i, s i)) :
   f '' (⋂ i, s i) = ⋂ i, f '' (s i) :=
 begin
@@ -1526,6 +1538,13 @@ lemma disjoint_iff_subset_compl_left :
   disjoint s t ↔ t ⊆ sᶜ :=
 disjoint_right
 
+lemma _root_.disjoint.image {s t u : set α} {f : α → β} (h : disjoint s t) (hf : inj_on f u)
+  (hs : s ⊆ u) (ht : t ⊆ u) : disjoint (f '' s) (f '' t) :=
+begin
+  rw disjoint_iff_inter_eq_empty at h ⊢,
+  rw [← hf.image_inter hs ht, h, image_empty],
+end
+
 end set
 
 end disjoint

src/data/set/pairwise.lean

@@ -24,7 +24,7 @@ open set
 variables {α ι ι' : Type*} {r p q : α → α → Prop}
 
 section pairwise
-variables {f : ι → α} {s t u : set α} {a b : α}
+variables {f g : ι → α} {s t u : set α} {a b : α}
 
 /-- A relation `r` holds pairwise if `r i j` for all `i ≠ j`. -/
 def pairwise (r : α → α → Prop) := ∀ i j, i ≠ j → r i j
@@ -51,6 +51,10 @@ lemma pairwise_disjoint_on [semilattice_inf α] [order_bot α] [linear_order ι]
   pairwise (disjoint on f) ↔ ∀ m n, m < n → disjoint (f m) (f n) :=
 symmetric.pairwise_on disjoint.symm f
 
+lemma pairwise_disjoint.mono [semilattice_inf α] [order_bot α]
+  (hs : pairwise (disjoint on f)) (h : g ≤ f) : pairwise (disjoint on g) :=
+hs.mono (λ i j hij, disjoint.mono (h i) (h j) hij)
+
 namespace set
 
 /-- The relation `r` holds pairwise on the set `s` if `r x y` for all *distinct* `x y ∈ s`. -/

src/measure_theory/measure/haar_lebesgue.lean

@@ -138,7 +138,6 @@ begin
   apply add_haar_eq_zero_of_disjoint_translates_aux μ u
     (bounded.mono (inter_subset_right _ _) bounded_closed_ball) hu _
     (h's.inter (measurable_set_closed_ball)),
-  rw ← pairwise_univ at ⊢ hs,
   apply pairwise_disjoint.mono hs (λ n, _),
   exact add_subset_add (subset.refl _) (inter_subset_left _ _)
 end