Theorem: Matroid.Basis'.encard_dual_switch_switch_eq (Matroid/Connectivity.lean)

State before:
α : Type u_1
M : Matroid α
B B' I✝ I'✝ J✝ K X✝ Y✝ I I' J J' X Y : Set α
hI : M.Basis' I X
hI' : M.Basis' I' X
hJ : M.Basis' J Y
hJ' : M.Basis' J' Y
⊢ (I ∩ J).encard + (M ↾ (I ∪ J))✶.erk = (I' ∩ J').encard + (M ↾ (I' ∪ J'))✶.erk
Tactic:
rw [hI.indep.encard_inter_add_erk_dual_eq_of_cl_eq_cl hI'.indep
    (by rw [hI.cl_eq_cl, hI'.cl_eq_cl]) hJ.indep,
  inter_comm, union_comm, hJ.indep.encard_inter_add_erk_dual_eq_of_cl_eq_cl hJ'.indep
    (by rw [hJ.cl_eq_cl, hJ'.cl_eq_cl]) hI'.indep, inter_comm, union_comm]
State after:
no goals

State before:
α : Type u_1
M : Matroid α
B B' I✝ I'✝ J✝ K X✝ Y✝ I I' J J' X Y : Set α
hI : M.Basis' I X
hI' : M.Basis' I' X
hJ : M.Basis' J Y
hJ' : M.Basis' J' Y
⊢ M.cl I = M.cl I'
Tactic:
rw [hI.cl_eq_cl, hI'.cl_eq_cl]
State after:
no goals

State before:
α : Type u_1
M : Matroid α
B B' I✝ I'✝ J✝ K X✝ Y✝ I I' J J' X Y : Set α
hI : M.Basis' I X
hI' : M.Basis' I' X
hJ : M.Basis' J Y
hJ' : M.Basis' J' Y
⊢ M.cl J = M.cl J'
Tactic:
rw [hJ.cl_eq_cl, hJ'.cl_eq_cl]
State after:
no goals