. suffices h : ∀ b c, Basis.as_filter b = Basis.as_filter c → b ≤' c
  . intros heq
    exact ⟨h _ _ heq, h _ _ heq.symm⟩
  intros b c hbc s hs
  have hs' := Basis.mem_as_filter_of_mem hs
  rw [← hbc] at hs'
  exact hs'
case mpr
α : Type u_1
b c : Basis α
⊢ as_filter b = as_filter c → b ≤' c ∧ c ≤' b
no goals