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

State before:
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
h_rk : M.erk ≤ k
⊢ M.truncateTo k = M
Tactic:
refine eq_of_indep_iff_indep_forall truncateTo_ground_eq (fun I _ ↦ ?_)
State after:
α : Type u_1
M : Matroid α
E I✝ B : Set α
k : ℕ∞
h_rk : M.erk ≤ k
I : Set α
x✝ : I ⊆ (M.truncateTo k).E
⊢ (M.truncateTo k).Indep I ↔ M.Indep I

State before:
α : Type u_1
M : Matroid α
E I✝ B : Set α
k : ℕ∞
h_rk : M.erk ≤ k
I : Set α
x✝ : I ⊆ (M.truncateTo k).E
⊢ (M.truncateTo k).Indep I ↔ M.Indep I
Tactic:
rw [truncateTo_indep_iff, and_iff_left_iff_imp]
State after:
α : Type u_1
M : Matroid α
E I✝ B : Set α
k : ℕ∞
h_rk : M.erk ≤ k
I : Set α
x✝ : I ⊆ (M.truncateTo k).E
⊢ M.Indep I → I.encard ≤ k

State before:
α : Type u_1
M : Matroid α
E I✝ B : Set α
k : ℕ∞
h_rk : M.erk ≤ k
I : Set α
x✝ : I ⊆ (M.truncateTo k).E
⊢ M.Indep I → I.encard ≤ k
Tactic:
exact fun hi ↦ hi.encard_le_erk.trans h_rk
State after:
no goals