refactor(data/set/basic): clean up #288 and #289

data/set/basic.lean

@@ -883,6 +883,7 @@ set.ext $ assume a,
 
 lemma preimage_subset_iff {A : set α} {B : set β} {f : α → β} :
   f⁻¹' B ⊆ A ↔ (∀ a : α, f a ∈ B → a ∈ A) := iff.rfl
+
 end image
 
 theorem univ_eq_true_false : univ = ({true, false} : set Prop) :=
@@ -956,7 +957,7 @@ theorem mem_prod_eq {p : α × β} : p ∈ set.prod s t = (p.1 ∈ s ∧ p.2 ∈
 
 @[simp] theorem mem_prod {p : α × β} : p ∈ set.prod s t ↔ p.1 ∈ s ∧ p.2 ∈ t := iff.rfl
 
-lemma mem_prod' {a : α} {b : β} (a_in : a ∈ s) (b_in : b ∈ t) : (a, b) ∈ set.prod s t := ⟨a_in, b_in⟩
+lemma mk_mem_prod {a : α} {b : β} (a_in : a ∈ s) (b_in : b ∈ t) : (a, b) ∈ set.prod s t := ⟨a_in, b_in⟩
 
 @[simp] theorem prod_empty {s : set α} : set.prod s ∅ = (∅ : set (α × β)) :=
 set.ext $ by simp [set.prod]
@@ -1013,12 +1014,12 @@ by simp [not_eq_empty_iff_exists]
 @[simp] theorem prod_mk_mem_set_prod_eq {a : α} {b : β} {s : set α} {t : set β} :
   (a, b) ∈ set.prod s t = (a ∈ s ∧ b ∈ t) := rfl
 
-@[simp] theorem univ_prod_univ : set.prod univ univ = (univ : set (α×β)) :=
+@[simp] theorem univ_prod_univ : set.prod (@univ α) (@univ β) = univ :=
 set.ext $ assume ⟨a, b⟩, by simp
 
 lemma prod_sub_preimage_iff {W : set γ} {f : α × β → γ} :
-set.prod s t ⊆ f ⁻¹' W ↔ ∀ a b, a ∈ s → b ∈ t → f (a, b) ∈ W :=
-⟨λ h a b a_in b_in, h (mem_prod' a_in b_in),
- λ h p p_in, by have := h p.1 p.2 p_in.1 p_in.2 ; rwa prod.mk.eta at this⟩
+  set.prod s t ⊆ f ⁻¹' W ↔ ∀ a b, a ∈ s → b ∈ t → f (a, b) ∈ W :=
+by simp [subset_def]
+
 end prod
 end set

order/filter.lean

@@ -767,7 +767,7 @@ vmap_neq_bot $ assume t ht,
 lemma map_ne_bot (hf : f ≠ ⊥) : map m f ≠ ⊥ :=
 assume h, hf $ by rwa [map_eq_bot_iff] at h
 
-lemma inter_vmap_sets (f : α → β) (F : filter β) : 
+lemma sInter_vmap_sets (f : α → β) (F : filter β) :
   ⋂₀(vmap f F).sets = ⋂ U ∈ F.sets, f ⁻¹' U :=
 begin
   ext x,
@@ -1001,7 +1001,7 @@ have tendsto m (map i $ vmap i $ f) g,
   by rwa [tendsto, ←map_compose] at h,
 le_trans (map_mono $ le_map_vmap' hs hi) this
 
-lemma vmap_eq_of_inverse {f : filter α} {g : filter β} 
+lemma vmap_eq_of_inverse {f : filter α} {g : filter β}
   {φ : α → β} {ψ : β → α} (inv₁ : φ ∘ ψ = id) (inv₂ : ψ ∘ φ = id)
   (lim₁ : tendsto φ f g) (lim₂ : tendsto ψ g f) : vmap φ g = f :=
 begin
@@ -1506,12 +1506,12 @@ calc filter.prod f g ≠ ⊥ ↔ (∀s∈f.sets, g.lift' (set.prod s) ≠ ⊥) :
   ... ↔ _ : by simp only  [forall_sets_neq_empty_iff_neq_bot]
 
 lemma tendsto_prod_iff {f : α × β → γ} {x : filter α} {y : filter β} {z : filter γ} :
-  filter.tendsto f (filter.prod x y) z  ↔ 
+  filter.tendsto f (filter.prod x y) z ↔
   ∀ W ∈ z.sets, ∃ U ∈ x.sets,  ∃ V ∈ y.sets, ∀ x y, x ∈ U → y ∈ V → f (x, y) ∈ W :=
 by simp [tendsto_def, mem_prod_iff, set.prod_sub_preimage_iff]
 
 lemma tendsto_prod_self_iff {f : α × α → β} {x : filter α} {y : filter β} :
-  filter.tendsto f (filter.prod x x) y  ↔ 
+  filter.tendsto f (filter.prod x x) y ↔
   ∀ W ∈ y.sets, ∃ U ∈ x.sets, ∀ (x x' : α), x ∈ U → x' ∈ U → f (x, x') ∈ W :=
 by simp [tendsto_def, mem_prod_same_iff, set.prod_sub_preimage_iff]