kbuzzard

import analysis.real 

def S (a : {n : ℕ // n ≥ 1} → ℝ) 
  (n : ℕ) (H : n ≥ 1) := { r: ℝ | ∃ (m : ℕ) (Hm : m ≥ n), r = a ⟨m,ge_trans Hm H⟩ }

noncomputable def a2 : {n : ℕ // n ≥ 1} → ℝ := λ N, 1/N.val 

def liminf (a : {n : ℕ // n ≥ 1} → ℝ) (linf : ℝ) : Prop :=
  ∃ c : { n : ℕ // n ≥ 1} → ℝ, is_lub { x : ℝ | ∃ (n : ℕ) (H : n ≥ 1), x = c ⟨n,H⟩} linf 
  ∧ ∀ (n : ℕ) (H : n ≥ 1), is_glb (S a n H) (c ⟨n,H⟩) 

kbuzzard

-- m and n (the two numbers on the board) are constant.

-- The possible worlds are pairs (a,b) of nats with a+b=m or a+b=n

structure possible_worlds (m n : ℕ) :=
(a : ℕ) (b : ℕ) (H : a+b=m ∨ a+b=n)

open nat

-- the predicate "beliefs m n t" represents the beliefs (i.e. opinions of the

kbuzzard

def extended_le : option ℕ → option ℕ → Prop
| _ none := true
| none (some n) := false
| (some m) (some n) := m ≤ n

instance : has_le (option ℕ) := ⟨extended_le⟩

lemma none_le_none : (none : option ℕ) ≤ none := trivial

lemma some_le_none (m : ℕ) : (some m) ≤ none := trivial

kbuzzard

import data.multiset

def extended_le : option ℕ → option ℕ → Prop
| _ none := true
| none (some n) := false
| (some m) (some n) := m ≤ n

instance : has_le (option ℕ) := ⟨extended_le⟩

lemma none_le_none : (none : option ℕ) ≤ none := trivial

kbuzzard

import analysis.topology.continuity 

universes u v 

local attribute [class] topological_space.is_open 

structure presheaf_of_types (α : Type*) [T : topological_space α] := 
(F : Π U : set α, T.is_open U → Type*)
(res : ∀ (U V : set α) (OU : T.is_open U) (OV : T.is_open V) (H : V ⊆ U), 
  (F U OU) → (F V OV))

kbuzzard

universes u v 

theorem set.subset.trans {α : Type*} {a b c : set α} (ab : a ⊆ b) (bc : b ⊆ c) : a ⊆ c :=
assume x h, bc (ab h)

def set.preimage {α : Type u} {β : Type v} (f : α → β) (s : set β) : set α := {x | f x ∈ s}
infix ` ⁻¹' `:80 := set.preimage

structure presheaf_of_types (α : Type*) := 
(F : Π U : set α,  Type*)

kbuzzard

goal before show (apply_instance fails)

⊢ @is_ring_hom.{u u} R
    (@localization.away.{u}
       (@localization.loc.{u} R _inst_1 (@powers.{u} R (@ring.to_monoid.{u} R (@comm_ring.to_ring.{u} R _inst_1)) f)
          (@powers.is_submonoid.{u} R (@ring.to_monoid.{u} R (@comm_ring.to_ring.{u} R _inst_1)) f))
       (@localization.comm_ring.{u} R _inst_1
          (@powers.{u} R (@ring.to_monoid.{u} R (@comm_ring.to_ring.{u} R _inst_1)) f)
          (@powers.is_submonoid.{u} R (@ring.to_monoid.{u} R (@comm_ring.to_ring.{u} R _inst_1)) f))
       (@localization.of_comm_ring.{u} R _inst_1

kbuzzard

[class_instances]  class-instance resolution trace
[class_instances] (0) ?x_0 : comm_ring
  (@loc (@loc R _inst_5 (@powers R (@ring.to_monoid R (@comm_ring.to_ring R _inst_5)) f) _)
     (@localization.comm_ring R _inst_5 (@powers R (@ring.to_monoid R (@comm_ring.to_ring R _inst_5)) f) _)
     (@powers (@loc R _inst_5 (@powers R (@ring.to_monoid R (@comm_ring.to_ring R _inst_5)) f) _)
        (@ring.to_monoid (@loc R _inst_5 (@powers R (@ring.to_monoid R (@comm_ring.to_ring R _inst_5)) f) _)
           (@comm_ring.to_ring (@loc R _inst_5 (@powers R (@ring.to_monoid R (@comm_ring.to_ring R _inst_5)) f) _)
              (@localization.comm_ring R _inst_5 (@powers R (@ring.to_monoid R (@comm_ring.to_ring R _inst_5)) f) _)))
        g)
     _) := _inst_6

kbuzzard

-- do I use a section? What even is a section?
-- so I use a namespace? What would a sensible convention be?
-- I don't care about junk like imports at the beginning of files

-- I am trying to write down a really uncluttered proof that 
-- one of the axioms that Lean uses to define a group
-- actually follows from the others.

-- We will build a structure modelling groups as defined by Lean, minus the axiom mul_one.

kbuzzard

X : Type u,
_inst_1 : topological_space.{u} X,
B : set.{u} (set.{u} X),
HB : @topological_space.is_topological_basis.{u} X _inst_1 B,
FPRB : @presheaf_of_rings_on_basis.{u} X _inst_1 B HB,
x : X,
Hstandard :
  ∀ (U V : set.{u} X),
    @has_mem.mem.{u u} (set.{u} X) (set.{u} (set.{u} X)) (@set.has_mem.{u} (set.{u} X)) U B →
    @has_mem.mem.{u u} (set.{u} X) (set.{u} (set.{u} X)) (@set.has_mem.{u} (set.{u} X)) V B →