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],

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

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

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

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

/- All declarations in mathlib that
  * are a lemma/theorem but construct data
  * are a definition, but define an element of a proposition
  
  All automatically generated definitions and all instances are filtered out.
-/

-- topology\uniform_space\uniform_embedding.lean
#print uniform_inducing.mk' -- is a def, should be a lemma/theorem

fpvandoorn

2020-02-03T19:39:15.8860466Z /- TYPES ARE MISSING INHABITED INSTANCES: -/
2020-02-03T19:39:15.8860718Z 
2020-02-03T19:39:15.8861155Z -- topology/topological_fiber_bundle.lean
2020-02-03T19:39:15.8861629Z #print bundle_trivialization /- inhabited instance missing -/
2020-02-03T19:39:15.8867768Z #print topological_fiber_bundle_core /- inhabited instance missing -/
2020-02-03T19:39:15.8867878Z 
2020-02-03T19:39:15.8868166Z -- topology/opens.lean
2020-02-03T19:39:15.8868492Z #print topological_space.nonempty_compacts /- inhabited instance missing -/
2020-02-03T19:39:15.8868820Z #print topological_space.closeds /- inhabited instance missing -/
2020-02-03T19:39:15.8868884Z 

fpvandoorn

import tactic -- all

open tactic declaration environment native

meta def pos_line (p : option pos) : string :=
match p with
| some x := to_string x.line
| _      := ""
end

fpvandoorn

/- Checking 74465 declarations (plus 74875 automatically generated ones) in mathlib (only in imported files) -/

/- The `check_type` linter reports: -/
/- THE STATEMENTS OF THE FOLLOWING DECLARATIONS DO NOT TYPE-CHECK.
Some definitions in the statement are marked @[irreducible], which means that the statement is now ill-formed. It is likely that these definitions were locally marked @[reducible], and that type-class instances were applied that don't apply when the definitions are @[irreducible].: -/
-- algebra\category\Mon\adjunctions.lean
#print adjoin_one.equations._eqn_1 /- The statement doesn't type-check -/
#print adjoin_zero_map /- The statement doesn't type-check -/
#print adjoin_zero.equations._eqn_1 /- The statement doesn't type-check -/
#print adjoin_one_map /- The statement doesn't type-check -/

fpvandoorn

 antitone.const_mul' ← antitone.const_add,
 finset.prod_powerset_insert ← finset.sum_powerset_insert,
 dist_eq_norm_div' ← dist_eq_norm_sub',
 units.is_unit_mul_units ← add_units.is_add_unit_add_add_units,
 Group.filtered_colimits.colimit_has_inv ← AddGroup.filtered_colimits.colimit_has_neg,
 unique_mul.exists_iff_exists_exists_unique ← unique_add.exists_iff_exists_exists_unique,
 subsemigroup.mem_map ← add_subsemigroup.mem_map,
 free_group.norm ← free_add_group.norm,
 finset.prod_ite_index ← finset.sum_ite_index,
 monoid_hom.to_localization_map ← add_monoid_hom.to_localization_map,