Theorem: Matroid.Flat.spanning_iff (Matroid/Flat.lean)

State before:
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
hF : M.Flat F
⊢ F = M.E → M.Spanning F
Tactic:
rintro rfl
State after:
α : Type u_1
M : Matroid α
I X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
hF : M.Flat M.E
⊢ M.Spanning M.E

State before:
α : Type u_1
M : Matroid α
I X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
hF : M.Flat M.E
⊢ M.Spanning M.E
Tactic:
exact M.ground_spanning
State after:
no goals