feat(data/set/lattice): add @[simp] to lemmas (#2091)

* feat(data/set/lattice): add @[simp] to lemmas

* fix proof

* fix proof

* fix proof

* oops

* fix proofs

* typo in doc string

Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>

Author: kim-em

src/data/set/finite.lean

@@ -365,7 +365,7 @@ begin
   refine ⟨range f, finite_range f, _⟩,
   rintro x hx,
   simp,
-  exact ⟨_, ⟨_, hx, rfl⟩, hf ⟨x, hx⟩⟩
+  exact ⟨x, ⟨hx, hf _⟩⟩,
 end
 
 lemma finite_range_ite {p : α → Prop} [decidable_pred p] {f g : α → β} (hf : finite (range f))

src/data/set/lattice.lean

@@ -603,18 +603,18 @@ set.ext $ assume a, by simp [@eq_comm α a]
 lemma image_eq_Union (f : α → β) (s : set α) : f '' s = (⋃i∈s, {f i}) :=
 set.ext $ assume b, by simp [@eq_comm β b]
 
-lemma bUnion_range {f : ι → α} {g : α → set β} : (⋃x ∈ range f, g x) = (⋃y, g (f y)) :=
+@[simp] lemma bUnion_range {f : ι → α} {g : α → set β} : (⋃x ∈ range f, g x) = (⋃y, g (f y)) :=
 by rw [← sUnion_image, ← range_comp, sUnion_range]
 
-lemma bInter_range {f : ι → α} {g : α → set β} : (⋂x ∈ range f, g x) = (⋂y, g (f y)) :=
+@[simp] lemma bInter_range {f : ι → α} {g : α → set β} : (⋂x ∈ range f, g x) = (⋂y, g (f y)) :=
 by rw [← sInter_image, ← range_comp, sInter_range]
 
 variables {s : set γ} {f : γ → α} {g : α → set β}
 
-lemma bUnion_image : (⋃x∈ (f '' s), g x) = (⋃y ∈ s, g (f y)) :=
+@[simp] lemma bUnion_image : (⋃x∈ (f '' s), g x) = (⋃y ∈ s, g (f y)) :=
 by rw [← sUnion_image, ← image_comp, sUnion_image]
 
-lemma bInter_image : (⋂x∈ (f '' s), g x) = (⋂y ∈ s, g (f y)) :=
+@[simp] lemma bInter_image : (⋂x∈ (f '' s), g x) = (⋂y ∈ s, g (f y)) :=
 by rw [← sInter_image, ← image_comp, sInter_image]
 
 end image

src/measure_theory/integration.lean

@@ -74,7 +74,7 @@ begin
   { exact is_measurable.bUnion (countable_finite f.finite)
       (λ b _, is_measurable.inter (h b) (f.measurable_sn _)) },
   ext a, simp,
-  exact ⟨λ h, ⟨_, ⟨a, rfl⟩, h, rfl⟩, λ ⟨_, ⟨a', rfl⟩, h', e⟩, e.symm ▸ h'⟩
+  exact ⟨λ h, ⟨a, ⟨h, rfl⟩⟩, λ ⟨a', ⟨h', e⟩⟩, e.symm ▸ h'⟩
 end
 
 theorem preimage_measurable (f : α →ₛ β) (s) : is_measurable (f ⁻¹' s) :=
@@ -103,12 +103,12 @@ def bind (f : α →ₛ β) (g : β → α →ₛ γ) : α →ₛ γ :=
 ⟨λa, g (f a) a,
  λ c, is_measurable_cut (λa b, g b a ∈ ({c} : set γ)) f (λ b, (g b).measurable_sn c),
  finite_subset (finite_bUnion f.finite (λ b, (g b).finite)) $
- by rintro _ ⟨a, rfl⟩; simp; exact ⟨_, ⟨a, rfl⟩, _, rfl⟩⟩
+ by rintro _ ⟨a, rfl⟩; simp; exact ⟨a, a, rfl⟩⟩
 
 @[simp] theorem bind_apply (f : α →ₛ β) (g : β → α →ₛ γ) (a) :
   f.bind g a = g (f a) a := rfl
 
-/-- Restrict a simple function `f : α →ₛ β`` to a set `s`. If `s` is measurable,
+/-- Restrict a simple function `f : α →ₛ β` to a set `s`. If `s` is measurable,
 then `f.restrict s a = if a ∈ s then f a else 0`, otherwise `f.restrict s = const α 0`. -/
 def restrict [has_zero β] (f : α →ₛ β) (s : set α) : α →ₛ β :=
 if hs : is_measurable s then ite hs f (const α 0) else const α 0

src/topology/instances/real.lean

@@ -233,7 +233,7 @@ metric.totally_bounded_iff.2 $ λ ε ε0, begin
   let i : ℕ := ⌊(x - a) / ε⌋.to_nat,
   have : (i : ℤ) = ⌊(x - a) / ε⌋ :=
     int.to_nat_of_nonneg (floor_nonneg.2 $ le_of_lt (div_pos (sub_pos.2 ax) ε0)),
-  simp, refine ⟨_, ⟨i, _, rfl⟩, _⟩,
+  simp, use i, split,
   { rw [← int.coe_nat_lt, this],
     refine int.cast_lt.1 (lt_of_le_of_lt (floor_le _) _),
     rw [int.cast_coe_nat, div_lt_iff' ε0, sub_lt_iff_lt_add'],

src/topology/uniform_space/cauchy.lean

@@ -293,8 +293,8 @@ let ⟨c, hfc, hct⟩ := hs _ this in
   begin
     simp [image_subset_iff],
     simp [subset_def] at hct,
-    intros x hx, simp [-mem_image],
-    exact let ⟨i, hi, ht⟩ := hct x hx in ⟨f i, mem_image_of_mem f hi, ht⟩
+    intros x hx, simp,
+    exact hct x hx
   end⟩
 
 lemma cauchy_of_totally_bounded_of_ultrafilter {s : set α} {f : filter α}