Theorem: Matroid.truncate_base_iff_of_finiteRk (Matroid/Constructions/Truncate.lean)

State before:
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
inst✝ : M.FiniteRk
h_rk : k ≤ M.erk
⊢ (M.truncateTo k).Base B ↔ M.Indep B ∧ B.encard = k
Tactic:
lift k to ℕ using (h_rk.trans_lt M.erk_lt_top).ne
State after:
case intro
α : Type u_1
M : Matroid α
E I B : Set α
inst✝ : M.FiniteRk
k : ℕ
h_rk : ↑k ≤ M.erk
⊢ (M.truncateTo ↑k).Base B ↔ M.Indep B ∧ B.encard = ↑k

State before:
case intro
α : Type u_1
M : Matroid α
E I B : Set α
inst✝ : M.FiniteRk
k : ℕ
h_rk : ↑k ≤ M.erk
⊢ (M.truncateTo ↑k).Base B ↔ M.Indep B ∧ B.encard = ↑k
Tactic:
rwa [truncateTo_base_iff]
State after:
no goals