awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
hb₁ : M.IsBase (insert f B \ {e})
⊢ f ≠ e

Tactic:
rw [insert_diff_singleton_comm hne] at hb

Premises used: Set.insert_diff_singleton_comm
-- 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
⊢ ∃ f ∈ B' \ B, B' = insert f B \ {e}

Tactic:
⟨f, hf, (hb.eq_of_subset_isBase hB' ?_).symm⟩

Premises used: Matroid.IsBase.eq_of_subset_isBase, And.intro, Exists.intro, 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})
hne : f ≠ e
refine : insert f B \ {e} ⊆ B'
⊢ ∃ f ∈ B' \ B, B' = insert f B \ {e}

Tactic:
refine ⟨f, hf, (hb.eq_of_subset_isBase hB' ?_).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})
hne : f ≠ e
rw : f ∈ B' ∪ {e}
⊢ insert f B \ {e} ⊆ B'

Tactic:
rw [diff_subset_iff, insert_subset_iff, union_comm, ← diff_subset_iff, h, and_iff_left rfl.subset]

Premises used: Set.diff_subset_iff, and_iff_left, Set.union_comm, Eq.subset, Set.insert_subset_iff, rfl
-- 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
⊢ f ∈ B' ∪ {e}

Tactic:
Or.inl hf.1

Premises used: Set.union, Set.Mem, setOf, And.left, Or.inl
-- 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
⊢ f ∈ B' ∪ {e}

Tactic:
exact Or.inl hf.1

Premises used: And.left, Or.inl
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
B : Set α
e f : α
hB : M.IsBase B
hf : f ∉ B
hI : M.Indep (insert f (B \ {e}))
obtain : ∀ (B' : Set α) (hB' : M.IsBase B') (hIB' : insert f (B \ {e}) ⊆ B'), M.IsBase (insert f (B \ {e}))
⊢ M.IsBase (insert f (B \ {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 α
B : Set α
e f : α
hB : M.IsBase B
hf : f ∉ B
hI : M.Indep (insert f (B \ {e}))
B' : Set α
hB' : M.IsBase B'
hIB' : insert f (B \ {e}) ⊆ B'
⊢ (B' \ B).encard = (B \ B').encard

Tactic:
have hcard := hB'.encard_diff_comm hB
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
B : Set α
e f : α
hB : M.IsBase B
hf : f ∉ B
hI : M.Indep (insert f (B \ {e}))
B' : Set α
hB' : M.IsBase B'
hIB' : insert f (B \ {e}) ⊆ B'
hcard : (B' \ B).encard = (B \ B').encard
⊢ f ∈ B' ∧ (B \ B' = ∅ ∨ B \ B' = {e})

Tactic:
rw [insert_subset_iff, ← diff_eq_empty, diff_diff_comm, diff_eq_empty, subset_singleton_iff_eq]
    at hIB'

Premises used: Set.diff_diff_comm, Set.insert_subset_iff, Set.subset_singleton_iff_eq, Set.diff_eq_empty
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
B : Set α
e f : α
hB : M.IsBase B
hf : f ∉ B
hI : M.Indep (insert f (B \ {e}))
B' : Set α
hB' : M.IsBase B'
hIB' : insert f (B \ {e}) ⊆ B'
hcard : (B' \ B).encard = (B \ B').encard
hIB'₁ : f ∈ B' ∧ (B \ B' = ∅ ∨ B \ B' = {e})
⊢ (B' \ B).encard = (B \ B').encard

Tactic:
rw [insert_subset_iff, ← diff_eq_empty, diff_diff_comm, diff_eq_empty, subset_singleton_iff_eq]
    at hIB'

Premises used: Set.diff_diff_comm, Set.insert_subset_iff, Set.subset_singleton_iff_eq, Set.diff_eq_empty
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
B : Set α
e f : α
hB : M.IsBase B
hf : f ∉ B
hI : M.Indep (insert f (B \ {e}))
B' : Set α
hB' : M.IsBase B'
hIB' : f ∈ B' ∧ (B \ B' = ∅ ∨ B \ B' = {e})
hcard : (B' \ B).encard = (B \ B').encard
inl : ∀ (hfB : f ∈ B') (h : B \ B' = ∅), M.IsBase (insert f (B \ {e}))
inr : ∀ (hfB : f ∈ B') (h : B \ B' = {e}), M.IsBase (insert f (B \ {e}))
⊢ M.IsBase (insert f (B \ {e}))

Tactic:
obtain ⟨hfB, (h | h)⟩ := hIB'
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
B : Set α
e f : α
hB : M.IsBase B
hf : f ∉ B
hI : M.Indep (insert f (B \ {e}))
B' : Set α
hB' : M.IsBase B'
hcard : (B' \ B).encard = (B \ B').encard
hfB : f ∈ B'
h : B \ B' = ∅
⊢ ∀ (x : α), x ∉ B' \ B

Tactic:
rw [h, encard_empty, encard_eq_zero, eq_empty_iff_forall_notMem] at hcard

Premises used: Set.encard_eq_zero, Set.encard_empty, Set.eq_empty_iff_forall_notMem
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
B : Set α
e f : α
hB : M.IsBase B
hf : f ∉ B
hI : M.Indep (insert f (B \ {e}))
B' : Set α
hB' : M.IsBase B'
hcard : (B' \ B).encard = (B \ B').encard
hfB : f ∈ B'
h : B \ B' = ∅
hcard₁ : ∀ (x : α), x ∉ B' \ B
⊢ f ∈ B'

Tactic:
rw [h, encard_empty, encard_eq_zero, eq_empty_iff_forall_notMem] at hcard

Premises used: Set.encard_eq_zero, Set.encard_empty, Set.eq_empty_iff_forall_notMem
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
B : Set α
e f : α
hB : M.IsBase B
hf : f ∉ B
hI : M.Indep (insert f (B \ {e}))
B' : Set α
hB' : M.IsBase B'
hcard : (B' \ B).encard = (B \ B').encard
hfB : f ∈ B'
h : B \ B' = ∅
hcard₁ : ∀ (x : α), x ∉ B' \ B
hfB₁ : f ∈ B'
⊢ B \ B' = ∅

Tactic:
rw [h, encard_empty, encard_eq_zero, eq_empty_iff_forall_notMem] at hcard

Premises used: Set.encard_eq_zero, Set.encard_empty, Set.eq_empty_iff_forall_notMem
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
B : Set α
e f : α
hB : M.IsBase B
hf : f ∉ B
hI : M.Indep (insert f (B \ {e}))
B' : Set α
hB' : M.IsBase B'
hcard : ∀ (x : α), x ∉ B' \ B
hfB : f ∈ B'
h : B \ B' = ∅
⊢ M.IsBase (insert f (B \ {e}))

Tactic:
(hcard f ⟨hfB, hf⟩).elim

Premises used: False.elim, And.intro
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
B : Set α
e f : α
hB : M.IsBase B
hf : f ∉ B
hI : M.Indep (insert f (B \ {e}))
B' : Set α
hB' : M.IsBase B'
hcard : ∀ (x : α), x ∉ B' \ B
hfB : f ∈ B'
h : B \ B' = ∅
⊢ M.IsBase (insert f (B \ {e}))

Tactic:
exact (hcard f ⟨hfB, hf⟩).elim

Premises used: False.elim, And.intro
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
B : Set α
e f : α
hB : M.IsBase B
hf : f ∉ B
hI : M.Indep (insert f (B \ {e}))
B' : Set α
hB' : M.IsBase B'
hcard : (B' \ B).encard = (B \ B').encard
hfB : f ∈ B'
h : B \ B' = {e}
⊢ ∃ (x : α), B' \ B = {x}

Tactic:
rw [h, encard_singleton, encard_eq_one] at hcard

Premises used: Set.encard_eq_one, Set.encard_singleton
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
B : Set α
e f : α
hB : M.IsBase B
hf : f ∉ B
hI : M.Indep (insert f (B \ {e}))
B' : Set α
hB' : M.IsBase B'
hcard : (B' \ B).encard = (B \ B').encard
hfB : f ∈ B'
h : B \ B' = {e}
hcard₁ : ∃ (x : α), B' \ B = {x}
⊢ f ∈ B'

Tactic:
rw [h, encard_singleton, encard_eq_one] at hcard

Premises used: Set.encard_eq_one, Set.encard_singleton
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
B : Set α
e f : α
hB : M.IsBase B
hf : f ∉ B
hI : M.Indep (insert f (B \ {e}))
B' : Set α
hB' : M.IsBase B'
hcard : (B' \ B).encard = (B \ B').encard
hfB : f ∈ B'
h : B \ B' = {e}
hcard₁ : ∃ (x : α), B' \ B = {x}
hfB₁ : f ∈ B'
⊢ B \ B' = {e}

Tactic:
rw [h, encard_singleton, encard_eq_one] at hcard

Premises used: Set.encard_eq_one, Set.encard_singleton
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
B : Set α
e f : α
hB : M.IsBase B
hf : f ∉ B
hI : M.Indep (insert f (B \ {e}))
B' : Set α
hB' : M.IsBase B'
hcard : ∃ (x : α), B' \ B = {x}
hfB : f ∈ B'
h : B \ B' = {e}
inr : ∀ (x : α) (hx : B' \ B = {x}), M.IsBase (insert f (B \ {e}))
⊢ M.IsBase (insert f (B \ {e}))

Tactic:
obtain ⟨x, hx⟩ := hcard
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
B : Set α
e f : α
hB : M.IsBase B
hf : f ∉ B
hI : M.Indep (insert f (B \ {e}))
B' : Set α
hB' : M.IsBase B'
hfB : f ∈ B'
h : B \ B' = {e}
x : α
hx : B' \ B = {x}
⊢ B' \ B = {f}

Tactic:
obtain (rfl : f = x) := hx.subset ⟨hfB, hf⟩

Premises used: Eq.subset, And.intro, rfl
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
B : Set α
e f : α
hB : M.IsBase B
hf : f ∉ B
hI : M.Indep (insert f (B \ {e}))
B' : Set α
hB' : M.IsBase B'
hfB : f ∈ B'
h : B \ B' = {e}
hx : B' \ B = {f}
inr : M.IsBase B'
⊢ M.IsBase (insert f (B \ {e}))

Tactic:
simp_rw [← h, ← singleton_union, ← hx, sdiff_sdiff_right_self, inf_eq_inter, inter_comm B,
    diff_union_inter]

Premises used: Set.singleton_union, Set.inter_comm, Set.diff_union_inter, Set.inf_eq_inter, sdiff_sdiff_right_self
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
B : Set α
e f : α
hB : M.IsBase B
hf : f ∉ B
hI : M.Indep (insert f (B \ {e}))
B' : Set α
hB' : M.IsBase B'
hfB : f ∈ B'
h : B \ B' = {e}
hx : B' \ B = {f}
⊢ M.IsBase B'

Tactic:
hB'
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
B : Set α
e f : α
hB : M.IsBase B
hf : f ∉ B
hI : M.Indep (insert f (B \ {e}))
B' : Set α
hB' : M.IsBase B'
hfB : f ∈ B'
h : B \ B' = {e}
hx : B' \ B = {f}
⊢ M.IsBase B'

Tactic:
exact hB'
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
B : Set α
e f : α
hB : M.IsBase B
he : e ∈ B
hf : f ∉ B
hI : M.Indep (insert f B \ {e})
⊢ f ≠ e

Tactic:
have hfe : f ≠ e := ne_of_mem_of_not_mem he hf |>.symm
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
B : Set α
e f : α
hB : M.IsBase B
he : e ∈ B
hf : f ∉ B
hI : M.Indep (insert f B \ {e})
hfe : f ≠ e
rw : ∀ (hI : M.Indep (insert f (B \ {e}))) (hfe : f ≠ e), M.IsBase (insert f (B \ {e}))
⊢ M.IsBase (insert f B \ {e})

Tactic:
rw [← insert_diff_singleton_comm hfe] at *

Premises used: Set.insert_diff_singleton_comm
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
B : Set α
e f : α
hB : M.IsBase B
he : e ∈ B
hf : f ∉ B
hI : M.Indep (insert f (B \ {e}))
hfe : f ≠ e
⊢ M.IsBase (insert f (B \ {e}))

Tactic:
hB.exchange_isBase_of_indep hf hI

Premises used: Matroid.IsBase.exchange_isBase_of_indep
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
B : Set α
e f : α
hB : M.IsBase B
he : e ∈ B
hf : f ∉ B
hI : M.Indep (insert f (B \ {e}))
hfe : f ≠ e
⊢ M.IsBase (insert f (B \ {e}))

Tactic:
exact hB.exchange_isBase_of_indep hf hI

Premises used: Matroid.IsBase.exchange_isBase_of_indep
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
I : Set α
e f : α
he : e ∉ I
hf : f ∉ I
heI : M.IsBase (insert e I)
hfI : M.Indep (insert f I)
inl : ∀ (hf : e ∉ I) (hfI : M.Indep (insert e I)), M.IsBase (insert e I)
inr : ∀ (hef : e ≠ f), M.IsBase (insert f I)
⊢ M.IsBase (insert f I)

Tactic:
obtain rfl | hef := eq_or_ne e f

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
I : Set α
e : α
he : e ∉ I
heI : M.IsBase (insert e I)
hf : e ∉ I
hfI : M.Indep (insert e I)
⊢ M.IsBase (insert e I)

Tactic:
assumption
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
I : Set α
e f : α
he : e ∉ I
hf : f ∉ I
heI : M.IsBase (insert e I)
hfI : M.Indep (insert f I)
hef : e ≠ f
⊢ f ∉ insert e I

Tactic:
simp [hef.symm, hf]

Premises used: Ne.symm
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
I : Set α
e f : α
he : e ∉ I
hf : f ∉ I
heI : M.IsBase (insert e I)
hfI : M.Indep (insert f I)
hef : e ≠ f
⊢ M.IsBase (insert f I)

Tactic:
simpa [diff_singleton_eq_self he, hfI]
    using heI.exchange_isBase_of_indep (e := e) (f := f) (by simp [hef.symm, hf])

Premises used: Set.diff_singleton_eq_self, Matroid.IsBase.exchange_isBase_of_indep
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
B : Set α
e : α
hB : M.IsBase B
h : e ∈ M.E \ B
rw : ¬M.Indep (insert e B)
⊢ M.Dep (insert e B)

Tactic:
rw [← not_indep_iff (insert_subset h.1 hB.subset_ground)]

Premises used: Matroid.IsBase.subset_ground, And.left, Matroid.not_indep_iff, Set.insert_subset
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
B : Set α
e : α
hB : M.IsBase B
h : e ∈ M.E \ B
⊢ ¬M.Indep (insert e B)

Tactic:
h.2 ∘ (fun hi ↦ insert_eq_self.mp (hB.eq_of_subset_indep hi (subset_insert e B)).symm)

Premises used: Matroid.IsBase.eq_of_subset_indep, Function.comp, And.right, Iff.mp, Eq.symm, Set.insert_eq_self, Not, Set.subset_insert
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
B : Set α
e : α
hB : M.IsBase B
h : e ∈ M.E \ B
⊢ ¬M.Indep (insert e B)

Tactic:
exact h.2 ∘ (fun hi ↦ insert_eq_self.mp (hB.eq_of_subset_indep hi (subset_insert e B)).symm)

Premises used: Matroid.IsBase.eq_of_subset_indep, And.right, Iff.mp, Eq.symm, Set.insert_eq_self, Set.subset_insert
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
B I : Set α
hI : M.Indep I
hI' : ¬M.IsBase I
hB : M.IsBase B
obtain : ∀ (B' : Set α) (hB' : M.IsBase B') (hIB' : I ⊆ B'), ∃ e ∈ B \ I, M.Indep (insert e I)
⊢ ∃ e ∈ B \ I, M.Indep (insert e I)

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 α
B I : Set α
hI : M.Indep I
hI' : ¬M.IsBase I
hB : M.IsBase B
hB' : M.IsBase I
hIB' : I ⊆ I
⊢ False

Tactic:
hI' hB'
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
B I : Set α
hI : M.Indep I
hI' : ¬M.IsBase I
hB : M.IsBase B
hB' : M.IsBase I
hIB' : I ⊆ I
⊢ False

Tactic:
exact hI' hB'
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
B I : Set α
hI : M.Indep I
hI' : ¬M.IsBase I
hB : M.IsBase B
B' : Set α
hB' : M.IsBase B'
hIB' : I ⊆ B'
obtain : ∀ (x : α) (hxB' : x ∈ B') (hx : x ∉ I), ∃ e ∈ B \ I, M.Indep (insert e I)
⊢ ∃ e ∈ B \ I, M.Indep (insert e I)

Tactic:
obtain ⟨x, hxB', hx⟩ := exists_of_ssubset (hIB'.ssubset_of_ne (by (rintro rfl; exact hI' hB')))

Premises used: Set.exists_of_ssubset, HasSubset.Subset.ssubset_of_ne
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
B I : Set α
hI : M.Indep I
hI' : ¬M.IsBase I
hB : M.IsBase B
B' : Set α
hB' : M.IsBase B'
hIB' : I ⊆ B'
x : α
hxB' : x ∈ B'
hx : x ∉ I
pos : ∀ (hxB : x ∈ B), ∃ e ∈ B \ I, M.Indep (insert e I)
neg : ∀ (hxB : x ∉ B), ∃ e ∈ B \ I, M.Indep (insert e I)
⊢ ∃ e ∈ B \ I, M.Indep (insert e I)

Tactic:
by_cases hxB : x ∈ B
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
B I : Set α
hI : M.Indep I
hI' : ¬M.IsBase I
hB : M.IsBase B
B' : Set α
hB' : M.IsBase B'
hIB' : I ⊆ B'
x : α
hxB' : x ∈ B'
hx : x ∉ I
hxB : x ∈ B
⊢ ∃ e ∈ B \ I, M.Indep (insert e I)

Tactic:
⟨x, ⟨hxB, hx⟩, hB'.indep.subset (insert_subset hxB' hIB')⟩

Premises used: Matroid.Indep.subset, And.intro, Exists.intro, Matroid.IsBase.indep, Set.insert_subset
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
B I : Set α
hI : M.Indep I
hI' : ¬M.IsBase I
hB : M.IsBase B
B' : Set α
hB' : M.IsBase B'
hIB' : I ⊆ B'
x : α
hxB' : x ∈ B'
hx : x ∉ I
hxB : x ∈ B
⊢ ∃ e ∈ B \ I, M.Indep (insert e I)

Tactic:
exact ⟨x, ⟨hxB, hx⟩, hB'.indep.subset (insert_subset hxB' hIB')⟩
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
B I : Set α
hI : M.Indep I
hI' : ¬M.IsBase I
hB : M.IsBase B
B' : Set α
hB' : M.IsBase B'
hIB' : I ⊆ B'
x : α
hxB' : x ∈ B'
hx : x ∉ I
hxB : x ∉ B
neg : ∀ (e : α) (he : e ∈ B \ B') (hBase : M.IsBase (insert e (B' \ {x}))), ∃ e ∈ B \ I, M.Indep (insert e I)
⊢ ∃ e ∈ B \ I, M.Indep (insert e I)

Tactic:
obtain ⟨e, he, hBase⟩ := hB'.exchange hB ⟨hxB', hxB⟩

Premises used: Matroid.IsBase.exchange, And.intro
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
B I : Set α
hI : M.Indep I
hI' : ¬M.IsBase I
hB : M.IsBase B
B' : Set α
hB' : M.IsBase B'
hIB' : I ⊆ B'
x : α
hxB' : x ∈ B'
hx : x ∉ I
hxB : x ∉ B
e : α
he : e ∈ B \ B'
hBase : M.IsBase (insert e (B' \ {x}))
⊢ ∃ e ∈ B \ I, M.Indep (insert e I)

Tactic:
⟨e, ⟨he.1, notMem_subset hIB' he.2⟩,
    indep_iff.2 ⟨_, hBase, insert_subset_insert (subset_diff_singleton hIB' hx)⟩⟩

Premises used: Iff.mpr, Matroid.indep_iff, And.right, And.left, Set.subset_diff_singleton, And.intro, Exists.intro, Set.insert_subset_insert, Set.notMem_subset
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
B I : Set α
hI : M.Indep I
hI' : ¬M.IsBase I
hB : M.IsBase B
B' : Set α
hB' : M.IsBase B'
hIB' : I ⊆ B'
x : α
hxB' : x ∈ B'
hx : x ∉ I
hxB : x ∉ B
e : α
he : e ∈ B \ B'
hBase : M.IsBase (insert e (B' \ {x}))
⊢ ∃ e ∈ B \ I, M.Indep (insert e I)

Tactic:
exact ⟨e, ⟨he.1, notMem_subset hIB' he.2⟩,
    indep_iff.2 ⟨_, hBase, insert_subset_insert (subset_diff_singleton hIB' hx)⟩⟩
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
I B : Set α
hI : M.Indep I
hInotmax : ¬Maximal M.Indep I
hB : Maximal M.Indep B
⊢ M.Indep B ∧ ∀ ⦃t : Set α⦄, M.Indep t → B ⊆ t → B = t

Tactic:
simp only [maximal_subset_iff, hI, not_and, not_forall, exists_prop, true_imp_iff] at hB hInotmax

Premises used: exists_prop, true_imp_iff, maximal_subset_iff, not_and, Classical.not_forall
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
I B : Set α
hI : M.Indep I
hInotmax : ¬Maximal M.Indep I
hB : Maximal M.Indep B
hB₁ : M.Indep B ∧ ∀ ⦃t : Set α⦄, M.Indep t → B ⊆ t → B = t
⊢ ∃ (x : Set α), M.Indep x ∧ I ⊆ x ∧ ¬I = x

Tactic:
simp only [maximal_subset_iff, hI, not_and, not_forall, exists_prop, true_imp_iff] at hB hInotmax

Premises used: exists_prop, true_imp_iff, maximal_subset_iff, not_and, Classical.not_forall
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
I B : Set α
hI : M.Indep I
hB : M.Indep B ∧ ∀ ⦃t : Set α⦄, M.Indep t → B ⊆ t → B = t
hInotmax : ∃ (x : Set α), M.Indep x ∧ I ⊆ x ∧ ¬I = x
⊢ ∃ x ∈ B \ I, M.Indep (insert x I)

Tactic:
hI.exists_insert_of_not_isBase (fun hIb ↦ ?_) ?_

Premises used: Matroid.Indep.exists_insert_of_not_isBase
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
I B : Set α
hI : M.Indep I
hB : M.Indep B ∧ ∀ ⦃t : Set α⦄, M.Indep t → B ⊆ t → B = t
hInotmax : ∃ (x : Set α), M.Indep x ∧ I ⊆ x ∧ ¬I = x
refine_1 : ∀ (hIb : M.IsBase I), False
refine_2 : M.IsBase B
⊢ ∃ x ∈ B \ I, M.Indep (insert x I)

Tactic:
refine hI.exists_insert_of_not_isBase (fun hIb ↦ ?_) ?_

Premises used: Matroid.Indep.exists_insert_of_not_isBase
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
I B : Set α
hI : M.Indep I
hB : M.Indep B ∧ ∀ ⦃t : Set α⦄, M.Indep t → B ⊆ t → B = t
hInotmax : ∃ (x : Set α), M.Indep x ∧ I ⊆ x ∧ ¬I = x
hIb : M.IsBase I
refine_1 : ∀ (I' : Set α) (hII' : M.Indep I') (hI' : I ⊆ I') (hne : ¬I = I'), False
⊢ False

Tactic:
obtain ⟨I', hII', hI', hne⟩ := hInotmax
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
I B : Set α
hI : M.Indep I
hB : M.Indep B ∧ ∀ ⦃t : Set α⦄, M.Indep t → B ⊆ t → B = t
hIb : M.IsBase I
I' : Set α
hII' : M.Indep I'
hI' : I ⊆ I'
hne : ¬I = I'
⊢ False

Tactic:
hne <| hIb.eq_of_subset_indep hII' hI'

Premises used: Matroid.IsBase.eq_of_subset_indep
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
I B : Set α
hI : M.Indep I
hB : M.Indep B ∧ ∀ ⦃t : Set α⦄, M.Indep t → B ⊆ t → B = t
hIb : M.IsBase I
I' : Set α
hII' : M.Indep I'
hI' : I ⊆ I'
hne : ¬I = I'
⊢ False

Tactic:
exact hne <| hIb.eq_of_subset_indep hII' hI'

Premises used: Matroid.IsBase.eq_of_subset_indep
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
I B : Set α
hI : M.Indep I
hB : M.Indep B ∧ ∀ ⦃t : Set α⦄, M.Indep t → B ⊆ t → B = t
hInotmax : ∃ (x : Set α), M.Indep x ∧ I ⊆ x ∧ ¬I = x
⊢ M.IsBase B

Tactic:
hB.1.isBase_of_maximal fun J hJ hBJ ↦ hB.2 hJ hBJ

Premises used: Matroid.Indep.isBase_of_maximal, And.right, And.left
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
I B : Set α
hI : M.Indep I
hB : M.Indep B ∧ ∀ ⦃t : Set α⦄, M.Indep t → B ⊆ t → B = t
hInotmax : ∃ (x : Set α), M.Indep x ∧ I ⊆ x ∧ ¬I = x
⊢ M.IsBase B

Tactic:
exact hB.1.isBase_of_maximal fun J hJ hBJ ↦ hB.2 hJ hBJ

Premises used: Matroid.Indep.isBase_of_maximal, And.right, And.left
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
B : Set α
hB : M.Indep B
hBmax : ∀ e ∈ M.E \ B, ¬M.Indep (insert e B)
by_contra : ∀ (hnb : ¬M.IsBase B), False
⊢ M.IsBase B

Tactic:
by_contra hnb
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
B : Set α
hB : M.Indep B
hBmax : ∀ e ∈ M.E \ B, ¬M.Indep (insert e B)
hnb : ¬M.IsBase B
obtain : ∀ (B' : Set α) (hB' : M.IsBase B'), False
⊢ False

Tactic:
obtain ⟨B', hB'⟩ := M.exists_isBase

Premises used: Matroid.exists_isBase
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
B : Set α
hB : M.Indep B
hBmax : ∀ e ∈ M.E \ B, ¬M.Indep (insert e B)
hnb : ¬M.IsBase B
B' : Set α
hB' : M.IsBase B'
obtain : ∀ (e : α) (he : e ∈ B' \ B) (h : M.Indep (insert e B)), False
⊢ False

Tactic:
obtain ⟨e, he, h⟩ := hB.exists_insert_of_not_isBase hnb hB'

Premises used: Matroid.Indep.exists_insert_of_not_isBase
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
B : Set α
hB : M.Indep B
hBmax : ∀ e ∈ M.E \ B, ¬M.Indep (insert e B)
hnb : ¬M.IsBase B
B' : Set α
hB' : M.IsBase B'
e : α
he : e ∈ B' \ B
h : M.Indep (insert e B)
⊢ False

Tactic:
hBmax e ⟨hB'.subset_ground he.1, he.2⟩ h

Premises used: Matroid.IsBase.subset_ground, And.right, And.left, And.intro
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
B : Set α
hB : M.Indep B
hBmax : ∀ e ∈ M.E \ B, ¬M.Indep (insert e B)
hnb : ¬M.IsBase B
B' : Set α
hB' : M.IsBase B'
e : α
he : e ∈ B' \ B
h : M.Indep (insert e B)
⊢ False

Tactic:
exact hBmax e ⟨hB'.subset_ground he.1, he.2⟩ h

Premises used: Matroid.IsBase.subset_ground, And.right, And.left, And.intro
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
⊢ M.Indep M.E ↔ M.IsBase M.E

Tactic:
⟨fun h ↦ h.isBase_of_maximal (fun _ hJ hEJ ↦ hEJ.antisymm hJ.subset_ground), IsBase.indep⟩

Premises used: Matroid.Indep.isBase_of_maximal, Matroid.Indep.subset_ground, HasSubset.Subset.antisymm, Iff.intro, Matroid.IsBase.indep
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M : Matroid α
B B' I : Set α
hB : M.IsBase B
hIB : I ⊂ B
hB' : M.IsBase B'
⊢ ∃ e ∈ B' \ I, M.Indep (insert e I)

Tactic:
(hB.indep.subset hIB.subset).exists_insert_of_not_isBase
    (fun hI ↦ hIB.ne (hI.eq_of_subset_isBase hB hIB.subset)) hB'

Premises used: Matroid.Indep.subset, HasSSubset.SSubset.subset, Matroid.IsBase.eq_of_subset_isBase, Matroid.Indep.exists_insert_of_not_isBase, HasSSubset.SSubset.ne, Matroid.IsBase.indep
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
h : ∀ ⦃I : Set α⦄, I ⊆ M₁.E → (M₁.Indep I ↔ M₂.Indep I)
h₁ : ∀ (I : Set α), M₁.Indep I ↔ M₂.Indep I
⊢ M₁.Indep = M₂.Indep

Tactic:
ext I
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
h : ∀ ⦃I : Set α⦄, I ⊆ M₁.E → (M₁.Indep I ↔ M₂.Indep I)
I : Set α
pos : ∀ (hI : I ⊆ M₁.E), M₁.Indep I ↔ M₂.Indep I
neg : ∀ (hI : ¬I ⊆ M₁.E), M₁.Indep I ↔ M₂.Indep I
⊢ M₁.Indep I ↔ M₂.Indep I

Tactic:
by_cases hI : I ⊆ M₁.E

Premises used: Matroid.E
-- Module: Mathlib.Combinatorics.Matroid.Basic
Goal:
α : Type u_1
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
h : ∀ ⦃I : Set α⦄, I ⊆ M₁.E → (M₁.Indep I ↔ M₂.Indep I)
I : Set α
hI : I ⊆ M₁.E
pos : M₂.Indep I ↔ M₂.Indep I
pos₁ : I ⊆ M₁.E
pos₂ : M₂.Indep I ↔ M₂.Indep I
pos₃ pos₄ pos₅ : I ⊆ M₁.E
⊢ M₁.Indep I ↔ M₂.Indep I

Tactic:
rwa [h]