internlm/Lean-Github huggingface dataset:
Theorem: Matroid.ModularFamily.modularPair_compl_biInter
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 ι
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)
Tactic:
exact ⟨B, hB.indep, hB.basis_biInter hA, hB.basis_biInter (by rwa [nonempty_compl])⟩
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 : α
A : Set ι
hA : A.Nonempty
hA' : A ≠ univ
B : Set α
hB : M.ModularBase B Xs
⊢ Aᶜ.Nonempty
Tactic:
rwa [nonempty_compl]
Proof state after:
no goals
Theorem: Matroid.ModularFamily.modularPair_singleton_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
i₀ : ι
⊢ M.ModularPair (Xs i₀) (⋃ i ∈ {i₀}ᶜ, Xs i)
Tactic:
convert h.modularPair_compl_biUnion {i₀}
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 : α
h : M.ModularFamily Xs
i₀ : ι
⊢ Xs i₀ = ⋃ i ∈ {i₀}, Xs i
Theorem: Matroid.ModularFamily.modularPair_singleton_compl_biUnion
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.ModularFamily Xs
i₀ : ι
⊢ Xs i₀ = ⋃ i ∈ {i₀}, Xs i
Tactic:
simp
Proof state after:
no goals
Theorem: Matroid.ModularFamily.modularPair_singleton_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 : α
inst✝ : Nontrivial ι
h : M.ModularFamily Xs
i₀ : ι
⊢ M.ModularPair (Xs i₀) (⋂ i ∈ {i₀}ᶜ, Xs i)
Tactic:
convert h.modularPair_compl_biInter {i₀} (by simp)
  (by simpa [ne_univ_iff_exists_not_mem, mem_singleton_iff] using exists_ne i₀)
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 : α
inst✝ : Nontrivial ι
h : M.ModularFamily Xs
i₀ : ι
⊢ Xs i₀ = ⋂ i ∈ {i₀}, Xs i
Theorem: Matroid.ModularFamily.modularPair_singleton_compl_biInter
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 : α
inst✝ : Nontrivial ι
h : M.ModularFamily Xs
i₀ : ι
⊢ Xs i₀ = ⋂ i ∈ {i₀}, Xs i
Tactic:
simp
Proof state after:
no goals
Theorem: Matroid.ModularFamily.modularPair_singleton_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 : α
inst✝ : Nontrivial ι
h : M.ModularFamily Xs
i₀ : ι
⊢ {i₀}.Nonempty
Tactic:
simp
Proof state after:
no goals
Theorem: Matroid.ModularFamily.modularPair_singleton_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 : α
inst✝ : Nontrivial ι
h : M.ModularFamily Xs
i₀ : ι
⊢ {i₀} ≠ univ
Tactic:
simpa [ne_univ_iff_exists_not_mem, mem_singleton_iff] using exists_ne i₀
Proof state after:
no goals
Theorem: Matroid.modularPair_insert_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✝ : α
M : Matroid α
X : Set α
e f : α
⊢ M.ModularPair (M.cl (insert e X)) (M.cl (insert f 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✝ : α
M : Matroid α
X : Set α
e f : α
I : Set α
hI : M.Basis' I X
⊢ M.ModularPair (M.cl (insert e X)) (M.cl (insert f X))
Theorem: Matroid.modularPair_insert_cl
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✝ : α
M : Matroid α
X : Set α
e f : α
I : Set α
hI : M.Basis' I X
⊢ M.ModularPair (M.cl (insert e X)) (M.cl (insert f X))
Tactic:
rw [← cl_insert_cl_eq_cl_insert, ← cl_insert_cl_eq_cl_insert (e := f), ← hI.cl_eq_cl]
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✝ : α
M : Matroid α
X : Set α
e f : α
I : Set α
hI : M.Basis' I X
⊢ M.ModularPair (M.cl (insert e (M.cl I))) (M.cl (insert f (M.cl I)))
Theorem: Matroid.modularPair_insert_cl
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✝ : α
M : Matroid α
X : Set α
e f : α
I : Set α
hI : M.Basis' I X
⊢ M.ModularPair (M.cl (insert e (M.cl I))) (M.cl (insert f (M.cl I)))
Tactic:
obtain (he | he) := em' (e ∈ M.E)
Proof state after:
case intro.inl
ι : 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 : Set α
e f : α
I : Set α
hI : M.Basis' I X
he : e ∉ M.E
⊢ M.ModularPair (M.cl (insert e (M.cl I))) (M.cl (insert f (M.cl I)))

case intro.inr
ι : 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 : Set α
e f : α
I : Set α
hI : M.Basis' I X
he : e ∈ M.E
⊢ M.ModularPair (M.cl (insert e (M.cl I))) (M.cl (insert f (M.cl I)))
Theorem: Matroid.modularPair_insert_cl
Proof state before:
case intro.inr
ι : 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 : Set α
e f : α
I : Set α
hI : M.Basis' I X
he : e ∈ M.E
⊢ M.ModularPair (M.cl (insert e (M.cl I))) (M.cl (insert f (M.cl I)))
Tactic:
obtain (hf | hf) := em' (f ∈ M.E)
Proof state after:
case intro.inr.inl
ι : 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 : Set α
e f : α
I : Set α
hI : M.Basis' I X
he : e ∈ M.E
hf : f ∉ M.E
⊢ M.ModularPair (M.cl (insert e (M.cl I))) (M.cl (insert f (M.cl I)))

case intro.inr.inr
ι : 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 : Set α
e f : α
I : Set α
hI : M.Basis' I X
he : e ∈ M.E
hf : f ∈ M.E
⊢ M.ModularPair (M.cl (insert e (M.cl I))) (M.cl (insert f (M.cl I)))
Theorem: Matroid.modularPair_insert_cl
Proof state before:
case intro.inr.inr
ι : 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 : Set α
e f : α
I : Set α
hI : M.Basis' I X
he : e ∈ M.E
hf : f ∈ M.E
⊢ M.ModularPair (M.cl (insert e (M.cl I))) (M.cl (insert f (M.cl I)))
Tactic:
obtain (hfI | hfI) := em (f ∈ M.cl I)
Proof state after:
case intro.inr.inr.inl
ι : 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 : Set α
e f : α
I : Set α
hI : M.Basis' I X
he : e ∈ M.E
hf : f ∈ M.E
hfI : f ∈ M.cl I
⊢ M.ModularPair (M.cl (insert e (M.cl I))) (M.cl (insert f (M.cl I)))

case intro.inr.inr.inr
ι : 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 : Set α
e f : α
I : Set α
hI : M.Basis' I X
he : e ∈ M.E
hf : f ∈ M.E
hfI : f ∉ M.cl I
⊢ M.ModularPair (M.cl (insert e (M.cl I))) (M.cl (insert f (M.cl I)))
Theorem: Matroid.modularPair_insert_cl
Proof state before:
case intro.inr.inr.inr
ι : 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 : Set α
e f : α
I : Set α
hI : M.Basis' I X
he : e ∈ M.E
hf : f ∈ M.E
hfI : f ∉ M.cl I
⊢ M.ModularPair (M.cl (insert e (M.cl I))) (M.cl (insert f (M.cl I)))
Tactic:
rw [cl_insert_cl_eq_cl_insert, cl_insert_cl_eq_cl_insert]
Proof state after:
case intro.inr.inr.inr
ι : 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 : Set α
e f : α
I : Set α
hI : M.Basis' I X
he : e ∈ M.E
hf : f ∈ M.E
hfI : f ∉ M.cl I
⊢ M.ModularPair (M.cl (insert e I)) (M.cl (insert f I))
Theorem: Matroid.modularPair_insert_cl
Proof state before:
case intro.inr.inr.inr
ι : 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 : Set α
e f : α
I : Set α
hI : M.Basis' I X
he : e ∈ M.E
hf : f ∈ M.E
hfI : f ∉ M.cl I
⊢ M.ModularPair (M.cl (insert e I)) (M.cl (insert f I))
Tactic:
obtain (hef | hef) := em (e ∈ M.cl (insert f I))
Proof state after:
case intro.inr.inr.inr.inl
ι : 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 : Set α
e f : α
I : Set α
hI : M.Basis' I X
he : e ∈ M.E
hf : f ∈ M.E
hfI : f ∉ M.cl I
hef : e ∈ M.cl (insert f I)
⊢ M.ModularPair (M.cl (insert e I)) (M.cl (insert f I))

case intro.inr.inr.inr.inr
ι : 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 : Set α
e f : α
I : Set α
hI : M.Basis' I X
he : e ∈ M.E
hf : f ∈ M.E
hfI : f ∉ M.cl I
hef : e ∉ M.cl (insert f I)
⊢ M.ModularPair (M.cl (insert e I)) (M.cl (insert f I))
Theorem: Matroid.modularPair_insert_cl
Proof state before:
case intro.inr.inr.inr.inr
ι : 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 : Set α
e f : α
I : Set α
hI : M.Basis' I X
he : e ∈ M.E
hf : f ∈ M.E
hfI : f ∉ M.cl I
hef : e ∉ M.cl (insert f I)
⊢ M.ModularPair (M.cl (insert e I)) (M.cl (insert f I))
Tactic:
refine ModularPair.cl_cl ?_
Proof state after:
case intro.inr.inr.inr.inr
ι : 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 : Set α
e f : α
I : Set α
hI : M.Basis' I X
he : e ∈ M.E
hf : f ∈ M.E
hfI : f ∉ M.cl I
hef : e ∉ M.cl (insert f I)
⊢ M.ModularPair (insert e I) (insert f I)
Theorem: Matroid.modularPair_insert_cl
Proof state before:
case intro.inr.inr.inr.inr
ι : 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 : Set α
e f : α
I : Set α
hI : M.Basis' I X
he : e ∈ M.E
hf : f ∈ M.E
hfI : f ∉ M.cl I
hef : e ∉ M.cl (insert f I)
⊢ M.ModularPair (insert e I) (insert f I)
Tactic:
apply Indep.modularPair_of_union
Proof state after:
case intro.inr.inr.inr.inr.hi
ι : 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 : Set α
e f : α
I : Set α
hI : M.Basis' I X
he : e ∈ M.E
hf : f ∈ M.E
hfI : f ∉ M.cl I
hef : e ∉ M.cl (insert f I)
⊢ M.Indep (insert e I ∪ insert f I)
Theorem: Matroid.modularPair_insert_cl
Proof state before:
case intro.inr.inr.inr.inr.hi
ι : 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 : Set α
e f : α
I : Set α
hI : M.Basis' I X
he : e ∈ M.E
hf : f ∈ M.E
hfI : f ∉ M.cl I
hef : e ∉ M.cl (insert f I)
⊢ M.Indep (insert e I ∪ insert f I)
Tactic:
rw [union_insert, union_eq_self_of_subset_right (subset_insert _ _), insert_comm,
  Indep.insert_indep_iff]
Proof state after:
case intro.inr.inr.inr.inr.hi
ι : 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 : Set α
e f : α
I : Set α
hI : M.Basis' I X
he : e ∈ M.E
hf : f ∈ M.E
hfI : f ∉ M.cl I
hef : e ∉ M.cl (insert f I)
⊢ e ∈ M.E \ M.cl (insert f I) ∨ e ∈ insert f I

case intro.inr.inr.inr.inr.hi
ι : 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 : Set α
e f : α
I : Set α
hI : M.Basis' I X
he : e ∈ M.E
hf : f ∈ M.E
hfI : f ∉ M.cl I
hef : e ∉ M.cl (insert f I)
⊢ M.Indep (insert f I)
Theorem: Matroid.modularPair_insert_cl
Proof state before:
case intro.inr.inr.inr.inr.hi
ι : 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 : Set α
e f : α
I : Set α
hI : M.Basis' I X
he : e ∈ M.E
hf : f ∈ M.E
hfI : f ∉ M.cl I
hef : e ∉ M.cl (insert f I)
⊢ M.Indep (insert f I)
Tactic:
rw [hI.indep.insert_indep_iff]
Proof state after:
case intro.inr.inr.inr.inr.hi
ι : 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 : Set α
e f : α
I : Set α
hI : M.Basis' I X
he : e ∈ M.E
hf : f ∈ M.E
hfI : f ∉ M.cl I
hef : e ∉ M.cl (insert f I)
⊢ f ∈ M.E \ M.cl I ∨ f ∈ I
Theorem: Matroid.modularPair_insert_cl
Proof state before:
case intro.inr.inr.inr.inr.hi
ι : 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 : Set α
e f : α
I : Set α
hI : M.Basis' I X
he : e ∈ M.E
hf : f ∈ M.E
hfI : f ∉ M.cl I
hef : e ∉ M.cl (insert f I)
⊢ f ∈ M.E \ M.cl I ∨ f ∈ I
Tactic:
exact .inl ⟨hf, hfI⟩
Proof state after:
no goals
Theorem: Matroid.modularPair_insert_cl
Proof state before:
case intro.inl
ι : 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 : Set α
e f : α
I : Set α
hI : M.Basis' I X
he : e ∉ M.E
⊢ M.ModularPair (M.cl (insert e (M.cl I))) (M.cl (insert f (M.cl I)))
Tactic:
rw [← cl_inter_ground, insert_inter_of_not_mem he, cl_inter_ground]
Proof state after:
case intro.inl
ι : 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 : Set α
e f : α
I : Set α
hI : M.Basis' I X
he : e ∉ M.E
⊢ M.ModularPair (M.cl (M.cl I)) (M.cl (insert f (M.cl I)))
Theorem: Matroid.modularPair_insert_cl
Proof state before:
case intro.inl
ι : 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 : Set α
e f : α
I : Set α
hI : M.Basis' I X
he : e ∉ M.E
⊢ M.ModularPair (M.cl (M.cl I)) (M.cl (insert f (M.cl I)))
Tactic:
exact modularPair_of_subset (M.cl_subset_cl (subset_insert _ _)) (M.cl_subset_ground _)
Proof state after:
no goals
Theorem: Matroid.modularPair_insert_cl
Proof state before:
case intro.inr.inl
ι : 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 : Set α
e f : α
I : Set α
hI : M.Basis' I X
he : e ∈ M.E
hf : f ∉ M.E
⊢ M.ModularPair (M.cl (insert e (M.cl I))) (M.cl (insert f (M.cl I)))
Tactic:
rw [ModularPair.comm, ← cl_inter_ground, insert_inter_of_not_mem hf, cl_inter_ground]
Proof state after:
case intro.inr.inl
ι : 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 : Set α
e f : α
I : Set α
hI : M.Basis' I X
he : e ∈ M.E
hf : f ∉ M.E
⊢ M.ModularPair (M.cl (M.cl I)) (M.cl (insert e (M.cl I)))
Theorem: Matroid.modularPair_insert_cl
Proof state before:
case intro.inr.inl
ι : 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 : Set α
e f : α
I : Set α
hI : M.Basis' I X
he : e ∈ M.E
hf : f ∉ M.E
⊢ M.ModularPair (M.cl (M.cl I)) (M.cl (insert e (M.cl I)))
Tactic:
exact modularPair_of_subset (M.cl_subset_cl (subset_insert _ _)) (M.cl_subset_ground _)
Proof state after:
no goals
Theorem: Matroid.modularPair_insert_cl
Proof state before:
case intro.inr.inr.inl
ι : 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 : Set α
e f : α
I : Set α
hI : M.Basis' I X
he : e ∈ M.E
hf : f ∈ M.E
hfI : f ∈ M.cl I
⊢ M.ModularPair (M.cl (insert e (M.cl I))) (M.cl (insert f (M.cl I)))
Tactic:
rw [ModularPair.comm, insert_eq_of_mem hfI]
Proof state after:
case intro.inr.inr.inl
ι : 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 : Set α
e f : α
I : Set α
hI : M.Basis' I X
he : e ∈ M.E
hf : f ∈ M.E
hfI : f ∈ M.cl I
⊢ M.ModularPair (M.cl (M.cl I)) (M.cl (insert e (M.cl I)))
Theorem: Matroid.modularPair_insert_cl
Proof state before:
case intro.inr.inr.inl
ι : 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 : Set α
e f : α
I : Set α
hI : M.Basis' I X
he : e ∈ M.E
hf : f ∈ M.E
hfI : f ∈ M.cl I
⊢ M.ModularPair (M.cl (M.cl I)) (M.cl (insert e (M.cl I)))
Tactic:
exact modularPair_of_subset (M.cl_subset_cl (subset_insert _ _)) (M.cl_subset_ground _)
Proof state after:
no goals
Theorem: Matroid.modularPair_insert_cl
Proof state before:
case intro.inr.inr.inr.inl
ι : 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 : Set α
e f : α
I : Set α
hI : M.Basis' I X
he : e ∈ M.E
hf : f ∈ M.E
hfI : f ∉ M.cl I
hef : e ∈ M.cl (insert f I)
⊢ M.ModularPair (M.cl (insert e I)) (M.cl (insert f I))
Tactic:
refine modularPair_of_subset (M.cl_subset_cl_of_subset_cl ?_) (M.cl_subset_ground _)
Proof state after:
case intro.inr.inr.inr.inl
ι : 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 : Set α
e f : α
I : Set α
hI : M.Basis' I X
he : e ∈ M.E
hf : f ∈ M.E
hfI : f ∉ M.cl I
hef : e ∈ M.cl (insert f I)
⊢ insert e I ⊆ M.cl (insert f I)
Theorem: Matroid.modularPair_insert_cl
Proof state before:
case intro.inr.inr.inr.inl
ι : 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 : Set α
e f : α
I : Set α
hI : M.Basis' I X
he : e ∈ M.E
hf : f ∈ M.E
hfI : f ∉ M.cl I
hef : e ∈ M.cl (insert f I)
⊢ insert e I ⊆ M.cl (insert f I)
Tactic:
exact insert_subset hef (M.subset_cl_of_subset (subset_insert _ _)
  (insert_subset hf hI.indep.subset_ground))
Proof state after:
no goals
Theorem: Matroid.modularPair_insert_cl
Proof state before:
case intro.inr.inr.inr.inr.hi
ι : 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 : Set α
e f : α
I : Set α
hI : M.Basis' I X
he : e ∈ M.E
hf : f ∈ M.E
hfI : f ∉ M.cl I
hef : e ∉ M.cl (insert f I)
⊢ e ∈ M.E \ M.cl (insert f I) ∨ e ∈ insert f I
Tactic:
exact .inl ⟨he, hef⟩
Proof state after:
no goals
Theorem: Matroid.modularSet_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 : Set α
⊢ M.ModularSet X ↔ ∀ ⦃F : Set α⦄, M.Flat F → ∃ I, M.Indep I ∧ M.Basis (X ∩ I) X ∧ M.Basis (F ∩ I) F
Tactic:
simp [ModularSet, modularPair_iff]
Proof state after:
no goals
Theorem: Matroid.modularSet_iff_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 : α
M : Matroid α
X : Set α
⊢ M.ModularSet X ↔ ∀ ⦃F : Set α⦄, M.Flat F → ∃ I, M.Indep I ∧ X ⊆ M.cl (X ∩ I) ∧ F ⊆ M.cl (F ∩ I)
Tactic:
rw [modularSet_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 : Set α
⊢ (∀ ⦃F : Set α⦄, M.Flat F → ∃ I, M.Indep I ∧ M.Basis (X ∩ I) X ∧ M.Basis (F ∩ I) F) ↔
    ∀ ⦃F : Set α⦄, M.Flat F → ∃ I, M.Indep I ∧ X ⊆ M.cl (X ∩ I) ∧ F ⊆ M.cl (F ∩ I)
Theorem: Matroid.modularSet_iff_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 : α
M : Matroid α
X : Set α
⊢ (∀ ⦃F : Set α⦄, M.Flat F → ∃ I, M.Indep I ∧ M.Basis (X ∩ I) X ∧ M.Basis (F ∩ I) F) ↔
    ∀ ⦃F : Set α⦄, M.Flat F → ∃ I, M.Indep I ∧ X ⊆ M.cl (X ∩ I) ∧ F ⊆ M.cl (F ∩ I)
Tactic:
refine ⟨fun h F hF ↦ ?_, fun h F hF ↦ ?_⟩
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 : Set α
h : ∀ ⦃F : Set α⦄, M.Flat F → ∃ I, M.Indep I ∧ M.Basis (X ∩ I) X ∧ M.Basis (F ∩ I) F
F : Set α
hF : M.Flat F
⊢ ∃ I, M.Indep I ∧ X ⊆ M.cl (X ∩ I) ∧ F ⊆ M.cl (F ∩ 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 : α
M : Matroid α
X : Set α
h : ∀ ⦃F : Set α⦄, M.Flat F → ∃ I, M.Indep I ∧ X ⊆ M.cl (X ∩ I) ∧ F ⊆ M.cl (F ∩ I)
F : Set α
hF : M.Flat F
⊢ ∃ I, M.Indep I ∧ M.Basis (X ∩ I) X ∧ M.Basis (F ∩ I) F
Theorem: Matroid.modularSet_iff_cl
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 : Set α
h : ∀ ⦃F : Set α⦄, M.Flat F → ∃ I, M.Indep I ∧ X ⊆ M.cl (X ∩ I) ∧ F ⊆ M.cl (F ∩ I)
F : Set α
hF : M.Flat F
⊢ ∃ I, M.Indep I ∧ M.Basis (X ∩ I) X ∧ M.Basis (F ∩ I) F
Tactic:
obtain ⟨I, hI, hI'⟩ := h hF
Proof state after:
case refine_2.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 : α
M : Matroid α
X : Set α
h : ∀ ⦃F : Set α⦄, M.Flat F → ∃ I, M.Indep I ∧ X ⊆ M.cl (X ∩ I) ∧ F ⊆ M.cl (F ∩ I)
F : Set α
hF : M.Flat F
I : Set α
hI : M.Indep I
hI' : X ⊆ M.cl (X ∩ I) ∧ F ⊆ M.cl (F ∩ I)
⊢ ∃ I, M.Indep I ∧ M.Basis (X ∩ I) X ∧ M.Basis (F ∩ I) F
Theorem: Matroid.modularSet_iff_cl
Proof state before:
case refine_2.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 : α
M : Matroid α
X : Set α
h : ∀ ⦃F : Set α⦄, M.Flat F → ∃ I, M.Indep I ∧ X ⊆ M.cl (X ∩ I) ∧ F ⊆ M.cl (F ∩ I)
F : Set α
hF : M.Flat F
I : Set α
hI : M.Indep I
hI' : X ⊆ M.cl (X ∩ I) ∧ F ⊆ M.cl (F ∩ I)
⊢ ∃ I, M.Indep I ∧ M.Basis (X ∩ I) X ∧ M.Basis (F ∩ I) F
Tactic:
refine ⟨I, hI, ?_⟩
Proof state after:
case refine_2.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 : α
M : Matroid α
X : Set α
h : ∀ ⦃F : Set α⦄, M.Flat F → ∃ I, M.Indep I ∧ X ⊆ M.cl (X ∩ I) ∧ F ⊆ M.cl (F ∩ I)
F : Set α
hF : M.Flat F
I : Set α
hI : M.Indep I
hI' : X ⊆ M.cl (X ∩ I) ∧ F ⊆ M.cl (F ∩ I)
⊢ M.Basis (X ∩ I) X ∧ M.Basis (F ∩ I) F
Theorem: Matroid.modularSet_iff_cl
Proof state before:
case refine_2.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 : α
M : Matroid α
X : Set α
h : ∀ ⦃F : Set α⦄, M.Flat F → ∃ I, M.Indep I ∧ X ⊆ M.cl (X ∩ I) ∧ F ⊆ M.cl (F ∩ I)
F : Set α
hF : M.Flat F
I : Set α
hI : M.Indep I
hI' : X ⊆ M.cl (X ∩ I) ∧ F ⊆ M.cl (F ∩ I)
⊢ M.Basis (X ∩ I) X ∧ M.Basis (F ∩ I) F
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.modularSet_iff_cl
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 : Set α
h : ∀ ⦃F : Set α⦄, M.Flat F → ∃ I, M.Indep I ∧ M.Basis (X ∩ I) X ∧ M.Basis (F ∩ I) F
F : Set α
hF : M.Flat F
⊢ ∃ I, M.Indep I ∧ X ⊆ M.cl (X ∩ I) ∧ F ⊆ M.cl (F ∩ I)
Tactic:
obtain ⟨I, hI, hI'⟩ := h hF
Proof state after:
case refine_1.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 : α
M : Matroid α
X : Set α
h : ∀ ⦃F : Set α⦄, M.Flat F → ∃ I, M.Indep I ∧ M.Basis (X ∩ I) X ∧ M.Basis (F ∩ I) F
F : Set α
hF : M.Flat F
I : Set α
hI : M.Indep I
hI' : M.Basis (X ∩ I) X ∧ M.Basis (F ∩ I) F
⊢ ∃ I, M.Indep I ∧ X ⊆ M.cl (X ∩ I) ∧ F ⊆ M.cl (F ∩ I)
Theorem: Matroid.modularSet_iff_cl
Proof state before:
case refine_1.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 : α
M : Matroid α
X : Set α
h : ∀ ⦃F : Set α⦄, M.Flat F → ∃ I, M.Indep I ∧ M.Basis (X ∩ I) X ∧ M.Basis (F ∩ I) F
F : Set α
hF : M.Flat F
I : Set α
hI : M.Indep I
hI' : M.Basis (X ∩ I) X ∧ M.Basis (F ∩ I) F
⊢ ∃ I, M.Indep I ∧ X ⊆ M.cl (X ∩ I) ∧ F ⊆ M.cl (F ∩ I)
Tactic:
refine ⟨I, hI, ?_⟩
Proof state after:
case refine_1.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 : α
M : Matroid α
X : Set α
h : ∀ ⦃F : Set α⦄, M.Flat F → ∃ I, M.Indep I ∧ M.Basis (X ∩ I) X ∧ M.Basis (F ∩ I) F
F : Set α
hF : M.Flat F
I : Set α
hI : M.Indep I
hI' : M.Basis (X ∩ I) X ∧ M.Basis (F ∩ I) F
⊢ X ⊆ M.cl (X ∩ I) ∧ F ⊆ M.cl (F ∩ I)