lean_workbook_plus_23851
ProvedProve that if , then the sum of three members of would be divisible by 3 or there exist three members with the same remainder modulo 3.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_23851 (A : Finset ℤ) (hA : 5 ≤ A.card) : (∃ x y z : ℤ, x ∈ A ∧ y ∈ A ∧ z ∈ A ∧ 3 ∣ x + y + z) ∨ (∃ x y z : ℤ, x ∈ A ∧ y ∈ A ∧ z ∈ A ∧ x % 3 = y % 3 ∧ y % 3 = z % 3 ∧ z % 3 = x % 3) := by sorry
Source