internlm/Lean-Github huggingface dataset:
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
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
Tactic:
rw [← add_zero (M.er X), hins,
  WithTop.add_le_add_iff_left (fun htop ↦ not_top_lt (htop ▸ hlt))] at hY
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 : 1 ≤ 0
⊢ 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
hlt : M.er X < M.er Y
e : α
he : e ∈ Y \ X
hins : M.er (insert e X) = M.er X + 1
hY : 1 ≤ 0
⊢ False
Tactic:
simp at hY
Proof state after:
no goals
Theorem: Matroid.Indep.exists_insert_of_encard_lt
Proof state before:
α : Type u_1
ι : Type u_2
M N : Matroid α
I✝ B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
I J : Set α
hI : M.Indep I
hJ : M.Indep J
hcard : I.encard < J.encard
⊢ ∃ e ∈ J \ I, M.Indep (insert e I)
Tactic:
have hIfin : I.Finite := encard_lt_top_iff.1 <| hcard.trans_le le_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 : α
I J : Set α
hI : M.Indep I
hJ : M.Indep J
hcard : I.encard < J.encard
hIfin : I.Finite
⊢ ∃ e ∈ J \ I, M.Indep (insert e I)
Theorem: Matroid.Indep.exists_insert_of_encard_lt
Proof state before:
α : Type u_1
ι : Type u_2
M N : Matroid α
I✝ B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
I J : Set α
hI : M.Indep I
hJ : M.Indep J
hcard : I.encard < J.encard
hIfin : I.Finite
⊢ ∃ e ∈ J \ I, M.Indep (insert e I)
Tactic:
rw [← hI.er, ← hJ.er] at 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 : α
I J : Set α
hI : M.Indep I
hJ : M.Indep J
hcard : M.er I < M.er J
hIfin : I.Finite
⊢ ∃ e ∈ J \ I, M.Indep (insert e I)
Theorem: Matroid.Indep.exists_insert_of_encard_lt
Proof state before:
α : Type u_1
ι : Type u_2
M N : Matroid α
I✝ B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
I J : Set α
hI : M.Indep I
hJ : M.Indep J
hcard : M.er I < M.er J
hIfin : I.Finite
⊢ ∃ e ∈ J \ I, M.Indep (insert e I)
Tactic:
obtain ⟨e, he, hIe⟩ := er_augment hcard
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 : α
I J : Set α
hI : M.Indep I
hJ : M.Indep J
hcard : M.er I < M.er J
hIfin : I.Finite
e : α
he : e ∈ J \ I
hIe : M.er (insert e I) = M.er I + 1
⊢ ∃ e ∈ J \ I, M.Indep (insert e I)
Theorem: Matroid.Indep.exists_insert_of_encard_lt
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 : α
I J : Set α
hI : M.Indep I
hJ : M.Indep J
hcard : M.er I < M.er J
hIfin : I.Finite
e : α
he : e ∈ J \ I
hIe : M.er (insert e I) = M.er I + 1
⊢ ∃ e ∈ J \ I, M.Indep (insert e I)
Tactic:
refine ⟨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 : α
I J : Set α
hI : M.Indep I
hJ : M.Indep J
hcard : M.er I < M.er J
hIfin : I.Finite
e : α
he : e ∈ J \ I
hIe : M.er (insert e I) = M.er I + 1
⊢ M.Indep (insert e I)
Theorem: Matroid.Indep.exists_insert_of_encard_lt
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 : α
I J : Set α
hI : M.Indep I
hJ : M.Indep J
hcard : M.er I < M.er J
hIfin : I.Finite
e : α
he : e ∈ J \ I
hIe : M.er (insert e I) = M.er I + 1
⊢ M.Indep (insert e I)
Tactic:
rw [indep_iff_er_eq_encard_of_finite (hIfin.insert e), hIe, encard_insert_of_not_mem he.2,
  hI.er]
Proof state after:
no goals
Theorem: Matroid.spanning_iff_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 : α
inst✝ : M.FiniteRk
⊢ M.Spanning X ↔ M.erk ≤ M.er X ∧ X ⊆ M.E
Tactic:
refine' ⟨fun h ↦ _, fun ⟨hr, hX⟩ ↦ _⟩
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 : α
inst✝ : M.FiniteRk
h : M.Spanning X
⊢ M.erk ≤ M.er X ∧ X ⊆ M.E

case refine'_2
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
inst✝ : M.FiniteRk
x✝ : M.erk ≤ M.er X ∧ X ⊆ M.E
hr : M.erk ≤ M.er X
hX : X ⊆ M.E
⊢ M.Spanning X
Theorem: Matroid.spanning_iff_er'
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 : α
inst✝ : M.FiniteRk
x✝ : M.erk ≤ M.er X ∧ X ⊆ M.E
hr : M.erk ≤ M.er X
hX : X ⊆ M.E
⊢ M.Spanning X
Tactic:
obtain ⟨J, hJ⟩ := M.exists_basis X
Proof state after:
case refine'_2.intro
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
inst✝ : M.FiniteRk
x✝ : M.erk ≤ M.er X ∧ X ⊆ M.E
hr : M.erk ≤ M.er X
hX : X ⊆ M.E
J : Set α
hJ : M.Basis J X
⊢ M.Spanning X
Theorem: Matroid.spanning_iff_er'
Proof state before:
case refine'_2.intro
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
inst✝ : M.FiniteRk
x✝ : M.erk ≤ M.er X ∧ X ⊆ M.E
hr : M.erk ≤ M.er X
hX : X ⊆ M.E
J : Set α
hJ : M.Basis J X
⊢ M.Spanning X
Tactic:
obtain ⟨B, hB, hJB⟩ := hJ.indep.exists_base_superset
Proof state after:
case refine'_2.intro.intro.intro
α : Type u_1
ι : Type u_2
M N : Matroid α
I B✝ X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
inst✝ : M.FiniteRk
x✝ : M.erk ≤ M.er X ∧ X ⊆ M.E
hr : M.erk ≤ M.er X
hX : X ⊆ M.E
J : Set α
hJ : M.Basis J X
B : Set α
hB : M.Base B
hJB : J ⊆ B
⊢ M.Spanning X
Theorem: Matroid.spanning_iff_er'
Proof state before:
case refine'_2.intro.intro.intro
α : Type u_1
ι : Type u_2
M N : Matroid α
I B✝ X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
inst✝ : M.FiniteRk
x✝ : M.erk ≤ M.er X ∧ X ⊆ M.E
hr : M.erk ≤ M.er X
hX : X ⊆ M.E
J : Set α
hJ : M.Basis J X
B : Set α
hB : M.Base B
hJB : J ⊆ B
⊢ M.Spanning X
Tactic:
rw [← hJ.encard, ← hB.encard] at hr
Proof state after:
case refine'_2.intro.intro.intro
α : Type u_1
ι : Type u_2
M N : Matroid α
I B✝ X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
inst✝ : M.FiniteRk
x✝ : M.erk ≤ M.er X ∧ X ⊆ M.E
hX : X ⊆ M.E
J : Set α
hJ : M.Basis J X
B : Set α
hr : B.encard ≤ J.encard
hB : M.Base B
hJB : J ⊆ B
⊢ M.Spanning X
Theorem: Matroid.spanning_iff_er'
Proof state before:
case refine'_2.intro.intro.intro
α : Type u_1
ι : Type u_2
M N : Matroid α
I B✝ X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
inst✝ : M.FiniteRk
x✝ : M.erk ≤ M.er X ∧ X ⊆ M.E
hX : X ⊆ M.E
J : Set α
hJ : M.Basis J X
B : Set α
hr : B.encard ≤ J.encard
hB : M.Base B
hJB : J ⊆ B
⊢ M.Spanning X
Tactic:
obtain rfl := hB.finite.eq_of_subset_of_encard_le hJB hr
Proof state after:
case refine'_2.intro.intro.intro
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
inst✝ : M.FiniteRk
x✝ : M.erk ≤ M.er X ∧ X ⊆ M.E
hX : X ⊆ M.E
J : Set α
hJ : M.Basis J X
hr : J.encard ≤ J.encard
hB : M.Base J
hJB : J ⊆ J
⊢ M.Spanning X
Theorem: Matroid.spanning_iff_er'
Proof state before:
case refine'_2.intro.intro.intro
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
inst✝ : M.FiniteRk
x✝ : M.erk ≤ M.er X ∧ X ⊆ M.E
hX : X ⊆ M.E
J : Set α
hJ : M.Basis J X
hr : J.encard ≤ J.encard
hB : M.Base J
hJB : J ⊆ J
⊢ M.Spanning X
Tactic:
rw [spanning_iff_superset_base]
Proof state after:
case refine'_2.intro.intro.intro
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
inst✝ : M.FiniteRk
x✝ : M.erk ≤ M.er X ∧ X ⊆ M.E
hX : X ⊆ M.E
J : Set α
hJ : M.Basis J X
hr : J.encard ≤ J.encard
hB : M.Base J
hJB : J ⊆ J
⊢ ∃ B, M.Base B ∧ B ⊆ X
Theorem: Matroid.spanning_iff_er'
Proof state before:
case refine'_2.intro.intro.intro
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
inst✝ : M.FiniteRk
x✝ : M.erk ≤ M.er X ∧ X ⊆ M.E
hX : X ⊆ M.E
J : Set α
hJ : M.Basis J X
hr : J.encard ≤ J.encard
hB : M.Base J
hJB : J ⊆ J
⊢ ∃ B, M.Base B ∧ B ⊆ X
Tactic:
exact ⟨J, hB, hJ.subset⟩
Proof state after:
no goals
Theorem: Matroid.spanning_iff_er'
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 : α
inst✝ : M.FiniteRk
h : M.Spanning X
⊢ M.erk ≤ M.er X ∧ X ⊆ M.E
Tactic:
rw [erk_eq_er_ground, ← er_cl_eq _ X, h.cl_eq]
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 : α
inst✝ : M.FiniteRk
h : M.Spanning X
⊢ M.er M.E ≤ M.er M.E ∧ X ⊆ M.E
Theorem: Matroid.spanning_iff_er'
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 : α
inst✝ : M.FiniteRk
h : M.Spanning X
⊢ M.er M.E ≤ M.er M.E ∧ X ⊆ M.E
Tactic:
exact ⟨rfl.le, h.subset_ground⟩
Proof state after:
no goals
Theorem: Matroid.spanning_iff_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 : α
inst✝ : M.FiniteRk
hX : autoParam (X ⊆ M.E) _auto✝
⊢ M.Spanning X ↔ M.erk ≤ M.er X
Tactic:
rw [spanning_iff_er', and_iff_left hX]
Proof state after:
no goals
Theorem: Matroid.Spanning.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 : α
hX : M.Spanning X
⊢ M.er X = M.erk
Tactic:
obtain ⟨B, hB, hBX⟩ := hX.exists_base_subset
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 : α
hX : M.Spanning X
B : Set α
hB : M.Base B
hBX : B ⊆ X
⊢ M.er X = M.erk
Theorem: Matroid.Spanning.er_eq
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 : α
hX : M.Spanning X
B : Set α
hB : M.Base B
hBX : B ⊆ X
⊢ M.er X = M.erk
Tactic:
rw [le_antisymm_iff, and_iff_right (M.er_le_erk _), ← hB.er]
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 : α
hX : M.Spanning X
B : Set α
hB : M.Base B
hBX : B ⊆ X
⊢ M.er B ≤ M.er X
Theorem: Matroid.Spanning.er_eq
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 : α
hX : M.Spanning X
B : Set α
hB : M.Base B
hBX : B ⊆ X
⊢ M.er B ≤ M.er X
Tactic:
exact M.er_mono hBX
Proof state after:
no goals
Theorem: Matroid.Loop.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 : α
he : M.Loop e
⊢ M.er {e} = 0
Tactic:
rw [← er_cl_eq, he.cl, er_cl_eq, er_empty]
Proof state after:
no goals
Theorem: Matroid.Nonloop.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 : α
he : M.Nonloop e
⊢ M.er {e} = 1
Tactic:
rw [← he.indep.basis_self.encard, encard_singleton]
Proof state after:
no goals
Theorem: Matroid.LoopEquiv.er_eq_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 : α
h : M.LoopEquiv X Y
⊢ M.er X = M.er Y
Tactic:
rw [← M.er_cl_eq, h.cl_eq_cl, M.er_cl_eq]
Proof state after:
no goals
Theorem: Matroid.er_eq_zero_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 : autoParam (X ⊆ M.E) _auto✝
⊢ M.er X = 0 ↔ X ⊆ M.cl ∅
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 : autoParam (X ⊆ M.E) _auto✝
I : Set α
hI : M.Basis I X
⊢ M.er X = 0 ↔ X ⊆ M.cl ∅
Theorem: Matroid.er_eq_zero_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 : α
hX : autoParam (X ⊆ M.E) _auto✝
I : Set α
hI : M.Basis I X
⊢ M.er X = 0 ↔ X ⊆ M.cl ∅
Tactic:
rw [← hI.encard, encard_eq_zero]
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 : autoParam (X ⊆ M.E) _auto✝
I : Set α
hI : M.Basis I X
⊢ I = ∅ ↔ X ⊆ M.cl ∅
Theorem: Matroid.er_eq_zero_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 : α
hX : autoParam (X ⊆ M.E) _auto✝
I : Set α
hI : M.Basis I X
⊢ I = ∅ ↔ X ⊆ M.cl ∅
Tactic:
exact ⟨by rintro rfl; exact hI.subset_cl, fun h ↦ eq_empty_of_forall_not_mem
  fun x hx ↦ (hI.indep.nonloop_of_mem hx).not_loop (h (hI.subset hx))⟩
Proof state after:
no goals
Theorem: Matroid.er_eq_zero_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 : autoParam (X ⊆ M.E) _auto✝
I : Set α
hI : M.Basis I X
⊢ I = ∅ → X ⊆ M.cl ∅
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 : α
hX : autoParam (X ⊆ M.E) _auto✝
hI : M.Basis ∅ X
⊢ X ⊆ M.cl ∅
Theorem: Matroid.er_eq_zero_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 : autoParam (X ⊆ M.E) _auto✝
hI : M.Basis ∅ X
⊢ X ⊆ M.cl ∅
Tactic:
exact hI.subset_cl
Proof state after:
no goals
Theorem: Matroid.er_eq_zero_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 = 0 ↔ X ∩ M.E ⊆ M.cl ∅
Tactic:
rw [← er_inter_ground_eq, er_eq_zero_iff]
Proof state after:
no goals
Theorem: Matroid.er_loops
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 (M.cl ∅) = 0
Tactic:
rw [er_eq_zero_iff]
Proof state after:
no goals
Theorem: Matroid.er_eq_one_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 : autoParam (X ⊆ M.E) _auto✝
⊢ M.er X = 1 ↔ ∃ e ∈ X, M.Nonloop e ∧ X ⊆ M.cl {e}
Tactic:
refine ⟨?_, fun ⟨e, heX, he, hXe⟩ ↦ ?_⟩
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 : α
hX : autoParam (X ⊆ M.E) _auto✝
⊢ M.er X = 1 → ∃ e ∈ X, M.Nonloop e ∧ X ⊆ M.cl {e}

case refine_2
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e✝ f : α
hX : autoParam (X ⊆ M.E) _auto✝
x✝ : ∃ e ∈ X, M.Nonloop e ∧ X ⊆ M.cl {e}
e : α
heX : e ∈ X
he : M.Nonloop e
hXe : X ⊆ M.cl {e}
⊢ M.er X = 1
Theorem: Matroid.er_eq_one_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 : α
hX : autoParam (X ⊆ M.E) _auto✝
x✝ : ∃ e ∈ X, M.Nonloop e ∧ X ⊆ M.cl {e}
e : α
heX : e ∈ X
he : M.Nonloop e
hXe : X ⊆ M.cl {e}
⊢ M.er X = 1
Tactic:
rw [← he.er_eq]
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 : α
hX : autoParam (X ⊆ M.E) _auto✝
x✝ : ∃ e ∈ X, M.Nonloop e ∧ X ⊆ M.cl {e}
e : α
heX : e ∈ X
he : M.Nonloop e
hXe : X ⊆ M.cl {e}
⊢ M.er X = M.er {e}
Theorem: Matroid.er_eq_one_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 : α
hX : autoParam (X ⊆ M.E) _auto✝
x✝ : ∃ e ∈ X, M.Nonloop e ∧ X ⊆ M.cl {e}
e : α
heX : e ∈ X
he : M.Nonloop e
hXe : X ⊆ M.cl {e}
⊢ M.er X = M.er {e}
Tactic:
exact ((M.er_mono hXe).trans (M.er_cl_eq _).le).antisymm (M.er_mono (singleton_subset_iff.2 heX))
Proof state after:
no goals
Theorem: Matroid.er_eq_one_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 : α
hX : autoParam (X ⊆ M.E) _auto✝
⊢ M.er X = 1 → ∃ e ∈ X, M.Nonloop e ∧ X ⊆ M.cl {e}
Tactic:
obtain ⟨I, hI⟩ := 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 : α
hX : autoParam (X ⊆ M.E) _auto✝
I : Set α
hI : M.Basis I X
⊢ M.er X = 1 → ∃ e ∈ X, M.Nonloop e ∧ X ⊆ M.cl {e}
Theorem: Matroid.er_eq_one_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 : α
hX : autoParam (X ⊆ M.E) _auto✝
I : Set α
hI : M.Basis I X
⊢ M.er X = 1 → ∃ e ∈ X, M.Nonloop e ∧ X ⊆ M.cl {e}
Tactic:
rw [hI.er_eq_encard, encard_eq_one]
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 : α
hX : autoParam (X ⊆ M.E) _auto✝
I : Set α
hI : M.Basis I X
⊢ (∃ x, I = {x}) → ∃ e ∈ X, M.Nonloop e ∧ X ⊆ M.cl {e}
Theorem: Matroid.er_eq_one_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 : α
hX : autoParam (X ⊆ M.E) _auto✝
I : Set α
hI : M.Basis I X
⊢ (∃ x, I = {x}) → ∃ e ∈ X, M.Nonloop e ∧ X ⊆ M.cl {e}
Tactic:
rintro ⟨e, rfl⟩
Proof state after:
case refine_1.intro.intro
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e✝ f : α
hX : autoParam (X ⊆ M.E) _auto✝
e : α
hI : M.Basis {e} X
⊢ ∃ e ∈ X, M.Nonloop e ∧ X ⊆ M.cl {e}
Theorem: Matroid.er_eq_one_iff
Proof state before:
case refine_1.intro.intro
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e✝ f : α
hX : autoParam (X ⊆ M.E) _auto✝
e : α
hI : M.Basis {e} X
⊢ ∃ e ∈ X, M.Nonloop e ∧ X ⊆ M.cl {e}
Tactic:
exact ⟨e, singleton_subset_iff.1 hI.subset, indep_singleton.1 hI.indep, hI.subset_cl⟩
Proof state after:
no goals
Theorem: Matroid.er_le_one_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.Nonempty
hX : autoParam (X ⊆ M.E) _auto✝
⊢ M.er X ≤ 1 ↔ ∃ e ∈ M.E, X ⊆ M.cl {e}
Tactic:
refine' ⟨fun h ↦ _, fun ⟨e, _, he⟩ ↦ _⟩
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 : α
inst✝ : M.Nonempty
hX : autoParam (X ⊆ M.E) _auto✝
h : M.er X ≤ 1
⊢ ∃ e ∈ M.E, X ⊆ M.cl {e}

case refine'_2
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e✝ f : α
inst✝ : M.Nonempty
hX : autoParam (X ⊆ M.E) _auto✝
x✝ : ∃ e ∈ M.E, X ⊆ M.cl {e}
e : α
left✝ : e ∈ M.E
he : X ⊆ M.cl {e}
⊢ M.er X ≤ 1
Theorem: Matroid.er_le_one_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 : α
inst✝ : M.Nonempty
hX : autoParam (X ⊆ M.E) _auto✝
x✝ : ∃ e ∈ M.E, X ⊆ M.cl {e}
e : α
left✝ : e ∈ M.E
he : X ⊆ M.cl {e}
⊢ M.er X ≤ 1
Tactic:
refine (M.er_mono he).trans ?_
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 : α
inst✝ : M.Nonempty
hX : autoParam (X ⊆ M.E) _auto✝
x✝ : ∃ e ∈ M.E, X ⊆ M.cl {e}
e : α
left✝ : e ∈ M.E
he : X ⊆ M.cl {e}
⊢ M.er (M.cl {e}) ≤ 1
Theorem: Matroid.er_le_one_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 : α
inst✝ : M.Nonempty
hX : autoParam (X ⊆ M.E) _auto✝
x✝ : ∃ e ∈ M.E, X ⊆ M.cl {e}
e : α
left✝ : e ∈ M.E
he : X ⊆ M.cl {e}
⊢ M.er (M.cl {e}) ≤ 1
Tactic:
rw [er_cl_eq, ← encard_singleton e]
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 : α
inst✝ : M.Nonempty
hX : autoParam (X ⊆ M.E) _auto✝
x✝ : ∃ e ∈ M.E, X ⊆ M.cl {e}
e : α
left✝ : e ∈ M.E
he : X ⊆ M.cl {e}
⊢ M.er {e} ≤ {e}.encard
Theorem: Matroid.er_le_one_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 : α
inst✝ : M.Nonempty
hX : autoParam (X ⊆ M.E) _auto✝
x✝ : ∃ e ∈ M.E, X ⊆ M.cl {e}
e : α
left✝ : e ∈ M.E
he : X ⊆ M.cl {e}
⊢ M.er {e} ≤ {e}.encard
Tactic:
exact M.er_le_encard {e}
Proof state after:
no goals
Theorem: Matroid.er_le_one_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 : α
inst✝ : M.Nonempty
hX : autoParam (X ⊆ M.E) _auto✝
h : M.er X ≤ 1
⊢ ∃ e ∈ M.E, X ⊆ M.cl {e}
Tactic:
obtain ⟨I, hI⟩ := 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 : α
inst✝ : M.Nonempty
hX : autoParam (X ⊆ M.E) _auto✝
h : M.er X ≤ 1
I : Set α
hI : M.Basis I X
⊢ ∃ e ∈ M.E, X ⊆ M.cl {e}
Theorem: Matroid.er_le_one_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 : α
inst✝ : M.Nonempty
hX : autoParam (X ⊆ M.E) _auto✝
h : M.er X ≤ 1
I : Set α
hI : M.Basis I X
⊢ ∃ e ∈ M.E, X ⊆ M.cl {e}
Tactic:
rw [hI.er_eq_encard, encard_le_one_iff_eq] 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 : α
inst✝ : M.Nonempty
hX : autoParam (X ⊆ M.E) _auto✝
I : Set α
h : I = ∅ ∨ ∃ x, I = {x}
hI : M.Basis I X
⊢ ∃ e ∈ M.E, X ⊆ M.cl {e}
Theorem: Matroid.er_le_one_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 : α
inst✝ : M.Nonempty
hX : autoParam (X ⊆ M.E) _auto✝
I : Set α
h : I = ∅ ∨ ∃ x, I = {x}
hI : M.Basis I X
⊢ ∃ e ∈ M.E, X ⊆ M.cl {e}
Tactic:
obtain (rfl | ⟨e, rfl⟩) := h
Proof state after:
case refine'_1.intro.inl
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
inst✝ : M.Nonempty
hX : autoParam (X ⊆ M.E) _auto✝
hI : M.Basis ∅ X
⊢ ∃ e ∈ M.E, X ⊆ M.cl {e}

case refine'_1.intro.inr.intro
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e✝ f : α
inst✝ : M.Nonempty
hX : autoParam (X ⊆ M.E) _auto✝
e : α
hI : M.Basis {e} X
⊢ ∃ e ∈ M.E, X ⊆ M.cl {e}
Theorem: Matroid.er_le_one_iff
Proof state before:
case refine'_1.intro.inr.intro
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e✝ f : α
inst✝ : M.Nonempty
hX : autoParam (X ⊆ M.E) _auto✝
e : α
hI : M.Basis {e} X
⊢ ∃ e ∈ M.E, X ⊆ M.cl {e}
Tactic:
exact ⟨e, hI.indep.subset_ground rfl,  hI.subset_cl⟩
Proof state after:
no goals
Theorem: Matroid.er_le_one_iff
Proof state before:
case refine'_1.intro.inl
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
inst✝ : M.Nonempty
hX : autoParam (X ⊆ M.E) _auto✝
hI : M.Basis ∅ X
⊢ ∃ e ∈ M.E, X ⊆ M.cl {e}
Tactic:
exact ⟨M.ground_nonempty.some, M.ground_nonempty.some_mem,
  hI.subset_cl.trans ((M.cl_subset_cl (empty_subset _)))⟩
Proof state after:
no goals
Theorem: Matroid.er_ne_top_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 ≠ ⊤ ↔ M.rFin X
Tactic:
rw [rFin, ← lt_top_iff_ne_top]
Proof state after:
no goals
Theorem: Matroid.er_eq_top_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 = ⊤ ↔ ¬M.rFin X
Tactic:
rw [← er_ne_top_iff, not_ne_iff]
Proof state after:
no goals
Theorem: Matroid.rFin_inter_ground_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 ∩ M.E) ↔ M.rFin X
Tactic:
rw [rFin, er_inter_ground_eq, rFin]
Proof state after:
no goals
Theorem: Matroid.rFin.finite_of_basis'
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
hI : M.Basis' I X
⊢ I.Finite
Tactic:
rwa [← encard_lt_top_iff, hI.encard]
Proof state after:
no goals
Theorem: Matroid.rFin.finite_of_basis
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
hI : M.Basis I X
⊢ I.Finite
Tactic:
rwa [← encard_lt_top_iff, hI.encard]
Proof state after:
no goals
Theorem: Matroid.rFin_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 : α
x✝ : ∃ I, M.Basis' I X ∧ I.Finite
I : Set α
hI : M.Basis' I X
hIfin : I.Finite
⊢ M.rFin X
Tactic:
rwa [← er_lt_top_iff, hI.er_eq_encard, encard_lt_top_iff]
Proof state after:
no goals
Theorem: Matroid.rFin_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 : autoParam (X ⊆ M.E) _auto✝
⊢ M.rFin X ↔ ∃ I, M.Basis I X ∧ I.Finite
Tactic:
simp_rw [rFin_iff', M.basis'_iff_basis hX]
Proof state after:
no goals
Theorem: Matroid.Basis'.rFin_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 : α
hIX : M.Basis' I X
h : I.Finite
⊢ M.rFin X
Tactic:
rwa [← er_ne_top_iff, ← hIX.encard, encard_ne_top_iff]
Proof state after:
no goals
Theorem: Matroid.Basis.rFin_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 : α
hIX : M.Basis I X
h : I.Finite
⊢ M.rFin X
Tactic:
rwa [← er_ne_top_iff, ← hIX.encard, encard_ne_top_iff]
Proof state after:
no goals