internlm/Lean-Github huggingface dataset:
Theorem: Matroid.erk_emptyOn
Proof state before:
α✝ : Type u_1
ι : Type u_2
M N : Matroid α✝
I B X X' Y Y' Z R : Set α✝
n : ℕ∞
e f : α✝
α : Type u_3
⊢ (emptyOn α).erk = 0
Tactic:
simp [← (show (emptyOn α).Base ∅ by simp).encard]
Proof state after:
no goals
Theorem: Matroid.erk_emptyOn
Proof state before:
α✝ : Type u_1
ι : Type u_2
M N : Matroid α✝
I B X X' Y Y' Z R : Set α✝
n : ℕ∞
e f : α✝
α : Type u_3
⊢ (emptyOn α).Base ∅
Tactic:
simp
Proof state after:
no goals
Theorem: Matroid.Iso.erk_eq
Proof state before:
α : Type u_1
ι : Type u_2
M N✝ : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e✝ f : α
β : Type u_3
N : Matroid β
e : M ≂ N
⊢ M.erk = N.erk
Tactic:
obtain (rfl | hne) := M.eq_emptyOn_or_nonempty
Proof state after:
case inl
α : Type u_1
ι : Type u_2
N✝ : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e✝ f : α
β : Type u_3
N : Matroid β
e : emptyOn α ≂ N
⊢ (emptyOn α).erk = N.erk

case inr
α : Type u_1
ι : Type u_2
M N✝ : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e✝ f : α
β : Type u_3
N : Matroid β
e : M ≂ N
hne : M.Nonempty
⊢ M.erk = N.erk
Theorem: Matroid.Iso.erk_eq
Proof state before:
case inr
α : Type u_1
ι : Type u_2
M N✝ : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e✝ f : α
β : Type u_3
N : Matroid β
e : M ≂ N
hne : M.Nonempty
⊢ M.erk = N.erk
Tactic:
obtain ⟨f, hf, rfl⟩ := e.exists_eq_map'
Proof state after:
case inr.intro.intro
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e✝ f✝ : α
β : Type u_3
hne : M.Nonempty
f : α → β
hf : InjOn f M.E
e : M ≂ M.map f hf
⊢ M.erk = (M.map f hf).erk
Theorem: Matroid.Iso.erk_eq
Proof state before:
case inr.intro.intro
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e✝ f✝ : α
β : Type u_3
hne : M.Nonempty
f : α → β
hf : InjOn f M.E
e : M ≂ M.map f hf
⊢ M.erk = (M.map f hf).erk
Tactic:
simp
Proof state after:
no goals
Theorem: Matroid.Iso.erk_eq
Proof state before:
case inl
α : Type u_1
ι : Type u_2
N✝ : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e✝ f : α
β : Type u_3
N : Matroid β
e : emptyOn α ≂ N
⊢ (emptyOn α).erk = N.erk
Tactic:
simp [e.right_eq_empty]
Proof state after:
no goals
Theorem: Matroid.er_inter_ground_eq
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.er (X ∩ M.E) = M.er X
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 I : Set α
hI : M.Basis' I X
⊢ M.er (X ∩ M.E) = M.er X
Theorem: Matroid.er_inter_ground_eq
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 α
hI : M.Basis' I X
⊢ M.er (X ∩ M.E) = M.er X
Tactic:
rw [← hI.basis_inter_ground.encard, ← hI.encard]
Proof state after:
no goals
Theorem: Matroid.er_map_eq
Proof state before:
α : Type u_1
ι : Type u_2
M✝ N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f✝ : α
β : Type u_3
f : α → β
M : Matroid α
hf : InjOn f M.E
hX : autoParam (X ⊆ M.E) _auto✝
⊢ (M.map f hf).er (f '' X) = M.er X
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✝ : α
β : Type u_3
f : α → β
M : Matroid α
hf : InjOn f M.E
hX : autoParam (X ⊆ M.E) _auto✝
I : Set α
hI : M.Basis I X
⊢ (M.map f hf).er (f '' X) = M.er X
Theorem: Matroid.er_map_eq
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✝ : α
β : Type u_3
f : α → β
M : Matroid α
hf : InjOn f M.E
hX : autoParam (X ⊆ M.E) _auto✝
I : Set α
hI : M.Basis I X
⊢ (M.map f hf).er (f '' X) = M.er X
Tactic:
rw [hI.er_eq_encard, (hI.map hf).er_eq_encard, (hf.mono hI.indep.subset_ground).encard_image]
Proof state after:
no goals
Theorem: Matroid.er_univ_eq
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 α
⊢ M.er univ = M.erk
Tactic:
rw [← er_inter_ground_eq, univ_inter, erk_eq_er_ground]
Proof state after:
no goals
Theorem: Matroid.er_empty
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 α
⊢ M.er ∅ = 0
Tactic:
rw [← M.empty_indep.basis_self.encard, encard_empty]
Proof state after:
no goals
Theorem: Matroid.er_cl_eq
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.er (M.cl X) = M.er X
Tactic:
rw [← cl_inter_ground, ← M.er_inter_ground_eq X]
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 α
X : Set α
⊢ M.er (M.cl (X ∩ M.E)) = M.er (X ∩ M.E)
Theorem: Matroid.er_cl_eq
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.er (M.cl (X ∩ M.E)) = M.er (X ∩ M.E)
Tactic:
obtain ⟨I, hI⟩ := M.exists_basis (X ∩ M.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 α
X I : Set α
hI : M.Basis I (X ∩ M.E)
⊢ M.er (M.cl (X ∩ M.E)) = M.er (X ∩ M.E)
Theorem: Matroid.er_cl_eq
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 α
hI : M.Basis I (X ∩ M.E)
⊢ M.er (M.cl (X ∩ M.E)) = M.er (X ∩ M.E)
Tactic:
rw [← hI.er, ← hI.cl_eq_cl, hI.indep.basis_cl.er]
Proof state after:
no goals
Theorem: Matroid.er_union_cl_right_eq
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 Y : Set α
⊢ M.er (X ∪ M.cl Y) = M.er (X ∪ Y)
Tactic:
rw [← er_cl_eq, cl_union_cl_right_eq, er_cl_eq]
Proof state after:
no goals
Theorem: Matroid.er_union_cl_left_eq
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 Y : Set α
⊢ M.er (M.cl X ∪ Y) = M.er (X ∪ Y)
Tactic:
rw [← er_cl_eq, cl_union_cl_left_eq, er_cl_eq]
Proof state after:
no goals
Theorem: Matroid.er_insert_cl_eq
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 (M.cl X)) = M.er (insert e X)
Tactic:
rw [← union_singleton, er_union_cl_left_eq, union_singleton]
Proof state after:
no goals
Theorem: Matroid.restrict_er_eq'
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 α
R X : Set α
⊢ (M ↾ R).er X = M.er (X ∩ R)
Tactic:
obtain ⟨I, hI⟩ := (M ↾ R).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 α
R X I : Set α
hI : (M ↾ R).Basis' I X
⊢ (M ↾ R).er X = M.er (X ∩ R)
Theorem: Matroid.restrict_er_eq'
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 α
R X I : Set α
hI : (M ↾ R).Basis' I X
⊢ (M ↾ R).er X = M.er (X ∩ R)
Tactic:
rw [hI.er_eq_encard]
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 α
R X I : Set α
hI : (M ↾ R).Basis' I X
⊢ I.encard = M.er (X ∩ R)
Theorem: Matroid.restrict_er_eq'
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 α
R X I : Set α
hI : (M ↾ R).Basis' I X
⊢ I.encard = M.er (X ∩ R)
Tactic:
rw [basis'_iff_basis_inter_ground, basis_restrict_iff', restrict_ground_eq] at hI
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 α
R X I : Set α
hI : M.Basis I (X ∩ R ∩ M.E) ∧ X ∩ R ⊆ R
⊢ I.encard = M.er (X ∩ R)
Theorem: Matroid.restrict_er_eq'
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 α
R X I : Set α
hI : M.Basis I (X ∩ R ∩ M.E) ∧ X ∩ R ⊆ R
⊢ I.encard = M.er (X ∩ R)
Tactic:
rw [← er_inter_ground_eq, ← hI.1.er_eq_encard]
Proof state after:
no goals
Theorem: Matroid.restrict_er_eq
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 α
h : X ⊆ R
⊢ (M ↾ R).er X = M.er X
Tactic:
rw [restrict_er_eq', inter_eq_self_of_subset_left h]
Proof state after:
no goals
Theorem: Matroid.er_lt_top_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 : α
M : Matroid α
hX : X.Finite
⊢ M.er X < ⊤
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 α
hX : X.Finite
I : Set α
hI : M.Basis' I X
⊢ M.er X < ⊤
Theorem: Matroid.er_lt_top_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 : α
M : Matroid α
hX : X.Finite
I : Set α
hI : M.Basis' I X
⊢ M.er X < ⊤
Tactic:
rw [hI.er_eq_encard, encard_lt_top_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 α
hX : X.Finite
I : Set α
hI : M.Basis' I X
⊢ I.Finite
Theorem: Matroid.er_lt_top_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 : α
M : Matroid α
hX : X.Finite
I : Set α
hI : M.Basis' I X
⊢ I.Finite
Tactic:
exact hX.subset hI.subset
Proof state after:
no goals
Theorem: Matroid.Basis'.er_eq_er_union
Proof state before:
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y✝ Y' Z R : Set α
n : ℕ∞
e f : α
hIX : M.Basis' I X
Y : Set α
⊢ M.er (I ∪ Y) = M.er (X ∪ Y)
Tactic:
rw [← er_union_cl_left_eq, hIX.cl_eq_cl, er_union_cl_left_eq]
Proof state after:
no goals
Theorem: Matroid.Basis'.er_eq_er_insert
Proof state before:
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e✝ f : α
hIX : M.Basis' I X
e : α
⊢ M.er (insert e I) = M.er (insert e X)
Tactic:
rw [← union_singleton, hIX.er_eq_er_union, union_singleton]
Proof state after:
no goals
Theorem: Matroid.Basis.er_eq_er_insert
Proof state before:
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e✝ f : α
hIX : M.Basis I X
e : α
⊢ M.er (insert e I) = M.er (insert e X)
Tactic:
rw [← union_singleton, hIX.er_eq_er_union, union_singleton]
Proof state after:
no goals
Theorem: Matroid.er_le_encard
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.er X ≤ X.encard
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 I : Set α
hI : M.Basis' I X
⊢ M.er X ≤ X.encard
Theorem: Matroid.er_le_encard
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 α
hI : M.Basis' I X
⊢ M.er X ≤ X.encard
Tactic:
rw [hI.er_eq_encard]
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 α
hI : M.Basis' I X
⊢ I.encard ≤ X.encard
Theorem: Matroid.er_le_encard
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 α
hI : M.Basis' I X
⊢ I.encard ≤ X.encard
Tactic:
exact encard_mono hI.subset
Proof state after:
no goals
Theorem: Matroid.er_mono
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 α
⊢ Monotone M.er
Tactic:
rintro X Y (hXY : 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 : α
M : Matroid α
X Y : Set α
hXY : X ⊆ Y
⊢ M.er X ≤ M.er Y
Theorem: Matroid.er_mono
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 Y : Set α
hXY : X ⊆ Y
⊢ M.er X ≤ M.er Y
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 Y : Set α
hXY : X ⊆ Y
I : Set α
hI : M.Basis' I X
⊢ M.er X ≤ M.er Y
Theorem: Matroid.er_mono
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 Y : Set α
hXY : X ⊆ Y
I : Set α
hI : M.Basis' I X
⊢ M.er X ≤ M.er Y
Tactic:
obtain ⟨J, hJ, hIJ⟩ := hI.indep.subset_basis'_of_subset (hI.subset.trans hXY)
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 : α
M : Matroid α
X Y : Set α
hXY : X ⊆ Y
I : Set α
hI : M.Basis' I X
J : Set α
hJ : M.Basis' J Y
hIJ : I ⊆ J
⊢ M.er X ≤ M.er Y
Theorem: Matroid.er_mono
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 : α
M : Matroid α
X Y : Set α
hXY : X ⊆ Y
I : Set α
hI : M.Basis' I X
J : Set α
hJ : M.Basis' J Y
hIJ : I ⊆ J
⊢ M.er X ≤ M.er Y
Tactic:
rw [hI.er_eq_encard, hJ.er_eq_encard]
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 : α
M : Matroid α
X Y : Set α
hXY : X ⊆ Y
I : Set α
hI : M.Basis' I X
J : Set α
hJ : M.Basis' J Y
hIJ : I ⊆ J
⊢ I.encard ≤ J.encard
Theorem: Matroid.er_mono
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 : α
M : Matroid α
X Y : Set α
hXY : X ⊆ Y
I : Set α
hI : M.Basis' I X
J : Set α
hJ : M.Basis' J Y
hIJ : I ⊆ J
⊢ I.encard ≤ J.encard
Tactic:
exact encard_mono hIJ
Proof state after:
no goals
Theorem: Matroid.er_le_erk
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.er X ≤ M.erk
Tactic:
rw [erk_eq_er_ground, ← er_inter_ground_eq]
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 α
X : Set α
⊢ M.er (X ∩ M.E) ≤ M.er M.E
Theorem: Matroid.er_le_erk
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.er (X ∩ M.E) ≤ M.er M.E
Tactic:
exact M.er_mono inter_subset_right
Proof state after:
no goals
Theorem: Matroid.le_er_iff
Proof state before:
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
⊢ n ≤ M.er X ↔ ∃ I ⊆ X, M.Indep I ∧ I.encard = n
Tactic:
refine' ⟨fun h ↦ _, fun ⟨I, hIX, hI, hIc⟩ ↦ _⟩
Proof state after:
case refine'_1
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
h : n ≤ M.er X
⊢ ∃ I ⊆ X, M.Indep I ∧ I.encard = n

case refine'_2
α : Type u_1
ι : Type u_2
M N : Matroid α
I✝ B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
x✝ : ∃ I ⊆ X, M.Indep I ∧ I.encard = n
I : Set α
hIX : I ⊆ X
hI : M.Indep I
hIc : I.encard = n
⊢ n ≤ M.er X
Theorem: Matroid.le_er_iff
Proof state before:
case refine'_2
α : Type u_1
ι : Type u_2
M N : Matroid α
I✝ B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
x✝ : ∃ I ⊆ X, M.Indep I ∧ I.encard = n
I : Set α
hIX : I ⊆ X
hI : M.Indep I
hIc : I.encard = n
⊢ n ≤ M.er X
Tactic:
rw [← hIc, ← hI.er]
Proof state after:
case refine'_2
α : Type u_1
ι : Type u_2
M N : Matroid α
I✝ B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
x✝ : ∃ I ⊆ X, M.Indep I ∧ I.encard = n
I : Set α
hIX : I ⊆ X
hI : M.Indep I
hIc : I.encard = n
⊢ M.er I ≤ M.er X
Theorem: Matroid.le_er_iff
Proof state before:
case refine'_2
α : Type u_1
ι : Type u_2
M N : Matroid α
I✝ B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
x✝ : ∃ I ⊆ X, M.Indep I ∧ I.encard = n
I : Set α
hIX : I ⊆ X
hI : M.Indep I
hIc : I.encard = n
⊢ M.er I ≤ M.er X
Tactic:
exact M.er_mono hIX
Proof state after:
no goals
Theorem: Matroid.le_er_iff
Proof state before:
case refine'_1
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
h : n ≤ M.er X
⊢ ∃ I ⊆ X, M.Indep I ∧ I.encard = n
Tactic:
obtain ⟨J, hJ⟩ := M.exists_basis' X
Proof state after:
case refine'_1.intro
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
h : n ≤ M.er X
J : Set α
hJ : M.Basis' J X
⊢ ∃ I ⊆ X, M.Indep I ∧ I.encard = n
Theorem: Matroid.le_er_iff
Proof state before:
case refine'_1.intro
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
h : n ≤ M.er X
J : Set α
hJ : M.Basis' J X
⊢ ∃ I ⊆ X, M.Indep I ∧ I.encard = n
Tactic:
rw [← hJ.encard] at h
Proof state after:
case refine'_1.intro
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
J : Set α
h : n ≤ J.encard
hJ : M.Basis' J X
⊢ ∃ I ⊆ X, M.Indep I ∧ I.encard = n
Theorem: Matroid.le_er_iff
Proof state before:
case refine'_1.intro
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
J : Set α
h : n ≤ J.encard
hJ : M.Basis' J X
⊢ ∃ I ⊆ X, M.Indep I ∧ I.encard = n
Tactic:
obtain ⟨I, hIJ, rfl⟩ :=  exists_subset_encard_eq h
Proof state after:
case refine'_1.intro.intro.intro
α : Type u_1
ι : Type u_2
M N : Matroid α
I✝ B X X' Y Y' Z R : Set α
e f : α
J : Set α
hJ : M.Basis' J X
I : Set α
hIJ : I ⊆ J
h : I.encard ≤ J.encard
⊢ ∃ I_1 ⊆ X, M.Indep I_1 ∧ I_1.encard = I.encard
Theorem: Matroid.le_er_iff
Proof state before:
case refine'_1.intro.intro.intro
α : Type u_1
ι : Type u_2
M N : Matroid α
I✝ B X X' Y Y' Z R : Set α
e f : α
J : Set α
hJ : M.Basis' J X
I : Set α
hIJ : I ⊆ J
h : I.encard ≤ J.encard
⊢ ∃ I_1 ⊆ X, M.Indep I_1 ∧ I_1.encard = I.encard
Tactic:
exact ⟨_, hIJ.trans hJ.subset, hJ.indep.subset hIJ, rfl⟩
Proof state after:
no goals
Theorem: Matroid.er_le_iff
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.er X ≤ n ↔ ∀ {I : Set α}, I ⊆ X → M.Indep I → I.encard ≤ n
Tactic:
refine ⟨fun h I hIX hI ↦ (hI.er.symm.trans_le ((M.er_mono hIX).trans h)), 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 : α
h : ∀ {I : Set α}, I ⊆ X → M.Indep I → I.encard ≤ n
⊢ M.er X ≤ n
Theorem: Matroid.er_le_iff
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 : ∀ {I : Set α}, I ⊆ X → M.Indep I → I.encard ≤ n
⊢ M.er X ≤ n
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 : ∀ {I : Set α}, I ⊆ X → M.Indep I → I.encard ≤ n
I : Set α
hI : M.Basis' I X
⊢ M.er X ≤ n
Theorem: Matroid.er_le_iff
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 : ∀ {I : Set α}, I ⊆ X → M.Indep I → I.encard ≤ n
I : Set α
hI : M.Basis' I X
⊢ M.er X ≤ n
Tactic:
rw [← hI.encard]
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 : ∀ {I : Set α}, I ⊆ X → M.Indep I → I.encard ≤ n
I : Set α
hI : M.Basis' I X
⊢ I.encard ≤ n
Theorem: Matroid.er_le_iff
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 : ∀ {I : Set α}, I ⊆ X → M.Indep I → I.encard ≤ n
I : Set α
hI : M.Basis' I X
⊢ I.encard ≤ n
Tactic:
exact h hI.subset hI.indep
Proof state after:
no goals
Theorem: Matroid.Indep.encard_le_er_of_subset
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
⊢ I.encard ≤ M.er X
Tactic:
rw [← 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
⊢ M.er I ≤ M.er X
Theorem: Matroid.Indep.encard_le_er_of_subset
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
⊢ M.er I ≤ M.er X
Tactic:
exact M.er_mono hIX
Proof state after:
no goals
Theorem: Matroid.Indep.encard_le_erk
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
⊢ I.encard ≤ M.erk
Tactic:
rw [← hI.er, erk_eq_er_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 : α
hI : M.Indep I
⊢ M.er I ≤ M.er M.E
Theorem: Matroid.Indep.encard_le_erk
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
⊢ M.er I ≤ M.er M.E
Tactic:
exact M.er_mono hI.subset_ground
Proof state after:
no goals
Theorem: Matroid.er_inter_add_er_union_le_er_add_er
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 Y : Set α
⊢ M.er (X ∩ Y) + M.er (X ∪ Y) ≤ M.er X + M.er Y
Tactic:
obtain ⟨Ii, hIi⟩ := M.exists_basis' (X ∩ Y)
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 Y Ii : Set α
hIi : M.Basis' Ii (X ∩ Y)
⊢ M.er (X ∩ Y) + M.er (X ∪ Y) ≤ M.er X + M.er Y
Theorem: Matroid.er_inter_add_er_union_le_er_add_er
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 Y Ii : Set α
hIi : M.Basis' Ii (X ∩ Y)
⊢ M.er (X ∩ Y) + M.er (X ∪ Y) ≤ M.er X + M.er Y
Tactic:
obtain ⟨IX, hIX, hIX'⟩ :=
  hIi.indep.subset_basis'_of_subset (hIi.subset.trans inter_subset_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 : α
M : Matroid α
X Y Ii : Set α
hIi : M.Basis' Ii (X ∩ Y)
IX : Set α
hIX : M.Basis' IX X
hIX' : Ii ⊆ IX
⊢ M.er (X ∩ Y) + M.er (X ∪ Y) ≤ M.er X + M.er Y
Theorem: Matroid.er_inter_add_er_union_le_er_add_er
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 : α
M : Matroid α
X Y Ii : Set α
hIi : M.Basis' Ii (X ∩ Y)
IX : Set α
hIX : M.Basis' IX X
hIX' : Ii ⊆ IX
⊢ M.er (X ∩ Y) + M.er (X ∪ Y) ≤ M.er X + M.er Y
Tactic:
obtain ⟨IY, hIY, hIY'⟩ :=
  hIi.indep.subset_basis'_of_subset (hIi.subset.trans inter_subset_right)
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 : α
M : Matroid α
X Y Ii : Set α
hIi : M.Basis' Ii (X ∩ Y)
IX : Set α
hIX : M.Basis' IX X
hIX' : Ii ⊆ IX
IY : Set α
hIY : M.Basis' IY Y
hIY' : Ii ⊆ IY
⊢ M.er (X ∩ Y) + M.er (X ∪ Y) ≤ M.er X + M.er Y
Theorem: Matroid.er_inter_add_er_union_le_er_add_er
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 : α
M : Matroid α
X Y Ii : Set α
hIi : M.Basis' Ii (X ∩ Y)
IX : Set α
hIX : M.Basis' IX X
hIX' : Ii ⊆ IX
IY : Set α
hIY : M.Basis' IY Y
hIY' : Ii ⊆ IY
⊢ M.er (X ∩ Y) + M.er (X ∪ Y) ≤ M.er X + M.er Y
Tactic:
rw [← hIX.er_eq_er_union, union_comm, ← hIY.er_eq_er_union, ← hIi.encard, ← hIX.encard,
  ← hIY.encard, union_comm, ← encard_union_add_encard_inter, add_comm]
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 : α
M : Matroid α
X Y Ii : Set α
hIi : M.Basis' Ii (X ∩ Y)
IX : Set α
hIX : M.Basis' IX X
hIX' : Ii ⊆ IX
IY : Set α
hIY : M.Basis' IY Y
hIY' : Ii ⊆ IY
⊢ M.er (IX ∪ IY) + Ii.encard ≤ (IX ∪ IY).encard + (IX ∩ IY).encard
Theorem: Matroid.er_inter_add_er_union_le_er_add_er
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 : α
M : Matroid α
X Y Ii : Set α
hIi : M.Basis' Ii (X ∩ Y)
IX : Set α
hIX : M.Basis' IX X
hIX' : Ii ⊆ IX
IY : Set α
hIY : M.Basis' IY Y
hIY' : Ii ⊆ IY
⊢ M.er (IX ∪ IY) + Ii.encard ≤ (IX ∪ IY).encard + (IX ∩ IY).encard
Tactic:
exact add_le_add (er_le_encard _ _) (encard_mono (subset_inter hIX' hIY'))
Proof state after:
no goals
Theorem: Matroid.er_eq_er_diff_er_le_zero
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 : Set α
hY : M.er Y ≤ 0
⊢ M.er (X \ Y) = M.er X
Tactic:
rw [← er_eq_er_union_er_le_zero (X \ Y) hY, diff_union_self, er_eq_er_union_er_le_zero _ hY]
Proof state after:
no goals