mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Combinatorics.Matroid.Minor.Restrict

Goal state before:
pp: α : Type u_1
M✝ : Matroid α
R✝ I✝ 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)
⊢ M.IsBasis I (R ∩ M.E)

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Matroid.IndepAxioms

Goal state before:
pp: α : Type u_1
E : Set α
Indep : Set α → Prop
indep_empty : Indep ∅
indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I
indep_aug :
  ∀ ⦃I J : Set α⦄, Indep I → I.Finite → Indep J → J.Finite → I.ncard < J.ncard → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)
indep_compact : ∀ (I : Set α), (∀ J ⊆ I, J.Finite → Indep J) → Indep I
subset_ground : ∀ (I : Set α), Indep I → I ⊆ E
htofin : ∀ (I : Set α) (e : α), Indep I → ¬Indep (insert e I) → ∃ I₀ ⊆ I, I₀.Finite ∧ ¬Indep (insert e I₀)
I B : Set α
hI : Indep I
hImax : ¬Maximal Indep I
hBmax : Maximal Indep B
e : α
heI : e ∉ I
hins : Indep (insert e I)
heB : e ∉ B
hcon : ∀ x ∈ B \ I, ¬Indep (insert x I)
heBdep : ¬Indep (insert e B)
B₀ : Set α
hB₀B : B₀ ⊆ B
hB₀fin : B₀.Finite
hB₀e : ¬Indep (insert e B₀)
hB₀ : Indep B₀
I₀ : Set α
hI₀I : I₀ ⊆ I
hI₀fin : I₀.Finite
hI₀ : ∀ x ∈ B₀ \ I₀, ¬Indep (insert x I₀)
E₀ : Set α := insert e (I₀ ∪ B₀)
hE₀fin : E₀.Finite
J : Set α
hJmax : ∀ ⦃j : Set α⦄, (fun x ↦ x ∈ {J | B₀ ⊆ J ∧ Indep J ∧ J ⊆ E₀}) j → id J ⊆ id j → id j ⊆ id J
hB₀J : B₀ ⊆ J
hJ : Indep J
hJss : J ⊆ E₀
heI₀ : e ∉ I₀
heI₀i : Indep (insert e I₀)
heJ : e ∉ J
hJfin : J.Finite
⊢ (insert e I₀).ncard ≤ J.ncard

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Constructions

Goal state before:
pp: α✝ : Type u_1
M : Matroid α✝
E B I X R J : Set α✝
α : Type u_2
⊢ ∀ ⦃I : Set α⦄, I = ∅ ↔ ∃ B, B = ∅ ∧ I ⊆ B

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Constructions

Goal state before:
pp: α✝ : Type u_1
M : Matroid α✝
E B I X R J : Set α✝
α : Type u_2
⊢ ExchangeProperty fun x ↦ x = ∅

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Constructions

Goal state before:
pp: α✝ : Type u_1
M : Matroid α✝
E B I X R J : Set α✝
α : Type u_2
X✝ : Set α
a✝ : X✝ ⊆ ∅
⊢ ∅ ⊆ ∅ ∧ Maximal (fun K ↦ (fun x ↦ x = ∅) K ∧ K ⊆ X✝) ∅

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Constructions

Goal state before:
pp: α✝ : Type u_1
M : Matroid α✝
E B I X R J : Set α✝
α : Type u_2
⊢ ∀ X ⊆ ∅, ExistsMaximalSubsetProperty (fun x ↦ x = ∅) X

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Constructions

Goal state before:
pp: α✝ : Type u_1
M : Matroid α✝
E B I X R J : Set α✝
α : Type u_2
⊢ ∀ (B : Set α), B = ∅ → B ⊆ ∅

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Constructions

Goal state before:
pp: α : Type u_1
M : Matroid α
h : M.E = ∅
⊢ ∀ ⦃I : Set α⦄, I ⊆ M.E → (M.Indep I ↔ I = ∅)

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Constructions

Goal state before:
pp: α : Type u_1
M : Matroid α
⊢ M.E = ∅ ↔ M = emptyOn α

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Constructions

Goal state before:
pp: α : Type u_1
⊢ (emptyOn α)✶ = emptyOn α

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Constructions

Goal state before:
pp: α : Type u_1
M : Matroid α
⊢ M ↾ ∅ = emptyOn α

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Constructions

Goal state before:
pp: α : Type u_1
M : Matroid α
⊢ M = emptyOn α ∨ M.Nonempty

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Constructions

Goal state before:
pp: α : Type u_1
inst✝ : IsEmpty α
M : Matroid α
⊢ M = emptyOn α

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Constructions

Goal state before:
pp: α : Type u_2
⊢ loopyOn ∅ = emptyOn α

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Constructions

Goal state before:
pp: α : Type u_1
E I : Set α
⊢ (loopyOn E).Indep I ↔ I = ∅

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Minor.Restrict

Goal state before:
pp: α : Type u_1
M✝ : Matroid α
R✝ I X Y : Set α
M : Matroid α
R : Set α
⊢ ∀ ⦃I B : Set α⦄,
    M.Indep I ∧ I ⊆ R →
      ¬Maximal (fun I ↦ M.Indep I ∧ I ⊆ R) I →
        Maximal (fun I ↦ M.Indep I ∧ I ⊆ R) B → ∃ x ∈ B \ I, M.Indep (insert x I) ∧ insert x I ⊆ R

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Constructions

Goal state before:
pp: α : Type u_1
M : Matroid α
h : ∀ X ⊆ M.E, M.Indep X → X = ∅
I : Set α
hIE : I ⊆ M.E
⊢ I = ∅ → M.Indep I

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Constructions

Goal state before:
pp: α : Type u_1
M : Matroid α
E : Set α
⊢ M = loopyOn E ↔ M.E = E ∧ ∀ X ⊆ M.E, M.Indep X → X = ∅

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Constructions

Goal state before:
pp: α : Type u_1
E B : Set α
⊢ (loopyOn E).IsBase B ↔ B = ∅

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Minor.Restrict

Goal state before:
pp: α : Type u_1
M✝ : Matroid α
R✝ I X Y : Set α
M : Matroid α
R : Set α
⊢ ∀ X ⊆ R, ExistsMaximalSubsetProperty (fun I ↦ M.Indep I ∧ I ⊆ R) X

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Constructions

Goal state before:
pp: α : Type u_1
E I X : Set α
⊢ I = ∅ ∧ X ⊆ E → (loopyOn E).IsBasis I X

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Constructions

Goal state before:
pp: α : Type u_1
M : Matroid α
E B I X R J : Set α
⊢ (loopyOn E).IsBase ∅ ∧ ∅.Finite

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Minor.Restrict

Goal state before:
pp: α : Type u_1
M : Matroid α
R X : Set α
⊢ (M ↾ R).Dep X ↔ ¬M.Indep X ∧ X ⊆ R

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Constructions

Goal state before:
pp: α : Type u_1
E R : Set α
⊢ loopyOn E ↾ R = loopyOn R

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Minor.Restrict

Goal state before:
pp: α : Type u_1
M : Matroid α
⊢ M ↾ M.E = M

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Constructions

Goal state before:
pp: α : Type u_1
M : Matroid α
h : ∀ ⦃y : Set α⦄, M.Indep y → y = ∅
I : Set α
x✝ : I ⊆ M.E
hI : I = ∅
⊢ M.Indep I

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Constructions

Goal state before:
pp: α : Type u_1
M : Matroid α
⊢ M.IsBase ∅ ↔ M = loopyOn M.E

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Minor.Restrict

Goal state before:
pp: α : Type u_1
R₁ R₂ : Set α
M : Matroid α
hR : R₂ ⊆ R₁
⊢ M ↾ R₁ ↾ R₂ = M ↾ R₂

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Constructions

Goal state before:
pp: α : Type u_1
M : Matroid α
⊢ M = loopyOn M.E ∨ M.RankPos

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Minor.Restrict

Goal state before:
pp: α : Type u_1
M : Matroid α
R : Set α
⊢ M ↾ R ↾ R = M ↾ R

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Constructions

Goal state before:
pp: α : Type u_1
M : Matroid α
⊢ ¬M.RankPos ↔ M = loopyOn M.E

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Constructions

Goal state before:
pp: α : Type u_1
E : Set α
⊢ (freeOn E)✶ = loopyOn E

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Constructions

Goal state before:
pp: α : Type u_2
⊢ freeOn ∅ = emptyOn α

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Constructions

Goal state before:
pp: α : Type u_1
E B : Set α
⊢ (freeOn E).IsBase B ↔ B = E

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Constructions

Goal state before:
pp: α : Type u_1
E I : Set α
⊢ (freeOn E).Indep I ↔ I ⊆ E

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Minor.Restrict

Goal state before:
pp: α : Type u_1
M : Matroid α
I X : Set α
hX : X ⊆ M.E
⊢ (M ↾ X).IsBase I ↔ M.IsBasis I X

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Minor.Restrict

Goal state before:
pp: α : Type u_1
M : Matroid α
I X : Set α
⊢ (M ↾ X).IsBase I ↔ M.IsBasis' I X

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Constructions

Goal state before:
pp: α : Type u_1
E I X : Set α
⊢ (freeOn E).IsBasis I X ↔ I = X ∧ X ⊆ E

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Dual

Goal state before:
pp: α : Type u_1
M✝ : Matroid α
I B✝ X✝ : 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:
by

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Minor.Restrict

Goal state before:
pp: α : Type u_1
M : Matroid α
R✝ I✝ X Y : Set α
inst✝ : M.Finitary
R I : Set α
hI : ∀ J ⊆ I, J.Finite → M.Indep J ∧ J ⊆ R
e : α
heI : e ∈ I
⊢ {e} ⊆ I

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Minor.Restrict

Goal state before:
pp: α : Type u_1
M : Matroid α
R✝ I X Y : Set α
inst✝ : M.Finitary
R : Set α
⊢ (M ↾ R).Finitary

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Minor.Restrict

Goal state before:
pp: α : Type u_1
M : Matroid α
I X Y : Set α
hI : M.IsBasis I X
hXY : X ⊆ Y
⊢ (M ↾ Y).IsBasis I X

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Constructions

Goal state before:
pp: α : Type u_1
E I X : Set α
⊢ (freeOn E).IsBasis' I X ↔ I = X ∩ E

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Constructions

Goal state before:
pp: α : Type u_1
M : Matroid α
E : Set α
⊢ M = freeOn E ↔ M.E = E ∧ M.Indep E

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Constructions

Goal state before:
pp: α : Type u_1
M : Matroid α
⊢ M.Indep M.E ↔ M = freeOn M.E

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Constructions

Goal state before:
pp: α : Type u_1
E R : Set α
h : R ⊆ E
⊢ freeOn E ↾ R = freeOn R

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Constructions

Goal state before:
pp: α : Type u_1
M : Matroid α
I : Set α
⊢ M ↾ I = freeOn I ↔ M.Indep I

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Constructions

Goal state before:
pp: α : Type u_1
M : Matroid α
I : Set α
hI : M.Indep I
⊢ M ↾ I = freeOn I

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Constructions

Goal state before:
pp: α : Type u_1
M : Matroid α
E B I✝ X R J I : Set α
h : ∀ J ⊆ I, J.Finite → J ⊆ E
e : α
heI : e ∈ I
⊢ {e} ⊆ I

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Matroid.IndepAxioms

Goal state before:
pp: α : Type u_1
E : Set α
Indep : Set α → Prop
indep_empty : Indep ∅
indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I
indep_aug :
  ∀ ⦃I J : Set α⦄, Indep I → I.Finite → Indep J → J.Finite → I.ncard < J.ncard → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)
indep_compact : ∀ (I : Set α), (∀ J ⊆ I, J.Finite → Indep J) → Indep I
subset_ground : ∀ (I : Set α), Indep I → I ⊆ E
htofin : ∀ (I : Set α) (e : α), Indep I → ¬Indep (insert e I) → ∃ I₀ ⊆ I, I₀.Finite ∧ ¬Indep (insert e I₀)
I B : Set α
hI : Indep I
hImax : ¬Maximal Indep I
hBmax : Maximal Indep B
e : α
heI : e ∉ I
hins : Indep (insert e I)
heB : e ∉ B
hcon : ∀ x ∈ B \ I, ¬Indep (insert x I)
heBdep : ¬Indep (insert e B)
B₀ : Set α
hB₀B : B₀ ⊆ B
hB₀fin : B₀.Finite
hB₀e : ¬Indep (insert e B₀)
hB₀ : Indep B₀
I₀ : Set α
hI₀I : I₀ ⊆ I
hI₀fin : I₀.Finite
hI₀ : ∀ x ∈ B₀ \ I₀, ¬Indep (insert x I₀)
E₀ : Set α := insert e (I₀ ∪ B₀)
hE₀fin : E₀.Finite
J : Set α
hJmax : ∀ ⦃j : Set α⦄, (fun x ↦ x ∈ {J | B₀ ⊆ J ∧ Indep J ∧ J ⊆ E₀}) j → id J ⊆ id j → id j ⊆ id J
hB₀J : B₀ ⊆ J
hJ : Indep J
hJss : J ⊆ E₀
heI₀ : e ∉ I₀
heI₀i : Indep (insert e I₀)
heJ : e ∉ J
hJfin : J.Finite
hcard : I₀.ncard < J.ncard
f : α
hfJ : f ∈ J
hfI₀ : f ∉ I₀
hfi : Indep (insert f I₀)
⊢ f ∈ I₀ ∪ B₀ → f ∈ B₀

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Constructions

Goal state before:
pp: α : Type u_1
M : Matroid α
E B I✝ X R J I : Set α
h : ∀ J ⊆ I, J.Finite → J ⊆ E
e : α
heI : e ∈ I
⊢ e ∈ E

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Constructions

Goal state before:
pp: α : Type u_1
M : Matroid α
E B I X R J : Set α
⊢ (freeOn E).Finitary

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Minor.Restrict

Goal state before:
pp: α : Type u_1
M : Matroid α
R I X : Set α
⊢ (M ↾ R).IsBasis' I X ↔ M.IsBasis' I (X ∩ R) ∧ I ⊆ R

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Constructions

Goal state before:
pp: α : Type u_1
E : Set α
hE : E.Nonempty
⊢ (freeOn E).RankPos

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Constructions

Goal state before:
pp: α : Type u_1
E B I : Set α
hIE : I ⊆ E
⊢ (uniqueBaseOn I E).IsBase B ↔ B = I

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Constructions

Goal state before:
pp: α : Type u_1
I E : Set α
⊢ uniqueBaseOn (I ∩ E) E = uniqueBaseOn I E

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Matroid.IndepAxioms

Goal state before:
pp: α : Type u_1
E : Set α
Indep : Set α → Prop
indep_empty : Indep ∅
indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I
indep_aug :
  ∀ ⦃I J : Set α⦄, Indep I → I.Finite → Indep J → J.Finite → I.ncard < J.ncard → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)
indep_compact : ∀ (I : Set α), (∀ J ⊆ I, J.Finite → Indep J) → Indep I
subset_ground : ∀ (I : Set α), Indep I → I ⊆ E
⊢ ∀ ⦃I B : Set α⦄, Indep I → ¬Maximal Indep I → Maximal Indep B → ∃ x ∈ B \ I, Indep (insert x I)

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Constructions

Goal state before:
pp: α : Type u_1
E I J : Set α
⊢ (uniqueBaseOn I E).Indep J ↔ J ⊆ I ∩ E

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Minor.Restrict

Goal state before:
pp: α : Type u_1
M : Matroid α
R I X : Set α
⊢ (M ↾ R).IsBasis I X ↔ M.IsBasis I (X ∩ M.E) ∧ X ⊆ R

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Dual

Goal state before:
pp: α : Type u_1
M✝ : Matroid α
I B✝ X✝ : Set α
M : Matroid α
X I' : Set α
hI'E : I' ⊆ M.E
B : Set α
hB : M.IsBase B
hI'B : Disjoint I' B
hI'X : I' ⊆ X
B' : Set α
hB' : M.IsBase B'
hI : M.IsBasis (B' \ X) (M.E \ X)
hIB' : B' \ X ⊆ B'
hB'IB : B' ⊆ B' \ X ∪ B
J : Set α
hJE : J ⊆ M.E
B'' : Set α
hB'' : M.IsBase B''
hdj : Disjoint J B''
hJX : J ⊆ X
hXJ : X \ B' ∩ M.E ⊆ J
hI' : B'' ∩ X ∪ B' \ X ⊆ B'
B₁ : Set α
hB₁ : M.IsBase B₁
hI'B₁ : B'' ∩ X ∪ B' \ X ⊆ B₁
hB₁I : B₁ ⊆ B'' ∪ B' \ X
⊢ B₁ = B'

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Constructions

Goal state before:
pp: α : Type u_1
E I J : Set α
hIE : I ⊆ E
⊢ (uniqueBaseOn I E).Indep J ↔ J ⊆ I

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Matroid.IndepAxioms

Goal state before:
pp: α : Type u_1
E : Set α
Indep : Set α → Prop
indep_empty : Indep ∅
indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I
indep_aug :
  ∀ ⦃I J : Set α⦄, Indep I → I.Finite → Indep J → J.Finite → I.ncard < J.ncard → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)
indep_compact : ∀ (I : Set α), (∀ J ⊆ I, J.Finite → Indep J) → Indep I
subset_ground : ∀ (I : Set α), Indep I → I ⊆ E
⊢ ∀ (I : Set α),
    (∀ J ⊆ I,
        J.Finite →
          (IndepMatroid.ofFinitaryCardAugment E Indep indep_empty indep_subset indep_aug indep_compact
                  subset_ground).matroid.Indep
            J) →
      (IndepMatroid.ofFinitaryCardAugment E Indep indep_empty indep_subset indep_aug indep_compact
              subset_ground).matroid.Indep
        I

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Minor.Restrict

Goal state before:
pp: α : Type u_1
M : Matroid α
R I X : Set α
hR : R ⊆ M.E
⊢ (M ↾ R).IsBasis I X ↔ M.IsBasis I X ∧ X ⊆ R

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Constructions

Goal state before:
pp: α : Type u_1
E I X J : Set α
hX : X ⊆ E
⊢ (uniqueBaseOn I E).Indep (X ∩ I) ∧ X ∩ I ⊆ X

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Constructions

Goal state before:
pp: α : Type u_1
E I X J : Set α
hX : X ⊆ E
⊢ ∀ ⦃x : Set α⦄, (uniqueBaseOn I E).Indep x ∧ x ⊆ X → x ⊆ X ∩ I

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Minor.Restrict

Goal state before:
pp: α : Type u_1
M : Matroid α
I X : Set α
⊢ M.IsBasis' I X ↔ (M ↾ univ).IsBasis I X

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Constructions

Goal state before:
pp: α : Type u_1
E I X J : Set α
hX : X ⊆ E
⊢ (uniqueBaseOn I E).IsBasis J X ↔ J = X ∩ I

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Constructions

Goal state before:
pp: α : Type u_1
E I X : Set α
hX : X ⊆ E
⊢ (uniqueBaseOn I E).IsBasis (X ∩ I) X

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Dual

Goal state before:
pp: α : Type u_1
M✝ : Matroid α
I B X : Set α
M : Matroid α
⊢ ∀ X ⊆ M.E, ExistsMaximalSubsetProperty (fun I ↦ I ⊆ M.E ∧ ∃ B, M.IsBase B ∧ Disjoint I B) X

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Dual

Goal state before:
pp: α : Type u_1
M✝ : Matroid α
I B X : Set α
M : Matroid α
⊢ ∀ (I : Set α), (I ⊆ M.E ∧ ∃ B, M.IsBase B ∧ Disjoint I B) → I ⊆ M.E

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Constructions

Goal state before:
pp: α : Type u_1
I E B : Set α
hB : B ⊆ E
h : E \ B = I ∩ E
⊢ B = E \ I

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Dual

Goal state before:
pp: α : Type u_1
M : Matroid α
I : Set α
hI : I ⊆ M.E
⊢ M✶.Indep I ↔ ∃ B, M.IsBase B ∧ Disjoint I B

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Constructions

Goal state before:
pp: α : Type u_1
I E B : Set α
hB : B ⊆ E
h : B = E \ I
⊢ E \ B = I ∩ E

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Constructions

Goal state before:
pp: α : Type u_1
I E : Set α
⊢ (uniqueBaseOn I E)✶ = uniqueBaseOn (E \ I) E

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Constructions

Goal state before:
pp: α : Type u_1
I : Set α
⊢ uniqueBaseOn I I = freeOn I

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Minor.Restrict

Goal state before:
pp: α : Type u_1
M M' : Matroid α
X : Set α
⊢ M ↾ X = M' ↾ X ↔ ∀ I ⊆ X, M.Indep I ↔ M'.Indep I

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Dual

Goal state before:
pp: α : Type u_1
M : Matroid α
I : Set α
⊢ M✶.Dep I ↔ (∀ (B : Set α), M.IsBase B → (I ∩ B).Nonempty) ∧ I ⊆ M.E

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Constructions

Goal state before:
pp: α : Type u_1
I : Set α
⊢ uniqueBaseOn ∅ I = loopyOn I

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Matroid.IndepAxioms

Goal state before:
pp: α : Type u_1
P : Set α → Prop
X : Set α
n : ℕ
hP : ∀ (Y : Set α), P Y → Y.encard ≤ ↑n
I : Set α
hI : P I
hIX : I ⊆ X
⊢ (ncard '' {Y | P Y ∧ I ⊆ Y ∧ Y ⊆ X}).Finite

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Minor.Restrict

Goal state before:
pp: α : Type u_1
M : Matroid α
R : Set α
h : M ↾ R = M
⊢ R = M.E

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Minor.Restrict

Goal state before:
pp: α : Type u_1
M : Matroid α
R : Set α
h : R = M.E
⊢ M ↾ R = M

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Constructions

Goal state before:
pp: α : Type u_1
I E R : Set α
⊢ uniqueBaseOn I E ↾ R = uniqueBaseOn (I ∩ R ∩ E) R

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Dual

Goal state before:
pp: α : Type u_1
M : Matroid α
B : Set α
hB : B ⊆ M.E
⊢ M✶.IsBase B ↔ M.IsBase (M.E \ B)

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Constructions

Goal state before:
pp: α : Type u_1
E I : Set α
h : I ⊆ E
R : Set α
⊢ uniqueBaseOn I E ↾ R = uniqueBaseOn (I ∩ R) R

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Dual

Goal state before:
pp: α : Type u_1
M : Matroid α
B : Set α
h : B ⊆ M.E
⊢ M✶.IsBase B ↔ M.IsBase (M.E \ B) ∧ B ⊆ M.E

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Constructions

Goal state before:
pp: α : Type u_1
E I : Set α
hI : I.Finite
⊢ (uniqueBaseOn I E).RankFinite

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Matroid.IndepAxioms

Goal state before:
pp: α : Type u_1
P : Set α → Prop
hP : ∃ n, ∀ (Y : Set α), P Y → Y.encard ≤ ↑n
X : Set α
⊢ ExistsMaximalSubsetProperty P X

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Constructions

Goal state before:
pp: α : 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:
by

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Constructions

Goal state before:
pp: α : 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}.Finite

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Constructions

Goal state before:
pp: α : Type u_1
M : Matroid α
E B I X R J : Set α
⊢ (uniqueBaseOn I E).Finitary

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Dual

Goal state before:
pp: α : Type u_1
M : Matroid α
⊢ {B | M✶.IsBase B} = (fun X ↦ M.E \ X) '' {B | M.IsBase B}

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Constructions

Goal state before:
pp: α : Type u_1
E I : Set α
hIE : I ⊆ E
hI : I.Nonempty
⊢ ¬(uniqueBaseOn I E).IsBase ∅

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Dual

Goal state before:
pp: α : Type u_1
M : Matroid α
B : Set α
h : B ⊆ M.E
⊢ M✶✶.IsBase B ↔ M.IsBase B

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Minor.Restrict

Goal state before:
pp: α✝ : Type u_1
M : Matroid α✝
R I X Y : Set α✝
N : Matroid α✝
α : Type u_2
M₁ M₂ M₃ : Matroidᵣ α
⊢ M₁.toMatroid ≤r M₂.toMatroid → M₂.toMatroid ≤r M₃.toMatroid → M₁.toMatroid ≤r M₃.toMatroid

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
f✝ : α → β
E I : Set α
M : Matroid α
N✝ N : Matroid β
f : α → β
⊢ N.Indep (f '' ∅) ∧ InjOn f ∅

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
f✝ : α → β
E I✝ : Set α
M : Matroid α
N✝ N : Matroid β
f : α → β
I B : Set α
hI : N.Indep (f '' I)
hIinj : InjOn f I
hImax : ¬Maximal (fun I ↦ N.Indep (f '' I) ∧ InjOn f I) I
hBmax : Maximal (fun I ↦ N.Indep (f '' I) ∧ InjOn f I) B
I' : Set α
hII' : I ⊂ I'
hI' : N.Indep (f '' I')
hI'inj : InjOn f I'
hB : (N ↾ range f).IsBase (f '' I)
⊢ (N ↾ range f).Indep (f '' I')

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
f✝ : α → β
E I✝ : Set α
M : Matroid α
N✝ N : Matroid β
f : α → β
I B : Set α
hI : N.Indep (f '' I)
hIinj : InjOn f I
hImax : ¬Maximal (fun I ↦ N.Indep (f '' I) ∧ InjOn f I) I
hBmax : Maximal (fun I ↦ N.Indep (f '' I) ∧ InjOn f I) B
I' : Set α
hII' : I ⊂ I'
hI' : N.Indep (f '' I')
hI'inj : InjOn f I'
⊢ ¬(N ↾ range f).IsBase (f '' I)

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
f✝ : α → β
E I✝ : Set α
M : Matroid α
N✝ N : Matroid β
f : α → β
I B : Set α
hI : N.Indep (f '' I)
hIinj : InjOn f I
hImax : ¬Maximal (fun I ↦ N.Indep (f '' I) ∧ InjOn f I) I
hBmax : Maximal (fun I ↦ N.Indep (f '' I) ∧ InjOn f I) B
I' : Set α
hII' : I ⊂ I'
hI' : N.Indep (f '' I')
hI'inj : InjOn f I'
h₁ : ¬(N ↾ range f).IsBase (f '' I)
⊢ (N ↾ range f).Indep (f '' B)

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Dual

Goal state before:
pp: α : Type u_1
M₁ M₂ : Matroid α
⊢ M₁ = M₂✶ ↔ M₂ = M₁✶

Tactic:
by

Goal state after: