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

prelude 

universes u v w

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

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

/--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} : α 

set_option bootstrap.inductiveCheckResultingUniverse false in
  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 

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

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

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

init_quot 

inductive HEq {α : Sort u} (a : α) : {β : Sort u} → β → Prop
| refl{} : HEq a 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)

@[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₁ 

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

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

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

theorem eqOfHEq {α : Sort u} {a a' : α} (h : a ≅ a') : a = a' :=
by 
  have (α β : Sort u) → (a : α) → (b : β) → a ≅ b → (h : α = β) → cast h a = b by 
    intro α β a b h₁ h₂ 
    induction h₁ 
    exact rfl 
  show cast rfl a = a' 
  exact this α α a a' h rfl 

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 a b
| inr (h : b) : Or a b 

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 p 

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 p
  | isTrue (h : p) : Decidable p 

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 (α : Type u)
| nil : List α
| cons (head : α) (tail : List α) : List α 

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

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

export OfNat(ofNat)

instance  : OfNat Nat :=
⟨id⟩

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

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

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

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

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

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

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

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

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

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

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

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

class OrElse(α : Type u) := 
(orElse : α → α → α)

class AndThen(α : Type u) := 
(andThen : α → α → α)

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

class EmptyCollection(α : Type u) := 
(emptyCollection : α)

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

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

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

set_option bootstrap.gen_matcher_code false in
  @[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 Add.add Neg.neg 

instance  : Add Nat :=
⟨Nat.add⟩

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 

structure NonScalar := 
(val : Nat)

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

class SizeOf(α : Sort u) := 
(sizeOf : α → Nat)

export SizeOf(sizeOf)

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

instance  (α : Sort u) : SizeOf α :=
⟨default.sizeOf α⟩

instance  : SizeOf Nat :=
{ sizeOf := fun n => n }

instance  (α : Type u) (β : Type v) [SizeOf α] [SizeOf β] : SizeOf (Prod α β) :=
{ sizeOf := fun (a, b) => 1 + sizeOf a + sizeOf b }

instance  (α : Type u) (β : Type v) [SizeOf α] [SizeOf β] : SizeOf (Sum α β) :=
{ sizeOf :=
    fun
    | Sum.inl a => 1 + sizeOf a
    | Sum.inr b => 1 + sizeOf b }

instance  (α : Type u) (β : Type v) [SizeOf α] [SizeOf β] : SizeOf (PSum α β) :=
{ sizeOf :=
    fun
    | PSum.inl a => 1 + sizeOf a
    | PSum.inr b => 1 + sizeOf b }

instance  (α : Type u) (β : α → Type v) [SizeOf α] [∀  a, SizeOf (β a)] : SizeOf (Sigma β) :=
{ sizeOf := fun ⟨a, b⟩ => 1 + sizeOf a + sizeOf b }

instance  (α : Type u) (β : α → Type v) [SizeOf α] [(a : α) → SizeOf (β a)] : SizeOf (PSigma β) :=
{ sizeOf := fun ⟨a, b⟩ => 1 + sizeOf a + sizeOf b }

instance  : SizeOf PUnit :=
{ sizeOf := fun _ => 1 }

instance  : SizeOf Bool :=
{ sizeOf := fun _ => 1 }

instance  (α : Type u) [SizeOf α] : SizeOf (Option α) :=
{ sizeOf :=
    fun
    | none => 1
    | some a => 1 + sizeOf a }

instance  (α : Type u) [SizeOf α] : SizeOf (List α) :=
{ sizeOf :=
    fun as =>
      let rec loop 
      | List.nil => 1
      | List.cons x xs => 1 + sizeOf x + loop xs 
      loop as }

instance  {α : Type u} [SizeOf α] (p : α → Prop) : SizeOf (Subtype p) :=
{ sizeOf := fun ⟨a, _⟩ => sizeOf a }

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

@[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} [BEq α] (a b : α) : Bool :=
!(a == b)

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 : α = β) (a : α) : β :=
h ▸ a

@[macroInline]
def Eq.mpr {α β : Sort u} (h : α = β) (b : β) : α :=
h ▸ b

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

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

theorem congrFun {α : Sort u} {β : α → Sort v} {f g : ∀  x, β x} (h : f = g) (a : α) : f a = g a :=
h ▸ rfl 

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₁ ▸ h₂ 

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

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

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)

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) =>
  have ¬True from h ▸ hnp 
  this 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 : α} {motive : {β : Sort u2} → β → Sort u1} (m : motive a) {β : Sort u2}
  {b : β} (h : a ≅ b) : motive b :=
@HEq.rec α a (fun b _ => motive b) m β b h

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

theorem HEq.elim {α : Sort u} {a : α} {p : α → Sort v} {b : α} (h₁ : a ≅ b) (h₂ : p a) : p b :=
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 (motive := fun x => x ≅ a) 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 (motive := @fun (x : Sort u) _ => α = x) h (Eq.refl α)

end 

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

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

theorem heqOfEqRecEq {α β : Sort u} {a : α} {b : β} (h₁ : α = β) (h₂ : Eq.rec (motive := fun α _ => α) a h₁ = b) :
  a ≅ b :=
by 
  subst h₁ 
  apply heqOfEq 
  exact h₂ 
  done 

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 :=
h₂ h₁.1 h₁.2

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 :=
match h₁ with 
| Or.inl h => h₂ h
| Or.inr 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 :=
h₁ h₂.1 h₂.2

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 :=
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 :=
h₂ h₁.1 h₁.2

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

export Decidable(isTrue isFalse decide)

instance  {α : Type u} [DecidableEq α] : BEq α :=
⟨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] (t : c → α) (e : ¬c → α) : α :=
Decidable.casesOn (motive := fun _ => α) h e t

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

namespace Decidable 

variables{p q : Prop}

@[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  [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 from Sort to Type -/
structure PLift(α : Sort u) : Type u := up :: 
(down : α)

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

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

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

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

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

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

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

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

instance  : Inhabited Prop :=
{ default := True }

instance  (α : Sort u) {β : Sort v} [Inhabited β] : Inhabited (α → β) :=
{ default := fun _ => arbitrary β }

instance  (α : Sort u) {β : α → Sort v} [(a : α) → Inhabited (β a)] : Inhabited ((a : α) → β a) :=
{ default := fun a => arbitrary (β a) }

instance  : Inhabited Bool :=
{ default := false }

instance  : Inhabited True :=
{ default := trivial }

instance  : Inhabited Nat :=
{ default := 0 }

instance  : Inhabited NonScalar :=
{ default := ⟨arbitrary _⟩ }

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

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

instance  {α} [Inhabited α] : Inhabited (ForInStep α) :=
{ default := 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 :=
h₂ h₁.1

instance  {α : Sort u} [Inhabited α] : Nonempty α :=
{ val := 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 :=
match h with 
| intro h => h 

protected def Subsingleton.helim {α β : Sort u} [h₁ : Subsingleton α] (h₂ : α = β) (a : α) (b : β) : a ≅ b :=
by 
  subst h₂ 
  apply heqOfEq 
  apply Subsingleton.elim 

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

instance  (p : Prop) : Subsingleton (Decidable p) :=
Subsingleton.intro
  fun
  | (isTrue t₁) =>
    fun
    | (isTrue t₂) => proofIrrel t₁ t₂ ▸ rfl
    | (isFalse f₂) => absurd t₁ f₂
  | (isFalse f₁) =>
    fun
    | (isTrue t₂) => absurd t₂ f₁
    | (isFalse f₂) => proofIrrel f₁ f₂ ▸ rfl 

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 (motive := fun _ => Sort u) 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 h₁ h₂ => 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 r a b
| trans : ∀  a b c, TC r a b → TC r b c → TC r a c

@[elabAsEliminator]
theorem TC.ndrec {α : 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 {α : 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⟩, ⟨_, _⟩, rfl => rfl 

theorem eta (a : { x // p x }) (h : p (val a)) : mk (val a) h = a :=
by 
  cases a 
  exact rfl 

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

instance  {α : Type u} {p : α → Prop} [DecidableEq α] : DecidableEq { x : α // p x } :=
fun ⟨a, h₁⟩ ⟨b, h₂⟩ =>
  if h : a = b then
    isTrue
      (by 
          subst h;
          exact rfl) 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 α β) :=
{ default := Sum.inl (arbitrary α) }

instance Sum.inhabitedRight [h : Inhabited β] : Inhabited (Sum α β) :=
{ default := 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 (α × β) :=
{ default := (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 (e₁ ▸ 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  [BEq α] [BEq β] : BEq (α × β) :=
{ beq := fun ⟨a₁, b₁⟩ ⟨a₂, b₂⟩ => a₁ == a₂ && b₁ == b₂ }

instance  [Less α] [Less β] : Less (α × β) :=
{ Less := fun s t => s.1 < t.1 ∨ (s.1 = t.1 ∧ s.2 < t.2) }

instance prodHasDecidableLt [Less α] [Less β] [DecidableEq α] [DecidableEq β] [(a b : α) → Decidable (a < b)]
  [(a b : β) → Decidable (a < b)] : (s t : α × β) → Decidable (s < t) :=
fun t s => inferInstanceAs (Decidable (_ ∨ _))

theorem Prod.ltDef [Less α] [Less β] (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⟩

protected theorem PSigma.eta {α : Sort u} {β : α → Sort v} {a₁ a₂ : α} {b₁ : β a₁} {b₂ : β a₂} (h₁ : a₁ = a₂)
  (h₂ : Eq.rec (motive := fun a _ => β a) b₁ h₁ = b₂) : PSigma.mk a₁ b₁ = PSigma.mk a₂ b₂ :=
by 
  subst h₁ 
  subst h₂ 
  exact rfl 

theorem punitEq (a b : PUnit) : a = b :=
by 
  cases a;
  cases b;
  exact rfl 

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

instance  : Subsingleton PUnit :=
Subsingleton.intro punitEq 

instance  : Inhabited PUnit :=
{ default := ⟨⟩ }

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

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

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

namespace Setoid 

variables{α : Sort u}[Setoid α]

theorem refl (a : α) : a ≈ a :=
(Setoid.iseqv α).1 a 

theorem symm {a b : α} (hab : a ≈ b) : b ≈ a :=
(Setoid.iseqv α).2.1 hab 

theorem trans {a b c : α} (hab : a ≈ b) (hbc : b ≈ c) : a ≈ c :=
(Setoid.iseqv α).2.2 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 (β := fun q => Exists (fun a => (Quot.mk r a) = q)) 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 (motive := fun x _ => β x) (f a) (sound p)) = f b) :
  ∀  a b, r a b → Quot.indep f a = Quot.indep f b :=
fun a b e => PSigma.eta (sound e) (h a b e)

protected theorem liftIndepPr1 (f : ∀  a, β (Quot.mk r a))
  (h : ∀  (a b : α) (p : r a b), (Eq.rec (motive := fun x _ => β x) (f a) (sound p)) = f b) (q : Quot r) :
  (lift (Quot.indep f) (Quot.indepCoherent f h) q).1 = q :=
by 
  induction q using Quot.ind 
  exact rfl

@[reducible, elabAsEliminator, inline]
protected def rec (f : ∀  a, β (Quot.mk r a))
  (h : ∀  (a b : α) (p : r a b), (Eq.rec (motive := fun x _ => β x) (f a) (sound p)) = 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 (motive := fun x _ => β x) (f a) (sound p)) = 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 :=
by 
  induction q using Quot.rec 
  apply f 
  apply Subsingleton.elim

@[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 (motive := fun x _ => β x) (f a) (sound p)) ≅ 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 (motive := fun a _ => β a) (f a) (Quotient.sound p)) = 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 (motive := fun a _ => β a) (f a) (Quotient.sound p)) = f b) :=
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₂ :=
by 
  induction q₁ using Quotient.ind 
  induction q₂ using Quotient.ind 
  apply h

@[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₂ :=
by 
  induction q₁ using Quotient.ind 
  induction q₂ using Quotient.ind 
  apply h

@[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₃ :=
by 
  induction q₁ using Quotient.ind 
  induction q₂ using Quotient.ind 
  induction q₃ using Quotient.ind 
  apply h 

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 :=
Quot.inductionOn (β := fun q => rel q q) 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}
  [s : ∀  a b, Subsingleton (φ (Quotient.mk a) (Quotient.mk b))] (q₁ : Quotient s₁) (q₂ : Quotient s₂)
  (g : ∀  a b, φ (Quotient.mk a) (Quotient.mk b)) : φ q₁ q₂ :=
by 
  induction q₁ using Quot.recOnSubsingleton 
  induction q₂ using Quot.recOnSubsingleton 
  intro a;
  apply s 
  induction q₂ using Quot.recOnSubsingleton 
  intro a;
  apply s 
  apply g 

end 

end Quotient 

section 

variable{α : Type u}

variable(r : α → α → Prop)

instance  {α : Sort u} {s : Setoid α} [d : ∀  (a b : α), Decidable (a ≈ b)] : DecidableEq (Quotient s) :=
fun (q₁ q₂ : Quotient s) =>
  Quotient.recOnSubsingleton₂ (φ := fun a b => Decidable (a = b)) 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 :=
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₂ :=
by 
  show extfunApp (Quotient.mk f₁) = extfunApp (Quotient.mk f₂)
  apply congrArg 
  apply Quotient.sound 
  exact h 

end 

instance  {α : 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)

@[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} {motive : Squash α → Prop} (h : ∀  (a : α), motive (Squash.mk a)) :
  ∀  (q : Squash α), motive q :=
Quot.ind h

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

instance  {α} : Subsingleton (Squash α) :=
⟨fun a b =>
    Squash.ind (motive := fun a => a = b)
      (fun a =>
          Squash.ind (motive := fun b => Squash.mk a = b)
            (fun b =>
                show Quot.mk _ a = Quot.mk _ b by 
                  apply Quot.sound;
                  exact trivial)
            b)
      a⟩

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