awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
M : Matroid α
R : Set α
hR : R ⊆ M.E
⊢ (M ↾ R).E ⊆ M.E

Tactic:
hR
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
M : Matroid α
R : Set α
hR : R ⊆ M.E
⊢ (M ↾ R).E ⊆ M.E

Tactic:
exact hR
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
M N : Matroid α
h : N ≤r M
⊢ ∃ R ⊆ M.E, N = M ↾ R

Tactic:
h

Premises used: Matroid.IsRestriction
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
R R' : Set α
M : Matroid α
h : R ⊆ R'
rw : M ↾ R' ↾ R ≤r M ↾ R'
⊢ M ↾ R ≤r M ↾ R'

Tactic:
rw [← restrict_restrict_eq M h]

Premises used: Matroid.restrict_restrict_eq
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
R R' : Set α
M : Matroid α
h : R ⊆ R'
⊢ M ↾ R' ↾ R ≤r M ↾ R'

Tactic:
restrict_isRestriction _ _ h

Premises used: Matroid.restrict_isRestriction
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
R R' : Set α
M : Matroid α
h : R ⊆ R'
⊢ M ↾ R' ↾ R ≤r M ↾ R'

Tactic:
exact restrict_isRestriction _ _ h

Premises used: Matroid.restrict_isRestriction
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
M N : Matroid α
mpr : (∃ R ⊆ M.E, N = M ↾ R) → N ≤r M
⊢ N ≤r M ↔ ∃ R ⊆ M.E, N = M ↾ R

Tactic:
use IsRestriction.exists_eq_restrict

Premises used: Matroid.IsRestriction.exists_eq_restrict
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
M : Matroid α
R : Set α
hR : R ⊆ M.E
⊢ M ↾ R ≤r M

Tactic:
restrict_isRestriction M R hR

Premises used: Matroid.restrict_isRestriction
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
M : Matroid α
R : Set α
hR : R ⊆ M.E
⊢ M ↾ R ≤r M

Tactic:
exact restrict_isRestriction M R hR

Premises used: Matroid.restrict_isRestriction
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
M N : Matroid α
h : N <r M
⊢ N ≤r M

Tactic:
h.1

Premises used: And.left
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
N : Matroid α
h : N <r N
⊢ { toMatroid := N : Matroidᵣ α } < { toMatroid := N }

Tactic:
rw [← ofMatroid_lt_iff] at h

Premises used: Matroid.ofMatroid_lt_iff
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
N : Matroid α
h : { toMatroid := N : Matroidᵣ α } < { toMatroid := N }
⊢ False

Tactic:
simp at h
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
M : Matroid α
⊢ ¬M <r M

Tactic:
fun h ↦ h.ne rfl

Premises used: Matroid.IsStrictRestriction.ne, Not, rfl
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
M N : Matroid α
h : N <r M
obtain : ∀ (R : Set α) (h : M ↾ R <r M), (M ↾ R).E ⊂ M.E
⊢ N.E ⊂ M.E

Tactic:
obtain ⟨R, -, rfl⟩ := h.1

Premises used: And.left, rfl
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
M : Matroid α
R : Set α
h : M ↾ R <r M
⊢ (M ↾ R).E ⊂ M.E

Tactic:
h.isRestriction.subset.ssubset_of_ne (fun h' ↦ h.2 ⟨R, Subset.rfl, ?_⟩)

Premises used: Matroid.IsStrictRestriction.isRestriction, Set.Subset.rfl, And.right, And.intro, Matroid.IsRestriction.subset, Exists.intro, HasSubset.Subset.ssubset_of_ne
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
M : Matroid α
R : Set α
h : M ↾ R <r M
refine : ∀ (h' : (M ↾ R).E = M.E), M = M ↾ R ↾ R
⊢ (M ↾ R).E ⊂ M.E

Tactic:
refine h.isRestriction.subset.ssubset_of_ne (fun h' ↦ h.2 ⟨R, Subset.rfl, ?_⟩)

Premises used: Matroid.IsStrictRestriction.isRestriction, Set.Subset.rfl, And.right, And.intro, Matroid.IsRestriction.subset, Exists.intro, HasSubset.Subset.ssubset_of_ne
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
M : Matroid α
R : Set α
h : M ↾ R <r M
h' : (M ↾ R).E = M.E
rw : M = M ↾ M.E ↾ M.E
rw₁ : M = M ↾ M.E
rw₂ rw₃ : M = M
⊢ M = M ↾ R ↾ R

Tactic:
rw [show R = M.E from h', restrict_idem, restrict_ground_eq_self]

Premises used: Matroid.restrict_ground_eq_self, Matroid.restrict_idem
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
M N : Matroid α
h : N <r M
⊢ M ↾ N.E = N

Tactic:
h.isRestriction.eq_restrict

Premises used: Matroid.IsStrictRestriction.isRestriction, Matroid.IsRestriction.eq_restrict
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
M N : Matroid α
h : N <r M
rw rw₁ : N = N
⊢ N = M ↾ N.E

Tactic:
rw [h.eq_restrict]

Premises used: Matroid.IsStrictRestriction.eq_restrict
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
M N : Matroid α
h : N ≤r M
hne : N ≠ M
⊢ N <r M

Tactic:
⟨h, fun h' ↦ hne <| h.antisymm h'⟩

Premises used: Matroid.IsRestriction.antisymm, Matroid.IsStrictRestriction, And.intro
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
M N : Matroid α
h : N ≤r M
⊢ N = M ∨ N <r M

Tactic:
simpa using eq_or_lt_of_le (ofMatroid_le_iff.2 h)

Premises used: Iff.mpr, Matroid.ofMatroid_le_iff, eq_or_lt_of_le
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
R : Set α
M : Matroid α
hR : R ⊂ M.E
⊢ M ↾ R <r M

Tactic:
(M.restrict_isRestriction R hR.subset).isStrictRestriction_of_ne (fun h ↦ ?_)

Premises used: Matroid.restrict_isRestriction, HasSSubset.SSubset.subset, Matroid.IsRestriction.isStrictRestriction_of_ne
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
R : Set α
M : Matroid α
hR : R ⊂ M.E
refine : ∀ (h : M ↾ R = M), False
⊢ M ↾ R <r M

Tactic:
refine (M.restrict_isRestriction R hR.subset).isStrictRestriction_of_ne (fun h ↦ ?_)

Premises used: Matroid.restrict_isRestriction, HasSSubset.SSubset.subset, Matroid.IsRestriction.isStrictRestriction_of_ne
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
R : Set α
M : Matroid α
hR : R ⊂ M.E
h : M ↾ R = M
⊢ R ⊂ R

Tactic:
rw [← h, restrict_ground_eq] at hR

Premises used: Matroid.restrict_ground_eq
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
R : Set α
M : Matroid α
hR : R ⊂ M.E
h : M ↾ R = M
hR₁ : R ⊂ R
⊢ M ↾ R = M

Tactic:
rw [← h, restrict_ground_eq] at hR

Premises used: Matroid.restrict_ground_eq
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
R : Set α
M : Matroid α
hR : R ⊂ R
h : M ↾ R = M
⊢ False

Tactic:
hR.ne rfl

Premises used: HasSSubset.SSubset.ne, rfl
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
R : Set α
M : Matroid α
hR : R ⊂ R
h : M ↾ R = M
⊢ False

Tactic:
exact hR.ne rfl

Premises used: HasSSubset.SSubset.ne, rfl
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
M N : Matroid α
h : N ≤r M
hne : N.E ≠ M.E
rw : M ↾ N.E <r M
⊢ N <r M

Tactic:
rw [← h.eq_restrict]

Premises used: Matroid.IsRestriction.eq_restrict
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
M N : Matroid α
h : N ≤r M
hne : N.E ≠ M.E
⊢ M ↾ N.E <r M

Tactic:
restrict_isStrictRestriction (h.subset.ssubset_of_ne hne)

Premises used: Matroid.restrict_isStrictRestriction, Matroid.IsRestriction.subset, HasSubset.Subset.ssubset_of_ne
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
M N : Matroid α
h : N ≤r M
hne : N.E ≠ M.E
⊢ M ↾ N.E <r M

Tactic:
exact restrict_isStrictRestriction (h.subset.ssubset_of_ne hne)

Premises used: Matroid.restrict_isStrictRestriction, Matroid.IsRestriction.subset, HasSubset.Subset.ssubset_of_ne
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
R R' : Set α
M : Matroid α
h : R ⊂ R'
⊢ M ↾ R <r M ↾ R'

Tactic:
(IsRestriction.of_subset M h.subset).isStrictRestriction_of_ground_ne h.ne

Premises used: Matroid.IsRestriction.of_subset, Matroid.IsRestriction.isStrictRestriction_of_ground_ne, HasSSubset.SSubset.subset, HasSSubset.SSubset.ne
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
N M : Matroid α
inst : M.Finite
h : N ≤r M
obtain : ∀ (R : Set α) (hR : R ⊆ M.E), (M ↾ R).Finite
⊢ N.Finite

Tactic:
obtain ⟨R, hR, rfl⟩ := h

Premises used: rfl
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
M : Matroid α
inst : M.Finite
R : Set α
hR : R ⊆ M.E
⊢ (M ↾ R).Finite

Tactic:
restrict_finite <| M.ground_finite.subset hR

Premises used: Set.Finite.subset, Matroid.restrict_finite, Matroid.ground_finite
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
M : Matroid α
inst : M.Finite
R : Set α
hR : R ⊆ M.E
⊢ (M ↾ R).Finite

Tactic:
exact restrict_finite <| M.ground_finite.subset hR

Premises used: Set.Finite.subset, Matroid.restrict_finite, Matroid.ground_finite
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
N M : Matroid α
inst : M.RankFinite
h : N ≤r M
obtain : ∀ (R : Set α), (M ↾ R).RankFinite
⊢ N.RankFinite

Tactic:
obtain ⟨R, -, rfl⟩ := h

Premises used: rfl
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
M : Matroid α
inst : M.RankFinite
R : Set α
⊢ (M ↾ R).RankFinite

Tactic:
infer_instance
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
N M : Matroid α
inst : M.Finitary
h : N ≤r M
obtain : ∀ (R : Set α), (M ↾ R).Finitary
⊢ N.Finitary

Tactic:
obtain ⟨R, -, rfl⟩ := h

Premises used: rfl
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
M : Matroid α
inst : M.Finitary
R : Set α
⊢ (M ↾ R).Finitary

Tactic:
infer_instance
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
M : Matroid α
inst : M.Finite
R : Set α
hR : R ⊆ M.E
⊢ Membership.mem (γ := Set (Matroid α)) ((fun (R : Set α) ↦ M ↾ R) '' {b : Set α | b ⊆ M.E}) (M ↾ R)

Tactic:
⟨_, hR, rfl⟩

Premises used: Set.Mem, setOf, And.intro, Exists.intro, Set.image, rfl
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
M : Matroid α
inst : M.Finite
R : Set α
hR : R ⊆ M.E
⊢ Membership.mem (γ := Set (Matroid α)) ((fun (R : Set α) ↦ M ↾ R) '' {b : Set α | b ⊆ M.E}) (M ↾ R)

Tactic:
exact ⟨_, hR, rfl⟩
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
M : Matroid α
I : Set α
N : Matroid α
hI : N.Indep I
hNM : N ≤r M
obtain : ∀ (R : Set α) (hI : (M ↾ R).Indep I), M.Indep I
⊢ M.Indep I

Tactic:
obtain ⟨R, -, rfl⟩ := hNM

Premises used: rfl
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
M : Matroid α
I R : Set α
hI : (M ↾ R).Indep I
⊢ M.Indep I

Tactic:
hI.of_restrict

Premises used: Matroid.Indep.of_restrict
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
M : Matroid α
I R : Set α
hI : (M ↾ R).Indep I
⊢ M.Indep I

Tactic:
exact hI.of_restrict

Premises used: Matroid.Indep.of_restrict
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
M : Matroid α
I : Set α
N : Matroid α
hI : M.Indep I
hNM : N ≤r M
hIN : I ⊆ N.E
obtain : ∀ (R : Set α) (hIN : I ⊆ (M ↾ R).E), (M ↾ R).Indep I
⊢ N.Indep I

Tactic:
obtain ⟨R, -, rfl⟩ := hNM

Premises used: rfl
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
M : Matroid α
I : Set α
hI : M.Indep I
R : Set α
hIN : I ⊆ (M ↾ R).E
⊢ (M ↾ R).Indep I

Tactic:
simpa [hI]
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
M : Matroid α
I : Set α
N : Matroid α
hMN : N ≤r M
⊢ N.Indep I ↔ M.Indep I ∧ I ⊆ N.E

Tactic:
⟨fun h ↦ ⟨h.of_isRestriction hMN, h.subset_ground⟩, fun h ↦ h.1.indep_isRestriction hMN h.2⟩

Premises used: Matroid.Indep.indep_isRestriction, Matroid.Indep.subset_ground, And.right, And.left, Matroid.Indep.of_isRestriction, And.intro, Iff.intro
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
M : Matroid α
I X : Set α
N : Matroid α
hI : M.IsBasis I X
hNM : N ≤r M
hX : X ⊆ N.E
obtain : ∀ (R : Set α) (hR : R ⊆ M.E) (hX : X ⊆ (M ↾ R).E), (M ↾ R).IsBasis I X
⊢ N.IsBasis I X

Tactic:
obtain ⟨R, hR, rfl⟩ := hNM

Premises used: rfl
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
M : Matroid α
I X : Set α
hI : M.IsBasis I X
R : Set α
hR : R ⊆ M.E
hX : X ⊆ (M ↾ R).E
rwa : M.IsBasis I X ∧ X ⊆ R
rwa₁ rwa₂ rwa₃ rwa₄ : M.IsBasis I X
⊢ (M ↾ R).IsBasis I X

Tactic:
rwa [isBasis_restrict_iff, and_iff_left (show X ⊆ R from hX)]

Premises used: Matroid.isBasis_restrict_iff, and_iff_left
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
M : Matroid α
I X : Set α
N : Matroid α
hI : N.IsBasis I X
hNM : N ≤r M
obtain : ∀ (R : Set α) (hR : R ⊆ M.E) (hI : (M ↾ R).IsBasis I X), M.IsBasis I X
⊢ M.IsBasis I X

Tactic:
obtain ⟨R, hR, rfl⟩ := hNM

Premises used: rfl
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
M : Matroid α
I X R : Set α
hR : R ⊆ M.E
hI : (M ↾ R).IsBasis I X
⊢ M.IsBasis I X

Tactic:
((isBasis_restrict_iff hR).1 hI).1

Premises used: Matroid.isBasis_restrict_iff, And.left, Iff.mp
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
M : Matroid α
I X R : Set α
hR : R ⊆ M.E
hI : (M ↾ R).IsBasis I X
⊢ M.IsBasis I X

Tactic:
exact ((isBasis_restrict_iff hR).1 hI).1

Premises used: Matroid.isBasis_restrict_iff, And.left, Iff.mp
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
M : Matroid α
I : Set α
N : Matroid α
hI : N.IsBase I
hNM : N ≤r M
obtain : ∀ (R : Set α) (hR : R ⊆ M.E) (hI : (M ↾ R).IsBase I), M.IsBasis I (M ↾ R).E
⊢ M.IsBasis I N.E

Tactic:
obtain ⟨R, hR, rfl⟩ := hNM

Premises used: rfl
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
M : Matroid α
I R : Set α
hR : R ⊆ M.E
hI : (M ↾ R).IsBase I
rwa rwa₁ rwa₂ rwa₃ : ∀ (hI : M.IsBasis I R), M.IsBasis I (M ↾ R).E
⊢ M.IsBasis I (M ↾ R).E

Tactic:
rwa [isBase_restrict_iff] at hI

Premises used: Matroid.isBase_restrict_iff
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
M N : Matroid α
hMN : N ≤r M
B : Set α
h : M.IsBasis B N.E
⊢ N.IsBase B

Tactic:
simpa [hMN.eq_restrict] using h.restrict_isBase

Premises used: Matroid.IsBasis.restrict_isBase, Matroid.IsRestriction.eq_restrict
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
M : Matroid α
I X : Set α
N : Matroid α
hMN : N ≤r M
⊢ N.IsBasis I X ↔ M.IsBasis I X ∧ X ⊆ N.E

Tactic:
⟨fun h ↦ ⟨h.of_isRestriction hMN, h.subset_ground⟩, fun h ↦ h.1.isBasis_isRestriction hMN h.2⟩

Premises used: Matroid.IsBasis.subset_ground, Matroid.IsBasis.isBasis_isRestriction, And.right, And.left, And.intro, Iff.intro, Matroid.IsBasis.of_isRestriction
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
M : Matroid α
X : Set α
N : Matroid α
hX : N.Dep X
hNM : N ≤r M
obtain : ∀ (R : Set α) (hR : R ⊆ M.E) (hX : (M ↾ R).Dep X), M.Dep X
⊢ M.Dep X

Tactic:
obtain ⟨R, hR, rfl⟩ := hNM

Premises used: rfl
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
M : Matroid α
X R : Set α
hR : R ⊆ M.E
hX : (M ↾ R).Dep X
⊢ ¬M.Indep X ∧ X ⊆ R

Tactic:
rw [restrict_dep_iff] at hX

Premises used: Matroid.restrict_dep_iff
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
M : Matroid α
X R : Set α
hR : R ⊆ M.E
hX : ¬M.Indep X ∧ X ⊆ R
⊢ M.Dep X

Tactic:
⟨hX.1, hX.2.trans hR⟩

Premises used: Matroid.Dep, HasSubset.Subset.trans, And.right, And.left, And.intro
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
M : Matroid α
X R : Set α
hR : R ⊆ M.E
hX : ¬M.Indep X ∧ X ⊆ R
⊢ M.Dep X

Tactic:
exact ⟨hX.1, hX.2.trans hR⟩
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
M : Matroid α
X : Set α
N : Matroid α
hX : M.Dep X
hNM : N ≤r M
hXE : X ⊆ N.E
obtain : ∀ (R : Set α) (hXE : X ⊆ (M ↾ R).E), (M ↾ R).Dep X
⊢ N.Dep X

Tactic:
obtain ⟨R, -, rfl⟩ := hNM

Premises used: rfl
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
M : Matroid α
X : Set α
hX : M.Dep X
R : Set α
hXE : X ⊆ (M ↾ R).E
⊢ (M ↾ R).Dep X

Tactic:
simpa [hX.not_indep]

Premises used: Matroid.Dep.not_indep
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
M : Matroid α
X : Set α
N : Matroid α
hMN : N ≤r M
⊢ N.Dep X ↔ M.Dep X ∧ X ⊆ N.E

Tactic:
⟨fun h ↦ ⟨h.of_isRestriction hMN, h.subset_ground⟩, fun h ↦ h.1.dep_isRestriction hMN h.2⟩

Premises used: Matroid.Dep.subset_ground, Matroid.Dep.dep_isRestriction, Matroid.Dep.of_isRestriction, And.right, And.left, And.intro, Iff.intro
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
M : Matroid α
I X Y J : Set α
hIX : M.IsBasis I X
hJX : M.IsBasis J X
hXY : X ⊆ Y
hJY : M.IsBasis J Y
rw : (M ↾ Y).IsBase I
⊢ M.IsBasis I Y

Tactic:
rw [← isBase_restrict_iff]

Premises used: Matroid.isBase_restrict_iff
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
M : Matroid α
I X Y J : Set α
hIX : M.IsBasis I X
hJX : M.IsBasis J X
hXY : X ⊆ Y
hJY : M.IsBasis J Y
⊢ (M ↾ Y).IsBase J

Tactic:
rw [← isBase_restrict_iff] at hJY

Premises used: Matroid.isBase_restrict_iff
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
M : Matroid α
I X Y J : Set α
hIX : M.IsBasis I X
hJX : M.IsBasis J X
hXY : X ⊆ Y
hJY : (M ↾ Y).IsBase J
⊢ (M ↾ Y).IsBase I

Tactic:
hJY.isBase_of_isBasis_superset hJX.subset (hIX.isBasis_restrict_of_subset hXY)

Premises used: Matroid.IsBase.isBase_of_isBasis_superset, Matroid.IsBasis.subset, Matroid.IsBasis.isBasis_restrict_of_subset
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
M : Matroid α
I X Y J : Set α
hIX : M.IsBasis I X
hJX : M.IsBasis J X
hXY : X ⊆ Y
hJY : (M ↾ Y).IsBase J
⊢ (M ↾ Y).IsBase I

Tactic:
exact hJY.isBase_of_isBasis_superset hJX.subset (hIX.isBasis_restrict_of_subset hXY)

Premises used: Matroid.IsBase.isBase_of_isBasis_superset, Matroid.IsBasis.subset, Matroid.IsBasis.isBasis_restrict_of_subset
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
M : Matroid α
I X Y J : Set α
hI : M.IsBasis I X
hJ : M.IsBasis J Y
hJX : J ⊆ X
hIY : I ⊆ Y
⊢ M.IsBasis I (X ∩ Y)

Tactic:
have hI' := hI.isBasis_subset (subset_inter hI.subset hIY) inter_subset_left
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
M : Matroid α
I X Y J : Set α
hI : M.IsBasis I X
hJ : M.IsBasis J Y
hJX : J ⊆ X
hIY : I ⊆ Y
hI' : M.IsBasis I (X ∩ Y)
⊢ M.IsBasis J (X ∩ Y)

Tactic:
have hJ' := hJ.isBasis_subset (subset_inter hJX hJ.subset) inter_subset_right
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
M : Matroid α
I X Y J : Set α
hI : M.IsBasis I X
hJ : M.IsBasis J Y
hJX : J ⊆ X
hIY : I ⊆ Y
hI' : M.IsBasis I (X ∩ Y)
hJ' : M.IsBasis J (X ∩ Y)
⊢ M.IsBasis I Y

Tactic:
hI'.transfer hJ' inter_subset_right hJ

Premises used: Matroid.IsBasis.transfer, Set.inter_subset_right
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
M : Matroid α
I X Y J : Set α
hI : M.IsBasis I X
hJ : M.IsBasis J Y
hJX : J ⊆ X
hIY : I ⊆ Y
hI' : M.IsBasis I (X ∩ Y)
hJ' : M.IsBasis J (X ∩ Y)
⊢ M.IsBasis I Y

Tactic:
exact hI'.transfer hJ' inter_subset_right hJ

Premises used: Matroid.IsBasis.transfer, Set.inter_subset_right
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
M : Matroid α
I X J : Set α
hI : M.Indep I
hIX : I ⊆ X
hJ : M.IsBasis J X
obtain :
  ∀ (I' : Set α) (hI' : (M ↾ X).IsBase I') (hII' : I ⊆ I') (hI'IJ : I' ⊆ I ∪ J),
    ∃ (I' : Set α), M.IsBasis I' X ∧ I ⊆ I' ∧ I' ⊆ I ∪ J
⊢ ∃ (I' : Set α), M.IsBasis I' X ∧ I ⊆ I' ∧ I' ⊆ I ∪ J

Tactic:
obtain ⟨I', hI', hII', hI'IJ⟩ :=
    (hI.indep_restrict_of_subset hIX).exists_isBase_subset_union_isBase (IsBasis.isBase_restrict hJ)

Premises used: Matroid.IsBasis.isBase_restrict, Matroid.Indep.indep_restrict_of_subset, Matroid.Indep.exists_isBase_subset_union_isBase
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
M : Matroid α
I X J : Set α
hI : M.Indep I
hIX : I ⊆ X
hJ : M.IsBasis J X
I' : Set α
hI' : (M ↾ X).IsBase I'
hII' : I ⊆ I'
hI'IJ : I' ⊆ I ∪ J
⊢ M.IsBasis I' X

Tactic:
rw [isBase_restrict_iff] at hI'

Premises used: Matroid.isBase_restrict_iff
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
M : Matroid α
I X J : Set α
hI : M.Indep I
hIX : I ⊆ X
hJ : M.IsBasis J X
I' : Set α
hI' : (M ↾ X).IsBase I'
hII' : I ⊆ I'
hI'IJ : I' ⊆ I ∪ J
hI'₁ : M.IsBasis I' X
⊢ I ⊆ I'

Tactic:
rw [isBase_restrict_iff] at hI'

Premises used: Matroid.isBase_restrict_iff
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
M : Matroid α
I X J : Set α
hI : M.Indep I
hIX : I ⊆ X
hJ : M.IsBasis J X
I' : Set α
hI' : (M ↾ X).IsBase I'
hII' : I ⊆ I'
hI'IJ : I' ⊆ I ∪ J
hI'₁ : M.IsBasis I' X
hII'₁ : I ⊆ I'
⊢ I' ⊆ I ∪ J

Tactic:
rw [isBase_restrict_iff] at hI'

Premises used: Matroid.isBase_restrict_iff
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
M : Matroid α
I X J : Set α
hI : M.Indep I
hIX : I ⊆ X
hJ : M.IsBasis J X
I' : Set α
hI' : M.IsBasis I' X
hII' : I ⊆ I'
hI'IJ : I' ⊆ I ∪ J
⊢ ∃ (I' : Set α), M.IsBasis I' X ∧ I ⊆ I' ∧ I' ⊆ I ∪ J

Tactic:
⟨I', hI', hII', hI'IJ⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
M : Matroid α
I X J : Set α
hI : M.Indep I
hIX : I ⊆ X
hJ : M.IsBasis J X
I' : Set α
hI' : M.IsBasis I' X
hII' : I ⊆ I'
hI'IJ : I' ⊆ I ∪ J
⊢ ∃ (I' : Set α), M.IsBasis I' X ∧ I ⊆ I' ∧ I' ⊆ I ∪ J

Tactic:
exact ⟨I', hI', hII', hI'IJ⟩
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
M : Matroid α
I X J : Set α
hI : M.Indep I
hIX : I ⊆ X
hI' : ¬M.IsBasis I X
hJ : M.IsBasis J X
⊢ ¬(M ↾ X).IsBase I

Tactic:
rw [← isBase_restrict_iff] at hI'

Premises used: Matroid.isBase_restrict_iff
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
M : Matroid α
I X J : Set α
hI : M.Indep I
hIX : I ⊆ X
hI' : ¬M.IsBasis I X
hJ : M.IsBasis J X
hI'₁ : ¬(M ↾ X).IsBase I
⊢ M.IsBasis J X

Tactic:
rw [← isBase_restrict_iff] at hI'

Premises used: Matroid.isBase_restrict_iff
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
M : Matroid α
I X J : Set α
hI : M.Indep I
hIX : I ⊆ X
hI' : ¬(M ↾ X).IsBase I
hJ : M.IsBasis J X
⊢ (M ↾ X).IsBase J

Tactic:
rw [← isBase_restrict_iff] at hJ

Premises used: Matroid.isBase_restrict_iff
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
M : Matroid α
I X J : Set α
hI : M.Indep I
hIX : I ⊆ X
hI' : ¬(M ↾ X).IsBase I
hJ : (M ↾ X).IsBase J
obtain : ∀ (e : α) (he : e ∈ J \ I) (hi : (M ↾ X).Indep (insert e I)), ∃ e ∈ J \ I, M.Indep (insert e I)
⊢ ∃ e ∈ J \ I, M.Indep (insert e I)

Tactic:
obtain ⟨e, he, hi⟩ := (hI.indep_restrict_of_subset hIX).exists_insert_of_not_isBase hI' hJ

Premises used: Matroid.Indep.exists_insert_of_not_isBase, Matroid.Indep.indep_restrict_of_subset
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
M : Matroid α
I X J : Set α
hI : M.Indep I
hIX : I ⊆ X
hI' : ¬(M ↾ X).IsBase I
hJ : (M ↾ X).IsBase J
e : α
he : e ∈ J \ I
hi : (M ↾ X).Indep (insert e I)
⊢ ∃ e ∈ J \ I, M.Indep (insert e I)

Tactic:
⟨e, he, (restrict_indep_iff.mp hi).1⟩

Premises used: And.left, And.intro, Exists.intro, Iff.mp, Matroid.restrict_indep_iff
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
M : Matroid α
I X J : Set α
hI : M.Indep I
hIX : I ⊆ X
hI' : ¬(M ↾ X).IsBase I
hJ : (M ↾ X).IsBase J
e : α
he : e ∈ J \ I
hi : (M ↾ X).Indep (insert e I)
⊢ ∃ e ∈ J \ I, M.Indep (insert e I)

Tactic:
exact ⟨e, he, (restrict_indep_iff.mp hi).1⟩
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
M : Matroid α
I X B : Set α
hIX : M.IsBasis I X
hB : M.IsBase B
hBX : B ⊆ X
⊢ M.IsBase I

Tactic:
hB.isBase_of_isBasis_superset hBX hIX

Premises used: Matroid.IsBase.isBase_of_isBasis_superset
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
M : Matroid α
I X J : Set α
e : α
hIX : M.IsBasis I X
hJX : M.IsBasis J X
he : e ∈ I \ J
obtain :
  ∀ (y : α) (hy : y ∈ J \ I) (h : (M ↾ X).IsBase (insert y (I \ {e}))), ∃ f ∈ J \ I, M.IsBasis (insert f (I \ {e})) X
⊢ ∃ f ∈ J \ I, M.IsBasis (insert f (I \ {e})) X

Tactic:
obtain ⟨y, hy, h⟩ := hIX.restrict_isBase.exchange hJX.restrict_isBase he

Premises used: Matroid.IsBase.exchange, Matroid.IsBasis.restrict_isBase
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
M : Matroid α
I X J : Set α
e : α
hIX : M.IsBasis I X
hJX : M.IsBasis J X
he : e ∈ I \ J
y : α
hy : y ∈ J \ I
h : (M ↾ X).IsBase (insert y (I \ {e}))
rwa rwa₁ rwa₂ rwa₃ : ∀ (h : M.IsBasis (insert y (I \ {e})) X), M.IsBasis (insert y (I \ {e})) X
⊢ M.IsBasis (insert y (I \ {e})) X

Tactic:
rwa [isBase_restrict_iff] at h

Premises used: Matroid.isBase_restrict_iff