text:
/-
Copyright (c) 2017 Mario Carneiro. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Mario Carneiro
-/
import data.dlist
import tactic.core
import tactic.clear

/-!

# Recursive cases (`rcases`) tactic and related tactics

`rcases` is a tactic that will perform `cases` recursively, according to a pattern. It is used to
destructure hypotheses or expressions composed of inductive types like `h1 : a ∧ b ∧ c ∨ d` or
`h2 : ∃ x y, trans_rel R x y`. Usual usage might be `rcases h1 with ⟨ha, hb, hc⟩ | hd` or
`rcases h2 with ⟨x, y, _ | ⟨z, hxz, hzy⟩⟩` for these examples.

Each element of an `rcases` pattern is matched against a particular local hypothesis (most of which
are generated during the execution of `rcases` and represent individual elements destructured from
the input expression). An `rcases` pattern has the following grammar:

* A name like `x`, which names the active hypothesis as `x`.
* A blank `_`, which does nothing (letting the automatic naming system used by `cases` name the
  hypothesis).
* A hyphen `-`, which clears the active hypothesis and any dependents.
* The keyword `rfl`, which expects the hypothesis to be `h : a = b`, and calls `subst` on the
  hypothesis (which has the effect of replacing `b` with `a` everywhere or vice versa).
* A type ascription `p : ty`, which sets the type of the hypothesis to `ty` and then matches it
  against `p`. (Of course, `ty` must unify with the actual type of `h` for this to work.)
* A tuple pattern `⟨p1, p2, p3⟩`, which matches a constructor with many arguments, or a series
  of nested conjunctions or existentials. For example if the active hypothesis is `a ∧ b ∧ c`,
  then the conjunction will be destructured, and `p1` will be matched against `a`, `p2` against `b`
  and so on.
* A `@` before a tuple pattern as in `@⟨p1, p2, p3⟩` will bind all arguments in the constructor,
  while leaving the `@` off will only use the patterns on the explicit arguments.
* An alteration pattern `p1 | p2 | p3`, which matches an inductive type with multiple constructors,
  or a nested disjunction like `a ∨ b ∨ c`.

The patterns are fairly liberal about the exact shape of the constructors, and will insert
additional alternation branches and tuple arguments if there are not enough arguments provided, and
reuse the tail for further matches if there are too many arguments provided to alternation and
tuple patterns.

This file also contains the `obtain` and `rintro` tactics, which use the same syntax of `rcases`
patterns but with a slightly different use case:

* `rintro` (or `rintros`) is used like `rintro x ⟨y, z⟩` and is the same as `intros` followed by
  `rcases` on the newly introduced arguments.
* `obtain` is the same as `rcases` but with a syntax styled after `have` rather than `cases`.
  `obtain ⟨hx, hy⟩ | hz := foo` is equivalent to `rcases foo with ⟨hx, hy⟩ | hz`. Unlike `rcases`,
  `obtain` also allows one to omit `:= foo`, although a type must be provided in this case,
  as in `obtain ⟨hx, hy⟩ | hz : a ∧ b ∨ c`, in which case it produces a subgoal for proving
  `a ∧ b ∨ c` in addition to the subgoals `hx : a, hy : b |- goal` and `hz : c |- goal`.

## Tags

rcases, rintro, obtain, destructuring, cases, pattern matching, match
-/

open lean lean.parser

namespace tactic

/-!
These synonyms for `list` are used to clarify the meanings of the many
usages of lists in this module.

- `listΣ` is used where a list represents a disjunction, such as the
  list of possible constructors of an inductive type.

- `listΠ` is used where a list represents a conjunction, such as the
  list of arguments of an individual constructor.

These are merely type synonyms, and so are not checked for consistency
by the compiler.

The `def`/`local notation` combination makes Lean retain these
annotations in reported types.
-/

/-- A list, with a disjunctive meaning (like a list of inductive constructors, or subgoals) -/
@[reducible] def list_Sigma := list

/-- A list, with a conjunctive meaning (like a list of constructor arguments, or hypotheses) -/
@[reducible] def list_Pi := list

local notation `listΣ` := list_Sigma
local notation `listΠ` := list_Pi

/-- A metavariable representing a subgoal, together with a list of local constants to clear. -/
@[reducible] meta def uncleared_goal := list expr × expr

/--
An `rcases` pattern can be one of the following, in a nested combination:

* A name like `foo`
* The special keyword `rfl` (for pattern matching on equality using `subst`)
* A hyphen `-`, which clears the active hypothesis and any dependents.
* A type ascription like `pat : ty` (parentheses are optional)
* A tuple constructor like `⟨p1, p2, p3⟩`
* An alternation / variant pattern `p1 | p2 | p3`

Parentheses can be used for grouping; alternation is higher precedence than type ascription, so
`p1 | p2 | p3 : ty` means `(p1 | p2 | p3) : ty`.

N-ary alternations are treated as a group, so `p1 | p2 | p3` is not the same as `p1 | (p2 | p3)`,
and similarly for tuples. However, note that an n-ary alternation or tuple can match an n-ary
conjunction or disjunction, because if the number of patterns exceeds the number of constructors in
the type being destructed, the extra patterns will match on the last element, meaning that
`p1 | p2 | p3` will act like `p1 | (p2 | p3)` when matching `a1 ∨ a2 ∨ a3`. If matching against a
type with 3 constructors,  `p1 | (p2 | p3)` will act like `p1 | (p2 | p3) | _` instead.
-/
meta inductive rcases_patt : Type
| one : name → rcases_patt
| clear : rcases_patt
| explicit : rcases_patt → rcases_patt
| typed : rcases_patt → pexpr → rcases_patt
| tuple : listΠ rcases_patt → rcases_patt
| alts : listΣ rcases_patt → rcases_patt

namespace rcases_patt
meta instance inhabited : inhabited rcases_patt :=
⟨one `_⟩

/-- Get the name from a pattern, if provided -/
meta def name : rcases_patt → option name
| (one `_) := none
| (one `rfl) := none
| (one n) := some n
| (explicit p) := p.name
| (typed p _) := p.name
| (alts [p]) := p.name
| _ := none

/-- Interpret an rcases pattern as a tuple, where `p` becomes `⟨p⟩`
if `p` is not already a tuple. -/
meta def as_tuple : rcases_patt → bool × listΠ rcases_patt
| (explicit p) := (tt, (as_tuple p).2)
| (tuple ps) := (ff, ps)
| p := (ff, [p])

/-- Interpret an rcases pattern as an alternation, where non-alternations are treated as one
alternative. -/
meta def as_alts : rcases_patt → listΣ rcases_patt
| (alts ps) := ps
| p := [p]

/-- Convert a list of patterns to a tuple pattern, but mapping `[p]` to `p` instead of `⟨p⟩`. -/
meta def tuple' : listΠ rcases_patt → rcases_patt
| [p] := p
| ps := tuple ps

/-- Convert a list of patterns to an alternation pattern, but mapping `[p]` to `p` instead of
a unary alternation `|p`. -/
meta def alts' : listΣ rcases_patt → rcases_patt
| [p] := p
| ps := alts ps

/-- This function is used for producing rcases patterns based on a case tree. Suppose that we have
a list of patterns `ps` that will match correctly against the branches of the case tree for one
constructor. This function will merge tuples at the end of the list, so that `[a, b, ⟨c, d⟩]`
becomes `⟨a, b, c, d⟩` instead of `⟨a, b, ⟨c, d⟩⟩`.

We must be careful to turn `[a, ⟨⟩]` into `⟨a, ⟨⟩⟩` instead of `⟨a⟩` (which will not perform the
nested match). -/
meta def tuple₁_core : listΠ rcases_patt → listΠ rcases_patt
| [] := []
| [tuple []] := [tuple []]
| [tuple ps] := ps
| (p :: ps) := p :: tuple₁_core ps

/-- This function is used for producing rcases patterns based on a case tree. This is like
`tuple₁_core` but it produces a pattern instead of a tuple pattern list, converting `[n]` to `n`
instead of `⟨n⟩` and `[]` to `_`, and otherwise just converting `[a, b, c]` to `⟨a, b, c⟩`. -/
meta def tuple₁ : listΠ rcases_patt → rcases_patt
| [] := default
| [one n] := one n
| ps := tuple (tuple₁_core ps)

/-- This function is used for producing rcases patterns based on a case tree. Here we are given
the list of patterns to apply to each argument of each constructor after the main case, and must
produce a list of alternatives with the same effect. This function calls `tuple₁` to make the
individual alternatives, and handles merging `[a, b, c | d]` to `a | b | c | d` instead of
`a | b | (c | d)`. -/
meta def alts₁_core : listΣ (listΠ rcases_patt) → listΣ rcases_patt
| [] := []
| [[alts ps]] := ps
| (p :: ps) := tuple₁ p :: alts₁_core ps

/-- This function is used for producing rcases patterns based on a case tree. This is like
`alts₁_core`, but it produces a cases pattern directly instead of a list of alternatives. We
specially translate the empty alternation to `⟨⟩`, and translate `|(a | b)` to `⟨a | b⟩` (because we
don't have any syntax for unary alternation). Otherwise we can use the regular merging of
alternations at the last argument so that `a | b | (c | d)` becomes `a | b | c | d`. -/
meta def alts₁ : listΣ (listΠ rcases_patt) → rcases_patt
| [[]] := tuple []
| [[alts ps]] := tuple [alts ps]
| ps := alts' (alts₁_core ps)

meta instance has_reflect : has_reflect rcases_patt
| (one n) := `(_)
| clear := `(_)
| (explicit l) := `(explicit).subst (has_reflect l)
| (typed l e) :=
  (`(typed).subst (has_reflect l)).subst (reflect e)
| (tuple l) := `(λ l, tuple l).subst $
  by haveI := has_reflect; exact list.reflect l
| (alts l) := `(λ l, alts l).subst $
  by haveI := has_reflect; exact list.reflect l

/-- Formats an `rcases` pattern. If the `bracket` argument is true, then it will be
printed at high precedence, i.e. it will have parentheses around it if it is not already a tuple
or atomic name. -/
protected meta def format : ∀ bracket : bool, rcases_patt → tactic _root_.format
| _ (one n) := pure $ to_fmt n
| _ clear := pure "-"
| _ (explicit p) := do f ← format tt p, pure $ "@" ++ f
| _ (tuple []) := pure "⟨⟩"
| _ (tuple ls) := do
  fs ← ls.mmap $ format ff,
  pure $ "⟨" ++ _root_.format.group (_root_.format.nest 1 $
    _root_.format.join $ list.intersperse ("," ++ _root_.format.line) fs) ++ "⟩"
| br (alts ls) := do
  fs ← ls.mmap $ format tt,
  let fmt := _root_.format.join $ list.intersperse (↑" |" ++ _root_.format.space) fs,
  pure $ if br then _root_.format.bracket "(" ")" fmt else fmt
| br (typed p e) := do
  fp ← format ff p,
  fe ← pp e,
  let fmt := fp ++ " : " ++ fe,
  pure $ if br then _root_.format.bracket "(" ")" fmt else fmt

meta instance has_to_tactic_format : has_to_tactic_format rcases_patt := ⟨rcases_patt.format ff⟩

end rcases_patt

/-- Takes the number of fields of a single constructor and patterns to match its fields against
(not necessarily the same number). The returned lists each contain one element per field of the
constructor. The `name` is the name which will be used in the top-level `cases` tactic, and the
`rcases_patt` is the pattern which the field will be matched against by subsequent `cases`
tactics. -/
meta def rcases.process_constructor :
  bool → list binder_info → listΠ rcases_patt → listΠ name × listΠ rcases_patt
| _        []      ps := ([], [])
| explicit (bi::l) ps :=
  if !explicit && (bi ≠ binder_info.default) then
    let (ns, tl) := rcases.process_constructor explicit l ps in
    (`_ :: ns, default :: tl)
  else
    match l, ps with
    | [], []  := ([`_], [default])
    | [], [p] := ([p.name.get_or_else `_], [p])
    -- The interesting case: we matched the last field against multiple
    -- patterns, so split off the remaining patterns into a subsequent
    -- match. This handles matching `α × β × γ` against `⟨a, b, c⟩`.
    | [],   ps  :=
      ([`_], [cond explicit (rcases_patt.tuple ps).explicit (rcases_patt.tuple ps)])
    | l, ps  :=
      let hd := ps.head, (ns, tl) := rcases.process_constructor explicit l ps.tail in
      (hd.name.get_or_else `_ :: ns, hd :: tl)
    end

private meta def get_pi_arity_list_aux : expr → tactic (list binder_info)
| (expr.pi n bi d b) :=
  do m     ← mk_fresh_name,
     let l := expr.local_const m n bi d,
     new_b ← whnf (expr.instantiate_var b l),
     r     ← get_pi_arity_list_aux new_b,
     return (bi :: r)
| e                  := return []

/-- Compute the arity of the given (Pi-)type -/
meta def get_pi_arity_list (type : expr) : tactic (list binder_info) :=
whnf type >>= get_pi_arity_list_aux

/-- Compute the arity of the given function -/
meta def get_arity_list (fn : expr) : tactic (list binder_info) :=
infer_type fn >>= get_pi_arity_list

/-- Takes a list of constructor names, and an (alternation) list of patterns, and matches each
pattern against its constructor. It returns the list of names that will be passed to `cases`,
and the list of `(constructor name, patterns)` for each constructor, where `patterns` is the
(conjunctive) list of patterns to apply to each constructor argument. -/
meta def rcases.process_constructors (params : nat) :
  listΣ name → listΣ rcases_patt →
  tactic (dlist name × listΣ (name × listΠ rcases_patt))
| []      ps := pure (dlist.empty, [])
| (c::cs) ps := do
  l ← mk_const c >>= get_arity_list,
  let ((explicit, h), t) := (match cs, ps.tail with
  -- We matched the last constructor against multiple patterns,
  -- so split off the remaining constructors. This handles matching
  -- `α ⊕ β ⊕ γ` against `a|b|c`.
  | [], _::_ := ((ff, [rcases_patt.alts ps]), [])
  | _, _ := (ps.head.as_tuple, ps.tail)
  end : _),
  let (ns, ps) := rcases.process_constructor explicit (l.drop params) h,
  (l, r) ← rcases.process_constructors cs t,
  pure (dlist.of_list ns ++ l, (c, ps) :: r)

/-- Like `zip`, but only elements satisfying a matching predicate `p` will go in the list,
and elements of the first list that fail to match the second list will be skipped. -/
private def align {α β} (p : α → β → Prop) [∀ a b, decidable (p a b)] :
  list α → list β → list (α × β)
| (a::as) (b::bs) :=
  if p a b then (a, b) :: align as bs else align as (b::bs)
| _ _ := []

/-- Given a local constant `e`, get its type. *But* if `e` does not exist, go find a hypothesis
with the same pretty name as `e` and get it instead. This is needed because we can sometimes lose
track of the unique names of hypotheses when they are revert/intro'd by `change` and `cases`. (A
better solution would be for these tactics to return a map of renamed hypotheses so that we don't
lose track of them.) -/
private meta def get_local_and_type (e : expr) : tactic (expr × expr) :=
(do t ← infer_type e, pure (t, e)) <|> (do
    e ← get_local e.local_pp_name,
    t ← infer_type e, pure (t, e))

/--
* `rcases_core p e` will match a pattern `p` against a local hypothesis `e`.
  It returns the list of subgoals that were produced.
* `rcases.continue pes` will match a (conjunctive) list of `(p, e)` pairs which refer to
  patterns and local hypotheses to match against, and applies all of them. Note that this can
  involve matching later arguments multiple times given earlier arguments, for example
  `⟨a | b, ⟨c, d⟩⟩` performs the `⟨c, d⟩` match twice, once on the `a` branch and once on `b`.
-/
meta mutual def rcases_core, rcases.continue
with rcases_core : rcases_patt → expr → tactic (list uncleared_goal)
| (rcases_patt.one `rfl) e := do
  (t, e) ← get_local_and_type e,
  subst' e,
  list.map (prod.mk []) <$> get_goals
-- If the pattern is any other name, we already bound the name in the
-- top-level `cases` tactic, so there is no more work to do for it.
| (rcases_patt.one _) _ := list.map (prod.mk []) <$> get_goals
| rcases_patt.clear e := do
  m ← try_core (get_local_and_type e),
  list.map (prod.mk $ m.elim [] (λ ⟨_, e⟩, [e])) <$> get_goals
| (rcases_patt.typed p ty) e := do
  (t, e) ← get_local_and_type e,
  ty ← i_to_expr_no_subgoals ``(%%ty : Sort*),
  unify t ty,
  t ← instantiate_mvars t,
  ty ← instantiate_mvars ty,
  e ← if t =ₐ ty then pure e else
    change_core ty (some e) >> get_local e.local_pp_name,
  rcases_core p e
| (rcases_patt.alts [p]) e := rcases_core p e
| pat e := do
  (t, e) ← get_local_and_type e,
  t ← whnf t,
  env ← get_env,
  let I := t.get_app_fn.const_name,
  let pat := pat.as_alts,
  (ids, r, l) ← (if I ≠ `quot
  then do
    when (¬env.is_inductive I) $
      fail format!"rcases tactic failed: {e} : {I} is not an inductive datatype",
    let params := env.inductive_num_params I,
    let c := env.constructors_of I,
    (ids, r) ← rcases.process_constructors params c pat,
    l ← cases_core e ids.to_list,
    pure (ids, r, l)
  else do
    (ids, r) ← rcases.process_constructors 2 [`quot.mk] pat,
    [(_, d)] ← induction e ids.to_list `quot.induction_on |
      fail format!"quotient induction on {e} failed. Maybe goal is not in Prop?",
    -- the result from `induction` is missing the information that the original constructor was
    -- `quot.mk` so we fix this up:
    pure (ids, r, [(`quot.mk, d)])),
  gs ← get_goals,
  -- `cases_core` may not generate a new goal for every constructor,
  -- as some constructors may be impossible for type reasons. (See its
  -- documentation.) Match up the new goals with our remaining work
  -- by constructor name.
  let ls := align (λ (a : name × _) (b : _ × name × _), a.1 = b.2.1) r (gs.zip l),
  list.join <$> ls.mmap (λ⟨⟨_, ps⟩, g, _, hs, _⟩, set_goals [g] >> rcases.continue (ps.zip hs))

with rcases.continue : listΠ (rcases_patt × expr) → tactic (list uncleared_goal)
| [] := list.map (prod.mk []) <$> get_goals
| ((pat, e) :: pes) := do
  gs ← rcases_core pat e,
  list.join <$> gs.mmap (λ ⟨cs, g⟩, do
    set_goals [g],
    ugs ← rcases.continue pes,
    pure $ ugs.map $ λ ⟨cs', gs⟩, (cs ++ cs', gs))

/-- Given a list of `uncleared_goal`s, each of which is a goal metavariable and
a list of variables to clear, actually perform the clear and set the goals with the result. -/
meta def clear_goals (ugs : list uncleared_goal) : tactic unit := do
  gs ← ugs.mmap (λ ⟨cs, g⟩, do
    set_goals [g],
    cs ← cs.mfoldr (λ c cs,
      (do (_, c) ← get_local_and_type c, pure (c :: cs)) <|> pure cs) [],
    clear' tt cs,
    [g] ← get_goals,
    pure g),
  set_goals gs

/-- `rcases h e pat` performs case distinction on `e` using `pat` to
name the arising new variables and assumptions. If `h` is `some` name,
a new assumption `h : e = pat` will relate the expression `e` with the
current pattern. See the module comment for the syntax of `pat`. -/
meta def rcases (h : option name) (p : pexpr) (pat : rcases_patt) : tactic unit := do
  let p := match pat with
  | rcases_patt.typed _ ty := ``(%%p : %%ty)
  | _ := p
  end,
  e ← match h with
    | some h := do
      x ← get_unused_name $ pat.name.get_or_else `this,
      interactive.generalize h () (p, x),
      get_local x
    | none := i_to_expr p
    end,
  if e.is_local_constant then
    match pat.name with
    | some x := do
      n ← revert e,
      e ← intro x,
      intron (n - 1),
      focus1 (rcases_core pat e >>= clear_goals)
    | none := focus1 (rcases_core pat e >>= clear_goals)
    end
  else do
    x ← pat.name.elim mk_fresh_name pure,
    n ← revert_kdependencies e semireducible,
    tactic.generalize e x <|> (do
      t ← infer_type e,
      tactic.assertv x t e,
      get_local x >>= tactic.revert,
      pure ()),
    h ← tactic.intro1,
    focus1 (rcases_core pat h >>= clear_goals)

/-- `rcases_many es pats` performs case distinction on the `es` using `pat` to
name the arising new variables and assumptions.
See the module comment for the syntax of `pat`. -/
meta def rcases_many (ps : listΠ pexpr) (pat : rcases_patt) : tactic unit := do
  let (_, pats) := rcases.process_constructor ff (ps.map (λ _, default)) pat.as_tuple.2,
  pes ← (ps.zip pats).mmap (λ ⟨p, pat⟩, do
    let p := match pat with
    | rcases_patt.typed _ ty := ``(%%p : %%ty)
    | _ := p
    end,
    e ← i_to_expr p,
    if e.is_local_constant then
      match pat.name with
      | some x := do
        n ← revert e,
        e ← intro x,
        intron (n - 1),
        pure (pat, e)
      | none := pure (pat, e)
      end
    else do
      x ← pat.name.elim mk_fresh_name pure,
      n ← revert_kdependencies e semireducible,
      tactic.generalize e x <|> (do
        t ← infer_type e,
        tactic.assertv x t e,
        get_local x >>= tactic.revert,
        pure ()),
      prod.mk pat <$> tactic.intro1),
  focus1 (rcases.continue pes >>= clear_goals)

/-- `rintro pat₁ pat₂ ... patₙ` introduces `n` arguments, then pattern matches on the `patᵢ` using
the same syntax as `rcases`. -/
meta def rintro (ids : listΠ rcases_patt) : tactic unit :=
do l ← ids.mmap (λ id, do
    e ← intro $ id.name.get_or_else `_,
    pure (id, e)),
  focus1 (rcases.continue l >>= clear_goals)

/-- Like `zip_with`, but if the lists don't match in length, the excess elements will be put at the
end of the result. -/
def merge_list {α} (m : α → α → α) : list α → list α → list α
| [] l₂ := l₂
| l₁ [] := l₁
| (a :: l₁) (b :: l₂) := m a b :: merge_list l₁ l₂

/-- Merge two `rcases` patterns. This is used to underapproximate a case tree by an `rcases`
pattern. The two patterns come from cases in two branches, that due to the syntax of `rcases`
patterns are forced to overlap. The rule here is that we take only the case splits that are in
common between both branches. For example if one branch does `⟨a, b⟩` and the other does `c`,
then we return `c` because we don't know that a case on `c` would be safe to do. -/
meta def rcases_patt.merge : rcases_patt → rcases_patt → rcases_patt
| (rcases_patt.alts p₁) p₂ := rcases_patt.alts (merge_list rcases_patt.merge p₁ p₂.as_alts)
| p₁ (rcases_patt.alts p₂) := rcases_patt.alts (merge_list rcases_patt.merge p₁.as_alts p₂)
| (rcases_patt.explicit p₁) p₂ := rcases_patt.explicit (p₁.merge p₂)
| p₁ (rcases_patt.explicit p₂) := rcases_patt.explicit (p₁.merge p₂)
| (rcases_patt.tuple p₁) p₂ := rcases_patt.tuple (merge_list rcases_patt.merge p₁ p₂.as_tuple.2)
| p₁ (rcases_patt.tuple p₂) := rcases_patt.tuple (merge_list rcases_patt.merge p₁.as_tuple.2 p₂)
| (rcases_patt.typed p₁ e) p₂ := rcases_patt.typed (p₁.merge p₂) e
| p₁ (rcases_patt.typed p₂ e) := rcases_patt.typed (p₁.merge p₂) e
| (rcases_patt.one `rfl) (rcases_patt.one `rfl) := rcases_patt.one `rfl
| (rcases_patt.one `_) p := p
| p (rcases_patt.one `_) := p
| rcases_patt.clear p := p
| p rcases_patt.clear := p
| (rcases_patt.one n) _ := rcases_patt.one n

/--
* `rcases_hint_core depth e` does the same as `rcases p e`, except the pattern `p` is an output
  instead of an input, controlled only by the case depth argument `depth`. We use `cases` to depth
  `depth` and then reconstruct an `rcases` pattern `p` that would, if passed to `rcases`, perform
  the same thing as the case tree we just constructed (or at least, the nearest expressible
  approximation to this.)
* `rcases_hint.process_constructors depth cs l` takes a list of constructor names `cs` and a
  matching list `l` of elements `(g, c', hs, _)` where  `c'` is a constructor name (used for
  alignment with `cs`), `g` is the subgoal, and `hs` is the list of local hypotheses created by
  `cases` in that subgoal. It matches on all of them, and then produces a `ΣΠ`-list of `rcases`
  patterns describing the result, and the list of generated subgoals.
* `rcases_hint.continue depth es` does the same as `rcases.continue (ps.zip es)`, except the
  patterns `ps` are an output instead of an input, created by matching on everything to depth
  `depth` and recording the successful cases. It returns `ps`, and the list of generated subgoals.
-/
meta mutual def rcases_hint_core, rcases_hint.process_constructors, rcases_hint.continue
  (explicit : bool)
with rcases_hint_core : bool → ℕ → expr → tactic (option rcases_patt × list expr)
| force depth e := do
  (t, e) ← get_local_and_type e,
  tt ← pure (explicit || force || (e.local_binding_info = binder_info.default)) |
    prod.mk none <$> get_goals,
  t ← whnf t,
  env ← get_env,
  let I := t.get_app_fn.const_name,
  (do guard (I = ``eq),
    subst' e,
    prod.mk (some (rcases_patt.one `rfl)) <$> get_goals) <|>
  (do
    let c := env.constructors_of I,
    some l ← try_core (guard (depth ≠ 0) >> cases_core e) |
      let n := match e.local_pp_name with name.anonymous := `_ | n := n end in
      prod.mk (some (rcases_patt.one n)) <$> get_goals,
    gs ← get_goals,
    if gs.empty then
      pure (some (rcases_patt.tuple []), [])
    else do
      (ps, gs') ← rcases_hint.process_constructors (depth - 1) c (gs.zip l),
      pure (some (rcases_patt.alts₁ ps), gs'))

with rcases_hint.process_constructors : ℕ → listΣ name →
  list (expr × name × listΠ expr × list (name × expr)) →
  tactic (listΣ (listΠ rcases_patt) × list expr)
| depth [] _  := pure ([], [])
| depth cs [] := pure (cs.map (λ _, []), [])
| depth (c::cs) ls@((g, c', hs, _) :: l) :=
  if c ≠ c' then do
    (ps, gs) ← rcases_hint.process_constructors depth cs ls,
    pure ([] :: ps, gs)
  else do
    (p, gs) ← set_goals [g] >> rcases_hint.continue depth hs,
    (ps, gs') ← rcases_hint.process_constructors depth cs l,
    pure (p :: ps, gs ++ gs')

with rcases_hint.continue : ℕ → listΠ expr → tactic (listΠ rcases_patt × list expr)
| depth [] := prod.mk [] <$> get_goals
| depth (e :: es) := do
  (p, gs) ← rcases_hint_core ff depth e,
  (ps, gs') ← gs.mfoldl (λ (r : listΠ rcases_patt × list expr) g,
    do (ps, gs') ← set_goals [g] >> rcases_hint.continue depth es,
      pure (merge_list rcases_patt.merge r.1 ps, r.2 ++ gs')) ([], []),
  pure (match p with none := ps | some p := p :: ps end, gs')

/--
* `rcases? e` is like `rcases e with ...`, except it generates `...` by matching on everything it
can, and it outputs an `rcases` invocation that should have the same effect.
* `rcases? e : n` can be used to control the depth of case splits (especially important for
recursive types like `nat`, which can be cased as many times as you like). -/
meta def rcases_hint (p : pexpr) (depth : nat) : tactic rcases_patt :=
do e ← i_to_expr p,
  if e.is_local_constant then
    focus1 $ do
      (p, gs) ← rcases_hint_core ff tt depth e,
      set_goals gs,
      pure (p.get_or_else default)
  else do
    x ← mk_fresh_name,
    n ← revert_kdependencies e semireducible,
    tactic.generalize e x <|> (do
      t ← infer_type e,
      tactic.assertv x t e,
      get_local x >>= tactic.revert,
      pure ()),
    h ← tactic.intro1,
    focus1 $ do
      (p, gs) ← rcases_hint_core ff tt depth h,
      set_goals gs,
      pure (p.get_or_else default)

/--
* `rcases? ⟨e1, e2, e3⟩` is like `rcases ⟨e1, e2, e3⟩ with ...`, except it
  generates `...` by matching on everything it can, and it outputs an `rcases`
  invocation that should have the same effect.
* `rcases? ⟨e1, e2, e3⟩ : n` can be used to control the depth of case splits
  (especially important for recursive types like `nat`, which can be cased as many
  times as you like). -/
meta def rcases_hint_many (ps : list pexpr) (depth : nat) : tactic (listΠ rcases_patt) :=
do es ← ps.mmap (λ p, do
    e ← i_to_expr p,
    if e.is_local_constant then pure e
    else do
      x ← mk_fresh_name,
      n ← revert_kdependencies e semireducible,
      tactic.generalize e x <|> (do
        t ← infer_type e,
        tactic.assertv x t e,
        get_local x >>= tactic.revert,
        pure ()),
      tactic.intro1),
  focus1 $ do
    (ps, gs) ← rcases_hint.continue ff depth es,
    set_goals gs,
    pure ps

/--
* `rintro?` is like `rintro ...`, except it generates `...` by introducing and matching on
everything it can, and it outputs an `rintro` invocation that should have the same effect.
* `rintro? : n` can be used to control the depth of case splits (especially important for
recursive types like `nat`, which can be cased as many times as you like). -/
meta def rintro_hint (depth : nat) : tactic (listΠ rcases_patt) :=
do l ← intros,
  focus1 $ do
    (p, gs) ← rcases_hint.continue ff depth l,
    set_goals gs,
    pure p

setup_tactic_parser

/--
* `rcases_patt_parse_hi` will parse a high precedence `rcases` pattern, `patt_hi`.
  This means only tuples and identifiers are allowed; alternations and type ascriptions
  require `(...)` instead, which switches to `patt`.
* `rcases_patt_parse` will parse a low precedence `rcases` pattern, `patt`. This consists of a
  `patt_med` (which deals with alternations), optionally followed by a `: ty` type ascription. The
  expression `ty` is at `texpr` precedence because it can appear at the end of a tactic, for
  example in `rcases e with x : ty <|> skip`.
* `rcases_patt_parse_list` will parse an alternation list, `patt_med`, one or more `patt`
  patterns separated by `|`. It does not parse a `:` at the end, so that `a | b : ty` parses as
  `(a | b) : ty` where `a | b` is the `patt_med` part.
* `rcases_patt_parse_list_rest a` parses an alternation list after the initial pattern, `| b | c`.

```lean
patt ::= patt_med (":" expr)?
patt_med ::= (patt_hi "|")* patt_hi
patt_hi ::= id | "rfl" | "_" | "@" patt_hi | "⟨" (patt ",")* patt "⟩" | "(" patt ")"
```
-/
meta mutual def
  rcases_patt_parse_hi', rcases_patt_parse', rcases_patt_parse_list', rcases_patt_parse_list_rest
with rcases_patt_parse_hi' : parser rcases_patt
| x := ((brackets "(" ")" rcases_patt_parse') <|>
  (rcases_patt.tuple <$> brackets "⟨" "⟩" (sep_by (tk ",") rcases_patt_parse')) <|>
  (tk "-" $> rcases_patt.clear) <|>
  (tk "@" *> rcases_patt.explicit <$> rcases_patt_parse_hi') <|>
  (rcases_patt.one <$> ident_)) x

with rcases_patt_parse' : parser rcases_patt
| x := (do
  pat ← rcases_patt.alts' <$> rcases_patt_parse_list',
  (tk ":" *> pat.typed <$> texpr) <|> pure pat) x

with rcases_patt_parse_list' : parser (listΣ rcases_patt)
| x := (rcases_patt_parse_hi' >>= rcases_patt_parse_list_rest) x

with rcases_patt_parse_list_rest : rcases_patt → parser (listΣ rcases_patt)
| pat :=
  (tk "|" *> list.cons pat <$> rcases_patt_parse_list') <|>
  -- hack to support `-|-` patterns, because `|-` is a token
  (tk "|-" *> list.cons pat <$> rcases_patt_parse_list_rest rcases_patt.clear) <|>
  pure [pat]

/-- `rcases_patt_parse_hi` will parse a high precedence `rcases` pattern, `patt_hi`.
This means only tuples and identifiers are allowed; alternations and type ascriptions
require `(...)` instead, which switches to `patt`.
```lean
patt_hi ::= id | "rfl" | "_" | "@" patt_hi | "⟨" (patt ",")* patt "⟩" | "(" patt ")"
```
-/
meta def rcases_patt_parse_hi := with_desc "patt_hi" rcases_patt_parse_hi'

/-- `rcases_patt_parse` will parse a low precedence `rcases` pattern, `patt`. This consists of a
`patt_med` (which deals with alternations), optionally followed by a `: ty` type ascription. The
expression `ty` is at `texpr` precedence because it can appear at the end of a tactic, for
example in `rcases e with x : ty <|> skip`.
```lean
patt ::= patt_med (":" expr)?
```
-/
meta def rcases_patt_parse := with_desc "patt" rcases_patt_parse'

/-- `rcases_patt_parse_list` will parse an alternation list, `patt_med`, one or more `patt`
patterns separated by `|`. It does not parse a `:` at the end, so that `a | b : ty` parses as
`(a | b) : ty` where `a | b` is the `patt_med` part.
```lean
patt_med ::= (patt_hi "|")* patt_hi
```
-/
meta def rcases_patt_parse_list := with_desc "patt_med" rcases_patt_parse_list'

/-- Parse the optional depth argument `(: n)?` of `rcases?` and `rintro?`, with default depth 5. -/
meta def rcases_parse_depth : parser nat :=
do o ← (tk ":" *> small_nat)?, pure $ o.get_or_else 5

/-- The arguments to `rcases`, which in fact dispatch to several other tactics.
* `rcases? expr (: n)?` or `rcases? ⟨expr, ...⟩ (: n)?` calls `rcases_hint`
* `rcases? ⟨expr, ...⟩ (: n)?` calls `rcases_hint_many`
* `rcases (h :)? expr (with patt)?` calls `rcases`
* `rcases ⟨expr, ...⟩ (with patt)?` calls `rcases_many`
-/
@[derive has_reflect]
meta inductive rcases_args
| hint (tgt : pexpr ⊕ list pexpr) (depth : nat)
| rcases (name : option name) (tgt : pexpr) (pat : rcases_patt)
| rcases_many (tgt : listΠ pexpr) (pat : rcases_patt)

/-- Syntax for a `rcases` pattern:
* `rcases? expr (: n)?`
* `rcases (h :)? expr (with patt_list (: expr)?)?`. -/
meta def rcases_parse : parser rcases_args :=
with_desc "('?' expr (: n)?) | ((h :)? expr (with patt)?)" $ do
  hint ← (tk "?")?,
  p ← (sum.inr <$> brackets "⟨" "⟩" (sep_by (tk ",") (parser.pexpr 0))) <|>
      (sum.inl <$> texpr),
  match hint with
  | none := do
    p ← (do
      sum.inl (expr.local_const h _ _ _) ← pure p,
      tk ":" *> (@sum.inl _ (pexpr ⊕ list pexpr) ∘ prod.mk h) <$> texpr) <|>
      pure (sum.inr p),
    ids ← (tk "with" *> rcases_patt_parse)?,
    let ids := ids.get_or_else (rcases_patt.tuple []),
    pure $ match p with
    | sum.inl (name, tgt) := rcases_args.rcases (some name) tgt ids
    | sum.inr (sum.inl tgt) := rcases_args.rcases none tgt ids
    | sum.inr (sum.inr tgts) := rcases_args.rcases_many tgts ids
    end
  | some _ := do
    depth ← rcases_parse_depth,
    pure $ rcases_args.hint p depth
  end

/--
`rintro_patt_parse_hi` and `rintro_patt_parse` are like `rcases_patt_parse`, but is used for
parsing top level `rintro` patterns, which allow sequences like `(x y : t)` in addition to simple
`rcases` patterns.

* `rintro_patt_parse_hi` will parse a high precedence `rcases` pattern, `rintro_patt_hi` below.
  This means only tuples and identifiers are allowed; alternations and type ascriptions
  require `(...)` instead, which switches to `patt`.
* `rintro_patt_parse` will parse a low precedence `rcases` pattern, `rintro_patt` below.
  This consists of either a sequence of patterns `p1 p2 p3` or an alternation list `p1 | p2 | p3`
  treated as a single pattern, optionally followed by a `: ty` type ascription, which applies to
  every pattern in the list.
* `rintro_patt_parse_low` parses `rintro_patt_low`, which is the same as `rintro_patt_parse tt` but
  it does not permit an unparenthesized alternation list, it must have the form `p1 p2 p3 (: ty)?`.

```lean
rintro_patt ::= (rintro_patt_hi+ | patt_med) (":" expr)?
rintro_patt_low ::= rintro_patt_hi* (":" expr)?
rintro_patt_hi ::= patt_hi | "(" rintro_patt ")"
```
-/
meta mutual def rintro_patt_parse_hi', rintro_patt_parse'
with rintro_patt_parse_hi' : parser (listΠ rcases_patt)
| x := (brackets "(" ")" (rintro_patt_parse' tt) <|>
  (do p ← rcases_patt_parse_hi, pure [p])) x
with rintro_patt_parse' : bool → parser (listΠ rcases_patt)
| med := do
  ll ← rintro_patt_parse_hi'*,
  pats ← match med, ll.join with
  | tt, [] := failure
  | tt, [pat] := do l ← rcases_patt_parse_list_rest pat, pure [rcases_patt.alts' l]
  | _, pats := pure pats
  end,
  (do tk ":", e ← texpr, pure (pats.map (λ p, rcases_patt.typed p e))) <|>
  pure pats

/--
`rintro_patt_parse_hi` will parse a high precedence `rcases` pattern, `rintro_patt_hi` below.
This means only tuples and identifiers are allowed; alternations and type ascriptions
require `(...)` instead, which switches to `patt`.
```lean
rintro_patt_hi ::= patt_hi | "(" rintro_patt ")"
```
-/
meta def rintro_patt_parse_hi := with_desc "rintro_patt_hi" rintro_patt_parse_hi'

/--
`rintro_patt_parse` will parse a low precedence `rcases` pattern, `rintro_patt` below.
This consists of either a sequence of patterns `p1 p2 p3` or an alternation list `p1 | p2 | p3`
treated as a single pattern, optionally followed by a `: ty` type ascription, which applies to
every pattern in the list.
```lean
rintro_patt ::= (rintro_patt_hi+ | patt_med) (":" expr)?
```
-/
meta def rintro_patt_parse := with_desc "rintro_patt" $ rintro_patt_parse' tt

/--
`rintro_patt_parse_low` parses `rintro_patt_low`, which is the same as `rintro_patt_parse tt` but
it does not permit an unparenthesized alternation list, it must have the form `p1 p2 p3 (: ty)?`.
```lean
rintro_patt_low ::= rintro_patt_hi* (":" expr)?
```
-/
meta def rintro_patt_parse_low := with_desc "rintro_patt_low" $ rintro_patt_parse' ff

/-- Syntax for a `rintro` pattern: `('?' (: n)?) | rintro_patt`. -/
meta def rintro_parse : parser (listΠ rcases_patt ⊕ nat) :=
with_desc "('?' (: n)?) | patt*" $
(tk "?" >> sum.inr <$> rcases_parse_depth) <|>
sum.inl <$> rintro_patt_parse_low

namespace interactive
open interactive interactive.types expr

/--
`rcases` is a tactic that will perform `cases` recursively, according to a pattern. It is used to
destructure hypotheses or expressions composed of inductive types like `h1 : a ∧ b ∧ c ∨ d` or
`h2 : ∃ x y, trans_rel R x y`. Usual usage might be `rcases h1 with ⟨ha, hb, hc⟩ | hd` or
`rcases h2 with ⟨x, y, _ | ⟨z, hxz, hzy⟩⟩` for these examples.

Each element of an `rcases` pattern is matched against a particular local hypothesis (most of which
are generated during the execution of `rcases` and represent individual elements destructured from
the input expression). An `rcases` pattern has the following grammar:

* A name like `x`, which names the active hypothesis as `x`.
* A blank `_`, which does nothing (letting the automatic naming system used by `cases` name the
  hypothesis).
* A hyphen `-`, which clears the active hypothesis and any dependents.
* The keyword `rfl`, which expects the hypothesis to be `h : a = b`, and calls `subst` on the
  hypothesis (which has the effect of replacing `b` with `a` everywhere or vice versa).
* A type ascription `p : ty`, which sets the type of the hypothesis to `ty` and then matches it
  against `p`. (Of course, `ty` must unify with the actual type of `h` for this to work.)
* A tuple pattern `⟨p1, p2, p3⟩`, which matches a constructor with many arguments, or a series
  of nested conjunctions or existentials. For example if the active hypothesis is `a ∧ b ∧ c`,
  then the conjunction will be destructured, and `p1` will be matched against `a`, `p2` against `b`
  and so on.
* A `@` before a tuple pattern as in `@⟨p1, p2, p3⟩` will bind all arguments in the constructor,
  while leaving the `@` off will only use the patterns on the explicit arguments.
* An alteration pattern `p1 | p2 | p3`, which matches an inductive type with multiple constructors,
  or a nested disjunction like `a ∨ b ∨ c`.

A pattern like `⟨a, b, c⟩ | ⟨d, e⟩` will do a split over the inductive datatype,
naming the first three parameters of the first constructor as `a,b,c` and the
first two of the second constructor `d,e`. If the list is not as long as the
number of arguments to the constructor or the number of constructors, the
remaining variables will be automatically named. If there are nested brackets
such as `⟨⟨a⟩, b | c⟩ | d` then these will cause more case splits as necessary.
If there are too many arguments, such as `⟨a, b, c⟩` for splitting on
`∃ x, ∃ y, p x`, then it will be treated as `⟨a, ⟨b, c⟩⟩`, splitting the last
parameter as necessary.

`rcases` also has special support for quotient types: quotient induction into Prop works like
matching on the constructor `quot.mk`.

`rcases h : e with PAT` will do the same as `rcases e with PAT` with the exception that an
assumption `h : e = PAT` will be added to the context.

`rcases? e` will perform case splits on `e` in the same way as `rcases e`,
but rather than accepting a pattern, it does a maximal cases and prints the
pattern that would produce this case splitting. The default maximum depth is 5,
but this can be modified with `rcases? e : n`.
-/
meta def rcases : parse rcases_parse → tactic unit
| (rcases_args.rcases h p ids) := tactic.rcases h p ids
| (rcases_args.rcases_many ps ids) := tactic.rcases_many ps ids
| (rcases_args.hint p depth) := do
  (pe, patt) ← match p with
  | sum.inl p := prod.mk <$> pp p <*> rcases_hint p depth
  | sum.inr ps := do
    patts ← rcases_hint_many ps depth,
    pes ← ps.mmap pp,
    pure (format.bracket "⟨" "⟩" (format.comma_separated pes), rcases_patt.tuple patts)
  end,
  ppat ← pp patt,
  trace $ ↑"Try this: rcases " ++ pe ++ " with " ++ ppat

add_tactic_doc
{ name       := "rcases",
  category   := doc_category.tactic,
  decl_names := [`tactic.interactive.rcases],
  tags       := ["induction"] }

/--
The `rintro` tactic is a combination of the `intros` tactic with `rcases` to
allow for destructuring patterns while introducing variables. See `rcases` for
a description of supported patterns. For example, `rintro (a | ⟨b, c⟩) ⟨d, e⟩`
will introduce two variables, and then do case splits on both of them producing
two subgoals, one with variables `a d e` and the other with `b c d e`.

`rintro`, unlike `rcases`, also supports the form `(x y : ty)` for introducing
and type-ascripting multiple variables at once, similar to binders.

`rintro?` will introduce and case split on variables in the same way as
`rintro`, but will also print the `rintro` invocation that would have the same
result. Like `rcases?`, `rintro? : n` allows for modifying the
depth of splitting; the default is 5.

`rintros` is an alias for `rintro`.
-/
meta def rintro : parse rintro_parse → tactic unit
| (sum.inl []) := intros []
| (sum.inl l)  := tactic.rintro l
| (sum.inr depth) := do
  ps ← tactic.rintro_hint depth,
  fs ← ps.mmap (λ p, do
    f ← pp $ p.format tt,
    pure $ format.space ++ format.group f),
  trace $ ↑"Try this: rintro" ++ format.join fs

/-- Alias for `rintro`. -/
meta def rintros := rintro

add_tactic_doc
{ name       := "rintro",
  category   := doc_category.tactic,
  decl_names := [`tactic.interactive.rintro, `tactic.interactive.rintros],
  tags       := ["induction"],
  inherit_description_from := `tactic.interactive.rintro }

/-- Parses `patt? (: expr)? (:= expr)?`, the arguments for `obtain`.
 (This is almost the same as `rcases_patt_parse`,
but it allows the pattern part to be empty.) -/
meta def obtain_parse :
  parser ((option rcases_patt × option pexpr) × option (pexpr ⊕ list pexpr)) :=
with_desc "patt? (: expr)? (:= expr)?" $ do
  (pat, tp) ←
    (do pat ← rcases_patt_parse,
      pure $ match pat with
      | rcases_patt.typed pat tp := (some pat, some tp)
      | _ := (some pat, none)
      end) <|>
    prod.mk none <$> (tk ":" >> texpr)?,
  prod.mk (pat, tp) <$> (do
    tk ":=",
    (guard tp.is_none >>
      sum.inr <$> brackets "⟨" "⟩" (sep_by (tk ",") (parser.pexpr 0))) <|>
    (sum.inl <$> texpr))?

/--
The `obtain` tactic is a combination of `have` and `rcases`. See `rcases` for
a description of supported patterns.

```lean
obtain ⟨patt⟩ : type,
{ ... }
```
is equivalent to
```lean
have h : type,
{ ... },
rcases h with ⟨patt⟩
```

The syntax `obtain ⟨patt⟩ : type := proof` is also supported.

If `⟨patt⟩` is omitted, `rcases` will try to infer the pattern.

If `type` is omitted, `:= proof` is required.
-/
meta def obtain : parse obtain_parse → tactic unit
| ((pat, _), some (sum.inr val)) :=
  tactic.rcases_many val (pat.get_or_else default)
| ((pat, none), some (sum.inl val)) :=
  tactic.rcases none val (pat.get_or_else default)
| ((pat, some tp), some (sum.inl val)) :=
  tactic.rcases none val $ (pat.get_or_else default).typed tp
| ((pat, some tp), none) := do
  nm ← mk_fresh_name,
  e ← to_expr tp >>= assert nm,
  (g :: gs) ← get_goals,
  set_goals gs,
  tactic.rcases none ``(%%e) (pat.get_or_else (rcases_patt.one `this)),
  gs ← get_goals,
  set_goals (g::gs)
| ((pat, none), none) :=
  fail $ "`obtain` requires either an expected type or a value.\n" ++
         "usage: `obtain ⟨patt⟩? : type (:= val)?` or `obtain ⟨patt⟩? (: type)? := val`"

add_tactic_doc
{ name       := "obtain",
  category   := doc_category.tactic,
  decl_names := [`tactic.interactive.obtain],
  tags       := ["induction"] }

/--
The `rsuffices` tactic is an alternative version of `suffices`, that allows the usage
of any syntax that would be valid in an `obtain` block. This tactic just calls `obtain`
on the expression, and then `rotate 1`.
-/
meta def rsuffices (h : parse obtain_parse) : tactic unit :=
focus1 $ obtain h >> tactic.rotate 1

add_tactic_doc
{ name       := "rsuffices",
  category   := doc_category.tactic,
  decl_names := [`tactic.interactive.rsuffices],
  tags       := ["induction"] }

/--
The `rsufficesI` tactic is an instance-cache aware version of `rsuffices`; it resets the instance
cache on the resulting goals.
-/

meta def rsufficesI (h : parse obtain_parse) : tactic unit :=
rsuffices h ; resetI

add_tactic_doc
{ name       := "rsufficesI",
  category   := doc_category.tactic,
  decl_names := [`tactic.interactive.rsufficesI],
  tags       := ["induction", "type class"] }

end interactive
end tactic


text:
/-
Copyright (c) 2019 Johannes Hölzl, Zhouhang Zhou. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Johannes Hölzl, Zhouhang Zhou
-/
import measure_theory.integration
import order.filter.germ
import topology.continuous_function.algebra

/-!

# Almost everywhere equal functions

Two measurable functions are treated as identical if they are almost everywhere equal. We form the
set of equivalence classes under the relation of being almost everywhere equal, which is sometimes
known as the `L⁰` space.

See `l1_space.lean` for `L¹` space.

## Notation

* `α →ₘ[μ] β` is the type of `L⁰` space, where `α` and `β` are measurable spaces and `μ`
  is a measure on `α`. `f : α →ₘ β` is a "function" in `L⁰`. In comments, `[f]` is also used
  to denote an `L⁰` function.

  `ₘ` can be typed as `\_m`. Sometimes it is shown as a box if font is missing.

## Main statements

* The linear structure of `L⁰` :
    Addition and scalar multiplication are defined on `L⁰` in the natural way, i.e.,
    `[f] + [g] := [f + g]`, `c • [f] := [c • f]`. So defined, `α →ₘ β` inherits the linear structure
    of `β`. For example, if `β` is a module, then `α →ₘ β` is a module over the same ring.

    See `mk_add_mk`,  `neg_mk`,     `mk_sub_mk`,  `smul_mk`,
        `add_to_fun`, `neg_to_fun`, `sub_to_fun`, `smul_to_fun`

* The order structure of `L⁰` :
    `≤` can be defined in a similar way: `[f] ≤ [g]` if `f a ≤ g a` for almost all `a` in domain.
    And `α →ₘ β` inherits the preorder and partial order of `β`.

    TODO: Define `sup` and `inf` on `L⁰` so that it forms a lattice. It seems that `β` must be a
    linear order, since otherwise `f ⊔ g` may not be a measurable function.

## Implementation notes

* `f.to_fun`     : To find a representative of `f : α →ₘ β`, use `f.to_fun`.
                 For each operation `op` in `L⁰`, there is a lemma called `op_to_fun`,
                 characterizing, say, `(f op g).to_fun`.
* `ae_eq_fun.mk` : To constructs an `L⁰` function `α →ₘ β` from a measurable function `f : α → β`,
                 use `ae_eq_fun.mk`
* `comp`         : Use `comp g f` to get `[g ∘ f]` from `g : β → γ` and `[f] : α →ₘ γ`
* `comp₂`        : Use `comp₂ g f₁ f₂ to get `[λa, g (f₁ a) (f₂ a)]`.
                 For example, `[f + g]` is `comp₂ (+)`

## Tags

function space, almost everywhere equal, `L⁰`, ae_eq_fun

-/

noncomputable theory
open_locale classical ennreal

open set filter topological_space ennreal emetric measure_theory function
variables {α β γ δ : Type*} [measurable_space α] {μ ν : measure α}

namespace measure_theory

section measurable_space
variables [measurable_space β]

variable (β)

/-- The equivalence relation of being almost everywhere equal -/
def measure.ae_eq_setoid (μ : measure α) : setoid { f : α → β // ae_measurable f μ } :=
⟨λf g, (f : α → β) =ᵐ[μ] g, λ f, ae_eq_refl f, λ f g, ae_eq_symm, λ f g h, ae_eq_trans⟩

variable (α)

/-- The space of equivalence classes of measurable functions, where two measurable functions are
    equivalent if they agree almost everywhere, i.e., they differ on a set of measure `0`.  -/
def ae_eq_fun (μ : measure α) : Type* := quotient (μ.ae_eq_setoid β)

variables {α β}

notation α ` →ₘ[`:25 μ `] ` β := ae_eq_fun α β μ

end measurable_space

namespace ae_eq_fun
variables [measurable_space β] [measurable_space γ] [measurable_space δ]

/-- Construct the equivalence class `[f]` of an almost everywhere measurable function `f`, based
    on the equivalence relation of being almost everywhere equal. -/
def mk (f : α → β) (hf : ae_measurable f μ) : α →ₘ[μ] β := quotient.mk' ⟨f, hf⟩

/-- A measurable representative of an `ae_eq_fun` [f] -/
instance : has_coe_to_fun (α →ₘ[μ] β) :=
⟨_, λf, ae_measurable.mk _ (quotient.out' f : {f : α → β // ae_measurable f μ}).2⟩

protected lemma measurable (f : α →ₘ[μ] β) : measurable f :=
ae_measurable.measurable_mk _

protected lemma ae_measurable (f : α →ₘ[μ] β) : ae_measurable f μ :=
f.measurable.ae_measurable

@[simp] lemma quot_mk_eq_mk (f : α → β) (hf) :
  (quot.mk (@setoid.r _ $ μ.ae_eq_setoid β) ⟨f, hf⟩ : α →ₘ[μ] β) = mk f hf :=
rfl

@[simp] lemma mk_eq_mk {f g : α → β} {hf hg} :
  (mk f hf : α →ₘ[μ] β) = mk g hg ↔ f =ᵐ[μ] g :=
quotient.eq'

@[simp] lemma mk_coe_fn (f : α →ₘ[μ] β) : mk f f.ae_measurable = f :=
begin
  conv_rhs { rw ← quotient.out_eq' f },
  set g : {f : α → β // ae_measurable f μ} := quotient.out' f with hg,
  have : g = ⟨g.1, g.2⟩ := subtype.eq rfl,
  rw [this, ← mk, mk_eq_mk],
  exact (ae_measurable.ae_eq_mk _).symm,
end

@[ext] lemma ext {f g : α →ₘ[μ] β} (h : f =ᵐ[μ] g) : f = g :=
by rwa [← f.mk_coe_fn, ← g.mk_coe_fn, mk_eq_mk]

lemma ext_iff {f g : α →ₘ[μ] β} : f = g ↔ f =ᵐ[μ] g :=
⟨λ h, by rw h, λ h, ext h⟩

lemma coe_fn_mk (f : α → β) (hf) : (mk f hf : α →ₘ[μ] β) =ᵐ[μ] f :=
begin
  apply (ae_measurable.ae_eq_mk _).symm.trans,
  exact @quotient.mk_out' _ (μ.ae_eq_setoid β) (⟨f, hf⟩ : {f // ae_measurable f μ})
end

@[elab_as_eliminator]
lemma induction_on (f : α →ₘ[μ] β) {p : (α →ₘ[μ] β) → Prop} (H : ∀ f hf, p (mk f hf)) : p f :=
quotient.induction_on' f $ subtype.forall.2 H

@[elab_as_eliminator]
lemma induction_on₂ {α' β' : Type*} [measurable_space α'] [measurable_space β'] {μ' : measure α'}
  (f : α →ₘ[μ] β) (f' : α' →ₘ[μ'] β') {p : (α →ₘ[μ] β) → (α' →ₘ[μ'] β') → Prop}
  (H : ∀ f hf f' hf', p (mk f hf) (mk f' hf')) :
  p f f' :=
induction_on f $ λ f hf, induction_on f' $ H f hf

@[elab_as_eliminator]
lemma induction_on₃ {α' β' : Type*} [measurable_space α'] [measurable_space β'] {μ' : measure α'}
  {α'' β'' : Type*} [measurable_space α''] [measurable_space β''] {μ'' : measure α''}
  (f : α →ₘ[μ] β) (f' : α' →ₘ[μ'] β') (f'' : α'' →ₘ[μ''] β'')
  {p : (α →ₘ[μ] β) → (α' →ₘ[μ'] β') → (α'' →ₘ[μ''] β'') → Prop}
  (H : ∀ f hf f' hf' f'' hf'', p (mk f hf) (mk f' hf') (mk f'' hf'')) :
  p f f' f'' :=
induction_on f $ λ f hf, induction_on₂ f' f'' $ H f hf

/-- Given a measurable function `g : β → γ`, and an almost everywhere equal function `[f] : α →ₘ β`,
    return the equivalence class of `g ∘ f`, i.e., the almost everywhere equal function
    `[g ∘ f] : α →ₘ γ`. -/
def comp (g : β → γ) (hg : measurable g) (f : α →ₘ[μ] β) : α →ₘ[μ] γ :=
quotient.lift_on' f (λ f, mk (g ∘ (f : α → β)) (hg.comp_ae_measurable f.2)) $
  λ f f' H, mk_eq_mk.2 $ H.fun_comp g

@[simp] lemma comp_mk (g : β → γ) (hg : measurable g)
  (f : α → β) (hf) :
  comp g hg (mk f hf : α →ₘ[μ] β) = mk (g ∘ f) (hg.comp_ae_measurable hf) :=
rfl

lemma comp_eq_mk (g : β → γ) (hg : measurable g) (f : α →ₘ[μ] β) :
  comp g hg f = mk (g ∘ f) (hg.comp_ae_measurable f.ae_measurable) :=
by rw [← comp_mk g hg f f.ae_measurable, mk_coe_fn]

lemma coe_fn_comp (g : β → γ) (hg : measurable g) (f : α →ₘ[μ] β) :
  comp g hg f =ᵐ[μ] g ∘ f :=
by { rw [comp_eq_mk], apply coe_fn_mk }

/-- The class of `x ↦ (f x, g x)`. -/
def pair (f : α →ₘ[μ] β) (g : α →ₘ[μ] γ) : α →ₘ[μ] β × γ :=
quotient.lift_on₂' f g (λ f g, mk (λ x, (f.1 x, g.1 x)) (f.2.prod_mk g.2)) $
  λ f g f' g' Hf Hg, mk_eq_mk.2 $ Hf.prod_mk Hg

@[simp] lemma pair_mk_mk (f : α → β) (hf) (g : α → γ) (hg) :
  (mk f hf : α →ₘ[μ] β).pair (mk g hg) = mk (λ x, (f x, g x)) (hf.prod_mk hg) :=
rfl

lemma pair_eq_mk (f : α →ₘ[μ] β) (g : α →ₘ[μ] γ) :
  f.pair g = mk (λ x, (f x, g x)) (f.ae_measurable.prod_mk g.ae_measurable) :=
by simp only [← pair_mk_mk, mk_coe_fn]

lemma coe_fn_pair (f : α →ₘ[μ] β) (g : α →ₘ[μ] γ) :
  f.pair g =ᵐ[μ] (λ x, (f x, g x)) :=
by { rw pair_eq_mk, apply coe_fn_mk }

/-- Given a measurable function `g : β → γ → δ`, and almost everywhere equal functions
    `[f₁] : α →ₘ β` and `[f₂] : α →ₘ γ`, return the equivalence class of the function
    `λa, g (f₁ a) (f₂ a)`, i.e., the almost everywhere equal function
    `[λa, g (f₁ a) (f₂ a)] : α →ₘ γ` -/
def comp₂ {γ δ : Type*} [measurable_space γ] [measurable_space δ] (g : β → γ → δ)
  (hg : measurable (uncurry g)) (f₁ : α →ₘ[μ] β) (f₂ : α →ₘ[μ] γ) : α →ₘ[μ] δ :=
comp _ hg (f₁.pair f₂)

@[simp] lemma comp₂_mk_mk {γ δ : Type*} [measurable_space γ] [measurable_space δ]
  (g : β → γ → δ) (hg : measurable (uncurry g)) (f₁ : α → β) (f₂ : α → γ) (hf₁ hf₂) :
  comp₂ g hg (mk f₁ hf₁ : α →ₘ[μ] β) (mk f₂ hf₂) =
    mk (λa, g (f₁ a) (f₂ a)) (hg.comp_ae_measurable (hf₁.prod_mk hf₂)) :=
rfl

lemma comp₂_eq_pair {γ δ : Type*} [measurable_space γ] [measurable_space δ]
  (g : β → γ → δ) (hg : measurable (uncurry g)) (f₁ : α →ₘ[μ] β) (f₂ : α →ₘ[μ] γ) :
  comp₂ g hg f₁ f₂ = comp _ hg (f₁.pair f₂) :=
rfl

lemma comp₂_eq_mk {γ δ : Type*} [measurable_space γ] [measurable_space δ]
  (g : β → γ → δ) (hg : measurable (uncurry g)) (f₁ : α →ₘ[μ] β) (f₂ : α →ₘ[μ] γ) :
  comp₂ g hg f₁ f₂ = mk (λ a, g (f₁ a) (f₂ a))
    (hg.comp_ae_measurable (f₁.ae_measurable.prod_mk f₂.ae_measurable)) :=
by rw [comp₂_eq_pair, pair_eq_mk, comp_mk]; refl

lemma coe_fn_comp₂ {γ δ : Type*} [measurable_space γ] [measurable_space δ]
  (g : β → γ → δ) (hg : measurable (uncurry g)) (f₁ : α →ₘ[μ] β) (f₂ : α →ₘ[μ] γ) :
  comp₂ g hg f₁ f₂ =ᵐ[μ] λ a, g (f₁ a) (f₂ a) :=
by { rw comp₂_eq_mk, apply coe_fn_mk }

/-- Interpret `f : α →ₘ[μ] β` as a germ at `μ.ae` forgetting that `f` is almost everywhere
    measurable. -/
def to_germ (f : α →ₘ[μ] β) : germ μ.ae β :=
quotient.lift_on' f (λ f, ((f : α → β) : germ μ.ae β)) $ λ f g H, germ.coe_eq.2 H

@[simp] lemma mk_to_germ (f : α → β) (hf) : (mk f hf : α →ₘ[μ] β).to_germ = f := rfl

lemma to_germ_eq (f : α →ₘ[μ] β) : f.to_germ = (f : α → β) :=
by rw [← mk_to_germ, mk_coe_fn]

lemma to_germ_injective : injective (to_germ : (α →ₘ[μ] β) → germ μ.ae β) :=
λ f g H, ext $ germ.coe_eq.1 $ by rwa [← to_germ_eq, ← to_germ_eq]

lemma comp_to_germ (g : β → γ) (hg : measurable g) (f : α →ₘ[μ] β) :
  (comp g hg f).to_germ = f.to_germ.map g :=
induction_on f $ λ f hf, by simp

lemma comp₂_to_germ (g : β → γ → δ) (hg : measurable (uncurry g))
  (f₁ : α →ₘ[μ] β) (f₂ : α →ₘ[μ] γ) :
  (comp₂ g hg f₁ f₂).to_germ = f₁.to_germ.map₂ g f₂.to_germ :=
induction_on₂ f₁ f₂ $ λ f₁ hf₁ f₂ hf₂, by simp

/-- Given a predicate `p` and an equivalence class `[f]`, return true if `p` holds of `f a`
    for almost all `a` -/
def lift_pred (p : β → Prop) (f : α →ₘ[μ] β) : Prop := f.to_germ.lift_pred p

/-- Given a relation `r` and equivalence class `[f]` and `[g]`, return true if `r` holds of
    `(f a, g a)` for almost all `a` -/
def lift_rel (r : β → γ → Prop) (f : α →ₘ[μ] β) (g : α →ₘ[μ] γ) : Prop :=
f.to_germ.lift_rel r g.to_germ

lemma lift_rel_mk_mk {r : β → γ → Prop} {f : α → β} {g : α → γ} {hf hg} :
  lift_rel r (mk f hf : α →ₘ[μ] β) (mk g hg) ↔ ∀ᵐ a ∂μ, r (f a) (g a) :=
iff.rfl

lemma lift_rel_iff_coe_fn {r : β → γ → Prop} {f : α →ₘ[μ] β} {g : α →ₘ[μ] γ} :
  lift_rel r f g ↔ ∀ᵐ a ∂μ, r (f a) (g a) :=
by rw [← lift_rel_mk_mk, mk_coe_fn, mk_coe_fn]

section order

instance [preorder β] : preorder (α →ₘ[μ] β) := preorder.lift to_germ

@[simp] lemma mk_le_mk [preorder β] {f g : α → β} (hf hg) :
  (mk f hf : α →ₘ[μ] β) ≤ mk g hg ↔ f ≤ᵐ[μ] g :=
iff.rfl

@[simp, norm_cast] lemma coe_fn_le [preorder β] {f g : α →ₘ[μ] β} :
  (f : α → β) ≤ᵐ[μ] g ↔ f ≤ g :=
lift_rel_iff_coe_fn.symm

instance [partial_order β] : partial_order (α →ₘ[μ] β) :=
partial_order.lift to_germ to_germ_injective

/- TODO: Prove `L⁰` space is a lattice if β is linear order.
         What if β is only a lattice? -/

-- instance [linear_order β] : semilattice_sup (α →ₘ β) :=
-- { sup := comp₂ (⊔) (_),
--    .. ae_eq_fun.partial_order }

end order

variable (α)
/-- The equivalence class of a constant function: `[λa:α, b]`, based on the equivalence relation of
    being almost everywhere equal -/
def const (b : β) : α →ₘ[μ] β := mk (λa:α, b) ae_measurable_const

lemma coe_fn_const (b : β) : (const α b : α →ₘ[μ] β) =ᵐ[μ] function.const α b :=
coe_fn_mk _ _

variable {α}

instance [inhabited β] : inhabited (α →ₘ[μ] β) := ⟨const α (default β)⟩

@[to_additive] instance [has_one β] : has_one (α →ₘ[μ] β) := ⟨const α 1⟩
@[to_additive] lemma one_def [has_one β] :
  (1 : α →ₘ[μ] β) = mk (λa:α, 1) ae_measurable_const := rfl
@[to_additive] lemma coe_fn_one [has_one β] : ⇑(1 : α →ₘ[μ] β) =ᵐ[μ] 1 := coe_fn_const _ _
@[simp, to_additive] lemma one_to_germ [has_one β] : (1 : α →ₘ[μ] β).to_germ = 1 := rfl

section monoid
variables
  [topological_space γ] [second_countable_topology γ] [borel_space γ]
  [monoid γ] [has_continuous_mul γ]

@[to_additive]
instance : has_mul (α →ₘ[μ] γ) := ⟨comp₂ (*) measurable_mul⟩

@[simp, to_additive] lemma mk_mul_mk (f g : α → γ) (hf hg) :
  (mk f hf : α →ₘ[μ] γ) * (mk g hg) = mk (f * g) (hf.mul hg) :=
rfl

@[to_additive] lemma coe_fn_mul (f g : α →ₘ[μ] γ) : ⇑(f * g) =ᵐ[μ] f * g := coe_fn_comp₂ _ _ _ _

@[simp, to_additive] lemma mul_to_germ (f g : α →ₘ[μ] γ) :
  (f * g).to_germ = f.to_germ * g.to_germ :=
comp₂_to_germ _ _ _ _

@[to_additive]
instance : monoid (α →ₘ[μ] γ) :=
to_germ_injective.monoid to_germ one_to_germ mul_to_germ

end monoid

@[to_additive]
instance comm_monoid [topological_space γ] [second_countable_topology γ] [borel_space γ]
  [comm_monoid γ] [has_continuous_mul γ] : comm_monoid (α →ₘ[μ] γ) :=
to_germ_injective.comm_monoid to_germ one_to_germ mul_to_germ

section group

variables [topological_space γ] [borel_space γ] [group γ] [topological_group γ]

@[to_additive] instance : has_inv (α →ₘ[μ] γ) := ⟨comp has_inv.inv measurable_inv⟩

@[simp, to_additive] lemma inv_mk (f : α → γ) (hf) : (mk f hf : α →ₘ[μ] γ)⁻¹ = mk f⁻¹ hf.inv := rfl

@[to_additive] lemma coe_fn_inv (f : α →ₘ[μ] γ) : ⇑(f⁻¹) =ᵐ[μ] f⁻¹ := coe_fn_comp _ _ _

@[to_additive] lemma inv_to_germ (f : α →ₘ[μ] γ) : (f⁻¹).to_germ = f.to_germ⁻¹ := comp_to_germ _ _ _

variables [second_countable_topology γ]

@[to_additive] instance : has_div (α →ₘ[μ] γ) := ⟨comp₂ has_div.div measurable_div⟩

@[to_additive, simp] lemma mk_div (f g : α → γ) (hf hg) :
  mk (f / g) (ae_measurable.div hf hg) = (mk f hf : α →ₘ[μ] γ) / (mk g hg) :=
rfl

@[to_additive] lemma coe_fn_div (f g : α →ₘ[μ] γ) : ⇑(f / g) =ᵐ[μ] f / g := coe_fn_comp₂ _ _ _ _

@[to_additive] lemma div_to_germ (f g : α →ₘ[μ] γ) : (f / g).to_germ = f.to_germ / g.to_germ :=
comp₂_to_germ _ _ _ _

@[to_additive]
instance : group (α →ₘ[μ] γ) :=
to_germ_injective.group _ one_to_germ mul_to_germ inv_to_germ div_to_germ

end group

@[to_additive]
instance [topological_space γ] [borel_space γ] [comm_group γ] [topological_group γ]
  [second_countable_topology γ] : comm_group (α →ₘ[μ] γ) :=
{ .. ae_eq_fun.group, .. ae_eq_fun.comm_monoid }

section module

variables {𝕜 : Type*} [semiring 𝕜] [topological_space 𝕜] [measurable_space 𝕜]
  [opens_measurable_space 𝕜]
variables [topological_space γ] [borel_space γ] [add_comm_monoid γ] [module 𝕜 γ]
  [has_continuous_smul 𝕜 γ]

instance : has_scalar 𝕜 (α →ₘ[μ] γ) :=
⟨λ c f, comp ((•) c) (measurable_id.const_smul c) f⟩

@[simp] lemma smul_mk (c : 𝕜) (f : α → γ) (hf) :
  c • (mk f hf : α →ₘ[μ] γ) = mk (c • f) (hf.const_smul _) :=
rfl

lemma coe_fn_smul (c : 𝕜) (f : α →ₘ[μ] γ) : ⇑(c • f) =ᵐ[μ] c • f := coe_fn_comp _ _ _

lemma smul_to_germ (c : 𝕜) (f : α →ₘ[μ] γ) : (c • f).to_germ = c • f.to_germ :=
comp_to_germ _ _ _

variables [second_countable_topology γ] [has_continuous_add γ]

instance : module 𝕜 (α →ₘ[μ] γ) :=
to_germ_injective.module 𝕜 ⟨@to_germ α γ _ μ _, zero_to_germ, add_to_germ⟩ smul_to_germ

end module

open ennreal

/-- For `f : α → ℝ≥0∞`, define `∫ [f]` to be `∫ f` -/
def lintegral (f : α →ₘ[μ] ℝ≥0∞) : ℝ≥0∞ :=
quotient.lift_on' f (λf, ∫⁻ a, (f : α → ℝ≥0∞) a ∂μ) (assume f g, lintegral_congr_ae)

@[simp] lemma lintegral_mk (f : α → ℝ≥0∞) (hf) :
  (mk f hf : α →ₘ[μ] ℝ≥0∞).lintegral = ∫⁻ a, f a ∂μ := rfl

lemma lintegral_coe_fn (f : α →ₘ[μ] ℝ≥0∞) : ∫⁻ a, f a ∂μ = f.lintegral :=
by rw [← lintegral_mk, mk_coe_fn]

@[simp] lemma lintegral_zero : lintegral (0 : α →ₘ[μ] ℝ≥0∞) = 0 := lintegral_zero

@[simp] lemma lintegral_eq_zero_iff {f : α →ₘ[μ] ℝ≥0∞} : lintegral f = 0 ↔ f = 0 :=
induction_on f $ λ f hf, (lintegral_eq_zero_iff' hf).trans mk_eq_mk.symm

lemma lintegral_add (f g : α →ₘ[μ] ℝ≥0∞) : lintegral (f + g) = lintegral f + lintegral g :=
induction_on₂ f g $ λ f hf g hg, by simp [lintegral_add' hf hg]

lemma lintegral_mono {f g : α →ₘ[μ] ℝ≥0∞} : f ≤ g → lintegral f ≤ lintegral g :=
induction_on₂ f g $ λ f hf g hg hfg, lintegral_mono_ae hfg

section pos_part

variables [topological_space γ] [linear_order γ] [order_closed_topology γ]
  [second_countable_topology γ] [has_zero γ] [opens_measurable_space γ]

/-- Positive part of an `ae_eq_fun`. -/
def pos_part (f : α →ₘ[μ] γ) : α →ₘ[μ] γ :=
comp (λ x, max x 0) (measurable_id.max measurable_const) f

@[simp] lemma pos_part_mk (f : α → γ) (hf) :
  pos_part (mk f hf : α →ₘ[μ] γ) = mk (λ x, max (f x) 0) (hf.max ae_measurable_const) :=
rfl

lemma coe_fn_pos_part (f : α →ₘ[μ] γ) : ⇑(pos_part f) =ᵐ[μ] (λ a, max (f a) 0) :=
coe_fn_comp _ _ _

end pos_part

end ae_eq_fun

end measure_theory

namespace continuous_map

open measure_theory

variables [topological_space α] [borel_space α] (μ)
variables [topological_space β] [measurable_space β] [borel_space β]

/-- The equivalence class of `μ`-almost-everywhere measurable functions associated to a continuous
map. -/
def to_ae_eq_fun (f : C(α, β)) : α →ₘ[μ] β :=
ae_eq_fun.mk f f.continuous.measurable.ae_measurable

lemma coe_fn_to_ae_eq_fun (f : C(α, β)) : f.to_ae_eq_fun μ =ᵐ[μ] f :=
ae_eq_fun.coe_fn_mk f _

variables [group β] [topological_group β] [second_countable_topology β]

/-- The `mul_hom` from the group of continuous maps from `α` to `β` to the group of equivalence
classes of `μ`-almost-everywhere measurable functions. -/
@[to_additive "The `add_hom` from the group of continuous maps from `α` to `β` to the group of
equivalence classes of `μ`-almost-everywhere measurable functions."]
def to_ae_eq_fun_mul_hom : C(α, β) →* α →ₘ[μ] β :=
{ to_fun := continuous_map.to_ae_eq_fun μ,
  map_one' := rfl,
  map_mul' := λ f g, ae_eq_fun.mk_mul_mk f g f.continuous.measurable.ae_measurable
    g.continuous.measurable.ae_measurable }

variables {𝕜 : Type*} [semiring 𝕜] [topological_space 𝕜] [measurable_space 𝕜]
  [opens_measurable_space 𝕜]
variables [topological_space γ] [measurable_space γ] [borel_space γ] [add_comm_group γ]
  [module 𝕜 γ] [topological_add_group γ] [has_continuous_smul 𝕜 γ]
  [second_countable_topology γ]

/-- The linear map from the group of continuous maps from `α` to `β` to the group of equivalence
classes of `μ`-almost-everywhere measurable functions. -/
def to_ae_eq_fun_linear_map : C(α, γ) →ₗ[𝕜] α →ₘ[μ] γ :=
{ map_smul' := λ c f, ae_eq_fun.smul_mk c f f.continuous.measurable.ae_measurable,
  .. to_ae_eq_fun_add_hom μ }

end continuous_map

author: JLimperg


text:
/-
Copyright (c) 2020 Johan Commelin. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Johan Commelin

! This file was ported from Lean 3 source module ring_theory.witt_vector.mul_p
! leanprover-community/mathlib commit 7abfbc92eec87190fba3ed3d5ec58e7c167e7144
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathbin.RingTheory.WittVector.IsPoly

/-!
## Multiplication by `n` in the ring of Witt vectors

In this file we show that multiplication by `n` in the ring of Witt vectors
is a polynomial function. We then use this fact to show that the composition of Frobenius
and Verschiebung is equal to multiplication by `p`.

### Main declarations

* `mul_n_is_poly`: multiplication by `n` is a polynomial function

## References

* [Hazewinkel, *Witt Vectors*][Haze09]

* [Commelin and Lewis, *Formalizing the Ring of Witt Vectors*][CL21]
-/

namespace WittVector

variable {p : ℕ} {R : Type _} [hp : Fact p.Prime] [CommRing R]

-- mathport name: expr𝕎
local notation "𝕎" => WittVector p

-- type as `\bbW`
open MvPolynomial

noncomputable section

include hp

variable (p)

/-- `witt_mul_n p n` is the family of polynomials that computes
the coefficients of `x * n` in terms of the coefficients of the Witt vector `x`. -/
noncomputable def wittMulN : ℕ → ℕ → MvPolynomial ℕ ℤ
  | 0 => 0
  | n + 1 => fun k => bind₁ (Function.uncurry <| ![witt_mul_n n, X]) (wittAdd p k)
#align witt_vector.witt_mul_n WittVector.wittMulN

variable {p}

theorem mul_n_coeff (n : ℕ) (x : 𝕎 R) (k : ℕ) : (x * n).coeff k = aeval x.coeff (wittMulN p n k) :=
  by
  induction' n with n ih generalizing k
  ·
    simp only [Nat.zero_eq, Nat.cast_zero, MulZeroClass.mul_zero, zero_coeff, witt_mul_n,
      AlgHom.map_zero, Pi.zero_apply]
  · rw [witt_mul_n, Nat.succ_eq_add_one, Nat.cast_add, Nat.cast_one, mul_add, mul_one, aeval_bind₁,
      add_coeff]
    apply eval₂_hom_congr (RingHom.ext_int _ _) _ rfl
    ext1 ⟨b, i⟩
    fin_cases b
    · simp only [Function.uncurry, Matrix.cons_val_zero, ih]
    · simp only [Function.uncurry, Matrix.cons_val_one, Matrix.head_cons, aeval_X]
#align witt_vector.mul_n_coeff WittVector.mul_n_coeff

variable (p)

/-- Multiplication by `n` is a polynomial function. -/
@[is_poly]
theorem mulNIsPoly (n : ℕ) : IsPoly p fun R _Rcr x => x * n :=
  ⟨⟨wittMulN p n, fun R _Rcr x => by
      funext k
      exact mul_n_coeff n x k⟩⟩
#align witt_vector.mul_n_is_poly WittVector.mulNIsPoly

@[simp]
theorem bind₁_wittMulN_wittPolynomial (n k : ℕ) :
    bind₁ (wittMulN p n) (wittPolynomial p ℤ k) = n * wittPolynomial p ℤ k :=
  by
  induction' n with n ih
  · simp only [witt_mul_n, Nat.cast_zero, MulZeroClass.zero_mul, bind₁_zero_witt_polynomial]
  · rw [witt_mul_n, ← bind₁_bind₁, witt_add, wittStructureInt_prop]
    simp only [AlgHom.map_add, Nat.cast_succ, bind₁_X_right]
    rw [add_mul, one_mul, bind₁_rename, bind₁_rename]
    simp only [ih, Function.uncurry, Function.comp, bind₁_X_left, AlgHom.id_apply,
      Matrix.cons_val_zero, Matrix.head_cons, Matrix.cons_val_one]
#align witt_vector.bind₁_witt_mul_n_witt_polynomial WittVector.bind₁_wittMulN_wittPolynomial

end WittVector

author: leanprover-community


text:
/-
Copyright (c) 2016 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura, Jeremy Avigad, Mario Carneiro
-/
import Std.Logic
import Std.Tactic.Basic
import Std.Data.Nat.Basic

namespace Nat

attribute [simp] succ_ne_zero lt_succ_self Nat.add_sub_cancel succ_sub_succ_eq_sub

theorem succ_ne_self : ∀ n : Nat, succ n ≠ n
| 0,   h => absurd h (succ_ne_zero 0)
| n+1, h => succ_ne_self n (Nat.noConfusion h id)

protected theorem eq_zero_of_add_eq_zero_right : ∀ {n m : Nat}, n + m = 0 → n = 0
| 0,   m => by simp [Nat.zero_add]
| n+1, m => fun h => by
  rw [add_one, succ_add] at h
  cases succ_ne_zero _ h

protected theorem eq_zero_of_add_eq_zero_left {n m : Nat} (h : n + m = 0) : m = 0 :=
  @Nat.eq_zero_of_add_eq_zero_right m n (Nat.add_comm n m ▸ h)

attribute [simp] Nat.pred_zero Nat.pred_succ

/- properties of inequality -/

theorem ne_of_gt {a b : Nat} (h : b < a) : a ≠ b := (ne_of_lt h).symm

theorem succ_le {n m : Nat} : succ n ≤ m ↔ n < m := .rfl

protected theorem le_of_not_le {a b : Nat} : ¬ a ≤ b → b ≤ a := (Nat.le_total a b).resolve_left

protected theorem pos_of_ne_zero {n : Nat} : n ≠ 0 → 0 < n := (eq_zero_or_pos n).resolve_left

protected theorem pos_iff_ne_zero {n : Nat} : 0 < n ↔ n ≠ 0 := ⟨ne_of_gt, Nat.pos_of_ne_zero⟩

protected theorem lt_iff_le_not_le {m n : Nat} : m < n ↔ m ≤ n ∧ ¬ n ≤ m :=
  ⟨fun h => ⟨Nat.le_of_lt h, Nat.not_le_of_gt h⟩, fun h => Nat.gt_of_not_le h.2⟩

protected theorem lt_iff_le_and_ne {m n : Nat} : m < n ↔ m ≤ n ∧ m ≠ n :=
  Nat.lt_iff_le_not_le.trans (and_congr_right fun h =>
    not_congr ⟨Nat.le_antisymm h, fun e => e ▸ Nat.le_refl _⟩)

@[simp] protected theorem not_le {a b : Nat} : ¬ a ≤ b ↔ b < a :=
  ⟨Nat.gt_of_not_le, Nat.not_le_of_gt⟩

@[simp] protected theorem not_lt {a b : Nat} : ¬ a < b ↔ b ≤ a :=
  ⟨Nat.ge_of_not_lt, flip Nat.not_le_of_gt⟩

theorem pred_lt_pred : ∀ {n m : Nat}, n ≠ 0 → n < m → pred n < pred m
| 0,   _,   h, _ => (h rfl).elim
| _+1, _+1, _, h => lt_of_succ_lt_succ h

theorem succ_le_succ_iff {a b : Nat} : succ a ≤ succ b ↔ a ≤ b :=
  ⟨le_of_succ_le_succ, succ_le_succ⟩

protected theorem add_left_cancel_iff {n m k : Nat} : n + m = n + k ↔ m = k :=
  ⟨Nat.add_left_cancel, fun | rfl => rfl⟩

protected theorem add_le_add_iff_le_right (k n m : Nat) : n + k ≤ m + k ↔ n ≤ m :=
⟨Nat.le_of_add_le_add_right, fun h => Nat.add_le_add_right h _⟩

protected theorem lt_of_add_lt_add_left {k n m : Nat} (h : k + n < k + m) : n < m :=
  Nat.lt_of_le_of_ne (Nat.le_of_add_le_add_left (Nat.le_of_lt h)) fun heq =>
    Nat.lt_irrefl (k + m) <| by rwa [heq] at h

protected theorem lt_of_add_lt_add_right {a b c : Nat} (h : a + b < c + b) : a < c :=
  Nat.lt_of_add_lt_add_left ((by rwa [Nat.add_comm b a, Nat.add_comm b c]): b + a < b + c)

protected theorem lt_add_right (a b c : Nat) (h : a < b) : a < b + c :=
  Nat.lt_of_lt_of_le h (Nat.le_add_right _ _)

protected theorem lt_add_of_pos_right {n k : Nat} (h : 0 < k) : n < n + k :=
  Nat.add_lt_add_left h n

protected theorem lt_add_of_pos_left {n k : Nat} (h : 0 < k) : n < k + n := by
  rw [Nat.add_comm]; exact Nat.lt_add_of_pos_right h

/- sub properties -/

attribute [simp] Nat.zero_sub

theorem sub_lt_succ (a b : Nat) : a - b < succ a :=
  lt_succ_of_le (sub_le a b)

protected theorem sub_le_sub_right {n m : Nat} (h : n ≤ m) : ∀ k, n - k ≤ m - k
  | 0   => h
  | z+1 => pred_le_pred (Nat.sub_le_sub_right h z)

-- port note: bit0/bit1 items have been omitted.

protected theorem add_self_ne_one : ∀ (n : Nat), n + n ≠ 1
  | n+1, h =>
    have h1 : succ (succ (n + n)) = 1 := succ_add n n ▸ h
    Nat.noConfusion h1 fun.

/- subtraction -/

protected theorem le_of_le_of_sub_le_sub_right :
    ∀ {n m k : Nat}, k ≤ m → n - k ≤ m - k → n ≤ m
  | 0, m, _, _, _ => m.zero_le
  | succ _, _, 0, _, h₁ => h₁
  | succ _, 0, succ k, h₀, _ => nomatch not_succ_le_zero k h₀
  | succ n, succ m, succ k, h₀, h₁ => by
    simp [succ_sub_succ] at h₁
    exact succ_le_succ <| Nat.le_of_le_of_sub_le_sub_right (le_of_succ_le_succ h₀) h₁

protected theorem sub_le_sub_right_iff {n m k : Nat} (h : k ≤ m) : n - k ≤ m - k ↔ n ≤ m :=
  ⟨Nat.le_of_le_of_sub_le_sub_right h, fun h => Nat.sub_le_sub_right h k⟩

protected theorem add_le_to_le_sub (x : Nat) {y k : Nat} (h : k ≤ y) :
    x + k ≤ y ↔ x ≤ y - k := by
  rw [← Nat.add_sub_cancel x k, Nat.sub_le_sub_right_iff h, Nat.add_sub_cancel]

protected theorem sub_lt_of_pos_le (a b : Nat) (h₀ : 0 < a) (h₁ : a ≤ b) : b - a < b :=
  Nat.sub_lt (Nat.lt_of_lt_of_le h₀ h₁) h₀

protected theorem sub_one (n : Nat) : n - 1 = pred n := rfl

theorem succ_sub_one (n : Nat) : succ n - 1 = n := rfl

theorem succ_pred_eq_of_pos : ∀ {n : Nat}, 0 < n → succ (pred n) = n
  | succ _, _ => rfl

protected

protected theorem eq_zero_of_nonpos : ∀ (n : Nat), ¬0 < n → n = 0
  | 0 => fun _ => rfl
  | n+1 => fun h => absurd (Nat.zero_lt_succ n) h

protected theorem sub_eq_zero_iff_le : n - m = 0 ↔ n ≤ m :=
  ⟨Nat.le_of_sub_eq_zero, Nat.sub_eq_zero_of_le⟩

protected theorem sub_eq_iff_eq_add {a b c : Nat} (ab : b ≤ a) : a - b = c ↔ a = c + b :=
  ⟨fun c_eq => by rw [c_eq.symm, Nat.sub_add_cancel ab],
   fun a_eq => by rw [a_eq, Nat.add_sub_cancel]⟩

protected theorem lt_of_sub_eq_succ (H : m - n = succ l) : n < m :=
  Nat.not_le.1 fun H' => by simp [Nat.sub_eq_zero_of_le H'] at H

protected theorem min_eq_min (a : Nat) : Nat.min a b = min a b := rfl

protected theorem max_eq_max (a : Nat) : Nat.max a b = max a b := rfl

protected theorem min_comm (a b : Nat) : min a b = min b a := by
  simp [Nat.min_def]; split <;> split <;> simp [*]
  · next h₁ h₂ => exact Nat.le_antisymm h₁ h₂
  · next h₁ h₂ => cases not_or_intro h₁ h₂ <| Nat.le_total ..

protected theorem min_le_right (a b : Nat) : min a b ≤ b := by rw [Nat.min_def]; split <;> simp [*]

protected theorem min_le_left (a b : Nat) : min a b ≤ a := Nat.min_comm .. ▸ Nat.min_le_right ..

protected theorem le_min {a b c : Nat} : a ≤ min b c ↔ a ≤ b ∧ a ≤ c :=
  ⟨fun h => ⟨Nat.le_trans h (Nat.min_le_left ..), Nat.le_trans h (Nat.min_le_right ..)⟩,
   fun ⟨h₁, h₂⟩ => by rw [Nat.min_def]; split <;> assumption⟩

protected theorem min_eq_left {a b : Nat} (h : a ≤ b) : min a b = a := by simp [Nat.min_def, h]

protected theorem min_eq_right {a b : Nat} (h : b ≤ a) : min a b = b := by
  rw [Nat.min_comm a b]; exact Nat.min_eq_left h

protected theorem zero_min (a : Nat) : min 0 a = 0 := Nat.min_eq_left (zero_le a)

protected theorem min_zero (a : Nat) : min a 0 = 0 := Nat.min_eq_right (zero_le a)

protected theorem max_comm (a b : Nat) : max a b = max b a := by
  simp only [Nat.max_def]
  by_cases h₁ : a ≤ b <;> by_cases h₂ : b ≤ a <;> simp [h₁, h₂]
  · exact Nat.le_antisymm h₂ h₁
  · cases not_or_intro h₁ h₂ <| Nat.le_total ..

protected theorem le_max_left (a b : Nat) : a ≤ max a b := by rw [Nat.max_def]; split <;> simp [*]

protected theorem le_max_right (a b : Nat) : b ≤ max a b := Nat.max_comm .. ▸ Nat.le_max_left ..

protected theorem max_le {a b c : Nat} : max a b ≤ c ↔ a ≤ c ∧ b ≤ c :=
  ⟨fun h => ⟨Nat.le_trans (Nat.le_max_left ..) h, Nat.le_trans (Nat.le_max_right ..) h⟩,
   fun ⟨h₁, h₂⟩ => by rw [Nat.max_def]; split <;> assumption⟩

protected theorem max_eq_right {a b : Nat} (h : a ≤ b) : max a b = b := by
  simp [Nat.max_def, h, Nat.not_lt.2 h]

protected theorem max_eq_left {a b : Nat} (h : b ≤ a) : max a b = a := by
  rw [← Nat.max_comm b a]; exact Nat.max_eq_right h

-- Distribute succ over min
theorem min_succ_succ (x y : Nat) : min (succ x) (succ y) = succ (min x y) := by
  simp [Nat.min_def, succ_le_succ_iff]; split <;> rfl

theorem sub_eq_sub_min (n m : Nat) : n - m = n - min n m := by
  rw [Nat.min_def]; split
  · rw [Nat.sub_eq_zero_of_le ‹n ≤ m›, Nat.sub_self]
  · rfl

@[simp] protected theorem sub_add_min_cancel (n m : Nat) : n - m + min n m = n := by
  rw [sub_eq_sub_min, Nat.sub_add_cancel (Nat.min_le_left n m)]

/- multiplication -/

protected theorem mul_right_comm (n m k : Nat) : n * m * k = n * k * m := by
  rw [Nat.mul_assoc, Nat.mul_comm m, ← Nat.mul_assoc]

protected theorem mul_two (n : Nat) : n * 2 = n + n := by simp [Nat.mul_succ]

protected theorem two_mul (n : Nat) : 2 * n = n + n := by simp [Nat.succ_mul]

/- mod -/

-- TODO mod_core_congr, mod_def

theorem mod_two_eq_zero_or_one (n : Nat) : n % 2 = 0 ∨ n % 2 = 1 :=
  match n % 2, @Nat.mod_lt n 2 (by simp) with
  | 0, _ => .inl rfl
  | 1, _ => .inr rfl

/- div & mod -/

-- TODO div_core_congr, div_def

theorem mod_add_div (m k : Nat) : m % k + k * (m / k) = m := by
  induction m, k using mod.inductionOn with rw [div_eq, mod_eq]
  | base x y h => simp [h]
  | ind x y h IH => simp [h]; rw [Nat.mul_succ, ← Nat.add_assoc, IH, Nat.sub_add_cancel h.2]

/- div -/

@[simp] protected theorem div_one (n : Nat) : n / 1 = n := by
  have := mod_add_div n 1
  rwa [mod_one, Nat.zero_add, Nat.one_mul] at this

@[simp] protected theorem div_zero (n : Nat) : n / 0 = 0 := by
  rw [div_eq]; simp [Nat.lt_irrefl]

@[simp] protected theorem zero_div (b : Nat) : 0 / b = 0 :=
  (div_eq 0 b).trans <| if_neg <| And.rec Nat.not_le_of_gt

theorem le_div_iff_mul_le (k0 : 0 < k) : x ≤ y / k ↔ x * k ≤ y := by
  induction y, k using mod.inductionOn generalizing x with
    (rw [div_eq]; simp [h]; cases x with simp [zero_le] | succ x => ?_)
  | base y k h =>
    simp [not_succ_le_zero x, succ_mul, Nat.add_comm]
    refine Nat.lt_of_lt_of_le ?_ (Nat.le_add_right ..)
    exact Nat.not_le.1 fun h' => h ⟨k0, h'⟩
  | ind y k h IH =>
    rw [← add_one, Nat.add_le_add_iff_le_right, IH k0, succ_mul,
        ← Nat.add_sub_cancel (x*k) k, Nat.sub_le_sub_right_iff h.2, Nat.add_sub_cancel]

protected theorem div_le_of_le_mul {m n : Nat} : ∀ {k}, m ≤ k * n → m / k ≤ n
  | 0, _ => by simp [Nat.div_zero, n.zero_le]
  | succ k, h => by
    suffices succ k * (m / succ k) ≤ succ k * n from
      Nat.le_of_mul_le_mul_left this (zero_lt_succ _)
    have h1 : succ k * (m / succ k) ≤ m % succ k + succ k * (m / succ k) := Nat.le_add_left _ _
    have h2 : m % succ k + succ k * (m / succ k) = m := by rw [mod_add_div]
    have h3 : m ≤ succ k * n := h
    rw [← h2] at h3
    exact Nat.le_trans h1 h3

theorem div_eq_sub_div (h₁ : 0 < b) (h₂ : b ≤ a) : a / b = (a - b) / b + 1 := by
 rw [div_eq a, if_pos]; constructor <;> assumption

theorem div_eq_of_lt (h₀ : a < b) : a / b = 0 := by
  rw [div_eq a, if_neg]
  intro h₁
  apply Nat.not_le_of_gt h₀ h₁.right

theorem div_lt_iff_lt_mul (Hk : 0 < k) : x / k < y ↔ x < y * k := by
  rw [← Nat.not_le, ← Nat.not_le]; exact not_congr (le_div_iff_mul_le Hk)

/- successor and predecessor -/

theorem add_one_ne_zero (n : Nat) : n + 1 ≠ 0 := succ_ne_zero _

theorem eq_zero_or_eq_succ_pred (n : Nat) : n = 0 ∨ n = succ (pred n) := by
  cases n <;> simp

theorem exists_eq_succ_of_ne_zero {n : Nat} (H : n ≠ 0) : ∃ k, n = succ k :=
  ⟨_, (eq_zero_or_eq_succ_pred _).resolve_left H⟩

theorem succ_eq_one_add (n : Nat) : n.succ = 1 + n := by
  rw [Nat.succ_eq_add_one, Nat.add_comm]

theorem succ_inj' : succ n = succ m ↔ n = m :=
  ⟨succ.inj, congrArg _⟩

/- addition -/

theorem succ_add_eq_succ_add (n m : Nat) : succ n + m = n + succ m := by
  simp [succ_add, add_succ]

theorem one_add (n : Nat) : 1 + n = succ n := by simp [Nat.add_comm]

theorem eq_zero_of_add_eq_zero {n m : Nat} (H : n + m = 0) : n = 0 ∧ m = 0 :=
  ⟨Nat.eq_zero_of_add_eq_zero_right H, Nat.eq_zero_of_add_eq_zero_left H⟩

theorem mul_eq_zero {n m : Nat} : n * m = 0 ↔ n = 0 ∨ m = 0 :=
  ⟨fun h => match n, m, h with
    | 0,   m, _ => .inl rfl
    | n+1, m, h => by rw [succ_mul] at h; exact .inr (Nat.eq_zero_of_add_eq_zero_left h),
   fun | .inl h | .inr h => by simp [h]⟩

protected theorem mul_ne_zero_iff : n * m ≠ 0 ↔ n ≠ 0 ∧ m ≠ 0 := by simp [mul_eq_zero, not_or]

protected theorem mul_ne_zero (n0 : n ≠ 0) (m0 : m ≠ 0) : n * m ≠ 0 :=
  Nat.mul_ne_zero_iff.2 ⟨n0, m0⟩

/- properties of inequality -/

theorem le_succ_of_pred_le {n m : Nat} : pred n ≤ m → n ≤ succ m :=
  match n with
  | 0 => fun _ => zero_le _
  | _+1 => succ_le_succ

theorem le_lt_antisymm {n m : Nat} (h₁ : n ≤ m) (h₂ : m < n) : False :=
  Nat.lt_irrefl n (Nat.lt_of_le_of_lt h₁ h₂)

theorem lt_le_antisymm {n m : Nat} (h₁ : n < m) (h₂ : m ≤ n) : False :=
  le_lt_antisymm h₂ h₁

protected theorem lt_asymm {n m : Nat} (h₁ : n < m) : ¬ m < n :=
  le_lt_antisymm (Nat.le_of_lt h₁)

/-- Strong case analysis on `a < b ∨ b ≤ a` -/
protected def lt_sum_ge (a b : Nat) : a < b ⊕' b ≤ a :=
  if h : a < b then .inl h else .inr (Nat.not_lt.1 h)

/-- Strong case analysis on `a < b ∨ a = b ∨ b < a` -/
protected def sum_trichotomy (a b : Nat) : a < b ⊕' a = b ⊕' b < a :=
  match a.lt_sum_ge b with
  | .inl h => .inl h
  | .inr h₂ => match b.lt_sum_ge a with
    | .inl h => .inr <| .inr h
    | .inr h₁ => .inr <| .inl <| Nat.le_antisymm h₁ h₂

protected theorem lt_trichotomy (a b : Nat) : a < b ∨ a = b ∨ b < a :=
  match a.sum_trichotomy b with
  | .inl h => .inl h
  | .inr (.inl h) => .inr (.inl h)
  | .inr (.inr h) => .inr (.inr h)

protected theorem eq_or_lt_of_not_lt {a b : Nat} (hnlt : ¬ a < b) : a = b ∨ b < a :=
  (Nat.lt_trichotomy a b).resolve_left hnlt

theorem lt_succ_of_lt (h : a < b) : a < succ b := le_succ_of_le h

theorem one_pos : 0 < 1 := Nat.zero_lt_one

protected theorem not_lt_of_le {n m : Nat} (h₁ : m ≤ n) : ¬ n < m := (Nat.not_le_of_gt · h₁)

protected theorem not_le_of_lt {n m : Nat} : m < n → ¬ n ≤ m := Nat.not_le_of_gt

protected theorem lt_of_not_le {a b : Nat} : ¬ a ≤ b → b < a := (Nat.lt_or_ge b a).resolve_right

protected theorem le_of_not_lt {a b : Nat} : ¬ a < b → b ≤ a := (Nat.lt_or_ge a b).resolve_left

protected theorem le_or_le (a b : Nat) : a ≤ b ∨ b ≤ a := (Nat.lt_or_ge _ _).imp_left Nat.le_of_lt

protected theorem lt_or_eq_of_le {n m : Nat} (h : n ≤ m) : n < m ∨ n = m :=
  (Nat.lt_or_ge _ _).imp_right (Nat.le_antisymm h)

theorem le_zero {i : Nat} : i ≤ 0 ↔ i = 0 :=
  ⟨Nat.eq_zero_of_le_zero, fun h => h ▸ Nat.le_refl i⟩

theorem lt_succ {m n : Nat} : m < succ n ↔ m ≤ n :=
  ⟨le_of_lt_succ, lt_succ_of_le⟩

/- subtraction -/

protected theorem sub_add_eq_max {a b : Nat} : a - b + b = max a b := by
  match a.le_total b with
  | .inl hl => rw [Nat.max_eq_right hl, Nat.sub_eq_zero_iff_le.mpr hl, Nat.zero_add]
  | .inr hr => rw [Nat.max_eq_left hr, Nat.sub_add_cancel hr]

protected theorem sub_le_sub_left (k : Nat) (h : n ≤ m) : k - m ≤ k - n :=
  match m, le.dest h with
  | _, ⟨a, rfl⟩ => by rw [← Nat.sub_sub]; apply sub_le

theorem succ_sub_sub_succ (n m k : Nat) : succ n - m - succ k = n - m - k := by
  rw [Nat.sub_sub, Nat.sub_sub, add_succ, succ_sub_succ]

protected theorem sub.right_comm (m n k : Nat) : m - n - k = m - k - n := by
  rw [Nat.sub_sub, Nat.sub_sub, Nat.add_comm]

protected theorem mul_self_sub_mul_self_eq (a b : Nat) : a * a - b * b = (a + b) * (a - b) := by
  rw [Nat.mul_sub_left_distrib, Nat.right_distrib, Nat.right_distrib,
      Nat.mul_comm b a, Nat.add_comm (a*a) (a*b), Nat.add_sub_add_left]

theorem succ_mul_succ_eq (a b : Nat) : succ a * succ b = a * b + a + b + 1 := by
  rw [mul_succ, succ_mul, Nat.add_right_comm _ a]; rfl

theorem succ_sub {m n : Nat} (h : n ≤ m) : succ m - n = succ (m - n) := by
  let ⟨k, hk⟩ := Nat.le.dest h
  rw [← hk, Nat.add_sub_cancel_left, ← add_succ, Nat.add_sub_cancel_left]

protected theorem sub_pos_of_lt (h : m < n) : 0 < n - m := by
  apply Nat.lt_of_add_lt_add_right (b := m)
  rwa [Nat.zero_add, Nat.sub_add_cancel (Nat.le_of_lt h)]

protected theorem sub_sub_self {n m : Nat} (h : m ≤ n) : n - (n - m) = m :=
  (Nat.sub_eq_iff_eq_add (Nat.sub_le ..)).2 (Nat.add_sub_of_le h).symm

protected theorem sub_add_comm {n m k : Nat} (h : k ≤ n) : n + m - k = n - k + m := by
  rw [Nat.sub_eq_iff_eq_add (Nat.le_trans h (Nat.le_add_right ..))]
  rwa [Nat.add_right_comm, Nat.sub_add_cancel]

theorem sub_one_sub_lt (h : i < n) : n - 1 - i < n := by
  rw [Nat.sub_sub]
  apply Nat.sub_lt (Nat.lt_of_lt_of_le (Nat.zero_lt_succ _) h)
  rw [Nat.add_comm]; apply Nat.zero_lt_succ

theorem pred_inj : ∀ {a b : Nat}, 0 < a → 0 < b → Nat.pred a = Nat.pred b → a = b
| a+1, b+1, _,  _, h => by rw [show a = b from h]
| a+1, 0,   _, hb, _ => absurd hb (Nat.lt_irrefl _)
| 0,   b+1, ha, _, _ => absurd ha (Nat.lt_irrefl _)
| 0,   0,   _,  _, _ => rfl

theorem sub_lt_self {a b : Nat} (h₀ : 0 < a) (h₁ : a ≤ b) : b - a < b := by
  apply sub_lt _ h₀
  apply Nat.lt_of_lt_of_le h₀ h₁

protected theorem add_sub_cancel' {n m : Nat} (h : m ≤ n) : m + (n - m) = n := by
  rw [Nat.add_comm, Nat.sub_add_cancel h]

protected theorem sub_lt_sub_left : ∀ {k m n : Nat}, k < m → k < n → m - n < m - k
  | 0, m+1, n+1, _, _ => by rw [Nat.add_sub_add_right]; exact lt_succ_of_le (Nat.sub_le _ _)
  | k+1, m+1, n+1, h1, h2 => by
    rw [Nat.add_sub_add_right, Nat.add_sub_add_right]
    exact Nat.sub_lt_sub_left (Nat.lt_of_succ_lt_succ h1) (Nat.lt_of_succ_lt_succ h2)

protected theorem sub_lt_left_of_lt_add {n k m : Nat} (H : n ≤ k) (h : k < n + m) : k - n < m := by
  have := Nat.sub_le_sub_right (succ_le_of_lt h) n
  rwa [Nat.add_sub_cancel_left, Nat.succ_sub H] at this

protected theorem add_le_of_le_sub_left {n k m : Nat} (H : m ≤ k) (h : n ≤ k - m) : m + n ≤ k :=
  Nat.not_lt.1 fun h' => Nat.not_lt.2 h (Nat.sub_lt_left_of_lt_add H h')

theorem le_sub_iff_add_le {x y k : Nat} (h : k ≤ y) : x ≤ y - k ↔ x + k ≤ y := by
  rw [← Nat.add_sub_cancel x k, Nat.sub_le_sub_right_iff h, Nat.add_sub_cancel]

theorem le_pred_of_lt {m n : Nat} (h : m < n) : m ≤ n - 1 :=
  Nat.sub_le_sub_right h 1

protected theorem sub_add_lt_sub {n m k : Nat} (h₁ : m + k ≤ n) (h₂ : 0 < k) :
    n - (m + k) < n - m :=
  match k with
  | zero => Nat.lt_irrefl _ h₂ |>.elim
  | succ _ =>
    Nat.lt_of_lt_of_le
      (pred_lt (Nat.ne_of_lt $ Nat.sub_pos_of_lt $ lt_of_succ_le h₁).symm)
      (Nat.sub_le_sub_left _ $ Nat.le_add_right _ _)

/- mod -/

theorem le_of_mod_lt {a b : Nat} (h : a % b < a) : b ≤ a :=
  Nat.not_lt.1 fun hf => (ne_of_lt h).elim (Nat.mod_eq_of_lt hf)

@[simp] theorem add_mod_right (x z : Nat) : (x + z) % z = x % z := by
  rw [mod_eq_sub_mod (Nat.le_add_left ..), Nat.add_sub_cancel]

@[simp] theorem add_mod_left (x z : Nat) : (x + z) % x = z % x := by
  rw [Nat.add_comm, add_mod_right]

@[simp] theorem add_mul_mod_self_left (x y z : Nat) : (x + y * z) % y = x % y := by
  match z with
  | 0 => rw [Nat.mul_zero, Nat.add_zero]
  | succ z => rw [mul_succ, ← Nat.add_assoc, add_mod_right, add_mul_mod_self_left (z := z)]

@[simp] theorem add_mul_mod_self_right (x y z : Nat) : (x + y * z) % z = x % z := by
  rw [Nat.mul_comm, add_mul_mod_self_left]

@[simp] theorem mul_mod_right (m n : Nat) : (m * n) % m = 0 := by
  rw [← Nat.zero_add (m * n), add_mul_mod_self_left, zero_mod]

@[simp] theorem mul_mod_left (m n : Nat) : (m * n) % n = 0 := by
  rw [Nat.mul_comm, mul_mod_right]

theorem mul_mod_mul_left (z x y : Nat) : (z * x) % (z * y) = z * (x % y) :=
  if y0 : y = 0 then by
    rw [y0, Nat.mul_zero, mod_zero, mod_zero]
  else if z0 : z = 0 then by
    rw [z0, Nat.zero_mul, Nat.zero_mul, Nat.zero_mul, mod_zero]
  else by
    induction x using Nat.strongInductionOn with
    | _ n IH =>
      have y0 : y > 0 := Nat.pos_of_ne_zero y0
      have z0 : z > 0 := Nat.pos_of_ne_zero z0
      cases Nat.lt_or_ge n y with
      | inl yn => rw [mod_eq_of_lt yn, mod_eq_of_lt (Nat.mul_lt_mul_of_pos_left yn z0)]
      | inr yn =>
        rw [mod_eq_sub_mod yn, mod_eq_sub_mod (Nat.mul_le_mul_left z yn),
          ← Nat.mul_sub_left_distrib]
        exact IH _ (sub_lt (Nat.lt_of_lt_of_le y0 yn) y0)

theorem mul_mod_mul_right (z x y : Nat) : (x * z) % (y * z) = (x % y) * z := by
  rw [Nat.mul_comm x z, Nat.mul_comm y z, Nat.mul_comm (x % y) z]; apply mul_mod_mul_left

-- TODO cont_to_bool_mod_two

theorem sub_mul_mod {x k n : Nat} (h₁ : n*k ≤ x) : (x - n*k) % n = x % n := by
  match k with
  | 0 => rw [Nat.mul_zero, Nat.sub_zero]
  | succ k =>
    have h₂ : n * k ≤ x := Nat.le_trans (le_add_right _ n) h₁
    have h₄ : x - n * k ≥ n := by
      apply Nat.le_of_add_le_add_right (b := n * k)
      rw [Nat.sub_add_cancel h₂]
      simp [mul_succ, Nat.add_comm] at h₁; simp [h₁]
    rw [mul_succ, ← Nat.sub_sub, ← mod_eq_sub_mod h₄, sub_mul_mod h₂]

/- div -/

theorem sub_mul_div (x n p : Nat) (h₁ : n*p ≤ x) : (x - n*p) / n = x / n - p := by
  match eq_zero_or_pos n with
  | .inl h₀ => rw [h₀, Nat.div_zero, Nat.div_zero, Nat.zero_sub]
  | .inr h₀ => induction p with
    | zero => rw [Nat.mul_zero, Nat.sub_zero, Nat.sub_zero]
    | succ p IH =>
      have h₂ : n * p ≤ x := Nat.le_trans (Nat.mul_le_mul_left _ (le_succ _)) h₁
      have h₃ : x - n * p ≥ n := by
        apply Nat.le_of_add_le_add_right
        rw [Nat.sub_add_cancel h₂, Nat.add_comm]
        rw [mul_succ] at h₁
        exact h₁
      rw [sub_succ, ← IH h₂, div_eq_sub_div h₀ h₃]
      simp [add_one, Nat.pred_succ, mul_succ, Nat.sub_sub]

theorem div_mul_le_self : ∀ (m n : Nat), m / n * n ≤ m
  | m, 0   => by simp
  | m, n+1 => (le_div_iff_mul_le (Nat.succ_pos _)).1 (Nat.le_refl _)

@[simp] theorem add_div_right (x : Nat) {z : Nat} (H : 0 < z) : (x + z) / z = succ (x / z) := by
  rw [div_eq_sub_div H (Nat.le_add_left _ _), Nat.add_sub_cancel]

@[simp] theorem add_div_left (x : Nat) {z : Nat} (H : 0 < z) : (z + x) / z = succ (x / z) := by
  rw [Nat.add_comm, add_div_right x H]

@[simp] theorem mul_div_right (n : Nat) {m : Nat} (H : 0 < m) : m * n / m = n := by
  induction n <;> simp_all [mul_succ]

@[simp] theorem mul_div_left (m : Nat) {n : Nat} (H : 0 < n) : m * n / n = m := by
  rw [Nat.mul_comm, mul_div_right _ H]

protected theorem div_self (H : 0 < n) : n / n = 1 := by
  let t := add_div_right 0 H
  rwa [Nat.zero_add, Nat.zero_div] at t

theorem add_mul_div_left (x z : Nat) {y : Nat} (H : 0 < y) : (x + y * z) / y = x / y + z := by
  induction z with
  | zero => rw [Nat.mul_zero, Nat.add_zero, Nat.add_zero]
  | succ z ih => rw [mul_succ, ← Nat.add_assoc, add_div_right _ H, ih]; rfl

theorem add_mul_div_right (x y : Nat) {z : Nat} (H : 0 < z) : (x + y * z) / z = x / z + y := by
  rw [Nat.mul_comm, add_mul_div_left _ _ H]

protected theorem mul_div_cancel (m : Nat) {n : Nat} (H : 0 < n) : m * n / n = m := by
  let t := add_mul_div_right 0 m H
  rwa [Nat.zero_add, Nat.zero_div, Nat.zero_add] at t

protected theorem mul_div_cancel_left (m : Nat) {n : Nat} (H : 0 < n) : n * m / n = m :=
by rw [Nat.mul_comm, Nat.mul_div_cancel _ H]

protected theorem div_eq_of_eq_mul_left (H1 : 0 < n) (H2 : m = k * n) : m / n = k :=
by rw [H2, Nat.mul_div_cancel _ H1]

protected theorem div_eq_of_eq_mul_right (H1 : 0 < n) (H2 : m = n * k) : m / n = k :=
by rw [H2, Nat.mul_div_cancel_left _ H1]

protected theorem div_eq_of_lt_le (lo : k * n ≤ m) (hi : m < succ k * n) : m / n = k :=
have npos : 0 < n := (eq_zero_or_pos _).resolve_left fun hn => by
  rw [hn, Nat.mul_zero] at hi lo; exact absurd lo (Nat.not_le_of_gt hi)
Nat.le_antisymm
  (le_of_lt_succ ((Nat.div_lt_iff_lt_mul npos).2 hi))
  ((Nat.le_div_iff_mul_le npos).2 lo)

theorem mul_sub_div (x n p : Nat) (h₁ : x < n*p) : (n * p - succ x) / n = p - succ (x / n) := by
  have npos : 0 < n := (eq_zero_or_pos _).resolve_left fun n0 => by
    rw [n0, Nat.zero_mul] at h₁; exact not_lt_zero _ h₁
  apply Nat.div_eq_of_lt_le
  · rw [Nat.mul_sub_right_distrib, Nat.mul_comm]
    exact Nat.sub_le_sub_left _ <| (div_lt_iff_lt_mul npos).1 (lt_succ_self _)
  · show succ (pred (n * p - x)) ≤ (succ (pred (p - x / n))) * n
    rw [succ_pred_eq_of_pos (Nat.sub_pos_of_lt h₁),
      fun h => succ_pred_eq_of_pos (Nat.sub_pos_of_lt h)] -- TODO: why is the function needed?
    · rw [Nat.mul_sub_right_distrib, Nat.mul_comm]
      exact Nat.sub_le_sub_left _ <| div_mul_le_self ..
    · rwa [div_lt_iff_lt_mul npos, Nat.mul_comm]

protected theorem div_div_eq_div_mul (m n k : Nat) : m / n / k = m / (n * k) := by
  cases eq_zero_or_pos k with
  | inl k0 => rw [k0, Nat.mul_zero, Nat.div_zero, Nat.div_zero] | inr kpos => ?_
  cases eq_zero_or_pos n with
  | inl n0 => rw [n0, Nat.zero_mul, Nat.div_zero, Nat.zero_div] | inr npos => ?_
  apply Nat.le_antisymm
  · apply (le_div_iff_mul_le (Nat.mul_pos npos kpos)).2
    rw [Nat.mul_comm n k, ← Nat.mul_assoc]
    apply (le_div_iff_mul_le npos).1
    apply (le_div_iff_mul_le kpos).1
    (apply Nat.le_refl)
  · apply (le_div_iff_mul_le kpos).2
    apply (le_div_iff_mul_le npos).2
    rw [Nat.mul_assoc, Nat.mul_comm n k]
    apply (le_div_iff_mul_le (Nat.mul_pos kpos npos)).1
    apply Nat.le_refl

protected theorem mul_div_mul_left {m : Nat} (n k : Nat) (H : 0 < m) :
    m * n / (m * k) = n / k := by rw [← Nat.div_div_eq_div_mul, Nat.mul_div_cancel_left _ H]

protected theorem mul_div_mul_right {m : Nat} (n k : Nat) (H : 0 < m) :
    n * m / (k * m) = n / k := by rw [Nat.mul_comm, Nat.mul_comm k, Nat.mul_div_mul_left _ _ H]

theorem mul_div_le (m n : Nat) : n * (m / n) ≤ m := by
  match n, Nat.eq_zero_or_pos n with
  | _, Or.inl rfl => rw [Nat.zero_mul]; exact m.zero_le
  | n, Or.inr h => rw [Nat.mul_comm, ← Nat.le_div_iff_mul_le h]; exact Nat.le_refl _

/- dvd -/

protected theorem dvd_refl (a : Nat) : a ∣ a := ⟨1, by simp⟩

protected theorem dvd_zero (a : Nat) : a ∣ 0 := ⟨0, by simp⟩

protected theorem dvd_mul_left (a b : Nat) : a ∣ b * a := ⟨b, Nat.mul_comm b a⟩

protected theorem dvd_mul_right (a b : Nat) : a ∣ a * b := ⟨b, rfl⟩

protected theorem dvd_trans {a b c : Nat} (h₁ : a ∣ b) (h₂ : b ∣ c) : a ∣ c :=
  match h₁, h₂ with
  | ⟨d, (h₃ : b = a * d)⟩, ⟨e, (h₄ : c = b * e)⟩ =>
    ⟨d * e, show c = a * (d * e) by simp[h₃,h₄, Nat.mul_assoc]⟩

protected theorem eq_zero_of_zero_dvd {a : Nat} (h : 0 ∣ a) : a = 0 :=
  let ⟨c, H'⟩ := h; H'.trans c.zero_mul

protected theorem dvd_add {a b c : Nat} (h₁ : a ∣ b) (h₂ : a ∣ c) : a ∣ b + c :=
  let ⟨d, hd⟩ := h₁; let ⟨e, he⟩ := h₂; ⟨d + e, by simp [Nat.left_distrib, hd, he]⟩

protected theorem dvd_add_iff_right {k m n : Nat} (h : k ∣ m) : k ∣ n ↔ k ∣ m + n :=
  ⟨Nat.dvd_add h,
    match m, h with
    | _, ⟨d, rfl⟩ => fun ⟨e, he⟩ =>
      ⟨e - d, by rw [Nat.mul_sub_left_distrib, ← he, Nat.add_sub_cancel_left]⟩⟩

protected theorem dvd_add_iff_left {k m n : Nat} (h : k ∣ n) : k ∣ m ↔ k ∣ m + n := by
  rw [Nat.add_comm]; exact Nat.dvd_add_iff_right h

theorem dvd_sub {k m n : Nat} (H : n ≤ m) (h₁ : k ∣ m) (h₂ : k ∣ n) : k ∣ m - n :=
  (Nat.dvd_add_iff_left h₂).2 <| by rwa [Nat.sub_add_cancel H]

protected theorem mul_dvd_mul {a b c d : Nat} : a ∣ b → c ∣ d → a * c ∣ b * d
  | ⟨e, he⟩, ⟨f, hf⟩ =>
    ⟨e * f, by simp [he, hf, Nat.mul_assoc, Nat.mul_left_comm, Nat.mul_comm]⟩

protected theorem mul_dvd_mul_left (a : Nat) (h : b ∣ c) : a * b ∣ a * c :=
  Nat.mul_dvd_mul (Nat.dvd_refl a) h

protected theorem mul_dvd_mul_right (h: a ∣ b) (c : Nat) : a * c ∣ b * c :=
  Nat.mul_dvd_mul h (Nat.dvd_refl c)

theorem dvd_mod_iff {k m n : Nat} (h: k ∣ n) : k ∣ m % n ↔ k ∣ m :=
  have := Nat.dvd_add_iff_left <| Nat.dvd_trans h <| Nat.dvd_mul_right n (m / n)
  by rwa [mod_add_div] at this

theorem le_of_dvd {m n : Nat} (h : 0 < n) : m ∣ n → m ≤ n
  | ⟨k, e⟩ => by
    revert h
    rw [e]
    match k with
    | 0 => intro hn; simp at hn
    | pk+1 =>
      intro
      have := Nat.mul_le_mul_left m (succ_pos pk)
      rwa [Nat.mul_one] at this

theorem dvd_antisymm : ∀ {m n : Nat}, m ∣ n → n ∣ m → m = n
  | _, 0, _, h₂ => Nat.eq_zero_of_zero_dvd h₂
  | 0, _, h₁, _ => (Nat.eq_zero_of_zero_dvd h₁).symm
  | _+1, _+1, h₁, h₂ => Nat.le_antisymm (le_of_dvd (succ_pos _) h₁) (le_of_dvd (succ_pos _) h₂)

theorem pos_of_dvd_of_pos {m n : Nat} (H1 : m ∣ n) (H2 : 0 < n) : 0 < m :=
  Nat.pos_of_ne_zero fun m0 => Nat.ne_of_gt H2 <| Nat.eq_zero_of_zero_dvd (m0 ▸ H1)

theorem eq_one_of_dvd_one {n : Nat} (H : n ∣ 1) : n = 1 :=
  Nat.le_antisymm (le_of_dvd (by decide) H) (pos_of_dvd_of_pos H (by decide))

theorem dvd_of_mod_eq_zero {m n : Nat} (H : n % m = 0) : m ∣ n := by
  exists n / m
  have := (mod_add_div n m).symm
  rwa [H, Nat.zero_add] at this

theorem mod_eq_zero_of_dvd {m n : Nat} (H : m ∣ n) : n % m = 0 := by
  let ⟨z, H⟩ := H; rw [H, mul_mod_right]

theorem dvd_iff_mod_eq_zero (m n : Nat) : m ∣ n ↔ n % m = 0 :=
  ⟨mod_eq_zero_of_dvd, dvd_of_mod_eq_zero⟩

instance decidable_dvd : @DecidableRel Nat (·∣·) :=
  fun _ _ => decidable_of_decidable_of_iff (dvd_iff_mod_eq_zero _ _).symm

protected theorem mul_div_cancel' {n m : Nat} (H : n ∣ m) : n * (m / n) = m := by
  have := mod_add_div m n
  rwa [mod_eq_zero_of_dvd H, Nat.zero_add] at this

protected theorem div_mul_cancel {n m : Nat} (H : n ∣ m) : m / n * n = m := by
  rw [Nat.mul_comm, Nat.mul_div_cancel' H]

protected theorem mul_div_assoc (m : Nat) (H : k ∣ n) : m * n / k = m * (n / k) := by
  match Nat.eq_zero_or_pos k with
  | .inl h0 => rw [h0, Nat.div_zero, Nat.div_zero, Nat.mul_zero]
  | .inr hpos =>
    have h1 : m * n / k = m * (n / k * k) / k := by rw [Nat.div_mul_cancel H]
    rw [h1, ← Nat.mul_assoc, Nat.mul_div_cancel _ hpos]

protected theorem dvd_of_mul_dvd_mul_left
    (kpos : 0 < k) (H : k * m ∣ k * n) : m ∣ n := by
  let ⟨l, H⟩ := H
  rw [Nat.mul_assoc] at H
  exact ⟨_, Nat.eq_of_mul_eq_mul_left kpos H⟩

protected theorem dvd_of_mul_dvd_mul_right (kpos : 0 < k) (H : m * k ∣ n * k) : m ∣ n := by
  rw [Nat.mul_comm m k, Nat.mul_comm n k] at H; exact Nat.dvd_of_mul_dvd_mul_left kpos H

/- --- -/

protected theorem mul_le_mul_of_nonneg_left {a b c : Nat} (h₁ : a ≤ b) : c * a ≤ c * b := by
  if hba : b ≤ a then simp [Nat.le_antisymm hba h₁] else
  if hc0 : c ≤ 0 then simp [Nat.le_antisymm hc0 (zero_le c), Nat.zero_mul] else
  exact Nat.le_of_lt (Nat.mul_lt_mul_of_pos_left (Nat.not_le.1 hba) (Nat.not_le.1 hc0))

protected theorem mul_le_mul_of_nonneg_right {a b c : Nat} (h₁ : a ≤ b) : a * c ≤ b * c := by
  if hba : b ≤ a then simp [Nat.le_antisymm hba h₁] else
  if hc0 : c ≤ 0 then simp [Nat.le_antisymm hc0 (zero_le c), Nat.mul_zero] else
  exact Nat.le_of_lt (Nat.mul_lt_mul_of_pos_right (Nat.not_le.1 hba) (Nat.not_le.1 hc0))

protected theorem mul_lt_mul (hac : a < c) (hbd : b ≤ d) (pos_b : 0 < b) : a * b < c * d :=
  Nat.lt_of_lt_of_le (Nat.mul_lt_mul_of_pos_right hac pos_b) (Nat.mul_le_mul_of_nonneg_left hbd)

protected theorem mul_lt_mul' (h1 : a ≤ c) (h2 : b < d) (h3 : 0 < c) : a * b < c * d :=
  Nat.lt_of_le_of_lt (Nat.mul_le_mul_of_nonneg_right h1) (Nat.mul_lt_mul_of_pos_left h2 h3)

@[simp] theorem mod_mod (a n : Nat) : (a % n) % n = a % n :=
  match eq_zero_or_pos n with
  | .inl n0 => by simp [n0, mod_zero]
  | .inr npos => Nat.mod_eq_of_lt (mod_lt _ npos)

theorem mul_mod (a b n : Nat) : a * b % n = (a % n) * (b % n) % n := by
  conv => lhs; rw [
    ← mod_add_div a n, ← mod_add_div b n, Nat.add_mul, Nat.mul_add, Nat.mul_add,
    Nat.mul_assoc, Nat.mul_assoc, ← Nat.mul_add n, add_mul_mod_self_left,
    Nat.mul_comm _ (n * (b / n)), Nat.mul_assoc, add_mul_mod_self_left]

@[simp] theorem mod_add_mod (m n k : Nat) : (m % n + k) % n = (m + k) % n := by
  have := (add_mul_mod_self_left (m % n + k) n (m / n)).symm
  rwa [Nat.add_right_comm, mod_add_div] at this

@[simp] theorem add_mod_mod (m n k : Nat) : (m + n % k) % k = (m + n) % k := by
  rw [Nat.add_comm, mod_add_mod, Nat.add_comm]

theorem add_mod (a b n : Nat) : (a + b) % n = ((a % n) + (b % n)) % n := by
  rw [add_mod_mod, mod_add_mod]

theorem pow_succ' {m n : Nat} : m ^ n.succ = m * m ^ n := by
  rw [Nat.pow_succ, Nat.mul_comm]

@[simp] theorem pow_eq {m n : Nat} : m.pow n = m ^ n := rfl

@[simp] theorem shiftLeft_eq (a b : Nat) : a <<< b = a * 2 ^ b :=
  match b with
  | 0 => (Nat.mul_one _).symm
  | b+1 => (shiftLeft_eq _ b).trans <| by
    simp [pow_succ, Nat.mul_assoc, Nat.mul_left_comm, Nat.mul_comm]

theorem one_shiftLeft (n : Nat) : 1 <<< n = 2 ^ n := by rw [shiftLeft_eq, Nat.one_mul]

/-! ### log2 -/

attribute [simp] Nat.pow_zero

theorem le_log2 (h : n ≠ 0) : k ≤ n.log2 ↔ 2 ^ k ≤ n := by
  match k with
  | 0 => simp [show 1 ≤ n from Nat.pos_of_ne_zero h]
  | k+1 =>
    rw [log2]; split
    · have n0 : 0 < n / 2 := (Nat.le_div_iff_mul_le (by decide)).2 ‹_›
      simp [Nat.add_le_add_iff_le_right, le_log2 (Nat.ne_of_gt n0), le_div_iff_mul_le, Nat.pow_succ]
    · simp only [le_zero_eq, succ_ne_zero, false_iff]
      refine mt (Nat.le_trans ?_) ‹_›
      exact Nat.pow_le_pow_of_le_right (Nat.succ_pos 1) (Nat.le_add_left 1 k)

theorem log2_lt (h : n ≠ 0) : n.log2 < k ↔ n < 2 ^ k := by
  rw [← Nat.not_le, ← Nat.not_le, le_log2 h]

theorem log2_self_le (h : n ≠ 0) : 2 ^ n.log2 ≤ n := (le_log2 h).1 (Nat.le_refl _)

theorem lt_log2_self (h : n ≠ 0) : n < 2 ^ (n.log2 + 1) := (log2_lt h).1 (Nat.le_refl _)

/-! ### sum -/

@[simp] theorem sum_nil : Nat.sum [] = 0 := rfl
@[simp] theorem sum_cons : Nat.sum (a :: l) = a + Nat.sum l := rfl
@[simp] theorem sum_append : Nat.sum (l₁ ++ l₂) = Nat.sum l₁ + Nat.sum l₂ := by
  induction l₁ <;> simp [*, Nat.add_assoc]

author: leanprover