fpvandoorn

import ring_theory.multiplicity algebra.big_operators tactic.default data.rat.basic
  .two_adic_val_fact

/- two_adic_val_fact.lean is located here:
https://gist.githubusercontent.com/kbuzzard/4ca88f429bda4744fd038f7471ebfb67/raw/5fa02ec9f5f2b5edf5020cb20c44167a648e0514/two_adic_val_fact.lean
-/

universe variables u v

open finset

fpvandoorn

-- this Git is supposed to be used on branch sanity_check
-- You have to run the script "scripts/mk_all.sh", and then this file should compile.
-- The list after each declaration gives all the positions of the unused arguments (starting at 1). E.g. [2] means that the second argument is unused.
import all

#sanity_check_mathlib

-- topology\uniform_space\uniform_embedding.lean
#print uniformly_extend_exists -- [7]

fpvandoorn

/-
Copyright (c) 2019 Floris van Doorn. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Floris van Doorn

---

Proof that a cube (in dimension n ≥ 3) cannot be cubed:
there does not exist a partition of a cube into finitely many smaller cubes (at least two)
of different sizes.

fpvandoorn

import data.real.pi

set_option profiler true

namespace real

lemma sqrt_two_add_series_step_up' {x z : ℝ} {n : ℕ} (y : ℝ) (hz : sqrt_two_add_series y n ≤ z)
  (h : 2 + x ≤ y ^ 2) (h2 : 0 ≤ y) : sqrt_two_add_series x (n+1) ≤ z :=
begin
  refine le_trans _ hz, rw [sqrt_two_add_series_succ], apply sqrt_two_add_series_monotone_left,

fpvandoorn

import data.real.pi

set_option profiler true

set_option timeout 1000000
namespace real
-- the following lemma takes about 9 seconds
lemma pi_gt_31415 : pi > 3.1415 :=
begin
  refine lt_of_le_of_lt _ (pi_gt_sqrt_two_add_series 6), rw [mul_comm],