lean4-htt/tests/lean/Reformat.lean.expected.out

prelude 

notation `Prop` := Sort 0

reserve infixr ` $ `:1

notation f ` $ ` a := f a 

reserve prefix `¬`:40

reserve infixr ` ∧ `:35

reserve infixr ` /\ `:35

reserve infixr ` \/ `:30

reserve infixr ` ∨ `:30

reserve infix ` <-> `:20

reserve infix ` ↔ `:20

reserve infix ` = `:50

reserve infix ` == `:50

reserve infix ` != `:50

reserve infix ` ~= `:50

reserve infix ` ≅ `:50

reserve infix ` ≠ `:50

reserve infix ` ≈ `:50

reserve infixr ` ▸ `:75

reserve infixr ` × `:35

reserve infixl ` + `:65

reserve infixl ` - `:65

reserve infixl ` * `:70

reserve infixl ` / `:70

reserve infixl ` % `:70

reserve infixl ` %ₙ `:70

reserve prefix `-`:100

reserve infixr ` ^ `:80

reserve infixr ` ∘ `:90

reserve infix ` <= `:50

reserve infix ` ≤ `:50

reserve infix ` < `:50

reserve infix ` >= `:50

reserve infix ` ≥ `:50

reserve infix ` > `:50

reserve prefix `!`:40

reserve infixl ` && `:35

reserve infixl ` || `:30

reserve infixl ` ++ `:65

reserve infixr ` :: `:67

reserve infixr ` <|> `:2

reserve infixl ` >>= `:55

reserve infixr ` >=> `:55

reserve infixl ` <*> `:60

reserve infixl ` <* `:60

reserve infixr ` *> `:60

reserve infixr ` >> `:60

reserve infixr ` <$> `:100

reserve infixl ` <&> `:100

universes u v w

/--Auxiliary unsafe constant used by the Compiler when erasing proofs from code. -/
unsafe axiom lcProof {α : Prop} : α

/--Auxiliary unsafe constant used by the Compiler to mark unreachable code. -/
unsafe axiom lcUnreachable {α : Sort u} : α

@[inline]
def id {α : Sort u} (a : α) : α :=
a 

def inline {α : Sort u} (a : α) : α :=
a

@[inline]
def flip {α : Sort u} {β : Sort v} {φ : Sort w} (f : α → β → φ) : β → α → φ :=
fun b a => f a b

@[inline]
def idDelta {α : Sort u} (a : α) : α :=
a

/--Gadget for optional parameter support. -/
@[reducible]
def optParam (α : Sort u) (default : α) : Sort u :=
α

/--Gadget for marking output parameters in type classes. -/
@[reducible]
def outParam (α : Sort u) : Sort u :=
α

/--Auxiliary Declaration used to implement the notation (a : α) -/
@[reducible]
def typedExpr (α : Sort u) (a : α) : α :=
a

@[macroInline, reducible]
def idRhs (α : Sort u) (a : α) : α :=
a

/--Auxiliary Declaration used to implement the named patterns `x@p` -/
@[reducible]
def namedPattern {α : Sort u} (x a : α) : α :=
a 

inductive PUnit : Sort u
| unit : PUnit

/--An abbreviation for `PUnit.{0}`, its most common instantiation.
    This Type should be preferred over `PUnit` where possible to avoid
    unnecessary universe parameters. -/
abbrev Unit : Type :=
PUnit

@[matchPattern]
abbrev Unit.unit : Unit :=
PUnit.unit 

structure Thunk(α : Type u) : Type u := 
(fn : Unit → α)

attribute [extern "lean_mk_thunk"] Thunk.mk

@[noinline, extern "lean_thunk_pure"]
protected def Thunk.pure {α : Type u} (a : α) : Thunk α :=
⟨fun _ => a⟩

@[noinline, extern "lean_thunk_get_own"]
protected def Thunk.get {α : Type u} (x : @&Thunk α) : α :=
x.fn ()

@[noinline, extern "lean_thunk_map"]
protected def Thunk.map {α : Type u} {β : Type v} (f : α → β) (x : Thunk α) : Thunk β :=
⟨fun _ => f x.get⟩

@[noinline, extern "lean_thunk_bind"]
protected def Thunk.bind {α : Type u} {β : Type v} (x : Thunk α) (f : α → Thunk β) : Thunk β :=
⟨fun _ => (f x.get).get⟩

inductive True : Prop
| intro : True 

inductive False : Prop 

inductive Empty : Type 

def Not (a : Prop) : Prop :=
a → False 

prefix `¬` := Not 

inductive Eq {α : Sort u} (a : α) : α → Prop
| refl{} : Eq a

@[elabAsEliminator, inline, reducible]
def Eq.ndrec.{u1, u2} {α : Sort u2} {a : α} {C : α → Sort u1} (m : C a) {b : α} (h : Eq a b) : C b :=
@Eq.rec α a (fun α _ => C α) m b h

@[elabAsEliminator, inline, reducible]
def Eq.ndrecOn.{u1, u2} {α : Sort u2} {a : α} {C : α → Sort u1} {b : α} (h : Eq a b) (m : C a) : C b :=
@Eq.rec α a (fun α _ => C α) m b h 

init_quot 

inductive HEq {α : Sort u} (a : α) : ∀  {β : Sort u}, β → Prop
| refl{} : HEq a 

structure Prod(α : Type u)(β : Type v) := 
(fst : α)
(snd : β)

attribute [unbox] Prod

/--Similar to `Prod`, but `α` and `β` can be propositions.
   We use this Type internally to automatically generate the brecOn recursor. -/
structure PProd(α : Sort u)(β : Sort v) := 
(fst : α)
(snd : β)

/--Similar to `Prod`, but `α` and `β` are in the same universe. -/
structure MProd(α β : Type u) := 
(fst : α)
(snd : β)

structure And(a b : Prop) : Prop := intro :: 
(left : a)
(right : b)

structure Iff(a b : Prop) : Prop := intro :: 
(mp : a → b)
(mpr : b → a)

infix `=` := Eq

@[matchPattern]
def rfl {α : Sort u} {a : α} : a = a :=
Eq.refl a

@[elabAsEliminator]
theorem Eq.subst {α : Sort u} {P : α → Prop} {a b : α} (h₁ : a = b) (h₂ : P a) : P b :=
Eq.ndrec h₂ h₁ 

infixr `▸` := Eq.subst 

theorem Eq.trans {α : Sort u} {a b c : α} (h₁ : a = b) (h₂ : b = c) : a = c :=
h₂ ▸ h₁ 

theorem Eq.symm {α : Sort u} {a b : α} (h : a = b) : b = a :=
h ▸ rfl 

infix `~=` := HEq 

infix `≅` := HEq

@[matchPattern]
def HEq.rfl {α : Sort u} {a : α} : a ≅ a :=
HEq.refl a 

theorem eqOfHEq {α : Sort u} {a a' : α} (h : a ≅ a') : a = a' :=
have ∀  (α' : Sort u) (a' : α') (h₁ : @HEq α a α' a') (h₂ : α = α'), (Eq.recOn h₂ a : α') = a' :=
  fun (α' : Sort u) (a' : α') (h₁ : @HEq α a α' a') => HEq.recOn h₁ (fun (h₂ : α = α) => rfl);
show (Eq.ndrecOn (Eq.refl α) a : α) = a' from this α a' h (Eq.refl α)

inductive Sum (α : Type u) (β : Type v)
| inl (val : α) : Sum
| inr (val : β) : Sum 

inductive PSum (α : Sort u) (β : Sort v)
| inl (val : α) : PSum
| inr (val : β) : PSum 

inductive Or (a b : Prop) : Prop
| inl (h : a) : Or
| inr (h : b) : Or 

def Or.introLeft {a : Prop} (b : Prop) (ha : a) : Or a b :=
Or.inl ha 

def Or.introRight (a : Prop) {b : Prop} (hb : b) : Or a b :=
Or.inr hb 

structure Sigma{α : Type u}(β : α → Type v) := mk :: 
(fst : α)
(snd : β fst)

attribute [unbox] Sigma 

structure PSigma{α : Sort u}(β : α → Sort v) := mk :: 
(fst : α)
(snd : β fst)

inductive Bool : Type
| false : Bool
| true : Bool 

structure Subtype{α : Sort u}(p : α → Prop) := 
(val : α)
(property : p val)

inductive Exists {α : Sort u} (p : α → Prop) : Prop
| intro (w : α) (h : p w) : Exists 

inductive ForInStep (α : Type u)
| done : α → ForInStep
| yield : α → ForInStep 

inductive DoResultPRBC (α β σ : Type u)
| «pure» : α → σ → DoResultPRBC
| «return» : β → σ → DoResultPRBC
| «break» : σ → DoResultPRBC
| «continue» : σ → DoResultPRBC 

inductive DoResultPR (α β σ : Type u)
| «pure» : α → σ → DoResultPR
| «return» : β → σ → DoResultPR 

inductive DoResultBC (σ : Type u)
| «break» : σ → DoResultBC
| «continue» : σ → DoResultBC 

inductive DoResultSBC (α σ : Type u)
| «pureReturn» : α → σ → DoResultSBC
| «break» : σ → DoResultSBC
| «continue» : σ → DoResultSBC 

class inductive Decidable (p : Prop)
  | isFalse (h : ¬p) : Decidable
  | isTrue (h : p) : Decidable 

abbrev DecidablePred {α : Sort u} (r : α → Prop) :=
∀  (a : α), Decidable (r a)

abbrev DecidableRel {α : Sort u} (r : α → α → Prop) :=
∀  (a b : α), Decidable (r a b)

abbrev DecidableEq (α : Sort u) :=
∀  (a b : α), Decidable (a = b)

def decEq {α : Sort u} [s : DecidableEq α] (a b : α) : Decidable (a = b) :=
s a b 

inductive Option (α : Type u)
| none : Option
| some (val : α) : Option 

attribute [unbox] Option 

export Option(none some)

export Bool(false true)

inductive List (T : Type u)
| nil : List
| cons (hd : T) (tl : List) : List 

infixr `::` := List.cons 

inductive Nat
| zero : Nat
| succ (n : Nat) : Nat 

axiom sorryAx (α : Sort u) (synthetic := true) : α 

class HasZero(α : Type u) := mk{} :: 
(zero : α)

class HasOne(α : Type u) := mk{} :: 
(one : α)

class HasAdd(α : Type u) := 
(add : α → α → α)

class HasMul(α : Type u) := 
(mul : α → α → α)

class HasNeg(α : Type u) := 
(neg : α → α)

class HasSub(α : Type u) := 
(sub : α → α → α)

class HasDiv(α : Type u) := 
(div : α → α → α)

class HasMod(α : Type u) := 
(mod : α → α → α)

class HasModN(α : Type u) := 
(modn : α → Nat → α)

class HasLessEq(α : Type u) := 
(LessEq : α → α → Prop)

class HasLess(α : Type u) := 
(Less : α → α → Prop)

class HasBeq(α : Type u) := 
(beq : α → α → Bool)

class HasAppend(α : Type u) := 
(append : α → α → α)

class HasOrelse(α : Type u) := 
(orelse : α → α → α)

class HasAndthen(α : Type u) := 
(andthen : α → α → α)

class HasEquiv(α : Sort u) := 
(Equiv : α → α → Prop)

class HasEmptyc(α : Type u) := 
(emptyc : α)

class HasPow(α : Type u)(β : Type v) := 
(pow : α → β → α)

infix `+` := HasAdd.add 

infix `*` := HasMul.mul 

infix `-` := HasSub.sub 

infix `/` := HasDiv.div 

infix `%` := HasMod.mod 

infix `%ₙ` := HasModN.modn 

prefix `-` := HasNeg.neg 

infix `<=` := HasLessEq.LessEq 

infix `≤` := HasLessEq.LessEq 

infix `<` := HasLess.Less 

infix `==` := HasBeq.beq 

infix `++` := HasAppend.append 

notation `∅` := HasEmptyc.emptyc 

infix `≈` := HasEquiv.Equiv 

infixr `^` := HasPow.pow 

infixr `/\` := And 

infixr `∧` := And 

infixr `\/` := Or 

infixr `∨` := Or 

infix `<->` := Iff 

infix `↔` := Iff 

infixr `<|>` := HasOrelse.orelse 

infixr `>>` := HasAndthen.andthen

@[reducible]
def GreaterEq {α : Type u} [HasLessEq α] (a b : α) : Prop :=
HasLessEq.LessEq b a

@[reducible]
def Greater {α : Type u} [HasLess α] (a b : α) : Prop :=
HasLess.Less b a 

infix `>=` := GreaterEq 

infix `≥` := GreaterEq 

infix `>` := Greater

@[inline]
def bit0 {α : Type u} [s : HasAdd α] (a : α) : α :=
a + a

@[inline]
def bit1 {α : Type u} [s₁ : HasOne α] [s₂ : HasAdd α] (a : α) : α :=
(bit0 a) + 1

attribute [matchPattern] HasZero.zero HasOne.one bit0 bit1 HasAdd.add HasNeg.neg

@[extern "lean_nat_add"]
protected def Nat.add : (@&Nat) → (@&Nat) → Nat
| a, Nat.zero => a
| a, Nat.succ b => Nat.succ (Nat.add a b)

attribute [matchPattern] Nat.add Nat.add._main 

instance  : HasZero Nat :=
⟨Nat.zero⟩

instance  : HasOne Nat :=
⟨Nat.succ (Nat.zero)⟩

instance  : HasAdd Nat :=
⟨Nat.add⟩

constant hugeFuel : Nat :=
10000

def std.priority.default : Nat :=
1000

def std.priority.max : Nat :=
0xFFFFFFFF

protected def Nat.prio :=
std.priority.default + 100

def std.prec.max : Nat :=
1024

def std.prec.arrow : Nat :=
25

def std.prec.maxPlus : Nat :=
std.prec.max + 10

structure Task(α : Type u) : Type u := pure :: 
(get : α)

attribute [extern "lean_task_pure"] Task.pure 

attribute [extern "lean_task_get_own"] Task.get 

namespace Task

/--Task priority. Tasks with higher priority will always be scheduled before ones with lower priority. -/
abbrev Priority :=
Nat 

def Priority.default : Priority :=
0

def Priority.max : Priority :=
8

/--Any priority higher than `Task.Priority.max` will result in the task being scheduled immediately on a dedicated thread.
  This is particularly useful for long-running and/or I/O-bound tasks since Lean will by default allocate no more
  non-dedicated workers than the number of cores to reduce context switches. -/
def Priority.dedicated : Priority :=
9

@[noinline, extern "lean_task_spawn"]
protected def spawn {α : Type u} (fn : Unit → α) (prio := Priority.default) : Task α :=
⟨fn ()⟩

@[noinline, extern "lean_task_map"]
protected def map {α : Type u} {β : Type v} (f : α → β) (x : Task α) (prio := Priority.default) : Task β :=
⟨f x.get⟩

@[noinline, extern "lean_task_bind"]
protected def bind {α : Type u} {β : Type v} (x : Task α) (f : α → Task β) (prio := Priority.default) : Task β :=
⟨(f x.get).get⟩

end Task 

infixr `×` := Prod 

structure NonScalar := 
(val : Nat)

inductive PNonScalar : Type u
| mk (v : Nat) : PNonScalar 

class HasOfNat(α : Type u) := 
(ofNat : Nat → α)

export HasOfNat(ofNat)

instance  : HasOfNat Nat :=
⟨id⟩

class HasSizeof(α : Sort u) := 
(sizeof : α → Nat)

export HasSizeof(sizeof)

protected def default.sizeof (α : Sort u) : α → Nat
| a => 0

instance defaultHasSizeof (α : Sort u) : HasSizeof α :=
⟨default.sizeof α⟩

protected def Nat.sizeof : Nat → Nat
| n => n 

instance  : HasSizeof Nat :=
⟨Nat.sizeof⟩

protected def Prod.sizeof {α : Type u} {β : Type v} [HasSizeof α] [HasSizeof β] : (Prod α β) → Nat
| ⟨a, b⟩ => 1 + sizeof a + sizeof b 

instance  (α : Type u) (β : Type v) [HasSizeof α] [HasSizeof β] : HasSizeof (Prod α β) :=
⟨Prod.sizeof⟩

protected def Sum.sizeof {α : Type u} {β : Type v} [HasSizeof α] [HasSizeof β] : (Sum α β) → Nat
| Sum.inl a => 1 + sizeof a
| Sum.inr b => 1 + sizeof b 

instance  (α : Type u) (β : Type v) [HasSizeof α] [HasSizeof β] : HasSizeof (Sum α β) :=
⟨Sum.sizeof⟩

protected def PSum.sizeof {α : Type u} {β : Type v} [HasSizeof α] [HasSizeof β] : (PSum α β) → Nat
| PSum.inl a => 1 + sizeof a
| PSum.inr b => 1 + sizeof b 

instance  (α : Type u) (β : Type v) [HasSizeof α] [HasSizeof β] : HasSizeof (PSum α β) :=
⟨PSum.sizeof⟩

protected def Sigma.sizeof {α : Type u} {β : α → Type v} [HasSizeof α] [∀  a, HasSizeof (β a)] : Sigma β → Nat
| ⟨a, b⟩ => 1 + sizeof a + sizeof b 

instance  (α : Type u) (β : α → Type v) [HasSizeof α] [∀  a, HasSizeof (β a)] : HasSizeof (Sigma β) :=
⟨Sigma.sizeof⟩

protected def PSigma.sizeof {α : Type u} {β : α → Type v} [HasSizeof α] [∀  a, HasSizeof (β a)] : PSigma β → Nat
| ⟨a, b⟩ => 1 + sizeof a + sizeof b 

instance  (α : Type u) (β : α → Type v) [HasSizeof α] [∀  a, HasSizeof (β a)] : HasSizeof (PSigma β) :=
⟨PSigma.sizeof⟩

protected def PUnit.sizeof : PUnit → Nat
| u => 1

instance  : HasSizeof PUnit :=
⟨PUnit.sizeof⟩

protected def Bool.sizeof : Bool → Nat
| b => 1

instance  : HasSizeof Bool :=
⟨Bool.sizeof⟩

protected def Option.sizeof {α : Type u} [HasSizeof α] : Option α → Nat
| none => 1
| some a => 1 + sizeof a 

instance  (α : Type u) [HasSizeof α] : HasSizeof (Option α) :=
⟨Option.sizeof⟩

protected def List.sizeof {α : Type u} [HasSizeof α] : List α → Nat
| List.nil => 1
| List.cons a l => 1 + sizeof a + List.sizeof l 

instance  (α : Type u) [HasSizeof α] : HasSizeof (List α) :=
⟨List.sizeof⟩

protected def Subtype.sizeof {α : Type u} [HasSizeof α] {p : α → Prop} : Subtype p → Nat
| ⟨a, _⟩ => sizeof a 

instance  {α : Type u} [HasSizeof α] (p : α → Prop) : HasSizeof (Subtype p) :=
⟨Subtype.sizeof⟩

theorem natAddZero (n : Nat) : n + 0 = n :=
rfl 

theorem optParamEq (α : Sort u) (default : α) : optParam α default = α :=
rfl

/--Like `by applyInstance`, but not dependent on the tactic framework. -/
@[reducible]
def inferInstance {α : Type u} [i : α] : α :=
i

@[reducible, elabSimple]
def inferInstanceAs (α : Type u) [i : α] : α :=
i

@[macroInline]
def cond {a : Type u} : Bool → a → a → a
| true, x, y => x
| false, x, y => y

@[inline]
def condEq {β : Sort u} (b : Bool) (h₁ : b = true → β) (h₂ : b = false → β) : β :=
@Bool.casesOn (λ x => b = x → β) b h₂ h₁ rfl

@[macroInline]
def or : Bool → Bool → Bool
| true, _ => true
| false, b => b

@[macroInline]
def and : Bool → Bool → Bool
| false, _ => false
| true, b => b

@[macroInline]
def not : Bool → Bool
| true => false
| false => true

@[macroInline]
def xor : Bool → Bool → Bool
| true, b => not b
| false, b => b 

prefix `!` := not 

infix `||` := or 

infix `&&` := and

@[extern c inline "#1 || #2"]
def strictOr (b₁ b₂ : Bool) :=
b₁ || b₂

@[extern c inline "#1 && #2"]
def strictAnd (b₁ b₂ : Bool) :=
b₁ && b₂

@[inline]
def bne {α : Type u} [HasBeq α] (a b : α) : Bool :=
!(a == b)

infix `!=` := bne 

def implies (a b : Prop) :=
a → b 

theorem implies.trans {p q r : Prop} (h₁ : implies p q) (h₂ : implies q r) : implies p r :=
fun hp => h₂ (h₁ hp)

def trivial : True :=
⟨⟩

@[macroInline]
def False.elim {C : Sort u} (h : False) : C :=
False.rec (fun _ => C) h

@[macroInline]
def absurd {a : Prop} {b : Sort v} (h₁ : a) (h₂ : ¬a) : b :=
False.elim (h₂ h₁)

theorem mt {a b : Prop} (h₁ : a → b) (h₂ : ¬b) : ¬a :=
fun ha => h₂ (h₁ ha)

theorem notFalse : ¬False :=
id 

theorem proofIrrel {a : Prop} (h₁ h₂ : a) : h₁ = h₂ :=
rfl 

theorem id.def {α : Sort u} (a : α) : id a = a :=
rfl

@[macroInline]
def Eq.mp {α β : Sort u} (h₁ : α = β) (h₂ : α) : β :=
Eq.recOn h₁ h₂

@[macroInline]
def Eq.mpr {α β : Sort u} : (α = β) → β → α :=
fun h₁ h₂ => Eq.recOn (Eq.symm h₁) h₂

@[elabAsEliminator]
theorem Eq.substr {α : Sort u} {p : α → Prop} {a b : α} (h₁ : b = a) (h₂ : p a) : p b :=
Eq.subst (Eq.symm h₁) h₂ 

theorem congr {α : Sort u} {β : Sort v} {f₁ f₂ : α → β} {a₁ a₂ : α} (h₁ : f₁ = f₂) (h₂ : a₁ = a₂) : f₁ a₁ = f₂ a₂ :=
Eq.subst h₁ (Eq.subst h₂ rfl)

theorem congrFun {α : Sort u} {β : α → Sort v} {f g : ∀  x, β x} (h : f = g) (a : α) : f a = g a :=
Eq.subst h (Eq.refl (f a))

theorem congrArg {α : Sort u} {β : Sort v} {a₁ a₂ : α} (f : α → β) (h : a₁ = a₂) : f a₁ = f a₂ :=
congr rfl h 

theorem transRelLeft {α : Sort u} {a b c : α} (r : α → α → Prop) (h₁ : r a b) (h₂ : b = c) : r a c :=
h₂ ▸ h₁ 

theorem transRelRight {α : Sort u} {a b c : α} (r : α → α → Prop) (h₁ : a = b) (h₂ : r b c) : r a c :=
h₁.symm ▸ h₂ 

theorem ofEqTrue {p : Prop} (h : p = True) : p :=
h.symm ▸ trivial 

theorem notOfEqFalse {p : Prop} (h : p = False) : ¬p :=
fun hp => h ▸ hp

@[macroInline]
def cast {α β : Sort u} (h : α = β) (a : α) : β :=
Eq.rec a h 

theorem castProofIrrel {α β : Sort u} (h₁ h₂ : α = β) (a : α) : cast h₁ a = cast h₂ a :=
rfl 

theorem castEq {α : Sort u} (h : α = α) (a : α) : cast h a = a :=
rfl

@[reducible]
def Ne {α : Sort u} (a b : α) :=
¬(a = b)

infix `≠` := Ne 

theorem Ne.def {α : Sort u} (a b : α) : a ≠ b = ¬(a = b) :=
rfl 

section Ne 

variable{α : Sort u}

variables{a b : α}{p : Prop}

theorem Ne.intro (h : a = b → False) : a ≠ b :=
h 

theorem Ne.elim (h : a ≠ b) : a = b → False :=
h 

theorem Ne.irrefl (h : a ≠ a) : False :=
h rfl 

theorem Ne.symm (h : a ≠ b) : b ≠ a :=
fun h₁ => h (h₁.symm)

theorem falseOfNe : a ≠ a → False :=
Ne.irrefl 

theorem neFalseOfSelf : p → p ≠ False :=
fun (hp : p) (h : p = False) => h ▸ hp 

theorem neTrueOfNot : ¬p → p ≠ True :=
fun (hnp : ¬p) (h : p = True) => (h ▸ hnp) trivial 

theorem trueNeFalse : ¬True = False :=
neFalseOfSelf trivial 

end Ne 

theorem eqFalseOfNeTrue : ∀  {b : Bool}, b ≠ true → b = false
| true, h => False.elim (h rfl)
| false, h => rfl 

theorem eqTrueOfNeFalse : ∀  {b : Bool}, b ≠ false → b = true
| true, h => rfl
| false, h => False.elim (h rfl)

theorem neFalseOfEqTrue : ∀  {b : Bool}, b = true → b ≠ false
| true, _ => fun h => Bool.noConfusion h
| false, h => Bool.noConfusion h 

theorem neTrueOfEqFalse : ∀  {b : Bool}, b = false → b ≠ true
| true, h => Bool.noConfusion h
| false, _ => fun h => Bool.noConfusion h 

section 

variables{α β φ : Sort u}{a a' : α}{b b' : β}{c : φ}

@[elabAsEliminator]
theorem HEq.ndrec.{u1, u2} {α : Sort u2} {a : α} {C : ∀  {β : Sort u2}, β → Sort u1} (m : C a) {β : Sort u2} {b : β}
  (h : a ≅ b) : C b :=
@HEq.rec α a (fun β b _ => C b) m β b h

@[elabAsEliminator]
theorem HEq.ndrecOn.{u1, u2} {α : Sort u2} {a : α} {C : ∀  {β : Sort u2}, β → Sort u1} {β : Sort u2} {b : β} (h : a ≅ b)
  (m : C a) : C b :=
@HEq.rec α a (fun β b _ => C b) m β b h 

theorem HEq.elim {α : Sort u} {a : α} {p : α → Sort v} {b : α} (h₁ : a ≅ b) (h₂ : p a) : p b :=
Eq.recOn (eqOfHEq h₁) h₂ 

theorem HEq.subst {p : ∀  (T : Sort u), T → Prop} (h₁ : a ≅ b) (h₂ : p α a) : p β b :=
HEq.ndrecOn h₁ h₂ 

theorem HEq.symm (h : a ≅ b) : b ≅ a :=
HEq.ndrecOn h (HEq.refl a)

theorem heqOfEq (h : a = a') : a ≅ a' :=
Eq.subst h (HEq.refl a)

theorem HEq.trans (h₁ : a ≅ b) (h₂ : b ≅ c) : a ≅ c :=
HEq.subst h₂ h₁ 

theorem heqOfHEqOfEq (h₁ : a ≅ b) (h₂ : b = b') : a ≅ b' :=
HEq.trans h₁ (heqOfEq h₂)

theorem heqOfEqOfHEq (h₁ : a = a') (h₂ : a' ≅ b) : a ≅ b :=
HEq.trans (heqOfEq h₁) h₂ 

def typeEqOfHEq (h : a ≅ b) : α = β :=
HEq.ndrecOn h (Eq.refl α)

end 

theorem eqRecHEq {α : Sort u} {φ : α → Sort v} : ∀  {a a' : α} (h : a = a') (p : φ a), (Eq.recOn h p : φ a') ≅ p
| a, _, rfl, p => HEq.refl p 

theorem ofHEqTrue {a : Prop} (h : a ≅ True) : a :=
ofEqTrue (eqOfHEq h)

theorem castHEq : ∀  {α β : Sort u} (h : α = β) (a : α), cast h a ≅ a
| α, _, rfl, a => HEq.refl a 

variables{a b c d : Prop}

theorem And.elim (h₁ : a ∧ b) (h₂ : a → b → c) : c :=
And.rec h₂ h₁ 

theorem And.swap : a ∧ b → b ∧ a :=
fun ⟨ha, hb⟩ => ⟨hb, ha⟩

def And.symm :=
@And.swap 

theorem Or.elim (h₁ : a ∨ b) (h₂ : a → c) (h₃ : b → c) : c :=
Or.rec h₂ h₃ h₁ 

theorem Or.swap (h : a ∨ b) : b ∨ a :=
Or.elim h Or.inr Or.inl 

def Or.symm :=
@Or.swap 

def Xor (a b : Prop) : Prop :=
(a ∧ ¬b) ∨ (b ∧ ¬a)

@[recursor 5]
theorem Iff.elim (h₁ : (a → b) → (b → a) → c) (h₂ : a ↔ b) : c :=
Iff.rec h₁ h₂ 

theorem Iff.left : (a ↔ b) → a → b :=
Iff.mp 

theorem Iff.right : (a ↔ b) → b → a :=
Iff.mpr 

theorem iffIffImpliesAndImplies (a b : Prop) : (a ↔ b) ↔ (a → b) ∧ (b → a) :=
Iff.intro (fun h => And.intro h.mp h.mpr) (fun h => Iff.intro h.left h.right)

theorem Iff.refl (a : Prop) : a ↔ a :=
Iff.intro (fun h => h) (fun h => h)

theorem Iff.rfl {a : Prop} : a ↔ a :=
Iff.refl a 

theorem Iff.trans (h₁ : a ↔ b) (h₂ : b ↔ c) : a ↔ c :=
Iff.intro (fun ha => Iff.mp h₂ (Iff.mp h₁ ha)) (fun hc => Iff.mpr h₁ (Iff.mpr h₂ hc))

theorem Iff.symm (h : a ↔ b) : b ↔ a :=
Iff.intro (Iff.right h) (Iff.left h)

theorem Iff.comm : (a ↔ b) ↔ (b ↔ a) :=
Iff.intro Iff.symm Iff.symm 

theorem Eq.toIff {a b : Prop} (h : a = b) : a ↔ b :=
Eq.recOn h Iff.rfl 

theorem neqOfNotIff {a b : Prop} : ¬(a ↔ b) → a ≠ b :=
fun h₁ h₂ =>
  have a ↔ b from Eq.subst h₂ (Iff.refl a);
  absurd this h₁ 

theorem notIffNotOfIff (h₁ : a ↔ b) : ¬a ↔ ¬b :=
Iff.intro (fun (hna : ¬a) (hb : b) => hna (Iff.right h₁ hb)) (fun (hnb : ¬b) (ha : a) => hnb (Iff.left h₁ ha))

theorem ofIffTrue (h : a ↔ True) : a :=
Iff.mp (Iff.symm h) trivial 

theorem notOfIffFalse : (a ↔ False) → ¬a :=
Iff.mp 

theorem iffTrueIntro (h : a) : a ↔ True :=
Iff.intro (fun hl => trivial) (fun hr => h)

theorem iffFalseIntro (h : ¬a) : a ↔ False :=
Iff.intro h (False.rec (fun _ => a))

theorem notNotIntro (ha : a) : ¬¬a :=
fun hna => hna ha 

theorem notTrue : (¬True) ↔ False :=
iffFalseIntro (notNotIntro trivial)

theorem resolveLeft {a b : Prop} (h : a ∨ b) (na : ¬a) : b :=
Or.elim h (fun ha => absurd ha na) id 

theorem negResolveLeft {a b : Prop} (h : ¬a ∨ b) (ha : a) : b :=
Or.elim h (fun na => absurd ha na) id 

theorem resolveRight {a b : Prop} (h : a ∨ b) (nb : ¬b) : a :=
Or.elim h id (fun hb => absurd hb nb)

theorem negResolveRight {a b : Prop} (h : a ∨ ¬b) (hb : b) : a :=
Or.elim h id (fun nb => absurd hb nb)

theorem Exists.elim {α : Sort u} {p : α → Prop} {b : Prop} (h₁ : Exists (fun x => p x)) (h₂ : ∀  (a : α), p a → b) :
  b :=
Exists.rec h₂ h₁

@[inlineIfReduce, nospecialize]
def Decidable.decide (p : Prop) [h : Decidable p] : Bool :=
Decidable.casesOn h (fun h₁ => false) (fun h₂ => true)

export Decidable(isTrue isFalse decide)

instance beqOfEq {α : Type u} [DecidableEq α] : HasBeq α :=
⟨fun a b => decide (a = b)⟩

theorem decideTrueEqTrue (h : Decidable True) : @decide True h = true :=
match h with 
| isTrue h => rfl
| isFalse h => False.elim (Iff.mp notTrue h)

theorem decideFalseEqFalse (h : Decidable False) : @decide False h = false :=
match h with 
| isFalse h => rfl
| isTrue h => False.elim h 

theorem decideEqTrue : ∀  {p : Prop} [s : Decidable p], p → decide p = true
| _, isTrue _, _ => rfl
| _, isFalse h₁, h₂ => absurd h₂ h₁ 

theorem decideEqFalse : ∀  {p : Prop} [s : Decidable p], ¬p → decide p = false
| _, isTrue h₁, h₂ => absurd h₁ h₂
| _, isFalse h, _ => rfl 

theorem ofDecideEqTrue {p : Prop} [s : Decidable p] : decide p = true → p :=
fun h =>
  match s with 
  | isTrue h₁ => h₁
  | isFalse h₁ => absurd h (neTrueOfEqFalse (decideEqFalse h₁))

theorem ofDecideEqFalse {p : Prop} [s : Decidable p] : decide p = false → ¬p :=
fun h =>
  match s with 
  | isTrue h₁ => absurd h (neFalseOfEqTrue (decideEqTrue h₁))
  | isFalse h₁ => h₁

/--Similar to `decide`, but uses an explicit instance -/
@[inline]
def toBoolUsing {p : Prop} (d : Decidable p) : Bool :=
@decide p d 

theorem toBoolUsingEqTrue {p : Prop} (d : Decidable p) (h : p) : toBoolUsing d = true :=
@decideEqTrue _ d h 

theorem ofBoolUsingEqTrue {p : Prop} {d : Decidable p} (h : toBoolUsing d = true) : p :=
@ofDecideEqTrue _ d h 

theorem ofBoolUsingEqFalse {p : Prop} {d : Decidable p} (h : toBoolUsing d = false) : ¬p :=
@ofDecideEqFalse _ d h 

instance  : Decidable True :=
isTrue trivial 

instance  : Decidable False :=
isFalse notFalse

@[macroInline]
def dite {α : Sort u} (c : Prop) [h : Decidable c] : (c → α) → (¬c → α) → α :=
fun t e => Decidable.casesOn h e t

@[macroInline]
def ite {α : Sort u} (c : Prop) [h : Decidable c] (t e : α) : α :=
Decidable.casesOn h (fun hnc => e) (fun hc => t)

namespace Decidable 

variables{p q : Prop}

def recOnTrue [h : Decidable p] {h₁ : p → Sort u} {h₂ : ¬p → Sort u} (h₃ : p) (h₄ : h₁ h₃) :
  (Decidable.recOn h h₂ h₁ : Sort u) :=
Decidable.casesOn h (fun h => False.rec _ (h h₃)) (fun h => h₄)

def recOnFalse [h : Decidable p] {h₁ : p → Sort u} {h₂ : ¬p → Sort u} (h₃ : ¬p) (h₄ : h₂ h₃) :
  (Decidable.recOn h h₂ h₁ : Sort u) :=
Decidable.casesOn h (fun h => h₄) (fun h => False.rec _ (h₃ h))

@[macroInline]
def byCases {q : Sort u} [s : Decidable p] (h1 : p → q) (h2 : ¬p → q) : q :=
match s with 
| isTrue h => h1 h
| isFalse h => h2 h 

theorem em (p : Prop) [Decidable p] : p ∨ ¬p :=
byCases Or.inl Or.inr 

theorem byContradiction [Decidable p] (h : ¬p → False) : p :=
byCases id (fun np => False.elim (h np))

theorem ofNotNot [Decidable p] : ¬¬p → p :=
fun hnn => byContradiction (fun hn => absurd hn hnn)

theorem notNotIff (p) [Decidable p] : (¬¬p) ↔ p :=
Iff.intro ofNotNot notNotIntro 

theorem notAndIffOrNot (p q : Prop) [d₁ : Decidable p] [d₂ : Decidable q] : ¬(p ∧ q) ↔ ¬p ∨ ¬q :=
Iff.intro
  (fun h =>
      match d₁, d₂ with 
      | isTrue h₁, isTrue h₂ => absurd (And.intro h₁ h₂) h
      | _, isFalse h₂ => Or.inr h₂
      | isFalse h₁, _ => Or.inl h₁)
  (fun (h) ⟨hp, hq⟩ => Or.elim h (fun h => h hp) (fun h => h hq))

end Decidable 

section 

variables{p q : Prop}

@[inline]
def decidableOfDecidableOfIff (hp : Decidable p) (h : p ↔ q) : Decidable q :=
if hp : p then isTrue (Iff.mp h hp) else isFalse (Iff.mp (notIffNotOfIff h) hp)

@[inline]
def decidableOfDecidableOfEq (hp : Decidable p) (h : p = q) : Decidable q :=
decidableOfDecidableOfIff hp h.toIff 

end 

section 

variables{p q : Prop}

@[macroInline]
instance  [Decidable p] [Decidable q] : Decidable (p ∧ q) :=
if hp : p then if hq : q then isTrue ⟨hp, hq⟩ else isFalse (fun h => hq (And.right h)) else
  isFalse (fun h => hp (And.left h))

@[macroInline]
instance  [Decidable p] [Decidable q] : Decidable (p ∨ q) :=
if hp : p then isTrue (Or.inl hp) else if hq : q then isTrue (Or.inr hq) else isFalse (fun h => Or.elim h hp hq)

instance  [Decidable p] : Decidable (¬p) :=
if hp : p then isFalse (absurd hp) else isTrue hp

@[macroInline]
instance implies.Decidable [Decidable p] [Decidable q] : Decidable (p → q) :=
if hp : p then if hq : q then isTrue (fun h => hq) else isFalse (fun h => absurd (h hp) hq) else
  isTrue (fun h => absurd h hp)

instance  [Decidable p] [Decidable q] : Decidable (p ↔ q) :=
if hp : p then if hq : q then isTrue ⟨fun _ => hq, fun _ => hp⟩ else isFalse $ fun h => hq (h.1 hp) else
  if hq : q then isFalse $ fun h => hp (h.2 hq) else isTrue $ ⟨fun h => absurd h hp, fun h => absurd h hq⟩

instance  [Decidable p] [Decidable q] : Decidable (Xor p q) :=
if hp : p then
  if hq : q then isFalse (fun h => Or.elim h (fun ⟨_, h⟩ => h hq : ¬(p ∧ ¬q)) (fun ⟨_, h⟩ => h hp : ¬(q ∧ ¬p))) else
    isTrue $ Or.inl ⟨hp, hq⟩ else
  if hq : q then isTrue $ Or.inr ⟨hq, hp⟩ else
    isFalse (fun h => Or.elim h (fun ⟨h, _⟩ => hp h : ¬(p ∧ ¬q)) (fun ⟨h, _⟩ => hq h : ¬(q ∧ ¬p)))

end 

@[inline]
instance  {α : Sort u} [DecidableEq α] (a b : α) : Decidable (a ≠ b) :=
match decEq a b with 
| isTrue h => isFalse $ fun h' => absurd h h'
| isFalse h => isTrue h 

theorem Bool.falseNeTrue (h : false = true) : False :=
Bool.noConfusion h

@[inline]
instance  : DecidableEq Bool :=
fun a b =>
  match a, b with 
  | false, false => isTrue rfl
  | false, true => isFalse Bool.falseNeTrue
  | true, false => isFalse (Ne.symm Bool.falseNeTrue)
  | true, true => isTrue rfl 

theorem ifPos {c : Prop} [h : Decidable c] (hc : c) {α : Sort u} {t e : α} : (ite c t e) = t :=
match h with 
| (isTrue hc) => rfl
| (isFalse hnc) => absurd hc hnc 

theorem ifNeg {c : Prop} [h : Decidable c] (hnc : ¬c) {α : Sort u} {t e : α} : (ite c t e) = e :=
match h with 
| (isTrue hc) => absurd hc hnc
| (isFalse hnc) => rfl 

theorem difPos {c : Prop} [h : Decidable c] (hc : c) {α : Sort u} {t : c → α} {e : ¬c → α} : (dite c t e) = t hc :=
match h with 
| (isTrue hc) => rfl
| (isFalse hnc) => absurd hc hnc 

theorem difNeg {c : Prop} [h : Decidable c] (hnc : ¬c) {α : Sort u} {t : c → α} {e : ¬c → α} : (dite c t e) = e hnc :=
match h with 
| (isTrue hc) => absurd hc hnc
| (isFalse hnc) => rfl 

theorem difEqIf (c : Prop) [h : Decidable c] {α : Sort u} (t : α) (e : α) :
  dite c (fun h => t) (fun h => e) = ite c t e :=
match h with 
| (isTrue hc) => rfl
| (isFalse hnc) => rfl 

instance  {c t e : Prop} [dC : Decidable c] [dT : Decidable t] [dE : Decidable e] : Decidable (if c then t else e) :=
match dC with 
| (isTrue hc) => dT
| (isFalse hc) => dE 

instance  {c : Prop} {t : c → Prop} {e : ¬c → Prop} [dC : Decidable c] [dT : ∀  h, Decidable (t h)]
  [dE : ∀  h, Decidable (e h)] : Decidable (if h : c then t h else e h) :=
match dC with 
| (isTrue hc) => dT hc
| (isFalse hc) => dE hc

/--Universe lifting operation -/
structure ULift.{r, s}(α : Type s) : Type (max s r) := up :: 
(down : α)

namespace ULift 

theorem upDown {α : Type u} : ∀  (b : ULift.{v} α), up (down b) = b
| up a => rfl 

theorem downUp {α : Type u} (a : α) : down (up.{v} a) = a :=
rfl 

end ULift

/--Universe lifting operation from Sort to Type -/
structure PLift(α : Sort u) : Type u := up :: 
(down : α)

namespace PLift 

theorem upDown {α : Sort u} : ∀  (b : PLift α), up (down b) = b
| up a => rfl 

theorem downUp {α : Sort u} (a : α) : down (up a) = a :=
rfl 

end PLift 

structure PointedType := 
(type : Type u)
(val : type)

class Inhabited(α : Sort u) := mk{} :: 
(default : α)

constant arbitrary (α : Sort u) [Inhabited α] : α :=
Inhabited.default α 

instance Prop.Inhabited : Inhabited Prop :=
⟨True⟩

instance Fun.Inhabited (α : Sort u) {β : Sort v} [h : Inhabited β] : Inhabited (α → β) :=
Inhabited.casesOn h (fun b => ⟨fun a => b⟩)

instance Forall.Inhabited (α : Sort u) {β : α → Sort v} [∀  x, Inhabited (β x)] : Inhabited (∀  x, β x) :=
⟨fun a => arbitrary (β a)⟩

instance  : Inhabited Bool :=
⟨false⟩

instance  : Inhabited True :=
⟨trivial⟩

instance  : Inhabited Nat :=
⟨0⟩

instance  : Inhabited NonScalar :=
⟨⟨arbitrary _⟩⟩

instance  : Inhabited PNonScalar.{u} :=
⟨⟨arbitrary _⟩⟩

instance  : Inhabited PointedType :=
⟨{ type := PUnit, val := ⟨⟩ }⟩

instance  {α} [Inhabited α] : Inhabited (ForInStep α) :=
⟨ForInStep.done (arbitrary _)⟩

class inductive Nonempty (α : Sort u) : Prop
  | intro (val : α) : Nonempty 

protected def Nonempty.elim {α : Sort u} {p : Prop} (h₁ : Nonempty α) (h₂ : α → p) : p :=
Nonempty.rec h₂ h₁ 

instance nonemptyOfInhabited {α : Sort u} [Inhabited α] : Nonempty α :=
⟨arbitrary α⟩

theorem nonemptyOfExists {α : Sort u} {p : α → Prop} : Exists (fun x => p x) → Nonempty α
| ⟨w, h⟩ => ⟨w⟩

class inductive Subsingleton (α : Sort u) : Prop
  | intro (h : ∀  (a b : α), a = b) : Subsingleton 

protected def Subsingleton.elim {α : Sort u} [h : Subsingleton α] : ∀  (a b : α), a = b :=
Subsingleton.casesOn h (fun p => p)

protected def Subsingleton.helim {α β : Sort u} [h : Subsingleton α] (h : α = β) : ∀  (a : α) (b : β), a ≅ b :=
Eq.recOn h (fun a b => heqOfEq (Subsingleton.elim a b))

instance subsingletonProp (p : Prop) : Subsingleton p :=
⟨fun a b => proofIrrel a b⟩

instance  (p : Prop) : Subsingleton (Decidable p) :=
Subsingleton.intro $
  fun d₁ =>
    match d₁ with 
    | (isTrue t₁) =>
      fun d₂ =>
        match d₂ with 
        | (isTrue t₂) => Eq.recOn (proofIrrel t₁ t₂) rfl
        | (isFalse f₂) => absurd t₁ f₂
    | (isFalse f₁) =>
      fun d₂ =>
        match d₂ with 
        | (isTrue t₂) => absurd t₂ f₁
        | (isFalse f₂) => Eq.recOn (proofIrrel f₁ f₂) rfl 

protected theorem recSubsingleton {p : Prop} [h : Decidable p] {h₁ : p → Sort u} {h₂ : ¬p → Sort u}
  [h₃ : ∀  (h : p), Subsingleton (h₁ h)] [h₄ : ∀  (h : ¬p), Subsingleton (h₂ h)] :
  Subsingleton (Decidable.casesOn h h₂ h₁) :=
match h with 
| (isTrue h) => h₃ h
| (isFalse h) => h₄ h 

section relation 

variables{α : Sort u}{β : Sort v}(r : β → β → Prop)

def Reflexive :=
∀  x, r x x 

def Symmetric :=
∀  {x y}, r x y → r y x 

def Transitive :=
∀  {x y z}, r x y → r y z → r x z 

def Equivalence :=
Reflexive r ∧ Symmetric r ∧ Transitive r 

def Total :=
∀  x y, r x y ∨ r y x 

def mkEquivalence (rfl : Reflexive r) (symm : Symmetric r) (trans : Transitive r) : Equivalence r :=
⟨rfl, @symm, @trans⟩

def Irreflexive :=
∀  x, ¬r x x 

def AntiSymmetric :=
∀  {x y}, r x y → r y x → x = y 

def emptyRelation (a₁ a₂ : α) : Prop :=
False 

def Subrelation (q r : β → β → Prop) :=
∀  {x y}, q x y → r x y 

def InvImage (f : α → β) : α → α → Prop :=
fun a₁ a₂ => r (f a₁) (f a₂)

theorem InvImage.Transitive (f : α → β) (h : Transitive r) : Transitive (InvImage r f) :=
fun (a₁ a₂ a₃ : α) (h₁ : InvImage r f a₁ a₂) (h₂ : InvImage r f a₂ a₃) => h h₁ h₂ 

theorem InvImage.Irreflexive (f : α → β) (h : Irreflexive r) : Irreflexive (InvImage r f) :=
fun (a : α) (h₁ : InvImage r f a a) => h (f a) h₁ 

inductive TC {α : Sort u} (r : α → α → Prop) : α → α → Prop
| base : ∀  a b, r a b → TC a b
| trans : ∀  a b c, TC a b → TC b c → TC a c

@[elabAsEliminator]
theorem TC.ndrec.{u1, u2} {α : Sort u} {r : α → α → Prop} {C : α → α → Prop} (m₁ : ∀  (a b : α), r a b → C a b)
  (m₂ : ∀  (a b c : α), TC r a b → TC r b c → C a b → C b c → C a c) {a b : α} (h : TC r a b) : C a b :=
@TC.rec α r (fun a b _ => C a b) m₁ m₂ a b h

@[elabAsEliminator]
theorem TC.ndrecOn.{u1, u2} {α : Sort u} {r : α → α → Prop} {C : α → α → Prop} {a b : α} (h : TC r a b)
  (m₁ : ∀  (a b : α), r a b → C a b) (m₂ : ∀  (a b c : α), TC r a b → TC r b c → C a b → C b c → C a c) : C a b :=
@TC.rec α r (fun a b _ => C a b) m₁ m₂ a b h 

end relation 

section Binary 

variables{α : Type u}{β : Type v}

variable(f : α → α → α)

def Commutative :=
∀  a b, f a b = f b a 

def Associative :=
∀  a b c, f (f a b) c = f a (f b c)

def RightCommutative (h : β → α → β) :=
∀  b a₁ a₂, h (h b a₁) a₂ = h (h b a₂) a₁ 

def LeftCommutative (h : α → β → β) :=
∀  a₁ a₂ b, h a₁ (h a₂ b) = h a₂ (h a₁ b)

theorem leftComm : Commutative f → Associative f → LeftCommutative f :=
fun hcomm hassoc a b c =>
  ((Eq.symm (hassoc a b c)).trans (hcomm a b ▸ rfl : f (f a b) c = f (f b a) c)).trans (hassoc b a c)

theorem rightComm : Commutative f → Associative f → RightCommutative f :=
fun hcomm hassoc a b c =>
  ((hassoc a b c).trans (hcomm b c ▸ rfl : f a (f b c) = f a (f c b))).trans (Eq.symm (hassoc a c b))

end Binary 

namespace Subtype 

def existsOfSubtype {α : Type u} {p : α → Prop} : { x // p x } → Exists (fun x => p x)
| ⟨a, h⟩ => ⟨a, h⟩

variables{α : Type u}{p : α → Prop}

theorem tagIrrelevant {a : α} (h1 h2 : p a) : mk a h1 = mk a h2 :=
rfl 

protected theorem eq : ∀  {a1 a2 : { x // p x }}, val a1 = val a2 → a1 = a2
| ⟨x, h1⟩, ⟨.(x), h2⟩, rfl => rfl 

theorem eta (a : { x // p x }) (h : p (val a)) : mk (val a) h = a :=
Subtype.eq rfl 

instance  {α : Type u} {p : α → Prop} {a : α} (h : p a) : Inhabited { x // p x } :=
⟨⟨a, h⟩⟩

instance  {α : Type u} {p : α → Prop} [DecidableEq α] : DecidableEq { x : α // p x } :=
fun ⟨a, h₁⟩ ⟨b, h₂⟩ =>
  if h : a = b then isTrue (Subtype.eq h) else isFalse (fun h' => Subtype.noConfusion h' (fun h' => absurd h' h))

end Subtype 

section 

variables{α : Type u}{β : Type v}

instance Sum.inhabitedLeft [h : Inhabited α] : Inhabited (Sum α β) :=
⟨Sum.inl (arbitrary α)⟩

instance Sum.inhabitedRight [h : Inhabited β] : Inhabited (Sum α β) :=
⟨Sum.inr (arbitrary β)⟩

instance  {α : Type u} {β : Type v} [DecidableEq α] [DecidableEq β] : DecidableEq (Sum α β) :=
fun a b =>
  match a, b with 
  | (Sum.inl a), (Sum.inl b) =>
    if h : a = b then isTrue (h ▸ rfl) else isFalse (fun h' => Sum.noConfusion h' (fun h' => absurd h' h))
  | (Sum.inr a), (Sum.inr b) =>
    if h : a = b then isTrue (h ▸ rfl) else isFalse (fun h' => Sum.noConfusion h' (fun h' => absurd h' h))
  | (Sum.inr a), (Sum.inl b) => isFalse (fun h => Sum.noConfusion h)
  | (Sum.inl a), (Sum.inr b) => isFalse (fun h => Sum.noConfusion h)

end 

section 

variables{α : Type u}{β : Type v}

instance  [Inhabited α] [Inhabited β] : Inhabited (Prod α β) :=
⟨(arbitrary α, arbitrary β)⟩

instance  [DecidableEq α] [DecidableEq β] : DecidableEq (α × β) :=
fun ⟨a, b⟩ ⟨a', b'⟩ =>
  match (decEq a a') with 
  | (isTrue e₁) =>
    match (decEq b b') with 
    | (isTrue e₂) => isTrue (Eq.recOn e₁ (Eq.recOn e₂ rfl))
    | (isFalse n₂) => isFalse (fun h => Prod.noConfusion h (fun e₁' e₂' => absurd e₂' n₂))
  | (isFalse n₁) => isFalse (fun h => Prod.noConfusion h (fun e₁' e₂' => absurd e₁' n₁))

instance  [HasBeq α] [HasBeq β] : HasBeq (α × β) :=
⟨fun ⟨a₁, b₁⟩ ⟨a₂, b₂⟩ => a₁ == a₂ && b₁ == b₂⟩

instance  [HasLess α] [HasLess β] : HasLess (α × β) :=
⟨fun s t => s.1 < t.1 ∨ (s.1 = t.1 ∧ s.2 < t.2)⟩

instance prodHasDecidableLt [HasLess α] [HasLess β] [DecidableEq α] [DecidableEq β] [∀  (a b : α), Decidable (a < b)]
  [∀  (a b : β), Decidable (a < b)] : ∀  (s t : α × β), Decidable (s < t) :=
fun t s => Or.Decidable 

theorem Prod.ltDef [HasLess α] [HasLess β] (s t : α × β) : (s < t) = (s.1 < t.1 ∨ (s.1 = t.1 ∧ s.2 < t.2)) :=
rfl 

end 

def Prod.map.{u₁, u₂, v₁, v₂} {α₁ : Type u₁} {α₂ : Type u₂} {β₁ : Type v₁} {β₂ : Type v₂} (f : α₁ → α₂) (g : β₁ → β₂) :
  α₁ × β₁ → α₂ × β₂
| (a, b) => (f a, g b)

theorem exOfPsig {α : Type u} {p : α → Prop} : (PSigma (fun x => p x)) → Exists (fun x => p x)
| ⟨x, hx⟩ => ⟨x, hx⟩

section 

variables{α : Type u}{β : α → Type v}

protected theorem Sigma.eq :
  ∀  {p₁ p₂ : Sigma (fun a => β a)} (h₁ : p₁.1 = p₂.1), (Eq.recOn h₁ p₁.2 : β p₂.1) = p₂.2 → p₁ = p₂
| ⟨a, b⟩, ⟨.(a), .(b)⟩, rfl, rfl => rfl 

end 

section 

variables{α : Sort u}{β : α → Sort v}

protected theorem PSigma.eq : ∀  {p₁ p₂ : PSigma β} (h₁ : p₁.1 = p₂.1), (Eq.recOn h₁ p₁.2 : β p₂.1) = p₂.2 → p₁ = p₂
| ⟨a, b⟩, ⟨.(a), .(b)⟩, rfl, rfl => rfl 

end 

theorem punitEq (a b : PUnit) : a = b :=
PUnit.recOn a (PUnit.recOn b rfl)

theorem punitEqPUnit (a : PUnit) : a = () :=
punitEq a ()

instance  : Subsingleton PUnit :=
Subsingleton.intro punitEq 

instance  : Inhabited PUnit :=
⟨⟨⟩⟩

instance  : DecidableEq PUnit :=
fun a b => isTrue (punitEq a b)

class Setoid(α : Sort u) := 
(r : α → α → Prop)
(iseqv{} : Equivalence r)

instance setoidHasEquiv {α : Sort u} [Setoid α] : HasEquiv α :=
⟨Setoid.r⟩

namespace Setoid 

variables{α : Sort u}[Setoid α]

theorem refl (a : α) : a ≈ a :=
match Setoid.iseqv α with 
| ⟨hRefl, hSymm, hTrans⟩ => hRefl a 

theorem symm {a b : α} (hab : a ≈ b) : b ≈ a :=
match Setoid.iseqv α with 
| ⟨hRefl, hSymm, hTrans⟩ => hSymm hab 

theorem trans {a b c : α} (hab : a ≈ b) (hbc : b ≈ c) : a ≈ c :=
match Setoid.iseqv α with 
| ⟨hRefl, hSymm, hTrans⟩ => hTrans hab hbc 

end Setoid 

axiom propext {a b : Prop} : (a ↔ b) → a = b 

theorem eqTrueIntro {a : Prop} (h : a) : a = True :=
propext (iffTrueIntro h)

theorem eqFalseIntro {a : Prop} (h : ¬a) : a = False :=
propext (iffFalseIntro h)

theorem iffSubst {a b : Prop} {p : Prop → Prop} (h₁ : a ↔ b) (h₂ : p a) : p b :=
Eq.subst (propext h₁) h₂ 

namespace Quot 

axiom sound : ∀  {α : Sort u} {r : α → α → Prop} {a b : α}, r a b → Quot.mk r a = Quot.mk r b 

attribute [elabAsEliminator] lift ind 

protected theorem liftBeta {α : Sort u} {r : α → α → Prop} {β : Sort v} (f : α → β) (c : ∀  a b, r a b → f a = f b)
  (a : α) : lift f c (Quot.mk r a) = f a :=
rfl 

protected theorem indBeta {α : Sort u} {r : α → α → Prop} {β : Quot r → Prop} (p : ∀  a, β (Quot.mk r a)) (a : α) :
  (ind p (Quot.mk r a) : β (Quot.mk r a)) = p a :=
rfl

@[reducible, elabAsEliminator, inline]
protected def liftOn {α : Sort u} {β : Sort v} {r : α → α → Prop} (q : Quot r) (f : α → β)
  (c : ∀  a b, r a b → f a = f b) : β :=
lift f c q

@[elabAsEliminator]
protected theorem inductionOn {α : Sort u} {r : α → α → Prop} {β : Quot r → Prop} (q : Quot r)
  (h : ∀  a, β (Quot.mk r a)) : β q :=
ind h q 

theorem existsRep {α : Sort u} {r : α → α → Prop} (q : Quot r) : Exists (fun a => (Quot.mk r a) = q) :=
Quot.inductionOn q (fun a => ⟨a, rfl⟩)

section 

variable{α : Sort u}

variable{r : α → α → Prop}

variable{β : Quot r → Sort v}

@[reducible, macroInline]
protected def indep (f : ∀  a, β (Quot.mk r a)) (a : α) : PSigma β :=
⟨Quot.mk r a, f a⟩

protected theorem indepCoherent (f : ∀  a, β (Quot.mk r a))
  (h : ∀  (a b : α) (p : r a b), (Eq.rec (f a) (sound p) : β (Quot.mk r b)) = f b) :
  ∀  a b, r a b → Quot.indep f a = Quot.indep f b :=
fun a b e => PSigma.eq (sound e) (h a b e)

protected theorem liftIndepPr1 (f : ∀  a, β (Quot.mk r a))
  (h : ∀  (a b : α) (p : r a b), (Eq.rec (f a) (sound p) : β (Quot.mk r b)) = f b) (q : Quot r) :
  (lift (Quot.indep f) (Quot.indepCoherent f h) q).1 = q :=
Quot.ind (fun (a : α) => Eq.refl (Quot.indep f a).1) q

@[reducible, elabAsEliminator, inline]
protected def rec (f : ∀  a, β (Quot.mk r a))
  (h : ∀  (a b : α) (p : r a b), (Eq.rec (f a) (sound p) : β (Quot.mk r b)) = f b) (q : Quot r) : β q :=
Eq.ndrecOn (Quot.liftIndepPr1 f h q) ((lift (Quot.indep f) (Quot.indepCoherent f h) q).2)

@[reducible, elabAsEliminator, inline]
protected def recOn (q : Quot r) (f : ∀  a, β (Quot.mk r a))
  (h : ∀  (a b : α) (p : r a b), (Eq.rec (f a) (sound p) : β (Quot.mk r b)) = f b) : β q :=
Quot.rec f h q

@[reducible, elabAsEliminator, inline]
protected def recOnSubsingleton [h : ∀  a, Subsingleton (β (Quot.mk r a))] (q : Quot r) (f : ∀  a, β (Quot.mk r a)) :
  β q :=
Quot.rec f (fun a b h => Subsingleton.elim _ (f b)) q

@[reducible, elabAsEliminator, inline]
protected def hrecOn (q : Quot r) (f : ∀  a, β (Quot.mk r a)) (c : ∀  (a b : α) (p : r a b), f a ≅ f b) : β q :=
Quot.recOn q f $
  fun a b p =>
    eqOfHEq $
      have p₁ : (Eq.rec (f a) (sound p) : β (Quot.mk r b)) ≅ f a := eqRecHEq (sound p) (f a);
      HEq.trans p₁ (c a b p)

end 

end Quot 

def Quotient {α : Sort u} (s : Setoid α) :=
@Quot α Setoid.r 

namespace Quotient

@[inline]
protected def mk {α : Sort u} [s : Setoid α] (a : α) : Quotient s :=
Quot.mk Setoid.r a 

def sound {α : Sort u} [s : Setoid α] {a b : α} : a ≈ b → Quotient.mk a = Quotient.mk b :=
Quot.sound

@[reducible, elabAsEliminator]
protected def lift {α : Sort u} {β : Sort v} [s : Setoid α] (f : α → β) :
  (∀  a b, a ≈ b → f a = f b) → Quotient s → β :=
Quot.lift f

@[elabAsEliminator]
protected theorem ind {α : Sort u} [s : Setoid α] {β : Quotient s → Prop} : (∀  a, β (Quotient.mk a)) → ∀  q, β q :=
Quot.ind

@[reducible, elabAsEliminator, inline]
protected def liftOn {α : Sort u} {β : Sort v} [s : Setoid α] (q : Quotient s) (f : α → β)
  (c : ∀  a b, a ≈ b → f a = f b) : β :=
Quot.liftOn q f c

@[elabAsEliminator]
protected theorem inductionOn {α : Sort u} [s : Setoid α] {β : Quotient s → Prop} (q : Quotient s)
  (h : ∀  a, β (Quotient.mk a)) : β q :=
Quot.inductionOn q h 

theorem existsRep {α : Sort u} [s : Setoid α] (q : Quotient s) : Exists (fun (a : α) => Quotient.mk a = q) :=
Quot.existsRep q 

section 

variable{α : Sort u}

variable[s : Setoid α]

variable{β : Quotient s → Sort v}

@[inline]
protected def rec (f : ∀  a, β (Quotient.mk a))
  (h : ∀  (a b : α) (p : a ≈ b), (Eq.rec (f a) (Quotient.sound p) : β (Quotient.mk b)) = f b) (q : Quotient s) : β q :=
Quot.rec f h q

@[reducible, elabAsEliminator, inline]
protected def recOn (q : Quotient s) (f : ∀  a, β (Quotient.mk a))
  (h : ∀  (a b : α) (p : a ≈ b), (Eq.rec (f a) (Quotient.sound p) : β (Quotient.mk b)) = f b) : β q :=
Quot.recOn q f h

@[reducible, elabAsEliminator, inline]
protected def recOnSubsingleton [h : ∀  a, Subsingleton (β (Quotient.mk a))] (q : Quotient s)
  (f : ∀  a, β (Quotient.mk a)) : β q :=
@Quot.recOnSubsingleton _ _ _ h q f

@[reducible, elabAsEliminator, inline]
protected def hrecOn (q : Quotient s) (f : ∀  a, β (Quotient.mk a)) (c : ∀  (a b : α) (p : a ≈ b), f a ≅ f b) : β q :=
Quot.hrecOn q f c 

end 

section 

universes uA uB uC 

variables{α : Sort uA}{β : Sort uB}{φ : Sort uC}

variables[s₁ : Setoid α][s₂ : Setoid β]

@[reducible, elabAsEliminator, inline]
protected def lift₂ (f : α → β → φ) (c : ∀  a₁ a₂ b₁ b₂, a₁ ≈ b₁ → a₂ ≈ b₂ → f a₁ a₂ = f b₁ b₂) (q₁ : Quotient s₁)
  (q₂ : Quotient s₂) : φ :=
Quotient.lift (fun (a₁ : α) => Quotient.lift (f a₁) (fun (a b : β) => c a₁ a a₁ b (Setoid.refl a₁)) q₂)
  (fun (a b : α) (h : a ≈ b) =>
      @Quotient.ind β s₂
        (fun (a1 : Quotient s₂) =>
            (Quotient.lift (f a) (fun (a1 b : β) => c a a1 a b (Setoid.refl a)) a1) =
              (Quotient.lift (f b) (fun (a b1 : β) => c b a b b1 (Setoid.refl b)) a1))
        (fun (a' : β) => c a a' b a' h (Setoid.refl a')) q₂)
  q₁

@[reducible, elabAsEliminator, inline]
protected def liftOn₂ (q₁ : Quotient s₁) (q₂ : Quotient s₂) (f : α → β → φ)
  (c : ∀  a₁ a₂ b₁ b₂, a₁ ≈ b₁ → a₂ ≈ b₂ → f a₁ a₂ = f b₁ b₂) : φ :=
Quotient.lift₂ f c q₁ q₂

@[elabAsEliminator]
protected theorem ind₂ {φ : Quotient s₁ → Quotient s₂ → Prop} (h : ∀  a b, φ (Quotient.mk a) (Quotient.mk b))
  (q₁ : Quotient s₁) (q₂ : Quotient s₂) : φ q₁ q₂ :=
Quotient.ind (fun a₁ => Quotient.ind (fun a₂ => h a₁ a₂) q₂) q₁

@[elabAsEliminator]
protected theorem inductionOn₂ {φ : Quotient s₁ → Quotient s₂ → Prop} (q₁ : Quotient s₁) (q₂ : Quotient s₂)
  (h : ∀  a b, φ (Quotient.mk a) (Quotient.mk b)) : φ q₁ q₂ :=
Quotient.ind (fun a₁ => Quotient.ind (fun a₂ => h a₁ a₂) q₂) q₁

@[elabAsEliminator]
protected theorem inductionOn₃ [s₃ : Setoid φ] {δ : Quotient s₁ → Quotient s₂ → Quotient s₃ → Prop} (q₁ : Quotient s₁)
  (q₂ : Quotient s₂) (q₃ : Quotient s₃) (h : ∀  a b c, δ (Quotient.mk a) (Quotient.mk b) (Quotient.mk c)) :
  δ q₁ q₂ q₃ :=
Quotient.ind (fun a₁ => Quotient.ind (fun a₂ => Quotient.ind (fun a₃ => h a₁ a₂ a₃) q₃) q₂) q₁ 

end 

section Exact 

variable{α : Sort u}

private def rel [s : Setoid α] (q₁ q₂ : Quotient s) : Prop :=
Quotient.liftOn₂ q₁ q₂ (fun a₁ a₂ => a₁ ≈ a₂)
  (fun a₁ a₂ b₁ b₂ a₁b₁ a₂b₂ =>
      propext
        (Iff.intro (fun a₁a₂ => Setoid.trans (Setoid.symm a₁b₁) (Setoid.trans a₁a₂ a₂b₂))
            (fun b₁b₂ => Setoid.trans a₁b₁ (Setoid.trans b₁b₂ (Setoid.symm a₂b₂)))))

private theorem rel.refl [s : Setoid α] : ∀  (q : Quotient s), rel q q :=
fun q => Quot.inductionOn q (fun a => Setoid.refl a)

private theorem eqImpRel [s : Setoid α] {q₁ q₂ : Quotient s} : q₁ = q₂ → rel q₁ q₂ :=
fun h => Eq.ndrecOn h (rel.refl q₁)

theorem exact [s : Setoid α] {a b : α} : Quotient.mk a = Quotient.mk b → a ≈ b :=
fun h => eqImpRel h 

end Exact 

section 

universes uA uB uC 

variables{α : Sort uA}{β : Sort uB}

variables[s₁ : Setoid α][s₂ : Setoid β]

@[reducible, elabAsEliminator]
protected def recOnSubsingleton₂ {φ : Quotient s₁ → Quotient s₂ → Sort uC}
  [h : ∀  a b, Subsingleton (φ (Quotient.mk a) (Quotient.mk b))] (q₁ : Quotient s₁) (q₂ : Quotient s₂)
  (f : ∀  a b, φ (Quotient.mk a) (Quotient.mk b)) : φ q₁ q₂ :=
@Quotient.recOnSubsingleton _ s₁ (fun q => φ q q₂) (fun a => Quotient.ind (fun b => h a b) q₂) q₁
  (fun a => Quotient.recOnSubsingleton q₂ (fun b => f a b))

end 

end Quotient 

section 

variable{α : Type u}

variable(r : α → α → Prop)

inductive EqvGen : α → α → Prop
| rel : ∀  x y, r x y → EqvGen x y
| refl : ∀  x, EqvGen x x
| symm : ∀  x y, EqvGen x y → EqvGen y x
| trans : ∀  x y z, EqvGen x y → EqvGen y z → EqvGen x z 

theorem EqvGen.isEquivalence : Equivalence (@EqvGen α r) :=
mkEquivalence _ EqvGen.refl EqvGen.symm EqvGen.trans 

def EqvGen.Setoid : Setoid α :=
Setoid.mk _ (EqvGen.isEquivalence r)

theorem Quot.exact {a b : α} (H : Quot.mk r a = Quot.mk r b) : EqvGen r a b :=
@Quotient.exact _ (EqvGen.Setoid r) a b
  (@congrArg _ _ _ _ (Quot.lift (@Quotient.mk _ (EqvGen.Setoid r)) (fun x y h => Quot.sound (EqvGen.rel x y h))) H)

theorem Quot.eqvGenSound {r : α → α → Prop} {a b : α} (H : EqvGen r a b) : Quot.mk r a = Quot.mk r b :=
EqvGen.recOn H (fun x y h => Quot.sound h) (fun x => rfl) (fun x y _ IH => Eq.symm IH)
  (fun x y z _ _ IH₁ IH₂ => Eq.trans IH₁ IH₂)

end 

instance  {α : Sort u} {s : Setoid α} [d : ∀  (a b : α), Decidable (a ≈ b)] : DecidableEq (Quotient s) :=
fun (q₁ q₂ : Quotient s) =>
  Quotient.recOnSubsingleton₂ q₁ q₂
    (fun a₁ a₂ =>
        match (d a₁ a₂) with 
        | (isTrue h₁) => isTrue (Quotient.sound h₁)
        | (isFalse h₂) => isFalse (fun h => absurd (Quotient.exact h) h₂))

namespace Function 

variables{α : Sort u}{β : α → Sort v}

def Equiv (f₁ f₂ : ∀  (x : α), β x) : Prop :=
∀  x, f₁ x = f₂ x 

protected theorem Equiv.refl (f : ∀  (x : α), β x) : Equiv f f :=
fun x => rfl 

protected theorem Equiv.symm {f₁ f₂ : ∀  (x : α), β x} : Equiv f₁ f₂ → Equiv f₂ f₁ :=
fun h x => Eq.symm (h x)

protected theorem Equiv.trans {f₁ f₂ f₃ : ∀  (x : α), β x} : Equiv f₁ f₂ → Equiv f₂ f₃ → Equiv f₁ f₃ :=
fun h₁ h₂ x => Eq.trans (h₁ x) (h₂ x)

protected theorem Equiv.isEquivalence (α : Sort u) (β : α → Sort v) : Equivalence (@Function.Equiv α β) :=
mkEquivalence (@Function.Equiv α β) (@Equiv.refl α β) (@Equiv.symm α β) (@Equiv.trans α β)

end Function 

section 

open Quotient 

variables{α : Sort u}{β : α → Sort v}

@[instance]
private def funSetoid (α : Sort u) (β : α → Sort v) : Setoid (∀  (x : α), β x) :=
Setoid.mk (@Function.Equiv α β) (Function.Equiv.isEquivalence α β)

private def extfunApp (f : Quotient $ funSetoid α β) : ∀  (x : α), β x :=
fun x => Quot.liftOn f (fun (f : ∀  (x : α), β x) => f x) (fun f₁ f₂ h => h x)

theorem funext {f₁ f₂ : ∀  (x : α), β x} (h : ∀  x, f₁ x = f₂ x) : f₁ = f₂ :=
show extfunApp (Quotient.mk f₁) = extfunApp (Quotient.mk f₂) from congrArg extfunApp (sound h)

end 

instance Forall.Subsingleton {α : Sort u} {β : α → Sort v} [∀  a, Subsingleton (β a)] : Subsingleton (∀  a, β a) :=
⟨fun f₁ f₂ => funext (fun a => Subsingleton.elim (f₁ a) (f₂ a))⟩

namespace Function 

universes u₁ u₂ u₃ u₄ 

variables{α : Sort u₁}{β : Sort u₂}{φ : Sort u₃}{δ : Sort u₄}{ζ : Sort u₁}

@[inline, reducible]
def comp (f : β → φ) (g : α → β) : α → φ :=
fun x => f (g x)

infixr ` ∘ ` := Function.comp

@[inline, reducible]
def onFun (f : β → β → φ) (g : α → β) : α → α → φ :=
fun x y => f (g x) (g y)

@[inline, reducible]
def combine (f : α → β → φ) (op : φ → δ → ζ) (g : α → β → δ) : α → β → ζ :=
fun x y => op (f x y) (g x y)

@[inline, reducible]
def const (β : Sort u₂) (a : α) : β → α :=
fun x => a

@[inline, reducible]
def swap {φ : α → β → Sort u₃} (f : ∀  x y, φ x y) : ∀  y x, φ x y :=
fun y x => f x y 

end Function 

def Squash (α : Type u) :=
Quot (fun (a b : α) => True)

def Squash.mk {α : Type u} (x : α) : Squash α :=
Quot.mk _ x 

theorem Squash.ind {α : Type u} {β : Squash α → Prop} (h : ∀  (a : α), β (Squash.mk a)) : ∀  (q : Squash α), β q :=
Quot.ind h

@[inline]
def Squash.lift {α β} [Subsingleton β] (s : Squash α) (f : α → β) : β :=
Quot.lift f (fun a b _ => Subsingleton.elim _ _) s 

instance Squash.Subsingleton {α} : Subsingleton (Squash α) :=
⟨Squash.ind (fun (a : α) => Squash.ind (fun (b : α) => Quot.sound trivial))⟩

namespace Lean

/--When the kernel tries to reduce a term `Lean.reduceBool c`, it will invoke the Lean interpreter to evaluate `c`.
  The kernel will not use the interpreter if `c` is not a constant.
  This feature is useful for performing proofs by reflection.

  Remark: the Lean frontend allows terms of the from `Lean.reduceBool t` where `t` is a term not containing
  free variables. The frontend automatically declares a fresh auxiliary constant `c` and replaces the term with
  `Lean.reduceBool c`. The main motivation is that the code for `t` will be pre-compiled.

  Warning: by using this feature, the Lean compiler and interpreter become part of your trusted code base.
  This is extra 30k lines of code. More importantly, you will probably not be able to check your developement using
  external type checkers (e.g., Trepplein) that do not implement this feature.
  Keep in mind that if you are using Lean as programming language, you are already trusting the Lean compiler and interpreter.
  So, you are mainly losing the capability of type checking your developement using external checkers.

  Recall that the compiler trusts the correctness of all `[implementedBy ...]` and `[extern ...]` annotations.
  If an extern function is executed, then the trusted code base will also include the implementation of the associated
  foreign function.
-/
constant reduceBool (b : Bool) : Bool :=
b

/--Similar to `Lean.reduceBool` for closed `Nat` terms.

  Remark: we do not have plans for supporting a generic `reduceValue {α} (a : α) : α := a`.
  The main issue is that it is non-trivial to convert an arbitrary runtime object back into a Lean expression.
  We believe `Lean.reduceBool` enables most interesting applications (e.g., proof by reflection). -/
constant reduceNat (n : Nat) : Nat :=
n 

axiom ofReduceBool (a b : Bool) (h : reduceBool a = b) : a = b 

axiom ofReduceNat (a b : Nat) (h : reduceNat a = b) : a = b 

end Lean 

namespace Classical 

axiom choice {α : Sort u} : Nonempty α → α 

noncomputable def indefiniteDescription {α : Sort u} (p : α → Prop) (h : Exists (fun x => p x)) : { x // p x } :=
choice $
  let ⟨x, px⟩ := h;
  ⟨⟨x, px⟩⟩

noncomputable def choose {α : Sort u} {p : α → Prop} (h : Exists (fun x => p x)) : α :=
(indefiniteDescription p h).val 

theorem chooseSpec {α : Sort u} {p : α → Prop} (h : Exists (fun x => p x)) : p (choose h) :=
(indefiniteDescription p h).property 

theorem em (p : Prop) : p ∨ ¬p :=
let U (x : Prop) : Prop := x = True ∨ p;
let V (x : Prop) : Prop := x = False ∨ p;
have exU : Exists (fun x => U x) from ⟨True, Or.inl rfl⟩;
have exV : Exists (fun x => V x) from ⟨False, Or.inl rfl⟩;
let u : Prop := choose exU;
let v : Prop := choose exV;
have uDef : U u from chooseSpec exU;
have vDef : V v from chooseSpec exV;
have notUvOrP : u ≠ v ∨ p from
  Or.elim uDef
    (fun hut =>
        Or.elim vDef
          (fun hvf =>
              have hne : u ≠ v from hvf.symm ▸ hut.symm ▸ trueNeFalse;
              Or.inl hne)
          Or.inr)
    Or.inr;
have pImpliesUv : p → u = v from
  fun hp =>
    have hpred : U = V from
      funext $
        fun x =>
          have hl : (x = True ∨ p) → (x = False ∨ p) from fun a => Or.inr hp;
          have hr : (x = False ∨ p) → (x = True ∨ p) from fun a => Or.inr hp;
          show (x = True ∨ p) = (x = False ∨ p) from propext (Iff.intro hl hr);
    have h₀ : ∀  exU exV, @choose _ U exU = @choose _ V exV from hpred ▸ fun exU exV => rfl;
    show u = v from h₀ _ _;
Or.elim notUvOrP (fun (hne : u ≠ v) => Or.inr (mt pImpliesUv hne)) Or.inl 

theorem existsTrueOfNonempty {α : Sort u} : Nonempty α → Exists (fun (x : α) => True)
| ⟨x⟩ => ⟨x, trivial⟩

noncomputable def inhabitedOfNonempty {α : Sort u} (h : Nonempty α) : Inhabited α :=
⟨choice h⟩

noncomputable def inhabitedOfExists {α : Sort u} {p : α → Prop} (h : Exists (fun x => p x)) : Inhabited α :=
inhabitedOfNonempty (Exists.elim h (fun w hw => ⟨w⟩))

noncomputable def propDecidable (a : Prop) : Decidable a :=
choice $ Or.elim (em a) (fun ha => ⟨isTrue ha⟩) (fun hna => ⟨isFalse hna⟩)

noncomputable def decidableInhabited (a : Prop) : Inhabited (Decidable a) :=
⟨propDecidable a⟩

noncomputable def typeDecidableEq (α : Sort u) : DecidableEq α :=
fun x y => propDecidable (x = y)

noncomputable def typeDecidable (α : Sort u) : PSum α (α → False) :=
match (propDecidable (Nonempty α)) with 
| (isTrue hp) => PSum.inl (@arbitrary _ (inhabitedOfNonempty hp))
| (isFalse hn) => PSum.inr (fun a => absurd (Nonempty.intro a) hn)

noncomputable def strongIndefiniteDescription {α : Sort u} (p : α → Prop) (h : Nonempty α) :
  { x : α // Exists (fun (y : α) => p y) → p x } :=
@dite _ (Exists (fun (x : α) => p x)) (propDecidable _)
  (fun (hp : Exists (fun (x : α) => p x)) =>
      show { x : α // Exists (fun (y : α) => p y) → p x } from
        let xp := indefiniteDescription _ hp;
        ⟨xp.val, fun h' => xp.property⟩)
  (fun hp => ⟨choice h, fun h => absurd h hp⟩)

noncomputable def epsilon {α : Sort u} [h : Nonempty α] (p : α → Prop) : α :=
(strongIndefiniteDescription p h).val 

theorem epsilonSpecAux {α : Sort u} (h : Nonempty α) (p : α → Prop) : Exists (fun y => p y) → p (@epsilon α h p) :=
(strongIndefiniteDescription p h).property 

theorem epsilonSpec {α : Sort u} {p : α → Prop} (hex : Exists (fun y => p y)) :
  p (@epsilon α (nonemptyOfExists hex) p) :=
epsilonSpecAux (nonemptyOfExists hex) p hex 

theorem epsilonSingleton {α : Sort u} (x : α) : @epsilon α ⟨x⟩ (fun y => y = x) = x :=
@epsilonSpec α (fun y => y = x) ⟨x, rfl⟩

theorem axiomOfChoice {α : Sort u} {β : α → Sort v} {r : ∀  x, β x → Prop} (h : ∀  x, Exists (fun y => r x y)) :
  Exists (fun (f : ∀  x, β x) => ∀  x, r x (f x)) :=
⟨_, fun x => chooseSpec (h x)⟩

theorem skolem {α : Sort u} {b : α → Sort v} {p : ∀  x, b x → Prop} :
  (∀  x, Exists (fun y => p x y)) ↔ Exists (fun (f : ∀  x, b x) => ∀  x, p x (f x)) :=
⟨axiomOfChoice, fun ⟨f, hw⟩ (x) => ⟨f x, hw x⟩⟩

theorem propComplete (a : Prop) : a = True ∨ a = False :=
Or.elim (em a) (fun t => Or.inl (eqTrueIntro t)) (fun f => Or.inr (eqFalseIntro f))

theorem byCases {p q : Prop} (hpq : p → q) (hnpq : ¬p → q) : q :=
@Decidable.byCases _ _ (propDecidable _) hpq hnpq 

theorem byContradiction {p : Prop} (h : ¬p → False) : p :=
@Decidable.byContradiction _ (propDecidable _) h 

end Classical