Theorem: Matroid.basis'_iff_basis_cl (Matroid/Closure.lean)

State before:
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e f x y : α
⊢ M.Basis' I X ↔ M.Basis I (M.cl X) ∧ I ⊆ X
Tactic:
rw [← cl_inter_ground, basis'_iff_basis_inter_ground]
State after:
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e f x y : α
⊢ M.Basis I (X ∩ M.E) ↔ M.Basis I (M.cl (X ∩ M.E)) ∧ I ⊆ X

State before:
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e f x y : α
⊢ M.Basis I (X ∩ M.E) ↔ M.Basis I (M.cl (X ∩ M.E)) ∧ I ⊆ X
Tactic:
exact ⟨fun h ↦ ⟨h.basis_cl_right, h.subset.trans inter_subset_left⟩,
  fun h ↦ h.1.basis_subset (subset_inter h.2 h.1.indep.subset_ground) (M.subset_cl _)⟩
State after:
no goals