simp_rw [indep_iff, relaxSet_base_iff h]
α : 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).Indep I ↔ M.Indep I ∨ I ∈ 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
⊢ (∃ B, (M.Base B ∨ B ∈ Hs) ∧ I ⊆ B) ↔ (∃ B, M.Base B ∧ I ⊆ B) ∨ I ∈ Hs