awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
X : Set α
e f : α
he : e ∉ M.closure (X ∩ M.E)
hef : e ∈ M.closure (insert f X ∩ M.E)
hfE : f ∈ M.E
⊢ e ∈ M.E

Tactic:
have heE : e ∈ M.E := (M.closure_subset_ground _) hef
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
X : Set α
e f : α
he : e ∉ M.closure (X ∩ M.E)
hef : e ∈ M.closure (insert f X ∩ M.E)
hfE : f ∈ M.E
heE : e ∈ M.E
⊢ e ∈ M.closure (insert f (X ∩ M.E))

Tactic:
rw [insert_inter_of_mem hfE] at hef

Premises used: Set.insert_inter_of_mem
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
X : Set α
e f : α
he : e ∉ M.closure (X ∩ M.E)
hef : e ∈ M.closure (insert f X ∩ M.E)
hfE : f ∈ M.E
heE : e ∈ M.E
hef₁ : e ∈ M.closure (insert f (X ∩ M.E))
⊢ f ∈ M.E

Tactic:
rw [insert_inter_of_mem hfE] at hef

Premises used: Set.insert_inter_of_mem
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
X : Set α
e f : α
he : e ∉ M.closure (X ∩ M.E)
hef : e ∈ M.closure (insert f X ∩ M.E)
hfE : f ∈ M.E
heE : e ∈ M.E
hef₁ : e ∈ M.closure (insert f (X ∩ M.E))
hfE₁ : f ∈ M.E
⊢ e ∈ M.E

Tactic:
rw [insert_inter_of_mem hfE] at hef

Premises used: Set.insert_inter_of_mem
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
X : Set α
e f : α
he : e ∉ M.closure (X ∩ M.E)
hef : e ∈ M.closure (insert f (X ∩ M.E))
hfE : f ∈ M.E
heE : e ∈ M.E
rw : f ∈ M.closure (insert e (X ∩ M.E))
⊢ f ∈ M.closure (insert e X ∩ M.E)

Tactic:
rw [insert_inter_of_mem heE]

Premises used: Set.insert_inter_of_mem
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
X : Set α
e f : α
he : e ∉ M.closure (X ∩ M.E)
hef : e ∈ M.closure (insert f (X ∩ M.E))
hfE : f ∈ M.E
heE : e ∈ M.E
obtain : ∀ (I : Set α) (hI : M.IsBasis I (X ∩ M.E)), f ∈ M.closure (insert e (X ∩ M.E))
⊢ f ∈ M.closure (insert e (X ∩ M.E))

Tactic:
obtain ⟨I, hI⟩ := M.exists_isBasis (X ∩ M.E)

Premises used: Matroid.E, Inter.inter, Matroid.exists_isBasis
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
X : Set α
e f : α
he : e ∉ M.closure (X ∩ M.E)
hef : e ∈ M.closure (insert f (X ∩ M.E))
hfE : f ∈ M.E
heE : e ∈ M.E
I : Set α
hI : M.IsBasis I (X ∩ M.E)
⊢ M.Indep (insert e I) ∧ e ∉ I

Tactic:
rw [← hI.closure_eq_closure, hI.indep.notMem_closure_iff] at he

Premises used: Matroid.Indep.notMem_closure_iff, Matroid.IsBasis.indep, Matroid.IsBasis.closure_eq_closure
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
X : Set α
e f : α
he : e ∉ M.closure (X ∩ M.E)
hef : e ∈ M.closure (insert f (X ∩ M.E))
hfE : f ∈ M.E
heE : e ∈ M.E
I : Set α
hI : M.IsBasis I (X ∩ M.E)
he₁ : M.Indep (insert e I) ∧ e ∉ I
⊢ M.IsBasis I (X ∩ M.E)

Tactic:
rw [← hI.closure_eq_closure, hI.indep.notMem_closure_iff] at he

Premises used: Matroid.Indep.notMem_closure_iff, Matroid.IsBasis.indep, Matroid.IsBasis.closure_eq_closure
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
X : Set α
e f : α
hef : e ∈ M.closure (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.IsBasis I (X ∩ M.E)
rw :
  ∀ (hfE : f ∈ M.E) (heE : e ∈ M.E) (I : Set α) (hef : e ∈ M.closure (insert f I)) (he : M.Indep (insert e I) ∧ e ∉ I)
    (hI : M.IsBasis I (X ∩ M.E)), M.Dep (insert f (insert e I)) ∨ f ∈ insert e I
⊢ f ∈ M.closure (insert e (X ∩ M.E))

Tactic:
rw [← closure_insert_closure_eq_closure_insert, ← hI.closure_eq_closure,
    closure_insert_closure_eq_closure_insert, he.1.mem_closure_iff] at *

Premises used: Matroid.Indep.mem_closure_iff, Matroid.closure_insert_closure_eq_closure_insert, And.left, Matroid.IsBasis.closure_eq_closure
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
X : Set α
e f : α
hfE : f ∈ M.E
heE : e ∈ M.E
I : Set α
hef : e ∈ M.closure (insert f I)
he : M.Indep (insert e I) ∧ e ∉ I
hI : M.IsBasis I (X ∩ M.E)
rw : M.Indep (insert e (insert f I)) → f ∈ insert e I
⊢ 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]

Premises used: Classical.not_not, and_iff_left, Set.insert_comm, Matroid.Indep.subset_ground, Classical.or_iff_not_imp_left, Matroid.IsBasis.indep, Set.insert_subset, Matroid.dep_iff
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
X : Set α
e f : α
hfE : f ∈ M.E
heE : e ∈ M.E
I : Set α
hef : e ∈ M.closure (insert f I)
he : M.Indep (insert e I) ∧ e ∉ I
hI : M.IsBasis I (X ∩ M.E)
h : M.Indep (insert e (insert f I))
⊢ e = f

Tactic:
rw [(h.subset (subset_insert _ _)).mem_closure_iff, or_iff_right (h.not_dep), mem_insert_iff,
    or_iff_left he.2] at hef

Premises used: Matroid.Indep.mem_closure_iff, Matroid.Indep.subset, And.right, or_iff_right, Set.mem_insert_iff, or_iff_left, Matroid.Indep.not_dep, Set.subset_insert
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
X : Set α
e f : α
hfE : f ∈ M.E
heE : e ∈ M.E
I : Set α
hef : e ∈ M.closure (insert f I)
he : M.Indep (insert e I) ∧ e ∉ I
hI : M.IsBasis I (X ∩ M.E)
h : M.Indep (insert e (insert f I))
hef₁ : e = f
⊢ M.Indep (insert e I) ∧ e ∉ I

Tactic:
rw [(h.subset (subset_insert _ _)).mem_closure_iff, or_iff_right (h.not_dep), mem_insert_iff,
    or_iff_left he.2] at hef

Premises used: Matroid.Indep.mem_closure_iff, Matroid.Indep.subset, And.right, or_iff_right, Set.mem_insert_iff, or_iff_left, Matroid.Indep.not_dep, Set.subset_insert
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
X : Set α
e f : α
hfE : f ∈ M.E
heE : e ∈ M.E
I : Set α
hef : e ∈ M.closure (insert f I)
he : M.Indep (insert e I) ∧ e ∉ I
hI : M.IsBasis I (X ∩ M.E)
h : M.Indep (insert e (insert f I))
hef₁ : e = f
he₁ : M.Indep (insert e I) ∧ e ∉ I
⊢ M.IsBasis I (X ∩ M.E)

Tactic:
rw [(h.subset (subset_insert _ _)).mem_closure_iff, or_iff_right (h.not_dep), mem_insert_iff,
    or_iff_left he.2] at hef

Premises used: Matroid.Indep.mem_closure_iff, Matroid.Indep.subset, And.right, or_iff_right, Set.mem_insert_iff, or_iff_left, Matroid.Indep.not_dep, Set.subset_insert
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
X : Set α
e f : α
hfE : f ∈ M.E
heE : e ∈ M.E
I : Set α
hef : e ∈ M.closure (insert f I)
he : M.Indep (insert e I) ∧ e ∉ I
hI : M.IsBasis I (X ∩ M.E)
h : M.Indep (insert e (insert f I))
hef₁ : e = f
he₁ : M.Indep (insert e I) ∧ e ∉ I
hI₁ : M.IsBasis I (X ∩ M.E)
⊢ M.Indep (insert e (insert f I))

Tactic:
rw [(h.subset (subset_insert _ _)).mem_closure_iff, or_iff_right (h.not_dep), mem_insert_iff,
    or_iff_left he.2] at hef

Premises used: Matroid.Indep.mem_closure_iff, Matroid.Indep.subset, And.right, or_iff_right, Set.mem_insert_iff, or_iff_left, Matroid.Indep.not_dep, Set.subset_insert
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
X : Set α
e f : α
hfE : f ∈ M.E
heE : e ∈ M.E
I : Set α
hef : e = f
he : M.Indep (insert e I) ∧ e ∉ I
hI : M.IsBasis I (X ∩ M.E)
h : M.Indep (insert e (insert f I))
subst : ∀ (hfE : e ∈ M.E) (h : M.Indep (insert e (insert e I))), e ∈ insert e I
⊢ f ∈ insert e I

Tactic:
subst hef
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
X : Set α
e : α
heE : e ∈ M.E
I : Set α
he : M.Indep (insert e I) ∧ e ∉ I
hI : M.IsBasis I (X ∩ M.E)
hfE : e ∈ M.E
h : M.Indep (insert e (insert e I))
⊢ e ∈ insert e I

Tactic:
apply mem_insert

Premises used: Set.mem_insert
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
X : Set α
e f : α
he : e ∈ M.closure (insert f X) \ M.closure X
hf : f ∈ M.closure X
rwa : ∀ (he : e ∈ M.closure X \ M.closure X) (hf : f ∈ M.closure X), False
rwa₁ : ∀ (he : Membership.mem (γ := Set α) ∅ e) (hf : f ∈ M.closure X), False
rwa₂ rwa₃ rwa₄ rwa₅ : ∀ (he : False) (hf : f ∈ M.closure X), False
⊢ False

Tactic:
rwa [closure_insert_eq_of_mem_closure hf, diff_self, iff_false_intro (notMem_empty _)] at he

Premises used: Matroid.closure_insert_eq_of_mem_closure, iff_false_intro, Set.notMem_empty, Set.diff_self
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
X : Set α
e f : α
⊢ e ∈ M.closure (insert f X) \ M.closure X ↔ f ∈ M.closure (insert e X) \ M.closure X

Tactic:
⟨closure_exchange, closure_exchange⟩

Premises used: Matroid.closure_exchange, Iff.intro
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
X : Set α
e f : α
he : e ∈ M.closure (insert f X) \ M.closure X
⊢ f ∈ M.closure (insert e X) \ M.closure X

Tactic:
have hf := closure_exchange he
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
X : Set α
e f : α
he : e ∈ M.closure (insert f X) \ M.closure X
hf : f ∈ M.closure (insert e X) \ M.closure X
rw : M.closure (insert f X) = M.closure (insert e X)
rw₁ : M.closure (M.closure (insert f X)) = M.closure (insert e X)
rw₂ : M.closure (insert e (M.closure (insert f X))) = M.closure (insert e X)
rw₃ : M.closure (insert e (insert f X)) = M.closure (insert e X)
rw₄ : M.closure (insert f (insert e X)) = M.closure (insert e X)
rw₅ : M.closure (M.closure (insert f (insert e X))) = M.closure (insert e X)
rw₆ : M.closure (M.closure (insert f (M.closure (insert e X)))) = M.closure (insert e X)
rw₇ : M.closure (M.closure (M.closure (insert e X))) = M.closure (insert e X)
rw₈ : M.closure (M.closure (insert e X)) = M.closure (insert e X)
rw₉ rw₁₀ : M.closure (insert e X) = M.closure (insert e X)
⊢ M.closure (insert e X) = M.closure (insert f X)

Tactic:
rw [eq_comm, ← closure_closure, ← insert_eq_of_mem he.1, closure_insert_closure_eq_closure_insert,
    insert_comm, ← closure_closure, ← closure_insert_closure_eq_closure_insert,
    insert_eq_of_mem hf.1, closure_closure, closure_closure]

Premises used: Matroid.closure_insert_closure_eq_closure_insert, Set.insert_eq_of_mem, Matroid.closure_closure, eq_comm, Set.insert_comm, And.left
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
X Y : Set α
h : Y ⊆ M.closure (X \ Y)
rw : M.closure ((X \ Y ∪ X ∩ Y) \ Y) = M.closure (X \ Y ∪ X ∩ Y)
rw₁ : M.closure ((X \ Y ∪ X ∩ Y) \ Y) = M.closure (M.closure (X \ Y) ∪ X ∩ Y)
rw₂ : M.closure ((X \ Y ∪ X ∩ Y) \ Y) = M.closure (M.closure (X \ Y))
rw₃ : M.closure ((X \ Y ∪ X ∩ Y) \ Y) = M.closure (X \ Y)
rw₄ rw₅ : M.closure (X \ Y) = M.closure (X \ Y)
⊢ M.closure (X \ Y) = M.closure X

Tactic:
rw [← diff_union_inter X Y, ← closure_union_closure_left_eq,
    union_eq_self_of_subset_right (inter_subset_right.trans h), closure_closure, diff_union_inter]

Premises used: Set.union_eq_self_of_subset_right, HasSubset.Subset.trans, Matroid.closure_union_closure_left_eq, Matroid.closure_closure, Set.diff_union_inter, Set.inter_subset_right
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
X : Set α
e : α
h : e ∈ M.closure (X \ {e})
⊢ {e} ⊆ M.closure (X \ {e})

Tactic:
simpa
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
X Y : Set α
h : Y ⊆ X
hY : Y ⊆ M.E
⊢ Y ⊆ M.closure (X \ Y) ↔ M.closure (X \ Y) = M.closure X

Tactic:
⟨closure_diff_eq_self, fun h' ↦ (M.subset_closure_of_subset' h).trans h'.symm.subset⟩

Premises used: HasSubset.Subset.trans, Eq.subset, Iff.intro, Eq.symm, Matroid.subset_closure_of_subset', Matroid.closure_diff_eq_self
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
X : Set α
e : α
he : e ∈ X
heE : e ∈ M.E
⊢ {e} ⊆ X

Tactic:
simpa
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
X : Set α
e : α
he : e ∈ X
heE : e ∈ M.E
⊢ e ∈ M.closure (X \ {e}) ↔ M.closure (X \ {e}) = M.closure X

Tactic:
simpa using subset_closure_diff_iff_closure_eq (Y := {e}) (X := X) (by simpa)

Premises used: Matroid.subset_closure_diff_iff_closure_eq
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M₁ M₂ : Matroid α
h : ∀ (X : Set α), M₁.closure X = M₂.closure X
⊢ M₁.E = M₂.E

Tactic:
simpa using h univ

Premises used: Set.univ
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M₁ M₂ : Matroid α
h : ∀ (X : Set α), M₁.closure X = M₂.closure X
x : Set α
h_1 : x ⊆ M₁.E
simp_rw :
  (∀ ⦃e : α⦄, e ∈ x → M₁.closure (x \ {e}) ≠ M₁.closure x) ↔ ∀ ⦃e : α⦄, e ∈ x → M₂.closure (x \ {e}) ≠ M₂.closure x
⊢ M₁.Indep x ↔ M₂.Indep x

Tactic:
simp_rw [indep_iff_forall_closure_diff_ne, h]

Premises used: Matroid.indep_iff_forall_closure_diff_ne
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
S : Set α
hS : S ⊆ M.E
rw : M.closure S = M.E ∧ S ⊆ M.E ↔ M.closure S = M.E
rw₁ rw₂ : M.closure S = M.E ↔ M.closure S = M.E
⊢ M.Spanning S ↔ M.closure S = M.E

Tactic:
rw [spanning_iff, and_iff_left hS]

Premises used: and_iff_left, Matroid.spanning_iff
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
S : Set α
hS : S ⊆ M.E
rw : M.closure (M.closure S) = M.E ↔ M.Spanning S
rw₁ : M.closure S = M.E ↔ M.Spanning S
rw₂ rw₃ : M.Spanning S ↔ M.Spanning S
⊢ M.Spanning (M.closure S) ↔ M.Spanning S

Tactic:
rw [spanning_iff_closure_eq, closure_closure, ← spanning_iff_closure_eq]

Premises used: Matroid.closure_closure, Matroid.spanning_iff_closure_eq
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
S : Set α
hS : S ⊆ M.E
rw : M.closure S = M.E ↔ M.E ⊆ M.closure S
rw₁ : M.closure S ⊆ M.E ∧ M.E ⊆ M.closure S ↔ M.E ⊆ M.closure S
rw₂ rw₃ : M.E ⊆ M.closure S ↔ M.E ⊆ M.closure S
⊢ M.Spanning S ↔ M.E ⊆ M.closure S

Tactic:
rw [spanning_iff_closure_eq, subset_antisymm_iff, and_iff_right (closure_subset_ground _ _)]

Premises used: Matroid.closure_subset_ground, and_iff_right, Matroid.spanning_iff_closure_eq, subset_antisymm_iff
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
S : Set α
hS : S ⊆ M.E
rw : ¬M.closure S = M.E → True
⊢ ¬M.Spanning S ↔ M.closure S ⊂ M.E

Tactic:
rw [spanning_iff_closure_eq, ssubset_iff_subset_ne, iff_and_self,
    iff_true_intro (M.closure_subset_ground _)]

Premises used: Matroid.closure_subset_ground, Matroid.spanning_iff_closure_eq, iff_true_intro, iff_and_self, ssubset_iff_subset_ne
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
S : Set α
hS : S ⊆ M.E
⊢ ¬M.closure S = M.E → True

Tactic:
fun _ ↦ trivial

Premises used: trivial
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
S : Set α
hS : S ⊆ M.E
⊢ ¬M.closure S = M.E → True

Tactic:
exact fun _ ↦ trivial

Premises used: trivial
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
S T : Set α
hS : M.Spanning S
hST : S ⊆ T
hT : T ⊆ M.E
rw : M.closure S ⊆ M.closure T
⊢ M.E ⊆ M.closure T

Tactic:
rw [← hS.closure_eq]

Premises used: Matroid.Spanning.closure_eq
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
S T : Set α
hS : M.Spanning S
hST : S ⊆ T
hT : T ⊆ M.E
⊢ M.closure S ⊆ M.closure T

Tactic:
M.closure_subset_closure hST

Premises used: Matroid.closure_subset_closure
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
S T : Set α
hS : M.Spanning S
hST : S ⊆ T
hT : T ⊆ M.E
⊢ M.closure S ⊆ M.closure T

Tactic:
exact M.closure_subset_closure hST

Premises used: Matroid.closure_subset_closure
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
S T : Set α
hS : M.Spanning S
hST : S ⊆ T
rw : M.Spanning (T ∩ M.E)
⊢ M.closure T = M.E

Tactic:
rw [← closure_inter_ground, ← spanning_iff_closure_eq]

Premises used: Matroid.spanning_iff_closure_eq, Matroid.closure_inter_ground
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
S T : Set α
hS : M.Spanning S
hST : S ⊆ T
⊢ M.Spanning (T ∩ M.E)

Tactic:
hS.superset (subset_inter hST hS.subset_ground)

Premises used: Matroid.Spanning.superset, Set.subset_inter, Matroid.Spanning.subset_ground
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
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)

Premises used: Matroid.Spanning.superset, Set.subset_inter, Matroid.Spanning.subset_ground
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
X S : Set α
hS : M.Spanning S
hX : X ⊆ M.E
⊢ M.Spanning (S ∪ X)

Tactic:
hS.superset subset_union_left

Premises used: Set.subset_union_left, Matroid.Spanning.superset
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
X S : Set α
hS : M.Spanning S
hX : X ⊆ M.E
⊢ M.Spanning (X ∪ S)

Tactic:
hS.superset subset_union_right

Premises used: Set.subset_union_right, Matroid.Spanning.superset
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
B : Set α
hB : M.IsBase B
⊢ M.Spanning B

Tactic:
⟨hB.closure_eq, hB.subset_ground⟩

Premises used: Matroid.IsBase.subset_ground, Matroid.IsBase.closure_eq, Matroid.Spanning.mk
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
⊢ M.Spanning M.E

Tactic:
⟨M.closure_ground, rfl.subset⟩

Premises used: Matroid.closure_ground, Matroid.Spanning.mk, Eq.subset, rfl
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
X B : Set α
hB : M.IsBase B
hBX : B ⊆ X
hX : X ⊆ M.E
⊢ M.Spanning X

Tactic:
hB.spanning.superset hBX

Premises used: Matroid.IsBase.spanning, Matroid.Spanning.superset
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
S : Set α
⊢ M.Spanning S ↔ (∃ (B : Set α), M.IsBase B ∧ B ⊆ S) ∧ S ⊆ M.E

Tactic:
⟨fun h ↦ ⟨?_, h.subset_ground⟩, fun ⟨⟨B, hB, hBS⟩, hSE⟩ ↦ hB.spanning.superset hBS⟩

Premises used: Matroid.IsBase.spanning, Matroid.Spanning.superset, _private.0.Matroid.spanning_iff_exists_isBase_subset'.match_1, Matroid.Spanning.subset_ground, Matroid.Spanning, And.intro, Iff.intro
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
S : Set α
refine : ∀ (h : M.Spanning S), ∃ (B : Set α), M.IsBase B ∧ B ⊆ S
⊢ M.Spanning S ↔ (∃ (B : Set α), M.IsBase B ∧ B ⊆ S) ∧ S ⊆ M.E

Tactic:
refine ⟨fun h ↦ ⟨?_, h.subset_ground⟩, fun ⟨⟨B, hB, hBS⟩, hSE⟩ ↦ hB.spanning.superset hBS⟩
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
S : Set α
h : M.Spanning S
obtain : ∀ (B : Set α) (hB : M.IsBasis B S), ∃ (B : Set α), M.IsBase B ∧ B ⊆ S
⊢ ∃ (B : Set α), M.IsBase B ∧ B ⊆ S

Tactic:
obtain ⟨B, hB⟩ := M.exists_isBasis S

Premises used: Matroid.exists_isBasis
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
S : Set α
h : M.Spanning S
B : Set α
hB : M.IsBasis B S
⊢ M.IsBasis B (M.closure S)

Tactic:
have hB' := hB.isBasis_closure_right
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
S : Set α
h : M.Spanning S
B : Set α
hB : M.IsBasis B S
hB' : M.IsBasis B (M.closure S)
⊢ M.IsBase B

Tactic:
rw [h.closure_eq, isBasis_ground_iff] at hB'

Premises used: Matroid.isBasis_ground_iff, Matroid.Spanning.closure_eq
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
S : Set α
h : M.Spanning S
B : Set α
hB : M.IsBasis B S
hB' : M.IsBase B
⊢ ∃ (B : Set α), M.IsBase B ∧ B ⊆ S

Tactic:
⟨B, hB', hB.subset⟩

Premises used: Matroid.IsBasis.subset, And.intro, Exists.intro
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
S : Set α
h : M.Spanning S
B : Set α
hB : M.IsBasis B S
hB' : M.IsBase B
⊢ ∃ (B : Set α), M.IsBase B ∧ B ⊆ S

Tactic:
exact ⟨B, hB', hB.subset⟩
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
S : Set α
hS : S ⊆ M.E
rw : (∃ (B : Set α), M.IsBase B ∧ B ⊆ S) ∧ S ⊆ M.E ↔ ∃ (B : Set α), M.IsBase B ∧ B ⊆ S
rw₁ rw₂ : (∃ (B : Set α), M.IsBase B ∧ B ⊆ S) ↔ ∃ (B : Set α), M.IsBase B ∧ B ⊆ S
⊢ M.Spanning S ↔ ∃ (B : Set α), M.IsBase B ∧ B ⊆ S

Tactic:
rw [spanning_iff_exists_isBase_subset', and_iff_left hS]

Premises used: and_iff_left, Matroid.spanning_iff_exists_isBase_subset'
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
S : Set α
hS : M.Spanning S
rwa rwa₁ rwa₂ rwa₃ : ∀ (hS : ∃ (B : Set α), M.IsBase B ∧ B ⊆ S), ∃ (B : Set α), M.IsBase B ∧ B ⊆ S
⊢ ∃ (B : Set α), M.IsBase B ∧ B ⊆ S

Tactic:
rwa [spanning_iff_exists_isBase_subset] at hS

Premises used: Matroid.spanning_iff_exists_isBase_subset
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
I : Set α
hI : I ⊆ M.E
rw : (∃ (B : Set α), M.IsBase B ∧ B ⊆ M.E \ I) ↔ M.Spanning (M.E \ I)
rw₁ rw₂ : (∃ (B : Set α), M.IsBase B ∧ B ⊆ M.E \ I) ↔ ∃ (B : Set α), M.IsBase B ∧ B ⊆ M.E \ I
⊢ M.Coindep I ↔ M.Spanning (M.E \ I)

Tactic:
rw [coindep_iff_exists, spanning_iff_exists_isBase_subset]

Premises used: Matroid.spanning_iff_exists_isBase_subset, Matroid.coindep_iff_exists
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
S : Set α
hS : S ⊆ M.E
rw : M.Spanning S ↔ M.Spanning (M.E \ (M.E \ S))
rw₁ rw₂ : M.Spanning S ↔ M.Spanning S
⊢ M.Spanning S ↔ M.Coindep (M.E \ S)

Tactic:
rw [coindep_iff_compl_spanning, diff_diff_cancel_left hS]

Premises used: Set.diff_diff_cancel_left, Matroid.coindep_iff_compl_spanning
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
I : Set α
hI : M.Coindep I
⊢ M.Spanning (M.E \ I)

Tactic:
(coindep_iff_compl_spanning hI.subset_ground).mp hI

Premises used: Matroid.Coindep.subset_ground, Iff.mp, Matroid.coindep_iff_compl_spanning
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
X : Set α
hK : X ⊆ M.E
rw : M.Spanning (M.E \ X) ↔ M.closure (M.E \ X) = M.E
rw₁ rw₂ : M.closure (M.E \ X) = M.E ↔ M.closure (M.E \ X) = M.E
⊢ M.Coindep X ↔ M.closure (M.E \ X) = M.E

Tactic:
rw [coindep_iff_compl_spanning, spanning_iff_closure_eq]

Premises used: Matroid.spanning_iff_closure_eq, Matroid.coindep_iff_compl_spanning
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
X : Set α
hX : M.Coindep X
⊢ M.closure (M.E \ X) = M.E

Tactic:
(coindep_iff_closure_compl_eq_ground hX.subset_ground).mp hX

Premises used: Matroid.coindep_iff_closure_compl_eq_ground, Matroid.Coindep.subset_ground, Iff.mp
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
I : Set α
hI : M.Indep I
hIs : M.Spanning I
obtain : ∀ (B : Set α) (hB : M.IsBase B) (hBI : B ⊆ I), M.IsBase I
⊢ M.IsBase I

Tactic:
obtain ⟨B, hB, hBI⟩ := hIs.exists_isBase_subset

Premises used: Matroid.Spanning.exists_isBase_subset
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
I : Set α
hI : M.Indep I
hIs : M.Spanning I
B : Set α
hB : M.IsBase B
hBI : B ⊆ I
rwa rwa₁ rwa₂ rwa₃ : M.IsBase B
⊢ M.IsBase I

Tactic:
rwa [← hB.eq_of_subset_indep hI hBI]

Premises used: Matroid.IsBase.eq_of_subset_indep
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
I : Set α
hIs : M.Spanning I
hI : M.Indep I
⊢ M.IsBase I

Tactic:
hI.isBase_of_spanning hIs

Premises used: Matroid.Indep.isBase_of_spanning
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
S I : Set α
hI : M.Indep I
hS : M.Spanning S
hSI : S ⊆ I
⊢ S = I

Tactic:
((hI.subset hSI).isBase_of_spanning hS).eq_of_subset_indep hI hSI

Premises used: Matroid.IsBase.eq_of_subset_indep, Matroid.Indep.isBase_of_spanning, Matroid.Indep.subset
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
X I : Set α
hIX : M.IsBasis I X
rw : M.closure I = M.E ↔ M.Spanning X
rw₁ : M.closure I = M.E ↔ M.closure X = M.E
rw₂ rw₃ : M.closure X = M.E ↔ M.closure X = M.E
⊢ M.Spanning I ↔ M.Spanning X

Tactic:
rw [spanning_iff_closure_eq, spanning_iff_closure_eq, hIX.closure_eq_closure]

Premises used: Matroid.spanning_iff_closure_eq, Matroid.IsBasis.closure_eq_closure
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
S B : Set α
hS : M.Spanning S
rw : M.IsBasis B S ↔ M.IsBase B ∧ B ⊆ S
⊢ (M ↾ S).IsBase B ↔ M.IsBase B ∧ B ⊆ S

Tactic:
rw [isBase_restrict_iff', isBasis'_iff_isBasis]

Premises used: Matroid.isBase_restrict_iff', Matroid.isBasis'_iff_isBasis