Theorem: Matroid.unifOn_base_iff (Matroid/Constructions/Uniform.lean)

State before:
α : Type u_1
M : Matroid α
E I B X C : Set α
k✝ : ℕ∞
k : ℕ
hk : ↑k ≤ E.encard
hBE : B ⊆ E
⊢ (unifOn E ↑k).Base B ↔ B.encard = ↑k
Tactic:
rw [unifOn, truncateTo_base_iff, freeOn_indep_iff, and_iff_right hBE]
State after:
α : Type u_1
M : Matroid α
E I B X C : Set α
k✝ : ℕ∞
k : ℕ
hk : ↑k ≤ E.encard
hBE : B ⊆ E
⊢ ↑k ≤ (freeOn E).erk

State before:
α : Type u_1
M : Matroid α
E I B X C : Set α
k✝ : ℕ∞
k : ℕ
hk : ↑k ≤ E.encard
hBE : B ⊆ E
⊢ ↑k ≤ (freeOn E).erk
Tactic:
rwa [freeOn_erk_eq]
State after:
no goals