shingtaklam1324

import data.equiv.fin
import group_theory.perm.cycle_type
import group_theory.perm.fin

@[simp] lemma fin.val_mod (n : ℕ) (i : fin n) : (i : ℕ) % n = (i : ℕ) :=
begin
  apply nat.mod_eq_of_lt,
  exact fin.is_lt i,
end

shingtaklam1324

import Lean
open Lean Macro

universes u v

class Mem (α : outParam $ Type u) (γ : Type v) where
  mem : α → γ → Prop

infix:50 " ∈ " => Mem.mem

shingtaklam1324

import data.real.basic

@[ext]
structure quantity (L M T I Θ N J : ℚ) := (x : ℚ) -- reals are noncomputable so I'm using `ℚ` here 

namespace quantity

variables {l m t i θ n j : ℚ}
variables {l' m' t' i' θ' n' j' : ℚ}

shingtaklam1324

import tactic
import data.real.basic
import topology.metric_space.basic

notation `|` x `|` := abs x

namespace epsilon_delta

/-!
## Epsilon-Delta - Motivation for Filters

shingtaklam1324

-- Stuff that's not there yet

class One (α : Type u) where
  one : α

instance [One α] : OfNat α (natLit! 1) where
  ofNat := One.one

class Inv (α : Type u) where

shingtaklam1324

open Nat (succ addSucc addZero mulZero mulSucc powZero powSucc)

/-
# Natural Number Game - Lean 4

Right now, all levels have been ported over, although this is using Lean 4's builtin
`Nat`, so some of the Lemmas have been changed slightly, and there is one `sorry` as
the definition of `≤` in Lean 3/4 is different to the one used in the NNG.
-/

shingtaklam1324

import algebra.archimedean
import tactic

open_locale classical
noncomputable theory

/-!

# Definition of the Reals, as cuts of the rationals

shingtaklam1324

import group_theory.subgroup
import group_theory.coset
import group_theory.order_of_element
import tactic
import data.zmod.basic

variables (G : Type) [fintype G] [group G] (H : subgroup G)

lemma subgroup.eq_top_of_card_eq (h : fintype.card H = fintype.card G) : H = ⊤ :=
begin

shingtaklam1324

private meta def show_aux (p : pexpr) : -- p is the type which we want to change the goal to
  list expr →                          -- The list of all of the goals
  list expr →                          -- and the list of goals we've already tried
  tactic unit
| []      r := fail "show tactic failed" -- If there are no goals left to try, then fail
| (g::gs) r := do
  do {
    set_goals [g],                    -- Ignore every goal except the first one
    g_ty ← target,                   -- get the type of the goal
    ty ← i_to_expr p,                -- get the type of the expression being passed into show

shingtaklam1324

/-
Copyright (c) 2019 Kevin Buzzard. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Kevin Buzzard
-/

import algebra.archimedean tactic.linarith

/-