awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
I X : Set α
e : α
hI : M.IsBasis' I X
he : e ∈ X \ I
⊢ ¬M.Indep (insert e I)

Tactic:
fun hi ↦ he.2 <| insert_eq_self.1 <| Eq.symm <|
    hI.eq_of_subset_indep hi (subset_insert _ _) (insert_subset he.1 hI.subset)

Premises used: Matroid.IsBasis'.eq_of_subset_indep, And.right, And.left, Iff.mp, Matroid.IsBasis'.subset, Eq.symm, Set.insert_eq_self, Not, Set.subset_insert, Set.insert_subset
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
I X : Set α
hX : X ⊆ M.E
rw : Maximal (fun (A : Set α) ↦ M.Indep A ∧ A ⊆ X) I ∧ X ⊆ M.E ↔ Maximal (fun (I : Set α) ↦ M.Indep I ∧ I ⊆ X) I
rw₁ rw₂ : Maximal (fun (A : Set α) ↦ M.Indep A ∧ A ⊆ X) I ↔ Maximal (fun (I : Set α) ↦ M.Indep I ∧ I ⊆ X) I
⊢ M.IsBasis I X ↔ Maximal (fun (I : Set α) ↦ M.Indep I ∧ I ⊆ X) I

Tactic:
rw [IsBasis, and_iff_left hX]

Premises used: and_iff_left, Matroid.IsBasis
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
I X : Set α
hI : M.Indep I
hIX : I ⊆ X
hmax : ∀ ⦃J : Set α⦄, M.Indep J → I ⊆ J → J ⊆ X → J ⊆ I
hX : X ⊆ M.E
⊢ X ⊆ M.E

Tactic:
aesop_mat
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
I X : Set α
hI : M.Indep I
hIX : I ⊆ X
hmax : ∀ ⦃J : Set α⦄, M.Indep J → I ⊆ J → J ⊆ X → J ⊆ I
hX : X ⊆ M.E
rw : ∀ (J : Set α), M.Indep J → I ⊆ J → J ⊆ X → I = J
⊢ M.IsBasis I X

Tactic:
rw [isBasis_iff (by aesop_mat : X ⊆ M.E), and_iff_right hI, and_iff_right hIX]

Premises used: Matroid.isBasis_iff, and_iff_right
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
I X : Set α
hI : M.Indep I
hIX : I ⊆ X
hmax : ∀ ⦃J : Set α⦄, M.Indep J → I ⊆ J → J ⊆ X → J ⊆ I
hX : X ⊆ M.E
⊢ ∀ (J : Set α), M.Indep J → I ⊆ J → J ⊆ X → I = J

Tactic:
fun J hJ hIJ hJX ↦ hIJ.antisymm (hmax hJ hIJ hJX)

Premises used: HasSubset.Subset.antisymm
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
I X : Set α
hI : M.Indep I
hIX : I ⊆ X
hmax : ∀ ⦃J : Set α⦄, M.Indep J → I ⊆ J → J ⊆ X → J ⊆ I
hX : X ⊆ M.E
⊢ ∀ (J : Set α), M.Indep J → I ⊆ J → J ⊆ X → I = J

Tactic:
exact fun J hJ hIJ hJX ↦ hIJ.antisymm (hmax hJ hIJ hJX)
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
I X Y : Set α
hI : M.IsBasis I X
hIY : I ⊆ Y
hYX : Y ⊆ X
rw : ∀ (J : Set α), M.Indep J → I ⊆ J → J ⊆ Y → I = J
⊢ M.IsBasis I Y

Tactic:
rw [isBasis_iff (hYX.trans hI.subset_ground), and_iff_right hI.indep, and_iff_right hIY]

Premises used: Matroid.isBasis_iff, Matroid.IsBasis.subset_ground, HasSubset.Subset.trans, and_iff_right, Matroid.IsBasis.indep
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
I X Y : Set α
hI : M.IsBasis I X
hIY : I ⊆ Y
hYX : Y ⊆ X
⊢ ∀ (J : Set α), M.Indep J → I ⊆ J → J ⊆ Y → I = J

Tactic:
fun J hJ hIJ hJY ↦ hI.eq_of_subset_indep hJ hIJ (hJY.trans hYX)

Premises used: HasSubset.Subset.trans, Matroid.IsBasis.eq_of_subset_indep
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
I X Y : Set α
hI : M.IsBasis I X
hIY : I ⊆ Y
hYX : Y ⊆ X
⊢ ∀ (J : Set α), M.Indep J → I ⊆ J → J ⊆ Y → I = J

Tactic:
exact fun J hJ hIJ hJY ↦ hI.eq_of_subset_indep hJ hIJ (hJY.trans hYX)

Premises used: Matroid.IsBasis.eq_of_subset_indep
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
I : Set α
rw : M.Indep I → (∀ ⦃J : Set α⦄, M.Indep J → I ⊆ J → J ⊆ I → I = J) ∧ I ⊆ M.E
⊢ M.IsBasis I I ↔ M.Indep I

Tactic:
rw [isBasis_iff', and_iff_right rfl.subset, and_assoc, and_iff_left_iff_imp]

Premises used: Matroid.isBasis_iff', and_iff_right, Eq.subset, and_assoc, and_iff_left_iff_imp, rfl
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
I : Set α
⊢ M.Indep I → (∀ ⦃J : Set α⦄, M.Indep J → I ⊆ J → J ⊆ I → I = J) ∧ I ⊆ M.E

Tactic:
fun hi ↦ ⟨fun _ _ ↦ subset_antisymm, hi.subset_ground⟩

Premises used: subset_antisymm, Matroid.Indep.subset_ground, And.intro
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
I : Set α
⊢ M.Indep I → (∀ ⦃J : Set α⦄, M.Indep J → I ⊆ J → J ⊆ I → I = J) ∧ I ⊆ M.E

Tactic:
exact fun hi ↦ ⟨fun _ _ ↦ subset_antisymm, hi.subset_ground⟩
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
I : Set α
h : M.Indep I
⊢ M.IsBasis I I

Tactic:
isBasis_self_iff_indep.mpr h

Premises used: Iff.mpr, Matroid.isBasis_self_iff_indep
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
I : Set α
M : Matroid α
h : I = ∅
rw : M.IsBasis ∅ ∅
⊢ M.IsBasis I ∅

Tactic:
rw [h]
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
I : Set α
M : Matroid α
h : I = ∅
⊢ M.IsBasis ∅ ∅

Tactic:
M.empty_indep.isBasis_self

Premises used: Matroid.empty_indep, Matroid.Indep.isBasis_self
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
I : Set α
M : Matroid α
h : I = ∅
⊢ M.IsBasis ∅ ∅

Tactic:
exact M.empty_indep.isBasis_self

Premises used: Matroid.empty_indep, Matroid.Indep.isBasis_self
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
I X Y : Set α
hI : M.IsBasis I X
hIY : I ⊂ Y
hYX : Y ⊆ X
⊢ X ⊆ M.E

Tactic:
have : X ⊆ M.E := hI.subset_ground
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
I X Y : Set α
hI : M.IsBasis I X
hIY : I ⊂ Y
hYX : Y ⊆ X
this : X ⊆ M.E
rw : ¬M.Indep Y
⊢ M.Dep Y

Tactic:
rw [← not_indep_iff]

Premises used: Matroid.not_indep_iff
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
I X Y : Set α
hI : M.IsBasis I X
hIY : I ⊂ Y
hYX : Y ⊆ X
this : X ⊆ M.E
⊢ ¬M.Indep Y

Tactic:
fun hY ↦ hIY.ne (hI.eq_of_subset_indep hY hIY.subset hYX)

Premises used: HasSSubset.SSubset.subset, Matroid.IsBasis.eq_of_subset_indep, HasSSubset.SSubset.ne, Not
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
I X Y : Set α
hI : M.IsBasis I X
hIY : I ⊂ Y
hYX : Y ⊆ X
this : X ⊆ M.E
⊢ ¬M.Indep Y

Tactic:
exact fun hY ↦ hIY.ne (hI.eq_of_subset_indep hY hIY.subset hYX)

Premises used: HasSSubset.SSubset.subset, Matroid.IsBasis.eq_of_subset_indep, HasSSubset.SSubset.ne
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
I X : Set α
e : α
hI : M.IsBasis I X
he : e ∈ X \ I
⊢ M.Dep (insert e I)

Tactic:
hI.dep_of_ssubset (ssubset_insert he.2) (insert_subset he.1 hI.subset)

Premises used: Set.ssubset_insert, Matroid.IsBasis.subset, And.right, And.left, Matroid.IsBasis.dep_of_ssubset, Set.insert_subset
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
I X : Set α
e : α
hI : M.IsBasis I X
he : e ∈ X
hIe : M.Indep (insert e I)
⊢ e ∈ I

Tactic:
by_contra (fun heI ↦ (hI.insert_dep ⟨he, heI⟩).not_indep hIe)

Premises used: Matroid.Dep.not_indep, And.intro, by_contra, Matroid.IsBasis.insert_dep
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
I X : Set α
e : α
hI : M.IsBasis' I X
he : e ∈ X
hIe : M.Indep (insert e I)
⊢ e ∈ I

Tactic:
hI.isBasis_inter_ground.mem_of_insert_indep ⟨he, hIe.subset_ground (mem_insert _ _)⟩ hIe

Premises used: Matroid.IsBasis'.isBasis_inter_ground, Matroid.Indep.subset_ground, And.intro, Set.mem_insert, Matroid.IsBasis.mem_of_insert_indep
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
I J X : Set α
hI : M.IsBasis I X
hJI : J ⊂ I
⊢ ¬M.IsBasis J X

Tactic:
fun h ↦ hJI.ne (h.eq_of_subset_indep hI.indep hJI.subset hI.subset)

Premises used: HasSSubset.SSubset.subset, Matroid.IsBasis.subset, Matroid.IsBasis.eq_of_subset_indep, HasSSubset.SSubset.ne, Matroid.IsBasis.indep, Not
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
I X : Set α
hI : M.Indep I
hIX : I ⊆ X
hX : X ⊆ M.E
obtain :
  ∀ (J : Set α) (hJ : I ⊆ J) (hJmax : Maximal (fun (K : Set α) ↦ M.Indep K ∧ K ⊆ X) J),
    ∃ (J : Set α), M.IsBasis J X ∧ I ⊆ J
⊢ ∃ (J : Set α), M.IsBasis J X ∧ I ⊆ J

Tactic:
obtain ⟨J, hJ, hJmax⟩ := M.maximality X hX I hI hIX

Premises used: Matroid.maximality
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
I X : Set α
hI : M.Indep I
hIX : I ⊆ X
hX : X ⊆ M.E
J : Set α
hJ : I ⊆ J
hJmax : Maximal (fun (K : Set α) ↦ M.Indep K ∧ K ⊆ X) J
⊢ ∃ (J : Set α), M.IsBasis J X ∧ I ⊆ J

Tactic:
⟨J, ⟨hJmax, hX⟩, hJ⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
I X : Set α
hI : M.Indep I
hIX : I ⊆ X
hX : X ⊆ M.E
J : Set α
hJ : I ⊆ J
hJmax : Maximal (fun (K : Set α) ↦ M.Indep K ∧ K ⊆ X) J
⊢ ∃ (J : Set α), M.IsBasis J X ∧ I ⊆ J

Tactic:
exact ⟨J, ⟨hJmax, hX⟩, hJ⟩
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
I X : Set α
hI : M.Indep I
hIX : I ⊆ X
simp_rw : ∃ (J : Set α), M.IsBasis J (X ∩ M.E) ∧ I ⊆ J
⊢ ∃ (J : Set α), M.IsBasis' J X ∧ I ⊆ J

Tactic:
simp_rw [isBasis'_iff_isBasis_inter_ground]

Premises used: Matroid.isBasis'_iff_isBasis_inter_ground
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
I X : Set α
hI : M.Indep I
hIX : I ⊆ X
⊢ ∃ (J : Set α), M.IsBasis J (X ∩ M.E) ∧ I ⊆ J

Tactic:
hI.subset_isBasis_of_subset (subset_inter hIX hI.subset_ground)

Premises used: Matroid.Indep.subset_ground, Set.subset_inter, Matroid.Indep.subset_isBasis_of_subset
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
I X : Set α
hI : M.Indep I
hIX : I ⊆ X
⊢ ∃ (J : Set α), M.IsBasis J (X ∩ M.E) ∧ I ⊆ J

Tactic:
exact hI.subset_isBasis_of_subset (subset_inter hIX hI.subset_ground)

Premises used: Matroid.Indep.subset_ground, Set.subset_inter, Matroid.Indep.subset_isBasis_of_subset
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
X : Set α
hX : X ⊆ M.E
⊢ ∃ (I : Set α), M.IsBasis I X

Tactic:
let ⟨_, hI, _⟩ := M.empty_indep.subset_isBasis_of_subset (empty_subset X)
  ⟨_, hI⟩

Premises used: Exists, Matroid.empty_indep, _private.0.Matroid.exists_isBasis.match_1, Set.empty_subset, Exists.intro, Matroid.IsBasis, Matroid.Indep.subset_isBasis_of_subset
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
X : Set α
⊢ ∃ (I : Set α), M.IsBasis' I X

Tactic:
let ⟨_, hI, _⟩ := M.empty_indep.subset_isBasis'_of_subset (empty_subset X)
  ⟨_, hI⟩

Premises used: Matroid.IsBasis', Exists, Matroid.empty_indep, Matroid.Indep.subset_isBasis'_of_subset, _private.0.Matroid.exists_isBasis'.match_1, Set.empty_subset, Exists.intro
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
X Y : Set α
M : Matroid α
hXY : X ⊆ Y
hY : Y ⊆ M.E
obtain : ∀ (I : Set α) (hI : M.IsBasis I X), ∃ (I : Set α) (J : Set α), M.IsBasis I X ∧ M.IsBasis J Y ∧ I ⊆ J
⊢ ∃ (I : Set α) (J : Set α), M.IsBasis I X ∧ M.IsBasis J Y ∧ I ⊆ J

Tactic:
obtain ⟨I, hI⟩ := M.exists_isBasis X (hXY.trans hY)

Premises used: HasSubset.Subset.trans, Matroid.exists_isBasis
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
X Y : Set α
M : Matroid α
hXY : X ⊆ Y
hY : Y ⊆ M.E
I : Set α
hI : M.IsBasis I X
obtain :
  ∀ (J : Set α) (hJ : M.IsBasis J Y) (hIJ : I ⊆ J), ∃ (I : Set α) (J : Set α), M.IsBasis I X ∧ M.IsBasis J Y ∧ I ⊆ J
⊢ ∃ (I : Set α) (J : Set α), M.IsBasis I X ∧ M.IsBasis J Y ∧ I ⊆ J

Tactic:
obtain ⟨J, hJ, hIJ⟩ := hI.indep.subset_isBasis_of_subset (hI.subset.trans hXY)

Premises used: HasSubset.Subset.trans, Matroid.IsBasis.subset, Matroid.IsBasis.indep, Matroid.Indep.subset_isBasis_of_subset
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
X Y : Set α
M : Matroid α
hXY : X ⊆ Y
hY : Y ⊆ M.E
I : Set α
hI : M.IsBasis I X
J : Set α
hJ : M.IsBasis J Y
hIJ : I ⊆ J
⊢ ∃ (I : Set α) (J : Set α), M.IsBasis I X ∧ M.IsBasis J Y ∧ I ⊆ J

Tactic:
⟨_, _, hI, hJ, hIJ⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
X Y : Set α
M : Matroid α
hXY : X ⊆ Y
hY : Y ⊆ M.E
I : Set α
hI : M.IsBasis I X
J : Set α
hJ : M.IsBasis J Y
hIJ : I ⊆ J
⊢ ∃ (I : Set α) (J : Set α), M.IsBasis I X ∧ M.IsBasis J Y ∧ I ⊆ J

Tactic:
exact ⟨_, _, hI, hJ, hIJ⟩
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
I X Y : Set α
hI : M.IsBasis I X
hXY : X ⊆ Y
hY : Y ⊆ M.E
obtain : ∀ (J : Set α) (hJ : M.IsBasis J Y) (hIJ : I ⊆ J), ∃ (J : Set α), M.IsBasis J Y ∧ J ∩ X = I
⊢ ∃ (J : Set α), M.IsBasis J Y ∧ J ∩ X = I

Tactic:
obtain ⟨J, hJ, hIJ⟩ := hI.indep.subset_isBasis_of_subset (hI.subset.trans hXY)

Premises used: HasSubset.Subset.trans, Matroid.IsBasis.subset, Matroid.IsBasis.indep, Matroid.Indep.subset_isBasis_of_subset
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
I X Y : Set α
hI : M.IsBasis I X
hXY : X ⊆ Y
hY : Y ⊆ M.E
J : Set α
hJ : M.IsBasis J Y
hIJ : I ⊆ J
⊢ ∃ (J : Set α), M.IsBasis J Y ∧ J ∩ X = I

Tactic:
⟨J, hJ, subset_antisymm ?_ (subset_inter hIJ hI.subset)⟩

Premises used: subset_antisymm, Matroid.IsBasis.subset, Set.subset_inter, And.intro, Exists.intro
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
I X Y : Set α
hI : M.IsBasis I X
hXY : X ⊆ Y
hY : Y ⊆ M.E
J : Set α
hJ : M.IsBasis J Y
hIJ : I ⊆ J
refine : J ∩ X ⊆ I
⊢ ∃ (J : Set α), M.IsBasis J Y ∧ J ∩ X = I

Tactic:
refine ⟨J, hJ, subset_antisymm ?_ (subset_inter hIJ hI.subset)⟩
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
I X Y : Set α
hI : M.IsBasis I X
hXY : X ⊆ Y
hY : Y ⊆ M.E
J : Set α
hJ : M.IsBasis J Y
hIJ : I ⊆ J
⊢ J ∩ X ⊆ I

Tactic:
fun e he ↦ hI.mem_of_insert_indep he.2 (hJ.indep.subset (insert_subset he.1 hIJ))

Premises used: Matroid.Indep.subset, Set.Subset, And.right, And.left, Matroid.IsBasis.mem_of_insert_indep, Matroid.IsBasis.indep, Set.insert_subset
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
I X Y : Set α
hI : M.IsBasis I X
hXY : X ⊆ Y
hY : Y ⊆ M.E
J : Set α
hJ : M.IsBasis J Y
hIJ : I ⊆ J
⊢ J ∩ X ⊆ I

Tactic:
exact fun e he ↦ hI.mem_of_insert_indep he.2 (hJ.indep.subset (insert_subset he.1 hIJ))

Premises used: Matroid.Indep.subset, Matroid.IsBasis.mem_of_insert_indep, Matroid.IsBasis.indep, Set.insert_subset
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
X Y : Set α
hX : X ⊆ M.E
hY : Y ⊆ M.E
J : Set α
hJ : M.IsBasis J Y
I : Set α
hI : M.IsBasis I (X ∪ Y) ∧ I ∩ Y = J
rwa rwa₁ rwa₂ rwa₃ : M.IsBasis J Y
⊢ M.IsBasis (I ∩ Y) Y

Tactic:
rwa [hI.2]

Premises used: And.right
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
I J : Set α
hI : M.Indep I
hJ : M.IsBasis J I
⊢ J = I

Tactic:
hJ.eq_of_subset_indep hI hJ.subset rfl.subset

Premises used: Matroid.IsBasis.subset, Eq.subset, Matroid.IsBasis.eq_of_subset_indep, rfl
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
I X : Set α
hI : M.IsBasis I X
B : Set α
hB : M.IsBase B
hIB : I ⊆ B
rw rw₁ : B ∩ X ⊆ B ∩ X
⊢ B ∩ X ⊆ I

Tactic:
rw [hI.eq_of_subset_indep (hB.indep.inter_right X) (subset_inter hIB hI.subset)
    inter_subset_right]

Premises used: Matroid.IsBasis.subset, Set.subset_inter, Matroid.IsBasis.eq_of_subset_indep, Matroid.Indep.inter_right, Matroid.IsBase.indep, Set.inter_subset_right
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
B : Set α
rw : Maximal (fun (A : Set α) ↦ M.Indep A ∧ A ⊆ M.E) B ∧ M.E ⊆ M.E ↔ M.IsBase B
rw₁ : Maximal (fun (A : Set α) ↦ M.Indep A ∧ A ⊆ M.E) B ↔ M.IsBase B
rw₂ : Maximal (fun (A : Set α) ↦ M.Indep A ∧ A ⊆ M.E) B ↔ Maximal M.Indep B
rw₃ : Maximal M.Indep B ∧ B ⊆ M.E ↔ Maximal M.Indep B
rw₄ rw₅ : Maximal M.Indep B ↔ Maximal M.Indep B
⊢ M.IsBasis B M.E ↔ M.IsBase B

Tactic:
rw [IsBasis, and_iff_left rfl.subset, isBase_iff_maximal_indep,
    maximal_and_iff_right_of_imp (fun _ h ↦ h.subset_ground),
    and_iff_left_of_imp (fun h ↦ h.1.subset_ground)]

Premises used: and_iff_left_of_imp, and_iff_left, maximal_and_iff_right_of_imp, Eq.subset, Matroid.isBase_iff_maximal_indep, Matroid.IsBasis, rfl
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
B : Set α
hB : M.IsBase B
⊢ M.IsBasis B M.E

Tactic:
isBasis_ground_iff.mpr hB

Premises used: Iff.mpr, Matroid.isBasis_ground_iff
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
I X : Set α
hI : M.Indep I
hIX : I ⊆ X
rw :
  ((M.Indep I ∧ I ⊆ X) ∧ ∀ x ∉ I, ¬(M.Indep (insert x I) ∧ insert x I ⊆ X)) ∧ X ⊆ M.E ↔ ∀ e ∈ X \ I, M.Dep (insert e I)
⊢ M.IsBasis I X ↔ ∀ e ∈ X \ I, M.Dep (insert e I)

Tactic:
rw [IsBasis, maximal_iff_forall_insert (fun I J hI hIJ ↦ ⟨hI.1.subset hIJ, hIJ.trans hI.2⟩)]

Premises used: Set.maximal_iff_forall_insert, Matroid.IsBasis
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
I X : Set α
hI : M.Indep I
hIX : I ⊆ X
simp : (∀ x ∉ I, M.Indep (insert x I) → x ∉ X) ∧ X ⊆ M.E ↔ ∀ e ∈ X, e ∉ I → ¬M.Indep (insert e I) ∧ e ∈ M.E
⊢ ((M.Indep I ∧ I ⊆ X) ∧ ∀ x ∉ I, ¬(M.Indep (insert x I) ∧ insert x I ⊆ X)) ∧ X ⊆ M.E ↔ ∀ e ∈ X \ I, M.Dep (insert e I)

Tactic:
simp only [hI, hIX, and_self, insert_subset_iff, and_true, not_and, true_and, mem_diff, and_imp,
    Dep, hI.subset_ground]

Premises used: Matroid.Dep, and_true, and_self, and_imp, Set.insert_subset_iff, Matroid.Indep.subset_ground, Set.mem_diff, not_and, true_and
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
I X : Set α
hI : M.Indep I
hIX : I ⊆ X
⊢ (∀ x ∉ I, M.Indep (insert x I) → x ∉ X) ∧ X ⊆ M.E ↔ ∀ e ∈ X, e ∉ I → ¬M.Indep (insert e I) ∧ e ∈ M.E

Tactic:
⟨fun h e heX heI ↦ ⟨fun hi ↦ h.1 e heI hi heX, h.2 heX⟩,
    fun h ↦ ⟨fun e heI hi heX ↦ (h e heX heI).1 hi,
      fun e heX ↦ (em (e ∈ I)).elim (fun h ↦ hI.subset_ground h) fun heI ↦ (h _ heX heI).2 ⟩⟩

Premises used: Membership.mem, em, Matroid.Indep.subset_ground, And.right, And.left, And.intro, Iff.intro, Or.elim
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
I X : Set α
hI : M.Indep I
hIX : I ⊆ X
⊢ (∀ x ∉ I, M.Indep (insert x I) → x ∉ X) ∧ X ⊆ M.E ↔ ∀ e ∈ X, e ∉ I → ¬M.Indep (insert e I) ∧ e ∈ M.E

Tactic:
exact ⟨fun h e heX heI ↦ ⟨fun hi ↦ h.1 e heI hi heX, h.2 heX⟩,
    fun h ↦ ⟨fun e heI hi heX ↦ (h e heX heI).1 hi,
      fun e heX ↦ (em (e ∈ I)).elim (fun h ↦ hI.subset_ground h) fun heI ↦ (h _ heX heI).2 ⟩⟩
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
I X : Set α
hI : M.Indep I
hIX : I ⊆ X
he : ∀ e ∈ X \ I, M.Dep (insert e I)
⊢ M.IsBasis I X

Tactic:
(hI.isBasis_iff_forall_insert_dep hIX).mpr he

Premises used: Iff.mpr, Matroid.Indep.isBasis_iff_forall_insert_dep
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
I : Set α
e : α
hI : M.Indep I
simp_rw : e ∉ I → ¬M.Indep (insert e I) ∧ e ∈ M.E ↔ ¬M.Indep (insert e I) ∧ e ∈ M.E ∨ e ∈ I
⊢ M.IsBasis I (insert e I) ↔ M.Dep (insert e I) ∨ e ∈ I

Tactic:
simp_rw [hI.isBasis_iff_forall_insert_dep (subset_insert _ _), dep_iff, insert_subset_iff,
    and_iff_left hI.subset_ground, mem_diff, mem_insert_iff, or_and_right, and_not_self,
    or_false, and_imp, forall_eq]

Premises used: and_imp, and_iff_left, forall_eq, Set.insert_subset_iff, Matroid.Indep.subset_ground, and_not_self, Set.mem_diff, Matroid.Indep.isBasis_iff_forall_insert_dep, or_false, Set.mem_insert_iff, or_and_right, Set.subset_insert, Matroid.dep_iff
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
I : Set α
e : α
hI : M.Indep I
mp : (e ∉ I → ¬M.Indep (insert e I) ∧ e ∈ M.E) → ¬M.Indep (insert e I) ∧ e ∈ M.E ∨ e ∈ I
mpr : ¬M.Indep (insert e I) ∧ e ∈ M.E ∨ e ∈ I → e ∉ I → ¬M.Indep (insert e I) ∧ e ∈ M.E
mp₁ : ¬e ∉ I → ¬M.Indep (insert e I) ∧ e ∈ M.E ∨ e ∈ I
mp₂ : ¬M.Indep (insert e I) → e ∈ M.E → ¬M.Indep (insert e I) ∧ e ∈ M.E ∨ e ∈ I
mp₃ : ¬e ∉ I → ¬M.Indep (insert e I) ∧ e ∈ M.E ∨ e ∈ I
mp₄ : ¬M.Indep (insert e I) → e ∈ M.E → ¬M.Indep (insert e I) ∧ e ∈ M.E ∨ e ∈ I
mp₅ : ¬e ∉ I → ¬(¬M.Indep (insert e I) ∧ e ∈ M.E) → e ∈ I
mp₆ : ¬M.Indep (insert e I) → e ∈ M.E → ¬(¬M.Indep (insert e I) ∧ e ∈ M.E) → e ∈ I
mpr₁ : ¬M.Indep (insert e I) → e ∈ M.E → e ∉ I → ¬M.Indep (insert e I) ∧ e ∈ M.E
mpr₂ : e ∈ I → e ∉ I → ¬M.Indep (insert e I) ∧ e ∈ M.E
mpr₃ : ¬M.Indep (insert e I) → e ∈ M.E → e ∉ I → ¬M.Indep (insert e I) ∧ e ∈ M.E
mpr₄ : e ∈ I → e ∉ I → ¬M.Indep (insert e I) ∧ e ∈ M.E
mpr₅ : ¬M.Indep (insert e I) → e ∈ M.E → e ∉ I → ¬M.Indep (insert e I)
mpr₆ : ¬M.Indep (insert e I) → e ∈ M.E → e ∉ I → e ∈ M.E
mpr₇ : e ∈ I → e ∉ I → ¬M.Indep (insert e I)
mpr₈ : e ∈ I → e ∉ I → e ∈ M.E
mp₇ : e ∈ I → ¬¬M.Indep (insert e I) → e ∈ I
mp₈ : e ∈ I → e ∉ M.E → e ∈ I
mp₉ : e ∈ I → ¬¬M.Indep (insert e I) → e ∈ I
mp₁₀ : e ∈ I → e ∉ M.E → e ∈ I
mp₁₁ : e ∈ I → ¬¬M.Indep (insert e I) → e ∈ I
mp₁₂ : e ∈ I → e ∉ M.E → e ∈ I
mp₁₃ : ¬M.Indep (insert e I) → e ∈ M.E → ¬¬M.Indep (insert e I) → e ∈ I
mp₁₄ : ¬M.Indep (insert e I) → e ∈ M.E → e ∉ M.E → e ∈ I
mpr₉ : e ∈ I → e ∉ I → M.Indep (insert e I) → False
mpr₁₀ : e ∈ I → e ∉ I → e ∈ M.E
⊢ e ∉ I → ¬M.Indep (insert e I) ∧ e ∈ M.E ↔ ¬M.Indep (insert e I) ∧ e ∈ M.E ∨ e ∈ I

Tactic:
tauto
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
ι : Type u_2
X I : ι → Set α
hI : ∀ (i : ι), M.IsBasis (I i) (X i)
h_ind : M.Indep (⋃ (i : ι), I i)
⊢ M.IsBasis (⋃ (i : ι), I i) (⋃ (i : ι), X i)

Tactic:
h_ind.isBasis_of_forall_insert
    (iUnion_subset (fun i ↦ (hI i).subset.trans (subset_iUnion _ _))) ?_

Premises used: Matroid.Indep.isBasis_of_forall_insert, Set.iUnion_subset, HasSubset.Subset.trans, Matroid.IsBasis.subset, Set.subset_iUnion
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
ι : Type u_2
X I : ι → Set α
hI : ∀ (i : ι), M.IsBasis (I i) (X i)
h_ind : M.Indep (⋃ (i : ι), I i)
refine :
  ∀ (e : α), Membership.mem (γ := Set α) ((⋃ (i : ι), X i) \ ⋃ (i : ι), I i) e → M.Dep (insert e (⋃ (i : ι), I i))
⊢ M.IsBasis (⋃ (i : ι), I i) (⋃ (i : ι), X i)

Tactic:
refine h_ind.isBasis_of_forall_insert
    (iUnion_subset (fun i ↦ (hI i).subset.trans (subset_iUnion _ _))) ?_

Premises used: Matroid.Indep.isBasis_of_forall_insert, Set.iUnion_subset, HasSubset.Subset.trans, Matroid.IsBasis.subset, Set.subset_iUnion
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
ι : Type u_2
X I : ι → Set α
hI : ∀ (i : ι), M.IsBasis (I i) (X i)
h_ind : M.Indep (⋃ (i : ι), I i)
e : α
he' : e ∉ ⋃ (i : ι), I i
i : ι
hes : e ∈ X i
rw : ∀ (he' : ∀ (x : ι), e ∉ I x) (i : ι) (hes : e ∈ X i), M.Dep (insert e (⋃ (i : ι), I i))
⊢ M.Dep (insert e (⋃ (i : ι), I i))

Tactic:
rw [mem_iUnion, not_exists] at he'

Premises used: Set.mem_iUnion, not_exists
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
ι : Type u_2
X I : ι → Set α
hI : ∀ (i : ι), M.IsBasis (I i) (X i)
h_ind : M.Indep (⋃ (i : ι), I i)
e : α
he' : ∀ (x : ι), e ∉ I x
i : ι
hes : e ∈ X i
⊢ M.Dep (insert e (⋃ (i : ι), I i))

Tactic:
((hI i).insert_dep ⟨hes, he' _⟩).superset (insert_subset_insert (subset_iUnion _ _)) ?_

Premises used: Matroid.Dep.superset, Set.subset_iUnion, And.intro, Matroid.IsBasis.insert_dep, Set.insert_subset_insert
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
ι : Type u_2
X I : ι → Set α
hI : ∀ (i : ι), M.IsBasis (I i) (X i)
h_ind : M.Indep (⋃ (i : ι), I i)
e : α
he' : ∀ (x : ι), e ∉ I x
i : ι
hes : e ∈ X i
refine : insert e (⋃ (i : ι), I i) ⊆ M.E
⊢ M.Dep (insert e (⋃ (i : ι), I i))

Tactic:
refine ((hI i).insert_dep ⟨hes, he' _⟩).superset (insert_subset_insert (subset_iUnion _ _)) ?_

Premises used: Matroid.Dep.superset, Set.subset_iUnion, And.intro, Matroid.IsBasis.insert_dep, Set.insert_subset_insert
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
ι : Type u_2
X I : ι → Set α
hI : ∀ (i : ι), M.IsBasis (I i) (X i)
h_ind : M.Indep (⋃ (i : ι), I i)
e : α
he' : ∀ (x : ι), e ∉ I x
i : ι
hes : e ∈ X i
rw : e ∈ M.E
⊢ insert e (⋃ (i : ι), I i) ⊆ M.E

Tactic:
rw [insert_subset_iff, iUnion_subset_iff, and_iff_left (fun i ↦ (hI i).indep.subset_ground)]

Premises used: Set.iUnion_subset_iff, and_iff_left, Set.insert_subset_iff, Matroid.Indep.subset_ground, Matroid.IsBasis.indep
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
ι : Type u_2
X I : ι → Set α
hI : ∀ (i : ι), M.IsBasis (I i) (X i)
h_ind : M.Indep (⋃ (i : ι), I i)
e : α
he' : ∀ (x : ι), e ∉ I x
i : ι
hes : e ∈ X i
⊢ e ∈ M.E

Tactic:
(hI i).subset_ground hes

Premises used: Matroid.IsBasis.subset_ground