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
hFI : F ⊆ I
hF : M.Basis' (I \ F ∪ J) (X ∪ Y)
⊢ M.conn X Y = F.encard
Tactic:
apply conn_eq_encard_of_diff hXY hI hJ (hFI.trans subset_union_left)
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
hFI : F ⊆ I
hF : M.Basis' (I \ F ∪ J) (X ∪ Y)
⊢ M.Basis' ((I ∪ J) \ F) (X ∪ Y)

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
hFI : F ⊆ I
hF : M.Basis' (I \ F ∪ J) (X ∪ Y)
⊢ M.Basis' ((I ∪ J) \ F) (X ∪ Y)
Tactic:
rwa [union_diff_distrib, (sdiff_eq_left (x := J)).2 ]
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
hFI : F ⊆ I
hF : M.Basis' (I \ F ∪ J) (X ∪ Y)
⊢ Disjoint J F

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
hFI : F ⊆ I
hF : M.Basis' (I \ F ∪ J) (X ∪ Y)
⊢ Disjoint J F
Tactic:
exact (hXY.symm.mono hJ.subset (hFI.trans hI.subset))
State after:
no goals