Schauder's theorem (transpose of compact is compact) in Lean without Arzelà–Ascoli

Statement: for normed X, Y over RCLike 𝕜 and compact K, IsCompactOperator (fun f : StrongDual 𝕜 Y ↦ f ∘L K). Package the map as T := (ContinuousLinearMap.compL 𝕜 X Y 𝕜).flip K and change IsCompactOperator T. Use isCompactOperator_iff_isCompact_closure_image_closedBall (T : StrongDual 𝕜 Y →ₗ[𝕜] StrongDual 𝕜 X) one_pos (the explicit ascription is needed) and isCompact_iff_totallyBounded_isComplete (the dual is complete). Nets: Set.exists_subset_image_finite_and.1 (Metric.finite_approx_of_totallyBounded hTB (ε/4) _) gives a finite u ⊆ closedBall with K '' closedBall ⊆ ⋃ y ∈ K '' u, ball y (ε/4). With Fintype u := huf.fintype, Φ f := fun i : u ↦ f (K i) lands in a proper space, so the image of the dual ball is totally bounded via IsBounded.isCompact_closure (bound it with pi_norm_le_iff_of_nonneg). Take a second net and compare coordinates with norm_le_pi_norm. Use the closed ball, not the open one, so that ContinuousLinearMap.opNorm_le_of_unit_norm (‖x‖ = 1 → bound) applies.