Theorem: Matroid.Indep.of_truncateTo (Matroid/Constructions/Truncate.lean)

State before:
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
h : (M.truncateTo k).Indep I
⊢ M.Indep I
Tactic:
rw [truncateTo_indep_iff] at h
State after:
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
h : M.Indep I ∧ I.encard ≤ k
⊢ M.Indep I

State before:
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
h : M.Indep I ∧ I.encard ≤ k
⊢ M.Indep I
Tactic:
exact h.1
State after:
no goals