Theorem: Matroid.SparsePaving.dual (Matroid/Paving.lean)

State before:
α : Type u_1
N M : Matroid α
C D : Set α
h : M.SparsePaving
⊢ M✶.SparsePaving
Tactic:
rw [SparsePaving, dual_dual]
State after:
α : Type u_1
N M : Matroid α
C D : Set α
h : M.SparsePaving
⊢ M✶.Paving ∧ M.Paving

State before:
α : Type u_1
N M : Matroid α
C D : Set α
h : M.SparsePaving
⊢ M✶.Paving ∧ M.Paving
Tactic:
exact And.symm h
State after:
no goals