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

State before:
α : Type u_1
M✝ : Matroid α
B B' I I' J K X✝ Y : Set α
M : Matroid α
X : Set α
⊢ M.conn ∅ X = 0
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 I : Set α
hI : M.Basis' I X
⊢ M.conn ∅ X = 0

State before:
case intro
α : Type u_1
M✝ : Matroid α
B B' I✝ I' J K X✝ Y : Set α
M : Matroid α
X I : Set α
hI : M.Basis' I X
⊢ M.conn ∅ X = 0
Tactic:
rw [(M.empty_indep.basis_self.basis').conn_eq hI, empty_inter, encard_empty,
  erk_dual_restrict_eq_zero_iff.2 (by simpa using hI.indep), zero_add]
State after:
no goals

State before:
α : Type u_1
M✝ : Matroid α
B B' I✝ I' J K X✝ Y : Set α
M : Matroid α
X I : Set α
hI : M.Basis' I X
⊢ M.Indep (∅ ∪ I)
Tactic:
simpa using hI.indep
State after:
no goals