FormalConjectures.OEIS.«34693»

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

Smallest number k such that kn + 1 is prime

Smallest number $k$ such that $kn + 1$ is prime.

Reference: A34693


namespace OeisA34693


open Filter

Smallest number $k$ such that $kn + 1$ is prime.

noncomputable def a (n : ℕ) : ℕ := Nat.nth (fun k ↦ (k * n + 1).Prime) 0


@[category test, AMS 11]
theorem a_0 : a 0 = 0 := by⊢ a 0 = 0
  simpa [a] using Nat.nth_eq_zero.2 <| .inr ⟨by⊢ {k | Nat.Prime 1}.Finite convert Set.finite_emptyh.e'_2⊢ {k | Nat.Prime 1} = ∅; aesopAll goals completed! 🐙, by⊢ ⋯.toFinset.card ≤ 0 aesopAll goals completed! 🐙⟩


@[category test, AMS 11]
theorem a_1 : a 1 = 1 := by⊢ a 1 = 1
  conv_rhs => rw [← Nat.nth_count (p := fun k ↦ (k + 1).Prime) (n := 1) (by⊢ (fun k => Nat.Prime (k + 1)) 1 norm_numAll goals completed! 🐙)]
  aesop (add simp [a])All goals completed! 🐙


@[category test, AMS 11]
theorem a_2 : a 2 = 1 := by⊢ a 2 = 1
  conv_rhs => rw [← Nat.nth_count (p := fun k ↦ (k * 2 + 1).Prime) (n := 1) (by⊢ (fun k => Nat.Prime (k * 2 + 1)) 1 norm_numAll goals completed! 🐙)]
  aesop (add simp [a])All goals completed! 🐙


@[category test, AMS 11]
theorem a_3 : a 3 = 2 := by⊢ a 3 = 2
  conv_rhs => rw [← Nat.nth_count (p := fun k ↦ (k * 3 + 1).Prime) (n := 2) (by⊢ (fun k => Nat.Prime (k * 3 + 1)) 2 norm_numAll goals completed! 🐙)]
  aesop (add simp [a])All goals completed! 🐙


@[category test, AMS 11]
theorem a_7 : a 7 = 4 := by⊢ a 7 = 4
  conv_rhs => rw [← Nat.nth_count (p := fun k ↦ (k * 7 + 1).Prime) (n := 4) (by⊢ (fun k => Nat.Prime (k * 7 + 1)) 4 norm_numAll goals completed! 🐙)]
  aesop (add simp [a])All goals completed! 🐙

Conjecture: for every $n > 1$ there exists a number $k < n$ such that $nk + 1$ is a prime.

@[category research open, AMS 11]
theorem declaration uses 'sorry'exists_k {n : ℕ} (hn : 1 < n) : ∃ k < n, (n * k + 1).Prime := byn:ℕhn:1 < n⊢ ∃ k < n, Nat.Prime (n * k + 1)
  sorryAll goals completed! 🐙

A stronger conjecture: for every n there exists a number $k < 1 + n^{0.75}$ such that $nk + 1$ is a prime.

@[category research open, AMS 11]
theorem declaration uses 'sorry'exists_k_stronger {n : ℕ} (hn : 0 < n) : ∃ k : ℕ,
    k < 1 + (Real.nthRoot 4 n) ^ 3 ∧ (n * k + 1).Prime := byn:ℕhn:0 < n⊢ ∃ k, ↑k < 1 + Real.nthRoot 4 ↑n ^ 3 ∧ Nat.Prime (n * k + 1)
  sorryAll goals completed! 🐙

The expression $1 + n^{0.74}$ does not work as an upper bound.

@[category research solved, AMS 11]
theorem exists_k_best_possible : ∃ n > (0 : ℕ), ∀ (k : ℕ),
    k < 1 + (Real.nthRoot 100 n) ^ 74 → ¬(n * k + 1).Prime := by⊢ ∃ n > 0, ∀ (k : ℕ), ↑k < 1 + Real.nthRoot 100 ↑n ^ 74 → ¬Nat.Prime (n * k + 1)
  refine ⟨19, by⊢ 19 > 0 norm_numAll goals completed! 🐙, ?_⟩
  have hy : Real.nthRoot 100 ((19 : ℕ) : ℝ) = (19 : ℝ) ^ (((100 : ℕ) : ℝ))⁻¹ := by⊢ ∃ n > 0, ∀ (k : ℕ), ↑k < 1 + Real.nthRoot 100 ↑n ^ 74 → ¬Nat.Prime (n * k + 1)
    simp only [Real.nthRoot]⊢ (if Even 100 then ↑19 ^ (↑100)⁻¹ else ↑(SignType.sign ↑19) ^ 100 * |↑19| ^ (↑100)⁻¹) = 19 ^ (↑100)⁻¹
    rw [if_pos (by decide : Even 100)]⊢ ↑19 ^ (↑100)⁻¹ = 19 ^ (↑100)⁻¹
    norm_numAll goals completed! 🐙
  have h100 : (Real.nthRoot 100 ((19 : ℕ) : ℝ)) ^ (100 : ℕ) = 19 := by⊢ ∃ n > 0, ∀ (k : ℕ), ↑k < 1 + Real.nthRoot 100 ↑n ^ 74 → ¬Nat.Prime (n * k + 1)
    rw [hy]hy:Real.nthRoot 100 ↑19 = 19 ^ (↑100)⁻¹ := 
  id
    (Eq.mpr (id (congrArg (fun _a => _a = 19 ^ (↑100)⁻¹) (if_pos (of_decide_eq_true (id (Eq.refl true))))))
      (of_eq_true
        (Eq.trans
          (Eq.trans
            (congr
              (congrArg Eq
                (Eq.trans
                  (congr
                    (congrArg HPow.hPow
                      (Mathlib.Meta.NormNum.IsNat.to_eq
                        (Mathlib.Meta.NormNum.isNat_natCast 19 19 (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 19)))
                        (Eq.refl 19)))
                    (Mathlib.Meta.NormNum.IsNNRat.to_eq
                      (Mathlib.Meta.NormNum.isNNRat_inv_pos
                        (Mathlib.Meta.NormNum.IsNat.to_isNNRat
                          (Mathlib.Meta.NormNum.isNat_natCast 100 100
                            (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 100)))))
                      Nat.cast_one (Eq.refl 100)))
                  (congrArg (HPow.hPow 19)
                    (Mathlib.Meta.NormNum.IsNNRat.to_eq
                      (Mathlib.Meta.NormNum.isNNRat_div
                        (Mathlib.Meta.NormNum.isNNRat_mul (Eq.refl HMul.hMul)
                          (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one))
                          (Mathlib.Meta.NormNum.isNNRat_inv_pos
                            (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 100))))
                          (Eq.refl (Nat.mul 1 1)) (Eq.refl 100)))
                      Nat.cast_one (Eq.refl 100)))))
              (Eq.trans
                (congrArg (HPow.hPow 19)
                  (Mathlib.Meta.NormNum.IsNNRat.to_eq
                    (Mathlib.Meta.NormNum.isNNRat_inv_pos
                      (Mathlib.Meta.NormNum.IsNat.to_isNNRat
                        (Mathlib.Meta.NormNum.isNat_natCast 100 100 (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 100)))))
                    Nat.cast_one (Eq.refl 100)))
                (congrArg (HPow.hPow 19)
                  (Mathlib.Meta.NormNum.IsNNRat.to_eq
                    (Mathlib.Meta.NormNum.isNNRat_div
                      (Mathlib.Meta.NormNum.isNNRat_mul (Eq.refl HMul.hMul)
                        (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one))
                        (Mathlib.Meta.NormNum.isNNRat_inv_pos
                          (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 100))))
                        (Eq.refl (Nat.mul 1 1)) (Eq.refl 100)))
                    Nat.cast_one (Eq.refl 100)))))
            (eq_self (19 ^ (1 / 100))))
          (eq_true True.intro))))⊢ (19 ^ (↑100)⁻¹) ^ 100 = 19; exact Real.rpow_inv_natCast_pow (byhy:Real.nthRoot 100 ↑19 = 19 ^ (↑100)⁻¹ := 
  id
    (Eq.mpr (id (congrArg (fun _a => _a = 19 ^ (↑100)⁻¹) (if_pos (of_decide_eq_true (id (Eq.refl true))))))
      (of_eq_true
        (Eq.trans
          (Eq.trans
            (congr
              (congrArg Eq
                (Eq.trans
                  (congr
                    (congrArg HPow.hPow
                      (Mathlib.Meta.NormNum.IsNat.to_eq
                        (Mathlib.Meta.NormNum.isNat_natCast 19 19 (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 19)))
                        (Eq.refl 19)))
                    (Mathlib.Meta.NormNum.IsNNRat.to_eq
                      (Mathlib.Meta.NormNum.isNNRat_inv_pos
                        (Mathlib.Meta.NormNum.IsNat.to_isNNRat
                          (Mathlib.Meta.NormNum.isNat_natCast 100 100
                            (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 100)))))
                      Nat.cast_one (Eq.refl 100)))
                  (congrArg (HPow.hPow 19)
                    (Mathlib.Meta.NormNum.IsNNRat.to_eq
                      (Mathlib.Meta.NormNum.isNNRat_div
                        (Mathlib.Meta.NormNum.isNNRat_mul (Eq.refl HMul.hMul)
                          (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one))
                          (Mathlib.Meta.NormNum.isNNRat_inv_pos
                            (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 100))))
                          (Eq.refl (Nat.mul 1 1)) (Eq.refl 100)))
                      Nat.cast_one (Eq.refl 100)))))
              (Eq.trans
                (congrArg (HPow.hPow 19)
                  (Mathlib.Meta.NormNum.IsNNRat.to_eq
                    (Mathlib.Meta.NormNum.isNNRat_inv_pos
                      (Mathlib.Meta.NormNum.IsNat.to_isNNRat
                        (Mathlib.Meta.NormNum.isNat_natCast 100 100 (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 100)))))
                    Nat.cast_one (Eq.refl 100)))
                (congrArg (HPow.hPow 19)
                  (Mathlib.Meta.NormNum.IsNNRat.to_eq
                    (Mathlib.Meta.NormNum.isNNRat_div
                      (Mathlib.Meta.NormNum.isNNRat_mul (Eq.refl HMul.hMul)
                        (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one))
                        (Mathlib.Meta.NormNum.isNNRat_inv_pos
                          (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 100))))
                        (Eq.refl (Nat.mul 1 1)) (Eq.refl 100)))
                    Nat.cast_one (Eq.refl 100)))))
            (eq_self (19 ^ (1 / 100))))
          (eq_true True.intro))))⊢ 0 ≤ 19 norm_numAll goals completed! 🐙) (byhy:Real.nthRoot 100 ↑19 = 19 ^ (↑100)⁻¹ := 
  id
    (Eq.mpr (id (congrArg (fun _a => _a = 19 ^ (↑100)⁻¹) (if_pos (of_decide_eq_true (id (Eq.refl true))))))
      (of_eq_true
        (Eq.trans
          (Eq.trans
            (congr
              (congrArg Eq
                (Eq.trans
                  (congr
                    (congrArg HPow.hPow
                      (Mathlib.Meta.NormNum.IsNat.to_eq
                        (Mathlib.Meta.NormNum.isNat_natCast 19 19 (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 19)))
                        (Eq.refl 19)))
                    (Mathlib.Meta.NormNum.IsNNRat.to_eq
                      (Mathlib.Meta.NormNum.isNNRat_inv_pos
                        (Mathlib.Meta.NormNum.IsNat.to_isNNRat
                          (Mathlib.Meta.NormNum.isNat_natCast 100 100
                            (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 100)))))
                      Nat.cast_one (Eq.refl 100)))
                  (congrArg (HPow.hPow 19)
                    (Mathlib.Meta.NormNum.IsNNRat.to_eq
                      (Mathlib.Meta.NormNum.isNNRat_div
                        (Mathlib.Meta.NormNum.isNNRat_mul (Eq.refl HMul.hMul)
                          (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one))
                          (Mathlib.Meta.NormNum.isNNRat_inv_pos
                            (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 100))))
                          (Eq.refl (Nat.mul 1 1)) (Eq.refl 100)))
                      Nat.cast_one (Eq.refl 100)))))
              (Eq.trans
                (congrArg (HPow.hPow 19)
                  (Mathlib.Meta.NormNum.IsNNRat.to_eq
                    (Mathlib.Meta.NormNum.isNNRat_inv_pos
                      (Mathlib.Meta.NormNum.IsNat.to_isNNRat
                        (Mathlib.Meta.NormNum.isNat_natCast 100 100 (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 100)))))
                    Nat.cast_one (Eq.refl 100)))
                (congrArg (HPow.hPow 19)
                  (Mathlib.Meta.NormNum.IsNNRat.to_eq
                    (Mathlib.Meta.NormNum.isNNRat_div
                      (Mathlib.Meta.NormNum.isNNRat_mul (Eq.refl HMul.hMul)
                        (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one))
                        (Mathlib.Meta.NormNum.isNNRat_inv_pos
                          (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 100))))
                        (Eq.refl (Nat.mul 1 1)) (Eq.refl 100)))
                    Nat.cast_one (Eq.refl 100)))))
            (eq_self (19 ^ (1 / 100))))
          (eq_true True.intro))))⊢ 100 ≠ 0 norm_numAll goals completed! 🐙)
  have hb : (Real.nthRoot 100 ((19 : ℕ) : ℝ)) ^ 74 ≤ 9 := by⊢ ∃ n > 0, ∀ (k : ℕ), ↑k < 1 + Real.nthRoot 100 ↑n ^ 74 → ¬Nat.Prime (n * k + 1)
    apply le_of_pow_le_pow_left₀ (n := 100) (byhy:Real.nthRoot 100 ↑19 = 19 ^ (↑100)⁻¹ := 
  id
    (Eq.mpr (id (congrArg (fun _a => _a = 19 ^ (↑100)⁻¹) (if_pos (of_decide_eq_true (id (Eq.refl true))))))
      (of_eq_true
        (Eq.trans
          (Eq.trans
            (congr
              (congrArg Eq
                (Eq.trans
                  (congr
                    (congrArg HPow.hPow
                      (Mathlib.Meta.NormNum.IsNat.to_eq
                        (Mathlib.Meta.NormNum.isNat_natCast 19 19 (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 19)))
                        (Eq.refl 19)))
                    (Mathlib.Meta.NormNum.IsNNRat.to_eq
                      (Mathlib.Meta.NormNum.isNNRat_inv_pos
                        (Mathlib.Meta.NormNum.IsNat.to_isNNRat
                          (Mathlib.Meta.NormNum.isNat_natCast 100 100
                            (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 100)))))
                      Nat.cast_one (Eq.refl 100)))
                  (congrArg (HPow.hPow 19)
                    (Mathlib.Meta.NormNum.IsNNRat.to_eq
                      (Mathlib.Meta.NormNum.isNNRat_div
                        (Mathlib.Meta.NormNum.isNNRat_mul (Eq.refl HMul.hMul)
                          (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one))
                          (Mathlib.Meta.NormNum.isNNRat_inv_pos
                            (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 100))))
                          (Eq.refl (Nat.mul 1 1)) (Eq.refl 100)))
                      Nat.cast_one (Eq.refl 100)))))
              (Eq.trans
                (congrArg (HPow.hPow 19)
                  (Mathlib.Meta.NormNum.IsNNRat.to_eq
                    (Mathlib.Meta.NormNum.isNNRat_inv_pos
                      (Mathlib.Meta.NormNum.IsNat.to_isNNRat
                        (Mathlib.Meta.NormNum.isNat_natCast 100 100 (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 100)))))
                    Nat.cast_one (Eq.refl 100)))
                (congrArg (HPow.hPow 19)
                  (Mathlib.Meta.NormNum.IsNNRat.to_eq
                    (Mathlib.Meta.NormNum.isNNRat_div
                      (Mathlib.Meta.NormNum.isNNRat_mul (Eq.refl HMul.hMul)
                        (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one))
                        (Mathlib.Meta.NormNum.isNNRat_inv_pos
                          (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 100))))
                        (Eq.refl (Nat.mul 1 1)) (Eq.refl 100)))
                    Nat.cast_one (Eq.refl 100)))))
            (eq_self (19 ^ (1 / 100))))
          (eq_true True.intro))))h100:Real.nthRoot 100 ↑19 ^ 100 = 19 := 
  Eq.mpr (id (congrArg (fun _a => _a ^ 100 = 19) hy))
    (Real.rpow_inv_natCast_pow
      (Mathlib.Meta.NormNum.isNat_le_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)
        (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 19)) (Eq.refl true))
      (Mathlib.Meta.NormNum.isNat_eq_false (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 100))
        (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 0)) (Eq.refl false)))⊢ 100 ≠ 0 norm_numAll goals completed! 🐙) (byhy:Real.nthRoot 100 ↑19 = 19 ^ (↑100)⁻¹ := 
  id
    (Eq.mpr (id (congrArg (fun _a => _a = 19 ^ (↑100)⁻¹) (if_pos (of_decide_eq_true (id (Eq.refl true))))))
      (of_eq_true
        (Eq.trans
          (Eq.trans
            (congr
              (congrArg Eq
                (Eq.trans
                  (congr
                    (congrArg HPow.hPow
                      (Mathlib.Meta.NormNum.IsNat.to_eq
                        (Mathlib.Meta.NormNum.isNat_natCast 19 19 (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 19)))
                        (Eq.refl 19)))
                    (Mathlib.Meta.NormNum.IsNNRat.to_eq
                      (Mathlib.Meta.NormNum.isNNRat_inv_pos
                        (Mathlib.Meta.NormNum.IsNat.to_isNNRat
                          (Mathlib.Meta.NormNum.isNat_natCast 100 100
                            (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 100)))))
                      Nat.cast_one (Eq.refl 100)))
                  (congrArg (HPow.hPow 19)
                    (Mathlib.Meta.NormNum.IsNNRat.to_eq
                      (Mathlib.Meta.NormNum.isNNRat_div
                        (Mathlib.Meta.NormNum.isNNRat_mul (Eq.refl HMul.hMul)
                          (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one))
                          (Mathlib.Meta.NormNum.isNNRat_inv_pos
                            (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 100))))
                          (Eq.refl (Nat.mul 1 1)) (Eq.refl 100)))
                      Nat.cast_one (Eq.refl 100)))))
              (Eq.trans
                (congrArg (HPow.hPow 19)
                  (Mathlib.Meta.NormNum.IsNNRat.to_eq
                    (Mathlib.Meta.NormNum.isNNRat_inv_pos
                      (Mathlib.Meta.NormNum.IsNat.to_isNNRat
                        (Mathlib.Meta.NormNum.isNat_natCast 100 100 (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 100)))))
                    Nat.cast_one (Eq.refl 100)))
                (congrArg (HPow.hPow 19)
                  (Mathlib.Meta.NormNum.IsNNRat.to_eq
                    (Mathlib.Meta.NormNum.isNNRat_div
                      (Mathlib.Meta.NormNum.isNNRat_mul (Eq.refl HMul.hMul)
                        (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one))
                        (Mathlib.Meta.NormNum.isNNRat_inv_pos
                          (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 100))))
                        (Eq.refl (Nat.mul 1 1)) (Eq.refl 100)))
                    Nat.cast_one (Eq.refl 100)))))
            (eq_self (19 ^ (1 / 100))))
          (eq_true True.intro))))h100:Real.nthRoot 100 ↑19 ^ 100 = 19 := 
  Eq.mpr (id (congrArg (fun _a => _a ^ 100 = 19) hy))
    (Real.rpow_inv_natCast_pow
      (Mathlib.Meta.NormNum.isNat_le_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)
        (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 19)) (Eq.refl true))
      (Mathlib.Meta.NormNum.isNat_eq_false (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 100))
        (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 0)) (Eq.refl false)))⊢ 0 ≤ 9 norm_numAll goals completed! 🐙)
    have e : ((Real.nthRoot 100 ((19 : ℕ) : ℝ)) ^ (74 : ℕ)) ^ (100 : ℕ)
        = ((Real.nthRoot 100 ((19 : ℕ) : ℝ)) ^ (100 : ℕ)) ^ (74 : ℕ) := by⊢ ∃ n > 0, ∀ (k : ℕ), ↑k < 1 + Real.nthRoot 100 ↑n ^ 74 → ¬Nat.Prime (n * k + 1)
      rw [← pow_mul, ← pow_mul, Nat.mul_comm]All goals completed! 🐙
    rw [e, h100]hy:Real.nthRoot 100 ↑19 = 19 ^ (↑100)⁻¹ := 
  id
    (Eq.mpr (id (congrArg (fun _a => _a = 19 ^ (↑100)⁻¹) (if_pos (of_decide_eq_true (id (Eq.refl true))))))
      (of_eq_true
        (Eq.trans
          (Eq.trans
            (congr
              (congrArg Eq
                (Eq.trans
                  (congr
                    (congrArg HPow.hPow
                      (Mathlib.Meta.NormNum.IsNat.to_eq
                        (Mathlib.Meta.NormNum.isNat_natCast 19 19 (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 19)))
                        (Eq.refl 19)))
                    (Mathlib.Meta.NormNum.IsNNRat.to_eq
                      (Mathlib.Meta.NormNum.isNNRat_inv_pos
                        (Mathlib.Meta.NormNum.IsNat.to_isNNRat
                          (Mathlib.Meta.NormNum.isNat_natCast 100 100
                            (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 100)))))
                      Nat.cast_one (Eq.refl 100)))
                  (congrArg (HPow.hPow 19)
                    (Mathlib.Meta.NormNum.IsNNRat.to_eq
                      (Mathlib.Meta.NormNum.isNNRat_div
                        (Mathlib.Meta.NormNum.isNNRat_mul (Eq.refl HMul.hMul)
                          (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one))
                          (Mathlib.Meta.NormNum.isNNRat_inv_pos
                            (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 100))))
                          (Eq.refl (Nat.mul 1 1)) (Eq.refl 100)))
                      Nat.cast_one (Eq.refl 100)))))
              (Eq.trans
                (congrArg (HPow.hPow 19)
                  (Mathlib.Meta.NormNum.IsNNRat.to_eq
                    (Mathlib.Meta.NormNum.isNNRat_inv_pos
                      (Mathlib.Meta.NormNum.IsNat.to_isNNRat
                        (Mathlib.Meta.NormNum.isNat_natCast 100 100 (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 100)))))
                    Nat.cast_one (Eq.refl 100)))
                (congrArg (HPow.hPow 19)
                  (Mathlib.Meta.NormNum.IsNNRat.to_eq
                    (Mathlib.Meta.NormNum.isNNRat_div
                      (Mathlib.Meta.NormNum.isNNRat_mul (Eq.refl HMul.hMul)
                        (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one))
                        (Mathlib.Meta.NormNum.isNNRat_inv_pos
                          (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 100))))
                        (Eq.refl (Nat.mul 1 1)) (Eq.refl 100)))
                    Nat.cast_one (Eq.refl 100)))))
            (eq_self (19 ^ (1 / 100))))
          (eq_true True.intro))))h100:Real.nthRoot 100 ↑19 ^ 100 = 19 := 
  Eq.mpr (id (congrArg (fun _a => _a ^ 100 = 19) hy))
    (Real.rpow_inv_natCast_pow
      (Mathlib.Meta.NormNum.isNat_le_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)
        (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 19)) (Eq.refl true))
      (Mathlib.Meta.NormNum.isNat_eq_false (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 100))
        (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 0)) (Eq.refl false)))e:(Real.nthRoot 100 ↑19 ^ 74) ^ 100 = (Real.nthRoot 100 ↑19 ^ 100) ^ 74 := 
  Eq.mpr
    (id (congrArg (fun _a => _a = (Real.nthRoot 100 ↑19 ^ 100) ^ 74) (Eq.symm (pow_mul (Real.nthRoot 100 ↑19) 74 100))))
    (Eq.mpr
      (id (congrArg (fun _a => Real.nthRoot 100 ↑19 ^ (74 * 100) = _a) (Eq.symm (pow_mul (Real.nthRoot 100 ↑19) 100 74))))
      (Eq.mpr (id (congrArg (fun _a => Real.nthRoot 100 ↑19 ^ _a = Real.nthRoot 100 ↑19 ^ _a) (Nat.mul_comm 74 100)))
        (Eq.refl (Real.nthRoot 100 ↑19 ^ (100 * 74)))))⊢ 19 ^ 74 ≤ 9 ^ 100
    norm_numAll goals completed! 🐙
  intro k hkhy:Real.nthRoot 100 ↑19 = 19 ^ (↑100)⁻¹ := 
  id
    (Eq.mpr (id (congrArg (fun _a => _a = 19 ^ (↑100)⁻¹) (if_pos (of_decide_eq_true (id (Eq.refl true))))))
      (of_eq_true
        (Eq.trans
          (Eq.trans
            (congr
              (congrArg Eq
                (Eq.trans
                  (congr
                    (congrArg HPow.hPow
                      (Mathlib.Meta.NormNum.IsNat.to_eq
                        (Mathlib.Meta.NormNum.isNat_natCast 19 19 (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 19)))
                        (Eq.refl 19)))
                    (Mathlib.Meta.NormNum.IsNNRat.to_eq
                      (Mathlib.Meta.NormNum.isNNRat_inv_pos
                        (Mathlib.Meta.NormNum.IsNat.to_isNNRat
                          (Mathlib.Meta.NormNum.isNat_natCast 100 100
                            (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 100)))))
                      Nat.cast_one (Eq.refl 100)))
                  (congrArg (HPow.hPow 19)
                    (Mathlib.Meta.NormNum.IsNNRat.to_eq
                      (Mathlib.Meta.NormNum.isNNRat_div
                        (Mathlib.Meta.NormNum.isNNRat_mul (Eq.refl HMul.hMul)
                          (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one))
                          (Mathlib.Meta.NormNum.isNNRat_inv_pos
                            (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 100))))
                          (Eq.refl (Nat.mul 1 1)) (Eq.refl 100)))
                      Nat.cast_one (Eq.refl 100)))))
              (Eq.trans
                (congrArg (HPow.hPow 19)
                  (Mathlib.Meta.NormNum.IsNNRat.to_eq
                    (Mathlib.Meta.NormNum.isNNRat_inv_pos
                      (Mathlib.Meta.NormNum.IsNat.to_isNNRat
                        (Mathlib.Meta.NormNum.isNat_natCast 100 100 (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 100)))))
                    Nat.cast_one (Eq.refl 100)))
                (congrArg (HPow.hPow 19)
                  (Mathlib.Meta.NormNum.IsNNRat.to_eq
                    (Mathlib.Meta.NormNum.isNNRat_div
                      (Mathlib.Meta.NormNum.isNNRat_mul (Eq.refl HMul.hMul)
                        (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one))
                        (Mathlib.Meta.NormNum.isNNRat_inv_pos
                          (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 100))))
                        (Eq.refl (Nat.mul 1 1)) (Eq.refl 100)))
                    Nat.cast_one (Eq.refl 100)))))
            (eq_self (19 ^ (1 / 100))))
          (eq_true True.intro))))h100:Real.nthRoot 100 ↑19 ^ 100 = 19 := 
  Eq.mpr (id (congrArg (fun _a => _a ^ 100 = 19) hy))
    (Real.rpow_inv_natCast_pow
      (Mathlib.Meta.NormNum.isNat_le_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)
        (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 19)) (Eq.refl true))
      (Mathlib.Meta.NormNum.isNat_eq_false (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 100))
        (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 0)) (Eq.refl false)))hb:Real.nthRoot 100 ↑19 ^ 74 ≤ 9 := 
  le_of_pow_le_pow_left₀
    (Mathlib.Meta.NormNum.isNat_eq_false (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 100))
      (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 0)) (Eq.refl false))
    (Mathlib.Meta.NormNum.isNat_le_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)
      (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 9)) (Eq.refl true))
    (have e :=
      Eq.mpr
        (id
          (congrArg (fun _a => _a = (Real.nthRoot 100 ↑19 ^ 100) ^ 74) (Eq.symm (pow_mul (Real.nthRoot 100 ↑19) 74 100))))
        (Eq.mpr
          (id
            (congrArg (fun _a => Real.nthRoot 100 ↑19 ^ (74 * 100) = _a)
              (Eq.symm (pow_mul (Real.nthRoot 100 ↑19) 100 74))))
          (Eq.mpr (id (congrArg (fun _a => Real.nthRoot 100 ↑19 ^ _a = Real.nthRoot 100 ↑19 ^ _a) (Nat.mul_comm 74 100)))
            (Eq.refl (Real.nthRoot 100 ↑19 ^ (100 * 74)))));
    Eq.mpr (id (congrArg (fun _a => _a ≤ 9 ^ 100) e))
      (Eq.mpr (id (congrArg (fun _a => _a ^ 74 ≤ 9 ^ 100) h100))
        (Mathlib.Meta.NormNum.isNat_le_true
          (Mathlib.Meta.NormNum.isNat_pow (Eq.refl HPow.hPow) (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 19))
            (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 74))
            (Mathlib.Meta.NormNum.IsNatPowT.run
              (Mathlib.Meta.NormNum.IsNatPowT.trans
                (Mathlib.Meta.NormNum.IsNatPowT.trans
                  (Mathlib.Meta.NormNum.IsNatPowT.trans Mathlib.Meta.NormNum.IsNatPowT.bit0
                    Mathlib.Meta.NormNum.IsNatPowT.bit0)
                  Mathlib.Meta.NormNum.IsNatPowT.bit1)
                (Mathlib.Meta.NormNum.IsNatPowT.trans
                  (Mathlib.Meta.NormNum.IsNatPowT.trans Mathlib.Meta.NormNum.IsNatPowT.bit0
                    Mathlib.Meta.NormNum.IsNatPowT.bit1)
                  Mathlib.Meta.NormNum.IsNatPowT.bit0))))
          (Mathlib.Meta.NormNum.isNat_pow (Eq.refl HPow.hPow) (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 9))
            (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 100))
            (Mathlib.Meta.NormNum.IsNatPowT.run
              (Mathlib.Meta.NormNum.IsNatPowT.trans
                (Mathlib.Meta.NormNum.IsNatPowT.trans
                  (Mathlib.Meta.NormNum.IsNatPowT.trans Mathlib.Meta.NormNum.IsNatPowT.bit1
                    Mathlib.Meta.NormNum.IsNatPowT.bit0)
                  Mathlib.Meta.NormNum.IsNatPowT.bit0)
                (Mathlib.Meta.NormNum.IsNatPowT.trans
                  (Mathlib.Meta.NormNum.IsNatPowT.trans Mathlib.Meta.NormNum.IsNatPowT.bit1
                    Mathlib.Meta.NormNum.IsNatPowT.bit0)
                  Mathlib.Meta.NormNum.IsNatPowT.bit0))))
          (Eq.refl true))))k:ℕhk:↑k < 1 + Real.nthRoot 100 ↑19 ^ 74⊢ ¬Nat.Prime (19 * k + 1)
  have hk10 : (k : ℝ) < 10 := by⊢ ∃ n > 0, ∀ (k : ℕ), ↑k < 1 + Real.nthRoot 100 ↑n ^ 74 → ¬Nat.Prime (n * k + 1) linarithAll goals completed! 🐙
  have hk10' : k < 10 := by⊢ ∃ n > 0, ∀ (k : ℕ), ↑k < 1 + Real.nthRoot 100 ↑n ^ 74 → ¬Nat.Prime (n * k + 1) exact_mod_cast hk10All goals completed! 🐙
  interval_cases k«0»hy:Real.nthRoot 100 ↑19 = 19 ^ (↑100)⁻¹ := 
  id
    (Eq.mpr (id (congrArg (fun _a => _a = 19 ^ (↑100)⁻¹) (if_pos (of_decide_eq_true (id (Eq.refl true))))))
      (of_eq_true
        (Eq.trans
          (Eq.trans
            (congr
              (congrArg Eq
                (Eq.trans
                  (congr
                    (congrArg HPow.hPow
                      (Mathlib.Meta.NormNum.IsNat.to_eq
                        (Mathlib.Meta.NormNum.isNat_natCast 19 19 (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 19)))
                        (Eq.refl 19)))
                    (Mathlib.Meta.NormNum.IsNNRat.to_eq
                      (Mathlib.Meta.NormNum.isNNRat_inv_pos
                        (Mathlib.Meta.NormNum.IsNat.to_isNNRat
                          (Mathlib.Meta.NormNum.isNat_natCast 100 100
                            (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 100)))))
                      Nat.cast_one (Eq.refl 100)))
                  (congrArg (HPow.hPow 19)
                    (Mathlib.Meta.NormNum.IsNNRat.to_eq
                      (Mathlib.Meta.NormNum.isNNRat_div
                        (Mathlib.Meta.NormNum.isNNRat_mul (Eq.refl HMul.hMul)
                          (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one))
                          (Mathlib.Meta.NormNum.isNNRat_inv_pos
                            (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 100))))
                          (Eq.refl (Nat.mul 1 1)) (Eq.refl 100)))
                      Nat.cast_one (Eq.refl 100)))))
              (Eq.trans
                (congrArg (HPow.hPow 19)
                  (Mathlib.Meta.NormNum.IsNNRat.to_eq
                    (Mathlib.Meta.NormNum.isNNRat_inv_pos
                      (Mathlib.Meta.NormNum.IsNat.to_isNNRat
                        (Mathlib.Meta.NormNum.isNat_natCast 100 100 (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 100)))))
                    Nat.cast_one (Eq.refl 100)))
                (congrArg (HPow.hPow 19)
                  (Mathlib.Meta.NormNum.IsNNRat.to_eq
                    (Mathlib.Meta.NormNum.isNNRat_div
                      (Mathlib.Meta.NormNum.isNNRat_mul (Eq.refl HMul.hMul)
                        (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one))
                        (Mathlib.Meta.NormNum.isNNRat_inv_pos
                          (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 100))))
                        (Eq.refl (Nat.mul 1 1)) (Eq.refl 100)))
                    Nat.cast_one (Eq.refl 100)))))
            (eq_self (19 ^ (1 / 100))))
          (eq_true True.intro))))h100:Real.nthRoot 100 ↑19 ^ 100 = 19 := 
  Eq.mpr (id (congrArg (fun _a => _a ^ 100 = 19) hy))
    (Real.rpow_inv_natCast_pow
      (Mathlib.Meta.NormNum.isNat_le_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)
        (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 19)) (Eq.refl true))
      (Mathlib.Meta.NormNum.isNat_eq_false (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 100))
        (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 0)) (Eq.refl false)))hb:Real.nthRoot 100 ↑19 ^ 74 ≤ 9 := 
  le_of_pow_le_pow_left₀
    (Mathlib.Meta.NormNum.isNat_eq_false (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 100))
      (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 0)) (Eq.refl false))
    (Mathlib.Meta.NormNum.isNat_le_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)
      (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 9)) (Eq.refl true))
    (have e :=
      Eq.mpr
        (id
          (congrArg (fun _a => _a = (Real.nthRoot 100 ↑19 ^ 100) ^ 74) (Eq.symm (pow_mul (Real.nthRoot 100 ↑19) 74 100))))
        (Eq.mpr
          (id
            (congrArg (fun _a => Real.nthRoot 100 ↑19 ^ (74 * 100) = _a)
              (Eq.symm (pow_mul (Real.nthRoot 100 ↑19) 100 74))))
          (Eq.mpr (id (congrArg (fun _a => Real.nthRoot 100 ↑19 ^ _a = Real.nthRoot 100 ↑19 ^ _a) (Nat.mul_comm 74 100)))
            (Eq.refl (Real.nthRoot 100 ↑19 ^ (100 * 74)))));
    Eq.mpr (id (congrArg (fun _a => _a ≤ 9 ^ 100) e))
      (Eq.mpr (id (congrArg (fun _a => _a ^ 74 ≤ 9 ^ 100) h100))
        (Mathlib.Meta.NormNum.isNat_le_true
          (Mathlib.Meta.NormNum.isNat_pow (Eq.refl HPow.hPow) (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 19))
            (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 74))
            (Mathlib.Meta.NormNum.IsNatPowT.run
              (Mathlib.Meta.NormNum.IsNatPowT.trans
                (Mathlib.Meta.NormNum.IsNatPowT.trans
                  (Mathlib.Meta.NormNum.IsNatPowT.trans Mathlib.Meta.NormNum.IsNatPowT.bit0
                    Mathlib.Meta.NormNum.IsNatPowT.bit0)
                  Mathlib.Meta.NormNum.IsNatPowT.bit1)
                (Mathlib.Meta.NormNum.IsNatPowT.trans
                  (Mathlib.Meta.NormNum.IsNatPowT.trans Mathlib.Meta.NormNum.IsNatPowT.bit0
                    Mathlib.Meta.NormNum.IsNatPowT.bit1)
                  Mathlib.Meta.NormNum.IsNatPowT.bit0))))
          (Mathlib.Meta.NormNum.isNat_pow (Eq.refl HPow.hPow) (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 9))
            (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 100))
            (Mathlib.Meta.NormNum.IsNatPowT.run
              (Mathlib.Meta.NormNum.IsNatPowT.trans
                (Mathlib.Meta.NormNum.IsNatPowT.trans
                  (Mathlib.Meta.NormNum.IsNatPowT.trans Mathlib.Meta.NormNum.IsNatPowT.bit1
                    Mathlib.Meta.NormNum.IsNatPowT.bit0)
                  Mathlib.Meta.NormNum.IsNatPowT.bit0)
                (Mathlib.Meta.NormNum.IsNatPowT.trans
                  (Mathlib.Meta.NormNum.IsNatPowT.trans Mathlib.Meta.NormNum.IsNatPowT.bit1
                    Mathlib.Meta.NormNum.IsNatPowT.bit0)
                  Mathlib.Meta.NormNum.IsNatPowT.bit0))))
          (Eq.refl true))))k:ℕhk:↑0 < 1 + Real.nthRoot 100 ↑19 ^ 74hk10:↑0 < 10hk10':0 < 10⊢ ¬Nat.Prime (19 * 0 + 1)«1»hy:Real.nthRoot 100 ↑19 = 19 ^ (↑100)⁻¹ := 
  id
    (Eq.mpr (id (congrArg (fun _a => _a = 19 ^ (↑100)⁻¹) (if_pos (of_decide_eq_true (id (Eq.refl true))))))
      (of_eq_true
        (Eq.trans
          (Eq.trans
            (congr
              (congrArg Eq
                (Eq.trans
                  (congr
                    (congrArg HPow.hPow
                      (Mathlib.Meta.NormNum.IsNat.to_eq
                        (Mathlib.Meta.NormNum.isNat_natCast 19 19 (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 19)))
                        (Eq.refl 19)))
                    (Mathlib.Meta.NormNum.IsNNRat.to_eq
                      (Mathlib.Meta.NormNum.isNNRat_inv_pos
                        (Mathlib.Meta.NormNum.IsNat.to_isNNRat
                          (Mathlib.Meta.NormNum.isNat_natCast 100 100
                            (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 100)))))
                      Nat.cast_one (Eq.refl 100)))
                  (congrArg (HPow.hPow 19)
                    (Mathlib.Meta.NormNum.IsNNRat.to_eq
                      (Mathlib.Meta.NormNum.isNNRat_div
                        (Mathlib.Meta.NormNum.isNNRat_mul (Eq.refl HMul.hMul)
                          (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one))
                          (Mathlib.Meta.NormNum.isNNRat_inv_pos
                            (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 100))))
                          (Eq.refl (Nat.mul 1 1)) (Eq.refl 100)))
                      Nat.cast_one (Eq.refl 100)))))
              (Eq.trans
                (congrArg (HPow.hPow 19)
                  (Mathlib.Meta.NormNum.IsNNRat.to_eq
                    (Mathlib.Meta.NormNum.isNNRat_inv_pos
                      (Mathlib.Meta.NormNum.IsNat.to_isNNRat
                        (Mathlib.Meta.NormNum.isNat_natCast 100 100 (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 100)))))
                    Nat.cast_one (Eq.refl 100)))
                (congrArg (HPow.hPow 19)
                  (Mathlib.Meta.NormNum.IsNNRat.to_eq
                    (Mathlib.Meta.NormNum.isNNRat_div
                      (Mathlib.Meta.NormNum.isNNRat_mul (Eq.refl HMul.hMul)
                        (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one))
                        (Mathlib.Meta.NormNum.isNNRat_inv_pos
                          (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 100))))
                        (Eq.refl (Nat.mul 1 1)) (Eq.refl 100)))
                    Nat.cast_one (Eq.refl 100)))))
            (eq_self (19 ^ (1 / 100))))
          (eq_true True.intro))))h100:Real.nthRoot 100 ↑19 ^ 100 = 19 := 
  Eq.mpr (id (congrArg (fun _a => _a ^ 100 = 19) hy))
    (Real.rpow_inv_natCast_pow
      (Mathlib.Meta.NormNum.isNat_le_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)
        (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 19)) (Eq.refl true))
      (Mathlib.Meta.NormNum.isNat_eq_false (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 100))
        (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 0)) (Eq.refl false)))hb:Real.nthRoot 100 ↑19 ^ 74 ≤ 9 := 
  le_of_pow_le_pow_left₀
    (Mathlib.Meta.NormNum.isNat_eq_false (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 100))
      (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 0)) (Eq.refl false))
    (Mathlib.Meta.NormNum.isNat_le_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)
      (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 9)) (Eq.refl true))
    (have e :=
      Eq.mpr
        (id
          (congrArg (fun _a => _a = (Real.nthRoot 100 ↑19 ^ 100) ^ 74) (Eq.symm (pow_mul (Real.nthRoot 100 ↑19) 74 100))))
        (Eq.mpr
          (id
            (congrArg (fun _a => Real.nthRoot 100 ↑19 ^ (74 * 100) = _a)
              (Eq.symm (pow_mul (Real.nthRoot 100 ↑19) 100 74))))
          (Eq.mpr (id (congrArg (fun _a => Real.nthRoot 100 ↑19 ^ _a = Real.nthRoot 100 ↑19 ^ _a) (Nat.mul_comm 74 100)))
            (Eq.refl (Real.nthRoot 100 ↑19 ^ (100 * 74)))));
    Eq.mpr (id (congrArg (fun _a => _a ≤ 9 ^ 100) e))
      (Eq.mpr (id (congrArg (fun _a => _a ^ 74 ≤ 9 ^ 100) h100))
        (Mathlib.Meta.NormNum.isNat_le_true
          (Mathlib.Meta.NormNum.isNat_pow (Eq.refl HPow.hPow) (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 19))
            (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 74))
            (Mathlib.Meta.NormNum.IsNatPowT.run
              (Mathlib.Meta.NormNum.IsNatPowT.trans
                (Mathlib.Meta.NormNum.IsNatPowT.trans
                  (Mathlib.Meta.NormNum.IsNatPowT.trans Mathlib.Meta.NormNum.IsNatPowT.bit0
                    Mathlib.Meta.NormNum.IsNatPowT.bit0)
                  Mathlib.Meta.NormNum.IsNatPowT.bit1)
                (Mathlib.Meta.NormNum.IsNatPowT.trans
                  (Mathlib.Meta.NormNum.IsNatPowT.trans Mathlib.Meta.NormNum.IsNatPowT.bit0
                    Mathlib.Meta.NormNum.IsNatPowT.bit1)
                  Mathlib.Meta.NormNum.IsNatPowT.bit0))))
          (Mathlib.Meta.NormNum.isNat_pow (Eq.refl HPow.hPow) (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 9))
            (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 100))
            (Mathlib.Meta.NormNum.IsNatPowT.run
              (Mathlib.Meta.NormNum.IsNatPowT.trans
                (Mathlib.Meta.NormNum.IsNatPowT.trans
                  (Mathlib.Meta.NormNum.IsNatPowT.trans Mathlib.Meta.NormNum.IsNatPowT.bit1
                    Mathlib.Meta.NormNum.IsNatPowT.bit0)
                  Mathlib.Meta.NormNum.IsNatPowT.bit0)
                (Mathlib.Meta.NormNum.IsNatPowT.trans
                  (Mathlib.Meta.NormNum.IsNatPowT.trans Mathlib.Meta.NormNum.IsNatPowT.bit1
                    Mathlib.Meta.NormNum.IsNatPowT.bit0)
                  Mathlib.Meta.NormNum.IsNatPowT.bit0))))
          (Eq.refl true))))k:ℕhk:↑1 < 1 + Real.nthRoot 100 ↑19 ^ 74hk10:↑1 < 10hk10':1 < 10⊢ ¬Nat.Prime (19 * 1 + 1)«2»hy:Real.nthRoot 100 ↑19 = 19 ^ (↑100)⁻¹ := 
  id
    (Eq.mpr (id (congrArg (fun _a => _a = 19 ^ (↑100)⁻¹) (if_pos (of_decide_eq_true (id (Eq.refl true))))))
      (of_eq_true
        (Eq.trans
          (Eq.trans
            (congr
              (congrArg Eq
                (Eq.trans
                  (congr
                    (congrArg HPow.hPow
                      (Mathlib.Meta.NormNum.IsNat.to_eq
                        (Mathlib.Meta.NormNum.isNat_natCast 19 19 (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 19)))
                        (Eq.refl 19)))
                    (Mathlib.Meta.NormNum.IsNNRat.to_eq
                      (Mathlib.Meta.NormNum.isNNRat_inv_pos
                        (Mathlib.Meta.NormNum.IsNat.to_isNNRat
                          (Mathlib.Meta.NormNum.isNat_natCast 100 100
                            (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 100)))))
                      Nat.cast_one (Eq.refl 100)))
                  (congrArg (HPow.hPow 19)
                    (Mathlib.Meta.NormNum.IsNNRat.to_eq
                      (Mathlib.Meta.NormNum.isNNRat_div
                        (Mathlib.Meta.NormNum.isNNRat_mul (Eq.refl HMul.hMul)
                          (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one))
                          (Mathlib.Meta.NormNum.isNNRat_inv_pos
                            (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 100))))
                          (Eq.refl (Nat.mul 1 1)) (Eq.refl 100)))
                      Nat.cast_one (Eq.refl 100)))))
              (Eq.trans
                (congrArg (HPow.hPow 19)
                  (Mathlib.Meta.NormNum.IsNNRat.to_eq
                    (Mathlib.Meta.NormNum.isNNRat_inv_pos
                      (Mathlib.Meta.NormNum.IsNat.to_isNNRat
                        (Mathlib.Meta.NormNum.isNat_natCast 100 100 (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 100)))))
                    Nat.cast_one (Eq.refl 100)))
                (congrArg (HPow.hPow 19)
                  (Mathlib.Meta.NormNum.IsNNRat.to_eq
                    (Mathlib.Meta.NormNum.isNNRat_div
                      (Mathlib.Meta.NormNum.isNNRat_mul (Eq.refl HMul.hMul)
                        (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one))
                        (Mathlib.Meta.NormNum.isNNRat_inv_pos
                          (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 100))))
                        (Eq.refl (Nat.mul 1 1)) (Eq.refl 100)))
                    Nat.cast_one (Eq.refl 100)))))
            (eq_self (19 ^ (1 / 100))))
          (eq_true True.intro))))h100:Real.nthRoot 100 ↑19 ^ 100 = 19 := 
  Eq.mpr (id (congrArg (fun _a => _a ^ 100 = 19) hy))
    (Real.rpow_inv_natCast_pow
      (Mathlib.Meta.NormNum.isNat_le_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)
        (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 19)) (Eq.refl true))
      (Mathlib.Meta.NormNum.isNat_eq_false (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 100))
        (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 0)) (Eq.refl false)))hb:Real.nthRoot 100 ↑19 ^ 74 ≤ 9 := 
  le_of_pow_le_pow_left₀
    (Mathlib.Meta.NormNum.isNat_eq_false (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 100))
      (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 0)) (Eq.refl false))
    (Mathlib.Meta.NormNum.isNat_le_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)
      (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 9)) (Eq.refl true))
    (have e :=
      Eq.mpr
        (id
          (congrArg (fun _a => _a = (Real.nthRoot 100 ↑19 ^ 100) ^ 74) (Eq.symm (pow_mul (Real.nthRoot 100 ↑19) 74 100))))
        (Eq.mpr
          (id
            (congrArg (fun _a => Real.nthRoot 100 ↑19 ^ (74 * 100) = _a)
              (Eq.symm (pow_mul (Real.nthRoot 100 ↑19) 100 74))))
          (Eq.mpr (id (congrArg (fun _a => Real.nthRoot 100 ↑19 ^ _a = Real.nthRoot 100 ↑19 ^ _a) (Nat.mul_comm 74 100)))
            (Eq.refl (Real.nthRoot 100 ↑19 ^ (100 * 74)))));
    Eq.mpr (id (congrArg (fun _a => _a ≤ 9 ^ 100) e))
      (Eq.mpr (id (congrArg (fun _a => _a ^ 74 ≤ 9 ^ 100) h100))
        (Mathlib.Meta.NormNum.isNat_le_true
          (Mathlib.Meta.NormNum.isNat_pow (Eq.refl HPow.hPow) (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 19))
            (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 74))
            (Mathlib.Meta.NormNum.IsNatPowT.run
              (Mathlib.Meta.NormNum.IsNatPowT.trans
                (Mathlib.Meta.NormNum.IsNatPowT.trans
                  (Mathlib.Meta.NormNum.IsNatPowT.trans Mathlib.Meta.NormNum.IsNatPowT.bit0
                    Mathlib.Meta.NormNum.IsNatPowT.bit0)
                  Mathlib.Meta.NormNum.IsNatPowT.bit1)
                (Mathlib.Meta.NormNum.IsNatPowT.trans
                  (Mathlib.Meta.NormNum.IsNatPowT.trans Mathlib.Meta.NormNum.IsNatPowT.bit0
                    Mathlib.Meta.NormNum.IsNatPowT.bit1)
                  Mathlib.Meta.NormNum.IsNatPowT.bit0))))
          (Mathlib.Meta.NormNum.isNat_pow (Eq.refl HPow.hPow) (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 9))
            (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 100))
            (Mathlib.Meta.NormNum.IsNatPowT.run
              (Mathlib.Meta.NormNum.IsNatPowT.trans
                (Mathlib.Meta.NormNum.IsNatPowT.trans
                  (Mathlib.Meta.NormNum.IsNatPowT.trans Mathlib.Meta.NormNum.IsNatPowT.bit1
                    Mathlib.Meta.NormNum.IsNatPowT.bit0)
                  Mathlib.Meta.NormNum.IsNatPowT.bit0)
                (Mathlib.Meta.NormNum.IsNatPowT.trans
                  (Mathlib.Meta.NormNum.IsNatPowT.trans Mathlib.Meta.NormNum.IsNatPowT.bit1
                    Mathlib.Meta.NormNum.IsNatPowT.bit0)
                  Mathlib.Meta.NormNum.IsNatPowT.bit0))))
          (Eq.refl true))))k:ℕhk:↑2 < 1 + Real.nthRoot 100 ↑19 ^ 74hk10:↑2 < 10hk10':2 < 10⊢ ¬Nat.Prime (19 * 2 + 1)«3»hy:Real.nthRoot 100 ↑19 = 19 ^ (↑100)⁻¹ := 
  id
    (Eq.mpr (id (congrArg (fun _a => _a = 19 ^ (↑100)⁻¹) (if_pos (of_decide_eq_true (id (Eq.refl true))))))
      (of_eq_true
        (Eq.trans
          (Eq.trans
            (congr
              (congrArg Eq
                (Eq.trans
                  (congr
                    (congrArg HPow.hPow
                      (Mathlib.Meta.NormNum.IsNat.to_eq
                        (Mathlib.Meta.NormNum.isNat_natCast 19 19 (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 19)))
                        (Eq.refl 19)))
                    (Mathlib.Meta.NormNum.IsNNRat.to_eq
                      (Mathlib.Meta.NormNum.isNNRat_inv_pos
                        (Mathlib.Meta.NormNum.IsNat.to_isNNRat
                          (Mathlib.Meta.NormNum.isNat_natCast 100 100
                            (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 100)))))
                      Nat.cast_one (Eq.refl 100)))
                  (congrArg (HPow.hPow 19)
                    (Mathlib.Meta.NormNum.IsNNRat.to_eq
                      (Mathlib.Meta.NormNum.isNNRat_div
                        (Mathlib.Meta.NormNum.isNNRat_mul (Eq.refl HMul.hMul)
                          (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one))
                          (Mathlib.Meta.NormNum.isNNRat_inv_pos
                            (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 100))))
                          (Eq.refl (Nat.mul 1 1)) (Eq.refl 100)))
                      Nat.cast_one (Eq.refl 100)))))
              (Eq.trans
                (congrArg (HPow.hPow 19)
                  (Mathlib.Meta.NormNum.IsNNRat.to_eq
                    (Mathlib.Meta.NormNum.isNNRat_inv_pos
                      (Mathlib.Meta.NormNum.IsNat.to_isNNRat
                        (Mathlib.Meta.NormNum.isNat_natCast 100 100 (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 100)))))
                    Nat.cast_one (Eq.refl 100)))
                (congrArg (HPow.hPow 19)
                  (Mathlib.Meta.NormNum.IsNNRat.to_eq
                    (Mathlib.Meta.NormNum.isNNRat_div
                      (Mathlib.Meta.NormNum.isNNRat_mul (Eq.refl HMul.hMul)
                        (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one))
                        (Mathlib.Meta.NormNum.isNNRat_inv_pos
                          (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 100))))
                        (Eq.refl (Nat.mul 1 1)) (Eq.refl 100)))
                    Nat.cast_one (Eq.refl 100)))))
            (eq_self (19 ^ (1 / 100))))
          (eq_true True.intro))))h100:Real.nthRoot 100 ↑19 ^ 100 = 19 := 
  Eq.mpr (id (congrArg (fun _a => _a ^ 100 = 19) hy))
    (Real.rpow_inv_natCast_pow
      (Mathlib.Meta.NormNum.isNat_le_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)
        (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 19)) (Eq.refl true))
      (Mathlib.Meta.NormNum.isNat_eq_false (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 100))
        (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 0)) (Eq.refl false)))hb:Real.nthRoot 100 ↑19 ^ 74 ≤ 9 := 
  le_of_pow_le_pow_left₀
    (Mathlib.Meta.NormNum.isNat_eq_false (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 100))
      (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 0)) (Eq.refl false))
    (Mathlib.Meta.NormNum.isNat_le_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)
      (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 9)) (Eq.refl true))
    (have e :=
      Eq.mpr
        (id
          (congrArg (fun _a => _a = (Real.nthRoot 100 ↑19 ^ 100) ^ 74) (Eq.symm (pow_mul (Real.nthRoot 100 ↑19) 74 100))))
        (Eq.mpr
          (id
            (congrArg (fun _a => Real.nthRoot 100 ↑19 ^ (74 * 100) = _a)
              (Eq.symm (pow_mul (Real.nthRoot 100 ↑19) 100 74))))
          (Eq.mpr (id (congrArg (fun _a => Real.nthRoot 100 ↑19 ^ _a = Real.nthRoot 100 ↑19 ^ _a) (Nat.mul_comm 74 100)))
            (Eq.refl (Real.nthRoot 100 ↑19 ^ (100 * 74)))));
    Eq.mpr (id (congrArg (fun _a => _a ≤ 9 ^ 100) e))
      (Eq.mpr (id (congrArg (fun _a => _a ^ 74 ≤ 9 ^ 100) h100))
        (Mathlib.Meta.NormNum.isNat_le_true
          (Mathlib.Meta.NormNum.isNat_pow (Eq.refl HPow.hPow) (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 19))
            (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 74))
            (Mathlib.Meta.NormNum.IsNatPowT.run
              (Mathlib.Meta.NormNum.IsNatPowT.trans
                (Mathlib.Meta.NormNum.IsNatPowT.trans
                  (Mathlib.Meta.NormNum.IsNatPowT.trans Mathlib.Meta.NormNum.IsNatPowT.bit0
                    Mathlib.Meta.NormNum.IsNatPowT.bit0)
                  Mathlib.Meta.NormNum.IsNatPowT.bit1)
                (Mathlib.Meta.NormNum.IsNatPowT.trans
                  (Mathlib.Meta.NormNum.IsNatPowT.trans Mathlib.Meta.NormNum.IsNatPowT.bit0
                    Mathlib.Meta.NormNum.IsNatPowT.bit1)
                  Mathlib.Meta.NormNum.IsNatPowT.bit0))))
          (Mathlib.Meta.NormNum.isNat_pow (Eq.refl HPow.hPow) (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 9))
            (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 100))
            (Mathlib.Meta.NormNum.IsNatPowT.run
              (Mathlib.Meta.NormNum.IsNatPowT.trans
                (Mathlib.Meta.NormNum.IsNatPowT.trans
                  (Mathlib.Meta.NormNum.IsNatPowT.trans Mathlib.Meta.NormNum.IsNatPowT.bit1
                    Mathlib.Meta.NormNum.IsNatPowT.bit0)
                  Mathlib.Meta.NormNum.IsNatPowT.bit0)
                (Mathlib.Meta.NormNum.IsNatPowT.trans
                  (Mathlib.Meta.NormNum.IsNatPowT.trans Mathlib.Meta.NormNum.IsNatPowT.bit1
                    Mathlib.Meta.NormNum.IsNatPowT.bit0)
                  Mathlib.Meta.NormNum.IsNatPowT.bit0))))
          (Eq.refl true))))k:ℕhk:↑3 < 1 + Real.nthRoot 100 ↑19 ^ 74hk10:↑3 < 10hk10':3 < 10⊢ ¬Nat.Prime (19 * 3 + 1)«4»hy:Real.nthRoot 100 ↑19 = 19 ^ (↑100)⁻¹ := 
  id
    (Eq.mpr (id (congrArg (fun _a => _a = 19 ^ (↑100)⁻¹) (if_pos (of_decide_eq_true (id (Eq.refl true))))))
      (of_eq_true
        (Eq.trans
          (Eq.trans
            (congr
              (congrArg Eq
                (Eq.trans
                  (congr
                    (congrArg HPow.hPow
                      (Mathlib.Meta.NormNum.IsNat.to_eq
                        (Mathlib.Meta.NormNum.isNat_natCast 19 19 (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 19)))
                        (Eq.refl 19)))
                    (Mathlib.Meta.NormNum.IsNNRat.to_eq
                      (Mathlib.Meta.NormNum.isNNRat_inv_pos
                        (Mathlib.Meta.NormNum.IsNat.to_isNNRat
                          (Mathlib.Meta.NormNum.isNat_natCast 100 100
                            (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 100)))))
                      Nat.cast_one (Eq.refl 100)))
                  (congrArg (HPow.hPow 19)
                    (Mathlib.Meta.NormNum.IsNNRat.to_eq
                      (Mathlib.Meta.NormNum.isNNRat_div
                        (Mathlib.Meta.NormNum.isNNRat_mul (Eq.refl HMul.hMul)
                          (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one))
                          (Mathlib.Meta.NormNum.isNNRat_inv_pos
                            (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 100))))
                          (Eq.refl (Nat.mul 1 1)) (Eq.refl 100)))
                      Nat.cast_one (Eq.refl 100)))))
              (Eq.trans
                (congrArg (HPow.hPow 19)
                  (Mathlib.Meta.NormNum.IsNNRat.to_eq
                    (Mathlib.Meta.NormNum.isNNRat_inv_pos
                      (Mathlib.Meta.NormNum.IsNat.to_isNNRat
                        (Mathlib.Meta.NormNum.isNat_natCast 100 100 (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 100)))))
                    Nat.cast_one (Eq.refl 100)))
                (congrArg (HPow.hPow 19)
                  (Mathlib.Meta.NormNum.IsNNRat.to_eq
                    (Mathlib.Meta.NormNum.isNNRat_div
                      (Mathlib.Meta.NormNum.isNNRat_mul (Eq.refl HMul.hMul)
                        (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one))
                        (Mathlib.Meta.NormNum.isNNRat_inv_pos
                          (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 100))))
                        (Eq.refl (Nat.mul 1 1)) (Eq.refl 100)))
                    Nat.cast_one (Eq.refl 100)))))
            (eq_self (19 ^ (1 / 100))))
          (eq_true True.intro))))h100:Real.nthRoot 100 ↑19 ^ 100 = 19 := 
  Eq.mpr (id (congrArg (fun _a => _a ^ 100 = 19) hy))
    (Real.rpow_inv_natCast_pow
      (Mathlib.Meta.NormNum.isNat_le_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)
        (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 19)) (Eq.refl true))
      (Mathlib.Meta.NormNum.isNat_eq_false (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 100))
        (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 0)) (Eq.refl false)))hb:Real.nthRoot 100 ↑19 ^ 74 ≤ 9 := 
  le_of_pow_le_pow_left₀
    (Mathlib.Meta.NormNum.isNat_eq_false (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 100))
      (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 0)) (Eq.refl false))
    (Mathlib.Meta.NormNum.isNat_le_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)
      (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 9)) (Eq.refl true))
    (have e :=
      Eq.mpr
        (id
          (congrArg (fun _a => _a = (Real.nthRoot 100 ↑19 ^ 100) ^ 74) (Eq.symm (pow_mul (Real.nthRoot 100 ↑19) 74 100))))
        (Eq.mpr
          (id
            (congrArg (fun _a => Real.nthRoot 100 ↑19 ^ (74 * 100) = _a)
              (Eq.symm (pow_mul (Real.nthRoot 100 ↑19) 100 74))))
          (Eq.mpr (id (congrArg (fun _a => Real.nthRoot 100 ↑19 ^ _a = Real.nthRoot 100 ↑19 ^ _a) (Nat.mul_comm 74 100)))
            (Eq.refl (Real.nthRoot 100 ↑19 ^ (100 * 74)))));
    Eq.mpr (id (congrArg (fun _a => _a ≤ 9 ^ 100) e))
      (Eq.mpr (id (congrArg (fun _a => _a ^ 74 ≤ 9 ^ 100) h100))
        (Mathlib.Meta.NormNum.isNat_le_true
          (Mathlib.Meta.NormNum.isNat_pow (Eq.refl HPow.hPow) (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 19))
            (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 74))
            (Mathlib.Meta.NormNum.IsNatPowT.run
              (Mathlib.Meta.NormNum.IsNatPowT.trans
                (Mathlib.Meta.NormNum.IsNatPowT.trans
                  (Mathlib.Meta.NormNum.IsNatPowT.trans Mathlib.Meta.NormNum.IsNatPowT.bit0
                    Mathlib.Meta.NormNum.IsNatPowT.bit0)
                  Mathlib.Meta.NormNum.IsNatPowT.bit1)
                (Mathlib.Meta.NormNum.IsNatPowT.trans
                  (Mathlib.Meta.NormNum.IsNatPowT.trans Mathlib.Meta.NormNum.IsNatPowT.bit0
                    Mathlib.Meta.NormNum.IsNatPowT.bit1)
                  Mathlib.Meta.NormNum.IsNatPowT.bit0))))
          (Mathlib.Meta.NormNum.isNat_pow (Eq.refl HPow.hPow) (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 9))
            (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 100))
            (Mathlib.Meta.NormNum.IsNatPowT.run
              (Mathlib.Meta.NormNum.IsNatPowT.trans
                (Mathlib.Meta.NormNum.IsNatPowT.trans
                  (Mathlib.Meta.NormNum.IsNatPowT.trans Mathlib.Meta.NormNum.IsNatPowT.bit1
                    Mathlib.Meta.NormNum.IsNatPowT.bit0)
                  Mathlib.Meta.NormNum.IsNatPowT.bit0)
                (Mathlib.Meta.NormNum.IsNatPowT.trans
                  (Mathlib.Meta.NormNum.IsNatPowT.trans Mathlib.Meta.NormNum.IsNatPowT.bit1
                    Mathlib.Meta.NormNum.IsNatPowT.bit0)
                  Mathlib.Meta.NormNum.IsNatPowT.bit0))))
          (Eq.refl true))))k:ℕhk:↑4 < 1 + Real.nthRoot 100 ↑19 ^ 74hk10:↑4 < 10hk10':4 < 10⊢ ¬Nat.Prime (19 * 4 + 1)«5»hy:Real.nthRoot 100 ↑19 = 19 ^ (↑100)⁻¹ := 
  id
    (Eq.mpr (id (congrArg (fun _a => _a = 19 ^ (↑100)⁻¹) (if_pos (of_decide_eq_true (id (Eq.refl true))))))
      (of_eq_true
        (Eq.trans
          (Eq.trans
            (congr
              (congrArg Eq
                (Eq.trans
                  (congr
                    (congrArg HPow.hPow
                      (Mathlib.Meta.NormNum.IsNat.to_eq
                        (Mathlib.Meta.NormNum.isNat_natCast 19 19 (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 19)))
                        (Eq.refl 19)))
                    (Mathlib.Meta.NormNum.IsNNRat.to_eq
                      (Mathlib.Meta.NormNum.isNNRat_inv_pos
                        (Mathlib.Meta.NormNum.IsNat.to_isNNRat
                          (Mathlib.Meta.NormNum.isNat_natCast 100 100
                            (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 100)))))
                      Nat.cast_one (Eq.refl 100)))
                  (congrArg (HPow.hPow 19)
                    (Mathlib.Meta.NormNum.IsNNRat.to_eq
                      (Mathlib.Meta.NormNum.isNNRat_div
                        (Mathlib.Meta.NormNum.isNNRat_mul (Eq.refl HMul.hMul)
                          (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one))
                          (Mathlib.Meta.NormNum.isNNRat_inv_pos
                            (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 100))))
                          (Eq.refl (Nat.mul 1 1)) (Eq.refl 100)))
                      Nat.cast_one (Eq.refl 100)))))
              (Eq.trans
                (congrArg (HPow.hPow 19)
                  (Mathlib.Meta.NormNum.IsNNRat.to_eq
                    (Mathlib.Meta.NormNum.isNNRat_inv_pos
                      (Mathlib.Meta.NormNum.IsNat.to_isNNRat
                        (Mathlib.Meta.NormNum.isNat_natCast 100 100 (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 100)))))
                    Nat.cast_one (Eq.refl 100)))
                (congrArg (HPow.hPow 19)
                  (Mathlib.Meta.NormNum.IsNNRat.to_eq
                    (Mathlib.Meta.NormNum.isNNRat_div
                      (Mathlib.Meta.NormNum.isNNRat_mul (Eq.refl HMul.hMul)
                        (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one))
                        (Mathlib.Meta.NormNum.isNNRat_inv_pos
                          (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 100))))
                        (Eq.refl (Nat.mul 1 1)) (Eq.refl 100)))
                    Nat.cast_one (Eq.refl 100)))))
            (eq_self (19 ^ (1 / 100))))
          (eq_true True.intro))))h100:Real.nthRoot 100 ↑19 ^ 100 = 19 := 
  Eq.mpr (id (congrArg (fun _a => _a ^ 100 = 19) hy))
    (Real.rpow_inv_natCast_pow
      (Mathlib.Meta.NormNum.isNat_le_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)
        (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 19)) (Eq.refl true))
      (Mathlib.Meta.NormNum.isNat_eq_false (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 100))
        (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 0)) (Eq.refl false)))hb:Real.nthRoot 100 ↑19 ^ 74 ≤ 9 := 
  le_of_pow_le_pow_left₀
    (Mathlib.Meta.NormNum.isNat_eq_false (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 100))
      (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 0)) (Eq.refl false))
    (Mathlib.Meta.NormNum.isNat_le_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)
      (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 9)) (Eq.refl true))
    (have e :=
      Eq.mpr
        (id
          (congrArg (fun _a => _a = (Real.nthRoot 100 ↑19 ^ 100) ^ 74) (Eq.symm (pow_mul (Real.nthRoot 100 ↑19) 74 100))))
        (Eq.mpr
          (id
            (congrArg (fun _a => Real.nthRoot 100 ↑19 ^ (74 * 100) = _a)
              (Eq.symm (pow_mul (Real.nthRoot 100 ↑19) 100 74))))
          (Eq.mpr (id (congrArg (fun _a => Real.nthRoot 100 ↑19 ^ _a = Real.nthRoot 100 ↑19 ^ _a) (Nat.mul_comm 74 100)))
            (Eq.refl (Real.nthRoot 100 ↑19 ^ (100 * 74)))));
    Eq.mpr (id (congrArg (fun _a => _a ≤ 9 ^ 100) e))
      (Eq.mpr (id (congrArg (fun _a => _a ^ 74 ≤ 9 ^ 100) h100))
        (Mathlib.Meta.NormNum.isNat_le_true
          (Mathlib.Meta.NormNum.isNat_pow (Eq.refl HPow.hPow) (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 19))
            (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 74))
            (Mathlib.Meta.NormNum.IsNatPowT.run
              (Mathlib.Meta.NormNum.IsNatPowT.trans
                (Mathlib.Meta.NormNum.IsNatPowT.trans
                  (Mathlib.Meta.NormNum.IsNatPowT.trans Mathlib.Meta.NormNum.IsNatPowT.bit0
                    Mathlib.Meta.NormNum.IsNatPowT.bit0)
                  Mathlib.Meta.NormNum.IsNatPowT.bit1)
                (Mathlib.Meta.NormNum.IsNatPowT.trans
                  (Mathlib.Meta.NormNum.IsNatPowT.trans Mathlib.Meta.NormNum.IsNatPowT.bit0
                    Mathlib.Meta.NormNum.IsNatPowT.bit1)
                  Mathlib.Meta.NormNum.IsNatPowT.bit0))))
          (Mathlib.Meta.NormNum.isNat_pow (Eq.refl HPow.hPow) (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 9))
            (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 100))
            (Mathlib.Meta.NormNum.IsNatPowT.run
              (Mathlib.Meta.NormNum.IsNatPowT.trans
                (Mathlib.Meta.NormNum.IsNatPowT.trans
                  (Mathlib.Meta.NormNum.IsNatPowT.trans Mathlib.Meta.NormNum.IsNatPowT.bit1
                    Mathlib.Meta.NormNum.IsNatPowT.bit0)
                  Mathlib.Meta.NormNum.IsNatPowT.bit0)
                (Mathlib.Meta.NormNum.IsNatPowT.trans
                  (Mathlib.Meta.NormNum.IsNatPowT.trans Mathlib.Meta.NormNum.IsNatPowT.bit1
                    Mathlib.Meta.NormNum.IsNatPowT.bit0)
                  Mathlib.Meta.NormNum.IsNatPowT.bit0))))
          (Eq.refl true))))k:ℕhk:↑5 < 1 + Real.nthRoot 100 ↑19 ^ 74hk10:↑5 < 10hk10':5 < 10⊢ ¬Nat.Prime (19 * 5 + 1)«6»hy:Real.nthRoot 100 ↑19 = 19 ^ (↑100)⁻¹ := 
  id
    (Eq.mpr (id (congrArg (fun _a => _a = 19 ^ (↑100)⁻¹) (if_pos (of_decide_eq_true (id (Eq.refl true))))))
      (of_eq_true
        (Eq.trans
          (Eq.trans
            (congr
              (congrArg Eq
                (Eq.trans
                  (congr
                    (congrArg HPow.hPow
                      (Mathlib.Meta.NormNum.IsNat.to_eq
                        (Mathlib.Meta.NormNum.isNat_natCast 19 19 (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 19)))
                        (Eq.refl 19)))
                    (Mathlib.Meta.NormNum.IsNNRat.to_eq
                      (Mathlib.Meta.NormNum.isNNRat_inv_pos
                        (Mathlib.Meta.NormNum.IsNat.to_isNNRat
                          (Mathlib.Meta.NormNum.isNat_natCast 100 100
                            (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 100)))))
                      Nat.cast_one (Eq.refl 100)))
                  (congrArg (HPow.hPow 19)
                    (Mathlib.Meta.NormNum.IsNNRat.to_eq
                      (Mathlib.Meta.NormNum.isNNRat_div
                        (Mathlib.Meta.NormNum.isNNRat_mul (Eq.refl HMul.hMul)
                          (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one))
                          (Mathlib.Meta.NormNum.isNNRat_inv_pos
                            (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 100))))
                          (Eq.refl (Nat.mul 1 1)) (Eq.refl 100)))
                      Nat.cast_one (Eq.refl 100)))))
              (Eq.trans
                (congrArg (HPow.hPow 19)
                  (Mathlib.Meta.NormNum.IsNNRat.to_eq
                    (Mathlib.Meta.NormNum.isNNRat_inv_pos
                      (Mathlib.Meta.NormNum.IsNat.to_isNNRat
                        (Mathlib.Meta.NormNum.isNat_natCast 100 100 (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 100)))))
                    Nat.cast_one (Eq.refl 100)))
                (congrArg (HPow.hPow 19)
                  (Mathlib.Meta.NormNum.IsNNRat.to_eq
                    (Mathlib.Meta.NormNum.isNNRat_div
                      (Mathlib.Meta.NormNum.isNNRat_mul (Eq.refl HMul.hMul)
                        (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one))
                        (Mathlib.Meta.NormNum.isNNRat_inv_pos
                          (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 100))))
                        (Eq.refl (Nat.mul 1 1)) (Eq.refl 100)))
                    Nat.cast_one (Eq.refl 100)))))
            (eq_self (19 ^ (1 / 100))))
          (eq_true True.intro))))h100:Real.nthRoot 100 ↑19 ^ 100 = 19 := 
  Eq.mpr (id (congrArg (fun _a => _a ^ 100 = 19) hy))
    (Real.rpow_inv_natCast_pow
      (Mathlib.Meta.NormNum.isNat_le_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)
        (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 19)) (Eq.refl true))
      (Mathlib.Meta.NormNum.isNat_eq_false (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 100))
        (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 0)) (Eq.refl false)))hb:Real.nthRoot 100 ↑19 ^ 74 ≤ 9 := 
  le_of_pow_le_pow_left₀
    (Mathlib.Meta.NormNum.isNat_eq_false (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 100))
      (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 0)) (Eq.refl false))
    (Mathlib.Meta.NormNum.isNat_le_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)
      (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 9)) (Eq.refl true))
    (have e :=
      Eq.mpr
        (id
          (congrArg (fun _a => _a = (Real.nthRoot 100 ↑19 ^ 100) ^ 74) (Eq.symm (pow_mul (Real.nthRoot 100 ↑19) 74 100))))
        (Eq.mpr
          (id
            (congrArg (fun _a => Real.nthRoot 100 ↑19 ^ (74 * 100) = _a)
              (Eq.symm (pow_mul (Real.nthRoot 100 ↑19) 100 74))))
          (Eq.mpr (id (congrArg (fun _a => Real.nthRoot 100 ↑19 ^ _a = Real.nthRoot 100 ↑19 ^ _a) (Nat.mul_comm 74 100)))
            (Eq.refl (Real.nthRoot 100 ↑19 ^ (100 * 74)))));
    Eq.mpr (id (congrArg (fun _a => _a ≤ 9 ^ 100) e))
      (Eq.mpr (id (congrArg (fun _a => _a ^ 74 ≤ 9 ^ 100) h100))
        (Mathlib.Meta.NormNum.isNat_le_true
          (Mathlib.Meta.NormNum.isNat_pow (Eq.refl HPow.hPow) (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 19))
            (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 74))
            (Mathlib.Meta.NormNum.IsNatPowT.run
              (Mathlib.Meta.NormNum.IsNatPowT.trans
                (Mathlib.Meta.NormNum.IsNatPowT.trans
                  (Mathlib.Meta.NormNum.IsNatPowT.trans Mathlib.Meta.NormNum.IsNatPowT.bit0
                    Mathlib.Meta.NormNum.IsNatPowT.bit0)
                  Mathlib.Meta.NormNum.IsNatPowT.bit1)
                (Mathlib.Meta.NormNum.IsNatPowT.trans
                  (Mathlib.Meta.NormNum.IsNatPowT.trans Mathlib.Meta.NormNum.IsNatPowT.bit0
                    Mathlib.Meta.NormNum.IsNatPowT.bit1)
                  Mathlib.Meta.NormNum.IsNatPowT.bit0))))
          (Mathlib.Meta.NormNum.isNat_pow (Eq.refl HPow.hPow) (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 9))
            (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 100))
            (Mathlib.Meta.NormNum.IsNatPowT.run
              (Mathlib.Meta.NormNum.IsNatPowT.trans
                (Mathlib.Meta.NormNum.IsNatPowT.trans
                  (Mathlib.Meta.NormNum.IsNatPowT.trans Mathlib.Meta.NormNum.IsNatPowT.bit1
                    Mathlib.Meta.NormNum.IsNatPowT.bit0)
                  Mathlib.Meta.NormNum.IsNatPowT.bit0)
                (Mathlib.Meta.NormNum.IsNatPowT.trans
                  (Mathlib.Meta.NormNum.IsNatPowT.trans Mathlib.Meta.NormNum.IsNatPowT.bit1
                    Mathlib.Meta.NormNum.IsNatPowT.bit0)
                  Mathlib.Meta.NormNum.IsNatPowT.bit0))))
          (Eq.refl true))))k:ℕhk:↑6 < 1 + Real.nthRoot 100 ↑19 ^ 74hk10:↑6 < 10hk10':6 < 10⊢ ¬Nat.Prime (19 * 6 + 1)«7»hy:Real.nthRoot 100 ↑19 = 19 ^ (↑100)⁻¹ := 
  id
    (Eq.mpr (id (congrArg (fun _a => _a = 19 ^ (↑100)⁻¹) (if_pos (of_decide_eq_true (id (Eq.refl true))))))
      (of_eq_true
        (Eq.trans
          (Eq.trans
            (congr
              (congrArg Eq
                (Eq.trans
                  (congr
                    (congrArg HPow.hPow
                      (Mathlib.Meta.NormNum.IsNat.to_eq
                        (Mathlib.Meta.NormNum.isNat_natCast 19 19 (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 19)))
                        (Eq.refl 19)))
                    (Mathlib.Meta.NormNum.IsNNRat.to_eq
                      (Mathlib.Meta.NormNum.isNNRat_inv_pos
                        (Mathlib.Meta.NormNum.IsNat.to_isNNRat
                          (Mathlib.Meta.NormNum.isNat_natCast 100 100
                            (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 100)))))
                      Nat.cast_one (Eq.refl 100)))
                  (congrArg (HPow.hPow 19)
                    (Mathlib.Meta.NormNum.IsNNRat.to_eq
                      (Mathlib.Meta.NormNum.isNNRat_div
                        (Mathlib.Meta.NormNum.isNNRat_mul (Eq.refl HMul.hMul)
                          (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one))
                          (Mathlib.Meta.NormNum.isNNRat_inv_pos
                            (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 100))))
                          (Eq.refl (Nat.mul 1 1)) (Eq.refl 100)))
                      Nat.cast_one (Eq.refl 100)))))
              (Eq.trans
                (congrArg (HPow.hPow 19)
                  (Mathlib.Meta.NormNum.IsNNRat.to_eq
                    (Mathlib.Meta.NormNum.isNNRat_inv_pos
                      (Mathlib.Meta.NormNum.IsNat.to_isNNRat
                        (Mathlib.Meta.NormNum.isNat_natCast 100 100 (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 100)))))
                    Nat.cast_one (Eq.refl 100)))
                (congrArg (HPow.hPow 19)
                  (Mathlib.Meta.NormNum.IsNNRat.to_eq
                    (Mathlib.Meta.NormNum.isNNRat_div
                      (Mathlib.Meta.NormNum.isNNRat_mul (Eq.refl HMul.hMul)
                        (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one))
                        (Mathlib.Meta.NormNum.isNNRat_inv_pos
                          (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 100))))
                        (Eq.refl (Nat.mul 1 1)) (Eq.refl 100)))
                    Nat.cast_one (Eq.refl 100)))))
            (eq_self (19 ^ (1 / 100))))
          (eq_true True.intro))))h100:Real.nthRoot 100 ↑19 ^ 100 = 19 := 
  Eq.mpr (id (congrArg (fun _a => _a ^ 100 = 19) hy))
    (Real.rpow_inv_natCast_pow
      (Mathlib.Meta.NormNum.isNat_le_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)
        (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 19)) (Eq.refl true))
      (Mathlib.Meta.NormNum.isNat_eq_false (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 100))
        (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 0)) (Eq.refl false)))hb:Real.nthRoot 100 ↑19 ^ 74 ≤ 9 := 
  le_of_pow_le_pow_left₀
    (Mathlib.Meta.NormNum.isNat_eq_false (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 100))
      (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 0)) (Eq.refl false))
    (Mathlib.Meta.NormNum.isNat_le_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)
      (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 9)) (Eq.refl true))
    (have e :=
      Eq.mpr
        (id
          (congrArg (fun _a => _a = (Real.nthRoot 100 ↑19 ^ 100) ^ 74) (Eq.symm (pow_mul (Real.nthRoot 100 ↑19) 74 100))))
        (Eq.mpr
          (id
            (congrArg (fun _a => Real.nthRoot 100 ↑19 ^ (74 * 100) = _a)
              (Eq.symm (pow_mul (Real.nthRoot 100 ↑19) 100 74))))
          (Eq.mpr (id (congrArg (fun _a => Real.nthRoot 100 ↑19 ^ _a = Real.nthRoot 100 ↑19 ^ _a) (Nat.mul_comm 74 100)))
            (Eq.refl (Real.nthRoot 100 ↑19 ^ (100 * 74)))));
    Eq.mpr (id (congrArg (fun _a => _a ≤ 9 ^ 100) e))
      (Eq.mpr (id (congrArg (fun _a => _a ^ 74 ≤ 9 ^ 100) h100))
        (Mathlib.Meta.NormNum.isNat_le_true
          (Mathlib.Meta.NormNum.isNat_pow (Eq.refl HPow.hPow) (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 19))
            (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 74))
            (Mathlib.Meta.NormNum.IsNatPowT.run
              (Mathlib.Meta.NormNum.IsNatPowT.trans
                (Mathlib.Meta.NormNum.IsNatPowT.trans
                  (Mathlib.Meta.NormNum.IsNatPowT.trans Mathlib.Meta.NormNum.IsNatPowT.bit0
                    Mathlib.Meta.NormNum.IsNatPowT.bit0)
                  Mathlib.Meta.NormNum.IsNatPowT.bit1)
                (Mathlib.Meta.NormNum.IsNatPowT.trans
                  (Mathlib.Meta.NormNum.IsNatPowT.trans Mathlib.Meta.NormNum.IsNatPowT.bit0
                    Mathlib.Meta.NormNum.IsNatPowT.bit1)
                  Mathlib.Meta.NormNum.IsNatPowT.bit0))))
          (Mathlib.Meta.NormNum.isNat_pow (Eq.refl HPow.hPow) (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 9))
            (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 100))
            (Mathlib.Meta.NormNum.IsNatPowT.run
              (Mathlib.Meta.NormNum.IsNatPowT.trans
                (Mathlib.Meta.NormNum.IsNatPowT.trans
                  (Mathlib.Meta.NormNum.IsNatPowT.trans Mathlib.Meta.NormNum.IsNatPowT.bit1
                    Mathlib.Meta.NormNum.IsNatPowT.bit0)
                  Mathlib.Meta.NormNum.IsNatPowT.bit0)
                (Mathlib.Meta.NormNum.IsNatPowT.trans
                  (Mathlib.Meta.NormNum.IsNatPowT.trans Mathlib.Meta.NormNum.IsNatPowT.bit1
                    Mathlib.Meta.NormNum.IsNatPowT.bit0)
                  Mathlib.Meta.NormNum.IsNatPowT.bit0))))
          (Eq.refl true))))k:ℕhk:↑7 < 1 + Real.nthRoot 100 ↑19 ^ 74hk10:↑7 < 10hk10':7 < 10⊢ ¬Nat.Prime (19 * 7 + 1)«8»hy:Real.nthRoot 100 ↑19 = 19 ^ (↑100)⁻¹ := 
  id
    (Eq.mpr (id (congrArg (fun _a => _a = 19 ^ (↑100)⁻¹) (if_pos (of_decide_eq_true (id (Eq.refl true))))))
      (of_eq_true
        (Eq.trans
          (Eq.trans
            (congr
              (congrArg Eq
                (Eq.trans
                  (congr
                    (congrArg HPow.hPow
                      (Mathlib.Meta.NormNum.IsNat.to_eq
                        (Mathlib.Meta.NormNum.isNat_natCast 19 19 (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 19)))
                        (Eq.refl 19)))
                    (Mathlib.Meta.NormNum.IsNNRat.to_eq
                      (Mathlib.Meta.NormNum.isNNRat_inv_pos
                        (Mathlib.Meta.NormNum.IsNat.to_isNNRat
                          (Mathlib.Meta.NormNum.isNat_natCast 100 100
                            (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 100)))))
                      Nat.cast_one (Eq.refl 100)))
                  (congrArg (HPow.hPow 19)
                    (Mathlib.Meta.NormNum.IsNNRat.to_eq
                      (Mathlib.Meta.NormNum.isNNRat_div
                        (Mathlib.Meta.NormNum.isNNRat_mul (Eq.refl HMul.hMul)
                          (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one))
                          (Mathlib.Meta.NormNum.isNNRat_inv_pos
                            (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 100))))
                          (Eq.refl (Nat.mul 1 1)) (Eq.refl 100)))
                      Nat.cast_one (Eq.refl 100)))))
              (Eq.trans
                (congrArg (HPow.hPow 19)
                  (Mathlib.Meta.NormNum.IsNNRat.to_eq
                    (Mathlib.Meta.NormNum.isNNRat_inv_pos
                      (Mathlib.Meta.NormNum.IsNat.to_isNNRat
                        (Mathlib.Meta.NormNum.isNat_natCast 100 100 (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 100)))))
                    Nat.cast_one (Eq.refl 100)))
                (congrArg (HPow.hPow 19)
                  (Mathlib.Meta.NormNum.IsNNRat.to_eq
                    (Mathlib.Meta.NormNum.isNNRat_div
                      (Mathlib.Meta.NormNum.isNNRat_mul (Eq.refl HMul.hMul)
                        (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one))
                        (Mathlib.Meta.NormNum.isNNRat_inv_pos
                          (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 100))))
                        (Eq.refl (Nat.mul 1 1)) (Eq.refl 100)))
                    Nat.cast_one (Eq.refl 100)))))
            (eq_self (19 ^ (1 / 100))))
          (eq_true True.intro))))h100:Real.nthRoot 100 ↑19 ^ 100 = 19 := 
  Eq.mpr (id (congrArg (fun _a => _a ^ 100 = 19) hy))
    (Real.rpow_inv_natCast_pow
      (Mathlib.Meta.NormNum.isNat_le_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)
        (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 19)) (Eq.refl true))
      (Mathlib.Meta.NormNum.isNat_eq_false (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 100))
        (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 0)) (Eq.refl false)))hb:Real.nthRoot 100 ↑19 ^ 74 ≤ 9 := 
  le_of_pow_le_pow_left₀
    (Mathlib.Meta.NormNum.isNat_eq_false (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 100))
      (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 0)) (Eq.refl false))
    (Mathlib.Meta.NormNum.isNat_le_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)
      (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 9)) (Eq.refl true))
    (have e :=
      Eq.mpr
        (id
          (congrArg (fun _a => _a = (Real.nthRoot 100 ↑19 ^ 100) ^ 74) (Eq.symm (pow_mul (Real.nthRoot 100 ↑19) 74 100))))
        (Eq.mpr
          (id
            (congrArg (fun _a => Real.nthRoot 100 ↑19 ^ (74 * 100) = _a)
              (Eq.symm (pow_mul (Real.nthRoot 100 ↑19) 100 74))))
          (Eq.mpr (id (congrArg (fun _a => Real.nthRoot 100 ↑19 ^ _a = Real.nthRoot 100 ↑19 ^ _a) (Nat.mul_comm 74 100)))
            (Eq.refl (Real.nthRoot 100 ↑19 ^ (100 * 74)))));
    Eq.mpr (id (congrArg (fun _a => _a ≤ 9 ^ 100) e))
      (Eq.mpr (id (congrArg (fun _a => _a ^ 74 ≤ 9 ^ 100) h100))
        (Mathlib.Meta.NormNum.isNat_le_true
          (Mathlib.Meta.NormNum.isNat_pow (Eq.refl HPow.hPow) (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 19))
            (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 74))
            (Mathlib.Meta.NormNum.IsNatPowT.run
              (Mathlib.Meta.NormNum.IsNatPowT.trans
                (Mathlib.Meta.NormNum.IsNatPowT.trans
                  (Mathlib.Meta.NormNum.IsNatPowT.trans Mathlib.Meta.NormNum.IsNatPowT.bit0
                    Mathlib.Meta.NormNum.IsNatPowT.bit0)
                  Mathlib.Meta.NormNum.IsNatPowT.bit1)
                (Mathlib.Meta.NormNum.IsNatPowT.trans
                  (Mathlib.Meta.NormNum.IsNatPowT.trans Mathlib.Meta.NormNum.IsNatPowT.bit0
                    Mathlib.Meta.NormNum.IsNatPowT.bit1)
                  Mathlib.Meta.NormNum.IsNatPowT.bit0))))
          (Mathlib.Meta.NormNum.isNat_pow (Eq.refl HPow.hPow) (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 9))
            (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 100))
            (Mathlib.Meta.NormNum.IsNatPowT.run
              (Mathlib.Meta.NormNum.IsNatPowT.trans
                (Mathlib.Meta.NormNum.IsNatPowT.trans
                  (Mathlib.Meta.NormNum.IsNatPowT.trans Mathlib.Meta.NormNum.IsNatPowT.bit1
                    Mathlib.Meta.NormNum.IsNatPowT.bit0)
                  Mathlib.Meta.NormNum.IsNatPowT.bit0)
                (Mathlib.Meta.NormNum.IsNatPowT.trans
                  (Mathlib.Meta.NormNum.IsNatPowT.trans Mathlib.Meta.NormNum.IsNatPowT.bit1
                    Mathlib.Meta.NormNum.IsNatPowT.bit0)
                  Mathlib.Meta.NormNum.IsNatPowT.bit0))))
          (Eq.refl true))))k:ℕhk:↑8 < 1 + Real.nthRoot 100 ↑19 ^ 74hk10:↑8 < 10hk10':8 < 10⊢ ¬Nat.Prime (19 * 8 + 1)«9»hy:Real.nthRoot 100 ↑19 = 19 ^ (↑100)⁻¹ := 
  id
    (Eq.mpr (id (congrArg (fun _a => _a = 19 ^ (↑100)⁻¹) (if_pos (of_decide_eq_true (id (Eq.refl true))))))
      (of_eq_true
        (Eq.trans
          (Eq.trans
            (congr
              (congrArg Eq
                (Eq.trans
                  (congr
                    (congrArg HPow.hPow
                      (Mathlib.Meta.NormNum.IsNat.to_eq
                        (Mathlib.Meta.NormNum.isNat_natCast 19 19 (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 19)))
                        (Eq.refl 19)))
                    (Mathlib.Meta.NormNum.IsNNRat.to_eq
                      (Mathlib.Meta.NormNum.isNNRat_inv_pos
                        (Mathlib.Meta.NormNum.IsNat.to_isNNRat
                          (Mathlib.Meta.NormNum.isNat_natCast 100 100
                            (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 100)))))
                      Nat.cast_one (Eq.refl 100)))
                  (congrArg (HPow.hPow 19)
                    (Mathlib.Meta.NormNum.IsNNRat.to_eq
                      (Mathlib.Meta.NormNum.isNNRat_div
                        (Mathlib.Meta.NormNum.isNNRat_mul (Eq.refl HMul.hMul)
                          (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one))
                          (Mathlib.Meta.NormNum.isNNRat_inv_pos
                            (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 100))))
                          (Eq.refl (Nat.mul 1 1)) (Eq.refl 100)))
                      Nat.cast_one (Eq.refl 100)))))
              (Eq.trans
                (congrArg (HPow.hPow 19)
                  (Mathlib.Meta.NormNum.IsNNRat.to_eq
                    (Mathlib.Meta.NormNum.isNNRat_inv_pos
                      (Mathlib.Meta.NormNum.IsNat.to_isNNRat
                        (Mathlib.Meta.NormNum.isNat_natCast 100 100 (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 100)))))
                    Nat.cast_one (Eq.refl 100)))
                (congrArg (HPow.hPow 19)
                  (Mathlib.Meta.NormNum.IsNNRat.to_eq
                    (Mathlib.Meta.NormNum.isNNRat_div
                      (Mathlib.Meta.NormNum.isNNRat_mul (Eq.refl HMul.hMul)
                        (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one))
                        (Mathlib.Meta.NormNum.isNNRat_inv_pos
                          (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 100))))
                        (Eq.refl (Nat.mul 1 1)) (Eq.refl 100)))
                    Nat.cast_one (Eq.refl 100)))))
            (eq_self (19 ^ (1 / 100))))
          (eq_true True.intro))))h100:Real.nthRoot 100 ↑19 ^ 100 = 19 := 
  Eq.mpr (id (congrArg (fun _a => _a ^ 100 = 19) hy))
    (Real.rpow_inv_natCast_pow
      (Mathlib.Meta.NormNum.isNat_le_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)
        (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 19)) (Eq.refl true))
      (Mathlib.Meta.NormNum.isNat_eq_false (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 100))
        (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 0)) (Eq.refl false)))hb:Real.nthRoot 100 ↑19 ^ 74 ≤ 9 := 
  le_of_pow_le_pow_left₀
    (Mathlib.Meta.NormNum.isNat_eq_false (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 100))
      (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 0)) (Eq.refl false))
    (Mathlib.Meta.NormNum.isNat_le_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)
      (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 9)) (Eq.refl true))
    (have e :=
      Eq.mpr
        (id
          (congrArg (fun _a => _a = (Real.nthRoot 100 ↑19 ^ 100) ^ 74) (Eq.symm (pow_mul (Real.nthRoot 100 ↑19) 74 100))))
        (Eq.mpr
          (id
            (congrArg (fun _a => Real.nthRoot 100 ↑19 ^ (74 * 100) = _a)
              (Eq.symm (pow_mul (Real.nthRoot 100 ↑19) 100 74))))
          (Eq.mpr (id (congrArg (fun _a => Real.nthRoot 100 ↑19 ^ _a = Real.nthRoot 100 ↑19 ^ _a) (Nat.mul_comm 74 100)))
            (Eq.refl (Real.nthRoot 100 ↑19 ^ (100 * 74)))));
    Eq.mpr (id (congrArg (fun _a => _a ≤ 9 ^ 100) e))
      (Eq.mpr (id (congrArg (fun _a => _a ^ 74 ≤ 9 ^ 100) h100))
        (Mathlib.Meta.NormNum.isNat_le_true
          (Mathlib.Meta.NormNum.isNat_pow (Eq.refl HPow.hPow) (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 19))
            (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 74))
            (Mathlib.Meta.NormNum.IsNatPowT.run
              (Mathlib.Meta.NormNum.IsNatPowT.trans
                (Mathlib.Meta.NormNum.IsNatPowT.trans
                  (Mathlib.Meta.NormNum.IsNatPowT.trans Mathlib.Meta.NormNum.IsNatPowT.bit0
                    Mathlib.Meta.NormNum.IsNatPowT.bit0)
                  Mathlib.Meta.NormNum.IsNatPowT.bit1)
                (Mathlib.Meta.NormNum.IsNatPowT.trans
                  (Mathlib.Meta.NormNum.IsNatPowT.trans Mathlib.Meta.NormNum.IsNatPowT.bit0
                    Mathlib.Meta.NormNum.IsNatPowT.bit1)
                  Mathlib.Meta.NormNum.IsNatPowT.bit0))))
          (Mathlib.Meta.NormNum.isNat_pow (Eq.refl HPow.hPow) (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 9))
            (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 100))
            (Mathlib.Meta.NormNum.IsNatPowT.run
              (Mathlib.Meta.NormNum.IsNatPowT.trans
                (Mathlib.Meta.NormNum.IsNatPowT.trans
                  (Mathlib.Meta.NormNum.IsNatPowT.trans Mathlib.Meta.NormNum.IsNatPowT.bit1
                    Mathlib.Meta.NormNum.IsNatPowT.bit0)
                  Mathlib.Meta.NormNum.IsNatPowT.bit0)
                (Mathlib.Meta.NormNum.IsNatPowT.trans
                  (Mathlib.Meta.NormNum.IsNatPowT.trans Mathlib.Meta.NormNum.IsNatPowT.bit1
                    Mathlib.Meta.NormNum.IsNatPowT.bit0)
                  Mathlib.Meta.NormNum.IsNatPowT.bit0))))
          (Eq.refl true))))k:ℕhk:↑9 < 1 + Real.nthRoot 100 ↑19 ^ 74hk10:↑9 < 10hk10':9 < 10⊢ ¬Nat.Prime (19 * 9 + 1) <;>«0»hy:Real.nthRoot 100 ↑19 = 19 ^ (↑100)⁻¹ := 
  id
    (Eq.mpr (id (congrArg (fun _a => _a = 19 ^ (↑100)⁻¹) (if_pos (of_decide_eq_true (id (Eq.refl true))))))
      (of_eq_true
        (Eq.trans
          (Eq.trans
            (congr
              (congrArg Eq
                (Eq.trans
                  (congr
                    (congrArg HPow.hPow
                      (Mathlib.Meta.NormNum.IsNat.to_eq
                        (Mathlib.Meta.NormNum.isNat_natCast 19 19 (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 19)))
                        (Eq.refl 19)))
                    (Mathlib.Meta.NormNum.IsNNRat.to_eq
                      (Mathlib.Meta.NormNum.isNNRat_inv_pos
                        (Mathlib.Meta.NormNum.IsNat.to_isNNRat
                          (Mathlib.Meta.NormNum.isNat_natCast 100 100
                            (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 100)))))
                      Nat.cast_one (Eq.refl 100)))
                  (congrArg (HPow.hPow 19)
                    (Mathlib.Meta.NormNum.IsNNRat.to_eq
                      (Mathlib.Meta.NormNum.isNNRat_div
                        (Mathlib.Meta.NormNum.isNNRat_mul (Eq.refl HMul.hMul)
                          (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one))
                          (Mathlib.Meta.NormNum.isNNRat_inv_pos
                            (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 100))))
                          (Eq.refl (Nat.mul 1 1)) (Eq.refl 100)))
                      Nat.cast_one (Eq.refl 100)))))
              (Eq.trans
                (congrArg (HPow.hPow 19)
                  (Mathlib.Meta.NormNum.IsNNRat.to_eq
                    (Mathlib.Meta.NormNum.isNNRat_inv_pos
                      (Mathlib.Meta.NormNum.IsNat.to_isNNRat
                        (Mathlib.Meta.NormNum.isNat_natCast 100 100 (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 100)))))
                    Nat.cast_one (Eq.refl 100)))
                (congrArg (HPow.hPow 19)
                  (Mathlib.Meta.NormNum.IsNNRat.to_eq
                    (Mathlib.Meta.NormNum.isNNRat_div
                      (Mathlib.Meta.NormNum.isNNRat_mul (Eq.refl HMul.hMul)
                        (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one))
                        (Mathlib.Meta.NormNum.isNNRat_inv_pos
                          (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 100))))
                        (Eq.refl (Nat.mul 1 1)) (Eq.refl 100)))
                    Nat.cast_one (Eq.refl 100)))))
            (eq_self (19 ^ (1 / 100))))
          (eq_true True.intro))))h100:Real.nthRoot 100 ↑19 ^ 100 = 19 := 
  Eq.mpr (id (congrArg (fun _a => _a ^ 100 = 19) hy))
    (Real.rpow_inv_natCast_pow
      (Mathlib.Meta.NormNum.isNat_le_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)
        (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 19)) (Eq.refl true))
      (Mathlib.Meta.NormNum.isNat_eq_false (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 100))
        (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 0)) (Eq.refl false)))hb:Real.nthRoot 100 ↑19 ^ 74 ≤ 9 := 
  le_of_pow_le_pow_left₀
    (Mathlib.Meta.NormNum.isNat_eq_false (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 100))
      (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 0)) (Eq.refl false))
    (Mathlib.Meta.NormNum.isNat_le_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)
      (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 9)) (Eq.refl true))
    (have e :=
      Eq.mpr
        (id
          (congrArg (fun _a => _a = (Real.nthRoot 100 ↑19 ^ 100) ^ 74) (Eq.symm (pow_mul (Real.nthRoot 100 ↑19) 74 100))))
        (Eq.mpr
          (id
            (congrArg (fun _a => Real.nthRoot 100 ↑19 ^ (74 * 100) = _a)
              (Eq.symm (pow_mul (Real.nthRoot 100 ↑19) 100 74))))
          (Eq.mpr (id (congrArg (fun _a => Real.nthRoot 100 ↑19 ^ _a = Real.nthRoot 100 ↑19 ^ _a) (Nat.mul_comm 74 100)))
            (Eq.refl (Real.nthRoot 100 ↑19 ^ (100 * 74)))));
    Eq.mpr (id (congrArg (fun _a => _a ≤ 9 ^ 100) e))
      (Eq.mpr (id (congrArg (fun _a => _a ^ 74 ≤ 9 ^ 100) h100))
        (Mathlib.Meta.NormNum.isNat_le_true
          (Mathlib.Meta.NormNum.isNat_pow (Eq.refl HPow.hPow) (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 19))
            (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 74))
            (Mathlib.Meta.NormNum.IsNatPowT.run
              (Mathlib.Meta.NormNum.IsNatPowT.trans
                (Mathlib.Meta.NormNum.IsNatPowT.trans
                  (Mathlib.Meta.NormNum.IsNatPowT.trans Mathlib.Meta.NormNum.IsNatPowT.bit0
                    Mathlib.Meta.NormNum.IsNatPowT.bit0)
                  Mathlib.Meta.NormNum.IsNatPowT.bit1)
                (Mathlib.Meta.NormNum.IsNatPowT.trans
                  (Mathlib.Meta.NormNum.IsNatPowT.trans Mathlib.Meta.NormNum.IsNatPowT.bit0
                    Mathlib.Meta.NormNum.IsNatPowT.bit1)
                  Mathlib.Meta.NormNum.IsNatPowT.bit0))))
          (Mathlib.Meta.NormNum.isNat_pow (Eq.refl HPow.hPow) (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 9))
            (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 100))
            (Mathlib.Meta.NormNum.IsNatPowT.run
              (Mathlib.Meta.NormNum.IsNatPowT.trans
                (Mathlib.Meta.NormNum.IsNatPowT.trans
                  (Mathlib.Meta.NormNum.IsNatPowT.trans Mathlib.Meta.NormNum.IsNatPowT.bit1
                    Mathlib.Meta.NormNum.IsNatPowT.bit0)
                  Mathlib.Meta.NormNum.IsNatPowT.bit0)
                (Mathlib.Meta.NormNum.IsNatPowT.trans
                  (Mathlib.Meta.NormNum.IsNatPowT.trans Mathlib.Meta.NormNum.IsNatPowT.bit1
                    Mathlib.Meta.NormNum.IsNatPowT.bit0)
                  Mathlib.Meta.NormNum.IsNatPowT.bit0))))
          (Eq.refl true))))k:ℕhk:↑0 < 1 + Real.nthRoot 100 ↑19 ^ 74hk10:↑0 < 10hk10':0 < 10⊢ ¬Nat.Prime (19 * 0 + 1)«1»hy:Real.nthRoot 100 ↑19 = 19 ^ (↑100)⁻¹ := 
  id
    (Eq.mpr (id (congrArg (fun _a => _a = 19 ^ (↑100)⁻¹) (if_pos (of_decide_eq_true (id (Eq.refl true))))))
      (of_eq_true
        (Eq.trans
          (Eq.trans
            (congr
              (congrArg Eq
                (Eq.trans
                  (congr
                    (congrArg HPow.hPow
                      (Mathlib.Meta.NormNum.IsNat.to_eq
                        (Mathlib.Meta.NormNum.isNat_natCast 19 19 (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 19)))
                        (Eq.refl 19)))
                    (Mathlib.Meta.NormNum.IsNNRat.to_eq
                      (Mathlib.Meta.NormNum.isNNRat_inv_pos
                        (Mathlib.Meta.NormNum.IsNat.to_isNNRat
                          (Mathlib.Meta.NormNum.isNat_natCast 100 100
                            (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 100)))))
                      Nat.cast_one (Eq.refl 100)))
                  (congrArg (HPow.hPow 19)
                    (Mathlib.Meta.NormNum.IsNNRat.to_eq
                      (Mathlib.Meta.NormNum.isNNRat_div
                        (Mathlib.Meta.NormNum.isNNRat_mul (Eq.refl HMul.hMul)
                          (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one))
                          (Mathlib.Meta.NormNum.isNNRat_inv_pos
                            (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 100))))
                          (Eq.refl (Nat.mul 1 1)) (Eq.refl 100)))
                      Nat.cast_one (Eq.refl 100)))))
              (Eq.trans
                (congrArg (HPow.hPow 19)
                  (Mathlib.Meta.NormNum.IsNNRat.to_eq
                    (Mathlib.Meta.NormNum.isNNRat_inv_pos
                      (Mathlib.Meta.NormNum.IsNat.to_isNNRat
                        (Mathlib.Meta.NormNum.isNat_natCast 100 100 (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 100)))))
                    Nat.cast_one (Eq.refl 100)))
                (congrArg (HPow.hPow 19)
                  (Mathlib.Meta.NormNum.IsNNRat.to_eq
                    (Mathlib.Meta.NormNum.isNNRat_div
                      (Mathlib.Meta.NormNum.isNNRat_mul (Eq.refl HMul.hMul)
                        (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one))
                        (Mathlib.Meta.NormNum.isNNRat_inv_pos
                          (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 100))))
                        (Eq.refl (Nat.mul 1 1)) (Eq.refl 100)))
                    Nat.cast_one (Eq.refl 100)))))
            (eq_self (19 ^ (1 / 100))))
          (eq_true True.intro))))h100:Real.nthRoot 100 ↑19 ^ 100 = 19 := 
  Eq.mpr (id (congrArg (fun _a => _a ^ 100 = 19) hy))
    (Real.rpow_inv_natCast_pow
      (Mathlib.Meta.NormNum.isNat_le_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)
        (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 19)) (Eq.refl true))
      (Mathlib.Meta.NormNum.isNat_eq_false (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 100))
        (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 0)) (Eq.refl false)))hb:Real.nthRoot 100 ↑19 ^ 74 ≤ 9 := 
  le_of_pow_le_pow_left₀
    (Mathlib.Meta.NormNum.isNat_eq_false (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 100))
      (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 0)) (Eq.refl false))
    (Mathlib.Meta.NormNum.isNat_le_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)
      (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 9)) (Eq.refl true))
    (have e :=
      Eq.mpr
        (id
          (congrArg (fun _a => _a = (Real.nthRoot 100 ↑19 ^ 100) ^ 74) (Eq.symm (pow_mul (Real.nthRoot 100 ↑19) 74 100))))
        (Eq.mpr
          (id
            (congrArg (fun _a => Real.nthRoot 100 ↑19 ^ (74 * 100) = _a)
              (Eq.symm (pow_mul (Real.nthRoot 100 ↑19) 100 74))))
          (Eq.mpr (id (congrArg (fun _a => Real.nthRoot 100 ↑19 ^ _a = Real.nthRoot 100 ↑19 ^ _a) (Nat.mul_comm 74 100)))
            (Eq.refl (Real.nthRoot 100 ↑19 ^ (100 * 74)))));
    Eq.mpr (id (congrArg (fun _a => _a ≤ 9 ^ 100) e))
      (Eq.mpr (id (congrArg (fun _a => _a ^ 74 ≤ 9 ^ 100) h100))
        (Mathlib.Meta.NormNum.isNat_le_true
          (Mathlib.Meta.NormNum.isNat_pow (Eq.refl HPow.hPow) (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 19))
            (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 74))
            (Mathlib.Meta.NormNum.IsNatPowT.run
              (Mathlib.Meta.NormNum.IsNatPowT.trans
                (Mathlib.Meta.NormNum.IsNatPowT.trans
                  (Mathlib.Meta.NormNum.IsNatPowT.trans Mathlib.Meta.NormNum.IsNatPowT.bit0
                    Mathlib.Meta.NormNum.IsNatPowT.bit0)
                  Mathlib.Meta.NormNum.IsNatPowT.bit1)
                (Mathlib.Meta.NormNum.IsNatPowT.trans
                  (Mathlib.Meta.NormNum.IsNatPowT.trans Mathlib.Meta.NormNum.IsNatPowT.bit0
                    Mathlib.Meta.NormNum.IsNatPowT.bit1)
                  Mathlib.Meta.NormNum.IsNatPowT.bit0))))
          (Mathlib.Meta.NormNum.isNat_pow (Eq.refl HPow.hPow) (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 9))
            (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 100))
            (Mathlib.Meta.NormNum.IsNatPowT.run
              (Mathlib.Meta.NormNum.IsNatPowT.trans
                (Mathlib.Meta.NormNum.IsNatPowT.trans
                  (Mathlib.Meta.NormNum.IsNatPowT.trans Mathlib.Meta.NormNum.IsNatPowT.bit1
                    Mathlib.Meta.NormNum.IsNatPowT.bit0)
                  Mathlib.Meta.NormNum.IsNatPowT.bit0)
                (Mathlib.Meta.NormNum.IsNatPowT.trans
                  (Mathlib.Meta.NormNum.IsNatPowT.trans Mathlib.Meta.NormNum.IsNatPowT.bit1
                    Mathlib.Meta.NormNum.IsNatPowT.bit0)
                  Mathlib.Meta.NormNum.IsNatPowT.bit0))))
          (Eq.refl true))))k:ℕhk:↑1 < 1 + Real.nthRoot 100 ↑19 ^ 74hk10:↑1 < 10hk10':1 < 10⊢ ¬Nat.Prime (19 * 1 + 1)«2»hy:Real.nthRoot 100 ↑19 = 19 ^ (↑100)⁻¹ := 
  id
    (Eq.mpr (id (congrArg (fun _a => _a = 19 ^ (↑100)⁻¹) (if_pos (of_decide_eq_true (id (Eq.refl true))))))
      (of_eq_true
        (Eq.trans
          (Eq.trans
            (congr
              (congrArg Eq
                (Eq.trans
                  (congr
                    (congrArg HPow.hPow
                      (Mathlib.Meta.NormNum.IsNat.to_eq
                        (Mathlib.Meta.NormNum.isNat_natCast 19 19 (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 19)))
                        (Eq.refl 19)))
                    (Mathlib.Meta.NormNum.IsNNRat.to_eq
                      (Mathlib.Meta.NormNum.isNNRat_inv_pos
                        (Mathlib.Meta.NormNum.IsNat.to_isNNRat
                          (Mathlib.Meta.NormNum.isNat_natCast 100 100
                            (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 100)))))
                      Nat.cast_one (Eq.refl 100)))
                  (congrArg (HPow.hPow 19)
                    (Mathlib.Meta.NormNum.IsNNRat.to_eq
                      (Mathlib.Meta.NormNum.isNNRat_div
                        (Mathlib.Meta.NormNum.isNNRat_mul (Eq.refl HMul.hMul)
                          (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one))
                          (Mathlib.Meta.NormNum.isNNRat_inv_pos
                            (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 100))))
                          (Eq.refl (Nat.mul 1 1)) (Eq.refl 100)))
                      Nat.cast_one (Eq.refl 100)))))
              (Eq.trans
                (congrArg (HPow.hPow 19)
                  (Mathlib.Meta.NormNum.IsNNRat.to_eq
                    (Mathlib.Meta.NormNum.isNNRat_inv_pos
                      (Mathlib.Meta.NormNum.IsNat.to_isNNRat
                        (Mathlib.Meta.NormNum.isNat_natCast 100 100 (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 100)))))
                    Nat.cast_one (Eq.refl 100)))
                (congrArg (HPow.hPow 19)
                  (Mathlib.Meta.NormNum.IsNNRat.to_eq
                    (Mathlib.Meta.NormNum.isNNRat_div
                      (Mathlib.Meta.NormNum.isNNRat_mul (Eq.refl HMul.hMul)
                        (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one))
                        (Mathlib.Meta.NormNum.isNNRat_inv_pos
                          (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 100))))
                        (Eq.refl (Nat.mul 1 1)) (Eq.refl 100)))
                    Nat.cast_one (Eq.refl 100)))))
            (eq_self (19 ^ (1 / 100))))
          (eq_true True.intro))))h100:Real.nthRoot 100 ↑19 ^ 100 = 19 := 
  Eq.mpr (id (congrArg (fun _a => _a ^ 100 = 19) hy))
    (Real.rpow_inv_natCast_pow
      (Mathlib.Meta.NormNum.isNat_le_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)
        (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 19)) (Eq.refl true))
      (Mathlib.Meta.NormNum.isNat_eq_false (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 100))
        (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 0)) (Eq.refl false)))hb:Real.nthRoot 100 ↑19 ^ 74 ≤ 9 := 
  le_of_pow_le_pow_left₀
    (Mathlib.Meta.NormNum.isNat_eq_false (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 100))
      (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 0)) (Eq.refl false))
    (Mathlib.Meta.NormNum.isNat_le_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)
      (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 9)) (Eq.refl true))
    (have e :=
      Eq.mpr
        (id
          (congrArg (fun _a => _a = (Real.nthRoot 100 ↑19 ^ 100) ^ 74) (Eq.symm (pow_mul (Real.nthRoot 100 ↑19) 74 100))))
        (Eq.mpr
          (id
            (congrArg (fun _a => Real.nthRoot 100 ↑19 ^ (74 * 100) = _a)
              (Eq.symm (pow_mul (Real.nthRoot 100 ↑19) 100 74))))
          (Eq.mpr (id (congrArg (fun _a => Real.nthRoot 100 ↑19 ^ _a = Real.nthRoot 100 ↑19 ^ _a) (Nat.mul_comm 74 100)))
            (Eq.refl (Real.nthRoot 100 ↑19 ^ (100 * 74)))));
    Eq.mpr (id (congrArg (fun _a => _a ≤ 9 ^ 100) e))
      (Eq.mpr (id (congrArg (fun _a => _a ^ 74 ≤ 9 ^ 100) h100))
        (Mathlib.Meta.NormNum.isNat_le_true
          (Mathlib.Meta.NormNum.isNat_pow (Eq.refl HPow.hPow) (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 19))
            (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 74))
            (Mathlib.Meta.NormNum.IsNatPowT.run
              (Mathlib.Meta.NormNum.IsNatPowT.trans
                (Mathlib.Meta.NormNum.IsNatPowT.trans
                  (Mathlib.Meta.NormNum.IsNatPowT.trans Mathlib.Meta.NormNum.IsNatPowT.bit0
                    Mathlib.Meta.NormNum.IsNatPowT.bit0)
                  Mathlib.Meta.NormNum.IsNatPowT.bit1)
                (Mathlib.Meta.NormNum.IsNatPowT.trans
                  (Mathlib.Meta.NormNum.IsNatPowT.trans Mathlib.Meta.NormNum.IsNatPowT.bit0
                    Mathlib.Meta.NormNum.IsNatPowT.bit1)
                  Mathlib.Meta.NormNum.IsNatPowT.bit0))))
          (Mathlib.Meta.NormNum.isNat_pow (Eq.refl HPow.hPow) (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 9))
            (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 100))
            (Mathlib.Meta.NormNum.IsNatPowT.run
              (Mathlib.Meta.NormNum.IsNatPowT.trans
                (Mathlib.Meta.NormNum.IsNatPowT.trans
                  (Mathlib.Meta.NormNum.IsNatPowT.trans Mathlib.Meta.NormNum.IsNatPowT.bit1
                    Mathlib.Meta.NormNum.IsNatPowT.bit0)
                  Mathlib.Meta.NormNum.IsNatPowT.bit0)
                (Mathlib.Meta.NormNum.IsNatPowT.trans
                  (Mathlib.Meta.NormNum.IsNatPowT.trans Mathlib.Meta.NormNum.IsNatPowT.bit1
                    Mathlib.Meta.NormNum.IsNatPowT.bit0)
                  Mathlib.Meta.NormNum.IsNatPowT.bit0))))
          (Eq.refl true))))k:ℕhk:↑2 < 1 + Real.nthRoot 100 ↑19 ^ 74hk10:↑2 < 10hk10':2 < 10⊢ ¬Nat.Prime (19 * 2 + 1)«3»hy:Real.nthRoot 100 ↑19 = 19 ^ (↑100)⁻¹ := 
  id
    (Eq.mpr (id (congrArg (fun _a => _a = 19 ^ (↑100)⁻¹) (if_pos (of_decide_eq_true (id (Eq.refl true))))))
      (of_eq_true
        (Eq.trans
          (Eq.trans
            (congr
              (congrArg Eq
                (Eq.trans
                  (congr
                    (congrArg HPow.hPow
                      (Mathlib.Meta.NormNum.IsNat.to_eq
                        (Mathlib.Meta.NormNum.isNat_natCast 19 19 (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 19)))
                        (Eq.refl 19)))
                    (Mathlib.Meta.NormNum.IsNNRat.to_eq
                      (Mathlib.Meta.NormNum.isNNRat_inv_pos
                        (Mathlib.Meta.NormNum.IsNat.to_isNNRat
                          (Mathlib.Meta.NormNum.isNat_natCast 100 100
                            (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 100)))))
                      Nat.cast_one (Eq.refl 100)))
                  (congrArg (HPow.hPow 19)
                    (Mathlib.Meta.NormNum.IsNNRat.to_eq
                      (Mathlib.Meta.NormNum.isNNRat_div
                        (Mathlib.Meta.NormNum.isNNRat_mul (Eq.refl HMul.hMul)
                          (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one))
                          (Mathlib.Meta.NormNum.isNNRat_inv_pos
                            (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 100))))
                          (Eq.refl (Nat.mul 1 1)) (Eq.refl 100)))
                      Nat.cast_one (Eq.refl 100)))))
              (Eq.trans
                (congrArg (HPow.hPow 19)
                  (Mathlib.Meta.NormNum.IsNNRat.to_eq
                    (Mathlib.Meta.NormNum.isNNRat_inv_pos
                      (Mathlib.Meta.NormNum.IsNat.to_isNNRat
                        (Mathlib.Meta.NormNum.isNat_natCast 100 100 (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 100)))))
                    Nat.cast_one (Eq.refl 100)))
                (congrArg (HPow.hPow 19)
                  (Mathlib.Meta.NormNum.IsNNRat.to_eq
                    (Mathlib.Meta.NormNum.isNNRat_div
                      (Mathlib.Meta.NormNum.isNNRat_mul (Eq.refl HMul.hMul)
                        (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one))
                        (Mathlib.Meta.NormNum.isNNRat_inv_pos
                          (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 100))))
                        (Eq.refl (Nat.mul 1 1)) (Eq.refl 100)))
                    Nat.cast_one (Eq.refl 100)))))
            (eq_self (19 ^ (1 / 100))))
          (eq_true True.intro))))h100:Real.nthRoot 100 ↑19 ^ 100 = 19 := 
  Eq.mpr (id (congrArg (fun _a => _a ^ 100 = 19) hy))
    (Real.rpow_inv_natCast_pow
      (Mathlib.Meta.NormNum.isNat_le_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)
        (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 19)) (Eq.refl true))
      (Mathlib.Meta.NormNum.isNat_eq_false (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 100))
        (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 0)) (Eq.refl false)))hb:Real.nthRoot 100 ↑19 ^ 74 ≤ 9 := 
  le_of_pow_le_pow_left₀
    (Mathlib.Meta.NormNum.isNat_eq_false (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 100))
      (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 0)) (Eq.refl false))
    (Mathlib.Meta.NormNum.isNat_le_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)
      (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 9)) (Eq.refl true))
    (have e :=
      Eq.mpr
        (id
          (congrArg (fun _a => _a = (Real.nthRoot 100 ↑19 ^ 100) ^ 74) (Eq.symm (pow_mul (Real.nthRoot 100 ↑19) 74 100))))
        (Eq.mpr
          (id
            (congrArg (fun _a => Real.nthRoot 100 ↑19 ^ (74 * 100) = _a)
              (Eq.symm (pow_mul (Real.nthRoot 100 ↑19) 100 74))))
          (Eq.mpr (id (congrArg (fun _a => Real.nthRoot 100 ↑19 ^ _a = Real.nthRoot 100 ↑19 ^ _a) (Nat.mul_comm 74 100)))
            (Eq.refl (Real.nthRoot 100 ↑19 ^ (100 * 74)))));
    Eq.mpr (id (congrArg (fun _a => _a ≤ 9 ^ 100) e))
      (Eq.mpr (id (congrArg (fun _a => _a ^ 74 ≤ 9 ^ 100) h100))
        (Mathlib.Meta.NormNum.isNat_le_true
          (Mathlib.Meta.NormNum.isNat_pow (Eq.refl HPow.hPow) (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 19))
            (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 74))
            (Mathlib.Meta.NormNum.IsNatPowT.run
              (Mathlib.Meta.NormNum.IsNatPowT.trans
                (Mathlib.Meta.NormNum.IsNatPowT.trans
                  (Mathlib.Meta.NormNum.IsNatPowT.trans Mathlib.Meta.NormNum.IsNatPowT.bit0
                    Mathlib.Meta.NormNum.IsNatPowT.bit0)
                  Mathlib.Meta.NormNum.IsNatPowT.bit1)
                (Mathlib.Meta.NormNum.IsNatPowT.trans
                  (Mathlib.Meta.NormNum.IsNatPowT.trans Mathlib.Meta.NormNum.IsNatPowT.bit0
                    Mathlib.Meta.NormNum.IsNatPowT.bit1)
                  Mathlib.Meta.NormNum.IsNatPowT.bit0))))
          (Mathlib.Meta.NormNum.isNat_pow (Eq.refl HPow.hPow) (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 9))
            (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 100))
            (Mathlib.Meta.NormNum.IsNatPowT.run
              (Mathlib.Meta.NormNum.IsNatPowT.trans
                (Mathlib.Meta.NormNum.IsNatPowT.trans
                  (Mathlib.Meta.NormNum.IsNatPowT.trans Mathlib.Meta.NormNum.IsNatPowT.bit1
                    Mathlib.Meta.NormNum.IsNatPowT.bit0)
                  Mathlib.Meta.NormNum.IsNatPowT.bit0)
                (Mathlib.Meta.NormNum.IsNatPowT.trans
                  (Mathlib.Meta.NormNum.IsNatPowT.trans Mathlib.Meta.NormNum.IsNatPowT.bit1
                    Mathlib.Meta.NormNum.IsNatPowT.bit0)
                  Mathlib.Meta.NormNum.IsNatPowT.bit0))))
          (Eq.refl true))))k:ℕhk:↑3 < 1 + Real.nthRoot 100 ↑19 ^ 74hk10:↑3 < 10hk10':3 < 10⊢ ¬Nat.Prime (19 * 3 + 1)«4»hy:Real.nthRoot 100 ↑19 = 19 ^ (↑100)⁻¹ := 
  id
    (Eq.mpr (id (congrArg (fun _a => _a = 19 ^ (↑100)⁻¹) (if_pos (of_decide_eq_true (id (Eq.refl true))))))
      (of_eq_true
        (Eq.trans
          (Eq.trans
            (congr
              (congrArg Eq
                (Eq.trans
                  (congr
                    (congrArg HPow.hPow
                      (Mathlib.Meta.NormNum.IsNat.to_eq
                        (Mathlib.Meta.NormNum.isNat_natCast 19 19 (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 19)))
                        (Eq.refl 19)))
                    (Mathlib.Meta.NormNum.IsNNRat.to_eq
                      (Mathlib.Meta.NormNum.isNNRat_inv_pos
                        (Mathlib.Meta.NormNum.IsNat.to_isNNRat
                          (Mathlib.Meta.NormNum.isNat_natCast 100 100
                            (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 100)))))
                      Nat.cast_one (Eq.refl 100)))
                  (congrArg (HPow.hPow 19)
                    (Mathlib.Meta.NormNum.IsNNRat.to_eq
                      (Mathlib.Meta.NormNum.isNNRat_div
                        (Mathlib.Meta.NormNum.isNNRat_mul (Eq.refl HMul.hMul)
                          (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one))
                          (Mathlib.Meta.NormNum.isNNRat_inv_pos
                            (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 100))))
                          (Eq.refl (Nat.mul 1 1)) (Eq.refl 100)))
                      Nat.cast_one (Eq.refl 100)))))
              (Eq.trans
                (congrArg (HPow.hPow 19)
                  (Mathlib.Meta.NormNum.IsNNRat.to_eq
                    (Mathlib.Meta.NormNum.isNNRat_inv_pos
                      (Mathlib.Meta.NormNum.IsNat.to_isNNRat
                        (Mathlib.Meta.NormNum.isNat_natCast 100 100 (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 100)))))
                    Nat.cast_one (Eq.refl 100)))
                (congrArg (HPow.hPow 19)
                  (Mathlib.Meta.NormNum.IsNNRat.to_eq
                    (Mathlib.Meta.NormNum.isNNRat_div
                      (Mathlib.Meta.NormNum.isNNRat_mul (Eq.refl HMul.hMul)
                        (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one))
                        (Mathlib.Meta.NormNum.isNNRat_inv_pos
                          (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 100))))
                        (Eq.refl (Nat.mul 1 1)) (Eq.refl 100)))
                    Nat.cast_one (Eq.refl 100)))))
            (eq_self (19 ^ (1 / 100))))
          (eq_true True.intro))))h100:Real.nthRoot 100 ↑19 ^ 100 = 19 := 
  Eq.mpr (id (congrArg (fun _a => _a ^ 100 = 19) hy))
    (Real.rpow_inv_natCast_pow
      (Mathlib.Meta.NormNum.isNat_le_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)
        (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 19)) (Eq.refl true))
      (Mathlib.Meta.NormNum.isNat_eq_false (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 100))
        (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 0)) (Eq.refl false)))hb:Real.nthRoot 100 ↑19 ^ 74 ≤ 9 := 
  le_of_pow_le_pow_left₀
    (Mathlib.Meta.NormNum.isNat_eq_false (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 100))
      (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 0)) (Eq.refl false))
    (Mathlib.Meta.NormNum.isNat_le_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)
      (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 9)) (Eq.refl true))
    (have e :=
      Eq.mpr
        (id
          (congrArg (fun _a => _a = (Real.nthRoot 100 ↑19 ^ 100) ^ 74) (Eq.symm (pow_mul (Real.nthRoot 100 ↑19) 74 100))))
        (Eq.mpr
          (id
            (congrArg (fun _a => Real.nthRoot 100 ↑19 ^ (74 * 100) = _a)
              (Eq.symm (pow_mul (Real.nthRoot 100 ↑19) 100 74))))
          (Eq.mpr (id (congrArg (fun _a => Real.nthRoot 100 ↑19 ^ _a = Real.nthRoot 100 ↑19 ^ _a) (Nat.mul_comm 74 100)))
            (Eq.refl (Real.nthRoot 100 ↑19 ^ (100 * 74)))));
    Eq.mpr (id (congrArg (fun _a => _a ≤ 9 ^ 100) e))
      (Eq.mpr (id (congrArg (fun _a => _a ^ 74 ≤ 9 ^ 100) h100))
        (Mathlib.Meta.NormNum.isNat_le_true
          (Mathlib.Meta.NormNum.isNat_pow (Eq.refl HPow.hPow) (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 19))
            (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 74))
            (Mathlib.Meta.NormNum.IsNatPowT.run
              (Mathlib.Meta.NormNum.IsNatPowT.trans
                (Mathlib.Meta.NormNum.IsNatPowT.trans
                  (Mathlib.Meta.NormNum.IsNatPowT.trans Mathlib.Meta.NormNum.IsNatPowT.bit0
                    Mathlib.Meta.NormNum.IsNatPowT.bit0)
                  Mathlib.Meta.NormNum.IsNatPowT.bit1)
                (Mathlib.Meta.NormNum.IsNatPowT.trans
                  (Mathlib.Meta.NormNum.IsNatPowT.trans Mathlib.Meta.NormNum.IsNatPowT.bit0
                    Mathlib.Meta.NormNum.IsNatPowT.bit1)
                  Mathlib.Meta.NormNum.IsNatPowT.bit0))))
          (Mathlib.Meta.NormNum.isNat_pow (Eq.refl HPow.hPow) (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 9))
            (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 100))
            (Mathlib.Meta.NormNum.IsNatPowT.run
              (Mathlib.Meta.NormNum.IsNatPowT.trans
                (Mathlib.Meta.NormNum.IsNatPowT.trans
                  (Mathlib.Meta.NormNum.IsNatPowT.trans Mathlib.Meta.NormNum.IsNatPowT.bit1
                    Mathlib.Meta.NormNum.IsNatPowT.bit0)
                  Mathlib.Meta.NormNum.IsNatPowT.bit0)
                (Mathlib.Meta.NormNum.IsNatPowT.trans
                  (Mathlib.Meta.NormNum.IsNatPowT.trans Mathlib.Meta.NormNum.IsNatPowT.bit1
                    Mathlib.Meta.NormNum.IsNatPowT.bit0)
                  Mathlib.Meta.NormNum.IsNatPowT.bit0))))
          (Eq.refl true))))k:ℕhk:↑4 < 1 + Real.nthRoot 100 ↑19 ^ 74hk10:↑4 < 10hk10':4 < 10⊢ ¬Nat.Prime (19 * 4 + 1)«5»hy:Real.nthRoot 100 ↑19 = 19 ^ (↑100)⁻¹ := 
  id
    (Eq.mpr (id (congrArg (fun _a => _a = 19 ^ (↑100)⁻¹) (if_pos (of_decide_eq_true (id (Eq.refl true))))))
      (of_eq_true
        (Eq.trans
          (Eq.trans
            (congr
              (congrArg Eq
                (Eq.trans
                  (congr
                    (congrArg HPow.hPow
                      (Mathlib.Meta.NormNum.IsNat.to_eq
                        (Mathlib.Meta.NormNum.isNat_natCast 19 19 (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 19)))
                        (Eq.refl 19)))
                    (Mathlib.Meta.NormNum.IsNNRat.to_eq
                      (Mathlib.Meta.NormNum.isNNRat_inv_pos
                        (Mathlib.Meta.NormNum.IsNat.to_isNNRat
                          (Mathlib.Meta.NormNum.isNat_natCast 100 100
                            (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 100)))))
                      Nat.cast_one (Eq.refl 100)))
                  (congrArg (HPow.hPow 19)
                    (Mathlib.Meta.NormNum.IsNNRat.to_eq
                      (Mathlib.Meta.NormNum.isNNRat_div
                        (Mathlib.Meta.NormNum.isNNRat_mul (Eq.refl HMul.hMul)
                          (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one))
                          (Mathlib.Meta.NormNum.isNNRat_inv_pos
                            (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 100))))
                          (Eq.refl (Nat.mul 1 1)) (Eq.refl 100)))
                      Nat.cast_one (Eq.refl 100)))))
              (Eq.trans
                (congrArg (HPow.hPow 19)
                  (Mathlib.Meta.NormNum.IsNNRat.to_eq
                    (Mathlib.Meta.NormNum.isNNRat_inv_pos
                      (Mathlib.Meta.NormNum.IsNat.to_isNNRat
                        (Mathlib.Meta.NormNum.isNat_natCast 100 100 (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 100)))))
                    Nat.cast_one (Eq.refl 100)))
                (congrArg (HPow.hPow 19)
                  (Mathlib.Meta.NormNum.IsNNRat.to_eq
                    (Mathlib.Meta.NormNum.isNNRat_div
                      (Mathlib.Meta.NormNum.isNNRat_mul (Eq.refl HMul.hMul)
                        (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one))
                        (Mathlib.Meta.NormNum.isNNRat_inv_pos
                          (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 100))))
                        (Eq.refl (Nat.mul 1 1)) (Eq.refl 100)))
                    Nat.cast_one (Eq.refl 100)))))
            (eq_self (19 ^ (1 / 100))))
          (eq_true True.intro))))h100:Real.nthRoot 100 ↑19 ^ 100 = 19 := 
  Eq.mpr (id (congrArg (fun _a => _a ^ 100 = 19) hy))
    (Real.rpow_inv_natCast_pow
      (Mathlib.Meta.NormNum.isNat_le_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)
        (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 19)) (Eq.refl true))
      (Mathlib.Meta.NormNum.isNat_eq_false (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 100))
        (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 0)) (Eq.refl false)))hb:Real.nthRoot 100 ↑19 ^ 74 ≤ 9 := 
  le_of_pow_le_pow_left₀
    (Mathlib.Meta.NormNum.isNat_eq_false (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 100))
      (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 0)) (Eq.refl false))
    (Mathlib.Meta.NormNum.isNat_le_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)
      (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 9)) (Eq.refl true))
    (have e :=
      Eq.mpr
        (id
          (congrArg (fun _a => _a = (Real.nthRoot 100 ↑19 ^ 100) ^ 74) (Eq.symm (pow_mul (Real.nthRoot 100 ↑19) 74 100))))
        (Eq.mpr
          (id
            (congrArg (fun _a => Real.nthRoot 100 ↑19 ^ (74 * 100) = _a)
              (Eq.symm (pow_mul (Real.nthRoot 100 ↑19) 100 74))))
          (Eq.mpr (id (congrArg (fun _a => Real.nthRoot 100 ↑19 ^ _a = Real.nthRoot 100 ↑19 ^ _a) (Nat.mul_comm 74 100)))
            (Eq.refl (Real.nthRoot 100 ↑19 ^ (100 * 74)))));
    Eq.mpr (id (congrArg (fun _a => _a ≤ 9 ^ 100) e))
      (Eq.mpr (id (congrArg (fun _a => _a ^ 74 ≤ 9 ^ 100) h100))
        (Mathlib.Meta.NormNum.isNat_le_true
          (Mathlib.Meta.NormNum.isNat_pow (Eq.refl HPow.hPow) (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 19))
            (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 74))
            (Mathlib.Meta.NormNum.IsNatPowT.run
              (Mathlib.Meta.NormNum.IsNatPowT.trans
                (Mathlib.Meta.NormNum.IsNatPowT.trans
                  (Mathlib.Meta.NormNum.IsNatPowT.trans Mathlib.Meta.NormNum.IsNatPowT.bit0
                    Mathlib.Meta.NormNum.IsNatPowT.bit0)
                  Mathlib.Meta.NormNum.IsNatPowT.bit1)
                (Mathlib.Meta.NormNum.IsNatPowT.trans
                  (Mathlib.Meta.NormNum.IsNatPowT.trans Mathlib.Meta.NormNum.IsNatPowT.bit0
                    Mathlib.Meta.NormNum.IsNatPowT.bit1)
                  Mathlib.Meta.NormNum.IsNatPowT.bit0))))
          (Mathlib.Meta.NormNum.isNat_pow (Eq.refl HPow.hPow) (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 9))
            (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 100))
            (Mathlib.Meta.NormNum.IsNatPowT.run
              (Mathlib.Meta.NormNum.IsNatPowT.trans
                (Mathlib.Meta.NormNum.IsNatPowT.trans
                  (Mathlib.Meta.NormNum.IsNatPowT.trans Mathlib.Meta.NormNum.IsNatPowT.bit1
                    Mathlib.Meta.NormNum.IsNatPowT.bit0)
                  Mathlib.Meta.NormNum.IsNatPowT.bit0)
                (Mathlib.Meta.NormNum.IsNatPowT.trans
                  (Mathlib.Meta.NormNum.IsNatPowT.trans Mathlib.Meta.NormNum.IsNatPowT.bit1
                    Mathlib.Meta.NormNum.IsNatPowT.bit0)
                  Mathlib.Meta.NormNum.IsNatPowT.bit0))))
          (Eq.refl true))))k:ℕhk:↑5 < 1 + Real.nthRoot 100 ↑19 ^ 74hk10:↑5 < 10hk10':5 < 10⊢ ¬Nat.Prime (19 * 5 + 1)«6»hy:Real.nthRoot 100 ↑19 = 19 ^ (↑100)⁻¹ := 
  id
    (Eq.mpr (id (congrArg (fun _a => _a = 19 ^ (↑100)⁻¹) (if_pos (of_decide_eq_true (id (Eq.refl true))))))
      (of_eq_true
        (Eq.trans
          (Eq.trans
            (congr
              (congrArg Eq
                (Eq.trans
                  (congr
                    (congrArg HPow.hPow
                      (Mathlib.Meta.NormNum.IsNat.to_eq
                        (Mathlib.Meta.NormNum.isNat_natCast 19 19 (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 19)))
                        (Eq.refl 19)))
                    (Mathlib.Meta.NormNum.IsNNRat.to_eq
                      (Mathlib.Meta.NormNum.isNNRat_inv_pos
                        (Mathlib.Meta.NormNum.IsNat.to_isNNRat
                          (Mathlib.Meta.NormNum.isNat_natCast 100 100
                            (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 100)))))
                      Nat.cast_one (Eq.refl 100)))
                  (congrArg (HPow.hPow 19)
                    (Mathlib.Meta.NormNum.IsNNRat.to_eq
                      (Mathlib.Meta.NormNum.isNNRat_div
                        (Mathlib.Meta.NormNum.isNNRat_mul (Eq.refl HMul.hMul)
                          (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one))
                          (Mathlib.Meta.NormNum.isNNRat_inv_pos
                            (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 100))))
                          (Eq.refl (Nat.mul 1 1)) (Eq.refl 100)))
                      Nat.cast_one (Eq.refl 100)))))
              (Eq.trans
                (congrArg (HPow.hPow 19)
                  (Mathlib.Meta.NormNum.IsNNRat.to_eq
                    (Mathlib.Meta.NormNum.isNNRat_inv_pos
                      (Mathlib.Meta.NormNum.IsNat.to_isNNRat
                        (Mathlib.Meta.NormNum.isNat_natCast 100 100 (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 100)))))
                    Nat.cast_one (Eq.refl 100)))
                (congrArg (HPow.hPow 19)
                  (Mathlib.Meta.NormNum.IsNNRat.to_eq
                    (Mathlib.Meta.NormNum.isNNRat_div
                      (Mathlib.Meta.NormNum.isNNRat_mul (Eq.refl HMul.hMul)
                        (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one))
                        (Mathlib.Meta.NormNum.isNNRat_inv_pos
                          (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 100))))
                        (Eq.refl (Nat.mul 1 1)) (Eq.refl 100)))
                    Nat.cast_one (Eq.refl 100)))))
            (eq_self (19 ^ (1 / 100))))
          (eq_true True.intro))))h100:Real.nthRoot 100 ↑19 ^ 100 = 19 := 
  Eq.mpr (id (congrArg (fun _a => _a ^ 100 = 19) hy))
    (Real.rpow_inv_natCast_pow
      (Mathlib.Meta.NormNum.isNat_le_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)
        (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 19)) (Eq.refl true))
      (Mathlib.Meta.NormNum.isNat_eq_false (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 100))
        (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 0)) (Eq.refl false)))hb:Real.nthRoot 100 ↑19 ^ 74 ≤ 9 := 
  le_of_pow_le_pow_left₀
    (Mathlib.Meta.NormNum.isNat_eq_false (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 100))
      (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 0)) (Eq.refl false))
    (Mathlib.Meta.NormNum.isNat_le_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)
      (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 9)) (Eq.refl true))
    (have e :=
      Eq.mpr
        (id
          (congrArg (fun _a => _a = (Real.nthRoot 100 ↑19 ^ 100) ^ 74) (Eq.symm (pow_mul (Real.nthRoot 100 ↑19) 74 100))))
        (Eq.mpr
          (id
            (congrArg (fun _a => Real.nthRoot 100 ↑19 ^ (74 * 100) = _a)
              (Eq.symm (pow_mul (Real.nthRoot 100 ↑19) 100 74))))
          (Eq.mpr (id (congrArg (fun _a => Real.nthRoot 100 ↑19 ^ _a = Real.nthRoot 100 ↑19 ^ _a) (Nat.mul_comm 74 100)))
            (Eq.refl (Real.nthRoot 100 ↑19 ^ (100 * 74)))));
    Eq.mpr (id (congrArg (fun _a => _a ≤ 9 ^ 100) e))
      (Eq.mpr (id (congrArg (fun _a => _a ^ 74 ≤ 9 ^ 100) h100))
        (Mathlib.Meta.NormNum.isNat_le_true
          (Mathlib.Meta.NormNum.isNat_pow (Eq.refl HPow.hPow) (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 19))
            (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 74))
            (Mathlib.Meta.NormNum.IsNatPowT.run
              (Mathlib.Meta.NormNum.IsNatPowT.trans
                (Mathlib.Meta.NormNum.IsNatPowT.trans
                  (Mathlib.Meta.NormNum.IsNatPowT.trans Mathlib.Meta.NormNum.IsNatPowT.bit0
                    Mathlib.Meta.NormNum.IsNatPowT.bit0)
                  Mathlib.Meta.NormNum.IsNatPowT.bit1)
                (Mathlib.Meta.NormNum.IsNatPowT.trans
                  (Mathlib.Meta.NormNum.IsNatPowT.trans Mathlib.Meta.NormNum.IsNatPowT.bit0
                    Mathlib.Meta.NormNum.IsNatPowT.bit1)
                  Mathlib.Meta.NormNum.IsNatPowT.bit0))))
          (Mathlib.Meta.NormNum.isNat_pow (Eq.refl HPow.hPow) (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 9))
            (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 100))
            (Mathlib.Meta.NormNum.IsNatPowT.run
              (Mathlib.Meta.NormNum.IsNatPowT.trans
                (Mathlib.Meta.NormNum.IsNatPowT.trans
                  (Mathlib.Meta.NormNum.IsNatPowT.trans Mathlib.Meta.NormNum.IsNatPowT.bit1
                    Mathlib.Meta.NormNum.IsNatPowT.bit0)
                  Mathlib.Meta.NormNum.IsNatPowT.bit0)
                (Mathlib.Meta.NormNum.IsNatPowT.trans
                  (Mathlib.Meta.NormNum.IsNatPowT.trans Mathlib.Meta.NormNum.IsNatPowT.bit1
                    Mathlib.Meta.NormNum.IsNatPowT.bit0)
                  Mathlib.Meta.NormNum.IsNatPowT.bit0))))
          (Eq.refl true))))k:ℕhk:↑6 < 1 + Real.nthRoot 100 ↑19 ^ 74hk10:↑6 < 10hk10':6 < 10⊢ ¬Nat.Prime (19 * 6 + 1)«7»hy:Real.nthRoot 100 ↑19 = 19 ^ (↑100)⁻¹ := 
  id
    (Eq.mpr (id (congrArg (fun _a => _a = 19 ^ (↑100)⁻¹) (if_pos (of_decide_eq_true (id (Eq.refl true))))))
      (of_eq_true
        (Eq.trans
          (Eq.trans
            (congr
              (congrArg Eq
                (Eq.trans
                  (congr
                    (congrArg HPow.hPow
                      (Mathlib.Meta.NormNum.IsNat.to_eq
                        (Mathlib.Meta.NormNum.isNat_natCast 19 19 (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 19)))
                        (Eq.refl 19)))
                    (Mathlib.Meta.NormNum.IsNNRat.to_eq
                      (Mathlib.Meta.NormNum.isNNRat_inv_pos
                        (Mathlib.Meta.NormNum.IsNat.to_isNNRat
                          (Mathlib.Meta.NormNum.isNat_natCast 100 100
                            (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 100)))))
                      Nat.cast_one (Eq.refl 100)))
                  (congrArg (HPow.hPow 19)
                    (Mathlib.Meta.NormNum.IsNNRat.to_eq
                      (Mathlib.Meta.NormNum.isNNRat_div
                        (Mathlib.Meta.NormNum.isNNRat_mul (Eq.refl HMul.hMul)
                          (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one))
                          (Mathlib.Meta.NormNum.isNNRat_inv_pos
                            (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 100))))
                          (Eq.refl (Nat.mul 1 1)) (Eq.refl 100)))
                      Nat.cast_one (Eq.refl 100)))))
              (Eq.trans
                (congrArg (HPow.hPow 19)
                  (Mathlib.Meta.NormNum.IsNNRat.to_eq
                    (Mathlib.Meta.NormNum.isNNRat_inv_pos
                      (Mathlib.Meta.NormNum.IsNat.to_isNNRat
                        (Mathlib.Meta.NormNum.isNat_natCast 100 100 (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 100)))))
                    Nat.cast_one (Eq.refl 100)))
                (congrArg (HPow.hPow 19)
                  (Mathlib.Meta.NormNum.IsNNRat.to_eq
                    (Mathlib.Meta.NormNum.isNNRat_div
                      (Mathlib.Meta.NormNum.isNNRat_mul (Eq.refl HMul.hMul)
                        (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one))
                        (Mathlib.Meta.NormNum.isNNRat_inv_pos
                          (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 100))))
                        (Eq.refl (Nat.mul 1 1)) (Eq.refl 100)))
                    Nat.cast_one (Eq.refl 100)))))
            (eq_self (19 ^ (1 / 100))))
          (eq_true True.intro))))h100:Real.nthRoot 100 ↑19 ^ 100 = 19 := 
  Eq.mpr (id (congrArg (fun _a => _a ^ 100 = 19) hy))
    (Real.rpow_inv_natCast_pow
      (Mathlib.Meta.NormNum.isNat_le_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)
        (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 19)) (Eq.refl true))
      (Mathlib.Meta.NormNum.isNat_eq_false (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 100))
        (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 0)) (Eq.refl false)))hb:Real.nthRoot 100 ↑19 ^ 74 ≤ 9 := 
  le_of_pow_le_pow_left₀
    (Mathlib.Meta.NormNum.isNat_eq_false (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 100))
      (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 0)) (Eq.refl false))
    (Mathlib.Meta.NormNum.isNat_le_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)
      (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 9)) (Eq.refl true))
    (have e :=
      Eq.mpr
        (id
          (congrArg (fun _a => _a = (Real.nthRoot 100 ↑19 ^ 100) ^ 74) (Eq.symm (pow_mul (Real.nthRoot 100 ↑19) 74 100))))
        (Eq.mpr
          (id
            (congrArg (fun _a => Real.nthRoot 100 ↑19 ^ (74 * 100) = _a)
              (Eq.symm (pow_mul (Real.nthRoot 100 ↑19) 100 74))))
          (Eq.mpr (id (congrArg (fun _a => Real.nthRoot 100 ↑19 ^ _a = Real.nthRoot 100 ↑19 ^ _a) (Nat.mul_comm 74 100)))
            (Eq.refl (Real.nthRoot 100 ↑19 ^ (100 * 74)))));
    Eq.mpr (id (congrArg (fun _a => _a ≤ 9 ^ 100) e))
      (Eq.mpr (id (congrArg (fun _a => _a ^ 74 ≤ 9 ^ 100) h100))
        (Mathlib.Meta.NormNum.isNat_le_true
          (Mathlib.Meta.NormNum.isNat_pow (Eq.refl HPow.hPow) (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 19))
            (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 74))
            (Mathlib.Meta.NormNum.IsNatPowT.run
              (Mathlib.Meta.NormNum.IsNatPowT.trans
                (Mathlib.Meta.NormNum.IsNatPowT.trans
                  (Mathlib.Meta.NormNum.IsNatPowT.trans Mathlib.Meta.NormNum.IsNatPowT.bit0
                    Mathlib.Meta.NormNum.IsNatPowT.bit0)
                  Mathlib.Meta.NormNum.IsNatPowT.bit1)
                (Mathlib.Meta.NormNum.IsNatPowT.trans
                  (Mathlib.Meta.NormNum.IsNatPowT.trans Mathlib.Meta.NormNum.IsNatPowT.bit0
                    Mathlib.Meta.NormNum.IsNatPowT.bit1)
                  Mathlib.Meta.NormNum.IsNatPowT.bit0))))
          (Mathlib.Meta.NormNum.isNat_pow (Eq.refl HPow.hPow) (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 9))
            (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 100))
            (Mathlib.Meta.NormNum.IsNatPowT.run
              (Mathlib.Meta.NormNum.IsNatPowT.trans
                (Mathlib.Meta.NormNum.IsNatPowT.trans
                  (Mathlib.Meta.NormNum.IsNatPowT.trans Mathlib.Meta.NormNum.IsNatPowT.bit1
                    Mathlib.Meta.NormNum.IsNatPowT.bit0)
                  Mathlib.Meta.NormNum.IsNatPowT.bit0)
                (Mathlib.Meta.NormNum.IsNatPowT.trans
                  (Mathlib.Meta.NormNum.IsNatPowT.trans Mathlib.Meta.NormNum.IsNatPowT.bit1
                    Mathlib.Meta.NormNum.IsNatPowT.bit0)
                  Mathlib.Meta.NormNum.IsNatPowT.bit0))))
          (Eq.refl true))))k:ℕhk:↑7 < 1 + Real.nthRoot 100 ↑19 ^ 74hk10:↑7 < 10hk10':7 < 10⊢ ¬Nat.Prime (19 * 7 + 1)«8»hy:Real.nthRoot 100 ↑19 = 19 ^ (↑100)⁻¹ := 
  id
    (Eq.mpr (id (congrArg (fun _a => _a = 19 ^ (↑100)⁻¹) (if_pos (of_decide_eq_true (id (Eq.refl true))))))
      (of_eq_true
        (Eq.trans
          (Eq.trans
            (congr
              (congrArg Eq
                (Eq.trans
                  (congr
                    (congrArg HPow.hPow
                      (Mathlib.Meta.NormNum.IsNat.to_eq
                        (Mathlib.Meta.NormNum.isNat_natCast 19 19 (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 19)))
                        (Eq.refl 19)))
                    (Mathlib.Meta.NormNum.IsNNRat.to_eq
                      (Mathlib.Meta.NormNum.isNNRat_inv_pos
                        (Mathlib.Meta.NormNum.IsNat.to_isNNRat
                          (Mathlib.Meta.NormNum.isNat_natCast 100 100
                            (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 100)))))
                      Nat.cast_one (Eq.refl 100)))
                  (congrArg (HPow.hPow 19)
                    (Mathlib.Meta.NormNum.IsNNRat.to_eq
                      (Mathlib.Meta.NormNum.isNNRat_div
                        (Mathlib.Meta.NormNum.isNNRat_mul (Eq.refl HMul.hMul)
                          (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one))
                          (Mathlib.Meta.NormNum.isNNRat_inv_pos
                            (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 100))))
                          (Eq.refl (Nat.mul 1 1)) (Eq.refl 100)))
                      Nat.cast_one (Eq.refl 100)))))
              (Eq.trans
                (congrArg (HPow.hPow 19)
                  (Mathlib.Meta.NormNum.IsNNRat.to_eq
                    (Mathlib.Meta.NormNum.isNNRat_inv_pos
                      (Mathlib.Meta.NormNum.IsNat.to_isNNRat
                        (Mathlib.Meta.NormNum.isNat_natCast 100 100 (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 100)))))
                    Nat.cast_one (Eq.refl 100)))
                (congrArg (HPow.hPow 19)
                  (Mathlib.Meta.NormNum.IsNNRat.to_eq
                    (Mathlib.Meta.NormNum.isNNRat_div
                      (Mathlib.Meta.NormNum.isNNRat_mul (Eq.refl HMul.hMul)
                        (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one))
                        (Mathlib.Meta.NormNum.isNNRat_inv_pos
                          (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 100))))
                        (Eq.refl (Nat.mul 1 1)) (Eq.refl 100)))
                    Nat.cast_one (Eq.refl 100)))))
            (eq_self (19 ^ (1 / 100))))
          (eq_true True.intro))))h100:Real.nthRoot 100 ↑19 ^ 100 = 19 := 
  Eq.mpr (id (congrArg (fun _a => _a ^ 100 = 19) hy))
    (Real.rpow_inv_natCast_pow
      (Mathlib.Meta.NormNum.isNat_le_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)
        (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 19)) (Eq.refl true))
      (Mathlib.Meta.NormNum.isNat_eq_false (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 100))
        (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 0)) (Eq.refl false)))hb:Real.nthRoot 100 ↑19 ^ 74 ≤ 9 := 
  le_of_pow_le_pow_left₀
    (Mathlib.Meta.NormNum.isNat_eq_false (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 100))
      (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 0)) (Eq.refl false))
    (Mathlib.Meta.NormNum.isNat_le_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)
      (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 9)) (Eq.refl true))
    (have e :=
      Eq.mpr
        (id
          (congrArg (fun _a => _a = (Real.nthRoot 100 ↑19 ^ 100) ^ 74) (Eq.symm (pow_mul (Real.nthRoot 100 ↑19) 74 100))))
        (Eq.mpr
          (id
            (congrArg (fun _a => Real.nthRoot 100 ↑19 ^ (74 * 100) = _a)
              (Eq.symm (pow_mul (Real.nthRoot 100 ↑19) 100 74))))
          (Eq.mpr (id (congrArg (fun _a => Real.nthRoot 100 ↑19 ^ _a = Real.nthRoot 100 ↑19 ^ _a) (Nat.mul_comm 74 100)))
            (Eq.refl (Real.nthRoot 100 ↑19 ^ (100 * 74)))));
    Eq.mpr (id (congrArg (fun _a => _a ≤ 9 ^ 100) e))
      (Eq.mpr (id (congrArg (fun _a => _a ^ 74 ≤ 9 ^ 100) h100))
        (Mathlib.Meta.NormNum.isNat_le_true
          (Mathlib.Meta.NormNum.isNat_pow (Eq.refl HPow.hPow) (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 19))
            (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 74))
            (Mathlib.Meta.NormNum.IsNatPowT.run
              (Mathlib.Meta.NormNum.IsNatPowT.trans
                (Mathlib.Meta.NormNum.IsNatPowT.trans
                  (Mathlib.Meta.NormNum.IsNatPowT.trans Mathlib.Meta.NormNum.IsNatPowT.bit0
                    Mathlib.Meta.NormNum.IsNatPowT.bit0)
                  Mathlib.Meta.NormNum.IsNatPowT.bit1)
                (Mathlib.Meta.NormNum.IsNatPowT.trans
                  (Mathlib.Meta.NormNum.IsNatPowT.trans Mathlib.Meta.NormNum.IsNatPowT.bit0
                    Mathlib.Meta.NormNum.IsNatPowT.bit1)
                  Mathlib.Meta.NormNum.IsNatPowT.bit0))))
          (Mathlib.Meta.NormNum.isNat_pow (Eq.refl HPow.hPow) (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 9))
            (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 100))
            (Mathlib.Meta.NormNum.IsNatPowT.run
              (Mathlib.Meta.NormNum.IsNatPowT.trans
                (Mathlib.Meta.NormNum.IsNatPowT.trans
                  (Mathlib.Meta.NormNum.IsNatPowT.trans Mathlib.Meta.NormNum.IsNatPowT.bit1
                    Mathlib.Meta.NormNum.IsNatPowT.bit0)
                  Mathlib.Meta.NormNum.IsNatPowT.bit0)
                (Mathlib.Meta.NormNum.IsNatPowT.trans
                  (Mathlib.Meta.NormNum.IsNatPowT.trans Mathlib.Meta.NormNum.IsNatPowT.bit1
                    Mathlib.Meta.NormNum.IsNatPowT.bit0)
                  Mathlib.Meta.NormNum.IsNatPowT.bit0))))
          (Eq.refl true))))k:ℕhk:↑8 < 1 + Real.nthRoot 100 ↑19 ^ 74hk10:↑8 < 10hk10':8 < 10⊢ ¬Nat.Prime (19 * 8 + 1)«9»hy:Real.nthRoot 100 ↑19 = 19 ^ (↑100)⁻¹ := 
  id
    (Eq.mpr (id (congrArg (fun _a => _a = 19 ^ (↑100)⁻¹) (if_pos (of_decide_eq_true (id (Eq.refl true))))))
      (of_eq_true
        (Eq.trans
          (Eq.trans
            (congr
              (congrArg Eq
                (Eq.trans
                  (congr
                    (congrArg HPow.hPow
                      (Mathlib.Meta.NormNum.IsNat.to_eq
                        (Mathlib.Meta.NormNum.isNat_natCast 19 19 (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 19)))
                        (Eq.refl 19)))
                    (Mathlib.Meta.NormNum.IsNNRat.to_eq
                      (Mathlib.Meta.NormNum.isNNRat_inv_pos
                        (Mathlib.Meta.NormNum.IsNat.to_isNNRat
                          (Mathlib.Meta.NormNum.isNat_natCast 100 100
                            (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 100)))))
                      Nat.cast_one (Eq.refl 100)))
                  (congrArg (HPow.hPow 19)
                    (Mathlib.Meta.NormNum.IsNNRat.to_eq
                      (Mathlib.Meta.NormNum.isNNRat_div
                        (Mathlib.Meta.NormNum.isNNRat_mul (Eq.refl HMul.hMul)
                          (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one))
                          (Mathlib.Meta.NormNum.isNNRat_inv_pos
                            (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 100))))
                          (Eq.refl (Nat.mul 1 1)) (Eq.refl 100)))
                      Nat.cast_one (Eq.refl 100)))))
              (Eq.trans
                (congrArg (HPow.hPow 19)
                  (Mathlib.Meta.NormNum.IsNNRat.to_eq
                    (Mathlib.Meta.NormNum.isNNRat_inv_pos
                      (Mathlib.Meta.NormNum.IsNat.to_isNNRat
                        (Mathlib.Meta.NormNum.isNat_natCast 100 100 (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 100)))))
                    Nat.cast_one (Eq.refl 100)))
                (congrArg (HPow.hPow 19)
                  (Mathlib.Meta.NormNum.IsNNRat.to_eq
                    (Mathlib.Meta.NormNum.isNNRat_div
                      (Mathlib.Meta.NormNum.isNNRat_mul (Eq.refl HMul.hMul)
                        (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one))
                        (Mathlib.Meta.NormNum.isNNRat_inv_pos
                          (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 100))))
                        (Eq.refl (Nat.mul 1 1)) (Eq.refl 100)))
                    Nat.cast_one (Eq.refl 100)))))
            (eq_self (19 ^ (1 / 100))))
          (eq_true True.intro))))h100:Real.nthRoot 100 ↑19 ^ 100 = 19 := 
  Eq.mpr (id (congrArg (fun _a => _a ^ 100 = 19) hy))
    (Real.rpow_inv_natCast_pow
      (Mathlib.Meta.NormNum.isNat_le_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)
        (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 19)) (Eq.refl true))
      (Mathlib.Meta.NormNum.isNat_eq_false (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 100))
        (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 0)) (Eq.refl false)))hb:Real.nthRoot 100 ↑19 ^ 74 ≤ 9 := 
  le_of_pow_le_pow_left₀
    (Mathlib.Meta.NormNum.isNat_eq_false (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 100))
      (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 0)) (Eq.refl false))
    (Mathlib.Meta.NormNum.isNat_le_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)
      (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 9)) (Eq.refl true))
    (have e :=
      Eq.mpr
        (id
          (congrArg (fun _a => _a = (Real.nthRoot 100 ↑19 ^ 100) ^ 74) (Eq.symm (pow_mul (Real.nthRoot 100 ↑19) 74 100))))
        (Eq.mpr
          (id
            (congrArg (fun _a => Real.nthRoot 100 ↑19 ^ (74 * 100) = _a)
              (Eq.symm (pow_mul (Real.nthRoot 100 ↑19) 100 74))))
          (Eq.mpr (id (congrArg (fun _a => Real.nthRoot 100 ↑19 ^ _a = Real.nthRoot 100 ↑19 ^ _a) (Nat.mul_comm 74 100)))
            (Eq.refl (Real.nthRoot 100 ↑19 ^ (100 * 74)))));
    Eq.mpr (id (congrArg (fun _a => _a ≤ 9 ^ 100) e))
      (Eq.mpr (id (congrArg (fun _a => _a ^ 74 ≤ 9 ^ 100) h100))
        (Mathlib.Meta.NormNum.isNat_le_true
          (Mathlib.Meta.NormNum.isNat_pow (Eq.refl HPow.hPow) (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 19))
            (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 74))
            (Mathlib.Meta.NormNum.IsNatPowT.run
              (Mathlib.Meta.NormNum.IsNatPowT.trans
                (Mathlib.Meta.NormNum.IsNatPowT.trans
                  (Mathlib.Meta.NormNum.IsNatPowT.trans Mathlib.Meta.NormNum.IsNatPowT.bit0
                    Mathlib.Meta.NormNum.IsNatPowT.bit0)
                  Mathlib.Meta.NormNum.IsNatPowT.bit1)
                (Mathlib.Meta.NormNum.IsNatPowT.trans
                  (Mathlib.Meta.NormNum.IsNatPowT.trans Mathlib.Meta.NormNum.IsNatPowT.bit0
                    Mathlib.Meta.NormNum.IsNatPowT.bit1)
                  Mathlib.Meta.NormNum.IsNatPowT.bit0))))
          (Mathlib.Meta.NormNum.isNat_pow (Eq.refl HPow.hPow) (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 9))
            (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 100))
            (Mathlib.Meta.NormNum.IsNatPowT.run
              (Mathlib.Meta.NormNum.IsNatPowT.trans
                (Mathlib.Meta.NormNum.IsNatPowT.trans
                  (Mathlib.Meta.NormNum.IsNatPowT.trans Mathlib.Meta.NormNum.IsNatPowT.bit1
                    Mathlib.Meta.NormNum.IsNatPowT.bit0)
                  Mathlib.Meta.NormNum.IsNatPowT.bit0)
                (Mathlib.Meta.NormNum.IsNatPowT.trans
                  (Mathlib.Meta.NormNum.IsNatPowT.trans Mathlib.Meta.NormNum.IsNatPowT.bit1
                    Mathlib.Meta.NormNum.IsNatPowT.bit0)
                  Mathlib.Meta.NormNum.IsNatPowT.bit0))))
          (Eq.refl true))))k:ℕhk:↑9 < 1 + Real.nthRoot 100 ↑19 ^ 74hk10:↑9 < 10hk10':9 < 10⊢ ¬Nat.Prime (19 * 9 + 1) norm_numAll goals completed! 🐙

Conjecture: $a(n) = O(\log(n)\log(\log(n)))$.

@[category research open, AMS 11]
theorem declaration uses 'sorry'a_isBigO : (fun n ↦ (a n : ℝ)) =O[atTop] (fun n ↦ Real.log n * Real.log (Real.log n)) := by⊢ (fun n => ↑(a n)) =O[atTop] fun n => Real.log ↑n * Real.log (Real.log ↑n)
  sorryAll goals completed! 🐙

Counter-conjecture to a_isBigO: $a(n) / (\log n \log \log n)$ is unbounded.

@[category research open, AMS 11]
theorem declaration uses 'sorry'a_unbounded : ¬BddAbove (Set.range fun n ↦ a n / (Real.log n * Real.log (Real.log n))) := by⊢ ¬BddAbove (Set.range fun n => ↑(a n) / (Real.log ↑n * Real.log (Real.log ↑n)))
  sorryAll goals completed! 🐙


end OeisA34693