. intro h; rw [h]
case mp
α : Type u_1
b c : Basis α
⊢ b = c → b.sets = c.sets

case mpr
α : Type u_1
b c : Basis α
⊢ b.sets = c.sets → b = c
case mpr
α : Type u_1
b c : Basis α
⊢ b.sets = c.sets → b = c