kbuzzard

import tactic

-- need to teach pairs

-- (3, 6) : ℕ × ℕ
-- x.1 is first element of x, x.2 is second

/-- The equivalence relation on ℕ² such that equivalence classes are ℤ -/
def nat2.R (a b : ℕ × ℕ) : Prop :=
a.1 + b.2 = b.1 + a.2

kbuzzard

/- Theory of presheaves (of objects of a category) on a topological space

cf :   https://stacks.math.columbia.edu/tag/006D

Notes: KMB has never really understood whether we should be using
category theory or not when working with sheaves on a topological space.
By explicitly avoiding this and doing everything from first principles
on the topological space side, but letting sheaves take values which are
objects of a general category is certainly something we want to do.

kbuzzard

[class_instances]  class-instance resolution trace
[class_instances] (0) ?x_0 : has_mul G := @ideal.has_mul ?x_1 ?x_2
failed is_def_eq
[class_instances] (0) ?x_0 : has_mul G := @submodule.has_mul ?x_3 ?x_4 ?x_5 ?x_6 ?x_7
failed is_def_eq
[class_instances] (0) ?x_0 : has_mul G := @matrix.has_mul ?x_8 ?x_9 ?x_10 ?x_11 ?x_12
failed is_def_eq
[class_instances] (0) ?x_0 : has_mul G := complex.has_mul
failed is_def_eq
[class_instances] (0) ?x_0 : has_mul G := snum.has_mul

kbuzzard

[class_instances]  class-instance resolution trace
[class_instances] (0) ?x_0 : has_scalar k V := @continuous_linear_map.has_scalar ?x_1 ?x_2 ?x_3 ?x_4 ?x_5 ?x_6 ?x_7 ?x_8 ?x_9 ?x_10 ?x_11 ?x_12
failed is_def_eq
[class_instances] (0) ?x_0 : has_scalar k V := complex.has_scalar
failed is_def_eq
[class_instances] (0) ?x_0 : has_scalar k V := @algebra.comap.has_scalar ?x_13 ?x_14 ?x_15 ?x_16 ?x_17 ?x_18 ?x_19 ?x_20
failed is_def_eq
[class_instances] (0) ?x_0 : has_scalar k V := @algebra.has_scalar ?x_21 ?x_22 ?x_23 ?x_24 ?x_25
[class_instances] (1) ?x_23 : comm_ring k := @subalgebra.comm_ring ?x_26 ?x_27 ?x_28 ?x_29 ?x_30 ?x_31
failed is_def_eq

kbuzzard

import order.conditionally_complete_lattice

open lattice

open_locale classical

/- with_top -/

noncomputable instance with_top.conditionally_complete_lattice.has_Sup
  {α : Type*} [conditionally_complete_lattice α] : has_Sup (with_top α) :=

kbuzzard

import data.real.basic 

/-- ereal : The set $$[-\infty,+\infty]$$ -/
def ereal := with_bot (with_top ℝ)

instance : linear_order ereal := 
by unfold ereal; apply_instance
instance : lattice.has_top ereal := 
by unfold ereal; apply_instance
instance : lattice.has_bot ereal :=

kbuzzard

import data.padics imo2019_4

instance two_prime : nat.prime 2 := by norm_num

lemma aux1 (n : ℕ) : padic_val_rat 2 (n + 1).fact = padic_val_rat 2 (n + 1) + padic_val_rat 2 n.fact :=
begin
  rw (show (n + 1).fact = (n + 1) * n.fact, from rfl),
  rw nat.cast_mul,
  rw padic_val_rat.mul 2,
  refl,

kbuzzard

-- this was compiling with mathlib in June 2020
import tactic

theorem imo2019Q1 (f : ℤ → ℤ) :
(∀ a b : ℤ, f (2 * a) + 2 * (f b) = f (f (a + b))) ↔
(∀ x, f x = 0) ∨ ∃ c, ∀ x, f x = 2 * x + c :=
begin
  split, swap,
  { -- easy way: f(x)=0 and f(x)=2x+c work.
    intro h,

kbuzzard

open tactic

meta def copy_decl (d : declaration) : tactic unit :=
add_decl $ d.update_name $ d.to_name.update_prefix `kevin.interactive

@[reducible] meta def filter (d : declaration) : bool :=
d.to_name ∉ [`tactic.interactive.induction]

meta def copy_decls : tactic unit :=
do env ← get_env,

kbuzzard

lean-perfectoid-spaces/src$ git grep \^class\
Huber_ring/basic.lean:class Huber_ring (A : Type u) extends comm_ring A, topological_space A, topological_ring A :=
Tate_ring.lean:class Tate_ring (R : Type u) [Huber_ring R] : Prop :=
for_mathlib/linear_ordered_comm_group.lean:class linear_ordered_comm_monoid (α : Type*) extends comm_monoid α, linear_order α :=
for_mathlib/linear_ordered_comm_group.lean:class linear_ordered_comm_group (α : Type*) extends comm_group α, linear_ordered_comm_monoid α
for_mathlib/linear_ordered_comm_group.lean:class linear_ordered_comm_monoid.is_hom (f : α → β) extends is_monoid_hom f : Prop :=
for_mathlib/linear_ordered_comm_group.lean:class linear_ordered_comm_group.is_hom (f : α → β) extends is_group_hom f : Prop :=
for_mathlib/linear_ordered_comm_group.lean:class is_convex (S : set α) : Prop :=
for_mathlib/linear_ordered_comm_group.lean:class is_proper_convex (S : set α) extends is_convex S : Prop :=
for_mathlib/linear_ordered_comm_group.lean:class actual_ordered_comm_monoid (α :