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

State before:
α : Type u_1
M : Matroid α
B B' I I' J K X Y F : Set α
hXY : Disjoint X Y
hI : M.Basis' I X
hJ : M.Basis' J Y
hFIJ : F ⊆ I ∪ J
hF : M.Basis' ((I ∪ J) \ F) (X ∪ Y)
⊢ M.conn X Y = F.encard
Tactic:
have hF' : M.Basis ((I ∪ J) \ F) (I ∪ J) := by
  refine hF.basis_inter_ground.basis_subset diff_subset
    (subset_inter (union_subset_union hI.subset hJ.subset)
    (union_subset hI.indep.subset_ground hJ.indep.subset_ground))
State after:
α : Type u_1
M : Matroid α
B B' I I' J K X Y F : Set α
hXY : Disjoint X Y
hI : M.Basis' I X
hJ : M.Basis' J Y
hFIJ : F ⊆ I ∪ J
hF : M.Basis' ((I ∪ J) \ F) (X ∪ Y)
hF' : M.Basis ((I ∪ J) \ F) (I ∪ J)
⊢ M.conn X Y = F.encard

State before:
α : Type u_1
M : Matroid α
B B' I I' J K X Y F : Set α
hXY : Disjoint X Y
hI : M.Basis' I X
hJ : M.Basis' J Y
hFIJ : F ⊆ I ∪ J
hF : M.Basis' ((I ∪ J) \ F) (X ∪ Y)
hF' : M.Basis ((I ∪ J) \ F) (I ∪ J)
⊢ M.conn X Y = F.encard
Tactic:
rw [hI.conn_eq hJ, hF'.erk_dual_restrict, diff_diff_cancel_left hFIJ,
  (hXY.mono hI.subset hJ.subset).inter_eq, encard_empty, zero_add]
State after:
no goals

State before:
α : Type u_1
M : Matroid α
B B' I I' J K X Y F : Set α
hXY : Disjoint X Y
hI : M.Basis' I X
hJ : M.Basis' J Y
hFIJ : F ⊆ I ∪ J
hF : M.Basis' ((I ∪ J) \ F) (X ∪ Y)
⊢ M.Basis ((I ∪ J) \ F) (I ∪ J)
Tactic:
refine hF.basis_inter_ground.basis_subset diff_subset
  (subset_inter (union_subset_union hI.subset hJ.subset)
  (union_subset hI.indep.subset_ground hJ.indep.subset_ground))
State after:
no goals