awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.Matroid.Minor.Order
Goal:
α : Type u_1
M M' N : Matroid α
h : N <m M
h' : M ≤m M'
⊢ N <m M'

Tactic:
h.lt.trans_le h'

Premises used: LT.lt.trans_le, Matroid.IsStrictMinor.lt
-- Module: Mathlib.Combinatorics.Matroid.Minor.Order
Goal:
α : Type u_1
M M' N : Matroid α
h : N ≤m M
h' : M <m M'
⊢ N <m M'

Tactic:
h.le.trans_lt h'

Premises used: Matroid.IsMinor.le, LE.le.trans_lt
-- Module: Mathlib.Combinatorics.Matroid.Minor.Order
Goal:
α : Type u_1
M M' N : Matroid α
h : N <m M
h' : M <m M'
⊢ N <m M'

Tactic:
h.lt.trans h'

Premises used: LT.lt.trans, Matroid.IsStrictMinor.lt
-- Module: Mathlib.Combinatorics.Matroid.Minor.Order
Goal:
α : Type u_1
M N : Matroid α
I : Set α
hI : N.Indep I
hNM : N ≤m M
obtain : ∀ (C D : Set α) (hI : (M ／ C ＼ D).Indep I), M.Indep I
⊢ M.Indep I

Tactic:
obtain ⟨C, D, rfl⟩ := hNM

Premises used: rfl
-- Module: Mathlib.Combinatorics.Matroid.Minor.Order
Goal:
α : Type u_1
M : Matroid α
I C D : Set α
hI : (M ／ C ＼ D).Indep I
⊢ M.Indep I

Tactic:
hI.of_delete.of_contract

Premises used: Matroid.Indep.of_contract, Matroid.Indep.of_delete
-- Module: Mathlib.Combinatorics.Matroid.Minor.Order
Goal:
α : Type u_1
M : Matroid α
I C D : Set α
hI : (M ／ C ＼ D).Indep I
⊢ M.Indep I

Tactic:
exact hI.of_delete.of_contract

Premises used: Matroid.Indep.of_contract, Matroid.Indep.of_delete
-- Module: Mathlib.Combinatorics.Matroid.Minor.Order
Goal:
α : Type u_1
M N : Matroid α
e : α
h : N.IsNonloop e
hNM : N ≤m M
obtain : ∀ (C D : Set α) (h : (M ／ C ＼ D).IsNonloop e), M.IsNonloop e
⊢ M.IsNonloop e

Tactic:
obtain ⟨C, D, rfl⟩ := hNM

Premises used: rfl
-- Module: Mathlib.Combinatorics.Matroid.Minor.Order
Goal:
α : Type u_1
M : Matroid α
e : α
C D : Set α
h : (M ／ C ＼ D).IsNonloop e
⊢ M.IsNonloop e

Tactic:
h.of_delete.of_contract

Premises used: Matroid.IsNonloop.of_contract, Matroid.IsNonloop.of_delete
-- Module: Mathlib.Combinatorics.Matroid.Minor.Order
Goal:
α : Type u_1
M : Matroid α
e : α
C D : Set α
h : (M ／ C ＼ D).IsNonloop e
⊢ M.IsNonloop e

Tactic:
exact h.of_delete.of_contract

Premises used: Matroid.IsNonloop.of_contract, Matroid.IsNonloop.of_delete
-- Module: Mathlib.Combinatorics.Matroid.Minor.Order
Goal:
α : Type u_1
M N : Matroid α
D : Set α
hD : M.Dep D
hDN : D ⊆ N.E
hNM : N ≤m M
⊢ N.Dep D

Tactic:
⟨fun h ↦ hD.not_indep <| h.of_isMinor hNM, hDN⟩

Premises used: Matroid.Dep.not_indep, Matroid.Dep, Matroid.Indep.of_isMinor, And.intro
-- Module: Mathlib.Combinatorics.Matroid.Minor.Order
Goal:
α : Type u_1
M N : Matroid α
e : α
he : M.IsLoop e
heN : e ∈ N.E
hNM : N ≤m M
rw : ∀ (he : M.Dep {e}) (heN : e ∈ N.E) (hNM : N ≤m M), N.Dep {e}
⊢ N.IsLoop e

Tactic:
rw [← singleton_dep] at he ⊢

Premises used: Matroid.singleton_dep
-- Module: Mathlib.Combinatorics.Matroid.Minor.Order
Goal:
α : Type u_1
M N : Matroid α
e : α
he : M.Dep {e}
heN : e ∈ N.E
hNM : N ≤m M
⊢ {e} ⊆ N.E

Tactic:
simpa
-- Module: Mathlib.Combinatorics.Matroid.Minor.Order
Goal:
α : Type u_1
M N : Matroid α
e : α
he : M.Dep {e}
heN : e ∈ N.E
hNM : N ≤m M
⊢ N.Dep {e}

Tactic:
exact he.of_isMinor (by simpa) hNM

Premises used: Matroid.Dep.of_isMinor
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
M_1 : Matroid α
R_1 I_1 X Y : Set α
M : Matroid α
R I I' : Set α
hI : M.Indep I
hIY : I ⊆ R
hIn : ¬M.IsBasis' I R
hI' : M.IsBasis' I' R
⊢ ¬M.IsBasis I (R ∩ M.E)

Tactic:
rw [isBasis'_iff_isBasis_inter_ground] at hIn hI'

Premises used: Matroid.isBasis'_iff_isBasis_inter_ground
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
M_1 : Matroid α
R_1 I_1 X Y : Set α
M : Matroid α
R I I' : Set α
hI : M.Indep I
hIY : I ⊆ R
hIn : ¬M.IsBasis' I R
hI' : M.IsBasis' I' R
hIn₁ : ¬M.IsBasis I (R ∩ M.E)
⊢ M.IsBasis I' (R ∩ M.E)

Tactic:
rw [isBasis'_iff_isBasis_inter_ground] at hIn hI'

Premises used: Matroid.isBasis'_iff_isBasis_inter_ground
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
M_1 : Matroid α
R_1 I_1 X Y : Set α
M : Matroid α
R I I' : Set α
hI : M.Indep I
hIY : I ⊆ R
hIn : ¬M.IsBasis I (R ∩ M.E)
hI' : M.IsBasis I' (R ∩ M.E)
obtain :
  ∀ (B' : Set α) (hB' : M.IsBase B') (hI' : M.IsBasis (B' ∩ (R ∩ M.E)) (R ∩ M.E)),
    ∃ x ∈ (B' ∩ (R ∩ M.E)) \ I, M.Indep (insert x I) ∧ insert x I ⊆ R
⊢ ∃ x ∈ I' \ I, M.Indep (insert x I) ∧ insert x I ⊆ R

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

Premises used: Matroid.IsBasis.exists_isBase, rfl
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
M_1 : Matroid α
R_1 I_1 X Y : Set α
M : Matroid α
R I : Set α
hI : M.Indep I
hIY : I ⊆ R
hIn : ¬M.IsBasis I (R ∩ M.E)
B' : Set α
hB' : M.IsBase B'
hI' : M.IsBasis (B' ∩ (R ∩ M.E)) (R ∩ M.E)
obtain :
  ∀ (B : Set α) (hB : M.IsBase B) (hIB : I ⊆ B) (hBIB' : B ⊆ I ∪ B'),
    ∃ x ∈ (B' ∩ (R ∩ M.E)) \ I, M.Indep (insert x I) ∧ insert x I ⊆ R
⊢ ∃ x ∈ (B' ∩ (R ∩ M.E)) \ I, M.Indep (insert x I) ∧ insert x I ⊆ R

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

Premises used: Matroid.Indep.exists_isBase_subset_union_isBase
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
M_1 : Matroid α
R_1 I_1 X Y : Set α
M : Matroid α
R I : Set α
hI : M.Indep I
hIY : I ⊆ R
hIn : ¬M.IsBasis I (R ∩ M.E)
B' : Set α
hB' : M.IsBase B'
hI' : M.IsBasis (B' ∩ (R ∩ M.E)) (R ∩ M.E)
B : Set α
hB : M.IsBase B
hIB : I ⊆ B
hBIB' : B ⊆ I ∪ B'
rw :
  ∀ (hI' : M✶.IsBasis (M.E \ (B' ∪ R ∩ M.E)) (M.E \ (R ∩ M.E))) (B : Set α) (hB : M.IsBase B) (hIB : I ⊆ B)
    (hBIB' : B ⊆ I ∪ B'), ∃ x ∈ (B' ∩ (R ∩ M.E)) \ I, M.Indep (insert x I) ∧ insert x I ⊆ R
⊢ ∃ x ∈ (B' ∩ (R ∩ M.E)) \ I, M.Indep (insert x I) ∧ insert x I ⊆ R

Tactic:
rw [hB'.inter_isBasis_iff_compl_inter_isBasis_dual, diff_inter_diff] at hI'

Premises used: Matroid.IsBase.inter_isBasis_iff_compl_inter_isBasis_dual, Set.diff_inter_diff
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
M_1 : Matroid α
R_1 I_1 X Y : Set α
M : Matroid α
R I : Set α
hI : M.Indep I
hIY : I ⊆ R
hIn : ¬M.IsBasis I (R ∩ M.E)
B' : Set α
hB' : M.IsBase B'
hI' : M✶.IsBasis (M.E \ (B' ∪ R ∩ M.E)) (M.E \ (R ∩ M.E))
B : Set α
hB : M.IsBase B
hIB : I ⊆ B
hBIB' : B ⊆ I ∪ B'
h : B ∪ R ∩ M.E ⊆ B' ∪ R ∩ M.E
⊢ M.E \ (B' ∪ R ∩ M.E) ⊆ M.E \ (B ∪ R ∩ M.E)

Tactic:
apply diff_subset_diff_right

Premises used: Set.diff_subset_diff_right
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
M_1 : Matroid α
R_1 I_1 X Y : Set α
M : Matroid α
R I : Set α
hI : M.Indep I
hIY : I ⊆ R
hIn : ¬M.IsBasis I (R ∩ M.E)
B' : Set α
hB' : M.IsBase B'
hI' : M✶.IsBasis (M.E \ (B' ∪ R ∩ M.E)) (M.E \ (R ∩ M.E))
B : Set α
hB : M.IsBase B
hIB : I ⊆ B
hBIB' : B ⊆ I ∪ B'
h : B ⊆ R ∩ M.E ∪ B'
⊢ B ∪ R ∩ M.E ⊆ B' ∪ R ∩ M.E

Tactic:
rw [union_subset_iff, and_iff_left subset_union_right, union_comm]

Premises used: Set.union_subset_iff, and_iff_left, Set.subset_union_right, Set.union_comm
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
M_1 : Matroid α
R_1 I_1 X Y : Set α
M : Matroid α
R I : Set α
hI : M.Indep I
hIY : I ⊆ R
hIn : ¬M.IsBasis I (R ∩ M.E)
B' : Set α
hB' : M.IsBase B'
hI' : M✶.IsBasis (M.E \ (B' ∪ R ∩ M.E)) (M.E \ (R ∩ M.E))
B : Set α
hB : M.IsBase B
hIB : I ⊆ B
hBIB' : B ⊆ I ∪ B'
⊢ B ⊆ R ∩ M.E ∪ B'

Tactic:
hBIB'.trans (union_subset_union_left _ (subset_inter hIY hI.subset_ground))

Premises used: HasSubset.Subset.trans, Matroid.Indep.subset_ground, Set.subset_inter, Set.union_subset_union_left
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
M_1 : Matroid α
R_1 I_1 X Y : Set α
M : Matroid α
R I : Set α
hI : M.Indep I
hIY : I ⊆ R
hIn : ¬M.IsBasis I (R ∩ M.E)
B' : Set α
hB' : M.IsBase B'
hI' : M✶.IsBasis (M.E \ (B' ∪ R ∩ M.E)) (M.E \ (R ∩ M.E))
B : Set α
hB : M.IsBase B
hIB : I ⊆ B
hBIB' : B ⊆ I ∪ B'
⊢ B ⊆ R ∩ M.E ∪ B'

Tactic:
exact hBIB'.trans (union_subset_union_left _ (subset_inter hIY hI.subset_ground))

Premises used: HasSubset.Subset.trans, Matroid.Indep.subset_ground, Set.subset_inter, Set.union_subset_union_left
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
M_1 : Matroid α
R_1 I_1 X Y : Set α
M : Matroid α
R I : Set α
hI : M.Indep I
hIY : I ⊆ R
hIn : ¬M.IsBasis I (R ∩ M.E)
B' : Set α
hB' : M.IsBase B'
hI' : M✶.IsBasis (M.E \ (B' ∪ R ∩ M.E)) (M.E \ (R ∩ M.E))
B : Set α
hB : M.IsBase B
hIB : I ⊆ B
hBIB' : B ⊆ I ∪ B'
⊢ M.E \ (B' ∪ R ∩ M.E) ⊆ M.E \ (B ∪ R ∩ M.E)

Tactic:
have hss : M.E \ (B' ∪ (R ∩ M.E)) ⊆ M.E \ (B ∪ (R ∩ M.E)) := by
      apply diff_subset_diff_right
      rw [union_subset_iff, and_iff_left subset_union_right, union_comm]
      exact hBIB'.trans (union_subset_union_left _ (subset_inter hIY hI.subset_ground))
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
M_1 : Matroid α
R_1 I_1 X Y : Set α
M : Matroid α
R I : Set α
hI : M.Indep I
hIY : I ⊆ R
hIn : ¬M.IsBasis I (R ∩ M.E)
B' : Set α
hB' : M.IsBase B'
hI' : M✶.IsBasis (M.E \ (B' ∪ R ∩ M.E)) (M.E \ (R ∩ M.E))
B : Set α
hB : M.IsBase B
hIB : I ⊆ B
hBIB' : B ⊆ I ∪ B'
hss : M.E \ (B' ∪ R ∩ M.E) ⊆ M.E \ (B ∪ R ∩ M.E)
rw : ∃ (B_1 : Set α), M.IsBase B_1 ∧ Disjoint (M.E \ (B ∪ R ∩ M.E)) B_1
⊢ M✶.Indep (M.E \ (B ∪ R ∩ M.E))

Tactic:
rw [dual_indep_iff_exists]

Premises used: Matroid.dual_indep_iff_exists
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
M_1 : Matroid α
R_1 I_1 X Y : Set α
M : Matroid α
R I : Set α
hI : M.Indep I
hIY : I ⊆ R
hIn : ¬M.IsBasis I (R ∩ M.E)
B' : Set α
hB' : M.IsBase B'
hI' : M✶.IsBasis (M.E \ (B' ∪ R ∩ M.E)) (M.E \ (R ∩ M.E))
B : Set α
hB : M.IsBase B
hIB : I ⊆ B
hBIB' : B ⊆ I ∪ B'
hss : M.E \ (B' ∪ R ∩ M.E) ⊆ M.E \ (B ∪ R ∩ M.E)
⊢ ∃ (B_1 : Set α), M.IsBase B_1 ∧ Disjoint (M.E \ (B ∪ R ∩ M.E)) B_1

Tactic:
⟨B, hB, disjoint_of_subset_right subset_union_left disjoint_sdiff_left⟩

Premises used: Set.subset_union_left, Set.disjoint_sdiff_left, And.intro, Exists.intro, Set.disjoint_of_subset_right
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
M_1 : Matroid α
R_1 I_1 X Y : Set α
M : Matroid α
R I : Set α
hI : M.Indep I
hIY : I ⊆ R
hIn : ¬M.IsBasis I (R ∩ M.E)
B' : Set α
hB' : M.IsBase B'
hI' : M✶.IsBasis (M.E \ (B' ∪ R ∩ M.E)) (M.E \ (R ∩ M.E))
B : Set α
hB : M.IsBase B
hIB : I ⊆ B
hBIB' : B ⊆ I ∪ B'
hss : M.E \ (B' ∪ R ∩ M.E) ⊆ M.E \ (B ∪ R ∩ M.E)
⊢ ∃ (B_1 : Set α), M.IsBase B_1 ∧ Disjoint (M.E \ (B ∪ R ∩ M.E)) B_1

Tactic:
exact ⟨B, hB, disjoint_of_subset_right subset_union_left disjoint_sdiff_left⟩
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
M_1 : Matroid α
R_1 I_1 X Y : Set α
M : Matroid α
R I : Set α
hI : M.Indep I
hIY : I ⊆ R
hIn : ¬M.IsBasis I (R ∩ M.E)
B' : Set α
hB' : M.IsBase B'
hI' : M✶.IsBasis (M.E \ (B' ∪ R ∩ M.E)) (M.E \ (R ∩ M.E))
B : Set α
hB : M.IsBase B
hIB : I ⊆ B
hBIB' : B ⊆ I ∪ B'
hss : M.E \ (B' ∪ R ∩ M.E) ⊆ M.E \ (B ∪ R ∩ M.E)
⊢ M✶.Indep (M.E \ (B ∪ R ∩ M.E))

Tactic:
have hi : M✶.Indep (M.E \ (B ∪ (R ∩ M.E))) := by
      rw [dual_indep_iff_exists]
      exact ⟨B, hB, disjoint_of_subset_right subset_union_left disjoint_sdiff_left⟩
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
M_1 : Matroid α
R_1 I_1 X Y : Set α
M : Matroid α
R I : Set α
hI : M.Indep I
hIY : I ⊆ R
hIn : ¬M.IsBasis I (R ∩ M.E)
B' : Set α
hB' : M.IsBase B'
hI' : M✶.IsBasis (M.E \ (B' ∪ R ∩ M.E)) (M.E \ (R ∩ M.E))
B : Set α
hB : M.IsBase B
hIB : I ⊆ B
hBIB' : B ⊆ I ∪ B'
hss : M.E \ (B' ∪ R ∩ M.E) ⊆ M.E \ (B ∪ R ∩ M.E)
hi : M✶.Indep (M.E \ (B ∪ R ∩ M.E))
⊢ M.E \ (B' ∪ R ∩ M.E) = M.E \ (B ∪ R ∩ M.E)

Tactic:
have h_eq := hI'.eq_of_subset_indep hi hss
      (diff_subset_diff_right subset_union_right)
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
M_1 : Matroid α
R_1 I_1 X Y : Set α
M : Matroid α
R I : Set α
hI : M.Indep I
hIY : I ⊆ R
hIn : ¬M.IsBasis I (R ∩ M.E)
B' : Set α
hB' : M.IsBase B'
hI' : M✶.IsBasis (M.E \ (B' ∪ R ∩ M.E)) (M.E \ (R ∩ M.E))
B : Set α
hB : M.IsBase B
hIB : I ⊆ B
hBIB' : B ⊆ I ∪ B'
hss : M.E \ (B' ∪ R ∩ M.E) ⊆ M.E \ (B ∪ R ∩ M.E)
hi : M✶.Indep (M.E \ (B ∪ R ∩ M.E))
h_eq : M.E \ (B' ∪ R ∩ M.E) = M.E \ (B ∪ R ∩ M.E)
⊢ M.IsBasis (B ∩ (R ∩ M.E)) (R ∩ M.E)

Tactic:
rw [h_eq, ← diff_inter_diff, ← hB.inter_isBasis_iff_compl_inter_isBasis_dual] at hI'

Premises used: Matroid.IsBase.inter_isBasis_iff_compl_inter_isBasis_dual, Set.diff_inter_diff
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
M_1 : Matroid α
R_1 I_1 X Y : Set α
M : Matroid α
R I : Set α
hI : M.Indep I
hIY : I ⊆ R
hIn : ¬M.IsBasis I (R ∩ M.E)
B' : Set α
hB' : M.IsBase B'
hI' : M✶.IsBasis (M.E \ (B' ∪ R ∩ M.E)) (M.E \ (R ∩ M.E))
B : Set α
hB : M.IsBase B
hIB : I ⊆ B
hBIB' : B ⊆ I ∪ B'
hss : M.E \ (B' ∪ R ∩ M.E) ⊆ M.E \ (B ∪ R ∩ M.E)
hi : M✶.Indep (M.E \ (B ∪ R ∩ M.E))
h_eq : M.E \ (B' ∪ R ∩ M.E) = M.E \ (B ∪ R ∩ M.E)
hI'₁ : M.IsBasis (B ∩ (R ∩ M.E)) (R ∩ M.E)
⊢ M.IsBase B

Tactic:
rw [h_eq, ← diff_inter_diff, ← hB.inter_isBasis_iff_compl_inter_isBasis_dual] at hI'

Premises used: Matroid.IsBase.inter_isBasis_iff_compl_inter_isBasis_dual, Set.diff_inter_diff
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
M_1 : Matroid α
R_1 I_1 X Y : Set α
M : Matroid α
R I : Set α
hI : M.Indep I
hIY : I ⊆ R
hIn : ¬M.IsBasis I (R ∩ M.E)
B' : Set α
hB' : M.IsBase B'
hI' : M✶.IsBasis (M.E \ (B' ∪ R ∩ M.E)) (M.E \ (R ∩ M.E))
B : Set α
hB : M.IsBase B
hIB : I ⊆ B
hBIB' : B ⊆ I ∪ B'
hss : M.E \ (B' ∪ R ∩ M.E) ⊆ M.E \ (B ∪ R ∩ M.E)
hi : M✶.Indep (M.E \ (B ∪ R ∩ M.E))
h_eq : M.E \ (B' ∪ R ∩ M.E) = M.E \ (B ∪ R ∩ M.E)
hI'₁ : M.IsBasis (B ∩ (R ∩ M.E)) (R ∩ M.E)
hB₁ : M.IsBase B
⊢ I ⊆ B

Tactic:
rw [h_eq, ← diff_inter_diff, ← hB.inter_isBasis_iff_compl_inter_isBasis_dual] at hI'

Premises used: Matroid.IsBase.inter_isBasis_iff_compl_inter_isBasis_dual, Set.diff_inter_diff
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
M_1 : Matroid α
R_1 I_1 X Y : Set α
M : Matroid α
R I : Set α
hI : M.Indep I
hIY : I ⊆ R
hIn : ¬M.IsBasis I (R ∩ M.E)
B' : Set α
hB' : M.IsBase B'
hI' : M✶.IsBasis (M.E \ (B' ∪ R ∩ M.E)) (M.E \ (R ∩ M.E))
B : Set α
hB : M.IsBase B
hIB : I ⊆ B
hBIB' : B ⊆ I ∪ B'
hss : M.E \ (B' ∪ R ∩ M.E) ⊆ M.E \ (B ∪ R ∩ M.E)
hi : M✶.Indep (M.E \ (B ∪ R ∩ M.E))
h_eq : M.E \ (B' ∪ R ∩ M.E) = M.E \ (B ∪ R ∩ M.E)
hI'₁ : M.IsBasis (B ∩ (R ∩ M.E)) (R ∩ M.E)
hB₁ : M.IsBase B
hIB₁ : I ⊆ B
⊢ B ⊆ I ∪ B'

Tactic:
rw [h_eq, ← diff_inter_diff, ← hB.inter_isBasis_iff_compl_inter_isBasis_dual] at hI'

Premises used: Matroid.IsBase.inter_isBasis_iff_compl_inter_isBasis_dual, Set.diff_inter_diff
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
M_1 : Matroid α
R_1 I_1 X Y : Set α
M : Matroid α
R I : Set α
hI : M.Indep I
hIY : I ⊆ R
hIn : ¬M.IsBasis I (R ∩ M.E)
B' : Set α
hB' : M.IsBase B'
hI' : M✶.IsBasis (M.E \ (B' ∪ R ∩ M.E)) (M.E \ (R ∩ M.E))
B : Set α
hB : M.IsBase B
hIB : I ⊆ B
hBIB' : B ⊆ I ∪ B'
hss : M.E \ (B' ∪ R ∩ M.E) ⊆ M.E \ (B ∪ R ∩ M.E)
hi : M✶.Indep (M.E \ (B ∪ R ∩ M.E))
h_eq : M.E \ (B' ∪ R ∩ M.E) = M.E \ (B ∪ R ∩ M.E)
hI'₁ : M.IsBasis (B ∩ (R ∩ M.E)) (R ∩ M.E)
hB₁ : M.IsBase B
hIB₁ : I ⊆ B
hBIB'₁ : B ⊆ I ∪ B'
⊢ M.E \ (B' ∪ R ∩ M.E) ⊆ M.E \ (B ∪ R ∩ M.E)

Tactic:
rw [h_eq, ← diff_inter_diff, ← hB.inter_isBasis_iff_compl_inter_isBasis_dual] at hI'

Premises used: Matroid.IsBase.inter_isBasis_iff_compl_inter_isBasis_dual, Set.diff_inter_diff
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
M_1 : Matroid α
R_1 I_1 X Y : Set α
M : Matroid α
R I : Set α
hI : M.Indep I
hIY : I ⊆ R
hIn : ¬M.IsBasis I (R ∩ M.E)
B' : Set α
hB' : M.IsBase B'
hI' : M✶.IsBasis (M.E \ (B' ∪ R ∩ M.E)) (M.E \ (R ∩ M.E))
B : Set α
hB : M.IsBase B
hIB : I ⊆ B
hBIB' : B ⊆ I ∪ B'
hss : M.E \ (B' ∪ R ∩ M.E) ⊆ M.E \ (B ∪ R ∩ M.E)
hi : M✶.Indep (M.E \ (B ∪ R ∩ M.E))
h_eq : M.E \ (B' ∪ R ∩ M.E) = M.E \ (B ∪ R ∩ M.E)
hI'₁ : M.IsBasis (B ∩ (R ∩ M.E)) (R ∩ M.E)
hB₁ : M.IsBase B
hIB₁ : I ⊆ B
hBIB'₁ : B ⊆ I ∪ B'
hss₁ : M.E \ (B' ∪ R ∩ M.E) ⊆ M.E \ (B ∪ R ∩ M.E)
⊢ M✶.Indep (M.E \ (B ∪ R ∩ M.E))

Tactic:
rw [h_eq, ← diff_inter_diff, ← hB.inter_isBasis_iff_compl_inter_isBasis_dual] at hI'

Premises used: Matroid.IsBase.inter_isBasis_iff_compl_inter_isBasis_dual, Set.diff_inter_diff
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
M_1 : Matroid α
R_1 I_1 X Y : Set α
M : Matroid α
R I : Set α
hI : M.Indep I
hIY : I ⊆ R
hIn : ¬M.IsBasis I (R ∩ M.E)
B' : Set α
hB' : M.IsBase B'
hI' : M✶.IsBasis (M.E \ (B' ∪ R ∩ M.E)) (M.E \ (R ∩ M.E))
B : Set α
hB : M.IsBase B
hIB : I ⊆ B
hBIB' : B ⊆ I ∪ B'
hss : M.E \ (B' ∪ R ∩ M.E) ⊆ M.E \ (B ∪ R ∩ M.E)
hi : M✶.Indep (M.E \ (B ∪ R ∩ M.E))
h_eq : M.E \ (B' ∪ R ∩ M.E) = M.E \ (B ∪ R ∩ M.E)
hI'₁ : M.IsBasis (B ∩ (R ∩ M.E)) (R ∩ M.E)
hB₁ : M.IsBase B
hIB₁ : I ⊆ B
hBIB'₁ : B ⊆ I ∪ B'
hss₁ : M.E \ (B' ∪ R ∩ M.E) ⊆ M.E \ (B ∪ R ∩ M.E)
hi₁ : M✶.Indep (M.E \ (B ∪ R ∩ M.E))
⊢ M.E \ (B' ∪ R ∩ M.E) = M.E \ (B ∪ R ∩ M.E)

Tactic:
rw [h_eq, ← diff_inter_diff, ← hB.inter_isBasis_iff_compl_inter_isBasis_dual] at hI'

Premises used: Matroid.IsBase.inter_isBasis_iff_compl_inter_isBasis_dual, Set.diff_inter_diff
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
M_1 : Matroid α
R_1 I_1 X Y : Set α
M : Matroid α
R I : Set α
hI : M.Indep I
hIY : I ⊆ R
hIn : ¬M.IsBasis I (R ∩ M.E)
B' : Set α
hB' : M.IsBase B'
B : Set α
hI' : M.IsBasis (B ∩ (R ∩ M.E)) (R ∩ M.E)
hB : M.IsBase B
hIB : I ⊆ B
hBIB' : B ⊆ I ∪ B'
hss : M.E \ (B' ∪ R ∩ M.E) ⊆ M.E \ (B ∪ R ∩ M.E)
hi : M✶.Indep (M.E \ (B ∪ R ∩ M.E))
h_eq : M.E \ (B' ∪ R ∩ M.E) = M.E \ (B ∪ R ∩ M.E)
obtain :
  ∀ (J : Set α) (hJ : M.IsBasis J (B ∩ (R ∩ M.E))) (hIJ : I ⊆ J),
    ∃ x ∈ (B' ∩ (R ∩ M.E)) \ I, M.Indep (insert x I) ∧ insert x I ⊆ R
⊢ ∃ x ∈ (B' ∩ (R ∩ M.E)) \ I, M.Indep (insert x I) ∧ insert x I ⊆ R

Tactic:
obtain ⟨J, hJ, hIJ⟩ := hI.subset_isBasis_of_subset
      (subset_inter hIB (subset_inter hIY hI.subset_ground))

Premises used: Matroid.Indep.subset_ground, Set.subset_inter, Matroid.Indep.subset_isBasis_of_subset
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
M_1 : Matroid α
R_1 I_1 X Y : Set α
M : Matroid α
R I : Set α
hI : M.Indep I
hIY : I ⊆ R
hIn : ¬M.IsBasis I (R ∩ M.E)
B' : Set α
hB' : M.IsBase B'
B : Set α
hI' : M.IsBasis (B ∩ (R ∩ M.E)) (R ∩ M.E)
hB : M.IsBase B
hIB : I ⊆ B
hBIB' : B ⊆ I ∪ B'
hss : M.E \ (B' ∪ R ∩ M.E) ⊆ M.E \ (B ∪ R ∩ M.E)
hi : M✶.Indep (M.E \ (B ∪ R ∩ M.E))
h_eq : M.E \ (B' ∪ R ∩ M.E) = M.E \ (B ∪ R ∩ M.E)
J : Set α
hJ : M.IsBasis J (B ∩ (R ∩ M.E))
hIJ : I ⊆ J
⊢ M.IsBasis (B ∩ (R ∩ M.E)) (B ∩ (R ∩ M.E))

Tactic:
obtain rfl := hI'.indep.eq_of_isBasis hJ

Premises used: Matroid.IsBasis.indep, Matroid.Indep.eq_of_isBasis, rfl
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
M_1 : Matroid α
R_1 I_1 X Y : Set α
M : Matroid α
R I : Set α
hI : M.Indep I
hIY : I ⊆ R
hIn : ¬M.IsBasis I (R ∩ M.E)
B' : Set α
hB' : M.IsBase B'
B : Set α
hI' : M.IsBasis (B ∩ (R ∩ M.E)) (R ∩ M.E)
hB : M.IsBase B
hIB : I ⊆ B
hBIB' : B ⊆ I ∪ B'
hss : M.E \ (B' ∪ R ∩ M.E) ⊆ M.E \ (B ∪ R ∩ M.E)
hi : M✶.Indep (M.E \ (B ∪ R ∩ M.E))
h_eq : M.E \ (B' ∪ R ∩ M.E) = M.E \ (B ∪ R ∩ M.E)
J : Set α
hJ : M.IsBasis J (B ∩ (R ∩ M.E))
hIJ : I ⊆ J
hJ₁ : M.IsBasis (B ∩ (R ∩ M.E)) (B ∩ (R ∩ M.E))
⊢ I ⊆ B ∩ (R ∩ M.E)

Tactic:
obtain rfl := hI'.indep.eq_of_isBasis hJ

Premises used: Matroid.IsBasis.indep, Matroid.Indep.eq_of_isBasis, rfl
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
M_1 : Matroid α
R_1 I_1 X Y : Set α
M : Matroid α
R I : Set α
hI : M.Indep I
hIY : I ⊆ R
hIn : ¬M.IsBasis I (R ∩ M.E)
B' : Set α
hB' : M.IsBase B'
B : Set α
hI' : M.IsBasis (B ∩ (R ∩ M.E)) (R ∩ M.E)
hB : M.IsBase B
hIB : I ⊆ B
hBIB' : B ⊆ I ∪ B'
hss : M.E \ (B' ∪ R ∩ M.E) ⊆ M.E \ (B ∪ R ∩ M.E)
hi : M✶.Indep (M.E \ (B ∪ R ∩ M.E))
h_eq : M.E \ (B' ∪ R ∩ M.E) = M.E \ (B ∪ R ∩ M.E)
hJ : M.IsBasis (B ∩ (R ∩ M.E)) (B ∩ (R ∩ M.E))
hIJ : I ⊆ B ∩ (R ∩ M.E)
he : I = B ∩ (R ∩ M.E)
rwa rwa₁ rwa₂ rwa₃ : M.IsBasis (B ∩ (R ∩ M.E)) (R ∩ M.E)
⊢ M.IsBasis I (R ∩ M.E)

Tactic:
rwa [he]
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
M_1 : Matroid α
R_1 I_1 X Y : Set α
M : Matroid α
R I : Set α
hI : M.Indep I
hIY : I ⊆ R
hIn : ¬M.IsBasis I (R ∩ M.E)
B' : Set α
hB' : M.IsBase B'
B : Set α
hI' : M.IsBasis (B ∩ (R ∩ M.E)) (R ∩ M.E)
hB : M.IsBase B
hIB : I ⊆ B
hBIB' : B ⊆ I ∪ B'
hss : M.E \ (B' ∪ R ∩ M.E) ⊆ M.E \ (B ∪ R ∩ M.E)
hi : M✶.Indep (M.E \ (B ∪ R ∩ M.E))
h_eq : M.E \ (B' ∪ R ∩ M.E) = M.E \ (B ∪ R ∩ M.E)
hJ : M.IsBasis (B ∩ (R ∩ M.E)) (B ∩ (R ∩ M.E))
hIJ : I ⊆ B ∩ (R ∩ M.E)
⊢ I ⊂ B ∩ (R ∩ M.E)

Tactic:
have hIJ' : I ⊂ B ∩ (R ∩ M.E) := hIJ.ssubset_of_ne (fun he ↦ hIn (by rwa [he]))
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
M_1 : Matroid α
R_1 I_1 X Y : Set α
M : Matroid α
R I : Set α
hI : M.Indep I
hIY : I ⊆ R
hIn : ¬M.IsBasis I (R ∩ M.E)
B' : Set α
hB' : M.IsBase B'
B : Set α
hI' : M.IsBasis (B ∩ (R ∩ M.E)) (R ∩ M.E)
hB : M.IsBase B
hIB : I ⊆ B
hBIB' : B ⊆ I ∪ B'
hss : M.E \ (B' ∪ R ∩ M.E) ⊆ M.E \ (B ∪ R ∩ M.E)
hi : M✶.Indep (M.E \ (B ∪ R ∩ M.E))
h_eq : M.E \ (B' ∪ R ∩ M.E) = M.E \ (B ∪ R ∩ M.E)
hJ : M.IsBasis (B ∩ (R ∩ M.E)) (B ∩ (R ∩ M.E))
hIJ : I ⊆ B ∩ (R ∩ M.E)
hIJ' : I ⊂ B ∩ (R ∩ M.E)
obtain : ∀ (e : α) (he : e ∈ B ∩ (R ∩ M.E) ∧ e ∉ I), ∃ x ∈ (B' ∩ (R ∩ M.E)) \ I, M.Indep (insert x I) ∧ insert x I ⊆ R
⊢ ∃ x ∈ (B' ∩ (R ∩ M.E)) \ I, M.Indep (insert x I) ∧ insert x I ⊆ R

Tactic:
obtain ⟨e, he⟩ := exists_of_ssubset hIJ'

Premises used: Set.exists_of_ssubset
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
M_1 : Matroid α
R_1 I_1 X Y : Set α
M : Matroid α
R I : Set α
hI : M.Indep I
hIY : I ⊆ R
hIn : ¬M.IsBasis I (R ∩ M.E)
B' : Set α
hB' : M.IsBase B'
B : Set α
hI' : M.IsBasis (B ∩ (R ∩ M.E)) (R ∩ M.E)
hB : M.IsBase B
hIB : I ⊆ B
hBIB' : B ⊆ I ∪ B'
hss : M.E \ (B' ∪ R ∩ M.E) ⊆ M.E \ (B ∪ R ∩ M.E)
hi : M✶.Indep (M.E \ (B ∪ R ∩ M.E))
h_eq : M.E \ (B' ∪ R ∩ M.E) = M.E \ (B ∪ R ∩ M.E)
hJ : M.IsBasis (B ∩ (R ∩ M.E)) (B ∩ (R ∩ M.E))
hIJ : I ⊆ B ∩ (R ∩ M.E)
hIJ' : I ⊂ B ∩ (R ∩ M.E)
e : α
he : e ∈ B ∩ (R ∩ M.E) ∧ e ∉ I
⊢ ∃ x ∈ (B' ∩ (R ∩ M.E)) \ I, M.Indep (insert x I) ∧ insert x I ⊆ R

Tactic:
⟨e, ⟨⟨(hBIB' he.1.1).elim (fun h ↦ (he.2 h).elim) id,he.1.2⟩, he.2⟩,
      hI'.indep.subset (insert_subset he.1 hIJ), insert_subset he.1.2.1 hIY⟩

Premises used: False.elim, Matroid.Indep.subset, id, And.right, And.left, And.intro, Exists.intro, Matroid.IsBasis.indep, Or.elim, Set.insert_subset
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
M_1 : Matroid α
R_1 I_1 X Y : Set α
M : Matroid α
R I : Set α
hI : M.Indep I
hIY : I ⊆ R
hIn : ¬M.IsBasis I (R ∩ M.E)
B' : Set α
hB' : M.IsBase B'
B : Set α
hI' : M.IsBasis (B ∩ (R ∩ M.E)) (R ∩ M.E)
hB : M.IsBase B
hIB : I ⊆ B
hBIB' : B ⊆ I ∪ B'
hss : M.E \ (B' ∪ R ∩ M.E) ⊆ M.E \ (B ∪ R ∩ M.E)
hi : M✶.Indep (M.E \ (B ∪ R ∩ M.E))
h_eq : M.E \ (B' ∪ R ∩ M.E) = M.E \ (B ∪ R ∩ M.E)
hJ : M.IsBasis (B ∩ (R ∩ M.E)) (B ∩ (R ∩ M.E))
hIJ : I ⊆ B ∩ (R ∩ M.E)
hIJ' : I ⊂ B ∩ (R ∩ M.E)
e : α
he : e ∈ B ∩ (R ∩ M.E) ∧ e ∉ I
⊢ ∃ x ∈ (B' ∩ (R ∩ M.E)) \ I, M.Indep (insert x I) ∧ insert x I ⊆ R

Tactic:
exact ⟨e, ⟨⟨(hBIB' he.1.1).elim (fun h ↦ (he.2 h).elim) id,he.1.2⟩, he.2⟩,
      hI'.indep.subset (insert_subset he.1 hIJ), insert_subset he.1.2.1 hIY⟩
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
M_1 : Matroid α
R_1 I_1 X Y : Set α
M : Matroid α
R A : Set α
hAR : A ⊆ R
I : Set α
hI : M.Indep I
right : I ⊆ R
hIA : I ⊆ A
obtain :
  ∀ (J : Set α) (hJ : M.IsBasis' J A) (hIJ : I ⊆ J),
    ∃ (J : Set α), I ⊆ J ∧ Maximal (fun (K : Set α) ↦ (fun (I : Set α) ↦ M.Indep I ∧ I ⊆ R) K ∧ K ⊆ A) J
⊢ ∃ (J : Set α), I ⊆ J ∧ Maximal (fun (K : Set α) ↦ (fun (I : Set α) ↦ M.Indep I ∧ I ⊆ R) K ∧ K ⊆ A) J

Tactic:
obtain ⟨J, hJ, hIJ⟩ := hI.subset_isBasis'_of_subset hIA

Premises used: Matroid.Indep.subset_isBasis'_of_subset
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
M_1 : Matroid α
R_1 I_1 X Y : Set α
M : Matroid α
R A : Set α
hAR : A ⊆ R
I : Set α
hI : M.Indep I
right : I ⊆ R
hIA : I ⊆ A
J : Set α
hJ : M.IsBasis' J A
hIJ : I ⊆ J
h : I ⊆ J ∧ Maximal (fun (K : Set α) ↦ (fun (I : Set α) ↦ M.Indep I ∧ I ⊆ R) K ∧ K ⊆ A) J
⊢ ∃ (J : Set α), I ⊆ J ∧ Maximal (fun (K : Set α) ↦ (fun (I : Set α) ↦ M.Indep I ∧ I ⊆ R) K ∧ K ⊆ A) J

Tactic:
use J