awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.Matroid.Dual
Goal:
α : Type u_1
M : Matroid α
B X : Set α
hB : M.IsBase B
hBX : M.IsBasis (B ∩ X) X
⊢ ∃ (B_1 : Set α), M.IsBase B_1 ∧ Disjoint (M.E \ B ∩ (M.E \ X)) B_1

Tactic:
exact ⟨B, hB, disjoint_of_subset_left inter_subset_left disjoint_sdiff_left⟩
-- Module: Mathlib.Combinatorics.Matroid.Dual
Goal:
α : Type u_1
M : Matroid α
B X : Set α
hB : M.IsBase B
hBX : M.IsBasis (B ∩ X) X
e : α
he : e ∈ (M.E \ X) \ (M.E \ B ∩ (M.E \ X))
⊢ (e ∈ M.E ∧ e ∉ X) ∧ e ∈ B

Tactic:
simp only [diff_inter_self_eq_diff, mem_diff, not_and, not_not, imp_iff_right he.1.1] at he

Premises used: Classical.not_not, imp_iff_right, Set.diff_inter_self_eq_diff, And.left, Set.mem_diff, not_and
-- Module: Mathlib.Combinatorics.Matroid.Dual
Goal:
α : Type u_1
M : Matroid α
B X : Set α
hB : M.IsBase B
hBX : M.IsBasis (B ∩ X) X
e : α
he : (e ∈ M.E ∧ e ∉ X) ∧ e ∈ B
refine_2 : ∀ (B_1 : Set α), M.IsBase B_1 → (insert e (M.E \ B ∩ (M.E \ X)) ∩ B_1).Nonempty
⊢ M✶.Dep (insert e (M.E \ B ∩ (M.E \ X)))

Tactic:
simp_rw [dual_dep_iff_forall, insert_subset_iff, and_iff_right he.1.1,
    and_iff_left (inter_subset_left.trans diff_subset)]

Premises used: Set.diff_subset, and_iff_left, Matroid.dual_dep_iff_forall, HasSubset.Subset.trans, Set.inter_subset_left, and_iff_right, Set.insert_subset_iff, And.left
-- Module: Mathlib.Combinatorics.Matroid.Dual
Goal:
α : Type u_1
M : Matroid α
B X : Set α
hB : M.IsBase B
hBX : M.IsBasis (B ∩ X) X
e : α
he : (e ∈ M.E ∧ e ∉ X) ∧ e ∈ B
⊢ ∀ (B_1 : Set α), M.IsBase B_1 → (insert e (M.E \ B ∩ (M.E \ X)) ∩ B_1).Nonempty

Tactic:
fun B' hB' ↦ by_contra (fun hem ↦ ?_)

Premises used: by_contra
-- Module: Mathlib.Combinatorics.Matroid.Dual
Goal:
α : Type u_1
M : Matroid α
B X : Set α
hB : M.IsBase B
hBX : M.IsBasis (B ∩ X) X
e : α
he : (e ∈ M.E ∧ e ∉ X) ∧ e ∈ B
refine_2 : ∀ (B' : Set α) (hB' : M.IsBase B') (hem : ¬(insert e (M.E \ B ∩ (M.E \ X)) ∩ B').Nonempty), False
⊢ ∀ (B_1 : Set α), M.IsBase B_1 → (insert e (M.E \ B ∩ (M.E \ X)) ∩ B_1).Nonempty

Tactic:
refine fun B' hB' ↦ by_contra (fun hem ↦ ?_)

Premises used: by_contra
-- Module: Mathlib.Combinatorics.Matroid.Dual
Goal:
α : Type u_1
M : Matroid α
B X : Set α
hB : M.IsBase B
hBX : M.IsBasis (B ∩ X) X
e : α
he : (e ∈ M.E ∧ e ∉ X) ∧ e ∈ B
B' : Set α
hB' : M.IsBase B'
hem : ¬(insert e (M.E \ B ∩ (M.E \ X)) ∩ B').Nonempty
⊢ B' ⊆ B ∪ X ∧ e ∉ B'

Tactic:
rw [nonempty_iff_ne_empty, not_ne_iff, ← union_singleton, diff_inter_diff,
    union_inter_distrib_right, union_empty_iff, singleton_inter_eq_empty, diff_eq,
    inter_right_comm, inter_eq_self_of_subset_right hB'.subset_ground, ← diff_eq,
    diff_eq_empty] at hem

Premises used: Set.singleton_inter_eq_empty, Set.union_empty_iff, Set.diff_eq, not_ne_iff, Matroid.IsBase.subset_ground, Set.inter_right_comm, Set.inter_eq_self_of_subset_right, Set.nonempty_iff_ne_empty, Set.union_inter_distrib_right, Set.union_singleton, Set.diff_inter_diff, Set.diff_eq_empty
-- Module: Mathlib.Combinatorics.Matroid.Dual
Goal:
α : Type u_1
M : Matroid α
B X : Set α
hB : M.IsBase B
hBX : M.IsBasis (B ∩ X) X
e : α
he : (e ∈ M.E ∧ e ∉ X) ∧ e ∈ B
B' : Set α
hB' : M.IsBase B'
hem : B' ⊆ B ∪ X ∧ e ∉ B'
refine_2 : ∀ (f : α) (hfb : f ∈ B' \ B) (hBf : M.IsBase (insert f (B \ {e}))), False
⊢ False

Tactic:
obtain ⟨f, hfb, hBf⟩ := hB.exchange hB' ⟨he.2, hem.2⟩

Premises used: And.right, Matroid.IsBase.exchange, And.intro
-- Module: Mathlib.Combinatorics.Matroid.Dual
Goal:
α : Type u_1
M : Matroid α
B X : Set α
hB : M.IsBase B
hBX : M.IsBasis (B ∩ X) X
e : α
he : (e ∈ M.E ∧ e ∉ X) ∧ e ∈ B
B' : Set α
hB' : M.IsBase B'
hem : B' ⊆ B ∪ X ∧ e ∉ B'
f : α
hfb : f ∈ B' \ B
hBf : M.IsBase (insert f (B \ {e}))
⊢ M.Indep (insert f (B ∩ X))

Tactic:
hBf.indep.subset (insert_subset_insert ?_)

Premises used: Matroid.Indep.subset, Matroid.IsBase.indep, Set.insert_subset_insert
-- Module: Mathlib.Combinatorics.Matroid.Dual
Goal:
α : Type u_1
M : Matroid α
B X : Set α
hB : M.IsBase B
hBX : M.IsBasis (B ∩ X) X
e : α
he : (e ∈ M.E ∧ e ∉ X) ∧ e ∈ B
B' : Set α
hB' : M.IsBase B'
hem : B' ⊆ B ∪ X ∧ e ∉ B'
f : α
hfb : f ∈ B' \ B
hBf : M.IsBase (insert f (B \ {e}))
refine : B ∩ X ⊆ B \ {e}
⊢ M.Indep (insert f (B ∩ X))

Tactic:
refine hBf.indep.subset (insert_subset_insert ?_)

Premises used: Matroid.Indep.subset, Matroid.IsBase.indep, Set.insert_subset_insert
-- Module: Mathlib.Combinatorics.Matroid.Dual
Goal:
α : Type u_1
M : Matroid α
B X : Set α
hB : M.IsBase B
hBX : M.IsBasis (B ∩ X) X
e : α
he : (e ∈ M.E ∧ e ∉ X) ∧ e ∈ B
B' : Set α
hB' : M.IsBase B'
hem : B' ⊆ B ∪ X ∧ e ∉ B'
f : α
hfb : f ∈ B' \ B
hBf : M.IsBase (insert f (B \ {e}))
simp_rw : B ∩ X ⊆ B ∧ Disjoint (B ∩ X) {e}
simp_rw₁ : Disjoint (B ∩ X) {e}
simp_rw₂ : e ∉ B ∩ X
simp_rw₃ : ¬(e ∈ B ∧ e ∈ X)
simp_rw₄ : ¬(e ∈ B ∧ False)
simp_rw₅ : ¬False
⊢ B ∩ X ⊆ B \ {e}

Tactic:
simp_rw [subset_diff, and_iff_right inter_subset_left, disjoint_singleton_right,
      mem_inter_iff, iff_false_intro he.1.2, and_false, not_false_iff]

Premises used: Set.disjoint_singleton_right, Set.mem_inter_iff, Set.subset_diff, Set.inter_subset_left, iff_false_intro, and_iff_right, And.right, And.left, and_false, not_false_iff
-- Module: Mathlib.Combinatorics.Matroid.Dual
Goal:
α : Type u_1
M : Matroid α
B X : Set α
hB : M.IsBase B
hBX : M.IsBasis (B ∩ X) X
e : α
he : (e ∈ M.E ∧ e ∉ X) ∧ e ∈ B
B' : Set α
hB' : M.IsBase B'
hem : B' ⊆ B ∪ X ∧ e ∉ B'
f : α
hfb : f ∈ B' \ B
hBf : M.IsBase (insert f (B \ {e}))
⊢ M.Indep (insert f (B ∩ X))

Tactic:
have hi : M.Indep (insert f (B ∩ X)) := by
    refine hBf.indep.subset (insert_subset_insert ?_)
    simp_rw [subset_diff, and_iff_right inter_subset_left, disjoint_singleton_right,
      mem_inter_iff, iff_false_intro he.1.2, and_false, not_false_iff]
-- Module: Mathlib.Combinatorics.Matroid.Dual
Goal:
α : Type u_1
M : Matroid α
B X : Set α
hB : M.IsBase B
hBX : M.IsBasis (B ∩ X) X
e : α
he : (e ∈ M.E ∧ e ∉ X) ∧ e ∈ B
B' : Set α
hB' : M.IsBase B'
hem : B' ⊆ B ∪ X ∧ e ∉ B'
f : α
hfb : f ∈ B' \ B
hBf : M.IsBase (insert f (B \ {e}))
hi : M.Indep (insert f (B ∩ X))
⊢ False

Tactic:
hfb.2 (hBX.mem_of_insert_indep (Or.elim (hem.1 hfb.1) (False.elim ∘ hfb.2) id) hi).1

Premises used: False.elim, Function.comp, id, And.right, And.left, Matroid.IsBasis.mem_of_insert_indep, Or.elim
-- Module: Mathlib.Combinatorics.Matroid.Dual
Goal:
α : Type u_1
M : Matroid α
B X : Set α
hB : M.IsBase B
hBX : M.IsBasis (B ∩ X) X
e : α
he : (e ∈ M.E ∧ e ∉ X) ∧ e ∈ B
B' : Set α
hB' : M.IsBase B'
hem : B' ⊆ B ∪ X ∧ e ∉ B'
f : α
hfb : f ∈ B' \ B
hBf : M.IsBase (insert f (B \ {e}))
hi : M.Indep (insert f (B ∩ X))
⊢ False

Tactic:
exact hfb.2 (hBX.mem_of_insert_indep (Or.elim (hem.1 hfb.1) (False.elim ∘ hfb.2) id) hi).1

Premises used: False.elim, Function.comp, id, And.right, And.left, Matroid.IsBasis.mem_of_insert_indep, Or.elim
-- Module: Mathlib.Combinatorics.Matroid.Dual
Goal:
α : Type u_1
M : Matroid α
B X : Set α
hB : M.IsBase B
hX : X ⊆ M.E
⊢ M.IsBasis (B ∩ X) X ↔ M✶.IsBasis (M.E \ B ∩ (M.E \ X)) (M.E \ X)

Tactic:
⟨hB.compl_inter_isBasis_of_inter_isBasis, fun h ↦ ?_⟩

Premises used: Matroid.IsBase.compl_inter_isBasis_of_inter_isBasis, Iff.intro
-- Module: Mathlib.Combinatorics.Matroid.Dual
Goal:
α : Type u_1
M : Matroid α
B X : Set α
hB : M.IsBase B
hX : X ⊆ M.E
refine : ∀ (h : M✶.IsBasis (M.E \ B ∩ (M.E \ X)) (M.E \ X)), M.IsBasis (B ∩ X) X
⊢ M.IsBasis (B ∩ X) X ↔ M✶.IsBasis (M.E \ B ∩ (M.E \ X)) (M.E \ X)

Tactic:
refine ⟨hB.compl_inter_isBasis_of_inter_isBasis, fun h ↦ ?_⟩
-- Module: Mathlib.Combinatorics.Matroid.Dual
Goal:
α : Type u_1
M : Matroid α
B X : Set α
hB : M.IsBase B
hX : X ⊆ M.E
h : M✶.IsBasis (M.E \ B ∩ (M.E \ X)) (M.E \ X)
⊢ M.IsBasis (B ∩ X) X

Tactic:
simpa [inter_eq_self_of_subset_right hX, inter_eq_self_of_subset_right hB.subset_ground] using
    hB.compl_isBase_dual.compl_inter_isBasis_of_inter_isBasis h

Premises used: Matroid.IsBase.subset_ground, Matroid.IsBase.compl_isBase_dual, Matroid.IsBase.compl_inter_isBasis_of_inter_isBasis, Set.inter_eq_self_of_subset_right
-- Module: Mathlib.Combinatorics.Matroid.Dual
Goal:
α : Type u_1
M : Matroid α
B : Set α
hB : B ⊆ M.E
rw : M.IsBase B ↔ M.IsBase (M.E \ (M.E \ B))
rw₁ rw₂ : M.IsBase B ↔ M.IsBase B
⊢ M.IsBase B ↔ M✶.IsBase (M.E \ B)

Tactic:
rw [dual_isBase_iff, diff_diff_cancel_left hB]

Premises used: Matroid.dual_isBase_iff, Set.diff_diff_cancel_left
-- Module: Mathlib.Combinatorics.Matroid.Dual
Goal:
α : Type u_1
M : Matroid α
h : M✶.RankPos
rwa : ∀ (h : ¬M✶.IsBase ∅), ¬M.IsBase M.E
rwa₁ : ∀ (h : ¬M.IsBase (M.E \ ∅)), ¬M.IsBase M.E
rwa₂ rwa₃ rwa₄ rwa₅ : ∀ (h : ¬M.IsBase M.E), ¬M.IsBase M.E
⊢ ¬M.IsBase M.E

Tactic:
rwa [rankPos_iff, dual_isBase_iff, diff_empty] at h

Premises used: Matroid.rankPos_iff, Matroid.dual_isBase_iff, Set.diff_empty
-- Module: Mathlib.Combinatorics.Matroid.Dual
Goal:
α : Type u_1
M : Matroid α
h : M✶.RankPos
hB : M.IsBase M.E
⊢ False

Tactic:
M.ground_not_isBase hB

Premises used: Matroid.ground_not_isBase
-- Module: Mathlib.Combinatorics.Matroid.Dual
Goal:
α : Type u_1
M : Matroid α
h : M✶.RankPos
hB : M.IsBase M.E
⊢ False

Tactic:
exact M.ground_not_isBase hB

Premises used: Matroid.ground_not_isBase
-- Module: Mathlib.Combinatorics.Matroid.Dual
Goal:
α : Type u_1
M : Matroid α
I : Set α
h : M✶.RankPos
hI : M.Indep I
obtain : ∀ (B : Set α) (hB : M.IsBase B ∧ I ⊆ B), I ⊂ M.E
⊢ I ⊂ M.E

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

Premises used: Matroid.Indep.exists_isBase_superset
-- Module: Mathlib.Combinatorics.Matroid.Dual
Goal:
α : Type u_1
M : Matroid α
I : Set α
h : M✶.RankPos
hI : M.Indep I
B : Set α
hB : M.IsBase B ∧ I ⊆ B
⊢ I ⊂ M.E

Tactic:
hB.2.trans_ssubset hB.1.ssubset_ground

Premises used: HasSubset.Subset.trans_ssubset, And.right, And.left, Matroid.IsBase.ssubset_ground
-- Module: Mathlib.Combinatorics.Matroid.Dual
Goal:
α : Type u_1
M : Matroid α
I : Set α
h : M✶.RankPos
hI : M.Indep I
B : Set α
hB : M.IsBase B ∧ I ⊆ B
⊢ I ⊂ M.E

Tactic:
exact hB.2.trans_ssubset hB.1.ssubset_ground

Premises used: HasSubset.Subset.trans_ssubset, And.right, And.left, Matroid.IsBase.ssubset_ground
-- Module: Mathlib.Combinatorics.Matroid.Dual
Goal:
α : Type u_1
M : Matroid α
X : Set α
⊢ M.Coindep X ↔ M✶.Indep X

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Combinatorics.Matroid.Dual
Goal:
α : Type u_1
M : Matroid α
X : Set α
hX : M.Coindep X
⊢ M✶.Indep X

Tactic:
hX
-- Module: Mathlib.Combinatorics.Matroid.Dual
Goal:
α : Type u_1
M : Matroid α
X : Set α
rw : M✶✶.Indep X ↔ M.Indep X
rw₁ rw₂ : M.Indep X ↔ M.Indep X
⊢ M✶.Coindep X ↔ M.Indep X

Tactic:
rw [Coindep, dual_dual]

Premises used: Matroid.dual_dual, Matroid.Coindep
-- Module: Mathlib.Combinatorics.Matroid.Dual
Goal:
α : Type u_1
M : Matroid α
I : Set α
hI : M.Indep I
⊢ M✶.Coindep I

Tactic:
dual_coindep_iff.2 hI

Premises used: Iff.mpr, Matroid.dual_coindep_iff
-- Module: Mathlib.Combinatorics.Matroid.Dual
Goal:
α : Type u_1
M : Matroid α
X : Set α
simp_rw : X ⊆ M.E → ((∃ (B : Set α), M.IsBase B ∧ Disjoint X B) ↔ ∃ (B : Set α), M.IsBase B ∧ B ⊆ M.E ∧ Disjoint B X)
⊢ M.Coindep X ↔ (∃ (B : Set α), M.IsBase B ∧ B ⊆ M.E \ X) ∧ X ⊆ M.E

Tactic:
simp_rw [Coindep, dual_indep_iff_exists', and_comm (a := _ ⊆ _), and_congr_left_iff, subset_diff]

Premises used: Matroid.dual_indep_iff_exists', Set.subset_diff, and_comm, and_congr_left_iff, Matroid.Coindep
-- Module: Mathlib.Combinatorics.Matroid.Dual
Goal:
α : Type u_1
M : Matroid α
X : Set α
⊢ X ⊆ M.E → ((∃ (B : Set α), M.IsBase B ∧ Disjoint X B) ↔ ∃ (B : Set α), M.IsBase B ∧ B ⊆ M.E ∧ Disjoint B X)

Tactic:
fun _ ↦ ⟨fun ⟨B, hB, hXB⟩ ↦ ⟨B, hB, hB.subset_ground, hXB.symm⟩,
    fun ⟨B, hB, _, hBX⟩ ↦ ⟨B, hB, hBX.symm⟩⟩

Premises used: Matroid.E, Disjoint, Exists, Matroid.IsBase, HasSubset.Subset, Matroid.IsBase.subset_ground, _private.0.Matroid.coindep_iff_exists'.match_1, And, Disjoint.symm, And.intro, Iff.intro, Exists.intro, _private.0.Matroid.coindep_iff_exists'.match_2
-- Module: Mathlib.Combinatorics.Matroid.Dual
Goal:
α : Type u_1
M : Matroid α
X : Set α
⊢ X ⊆ M.E → ((∃ (B : Set α), M.IsBase B ∧ Disjoint X B) ↔ ∃ (B : Set α), M.IsBase B ∧ B ⊆ M.E ∧ Disjoint B X)

Tactic:
exact fun _ ↦ ⟨fun ⟨B, hB, hXB⟩ ↦ ⟨B, hB, hB.subset_ground, hXB.symm⟩,
    fun ⟨B, hB, _, hBX⟩ ↦ ⟨B, hB, hBX.symm⟩⟩
-- Module: Mathlib.Combinatorics.Matroid.Dual
Goal:
α : Type u_1
M : Matroid α
X : Set α
hX : X ⊆ M.E
rw : (∃ (B : Set α), M.IsBase B ∧ B ⊆ M.E \ X) ∧ X ⊆ M.E ↔ ∃ (B : Set α), M.IsBase B ∧ B ⊆ M.E \ X
rw₁ rw₂ : (∃ (B : Set α), M.IsBase B ∧ B ⊆ M.E \ X) ↔ ∃ (B : Set α), M.IsBase B ∧ B ⊆ M.E \ X
⊢ M.Coindep X ↔ ∃ (B : Set α), M.IsBase B ∧ B ⊆ M.E \ X

Tactic:
rw [coindep_iff_exists', and_iff_left hX]

Premises used: and_iff_left, Matroid.coindep_iff_exists'
-- Module: Mathlib.Combinatorics.Matroid.Dual
Goal:
α : Type u_1
M : Matroid α
X : Set α
simp_rw :
  (∃ (B : Set α), M.IsBase B ∧ B ⊆ M.E ∧ Disjoint B X) ∧ X ⊆ M.E ↔ ∃ (B : Set α), M.IsBase B ∧ X ⊆ M.E ∧ Disjoint X B
⊢ M.Coindep X ↔ ∃ (B : Set α), M.IsBase B ∧ X ⊆ M.E \ B

Tactic:
simp_rw [coindep_iff_exists', subset_diff]

Premises used: Set.subset_diff, Matroid.coindep_iff_exists'
-- Module: Mathlib.Combinatorics.Matroid.Dual
Goal:
α : Type u_1
M : Matroid α
X : Set α
⊢ (∃ (B : Set α), M.IsBase B ∧ B ⊆ M.E ∧ Disjoint B X) ∧ X ⊆ M.E ↔ ∃ (B : Set α), M.IsBase B ∧ X ⊆ M.E ∧ Disjoint X B

Tactic:
⟨fun ⟨⟨B, hB, _, hBX⟩, hX⟩ ↦ ⟨B, hB, hX, hBX.symm⟩,
    fun ⟨B, hB, hXE, hXB⟩ ↦ ⟨⟨B, hB, hB.subset_ground, hXB.symm⟩, hXE⟩⟩

Premises used: Matroid.E, Disjoint, Exists, Matroid.IsBase, HasSubset.Subset, Matroid.IsBase.subset_ground, _private.0.Matroid.coindep_iff_subset_compl_isBase.match_2, And, Disjoint.symm, And.intro, Iff.intro, Exists.intro, _private.0.Matroid.coindep_iff_subset_compl_isBase.match_1
-- Module: Mathlib.Combinatorics.Matroid.Dual
Goal:
α : Type u_1
M : Matroid α
X : Set α
⊢ (∃ (B : Set α), M.IsBase B ∧ B ⊆ M.E ∧ Disjoint B X) ∧ X ⊆ M.E ↔ ∃ (B : Set α), M.IsBase B ∧ X ⊆ M.E ∧ Disjoint X B

Tactic:
exact ⟨fun ⟨⟨B, hB, _, hBX⟩, hX⟩ ↦ ⟨B, hB, hX, hBX.symm⟩,
    fun ⟨B, hB, hXE, hXB⟩ ↦ ⟨⟨B, hB, hB.subset_ground, hXB.symm⟩, hXE⟩⟩
-- Module: Mathlib.Combinatorics.Matroid.Dual
Goal:
α : Type u_1
M : Matroid α
X : Set α
hX : M.Coindep X
⊢ X ⊆ M.E

Tactic:
hX.indep.subset_ground

Premises used: Matroid.Coindep.indep, Matroid.Indep.subset_ground, Maximal
-- Module: Mathlib.Combinatorics.Matroid.Dual
Goal:
α : Type u_1
M : Matroid α
X : Set α
h : M.Coindep X
⊢ ∃ (B : Set α), M.IsBase B ∧ B ⊆ M.E \ X

Tactic:
(coindep_iff_exists h.subset_ground).1 h

Premises used: Matroid.coindep_iff_exists, Matroid.Coindep.subset_ground, Iff.mp
-- Module: Mathlib.Combinatorics.Matroid.Dual
Goal:
α : Type u_1
M : Matroid α
X : Set α
h : M.Coindep X
⊢ ∃ (B : Set α), M.IsBase B ∧ X ⊆ M.E \ B

Tactic:
coindep_iff_subset_compl_isBase.1 h

Premises used: Iff.mp, Matroid.coindep_iff_subset_compl_isBase
-- Module: Mathlib.Combinatorics.Matroid.IndepAxioms
Goal:
α : Type u_1
M : IndepMatroid α
⊢ ∀ ⦃I : Set α⦄, M.Indep I ↔ ∃ (B : Set α), Maximal M.Indep B ∧ I ⊆ B

Tactic:
fun I ↦ ⟨fun h ↦ ?_, fun ⟨B, ⟨h, _⟩, hIB'⟩ ↦ M.indep_subset h hIB'⟩

Premises used: _private.0.IndepMatroid.matroid.match_1, Iff.intro, IndepMatroid.indep_subset, IndepMatroid.Indep
-- Module: Mathlib.Combinatorics.Matroid.IndepAxioms
Goal:
α : Type u_1
M : IndepMatroid α
refine : ∀ (I : Set α) (h : M.Indep I), ∃ (B : Set α), Maximal M.Indep B ∧ I ⊆ B
⊢ ∀ ⦃I : Set α⦄, M.Indep I ↔ ∃ (B : Set α), Maximal M.Indep B ∧ I ⊆ B

Tactic:
refine fun I ↦ ⟨fun h ↦ ?_, fun ⟨B, ⟨h, _⟩, hIB'⟩ ↦ M.indep_subset h hIB'⟩
-- Module: Mathlib.Combinatorics.Matroid.IndepAxioms
Goal:
α : Type u_1
M : IndepMatroid α
I : Set α
h : M.Indep I
obtain :
  ∀ (J : Set α) (hIJ : I ⊆ J) (hmax : Maximal (fun (K : Set α) ↦ M.Indep K ∧ K ⊆ M.E) J),
    ∃ (B : Set α), Maximal M.Indep B ∧ I ⊆ B
⊢ ∃ (B : Set α), Maximal M.Indep B ∧ I ⊆ B

Tactic:
obtain ⟨J, hIJ, hmax⟩ := M.indep_maximal M.E rfl.subset I h (M.subset_ground I h)

Premises used: IndepMatroid.subset_ground, Eq.subset, IndepMatroid.indep_maximal, rfl, IndepMatroid.E
-- Module: Mathlib.Combinatorics.Matroid.IndepAxioms
Goal:
α : Type u_1
M : IndepMatroid α
I : Set α
h : M.Indep I
J : Set α
hIJ : I ⊆ J
hmax : Maximal (fun (K : Set α) ↦ M.Indep K ∧ K ⊆ M.E) J
⊢ Maximal M.Indep J ∧ J ⊆ M.E

Tactic:
rw [maximal_and_iff_right_of_imp M.subset_ground] at hmax

Premises used: IndepMatroid.subset_ground, maximal_and_iff_right_of_imp
-- Module: Mathlib.Combinatorics.Matroid.IndepAxioms
Goal:
α : Type u_1
M : IndepMatroid α
I : Set α
h : M.Indep I
J : Set α
hIJ : I ⊆ J
hmax : Maximal M.Indep J ∧ J ⊆ M.E
⊢ ∃ (B : Set α), Maximal M.Indep B ∧ I ⊆ B

Tactic:
⟨J, hmax.1, hIJ⟩

Premises used: And.left, And.intro, Exists.intro
-- Module: Mathlib.Combinatorics.Matroid.IndepAxioms
Goal:
α : Type u_1
M : IndepMatroid α
I : Set α
h : M.Indep I
J : Set α
hIJ : I ⊆ J
hmax : Maximal M.Indep J ∧ J ⊆ M.E
⊢ ∃ (B : Set α), Maximal M.Indep B ∧ I ⊆ B

Tactic:
exact ⟨J, hmax.1, hIJ⟩
-- Module: Mathlib.Combinatorics.Matroid.IndepAxioms
Goal:
α : Type u_1
M : IndepMatroid α
obtain : ∀ (B : Set α) (hB : Maximal (fun (K : Set α) ↦ M.Indep K ∧ K ⊆ M.E) B), ∃ (B : Set α), Maximal M.Indep B
⊢ ∃ (B : Set α), Maximal M.Indep B

Tactic:
obtain ⟨B, -, hB⟩ := M.indep_maximal M.E rfl.subset ∅ M.indep_empty <| empty_subset _

Premises used: Eq.subset, IndepMatroid.indep_empty, Set.empty_subset, EmptyCollection.emptyCollection, IndepMatroid.indep_maximal, rfl, IndepMatroid.E
-- Module: Mathlib.Combinatorics.Matroid.IndepAxioms
Goal:
α : Type u_1
M : IndepMatroid α
B : Set α
hB : Maximal (fun (K : Set α) ↦ M.Indep K ∧ K ⊆ M.E) B
⊢ Maximal M.Indep B ∧ B ⊆ M.E

Tactic:
rw [maximal_and_iff_right_of_imp M.subset_ground] at hB

Premises used: IndepMatroid.subset_ground, maximal_and_iff_right_of_imp
-- Module: Mathlib.Combinatorics.Matroid.IndepAxioms
Goal:
α : Type u_1
M : IndepMatroid α
B : Set α
hB : Maximal M.Indep B ∧ B ⊆ M.E
⊢ ∃ (B : Set α), Maximal M.Indep B

Tactic:
⟨B, hB.1⟩

Premises used: And.left, Exists.intro
-- Module: Mathlib.Combinatorics.Matroid.IndepAxioms
Goal:
α : Type u_1
M : IndepMatroid α
B : Set α
hB : Maximal M.Indep B ∧ B ⊆ M.E
⊢ ∃ (B : Set α), Maximal M.Indep B

Tactic:
exact ⟨B, hB.1⟩
-- Module: Mathlib.Combinatorics.Matroid.IndepAxioms
Goal:
α : Type u_1
M : IndepMatroid α
B B' : Set α
hB : Maximal M.Indep B
hB' : Maximal M.Indep B'
e : α
he : e ∈ B \ B'
⊢ ¬Maximal M.Indep (B \ {e})

Tactic:
have hnotmax : ¬ Maximal M.Indep (B \ {e}) :=
      fun h ↦ h.not_prop_of_ssuperset (diff_singleton_ssubset.2 he.1) hB.prop
-- Module: Mathlib.Combinatorics.Matroid.IndepAxioms
Goal:
α : Type u_1
M : IndepMatroid α
B B' : Set α
hB : Maximal M.Indep B
hB' : Maximal M.Indep B'
e : α
he : e ∈ B \ B'
hnotmax : ¬Maximal M.Indep (B \ {e})
obtain :
  ∀ (f : α) (hf : f ∈ B' \ (B \ {e})) (hfB : M.Indep (insert f (B \ {e}))),
    ∃ b ∈ B' \ B, Maximal M.Indep (insert b (B \ {e}))
⊢ ∃ b ∈ B' \ B, Maximal M.Indep (insert b (B \ {e}))

Tactic:
obtain ⟨f, hf, hfB⟩ := M.indep_aug (M.indep_subset hB.prop diff_subset) hnotmax hB'

Premises used: Set.diff_subset, Maximal.prop, IndepMatroid.indep_aug, IndepMatroid.indep_subset
-- Module: Mathlib.Combinatorics.Matroid.IndepAxioms
Goal:
α : Type u_1
M : IndepMatroid α
B B' : Set α
hB : Maximal M.Indep B
hB' : Maximal M.Indep B'
f : α
he : f ∈ B \ B'
hnotmax : ¬Maximal M.Indep (B \ {f})
hf : f ∈ B' \ (B \ {f})
hfB : M.Indep (insert f (B \ {f}))
⊢ False

Tactic:
he.2 hf.1

Premises used: And.right, And.left
-- Module: Mathlib.Combinatorics.Matroid.IndepAxioms
Goal:
α : Type u_1
M : IndepMatroid α
B B' : Set α
hB : Maximal M.Indep B
hB' : Maximal M.Indep B'
f : α
he : f ∈ B \ B'
hnotmax : ¬Maximal M.Indep (B \ {f})
hf : f ∈ B' \ (B \ {f})
hfB : M.Indep (insert f (B \ {f}))
⊢ False

Tactic:
exact he.2 hf.1

Premises used: And.right, And.left
-- Module: Mathlib.Combinatorics.Matroid.IndepAxioms
Goal:
α : Type u_1
M : IndepMatroid α
B B' : Set α
hB : Maximal M.Indep B
hB' : Maximal M.Indep B'
e : α
he : e ∈ B \ B'
hnotmax : ¬Maximal M.Indep (B \ {e})
f : α
hf : f ∈ B' \ (B \ {e})
hfB : M.Indep (insert f (B \ {e}))
⊢ f ∈ B' \ B

Tactic:
simpa [show f ≠ e by rintro rfl; exact he.2 hf.1] using hf
-- Module: Mathlib.Combinatorics.Matroid.IndepAxioms
Goal:
α : Type u_1
M : IndepMatroid α
B B' : Set α
hB : Maximal M.Indep B
hB' : Maximal M.Indep B'
e : α
he : e ∈ B \ B'
hnotmax : ¬Maximal M.Indep (B \ {e})
f : α
hf : f ∈ B' \ (B \ {e})
hfB : M.Indep (insert f (B \ {e}))
⊢ f ∈ B' \ B

Tactic:
replace hf := show f ∈ B' \ B by simpa [show f ≠ e by rintro rfl; exact he.2 hf.1] using hf
-- Module: Mathlib.Combinatorics.Matroid.IndepAxioms
Goal:
α : Type u_1
M : IndepMatroid α
B B' : Set α
hB : Maximal M.Indep B
hB' : Maximal M.Indep B'
e : α
he : e ∈ B \ B'
hnotmax : ¬Maximal M.Indep (B \ {e})
f : α
hfB : M.Indep (insert f (B \ {e}))
hf : f ∈ B' \ B
⊢ ∃ b ∈ B' \ B, Maximal M.Indep (insert b (B \ {e}))

Tactic:
⟨f, hf, by_contra fun hnot ↦ ?_⟩

Premises used: And.intro, Exists.intro, by_contra
-- Module: Mathlib.Combinatorics.Matroid.IndepAxioms
Goal:
α : Type u_1
M : IndepMatroid α
B B' : Set α
hB : Maximal M.Indep B
hB' : Maximal M.Indep B'
e : α
he : e ∈ B \ B'
hnotmax : ¬Maximal M.Indep (B \ {e})
f : α
hfB : M.Indep (insert f (B \ {e}))
hf : f ∈ B' \ B
refine : ∀ (hnot : ¬Maximal M.Indep (insert f (B \ {e}))), False
⊢ ∃ b ∈ B' \ B, Maximal M.Indep (insert b (B \ {e}))

Tactic:
refine ⟨f, hf, by_contra fun hnot ↦ ?_⟩
-- Module: Mathlib.Combinatorics.Matroid.IndepAxioms
Goal:
α : Type u_1
M : IndepMatroid α
B B' : Set α
hB : Maximal M.Indep B
hB' : Maximal M.Indep B'
e : α
he : e ∈ B \ B'
hnotmax : ¬Maximal M.Indep (B \ {e})
f : α
hfB : M.Indep (insert f (B \ {e}))
hf : f ∈ B' \ B
hnot : ¬Maximal M.Indep (insert f (B \ {e}))
obtain : ∀ (x : α) (hxB : x ∈ B \ insert f (B \ {e})) (hind : M.Indep (insert x (insert f (B \ {e})))), False
⊢ False

Tactic:
obtain ⟨x, hxB, hind⟩ := M.indep_aug hfB hnot hB

Premises used: IndepMatroid.indep_aug
-- Module: Mathlib.Combinatorics.Matroid.IndepAxioms
Goal:
α : Type u_1
M : IndepMatroid α
B B' : Set α
hB : Maximal M.Indep B
hB' : Maximal M.Indep B'
e : α
he : e ∈ B \ B'
hnotmax : ¬Maximal M.Indep (B \ {e})
f : α
hfB : M.Indep (insert f (B \ {e}))
hf : f ∈ B' \ B
hnot : ¬Maximal M.Indep (insert f (B \ {e}))
x : α
hxB : x ∈ B \ insert f (B \ {e})
hind : M.Indep (insert x (insert f (B \ {e})))
⊢ ¬x = f ∧ x = e

Tactic:
simpa [hxB.1] using hxB

Premises used: And.left
-- Module: Mathlib.Combinatorics.Matroid.IndepAxioms
Goal:
α : Type u_1
M : IndepMatroid α
B B' : Set α
hB : Maximal M.Indep B
hB' : Maximal M.Indep B'
e : α
he : e ∈ B \ B'
hnotmax : ¬Maximal M.Indep (B \ {e})
f : α
hfB : M.Indep (insert f (B \ {e}))
hf : f ∈ B' \ B
hnot : ¬Maximal M.Indep (insert f (B \ {e}))
x : α
hxB : x ∈ B \ insert f (B \ {e})
hind : M.Indep (insert x (insert f (B \ {e})))
⊢ x ∈ B \ B'

Tactic:
obtain ⟨-, rfl⟩ : _ ∧ x = e := by simpa [hxB.1] using hxB

Premises used: rfl
-- Module: Mathlib.Combinatorics.Matroid.IndepAxioms
Goal:
α : Type u_1
M : IndepMatroid α
B B' : Set α
hB : Maximal M.Indep B
hB' : Maximal M.Indep B'
e : α
he : e ∈ B \ B'
hnotmax : ¬Maximal M.Indep (B \ {e})
f : α
hfB : M.Indep (insert f (B \ {e}))
hf : f ∈ B' \ B
hnot : ¬Maximal M.Indep (insert f (B \ {e}))
x : α
hxB : x ∈ B \ insert f (B \ {e})
hind : M.Indep (insert x (insert f (B \ {e})))
he₁ : x ∈ B \ B'
⊢ ¬Maximal M.Indep (B \ {x})

Tactic:
obtain ⟨-, rfl⟩ : _ ∧ x = e := by simpa [hxB.1] using hxB

Premises used: rfl
-- Module: Mathlib.Combinatorics.Matroid.IndepAxioms
Goal:
α : Type u_1
M : IndepMatroid α
B B' : Set α
hB : Maximal M.Indep B
hB' : Maximal M.Indep B'
e : α
he : e ∈ B \ B'
hnotmax : ¬Maximal M.Indep (B \ {e})
f : α
hfB : M.Indep (insert f (B \ {e}))
hf : f ∈ B' \ B
hnot : ¬Maximal M.Indep (insert f (B \ {e}))
x : α
hxB : x ∈ B \ insert f (B \ {e})
hind : M.Indep (insert x (insert f (B \ {e})))
he₁ : x ∈ B \ B'
hnotmax₁ : ¬Maximal M.Indep (B \ {x})
⊢ M.Indep (insert f (B \ {x}))

Tactic:
obtain ⟨-, rfl⟩ : _ ∧ x = e := by simpa [hxB.1] using hxB

Premises used: rfl
-- Module: Mathlib.Combinatorics.Matroid.IndepAxioms
Goal:
α : Type u_1
M : IndepMatroid α
B B' : Set α
hB : Maximal M.Indep B
hB' : Maximal M.Indep B'
e : α
he : e ∈ B \ B'
hnotmax : ¬Maximal M.Indep (B \ {e})
f : α
hfB : M.Indep (insert f (B \ {e}))
hf : f ∈ B' \ B
hnot : ¬Maximal M.Indep (insert f (B \ {e}))
x : α
hxB : x ∈ B \ insert f (B \ {e})
hind : M.Indep (insert x (insert f (B \ {e})))
he₁ : x ∈ B \ B'
hnotmax₁ : ¬Maximal M.Indep (B \ {x})
hfB₁ : M.Indep (insert f (B \ {x}))
⊢ ¬Maximal M.Indep (insert f (B \ {x}))

Tactic:
obtain ⟨-, rfl⟩ : _ ∧ x = e := by simpa [hxB.1] using hxB

Premises used: rfl