refine eq_of_indep_iff_indep_forall (by simpa) fun I hI ↦ ?_
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
he : e ∉ M.E
⊢ M.extendBy e U ＼ e = M
α : Type u_1
M : Matroid α
I✝ J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
he : e ∉ M.E
I : Set α
hI : I ⊆ (M.extendBy e U ＼ e).E
⊢ (M.extendBy e U ＼ e).Indep I ↔ M.Indep I