internlm/Lean-Github huggingface dataset:
Theorem: Matroid.conn_compl_dual
Proof 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
Proof 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)
Theorem: Matroid.conn_compl_dual
Proof 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
Proof 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)
Theorem: Matroid.conn_compl_dual
Proof 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))
Proof 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)
Theorem: Matroid.conn_compl_dual
Proof 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
Proof 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)
Theorem: Matroid.conn_compl_dual
Proof 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
Proof 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)
Theorem: Matroid.conn_compl_dual
Proof 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
Proof 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)
Theorem: Matroid.conn_compl_dual
Proof 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
Proof 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)
Theorem: Matroid.conn_compl_dual
Proof 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 _ _)]
Proof 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
Theorem: Matroid.conn_compl_dual
Proof 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)
Proof state after:
no goals
Theorem: Matroid.conn_compl_dual
Proof 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]
Proof state after:
no goals
Theorem: Matroid.conn_compl_dual
Proof 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
Proof state after:
no goals
Theorem: Matroid.conn_compl_dual
Proof 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]
Proof state after:
no goals
Theorem: Matroid.conn_compl_dual
Proof 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]
Proof 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))
Theorem: Matroid.conn_compl_dual
Proof 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
Proof state after:
no goals
Theorem: Matroid.conn_compl_dual
Proof 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]
Proof 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))
Theorem: Matroid.conn_compl_dual
Proof 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
Proof state after:
no goals
Theorem: Matroid.conn_compl_dual
Proof 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]
Proof state after:
no goals
Theorem: Matroid.conn_compl_dual
Proof 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]
Proof 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)
Theorem: Matroid.conn_compl_dual
Proof 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 ?_)
Proof 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
Theorem: Matroid.conn_compl_dual
Proof 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]
Proof 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
Theorem: Matroid.conn_compl_dual
Proof 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)
Proof state after:
no goals
Theorem: Matroid.Partition.left_subset_ground
Proof state before:
α : Type u_1
M : Matroid α
k : ℕ
P✝ : Set α → Prop
a b : α
P : M.Partition
⊢ P.left ⊆ M.E
Tactic:
rw [← P.union_eq]
Proof state after:
α : Type u_1
M : Matroid α
k : ℕ
P✝ : Set α → Prop
a b : α
P : M.Partition
⊢ P.left ⊆ P.left ∪ P.right
Theorem: Matroid.Partition.left_subset_ground
Proof state before:
α : Type u_1
M : Matroid α
k : ℕ
P✝ : Set α → Prop
a b : α
P : M.Partition
⊢ P.left ⊆ P.left ∪ P.right
Tactic:
apply subset_union_left
Proof state after:
no goals
Theorem: Matroid.Partition.right_subset_ground
Proof state before:
α : Type u_1
M : Matroid α
k : ℕ
P✝ : Set α → Prop
a b : α
P : M.Partition
⊢ P.right ⊆ M.E
Tactic:
rw [← P.union_eq]
Proof state after:
α : Type u_1
M : Matroid α
k : ℕ
P✝ : Set α → Prop
a b : α
P : M.Partition
⊢ P.right ⊆ P.left ∪ P.right
Theorem: Matroid.Partition.right_subset_ground
Proof state before:
α : Type u_1
M : Matroid α
k : ℕ
P✝ : Set α → Prop
a b : α
P : M.Partition
⊢ P.right ⊆ P.left ∪ P.right
Tactic:
apply subset_union_right
Proof state after:
no goals
Theorem: Matroid.Partition.compl_left
Proof state before:
α : Type u_1
M : Matroid α
k : ℕ
P✝ : Set α → Prop
a b : α
P : M.Partition
⊢ M.E \ P.left = P.right
Tactic:
simp [← P.union_eq, P.disjoint.symm]
Proof state after:
no goals
Theorem: Matroid.Partition.compl_right
Proof state before:
α : Type u_1
M : Matroid α
k : ℕ
P✝ : Set α → Prop
a b : α
P : M.Partition
⊢ M.E \ P.right = P.left
Tactic:
simp [← P.union_eq, P.disjoint]
Proof state after:
no goals
Theorem: Matroid.Partition.conn_dual
Proof state before:
α : Type u_1
M : Matroid α
k : ℕ
P✝ : Set α → Prop
a b : α
P : M.Partition
⊢ P.dual.conn = P.conn
Tactic:
change M✶.conn _ _ = M.conn _ _
Proof state after:
α : Type u_1
M : Matroid α
k : ℕ
P✝ : Set α → Prop
a b : α
P : M.Partition
⊢ M✶.conn P.dual.left P.dual.right = M.conn P.left P.right
Theorem: Matroid.Partition.conn_dual
Proof state before:
α : Type u_1
M : Matroid α
k : ℕ
P✝ : Set α → Prop
a b : α
P : M.Partition
⊢ M✶.conn P.dual.left P.dual.right = M.conn P.left P.right
Tactic:
rw [← P.compl_left, conn_compl_dual, P.compl_left]
Proof state after:
α : Type u_1
M : Matroid α
k : ℕ
P✝ : Set α → Prop
a b : α
P : M.Partition
⊢ M✶.conn P.dual.left P.dual.right = M✶.conn P.left P.right
Theorem: Matroid.Partition.conn_dual
Proof state before:
α : Type u_1
M : Matroid α
k : ℕ
P✝ : Set α → Prop
a b : α
P : M.Partition
⊢ M✶.conn P.dual.left P.dual.right = M✶.conn P.left P.right
Tactic:
rfl
Proof state after:
no goals
Theorem: Matroid.connected_iff_not_exists_tutteSep
Proof state before:
α : Type u_1
M : Matroid α
k : ℕ
P : Set α → Prop
a b : α
inst✝ : M.Nonempty
⊢ M.Connected ↔ ¬∃ P, P.IsTutteSep 1
Tactic:
rw [iff_not_comm]
Proof state after:
α : Type u_1
M : Matroid α
k : ℕ
P : Set α → Prop
a b : α
inst✝ : M.Nonempty
⊢ (∃ P, P.IsTutteSep 1) ↔ ¬M.Connected
Theorem: Matroid.connected_iff_not_exists_tutteSep
Proof state before:
α : Type u_1
M : Matroid α
k : ℕ
P : Set α → Prop
a b : α
inst✝ : M.Nonempty
⊢ (∃ P, P.IsTutteSep 1) ↔ ¬M.Connected
Tactic:
simp only [Connected, show M.Nonempty by assumption, true_and, not_forall, Classical.not_imp,
  exists_and_left, exists_prop, exists_and_left, Partition.IsTutteSep, Nat.cast_one,
  ENat.lt_one_iff, one_le_encard_iff_nonempty]
Proof state after:
α : Type u_1
M : Matroid α
k : ℕ
P : Set α → Prop
a b : α
inst✝ : M.Nonempty
⊢ (∃ P, P.conn = 0 ∧ P.left.Nonempty ∧ P.right.Nonempty) ↔ ∃ x, ∃ x_1 ∈ M.E, x ∈ M.E ∧ ¬M.ConnectedTo x x_1
Theorem: Matroid.connected_iff_not_exists_tutteSep
Proof state before:
α : Type u_1
M : Matroid α
k : ℕ
P : Set α → Prop
a b : α
inst✝ : M.Nonempty
⊢ (∃ P, P.conn = 0 ∧ P.left.Nonempty ∧ P.right.Nonempty) ↔ ∃ x, ∃ x_1 ∈ M.E, x ∈ M.E ∧ ¬M.ConnectedTo x x_1
Tactic:
simp only [Partition.conn_eq_zero_iff, and_self,
  skew_iff_forall_circuit (Partition.disjoint _) (Partition.left_subset_ground _)
    (Partition.right_subset_ground _)]
Proof state after:
α : Type u_1
M : Matroid α
k : ℕ
P : Set α → Prop
a b : α
inst✝ : M.Nonempty
⊢ (∃ P,
      (∀ (C : Set α), M.Circuit C → C ⊆ P.left ∪ P.right → C ⊆ P.left ∨ C ⊆ P.right) ∧
        P.left.Nonempty ∧ P.right.Nonempty) ↔
    ∃ x, ∃ x_1 ∈ M.E, x ∈ M.E ∧ ¬M.ConnectedTo x x_1