simp only [relaxSet, Matroid.ofBase]
α : Type u_1
M : Matroid α
E I H B X : Set α
e f : α
Hs : Set (Set α)
h : ∀ H ∈ Hs, M.Circuit H ∧ M.Hyperplane H
⊢ (M.relaxSet Hs).Base B ↔ M.Base B ∨ B ∈ Hs
α : Type u_1
M : Matroid α
E I H B X : Set α
e f : α
Hs : Set (Set α)
h : ∀ H ∈ Hs, M.Circuit H ∧ M.Hyperplane H
⊢ M.Base B ∨ B ∈ Hs ∧ M.Circuit B ∧ M.Hyperplane B ↔ M.Base B ∨ B ∈ Hs