Theorem: Matroid.conn_compl_dual (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 (M.E \ X) = M✶.conn X (M.E \ X)
Tactic:
suffices ∀ X ⊆ M.E, M.conn X (M.E \ X) = M✶.conn X (M.E \ X) by
  rw [conn_eq_conn_inter_ground_left, M✶.conn_eq_conn_inter_ground_left,
    show M.E \ X = M.E \ (X ∩ M.E) by simp, this _ inter_subset_right, dual_ground]
State after:
α : Type u_1
M✝ : Matroid α
B B' I I' J K X✝ Y : Set α
M : Matroid α
X : Set α
⊢ ∀ X ⊆ M.E, M.conn X (M.E \ X) = M✶.conn X (M.E \ X)

State before:
α : Type u_1
M✝ : Matroid α
B B' I I' J K X✝ Y : Set α
M : Matroid α
X : Set α
⊢ ∀ X ⊆ M.E, M.conn X (M.E \ X) = M✶.conn X (M.E \ X)
Tactic:
intro X hX
State after:
α : Type u_1
M✝ : Matroid α
B B' I I' J K X✝¹ Y : Set α
M : Matroid α
X✝ X : Set α
hX : X ⊆ M.E
⊢ M.conn X (M.E \ X) = M✶.conn X (M.E \ X)

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

State before:
case intro
α : Type u_1
M✝ : Matroid α
B B' I✝ I' J K X✝¹ Y : Set α
M : Matroid α
X✝ X : Set α
hX : X ⊆ M.E
I : Set α
hI : M.Basis I X
⊢ M.conn X (M.E \ X) = M✶.conn X (M.E \ X)
Tactic:
obtain ⟨J, hJ⟩ := M.exists_basis (M.E \ X)
State after:
case intro.intro
α : Type u_1
M✝ : Matroid α
B B' I✝ I' J✝ K X✝¹ Y : Set α
M : Matroid α
X✝ X : Set α
hX : X ⊆ M.E
I : Set α
hI : M.Basis I X
J : Set α
hJ : M.Basis J (M.E \ X)
⊢ M.conn X (M.E \ X) = M✶.conn X (M.E \ X)

State before:
case intro.intro
α : Type u_1
M✝ : Matroid α
B B' I✝ I' J✝ K X✝¹ Y : Set α
M : Matroid α
X✝ X : Set α
hX : X ⊆ M.E
I : Set α
hI : M.Basis I X
J : Set α
hJ : M.Basis J (M.E \ X)
⊢ M.conn X (M.E \ X) = M✶.conn X (M.E \ X)
Tactic:
obtain ⟨BX, hBX, hIBX⟩ := hI.indep.subset_basis_of_subset
  (subset_union_left (s := I) (t := J))
State after:
case intro.intro.intro.intro
α : Type u_1
M✝ : Matroid α
B B' I✝ I' J✝ K X✝¹ Y : Set α
M : Matroid α
X✝ X : Set α
hX : X ⊆ M.E
I : Set α
hI : M.Basis I X
J : Set α
hJ : M.Basis J (M.E \ X)
BX : Set α
hBX : M.Basis BX (I ∪ J)
hIBX : I ⊆ BX
⊢ M.conn X (M.E \ X) = M✶.conn X (M.E \ X)

State before:
case intro.intro.intro.intro
α : Type u_1
M✝ : Matroid α
B B' I✝ I' J✝ K X✝¹ Y : Set α
M : Matroid α
X✝ X : Set α
hX : X ⊆ M.E
I : Set α
hI : M.Basis I X
J : Set α
hJ : M.Basis J (M.E \ X)
BX : Set α
hBX : M.Basis BX (I ∪ J)
hIBX : I ⊆ BX
⊢ M.conn X (M.E \ X) = M✶.conn X (M.E \ X)
Tactic:
have hIJE : M.Spanning (I ∪ J) := by
  rw [spanning_iff_cl, ← cl_cl_union_cl_eq_cl_union, hI.cl_eq_cl, hJ.cl_eq_cl,
    cl_cl_union_cl_eq_cl_union, union_diff_cancel hX, cl_ground]
State after:
case intro.intro.intro.intro
α : Type u_1
M✝ : Matroid α
B B' I✝ I' J✝ K X✝¹ Y : Set α
M : Matroid α
X✝ X : Set α
hX : X ⊆ M.E
I : Set α
hI : M.Basis I X
J : Set α
hJ : M.Basis J (M.E \ X)
BX : Set α
hBX : M.Basis BX (I ∪ J)
hIBX : I ⊆ BX
hIJE : M.Spanning (I ∪ J)
⊢ M.conn X (M.E \ X) = M✶.conn X (M.E \ X)

State before:
case intro.intro.intro.intro
α : Type u_1
M✝ : Matroid α
B B' I✝ I' J✝ K X✝¹ Y : Set α
M : Matroid α
X✝ X : Set α
hX : X ⊆ M.E
I : Set α
hI : M.Basis I X
J : Set α
hJ : M.Basis J (M.E \ X)
BX : Set α
hBX : M.Basis BX (I ∪ J)
hIBX : I ⊆ BX
hIJE : M.Spanning (I ∪ J)
⊢ M.conn X (M.E \ X) = M✶.conn X (M.E \ X)
Tactic:
have hBXb : M.Base BX := by rw [← basis_ground_iff, ← hIJE.cl_eq]; exact hBX.basis_cl_right
State after:
case intro.intro.intro.intro
α : Type u_1
M✝ : Matroid α
B B' I✝ I' J✝ K X✝¹ Y : Set α
M : Matroid α
X✝ X : Set α
hX : X ⊆ M.E
I : Set α
hI : M.Basis I X
J : Set α
hJ : M.Basis J (M.E \ X)
BX : Set α
hBX : M.Basis BX (I ∪ J)
hIBX : I ⊆ BX
hIJE : M.Spanning (I ∪ J)
hBXb : M.Base BX
⊢ M.conn X (M.E \ X) = M✶.conn X (M.E \ X)

State before:
case intro.intro.intro.intro
α : Type u_1
M✝ : Matroid α
B B' I✝ I' J✝ K X✝¹ Y : Set α
M : Matroid α
X✝ X : Set α
hX : X ⊆ M.E
I : Set α
hI : M.Basis I X
J : Set α
hJ : M.Basis J (M.E \ X)
BX : Set α
hBX : M.Basis BX (I ∪ J)
hIBX : I ⊆ BX
hIJE : M.Spanning (I ∪ J)
hBXb : M.Base BX
⊢ M.conn X (M.E \ X) = M✶.conn X (M.E \ X)
Tactic:
obtain rfl : I = BX ∩ X := hI.eq_of_subset_indep (hBXb.indep.inter_right _)
  (subset_inter hIBX hI.subset) inter_subset_right
State after:
case intro.intro.intro.intro
α : Type u_1
M✝ : Matroid α
B B' I I' J✝ K X✝¹ Y : Set α
M : Matroid α
X✝ X : Set α
hX : X ⊆ M.E
J : Set α
hJ : M.Basis J (M.E \ X)
BX : Set α
hBXb : M.Base BX
hI : M.Basis (BX ∩ X) X
hBX : M.Basis BX (BX ∩ X ∪ J)
hIBX : BX ∩ X ⊆ BX
hIJE : M.Spanning (BX ∩ X ∪ J)
⊢ M.conn X (M.E \ X) = M✶.conn X (M.E \ X)

State before:
case intro.intro.intro.intro
α : Type u_1
M✝ : Matroid α
B B' I I' J✝ K X✝¹ Y : Set α
M : Matroid α
X✝ X : Set α
hX : X ⊆ M.E
J : Set α
hJ : M.Basis J (M.E \ X)
BX : Set α
hBXb : M.Base BX
hI : M.Basis (BX ∩ X) X
hBX : M.Basis BX (BX ∩ X ∪ J)
hIBX : BX ∩ X ⊆ BX
hIJE : M.Spanning (BX ∩ X ∪ J)
⊢ M.conn X (M.E \ X) = M✶.conn X (M.E \ X)
Tactic:
have hBXdual := hBXb.compl_inter_basis_of_inter_basis hI
State after:
case intro.intro.intro.intro
α : Type u_1
M✝ : Matroid α
B B' I I' J✝ K X✝¹ Y : Set α
M : Matroid α
X✝ X : Set α
hX : X ⊆ M.E
J : Set α
hJ : M.Basis J (M.E \ X)
BX : Set α
hBXb : M.Base BX
hI : M.Basis (BX ∩ X) X
hBX : M.Basis BX (BX ∩ X ∪ J)
hIBX : BX ∩ X ⊆ BX
hIJE : M.Spanning (BX ∩ X ∪ J)
hBXdual : M✶.Basis (M.E \ BX ∩ (M.E \ X)) (M.E \ X)
⊢ M.conn X (M.E \ X) = M✶.conn X (M.E \ X)

State before:
case intro.intro.intro.intro
α : Type u_1
M✝ : Matroid α
B B' I I' J✝ K X✝¹ Y : Set α
M : Matroid α
X✝ X : Set α
hX : X ⊆ M.E
J : Set α
hJ : M.Basis J (M.E \ X)
BX : Set α
hBXb : M.Base BX
hI : M.Basis (BX ∩ X) X
hBX : M.Basis BX (BX ∩ X ∪ J)
hIBX : BX ∩ X ⊆ BX
hIJE : M.Spanning (BX ∩ X ∪ J)
hBXdual : M✶.Basis (M.E \ BX ∩ (M.E \ X)) (M.E \ X)
⊢ M.conn X (M.E \ X) = M✶.conn X (M.E \ X)
Tactic:
rw [diff_inter_diff, union_comm, ← diff_diff] at hBXdual
State after:
case intro.intro.intro.intro
α : Type u_1
M✝ : Matroid α
B B' I I' J✝ K X✝¹ Y : Set α
M : Matroid α
X✝ X : Set α
hX : X ⊆ M.E
J : Set α
hJ : M.Basis J (M.E \ X)
BX : Set α
hBXb : M.Base BX
hI : M.Basis (BX ∩ X) X
hBX : M.Basis BX (BX ∩ X ∪ J)
hIBX : BX ∩ X ⊆ BX
hIJE : M.Spanning (BX ∩ X ∪ J)
hBXdual : M✶.Basis ((M.E \ X) \ BX) (M.E \ X)
⊢ M.conn X (M.E \ X) = M✶.conn X (M.E \ X)

State before:
case intro.intro.intro.intro
α : Type u_1
M✝ : Matroid α
B B' I I' J✝ K X✝¹ Y : Set α
M : Matroid α
X✝ X : Set α
hX : X ⊆ M.E
J : Set α
hJ : M.Basis J (M.E \ X)
BX : Set α
hBXb : M.Base BX
hI : M.Basis (BX ∩ X) X
hBX : M.Basis BX (BX ∩ X ∪ J)
hIBX : BX ∩ X ⊆ BX
hIJE : M.Spanning (BX ∩ X ∪ J)
hBXdual : M✶.Basis ((M.E \ X) \ BX) (M.E \ X)
⊢ M.conn X (M.E \ X) = M✶.conn X (M.E \ X)
Tactic:
obtain ⟨BY, hBY, hJBY⟩ := hJ.indep.subset_basis_of_subset (subset_union_right (s := BX ∩ X))
State after:
case intro.intro.intro.intro.intro.intro
α : Type u_1
M✝ : Matroid α
B B' I I' J✝ K X✝¹ Y : Set α
M : Matroid α
X✝ X : Set α
hX : X ⊆ M.E
J : Set α
hJ : M.Basis J (M.E \ X)
BX : Set α
hBXb : M.Base BX
hI : M.Basis (BX ∩ X) X
hBX : M.Basis BX (BX ∩ X ∪ J)
hIBX : BX ∩ X ⊆ BX
hIJE : M.Spanning (BX ∩ X ∪ J)
hBXdual : M✶.Basis ((M.E \ X) \ BX) (M.E \ X)
BY : Set α
hBY : M.Basis BY (BX ∩ X ∪ J)
hJBY : J ⊆ BY
⊢ M.conn X (M.E \ X) = M✶.conn X (M.E \ X)

State before:
case intro.intro.intro.intro.intro.intro
α : Type u_1
M✝ : Matroid α
B B' I I' J✝ K X✝¹ Y : Set α
M : Matroid α
X✝ X : Set α
hX : X ⊆ M.E
J : Set α
hJ : M.Basis J (M.E \ X)
BX : Set α
hBXb : M.Base BX
hI : M.Basis (BX ∩ X) X
hBX : M.Basis BX (BX ∩ X ∪ J)
hIBX : BX ∩ X ⊆ BX
hIJE : M.Spanning (BX ∩ X ∪ J)
hBXdual : M✶.Basis ((M.E \ X) \ BX) (M.E \ X)
BY : Set α
hBY : M.Basis BY (BX ∩ X ∪ J)
hJBY : J ⊆ BY
⊢ M.conn X (M.E \ X) = M✶.conn X (M.E \ X)
Tactic:
have hBYb : M.Base BY := by rw [← basis_ground_iff, ← hIJE.cl_eq]; exact hBY.basis_cl_right
State after:
case intro.intro.intro.intro.intro.intro
α : Type u_1
M✝ : Matroid α
B B' I I' J✝ K X✝¹ Y : Set α
M : Matroid α
X✝ X : Set α
hX : X ⊆ M.E
J : Set α
hJ : M.Basis J (M.E \ X)
BX : Set α
hBXb : M.Base BX
hI : M.Basis (BX ∩ X) X
hBX : M.Basis BX (BX ∩ X ∪ J)
hIBX : BX ∩ X ⊆ BX
hIJE : M.Spanning (BX ∩ X ∪ J)
hBXdual : M✶.Basis ((M.E \ X) \ BX) (M.E \ X)
BY : Set α
hBY : M.Basis BY (BX ∩ X ∪ J)
hJBY : J ⊆ BY
hBYb : M.Base BY
⊢ M.conn X (M.E \ X) = M✶.conn X (M.E \ X)

State before:
case intro.intro.intro.intro.intro.intro
α : Type u_1
M✝ : Matroid α
B B' I I' J✝ K X✝¹ Y : Set α
M : Matroid α
X✝ X : Set α
hX : X ⊆ M.E
J : Set α
hJ : M.Basis J (M.E \ X)
BX : Set α
hBXb : M.Base BX
hI : M.Basis (BX ∩ X) X
hBX : M.Basis BX (BX ∩ X ∪ J)
hIBX : BX ∩ X ⊆ BX
hIJE : M.Spanning (BX ∩ X ∪ J)
hBXdual : M✶.Basis ((M.E \ X) \ BX) (M.E \ X)
BY : Set α
hBY : M.Basis BY (BX ∩ X ∪ J)
hJBY : J ⊆ BY
hBYb : M.Base BY
⊢ M.conn X (M.E \ X) = M✶.conn X (M.E \ X)
Tactic:
obtain rfl : J = BY ∩ (M.E \ X) := hJ.eq_of_subset_indep (hBYb.indep.inter_right _)
  (subset_inter hJBY hJ.subset) inter_subset_right
State after:
case intro.intro.intro.intro.intro.intro
α : Type u_1
M✝ : Matroid α
B B' I I' J K X✝¹ Y : Set α
M : Matroid α
X✝ X : Set α
hX : X ⊆ M.E
BX : Set α
hBXb : M.Base BX
hI : M.Basis (BX ∩ X) X
hIBX : BX ∩ X ⊆ BX
hBXdual : M✶.Basis ((M.E \ X) \ BX) (M.E \ X)
BY : Set α
hBYb : M.Base BY
hJ : M.Basis (BY ∩ (M.E \ X)) (M.E \ X)
hBX : M.Basis BX (BX ∩ X ∪ BY ∩ (M.E \ X))
hIJE : M.Spanning (BX ∩ X ∪ BY ∩ (M.E \ X))
hBY : M.Basis BY (BX ∩ X ∪ BY ∩ (M.E \ X))
hJBY : BY ∩ (M.E \ X) ⊆ BY
⊢ M.conn X (M.E \ X) = M✶.conn X (M.E \ X)

State before:
case intro.intro.intro.intro.intro.intro
α : Type u_1
M✝ : Matroid α
B B' I I' J K X✝¹ Y : Set α
M : Matroid α
X✝ X : Set α
hX : X ⊆ M.E
BX : Set α
hBXb : M.Base BX
hI : M.Basis (BX ∩ X) X
hIBX : BX ∩ X ⊆ BX
hBXdual : M✶.Basis ((M.E \ X) \ BX) (M.E \ X)
BY : Set α
hBYb : M.Base BY
hJ : M.Basis (BY ∩ (M.E \ X)) (M.E \ X)
hBX : M.Basis BX (BX ∩ X ∪ BY ∩ (M.E \ X))
hIJE : M.Spanning (BX ∩ X ∪ BY ∩ (M.E \ X))
hBY : M.Basis BY (BX ∩ X ∪ BY ∩ (M.E \ X))
hJBY : BY ∩ (M.E \ X) ⊆ BY
⊢ M.conn X (M.E \ X) = M✶.conn X (M.E \ X)
Tactic:
have hBYdual := hBYb.compl_inter_basis_of_inter_basis hJ
State after:
case intro.intro.intro.intro.intro.intro
α : Type u_1
M✝ : Matroid α
B B' I I' J K X✝¹ Y : Set α
M : Matroid α
X✝ X : Set α
hX : X ⊆ M.E
BX : Set α
hBXb : M.Base BX
hI : M.Basis (BX ∩ X) X
hIBX : BX ∩ X ⊆ BX
hBXdual : M✶.Basis ((M.E \ X) \ BX) (M.E \ X)
BY : Set α
hBYb : M.Base BY
hJ : M.Basis (BY ∩ (M.E \ X)) (M.E \ X)
hBX : M.Basis BX (BX ∩ X ∪ BY ∩ (M.E \ X))
hIJE : M.Spanning (BX ∩ X ∪ BY ∩ (M.E \ X))
hBY : M.Basis BY (BX ∩ X ∪ BY ∩ (M.E \ X))
hJBY : BY ∩ (M.E \ X) ⊆ BY
hBYdual : M✶.Basis (M.E \ BY ∩ (M.E \ (M.E \ X))) (M.E \ (M.E \ X))
⊢ M.conn X (M.E \ X) = M✶.conn X (M.E \ X)

State before:
case intro.intro.intro.intro.intro.intro
α : Type u_1
M✝ : Matroid α
B B' I I' J K X✝¹ Y : Set α
M : Matroid α
X✝ X : Set α
hX : X ⊆ M.E
BX : Set α
hBXb : M.Base BX
hI : M.Basis (BX ∩ X) X
hIBX : BX ∩ X ⊆ BX
hBXdual : M✶.Basis ((M.E \ X) \ BX) (M.E \ X)
BY : Set α
hBYb : M.Base BY
hJ : M.Basis (BY ∩ (M.E \ X)) (M.E \ X)
hBX : M.Basis BX (BX ∩ X ∪ BY ∩ (M.E \ X))
hIJE : M.Spanning (BX ∩ X ∪ BY ∩ (M.E \ X))
hBY : M.Basis BY (BX ∩ X ∪ BY ∩ (M.E \ X))
hJBY : BY ∩ (M.E \ X) ⊆ BY
hBYdual : M✶.Basis (M.E \ BY ∩ (M.E \ (M.E \ X))) (M.E \ (M.E \ X))
⊢ M.conn X (M.E \ X) = M✶.conn X (M.E \ X)
Tactic:
rw [diff_inter_diff, union_comm, ← diff_diff, diff_diff_cancel_left hX] at hBYdual
State after:
case intro.intro.intro.intro.intro.intro
α : Type u_1
M✝ : Matroid α
B B' I I' J K X✝¹ Y : Set α
M : Matroid α
X✝ X : Set α
hX : X ⊆ M.E
BX : Set α
hBXb : M.Base BX
hI : M.Basis (BX ∩ X) X
hIBX : BX ∩ X ⊆ BX
hBXdual : M✶.Basis ((M.E \ X) \ BX) (M.E \ X)
BY : Set α
hBYb : M.Base BY
hJ : M.Basis (BY ∩ (M.E \ X)) (M.E \ X)
hBX : M.Basis BX (BX ∩ X ∪ BY ∩ (M.E \ X))
hIJE : M.Spanning (BX ∩ X ∪ BY ∩ (M.E \ X))
hBY : M.Basis BY (BX ∩ X ∪ BY ∩ (M.E \ X))
hJBY : BY ∩ (M.E \ X) ⊆ BY
hBYdual : M✶.Basis (X \ BY) X
⊢ M.conn X (M.E \ X) = M✶.conn X (M.E \ X)

State before:
case intro.intro.intro.intro.intro.intro
α : Type u_1
M✝ : Matroid α
B B' I I' J K X✝¹ Y : Set α
M : Matroid α
X✝ X : Set α
hX : X ⊆ M.E
BX : Set α
hBXb : M.Base BX
hI : M.Basis (BX ∩ X) X
hIBX : BX ∩ X ⊆ BX
hBXdual : M✶.Basis ((M.E \ X) \ BX) (M.E \ X)
BY : Set α
hBYb : M.Base BY
hJ : M.Basis (BY ∩ (M.E \ X)) (M.E \ X)
hBX : M.Basis BX (BX ∩ X ∪ BY ∩ (M.E \ X))
hIJE : M.Spanning (BX ∩ X ∪ BY ∩ (M.E \ X))
hBY : M.Basis BY (BX ∩ X ∪ BY ∩ (M.E \ X))
hJBY : BY ∩ (M.E \ X) ⊆ BY
hBYdual : M✶.Basis (X \ BY) X
⊢ M.conn X (M.E \ X) = M✶.conn X (M.E \ X)
Tactic:
rw [hBYdual.basis'.conn_eq_of_disjoint hBXdual.basis' disjoint_sdiff_right,
  hI.basis'.conn_eq_of_disjoint hJ.basis' disjoint_sdiff_right, hBX.erk_dual_restrict,
  union_diff_distrib, diff_eq_empty.2 inter_subset_left, empty_union,
  Basis.erk_dual_restrict (hBYb.compl_base_dual.basis_ground.basis_subset _ _)]
State after:
case intro.intro.intro.intro.intro.intro
α : Type u_1
M✝ : Matroid α
B B' I I' J K X✝¹ Y : Set α
M : Matroid α
X✝ X : Set α
hX : X ⊆ M.E
BX : Set α
hBXb : M.Base BX
hI : M.Basis (BX ∩ X) X
hIBX : BX ∩ X ⊆ BX
hBXdual : M✶.Basis ((M.E \ X) \ BX) (M.E \ X)
BY : Set α
hBYb : M.Base BY
hJ : M.Basis (BY ∩ (M.E \ X)) (M.E \ X)
hBX : M.Basis BX (BX ∩ X ∪ BY ∩ (M.E \ X))
hIJE : M.Spanning (BX ∩ X ∪ BY ∩ (M.E \ X))
hBY : M.Basis BY (BX ∩ X ∪ BY ∩ (M.E \ X))
hJBY : BY ∩ (M.E \ X) ⊆ BY
hBYdual : M✶.Basis (X \ BY) X
⊢ ((BY ∩ (M.E \ X)) \ BX).encard = ((X \ BY ∪ (M.E \ X) \ BX) \ (M.E \ BY)).encard

α : Type u_1
M✝ : Matroid α
B B' I I' J K X✝¹ Y : Set α
M : Matroid α
X✝ X : Set α
hX : X ⊆ M.E
BX : Set α
hBXb : M.Base BX
hI : M.Basis (BX ∩ X) X
hIBX : BX ∩ X ⊆ BX
hBXdual : M✶.Basis ((M.E \ X) \ BX) (M.E \ X)
BY : Set α
hBYb : M.Base BY
hJ : M.Basis (BY ∩ (M.E \ X)) (M.E \ X)
hBX : M.Basis BX (BX ∩ X ∪ BY ∩ (M.E \ X))
hIJE : M.Spanning (BX ∩ X ∪ BY ∩ (M.E \ X))
hBY : M.Basis BY (BX ∩ X ∪ BY ∩ (M.E \ X))
hJBY : BY ∩ (M.E \ X) ⊆ BY
hBYdual : M✶.Basis (X \ BY) X
⊢ M.E \ BY ⊆ X \ BY ∪ (M.E \ X) \ BX

α : Type u_1
M✝ : Matroid α
B B' I I' J K X✝¹ Y : Set α
M : Matroid α
X✝ X : Set α
hX : X ⊆ M.E
BX : Set α
hBXb : M.Base BX
hI : M.Basis (BX ∩ X) X
hIBX : BX ∩ X ⊆ BX
hBXdual : M✶.Basis ((M.E \ X) \ BX) (M.E \ X)
BY : Set α
hBYb : M.Base BY
hJ : M.Basis (BY ∩ (M.E \ X)) (M.E \ X)
hBX : M.Basis BX (BX ∩ X ∪ BY ∩ (M.E \ X))
hIJE : M.Spanning (BX ∩ X ∪ BY ∩ (M.E \ X))
hBY : M.Basis BY (BX ∩ X ∪ BY ∩ (M.E \ X))
hJBY : BY ∩ (M.E \ X) ⊆ BY
hBYdual : M✶.Basis (X \ BY) X
⊢ X \ BY ∪ (M.E \ X) \ BX ⊆ M✶.E

State before:
α : Type u_1
M✝ : Matroid α
B B' I I' J K X✝¹ Y : Set α
M : Matroid α
X✝ X : Set α
hX : X ⊆ M.E
BX : Set α
hBXb : M.Base BX
hI : M.Basis (BX ∩ X) X
hIBX : BX ∩ X ⊆ BX
hBXdual : M✶.Basis ((M.E \ X) \ BX) (M.E \ X)
BY : Set α
hBYb : M.Base BY
hJ : M.Basis (BY ∩ (M.E \ X)) (M.E \ X)
hBX : M.Basis BX (BX ∩ X ∪ BY ∩ (M.E \ X))
hIJE : M.Spanning (BX ∩ X ∪ BY ∩ (M.E \ X))
hBY : M.Basis BY (BX ∩ X ∪ BY ∩ (M.E \ X))
hJBY : BY ∩ (M.E \ X) ⊆ BY
hBYdual : M✶.Basis (X \ BY) X
⊢ X \ BY ∪ (M.E \ X) \ BX ⊆ M✶.E
Tactic:
exact union_subset (diff_subset.trans hX) (diff_subset.trans diff_subset)
State after:
no goals

State before:
α : Type u_1
M✝ : Matroid α
B B' I I' J K X✝ Y : Set α
M : Matroid α
X : Set α
this : ∀ X ⊆ M.E, M.conn X (M.E \ X) = M✶.conn X (M.E \ X)
⊢ M.conn X (M.E \ X) = M✶.conn X (M.E \ X)
Tactic:
rw [conn_eq_conn_inter_ground_left, M✶.conn_eq_conn_inter_ground_left,
  show M.E \ X = M.E \ (X ∩ M.E) by simp, this _ inter_subset_right, dual_ground]
State after:
no goals

State before:
α : Type u_1
M✝ : Matroid α
B B' I I' J K X✝ Y : Set α
M : Matroid α
X : Set α
this : ∀ X ⊆ M.E, M.conn X (M.E \ X) = M✶.conn X (M.E \ X)
⊢ M.E \ X = M.E \ (X ∩ M.E)
Tactic:
simp
State after:
no goals

State before:
α : Type u_1
M✝ : Matroid α
B B' I✝ I' J✝ K X✝¹ Y : Set α
M : Matroid α
X✝ X : Set α
hX : X ⊆ M.E
I : Set α
hI : M.Basis I X
J : Set α
hJ : M.Basis J (M.E \ X)
BX : Set α
hBX : M.Basis BX (I ∪ J)
hIBX : I ⊆ BX
⊢ M.Spanning (I ∪ J)
Tactic:
rw [spanning_iff_cl, ← cl_cl_union_cl_eq_cl_union, hI.cl_eq_cl, hJ.cl_eq_cl,
  cl_cl_union_cl_eq_cl_union, union_diff_cancel hX, cl_ground]
State after:
no goals

State before:
α : Type u_1
M✝ : Matroid α
B B' I✝ I' J✝ K X✝¹ Y : Set α
M : Matroid α
X✝ X : Set α
hX : X ⊆ M.E
I : Set α
hI : M.Basis I X
J : Set α
hJ : M.Basis J (M.E \ X)
BX : Set α
hBX : M.Basis BX (I ∪ J)
hIBX : I ⊆ BX
hIJE : M.Spanning (I ∪ J)
⊢ M.Base BX
Tactic:
rw [← basis_ground_iff, ← hIJE.cl_eq]
State after:
α : Type u_1
M✝ : Matroid α
B B' I✝ I' J✝ K X✝¹ Y : Set α
M : Matroid α
X✝ X : Set α
hX : X ⊆ M.E
I : Set α
hI : M.Basis I X
J : Set α
hJ : M.Basis J (M.E \ X)
BX : Set α
hBX : M.Basis BX (I ∪ J)
hIBX : I ⊆ BX
hIJE : M.Spanning (I ∪ J)
⊢ M.Basis BX (M.cl (I ∪ J))

State before:
α : Type u_1
M✝ : Matroid α
B B' I✝ I' J✝ K X✝¹ Y : Set α
M : Matroid α
X✝ X : Set α
hX : X ⊆ M.E
I : Set α
hI : M.Basis I X
J : Set α
hJ : M.Basis J (M.E \ X)
BX : Set α
hBX : M.Basis BX (I ∪ J)
hIBX : I ⊆ BX
hIJE : M.Spanning (I ∪ J)
⊢ M.Basis BX (M.cl (I ∪ J))
Tactic:
exact hBX.basis_cl_right
State after:
no goals

State before:
α : Type u_1
M✝ : Matroid α
B B' I I' J✝ K X✝¹ Y : Set α
M : Matroid α
X✝ X : Set α
hX : X ⊆ M.E
J : Set α
hJ : M.Basis J (M.E \ X)
BX : Set α
hBXb : M.Base BX
hI : M.Basis (BX ∩ X) X
hBX : M.Basis BX (BX ∩ X ∪ J)
hIBX : BX ∩ X ⊆ BX
hIJE : M.Spanning (BX ∩ X ∪ J)
hBXdual : M✶.Basis ((M.E \ X) \ BX) (M.E \ X)
BY : Set α
hBY : M.Basis BY (BX ∩ X ∪ J)
hJBY : J ⊆ BY
⊢ M.Base BY
Tactic:
rw [← basis_ground_iff, ← hIJE.cl_eq]
State after:
α : Type u_1
M✝ : Matroid α
B B' I I' J✝ K X✝¹ Y : Set α
M : Matroid α
X✝ X : Set α
hX : X ⊆ M.E
J : Set α
hJ : M.Basis J (M.E \ X)
BX : Set α
hBXb : M.Base BX
hI : M.Basis (BX ∩ X) X
hBX : M.Basis BX (BX ∩ X ∪ J)
hIBX : BX ∩ X ⊆ BX
hIJE : M.Spanning (BX ∩ X ∪ J)
hBXdual : M✶.Basis ((M.E \ X) \ BX) (M.E \ X)
BY : Set α
hBY : M.Basis BY (BX ∩ X ∪ J)
hJBY : J ⊆ BY
⊢ M.Basis BY (M.cl (BX ∩ X ∪ J))

State before:
α : Type u_1
M✝ : Matroid α
B B' I I' J✝ K X✝¹ Y : Set α
M : Matroid α
X✝ X : Set α
hX : X ⊆ M.E
J : Set α
hJ : M.Basis J (M.E \ X)
BX : Set α
hBXb : M.Base BX
hI : M.Basis (BX ∩ X) X
hBX : M.Basis BX (BX ∩ X ∪ J)
hIBX : BX ∩ X ⊆ BX
hIJE : M.Spanning (BX ∩ X ∪ J)
hBXdual : M✶.Basis ((M.E \ X) \ BX) (M.E \ X)
BY : Set α
hBY : M.Basis BY (BX ∩ X ∪ J)
hJBY : J ⊆ BY
⊢ M.Basis BY (M.cl (BX ∩ X ∪ J))
Tactic:
exact hBY.basis_cl_right
State after:
no goals

State before:
case intro.intro.intro.intro.intro.intro
α : Type u_1
M✝ : Matroid α
B B' I I' J K X✝¹ Y : Set α
M : Matroid α
X✝ X : Set α
hX : X ⊆ M.E
BX : Set α
hBXb : M.Base BX
hI : M.Basis (BX ∩ X) X
hIBX : BX ∩ X ⊆ BX
hBXdual : M✶.Basis ((M.E \ X) \ BX) (M.E \ X)
BY : Set α
hBYb : M.Base BY
hJ : M.Basis (BY ∩ (M.E \ X)) (M.E \ X)
hBX : M.Basis BX (BX ∩ X ∪ BY ∩ (M.E \ X))
hIJE : M.Spanning (BX ∩ X ∪ BY ∩ (M.E \ X))
hBY : M.Basis BY (BX ∩ X ∪ BY ∩ (M.E \ X))
hJBY : BY ∩ (M.E \ X) ⊆ BY
hBYdual : M✶.Basis (X \ BY) X
⊢ ((BY ∩ (M.E \ X)) \ BX).encard = ((X \ BY ∪ (M.E \ X) \ BX) \ (M.E \ BY)).encard
Tactic:
rw [union_diff_distrib, diff_eq_empty.2 (diff_subset_diff_left hX), empty_union, diff_diff,
  diff_diff, ← union_assoc, union_comm, ← diff_diff, diff_diff_cancel_left hBYb.subset_ground,
  ← diff_diff, inter_diff_distrib_left, inter_eq_self_of_subset_left hBYb.subset_ground,
  diff_self_inter]
State after:
no goals

State before:
α : Type u_1
M✝ : Matroid α
B B' I I' J K X✝¹ Y : Set α
M : Matroid α
X✝ X : Set α
hX : X ⊆ M.E
BX : Set α
hBXb : M.Base BX
hI : M.Basis (BX ∩ X) X
hIBX : BX ∩ X ⊆ BX
hBXdual : M✶.Basis ((M.E \ X) \ BX) (M.E \ X)
BY : Set α
hBYb : M.Base BY
hJ : M.Basis (BY ∩ (M.E \ X)) (M.E \ X)
hBX : M.Basis BX (BX ∩ X ∪ BY ∩ (M.E \ X))
hIJE : M.Spanning (BX ∩ X ∪ BY ∩ (M.E \ X))
hBY : M.Basis BY (BX ∩ X ∪ BY ∩ (M.E \ X))
hJBY : BY ∩ (M.E \ X) ⊆ BY
hBYdual : M✶.Basis (X \ BY) X
⊢ M.E \ BY ⊆ X \ BY ∪ (M.E \ X) \ BX
Tactic:
rw [← union_diff_cancel hX, union_diff_distrib, union_diff_cancel hX, diff_diff, diff_diff]
State after:
α : Type u_1
M✝ : Matroid α
B B' I I' J K X✝¹ Y : Set α
M : Matroid α
X✝ X : Set α
hX : X ⊆ M.E
BX : Set α
hBXb : M.Base BX
hI : M.Basis (BX ∩ X) X
hIBX : BX ∩ X ⊆ BX
hBXdual : M✶.Basis ((M.E \ X) \ BX) (M.E \ X)
BY : Set α
hBYb : M.Base BY
hJ : M.Basis (BY ∩ (M.E \ X)) (M.E \ X)
hBX : M.Basis BX (BX ∩ X ∪ BY ∩ (M.E \ X))
hIJE : M.Spanning (BX ∩ X ∪ BY ∩ (M.E \ X))
hBY : M.Basis BY (BX ∩ X ∪ BY ∩ (M.E \ X))
hJBY : BY ∩ (M.E \ X) ⊆ BY
hBYdual : M✶.Basis (X \ BY) X
⊢ X \ BY ∪ M.E \ (X ∪ BY) ⊆ X \ BY ∪ M.E \ (X ∪ BX)

State before:
α : Type u_1
M✝ : Matroid α
B B' I I' J K X✝¹ Y : Set α
M : Matroid α
X✝ X : Set α
hX : X ⊆ M.E
BX : Set α
hBXb : M.Base BX
hI : M.Basis (BX ∩ X) X
hIBX : BX ∩ X ⊆ BX
hBXdual : M✶.Basis ((M.E \ X) \ BX) (M.E \ X)
BY : Set α
hBYb : M.Base BY
hJ : M.Basis (BY ∩ (M.E \ X)) (M.E \ X)
hBX : M.Basis BX (BX ∩ X ∪ BY ∩ (M.E \ X))
hIJE : M.Spanning (BX ∩ X ∪ BY ∩ (M.E \ X))
hBY : M.Basis BY (BX ∩ X ∪ BY ∩ (M.E \ X))
hJBY : BY ∩ (M.E \ X) ⊆ BY
hBYdual : M✶.Basis (X \ BY) X
⊢ X \ BY ∪ M.E \ (X ∪ BY) ⊆ X \ BY ∪ M.E \ (X ∪ BX)
Tactic:
refine union_subset_union_right _ (diff_subset_diff_right ?_)
State after:
α : Type u_1
M✝ : Matroid α
B B' I I' J K X✝¹ Y : Set α
M : Matroid α
X✝ X : Set α
hX : X ⊆ M.E
BX : Set α
hBXb : M.Base BX
hI : M.Basis (BX ∩ X) X
hIBX : BX ∩ X ⊆ BX
hBXdual : M✶.Basis ((M.E \ X) \ BX) (M.E \ X)
BY : Set α
hBYb : M.Base BY
hJ : M.Basis (BY ∩ (M.E \ X)) (M.E \ X)
hBX : M.Basis BX (BX ∩ X ∪ BY ∩ (M.E \ X))
hIJE : M.Spanning (BX ∩ X ∪ BY ∩ (M.E \ X))
hBY : M.Basis BY (BX ∩ X ∪ BY ∩ (M.E \ X))
hJBY : BY ∩ (M.E \ X) ⊆ BY
hBYdual : M✶.Basis (X \ BY) X
⊢ X ∪ BX ⊆ X ∪ BY

State before:
α : Type u_1
M✝ : Matroid α
B B' I I' J K X✝¹ Y : Set α
M : Matroid α
X✝ X : Set α
hX : X ⊆ M.E
BX : Set α
hBXb : M.Base BX
hI : M.Basis (BX ∩ X) X
hIBX : BX ∩ X ⊆ BX
hBXdual : M✶.Basis ((M.E \ X) \ BX) (M.E \ X)
BY : Set α
hBYb : M.Base BY
hJ : M.Basis (BY ∩ (M.E \ X)) (M.E \ X)
hBX : M.Basis BX (BX ∩ X ∪ BY ∩ (M.E \ X))
hIJE : M.Spanning (BX ∩ X ∪ BY ∩ (M.E \ X))
hBY : M.Basis BY (BX ∩ X ∪ BY ∩ (M.E \ X))
hJBY : BY ∩ (M.E \ X) ⊆ BY
hBYdual : M✶.Basis (X \ BY) X
⊢ X ∪ BX ⊆ X ∪ BY
Tactic:
simp only [union_subset_iff, subset_union_left, true_and]
State after:
α : Type u_1
M✝ : Matroid α
B B' I I' J K X✝¹ Y : Set α
M : Matroid α
X✝ X : Set α
hX : X ⊆ M.E
BX : Set α
hBXb : M.Base BX
hI : M.Basis (BX ∩ X) X
hIBX : BX ∩ X ⊆ BX
hBXdual : M✶.Basis ((M.E \ X) \ BX) (M.E \ X)
BY : Set α
hBYb : M.Base BY
hJ : M.Basis (BY ∩ (M.E \ X)) (M.E \ X)
hBX : M.Basis BX (BX ∩ X ∪ BY ∩ (M.E \ X))
hIJE : M.Spanning (BX ∩ X ∪ BY ∩ (M.E \ X))
hBY : M.Basis BY (BX ∩ X ∪ BY ∩ (M.E \ X))
hJBY : BY ∩ (M.E \ X) ⊆ BY
hBYdual : M✶.Basis (X \ BY) X
⊢ BX ⊆ X ∪ BY

State before:
α : Type u_1
M✝ : Matroid α
B B' I I' J K X✝¹ Y : Set α
M : Matroid α
X✝ X : Set α
hX : X ⊆ M.E
BX : Set α
hBXb : M.Base BX
hI : M.Basis (BX ∩ X) X
hIBX : BX ∩ X ⊆ BX
hBXdual : M✶.Basis ((M.E \ X) \ BX) (M.E \ X)
BY : Set α
hBYb : M.Base BY
hJ : M.Basis (BY ∩ (M.E \ X)) (M.E \ X)
hBX : M.Basis BX (BX ∩ X ∪ BY ∩ (M.E \ X))
hIJE : M.Spanning (BX ∩ X ∪ BY ∩ (M.E \ X))
hBY : M.Basis BY (BX ∩ X ∪ BY ∩ (M.E \ X))
hJBY : BY ∩ (M.E \ X) ⊆ BY
hBYdual : M✶.Basis (X \ BY) X
⊢ BX ⊆ X ∪ BY
Tactic:
exact hBX.subset.trans (union_subset_union inter_subset_right inter_subset_left)
State after:
no goals