rwa [Subtype.val_injective.encard_image, (EmbeddingLike.injective' _).encard_image,
  encard_preimage_of_injective_subset_range Subtype.val_injective (by simpa)] at hwin
case refine_1.inr
α : Type u_1
M : Matroid α
E I✝ B X C : Set α
k : ℕ∞
a b a' b' : ℕ
x✝ : Nonempty (M ≂ unif a b)
e : M ≂ unif a b
I : Set α
hIE : I ⊆ M.E
hwin : M.Indep I ↔ ((fun a => ↑a) '' ((fun a_1 => e a_1) '' M.E ↓∩ I)).encard ≤ ↑a
⊢ M.Indep I ↔ I.encard ≤ ↑a
no goals