theorem cantor_diag {α : Type} (f : α → Set α) : ¬ Function.Surjective f := Function.cantor_surjective f

theorem identity_mob {α : Type} (a : α) : a = a := by rfl

theorem identity_prod {α : Type} (a : α) : a = a := by rfl

@[category test, AMS 11] theorem isBehrend_of_contains_one {ι : Type*} (A : ι → ℕ) (h : 1 ∈ Set.range A) : IsBehrend A := by rw [IsBehrend, Set.HasDensity] exact tendsto_atTop_of_eventually_const (i₀ := 1) fun n hn ↦ by simp [multiplesOf_eq_univ A h, Set.partialDensity] lia -- closed: sorry-free in formal-conjectures @ b5389792

open Filter open scoped Topology Real abbrev IsSumDistinctSet (A : Finset ℕ) (N : ℕ) : Prop := A ⊆ Finset.Icc 1 N ∧ (fun (⟨S, _⟩ : A.powerset) => S.sum id).Injective theorem erdos1_least_N_3 : IsLeast { N | ∃ A, IsSumDistinctSet A N ∧ A.card = 3 } 4 := by refine ⟨⟨{1, 2, 4}, ?_⟩, ?_⟩ · simp refine ⟨by decide, ?_⟩ let P := Finset...

@[category research solved, AMS 11] theorem fixture_fc_pipeline (n : ℕ) : 0 < n.factorial := Nat.factorial_pos n

theorem fixture_inf_primes (n : ℕ) : ∃ p, n < p ∧ Nat.Prime p := Nat.exists_infinite_primes n.succ

theorem fixture_even_or_odd (n : ℕ) : Even n ∨ Odd n := Nat.even_or_odd n

theorem fixture_add_comm (a b : ℕ) : a + b = b + a := by omega

theorem flt_invariant_isIntegral (A B G : Type*) [CommRing A] [CommRing B] [Algebra A B] [Group G] [MulSemiringAction G B] [SMulCommClass G A B] [Algebra.IsInvariant A B G] [Finite G] : Algebra.IsIntegral A B := Algebra.IsInvariant.isIntegral A B G