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

State before:
α : Type u_1
M : Matroid α
E I B X C : Set α
k : ℕ∞
hktop : k ≠ ⊤
hk : k ≤ E.encard
hBE : B ⊆ E
⊢ (unifOn E k).Base B ↔ B.encard = k
Tactic:
lift k to ℕ using hktop
State after:
case intro
α : Type u_1
M : Matroid α
E I B X C : Set α
hBE : B ⊆ E
k : ℕ
hk : ↑k ≤ E.encard
⊢ (unifOn E ↑k).Base B ↔ B.encard = ↑k

State before:
case intro
α : Type u_1
M : Matroid α
E I B X C : Set α
hBE : B ⊆ E
k : ℕ
hk : ↑k ≤ E.encard
⊢ (unifOn E ↑k).Base B ↔ B.encard = ↑k
Tactic:
rw [unifOn_base_iff hk hBE]
State after:
no goals