internlm/Lean-Github huggingface dataset:
Theorem: Matroid.ModularPair.inter_cl_eq
Proof state before:
ι : Type u_1
α : Type u_2
M : Matroid α
B I J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
h : M.ModularPair X Y
⊢ M.cl (X ∩ Y) = M.cl X ∩ M.cl Y
Tactic:
convert (ModularFamily.iInter_cl_eq_cl_iInter h).symm
Proof state after:
case h.e'_2.h.e'_3
ι : Type u_1
α : Type u_2
M : Matroid α
B I J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
h : M.ModularPair X Y
⊢ X ∩ Y = ⋂ i, bif i then X else Y

case h.e'_3
ι : Type u_1
α : Type u_2
M : Matroid α
B I J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
h : M.ModularPair X Y
⊢ M.cl X ∩ M.cl Y = ⋂ i, M.cl (bif i then X else Y)
Theorem: Matroid.ModularPair.inter_cl_eq
Proof state before:
case h.e'_3
ι : Type u_1
α : Type u_2
M : Matroid α
B I J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
h : M.ModularPair X Y
⊢ M.cl X ∩ M.cl Y = ⋂ i, M.cl (bif i then X else Y)
Tactic:
simp_rw [Bool.cond_eq_ite, apply_ite, ← Bool.cond_eq_ite, inter_eq_iInter]
Proof state after:
no goals
Theorem: Matroid.ModularPair.inter_cl_eq
Proof state before:
case h.e'_2.h.e'_3
ι : Type u_1
α : Type u_2
M : Matroid α
B I J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
h : M.ModularPair X Y
⊢ X ∩ Y = ⋂ i, bif i then X else Y
Tactic:
rw [inter_eq_iInter]
Proof state after:
no goals
Theorem: Matroid.modularPair_of_subset
Proof state before:
ι : Type u_1
α : Type u_2
M : Matroid α
B I J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
hXY : X ⊆ Y
hY : Y ⊆ M.E
⊢ M.ModularPair X Y
Tactic:
obtain ⟨I,J, hI, hJ, hIJ⟩ := M.exists_basis_subset_basis hXY
Proof state after:
case intro.intro.intro.intro
ι : Type u_1
α : Type u_2
M : Matroid α
B I✝ J✝ X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
hXY : X ⊆ Y
hY : Y ⊆ M.E
I J : Set α
hI : M.Basis I X
hJ : M.Basis J Y
hIJ : I ⊆ J
⊢ M.ModularPair X Y
Theorem: Matroid.modularPair_of_subset
Proof state before:
case intro.intro.intro.intro
ι : Type u_1
α : Type u_2
M : Matroid α
B I✝ J✝ X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
hXY : X ⊆ Y
hY : Y ⊆ M.E
I J : Set α
hI : M.Basis I X
hJ : M.Basis J Y
hIJ : I ⊆ J
⊢ M.ModularPair X Y
Tactic:
refine modularPair_iff.2 ⟨J, hJ.indep, ?_, by rwa [inter_eq_self_of_subset_right hJ.subset]⟩
Proof state after:
case intro.intro.intro.intro
ι : Type u_1
α : Type u_2
M : Matroid α
B I✝ J✝ X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
hXY : X ⊆ Y
hY : Y ⊆ M.E
I J : Set α
hI : M.Basis I X
hJ : M.Basis J Y
hIJ : I ⊆ J
⊢ M.Basis (X ∩ J) X
Theorem: Matroid.modularPair_of_subset
Proof state before:
case intro.intro.intro.intro
ι : Type u_1
α : Type u_2
M : Matroid α
B I✝ J✝ X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
hXY : X ⊆ Y
hY : Y ⊆ M.E
I J : Set α
hI : M.Basis I X
hJ : M.Basis J Y
hIJ : I ⊆ J
⊢ M.Basis (X ∩ J) X
Tactic:
rwa [← hI.eq_of_subset_indep (hJ.indep.inter_left X) (subset_inter hI.subset hIJ)
  inter_subset_left]
Proof state after:
no goals
Theorem: Matroid.modularPair_of_subset
Proof state before:
ι : Type u_1
α : Type u_2
M : Matroid α
B I✝ J✝ X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
hXY : X ⊆ Y
hY : Y ⊆ M.E
I J : Set α
hI : M.Basis I X
hJ : M.Basis J Y
hIJ : I ⊆ J
⊢ M.Basis (Y ∩ J) Y
Tactic:
rwa [inter_eq_self_of_subset_right hJ.subset]
Proof state after:
no goals
Theorem: Matroid.Indep.modularPair_of_union
Proof state before:
ι : Type u_1
α : Type u_2
M : Matroid α
B I J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
hi : M.Indep (I ∪ J)
⊢ M.ModularPair I J
Tactic:
simpa only [iUnion_subset_iff, Bool.forall_bool, cond_false, subset_union_right, cond_true,
  subset_union_left, and_self, forall_true_left] using
  hi.modularFamily_of_subsets (Js := fun i ↦ bif i then I else J)
Proof state after:
no goals
Theorem: Matroid.ModularPair.of_subset_cl_subset_cl
Proof state before:
ι : Type u_1
α : Type u_2
M : Matroid α
B I J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
h : M.ModularPair X Y
hXX' : X ⊆ X'
hX' : X' ⊆ M.cl X
hYY' : Y ⊆ Y'
hY' : Y' ⊆ M.cl Y
⊢ M.ModularPair X' Y'
Tactic:
apply ModularFamily.modularFamily_of_forall_subset_cl h
Proof state after:
case hXY
ι : Type u_1
α : Type u_2
M : Matroid α
B I J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
h : M.ModularPair X Y
hXX' : X ⊆ X'
hX' : X' ⊆ M.cl X
hYY' : Y ⊆ Y'
hY' : Y' ⊆ M.cl Y
⊢ ∀ (i : Bool), (bif i then X else Y) ⊆ bif i then X' else Y'

case hYX
ι : Type u_1
α : Type u_2
M : Matroid α
B I J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
h : M.ModularPair X Y
hXX' : X ⊆ X'
hX' : X' ⊆ M.cl X
hYY' : Y ⊆ Y'
hY' : Y' ⊆ M.cl Y
⊢ ∀ (i : Bool), (bif i then X' else Y') ⊆ M.cl (bif i then X else Y)
Theorem: Matroid.ModularPair.of_subset_cl_subset_cl
Proof state before:
case hYX
ι : Type u_1
α : Type u_2
M : Matroid α
B I J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
h : M.ModularPair X Y
hXX' : X ⊆ X'
hX' : X' ⊆ M.cl X
hYY' : Y ⊆ Y'
hY' : Y' ⊆ M.cl Y
⊢ ∀ (i : Bool), (bif i then X' else Y') ⊆ M.cl (bif i then X else Y)
Tactic:
simp [hY', hX']
Proof state after:
no goals
Theorem: Matroid.ModularPair.of_subset_cl_subset_cl
Proof state before:
case hXY
ι : Type u_1
α : Type u_2
M : Matroid α
B I J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
h : M.ModularPair X Y
hXX' : X ⊆ X'
hX' : X' ⊆ M.cl X
hYY' : Y ⊆ Y'
hY' : Y' ⊆ M.cl Y
⊢ ∀ (i : Bool), (bif i then X else Y) ⊆ bif i then X' else Y'
Tactic:
simp [hYY', hXX']
Proof state after:
no goals
Theorem: Matroid.modularPair_singleton
Proof state before:
ι : Type u_1
α : Type u_2
M : Matroid α
B I J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
he : e ∈ M.E
hX : X ⊆ M.E
heX : e ∉ M.cl X
⊢ M.ModularPair {e} X
Tactic:
obtain ⟨I, hI⟩ := M.exists_basis X
Proof state after:
case intro
ι : Type u_1
α : Type u_2
M : Matroid α
B I✝ J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
he : e ∈ M.E
hX : X ⊆ M.E
heX : e ∉ M.cl X
I : Set α
hI : M.Basis I X
⊢ M.ModularPair {e} X
Theorem: Matroid.modularPair_singleton
Proof state before:
case intro
ι : Type u_1
α : Type u_2
M : Matroid α
B I✝ J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
he : e ∈ M.E
hX : X ⊆ M.E
heX : e ∉ M.cl X
I : Set α
hI : M.Basis I X
⊢ M.ModularPair {e} X
Tactic:
have hi : M.Indep (insert e I) := by
  rw [hI.indep.insert_indep_iff, hI.cl_eq_cl]
  exact Or.inl ⟨he, heX⟩
Proof state after:
case intro
ι : Type u_1
α : Type u_2
M : Matroid α
B I✝ J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
he : e ∈ M.E
hX : X ⊆ M.E
heX : e ∉ M.cl X
I : Set α
hI : M.Basis I X
hi : M.Indep (insert e I)
⊢ M.ModularPair {e} X
Theorem: Matroid.modularPair_singleton
Proof state before:
case intro
ι : Type u_1
α : Type u_2
M : Matroid α
B I✝ J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
he : e ∈ M.E
hX : X ⊆ M.E
heX : e ∉ M.cl X
I : Set α
hI : M.Basis I X
hi : M.Indep (insert e I)
⊢ M.ModularPair {e} X
Tactic:
have hI' := hI.insert_basis_insert hi
Proof state after:
case intro
ι : Type u_1
α : Type u_2
M : Matroid α
B I✝ J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
he : e ∈ M.E
hX : X ⊆ M.E
heX : e ∉ M.cl X
I : Set α
hI : M.Basis I X
hi : M.Indep (insert e I)
hI' : M.Basis (insert e I) (insert e X)
⊢ M.ModularPair {e} X
Theorem: Matroid.modularPair_singleton
Proof state before:
case intro
ι : Type u_1
α : Type u_2
M : Matroid α
B I✝ J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
he : e ∈ M.E
hX : X ⊆ M.E
heX : e ∉ M.cl X
I : Set α
hI : M.Basis I X
hi : M.Indep (insert e I)
hI' : M.Basis (insert e I) (insert e X)
⊢ M.ModularPair {e} X
Tactic:
rw [← singleton_union] at hI'
Proof state after:
case intro
ι : Type u_1
α : Type u_2
M : Matroid α
B I✝ J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
he : e ∈ M.E
hX : X ⊆ M.E
heX : e ∉ M.cl X
I : Set α
hI : M.Basis I X
hi : M.Indep (insert e I)
hI' : M.Basis ({e} ∪ I) (insert e X)
⊢ M.ModularPair {e} X
Theorem: Matroid.modularPair_singleton
Proof state before:
case intro
ι : Type u_1
α : Type u_2
M : Matroid α
B I✝ J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
he : e ∈ M.E
hX : X ⊆ M.E
heX : e ∉ M.cl X
I : Set α
hI : M.Basis I X
hi : M.Indep (insert e I)
hI' : M.Basis ({e} ∪ I) (insert e X)
⊢ M.ModularPair {e} X
Tactic:
exact hI'.indep.modularPair_of_union.of_basis_right hI
Proof state after:
no goals
Theorem: Matroid.modularPair_singleton
Proof state before:
ι : Type u_1
α : Type u_2
M : Matroid α
B I✝ J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
he : e ∈ M.E
hX : X ⊆ M.E
heX : e ∉ M.cl X
I : Set α
hI : M.Basis I X
⊢ M.Indep (insert e I)
Tactic:
rw [hI.indep.insert_indep_iff, hI.cl_eq_cl]
Proof state after:
ι : Type u_1
α : Type u_2
M : Matroid α
B I✝ J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
he : e ∈ M.E
hX : X ⊆ M.E
heX : e ∉ M.cl X
I : Set α
hI : M.Basis I X
⊢ e ∈ M.E \ M.cl X ∨ e ∈ I
Theorem: Matroid.modularPair_singleton
Proof state before:
ι : Type u_1
α : Type u_2
M : Matroid α
B I✝ J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
he : e ∈ M.E
hX : X ⊆ M.E
heX : e ∉ M.cl X
I : Set α
hI : M.Basis I X
⊢ e ∈ M.E \ M.cl X ∨ e ∈ I
Tactic:
exact Or.inl ⟨he, heX⟩
Proof state after:
no goals
Theorem: Matroid.ModularPair.er_add_er
Proof state before:
ι : Type u_1
α : Type u_2
M : Matroid α
B I J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
h : M.ModularPair X Y
⊢ M.er X + M.er Y = M.er (X ∩ Y) + M.er (X ∪ Y)
Tactic:
obtain ⟨I, hIu, hIX, hIY, hIi⟩ := h.exists_common_basis
Proof state after:
case intro.intro.intro.intro
ι : Type u_1
α : Type u_2
M : Matroid α
B I✝ J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
h : M.ModularPair X Y
I : Set α
hIu : M.Basis I (X ∪ Y)
hIX : M.Basis (I ∩ X) X
hIY : M.Basis (I ∩ Y) Y
hIi : M.Basis (I ∩ X ∩ Y) (X ∩ Y)
⊢ M.er X + M.er Y = M.er (X ∩ Y) + M.er (X ∪ Y)
Theorem: Matroid.ModularPair.er_add_er
Proof state before:
case intro.intro.intro.intro
ι : Type u_1
α : Type u_2
M : Matroid α
B I✝ J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
h : M.ModularPair X Y
I : Set α
hIu : M.Basis I (X ∪ Y)
hIX : M.Basis (I ∩ X) X
hIY : M.Basis (I ∩ Y) Y
hIi : M.Basis (I ∩ X ∩ Y) (X ∩ Y)
⊢ M.er X + M.er Y = M.er (X ∩ Y) + M.er (X ∪ Y)
Tactic:
rw [hIi.er_eq_encard, hIu.er_eq_encard, hIX.er_eq_encard, hIY.er_eq_encard,
  ← encard_union_add_encard_inter, ← inter_union_distrib_left, ← inter_inter_distrib_left,
  ← inter_assoc, inter_eq_self_of_subset_left hIu.subset, add_comm]
Proof state after:
no goals
Theorem: Matroid.rFin.modularPair_iff
Proof state before:
ι : Type u_1
α : Type u_2
M : Matroid α
B I J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
hXfin : M.rFin X
hYfin : M.rFin Y
hXE : autoParam (X ⊆ M.E) _auto✝
hYE : autoParam (Y ⊆ M.E) _auto✝
⊢ M.ModularPair X Y ↔ M.er X + M.er Y = M.er (X ∩ Y) + M.er (X ∪ Y)
Tactic:
refine ⟨fun h ↦ h.er_add_er, fun hr ↦ modularPair_iff_exists_basis_basis.2 ?_ ⟩
Proof state after:
ι : Type u_1
α : Type u_2
M : Matroid α
B I J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
hXfin : M.rFin X
hYfin : M.rFin Y
hXE : autoParam (X ⊆ M.E) _auto✝
hYE : autoParam (Y ⊆ M.E) _auto✝
hr : M.er X + M.er Y = M.er (X ∩ Y) + M.er (X ∪ Y)
⊢ ∃ I J, M.Basis I X ∧ M.Basis J Y ∧ M.Indep (I ∪ J)
Theorem: Matroid.rFin.modularPair_iff
Proof state before:
ι : Type u_1
α : Type u_2
M : Matroid α
B I J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
hXfin : M.rFin X
hYfin : M.rFin Y
hXE : autoParam (X ⊆ M.E) _auto✝
hYE : autoParam (Y ⊆ M.E) _auto✝
hr : M.er X + M.er Y = M.er (X ∩ Y) + M.er (X ∪ Y)
⊢ ∃ I J, M.Basis I X ∧ M.Basis J Y ∧ M.Indep (I ∪ J)
Tactic:
obtain ⟨Ii, hIi⟩ := M.exists_basis (X ∩ Y)
Proof state after:
case intro
ι : Type u_1
α : Type u_2
M : Matroid α
B I J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
hXfin : M.rFin X
hYfin : M.rFin Y
hXE : autoParam (X ⊆ M.E) _auto✝
hYE : autoParam (Y ⊆ M.E) _auto✝
hr : M.er X + M.er Y = M.er (X ∩ Y) + M.er (X ∪ Y)
Ii : Set α
hIi : M.Basis Ii (X ∩ Y)
⊢ ∃ I J, M.Basis I X ∧ M.Basis J Y ∧ M.Indep (I ∪ J)
Theorem: Matroid.rFin.modularPair_iff
Proof state before:
case intro
ι : Type u_1
α : Type u_2
M : Matroid α
B I J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
hXfin : M.rFin X
hYfin : M.rFin Y
hXE : autoParam (X ⊆ M.E) _auto✝
hYE : autoParam (Y ⊆ M.E) _auto✝
hr : M.er X + M.er Y = M.er (X ∩ Y) + M.er (X ∪ Y)
Ii : Set α
hIi : M.Basis Ii (X ∩ Y)
⊢ ∃ I J, M.Basis I X ∧ M.Basis J Y ∧ M.Indep (I ∪ J)
Tactic:
have hifin : Ii.encard ≠ ⊤ := by
  simpa using (hXfin.inter_right Y).finite_of_basis hIi
Proof state after:
case intro
ι : Type u_1
α : Type u_2
M : Matroid α
B I J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
hXfin : M.rFin X
hYfin : M.rFin Y
hXE : autoParam (X ⊆ M.E) _auto✝
hYE : autoParam (Y ⊆ M.E) _auto✝
hr : M.er X + M.er Y = M.er (X ∩ Y) + M.er (X ∪ Y)
Ii : Set α
hIi : M.Basis Ii (X ∩ Y)
hifin : Ii.encard ≠ ⊤
⊢ ∃ I J, M.Basis I X ∧ M.Basis J Y ∧ M.Indep (I ∪ J)
Theorem: Matroid.rFin.modularPair_iff
Proof state before:
case intro
ι : Type u_1
α : Type u_2
M : Matroid α
B I J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
hXfin : M.rFin X
hYfin : M.rFin Y
hXE : autoParam (X ⊆ M.E) _auto✝
hYE : autoParam (Y ⊆ M.E) _auto✝
hr : M.er X + M.er Y = M.er (X ∩ Y) + M.er (X ∪ Y)
Ii : Set α
hIi : M.Basis Ii (X ∩ Y)
hifin : Ii.encard ≠ ⊤
⊢ ∃ I J, M.Basis I X ∧ M.Basis J Y ∧ M.Indep (I ∪ J)
Tactic:
obtain ⟨IX, hIX, hX⟩ := hIi.indep.subset_basis_of_subset
  (hIi.subset.trans inter_subset_left)
Proof state after:
case intro.intro.intro
ι : Type u_1
α : Type u_2
M : Matroid α
B I J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
hXfin : M.rFin X
hYfin : M.rFin Y
hXE : autoParam (X ⊆ M.E) _auto✝
hYE : autoParam (Y ⊆ M.E) _auto✝
hr : M.er X + M.er Y = M.er (X ∩ Y) + M.er (X ∪ Y)
Ii : Set α
hIi : M.Basis Ii (X ∩ Y)
hifin : Ii.encard ≠ ⊤
IX : Set α
hIX : M.Basis IX X
hX : Ii ⊆ IX
⊢ ∃ I J, M.Basis I X ∧ M.Basis J Y ∧ M.Indep (I ∪ J)
Theorem: Matroid.rFin.modularPair_iff
Proof state before:
case intro.intro.intro
ι : Type u_1
α : Type u_2
M : Matroid α
B I J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
hXfin : M.rFin X
hYfin : M.rFin Y
hXE : autoParam (X ⊆ M.E) _auto✝
hYE : autoParam (Y ⊆ M.E) _auto✝
hr : M.er X + M.er Y = M.er (X ∩ Y) + M.er (X ∪ Y)
Ii : Set α
hIi : M.Basis Ii (X ∩ Y)
hifin : Ii.encard ≠ ⊤
IX : Set α
hIX : M.Basis IX X
hX : Ii ⊆ IX
⊢ ∃ I J, M.Basis I X ∧ M.Basis J Y ∧ M.Indep (I ∪ J)
Tactic:
obtain ⟨IY, hIY, hY⟩ := hIi.indep.subset_basis_of_subset
  (hIi.subset.trans inter_subset_right)
Proof state after:
case intro.intro.intro.intro.intro
ι : Type u_1
α : Type u_2
M : Matroid α
B I J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
hXfin : M.rFin X
hYfin : M.rFin Y
hXE : autoParam (X ⊆ M.E) _auto✝
hYE : autoParam (Y ⊆ M.E) _auto✝
hr : M.er X + M.er Y = M.er (X ∩ Y) + M.er (X ∪ Y)
Ii : Set α
hIi : M.Basis Ii (X ∩ Y)
hifin : Ii.encard ≠ ⊤
IX : Set α
hIX : M.Basis IX X
hX : Ii ⊆ IX
IY : Set α
hIY : M.Basis IY Y
hY : Ii ⊆ IY
⊢ ∃ I J, M.Basis I X ∧ M.Basis J Y ∧ M.Indep (I ∪ J)
Theorem: Matroid.rFin.modularPair_iff
Proof state before:
case intro.intro.intro.intro.intro
ι : Type u_1
α : Type u_2
M : Matroid α
B I J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
hXfin : M.rFin X
hYfin : M.rFin Y
hXE : autoParam (X ⊆ M.E) _auto✝
hYE : autoParam (Y ⊆ M.E) _auto✝
hr : M.er X + M.er Y = M.er (X ∩ Y) + M.er (X ∪ Y)
Ii : Set α
hIi : M.Basis Ii (X ∩ Y)
hifin : Ii.encard ≠ ⊤
IX : Set α
hIX : M.Basis IX X
hX : Ii ⊆ IX
IY : Set α
hIY : M.Basis IY Y
hY : Ii ⊆ IY
⊢ ∃ I J, M.Basis I X ∧ M.Basis J Y ∧ M.Indep (I ∪ J)
Tactic:
refine ⟨IX, IY, hIX, hIY, ?_⟩
Proof state after:
case intro.intro.intro.intro.intro
ι : Type u_1
α : Type u_2
M : Matroid α
B I J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
hXfin : M.rFin X
hYfin : M.rFin Y
hXE : autoParam (X ⊆ M.E) _auto✝
hYE : autoParam (Y ⊆ M.E) _auto✝
hr : M.er X + M.er Y = M.er (X ∩ Y) + M.er (X ∪ Y)
Ii : Set α
hIi : M.Basis Ii (X ∩ Y)
hifin : Ii.encard ≠ ⊤
IX : Set α
hIX : M.Basis IX X
hX : Ii ⊆ IX
IY : Set α
hIY : M.Basis IY Y
hY : Ii ⊆ IY
⊢ M.Indep (IX ∪ IY)
Theorem: Matroid.rFin.modularPair_iff
Proof state before:
case intro.intro.intro.intro.intro
ι : Type u_1
α : Type u_2
M : Matroid α
B I J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
hXfin : M.rFin X
hYfin : M.rFin Y
hXE : autoParam (X ⊆ M.E) _auto✝
hYE : autoParam (Y ⊆ M.E) _auto✝
hr : M.er X + M.er Y = M.er (X ∩ Y) + M.er (X ∪ Y)
Ii : Set α
hIi : M.Basis Ii (X ∩ Y)
hifin : Ii.encard ≠ ⊤
IX : Set α
hIX : M.Basis IX X
hX : Ii ⊆ IX
IY : Set α
hIY : M.Basis IY Y
hY : Ii ⊆ IY
⊢ M.Indep (IX ∪ IY)
Tactic:
rw [hIi.er_eq_encard, hIX.er_eq_encard, ← encard_diff_add_encard_of_subset hX,
  add_comm (encard _), add_assoc, WithTop.add_left_cancel_iff hifin, hIY.er_eq_encard,
  ← encard_union_add_encard_inter, ← union_eq_self_of_subset_left hY, ← union_assoc,
  diff_union_self, union_eq_self_of_subset_right hX] at hr
Proof state after:
case intro.intro.intro.intro.intro
ι : Type u_1
α : Type u_2
M : Matroid α
B I J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
hXfin : M.rFin X
hYfin : M.rFin Y
hXE : autoParam (X ⊆ M.E) _auto✝
hYE : autoParam (Y ⊆ M.E) _auto✝
Ii : Set α
hIi : M.Basis Ii (X ∩ Y)
hifin : Ii.encard ≠ ⊤
IX : Set α
hIX : M.Basis IX X
hX : Ii ⊆ IX
IY : Set α
hr : (IX ∪ IY).encard + (IX \ Ii ∩ (Ii ∪ IY)).encard = M.er (X ∪ Y)
hIY : M.Basis IY Y
hY : Ii ⊆ IY
⊢ M.Indep (IX ∪ IY)
Theorem: Matroid.rFin.modularPair_iff
Proof state before:
case intro.intro.intro.intro.intro
ι : Type u_1
α : Type u_2
M : Matroid α
B I J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
hXfin : M.rFin X
hYfin : M.rFin Y
hXE : autoParam (X ⊆ M.E) _auto✝
hYE : autoParam (Y ⊆ M.E) _auto✝
Ii : Set α
hIi : M.Basis Ii (X ∩ Y)
hifin : Ii.encard ≠ ⊤
IX : Set α
hIX : M.Basis IX X
hX : Ii ⊆ IX
IY : Set α
hr : (IX ∪ IY).encard + (IX \ Ii ∩ (Ii ∪ IY)).encard = M.er (X ∪ Y)
hIY : M.Basis IY Y
hY : Ii ⊆ IY
⊢ M.Indep (IX ∪ IY)
Tactic:
refine Basis.indep <| (hXfin.union hYfin).basis_of_subset_cl_of_subset_of_encard_le ?_
  (union_subset_union hIX.subset hIY.subset) (le_of_add_le_left hr.le)
Proof state after:
case intro.intro.intro.intro.intro
ι : Type u_1
α : Type u_2
M : Matroid α
B I J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
hXfin : M.rFin X
hYfin : M.rFin Y
hXE : autoParam (X ⊆ M.E) _auto✝
hYE : autoParam (Y ⊆ M.E) _auto✝
Ii : Set α
hIi : M.Basis Ii (X ∩ Y)
hifin : Ii.encard ≠ ⊤
IX : Set α
hIX : M.Basis IX X
hX : Ii ⊆ IX
IY : Set α
hr : (IX ∪ IY).encard + (IX \ Ii ∩ (Ii ∪ IY)).encard = M.er (X ∪ Y)
hIY : M.Basis IY Y
hY : Ii ⊆ IY
⊢ X ∪ Y ⊆ M.cl (IX ∪ IY)
Theorem: Matroid.rFin.modularPair_iff
Proof state before:
case intro.intro.intro.intro.intro
ι : Type u_1
α : Type u_2
M : Matroid α
B I J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
hXfin : M.rFin X
hYfin : M.rFin Y
hXE : autoParam (X ⊆ M.E) _auto✝
hYE : autoParam (Y ⊆ M.E) _auto✝
Ii : Set α
hIi : M.Basis Ii (X ∩ Y)
hifin : Ii.encard ≠ ⊤
IX : Set α
hIX : M.Basis IX X
hX : Ii ⊆ IX
IY : Set α
hr : (IX ∪ IY).encard + (IX \ Ii ∩ (Ii ∪ IY)).encard = M.er (X ∪ Y)
hIY : M.Basis IY Y
hY : Ii ⊆ IY
⊢ X ∪ Y ⊆ M.cl (IX ∪ IY)
Tactic:
rw [← M.cl_union_cl_left_eq, ← M.cl_union_cl_right_eq]
Proof state after:
case intro.intro.intro.intro.intro
ι : Type u_1
α : Type u_2
M : Matroid α
B I J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
hXfin : M.rFin X
hYfin : M.rFin Y
hXE : autoParam (X ⊆ M.E) _auto✝
hYE : autoParam (Y ⊆ M.E) _auto✝
Ii : Set α
hIi : M.Basis Ii (X ∩ Y)
hifin : Ii.encard ≠ ⊤
IX : Set α
hIX : M.Basis IX X
hX : Ii ⊆ IX
IY : Set α
hr : (IX ∪ IY).encard + (IX \ Ii ∩ (Ii ∪ IY)).encard = M.er (X ∪ Y)
hIY : M.Basis IY Y
hY : Ii ⊆ IY
⊢ X ∪ Y ⊆ M.cl (M.cl IX ∪ M.cl IY)
Theorem: Matroid.rFin.modularPair_iff
Proof state before:
case intro.intro.intro.intro.intro
ι : Type u_1
α : Type u_2
M : Matroid α
B I J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
hXfin : M.rFin X
hYfin : M.rFin Y
hXE : autoParam (X ⊆ M.E) _auto✝
hYE : autoParam (Y ⊆ M.E) _auto✝
Ii : Set α
hIi : M.Basis Ii (X ∩ Y)
hifin : Ii.encard ≠ ⊤
IX : Set α
hIX : M.Basis IX X
hX : Ii ⊆ IX
IY : Set α
hr : (IX ∪ IY).encard + (IX \ Ii ∩ (Ii ∪ IY)).encard = M.er (X ∪ Y)
hIY : M.Basis IY Y
hY : Ii ⊆ IY
⊢ X ∪ Y ⊆ M.cl (M.cl IX ∪ M.cl IY)
Tactic:
exact (M.subset_cl _).trans (M.cl_subset_cl (union_subset_union hIX.subset_cl hIY.subset_cl))
Proof state after:
no goals
Theorem: Matroid.rFin.modularPair_iff
Proof state before:
ι : Type u_1
α : Type u_2
M : Matroid α
B I J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
hXfin : M.rFin X
hYfin : M.rFin Y
hXE : autoParam (X ⊆ M.E) _auto✝
hYE : autoParam (Y ⊆ M.E) _auto✝
hr : M.er X + M.er Y = M.er (X ∩ Y) + M.er (X ∪ Y)
Ii : Set α
hIi : M.Basis Ii (X ∩ Y)
⊢ Ii.encard ≠ ⊤
Tactic:
simpa using (hXfin.inter_right Y).finite_of_basis hIi
Proof state after:
no goals
Theorem: Matroid.modularPair_iff_r
Proof state before:
ι : Type u_1
α : Type u_2
M : Matroid α
B I J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
inst✝ : M.FiniteRk
hXE : autoParam (X ⊆ M.E) _auto✝
hYE : autoParam (Y ⊆ M.E) _auto✝
⊢ M.ModularPair X Y ↔ M.r X + M.r Y = M.r (X ∩ Y) + M.r (X ∪ Y)
Tactic:
simp_rw [(M.to_rFin X).modularPair_iff (M.to_rFin Y), ← coe_r_eq, ← Nat.cast_add, Nat.cast_inj]
Proof state after:
no goals
Theorem: Matroid.ModularFamily.modularPair_compl_biUnion
Proof state before:
ι : Type u_1
α : Type u_2
M : Matroid α
B I J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
h : M.ModularFamily Xs
A : Set ι
⊢ M.ModularPair (⋃ i ∈ A, Xs i) (⋃ i ∈ Aᶜ, Xs i)
Tactic:
rw [modularPair_iff]
Proof state after:
ι : Type u_1
α : Type u_2
M : Matroid α
B I J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
h : M.ModularFamily Xs
A : Set ι
⊢ ∃ I, M.Indep I ∧ M.Basis ((⋃ i ∈ A, Xs i) ∩ I) (⋃ i ∈ A, Xs i) ∧ M.Basis ((⋃ i ∈ Aᶜ, Xs i) ∩ I) (⋃ i ∈ Aᶜ, Xs i)
Theorem: Matroid.ModularFamily.modularPair_compl_biUnion
Proof state before:
ι : Type u_1
α : Type u_2
M : Matroid α
B I J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
h : M.ModularFamily Xs
A : Set ι
⊢ ∃ I, M.Indep I ∧ M.Basis ((⋃ i ∈ A, Xs i) ∩ I) (⋃ i ∈ A, Xs i) ∧ M.Basis ((⋃ i ∈ Aᶜ, Xs i) ∩ I) (⋃ i ∈ Aᶜ, Xs i)
Tactic:
obtain ⟨B, hB⟩ := h
Proof state after:
case intro
ι : Type u_1
α : Type u_2
M : Matroid α
B✝ I J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
A : Set ι
B : Set α
hB : M.ModularBase B Xs
⊢ ∃ I, M.Indep I ∧ M.Basis ((⋃ i ∈ A, Xs i) ∩ I) (⋃ i ∈ A, Xs i) ∧ M.Basis ((⋃ i ∈ Aᶜ, Xs i) ∩ I) (⋃ i ∈ Aᶜ, Xs i)
Theorem: Matroid.ModularFamily.modularPair_compl_biUnion
Proof state before:
case intro
ι : Type u_1
α : Type u_2
M : Matroid α
B✝ I J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
A : Set ι
B : Set α
hB : M.ModularBase B Xs
⊢ ∃ I, M.Indep I ∧ M.Basis ((⋃ i ∈ A, Xs i) ∩ I) (⋃ i ∈ A, Xs i) ∧ M.Basis ((⋃ i ∈ Aᶜ, Xs i) ∩ I) (⋃ i ∈ Aᶜ, Xs i)
Tactic:
exact ⟨B, hB.indep, hB.basis_biUnion A, hB.basis_biUnion Aᶜ⟩
Proof state after:
no goals
Theorem: Matroid.ModularFamily.modularPair_compl_biInter
Proof state before:
ι : Type u_1
α : Type u_2
M : Matroid α
B I J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
h : M.ModularFamily Xs
A : Set ι
hA : A.Nonempty
hA' : A ≠ univ
⊢ M.ModularPair (⋂ i ∈ A, Xs i) (⋂ i ∈ Aᶜ, Xs i)
Tactic:
rw [modularPair_iff]
Proof state after:
ι : Type u_1
α : Type u_2
M : Matroid α
B I J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
h : M.ModularFamily Xs
A : Set ι
hA : A.Nonempty
hA' : A ≠ univ
⊢ ∃ I, M.Indep I ∧ M.Basis ((⋂ i ∈ A, Xs i) ∩ I) (⋂ i ∈ A, Xs i) ∧ M.Basis ((⋂ i ∈ Aᶜ, Xs i) ∩ I) (⋂ i ∈ Aᶜ, Xs i)
Theorem: Matroid.ModularFamily.modularPair_compl_biInter
Proof state before:
ι : Type u_1
α : Type u_2
M : Matroid α
B I J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
h : M.ModularFamily Xs
A : Set ι
hA : A.Nonempty
hA' : A ≠ univ
⊢ ∃ I, M.Indep I ∧ M.Basis ((⋂ i ∈ A, Xs i) ∩ I) (⋂ i ∈ A, Xs i) ∧ M.Basis ((⋂ i ∈ Aᶜ, Xs i) ∩ I) (⋂ i ∈ Aᶜ, Xs i)
Tactic:
obtain ⟨B, hB⟩ := h
Proof state after:
case intro
ι : Type u_1
α : Type u_2
M : Matroid α
B✝ I J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
A : Set ι
hA : A.Nonempty
hA' : A ≠ univ
B : Set α
hB : M.ModularBase B Xs
⊢ ∃ I, M.Indep I ∧ M.Basis ((⋂ i ∈ A, Xs i) ∩ I) (⋂ i ∈ A, Xs i) ∧ M.Basis ((⋂ i ∈ Aᶜ, Xs i) ∩ I) (⋂ i ∈ Aᶜ, Xs i)