1. FormalConjectures
  2. ErdosProblems
  3. «346»
/- 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

Erdős Problem 346

References:

    erdosproblems.com/346

    [Gr64d] Graham, R. L., A property of Fibonacci numbers. Fibonacci Quart. (1964), 1-10.

    [ErGr80] Erdős, P. and Graham, R., Old and new problems and results in combinatorial number theory. Monographies de L'Enseignement Mathematique (1980).

open Filter Topology Set namespace Erdos346

Is it true that for every lacunary, strongly complete sequence A that is not complete whenever infinitely many terms are removed from it, lim A (n + 1) / A n = (1 + √5) / 2?

@[category research open, AMS 11] theorem declaration uses 'sorry'erdos_346 : answer(sorry) ↔ ∀ {A : ℕ → ℕ}, IsLacunary A → IsAddStronglyCompleteNatSeq A → (∀ B : Set ℕ, B ⊆ range A → B.Infinite → ¬ IsAddComplete (range A \ B)) → Tendsto (fun n => A (n + 1) / (A n : ℝ)) atTop (𝓝 ((1 + √5) / 2)) := ⊢ True ↔ ∀ {A : ℕ → ℕ}, IsLacunary A → IsAddStronglyCompleteNatSeq A → (∀ B ⊆ range A, B.Infinite → ¬IsAddComplete (range A \ B)) → Tendsto (fun n => ↑(A (n + 1)) / ↑(A n)) atTop (𝓝 ((1 + √5) / 2)) All goals completed! 🐙

We define a sequence f by the formula f n = n.fib - (- 1) ^ n.

def f (n : ℕ) : ℕ := if Even n then n.fib - 1 else n.fib + 1

The sequence f is lacunary.

@[category test, AMS 11] theorem erdos_346.variants.f_isLacunary : IsLacunary f := ⊢ IsLacunary f refine ⟨3/2, ⊢ 3 / 2 > 1 All goals completed! 🐙, Filter.eventually_atTop.mpr ⟨9, fun k hk => ?_⟩⟩ -- Key: `2·fib(k+1) > 3·fib(k) + 5` for `k ≥ 9`, since -- `2·fib(k+1) - 3·fib(k) = fib(k-3) ≥ fib(6) = 8 > 5`. have hfib_strict : 3 * Nat.fib k + 5 < 2 * Nat.fib (k + 1) := ⊢ IsLacunary f obtain ⟨m, rfl⟩ : ∃ m, k = m + 9 := ⟨k - 9, k:ℕhk:k ≥ 9⊢ k = k - 9 + 9 All goals completed! 🐙⟩ have h1 : Nat.fib (m + 9 + 1) = Nat.fib (m + 8) + Nat.fib (m + 9) := ⊢ IsLacunary f All goals completed! 🐙 have h2 : Nat.fib (m + 9) = Nat.fib (m + 7) + Nat.fib (m + 8) := ⊢ IsLacunary f All goals completed! 🐙 have h3 : Nat.fib (m + 8) = Nat.fib (m + 6) + Nat.fib (m + 7) := ⊢ IsLacunary f All goals completed! 🐙 have h4 : 8 ≤ Nat.fib (m + 6) := le_trans (m:ℕhk:m + 9 ≥ 9h1:Nat.fib (m + 9 + 1) = Nat.fib (m + 8) + Nat.fib (m + 9) := Eq.mpr (id (congrArg (fun _a => Nat.fib _a = Nat.fib (m + 8) + Nat.fib (m + 9)) (have this := Mathlib.Tactic.Ring.of_eq (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.atom_pf m) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 9))) (Mathlib.Tactic.Ring.add_pf_add_gt (Nat.rawCast 9) (Mathlib.Tactic.Ring.add_pf_add_zero (m ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 1))) (Mathlib.Tactic.Ring.add_pf_add_overlap (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.isNat_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.of_raw ℕ 9) (Mathlib.Meta.NormNum.IsNat.of_raw ℕ 1) (Eq.refl 10))) (Mathlib.Tactic.Ring.add_pf_add_zero (m ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.atom_pf m) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 8))) (Mathlib.Tactic.Ring.add_pf_add_gt (Nat.rawCast 8) (Mathlib.Tactic.Ring.add_pf_add_zero (m ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2))) (Mathlib.Tactic.Ring.add_pf_add_overlap (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.isNat_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.of_raw ℕ 8) (Mathlib.Meta.NormNum.IsNat.of_raw ℕ 2) (Eq.refl 10))) (Mathlib.Tactic.Ring.add_pf_add_zero (m ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))); this))) (Eq.mpr (id (congrArg (fun _a => _a = Nat.fib (m + 8) + Nat.fib (m + 9)) Nat.fib_add_two)) (Eq.refl (Nat.fib (m + 8) + Nat.fib (m + 8 + 1))))h2:Nat.fib (m + 9) = Nat.fib (m + 7) + Nat.fib (m + 8) := Eq.mpr (id (congrArg (fun _a => Nat.fib _a = Nat.fib (m + 7) + Nat.fib (m + 8)) (have this := Mathlib.Tactic.Ring.of_eq (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.atom_pf m) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 9))) (Mathlib.Tactic.Ring.add_pf_add_gt (Nat.rawCast 9) (Mathlib.Tactic.Ring.add_pf_add_zero (m ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.atom_pf m) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 7))) (Mathlib.Tactic.Ring.add_pf_add_gt (Nat.rawCast 7) (Mathlib.Tactic.Ring.add_pf_add_zero (m ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2))) (Mathlib.Tactic.Ring.add_pf_add_overlap (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.isNat_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.of_raw ℕ 7) (Mathlib.Meta.NormNum.IsNat.of_raw ℕ 2) (Eq.refl 9))) (Mathlib.Tactic.Ring.add_pf_add_zero (m ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))); this))) (Eq.mpr (id (congrArg (fun _a => _a = Nat.fib (m + 7) + Nat.fib (m + 8)) Nat.fib_add_two)) (Eq.refl (Nat.fib (m + 7) + Nat.fib (m + 7 + 1))))h3:Nat.fib (m + 8) = Nat.fib (m + 6) + Nat.fib (m + 7) := Eq.mpr (id (congrArg (fun _a => Nat.fib _a = Nat.fib (m + 6) + Nat.fib (m + 7)) (have this := Mathlib.Tactic.Ring.of_eq (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.atom_pf m) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 8))) (Mathlib.Tactic.Ring.add_pf_add_gt (Nat.rawCast 8) (Mathlib.Tactic.Ring.add_pf_add_zero (m ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.atom_pf m) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 6))) (Mathlib.Tactic.Ring.add_pf_add_gt (Nat.rawCast 6) (Mathlib.Tactic.Ring.add_pf_add_zero (m ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2))) (Mathlib.Tactic.Ring.add_pf_add_overlap (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.isNat_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.of_raw ℕ 6) (Mathlib.Meta.NormNum.IsNat.of_raw ℕ 2) (Eq.refl 8))) (Mathlib.Tactic.Ring.add_pf_add_zero (m ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))); this))) (Eq.mpr (id (congrArg (fun _a => _a = Nat.fib (m + 6) + Nat.fib (m + 7)) Nat.fib_add_two)) (Eq.refl (Nat.fib (m + 6) + Nat.fib (m + 6 + 1))))⊢ 8 ≤ Nat.fib 6 All goals completed! 🐙 : 8 ≤ Nat.fib 6) (Nat.fib_mono (m:ℕhk:m + 9 ≥ 9h1:Nat.fib (m + 9 + 1) = Nat.fib (m + 8) + Nat.fib (m + 9) := Eq.mpr (id (congrArg (fun _a => Nat.fib _a = Nat.fib (m + 8) + Nat.fib (m + 9)) (have this := Mathlib.Tactic.Ring.of_eq (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.atom_pf m) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 9))) (Mathlib.Tactic.Ring.add_pf_add_gt (Nat.rawCast 9) (Mathlib.Tactic.Ring.add_pf_add_zero (m ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 1))) (Mathlib.Tactic.Ring.add_pf_add_overlap (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.isNat_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.of_raw ℕ 9) (Mathlib.Meta.NormNum.IsNat.of_raw ℕ 1) (Eq.refl 10))) (Mathlib.Tactic.Ring.add_pf_add_zero (m ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.atom_pf m) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 8))) (Mathlib.Tactic.Ring.add_pf_add_gt (Nat.rawCast 8) (Mathlib.Tactic.Ring.add_pf_add_zero (m ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2))) (Mathlib.Tactic.Ring.add_pf_add_overlap (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.isNat_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.of_raw ℕ 8) (Mathlib.Meta.NormNum.IsNat.of_raw ℕ 2) (Eq.refl 10))) (Mathlib.Tactic.Ring.add_pf_add_zero (m ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))); this))) (Eq.mpr (id (congrArg (fun _a => _a = Nat.fib (m + 8) + Nat.fib (m + 9)) Nat.fib_add_two)) (Eq.refl (Nat.fib (m + 8) + Nat.fib (m + 8 + 1))))h2:Nat.fib (m + 9) = Nat.fib (m + 7) + Nat.fib (m + 8) := Eq.mpr (id (congrArg (fun _a => Nat.fib _a = Nat.fib (m + 7) + Nat.fib (m + 8)) (have this := Mathlib.Tactic.Ring.of_eq (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.atom_pf m) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 9))) (Mathlib.Tactic.Ring.add_pf_add_gt (Nat.rawCast 9) (Mathlib.Tactic.Ring.add_pf_add_zero (m ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.atom_pf m) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 7))) (Mathlib.Tactic.Ring.add_pf_add_gt (Nat.rawCast 7) (Mathlib.Tactic.Ring.add_pf_add_zero (m ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2))) (Mathlib.Tactic.Ring.add_pf_add_overlap (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.isNat_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.of_raw ℕ 7) (Mathlib.Meta.NormNum.IsNat.of_raw ℕ 2) (Eq.refl 9))) (Mathlib.Tactic.Ring.add_pf_add_zero (m ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))); this))) (Eq.mpr (id (congrArg (fun _a => _a = Nat.fib (m + 7) + Nat.fib (m + 8)) Nat.fib_add_two)) (Eq.refl (Nat.fib (m + 7) + Nat.fib (m + 7 + 1))))h3:Nat.fib (m + 8) = Nat.fib (m + 6) + Nat.fib (m + 7) := Eq.mpr (id (congrArg (fun _a => Nat.fib _a = Nat.fib (m + 6) + Nat.fib (m + 7)) (have this := Mathlib.Tactic.Ring.of_eq (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.atom_pf m) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 8))) (Mathlib.Tactic.Ring.add_pf_add_gt (Nat.rawCast 8) (Mathlib.Tactic.Ring.add_pf_add_zero (m ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.atom_pf m) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 6))) (Mathlib.Tactic.Ring.add_pf_add_gt (Nat.rawCast 6) (Mathlib.Tactic.Ring.add_pf_add_zero (m ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2))) (Mathlib.Tactic.Ring.add_pf_add_overlap (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.isNat_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.of_raw ℕ 6) (Mathlib.Meta.NormNum.IsNat.of_raw ℕ 2) (Eq.refl 8))) (Mathlib.Tactic.Ring.add_pf_add_zero (m ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))); this))) (Eq.mpr (id (congrArg (fun _a => _a = Nat.fib (m + 6) + Nat.fib (m + 7)) Nat.fib_add_two)) (Eq.refl (Nat.fib (m + 6) + Nat.fib (m + 6 + 1))))⊢ 6 ≤ m + 6 All goals completed! 🐙)) All goals completed! 🐙 have hfib_R : 3 * (Nat.fib k : ℝ) + 5 < 2 * Nat.fib (k + 1) := ⊢ IsLacunary f All goals completed! 🐙 have hpos : 1 ≤ Nat.fib k := Nat.fib_pos.mpr (k:ℕhk:k ≥ 9hfib_strict:3 * Nat.fib k + 5 < 2 * Nat.fib (k + 1) := Exists.casesOn (Exists.intro (k - 9) (Decidable.byContradiction fun a => f_isLacunary._proof_1 k hk a)) fun m h => Eq.ndrec (motive := fun k => k ≥ 9 → 3 * Nat.fib k + 5 < 2 * Nat.fib (k + 1)) (fun hk => have h1 := Eq.mpr (id (congrArg (fun _a => Nat.fib _a = Nat.fib (m + 8) + Nat.fib (m + 9)) (have this := Mathlib.Tactic.Ring.of_eq (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.atom_pf m) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 9))) (Mathlib.Tactic.Ring.add_pf_add_gt (Nat.rawCast 9) (Mathlib.Tactic.Ring.add_pf_add_zero (m ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 1))) (Mathlib.Tactic.Ring.add_pf_add_overlap (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.isNat_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.of_raw ℕ 9) (Mathlib.Meta.NormNum.IsNat.of_raw ℕ 1) (Eq.refl 10))) (Mathlib.Tactic.Ring.add_pf_add_zero (m ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.atom_pf m) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 8))) (Mathlib.Tactic.Ring.add_pf_add_gt (Nat.rawCast 8) (Mathlib.Tactic.Ring.add_pf_add_zero (m ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2))) (Mathlib.Tactic.Ring.add_pf_add_overlap (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.isNat_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.of_raw ℕ 8) (Mathlib.Meta.NormNum.IsNat.of_raw ℕ 2) (Eq.refl 10))) (Mathlib.Tactic.Ring.add_pf_add_zero (m ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))); this))) (Eq.mpr (id (congrArg (fun _a => _a = Nat.fib (m + 8) + Nat.fib (m + 9)) Nat.fib_add_two)) (Eq.refl (Nat.fib (m + 8) + Nat.fib (m + 8 + 1)))); have h2 := Eq.mpr (id (congrArg (fun _a => Nat.fib _a = Nat.fib (m + 7) + Nat.fib (m + 8)) (have this := Mathlib.Tactic.Ring.of_eq (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.atom_pf m) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 9))) (Mathlib.Tactic.Ring.add_pf_add_gt (Nat.rawCast 9) (Mathlib.Tactic.Ring.add_pf_add_zero (m ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.atom_pf m) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 7))) (Mathlib.Tactic.Ring.add_pf_add_gt (Nat.rawCast 7) (Mathlib.Tactic.Ring.add_pf_add_zero (m ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2))) (Mathlib.Tactic.Ring.add_pf_add_overlap (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.isNat_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.of_raw ℕ 7) (Mathlib.Meta.NormNum.IsNat.of_raw ℕ 2) (Eq.refl 9))) (Mathlib.Tactic.Ring.add_pf_add_zero (m ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))); this))) (Eq.mpr (id (congrArg (fun _a => _a = Nat.fib (m + 7) + Nat.fib (m + 8)) Nat.fib_add_two)) (Eq.refl (Nat.fib (m + 7) + Nat.fib (m + 7 + 1)))); have h3 := Eq.mpr (id (congrArg (fun _a => Nat.fib _a = Nat.fib (m + 6) + Nat.fib (m + 7)) (have this := Mathlib.Tactic.Ring.of_eq (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.atom_pf m) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 8))) (Mathlib.Tactic.Ring.add_pf_add_gt (Nat.rawCast 8) (Mathlib.Tactic.Ring.add_pf_add_zero (m ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.atom_pf m) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 6))) (Mathlib.Tactic.Ring.add_pf_add_gt (Nat.rawCast 6) (Mathlib.Tactic.Ring.add_pf_add_zero (m ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2))) (Mathlib.Tactic.Ring.add_pf_add_overlap (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.isNat_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.of_raw ℕ 6) (Mathlib.Meta.NormNum.IsNat.of_raw ℕ 2) (Eq.refl 8))) (Mathlib.Tactic.Ring.add_pf_add_zero (m ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))); this))) (Eq.mpr (id (congrArg (fun _a => _a = Nat.fib (m + 6) + Nat.fib (m + 7)) Nat.fib_add_two)) (Eq.refl (Nat.fib (m + 6) + Nat.fib (m + 6 + 1)))); have h4 := le_trans (of_decide_eq_true (id (Eq.refl true))) (Nat.fib_mono (Decidable.byContradiction fun a => f_isLacunary._proof_2 m hk a)); Decidable.byContradiction fun a => f_isLacunary._proof_3 m h1 h2 h3 h4 a) (Eq.symm h) hkhfib_R:3 * ↑(Nat.fib k) + 5 < 2 * ↑(Nat.fib (k + 1)) := cast (Eq.symm (Eq.trans (congr (congrArg LT.lt (Eq.trans (congrArg (fun x => x + ↑5) (Nat.cast_mul._simp_1 3 (Nat.fib k))) (Nat.cast_add._simp_1 (3 * Nat.fib k) 5))) (Nat.cast_mul._simp_1 2 (Nat.fib (k + 1)))) Nat.cast_lt._simp_1)) hfib_strict⊢ 0 < k All goals completed! 🐙) have hpos1 : 1 ≤ Nat.fib (k + 1) := Nat.fib_pos.mpr (k:ℕhk:k ≥ 9hfib_strict:3 * Nat.fib k + 5 < 2 * Nat.fib (k + 1) := Exists.casesOn (Exists.intro (k - 9) (Decidable.byContradiction fun a => f_isLacunary._proof_1 k hk a)) fun m h => Eq.ndrec (motive := fun k => k ≥ 9 → 3 * Nat.fib k + 5 < 2 * Nat.fib (k + 1)) (fun hk => have h1 := Eq.mpr (id (congrArg (fun _a => Nat.fib _a = Nat.fib (m + 8) + Nat.fib (m + 9)) (have this := Mathlib.Tactic.Ring.of_eq (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.atom_pf m) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 9))) (Mathlib.Tactic.Ring.add_pf_add_gt (Nat.rawCast 9) (Mathlib.Tactic.Ring.add_pf_add_zero (m ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 1))) (Mathlib.Tactic.Ring.add_pf_add_overlap (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.isNat_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.of_raw ℕ 9) (Mathlib.Meta.NormNum.IsNat.of_raw ℕ 1) (Eq.refl 10))) (Mathlib.Tactic.Ring.add_pf_add_zero (m ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.atom_pf m) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 8))) (Mathlib.Tactic.Ring.add_pf_add_gt (Nat.rawCast 8) (Mathlib.Tactic.Ring.add_pf_add_zero (m ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2))) (Mathlib.Tactic.Ring.add_pf_add_overlap (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.isNat_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.of_raw ℕ 8) (Mathlib.Meta.NormNum.IsNat.of_raw ℕ 2) (Eq.refl 10))) (Mathlib.Tactic.Ring.add_pf_add_zero (m ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))); this))) (Eq.mpr (id (congrArg (fun _a => _a = Nat.fib (m + 8) + Nat.fib (m + 9)) Nat.fib_add_two)) (Eq.refl (Nat.fib (m + 8) + Nat.fib (m + 8 + 1)))); have h2 := Eq.mpr (id (congrArg (fun _a => Nat.fib _a = Nat.fib (m + 7) + Nat.fib (m + 8)) (have this := Mathlib.Tactic.Ring.of_eq (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.atom_pf m) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 9))) (Mathlib.Tactic.Ring.add_pf_add_gt (Nat.rawCast 9) (Mathlib.Tactic.Ring.add_pf_add_zero (m ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.atom_pf m) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 7))) (Mathlib.Tactic.Ring.add_pf_add_gt (Nat.rawCast 7) (Mathlib.Tactic.Ring.add_pf_add_zero (m ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2))) (Mathlib.Tactic.Ring.add_pf_add_overlap (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.isNat_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.of_raw ℕ 7) (Mathlib.Meta.NormNum.IsNat.of_raw ℕ 2) (Eq.refl 9))) (Mathlib.Tactic.Ring.add_pf_add_zero (m ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))); this))) (Eq.mpr (id (congrArg (fun _a => _a = Nat.fib (m + 7) + Nat.fib (m + 8)) Nat.fib_add_two)) (Eq.refl (Nat.fib (m + 7) + Nat.fib (m + 7 + 1)))); have h3 := Eq.mpr (id (congrArg (fun _a => Nat.fib _a = Nat.fib (m + 6) + Nat.fib (m + 7)) (have this := Mathlib.Tactic.Ring.of_eq (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.atom_pf m) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 8))) (Mathlib.Tactic.Ring.add_pf_add_gt (Nat.rawCast 8) (Mathlib.Tactic.Ring.add_pf_add_zero (m ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.atom_pf m) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 6))) (Mathlib.Tactic.Ring.add_pf_add_gt (Nat.rawCast 6) (Mathlib.Tactic.Ring.add_pf_add_zero (m ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2))) (Mathlib.Tactic.Ring.add_pf_add_overlap (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.isNat_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.of_raw ℕ 6) (Mathlib.Meta.NormNum.IsNat.of_raw ℕ 2) (Eq.refl 8))) (Mathlib.Tactic.Ring.add_pf_add_zero (m ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))); this))) (Eq.mpr (id (congrArg (fun _a => _a = Nat.fib (m + 6) + Nat.fib (m + 7)) Nat.fib_add_two)) (Eq.refl (Nat.fib (m + 6) + Nat.fib (m + 6 + 1)))); have h4 := le_trans (of_decide_eq_true (id (Eq.refl true))) (Nat.fib_mono (Decidable.byContradiction fun a => f_isLacunary._proof_2 m hk a)); Decidable.byContradiction fun a => f_isLacunary._proof_3 m h1 h2 h3 h4 a) (Eq.symm h) hkhfib_R:3 * ↑(Nat.fib k) + 5 < 2 * ↑(Nat.fib (k + 1)) := cast (Eq.symm (Eq.trans (congr (congrArg LT.lt (Eq.trans (congrArg (fun x => x + ↑5) (Nat.cast_mul._simp_1 3 (Nat.fib k))) (Nat.cast_add._simp_1 (3 * Nat.fib k) 5))) (Nat.cast_mul._simp_1 2 (Nat.fib (k + 1)))) Nat.cast_lt._simp_1)) hfib_stricthpos:1 ≤ Nat.fib k := Nat.fib_pos.mpr (Decidable.byContradiction fun a => f_isLacunary._proof_4 k hk a)⊢ 0 < k + 1 All goals completed! 🐙) k:ℕhk:k ≥ 9hfib_strict:3 * Nat.fib k + 5 < 2 * Nat.fib (k + 1) := Exists.casesOn (Exists.intro (k - 9) (Decidable.byContradiction fun a => f_isLacunary._proof_1 k hk a)) fun m h => Eq.ndrec (motive := fun k => k ≥ 9 → 3 * Nat.fib k + 5 < 2 * Nat.fib (k + 1)) (fun hk => have h1 := Eq.mpr (id (congrArg (fun _a => Nat.fib _a = Nat.fib (m + 8) + Nat.fib (m + 9)) (have this := Mathlib.Tactic.Ring.of_eq (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.atom_pf m) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 9))) (Mathlib.Tactic.Ring.add_pf_add_gt (Nat.rawCast 9) (Mathlib.Tactic.Ring.add_pf_add_zero (m ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 1))) (Mathlib.Tactic.Ring.add_pf_add_overlap (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.isNat_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.of_raw ℕ 9) (Mathlib.Meta.NormNum.IsNat.of_raw ℕ 1) (Eq.refl 10))) (Mathlib.Tactic.Ring.add_pf_add_zero (m ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.atom_pf m) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 8))) (Mathlib.Tactic.Ring.add_pf_add_gt (Nat.rawCast 8) (Mathlib.Tactic.Ring.add_pf_add_zero (m ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2))) (Mathlib.Tactic.Ring.add_pf_add_overlap (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.isNat_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.of_raw ℕ 8) (Mathlib.Meta.NormNum.IsNat.of_raw ℕ 2) (Eq.refl 10))) (Mathlib.Tactic.Ring.add_pf_add_zero (m ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))); this))) (Eq.mpr (id (congrArg (fun _a => _a = Nat.fib (m + 8) + Nat.fib (m + 9)) Nat.fib_add_two)) (Eq.refl (Nat.fib (m + 8) + Nat.fib (m + 8 + 1)))); have h2 := Eq.mpr (id (congrArg (fun _a => Nat.fib _a = Nat.fib (m + 7) + Nat.fib (m + 8)) (have this := Mathlib.Tactic.Ring.of_eq (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.atom_pf m) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 9))) (Mathlib.Tactic.Ring.add_pf_add_gt (Nat.rawCast 9) (Mathlib.Tactic.Ring.add_pf_add_zero (m ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.atom_pf m) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 7))) (Mathlib.Tactic.Ring.add_pf_add_gt (Nat.rawCast 7) (Mathlib.Tactic.Ring.add_pf_add_zero (m ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2))) (Mathlib.Tactic.Ring.add_pf_add_overlap (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.isNat_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.of_raw ℕ 7) (Mathlib.Meta.NormNum.IsNat.of_raw ℕ 2) (Eq.refl 9))) (Mathlib.Tactic.Ring.add_pf_add_zero (m ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))); this))) (Eq.mpr (id (congrArg (fun _a => _a = Nat.fib (m + 7) + Nat.fib (m + 8)) Nat.fib_add_two)) (Eq.refl (Nat.fib (m + 7) + Nat.fib (m + 7 + 1)))); have h3 := Eq.mpr (id (congrArg (fun _a => Nat.fib _a = Nat.fib (m + 6) + Nat.fib (m + 7)) (have this := Mathlib.Tactic.Ring.of_eq (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.atom_pf m) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 8))) (Mathlib.Tactic.Ring.add_pf_add_gt (Nat.rawCast 8) (Mathlib.Tactic.Ring.add_pf_add_zero (m ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.atom_pf m) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 6))) (Mathlib.Tactic.Ring.add_pf_add_gt (Nat.rawCast 6) (Mathlib.Tactic.Ring.add_pf_add_zero (m ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2))) (Mathlib.Tactic.Ring.add_pf_add_overlap (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.isNat_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.of_raw ℕ 6) (Mathlib.Meta.NormNum.IsNat.of_raw ℕ 2) (Eq.refl 8))) (Mathlib.Tactic.Ring.add_pf_add_zero (m ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))); this))) (Eq.mpr (id (congrArg (fun _a => _a = Nat.fib (m + 6) + Nat.fib (m + 7)) Nat.fib_add_two)) (Eq.refl (Nat.fib (m + 6) + Nat.fib (m + 6 + 1)))); have h4 := le_trans (of_decide_eq_true (id (Eq.refl true))) (Nat.fib_mono (Decidable.byContradiction fun a => f_isLacunary._proof_2 m hk a)); Decidable.byContradiction fun a => f_isLacunary._proof_3 m h1 h2 h3 h4 a) (Eq.symm h) hkhfib_R:3 * ↑(Nat.fib k) + 5 < 2 * ↑(Nat.fib (k + 1)) := cast (Eq.symm (Eq.trans (congr (congrArg LT.lt (Eq.trans (congrArg (fun x => x + ↑5) (Nat.cast_mul._simp_1 3 (Nat.fib k))) (Nat.cast_add._simp_1 (3 * Nat.fib k) 5))) (Nat.cast_mul._simp_1 2 (Nat.fib (k + 1)))) Nat.cast_lt._simp_1)) hfib_stricthpos:1 ≤ Nat.fib k := Nat.fib_pos.mpr (Decidable.byContradiction fun a => f_isLacunary._proof_4 k hk a)hpos1:1 ≤ Nat.fib (k + 1) := Nat.fib_pos.mpr (Decidable.byContradiction fun a => f_isLacunary._proof_5 k hk a)⊢ 3 / 2 * ↑(if Even k then Nat.fib k - 1 else Nat.fib k + 1) < ↑(if Even (k + 1) then Nat.fib (k + 1) - 1 else Nat.fib (k + 1) + 1) k:ℕhk:k ≥ 9hfib_strict:3 * Nat.fib k + 5 < 2 * Nat.fib (k + 1) := Exists.casesOn (Exists.intro (k - 9) (Decidable.byContradiction fun a => f_isLacunary._proof_1 k hk a)) fun m h => Eq.ndrec (motive := fun k => k ≥ 9 → 3 * Nat.fib k + 5 < 2 * Nat.fib (k + 1)) (fun hk => have h1 := Eq.mpr (id (congrArg (fun _a => Nat.fib _a = Nat.fib (m + 8) + Nat.fib (m + 9)) (have this := Mathlib.Tactic.Ring.of_eq (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.atom_pf m) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 9))) (Mathlib.Tactic.Ring.add_pf_add_gt (Nat.rawCast 9) (Mathlib.Tactic.Ring.add_pf_add_zero (m ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 1))) (Mathlib.Tactic.Ring.add_pf_add_overlap (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.isNat_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.of_raw ℕ 9) (Mathlib.Meta.NormNum.IsNat.of_raw ℕ 1) (Eq.refl 10))) (Mathlib.Tactic.Ring.add_pf_add_zero (m ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.atom_pf m) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 8))) (Mathlib.Tactic.Ring.add_pf_add_gt (Nat.rawCast 8) (Mathlib.Tactic.Ring.add_pf_add_zero (m ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2))) (Mathlib.Tactic.Ring.add_pf_add_overlap (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.isNat_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.of_raw ℕ 8) (Mathlib.Meta.NormNum.IsNat.of_raw ℕ 2) (Eq.refl 10))) (Mathlib.Tactic.Ring.add_pf_add_zero (m ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))); this))) (Eq.mpr (id (congrArg (fun _a => _a = Nat.fib (m + 8) + Nat.fib (m + 9)) Nat.fib_add_two)) (Eq.refl (Nat.fib (m + 8) + Nat.fib (m + 8 + 1)))); have h2 := Eq.mpr (id (congrArg (fun _a => Nat.fib _a = Nat.fib (m + 7) + Nat.fib (m + 8)) (have this := Mathlib.Tactic.Ring.of_eq (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.atom_pf m) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 9))) (Mathlib.Tactic.Ring.add_pf_add_gt (Nat.rawCast 9) (Mathlib.Tactic.Ring.add_pf_add_zero (m ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.atom_pf m) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 7))) (Mathlib.Tactic.Ring.add_pf_add_gt (Nat.rawCast 7) (Mathlib.Tactic.Ring.add_pf_add_zero (m ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2))) (Mathlib.Tactic.Ring.add_pf_add_overlap (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.isNat_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.of_raw ℕ 7) (Mathlib.Meta.NormNum.IsNat.of_raw ℕ 2) (Eq.refl 9))) (Mathlib.Tactic.Ring.add_pf_add_zero (m ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))); this))) (Eq.mpr (id (congrArg (fun _a => _a = Nat.fib (m + 7) + Nat.fib (m + 8)) Nat.fib_add_two)) (Eq.refl (Nat.fib (m + 7) + Nat.fib (m + 7 + 1)))); have h3 := Eq.mpr (id (congrArg (fun _a => Nat.fib _a = Nat.fib (m + 6) + Nat.fib (m + 7)) (have this := Mathlib.Tactic.Ring.of_eq (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.atom_pf m) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 8))) (Mathlib.Tactic.Ring.add_pf_add_gt (Nat.rawCast 8) (Mathlib.Tactic.Ring.add_pf_add_zero (m ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.atom_pf m) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 6))) (Mathlib.Tactic.Ring.add_pf_add_gt (Nat.rawCast 6) (Mathlib.Tactic.Ring.add_pf_add_zero (m ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2))) (Mathlib.Tactic.Ring.add_pf_add_overlap (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.isNat_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.of_raw ℕ 6) (Mathlib.Meta.NormNum.IsNat.of_raw ℕ 2) (Eq.refl 8))) (Mathlib.Tactic.Ring.add_pf_add_zero (m ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))); this))) (Eq.mpr (id (congrArg (fun _a => _a = Nat.fib (m + 6) + Nat.fib (m + 7)) Nat.fib_add_two)) (Eq.refl (Nat.fib (m + 6) + Nat.fib (m + 6 + 1)))); have h4 := le_trans (of_decide_eq_true (id (Eq.refl true))) (Nat.fib_mono (Decidable.byContradiction fun a => f_isLacunary._proof_2 m hk a)); Decidable.byContradiction fun a => f_isLacunary._proof_3 m h1 h2 h3 h4 a) (Eq.symm h) hkhfib_R:3 * ↑(Nat.fib k) + 5 < 2 * ↑(Nat.fib (k + 1)) := cast (Eq.symm (Eq.trans (congr (congrArg LT.lt (Eq.trans (congrArg (fun x => x + ↑5) (Nat.cast_mul._simp_1 3 (Nat.fib k))) (Nat.cast_add._simp_1 (3 * Nat.fib k) 5))) (Nat.cast_mul._simp_1 2 (Nat.fib (k + 1)))) Nat.cast_lt._simp_1)) hfib_stricthpos:1 ≤ Nat.fib k := Nat.fib_pos.mpr (Decidable.byContradiction fun a => f_isLacunary._proof_4 k hk a)hpos1:1 ≤ Nat.fib (k + 1) := Nat.fib_pos.mpr (Decidable.byContradiction fun a => f_isLacunary._proof_5 k hk a)heven:Even k⊢ 3 / 2 * ↑(if Even k then Nat.fib k - 1 else Nat.fib k + 1) < ↑(if Even (k + 1) then Nat.fib (k + 1) - 1 else Nat.fib (k + 1) + 1)k:ℕhk:k ≥ 9hfib_strict:3 * Nat.fib k + 5 < 2 * Nat.fib (k + 1) := Exists.casesOn (Exists.intro (k - 9) (Decidable.byContradiction fun a => f_isLacunary._proof_1 k hk a)) fun m h => Eq.ndrec (motive := fun k => k ≥ 9 → 3 * Nat.fib k + 5 < 2 * Nat.fib (k + 1)) (fun hk => have h1 := Eq.mpr (id (congrArg (fun _a => Nat.fib _a = Nat.fib (m + 8) + Nat.fib (m + 9)) (have this := Mathlib.Tactic.Ring.of_eq (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.atom_pf m) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 9))) (Mathlib.Tactic.Ring.add_pf_add_gt (Nat.rawCast 9) (Mathlib.Tactic.Ring.add_pf_add_zero (m ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 1))) (Mathlib.Tactic.Ring.add_pf_add_overlap (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.isNat_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.of_raw ℕ 9) (Mathlib.Meta.NormNum.IsNat.of_raw ℕ 1) (Eq.refl 10))) (Mathlib.Tactic.Ring.add_pf_add_zero (m ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.atom_pf m) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 8))) (Mathlib.Tactic.Ring.add_pf_add_gt (Nat.rawCast 8) (Mathlib.Tactic.Ring.add_pf_add_zero (m ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2))) (Mathlib.Tactic.Ring.add_pf_add_overlap (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.isNat_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.of_raw ℕ 8) (Mathlib.Meta.NormNum.IsNat.of_raw ℕ 2) (Eq.refl 10))) (Mathlib.Tactic.Ring.add_pf_add_zero (m ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))); this))) (Eq.mpr (id (congrArg (fun _a => _a = Nat.fib (m + 8) + Nat.fib (m + 9)) Nat.fib_add_two)) (Eq.refl (Nat.fib (m + 8) + Nat.fib (m + 8 + 1)))); have h2 := Eq.mpr (id (congrArg (fun _a => Nat.fib _a = Nat.fib (m + 7) + Nat.fib (m + 8)) (have this := Mathlib.Tactic.Ring.of_eq (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.atom_pf m) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 9))) (Mathlib.Tactic.Ring.add_pf_add_gt (Nat.rawCast 9) (Mathlib.Tactic.Ring.add_pf_add_zero (m ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.atom_pf m) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 7))) (Mathlib.Tactic.Ring.add_pf_add_gt (Nat.rawCast 7) (Mathlib.Tactic.Ring.add_pf_add_zero (m ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2))) (Mathlib.Tactic.Ring.add_pf_add_overlap (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.isNat_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.of_raw ℕ 7) (Mathlib.Meta.NormNum.IsNat.of_raw ℕ 2) (Eq.refl 9))) (Mathlib.Tactic.Ring.add_pf_add_zero (m ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))); this))) (Eq.mpr (id (congrArg (fun _a => _a = Nat.fib (m + 7) + Nat.fib (m + 8)) Nat.fib_add_two)) (Eq.refl (Nat.fib (m + 7) + Nat.fib (m + 7 + 1)))); have h3 := Eq.mpr (id (congrArg (fun _a => Nat.fib _a = Nat.fib (m + 6) + Nat.fib (m + 7)) (have this := Mathlib.Tactic.Ring.of_eq (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.atom_pf m) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 8))) (Mathlib.Tactic.Ring.add_pf_add_gt (Nat.rawCast 8) (Mathlib.Tactic.Ring.add_pf_add_zero (m ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.atom_pf m) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 6))) (Mathlib.Tactic.Ring.add_pf_add_gt (Nat.rawCast 6) (Mathlib.Tactic.Ring.add_pf_add_zero (m ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2))) (Mathlib.Tactic.Ring.add_pf_add_overlap (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.isNat_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.of_raw ℕ 6) (Mathlib.Meta.NormNum.IsNat.of_raw ℕ 2) (Eq.refl 8))) (Mathlib.Tactic.Ring.add_pf_add_zero (m ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))); this))) (Eq.mpr (id (congrArg (fun _a => _a = Nat.fib (m + 6) + Nat.fib (m + 7)) Nat.fib_add_two)) (Eq.refl (Nat.fib (m + 6) + Nat.fib (m + 6 + 1)))); have h4 := le_trans (of_decide_eq_true (id (Eq.refl true))) (Nat.fib_mono (Decidable.byContradiction fun a => f_isLacunary._proof_2 m hk a)); Decidable.byContradiction fun a => f_isLacunary._proof_3 m h1 h2 h3 h4 a) (Eq.symm h) hkhfib_R:3 * ↑(Nat.fib k) + 5 < 2 * ↑(Nat.fib (k + 1)) := cast (Eq.symm (Eq.trans (congr (congrArg LT.lt (Eq.trans (congrArg (fun x => x + ↑5) (Nat.cast_mul._simp_1 3 (Nat.fib k))) (Nat.cast_add._simp_1 (3 * Nat.fib k) 5))) (Nat.cast_mul._simp_1 2 (Nat.fib (k + 1)))) Nat.cast_lt._simp_1)) hfib_stricthpos:1 ≤ Nat.fib k := Nat.fib_pos.mpr (Decidable.byContradiction fun a => f_isLacunary._proof_4 k hk a)hpos1:1 ≤ Nat.fib (k + 1) := Nat.fib_pos.mpr (Decidable.byContradiction fun a => f_isLacunary._proof_5 k hk a)heven:¬Even k⊢ 3 / 2 * ↑(if Even k then Nat.fib k - 1 else Nat.fib k + 1) < ↑(if Even (k + 1) then Nat.fib (k + 1) - 1 else Nat.fib (k + 1) + 1) k:ℕhk:k ≥ 9hfib_strict:3 * Nat.fib k + 5 < 2 * Nat.fib (k + 1) := Exists.casesOn (Exists.intro (k - 9) (Decidable.byContradiction fun a => f_isLacunary._proof_1 k hk a)) fun m h => Eq.ndrec (motive := fun k => k ≥ 9 → 3 * Nat.fib k + 5 < 2 * Nat.fib (k + 1)) (fun hk => have h1 := Eq.mpr (id (congrArg (fun _a => Nat.fib _a = Nat.fib (m + 8) + Nat.fib (m + 9)) (have this := Mathlib.Tactic.Ring.of_eq (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.atom_pf m) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 9))) (Mathlib.Tactic.Ring.add_pf_add_gt (Nat.rawCast 9) (Mathlib.Tactic.Ring.add_pf_add_zero (m ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 1))) (Mathlib.Tactic.Ring.add_pf_add_overlap (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.isNat_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.of_raw ℕ 9) (Mathlib.Meta.NormNum.IsNat.of_raw ℕ 1) (Eq.refl 10))) (Mathlib.Tactic.Ring.add_pf_add_zero (m ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.atom_pf m) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 8))) (Mathlib.Tactic.Ring.add_pf_add_gt (Nat.rawCast 8) (Mathlib.Tactic.Ring.add_pf_add_zero (m ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2))) (Mathlib.Tactic.Ring.add_pf_add_overlap (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.isNat_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.of_raw ℕ 8) (Mathlib.Meta.NormNum.IsNat.of_raw ℕ 2) (Eq.refl 10))) (Mathlib.Tactic.Ring.add_pf_add_zero (m ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))); this))) (Eq.mpr (id (congrArg (fun _a => _a = Nat.fib (m + 8) + Nat.fib (m + 9)) Nat.fib_add_two)) (Eq.refl (Nat.fib (m + 8) + Nat.fib (m + 8 + 1)))); have h2 := Eq.mpr (id (congrArg (fun _a => Nat.fib _a = Nat.fib (m + 7) + Nat.fib (m + 8)) (have this := Mathlib.Tactic.Ring.of_eq (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.atom_pf m) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 9))) (Mathlib.Tactic.Ring.add_pf_add_gt (Nat.rawCast 9) (Mathlib.Tactic.Ring.add_pf_add_zero (m ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.atom_pf m) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 7))) (Mathlib.Tactic.Ring.add_pf_add_gt (Nat.rawCast 7) (Mathlib.Tactic.Ring.add_pf_add_zero (m ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2))) (Mathlib.Tactic.Ring.add_pf_add_overlap (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.isNat_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.of_raw ℕ 7) (Mathlib.Meta.NormNum.IsNat.of_raw ℕ 2) (Eq.refl 9))) (Mathlib.Tactic.Ring.add_pf_add_zero (m ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))); this))) (Eq.mpr (id (congrArg (fun _a => _a = Nat.fib (m + 7) + Nat.fib (m + 8)) Nat.fib_add_two)) (Eq.refl (Nat.fib (m + 7) + Nat.fib (m + 7 + 1)))); have h3 := Eq.mpr (id (congrArg (fun _a => Nat.fib _a = Nat.fib (m + 6) + Nat.fib (m + 7)) (have this := Mathlib.Tactic.Ring.of_eq (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.atom_pf m) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 8))) (Mathlib.Tactic.Ring.add_pf_add_gt (Nat.rawCast 8) (Mathlib.Tactic.Ring.add_pf_add_zero (m ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.atom_pf m) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 6))) (Mathlib.Tactic.Ring.add_pf_add_gt (Nat.rawCast 6) (Mathlib.Tactic.Ring.add_pf_add_zero (m ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2))) (Mathlib.Tactic.Ring.add_pf_add_overlap (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.isNat_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.of_raw ℕ 6) (Mathlib.Meta.NormNum.IsNat.of_raw ℕ 2) (Eq.refl 8))) (Mathlib.Tactic.Ring.add_pf_add_zero (m ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))); this))) (Eq.mpr (id (congrArg (fun _a => _a = Nat.fib (m + 6) + Nat.fib (m + 7)) Nat.fib_add_two)) (Eq.refl (Nat.fib (m + 6) + Nat.fib (m + 6 + 1)))); have h4 := le_trans (of_decide_eq_true (id (Eq.refl true))) (Nat.fib_mono (Decidable.byContradiction fun a => f_isLacunary._proof_2 m hk a)); Decidable.byContradiction fun a => f_isLacunary._proof_3 m h1 h2 h3 h4 a) (Eq.symm h) hkhfib_R:3 * ↑(Nat.fib k) + 5 < 2 * ↑(Nat.fib (k + 1)) := cast (Eq.symm (Eq.trans (congr (congrArg LT.lt (Eq.trans (congrArg (fun x => x + ↑5) (Nat.cast_mul._simp_1 3 (Nat.fib k))) (Nat.cast_add._simp_1 (3 * Nat.fib k) 5))) (Nat.cast_mul._simp_1 2 (Nat.fib (k + 1)))) Nat.cast_lt._simp_1)) hfib_stricthpos:1 ≤ Nat.fib k := Nat.fib_pos.mpr (Decidable.byContradiction fun a => f_isLacunary._proof_4 k hk a)hpos1:1 ≤ Nat.fib (k + 1) := Nat.fib_pos.mpr (Decidable.byContradiction fun a => f_isLacunary._proof_5 k hk a)heven:Even k⊢ 3 / 2 * ↑(if Even k then Nat.fib k - 1 else Nat.fib k + 1) < ↑(if Even (k + 1) then Nat.fib (k + 1) - 1 else Nat.fib (k + 1) + 1) have hodd : ¬ Even (k + 1) := ⊢ IsLacunary f All goals completed! 🐙 k:ℕhk:k ≥ 9hfib_strict:3 * Nat.fib k + 5 < 2 * Nat.fib (k + 1) := Exists.casesOn (Exists.intro (k - 9) (Decidable.byContradiction fun a => f_isLacunary._proof_1 k hk a)) fun m h => Eq.ndrec (motive := fun k => k ≥ 9 → 3 * Nat.fib k + 5 < 2 * Nat.fib (k + 1)) (fun hk => have h1 := Eq.mpr (id (congrArg (fun _a => Nat.fib _a = Nat.fib (m + 8) + Nat.fib (m + 9)) (have this := Mathlib.Tactic.Ring.of_eq (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.atom_pf m) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 9))) (Mathlib.Tactic.Ring.add_pf_add_gt (Nat.rawCast 9) (Mathlib.Tactic.Ring.add_pf_add_zero (m ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 1))) (Mathlib.Tactic.Ring.add_pf_add_overlap (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.isNat_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.of_raw ℕ 9) (Mathlib.Meta.NormNum.IsNat.of_raw ℕ 1) (Eq.refl 10))) (Mathlib.Tactic.Ring.add_pf_add_zero (m ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.atom_pf m) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 8))) (Mathlib.Tactic.Ring.add_pf_add_gt (Nat.rawCast 8) (Mathlib.Tactic.Ring.add_pf_add_zero (m ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2))) (Mathlib.Tactic.Ring.add_pf_add_overlap (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.isNat_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.of_raw ℕ 8) (Mathlib.Meta.NormNum.IsNat.of_raw ℕ 2) (Eq.refl 10))) (Mathlib.Tactic.Ring.add_pf_add_zero (m ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))); this))) (Eq.mpr (id (congrArg (fun _a => _a = Nat.fib (m + 8) + Nat.fib (m + 9)) Nat.fib_add_two)) (Eq.refl (Nat.fib (m + 8) + Nat.fib (m + 8 + 1)))); have h2 := Eq.mpr (id (congrArg (fun _a => Nat.fib _a = Nat.fib (m + 7) + Nat.fib (m + 8)) (have this := Mathlib.Tactic.Ring.of_eq (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.atom_pf m) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 9))) (Mathlib.Tactic.Ring.add_pf_add_gt (Nat.rawCast 9) (Mathlib.Tactic.Ring.add_pf_add_zero (m ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.atom_pf m) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 7))) (Mathlib.Tactic.Ring.add_pf_add_gt (Nat.rawCast 7) (Mathlib.Tactic.Ring.add_pf_add_zero (m ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2))) (Mathlib.Tactic.Ring.add_pf_add_overlap (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.isNat_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.of_raw ℕ 7) (Mathlib.Meta.NormNum.IsNat.of_raw ℕ 2) (Eq.refl 9))) (Mathlib.Tactic.Ring.add_pf_add_zero (m ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))); this))) (Eq.mpr (id (congrArg (fun _a => _a = Nat.fib (m + 7) + Nat.fib (m + 8)) Nat.fib_add_two)) (Eq.refl (Nat.fib (m + 7) + Nat.fib (m + 7 + 1)))); have h3 := Eq.mpr (id (congrArg (fun _a => Nat.fib _a = Nat.fib (m + 6) + Nat.fib (m + 7)) (have this := Mathlib.Tactic.Ring.of_eq (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.atom_pf m) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 8))) (Mathlib.Tactic.Ring.add_pf_add_gt (Nat.rawCast 8) (Mathlib.Tactic.Ring.add_pf_add_zero (m ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.atom_pf m) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 6))) (Mathlib.Tactic.Ring.add_pf_add_gt (Nat.rawCast 6) (Mathlib.Tactic.Ring.add_pf_add_zero (m ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2))) (Mathlib.Tactic.Ring.add_pf_add_overlap (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.isNat_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.of_raw ℕ 6) (Mathlib.Meta.NormNum.IsNat.of_raw ℕ 2) (Eq.refl 8))) (Mathlib.Tactic.Ring.add_pf_add_zero (m ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))); this))) (Eq.mpr (id (congrArg (fun _a => _a = Nat.fib (m + 6) + Nat.fib (m + 7)) Nat.fib_add_two)) (Eq.refl (Nat.fib (m + 6) + Nat.fib (m + 6 + 1)))); have h4 := le_trans (of_decide_eq_true (id (Eq.refl true))) (Nat.fib_mono (Decidable.byContradiction fun a => f_isLacunary._proof_2 m hk a)); Decidable.byContradiction fun a => f_isLacunary._proof_3 m h1 h2 h3 h4 a) (Eq.symm h) hkhfib_R:3 * ↑(Nat.fib k) + 5 < 2 * ↑(Nat.fib (k + 1)) := cast (Eq.symm (Eq.trans (congr (congrArg LT.lt (Eq.trans (congrArg (fun x => x + ↑5) (Nat.cast_mul._simp_1 3 (Nat.fib k))) (Nat.cast_add._simp_1 (3 * Nat.fib k) 5))) (Nat.cast_mul._simp_1 2 (Nat.fib (k + 1)))) Nat.cast_lt._simp_1)) hfib_stricthpos:1 ≤ Nat.fib k := Nat.fib_pos.mpr (Decidable.byContradiction fun a => f_isLacunary._proof_4 k hk a)hpos1:1 ≤ Nat.fib (k + 1) := Nat.fib_pos.mpr (Decidable.byContradiction fun a => f_isLacunary._proof_5 k hk a)heven:Even khodd:¬Even (k + 1) := of_eq_true (Eq.trans (congrArg Not (Eq.trans f_isLacunary._simp_5 (Eq.trans (congrArg Not (eq_true heven)) not_true_eq_false))) not_false_eq_true)⊢ 3 / 2 * ↑(Nat.fib k - 1) < ↑(Nat.fib (k + 1) + 1) k:ℕhk:k ≥ 9hfib_strict:3 * Nat.fib k + 5 < 2 * Nat.fib (k + 1) := Exists.casesOn (Exists.intro (k - 9) (Decidable.byContradiction fun a => f_isLacunary._proof_1 k hk a)) fun m h => Eq.ndrec (motive := fun k => k ≥ 9 → 3 * Nat.fib k + 5 < 2 * Nat.fib (k + 1)) (fun hk => have h1 := Eq.mpr (id (congrArg (fun _a => Nat.fib _a = Nat.fib (m + 8) + Nat.fib (m + 9)) (have this := Mathlib.Tactic.Ring.of_eq (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.atom_pf m) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 9))) (Mathlib.Tactic.Ring.add_pf_add_gt (Nat.rawCast 9) (Mathlib.Tactic.Ring.add_pf_add_zero (m ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 1))) (Mathlib.Tactic.Ring.add_pf_add_overlap (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.isNat_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.of_raw ℕ 9) (Mathlib.Meta.NormNum.IsNat.of_raw ℕ 1) (Eq.refl 10))) (Mathlib.Tactic.Ring.add_pf_add_zero (m ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.atom_pf m) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 8))) (Mathlib.Tactic.Ring.add_pf_add_gt (Nat.rawCast 8) (Mathlib.Tactic.Ring.add_pf_add_zero (m ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2))) (Mathlib.Tactic.Ring.add_pf_add_overlap (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.isNat_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.of_raw ℕ 8) (Mathlib.Meta.NormNum.IsNat.of_raw ℕ 2) (Eq.refl 10))) (Mathlib.Tactic.Ring.add_pf_add_zero (m ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))); this))) (Eq.mpr (id (congrArg (fun _a => _a = Nat.fib (m + 8) + Nat.fib (m + 9)) Nat.fib_add_two)) (Eq.refl (Nat.fib (m + 8) + Nat.fib (m + 8 + 1)))); have h2 := Eq.mpr (id (congrArg (fun _a => Nat.fib _a = Nat.fib (m + 7) + Nat.fib (m + 8)) (have this := Mathlib.Tactic.Ring.of_eq (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.atom_pf m) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 9))) (Mathlib.Tactic.Ring.add_pf_add_gt (Nat.rawCast 9) (Mathlib.Tactic.Ring.add_pf_add_zero (m ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.atom_pf m) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 7))) (Mathlib.Tactic.Ring.add_pf_add_gt (Nat.rawCast 7) (Mathlib.Tactic.Ring.add_pf_add_zero (m ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2))) (Mathlib.Tactic.Ring.add_pf_add_overlap (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.isNat_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.of_raw ℕ 7) (Mathlib.Meta.NormNum.IsNat.of_raw ℕ 2) (Eq.refl 9))) (Mathlib.Tactic.Ring.add_pf_add_zero (m ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))); this))) (Eq.mpr (id (congrArg (fun _a => _a = Nat.fib (m + 7) + Nat.fib (m + 8)) Nat.fib_add_two)) (Eq.refl (Nat.fib (m + 7) + Nat.fib (m + 7 + 1)))); have h3 := Eq.mpr (id (congrArg (fun _a => Nat.fib _a = Nat.fib (m + 6) + Nat.fib (m + 7)) (have this := Mathlib.Tactic.Ring.of_eq (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.atom_pf m) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 8))) (Mathlib.Tactic.Ring.add_pf_add_gt (Nat.rawCast 8) (Mathlib.Tactic.Ring.add_pf_add_zero (m ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.atom_pf m) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 6))) (Mathlib.Tactic.Ring.add_pf_add_gt (Nat.rawCast 6) (Mathlib.Tactic.Ring.add_pf_add_zero (m ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2))) (Mathlib.Tactic.Ring.add_pf_add_overlap (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.isNat_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.of_raw ℕ 6) (Mathlib.Meta.NormNum.IsNat.of_raw ℕ 2) (Eq.refl 8))) (Mathlib.Tactic.Ring.add_pf_add_zero (m ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))); this))) (Eq.mpr (id (congrArg (fun _a => _a = Nat.fib (m + 6) + Nat.fib (m + 7)) Nat.fib_add_two)) (Eq.refl (Nat.fib (m + 6) + Nat.fib (m + 6 + 1)))); have h4 := le_trans (of_decide_eq_true (id (Eq.refl true))) (Nat.fib_mono (Decidable.byContradiction fun a => f_isLacunary._proof_2 m hk a)); Decidable.byContradiction fun a => f_isLacunary._proof_3 m h1 h2 h3 h4 a) (Eq.symm h) hkhfib_R:3 * ↑(Nat.fib k) + 5 < 2 * ↑(Nat.fib (k + 1)) := cast (Eq.symm (Eq.trans (congr (congrArg LT.lt (Eq.trans (congrArg (fun x => x + ↑5) (Nat.cast_mul._simp_1 3 (Nat.fib k))) (Nat.cast_add._simp_1 (3 * Nat.fib k) 5))) (Nat.cast_mul._simp_1 2 (Nat.fib (k + 1)))) Nat.cast_lt._simp_1)) hfib_stricthpos:1 ≤ Nat.fib k := Nat.fib_pos.mpr (Decidable.byContradiction fun a => f_isLacunary._proof_4 k hk a)hpos1:1 ≤ Nat.fib (k + 1) := Nat.fib_pos.mpr (Decidable.byContradiction fun a => f_isLacunary._proof_5 k hk a)heven:Even khodd:¬Even (k + 1) := of_eq_true (Eq.trans (congrArg Not (Eq.trans f_isLacunary._simp_5 (Eq.trans (congrArg Not (eq_true heven)) not_true_eq_false))) not_false_eq_true)⊢ 3 / 2 * (↑(Nat.fib k) - 1) < ↑(Nat.fib (k + 1)) + 1 All goals completed! 🐙 k:ℕhk:k ≥ 9hfib_strict:3 * Nat.fib k + 5 < 2 * Nat.fib (k + 1) := Exists.casesOn (Exists.intro (k - 9) (Decidable.byContradiction fun a => f_isLacunary._proof_1 k hk a)) fun m h => Eq.ndrec (motive := fun k => k ≥ 9 → 3 * Nat.fib k + 5 < 2 * Nat.fib (k + 1)) (fun hk => have h1 := Eq.mpr (id (congrArg (fun _a => Nat.fib _a = Nat.fib (m + 8) + Nat.fib (m + 9)) (have this := Mathlib.Tactic.Ring.of_eq (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.atom_pf m) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 9))) (Mathlib.Tactic.Ring.add_pf_add_gt (Nat.rawCast 9) (Mathlib.Tactic.Ring.add_pf_add_zero (m ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 1))) (Mathlib.Tactic.Ring.add_pf_add_overlap (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.isNat_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.of_raw ℕ 9) (Mathlib.Meta.NormNum.IsNat.of_raw ℕ 1) (Eq.refl 10))) (Mathlib.Tactic.Ring.add_pf_add_zero (m ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.atom_pf m) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 8))) (Mathlib.Tactic.Ring.add_pf_add_gt (Nat.rawCast 8) (Mathlib.Tactic.Ring.add_pf_add_zero (m ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2))) (Mathlib.Tactic.Ring.add_pf_add_overlap (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.isNat_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.of_raw ℕ 8) (Mathlib.Meta.NormNum.IsNat.of_raw ℕ 2) (Eq.refl 10))) (Mathlib.Tactic.Ring.add_pf_add_zero (m ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))); this))) (Eq.mpr (id (congrArg (fun _a => _a = Nat.fib (m + 8) + Nat.fib (m + 9)) Nat.fib_add_two)) (Eq.refl (Nat.fib (m + 8) + Nat.fib (m + 8 + 1)))); have h2 := Eq.mpr (id (congrArg (fun _a => Nat.fib _a = Nat.fib (m + 7) + Nat.fib (m + 8)) (have this := Mathlib.Tactic.Ring.of_eq (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.atom_pf m) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 9))) (Mathlib.Tactic.Ring.add_pf_add_gt (Nat.rawCast 9) (Mathlib.Tactic.Ring.add_pf_add_zero (m ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.atom_pf m) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 7))) (Mathlib.Tactic.Ring.add_pf_add_gt (Nat.rawCast 7) (Mathlib.Tactic.Ring.add_pf_add_zero (m ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2))) (Mathlib.Tactic.Ring.add_pf_add_overlap (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.isNat_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.of_raw ℕ 7) (Mathlib.Meta.NormNum.IsNat.of_raw ℕ 2) (Eq.refl 9))) (Mathlib.Tactic.Ring.add_pf_add_zero (m ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))); this))) (Eq.mpr (id (congrArg (fun _a => _a = Nat.fib (m + 7) + Nat.fib (m + 8)) Nat.fib_add_two)) (Eq.refl (Nat.fib (m + 7) + Nat.fib (m + 7 + 1)))); have h3 := Eq.mpr (id (congrArg (fun _a => Nat.fib _a = Nat.fib (m + 6) + Nat.fib (m + 7)) (have this := Mathlib.Tactic.Ring.of_eq (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.atom_pf m) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 8))) (Mathlib.Tactic.Ring.add_pf_add_gt (Nat.rawCast 8) (Mathlib.Tactic.Ring.add_pf_add_zero (m ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.atom_pf m) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 6))) (Mathlib.Tactic.Ring.add_pf_add_gt (Nat.rawCast 6) (Mathlib.Tactic.Ring.add_pf_add_zero (m ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2))) (Mathlib.Tactic.Ring.add_pf_add_overlap (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.isNat_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.of_raw ℕ 6) (Mathlib.Meta.NormNum.IsNat.of_raw ℕ 2) (Eq.refl 8))) (Mathlib.Tactic.Ring.add_pf_add_zero (m ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))); this))) (Eq.mpr (id (congrArg (fun _a => _a = Nat.fib (m + 6) + Nat.fib (m + 7)) Nat.fib_add_two)) (Eq.refl (Nat.fib (m + 6) + Nat.fib (m + 6 + 1)))); have h4 := le_trans (of_decide_eq_true (id (Eq.refl true))) (Nat.fib_mono (Decidable.byContradiction fun a => f_isLacunary._proof_2 m hk a)); Decidable.byContradiction fun a => f_isLacunary._proof_3 m h1 h2 h3 h4 a) (Eq.symm h) hkhfib_R:3 * ↑(Nat.fib k) + 5 < 2 * ↑(Nat.fib (k + 1)) := cast (Eq.symm (Eq.trans (congr (congrArg LT.lt (Eq.trans (congrArg (fun x => x + ↑5) (Nat.cast_mul._simp_1 3 (Nat.fib k))) (Nat.cast_add._simp_1 (3 * Nat.fib k) 5))) (Nat.cast_mul._simp_1 2 (Nat.fib (k + 1)))) Nat.cast_lt._simp_1)) hfib_stricthpos:1 ≤ Nat.fib k := Nat.fib_pos.mpr (Decidable.byContradiction fun a => f_isLacunary._proof_4 k hk a)hpos1:1 ≤ Nat.fib (k + 1) := Nat.fib_pos.mpr (Decidable.byContradiction fun a => f_isLacunary._proof_5 k hk a)heven:¬Even k⊢ 3 / 2 * ↑(if Even k then Nat.fib k - 1 else Nat.fib k + 1) < ↑(if Even (k + 1) then Nat.fib (k + 1) - 1 else Nat.fib (k + 1) + 1) have hodd_plus : Even (k + 1) := ⊢ IsLacunary f All goals completed! 🐙 k:ℕhk:k ≥ 9hfib_strict:3 * Nat.fib k + 5 < 2 * Nat.fib (k + 1) := Exists.casesOn (Exists.intro (k - 9) (Decidable.byContradiction fun a => f_isLacunary._proof_1 k hk a)) fun m h => Eq.ndrec (motive := fun k => k ≥ 9 → 3 * Nat.fib k + 5 < 2 * Nat.fib (k + 1)) (fun hk => have h1 := Eq.mpr (id (congrArg (fun _a => Nat.fib _a = Nat.fib (m + 8) + Nat.fib (m + 9)) (have this := Mathlib.Tactic.Ring.of_eq (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.atom_pf m) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 9))) (Mathlib.Tactic.Ring.add_pf_add_gt (Nat.rawCast 9) (Mathlib.Tactic.Ring.add_pf_add_zero (m ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 1))) (Mathlib.Tactic.Ring.add_pf_add_overlap (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.isNat_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.of_raw ℕ 9) (Mathlib.Meta.NormNum.IsNat.of_raw ℕ 1) (Eq.refl 10))) (Mathlib.Tactic.Ring.add_pf_add_zero (m ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.atom_pf m) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 8))) (Mathlib.Tactic.Ring.add_pf_add_gt (Nat.rawCast 8) (Mathlib.Tactic.Ring.add_pf_add_zero (m ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2))) (Mathlib.Tactic.Ring.add_pf_add_overlap (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.isNat_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.of_raw ℕ 8) (Mathlib.Meta.NormNum.IsNat.of_raw ℕ 2) (Eq.refl 10))) (Mathlib.Tactic.Ring.add_pf_add_zero (m ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))); this))) (Eq.mpr (id (congrArg (fun _a => _a = Nat.fib (m + 8) + Nat.fib (m + 9)) Nat.fib_add_two)) (Eq.refl (Nat.fib (m + 8) + Nat.fib (m + 8 + 1)))); have h2 := Eq.mpr (id (congrArg (fun _a => Nat.fib _a = Nat.fib (m + 7) + Nat.fib (m + 8)) (have this := Mathlib.Tactic.Ring.of_eq (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.atom_pf m) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 9))) (Mathlib.Tactic.Ring.add_pf_add_gt (Nat.rawCast 9) (Mathlib.Tactic.Ring.add_pf_add_zero (m ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.atom_pf m) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 7))) (Mathlib.Tactic.Ring.add_pf_add_gt (Nat.rawCast 7) (Mathlib.Tactic.Ring.add_pf_add_zero (m ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2))) (Mathlib.Tactic.Ring.add_pf_add_overlap (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.isNat_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.of_raw ℕ 7) (Mathlib.Meta.NormNum.IsNat.of_raw ℕ 2) (Eq.refl 9))) (Mathlib.Tactic.Ring.add_pf_add_zero (m ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))); this))) (Eq.mpr (id (congrArg (fun _a => _a = Nat.fib (m + 7) + Nat.fib (m + 8)) Nat.fib_add_two)) (Eq.refl (Nat.fib (m + 7) + Nat.fib (m + 7 + 1)))); have h3 := Eq.mpr (id (congrArg (fun _a => Nat.fib _a = Nat.fib (m + 6) + Nat.fib (m + 7)) (have this := Mathlib.Tactic.Ring.of_eq (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.atom_pf m) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 8))) (Mathlib.Tactic.Ring.add_pf_add_gt (Nat.rawCast 8) (Mathlib.Tactic.Ring.add_pf_add_zero (m ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.atom_pf m) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 6))) (Mathlib.Tactic.Ring.add_pf_add_gt (Nat.rawCast 6) (Mathlib.Tactic.Ring.add_pf_add_zero (m ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2))) (Mathlib.Tactic.Ring.add_pf_add_overlap (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.isNat_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.of_raw ℕ 6) (Mathlib.Meta.NormNum.IsNat.of_raw ℕ 2) (Eq.refl 8))) (Mathlib.Tactic.Ring.add_pf_add_zero (m ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))); this))) (Eq.mpr (id (congrArg (fun _a => _a = Nat.fib (m + 6) + Nat.fib (m + 7)) Nat.fib_add_two)) (Eq.refl (Nat.fib (m + 6) + Nat.fib (m + 6 + 1)))); have h4 := le_trans (of_decide_eq_true (id (Eq.refl true))) (Nat.fib_mono (Decidable.byContradiction fun a => f_isLacunary._proof_2 m hk a)); Decidable.byContradiction fun a => f_isLacunary._proof_3 m h1 h2 h3 h4 a) (Eq.symm h) hkhfib_R:3 * ↑(Nat.fib k) + 5 < 2 * ↑(Nat.fib (k + 1)) := cast (Eq.symm (Eq.trans (congr (congrArg LT.lt (Eq.trans (congrArg (fun x => x + ↑5) (Nat.cast_mul._simp_1 3 (Nat.fib k))) (Nat.cast_add._simp_1 (3 * Nat.fib k) 5))) (Nat.cast_mul._simp_1 2 (Nat.fib (k + 1)))) Nat.cast_lt._simp_1)) hfib_stricthpos:1 ≤ Nat.fib k := Nat.fib_pos.mpr (Decidable.byContradiction fun a => f_isLacunary._proof_4 k hk a)hpos1:1 ≤ Nat.fib (k + 1) := Nat.fib_pos.mpr (Decidable.byContradiction fun a => f_isLacunary._proof_5 k hk a)heven:¬Even khodd_plus:Even (k + 1) := of_eq_true (Eq.trans f_isLacunary._simp_5 (Eq.trans (congrArg Not (eq_false heven)) not_false_eq_true))⊢ 3 / 2 * ↑(Nat.fib k + 1) < ↑(Nat.fib (k + 1) - 1) k:ℕhk:k ≥ 9hfib_strict:3 * Nat.fib k + 5 < 2 * Nat.fib (k + 1) := Exists.casesOn (Exists.intro (k - 9) (Decidable.byContradiction fun a => f_isLacunary._proof_1 k hk a)) fun m h => Eq.ndrec (motive := fun k => k ≥ 9 → 3 * Nat.fib k + 5 < 2 * Nat.fib (k + 1)) (fun hk => have h1 := Eq.mpr (id (congrArg (fun _a => Nat.fib _a = Nat.fib (m + 8) + Nat.fib (m + 9)) (have this := Mathlib.Tactic.Ring.of_eq (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.atom_pf m) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 9))) (Mathlib.Tactic.Ring.add_pf_add_gt (Nat.rawCast 9) (Mathlib.Tactic.Ring.add_pf_add_zero (m ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 1))) (Mathlib.Tactic.Ring.add_pf_add_overlap (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.isNat_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.of_raw ℕ 9) (Mathlib.Meta.NormNum.IsNat.of_raw ℕ 1) (Eq.refl 10))) (Mathlib.Tactic.Ring.add_pf_add_zero (m ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.atom_pf m) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 8))) (Mathlib.Tactic.Ring.add_pf_add_gt (Nat.rawCast 8) (Mathlib.Tactic.Ring.add_pf_add_zero (m ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2))) (Mathlib.Tactic.Ring.add_pf_add_overlap (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.isNat_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.of_raw ℕ 8) (Mathlib.Meta.NormNum.IsNat.of_raw ℕ 2) (Eq.refl 10))) (Mathlib.Tactic.Ring.add_pf_add_zero (m ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))); this))) (Eq.mpr (id (congrArg (fun _a => _a = Nat.fib (m + 8) + Nat.fib (m + 9)) Nat.fib_add_two)) (Eq.refl (Nat.fib (m + 8) + Nat.fib (m + 8 + 1)))); have h2 := Eq.mpr (id (congrArg (fun _a => Nat.fib _a = Nat.fib (m + 7) + Nat.fib (m + 8)) (have this := Mathlib.Tactic.Ring.of_eq (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.atom_pf m) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 9))) (Mathlib.Tactic.Ring.add_pf_add_gt (Nat.rawCast 9) (Mathlib.Tactic.Ring.add_pf_add_zero (m ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.atom_pf m) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 7))) (Mathlib.Tactic.Ring.add_pf_add_gt (Nat.rawCast 7) (Mathlib.Tactic.Ring.add_pf_add_zero (m ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2))) (Mathlib.Tactic.Ring.add_pf_add_overlap (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.isNat_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.of_raw ℕ 7) (Mathlib.Meta.NormNum.IsNat.of_raw ℕ 2) (Eq.refl 9))) (Mathlib.Tactic.Ring.add_pf_add_zero (m ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))); this))) (Eq.mpr (id (congrArg (fun _a => _a = Nat.fib (m + 7) + Nat.fib (m + 8)) Nat.fib_add_two)) (Eq.refl (Nat.fib (m + 7) + Nat.fib (m + 7 + 1)))); have h3 := Eq.mpr (id (congrArg (fun _a => Nat.fib _a = Nat.fib (m + 6) + Nat.fib (m + 7)) (have this := Mathlib.Tactic.Ring.of_eq (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.atom_pf m) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 8))) (Mathlib.Tactic.Ring.add_pf_add_gt (Nat.rawCast 8) (Mathlib.Tactic.Ring.add_pf_add_zero (m ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.atom_pf m) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 6))) (Mathlib.Tactic.Ring.add_pf_add_gt (Nat.rawCast 6) (Mathlib.Tactic.Ring.add_pf_add_zero (m ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2))) (Mathlib.Tactic.Ring.add_pf_add_overlap (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.isNat_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.of_raw ℕ 6) (Mathlib.Meta.NormNum.IsNat.of_raw ℕ 2) (Eq.refl 8))) (Mathlib.Tactic.Ring.add_pf_add_zero (m ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))); this))) (Eq.mpr (id (congrArg (fun _a => _a = Nat.fib (m + 6) + Nat.fib (m + 7)) Nat.fib_add_two)) (Eq.refl (Nat.fib (m + 6) + Nat.fib (m + 6 + 1)))); have h4 := le_trans (of_decide_eq_true (id (Eq.refl true))) (Nat.fib_mono (Decidable.byContradiction fun a => f_isLacunary._proof_2 m hk a)); Decidable.byContradiction fun a => f_isLacunary._proof_3 m h1 h2 h3 h4 a) (Eq.symm h) hkhfib_R:3 * ↑(Nat.fib k) + 5 < 2 * ↑(Nat.fib (k + 1)) := cast (Eq.symm (Eq.trans (congr (congrArg LT.lt (Eq.trans (congrArg (fun x => x + ↑5) (Nat.cast_mul._simp_1 3 (Nat.fib k))) (Nat.cast_add._simp_1 (3 * Nat.fib k) 5))) (Nat.cast_mul._simp_1 2 (Nat.fib (k + 1)))) Nat.cast_lt._simp_1)) hfib_stricthpos:1 ≤ Nat.fib k := Nat.fib_pos.mpr (Decidable.byContradiction fun a => f_isLacunary._proof_4 k hk a)hpos1:1 ≤ Nat.fib (k + 1) := Nat.fib_pos.mpr (Decidable.byContradiction fun a => f_isLacunary._proof_5 k hk a)heven:¬Even khodd_plus:Even (k + 1) := of_eq_true (Eq.trans f_isLacunary._simp_5 (Eq.trans (congrArg Not (eq_false heven)) not_false_eq_true))⊢ 3 / 2 * (↑(Nat.fib k) + 1) < ↑(Nat.fib (k + 1)) - 1 All goals completed! 🐙

The sequence f is strongly complete, and this is proved in [Gr64d].

@[category research solved, AMS 11] theorem declaration uses 'sorry'erdos_346.variants.f_isAddStronglyCompleteNatSeq : IsAddStronglyCompleteNatSeq f := ⊢ IsAddStronglyCompleteNatSeq f All goals completed! 🐙

The sequence f is not complete whenever infinitely many terms are removed from it, and this is proved in [Gr64d].

@[category research solved, AMS 11] theorem declaration uses 'sorry'erdos_346.variants.f_not_isAddComplete {B : Set ℕ} (h : B ⊆ range f) (hB : B.Infinite) : ¬ IsAddComplete (range f \ B) := B:Set ℕh:B ⊆ range fhB:B.Infinite⊢ ¬IsAddComplete (range f \ B) All goals completed! 🐙

Erdős and Graham [ErGr80] remark that it is easy to see that if A (n + 1) / A n > (1 + √5) / 2 then the second property is automatically satisfied.

@[category research solved, AMS 11] theorem declaration uses 'sorry'erdos_346.variants.gt_goldenRatio_not_IsAddComplete {A : ℕ → ℕ} (hA : ∀ n, (1 + √5) / 2 * A n < A (n + 1)) {B : Set ℕ} (h : B ⊆ range A) (hB : B.Infinite) : ¬ IsAddComplete (range A \ B) := A:ℕ → ℕhA:∀ (n : ℕ), (1 + √5) / 2 * ↑(A n) < ↑(A (n + 1))B:Set ℕh:B ⊆ range AhB:B.Infinite⊢ ¬IsAddComplete (range A \ B) All goals completed! 🐙

Erdős and Graham [ErGr80] also say that it is not hard to construct very irregular sequences satisfying the aforementioned properties.

@[category research solved, AMS 11] theorem declaration uses 'sorry'erdos_346.variants.example : ∃ A : ℕ → ℕ, IsAddStronglyCompleteNatSeq A ∧ (∀ B : Set ℕ, B ⊆ range A → B.Infinite → ¬ IsAddComplete (range A \ B)) ∧ liminf (fun n => A (n + 1) / (2 : ℝ)) atTop = 1 ∧ limsup (fun n => A (n + 1) / (A n : ENNReal)) atTop = ⊤ := ⊢ ∃ A, IsAddStronglyCompleteNatSeq A ∧ (∀ B ⊆ range A, B.Infinite → ¬IsAddComplete (range A \ B)) ∧ liminf (fun n => ↑(A (n + 1)) / 2) atTop = 1 ∧ limsup (fun n => ↑(A (n + 1)) / ↑(A n)) atTop = ⊤ All goals completed! 🐙 end Erdos346