lean_workbook_plus_471
ProvedLastly, we oversubtracted the case where the number is divisible by all three, so we need to add this back. The product of the three prime factors is , so we have . Finally, we have numbers below 750 that are divisible by , , or .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_471 : Finset.card (Finset.filter (λ x => 2 ∣ x ∨ 3 ∣ x ∨ 7 ∣ x) (Finset.range 750)) = 536 := by sorry
Source