rw [Function.Injective.encard_image (fun _ _ ↦ by simp), and_iff_left_iff_imp]
case refine_2.intro.intro.intro
α : Type u_1
E✝ I✝ B X C : Set α
k : ℕ∞
a b a' b' : ℕ
E : Set α
hE : E.encard = ↑b
e : ↑E ≃ Fin b
I : Set ↑(unifOn E ↑a).E
⊢ I.encard ≤ ↑a ∧ I ⊆ Subtype.val ⁻¹' E ↔ ((fun a_1 => ⟨e a_1, trivial⟩) '' I).encard ≤ ↑a
case refine_2.intro.intro.intro
α : Type u_1
E✝ I✝ B X C : Set α
k : ℕ∞
a b a' b' : ℕ
E : Set α
hE : E.encard = ↑b
e : ↑E ≃ Fin b
I : Set ↑(unifOn E ↑a).E
⊢ I.encard ≤ ↑a → I ⊆ Subtype.val ⁻¹' E