rw [relax, relaxSet_indep_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).Indep I ↔ M.Indep I ∨ I = 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