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

State before:
α : Type u_1
M✝ : Matroid α
B B' I I' J K X Y : Set α
M : Matroid α
hX : autoParam (X ⊆ M.E) _auto✝
hY : autoParam (Y ⊆ M.E) _auto✝
⊢ M.conn X Y = 0 ↔ M.Skew 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 α
hX : autoParam (X ⊆ M.E) _auto✝
hY : autoParam (Y ⊆ M.E) _auto✝
I : Set α
hI : M.Basis I X
⊢ M.conn X Y = 0 ↔ M.Skew X Y

State before:
case intro
α : Type u_1
M✝ : Matroid α
B B' I✝ I' J K X Y : Set α
M : Matroid α
hX : autoParam (X ⊆ M.E) _auto✝
hY : autoParam (Y ⊆ M.E) _auto✝
I : Set α
hI : M.Basis I X
⊢ M.conn X Y = 0 ↔ M.Skew 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 α
hX : autoParam (X ⊆ M.E) _auto✝
hY : autoParam (Y ⊆ M.E) _auto✝
I : Set α
hI : M.Basis I X
J : Set α
hJ : M.Basis J Y
⊢ M.conn X Y = 0 ↔ M.Skew X Y

State before:
case intro.intro
α : Type u_1
M✝ : Matroid α
B B' I✝ I' J✝ K X Y : Set α
M : Matroid α
hX : autoParam (X ⊆ M.E) _auto✝
hY : autoParam (Y ⊆ M.E) _auto✝
I : Set α
hI : M.Basis I X
J : Set α
hJ : M.Basis J Y
⊢ M.conn X Y = 0 ↔ M.Skew X Y
Tactic:
rw [skew_iff_cl_skew, conn_cl_cl, ← hI.cl_eq_cl, ← hJ.cl_eq_cl, ← skew_iff_cl_skew,
  ← conn_cl_cl, hI.indep.conn_eq hJ.indep, add_eq_zero_iff, encard_eq_zero,
  ← disjoint_iff_inter_eq_empty, erk_dual_restrict_eq_zero_iff,
  hI.indep.skew_iff_disjoint_union_indep hJ.indep]
State after:
no goals