FormalConjectures.ErdosProblems.«913»

/-
Copyright 2025 The Formal Conjectures Authors.

Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at

    https://www.apache.org/licenses/LICENSE-2.0

Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
-/

import FormalConjecturesUtil

Erdős Problem 913

Reference: erdosproblems.com/913

Reviewed by @b-mehta on 2025-05-27

namespace Erdos913

Are there infinitely many $n$ such that if $$ n(n + 1) = \prod_i p_i^{k_i} $$ is the factorisation into distinct primes then all exponents $k_i$ are distinct?

@[category research open, AMS 11]
theorem erdos_913 : answer(sorry) ↔
    { n | Set.InjOn (n * (n + 1)).factorization (n * (n + 1)).primeFactors }.Infinite := by⊢ True ↔ {n | Set.InjOn ⇑(n * (n + 1)).factorization ↑(n * (n + 1)).primeFactors}.Infinite
  sorryAll goals completed! 🐙

It is likely that there are infinitely many primes $p$ such that $8p^2 - 1$ is also prime.

@[category research open, AMS 11]
theorem erdos_913.variants.infinite_many_8p_sq_add_one_primes :
    { p | p.Prime ∧ (8 * p ^ 2 - 1).Prime }.Infinite := by⊢ {p | Nat.Prime p ∧ Nat.Prime (8 * p ^ 2 - 1)}.Infinite
  sorryAll goals completed! 🐙

If there are infinitely many primes $p$ such that $8p^2 - 1$ is prime, then this is true.


@[category research solved, AMS 11]
theorem erdos_913.variants.conditional (h : { p | p.Prime ∧ (8 * p ^ 2 - 1).Prime }.Infinite) :
    { n | Set.InjOn (n * (n + 1)).factorization (n * (n + 1)).primeFactors }.Infinite := byh:{p | Nat.Prime p ∧ Nat.Prime (8 * p ^ 2 - 1)}.Infinite⊢ {n | Set.InjOn ⇑(n * (n + 1)).factorization ↑(n * (n + 1)).primeFactors}.Infinite
  set S := { p | p.Prime ∧ (8 * p ^ 2 - 1).Prime }S:Set ℕ := {p | Nat.Prime p ∧ Nat.Prime (8 * p ^ 2 - 1)}h:S.Infinite⊢ {n | Set.InjOn ⇑(n * (n + 1)).factorization ↑(n * (n + 1)).primeFactors}.Infinite
  let f : ℕ → ℕ := fun p ↦ 8 * p ^ 2 - 1S:Set ℕ := {p | Nat.Prime p ∧ Nat.Prime (8 * p ^ 2 - 1)}h:S.Infinitef:ℕ → ℕ := fun p ↦ 8 * p ^ 2 - 1⊢ {n | Set.InjOn ⇑(n * (n + 1)).factorization ↑(n * (n + 1)).primeFactors}.Infinite
  have hS : ∀ p, p.Prime → 1 < 8 * p ^ 2 := by
    rintro p hpS:Set ℕ := {p | Nat.Prime p ∧ Nat.Prime (8 * p ^ 2 - 1)}h:S.Infinitef:ℕ → ℕ := fun p ↦ 8 * p ^ 2 - 1p:ℕhp:Nat.Prime p⊢ 1 < 8 * p ^ 2S:Set ℕ := {p | Nat.Prime p ∧ Nat.Prime (8 * p ^ 2 - 1)}h:S.Infinitef:ℕ → ℕ := fun p ↦ 8 * p ^ 2 - 1hS:∀ (p : ℕ), Nat.Prime p → 1 < 8 * p ^ 2⊢ {n | Set.InjOn ⇑(n * (n + 1)).factorization ↑(n * (n + 1)).primeFactors}.Infinite
    nlinarith [hp.two_le]S:Set ℕ := {p | Nat.Prime p ∧ Nat.Prime (8 * p ^ 2 - 1)}h:S.Infinitef:ℕ → ℕ := fun p ↦ 8 * p ^ 2 - 1hS:∀ (p : ℕ), Nat.Prime p → 1 < 8 * p ^ 2⊢ {n | Set.InjOn ⇑(n * (n + 1)).factorization ↑(n * (n + 1)).primeFactors}.InfiniteS:Set ℕ := {p | Nat.Prime p ∧ Nat.Prime (8 * p ^ 2 - 1)}h:S.Infinitef:ℕ → ℕ := fun p ↦ 8 * p ^ 2 - 1hS:∀ (p : ℕ), Nat.Prime p → 1 < 8 * p ^ 2⊢ {n | Set.InjOn ⇑(n * (n + 1)).factorization ↑(n * (n + 1)).primeFactors}.Infinite
  have : S.InjOn f := by
    simp only [Set.InjOn, f]S:Set ℕ := {p | Nat.Prime p ∧ Nat.Prime (8 * p ^ 2 - 1)}h:S.Infinitef:ℕ → ℕ := fun p ↦ 8 * p ^ 2 - 1hS:∀ (p : ℕ), Nat.Prime p → 1 < 8 * p ^ 2⊢ ∀ ⦃x₁ : ℕ⦄, x₁ ∈ S → ∀ ⦃x₂ : ℕ⦄, x₂ ∈ S → 8 * x₁ ^ 2 - 1 = 8 * x₂ ^ 2 - 1 → x₁ = x₂S:Set ℕ := {p | Nat.Prime p ∧ Nat.Prime (8 * p ^ 2 - 1)}h:S.Infinitef:ℕ → ℕ := fun p ↦ 8 * p ^ 2 - 1hS:∀ (p : ℕ), Nat.Prime p → 1 < 8 * p ^ 2this:Set.InjOn f S⊢ {n | Set.InjOn ⇑(n * (n + 1)).factorization ↑(n * (n + 1)).primeFactors}.Infinite
    rintro a ha b hb hS:Set ℕ := {p | Nat.Prime p ∧ Nat.Prime (8 * p ^ 2 - 1)}h✝:S.Infinitef:ℕ → ℕ := fun p ↦ 8 * p ^ 2 - 1hS:∀ (p : ℕ), Nat.Prime p → 1 < 8 * p ^ 2a:ℕha:a ∈ Sb:ℕhb:b ∈ Sh:8 * a ^ 2 - 1 = 8 * b ^ 2 - 1⊢ a = bS:Set ℕ := {p | Nat.Prime p ∧ Nat.Prime (8 * p ^ 2 - 1)}h:S.Infinitef:ℕ → ℕ := fun p ↦ 8 * p ^ 2 - 1hS:∀ (p : ℕ), Nat.Prime p → 1 < 8 * p ^ 2this:Set.InjOn f S⊢ {n | Set.InjOn ⇑(n * (n + 1)).factorization ↑(n * (n + 1)).primeFactors}.Infinite
    rw [tsub_left_inj (hS a ha.1).le (hS b hb.1).leS:Set ℕ := {p | Nat.Prime p ∧ Nat.Prime (8 * p ^ 2 - 1)}h✝:S.Infinitef:ℕ → ℕ := fun p ↦ 8 * p ^ 2 - 1hS:∀ (p : ℕ), Nat.Prime p → 1 < 8 * p ^ 2a:ℕha:a ∈ Sb:ℕhb:b ∈ Sh:8 * a ^ 2 = 8 * b ^ 2⊢ a = bS:Set ℕ := {p | Nat.Prime p ∧ Nat.Prime (8 * p ^ 2 - 1)}h✝:S.Infinitef:ℕ → ℕ := fun p ↦ 8 * p ^ 2 - 1hS:∀ (p : ℕ), Nat.Prime p → 1 < 8 * p ^ 2a:ℕha:a ∈ Sb:ℕhb:b ∈ Sh:8 * a ^ 2 = 8 * b ^ 2⊢ a = bS:Set ℕ := {p | Nat.Prime p ∧ Nat.Prime (8 * p ^ 2 - 1)}h:S.Infinitef:ℕ → ℕ := fun p ↦ 8 * p ^ 2 - 1hS:∀ (p : ℕ), Nat.Prime p → 1 < 8 * p ^ 2this:Set.InjOn f S⊢ {n | Set.InjOn ⇑(n * (n + 1)).factorization ↑(n * (n + 1)).primeFactors}.Infinite] at hS:Set ℕ := {p | Nat.Prime p ∧ Nat.Prime (8 * p ^ 2 - 1)}h✝:S.Infinitef:ℕ → ℕ := fun p ↦ 8 * p ^ 2 - 1hS:∀ (p : ℕ), Nat.Prime p → 1 < 8 * p ^ 2a:ℕha:a ∈ Sb:ℕhb:b ∈ Sh:8 * a ^ 2 = 8 * b ^ 2⊢ a = bS:Set ℕ := {p | Nat.Prime p ∧ Nat.Prime (8 * p ^ 2 - 1)}h:S.Infinitef:ℕ → ℕ := fun p ↦ 8 * p ^ 2 - 1hS:∀ (p : ℕ), Nat.Prime p → 1 < 8 * p ^ 2this:Set.InjOn f S⊢ {n | Set.InjOn ⇑(n * (n + 1)).factorization ↑(n * (n + 1)).primeFactors}.Infinite
    simpa using hS:Set ℕ := {p | Nat.Prime p ∧ Nat.Prime (8 * p ^ 2 - 1)}h:S.Infinitef:ℕ → ℕ := fun p ↦ 8 * p ^ 2 - 1hS:∀ (p : ℕ), Nat.Prime p → 1 < 8 * p ^ 2this:Set.InjOn f S⊢ {n | Set.InjOn ⇑(n * (n + 1)).factorization ↑(n * (n + 1)).primeFactors}.InfiniteS:Set ℕ := {p | Nat.Prime p ∧ Nat.Prime (8 * p ^ 2 - 1)}h:S.Infinitef:ℕ → ℕ := fun p ↦ 8 * p ^ 2 - 1hS:∀ (p : ℕ), Nat.Prime p → 1 < 8 * p ^ 2this:Set.InjOn f S⊢ {n | Set.InjOn ⇑(n * (n + 1)).factorization ↑(n * (n + 1)).primeFactors}.Infinite
  refine ((h.sdiff (Set.finite_singleton 2)).image (this.mono Set.sdiff_subset)).mono ?_S:Set ℕ := {p | Nat.Prime p ∧ Nat.Prime (8 * p ^ 2 - 1)}h:S.Infinitef:ℕ → ℕ := fun p ↦ 8 * p ^ 2 - 1hS:∀ (p : ℕ), Nat.Prime p → 1 < 8 * p ^ 2this:Set.InjOn f S⊢ f '' (S \ {2}) ⊆ {n | Set.InjOn ⇑(n * (n + 1)).factorization ↑(n * (n + 1)).primeFactors}
  simp only [Set.image_subset_iff, Set.preimage_ofPred_eq, S]S:Set ℕ := {p | Nat.Prime p ∧ Nat.Prime (8 * p ^ 2 - 1)}h:S.Infinitef:ℕ → ℕ := fun p ↦ 8 * p ^ 2 - 1hS:∀ (p : ℕ), Nat.Prime p → 1 < 8 * p ^ 2this:Set.InjOn f S⊢ {p | Nat.Prime p ∧ Nat.Prime (8 * p ^ 2 - 1)} \ {2} ⊆
  {a | Set.InjOn ⇑(f a * (f a + 1)).factorization ↑(f a * (f a + 1)).primeFactors}
  rintro p ⟨⟨hp, hp'⟩, hp''⟩S:Set ℕ := {p | Nat.Prime p ∧ Nat.Prime (8 * p ^ 2 - 1)}h:S.Infinitef:ℕ → ℕ := fun p ↦ 8 * p ^ 2 - 1hS:∀ (p : ℕ), Nat.Prime p → 1 < 8 * p ^ 2this:Set.InjOn f Sp:ℕhp'':p ∉ {2}hp:Nat.Prime php':Nat.Prime (8 * p ^ 2 - 1)⊢ p ∈ {a | Set.InjOn ⇑(f a * (f a + 1)).factorization ↑(f a * (f a + 1)).primeFactors}
  simp only [Set.mem_singleton_iff] at hp''S:Set ℕ := {p | Nat.Prime p ∧ Nat.Prime (8 * p ^ 2 - 1)}h:S.Infinitef:ℕ → ℕ := fun p ↦ 8 * p ^ 2 - 1hS:∀ (p : ℕ), Nat.Prime p → 1 < 8 * p ^ 2this:Set.InjOn f Sp:ℕhp:Nat.Prime php':Nat.Prime (8 * p ^ 2 - 1)hp'':¬p = 2⊢ p ∈ {a | Set.InjOn ⇑(f a * (f a + 1)).factorization ↑(f a * (f a + 1)).primeFactors}
  have fac : (f p * (f p + 1)).factorization =
      Finsupp.single (8 * p ^ 2 - 1) 1 + (Finsupp.single p 2 + Finsupp.single 2 3) := byh:{p | Nat.Prime p ∧ Nat.Prime (8 * p ^ 2 - 1)}.Infinite⊢ {n | Set.InjOn ⇑(n * (n + 1)).factorization ↑(n * (n + 1)).primeFactors}.InfiniteS:Set ℕ := {p | Nat.Prime p ∧ Nat.Prime (8 * p ^ 2 - 1)}h:S.Infinitef:ℕ → ℕ := fun p ↦ 8 * p ^ 2 - 1hS:∀ (p : ℕ), Nat.Prime p → 1 < 8 * p ^ 2this:Set.InjOn f Sp:ℕhp:Nat.Prime php':Nat.Prime (8 * p ^ 2 - 1)hp'':¬p = 2fac:(f p * (f p + 1)).factorization = (fun₀ | 8 * p ^ 2 - 1 => 1) + ((fun₀ | p => 2) + fun₀ | 2 => 3)⊢ p ∈ {a | Set.InjOn ⇑(f a * (f a + 1)).factorization ↑(f a * (f a + 1)).primeFactors}
    simp only [f, Nat.sub_add_cancel (hS p hp).le]S:Set ℕ := {p | Nat.Prime p ∧ Nat.Prime (8 * p ^ 2 - 1)}h:S.Infinitef:ℕ → ℕ := fun p ↦ 8 * p ^ 2 - 1hS:∀ (p : ℕ), Nat.Prime p → 1 < 8 * p ^ 2this:Set.InjOn f Sp:ℕhp:Nat.Prime php':Nat.Prime (8 * p ^ 2 - 1)hp'':¬p = 2⊢ ((8 * p ^ 2 - 1) * (8 * p ^ 2)).factorization = (fun₀ | 8 * p ^ 2 - 1 => 1) + ((fun₀ | p => 2) + fun₀ | 2 => 3)S:Set ℕ := {p | Nat.Prime p ∧ Nat.Prime (8 * p ^ 2 - 1)}h:S.Infinitef:ℕ → ℕ := fun p ↦ 8 * p ^ 2 - 1hS:∀ (p : ℕ), Nat.Prime p → 1 < 8 * p ^ 2this:Set.InjOn f Sp:ℕhp:Nat.Prime php':Nat.Prime (8 * p ^ 2 - 1)hp'':¬p = 2fac:(f p * (f p + 1)).factorization = (fun₀ | 8 * p ^ 2 - 1 => 1) + ((fun₀ | p => 2) + fun₀ | 2 => 3)⊢ p ∈ {a | Set.InjOn ⇑(f a * (f a + 1)).factorization ↑(f a * (f a + 1)).primeFactors}
    have : 2 ≤ p := hp.two_leS:Set ℕ := {p | Nat.Prime p ∧ Nat.Prime (8 * p ^ 2 - 1)}h:S.Infinitef:ℕ → ℕ := fun p ↦ 8 * p ^ 2 - 1hS:∀ (p : ℕ), Nat.Prime p → 1 < 8 * p ^ 2this✝:Set.InjOn f Sp:ℕhp:Nat.Prime php':Nat.Prime (8 * p ^ 2 - 1)hp'':¬p = 2this:2 ≤ p⊢ ((8 * p ^ 2 - 1) * (8 * p ^ 2)).factorization = (fun₀ | 8 * p ^ 2 - 1 => 1) + ((fun₀ | p => 2) + fun₀ | 2 => 3)S:Set ℕ := {p | Nat.Prime p ∧ Nat.Prime (8 * p ^ 2 - 1)}h:S.Infinitef:ℕ → ℕ := fun p ↦ 8 * p ^ 2 - 1hS:∀ (p : ℕ), Nat.Prime p → 1 < 8 * p ^ 2this:Set.InjOn f Sp:ℕhp:Nat.Prime php':Nat.Prime (8 * p ^ 2 - 1)hp'':¬p = 2fac:(f p * (f p + 1)).factorization = (fun₀ | 8 * p ^ 2 - 1 => 1) + ((fun₀ | p => 2) + fun₀ | 2 => 3)⊢ p ∈ {a | Set.InjOn ⇑(f a * (f a + 1)).factorization ↑(f a * (f a + 1)).primeFactors}
    rw [Nat.factorization_mul hp'.ne_zero (byS:Set ℕ := {p | Nat.Prime p ∧ Nat.Prime (8 * p ^ 2 - 1)}h:S.Infinitef:ℕ → ℕ := fun p ↦ 8 * p ^ 2 - 1hS:∀ (p : ℕ), Nat.Prime p → 1 < 8 * p ^ 2this✝:Set.InjOn f Sp:ℕhp:Nat.Prime php':Nat.Prime (8 * p ^ 2 - 1)hp'':¬p = 2this:2 ≤ p⊢ 8 * p ^ 2 ≠ 0S:Set ℕ := {p | Nat.Prime p ∧ Nat.Prime (8 * p ^ 2 - 1)}h:S.Infinitef:ℕ → ℕ := fun p ↦ 8 * p ^ 2 - 1hS:∀ (p : ℕ), Nat.Prime p → 1 < 8 * p ^ 2this:Set.InjOn f Sp:ℕhp:Nat.Prime php':Nat.Prime (8 * p ^ 2 - 1)hp'':¬p = 2fac:(f p * (f p + 1)).factorization = (fun₀ | 8 * p ^ 2 - 1 => 1) + ((fun₀ | p => 2) + fun₀ | 2 => 3)⊢ p ∈ {a | Set.InjOn ⇑(f a * (f a + 1)).factorization ↑(f a * (f a + 1)).primeFactors} positivityAll goals completed! 🐙S:Set ℕ := {p | Nat.Prime p ∧ Nat.Prime (8 * p ^ 2 - 1)}h:S.Infinitef:ℕ → ℕ := fun p ↦ 8 * p ^ 2 - 1hS:∀ (p : ℕ), Nat.Prime p → 1 < 8 * p ^ 2this:Set.InjOn f Sp:ℕhp:Nat.Prime php':Nat.Prime (8 * p ^ 2 - 1)hp'':¬p = 2fac:(f p * (f p + 1)).factorization = (fun₀ | 8 * p ^ 2 - 1 => 1) + ((fun₀ | p => 2) + fun₀ | 2 => 3)⊢ p ∈ {a | Set.InjOn ⇑(f a * (f a + 1)).factorization ↑(f a * (f a + 1)).primeFactors}),
      Nat.factorization_mul (byS:Set ℕ := {p | Nat.Prime p ∧ Nat.Prime (8 * p ^ 2 - 1)}h:S.Infinitef:ℕ → ℕ := fun p ↦ 8 * p ^ 2 - 1hS:∀ (p : ℕ), Nat.Prime p → 1 < 8 * p ^ 2this✝:Set.InjOn f Sp:ℕhp:Nat.Prime php':Nat.Prime (8 * p ^ 2 - 1)hp'':¬p = 2this:2 ≤ p⊢ 8 ≠ 0S:Set ℕ := {p | Nat.Prime p ∧ Nat.Prime (8 * p ^ 2 - 1)}h:S.Infinitef:ℕ → ℕ := fun p ↦ 8 * p ^ 2 - 1hS:∀ (p : ℕ), Nat.Prime p → 1 < 8 * p ^ 2this:Set.InjOn f Sp:ℕhp:Nat.Prime php':Nat.Prime (8 * p ^ 2 - 1)hp'':¬p = 2fac:(f p * (f p + 1)).factorization = (fun₀ | 8 * p ^ 2 - 1 => 1) + ((fun₀ | p => 2) + fun₀ | 2 => 3)⊢ p ∈ {a | Set.InjOn ⇑(f a * (f a + 1)).factorization ↑(f a * (f a + 1)).primeFactors} positivityAll goals completed! 🐙S:Set ℕ := {p | Nat.Prime p ∧ Nat.Prime (8 * p ^ 2 - 1)}h:S.Infinitef:ℕ → ℕ := fun p ↦ 8 * p ^ 2 - 1hS:∀ (p : ℕ), Nat.Prime p → 1 < 8 * p ^ 2this:Set.InjOn f Sp:ℕhp:Nat.Prime php':Nat.Prime (8 * p ^ 2 - 1)hp'':¬p = 2fac:(f p * (f p + 1)).factorization = (fun₀ | 8 * p ^ 2 - 1 => 1) + ((fun₀ | p => 2) + fun₀ | 2 => 3)⊢ p ∈ {a | Set.InjOn ⇑(f a * (f a + 1)).factorization ↑(f a * (f a + 1)).primeFactors}) (byS:Set ℕ := {p | Nat.Prime p ∧ Nat.Prime (8 * p ^ 2 - 1)}h:S.Infinitef:ℕ → ℕ := fun p ↦ 8 * p ^ 2 - 1hS:∀ (p : ℕ), Nat.Prime p → 1 < 8 * p ^ 2this✝:Set.InjOn f Sp:ℕhp:Nat.Prime php':Nat.Prime (8 * p ^ 2 - 1)hp'':¬p = 2this:2 ≤ p⊢ p ^ 2 ≠ 0S:Set ℕ := {p | Nat.Prime p ∧ Nat.Prime (8 * p ^ 2 - 1)}h:S.Infinitef:ℕ → ℕ := fun p ↦ 8 * p ^ 2 - 1hS:∀ (p : ℕ), Nat.Prime p → 1 < 8 * p ^ 2this:Set.InjOn f Sp:ℕhp:Nat.Prime php':Nat.Prime (8 * p ^ 2 - 1)hp'':¬p = 2fac:(f p * (f p + 1)).factorization = (fun₀ | 8 * p ^ 2 - 1 => 1) + ((fun₀ | p => 2) + fun₀ | 2 => 3)⊢ p ∈ {a | Set.InjOn ⇑(f a * (f a + 1)).factorization ↑(f a * (f a + 1)).primeFactors} positivityAll goals completed! 🐙S:Set ℕ := {p | Nat.Prime p ∧ Nat.Prime (8 * p ^ 2 - 1)}h:S.Infinitef:ℕ → ℕ := fun p ↦ 8 * p ^ 2 - 1hS:∀ (p : ℕ), Nat.Prime p → 1 < 8 * p ^ 2this:Set.InjOn f Sp:ℕhp:Nat.Prime php':Nat.Prime (8 * p ^ 2 - 1)hp'':¬p = 2fac:(f p * (f p + 1)).factorization = (fun₀ | 8 * p ^ 2 - 1 => 1) + ((fun₀ | p => 2) + fun₀ | 2 => 3)⊢ p ∈ {a | Set.InjOn ⇑(f a * (f a + 1)).factorization ↑(f a * (f a + 1)).primeFactors}), hp'.factorization,S:Set ℕ := {p | Nat.Prime p ∧ Nat.Prime (8 * p ^ 2 - 1)}h:S.Infinitef:ℕ → ℕ := fun p ↦ 8 * p ^ 2 - 1hS:∀ (p : ℕ), Nat.Prime p → 1 < 8 * p ^ 2this✝:Set.InjOn f Sp:ℕhp:Nat.Prime php':Nat.Prime (8 * p ^ 2 - 1)hp'':¬p = 2this:2 ≤ p⊢ (fun₀ | 8 * p ^ 2 - 1 => 1) + (Nat.factorization 8 + (p ^ 2).factorization) =
  (fun₀ | 8 * p ^ 2 - 1 => 1) + ((fun₀ | p => 2) + fun₀ | 2 => 3)S:Set ℕ := {p | Nat.Prime p ∧ Nat.Prime (8 * p ^ 2 - 1)}h:S.Infinitef:ℕ → ℕ := fun p ↦ 8 * p ^ 2 - 1hS:∀ (p : ℕ), Nat.Prime p → 1 < 8 * p ^ 2this:Set.InjOn f Sp:ℕhp:Nat.Prime php':Nat.Prime (8 * p ^ 2 - 1)hp'':¬p = 2fac:(f p * (f p + 1)).factorization = (fun₀ | 8 * p ^ 2 - 1 => 1) + ((fun₀ | p => 2) + fun₀ | 2 => 3)⊢ p ∈ {a | Set.InjOn ⇑(f a * (f a + 1)).factorization ↑(f a * (f a + 1)).primeFactors}
      hp.factorization_pow,S:Set ℕ := {p | Nat.Prime p ∧ Nat.Prime (8 * p ^ 2 - 1)}h:S.Infinitef:ℕ → ℕ := fun p ↦ 8 * p ^ 2 - 1hS:∀ (p : ℕ), Nat.Prime p → 1 < 8 * p ^ 2this✝:Set.InjOn f Sp:ℕhp:Nat.Prime php':Nat.Prime (8 * p ^ 2 - 1)hp'':¬p = 2this:2 ≤ p⊢ (fun₀ | 8 * p ^ 2 - 1 => 1) + (Nat.factorization 8 + fun₀ | p => 2) =
  (fun₀ | 8 * p ^ 2 - 1 => 1) + ((fun₀ | p => 2) + fun₀ | 2 => 3)S:Set ℕ := {p | Nat.Prime p ∧ Nat.Prime (8 * p ^ 2 - 1)}h:S.Infinitef:ℕ → ℕ := fun p ↦ 8 * p ^ 2 - 1hS:∀ (p : ℕ), Nat.Prime p → 1 < 8 * p ^ 2this:Set.InjOn f Sp:ℕhp:Nat.Prime php':Nat.Prime (8 * p ^ 2 - 1)hp'':¬p = 2fac:(f p * (f p + 1)).factorization = (fun₀ | 8 * p ^ 2 - 1 => 1) + ((fun₀ | p => 2) + fun₀ | 2 => 3)⊢ p ∈ {a | Set.InjOn ⇑(f a * (f a + 1)).factorization ↑(f a * (f a + 1)).primeFactors} (show 8 = 2 ^ 3 from rfl),S:Set ℕ := {p | Nat.Prime p ∧ Nat.Prime (8 * p ^ 2 - 1)}h:S.Infinitef:ℕ → ℕ := fun p ↦ 8 * p ^ 2 - 1hS:∀ (p : ℕ), Nat.Prime p → 1 < 8 * p ^ 2this✝:Set.InjOn f Sp:ℕhp:Nat.Prime php':Nat.Prime (8 * p ^ 2 - 1)hp'':¬p = 2this:2 ≤ p⊢ (fun₀ | 2 ^ 3 * p ^ 2 - 1 => 1) + ((2 ^ 3).factorization + fun₀ | p => 2) =
  (fun₀ | 2 ^ 3 * p ^ 2 - 1 => 1) + ((fun₀ | p => 2) + fun₀ | 2 => 3)S:Set ℕ := {p | Nat.Prime p ∧ Nat.Prime (8 * p ^ 2 - 1)}h:S.Infinitef:ℕ → ℕ := fun p ↦ 8 * p ^ 2 - 1hS:∀ (p : ℕ), Nat.Prime p → 1 < 8 * p ^ 2this:Set.InjOn f Sp:ℕhp:Nat.Prime php':Nat.Prime (8 * p ^ 2 - 1)hp'':¬p = 2fac:(f p * (f p + 1)).factorization = (fun₀ | 8 * p ^ 2 - 1 => 1) + ((fun₀ | p => 2) + fun₀ | 2 => 3)⊢ p ∈ {a | Set.InjOn ⇑(f a * (f a + 1)).factorization ↑(f a * (f a + 1)).primeFactors} Nat.prime_two.factorization_pow,S:Set ℕ := {p | Nat.Prime p ∧ Nat.Prime (8 * p ^ 2 - 1)}h:S.Infinitef:ℕ → ℕ := fun p ↦ 8 * p ^ 2 - 1hS:∀ (p : ℕ), Nat.Prime p → 1 < 8 * p ^ 2this✝:Set.InjOn f Sp:ℕhp:Nat.Prime php':Nat.Prime (8 * p ^ 2 - 1)hp'':¬p = 2this:2 ≤ p⊢ (fun₀ | 2 ^ 3 * p ^ 2 - 1 => 1) + ((fun₀ | 2 => 3) + fun₀ | p => 2) =
  (fun₀ | 2 ^ 3 * p ^ 2 - 1 => 1) + ((fun₀ | p => 2) + fun₀ | 2 => 3)S:Set ℕ := {p | Nat.Prime p ∧ Nat.Prime (8 * p ^ 2 - 1)}h:S.Infinitef:ℕ → ℕ := fun p ↦ 8 * p ^ 2 - 1hS:∀ (p : ℕ), Nat.Prime p → 1 < 8 * p ^ 2this:Set.InjOn f Sp:ℕhp:Nat.Prime php':Nat.Prime (8 * p ^ 2 - 1)hp'':¬p = 2fac:(f p * (f p + 1)).factorization = (fun₀ | 8 * p ^ 2 - 1 => 1) + ((fun₀ | p => 2) + fun₀ | 2 => 3)⊢ p ∈ {a | Set.InjOn ⇑(f a * (f a + 1)).factorization ↑(f a * (f a + 1)).primeFactors}
      add_comm (Finsupp.single 2 3)S:Set ℕ := {p | Nat.Prime p ∧ Nat.Prime (8 * p ^ 2 - 1)}h:S.Infinitef:ℕ → ℕ := fun p ↦ 8 * p ^ 2 - 1hS:∀ (p : ℕ), Nat.Prime p → 1 < 8 * p ^ 2this✝:Set.InjOn f Sp:ℕhp:Nat.Prime php':Nat.Prime (8 * p ^ 2 - 1)hp'':¬p = 2this:2 ≤ p⊢ (fun₀ | 2 ^ 3 * p ^ 2 - 1 => 1) + ((fun₀ | p => 2) + fun₀ | 2 => 3) =
  (fun₀ | 2 ^ 3 * p ^ 2 - 1 => 1) + ((fun₀ | p => 2) + fun₀ | 2 => 3)S:Set ℕ := {p | Nat.Prime p ∧ Nat.Prime (8 * p ^ 2 - 1)}h:S.Infinitef:ℕ → ℕ := fun p ↦ 8 * p ^ 2 - 1hS:∀ (p : ℕ), Nat.Prime p → 1 < 8 * p ^ 2this:Set.InjOn f Sp:ℕhp:Nat.Prime php':Nat.Prime (8 * p ^ 2 - 1)hp'':¬p = 2fac:(f p * (f p + 1)).factorization = (fun₀ | 8 * p ^ 2 - 1 => 1) + ((fun₀ | p => 2) + fun₀ | 2 => 3)⊢ p ∈ {a | Set.InjOn ⇑(f a * (f a + 1)).factorization ↑(f a * (f a + 1)).primeFactors}]S:Set ℕ := {p | Nat.Prime p ∧ Nat.Prime (8 * p ^ 2 - 1)}h:S.Infinitef:ℕ → ℕ := fun p ↦ 8 * p ^ 2 - 1hS:∀ (p : ℕ), Nat.Prime p → 1 < 8 * p ^ 2this:Set.InjOn f Sp:ℕhp:Nat.Prime php':Nat.Prime (8 * p ^ 2 - 1)hp'':¬p = 2fac:(f p * (f p + 1)).factorization = (fun₀ | 8 * p ^ 2 - 1 => 1) + ((fun₀ | p => 2) + fun₀ | 2 => 3)⊢ p ∈ {a | Set.InjOn ⇑(f a * (f a + 1)).factorization ↑(f a * (f a + 1)).primeFactors}S:Set ℕ := {p | Nat.Prime p ∧ Nat.Prime (8 * p ^ 2 - 1)}h:S.Infinitef:ℕ → ℕ := fun p ↦ 8 * p ^ 2 - 1hS:∀ (p : ℕ), Nat.Prime p → 1 < 8 * p ^ 2this:Set.InjOn f Sp:ℕhp:Nat.Prime php':Nat.Prime (8 * p ^ 2 - 1)hp'':¬p = 2fac:(f p * (f p + 1)).factorization = (fun₀ | 8 * p ^ 2 - 1 => 1) + ((fun₀ | p => 2) + fun₀ | 2 => 3)⊢ p ∈ {a | Set.InjOn ⇑(f a * (f a + 1)).factorization ↑(f a * (f a + 1)).primeFactors}
  have aux₂ : (fun₀ | 2 => 3).support = {2} := byh:{p | Nat.Prime p ∧ Nat.Prime (8 * p ^ 2 - 1)}.Infinite⊢ {n | Set.InjOn ⇑(n * (n + 1)).factorization ↑(n * (n + 1)).primeFactors}.InfiniteS:Set ℕ := {p | Nat.Prime p ∧ Nat.Prime (8 * p ^ 2 - 1)}h:S.Infinitef:ℕ → ℕ := fun p ↦ 8 * p ^ 2 - 1hS:∀ (p : ℕ), Nat.Prime p → 1 < 8 * p ^ 2this:Set.InjOn f Sp:ℕhp:Nat.Prime php':Nat.Prime (8 * p ^ 2 - 1)hp'':¬p = 2fac:(f p * (f p + 1)).factorization = (fun₀ | 8 * p ^ 2 - 1 => 1) + ((fun₀ | p => 2) + fun₀ | 2 => 3)aux₂:(fun₀ | 2 => 3).support = {2}⊢ p ∈ {a | Set.InjOn ⇑(f a * (f a + 1)).factorization ↑(f a * (f a + 1)).primeFactors} simpS:Set ℕ := {p | Nat.Prime p ∧ Nat.Prime (8 * p ^ 2 - 1)}h:S.Infinitef:ℕ → ℕ := fun p ↦ 8 * p ^ 2 - 1hS:∀ (p : ℕ), Nat.Prime p → 1 < 8 * p ^ 2this:Set.InjOn f Sp:ℕhp:Nat.Prime php':Nat.Prime (8 * p ^ 2 - 1)hp'':¬p = 2fac:(f p * (f p + 1)).factorization = (fun₀ | 8 * p ^ 2 - 1 => 1) + ((fun₀ | p => 2) + fun₀ | 2 => 3)aux₂:(fun₀ | 2 => 3).support = {2}⊢ p ∈ {a | Set.InjOn ⇑(f a * (f a + 1)).factorization ↑(f a * (f a + 1)).primeFactors}S:Set ℕ := {p | Nat.Prime p ∧ Nat.Prime (8 * p ^ 2 - 1)}h:S.Infinitef:ℕ → ℕ := fun p ↦ 8 * p ^ 2 - 1hS:∀ (p : ℕ), Nat.Prime p → 1 < 8 * p ^ 2this:Set.InjOn f Sp:ℕhp:Nat.Prime php':Nat.Prime (8 * p ^ 2 - 1)hp'':¬p = 2fac:(f p * (f p + 1)).factorization = (fun₀ | 8 * p ^ 2 - 1 => 1) + ((fun₀ | p => 2) + fun₀ | 2 => 3)aux₂:(fun₀ | 2 => 3).support = {2}⊢ p ∈ {a | Set.InjOn ⇑(f a * (f a + 1)).factorization ↑(f a * (f a + 1)).primeFactors}
  have aux₁ : ((fun₀ | p => 2) + fun₀ | 2 => 3).support = {p, 2} := byh:{p | Nat.Prime p ∧ Nat.Prime (8 * p ^ 2 - 1)}.Infinite⊢ {n | Set.InjOn ⇑(n * (n + 1)).factorization ↑(n * (n + 1)).primeFactors}.InfiniteS:Set ℕ := {p | Nat.Prime p ∧ Nat.Prime (8 * p ^ 2 - 1)}h:S.Infinitef:ℕ → ℕ := fun p ↦ 8 * p ^ 2 - 1hS:∀ (p : ℕ), Nat.Prime p → 1 < 8 * p ^ 2this:Set.InjOn f Sp:ℕhp:Nat.Prime php':Nat.Prime (8 * p ^ 2 - 1)hp'':¬p = 2fac:(f p * (f p + 1)).factorization = (fun₀ | 8 * p ^ 2 - 1 => 1) + ((fun₀ | p => 2) + fun₀ | 2 => 3)aux₂:(fun₀ | 2 => 3).support = {2}aux₁:((fun₀ | p => 2) + fun₀ | 2 => 3).support = {p, 2}⊢ p ∈ {a | Set.InjOn ⇑(f a * (f a + 1)).factorization ↑(f a * (f a + 1)).primeFactors}
    rw [Finsupp.support_single_add (byS:Set ℕ := {p | Nat.Prime p ∧ Nat.Prime (8 * p ^ 2 - 1)}h:S.Infinitef:ℕ → ℕ := fun p ↦ 8 * p ^ 2 - 1hS:∀ (p : ℕ), Nat.Prime p → 1 < 8 * p ^ 2this:Set.InjOn f Sp:ℕhp:Nat.Prime php':Nat.Prime (8 * p ^ 2 - 1)hp'':¬p = 2fac:(f p * (f p + 1)).factorization = (fun₀ | 8 * p ^ 2 - 1 => 1) + ((fun₀ | p => 2) + fun₀ | 2 => 3)aux₂:(fun₀ | 2 => 3).support = {2}⊢ p ∉ (fun₀ | 2 => 3).supportS:Set ℕ := {p | Nat.Prime p ∧ Nat.Prime (8 * p ^ 2 - 1)}h:S.Infinitef:ℕ → ℕ := fun p ↦ 8 * p ^ 2 - 1hS:∀ (p : ℕ), Nat.Prime p → 1 < 8 * p ^ 2this:Set.InjOn f Sp:ℕhp:Nat.Prime php':Nat.Prime (8 * p ^ 2 - 1)hp'':¬p = 2fac:(f p * (f p + 1)).factorization = (fun₀ | 8 * p ^ 2 - 1 => 1) + ((fun₀ | p => 2) + fun₀ | 2 => 3)aux₂:(fun₀ | 2 => 3).support = {2}aux₁:((fun₀ | p => 2) + fun₀ | 2 => 3).support = {p, 2}⊢ p ∈ {a | Set.InjOn ⇑(f a * (f a + 1)).factorization ↑(f a * (f a + 1)).primeFactors} simp [hp'']All goals completed! 🐙S:Set ℕ := {p | Nat.Prime p ∧ Nat.Prime (8 * p ^ 2 - 1)}h:S.Infinitef:ℕ → ℕ := fun p ↦ 8 * p ^ 2 - 1hS:∀ (p : ℕ), Nat.Prime p → 1 < 8 * p ^ 2this:Set.InjOn f Sp:ℕhp:Nat.Prime php':Nat.Prime (8 * p ^ 2 - 1)hp'':¬p = 2fac:(f p * (f p + 1)).factorization = (fun₀ | 8 * p ^ 2 - 1 => 1) + ((fun₀ | p => 2) + fun₀ | 2 => 3)aux₂:(fun₀ | 2 => 3).support = {2}aux₁:((fun₀ | p => 2) + fun₀ | 2 => 3).support = {p, 2}⊢ p ∈ {a | Set.InjOn ⇑(f a * (f a + 1)).factorization ↑(f a * (f a + 1)).primeFactors}) (byS:Set ℕ := {p | Nat.Prime p ∧ Nat.Prime (8 * p ^ 2 - 1)}h:S.Infinitef:ℕ → ℕ := fun p ↦ 8 * p ^ 2 - 1hS:∀ (p : ℕ), Nat.Prime p → 1 < 8 * p ^ 2this:Set.InjOn f Sp:ℕhp:Nat.Prime php':Nat.Prime (8 * p ^ 2 - 1)hp'':¬p = 2fac:(f p * (f p + 1)).factorization = (fun₀ | 8 * p ^ 2 - 1 => 1) + ((fun₀ | p => 2) + fun₀ | 2 => 3)aux₂:(fun₀ | 2 => 3).support = {2}⊢ 2 ≠ 0S:Set ℕ := {p | Nat.Prime p ∧ Nat.Prime (8 * p ^ 2 - 1)}h:S.Infinitef:ℕ → ℕ := fun p ↦ 8 * p ^ 2 - 1hS:∀ (p : ℕ), Nat.Prime p → 1 < 8 * p ^ 2this:Set.InjOn f Sp:ℕhp:Nat.Prime php':Nat.Prime (8 * p ^ 2 - 1)hp'':¬p = 2fac:(f p * (f p + 1)).factorization = (fun₀ | 8 * p ^ 2 - 1 => 1) + ((fun₀ | p => 2) + fun₀ | 2 => 3)aux₂:(fun₀ | 2 => 3).support = {2}aux₁:((fun₀ | p => 2) + fun₀ | 2 => 3).support = {p, 2}⊢ p ∈ {a | Set.InjOn ⇑(f a * (f a + 1)).factorization ↑(f a * (f a + 1)).primeFactors} simpAll goals completed! 🐙S:Set ℕ := {p | Nat.Prime p ∧ Nat.Prime (8 * p ^ 2 - 1)}h:S.Infinitef:ℕ → ℕ := fun p ↦ 8 * p ^ 2 - 1hS:∀ (p : ℕ), Nat.Prime p → 1 < 8 * p ^ 2this:Set.InjOn f Sp:ℕhp:Nat.Prime php':Nat.Prime (8 * p ^ 2 - 1)hp'':¬p = 2fac:(f p * (f p + 1)).factorization = (fun₀ | 8 * p ^ 2 - 1 => 1) + ((fun₀ | p => 2) + fun₀ | 2 => 3)aux₂:(fun₀ | 2 => 3).support = {2}aux₁:((fun₀ | p => 2) + fun₀ | 2 => 3).support = {p, 2}⊢ p ∈ {a | Set.InjOn ⇑(f a * (f a + 1)).factorization ↑(f a * (f a + 1)).primeFactors}), Finset.cons_eq_insert,S:Set ℕ := {p | Nat.Prime p ∧ Nat.Prime (8 * p ^ 2 - 1)}h:S.Infinitef:ℕ → ℕ := fun p ↦ 8 * p ^ 2 - 1hS:∀ (p : ℕ), Nat.Prime p → 1 < 8 * p ^ 2this:Set.InjOn f Sp:ℕhp:Nat.Prime php':Nat.Prime (8 * p ^ 2 - 1)hp'':¬p = 2fac:(f p * (f p + 1)).factorization = (fun₀ | 8 * p ^ 2 - 1 => 1) + ((fun₀ | p => 2) + fun₀ | 2 => 3)aux₂:(fun₀ | 2 => 3).support = {2}⊢ insert p (fun₀ | 2 => 3).support = {p, 2}S:Set ℕ := {p | Nat.Prime p ∧ Nat.Prime (8 * p ^ 2 - 1)}h:S.Infinitef:ℕ → ℕ := fun p ↦ 8 * p ^ 2 - 1hS:∀ (p : ℕ), Nat.Prime p → 1 < 8 * p ^ 2this:Set.InjOn f Sp:ℕhp:Nat.Prime php':Nat.Prime (8 * p ^ 2 - 1)hp'':¬p = 2fac:(f p * (f p + 1)).factorization = (fun₀ | 8 * p ^ 2 - 1 => 1) + ((fun₀ | p => 2) + fun₀ | 2 => 3)aux₂:(fun₀ | 2 => 3).support = {2}aux₁:((fun₀ | p => 2) + fun₀ | 2 => 3).support = {p, 2}⊢ p ∈ {a | Set.InjOn ⇑(f a * (f a + 1)).factorization ↑(f a * (f a + 1)).primeFactors} aux₂S:Set ℕ := {p | Nat.Prime p ∧ Nat.Prime (8 * p ^ 2 - 1)}h:S.Infinitef:ℕ → ℕ := fun p ↦ 8 * p ^ 2 - 1hS:∀ (p : ℕ), Nat.Prime p → 1 < 8 * p ^ 2this:Set.InjOn f Sp:ℕhp:Nat.Prime php':Nat.Prime (8 * p ^ 2 - 1)hp'':¬p = 2fac:(f p * (f p + 1)).factorization = (fun₀ | 8 * p ^ 2 - 1 => 1) + ((fun₀ | p => 2) + fun₀ | 2 => 3)aux₂:(fun₀ | 2 => 3).support = {2}⊢ {p, 2} = {p, 2}S:Set ℕ := {p | Nat.Prime p ∧ Nat.Prime (8 * p ^ 2 - 1)}h:S.Infinitef:ℕ → ℕ := fun p ↦ 8 * p ^ 2 - 1hS:∀ (p : ℕ), Nat.Prime p → 1 < 8 * p ^ 2this:Set.InjOn f Sp:ℕhp:Nat.Prime php':Nat.Prime (8 * p ^ 2 - 1)hp'':¬p = 2fac:(f p * (f p + 1)).factorization = (fun₀ | 8 * p ^ 2 - 1 => 1) + ((fun₀ | p => 2) + fun₀ | 2 => 3)aux₂:(fun₀ | 2 => 3).support = {2}aux₁:((fun₀ | p => 2) + fun₀ | 2 => 3).support = {p, 2}⊢ p ∈ {a | Set.InjOn ⇑(f a * (f a + 1)).factorization ↑(f a * (f a + 1)).primeFactors}]S:Set ℕ := {p | Nat.Prime p ∧ Nat.Prime (8 * p ^ 2 - 1)}h:S.Infinitef:ℕ → ℕ := fun p ↦ 8 * p ^ 2 - 1hS:∀ (p : ℕ), Nat.Prime p → 1 < 8 * p ^ 2this:Set.InjOn f Sp:ℕhp:Nat.Prime php':Nat.Prime (8 * p ^ 2 - 1)hp'':¬p = 2fac:(f p * (f p + 1)).factorization = (fun₀ | 8 * p ^ 2 - 1 => 1) + ((fun₀ | p => 2) + fun₀ | 2 => 3)aux₂:(fun₀ | 2 => 3).support = {2}aux₁:((fun₀ | p => 2) + fun₀ | 2 => 3).support = {p, 2}⊢ p ∈ {a | Set.InjOn ⇑(f a * (f a + 1)).factorization ↑(f a * (f a + 1)).primeFactors}S:Set ℕ := {p | Nat.Prime p ∧ Nat.Prime (8 * p ^ 2 - 1)}h:S.Infinitef:ℕ → ℕ := fun p ↦ 8 * p ^ 2 - 1hS:∀ (p : ℕ), Nat.Prime p → 1 < 8 * p ^ 2this:Set.InjOn f Sp:ℕhp:Nat.Prime php':Nat.Prime (8 * p ^ 2 - 1)hp'':¬p = 2fac:(f p * (f p + 1)).factorization = (fun₀ | 8 * p ^ 2 - 1 => 1) + ((fun₀ | p => 2) + fun₀ | 2 => 3)aux₂:(fun₀ | 2 => 3).support = {2}aux₁:((fun₀ | p => 2) + fun₀ | 2 => 3).support = {p, 2}⊢ p ∈ {a | Set.InjOn ⇑(f a * (f a + 1)).factorization ↑(f a * (f a + 1)).primeFactors}
  have aux₃ : p + 1 < 8 * p ^ 2 := byh:{p | Nat.Prime p ∧ Nat.Prime (8 * p ^ 2 - 1)}.Infinite⊢ {n | Set.InjOn ⇑(n * (n + 1)).factorization ↑(n * (n + 1)).primeFactors}.InfiniteS:Set ℕ := {p | Nat.Prime p ∧ Nat.Prime (8 * p ^ 2 - 1)}h:S.Infinitef:ℕ → ℕ := fun p ↦ 8 * p ^ 2 - 1hS:∀ (p : ℕ), Nat.Prime p → 1 < 8 * p ^ 2this:Set.InjOn f Sp:ℕhp:Nat.Prime php':Nat.Prime (8 * p ^ 2 - 1)hp'':¬p = 2fac:(f p * (f p + 1)).factorization = (fun₀ | 8 * p ^ 2 - 1 => 1) + ((fun₀ | p => 2) + fun₀ | 2 => 3)aux₂:(fun₀ | 2 => 3).support = {2}aux₁:((fun₀ | p => 2) + fun₀ | 2 => 3).support = {p, 2}aux₃:p + 1 < 8 * p ^ 2⊢ p ∈ {a | Set.InjOn ⇑(f a * (f a + 1)).factorization ↑(f a * (f a + 1)).primeFactors}
    replace hp := hp.two_leS:Set ℕ := {p | Nat.Prime p ∧ Nat.Prime (8 * p ^ 2 - 1)}h:S.Infinitef:ℕ → ℕ := fun p ↦ 8 * p ^ 2 - 1hS:∀ (p : ℕ), Nat.Prime p → 1 < 8 * p ^ 2this:Set.InjOn f Sp:ℕhp':Nat.Prime (8 * p ^ 2 - 1)hp'':¬p = 2fac:(f p * (f p + 1)).factorization = (fun₀ | 8 * p ^ 2 - 1 => 1) + ((fun₀ | p => 2) + fun₀ | 2 => 3)aux₂:(fun₀ | 2 => 3).support = {2}aux₁:((fun₀ | p => 2) + fun₀ | 2 => 3).support = {p, 2}hp:2 ≤ p⊢ p + 1 < 8 * p ^ 2S:Set ℕ := {p | Nat.Prime p ∧ Nat.Prime (8 * p ^ 2 - 1)}h:S.Infinitef:ℕ → ℕ := fun p ↦ 8 * p ^ 2 - 1hS:∀ (p : ℕ), Nat.Prime p → 1 < 8 * p ^ 2this:Set.InjOn f Sp:ℕhp:Nat.Prime php':Nat.Prime (8 * p ^ 2 - 1)hp'':¬p = 2fac:(f p * (f p + 1)).factorization = (fun₀ | 8 * p ^ 2 - 1 => 1) + ((fun₀ | p => 2) + fun₀ | 2 => 3)aux₂:(fun₀ | 2 => 3).support = {2}aux₁:((fun₀ | p => 2) + fun₀ | 2 => 3).support = {p, 2}aux₃:p + 1 < 8 * p ^ 2⊢ p ∈ {a | Set.InjOn ⇑(f a * (f a + 1)).factorization ↑(f a * (f a + 1)).primeFactors}
    zify at hp ⊢S:Set ℕ := {p | Nat.Prime p ∧ Nat.Prime (8 * p ^ 2 - 1)}h:S.Infinitef:ℕ → ℕ := fun p ↦ 8 * p ^ 2 - 1hS:∀ (p : ℕ), Nat.Prime p → 1 < 8 * p ^ 2this:Set.InjOn f Sp:ℕhp':Nat.Prime (8 * p ^ 2 - 1)hp'':¬p = 2fac:(f p * (f p + 1)).factorization = (fun₀ | 8 * p ^ 2 - 1 => 1) + ((fun₀ | p => 2) + fun₀ | 2 => 3)aux₂:(fun₀ | 2 => 3).support = {2}aux₁:((fun₀ | p => 2) + fun₀ | 2 => 3).support = {p, 2}hp:2 ≤ ↑p⊢ ↑p + 1 < 8 * ↑p ^ 2S:Set ℕ := {p | Nat.Prime p ∧ Nat.Prime (8 * p ^ 2 - 1)}h:S.Infinitef:ℕ → ℕ := fun p ↦ 8 * p ^ 2 - 1hS:∀ (p : ℕ), Nat.Prime p → 1 < 8 * p ^ 2this:Set.InjOn f Sp:ℕhp:Nat.Prime php':Nat.Prime (8 * p ^ 2 - 1)hp'':¬p = 2fac:(f p * (f p + 1)).factorization = (fun₀ | 8 * p ^ 2 - 1 => 1) + ((fun₀ | p => 2) + fun₀ | 2 => 3)aux₂:(fun₀ | 2 => 3).support = {2}aux₁:((fun₀ | p => 2) + fun₀ | 2 => 3).support = {p, 2}aux₃:p + 1 < 8 * p ^ 2⊢ p ∈ {a | Set.InjOn ⇑(f a * (f a + 1)).factorization ↑(f a * (f a + 1)).primeFactors}
    linear_combination (8 * p + 15 : ℤ) * hpS:Set ℕ := {p | Nat.Prime p ∧ Nat.Prime (8 * p ^ 2 - 1)}h:S.Infinitef:ℕ → ℕ := fun p ↦ 8 * p ^ 2 - 1hS:∀ (p : ℕ), Nat.Prime p → 1 < 8 * p ^ 2this:Set.InjOn f Sp:ℕhp:Nat.Prime php':Nat.Prime (8 * p ^ 2 - 1)hp'':¬p = 2fac:(f p * (f p + 1)).factorization = (fun₀ | 8 * p ^ 2 - 1 => 1) + ((fun₀ | p => 2) + fun₀ | 2 => 3)aux₂:(fun₀ | 2 => 3).support = {2}aux₁:((fun₀ | p => 2) + fun₀ | 2 => 3).support = {p, 2}aux₃:p + 1 < 8 * p ^ 2⊢ p ∈ {a | Set.InjOn ⇑(f a * (f a + 1)).factorization ↑(f a * (f a + 1)).primeFactors}S:Set ℕ := {p | Nat.Prime p ∧ Nat.Prime (8 * p ^ 2 - 1)}h:S.Infinitef:ℕ → ℕ := fun p ↦ 8 * p ^ 2 - 1hS:∀ (p : ℕ), Nat.Prime p → 1 < 8 * p ^ 2this:Set.InjOn f Sp:ℕhp:Nat.Prime php':Nat.Prime (8 * p ^ 2 - 1)hp'':¬p = 2fac:(f p * (f p + 1)).factorization = (fun₀ | 8 * p ^ 2 - 1 => 1) + ((fun₀ | p => 2) + fun₀ | 2 => 3)aux₂:(fun₀ | 2 => 3).support = {2}aux₁:((fun₀ | p => 2) + fun₀ | 2 => 3).support = {p, 2}aux₃:p + 1 < 8 * p ^ 2⊢ p ∈ {a | Set.InjOn ⇑(f a * (f a + 1)).factorization ↑(f a * (f a + 1)).primeFactors}
  have aux₄ : 8 * p ^ 2 - 1 ≠ p := byh:{p | Nat.Prime p ∧ Nat.Prime (8 * p ^ 2 - 1)}.Infinite⊢ {n | Set.InjOn ⇑(n * (n + 1)).factorization ↑(n * (n + 1)).primeFactors}.InfiniteS:Set ℕ := {p | Nat.Prime p ∧ Nat.Prime (8 * p ^ 2 - 1)}h:S.Infinitef:ℕ → ℕ := fun p ↦ 8 * p ^ 2 - 1hS:∀ (p : ℕ), Nat.Prime p → 1 < 8 * p ^ 2this:Set.InjOn f Sp:ℕhp:Nat.Prime php':Nat.Prime (8 * p ^ 2 - 1)hp'':¬p = 2fac:(f p * (f p + 1)).factorization = (fun₀ | 8 * p ^ 2 - 1 => 1) + ((fun₀ | p => 2) + fun₀ | 2 => 3)aux₂:(fun₀ | 2 => 3).support = {2}aux₁:((fun₀ | p => 2) + fun₀ | 2 => 3).support = {p, 2}aux₃:p + 1 < 8 * p ^ 2aux₄:8 * p ^ 2 - 1 ≠ p⊢ p ∈ {a | Set.InjOn ⇑(f a * (f a + 1)).factorization ↑(f a * (f a + 1)).primeFactors}
    rw [ne_eq,S:Set ℕ := {p | Nat.Prime p ∧ Nat.Prime (8 * p ^ 2 - 1)}h:S.Infinitef:ℕ → ℕ := fun p ↦ 8 * p ^ 2 - 1hS:∀ (p : ℕ), Nat.Prime p → 1 < 8 * p ^ 2this:Set.InjOn f Sp:ℕhp:Nat.Prime php':Nat.Prime (8 * p ^ 2 - 1)hp'':¬p = 2fac:(f p * (f p + 1)).factorization = (fun₀ | 8 * p ^ 2 - 1 => 1) + ((fun₀ | p => 2) + fun₀ | 2 => 3)aux₂:(fun₀ | 2 => 3).support = {2}aux₁:((fun₀ | p => 2) + fun₀ | 2 => 3).support = {p, 2}aux₃:p + 1 < 8 * p ^ 2⊢ ¬8 * p ^ 2 - 1 = pS:Set ℕ := {p | Nat.Prime p ∧ Nat.Prime (8 * p ^ 2 - 1)}h:S.Infinitef:ℕ → ℕ := fun p ↦ 8 * p ^ 2 - 1hS:∀ (p : ℕ), Nat.Prime p → 1 < 8 * p ^ 2this:Set.InjOn f Sp:ℕhp:Nat.Prime php':Nat.Prime (8 * p ^ 2 - 1)hp'':¬p = 2fac:(f p * (f p + 1)).factorization = (fun₀ | 8 * p ^ 2 - 1 => 1) + ((fun₀ | p => 2) + fun₀ | 2 => 3)aux₂:(fun₀ | 2 => 3).support = {2}aux₁:((fun₀ | p => 2) + fun₀ | 2 => 3).support = {p, 2}aux₃:p + 1 < 8 * p ^ 2⊢ ¬8 * p ^ 2 = p + 1S:Set ℕ := {p | Nat.Prime p ∧ Nat.Prime (8 * p ^ 2 - 1)}h:S.Infinitef:ℕ → ℕ := fun p ↦ 8 * p ^ 2 - 1hS:∀ (p : ℕ), Nat.Prime p → 1 < 8 * p ^ 2this:Set.InjOn f Sp:ℕhp:Nat.Prime php':Nat.Prime (8 * p ^ 2 - 1)hp'':¬p = 2fac:(f p * (f p + 1)).factorization = (fun₀ | 8 * p ^ 2 - 1 => 1) + ((fun₀ | p => 2) + fun₀ | 2 => 3)aux₂:(fun₀ | 2 => 3).support = {2}aux₁:((fun₀ | p => 2) + fun₀ | 2 => 3).support = {p, 2}aux₃:p + 1 < 8 * p ^ 2aux₄:8 * p ^ 2 - 1 ≠ p⊢ p ∈ {a | Set.InjOn ⇑(f a * (f a + 1)).factorization ↑(f a * (f a + 1)).primeFactors} tsub_eq_iff_eq_add_of_le (hS p hp).leS:Set ℕ := {p | Nat.Prime p ∧ Nat.Prime (8 * p ^ 2 - 1)}h:S.Infinitef:ℕ → ℕ := fun p ↦ 8 * p ^ 2 - 1hS:∀ (p : ℕ), Nat.Prime p → 1 < 8 * p ^ 2this:Set.InjOn f Sp:ℕhp:Nat.Prime php':Nat.Prime (8 * p ^ 2 - 1)hp'':¬p = 2fac:(f p * (f p + 1)).factorization = (fun₀ | 8 * p ^ 2 - 1 => 1) + ((fun₀ | p => 2) + fun₀ | 2 => 3)aux₂:(fun₀ | 2 => 3).support = {2}aux₁:((fun₀ | p => 2) + fun₀ | 2 => 3).support = {p, 2}aux₃:p + 1 < 8 * p ^ 2⊢ ¬8 * p ^ 2 = p + 1S:Set ℕ := {p | Nat.Prime p ∧ Nat.Prime (8 * p ^ 2 - 1)}h:S.Infinitef:ℕ → ℕ := fun p ↦ 8 * p ^ 2 - 1hS:∀ (p : ℕ), Nat.Prime p → 1 < 8 * p ^ 2this:Set.InjOn f Sp:ℕhp:Nat.Prime php':Nat.Prime (8 * p ^ 2 - 1)hp'':¬p = 2fac:(f p * (f p + 1)).factorization = (fun₀ | 8 * p ^ 2 - 1 => 1) + ((fun₀ | p => 2) + fun₀ | 2 => 3)aux₂:(fun₀ | 2 => 3).support = {2}aux₁:((fun₀ | p => 2) + fun₀ | 2 => 3).support = {p, 2}aux₃:p + 1 < 8 * p ^ 2⊢ ¬8 * p ^ 2 = p + 1S:Set ℕ := {p | Nat.Prime p ∧ Nat.Prime (8 * p ^ 2 - 1)}h:S.Infinitef:ℕ → ℕ := fun p ↦ 8 * p ^ 2 - 1hS:∀ (p : ℕ), Nat.Prime p → 1 < 8 * p ^ 2this:Set.InjOn f Sp:ℕhp:Nat.Prime php':Nat.Prime (8 * p ^ 2 - 1)hp'':¬p = 2fac:(f p * (f p + 1)).factorization = (fun₀ | 8 * p ^ 2 - 1 => 1) + ((fun₀ | p => 2) + fun₀ | 2 => 3)aux₂:(fun₀ | 2 => 3).support = {2}aux₁:((fun₀ | p => 2) + fun₀ | 2 => 3).support = {p, 2}aux₃:p + 1 < 8 * p ^ 2aux₄:8 * p ^ 2 - 1 ≠ p⊢ p ∈ {a | Set.InjOn ⇑(f a * (f a + 1)).factorization ↑(f a * (f a + 1)).primeFactors}]S:Set ℕ := {p | Nat.Prime p ∧ Nat.Prime (8 * p ^ 2 - 1)}h:S.Infinitef:ℕ → ℕ := fun p ↦ 8 * p ^ 2 - 1hS:∀ (p : ℕ), Nat.Prime p → 1 < 8 * p ^ 2this:Set.InjOn f Sp:ℕhp:Nat.Prime php':Nat.Prime (8 * p ^ 2 - 1)hp'':¬p = 2fac:(f p * (f p + 1)).factorization = (fun₀ | 8 * p ^ 2 - 1 => 1) + ((fun₀ | p => 2) + fun₀ | 2 => 3)aux₂:(fun₀ | 2 => 3).support = {2}aux₁:((fun₀ | p => 2) + fun₀ | 2 => 3).support = {p, 2}aux₃:p + 1 < 8 * p ^ 2⊢ ¬8 * p ^ 2 = p + 1S:Set ℕ := {p | Nat.Prime p ∧ Nat.Prime (8 * p ^ 2 - 1)}h:S.Infinitef:ℕ → ℕ := fun p ↦ 8 * p ^ 2 - 1hS:∀ (p : ℕ), Nat.Prime p → 1 < 8 * p ^ 2this:Set.InjOn f Sp:ℕhp:Nat.Prime php':Nat.Prime (8 * p ^ 2 - 1)hp'':¬p = 2fac:(f p * (f p + 1)).factorization = (fun₀ | 8 * p ^ 2 - 1 => 1) + ((fun₀ | p => 2) + fun₀ | 2 => 3)aux₂:(fun₀ | 2 => 3).support = {2}aux₁:((fun₀ | p => 2) + fun₀ | 2 => 3).support = {p, 2}aux₃:p + 1 < 8 * p ^ 2aux₄:8 * p ^ 2 - 1 ≠ p⊢ p ∈ {a | Set.InjOn ⇑(f a * (f a + 1)).factorization ↑(f a * (f a + 1)).primeFactors}
    exact aux₃.ne'S:Set ℕ := {p | Nat.Prime p ∧ Nat.Prime (8 * p ^ 2 - 1)}h:S.Infinitef:ℕ → ℕ := fun p ↦ 8 * p ^ 2 - 1hS:∀ (p : ℕ), Nat.Prime p → 1 < 8 * p ^ 2this:Set.InjOn f Sp:ℕhp:Nat.Prime php':Nat.Prime (8 * p ^ 2 - 1)hp'':¬p = 2fac:(f p * (f p + 1)).factorization = (fun₀ | 8 * p ^ 2 - 1 => 1) + ((fun₀ | p => 2) + fun₀ | 2 => 3)aux₂:(fun₀ | 2 => 3).support = {2}aux₁:((fun₀ | p => 2) + fun₀ | 2 => 3).support = {p, 2}aux₃:p + 1 < 8 * p ^ 2aux₄:8 * p ^ 2 - 1 ≠ p⊢ p ∈ {a | Set.InjOn ⇑(f a * (f a + 1)).factorization ↑(f a * (f a + 1)).primeFactors}S:Set ℕ := {p | Nat.Prime p ∧ Nat.Prime (8 * p ^ 2 - 1)}h:S.Infinitef:ℕ → ℕ := fun p ↦ 8 * p ^ 2 - 1hS:∀ (p : ℕ), Nat.Prime p → 1 < 8 * p ^ 2this:Set.InjOn f Sp:ℕhp:Nat.Prime php':Nat.Prime (8 * p ^ 2 - 1)hp'':¬p = 2fac:(f p * (f p + 1)).factorization = (fun₀ | 8 * p ^ 2 - 1 => 1) + ((fun₀ | p => 2) + fun₀ | 2 => 3)aux₂:(fun₀ | 2 => 3).support = {2}aux₁:((fun₀ | p => 2) + fun₀ | 2 => 3).support = {p, 2}aux₃:p + 1 < 8 * p ^ 2aux₄:8 * p ^ 2 - 1 ≠ p⊢ p ∈ {a | Set.InjOn ⇑(f a * (f a + 1)).factorization ↑(f a * (f a + 1)).primeFactors}
  have aux₅ : 8 * p ^ 2 - 1 ≠ 2 := byh:{p | Nat.Prime p ∧ Nat.Prime (8 * p ^ 2 - 1)}.Infinite⊢ {n | Set.InjOn ⇑(n * (n + 1)).factorization ↑(n * (n + 1)).primeFactors}.InfiniteS:Set ℕ := {p | Nat.Prime p ∧ Nat.Prime (8 * p ^ 2 - 1)}h:S.Infinitef:ℕ → ℕ := fun p ↦ 8 * p ^ 2 - 1hS:∀ (p : ℕ), Nat.Prime p → 1 < 8 * p ^ 2this:Set.InjOn f Sp:ℕhp:Nat.Prime php':Nat.Prime (8 * p ^ 2 - 1)hp'':¬p = 2fac:(f p * (f p + 1)).factorization = (fun₀ | 8 * p ^ 2 - 1 => 1) + ((fun₀ | p => 2) + fun₀ | 2 => 3)aux₂:(fun₀ | 2 => 3).support = {2}aux₁:((fun₀ | p => 2) + fun₀ | 2 => 3).support = {p, 2}aux₃:p + 1 < 8 * p ^ 2aux₄:8 * p ^ 2 - 1 ≠ paux₅:8 * p ^ 2 - 1 ≠ 2⊢ p ∈ {a | Set.InjOn ⇑(f a * (f a + 1)).factorization ↑(f a * (f a + 1)).primeFactors}
    omegaS:Set ℕ := {p | Nat.Prime p ∧ Nat.Prime (8 * p ^ 2 - 1)}h:S.Infinitef:ℕ → ℕ := fun p ↦ 8 * p ^ 2 - 1hS:∀ (p : ℕ), Nat.Prime p → 1 < 8 * p ^ 2this:Set.InjOn f Sp:ℕhp:Nat.Prime php':Nat.Prime (8 * p ^ 2 - 1)hp'':¬p = 2fac:(f p * (f p + 1)).factorization = (fun₀ | 8 * p ^ 2 - 1 => 1) + ((fun₀ | p => 2) + fun₀ | 2 => 3)aux₂:(fun₀ | 2 => 3).support = {2}aux₁:((fun₀ | p => 2) + fun₀ | 2 => 3).support = {p, 2}aux₃:p + 1 < 8 * p ^ 2aux₄:8 * p ^ 2 - 1 ≠ paux₅:8 * p ^ 2 - 1 ≠ 2⊢ p ∈ {a | Set.InjOn ⇑(f a * (f a + 1)).factorization ↑(f a * (f a + 1)).primeFactors}S:Set ℕ := {p | Nat.Prime p ∧ Nat.Prime (8 * p ^ 2 - 1)}h:S.Infinitef:ℕ → ℕ := fun p ↦ 8 * p ^ 2 - 1hS:∀ (p : ℕ), Nat.Prime p → 1 < 8 * p ^ 2this:Set.InjOn f Sp:ℕhp:Nat.Prime php':Nat.Prime (8 * p ^ 2 - 1)hp'':¬p = 2fac:(f p * (f p + 1)).factorization = (fun₀ | 8 * p ^ 2 - 1 => 1) + ((fun₀ | p => 2) + fun₀ | 2 => 3)aux₂:(fun₀ | 2 => 3).support = {2}aux₁:((fun₀ | p => 2) + fun₀ | 2 => 3).support = {p, 2}aux₃:p + 1 < 8 * p ^ 2aux₄:8 * p ^ 2 - 1 ≠ paux₅:8 * p ^ 2 - 1 ≠ 2⊢ p ∈ {a | Set.InjOn ⇑(f a * (f a + 1)).factorization ↑(f a * (f a + 1)).primeFactors}
  have pf : (f p * (f p + 1)).primeFactors = {8 * p ^ 2 - 1, p, 2} := byh:{p | Nat.Prime p ∧ Nat.Prime (8 * p ^ 2 - 1)}.Infinite⊢ {n | Set.InjOn ⇑(n * (n + 1)).factorization ↑(n * (n + 1)).primeFactors}.InfiniteS:Set ℕ := {p | Nat.Prime p ∧ Nat.Prime (8 * p ^ 2 - 1)}h:S.Infinitef:ℕ → ℕ := fun p ↦ 8 * p ^ 2 - 1hS:∀ (p : ℕ), Nat.Prime p → 1 < 8 * p ^ 2this:Set.InjOn f Sp:ℕhp:Nat.Prime php':Nat.Prime (8 * p ^ 2 - 1)hp'':¬p = 2fac:(f p * (f p + 1)).factorization = (fun₀ | 8 * p ^ 2 - 1 => 1) + ((fun₀ | p => 2) + fun₀ | 2 => 3)aux₂:(fun₀ | 2 => 3).support = {2}aux₁:((fun₀ | p => 2) + fun₀ | 2 => 3).support = {p, 2}aux₃:p + 1 < 8 * p ^ 2aux₄:8 * p ^ 2 - 1 ≠ paux₅:8 * p ^ 2 - 1 ≠ 2pf:(f p * (f p + 1)).primeFactors = {8 * p ^ 2 - 1, p, 2}⊢ p ∈ {a | Set.InjOn ⇑(f a * (f a + 1)).factorization ↑(f a * (f a + 1)).primeFactors}
    rw [← Nat.support_factorization,S:Set ℕ := {p | Nat.Prime p ∧ Nat.Prime (8 * p ^ 2 - 1)}h:S.Infinitef:ℕ → ℕ := fun p ↦ 8 * p ^ 2 - 1hS:∀ (p : ℕ), Nat.Prime p → 1 < 8 * p ^ 2this:Set.InjOn f Sp:ℕhp:Nat.Prime php':Nat.Prime (8 * p ^ 2 - 1)hp'':¬p = 2fac:(f p * (f p + 1)).factorization = (fun₀ | 8 * p ^ 2 - 1 => 1) + ((fun₀ | p => 2) + fun₀ | 2 => 3)aux₂:(fun₀ | 2 => 3).support = {2}aux₁:((fun₀ | p => 2) + fun₀ | 2 => 3).support = {p, 2}aux₃:p + 1 < 8 * p ^ 2aux₄:8 * p ^ 2 - 1 ≠ paux₅:8 * p ^ 2 - 1 ≠ 2⊢ (f p * (f p + 1)).factorization.support = {8 * p ^ 2 - 1, p, 2}S:Set ℕ := {p | Nat.Prime p ∧ Nat.Prime (8 * p ^ 2 - 1)}h:S.Infinitef:ℕ → ℕ := fun p ↦ 8 * p ^ 2 - 1hS:∀ (p : ℕ), Nat.Prime p → 1 < 8 * p ^ 2this:Set.InjOn f Sp:ℕhp:Nat.Prime php':Nat.Prime (8 * p ^ 2 - 1)hp'':¬p = 2fac:(f p * (f p + 1)).factorization = (fun₀ | 8 * p ^ 2 - 1 => 1) + ((fun₀ | p => 2) + fun₀ | 2 => 3)aux₂:(fun₀ | 2 => 3).support = {2}aux₁:((fun₀ | p => 2) + fun₀ | 2 => 3).support = {p, 2}aux₃:p + 1 < 8 * p ^ 2aux₄:8 * p ^ 2 - 1 ≠ paux₅:8 * p ^ 2 - 1 ≠ 2⊢ 8 * p ^ 2 - 1 ∉ ((fun₀ | p => 2) + fun₀ | 2 => 3).supportS:Set ℕ := {p | Nat.Prime p ∧ Nat.Prime (8 * p ^ 2 - 1)}h:S.Infinitef:ℕ → ℕ := fun p ↦ 8 * p ^ 2 - 1hS:∀ (p : ℕ), Nat.Prime p → 1 < 8 * p ^ 2this:Set.InjOn f Sp:ℕhp:Nat.Prime php':Nat.Prime (8 * p ^ 2 - 1)hp'':¬p = 2fac:(f p * (f p + 1)).factorization = (fun₀ | 8 * p ^ 2 - 1 => 1) + ((fun₀ | p => 2) + fun₀ | 2 => 3)aux₂:(fun₀ | 2 => 3).support = {2}aux₁:((fun₀ | p => 2) + fun₀ | 2 => 3).support = {p, 2}aux₃:p + 1 < 8 * p ^ 2aux₄:8 * p ^ 2 - 1 ≠ paux₅:8 * p ^ 2 - 1 ≠ 2pf:(f p * (f p + 1)).primeFactors = {8 * p ^ 2 - 1, p, 2}⊢ p ∈ {a | Set.InjOn ⇑(f a * (f a + 1)).factorization ↑(f a * (f a + 1)).primeFactors} fac,S:Set ℕ := {p | Nat.Prime p ∧ Nat.Prime (8 * p ^ 2 - 1)}h:S.Infinitef:ℕ → ℕ := fun p ↦ 8 * p ^ 2 - 1hS:∀ (p : ℕ), Nat.Prime p → 1 < 8 * p ^ 2this:Set.InjOn f Sp:ℕhp:Nat.Prime php':Nat.Prime (8 * p ^ 2 - 1)hp'':¬p = 2fac:(f p * (f p + 1)).factorization = (fun₀ | 8 * p ^ 2 - 1 => 1) + ((fun₀ | p => 2) + fun₀ | 2 => 3)aux₂:(fun₀ | 2 => 3).support = {2}aux₁:((fun₀ | p => 2) + fun₀ | 2 => 3).support = {p, 2}aux₃:p + 1 < 8 * p ^ 2aux₄:8 * p ^ 2 - 1 ≠ paux₅:8 * p ^ 2 - 1 ≠ 2⊢ ((fun₀ | 8 * p ^ 2 - 1 => 1) + ((fun₀ | p => 2) + fun₀ | 2 => 3)).support = {8 * p ^ 2 - 1, p, 2}S:Set ℕ := {p | Nat.Prime p ∧ Nat.Prime (8 * p ^ 2 - 1)}h:S.Infinitef:ℕ → ℕ := fun p ↦ 8 * p ^ 2 - 1hS:∀ (p : ℕ), Nat.Prime p → 1 < 8 * p ^ 2this:Set.InjOn f Sp:ℕhp:Nat.Prime php':Nat.Prime (8 * p ^ 2 - 1)hp'':¬p = 2fac:(f p * (f p + 1)).factorization = (fun₀ | 8 * p ^ 2 - 1 => 1) + ((fun₀ | p => 2) + fun₀ | 2 => 3)aux₂:(fun₀ | 2 => 3).support = {2}aux₁:((fun₀ | p => 2) + fun₀ | 2 => 3).support = {p, 2}aux₃:p + 1 < 8 * p ^ 2aux₄:8 * p ^ 2 - 1 ≠ paux₅:8 * p ^ 2 - 1 ≠ 2⊢ 8 * p ^ 2 - 1 ∉ ((fun₀ | p => 2) + fun₀ | 2 => 3).supportS:Set ℕ := {p | Nat.Prime p ∧ Nat.Prime (8 * p ^ 2 - 1)}h:S.Infinitef:ℕ → ℕ := fun p ↦ 8 * p ^ 2 - 1hS:∀ (p : ℕ), Nat.Prime p → 1 < 8 * p ^ 2this:Set.InjOn f Sp:ℕhp:Nat.Prime php':Nat.Prime (8 * p ^ 2 - 1)hp'':¬p = 2fac:(f p * (f p + 1)).factorization = (fun₀ | 8 * p ^ 2 - 1 => 1) + ((fun₀ | p => 2) + fun₀ | 2 => 3)aux₂:(fun₀ | 2 => 3).support = {2}aux₁:((fun₀ | p => 2) + fun₀ | 2 => 3).support = {p, 2}aux₃:p + 1 < 8 * p ^ 2aux₄:8 * p ^ 2 - 1 ≠ paux₅:8 * p ^ 2 - 1 ≠ 2pf:(f p * (f p + 1)).primeFactors = {8 * p ^ 2 - 1, p, 2}⊢ p ∈ {a | Set.InjOn ⇑(f a * (f a + 1)).factorization ↑(f a * (f a + 1)).primeFactors} Finsupp.support_single_add _ (byS:Set ℕ := {p | Nat.Prime p ∧ Nat.Prime (8 * p ^ 2 - 1)}h:S.Infinitef:ℕ → ℕ := fun p ↦ 8 * p ^ 2 - 1hS:∀ (p : ℕ), Nat.Prime p → 1 < 8 * p ^ 2this:Set.InjOn f Sp:ℕhp:Nat.Prime php':Nat.Prime (8 * p ^ 2 - 1)hp'':¬p = 2fac:(f p * (f p + 1)).factorization = (fun₀ | 8 * p ^ 2 - 1 => 1) + ((fun₀ | p => 2) + fun₀ | 2 => 3)aux₂:(fun₀ | 2 => 3).support = {2}aux₁:((fun₀ | p => 2) + fun₀ | 2 => 3).support = {p, 2}aux₃:p + 1 < 8 * p ^ 2aux₄:8 * p ^ 2 - 1 ≠ paux₅:8 * p ^ 2 - 1 ≠ 2⊢ 1 ≠ 0S:Set ℕ := {p | Nat.Prime p ∧ Nat.Prime (8 * p ^ 2 - 1)}h:S.Infinitef:ℕ → ℕ := fun p ↦ 8 * p ^ 2 - 1hS:∀ (p : ℕ), Nat.Prime p → 1 < 8 * p ^ 2this:Set.InjOn f Sp:ℕhp:Nat.Prime php':Nat.Prime (8 * p ^ 2 - 1)hp'':¬p = 2fac:(f p * (f p + 1)).factorization = (fun₀ | 8 * p ^ 2 - 1 => 1) + ((fun₀ | p => 2) + fun₀ | 2 => 3)aux₂:(fun₀ | 2 => 3).support = {2}aux₁:((fun₀ | p => 2) + fun₀ | 2 => 3).support = {p, 2}aux₃:p + 1 < 8 * p ^ 2aux₄:8 * p ^ 2 - 1 ≠ paux₅:8 * p ^ 2 - 1 ≠ 2⊢ 8 * p ^ 2 - 1 ∉ ((fun₀ | p => 2) + fun₀ | 2 => 3).supportS:Set ℕ := {p | Nat.Prime p ∧ Nat.Prime (8 * p ^ 2 - 1)}h:S.Infinitef:ℕ → ℕ := fun p ↦ 8 * p ^ 2 - 1hS:∀ (p : ℕ), Nat.Prime p → 1 < 8 * p ^ 2this:Set.InjOn f Sp:ℕhp:Nat.Prime php':Nat.Prime (8 * p ^ 2 - 1)hp'':¬p = 2fac:(f p * (f p + 1)).factorization = (fun₀ | 8 * p ^ 2 - 1 => 1) + ((fun₀ | p => 2) + fun₀ | 2 => 3)aux₂:(fun₀ | 2 => 3).support = {2}aux₁:((fun₀ | p => 2) + fun₀ | 2 => 3).support = {p, 2}aux₃:p + 1 < 8 * p ^ 2aux₄:8 * p ^ 2 - 1 ≠ paux₅:8 * p ^ 2 - 1 ≠ 2pf:(f p * (f p + 1)).primeFactors = {8 * p ^ 2 - 1, p, 2}⊢ p ∈ {a | Set.InjOn ⇑(f a * (f a + 1)).factorization ↑(f a * (f a + 1)).primeFactors} simpAll goals completed! 🐙S:Set ℕ := {p | Nat.Prime p ∧ Nat.Prime (8 * p ^ 2 - 1)}h:S.Infinitef:ℕ → ℕ := fun p ↦ 8 * p ^ 2 - 1hS:∀ (p : ℕ), Nat.Prime p → 1 < 8 * p ^ 2this:Set.InjOn f Sp:ℕhp:Nat.Prime php':Nat.Prime (8 * p ^ 2 - 1)hp'':¬p = 2fac:(f p * (f p + 1)).factorization = (fun₀ | 8 * p ^ 2 - 1 => 1) + ((fun₀ | p => 2) + fun₀ | 2 => 3)aux₂:(fun₀ | 2 => 3).support = {2}aux₁:((fun₀ | p => 2) + fun₀ | 2 => 3).support = {p, 2}aux₃:p + 1 < 8 * p ^ 2aux₄:8 * p ^ 2 - 1 ≠ paux₅:8 * p ^ 2 - 1 ≠ 2⊢ 8 * p ^ 2 - 1 ∉ ((fun₀ | p => 2) + fun₀ | 2 => 3).supportS:Set ℕ := {p | Nat.Prime p ∧ Nat.Prime (8 * p ^ 2 - 1)}h:S.Infinitef:ℕ → ℕ := fun p ↦ 8 * p ^ 2 - 1hS:∀ (p : ℕ), Nat.Prime p → 1 < 8 * p ^ 2this:Set.InjOn f Sp:ℕhp:Nat.Prime php':Nat.Prime (8 * p ^ 2 - 1)hp'':¬p = 2fac:(f p * (f p + 1)).factorization = (fun₀ | 8 * p ^ 2 - 1 => 1) + ((fun₀ | p => 2) + fun₀ | 2 => 3)aux₂:(fun₀ | 2 => 3).support = {2}aux₁:((fun₀ | p => 2) + fun₀ | 2 => 3).support = {p, 2}aux₃:p + 1 < 8 * p ^ 2aux₄:8 * p ^ 2 - 1 ≠ paux₅:8 * p ^ 2 - 1 ≠ 2pf:(f p * (f p + 1)).primeFactors = {8 * p ^ 2 - 1, p, 2}⊢ p ∈ {a | Set.InjOn ⇑(f a * (f a + 1)).factorization ↑(f a * (f a + 1)).primeFactors}),
      Finset.cons_eq_insert,S:Set ℕ := {p | Nat.Prime p ∧ Nat.Prime (8 * p ^ 2 - 1)}h:S.Infinitef:ℕ → ℕ := fun p ↦ 8 * p ^ 2 - 1hS:∀ (p : ℕ), Nat.Prime p → 1 < 8 * p ^ 2this:Set.InjOn f Sp:ℕhp:Nat.Prime php':Nat.Prime (8 * p ^ 2 - 1)hp'':¬p = 2fac:(f p * (f p + 1)).factorization = (fun₀ | 8 * p ^ 2 - 1 => 1) + ((fun₀ | p => 2) + fun₀ | 2 => 3)aux₂:(fun₀ | 2 => 3).support = {2}aux₁:((fun₀ | p => 2) + fun₀ | 2 => 3).support = {p, 2}aux₃:p + 1 < 8 * p ^ 2aux₄:8 * p ^ 2 - 1 ≠ paux₅:8 * p ^ 2 - 1 ≠ 2⊢ insert (8 * p ^ 2 - 1) ((fun₀ | p => 2) + fun₀ | 2 => 3).support = {8 * p ^ 2 - 1, p, 2}S:Set ℕ := {p | Nat.Prime p ∧ Nat.Prime (8 * p ^ 2 - 1)}h:S.Infinitef:ℕ → ℕ := fun p ↦ 8 * p ^ 2 - 1hS:∀ (p : ℕ), Nat.Prime p → 1 < 8 * p ^ 2this:Set.InjOn f Sp:ℕhp:Nat.Prime php':Nat.Prime (8 * p ^ 2 - 1)hp'':¬p = 2fac:(f p * (f p + 1)).factorization = (fun₀ | 8 * p ^ 2 - 1 => 1) + ((fun₀ | p => 2) + fun₀ | 2 => 3)aux₂:(fun₀ | 2 => 3).support = {2}aux₁:((fun₀ | p => 2) + fun₀ | 2 => 3).support = {p, 2}aux₃:p + 1 < 8 * p ^ 2aux₄:8 * p ^ 2 - 1 ≠ paux₅:8 * p ^ 2 - 1 ≠ 2⊢ 8 * p ^ 2 - 1 ∉ ((fun₀ | p => 2) + fun₀ | 2 => 3).supportS:Set ℕ := {p | Nat.Prime p ∧ Nat.Prime (8 * p ^ 2 - 1)}h:S.Infinitef:ℕ → ℕ := fun p ↦ 8 * p ^ 2 - 1hS:∀ (p : ℕ), Nat.Prime p → 1 < 8 * p ^ 2this:Set.InjOn f Sp:ℕhp:Nat.Prime php':Nat.Prime (8 * p ^ 2 - 1)hp'':¬p = 2fac:(f p * (f p + 1)).factorization = (fun₀ | 8 * p ^ 2 - 1 => 1) + ((fun₀ | p => 2) + fun₀ | 2 => 3)aux₂:(fun₀ | 2 => 3).support = {2}aux₁:((fun₀ | p => 2) + fun₀ | 2 => 3).support = {p, 2}aux₃:p + 1 < 8 * p ^ 2aux₄:8 * p ^ 2 - 1 ≠ paux₅:8 * p ^ 2 - 1 ≠ 2⊢ 8 * p ^ 2 - 1 ∉ ((fun₀ | p => 2) + fun₀ | 2 => 3).supportS:Set ℕ := {p | Nat.Prime p ∧ Nat.Prime (8 * p ^ 2 - 1)}h:S.Infinitef:ℕ → ℕ := fun p ↦ 8 * p ^ 2 - 1hS:∀ (p : ℕ), Nat.Prime p → 1 < 8 * p ^ 2this:Set.InjOn f Sp:ℕhp:Nat.Prime php':Nat.Prime (8 * p ^ 2 - 1)hp'':¬p = 2fac:(f p * (f p + 1)).factorization = (fun₀ | 8 * p ^ 2 - 1 => 1) + ((fun₀ | p => 2) + fun₀ | 2 => 3)aux₂:(fun₀ | 2 => 3).support = {2}aux₁:((fun₀ | p => 2) + fun₀ | 2 => 3).support = {p, 2}aux₃:p + 1 < 8 * p ^ 2aux₄:8 * p ^ 2 - 1 ≠ paux₅:8 * p ^ 2 - 1 ≠ 2pf:(f p * (f p + 1)).primeFactors = {8 * p ^ 2 - 1, p, 2}⊢ p ∈ {a | Set.InjOn ⇑(f a * (f a + 1)).factorization ↑(f a * (f a + 1)).primeFactors} aux₁S:Set ℕ := {p | Nat.Prime p ∧ Nat.Prime (8 * p ^ 2 - 1)}h:S.Infinitef:ℕ → ℕ := fun p ↦ 8 * p ^ 2 - 1hS:∀ (p : ℕ), Nat.Prime p → 1 < 8 * p ^ 2this:Set.InjOn f Sp:ℕhp:Nat.Prime php':Nat.Prime (8 * p ^ 2 - 1)hp'':¬p = 2fac:(f p * (f p + 1)).factorization = (fun₀ | 8 * p ^ 2 - 1 => 1) + ((fun₀ | p => 2) + fun₀ | 2 => 3)aux₂:(fun₀ | 2 => 3).support = {2}aux₁:((fun₀ | p => 2) + fun₀ | 2 => 3).support = {p, 2}aux₃:p + 1 < 8 * p ^ 2aux₄:8 * p ^ 2 - 1 ≠ paux₅:8 * p ^ 2 - 1 ≠ 2⊢ {8 * p ^ 2 - 1, p, 2} = {8 * p ^ 2 - 1, p, 2}S:Set ℕ := {p | Nat.Prime p ∧ Nat.Prime (8 * p ^ 2 - 1)}h:S.Infinitef:ℕ → ℕ := fun p ↦ 8 * p ^ 2 - 1hS:∀ (p : ℕ), Nat.Prime p → 1 < 8 * p ^ 2this:Set.InjOn f Sp:ℕhp:Nat.Prime php':Nat.Prime (8 * p ^ 2 - 1)hp'':¬p = 2fac:(f p * (f p + 1)).factorization = (fun₀ | 8 * p ^ 2 - 1 => 1) + ((fun₀ | p => 2) + fun₀ | 2 => 3)aux₂:(fun₀ | 2 => 3).support = {2}aux₁:((fun₀ | p => 2) + fun₀ | 2 => 3).support = {p, 2}aux₃:p + 1 < 8 * p ^ 2aux₄:8 * p ^ 2 - 1 ≠ paux₅:8 * p ^ 2 - 1 ≠ 2⊢ 8 * p ^ 2 - 1 ∉ ((fun₀ | p => 2) + fun₀ | 2 => 3).supportS:Set ℕ := {p | Nat.Prime p ∧ Nat.Prime (8 * p ^ 2 - 1)}h:S.Infinitef:ℕ → ℕ := fun p ↦ 8 * p ^ 2 - 1hS:∀ (p : ℕ), Nat.Prime p → 1 < 8 * p ^ 2this:Set.InjOn f Sp:ℕhp:Nat.Prime php':Nat.Prime (8 * p ^ 2 - 1)hp'':¬p = 2fac:(f p * (f p + 1)).factorization = (fun₀ | 8 * p ^ 2 - 1 => 1) + ((fun₀ | p => 2) + fun₀ | 2 => 3)aux₂:(fun₀ | 2 => 3).support = {2}aux₁:((fun₀ | p => 2) + fun₀ | 2 => 3).support = {p, 2}aux₃:p + 1 < 8 * p ^ 2aux₄:8 * p ^ 2 - 1 ≠ paux₅:8 * p ^ 2 - 1 ≠ 2⊢ 8 * p ^ 2 - 1 ∉ ((fun₀ | p => 2) + fun₀ | 2 => 3).supportS:Set ℕ := {p | Nat.Prime p ∧ Nat.Prime (8 * p ^ 2 - 1)}h:S.Infinitef:ℕ → ℕ := fun p ↦ 8 * p ^ 2 - 1hS:∀ (p : ℕ), Nat.Prime p → 1 < 8 * p ^ 2this:Set.InjOn f Sp:ℕhp:Nat.Prime php':Nat.Prime (8 * p ^ 2 - 1)hp'':¬p = 2fac:(f p * (f p + 1)).factorization = (fun₀ | 8 * p ^ 2 - 1 => 1) + ((fun₀ | p => 2) + fun₀ | 2 => 3)aux₂:(fun₀ | 2 => 3).support = {2}aux₁:((fun₀ | p => 2) + fun₀ | 2 => 3).support = {p, 2}aux₃:p + 1 < 8 * p ^ 2aux₄:8 * p ^ 2 - 1 ≠ paux₅:8 * p ^ 2 - 1 ≠ 2pf:(f p * (f p + 1)).primeFactors = {8 * p ^ 2 - 1, p, 2}⊢ p ∈ {a | Set.InjOn ⇑(f a * (f a + 1)).factorization ↑(f a * (f a + 1)).primeFactors}]S:Set ℕ := {p | Nat.Prime p ∧ Nat.Prime (8 * p ^ 2 - 1)}h:S.Infinitef:ℕ → ℕ := fun p ↦ 8 * p ^ 2 - 1hS:∀ (p : ℕ), Nat.Prime p → 1 < 8 * p ^ 2this:Set.InjOn f Sp:ℕhp:Nat.Prime php':Nat.Prime (8 * p ^ 2 - 1)hp'':¬p = 2fac:(f p * (f p + 1)).factorization = (fun₀ | 8 * p ^ 2 - 1 => 1) + ((fun₀ | p => 2) + fun₀ | 2 => 3)aux₂:(fun₀ | 2 => 3).support = {2}aux₁:((fun₀ | p => 2) + fun₀ | 2 => 3).support = {p, 2}aux₃:p + 1 < 8 * p ^ 2aux₄:8 * p ^ 2 - 1 ≠ paux₅:8 * p ^ 2 - 1 ≠ 2⊢ 8 * p ^ 2 - 1 ∉ ((fun₀ | p => 2) + fun₀ | 2 => 3).supportS:Set ℕ := {p | Nat.Prime p ∧ Nat.Prime (8 * p ^ 2 - 1)}h:S.Infinitef:ℕ → ℕ := fun p ↦ 8 * p ^ 2 - 1hS:∀ (p : ℕ), Nat.Prime p → 1 < 8 * p ^ 2this:Set.InjOn f Sp:ℕhp:Nat.Prime php':Nat.Prime (8 * p ^ 2 - 1)hp'':¬p = 2fac:(f p * (f p + 1)).factorization = (fun₀ | 8 * p ^ 2 - 1 => 1) + ((fun₀ | p => 2) + fun₀ | 2 => 3)aux₂:(fun₀ | 2 => 3).support = {2}aux₁:((fun₀ | p => 2) + fun₀ | 2 => 3).support = {p, 2}aux₃:p + 1 < 8 * p ^ 2aux₄:8 * p ^ 2 - 1 ≠ paux₅:8 * p ^ 2 - 1 ≠ 2pf:(f p * (f p + 1)).primeFactors = {8 * p ^ 2 - 1, p, 2}⊢ p ∈ {a | Set.InjOn ⇑(f a * (f a + 1)).factorization ↑(f a * (f a + 1)).primeFactors}
    simp [*]S:Set ℕ := {p | Nat.Prime p ∧ Nat.Prime (8 * p ^ 2 - 1)}h:S.Infinitef:ℕ → ℕ := fun p ↦ 8 * p ^ 2 - 1hS:∀ (p : ℕ), Nat.Prime p → 1 < 8 * p ^ 2this:Set.InjOn f Sp:ℕhp:Nat.Prime php':Nat.Prime (8 * p ^ 2 - 1)hp'':¬p = 2fac:(f p * (f p + 1)).factorization = (fun₀ | 8 * p ^ 2 - 1 => 1) + ((fun₀ | p => 2) + fun₀ | 2 => 3)aux₂:(fun₀ | 2 => 3).support = {2}aux₁:((fun₀ | p => 2) + fun₀ | 2 => 3).support = {p, 2}aux₃:p + 1 < 8 * p ^ 2aux₄:8 * p ^ 2 - 1 ≠ paux₅:8 * p ^ 2 - 1 ≠ 2pf:(f p * (f p + 1)).primeFactors = {8 * p ^ 2 - 1, p, 2}⊢ p ∈ {a | Set.InjOn ⇑(f a * (f a + 1)).factorization ↑(f a * (f a + 1)).primeFactors}S:Set ℕ := {p | Nat.Prime p ∧ Nat.Prime (8 * p ^ 2 - 1)}h:S.Infinitef:ℕ → ℕ := fun p ↦ 8 * p ^ 2 - 1hS:∀ (p : ℕ), Nat.Prime p → 1 < 8 * p ^ 2this:Set.InjOn f Sp:ℕhp:Nat.Prime php':Nat.Prime (8 * p ^ 2 - 1)hp'':¬p = 2fac:(f p * (f p + 1)).factorization = (fun₀ | 8 * p ^ 2 - 1 => 1) + ((fun₀ | p => 2) + fun₀ | 2 => 3)aux₂:(fun₀ | 2 => 3).support = {2}aux₁:((fun₀ | p => 2) + fun₀ | 2 => 3).support = {p, 2}aux₃:p + 1 < 8 * p ^ 2aux₄:8 * p ^ 2 - 1 ≠ paux₅:8 * p ^ 2 - 1 ≠ 2pf:(f p * (f p + 1)).primeFactors = {8 * p ^ 2 - 1, p, 2}⊢ p ∈ {a | Set.InjOn ⇑(f a * (f a + 1)).factorization ↑(f a * (f a + 1)).primeFactors}
  simp only [Set.mem_ofPred_eq]S:Set ℕ := {p | Nat.Prime p ∧ Nat.Prime (8 * p ^ 2 - 1)}h:S.Infinitef:ℕ → ℕ := fun p ↦ 8 * p ^ 2 - 1hS:∀ (p : ℕ), Nat.Prime p → 1 < 8 * p ^ 2this:Set.InjOn f Sp:ℕhp:Nat.Prime php':Nat.Prime (8 * p ^ 2 - 1)hp'':¬p = 2fac:(f p * (f p + 1)).factorization = (fun₀ | 8 * p ^ 2 - 1 => 1) + ((fun₀ | p => 2) + fun₀ | 2 => 3)aux₂:(fun₀ | 2 => 3).support = {2}aux₁:((fun₀ | p => 2) + fun₀ | 2 => 3).support = {p, 2}aux₃:p + 1 < 8 * p ^ 2aux₄:8 * p ^ 2 - 1 ≠ paux₅:8 * p ^ 2 - 1 ≠ 2pf:(f p * (f p + 1)).primeFactors = {8 * p ^ 2 - 1, p, 2}⊢ Set.InjOn ⇑(f p * (f p + 1)).factorization ↑(f p * (f p + 1)).primeFactors
  rw [fac,S:Set ℕ := {p | Nat.Prime p ∧ Nat.Prime (8 * p ^ 2 - 1)}h:S.Infinitef:ℕ → ℕ := fun p ↦ 8 * p ^ 2 - 1hS:∀ (p : ℕ), Nat.Prime p → 1 < 8 * p ^ 2this:Set.InjOn f Sp:ℕhp:Nat.Prime php':Nat.Prime (8 * p ^ 2 - 1)hp'':¬p = 2fac:(f p * (f p + 1)).factorization = (fun₀ | 8 * p ^ 2 - 1 => 1) + ((fun₀ | p => 2) + fun₀ | 2 => 3)aux₂:(fun₀ | 2 => 3).support = {2}aux₁:((fun₀ | p => 2) + fun₀ | 2 => 3).support = {p, 2}aux₃:p + 1 < 8 * p ^ 2aux₄:8 * p ^ 2 - 1 ≠ paux₅:8 * p ^ 2 - 1 ≠ 2pf:(f p * (f p + 1)).primeFactors = {8 * p ^ 2 - 1, p, 2}⊢ Set.InjOn ⇑((fun₀ | 8 * p ^ 2 - 1 => 1) + ((fun₀ | p => 2) + fun₀ | 2 => 3)) ↑(f p * (f p + 1)).primeFactorsS:Set ℕ := {p | Nat.Prime p ∧ Nat.Prime (8 * p ^ 2 - 1)}h:S.Infinitef:ℕ → ℕ := fun p ↦ 8 * p ^ 2 - 1hS:∀ (p : ℕ), Nat.Prime p → 1 < 8 * p ^ 2this:Set.InjOn f Sp:ℕhp:Nat.Prime php':Nat.Prime (8 * p ^ 2 - 1)hp'':¬p = 2fac:(f p * (f p + 1)).factorization = (fun₀ | 8 * p ^ 2 - 1 => 1) + ((fun₀ | p => 2) + fun₀ | 2 => 3)aux₂:(fun₀ | 2 => 3).support = {2}aux₁:((fun₀ | p => 2) + fun₀ | 2 => 3).support = {p, 2}aux₃:p + 1 < 8 * p ^ 2aux₄:8 * p ^ 2 - 1 ≠ paux₅:8 * p ^ 2 - 1 ≠ 2pf:(f p * (f p + 1)).primeFactors = {8 * p ^ 2 - 1, p, 2}⊢ Set.InjOn ⇑((fun₀ | 8 * p ^ 2 - 1 => 1) + ((fun₀ | p => 2) + fun₀ | 2 => 3)) ↑{8 * p ^ 2 - 1, p, 2} pfS:Set ℕ := {p | Nat.Prime p ∧ Nat.Prime (8 * p ^ 2 - 1)}h:S.Infinitef:ℕ → ℕ := fun p ↦ 8 * p ^ 2 - 1hS:∀ (p : ℕ), Nat.Prime p → 1 < 8 * p ^ 2this:Set.InjOn f Sp:ℕhp:Nat.Prime php':Nat.Prime (8 * p ^ 2 - 1)hp'':¬p = 2fac:(f p * (f p + 1)).factorization = (fun₀ | 8 * p ^ 2 - 1 => 1) + ((fun₀ | p => 2) + fun₀ | 2 => 3)aux₂:(fun₀ | 2 => 3).support = {2}aux₁:((fun₀ | p => 2) + fun₀ | 2 => 3).support = {p, 2}aux₃:p + 1 < 8 * p ^ 2aux₄:8 * p ^ 2 - 1 ≠ paux₅:8 * p ^ 2 - 1 ≠ 2pf:(f p * (f p + 1)).primeFactors = {8 * p ^ 2 - 1, p, 2}⊢ Set.InjOn ⇑((fun₀ | 8 * p ^ 2 - 1 => 1) + ((fun₀ | p => 2) + fun₀ | 2 => 3)) ↑{8 * p ^ 2 - 1, p, 2}S:Set ℕ := {p | Nat.Prime p ∧ Nat.Prime (8 * p ^ 2 - 1)}h:S.Infinitef:ℕ → ℕ := fun p ↦ 8 * p ^ 2 - 1hS:∀ (p : ℕ), Nat.Prime p → 1 < 8 * p ^ 2this:Set.InjOn f Sp:ℕhp:Nat.Prime php':Nat.Prime (8 * p ^ 2 - 1)hp'':¬p = 2fac:(f p * (f p + 1)).factorization = (fun₀ | 8 * p ^ 2 - 1 => 1) + ((fun₀ | p => 2) + fun₀ | 2 => 3)aux₂:(fun₀ | 2 => 3).support = {2}aux₁:((fun₀ | p => 2) + fun₀ | 2 => 3).support = {p, 2}aux₃:p + 1 < 8 * p ^ 2aux₄:8 * p ^ 2 - 1 ≠ paux₅:8 * p ^ 2 - 1 ≠ 2pf:(f p * (f p + 1)).primeFactors = {8 * p ^ 2 - 1, p, 2}⊢ Set.InjOn ⇑((fun₀ | 8 * p ^ 2 - 1 => 1) + ((fun₀ | p => 2) + fun₀ | 2 => 3)) ↑{8 * p ^ 2 - 1, p, 2}]S:Set ℕ := {p | Nat.Prime p ∧ Nat.Prime (8 * p ^ 2 - 1)}h:S.Infinitef:ℕ → ℕ := fun p ↦ 8 * p ^ 2 - 1hS:∀ (p : ℕ), Nat.Prime p → 1 < 8 * p ^ 2this:Set.InjOn f Sp:ℕhp:Nat.Prime php':Nat.Prime (8 * p ^ 2 - 1)hp'':¬p = 2fac:(f p * (f p + 1)).factorization = (fun₀ | 8 * p ^ 2 - 1 => 1) + ((fun₀ | p => 2) + fun₀ | 2 => 3)aux₂:(fun₀ | 2 => 3).support = {2}aux₁:((fun₀ | p => 2) + fun₀ | 2 => 3).support = {p, 2}aux₃:p + 1 < 8 * p ^ 2aux₄:8 * p ^ 2 - 1 ≠ paux₅:8 * p ^ 2 - 1 ≠ 2pf:(f p * (f p + 1)).primeFactors = {8 * p ^ 2 - 1, p, 2}⊢ Set.InjOn ⇑((fun₀ | 8 * p ^ 2 - 1 => 1) + ((fun₀ | p => 2) + fun₀ | 2 => 3)) ↑{8 * p ^ 2 - 1, p, 2}
  simp only [Finsupp.coe_add, Finset.coe_insert, Finset.coe_singleton]S:Set ℕ := {p | Nat.Prime p ∧ Nat.Prime (8 * p ^ 2 - 1)}h:S.Infinitef:ℕ → ℕ := fun p ↦ 8 * p ^ 2 - 1hS:∀ (p : ℕ), Nat.Prime p → 1 < 8 * p ^ 2this:Set.InjOn f Sp:ℕhp:Nat.Prime php':Nat.Prime (8 * p ^ 2 - 1)hp'':¬p = 2fac:(f p * (f p + 1)).factorization = (fun₀ | 8 * p ^ 2 - 1 => 1) + ((fun₀ | p => 2) + fun₀ | 2 => 3)aux₂:(fun₀ | 2 => 3).support = {2}aux₁:((fun₀ | p => 2) + fun₀ | 2 => 3).support = {p, 2}aux₃:p + 1 < 8 * p ^ 2aux₄:8 * p ^ 2 - 1 ≠ paux₅:8 * p ^ 2 - 1 ≠ 2pf:(f p * (f p + 1)).primeFactors = {8 * p ^ 2 - 1, p, 2}⊢ Set.InjOn ((⇑fun₀ | 8 * p ^ 2 - 1 => 1) + ((⇑fun₀ | p => 2) + ⇑fun₀ | 2 => 3)) {8 * p ^ 2 - 1, p, 2}
  rw [Set.injOn_insert (byS:Set ℕ := {p | Nat.Prime p ∧ Nat.Prime (8 * p ^ 2 - 1)}h:S.Infinitef:ℕ → ℕ := fun p ↦ 8 * p ^ 2 - 1hS:∀ (p : ℕ), Nat.Prime p → 1 < 8 * p ^ 2this:Set.InjOn f Sp:ℕhp:Nat.Prime php':Nat.Prime (8 * p ^ 2 - 1)hp'':¬p = 2fac:(f p * (f p + 1)).factorization = (fun₀ | 8 * p ^ 2 - 1 => 1) + ((fun₀ | p => 2) + fun₀ | 2 => 3)aux₂:(fun₀ | 2 => 3).support = {2}aux₁:((fun₀ | p => 2) + fun₀ | 2 => 3).support = {p, 2}aux₃:p + 1 < 8 * p ^ 2aux₄:8 * p ^ 2 - 1 ≠ paux₅:8 * p ^ 2 - 1 ≠ 2pf:(f p * (f p + 1)).primeFactors = {8 * p ^ 2 - 1, p, 2}⊢ 8 * p ^ 2 - 1 ∉ {p, 2}S:Set ℕ := {p | Nat.Prime p ∧ Nat.Prime (8 * p ^ 2 - 1)}h:S.Infinitef:ℕ → ℕ := fun p ↦ 8 * p ^ 2 - 1hS:∀ (p : ℕ), Nat.Prime p → 1 < 8 * p ^ 2this:Set.InjOn f Sp:ℕhp:Nat.Prime php':Nat.Prime (8 * p ^ 2 - 1)hp'':¬p = 2fac:(f p * (f p + 1)).factorization = (fun₀ | 8 * p ^ 2 - 1 => 1) + ((fun₀ | p => 2) + fun₀ | 2 => 3)aux₂:(fun₀ | 2 => 3).support = {2}aux₁:((fun₀ | p => 2) + fun₀ | 2 => 3).support = {p, 2}aux₃:p + 1 < 8 * p ^ 2aux₄:8 * p ^ 2 - 1 ≠ paux₅:8 * p ^ 2 - 1 ≠ 2pf:(f p * (f p + 1)).primeFactors = {8 * p ^ 2 - 1, p, 2}⊢ (Set.InjOn ((⇑fun₀ | 8 * p ^ 2 - 1 => 1) + ((⇑fun₀ | p => 2) + ⇑fun₀ | 2 => 3)) {2} ∧
    ((⇑fun₀ | 8 * p ^ 2 - 1 => 1) + ((⇑fun₀ | p => 2) + ⇑fun₀ | 2 => 3)) p ∉
      ((⇑fun₀ | 8 * p ^ 2 - 1 => 1) + ((⇑fun₀ | p => 2) + ⇑fun₀ | 2 => 3)) '' {2}) ∧
  ((⇑fun₀ | 8 * p ^ 2 - 1 => 1) + ((⇑fun₀ | p => 2) + ⇑fun₀ | 2 => 3)) (8 * p ^ 2 - 1) ∉
    ((⇑fun₀ | 8 * p ^ 2 - 1 => 1) + ((⇑fun₀ | p => 2) + ⇑fun₀ | 2 => 3)) '' {p, 2} simp [*]All goals completed! 🐙S:Set ℕ := {p | Nat.Prime p ∧ Nat.Prime (8 * p ^ 2 - 1)}h:S.Infinitef:ℕ → ℕ := fun p ↦ 8 * p ^ 2 - 1hS:∀ (p : ℕ), Nat.Prime p → 1 < 8 * p ^ 2this:Set.InjOn f Sp:ℕhp:Nat.Prime php':Nat.Prime (8 * p ^ 2 - 1)hp'':¬p = 2fac:(f p * (f p + 1)).factorization = (fun₀ | 8 * p ^ 2 - 1 => 1) + ((fun₀ | p => 2) + fun₀ | 2 => 3)aux₂:(fun₀ | 2 => 3).support = {2}aux₁:((fun₀ | p => 2) + fun₀ | 2 => 3).support = {p, 2}aux₃:p + 1 < 8 * p ^ 2aux₄:8 * p ^ 2 - 1 ≠ paux₅:8 * p ^ 2 - 1 ≠ 2pf:(f p * (f p + 1)).primeFactors = {8 * p ^ 2 - 1, p, 2}⊢ (Set.InjOn ((⇑fun₀ | 8 * p ^ 2 - 1 => 1) + ((⇑fun₀ | p => 2) + ⇑fun₀ | 2 => 3)) {2} ∧
    ((⇑fun₀ | 8 * p ^ 2 - 1 => 1) + ((⇑fun₀ | p => 2) + ⇑fun₀ | 2 => 3)) p ∉
      ((⇑fun₀ | 8 * p ^ 2 - 1 => 1) + ((⇑fun₀ | p => 2) + ⇑fun₀ | 2 => 3)) '' {2}) ∧
  ((⇑fun₀ | 8 * p ^ 2 - 1 => 1) + ((⇑fun₀ | p => 2) + ⇑fun₀ | 2 => 3)) (8 * p ^ 2 - 1) ∉
    ((⇑fun₀ | 8 * p ^ 2 - 1 => 1) + ((⇑fun₀ | p => 2) + ⇑fun₀ | 2 => 3)) '' {p, 2}), Set.injOn_insert (byS:Set ℕ := {p | Nat.Prime p ∧ Nat.Prime (8 * p ^ 2 - 1)}h:S.Infinitef:ℕ → ℕ := fun p ↦ 8 * p ^ 2 - 1hS:∀ (p : ℕ), Nat.Prime p → 1 < 8 * p ^ 2this:Set.InjOn f Sp:ℕhp:Nat.Prime php':Nat.Prime (8 * p ^ 2 - 1)hp'':¬p = 2fac:(f p * (f p + 1)).factorization = (fun₀ | 8 * p ^ 2 - 1 => 1) + ((fun₀ | p => 2) + fun₀ | 2 => 3)aux₂:(fun₀ | 2 => 3).support = {2}aux₁:((fun₀ | p => 2) + fun₀ | 2 => 3).support = {p, 2}aux₃:p + 1 < 8 * p ^ 2aux₄:8 * p ^ 2 - 1 ≠ paux₅:8 * p ^ 2 - 1 ≠ 2pf:(f p * (f p + 1)).primeFactors = {8 * p ^ 2 - 1, p, 2}⊢ p ∉ {2}S:Set ℕ := {p | Nat.Prime p ∧ Nat.Prime (8 * p ^ 2 - 1)}h:S.Infinitef:ℕ → ℕ := fun p ↦ 8 * p ^ 2 - 1hS:∀ (p : ℕ), Nat.Prime p → 1 < 8 * p ^ 2this:Set.InjOn f Sp:ℕhp:Nat.Prime php':Nat.Prime (8 * p ^ 2 - 1)hp'':¬p = 2fac:(f p * (f p + 1)).factorization = (fun₀ | 8 * p ^ 2 - 1 => 1) + ((fun₀ | p => 2) + fun₀ | 2 => 3)aux₂:(fun₀ | 2 => 3).support = {2}aux₁:((fun₀ | p => 2) + fun₀ | 2 => 3).support = {p, 2}aux₃:p + 1 < 8 * p ^ 2aux₄:8 * p ^ 2 - 1 ≠ paux₅:8 * p ^ 2 - 1 ≠ 2pf:(f p * (f p + 1)).primeFactors = {8 * p ^ 2 - 1, p, 2}⊢ (Set.InjOn ((⇑fun₀ | 8 * p ^ 2 - 1 => 1) + ((⇑fun₀ | p => 2) + ⇑fun₀ | 2 => 3)) {2} ∧
    ((⇑fun₀ | 8 * p ^ 2 - 1 => 1) + ((⇑fun₀ | p => 2) + ⇑fun₀ | 2 => 3)) p ∉
      ((⇑fun₀ | 8 * p ^ 2 - 1 => 1) + ((⇑fun₀ | p => 2) + ⇑fun₀ | 2 => 3)) '' {2}) ∧
  ((⇑fun₀ | 8 * p ^ 2 - 1 => 1) + ((⇑fun₀ | p => 2) + ⇑fun₀ | 2 => 3)) (8 * p ^ 2 - 1) ∉
    ((⇑fun₀ | 8 * p ^ 2 - 1 => 1) + ((⇑fun₀ | p => 2) + ⇑fun₀ | 2 => 3)) '' {p, 2} simp [hp'']All goals completed! 🐙S:Set ℕ := {p | Nat.Prime p ∧ Nat.Prime (8 * p ^ 2 - 1)}h:S.Infinitef:ℕ → ℕ := fun p ↦ 8 * p ^ 2 - 1hS:∀ (p : ℕ), Nat.Prime p → 1 < 8 * p ^ 2this:Set.InjOn f Sp:ℕhp:Nat.Prime php':Nat.Prime (8 * p ^ 2 - 1)hp'':¬p = 2fac:(f p * (f p + 1)).factorization = (fun₀ | 8 * p ^ 2 - 1 => 1) + ((fun₀ | p => 2) + fun₀ | 2 => 3)aux₂:(fun₀ | 2 => 3).support = {2}aux₁:((fun₀ | p => 2) + fun₀ | 2 => 3).support = {p, 2}aux₃:p + 1 < 8 * p ^ 2aux₄:8 * p ^ 2 - 1 ≠ paux₅:8 * p ^ 2 - 1 ≠ 2pf:(f p * (f p + 1)).primeFactors = {8 * p ^ 2 - 1, p, 2}⊢ (Set.InjOn ((⇑fun₀ | 8 * p ^ 2 - 1 => 1) + ((⇑fun₀ | p => 2) + ⇑fun₀ | 2 => 3)) {2} ∧
    ((⇑fun₀ | 8 * p ^ 2 - 1 => 1) + ((⇑fun₀ | p => 2) + ⇑fun₀ | 2 => 3)) p ∉
      ((⇑fun₀ | 8 * p ^ 2 - 1 => 1) + ((⇑fun₀ | p => 2) + ⇑fun₀ | 2 => 3)) '' {2}) ∧
  ((⇑fun₀ | 8 * p ^ 2 - 1 => 1) + ((⇑fun₀ | p => 2) + ⇑fun₀ | 2 => 3)) (8 * p ^ 2 - 1) ∉
    ((⇑fun₀ | 8 * p ^ 2 - 1 => 1) + ((⇑fun₀ | p => 2) + ⇑fun₀ | 2 => 3)) '' {p, 2})]S:Set ℕ := {p | Nat.Prime p ∧ Nat.Prime (8 * p ^ 2 - 1)}h:S.Infinitef:ℕ → ℕ := fun p ↦ 8 * p ^ 2 - 1hS:∀ (p : ℕ), Nat.Prime p → 1 < 8 * p ^ 2this:Set.InjOn f Sp:ℕhp:Nat.Prime php':Nat.Prime (8 * p ^ 2 - 1)hp'':¬p = 2fac:(f p * (f p + 1)).factorization = (fun₀ | 8 * p ^ 2 - 1 => 1) + ((fun₀ | p => 2) + fun₀ | 2 => 3)aux₂:(fun₀ | 2 => 3).support = {2}aux₁:((fun₀ | p => 2) + fun₀ | 2 => 3).support = {p, 2}aux₃:p + 1 < 8 * p ^ 2aux₄:8 * p ^ 2 - 1 ≠ paux₅:8 * p ^ 2 - 1 ≠ 2pf:(f p * (f p + 1)).primeFactors = {8 * p ^ 2 - 1, p, 2}⊢ (Set.InjOn ((⇑fun₀ | 8 * p ^ 2 - 1 => 1) + ((⇑fun₀ | p => 2) + ⇑fun₀ | 2 => 3)) {2} ∧
    ((⇑fun₀ | 8 * p ^ 2 - 1 => 1) + ((⇑fun₀ | p => 2) + ⇑fun₀ | 2 => 3)) p ∉
      ((⇑fun₀ | 8 * p ^ 2 - 1 => 1) + ((⇑fun₀ | p => 2) + ⇑fun₀ | 2 => 3)) '' {2}) ∧
  ((⇑fun₀ | 8 * p ^ 2 - 1 => 1) + ((⇑fun₀ | p => 2) + ⇑fun₀ | 2 => 3)) (8 * p ^ 2 - 1) ∉
    ((⇑fun₀ | 8 * p ^ 2 - 1 => 1) + ((⇑fun₀ | p => 2) + ⇑fun₀ | 2 => 3)) '' {p, 2}
  simp [aux₄, hp'', Ne.symm, aux₅]All goals completed! 🐙

end Erdos913