internlm/Lean-Github huggingface dataset:
Theorem: Matroid.Basis'.encard_dual_switch_switch_eq
Proof 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]
Proof state after:
no goals
Theorem: Matroid.Basis'.encard_dual_switch_switch_eq
Proof 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]
Proof state after:
no goals
Theorem: Matroid.conn_comm
Proof state before:
α : Type u_1
M✝ : Matroid α
B B' I I' J K X✝ Y✝ : Set α
M : Matroid α
X Y : Set α
⊢ M.conn X Y = M.conn Y X
Tactic:
simp_rw [conn, union_comm, inter_comm]
Proof state after:
no goals
Theorem: Matroid.Basis'.conn_eq
Proof state before:
α : Type u_1
M : Matroid α
B B' I I' J K X Y : Set α
hI : M.Basis' I X
hJ : M.Basis' J Y
⊢ M.conn X Y = (I ∩ J).encard + (M ↾ (I ∪ J))✶.erk
Tactic:
simp_rw [conn, hI.encard_dual_switch_switch_eq (M.exists_basis' X).choose_spec hJ
  (M.exists_basis' Y).choose_spec]
Proof state after:
no goals
Theorem: Matroid.Basis'.conn_eq_of_disjoint
Proof state before:
α : Type u_1
M : Matroid α
B B' I I' J K X Y : Set α
hI : M.Basis' I X
hJ : M.Basis' J Y
hXY : Disjoint X Y
⊢ M.conn X Y = (M ↾ (I ∪ J))✶.erk
Tactic:
rw [hI.conn_eq hJ, (hXY.mono hI.subset hJ.subset).inter_eq, encard_empty, zero_add]
Proof state after:
no goals
Theorem: Matroid.conn_eq_encard_of_diff
Proof 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))
Proof 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
Theorem: Matroid.conn_eq_encard_of_diff
Proof 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]
Proof state after:
no goals
Theorem: Matroid.conn_eq_encard_of_diff
Proof 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))
Proof state after:
no goals
Theorem: Matroid.conn_eq_encard_of_diff'
Proof 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)
Proof 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)
Theorem: Matroid.conn_eq_encard_of_diff'
Proof 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 ]
Proof 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
Theorem: Matroid.conn_eq_encard_of_diff'
Proof 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))
Proof state after:
no goals
Theorem: Matroid.er_add_er_eq_er_union_add_conn
Proof state before:
α : Type u_1
M✝ : Matroid α
B B' I I' J K X✝ Y✝ : Set α
M : Matroid α
X Y : Set α
⊢ M.er X + M.er Y = M.er (X ∪ Y) + M.conn X Y
Tactic:
obtain ⟨I, hI⟩ := M.exists_basis' X
Proof state after:
case intro
α : Type u_1
M✝ : Matroid α
B B' I✝ I' J K X✝ Y✝ : Set α
M : Matroid α
X Y I : Set α
hI : M.Basis' I X
⊢ M.er X + M.er Y = M.er (X ∪ Y) + M.conn X Y
Theorem: Matroid.er_add_er_eq_er_union_add_conn
Proof state before:
case intro
α : Type u_1
M✝ : Matroid α
B B' I✝ I' J K X✝ Y✝ : Set α
M : Matroid α
X Y I : Set α
hI : M.Basis' I X
⊢ M.er X + M.er Y = M.er (X ∪ Y) + M.conn X Y
Tactic:
obtain ⟨J, hJ⟩ := M.exists_basis' Y
Proof state after:
case intro.intro
α : Type u_1
M✝ : Matroid α
B B' I✝ I' J✝ K X✝ Y✝ : Set α
M : Matroid α
X Y I : Set α
hI : M.Basis' I X
J : Set α
hJ : M.Basis' J Y
⊢ M.er X + M.er Y = M.er (X ∪ Y) + M.conn X Y
Theorem: Matroid.er_add_er_eq_er_union_add_conn
Proof state before:
case intro.intro
α : Type u_1
M✝ : Matroid α
B B' I✝ I' J✝ K X✝ Y✝ : Set α
M : Matroid α
X Y I : Set α
hI : M.Basis' I X
J : Set α
hJ : M.Basis' J Y
⊢ M.er X + M.er Y = M.er (X ∪ Y) + M.conn X Y
Tactic:
obtain ⟨B, hB⟩ := M.exists_basis' (I ∪ J)
Proof state after:
case intro.intro.intro
α : Type u_1
M✝ : Matroid α
B✝ B' I✝ I' J✝ K X✝ Y✝ : Set α
M : Matroid α
X Y I : Set α
hI : M.Basis' I X
J : Set α
hJ : M.Basis' J Y
B : Set α
hB : M.Basis' B (I ∪ J)
⊢ M.er X + M.er Y = M.er (X ∪ Y) + M.conn X Y
Theorem: Matroid.er_add_er_eq_er_union_add_conn
Proof state before:
case intro.intro.intro
α : Type u_1
M✝ : Matroid α
B✝ B' I✝ I' J✝ K X✝ Y✝ : Set α
M : Matroid α
X Y I : Set α
hI : M.Basis' I X
J : Set α
hJ : M.Basis' J Y
B : Set α
hB : M.Basis' B (I ∪ J)
⊢ M.er X + M.er Y = M.er (X ∪ Y) + M.conn X Y
Tactic:
have hB' : M.Basis' B (X ∪ Y) := by
  rw [basis'_iff_basis_cl, ← cl_cl_union_cl_eq_cl_union, ← hI.cl_eq_cl, ← hJ.cl_eq_cl,
     cl_cl_union_cl_eq_cl_union, ← hB.cl_eq_cl]
  exact ⟨hB.indep.basis_cl, hB.subset.trans (union_subset_union hI.subset hJ.subset)⟩
Proof state after:
case intro.intro.intro
α : Type u_1
M✝ : Matroid α
B✝ B' I✝ I' J✝ K X✝ Y✝ : Set α
M : Matroid α
X Y I : Set α
hI : M.Basis' I X
J : Set α
hJ : M.Basis' J Y
B : Set α
hB : M.Basis' B (I ∪ J)
hB' : M.Basis' B (X ∪ Y)
⊢ M.er X + M.er Y = M.er (X ∪ Y) + M.conn X Y
Theorem: Matroid.er_add_er_eq_er_union_add_conn
Proof state before:
case intro.intro.intro
α : Type u_1
M✝ : Matroid α
B✝ B' I✝ I' J✝ K X✝ Y✝ : Set α
M : Matroid α
X Y I : Set α
hI : M.Basis' I X
J : Set α
hJ : M.Basis' J Y
B : Set α
hB : M.Basis' B (I ∪ J)
hB' : M.Basis' B (X ∪ Y)
⊢ M.er X + M.er Y = M.er (X ∪ Y) + M.conn X Y
Tactic:
rw [hI.conn_eq hJ, ← hI.encard, ← hJ.encard, ← encard_union_add_encard_inter, ← hB'.encard,
  ← (base_restrict_iff'.2 hB).encard_compl_eq, restrict_ground_eq, ← add_assoc, add_comm B.encard,
  add_assoc, add_comm B.encard, encard_diff_add_encard_of_subset hB.subset, add_comm]
Proof state after:
no goals
Theorem: Matroid.er_add_er_eq_er_union_add_conn
Proof state before:
α : Type u_1
M✝ : Matroid α
B✝ B' I✝ I' J✝ K X✝ Y✝ : Set α
M : Matroid α
X Y I : Set α
hI : M.Basis' I X
J : Set α
hJ : M.Basis' J Y
B : Set α
hB : M.Basis' B (I ∪ J)
⊢ M.Basis' B (X ∪ Y)
Tactic:
rw [basis'_iff_basis_cl, ← cl_cl_union_cl_eq_cl_union, ← hI.cl_eq_cl, ← hJ.cl_eq_cl,
   cl_cl_union_cl_eq_cl_union, ← hB.cl_eq_cl]
Proof state after:
α : Type u_1
M✝ : Matroid α
B✝ B' I✝ I' J✝ K X✝ Y✝ : Set α
M : Matroid α
X Y I : Set α
hI : M.Basis' I X
J : Set α
hJ : M.Basis' J Y
B : Set α
hB : M.Basis' B (I ∪ J)
⊢ M.Basis B (M.cl B) ∧ B ⊆ X ∪ Y
Theorem: Matroid.er_add_er_eq_er_union_add_conn
Proof state before:
α : Type u_1
M✝ : Matroid α
B✝ B' I✝ I' J✝ K X✝ Y✝ : Set α
M : Matroid α
X Y I : Set α
hI : M.Basis' I X
J : Set α
hJ : M.Basis' J Y
B : Set α
hB : M.Basis' B (I ∪ J)
⊢ M.Basis B (M.cl B) ∧ B ⊆ X ∪ Y
Tactic:
exact ⟨hB.indep.basis_cl, hB.subset.trans (union_subset_union hI.subset hJ.subset)⟩
Proof state after:
no goals
Theorem: Matroid.conn_cl_left
Proof state before:
α : Type u_1
M✝ : Matroid α
B B' I I' J K X✝ Y✝ : Set α
M : Matroid α
X Y : Set α
⊢ M.conn X Y = M.conn (M.cl X) Y
Tactic:
obtain ⟨I, hI⟩ := M.exists_basis' X
Proof state after:
case intro
α : Type u_1
M✝ : Matroid α
B B' I✝ I' J K X✝ Y✝ : Set α
M : Matroid α
X Y I : Set α
hI : M.Basis' I X
⊢ M.conn X Y = M.conn (M.cl X) Y
Theorem: Matroid.conn_cl_left
Proof state before:
case intro
α : Type u_1
M✝ : Matroid α
B B' I✝ I' J K X✝ Y✝ : Set α
M : Matroid α
X Y I : Set α
hI : M.Basis' I X
⊢ M.conn X Y = M.conn (M.cl X) Y
Tactic:
obtain ⟨J, hJ⟩ := M.exists_basis' Y
Proof state after:
case intro.intro
α : Type u_1
M✝ : Matroid α
B B' I✝ I' J✝ K X✝ Y✝ : Set α
M : Matroid α
X Y I : Set α
hI : M.Basis' I X
J : Set α
hJ : M.Basis' J Y
⊢ M.conn X Y = M.conn (M.cl X) Y
Theorem: Matroid.conn_cl_left
Proof state before:
case intro.intro
α : Type u_1
M✝ : Matroid α
B B' I✝ I' J✝ K X✝ Y✝ : Set α
M : Matroid α
X Y I : Set α
hI : M.Basis' I X
J : Set α
hJ : M.Basis' J Y
⊢ M.conn X Y = M.conn (M.cl X) Y
Tactic:
rw [hI.conn_eq hJ, hI.basis_cl_right.basis'.conn_eq hJ]
Proof state after:
no goals
Theorem: Matroid.conn_cl_right
Proof state before:
α : Type u_1
M✝ : Matroid α
B B' I I' J K X✝ Y✝ : Set α
M : Matroid α
X Y : Set α
⊢ M.conn X Y = M.conn X (M.cl Y)
Tactic:
rw [conn_comm, conn_cl_left, conn_comm]
Proof state after:
no goals
Theorem: Matroid.conn_cl_cl
Proof state before:
α : Type u_1
M✝ : Matroid α
B B' I I' J K X✝ Y✝ : Set α
M : Matroid α
X Y : Set α
⊢ M.conn X Y = M.conn (M.cl X) (M.cl Y)
Tactic:
rw [conn_cl_left, conn_cl_right]
Proof state after:
no goals
Theorem: Matroid.conn_mono_left
Proof state before:
α : Type u_1
M✝ : Matroid α
B B' I I' J K X Y✝ X' : Set α
M : Matroid α
hX : X' ⊆ X
Y : Set α
⊢ M.conn X' Y ≤ M.conn X Y
Tactic:
obtain ⟨I', hI'⟩ := M.exists_basis' X'
Proof state after:
case intro
α : Type u_1
M✝ : Matroid α
B B' I I'✝ J K X Y✝ X' : Set α
M : Matroid α
hX : X' ⊆ X
Y I' : Set α
hI' : M.Basis' I' X'
⊢ M.conn X' Y ≤ M.conn X Y
Theorem: Matroid.conn_mono_left
Proof state before:
case intro
α : Type u_1
M✝ : Matroid α
B B' I I'✝ J K X Y✝ X' : Set α
M : Matroid α
hX : X' ⊆ X
Y I' : Set α
hI' : M.Basis' I' X'
⊢ M.conn X' Y ≤ M.conn X Y
Tactic:
obtain ⟨I, hI, hII'⟩ := hI'.indep.subset_basis'_of_subset (hI'.subset.trans hX)
Proof state after:
case intro.intro.intro
α : Type u_1
M✝ : Matroid α
B B' I✝ I'✝ J K X Y✝ X' : Set α
M : Matroid α
hX : X' ⊆ X
Y I' : Set α
hI' : M.Basis' I' X'
I : Set α
hI : M.Basis' I X
hII' : I' ⊆ I
⊢ M.conn X' Y ≤ M.conn X Y
Theorem: Matroid.conn_mono_left
Proof state before:
case intro.intro.intro
α : Type u_1
M✝ : Matroid α
B B' I✝ I'✝ J K X Y✝ X' : Set α
M : Matroid α
hX : X' ⊆ X
Y I' : Set α
hI' : M.Basis' I' X'
I : Set α
hI : M.Basis' I X
hII' : I' ⊆ I
⊢ M.conn X' Y ≤ M.conn X Y
Tactic:
obtain ⟨J, hJ⟩ := M.exists_basis' Y
Proof state after:
case intro.intro.intro.intro
α : Type u_1
M✝ : Matroid α
B B' I✝ I'✝ J✝ K X Y✝ X' : Set α
M : Matroid α
hX : X' ⊆ X
Y I' : Set α
hI' : M.Basis' I' X'
I : Set α
hI : M.Basis' I X
hII' : I' ⊆ I
J : Set α
hJ : M.Basis' J Y
⊢ M.conn X' Y ≤ M.conn X Y
Theorem: Matroid.conn_mono_left
Proof state before:
case intro.intro.intro.intro
α : Type u_1
M✝ : Matroid α
B B' I✝ I'✝ J✝ K X Y✝ X' : Set α
M : Matroid α
hX : X' ⊆ X
Y I' : Set α
hI' : M.Basis' I' X'
I : Set α
hI : M.Basis' I X
hII' : I' ⊆ I
J : Set α
hJ : M.Basis' J Y
⊢ M.conn X' Y ≤ M.conn X Y
Tactic:
rw [hI'.conn_eq hJ, hI.conn_eq hJ]
Proof state after:
case intro.intro.intro.intro
α : Type u_1
M✝ : Matroid α
B B' I✝ I'✝ J✝ K X Y✝ X' : Set α
M : Matroid α
hX : X' ⊆ X
Y I' : Set α
hI' : M.Basis' I' X'
I : Set α
hI : M.Basis' I X
hII' : I' ⊆ I
J : Set α
hJ : M.Basis' J Y
⊢ (I' ∩ J).encard + (M ↾ (I' ∪ J))✶.erk ≤ (I ∩ J).encard + (M ↾ (I ∪ J))✶.erk
Theorem: Matroid.conn_mono_left
Proof state before:
case intro.intro.intro.intro
α : Type u_1
M✝ : Matroid α
B B' I✝ I'✝ J✝ K X Y✝ X' : Set α
M : Matroid α
hX : X' ⊆ X
Y I' : Set α
hI' : M.Basis' I' X'
I : Set α
hI : M.Basis' I X
hII' : I' ⊆ I
J : Set α
hJ : M.Basis' J Y
⊢ (I' ∩ J).encard + (M ↾ (I' ∪ J))✶.erk ≤ (I ∩ J).encard + (M ↾ (I ∪ J))✶.erk
Tactic:
refine add_le_add (encard_le_card (inter_subset_inter_left _ hII')) (Minor.erk_le ?_)
Proof state after:
case intro.intro.intro.intro
α : Type u_1
M✝ : Matroid α
B B' I✝ I'✝ J✝ K X Y✝ X' : Set α
M : Matroid α
hX : X' ⊆ X
Y I' : Set α
hI' : M.Basis' I' X'
I : Set α
hI : M.Basis' I X
hII' : I' ⊆ I
J : Set α
hJ : M.Basis' J Y
⊢ (M ↾ (I' ∪ J))✶ ≤m (M ↾ (I ∪ J))✶
Theorem: Matroid.conn_mono_left
Proof state before:
case intro.intro.intro.intro
α : Type u_1
M✝ : Matroid α
B B' I✝ I'✝ J✝ K X Y✝ X' : Set α
M : Matroid α
hX : X' ⊆ X
Y I' : Set α
hI' : M.Basis' I' X'
I : Set α
hI : M.Basis' I X
hII' : I' ⊆ I
J : Set α
hJ : M.Basis' J Y
⊢ (M ↾ (I' ∪ J))✶ ≤m (M ↾ (I ∪ J))✶
Tactic:
rw [dual_minor_iff]
Proof state after:
case intro.intro.intro.intro
α : Type u_1
M✝ : Matroid α
B B' I✝ I'✝ J✝ K X Y✝ X' : Set α
M : Matroid α
hX : X' ⊆ X
Y I' : Set α
hI' : M.Basis' I' X'
I : Set α
hI : M.Basis' I X
hII' : I' ⊆ I
J : Set α
hJ : M.Basis' J Y
⊢ M ↾ (I' ∪ J) ≤m M ↾ (I ∪ J)
Theorem: Matroid.conn_mono_left
Proof state before:
case intro.intro.intro.intro
α : Type u_1
M✝ : Matroid α
B B' I✝ I'✝ J✝ K X Y✝ X' : Set α
M : Matroid α
hX : X' ⊆ X
Y I' : Set α
hI' : M.Basis' I' X'
I : Set α
hI : M.Basis' I X
hII' : I' ⊆ I
J : Set α
hJ : M.Basis' J Y
⊢ M ↾ (I' ∪ J) ≤m M ↾ (I ∪ J)
Tactic:
exact (Restriction.of_subset M (union_subset_union_left _ hII')).minor
Proof state after:
no goals
Theorem: Matroid.conn_mono_right
Proof state before:
α : Type u_1
M✝ : Matroid α
B B' I I' J K X✝ Y Y' : Set α
M : Matroid α
X : Set α
hY : Y' ⊆ Y
⊢ M.conn X Y' ≤ M.conn X Y
Tactic:
rw [conn_comm, conn_comm _ X]
Proof state after:
α : Type u_1
M✝ : Matroid α
B B' I I' J K X✝ Y Y' : Set α
M : Matroid α
X : Set α
hY : Y' ⊆ Y
⊢ M.conn Y' X ≤ M.conn Y X
Theorem: Matroid.conn_mono_right
Proof state before:
α : Type u_1
M✝ : Matroid α
B B' I I' J K X✝ Y Y' : Set α
M : Matroid α
X : Set α
hY : Y' ⊆ Y
⊢ M.conn Y' X ≤ M.conn Y X
Tactic:
exact M.conn_mono_left hY _
Proof state after:
no goals
Theorem: Matroid.empty_conn
Proof state before:
α : Type u_1
M✝ : Matroid α
B B' I I' J K X✝ Y : Set α
M : Matroid α
X : Set α
⊢ M.conn ∅ X = 0
Tactic:
obtain ⟨I, hI⟩ := M.exists_basis' X
Proof state after:
case intro
α : Type u_1
M✝ : Matroid α
B B' I✝ I' J K X✝ Y : Set α
M : Matroid α
X I : Set α
hI : M.Basis' I X
⊢ M.conn ∅ X = 0
Theorem: Matroid.empty_conn
Proof state before:
case intro
α : Type u_1
M✝ : Matroid α
B B' I✝ I' J K X✝ Y : Set α
M : Matroid α
X I : Set α
hI : M.Basis' I X
⊢ M.conn ∅ X = 0
Tactic:
rw [(M.empty_indep.basis_self.basis').conn_eq hI, empty_inter, encard_empty,
  erk_dual_restrict_eq_zero_iff.2 (by simpa using hI.indep), zero_add]
Proof state after:
no goals
Theorem: Matroid.empty_conn
Proof state before:
α : Type u_1
M✝ : Matroid α
B B' I✝ I' J K X✝ Y : Set α
M : Matroid α
X I : Set α
hI : M.Basis' I X
⊢ M.Indep (∅ ∪ I)
Tactic:
simpa using hI.indep
Proof state after:
no goals
Theorem: Matroid.conn_empty
Proof state before:
α : Type u_1
M✝ : Matroid α
B B' I I' J K X✝ Y : Set α
M : Matroid α
X : Set α
⊢ M.conn X ∅ = 0
Tactic:
rw [conn_comm, empty_conn]
Proof state after:
no goals
Theorem: Matroid.conn_subset
Proof state before:
α : Type u_1
M✝ : Matroid α
B B' I I' J K X Y : Set α
M : Matroid α
hXY : X ⊆ Y
⊢ M.conn X Y = M.er X
Tactic:
obtain ⟨I, hI⟩ := M.exists_basis' X
Proof state after:
case intro
α : Type u_1
M✝ : Matroid α
B B' I✝ I' J K X Y : Set α
M : Matroid α
hXY : X ⊆ Y
I : Set α
hI : M.Basis' I X
⊢ M.conn X Y = M.er X
Theorem: Matroid.conn_subset
Proof state before:
case intro
α : Type u_1
M✝ : Matroid α
B B' I✝ I' J K X Y : Set α
M : Matroid α
hXY : X ⊆ Y
I : Set α
hI : M.Basis' I X
⊢ M.conn X Y = M.er X
Tactic:
obtain ⟨J, hJ, hIJ⟩ := hI.indep.subset_basis'_of_subset (hI.subset.trans hXY)
Proof state after:
case intro.intro.intro
α : Type u_1
M✝ : Matroid α
B B' I✝ I' J✝ K X Y : Set α
M : Matroid α
hXY : X ⊆ Y
I : Set α
hI : M.Basis' I X
J : Set α
hJ : M.Basis' J Y
hIJ : I ⊆ J
⊢ M.conn X Y = M.er X
Theorem: Matroid.conn_subset
Proof state before:
case intro.intro.intro
α : Type u_1
M✝ : Matroid α
B B' I✝ I' J✝ K X Y : Set α
M : Matroid α
hXY : X ⊆ Y
I : Set α
hI : M.Basis' I X
J : Set α
hJ : M.Basis' J Y
hIJ : I ⊆ J
⊢ M.conn X Y = M.er X
Tactic:
rw [hI.conn_eq hJ, inter_eq_self_of_subset_left hIJ, union_eq_self_of_subset_left hIJ,
  hJ.indep.erk_dual_restrict_eq, ← hI.encard, add_zero]
Proof state after:
no goals
Theorem: Matroid.conn_eq_zero
Proof state before:
α : Type u_1
M✝ : Matroid α
B B' I I' J K X Y : Set α
M : Matroid α
hX : autoParam (X ⊆ M.E) _auto✝
hY : autoParam (Y ⊆ M.E) _auto✝
⊢ M.conn X Y = 0 ↔ M.Skew X Y
Tactic:
obtain ⟨I, hI⟩ := M.exists_basis X
Proof state after:
case intro
α : Type u_1
M✝ : Matroid α
B B' I✝ I' J K X Y : Set α
M : Matroid α
hX : autoParam (X ⊆ M.E) _auto✝
hY : autoParam (Y ⊆ M.E) _auto✝
I : Set α
hI : M.Basis I X
⊢ M.conn X Y = 0 ↔ M.Skew X Y
Theorem: Matroid.conn_eq_zero
Proof state before:
case intro
α : Type u_1
M✝ : Matroid α
B B' I✝ I' J K X Y : Set α
M : Matroid α
hX : autoParam (X ⊆ M.E) _auto✝
hY : autoParam (Y ⊆ M.E) _auto✝
I : Set α
hI : M.Basis I X
⊢ M.conn X Y = 0 ↔ M.Skew X Y
Tactic:
obtain ⟨J, hJ⟩ := M.exists_basis Y
Proof state after:
case intro.intro
α : Type u_1
M✝ : Matroid α
B B' I✝ I' J✝ K X Y : Set α
M : Matroid α
hX : autoParam (X ⊆ M.E) _auto✝
hY : autoParam (Y ⊆ M.E) _auto✝
I : Set α
hI : M.Basis I X
J : Set α
hJ : M.Basis J Y
⊢ M.conn X Y = 0 ↔ M.Skew X Y
Theorem: Matroid.conn_eq_zero
Proof state before:
case intro.intro
α : Type u_1
M✝ : Matroid α
B B' I✝ I' J✝ K X Y : Set α
M : Matroid α
hX : autoParam (X ⊆ M.E) _auto✝
hY : autoParam (Y ⊆ M.E) _auto✝
I : Set α
hI : M.Basis I X
J : Set α
hJ : M.Basis J Y
⊢ M.conn X Y = 0 ↔ M.Skew X Y
Tactic:
rw [skew_iff_cl_skew, conn_cl_cl, ← hI.cl_eq_cl, ← hJ.cl_eq_cl, ← skew_iff_cl_skew,
  ← conn_cl_cl, hI.indep.conn_eq hJ.indep, add_eq_zero_iff, encard_eq_zero,
  ← disjoint_iff_inter_eq_empty, erk_dual_restrict_eq_zero_iff,
  hI.indep.skew_iff_disjoint_union_indep hJ.indep]
Proof state after:
no goals
Theorem: Matroid.conn_eq_conn_inter_ground
Proof state before:
α : Type u_1
M✝ : Matroid α
B B' I I' J K X✝ Y✝ : Set α
M : Matroid α
X Y : Set α
⊢ M.conn X Y = M.conn (X ∩ M.E) (Y ∩ M.E)
Tactic:
rw [conn_cl_cl, ← cl_inter_ground, ← cl_inter_ground _ Y, ← conn_cl_cl]
Proof state after:
no goals
Theorem: Matroid.conn_eq_conn_inter_ground_left
Proof state before:
α : Type u_1
M✝ : Matroid α
B B' I I' J K X✝ Y✝ : Set α
M : Matroid α
X Y : Set α
⊢ M.conn X Y = M.conn (X ∩ M.E) Y
Tactic:
rw [conn_cl_left, ← cl_inter_ground, ← conn_cl_left]
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 α
⊢ 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]
Proof 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)
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 α
⊢ ∀ X ⊆ M.E, M.conn X (M.E \ X) = M✶.conn X (M.E \ X)
Tactic:
intro X hX
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
⊢ M.conn X (M.E \ X) = M✶.conn X (M.E \ X)
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
⊢ M.conn X (M.E \ X) = M✶.conn X (M.E \ X)
Tactic:
obtain ⟨I, hI⟩ := M.exists_basis X
Proof 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)
Theorem: Matroid.conn_compl_dual
Proof 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)
Proof 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)
Theorem: Matroid.conn_compl_dual
Proof 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))
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
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)
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
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]
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
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)
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
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
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
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)
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
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
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)
⊢ M.conn X (M.E \ X) = M✶.conn X (M.E \ X)