Init.Core

/--
`inline (f x)` is an indication to the compiler to inline the definition of `f`
at the application site itself (by comparison to the `@[inline]` attribute,
which applies to all applications of the function).
-/
@[simp] def inline {α : Sort u} (a : α) : α := a

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

/--
`flip f a b` is `f b a`. It is useful for "point-free" programming,
since it can sometimes be used to avoid introducing variables.
For example, `(·<·)` is the less-than relation,
and `flip (·<·)` is the greater-than relation.
-/
@[inline] def flip {α : Sort u} {β : Sort v} {φ : Sort w} (f : α → β → φ) : β → α → φ :=
  fun b a => f a b

@[simp] theorem Function.const_apply {y : β} {x : α} : const α y x = y := rfl

@[simp] theorem Function.comp_apply {f : β → δ} {g : α → β} {x : α} : comp f g x = f (g x) := rfl

theorem Function.comp_def {α β δ} (f : β → δ) (g : α → β) : f ∘ g = fun x => f (g x) := rfl

@[simp] theorem Function.const_comp {f : α → β} {c : γ} :
    (Function.constFunction.const β c ∘ f) = Function.const α c := by
  rfl

@[simp] theorem Function.comp_const {f : β → γ} {b : β} :
    (f ∘ Function.const α b) = Function.const α (f b) := by
  rfl

@[simp] theorem Function.true_comp {f : α → β} : ((fun _ => true) ∘ f) = fun _ => true := by
  rfl

@[simp] theorem Function.false_comp {f : α → β} : ((fun _ => false) ∘ f) = fun _ => false := by
  rfl

/--
`Empty.elim : Empty → C` says that a value of any type can be constructed from
`Empty`. This can be thought of as a compiler-checked assertion that a code path is unreachable.
-/
@[macro_inline] def Empty.elim {C : Sort u} : Empty → C := Empty.rec

/-- Decidable equality for Empty -/
instance : DecidableEq Empty := fun a => a.elim

/--
`PEmpty.elim : Empty → C` says that a value of any type can be constructed from
`PEmpty`. This can be thought of as a compiler-checked assertion that a code path is unreachable.
-/
@[macro_inline] def PEmpty.elim {C : Sort _} : PEmpty → C := fun a => nomatch a

/-- Decidable equality for PEmpty -/
instance : DecidableEq PEmpty := fun a => a.elim

/--
Delays evaluation. The delayed code is evaluated at most once.

A thunk is code that constructs a value when it is requested via `Thunk.get`, `Thunk.map`, or
`Thunk.bind`. The resulting value is cached, so the code is executed at most once. This is also
known as lazy or call-by-need evaluation.

The Lean runtime has special support for the `Thunk` type in order to implement the caching
behavior.
-/
structure Thunk (α : Type u) : Type u where
  /--
  Constructs a new thunk from a function `Unit → α` that will be called when the thunk is first
  forced.

  The result is cached. It is re-used when the thunk is forced again.
  -/
  mk ::
  /-- Extract the getter function out of a thunk. Use `Thunk.get` instead. -/
  private fn : Unit → α

/--
Stores an already-computed value in a thunk.

Because the value has already been computed, there is no laziness.
-/
@[extern "lean_thunk_pure"] protected def Thunk.pure (a : α) : Thunk α :=
  ⟨fun _ => a⟩

/--
Gets the thunk's value. If the value is cached, it is returned in constant time; if not, it is
computed.

Computed values are cached, so the value is not recomputed.
-/
-- NOTE: we use `Thunk.get` instead of `Thunk.fn` as the accessor primitive as the latter has an additional `Unit` argument
@[extern "lean_thunk_get_own"] protected def Thunk.get (x : @& Thunk α) : α :=
  x.fn ()

/--
Constructs a new thunk that forces `x` and then applies `x` to the result. Upon forcing, the result
of `f` is cached and the reference to the thunk `x` is dropped.
-/
@[inline] protected def Thunk.map (f : α → β) (x : Thunk α) : Thunk β :=
  ⟨fun _ => f x.get⟩

/--
Constructs a new thunk that applies `f` to the result of `x` when forced.
-/
@[inline] protected def Thunk.bind (x : Thunk α) (f : α → Thunk β) : Thunk β :=
  ⟨fun _ => (f x.get).get⟩

@[simp] theorem Thunk.sizeOf_eq [SizeOf α] (a : Thunk α) : sizeOf a = 1 + sizeOf a.get := by
   cases a; rfl

instance thunkCoe : CoeTail α (Thunk α) where
  -- Since coercions are expanded eagerly, `a` is evaluated lazily.
  coe a := ⟨fun _ => a⟩

/-- A variation on `Eq.ndrec` with the equality argument first. -/
abbrev Eq.ndrecOn.{u1, u2} {α : Sort u2} {a : α} {motive : α → Sort u1} {b : α} (h : a = b) (m : motive a) : motive b :=
  Eq.ndrec m h

/--
If and only if, or logical bi-implication. `a ↔ b` means that `a` implies `b` and vice versa.
By `propext`, this implies that `a` and `b` are equal and hence any expression involving `a`
is equivalent to the corresponding expression with `b` instead.
-/
structure Iff (a b : Prop) : Prop where
  /-- If `a → b` and `b → a` then `a` and `b` are equivalent. -/
  intro ::
  /-- Modus ponens for if and only if. If `a ↔ b` and `a`, then `b`. -/
  mp : a → b
  /-- Modus ponens for if and only if, reversed. If `a ↔ b` and `b`, then `a`. -/
  mpr : b → a

@[inherit_doc] infix:20 " <-> " => Iff

@[inherit_doc] infix:20 " ↔ "   => Iff

/--
The disjoint union of types `α` and `β`, ordinarily written `α ⊕ β`.

An element of `α ⊕ β` is either an `a : α` wrapped in `Sum.inl` or a `b : β` wrapped in `Sum.inr`.
`α ⊕ β` is not equivalent to the set-theoretic union of `α` and `β` because its values include an
indication of which of the two types was chosen. The union of a singleton set with itself contains
one element, while `Unit ⊕ Unit` contains distinct values `inl ()` and `inr ()`.
-/
inductive Sum (α : Type u) (β : Type v) where
  /-- Left injection into the sum type `α ⊕ β`. -/
  | inl (val : α) : Sum α β
  /-- Right injection into the sum type `α ⊕ β`. -/
  | inr (val : β) : Sum α β

@[inherit_doc] infixr:30 " ⊕ " => Sum

/--
The disjoint union of arbitrary sorts `α` `β`, or `α ⊕' β`.

It differs from `α ⊕ β` in that it allows `α` and `β` to have arbitrary sorts `Sort u` and `Sort v`,
instead of restricting them to `Type u` and `Type v`. This means that it can be used in situations
where one side is a proposition, like `True ⊕' Nat`. However, the resulting universe level
constraints are often more difficult to solve than those that result from `Sum`.
-/
inductive PSum (α : Sort u) (β : Sort v) where
  /-- Left injection into the sum type `α ⊕' β`.-/
  | inl (val : α) : PSum α β
  /-- Right injection into the sum type `α ⊕' β`. -/
  | inr (val : β) : PSum α β

@[inherit_doc] infixr:30 " ⊕' " => PSum

/--
If the left type in a sum is inhabited then the sum is inhabited.

This is not an instance to avoid non-canonical instances when both the left and right types are
inhabited.
-/
@[reducible] def PSum.inhabitedLeft {α β} [Inhabited α] : Inhabited (PSum α β) := ⟨PSum.inl default⟩

/--
If the right type in a sum is inhabited then the sum is inhabited.

This is not an instance to avoid non-canonical instances when both the left and right types are
inhabited.
-/
@[reducible] def PSum.inhabitedRight {α β} [Inhabited β] : Inhabited (PSum α β) := ⟨PSum.inr default⟩

instance PSum.nonemptyLeft [h : Nonempty α] : Nonempty (PSum α β) :=
  Nonempty.elim h (fun a => ⟨PSum.inl a⟩)

instance PSum.nonemptyRight [h : Nonempty β] : Nonempty (PSum α β) :=
  Nonempty.elim h (fun b => ⟨PSum.inr b⟩)

/--
Dependent pairs, in which the second element's type depends on the value of the first element. The
type `Sigma β` is typically written `Σ a : α, β a` or `(a : α) × β a`.

Although its values are pairs, `Sigma` is sometimes known as the *dependent sum type*, since it is
the type level version of an indexed summation.
-/
@[pp_using_anonymous_constructor]
structure Sigma {α : Type u} (β : α → Type v) where
  /--
  Constructs a dependent pair.

  Using this constructor in a context in which the type is not known usually requires a type
  ascription to determine `β`. This is because the desired relationship between the two values can't
  generally be determined automatically.
  -/
  mk ::
  /--
  The first component of a dependent pair.
  -/
  fst : α
  /--
  The second component of a dependent pair. Its type depends on the first component.
  -/
  snd : β fst

/--
Fully universe-polymorphic dependent pairs, in which the second element's type depends on the value
of the first element and both types are allowed to be propositions. The type `PSigma β` is typically
written `Σ' a : α, β a` or `(a : α) ×' β a`.

In practice, this generality leads to universe level constraints that are difficult to solve, so
`PSigma` is rarely used in manually-written code. It is usually only used in automation that
constructs pairs of arbitrary types.

To pair a value with a proof that a predicate holds for it, use `Subtype`. To demonstrate that a
value exists that satisfies a predicate, use `Exists`. A dependent pair with a proposition as its
first component is not typically useful due to proof irrelevance: there's no point in depending on a
specific proof because all proofs are equal anyway.
-/
@[pp_using_anonymous_constructor]
structure PSigma {α : Sort u} (β : α → Sort v) where
  /-- Constructs a fully universe-polymorphic dependent pair. -/
  mk ::
  /--
  The first component of a dependent pair.
  -/
  fst : α
  /--
  The second component of a dependent pair. Its type depends on the first component.
  -/
  snd : β fst

/--
Existential quantification. If `p : α → Prop` is a predicate, then `∃ x : α, p x`
asserts that there is some `x` of type `α` such that `p x` holds.
To create an existential proof, use the `exists` tactic,
or the anonymous constructor notation `⟨x, h⟩`.
To unpack an existential, use `cases h` where `h` is a proof of `∃ x : α, p x`,
or `let ⟨x, hx⟩ := h` where `.

Because Lean has proof irrelevance, any two proofs of an existential are
definitionally equal. One consequence of this is that it is impossible to recover the
witness of an existential from the mere fact of its existence.
For example, the following does not compile:
```
example (h : ∃ x : Nat, x = x) : Nat :=
  let ⟨x, _⟩ := h  -- fail, because the goal is `Nat : Type`
  x
```
The error message `recursor 'Exists.casesOn' can only eliminate into Prop` means
that this only works when the current goal is another proposition:
```
example (h : ∃ x : Nat, x = x) : True :=
  let ⟨x, _⟩ := h  -- ok, because the goal is `True : Prop`
  trivial
```
-/
inductive Exists {α : Sort u} (p : α → Prop) : Prop where
  /-- Existential introduction. If `a : α` and `h : p a`,
  then `⟨a, h⟩` is a proof that `∃ x : α, p x`. -/
  | intro (w : α) (h : p w) : Exists p

/--
An indication of whether a loop's body terminated early that's used to compile the `for x in xs`
notation.

A collection's `ForIn` or `ForIn'` instance describe's how to iterate over its elements. The monadic
action that represents the body of the loop returns a `ForInStep α`, where `α` is the local state
used to implement features such as `let mut`.
-/
inductive ForInStep (α : Type u) where
  /--
  The loop should terminate early.

  `ForInStep.done` is produced by uses of `break` or `return` in the loop body.
  -/
  | done  : α → ForInStep α
  /--
  The loop should continue with the next iteration, using the returned state.

  `ForInStep.yield` is produced by `continue` and by reaching the bottom of the loop body.
  -/
  | yield : α → ForInStep α
  deriving Inhabited

Inhabited

/--
Monadic iteration in `do`-blocks, using the `for x in xs` notation.

The parameter `m` is the monad of the `do`-block in which iteration is performed, `ρ` is the type of
the collection being iterated over, and `α` is the type of elements.
-/
class ForIn (m : Type u₁ → Type u₂) (ρ : Type u) (α : outParam (Type v)) where
  /--
  Monadically iterates over the contents of a collection `xs`, with a local state `b` and the
  possibility of early termination.

  Because a `do` block supports local mutable bindings along with `return`, and `break`, the monadic
  action passed to `ForIn.forIn` takes a starting state in addition to the current element of the
  collection and returns an updated state together with an indication of whether iteration should
  continue or terminate. If the action returns `ForInStep.done`, then `ForIn.forIn` should stop
  iteration and return the updated state. If the action returns `ForInStep.yield`, then
  `ForIn.forIn` should continue iterating if there are further elements, passing the updated state
  to the action.

  More information about the translation of `for` loops into `ForIn.forIn` is available in [the Lean
  reference manual](lean-manual://section/monad-iteration-syntax).
  -/
  forIn {β} [Monad m] (xs : ρ) (b : β) (f : α → β → m (ForInStep β)) : m β

/--
Monadic iteration in `do`-blocks with a membership proof, using the `for h : x in xs` notation.

The parameter `m` is the monad of the `do`-block in which iteration is performed, `ρ` is the type of
the collection being iterated over, `α` is the type of elements, and `d` is the specific membership
predicate to provide.
-/
class ForIn' (m : Type u₁ → Type u₂) (ρ : Type u) (α : outParam (Type v)) (d : outParam (Membership α ρ)) where
  /--
  Monadically iterates over the contents of a collection `xs`, with a local state `b` and the
  possibility of early termination. At each iteration, the body of the loop is provided with a proof
  that the current element is in the collection.

  Because a `do` block supports local mutable bindings along with `return`, and `break`, the monadic
  action passed to `ForIn'.forIn'` takes a starting state in addition to the current element of the
  collection with its membership proof. The action returns an updated state together with an
  indication of whether iteration should continue or terminate. If the action returns
  `ForInStep.done`, then `ForIn'.forIn'` should stop iteration and return the updated state. If the
  action returns `ForInStep.yield`, then `ForIn'.forIn'` should continue iterating if there are
  further elements, passing the updated state to the action.

  More information about the translation of `for` loops into `ForIn'.forIn'` is available in [the
  Lean reference manual](lean-manual://section/monad-iteration-syntax).
  -/
  forIn' {β} [Monad m] (x : ρ) (b : β) (f : (a : α) → a ∈ x → β → m (ForInStep β)) : m β

/--
Auxiliary type used to compile `do` notation. It is used when compiling a do block
nested inside a combinator like `tryCatch`. It encodes the possible ways the
block can exit:
* `pure (a : α) s` means that the block exited normally with return value `a`.
* `return (b : β) s` means that the block exited via a `return b` early-exit command.
* `break s` means that `break` was called, meaning that we should exit
  from the containing loop.
* `continue s` means that `continue` was called, meaning that we should continue
  to the next iteration of the containing loop.

All cases return a value `s : σ` which bundles all the mutable variables of the do-block.
-/
inductive DoResultPRBC (α β σ : Type u) where
  /-- `pure (a : α) s` means that the block exited normally with return value `a` -/
  | pure : α → σ → DoResultPRBC α β σ
  /-- `return (b : β) s` means that the block exited via a `return b` early-exit command -/
  | return : β → σ → DoResultPRBC α β σ
  /-- `break s` means that `break` was called, meaning that we should exit
  from the containing loop -/
  | break : σ → DoResultPRBC α β σ
  /-- `continue s` means that `continue` was called, meaning that we should continue
  to the next iteration of the containing loop -/
  | continue : σ → DoResultPRBC α β σ

/--
Auxiliary type used to compile `do` notation. It is the same as
`DoResultPRBC α β σ` except that `break` and `continue` are not available
because we are not in a loop context.
-/
inductive DoResultPR (α β σ : Type u) where
  /-- `pure (a : α) s` means that the block exited normally with return value `a` -/
  | pure   : α → σ → DoResultPR α β σ
  /-- `return (b : β) s` means that the block exited via a `return b` early-exit command -/
  | return : β → σ → DoResultPR α β σ

/--
Auxiliary type used to compile `do` notation. It is an optimization of
`DoResultPRBC PEmpty PEmpty σ` to remove the impossible cases,
used when neither `pure` nor `return` are possible exit paths.
-/
inductive DoResultBC (σ : Type u) where
  /-- `break s` means that `break` was called, meaning that we should exit
  from the containing loop -/
  | break    : σ → DoResultBC σ
  /-- `continue s` means that `continue` was called, meaning that we should continue
  to the next iteration of the containing loop -/
  | continue : σ → DoResultBC σ

/--
Auxiliary type used to compile `do` notation. It is an optimization of
either `DoResultPRBC α PEmpty σ` or `DoResultPRBC PEmpty α σ` to remove the
impossible case, used when either `pure` or `return` is never used.
-/
inductive DoResultSBC (α σ : Type u) where
  /-- This encodes either `pure (a : α)` or `return (a : α)`:
  * `pure (a : α) s` means that the block exited normally with return value `a`
  * `return (b : β) s` means that the block exited via a `return b` early-exit command

  The one that is actually encoded depends on the context of use. -/
  | pureReturn : α → σ → DoResultSBC α σ
  /-- `break s` means that `break` was called, meaning that we should exit
  from the containing loop -/
  | break    : σ → DoResultSBC α σ
  /-- `continue s` means that `continue` was called, meaning that we should continue
  to the next iteration of the containing loop -/
  | continue   : σ → DoResultSBC α σ

/-- `HasEquiv α` is the typeclass which supports the notation `x ≈ y` where `x y : α`.-/
class HasEquiv (α : Sort u) where
  /-- `x ≈ y` says that `x` and `y` are equivalent. Because this is a typeclass,
  the notion of equivalence is type-dependent. -/
  Equiv : α → α → Sort v

@[inherit_doc] infix:50 " ≈ "  => HasEquiv.Equiv

/-- Notation type class for the subset relation `⊆`. -/
class HasSubset (α : Type u) where
  /-- Subset relation: `a ⊆ b`  -/
  Subset : α → α → Prop

/-- Notation type class for the strict subset relation `⊂`. -/
class HasSSubset (α : Type u) where
  /-- Strict subset relation: `a ⊂ b`  -/
  SSubset : α → α → Prop

/-- Superset relation: `a ⊇ b`  -/
abbrev Superset [HasSubset α] (a b : α) := Subset b a

/-- Strict superset relation: `a ⊃ b`  -/
abbrev SSuperset [HasSSubset α] (a b : α) := SSubset b a

/-- Notation type class for the union operation `∪`. -/
class Union (α : Type u) where
  /-- `a ∪ b` is the union of`a` and `b`. -/
  union : α → α → α

/-- Notation type class for the intersection operation `∩`. -/
class Inter (α : Type u) where
  /-- `a ∩ b` is the intersection of`a` and `b`. -/
  inter : α → α → α

/-- Notation type class for the set difference `\`. -/
class SDiff (α : Type u) where
  /--
  `a \ b` is the set difference of `a` and `b`,
  consisting of all elements in `a` that are not in `b`.
  -/
  sdiff : α → α → α

/-- Subset relation: `a ⊆ b`  -/
infix:50 " ⊆ " => Subset

/-- Strict subset relation: `a ⊂ b`  -/
infix:50 " ⊂ " => SSubset

/-- Superset relation: `a ⊇ b`  -/
infix:50 " ⊇ " => Superset

/-- Strict superset relation: `a ⊃ b`  -/
infix:50 " ⊃ " => SSuperset

/-- `a ∪ b` is the union of`a` and `b`. -/
infixl:65 " ∪ " => Union.union

/-- `a ∩ b` is the intersection of`a` and `b`. -/
infixl:70 " ∩ " => Inter.inter

/--
`a \ b` is the set difference of `a` and `b`,
consisting of all elements in `a` that are not in `b`.
-/
infix:70 " \\ " => SDiff.sdiff

/-- `EmptyCollection α` is the typeclass which supports the notation `∅`, also written as `{}`. -/
class EmptyCollection (α : Type u) where
  /-- `∅` or `{}` is the empty set or empty collection.
  It is supported by the `EmptyCollection` typeclass. -/
  emptyCollection : α

@[inherit_doc] notation "{" "}" => EmptyCollection.emptyCollection

@[inherit_doc] notation "∅"     => EmptyCollection.emptyCollection

/--
Type class for the `insert` operation.
Used to implement the `{ a, b, c }` syntax.
-/
class Insert (α : outParam <| Type u) (γ : Type v) where
  /-- `insert x xs` inserts the element `x` into the collection `xs`. -/
  insert : α → γ → γ

/--
Type class for the `singleton` operation.
Used to implement the `{ a, b, c }` syntax.
-/
class Singleton (α : outParam <| Type u) (β : Type v) where
  /-- `singleton x` is a collection with the single element `x` (notation: `{x}`). -/
  singleton : α → β

/-- `insert x ∅ = {x}` -/
class LawfulSingleton (α : Type u) (β : Type v) [EmptyCollection β] [Insert α β] [Singleton α β] :
    Prop where
  /-- `insert x ∅ = {x}` -/
  insert_empty_eq (x : α) : (insert x ∅ : β) = singleton x

@[deprecated insert_empty_eq (since := "2025-03-12")]
theorem insert_emptyc_eq [EmptyCollection β] [Insert α β] [Singleton α β]
    [LawfulSingleton α β] (x : α) : (insert x ∅ : β) = singleton x :=
  insert_empty_eq _

@[deprecated insert_empty_eq (since := "2025-03-12")]
theorem LawfulSingleton.insert_emptyc_eq [EmptyCollection β] [Insert α β] [Singleton α β]
    [LawfulSingleton α β] (x : α) : (insert x ∅ : β) = singleton x :=
  insert_empty_eq _

/-- Type class used to implement the notation `{ a ∈ c | p a }` -/
class Sep (α : outParam <| Type u) (γ : Type v) where
  /-- Computes `{ a ∈ c | p a }`. -/
  sep : (α → Prop) → γ → γ

/--
`Task α` is a primitive for asynchronous computation.
It represents a computation that will resolve to a value of type `α`,
possibly being computed on another thread. This is similar to `Future` in Scala,
`Promise` in Javascript, and `JoinHandle` in Rust.

The tasks have an overridden representation in the runtime.
-/
structure Task (α : Type u) : Type u where
  /-- `Task.pure (a : α)` constructs a task that is already resolved with value `a`. -/
  pure ::
  /--
  Blocks the current thread until the given task has finished execution, and then returns the result
  of the task. If the current thread is itself executing a (non-dedicated) task, the maximum
  threadpool size is temporarily increased by one while waiting so as to ensure the process cannot
  be deadlocked by threadpool starvation. Note that when the current thread is unblocked, more tasks
  than the configured threadpool size may temporarily be running at the same time until sufficiently
  many tasks have finished.

  `Task.map` and `Task.bind` should be preferred over `Task.get` for setting up task dependencies
  where possible as they do not require temporarily growing the threadpool in this way.
  -/
  get : α
  deriving Inhabited, Nonempty

Inhabited, Nonempty

Nonempty

/--
Task priority.

Tasks with higher priority will always be scheduled before tasks with lower priority. Tasks with a
priority greater than `Task.Priority.max` are scheduled on dedicated threads.
-/
abbrev Priority := Nat

/-- The default priority for spawned tasks, also the lowest priority: `0`. -/
def Priority.default : Priority := 0

/--
The highest regular priority for spawned tasks: `8`.

Spawning a task with a priority higher than `Task.Priority.max` is not an error but will spawn a
dedicated worker for the task. This is indicated using `Task.Priority.dedicated`. Regular priority
tasks are placed in a thread pool and worked on according to their priority order.
-/
-- see `LEAN_MAX_PRIO`
def Priority.max : Priority := 8

/--
Indicates that a task should be scheduled on a dedicated thread.

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

/--
`NonScalar` is a type that is not a scalar value in our runtime.
It is used as a stand-in for an arbitrary boxed value to avoid excessive
monomorphization, and it is only created using `unsafeCast`. It is somewhat
analogous to C `void*` in usage, but the type itself is not special.
-/
structure NonScalar where
  /-- You should not use this function -/ mk ::
  /-- You should not use this function -/ val : Nat

/--
`PNonScalar` is a type that is not a scalar value in our runtime.
It is used as a stand-in for an arbitrary boxed value to avoid excessive
monomorphization, and it is only created using `unsafeCast`. It is somewhat
analogous to C `void*` in usage, but the type itself is not special.

This is the universe-polymorphic version of `PNonScalar`; it is preferred to use
`NonScalar` instead where applicable.
-/
inductive PNonScalar : Type u where
  /-- You should not use this function -/
  | mk (v : Nat) : PNonScalar

@[simp] protected theorem Nat.add_zero (n : Nat) : n + 0 = n := rfl

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

/--
`strictOr` is the same as `or`, but it does not use short-circuit evaluation semantics:
both sides are evaluated, even if the first value is `true`.
-/
@[extern "lean_strict_or"] def strictOr  (b₁ b₂ : Bool) := b₁ || b₂

/--
`strictAnd` is the same as `and`, but it does not use short-circuit evaluation semantics:
both sides are evaluated, even if the first value is `false`.
-/
@[extern "lean_strict_and"] def strictAnd (b₁ b₂ : Bool) := b₁ && b₂

/--
`x != y` is boolean not-equal. It is the negation of `x == y` which is supplied by
the `BEq` typeclass.

Unlike `x ≠ y` (which is notation for `Ne x y`), this is `Bool` valued instead of
`Prop` valued. It is mainly intended for programming applications.
-/
@[inline] def bne {α : Type u} [BEq α] (a b : α) : Bool :=
  !(a == b)

@[inherit_doc] infix:50 " != " => bne

/--
A Boolean equality test coincides with propositional equality.

In other words:
 * `a == b` implies `a = b`.
 * `a == a` is true.
-/
class LawfulBEq (α : Type u) [BEq α] : Prop where
  /-- If `a == b` evaluates to `true`, then `a` and `b` are equal in the logic. -/
  eq_of_beq : {a b : α} → a == b → a = b
  /-- `==` is reflexive, that is, `(a == a) = true`. -/
  protected rfl : {a : α} → a == a

instance : LawfulBEq Bool where
  eq_of_beq {a b} h := by cases a <;> cases b <;> first | rfl | contradiction
  rfl {a} := by cases a <;> decide

instance [DecidableEq α] : LawfulBEq α where
  eq_of_beq := of_decide_eq_true
  rfl := of_decide_eq_self_eq_true _

instance : LawfulBEq Char := inferInstance

instance : LawfulBEq String := inferInstance

@[inherit_doc True.intro] theorem trivial : True := ⟨⟩

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

theorem not_false : ¬False := id

theorem not_not_intro {p : Prop} (h : p) : ¬ ¬ p :=
  fun hn : ¬ p => hn h

/--
If `h : α = β` is a proof of type equality, then `h.mp : α → β` is the induced
"cast" operation, mapping elements of `α` to elements of `β`.

You can prove theorems about the resulting element by induction on `h`, since
`rfl.mp` is definitionally the identity function.
-/
@[macro_inline] def Eq.mp {α β : Sort u} (h : α = β) (a : α) : β :=
  h ▸ a

/--
If `h : α = β` is a proof of type equality, then `h.mpr : β → α` is the induced
"cast" operation in the reverse direction, mapping elements of `β` to elements of `α`.

You can prove theorems about the resulting element by induction on `h`, since
`rfl.mpr` is definitionally the identity function.
-/
@[macro_inline] def Eq.mpr {α β : Sort u} (h : α = β) (b : β) : α :=
  h ▸ b

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

@[simp] theorem cast_eq {α : Sort u} (h : α = α) (a : α) : cast h a = a :=
  rfl

/--
`a ≠ b`, or `Ne a b` is defined as `¬ (a = b)` or `a = b → False`,
and asserts that `a` and `b` are not equal.
-/
@[reducible] def Ne {α : Sort u} (a b : α) :=
  ¬(a = b)

@[inherit_doc] infix:50 " ≠ "  => Ne

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

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

theorem ne_comm {α} {a b : α} : a ≠ ba ≠ b ↔ b ≠ a := ⟨Ne.symm, Ne.symm⟩

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

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

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

theorem true_ne_false : ¬True = False := ne_false_of_self trivial

theorem false_ne_true : FalseFalse ≠ True := fun h => h.symm ▸ trivial

theorem Bool.of_not_eq_true : {b : Bool} → ¬ (b = true) → b = false
  | true,  h => absurd rfl h
  | false, _ => rfl

theorem Bool.of_not_eq_false : {b : Bool} → ¬ (b = false) → b = true
  | true,  _ => rfl
  | false, h => absurd rfl h

theorem ne_of_beq_false [BEq α] [LawfulBEq α] {a b : α} (h : (a == b) = false) : a ≠ b := by
  intro h'; subst h'; have : true = false := Eq.trans LawfulBEq.rfl.symm h; contradiction

theorem beq_false_of_ne [BEq α] [LawfulBEq α] {a b : α} (h : a ≠ b) : (a == b) = false :=
  have : ¬ (a == b) = true := by
    intro h'; rw [eq_of_beq h'] at h; contradiction
  Bool.of_not_eq_true this

/-- Non-dependent recursor for `HEq` -/
noncomputable def HEq.ndrec.{u1, u2} {α : Sort u2} {a : α} {motive : {β : Sort u2} → β → Sort u1} (m : motive a) {β : Sort u2} {b : β} (h : HEq a b) : motive b :=
  h.rec m

/-- `HEq.ndrec` variant -/
noncomputable def HEq.ndrecOn.{u1, u2} {α : Sort u2} {a : α} {motive : {β : Sort u2} → β → Sort u1} {β : Sort u2} {b : β} (h : HEq a b) (m : motive a) : motive b :=
  h.rec m

/-- `HEq.ndrec` variant -/
noncomputable def HEq.elim {α : Sort u} {a : α} {p : α → Sort v} {b : α} (h₁ : HEq a b) (h₂ : p a) : p b :=
  eq_of_heq h₁ ▸ h₂

/-- Substitution with heterogeneous equality. -/
theorem HEq.subst {p : (T : Sort u) → T → Prop} (h₁ : HEq a b) (h₂ : p α a) : p β b :=
  HEq.ndrecOn h₁ h₂

/-- Heterogeneous equality is symmetric. -/
@[symm] theorem HEq.symm (h : HEq a b) : HEq b a :=
  h.rec (HEq.refl a)

/-- Propositionally equal terms are also heterogeneously equal. -/
theorem heq_of_eq (h : a = a') : HEq a a' :=
  Eq.subst h (HEq.refl a)

/-- Heterogeneous equality is transitive. -/
theorem HEq.trans (h₁ : HEq a b) (h₂ : HEq b c) : HEq a c :=
  HEq.subst h₂ h₁

/-- Heterogeneous equality precomposes with propositional equality. -/
theorem heq_of_heq_of_eq (h₁ : HEq a b) (h₂ : b = b') : HEq a b' :=
  HEq.trans h₁ (heq_of_eq h₂)

/-- Heterogeneous equality postcomposes with propositional equality. -/
theorem heq_of_eq_of_heq (h₁ : a = a') (h₂ : HEq a' b) : HEq a b :=
  HEq.trans (heq_of_eq h₁) h₂

/-- If two terms are heterogeneously equal then their types are propositionally equal. -/
theorem type_eq_of_heq (h : HEq a b) : α = β :=
  h.rec (Eq.refl α)

/--
Rewriting inside `φ` using `Eq.recOn` yields a term that's heterogeneously equal to the original
term.
-/
theorem eqRec_heq {α : Sort u} {φ : α → Sort v} {a a' : α} : (h : a = a') → (p : φ a) → HEq (Eq.recOn (motive := fun x _ => φ x) h p) p
  | rfl, p => HEq.refl p

/--
If casting a term with `Eq.rec` to another type makes it equal to some other term, then the two
terms are heterogeneously equal.
-/
theorem heq_of_eqRec_eq {α β : Sort u} {a : α} {b : β} (h₁ : α = β) (h₂ : Eq.rec (motive := fun α _ => α) a h₁ = b) : HEq a b := by
  subst h₁
  apply heq_of_eq
  exact h₂

/--
The result of casting a term with `cast` is heterogeneously equal to the original term.
-/
theorem cast_heq {α β : Sort u} : (h : α = β) → (a : α) → HEq (cast h a) a
  | rfl, a => HEq.refl a

theorem iff_iff_implies_and_implies {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)

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

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

theorem Iff.of_eq (h : a = b) : a ↔ b := h ▸ Iff.rfl

theorem Iff.trans (h₁ : a ↔ b) (h₂ : b ↔ c) : a ↔ c :=
  Iff.intro (h₂.mp ∘ h₁.mp) (h₁.mpr ∘ h₂.mpr)

instance : Trans Iff Iff Iff where
  trans := Iff.trans

theorem Eq.comm {a b : α} : a = b ↔ b = a := Iff.intro Eq.symm Eq.symm

theorem HEq.comm {a : α} {b : β} : HEqHEq a b ↔ HEq b a := Iff.intro HEq.symm HEq.symm

theorem heq_comm {a : α} {b : β} : HEqHEq a b ↔ HEq b a := HEq.comm

@[symm] theorem Iff.symm (h : a ↔ b) : b ↔ a := Iff.intro h.mpr h.mp

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

theorem iff_comm : (a ↔ b) ↔ (b ↔ a) := Iff.comm

@[symm] theorem And.symm : a ∧ b → b ∧ a := fun ⟨ha, hb⟩ => ⟨hb, ha⟩

theorem And.comm : a ∧ ba ∧ b ↔ b ∧ a := Iff.intro And.symm And.symm

theorem and_comm : a ∧ ba ∧ b ↔ b ∧ a := And.comm

@[symm] theorem Or.symm : a ∨ b → b ∨ a := .rec .inr .inl

theorem Or.comm : a ∨ ba ∨ b ↔ b ∨ a := Iff.intro Or.symm Or.symm

theorem or_comm : a ∨ ba ∨ b ↔ b ∨ a := Or.comm

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

@[simp] theorem decide_true (h : Decidable True) : @decide True h = true :=
  match h with
  | isTrueisTrue _  => rfl
  | isFalseisFalse h => False.elim <| h ⟨⟩

@[simp] theorem decide_false (h : Decidable False) : @decide False h = false :=
  match h with
  | isFalseisFalse _ => rfl
  | isTrueisTrue h  => False.elim h

@[deprecated decide_true (since := "2024-11-05")] abbrev decide_true_eq_true := decide_true

@[deprecated decide_false (since := "2024-11-05")] abbrev decide_false_eq_false := decide_false

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

theorem toBoolUsing_eq_true {p : Prop} (d : Decidable p) (h : p) : toBoolUsing d = true :=
  decide_eq_true (inst := d) h

theorem ofBoolUsing_eq_true {p : Prop} {d : Decidable p} (h : toBoolUsing d = true) : p :=
  of_decide_eq_true (inst := d) h

theorem ofBoolUsing_eq_false {p : Prop} {d : Decidable p} (h : toBoolUsing d = false) : ¬ p :=
  of_decide_eq_false (inst := d) h

instance : Decidable True :=
  isTrue trivial

instance : Decidable False :=
  isFalse not_false

/--
Construct a `q` if some proposition `p` is decidable, and both the truth and falsity of `p` are
sufficient to construct a `q`.

This is a synonym for `dite`, the dependent if-then-else operator.
-/
@[macro_inline] def byCases {q : Sort u} [dec : Decidable p] (h1 : p → q) (h2 : ¬p → q) : q :=
  match dec with
  | isTrue h  => h1 h
  | isFalse h => h2 h

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

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

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

theorem not_and_iff_or_not {p q : Prop} [d₁ : Decidable p] [d₂ : Decidable q] : ¬ (p ∧ 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⟩ => match h with
      | Or.inl h => h hp
      | Or.inr h => h hq)

/-- Transfer a decidability proof across an equivalence of propositions. -/
@[inline] def decidable_of_decidable_of_iff [Decidable p] (h : p ↔ q) : Decidable q :=
  if hp : p then
    isTrue (Iff.mp h hp)
  else
    isFalse fun hq => absurd (Iff.mpr h hq) hp

/-- Transfer a decidability proof across an equality of propositions. -/
@[inline] def decidable_of_decidable_of_eq [Decidable p] (h : p = q) : Decidable q :=
  decidable_of_decidable_of_iff (p := p) (h ▸ Iff.rfl)

@[macro_inline] instance {p q} [Decidable p] [Decidable q] : Decidable (p → q) :=
  if hp : p then
    if hq : q then isTrue (fun _ => hq)
    else isFalse (fun h => absurd (h hp) hq)
  else isTrue (fun h => absurd h hp)

instance {p q} [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⟩

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

theorem if_neg {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 _   => rfl

/-- Split an if-then-else into cases. The `split` tactic is generally easier to use than this theorem. -/
def iteInduction {c} [inst : Decidable c] {motive : α → Sort _} {t e : α}
    (hpos : c → motive t) (hneg : ¬c → motive e) : motive (ite c t e) :=
  match inst with
  | isTrue h => hpos h
  | isFalse h => hneg h

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

theorem dif_neg {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 _   => rfl

theorem dif_eq_if (c : Prop) {h : Decidable c} {α : Sort u} (t : α) (e : α) : dite c (fun _ => t) (fun _ => e) = ite c t e :=
  match h with
  | isTrue _    => rfl
  | isFalse _   => 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 _   => dT
  | isFalse _  => 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

/-- Auxiliary definition for generating compact `noConfusion` for enumeration types -/
abbrev noConfusionTypeEnum {α : Sort u} {β : Sort v} [inst : DecidableEq β] (f : α → β) (P : Sort w) (x y : α) : Sort w :=
  (inst (f x) (f y)).casesOn
    (fun _ => P)
    (fun _ => P → P)

/-- Auxiliary definition for generating compact `noConfusion` for enumeration types -/
abbrev noConfusionEnum {α : Sort u} {β : Sort v} [inst : DecidableEq β] (f : α → β) {P : Sort w} {x y : α} (h : x = y) : noConfusionTypeEnum f P x y :=
  Decidable.casesOn
    (motive := fun (inst : Decidable (f x = f y)) => Decidable.casesOn (motive := fun _ => Sort w) inst (fun _ => P) (fun _ => P → P))
    (inst (f x) (f y))
    (fun h' => False.elim (h' (congrArg f h)))
    (fun _ => fun x => x)

instance : Inhabited Prop where
  default := True

Inhabited for NonScalar, PNonScalar, True, ForInStep

Inhabited for NonScalar, PNonScalar, True, ForInStep

Inhabited for NonScalar, PNonScalar, True, ForInStep

Inhabited for NonScalar, PNonScalar, True, ForInStep

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

/--
A _subsingleton_ is a type with at most one element. It is either empty or has a unique element.

All propositions are subsingletons because of proof irrelevance: false propositions are empty, and
all proofs of a true proposition are equal to one another. Some non-propositional types are also
subsingletons.
-/
class Subsingleton (α : Sort u) : Prop where
  /-- Prove that `α` is a subsingleton by showing that any two elements are equal. -/
  intro ::
  /-- Any two elements of a subsingleton are equal. -/
  allEq : (a b : α) → a = b

/--
If a type is a subsingleton, then all of its elements are equal.
-/
protected theorem Subsingleton.elim {α : Sort u} [h : Subsingleton α] : (a b : α) → a = b :=
  h.allEq

/--
If two types are equal and one of them is a subsingleton, then all of their elements are
[heterogeneously equal](lean-manual://section/HEq).
-/
protected theorem Subsingleton.helim {α β : Sort u} [h₁ : Subsingleton α] (h₂ : α = β) (a : α) (b : β) : HEq a b := by
  subst h₂
  apply heq_of_eq
  apply Subsingleton.elim

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

instance : Subsingleton Empty  := ⟨(·.elim)⟩

instance : Subsingleton PEmpty := ⟨(·.elim)⟩

instance [Subsingleton α] [Subsingleton β] : Subsingleton (α × β) :=
  ⟨fun {..} {..} => by congr <;> apply Subsingleton.elim⟩

instance (p : Prop) : Subsingleton (Decidable p) :=
  Subsingleton.intro fun
    | isTrue t₁ => fun
      | isTrue _   => rfl
      | isFalse f₂ => absurd t₁ f₂
    | isFalse f₁ => fun
      | isTrue t₂  => absurd t₂ f₁
      | isFalse _  => 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 (h.casesOn h₂ h₁) :=
  match h with
  | isTrue h  => h₃ h
  | isFalse h => h₄ h

/--
An equivalence relation `r : α → α → Prop` is a relation that is

* reflexive: `r x x`,
* symmetric: `r x y` implies `r y x`, and
* transitive: `r x y` and `r y z` implies `r x z`.

Equality is an equivalence relation, and equivalence relations share many of the properties of
equality.
-/
structure Equivalence {α : Sort u} (r : α → α → Prop) : Prop where
  /-- An equivalence relation is reflexive: `r x x` -/
  refl  : ∀ x, r x x
  /-- An equivalence relation is symmetric: `r x y` implies `r y x` -/
  symm  : ∀ {x y}, r x y → r y x
  /-- An equivalence relation is transitive: `r x y` and `r y z` implies `r x z` -/
  trans : ∀ {x y z}, r x y → r y z → r x z

/-- The empty relation is the relation on `α` which is always `False`. -/
def emptyRelation {α : Sort u} (_ _ : α) : Prop :=
  False

/--
`Subrelation q r` means that `q ⊆ r` or `∀ x y, q x y → r x y`.
It is the analogue of the subset relation on relations.
-/
def Subrelation {α : Sort u} (q r : α → α → Prop) :=
  ∀ {x y}, q x y → r x y

/--
The inverse image of `r : β → β → Prop` by a function `α → β` is the relation
`s : α → α → Prop` defined by `s a b = r (f a) (f b)`.
-/
def InvImage {α : Sort u} {β : Sort v} (r : β → β → Prop) (f : α → β) : α → α → Prop :=
  fun a₁ a₂ => r (f a₁) (f a₂)

/--
The transitive closure `TransGen r` of a relation `r` is the smallest relation which is
transitive and contains `r`. `TransGen r a z` if and only if there exists a sequence
`a r b r ... r z` of length at least 1 connecting `a` to `z`.
-/
inductive Relation.TransGen {α : Sort u} (r : α → α → Prop) : α → α → Prop
  /-- If `r a b`, then `TransGen r a b`. This is the base case of the transitive closure. -/
  | single {a b} : r a b → TransGen r a b
  /-- If `TransGen r a b` and `r b c`, then `TransGen r a c`.
  This is the inductive case of the transitive closure. -/
  | tail {a b c} : TransGen r a b → r b c → TransGen r a c

/-- The transitive closure is transitive. -/
theorem Relation.TransGen.trans {α : Sort u} {r : α → α → Prop} {a b c} :
    TransGen r a b → TransGen r b c → TransGen r a c := by
  intro hab hbc
  induction hbc with
  | single h => exact TransGen.tail hab h
  | tail _ h ih => exact TransGen.tail ih h

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

protected theorem eq : ∀ {a1 a2 : {x // p x}}, val a1 = val a2 → a1 = a2
  | ⟨_, _⟩, ⟨_, _⟩, 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} [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))

@[reducible, inherit_doc PSum.inhabitedLeft]
def Sum.inhabitedLeft [Inhabited α] : Inhabited (Sum α β) where
  default := Sum.inl default

@[reducible, inherit_doc PSum.inhabitedRight]
def Sum.inhabitedRight [Inhabited β] : Inhabited (Sum α β) where
  default := Sum.inr default

instance Sum.nonemptyLeft [h : Nonempty α] : Nonempty (Sum α β) :=
  Nonempty.elim h (fun a => ⟨Sum.inl a⟩)

instance Sum.nonemptyRight [h : Nonempty β] : Nonempty (Sum α β) :=
  Nonempty.elim h (fun b => ⟨Sum.inr b⟩)

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 _, Sum.inl _ => isFalse fun h => Sum.noConfusion h
  | Sum.inl _, Sum.inr _ => isFalse fun h => Sum.noConfusion h

instance [h1 : Nonempty α] [h2 : Nonempty β] : Nonempty (α × β) :=
  Nonempty.elim h1 fun x =>
    Nonempty.elim h2 fun y =>
      ⟨(x, y)⟩

instance [h1 : Nonempty α] [h2 : Nonempty β] : Nonempty (MProd α β) :=
  Nonempty.elim h1 fun x =>
    Nonempty.elim h2 fun y =>
      ⟨⟨x, y⟩⟩

instance [h1 : Nonempty α] [h2 : Nonempty β] : Nonempty (PProd α β) :=
  Nonempty.elim h1 fun x =>
    Nonempty.elim h2 fun y =>
      ⟨⟨x, y⟩⟩

instance [Inhabited α] [Inhabited β] : Inhabited (α × β) where
  default := (default, default)

instance [Inhabited α] [Inhabited β] : Inhabited (MProd α β) where
  default := ⟨default, default⟩

instance [Inhabited α] [Inhabited β] : Inhabited (PProd α β) where
  default := ⟨default, default⟩

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₂' => absurd e₂' n₂
    | isFalse n₁ => isFalse fun h => Prod.noConfusion h fun e₁' _   => absurd e₁' n₁

instance [BEq α] [BEq β] : BEq (α × β) where
  beq := fun (a₁, b₁) (a₂, b₂) => a₁ == a₂ && b₁ == b₂

/--
Lexicographical order for products.

Two pairs are lexicographically ordered if their first elements are ordered or if their first
elements are equal and their second elements are ordered.
-/
def Prod.lexLt [LT α] [LT β] (s : α × β) (t : α × β) : Prop :=
  s.1 < t.1 ∨ (s.1 = t.1 ∧ s.2 < t.2)

instance Prod.lexLtDec
    [LT α] [LT β] [DecidableEq α]
    [(a b : α) → Decidable (a < b)] [(a b : β) → Decidable (a < b)]
    : (s t : α × β) → Decidable (Prod.lexLt s t) :=
  fun _ _ => inferInstanceAs (Decidable (_ ∨ _))

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

theorem Prod.eta (p : α × β) : (p.1, p.2) = p := rfl

/--
Transforms a pair by applying functions to both elements.

Examples:
 * `(1, 2).map (· + 1) (· * 3) = (2, 6)`
 * `(1, 2).map toString (· * 3) = ("1", 6)`
-/
def Prod.map {α₁ : Type u₁} {α₂ : Type u₂} {β₁ : Type v₁} {β₂ : Type v₂}
    (f : α₁ → α₂) (g : β₁ → β₂) : α₁ × β₁ → α₂ × β₂
  | (a, b) => (f a, g b)

@[simp] theorem Prod.map_apply (f : α → β) (g : γ → δ) (x) (y) :
    Prod.map f g (x, y) = (f x, g y) := rfl

@[simp] theorem Prod.map_fst (f : α → β) (g : γ → δ) (x) : (Prod.map f g x).1 = f x.1 := rfl

@[simp] theorem Prod.map_snd (f : α → β) (g : γ → δ) (x) : (Prod.map f g x).2 = g x.2 := rfl

theorem Exists.of_psigma_prop {α : Sort 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.ndrec b₁ h₁ = b₂) : PSigma.mk a₁ b₁ = PSigma.mk a₂ b₂ := by
  subst h₁
  subst h₂
  exact rfl

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

instance : Subsingleton PUnit :=
  Subsingleton.intro PUnit.subsingleton

instance : Inhabited PUnit where
  default := ⟨⟩

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

/--
A setoid is a type with a distinguished equivalence relation, denoted `≈`.

The `Quotient` type constructor requires a `Setoid` instance.
-/
class Setoid (α : Sort u) where
  /-- `x ≈ y` is the distinguished equivalence relation of a setoid. -/
  r : α → α → Prop
  /-- The relation `x ≈ y` is an equivalence relation. -/
  iseqv : Equivalence r

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

/-- A setoid's equivalence relation is reflexive. -/
theorem refl (a : α) : a ≈ a :=
  iseqv.refl a

/-- A setoid's equivalence relation is symmetric. -/
theorem symm {a b : α} (hab : a ≈ b) : b ≈ a :=
  iseqv.symm hab

/-- A setoid's equivalence relation is transitive. -/
theorem trans {a b c : α} (hab : a ≈ b) (hbc : b ≈ c) : a ≈ c :=
  iseqv.trans hab hbc

/--
The axiom of **propositional extensionality**. It asserts that if propositions
`a` and `b` are logically equivalent (i.e. we can prove `a` from `b` and vice versa),
then `a` and `b` are *equal*, meaning that we can replace `a` with `b` in all
contexts.

For simple expressions like `a ∧ c ∨ d → e` we can prove that because all the logical
connectives respect logical equivalence, we can replace `a` with `b` in this expression
without using `propext`. However, for higher order expressions like `P a` where
`P : Prop → Prop` is unknown, or indeed for `a = b` itself, we cannot replace `a` with `b`
without an axiom which says exactly this.

This is a relatively uncontroversial axiom, which is intuitionistically valid.
It does however block computation when using `#reduce` to reduce proofs directly
(which is not recommended), meaning that canonicity,
the property that all closed terms of type `Nat` normalize to numerals,
fails to hold when this (or any) axiom is used:
```
set_option pp.proofs true

def foo : Nat := by
  have : (True → True) ↔ True := ⟨λ _ => trivial, λ _ _ => trivial⟩
  have := propext this ▸ (2 : Nat)
  exact this

#reduce foo
-- propext { mp := fun x x => True.intro, mpr := fun x => True.intro } ▸ 2

#eval foo -- 2
```
`#eval` can evaluate it to a numeral because the compiler erases casts and
does not evaluate proofs, so `propext`, whose return type is a proposition,
can never block it.
-/
axiom propext {a b : Prop} : (a ↔ b) → a = b

theorem Eq.propIntro {a b : Prop} (h₁ : a → b) (h₂ : b → a) : a = b :=
  propext <| Iff.intro h₁ h₂

instance {p q : Prop} [d : Decidable (p ↔ q)] : Decidable (p = q) :=
  match d with
  | isTrue h => isTrue (propext h)
  | isFalse h => isFalse fun heq => h (heq ▸ Iff.rfl)

theorem Nat.succ.inj {m n : Nat} : m.succ = n.succ → m = n :=
  fun x => Nat.noConfusion x id

theorem Nat.succ.injEq (u v : Nat) : (u.succ = v.succ) = (u = v) :=
  Eq.propIntro Nat.succ.inj (congrArg Nat.succ)

@[simp] theorem beq_iff_eq [BEq α] [LawfulBEq α] {a b : α} : a == b ↔ a = b :=
  ⟨eq_of_beq, by intro h; subst h; exact LawfulBEq.rfl⟩

/-- *Ex falso* for negation: from `¬a` and `a` anything follows. This is the same as `absurd` with
the arguments flipped, but it is in the `Not` namespace so that projection notation can be used. -/
def Not.elim {α : Sort _} (H1 : ¬a) (H2 : a) : α := absurd H2 H1

/-- Non-dependent eliminator for `And`. -/
abbrev And.elim (f : a → b → α) (h : a ∧ b) : α := f h.left h.right

/-- Non-dependent eliminator for `Iff`. -/
def Iff.elim (f : (a → b) → (b → a) → α) (h : a ↔ b) : α := f h.mp h.mpr

/-- Iff can now be used to do substitutions in a calculation -/
theorem Iff.subst {a b : Prop} {p : Prop → Prop} (h₁ : a ↔ b) (h₂ : p a) : p b :=
  Eq.subst (propext h₁) h₂

theorem Not.intro {a : Prop} (h : a → False) : ¬a := h

theorem Not.imp {a b : Prop} (H2 : ¬b) (H1 : a → b) : ¬a := mt H1 H2

theorem not_congr (h : a ↔ b) : ¬a¬a ↔ ¬b := ⟨mt h.2, mt h.1⟩

theorem not_not_not : ¬¬¬a¬¬¬a ↔ ¬a := ⟨mt not_not_intro, not_not_intro⟩

theorem iff_of_true (ha : a) (hb : b) : a ↔ b := Iff.intro (fun _ => hb) (fun _ => ha)

theorem iff_of_false (ha : ¬a) (hb : ¬b) : a ↔ b := Iff.intro ha.elim hb.elim

theorem iff_true_left  (ha : a) : (a ↔ b) ↔ b := Iff.intro (·.mp ha) (iff_of_true ha)

theorem iff_true_right (ha : a) : (b ↔ a) ↔ b := Iff.comm.trans (iff_true_left ha)

theorem iff_false_left  (ha : ¬a) : (a ↔ b) ↔ ¬b := Iff.intro (mt ·.mpr ha) (iff_of_false ha)

theorem iff_false_right (ha : ¬a) : (b ↔ a) ↔ ¬b := Iff.comm.trans (iff_false_left ha)

theorem of_iff_true    (h : a ↔ True) : a := h.mpr trivial

theorem iff_true_intro (h : a) : a ↔ True := iff_of_true h trivial

theorem not_of_iff_false : (p ↔ False) → ¬p := Iff.mp

theorem iff_false_intro (h : ¬a) : a ↔ False := iff_of_false h id

theorem not_iff_false_intro (h : a) : ¬a¬a ↔ False := iff_false_intro (not_not_intro h)

theorem not_true : (¬True) ↔ False := iff_false_intro (not_not_intro trivial)

theorem not_false_iff : (¬False) ↔ True := iff_true_intro not_false

theorem Eq.to_iff : a = b → (a ↔ b) := Iff.of_eq

theorem iff_of_eq : a = b → (a ↔ b) := Iff.of_eq

theorem neq_of_not_iff : ¬(a ↔ b) → a ≠ b := mt Iff.of_eq

theorem iff_iff_eq : (a ↔ b) ↔ a = b := Iff.intro propext Iff.of_eq

theorem ne_self_iff_false (a : α) : a ≠ aa ≠ a ↔ False := not_iff_false_intro rfl

theorem false_of_true_iff_false (h : TrueTrue ↔ False) : False := h.mp trivial

theorem false_of_true_eq_false  (h : True = False) : False := false_of_true_iff_false (Iff.of_eq h)

theorem true_eq_false_of_false : False → (True = False) := False.elim

theorem iff_def  : (a ↔ b) ↔ (a → b) ∧ (b → a) := iff_iff_implies_and_implies

theorem iff_def' : (a ↔ b) ↔ (b → a) ∧ (a → b) := Iff.trans iff_def And.comm

theorem true_iff_false : (True ↔ False) ↔ False := iff_false_intro (·.mp  True.intro)

theorem false_iff_true : (False ↔ True) ↔ False := iff_false_intro (·.mpr True.intro)

theorem iff_not_self : ¬(a ↔ ¬a) | H => let f h := H.1 h h; f (H.2 f)

theorem heq_self_iff_true (a : α) : HEqHEq a a ↔ True := iff_true_intro HEq.rfl

theorem not_not_of_not_imp : ¬(a → b) → ¬¬a := mt Not.elim

theorem not_of_not_imp {a : Prop} : ¬(a → b) → ¬b := mt fun h _ => h

@[simp] theorem imp_not_self : (a → ¬a) ↔ ¬a := Iff.intro (fun h ha => h ha ha) (fun h _ => h)

theorem imp_intro {α β : Prop} (h : α) : β → α := fun _ => h

theorem imp_imp_imp {a b c d : Prop} (h₀ : c → a) (h₁ : b → d) : (a → b) → (c → d) := (h₁ ∘ · ∘ h₀)

theorem imp_iff_right {a : Prop} (ha : a) : (a → b) ↔ b := Iff.intro (· ha) (fun a _ => a)

theorem imp_true_iff (α : Sort u) : (α → True) ↔ True := iff_true_intro (fun _ => trivial)

theorem false_imp_iff (a : Prop) : (False → a) ↔ True := iff_true_intro False.elim

theorem true_imp_iff {α : Prop} : (True → α) ↔ α := imp_iff_right True.intro

@[simp high] theorem imp_self : (a → a) ↔ True := iff_true_intro id

@[simp] theorem imp_false : (a → False) ↔ ¬a := Iff.rfl

theorem imp.swap : (a → b → c) ↔ (b → a → c) := Iff.intro flip flip

theorem imp_not_comm : (a → ¬b) ↔ (b → ¬a) := imp.swap

theorem imp_congr_left (h : a ↔ b) : (a → c) ↔ (b → c) := Iff.intro (· ∘ h.mpr) (· ∘ h.mp)

theorem imp_congr_right (h : a → (b ↔ c)) : (a → b) ↔ (a → c) :=
  Iff.intro (fun hab ha => (h ha).mp (hab ha)) (fun hcd ha => (h ha).mpr (hcd ha))

theorem imp_congr_ctx (h₁ : a ↔ c) (h₂ : c → (b ↔ d)) : (a → b) ↔ (c → d) :=
  Iff.trans (imp_congr_left h₁) (imp_congr_right h₂)

theorem imp_congr (h₁ : a ↔ c) (h₂ : b ↔ d) : (a → b) ↔ (c → d) := imp_congr_ctx h₁ fun _ => h₂

theorem imp_iff_not (hb : ¬b) : a → b ↔ ¬a := imp_congr_right fun _ => iff_false_intro hb

/--
The **quotient axiom**, which asserts the equality of elements related by the quotient's relation.

The relation `r` does not need to be an equivalence relation to use this axiom. When `r` is not an
equivalence relation, the quotient is with respect to the equivalence relation generated by `r`.

`Quot.sound` is part of the built-in primitive quotient type:
 * `Quot` is the built-in quotient type.
 * `Quot.mk` places elements of the underlying type `α` into the quotient.
 * `Quot.lift` allows the definition of functions from the quotient to some other type.
 * `Quot.ind` is used to write proofs about quotients by assuming that all elements are constructed
   with `Quot.mk`; it is analogous to the [recursor](lean-manual://section/recursors) for a
   structure.

[Quotient types](lean-manual://section/quotients) are described in more detail in the Lean Language
Reference.
-/
axiom sound : ∀ {α : Sort u} {r : α → α → Prop} {a b : α}, r a b → Quot.mk r a = Quot.mk r b

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} {motive : Quot r → Prop}
    (p : (a : α) → motive (Quot.mk r a))
    (a : α)
    : (ind p (Quot.mk r a) : motive (Quot.mk r a)) = p a :=
  rfl

/--
Lifts a function from an underlying type to a function on a quotient, requiring that it respects the
quotient's relation.

Given a relation `r : α → α → Prop` and a quotient's value `q : Quot r`, applying a `f : α → β`
requires a proof `c` that `f` respects `r`. In this case, `Quot.liftOn q f h : β` evaluates
to the result of applying `f` to the underlying value in `α` from `q`.

`Quot.liftOn` is a version of the built-in primitive `Quot.lift` with its parameters re-ordered.

[Quotient types](lean-manual://section/quotients) are described in more detail in the Lean Language
Reference.
-/
protected abbrev 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

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

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

/-- Auxiliary definition for `Quot.rec`. -/
@[reducible, macro_inline]
protected def indep (f : (a : α) → motive (Quot.mk r a)) (a : α) : PSigma motive :=
  ⟨Quot.mk r a, f a⟩

protected theorem indepCoherent
    (f : (a : α) → motive (Quot.mk r a))
    (h : (a b : α) → (p : r a b) → Eq.ndrec (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 : α) → motive (Quot.mk r a))
    (h : ∀ (a b : α) (p : r a b), Eq.ndrec (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

/--
A dependent recursion principle for `Quot`. It is analogous to the
[recursor](lean-manual://section/recursors) for a structure, and can be used when the resulting type
is not necessarily a proposition.

While it is very general, this recursor can be tricky to use. The following simpler alternatives may
be easier to use:
 * `Quot.lift` is useful for defining non-dependent functions.
 * `Quot.ind` is useful for proving theorems about quotients.
 * `Quot.recOnSubsingleton` can be used whenever the target type is a `Subsingleton`.
 * `Quot.hrecOn` uses [heterogeneous equality](lean-manual://section/HEq) instead of rewriting with
   `Quot.sound`.

`Quot.recOn` is a version of this recursor that takes the quotient parameter first.
-/
@[elab_as_elim] protected abbrev rec
    (f : (a : α) → motive (Quot.mk r a))
    (h : (a b : α) → (p : r a b) → Eq.ndrec (f a) (sound p) = f b)
    (q : Quot r) : motive q :=
  Eq.ndrecOn (Quot.liftIndepPr1 f h q) ((lift (Quot.indep f) (Quot.indepCoherent f h) q).2)

/--
A dependent recursion principle for `Quot` that takes the quotient first. It is analogous to the
[recursor](lean-manual://section/recursors) for a structure, and can be used when the resulting type
is not necessarily a proposition.

While it is very general, this recursor can be tricky to use. The following simpler alternatives may
be easier to use:
 * `Quot.lift` is useful for defining non-dependent functions.
 * `Quot.ind` is useful for proving theorems about quotients.
 * `Quot.recOnSubsingleton` can be used whenever the target type is a `Subsingleton`.
 * `Quot.hrecOn` uses [heterogeneous equality](lean-manual://section/HEq) instead of rewriting with
   `Quot.sound`.

`Quot.rec` is a version of this recursor that takes the quotient parameter last.
-/
@[elab_as_elim] protected abbrev recOn
    (q : Quot r)
    (f : (a : α) → motive (Quot.mk r a))
    (h : (a b : α) → (p : r a b) → Eq.ndrec (f a) (sound p) = f b)
    : motive q :=
 q.rec f h

/--
An alternative induction principle for quotients that can be used when the target type is a
subsingleton, in which all elements are equal.

In these cases, the proof that the function respects the quotient's relation is trivial, so any
function can be lifted.

`Quot.rec` does not assume that the type is a subsingleton.
-/
@[elab_as_elim] protected abbrev recOnSubsingleton
    [h : (a : α) → Subsingleton (motive (Quot.mk r a))]
    (q : Quot r)
    (f : (a : α) → motive (Quot.mk r a))
    : motive q := by
  induction q using Quot.rec
  apply f
  apply Subsingleton.elim

/--
A dependent recursion principle for `Quot` that uses [heterogeneous
equality](lean-manual://section/HEq), analogous to a [recursor](lean-manual://section/recursors) for
a structure.

`Quot.recOn` is a version of this recursor that uses `Eq` instead of `HEq`.
-/
protected abbrev hrecOn
    (q : Quot r)
    (f : (a : α) → motive (Quot.mk r a))
    (c : (a b : α) → (p : r a b) → HEq (f a) (f b))
    : motive q :=
  Quot.recOn q f fun a b p => eq_of_heq <|
    have p₁ : HEq (Eq.ndrec (f a) (sound p)) (f a) := eqRec_heq (sound p) (f a)
    HEq.trans p₁ (c a b p)

/--
Quotient types coarsen the propositional equality for a type so that terms related by some
equivalence relation are considered equal. The equivalence relation is given by an instance of
`Setoid`.

Set-theoretically, `Quotient s` can seen as the set of equivalence classes of `α` modulo the
`Setoid` instance's relation `s.r`. Functions from `Quotient s` must prove that they respect `s.r`:
to define a function `f : Quotient s → β`, it is necessary to provide `f' : α → β` and prove that
for all `x : α` and `y : α`, `s.r x y → f' x = f' y`. `Quotient.lift` implements this operation.

The key quotient operators are:
 * `Quotient.mk` places elements of the underlying type `α` into the quotient.
 * `Quotient.lift` allows the definition of functions from the quotient to some other type.
 * `Quotient.sound` asserts the equality of elements related by `r`
 * `Quotient.ind` is used to write proofs about quotients by assuming that all elements are
   constructed with `Quotient.mk`.

`Quotient` is built on top of the primitive quotient type `Quot`, which does not require a proof
that the relation is an equivalence relation. `Quotient` should be used instead of `Quot` for
relations that actually are equivalence relations.
-/
def Quotient {α : Sort u} (s : Setoid α) :=
  @Quot α Setoid.r

/--
Places an element of a type into the quotient that equates terms according to an equivalence
relation.

The setoid instance is provided explicitly. `Quotient.mk'` uses instance synthesis instead.

Given `v : α`, `Quotient.mk s v : Quotient s` is like `v`, except all observations of `v`'s value
must respect `s.r`. `Quotient.lift` allows values in a quotient to be mapped to other types, so long
as the mapping respects `s.r`.
-/
@[inline]
protected def mk {α : Sort u} (s : Setoid α) (a : α) : Quotient s :=
  Quot.mk Setoid.r a

/--
Places an element of a type into the quotient that equates terms according to an equivalence
relation.

The equivalence relation is found by synthesizing a `Setoid` instance. `Quotient.mk` instead expects
the instance to be provided explicitly.

Given `v : α`, `Quotient.mk' v : Quotient s` is like `v`, except all observations of `v`'s value
must respect `s.r`. `Quotient.lift` allows values in a quotient to be mapped to other types, so long
as the mapping respects `s.r`.

-/
protected def mk' {α : Sort u} [s : Setoid α] (a : α) : Quotient s :=
  Quotient.mk s a

/--
The **quotient axiom**, which asserts the equality of elements related in the setoid.

Because `Quotient` is built on a lower-level type `Quot`, `Quotient.sound` is implemented as a
theorem. It is derived from `Quot.sound`, the soundness axiom for the lower-level quotient type
`Quot`.
-/
theorem sound {α : Sort u} {s : Setoid α} {a b : α} : a ≈ b → Quotient.mk s a = Quotient.mk s b :=
  Quot.sound

/--
Lifts a function from an underlying type to a function on a quotient, requiring that it respects the
quotient's equivalence relation.

Given `s : Setoid α` and a quotient `Quotient s`, applying a function `f : α → β` requires a proof
`h` that `f` respects the equivalence relation `s.r`. In this case, the function
`Quotient.lift f h : Quotient s → β` computes the same values as `f`.

`Quotient.liftOn` is a version of this operation that takes the quotient value as its first explicit
parameter.
-/
protected abbrev lift {α : Sort u} {β : Sort v} {s : Setoid α} (f : α → β) : ((a b : α) → a ≈ b → f a = f b) → Quotient s → β :=
  Quot.lift f

/--
A reasoning principle for quotients that allows proofs about quotients to assume that all values are
constructed with `Quotient.mk`.
-/
protected theorem ind {α : Sort u} {s : Setoid α} {motive : Quotient s → Prop} : ((a : α) → motive (Quotient.mk s a)) → (q : Quotient s) → motive q :=
  Quot.ind

/--
Lifts a function from an underlying type to a function on a quotient, requiring that it respects the
quotient's equivalence relation.

Given `s : Setoid α` and a quotient value `q : Quotient s`, applying a function `f : α → β` requires
a proof `c` that `f` respects the equivalence relation `s.r`. In this case, the term
`Quotient.liftOn q f h : β` reduces to the result of applying `f` to the underlying `α` value.

`Quotient.lift` is a version of this operation that takes the quotient value last, rather than
first.
-/
protected abbrev 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

/-- The analogue of `Quot.inductionOn`: every element of `Quotient s` is of the form `Quotient.mk s a`. -/
@[elab_as_elim]
protected theorem inductionOn {α : Sort u} {s : Setoid α} {motive : Quotient s → Prop}
    (q : Quotient s)
    (h : (a : α) → motive (Quotient.mk s a))
    : motive q :=
  Quot.inductionOn q h

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

/--
A dependent recursion principle for `Quotient`. It is analogous to the
[recursor](lean-manual://section/recursors) for a structure, and can be used when the resulting type
is not necessarily a proposition.

While it is very general, this recursor can be tricky to use. The following simpler alternatives may
be easier to use:

 * `Quotient.lift` is useful for defining non-dependent functions.
 * `Quotient.ind` is useful for proving theorems about quotients.
 * `Quotient.recOnSubsingleton` can be used whenever the target type is a `Subsingleton`.
 * `Quotient.hrecOn` uses heterogeneous equality instead of rewriting with `Quotient.sound`.

`Quotient.recOn` is a version of this recursor that takes the quotient parameter first.
-/
@[inline, elab_as_elim]
protected def rec
    (f : (a : α) → motive (Quotient.mk s a))
    (h : (a b : α) → (p : a ≈ b) → Eq.ndrec (f a) (Quotient.sound p) = f b)
    (q : Quotient s)
    : motive q :=
  Quot.rec f h q

/--
A dependent recursion principle for `Quotient`. It is analogous to the
[recursor](lean-manual://section/recursors) for a structure, and can be used when the resulting type
is not necessarily a proposition.

While it is very general, this recursor can be tricky to use. The following simpler alternatives may
be easier to use:

 * `Quotient.lift` is useful for defining non-dependent functions.
 * `Quotient.ind` is useful for proving theorems about quotients.
 * `Quotient.recOnSubsingleton` can be used whenever the target type is a `Subsingleton`.
 * `Quotient.hrecOn` uses heterogeneous equality instead of rewriting with `Quotient.sound`.

`Quotient.rec` is a version of this recursor that takes the quotient parameter last.
-/
@[elab_as_elim]
protected abbrev recOn
    (q : Quotient s)
    (f : (a : α) → motive (Quotient.mk s a))
    (h : (a b : α) → (p : a ≈ b) → Eq.ndrec (f a) (Quotient.sound p) = f b)
    : motive q :=
  Quot.recOn q f h

/--
An alternative recursion or induction principle for quotients that can be used when the target type
is a subsingleton, in which all elements are equal.

In these cases, the proof that the function respects the quotient's equivalence relation is trivial,
so any function can be lifted.

`Quotient.rec` does not assume that the target type is a subsingleton.
-/
@[elab_as_elim]
protected abbrev recOnSubsingleton
    [h : (a : α) → Subsingleton (motive (Quotient.mk s a))]
    (q : Quotient s)
    (f : (a : α) → motive (Quotient.mk s a))
    : motive q :=
  Quot.recOnSubsingleton (h := h) q f

/--
A dependent recursion principle for `Quotient` that uses [heterogeneous
equality](lean-manual://section/HEq), analogous to a [recursor](lean-manual://section/recursors) for
a structure.

`Quotient.recOn` is a version of this recursor that uses `Eq` instead of `HEq`.
-/
@[elab_as_elim]
protected abbrev hrecOn
    (q : Quotient s)
    (f : (a : α) → motive (Quotient.mk s a))
    (c : (a b : α) → (p : a ≈ b) → HEq (f a) (f b))
    : motive q :=
  Quot.hrecOn q f c

/--
Lifts a binary function from the underlying types to a binary function on quotients. The function
must respect both quotients' equivalence relations.

`Quotient.lift` is a version of this operation for unary functions. `Quotient.liftOn₂` is a version
that take the quotient parameters first.
-/
protected abbrev lift₂
    (f : α → β → φ)
    (c : (a₁ : α) → (b₁ : β) → (a₂ : α) → (b₂ : β) → a₁ ≈ a₂ → b₁ ≈ b₂ → f a₁ b₁ = f a₂ b₂)
    (q₁ : Quotient s₁) (q₂ : Quotient s₂)
    : φ := by
  apply Quotient.lift (fun (a₁ : α) => Quotient.lift (f a₁) (fun (a b : β) => c a₁ a a₁ b (Setoid.refl a₁)) q₂) _ q₁
  intros
  induction q₂ using Quotient.ind
  apply c; assumption; apply Setoid.refl