Theorem: Matroid.conn_cl_left (Matroid/Connectivity.lean)

State before:
α : Type u_1
M✝ : Matroid α
B B' I I' J K X✝ Y✝ : Set α
M : Matroid α
X Y : Set α
⊢ M.conn X Y = M.conn (M.cl X) Y
Tactic:
obtain ⟨I, hI⟩ := M.exists_basis' X
State after:
case intro
α : Type u_1
M✝ : Matroid α
B B' I✝ I' J K X✝ Y✝ : Set α
M : Matroid α
X Y I : Set α
hI : M.Basis' I X
⊢ M.conn X Y = M.conn (M.cl X) Y

State before:
case intro
α : Type u_1
M✝ : Matroid α
B B' I✝ I' J K X✝ Y✝ : Set α
M : Matroid α
X Y I : Set α
hI : M.Basis' I X
⊢ M.conn X Y = M.conn (M.cl X) Y
Tactic:
obtain ⟨J, hJ⟩ := M.exists_basis' Y
State after:
case intro.intro
α : Type u_1
M✝ : Matroid α
B B' I✝ I' J✝ K X✝ Y✝ : Set α
M : Matroid α
X Y I : Set α
hI : M.Basis' I X
J : Set α
hJ : M.Basis' J Y
⊢ M.conn X Y = M.conn (M.cl X) Y

State before:
case intro.intro
α : Type u_1
M✝ : Matroid α
B B' I✝ I' J✝ K X✝ Y✝ : Set α
M : Matroid α
X Y I : Set α
hI : M.Basis' I X
J : Set α
hJ : M.Basis' J Y
⊢ M.conn X Y = M.conn (M.cl X) Y
Tactic:
rw [hI.conn_eq hJ, hI.basis_cl_right.basis'.conn_eq hJ]
State after:
no goals