Theorem: Matroid.modular_of_modular_restrict (Matroid/Old/ModularCut.lean)

State before:
α : Type u_1
M : Matroid α
X : Set (Set α)
hX : ⋃₀ X ⊆ M.E
R : Set α
hR : ∃ B, sorryAx Prop true
⊢ ∃ B, sorryAx Prop true
Tactic:
obtain ⟨B, ⟨B_base, B_mod⟩⟩ := hR
State after:
no goals