internlm/Lean-Github huggingface dataset:
Theorem: Matroid.er_le_er_inter_add_er_diff
Proof state before:
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X✝ X' Y✝ Y' Z R : Set α
n : ℕ∞
e f : α
X Y : Set α
⊢ M.er X ≤ M.er (X ∩ Y) + M.er (X \ Y)
Tactic:
nth_rw 1 [← inter_union_diff X Y]
Proof state after:
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X✝ X' Y✝ Y' Z R : Set α
n : ℕ∞
e f : α
X Y : Set α
⊢ M.er (X ∩ Y ∪ X \ Y) ≤ M.er (X ∩ Y) + M.er (X \ Y)
Theorem: Matroid.er_le_er_inter_add_er_diff
Proof state before:
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X✝ X' Y✝ Y' Z R : Set α
n : ℕ∞
e f : α
X Y : Set α
⊢ M.er (X ∩ Y ∪ X \ Y) ≤ M.er (X ∩ Y) + M.er (X \ Y)
Tactic:
apply er_union_le_er_add_er
Proof state after:
no goals
Theorem: Matroid.er_le_er_add_er_diff
Proof state before:
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
h : Y ⊆ X
⊢ M.er X ≤ M.er Y + M.er (X \ Y)
Tactic:
nth_rw 1 [← union_diff_cancel h]
Proof state after:
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
h : Y ⊆ X
⊢ M.er (Y ∪ X \ Y) ≤ M.er Y + M.er (X \ Y)
Theorem: Matroid.er_le_er_add_er_diff
Proof state before:
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
h : Y ⊆ X
⊢ M.er (Y ∪ X \ Y) ≤ M.er Y + M.er (X \ Y)
Tactic:
apply er_union_le_er_add_er
Proof state after:
no goals
Theorem: Matroid.indep_iff_er_eq_encard_of_finite
Proof state before:
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
hI : I.Finite
⊢ M.Indep I ↔ M.er I = I.encard
Tactic:
refine' ⟨fun h ↦ by rw [h.er], fun h ↦ _⟩
Proof state after:
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
hI : I.Finite
h : M.er I = I.encard
⊢ M.Indep I
Theorem: Matroid.indep_iff_er_eq_encard_of_finite
Proof state before:
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
hI : I.Finite
h : M.er I = I.encard
⊢ M.Indep I
Tactic:
obtain ⟨J, hJ⟩ := M.exists_basis' I
Proof state after:
case intro
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
hI : I.Finite
h : M.er I = I.encard
J : Set α
hJ : M.Basis' J I
⊢ M.Indep I
Theorem: Matroid.indep_iff_er_eq_encard_of_finite
Proof state before:
case intro
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
hI : I.Finite
h : M.er I = I.encard
J : Set α
hJ : M.Basis' J I
⊢ M.Indep I
Tactic:
rw [← hI.eq_of_subset_of_encard_le hJ.subset]
Proof state after:
case intro
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
hI : I.Finite
h : M.er I = I.encard
J : Set α
hJ : M.Basis' J I
⊢ M.Indep J

case intro
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
hI : I.Finite
h : M.er I = I.encard
J : Set α
hJ : M.Basis' J I
⊢ I.encard ≤ J.encard
Theorem: Matroid.indep_iff_er_eq_encard_of_finite
Proof state before:
case intro
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
hI : I.Finite
h : M.er I = I.encard
J : Set α
hJ : M.Basis' J I
⊢ I.encard ≤ J.encard
Tactic:
rw [← h, ← hJ.er_eq_encard]
Proof state after:
no goals
Theorem: Matroid.indep_iff_er_eq_encard_of_finite
Proof state before:
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
hI : I.Finite
h : M.Indep I
⊢ M.er I = I.encard
Tactic:
rw [h.er]
Proof state after:
no goals
Theorem: Matroid.indep_iff_er_eq_encard_of_finite
Proof state before:
case intro
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
hI : I.Finite
h : M.er I = I.encard
J : Set α
hJ : M.Basis' J I
⊢ M.Indep J
Tactic:
exact hJ.indep
Proof state after:
no goals
Theorem: Matroid.er_singleton_le
Proof state before:
α : Type u_1
ι : Type u_2
M✝ N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e✝ f : α
M : Matroid α
e : α
⊢ M.er {e} ≤ 1
Tactic:
obtain ⟨J, hJ⟩ := M.exists_basis' {e}
Proof state after:
case intro
α : Type u_1
ι : Type u_2
M✝ N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e✝ f : α
M : Matroid α
e : α
J : Set α
hJ : M.Basis' J {e}
⊢ M.er {e} ≤ 1
Theorem: Matroid.er_singleton_le
Proof state before:
case intro
α : Type u_1
ι : Type u_2
M✝ N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e✝ f : α
M : Matroid α
e : α
J : Set α
hJ : M.Basis' J {e}
⊢ M.er {e} ≤ 1
Tactic:
rw [hJ.er_eq_encard, ← encard_singleton e]
Proof state after:
case intro
α : Type u_1
ι : Type u_2
M✝ N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e✝ f : α
M : Matroid α
e : α
J : Set α
hJ : M.Basis' J {e}
⊢ J.encard ≤ {e}.encard
Theorem: Matroid.er_singleton_le
Proof state before:
case intro
α : Type u_1
ι : Type u_2
M✝ N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e✝ f : α
M : Matroid α
e : α
J : Set α
hJ : M.Basis' J {e}
⊢ J.encard ≤ {e}.encard
Tactic:
exact encard_mono hJ.subset
Proof state after:
no goals
Theorem: Matroid.er_lt_encard_iff_dep_of_finite
Proof state before:
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
hX : X.Finite
hXE : autoParam (X ⊆ M.E) _auto✝
⊢ M.er X < X.encard ↔ M.Dep X
Tactic:
refine' ⟨fun h ↦ _, fun h ↦ er_lt_encard_of_dep_of_finite hX h⟩
Proof state after:
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
hX : X.Finite
hXE : autoParam (X ⊆ M.E) _auto✝
h : M.er X < X.encard
⊢ M.Dep X
Theorem: Matroid.er_lt_encard_iff_dep_of_finite
Proof state before:
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
hX : X.Finite
hXE : autoParam (X ⊆ M.E) _auto✝
h : M.er X < X.encard
⊢ M.Dep X
Tactic:
rw [← not_indep_iff, indep_iff_er_eq_encard_of_finite hX]
Proof state after:
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
hX : X.Finite
hXE : autoParam (X ⊆ M.E) _auto✝
h : M.er X < X.encard
⊢ ¬M.er X = X.encard
Theorem: Matroid.er_lt_encard_iff_dep_of_finite
Proof state before:
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
hX : X.Finite
hXE : autoParam (X ⊆ M.E) _auto✝
h : M.er X < X.encard
⊢ ¬M.er X = X.encard
Tactic:
exact h.ne
Proof state after:
no goals
Theorem: Matroid.basis'_iff_indep_encard_eq_of_finite
Proof state before:
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
hIfin : I.Finite
⊢ M.Basis' I X ↔ I ⊆ X ∧ M.Indep I ∧ I.encard = M.er X
Tactic:
refine' ⟨fun h ↦ ⟨h.subset,h.indep, h.er_eq_encard.symm⟩, fun ⟨hIX, hI, hcard⟩  ↦ _⟩
Proof state after:
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
hIfin : I.Finite
x✝ : I ⊆ X ∧ M.Indep I ∧ I.encard = M.er X
hIX : I ⊆ X
hI : M.Indep I
hcard : I.encard = M.er X
⊢ M.Basis' I X
Theorem: Matroid.basis'_iff_indep_encard_eq_of_finite
Proof state before:
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
hIfin : I.Finite
x✝ : I ⊆ X ∧ M.Indep I ∧ I.encard = M.er X
hIX : I ⊆ X
hI : M.Indep I
hcard : I.encard = M.er X
⊢ M.Basis' I X
Tactic:
rw [basis'_iff_basis_inter_ground]
Proof state after:
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
hIfin : I.Finite
x✝ : I ⊆ X ∧ M.Indep I ∧ I.encard = M.er X
hIX : I ⊆ X
hI : M.Indep I
hcard : I.encard = M.er X
⊢ M.Basis I (X ∩ M.E)
Theorem: Matroid.basis'_iff_indep_encard_eq_of_finite
Proof state before:
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
hIfin : I.Finite
x✝ : I ⊆ X ∧ M.Indep I ∧ I.encard = M.er X
hIX : I ⊆ X
hI : M.Indep I
hcard : I.encard = M.er X
⊢ M.Basis I (X ∩ M.E)
Tactic:
obtain ⟨J, hJ, hIJ⟩ := hI.subset_basis_of_subset (subset_inter hIX hI.subset_ground)
Proof state after:
case intro.intro
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
hIfin : I.Finite
x✝ : I ⊆ X ∧ M.Indep I ∧ I.encard = M.er X
hIX : I ⊆ X
hI : M.Indep I
hcard : I.encard = M.er X
J : Set α
hJ : M.Basis J (X ∩ M.E)
hIJ : I ⊆ J
⊢ M.Basis I (X ∩ M.E)
Theorem: Matroid.basis'_iff_indep_encard_eq_of_finite
Proof state before:
case intro.intro
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
hIfin : I.Finite
x✝ : I ⊆ X ∧ M.Indep I ∧ I.encard = M.er X
hIX : I ⊆ X
hI : M.Indep I
hcard : I.encard = M.er X
J : Set α
hJ : M.Basis J (X ∩ M.E)
hIJ : I ⊆ J
⊢ M.Basis I (X ∩ M.E)
Tactic:
apply hI.basis_of_subset_of_subset_cl (subset_inter hIX hI.subset_ground)
Proof state after:
case intro.intro
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
hIfin : I.Finite
x✝ : I ⊆ X ∧ M.Indep I ∧ I.encard = M.er X
hIX : I ⊆ X
hI : M.Indep I
hcard : I.encard = M.er X
J : Set α
hJ : M.Basis J (X ∩ M.E)
hIJ : I ⊆ J
⊢ X ∩ M.E ⊆ M.cl I
Theorem: Matroid.basis'_iff_indep_encard_eq_of_finite
Proof state before:
case intro.intro
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
hIfin : I.Finite
x✝ : I ⊆ X ∧ M.Indep I ∧ I.encard = M.er X
hIX : I ⊆ X
hI : M.Indep I
hcard : I.encard = M.er X
J : Set α
hJ : M.Basis J (X ∩ M.E)
hIJ : I ⊆ J
⊢ X ∩ M.E ⊆ M.cl I
Tactic:
obtain rfl := hIfin.eq_of_subset_of_encard_le' hIJ
  (by rw [hcard, ← hJ.er_eq_encard, er_inter_ground_eq ])
Proof state after:
case intro.intro
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
hIfin : I.Finite
x✝ : I ⊆ X ∧ M.Indep I ∧ I.encard = M.er X
hIX : I ⊆ X
hI : M.Indep I
hcard : I.encard = M.er X
hJ : M.Basis I (X ∩ M.E)
hIJ : I ⊆ I
⊢ X ∩ M.E ⊆ M.cl I
Theorem: Matroid.basis'_iff_indep_encard_eq_of_finite
Proof state before:
case intro.intro
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
hIfin : I.Finite
x✝ : I ⊆ X ∧ M.Indep I ∧ I.encard = M.er X
hIX : I ⊆ X
hI : M.Indep I
hcard : I.encard = M.er X
hJ : M.Basis I (X ∩ M.E)
hIJ : I ⊆ I
⊢ X ∩ M.E ⊆ M.cl I
Tactic:
exact hJ.subset_cl
Proof state after:
no goals
Theorem: Matroid.basis'_iff_indep_encard_eq_of_finite
Proof state before:
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
hIfin : I.Finite
x✝ : I ⊆ X ∧ M.Indep I ∧ I.encard = M.er X
hIX : I ⊆ X
hI : M.Indep I
hcard : I.encard = M.er X
J : Set α
hJ : M.Basis J (X ∩ M.E)
hIJ : I ⊆ J
⊢ J.encard ≤ I.encard
Tactic:
rw [hcard, ← hJ.er_eq_encard, er_inter_ground_eq ]
Proof state after:
no goals
Theorem: Matroid.basis_iff_indep_encard_eq_of_finite
Proof state before:
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
hIfin : I.Finite
hX : autoParam (X ⊆ M.E) _auto✝
⊢ M.Basis I X ↔ I ⊆ X ∧ M.Indep I ∧ I.encard = M.er X
Tactic:
rw [← basis'_iff_basis, basis'_iff_indep_encard_eq_of_finite hIfin]
Proof state after:
no goals
Theorem: Matroid.Indep.basis_of_subset_of_er_le_of_finite
Proof state before:
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
hI : M.Indep I
hIX : I ⊆ X
h : M.er X ≤ M.er I
hIfin : I.Finite
hX : autoParam (X ⊆ M.E) _auto✝
⊢ M.Basis I X
Tactic:
rw [basis_iff_indep_encard_eq_of_finite hIfin hX, and_iff_right hIX, and_iff_right hI,
   le_antisymm_iff, and_iff_left (h.trans hI.er.le), ← hI.er]
Proof state after:
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
hI : M.Indep I
hIX : I ⊆ X
h : M.er X ≤ M.er I
hIfin : I.Finite
hX : autoParam (X ⊆ M.E) _auto✝
⊢ M.er I ≤ M.er X
Theorem: Matroid.Indep.basis_of_subset_of_er_le_of_finite
Proof state before:
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
hI : M.Indep I
hIX : I ⊆ X
h : M.er X ≤ M.er I
hIfin : I.Finite
hX : autoParam (X ⊆ M.E) _auto✝
⊢ M.er I ≤ M.er X
Tactic:
exact M.er_mono hIX
Proof state after:
no goals
Theorem: Matroid.er_insert_le_add_one
Proof state before:
α : Type u_1
ι : Type u_2
M✝ N : Matroid α
I B X✝ X' Y Y' Z R : Set α
n : ℕ∞
e✝ f : α
M : Matroid α
e : α
X : Set α
⊢ M.er (insert e X) ≤ M.er X + 1
Tactic:
rw [← union_singleton]
Proof state after:
α : Type u_1
ι : Type u_2
M✝ N : Matroid α
I B X✝ X' Y Y' Z R : Set α
n : ℕ∞
e✝ f : α
M : Matroid α
e : α
X : Set α
⊢ M.er (X ∪ {e}) ≤ M.er X + 1
Theorem: Matroid.er_insert_le_add_one
Proof state before:
α : Type u_1
ι : Type u_2
M✝ N : Matroid α
I B X✝ X' Y Y' Z R : Set α
n : ℕ∞
e✝ f : α
M : Matroid α
e : α
X : Set α
⊢ M.er (X ∪ {e}) ≤ M.er X + 1
Tactic:
exact (M.er_union_le_er_add_er _ _).trans (add_le_add_left (er_singleton_le _ _) _)
Proof state after:
no goals
Theorem: Matroid.erk_le_encard_add_er_compl
Proof state before:
α : Type u_1
ι : Type u_2
M✝ N : Matroid α
I B X✝ X' Y Y' Z R : Set α
n : ℕ∞
e f : α
M : Matroid α
X : Set α
⊢ M.erk ≤ M.er (X ∪ M.E \ X)
Tactic:
rw [← er_inter_ground_eq, erk_eq_er_ground, union_diff_self,
union_inter_cancel_right]
Proof state after:
no goals
Theorem: Matroid.er_insert_eq_add_one
Proof state before:
α : Type u_1
ι : Type u_2
M✝ N : Matroid α
I B X✝ X' Y Y' Z R : Set α
n : ℕ∞
e f : α
M : Matroid α
X : Set α
he : e ∈ M.E \ M.cl X
⊢ M.er (insert e X) = M.er X + 1
Tactic:
obtain ⟨I, hI⟩ := M.exists_basis' X
Proof state after:
case intro
α : Type u_1
ι : Type u_2
M✝ N : Matroid α
I✝ B X✝ X' Y Y' Z R : Set α
n : ℕ∞
e f : α
M : Matroid α
X : Set α
he : e ∈ M.E \ M.cl X
I : Set α
hI : M.Basis' I X
⊢ M.er (insert e X) = M.er X + 1
Theorem: Matroid.er_insert_eq_add_one
Proof state before:
case intro
α : Type u_1
ι : Type u_2
M✝ N : Matroid α
I✝ B X✝ X' Y Y' Z R : Set α
n : ℕ∞
e f : α
M : Matroid α
X : Set α
he : e ∈ M.E \ M.cl X
I : Set α
hI : M.Basis' I X
⊢ M.er (insert e X) = M.er X + 1
Tactic:
rw [← hI.cl_eq_cl] at he
Proof state after:
case intro
α : Type u_1
ι : Type u_2
M✝ N : Matroid α
I✝ B X✝ X' Y Y' Z R : Set α
n : ℕ∞
e f : α
M : Matroid α
X I : Set α
he : e ∈ M.E \ M.cl I
hI : M.Basis' I X
⊢ M.er (insert e X) = M.er X + 1
Theorem: Matroid.er_insert_eq_add_one
Proof state before:
case intro
α : Type u_1
ι : Type u_2
M✝ N : Matroid α
I✝ B X✝ X' Y Y' Z R : Set α
n : ℕ∞
e f : α
M : Matroid α
X I : Set α
he : e ∈ M.E \ M.cl I
hI : M.Basis' I X
⊢ M.er (insert e X) = M.er X + 1
Tactic:
rw [← er_cl_eq, ← cl_insert_cl_eq_cl_insert, ← hI.cl_eq_cl, hI.er_eq_encard,
  cl_insert_cl_eq_cl_insert, er_cl_eq, Indep.er, encard_insert_of_not_mem]
Proof state after:
case intro
α : Type u_1
ι : Type u_2
M✝ N : Matroid α
I✝ B X✝ X' Y Y' Z R : Set α
n : ℕ∞
e f : α
M : Matroid α
X I : Set α
he : e ∈ M.E \ M.cl I
hI : M.Basis' I X
⊢ e ∉ I

case intro
α : Type u_1
ι : Type u_2
M✝ N : Matroid α
I✝ B X✝ X' Y Y' Z R : Set α
n : ℕ∞
e f : α
M : Matroid α
X I : Set α
he : e ∈ M.E \ M.cl I
hI : M.Basis' I X
⊢ M.Indep (insert e I)
Theorem: Matroid.er_insert_eq_add_one
Proof state before:
case intro
α : Type u_1
ι : Type u_2
M✝ N : Matroid α
I✝ B X✝ X' Y Y' Z R : Set α
n : ℕ∞
e f : α
M : Matroid α
X I : Set α
he : e ∈ M.E \ M.cl I
hI : M.Basis' I X
⊢ M.Indep (insert e I)
Tactic:
rw [hI.indep.insert_indep_iff]
Proof state after:
case intro
α : Type u_1
ι : Type u_2
M✝ N : Matroid α
I✝ B X✝ X' Y Y' Z R : Set α
n : ℕ∞
e f : α
M : Matroid α
X I : Set α
he : e ∈ M.E \ M.cl I
hI : M.Basis' I X
⊢ e ∈ M.E \ M.cl I ∨ e ∈ I
Theorem: Matroid.er_insert_eq_add_one
Proof state before:
case intro
α : Type u_1
ι : Type u_2
M✝ N : Matroid α
I✝ B X✝ X' Y Y' Z R : Set α
n : ℕ∞
e f : α
M : Matroid α
X I : Set α
he : e ∈ M.E \ M.cl I
hI : M.Basis' I X
⊢ e ∈ M.E \ M.cl I ∨ e ∈ I
Tactic:
exact Or.inl he
Proof state after:
no goals
Theorem: Matroid.er_insert_eq_add_one
Proof state before:
case intro
α : Type u_1
ι : Type u_2
M✝ N : Matroid α
I✝ B X✝ X' Y Y' Z R : Set α
n : ℕ∞
e f : α
M : Matroid α
X I : Set α
he : e ∈ M.E \ M.cl I
hI : M.Basis' I X
⊢ e ∉ I
Tactic:
exact fun heI ↦ he.2 (M.subset_cl I hI.indep.subset_ground heI)
Proof state after:
no goals
Theorem: Matroid.er_augment
Proof state before:
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
h : M.er X < M.er Z
⊢ ∃ z ∈ Z \ X, M.er (insert z X) = M.er X + 1
Tactic:
obtain ⟨I, hI⟩ := M.exists_basis' X
Proof state after:
case intro
α : Type u_1
ι : Type u_2
M N : Matroid α
I✝ B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
h : M.er X < M.er Z
I : Set α
hI : M.Basis' I X
⊢ ∃ z ∈ Z \ X, M.er (insert z X) = M.er X + 1
Theorem: Matroid.er_augment
Proof state before:
case intro
α : Type u_1
ι : Type u_2
M N : Matroid α
I✝ B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
h : M.er X < M.er Z
I : Set α
hI : M.Basis' I X
⊢ ∃ z ∈ Z \ X, M.er (insert z X) = M.er X + 1
Tactic:
obtain ⟨J, hJ, hIJ⟩ := hI.indep.subset_basis'_of_subset (hI.subset.trans subset_union_left)
Proof state after:
case intro.intro.intro
α : Type u_1
ι : Type u_2
M N : Matroid α
I✝ B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
h : M.er X < M.er Z
I : Set α
hI : M.Basis' I X
J : Set α
hJ : M.Basis' J (X ∪ ?m.32367)
hIJ : I ⊆ J
⊢ ∃ z ∈ Z \ X, M.er (insert z X) = M.er X + 1
Theorem: Matroid.er_augment
Proof state before:
case intro.intro.intro
α : Type u_1
ι : Type u_2
M N : Matroid α
I✝ B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
h : M.er X < M.er Z
I : Set α
hI : M.Basis' I X
J : Set α
hJ : M.Basis' J (X ∪ ?m.32367)
hIJ : I ⊆ J
⊢ ∃ z ∈ Z \ X, M.er (insert z X) = M.er X + 1
Tactic:
have hlt := h.trans_le (M.er_mono (subset_union_right (s := X)))
Proof state after:
case intro.intro.intro
α : Type u_1
ι : Type u_2
M N : Matroid α
I✝ B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
h : M.er X < M.er Z
I : Set α
hI : M.Basis' I X
J : Set α
hJ : M.Basis' J (X ∪ ?m.32367)
hIJ : I ⊆ J
hlt : M.er X < M.er (X ∪ Z)
⊢ ∃ z ∈ Z \ X, M.er (insert z X) = M.er X + 1
Theorem: Matroid.er_augment
Proof state before:
case intro.intro.intro
α : Type u_1
ι : Type u_2
M N : Matroid α
I✝ B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
h : M.er X < M.er Z
I : Set α
hI : M.Basis' I X
J : Set α
hJ : M.Basis' J (X ∪ ?m.32367)
hIJ : I ⊆ J
hlt : M.er X < M.er (X ∪ Z)
⊢ ∃ z ∈ Z \ X, M.er (insert z X) = M.er X + 1
Tactic:
rw [hI.er_eq_encard, hJ.er_eq_encard] at hlt
Proof state after:
case intro.intro.intro
α : Type u_1
ι : Type u_2
M N : Matroid α
I✝ B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
h : M.er X < M.er Z
I : Set α
hI : M.Basis' I X
J : Set α
hJ : M.Basis' J (X ∪ Z)
hIJ : I ⊆ J
hlt : I.encard < J.encard
⊢ ∃ z ∈ Z \ X, M.er (insert z X) = M.er X + 1
Theorem: Matroid.er_augment
Proof state before:
case intro.intro.intro
α : Type u_1
ι : Type u_2
M N : Matroid α
I✝ B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
h : M.er X < M.er Z
I : Set α
hI : M.Basis' I X
J : Set α
hJ : M.Basis' J (X ∪ Z)
hIJ : I ⊆ J
hlt : I.encard < J.encard
⊢ ∃ z ∈ Z \ X, M.er (insert z X) = M.er X + 1
Tactic:
obtain ⟨e, heJ, heI⟩ := exists_of_ssubset (hIJ.ssubset_of_ne (by rintro rfl; exact hlt.ne rfl))
Proof state after:
case intro.intro.intro.intro.intro
α : Type u_1
ι : Type u_2
M N : Matroid α
I✝ B X X' Y Y' Z R : Set α
n : ℕ∞
e✝ f : α
h : M.er X < M.er Z
I : Set α
hI : M.Basis' I X
J : Set α
hJ : M.Basis' J (X ∪ Z)
hIJ : I ⊆ J
hlt : I.encard < J.encard
e : α
heJ : e ∈ J
heI : e ∉ I
⊢ ∃ z ∈ Z \ X, M.er (insert z X) = M.er X + 1
Theorem: Matroid.er_augment
Proof state before:
case intro.intro.intro.intro.intro
α : Type u_1
ι : Type u_2
M N : Matroid α
I✝ B X X' Y Y' Z R : Set α
n : ℕ∞
e✝ f : α
h : M.er X < M.er Z
I : Set α
hI : M.Basis' I X
J : Set α
hJ : M.Basis' J (X ∪ Z)
hIJ : I ⊆ J
hlt : I.encard < J.encard
e : α
heJ : e ∈ J
heI : e ∉ I
⊢ ∃ z ∈ Z \ X, M.er (insert z X) = M.er X + 1
Tactic:
have heIi : M.Indep (insert e I) := hJ.indep.subset (insert_subset heJ hIJ)
Proof state after:
case intro.intro.intro.intro.intro
α : Type u_1
ι : Type u_2
M N : Matroid α
I✝ B X X' Y Y' Z R : Set α
n : ℕ∞
e✝ f : α
h : M.er X < M.er Z
I : Set α
hI : M.Basis' I X
J : Set α
hJ : M.Basis' J (X ∪ Z)
hIJ : I ⊆ J
hlt : I.encard < J.encard
e : α
heJ : e ∈ J
heI : e ∉ I
heIi : M.Indep (insert e I)
⊢ ∃ z ∈ Z \ X, M.er (insert z X) = M.er X + 1
Theorem: Matroid.er_augment
Proof state before:
case intro.intro.intro.intro.intro
α : Type u_1
ι : Type u_2
M N : Matroid α
I✝ B X X' Y Y' Z R : Set α
n : ℕ∞
e✝ f : α
h : M.er X < M.er Z
I : Set α
hI : M.Basis' I X
J : Set α
hJ : M.Basis' J (X ∪ Z)
hIJ : I ⊆ J
hlt : I.encard < J.encard
e : α
heJ : e ∈ J
heI : e ∉ I
heIi : M.Indep (insert e I)
⊢ ∃ z ∈ Z \ X, M.er (insert z X) = M.er X + 1
Tactic:
have heX : e ∉ X := fun h ↦
  heI (hI.basis_inter_ground.mem_of_insert_indep ⟨h, hJ.indep.subset_ground heJ⟩ heIi)
Proof state after:
case intro.intro.intro.intro.intro
α : Type u_1
ι : Type u_2
M N : Matroid α
I✝ B X X' Y Y' Z R : Set α
n : ℕ∞
e✝ f : α
h : M.er X < M.er Z
I : Set α
hI : M.Basis' I X
J : Set α
hJ : M.Basis' J (X ∪ Z)
hIJ : I ⊆ J
hlt : I.encard < J.encard
e : α
heJ : e ∈ J
heI : e ∉ I
heIi : M.Indep (insert e I)
heX : e ∉ X
⊢ ∃ z ∈ Z \ X, M.er (insert z X) = M.er X + 1
Theorem: Matroid.er_augment
Proof state before:
case intro.intro.intro.intro.intro
α : Type u_1
ι : Type u_2
M N : Matroid α
I✝ B X X' Y Y' Z R : Set α
n : ℕ∞
e✝ f : α
h : M.er X < M.er Z
I : Set α
hI : M.Basis' I X
J : Set α
hJ : M.Basis' J (X ∪ Z)
hIJ : I ⊆ J
hlt : I.encard < J.encard
e : α
heJ : e ∈ J
heI : e ∉ I
heIi : M.Indep (insert e I)
heX : e ∉ X
⊢ ∃ z ∈ Z \ X, M.er (insert z X) = M.er X + 1
Tactic:
refine ⟨e, ⟨Or.elim (hJ.subset heJ) (False.elim ∘ heX) id, heX⟩, ?_⟩
Proof state after:
case intro.intro.intro.intro.intro
α : Type u_1
ι : Type u_2
M N : Matroid α
I✝ B X X' Y Y' Z R : Set α
n : ℕ∞
e✝ f : α
h : M.er X < M.er Z
I : Set α
hI : M.Basis' I X
J : Set α
hJ : M.Basis' J (X ∪ Z)
hIJ : I ⊆ J
hlt : I.encard < J.encard
e : α
heJ : e ∈ J
heI : e ∉ I
heIi : M.Indep (insert e I)
heX : e ∉ X
⊢ M.er (insert e X) = M.er X + 1
Theorem: Matroid.er_augment
Proof state before:
case intro.intro.intro.intro.intro
α : Type u_1
ι : Type u_2
M N : Matroid α
I✝ B X X' Y Y' Z R : Set α
n : ℕ∞
e✝ f : α
h : M.er X < M.er Z
I : Set α
hI : M.Basis' I X
J : Set α
hJ : M.Basis' J (X ∪ Z)
hIJ : I ⊆ J
hlt : I.encard < J.encard
e : α
heJ : e ∈ J
heI : e ∉ I
heIi : M.Indep (insert e I)
heX : e ∉ X
⊢ M.er (insert e X) = M.er X + 1
Tactic:
rw [← hI.er_eq_er_insert, hI.er_eq_encard, heIi.er, encard_insert_of_not_mem heI]
Proof state after:
no goals
Theorem: Matroid.er_augment
Proof state before:
α : Type u_1
ι : Type u_2
M N : Matroid α
I✝ B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
h : M.er X < M.er Z
I : Set α
hI : M.Basis' I X
J : Set α
hJ : M.Basis' J (X ∪ Z)
hIJ : I ⊆ J
hlt : I.encard < J.encard
⊢ I ≠ J
Tactic:
rintro rfl
Proof state after:
α : Type u_1
ι : Type u_2
M N : Matroid α
I✝ B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
h : M.er X < M.er Z
I : Set α
hI : M.Basis' I X
hJ : M.Basis' I (X ∪ Z)
hIJ : I ⊆ I
hlt : I.encard < I.encard
⊢ False
Theorem: Matroid.er_augment
Proof state before:
α : Type u_1
ι : Type u_2
M N : Matroid α
I✝ B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
h : M.er X < M.er Z
I : Set α
hI : M.Basis' I X
hJ : M.Basis' I (X ∪ Z)
hIJ : I ⊆ I
hlt : I.encard < I.encard
⊢ False
Tactic:
exact hlt.ne rfl
Proof state after:
no goals
Theorem: Matroid.er_eq_of_er_insert_le_forall
Proof state before:
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
hXY : X ⊆ Y
hY : ∀ e ∈ Y \ X, M.er (insert e X) ≤ M.er X
⊢ M.er X = M.er Y
Tactic:
refine (M.er_mono hXY).eq_of_not_lt (fun hlt ↦ ?_)
Proof state after:
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
hXY : X ⊆ Y
hY : ∀ e ∈ Y \ X, M.er (insert e X) ≤ M.er X
hlt : M.er X < M.er Y
⊢ False
Theorem: Matroid.er_eq_of_er_insert_le_forall
Proof state before:
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
hXY : X ⊆ Y
hY : ∀ e ∈ Y \ X, M.er (insert e X) ≤ M.er X
hlt : M.er X < M.er Y
⊢ False
Tactic:
obtain ⟨e, he, hins⟩ := er_augment hlt
Proof state after:
case intro.intro
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e✝ f : α
hXY : X ⊆ Y
hY : ∀ e ∈ Y \ X, M.er (insert e X) ≤ M.er X
hlt : M.er X < M.er Y
e : α
he : e ∈ Y \ X
hins : M.er (insert e X) = M.er X + 1
⊢ False
Theorem: Matroid.er_eq_of_er_insert_le_forall
Proof state before:
case intro.intro
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e✝ f : α
hXY : X ⊆ Y
hY : ∀ e ∈ Y \ X, M.er (insert e X) ≤ M.er X
hlt : M.er X < M.er Y
e : α
he : e ∈ Y \ X
hins : M.er (insert e X) = M.er X + 1
⊢ False
Tactic:
specialize hY e he
Proof state after:
case intro.intro
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e✝ f : α
hXY : X ⊆ Y
hlt : M.er X < M.er Y
e : α
he : e ∈ Y \ X
hins : M.er (insert e X) = M.er X + 1
hY : M.er (insert e X) ≤ M.er X
⊢ False