awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.Matroid.Constructions
Goal:
α : Type u_1
M : Matroid α
E B I X R J : Set α
⊢ ∀ (I : Set α), (∀ J ⊆ I, J.Finite → J ⊆ E) → I ⊆ E

Tactic:
exact fun I h e heI ↦ by simpa using h {e} (by simpa)
-- Module: Mathlib.Combinatorics.Matroid.Constructions
Goal:
α : Type u_1
E : Set α
hE : E.Nonempty
⊢ (freeOn E).RankPos

Tactic:
simp [rankPos_iff, hE.ne_empty.symm]

Premises used: Matroid.rankPos_iff, Set.Nonempty.ne_empty, Ne.symm
-- Module: Mathlib.Combinatorics.Matroid.Constructions
Goal:
α : Type u_1
E I : Set α
⊢ (uniqueBaseOn I E).E = E

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Combinatorics.Matroid.Constructions
Goal:
α : Type u_1
E B I : Set α
hIE : I ⊆ E
rw : (freeOn I ↾ E).IsBase B ↔ B = I
rw₁ : (freeOn I).IsBasis' B E ↔ B = I
rw₂ : B = E ∩ I ↔ B = I
rw₃ rw₄ : B = I ↔ B = I
⊢ (uniqueBaseOn I E).IsBase B ↔ B = I

Tactic:
rw [uniqueBaseOn, isBase_restrict_iff', freeOn_isBasis'_iff, inter_eq_self_of_subset_right hIE]

Premises used: Matroid.isBase_restrict_iff', Matroid.freeOn_isBasis'_iff, Matroid.uniqueBaseOn, Set.inter_eq_self_of_subset_right
-- Module: Mathlib.Combinatorics.Matroid.Constructions
Goal:
α : Type u_1
I E : Set α
simp : ∀ I_1 ⊆ E, I_1 ⊆ I ∧ I_1 ⊆ E ↔ I_1 ⊆ I
⊢ uniqueBaseOn (I ∩ E) E = uniqueBaseOn I E

Tactic:
simp only [uniqueBaseOn, restrict_eq_restrict_iff, freeOn_indep_iff, subset_inter_iff]

Premises used: Set.subset_inter_iff, Matroid.restrict_eq_restrict_iff, Matroid.uniqueBaseOn, Matroid.freeOn_indep_iff
-- Module: Mathlib.Combinatorics.Matroid.Constructions
Goal:
α : Type u_1
I E : Set α
tauto tauto₁ : ∀ I_1 ⊆ E, I_1 ⊆ I ∧ I_1 ⊆ E ↔ I_1 ⊆ I
mp : ∀ I_1 ⊆ E, I_1 ⊆ I ∧ I_1 ⊆ E → I_1 ⊆ I
mpr : ∀ I_1 ⊆ E, I_1 ⊆ I → I_1 ⊆ I ∧ I_1 ⊆ E
mp₁ mp₂ : ∀ I_1 ⊆ E, I_1 ⊆ I → I_1 ⊆ E → I_1 ⊆ I
mp₃ : ∀ I_1 ⊆ E, I_1 ⊆ I → I_1 ⊆ E → ∀ ⦃a : α⦄, a ∈ I_1 → a ∈ I
mpr₁ mpr₂ : ∀ I_1 ⊆ E, I_1 ⊆ I → I_1 ⊆ I ∧ I_1 ⊆ E
mpr₃ : ∀ I_1 ⊆ E, I_1 ⊆ I → I_1 ⊆ I
mpr₄ : ∀ I_1 ⊆ E, I_1 ⊆ I → I_1 ⊆ E
mp₄ mp₅ mp₆ mp₇ mp₈ mp₉ mp₁₀ mp₁₁ : ∀ I_1 ⊆ E, I_1 ⊆ I → I_1 ⊆ E → ∀ ⦃a : α⦄, a ∈ I_1 → a ∈ I
⊢ ∀ I_1 ⊆ E, I_1 ⊆ I ∧ I_1 ⊆ E ↔ I_1 ⊆ I

Tactic:
tauto
-- Module: Mathlib.Combinatorics.Matroid.Constructions
Goal:
α : Type u_1
E I J : Set α
rw : (freeOn I ↾ E).Indep J ↔ J ⊆ I ∩ E
rw₁ : (freeOn I).Indep J ∧ J ⊆ E ↔ J ⊆ I ∩ E
rw₂ : J ⊆ I ∧ J ⊆ E ↔ J ⊆ I ∩ E
rw₃ rw₄ : J ⊆ I ∧ J ⊆ E ↔ J ⊆ I ∧ J ⊆ E
⊢ (uniqueBaseOn I E).Indep J ↔ J ⊆ I ∩ E

Tactic:
rw [uniqueBaseOn, restrict_indep_iff, freeOn_indep_iff, subset_inter_iff]

Premises used: Set.subset_inter_iff, Matroid.uniqueBaseOn, Matroid.restrict_indep_iff, Matroid.freeOn_indep_iff
-- Module: Mathlib.Combinatorics.Matroid.Constructions
Goal:
α : Type u_1
E I J : Set α
hIE : I ⊆ E
rw : J ⊆ I → J ⊆ E
⊢ (uniqueBaseOn I E).Indep J ↔ J ⊆ I

Tactic:
rw [uniqueBaseOn, restrict_indep_iff, freeOn_indep_iff, and_iff_left_iff_imp]

Premises used: Matroid.uniqueBaseOn, Matroid.restrict_indep_iff, Matroid.freeOn_indep_iff, and_iff_left_iff_imp
-- Module: Mathlib.Combinatorics.Matroid.Constructions
Goal:
α : Type u_1
E I J : Set α
hIE : I ⊆ E
⊢ J ⊆ I → J ⊆ E

Tactic:
fun h ↦ h.trans hIE

Premises used: HasSubset.Subset.trans
-- Module: Mathlib.Combinatorics.Matroid.Constructions
Goal:
α : Type u_1
E I J : Set α
hIE : I ⊆ E
⊢ J ⊆ I → J ⊆ E

Tactic:
exact fun h ↦ h.trans hIE
-- Module: Mathlib.Combinatorics.Matroid.Constructions
Goal:
α : Type u_1
E I X J : Set α
hX : X ⊆ E
rw : Maximal (fun (I_1 : Set α) ↦ (uniqueBaseOn I E).Indep I_1 ∧ I_1 ⊆ X) J ↔ J = X ∩ I
⊢ (uniqueBaseOn I E).IsBasis J X ↔ J = X ∩ I

Tactic:
rw [isBasis_iff_maximal]

Premises used: Matroid.isBasis_iff_maximal
-- Module: Mathlib.Combinatorics.Matroid.Constructions
Goal:
α : Type u_1
E I X J : Set α
hX : X ⊆ E
⊢ (uniqueBaseOn I E).Indep (X ∩ I) ∧ X ∩ I ⊆ X

Tactic:
simp [inter_subset_left.trans hX]

Premises used: HasSubset.Subset.trans, Set.inter_subset_left
-- Module: Mathlib.Combinatorics.Matroid.Constructions
Goal:
α : Type u_1
E I X J : Set α
hX : X ⊆ E
⊢ ∀ ⦃x : Set α⦄, (uniqueBaseOn I E).Indep x ∧ x ⊆ X → x ≤ X ∩ I

Tactic:
simp +contextual
-- Module: Mathlib.Combinatorics.Matroid.Constructions
Goal:
α : Type u_1
E I X J : Set α
hX : X ⊆ E
⊢ Maximal (fun (I_1 : Set α) ↦ (uniqueBaseOn I E).Indep I_1 ∧ I_1 ⊆ X) J ↔ J = X ∩ I

Tactic:
exact maximal_iff_eq (by simp [inter_subset_left.trans hX])
    (by simp +contextual)

Premises used: maximal_iff_eq
-- Module: Mathlib.Combinatorics.Matroid.Constructions
Goal:
α : Type u_1
E I X : Set α
hX : X ⊆ E
rw rw₁ : X ∩ I = X ∩ I
⊢ (uniqueBaseOn I E).IsBasis (X ∩ I) X

Tactic:
rw [uniqueBaseOn_isBasis_iff hX]

Premises used: Matroid.uniqueBaseOn_isBasis_iff
-- Module: Mathlib.Combinatorics.Matroid.Constructions
Goal:
α : Type u_1
I E : Set α
rw : (uniqueBaseOn (I ∩ E) E)✶ = uniqueBaseOn (E \ I) E
⊢ (uniqueBaseOn I E)✶ = uniqueBaseOn (E \ I) E

Tactic:
rw [← uniqueBaseOn_inter_ground_eq]

Premises used: Matroid.uniqueBaseOn_inter_ground_eq
-- Module: Mathlib.Combinatorics.Matroid.Constructions
Goal:
α : Type u_1
I E : Set α
⊢ (uniqueBaseOn (I ∩ E) E)✶ = uniqueBaseOn (E \ I) E

Tactic:
ext_isBase rfl (fun B (hB : B ⊆ E) ↦ ?_)

Premises used: Matroid.ext_isBase, rfl
-- Module: Mathlib.Combinatorics.Matroid.Constructions
Goal:
α : Type u_1
I E : Set α
refine : ∀ (B : Set α) (hB : B ⊆ E), (uniqueBaseOn (I ∩ E) E)✶.IsBase B ↔ (uniqueBaseOn (E \ I) E).IsBase B
⊢ (uniqueBaseOn (I ∩ E) E)✶ = uniqueBaseOn (E \ I) E

Tactic:
refine ext_isBase rfl (fun B (hB : B ⊆ E) ↦ ?_)

Premises used: Matroid.ext_isBase, rfl
-- Module: Mathlib.Combinatorics.Matroid.Constructions
Goal:
α : Type u_1
I E B : Set α
hB : B ⊆ E
rw : E \ B = I ∩ E ↔ B = E \ I
⊢ (uniqueBaseOn (I ∩ E) E)✶.IsBase B ↔ (uniqueBaseOn (E \ I) E).IsBase B

Tactic:
rw [dual_isBase_iff, uniqueBaseOn_isBase_iff inter_subset_right,
    uniqueBaseOn_isBase_iff diff_subset, uniqueBaseOn_ground]

Premises used: Set.diff_subset, Matroid.dual_isBase_iff, Matroid.uniqueBaseOn_ground, Set.inter_subset_right, Matroid.uniqueBaseOn_isBase_iff
-- Module: Mathlib.Combinatorics.Matroid.Constructions
Goal:
α : Type u_1
I E B : Set α
hB : B ⊆ E
h : E \ B = I ∩ E
rw : E \ (E \ B) = E \ I
rw₁ : E \ (I ∩ E) = E \ I
rw₂ rw₃ : E \ I = E \ I
⊢ B = E \ I

Tactic:
rw [← diff_diff_cancel_left hB, h, diff_inter_self_eq_diff]

Premises used: Set.diff_inter_self_eq_diff, Set.diff_diff_cancel_left
-- Module: Mathlib.Combinatorics.Matroid.Constructions
Goal:
α : Type u_1
I E B : Set α
hB : B ⊆ E
h : B = E \ I
rw : E \ (E \ I) = E ∩ I
⊢ E \ B = I ∩ E

Tactic:
rw [h, inter_comm I]

Premises used: Set.inter_comm
-- Module: Mathlib.Combinatorics.Matroid.Constructions
Goal:
α : Type u_1
I E B : Set α
hB : B ⊆ E
h : B = E \ I
⊢ E \ (E \ I) = E ∩ I

Tactic:
simp
-- Module: Mathlib.Combinatorics.Matroid.Constructions
Goal:
α : Type u_1
I E B : Set α
hB : B ⊆ E
⊢ E \ B = I ∩ E ↔ B = E \ I

Tactic:
exact ⟨fun h ↦ by rw [← diff_diff_cancel_left hB, h, diff_inter_self_eq_diff],
    fun h ↦ by rw [h, inter_comm I]; simp⟩
-- Module: Mathlib.Combinatorics.Matroid.Constructions
Goal:
α : Type u_1
I : Set α
rw : freeOn I ↾ I = freeOn I
rw₁ rw₂ : freeOn I = freeOn I
⊢ uniqueBaseOn I I = freeOn I

Tactic:
rw [uniqueBaseOn, freeOn_restrict rfl.subset]

Premises used: Matroid.freeOn_restrict, Matroid.uniqueBaseOn, Eq.subset, rfl
-- Module: Mathlib.Combinatorics.Matroid.Constructions
Goal:
α : Type u_1
I : Set α
rw : (uniqueBaseOn ∅ I)✶ = (loopyOn I)✶
rw₁ : uniqueBaseOn (I \ ∅) I = (loopyOn I)✶
rw₂ : uniqueBaseOn I I = (loopyOn I)✶
rw₃ : freeOn I = (loopyOn I)✶
rw₄ rw₅ : freeOn I = freeOn I
⊢ uniqueBaseOn ∅ I = loopyOn I

Tactic:
rw [← dual_inj, uniqueBaseOn_dual_eq, diff_empty, uniqueBaseOn_self, loopyOn_dual_eq]

Premises used: Matroid.uniqueBaseOn_self, Matroid.uniqueBaseOn_dual_eq, Set.diff_empty, Matroid.loopyOn_dual_eq, Matroid.dual_inj
-- Module: Mathlib.Combinatorics.Matroid.Constructions
Goal:
α : Type u_1
I E R : Set α
simp_rw : ∀ ⦃I_1 : Set α⦄, I_1 ⊆ R → ((I_1 ⊆ I ∧ I_1 ⊆ E) ∧ I_1 ⊆ R ↔ ((I_1 ⊆ I ∧ I_1 ⊆ R) ∧ I_1 ⊆ E) ∧ I_1 ⊆ R)
⊢ uniqueBaseOn I E ↾ R = uniqueBaseOn (I ∩ R ∩ E) R

Tactic:
simp_rw [ext_iff_indep, restrict_ground_eq, uniqueBaseOn_ground, true_and,
    restrict_indep_iff, uniqueBaseOn_indep_iff', subset_inter_iff]

Premises used: Matroid.uniqueBaseOn_indep_iff', Set.subset_inter_iff, Matroid.restrict_ground_eq, Matroid.uniqueBaseOn_ground, Matroid.restrict_indep_iff, Matroid.ext_iff_indep, true_and
-- Module: Mathlib.Combinatorics.Matroid.Constructions
Goal:
α : Type u_1
I E R : Set α
tauto tauto₁ : ∀ ⦃I_1 : Set α⦄, I_1 ⊆ R → ((I_1 ⊆ I ∧ I_1 ⊆ E) ∧ I_1 ⊆ R ↔ ((I_1 ⊆ I ∧ I_1 ⊆ R) ∧ I_1 ⊆ E) ∧ I_1 ⊆ R)
mp : ∀ ⦃I_1 : Set α⦄, I_1 ⊆ R → (I_1 ⊆ I ∧ I_1 ⊆ E) ∧ I_1 ⊆ R → ((I_1 ⊆ I ∧ I_1 ⊆ R) ∧ I_1 ⊆ E) ∧ I_1 ⊆ R
mpr : ∀ ⦃I_1 : Set α⦄, I_1 ⊆ R → ((I_1 ⊆ I ∧ I_1 ⊆ R) ∧ I_1 ⊆ E) ∧ I_1 ⊆ R → (I_1 ⊆ I ∧ I_1 ⊆ E) ∧ I_1 ⊆ R
mp₁ mp₂ : ∀ ⦃I_1 : Set α⦄, I_1 ⊆ R → I_1 ⊆ R → I_1 ⊆ I → I_1 ⊆ E → ((I_1 ⊆ I ∧ I_1 ⊆ R) ∧ I_1 ⊆ E) ∧ I_1 ⊆ R
mp₃ : ∀ ⦃I_1 : Set α⦄, I_1 ⊆ R → I_1 ⊆ R → I_1 ⊆ I → I_1 ⊆ E → I_1 ⊆ I
mp₄ : ∀ ⦃I_1 : Set α⦄, I_1 ⊆ R → I_1 ⊆ R → I_1 ⊆ I → I_1 ⊆ E → I_1 ⊆ R
mp₅ : ∀ ⦃I_1 : Set α⦄, I_1 ⊆ R → I_1 ⊆ R → I_1 ⊆ I → I_1 ⊆ E → I_1 ⊆ E
mp₆ : ∀ ⦃I_1 : Set α⦄, I_1 ⊆ R → I_1 ⊆ R → I_1 ⊆ I → I_1 ⊆ E → I_1 ⊆ R
mpr₁ mpr₂ : ∀ ⦃I_1 : Set α⦄, I_1 ⊆ R → I_1 ⊆ R → I_1 ⊆ E → I_1 ⊆ I → I_1 ⊆ R → (I_1 ⊆ I ∧ I_1 ⊆ E) ∧ I_1 ⊆ R
mpr₃ : ∀ ⦃I_1 : Set α⦄, I_1 ⊆ R → I_1 ⊆ R → I_1 ⊆ E → I_1 ⊆ I → I_1 ⊆ R → I_1 ⊆ I
mpr₄ : ∀ ⦃I_1 : Set α⦄, I_1 ⊆ R → I_1 ⊆ R → I_1 ⊆ E → I_1 ⊆ I → I_1 ⊆ R → I_1 ⊆ E
mpr₅ : ∀ ⦃I_1 : Set α⦄, I_1 ⊆ R → I_1 ⊆ R → I_1 ⊆ E → I_1 ⊆ I → I_1 ⊆ R → I_1 ⊆ R
⊢ ∀ ⦃I_1 : Set α⦄, I_1 ⊆ R → ((I_1 ⊆ I ∧ I_1 ⊆ E) ∧ I_1 ⊆ R ↔ ((I_1 ⊆ I ∧ I_1 ⊆ R) ∧ I_1 ⊆ E) ∧ I_1 ⊆ R)

Tactic:
tauto
-- Module: Mathlib.Combinatorics.Matroid.Constructions
Goal:
α : Type u_1
E I : Set α
h : I ⊆ E
R : Set α
rw : uniqueBaseOn (I ∩ R ∩ E) R = uniqueBaseOn (I ∩ R) R
rw₁ : uniqueBaseOn (I ∩ E ∩ R) R = uniqueBaseOn (I ∩ R) R
rw₂ rw₃ : uniqueBaseOn (I ∩ R) R = uniqueBaseOn (I ∩ R) R
⊢ uniqueBaseOn I E ↾ R = uniqueBaseOn (I ∩ R) R

Tactic:
rw [uniqueBaseOn_restrict', inter_right_comm, inter_eq_self_of_subset_left h]

Premises used: Matroid.uniqueBaseOn_restrict', Set.inter_right_comm, Set.inter_eq_self_of_subset_left
-- Module: Mathlib.Combinatorics.Matroid.Constructions
Goal:
α : Type u_1
E I : Set α
hI : I.Finite
rw : (uniqueBaseOn (I ∩ E) E).RankFinite
⊢ (uniqueBaseOn I E).RankFinite

Tactic:
rw [← uniqueBaseOn_inter_ground_eq]

Premises used: Matroid.uniqueBaseOn_inter_ground_eq
-- Module: Mathlib.Combinatorics.Matroid.Constructions
Goal:
α : Type u_1
E I : Set α
hI : I.Finite
⊢ (uniqueBaseOn (I ∩ E) E).RankFinite

Tactic:
⟨I ∩ E, ?_⟩

Premises used: Matroid.RankFinite.mk, Inter.inter, Exists.intro
-- Module: Mathlib.Combinatorics.Matroid.Constructions
Goal:
α : Type u_1
E I : Set α
hI : I.Finite
refine : (uniqueBaseOn (I ∩ E) E).IsBase (I ∩ E) ∧ (I ∩ E).Finite
⊢ (uniqueBaseOn (I ∩ E) E).RankFinite

Tactic:
refine ⟨I ∩ E, ?_⟩
-- Module: Mathlib.Combinatorics.Matroid.Constructions
Goal:
α : Type u_1
E I : Set α
hI : I.Finite
rw : (I ∩ E).Finite
⊢ (uniqueBaseOn (I ∩ E) E).IsBase (I ∩ E) ∧ (I ∩ E).Finite

Tactic:
rw [uniqueBaseOn_isBase_iff inter_subset_right, and_iff_right rfl]

Premises used: and_iff_right, rfl, Set.inter_subset_right, Matroid.uniqueBaseOn_isBase_iff
-- Module: Mathlib.Combinatorics.Matroid.Constructions
Goal:
α : Type u_1
E I : Set α
hI : I.Finite
⊢ (I ∩ E).Finite

Tactic:
hI.subset inter_subset_left

Premises used: Set.inter_subset_left, Set.Finite.subset
-- Module: Mathlib.Combinatorics.Matroid.Constructions
Goal:
α : Type u_1
E I : Set α
hI : I.Finite
⊢ (I ∩ E).Finite

Tactic:
exact hI.subset inter_subset_left

Premises used: Set.inter_subset_left, Set.Finite.subset
-- Module: Mathlib.Combinatorics.Matroid.Constructions
Goal:
α : Type u_1
M : Matroid α
E B I X R J : Set α
⊢ (uniqueBaseOn I E).Finitary

Tactic:
⟨fun K hK ↦ ?_⟩

Premises used: Matroid.Finitary.mk
-- Module: Mathlib.Combinatorics.Matroid.Constructions
Goal:
α : Type u_1
M : Matroid α
E B I X R J : Set α
refine : ∀ (K : Set α) (hK : ∀ J ⊆ K, J.Finite → (uniqueBaseOn I E).Indep J), (uniqueBaseOn I E).Indep K
⊢ (uniqueBaseOn I E).Finitary

Tactic:
refine ⟨fun K hK ↦ ?_⟩
-- Module: Mathlib.Combinatorics.Matroid.Constructions
Goal:
α : Type u_1
M : Matroid α
E B I X R J K : Set α
hK : ∀ J ⊆ K, J.Finite → (uniqueBaseOn I E).Indep J
simp : ∀ (hK : ∀ J ⊆ K, J.Finite → J ⊆ I ∩ E), K ⊆ I ∩ E
⊢ (uniqueBaseOn I E).Indep K

Tactic:
simp only [uniqueBaseOn_indep_iff'] at hK ⊢

Premises used: Matroid.uniqueBaseOn_indep_iff'
-- Module: Mathlib.Combinatorics.Matroid.Constructions
Goal:
α : Type u_1
M : Matroid α
E B I X R J K : Set α
hK : ∀ J ⊆ K, J.Finite → J ⊆ I ∩ E
e : α
heK : e ∈ K
⊢ {e} ⊆ K

Tactic:
simpa
-- Module: Mathlib.Combinatorics.Matroid.Constructions
Goal:
α : Type u_1
M : Matroid α
E B I X R J K : Set α
hK : ∀ J ⊆ K, J.Finite → J ⊆ I ∩ E
e : α
heK : e ∈ K
⊢ Set.Finite (α := α) {e}

Tactic:
simp
-- Module: Mathlib.Combinatorics.Matroid.Constructions
Goal:
α : Type u_1
M : Matroid α
E B I X R J K : Set α
hK : ∀ J ⊆ K, J.Finite → J ⊆ I ∩ E
⊢ K ⊆ I ∩ E

Tactic:
exact fun e heK ↦ singleton_subset_iff.1 <| hK _ (by simpa) (by simp)

Premises used: Set.singleton_subset_iff, Iff.mp, Singleton.singleton
-- Module: Mathlib.Combinatorics.Matroid.Constructions
Goal:
α : Type u_1
E I : Set α
hIE : I ⊆ E
hI : I.Nonempty
⊢ ¬(uniqueBaseOn I E).IsBase ∅

Tactic:
simpa [uniqueBaseOn_isBase_iff hIE] using Ne.symm <| hI.ne_empty

Premises used: Set.Nonempty.ne_empty, Ne.symm, Matroid.uniqueBaseOn_isBase_iff
-- Module: Mathlib.Combinatorics.Matroid.Dual
Goal:
α : Type u_1
M_1 : Matroid α
I_1 B_1 X : Set α
M : Matroid α
I J : Set α
hJE : J ⊆ M.E
B : Set α
hB : M.IsBase B
hJB : Disjoint J B
hIJ : I ⊆ J
⊢ I ⊆ M.E ∧ ∃ (B : Set α), M.IsBase B ∧ Disjoint I B

Tactic:
⟨hIJ.trans hJE, ⟨B, hB, disjoint_of_subset_left hIJ hJB⟩⟩

Premises used: Set.disjoint_of_subset_left, HasSubset.Subset.trans, And.intro, Exists.intro
-- Module: Mathlib.Combinatorics.Matroid.Dual
Goal:
α : Type u_1
M_1 : Matroid α
I_1 B_1 X : Set α
M : Matroid α
I J : Set α
hJE : J ⊆ M.E
B : Set α
hB : M.IsBase B
hJB : Disjoint J B
hIJ : I ⊆ J
⊢ I ⊆ M.E ∧ ∃ (B : Set α), M.IsBase B ∧ Disjoint I B

Tactic:
exact ⟨hIJ.trans hJE, ⟨B, hB, disjoint_of_subset_left hIJ hJB⟩⟩
-- 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
⊢ X ⊆ M.E

Tactic:
have hXE := hX_max.1.1
-- 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
⊢ M.IsBase (M.E \ X)

Tactic:
have hB' := (isBase_compl_iff_maximal_disjoint_isBase hXE).mpr hX_max
-- 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
hB' : M.IsBase (M.E \ X)
⊢ let B' := M.E \ X;
  M.IsBase B'

Tactic:
set B' := M.E \ X with hX

Premises used: Matroid.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
hB' : M.IsBase (M.E \ X)
hB'₁ :
  let B' := M.E \ X;
  M.IsBase B'
⊢ let B' := M.E \ X;
  B' = M.E \ X

Tactic:
set B' := M.E \ X with hX

Premises used: Matroid.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
⊢ ¬M.IsBase (M.E \ I)

Tactic:
have hI := (not_iff_not.mpr (isBase_compl_iff_maximal_disjoint_isBase)).mpr hI_not_max
-- 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)
obtain :
  ∀ (B'' : Set α) (hB'' : M.IsBase B'') (hB''₁ : B' \ I ⊆ B'') (hB''₂ : B'' ⊆ B' \ I ∪ B),
    ∃ 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 ⟨B'', hB'', hB''₁, hB''₂⟩ := (hB'.indep.diff I).exists_isBase_subset_union_isBase hB

Premises used: Matroid.Indep.diff, Matroid.IsBase.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 α
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' \ I ∪ B
⊢ B'' ⊆ B' ∪ B ∧ I ⊆ B''ᶜ

Tactic:
rw [← compl_subset_compl, ← hIB.sdiff_eq_right, ← union_diff_distrib, diff_eq, compl_inter,
      compl_compl, union_subset_iff, compl_subset_compl] at hB''₂

Premises used: Disjoint.sdiff_eq_right, compl_compl, Set.union_subset_iff, Set.compl_inter, Set.diff_eq, Set.compl_subset_compl, Set.union_diff_distrib
-- Module: Mathlib.Combinatorics.Matroid.Dual
Goal:
α : Type u_1
M_1 : Matroid α
I B_1 X_1 : Set α
M : Matroid α
X B : Set α
hB : M.IsBase B
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
B'' : Set α
hB'' : M.IsBase B''
hIE : B''ᶜ ∩ M.E ⊆ M.E
hIB : Disjoint (B''ᶜ ∩ M.E) B
hI_not_max : ¬Maximal (fun (I : Set α) ↦ I ⊆ M.E ∧ ∃ (B : Set α), M.IsBase B ∧ Disjoint I B) (B''ᶜ ∩ M.E)
hI : ¬M.IsBase (M.E \ (B''ᶜ ∩ M.E))
hB''₁ : B' \ (B''ᶜ ∩ M.E) ⊆ B''
hB''₂ : B'' ⊆ B' ∪ B ∧ B''ᶜ ∩ M.E ⊆ B''ᶜ
apply : M.IsBase (M.E \ (B''ᶜ ∩ M.E))
⊢ False

Tactic:
apply hI
-- Module: Mathlib.Combinatorics.Matroid.Dual
Goal:
α : Type u_1
M_1 : Matroid α
I B_1 X_1 : Set α
M : Matroid α
X B : Set α
hB : M.IsBase B
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
B'' : Set α
hB'' : M.IsBase B''
hIE : B''ᶜ ∩ M.E ⊆ M.E
hIB : Disjoint (B''ᶜ ∩ M.E) B
hI_not_max : ¬Maximal (fun (I : Set α) ↦ I ⊆ M.E ∧ ∃ (B : Set α), M.IsBase B ∧ Disjoint I B) (B''ᶜ ∩ M.E)
hI : ¬M.IsBase (M.E \ (B''ᶜ ∩ M.E))
hB''₁ : B' \ (B''ᶜ ∩ M.E) ⊆ B''
hB''₂ : B'' ⊆ B' ∪ B ∧ B''ᶜ ∩ M.E ⊆ B''ᶜ
⊢ M.IsBase B''

Tactic:
hB''
-- Module: Mathlib.Combinatorics.Matroid.Dual
Goal:
α : Type u_1
M_1 : Matroid α
I B_1 X_1 : Set α
M : Matroid α
X B : Set α
hB : M.IsBase B
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
B'' : Set α
hB'' : M.IsBase B''
hIE : B''ᶜ ∩ M.E ⊆ M.E
hIB : Disjoint (B''ᶜ ∩ M.E) B
hI_not_max : ¬Maximal (fun (I : Set α) ↦ I ⊆ M.E ∧ ∃ (B : Set α), M.IsBase B ∧ Disjoint I B) (B''ᶜ ∩ M.E)
hI : ¬M.IsBase (M.E \ (B''ᶜ ∩ M.E))
hB''₁ : B' \ (B''ᶜ ∩ M.E) ⊆ B''
hB''₂ : B'' ⊆ B' ∪ B ∧ B''ᶜ ∩ M.E ⊆ B''ᶜ
h : M.E \ (B''ᶜ ∩ M.E) = B''
⊢ M.IsBase (M.E \ (B''ᶜ ∩ M.E))

Tactic:
convert! hB''
-- Module: Mathlib.Combinatorics.Matroid.Dual
Goal:
α : Type u_1
M_1 : Matroid α
I B_1 X_1 : Set α
M : Matroid α
X B : Set α
hB : M.IsBase B
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
B'' : Set α
hB'' : M.IsBase B''
hIE : B''ᶜ ∩ M.E ⊆ M.E
hIB : Disjoint (B''ᶜ ∩ M.E) B
hI_not_max : ¬Maximal (fun (I : Set α) ↦ I ⊆ M.E ∧ ∃ (B : Set α), M.IsBase B ∧ Disjoint I B) (B''ᶜ ∩ M.E)
hI : ¬M.IsBase (M.E \ (B''ᶜ ∩ M.E))
hB''₁ : B' \ (B''ᶜ ∩ M.E) ⊆ B''
hB''₂ : B'' ⊆ B' ∪ B ∧ B''ᶜ ∩ M.E ⊆ B''ᶜ
⊢ M.E \ (B''ᶜ ∩ M.E) = B''

Tactic:
simp [hB''.subset_ground]

Premises used: Matroid.IsBase.subset_ground
-- 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''ᶜ
rintro rintro₁ :
  ∀ (hIE : B''ᶜ ∩ M.E ⊆ M.E) (hIB : Disjoint (B''ᶜ ∩ M.E) B)
    (hI_not_max : ¬Maximal (fun (I : Set α) ↦ I ⊆ M.E ∧ ∃ (B : Set α), M.IsBase B ∧ Disjoint I B) (B''ᶜ ∩ M.E))
    (hI : ¬M.IsBase (M.E \ (B''ᶜ ∩ M.E))) (hB''₁ : B' \ (B''ᶜ ∩ M.E) ⊆ B'') (hB''₂ : B'' ⊆ B' ∪ B ∧ B''ᶜ ∩ M.E ⊆ B''ᶜ),
    False
rintro₂ rintro₃ :
  ∀ (hIE : B''ᶜ ∩ M.E ⊆ M.E) (hIB : Disjoint (B''ᶜ ∩ M.E) B)
    (hI_not_max : ¬Maximal (fun (I : Set α) ↦ I ⊆ M.E ∧ ∃ (B : Set α), M.IsBase B ∧ Disjoint I B) (B''ᶜ ∩ M.E))
    (hI : ¬M.IsBase (M.E \ (B''ᶜ ∩ M.E))) (hB''₁ : B' \ (B''ᶜ ∩ M.E) ⊆ B'') (hB''₂ : B'' ⊆ B' ∪ B ∧ B''ᶜ ∩ M.E ⊆ B''ᶜ),
    M.IsBase (M.E \ (B''ᶜ ∩ M.E))
h h₁ :
  ∀ (hIE : B''ᶜ ∩ M.E ⊆ M.E) (hIB : Disjoint (B''ᶜ ∩ M.E) B)
    (hI_not_max : ¬Maximal (fun (I : Set α) ↦ I ⊆ M.E ∧ ∃ (B : Set α), M.IsBase B ∧ Disjoint I B) (B''ᶜ ∩ M.E))
    (hI : ¬M.IsBase (M.E \ (B''ᶜ ∩ M.E))) (hB''₁ : B' \ (B''ᶜ ∩ M.E) ⊆ B'') (hB''₂ : B'' ⊆ B' ∪ B ∧ B''ᶜ ∩ M.E ⊆ B''ᶜ),
    M.E \ (B''ᶜ ∩ M.E) = B''
⊢ I ≠ B''ᶜ ∩ M.E

Tactic:
{ rintro rfl; apply hI; convert! hB''; simp [hB''.subset_ground] }

Premises used: Matroid.IsBase.subset_ground, rfl
-- 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''ᶜ
⊢ I ⊂ B''ᶜ ∩ M.E

Tactic:
have hssu := (subset_inter (hB''₂.2) hIE).ssubset_of_ne
      (by { rintro rfl; apply hI; convert! hB''; simp [hB''.subset_ground] })