Prove2Me

lean_workbook_plus_61940

Proved

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

Show that A1∩A2={2k  ∣  k∈N}∩{3k  ∣  k∈N}={6k  ∣  k∈N}A_1 \cap A_2 = \{ 2k \; | \; k \in \mathbb{N} \} \cap \{ 3k \; | \; k \in \mathbb{N} \} = \{ 6k \; | \; k \in \mathbb{N} \}.

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_61940 (A₁ A₂ : Set ℕ) (hA₁ : A₁ = {k | k % 2 = 0}) (hA₂ : A₂ = {k | k % 3 = 0}) : A₁ ∩ A₂ = {k | k % 6 = 0}   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph