Prove2Me

lean_workbook_plus_70079

Proved

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

Solution n−3∈{−15,−5,−3,−1,1,3,5,15}⇒n∈{−12,−2,0,2,4,6,8,18} n-3 \in \{ -15,-5,-3,-1,1,3,5,15 \} \Rightarrow n \in \{ -12,-2,0,2,4,6,8,18 \}

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_70079 (n : ℤ) : n - 3 ∈ ({-15, -5, -3, -1, 1, 3, 5, 15} : Finset ℤ) ↔ n ∈ ({-12, -2, 0, 2, 4, 6, 8, 18} : Finset ℤ)   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph