Prove2Me

lean_workbook_plus_71428

Proved

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

A certain positive integer is congruent to 4(mod9)4\pmod{9} , congruent to 1(mod5)1\pmod{5} , and congruent to 5(mod8)5\pmod{8} . Show that the number is congruent to 1(mod3)1\pmod{3} .

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_71428 (n : ℕ) (h₁ : n ≡ 4 [ZMOD 9]) (h₂ : n ≡ 1 [ZMOD 5]) (h₃ : n ≡ 5 [ZMOD 8]) : n ≡ 1 [ZMOD 3]   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph