Singleton bound

theorem singleton_bound (C : Set (n → R)) :    (ofFinite C).card ≤ (ofFinite R).card ^ (card n - (‖C‖₀ - 1)) := by  by_cases non_triv : ‖C‖₀ ≥ 1  · -- there exists some projection S of the desired size    have ax_proj: ∃ (S : Finset n), card S = card n - (‖C‖₀ - 1) := by      let instexists := Finset.le_card_iff_exists_subset_card         (α := n)         (s := @Fintype.elems n _)         (n := card n - (‖C‖₀ - 1))      have some: card n - (‖C‖₀ - 1) ≤ card n := by        omega      obtain ⟨t, ht⟩ := instexists.1 some      exists t      simp only [card_coe]      exact And.right ht    obtain ⟨S, hS⟩ := ax_proj    -- project C by only looking at indices in S    let Cproj := Set.image (projection S) C    -- The size of C is upper bounded by the size of its projection,    -- because the projection is injective    have C_le_Cproj: @card C (ofFinite C) ≤ @card Cproj (ofFinite Cproj) := by      apply @Fintype.card_le_of_injective C Cproj        (ofFinite C)        (ofFinite Cproj)        (Set.imageFactorization (projection S) C)      refine Set.imageFactorization_injective_iff.mpr ?_      intro u hu v hv heq      apply projection_injective (nontriv := non_triv) (S := S) (u := u) (v := v) <;>        assumption    -- The size of Cproj itself is sufficiently bounded by its type    have Cproj_le_type_card :    @card Cproj (ofFinite Cproj) ≤ @card R (ofFinite R) ^ (card n - (‖C‖₀ - 1)) := by      let card_fun := @card_fun S R (Classical.typeDecidableEq S) _ (ofFinite R)      rw[hS] at card_fun      rw[← card_fun]      let huniv := @set_fintype_card_le_univ (S → R) ?_ Cproj (ofFinite Cproj)      exact huniv    apply le_trans (b := @card Cproj (ofFinite Cproj)) <;>      assumption  · simp only [ge_iff_le, not_le, Nat.lt_one_iff] at non_triv    rw[non_triv]    simp only [zero_tsub, tsub_zero]    let card_fun := @card_fun n R (Classical.typeDecidableEq n) _ (ofFinite R)    rw[← card_fun]    let huniv := @set_fintype_card_le_univ (n → R) ?_ C (ofFinite C)    exact huniv