rw [relax, relaxSet_base_iff, mem_singleton_iff]
α : Type u_1
M : Matroid α
E I H B X : Set α
e f : α
hH : M.Hyperplane X
hC : M.Circuit X
⊢ (M.relax X).Base B ↔ M.Base B ∨ B = X
α : Type u_1
M : Matroid α
E I H B X : Set α
e f : α
hH : M.Hyperplane X
hC : M.Circuit X
⊢ ∀ H ∈ {X}, M.Circuit H ∧ M.Hyperplane H