internlm/Lean-Github huggingface dataset:
Theorem: Matroid.cl_iUnion_cl_eq_cl_iUnion
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 α
Xs : ι → Set α
⊢ M.cl (⋃ i, Xs i) ⊆ M.cl (⋃ i, M.cl (Xs i))
Tactic:
rw [← cl_inter_ground, iUnion_inter]
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 : Matroid α
Xs : ι → Set α
⊢ M.cl (⋃ i, Xs i ∩ M.E) ⊆ M.cl (⋃ i, M.cl (Xs i))
Theorem: Matroid.cl_iUnion_cl_eq_cl_iUnion
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 α
Xs : ι → Set α
⊢ M.cl (⋃ i, Xs i ∩ M.E) ⊆ M.cl (⋃ i, M.cl (Xs i))
Tactic:
refine' M.cl_subset_cl (iUnion_subset (fun i ↦ (M.subset_cl _).trans _))
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 : Matroid α
Xs : ι → Set α
i : ι
⊢ M.cl (Xs i ∩ M.E) ⊆ ⋃ i, M.cl (Xs i)
Theorem: Matroid.cl_iUnion_cl_eq_cl_iUnion
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 α
Xs : ι → Set α
i : ι
⊢ M.cl (Xs i ∩ M.E) ⊆ ⋃ i, M.cl (Xs i)
Tactic:
rw [cl_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 : Matroid α
Xs : ι → Set α
i : ι
⊢ M.cl (Xs i) ⊆ ⋃ i, M.cl (Xs i)
Theorem: Matroid.cl_iUnion_cl_eq_cl_iUnion
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 α
Xs : ι → Set α
i : ι
⊢ M.cl (Xs i) ⊆ ⋃ i, M.cl (Xs i)
Tactic:
exact subset_iUnion (fun i ↦ M.cl (Xs i)) i
Proof state after:
no goals
Theorem: Matroid.cl_iUnion_congr
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
Xs Ys : ι → Set α
h : ∀ (i : ι), M.cl (Xs i) = M.cl (Ys i)
⊢ M.cl (⋃ i, Xs i) = M.cl (⋃ i, Ys i)
Tactic:
rw [← M.cl_iUnion_cl_eq_cl_iUnion]
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
Xs Ys : ι → Set α
h : ∀ (i : ι), M.cl (Xs i) = M.cl (Ys i)
⊢ M.cl (⋃ i, M.cl (Xs i)) = M.cl (⋃ i, Ys i)
Theorem: Matroid.cl_iUnion_congr
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
Xs Ys : ι → Set α
h : ∀ (i : ι), M.cl (Xs i) = M.cl (Ys i)
⊢ M.cl (⋃ i, M.cl (Xs i)) = M.cl (⋃ i, Ys i)
Tactic:
simp [h, M.cl_iUnion_cl_eq_cl_iUnion]
Proof state after:
no goals
Theorem: Matroid.cl_biUnion_cl_eq_cl_sUnion
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 α
Xs : Set (Set α)
⊢ M.cl (⋃ X ∈ Xs, M.cl X) = M.cl (⋃₀ Xs)
Tactic:
rw [sUnion_eq_iUnion, biUnion_eq_iUnion, cl_iUnion_cl_eq_cl_iUnion]
Proof state after:
no goals
Theorem: Matroid.cl_biUnion_cl_eq_cl_biUnion
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 α
Xs : ι → Set α
A : Set ι
⊢ M.cl (⋃ i ∈ A, M.cl (Xs i)) = M.cl (⋃ i ∈ A, Xs i)
Tactic:
rw [biUnion_eq_iUnion, M.cl_iUnion_cl_eq_cl_iUnion, biUnion_eq_iUnion]
Proof state after:
no goals
Theorem: Matroid.cl_biUnion_congr
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 α
Xs Ys : ι → Set α
A : Set ι
h : ∀ i ∈ A, M.cl (Xs i) = M.cl (Ys i)
⊢ M.cl (⋃ i ∈ A, Xs i) = M.cl (⋃ i ∈ A, Ys i)
Tactic:
rw [← cl_biUnion_cl_eq_cl_biUnion, iUnion₂_congr h, cl_biUnion_cl_eq_cl_biUnion]
Proof state after:
no goals
Theorem: Matroid.cl_cl_union_cl_eq_cl_union
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 Y : Set α
⊢ M.cl (M.cl X ∪ M.cl Y) = M.cl (X ∪ Y)
Tactic:
rw [eq_comm, union_eq_iUnion, ← cl_iUnion_cl_eq_cl_iUnion, union_eq_iUnion]
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 : Matroid α
X Y : Set α
⊢ M.cl (⋃ i, M.cl (bif i then X else Y)) = M.cl (⋃ b, bif b then M.cl X else M.cl Y)
Theorem: Matroid.cl_cl_union_cl_eq_cl_union
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 Y : Set α
⊢ M.cl (⋃ i, M.cl (bif i then X else Y)) = M.cl (⋃ b, bif b then M.cl X else M.cl Y)
Tactic:
simp_rw [Bool.cond_eq_ite, apply_ite]
Proof state after:
no goals
Theorem: Matroid.cl_union_cl_right_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 : α
M : Matroid α
X Y : Set α
⊢ M.cl (X ∪ M.cl Y) = M.cl (X ∪ Y)
Tactic:
rw [← cl_cl_union_cl_eq_cl_union, cl_cl, cl_cl_union_cl_eq_cl_union]
Proof state after:
no goals
Theorem: Matroid.cl_union_cl_left_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 : α
M : Matroid α
X Y : Set α
⊢ M.cl (M.cl X ∪ Y) = M.cl (X ∪ Y)
Tactic:
rw [← cl_cl_union_cl_eq_cl_union, cl_cl, cl_cl_union_cl_eq_cl_union]
Proof state after:
no goals
Theorem: Matroid.cl_insert_cl_eq_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 : α
M : Matroid α
e : α
X : Set α
⊢ M.cl (insert e (M.cl X)) = M.cl (insert e X)
Tactic:
simp_rw [← singleton_union, cl_union_cl_right_eq]
Proof state after:
no goals
Theorem: Matroid.cl_insert_eq_of_mem_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 : α
he : e ∈ M.cl X
⊢ M.cl (insert e X) = M.cl X
Tactic:
rw [← cl_insert_cl_eq_cl_insert, insert_eq_of_mem he, cl_cl]
Proof state after:
no goals
Theorem: Matroid.Indep.cl_eq_setOf_basis_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 : α
hI : M.Indep I
⊢ M.cl I = {x | M.Basis I (insert x I)}
Tactic:
set F := {x | M.Basis I (insert x I)}
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.Indep I
F : Set α := {x | M.Basis I (insert x I)}
⊢ M.cl I = F
Theorem: Matroid.Indep.cl_eq_setOf_basis_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 : α
hI : M.Indep I
F : Set α := {x | M.Basis I (insert x I)}
⊢ M.cl I = F
Tactic:
have hIF : M.Basis I F := hI.basis_setOf_insert_basis
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.Indep I
F : Set α := {x | M.Basis I (insert x I)}
hIF : M.Basis I F
⊢ M.cl I = F
Theorem: Matroid.Indep.cl_eq_setOf_basis_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 : α
hI : M.Indep I
F : Set α := {x | M.Basis I (insert x I)}
hIF : M.Basis I F
⊢ M.cl I = F
Tactic:
have hF : M.Flat F := by
  refine' ⟨fun J X hJF hJX e heX ↦ (_ : M.Basis _ _), hIF.subset_ground⟩
  exact (hIF.basis_of_basis_of_subset_of_subset (hJX.basis_union hJF) hJF.subset
    (hIF.subset.trans subset_union_right)).basis_subset (subset_insert _ _)
    (insert_subset (Or.inl heX) (hIF.subset.trans subset_union_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.Indep I
F : Set α := {x | M.Basis I (insert x I)}
hIF : M.Basis I F
hF : M.Flat F
⊢ M.cl I = F
Theorem: Matroid.Indep.cl_eq_setOf_basis_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 : α
hI : M.Indep I
F : Set α := {x | M.Basis I (insert x I)}
hIF : M.Basis I F
hF : M.Flat F
⊢ M.cl I = F
Tactic:
rw [subset_antisymm_iff, cl_def, subset_sInter_iff, and_iff_right (sInter_subset_of_mem _)]
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.Indep I
F : Set α := {x | M.Basis I (insert x I)}
hIF : M.Basis I F
hF : M.Flat F
⊢ ∀ t' ∈ {F | M.Flat F ∧ I ∩ M.E ⊆ F}, F ⊆ t'

α : Type u_1
ι : Type u_2
M : Matroid α
F✝ I J X Y B C R : Set α
e f x y : α
hI : M.Indep I
F : Set α := {x | M.Basis I (insert x I)}
hIF : M.Basis I F
hF : M.Flat F
⊢ F ∈ {F | M.Flat F ∧ I ∩ M.E ⊆ F}
Theorem: Matroid.Indep.cl_eq_setOf_basis_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 : α
hI : M.Indep I
F : Set α := {x | M.Basis I (insert x I)}
hIF : M.Basis I F
hF : M.Flat F
⊢ F ∈ {F | M.Flat F ∧ I ∩ M.E ⊆ F}
Tactic:
exact ⟨hF, inter_subset_left.trans hIF.subset⟩
Proof state after:
no goals
Theorem: Matroid.Indep.cl_eq_setOf_basis_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 : α
hI : M.Indep I
F : Set α := {x | M.Basis I (insert x I)}
hIF : M.Basis I F
⊢ M.Flat F
Tactic:
refine' ⟨fun J X hJF hJX e heX ↦ (_ : M.Basis _ _), hIF.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 : α
hI : M.Indep I
F : Set α := {x | M.Basis I (insert x I)}
hIF : M.Basis I F
J X : Set α
hJF : M.Basis J F
hJX : M.Basis J X
e : α
heX : e ∈ X
⊢ M.Basis I (insert e I)
Theorem: Matroid.Indep.cl_eq_setOf_basis_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 : α
hI : M.Indep I
F : Set α := {x | M.Basis I (insert x I)}
hIF : M.Basis I F
J X : Set α
hJF : M.Basis J F
hJX : M.Basis J X
e : α
heX : e ∈ X
⊢ M.Basis I (insert e I)
Tactic:
exact (hIF.basis_of_basis_of_subset_of_subset (hJX.basis_union hJF) hJF.subset
  (hIF.subset.trans subset_union_right)).basis_subset (subset_insert _ _)
  (insert_subset (Or.inl heX) (hIF.subset.trans subset_union_right))
Proof state after:
no goals
Theorem: Matroid.Indep.cl_eq_setOf_basis_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 : α
hI : M.Indep I
F : Set α := {x | M.Basis I (insert x I)}
hIF : M.Basis I F
hF : M.Flat F
⊢ ∀ t' ∈ {F | M.Flat F ∧ I ∩ M.E ⊆ F}, F ⊆ t'
Tactic:
rintro F' ⟨hF', hIF'⟩ e (he : M.Basis I (insert e I))
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 : α
hI : M.Indep I
F : Set α := {x | M.Basis I (insert x I)}
hIF : M.Basis I F
hF : M.Flat F
F' : Set α
hF' : M.Flat F'
hIF' : I ∩ M.E ⊆ F'
e : α
he : M.Basis I (insert e I)
⊢ e ∈ F'
Theorem: Matroid.Indep.cl_eq_setOf_basis_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 : α
hI : M.Indep I
F : Set α := {x | M.Basis I (insert x I)}
hIF : M.Basis I F
hF : M.Flat F
F' : Set α
hF' : M.Flat F'
hIF' : I ∩ M.E ⊆ F'
e : α
he : M.Basis I (insert e I)
⊢ e ∈ F'
Tactic:
rw [inter_eq_left.mpr (hIF.subset.trans hIF.subset_ground)] at hIF'
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 : α
hI : M.Indep I
F : Set α := {x | M.Basis I (insert x I)}
hIF : M.Basis I F
hF : M.Flat F
F' : Set α
hF' : M.Flat F'
hIF' : I ⊆ F'
e : α
he : M.Basis I (insert e I)
⊢ e ∈ F'
Theorem: Matroid.Indep.cl_eq_setOf_basis_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 : α
hI : M.Indep I
F : Set α := {x | M.Basis I (insert x I)}
hIF : M.Basis I F
hF : M.Flat F
F' : Set α
hF' : M.Flat F'
hIF' : I ⊆ F'
e : α
he : M.Basis I (insert e I)
⊢ e ∈ F'
Tactic:
obtain ⟨J, hJ, hIJ⟩ := hI.subset_basis_of_subset hIF' hF'.2
Proof state after:
case intro.intro.intro
α : Type u_1
ι : Type u_2
M : Matroid α
F✝ I J✝ X Y B C R : Set α
e✝ f x y : α
hI : M.Indep I
F : Set α := {x | M.Basis I (insert x I)}
hIF : M.Basis I F
hF : M.Flat F
F' : Set α
hF' : M.Flat F'
hIF' : I ⊆ F'
e : α
he : M.Basis I (insert e I)
J : Set α
hJ : M.Basis J F'
hIJ : I ⊆ J
⊢ e ∈ F'
Theorem: Matroid.Indep.cl_eq_setOf_basis_insert
Proof state before:
case intro.intro.intro
α : Type u_1
ι : Type u_2
M : Matroid α
F✝ I J✝ X Y B C R : Set α
e✝ f x y : α
hI : M.Indep I
F : Set α := {x | M.Basis I (insert x I)}
hIF : M.Basis I F
hF : M.Flat F
F' : Set α
hF' : M.Flat F'
hIF' : I ⊆ F'
e : α
he : M.Basis I (insert e I)
J : Set α
hJ : M.Basis J F'
hIJ : I ⊆ J
⊢ e ∈ F'
Tactic:
exact (hF'.1 hJ (he.basis_union_of_subset hJ.indep hIJ)) (Or.inr (mem_insert _ _))
Proof state after:
no goals
Theorem: Matroid.Indep.insert_basis_iff_mem_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.Indep I
⊢ M.Basis I (insert e I) ↔ e ∈ M.cl I
Tactic:
rw [hI.cl_eq_setOf_basis_insert, mem_setOf]
Proof state after:
no goals
Theorem: Matroid.Indep.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 : α
hI : M.Indep I
⊢ M.Basis I (M.cl I)
Tactic:
rw [hI.cl_eq_setOf_basis_insert]
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.Indep I
⊢ M.Basis I {x | M.Basis I (insert x I)}
Theorem: Matroid.Indep.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 : α
hI : M.Indep I
⊢ M.Basis I {x | M.Basis I (insert x I)}
Tactic:
exact hI.basis_setOf_insert_basis
Proof state after:
no goals
Theorem: Matroid.Basis.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 : α
h : M.Basis I X
⊢ M.cl I = M.cl X
Tactic:
refine' subset_antisymm (M.cl_subset_cl h.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 : α
h : M.Basis I X
⊢ M.cl X ⊆ M.cl I
Theorem: Matroid.Basis.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 : α
h : M.Basis I X
⊢ M.cl X ⊆ M.cl I
Tactic:
rw [← M.cl_cl I, h.indep.cl_eq_setOf_basis_insert]
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.Basis I X
⊢ M.cl X ⊆ M.cl {x | M.Basis I (insert x I)}
Theorem: Matroid.Basis.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 : α
h : M.Basis I X
⊢ M.cl X ⊆ M.cl {x | M.Basis I (insert x I)}
Tactic:
exact M.cl_subset_cl fun e he ↦ (h.basis_subset (subset_insert _ _) (insert_subset he h.subset))
Proof state after:
no goals
Theorem: Matroid.Basis'.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 : α
h : M.Basis' I X
⊢ M.cl I = M.cl X
Tactic:
rw [← cl_inter_ground _ X, h.basis_inter_ground.cl_eq_cl]
Proof state after:
no goals
Theorem: Matroid.Basis.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 : α
h : M.Basis I X
⊢ X ⊆ M.cl I
Tactic:
rw [← cl_subset_cl_iff_subset_cl, h.cl_eq_cl]
Proof state after:
no goals
Theorem: Matroid.Basis'.basis_cl_right
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.Basis' I X
⊢ M.Basis I (M.cl X)
Tactic:
rw [← h.cl_eq_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 : α
h : M.Basis' I X
⊢ M.Basis I (M.cl I)
Theorem: Matroid.Basis'.basis_cl_right
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.Basis' I X
⊢ M.Basis I (M.cl I)
Tactic:
exact h.indep.basis_cl
Proof state after:
no goals
Theorem: Matroid.Indep.mem_cl_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 : α
hI : M.Indep I
⊢ x ∈ M.cl I ↔ M.Dep (insert x I) ∨ x ∈ I
Tactic:
rwa [hI.cl_eq_setOf_basis_insert, mem_setOf, basis_insert_iff]
Proof state after:
no goals
Theorem: Matroid.Indep.mem_cl_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 : α
hI : M.Indep I
⊢ x ∈ M.cl I ↔ x ∈ M.E ∧ (M.Indep (insert x I) → x ∈ I)
Tactic:
rw [hI.mem_cl_iff, dep_iff, insert_subset_iff, and_iff_left hI.subset_ground,
  imp_iff_not_or]
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.Indep I
⊢ ¬M.Indep (insert x I) ∧ x ∈ M.E ∨ x ∈ I ↔ x ∈ M.E ∧ (¬M.Indep (insert x I) ∨ x ∈ I)
Theorem: Matroid.Indep.mem_cl_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 : α
hI : M.Indep I
⊢ ¬M.Indep (insert x I) ∧ x ∈ M.E ∨ x ∈ I ↔ x ∈ M.E ∧ (¬M.Indep (insert x I) ∨ x ∈ I)
Tactic:
have := hI.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 : α
hI : M.Indep I
this : I ⊆ M.E
⊢ ¬M.Indep (insert x I) ∧ x ∈ M.E ∨ x ∈ I ↔ x ∈ M.E ∧ (¬M.Indep (insert x I) ∨ x ∈ I)
Theorem: Matroid.Indep.mem_cl_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 : α
hI : M.Indep I
this : I ⊆ M.E
⊢ ¬M.Indep (insert x I) ∧ x ∈ M.E ∨ x ∈ I ↔ x ∈ M.E ∧ (¬M.Indep (insert x I) ∨ x ∈ I)
Tactic:
aesop
Proof state after:
no goals
Theorem: Matroid.Indep.insert_dep_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 : α
hI : M.Indep I
⊢ M.Dep (insert e I) ↔ e ∈ M.cl I \ I
Tactic:
rw [mem_diff, hI.mem_cl_iff, or_and_right, and_not_self_iff, or_false,
  iff_self_and, imp_not_comm]
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.Indep I
⊢ e ∈ I → ¬M.Dep (insert e I)
Theorem: Matroid.Indep.insert_dep_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 : α
hI : M.Indep I
⊢ e ∈ I → ¬M.Dep (insert e I)
Tactic:
intro heI
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.Indep I
heI : e ∈ I
⊢ ¬M.Dep (insert e I)
Theorem: Matroid.Indep.insert_dep_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 : α
hI : M.Indep I
heI : e ∈ I
⊢ ¬M.Dep (insert e I)
Tactic:
rw [insert_eq_of_mem heI]
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.Indep I
heI : e ∈ I
⊢ ¬M.Dep I
Theorem: Matroid.Indep.insert_dep_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 : α
hI : M.Indep I
heI : e ∈ I
⊢ ¬M.Dep I
Tactic:
exact hI.not_dep
Proof state after:
no goals
Theorem: Matroid.Indep.mem_cl_iff_of_not_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 : α
hI : M.Indep I
heI : e ∉ I
⊢ e ∈ M.cl I ↔ M.Dep (insert e I)
Tactic:
rw [hI.insert_dep_iff, mem_diff, and_iff_left heI]
Proof state after:
no goals
Theorem: Matroid.Indep.not_mem_cl_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 : α
hI : M.Indep I
he : autoParam (e ∈ M.E) _auto✝
⊢ e ∉ M.cl I ↔ M.Indep (insert e I) ∧ e ∉ I
Tactic:
rw [hI.mem_cl_iff, dep_iff, insert_subset_iff, and_iff_right he,
  and_iff_left hI.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 : α
hI : M.Indep I
he : autoParam (e ∈ M.E) _auto✝
⊢ ¬(¬M.Indep (insert e I) ∨ e ∈ I) ↔ M.Indep (insert e I) ∧ e ∉ I
Theorem: Matroid.Indep.not_mem_cl_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 : α
hI : M.Indep I
he : autoParam (e ∈ M.E) _auto✝
⊢ ¬(¬M.Indep (insert e I) ∨ e ∈ I) ↔ M.Indep (insert e I) ∧ e ∉ I
Tactic:
tauto
Proof state after:
no goals
Theorem: Matroid.Indep.not_mem_cl_iff_of_not_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 : α
hI : M.Indep I
heI : e ∉ I
he : autoParam (e ∈ M.E) _auto✝
⊢ e ∉ M.cl I ↔ M.Indep (insert e I)
Tactic:
rw [hI.not_mem_cl_iff, and_iff_left heI]
Proof state after:
no goals
Theorem: Matroid.Indep.insert_indep_iff_of_not_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 : α
hI : M.Indep I
heI : e ∉ I
⊢ M.Indep (insert e I) ↔ e ∈ M.E \ M.cl I
Tactic:
rw [mem_diff, hI.mem_cl_iff_of_not_mem heI, dep_iff, not_and, not_imp_not, insert_subset_iff,
  and_iff_left hI.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 : α
hI : M.Indep I
heI : e ∉ I
⊢ M.Indep (insert e I) ↔ e ∈ M.E ∧ (e ∈ M.E → M.Indep (insert e I))
Theorem: Matroid.Indep.insert_indep_iff_of_not_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 : α
hI : M.Indep I
heI : e ∉ I
⊢ M.Indep (insert e I) ↔ e ∈ M.E ∧ (e ∈ M.E → M.Indep (insert e I))
Tactic:
exact ⟨fun h ↦ ⟨h.subset_ground (mem_insert e I), fun _ ↦ h⟩, fun h ↦ h.2 h.1⟩
Proof state after:
no goals
Theorem: Matroid.Indep.insert_indep_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 : α
hI : M.Indep I
⊢ M.Indep (insert e I) ↔ e ∈ M.E \ M.cl I ∨ e ∈ I
Tactic:
obtain (h | h) := em (e ∈ I)
Proof state after:
case inl
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e f x y : α
hI : M.Indep I
h : e ∈ I
⊢ M.Indep (insert e I) ↔ e ∈ M.E \ M.cl I ∨ e ∈ I

case inr
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e f x y : α
hI : M.Indep I
h : e ∉ I
⊢ M.Indep (insert e I) ↔ e ∈ M.E \ M.cl I ∨ e ∈ I
Theorem: Matroid.Indep.insert_indep_iff
Proof state before:
case inr
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e f x y : α
hI : M.Indep I
h : e ∉ I
⊢ M.Indep (insert e I) ↔ e ∈ M.E \ M.cl I ∨ e ∈ I
Tactic:
rw [hI.insert_indep_iff_of_not_mem h, or_iff_left h]
Proof state after:
no goals
Theorem: Matroid.Indep.insert_indep_iff
Proof state before:
case inl
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e f x y : α
hI : M.Indep I
h : e ∈ I
⊢ M.Indep (insert e I) ↔ e ∈ M.E \ M.cl I ∨ e ∈ I
Tactic:
simp_rw [insert_eq_of_mem h, iff_true_intro hI, true_iff, iff_true_intro h, or_true]
Proof state after:
no goals
Theorem: Matroid.insert_indep_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.Indep (insert e I) ↔ M.Indep I ∧ (e ∉ I → e ∈ M.E \ M.cl I)
Tactic:
by_cases hI : M.Indep I
Proof state after:
case pos
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e f x y : α
hI : M.Indep I
⊢ M.Indep (insert e I) ↔ M.Indep I ∧ (e ∉ I → e ∈ M.E \ M.cl I)

case neg
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e f x y : α
hI : ¬M.Indep I
⊢ M.Indep (insert e I) ↔ M.Indep I ∧ (e ∉ I → e ∈ M.E \ M.cl I)
Theorem: Matroid.insert_indep_iff
Proof state before:
case neg
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e f x y : α
hI : ¬M.Indep I
⊢ M.Indep (insert e I) ↔ M.Indep I ∧ (e ∉ I → e ∈ M.E \ M.cl I)
Tactic:
simp [hI, show ¬ M.Indep (insert e I) from fun h ↦ hI <| h.subset <| subset_insert _ _]
Proof state after:
no goals
Theorem: Matroid.insert_indep_iff
Proof state before:
case pos
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e f x y : α
hI : M.Indep I
⊢ M.Indep (insert e I) ↔ M.Indep I ∧ (e ∉ I → e ∈ M.E \ M.cl I)
Tactic:
rw [hI.insert_indep_iff, and_iff_right hI, or_iff_not_imp_right]
Proof state after:
no goals
Theorem: Matroid.Indep.insert_diff_indep_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 : α
hI : M.Indep (I \ {e})
heI : e ∈ I
⊢ M.Indep (insert f I \ {e}) ↔ f ∈ M.E \ M.cl (I \ {e}) ∨ f ∈ I
Tactic:
obtain (rfl | hne) := eq_or_ne e f
Proof state after:
case inl
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e x y : α
hI : M.Indep (I \ {e})
heI : e ∈ I
⊢ M.Indep (insert e I \ {e}) ↔ e ∈ M.E \ M.cl (I \ {e}) ∨ e ∈ I

case inr
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e f x y : α
hI : M.Indep (I \ {e})
heI : e ∈ I
hne : e ≠ f
⊢ M.Indep (insert f I \ {e}) ↔ f ∈ M.E \ M.cl (I \ {e}) ∨ f ∈ I
Theorem: Matroid.Indep.insert_diff_indep_iff
Proof state before:
case inr
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e f x y : α
hI : M.Indep (I \ {e})
heI : e ∈ I
hne : e ≠ f
⊢ M.Indep (insert f I \ {e}) ↔ f ∈ M.E \ M.cl (I \ {e}) ∨ f ∈ I
Tactic:
rw [← insert_diff_singleton_comm hne.symm, hI.insert_indep_iff, mem_diff_singleton,
  and_iff_left hne.symm]
Proof state after:
no goals
Theorem: Matroid.Indep.insert_diff_indep_iff
Proof state before:
case inl
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e x y : α
hI : M.Indep (I \ {e})
heI : e ∈ I
⊢ M.Indep (insert e I \ {e}) ↔ e ∈ M.E \ M.cl (I \ {e}) ∨ e ∈ I
Tactic:
simp [hI, heI]
Proof state after:
no goals
Theorem: Matroid.Indep.base_of_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 : α
hI : M.Indep I
h : M.E ⊆ M.cl I
⊢ M.Base I
Tactic:
rw [← basis_ground_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 : α
hI : M.Indep I
h : M.E ⊆ M.cl I
⊢ M.Basis I M.E