internlm/Lean-Github huggingface dataset:
Theorem: Matroid.rFin.r_le_r_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 : α
hY : M.rFin Y
hle : M.er X ≤ M.er Y
⊢ M.r X ≤ M.r Y
Tactic:
rwa [← rFin.er_le_er_iff _ hY]
Proof state after:
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
hY : M.rFin Y
hle : M.er X ≤ M.er Y
⊢ M.rFin X
Theorem: Matroid.rFin.r_le_r_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 : α
hY : M.rFin Y
hle : M.er X ≤ M.er Y
⊢ M.rFin X
Tactic:
exact hle.trans_lt hY.lt
Proof state after:
no goals
Theorem: Matroid.r_eq_r_inter_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 α
X : Set α
⊢ M.r X = M.r (X ∩ M.E)
Tactic:
rw [← er_toNat_eq_r, ← er_inter_ground_eq, er_toNat_eq_r]
Proof state after:
no goals
Theorem: Matroid.le_r_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.r X ↔ ∃ I ⊆ X, M.Indep I ∧ I.ncard = n
Tactic:
simp_rw [← coe_le_er_iff, le_er_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✝ : M.FiniteRk
n : ℕ
⊢ (∃ I ⊆ X, M.Indep I ∧ I.encard = ↑n) ↔ ∃ I ⊆ X, M.Indep I ∧ I.ncard = n
Theorem: Matroid.le_r_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 : ℕ
⊢ (∃ I ⊆ X, M.Indep I ∧ I.encard = ↑n) ↔ ∃ I ⊆ X, M.Indep I ∧ I.ncard = n
Tactic:
refine ⟨fun ⟨I, hIX, hI, hc⟩ ↦ ⟨I, hIX, hI, by rw [ncard_def, hc, toNat_coe]⟩,
  fun ⟨I, hIX, hI, hc⟩ ↦ ⟨I, hIX, hI, ?_⟩⟩
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✝ : M.FiniteRk
n : ℕ
x✝ : ∃ I ⊆ X, M.Indep I ∧ I.ncard = n
I : Set α
hIX : I ⊆ X
hI : M.Indep I
hc : I.ncard = n
⊢ I.encard = ↑n
Theorem: Matroid.le_r_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 : ℕ
x✝ : ∃ I ⊆ X, M.Indep I ∧ I.ncard = n
I : Set α
hIX : I ⊆ X
hI : M.Indep I
hc : I.ncard = n
⊢ I.encard = ↑n
Tactic:
rw [hI.finite.encard_eq_coe, ← hc]
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✝ : M.FiniteRk
n : ℕ
x✝ : ∃ I ⊆ X, M.Indep I ∧ I.ncard = n
I : Set α
hIX : I ⊆ X
hI : M.Indep I
hc : I.ncard = n
⊢ ↑(toNat I.encard) = ↑I.ncard
Theorem: Matroid.le_r_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 : ℕ
x✝ : ∃ I ⊆ X, M.Indep I ∧ I.ncard = n
I : Set α
hIX : I ⊆ X
hI : M.Indep I
hc : I.ncard = n
⊢ ↑(toNat I.encard) = ↑I.ncard
Tactic:
rfl
Proof state after:
no goals
Theorem: Matroid.le_r_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 : ℕ
x✝ : ∃ I ⊆ X, M.Indep I ∧ I.encard = ↑n
I : Set α
hIX : I ⊆ X
hI : M.Indep I
hc : I.encard = ↑n
⊢ I.ncard = n
Tactic:
rw [ncard_def, hc, toNat_coe]
Proof state after:
no goals
Theorem: Matroid.r_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 : α
inst✝ : M.FiniteRk
n : ℕ
⊢ M.r X ≤ n ↔ ∀ {I : Set α}, I ⊆ X → M.Indep I → I.ncard ≤ n
Tactic:
simp_rw [← er_le_coe_iff, er_le_iff, encard_le_coe_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✝ : M.FiniteRk
n : ℕ
⊢ (∀ {I : Set α}, I ⊆ X → M.Indep I → I.Finite ∧ ∃ n₀, I.encard = ↑n₀ ∧ n₀ ≤ n) ↔
    ∀ {I : Set α}, I ⊆ X → M.Indep I → I.ncard ≤ n
Theorem: Matroid.r_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 : α
inst✝ : M.FiniteRk
n : ℕ
⊢ (∀ {I : Set α}, I ⊆ X → M.Indep I → I.Finite ∧ ∃ n₀, I.encard = ↑n₀ ∧ n₀ ≤ n) ↔
    ∀ {I : Set α}, I ⊆ X → M.Indep I → I.ncard ≤ n
Tactic:
refine ⟨fun h I hIX hI ↦ ?_, fun h I hIX hI ↦ ⟨hI.finite, ⟨_, hI.finite.encard_eq_coe, h hIX hI⟩⟩⟩
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✝ : M.FiniteRk
n : ℕ
h : ∀ {I : Set α}, I ⊆ X → M.Indep I → I.Finite ∧ ∃ n₀, I.encard = ↑n₀ ∧ n₀ ≤ n
I : Set α
hIX : I ⊆ X
hI : M.Indep I
⊢ I.ncard ≤ n
Theorem: Matroid.r_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 : α
inst✝ : M.FiniteRk
n : ℕ
h : ∀ {I : Set α}, I ⊆ X → M.Indep I → I.Finite ∧ ∃ n₀, I.encard = ↑n₀ ∧ n₀ ≤ n
I : Set α
hIX : I ⊆ X
hI : M.Indep I
⊢ I.ncard ≤ n
Tactic:
obtain ⟨-, m, hm, hmn⟩ := h hIX hI
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 : α
inst✝ : M.FiniteRk
n : ℕ
h : ∀ {I : Set α}, I ⊆ X → M.Indep I → I.Finite ∧ ∃ n₀, I.encard = ↑n₀ ∧ n₀ ≤ n
I : Set α
hIX : I ⊆ X
hI : M.Indep I
m : ℕ
hm : I.encard = ↑m
hmn : m ≤ n
⊢ I.ncard ≤ n
Theorem: Matroid.r_le_iff
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 : α
inst✝ : M.FiniteRk
n : ℕ
h : ∀ {I : Set α}, I ⊆ X → M.Indep I → I.Finite ∧ ∃ n₀, I.encard = ↑n₀ ∧ n₀ ≤ n
I : Set α
hIX : I ⊆ X
hI : M.Indep I
m : ℕ
hm : I.encard = ↑m
hmn : m ≤ n
⊢ I.ncard ≤ n
Tactic:
rwa [ncard_def, hm, toNat_coe]
Proof state after:
no goals
Theorem: Matroid.r_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 α
inst✝ : M.FiniteRk
⊢ Monotone M.r
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 α
inst✝ : M.FiniteRk
X Y : Set α
hXY : X ⊆ Y
⊢ M.r X ≤ M.r Y
Theorem: Matroid.r_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 α
inst✝ : M.FiniteRk
X Y : Set α
hXY : X ⊆ Y
⊢ M.r X ≤ M.r Y
Tactic:
rw [← er_le_er_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
X Y : Set α
hXY : X ⊆ Y
⊢ M.er X ≤ M.er Y
Theorem: Matroid.r_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 α
inst✝ : M.FiniteRk
X Y : Set α
hXY : X ⊆ Y
⊢ M.er X ≤ M.er Y
Tactic:
exact M.er_mono hXY
Proof state after:
no goals
Theorem: Matroid.r_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.r ∅ = 0
Tactic:
rw [r, er_empty]
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 α
⊢ toNat 0 = 0
Theorem: Matroid.r_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 α
⊢ toNat 0 = 0
Tactic:
rfl
Proof state after:
no goals
Theorem: Matroid.r_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 α
⊢ M.r (M.cl X) = M.r X
Tactic:
rw [r, er_cl_eq, r]
Proof state after:
no goals
Theorem: Matroid.r_le_rk
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.r X ≤ M.rk
Tactic:
rw [r_eq_r_inter_ground, rk_def]
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
X : Set α
⊢ M.r (X ∩ M.E) ≤ M.r M.E
Theorem: Matroid.r_le_rk
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.r (X ∩ M.E) ≤ M.r M.E
Tactic:
exact M.r_mono inter_subset_right
Proof state after:
no goals
Theorem: Matroid.Indep.r
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.r I = I.ncard
Tactic:
rw [← er_toNat_eq_r, hI.er, ncard_def]
Proof state after:
no goals
Theorem: Matroid.Indep.card_le_r_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 : α
inst✝ : M.FiniteRk
hI : M.Indep I
h : I ⊆ X
⊢ I.ncard ≤ M.r X
Tactic:
rw [← hI.r]
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✝ : M.FiniteRk
hI : M.Indep I
h : I ⊆ X
⊢ M.r I ≤ M.r X
Theorem: Matroid.Indep.card_le_r_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 : α
inst✝ : M.FiniteRk
hI : M.Indep I
h : I ⊆ X
⊢ M.r I ≤ M.r X
Tactic:
exact M.r_mono h
Proof state after:
no goals
Theorem: Matroid.Basis'.card
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.Basis' I X
⊢ I.ncard = M.r X
Tactic:
rw [ncard_def, h.encard, ← er_toNat_eq_r]
Proof state after:
no goals
Theorem: Matroid.Basis'.r
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.Basis' I X
⊢ M.r I = M.r X
Tactic:
rw [← h.card, h.indep.r]
Proof state after:
no goals
Theorem: Matroid.r_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 : α
inst✝ : M.FiniteRk
hX : X ⊆ M.E
⊢ M.r X = 0 ↔ X ⊆ M.cl ∅
Tactic:
rw [← er_eq_coe_iff, coe_zero, er_eq_zero_iff]
Proof state after:
no goals
Theorem: Matroid.r_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.r (M.cl ∅) = 0
Tactic:
simp [r]
Proof state after:
no goals
Theorem: Matroid.Nonloop.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 : α
he : M.Nonloop e
⊢ M.r {e} = 1
Tactic:
rw [r, he.er_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 : α
he : M.Nonloop e
⊢ toNat 1 = 1
Theorem: Matroid.Nonloop.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 : α
he : M.Nonloop e
⊢ toNat 1 = 1
Tactic:
rfl
Proof state after:
no goals
Theorem: Matroid.Loop.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 : α
he : M.Loop e
⊢ M.r {e} = 0
Tactic:
rw [r, he.er_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 : α
he : M.Loop e
⊢ toNat 0 = 0
Theorem: Matroid.Loop.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 : α
he : M.Loop e
⊢ toNat 0 = 0
Tactic:
rfl
Proof state after:
no goals
Theorem: Matroid.rFin.submod
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.r (X ∩ Y) + M.r (X ∪ Y) ≤ M.r X + M.r Y
Tactic:
obtain ⟨c, h_eq⟩ := le_iff_exists_add.1 <| M.er_inter_add_er_union_le_er_add_er 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 : α
hX : M.rFin X
hY : M.rFin Y
c : ℕ∞
h_eq : M.er X + M.er Y = M.er (X ∩ Y) + M.er (X ∪ Y) + c
⊢ M.r (X ∩ Y) + M.r (X ∪ Y) ≤ M.r X + M.r Y
Theorem: Matroid.rFin.submod
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
hY : M.rFin Y
c : ℕ∞
h_eq : M.er X + M.er Y = M.er (X ∩ Y) + M.er (X ∪ Y) + c
⊢ M.r (X ∩ Y) + M.r (X ∪ Y) ≤ M.r X + M.r Y
Tactic:
obtain (rfl | hc) := eq_or_ne c ⊤
Proof state after:
case intro.inl
α : 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
h_eq : M.er X + M.er Y = M.er (X ∩ Y) + M.er (X ∪ Y) + ⊤
⊢ M.r (X ∩ Y) + M.r (X ∪ Y) ≤ M.r X + M.r Y

case intro.inr
α : 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
c : ℕ∞
h_eq : M.er X + M.er Y = M.er (X ∩ Y) + M.er (X ∪ Y) + c
hc : c ≠ ⊤
⊢ M.r (X ∩ Y) + M.r (X ∪ Y) ≤ M.r X + M.r Y
Theorem: Matroid.rFin.submod
Proof state before:
case intro.inr
α : 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
c : ℕ∞
h_eq : M.er X + M.er Y = M.er (X ∩ Y) + M.er (X ∪ Y) + c
hc : c ≠ ⊤
⊢ M.r (X ∩ Y) + M.r (X ∪ Y) ≤ M.r X + M.r Y
Tactic:
have hi : M.rFin (X ∩ Y) := hX.subset inter_subset_left
Proof state after:
case intro.inr
α : 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
c : ℕ∞
h_eq : M.er X + M.er Y = M.er (X ∩ Y) + M.er (X ∪ Y) + c
hc : c ≠ ⊤
hi : M.rFin (X ∩ Y)
⊢ M.r (X ∩ Y) + M.r (X ∪ Y) ≤ M.r X + M.r Y
Theorem: Matroid.rFin.submod
Proof state before:
case intro.inr
α : 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
c : ℕ∞
h_eq : M.er X + M.er Y = M.er (X ∩ Y) + M.er (X ∪ Y) + c
hc : c ≠ ⊤
hi : M.rFin (X ∩ Y)
⊢ M.r (X ∩ Y) + M.r (X ∪ Y) ≤ M.r X + M.r Y
Tactic:
have hu : M.rFin (X ∪ Y) := hX.union hY
Proof state after:
case intro.inr
α : 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
c : ℕ∞
h_eq : M.er X + M.er Y = M.er (X ∩ Y) + M.er (X ∪ Y) + c
hc : c ≠ ⊤
hi : M.rFin (X ∩ Y)
hu : M.rFin (X ∪ Y)
⊢ M.r (X ∩ Y) + M.r (X ∪ Y) ≤ M.r X + M.r Y
Theorem: Matroid.rFin.submod
Proof state before:
case intro.inr
α : 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
c : ℕ∞
h_eq : M.er X + M.er Y = M.er (X ∩ Y) + M.er (X ∪ Y) + c
hc : c ≠ ⊤
hi : M.rFin (X ∩ Y)
hu : M.rFin (X ∪ Y)
⊢ M.r (X ∩ Y) + M.r (X ∪ Y) ≤ M.r X + M.r Y
Tactic:
rw [← ge_iff_le, r,r, ge_iff_le, ← toNat_add hX.ne hY.ne, h_eq, toNat_add _ hc,
  toNat_add hi.ne hu.ne, ← r, ← r]
Proof state after:
case intro.inr
α : 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
c : ℕ∞
h_eq : M.er X + M.er Y = M.er (X ∩ Y) + M.er (X ∪ Y) + c
hc : c ≠ ⊤
hi : M.rFin (X ∩ Y)
hu : M.rFin (X ∪ Y)
⊢ M.r (X ∩ Y) + M.r (X ∪ Y) ≤ M.r (X ∩ Y) + M.r (X ∪ Y) + toNat c

α : 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
c : ℕ∞
h_eq : M.er X + M.er Y = M.er (X ∩ Y) + M.er (X ∪ Y) + c
hc : c ≠ ⊤
hi : M.rFin (X ∩ Y)
hu : M.rFin (X ∪ Y)
⊢ M.er (X ∩ Y) + M.er (X ∪ Y) ≠ ⊤
Theorem: Matroid.rFin.submod
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
c : ℕ∞
h_eq : M.er X + M.er Y = M.er (X ∩ Y) + M.er (X ∪ Y) + c
hc : c ≠ ⊤
hi : M.rFin (X ∩ Y)
hu : M.rFin (X ∪ Y)
⊢ M.er (X ∩ Y) + M.er (X ∪ Y) ≠ ⊤
Tactic:
rw [Ne, WithTop.add_eq_top, not_or]
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
hY : M.rFin Y
c : ℕ∞
h_eq : M.er X + M.er Y = M.er (X ∩ Y) + M.er (X ∪ Y) + c
hc : c ≠ ⊤
hi : M.rFin (X ∩ Y)
hu : M.rFin (X ∪ Y)
⊢ ¬M.er (X ∩ Y) = ⊤ ∧ ¬M.er (X ∪ Y) = ⊤
Theorem: Matroid.rFin.submod
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
c : ℕ∞
h_eq : M.er X + M.er Y = M.er (X ∩ Y) + M.er (X ∪ Y) + c
hc : c ≠ ⊤
hi : M.rFin (X ∩ Y)
hu : M.rFin (X ∪ Y)
⊢ ¬M.er (X ∩ Y) = ⊤ ∧ ¬M.er (X ∪ Y) = ⊤
Tactic:
exact ⟨hi.ne, hu.ne⟩
Proof state after:
no goals
Theorem: Matroid.rFin.submod
Proof state before:
case intro.inl
α : 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
h_eq : M.er X + M.er Y = M.er (X ∩ Y) + M.er (X ∪ Y) + ⊤
⊢ M.r (X ∩ Y) + M.r (X ∪ Y) ≤ M.r X + M.r Y
Tactic:
rw [add_top, WithTop.add_eq_top] at h_eq
Proof state after:
case intro.inl
α : 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
h_eq : M.er X = ⊤ ∨ M.er Y = ⊤
⊢ M.r (X ∩ Y) + M.r (X ∪ Y) ≤ M.r X + M.r Y
Theorem: Matroid.rFin.submod
Proof state before:
case intro.inl
α : 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
h_eq : M.er X = ⊤ ∨ M.er Y = ⊤
⊢ M.r (X ∩ Y) + M.r (X ∪ Y) ≤ M.r X + M.r Y
Tactic:
simp [hX.ne, hY.ne] at h_eq
Proof state after:
no goals
Theorem: Matroid.rFin.submod
Proof state before:
case intro.inr
α : 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
c : ℕ∞
h_eq : M.er X + M.er Y = M.er (X ∩ Y) + M.er (X ∪ Y) + c
hc : c ≠ ⊤
hi : M.rFin (X ∩ Y)
hu : M.rFin (X ∪ Y)
⊢ M.r (X ∩ Y) + M.r (X ∪ Y) ≤ M.r (X ∩ Y) + M.r (X ∪ Y) + toNat c
Tactic:
apply Nat.le_add_right
Proof state after:
no goals
Theorem: Matroid.Indep.exists_insert_of_ncard_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 : α
inst✝ : M.FiniteRk
J : Set α
hI : M.Indep I
hJ : M.Indep J
hcard : I.ncard < J.ncard
⊢ ∃ e ∈ J \ I, M.Indep (insert e I)
Tactic:
apply hI.exists_insert_of_encard_lt hJ
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✝ : M.FiniteRk
J : Set α
hI : M.Indep I
hJ : M.Indep J
hcard : I.ncard < J.ncard
⊢ I.encard < J.encard
Theorem: Matroid.Indep.exists_insert_of_ncard_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 : α
inst✝ : M.FiniteRk
J : Set α
hI : M.Indep I
hJ : M.Indep J
hcard : I.ncard < J.ncard
⊢ I.encard < J.encard
Tactic:
rw [← hJ.finite.cast_ncard_eq, ← hI.finite.cast_ncard_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 : α
inst✝ : M.FiniteRk
J : Set α
hI : M.Indep I
hJ : M.Indep J
hcard : I.ncard < J.ncard
⊢ ↑I.ncard < ↑J.ncard
Theorem: Matroid.Indep.exists_insert_of_ncard_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 : α
inst✝ : M.FiniteRk
J : Set α
hI : M.Indep I
hJ : M.Indep J
hcard : I.ncard < J.ncard
⊢ ↑I.ncard < ↑J.ncard
Tactic:
exact Nat.cast_lt.mpr hcard
Proof state after:
no goals
Theorem: Matroid.rk_map
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
M : Matroid α
f : α → β
hf : InjOn f M.E
⊢ (M.map f hf).rk = M.rk
Tactic:
simp [rk]
Proof state after:
no goals
Theorem: Matroid.Iso.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 : α
β : Type u_3
N : Matroid β
e : M ≂ N
⊢ M.rk = N.rk
Tactic:
rw [rk, e.erk_eq]
Proof state after:
no goals
Theorem: Matroid.loopyOn_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 : α
E✝ E X : Set α
⊢ (loopyOn E).er X = 0
Tactic:
obtain ⟨I, hI⟩ := (loopyOn E).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 : α
E✝ E X I : Set α
hI : (loopyOn E).Basis' I X
⊢ (loopyOn E).er X = 0
Theorem: Matroid.loopyOn_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 : α
E✝ E X I : Set α
hI : (loopyOn E).Basis' I X
⊢ (loopyOn E).er X = 0
Tactic:
rw [hI.er_eq_encard, loopyOn_indep_iff.1 hI.indep, encard_empty]
Proof state after:
no goals
Theorem: Matroid.loopyOn_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 : α
E✝ E : Set α
⊢ (loopyOn E).erk = 0
Tactic:
rw [erk_eq_er_ground, loopyOn_er_eq]
Proof state after:
no goals
Theorem: Matroid.loopyOn_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 : α
E✝ E X : Set α
⊢ (loopyOn E).r X = 0
Tactic:
rw [← er_toNat_eq_r, loopyOn_er_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 : α
E✝ E X : Set α
⊢ toNat 0 = 0
Theorem: Matroid.loopyOn_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 : α
E✝ E X : Set α
⊢ toNat 0 = 0
Tactic:
rfl
Proof state after:
no goals
Theorem: Matroid.erk_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 : α
E : Set α
⊢ M.erk = 0 ↔ M = loopyOn M.E
Tactic:
refine ⟨fun h ↦ cl_empty_eq_ground_iff.1 ?_, fun h ↦ by rw [h, loopyOn_erk_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 : α
E : Set α
h : M.erk = 0
⊢ M.cl ∅ = M.E
Theorem: Matroid.erk_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 : α
E : Set α
h : M.erk = 0
⊢ M.cl ∅ = M.E
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 : α
E : Set α
h : M.erk = 0
B : Set α
hB : M.Base B
⊢ M.cl ∅ = M.E
Theorem: Matroid.erk_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 : α
E : Set α
h : M.erk = 0
B : Set α
hB : M.Base B
⊢ M.cl ∅ = M.E
Tactic:
rw [← hB.encard, encard_eq_zero] at h
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 : α
E B : Set α
h : B = ∅
hB : M.Base B
⊢ M.cl ∅ = M.E
Theorem: Matroid.erk_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 : α
E B : Set α
h : B = ∅
hB : M.Base B
⊢ M.cl ∅ = M.E
Tactic:
rw [← h, hB.cl_eq]
Proof state after:
no goals
Theorem: Matroid.erk_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 : α
E : Set α
h : M = loopyOn M.E
⊢ M.erk = 0
Tactic:
rw [h, loopyOn_erk_eq]
Proof state after:
no goals
Theorem: Matroid.erk_loopyOn_eq_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 : α✝
E : Set α✝
α : Type u_3
⊢ (emptyOn α).erk = 0
Tactic:
rw [erk_eq_zero_iff, emptyOn_ground, loopyOn_empty]
Proof state after:
no goals
Theorem: Matroid.eq_loopyOn_iff_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 : α
E : Set α
h : M = loopyOn E
⊢ M.cl ∅ = E ∧ M.E = E
Tactic:
rw [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 : α
E : Set α
h : M = loopyOn E
⊢ (loopyOn E).cl ∅ = E ∧ (loopyOn E).E = E
Theorem: Matroid.eq_loopyOn_iff_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 : α
E : Set α
h : M = loopyOn E
⊢ (loopyOn E).cl ∅ = E ∧ (loopyOn E).E = E
Tactic:
simp
Proof state after:
no goals
Theorem: Matroid.eq_loopyOn_iff_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 : α
E : Set α
x✝ : M.cl ∅ = E ∧ M.E = E
h : M.cl ∅ = E
h' : M.E = E
⊢ M = loopyOn E
Tactic:
rw [← h', ← cl_empty_eq_ground_iff, h, h']
Proof state after:
no goals
Theorem: Matroid.eq_loopyOn_iff_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 : α
E : Set α
h : M = loopyOn E
⊢ M.erk = 0 ∧ M.E = E
Tactic:
rw [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 : α
E : Set α
h : M = loopyOn E
⊢ (loopyOn E).erk = 0 ∧ (loopyOn E).E = E
Theorem: Matroid.eq_loopyOn_iff_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 : α
E : Set α
h : M = loopyOn E
⊢ (loopyOn E).erk = 0 ∧ (loopyOn E).E = E
Tactic:
simp
Proof state after:
no goals
Theorem: Matroid.eq_loopyOn_iff_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 : α
E : Set α
x✝ : M.erk = 0 ∧ M.E = E
h : M.erk = 0
h' : M.E = E
⊢ M = loopyOn E
Tactic:
rw [← h', ← erk_eq_zero_iff, h]
Proof state after:
no goals
Theorem: Matroid.freeOn_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 : α
E✝ E : Set α
⊢ (freeOn E).erk = E.encard
Tactic:
rw [erk_eq_er_ground, freeOn_ground, (freeOn_indep_iff.2 rfl.subset).er]
Proof state after:
no goals