Theorem: Matroid.base_iff_indep_cl_eq (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.Base B ↔ M.Indep B ∧ M.cl B = M.E
Tactic:
rw [← basis_ground_iff, basis_iff_indep_subset_cl, and_congr_right_iff]
State after:
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e f x y : α
⊢ M.Indep B → (B ⊆ M.E ∧ M.E ⊆ M.cl B ↔ M.cl B = M.E)

State before:
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e f x y : α
⊢ M.Indep B → (B ⊆ M.E ∧ M.E ⊆ M.cl B ↔ M.cl B = M.E)
Tactic:
exact fun hI ↦ ⟨fun h ↦ (M.cl_subset_ground _).antisymm h.2,
  fun h ↦ ⟨(M.subset_cl B).trans_eq h, h.symm.subset⟩⟩
State after:
no goals