awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.Matroid.Dual
Goal:
α : Type u_1
M_1 : Matroid α
I B_1 X_1 : Set α
M : Matroid α
X I' : Set α
hI'E : I' ⊆ M.E
B : Set α
hB : M.IsBase B
hI'B : Disjoint I' B
hI'X : I' ⊆ X
B' : Set α
hB' : M.IsBase B'
hI : M.IsBasis (B' \ X) (M.E \ X)
hIB' : B' \ X ⊆ B'
hB'IB : B' ⊆ B' \ X ∪ B
J : Set α
hJE : J ⊆ M.E
B'' : Set α
hB'' : M.IsBase B''
hdj : Disjoint J B''
hJX : J ⊆ X
hXJ : X \ B' ∩ M.E ⊆ J
hI' : B'' ∩ X ∪ B' \ X ⊆ B'
B₁ : Set α
hB₁ : M.IsBase B₁
hI'B₁ : B'' ∩ X ∪ B' \ X ⊆ B₁
hB₁I : B₁ ⊆ B'' ∩ X ∪ B' \ X ∪ B''
⊢ B₁ ⊆ B'' ∪ B' \ X

Tactic:
rw [union_comm, ← union_assoc, union_eq_self_of_subset_right inter_subset_left] at hB₁I

Premises used: Set.union_eq_self_of_subset_right, Set.inter_subset_left, Set.union_comm, Set.union_assoc
-- Module: Mathlib.Combinatorics.Matroid.Dual
Goal:
α : Type u_1
M_1 : Matroid α
I B_1 X_1 : Set α
M : Matroid α
X I' : Set α
hI'E : I' ⊆ M.E
B : Set α
hB : M.IsBase B
hI'B : Disjoint I' B
hI'X : I' ⊆ X
B' : Set α
hB' : M.IsBase B'
hI : M.IsBasis (B' \ X) (M.E \ X)
hIB' : B' \ X ⊆ B'
hB'IB : B' ⊆ B' \ X ∪ B
J : Set α
hJE : J ⊆ M.E
B'' : Set α
hB'' : M.IsBase B''
hdj : Disjoint J B''
hJX : J ⊆ X
hXJ : X \ B' ∩ M.E ⊆ J
hI' : B'' ∩ X ∪ B' \ X ⊆ B'
B₁ : Set α
hB₁ : M.IsBase B₁
hI'B₁ : B'' ∩ X ∪ B' \ X ⊆ B₁
hB₁I : B₁ ⊆ B'' ∪ B' \ X
⊢ B₁ = B'

Tactic:
hB₁.eq_of_subset_indep hB'.indep (fun e he ↦ ?_)

Premises used: Matroid.IsBase.eq_of_subset_indep, Matroid.IsBase.indep
-- Module: Mathlib.Combinatorics.Matroid.Dual
Goal:
α : Type u_1
M_1 : Matroid α
I B_1 X_1 : Set α
M : Matroid α
X I' : Set α
hI'E : I' ⊆ M.E
B : Set α
hB : M.IsBase B
hI'B : Disjoint I' B
hI'X : I' ⊆ X
B' : Set α
hB' : M.IsBase B'
hI : M.IsBasis (B' \ X) (M.E \ X)
hIB' : B' \ X ⊆ B'
hB'IB : B' ⊆ B' \ X ∪ B
J : Set α
hJE : J ⊆ M.E
B'' : Set α
hB'' : M.IsBase B''
hdj : Disjoint J B''
hJX : J ⊆ X
hXJ : X \ B' ∩ M.E ⊆ J
hI' : B'' ∩ X ∪ B' \ X ⊆ B'
B₁ : Set α
hB₁ : M.IsBase B₁
hI'B₁ : B'' ∩ X ∪ B' \ X ⊆ B₁
hB₁I : B₁ ⊆ B'' ∪ B' \ X
refine : ∀ (e : α) (he : e ∈ B₁), e ∈ B'
⊢ B₁ = B'

Tactic:
refine hB₁.eq_of_subset_indep hB'.indep (fun e he ↦ ?_)

Premises used: Matroid.IsBase.eq_of_subset_indep, Matroid.IsBase.indep
-- Module: Mathlib.Combinatorics.Matroid.Dual
Goal:
α : Type u_1
M_1 : Matroid α
I B_1 X_1 : Set α
M : Matroid α
X I' : Set α
hI'E : I' ⊆ M.E
B : Set α
hB : M.IsBase B
hI'B : Disjoint I' B
hI'X : I' ⊆ X
B' : Set α
hB' : M.IsBase B'
hI : M.IsBasis (B' \ X) (M.E \ X)
hIB' : B' \ X ⊆ B'
hB'IB : B' ⊆ B' \ X ∪ B
J : Set α
hJE : J ⊆ M.E
B'' : Set α
hB'' : M.IsBase B''
hdj : Disjoint J B''
hJX : J ⊆ X
hXJ : X \ B' ∩ M.E ⊆ J
hI' : B'' ∩ X ∪ B' \ X ⊆ B'
B₁ : Set α
hB₁ : M.IsBase B₁
hI'B₁ : B'' ∩ X ∪ B' \ X ⊆ B₁
hB₁I : B₁ ⊆ B'' ∪ B' \ X
e : α
he : e ∈ B₁
⊢ e ∈ B'

Tactic:
(hB₁I he).elim (fun heB'' ↦ ?_) (fun h ↦ h.1)

Premises used: And.left, Or.elim
-- Module: Mathlib.Combinatorics.Matroid.Dual
Goal:
α : Type u_1
M_1 : Matroid α
I B_1 X_1 : Set α
M : Matroid α
X I' : Set α
hI'E : I' ⊆ M.E
B : Set α
hB : M.IsBase B
hI'B : Disjoint I' B
hI'X : I' ⊆ X
B' : Set α
hB' : M.IsBase B'
hI : M.IsBasis (B' \ X) (M.E \ X)
hIB' : B' \ X ⊆ B'
hB'IB : B' ⊆ B' \ X ∪ B
J : Set α
hJE : J ⊆ M.E
B'' : Set α
hB'' : M.IsBase B''
hdj : Disjoint J B''
hJX : J ⊆ X
hXJ : X \ B' ∩ M.E ⊆ J
hI' : B'' ∩ X ∪ B' \ X ⊆ B'
B₁ : Set α
hB₁ : M.IsBase B₁
hI'B₁ : B'' ∩ X ∪ B' \ X ⊆ B₁
hB₁I : B₁ ⊆ B'' ∪ B' \ X
e : α
he : e ∈ B₁
⊢ e ∈ B''

Tactic:
refine (hB₁I he).elim (fun heB'' ↦ ?_) (fun h ↦ h.1)

Premises used: And.left, Or.elim
-- Module: Mathlib.Combinatorics.Matroid.Dual
Goal:
α : Type u_1
M_1 : Matroid α
I B_1 X_1 : Set α
M : Matroid α
X I' : Set α
hI'E : I' ⊆ M.E
B : Set α
hB : M.IsBase B
hI'B : Disjoint I' B
hI'X : I' ⊆ X
B' : Set α
hB' : M.IsBase B'
hI : M.IsBasis (B' \ X) (M.E \ X)
hIB' : B' \ X ⊆ B'
hB'IB : B' ⊆ B' \ X ∪ B
J : Set α
hJE : J ⊆ M.E
B'' : Set α
hB'' : M.IsBase B''
hdj : Disjoint J B''
hJX : J ⊆ X
hXJ : X \ B' ∩ M.E ⊆ J
hI' : B'' ∩ X ∪ B' \ X ⊆ B'
B₁ : Set α
hB₁ : M.IsBase B₁
hI'B₁ : B'' ∩ X ∪ B' \ X ⊆ B₁
hB₁I : B₁ ⊆ B'' ∪ B' \ X
e : α
he : e ∈ B₁
heB'' : e ∈ B''
⊢ e ∈ B'

Tactic:
(em (e ∈ X)).elim (fun heX ↦ hI' (Or.inl ⟨heB'', heX⟩)) (fun heX ↦ hIB' ?_)

Premises used: Membership.mem, em, And.intro, Or.inl, Or.elim
-- Module: Mathlib.Combinatorics.Matroid.Dual
Goal:
α : Type u_1
M_1 : Matroid α
I B_1 X_1 : Set α
M : Matroid α
X I' : Set α
hI'E : I' ⊆ M.E
B : Set α
hB : M.IsBase B
hI'B : Disjoint I' B
hI'X : I' ⊆ X
B' : Set α
hB' : M.IsBase B'
hI : M.IsBasis (B' \ X) (M.E \ X)
hIB' : B' \ X ⊆ B'
hB'IB : B' ⊆ B' \ X ∪ B
J : Set α
hJE : J ⊆ M.E
B'' : Set α
hB'' : M.IsBase B''
hdj : Disjoint J B''
hJX : J ⊆ X
hXJ : X \ B' ∩ M.E ⊆ J
hI' : B'' ∩ X ∪ B' \ X ⊆ B'
B₁ : Set α
hB₁ : M.IsBase B₁
hI'B₁ : B'' ∩ X ∪ B' \ X ⊆ B₁
hB₁I : B₁ ⊆ B'' ∪ B' \ X
e : α
he : e ∈ B₁
heB'' : e ∈ B''
refine : ∀ (heX : e ∉ X), e ∈ B' \ X
⊢ e ∈ B'

Tactic:
refine (em (e ∈ X)).elim (fun heX ↦ hI' (Or.inl ⟨heB'', heX⟩)) (fun heX ↦ hIB' ?_)

Premises used: Membership.mem, em, And.intro, Or.inl, Or.elim
-- Module: Mathlib.Combinatorics.Matroid.Dual
Goal:
α : Type u_1
M_1 : Matroid α
I B_1 X_1 : Set α
M : Matroid α
X I' : Set α
hI'E : I' ⊆ M.E
B : Set α
hB : M.IsBase B
hI'B : Disjoint I' B
hI'X : I' ⊆ X
B' : Set α
hB' : M.IsBase B'
hI : M.IsBasis (B' \ X) (M.E \ X)
hIB' : B' \ X ⊆ B'
hB'IB : B' ⊆ B' \ X ∪ B
J : Set α
hJE : J ⊆ M.E
B'' : Set α
hB'' : M.IsBase B''
hdj : Disjoint J B''
hJX : J ⊆ X
hXJ : X \ B' ∩ M.E ⊆ J
hI' : B'' ∩ X ∪ B' \ X ⊆ B'
B₁ : Set α
hB₁ : M.IsBase B₁
hI'B₁ : B'' ∩ X ∪ B' \ X ⊆ B₁
hB₁I : B₁ ⊆ B'' ∪ B' \ X
e : α
he : e ∈ B₁
heB'' : e ∈ B''
heX : e ∉ X
⊢ e ∈ B' \ X

Tactic:
hI.mem_of_insert_indep ⟨hB₁.subset_ground he, heX⟩ ?_

Premises used: Matroid.IsBase.subset_ground, And.intro, Matroid.IsBasis.mem_of_insert_indep
-- Module: Mathlib.Combinatorics.Matroid.Dual
Goal:
α : Type u_1
M_1 : Matroid α
I B_1 X_1 : Set α
M : Matroid α
X I' : Set α
hI'E : I' ⊆ M.E
B : Set α
hB : M.IsBase B
hI'B : Disjoint I' B
hI'X : I' ⊆ X
B' : Set α
hB' : M.IsBase B'
hI : M.IsBasis (B' \ X) (M.E \ X)
hIB' : B' \ X ⊆ B'
hB'IB : B' ⊆ B' \ X ∪ B
J : Set α
hJE : J ⊆ M.E
B'' : Set α
hB'' : M.IsBase B''
hdj : Disjoint J B''
hJX : J ⊆ X
hXJ : X \ B' ∩ M.E ⊆ J
hI' : B'' ∩ X ∪ B' \ X ⊆ B'
B₁ : Set α
hB₁ : M.IsBase B₁
hI'B₁ : B'' ∩ X ∪ B' \ X ⊆ B₁
hB₁I : B₁ ⊆ B'' ∪ B' \ X
e : α
he : e ∈ B₁
heB'' : e ∈ B''
heX : e ∉ X
refine : M.Indep (insert e (B' \ X))
⊢ e ∈ B' \ X

Tactic:
refine hI.mem_of_insert_indep ⟨hB₁.subset_ground he, heX⟩ ?_

Premises used: Matroid.IsBase.subset_ground, And.intro, Matroid.IsBasis.mem_of_insert_indep
-- Module: Mathlib.Combinatorics.Matroid.Dual
Goal:
α : Type u_1
M_1 : Matroid α
I B_1 X_1 : Set α
M : Matroid α
X I' : Set α
hI'E : I' ⊆ M.E
B : Set α
hB : M.IsBase B
hI'B : Disjoint I' B
hI'X : I' ⊆ X
B' : Set α
hB' : M.IsBase B'
hI : M.IsBasis (B' \ X) (M.E \ X)
hIB' : B' \ X ⊆ B'
hB'IB : B' ⊆ B' \ X ∪ B
J : Set α
hJE : J ⊆ M.E
B'' : Set α
hB'' : M.IsBase B''
hdj : Disjoint J B''
hJX : J ⊆ X
hXJ : X \ B' ∩ M.E ⊆ J
hI' : B'' ∩ X ∪ B' \ X ⊆ B'
B₁ : Set α
hB₁ : M.IsBase B₁
hI'B₁ : B'' ∩ X ∪ B' \ X ⊆ B₁
hB₁I : B₁ ⊆ B'' ∪ B' \ X
e : α
he : e ∈ B₁
heB'' : e ∈ B''
heX : e ∉ X
⊢ M.Indep (insert e (B' \ X))

Tactic:
hB₁.indep.subset (insert_subset he (subset_union_right.trans hI'B₁))

Premises used: Set.subset_union_right, HasSubset.Subset.trans, Matroid.Indep.subset, Matroid.IsBase.indep, Set.insert_subset
-- Module: Mathlib.Combinatorics.Matroid.Dual
Goal:
α : Type u_1
M_1 : Matroid α
I B_1 X_1 : Set α
M : Matroid α
X I' : Set α
hI'E : I' ⊆ M.E
B : Set α
hB : M.IsBase B
hI'B : Disjoint I' B
hI'X : I' ⊆ X
B' : Set α
hB' : M.IsBase B'
hI : M.IsBasis (B' \ X) (M.E \ X)
hIB' : B' \ X ⊆ B'
hB'IB : B' ⊆ B' \ X ∪ B
J : Set α
hJE : J ⊆ M.E
B'' : Set α
hB'' : M.IsBase B''
hdj : Disjoint J B''
hJX : J ⊆ X
hXJ : X \ B' ∩ M.E ⊆ J
hI' : B'' ∩ X ∪ B' \ X ⊆ B'
B₁ : Set α
hB₁ : M.IsBase B₁
hI'B₁ : B'' ∩ X ∪ B' \ X ⊆ B₁
hB₁I : B₁ ⊆ B'' ∪ B' \ X
e : α
he : e ∈ B₁
heB'' : e ∈ B''
heX : e ∉ X
⊢ M.Indep (insert e (B' \ X))

Tactic:
exact hB₁.indep.subset (insert_subset he (subset_union_right.trans hI'B₁))

Premises used: Set.subset_union_right, HasSubset.Subset.trans, Matroid.Indep.subset, Matroid.IsBase.indep, Set.insert_subset
-- Module: Mathlib.Combinatorics.Matroid.Dual
Goal:
α : Type u_1
M_1 : Matroid α
I B_1 X_1 : Set α
M : Matroid α
X I' : Set α
hI'E : I' ⊆ M.E
B : Set α
hB : M.IsBase B
hI'B : Disjoint I' B
hI'X : I' ⊆ X
B' : Set α
hB' : M.IsBase B'
hI : M.IsBasis (B' \ X) (M.E \ X)
hIB' : B' \ X ⊆ B'
hB'IB : B' ⊆ B' \ X ∪ B
J : Set α
hJE : J ⊆ M.E
B'' : Set α
hB'' : M.IsBase B''
hdj : Disjoint J B''
hJX : J ⊆ X
hXJ : X \ B' ∩ M.E ⊆ J
hI' : B'' ∩ X ∪ B' \ X ⊆ B'
B₁ : Set α
hB₁ : M.IsBase B₁
hI'B₁ : B'' ∩ X ∪ B' \ X ⊆ B₁
hB₁I : B₁ ⊆ B'' ∪ B' \ X
refine_4 :
  ∀ (hB' : M.IsBase B₁) (hI : M.IsBasis (B₁ \ X) (M.E \ X)) (hIB' : B₁ \ X ⊆ B₁) (hB'IB : B₁ ⊆ B₁ \ X ∪ B)
    (hXJ : X \ B₁ ∩ M.E ⊆ J) (hI' hI'B₁ : B'' ∩ X ∪ B₁ \ X ⊆ B₁) (hB₁I : B₁ ⊆ B'' ∪ B₁ \ X), Disjoint J B₁
⊢ Disjoint J B'

Tactic:
obtain rfl : B₁ = B' := by
      refine hB₁.eq_of_subset_indep hB'.indep (fun e he ↦ ?_)
      refine (hB₁I he).elim (fun heB'' ↦ ?_) (fun h ↦ h.1)
      refine (em (e ∈ X)).elim (fun heX ↦ hI' (Or.inl ⟨heB'', heX⟩)) (fun heX ↦ hIB' ?_)
      refine hI.mem_of_insert_indep ⟨hB₁.subset_ground he, heX⟩ ?_
      exact hB₁.indep.subset (insert_subset he (subset_union_right.trans hI'B₁))

Premises used: rfl
-- Module: Mathlib.Combinatorics.Matroid.Dual
Goal:
α : Type u_1
M_1 : Matroid α
I B_1 X_1 : Set α
M : Matroid α
X I' : Set α
hI'E : I' ⊆ M.E
B : Set α
hB : M.IsBase B
hI'B : Disjoint I' B
hI'X : I' ⊆ X
J : Set α
hJE : J ⊆ M.E
B'' : Set α
hB'' : M.IsBase B''
hdj : Disjoint J B''
hJX : J ⊆ X
B₁ : Set α
hB₁ hB' : M.IsBase B₁
hI : M.IsBasis (B₁ \ X) (M.E \ X)
hIB' : B₁ \ X ⊆ B₁
hB'IB : B₁ ⊆ B₁ \ X ∪ B
hXJ : X \ B₁ ∩ M.E ⊆ J
hI' hI'B₁ : B'' ∩ X ∪ B₁ \ X ⊆ B₁
hB₁I : B₁ ⊆ B'' ∪ B₁ \ X
refine_4 : ∀ (hdj' : ¬Disjoint J B₁), False
⊢ Disjoint J B₁

Tactic:
by_contra hdj'
-- Module: Mathlib.Combinatorics.Matroid.Dual
Goal:
α : Type u_1
M_1 : Matroid α
I B_1 X_1 : Set α
M : Matroid α
X I' : Set α
hI'E : I' ⊆ M.E
B : Set α
hB : M.IsBase B
hI'B : Disjoint I' B
hI'X : I' ⊆ X
J : Set α
hJE : J ⊆ M.E
B'' : Set α
hB'' : M.IsBase B''
hdj : Disjoint J B''
hJX : J ⊆ X
B₁ : Set α
hB₁ hB' : M.IsBase B₁
hI : M.IsBasis (B₁ \ X) (M.E \ X)
hIB' : B₁ \ X ⊆ B₁
hB'IB : B₁ ⊆ B₁ \ X ∪ B
hXJ : X \ B₁ ∩ M.E ⊆ J
hI' hI'B₁ : B'' ∩ X ∪ B₁ \ X ⊆ B₁
hB₁I : B₁ ⊆ B'' ∪ B₁ \ X
hdj' : ¬Disjoint J B₁
refine_4 : ∀ (e : α) (heJ : e ∈ J) (heB' : e ∈ B₁), False
⊢ False

Tactic:
obtain ⟨e, heJ, heB'⟩ := not_disjoint_iff.mp hdj'

Premises used: Set.not_disjoint_iff, Iff.mp
-- Module: Mathlib.Combinatorics.Matroid.Dual
Goal:
α : Type u_1
M_1 : Matroid α
I B_1 X_1 : Set α
M : Matroid α
X I' : Set α
hI'E : I' ⊆ M.E
B : Set α
hB : M.IsBase B
hI'B : Disjoint I' B
hI'X : I' ⊆ X
J : Set α
hJE : J ⊆ M.E
B'' : Set α
hB'' : M.IsBase B''
hdj : Disjoint J B''
hJX : J ⊆ X
B₁ : Set α
hB₁ hB' : M.IsBase B₁
hI : M.IsBasis (B₁ \ X) (M.E \ X)
hIB' : B₁ \ X ⊆ B₁
hB'IB : B₁ ⊆ B₁ \ X ∪ B
hXJ : X \ B₁ ∩ M.E ⊆ J
hI' hI'B₁ : B'' ∩ X ∪ B₁ \ X ⊆ B₁
hB₁I : B₁ ⊆ B'' ∪ B₁ \ X
hdj' : ¬Disjoint J B₁
e : α
heJ : e ∈ J
heB' : e ∈ B₁
refine_4 : ∀ (heB'' : e ∈ B''), False
refine_4₁ : ∀ (heX : e ∉ X), False
⊢ False

Tactic:
obtain (heB'' | ⟨-, heX⟩) := hB₁I heB'
-- Module: Mathlib.Combinatorics.Matroid.Dual
Goal:
α : Type u_1
M_1 : Matroid α
I B_1 X_1 : Set α
M : Matroid α
X I' : Set α
hI'E : I' ⊆ M.E
B : Set α
hB : M.IsBase B
hI'B : Disjoint I' B
hI'X : I' ⊆ X
J : Set α
hJE : J ⊆ M.E
B'' : Set α
hB'' : M.IsBase B''
hdj : Disjoint J B''
hJX : J ⊆ X
B₁ : Set α
hB₁ hB' : M.IsBase B₁
hI : M.IsBasis (B₁ \ X) (M.E \ X)
hIB' : B₁ \ X ⊆ B₁
hB'IB : B₁ ⊆ B₁ \ X ∪ B
hXJ : X \ B₁ ∩ M.E ⊆ J
hI' hI'B₁ : B'' ∩ X ∪ B₁ \ X ⊆ B₁
hB₁I : B₁ ⊆ B'' ∪ B₁ \ X
hdj' : ¬Disjoint J B₁
e : α
heJ : e ∈ J
heB' : e ∈ B₁
heB'' : e ∈ B''
⊢ False

Tactic:
hdj.ne_of_mem heJ heB'' rfl

Premises used: Disjoint.ne_of_mem, rfl
-- Module: Mathlib.Combinatorics.Matroid.Dual
Goal:
α : Type u_1
M_1 : Matroid α
I B_1 X_1 : Set α
M : Matroid α
X I' : Set α
hI'E : I' ⊆ M.E
B : Set α
hB : M.IsBase B
hI'B : Disjoint I' B
hI'X : I' ⊆ X
J : Set α
hJE : J ⊆ M.E
B'' : Set α
hB'' : M.IsBase B''
hdj : Disjoint J B''
hJX : J ⊆ X
B₁ : Set α
hB₁ hB' : M.IsBase B₁
hI : M.IsBasis (B₁ \ X) (M.E \ X)
hIB' : B₁ \ X ⊆ B₁
hB'IB : B₁ ⊆ B₁ \ X ∪ B
hXJ : X \ B₁ ∩ M.E ⊆ J
hI' hI'B₁ : B'' ∩ X ∪ B₁ \ X ⊆ B₁
hB₁I : B₁ ⊆ B'' ∪ B₁ \ X
hdj' : ¬Disjoint J B₁
e : α
heJ : e ∈ J
heB' : e ∈ B₁
heB'' : e ∈ B''
⊢ False

Tactic:
exact hdj.ne_of_mem heJ heB'' rfl

Premises used: Disjoint.ne_of_mem, rfl
-- Module: Mathlib.Combinatorics.Matroid.Dual
Goal:
α : Type u_1
M_1 : Matroid α
I B_1 X_1 : Set α
M : Matroid α
X I' : Set α
hI'E : I' ⊆ M.E
B : Set α
hB : M.IsBase B
hI'B : Disjoint I' B
hI'X : I' ⊆ X
J : Set α
hJE : J ⊆ M.E
B'' : Set α
hB'' : M.IsBase B''
hdj : Disjoint J B''
hJX : J ⊆ X
B₁ : Set α
hB₁ hB' : M.IsBase B₁
hI : M.IsBasis (B₁ \ X) (M.E \ X)
hIB' : B₁ \ X ⊆ B₁
hB'IB : B₁ ⊆ B₁ \ X ∪ B
hXJ : X \ B₁ ∩ M.E ⊆ J
hI' hI'B₁ : B'' ∩ X ∪ B₁ \ X ⊆ B₁
hB₁I : B₁ ⊆ B'' ∪ B₁ \ X
hdj' : ¬Disjoint J B₁
e : α
heJ : e ∈ J
heB' : e ∈ B₁
heX : e ∉ X
⊢ False

Tactic:
heX (hJX heJ)
-- Module: Mathlib.Combinatorics.Matroid.Dual
Goal:
α : Type u_1
M_1 : Matroid α
I B_1 X_1 : Set α
M : Matroid α
X I' : Set α
hI'E : I' ⊆ M.E
B : Set α
hB : M.IsBase B
hI'B : Disjoint I' B
hI'X : I' ⊆ X
J : Set α
hJE : J ⊆ M.E
B'' : Set α
hB'' : M.IsBase B''
hdj : Disjoint J B''
hJX : J ⊆ X
B₁ : Set α
hB₁ hB' : M.IsBase B₁
hI : M.IsBasis (B₁ \ X) (M.E \ X)
hIB' : B₁ \ X ⊆ B₁
hB'IB : B₁ ⊆ B₁ \ X ∪ B
hXJ : X \ B₁ ∩ M.E ⊆ J
hI' hI'B₁ : B'' ∩ X ∪ B₁ \ X ⊆ B₁
hB₁I : B₁ ⊆ B'' ∪ B₁ \ X
hdj' : ¬Disjoint J B₁
e : α
heJ : e ∈ J
heB' : e ∈ B₁
heX : e ∉ X
⊢ False

Tactic:
exact heX (hJX heJ)
-- Module: Mathlib.Combinatorics.Matroid.Dual
Goal:
α : Type u_1
M_1 : Matroid α
I B X : Set α
M : Matroid α
tauto tauto₁ tauto₂ : ∀ (I : Set α), (I ⊆ M.E ∧ ∃ (B : Set α), M.IsBase B ∧ Disjoint I B) → I ⊆ M.E
tauto₃ tauto₄ tauto₅ tauto₆ tauto₇ tauto₈ tauto₉ tauto₁₀ :
  ∀ (I : Set α) ⦃a : α⦄, I ⊆ M.E → ∀ (w : Set α), M.IsBase w → Disjoint I w → a ∈ I → a ∈ M.E
⊢ ∀ (I : Set α), (I ⊆ M.E ∧ ∃ (B : Set α), M.IsBase B ∧ Disjoint I B) → I ⊆ M.E

Tactic:
tauto
-- Module: Mathlib.Combinatorics.Matroid.Dual
Goal:
α : Type u_1
M : Matroid α
I : Set α
⊢ M✶.Indep I ↔ I ⊆ M.E ∧ ∃ (B : Set α), M.IsBase B ∧ Disjoint I B

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Combinatorics.Matroid.Dual
Goal:
α : Type u_1
M : Matroid α
⊢ M✶.E = M.E

Tactic:
rfl

Premises used: Maximal, rfl
-- Module: Mathlib.Combinatorics.Matroid.Dual
Goal:
α : Type u_1
M : Matroid α
I : Set α
hI : I ⊆ M.E
rw : (I ⊆ M.E ∧ ∃ (B : Set α), M.IsBase B ∧ Disjoint I B) ↔ ∃ (B : Set α), M.IsBase B ∧ Disjoint I B
rw₁ rw₂ : (∃ (B : Set α), M.IsBase B ∧ Disjoint I B) ↔ ∃ (B : Set α), M.IsBase B ∧ Disjoint I B
⊢ M✶.Indep I ↔ ∃ (B : Set α), M.IsBase B ∧ Disjoint I B

Tactic:
rw [dual_indep_iff_exists', and_iff_right hI]

Premises used: Matroid.dual_indep_iff_exists', and_iff_right
-- Module: Mathlib.Combinatorics.Matroid.Dual
Goal:
α : Type u_1
M : Matroid α
I : Set α
simp_rw : ¬M✶.Indep I ∧ I ⊆ M✶.E ↔ (∀ (B : Set α), M.IsBase B → (I ∩ B).Nonempty) ∧ I ⊆ M.E
simp_rw₁ :
  ¬(I ⊆ M.E ∧ ∃ (B : Set α), M.IsBase B ∧ Disjoint I B) ∧ I ⊆ M✶.E ↔
    (∀ (B : Set α), M.IsBase B → (I ∩ B).Nonempty) ∧ I ⊆ M.E
simp_rw₂ :
  ¬(I ⊆ M.E ∧ ∃ (B : Set α), M.IsBase B ∧ Disjoint I B) ∧ I ⊆ M.E ↔
    (∀ (B : Set α), M.IsBase B → (I ∩ B).Nonempty) ∧ I ⊆ M.E
simp_rw₃ :
  I ⊆ M.E → (¬(I ⊆ M.E ∧ ∃ (B : Set α), M.IsBase B ∧ Disjoint I B) ↔ ∀ (B : Set α), M.IsBase B → (I ∩ B).Nonempty)
simp_rw₄ :
  I ⊆ M.E → ((I ⊆ M.E → ¬∃ (B : Set α), M.IsBase B ∧ Disjoint I B) ↔ ∀ (B : Set α), M.IsBase B → (I ∩ B).Nonempty)
simp_rw₅ :
  I ⊆ M.E → ((I ⊆ M.E → ∀ (x : Set α), ¬(M.IsBase x ∧ Disjoint I x)) ↔ ∀ (B : Set α), M.IsBase B → (I ∩ B).Nonempty)
simp_rw₆ :
  I ⊆ M.E → ((I ⊆ M.E → ∀ (x : Set α), M.IsBase x → ¬Disjoint I x) ↔ ∀ (B : Set α), M.IsBase B → (I ∩ B).Nonempty)
simp_rw₇ :
  I ⊆ M.E → ((I ⊆ M.E → ∀ (x : Set α), M.IsBase x → (I ∩ x).Nonempty) ↔ ∀ (x : Set α), M.IsBase x → (I ∩ x).Nonempty)
simp_rw₈ : I ⊆ M.E → I ⊆ M.E ∨ ∀ (x : Set α), M.IsBase x → (I ∩ x).Nonempty
⊢ M✶.Dep I ↔ (∀ (B : Set α), M.IsBase B → (I ∩ B).Nonempty) ∧ I ⊆ M.E

Tactic:
simp_rw [dep_iff, dual_indep_iff_exists', dual_ground, and_congr_left_iff, not_and,
    not_exists, not_and, not_disjoint_iff_nonempty_inter, Classical.imp_iff_right_iff,
    iff_true_intro Or.inl]

Premises used: not_exists, Matroid.dual_indep_iff_exists', Set.not_disjoint_iff_nonempty_inter, and_congr_left_iff, Classical.imp_iff_right_iff, Matroid.dual_ground, iff_true_intro, Or.inl, not_and, Matroid.dep_iff
-- Module: Mathlib.Combinatorics.Matroid.Dual
Goal:
α : Type u_1
M : Matroid α
I B X : Set α
inst : M.Finite
⊢ M✶.Finite

Tactic:
⟨M.ground_finite⟩

Premises used: Matroid.Finite.mk, Matroid.ground_finite
-- Module: Mathlib.Combinatorics.Matroid.Dual
Goal:
α : Type u_1
M : Matroid α
I B X : Set α
inst : M.Nonempty
⊢ M✶.Nonempty

Tactic:
⟨M.ground_nonempty⟩

Premises used: Matroid.ground_nonempty, Matroid.Nonempty.mk
-- Module: Mathlib.Combinatorics.Matroid.Dual
Goal:
α : Type u_1
M : Matroid α
B : Set α
hB : B ⊆ M.E
rw :
  (M✶.Indep B ∧ ∀ ⦃t : Set α⦄, M✶.Indep t → B ⊆ t → B = t) ↔
    (B ⊆ M.E ∧ ∃ (B_1 : Set α), M.IsBase B_1 ∧ Disjoint B B_1) ∧
      ∀ ⦃t : Set α⦄, (t ⊆ M.E ∧ ∃ (B : Set α), M.IsBase B ∧ Disjoint t B) → B ⊆ t → B = t
⊢ M✶.IsBase B ↔ M.IsBase (M.E \ B)

Tactic:
rw [isBase_compl_iff_maximal_disjoint_isBase, isBase_iff_maximal_indep, maximal_subset_iff,
    maximal_subset_iff]

Premises used: Matroid.isBase_compl_iff_maximal_disjoint_isBase, maximal_subset_iff, Matroid.isBase_iff_maximal_indep
-- Module: Mathlib.Combinatorics.Matroid.Dual
Goal:
α : Type u_1
M : Matroid α
B : Set α
hB : B ⊆ M.E
⊢ (M✶.Indep B ∧ ∀ ⦃t : Set α⦄, M✶.Indep t → B ⊆ t → B = t) ↔
    (B ⊆ M.E ∧ ∃ (B_1 : Set α), M.IsBase B_1 ∧ Disjoint B B_1) ∧
      ∀ ⦃t : Set α⦄, (t ⊆ M.E ∧ ∃ (B : Set α), M.IsBase B ∧ Disjoint t B) → B ⊆ t → B = t

Tactic:
simp [dual_indep_iff_exists', hB]

Premises used: Matroid.dual_indep_iff_exists'
-- Module: Mathlib.Combinatorics.Matroid.Dual
Goal:
α : Type u_1
M : Matroid α
B : Set α
h : B ⊆ M.E
rw : M.IsBase (M.E \ B) ↔ M.IsBase (M.E \ B) ∧ B ⊆ M.E
rw₁ rw₂ : M.IsBase (M.E \ B) ↔ M.IsBase (M.E \ B)
⊢ M✶.IsBase B ↔ M.IsBase (M.E \ B) ∧ B ⊆ M.E

Tactic:
rw [dual_isBase_iff, and_iff_left h]

Premises used: and_iff_left, Matroid.dual_isBase_iff
-- Module: Mathlib.Combinatorics.Matroid.Dual
Goal:
α : Type u_1
M : Matroid α
h :
  ∀ (B : Set α),
    Membership.mem (γ := Set (Set α)) {B : Set α | M✶.IsBase B} B ↔
      Membership.mem (γ := Set (Set α)) ((fun (X : Set α) ↦ M.E \ X) '' {B : Set α | M.IsBase B}) B
⊢ Eq.{u_1 + 1} (α := Set (Set α)) {B : Set α | M✶.IsBase B} ((fun (X : Set α) ↦ M.E \ X) '' {B : Set α | M.IsBase B})

Tactic:
ext B
-- Module: Mathlib.Combinatorics.Matroid.Dual
Goal:
α : Type u_1
M : Matroid α
B : Set α
h : M.IsBase (M.E \ B) ∧ B ⊆ M.E ↔ ∃ (x : Set α), M.IsBase x ∧ M.E \ x = B
⊢ Membership.mem (γ := Set (Set α)) {B : Set α | M✶.IsBase B} B ↔
    Membership.mem (γ := Set (Set α)) ((fun (X : Set α) ↦ M.E \ X) '' {B : Set α | M.IsBase B}) B

Tactic:
simp only [mem_setOf_eq, mem_image, dual_isBase_iff']

Premises used: Matroid.dual_isBase_iff', Set.mem_image, Set.mem_setOf_eq
-- Module: Mathlib.Combinatorics.Matroid.Dual
Goal:
α : Type u_1
M : Matroid α
B : Set α
⊢ M.IsBase (M.E \ B) ∧ B ⊆ M.E ↔ ∃ (x : Set α), M.IsBase x ∧ M.E \ x = B

Tactic:
⟨fun h ↦ ⟨_, h.1, diff_diff_cancel_left h.2⟩,
    fun ⟨B', hB', h⟩ ↦ ⟨?_,h.symm.trans_subset diff_subset⟩⟩

Premises used: Set.diff_subset, _private.0.Matroid.setOf_dual_isBase_eq.match_2, Matroid.E, Matroid.IsBase, HasSubset.Subset, SDiff.sdiff, And, And.right, And.left, And.intro, Iff.intro, Exists.intro, Set.diff_diff_cancel_left, Eq.symm, Eq.trans_subset
-- Module: Mathlib.Combinatorics.Matroid.Dual
Goal:
α : Type u_1
M : Matroid α
B : Set α
h :
  (∃ (x : Set α), M.IsBase x ∧ M.E \ x = B) → ∀ (B' : Set α) (hB' : M.IsBase B') (h : M.E \ B' = B), M.IsBase (M.E \ B)
⊢ M.IsBase (M.E \ B) ∧ B ⊆ M.E ↔ ∃ (x : Set α), M.IsBase x ∧ M.E \ x = B

Tactic:
refine ⟨fun h ↦ ⟨_, h.1, diff_diff_cancel_left h.2⟩,
    fun ⟨B', hB', h⟩ ↦ ⟨?_,h.symm.trans_subset diff_subset⟩⟩
-- Module: Mathlib.Combinatorics.Matroid.Dual
Goal:
α : Type u_1
M : Matroid α
B : Set α
h_1 : ∃ (x : Set α), M.IsBase x ∧ M.E \ x = B
B' : Set α
hB' : M.IsBase B'
h : M.E \ B' = B
h₁ : M.IsBase (M.E \ (M.E \ B'))
h₂ h₃ h₄ h₅ : M.IsBase B'
⊢ M.IsBase (M.E \ B)

Tactic:
rwa [← h, diff_diff_cancel_left hB'.subset_ground]

Premises used: Matroid.IsBase.subset_ground, Set.diff_diff_cancel_left
-- Module: Mathlib.Combinatorics.Matroid.Dual
Goal:
α : Type u_1
M : Matroid α
B : Set α
h : B ⊆ M.E
rw : M✶.IsBase (M✶.E \ B) ↔ M.IsBase B
rw₁ : M.IsBase (M.E \ (M✶.E \ B)) ↔ M.IsBase B
rw₂ : M.IsBase (M.E \ (M.E \ B)) ↔ M.IsBase B
rw₃ rw₄ : M.IsBase B ↔ M.IsBase B
⊢ M✶✶.IsBase B ↔ M.IsBase B

Tactic:
rw [dual_isBase_iff, dual_isBase_iff, dual_ground, diff_diff_cancel_left h]

Premises used: Matroid.dual_isBase_iff, Set.diff_diff_cancel_left, Matroid.dual_ground
-- Module: Mathlib.Combinatorics.Matroid.Dual
Goal:
α : Type u_1
⊢ Function.Involutive.{u_1 + 1} (α := Matroid α) dual

Tactic:
dual_dual

Premises used: Matroid.dual_dual, Function.Involutive
-- Module: Mathlib.Combinatorics.Matroid.Dual
Goal:
α : Type u_1
⊢ Function.Injective.{u_1 + 1, u_1 + 1} (α := Matroid α) dual

Tactic:
dual_involutive.injective

Premises used: Function.Involutive.injective, Matroid.dual_involutive
-- Module: Mathlib.Combinatorics.Matroid.Dual
Goal:
α : Type u_1
M₁ M₂ : Matroid α
⊢ M₁✶ = M₂✶ ↔ M₁ = M₂

Tactic:
dual_injective.eq_iff

Premises used: Function.Injective.eq_iff, Matroid.dual_injective
-- Module: Mathlib.Combinatorics.Matroid.Dual
Goal:
α : Type u_1
M₁ M₂ : Matroid α
rw : M₁✶ = M₂✶✶ ↔ M₂ = M₁✶
rw₁ : M₁✶ = M₂ ↔ M₂ = M₁✶
rw₂ rw₃ : M₂ = M₁✶ ↔ M₂ = M₁✶
⊢ M₁ = M₂✶ ↔ M₂ = M₁✶

Tactic:
rw [← dual_inj, dual_dual, eq_comm]

Premises used: eq_comm, Matroid.dual_dual, Matroid.dual_inj
-- Module: Mathlib.Combinatorics.Matroid.Dual
Goal:
α : Type u_1
M₁ M₂ : Matroid α
⊢ M₁ = M₂✶ ↔ M₁✶ = M₂

Tactic:
dual_involutive.eq_iff.symm

Premises used: Matroid.dual_involutive, Function.Involutive.eq_iff, Iff.symm
-- Module: Mathlib.Combinatorics.Matroid.Dual
Goal:
α : Type u_1
M : Matroid α
B : Set α
h : M✶.IsBase B
⊢ M.IsBase (M.E \ B)

Tactic:
(dual_isBase_iff'.1 h).1

Premises used: Matroid.dual_isBase_iff', And.left, Iff.mp
-- Module: Mathlib.Combinatorics.Matroid.Dual
Goal:
α : Type u_1
M : Matroid α
B : Set α
h : M.IsBase B
rwa : M.IsBase (M.E \ (M.E \ B))
rwa₁ rwa₂ rwa₃ rwa₄ : M.IsBase B
⊢ M✶.IsBase (M.E \ B)

Tactic:
rwa [dual_isBase_iff, diff_diff_cancel_left h.subset_ground]

Premises used: Matroid.dual_isBase_iff, Matroid.IsBase.subset_ground, Set.diff_diff_cancel_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
⊢ M✶.IsBasis (M.E \ B ∩ (M.E \ X)) (M.E \ X)

Tactic:
Indep.isBasis_of_forall_insert ?_ inter_subset_right (fun e he ↦ ?_)

Premises used: Matroid.Indep.isBasis_of_forall_insert, Set.inter_subset_right
-- Module: Mathlib.Combinatorics.Matroid.Dual
Goal:
α : Type u_1
M : Matroid α
B X : Set α
hB : M.IsBase B
hBX : M.IsBasis (B ∩ X) X
refine_1 : M✶.Indep (M.E \ B ∩ (M.E \ X))
refine_2 : ∀ (e : α) (he : e ∈ (M.E \ X) \ (M.E \ B ∩ (M.E \ X))), M✶.Dep (insert e (M.E \ B ∩ (M.E \ X)))
⊢ M✶.IsBasis (M.E \ B ∩ (M.E \ X)) (M.E \ X)

Tactic:
refine Indep.isBasis_of_forall_insert ?_ inter_subset_right (fun e he ↦ ?_)

Premises used: Matroid.Indep.isBasis_of_forall_insert, Set.inter_subset_right
-- Module: Mathlib.Combinatorics.Matroid.Dual
Goal:
α : Type u_1
M : Matroid α
B X : Set α
hB : M.IsBase B
hBX : M.IsBasis (B ∩ X) X
refine_1 : ∃ (B_1 : Set α), M.IsBase B_1 ∧ Disjoint (M.E \ B ∩ (M.E \ X)) B_1
⊢ M✶.Indep (M.E \ B ∩ (M.E \ X))

Tactic:
rw [dual_indep_iff_exists]

Premises used: Matroid.dual_indep_iff_exists
-- 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:
⟨B, hB, disjoint_of_subset_left inter_subset_left disjoint_sdiff_left⟩

Premises used: Set.disjoint_of_subset_left, Set.inter_subset_left, Set.disjoint_sdiff_left, And.intro, Exists.intro