internlm/Lean-Github huggingface dataset:
Theorem: Matroid.map_cl_eq
Proof state before:
case intro.intro.intro.intro.intro.h.refine_1.intro.intro.intro
α : Type u_1
ι : Type u_2
M✝ : Matroid α
F I✝ J✝ X✝ Y B C R : Set α
e✝ f✝ x y : α
β : Type u_3
M : Matroid α
f : α → β
hf : InjOn f M.E
I X : Set α
hI' : M.Basis I X
hX : f '' X ⊆ f '' M.E
hI : (M.map f hf).Basis (f '' I) (f '' X)
e : α
heE : e ∈ M.E
hind : M.Indep (insert e I) → e ∈ I
J : Set α
hJ : M.Indep J
hins : insert (f e) (f '' I) = f '' J
⊢ M.Indep (insert e I)
Tactic:
rw [← image_insert_eq,
  hf.image_eq_image_iff (insert_subset heE hI'.indep.subset_ground) hJ.subset_ground] at hins
Proof state after:
case intro.intro.intro.intro.intro.h.refine_1.intro.intro.intro
α : Type u_1
ι : Type u_2
M✝ : Matroid α
F I✝ J✝ X✝ Y B C R : Set α
e✝ f✝ x y : α
β : Type u_3
M : Matroid α
f : α → β
hf : InjOn f M.E
I X : Set α
hI' : M.Basis I X
hX : f '' X ⊆ f '' M.E
hI : (M.map f hf).Basis (f '' I) (f '' X)
e : α
heE : e ∈ M.E
hind : M.Indep (insert e I) → e ∈ I
J : Set α
hJ : M.Indep J
hins : insert e I = J
⊢ M.Indep (insert e I)
Theorem: Matroid.map_cl_eq
Proof state before:
case intro.intro.intro.intro.intro.h.refine_1.intro.intro.intro
α : Type u_1
ι : Type u_2
M✝ : Matroid α
F I✝ J✝ X✝ Y B C R : Set α
e✝ f✝ x y : α
β : Type u_3
M : Matroid α
f : α → β
hf : InjOn f M.E
I X : Set α
hI' : M.Basis I X
hX : f '' X ⊆ f '' M.E
hI : (M.map f hf).Basis (f '' I) (f '' X)
e : α
heE : e ∈ M.E
hind : M.Indep (insert e I) → e ∈ I
J : Set α
hJ : M.Indep J
hins : insert e I = J
⊢ M.Indep (insert e I)
Tactic:
rwa [hins]
Proof state after:
no goals
Theorem: Matroid.map_cl_eq
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
M : Matroid α
f : α → β
hf : InjOn f M.E
I X : Set α
hI' : M.Basis I X
hX : f '' X ⊆ f '' M.E
hI : (M.map f hf).Basis (f '' I) (f '' X)
x : α
hx : x ∈ M.E
h : ∀ (x_1 : Set α), M.Indep x_1 → insert (f x) (f '' I) = f '' x_1 → ∃ x_2 ∈ I, f x_2 = f x
hind : M.Indep (insert x I)
⊢ insert (f x) (f '' I) = f '' insert x I
Tactic:
rw [image_insert_eq]
Proof state after:
no goals
Theorem: Matroid.cl_spanning_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 : α
S T : Set α
hS : autoParam (S ⊆ M.E) _auto✝
⊢ M.Spanning (M.cl S) ↔ M.Spanning S
Tactic:
rw [spanning_iff_cl, cl_cl, ← spanning_iff_cl]
Proof state after:
no goals
Theorem: Matroid.spanning_iff_ground_subset_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 : α
S T : Set α
hS : autoParam (S ⊆ M.E) _auto✝
⊢ M.Spanning S ↔ M.E ⊆ M.cl S
Tactic:
rw [spanning_iff_cl, subset_antisymm_iff, and_iff_right (cl_subset_ground _ _)]
Proof state after:
no goals
Theorem: Matroid.not_spanning_iff_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 : α
S T : Set α
hS : autoParam (S ⊆ M.E) _auto✝
⊢ ¬M.Spanning S ↔ M.cl S ⊂ M.E
Tactic:
rw [spanning_iff_cl, ssubset_iff_subset_ne, iff_and_self, iff_true_intro (M.cl_subset_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 : α
S T : Set α
hS : autoParam (S ⊆ M.E) _auto✝
⊢ ¬M.cl S = M.E → True
Theorem: Matroid.not_spanning_iff_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 : α
S T : Set α
hS : autoParam (S ⊆ M.E) _auto✝
⊢ ¬M.cl S = M.E → True
Tactic:
exact fun _ ↦ trivial
Proof state after:
no goals
Theorem: Matroid.Spanning.superset
Proof state before:
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e f x y : α
S T : Set α
hS : M.Spanning S
hST : S ⊆ T
hT : autoParam (T ⊆ M.E) _auto✝
⊢ M.E ⊆ M.cl T
Tactic:
rw [← hS.cl_eq]
Proof state after:
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e f x y : α
S T : Set α
hS : M.Spanning S
hST : S ⊆ T
hT : autoParam (T ⊆ M.E) _auto✝
⊢ M.cl S ⊆ M.cl T
Theorem: Matroid.Spanning.superset
Proof state before:
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e f x y : α
S T : Set α
hS : M.Spanning S
hST : S ⊆ T
hT : autoParam (T ⊆ M.E) _auto✝
⊢ M.cl S ⊆ M.cl T
Tactic:
exact M.cl_subset_cl hST
Proof state after:
no goals
Theorem: Matroid.Spanning.cl_superset_eq
Proof state before:
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e f x y : α
S T : Set α
hS : M.Spanning S
hST : S ⊆ T
⊢ M.cl T = M.E
Tactic:
rw [← cl_inter_ground, ← spanning_iff_cl]
Proof state after:
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e f x y : α
S T : Set α
hS : M.Spanning S
hST : S ⊆ T
⊢ M.Spanning (T ∩ M.E)
Theorem: Matroid.Spanning.cl_superset_eq
Proof state before:
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e f x y : α
S T : Set α
hS : M.Spanning S
hST : S ⊆ T
⊢ M.Spanning (T ∩ M.E)
Tactic:
exact hS.superset (subset_inter hST hS.subset_ground)
Proof state after:
no goals
Theorem: Matroid.spanning_iff_superset_base'
Proof state before:
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e f x y : α
S T : Set α
⊢ M.Spanning S ↔ (∃ B, M.Base B ∧ B ⊆ S) ∧ S ⊆ M.E
Tactic:
refine' ⟨fun h ↦ ⟨_, h.subset_ground⟩, fun ⟨⟨B, hB, hBS⟩, hSE⟩ ↦ hB.spanning.superset hBS⟩
Proof state after:
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e f x y : α
S T : Set α
h : M.Spanning S
⊢ ∃ B, M.Base B ∧ B ⊆ S
Theorem: Matroid.spanning_iff_superset_base'
Proof state before:
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e f x y : α
S T : Set α
h : M.Spanning S
⊢ ∃ B, M.Base B ∧ B ⊆ S
Tactic:
obtain ⟨B, hB⟩ := M.exists_basis S
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 : α
S T : Set α
h : M.Spanning S
B : Set α
hB : M.Basis B S
⊢ ∃ B, M.Base B ∧ B ⊆ S
Theorem: Matroid.spanning_iff_superset_base'
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 : α
S T : Set α
h : M.Spanning S
B : Set α
hB : M.Basis B S
⊢ ∃ B, M.Base B ∧ B ⊆ S
Tactic:
have hB' := hB.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 : α
S T : Set α
h : M.Spanning S
B : Set α
hB : M.Basis B S
hB' : M.Basis B (M.cl S)
⊢ ∃ B, M.Base B ∧ B ⊆ S
Theorem: Matroid.spanning_iff_superset_base'
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 : α
S T : Set α
h : M.Spanning S
B : Set α
hB : M.Basis B S
hB' : M.Basis B (M.cl S)
⊢ ∃ B, M.Base B ∧ B ⊆ S
Tactic:
rw [h.cl_eq, basis_ground_iff] at hB'
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 : α
S T : Set α
h : M.Spanning S
B : Set α
hB : M.Basis B S
hB' : M.Base B
⊢ ∃ B, M.Base B ∧ B ⊆ S
Theorem: Matroid.spanning_iff_superset_base'
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 : α
S T : Set α
h : M.Spanning S
B : Set α
hB : M.Basis B S
hB' : M.Base B
⊢ ∃ B, M.Base B ∧ B ⊆ S
Tactic:
exact ⟨B, hB', hB.subset⟩
Proof state after:
no goals
Theorem: Matroid.spanning_iff_superset_base
Proof state before:
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e f x y : α
S T : Set α
hS : autoParam (S ⊆ M.E) _auto✝
⊢ M.Spanning S ↔ ∃ B, M.Base B ∧ B ⊆ S
Tactic:
rw [spanning_iff_superset_base', and_iff_left hS]
Proof state after:
no goals
Theorem: Matroid.Spanning.exists_base_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 : α
S T : Set α
hS : M.Spanning S
⊢ ∃ B, M.Base B ∧ B ⊆ S
Tactic:
rwa [spanning_iff_superset_base] at hS
Proof state after:
no goals
Theorem: Matroid.coindep_iff_compl_spanning
Proof state before:
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e f x y : α
S T : Set α
hI : autoParam (I ⊆ M.E) _auto✝
⊢ M.Coindep I ↔ M.Spanning (M.E \ I)
Tactic:
rw [coindep_iff_exists, spanning_iff_superset_base]
Proof state after:
no goals
Theorem: Matroid.spanning_iff_compl_coindep
Proof state before:
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e f x y : α
S T : Set α
hS : autoParam (S ⊆ M.E) _auto✝
⊢ M.Spanning S ↔ M.Coindep (M.E \ S)
Tactic:
rw [coindep_iff_compl_spanning, diff_diff_cancel_left hS]
Proof state after:
no goals
Theorem: Matroid.coindep_iff_cl_compl_eq_ground
Proof state before:
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e f x y : α
S T : Set α
hK : autoParam (X ⊆ M.E) _auto✝
⊢ M.Coindep X ↔ M.cl (M.E \ X) = M.E
Tactic:
rw [coindep_iff_compl_spanning, spanning_iff_cl]
Proof state after:
no goals
Theorem: Matroid.Indep.base_of_spanning
Proof state before:
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e f x y : α
S T : Set α
hI : M.Indep I
hIs : M.Spanning I
⊢ M.Base I
Tactic:
obtain ⟨B, hB, hBI⟩ := hIs.exists_base_subset
Proof state after:
case intro.intro
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B✝ C R : Set α
e f x y : α
S T : Set α
hI : M.Indep I
hIs : M.Spanning I
B : Set α
hB : M.Base B
hBI : B ⊆ I
⊢ M.Base I
Theorem: Matroid.Indep.base_of_spanning
Proof state before:
case intro.intro
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B✝ C R : Set α
e f x y : α
S T : Set α
hI : M.Indep I
hIs : M.Spanning I
B : Set α
hB : M.Base B
hBI : B ⊆ I
⊢ M.Base I
Tactic:
rwa [← hB.eq_of_subset_indep hI hBI]
Proof state after:
no goals
Theorem: Matroid.eq_of_spanning_iff_spanning_forall
Proof state before:
α : Type u_1
ι : Type u_2
M✝ : Matroid α
F I J X Y B C R : Set α
e f x y : α
S T : Set α
M M' : Matroid α
h : M.E = M'.E
hsp : ∀ S ⊆ M.E, M.Spanning S ↔ M'.Spanning S
⊢ M = M'
Tactic:
have hsp' : M.Spanning = M'.Spanning := by
  ext S
  refine (em (S ⊆ M.E)).elim (fun hSE ↦ by rw [hsp _ hSE] )
    (fun hSE ↦ iff_of_false (fun h ↦ hSE h.subset_ground)
    (fun h' ↦ hSE (h'.subset_ground.trans h.symm.subset)))
Proof state after:
α : Type u_1
ι : Type u_2
M✝ : Matroid α
F I J X Y B C R : Set α
e f x y : α
S T : Set α
M M' : Matroid α
h : M.E = M'.E
hsp : ∀ S ⊆ M.E, M.Spanning S ↔ M'.Spanning S
hsp' : M.Spanning = M'.Spanning
⊢ M = M'
Theorem: Matroid.eq_of_spanning_iff_spanning_forall
Proof state before:
α : Type u_1
ι : Type u_2
M✝ : Matroid α
F I J X Y B C R : Set α
e f x y : α
S T : Set α
M M' : Matroid α
h : M.E = M'.E
hsp : ∀ S ⊆ M.E, M.Spanning S ↔ M'.Spanning S
hsp' : M.Spanning = M'.Spanning
⊢ M = M'
Tactic:
rw [← dual_inj, eq_iff_indep_iff_indep_forall, dual_ground, dual_ground, and_iff_right 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 : α
S T : Set α
M M' : Matroid α
h : M.E = M'.E
hsp : ∀ S ⊆ M.E, M.Spanning S ↔ M'.Spanning S
hsp' : M.Spanning = M'.Spanning
⊢ ∀ I ⊆ M.E, M✶.Indep I ↔ M'✶.Indep I
Theorem: Matroid.eq_of_spanning_iff_spanning_forall
Proof state before:
α : Type u_1
ι : Type u_2
M✝ : Matroid α
F I J X Y B C R : Set α
e f x y : α
S T : Set α
M M' : Matroid α
h : M.E = M'.E
hsp : ∀ S ⊆ M.E, M.Spanning S ↔ M'.Spanning S
hsp' : M.Spanning = M'.Spanning
⊢ ∀ I ⊆ M.E, M✶.Indep I ↔ M'✶.Indep I
Tactic:
intro I hIE
Proof state after:
α : Type u_1
ι : Type u_2
M✝ : Matroid α
F I✝ J X Y B C R : Set α
e f x y : α
S T : Set α
M M' : Matroid α
h : M.E = M'.E
hsp : ∀ S ⊆ M.E, M.Spanning S ↔ M'.Spanning S
hsp' : M.Spanning = M'.Spanning
I : Set α
hIE : I ⊆ M.E
⊢ M✶.Indep I ↔ M'✶.Indep I
Theorem: Matroid.eq_of_spanning_iff_spanning_forall
Proof state before:
α : Type u_1
ι : Type u_2
M✝ : Matroid α
F I✝ J X Y B C R : Set α
e f x y : α
S T : Set α
M M' : Matroid α
h : M.E = M'.E
hsp : ∀ S ⊆ M.E, M.Spanning S ↔ M'.Spanning S
hsp' : M.Spanning = M'.Spanning
I : Set α
hIE : I ⊆ M.E
⊢ M✶.Indep I ↔ M'✶.Indep I
Tactic:
rw [← coindep_def, ← coindep_def, coindep_iff_compl_spanning, coindep_iff_compl_spanning, hsp', h]
Proof state after:
no goals
Theorem: Matroid.eq_of_spanning_iff_spanning_forall
Proof state before:
α : Type u_1
ι : Type u_2
M✝ : Matroid α
F I J X Y B C R : Set α
e f x y : α
S T : Set α
M M' : Matroid α
h : M.E = M'.E
hsp : ∀ S ⊆ M.E, M.Spanning S ↔ M'.Spanning S
⊢ M.Spanning = M'.Spanning
Tactic:
ext S
Proof state after:
case h.a
α : Type u_1
ι : Type u_2
M✝ : Matroid α
F I J X Y B C R : Set α
e f x y : α
S✝ T : Set α
M M' : Matroid α
h : M.E = M'.E
hsp : ∀ S ⊆ M.E, M.Spanning S ↔ M'.Spanning S
S : Set α
⊢ M.Spanning S ↔ M'.Spanning S
Theorem: Matroid.eq_of_spanning_iff_spanning_forall
Proof state before:
case h.a
α : Type u_1
ι : Type u_2
M✝ : Matroid α
F I J X Y B C R : Set α
e f x y : α
S✝ T : Set α
M M' : Matroid α
h : M.E = M'.E
hsp : ∀ S ⊆ M.E, M.Spanning S ↔ M'.Spanning S
S : Set α
⊢ M.Spanning S ↔ M'.Spanning S
Tactic:
refine (em (S ⊆ M.E)).elim (fun hSE ↦ by rw [hsp _ hSE] )
  (fun hSE ↦ iff_of_false (fun h ↦ hSE h.subset_ground)
  (fun h' ↦ hSE (h'.subset_ground.trans h.symm.subset)))
Proof state after:
no goals
Theorem: Matroid.eq_of_spanning_iff_spanning_forall
Proof state before:
α : Type u_1
ι : Type u_2
M✝ : Matroid α
F I J X Y B C R : Set α
e f x y : α
S✝ T : Set α
M M' : Matroid α
h : M.E = M'.E
hsp : ∀ S ⊆ M.E, M.Spanning S ↔ M'.Spanning S
S : Set α
hSE : S ⊆ M.E
⊢ M.Spanning S ↔ M'.Spanning S
Tactic:
rw [hsp _ hSE]
Proof state after:
no goals
Theorem: Matroid.emptyOn_cl_eq
Proof state before:
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X✝ Y B C R : Set α
e f x y : α
X : Set α
⊢ (emptyOn α).cl X = ∅
Tactic:
rw [← subset_empty_iff, ← emptyOn_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 : α
X : Set α
⊢ (emptyOn α).cl X ⊆ (emptyOn α).E
Theorem: Matroid.emptyOn_cl_eq
Proof state before:
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X✝ Y B C R : Set α
e f x y : α
X : Set α
⊢ (emptyOn α).cl X ⊆ (emptyOn α).E
Tactic:
apply cl_subset_ground
Proof state after:
no goals
Theorem: Matroid.loopyOn_cl_eq
Proof state before:
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X✝ Y B C R : Set α
e f x y : α
E X : Set α
⊢ (loopyOn E).E ⊆ (loopyOn E).cl ∅
Tactic:
rw [(loopyOn_base_iff.2 rfl).cl_eq]
Proof state after:
no goals
Theorem: Matroid.cl_empty_eq_ground_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.cl ∅ = M.E ↔ M = loopyOn M.E
Tactic:
refine ⟨fun h ↦ eq_of_cl_eq_cl_forall ?_, fun h ↦ by rw [h, loopyOn_cl_eq, loopyOn_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 : α
h : M.cl ∅ = M.E
⊢ ∀ (X : Set α), M.cl X = (loopyOn M.E).cl X
Theorem: Matroid.cl_empty_eq_ground_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 : α
h : M.cl ∅ = M.E
⊢ ∀ (X : Set α), M.cl X = (loopyOn M.E).cl X
Tactic:
refine fun X ↦ subset_antisymm (by simp [cl_subset_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 : α
h : M.cl ∅ = M.E
X : Set α
⊢ (loopyOn M.E).cl X ⊆ M.cl X
Theorem: Matroid.cl_empty_eq_ground_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 : α
h : M.cl ∅ = M.E
X : Set α
⊢ (loopyOn M.E).cl X ⊆ M.cl X
Tactic:
rw [loopyOn_cl_eq, ← 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 : α
h : M.cl ∅ = M.E
X : Set α
⊢ M.cl ∅ ⊆ M.cl X
Theorem: Matroid.cl_empty_eq_ground_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 : α
h : M.cl ∅ = M.E
X : Set α
⊢ M.cl ∅ ⊆ M.cl X
Tactic:
exact M.cl_mono (empty_subset _)
Proof state after:
no goals
Theorem: Matroid.cl_empty_eq_ground_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 : α
h : M = loopyOn M.E
⊢ M.cl ∅ = M.E
Tactic:
rw [h, loopyOn_cl_eq, loopyOn_ground]
Proof state after:
no goals
Theorem: Matroid.cl_empty_eq_ground_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 : α
h : M.cl ∅ = M.E
X : Set α
⊢ M.cl X ⊆ (loopyOn M.E).cl X
Tactic:
simp [cl_subset_ground]
Proof state after:
no goals
Theorem: Matroid.uniqueBaseOn_cl_eq
Proof state before:
α : Type u_1
ι : Type u_2
M : Matroid α
F I✝ J X✝ Y B C R : Set α
e f x y : α
I E X : Set α
⊢ (uniqueBaseOn I E).cl X = X ∩ I ∩ E ∪ E \ I
Tactic:
have hb : (uniqueBaseOn (I ∩ E) E).Basis (X ∩ E ∩ (I ∩ E)) (X ∩ E) :=
  (uniqueBaseOn_basis_iff inter_subset_right inter_subset_right).2 rfl
Proof state after:
α : Type u_1
ι : Type u_2
M : Matroid α
F I✝ J X✝ Y B C R : Set α
e f x y : α
I E X : Set α
hb : (uniqueBaseOn (I ∩ E) E).Basis (X ∩ E ∩ (I ∩ E)) (X ∩ E)
⊢ (uniqueBaseOn I E).cl X = X ∩ I ∩ E ∪ E \ I
Theorem: Matroid.uniqueBaseOn_cl_eq
Proof state before:
α : Type u_1
ι : Type u_2
M : Matroid α
F I✝ J X✝ Y B C R : Set α
e f x y : α
I E X : Set α
hb : (uniqueBaseOn (I ∩ E) E).Basis (X ∩ E ∩ (I ∩ E)) (X ∩ E)
⊢ (uniqueBaseOn I E).cl X = X ∩ I ∩ E ∪ E \ I
Tactic:
ext e
Proof state after:
case h
α : Type u_1
ι : Type u_2
M : Matroid α
F I✝ J X✝ Y B C R : Set α
e✝ f x y : α
I E X : Set α
hb : (uniqueBaseOn (I ∩ E) E).Basis (X ∩ E ∩ (I ∩ E)) (X ∩ E)
e : α
⊢ e ∈ (uniqueBaseOn I E).cl X ↔ e ∈ X ∩ I ∩ E ∪ E \ I
Theorem: Matroid.uniqueBaseOn_cl_eq
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 : α
I E X : Set α
hb : (uniqueBaseOn (I ∩ E) E).Basis (X ∩ E ∩ (I ∩ E)) (X ∩ E)
e : α
⊢ e ∈ (uniqueBaseOn I E).cl X ↔ e ∈ X ∩ I ∩ E ∪ E \ I
Tactic:
rw [← uniqueBaseOn_inter_ground_eq I E, ← cl_inter_ground _ X, uniqueBaseOn_ground,
  ← hb.cl_eq_cl, hb.indep.mem_cl_iff, dep_iff, uniqueBaseOn_indep_iff', insert_subset_iff,
  uniqueBaseOn_ground, inter_assoc, inter_self,  and_iff_left inter_subset_right,
  ← inter_inter_distrib_right, inter_assoc, inter_union_distrib_right, inter_comm I,
  inter_union_diff, insert_subset_iff, inter_comm X, inter_assoc,
  and_iff_left inter_subset_left, mem_inter_iff]
Proof state after:
case h
α : Type u_1
ι : Type u_2
M : Matroid α
F I✝ J X✝ Y B C R : Set α
e✝ f x y : α
I E X : Set α
hb : (uniqueBaseOn (I ∩ E) E).Basis (X ∩ E ∩ (I ∩ E)) (X ∩ E)
e : α
⊢ ¬(e ∈ E ∧ e ∈ I) ∧ e ∈ E ∨ e ∈ E ∩ (I ∩ X) ↔ e ∈ (X ∪ E \ I) ∩ E
Theorem: Matroid.uniqueBaseOn_cl_eq
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 : α
I E X : Set α
hb : (uniqueBaseOn (I ∩ E) E).Basis (X ∩ E ∩ (I ∩ E)) (X ∩ E)
e : α
⊢ ¬(e ∈ E ∧ e ∈ I) ∧ e ∈ E ∨ e ∈ E ∩ (I ∩ X) ↔ e ∈ (X ∪ E \ I) ∩ E
Tactic:
simp only [not_and, mem_inter_iff, mem_union, mem_diff]
Proof state after:
case h
α : Type u_1
ι : Type u_2
M : Matroid α
F I✝ J X✝ Y B C R : Set α
e✝ f x y : α
I E X : Set α
hb : (uniqueBaseOn (I ∩ E) E).Basis (X ∩ E ∩ (I ∩ E)) (X ∩ E)
e : α
⊢ (e ∈ E → e ∉ I) ∧ e ∈ E ∨ e ∈ E ∧ e ∈ I ∧ e ∈ X ↔ (e ∈ X ∨ e ∈ E ∧ e ∉ I) ∧ e ∈ E
Theorem: Matroid.uniqueBaseOn_cl_eq
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 : α
I E X : Set α
hb : (uniqueBaseOn (I ∩ E) E).Basis (X ∩ E ∩ (I ∩ E)) (X ∩ E)
e : α
⊢ (e ∈ E → e ∉ I) ∧ e ∈ E ∨ e ∈ E ∧ e ∈ I ∧ e ∈ X ↔ (e ∈ X ∨ e ∈ E ∧ e ∉ I) ∧ e ∈ E
Tactic:
tauto
Proof state after:
no goals
Theorem: Matroid.Indep.interBasis_biInter
Proof state before:
α : Type u_1
ι✝ : Type u_2
M : Matroid α
F I J X✝ Y B C R : Set α
e f x y : α
Xs Ys : Set (Set α)
ι : Type u_3
hI : M.Indep I
X : ι → Set α
A : Set ι
hA : A.Nonempty
h : ∀ i ∈ A, M.Basis (X i ∩ I) (X i)
⊢ M.Basis ((⋂ i ∈ A, X i) ∩ I) (⋂ i ∈ A, X i)
Tactic:
refine (hI.inter_left _).basis_of_subset_of_subset_cl inter_subset_left ?_
Proof state after:
α : Type u_1
ι✝ : Type u_2
M : Matroid α
F I J X✝ Y B C R : Set α
e f x y : α
Xs Ys : Set (Set α)
ι : Type u_3
hI : M.Indep I
X : ι → Set α
A : Set ι
hA : A.Nonempty
h : ∀ i ∈ A, M.Basis (X i ∩ I) (X i)
⊢ ⋂ i ∈ A, X i ⊆ M.cl ((⋂ i ∈ A, X i) ∩ I)
Theorem: Matroid.Indep.interBasis_biInter
Proof state before:
α : Type u_1
ι✝ : Type u_2
M : Matroid α
F I J X✝ Y B C R : Set α
e f x y : α
Xs Ys : Set (Set α)
ι : Type u_3
hI : M.Indep I
X : ι → Set α
A : Set ι
hA : A.Nonempty
h : ∀ i ∈ A, M.Basis (X i ∩ I) (X i)
⊢ ⋂ i ∈ A, X i ⊆ M.cl ((⋂ i ∈ A, X i) ∩ I)
Tactic:
simp_rw [biInter_distrib_inter _ hA,
  cl_biInter_eq_biInter_cl_of_biUnion_indep hA (I := fun i ↦ (X i) ∩ I) (hI.subset (by simp)),
  subset_iInter_iff]
Proof state after:
α : Type u_1
ι✝ : Type u_2
M : Matroid α
F I J X✝ Y B C R : Set α
e f x y : α
Xs Ys : Set (Set α)
ι : Type u_3
hI : M.Indep I
X : ι → Set α
A : Set ι
hA : A.Nonempty
h : ∀ i ∈ A, M.Basis (X i ∩ I) (X i)
⊢ ∀ i ∈ A, ⋂ i ∈ A, X i ⊆ M.cl (X i ∩ I)
Theorem: Matroid.Indep.interBasis_biInter
Proof state before:
α : Type u_1
ι✝ : Type u_2
M : Matroid α
F I J X✝ Y B C R : Set α
e f x y : α
Xs Ys : Set (Set α)
ι : Type u_3
hI : M.Indep I
X : ι → Set α
A : Set ι
hA : A.Nonempty
h : ∀ i ∈ A, M.Basis (X i ∩ I) (X i)
⊢ ∀ i ∈ A, ⋂ i ∈ A, X i ⊆ M.cl (X i ∩ I)
Tactic:
exact fun i hiA ↦ (biInter_subset_of_mem hiA).trans (h i hiA).subset_cl
Proof state after:
no goals
Theorem: Matroid.Indep.interBasis_biInter
Proof state before:
α : Type u_1
ι✝ : Type u_2
M : Matroid α
F I J X✝ Y B C R : Set α
e f x y : α
Xs Ys : Set (Set α)
ι : Type u_3
hI : M.Indep I
X : ι → Set α
A : Set ι
hA : A.Nonempty
h : ∀ i ∈ A, M.Basis (X i ∩ I) (X i)
⊢ ⋃ i ∈ A, (fun i => X i ∩ I) i ⊆ I
Tactic:
simp
Proof state after:
no goals
Theorem: Matroid.Indep.interBasis_iInter
Proof state before:
α : Type u_1
ι✝ : Type u_2
M : Matroid α
F I J X✝ Y B C R : Set α
e f x y : α
Xs Ys : Set (Set α)
ι : Type u_3
inst✝ : Nonempty ι
X : ι → Set α
hI : M.Indep I
h : ∀ (i : ι), M.Basis (X i ∩ I) (X i)
⊢ M.Basis ((⋂ i, X i) ∩ I) (⋂ i, X i)
Tactic:
rw [← biInter_univ]
Proof state after:
α : Type u_1
ι✝ : Type u_2
M : Matroid α
F I J X✝ Y B C R : Set α
e f x y : α
Xs Ys : Set (Set α)
ι : Type u_3
inst✝ : Nonempty ι
X : ι → Set α
hI : M.Indep I
h : ∀ (i : ι), M.Basis (X i ∩ I) (X i)
⊢ M.Basis ((⋂ x ∈ univ, X x) ∩ I) (⋂ x ∈ univ, X x)
Theorem: Matroid.Indep.interBasis_iInter
Proof state before:
α : Type u_1
ι✝ : Type u_2
M : Matroid α
F I J X✝ Y B C R : Set α
e f x y : α
Xs Ys : Set (Set α)
ι : Type u_3
inst✝ : Nonempty ι
X : ι → Set α
hI : M.Indep I
h : ∀ (i : ι), M.Basis (X i ∩ I) (X i)
⊢ M.Basis ((⋂ x ∈ univ, X x) ∩ I) (⋂ x ∈ univ, X x)
Tactic:
exact hI.interBasis_biInter (by simp) (by simpa)
Proof state after:
no goals
Theorem: Matroid.Indep.interBasis_iInter
Proof state before:
α : Type u_1
ι✝ : Type u_2
M : Matroid α
F I J X✝ Y B C R : Set α
e f x y : α
Xs Ys : Set (Set α)
ι : Type u_3
inst✝ : Nonempty ι
X : ι → Set α
hI : M.Indep I
h : ∀ (i : ι), M.Basis (X i ∩ I) (X i)
⊢ univ.Nonempty
Tactic:
simp
Proof state after:
no goals
Theorem: Matroid.Indep.interBasis_iInter
Proof state before:
α : Type u_1
ι✝ : Type u_2
M : Matroid α
F I J X✝ Y B C R : Set α
e f x y : α
Xs Ys : Set (Set α)
ι : Type u_3
inst✝ : Nonempty ι
X : ι → Set α
hI : M.Indep I
h : ∀ (i : ι), M.Basis (X i ∩ I) (X i)
⊢ ∀ i ∈ univ, M.Basis (X i ∩ I) (X i)
Tactic:
simpa
Proof state after:
no goals
Theorem: Matroid.Indep.interBasis_sInter
Proof state before:
α : Type u_1
ι✝ : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e f x y : α
Xs Ys : Set (Set α)
ι : Type u_3
hI : M.Indep I
hXs : Xs.Nonempty
h : ∀ X ∈ Xs, M.Basis (X ∩ I) X
⊢ M.Basis (⋂₀ Xs ∩ I) (⋂₀ Xs)
Tactic:
rw [sInter_eq_biInter]
Proof state after:
α : Type u_1
ι✝ : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e f x y : α
Xs Ys : Set (Set α)
ι : Type u_3
hI : M.Indep I
hXs : Xs.Nonempty
h : ∀ X ∈ Xs, M.Basis (X ∩ I) X
⊢ M.Basis ((⋂ i ∈ Xs, i) ∩ I) (⋂ i ∈ Xs, i)
Theorem: Matroid.Indep.interBasis_sInter
Proof state before:
α : Type u_1
ι✝ : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e f x y : α
Xs Ys : Set (Set α)
ι : Type u_3
hI : M.Indep I
hXs : Xs.Nonempty
h : ∀ X ∈ Xs, M.Basis (X ∩ I) X
⊢ M.Basis ((⋂ i ∈ Xs, i) ∩ I) (⋂ i ∈ Xs, i)
Tactic:
exact hI.interBasis_biInter hXs h
Proof state after:
no goals
Theorem: Matroid.Basis.cl_inter_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 : α
Xs Ys : Set (Set α)
ι : Type u_3
h : M.Basis (X ∩ I) X
hI : M.Indep I
⊢ M.Basis (M.cl X ∩ I) (M.cl X)
Tactic:
rw [hI.inter_basis_cl_iff_subset_cl_inter] at 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 : α
Xs Ys : Set (Set α)
ι : Type u_3
h : X ⊆ M.cl (X ∩ I)
hI : M.Indep I
⊢ M.cl X ⊆ M.cl (M.cl X ∩ I)