Theorem: Matroid.Paving.spanning_of_dep (Matroid/Paving.lean)

State before:
α : Type u_1
N M : Matroid α
C D : Set α
hM : M.Paving
hD : M.Dep D
⊢ M.Spanning D
Tactic:
obtain ⟨C, hCD, hC⟩ := hD.exists_circuit_subset
State after:
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

State before:
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
Tactic:
exact (hM.spanning_of_circuit hC).superset hCD
State after:
no goals