internlm/Lean-Github huggingface dataset:
Theorem: Matroid.rFin_ground_iff_finiteRk
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.rFin M.E ↔ M.FiniteRk
Tactic:
obtain ⟨B, hB⟩ := M.exists_base
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 : α
B : Set α
hB : M.Base B
⊢ M.rFin M.E ↔ M.FiniteRk
Theorem: Matroid.rFin_ground_iff_finiteRk
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 : α
B : Set α
hB : M.Base B
⊢ M.rFin M.E ↔ M.FiniteRk
Tactic:
use fun h => ⟨⟨B, hB, h.finite_of_indep_subset hB.indep hB.subset_ground⟩⟩
Proof state after:
case mpr
α : Type u_1
ι : Type u_2
M N : Matroid α
I B✝ X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
B : Set α
hB : M.Base B
⊢ M.FiniteRk → M.rFin M.E
Theorem: Matroid.rFin_ground_iff_finiteRk
Proof state before:
case mpr
α : Type u_1
ι : Type u_2
M N : Matroid α
I B✝ X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
B : Set α
hB : M.Base B
⊢ M.FiniteRk → M.rFin M.E
Tactic:
simp_rw [rFin_iff (rfl.subset), basis_ground_iff]
Proof state after:
case mpr
α : Type u_1
ι : Type u_2
M N : Matroid α
I B✝ X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
B : Set α
hB : M.Base B
⊢ M.FiniteRk → ∃ I, M.Base I ∧ I.Finite
Theorem: Matroid.rFin_ground_iff_finiteRk
Proof state before:
case mpr
α : Type u_1
ι : Type u_2
M N : Matroid α
I B✝ X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
B : Set α
hB : M.Base B
⊢ M.FiniteRk → ∃ I, M.Base I ∧ I.Finite
Tactic:
exact fun ⟨h⟩ ↦ h
Proof state after:
no goals
Theorem: Matroid.rFin_ground
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 α
inst✝ : M.FiniteRk
⊢ M.rFin M.E
Tactic:
rwa [rFin_ground_iff_finiteRk]
Proof state after:
no goals
Theorem: Matroid.erk_lt_top
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 α
inst✝ : M.FiniteRk
⊢ M.erk < ⊤
Tactic:
rw [erk_eq_er_ground, er_lt_top_iff]
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 α
inst✝ : M.FiniteRk
⊢ M.rFin M.E
Theorem: Matroid.erk_lt_top
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 α
inst✝ : M.FiniteRk
⊢ M.rFin M.E
Tactic:
exact M.rFin_ground
Proof state after:
no goals
Theorem: Matroid.rFin.indep_of_encard_le_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 : α
hX : M.rFin I
h : I.encard ≤ M.er I
⊢ M.Indep I
Tactic:
rw [indep_iff_er_eq_encard_of_finite _]
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 : M.rFin I
h : I.encard ≤ M.er I
⊢ M.er I = I.encard

α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
hX : M.rFin I
h : I.encard ≤ M.er I
⊢ I.Finite
Theorem: Matroid.rFin.indep_of_encard_le_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 : α
hX : M.rFin I
h : I.encard ≤ M.er I
⊢ I.Finite
Tactic:
simpa using h.trans_lt hX.lt
Proof state after:
no goals
Theorem: Matroid.rFin.indep_of_encard_le_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 : α
hX : M.rFin I
h : I.encard ≤ M.er I
⊢ M.er I = I.encard
Tactic:
exact (M.er_le_encard I).antisymm h
Proof state after:
no goals
Theorem: Matroid.rFin.to_cl
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.rFin X
⊢ M.rFin (M.cl X)
Tactic:
rwa [← er_lt_top_iff, er_cl_eq]
Proof state after:
no goals
Theorem: Matroid.rFin_cl_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.rFin (M.cl X) ↔ M.rFin X
Tactic:
rw [← er_ne_top_iff, er_cl_eq, er_ne_top_iff]
Proof state after:
no goals
Theorem: Matroid.rFin.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 : α
hX : M.rFin X
hY : M.rFin Y
⊢ M.rFin (X ∪ Y)
Tactic:
rw [← er_lt_top_iff] at *
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 : M.er X < ⊤
hY : M.er Y < ⊤
⊢ M.er (X ∪ Y) < ⊤
Theorem: Matroid.rFin.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 : α
hX : M.er X < ⊤
hY : M.er Y < ⊤
⊢ M.er (X ∪ Y) < ⊤
Tactic:
apply (M.er_union_le_er_add_er X Y).trans_lt
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 : M.er X < ⊤
hY : M.er Y < ⊤
⊢ M.er X + M.er Y < ⊤
Theorem: Matroid.rFin.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 : α
hX : M.er X < ⊤
hY : M.er Y < ⊤
⊢ M.er X + M.er Y < ⊤
Tactic:
rw [WithTop.add_lt_top]
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 : M.er X < ⊤
hY : M.er Y < ⊤
⊢ M.er X < ⊤ ∧ M.er Y < ⊤
Theorem: Matroid.rFin.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 : α
hX : M.er X < ⊤
hY : M.er Y < ⊤
⊢ M.er X < ⊤ ∧ M.er Y < ⊤
Tactic:
exact ⟨hX, hY⟩
Proof state after:
no goals
Theorem: Matroid.rFin.rFin_diff_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 : α
hX : M.rFin X
⊢ M.rFin (Y \ X) ↔ M.rFin Y
Tactic:
rw [← hX.rFin_union_iff, union_diff_self, hX.rFin_union_iff]
Proof state after:
no goals
Theorem: Matroid.rFin.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 : α
hX : M.rFin X
e : α
⊢ M.rFin (Insert.insert e X)
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 : α
hX : M.rFin X
e : α
⊢ M.rFin (X ∪ {e})
Theorem: Matroid.rFin.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 : α
hX : M.rFin X
e : α
⊢ M.rFin (X ∪ {e})
Tactic:
exact hX.union (M.rFin_singleton e)
Proof state after:
no goals
Theorem: Matroid.rFin_insert_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.rFin (insert e X) ↔ M.rFin X
Tactic:
rw [← singleton_union, (M.rFin_singleton e).rFin_union_iff]
Proof state after:
no goals
Theorem: Matroid.rFin_diff_singleton_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.rFin (X \ {e}) ↔ M.rFin X
Tactic:
rw [(M.rFin_singleton e).rFin_diff_iff]
Proof state after:
no goals
Theorem: Matroid.to_rFin
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 α
inst✝ : M.FiniteRk
X : Set α
⊢ M.rFin 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 α
inst✝ : M.FiniteRk
X I : Set α
hI : M.Basis' I X
⊢ M.rFin X
Theorem: Matroid.to_rFin
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 α
inst✝ : M.FiniteRk
X I : Set α
hI : M.Basis' I X
⊢ M.rFin X
Tactic:
rw [← er_lt_top_iff, 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 α
inst✝ : M.FiniteRk
X I : Set α
hI : M.Basis' I X
⊢ I.Finite
Theorem: Matroid.to_rFin
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 α
inst✝ : M.FiniteRk
X I : Set α
hI : M.Basis' I X
⊢ I.Finite
Tactic:
exact hI.indep.finite_of_subset_rFin hI.indep.subset_ground M.rFin_ground
Proof state after:
no goals
Theorem: Matroid.rFin.cl_eq_cl_of_subset_of_er_ge_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 : α
hX : M.rFin X
hXY : X ⊆ Y
hr : M.er Y ≤ M.er X
⊢ M.cl X = M.cl 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 : α
hX : M.rFin X
hXY : X ⊆ Y
hr : M.er Y ≤ M.er X
I : Set α
hI : M.Basis' I X
⊢ M.cl X = M.cl Y
Theorem: Matroid.rFin.cl_eq_cl_of_subset_of_er_ge_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 : α
hX : M.rFin X
hXY : X ⊆ Y
hr : M.er Y ≤ M.er X
I : Set α
hI : M.Basis' I X
⊢ M.cl X = M.cl 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 : α
hX : M.rFin X
hXY : X ⊆ Y
hr : M.er Y ≤ M.er X
I : Set α
hI : M.Basis' I X
J : Set α
hJ : M.Basis' J Y
hIJ : I ⊆ J
⊢ M.cl X = M.cl Y
Theorem: Matroid.rFin.cl_eq_cl_of_subset_of_er_ge_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 : α
hX : M.rFin X
hXY : X ⊆ Y
hr : M.er Y ≤ M.er X
I : Set α
hI : M.Basis' I X
J : Set α
hJ : M.Basis' J Y
hIJ : I ⊆ J
⊢ M.cl X = M.cl Y
Tactic:
rw [hI.er_eq_encard, hJ.er_eq_encard] at hr
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 : α
hX : M.rFin X
hXY : X ⊆ Y
I : Set α
hI : M.Basis' I X
J : Set α
hr : J.encard ≤ I.encard
hJ : M.Basis' J Y
hIJ : I ⊆ J
⊢ M.cl X = M.cl Y
Theorem: Matroid.rFin.cl_eq_cl_of_subset_of_er_ge_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 : α
hX : M.rFin X
hXY : X ⊆ Y
I : Set α
hI : M.Basis' I X
J : Set α
hr : J.encard ≤ I.encard
hJ : M.Basis' J Y
hIJ : I ⊆ J
⊢ M.cl X = M.cl Y
Tactic:
rw [← cl_inter_ground, ← M.cl_inter_ground Y, ← hI.basis_inter_ground.cl_eq_cl,
  ← hJ.basis_inter_ground.cl_eq_cl, Finite.eq_of_subset_of_encard_le'
    (hI.indep.finite_of_subset_rFin hI.subset hX) hIJ hr]
Proof state after:
no goals
Theorem: Matroid.er_union_eq_of_subset_of_er_le_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 : α
Z : Set α
hXY : X ⊆ Y
hr : M.er Y ≤ M.er X
⊢ M.er (X ∪ Z) = M.er (Y ∪ Z)
Tactic:
obtain hX' | hX' := em (M.rFin X)
Proof state after:
case inl
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z✝ R : Set α
n : ℕ∞
e f : α
Z : Set α
hXY : X ⊆ Y
hr : M.er Y ≤ M.er X
hX' : M.rFin X
⊢ M.er (X ∪ Z) = M.er (Y ∪ Z)

case inr
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z✝ R : Set α
n : ℕ∞
e f : α
Z : Set α
hXY : X ⊆ Y
hr : M.er Y ≤ M.er X
hX' : ¬M.rFin X
⊢ M.er (X ∪ Z) = M.er (Y ∪ Z)
Theorem: Matroid.er_union_eq_of_subset_of_er_le_er
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 : α
Z : Set α
hXY : X ⊆ Y
hr : M.er Y ≤ M.er X
hX' : ¬M.rFin X
⊢ M.er (X ∪ Z) = M.er (Y ∪ Z)
Tactic:
rw [er_eq_top_iff.2, er_eq_top_iff.2]
Proof state after:
case inr
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z✝ R : Set α
n : ℕ∞
e f : α
Z : Set α
hXY : X ⊆ Y
hr : M.er Y ≤ M.er X
hX' : ¬M.rFin X
⊢ ¬M.rFin (Y ∪ Z)

case inr
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z✝ R : Set α
n : ℕ∞
e f : α
Z : Set α
hXY : X ⊆ Y
hr : M.er Y ≤ M.er X
hX' : ¬M.rFin X
⊢ ¬M.rFin (X ∪ Z)
Theorem: Matroid.er_union_eq_of_subset_of_er_le_er
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 : α
Z : Set α
hXY : X ⊆ Y
hr : M.er Y ≤ M.er X
hX' : ¬M.rFin X
⊢ ¬M.rFin (X ∪ Z)
Tactic:
exact not_rFin_of_er_ge hX' (M.er_mono subset_union_left)
Proof state after:
no goals
Theorem: Matroid.er_union_eq_of_subset_of_er_le_er
Proof state before:
case inl
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z✝ R : Set α
n : ℕ∞
e f : α
Z : Set α
hXY : X ⊆ Y
hr : M.er Y ≤ M.er X
hX' : M.rFin X
⊢ M.er (X ∪ Z) = M.er (Y ∪ Z)
Tactic:
rw [← er_union_cl_left_eq, hX'.cl_eq_cl_of_subset_of_er_ge_er hXY hr, er_union_cl_left_eq]
Proof state after:
no goals
Theorem: Matroid.er_union_eq_of_subset_of_er_le_er
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 : α
Z : Set α
hXY : X ⊆ Y
hr : M.er Y ≤ M.er X
hX' : ¬M.rFin X
⊢ ¬M.rFin (Y ∪ Z)
Tactic:
exact not_rFin_of_er_ge hX' (M.er_mono (subset_union_of_subset_left hXY _))
Proof state after:
no goals
Theorem: Matroid.er_union_eq_of_subsets_of_ers_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 : α
hX : X ⊆ X'
hY : Y ⊆ Y'
hXX' : M.er X' ≤ M.er X
hYY' : M.er Y' ≤ M.er Y
⊢ M.er (X ∪ Y) = M.er (X' ∪ Y')
Tactic:
rw [er_union_eq_of_subset_of_er_le_er _ hX hXX', union_comm,
  er_union_eq_of_subset_of_er_le_er _ hY hYY', union_comm]
Proof state after:
no goals
Theorem: Matroid.rFin.basis_of_subset_cl_of_subset_of_encard_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 : α
hX : M.rFin X
hXI : X ⊆ M.cl I
hIX : I ⊆ X
hI : I.encard ≤ M.er X
⊢ M.Basis I X
Tactic:
obtain ⟨J, hJ⟩ := M.exists_basis (I ∩ 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 : α
hX : M.rFin X
hXI : X ⊆ M.cl I
hIX : I ⊆ X
hI : I.encard ≤ M.er X
J : Set α
hJ : M.Basis J (I ∩ M.E)
⊢ M.Basis I X
Theorem: Matroid.rFin.basis_of_subset_cl_of_subset_of_encard_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 : α
hX : M.rFin X
hXI : X ⊆ M.cl I
hIX : I ⊆ X
hI : I.encard ≤ M.er X
J : Set α
hJ : M.Basis J (I ∩ M.E)
⊢ M.Basis I X
Tactic:
have hIJ := hJ.subset.trans inter_subset_left
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 : α
hX : M.rFin X
hXI : X ⊆ M.cl I
hIX : I ⊆ X
hI : I.encard ≤ M.er X
J : Set α
hJ : M.Basis J (I ∩ M.E)
hIJ : J ⊆ I
⊢ M.Basis I X
Theorem: Matroid.rFin.basis_of_subset_cl_of_subset_of_encard_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 : α
hX : M.rFin X
hXI : X ⊆ M.cl I
hIX : I ⊆ X
hI : I.encard ≤ M.er X
J : Set α
hJ : M.Basis J (I ∩ M.E)
hIJ : J ⊆ I
⊢ M.Basis I X
Tactic:
rw [← cl_inter_ground] at hXI
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 : α
hX : M.rFin X
hXI : X ⊆ M.cl (I ∩ M.E)
hIX : I ⊆ X
hI : I.encard ≤ M.er X
J : Set α
hJ : M.Basis J (I ∩ M.E)
hIJ : J ⊆ I
⊢ M.Basis I X
Theorem: Matroid.rFin.basis_of_subset_cl_of_subset_of_encard_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 : α
hX : M.rFin X
hXI : X ⊆ M.cl (I ∩ M.E)
hIX : I ⊆ X
hI : I.encard ≤ M.er X
J : Set α
hJ : M.Basis J (I ∩ M.E)
hIJ : J ⊆ I
⊢ M.Basis I X
Tactic:
replace hXI := hXI.trans <| M.cl_subset_cl_of_subset_cl hJ.subset_cl
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 : α
hX : M.rFin X
hIX : I ⊆ X
hI : I.encard ≤ M.er X
J : Set α
hJ : M.Basis J (I ∩ M.E)
hIJ : J ⊆ I
hXI : X ⊆ M.cl J
⊢ M.Basis I X
Theorem: Matroid.rFin.basis_of_subset_cl_of_subset_of_encard_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 : α
hX : M.rFin X
hIX : I ⊆ X
hI : I.encard ≤ M.er X
J : Set α
hJ : M.Basis J (I ∩ M.E)
hIJ : J ⊆ I
hXI : X ⊆ M.cl J
⊢ M.Basis I X
Tactic:
have hJX := hJ.indep.basis_of_subset_of_subset_cl (hIJ.trans hIX) hXI
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 : α
hX : M.rFin X
hIX : I ⊆ X
hI : I.encard ≤ M.er X
J : Set α
hJ : M.Basis J (I ∩ M.E)
hIJ : J ⊆ I
hXI : X ⊆ M.cl J
hJX : M.Basis J X
⊢ M.Basis I X
Theorem: Matroid.rFin.basis_of_subset_cl_of_subset_of_encard_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 : α
hX : M.rFin X
hIX : I ⊆ X
hI : I.encard ≤ M.er X
J : Set α
hJ : M.Basis J (I ∩ M.E)
hIJ : J ⊆ I
hXI : X ⊆ M.cl J
hJX : M.Basis J X
⊢ M.Basis I X
Tactic:
rw [← hJX.encard] 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 : α
hX : M.rFin X
hIX : I ⊆ X
J : Set α
hI : I.encard ≤ J.encard
hJ : M.Basis J (I ∩ M.E)
hIJ : J ⊆ I
hXI : X ⊆ M.cl J
hJX : M.Basis J X
⊢ M.Basis I X
Theorem: Matroid.rFin.basis_of_subset_cl_of_subset_of_encard_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 : α
hX : M.rFin X
hIX : I ⊆ X
J : Set α
hI : I.encard ≤ J.encard
hJ : M.Basis J (I ∩ M.E)
hIJ : J ⊆ I
hXI : X ⊆ M.cl J
hJX : M.Basis J X
⊢ M.Basis I X
Tactic:
rwa [← Finite.eq_of_subset_of_encard_le' (hX.finite_of_basis hJX) hIJ hI]
Proof state after:
no goals
Theorem: Matroid.rFin.iUnion
Proof state before:
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
inst✝ : Fintype ι
Xs : ι → Set α
h : ∀ (i : ι), M.rFin (Xs i)
⊢ M.rFin (⋃ i, Xs i)
Tactic:
choose Is hIs using fun i ↦ M.exists_basis' (Xs i)
Proof state after:
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
inst✝ : Fintype ι
Xs : ι → Set α
h : ∀ (i : ι), M.rFin (Xs i)
Is : ι → Set α
hIs : ∀ (i : ι), M.Basis' (Is i) (Xs i)
⊢ M.rFin (⋃ i, Xs i)
Theorem: Matroid.rFin.iUnion
Proof state before:
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
inst✝ : Fintype ι
Xs : ι → Set α
h : ∀ (i : ι), M.rFin (Xs i)
Is : ι → Set α
hIs : ∀ (i : ι), M.Basis' (Is i) (Xs i)
⊢ M.rFin (⋃ i, Xs i)
Tactic:
have hfin : (⋃ i, Is i).Finite := finite_iUnion <| fun i ↦ (h i).finite_of_basis' (hIs i)
Proof state after:
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
inst✝ : Fintype ι
Xs : ι → Set α
h : ∀ (i : ι), M.rFin (Xs i)
Is : ι → Set α
hIs : ∀ (i : ι), M.Basis' (Is i) (Xs i)
hfin : (⋃ i, Is i).Finite
⊢ M.rFin (⋃ i, Xs i)
Theorem: Matroid.rFin.iUnion
Proof state before:
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
inst✝ : Fintype ι
Xs : ι → Set α
h : ∀ (i : ι), M.rFin (Xs i)
Is : ι → Set α
hIs : ∀ (i : ι), M.Basis' (Is i) (Xs i)
hfin : (⋃ i, Is i).Finite
⊢ M.rFin (⋃ i, Xs i)
Tactic:
rw [← rFin_cl_iff]
Proof state after:
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
inst✝ : Fintype ι
Xs : ι → Set α
h : ∀ (i : ι), M.rFin (Xs i)
Is : ι → Set α
hIs : ∀ (i : ι), M.Basis' (Is i) (Xs i)
hfin : (⋃ i, Is i).Finite
⊢ M.rFin (M.cl (⋃ i, Xs i))
Theorem: Matroid.rFin.iUnion
Proof state before:
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
inst✝ : Fintype ι
Xs : ι → Set α
h : ∀ (i : ι), M.rFin (Xs i)
Is : ι → Set α
hIs : ∀ (i : ι), M.Basis' (Is i) (Xs i)
hfin : (⋃ i, Is i).Finite
⊢ M.rFin (M.cl (⋃ i, Xs i))
Tactic:
have hcl := (M.rFin_of_finite hfin).to_cl
Proof state after:
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
inst✝ : Fintype ι
Xs : ι → Set α
h : ∀ (i : ι), M.rFin (Xs i)
Is : ι → Set α
hIs : ∀ (i : ι), M.Basis' (Is i) (Xs i)
hfin : (⋃ i, Is i).Finite
hcl : M.rFin (M.cl (⋃ i, Is i))
⊢ M.rFin (M.cl (⋃ i, Xs i))
Theorem: Matroid.rFin.iUnion
Proof state before:
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
inst✝ : Fintype ι
Xs : ι → Set α
h : ∀ (i : ι), M.rFin (Xs i)
Is : ι → Set α
hIs : ∀ (i : ι), M.Basis' (Is i) (Xs i)
hfin : (⋃ i, Is i).Finite
hcl : M.rFin (M.cl (⋃ i, Is i))
⊢ M.rFin (M.cl (⋃ i, Xs i))
Tactic:
rw [← M.cl_iUnion_cl_eq_cl_iUnion]
Proof state after:
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
inst✝ : Fintype ι
Xs : ι → Set α
h : ∀ (i : ι), M.rFin (Xs i)
Is : ι → Set α
hIs : ∀ (i : ι), M.Basis' (Is i) (Xs i)
hfin : (⋃ i, Is i).Finite
hcl : M.rFin (M.cl (⋃ i, Is i))
⊢ M.rFin (M.cl (⋃ i, M.cl (Xs i)))
Theorem: Matroid.rFin.iUnion
Proof state before:
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
inst✝ : Fintype ι
Xs : ι → Set α
h : ∀ (i : ι), M.rFin (Xs i)
Is : ι → Set α
hIs : ∀ (i : ι), M.Basis' (Is i) (Xs i)
hfin : (⋃ i, Is i).Finite
hcl : M.rFin (M.cl (⋃ i, Is i))
⊢ M.rFin (M.cl (⋃ i, M.cl (Xs i)))
Tactic:
simp_rw [← (hIs _).cl_eq_cl, M.cl_iUnion_cl_eq_cl_iUnion]
Proof state after:
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
inst✝ : Fintype ι
Xs : ι → Set α
h : ∀ (i : ι), M.rFin (Xs i)
Is : ι → Set α
hIs : ∀ (i : ι), M.Basis' (Is i) (Xs i)
hfin : (⋃ i, Is i).Finite
hcl : M.rFin (M.cl (⋃ i, Is i))
⊢ M.rFin (M.cl (⋃ i, Is i))
Theorem: Matroid.rFin.iUnion
Proof state before:
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
inst✝ : Fintype ι
Xs : ι → Set α
h : ∀ (i : ι), M.rFin (Xs i)
Is : ι → Set α
hIs : ∀ (i : ι), M.Basis' (Is i) (Xs i)
hfin : (⋃ i, Is i).Finite
hcl : M.rFin (M.cl (⋃ i, Is i))
⊢ M.rFin (M.cl (⋃ i, Is i))
Tactic:
assumption
Proof state after:
no goals
Theorem: Matroid.rk_def
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.rk = M.r M.E
Tactic:
rw [rk,r,er,restrict_ground_eq_self]
Proof state after:
no goals
Theorem: Matroid.Base.ncard
Proof state before:
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
hB : M.Base B
⊢ B.ncard = M.rk
Tactic:
rw [rk_def, ← er_toNat_eq_r, ncard_def, hB.encard, erk_eq_er_ground]
Proof state after:
no goals
Theorem: Matroid.rFin.coe_r_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 : α
hX : M.rFin X
⊢ ↑(M.r X) = M.er X
Tactic:
rw [r, coe_toNat (by rwa [er_ne_top_iff])]
Proof state after:
no goals
Theorem: Matroid.rFin.coe_r_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 : α
hX : M.rFin X
⊢ M.er X ≠ ⊤
Tactic:
rwa [er_ne_top_iff]
Proof state after:
no goals
Theorem: Matroid.coe_rk_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 α
inst✝ : M.FiniteRk
⊢ ↑M.rk = M.erk
Tactic:
rw [erk_eq_er_ground, rk_def, coe_r_eq]
Proof state after:
no goals
Theorem: Matroid.r_eq_of_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 : α
h : M.er X = M.er Y
⊢ M.r X = M.r Y
Tactic:
rw [r, r, h]
Proof state after:
no goals
Theorem: Matroid.rFin.er_eq_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 : α
hX : M.rFin X
hY : M.rFin Y
⊢ M.er X = M.er Y ↔ M.r X = M.r Y
Tactic:
rw [← hX.coe_r_eq, ← hY.coe_r_eq, Nat.cast_inj]
Proof state after:
no goals
Theorem: Matroid.rFin.er_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 : α
hX : M.rFin X
hY : M.rFin Y
⊢ M.er X ≤ M.er Y ↔ M.r X ≤ M.r Y
Tactic:
rw [← hX.coe_r_eq, ← hY.coe_r_eq, Nat.cast_le]
Proof state after:
no goals
Theorem: Matroid.er_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 : α
inst✝ : M.FiniteRk
⊢ M.er X ≤ M.er Y ↔ M.r X ≤ M.r Y
Tactic:
rw [← coe_r_eq, ← coe_r_eq, Nat.cast_le]
Proof state after:
no goals
Theorem: Matroid.er_eq_coe_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 : α
inst✝ : M.FiniteRk
n : ℕ
⊢ M.er X = ↑n ↔ M.r X = n
Tactic:
rw [← coe_r_eq, Nat.cast_inj]
Proof state after:
no goals
Theorem: Matroid.er_le_coe_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 : α
inst✝ : M.FiniteRk
n : ℕ
⊢ M.er X ≤ ↑n ↔ M.r X ≤ n
Tactic:
rw [← coe_r_eq, Nat.cast_le]
Proof state after:
no goals
Theorem: Matroid.coe_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 : α
inst✝ : M.FiniteRk
n : ℕ
⊢ ↑n ≤ M.er X ↔ n ≤ M.r X
Tactic:
rw [← coe_r_eq, Nat.cast_le]
Proof state after:
no goals