instantiate general lemmas

src/measure_theory/outer_measure.lean

@@ -63,7 +63,7 @@ namespace outer_measure
 
 section basic
 
-variables {α : Type*} {ms : set (outer_measure α)} {m : outer_measure α}
+variables {α : Type*} {β : Type*} {ms : set (outer_measure α)} {m : outer_measure α}
 
 instance : has_coe_to_fun (outer_measure α) := ⟨_, λ m, m.measure_of⟩
 
@@ -77,19 +77,19 @@ theorem mono' (m : outer_measure α) {s₁ s₂}
 protected theorem Union (m : outer_measure α)
   {β} [encodable β] (s : β → set α) :
   m (⋃i, s i) ≤ (∑'i, m (s i)) :=
-by rw [Union_decode2, tsum_Union_decode2 _ m.empty' s]; exact m.Union_nat _
+supr_R_tsum m m.empty (≤) m.Union_nat s
 
 lemma Union_null (m : outer_measure α)
   {β} [encodable β] {s : β → set α} (h : ∀ i, m (s i) = 0) : m (⋃i, s i) = 0 :=
 by simpa [h] using m.Union s
 
+protected lemma Union_finset (m : outer_measure α) (s : β → set α) (t : finset β) :
+  m (⋃i ∈ t, s i) ≤ t.sum (λ d, m (s d)) :=
+supr_R_sum m m.empty (≤) m.Union_nat s t
+
 protected lemma union (m : outer_measure α) (s₁ s₂ : set α) :
   m (s₁ ∪ s₂) ≤ m s₁ + m s₂ :=
-begin
-  convert m.Union (λ b, cond b s₁ s₂),
-  { simp [union_eq_Union] },
-  { rw tsum_fintype, change _ = _ + _, simp }
-end
+sup_R_add m m.empty (≤) m.Union_nat s₁ s₂
 
 lemma le_inter_add_diff {m : outer_measure α} {t : set α} (s : set α) :
   m t ≤ m (t ∩ s) + m (t \ s) :=