Existence of embeddings from finite types

Let s : Set α be a finite set.

• Fin.Embedding.exists_embedding_disjoint_range_of_add_le_ENat_card If s.ncard + n ≤ ENat.card α, then there exists an embedding Fin n ↪ α whose range is disjoint from s.

• Fin.Embedding.exists_embedding_disjoint_range_of_add_le_Nat_card If α is finite and s.ncard + n ≤ Nat.card α, then there exists an embedding Fin n ↪ α whose range is disjoint from s.

• Fin.Embedding.restrictSurjective_of_add_le_ENatCard If m + n ≤ ENat.card α, then the restriction map from Fin (m + n) ↪ α to Fin m ↪ α is surjective.

• Fin.Embedding.restrictSurjective_of_add_le_natCard If α is finite and m + n ≤ Nat.card α, then the restriction map from Fin (m + n) ↪ α to Fin m ↪ α is surjective.

theorem Fin.Embedding.exists_embedding_disjoint_range_of_add_le_ENat_card {α : Type u_1} {n : ℕ} {s : Set α} [Finite ↑s] (hs : ↑s.ncard + ↑n ≤ ENat.card α) : ∃ (y : Fin n ↪ α), Disjoint s (Set.range ⇑y)

theorem Fin.Embedding.exists_embedding_disjoint_range_of_add_le_Nat_card {α : Type u_1} {n : ℕ} {s : Set α} [Finite α] (hs : s.ncard + n ≤ Nat.card α) : ∃ (y : Fin n ↪ α), Disjoint s (Set.range ⇑y)

theorem Fin.Embedding.restrictSurjective_of_add_le_ENatCard {α : Type u_1} {m n : ℕ} (hn : ↑m + ↑n ≤ ENat.card α) : Function.Surjective fun (x : Fin (m + n) ↪ α) => (castAddEmb n).trans x

theorem Fin.Embedding.restrictSurjective_of_le_ENatCard {α : Type u_1} {m n : ℕ} (hmn : m ≤ n) (hn : ↑n ≤ ENat.card α) : Function.Surjective fun (x : Fin n ↪ α) => (castLEEmb hmn).trans x

theorem Fin.Embedding.restrictSurjective_of_add_le_natCard {α : Type u_1} {m n : ℕ} [Finite α] (hn : m + n ≤ Nat.card α) : Function.Surjective fun (x : Fin (m + n) ↪ α) => (castAddEmb n).trans x

theorem Fin.Embedding.restrictSurjective_of_le_natCard {α : Type u_1} {m n : ℕ} [Finite α] (hmn : m ≤ n) (hn : n ≤ Nat.card α) : Function.Surjective fun (x : Fin n ↪ α) => (castLEEmb hmn).trans x