awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
rw : ¬¬M.RankFinite ↔ M.RankFinite
rw₁ rw₂ : M.RankFinite ↔ M.RankFinite
⊢ ¬M.RankInfinite ↔ M.RankFinite

Tactic:
rw [← not_rankFinite_iff, not_not]

Premises used: Classical.not_not, Matroid.not_rankFinite_iff
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
B₁ B₂ : Set α
hB₁ : M.IsBase B₁
hB₂ : M.IsBase B₂
⊢ (B₁ \ B₂).Finite ↔ (B₂ \ B₁).Finite

Tactic:
finite_iff_finite_of_encard_eq_encard (hB₁.encard_diff_comm hB₂)

Premises used: Set.finite_iff_finite_of_encard_eq_encard, Matroid.IsBase.encard_diff_comm
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
B₁ B₂ : Set α
hB₁ : M.IsBase B₁
hB₂ : M.IsBase B₂
⊢ (B₁ \ B₂).Infinite ↔ (B₂ \ B₁).Infinite

Tactic:
infinite_iff_infinite_of_encard_eq_encard (hB₁.encard_diff_comm hB₂)

Premises used: Matroid.IsBase.encard_diff_comm, Set.infinite_iff_infinite_of_encard_eq_encard
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
h : ∀ ⦃B : Set α⦄, B ⊆ M₁.E → (M₁.IsBase B ↔ M₂.IsBase B)
⊢ ∀ (B : Set α), M₁.IsBase B ↔ M₂.IsBase B

Tactic:
have h' : ∀ B, M₁.IsBase B ↔ M₂.IsBase B :=
    fun B ↦ ⟨fun hB ↦ (h hB.subset_ground).1 hB,
      fun hB ↦ (h <| hB.subset_ground.trans_eq hE.symm).2 hB⟩
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
h : ∀ ⦃B : Set α⦄, B ⊆ M₁.E → (M₁.IsBase B ↔ M₂.IsBase B)
h' : ∀ (B : Set α), M₁.IsBase B ↔ M₂.IsBase B
E : ∀ (x : α), x ∈ M₁.E ↔ x ∈ M₂.E
IsBase : ∀ (x : Set α), M₁.IsBase x ↔ M₂.IsBase x
Indep : ∀ (x : Set α), M₁.Indep x ↔ M₂.Indep x
⊢ M₁ = M₂

Tactic:
ext
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
h : ∀ ⦃B : Set α⦄, B ⊆ M₁.E → (M₁.IsBase B ↔ M₂.IsBase B)
h' : ∀ (B : Set α), M₁.IsBase B ↔ M₂.IsBase B
x : α
⊢ x ∈ M₁.E ↔ x ∈ M₂.E

Tactic:
simp [hE, M₁.indep_iff', M₂.indep_iff', h']

Premises used: Matroid.indep_iff'
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
h : ∀ ⦃B : Set α⦄, B ⊆ M₁.E → (M₁.IsBase B ↔ M₂.IsBase B)
h' : ∀ (B : Set α), M₁.IsBase B ↔ M₂.IsBase B
x : Set α
⊢ M₁.IsBase x ↔ M₂.IsBase x

Tactic:
simp [hE, M₁.indep_iff', M₂.indep_iff', h']

Premises used: Matroid.indep_iff'
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
h : ∀ ⦃B : Set α⦄, B ⊆ M₁.E → (M₁.IsBase B ↔ M₂.IsBase B)
h' : ∀ (B : Set α), M₁.IsBase B ↔ M₂.IsBase B
x : Set α
⊢ M₁.Indep x ↔ M₂.Indep x

Tactic:
simp [hE, M₁.indep_iff', M₂.indep_iff', h']

Premises used: Matroid.indep_iff'
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M₁ M₂ : Matroid α
h : M₁ = M₂
⊢ M₁.E = M₂.E ∧ ∀ ⦃B : Set α⦄, B ⊆ M₁.E → (M₁.IsBase B ↔ M₂.IsBase B)

Tactic:
simp [h]
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
B : Set α
hB : B ⊆ M.E
simp_rw :
  M.IsBase (M.E \ B) ↔
    (∃ (B_1 : Set α), M.IsBase B_1 ∧ Disjoint B B_1) ∧
      ∀ ⦃y : Set α⦄, y ⊆ M.E → ∀ (x : Set α) (h : M.IsBase x ∧ Disjoint y x), B ≤ y → B = y
⊢ M.IsBase (M.E \ B) ↔ Maximal (fun (I : Set α) ↦ I ⊆ M.E ∧ ∃ (B : Set α), M.IsBase B ∧ Disjoint I B) B

Tactic:
simp_rw [maximal_iff, and_iff_right hB, and_imp, forall_exists_index]

Premises used: and_imp, forall_exists_index, and_iff_right, maximal_iff
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
B : Set α
hB : B ⊆ M.E
⊢ M.IsBase (M.E \ B) ↔
    (∃ (B_1 : Set α), M.IsBase B_1 ∧ Disjoint B B_1) ∧
      ∀ ⦃y : Set α⦄, y ⊆ M.E → ∀ (x : Set α) (h : M.IsBase x ∧ Disjoint y x), B ≤ y → B = y

Tactic:
⟨fun h ↦ ⟨⟨_, h, disjoint_sdiff_right⟩,
    fun I hI B' ⟨hB', hIB'⟩ hBI ↦ hBI.antisymm ?_⟩, fun ⟨⟨B', hB', hBB'⟩,h⟩ ↦ ?_⟩

Premises used: Matroid.E, _private.0.Matroid.isBase_compl_iff_maximal_disjoint_isBase.match_4, LE.le.antisymm, Matroid.IsBase, SDiff.sdiff, _private.0.Matroid.isBase_compl_iff_maximal_disjoint_isBase.match_3, And.intro, Set.disjoint_sdiff_right, Iff.intro, Exists.intro, Eq
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
B : Set α
hB : B ⊆ M.E
refine_1 :
  ∀ (h : M.IsBase (M.E \ B)) (I : Set α) (hI : I ⊆ M.E) (B' : Set α),
    M.IsBase B' ∧ Disjoint I B' → ∀ (hBI : B ≤ I) (hB' : M.IsBase B') (hIB' : Disjoint I B'), I ≤ B
refine_2 :
  ((∃ (B_1 : Set α), M.IsBase B_1 ∧ Disjoint B B_1) ∧
      ∀ ⦃y : Set α⦄, y ⊆ M.E → ∀ (x : Set α) (h : M.IsBase x ∧ Disjoint y x), B ≤ y → B = y) →
    ∀ (B' : Set α) (hB' : M.IsBase B') (hBB' : Disjoint B B')
      (h : ∀ ⦃y : Set α⦄, y ⊆ M.E → ∀ (x : Set α) (h : M.IsBase x ∧ Disjoint y x), B ≤ y → B = y), M.IsBase (M.E \ B)
⊢ M.IsBase (M.E \ B) ↔
    (∃ (B_1 : Set α), M.IsBase B_1 ∧ Disjoint B B_1) ∧
      ∀ ⦃y : Set α⦄, y ⊆ M.E → ∀ (x : Set α) (h : M.IsBase x ∧ Disjoint y x), B ≤ y → B = y

Tactic:
refine ⟨fun h ↦ ⟨⟨_, h, disjoint_sdiff_right⟩,
    fun I hI B' ⟨hB', hIB'⟩ hBI ↦ hBI.antisymm ?_⟩, fun ⟨⟨B', hB', hBB'⟩,h⟩ ↦ ?_⟩
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
B : Set α
hB : B ⊆ M.E
h : M.IsBase (M.E \ B)
I : Set α
hI : I ⊆ M.E
B' : Set α
h_1 : M.IsBase B' ∧ Disjoint I B'
hBI : B ≤ I
hB' : M.IsBase B'
hIB' : Disjoint I B'
refine_1 : ∀ (hIB' : I ⊆ M.Eᶜ ∪ B), I ≤ B
refine_1₁ : B' ⊆ M.E \ B
⊢ I ≤ B

Tactic:
rw [hB'.eq_of_subset_isBase h, ← subset_compl_iff_disjoint_right, diff_eq, compl_inter,
      compl_compl] at hIB'

Premises used: compl_compl, Set.subset_compl_iff_disjoint_right, Set.compl_inter, Set.diff_eq, Matroid.IsBase.eq_of_subset_isBase
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
B : Set α
hB : B ⊆ M.E
h : M.IsBase (M.E \ B)
I : Set α
hI : I ⊆ M.E
B' : Set α
h_1 : M.IsBase B' ∧ Disjoint I B'
hBI : B ≤ I
hB' : M.IsBase B'
hIB' : I ⊆ M.Eᶜ ∪ B
⊢ I ≤ B

Tactic:
fun e he ↦ (hIB' he).elim (fun h' ↦ (h' (hI he)).elim) id

Premises used: False.elim, id, Set.Subset, Or.elim
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
B : Set α
hB : B ⊆ M.E
h : M.IsBase (M.E \ B)
I : Set α
hI : I ⊆ M.E
B' : Set α
h_1 : M.IsBase B' ∧ Disjoint I B'
hBI : B ≤ I
hB' : M.IsBase B'
hIB' : I ⊆ M.Eᶜ ∪ B
⊢ I ≤ B

Tactic:
exact fun e he ↦ (hIB' he).elim (fun h' ↦ (h' (hI he)).elim) id

Premises used: False.elim, id, Or.elim
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
B : Set α
hB : B ⊆ M.E
h : M.IsBase (M.E \ B)
I : Set α
hI : I ⊆ M.E
B' : Set α
h_1 : M.IsBase B' ∧ Disjoint I B'
hBI : B ≤ I
hB' : M.IsBase B'
hIB' : Disjoint I B'
refine_1 : Disjoint B B'
⊢ B' ⊆ M.E \ B

Tactic:
rw [subset_diff, and_iff_right hB'.subset_ground, disjoint_comm]

Premises used: disjoint_comm, Set.subset_diff, Matroid.IsBase.subset_ground, and_iff_right
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
B : Set α
hB : B ⊆ M.E
h : M.IsBase (M.E \ B)
I : Set α
hI : I ⊆ M.E
B' : Set α
h_1 : M.IsBase B' ∧ Disjoint I B'
hBI : B ≤ I
hB' : M.IsBase B'
hIB' : Disjoint I B'
⊢ Disjoint B B'

Tactic:
disjoint_of_subset_left hBI hIB'

Premises used: Set.disjoint_of_subset_left
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
B : Set α
hB : B ⊆ M.E
h : M.IsBase (M.E \ B)
I : Set α
hI : I ⊆ M.E
B' : Set α
h_1 : M.IsBase B' ∧ Disjoint I B'
hBI : B ≤ I
hB' : M.IsBase B'
hIB' : Disjoint I B'
⊢ Disjoint B B'

Tactic:
exact disjoint_of_subset_left hBI hIB'

Premises used: Set.disjoint_of_subset_left
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
B : Set α
hB : B ⊆ M.E
h_1 :
  (∃ (B_1 : Set α), M.IsBase B_1 ∧ Disjoint B B_1) ∧
    ∀ ⦃y : Set α⦄, y ⊆ M.E → ∀ (x : Set α) (h : M.IsBase x ∧ Disjoint y x), B ≤ y → B = y
B' : Set α
hB' : M.IsBase B'
hBB' : Disjoint B B'
h : ∀ ⦃y : Set α⦄, y ⊆ M.E → ∀ (x : Set α) (h : M.IsBase x ∧ Disjoint y x), B ≤ y → B = y
refine_2 : M.IsBase (M.E \ (M.E \ B'))
refine_2₁ : B ≤ M.E \ B'
⊢ M.IsBase (M.E \ B)

Tactic:
rw [h diff_subset B' ⟨hB', disjoint_sdiff_left⟩]

Premises used: Set.diff_subset, Set.disjoint_sdiff_left, And.intro
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
B : Set α
hB : B ⊆ M.E
h_1 :
  (∃ (B_1 : Set α), M.IsBase B_1 ∧ Disjoint B B_1) ∧
    ∀ ⦃y : Set α⦄, y ⊆ M.E → ∀ (x : Set α) (h : M.IsBase x ∧ Disjoint y x), B ≤ y → B = y
B' : Set α
hB' : M.IsBase B'
hBB' : Disjoint B B'
h : ∀ ⦃y : Set α⦄, y ⊆ M.E → ∀ (x : Set α) (h : M.IsBase x ∧ Disjoint y x), B ≤ y → B = y
⊢ M.IsBase (M.E \ (M.E \ B'))

Tactic:
simpa [hB'.subset_ground]

Premises used: Matroid.IsBase.subset_ground
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
B : Set α
hB : B ⊆ M.E
h_1 :
  (∃ (B_1 : Set α), M.IsBase B_1 ∧ Disjoint B B_1) ∧
    ∀ ⦃y : Set α⦄, y ⊆ M.E → ∀ (x : Set α) (h : M.IsBase x ∧ Disjoint y x), B ≤ y → B = y
B' : Set α
hB' : M.IsBase B'
hBB' : Disjoint B B'
h : ∀ ⦃y : Set α⦄, y ⊆ M.E → ∀ (x : Set α) (h : M.IsBase x ∧ Disjoint y x), B ≤ y → B = y
⊢ B ≤ M.E \ B'

Tactic:
simp [subset_diff, hB, hBB']

Premises used: Set.subset_diff
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
I : Set α
⊢ M.Indep I ↔ ∃ (B : Set α), M.IsBase B ∧ I ⊆ B

Tactic:
M.indep_iff' (I := I)

Premises used: Matroid.indep_iff'
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
simp_rw : {I : Set α | ∃ (B : Set α), M.IsBase B ∧ I ⊆ B} = (↑(lowerClosure {B : Set α | M.IsBase B}) : Set (Set α))
simp_rw₁ :
  {I : Set α | ∃ (B : Set α), M.IsBase B ∧ I ⊆ B} =
    (↑{ carrier := {x : Set α | ∃ (a : Set α), Membership.mem (γ := Set (Set α)) {B : Set α | M.IsBase B} a ∧ x ≤ a},
          lower' := ⋯ : LowerSet (Set α) } :
      Set (Set α))
simp_rw₂ :
  Eq.{u_1 + 1} (α := Set (Set α)) {I : Set α | ∃ (B : Set α), M.IsBase B ∧ I ⊆ B}
    {x : Set α | ∃ (a : Set α), Membership.mem (γ := Set (Set α)) {B : Set α | M.IsBase B} a ∧ x ≤ a}
simp_rw₃ :
  Eq.{u_1 + 1} (α := Set (Set α)) {I : Set α | ∃ (B : Set α), M.IsBase B ∧ I ⊆ B}
    {x : Set α | ∃ (a : Set α), M.IsBase a ∧ x ≤ a}
⊢ {I : Set α | M.Indep I} = (↑(lowerClosure {B : Set α | M.IsBase B}) : Set (Set α))

Tactic:
simp_rw [indep_iff, lowerClosure, LowerSet.coe_mk, mem_setOf, le_eq_subset]

Premises used: LowerSet.coe_mk, Set.le_eq_subset, Matroid.indep_iff, Set.mem_setOf, lowerClosure
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
I : Set α
hI : M.Indep I
⊢ ∃ (B : Set α), M.IsBase B ∧ I ⊆ B

Tactic:
indep_iff.1 hI

Premises used: Matroid.indep_iff, Iff.mp
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
D : Set α
⊢ M.Dep D ↔ ¬M.Indep D ∧ D ⊆ M.E

Tactic:
Iff.rfl

Premises used: Matroid.Dep, Iff.rfl
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
⊢ {D : Set α | M.Dep D} = {I : Set α | M.Indep I}ᶜ ∩ Iic M.E

Tactic:
rfl

Premises used: Matroid.Dep, Set.Mem, setOf, Set.inter, Set.Iic, Not, rfl
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
I : Set α
hI : M.Indep I
obtain : ∀ (B : Set α) (hB : M.IsBase B) (hIB : I ⊆ B), I ⊆ M.E
⊢ I ⊆ M.E

Tactic:
obtain ⟨B, hB, hIB⟩ := hI.exists_isBase_superset

Premises used: Matroid.Indep.exists_isBase_superset
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
I : Set α
hI : M.Indep I
B : Set α
hB : M.IsBase B
hIB : I ⊆ B
⊢ I ⊆ M.E

Tactic:
hIB.trans hB.subset_ground

Premises used: HasSubset.Subset.trans, Matroid.IsBase.subset_ground
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
I : Set α
hI : M.Indep I
B : Set α
hB : M.IsBase B
hIB : I ⊆ B
⊢ I ⊆ M.E

Tactic:
exact hIB.trans hB.subset_ground

Premises used: HasSubset.Subset.trans, Matroid.IsBase.subset_ground
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
D : Set α
hD : M.Dep D
⊢ D ⊆ M.E

Tactic:
hD.2

Premises used: And.right
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
X : Set α
hX : X ⊆ M.E
rw : M.Indep X ∨ ¬M.Indep X
⊢ M.Indep X ∨ M.Dep X

Tactic:
rw [Dep, and_iff_left hX]

Premises used: Matroid.Dep, and_iff_left
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
X : Set α
hX : X ⊆ M.E
⊢ M.Indep X ∨ ¬M.Indep X

Tactic:
apply em

Premises used: em
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
I : Set α
hI : M.Indep I
⊢ ¬M.Dep I

Tactic:
fun h ↦ h.1 hI

Premises used: And.left, Not
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
D : Set α
hD : M.Dep D
⊢ ¬M.Indep D

Tactic:
hD.1

Premises used: And.left
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
D : Set α
hD : ¬M.Indep D
hDE : D ⊆ M.E
⊢ M.Dep D

Tactic:
⟨hD, hDE⟩

Premises used: Matroid.Dep, And.intro
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
I : Set α
hI : ¬M.Dep I
hIE : I ⊆ M.E
⊢ M.Indep I

Tactic:
by_contra (fun h ↦ hI ⟨h, hIE⟩)

Premises used: And.intro, by_contra
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
X : Set α
hX : X ⊆ M.E
rw : ¬(¬M.Indep X ∧ X ⊆ M.E) ↔ M.Indep X
rw₁ : ¬¬M.Indep X ↔ M.Indep X
rw₂ rw₃ : M.Indep X ↔ M.Indep X
⊢ ¬M.Dep X ↔ M.Indep X

Tactic:
rw [Dep, and_iff_left hX, not_not]

Premises used: Matroid.Dep, Classical.not_not, and_iff_left
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
X : Set α
hX : X ⊆ M.E
rw : ¬M.Indep X ↔ ¬M.Indep X ∧ X ⊆ M.E
rw₁ rw₂ : ¬M.Indep X ↔ ¬M.Indep X
⊢ ¬M.Indep X ↔ M.Dep X

Tactic:
rw [Dep, and_iff_left hX]

Premises used: Matroid.Dep, and_iff_left
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
I : Set α
rw : M.Indep I ↔ (I ⊆ M.E → M.Indep I) ∧ I ⊆ M.E
⊢ M.Indep I ↔ ¬M.Dep I ∧ I ⊆ M.E

Tactic:
rw [dep_iff, not_and, not_imp_not]

Premises used: not_and, Matroid.dep_iff, not_imp_not
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
I : Set α
⊢ M.Indep I ↔ (I ⊆ M.E → M.Indep I) ∧ I ⊆ M.E

Tactic:
⟨fun h ↦ ⟨fun _ ↦ h, h.subset_ground⟩, fun h ↦ h.1 h.2⟩

Premises used: Matroid.Indep.subset_ground, And.right, And.left, And.intro, Iff.intro
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
I : Set α
⊢ M.Indep I ↔ (I ⊆ M.E → M.Indep I) ∧ I ⊆ M.E

Tactic:
exact ⟨fun h ↦ ⟨fun _ ↦ h, h.subset_ground⟩, fun h ↦ h.1 h.2⟩
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
I J : Set α
hJ : M.Indep J
hIJ : I ⊆ J
obtain : ∀ (B : Set α) (hB : M.IsBase B) (hJB : J ⊆ B), M.Indep I
⊢ M.Indep I

Tactic:
obtain ⟨B, hB, hJB⟩ := hJ.exists_isBase_superset

Premises used: Matroid.Indep.exists_isBase_superset
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
I J : Set α
hJ : M.Indep J
hIJ : I ⊆ J
B : Set α
hB : M.IsBase B
hJB : J ⊆ B
⊢ M.Indep I

Tactic:
indep_iff.2 ⟨B, hB, hIJ.trans hJB⟩

Premises used: Iff.mpr, Matroid.indep_iff, HasSubset.Subset.trans, And.intro, Exists.intro
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
I J : Set α
hJ : M.Indep J
hIJ : I ⊆ J
B : Set α
hB : M.IsBase B
hJB : J ⊆ B
⊢ M.Indep I

Tactic:
exact indep_iff.2 ⟨B, hB, hIJ.trans hJB⟩

Premises used: Iff.mpr, Matroid.indep_iff, HasSubset.Subset.trans, And.intro, Exists.intro
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
D X : Set α
hD : M.Dep D
hDX : D ⊆ X
hXE : X ⊆ M.E
⊢ M.Dep X

Tactic:
dep_of_not_indep (fun hI ↦ (hI.subset hDX).not_dep hD)

Premises used: Matroid.Indep.subset, Matroid.dep_of_not_indep, Matroid.Indep.not_dep
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
B : Set α
hB : M.IsBase B
⊢ M.Indep B

Tactic:
indep_iff.2 ⟨B, hB, subset_rfl⟩

Premises used: Iff.mpr, Matroid.indep_iff, And.intro, Exists.intro, subset_rfl
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
⊢ M.Indep ∅

Tactic:
Exists.elim M.exists_isBase (fun _ hB ↦ hB.indep.subset (empty_subset _))

Premises used: Matroid.Indep.subset, Matroid.exists_isBase, Set.empty_subset, Matroid.IsBase.indep, Exists.elim
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
D : Set α
hD : M.Dep D
rw : D ≠ ∅
⊢ D.Nonempty

Tactic:
rw [nonempty_iff_ne_empty]

Premises used: Set.nonempty_iff_ne_empty
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
hD : M.Dep ∅
⊢ False

Tactic:
hD.not_indep M.empty_indep

Premises used: Matroid.Dep.not_indep, Matroid.empty_indep
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
hD : M.Dep ∅
⊢ False

Tactic:
exact hD.not_indep M.empty_indep

Premises used: Matroid.Dep.not_indep, Matroid.empty_indep
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
I : Set α
inst : M.RankFinite
hI : M.Indep I
⊢ I.Finite

Tactic:
let ⟨_, hB, hIB⟩ := hI.exists_isBase_superset
  hB.finite.subset hIB

Premises used: Set.Finite, Set.Finite.subset, _private.0.Matroid.Indep.finite.match_1, Matroid.Indep.exists_isBase_superset, Matroid.IsBase.finite
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
I : Set α
hI : M.Indep I
hne : I.Nonempty
obtain : ∀ (B : Set α) (hB : M.IsBase B) (hIB : I ⊆ B), M.RankPos
⊢ M.RankPos

Tactic:
obtain ⟨B, hB, hIB⟩ := hI.exists_isBase_superset

Premises used: Matroid.Indep.exists_isBase_superset
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
I : Set α
hI : M.Indep I
hne : I.Nonempty
B : Set α
hB : M.IsBase B
hIB : I ⊆ B
⊢ M.RankPos

Tactic:
hB.rankPos_of_nonempty (hne.mono hIB)

Premises used: Matroid.IsBase.rankPos_of_nonempty, Set.Nonempty.mono
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
I : Set α
hI : M.Indep I
hne : I.Nonempty
B : Set α
hB : M.IsBase B
hIB : I ⊆ B
⊢ M.RankPos

Tactic:
exact hB.rankPos_of_nonempty (hne.mono hIB)

Premises used: Matroid.IsBase.rankPos_of_nonempty, Set.Nonempty.mono
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
I : Set α
hI : M.Indep I
X : Set α
⊢ M.Indep (I ∩ X)

Tactic:
hI.subset inter_subset_left

Premises used: Matroid.Indep.subset, Set.inter_subset_left
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
I : Set α
hI : M.Indep I
X : Set α
⊢ M.Indep (X ∩ I)

Tactic:
hI.subset inter_subset_right

Premises used: Matroid.Indep.subset, Set.inter_subset_right
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
I : Set α
hI : M.Indep I
X : Set α
⊢ M.Indep (I \ X)

Tactic:
hI.subset diff_subset

Premises used: Set.diff_subset, Matroid.Indep.subset
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
B I : Set α
hB : M.IsBase B
hI : M.Indep I
hBI : B ⊆ I
B' : Set α
hB' : M.IsBase B'
hB'I rwa rwa₁ rwa₂ rwa₃ : I ⊆ B'
⊢ I ⊆ B

Tactic:
rwa [hB.eq_of_subset_isBase hB' (hBI.trans hB'I)]

Premises used: HasSubset.Subset.trans, Matroid.IsBase.eq_of_subset_isBase
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
B : Set α
rw : M.IsBase B ↔ M.Indep B ∧ ∀ ⦃t : Set α⦄, M.Indep t → B ⊆ t → B = t
⊢ M.IsBase B ↔ Maximal M.Indep B

Tactic:
rw [maximal_subset_iff]

Premises used: maximal_subset_iff
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
B : Set α
⊢ M.IsBase B ↔ M.Indep B ∧ ∀ ⦃t : Set α⦄, M.Indep t → B ⊆ t → B = t

Tactic:
⟨fun h ↦ ⟨h.indep, fun _ ↦ h.eq_of_subset_indep⟩, fun ⟨h, h'⟩ ↦ ?_⟩

Premises used: Matroid.IsBase.eq_of_subset_indep, Matroid.IsBase, _private.0.Matroid.isBase_iff_maximal_indep.match_1, And.intro, Iff.intro, Matroid.IsBase.indep
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
B : Set α
refine :
  (M.Indep B ∧ ∀ ⦃t : Set α⦄, M.Indep t → B ⊆ t → B = t) →
    ∀ (h : M.Indep B) (h' : ∀ ⦃t : Set α⦄, M.Indep t → B ⊆ t → B = t), M.IsBase B
⊢ M.IsBase B ↔ M.Indep B ∧ ∀ ⦃t : Set α⦄, M.Indep t → B ⊆ t → B = t

Tactic:
refine ⟨fun h ↦ ⟨h.indep, fun _ ↦ h.eq_of_subset_indep⟩, fun ⟨h, h'⟩ ↦ ?_⟩
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
B : Set α
h_1 : M.Indep B ∧ ∀ ⦃t : Set α⦄, M.Indep t → B ⊆ t → B = t
h : M.Indep B
h' : ∀ ⦃t : Set α⦄, M.Indep t → B ⊆ t → B = t
obtain : ∀ (B' : Set α) (hB' : M.IsBase B') (hBB' : B ⊆ B'), M.IsBase B
⊢ M.IsBase B

Tactic:
obtain ⟨B', hB', hBB'⟩ := h.exists_isBase_superset

Premises used: Matroid.Indep.exists_isBase_superset
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
B : Set α
h_1 : M.Indep B ∧ ∀ ⦃t : Set α⦄, M.Indep t → B ⊆ t → B = t
h : M.Indep B
h' : ∀ ⦃t : Set α⦄, M.Indep t → B ⊆ t → B = t
B' : Set α
hB' : M.IsBase B'
hBB' : B ⊆ B'
rwa rwa₁ rwa₂ rwa₃ : M.IsBase B'
⊢ M.IsBase B

Tactic:
rwa [h' hB'.indep hBB']

Premises used: Matroid.IsBase.indep
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
I : Set α
hI : M.Indep I
h : ∀ ⦃J : Set α⦄, M.Indep J → I ⊆ J → I = J
rwa : Maximal M.Indep I
rwa₁ : M.Indep I ∧ ∀ ⦃t : Set α⦄, M.Indep t → I ⊆ t → I = t
rwa₂ rwa₃ rwa₄ rwa₅ : ∀ ⦃t : Set α⦄, M.Indep t → I ⊆ t → I = t
⊢ M.IsBase I

Tactic:
rwa [isBase_iff_maximal_indep, maximal_subset_iff, and_iff_right hI]

Premises used: and_iff_right, maximal_subset_iff, Matroid.isBase_iff_maximal_indep
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
B X : Set α
hB : M.IsBase B
h : B ⊂ X
hX : X ⊆ M.E
⊢ M.Dep X

Tactic:
⟨fun hX ↦ h.ne (hB.eq_of_subset_indep hX h.subset), hX⟩

Premises used: Matroid.Dep, Matroid.IsBase.eq_of_subset_indep, HasSSubset.SSubset.subset, HasSSubset.SSubset.ne, And.intro
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
B : Set α
e : α
hB : M.IsBase B
heB : e ∉ B
he : e ∈ M.E
⊢ M.Dep (insert e B)

Tactic:
hB.dep_of_ssubset (ssubset_insert heB) (insert_subset he hB.subset_ground)

Premises used: Set.ssubset_insert, Matroid.IsBase.dep_of_ssubset, Matroid.IsBase.subset_ground, Set.insert_subset
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
B : Set α
e : α
hB : M.IsBase B
heB : M.Indep (insert e B)
⊢ e ∈ B

Tactic:
by_contra fun he ↦ (hB.dep_of_insert he (heB.subset_ground (mem_insert _ _))).not_indep heB

Premises used: Matroid.Dep.not_indep, Matroid.IsBase.dep_of_insert, Matroid.Indep.subset_ground, by_contra, Set.mem_insert
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
B B' : Set α
e : α
hB : M.IsBase B
hB' : M.IsBase B'
h : B \ B' = {e}
obtain : ∀ (f : α) (hf : f ∈ B' \ B) (hb : M.IsBase (insert f (B \ {e}))), ∃ f ∈ B' \ B, B' = insert f B \ {e}
⊢ ∃ f ∈ B' \ B, B' = insert f B \ {e}

Tactic:
obtain ⟨f, hf, hb⟩ := hB.exchange hB' (h.symm.subset (mem_singleton e))

Premises used: Set.mem_singleton, Eq.subset, Matroid.IsBase.exchange, Eq.symm
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
B B' : Set α
hB : M.IsBase B
hB' : M.IsBase B'
f : α
hf : f ∈ B' \ B
h : B \ B' = {f}
hb : M.IsBase (insert f (B \ {f}))
⊢ False

Tactic:
hf.2 (h.symm.subset (mem_singleton f)).1

Premises used: Set.mem_singleton, Eq.subset, And.right, And.left, Eq.symm
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
B B' : Set α
hB : M.IsBase B
hB' : M.IsBase B'
f : α
hf : f ∈ B' \ B
h : B \ B' = {f}
hb : M.IsBase (insert f (B \ {f}))
⊢ False

Tactic:
exact hf.2 (h.symm.subset (mem_singleton f)).1

Premises used: Set.mem_singleton, Eq.subset, And.right, And.left, Eq.symm
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
B B' : Set α
e : α
hB : M.IsBase B
hB' : M.IsBase B'
h : B \ B' = {e}
f : α
hf : f ∈ B' \ B
hb : M.IsBase (insert f (B \ {e}))
⊢ f ≠ e

Tactic:
have hne : f ≠ e := by rintro rfl; exact hf.2 (h.symm.subset (mem_singleton f)).1
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
B B' : Set α
e : α
hB : M.IsBase B
hB' : M.IsBase B'
h : B \ B' = {e}
f : α
hf : f ∈ B' \ B
hb : M.IsBase (insert f (B \ {e}))
hne : f ≠ e
⊢ M.IsBase (insert f B \ {e})

Tactic:
rw [insert_diff_singleton_comm hne] at hb

Premises used: Set.insert_diff_singleton_comm