Sebastien's suggestions

src/data/equiv/local_equiv.lean

@@ -368,6 +368,15 @@ lemma source_inter_preimage_inv_preimage (s : set α) :
   e.source ∩ e ⁻¹' (e.symm ⁻¹' s) = e.source ∩ s :=
 set.ext $ λ x, and.congr_right_iff.2 $ λ hx, by simp only [mem_preimage, e.left_inv hx]
 
+lemma source_inter_preimage_target_inter (s : set β) :
+  e.source ∩ (e ⁻¹' (e.target ∩ s)) = e.source ∩ (e ⁻¹' s) :=
+begin
+  refine ext_iff.mpr (λ x, ⟨λ hx, _, λ hx, _⟩),
+  simp only [mem_inter_eq, mem_preimage] at *;
+  exact ⟨hx.1, hx.2.2⟩,
+  exact ⟨hx.1, e.map_source hx.1, hx.2⟩, --exacts?
+end
+
 lemma target_inter_inv_preimage_preimage (s : set β) :
   e.target ∩ e.symm ⁻¹' (e ⁻¹' s) = e.target ∩ s :=
 e.symm.source_inter_preimage_inv_preimage _

src/topology/continuous_on.lean

@@ -770,7 +770,7 @@ lemma continuous_on.preimage_open_of_open {f : α → β} {s : set α} {t : set
   (hf : continuous_on f s) (hs : is_open s) (ht : is_open t) : is_open (s ∩ f⁻¹' t) :=
 (continuous_on_open_iff hs).1 hf t ht
 
-lemma continuous_on.open_preimage {f : α → β} {s : set α} {t : set β} (h : continuous_on f s)
+lemma continuous_on.is_open_preimage {f : α → β} {s : set α} {t : set β} (h : continuous_on f s)
   (hs : is_open s) (hp : f ⁻¹' t ⊆ s) (ht : is_open t) : is_open (f ⁻¹' t) :=
 begin
   convert (continuous_on_open_iff hs).mp h t ht,

src/topology/local_homeomorph.lean

@@ -211,12 +211,7 @@ e.symm.source_inter_preimage_inv_preimage _
 
 lemma source_inter_preimage_target_inter (s : set β) :
   e.source ∩ (e ⁻¹' (e.target ∩ s)) = e.source ∩ (e ⁻¹' s) :=
-begin
-  refine ext_iff.mpr (λ x, ⟨λ hx, _, λ hx, _⟩),
-  simp only [mem_inter_eq, mem_preimage] at *;
-  exact ⟨hx.1, hx.2.2⟩,
-  exact ⟨hx.1, e.to_local_equiv.map_source hx.1, hx.2⟩, --exacts?
-end
+e.to_local_equiv.source_inter_preimage_target_inter s
 
 /-- Two local homeomorphisms are equal when they have equal `to_fun`, `inv_fun` and `source`.
 It is not sufficient to have equal `to_fun` and `source`, as this only determines `inv_fun` on

src/topology/order.lean

@@ -424,7 +424,7 @@ le_antisymm
   (coinduced_le_iff_le_induced.1 $ le_generate_from $ assume s hs,
     generate_open.basic _ $ mem_image_of_mem _ hs)
 
-lemma le_induced_generate {α β} [t : topological_space α] {b : set (set β)}
+lemma le_induced_generate_from {α β} [t : topological_space α] {b : set (set β)}
   {f : α → β} (h : ∀ (a : set β), a ∈ b → is_open (f ⁻¹' a)) : t ≤ induced f (generate_from b) :=
 begin
   rw induced_generate_from_eq,

src/topology/topological_fiber_bundle.lean

@@ -912,8 +912,10 @@ lemma local_triv'_trans (i j : ι) :
   (Z.local_triv' i).symm.trans (Z.local_triv' j) ≈ (Z.triv_change i j).to_local_equiv :=
 begin
   split,
-  { ext x, erw [mem_prod], simp only [mem_local_triv'_source, mem_local_triv'_target,
-    local_triv'_symm_apply] with mfld_simps},
+  { ext x,
+    erw [mem_prod],
+    simp only [mem_local_triv'_source, mem_local_triv'_target, local_triv'_symm_apply]
+      with mfld_simps, },
   { rintros ⟨x, v⟩ hx,
     simp only [triv_change, local_triv', local_equiv.symm, true_and, prod_mk_mem_set_prod_eq,
       local_equiv.trans_source, mem_inter_eq, and_true, mem_univ, prod.mk.inj_iff, mem_preimage,
@@ -1102,7 +1104,7 @@ lemma continuous_sigma_mk (b : B) : @continuous _ _ _ (Z.to_topological_space ι
   (λ a, (⟨b, a⟩ : (bundle.total_space Z.fiber))) :=
 begin
   rw [continuous_iff_le_induced, topological_fiber_bundle_core.to_topological_space],
-  apply le_induced_generate,
+  apply le_induced_generate_from,
   simp only [mem_Union, mem_singleton_iff, local_triv'_source, local_triv'_coe, mem_image],
   rintros s ⟨i, t, ht, rfl⟩,
   rw [←(local_homeomorph.source_inter_preimage_target_inter (Z.local_triv i) t),