internlm/Lean-Github huggingface dataset:
Theorem: Matroid.Indep.cl_sInter_eq_biInter_cl_of_forall_subset
Proof state before:
case intro.intro.intro.intro.inl
α : Type u_1
ι : Type u_2
M : Matroid α
F J✝ X✝ Y B C R : Set α
e✝ f✝ x y : α
Js : Set (Set α)
hne : Js.Nonempty
hiI : M.Indep (⋂₀ Js)
e : α
he : ∀ i ∈ Js, e ∈ M.cl i
he' : M.Indep (insert e (⋂₀ Js))
J : Set α
heJ : insert e (⋂₀ Js) ⊆ J
f : α
hI : M.Indep (insert f (J \ {e}))
hIs : ∀ J_1 ∈ Js, J_1 ⊆ insert f (J \ {e})
hiX : ⋂₀ Js ⊆ insert f (J \ {e})
heEI : e ∈ M.E \ insert f (J \ {e})
hJI : M.Basis J (insert e (insert f (J \ {e})))
hIb : M.Basis (insert f (J \ {e})) (insert e (insert f (J \ {e})))
hfIJ : f ∈ insert f (J \ {e}) \ J
hfb : M.Basis (insert f (J \ {e})) (insert e (insert f (J \ {e})))
X : Set α
hX' : X ∈ Js
hfX : f ∉ X
hd : M.Dep (insert e X)
⊢ False
Tactic:
refine' (hJI.indep.subset (insert_subset (heJ (mem_insert _ _)) _)).not_dep hd
Proof state after:
case intro.intro.intro.intro.inl
α : Type u_1
ι : Type u_2
M : Matroid α
F J✝ X✝ Y B C R : Set α
e✝ f✝ x y : α
Js : Set (Set α)
hne : Js.Nonempty
hiI : M.Indep (⋂₀ Js)
e : α
he : ∀ i ∈ Js, e ∈ M.cl i
he' : M.Indep (insert e (⋂₀ Js))
J : Set α
heJ : insert e (⋂₀ Js) ⊆ J
f : α
hI : M.Indep (insert f (J \ {e}))
hIs : ∀ J_1 ∈ Js, J_1 ⊆ insert f (J \ {e})
hiX : ⋂₀ Js ⊆ insert f (J \ {e})
heEI : e ∈ M.E \ insert f (J \ {e})
hJI : M.Basis J (insert e (insert f (J \ {e})))
hIb : M.Basis (insert f (J \ {e})) (insert e (insert f (J \ {e})))
hfIJ : f ∈ insert f (J \ {e}) \ J
hfb : M.Basis (insert f (J \ {e})) (insert e (insert f (J \ {e})))
X : Set α
hX' : X ∈ Js
hfX : f ∉ X
hd : M.Dep (insert e X)
⊢ X ⊆ J
Theorem: Matroid.Indep.cl_sInter_eq_biInter_cl_of_forall_subset
Proof state before:
case intro.intro.intro.intro.inl
α : Type u_1
ι : Type u_2
M : Matroid α
F J✝ X✝ Y B C R : Set α
e✝ f✝ x y : α
Js : Set (Set α)
hne : Js.Nonempty
hiI : M.Indep (⋂₀ Js)
e : α
he : ∀ i ∈ Js, e ∈ M.cl i
he' : M.Indep (insert e (⋂₀ Js))
J : Set α
heJ : insert e (⋂₀ Js) ⊆ J
f : α
hI : M.Indep (insert f (J \ {e}))
hIs : ∀ J_1 ∈ Js, J_1 ⊆ insert f (J \ {e})
hiX : ⋂₀ Js ⊆ insert f (J \ {e})
heEI : e ∈ M.E \ insert f (J \ {e})
hJI : M.Basis J (insert e (insert f (J \ {e})))
hIb : M.Basis (insert f (J \ {e})) (insert e (insert f (J \ {e})))
hfIJ : f ∈ insert f (J \ {e}) \ J
hfb : M.Basis (insert f (J \ {e})) (insert e (insert f (J \ {e})))
X : Set α
hX' : X ∈ Js
hfX : f ∉ X
hd : M.Dep (insert e X)
⊢ X ⊆ J
Tactic:
specialize hIs _ hX'
Proof state after:
case intro.intro.intro.intro.inl
α : Type u_1
ι : Type u_2
M : Matroid α
F J✝ X✝ Y B C R : Set α
e✝ f✝ x y : α
Js : Set (Set α)
hne : Js.Nonempty
hiI : M.Indep (⋂₀ Js)
e : α
he : ∀ i ∈ Js, e ∈ M.cl i
he' : M.Indep (insert e (⋂₀ Js))
J : Set α
heJ : insert e (⋂₀ Js) ⊆ J
f : α
hI : M.Indep (insert f (J \ {e}))
hiX : ⋂₀ Js ⊆ insert f (J \ {e})
heEI : e ∈ M.E \ insert f (J \ {e})
hJI : M.Basis J (insert e (insert f (J \ {e})))
hIb : M.Basis (insert f (J \ {e})) (insert e (insert f (J \ {e})))
hfIJ : f ∈ insert f (J \ {e}) \ J
hfb : M.Basis (insert f (J \ {e})) (insert e (insert f (J \ {e})))
X : Set α
hX' : X ∈ Js
hfX : f ∉ X
hd : M.Dep (insert e X)
hIs : X ⊆ insert f (J \ {e})
⊢ X ⊆ J
Theorem: Matroid.Indep.cl_sInter_eq_biInter_cl_of_forall_subset
Proof state before:
case intro.intro.intro.intro.inl
α : Type u_1
ι : Type u_2
M : Matroid α
F J✝ X✝ Y B C R : Set α
e✝ f✝ x y : α
Js : Set (Set α)
hne : Js.Nonempty
hiI : M.Indep (⋂₀ Js)
e : α
he : ∀ i ∈ Js, e ∈ M.cl i
he' : M.Indep (insert e (⋂₀ Js))
J : Set α
heJ : insert e (⋂₀ Js) ⊆ J
f : α
hI : M.Indep (insert f (J \ {e}))
hiX : ⋂₀ Js ⊆ insert f (J \ {e})
heEI : e ∈ M.E \ insert f (J \ {e})
hJI : M.Basis J (insert e (insert f (J \ {e})))
hIb : M.Basis (insert f (J \ {e})) (insert e (insert f (J \ {e})))
hfIJ : f ∈ insert f (J \ {e}) \ J
hfb : M.Basis (insert f (J \ {e})) (insert e (insert f (J \ {e})))
X : Set α
hX' : X ∈ Js
hfX : f ∉ X
hd : M.Dep (insert e X)
hIs : X ⊆ insert f (J \ {e})
⊢ X ⊆ J
Tactic:
rw [← singleton_union, ← diff_subset_iff, diff_singleton_eq_self hfX] at hIs
Proof state after:
case intro.intro.intro.intro.inl
α : Type u_1
ι : Type u_2
M : Matroid α
F J✝ X✝ Y B C R : Set α
e✝ f✝ x y : α
Js : Set (Set α)
hne : Js.Nonempty
hiI : M.Indep (⋂₀ Js)
e : α
he : ∀ i ∈ Js, e ∈ M.cl i
he' : M.Indep (insert e (⋂₀ Js))
J : Set α
heJ : insert e (⋂₀ Js) ⊆ J
f : α
hI : M.Indep (insert f (J \ {e}))
hiX : ⋂₀ Js ⊆ insert f (J \ {e})
heEI : e ∈ M.E \ insert f (J \ {e})
hJI : M.Basis J (insert e (insert f (J \ {e})))
hIb : M.Basis (insert f (J \ {e})) (insert e (insert f (J \ {e})))
hfIJ : f ∈ insert f (J \ {e}) \ J
hfb : M.Basis (insert f (J \ {e})) (insert e (insert f (J \ {e})))
X : Set α
hX' : X ∈ Js
hfX : f ∉ X
hd : M.Dep (insert e X)
hIs : X ⊆ J \ {e}
⊢ X ⊆ J
Theorem: Matroid.Indep.cl_sInter_eq_biInter_cl_of_forall_subset
Proof state before:
case intro.intro.intro.intro.inl
α : Type u_1
ι : Type u_2
M : Matroid α
F J✝ X✝ Y B C R : Set α
e✝ f✝ x y : α
Js : Set (Set α)
hne : Js.Nonempty
hiI : M.Indep (⋂₀ Js)
e : α
he : ∀ i ∈ Js, e ∈ M.cl i
he' : M.Indep (insert e (⋂₀ Js))
J : Set α
heJ : insert e (⋂₀ Js) ⊆ J
f : α
hI : M.Indep (insert f (J \ {e}))
hiX : ⋂₀ Js ⊆ insert f (J \ {e})
heEI : e ∈ M.E \ insert f (J \ {e})
hJI : M.Basis J (insert e (insert f (J \ {e})))
hIb : M.Basis (insert f (J \ {e})) (insert e (insert f (J \ {e})))
hfIJ : f ∈ insert f (J \ {e}) \ J
hfb : M.Basis (insert f (J \ {e})) (insert e (insert f (J \ {e})))
X : Set α
hX' : X ∈ Js
hfX : f ∉ X
hd : M.Dep (insert e X)
hIs : X ⊆ J \ {e}
⊢ X ⊆ J
Tactic:
exact hIs.trans diff_subset
Proof state after:
no goals
Theorem: Matroid.cl_iInter_eq_iInter_cl_of_iUnion_indep
Proof state before:
α : Type u_1
ι✝ : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e f x y : α
ι : Type u_3
hι : Nonempty ι
Is : ι → Set α
h : M.Indep (⋃ i, Is i)
⊢ M.cl (⋂ i, Is i) = ⋂ i, M.cl (Is i)
Tactic:
convert h.cl_sInter_eq_biInter_cl_of_forall_subset (range_nonempty Is) (by simp [subset_iUnion])
Proof state after:
case h.e'_3
α : Type u_1
ι✝ : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e f x y : α
ι : Type u_3
hι : Nonempty ι
Is : ι → Set α
h : M.Indep (⋃ i, Is i)
⊢ ⋂ i, M.cl (Is i) = ⋂ J ∈ range Is, M.cl J
Theorem: Matroid.cl_iInter_eq_iInter_cl_of_iUnion_indep
Proof state before:
case h.e'_3
α : Type u_1
ι✝ : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e f x y : α
ι : Type u_3
hι : Nonempty ι
Is : ι → Set α
h : M.Indep (⋃ i, Is i)
⊢ ⋂ i, M.cl (Is i) = ⋂ J ∈ range Is, M.cl J
Tactic:
simp
Proof state after:
no goals
Theorem: Matroid.cl_iInter_eq_iInter_cl_of_iUnion_indep
Proof state before:
α : Type u_1
ι✝ : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e f x y : α
ι : Type u_3
hι : Nonempty ι
Is : ι → Set α
h : M.Indep (⋃ i, Is i)
⊢ ∀ J ∈ range Is, J ⊆ ⋃ i, Is i
Tactic:
simp [subset_iUnion]
Proof state after:
no goals
Theorem: Matroid.cl_biInter_eq_biInter_cl_of_biUnion_indep
Proof state before:
α : Type u_1
ι✝ : Type u_2
M : Matroid α
F I✝ J X Y B C R : Set α
e f x y : α
ι : Type u_3
A : Set ι
hA : A.Nonempty
I : ι → Set α
h : M.Indep (⋃ i ∈ A, I i)
⊢ M.cl (⋂ i ∈ A, I i) = ⋂ i ∈ A, M.cl (I i)
Tactic:
have := hA.coe_sort
Proof state after:
α : Type u_1
ι✝ : Type u_2
M : Matroid α
F I✝ J X Y B C R : Set α
e f x y : α
ι : Type u_3
A : Set ι
hA : A.Nonempty
I : ι → Set α
h : M.Indep (⋃ i ∈ A, I i)
this : Nonempty ↑A
⊢ M.cl (⋂ i ∈ A, I i) = ⋂ i ∈ A, M.cl (I i)
Theorem: Matroid.cl_biInter_eq_biInter_cl_of_biUnion_indep
Proof state before:
α : Type u_1
ι✝ : Type u_2
M : Matroid α
F I✝ J X Y B C R : Set α
e f x y : α
ι : Type u_3
A : Set ι
hA : A.Nonempty
I : ι → Set α
h : M.Indep (⋃ i ∈ A, I i)
this : Nonempty ↑A
⊢ M.cl (⋂ i ∈ A, I i) = ⋂ i ∈ A, M.cl (I i)
Tactic:
convert cl_iInter_eq_iInter_cl_of_iUnion_indep (ι := A) (Is := fun i ↦ I i) (by simpa) <;> simp
Proof state after:
no goals
Theorem: Matroid.cl_biInter_eq_biInter_cl_of_biUnion_indep
Proof state before:
α : Type u_1
ι✝ : Type u_2
M : Matroid α
F I✝ J X Y B C R : Set α
e f x y : α
ι : Type u_3
A : Set ι
hA : A.Nonempty
I : ι → Set α
h : M.Indep (⋃ i ∈ A, I i)
this : Nonempty ↑A
⊢ ?m.45300.Indep (⋃ i, (fun i => I ↑i) i)
Tactic:
simpa
Proof state after:
no goals
Theorem: Matroid.Indep.cl_iInter_eq_biInter_cl_of_forall_subset
Proof state before:
α : Type u_1
ι✝ : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e f x y : α
ι : Type u_3
hι : Nonempty ι
Js : ι → Set α
hI : M.Indep I
hJs : ∀ (i : ι), Js i ⊆ I
⊢ ⋃ i, Js i ⊆ I
Tactic:
simpa
Proof state after:
no goals
Theorem: Matroid.Indep.cl_inter_eq_inter_cl
Proof state before:
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e f x y : α
h : M.Indep (I ∪ J)
⊢ M.cl (I ∩ J) = M.cl I ∩ M.cl J
Tactic:
rw [inter_eq_iInter, cl_iInter_eq_iInter_cl_of_iUnion_indep, inter_eq_iInter]
Proof state after:
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e f x y : α
h : M.Indep (I ∪ J)
⊢ ⋂ i, M.cl (bif i then I else J) = ⋂ b, bif b then M.cl I else M.cl J

case h
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e f x y : α
h : M.Indep (I ∪ J)
⊢ M.Indep (⋃ i, bif i then I else J)
Theorem: Matroid.Indep.cl_inter_eq_inter_cl
Proof state before:
case h
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e f x y : α
h : M.Indep (I ∪ J)
⊢ M.Indep (⋃ i, bif i then I else J)
Tactic:
rwa [← union_eq_iUnion]
Proof state after:
no goals
Theorem: Matroid.Indep.cl_inter_eq_inter_cl
Proof state before:
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e f x y : α
h : M.Indep (I ∪ J)
⊢ ⋂ i, M.cl (bif i then I else J) = ⋂ b, bif b then M.cl I else M.cl J
Tactic:
exact iInter_congr (by simp)
Proof state after:
no goals
Theorem: Matroid.Indep.cl_inter_eq_inter_cl
Proof state before:
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e f x y : α
h : M.Indep (I ∪ J)
⊢ ∀ (i : Bool), M.cl (bif i then I else J) = bif i then M.cl I else M.cl J
Tactic:
simp
Proof state after:
no goals
Theorem: Matroid.basis'_iff_basis_cl
Proof state before:
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e f x y : α
⊢ M.Basis' I X ↔ M.Basis I (M.cl X) ∧ I ⊆ X
Tactic:
rw [← cl_inter_ground, basis'_iff_basis_inter_ground]
Proof state after:
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e f x y : α
⊢ M.Basis I (X ∩ M.E) ↔ M.Basis I (M.cl (X ∩ M.E)) ∧ I ⊆ X
Theorem: Matroid.basis'_iff_basis_cl
Proof state before:
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e f x y : α
⊢ M.Basis I (X ∩ M.E) ↔ M.Basis I (M.cl (X ∩ M.E)) ∧ I ⊆ X
Tactic:
exact ⟨fun h ↦ ⟨h.basis_cl_right, h.subset.trans inter_subset_left⟩,
  fun h ↦ h.1.basis_subset (subset_inter h.2 h.1.indep.subset_ground) (M.subset_cl _)⟩
Proof state after:
no goals
Theorem: Matroid.exists_basis_inter_ground_basis_cl
Proof state before:
α : Type u_1
ι : Type u_2
M✝ : Matroid α
F I J X✝ Y B C R : Set α
e f x y : α
M : Matroid α
X : Set α
⊢ ∃ I, M.Basis I (X ∩ M.E) ∧ M.Basis I (M.cl X)
Tactic:
obtain ⟨I, hI⟩ := M.exists_basis (X ∩ M.E)
Proof state after:
case intro
α : Type u_1
ι : Type u_2
M✝ : Matroid α
F I✝ J X✝ Y B C R : Set α
e f x y : α
M : Matroid α
X I : Set α
hI : M.Basis I (X ∩ M.E)
⊢ ∃ I, M.Basis I (X ∩ M.E) ∧ M.Basis I (M.cl X)
Theorem: Matroid.exists_basis_inter_ground_basis_cl
Proof state before:
case intro
α : Type u_1
ι : Type u_2
M✝ : Matroid α
F I✝ J X✝ Y B C R : Set α
e f x y : α
M : Matroid α
X I : Set α
hI : M.Basis I (X ∩ M.E)
⊢ ∃ I, M.Basis I (X ∩ M.E) ∧ M.Basis I (M.cl X)
Tactic:
have hI' := hI.basis_cl_right
Proof state after:
case intro
α : Type u_1
ι : Type u_2
M✝ : Matroid α
F I✝ J X✝ Y B C R : Set α
e f x y : α
M : Matroid α
X I : Set α
hI : M.Basis I (X ∩ M.E)
hI' : M.Basis I (M.cl (X ∩ M.E))
⊢ ∃ I, M.Basis I (X ∩ M.E) ∧ M.Basis I (M.cl X)
Theorem: Matroid.exists_basis_inter_ground_basis_cl
Proof state before:
case intro
α : Type u_1
ι : Type u_2
M✝ : Matroid α
F I✝ J X✝ Y B C R : Set α
e f x y : α
M : Matroid α
X I : Set α
hI : M.Basis I (X ∩ M.E)
hI' : M.Basis I (M.cl (X ∩ M.E))
⊢ ∃ I, M.Basis I (X ∩ M.E) ∧ M.Basis I (M.cl X)
Tactic:
rw [cl_inter_ground] at hI'
Proof state after:
case intro
α : Type u_1
ι : Type u_2
M✝ : Matroid α
F I✝ J X✝ Y B C R : Set α
e f x y : α
M : Matroid α
X I : Set α
hI : M.Basis I (X ∩ M.E)
hI' : M.Basis I (M.cl X)
⊢ ∃ I, M.Basis I (X ∩ M.E) ∧ M.Basis I (M.cl X)
Theorem: Matroid.exists_basis_inter_ground_basis_cl
Proof state before:
case intro
α : Type u_1
ι : Type u_2
M✝ : Matroid α
F I✝ J X✝ Y B C R : Set α
e f x y : α
M : Matroid α
X I : Set α
hI : M.Basis I (X ∩ M.E)
hI' : M.Basis I (M.cl X)
⊢ ∃ I, M.Basis I (X ∩ M.E) ∧ M.Basis I (M.cl X)
Tactic:
exact ⟨_, hI, hI'⟩
Proof state after:
no goals
Theorem: Matroid.Basis.basis_of_cl_eq_cl
Proof state before:
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e f x y : α
hI : M.Basis I X
hY : I ⊆ Y
h : M.cl X = M.cl Y
hYE : autoParam (Y ⊆ M.E) _auto✝
⊢ M.Basis I Y
Tactic:
refine' hI.indep.basis_of_subset_of_subset_cl hY _
Proof state after:
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e f x y : α
hI : M.Basis I X
hY : I ⊆ Y
h : M.cl X = M.cl Y
hYE : autoParam (Y ⊆ M.E) _auto✝
⊢ Y ⊆ M.cl I
Theorem: Matroid.Basis.basis_of_cl_eq_cl
Proof state before:
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e f x y : α
hI : M.Basis I X
hY : I ⊆ Y
h : M.cl X = M.cl Y
hYE : autoParam (Y ⊆ M.E) _auto✝
⊢ Y ⊆ M.cl I
Tactic:
rw [hI.cl_eq_cl, h]
Proof state after:
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e f x y : α
hI : M.Basis I X
hY : I ⊆ Y
h : M.cl X = M.cl Y
hYE : autoParam (Y ⊆ M.E) _auto✝
⊢ Y ⊆ M.cl Y
Theorem: Matroid.Basis.basis_of_cl_eq_cl
Proof state before:
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e f x y : α
hI : M.Basis I X
hY : I ⊆ Y
h : M.cl X = M.cl Y
hYE : autoParam (Y ⊆ M.E) _auto✝
⊢ Y ⊆ M.cl Y
Tactic:
exact M.subset_cl Y
Proof state after:
no goals
Theorem: Matroid.Basis.eq_of_cl_subset
Proof state before:
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e f x y : α
hI : M.Basis I X
hJI : J ⊆ I
hJ : X ⊆ M.cl J
⊢ J = I
Tactic:
rw [← hI.indep.cl_inter_eq_self_of_subset hJI, inter_eq_self_of_subset_right]
Proof state after:
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e f x y : α
hI : M.Basis I X
hJI : J ⊆ I
hJ : X ⊆ M.cl J
⊢ I ⊆ M.cl J
Theorem: Matroid.Basis.eq_of_cl_subset
Proof state before:
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e f x y : α
hI : M.Basis I X
hJI : J ⊆ I
hJ : X ⊆ M.cl J
⊢ I ⊆ M.cl J
Tactic:
exact hI.subset.trans hJ
Proof state after:
no goals
Theorem: Matroid.empty_basis_iff
Proof state before:
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e f x y : α
⊢ M.Basis ∅ X ↔ X ⊆ M.cl ∅
Tactic:
rw [basis_iff_indep_cl, and_iff_right M.empty_indep, and_iff_left (empty_subset _)]
Proof state after:
no goals
Theorem: Matroid.mem_cl_insert
Proof state before:
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e f x y : α
he : e ∉ M.cl X
hef : e ∈ M.cl (insert f X)
⊢ f ∈ M.cl (insert e X)
Tactic:
rw [← cl_inter_ground] at *
Proof state after:
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e f x y : α
he : e ∉ M.cl (X ∩ M.E)
hef : e ∈ M.cl (insert f X ∩ M.E)
⊢ f ∈ M.cl (insert e X ∩ M.E)
Theorem: Matroid.mem_cl_insert
Proof state before:
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e f x y : α
he : e ∉ M.cl (X ∩ M.E)
hef : e ∈ M.cl (insert f X ∩ M.E)
⊢ f ∈ M.cl (insert e X ∩ M.E)
Tactic:
have hfE : f ∈ M.E := by
  by_contra! hfE; rw [insert_inter_of_not_mem hfE] at hef; exact he hef
Proof state after:
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e f x y : α
he : e ∉ M.cl (X ∩ M.E)
hef : e ∈ M.cl (insert f X ∩ M.E)
hfE : f ∈ M.E
⊢ f ∈ M.cl (insert e X ∩ M.E)
Theorem: Matroid.mem_cl_insert
Proof state before:
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e f x y : α
he : e ∉ M.cl (X ∩ M.E)
hef : e ∈ M.cl (insert f X ∩ M.E)
hfE : f ∈ M.E
⊢ f ∈ M.cl (insert e X ∩ M.E)
Tactic:
have heE : e ∈ M.E := (M.cl_subset_ground _) hef
Proof state after:
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e f x y : α
he : e ∉ M.cl (X ∩ M.E)
hef : e ∈ M.cl (insert f X ∩ M.E)
hfE : f ∈ M.E
heE : e ∈ M.E
⊢ f ∈ M.cl (insert e X ∩ M.E)
Theorem: Matroid.mem_cl_insert
Proof state before:
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e f x y : α
he : e ∉ M.cl (X ∩ M.E)
hef : e ∈ M.cl (insert f X ∩ M.E)
hfE : f ∈ M.E
heE : e ∈ M.E
⊢ f ∈ M.cl (insert e X ∩ M.E)
Tactic:
rw [insert_inter_of_mem hfE] at hef
Proof state after:
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e f x y : α
he : e ∉ M.cl (X ∩ M.E)
hef : e ∈ M.cl (insert f (X ∩ M.E))
hfE : f ∈ M.E
heE : e ∈ M.E
⊢ f ∈ M.cl (insert e X ∩ M.E)
Theorem: Matroid.mem_cl_insert
Proof state before:
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e f x y : α
he : e ∉ M.cl (X ∩ M.E)
hef : e ∈ M.cl (insert f (X ∩ M.E))
hfE : f ∈ M.E
heE : e ∈ M.E
⊢ f ∈ M.cl (insert e X ∩ M.E)
Tactic:
rw [insert_inter_of_mem heE]
Proof state after:
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e f x y : α
he : e ∉ M.cl (X ∩ M.E)
hef : e ∈ M.cl (insert f (X ∩ M.E))
hfE : f ∈ M.E
heE : e ∈ M.E
⊢ f ∈ M.cl (insert e (X ∩ M.E))
Theorem: Matroid.mem_cl_insert
Proof state before:
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e f x y : α
he : e ∉ M.cl (X ∩ M.E)
hef : e ∈ M.cl (insert f (X ∩ M.E))
hfE : f ∈ M.E
heE : e ∈ M.E
⊢ f ∈ M.cl (insert e (X ∩ M.E))
Tactic:
obtain ⟨I, hI⟩ := M.exists_basis (X ∩ M.E)
Proof state after:
case intro
α : Type u_1
ι : Type u_2
M : Matroid α
F I✝ J X Y B C R : Set α
e f x y : α
he : e ∉ M.cl (X ∩ M.E)
hef : e ∈ M.cl (insert f (X ∩ M.E))
hfE : f ∈ M.E
heE : e ∈ M.E
I : Set α
hI : M.Basis I (X ∩ M.E)
⊢ f ∈ M.cl (insert e (X ∩ M.E))
Theorem: Matroid.mem_cl_insert
Proof state before:
case intro
α : Type u_1
ι : Type u_2
M : Matroid α
F I✝ J X Y B C R : Set α
e f x y : α
he : e ∉ M.cl (X ∩ M.E)
hef : e ∈ M.cl (insert f (X ∩ M.E))
hfE : f ∈ M.E
heE : e ∈ M.E
I : Set α
hI : M.Basis I (X ∩ M.E)
⊢ f ∈ M.cl (insert e (X ∩ M.E))
Tactic:
rw [← hI.cl_eq_cl, hI.indep.not_mem_cl_iff] at he
Proof state after:
case intro
α : Type u_1
ι : Type u_2
M : Matroid α
F I✝ J X Y B C R : Set α
e f x y : α
hef : e ∈ M.cl (insert f (X ∩ M.E))
hfE : f ∈ M.E
heE : e ∈ M.E
I : Set α
he : M.Indep (insert e I) ∧ e ∉ I
hI : M.Basis I (X ∩ M.E)
⊢ f ∈ M.cl (insert e (X ∩ M.E))
Theorem: Matroid.mem_cl_insert
Proof state before:
case intro
α : Type u_1
ι : Type u_2
M : Matroid α
F I✝ J X Y B C R : Set α
e f x y : α
hef : e ∈ M.cl (insert f (X ∩ M.E))
hfE : f ∈ M.E
heE : e ∈ M.E
I : Set α
he : M.Indep (insert e I) ∧ e ∉ I
hI : M.Basis I (X ∩ M.E)
⊢ f ∈ M.cl (insert e (X ∩ M.E))
Tactic:
rw [← cl_insert_cl_eq_cl_insert, ← hI.cl_eq_cl, cl_insert_cl_eq_cl_insert, he.1.mem_cl_iff] at *
Proof state after:
case intro
α : Type u_1
ι : Type u_2
M : Matroid α
F I✝ J X Y B C R : Set α
e f x y : α
hfE : f ∈ M.E
heE : e ∈ M.E
I : Set α
hef : e ∈ M.cl (insert f I)
he : M.Indep (insert e I) ∧ e ∉ I
hI : M.Basis I (X ∩ M.E)
⊢ M.Dep (insert f (insert e I)) ∨ f ∈ insert e I
Theorem: Matroid.mem_cl_insert
Proof state before:
case intro
α : Type u_1
ι : Type u_2
M : Matroid α
F I✝ J X Y B C R : Set α
e f x y : α
hfE : f ∈ M.E
heE : e ∈ M.E
I : Set α
hef : e ∈ M.cl (insert f I)
he : M.Indep (insert e I) ∧ e ∉ I
hI : M.Basis I (X ∩ M.E)
⊢ M.Dep (insert f (insert e I)) ∨ f ∈ insert e I
Tactic:
rw [or_iff_not_imp_left, dep_iff, insert_comm,
  and_iff_left (insert_subset heE (insert_subset hfE hI.indep.subset_ground)), not_not]
Proof state after:
case intro
α : Type u_1
ι : Type u_2
M : Matroid α
F I✝ J X Y B C R : Set α
e f x y : α
hfE : f ∈ M.E
heE : e ∈ M.E
I : Set α
hef : e ∈ M.cl (insert f I)
he : M.Indep (insert e I) ∧ e ∉ I
hI : M.Basis I (X ∩ M.E)
⊢ M.Indep (insert e (insert f I)) → f ∈ insert e I
Theorem: Matroid.mem_cl_insert
Proof state before:
case intro
α : Type u_1
ι : Type u_2
M : Matroid α
F I✝ J X Y B C R : Set α
e f x y : α
hfE : f ∈ M.E
heE : e ∈ M.E
I : Set α
hef : e ∈ M.cl (insert f I)
he : M.Indep (insert e I) ∧ e ∉ I
hI : M.Basis I (X ∩ M.E)
⊢ M.Indep (insert e (insert f I)) → f ∈ insert e I
Tactic:
intro h
Proof state after:
case intro
α : Type u_1
ι : Type u_2
M : Matroid α
F I✝ J X Y B C R : Set α
e f x y : α
hfE : f ∈ M.E
heE : e ∈ M.E
I : Set α
hef : e ∈ M.cl (insert f I)
he : M.Indep (insert e I) ∧ e ∉ I
hI : M.Basis I (X ∩ M.E)
h : M.Indep (insert e (insert f I))
⊢ f ∈ insert e I
Theorem: Matroid.mem_cl_insert
Proof state before:
case intro
α : Type u_1
ι : Type u_2
M : Matroid α
F I✝ J X Y B C R : Set α
e f x y : α
hfE : f ∈ M.E
heE : e ∈ M.E
I : Set α
hef : e ∈ M.cl (insert f I)
he : M.Indep (insert e I) ∧ e ∉ I
hI : M.Basis I (X ∩ M.E)
h : M.Indep (insert e (insert f I))
⊢ f ∈ insert e I
Tactic:
rw [(h.subset (subset_insert _ _)).mem_cl_iff, or_iff_right (h.not_dep), mem_insert_iff,
  or_iff_left he.2] at hef
Proof state after:
case intro
α : Type u_1
ι : Type u_2
M : Matroid α
F I✝ J X Y B C R : Set α
e f x y : α
hfE : f ∈ M.E
heE : e ∈ M.E
I : Set α
hef : e = f
he : M.Indep (insert e I) ∧ e ∉ I
hI : M.Basis I (X ∩ M.E)
h : M.Indep (insert e (insert f I))
⊢ f ∈ insert e I
Theorem: Matroid.mem_cl_insert
Proof state before:
case intro
α : Type u_1
ι : Type u_2
M : Matroid α
F I✝ J X Y B C R : Set α
e f x y : α
hfE : f ∈ M.E
heE : e ∈ M.E
I : Set α
hef : e = f
he : M.Indep (insert e I) ∧ e ∉ I
hI : M.Basis I (X ∩ M.E)
h : M.Indep (insert e (insert f I))
⊢ f ∈ insert e I
Tactic:
subst hef
Proof state after:
case intro
α : Type u_1
ι : Type u_2
M : Matroid α
F I✝ J X Y B C R : Set α
e x y : α
heE : e ∈ M.E
I : Set α
he : M.Indep (insert e I) ∧ e ∉ I
hI : M.Basis I (X ∩ M.E)
hfE : e ∈ M.E
h : M.Indep (insert e (insert e I))
⊢ e ∈ insert e I
Theorem: Matroid.mem_cl_insert
Proof state before:
case intro
α : Type u_1
ι : Type u_2
M : Matroid α
F I✝ J X Y B C R : Set α
e x y : α
heE : e ∈ M.E
I : Set α
he : M.Indep (insert e I) ∧ e ∉ I
hI : M.Basis I (X ∩ M.E)
hfE : e ∈ M.E
h : M.Indep (insert e (insert e I))
⊢ e ∈ insert e I
Tactic:
apply mem_insert
Proof state after:
no goals
Theorem: Matroid.mem_cl_insert
Proof state before:
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e f x y : α
he : e ∉ M.cl (X ∩ M.E)
hef : e ∈ M.cl (insert f X ∩ M.E)
⊢ f ∈ M.E
Tactic:
by_contra! hfE
Proof state after:
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e f x y : α
he : e ∉ M.cl (X ∩ M.E)
hef : e ∈ M.cl (insert f X ∩ M.E)
hfE : f ∉ M.E
⊢ False
Theorem: Matroid.mem_cl_insert
Proof state before:
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e f x y : α
he : e ∉ M.cl (X ∩ M.E)
hef : e ∈ M.cl (insert f X ∩ M.E)
hfE : f ∉ M.E
⊢ False
Tactic:
rw [insert_inter_of_not_mem hfE] at hef
Proof state after:
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e f x y : α
he : e ∉ M.cl (X ∩ M.E)
hef : e ∈ M.cl (X ∩ M.E)
hfE : f ∉ M.E
⊢ False
Theorem: Matroid.mem_cl_insert
Proof state before:
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e f x y : α
he : e ∉ M.cl (X ∩ M.E)
hef : e ∈ M.cl (X ∩ M.E)
hfE : f ∉ M.E
⊢ False
Tactic:
exact he hef
Proof state after:
no goals
Theorem: Matroid.cl_exchange
Proof state before:
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e f x y : α
he : e ∈ M.cl (insert f X) \ M.cl X
hf : f ∈ M.cl X
⊢ False
Tactic:
rwa [cl_insert_eq_of_mem_cl hf, diff_self, iff_false_intro (not_mem_empty _)] at he
Proof state after:
no goals
Theorem: Matroid.cl_insert_eq_cl_insert_of_mem
Proof state before:
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e f x y : α
he : e ∈ M.cl (insert f X) \ M.cl X
⊢ M.cl (insert e X) = M.cl (insert f X)
Tactic:
have hf := cl_exchange he
Proof state after:
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e f x y : α
he : e ∈ M.cl (insert f X) \ M.cl X
hf : f ∈ M.cl (insert e X) \ M.cl X
⊢ M.cl (insert e X) = M.cl (insert f X)
Theorem: Matroid.cl_insert_eq_cl_insert_of_mem
Proof state before:
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e f x y : α
he : e ∈ M.cl (insert f X) \ M.cl X
hf : f ∈ M.cl (insert e X) \ M.cl X
⊢ M.cl (insert e X) = M.cl (insert f X)
Tactic:
rw [eq_comm, ← cl_cl, ← insert_eq_of_mem he.1, cl_insert_cl_eq_cl_insert, insert_comm, ← cl_cl,
  ← cl_insert_cl_eq_cl_insert, insert_eq_of_mem hf.1, cl_cl, cl_cl]
Proof state after:
no goals