CoveredByBalls.trans

lemma CoveredByBalls.trans (h : CoveredByBalls s n r)    (h2 : BallsCoverBalls X r r' m) : CoveredByBalls s (n * m) r' := by  obtain ⟨b0, hb0, hs0⟩ := h  rw [coveredByBalls_iff]  have := fun x ↦ ((coveredByBalls_iff ..).mp (h2 x))  classical    use b0.biUnion fun x ↦ (this x).choose    refine ⟨?_, fun p hp ↦ ?_⟩    · calc        _ ≤ ∑ x ∈ b0, (this x).choose.card := card_biUnion_le ..        _ ≤ ∑ _ ∈ b0, m := sum_le_sum fun x _ ↦ (this x).choose_spec.1        _ ≤ _ := by          rw [sum_const_nat fun x ↦ congrFun rfl]          exact Nat.mul_le_mul_right m hb0    · obtain ⟨b, _, hb⟩ := Set.mem_iUnion₂.mp (hs0 hp)      have tmp := ((this b).choose_spec.2) hb      push _ ∈ _ at tmp ⊢      obtain ⟨c, _, hc⟩ := tmp      use c, (by rw [mem_biUnion]; use b), hc