refine hS.symm.le.trans (M.r_le_of_subset ?_)
α : Type u_1
M M₁ M₂ : Matroid α
A I X E : Set α
ι : Type u_2
inst✝¹ : Finite ι
x : ι → α
inst✝ : M.FiniteRk
f : α → ι
hx : ∀ (i : ι), f (x i) = i
h_ind : M.Indep (range x)
S : Set ι
hinj : Function.Injective x
hS : M.r (x '' S) = S.ncard
⊢ S.ncard ≤ M.r (f ⁻¹' S)
α : Type u_1
M M₁ M₂ : Matroid α
A I X E : Set α
ι : Type u_2
inst✝¹ : Finite ι
x : ι → α
inst✝ : M.FiniteRk
f : α → ι
hx : ∀ (i : ι), f (x i) = i
h_ind : M.Indep (range x)
S : Set ι
hinj : Function.Injective x
hS : M.r (x '' S) = S.ncard
⊢ x '' S ⊆ f ⁻¹' S