awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.Matroid.Dual
Goal:
α : Type u_1
M_1 : Matroid α
I_1 B_1 X_1 : Set α
M : Matroid α
I X : Set α
hIE : I ⊆ M.E
B : Set α
hB : M.IsBase B
hIB : Disjoint I B
hI_not_max : ¬Maximal (fun (I : Set α) ↦ I ⊆ M.E ∧ ∃ (B : Set α), M.IsBase B ∧ Disjoint I B) I
hX_max : Maximal (fun (I : Set α) ↦ I ⊆ M.E ∧ ∃ (B : Set α), M.IsBase B ∧ Disjoint I B) X
hXE : X ⊆ M.E
B' : Set α := M.E \ X
hB' : M.IsBase B'
hX : B' = M.E \ X
hI : ¬M.IsBase (M.E \ I)
B'' : Set α
hB'' : M.IsBase B''
hB''₁ : B' \ I ⊆ B''
hB''₂ : B'' ⊆ B' ∪ B ∧ I ⊆ B''ᶜ
hssu : I ⊂ B''ᶜ ∩ M.E
obtain :
  ∀ (e : α) (heI : e ∉ I) (heB'' : e ∉ B'') (heE : e ∈ M.E),
    ∃ x ∈ X \ I, insert x I ⊆ M.E ∧ ∃ (B : Set α), M.IsBase B ∧ Disjoint (insert x I) B
⊢ ∃ x ∈ X \ I, insert x I ⊆ M.E ∧ ∃ (B : Set α), M.IsBase B ∧ Disjoint (insert x I) B

Tactic:
obtain ⟨e, ⟨(heB'' : e ∉ _), heE⟩, heI⟩ := exists_of_ssubset hssu

Premises used: Set.exists_of_ssubset
-- Module: Mathlib.Combinatorics.Matroid.Dual
Goal:
α : Type u_1
M_1 : Matroid α
I_1 B_1 X_1 : Set α
M : Matroid α
I X : Set α
hIE : I ⊆ M.E
B : Set α
hB : M.IsBase B
hIB : Disjoint I B
hI_not_max : ¬Maximal (fun (I : Set α) ↦ I ⊆ M.E ∧ ∃ (B : Set α), M.IsBase B ∧ Disjoint I B) I
hX_max : Maximal (fun (I : Set α) ↦ I ⊆ M.E ∧ ∃ (B : Set α), M.IsBase B ∧ Disjoint I B) X
hXE : X ⊆ M.E
B' : Set α := M.E \ X
hB' : M.IsBase B'
hX : B' = M.E \ X
hI : ¬M.IsBase (M.E \ I)
B'' : Set α
hB'' : M.IsBase B''
hB''₁ : B' \ I ⊆ B''
hB''₂ : B'' ⊆ B' ∪ B ∧ I ⊆ B''ᶜ
hssu : I ⊂ B''ᶜ ∩ M.E
e : α
heI : e ∉ I
heB'' : e ∉ B''
heE : e ∈ M.E
h : e ∈ X \ I ∧ insert e I ⊆ M.E ∧ ∃ (B : Set α), M.IsBase B ∧ Disjoint (insert e I) B
⊢ ∃ x ∈ X \ I, insert x I ⊆ M.E ∧ ∃ (B : Set α), M.IsBase B ∧ Disjoint (insert x I) B

Tactic:
use e
-- Module: Mathlib.Combinatorics.Matroid.Dual
Goal:
α : Type u_1
M_1 : Matroid α
I_1 B_1 X_1 : Set α
M : Matroid α
I X : Set α
hIE : I ⊆ M.E
B : Set α
hB : M.IsBase B
hIB : Disjoint I B
hI_not_max : ¬Maximal (fun (I : Set α) ↦ I ⊆ M.E ∧ ∃ (B : Set α), M.IsBase B ∧ Disjoint I B) I
hX_max : Maximal (fun (I : Set α) ↦ I ⊆ M.E ∧ ∃ (B : Set α), M.IsBase B ∧ Disjoint I B) X
hXE : X ⊆ M.E
B' : Set α := M.E \ X
hB' : M.IsBase B'
hX : B' = M.E \ X
hI : ¬M.IsBase (M.E \ I)
B'' : Set α
hB'' : M.IsBase B''
hB''₁ : B' \ I ⊆ B''
hB''₂ : B'' ⊆ B' ∪ B ∧ I ⊆ B''ᶜ
hssu : I ⊂ B''ᶜ ∩ M.E
e : α
heI : e ∉ I
heB'' : e ∉ B''
heE : e ∈ M.E
h : e ∈ X ∧ ∃ (B : Set α), M.IsBase B ∧ Disjoint (insert e I) B
⊢ e ∈ X \ I ∧ insert e I ⊆ M.E ∧ ∃ (B : Set α), M.IsBase B ∧ Disjoint (insert e I) B

Tactic:
simp_rw [mem_diff, insert_subset_iff, and_iff_left heI, and_iff_right heE, and_iff_right hIE]

Premises used: and_iff_left, and_iff_right, Set.insert_subset_iff, Set.mem_diff
-- Module: Mathlib.Combinatorics.Matroid.Dual
Goal:
α : Type u_1
M_1 : Matroid α
I_1 B_1 X_1 : Set α
M : Matroid α
I X : Set α
hIE : I ⊆ M.E
B : Set α
hB : M.IsBase B
hIB : Disjoint I B
hI_not_max : ¬Maximal (fun (I : Set α) ↦ I ⊆ M.E ∧ ∃ (B : Set α), M.IsBase B ∧ Disjoint I B) I
hX_max : Maximal (fun (I : Set α) ↦ I ⊆ M.E ∧ ∃ (B : Set α), M.IsBase B ∧ Disjoint I B) X
hXE : X ⊆ M.E
B' : Set α := M.E \ X
hB' : M.IsBase B'
hX : B' = M.E \ X
hI : ¬M.IsBase (M.E \ I)
B'' : Set α
hB'' : M.IsBase B''
hB''₁ : B' \ I ⊆ B''
hB''₂ : B'' ⊆ B' ∪ B ∧ I ⊆ B''ᶜ
hssu : I ⊂ B''ᶜ ∩ M.E
e : α
heI : e ∉ I
heB'' : e ∉ B''
heE : e ∈ M.E
⊢ e ∈ X ∧ ∃ (B : Set α), M.IsBase B ∧ Disjoint (insert e I) B

Tactic:
⟨by_contra (fun heX ↦ heB'' (hB''₁ ⟨?_, heI⟩)), ⟨B'', hB'', ?_⟩⟩

Premises used: And.intro, Exists.intro, by_contra
-- Module: Mathlib.Combinatorics.Matroid.Dual
Goal:
α : Type u_1
M_1 : Matroid α
I_1 B_1 X_1 : Set α
M : Matroid α
I X : Set α
hIE : I ⊆ M.E
B : Set α
hB : M.IsBase B
hIB : Disjoint I B
hI_not_max : ¬Maximal (fun (I : Set α) ↦ I ⊆ M.E ∧ ∃ (B : Set α), M.IsBase B ∧ Disjoint I B) I
hX_max : Maximal (fun (I : Set α) ↦ I ⊆ M.E ∧ ∃ (B : Set α), M.IsBase B ∧ Disjoint I B) X
hXE : X ⊆ M.E
B' : Set α := M.E \ X
hB' : M.IsBase B'
hX : B' = M.E \ X
hI : ¬M.IsBase (M.E \ I)
B'' : Set α
hB'' : M.IsBase B''
hB''₁ : B' \ I ⊆ B''
hB''₂ : B'' ⊆ B' ∪ B ∧ I ⊆ B''ᶜ
hssu : I ⊂ B''ᶜ ∩ M.E
e : α
heI : e ∉ I
heB'' : e ∉ B''
heE : e ∈ M.E
h : ∀ (heX : e ∉ X), e ∈ B'
h₁ : Disjoint (insert e I) B''
⊢ e ∈ X ∧ ∃ (B : Set α), M.IsBase B ∧ Disjoint (insert e I) B

Tactic:
refine ⟨by_contra (fun heX ↦ heB'' (hB''₁ ⟨?_, heI⟩)), ⟨B'', hB'', ?_⟩⟩
-- Module: Mathlib.Combinatorics.Matroid.Dual
Goal:
α : Type u_1
M_1 : Matroid α
I_1 B_1 X_1 : Set α
M : Matroid α
I X : Set α
hIE : I ⊆ M.E
B : Set α
hB : M.IsBase B
hIB : Disjoint I B
hI_not_max : ¬Maximal (fun (I : Set α) ↦ I ⊆ M.E ∧ ∃ (B : Set α), M.IsBase B ∧ Disjoint I B) I
hX_max : Maximal (fun (I : Set α) ↦ I ⊆ M.E ∧ ∃ (B : Set α), M.IsBase B ∧ Disjoint I B) X
hXE : X ⊆ M.E
B' : Set α := M.E \ X
hB' : M.IsBase B'
hX : B' = M.E \ X
hI : ¬M.IsBase (M.E \ I)
B'' : Set α
hB'' : M.IsBase B''
hB''₁ : B' \ I ⊆ B''
hB''₂ : B'' ⊆ B' ∪ B ∧ I ⊆ B''ᶜ
hssu : I ⊂ B''ᶜ ∩ M.E
e : α
heI : e ∉ I
heB'' : e ∉ B''
heE : e ∈ M.E
heX : e ∉ X
h : e ∈ M.E \ X
⊢ e ∈ B'

Tactic:
rw [hX]
-- Module: Mathlib.Combinatorics.Matroid.Dual
Goal:
α : Type u_1
M_1 : Matroid α
I_1 B_1 X_1 : Set α
M : Matroid α
I X : Set α
hIE : I ⊆ M.E
B : Set α
hB : M.IsBase B
hIB : Disjoint I B
hI_not_max : ¬Maximal (fun (I : Set α) ↦ I ⊆ M.E ∧ ∃ (B : Set α), M.IsBase B ∧ Disjoint I B) I
hX_max : Maximal (fun (I : Set α) ↦ I ⊆ M.E ∧ ∃ (B : Set α), M.IsBase B ∧ Disjoint I B) X
hXE : X ⊆ M.E
B' : Set α := M.E \ X
hB' : M.IsBase B'
hX : B' = M.E \ X
hI : ¬M.IsBase (M.E \ I)
B'' : Set α
hB'' : M.IsBase B''
hB''₁ : B' \ I ⊆ B''
hB''₂ : B'' ⊆ B' ∪ B ∧ I ⊆ B''ᶜ
hssu : I ⊂ B''ᶜ ∩ M.E
e : α
heI : e ∉ I
heB'' : e ∉ B''
heE : e ∈ M.E
heX : e ∉ X
⊢ e ∈ M.E \ X

Tactic:
⟨heE, heX⟩

Premises used: Set.Mem, Set.diff, setOf, And.intro
-- Module: Mathlib.Combinatorics.Matroid.Dual
Goal:
α : Type u_1
M_1 : Matroid α
I_1 B_1 X_1 : Set α
M : Matroid α
I X : Set α
hIE : I ⊆ M.E
B : Set α
hB : M.IsBase B
hIB : Disjoint I B
hI_not_max : ¬Maximal (fun (I : Set α) ↦ I ⊆ M.E ∧ ∃ (B : Set α), M.IsBase B ∧ Disjoint I B) I
hX_max : Maximal (fun (I : Set α) ↦ I ⊆ M.E ∧ ∃ (B : Set α), M.IsBase B ∧ Disjoint I B) X
hXE : X ⊆ M.E
B' : Set α := M.E \ X
hB' : M.IsBase B'
hX : B' = M.E \ X
hI : ¬M.IsBase (M.E \ I)
B'' : Set α
hB'' : M.IsBase B''
hB''₁ : B' \ I ⊆ B''
hB''₂ : B'' ⊆ B' ∪ B ∧ I ⊆ B''ᶜ
hssu : I ⊂ B''ᶜ ∩ M.E
e : α
heI : e ∉ I
heB'' : e ∉ B''
heE : e ∈ M.E
heX : e ∉ X
⊢ e ∈ M.E \ X

Tactic:
exact ⟨heE, heX⟩
-- Module: Mathlib.Combinatorics.Matroid.Dual
Goal:
α : Type u_1
M_1 : Matroid α
I_1 B_1 X_1 : Set α
M : Matroid α
I X : Set α
hIE : I ⊆ M.E
B : Set α
hB : M.IsBase B
hIB : Disjoint I B
hI_not_max : ¬Maximal (fun (I : Set α) ↦ I ⊆ M.E ∧ ∃ (B : Set α), M.IsBase B ∧ Disjoint I B) I
hX_max : Maximal (fun (I : Set α) ↦ I ⊆ M.E ∧ ∃ (B : Set α), M.IsBase B ∧ Disjoint I B) X
hXE : X ⊆ M.E
B' : Set α := M.E \ X
hB' : M.IsBase B'
hX : B' = M.E \ X
hI : ¬M.IsBase (M.E \ I)
B'' : Set α
hB'' : M.IsBase B''
hB''₁ : B' \ I ⊆ B''
hB''₂ : B'' ⊆ B' ∪ B ∧ I ⊆ B''ᶜ
hssu : I ⊂ B''ᶜ ∩ M.E
e : α
heI : e ∉ I
heB'' : e ∉ B''
heE : e ∈ M.E
h : Disjoint I B''
⊢ Disjoint (insert e I) B''

Tactic:
rw [← union_singleton, disjoint_union_left, disjoint_singleton_left, and_iff_left heB'']

Premises used: Set.disjoint_singleton_left, and_iff_left, Set.union_singleton, Set.disjoint_union_left
-- Module: Mathlib.Combinatorics.Matroid.Dual
Goal:
α : Type u_1
M_1 : Matroid α
I_1 B_1 X_1 : Set α
M : Matroid α
I X : Set α
hIE : I ⊆ M.E
B : Set α
hB : M.IsBase B
hIB : Disjoint I B
hI_not_max : ¬Maximal (fun (I : Set α) ↦ I ⊆ M.E ∧ ∃ (B : Set α), M.IsBase B ∧ Disjoint I B) I
hX_max : Maximal (fun (I : Set α) ↦ I ⊆ M.E ∧ ∃ (B : Set α), M.IsBase B ∧ Disjoint I B) X
hXE : X ⊆ M.E
B' : Set α := M.E \ X
hB' : M.IsBase B'
hX : B' = M.E \ X
hI : ¬M.IsBase (M.E \ I)
B'' : Set α
hB'' : M.IsBase B''
hB''₁ : B' \ I ⊆ B''
hB''₂ : B'' ⊆ B' ∪ B ∧ I ⊆ B''ᶜ
hssu : I ⊂ B''ᶜ ∩ M.E
e : α
heI : e ∉ I
heB'' : e ∉ B''
heE : e ∈ M.E
⊢ Disjoint I B''

Tactic:
disjoint_of_subset_left hB''₂.2 disjoint_compl_left

Premises used: Set.disjoint_of_subset_left, disjoint_compl_left, And.right
-- Module: Mathlib.Combinatorics.Matroid.Dual
Goal:
α : Type u_1
M_1 : Matroid α
I_1 B_1 X_1 : Set α
M : Matroid α
I X : Set α
hIE : I ⊆ M.E
B : Set α
hB : M.IsBase B
hIB : Disjoint I B
hI_not_max : ¬Maximal (fun (I : Set α) ↦ I ⊆ M.E ∧ ∃ (B : Set α), M.IsBase B ∧ Disjoint I B) I
hX_max : Maximal (fun (I : Set α) ↦ I ⊆ M.E ∧ ∃ (B : Set α), M.IsBase B ∧ Disjoint I B) X
hXE : X ⊆ M.E
B' : Set α := M.E \ X
hB' : M.IsBase B'
hX : B' = M.E \ X
hI : ¬M.IsBase (M.E \ I)
B'' : Set α
hB'' : M.IsBase B''
hB''₁ : B' \ I ⊆ B''
hB''₂ : B'' ⊆ B' ∪ B ∧ I ⊆ B''ᶜ
hssu : I ⊂ B''ᶜ ∩ M.E
e : α
heI : e ∉ I
heB'' : e ∉ B''
heE : e ∈ M.E
⊢ Disjoint I B''

Tactic:
exact disjoint_of_subset_left hB''₂.2 disjoint_compl_left

Premises used: Set.disjoint_of_subset_left, disjoint_compl_left, And.right
-- 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
obtain :
  ∀ (I : Set α) (hI : M.IsBasis I (M.E \ X)),
    ∃ (J : Set α),
      I' ⊆ J ∧
        Maximal (fun (K : Set α) ↦ (fun (I : Set α) ↦ I ⊆ M.E ∧ ∃ (B : Set α), M.IsBase B ∧ Disjoint I B) K ∧ K ⊆ X) J
⊢ ∃ (J : Set α),
    I' ⊆ J ∧
      Maximal (fun (K : Set α) ↦ (fun (I : Set α) ↦ I ⊆ M.E ∧ ∃ (B : Set α), M.IsBase B ∧ Disjoint I B) K ∧ K ⊆ X) J

Tactic:
obtain ⟨I, hI⟩ := M.exists_isBasis (M.E \ X)

Premises used: Matroid.E, SDiff.sdiff, Matroid.exists_isBasis
-- Module: Mathlib.Combinatorics.Matroid.Dual
Goal:
α : Type u_1
M_1 : Matroid α
I_1 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
I : Set α
hI : M.IsBasis I (M.E \ X)
obtain :
  ∀ (B' : Set α) (hB' : M.IsBase B') (hIB' : I ⊆ B') (hB'IB : B' ⊆ I ∪ B),
    ∃ (J : Set α),
      I' ⊆ J ∧
        Maximal (fun (K : Set α) ↦ (fun (I : Set α) ↦ I ⊆ M.E ∧ ∃ (B : Set α), M.IsBase B ∧ Disjoint I B) K ∧ K ⊆ X) J
⊢ ∃ (J : Set α),
    I' ⊆ J ∧
      Maximal (fun (K : Set α) ↦ (fun (I : Set α) ↦ I ⊆ M.E ∧ ∃ (B : Set α), M.IsBase B ∧ Disjoint I B) K ∧ K ⊆ X) J

Tactic:
obtain ⟨B', hB', hIB', hB'IB⟩ := hI.indep.exists_isBase_subset_union_isBase hB

Premises used: Matroid.IsBasis.indep, Matroid.Indep.exists_isBase_subset_union_isBase
-- Module: Mathlib.Combinatorics.Matroid.Dual
Goal:
α : Type u_1
M_1 : Matroid α
I_1 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
I : Set α
hI : M.IsBasis I (M.E \ X)
B' : Set α
hB' : M.IsBase B'
hIB' : I ⊆ B'
hB'IB : B' ⊆ I ∪ B
⊢ I = B' \ X

Tactic:
hI.eq_of_subset_indep (hB'.indep.diff _)
      (subset_diff.2 ⟨hIB', (subset_diff.1 hI.subset).2⟩)
      (diff_subset_diff_left hB'.subset_ground)

Premises used: Iff.mpr, Matroid.Indep.diff, Set.subset_diff, Set.diff_subset_diff_left, Matroid.IsBase.subset_ground, Matroid.IsBasis.subset, Matroid.IsBasis.eq_of_subset_indep, And.right, And.intro, Iff.mp, Matroid.IsBase.indep
-- Module: Mathlib.Combinatorics.Matroid.Dual
Goal:
α : Type u_1
M_1 : Matroid α
I_1 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
I : Set α
hI : M.IsBasis I (M.E \ X)
B' : Set α
hB' : M.IsBase B'
hIB' : I ⊆ B'
hB'IB : B' ⊆ I ∪ B
⊢ M.IsBasis (B' \ X) (M.E \ X)

Tactic:
obtain rfl : I = B' \ X := hI.eq_of_subset_indep (hB'.indep.diff _)
      (subset_diff.2 ⟨hIB', (subset_diff.1 hI.subset).2⟩)
      (diff_subset_diff_left hB'.subset_ground)

Premises used: Iff.mpr, Matroid.Indep.diff, Set.subset_diff, Set.diff_subset_diff_left, Matroid.IsBase.subset_ground, Matroid.IsBasis.subset, Matroid.IsBasis.eq_of_subset_indep, And.right, And.intro, Iff.mp, Matroid.IsBase.indep, rfl
-- Module: Mathlib.Combinatorics.Matroid.Dual
Goal:
α : Type u_1
M_1 : Matroid α
I_1 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
I : Set α
hI : M.IsBasis I (M.E \ X)
B' : Set α
hB' : M.IsBase B'
hIB' : I ⊆ B'
hB'IB : B' ⊆ I ∪ B
hI₁ : M.IsBasis (B' \ X) (M.E \ X)
⊢ B' \ X ⊆ B'

Tactic:
obtain rfl : I = B' \ X := hI.eq_of_subset_indep (hB'.indep.diff _)
      (subset_diff.2 ⟨hIB', (subset_diff.1 hI.subset).2⟩)
      (diff_subset_diff_left hB'.subset_ground)

Premises used: Iff.mpr, Matroid.Indep.diff, Set.subset_diff, Set.diff_subset_diff_left, Matroid.IsBase.subset_ground, Matroid.IsBasis.subset, Matroid.IsBasis.eq_of_subset_indep, And.right, And.intro, Iff.mp, Matroid.IsBase.indep, rfl
-- Module: Mathlib.Combinatorics.Matroid.Dual
Goal:
α : Type u_1
M_1 : Matroid α
I_1 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
I : Set α
hI : M.IsBasis I (M.E \ X)
B' : Set α
hB' : M.IsBase B'
hIB' : I ⊆ B'
hB'IB : B' ⊆ I ∪ B
hI₁ : M.IsBasis (B' \ X) (M.E \ X)
hIB'₁ : B' \ X ⊆ B'
⊢ B' ⊆ B' \ X ∪ B

Tactic:
obtain rfl : I = B' \ X := hI.eq_of_subset_indep (hB'.indep.diff _)
      (subset_diff.2 ⟨hIB', (subset_diff.1 hI.subset).2⟩)
      (diff_subset_diff_left hB'.subset_ground)

Premises used: Iff.mpr, Matroid.Indep.diff, Set.subset_diff, Set.diff_subset_diff_left, Matroid.IsBase.subset_ground, Matroid.IsBasis.subset, Matroid.IsBasis.eq_of_subset_indep, And.right, And.intro, Iff.mp, Matroid.IsBase.indep, 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
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 α),
    I' ⊆ J ∧
      ((J ⊆ M.E ∧ ∃ (B : Set α), M.IsBase B ∧ Disjoint J B) ∧ J ⊆ X) ∧
        ∀ ⦃t : Set α⦄, (t ⊆ M.E ∧ ∃ (B : Set α), M.IsBase B ∧ Disjoint t B) ∧ t ⊆ X → J ⊆ t → t ⊆ J

Tactic:
⟨(X \ B') ∩ M.E, ?_, ⟨⟨inter_subset_right, ?_⟩, ?_⟩, ?_⟩

Premises used: Matroid.E, Inter.inter, SDiff.sdiff, And.intro, Exists.intro, Set.inter_subset_right
-- 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
refine_1 : I' ⊆ X \ B' ∩ M.E
refine_2 : ∃ (B : Set α), M.IsBase B ∧ Disjoint (X \ B' ∩ M.E) B
refine_3 : X \ B' ∩ M.E ⊆ X
refine_4 :
  ∀ ⦃t : Set α⦄, (t ⊆ M.E ∧ ∃ (B : Set α), M.IsBase B ∧ Disjoint t B) ∧ t ⊆ X → X \ B' ∩ M.E ⊆ t → t ⊆ X \ B' ∩ M.E
⊢ ∃ (J : Set α),
    I' ⊆ J ∧
      ((J ⊆ M.E ∧ ∃ (B : Set α), M.IsBase B ∧ Disjoint J B) ∧ J ⊆ X) ∧
        ∀ ⦃t : Set α⦄, (t ⊆ M.E ∧ ∃ (B : Set α), M.IsBase B ∧ Disjoint t B) ∧ t ⊆ X → J ⊆ t → t ⊆ J

Tactic:
refine ⟨(X \ B') ∩ M.E, ?_, ⟨⟨inter_subset_right, ?_⟩, ?_⟩, ?_⟩
-- 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
refine_1 : Disjoint I' B'
⊢ I' ⊆ X \ B' ∩ M.E

Tactic:
rw [subset_inter_iff, and_iff_left hI'E, subset_diff, and_iff_right hI'X]

Premises used: Set.subset_inter_iff, and_iff_left, Set.subset_diff, and_iff_right
-- 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
⊢ Disjoint I' B'

Tactic:
Disjoint.mono_right hB'IB <| disjoint_union_right.2
        ⟨disjoint_sdiff_right.mono_left hI'X, hI'B⟩

Premises used: Iff.mpr, Set.disjoint_union_right, Disjoint.mono_left, And.intro, Set.disjoint_sdiff_right, Disjoint.mono_right
-- 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
⊢ Disjoint I' B'

Tactic:
exact Disjoint.mono_right hB'IB <| disjoint_union_right.2
        ⟨disjoint_sdiff_right.mono_left hI'X, hI'B⟩

Premises used: Iff.mpr, Set.disjoint_union_right, Disjoint.mono_left, And.intro, Set.disjoint_sdiff_right, Disjoint.mono_right
-- 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
⊢ ∃ (B : Set α), M.IsBase B ∧ Disjoint (X \ B' ∩ M.E) B

Tactic:
⟨B', hB', (disjoint_sdiff_left (t := X)).mono_left inter_subset_left⟩

Premises used: Set.inter_subset_left, Disjoint.mono_left, Set.disjoint_sdiff_left, And.intro, Exists.intro
-- 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
⊢ ∃ (B : Set α), M.IsBase B ∧ Disjoint (X \ B' ∩ M.E) B

Tactic:
exact ⟨B', hB', (disjoint_sdiff_left (t := X)).mono_left inter_subset_left⟩
-- 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
⊢ X \ B' ∩ M.E ⊆ X

Tactic:
inter_subset_left.trans diff_subset

Premises used: Set.diff_subset, HasSubset.Subset.trans, Set.inter_subset_left
-- 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
⊢ X \ B' ∩ M.E ⊆ X

Tactic:
exact inter_subset_left.trans diff_subset

Premises used: Set.diff_subset, HasSubset.Subset.trans, Set.inter_subset_left
-- 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
refine_4 :
  ∀ ⦃t : Set α⦄,
    t ⊆ M.E → ∀ (x : Set α), M.IsBase x → Disjoint t x → t ⊆ X → X \ B' ∩ M.E ⊆ t → (t ⊆ X ∧ Disjoint t B') ∧ t ⊆ M.E
⊢ ∀ ⦃t : Set α⦄, (t ⊆ M.E ∧ ∃ (B : Set α), M.IsBase B ∧ Disjoint t B) ∧ t ⊆ X → X \ B' ∩ M.E ⊆ t → t ⊆ X \ B' ∩ M.E

Tactic:
simp only [subset_inter_iff, subset_diff, and_imp, forall_exists_index]

Premises used: and_imp, Set.subset_inter_iff, forall_exists_index, Set.subset_diff
-- 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
⊢ ∀ ⦃t : Set α⦄,
    t ⊆ M.E → ∀ (x : Set α), M.IsBase x → Disjoint t x → t ⊆ X → X \ B' ∩ M.E ⊆ t → (t ⊆ X ∧ Disjoint t B') ∧ t ⊆ M.E

Tactic:
fun J hJE B'' hB'' hdj hJX hXJ ↦ ⟨⟨hJX, ?_⟩, hJE⟩

Premises used: And.intro
-- 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
refine_4 :
  ∀ (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), Disjoint J B'
⊢ ∀ ⦃t : Set α⦄,
    t ⊆ M.E → ∀ (x : Set α), M.IsBase x → Disjoint t x → t ⊆ X → X \ B' ∩ M.E ⊆ t → (t ⊆ X ∧ Disjoint t B') ∧ t ⊆ M.E

Tactic:
refine fun J hJE B'' hB'' hdj hJX hXJ ↦ ⟨⟨hJX, ?_⟩, hJE⟩
-- 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
rw : X \ B' ∩ B'' ⊆ J
⊢ B'' ∩ X ∪ B' \ X ⊆ B'

Tactic:
rw [union_subset_iff, and_iff_left diff_subset, ← union_diff_cancel hJX,
        inter_union_distrib_left, hdj.symm.inter_eq, empty_union, diff_eq, ← inter_assoc,
        ← diff_eq, diff_subset_comm, diff_eq, inter_assoc, ← diff_eq, inter_comm]

Premises used: Set.diff_subset, Set.union_subset_iff, and_iff_left, Set.empty_union, Set.diff_eq, Set.diff_subset_comm, Set.union_diff_cancel, Set.inter_comm, Disjoint.symm, Disjoint.inter_eq, Set.inter_assoc, Set.inter_union_distrib_left
-- 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
⊢ X \ B' ∩ B'' ⊆ J

Tactic:
subset_trans (inter_subset_inter_right _ hB''.subset_ground) hXJ

Premises used: Set.inter_subset_inter_right, subset_trans, Matroid.IsBase.subset_ground
-- 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
⊢ X \ B' ∩ B'' ⊆ J

Tactic:
exact subset_trans (inter_subset_inter_right _ hB''.subset_ground) hXJ

Premises used: Set.inter_subset_inter_right, subset_trans, Matroid.IsBase.subset_ground
-- 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
⊢ B'' ∩ X ∪ B' \ X ⊆ B'

Tactic:
have hI' : (B'' ∩ X) ∪ (B' \ X) ⊆ B' := by
      rw [union_subset_iff, and_iff_left diff_subset, ← union_diff_cancel hJX,
        inter_union_distrib_left, hdj.symm.inter_eq, empty_union, diff_eq, ← inter_assoc,
        ← diff_eq, diff_subset_comm, diff_eq, inter_assoc, ← diff_eq, inter_comm]
      exact subset_trans (inter_subset_inter_right _ hB''.subset_ground) hXJ
-- 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'
refine_4 :
  ∀ (B₁ : Set α) (hB₁ : M.IsBase B₁) (hI'B₁ : B'' ∩ X ∪ B' \ X ⊆ B₁) (hB₁I : B₁ ⊆ B'' ∩ X ∪ B' \ X ∪ B''), Disjoint J B'
⊢ Disjoint J B'

Tactic:
obtain ⟨B₁, hB₁, hI'B₁, hB₁I⟩ := (hB'.indep.subset hI').exists_isBase_subset_union_isBase hB''

Premises used: Matroid.Indep.subset, Matroid.IsBase.indep, Matroid.Indep.exists_isBase_subset_union_isBase