Theorem: Matroid.spanning_iff_superset_base' (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 : α
S T : Set α
⊢ M.Spanning S ↔ (∃ B, M.Base B ∧ B ⊆ S) ∧ S ⊆ M.E
Tactic:
refine' ⟨fun h ↦ ⟨_, h.subset_ground⟩, fun ⟨⟨B, hB, hBS⟩, hSE⟩ ↦ hB.spanning.superset hBS⟩
State after:
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e f x y : α
S T : Set α
h : M.Spanning S
⊢ ∃ B, M.Base B ∧ B ⊆ S

State before:
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e f x y : α
S T : Set α
h : M.Spanning S
⊢ ∃ B, M.Base B ∧ B ⊆ S
Tactic:
obtain ⟨B, hB⟩ := M.exists_basis S
State after:
case intro
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B✝ C R : Set α
e f x y : α
S T : Set α
h : M.Spanning S
B : Set α
hB : M.Basis B S
⊢ ∃ B, M.Base B ∧ B ⊆ S

State before:
case intro
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B✝ C R : Set α
e f x y : α
S T : Set α
h : M.Spanning S
B : Set α
hB : M.Basis B S
⊢ ∃ B, M.Base B ∧ B ⊆ S
Tactic:
have hB' := hB.basis_cl_right
State after:
case intro
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B✝ C R : Set α
e f x y : α
S T : Set α
h : M.Spanning S
B : Set α
hB : M.Basis B S
hB' : M.Basis B (M.cl S)
⊢ ∃ B, M.Base B ∧ B ⊆ S

State before:
case intro
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B✝ C R : Set α
e f x y : α
S T : Set α
h : M.Spanning S
B : Set α
hB : M.Basis B S
hB' : M.Basis B (M.cl S)
⊢ ∃ B, M.Base B ∧ B ⊆ S
Tactic:
rw [h.cl_eq, basis_ground_iff] at hB'
State after:
case intro
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B✝ C R : Set α
e f x y : α
S T : Set α
h : M.Spanning S
B : Set α
hB : M.Basis B S
hB' : M.Base B
⊢ ∃ B, M.Base B ∧ B ⊆ S

State before:
case intro
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B✝ C R : Set α
e f x y : α
S T : Set α
h : M.Spanning S
B : Set α
hB : M.Basis B S
hB' : M.Base B
⊢ ∃ B, M.Base B ∧ B ⊆ S
Tactic:
exact ⟨B, hB', hB.subset⟩
State after:
no goals