obtain ⟨C, hCD, hC⟩ := hD.exists_circuit_subset
α : Type u_1
N M : Matroid α
C D : Set α
hM : M.Paving
hD : M.Dep D
⊢ M.Spanning D
case intro.intro
α : Type u_1
N M : Matroid α
C✝ D : Set α
hM : M.Paving
hD : M.Dep D
C : Set α
hCD : C ⊆ D
hC : M.Circuit C
⊢ M.Spanning D