lean_workbook_plus_78977

Proved

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

Prove that if there are 5 numbers in set $A$ , there would be a sum of three numbers which is a multiple of 3.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_78977 (A : Finset ℕ) (hA : A.card = 5) : ∃ x y z : ℕ, x ∈ A ∧ y ∈ A ∧ z ∈ A ∧ 3 ∣ x + y + z   :=  by sorry

Source