apply le_antisymm
case mp
α : Type u_1
b c : Basis α
h : b ≤' c ∧ c ≤' b
⊢ as_filter b = as_filter c
case mp.a
α : Type u_1
b c : Basis α
h : b ≤' c ∧ c ≤' b
⊢ as_filter b ≤ as_filter c

case mp.a
α : Type u_1
b c : Basis α
h : b ≤' c ∧ c ≤' b
⊢ as_filter c ≤ as_filter b