/-
Copyright 2026 The Formal Conjectures Authors.
Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at
https://www.apache.org/licenses/LICENSE-2.0
Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
-/
import FormalConjecturesUtil
import FormalConjecturesForMathlib.Data.Real.NearestIntBugeaud Collection of Conjectures and Open Questions: Fractional Parts of Powers
Chapter 10 of the book collects open questions. This file formalizes Problems 10.1, 10.2, 10.3 and the unnumbered conjecture by Waldschmidt.
[Bug12] Bugeaud, Yann. "Distribution modulo one and Diophantine approximation." Vol. 193. Cambridge University Press, 2012. Chapter 10.
[Har19] Hardy, Gr H. "A problem of Diophantine approximation." J. Indian Math. Soc 11 (1919): 162-166.
[Kok45] Koksma, J. F. "Sur la théorie métrique des approximations diophantiques." Indag. Math 7 (1945): 54-70.
[Mah53] Mahler, Kurt. "On the approximation of logarithms of algebraic numbers." Philosophical Transactions of the Royal Society of London. Series A, Mathematical and Physical Sciences 245.898 (1953): 371-398.
Wal03 Waldschmidt, Michel. "Linear independence measures for logarithms of algebraic numbers." Diophantine Approximation: Lectures given at the CIME Summer School held in Cetraro, Italy, June 28–July 6, 2000. Berlin, Heidelberg: Springer Berlin Heidelberg, 2003. 249-344.
namespace Bugeaud01
Problem 10.1. Are there a transcendental number $\alpha$ and a positive real number $\xi$ such that $\lVert \xi \alpha^n \rVert$ tends to~$0$ as~$n$ tends to infinity? [Har19] (Trivial for $|\alpha| < 1$)
@[category research open, AMS 11]
theorem problem_10_1 : answer(sorry) ↔
∃ (α ξ : ℝ), 1 < |α| ∧ Transcendental ℚ α ∧ 0 < ξ ∧
Filter.Tendsto (fun n : ℕ ↦ distToNearestInt (ξ * α ^ n)) Filter.atTop (nhds 0) := ⊢ True ↔
∃ α ξ,
1 < |α| ∧ Transcendental ℚ α ∧ 0 < ξ ∧ Filter.Tendsto (fun n => distToNearestInt (ξ * α ^ n)) Filter.atTop (nhds 0)
All goals completed! 🐙
Problem 10.2. To prove that $\lVert e^n \rVert$ does not tend to 0 as n tends to infinity.
@[category research open, AMS 11]
theorem problem_10_2 :
¬ Filter.Tendsto (fun n : ℕ ↦ distToNearestInt (Real.exp n)) Filter.atTop (nhds 0) := ⊢ ¬Filter.Tendsto (fun n => distToNearestInt (Real.exp ↑n)) Filter.atTop (nhds 0)
All goals completed! 🐙
Problem 10.3. To prove that there exists a positive real number~$c$ such that $\lVert e^n \rVert > e^{−cn}$, for every~$n \ge 1$. Posed by Mahler [Mah53].
@[category research open, AMS 11]
theorem problem_10_3 :
∃ c : ℝ, 0 < c ∧ ∀ n : ℕ, 1 ≤ n → Real.exp (-c * n) < distToNearestInt (Real.exp n) := ⊢ ∃ c, 0 < c ∧ ∀ (n : ℕ), 1 ≤ n → Real.exp (-c * ↑n) < distToNearestInt (Real.exp ↑n)
All goals completed! 🐙
Waldschmidt [Wal03] conjectured that a stronger result holds, namely that there exists a positive real number~$c$ such that $\lVert e^n \rVert > n^{-c}$ for every~$n \ge 2$. This is supported by metrical results [Kok45].
Note: the bound $n^{-c}$ equals $1$ when $n = 1$ for all $c$, while the distance to the nearest integer is always at most $1/2$, so the conjecture must start at $n \ge 2$.
@[category research open, AMS 11]
theorem waldschmidt :
∃ c : ℝ, 0 < c ∧ ∀ n : ℕ, 2 ≤ n → (n : ℝ) ^ (-c) < distToNearestInt (Real.exp n) := ⊢ ∃ c, 0 < c ∧ ∀ (n : ℕ), 2 ≤ n → ↑n ^ (-c) < distToNearestInt (Real.exp ↑n)
All goals completed! 🐙
Waldschmidt's conjecture is stronger than Mahler's: since $\log n \le n$ for $n \ge 1$, the polynomial lower bound $n^{-c}$ dominates the exponential lower bound $e^{-cn}$. For the $n = 1$ case (not covered by Waldschmidt's $n \ge 2$), we choose a larger constant using the numerical bound $\lVert e \rVert = 3 - e > 0$.
@[category test, AMS 11]
theorem problem_10_3_of_waldschmidt (h : type_of% waldschmidt) : type_of% problem_10_3 := h:∃ c, 0 < c ∧ ∀ (n : ℕ), 2 ≤ n → ↑n ^ (-c) < distToNearestInt (Real.exp ↑n)⊢ ∃ c, 0 < c ∧ ∀ (n : ℕ), 1 ≤ n → Real.exp (-c * ↑n) < distToNearestInt (Real.exp ↑n)
c:ℝhc:0 < chyp:∀ (n : ℕ), 2 ≤ n → ↑n ^ (-c) < distToNearestInt (Real.exp ↑n)⊢ ∃ c, 0 < c ∧ ∀ (n : ℕ), 1 ≤ n → Real.exp (-c * ↑n) < distToNearestInt (Real.exp ↑n)
-- distToNearestInt(e) = |e - 3| = 3 - e > 0
have hd_pos : 0 < distToNearestInt (Real.exp 1) := h:∃ c, 0 < c ∧ ∀ (n : ℕ), 2 ≤ n → ↑n ^ (-c) < distToNearestInt (Real.exp ↑n)⊢ ∃ c, 0 < c ∧ ∀ (n : ℕ), 1 ≤ n → Real.exp (-c * ↑n) < distToNearestInt (Real.exp ↑n)
c:ℝhc:0 < chyp:∀ (n : ℕ), 2 ≤ n → ↑n ^ (-c) < distToNearestInt (Real.exp ↑n)⊢ 0 < |Real.exp 1 - 3|
c:ℝhc:0 < chyp:∀ (n : ℕ), 2 ≤ n → ↑n ^ (-c) < distToNearestInt (Real.exp ↑n)⊢ Real.exp 1 - 3 ≠ 0
All goals completed! 🐙
-- Pick c₀ such that exp(-c₀) < distToNearestInt(e); use c' = max c c₀
c:ℝhc:0 < chyp:∀ (n : ℕ), 2 ≤ n → ↑n ^ (-c) < distToNearestInt (Real.exp ↑n)hd_pos:0 < distToNearestInt (Real.exp 1) :=
Eq.mpr
(id
(congrArg (fun x => 0 < |Real.exp 1 - x|)
(Eq.trans (congrArg Int.cast Real.round_exp_one_eq_three) (Int.cast_ofNat 3))))
(Eq.mpr (id (congrArg (fun _a => _a) (propext abs_pos)))
(Not.intro fun a =>
Mathlib.Tactic.Linarith.lt_irrefl
(Eq.mp
(congrArg (fun _a => _a < 0)
(Mathlib.Tactic.Ring.of_eq
(Mathlib.Tactic.Ring.add_congr
(Mathlib.Tactic.Ring.neg_congr
(Mathlib.Tactic.Ring.sub_congr
(Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.atom_pf (Real.exp 1))
(Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 3)))
(Mathlib.Tactic.Ring.sub_pf
(Mathlib.Tactic.Ring.neg_add
(Mathlib.Tactic.Ring.neg_one_mul
(Mathlib.Meta.NormNum.IsInt.to_raw_eq
(Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 3))
(Eq.refl (Int.negOfNat 3)))))
Mathlib.Tactic.Ring.neg_zero)
(Mathlib.Tactic.Ring.add_pf_add_gt (Int.negOfNat 3).rawCast
(Mathlib.Tactic.Ring.add_pf_add_zero (Real.exp 1 ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))))
(Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero))
(Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_zero
(Mathlib.Tactic.Ring.add_pf_add_zero
((Int.negOfNat 3).rawCast + (Real.exp 1 ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))))
(Mathlib.Tactic.Ring.neg_add
(Mathlib.Tactic.Ring.neg_one_mul
(Mathlib.Meta.NormNum.IsNat.to_raw_eq
(Mathlib.Meta.NormNum.IsInt.to_isNat
(Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 3)) (Eq.refl (Int.ofNat 3))))))
(Mathlib.Tactic.Ring.neg_add
(Mathlib.Tactic.Ring.neg_mul (Real.exp 1) (Nat.rawCast 1)
(Mathlib.Tactic.Ring.neg_one_mul
(Mathlib.Meta.NormNum.IsInt.to_raw_eq
(Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1))
(Eq.refl (Int.negOfNat 1))))))
Mathlib.Tactic.Ring.neg_zero)))
(Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.atom_pf (Real.exp 1))
(Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 3)))
(Mathlib.Tactic.Ring.sub_pf
(Mathlib.Tactic.Ring.neg_add
(Mathlib.Tactic.Ring.neg_one_mul
(Mathlib.Meta.NormNum.IsInt.to_raw_eq
(Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 3))
(Eq.refl (Int.negOfNat 3)))))
Mathlib.Tactic.Ring.neg_zero)
(Mathlib.Tactic.Ring.add_pf_add_gt (Int.negOfNat 3).rawCast
(Mathlib.Tactic.Ring.add_pf_add_zero (Real.exp 1 ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))))
(Mathlib.Tactic.Ring.add_pf_add_overlap_zero
(Mathlib.Meta.NormNum.IsInt.to_isNat
(Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 3))
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 3)) (Eq.refl (Int.ofNat 0))))
(Mathlib.Tactic.Ring.add_pf_add_overlap_zero
(Mathlib.Tactic.Ring.add_overlap_pf_zero (Real.exp 1) (Nat.rawCast 1)
(Mathlib.Meta.NormNum.IsInt.to_isNat
(Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1))
(Eq.refl (Int.ofNat 0)))))
(Mathlib.Tactic.Ring.add_pf_zero_add 0))))
(Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero))))
(Mathlib.Tactic.Linarith.lt_of_eq_of_lt (neg_eq_zero.mpr (sub_eq_zero_of_eq a))
(Mathlib.Tactic.Linarith.sub_neg_of_lt Real.exp_one_lt_three)))))c₀:ℝ := -Real.log (distToNearestInt (Real.exp 1)) + 1⊢ ∃ c, 0 < c ∧ ∀ (n : ℕ), 1 ≤ n → Real.exp (-c * ↑n) < distToNearestInt (Real.exp ↑n)
c:ℝhc:0 < chyp:∀ (n : ℕ), 2 ≤ n → ↑n ^ (-c) < distToNearestInt (Real.exp ↑n)hd_pos:0 < distToNearestInt (Real.exp 1) :=
Eq.mpr
(id
(congrArg (fun x => 0 < |Real.exp 1 - x|)
(Eq.trans (congrArg Int.cast Real.round_exp_one_eq_three) (Int.cast_ofNat 3))))
(Eq.mpr (id (congrArg (fun _a => _a) (propext abs_pos)))
(Not.intro fun a =>
Mathlib.Tactic.Linarith.lt_irrefl
(Eq.mp
(congrArg (fun _a => _a < 0)
(Mathlib.Tactic.Ring.of_eq
(Mathlib.Tactic.Ring.add_congr
(Mathlib.Tactic.Ring.neg_congr
(Mathlib.Tactic.Ring.sub_congr
(Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.atom_pf (Real.exp 1))
(Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 3)))
(Mathlib.Tactic.Ring.sub_pf
(Mathlib.Tactic.Ring.neg_add
(Mathlib.Tactic.Ring.neg_one_mul
(Mathlib.Meta.NormNum.IsInt.to_raw_eq
(Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 3))
(Eq.refl (Int.negOfNat 3)))))
Mathlib.Tactic.Ring.neg_zero)
(Mathlib.Tactic.Ring.add_pf_add_gt (Int.negOfNat 3).rawCast
(Mathlib.Tactic.Ring.add_pf_add_zero (Real.exp 1 ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))))
(Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero))
(Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_zero
(Mathlib.Tactic.Ring.add_pf_add_zero
((Int.negOfNat 3).rawCast + (Real.exp 1 ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))))
(Mathlib.Tactic.Ring.neg_add
(Mathlib.Tactic.Ring.neg_one_mul
(Mathlib.Meta.NormNum.IsNat.to_raw_eq
(Mathlib.Meta.NormNum.IsInt.to_isNat
(Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 3)) (Eq.refl (Int.ofNat 3))))))
(Mathlib.Tactic.Ring.neg_add
(Mathlib.Tactic.Ring.neg_mul (Real.exp 1) (Nat.rawCast 1)
(Mathlib.Tactic.Ring.neg_one_mul
(Mathlib.Meta.NormNum.IsInt.to_raw_eq
(Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1))
(Eq.refl (Int.negOfNat 1))))))
Mathlib.Tactic.Ring.neg_zero)))
(Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.atom_pf (Real.exp 1))
(Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 3)))
(Mathlib.Tactic.Ring.sub_pf
(Mathlib.Tactic.Ring.neg_add
(Mathlib.Tactic.Ring.neg_one_mul
(Mathlib.Meta.NormNum.IsInt.to_raw_eq
(Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 3))
(Eq.refl (Int.negOfNat 3)))))
Mathlib.Tactic.Ring.neg_zero)
(Mathlib.Tactic.Ring.add_pf_add_gt (Int.negOfNat 3).rawCast
(Mathlib.Tactic.Ring.add_pf_add_zero (Real.exp 1 ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))))
(Mathlib.Tactic.Ring.add_pf_add_overlap_zero
(Mathlib.Meta.NormNum.IsInt.to_isNat
(Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 3))
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 3)) (Eq.refl (Int.ofNat 0))))
(Mathlib.Tactic.Ring.add_pf_add_overlap_zero
(Mathlib.Tactic.Ring.add_overlap_pf_zero (Real.exp 1) (Nat.rawCast 1)
(Mathlib.Meta.NormNum.IsInt.to_isNat
(Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1))
(Eq.refl (Int.ofNat 0)))))
(Mathlib.Tactic.Ring.add_pf_zero_add 0))))
(Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero))))
(Mathlib.Tactic.Linarith.lt_of_eq_of_lt (neg_eq_zero.mpr (sub_eq_zero_of_eq a))
(Mathlib.Tactic.Linarith.sub_neg_of_lt Real.exp_one_lt_three)))))c₀:ℝ := -Real.log (distToNearestInt (Real.exp 1)) + 1n:ℕhn:1 ≤ n⊢ Real.exp (-max c c₀ * ↑n) < distToNearestInt (Real.exp ↑n)
have hn_pos : (0 : ℝ) < n := h:∃ c, 0 < c ∧ ∀ (n : ℕ), 2 ≤ n → ↑n ^ (-c) < distToNearestInt (Real.exp ↑n)⊢ ∃ c, 0 < c ∧ ∀ (n : ℕ), 1 ≤ n → Real.exp (-c * ↑n) < distToNearestInt (Real.exp ↑n) All goals completed! 🐙
c:ℝhc:0 < chyp:∀ (n : ℕ), 2 ≤ n → ↑n ^ (-c) < distToNearestInt (Real.exp ↑n)hd_pos:0 < distToNearestInt (Real.exp 1) :=
Eq.mpr
(id
(congrArg (fun x => 0 < |Real.exp 1 - x|)
(Eq.trans (congrArg Int.cast Real.round_exp_one_eq_three) (Int.cast_ofNat 3))))
(Eq.mpr (id (congrArg (fun _a => _a) (propext abs_pos)))
(Not.intro fun a =>
Mathlib.Tactic.Linarith.lt_irrefl
(Eq.mp
(congrArg (fun _a => _a < 0)
(Mathlib.Tactic.Ring.of_eq
(Mathlib.Tactic.Ring.add_congr
(Mathlib.Tactic.Ring.neg_congr
(Mathlib.Tactic.Ring.sub_congr
(Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.atom_pf (Real.exp 1))
(Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 3)))
(Mathlib.Tactic.Ring.sub_pf
(Mathlib.Tactic.Ring.neg_add
(Mathlib.Tactic.Ring.neg_one_mul
(Mathlib.Meta.NormNum.IsInt.to_raw_eq
(Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 3))
(Eq.refl (Int.negOfNat 3)))))
Mathlib.Tactic.Ring.neg_zero)
(Mathlib.Tactic.Ring.add_pf_add_gt (Int.negOfNat 3).rawCast
(Mathlib.Tactic.Ring.add_pf_add_zero (Real.exp 1 ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))))
(Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero))
(Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_zero
(Mathlib.Tactic.Ring.add_pf_add_zero
((Int.negOfNat 3).rawCast + (Real.exp 1 ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))))
(Mathlib.Tactic.Ring.neg_add
(Mathlib.Tactic.Ring.neg_one_mul
(Mathlib.Meta.NormNum.IsNat.to_raw_eq
(Mathlib.Meta.NormNum.IsInt.to_isNat
(Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 3)) (Eq.refl (Int.ofNat 3))))))
(Mathlib.Tactic.Ring.neg_add
(Mathlib.Tactic.Ring.neg_mul (Real.exp 1) (Nat.rawCast 1)
(Mathlib.Tactic.Ring.neg_one_mul
(Mathlib.Meta.NormNum.IsInt.to_raw_eq
(Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1))
(Eq.refl (Int.negOfNat 1))))))
Mathlib.Tactic.Ring.neg_zero)))
(Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.atom_pf (Real.exp 1))
(Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 3)))
(Mathlib.Tactic.Ring.sub_pf
(Mathlib.Tactic.Ring.neg_add
(Mathlib.Tactic.Ring.neg_one_mul
(Mathlib.Meta.NormNum.IsInt.to_raw_eq
(Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 3))
(Eq.refl (Int.negOfNat 3)))))
Mathlib.Tactic.Ring.neg_zero)
(Mathlib.Tactic.Ring.add_pf_add_gt (Int.negOfNat 3).rawCast
(Mathlib.Tactic.Ring.add_pf_add_zero (Real.exp 1 ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))))
(Mathlib.Tactic.Ring.add_pf_add_overlap_zero
(Mathlib.Meta.NormNum.IsInt.to_isNat
(Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 3))
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 3)) (Eq.refl (Int.ofNat 0))))
(Mathlib.Tactic.Ring.add_pf_add_overlap_zero
(Mathlib.Tactic.Ring.add_overlap_pf_zero (Real.exp 1) (Nat.rawCast 1)
(Mathlib.Meta.NormNum.IsInt.to_isNat
(Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1))
(Eq.refl (Int.ofNat 0)))))
(Mathlib.Tactic.Ring.add_pf_zero_add 0))))
(Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero))))
(Mathlib.Tactic.Linarith.lt_of_eq_of_lt (neg_eq_zero.mpr (sub_eq_zero_of_eq a))
(Mathlib.Tactic.Linarith.sub_neg_of_lt Real.exp_one_lt_three)))))c₀:ℝ := -Real.log (distToNearestInt (Real.exp 1)) + 1n:ℕhn:1 ≤ nhn_pos:0 < ↑n := cast (Eq.symm (Eq.trans (congrArg (fun x => x < ↑n) (Eq.symm Nat.cast_zero)) Nat.cast_lt._simp_1)) hnh2:n < 2⊢ Real.exp (-max c c₀ * ↑n) < distToNearestInt (Real.exp ↑n)c:ℝhc:0 < chyp:∀ (n : ℕ), 2 ≤ n → ↑n ^ (-c) < distToNearestInt (Real.exp ↑n)hd_pos:0 < distToNearestInt (Real.exp 1) :=
Eq.mpr
(id
(congrArg (fun x => 0 < |Real.exp 1 - x|)
(Eq.trans (congrArg Int.cast Real.round_exp_one_eq_three) (Int.cast_ofNat 3))))
(Eq.mpr (id (congrArg (fun _a => _a) (propext abs_pos)))
(Not.intro fun a =>
Mathlib.Tactic.Linarith.lt_irrefl
(Eq.mp
(congrArg (fun _a => _a < 0)
(Mathlib.Tactic.Ring.of_eq
(Mathlib.Tactic.Ring.add_congr
(Mathlib.Tactic.Ring.neg_congr
(Mathlib.Tactic.Ring.sub_congr
(Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.atom_pf (Real.exp 1))
(Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 3)))
(Mathlib.Tactic.Ring.sub_pf
(Mathlib.Tactic.Ring.neg_add
(Mathlib.Tactic.Ring.neg_one_mul
(Mathlib.Meta.NormNum.IsInt.to_raw_eq
(Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 3))
(Eq.refl (Int.negOfNat 3)))))
Mathlib.Tactic.Ring.neg_zero)
(Mathlib.Tactic.Ring.add_pf_add_gt (Int.negOfNat 3).rawCast
(Mathlib.Tactic.Ring.add_pf_add_zero (Real.exp 1 ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))))
(Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero))
(Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_zero
(Mathlib.Tactic.Ring.add_pf_add_zero
((Int.negOfNat 3).rawCast + (Real.exp 1 ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))))
(Mathlib.Tactic.Ring.neg_add
(Mathlib.Tactic.Ring.neg_one_mul
(Mathlib.Meta.NormNum.IsNat.to_raw_eq
(Mathlib.Meta.NormNum.IsInt.to_isNat
(Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 3)) (Eq.refl (Int.ofNat 3))))))
(Mathlib.Tactic.Ring.neg_add
(Mathlib.Tactic.Ring.neg_mul (Real.exp 1) (Nat.rawCast 1)
(Mathlib.Tactic.Ring.neg_one_mul
(Mathlib.Meta.NormNum.IsInt.to_raw_eq
(Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1))
(Eq.refl (Int.negOfNat 1))))))
Mathlib.Tactic.Ring.neg_zero)))
(Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.atom_pf (Real.exp 1))
(Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 3)))
(Mathlib.Tactic.Ring.sub_pf
(Mathlib.Tactic.Ring.neg_add
(Mathlib.Tactic.Ring.neg_one_mul
(Mathlib.Meta.NormNum.IsInt.to_raw_eq
(Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 3))
(Eq.refl (Int.negOfNat 3)))))
Mathlib.Tactic.Ring.neg_zero)
(Mathlib.Tactic.Ring.add_pf_add_gt (Int.negOfNat 3).rawCast
(Mathlib.Tactic.Ring.add_pf_add_zero (Real.exp 1 ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))))
(Mathlib.Tactic.Ring.add_pf_add_overlap_zero
(Mathlib.Meta.NormNum.IsInt.to_isNat
(Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 3))
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 3)) (Eq.refl (Int.ofNat 0))))
(Mathlib.Tactic.Ring.add_pf_add_overlap_zero
(Mathlib.Tactic.Ring.add_overlap_pf_zero (Real.exp 1) (Nat.rawCast 1)
(Mathlib.Meta.NormNum.IsInt.to_isNat
(Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1))
(Eq.refl (Int.ofNat 0)))))
(Mathlib.Tactic.Ring.add_pf_zero_add 0))))
(Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero))))
(Mathlib.Tactic.Linarith.lt_of_eq_of_lt (neg_eq_zero.mpr (sub_eq_zero_of_eq a))
(Mathlib.Tactic.Linarith.sub_neg_of_lt Real.exp_one_lt_three)))))c₀:ℝ := -Real.log (distToNearestInt (Real.exp 1)) + 1n:ℕhn:1 ≤ nhn_pos:0 < ↑n := cast (Eq.symm (Eq.trans (congrArg (fun x => x < ↑n) (Eq.symm Nat.cast_zero)) Nat.cast_lt._simp_1)) hnh2:n ≥ 2⊢ Real.exp (-max c c₀ * ↑n) < distToNearestInt (Real.exp ↑n)
c:ℝhc:0 < chyp:∀ (n : ℕ), 2 ≤ n → ↑n ^ (-c) < distToNearestInt (Real.exp ↑n)hd_pos:0 < distToNearestInt (Real.exp 1) :=
Eq.mpr
(id
(congrArg (fun x => 0 < |Real.exp 1 - x|)
(Eq.trans (congrArg Int.cast Real.round_exp_one_eq_three) (Int.cast_ofNat 3))))
(Eq.mpr (id (congrArg (fun _a => _a) (propext abs_pos)))
(Not.intro fun a =>
Mathlib.Tactic.Linarith.lt_irrefl
(Eq.mp
(congrArg (fun _a => _a < 0)
(Mathlib.Tactic.Ring.of_eq
(Mathlib.Tactic.Ring.add_congr
(Mathlib.Tactic.Ring.neg_congr
(Mathlib.Tactic.Ring.sub_congr
(Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.atom_pf (Real.exp 1))
(Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 3)))
(Mathlib.Tactic.Ring.sub_pf
(Mathlib.Tactic.Ring.neg_add
(Mathlib.Tactic.Ring.neg_one_mul
(Mathlib.Meta.NormNum.IsInt.to_raw_eq
(Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 3))
(Eq.refl (Int.negOfNat 3)))))
Mathlib.Tactic.Ring.neg_zero)
(Mathlib.Tactic.Ring.add_pf_add_gt (Int.negOfNat 3).rawCast
(Mathlib.Tactic.Ring.add_pf_add_zero (Real.exp 1 ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))))
(Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero))
(Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_zero
(Mathlib.Tactic.Ring.add_pf_add_zero
((Int.negOfNat 3).rawCast + (Real.exp 1 ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))))
(Mathlib.Tactic.Ring.neg_add
(Mathlib.Tactic.Ring.neg_one_mul
(Mathlib.Meta.NormNum.IsNat.to_raw_eq
(Mathlib.Meta.NormNum.IsInt.to_isNat
(Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 3)) (Eq.refl (Int.ofNat 3))))))
(Mathlib.Tactic.Ring.neg_add
(Mathlib.Tactic.Ring.neg_mul (Real.exp 1) (Nat.rawCast 1)
(Mathlib.Tactic.Ring.neg_one_mul
(Mathlib.Meta.NormNum.IsInt.to_raw_eq
(Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1))
(Eq.refl (Int.negOfNat 1))))))
Mathlib.Tactic.Ring.neg_zero)))
(Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.atom_pf (Real.exp 1))
(Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 3)))
(Mathlib.Tactic.Ring.sub_pf
(Mathlib.Tactic.Ring.neg_add
(Mathlib.Tactic.Ring.neg_one_mul
(Mathlib.Meta.NormNum.IsInt.to_raw_eq
(Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 3))
(Eq.refl (Int.negOfNat 3)))))
Mathlib.Tactic.Ring.neg_zero)
(Mathlib.Tactic.Ring.add_pf_add_gt (Int.negOfNat 3).rawCast
(Mathlib.Tactic.Ring.add_pf_add_zero (Real.exp 1 ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))))
(Mathlib.Tactic.Ring.add_pf_add_overlap_zero
(Mathlib.Meta.NormNum.IsInt.to_isNat
(Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 3))
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 3)) (Eq.refl (Int.ofNat 0))))
(Mathlib.Tactic.Ring.add_pf_add_overlap_zero
(Mathlib.Tactic.Ring.add_overlap_pf_zero (Real.exp 1) (Nat.rawCast 1)
(Mathlib.Meta.NormNum.IsInt.to_isNat
(Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1))
(Eq.refl (Int.ofNat 0)))))
(Mathlib.Tactic.Ring.add_pf_zero_add 0))))
(Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero))))
(Mathlib.Tactic.Linarith.lt_of_eq_of_lt (neg_eq_zero.mpr (sub_eq_zero_of_eq a))
(Mathlib.Tactic.Linarith.sub_neg_of_lt Real.exp_one_lt_three)))))c₀:ℝ := -Real.log (distToNearestInt (Real.exp 1)) + 1n:ℕhn:1 ≤ nhn_pos:0 < ↑n := cast (Eq.symm (Eq.trans (congrArg (fun x => x < ↑n) (Eq.symm Nat.cast_zero)) Nat.cast_lt._simp_1)) hnh2:n < 2⊢ Real.exp (-max c c₀ * ↑n) < distToNearestInt (Real.exp ↑n) -- n = 1
have : n = 1 := h:∃ c, 0 < c ∧ ∀ (n : ℕ), 2 ≤ n → ↑n ^ (-c) < distToNearestInt (Real.exp ↑n)⊢ ∃ c, 0 < c ∧ ∀ (n : ℕ), 1 ≤ n → Real.exp (-c * ↑n) < distToNearestInt (Real.exp ↑n) All goals completed! 🐙
c:ℝhc:0 < chyp:∀ (n : ℕ), 2 ≤ n → ↑n ^ (-c) < distToNearestInt (Real.exp ↑n)hd_pos:0 < distToNearestInt (Real.exp 1) :=
Eq.mpr
(id
(congrArg (fun x => 0 < |Real.exp 1 - x|)
(Eq.trans (congrArg Int.cast Real.round_exp_one_eq_three) (Int.cast_ofNat 3))))
(Eq.mpr (id (congrArg (fun _a => _a) (propext abs_pos)))
(Not.intro fun a =>
Mathlib.Tactic.Linarith.lt_irrefl
(Eq.mp
(congrArg (fun _a => _a < 0)
(Mathlib.Tactic.Ring.of_eq
(Mathlib.Tactic.Ring.add_congr
(Mathlib.Tactic.Ring.neg_congr
(Mathlib.Tactic.Ring.sub_congr
(Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.atom_pf (Real.exp 1))
(Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 3)))
(Mathlib.Tactic.Ring.sub_pf
(Mathlib.Tactic.Ring.neg_add
(Mathlib.Tactic.Ring.neg_one_mul
(Mathlib.Meta.NormNum.IsInt.to_raw_eq
(Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 3))
(Eq.refl (Int.negOfNat 3)))))
Mathlib.Tactic.Ring.neg_zero)
(Mathlib.Tactic.Ring.add_pf_add_gt (Int.negOfNat 3).rawCast
(Mathlib.Tactic.Ring.add_pf_add_zero (Real.exp 1 ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))))
(Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero))
(Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_zero
(Mathlib.Tactic.Ring.add_pf_add_zero
((Int.negOfNat 3).rawCast + (Real.exp 1 ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))))
(Mathlib.Tactic.Ring.neg_add
(Mathlib.Tactic.Ring.neg_one_mul
(Mathlib.Meta.NormNum.IsNat.to_raw_eq
(Mathlib.Meta.NormNum.IsInt.to_isNat
(Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 3)) (Eq.refl (Int.ofNat 3))))))
(Mathlib.Tactic.Ring.neg_add
(Mathlib.Tactic.Ring.neg_mul (Real.exp 1) (Nat.rawCast 1)
(Mathlib.Tactic.Ring.neg_one_mul
(Mathlib.Meta.NormNum.IsInt.to_raw_eq
(Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1))
(Eq.refl (Int.negOfNat 1))))))
Mathlib.Tactic.Ring.neg_zero)))
(Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.atom_pf (Real.exp 1))
(Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 3)))
(Mathlib.Tactic.Ring.sub_pf
(Mathlib.Tactic.Ring.neg_add
(Mathlib.Tactic.Ring.neg_one_mul
(Mathlib.Meta.NormNum.IsInt.to_raw_eq
(Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 3))
(Eq.refl (Int.negOfNat 3)))))
Mathlib.Tactic.Ring.neg_zero)
(Mathlib.Tactic.Ring.add_pf_add_gt (Int.negOfNat 3).rawCast
(Mathlib.Tactic.Ring.add_pf_add_zero (Real.exp 1 ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))))
(Mathlib.Tactic.Ring.add_pf_add_overlap_zero
(Mathlib.Meta.NormNum.IsInt.to_isNat
(Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 3))
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 3)) (Eq.refl (Int.ofNat 0))))
(Mathlib.Tactic.Ring.add_pf_add_overlap_zero
(Mathlib.Tactic.Ring.add_overlap_pf_zero (Real.exp 1) (Nat.rawCast 1)
(Mathlib.Meta.NormNum.IsInt.to_isNat
(Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1))
(Eq.refl (Int.ofNat 0)))))
(Mathlib.Tactic.Ring.add_pf_zero_add 0))))
(Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero))))
(Mathlib.Tactic.Linarith.lt_of_eq_of_lt (neg_eq_zero.mpr (sub_eq_zero_of_eq a))
(Mathlib.Tactic.Linarith.sub_neg_of_lt Real.exp_one_lt_three)))))c₀:ℝ := -Real.log (distToNearestInt (Real.exp 1)) + 1hn:1 ≤ 1hn_pos:0 < ↑1h2:1 < 2⊢ Real.exp (-max c c₀ * ↑1) < distToNearestInt (Real.exp ↑1)
c:ℝhc:0 < chyp:∀ (n : ℕ), 2 ≤ n → ↑n ^ (-c) < distToNearestInt (Real.exp ↑n)hd_pos:0 < distToNearestInt (Real.exp 1) :=
Eq.mpr
(id
(congrArg (fun x => 0 < |Real.exp 1 - x|)
(Eq.trans (congrArg Int.cast Real.round_exp_one_eq_three) (Int.cast_ofNat 3))))
(Eq.mpr (id (congrArg (fun _a => _a) (propext abs_pos)))
(Not.intro fun a =>
Mathlib.Tactic.Linarith.lt_irrefl
(Eq.mp
(congrArg (fun _a => _a < 0)
(Mathlib.Tactic.Ring.of_eq
(Mathlib.Tactic.Ring.add_congr
(Mathlib.Tactic.Ring.neg_congr
(Mathlib.Tactic.Ring.sub_congr
(Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.atom_pf (Real.exp 1))
(Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 3)))
(Mathlib.Tactic.Ring.sub_pf
(Mathlib.Tactic.Ring.neg_add
(Mathlib.Tactic.Ring.neg_one_mul
(Mathlib.Meta.NormNum.IsInt.to_raw_eq
(Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 3))
(Eq.refl (Int.negOfNat 3)))))
Mathlib.Tactic.Ring.neg_zero)
(Mathlib.Tactic.Ring.add_pf_add_gt (Int.negOfNat 3).rawCast
(Mathlib.Tactic.Ring.add_pf_add_zero (Real.exp 1 ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))))
(Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero))
(Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_zero
(Mathlib.Tactic.Ring.add_pf_add_zero
((Int.negOfNat 3).rawCast + (Real.exp 1 ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))))
(Mathlib.Tactic.Ring.neg_add
(Mathlib.Tactic.Ring.neg_one_mul
(Mathlib.Meta.NormNum.IsNat.to_raw_eq
(Mathlib.Meta.NormNum.IsInt.to_isNat
(Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 3)) (Eq.refl (Int.ofNat 3))))))
(Mathlib.Tactic.Ring.neg_add
(Mathlib.Tactic.Ring.neg_mul (Real.exp 1) (Nat.rawCast 1)
(Mathlib.Tactic.Ring.neg_one_mul
(Mathlib.Meta.NormNum.IsInt.to_raw_eq
(Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1))
(Eq.refl (Int.negOfNat 1))))))
Mathlib.Tactic.Ring.neg_zero)))
(Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.atom_pf (Real.exp 1))
(Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 3)))
(Mathlib.Tactic.Ring.sub_pf
(Mathlib.Tactic.Ring.neg_add
(Mathlib.Tactic.Ring.neg_one_mul
(Mathlib.Meta.NormNum.IsInt.to_raw_eq
(Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 3))
(Eq.refl (Int.negOfNat 3)))))
Mathlib.Tactic.Ring.neg_zero)
(Mathlib.Tactic.Ring.add_pf_add_gt (Int.negOfNat 3).rawCast
(Mathlib.Tactic.Ring.add_pf_add_zero (Real.exp 1 ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))))
(Mathlib.Tactic.Ring.add_pf_add_overlap_zero
(Mathlib.Meta.NormNum.IsInt.to_isNat
(Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 3))
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 3)) (Eq.refl (Int.ofNat 0))))
(Mathlib.Tactic.Ring.add_pf_add_overlap_zero
(Mathlib.Tactic.Ring.add_overlap_pf_zero (Real.exp 1) (Nat.rawCast 1)
(Mathlib.Meta.NormNum.IsInt.to_isNat
(Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1))
(Eq.refl (Int.ofNat 0)))))
(Mathlib.Tactic.Ring.add_pf_zero_add 0))))
(Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero))))
(Mathlib.Tactic.Linarith.lt_of_eq_of_lt (neg_eq_zero.mpr (sub_eq_zero_of_eq a))
(Mathlib.Tactic.Linarith.sub_neg_of_lt Real.exp_one_lt_three)))))c₀:ℝ := -Real.log (distToNearestInt (Real.exp 1)) + 1hn:1 ≤ 1hn_pos:0 < ↑1h2:1 < 2⊢ Real.exp (-max c c₀ * 1) < distToNearestInt (Real.exp 1)
calc Real.exp (-(max c c₀) * 1)
≤ Real.exp (-c₀) := c:ℝhc:0 < chyp:∀ (n : ℕ), 2 ≤ n → ↑n ^ (-c) < distToNearestInt (Real.exp ↑n)hd_pos:0 < distToNearestInt (Real.exp 1) :=
Eq.mpr
(id
(congrArg (fun x => 0 < |Real.exp 1 - x|)
(Eq.trans (congrArg Int.cast Real.round_exp_one_eq_three) (Int.cast_ofNat 3))))
(Eq.mpr (id (congrArg (fun _a => _a) (propext abs_pos)))
(Not.intro fun a =>
Mathlib.Tactic.Linarith.lt_irrefl
(Eq.mp
(congrArg (fun _a => _a < 0)
(Mathlib.Tactic.Ring.of_eq
(Mathlib.Tactic.Ring.add_congr
(Mathlib.Tactic.Ring.neg_congr
(Mathlib.Tactic.Ring.sub_congr
(Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.atom_pf (Real.exp 1))
(Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 3)))
(Mathlib.Tactic.Ring.sub_pf
(Mathlib.Tactic.Ring.neg_add
(Mathlib.Tactic.Ring.neg_one_mul
(Mathlib.Meta.NormNum.IsInt.to_raw_eq
(Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 3))
(Eq.refl (Int.negOfNat 3)))))
Mathlib.Tactic.Ring.neg_zero)
(Mathlib.Tactic.Ring.add_pf_add_gt (Int.negOfNat 3).rawCast
(Mathlib.Tactic.Ring.add_pf_add_zero (Real.exp 1 ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))))
(Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero))
(Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_zero
(Mathlib.Tactic.Ring.add_pf_add_zero
((Int.negOfNat 3).rawCast + (Real.exp 1 ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))))
(Mathlib.Tactic.Ring.neg_add
(Mathlib.Tactic.Ring.neg_one_mul
(Mathlib.Meta.NormNum.IsNat.to_raw_eq
(Mathlib.Meta.NormNum.IsInt.to_isNat
(Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 3)) (Eq.refl (Int.ofNat 3))))))
(Mathlib.Tactic.Ring.neg_add
(Mathlib.Tactic.Ring.neg_mul (Real.exp 1) (Nat.rawCast 1)
(Mathlib.Tactic.Ring.neg_one_mul
(Mathlib.Meta.NormNum.IsInt.to_raw_eq
(Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1))
(Eq.refl (Int.negOfNat 1))))))
Mathlib.Tactic.Ring.neg_zero)))
(Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.atom_pf (Real.exp 1))
(Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 3)))
(Mathlib.Tactic.Ring.sub_pf
(Mathlib.Tactic.Ring.neg_add
(Mathlib.Tactic.Ring.neg_one_mul
(Mathlib.Meta.NormNum.IsInt.to_raw_eq
(Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 3))
(Eq.refl (Int.negOfNat 3)))))
Mathlib.Tactic.Ring.neg_zero)
(Mathlib.Tactic.Ring.add_pf_add_gt (Int.negOfNat 3).rawCast
(Mathlib.Tactic.Ring.add_pf_add_zero (Real.exp 1 ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))))
(Mathlib.Tactic.Ring.add_pf_add_overlap_zero
(Mathlib.Meta.NormNum.IsInt.to_isNat
(Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 3))
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 3)) (Eq.refl (Int.ofNat 0))))
(Mathlib.Tactic.Ring.add_pf_add_overlap_zero
(Mathlib.Tactic.Ring.add_overlap_pf_zero (Real.exp 1) (Nat.rawCast 1)
(Mathlib.Meta.NormNum.IsInt.to_isNat
(Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1))
(Eq.refl (Int.ofNat 0)))))
(Mathlib.Tactic.Ring.add_pf_zero_add 0))))
(Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero))))
(Mathlib.Tactic.Linarith.lt_of_eq_of_lt (neg_eq_zero.mpr (sub_eq_zero_of_eq a))
(Mathlib.Tactic.Linarith.sub_neg_of_lt Real.exp_one_lt_three)))))c₀:ℝ := -Real.log (distToNearestInt (Real.exp 1)) + 1hn:1 ≤ 1hn_pos:0 < ↑1h2:1 < 2⊢ Real.exp (-max c c₀ * 1) ≤ Real.exp (-c₀)
c:ℝhc:0 < chyp:∀ (n : ℕ), 2 ≤ n → ↑n ^ (-c) < distToNearestInt (Real.exp ↑n)hd_pos:0 < distToNearestInt (Real.exp 1) :=
Eq.mpr
(id
(congrArg (fun x => 0 < |Real.exp 1 - x|)
(Eq.trans (congrArg Int.cast Real.round_exp_one_eq_three) (Int.cast_ofNat 3))))
(Eq.mpr (id (congrArg (fun _a => _a) (propext abs_pos)))
(Not.intro fun a =>
Mathlib.Tactic.Linarith.lt_irrefl
(Eq.mp
(congrArg (fun _a => _a < 0)
(Mathlib.Tactic.Ring.of_eq
(Mathlib.Tactic.Ring.add_congr
(Mathlib.Tactic.Ring.neg_congr
(Mathlib.Tactic.Ring.sub_congr
(Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.atom_pf (Real.exp 1))
(Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 3)))
(Mathlib.Tactic.Ring.sub_pf
(Mathlib.Tactic.Ring.neg_add
(Mathlib.Tactic.Ring.neg_one_mul
(Mathlib.Meta.NormNum.IsInt.to_raw_eq
(Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 3))
(Eq.refl (Int.negOfNat 3)))))
Mathlib.Tactic.Ring.neg_zero)
(Mathlib.Tactic.Ring.add_pf_add_gt (Int.negOfNat 3).rawCast
(Mathlib.Tactic.Ring.add_pf_add_zero (Real.exp 1 ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))))
(Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero))
(Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_zero
(Mathlib.Tactic.Ring.add_pf_add_zero
((Int.negOfNat 3).rawCast + (Real.exp 1 ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))))
(Mathlib.Tactic.Ring.neg_add
(Mathlib.Tactic.Ring.neg_one_mul
(Mathlib.Meta.NormNum.IsNat.to_raw_eq
(Mathlib.Meta.NormNum.IsInt.to_isNat
(Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 3)) (Eq.refl (Int.ofNat 3))))))
(Mathlib.Tactic.Ring.neg_add
(Mathlib.Tactic.Ring.neg_mul (Real.exp 1) (Nat.rawCast 1)
(Mathlib.Tactic.Ring.neg_one_mul
(Mathlib.Meta.NormNum.IsInt.to_raw_eq
(Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1))
(Eq.refl (Int.negOfNat 1))))))
Mathlib.Tactic.Ring.neg_zero)))
(Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.atom_pf (Real.exp 1))
(Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 3)))
(Mathlib.Tactic.Ring.sub_pf
(Mathlib.Tactic.Ring.neg_add
(Mathlib.Tactic.Ring.neg_one_mul
(Mathlib.Meta.NormNum.IsInt.to_raw_eq
(Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 3))
(Eq.refl (Int.negOfNat 3)))))
Mathlib.Tactic.Ring.neg_zero)
(Mathlib.Tactic.Ring.add_pf_add_gt (Int.negOfNat 3).rawCast
(Mathlib.Tactic.Ring.add_pf_add_zero (Real.exp 1 ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))))
(Mathlib.Tactic.Ring.add_pf_add_overlap_zero
(Mathlib.Meta.NormNum.IsInt.to_isNat
(Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 3))
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 3)) (Eq.refl (Int.ofNat 0))))
(Mathlib.Tactic.Ring.add_pf_add_overlap_zero
(Mathlib.Tactic.Ring.add_overlap_pf_zero (Real.exp 1) (Nat.rawCast 1)
(Mathlib.Meta.NormNum.IsInt.to_isNat
(Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1))
(Eq.refl (Int.ofNat 0)))))
(Mathlib.Tactic.Ring.add_pf_zero_add 0))))
(Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero))))
(Mathlib.Tactic.Linarith.lt_of_eq_of_lt (neg_eq_zero.mpr (sub_eq_zero_of_eq a))
(Mathlib.Tactic.Linarith.sub_neg_of_lt Real.exp_one_lt_three)))))c₀:ℝ := -Real.log (distToNearestInt (Real.exp 1)) + 1hn:1 ≤ 1hn_pos:0 < ↑1h2:1 < 2⊢ -max c c₀ * 1 ≤ -c₀; All goals completed! 🐙
_ < distToNearestInt (Real.exp 1) := c:ℝhc:0 < chyp:∀ (n : ℕ), 2 ≤ n → ↑n ^ (-c) < distToNearestInt (Real.exp ↑n)hd_pos:0 < distToNearestInt (Real.exp 1) :=
Eq.mpr
(id
(congrArg (fun x => 0 < |Real.exp 1 - x|)
(Eq.trans (congrArg Int.cast Real.round_exp_one_eq_three) (Int.cast_ofNat 3))))
(Eq.mpr (id (congrArg (fun _a => _a) (propext abs_pos)))
(Not.intro fun a =>
Mathlib.Tactic.Linarith.lt_irrefl
(Eq.mp
(congrArg (fun _a => _a < 0)
(Mathlib.Tactic.Ring.of_eq
(Mathlib.Tactic.Ring.add_congr
(Mathlib.Tactic.Ring.neg_congr
(Mathlib.Tactic.Ring.sub_congr
(Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.atom_pf (Real.exp 1))
(Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 3)))
(Mathlib.Tactic.Ring.sub_pf
(Mathlib.Tactic.Ring.neg_add
(Mathlib.Tactic.Ring.neg_one_mul
(Mathlib.Meta.NormNum.IsInt.to_raw_eq
(Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 3))
(Eq.refl (Int.negOfNat 3)))))
Mathlib.Tactic.Ring.neg_zero)
(Mathlib.Tactic.Ring.add_pf_add_gt (Int.negOfNat 3).rawCast
(Mathlib.Tactic.Ring.add_pf_add_zero (Real.exp 1 ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))))
(Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero))
(Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_zero
(Mathlib.Tactic.Ring.add_pf_add_zero
((Int.negOfNat 3).rawCast + (Real.exp 1 ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))))
(Mathlib.Tactic.Ring.neg_add
(Mathlib.Tactic.Ring.neg_one_mul
(Mathlib.Meta.NormNum.IsNat.to_raw_eq
(Mathlib.Meta.NormNum.IsInt.to_isNat
(Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 3)) (Eq.refl (Int.ofNat 3))))))
(Mathlib.Tactic.Ring.neg_add
(Mathlib.Tactic.Ring.neg_mul (Real.exp 1) (Nat.rawCast 1)
(Mathlib.Tactic.Ring.neg_one_mul
(Mathlib.Meta.NormNum.IsInt.to_raw_eq
(Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1))
(Eq.refl (Int.negOfNat 1))))))
Mathlib.Tactic.Ring.neg_zero)))
(Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.atom_pf (Real.exp 1))
(Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 3)))
(Mathlib.Tactic.Ring.sub_pf
(Mathlib.Tactic.Ring.neg_add
(Mathlib.Tactic.Ring.neg_one_mul
(Mathlib.Meta.NormNum.IsInt.to_raw_eq
(Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 3))
(Eq.refl (Int.negOfNat 3)))))
Mathlib.Tactic.Ring.neg_zero)
(Mathlib.Tactic.Ring.add_pf_add_gt (Int.negOfNat 3).rawCast
(Mathlib.Tactic.Ring.add_pf_add_zero (Real.exp 1 ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))))
(Mathlib.Tactic.Ring.add_pf_add_overlap_zero
(Mathlib.Meta.NormNum.IsInt.to_isNat
(Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 3))
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 3)) (Eq.refl (Int.ofNat 0))))
(Mathlib.Tactic.Ring.add_pf_add_overlap_zero
(Mathlib.Tactic.Ring.add_overlap_pf_zero (Real.exp 1) (Nat.rawCast 1)
(Mathlib.Meta.NormNum.IsInt.to_isNat
(Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1))
(Eq.refl (Int.ofNat 0)))))
(Mathlib.Tactic.Ring.add_pf_zero_add 0))))
(Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero))))
(Mathlib.Tactic.Linarith.lt_of_eq_of_lt (neg_eq_zero.mpr (sub_eq_zero_of_eq a))
(Mathlib.Tactic.Linarith.sub_neg_of_lt Real.exp_one_lt_three)))))c₀:ℝ := -Real.log (distToNearestInt (Real.exp 1)) + 1hn:1 ≤ 1hn_pos:0 < ↑1h2:1 < 2⊢ Real.exp (-c₀) < distToNearestInt (Real.exp 1)
c:ℝhc:0 < chyp:∀ (n : ℕ), 2 ≤ n → ↑n ^ (-c) < distToNearestInt (Real.exp ↑n)hd_pos:0 < distToNearestInt (Real.exp 1) :=
Eq.mpr
(id
(congrArg (fun x => 0 < |Real.exp 1 - x|)
(Eq.trans (congrArg Int.cast Real.round_exp_one_eq_three) (Int.cast_ofNat 3))))
(Eq.mpr (id (congrArg (fun _a => _a) (propext abs_pos)))
(Not.intro fun a =>
Mathlib.Tactic.Linarith.lt_irrefl
(Eq.mp
(congrArg (fun _a => _a < 0)
(Mathlib.Tactic.Ring.of_eq
(Mathlib.Tactic.Ring.add_congr
(Mathlib.Tactic.Ring.neg_congr
(Mathlib.Tactic.Ring.sub_congr
(Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.atom_pf (Real.exp 1))
(Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 3)))
(Mathlib.Tactic.Ring.sub_pf
(Mathlib.Tactic.Ring.neg_add
(Mathlib.Tactic.Ring.neg_one_mul
(Mathlib.Meta.NormNum.IsInt.to_raw_eq
(Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 3))
(Eq.refl (Int.negOfNat 3)))))
Mathlib.Tactic.Ring.neg_zero)
(Mathlib.Tactic.Ring.add_pf_add_gt (Int.negOfNat 3).rawCast
(Mathlib.Tactic.Ring.add_pf_add_zero (Real.exp 1 ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))))
(Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero))
(Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_zero
(Mathlib.Tactic.Ring.add_pf_add_zero
((Int.negOfNat 3).rawCast + (Real.exp 1 ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))))
(Mathlib.Tactic.Ring.neg_add
(Mathlib.Tactic.Ring.neg_one_mul
(Mathlib.Meta.NormNum.IsNat.to_raw_eq
(Mathlib.Meta.NormNum.IsInt.to_isNat
(Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 3)) (Eq.refl (Int.ofNat 3))))))
(Mathlib.Tactic.Ring.neg_add
(Mathlib.Tactic.Ring.neg_mul (Real.exp 1) (Nat.rawCast 1)
(Mathlib.Tactic.Ring.neg_one_mul
(Mathlib.Meta.NormNum.IsInt.to_raw_eq
(Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1))
(Eq.refl (Int.negOfNat 1))))))
Mathlib.Tactic.Ring.neg_zero)))
(Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.atom_pf (Real.exp 1))
(Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 3)))
(Mathlib.Tactic.Ring.sub_pf
(Mathlib.Tactic.Ring.neg_add
(Mathlib.Tactic.Ring.neg_one_mul
(Mathlib.Meta.NormNum.IsInt.to_raw_eq
(Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 3))
(Eq.refl (Int.negOfNat 3)))))
Mathlib.Tactic.Ring.neg_zero)
(Mathlib.Tactic.Ring.add_pf_add_gt (Int.negOfNat 3).rawCast
(Mathlib.Tactic.Ring.add_pf_add_zero (Real.exp 1 ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))))
(Mathlib.Tactic.Ring.add_pf_add_overlap_zero
(Mathlib.Meta.NormNum.IsInt.to_isNat
(Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 3))
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 3)) (Eq.refl (Int.ofNat 0))))
(Mathlib.Tactic.Ring.add_pf_add_overlap_zero
(Mathlib.Tactic.Ring.add_overlap_pf_zero (Real.exp 1) (Nat.rawCast 1)
(Mathlib.Meta.NormNum.IsInt.to_isNat
(Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1))
(Eq.refl (Int.ofNat 0)))))
(Mathlib.Tactic.Ring.add_pf_zero_add 0))))
(Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero))))
(Mathlib.Tactic.Linarith.lt_of_eq_of_lt (neg_eq_zero.mpr (sub_eq_zero_of_eq a))
(Mathlib.Tactic.Linarith.sub_neg_of_lt Real.exp_one_lt_three)))))c₀:ℝ := -Real.log (distToNearestInt (Real.exp 1)) + 1hn:1 ≤ 1hn_pos:0 < ↑1h2:1 < 2⊢ Real.exp (Real.log (distToNearestInt (Real.exp 1)) - 1) < distToNearestInt (Real.exp 1)
c:ℝhc:0 < chyp:∀ (n : ℕ), 2 ≤ n → ↑n ^ (-c) < distToNearestInt (Real.exp ↑n)hd_pos:0 < distToNearestInt (Real.exp 1) :=
Eq.mpr
(id
(congrArg (fun x => 0 < |Real.exp 1 - x|)
(Eq.trans (congrArg Int.cast Real.round_exp_one_eq_three) (Int.cast_ofNat 3))))
(Eq.mpr (id (congrArg (fun _a => _a) (propext abs_pos)))
(Not.intro fun a =>
Mathlib.Tactic.Linarith.lt_irrefl
(Eq.mp
(congrArg (fun _a => _a < 0)
(Mathlib.Tactic.Ring.of_eq
(Mathlib.Tactic.Ring.add_congr
(Mathlib.Tactic.Ring.neg_congr
(Mathlib.Tactic.Ring.sub_congr
(Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.atom_pf (Real.exp 1))
(Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 3)))
(Mathlib.Tactic.Ring.sub_pf
(Mathlib.Tactic.Ring.neg_add
(Mathlib.Tactic.Ring.neg_one_mul
(Mathlib.Meta.NormNum.IsInt.to_raw_eq
(Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 3))
(Eq.refl (Int.negOfNat 3)))))
Mathlib.Tactic.Ring.neg_zero)
(Mathlib.Tactic.Ring.add_pf_add_gt (Int.negOfNat 3).rawCast
(Mathlib.Tactic.Ring.add_pf_add_zero (Real.exp 1 ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))))
(Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero))
(Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_zero
(Mathlib.Tactic.Ring.add_pf_add_zero
((Int.negOfNat 3).rawCast + (Real.exp 1 ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))))
(Mathlib.Tactic.Ring.neg_add
(Mathlib.Tactic.Ring.neg_one_mul
(Mathlib.Meta.NormNum.IsNat.to_raw_eq
(Mathlib.Meta.NormNum.IsInt.to_isNat
(Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 3)) (Eq.refl (Int.ofNat 3))))))
(Mathlib.Tactic.Ring.neg_add
(Mathlib.Tactic.Ring.neg_mul (Real.exp 1) (Nat.rawCast 1)
(Mathlib.Tactic.Ring.neg_one_mul
(Mathlib.Meta.NormNum.IsInt.to_raw_eq
(Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1))
(Eq.refl (Int.negOfNat 1))))))
Mathlib.Tactic.Ring.neg_zero)))
(Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.atom_pf (Real.exp 1))
(Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 3)))
(Mathlib.Tactic.Ring.sub_pf
(Mathlib.Tactic.Ring.neg_add
(Mathlib.Tactic.Ring.neg_one_mul
(Mathlib.Meta.NormNum.IsInt.to_raw_eq
(Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 3))
(Eq.refl (Int.negOfNat 3)))))
Mathlib.Tactic.Ring.neg_zero)
(Mathlib.Tactic.Ring.add_pf_add_gt (Int.negOfNat 3).rawCast
(Mathlib.Tactic.Ring.add_pf_add_zero (Real.exp 1 ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))))
(Mathlib.Tactic.Ring.add_pf_add_overlap_zero
(Mathlib.Meta.NormNum.IsInt.to_isNat
(Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 3))
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 3)) (Eq.refl (Int.ofNat 0))))
(Mathlib.Tactic.Ring.add_pf_add_overlap_zero
(Mathlib.Tactic.Ring.add_overlap_pf_zero (Real.exp 1) (Nat.rawCast 1)
(Mathlib.Meta.NormNum.IsInt.to_isNat
(Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1))
(Eq.refl (Int.ofNat 0)))))
(Mathlib.Tactic.Ring.add_pf_zero_add 0))))
(Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero))))
(Mathlib.Tactic.Linarith.lt_of_eq_of_lt (neg_eq_zero.mpr (sub_eq_zero_of_eq a))
(Mathlib.Tactic.Linarith.sub_neg_of_lt Real.exp_one_lt_three)))))c₀:ℝ := -Real.log (distToNearestInt (Real.exp 1)) + 1hn:1 ≤ 1hn_pos:0 < ↑1h2:1 < 2⊢ distToNearestInt (Real.exp 1) / Real.exp 1 < distToNearestInt (Real.exp 1)
have he : (1 : ℝ) < Real.exp 1 := Real.exp_one_gt_d9.trans' (c:ℝhc:0 < chyp:∀ (n : ℕ), 2 ≤ n → ↑n ^ (-c) < distToNearestInt (Real.exp ↑n)hd_pos:0 < distToNearestInt (Real.exp 1) :=
Eq.mpr
(id
(congrArg (fun x => 0 < |Real.exp 1 - x|)
(Eq.trans (congrArg Int.cast Real.round_exp_one_eq_three) (Int.cast_ofNat 3))))
(Eq.mpr (id (congrArg (fun _a => _a) (propext abs_pos)))
(Not.intro fun a =>
Mathlib.Tactic.Linarith.lt_irrefl
(Eq.mp
(congrArg (fun _a => _a < 0)
(Mathlib.Tactic.Ring.of_eq
(Mathlib.Tactic.Ring.add_congr
(Mathlib.Tactic.Ring.neg_congr
(Mathlib.Tactic.Ring.sub_congr
(Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.atom_pf (Real.exp 1))
(Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 3)))
(Mathlib.Tactic.Ring.sub_pf
(Mathlib.Tactic.Ring.neg_add
(Mathlib.Tactic.Ring.neg_one_mul
(Mathlib.Meta.NormNum.IsInt.to_raw_eq
(Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 3))
(Eq.refl (Int.negOfNat 3)))))
Mathlib.Tactic.Ring.neg_zero)
(Mathlib.Tactic.Ring.add_pf_add_gt (Int.negOfNat 3).rawCast
(Mathlib.Tactic.Ring.add_pf_add_zero (Real.exp 1 ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))))
(Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero))
(Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_zero
(Mathlib.Tactic.Ring.add_pf_add_zero
((Int.negOfNat 3).rawCast + (Real.exp 1 ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))))
(Mathlib.Tactic.Ring.neg_add
(Mathlib.Tactic.Ring.neg_one_mul
(Mathlib.Meta.NormNum.IsNat.to_raw_eq
(Mathlib.Meta.NormNum.IsInt.to_isNat
(Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 3)) (Eq.refl (Int.ofNat 3))))))
(Mathlib.Tactic.Ring.neg_add
(Mathlib.Tactic.Ring.neg_mul (Real.exp 1) (Nat.rawCast 1)
(Mathlib.Tactic.Ring.neg_one_mul
(Mathlib.Meta.NormNum.IsInt.to_raw_eq
(Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1))
(Eq.refl (Int.negOfNat 1))))))
Mathlib.Tactic.Ring.neg_zero)))
(Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.atom_pf (Real.exp 1))
(Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 3)))
(Mathlib.Tactic.Ring.sub_pf
(Mathlib.Tactic.Ring.neg_add
(Mathlib.Tactic.Ring.neg_one_mul
(Mathlib.Meta.NormNum.IsInt.to_raw_eq
(Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 3))
(Eq.refl (Int.negOfNat 3)))))
Mathlib.Tactic.Ring.neg_zero)
(Mathlib.Tactic.Ring.add_pf_add_gt (Int.negOfNat 3).rawCast
(Mathlib.Tactic.Ring.add_pf_add_zero (Real.exp 1 ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))))
(Mathlib.Tactic.Ring.add_pf_add_overlap_zero
(Mathlib.Meta.NormNum.IsInt.to_isNat
(Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 3))
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 3)) (Eq.refl (Int.ofNat 0))))
(Mathlib.Tactic.Ring.add_pf_add_overlap_zero
(Mathlib.Tactic.Ring.add_overlap_pf_zero (Real.exp 1) (Nat.rawCast 1)
(Mathlib.Meta.NormNum.IsInt.to_isNat
(Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1))
(Eq.refl (Int.ofNat 0)))))
(Mathlib.Tactic.Ring.add_pf_zero_add 0))))
(Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero))))
(Mathlib.Tactic.Linarith.lt_of_eq_of_lt (neg_eq_zero.mpr (sub_eq_zero_of_eq a))
(Mathlib.Tactic.Linarith.sub_neg_of_lt Real.exp_one_lt_three)))))c₀:ℝ := -Real.log (distToNearestInt (Real.exp 1)) + 1hn:1 ≤ 1hn_pos:0 < ↑1h2:1 < 2⊢ 1 < 2.7182818283 All goals completed! 🐙)
c:ℝhc:0 < chyp:∀ (n : ℕ), 2 ≤ n → ↑n ^ (-c) < distToNearestInt (Real.exp ↑n)hd_pos:0 < distToNearestInt (Real.exp 1) :=
Eq.mpr
(id
(congrArg (fun x => 0 < |Real.exp 1 - x|)
(Eq.trans (congrArg Int.cast Real.round_exp_one_eq_three) (Int.cast_ofNat 3))))
(Eq.mpr (id (congrArg (fun _a => _a) (propext abs_pos)))
(Not.intro fun a =>
Mathlib.Tactic.Linarith.lt_irrefl
(Eq.mp
(congrArg (fun _a => _a < 0)
(Mathlib.Tactic.Ring.of_eq
(Mathlib.Tactic.Ring.add_congr
(Mathlib.Tactic.Ring.neg_congr
(Mathlib.Tactic.Ring.sub_congr
(Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.atom_pf (Real.exp 1))
(Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 3)))
(Mathlib.Tactic.Ring.sub_pf
(Mathlib.Tactic.Ring.neg_add
(Mathlib.Tactic.Ring.neg_one_mul
(Mathlib.Meta.NormNum.IsInt.to_raw_eq
(Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 3))
(Eq.refl (Int.negOfNat 3)))))
Mathlib.Tactic.Ring.neg_zero)
(Mathlib.Tactic.Ring.add_pf_add_gt (Int.negOfNat 3).rawCast
(Mathlib.Tactic.Ring.add_pf_add_zero (Real.exp 1 ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))))
(Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero))
(Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_zero
(Mathlib.Tactic.Ring.add_pf_add_zero
((Int.negOfNat 3).rawCast + (Real.exp 1 ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))))
(Mathlib.Tactic.Ring.neg_add
(Mathlib.Tactic.Ring.neg_one_mul
(Mathlib.Meta.NormNum.IsNat.to_raw_eq
(Mathlib.Meta.NormNum.IsInt.to_isNat
(Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 3)) (Eq.refl (Int.ofNat 3))))))
(Mathlib.Tactic.Ring.neg_add
(Mathlib.Tactic.Ring.neg_mul (Real.exp 1) (Nat.rawCast 1)
(Mathlib.Tactic.Ring.neg_one_mul
(Mathlib.Meta.NormNum.IsInt.to_raw_eq
(Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1))
(Eq.refl (Int.negOfNat 1))))))
Mathlib.Tactic.Ring.neg_zero)))
(Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.atom_pf (Real.exp 1))
(Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 3)))
(Mathlib.Tactic.Ring.sub_pf
(Mathlib.Tactic.Ring.neg_add
(Mathlib.Tactic.Ring.neg_one_mul
(Mathlib.Meta.NormNum.IsInt.to_raw_eq
(Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 3))
(Eq.refl (Int.negOfNat 3)))))
Mathlib.Tactic.Ring.neg_zero)
(Mathlib.Tactic.Ring.add_pf_add_gt (Int.negOfNat 3).rawCast
(Mathlib.Tactic.Ring.add_pf_add_zero (Real.exp 1 ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))))
(Mathlib.Tactic.Ring.add_pf_add_overlap_zero
(Mathlib.Meta.NormNum.IsInt.to_isNat
(Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 3))
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 3)) (Eq.refl (Int.ofNat 0))))
(Mathlib.Tactic.Ring.add_pf_add_overlap_zero
(Mathlib.Tactic.Ring.add_overlap_pf_zero (Real.exp 1) (Nat.rawCast 1)
(Mathlib.Meta.NormNum.IsInt.to_isNat
(Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1))
(Eq.refl (Int.ofNat 0)))))
(Mathlib.Tactic.Ring.add_pf_zero_add 0))))
(Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero))))
(Mathlib.Tactic.Linarith.lt_of_eq_of_lt (neg_eq_zero.mpr (sub_eq_zero_of_eq a))
(Mathlib.Tactic.Linarith.sub_neg_of_lt Real.exp_one_lt_three)))))c₀:ℝ := -Real.log (distToNearestInt (Real.exp 1)) + 1hn:1 ≤ 1hn_pos:0 < ↑1h2:1 < 2he:1 < Real.exp 1 :=
LT.lt.trans' Real.exp_one_gt_d9
(Mathlib.Meta.NormNum.isNNRat_lt_true
(Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one))
(Mathlib.Meta.NormNum.isNNRat_ofScientific_of_true
(Mathlib.Meta.NormNum.isNNRat_ratCast
(Mathlib.Meta.NormNum.IsRat.to_isNNRat
(Mathlib.Meta.NormNum.isRat_mkRat
(Mathlib.Meta.NormNum.IsNat.to_isInt
(Mathlib.Meta.NormNum.isNat_natCast 27182818283 27182818283
(Mathlib.Meta.NormNum.IsNat.raw_refl 27182818283)))
(Mathlib.Meta.NormNum.isNat_pow (Eq.refl HPow.hPow) (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 10))
(Mathlib.Meta.NormNum.IsNat.raw_refl 10)
(Mathlib.Meta.NormNum.IsNatPowT.run
(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.IsNNRat.to_isRat
(Mathlib.Meta.NormNum.isNNRat_div
(Mathlib.Meta.NormNum.isNNRat_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.isNat_intCast (Int.ofNat 27182818283) 27182818283
(Mathlib.Meta.NormNum.isNat_intOfNat (Mathlib.Meta.NormNum.IsNat.raw_refl 27182818283))))
(Mathlib.Meta.NormNum.isNNRat_inv_pos
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.isNat_natCast 10000000000 10000000000
(Mathlib.Meta.NormNum.IsNat.raw_refl 10000000000))))
(Eq.refl (Nat.mul 27182818283 1)) (Eq.refl 10000000000))))))))
(Eq.refl true))this:0 < distToNearestInt (Real.exp 1) := hd_pos⊢ distToNearestInt (Real.exp 1) / Real.exp 1 < distToNearestInt (Real.exp 1)
c:ℝhc:0 < chyp:∀ (n : ℕ), 2 ≤ n → ↑n ^ (-c) < distToNearestInt (Real.exp ↑n)hd_pos:0 < distToNearestInt (Real.exp 1) :=
Eq.mpr
(id
(congrArg (fun x => 0 < |Real.exp 1 - x|)
(Eq.trans (congrArg Int.cast Real.round_exp_one_eq_three) (Int.cast_ofNat 3))))
(Eq.mpr (id (congrArg (fun _a => _a) (propext abs_pos)))
(Not.intro fun a =>
Mathlib.Tactic.Linarith.lt_irrefl
(Eq.mp
(congrArg (fun _a => _a < 0)
(Mathlib.Tactic.Ring.of_eq
(Mathlib.Tactic.Ring.add_congr
(Mathlib.Tactic.Ring.neg_congr
(Mathlib.Tactic.Ring.sub_congr
(Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.atom_pf (Real.exp 1))
(Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 3)))
(Mathlib.Tactic.Ring.sub_pf
(Mathlib.Tactic.Ring.neg_add
(Mathlib.Tactic.Ring.neg_one_mul
(Mathlib.Meta.NormNum.IsInt.to_raw_eq
(Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 3))
(Eq.refl (Int.negOfNat 3)))))
Mathlib.Tactic.Ring.neg_zero)
(Mathlib.Tactic.Ring.add_pf_add_gt (Int.negOfNat 3).rawCast
(Mathlib.Tactic.Ring.add_pf_add_zero (Real.exp 1 ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))))
(Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero))
(Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_zero
(Mathlib.Tactic.Ring.add_pf_add_zero
((Int.negOfNat 3).rawCast + (Real.exp 1 ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))))
(Mathlib.Tactic.Ring.neg_add
(Mathlib.Tactic.Ring.neg_one_mul
(Mathlib.Meta.NormNum.IsNat.to_raw_eq
(Mathlib.Meta.NormNum.IsInt.to_isNat
(Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 3)) (Eq.refl (Int.ofNat 3))))))
(Mathlib.Tactic.Ring.neg_add
(Mathlib.Tactic.Ring.neg_mul (Real.exp 1) (Nat.rawCast 1)
(Mathlib.Tactic.Ring.neg_one_mul
(Mathlib.Meta.NormNum.IsInt.to_raw_eq
(Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1))
(Eq.refl (Int.negOfNat 1))))))
Mathlib.Tactic.Ring.neg_zero)))
(Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.atom_pf (Real.exp 1))
(Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 3)))
(Mathlib.Tactic.Ring.sub_pf
(Mathlib.Tactic.Ring.neg_add
(Mathlib.Tactic.Ring.neg_one_mul
(Mathlib.Meta.NormNum.IsInt.to_raw_eq
(Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 3))
(Eq.refl (Int.negOfNat 3)))))
Mathlib.Tactic.Ring.neg_zero)
(Mathlib.Tactic.Ring.add_pf_add_gt (Int.negOfNat 3).rawCast
(Mathlib.Tactic.Ring.add_pf_add_zero (Real.exp 1 ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))))
(Mathlib.Tactic.Ring.add_pf_add_overlap_zero
(Mathlib.Meta.NormNum.IsInt.to_isNat
(Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 3))
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 3)) (Eq.refl (Int.ofNat 0))))
(Mathlib.Tactic.Ring.add_pf_add_overlap_zero
(Mathlib.Tactic.Ring.add_overlap_pf_zero (Real.exp 1) (Nat.rawCast 1)
(Mathlib.Meta.NormNum.IsInt.to_isNat
(Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1))
(Eq.refl (Int.ofNat 0)))))
(Mathlib.Tactic.Ring.add_pf_zero_add 0))))
(Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero))))
(Mathlib.Tactic.Linarith.lt_of_eq_of_lt (neg_eq_zero.mpr (sub_eq_zero_of_eq a))
(Mathlib.Tactic.Linarith.sub_neg_of_lt Real.exp_one_lt_three)))))c₀:ℝ := -Real.log (distToNearestInt (Real.exp 1)) + 1hn:1 ≤ 1hn_pos:0 < ↑1h2:1 < 2he:1 < Real.exp 1 :=
LT.lt.trans' Real.exp_one_gt_d9
(Mathlib.Meta.NormNum.isNNRat_lt_true
(Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one))
(Mathlib.Meta.NormNum.isNNRat_ofScientific_of_true
(Mathlib.Meta.NormNum.isNNRat_ratCast
(Mathlib.Meta.NormNum.IsRat.to_isNNRat
(Mathlib.Meta.NormNum.isRat_mkRat
(Mathlib.Meta.NormNum.IsNat.to_isInt
(Mathlib.Meta.NormNum.isNat_natCast 27182818283 27182818283
(Mathlib.Meta.NormNum.IsNat.raw_refl 27182818283)))
(Mathlib.Meta.NormNum.isNat_pow (Eq.refl HPow.hPow) (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 10))
(Mathlib.Meta.NormNum.IsNat.raw_refl 10)
(Mathlib.Meta.NormNum.IsNatPowT.run
(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.IsNNRat.to_isRat
(Mathlib.Meta.NormNum.isNNRat_div
(Mathlib.Meta.NormNum.isNNRat_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.isNat_intCast (Int.ofNat 27182818283) 27182818283
(Mathlib.Meta.NormNum.isNat_intOfNat (Mathlib.Meta.NormNum.IsNat.raw_refl 27182818283))))
(Mathlib.Meta.NormNum.isNNRat_inv_pos
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.isNat_natCast 10000000000 10000000000
(Mathlib.Meta.NormNum.IsNat.raw_refl 10000000000))))
(Eq.refl (Nat.mul 27182818283 1)) (Eq.refl 10000000000))))))))
(Eq.refl true))this:0 < distToNearestInt (Real.exp 1) := hd_pos⊢ distToNearestInt (Real.exp 1) < distToNearestInt (Real.exp 1) * Real.exp 1
All goals completed! 🐙
c:ℝhc:0 < chyp:∀ (n : ℕ), 2 ≤ n → ↑n ^ (-c) < distToNearestInt (Real.exp ↑n)hd_pos:0 < distToNearestInt (Real.exp 1) :=
Eq.mpr
(id
(congrArg (fun x => 0 < |Real.exp 1 - x|)
(Eq.trans (congrArg Int.cast Real.round_exp_one_eq_three) (Int.cast_ofNat 3))))
(Eq.mpr (id (congrArg (fun _a => _a) (propext abs_pos)))
(Not.intro fun a =>
Mathlib.Tactic.Linarith.lt_irrefl
(Eq.mp
(congrArg (fun _a => _a < 0)
(Mathlib.Tactic.Ring.of_eq
(Mathlib.Tactic.Ring.add_congr
(Mathlib.Tactic.Ring.neg_congr
(Mathlib.Tactic.Ring.sub_congr
(Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.atom_pf (Real.exp 1))
(Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 3)))
(Mathlib.Tactic.Ring.sub_pf
(Mathlib.Tactic.Ring.neg_add
(Mathlib.Tactic.Ring.neg_one_mul
(Mathlib.Meta.NormNum.IsInt.to_raw_eq
(Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 3))
(Eq.refl (Int.negOfNat 3)))))
Mathlib.Tactic.Ring.neg_zero)
(Mathlib.Tactic.Ring.add_pf_add_gt (Int.negOfNat 3).rawCast
(Mathlib.Tactic.Ring.add_pf_add_zero (Real.exp 1 ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))))
(Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero))
(Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_zero
(Mathlib.Tactic.Ring.add_pf_add_zero
((Int.negOfNat 3).rawCast + (Real.exp 1 ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))))
(Mathlib.Tactic.Ring.neg_add
(Mathlib.Tactic.Ring.neg_one_mul
(Mathlib.Meta.NormNum.IsNat.to_raw_eq
(Mathlib.Meta.NormNum.IsInt.to_isNat
(Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 3)) (Eq.refl (Int.ofNat 3))))))
(Mathlib.Tactic.Ring.neg_add
(Mathlib.Tactic.Ring.neg_mul (Real.exp 1) (Nat.rawCast 1)
(Mathlib.Tactic.Ring.neg_one_mul
(Mathlib.Meta.NormNum.IsInt.to_raw_eq
(Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1))
(Eq.refl (Int.negOfNat 1))))))
Mathlib.Tactic.Ring.neg_zero)))
(Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.atom_pf (Real.exp 1))
(Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 3)))
(Mathlib.Tactic.Ring.sub_pf
(Mathlib.Tactic.Ring.neg_add
(Mathlib.Tactic.Ring.neg_one_mul
(Mathlib.Meta.NormNum.IsInt.to_raw_eq
(Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 3))
(Eq.refl (Int.negOfNat 3)))))
Mathlib.Tactic.Ring.neg_zero)
(Mathlib.Tactic.Ring.add_pf_add_gt (Int.negOfNat 3).rawCast
(Mathlib.Tactic.Ring.add_pf_add_zero (Real.exp 1 ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))))
(Mathlib.Tactic.Ring.add_pf_add_overlap_zero
(Mathlib.Meta.NormNum.IsInt.to_isNat
(Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 3))
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 3)) (Eq.refl (Int.ofNat 0))))
(Mathlib.Tactic.Ring.add_pf_add_overlap_zero
(Mathlib.Tactic.Ring.add_overlap_pf_zero (Real.exp 1) (Nat.rawCast 1)
(Mathlib.Meta.NormNum.IsInt.to_isNat
(Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1))
(Eq.refl (Int.ofNat 0)))))
(Mathlib.Tactic.Ring.add_pf_zero_add 0))))
(Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero))))
(Mathlib.Tactic.Linarith.lt_of_eq_of_lt (neg_eq_zero.mpr (sub_eq_zero_of_eq a))
(Mathlib.Tactic.Linarith.sub_neg_of_lt Real.exp_one_lt_three)))))c₀:ℝ := -Real.log (distToNearestInt (Real.exp 1)) + 1n:ℕhn:1 ≤ nhn_pos:0 < ↑n := cast (Eq.symm (Eq.trans (congrArg (fun x => x < ↑n) (Eq.symm Nat.cast_zero)) Nat.cast_lt._simp_1)) hnh2:n ≥ 2⊢ Real.exp (-max c c₀ * ↑n) < distToNearestInt (Real.exp ↑n) -- n ≥ 2: use Waldschmidt
calc Real.exp (-(max c c₀) * n)
≤ Real.exp (-c * n) := c:ℝhc:0 < chyp:∀ (n : ℕ), 2 ≤ n → ↑n ^ (-c) < distToNearestInt (Real.exp ↑n)hd_pos:0 < distToNearestInt (Real.exp 1) :=
Eq.mpr
(id
(congrArg (fun x => 0 < |Real.exp 1 - x|)
(Eq.trans (congrArg Int.cast Real.round_exp_one_eq_three) (Int.cast_ofNat 3))))
(Eq.mpr (id (congrArg (fun _a => _a) (propext abs_pos)))
(Not.intro fun a =>
Mathlib.Tactic.Linarith.lt_irrefl
(Eq.mp
(congrArg (fun _a => _a < 0)
(Mathlib.Tactic.Ring.of_eq
(Mathlib.Tactic.Ring.add_congr
(Mathlib.Tactic.Ring.neg_congr
(Mathlib.Tactic.Ring.sub_congr
(Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.atom_pf (Real.exp 1))
(Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 3)))
(Mathlib.Tactic.Ring.sub_pf
(Mathlib.Tactic.Ring.neg_add
(Mathlib.Tactic.Ring.neg_one_mul
(Mathlib.Meta.NormNum.IsInt.to_raw_eq
(Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 3))
(Eq.refl (Int.negOfNat 3)))))
Mathlib.Tactic.Ring.neg_zero)
(Mathlib.Tactic.Ring.add_pf_add_gt (Int.negOfNat 3).rawCast
(Mathlib.Tactic.Ring.add_pf_add_zero (Real.exp 1 ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))))
(Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero))
(Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_zero
(Mathlib.Tactic.Ring.add_pf_add_zero
((Int.negOfNat 3).rawCast + (Real.exp 1 ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))))
(Mathlib.Tactic.Ring.neg_add
(Mathlib.Tactic.Ring.neg_one_mul
(Mathlib.Meta.NormNum.IsNat.to_raw_eq
(Mathlib.Meta.NormNum.IsInt.to_isNat
(Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 3)) (Eq.refl (Int.ofNat 3))))))
(Mathlib.Tactic.Ring.neg_add
(Mathlib.Tactic.Ring.neg_mul (Real.exp 1) (Nat.rawCast 1)
(Mathlib.Tactic.Ring.neg_one_mul
(Mathlib.Meta.NormNum.IsInt.to_raw_eq
(Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1))
(Eq.refl (Int.negOfNat 1))))))
Mathlib.Tactic.Ring.neg_zero)))
(Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.atom_pf (Real.exp 1))
(Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 3)))
(Mathlib.Tactic.Ring.sub_pf
(Mathlib.Tactic.Ring.neg_add
(Mathlib.Tactic.Ring.neg_one_mul
(Mathlib.Meta.NormNum.IsInt.to_raw_eq
(Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 3))
(Eq.refl (Int.negOfNat 3)))))
Mathlib.Tactic.Ring.neg_zero)
(Mathlib.Tactic.Ring.add_pf_add_gt (Int.negOfNat 3).rawCast
(Mathlib.Tactic.Ring.add_pf_add_zero (Real.exp 1 ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))))
(Mathlib.Tactic.Ring.add_pf_add_overlap_zero
(Mathlib.Meta.NormNum.IsInt.to_isNat
(Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 3))
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 3)) (Eq.refl (Int.ofNat 0))))
(Mathlib.Tactic.Ring.add_pf_add_overlap_zero
(Mathlib.Tactic.Ring.add_overlap_pf_zero (Real.exp 1) (Nat.rawCast 1)
(Mathlib.Meta.NormNum.IsInt.to_isNat
(Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1))
(Eq.refl (Int.ofNat 0)))))
(Mathlib.Tactic.Ring.add_pf_zero_add 0))))
(Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero))))
(Mathlib.Tactic.Linarith.lt_of_eq_of_lt (neg_eq_zero.mpr (sub_eq_zero_of_eq a))
(Mathlib.Tactic.Linarith.sub_neg_of_lt Real.exp_one_lt_three)))))c₀:ℝ := -Real.log (distToNearestInt (Real.exp 1)) + 1n:ℕhn:1 ≤ nhn_pos:0 < ↑n := cast (Eq.symm (Eq.trans (congrArg (fun x => x < ↑n) (Eq.symm Nat.cast_zero)) Nat.cast_lt._simp_1)) hnh2:n ≥ 2⊢ Real.exp (-max c c₀ * ↑n) ≤ Real.exp (-c * ↑n)
c:ℝhc:0 < chyp:∀ (n : ℕ), 2 ≤ n → ↑n ^ (-c) < distToNearestInt (Real.exp ↑n)hd_pos:0 < distToNearestInt (Real.exp 1) :=
Eq.mpr
(id
(congrArg (fun x => 0 < |Real.exp 1 - x|)
(Eq.trans (congrArg Int.cast Real.round_exp_one_eq_three) (Int.cast_ofNat 3))))
(Eq.mpr (id (congrArg (fun _a => _a) (propext abs_pos)))
(Not.intro fun a =>
Mathlib.Tactic.Linarith.lt_irrefl
(Eq.mp
(congrArg (fun _a => _a < 0)
(Mathlib.Tactic.Ring.of_eq
(Mathlib.Tactic.Ring.add_congr
(Mathlib.Tactic.Ring.neg_congr
(Mathlib.Tactic.Ring.sub_congr
(Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.atom_pf (Real.exp 1))
(Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 3)))
(Mathlib.Tactic.Ring.sub_pf
(Mathlib.Tactic.Ring.neg_add
(Mathlib.Tactic.Ring.neg_one_mul
(Mathlib.Meta.NormNum.IsInt.to_raw_eq
(Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 3))
(Eq.refl (Int.negOfNat 3)))))
Mathlib.Tactic.Ring.neg_zero)
(Mathlib.Tactic.Ring.add_pf_add_gt (Int.negOfNat 3).rawCast
(Mathlib.Tactic.Ring.add_pf_add_zero (Real.exp 1 ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))))
(Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero))
(Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_zero
(Mathlib.Tactic.Ring.add_pf_add_zero
((Int.negOfNat 3).rawCast + (Real.exp 1 ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))))
(Mathlib.Tactic.Ring.neg_add
(Mathlib.Tactic.Ring.neg_one_mul
(Mathlib.Meta.NormNum.IsNat.to_raw_eq
(Mathlib.Meta.NormNum.IsInt.to_isNat
(Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 3)) (Eq.refl (Int.ofNat 3))))))
(Mathlib.Tactic.Ring.neg_add
(Mathlib.Tactic.Ring.neg_mul (Real.exp 1) (Nat.rawCast 1)
(Mathlib.Tactic.Ring.neg_one_mul
(Mathlib.Meta.NormNum.IsInt.to_raw_eq
(Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1))
(Eq.refl (Int.negOfNat 1))))))
Mathlib.Tactic.Ring.neg_zero)))
(Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.atom_pf (Real.exp 1))
(Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 3)))
(Mathlib.Tactic.Ring.sub_pf
(Mathlib.Tactic.Ring.neg_add
(Mathlib.Tactic.Ring.neg_one_mul
(Mathlib.Meta.NormNum.IsInt.to_raw_eq
(Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 3))
(Eq.refl (Int.negOfNat 3)))))
Mathlib.Tactic.Ring.neg_zero)
(Mathlib.Tactic.Ring.add_pf_add_gt (Int.negOfNat 3).rawCast
(Mathlib.Tactic.Ring.add_pf_add_zero (Real.exp 1 ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))))
(Mathlib.Tactic.Ring.add_pf_add_overlap_zero
(Mathlib.Meta.NormNum.IsInt.to_isNat
(Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 3))
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 3)) (Eq.refl (Int.ofNat 0))))
(Mathlib.Tactic.Ring.add_pf_add_overlap_zero
(Mathlib.Tactic.Ring.add_overlap_pf_zero (Real.exp 1) (Nat.rawCast 1)
(Mathlib.Meta.NormNum.IsInt.to_isNat
(Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1))
(Eq.refl (Int.ofNat 0)))))
(Mathlib.Tactic.Ring.add_pf_zero_add 0))))
(Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero))))
(Mathlib.Tactic.Linarith.lt_of_eq_of_lt (neg_eq_zero.mpr (sub_eq_zero_of_eq a))
(Mathlib.Tactic.Linarith.sub_neg_of_lt Real.exp_one_lt_three)))))c₀:ℝ := -Real.log (distToNearestInt (Real.exp 1)) + 1n:ℕhn:1 ≤ nhn_pos:0 < ↑n := cast (Eq.symm (Eq.trans (congrArg (fun x => x < ↑n) (Eq.symm Nat.cast_zero)) Nat.cast_lt._simp_1)) hnh2:n ≥ 2⊢ -max c c₀ * ↑n ≤ -c * ↑n; All goals completed! 🐙
_ ≤ (n : ℝ) ^ (-c) := c:ℝhc:0 < chyp:∀ (n : ℕ), 2 ≤ n → ↑n ^ (-c) < distToNearestInt (Real.exp ↑n)hd_pos:0 < distToNearestInt (Real.exp 1) :=
Eq.mpr
(id
(congrArg (fun x => 0 < |Real.exp 1 - x|)
(Eq.trans (congrArg Int.cast Real.round_exp_one_eq_three) (Int.cast_ofNat 3))))
(Eq.mpr (id (congrArg (fun _a => _a) (propext abs_pos)))
(Not.intro fun a =>
Mathlib.Tactic.Linarith.lt_irrefl
(Eq.mp
(congrArg (fun _a => _a < 0)
(Mathlib.Tactic.Ring.of_eq
(Mathlib.Tactic.Ring.add_congr
(Mathlib.Tactic.Ring.neg_congr
(Mathlib.Tactic.Ring.sub_congr
(Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.atom_pf (Real.exp 1))
(Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 3)))
(Mathlib.Tactic.Ring.sub_pf
(Mathlib.Tactic.Ring.neg_add
(Mathlib.Tactic.Ring.neg_one_mul
(Mathlib.Meta.NormNum.IsInt.to_raw_eq
(Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 3))
(Eq.refl (Int.negOfNat 3)))))
Mathlib.Tactic.Ring.neg_zero)
(Mathlib.Tactic.Ring.add_pf_add_gt (Int.negOfNat 3).rawCast
(Mathlib.Tactic.Ring.add_pf_add_zero (Real.exp 1 ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))))
(Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero))
(Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_zero
(Mathlib.Tactic.Ring.add_pf_add_zero
((Int.negOfNat 3).rawCast + (Real.exp 1 ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))))
(Mathlib.Tactic.Ring.neg_add
(Mathlib.Tactic.Ring.neg_one_mul
(Mathlib.Meta.NormNum.IsNat.to_raw_eq
(Mathlib.Meta.NormNum.IsInt.to_isNat
(Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 3)) (Eq.refl (Int.ofNat 3))))))
(Mathlib.Tactic.Ring.neg_add
(Mathlib.Tactic.Ring.neg_mul (Real.exp 1) (Nat.rawCast 1)
(Mathlib.Tactic.Ring.neg_one_mul
(Mathlib.Meta.NormNum.IsInt.to_raw_eq
(Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1))
(Eq.refl (Int.negOfNat 1))))))
Mathlib.Tactic.Ring.neg_zero)))
(Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.atom_pf (Real.exp 1))
(Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 3)))
(Mathlib.Tactic.Ring.sub_pf
(Mathlib.Tactic.Ring.neg_add
(Mathlib.Tactic.Ring.neg_one_mul
(Mathlib.Meta.NormNum.IsInt.to_raw_eq
(Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 3))
(Eq.refl (Int.negOfNat 3)))))
Mathlib.Tactic.Ring.neg_zero)
(Mathlib.Tactic.Ring.add_pf_add_gt (Int.negOfNat 3).rawCast
(Mathlib.Tactic.Ring.add_pf_add_zero (Real.exp 1 ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))))
(Mathlib.Tactic.Ring.add_pf_add_overlap_zero
(Mathlib.Meta.NormNum.IsInt.to_isNat
(Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 3))
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 3)) (Eq.refl (Int.ofNat 0))))
(Mathlib.Tactic.Ring.add_pf_add_overlap_zero
(Mathlib.Tactic.Ring.add_overlap_pf_zero (Real.exp 1) (Nat.rawCast 1)
(Mathlib.Meta.NormNum.IsInt.to_isNat
(Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1))
(Eq.refl (Int.ofNat 0)))))
(Mathlib.Tactic.Ring.add_pf_zero_add 0))))
(Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero))))
(Mathlib.Tactic.Linarith.lt_of_eq_of_lt (neg_eq_zero.mpr (sub_eq_zero_of_eq a))
(Mathlib.Tactic.Linarith.sub_neg_of_lt Real.exp_one_lt_three)))))c₀:ℝ := -Real.log (distToNearestInt (Real.exp 1)) + 1n:ℕhn:1 ≤ nhn_pos:0 < ↑n := cast (Eq.symm (Eq.trans (congrArg (fun x => x < ↑n) (Eq.symm Nat.cast_zero)) Nat.cast_lt._simp_1)) hnh2:n ≥ 2⊢ Real.exp (-c * ↑n) ≤ ↑n ^ (-c)
c:ℝhc:0 < chyp:∀ (n : ℕ), 2 ≤ n → ↑n ^ (-c) < distToNearestInt (Real.exp ↑n)hd_pos:0 < distToNearestInt (Real.exp 1) :=
Eq.mpr
(id
(congrArg (fun x => 0 < |Real.exp 1 - x|)
(Eq.trans (congrArg Int.cast Real.round_exp_one_eq_three) (Int.cast_ofNat 3))))
(Eq.mpr (id (congrArg (fun _a => _a) (propext abs_pos)))
(Not.intro fun a =>
Mathlib.Tactic.Linarith.lt_irrefl
(Eq.mp
(congrArg (fun _a => _a < 0)
(Mathlib.Tactic.Ring.of_eq
(Mathlib.Tactic.Ring.add_congr
(Mathlib.Tactic.Ring.neg_congr
(Mathlib.Tactic.Ring.sub_congr
(Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.atom_pf (Real.exp 1))
(Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 3)))
(Mathlib.Tactic.Ring.sub_pf
(Mathlib.Tactic.Ring.neg_add
(Mathlib.Tactic.Ring.neg_one_mul
(Mathlib.Meta.NormNum.IsInt.to_raw_eq
(Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 3))
(Eq.refl (Int.negOfNat 3)))))
Mathlib.Tactic.Ring.neg_zero)
(Mathlib.Tactic.Ring.add_pf_add_gt (Int.negOfNat 3).rawCast
(Mathlib.Tactic.Ring.add_pf_add_zero (Real.exp 1 ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))))
(Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero))
(Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_zero
(Mathlib.Tactic.Ring.add_pf_add_zero
((Int.negOfNat 3).rawCast + (Real.exp 1 ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))))
(Mathlib.Tactic.Ring.neg_add
(Mathlib.Tactic.Ring.neg_one_mul
(Mathlib.Meta.NormNum.IsNat.to_raw_eq
(Mathlib.Meta.NormNum.IsInt.to_isNat
(Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 3)) (Eq.refl (Int.ofNat 3))))))
(Mathlib.Tactic.Ring.neg_add
(Mathlib.Tactic.Ring.neg_mul (Real.exp 1) (Nat.rawCast 1)
(Mathlib.Tactic.Ring.neg_one_mul
(Mathlib.Meta.NormNum.IsInt.to_raw_eq
(Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1))
(Eq.refl (Int.negOfNat 1))))))
Mathlib.Tactic.Ring.neg_zero)))
(Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.atom_pf (Real.exp 1))
(Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 3)))
(Mathlib.Tactic.Ring.sub_pf
(Mathlib.Tactic.Ring.neg_add
(Mathlib.Tactic.Ring.neg_one_mul
(Mathlib.Meta.NormNum.IsInt.to_raw_eq
(Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 3))
(Eq.refl (Int.negOfNat 3)))))
Mathlib.Tactic.Ring.neg_zero)
(Mathlib.Tactic.Ring.add_pf_add_gt (Int.negOfNat 3).rawCast
(Mathlib.Tactic.Ring.add_pf_add_zero (Real.exp 1 ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))))
(Mathlib.Tactic.Ring.add_pf_add_overlap_zero
(Mathlib.Meta.NormNum.IsInt.to_isNat
(Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 3))
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 3)) (Eq.refl (Int.ofNat 0))))
(Mathlib.Tactic.Ring.add_pf_add_overlap_zero
(Mathlib.Tactic.Ring.add_overlap_pf_zero (Real.exp 1) (Nat.rawCast 1)
(Mathlib.Meta.NormNum.IsInt.to_isNat
(Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1))
(Eq.refl (Int.ofNat 0)))))
(Mathlib.Tactic.Ring.add_pf_zero_add 0))))
(Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero))))
(Mathlib.Tactic.Linarith.lt_of_eq_of_lt (neg_eq_zero.mpr (sub_eq_zero_of_eq a))
(Mathlib.Tactic.Linarith.sub_neg_of_lt Real.exp_one_lt_three)))))c₀:ℝ := -Real.log (distToNearestInt (Real.exp 1)) + 1n:ℕhn:1 ≤ nhn_pos:0 < ↑n := cast (Eq.symm (Eq.trans (congrArg (fun x => x < ↑n) (Eq.symm Nat.cast_zero)) Nat.cast_lt._simp_1)) hnh2:n ≥ 2⊢ Real.exp (-c * ↑n) ≤ Real.exp (Real.log ↑n * -c)
exact Real.exp_le_exp.mpr (c:ℝhc:0 < chyp:∀ (n : ℕ), 2 ≤ n → ↑n ^ (-c) < distToNearestInt (Real.exp ↑n)hd_pos:0 < distToNearestInt (Real.exp 1) :=
Eq.mpr
(id
(congrArg (fun x => 0 < |Real.exp 1 - x|)
(Eq.trans (congrArg Int.cast Real.round_exp_one_eq_three) (Int.cast_ofNat 3))))
(Eq.mpr (id (congrArg (fun _a => _a) (propext abs_pos)))
(Not.intro fun a =>
Mathlib.Tactic.Linarith.lt_irrefl
(Eq.mp
(congrArg (fun _a => _a < 0)
(Mathlib.Tactic.Ring.of_eq
(Mathlib.Tactic.Ring.add_congr
(Mathlib.Tactic.Ring.neg_congr
(Mathlib.Tactic.Ring.sub_congr
(Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.atom_pf (Real.exp 1))
(Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 3)))
(Mathlib.Tactic.Ring.sub_pf
(Mathlib.Tactic.Ring.neg_add
(Mathlib.Tactic.Ring.neg_one_mul
(Mathlib.Meta.NormNum.IsInt.to_raw_eq
(Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 3))
(Eq.refl (Int.negOfNat 3)))))
Mathlib.Tactic.Ring.neg_zero)
(Mathlib.Tactic.Ring.add_pf_add_gt (Int.negOfNat 3).rawCast
(Mathlib.Tactic.Ring.add_pf_add_zero (Real.exp 1 ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))))
(Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero))
(Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_zero
(Mathlib.Tactic.Ring.add_pf_add_zero
((Int.negOfNat 3).rawCast + (Real.exp 1 ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))))
(Mathlib.Tactic.Ring.neg_add
(Mathlib.Tactic.Ring.neg_one_mul
(Mathlib.Meta.NormNum.IsNat.to_raw_eq
(Mathlib.Meta.NormNum.IsInt.to_isNat
(Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 3)) (Eq.refl (Int.ofNat 3))))))
(Mathlib.Tactic.Ring.neg_add
(Mathlib.Tactic.Ring.neg_mul (Real.exp 1) (Nat.rawCast 1)
(Mathlib.Tactic.Ring.neg_one_mul
(Mathlib.Meta.NormNum.IsInt.to_raw_eq
(Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1))
(Eq.refl (Int.negOfNat 1))))))
Mathlib.Tactic.Ring.neg_zero)))
(Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.atom_pf (Real.exp 1))
(Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 3)))
(Mathlib.Tactic.Ring.sub_pf
(Mathlib.Tactic.Ring.neg_add
(Mathlib.Tactic.Ring.neg_one_mul
(Mathlib.Meta.NormNum.IsInt.to_raw_eq
(Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 3))
(Eq.refl (Int.negOfNat 3)))))
Mathlib.Tactic.Ring.neg_zero)
(Mathlib.Tactic.Ring.add_pf_add_gt (Int.negOfNat 3).rawCast
(Mathlib.Tactic.Ring.add_pf_add_zero (Real.exp 1 ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))))
(Mathlib.Tactic.Ring.add_pf_add_overlap_zero
(Mathlib.Meta.NormNum.IsInt.to_isNat
(Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 3))
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 3)) (Eq.refl (Int.ofNat 0))))
(Mathlib.Tactic.Ring.add_pf_add_overlap_zero
(Mathlib.Tactic.Ring.add_overlap_pf_zero (Real.exp 1) (Nat.rawCast 1)
(Mathlib.Meta.NormNum.IsInt.to_isNat
(Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1))
(Eq.refl (Int.ofNat 0)))))
(Mathlib.Tactic.Ring.add_pf_zero_add 0))))
(Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero))))
(Mathlib.Tactic.Linarith.lt_of_eq_of_lt (neg_eq_zero.mpr (sub_eq_zero_of_eq a))
(Mathlib.Tactic.Linarith.sub_neg_of_lt Real.exp_one_lt_three)))))c₀:ℝ := -Real.log (distToNearestInt (Real.exp 1)) + 1n:ℕhn:1 ≤ nhn_pos:0 < ↑n := cast (Eq.symm (Eq.trans (congrArg (fun x => x < ↑n) (Eq.symm Nat.cast_zero)) Nat.cast_lt._simp_1)) hnh2:n ≥ 2⊢ -c * ↑n ≤ Real.log ↑n * -c All goals completed! 🐙)
_ < distToNearestInt (Real.exp n) := hyp n h2
end Bugeaud01