FormalConjectures.OEIS.«358684»

/-
Copyright 2026 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

Factor bounds for Fermat numbers

$a(n)$ is the minimum integer $k$ such that the smallest prime factor of the $n$-th Fermat number exceeds $2^{2^n - k}$.

References:

A358684

SA22 Lorenzo Sauras-Altuzarra, Some properties of the factors of Fermat numbers, Art Discrete Appl. Math. (2022).



namespace OeisA358684


open Nat

A358684: $a(n)$ is the minimum integer $k$ such that the smallest prime factor of the $n$-th Fermat number exceeds $2^{2^n - k}$. Let $F_n = 2^{2^n} + 1$ be the $n$-th Fermat number, and $P_n$ be its smallest prime factor. The definition of $a(n)$ is equivalent to the closed form: $$a(n) = 2^n - \lfloor \log_2(P_n) \rfloor$$ where $P_n = \operatorname{minFac}(\operatorname{fermatNumber} n)$. The subtraction is defined in $\mathbb{N}$ and is safe since $P_n \le F_n$, implying $\log_2 P_n < 2^n$.

def a (n : ℕ) : ℕ :=
  letI pn := minFac (fermatNumber n)
  (2 ^ n) - (log2 pn)

The "original" definition: $a'(n)$ is the minimum $k$ such that $P_n > 2^{2^n - k}$. We use Nat.find which returns the smallest natural number satisfying a predicate.

noncomputable def a' (n : ℕ) : ℕ :=
  letI Pn := minFac (fermatNumber n)
  Nat.find (show ∃ k, Pn > 2 ^ (2 ^ n - k) from byn:ℕPn:ℕ := n.fermatNumber.minFac⊢ ∃ k, Pn > 2 ^ (2 ^ n - k)
    use 2^nhn:ℕPn:ℕ := n.fermatNumber.minFac⊢ Pn > 2 ^ (2 ^ n - 2 ^ n)
    simp only [tsub_self, pow_zero]hn:ℕPn:ℕ := n.fermatNumber.minFac⊢ Pn > 1
    simp [Pn]hn:ℕPn:ℕ := n.fermatNumber.minFac⊢ 1 < n.fermatNumber.minFac
    unfold Nat.fermatNumberhn:ℕPn:ℕ := n.fermatNumber.minFac⊢ 1 < (2 ^ 2 ^ n + 1).minFac
    exact (Nat.minFac_prime (byn:ℕPn:ℕ := n.fermatNumber.minFac⊢ 2 ^ 2 ^ n + 1 ≠ 1 norm_numAll goals completed! 🐙)).one_lt
  )

The log2 of the smallest prime factor of $F_n$ is at most $2^n$.

@[category textbook, AMS 11]
private lemma log2_minFac_le (n : ℕ) : log2 (fermatNumber n).minFac ≤ 2^n := byn:ℕ⊢ n.fermatNumber.minFac.log2 ≤ 2 ^ n
  rw [log2_eq_log_two]n:ℕ⊢ log 2 n.fermatNumber.minFac ≤ 2 ^ n
  refine (log_mono_right (minFac_le (byn:ℕ⊢ 0 < n.fermatNumber rw [fermatNumber]n:ℕ⊢ 0 < 2 ^ 2 ^ n + 1; norm_numAll goals completed! 🐙))).trans_eq ?_
  rw [fermatNumber, log_eq_of_pow_le_of_lt_pow (le_add_right _ _)]n:ℕ⊢ 2 ^ 2 ^ n + 1 < 2 ^ (2 ^ n + 1)
  rw [pow_succ, mul_two]n:ℕ⊢ 2 ^ 2 ^ n + 1 < 2 ^ 2 ^ n + 2 ^ 2 ^ n
  gcongrbcn:ℕ⊢ 1 < 2 ^ 2 ^ n
  exact one_lt_pow (byn:ℕ⊢ 2 ^ n ≠ 0 norm_numAll goals completed! 🐙) (byn:ℕ⊢ 1 < 2 norm_numAll goals completed! 🐙)

The minimization definition is equivalent to the closed form.

@[category API, AMS 11]
theorem a_equiv_a' (n : ℕ) : a n = a' n := byn:ℕ⊢ a n = a' n
  unfold a a'n:ℕ⊢ 2 ^ n - n.fermatNumber.minFac.log2 = Nat.find ⋯; set Pn := (fermatNumber n).minFacn:ℕPn:ℕ := n.fermatNumber.minFac⊢ 2 ^ n - n.fermatNumber.minFac.log2 = Nat.find ⋯
  rw [Eq.comm, Nat.find_eq_iff]n:ℕPn:ℕ := n.fermatNumber.minFac⊢ n.fermatNumber.minFac > 2 ^ (2 ^ n - (2 ^ n - n.fermatNumber.minFac.log2)) ∧
  ∀ n_1 < 2 ^ n - n.fermatNumber.minFac.log2, ¬n.fermatNumber.minFac > 2 ^ (2 ^ n - n_1)
  constructorleftn:ℕPn:ℕ := n.fermatNumber.minFac⊢ n.fermatNumber.minFac > 2 ^ (2 ^ n - (2 ^ n - n.fermatNumber.minFac.log2))rightn:ℕPn:ℕ := n.fermatNumber.minFac⊢ ∀ n_1 < 2 ^ n - n.fermatNumber.minFac.log2, ¬n.fermatNumber.minFac > 2 ^ (2 ^ n - n_1)
  ·leftn:ℕPn:ℕ := n.fermatNumber.minFac⊢ n.fermatNumber.minFac > 2 ^ (2 ^ n - (2 ^ n - n.fermatNumber.minFac.log2)) rw [tsub_tsub_cancel_of_le (log2_minFac_le n), log2_eq_log_two]leftn:ℕPn:ℕ := n.fermatNumber.minFac⊢ n.fermatNumber.minFac > 2 ^ log 2 n.fermatNumber.minFac
    refine lt_of_le_of_ne (pow_log_le_self 2 (Nat.Prime.ne_zero (minFac_prime ?_))) fun h => ?_left.refine_1n:ℕPn:ℕ := n.fermatNumber.minFac⊢ n.fermatNumber ≠ 1left.refine_2n:ℕPn:ℕ := n.fermatNumber.minFach:2 ^ log 2 n.fermatNumber.minFac = n.fermatNumber.minFac⊢ False
    ·left.refine_1n:ℕPn:ℕ := n.fermatNumber.minFac⊢ n.fermatNumber ≠ 1 rw [fermatNumber]left.refine_1n:ℕPn:ℕ := n.fermatNumber.minFac⊢ 2 ^ 2 ^ n + 1 ≠ 1
      norm_numAll goals completed! 🐙
    ·left.refine_2n:ℕPn:ℕ := n.fermatNumber.minFach:2 ^ log 2 n.fermatNumber.minFac = n.fermatNumber.minFac⊢ False have hPn : Pn.Prime := minFac_prime (byn:ℕPn:ℕ := n.fermatNumber.minFach:2 ^ log 2 n.fermatNumber.minFac = n.fermatNumber.minFac⊢ n.fermatNumber ≠ 1 rw [fermatNumber]n:ℕPn:ℕ := n.fermatNumber.minFach:2 ^ log 2 n.fermatNumber.minFac = n.fermatNumber.minFac⊢ 2 ^ 2 ^ n + 1 ≠ 1; norm_numAll goals completed! 🐙)
      have hnz := log2_eq_log_two ▸ (Nat.log_pos one_lt_two hPn.two_le).ne'left.refine_2n:ℕPn:ℕ := n.fermatNumber.minFach:2 ^ log 2 n.fermatNumber.minFac = n.fermatNumber.minFachPn:Nat.Prime Pn := 
  minFac_prime
    (Eq.mpr (id (congrArg (fun _a => _a ≠ 1) (fermatNumber.eq_1 n)))
      (of_eq_true
        (Eq.trans
          (Eq.trans
            (congrArg Not
              (Eq.trans add_eq_right._simp_1
                (Eq.trans pow_eq_zero._simp_1
                  (Eq.trans
                    (Eq.trans
                      (congr
                        (congrArg And
                          (eq_false
                            (Mathlib.Meta.NormNum.isNat_eq_false (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2))
                              (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 0)) (Eq.refl false))))
                        (Eq.trans
                          (Eq.trans
                            (congrArg Not
                              (Eq.trans pow_eq_zero._simp_1
                                (Eq.trans
                                  (Eq.trans
                                    (congrArg (fun x => x ∧ ¬n = 0)
                                      (eq_false
                                        (Mathlib.Meta.NormNum.isNat_eq_false
                                          (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2))
                                          (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 0)) (Eq.refl false))))
                                    (false_and ¬n = 0))
                                  (eq_false not_false))))
                            not_false_eq_true)
                          (eq_true True.intro)))
                      (and_true False))
                    (eq_false not_false)))))
            not_false_eq_true)
          (eq_true True.intro))))hnz:Pn.log2 ≠ 0 := Eq.symm log2_eq_log_two ▸ LT.lt.ne' (log_pos one_lt_two (Prime.two_le hPn))⊢ False
      refine (Nat.not_even_iff_odd.mpr <| (odd_pow_iff hnz).mp ?_) even_twoleft.refine_2n:ℕPn:ℕ := n.fermatNumber.minFach:2 ^ log 2 n.fermatNumber.minFac = n.fermatNumber.minFachPn:Nat.Prime Pn := 
  minFac_prime
    (Eq.mpr (id (congrArg (fun _a => _a ≠ 1) (fermatNumber.eq_1 n)))
      (of_eq_true
        (Eq.trans
          (Eq.trans
            (congrArg Not
              (Eq.trans add_eq_right._simp_1
                (Eq.trans pow_eq_zero._simp_1
                  (Eq.trans
                    (Eq.trans
                      (congr
                        (congrArg And
                          (eq_false
                            (Mathlib.Meta.NormNum.isNat_eq_false (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2))
                              (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 0)) (Eq.refl false))))
                        (Eq.trans
                          (Eq.trans
                            (congrArg Not
                              (Eq.trans pow_eq_zero._simp_1
                                (Eq.trans
                                  (Eq.trans
                                    (congrArg (fun x => x ∧ ¬n = 0)
                                      (eq_false
                                        (Mathlib.Meta.NormNum.isNat_eq_false
                                          (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2))
                                          (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 0)) (Eq.refl false))))
                                    (false_and ¬n = 0))
                                  (eq_false not_false))))
                            not_false_eq_true)
                          (eq_true True.intro)))
                      (and_true False))
                    (eq_false not_false)))))
            not_false_eq_true)
          (eq_true True.intro))))hnz:Pn.log2 ≠ 0 := Eq.symm log2_eq_log_two ▸ LT.lt.ne' (log_pos one_lt_two (Prime.two_le hPn))⊢ Odd (2 ^ Pn.log2)
      rw [log2_eq_log_two, h]left.refine_2n:ℕPn:ℕ := n.fermatNumber.minFach:2 ^ log 2 n.fermatNumber.minFac = n.fermatNumber.minFachPn:Nat.Prime Pn := 
  minFac_prime
    (Eq.mpr (id (congrArg (fun _a => _a ≠ 1) (fermatNumber.eq_1 n)))
      (of_eq_true
        (Eq.trans
          (Eq.trans
            (congrArg Not
              (Eq.trans add_eq_right._simp_1
                (Eq.trans pow_eq_zero._simp_1
                  (Eq.trans
                    (Eq.trans
                      (congr
                        (congrArg And
                          (eq_false
                            (Mathlib.Meta.NormNum.isNat_eq_false (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2))
                              (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 0)) (Eq.refl false))))
                        (Eq.trans
                          (Eq.trans
                            (congrArg Not
                              (Eq.trans pow_eq_zero._simp_1
                                (Eq.trans
                                  (Eq.trans
                                    (congrArg (fun x => x ∧ ¬n = 0)
                                      (eq_false
                                        (Mathlib.Meta.NormNum.isNat_eq_false
                                          (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2))
                                          (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 0)) (Eq.refl false))))
                                    (false_and ¬n = 0))
                                  (eq_false not_false))))
                            not_false_eq_true)
                          (eq_true True.intro)))
                      (and_true False))
                    (eq_false not_false)))))
            not_false_eq_true)
          (eq_true True.intro))))hnz:Pn.log2 ≠ 0 := Eq.symm log2_eq_log_two ▸ LT.lt.ne' (log_pos one_lt_two (Prime.two_le hPn))⊢ Odd n.fermatNumber.minFac
      exact Odd.of_dvd_nat (odd_fermatNumber n) (minFac_dvd _)All goals completed! 🐙
  ·rightn:ℕPn:ℕ := n.fermatNumber.minFac⊢ ∀ n_1 < 2 ^ n - n.fermatNumber.minFac.log2, ¬n.fermatNumber.minFac > 2 ^ (2 ^ n - n_1) intro m hmrightn:ℕPn:ℕ := n.fermatNumber.minFacm:ℕhm:m < 2 ^ n - n.fermatNumber.minFac.log2⊢ ¬n.fermatNumber.minFac > 2 ^ (2 ^ n - m); simp only [not_lt]rightn:ℕPn:ℕ := n.fermatNumber.minFacm:ℕhm:m < 2 ^ n - n.fermatNumber.minFac.log2⊢ n.fermatNumber.minFac ≤ 2 ^ (2 ^ n - m)
    rw [lt_tsub_iff_left] at hmrightn:ℕPn:ℕ := n.fermatNumber.minFacm:ℕhm:n.fermatNumber.minFac.log2 + m < 2 ^ n⊢ n.fermatNumber.minFac ≤ 2 ^ (2 ^ n - m)
    rw [log2_eq_log_two] at hmrightn:ℕPn:ℕ := n.fermatNumber.minFacm:ℕhm:log 2 n.fermatNumber.minFac + m < 2 ^ n⊢ n.fermatNumber.minFac ≤ 2 ^ (2 ^ n - m)
    refine (lt_pow_succ_log_self (b:=2) (byn:ℕPn:ℕ := n.fermatNumber.minFacm:ℕhm:log 2 n.fermatNumber.minFac + m < 2 ^ n⊢ 1 < 2 norm_numAll goals completed! 🐙) _).le.trans ?_
    apply Nat.pow_le_pow_right (byn:ℕPn:ℕ := n.fermatNumber.minFacm:ℕhm:log 2 n.fermatNumber.minFac + m < 2 ^ n⊢ 2 > 0 norm_numAll goals completed! 🐙)
    apply le_tsub_of_add_le_rightright.hn:ℕPn:ℕ := n.fermatNumber.minFacm:ℕhm:log 2 n.fermatNumber.minFac + m < 2 ^ n⊢ (log 2 n.fermatNumber.minFac).succ + m ≤ 2 ^ n
    have := succ_le_of_lt hmright.hn:ℕPn:ℕ := n.fermatNumber.minFacm:ℕhm:log 2 n.fermatNumber.minFac + m < 2 ^ nthis:(log 2 n.fermatNumber.minFac + m).succ ≤ 2 ^ n := succ_le_of_lt hm⊢ (log 2 n.fermatNumber.minFac).succ + m ≤ 2 ^ n
    omegaAll goals completed! 🐙


@[category test, AMS 11]
theorem a_0 : a 0 = 0 := by⊢ a 0 = 0 norm_num [a]⊢ 1 - log2 3 = 0; simp [log2_def]All goals completed! 🐙


@[category test, AMS 11]
theorem a_1 : a 1 = 0 := by⊢ a 1 = 0 norm_num [a]⊢ 2 - log2 5 = 0; simp [log2_def]All goals completed! 🐙


@[category test, AMS 11]
theorem a_2 : a 2 = 0 := by⊢ a 2 = 0 norm_num [a]⊢ 4 - log2 17 = 0; simp [log2_def]All goals completed! 🐙


@[category test, AMS 11]
theorem a_3 : a 3 = 0 := by⊢ a 3 = 0
  norm_num only [a, Nat.log2_eq_log_two,Nat.fermatNumber]All goals completed! 🐙


@[category test, AMS 11]
theorem a_4 : a 4 = 0 := by⊢ a 4 = 0
  norm_num [a, fermatNumber, Nat.log2_eq_log_two]All goals completed! 🐙


@[category test, AMS 11]
theorem a_5 : a 5 = 23 := by⊢ a 5 = 23
  norm_num [a, fermatNumber,Nat.log2_eq_log_two]All goals completed! 🐙


@[category test, AMS 11]
theorem a_6 : a 6 = 46 := by⊢ a 6 = 46
  decide +nativeAll goals completed! 🐙


@[category test, AMS 11]
theorem declaration uses 'sorry'a_7 : a 7 = 73 := by⊢ a 7 = 73
  sorryAll goals completed! 🐙

Conjecture: the dyadic valuation of A93179(n) - 1 does not exceed 2^n - a(n).

A93179(n) is minFac(fermatNumber n), the smallest prime factor of the n-th Fermat number. The conjecture states that if $P_n$ is the smallest prime factor of the $n$-th Fermat number, then $\nu_2(P_n - 1) \le 2^n - a(n)$. Substituting the definition of $a(n)$, this is equivalent to $\nu_2(P_n - 1) \le \lfloor \log_2(P_n) \rfloor$.

This is Conjecture 3.4 in [SA22].

@[category research solved, AMS 11]
theorem oeis_358684_conjecture_0 (n : ℕ) :
    padicValNat 2 (minFac (fermatNumber n) - 1) ≤ 2 ^ n - a n := byn:ℕ⊢ padicValNat 2 (n.fermatNumber.minFac - 1) ≤ 2 ^ n - a n
  delta fermatNumber and an:ℕ⊢ padicValNat 2 ((2 ^ 2 ^ n + 1).minFac - 1) ≤ 2 ^ n - (2 ^ n - (2 ^ 2 ^ n + 1).minFac.log2)
  rw [Nat.sub_sub_self]n:ℕ⊢ padicValNat 2 ((2 ^ 2 ^ n + 1).minFac - 1) ≤ (2 ^ 2 ^ n + 1).minFac.log2n:ℕ⊢ (2 ^ 2 ^ n + 1).minFac.log2 ≤ 2 ^ n
  ·n:ℕ⊢ padicValNat 2 ((2 ^ 2 ^ n + 1).minFac - 1) ≤ (2 ^ 2 ^ n + 1).minFac.log2 rw [Nat.log2_eq_log_two]n:ℕ⊢ padicValNat 2 ((2 ^ 2 ^ n + 1).minFac - 1) ≤ log 2 (2 ^ 2 ^ n + 1).minFac
    apply Nat.le_log_of_pow_le (byn:ℕ⊢ 1 < 2 decideAll goals completed! 🐙)
    refine le_trans ?_ <| sub_le _ 1n:ℕ⊢ 2 ^ padicValNat 2 ((2 ^ 2 ^ n + 1).minFac - 1) ≤ (2 ^ 2 ^ n + 1).minFac - 1
    apply Nat.ordProj_le 2n:ℕ⊢ (2 ^ 2 ^ n + 1).minFac - 1 ≠ 0
    exact Nat.sub_ne_zero_of_lt (Nat.minFac_prime (byn:ℕ⊢ 2 ^ 2 ^ n + 1 ≠ 1 norm_numAll goals completed! 🐙)).one_lt
  ·n:ℕ⊢ (2 ^ 2 ^ n + 1).minFac.log2 ≤ 2 ^ n rw [Nat.log2_eq_log_two]n:ℕ⊢ log 2 (2 ^ 2 ^ n + 1).minFac ≤ 2 ^ n
    have : (2 ^ 2 ^ n) + 1 < 2 ^ ((2 ^ n) + 1) := byn:ℕ⊢ padicValNat 2 (n.fermatNumber.minFac - 1) ≤ 2 ^ n - a n
      simp [pow_add, mul_two]All goals completed! 🐙
    refine Nat.le_of_lt_succ <| (2).log_lt_of_lt_pow ?_ ?_refine_1n:ℕthis:2 ^ 2 ^ n + 1 < 2 ^ (2 ^ n + 1) := 
  of_eq_true
    (Eq.trans
      (Eq.trans
        (congrArg (LT.lt (2 ^ 2 ^ n + 1))
          (Eq.trans (pow_add 2 (2 ^ n) 1)
            (Eq.trans (congrArg (HMul.hMul (2 ^ 2 ^ n)) (pow_one 2)) (mul_two (2 ^ 2 ^ n)))))
        (mul_lt_mul_iff_left._simp_2 (2 ^ 2 ^ n)))
      (Eq.trans
        (one_lt_pow_iff._simp_1
          (of_eq_true
            (Eq.trans
              (congrArg Not
                (Eq.trans pow_eq_zero._simp_1
                  (Eq.trans (congrArg (fun x => x ∧ ¬n = 0) (OfNat.ofNat_ne_zero._simp_1 2)) (false_and ¬n = 0))))
              not_false_eq_true)))
        one_lt_ofNat._simp_1))⊢ (2 ^ 2 ^ n + 1).minFac ≠ 0refine_2n:ℕthis:2 ^ 2 ^ n + 1 < 2 ^ (2 ^ n + 1) := 
  of_eq_true
    (Eq.trans
      (Eq.trans
        (congrArg (LT.lt (2 ^ 2 ^ n + 1))
          (Eq.trans (pow_add 2 (2 ^ n) 1)
            (Eq.trans (congrArg (HMul.hMul (2 ^ 2 ^ n)) (pow_one 2)) (mul_two (2 ^ 2 ^ n)))))
        (mul_lt_mul_iff_left._simp_2 (2 ^ 2 ^ n)))
      (Eq.trans
        (one_lt_pow_iff._simp_1
          (of_eq_true
            (Eq.trans
              (congrArg Not
                (Eq.trans pow_eq_zero._simp_1
                  (Eq.trans (congrArg (fun x => x ∧ ¬n = 0) (OfNat.ofNat_ne_zero._simp_1 2)) (false_and ¬n = 0))))
              not_false_eq_true)))
        one_lt_ofNat._simp_1))⊢ (2 ^ 2 ^ n + 1).minFac < 2 ^ (2 ^ n).succ
    ·refine_1n:ℕthis:2 ^ 2 ^ n + 1 < 2 ^ (2 ^ n + 1) := 
  of_eq_true
    (Eq.trans
      (Eq.trans
        (congrArg (LT.lt (2 ^ 2 ^ n + 1))
          (Eq.trans (pow_add 2 (2 ^ n) 1)
            (Eq.trans (congrArg (HMul.hMul (2 ^ 2 ^ n)) (pow_one 2)) (mul_two (2 ^ 2 ^ n)))))
        (mul_lt_mul_iff_left._simp_2 (2 ^ 2 ^ n)))
      (Eq.trans
        (one_lt_pow_iff._simp_1
          (of_eq_true
            (Eq.trans
              (congrArg Not
                (Eq.trans pow_eq_zero._simp_1
                  (Eq.trans (congrArg (fun x => x ∧ ¬n = 0) (OfNat.ofNat_ne_zero._simp_1 2)) (false_and ¬n = 0))))
              not_false_eq_true)))
        one_lt_ofNat._simp_1))⊢ (2 ^ 2 ^ n + 1).minFac ≠ 0 exact Nat.minFac_pos _|>.ne'All goals completed! 🐙
    ·refine_2n:ℕthis:2 ^ 2 ^ n + 1 < 2 ^ (2 ^ n + 1) := 
  of_eq_true
    (Eq.trans
      (Eq.trans
        (congrArg (LT.lt (2 ^ 2 ^ n + 1))
          (Eq.trans (pow_add 2 (2 ^ n) 1)
            (Eq.trans (congrArg (HMul.hMul (2 ^ 2 ^ n)) (pow_one 2)) (mul_two (2 ^ 2 ^ n)))))
        (mul_lt_mul_iff_left._simp_2 (2 ^ 2 ^ n)))
      (Eq.trans
        (one_lt_pow_iff._simp_1
          (of_eq_true
            (Eq.trans
              (congrArg Not
                (Eq.trans pow_eq_zero._simp_1
                  (Eq.trans (congrArg (fun x => x ∧ ¬n = 0) (OfNat.ofNat_ne_zero._simp_1 2)) (false_and ¬n = 0))))
              not_false_eq_true)))
        one_lt_ofNat._simp_1))⊢ (2 ^ 2 ^ n + 1).minFac < 2 ^ (2 ^ n).succ exact (Nat.minFac_le (byn:ℕthis:2 ^ 2 ^ n + 1 < 2 ^ (2 ^ n + 1) := 
  of_eq_true
    (Eq.trans
      (Eq.trans
        (congrArg (LT.lt (2 ^ 2 ^ n + 1))
          (Eq.trans (pow_add 2 (2 ^ n) 1)
            (Eq.trans (congrArg (HMul.hMul (2 ^ 2 ^ n)) (pow_one 2)) (mul_two (2 ^ 2 ^ n)))))
        (mul_lt_mul_iff_left._simp_2 (2 ^ 2 ^ n)))
      (Eq.trans
        (one_lt_pow_iff._simp_1
          (of_eq_true
            (Eq.trans
              (congrArg Not
                (Eq.trans pow_eq_zero._simp_1
                  (Eq.trans (congrArg (fun x => x ∧ ¬n = 0) (OfNat.ofNat_ne_zero._simp_1 2)) (false_and ¬n = 0))))
              not_false_eq_true)))
        one_lt_ofNat._simp_1))⊢ 0 < 2 ^ 2 ^ n + 1 boundAll goals completed! 🐙)).trans_lt this


end OeisA358684