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

Reference: erdosproblems.com/68

namespace Erdos68

Is $$\sum_{n=2}^\infty \frac{1}{n!-1}$$ irrational?

@[category research open, AMS 11] theorem declaration uses 'sorry'erdos_68 : answer(sorry) ↔ Irrational (∑' n : ℕ, 1 / ((n + 2).factorial - 1 : ℝ)) := ⊢ True ↔ Irrational (∑' (n : ℕ), 1 / (↑(n + 2).factorial - 1)) All goals completed! 🐙

$$\sum_{n=2}^\infty \frac{1}{n!-1} = \sum_{n=2}^\infty \sum_{k=1}^\infty \frac{1}{(n!)^k}$$

@[category textbook, AMS 11] theorem sum_factorial_inv_eq_geometric : let f (n k : ℕ) : ℝ := 1 / ((n + 2).factorial : ℝ) ^ (k + 1) ∑' n : ℕ, (1 : ℝ) / ((n + 2).factorial - 1) = ∑' n : ℕ, ∑' k : ℕ, f n k := ⊢ let f := fun n k => 1 / ↑(n + 2).factorial ^ (k + 1); ∑' (n : ℕ), 1 / (↑(n + 2).factorial - 1) = ∑' (n : ℕ) (k : ℕ), f n k f:ℕ → ℕ → ℝ := fun n k => 1 / ↑(n + 2).factorial ^ (k + 1)⊢ ∑' (n : ℕ), 1 / (↑(n + 2).factorial - 1) = ∑' (n : ℕ) (k : ℕ), f n k f:ℕ → ℕ → ℝ := fun n k => 1 / ↑(n + 2).factorial ^ (k + 1)⊢ ∀ (b : ℕ), 1 / (↑(b + 2).factorial - 1) = ∑' (k : ℕ), f b k f:ℕ → ℕ → ℝ := fun n k => 1 / ↑(n + 2).factorial ^ (k + 1)n:ℕ⊢ 1 / (↑(n + 2).factorial - 1) = ∑' (k : ℕ), f n k f:ℕ → ℕ → ℝ := fun n k => 1 / ↑(n + 2).factorial ^ (k + 1)n:ℕ⊢ ∑' (k : ℕ), f n k = 1 / (↑(n + 2).factorial - 1) -- The inner sum is a geometric series with ratio r = ((n + 2)!)⁻¹. f:ℕ → ℕ → ℝ := fun n k => 1 / ↑(n + 2).factorial ^ (k + 1)n:ℕr:ℝ := (↑(n + 2).factorial)⁻¹hr_def:r = (↑(n + 2).factorial)⁻¹ := rfl⊢ ∑' (k : ℕ), f n k = 1 / (↑(n + 2).factorial - 1) have hr_nonneg : 0 ≤ r := ⊢ let f := fun n k => 1 / ↑(n + 2).factorial ^ (k + 1); ∑' (n : ℕ), 1 / (↑(n + 2).factorial - 1) = ∑' (n : ℕ) (k : ℕ), f n k All goals completed! 🐙 have hr_lt_one : r < 1 := inv_lt_one_of_one_lt₀ (f:ℕ → ℕ → ℝ := fun n k => 1 / ↑(n + 2).factorial ^ (k + 1)n:ℕr:ℝ := (↑(n + 2).factorial)⁻¹hr_def:r = (↑(n + 2).factorial)⁻¹ := rflhr_nonneg:0 ≤ r := le_of_lt (inv_pos_of_pos (Nat.cast_pos'.mpr (Nat.factorial_pos (n + 2))))⊢ 1 < ↑(n + 2).factorial All goals completed! 🐙) -- Geometric series: HasSum (fun k ↦ r ^ k) ((1 - r)⁻¹) f:ℕ → ℕ → ℝ := fun n k => 1 / ↑(n + 2).factorial ^ (k + 1)n:ℕr:ℝ := (↑(n + 2).factorial)⁻¹hr_def:r = (↑(n + 2).factorial)⁻¹ := rflhr_nonneg:0 ≤ r := le_of_lt (inv_pos_of_pos (Nat.cast_pos'.mpr (Nat.factorial_pos (n + 2))))hr_lt_one:r < 1 := inv_lt_one_of_one_lt₀ (of_eq_true (Eq.trans Nat.one_lt_cast._simp_1 (Eq.trans Nat.one_lt_factorial._simp_1 (Eq.trans (lt_mul_iff_one_lt_left'._simp_2 1) (Eq.trans Order.lt_add_one_iff._simp_1 (one_le._simp_2 n))))))hgeom:HasSum (fun n => r ^ n) (1 - r)⁻¹ := hasSum_geometric_of_lt_one hr_nonneg hr_lt_one⊢ ∑' (k : ℕ), f n k = 1 / (↑(n + 2).factorial - 1) -- Multiply by r to shift the index: HasSum (fun k ↦ r * r ^ k) (r * (1 - r)⁻¹) f:ℕ → ℕ → ℝ := fun n k => 1 / ↑(n + 2).factorial ^ (k + 1)n:ℕr:ℝ := (↑(n + 2).factorial)⁻¹hr_def:r = (↑(n + 2).factorial)⁻¹ := rflhr_nonneg:0 ≤ r := le_of_lt (inv_pos_of_pos (Nat.cast_pos'.mpr (Nat.factorial_pos (n + 2))))hr_lt_one:r < 1 := inv_lt_one_of_one_lt₀ (of_eq_true (Eq.trans Nat.one_lt_cast._simp_1 (Eq.trans Nat.one_lt_factorial._simp_1 (Eq.trans (lt_mul_iff_one_lt_left'._simp_2 1) (Eq.trans Order.lt_add_one_iff._simp_1 (one_le._simp_2 n))))))hgeom:HasSum (fun n => r ^ n) (1 - r)⁻¹ := hasSum_geometric_of_lt_one hr_nonneg hr_lt_onehshift:HasSum (fun i => r * r ^ i) (r * (1 - r)⁻¹) := HasSum.mul_left r hgeom⊢ ∑' (k : ℕ), f n k = 1 / (↑(n + 2).factorial - 1) -- Each summand satisfies f n k = r * r ^ k. have hf_eq : ∀ k, f n k = r * r ^ k := fun k => f:ℕ → ℕ → ℝ := fun n k => 1 / ↑(n + 2).factorial ^ (k + 1)n:ℕr:ℝ := (↑(n + 2).factorial)⁻¹hr_def:r = (↑(n + 2).factorial)⁻¹ := rflhr_nonneg:0 ≤ r := le_of_lt (inv_pos_of_pos (Nat.cast_pos'.mpr (Nat.factorial_pos (n + 2))))hr_lt_one:r < 1 := inv_lt_one_of_one_lt₀ (of_eq_true (Eq.trans Nat.one_lt_cast._simp_1 (Eq.trans Nat.one_lt_factorial._simp_1 (Eq.trans (lt_mul_iff_one_lt_left'._simp_2 1) (Eq.trans Order.lt_add_one_iff._simp_1 (one_le._simp_2 n))))))hgeom:HasSum (fun n => r ^ n) (1 - r)⁻¹ := hasSum_geometric_of_lt_one hr_nonneg hr_lt_onehshift:HasSum (fun i => r * r ^ i) (r * (1 - r)⁻¹) := HasSum.mul_left r hgeomk:ℕ⊢ f n k = r * r ^ k f:ℕ → ℕ → ℝ := fun n k => 1 / ↑(n + 2).factorial ^ (k + 1)n:ℕr:ℝ := (↑(n + 2).factorial)⁻¹hr_def:r = (↑(n + 2).factorial)⁻¹ := rflhr_nonneg:0 ≤ r := le_of_lt (inv_pos_of_pos (Nat.cast_pos'.mpr (Nat.factorial_pos (n + 2))))hr_lt_one:r < 1 := inv_lt_one_of_one_lt₀ (of_eq_true (Eq.trans Nat.one_lt_cast._simp_1 (Eq.trans Nat.one_lt_factorial._simp_1 (Eq.trans (lt_mul_iff_one_lt_left'._simp_2 1) (Eq.trans Order.lt_add_one_iff._simp_1 (one_le._simp_2 n))))))hgeom:HasSum (fun n => r ^ n) (1 - r)⁻¹ := hasSum_geometric_of_lt_one hr_nonneg hr_lt_onehshift:HasSum (fun i => r * r ^ i) (r * (1 - r)⁻¹) := HasSum.mul_left r hgeomk:ℕ⊢ 1 / ↑(n + 2).factorial ^ (k + 1) = (↑(n + 2).factorial)⁻¹ * (↑(n + 2).factorial)⁻¹ ^ k; All goals completed! 🐙 -- Evaluate ∑' k, f n k = r * (1 - r)⁻¹ = 1 / ((n + 2)! - 1). exact ((hshift.congr_fun hf_eq).tsum_eq.trans (f:ℕ → ℕ → ℝ := fun n k => 1 / ↑(n + 2).factorial ^ (k + 1)n:ℕr:ℝ := (↑(n + 2).factorial)⁻¹hr_def:r = (↑(n + 2).factorial)⁻¹ := rflhr_nonneg:0 ≤ r := le_of_lt (inv_pos_of_pos (Nat.cast_pos'.mpr (Nat.factorial_pos (n + 2))))hr_lt_one:r < 1 := inv_lt_one_of_one_lt₀ (of_eq_true (Eq.trans Nat.one_lt_cast._simp_1 (Eq.trans Nat.one_lt_factorial._simp_1 (Eq.trans (lt_mul_iff_one_lt_left'._simp_2 1) (Eq.trans Order.lt_add_one_iff._simp_1 (one_le._simp_2 n))))))hgeom:HasSum (fun n => r ^ n) (1 - r)⁻¹ := hasSum_geometric_of_lt_one hr_nonneg hr_lt_onehshift:HasSum (fun i => r * r ^ i) (r * (1 - r)⁻¹) := HasSum.mul_left r hgeomhf_eq:∀ (k : ℕ), f n k = r * r ^ k := fun k => Eq.mpr (id (congrArg (Eq (1 / ↑(n + 2).factorial ^ (k + 1))) (congr (congrArg HMul.hMul hr_def) (congrArg (fun x => x ^ k) hr_def)))) (Mathlib.Tactic.Ring.of_eq (Mathlib.Tactic.Ring.div_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one)) (Mathlib.Tactic.Ring.pow_congr (Mathlib.Tactic.Ring.atom_pf ↑(n + 2).factorial) (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.atom_pf k) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 1))) (Mathlib.Tactic.Ring.add_pf_add_gt (Nat.rawCast 1) (Mathlib.Tactic.Ring.add_pf_add_zero (k ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.pow_add (Mathlib.Tactic.Ring.pow_one_cast (↑(n + 2).factorial ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.pow_add (Mathlib.Tactic.Ring.single_pow (Mathlib.Tactic.Ring.mul_pow (Mathlib.Tactic.Ring.mul_pf_right k (Nat.rawCast 1) (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1))) (Mathlib.Tactic.Ring.one_pow (k ^ Nat.rawCast 1 * Nat.rawCast 1)))) (Mathlib.Tactic.Ring.pow_zero (↑(n + 2).factorial ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_left (↑(n + 2).factorial) (k ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1))) (Mathlib.Tactic.Ring.mul_zero (↑(n + 2).factorial ^ (k ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero (↑(n + 2).factorial ^ (k ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))) (Mathlib.Tactic.Ring.zero_mul (Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero (↑(n + 2).factorial ^ (k ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_left (↑(n + 2).factorial) (Nat.rawCast 1) (Mathlib.Tactic.Ring.mul_pf_right (↑(n + 2).factorial) (k ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1)))) (Mathlib.Tactic.Ring.mul_zero (↑(n + 2).factorial ^ Nat.rawCast 1 * Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero (↑(n + 2).factorial ^ Nat.rawCast 1 * (↑(n + 2).factorial ^ (k ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1) + 0))) (Mathlib.Tactic.Ring.zero_mul (↑(n + 2).factorial ^ (k ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero (↑(n + 2).factorial ^ Nat.rawCast 1 * (↑(n + 2).factorial ^ (k ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1) + 0))))) (Mathlib.Tactic.Ring.div_pf (Mathlib.Tactic.Ring.inv_single (Mathlib.Tactic.Ring.inv_mul (Eq.refl (↑(n + 2).factorial)⁻¹) (Mathlib.Tactic.Ring.inv_mul (Eq.refl (↑(n + 2).factorial)⁻¹) (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.IsNNRat.to_isNat (Mathlib.Meta.NormNum.isNNRat_inv_pos (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1))))) (Mathlib.Tactic.Ring.mul_pf_right (↑(n + 2).factorial)⁻¹ (k ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1)))) (Mathlib.Tactic.Ring.mul_pf_right (↑(n + 2).factorial)⁻¹ (Nat.rawCast 1) (Mathlib.Tactic.Ring.mul_pf_left (↑(n + 2).factorial)⁻¹ (k ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1)))))) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_right (↑(n + 2).factorial)⁻¹ (Nat.rawCast 1) (Mathlib.Tactic.Ring.mul_pf_right (↑(n + 2).factorial)⁻¹ (k ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1)))) (Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero ((↑(n + 2).factorial)⁻¹ ^ Nat.rawCast 1 * ((↑(n + 2).factorial)⁻¹ ^ (k ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1) + 0))) (Mathlib.Tactic.Ring.zero_mul ((↑(n + 2).factorial)⁻¹ ^ Nat.rawCast 1 * ((↑(n + 2).factorial)⁻¹ ^ (k ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1) + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero ((↑(n + 2).factorial)⁻¹ ^ Nat.rawCast 1 * ((↑(n + 2).factorial)⁻¹ ^ (k ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1) + 0))))) (Mathlib.Tactic.Ring.mul_congr (Mathlib.Tactic.Ring.inv_congr (Mathlib.Tactic.Ring.atom_pf ↑(n + 2).factorial) (Mathlib.Tactic.Ring.inv_single (Mathlib.Tactic.Ring.inv_mul (Eq.refl (↑(n + 2).factorial)⁻¹) (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.IsNNRat.to_isNat (Mathlib.Meta.NormNum.isNNRat_inv_pos (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1))))) (Mathlib.Tactic.Ring.mul_pf_right (↑(n + 2).factorial)⁻¹ (Nat.rawCast 1) (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1)))))) (Mathlib.Tactic.Ring.pow_congr (Mathlib.Tactic.Ring.inv_congr (Mathlib.Tactic.Ring.atom_pf ↑(n + 2).factorial) (Mathlib.Tactic.Ring.inv_single (Mathlib.Tactic.Ring.inv_mul (Eq.refl (↑(n + 2).factorial)⁻¹) (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.IsNNRat.to_isNat (Mathlib.Meta.NormNum.isNNRat_inv_pos (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1))))) (Mathlib.Tactic.Ring.mul_pf_right (↑(n + 2).factorial)⁻¹ (Nat.rawCast 1) (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1)))))) (Mathlib.Tactic.Ring.atom_pf k) (Mathlib.Tactic.Ring.pow_add (Mathlib.Tactic.Ring.single_pow (Mathlib.Tactic.Ring.mul_pow (Mathlib.Tactic.Ring.mul_pf_right k (Nat.rawCast 1) (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1))) (Mathlib.Tactic.Ring.one_pow (k ^ Nat.rawCast 1 * Nat.rawCast 1)))) (Mathlib.Tactic.Ring.pow_zero ((↑(n + 2).factorial)⁻¹ ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_left (↑(n + 2).factorial)⁻¹ (k ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1))) (Mathlib.Tactic.Ring.mul_zero ((↑(n + 2).factorial)⁻¹ ^ (k ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero ((↑(n + 2).factorial)⁻¹ ^ (k ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))) (Mathlib.Tactic.Ring.zero_mul (Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero ((↑(n + 2).factorial)⁻¹ ^ (k ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))))) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_left (↑(n + 2).factorial)⁻¹ (Nat.rawCast 1) (Mathlib.Tactic.Ring.mul_pf_right (↑(n + 2).factorial)⁻¹ (k ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1)))) (Mathlib.Tactic.Ring.mul_zero ((↑(n + 2).factorial)⁻¹ ^ Nat.rawCast 1 * Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero ((↑(n + 2).factorial)⁻¹ ^ Nat.rawCast 1 * ((↑(n + 2).factorial)⁻¹ ^ (k ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1) + 0))) (Mathlib.Tactic.Ring.zero_mul ((↑(n + 2).factorial)⁻¹ ^ (k ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero ((↑(n + 2).factorial)⁻¹ ^ Nat.rawCast 1 * ((↑(n + 2).factorial)⁻¹ ^ (k ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1) + 0)))))⊢ r * (1 - r)⁻¹ = 1 / (↑(n + 2).factorial - 1) f:ℕ → ℕ → ℝ := fun n k => 1 / ↑(n + 2).factorial ^ (k + 1)n:ℕr:ℝ := (↑(n + 2).factorial)⁻¹hr_def:r = (↑(n + 2).factorial)⁻¹ := rflhr_nonneg:0 ≤ r := le_of_lt (inv_pos_of_pos (Nat.cast_pos'.mpr (Nat.factorial_pos (n + 2))))hr_lt_one:r < 1 := inv_lt_one_of_one_lt₀ (of_eq_true (Eq.trans Nat.one_lt_cast._simp_1 (Eq.trans Nat.one_lt_factorial._simp_1 (Eq.trans (lt_mul_iff_one_lt_left'._simp_2 1) (Eq.trans Order.lt_add_one_iff._simp_1 (one_le._simp_2 n))))))hgeom:HasSum (fun n => r ^ n) (1 - r)⁻¹ := hasSum_geometric_of_lt_one hr_nonneg hr_lt_onehshift:HasSum (fun i => r * r ^ i) (r * (1 - r)⁻¹) := HasSum.mul_left r hgeomhf_eq:∀ (k : ℕ), f n k = r * r ^ k := fun k => Eq.mpr (id (congrArg (Eq (1 / ↑(n + 2).factorial ^ (k + 1))) (congr (congrArg HMul.hMul hr_def) (congrArg (fun x => x ^ k) hr_def)))) (Mathlib.Tactic.Ring.of_eq (Mathlib.Tactic.Ring.div_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one)) (Mathlib.Tactic.Ring.pow_congr (Mathlib.Tactic.Ring.atom_pf ↑(n + 2).factorial) (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.atom_pf k) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 1))) (Mathlib.Tactic.Ring.add_pf_add_gt (Nat.rawCast 1) (Mathlib.Tactic.Ring.add_pf_add_zero (k ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.pow_add (Mathlib.Tactic.Ring.pow_one_cast (↑(n + 2).factorial ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.pow_add (Mathlib.Tactic.Ring.single_pow (Mathlib.Tactic.Ring.mul_pow (Mathlib.Tactic.Ring.mul_pf_right k (Nat.rawCast 1) (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1))) (Mathlib.Tactic.Ring.one_pow (k ^ Nat.rawCast 1 * Nat.rawCast 1)))) (Mathlib.Tactic.Ring.pow_zero (↑(n + 2).factorial ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_left (↑(n + 2).factorial) (k ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1))) (Mathlib.Tactic.Ring.mul_zero (↑(n + 2).factorial ^ (k ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero (↑(n + 2).factorial ^ (k ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))) (Mathlib.Tactic.Ring.zero_mul (Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero (↑(n + 2).factorial ^ (k ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_left (↑(n + 2).factorial) (Nat.rawCast 1) (Mathlib.Tactic.Ring.mul_pf_right (↑(n + 2).factorial) (k ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1)))) (Mathlib.Tactic.Ring.mul_zero (↑(n + 2).factorial ^ Nat.rawCast 1 * Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero (↑(n + 2).factorial ^ Nat.rawCast 1 * (↑(n + 2).factorial ^ (k ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1) + 0))) (Mathlib.Tactic.Ring.zero_mul (↑(n + 2).factorial ^ (k ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero (↑(n + 2).factorial ^ Nat.rawCast 1 * (↑(n + 2).factorial ^ (k ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1) + 0))))) (Mathlib.Tactic.Ring.div_pf (Mathlib.Tactic.Ring.inv_single (Mathlib.Tactic.Ring.inv_mul (Eq.refl (↑(n + 2).factorial)⁻¹) (Mathlib.Tactic.Ring.inv_mul (Eq.refl (↑(n + 2).factorial)⁻¹) (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.IsNNRat.to_isNat (Mathlib.Meta.NormNum.isNNRat_inv_pos (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1))))) (Mathlib.Tactic.Ring.mul_pf_right (↑(n + 2).factorial)⁻¹ (k ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1)))) (Mathlib.Tactic.Ring.mul_pf_right (↑(n + 2).factorial)⁻¹ (Nat.rawCast 1) (Mathlib.Tactic.Ring.mul_pf_left (↑(n + 2).factorial)⁻¹ (k ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1)))))) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_right (↑(n + 2).factorial)⁻¹ (Nat.rawCast 1) (Mathlib.Tactic.Ring.mul_pf_right (↑(n + 2).factorial)⁻¹ (k ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1)))) (Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero ((↑(n + 2).factorial)⁻¹ ^ Nat.rawCast 1 * ((↑(n + 2).factorial)⁻¹ ^ (k ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1) + 0))) (Mathlib.Tactic.Ring.zero_mul ((↑(n + 2).factorial)⁻¹ ^ Nat.rawCast 1 * ((↑(n + 2).factorial)⁻¹ ^ (k ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1) + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero ((↑(n + 2).factorial)⁻¹ ^ Nat.rawCast 1 * ((↑(n + 2).factorial)⁻¹ ^ (k ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1) + 0))))) (Mathlib.Tactic.Ring.mul_congr (Mathlib.Tactic.Ring.inv_congr (Mathlib.Tactic.Ring.atom_pf ↑(n + 2).factorial) (Mathlib.Tactic.Ring.inv_single (Mathlib.Tactic.Ring.inv_mul (Eq.refl (↑(n + 2).factorial)⁻¹) (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.IsNNRat.to_isNat (Mathlib.Meta.NormNum.isNNRat_inv_pos (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1))))) (Mathlib.Tactic.Ring.mul_pf_right (↑(n + 2).factorial)⁻¹ (Nat.rawCast 1) (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1)))))) (Mathlib.Tactic.Ring.pow_congr (Mathlib.Tactic.Ring.inv_congr (Mathlib.Tactic.Ring.atom_pf ↑(n + 2).factorial) (Mathlib.Tactic.Ring.inv_single (Mathlib.Tactic.Ring.inv_mul (Eq.refl (↑(n + 2).factorial)⁻¹) (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.IsNNRat.to_isNat (Mathlib.Meta.NormNum.isNNRat_inv_pos (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1))))) (Mathlib.Tactic.Ring.mul_pf_right (↑(n + 2).factorial)⁻¹ (Nat.rawCast 1) (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1)))))) (Mathlib.Tactic.Ring.atom_pf k) (Mathlib.Tactic.Ring.pow_add (Mathlib.Tactic.Ring.single_pow (Mathlib.Tactic.Ring.mul_pow (Mathlib.Tactic.Ring.mul_pf_right k (Nat.rawCast 1) (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1))) (Mathlib.Tactic.Ring.one_pow (k ^ Nat.rawCast 1 * Nat.rawCast 1)))) (Mathlib.Tactic.Ring.pow_zero ((↑(n + 2).factorial)⁻¹ ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_left (↑(n + 2).factorial)⁻¹ (k ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1))) (Mathlib.Tactic.Ring.mul_zero ((↑(n + 2).factorial)⁻¹ ^ (k ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero ((↑(n + 2).factorial)⁻¹ ^ (k ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))) (Mathlib.Tactic.Ring.zero_mul (Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero ((↑(n + 2).factorial)⁻¹ ^ (k ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))))) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_left (↑(n + 2).factorial)⁻¹ (Nat.rawCast 1) (Mathlib.Tactic.Ring.mul_pf_right (↑(n + 2).factorial)⁻¹ (k ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1)))) (Mathlib.Tactic.Ring.mul_zero ((↑(n + 2).factorial)⁻¹ ^ Nat.rawCast 1 * Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero ((↑(n + 2).factorial)⁻¹ ^ Nat.rawCast 1 * ((↑(n + 2).factorial)⁻¹ ^ (k ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1) + 0))) (Mathlib.Tactic.Ring.zero_mul ((↑(n + 2).factorial)⁻¹ ^ (k ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero ((↑(n + 2).factorial)⁻¹ ^ Nat.rawCast 1 * ((↑(n + 2).factorial)⁻¹ ^ (k ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1) + 0)))))⊢ (↑(n + 2).factorial)⁻¹ * (1 - (↑(n + 2).factorial)⁻¹)⁻¹ = 1 / (↑(n + 2).factorial - 1); All goals completed! 🐙)) end Erdos68