chore(order/filter/bases): a few more constructors (#6798)

src/order/filter/bases.lean

@@ -268,23 +268,23 @@ by erw [(filter_basis.of_sets s).generate, ← (has_basis_generate s).filter_eq]
 lemma of_sets_filter_eq_generate (s : set (set α)) : (filter_basis.of_sets s).filter = generate s :=
 by rw [← (filter_basis.of_sets s).generate, generate_eq_generate_inter s] ; refl
 
-lemma has_basis.to_has_basis (hl : l.has_basis p s) (h : ∀ i, p i → ∃ i', p' i' ∧ s' i' ⊆ s i)
-  (h' : ∀ i', p' i' → ∃ i, p i ∧ s i ⊆ s' i') : l.has_basis p' s' :=
+lemma has_basis.to_has_basis' (hl : l.has_basis p s) (h : ∀ i, p i → ∃ i', p' i' ∧ s' i' ⊆ s i)
+  (h' : ∀ i', p' i' → s' i' ∈ l) : l.has_basis p' s' :=
 begin
-  constructor,
-  intro t,
-  rw hl.mem_iff,
-  split,
-  { rintros ⟨i, pi, hi⟩,
-    rcases h i pi with ⟨i', pi', hi'⟩,
-    use [i', pi'],
-    tauto },
-  { rintros ⟨i', pi', hi'⟩,
-    rcases h' i' pi' with ⟨i, pi, hi⟩,
-    use [i, pi],
-    tauto },
+  refine ⟨λ t, ⟨λ ht, _, λ ⟨i', hi', ht⟩, mem_sets_of_superset (h' i' hi') ht⟩⟩,
+  rcases hl.mem_iff.1 ht with ⟨i, hi, ht⟩,
+  rcases h i hi with ⟨i', hi', hs's⟩,
+  exact ⟨i', hi', subset.trans hs's ht⟩
 end
 
+lemma has_basis.to_has_basis (hl : l.has_basis p s) (h : ∀ i, p i → ∃ i', p' i' ∧ s' i' ⊆ s i)
+  (h' : ∀ i', p' i' → ∃ i, p i ∧ s i ⊆ s' i') : l.has_basis p' s' :=
+hl.to_has_basis' h $ λ i' hi', let ⟨i, hi, hss'⟩ := h' i' hi' in hl.mem_iff.2 ⟨i, hi, hss'⟩
+
+lemma has_basis.to_subset (hl : l.has_basis p s) {t : ι → set α} (h : ∀ i, p i → t i ⊆ s i)
+  (ht : ∀ i, p i → t i ∈ l) : l.has_basis p t :=
+hl.to_has_basis' (λ i hi, ⟨i, hi, h i hi⟩) ht
+
 lemma has_basis.eventually_iff (hl : l.has_basis p s) {q : α → Prop} :
   (∀ᶠ x in l, q x) ↔ ∃ i, p i ∧ ∀ ⦃x⦄, x ∈ s i → q x :=
 by simpa using hl.mem_iff