internlm/Lean-Github huggingface dataset:
Theorem: Matroid.modularFamily_map_iff
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✝ : α
β : Type u_3
f : α → β
hf : InjOn f M.E
Xs : ι → Set β
B : Set α
hB : M.Base B
Is Ys : ι → Set α
hYs : ∀ (i : ι), M.Basis (Is i) (Ys i) ∧ Xs i ∩ f '' B = f '' Is i ∧ Xs i = f '' Ys i
i : ι
⊢ Ys i ∩ B = Is i
Tactic:
rw [← hf.image_eq_image_iff (inter_subset_right.trans hB.subset_ground)
  (hYs i).1.indep.subset_ground, ← (hYs i).2.1, (hYs i).2.2, hf.image_inter]
Proof state after:
case h.e'_3.hs
ι : 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✝ : α
β : Type u_3
f : α → β
hf : InjOn f M.E
Xs : ι → Set β
B : Set α
hB : M.Base B
Is Ys : ι → Set α
hYs : ∀ (i : ι), M.Basis (Is i) (Ys i) ∧ Xs i ∩ f '' B = f '' Is i ∧ Xs i = f '' Ys i
i : ι
⊢ Ys i ⊆ M.E

case h.e'_3.ht
ι : 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✝ : α
β : Type u_3
f : α → β
hf : InjOn f M.E
Xs : ι → Set β
B : Set α
hB : M.Base B
Is Ys : ι → Set α
hYs : ∀ (i : ι), M.Basis (Is i) (Ys i) ∧ Xs i ∩ f '' B = f '' Is i ∧ Xs i = f '' Ys i
i : ι
⊢ B ⊆ M.E
Theorem: Matroid.modularFamily_map_iff
Proof state before:
case h.e'_3.ht
ι : 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✝ : α
β : Type u_3
f : α → β
hf : InjOn f M.E
Xs : ι → Set β
B : Set α
hB : M.Base B
Is Ys : ι → Set α
hYs : ∀ (i : ι), M.Basis (Is i) (Ys i) ∧ Xs i ∩ f '' B = f '' Is i ∧ Xs i = f '' Ys i
i : ι
⊢ B ⊆ M.E
Tactic:
exact hB.subset_ground
Proof state after:
no goals
Theorem: Matroid.modularFamily_map_iff
Proof state before:
case h.e'_3.hs
ι : 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✝ : α
β : Type u_3
f : α → β
hf : InjOn f M.E
Xs : ι → Set β
B : Set α
hB : M.Base B
Is Ys : ι → Set α
hYs : ∀ (i : ι), M.Basis (Is i) (Ys i) ∧ Xs i ∩ f '' B = f '' Is i ∧ Xs i = f '' Ys i
i : ι
⊢ Ys i ⊆ M.E
Tactic:
exact (hYs i).1.subset_ground
Proof state after:
no goals
Theorem: Matroid.ModularFamily.mapEmbedding
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✝ : α
β : Type u_3
f : α ↪ β
h : M.ModularFamily Xs
⊢ (M.mapEmbedding f).ModularFamily fun i => ⇑f '' Xs i
Tactic:
obtain ⟨B, hB, hBX⟩ := h
Proof state after:
case 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✝ : α
β : Type u_3
f : α ↪ β
B : Set α
hB : M.Base B
hBX : ∀ (i : ι), M.Basis (Xs i ∩ B) (Xs i)
⊢ (M.mapEmbedding f).ModularFamily fun i => ⇑f '' Xs i
Theorem: Matroid.ModularFamily.mapEmbedding
Proof state before:
case 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✝ : α
β : Type u_3
f : α ↪ β
B : Set α
hB : M.Base B
hBX : ∀ (i : ι), M.Basis (Xs i ∩ B) (Xs i)
⊢ (M.mapEmbedding f).ModularFamily fun i => ⇑f '' Xs i
Tactic:
refine ⟨f '' B, hB.mapEmbedding f, fun i ↦ ?_⟩
Proof state after:
case 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✝ : α
β : Type u_3
f : α ↪ β
B : Set α
hB : M.Base B
hBX : ∀ (i : ι), M.Basis (Xs i ∩ B) (Xs i)
i : ι
⊢ (M.mapEmbedding f).Basis ((fun i => ⇑f '' Xs i) i ∩ ⇑f '' B) ((fun i => ⇑f '' Xs i) i)
Theorem: Matroid.ModularFamily.mapEmbedding
Proof state before:
case 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✝ : α
β : Type u_3
f : α ↪ β
B : Set α
hB : M.Base B
hBX : ∀ (i : ι), M.Basis (Xs i ∩ B) (Xs i)
i : ι
⊢ (M.mapEmbedding f).Basis ((fun i => ⇑f '' Xs i) i ∩ ⇑f '' B) ((fun i => ⇑f '' Xs i) i)
Tactic:
convert (hBX i).mapEmbedding f
Proof state after:
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✝ : α
β : Type u_3
f : α ↪ β
B : Set α
hB : M.Base B
hBX : ∀ (i : ι), M.Basis (Xs i ∩ B) (Xs i)
i : ι
⊢ (fun i => ⇑f '' Xs i) i ∩ ⇑f '' B = ⇑f '' (Xs i ∩ B)
Theorem: Matroid.ModularFamily.mapEmbedding
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✝ : α
β : Type u_3
f : α ↪ β
B : Set α
hB : M.Base B
hBX : ∀ (i : ι), M.Basis (Xs i ∩ B) (Xs i)
i : ι
⊢ (fun i => ⇑f '' Xs i) i ∩ ⇑f '' B = ⇑f '' (Xs i ∩ B)
Tactic:
rw [image_inter f.injective]
Proof state after:
no goals
Theorem: Matroid.ModularPair.symm
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.ModularPair Y X
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 : α
B : Set α
hB : M.ModularBase B fun i => bif i then X else Y
⊢ M.ModularPair Y X
Theorem: Matroid.ModularPair.symm
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 : α
B : Set α
hB : M.ModularBase B fun i => bif i then X else Y
⊢ M.ModularPair Y X
Tactic:
exact ⟨B, hB.base, fun i ↦ by simpa using hB.2 !i⟩
Proof state after:
no goals
Theorem: Matroid.ModularPair.symm
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 : α
B : Set α
hB : M.ModularBase B fun i => bif i then X else Y
i : Bool
⊢ M.Basis ((fun i => bif i then Y else X) i ∩ B) ((fun i => bif i then Y else X) i)
Tactic:
simpa using hB.2 !i
Proof state after:
no goals
Theorem: Matroid.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 : α
M : Matroid α
X Y : Set α
⊢ M.ModularPair X Y ↔ ∃ I, M.Indep I ∧ M.Basis (X ∩ I) X ∧ M.Basis (Y ∩ I) Y
Tactic:
simp only [ModularPair, ModularFamily, mem_singleton_iff, modularBase_pair_iff, indep_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 : α
M : Matroid α
X Y : Set α
⊢ (∃ B, M.ModularBase B fun i => bif i then X else Y) ↔
    ∃ I, (∃ B, M.Base B ∧ I ⊆ B) ∧ M.Basis (X ∩ I) X ∧ M.Basis (Y ∩ I) Y
Theorem: Matroid.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 : α
M : Matroid α
X Y : Set α
⊢ (∃ B, M.ModularBase B fun i => bif i then X else Y) ↔
    ∃ I, (∃ B, M.Base B ∧ I ⊆ B) ∧ M.Basis (X ∩ I) X ∧ M.Basis (Y ∩ I) Y
Tactic:
refine ⟨fun ⟨B, hB, hB'⟩ ↦ ⟨B, indep_iff.1 hB.indep, ?_⟩,
  fun ⟨I, ⟨B, hB, hIB⟩, hIX, hIY⟩ ↦ ⟨B, hB, ?_⟩ ⟩
Proof state after:
case refine_1
ι : 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 : α
M : Matroid α
X Y : Set α
x✝ : ∃ B, M.ModularBase B fun i => bif i then X else Y
B : Set α
hB : M.Base B
hB' : ∀ (i : Bool), M.Basis ((fun i => bif i then X else Y) i ∩ B) ((fun i => bif i then X else Y) i)
⊢ M.Basis (X ∩ B) X ∧ M.Basis (Y ∩ B) Y

case refine_2
ι : 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 : α
M : Matroid α
X Y : Set α
x✝ : ∃ I, (∃ B, M.Base B ∧ I ⊆ B) ∧ M.Basis (X ∩ I) X ∧ M.Basis (Y ∩ I) Y
I B : Set α
hB : M.Base B
hIB : I ⊆ B
hIX : M.Basis (X ∩ I) X
hIY : M.Basis (Y ∩ I) Y
⊢ ∀ (i : Bool), M.Basis ((fun i => bif i then X else Y) i ∩ B) ((fun i => bif i then X else Y) i)
Theorem: Matroid.modularPair_iff
Proof state before:
case refine_2
ι : 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 : α
M : Matroid α
X Y : Set α
x✝ : ∃ I, (∃ B, M.Base B ∧ I ⊆ B) ∧ M.Basis (X ∩ I) X ∧ M.Basis (Y ∩ I) Y
I B : Set α
hB : M.Base B
hIB : I ⊆ B
hIX : M.Basis (X ∩ I) X
hIY : M.Basis (Y ∩ I) Y
⊢ ∀ (i : Bool), M.Basis ((fun i => bif i then X else Y) i ∩ B) ((fun i => bif i then X else Y) i)
Tactic:
simp only [Bool.forall_bool, cond_false, cond_true]
Proof state after:
case refine_2
ι : 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 : α
M : Matroid α
X Y : Set α
x✝ : ∃ I, (∃ B, M.Base B ∧ I ⊆ B) ∧ M.Basis (X ∩ I) X ∧ M.Basis (Y ∩ I) Y
I B : Set α
hB : M.Base B
hIB : I ⊆ B
hIX : M.Basis (X ∩ I) X
hIY : M.Basis (Y ∩ I) Y
⊢ M.Basis (Y ∩ B) Y ∧ M.Basis (X ∩ B) X
Theorem: Matroid.modularPair_iff
Proof state before:
case refine_2
ι : 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 : α
M : Matroid α
X Y : Set α
x✝ : ∃ I, (∃ B, M.Base B ∧ I ⊆ B) ∧ M.Basis (X ∩ I) X ∧ M.Basis (Y ∩ I) Y
I B : Set α
hB : M.Base B
hIB : I ⊆ B
hIX : M.Basis (X ∩ I) X
hIY : M.Basis (Y ∩ I) Y
⊢ M.Basis (Y ∩ B) Y ∧ M.Basis (X ∩ B) X
Tactic:
rw [← hIX.eq_of_subset_indep (hB.indep.inter_left X) (inter_subset_inter_right _ hIB)
  inter_subset_left, ← hIY.eq_of_subset_indep (hB.indep.inter_left Y)
  (inter_subset_inter_right _ hIB) inter_subset_left]
Proof state after:
case refine_2
ι : 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 : α
M : Matroid α
X Y : Set α
x✝ : ∃ I, (∃ B, M.Base B ∧ I ⊆ B) ∧ M.Basis (X ∩ I) X ∧ M.Basis (Y ∩ I) Y
I B : Set α
hB : M.Base B
hIB : I ⊆ B
hIX : M.Basis (X ∩ I) X
hIY : M.Basis (Y ∩ I) Y
⊢ M.Basis (Y ∩ I) Y ∧ M.Basis (X ∩ I) X
Theorem: Matroid.modularPair_iff
Proof state before:
case refine_2
ι : 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 : α
M : Matroid α
X Y : Set α
x✝ : ∃ I, (∃ B, M.Base B ∧ I ⊆ B) ∧ M.Basis (X ∩ I) X ∧ M.Basis (Y ∩ I) Y
I B : Set α
hB : M.Base B
hIB : I ⊆ B
hIX : M.Basis (X ∩ I) X
hIY : M.Basis (Y ∩ I) Y
⊢ M.Basis (Y ∩ I) Y ∧ M.Basis (X ∩ I) X
Tactic:
exact ⟨hIY,hIX⟩
Proof state after:
no goals
Theorem: Matroid.modularPair_iff
Proof state before:
case refine_1
ι : 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 : α
M : Matroid α
X Y : Set α
x✝ : ∃ B, M.ModularBase B fun i => bif i then X else Y
B : Set α
hB : M.Base B
hB' : ∀ (i : Bool), M.Basis ((fun i => bif i then X else Y) i ∩ B) ((fun i => bif i then X else Y) i)
⊢ M.Basis (X ∩ B) X ∧ M.Basis (Y ∩ B) Y
Tactic:
exact ⟨by simpa using hB' true, by simpa using hB' false⟩
Proof state after:
no goals
Theorem: Matroid.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 : α
M : Matroid α
X Y : Set α
x✝ : ∃ B, M.ModularBase B fun i => bif i then X else Y
B : Set α
hB : M.Base B
hB' : ∀ (i : Bool), M.Basis ((fun i => bif i then X else Y) i ∩ B) ((fun i => bif i then X else Y) i)
⊢ M.Basis (X ∩ B) X
Tactic:
simpa using hB' true
Proof state after:
no goals
Theorem: Matroid.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 : α
M : Matroid α
X Y : Set α
x✝ : ∃ B, M.ModularBase B fun i => bif i then X else Y
B : Set α
hB : M.Base B
hB' : ∀ (i : Bool), M.Basis ((fun i => bif i then X else Y) i ∩ B) ((fun i => bif i then X else Y) i)
⊢ M.Basis (Y ∩ B) Y
Tactic:
simpa using hB' false
Proof state after:
no goals
Theorem: Matroid.ModularFamily.modularPair
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
i j : ι
⊢ M.ModularPair (Xs i) (Xs j)
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 : α
i j : ι
B : Set α
hB : M.ModularBase B Xs
⊢ M.ModularPair (Xs i) (Xs j)
Theorem: Matroid.ModularFamily.modularPair
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 : α
i j : ι
B : Set α
hB : M.ModularBase B Xs
⊢ M.ModularPair (Xs i) (Xs j)
Tactic:
exact modularPair_iff.2 ⟨B, hB.indep, hB.basis_inter i, hB.basis_inter j⟩
Proof state after:
no goals
Theorem: Matroid.modularPair_iff_exists_subsets_cl_inter
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 : α
⊢ M.ModularPair X Y ↔ ∃ I, M.Indep I ∧ X ⊆ M.cl (X ∩ I) ∧ Y ⊆ M.cl (Y ∩ 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 : α
⊢ (∃ I, M.Indep I ∧ M.Basis (X ∩ I) X ∧ M.Basis (Y ∩ I) Y) ↔ ∃ I, M.Indep I ∧ X ⊆ M.cl (X ∩ I) ∧ Y ⊆ M.cl (Y ∩ I)
Theorem: Matroid.modularPair_iff_exists_subsets_cl_inter
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 : α
⊢ (∃ I, M.Indep I ∧ M.Basis (X ∩ I) X ∧ M.Basis (Y ∩ I) Y) ↔ ∃ I, M.Indep I ∧ X ⊆ M.cl (X ∩ I) ∧ Y ⊆ M.cl (Y ∩ I)
Tactic:
refine ⟨fun ⟨I,hI,h⟩ ↦ ⟨I,hI,?_⟩, fun ⟨I,hI,h⟩ ↦ ⟨I,hI,?_⟩⟩
Proof state after:
case refine_1
ι : 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 : α
x✝ : ∃ I, M.Indep I ∧ M.Basis (X ∩ I) X ∧ M.Basis (Y ∩ I) Y
I : Set α
hI : M.Indep I
h : M.Basis (X ∩ I) X ∧ M.Basis (Y ∩ I) Y
⊢ X ⊆ M.cl (X ∩ I) ∧ Y ⊆ M.cl (Y ∩ I)

case refine_2
ι : 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 : α
x✝ : ∃ I, M.Indep I ∧ X ⊆ M.cl (X ∩ I) ∧ Y ⊆ M.cl (Y ∩ I)
I : Set α
hI : M.Indep I
h : X ⊆ M.cl (X ∩ I) ∧ Y ⊆ M.cl (Y ∩ I)
⊢ M.Basis (X ∩ I) X ∧ M.Basis (Y ∩ I) Y
Theorem: Matroid.modularPair_iff_exists_subsets_cl_inter
Proof state before:
case refine_2
ι : 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 : α
x✝ : ∃ I, M.Indep I ∧ X ⊆ M.cl (X ∩ I) ∧ Y ⊆ M.cl (Y ∩ I)
I : Set α
hI : M.Indep I
h : X ⊆ M.cl (X ∩ I) ∧ Y ⊆ M.cl (Y ∩ I)
⊢ M.Basis (X ∩ I) X ∧ M.Basis (Y ∩ I) Y
Tactic:
rwa [hI.inter_basis_cl_iff_subset_cl_inter, hI.inter_basis_cl_iff_subset_cl_inter]
Proof state after:
no goals
Theorem: Matroid.modularPair_iff_exists_subsets_cl_inter
Proof state before:
case refine_1
ι : 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 : α
x✝ : ∃ I, M.Indep I ∧ M.Basis (X ∩ I) X ∧ M.Basis (Y ∩ I) Y
I : Set α
hI : M.Indep I
h : M.Basis (X ∩ I) X ∧ M.Basis (Y ∩ I) Y
⊢ X ⊆ M.cl (X ∩ I) ∧ Y ⊆ M.cl (Y ∩ I)
Tactic:
rwa [← hI.inter_basis_cl_iff_subset_cl_inter, ← hI.inter_basis_cl_iff_subset_cl_inter]
Proof state after:
no goals
Theorem: Matroid.modularPair_iff_exists_basis_basis
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 : α
⊢ M.ModularPair X Y ↔ ∃ I J, M.Basis I X ∧ M.Basis J Y ∧ M.Indep (I ∪ J)
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 : α
⊢ (∃ I, M.Indep I ∧ M.Basis (X ∩ I) X ∧ M.Basis (Y ∩ I) Y) ↔ ∃ I J, M.Basis I X ∧ M.Basis J Y ∧ M.Indep (I ∪ J)
Theorem: Matroid.modularPair_iff_exists_basis_basis
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 : α
⊢ (∃ I, M.Indep I ∧ M.Basis (X ∩ I) X ∧ M.Basis (Y ∩ I) Y) ↔ ∃ I J, M.Basis I X ∧ M.Basis J Y ∧ M.Indep (I ∪ J)
Tactic:
refine ⟨fun ⟨I,hI,hIX,hIY⟩ ↦ ⟨_, _, hIX, hIY, hI.subset (by simp)⟩,
  fun ⟨I,J,hI,hJ,hi⟩ ↦ ⟨_,hi, ?_⟩⟩
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 : α
x✝ : ∃ I J, M.Basis I X ∧ M.Basis J Y ∧ M.Indep (I ∪ J)
I J : Set α
hI : M.Basis I X
hJ : M.Basis J Y
hi : M.Indep (I ∪ J)
⊢ M.Basis (X ∩ (I ∪ J)) X ∧ M.Basis (Y ∩ (I ∪ J)) Y
Theorem: Matroid.modularPair_iff_exists_basis_basis
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 : α
x✝ : ∃ I J, M.Basis I X ∧ M.Basis J Y ∧ M.Indep (I ∪ J)
I J : Set α
hI : M.Basis I X
hJ : M.Basis J Y
hi : M.Indep (I ∪ J)
⊢ M.Basis (X ∩ (I ∪ J)) X ∧ M.Basis (Y ∩ (I ∪ J)) Y
Tactic:
simp_rw [hi.inter_basis_cl_iff_subset_cl_inter]
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 : α
x✝ : ∃ I J, M.Basis I X ∧ M.Basis J Y ∧ M.Indep (I ∪ J)
I J : Set α
hI : M.Basis I X
hJ : M.Basis J Y
hi : M.Indep (I ∪ J)
⊢ X ⊆ M.cl (X ∩ (I ∪ J)) ∧ Y ⊆ M.cl (Y ∩ (I ∪ J))
Theorem: Matroid.modularPair_iff_exists_basis_basis
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 : α
x✝ : ∃ I J, M.Basis I X ∧ M.Basis J Y ∧ M.Indep (I ∪ J)
I J : Set α
hI : M.Basis I X
hJ : M.Basis J Y
hi : M.Indep (I ∪ J)
⊢ X ⊆ M.cl (X ∩ (I ∪ J)) ∧ Y ⊆ M.cl (Y ∩ (I ∪ J))
Tactic:
use hI.subset_cl.trans (M.cl_subset_cl (subset_inter hI.subset subset_union_left))
Proof state after:
case right
ι : 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 : α
x✝ : ∃ I J, M.Basis I X ∧ M.Basis J Y ∧ M.Indep (I ∪ J)
I J : Set α
hI : M.Basis I X
hJ : M.Basis J Y
hi : M.Indep (I ∪ J)
⊢ Y ⊆ M.cl (Y ∩ (I ∪ J))
Theorem: Matroid.modularPair_iff_exists_basis_basis
Proof state before:
case right
ι : 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 : α
x✝ : ∃ I J, M.Basis I X ∧ M.Basis J Y ∧ M.Indep (I ∪ J)
I J : Set α
hI : M.Basis I X
hJ : M.Basis J Y
hi : M.Indep (I ∪ J)
⊢ Y ⊆ M.cl (Y ∩ (I ∪ J))
Tactic:
exact hJ.subset_cl.trans (M.cl_subset_cl (subset_inter hJ.subset subset_union_right))
Proof state after:
no goals
Theorem: Matroid.modularPair_iff_exists_basis_basis
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 : α
x✝ : ∃ I, M.Indep I ∧ M.Basis (X ∩ I) X ∧ M.Basis (Y ∩ I) Y
I : Set α
hI : M.Indep I
hIX : M.Basis (X ∩ I) X
hIY : M.Basis (Y ∩ I) Y
⊢ X ∩ I ∪ Y ∩ I ⊆ I
Tactic:
simp
Proof state after:
no goals
Theorem: Matroid.ModularPair.exists_common_basis
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
⊢ ∃ I, M.Basis I (X ∪ Y) ∧ M.Basis (I ∩ X) X ∧ M.Basis (I ∩ Y) Y ∧ M.Basis (I ∩ X ∩ Y) (X ∩ Y)
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 : α
B : Set α
hB : M.ModularBase B fun i => bif i then X else Y
⊢ ∃ I, M.Basis I (X ∪ Y) ∧ M.Basis (I ∩ X) X ∧ M.Basis (I ∩ Y) Y ∧ M.Basis (I ∩ X ∩ Y) (X ∩ Y)
Theorem: Matroid.ModularPair.exists_common_basis
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 : α
B : Set α
hB : M.ModularBase B fun i => bif i then X else Y
⊢ ∃ I, M.Basis I (X ∪ Y) ∧ M.Basis (I ∩ X) X ∧ M.Basis (I ∩ Y) Y ∧ M.Basis (I ∩ X ∩ Y) (X ∩ Y)
Tactic:
refine ⟨(X ∪ Y) ∩ B, ?_⟩
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 : α
B : Set α
hB : M.ModularBase B fun i => bif i then X else Y
⊢ M.Basis ((X ∪ Y) ∩ B) (X ∪ Y) ∧
    M.Basis ((X ∪ Y) ∩ B ∩ X) X ∧ M.Basis ((X ∪ Y) ∩ B ∩ Y) Y ∧ M.Basis ((X ∪ Y) ∩ B ∩ X ∩ Y) (X ∩ Y)
Theorem: Matroid.ModularPair.exists_common_basis
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 : α
B : Set α
hB : M.ModularBase B fun i => bif i then X else Y
⊢ M.Basis ((X ∪ Y) ∩ B) (X ∪ Y) ∧
    M.Basis ((X ∪ Y) ∩ B ∩ X) X ∧ M.Basis ((X ∪ Y) ∩ B ∩ Y) Y ∧ M.Basis ((X ∪ Y) ∩ B ∩ X ∩ Y) (X ∩ Y)
Tactic:
rw [inter_right_comm, inter_eq_self_of_subset_right subset_union_left,
  inter_right_comm, inter_eq_self_of_subset_right subset_union_right, inter_right_comm]
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 : α
B : Set α
hB : M.ModularBase B fun i => bif i then X else Y
⊢ M.Basis ((X ∪ Y) ∩ B) (X ∪ Y) ∧ M.Basis (X ∩ B) X ∧ M.Basis (Y ∩ B) Y ∧ M.Basis (X ∩ Y ∩ B) (X ∩ Y)
Theorem: Matroid.ModularPair.exists_common_basis
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 : α
B : Set α
hB : M.ModularBase B fun i => bif i then X else Y
⊢ M.Basis ((X ∪ Y) ∩ B) (X ∪ Y) ∧ M.Basis (X ∩ B) X ∧ M.Basis (Y ∩ B) Y ∧ M.Basis (X ∩ Y ∩ B) (X ∩ Y)
Tactic:
refine ⟨?_, by simpa using hB.basis_inter true, by simpa using hB.basis_inter false, ?_⟩
Proof state after:
case intro.refine_1
ι : 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 : α
B : Set α
hB : M.ModularBase B fun i => bif i then X else Y
⊢ M.Basis ((X ∪ Y) ∩ B) (X ∪ Y)

case intro.refine_2
ι : 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 : α
B : Set α
hB : M.ModularBase B fun i => bif i then X else Y
⊢ M.Basis (X ∩ Y ∩ B) (X ∩ Y)
Theorem: Matroid.ModularPair.exists_common_basis
Proof state before:
case intro.refine_2
ι : 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 : α
B : Set α
hB : M.ModularBase B fun i => bif i then X else Y
⊢ M.Basis (X ∩ Y ∩ B) (X ∩ Y)
Tactic:
have hi := hB.basis_iInter
Proof state after:
case intro.refine_2
ι : 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 : α
B : Set α
hB : M.ModularBase B fun i => bif i then X else Y
hi : M.Basis ((⋂ i, bif i then X else Y) ∩ B) (⋂ i, bif i then X else Y)
⊢ M.Basis (X ∩ Y ∩ B) (X ∩ Y)
Theorem: Matroid.ModularPair.exists_common_basis
Proof state before:
case intro.refine_2
ι : 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 : α
B : Set α
hB : M.ModularBase B fun i => bif i then X else Y
hi : M.Basis ((⋂ i, bif i then X else Y) ∩ B) (⋂ i, bif i then X else Y)
⊢ M.Basis (X ∩ Y ∩ B) (X ∩ Y)
Tactic:
rwa [← inter_eq_iInter] at hi
Proof state after:
no goals
Theorem: Matroid.ModularPair.exists_common_basis
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 : α
B : Set α
hB : M.ModularBase B fun i => bif i then X else Y
⊢ M.Basis (X ∩ B) X
Tactic:
simpa using hB.basis_inter true
Proof state after:
no goals
Theorem: Matroid.ModularPair.exists_common_basis
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 : α
B : Set α
hB : M.ModularBase B fun i => bif i then X else Y
⊢ M.Basis (Y ∩ B) Y
Tactic:
simpa using hB.basis_inter false
Proof state after:
no goals
Theorem: Matroid.ModularPair.exists_common_basis
Proof state before:
case intro.refine_1
ι : 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 : α
B : Set α
hB : M.ModularBase B fun i => bif i then X else Y
⊢ M.Basis ((X ∪ Y) ∩ B) (X ∪ Y)
Tactic:
have hu := hB.basis_iUnion
Proof state after:
case intro.refine_1
ι : 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 : α
B : Set α
hB : M.ModularBase B fun i => bif i then X else Y
hu : M.Basis ((⋃ i, bif i then X else Y) ∩ B) (⋃ i, bif i then X else Y)
⊢ M.Basis ((X ∪ Y) ∩ B) (X ∪ Y)
Theorem: Matroid.ModularPair.exists_common_basis
Proof state before:
case intro.refine_1
ι : 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 : α
B : Set α
hB : M.ModularBase B fun i => bif i then X else Y
hu : M.Basis ((⋃ i, bif i then X else Y) ∩ B) (⋃ i, bif i then X else Y)
⊢ M.Basis ((X ∪ Y) ∩ B) (X ∪ Y)
Tactic:
rwa [← union_eq_iUnion] at hu
Proof state after:
no goals