lean_workbook_plus_46936
ProvedFor examle:
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_46936 : 1 ∈ ({1, 2, 3} : Finset ℕ) := by sorrySource
For examle:
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_46936 : 1 ∈ ({1, 2, 3} : Finset ℕ) := by sorry