no goals
α : Type u
inst✝ : Infinite α
H1 : ℵ₀ ≤ (#α)
x✝ : α
⊢ ∀ ⦃a₂ : α⦄, (fun a => [a]) x✝ = (fun a => [a]) a₂ → x✝ = a₂
simp
no goals
α : Type u
inst✝ : Infinite α
H1 : ℵ₀ ≤ (#α)
⊢ (sum fun x => #α) = (#α)
simp [H1]