lean_workbook_plus_60827
Provedand Thus,
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_60827 (b : ℕ) (h1 : b % 5 = 0 ∨ b % 5 = 1 ∨ b % 5 = 4) (h2 : b % 7 = 0 ∨ b % 7 = 3 ∨ b % 7 = 4) : ∃ k : ℕ, b = 0 + k*5 ∨ b = 4 + k*5 ∨ b = 10 + k*5 ∨ b = 11 + k*5 ∨ b = 14 + k*5 ∨ b = 21 + k*5 ∨ b = 24 + k*5 ∨ b = 25 + k*5 := by sorry
Source