chore: add [ext] basic theorems, add test

and_intros and subst_eqs are not builtin

clarify failure modes

Clarify docString of extCore

clarify

chore: builtin `subst_eqs` tactic

chore: builtin `ext`

doc/examples/bintree.lean

@@ -282,7 +282,7 @@ theorem BinTree.find_insert_of_ne (b : BinTree β) (h : k ≠ k') (v : β)
   let ⟨t, h⟩ := b; simp
   induction t with simp
   | leaf =>
-    split <;> (try simp) <;> split <;> (try simp)
+    intros
     have_eq k k'
     contradiction
   | node left key value right ihl ihr =>

src/Init.lean

@@ -8,6 +8,7 @@ import Init.Prelude
 import Init.Notation
 import Init.Tactics
 import Init.TacticsExtra
+import Init.ByCases
 import Init.RCases
 import Init.Core
 import Init.Control
@@ -23,8 +24,11 @@ import Init.MetaTypes
 import Init.Meta
 import Init.NotationExtra
 import Init.SimpLemmas
+import Init.PropLemmas
 import Init.Hints
 import Init.Conv
 import Init.Guard
 import Init.Simproc
 import Init.SizeOfLemmas
+import Init.BinderPredicates
+import Init.Ext

src/Init/BinderPredicates.lean

@@ -0,0 +1,82 @@
+/-
+Copyright (c) 2021 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Gabriel Ebner
+-/
+prelude
+import Init.NotationExtra
+
+namespace Lean
+
+/--
+The syntax category of binder predicates contains predicates like `> 0`, `∈ s`, etc.
+(`: t` should not be a binder predicate because it would clash with the built-in syntax for ∀/∃.)
+-/
+declare_syntax_cat binderPred
+
+/--
+`satisfies_binder_pred% t pred` expands to a proposition expressing that `t` satisfies `pred`.
+-/
+syntax "satisfies_binder_pred% " term:max binderPred : term
+
+-- Extend ∀ and ∃ to binder predicates.
+
+/--
+The notation `∃ x < 2, p x` is shorthand for `∃ x, x < 2 ∧ p x`,
+and similarly for other binary operators.
+-/
+syntax "∃ " binderIdent binderPred ", " term : term
+/--
+The notation `∀ x < 2, p x` is shorthand for `∀ x, x < 2 → p x`,
+and similarly for other binary operators.
+-/
+syntax "∀ " binderIdent binderPred ", " term : term
+
+macro_rules
+  | `(∃ $x:ident $pred:binderPred, $p) =>
+    `(∃ $x:ident, satisfies_binder_pred% $x $pred ∧ $p)
+  | `(∃ _ $pred:binderPred, $p) =>
+    `(∃ x, satisfies_binder_pred% x $pred ∧ $p)
+
+macro_rules
+  | `(∀ $x:ident $pred:binderPred, $p) =>
+    `(∀ $x:ident, satisfies_binder_pred% $x $pred → $p)
+  | `(∀ _ $pred:binderPred, $p) =>
+    `(∀ x, satisfies_binder_pred% x $pred → $p)
+
+/-- Declare `∃ x > y, ...` as syntax for `∃ x, x > y ∧ ...` -/
+binder_predicate x " > " y:term => `($x > $y)
+/-- Declare `∃ x ≥ y, ...` as syntax for `∃ x, x ≥ y ∧ ...` -/
+binder_predicate x " ≥ " y:term => `($x ≥ $y)
+/-- Declare `∃ x < y, ...` as syntax for `∃ x, x < y ∧ ...` -/
+binder_predicate x " < " y:term => `($x < $y)
+/-- Declare `∃ x ≤ y, ...` as syntax for `∃ x, x ≤ y ∧ ...` -/
+binder_predicate x " ≤ " y:term => `($x ≤ $y)
+/-- Declare `∃ x ≠ y, ...` as syntax for `∃ x, x ≠ y ∧ ...` -/
+binder_predicate x " ≠ " y:term => `($x ≠ $y)
+
+/-- Declare `∀ x ∈ y, ...` as syntax for `∀ x, x ∈ y → ...` and `∃ x ∈ y, ...` as syntax for
+`∃ x, x ∈ y ∧ ...` -/
+binder_predicate x " ∈ " y:term => `($x ∈ $y)
+
+/-- Declare `∀ x ∉ y, ...` as syntax for `∀ x, x ∉ y → ...` and `∃ x ∉ y, ...` as syntax for
+`∃ x, x ∉ y ∧ ...` -/
+binder_predicate x " ∉ " y:term => `($x ∉ $y)
+
+/-- Declare `∀ x ⊆ y, ...` as syntax for `∀ x, x ⊆ y → ...` and `∃ x ⊆ y, ...` as syntax for
+`∃ x, x ⊆ y ∧ ...` -/
+binder_predicate x " ⊆ " y:term => `($x ⊆ $y)
+
+/-- Declare `∀ x ⊂ y, ...` as syntax for `∀ x, x ⊂ y → ...` and `∃ x ⊂ y, ...` as syntax for
+`∃ x, x ⊂ y ∧ ...` -/
+binder_predicate x " ⊂ " y:term => `($x ⊂ $y)
+
+/-- Declare `∀ x ⊇ y, ...` as syntax for `∀ x, x ⊇ y → ...` and `∃ x ⊇ y, ...` as syntax for
+`∃ x, x ⊇ y ∧ ...` -/
+binder_predicate x " ⊇ " y:term => `($x ⊇ $y)
+
+/-- Declare `∀ x ⊃ y, ...` as syntax for `∀ x, x ⊃ y → ...` and `∃ x ⊃ y, ...` as syntax for
+`∃ x, x ⊃ y ∧ ...` -/
+binder_predicate x " ⊃ " y:term => `($x ⊃ $y)
+
+end Lean

src/Init/ByCases.lean

@@ -0,0 +1,74 @@
+/-
+Copyright (c) 2024 Lean FRO. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura, Mario Carneiro
+-/
+prelude
+import Init.Classical
+
+/-! # by_cases tactic and if-then-else support -/
+
+/--
+`by_cases (h :)? p` splits the main goal into two cases, assuming `h : p` in the first branch, and `h : ¬ p` in the second branch.
+-/
+syntax "by_cases " (atomic(ident " : "))? term : tactic
+
+macro_rules
+  | `(tactic| by_cases $e) => `(tactic| by_cases h : $e)
+macro_rules
+  | `(tactic| by_cases $h : $e) =>
+    `(tactic| open Classical in refine if $h:ident : $e then ?pos else ?neg)
+
+/-! ## if-then-else -/
+
+@[simp] theorem if_true {h : Decidable True} (t e : α) : ite True t e = t := if_pos trivial
+
+@[simp] theorem if_false {h : Decidable False} (t e : α) : ite False t e = e := if_neg id
+
+theorem ite_id [Decidable c] {α} (t : α) : (if c then t else t) = t := by split <;> rfl
+
+/-- A function applied to a `dite` is a `dite` of that function applied to each of the branches. -/
+theorem apply_dite (f : α → β) (P : Prop) [Decidable P] (x : P → α) (y : ¬P → α) :
+    f (dite P x y) = dite P (fun h => f (x h)) (fun h => f (y h)) := by
+  by_cases h : P <;> simp [h]
+
+/-- A function applied to a `ite` is a `ite` of that function applied to each of the branches. -/
+theorem apply_ite (f : α → β) (P : Prop) [Decidable P] (x y : α) :
+    f (ite P x y) = ite P (f x) (f y) :=
+  apply_dite f P (fun _ => x) (fun _ => y)
+
+/-- Negation of the condition `P : Prop` in a `dite` is the same as swapping the branches. -/
+@[simp] theorem dite_not (P : Prop) {_ : Decidable P}  (x : ¬P → α) (y : ¬¬P → α) :
+    dite (¬P) x y = dite P (fun h => y (not_not_intro h)) x := by
+  by_cases h : P <;> simp [h]
+
+/-- Negation of the condition `P : Prop` in a `ite` is the same as swapping the branches. -/
+@[simp] theorem ite_not (P : Prop) {_ : Decidable P} (x y : α) : ite (¬P) x y = ite P y x :=
+  dite_not P (fun _ => x) (fun _ => y)
+
+@[simp] theorem dite_eq_left_iff {P : Prop} [Decidable P] {B : ¬ P → α} :
+    dite P (fun _ => a) B = a ↔ ∀ h, B h = a := by
+  by_cases P <;> simp [*, forall_prop_of_true, forall_prop_of_false]
+
+@[simp] theorem dite_eq_right_iff {P : Prop} [Decidable P] {A : P → α} :
+    (dite P A fun _ => b) = b ↔ ∀ h, A h = b := by
+  by_cases P <;> simp [*, forall_prop_of_true, forall_prop_of_false]
+
+@[simp] theorem ite_eq_left_iff {P : Prop} [Decidable P] : ite P a b = a ↔ ¬P → b = a :=
+  dite_eq_left_iff
+
+@[simp] theorem ite_eq_right_iff {P : Prop} [Decidable P] : ite P a b = b ↔ P → a = b :=
+  dite_eq_right_iff
+
+/-- A `dite` whose results do not actually depend on the condition may be reduced to an `ite`. -/
+@[simp] theorem dite_eq_ite [Decidable P] : (dite P (fun _ => a) fun _ => b) = ite P a b := rfl
+
+-- We don't mark this as `simp` as it is already handled by `ite_eq_right_iff`.
+theorem ite_some_none_eq_none [Decidable P] :
+    (if P then some x else none) = none ↔ ¬ P := by
+  simp only [ite_eq_right_iff]
+  rfl
+
+@[simp] theorem ite_some_none_eq_some [Decidable P] :
+    (if P then some x else none) = some y ↔ P ∧ x = y := by
+  split <;> simp_all

src/Init/Classical.lean

@@ -4,8 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura, Mario Carneiro
 -/
 prelude
-import Init.Core
-import Init.NotationExtra
+import Init.PropLemmas
 
 universe u v
 
@@ -112,8 +111,8 @@ theorem skolem {α : Sort u} {b : α → Sort v} {p : ∀ x, b x → Prop} : (
 
 theorem propComplete (a : Prop) : a = True ∨ a = False :=
   match em a with
-  | Or.inl ha => Or.inl (propext (Iff.intro (fun _ => ⟨⟩) (fun _ => ha)))
-  | Or.inr hn => Or.inr (propext (Iff.intro (fun h => hn h) (fun h => False.elim h)))
+  | Or.inl ha => Or.inl (eq_true ha)
+  | Or.inr hn => Or.inr (eq_false hn)
 
 -- this supercedes byCases in Decidable
 theorem byCases {p q : Prop} (hpq : p → q) (hnpq : ¬p → q) : q :=
@@ -123,15 +122,36 @@ theorem byCases {p q : Prop} (hpq : p → q) (hnpq : ¬p → q) : q :=
 theorem byContradiction {p : Prop} (h : ¬p → False) : p :=
   Decidable.byContradiction (dec := propDecidable _) h
 
+/-- The Double Negation Theorem: `¬¬P` is equivalent to `P`.
+The left-to-right direction, double negation elimination (DNE),
+is classically true but not constructively. -/
+@[scoped simp] theorem not_not : ¬¬a ↔ a := Decidable.not_not
+
+@[simp] theorem not_forall {p : α → Prop} : (¬∀ x, p x) ↔ ∃ x, ¬p x := Decidable.not_forall
+
+theorem not_forall_not {p : α → Prop} : (¬∀ x, ¬p x) ↔ ∃ x, p x := Decidable.not_forall_not
+theorem not_exists_not {p : α → Prop} : (¬∃ x, ¬p x) ↔ ∀ x, p x := Decidable.not_exists_not
+
+theorem forall_or_exists_not (P : α → Prop) : (∀ a, P a) ∨ ∃ a, ¬ P a := by
+  rw [← not_forall]; exact em _
+
+theorem exists_or_forall_not (P : α → Prop) : (∃ a, P a) ∨ ∀ a, ¬ P a := by
+  rw [← not_exists]; exact em _
+
+theorem or_iff_not_imp_left  : a ∨ b ↔ (¬a → b) := Decidable.or_iff_not_imp_left
+theorem or_iff_not_imp_right : a ∨ b ↔ (¬b → a) := Decidable.or_iff_not_imp_right
+
+theorem not_imp_iff_and_not : ¬(a → b) ↔ a ∧ ¬b := Decidable.not_imp_iff_and_not
+
+theorem not_and_iff_or_not_not : ¬(a ∧ b) ↔ ¬a ∨ ¬b := Decidable.not_and_iff_or_not_not
+
+theorem not_iff : ¬(a ↔ b) ↔ (¬a ↔ b) := Decidable.not_iff
+
 end Classical
 
-/--
-`by_cases (h :)? p` splits the main goal into two cases, assuming `h : p` in the first branch, and `h : ¬ p` in the second branch.
--/
-syntax "by_cases " (atomic(ident " : "))? term : tactic
+/-- Extract an element from a existential statement, using `Classical.choose`. -/
+-- This enables projection notation.
+@[reducible] noncomputable def Exists.choose {p : α → Prop} (P : ∃ a, p a) : α := Classical.choose P
 
-macro_rules
-  | `(tactic| by_cases $e) => `(tactic| by_cases h : $e)
-macro_rules
-  | `(tactic| by_cases $h : $e) =>
-    `(tactic| open Classical in refine if $h:ident : $e then ?pos else ?neg)
+/-- Show that an element extracted from `P : ∃ a, p a` using `P.choose` satisfies `p`. -/
+theorem Exists.choose_spec {p : α → Prop} (P : ∃ a, p a) : p P.choose := Classical.choose_spec P

src/Init/Control/Lawful.lean

@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2021 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Sebastian Ullrich, Leonardo de Moura
+Authors: Sebastian Ullrich, Leonardo de Moura, Mario Carneiro
 -/
 prelude
 import Init.SimpLemmas
@@ -84,6 +84,36 @@ theorem seqRight_eq_bind [Monad m] [LawfulMonad m] (x : m α) (y : m β) : x *>
 theorem seqLeft_eq_bind [Monad m] [LawfulMonad m] (x : m α) (y : m β) : x <* y = x >>= fun a => y >>= fun _ => pure a := by
   rw [seqLeft_eq]; simp [map_eq_pure_bind, seq_eq_bind_map]
 
+/--
+An alternative constructor for `LawfulMonad` which has more
+defaultable fields in the common case.
+-/
+theorem LawfulMonad.mk' (m : Type u → Type v) [Monad m]
+    (id_map : ∀ {α} (x : m α), id <$> x = x)
+    (pure_bind : ∀ {α β} (x : α) (f : α → m β), pure x >>= f = f x)
+    (bind_assoc : ∀ {α β γ} (x : m α) (f : α → m β) (g : β → m γ),
+      x >>= f >>= g = x >>= fun x => f x >>= g)
+    (map_const : ∀ {α β} (x : α) (y : m β),
+      Functor.mapConst x y = Function.const β x <$> y := by intros; rfl)
+    (seqLeft_eq : ∀ {α β} (x : m α) (y : m β),
+      x <* y = (x >>= fun a => y >>= fun _ => pure a) := by intros; rfl)
+    (seqRight_eq : ∀ {α β} (x : m α) (y : m β), x *> y = (x >>= fun _ => y) := by intros; rfl)
+    (bind_pure_comp : ∀ {α β} (f : α → β) (x : m α),
+      x >>= (fun y => pure (f y)) = f <$> x := by intros; rfl)
+    (bind_map : ∀ {α β} (f : m (α → β)) (x : m α), f >>= (. <$> x) = f <*> x := by intros; rfl)
+    : LawfulMonad m :=
+  have map_pure {α β} (g : α → β) (x : α) : g <$> (pure x : m α) = pure (g x) := by
+    rw [← bind_pure_comp]; simp [pure_bind]
+  { id_map, bind_pure_comp, bind_map, pure_bind, bind_assoc, map_pure,
+    comp_map := by simp [← bind_pure_comp, bind_assoc, pure_bind]
+    pure_seq := by intros; rw [← bind_map]; simp [pure_bind]
+    seq_pure := by intros; rw [← bind_map]; simp [map_pure, bind_pure_comp]
+    seq_assoc := by simp [← bind_pure_comp, ← bind_map, bind_assoc, pure_bind]
+    map_const := funext fun x => funext (map_const x)
+    seqLeft_eq := by simp [seqLeft_eq, ← bind_map, ← bind_pure_comp, pure_bind, bind_assoc]
+    seqRight_eq := fun x y => by
+      rw [seqRight_eq, ← bind_map, ← bind_pure_comp, bind_assoc]; simp [pure_bind, id_map] }
+
 /-! # Id -/
 
 namespace Id
@@ -173,6 +203,16 @@ instance [Monad m] [LawfulMonad m] : LawfulMonad (ExceptT ε m) where
 
 end ExceptT
 
+/-! # Except -/
+
+instance : LawfulMonad (Except ε) := LawfulMonad.mk'
+  (id_map := fun x => by cases x <;> rfl)
+  (pure_bind := fun a f => rfl)
+  (bind_assoc := fun a f g => by cases a <;> rfl)
+
+instance : LawfulApplicative (Except ε) := inferInstance
+instance : LawfulFunctor (Except ε) := inferInstance
+
 /-! # ReaderT -/
 
 namespace ReaderT
@@ -307,3 +347,30 @@ instance [Monad m] [LawfulMonad m] : LawfulMonad (StateT σ m) where
   bind_assoc     := by intros; apply ext; intros; simp
 
 end StateT
+
+/-! # EStateM -/
+
+instance : LawfulMonad (EStateM ε σ) := .mk'
+  (id_map := fun x => funext <| fun s => by
+    dsimp only [EStateM.instMonadEStateM, EStateM.map]
+    match x s with
+    | .ok _ _ => rfl
+    | .error _ _ => rfl)
+  (pure_bind := fun _ _ => rfl)
+  (bind_assoc := fun x _ _ => funext <| fun s => by
+    dsimp only [EStateM.instMonadEStateM, EStateM.bind]
+    match x s with
+    | .ok _ _ => rfl
+    | .error _ _ => rfl)
+  (map_const := fun _ _ => rfl)
+
+/-! # Option -/
+
+instance : LawfulMonad Option := LawfulMonad.mk'
+  (id_map := fun x => by cases x <;> rfl)
+  (pure_bind := fun x f => rfl)
+  (bind_assoc := fun x f g => by cases x <;> rfl)
+  (bind_pure_comp := fun f x => by cases x <;> rfl)
+
+instance : LawfulApplicative Option := inferInstance
+instance : LawfulFunctor Option := inferInstance

src/Init/Core.lean

@@ -17,7 +17,9 @@ universe u v w
 at the application site itself (by comparison to the `@[inline]` attribute,
 which applies to all applications of the function).
 -/
-def inline {α : Sort u} (a : α) : α := a
+@[simp] def inline {α : Sort u} (a : α) : α := a
+
+theorem id.def {α : Sort u} (a : α) : id a = a := rfl
 
 /--
 `flip f a b` is `f b a`. It is useful for "point-free" programming,
@@ -32,8 +34,32 @@ and `flip (·<·)` is the greater-than relation.
 
 @[simp] theorem Function.comp_apply {f : β → δ} {g : α → β} {x : α} : comp f g x = f (g x) := rfl
 
+theorem Function.comp_def {α β δ} (f : β → δ) (g : α → β) : f ∘ g = fun x => f (g x) := rfl
+
 attribute [simp] namedPattern
 
+/--
+`Empty.elim : Empty → C` says that a value of any type can be constructed from
+`Empty`. This can be thought of as a compiler-checked assertion that a code path is unreachable.
+
+This is a non-dependent variant of `Empty.rec`.
+-/
+@[macro_inline] def Empty.elim {C : Sort u} : Empty → C := Empty.rec
+
+/-- Decidable equality for Empty -/
+instance : DecidableEq Empty := fun a => a.elim
+
+/--
+`PEmpty.elim : Empty → C` says that a value of any type can be constructed from
+`PEmpty`. This can be thought of as a compiler-checked assertion that a code path is unreachable.
+
+This is a non-dependent variant of `PEmpty.rec`.
+-/
+@[macro_inline] def PEmpty.elim {C : Sort _} : PEmpty → C := fun a => nomatch a
+
+/-- Decidable equality for PEmpty -/
+instance : DecidableEq PEmpty := fun a => a.elim
+
 /--
   Thunks are "lazy" values that are evaluated when first accessed using `Thunk.get/map/bind`.
   The value is then stored and not recomputed for all further accesses. -/
@@ -78,6 +104,8 @@ instance thunkCoe : CoeTail α (Thunk α) where
 abbrev Eq.ndrecOn.{u1, u2} {α : Sort u2} {a : α} {motive : α → Sort u1} {b : α} (h : a = b) (m : motive a) : motive b :=
   Eq.ndrec m h
 
+/-! # definitions  -/
+
 /--
 If and only if, or logical bi-implication. `a ↔ b` means that `a` implies `b` and vice versa.
 By `propext`, this implies that `a` and `b` are equal and hence any expression involving `a`
@@ -126,6 +154,10 @@ inductive PSum (α : Sort u) (β : Sort v) where
 
 @[inherit_doc] infixr:30 " ⊕' " => PSum
 
+instance {α β} [Inhabited α] : Inhabited (PSum α β) := ⟨PSum.inl default⟩
+
+instance {α β} [Inhabited β] : Inhabited (PSum α β) := ⟨PSum.inr default⟩
+
 /--
 `Sigma β`, also denoted `Σ a : α, β a` or `(a : α) × β a`, is the type of dependent pairs
 whose first component is `a : α` and whose second component is `b : β a`
@@ -342,6 +374,70 @@ class HasEquiv (α : Sort u) where
 
 @[inherit_doc] infix:50 " ≈ "  => HasEquiv.Equiv
 
+/-! # set notation  -/
+
+/-- Notation type class for the subset relation `⊆`. -/
+class HasSubset (α : Type u) where
+  /-- Subset relation: `a ⊆ b`  -/
+  Subset : α → α → Prop
+export HasSubset (Subset)
+
+/-- Notation type class for the strict subset relation `⊂`. -/
+class HasSSubset (α : Type u) where
+  /-- Strict subset relation: `a ⊂ b`  -/
+  SSubset : α → α → Prop
+export HasSSubset (SSubset)
+
+/-- Superset relation: `a ⊇ b`  -/
+abbrev Superset [HasSubset α] (a b : α) := Subset b a
+
+/-- Strict superset relation: `a ⊃ b`  -/
+abbrev SSuperset [HasSSubset α] (a b : α) := SSubset b a
+
+/-- Notation type class for the union operation `∪`. -/
+class Union (α : Type u) where
+  /-- `a ∪ b` is the union of`a` and `b`. -/
+  union : α → α → α
+
+/-- Notation type class for the intersection operation `∩`. -/
+class Inter (α : Type u) where
+  /-- `a ∩ b` is the intersection of`a` and `b`. -/
+  inter : α → α → α
+
+/-- Notation type class for the set difference `\`. -/
+class SDiff (α : Type u) where
+  /--
+  `a \ b` is the set difference of `a` and `b`,
+  consisting of all elements in `a` that are not in `b`.
+  -/
+  sdiff : α → α → α
+
+/-- Subset relation: `a ⊆ b`  -/
+infix:50 " ⊆ " => Subset
+
+/-- Strict subset relation: `a ⊂ b`  -/
+infix:50 " ⊂ " => SSubset
+
+/-- Superset relation: `a ⊇ b`  -/
+infix:50 " ⊇ " => Superset
+
+/-- Strict superset relation: `a ⊃ b`  -/
+infix:50 " ⊃ " => SSuperset
+
+/-- `a ∪ b` is the union of`a` and `b`. -/
+infixl:65 " ∪ " => Union.union
+
+/-- `a ∩ b` is the intersection of`a` and `b`. -/
+infixl:70 " ∩ " => Inter.inter
+
+/--
+`a \ b` is the set difference of `a` and `b`,
+consisting of all elements in `a` that are not in `b`.
+-/
+infix:70 " \\ " => SDiff.sdiff
+
+/-! # collections  -/
+
 /-- `EmptyCollection α` is the typeclass which supports the notation `∅`, also written as `{}`. -/
 class EmptyCollection (α : Type u) where
   /-- `∅` or `{}` is the empty set or empty collection.
@@ -351,6 +447,36 @@ class EmptyCollection (α : Type u) where
 @[inherit_doc] notation "{" "}" => EmptyCollection.emptyCollection
 @[inherit_doc] notation "∅"     => EmptyCollection.emptyCollection
 
+/--
+Type class for the `insert` operation.
+Used to implement the `{ a, b, c }` syntax.
+-/
+class Insert (α : outParam <| Type u) (γ : Type v) where
+  /-- `insert x xs` inserts the element `x` into the collection `xs`. -/
+  insert : α → γ → γ
+export Insert (insert)
+
+/--
+Type class for the `singleton` operation.
+Used to implement the `{ a, b, c }` syntax.
+-/
+class Singleton (α : outParam <| Type u) (β : Type v) where
+  /-- `singleton x` is a collection with the single element `x` (notation: `{x}`). -/
+  singleton : α → β
+export Singleton (singleton)
+
+/-- `insert x ∅ = {x}` -/
+class IsLawfulSingleton (α : Type u) (β : Type v) [EmptyCollection β] [Insert α β] [Singleton α β] :
+    Prop where
+  /-- `insert x ∅ = {x}` -/
+  insert_emptyc_eq (x : α) : (insert x ∅ : β) = singleton x
+export IsLawfulSingleton (insert_emptyc_eq)
+
+/-- Type class used to implement the notation `{ a ∈ c | p a }` -/
+class Sep (α : outParam <| Type u) (γ : Type v) where
+  /-- Computes `{ a ∈ c | p a }`. -/
+  sep : (α → Prop) → γ → γ
+
 /--
 `Task α` is a primitive for asynchronous computation.
 It represents a computation that will resolve to a value of type `α`,
@@ -525,9 +651,7 @@ theorem not_not_intro {p : Prop} (h : p) : ¬ ¬ p :=
   fun hn : ¬ p => hn h
 
 -- proof irrelevance is built in
-theorem proofIrrel {a : Prop} (h₁ h₂ : a) : h₁ = h₂ := rfl
-
-theorem id.def {α : Sort u} (a : α) : id a = a := rfl
+theorem proof_irrel {a : Prop} (h₁ h₂ : a) : h₁ = h₂ := rfl
 
 /--
 If `h : α = β` is a proof of type equality, then `h.mp : α → β` is the induced
@@ -575,8 +699,9 @@ theorem Ne.elim (h : a ≠ b) : a = b → False := h
 
 theorem Ne.irrefl (h : a ≠ a) : False := h rfl
 
-theorem Ne.symm (h : a ≠ b) : b ≠ a :=
-  fun h₁ => h (h₁.symm)
+theorem Ne.symm (h : a ≠ b) : b ≠ a := fun h₁ => h (h₁.symm)
+
+theorem ne_comm {α} {a b : α} : a ≠ b ↔ b ≠ a := ⟨Ne.symm, Ne.symm⟩
 
 theorem false_of_ne : a ≠ a → False := Ne.irrefl
 
@@ -588,8 +713,8 @@ theorem ne_true_of_not : ¬p → p ≠ True :=
     have : ¬True := h ▸ hnp
     this trivial
 
-theorem true_ne_false : ¬True = False :=
-  ne_false_of_self trivial
+theorem true_ne_false : ¬True = False := ne_false_of_self trivial
+theorem false_ne_true : False ≠ True := fun h => h.symm ▸ trivial
 
 end Ne
 
@@ -668,22 +793,29 @@ protected theorem Iff.rfl {a : Prop} : a ↔ a :=
 
 macro_rules | `(tactic| rfl) => `(tactic| exact Iff.rfl)
 
+theorem Iff.of_eq (h : a = b) : a ↔ b := h ▸ Iff.rfl
+
 theorem Iff.trans (h₁ : a ↔ b) (h₂ : b ↔ c) : a ↔ c :=
-  Iff.intro
-    (fun ha => Iff.mp h₂ (Iff.mp h₁ ha))
-    (fun hc => Iff.mpr h₁ (Iff.mpr h₂ hc))
+  Iff.intro (h₂.mp ∘ h₁.mp) (h₁.mpr ∘ h₂.mpr)
 
-theorem Iff.symm (h : a ↔ b) : b ↔ a :=
-  Iff.intro (Iff.mpr h) (Iff.mp h)
+-- This is needed for `calc` to work with `iff`.
+instance : Trans Iff Iff Iff where
+  trans := Iff.trans
 
-theorem Iff.comm : (a ↔ b) ↔ (b ↔ a) :=
-  Iff.intro Iff.symm Iff.symm
+theorem Eq.comm {a b : α} : a = b ↔ b = a := Iff.intro Eq.symm Eq.symm
+theorem eq_comm {a b : α} : a = b ↔ b = a := Eq.comm
 
-theorem Iff.of_eq (h : a = b) : a ↔ b :=
-  h ▸ Iff.refl _
+theorem Iff.symm (h : a ↔ b) : b ↔ a := Iff.intro h.mpr h.mp
+theorem Iff.comm: (a ↔ b) ↔ (b ↔ a) := Iff.intro Iff.symm Iff.symm
+theorem iff_comm : (a ↔ b) ↔ (b ↔ a) := Iff.comm
 
-theorem And.comm : a ∧ b ↔ b ∧ a := by
-  constructor <;> intro ⟨h₁, h₂⟩ <;> exact ⟨h₂, h₁⟩
+theorem And.symm : a ∧ b → b ∧ a := fun ⟨ha, hb⟩ => ⟨hb, ha⟩
+theorem And.comm : a ∧ b ↔ b ∧ a := Iff.intro And.symm And.symm
+theorem and_comm : a ∧ b ↔ b ∧ a := And.comm
+
+theorem Or.symm : a ∨ b → b ∨ a := .rec .inr .inl
+theorem Or.comm : a ∨ b ↔ b ∨ a := Iff.intro Or.symm Or.symm
+theorem or_comm : a ∨ b ↔ b ∨ a := Or.comm
 
 /-! # Exists -/
 
@@ -883,8 +1015,13 @@ protected theorem Subsingleton.helim {α β : Sort u} [h₁ : Subsingleton α] (
   apply heq_of_eq
   apply Subsingleton.elim
 
-instance (p : Prop) : Subsingleton p :=
-  ⟨fun a b => proofIrrel a b⟩
+instance (p : Prop) : Subsingleton p := ⟨fun a b => proof_irrel a b⟩
+
+instance : Subsingleton Empty  := ⟨(·.elim)⟩
+instance : Subsingleton PEmpty := ⟨(·.elim)⟩
+
+instance [Subsingleton α] [Subsingleton β] : Subsingleton (α × β) :=
+  ⟨fun {..} {..} => by congr <;> apply Subsingleton.elim⟩
 
 instance (p : Prop) : Subsingleton (Decidable p) :=
   Subsingleton.intro fun
@@ -895,6 +1032,9 @@ instance (p : Prop) : Subsingleton (Decidable p) :=
       | isTrue t₂  => absurd t₂ f₁
       | isFalse _  => rfl
 
+example [Subsingleton α] (p : α → Prop) : Subsingleton (Subtype p) :=
+  ⟨fun ⟨x, _⟩ ⟨y, _⟩ => by congr; exact Subsingleton.elim x y⟩
+
 theorem recSubsingleton
      {p : Prop} [h : Decidable p]
      {h₁ : p → Sort u}
@@ -1174,12 +1314,117 @@ gen_injective_theorems% Lean.Syntax
 @[simp] theorem beq_iff_eq [BEq α] [LawfulBEq α] (a b : α) : a == b ↔ a = b :=
   ⟨eq_of_beq, by intro h; subst h; exact LawfulBEq.rfl⟩
 
-/-! # Quotients -/
+/-! # Prop lemmas -/
+
+/-- *Ex falso* for negation: from `¬a` and `a` anything follows. This is the same as `absurd` with
+the arguments flipped, but it is in the `Not` namespace so that projection notation can be used. -/
+def Not.elim {α : Sort _} (H1 : ¬a) (H2 : a) : α := absurd H2 H1
+
+/-- Non-dependent eliminator for `And`. -/
+abbrev And.elim (f : a → b → α) (h : a ∧ b) : α := f h.left h.right
+
+/-- Non-dependent eliminator for `Iff`. -/
+def Iff.elim (f : (a → b) → (b → a) → α) (h : a ↔ b) : α := f h.mp h.mpr
 
 /-- Iff can now be used to do substitutions in a calculation -/
 theorem Iff.subst {a b : Prop} {p : Prop → Prop} (h₁ : a ↔ b) (h₂ : p a) : p b :=
   Eq.subst (propext h₁) h₂
 
+theorem Not.intro {a : Prop} (h : a → False) : ¬a := h
+
+theorem Not.imp {a b : Prop} (H2 : ¬b) (H1 : a → b) : ¬a := mt H1 H2
+
+theorem not_congr (h : a ↔ b) : ¬a ↔ ¬b := ⟨mt h.2, mt h.1⟩
+
+theorem not_not_not : ¬¬¬a ↔ ¬a := ⟨mt not_not_intro, not_not_intro⟩
+
+theorem iff_of_true (ha : a) (hb : b) : a ↔ b := Iff.intro (fun _ => hb) (fun _ => ha)
+theorem iff_of_false (ha : ¬a) (hb : ¬b) : a ↔ b := Iff.intro ha.elim hb.elim
+
+theorem iff_true_left  (ha : a) : (a ↔ b) ↔ b := Iff.intro (·.mp ha) (iff_of_true ha)
+theorem iff_true_right (ha : a) : (b ↔ a) ↔ b := Iff.comm.trans (iff_true_left ha)
+
+theorem iff_false_left  (ha : ¬a) : (a ↔ b) ↔ ¬b := Iff.intro (mt ·.mpr ha) (iff_of_false ha)
+theorem iff_false_right (ha : ¬a) : (b ↔ a) ↔ ¬b := Iff.comm.trans (iff_false_left ha)
+
+theorem of_iff_true    (h : a ↔ True) : a := h.mpr trivial
+theorem iff_true_intro (h : a) : a ↔ True := iff_of_true h trivial
+
+theorem not_of_iff_false : (p ↔ False) → ¬p := Iff.mp
+theorem iff_false_intro (h : ¬a) : a ↔ False := iff_of_false h id
+
+theorem not_iff_false_intro (h : a) : ¬a ↔ False := iff_false_intro (not_not_intro h)
+theorem not_true : (¬True) ↔ False := iff_false_intro (not_not_intro trivial)
+
+theorem not_false_iff : (¬False) ↔ True := iff_true_intro not_false
+
+theorem Eq.to_iff : a = b → (a ↔ b) := Iff.of_eq
+theorem iff_of_eq : a = b → (a ↔ b) := Iff.of_eq
+theorem neq_of_not_iff : ¬(a ↔ b) → a ≠ b := mt Iff.of_eq
+
+theorem iff_iff_eq : (a ↔ b) ↔ a = b := Iff.intro propext Iff.of_eq
+@[simp] theorem eq_iff_iff : (a = b) ↔ (a ↔ b) := iff_iff_eq.symm
+
+theorem eq_self_iff_true (a : α)  : a = a ↔ True  := iff_true_intro rfl
+theorem ne_self_iff_false (a : α) : a ≠ a ↔ False := not_iff_false_intro rfl
+
+theorem false_of_true_iff_false (h : True ↔ False) : False := h.mp trivial
+theorem false_of_true_eq_false  (h : True = False) : False := false_of_true_iff_false (Iff.of_eq h)
+
+theorem true_eq_false_of_false : False → (True = False) := False.elim
+
+theorem iff_def  : (a ↔ b) ↔ (a → b) ∧ (b → a) := iff_iff_implies_and_implies a b
+theorem iff_def' : (a ↔ b) ↔ (b → a) ∧ (a → b) := Iff.trans iff_def And.comm
+
+theorem true_iff_false : (True ↔ False) ↔ False := iff_false_intro (·.mp  True.intro)
+theorem false_iff_true : (False ↔ True) ↔ False := iff_false_intro (·.mpr True.intro)
+
+theorem iff_not_self : ¬(a ↔ ¬a) | H => let f h := H.1 h h; f (H.2 f)
+theorem heq_self_iff_true (a : α) : HEq a a ↔ True := iff_true_intro HEq.rfl
+
+/-! ## implies -/
+
+theorem not_not_of_not_imp : ¬(a → b) → ¬¬a := mt Not.elim
+
+theorem not_of_not_imp {a : Prop} : ¬(a → b) → ¬b := mt fun h _ => h
+
+@[simp] theorem imp_not_self : (a → ¬a) ↔ ¬a := Iff.intro (fun h ha => h ha ha) (fun h _ => h)
+
+theorem imp_intro {α β : Prop} (h : α) : β → α := fun _ => h
+
+theorem imp_imp_imp {a b c d : Prop} (h₀ : c → a) (h₁ : b → d) : (a → b) → (c → d) := (h₁ ∘ · ∘ h₀)
+
+theorem imp_iff_right {a : Prop} (ha : a) : (a → b) ↔ b := Iff.intro (· ha) (fun a _ => a)
+
+-- This is not marked `@[simp]` because we have `implies_true : (α → True) = True`
+theorem imp_true_iff (α : Sort u) : (α → True) ↔ True := iff_true_intro (fun _ => trivial)
+
+theorem false_imp_iff (a : Prop) : (False → a) ↔ True := iff_true_intro False.elim
+
+theorem true_imp_iff (α : Prop) : (True → α) ↔ α := imp_iff_right True.intro
+
+@[simp] theorem imp_self : (a → a) ↔ True := iff_true_intro id
+
+theorem imp_false : (a → False) ↔ ¬a := Iff.rfl
+
+theorem imp.swap : (a → b → c) ↔ (b → a → c) := Iff.intro flip flip
+
+theorem imp_not_comm : (a → ¬b) ↔ (b → ¬a) := imp.swap
+
+theorem imp_congr_left (h : a ↔ b) : (a → c) ↔ (b → c) := Iff.intro (· ∘ h.mpr) (· ∘ h.mp)
+
+theorem imp_congr_right (h : a → (b ↔ c)) : (a → b) ↔ (a → c) :=
+  Iff.intro (fun hab ha => (h ha).mp (hab ha)) (fun hcd ha => (h ha).mpr (hcd ha))
+
+theorem imp_congr_ctx (h₁ : a ↔ c) (h₂ : c → (b ↔ d)) : (a → b) ↔ (c → d) :=
+  Iff.trans (imp_congr_left h₁) (imp_congr_right h₂)
+
+theorem imp_congr (h₁ : a ↔ c) (h₂ : b ↔ d) : (a → b) ↔ (c → d) := imp_congr_ctx h₁ fun _ => h₂
+
+theorem imp_iff_not (hb : ¬b) : a → b ↔ ¬a := imp_congr_right fun _ => iff_false_intro hb
+
+/-! # Quotients -/
+
 namespace Quot
 /--
 The **quotient axiom**, or at least the nontrivial part of the quotient

src/Init/Data/Array/DecidableEq.lean

@@ -5,7 +5,7 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Init.Data.Array.Basic
-import Init.Classical
+import Init.ByCases
 
 namespace Array
 

src/Init/Data/Fin/Basic.lean

@@ -106,6 +106,8 @@ instance instOfNat : OfNat (Fin (no_index (n+1))) i where
 instance : Inhabited (Fin (no_index (n+1))) where
   default := 0
 
+@[simp] theorem zero_eta : (⟨0, Nat.zero_lt_succ _⟩ : Fin (n + 1)) = 0 := rfl
+
 theorem val_ne_of_ne {i j : Fin n} (h : i ≠ j) : val i ≠ val j :=
   fun h' => absurd (eq_of_val_eq h') h
 

src/Init/Data/List/Basic.lean

@@ -603,6 +603,27 @@ The longer list is truncated to match the shorter list.
 def zip : List α → List β → List (Prod α β) :=
   zipWith Prod.mk
 
+/--
+`O(max |xs| |ys|)`.
+Version of `List.zipWith` that continues to the end of both lists,
+passing `none` to one argument once the shorter list has run out.
+-/
+def zipWithAll (f : Option α → Option β → γ) : List α → List β → List γ
+  | [], bs => bs.map fun b => f none (some b)
+  | a :: as, [] => (a :: as).map fun a => f (some a) none
+  | a :: as, b :: bs => f a b :: zipWithAll f as bs
+
+@[simp] theorem zipWithAll_nil_right :
+    zipWithAll f as [] = as.map fun a => f (some a) none := by
+  cases as <;> rfl
+
+@[simp] theorem zipWithAll_nil_left :
+    zipWithAll f [] bs = bs.map fun b => f none (some b) := by
+  rfl
+
+@[simp] theorem zipWithAll_cons_cons :
+    zipWithAll f (a :: as) (b :: bs) = f (some a) (some b) :: zipWithAll f as bs := rfl
+
 /--
 `O(|l|)`. Separates a list of pairs into two lists containing the first components and second components.
 * `unzip [(x₁, y₁), (x₂, y₂), (x₃, y₃)] = ([x₁, x₂, x₃], [y₁, y₂, y₃])`
@@ -876,7 +897,7 @@ instance [BEq α] [LawfulBEq α] : LawfulBEq (List α) where
       cases bs with
       | nil => intro h; contradiction
       | cons b bs =>
-        simp [show (a::as == b::bs) = (a == b && as == bs) from rfl]
+        simp [show (a::as == b::bs) = (a == b && as == bs) from rfl, -and_imp]
         intro ⟨h₁, h₂⟩
         exact ⟨h₁, ih h₂⟩
   rfl {as} := by

src/Init/Data/Nat.lean

@@ -6,7 +6,9 @@ Authors: Leonardo de Moura
 prelude
 import Init.Data.Nat.Basic
 import Init.Data.Nat.Div
+import Init.Data.Nat.Dvd
 import Init.Data.Nat.Gcd
+import Init.Data.Nat.MinMax
 import Init.Data.Nat.Bitwise
 import Init.Data.Nat.Control
 import Init.Data.Nat.Log2

src/Init/Data/Nat/Basic.lean

@@ -147,13 +147,20 @@ protected theorem add_right_comm (n m k : Nat) : (n + m) + k = (n + k) + m := by
 
 protected theorem add_left_cancel {n m k : Nat} : n + m = n + k → m = k := by
   induction n with
-  | zero => simp; intros; assumption
+  | zero => simp
   | succ n ih => simp [succ_add]; intro h; apply ih h
 
 protected theorem add_right_cancel {n m k : Nat} (h : n + m = k + m) : n = k := by
   rw [Nat.add_comm n m, Nat.add_comm k m] at h
   apply Nat.add_left_cancel h
 
+theorem eq_zero_of_add_eq_zero : ∀ {n m}, n + m = 0 → n = 0 ∧ m = 0
+  | 0, 0, _ => ⟨rfl, rfl⟩
+  | _+1, 0, h => Nat.noConfusion h
+
+protected theorem eq_zero_of_add_eq_zero_left (h : n + m = 0) : m = 0 :=
+  (Nat.eq_zero_of_add_eq_zero h).2
+
 /-! # Nat.mul theorems -/
 
 @[simp] protected theorem mul_zero (n : Nat) : n * 0 = 0 :=
@@ -206,16 +213,13 @@ protected theorem mul_left_comm (n m k : Nat) : n * (m * k) = m * (n * k) := by
 
 attribute [simp] Nat.le_refl
 
-theorem succ_lt_succ {n m : Nat} : n < m → succ n < succ m :=
-  succ_le_succ
+theorem succ_lt_succ {n m : Nat} : n < m → succ n < succ m := succ_le_succ
 
-theorem lt_succ_of_le {n m : Nat} : n ≤ m → n < succ m :=
-  succ_le_succ
+theorem lt_succ_of_le {n m : Nat} : n ≤ m → n < succ m := succ_le_succ
 
-@[simp] protected theorem sub_zero (n : Nat) : n - 0 = n :=
-  rfl
+@[simp] protected theorem sub_zero (n : Nat) : n - 0 = n := rfl
 
-theorem succ_sub_succ_eq_sub (n m : Nat) : succ n - succ m = n - m := by
+@[simp] theorem succ_sub_succ_eq_sub (n m : Nat) : succ n - succ m = n - m := by
   induction m with
   | zero      => exact rfl
   | succ m ih => apply congrArg pred ih
@@ -241,8 +245,7 @@ theorem sub_lt : ∀ {n m : Nat}, 0 < n → 0 < m → n - m < n
       show n - m < succ n from
       lt_succ_of_le (sub_le n m)
 
-theorem sub_succ (n m : Nat) : n - succ m = pred (n - m) :=
-  rfl
+theorem sub_succ (n m : Nat) : n - succ m = pred (n - m) := rfl
 
 theorem succ_sub_succ (n m : Nat) : succ n - succ m = n - m :=
   succ_sub_succ_eq_sub n m
@@ -277,20 +280,24 @@ instance : Trans (. ≤ . : Nat → Nat → Prop) (. < . : Nat → Nat → Prop)
 protected theorem le_of_eq {n m : Nat} (p : n = m) : n ≤ m :=
   p ▸ Nat.le_refl n
 
-theorem le_of_succ_le {n m : Nat} (h : succ n ≤ m) : n ≤ m :=
-  Nat.le_trans (le_succ n) h
-
-protected theorem le_of_lt {n m : Nat} (h : n < m) : n ≤ m :=
-  le_of_succ_le h
-
 theorem lt.step {n m : Nat} : n < m → n < succ m := le_step
 
+theorem le_of_succ_le {n m : Nat} (h : succ n ≤ m) : n ≤ m := Nat.le_trans (le_succ n) h
+theorem lt_of_succ_lt      {n m : Nat} : succ n < m → n < m := le_of_succ_le
+protected theorem le_of_lt {n m : Nat} : n < m → n ≤ m := le_of_succ_le
+
+theorem lt_of_succ_lt_succ {n m : Nat} : succ n < succ m → n < m := le_of_succ_le_succ
+
+theorem lt_of_succ_le {n m : Nat} (h : succ n ≤ m) : n < m := h
+theorem succ_le_of_lt {n m : Nat} (h : n < m) : succ n ≤ m := h
+
 theorem eq_zero_or_pos : ∀ (n : Nat), n = 0 ∨ n > 0
   | 0   => Or.inl rfl
   | _+1 => Or.inr (succ_pos _)
 
-theorem lt.base (n : Nat) : n < succ n := Nat.le_refl (succ n)
+protected theorem pos_of_ne_zero {n : Nat} : n ≠ 0 → 0 < n := (eq_zero_or_pos n).resolve_left
 
+theorem lt.base (n : Nat) : n < succ n := Nat.le_refl (succ n)
 theorem lt_succ_self (n : Nat) : n < succ n := lt.base n
 
 protected theorem le_total (m n : Nat) : m ≤ n ∨ n ≤ m :=
@@ -298,20 +305,7 @@ protected theorem le_total (m n : Nat) : m ≤ n ∨ n ≤ m :=
   | Or.inl h => Or.inl (Nat.le_of_lt h)
   | Or.inr h => Or.inr h
 
-theorem eq_zero_of_le_zero {n : Nat} (h : n ≤ 0) : n = 0 :=
-  Nat.le_antisymm h (zero_le _)
-
-theorem lt_of_succ_lt {n m : Nat} : succ n < m → n < m :=
-  le_of_succ_le
-
-theorem lt_of_succ_lt_succ {n m : Nat} : succ n < succ m → n < m :=
-  le_of_succ_le_succ
-
-theorem lt_of_succ_le {n m : Nat} (h : succ n ≤ m) : n < m :=
-  h
-
-theorem succ_le_of_lt {n m : Nat} (h : n < m) : succ n ≤ m :=
-  h
+theorem eq_zero_of_le_zero {n : Nat} (h : n ≤ 0) : n = 0 := Nat.le_antisymm h (zero_le _)
 
 theorem zero_lt_of_lt : {a b : Nat} → a < b → 0 < b
   | 0,   _, h => h
@@ -326,8 +320,7 @@ theorem zero_lt_of_ne_zero {a : Nat} (h : a ≠ 0) : 0 < a := by
 
 attribute [simp] Nat.lt_irrefl
 
-theorem ne_of_lt {a b : Nat} (h : a < b) : a ≠ b :=
-  fun he => absurd (he ▸ h) (Nat.lt_irrefl a)
+theorem ne_of_lt {a b : Nat} (h : a < b) : a ≠ b := fun he => absurd (he ▸ h) (Nat.lt_irrefl a)
 
 theorem le_or_eq_of_le_succ {m n : Nat} (h : m ≤ succ n) : m ≤ n ∨ m = succ n :=
   Decidable.byCases
@@ -363,16 +356,51 @@ protected theorem not_le_of_gt {n m : Nat} (h : n > m) : ¬ n ≤ m := fun h₁
   | Or.inr h₂ =>
     have Heq : n = m := Nat.le_antisymm h₁ h₂
     absurd (@Eq.subst _ _ _ _ Heq h) (Nat.lt_irrefl m)
+protected theorem not_le_of_lt : ∀{a b : Nat}, a < b → ¬(b ≤ a) := Nat.not_le_of_gt
+protected theorem not_lt_of_ge : ∀{a b : Nat}, b ≥ a → ¬(b < a) := flip Nat.not_le_of_gt
+protected theorem not_lt_of_le : ∀{a b : Nat}, a ≤ b → ¬(b < a) := flip Nat.not_le_of_gt
+protected theorem lt_le_asymm : ∀{a b : Nat}, a < b → ¬(b ≤ a) := Nat.not_le_of_gt
+protected theorem le_lt_asymm : ∀{a b : Nat}, a ≤ b → ¬(b < a) := flip Nat.not_le_of_gt
 
-theorem gt_of_not_le {n m : Nat} (h : ¬ n ≤ m) : n > m :=
-  match Nat.lt_or_ge m n with
-  | Or.inl h₁ => h₁
-  | Or.inr h₁ => absurd h₁ h
+theorem gt_of_not_le {n m : Nat} (h : ¬ n ≤ m) : n > m := (Nat.lt_or_ge m n).resolve_right h
+protected theorem lt_of_not_ge : ∀{a b : Nat}, ¬(b ≥ a) → b < a := Nat.gt_of_not_le
+protected theorem lt_of_not_le : ∀{a b : Nat}, ¬(a ≤ b) → b < a := Nat.gt_of_not_le
 
-theorem ge_of_not_lt {n m : Nat} (h : ¬ n < m) : n ≥ m :=
-  match Nat.lt_or_ge n m with
-  | Or.inl h₁ => absurd h₁ h
-  | Or.inr h₁ => h₁
+theorem ge_of_not_lt {n m : Nat} (h : ¬ n < m) : n ≥ m := (Nat.lt_or_ge n m).resolve_left h
+protected theorem le_of_not_gt : ∀{a b : Nat}, ¬(b > a) → b ≤ a := Nat.ge_of_not_lt
+protected theorem le_of_not_lt : ∀{a b : Nat}, ¬(a < b) → b ≤ a := Nat.ge_of_not_lt
+
+theorem ne_of_gt {a b : Nat} (h : b < a) : a ≠ b := (ne_of_lt h).symm
+protected theorem ne_of_lt' : ∀{a b : Nat}, a < b → b ≠ a := ne_of_gt
+
+@[simp] protected theorem not_le {a b : Nat} : ¬ a ≤ b ↔ b < a :=
+  Iff.intro Nat.gt_of_not_le Nat.not_le_of_gt
+@[simp] protected theorem not_lt {a b : Nat} : ¬ a < b ↔ b ≤ a :=
+  Iff.intro Nat.ge_of_not_lt (flip Nat.not_le_of_gt)
+
+protected theorem le_of_not_le {a b : Nat} (h : ¬ b ≤ a) : a ≤ b := Nat.le_of_lt (Nat.not_le.1 h)
+protected theorem le_of_not_ge : ∀{a b : Nat}, ¬(a ≥ b) → a ≤ b:= @Nat.le_of_not_le
+
+protected theorem lt_trichotomy (a b : Nat) : a < b ∨ a = b ∨ b < a :=
+  match Nat.lt_or_ge a b with
+  | .inl h => .inl h
+  | .inr h =>
+    match Nat.eq_or_lt_of_le h with
+    | .inl h => .inr (.inl h.symm)
+    | .inr h => .inr (.inr h)
+
+protected theorem lt_or_gt_of_ne {a b : Nat} (ne : a ≠ b) : a < b ∨ a > b :=
+  match Nat.lt_trichotomy a b with
+  | .inl h => .inl h
+  | .inr (.inl e) => False.elim (ne e)
+  | .inr (.inr h) => .inr h
+
+protected theorem lt_or_lt_of_ne : ∀{a b : Nat}, a ≠ b → a < b ∨ b < a := Nat.lt_or_gt_of_ne
+
+protected theorem le_antisymm_iff {a b : Nat} : a = b ↔ a ≤ b ∧ b ≤ a :=
+  Iff.intro (fun p => And.intro (Nat.le_of_eq p) (Nat.le_of_eq p.symm))
+            (fun ⟨hle, hge⟩ => Nat.le_antisymm hle hge)
+protected theorem eq_iff_le_and_ge : ∀{a b : Nat}, a = b ↔ a ≤ b ∧ b ≤ a := @Nat.le_antisymm_iff
 
 instance : Antisymm ( . ≤ . : Nat → Nat → Prop) where
   antisymm h₁ h₂ := Nat.le_antisymm h₁ h₂
@@ -401,6 +429,8 @@ protected theorem add_lt_add_right {n m : Nat} (h : n < m) (k : Nat) : n + k < m
 protected theorem zero_lt_one : 0 < (1:Nat) :=
   zero_lt_succ 0
 
+protected theorem pos_iff_ne_zero : 0 < n ↔ n ≠ 0 := ⟨ne_of_gt, Nat.pos_of_ne_zero⟩
+
 theorem add_le_add {a b c d : Nat} (h₁ : a ≤ b) (h₂ : c ≤ d) : a + c ≤ b + d :=
   Nat.le_trans (Nat.add_le_add_right h₁ c) (Nat.add_le_add_left h₂ b)
 
@@ -418,6 +448,9 @@ protected theorem le_of_add_le_add_right {a b c : Nat} : a + b ≤ c + b → a
   rw [Nat.add_comm _ b, Nat.add_comm _ b]
   apply Nat.le_of_add_le_add_left
 
+protected theorem add_le_add_iff_right {n : Nat} : m + n ≤ k + n ↔ m ≤ k :=
+  ⟨Nat.le_of_add_le_add_right, fun h => Nat.add_le_add_right h _⟩
+
 /-! # Basic theorems for comparing numerals -/
 
 theorem ctor_eq_zero : Nat.zero = 0 :=
@@ -527,7 +560,20 @@ theorem not_eq_zero_of_lt (h : b < a) : a ≠ 0 := by
 theorem pred_lt' {n m : Nat} (h : m < n) : pred n < n :=
   pred_lt (not_eq_zero_of_lt h)
 
-/-! # sub/pred theorems -/
+/-! # pred theorems -/
+
+@[simp] protected theorem pred_zero : pred 0 = 0 := rfl
+@[simp] protected theorem pred_succ (n : Nat) : pred n.succ = n := rfl
+
+theorem succ_pred {a : Nat} (h : a ≠ 0) : a.pred.succ = a := by
+  induction a with
+  | zero => contradiction
+  | succ => rfl
+
+theorem succ_pred_eq_of_pos : ∀ {n}, 0 < n → succ (pred n) = n
+  | _+1, _ => rfl
+
+/-! # sub theorems -/
 
 theorem add_sub_self_left (a b : Nat) : (a + b) - a = b := by
   induction a with
@@ -561,11 +607,6 @@ theorem sub_succ_lt_self (a i : Nat) (h : i < a) : a - (i + 1) < a - i := by
   apply Nat.zero_lt_sub_of_lt
   assumption
 
-theorem succ_pred {a : Nat} (h : a ≠ 0) : a.pred.succ = a := by
-  induction a with
-  | zero => contradiction
-  | succ => rfl
-
 theorem sub_ne_zero_of_lt : {a b : Nat} → a < b → b - a ≠ 0
   | 0, 0, h      => absurd h (Nat.lt_irrefl 0)
   | 0, succ b, _ => by simp
@@ -591,7 +632,7 @@ protected theorem add_sub_add_right (n k m : Nat) : (n + k) - (m + k) = n - m :=
 protected theorem add_sub_add_left (k n m : Nat) : (k + n) - (k + m) = n - m := by
   rw [Nat.add_comm k n, Nat.add_comm k m, Nat.add_sub_add_right]
 
-protected theorem add_sub_cancel (n m : Nat) : n + m - m = n :=
+@[simp] protected theorem add_sub_cancel (n m : Nat) : n + m - m = n :=
   suffices n + m - (0 + m) = n by rw [Nat.zero_add] at this; assumption
   by rw [Nat.add_sub_add_right, Nat.sub_zero]
 
@@ -680,12 +721,6 @@ theorem lt_sub_of_add_lt {a b c : Nat} (h : a + b < c) : a < c - b :=
   have : a.succ + b ≤ c := by simp [Nat.succ_add]; exact h
   le_sub_of_add_le this
 
-@[simp] protected theorem pred_zero : pred 0 = 0 :=
-  rfl
-
-@[simp] protected theorem pred_succ (n : Nat) : pred n.succ = n :=
-  rfl
-
 theorem sub.elim {motive : Nat → Prop}
     (x y : Nat)
     (h₁ : y ≤ x → (k : Nat) → x = y + k → motive k)
@@ -695,19 +730,76 @@ theorem sub.elim {motive : Nat → Prop}
   | inl hlt => rw [Nat.sub_eq_zero_of_le (Nat.le_of_lt hlt)]; exact h₂ hlt
   | inr hle => exact h₁ hle (x - y) (Nat.add_sub_of_le hle).symm
 
-theorem mul_pred_left (n m : Nat) : pred n * m = n * m - m := by
-  cases n with
-  | zero   => simp
-  | succ n => rw [Nat.pred_succ, succ_mul, Nat.add_sub_cancel]
+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]
 
-theorem mul_pred_right (n m : Nat) : n * pred m = n * m - n := by
-  rw [Nat.mul_comm, mul_pred_left, Nat.mul_comm]
+protected theorem sub_pos_of_lt (h : m < n) : 0 < n - m :=
+  Nat.pos_iff_ne_zero.2 (Nat.sub_ne_zero_of_lt h)
 
 protected theorem sub_sub (n m k : Nat) : n - m - k = n - (m + k) := by
   induction k with
   | zero => simp
   | succ k ih => rw [Nat.add_succ, Nat.sub_succ, Nat.sub_succ, ih]
 
+protected theorem sub_le_sub_left (h : n ≤ m) (k : Nat) : k - m ≤ k - n :=
+  match m, le.dest h with
+  | _, ⟨a, rfl⟩ => by rw [← Nat.sub_sub]; apply sub_le
+
+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)
+
+protected theorem lt_of_sub_ne_zero (h : n - m ≠ 0) : m < n :=
+  Nat.not_le.1 (mt Nat.sub_eq_zero_of_le h)
+
+protected theorem sub_ne_zero_iff_lt : n - m ≠ 0 ↔ m < n :=
+  ⟨Nat.lt_of_sub_ne_zero, Nat.sub_ne_zero_of_lt⟩
+
+protected theorem lt_of_sub_pos (h : 0 < n - m) : m < n :=
+  Nat.lt_of_sub_ne_zero (Nat.pos_iff_ne_zero.1 h)
+
+protected theorem lt_of_sub_eq_succ (h : m - n = succ l) : n < m :=
+  Nat.lt_of_sub_pos (h ▸ Nat.zero_lt_succ _)
+
+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 sub_lt_right_of_lt_add {n k m : Nat} (H : n ≤ k) (h : k < m + n) : k - n < m :=
+  Nat.sub_lt_left_of_lt_add H (Nat.add_comm .. ▸ h)
+
+protected theorem le_of_sub_eq_zero : ∀ {n m}, n - m = 0 → n ≤ m
+  | 0, _, _ => Nat.zero_le ..
+  | _+1, _+1, h => Nat.succ_le_succ <| Nat.le_of_sub_eq_zero (Nat.succ_sub_succ .. ▸ h)
+
+protected theorem le_of_sub_le_sub_right : ∀ {n m k : Nat}, k ≤ m → n - k ≤ m - k → n ≤ m
+  | 0, _, _, _, _ => Nat.zero_le ..
+  | _+1, _, 0, _, h₁ => h₁
+  | _+1, _+1, _+1, h₀, h₁ => by
+    simp only [Nat.succ_sub_succ] at h₁
+    exact succ_le_succ <| Nat.le_of_sub_le_sub_right (le_of_succ_le_succ h₀) h₁
+
+protected theorem sub_le_sub_iff_right {n : Nat} (h : k ≤ m) : n - k ≤ m - k ↔ n ≤ m :=
+  ⟨Nat.le_of_sub_le_sub_right h, fun h => Nat.sub_le_sub_right h _⟩
+
+protected theorem sub_eq_iff_eq_add {c : Nat} (h : b ≤ a) : a - b = c ↔ a = c + b :=
+  ⟨fun | rfl => by rw [Nat.sub_add_cancel h], fun heq => by rw [heq, Nat.add_sub_cancel]⟩
+
+protected theorem sub_eq_iff_eq_add' {c : Nat} (h : b ≤ a) : a - b = c ↔ a = b + c := by
+  rw [Nat.add_comm, Nat.sub_eq_iff_eq_add h]
+
+theorem mul_pred_left (n m : Nat) : pred n * m = n * m - m := by
+  cases n with
+  | zero   => simp
+  | succ n => rw [Nat.pred_succ, succ_mul, Nat.add_sub_cancel]
+
+/-! ## Mul sub distrib -/
+
+theorem mul_pred_right (n m : Nat) : n * pred m = n * m - n := by
+  rw [Nat.mul_comm, mul_pred_left, Nat.mul_comm]
+
+
 protected theorem mul_sub_right_distrib (n m k : Nat) : (n - m) * k = n * k - m * k := by
   induction m with
   | zero => simp
@@ -719,14 +811,12 @@ protected theorem mul_sub_left_distrib (n m k : Nat) : n * (m - k) = n * m - n *
 /-! # Helper normalization theorems -/
 
 theorem not_le_eq (a b : Nat) : (¬ (a ≤ b)) = (b + 1 ≤ a) :=
-  propext <| Iff.intro (fun h => Nat.gt_of_not_le h) (fun h => Nat.not_le_of_gt h)
-
+  Eq.propIntro Nat.gt_of_not_le Nat.not_le_of_gt
 theorem not_ge_eq (a b : Nat) : (¬ (a ≥ b)) = (a + 1 ≤ b) :=
   not_le_eq b a
 
 theorem not_lt_eq (a b : Nat) : (¬ (a < b)) = (b ≤ a) :=
-  propext <| Iff.intro (fun h => have h := Nat.succ_le_of_lt (Nat.gt_of_not_le h); Nat.le_of_succ_le_succ h) (fun h => Nat.not_le_of_gt (Nat.succ_le_succ h))
-
+  Eq.propIntro Nat.le_of_not_lt Nat.not_lt_of_le
 theorem not_gt_eq (a b : Nat) : (¬ (a > b)) = (a ≤ b) :=
   not_lt_eq b a
 

src/Init/Data/Nat/Div.lean

@@ -7,6 +7,7 @@ prelude
 import Init.WF
 import Init.WFTactics
 import Init.Data.Nat.Basic
+
 namespace Nat
 
 theorem div_rec_lemma {x y : Nat} : 0 < y ∧ y ≤ x → x - y < x :=
@@ -174,4 +175,136 @@ theorem div_add_mod (m n : Nat) : n * (m / n) + m % n = m := by
     rw [Nat.left_distrib, Nat.mul_one, Nat.add_assoc, Nat.add_left_comm, ih, Nat.add_comm, Nat.sub_add_cancel h.2]
 decreasing_by apply div_rec_lemma; assumption
 
+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 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]
+
+@[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 | zero => 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_right, IH k0, succ_mul,
+        ← Nat.add_sub_cancel (x*k) k, Nat.sub_le_sub_iff_right h.2, Nat.add_sub_cancel]
+
+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 _)
+
+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)
+
+@[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]
+
+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]
+
+@[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]
+
+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 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 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
+  focus
+    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 _)) _
+  focus
+    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?
+    focus
+      rw [Nat.mul_sub_right_distrib, Nat.mul_comm]
+      exact Nat.sub_le_sub_left (div_mul_le_self ..) _
+    focus
+      rwa [div_lt_iff_lt_mul npos, Nat.mul_comm]
+
+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 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
+
 end Nat

src/Init/Data/Nat/Dvd.lean

@@ -0,0 +1,96 @@
+prelude
+import Init.Data.Nat.Div
+
+namespace Nat
+
+/--
+Divisibility of natural numbers. `a ∣ b` (typed as `\|`) says that
+there is some `c` such that `b = a * c`.
+-/
+instance : Dvd Nat where
+  dvd a b := Exists (fun c => b = a * c)
+
+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
+
+@[simp] protected theorem zero_dvd {n : Nat} : 0 ∣ n ↔ n = 0 :=
+  ⟨Nat.eq_zero_of_zero_dvd, fun h => h.symm ▸ Nat.dvd_zero 0⟩
+
+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_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
+
+protected 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)
+
+@[simp] protected theorem one_dvd (n : Nat) : 1 ∣ n := ⟨n, n.one_mul.symm⟩
+
+theorem eq_one_of_dvd_one {n : Nat} (H : n ∣ 1) : n = 1 := Nat.dvd_antisymm H n.one_dvd
+
+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_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 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
+
+theorem emod_pos_of_not_dvd {a b : Nat} (h : ¬ a ∣ b) : 0 < b % a := by
+  rw [dvd_iff_mod_eq_zero] at h
+  exact Nat.pos_of_ne_zero h
+
+
+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]
+
+end Nat

src/Init/Data/Nat/Gcd.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import Init.Data.Nat.Div
+import Init.Data.Nat.Dvd
 
 namespace Nat
 
@@ -38,4 +38,35 @@ theorem gcd_succ (x y : Nat) : gcd (succ x) y = gcd (y % succ x) (succ x) :=
 @[simp] theorem gcd_self (n : Nat) : gcd n n = n := by
   cases n <;> simp [gcd_succ]
 
+theorem gcd_rec (m n : Nat) : gcd m n = gcd (n % m) m :=
+  match m with
+  | 0 => by have := (mod_zero n).symm; rwa [gcd_zero_right]
+  | _ + 1 => by simp [gcd_succ]
+
+@[elab_as_elim] theorem gcd.induction {P : Nat → Nat → Prop} (m n : Nat)
+    (H0 : ∀n, P 0 n) (H1 : ∀ m n, 0 < m → P (n % m) m → P m n) : P m n :=
+  Nat.strongInductionOn (motive := fun m => ∀ n, P m n) m
+    (fun
+    | 0, _ => H0
+    | _+1, IH => fun _ => H1 _ _ (succ_pos _) (IH _ (mod_lt _ (succ_pos _)) _) )
+    n
+
+theorem gcd_dvd (m n : Nat) : (gcd m n ∣ m) ∧ (gcd m n ∣ n) := by
+  induction m, n using gcd.induction with
+  | H0 n => rw [gcd_zero_left]; exact ⟨Nat.dvd_zero n, Nat.dvd_refl n⟩
+  | H1 m n _ IH => rw [← gcd_rec] at IH; exact ⟨IH.2, (dvd_mod_iff IH.2).1 IH.1⟩
+
+theorem gcd_dvd_left (m n : Nat) : gcd m n ∣ m := (gcd_dvd m n).left
+
+theorem gcd_dvd_right (m n : Nat) : gcd m n ∣ n := (gcd_dvd m n).right
+
+theorem gcd_le_left (n) (h : 0 < m) : gcd m n ≤ m := le_of_dvd h <| gcd_dvd_left m n
+
+theorem gcd_le_right (n) (h : 0 < n) : gcd m n ≤ n := le_of_dvd h <| gcd_dvd_right m n
+
+theorem dvd_gcd : k ∣ m → k ∣ n → k ∣ gcd m n := by
+  induction m, n using gcd.induction with intro km kn
+  | H0 n => rw [gcd_zero_left]; exact kn
+  | H1 n m _ IH => rw [gcd_rec]; exact IH ((dvd_mod_iff km).2 kn) km
+
 end Nat

src/Init/Data/Nat/Linear.lean

@@ -5,8 +5,7 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Init.Coe
-import Init.Classical
-import Init.SimpLemmas
+import Init.ByCases
 import Init.Data.Nat.Basic
 import Init.Data.List.Basic
 import Init.Data.Prod
@@ -539,13 +538,13 @@ theorem Expr.eq_of_toNormPoly (ctx : Context) (a b : Expr) (h : a.toNormPoly = b
 theorem Expr.of_cancel_eq (ctx : Context) (a b c d : Expr) (h : Poly.cancel a.toNormPoly b.toNormPoly = (c.toPoly, d.toPoly)) : (a.denote ctx = b.denote ctx) = (c.denote ctx = d.denote ctx) := by
   have := Poly.denote_eq_cancel_eq ctx a.toNormPoly b.toNormPoly
   rw [h] at this
-  simp [toNormPoly, Poly.norm, Poly.denote_eq] at this
+  simp [toNormPoly, Poly.norm, Poly.denote_eq, -eq_iff_iff] at this
   exact this.symm
 
 theorem Expr.of_cancel_le (ctx : Context) (a b c d : Expr) (h : Poly.cancel a.toNormPoly b.toNormPoly = (c.toPoly, d.toPoly)) : (a.denote ctx ≤ b.denote ctx) = (c.denote ctx ≤ d.denote ctx) := by
   have := Poly.denote_le_cancel_eq ctx a.toNormPoly b.toNormPoly
   rw [h] at this
-  simp [toNormPoly, Poly.norm,Poly.denote_le] at this
+  simp [toNormPoly, Poly.norm,Poly.denote_le, -eq_iff_iff] at this
   exact this.symm
 
 theorem Expr.of_cancel_lt (ctx : Context) (a b c d : Expr) (h : Poly.cancel a.inc.toNormPoly b.toNormPoly = (c.inc.toPoly, d.toPoly)) : (a.denote ctx < b.denote ctx) = (c.denote ctx < d.denote ctx) :=
@@ -590,7 +589,7 @@ theorem PolyCnstr.denote_mul (ctx : Context) (k : Nat) (c : PolyCnstr) : (c.mul
   have : (1 == (0 : Nat)) = false := rfl
   have : (1 == (1 : Nat)) = true  := rfl
   by_cases he : eq = true <;> simp [he, PolyCnstr.mul, PolyCnstr.denote, Poly.denote_le, Poly.denote_eq]
-     <;> by_cases hk : k == 0 <;> (try simp [eq_of_beq hk]) <;> simp [*] <;> apply propext <;> apply Iff.intro <;> intro h
+     <;> by_cases hk : k == 0 <;> (try simp [eq_of_beq hk]) <;> simp [*] <;> apply Iff.intro <;> intro h
   · exact Nat.eq_of_mul_eq_mul_left (Nat.zero_lt_succ _) h
   · rw [h]
   · exact Nat.le_of_mul_le_mul_left h (Nat.zero_lt_succ _)
@@ -637,20 +636,18 @@ theorem Poly.of_isNonZero (ctx : Context) {p : Poly} (h : isNonZero p = true) :
 theorem PolyCnstr.eq_false_of_isUnsat (ctx : Context) {c : PolyCnstr} : c.isUnsat → c.denote ctx = False := by
   cases c; rename_i eq lhs rhs
   simp [isUnsat]
-  by_cases he : eq = true <;> simp [he, denote, Poly.denote_eq, Poly.denote_le]
+  by_cases he : eq = true <;> simp [he, denote, Poly.denote_eq, Poly.denote_le, -and_imp]
   · intro
       | Or.inl ⟨h₁, h₂⟩ => simp [Poly.of_isZero, h₁]; have := Nat.not_eq_zero_of_lt (Poly.of_isNonZero ctx h₂); simp [this.symm]
       | Or.inr ⟨h₁, h₂⟩ => simp [Poly.of_isZero, h₂]; have := Nat.not_eq_zero_of_lt (Poly.of_isNonZero ctx h₁); simp [this]
   · intro ⟨h₁, h₂⟩
     simp [Poly.of_isZero, h₂]
-    have := Nat.not_eq_zero_of_lt (Poly.of_isNonZero ctx h₁)
-    simp [this]
-    done
+    exact Poly.of_isNonZero ctx h₁
 
 theorem PolyCnstr.eq_true_of_isValid (ctx : Context) {c : PolyCnstr} : c.isValid → c.denote ctx = True := by
   cases c; rename_i eq lhs rhs
   simp [isValid]
-  by_cases he : eq = true <;> simp [he, denote, Poly.denote_eq, Poly.denote_le]
+  by_cases he : eq = true <;> simp [he, denote, Poly.denote_eq, Poly.denote_le, -and_imp]
   · intro ⟨h₁, h₂⟩
     simp [Poly.of_isZero, h₁, h₂]
   · intro h
@@ -658,12 +655,12 @@ theorem PolyCnstr.eq_true_of_isValid (ctx : Context) {c : PolyCnstr} : c.isValid
 
 theorem ExprCnstr.eq_false_of_isUnsat (ctx : Context) (c : ExprCnstr) (h : c.toNormPoly.isUnsat) : c.denote ctx = False := by
   have := PolyCnstr.eq_false_of_isUnsat ctx h
-  simp at this
+  simp [-eq_iff_iff] at this
   assumption
 
 theorem ExprCnstr.eq_true_of_isValid (ctx : Context) (c : ExprCnstr) (h : c.toNormPoly.isValid) : c.denote ctx = True := by
   have := PolyCnstr.eq_true_of_isValid ctx h
-  simp at this
+  simp [-eq_iff_iff] at this
   assumption
 
 theorem Certificate.of_combineHyps (ctx : Context) (c : PolyCnstr) (cs : Certificate) (h : (combineHyps c cs).denote ctx → False) : c.denote ctx → cs.denote ctx := by
@@ -712,7 +709,7 @@ theorem Poly.denote_toExpr (ctx : Context) (p : Poly) : p.toExpr.denote ctx = p.
 
 theorem ExprCnstr.eq_of_toNormPoly_eq (ctx : Context) (c d : ExprCnstr) (h : c.toNormPoly == d.toPoly) : c.denote ctx = d.denote ctx := by
   have h := congrArg (PolyCnstr.denote ctx) (eq_of_beq h)
-  simp at h
+  simp [-eq_iff_iff] at h
   assumption
 
 theorem Expr.eq_of_toNormPoly_eq (ctx : Context) (e e' : Expr) (h : e.toNormPoly == e'.toPoly) : e.denote ctx = e'.denote ctx := by

src/Init/Data/Nat/MinMax.lean

@@ -0,0 +1,51 @@
+prelude
+import Init.ByCases
+
+namespace Nat
+
+/-! # min lemmas -/
+
+protected theorem min_eq_min (a : Nat) : Nat.min a b = min a b := rfl
+
+protected theorem min_comm (a b : Nat) : min a b = min b a := by
+  match Nat.lt_trichotomy a b with
+  | .inl h => simp [Nat.min_def, h, Nat.le_of_lt, Nat.not_le_of_lt]
+  | .inr (.inl h) => simp [Nat.min_def, h]
+  | .inr (.inr h) => simp [Nat.min_def, h, Nat.le_of_lt, Nat.not_le_of_lt]
+
+protected theorem min_le_right (a b : Nat) : min a b ≤ b := by
+  by_cases (a <= b) <;> simp [Nat.min_def, *]
+protected theorem min_le_left (a b : Nat) : min a b ≤ a :=
+  Nat.min_comm .. ▸ Nat.min_le_right ..
+
+protected theorem min_eq_left {a b : Nat} (h : a ≤ b) : min a b = a := if_pos h
+protected theorem min_eq_right {a b : Nat} (h : b ≤ a) : min a b = b :=
+  Nat.min_comm .. ▸ Nat.min_eq_left h
+
+protected theorem le_min_of_le_of_le {a b c : Nat} : a ≤ b → a ≤ c → a ≤ min b c := by
+  intros; cases Nat.le_total b c with
+  | inl h => rw [Nat.min_eq_left h]; assumption
+  | inr h => rw [Nat.min_eq_right h]; assumption
+
+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₂⟩ => Nat.le_min_of_le_of_le h₁ h₂⟩
+
+protected theorem lt_min {a b c : Nat} : a < min b c ↔ a < b ∧ a < c := Nat.le_min
+
+/-! # max lemmas -/
+
+protected theorem max_eq_max (a : Nat) : Nat.max a b = max a b := rfl
+
+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
+  by_cases (a <= b) <;> simp [Nat.max_def, *]
+protected theorem le_max_right (a b : Nat) : b ≤ max a b :=
+   Nat.max_comm .. ▸ Nat.le_max_left ..
+
+end Nat

src/Init/Data/Nat/Power2.lean

@@ -8,6 +8,8 @@ import Init.Data.Nat.Linear
 
 namespace Nat
 
+protected theorem two_pow_pos (w : Nat) : 0 < 2^w := Nat.pos_pow_of_pos _ (by decide)
+
 theorem nextPowerOfTwo_dec {n power : Nat} (h₁ : power > 0) (h₂ : power < n) : n - power * 2 < n - power := by
   have : power * 2 = power + power := by simp_arith
   rw [this, Nat.sub_add_eq]

src/Init/Ext.lean

@@ -0,0 +1,113 @@
+/-
+Copyright (c) 2021 Gabriel Ebner. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Gabriel Ebner, Mario Carneiro
+-/
+prelude
+import Init.TacticsExtra
+import Init.RCases
+
+namespace Lean
+namespace Parser.Attr
+/-- Registers an extensionality theorem.
+
+* When `@[ext]` is applied to a structure, it generates `.ext` and `.ext_iff` theorems and registers
+  them for the `ext` tactic.
+
+* When `@[ext]` is applied to a theorem, the theorem is registered for the `ext` tactic.
+
+* An optional natural number argument, e.g. `@[ext 9000]`, specifies a priority for the lemma. Higher-priority lemmas are chosen first, and the default is `1000`.
+
+* The flag `@[ext (flat := false)]` causes generated structure extensionality theorems to show inherited fields based on their representation,
+  rather than flattening the parents' fields into the lemma's equality hypotheses.
+  structures in the generated extensionality theorems. -/
+syntax (name := ext) "ext" (" (" &"flat" " := " term ")")? (ppSpace prio)? : attr
+end Parser.Attr
+
+-- TODO: rename this namespace?
+-- Remark: `ext` has scoped syntax, Mathlib may depend on the actual namespace name.
+namespace Elab.Tactic.Ext
+/--
+Creates the type of the extensionality theorem for the given structure,
+elaborating to `x.1 = y.1 → x.2 = y.2 → x = y`, for example.
+-/
+scoped syntax (name := extType) "ext_type% " term:max ppSpace ident : term
+
+/--
+Creates the type of the iff-variant of the extensionality theorem for the given structure,
+elaborating to `x = y ↔ x.1 = y.1 ∧ x.2 = y.2`, for example.
+-/
+scoped syntax (name := extIffType) "ext_iff_type% " term:max ppSpace ident : term
+
+/--
+`declare_ext_theorems_for A` declares the extensionality theorems for the structure `A`.
+
+These theorems state that two expressions with the structure type are equal if their fields are equal.
+-/
+syntax (name := declareExtTheoremFor) "declare_ext_theorems_for " ("(" &"flat" " := " term ") ")? ident (ppSpace prio)? : command
+
+macro_rules | `(declare_ext_theorems_for $[(flat := $f)]? $struct:ident $(prio)?) => do
+  let flat := f.getD (mkIdent `true)
+  let names ← Macro.resolveGlobalName struct.getId.eraseMacroScopes
+  let name ← match names.filter (·.2.isEmpty) with
+    | [] => Macro.throwError s!"unknown constant {struct.getId}"
+    | [(name, _)] => pure name
+    | _ => Macro.throwError s!"ambiguous name {struct.getId}"
+  let extName := mkIdentFrom struct (canonical := true) <| name.mkStr "ext"
+  let extIffName := mkIdentFrom struct (canonical := true) <| name.mkStr "ext_iff"
+  `(@[ext $(prio)?] protected theorem $extName:ident : ext_type% $flat $struct:ident :=
+      fun {..} {..} => by intros; subst_eqs; rfl
+    protected theorem $extIffName:ident : ext_iff_type% $flat $struct:ident :=
+      fun {..} {..} =>
+        ⟨fun h => by cases h; and_intros <;> rfl,
+         fun _ => by (repeat cases ‹_ ∧ _›); subst_eqs; rfl⟩)
+
+/--
+Applies extensionality lemmas that are registered with the `@[ext]` attribute.
+* `ext pat*` applies extensionality theorems as much as possible,
+  using the patterns `pat*` to introduce the variables in extensionality theorems using `rintro`.
+  For example, the patterns are used to name the variables introduced by lemmas such as `funext`.
+* Without patterns,`ext` applies extensionality lemmas as much
+  as possible but introduces anonymous hypotheses whenever needed.
+* `ext pat* : n` applies ext theorems only up to depth `n`.
+
+The `ext1 pat*` tactic is like `ext pat*` except that it only applies a single extensionality theorem.
+
+Unused patterns will generate warning.
+Patterns that don't match the variables will typically result in the introduction of anonymous hypotheses.
+-/
+syntax (name := ext) "ext" (colGt ppSpace rintroPat)* (" : " num)? : tactic
+
+/-- Apply a single extensionality theorem to the current goal. -/
+syntax (name := applyExtTheorem) "apply_ext_theorem" : tactic
+
+/--
+`ext1 pat*` is like `ext pat*` except that it only applies a single extensionality theorem rather
+than recursively applying as many extensionality theorems as possible.
+
+The `pat*` patterns are processed using the `rintro` tactic.
+If no patterns are supplied, then variables are introduced anonymously using the `intros` tactic.
+-/
+macro "ext1" xs:(colGt ppSpace rintroPat)* : tactic =>
+  if xs.isEmpty then `(tactic| apply_ext_theorem <;> intros)
+  else `(tactic| apply_ext_theorem <;> rintro $xs*)
+
+end Elab.Tactic.Ext
+end Lean
+
+attribute [ext] funext propext Subtype.eq
+
+@[ext] theorem Prod.ext : {x y : Prod α β} → x.fst = y.fst → x.snd = y.snd → x = y
+  | ⟨_,_⟩, ⟨_,_⟩, rfl, rfl => rfl
+
+@[ext] theorem PProd.ext : {x y : PProd α β} → x.fst = y.fst → x.snd = y.snd → x = y
+  | ⟨_,_⟩, ⟨_,_⟩, rfl, rfl => rfl
+
+@[ext] theorem Sigma.ext : {x y : Sigma β} → x.fst = y.fst → HEq x.snd y.snd → x = y
+  | ⟨_,_⟩, ⟨_,_⟩, rfl, .rfl => rfl
+
+@[ext] theorem PSigma.ext : {x y : PSigma β} → x.fst = y.fst → HEq x.snd y.snd → x = y
+  | ⟨_,_⟩, ⟨_,_⟩, rfl, .rfl => rfl
+
+@[ext] protected theorem PUnit.ext (x y : PUnit) : x = y := rfl
+protected theorem Unit.ext (x y : Unit) : x = y := rfl

src/Init/Notation.lean

@@ -464,6 +464,14 @@ macro "without_expected_type " x:term : term => `(let aux := $x; aux)
 
 namespace Lean
 
+/--
+* The `by_elab doSeq` expression runs the `doSeq` as a `TermElabM Expr` to
+  synthesize the expression.
+* `by_elab fun expectedType? => do doSeq` receives the expected type (an `Option Expr`)
+  as well.
+-/
+syntax (name := byElab) "by_elab " doSeq : term
+
 /--
 Category for carrying raw syntax trees between macros; any content is printed as is by the pretty printer.
 The only accepted parser for this category is an antiquotation.
@@ -498,3 +506,26 @@ a string literal with the contents of the file at `"parent_dir" / "path" / "to"
 file cannot be read, elaboration fails.
 -/
 syntax (name := includeStr) "include_str " term : term
+
+/--
+The `run_cmd doSeq` command executes code in `CommandElabM Unit`.
+This is almost the same as `#eval show CommandElabM Unit from do doSeq`,
+except that it doesn't print an empty diagnostic.
+-/
+syntax (name := runCmd) "run_cmd " doSeq : command
+
+/--
+The `run_elab doSeq` command executes code in `TermElabM Unit`.
+This is almost the same as `#eval show TermElabM Unit from do doSeq`,
+except that it doesn't print an empty diagnostic.
+-/
+syntax (name := runElab) "run_elab " doSeq : command
+
+/--
+The `run_meta doSeq` command executes code in `MetaM Unit`.
+This is almost the same as `#eval show MetaM Unit from do doSeq`,
+except that it doesn't print an empty diagnostic.
+
+(This is effectively a synonym for `run_elab`.)
+-/
+syntax (name := runMeta) "run_meta " doSeq : command

src/Init/NotationExtra.lean

@@ -391,6 +391,23 @@ macro_rules
     `($mods:declModifiers class $id $params* extends $parents,* $[: $ty]?
       attribute [instance] $ctor)
 
+macro_rules
+  | `(haveI $hy:hygieneInfo $bs* $[: $ty]? := $val; $body) =>
+    `(haveI $(HygieneInfo.mkIdent hy `this (canonical := true)) $bs* $[: $ty]? := $val; $body)
+  | `(haveI _ $bs* := $val; $body) => `(haveI x $bs* : _ := $val; $body)
+  | `(haveI _ $bs* : $ty := $val; $body) => `(haveI x $bs* : $ty := $val; $body)
+  | `(haveI $x:ident $bs* := $val; $body) => `(haveI $x $bs* : _ := $val; $body)
+  | `(haveI $_:ident $_* : $_ := $_; $_) => Lean.Macro.throwUnsupported -- handled by elab
+
+macro_rules
+  | `(letI $hy:hygieneInfo $bs* $[: $ty]? := $val; $body) =>
+    `(letI $(HygieneInfo.mkIdent hy `this (canonical := true)) $bs* $[: $ty]? := $val; $body)
+  | `(letI _ $bs* := $val; $body) => `(letI x $bs* : _ := $val; $body)
+  | `(letI _ $bs* : $ty := $val; $body) => `(letI x $bs* : $ty := $val; $body)
+  | `(letI $x:ident $bs* := $val; $body) => `(letI $x $bs* : _ := $val; $body)
+  | `(letI $_:ident $_* : $_ := $_; $_) => Lean.Macro.throwUnsupported -- handled by elab
+
+
 syntax cdotTk := patternIgnore("· " <|> ". ")
 /-- `· tac` focuses on the main goal and tries to solve it using `tac`, or else fails. -/
 syntax (name := cdot) cdotTk tacticSeqIndentGt : tactic

src/Init/Prelude.lean

@@ -548,6 +548,11 @@ theorem Or.elim {c : Prop} (h : Or a b) (left : a → c) (right : b → c) : c :
   | Or.inl h => left h
   | Or.inr h => right h
 
+theorem Or.resolve_left  (h: Or a b) (na : Not a) : b := h.elim (absurd · na) id
+theorem Or.resolve_right (h: Or a b) (nb : Not b) : a := h.elim id (absurd · nb)
+theorem Or.neg_resolve_left  (h : Or (Not a) b) (ha : a) : b := h.elim (absurd ha) id
+theorem Or.neg_resolve_right (h : Or a (Not b)) (nb : b) : a := h.elim id (absurd nb)
+
 /--
 `Bool` is the type of boolean values, `true` and `false`. Classically,
 this is equivalent to `Prop` (the type of propositions), but the distinction

src/Init/PropLemmas.lean

@@ -0,0 +1,437 @@
+/-
+Copyright (c) 2024 Lean FRO.  All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura, Jeremy Avigad, Floris van Doorn, Mario Carneiro
+
+This provides additional lemmas about propositional types beyond what is
+needed for Core and SimpLemmas.
+-/
+prelude
+import Init.Core
+import Init.NotationExtra
+set_option linter.missingDocs true -- keep it documented
+
+/-! ## not -/
+
+theorem not_not_em (a : Prop) : ¬¬(a ∨ ¬a) := fun h => h (.inr (h ∘ .inl))
+
+/-! ## and -/
+
+theorem and_self_iff : a ∧ a ↔ a := Iff.of_eq (and_self a)
+theorem and_not_self_iff (a : Prop) : a ∧ ¬a ↔ False := iff_false_intro and_not_self
+theorem not_and_self_iff (a : Prop) : ¬a ∧ a ↔ False := iff_false_intro not_and_self
+
+theorem And.imp (f : a → c) (g : b → d) (h : a ∧ b) : c ∧ d :=  And.intro (f h.left) (g h.right)
+theorem And.imp_left (h : a → b) : a ∧ c → b ∧ c := .imp h id
+theorem And.imp_right (h : a → b) : c ∧ a → c ∧ b := .imp id h
+
+theorem and_congr (h₁ : a ↔ c) (h₂ : b ↔ d) : a ∧ b ↔ c ∧ d :=
+  Iff.intro (And.imp h₁.mp h₂.mp) (And.imp h₁.mpr h₂.mpr)
+theorem and_congr_left' (h : a ↔ b) : a ∧ c ↔ b ∧ c := and_congr h .rfl
+theorem and_congr_right' (h : b ↔ c) : a ∧ b ↔ a ∧ c := and_congr .rfl h
+
+theorem not_and_of_not_left (b : Prop) : ¬a → ¬(a ∧ b) := mt And.left
+theorem not_and_of_not_right (a : Prop) {b : Prop} : ¬b → ¬(a ∧ b) := mt And.right
+
+theorem and_congr_right_eq (h : a → b = c) : (a ∧ b) = (a ∧ c) :=
+  propext (and_congr_right (Iff.of_eq ∘ h))
+theorem and_congr_left_eq  (h : c → a = b) : (a ∧ c) = (b ∧ c) :=
+  propext (and_congr_left  (Iff.of_eq ∘ h))
+
+theorem and_left_comm : a ∧ b ∧ c ↔ b ∧ a ∧ c :=
+  Iff.intro (fun ⟨ha, hb, hc⟩ => ⟨hb, ha, hc⟩)
+            (fun ⟨hb, ha, hc⟩ => ⟨ha, hb, hc⟩)
+
+theorem and_right_comm : (a ∧ b) ∧ c ↔ (a ∧ c) ∧ b :=
+  Iff.intro (fun ⟨⟨ha, hb⟩, hc⟩ => ⟨⟨ha, hc⟩, hb⟩)
+            (fun ⟨⟨ha, hc⟩, hb⟩ => ⟨⟨ha, hb⟩, hc⟩)
+
+theorem and_rotate : a ∧ b ∧ c ↔ b ∧ c ∧ a := by rw [and_left_comm, @and_comm a c]
+theorem and_and_and_comm : (a ∧ b) ∧ c ∧ d ↔ (a ∧ c) ∧ b ∧ d := by rw [← and_assoc, @and_right_comm a, and_assoc]
+theorem and_and_left  : a ∧ (b ∧ c) ↔ (a ∧ b) ∧ a ∧ c := by rw [and_and_and_comm, and_self]
+theorem and_and_right : (a ∧ b) ∧ c ↔ (a ∧ c) ∧ b ∧ c := by rw [and_and_and_comm, and_self]
+
+theorem and_iff_left  (hb : b) : a ∧ b ↔ a := Iff.intro And.left  (And.intro · hb)
+theorem and_iff_right (ha : a) : a ∧ b ↔ b := Iff.intro And.right (And.intro ha ·)
+
+/-! ## or -/
+
+theorem or_self_iff : a ∨ a ↔ a := or_self _ ▸ .rfl
+theorem not_or_intro {a b : Prop} (ha : ¬a) (hb : ¬b) : ¬(a ∨ b) := (·.elim ha hb)
+
+theorem or_congr (h₁ : a ↔ c) (h₂ : b ↔ d) : (a ∨ b) ↔ (c ∨ d) := ⟨.imp h₁.mp h₂.mp, .imp h₁.mpr h₂.mpr⟩
+theorem or_congr_left (h : a ↔ b) : a ∨ c ↔ b ∨ c := or_congr h .rfl
+theorem or_congr_right (h : b ↔ c) : a ∨ b ↔ a ∨ c := or_congr .rfl h
+
+theorem or_left_comm  : a ∨ (b ∨ c) ↔ b ∨ (a ∨ c) := by rw [← or_assoc, ← or_assoc, @or_comm a b]
+theorem or_right_comm : (a ∨ b) ∨ c ↔ (a ∨ c) ∨ b := by rw [or_assoc, or_assoc, @or_comm b]
+
+theorem or_or_or_comm : (a ∨ b) ∨ c ∨ d ↔ (a ∨ c) ∨ b ∨ d := by rw [← or_assoc, @or_right_comm a, or_assoc]
+
+theorem or_or_distrib_left : a ∨ b ∨ c ↔ (a ∨ b) ∨ a ∨ c := by rw [or_or_or_comm, or_self]
+theorem or_or_distrib_right : (a ∨ b) ∨ c ↔ (a ∨ c) ∨ b ∨ c := by rw [or_or_or_comm, or_self]
+
+theorem or_rotate : a ∨ b ∨ c ↔ b ∨ c ∨ a := by simp only [or_left_comm, Or.comm]
+
+theorem or_iff_left  (hb : ¬b) : a ∨ b ↔ a := or_iff_left_iff_imp.mpr  hb.elim
+theorem or_iff_right (ha : ¬a) : a ∨ b ↔ b := or_iff_right_iff_imp.mpr ha.elim
+
+/-! ## distributivity -/
+
+theorem not_imp_of_and_not : a ∧ ¬b → ¬(a → b)
+  | ⟨ha, hb⟩, h => hb <| h ha
+
+theorem imp_and {α} : (α → b ∧ c) ↔ (α → b) ∧ (α → c) :=
+  ⟨fun h => ⟨fun ha => (h ha).1, fun ha => (h ha).2⟩, fun h ha => ⟨h.1 ha, h.2 ha⟩⟩
+
+theorem not_and' : ¬(a ∧ b) ↔ b → ¬a := Iff.trans not_and imp_not_comm
+
+/-- `∧` distributes over `∨` (on the left). -/
+theorem and_or_left : a ∧ (b ∨ c) ↔ (a ∧ b) ∨ (a ∧ c) :=
+  Iff.intro (fun ⟨ha, hbc⟩ => hbc.imp (.intro ha) (.intro ha))
+            (Or.rec (.imp_right .inl) (.imp_right .inr))
+
+/-- `∧` distributes over `∨` (on the right). -/
+theorem or_and_right : (a ∨ b) ∧ c ↔ (a ∧ c) ∨ (b ∧ c) := by rw [@and_comm (a ∨ b), and_or_left, @and_comm c, @and_comm c]
+
+/-- `∨` distributes over `∧` (on the left). -/
+theorem or_and_left : a ∨ (b ∧ c) ↔ (a ∨ b) ∧ (a ∨ c) :=
+  Iff.intro (Or.rec (fun ha => ⟨.inl ha, .inl ha⟩) (.imp .inr .inr))
+            (And.rec <| .rec (fun _ => .inl ·) (.imp_right ∘ .intro))
+
+/-- `∨` distributes over `∧` (on the right). -/
+theorem and_or_right : (a ∧ b) ∨ c ↔ (a ∨ c) ∧ (b ∨ c) := by rw [@or_comm (a ∧ b), or_and_left, @or_comm c, @or_comm c]
+
+theorem or_imp : (a ∨ b → c) ↔ (a → c) ∧ (b → c) :=
+  Iff.intro (fun h => ⟨h ∘ .inl, h ∘ .inr⟩) (fun ⟨ha, hb⟩ => Or.rec ha hb)
+theorem not_or : ¬(p ∨ q) ↔ ¬p ∧ ¬q := or_imp
+
+theorem not_and_of_not_or_not (h : ¬a ∨ ¬b) : ¬(a ∧ b) := h.elim (mt (·.1)) (mt (·.2))
+
+/-! ## exists and forall -/
+
+section quantifiers
+variable {p q : α → Prop} {b : Prop}
+
+theorem forall_imp (h : ∀ a, p a → q a) : (∀ a, p a) → ∀ a, q a := fun h' a => h a (h' a)
+
+/--
+As `simp` does not index foralls, this `@[simp]` lemma is tried on every `forall` expression.
+This is not ideal, and likely a performance issue, but it is difficult to remove this attribute at this time.
+-/
+@[simp] theorem forall_exists_index {q : (∃ x, p x) → Prop} :
+    (∀ h, q h) ↔ ∀ x (h : p x), q ⟨x, h⟩ :=
+  ⟨fun h x hpx => h ⟨x, hpx⟩, fun h ⟨x, hpx⟩ => h x hpx⟩
+
+theorem Exists.imp (h : ∀ a, p a → q a) : (∃ a, p a) → ∃ a, q a
+  | ⟨a, hp⟩ => ⟨a, h a hp⟩
+
+theorem Exists.imp' {β} {q : β → Prop} (f : α → β) (hpq : ∀ a, p a → q (f a)) :
+    (∃ a, p a) → ∃ b, q b
+  | ⟨_, hp⟩ => ⟨_, hpq _ hp⟩
+
+theorem exists_imp : ((∃ x, p x) → b) ↔ ∀ x, p x → b := forall_exists_index
+
+@[simp] theorem exists_const (α) [i : Nonempty α] : (∃ _ : α, b) ↔ b :=
+  ⟨fun ⟨_, h⟩ => h, i.elim Exists.intro⟩
+
+section forall_congr
+
+theorem forall_congr' (h : ∀ a, p a ↔ q a) : (∀ a, p a) ↔ ∀ a, q a :=
+  ⟨fun H a => (h a).1 (H a), fun H a => (h a).2 (H a)⟩
+
+theorem exists_congr (h : ∀ a, p a ↔ q a) : (∃ a, p a) ↔ ∃ a, q a :=
+  ⟨Exists.imp fun x => (h x).1, Exists.imp fun x => (h x).2⟩
+
+variable {β : α → Sort _}
+
+theorem forall₂_congr {p q : ∀ a, β a → Prop} (h : ∀ a b, p a b ↔ q a b) :
+    (∀ a b, p a b) ↔ ∀ a b, q a b :=
+  forall_congr' fun a => forall_congr' <| h a
+
+theorem exists₂_congr {p q : ∀ a, β a → Prop} (h : ∀ a b, p a b ↔ q a b) :
+    (∃ a b, p a b) ↔ ∃ a b, q a b :=
+  exists_congr fun a => exists_congr <| h a
+
+variable {γ : ∀ a, β a → Sort _}
+theorem forall₃_congr {p q : ∀ a b, γ a b → Prop} (h : ∀ a b c, p a b c ↔ q a b c) :
+    (∀ a b c, p a b c) ↔ ∀ a b c, q a b c :=
+  forall_congr' fun a => forall₂_congr <| h a
+
+theorem exists₃_congr {p q : ∀ a b, γ a b → Prop} (h : ∀ a b c, p a b c ↔ q a b c) :
+    (∃ a b c, p a b c) ↔ ∃ a b c, q a b c :=
+  exists_congr fun a => exists₂_congr <| h a
+
+variable {δ : ∀ a b, γ a b → Sort _}
+theorem forall₄_congr {p q : ∀ a b c, δ a b c → Prop} (h : ∀ a b c d, p a b c d ↔ q a b c d) :
+    (∀ a b c d, p a b c d) ↔ ∀ a b c d, q a b c d :=
+  forall_congr' fun a => forall₃_congr <| h a
+
+theorem exists₄_congr {p q : ∀ a b c, δ a b c → Prop} (h : ∀ a b c d, p a b c d ↔ q a b c d) :
+    (∃ a b c d, p a b c d) ↔ ∃ a b c d, q a b c d :=
+  exists_congr fun a => exists₃_congr <| h a
+
+variable {ε : ∀ a b c, δ a b c → Sort _}
+theorem forall₅_congr {p q : ∀ a b c d, ε a b c d → Prop}
+    (h : ∀ a b c d e, p a b c d e ↔ q a b c d e) :
+    (∀ a b c d e, p a b c d e) ↔ ∀ a b c d e, q a b c d e :=
+  forall_congr' fun a => forall₄_congr <| h a
+
+theorem exists₅_congr {p q : ∀ a b c d, ε a b c d → Prop}
+    (h : ∀ a b c d e, p a b c d e ↔ q a b c d e) :
+    (∃ a b c d e, p a b c d e) ↔ ∃ a b c d e, q a b c d e :=
+  exists_congr fun a => exists₄_congr <| h a
+
+end forall_congr
+
+@[simp] theorem not_exists : (¬∃ x, p x) ↔ ∀ x, ¬p x := exists_imp
+
+theorem forall_and : (∀ x, p x ∧ q x) ↔ (∀ x, p x) ∧ (∀ x, q x) :=
+  ⟨fun h => ⟨fun x => (h x).1, fun x => (h x).2⟩, fun ⟨h₁, h₂⟩ x => ⟨h₁ x, h₂ x⟩⟩
+
+theorem exists_or : (∃ x, p x ∨ q x) ↔ (∃ x, p x) ∨ ∃ x, q x :=
+  ⟨fun | ⟨x, .inl h⟩ => .inl ⟨x, h⟩ | ⟨x, .inr h⟩ => .inr ⟨x, h⟩,
+   fun | .inl ⟨x, h⟩ => ⟨x, .inl h⟩ | .inr ⟨x, h⟩ => ⟨x, .inr h⟩⟩
+
+@[simp] theorem exists_false : ¬(∃ _a : α, False) := fun ⟨_, h⟩ => h
+
+@[simp] theorem forall_const (α : Sort _) [i : Nonempty α] : (α → b) ↔ b :=
+  ⟨i.elim, fun hb _ => hb⟩
+
+theorem Exists.nonempty : (∃ x, p x) → Nonempty α | ⟨x, _⟩ => ⟨x⟩
+
+theorem not_forall_of_exists_not {p : α → Prop} : (∃ x, ¬p x) → ¬∀ x, p x
+  | ⟨x, hn⟩, h => hn (h x)
+
+@[simp] theorem forall_eq {p : α → Prop} {a' : α} : (∀ a, a = a' → p a) ↔ p a' :=
+  ⟨fun h => h a' rfl, fun h _ e => e.symm ▸ h⟩
+
+@[simp] theorem forall_eq' {a' : α} : (∀ a, a' = a → p a) ↔ p a' := by simp [@eq_comm _ a']
+
+@[simp] theorem exists_eq : ∃ a, a = a' := ⟨_, rfl⟩
+
+@[simp] theorem exists_eq' : ∃ a, a' = a := ⟨_, rfl⟩
+
+@[simp] theorem exists_eq_left : (∃ a, a = a' ∧ p a) ↔ p a' :=
+  ⟨fun ⟨_, e, h⟩ => e ▸ h, fun h => ⟨_, rfl, h⟩⟩
+
+@[simp] theorem exists_eq_right : (∃ a, p a ∧ a = a') ↔ p a' :=
+  (exists_congr <| by exact fun a => And.comm).trans exists_eq_left
+
+@[simp] theorem exists_and_left : (∃ x, b ∧ p x) ↔ b ∧ (∃ x, p x) :=
+  ⟨fun ⟨x, h, hp⟩ => ⟨h, x, hp⟩, fun ⟨h, x, hp⟩ => ⟨x, h, hp⟩⟩
+
+@[simp] theorem exists_and_right : (∃ x, p x ∧ b) ↔ (∃ x, p x) ∧ b := by simp [And.comm]
+
+@[simp] theorem exists_eq_left' : (∃ a, a' = a ∧ p a) ↔ p a' := by simp [@eq_comm _ a']
+
+@[simp] theorem forall_eq_or_imp : (∀ a, a = a' ∨ q a → p a) ↔ p a' ∧ ∀ a, q a → p a := by
+  simp only [or_imp, forall_and, forall_eq]
+
+@[simp] theorem exists_eq_or_imp : (∃ a, (a = a' ∨ q a) ∧ p a) ↔ p a' ∨ ∃ a, q a ∧ p a := by
+  simp only [or_and_right, exists_or, exists_eq_left]
+
+@[simp] theorem exists_eq_right_right : (∃ (a : α), p a ∧ q a ∧ a = a') ↔ p a' ∧ q a' := by
+  simp [← and_assoc]
+
+@[simp] theorem exists_eq_right_right' : (∃ (a : α), p a ∧ q a ∧ a' = a) ↔ p a' ∧ q a' := by
+  simp [@eq_comm _ a']
+
+@[simp] theorem exists_prop : (∃ _h : a, b) ↔ a ∧ b :=
+  ⟨fun ⟨hp, hq⟩ => ⟨hp, hq⟩, fun ⟨hp, hq⟩ => ⟨hp, hq⟩⟩
+
+@[simp] theorem exists_apply_eq_apply (f : α → β) (a' : α) : ∃ a, f a = f a' := ⟨a', rfl⟩
+
+theorem forall_prop_of_true {p : Prop} {q : p → Prop} (h : p) : (∀ h' : p, q h') ↔ q h :=
+  @forall_const (q h) p ⟨h⟩
+
+theorem forall_comm {p : α → β → Prop} : (∀ a b, p a b) ↔ (∀ b a, p a b) :=
+  ⟨fun h b a => h a b, fun h a b => h b a⟩
+
+theorem exists_comm {p : α → β → Prop} : (∃ a b, p a b) ↔ (∃ b a, p a b) :=
+  ⟨fun ⟨a, b, h⟩ => ⟨b, a, h⟩, fun ⟨b, a, h⟩ => ⟨a, b, h⟩⟩
+
+@[simp] theorem forall_apply_eq_imp_iff {f : α → β} {p : β → Prop} :
+    (∀ b a, f a = b → p b) ↔ ∀ a, p (f a) := by simp [forall_comm]
+
+@[simp] theorem forall_eq_apply_imp_iff {f : α → β} {p : β → Prop} :
+    (∀ b a, b = f a → p b) ↔ ∀ a, p (f a) := by simp [forall_comm]
+
+@[simp] theorem forall_apply_eq_imp_iff₂ {f : α → β} {p : α → Prop} {q : β → Prop} :
+    (∀ b a, p a → f a = b → q b) ↔ ∀ a, p a → q (f a) :=
+  ⟨fun h a ha => h (f a) a ha rfl, fun h _ a ha hb => hb ▸ h a ha⟩
+
+theorem forall_prop_of_false {p : Prop} {q : p → Prop} (hn : ¬p) : (∀ h' : p, q h') ↔ True :=
+  iff_true_intro fun h => hn.elim h
+
+end quantifiers
+
+/-! ## decidable -/
+
+theorem Decidable.not_not [Decidable p] : ¬¬p ↔ p := ⟨of_not_not, not_not_intro⟩
+
+theorem Decidable.by_contra [Decidable p] : (¬p → False) → p := of_not_not
+
+/-- Construct a non-Prop by cases on an `Or`, when the left conjunct is decidable. -/
+protected def Or.by_cases [Decidable p] {α : Sort u} (h : p ∨ q) (h₁ : p → α) (h₂ : q → α) : α :=
+  if hp : p then h₁ hp else h₂ (h.resolve_left hp)
+
+/-- Construct a non-Prop by cases on an `Or`, when the right conjunct is decidable. -/
+protected def Or.by_cases' [Decidable q] {α : Sort u} (h : p ∨ q) (h₁ : p → α) (h₂ : q → α) : α :=
+  if hq : q then h₂ hq else h₁ (h.resolve_right hq)
+
+instance exists_prop_decidable {p} (P : p → Prop)
+  [Decidable p] [∀ h, Decidable (P h)] : Decidable (∃ h, P h) :=
+if h : p then
+  decidable_of_decidable_of_iff ⟨fun h2 => ⟨h, h2⟩, fun ⟨_, h2⟩ => h2⟩
+else isFalse fun ⟨h', _⟩ => h h'
+
+instance forall_prop_decidable {p} (P : p → Prop)
+  [Decidable p] [∀ h, Decidable (P h)] : Decidable (∀ h, P h) :=
+if h : p then
+  decidable_of_decidable_of_iff ⟨fun h2 _ => h2, fun al => al h⟩
+else isTrue fun h2 => absurd h2 h
+
+theorem decide_eq_true_iff (p : Prop) [Decidable p] : (decide p = true) ↔ p := by simp
+
+@[simp] theorem decide_eq_false_iff_not (p : Prop) {_ : Decidable p} : (decide p = false) ↔ ¬p :=
+  ⟨of_decide_eq_false, decide_eq_false⟩
+
+@[simp] theorem decide_eq_decide {p q : Prop} {_ : Decidable p} {_ : Decidable q} :
+    decide p = decide q ↔ (p ↔ q) :=
+  ⟨fun h => by rw [← decide_eq_true_iff p, h, decide_eq_true_iff], fun h => by simp [h]⟩
+
+theorem Decidable.of_not_imp [Decidable a] (h : ¬(a → b)) : a :=
+  byContradiction (not_not_of_not_imp h)
+
+theorem Decidable.not_imp_symm [Decidable a] (h : ¬a → b) (hb : ¬b) : a :=
+  byContradiction <| hb ∘ h
+
+theorem Decidable.not_imp_comm [Decidable a] [Decidable b] : (¬a → b) ↔ (¬b → a) :=
+  ⟨not_imp_symm, not_imp_symm⟩
+
+theorem Decidable.not_imp_self [Decidable a] : (¬a → a) ↔ a := by
+  have := @imp_not_self (¬a); rwa [not_not] at this
+
+theorem Decidable.or_iff_not_imp_left [Decidable a] : a ∨ b ↔ (¬a → b) :=
+  ⟨Or.resolve_left, fun h => dite _ .inl (.inr ∘ h)⟩
+
+theorem Decidable.or_iff_not_imp_right [Decidable b] : a ∨ b ↔ (¬b → a) :=
+  or_comm.trans or_iff_not_imp_left
+
+theorem Decidable.not_imp_not [Decidable a] : (¬a → ¬b) ↔ (b → a) :=
+  ⟨fun h hb => byContradiction (h · hb), mt⟩
+
+theorem Decidable.not_or_of_imp [Decidable a] (h : a → b) : ¬a ∨ b :=
+  if ha : a then .inr (h ha) else .inl ha
+
+theorem Decidable.imp_iff_not_or [Decidable a] : (a → b) ↔ (¬a ∨ b) :=
+  ⟨not_or_of_imp, Or.neg_resolve_left⟩
+
+theorem Decidable.imp_iff_or_not [Decidable b] : b → a ↔ a ∨ ¬b :=
+  Decidable.imp_iff_not_or.trans or_comm
+
+theorem Decidable.imp_or [h : Decidable a] : (a → b ∨ c) ↔ (a → b) ∨ (a → c) :=
+  if h : a then by
+    rw [imp_iff_right h, imp_iff_right h, imp_iff_right h]
+  else by
+    rw [iff_false_intro h, false_imp_iff, false_imp_iff, true_or]
+
+theorem Decidable.imp_or' [Decidable b] : (a → b ∨ c) ↔ (a → b) ∨ (a → c) :=
+  if h : b then by simp [h] else by
+    rw [eq_false h, false_or]; exact (or_iff_right_of_imp fun hx x => (hx x).elim).symm
+
+theorem Decidable.not_imp_iff_and_not [Decidable a] : ¬(a → b) ↔ a ∧ ¬b :=
+  ⟨fun h => ⟨of_not_imp h, not_of_not_imp h⟩, not_imp_of_and_not⟩
+
+theorem Decidable.peirce (a b : Prop) [Decidable a] : ((a → b) → a) → a :=
+  if ha : a then fun _ => ha else fun h => h ha.elim
+
+theorem peirce' {a : Prop} (H : ∀ b : Prop, (a → b) → a) : a := H _ id
+
+theorem Decidable.not_iff_not [Decidable a] [Decidable b] : (¬a ↔ ¬b) ↔ (a ↔ b) := by
+  rw [@iff_def (¬a), @iff_def' a]; exact and_congr not_imp_not not_imp_not
+
+theorem Decidable.not_iff_comm [Decidable a] [Decidable b] : (¬a ↔ b) ↔ (¬b ↔ a) := by
+  rw [@iff_def (¬a), @iff_def (¬b)]; exact and_congr not_imp_comm imp_not_comm
+
+theorem Decidable.not_iff [Decidable b] : ¬(a ↔ b) ↔ (¬a ↔ b) :=
+  if h : b then by
+    rw [iff_true_right h, iff_true_right h]
+  else by
+    rw [iff_false_right h, iff_false_right h]
+
+theorem Decidable.iff_not_comm [Decidable a] [Decidable b] : (a ↔ ¬b) ↔ (b ↔ ¬a) := by
+  rw [@iff_def a, @iff_def b]; exact and_congr imp_not_comm not_imp_comm
+
+theorem Decidable.iff_iff_and_or_not_and_not {a b : Prop} [Decidable b] :
+    (a ↔ b) ↔ (a ∧ b) ∨ (¬a ∧ ¬b) :=
+  ⟨fun e => if h : b then .inl ⟨e.2 h, h⟩ else .inr ⟨mt e.1 h, h⟩,
+   Or.rec (And.rec iff_of_true) (And.rec iff_of_false)⟩
+
+theorem Decidable.iff_iff_not_or_and_or_not [Decidable a] [Decidable b] :
+    (a ↔ b) ↔ (¬a ∨ b) ∧ (a ∨ ¬b) := by
+  rw [iff_iff_implies_and_implies a b]; simp only [imp_iff_not_or, Or.comm]
+
+theorem Decidable.not_and_not_right [Decidable b] : ¬(a ∧ ¬b) ↔ (a → b) :=
+  ⟨fun h ha => not_imp_symm (And.intro ha) h, fun h ⟨ha, hb⟩ => hb <| h ha⟩
+
+theorem Decidable.not_and_iff_or_not_not [Decidable a] : ¬(a ∧ b) ↔ ¬a ∨ ¬b :=
+  ⟨fun h => if ha : a then .inr (h ⟨ha, ·⟩) else .inl ha, not_and_of_not_or_not⟩
+
+theorem Decidable.not_and_iff_or_not_not' [Decidable b] : ¬(a ∧ b) ↔ ¬a ∨ ¬b :=
+  ⟨fun h => if hb : b then .inl (h ⟨·, hb⟩) else .inr hb, not_and_of_not_or_not⟩
+
+theorem Decidable.or_iff_not_and_not [Decidable a] [Decidable b] : a ∨ b ↔ ¬(¬a ∧ ¬b) := by
+  rw [← not_or, not_not]
+
+theorem Decidable.and_iff_not_or_not [Decidable a] [Decidable b] : a ∧ b ↔ ¬(¬a ∨ ¬b) := by
+  rw [← not_and_iff_or_not_not, not_not]
+
+theorem Decidable.imp_iff_right_iff [Decidable a] : (a → b ↔ b) ↔ a ∨ b :=
+  ⟨fun H => (Decidable.em a).imp_right fun ha' => H.1 fun ha => (ha' ha).elim,
+   fun H => H.elim imp_iff_right fun hb => iff_of_true (fun _ => hb) hb⟩
+
+theorem Decidable.and_or_imp [Decidable a] : a ∧ b ∨ (a → c) ↔ a → b ∨ c :=
+  if ha : a then by simp only [ha, true_and, true_imp_iff]
+  else by simp only [ha, false_or, false_and, false_imp_iff]
+
+theorem Decidable.or_congr_left' [Decidable c] (h : ¬c → (a ↔ b)) : a ∨ c ↔ b ∨ c := by
+  rw [or_iff_not_imp_right, or_iff_not_imp_right]; exact imp_congr_right h
+
+theorem Decidable.or_congr_right' [Decidable a] (h : ¬a → (b ↔ c)) : a ∨ b ↔ a ∨ c := by
+  rw [or_iff_not_imp_left, or_iff_not_imp_left]; exact imp_congr_right h
+
+/-- Transfer decidability of `a` to decidability of `b`, if the propositions are equivalent.
+**Important**: this function should be used instead of `rw` on `Decidable b`, because the
+kernel will get stuck reducing the usage of `propext` otherwise,
+and `decide` will not work. -/
+@[inline] def decidable_of_iff (a : Prop) (h : a ↔ b) [Decidable a] : Decidable b :=
+  decidable_of_decidable_of_iff h
+
+/-- Transfer decidability of `b` to decidability of `a`, if the propositions are equivalent.
+This is the same as `decidable_of_iff` but the iff is flipped. -/
+@[inline] def decidable_of_iff' (b : Prop) (h : a ↔ b) [Decidable b] : Decidable a :=
+  decidable_of_decidable_of_iff h.symm
+
+instance Decidable.predToBool (p : α → Prop) [DecidablePred p] :
+    CoeDep (α → Prop) p (α → Bool) := ⟨fun b => decide <| p b⟩
+
+/-- Prove that `a` is decidable by constructing a boolean `b` and a proof that `b ↔ a`.
+(This is sometimes taken as an alternate definition of decidability.) -/
+def decidable_of_bool : ∀ (b : Bool), (b ↔ a) → Decidable a
+  | true, h => isTrue (h.1 rfl)
+  | false, h => isFalse (mt h.2 Bool.noConfusion)
+
+protected theorem Decidable.not_forall {p : α → Prop} [Decidable (∃ x, ¬p x)]
+    [∀ x, Decidable (p x)] : (¬∀ x, p x) ↔ ∃ x, ¬p x :=
+  ⟨Decidable.not_imp_symm fun nx x => Decidable.not_imp_symm (fun h => ⟨x, h⟩) nx,
+   not_forall_of_exists_not⟩
+
+protected theorem Decidable.not_forall_not {p : α → Prop} [Decidable (∃ x, p x)] :
+    (¬∀ x, ¬p x) ↔ ∃ x, p x :=
+  (@Decidable.not_iff_comm _ _ _ (decidable_of_iff (¬∃ x, p x) not_exists)).1 not_exists
+
+protected theorem Decidable.not_exists_not {p : α → Prop} [∀ x, Decidable (p x)] :
+    (¬∃ x, ¬p x) ↔ ∀ x, p x := by
+  simp only [not_exists, Decidable.not_not]

src/Init/SimpLemmas.lean

@@ -31,6 +31,9 @@ theorem eq_false_of_decide {p : Prop} {_ : Decidable p} (h : decide p = false) :
 theorem implies_congr {p₁ p₂ : Sort u} {q₁ q₂ : Sort v} (h₁ : p₁ = p₂) (h₂ : q₁ = q₂) : (p₁ → q₁) = (p₂ → q₂) :=
   h₁ ▸ h₂ ▸ rfl
 
+theorem iff_congr {p₁ p₂ q₁ q₂ : Prop} (h₁ : p₁ ↔ p₂) (h₂ : q₁ ↔ q₂) : (p₁ ↔ q₁) ↔ (p₂ ↔ q₂) :=
+  Iff.of_eq (propext h₁ ▸ propext h₂ ▸ rfl)
+
 theorem implies_dep_congr_ctx {p₁ p₂ q₁ : Prop} (h₁ : p₁ = p₂) {q₂ : p₂ → Prop} (h₂ : (h : p₂) → q₁ = q₂ h) : (p₁ → q₁) = ((h : p₂) → q₂ h) :=
   propext ⟨
     fun hl hp₂ => (h₂ hp₂).mp (hl (h₁.mpr hp₂)),
@@ -93,11 +96,16 @@ theorem dite_cond_eq_true {α : Sort u} {c : Prop} {_ : Decidable c} {t : c →
 theorem dite_cond_eq_false {α : Sort u} {c : Prop} {_ : Decidable c} {t : c → α} {e : ¬ c → α} (h : c = False) : (dite c t e) = e (of_eq_false h) := by simp [h]
 end SimprocHelperLemmas
 @[simp] theorem ite_self {α : Sort u} {c : Prop} {d : Decidable c} (a : α) : ite c a a = a := by cases d <;> rfl
-@[simp] theorem and_self (p : Prop) : (p ∧ p) = p := propext ⟨(·.1), fun h => ⟨h, h⟩⟩
+
 @[simp] theorem and_true (p : Prop) : (p ∧ True) = p := propext ⟨(·.1), (⟨·, trivial⟩)⟩
 @[simp] theorem true_and (p : Prop) : (True ∧ p) = p := propext ⟨(·.2), (⟨trivial, ·⟩)⟩
 @[simp] theorem and_false (p : Prop) : (p ∧ False) = False := eq_false (·.2)
 @[simp] theorem false_and (p : Prop) : (False ∧ p) = False := eq_false (·.1)
+@[simp] theorem and_self (p : Prop) : (p ∧ p) = p := propext ⟨(·.left), fun h => ⟨h, h⟩⟩
+@[simp] theorem and_not_self : ¬(a ∧ ¬a) | ⟨ha, hn⟩ => absurd ha hn
+@[simp] theorem not_and_self : ¬(¬a ∧ a) := and_not_self ∘ And.symm
+@[simp] theorem and_imp : (a ∧ b → c) ↔ (a → b → c) := ⟨fun h ha hb => h ⟨ha, hb⟩, fun h ⟨ha, hb⟩ => h ha hb⟩
+@[simp] theorem not_and : ¬(a ∧ b) ↔ (a → ¬b) := and_imp
 @[simp] theorem or_self (p : Prop) : (p ∨ p) = p := propext ⟨fun | .inl h | .inr h => h, .inl⟩
 @[simp] theorem or_true (p : Prop) : (p ∨ True) = True := eq_true (.inr trivial)
 @[simp] theorem true_or (p : Prop) : (True ∨ p) = True := eq_true (.inl trivial)
@@ -114,6 +122,58 @@ end SimprocHelperLemmas
 @[simp] theorem not_false_eq_true : (¬ False) = True := eq_true False.elim
 @[simp] theorem not_true_eq_false : (¬ True) = False := by decide
 
+@[simp] theorem not_iff_self : ¬(¬a ↔ a) | H => iff_not_self H.symm
+
+/-! ## and -/
+
+theorem and_congr_right (h : a → (b ↔ c)) : a ∧ b ↔ a ∧ c :=
+  Iff.intro (fun ⟨ha, hb⟩ => And.intro ha ((h ha).mp hb))
+            (fun ⟨ha, hb⟩ => And.intro ha ((h ha).mpr hb))
+theorem and_congr_left (h : c → (a ↔ b)) : a ∧ c ↔ b ∧ c :=
+  Iff.trans and_comm (Iff.trans (and_congr_right h) and_comm)
+
+theorem and_assoc : (a ∧ b) ∧ c ↔ a ∧ (b ∧ c) :=
+  Iff.intro (fun ⟨⟨ha, hb⟩, hc⟩ => ⟨ha, hb, hc⟩)
+            (fun ⟨ha, hb, hc⟩ => ⟨⟨ha, hb⟩, hc⟩)
+
+@[simp] theorem and_self_left  : a ∧ (a ∧ b) ↔ a ∧ b := by rw [←propext and_assoc, and_self]
+@[simp] theorem and_self_right : (a ∧ b) ∧ b ↔ a ∧ b := by rw [ propext and_assoc, and_self]
+
+@[simp] theorem and_congr_right_iff : (a ∧ b ↔ a ∧ c) ↔ (a → (b ↔ c)) :=
+  Iff.intro (fun h ha => by simp [ha] at h; exact h) and_congr_right
+@[simp] theorem and_congr_left_iff : (a ∧ c ↔ b ∧ c) ↔ c → (a ↔ b) := by
+  rw [@and_comm _ c, @and_comm _ c, ← and_congr_right_iff]
+
+theorem and_iff_left_of_imp  (h : a → b) : (a ∧ b) ↔ a := Iff.intro And.left (fun ha => And.intro ha (h ha))
+theorem and_iff_right_of_imp (h : b → a) : (a ∧ b) ↔ b := Iff.trans And.comm (and_iff_left_of_imp h)
+
+@[simp] theorem and_iff_left_iff_imp  : ((a ∧ b) ↔ a) ↔ (a → b) := Iff.intro (And.right ∘ ·.mpr) and_iff_left_of_imp
+@[simp] theorem and_iff_right_iff_imp : ((a ∧ b) ↔ b) ↔ (b → a) := Iff.intro (And.left ∘ ·.mpr) and_iff_right_of_imp
+
+@[simp] theorem iff_self_and : (p ↔ p ∧ q) ↔ (p → q) := by rw [@Iff.comm p, and_iff_left_iff_imp]
+@[simp] theorem iff_and_self : (p ↔ q ∧ p) ↔ (p → q) := by rw [and_comm, iff_self_and]
+
+/-! ## or -/
+
+theorem Or.imp (f : a → c) (g : b → d) (h : a ∨ b) : c ∨ d := h.elim (inl ∘ f) (inr ∘ g)
+theorem Or.imp_left (f : a → b) : a ∨ c → b ∨ c := .imp f id
+theorem Or.imp_right (f : b → c) : a ∨ b → a ∨ c := .imp id f
+
+theorem or_assoc : (a ∨ b) ∨ c ↔ a ∨ (b ∨ c) :=
+  Iff.intro (.rec (.imp_right .inl) (.inr ∘ .inr))
+            (.rec (.inl ∘ .inl) (.imp_left .inr))
+
+@[simp] theorem or_self_left  : a ∨ (a ∨ b) ↔ a ∨ b := by rw [←propext or_assoc, or_self]
+@[simp] theorem or_self_right : (a ∨ b) ∨ b ↔ a ∨ b := by rw [ propext or_assoc, or_self]
+
+theorem or_iff_right_of_imp (ha : a → b) : (a ∨ b) ↔ b := Iff.intro (Or.rec ha id) .inr
+theorem or_iff_left_of_imp  (hb : b → a) : (a ∨ b) ↔ a  := Iff.intro (Or.rec id hb) .inl
+
+@[simp] theorem or_iff_left_iff_imp  : (a ∨ b ↔ a) ↔ (b → a) := Iff.intro (·.mp ∘ Or.inr) or_iff_left_of_imp
+@[simp] theorem or_iff_right_iff_imp : (a ∨ b ↔ b) ↔ (a → b) := by rw [or_comm, or_iff_left_iff_imp]
+
+/-# Bool -/
+
 @[simp] theorem Bool.or_false (b : Bool) : (b || false) = b  := by cases b <;> rfl
 @[simp] theorem Bool.or_true (b : Bool) : (b || true) = true := by cases b <;> rfl
 @[simp] theorem Bool.false_or (b : Bool) : (false || b) = b  := by cases b <;> rfl
@@ -166,11 +226,13 @@ theorem Bool.or_assoc (a b c : Bool) : (a || b || c) = (a || (b || c)) := by
 @[simp] theorem bne_self_eq_false [BEq α] [LawfulBEq α] (a : α) : (a != a) = false := by simp [bne]
 @[simp] theorem bne_self_eq_false' [DecidableEq α] (a : α) : (a != a) = false := by simp [bne]
 
-@[simp] theorem Nat.le_zero_eq (a : Nat) : (a ≤ 0) = (a = 0) :=
-  propext ⟨fun h => Nat.le_antisymm h (Nat.zero_le ..), fun h => by rw [h]; decide⟩
-
 @[simp] theorem decide_False : decide False = false := rfl
 @[simp] theorem decide_True : decide True = true := rfl
 
 @[simp] theorem bne_iff_ne [BEq α] [LawfulBEq α] (a b : α) : a != b ↔ a ≠ b := by
   simp [bne]; rw [← beq_iff_eq a b]; simp [-beq_iff_eq]
+
+/-# Nat -/
+
+@[simp] theorem Nat.le_zero_eq (a : Nat) : (a ≤ 0) = (a = 0) :=
+  propext ⟨fun h => Nat.le_antisymm h (Nat.zero_le ..), fun h => by rw [h]; decide⟩

src/Init/Tactics.lean

@@ -941,6 +941,21 @@ syntax (name := repeat1') "repeat1' " tacticSeq : tactic
 syntax "and_intros" : tactic
 macro_rules | `(tactic| and_intros) => `(tactic| repeat' refine And.intro ?_ ?_)
 
+/--
+`subst_eq` repeatedly substitutes according to the equality proof hypotheses in the context,
+replacing the left side of the equality with the right, until no more progress can be made.
+-/
+syntax (name := substEqs) "subst_eqs" : tactic
+
+/-- The `run_tac doSeq` tactic executes code in `TacticM Unit`. -/
+syntax (name := runTac) "run_tac " doSeq : tactic
+
+/-- `haveI` behaves like `have`, but inlines the value instead of producing a `let_fun` term. -/
+macro "haveI" d:haveDecl : tactic => `(tactic| refine_lift haveI $d:haveDecl; ?_)
+
+/-- `letI` behaves like `let`, but inlines the value instead of producing a `let_fun` term. -/
+macro "letI" d:haveDecl : tactic => `(tactic| refine_lift letI $d:haveDecl; ?_)
+
 end Tactic
 
 namespace Attr

src/Init/WF.lean

@@ -206,12 +206,39 @@ protected inductive Lex : α × β → α × β → Prop where
   | left  {a₁} (b₁) {a₂} (b₂) (h : ra a₁ a₂) : Prod.Lex (a₁, b₁) (a₂, b₂)
   | right (a) {b₁ b₂} (h : rb b₁ b₂)         : Prod.Lex (a, b₁)  (a, b₂)
 
+theorem lex_def (r : α → α → Prop) (s : β → β → Prop) {p q : α × β} :
+    Prod.Lex r s p q ↔ r p.1 q.1 ∨ p.1 = q.1 ∧ s p.2 q.2 :=
+  ⟨fun h => by cases h <;> simp [*], fun h =>
+    match p, q, h with
+    | (a, b), (c, d), Or.inl h => Lex.left _ _ h
+    | (a, b), (c, d), Or.inr ⟨e, h⟩ => by subst e; exact Lex.right _ h⟩
+
+namespace Lex
+
+instance [αeqDec : DecidableEq α] {r : α → α → Prop} [rDec : DecidableRel r]
+    {s : β → β → Prop} [sDec : DecidableRel s] : DecidableRel (Prod.Lex r s)
+  | (a, b), (a', b') =>
+    match rDec a a' with
+    | isTrue raa' => isTrue $ left b b' raa'
+    | isFalse nraa' =>
+      match αeqDec a a' with
+      | isTrue eq => by
+        subst eq
+        cases sDec b b' with
+        | isTrue sbb' => exact isTrue $ right a sbb'
+        | isFalse nsbb' =>
+          apply isFalse; intro contra; cases contra <;> contradiction
+      | isFalse neqaa' => by
+        apply isFalse; intro contra; cases contra <;> contradiction
+
 -- TODO: generalize
-def Lex.right' {a₁ : Nat} {b₁ : β} (h₁ : a₁ ≤ a₂) (h₂ : rb b₁ b₂) : Prod.Lex Nat.lt rb (a₁, b₁) (a₂, b₂) :=
+def right' {a₁ : Nat} {b₁ : β} (h₁ : a₁ ≤ a₂) (h₂ : rb b₁ b₂) : Prod.Lex Nat.lt rb (a₁, b₁) (a₂, b₂) :=
   match Nat.eq_or_lt_of_le h₁ with
   | Or.inl h => h ▸ Prod.Lex.right a₁ h₂
   | Or.inr h => Prod.Lex.left b₁ _ h
 
+end Lex
+
 -- relational product based on ra and rb
 inductive RProd : α × β → α × β → Prop where
   | intro {a₁ b₁ a₂ b₂} (h₁ : ra a₁ a₂) (h₂ : rb b₁ b₂) : RProd (a₁, b₁) (a₂, b₂)

src/Lean/Elab.lean

@@ -10,6 +10,7 @@ import Lean.Elab.Command
 import Lean.Elab.Term
 import Lean.Elab.App
 import Lean.Elab.Binders
+import Lean.Elab.BinderPredicates
 import Lean.Elab.LetRec
 import Lean.Elab.Frontend
 import Lean.Elab.BuiltinNotation

src/Lean/Elab/BinderPredicates.lean

@@ -0,0 +1,41 @@
+/-
+Copyright (c) 2021 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Gabriel Ebner
+-/
+import Lean.Parser.Syntax
+import Lean.Elab.MacroArgUtil
+import Lean.Linter.MissingDocs
+
+namespace Lean.Elab.Command
+
+@[builtin_command_elab binderPredicate] def elabBinderPred : CommandElab := fun stx => do
+  match stx with
+  | `($[$doc?:docComment]? $[@[$attrs?,*]]? $attrKind:attrKind binder_predicate%$tk
+      $[(name := $name?)]? $[(priority := $prio?)]? $x $args:macroArg* => $rhs) => do
+    let prio ← liftMacroM do evalOptPrio prio?
+    let (stxParts, patArgs) := (← args.mapM expandMacroArg).unzip
+    let name ← match name? with
+      | some name => pure name.getId
+      | none => liftMacroM do mkNameFromParserSyntax `binderTerm (mkNullNode stxParts)
+    let nameTk := name?.getD (mkIdentFrom tk name)
+    /- The command `syntax [<kind>] ...` adds the current namespace to the syntax node kind.
+    So, we must include current namespace when we create a pattern for the following
+    `macro_rules` commands. -/
+    let pat : TSyntax `binderPred := ⟨(mkNode ((← getCurrNamespace) ++ name) patArgs).1⟩
+    elabCommand <|<-
+    `($[$doc?:docComment]? $[@[$attrs?,*]]? $attrKind:attrKind syntax%$tk
+        (name := $nameTk) (priority := $(quote prio)) $[$stxParts]* : binderPred
+      $[$doc?:docComment]? macro_rules%$tk
+        | `(satisfies_binder_pred% $$($x):term $pat:binderPred) => $rhs)
+  | _ => throwUnsupportedSyntax
+
+open Linter.MissingDocs Parser Term in
+/-- Missing docs handler for `binder_predicate` -/
+@[builtin_missing_docs_handler Lean.Parser.Command.binderPredicate]
+def checkBinderPredicate : SimpleHandler := fun stx => do
+  if stx[0].isNone && stx[2][0][0].getKind != ``«local» then
+    if stx[4].isNone then lint stx[3] "binder predicate"
+    else lintNamed stx[4][0][3] "binder predicate"
+
+end Lean.Elab.Command

src/Lean/Elab/BuiltinCommand.lean

@@ -704,6 +704,39 @@ unsafe def elabEvalUnsafe : CommandElab
 @[builtin_command_elab «eval», implemented_by elabEvalUnsafe]
 opaque elabEval : CommandElab
 
+private def checkImportsForRunCmds : CommandElabM Unit := do
+  unless (← getEnv).contains ``CommandElabM do
+    throwError "to use this command, include `import Lean.Elab.Command`"
+
+@[builtin_command_elab runCmd]
+def elabRunCmd : CommandElab
+  | `(run_cmd $elems:doSeq) => do
+    checkImportsForRunCmds
+    (← liftTermElabM <| Term.withDeclName `_run_cmd <|
+      unsafe Term.evalTerm (CommandElabM Unit)
+        (mkApp (mkConst ``CommandElabM) (mkConst ``Unit))
+        (← `(discard do $elems)))
+  | _ => throwUnsupportedSyntax
+
+@[builtin_command_elab runElab]
+def elabRunElab : CommandElab
+  | `(run_elab $elems:doSeq) => do
+    checkImportsForRunCmds
+    (← liftTermElabM <| Term.withDeclName `_run_elab <|
+      unsafe Term.evalTerm (CommandElabM Unit)
+        (mkApp (mkConst ``CommandElabM) (mkConst ``Unit))
+        (← `(Command.liftTermElabM <| discard do $elems)))
+  | _ => throwUnsupportedSyntax
+
+@[builtin_command_elab runMeta]
+def elabRunMeta : CommandElab := fun stx =>
+  match stx with
+  | `(run_meta $elems:doSeq) => do
+     checkImportsForRunCmds
+     let stxNew ← `(command| run_elab (show Lean.Meta.MetaM Unit from do $elems))
+     withMacroExpansion stx stxNew do elabCommand stxNew
+  | _ => throwUnsupportedSyntax
+
 @[builtin_command_elab «synth»] def elabSynth : CommandElab := fun stx => do
   let term := stx[1]
   withoutModifyingEnv <| runTermElabM fun _ => Term.withDeclName `_synth_cmd do

src/Lean/Elab/BuiltinNotation.lean

@@ -7,8 +7,10 @@ import Lean.Compiler.BorrowedAnnotation
 import Lean.Meta.KAbstract
 import Lean.Meta.Closure
 import Lean.Meta.MatchUtil
-import Lean.Elab.SyntheticMVars
 import Lean.Compiler.ImplementedByAttr
+import Lean.Elab.SyntheticMVars
+import Lean.Elab.Eval
+import Lean.Elab.Binders
 
 namespace Lean.Elab.Term
 open Meta
@@ -427,12 +429,6 @@ private def withLocalIdentFor (stx : Term) (e : Expr) (k : Term → TermElabM Ex
   let e ← elabTerm stx[1] expectedType?
   return DiscrTree.mkNoindexAnnotation e
 
--- TODO: investigate whether we need this function
-private def mkAuxNameForElabUnsafe (hint : Name) : TermElabM Name :=
-  withFreshMacroScope do
-    let name := (← getDeclName?).getD Name.anonymous ++ hint
-    return addMacroScope (← getMainModule) name (← getCurrMacroScope)
-
 @[builtin_term_elab «unsafe»]
 def elabUnsafe : TermElab := fun stx expectedType? =>
   match stx with
@@ -443,7 +439,7 @@ def elabUnsafe : TermElab := fun stx expectedType? =>
     let t ← mkAuxDefinitionFor (← mkAuxName `unsafe) t
     let .const unsafeFn unsafeLvls .. := t.getAppFn | unreachable!
     let .defnInfo unsafeDefn ← getConstInfo unsafeFn | unreachable!
-    let implName ← mkAuxNameForElabUnsafe `impl
+    let implName ← mkAuxName `unsafe_impl
     addDecl <| Declaration.defnDecl {
       name        := implName
       type        := unsafeDefn.type
@@ -456,4 +452,44 @@ def elabUnsafe : TermElab := fun stx expectedType? =>
     return mkAppN (Lean.mkConst implName unsafeLvls) t.getAppArgs
   | _ => throwUnsupportedSyntax
 
+/-- Elaborator for `by_elab`. -/
+@[builtin_term_elab byElab] def elabRunElab : TermElab := fun stx expectedType? =>
+  match stx with
+  | `(by_elab $cmds:doSeq) => do
+    if let `(Lean.Parser.Term.doSeq| $e:term) := cmds then
+      if e matches `(Lean.Parser.Term.doSeq| fun $[$_args]* => $_) then
+        let tac ← unsafe evalTerm
+          (Option Expr → TermElabM Expr)
+          (Lean.mkForall `x .default
+            (mkApp (Lean.mkConst ``Option) (Lean.mkConst ``Expr))
+            (mkApp (Lean.mkConst ``TermElabM) (Lean.mkConst ``Expr))) e
+        return ← tac expectedType?
+    (← unsafe evalTerm (TermElabM Expr) (mkApp (Lean.mkConst ``TermElabM) (Lean.mkConst ``Expr))
+      (← `(do $cmds)))
+  | _ => throwUnsupportedSyntax
+
+@[builtin_term_elab Lean.Parser.Term.haveI] def elabHaveI : TermElab := fun stx expectedType? => do
+  match stx with
+  | `(haveI $x:ident $bs* : $ty := $val; $body) =>
+    withExpectedType expectedType? fun expectedType => do
+      let (ty, val) ← elabBinders bs fun bs => do
+        let ty ← elabType ty
+        let val ← elabTermEnsuringType val ty
+        pure (← mkForallFVars bs ty, ← mkLambdaFVars bs val)
+      withLocalDeclD x.getId ty fun x => do
+        return (← (← elabTerm body expectedType).abstractM #[x]).instantiate #[val]
+  | _ => throwUnsupportedSyntax
+
+@[builtin_term_elab Lean.Parser.Term.letI] def elabLetI : TermElab := fun stx expectedType? => do
+  match stx with
+  | `(letI $x:ident $bs* : $ty := $val; $body) =>
+    withExpectedType expectedType? fun expectedType => do
+      let (ty, val) ← elabBinders bs fun bs => do
+        let ty ← elabType ty
+        let val ← elabTermEnsuringType val ty
+        pure (← mkForallFVars bs ty, ← mkLambdaFVars bs val)
+      withLetDecl x.getId ty val fun x => do
+        return (← (← elabTerm body expectedType).abstractM #[x]).instantiate #[val]
+  | _ => throwUnsupportedSyntax
+
 end Lean.Elab.Term

src/Lean/Elab/ElabRules.lean

@@ -11,12 +11,6 @@ open Lean.Syntax
 open Lean.Parser.Term hiding macroArg
 open Lean.Parser.Command
 
-def withExpectedType (expectedType? : Option Expr) (x : Expr → TermElabM Expr) : TermElabM Expr := do
-  Term.tryPostponeIfNoneOrMVar expectedType?
-  let some expectedType ← pure expectedType?
-    | throwError "expected type must be known"
-  x expectedType
-
 def elabElabRulesAux (doc? : Option (TSyntax ``docComment))
     (attrs? : Option (TSepArray ``attrInstance ",")) (attrKind : TSyntax ``attrKind)
     (k : SyntaxNodeKind) (cat? expty? : Option (Ident)) (alts : Array (TSyntax ``matchAlt)) :
@@ -54,7 +48,7 @@ def elabElabRulesAux (doc? : Option (TSyntax ``docComment))
     if catName == `term then
       `($[$doc?:docComment]? @[$(← mkAttrs `term_elab),*]
         aux_def elabRules $(mkIdent k) : Lean.Elab.Term.TermElab :=
-        fun stx expectedType? => Lean.Elab.Command.withExpectedType expectedType? fun $expId => match stx with
+        fun stx expectedType? => Lean.Elab.Term.withExpectedType expectedType? fun $expId => match stx with
           $alts:matchAlt* | _ => no_error_if_unused% throwUnsupportedSyntax)
     else
       throwErrorAt expId "syntax category '{catName}' does not support expected type specification"

src/Lean/Elab/Eval.lean

@@ -9,7 +9,7 @@ import Lean.Elab.SyntheticMVars
 namespace Lean.Elab.Term
 open Meta
 
-unsafe def evalTerm (α) (type : Expr) (value : Syntax) (safety := DefinitionSafety.safe) : TermElabM α := do
+unsafe def evalTerm (α) (type : Expr) (value : Syntax) (safety := DefinitionSafety.safe) : TermElabM α := withoutModifyingEnv do
   let v ← elabTermEnsuringType value type
   synthesizeSyntheticMVarsNoPostponing
   let v ← instantiateMVars v

src/Lean/Elab/Tactic.lean

@@ -26,4 +26,5 @@ import Lean.Elab.Tactic.Congr
 import Lean.Elab.Tactic.Guard
 import Lean.Elab.Tactic.RCases
 import Lean.Elab.Tactic.Repeat
+import Lean.Elab.Tactic.Ext
 import Lean.Elab.Tactic.Change

src/Lean/Elab/Tactic/BuiltinTactic.lean

@@ -9,6 +9,7 @@ import Lean.Meta.Tactic.Contradiction
 import Lean.Meta.Tactic.Refl
 import Lean.Elab.Binders
 import Lean.Elab.Open
+import Lean.Elab.Eval
 import Lean.Elab.SetOption
 import Lean.Elab.Tactic.Basic
 import Lean.Elab.Tactic.ElabTerm
@@ -325,11 +326,8 @@ def forEachVar (hs : Array Syntax) (tac : MVarId → FVarId → MetaM MVarId) :
 @[builtin_tactic Lean.Parser.Tactic.substVars] def evalSubstVars : Tactic := fun _ =>
   liftMetaTactic fun mvarId => return [← substVars mvarId]
 
-/--
-`subst_eq` repeatedly substitutes according to the equality proof hypotheses in the context,
-replacing the left side of the equality with the right, until no more progress can be made.
--/
-elab "subst_eqs" : tactic => Elab.Tactic.liftMetaTactic1 (·.substEqs)
+@[builtin_tactic Lean.Parser.Tactic.substEqs] def evalSubstEqs : Tactic := fun _ =>
+  Elab.Tactic.liftMetaTactic1 (·.substEqs)
 
 /--
   Searches for a metavariable `g` s.t. `tag` is its exact name.
@@ -496,4 +494,11 @@ where
       liftMetaTactic1 (·.tryClearMany toClear)
   | _ => throwUnsupportedSyntax
 
+@[builtin_tactic runTac] def evalRunTac : Tactic := fun stx => do
+  match stx with
+  | `(tactic| run_tac $e:doSeq) =>
+    ← unsafe Term.evalTerm (TacticM Unit) (mkApp (Lean.mkConst ``TacticM) (Lean.mkConst ``Unit))
+      (← `(discard do $e))
+  | _ => throwUnsupportedSyntax
+
 end Lean.Elab.Tactic

src/Lean/Elab/Tactic/Ext.lean

@@ -0,0 +1,269 @@
+/-
+Copyright (c) 2021 Gabriel Ebner. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Gabriel Ebner, Mario Carneiro
+-/
+import Lean.Elab.Tactic.RCases
+import Lean.Elab.Tactic.Repeat
+import Lean.Elab.Tactic.BuiltinTactic
+import Lean.Elab.Command
+import Lean.Linter.Util
+
+namespace Lean.Elab.Tactic.Ext
+open Meta Term
+/-- Information about an extensionality theorem, stored in the environment extension. -/
+structure ExtTheorem where
+  /-- Declaration name of the extensionality theorem. -/
+  declName : Name
+  /-- Priority of the extensionality theorem. -/
+  priority : Nat
+  /--
+  Key in the discrimination tree,
+  for the type in which the extensionality theorem holds.
+  -/
+  keys : Array DiscrTree.Key
+  deriving Inhabited, Repr, BEq, Hashable
+
+/-- The state of the `ext` extension environment -/
+structure ExtTheorems where
+  /-- The tree of `ext` extensions. -/
+  tree   : DiscrTree ExtTheorem := {}
+  /-- Erased `ext`s via `attribute [-ext]`. -/
+  erased  : PHashSet Name := {}
+  deriving Inhabited
+
+/-- Discrimation tree settings for the `ext` extension. -/
+def extExt.config : WhnfCoreConfig := {}
+
+/-- The environment extension to track `@[ext]` theorems. -/
+builtin_initialize extExtension :
+    SimpleScopedEnvExtension ExtTheorem ExtTheorems ←
+  registerSimpleScopedEnvExtension {
+    addEntry := fun { tree, erased } thm =>
+      { tree := tree.insertCore thm.keys thm, erased := erased.erase thm.declName }
+    initial := {}
+  }
+
+/-- Gets the list of `@[ext]` theorems corresponding to the key `ty`,
+ordered from high priority to low. -/
+@[inline] def getExtTheorems (ty : Expr) : MetaM (Array ExtTheorem) := do
+  let extTheorems := extExtension.getState (← getEnv)
+  let arr ← extTheorems.tree.getMatch ty extExt.config
+  let erasedArr := arr.filter fun thm => !extTheorems.erased.contains thm.declName
+  -- Using insertion sort because it is stable and the list of matches should be mostly sorted.
+  -- Most ext theorems have default priority.
+  return erasedArr.insertionSort (·.priority < ·.priority) |>.reverse
+
+/--
+Erases a name marked `ext` by adding it to the state's `erased` field and
+removing it from the state's list of `Entry`s.
+
+This is triggered by `attribute [-ext] name`.
+-/
+def ExtTheorems.eraseCore (d : ExtTheorems) (declName : Name) : ExtTheorems :=
+ { d with erased := d.erased.insert declName }
+
+/--
+  Erases a name marked as a `ext` attribute.
+  Check that it does in fact have the `ext` attribute by making sure it names a `ExtTheorem`
+  found somewhere in the state's tree, and is not erased.
+-/
+def ExtTheorems.erase [Monad m] [MonadError m] (d : ExtTheorems) (declName : Name) :
+    m ExtTheorems := do
+  unless d.tree.containsValueP (·.declName == declName) && !d.erased.contains declName do
+    throwError "'{declName}' does not have [ext] attribute"
+  return d.eraseCore declName
+
+builtin_initialize registerBuiltinAttribute {
+  name := `ext
+  descr := "Marks a theorem as an extensionality theorem"
+  add := fun declName stx kind => do
+    let `(attr| ext $[(flat := $f)]? $(prio)?) := stx
+      | throwError "unexpected @[ext] attribute {stx}"
+    if isStructure (← getEnv) declName then
+      liftCommandElabM <| Elab.Command.elabCommand <|
+        ← `(declare_ext_theorems_for $[(flat := $f)]? $(mkCIdentFrom stx declName) $[$prio]?)
+    else MetaM.run' do
+      if let some flat := f then
+        throwErrorAt flat "unexpected 'flat' config on @[ext] theorem"
+      let declTy := (← getConstInfo declName).type
+      let (_, _, declTy) ← withDefault <| forallMetaTelescopeReducing declTy
+      let failNotEq := throwError
+        "@[ext] attribute only applies to structures or theorems proving x = y, got {declTy}"
+      let some (ty, lhs, rhs) := declTy.eq? | failNotEq
+      unless lhs.isMVar && rhs.isMVar do failNotEq
+      let keys ← withReducible <| DiscrTree.mkPath ty extExt.config
+      let priority ← liftCommandElabM do Elab.liftMacroM do
+        evalPrio (prio.getD (← `(prio| default)))
+      extExtension.add {declName, keys, priority} kind
+  erase := fun declName => do
+    let s := extExtension.getState (← getEnv)
+    let s ← s.erase declName
+    modifyEnv fun env => extExtension.modifyState env fun _ => s
+}
+
+/--
+Constructs the hypotheses for the structure extensionality theorem that
+states that two structures are equal if their fields are equal.
+
+Calls the continuation `k` with the list of parameters to the structure,
+two structure variables `x` and `y`, and a list of pairs `(field, ty)`
+where `ty` is `x.field = y.field` or `HEq x.field y.field`.
+
+If `flat` parses to `true`, any fields inherited from parent structures
+are treated fields of the given structure type.
+If it is `false`, then the behind-the-scenes encoding of inherited fields
+is visible in the extensionality lemma.
+-/
+-- TODO: this is probably the wrong place to have this function
+def withExtHyps (struct : Name) (flat : Term)
+    (k : Array Expr → (x y : Expr) → Array (Name × Expr) → MetaM α) : MetaM α := do
+  let flat ← match flat with
+  | `(true) => pure true
+  | `(false) => pure false
+  | _ => throwErrorAt flat "expected 'true' or 'false'"
+  unless isStructure (← getEnv) struct do throwError "not a structure: {struct}"
+  let structC ← mkConstWithLevelParams struct
+  forallTelescope (← inferType structC) fun params _ => do
+  withNewBinderInfos (params.map (·.fvarId!, BinderInfo.implicit)) do
+  withLocalDeclD `x (mkAppN structC params) fun x => do
+  withLocalDeclD `y (mkAppN structC params) fun y => do
+    let mut hyps := #[]
+    let fields := if flat then
+      getStructureFieldsFlattened (← getEnv) struct (includeSubobjectFields := false)
+    else
+      getStructureFields (← getEnv) struct
+    for field in fields do
+      let x_f ← mkProjection x field
+      let y_f ← mkProjection y field
+      if ← isProof x_f then
+        pure ()
+      else if ← isDefEq (← inferType x_f) (← inferType y_f) then
+        hyps := hyps.push (field, ← mkEq x_f y_f)
+      else
+        hyps := hyps.push (field, ← mkHEq x_f y_f)
+    k params x y hyps
+
+/--
+Creates the type of the extensionality theorem for the given structure,
+elaborating to `x.1 = y.1 → x.2 = y.2 → x = y`, for example.
+-/
+@[builtin_term_elab extType] def elabExtType : TermElab := fun stx _ => do
+  match stx with
+  | `(ext_type%  $flat:term $struct:ident) => do
+    withExtHyps (← resolveGlobalConstNoOverloadWithInfo struct) flat fun params x y hyps => do
+      let ty := hyps.foldr (init := ← mkEq x y) fun (f, h) ty =>
+        mkForall f BinderInfo.default h ty
+      mkForallFVars (params |>.push x |>.push y) ty
+  | _ => throwUnsupportedSyntax
+
+/--
+Creates the type of the iff-variant of the extensionality theorem for the given structure,
+elaborating to `x = y ↔ x.1 = y.1 ∧ x.2 = y.2`, for example.
+-/
+@[builtin_term_elab extIffType] def elabExtIffType : TermElab := fun stx _ => do
+  match stx with
+  | `(ext_iff_type% $flat:term $struct:ident) => do
+    withExtHyps (← resolveGlobalConstNoOverloadWithInfo struct) flat fun params x y hyps => do
+      mkForallFVars (params |>.push x |>.push y) <|
+        mkIff (← mkEq x y) <| mkAndN (hyps.map (·.2)).toList
+  | _ => throwUnsupportedSyntax
+
+/-- Apply a single extensionality theorem to `goal`. -/
+def applyExtTheoremAt (goal : MVarId) : MetaM (List MVarId) := goal.withContext do
+  let tgt ← goal.getType'
+  unless tgt.isAppOfArity ``Eq 3 do
+    throwError "applyExtTheorem only applies to equations, not{indentExpr tgt}"
+  let ty := tgt.getArg! 0
+  let s ← saveState
+  for lem in ← getExtTheorems ty do
+    try
+      -- Note: We have to do this extra check to ensure that we don't apply e.g.
+      -- funext to a goal `(?a₁ : ?b) = ?a₂` to produce `(?a₁ x : ?b') = ?a₂ x`,
+      -- since this will loop.
+      -- We require that the type of the equality is not changed by the `goal.apply c` line
+      -- TODO: add flag to apply tactic to toggle unification vs. matching
+      withNewMCtxDepth do
+        let c ← mkConstWithFreshMVarLevels lem.declName
+        let (_, _, declTy) ← withDefault <| forallMetaTelescopeReducing (← inferType c)
+        guard (← isDefEq tgt declTy)
+      -- We use `newGoals := .all` as this is
+      -- more useful in practice with dependently typed arguments of `@[ext]` theorems.
+      return ← goal.apply (cfg := { newGoals := .all }) (← mkConstWithFreshMVarLevels lem.declName)
+    catch _ => s.restore
+  throwError "no applicable extensionality theorem found for{indentExpr ty}"
+
+/-- Apply a single extensionality theorem to the current goal. -/
+@[builtin_tactic applyExtTheorem] def evalApplyExtTheorem : Tactic := fun _ => do
+  liftMetaTactic applyExtTheoremAt
+
+/--
+Postprocessor for `withExt` which runs `rintro` with the given patterns when the target is a
+pi type.
+-/
+def tryIntros [Monad m] [MonadLiftT TermElabM m] (g : MVarId) (pats : List (TSyntax `rcasesPat))
+    (k : MVarId → List (TSyntax `rcasesPat) → m Nat) : m Nat := do
+  match pats with
+  | [] => k (← (g.intros : TermElabM _)).2 []
+  | p::ps =>
+    if (← (g.withContext g.getType' : TermElabM _)).isForall then
+      let mut n := 0
+      for g in ← RCases.rintro #[p] none g do
+        n := n.max (← tryIntros g ps k)
+      pure (n + 1)
+    else k g pats
+
+/--
+Applies a single extensionality theorem, using `pats` to introduce variables in the result.
+Runs continuation `k` on each subgoal.
+-/
+def withExt1 [Monad m] [MonadLiftT TermElabM m] (g : MVarId) (pats : List (TSyntax `rcasesPat))
+    (k : MVarId → List (TSyntax `rcasesPat) → m Nat) : m Nat := do
+  let mut n := 0
+  for g in ← (applyExtTheoremAt g : TermElabM _) do
+    n := n.max (← tryIntros g pats k)
+  pure n
+
+/--
+Applies extensionality theorems recursively, using `pats` to introduce variables in the result.
+Runs continuation `k` on each subgoal.
+-/
+def withExtN [Monad m] [MonadLiftT TermElabM m] [MonadExcept Exception m]
+    (g : MVarId) (pats : List (TSyntax `rcasesPat)) (k : MVarId → List (TSyntax `rcasesPat) → m Nat)
+    (depth := 1000000) (failIfUnchanged := true) : m Nat :=
+  match depth with
+  | 0 => k g pats
+  | depth+1 => do
+    if failIfUnchanged then
+      withExt1 g pats fun g pats => withExtN g pats k depth (failIfUnchanged := false)
+    else try
+      withExt1 g pats fun g pats => withExtN g pats k depth (failIfUnchanged := false)
+    catch _ => k g pats
+
+/--
+Apply extensionality theorems as much as possible, using `pats` to introduce the variables
+in extensionality theorems like `funext`. Returns a list of subgoals.
+
+This is built on top of `withExtN`, running in `TermElabM` to build the list of new subgoals.
+(And, for each goal, the patterns consumed.)
+-/
+def extCore (g : MVarId) (pats : List (TSyntax `rcasesPat))
+    (depth := 1000000) (failIfUnchanged := true) :
+    TermElabM (Nat × Array (MVarId × List (TSyntax `rcasesPat))) := do
+  StateT.run (m := TermElabM) (s := #[])
+    (withExtN g pats (fun g qs => modify (·.push (g, qs)) *> pure 0) depth failIfUnchanged)
+
+@[builtin_tactic ext] def evalExt : Tactic := fun stx => do
+  match stx with
+  | `(tactic| ext $pats* $[: $n]?) => do
+    let pats := RCases.expandRIntroPats pats
+    let depth := n.map (·.getNat) |>.getD 1000000
+    let (used, gs) ← extCore (← getMainGoal) pats.toList depth
+    if RCases.linter.unusedRCasesPattern.get (← getOptions) then
+      if used < pats.size then
+        Linter.logLint RCases.linter.unusedRCasesPattern (mkNullNode pats[used:].toArray)
+          m!"`ext` did not consume the patterns: {pats[used:]}"
+    replaceMainGoal <| gs.map (·.1) |>.toList
+  | _ => throwUnsupportedSyntax
+
+end Lean.Elab.Tactic.Ext

src/Lean/Elab/Term.lean

@@ -865,6 +865,12 @@ def tryPostponeIfHasMVars (expectedType? : Option Expr) (msg : String) : TermEla
     throwError "{msg}, expected type contains metavariables{indentD expectedType?}"
   return expectedType
 
+def withExpectedType (expectedType? : Option Expr) (x : Expr → TermElabM Expr) : TermElabM Expr := do
+  tryPostponeIfNoneOrMVar expectedType?
+  let some expectedType ← pure expectedType?
+    | throwError "expected type must be known"
+  x expectedType
+
 /--
   Save relevant context for term elaboration postponement.
 -/

src/Lean/Expr.lean

@@ -1916,7 +1916,14 @@ def mkNot (p : Expr) : Expr := mkApp (mkConst ``Not) p
 def mkOr (p q : Expr) : Expr := mkApp2 (mkConst ``Or) p q
 /-- Return `p ∧ q` -/
 def mkAnd (p q : Expr) : Expr := mkApp2 (mkConst ``And) p q
+/-- Make an n-ary `And` application. `mkAndN []` returns `True`. -/
+def mkAndN : List Expr → Expr
+  | [] => mkConst ``True
+  | [p] => p
+  | p :: ps => mkAnd p (mkAndN ps)
 /-- Return `Classical.em p` -/
 def mkEM (p : Expr) : Expr := mkApp (mkConst ``Classical.em) p
+/-- Return `p ↔ q` -/
+def mkIff (p q : Expr) : Expr := mkApp2 (mkConst ``Iff) p q
 
 end Lean

src/Lean/Parser/Syntax.lean

@@ -104,6 +104,16 @@ def elabTail := leading_parser atomic (" : " >> ident >> optional (" <= " >> ide
   optional docComment >> optional Term.«attributes» >> Term.attrKind >>
   "elab" >> optPrecedence >> optNamedName >> optNamedPrio >> many1 (ppSpace >> elabArg) >> elabTail
 
+/--
+Declares a binder predicate.  For example:
+```
+binder_predicate x " > " y:term => `($x > $y)
+```
+-/
+@[builtin_command_parser] def binderPredicate := leading_parser
+   optional docComment >>  optional Term.attributes >> optional Term.attrKind >>
+   "binder_predicate" >> optNamedName >> optNamedPrio >> ppSpace >> ident >> many (ppSpace >> macroArg) >> " => " >> termParser
+
 end Command
 
 end Parser

src/Lean/Parser/Term.lean

@@ -569,6 +569,12 @@ def haveDecl     := leading_parser (withAnonymousAntiquot := false)
   haveIdDecl <|> (ppSpace >> letPatDecl) <|> haveEqnsDecl
 @[builtin_term_parser] def «have» := leading_parser:leadPrec
   withPosition ("have" >> haveDecl) >> optSemicolon termParser
+/-- `haveI` behaves like `have`, but inlines the value instead of producing a `let_fun` term. -/
+@[builtin_term_parser] def «haveI» := leading_parser
+  withPosition ("haveI " >> haveDecl) >> optSemicolon termParser
+/-- `letI` behaves like `let`, but inlines the value instead of producing a `let_fun` term. -/
+@[builtin_term_parser] def «letI» := leading_parser
+  withPosition ("letI " >> haveDecl) >> optSemicolon termParser
 
 def «scoped» := leading_parser "scoped "
 def «local»  := leading_parser "local "

src/Lean/PrettyPrinter/Delaborator/Builtins.lean

@@ -793,23 +793,50 @@ def delabProj : Delab := do
   let idx := Syntax.mkLit fieldIdxKind (toString (idx + 1));
   `($(e).$idx:fieldIdx)
 
-/-- Delaborate a call to a projection function such as `Prod.fst`. -/
+/--
+Delaborates an application of a projection function, for example `Prod.fst p` as `p.fst`.
+Collapses intermediate parent projections, so for example rather than `o.toB.toA.x` it produces `o.x`.
+
+Does not delaborate projection functions from classes, since the instance parameter is implicit;
+we would rather see `default` than `instInhabitedNat.default`.
+-/
 @[builtin_delab app]
-def delabProjectionApp : Delab := whenPPOption getPPStructureProjections $ do
-  let Expr.app fn _ ← getExpr | failure
-  let .const c@(.str _ f) _ ← pure fn.getAppFn | failure
-  let env ← getEnv
-  let some info ← pure $ env.getProjectionFnInfo? c | failure
-  -- can't use with classes since the instance parameter is implicit
-  guard $ !info.fromClass
-  -- If pp.explicit is true, and the structure has parameters, we should not
-  -- use field notation because we will not be able to see the parameters.
-  let expl ← getPPOption getPPExplicit
-  guard $ !expl || info.numParams == 0
-  -- projection function should be fully applied (#struct params + 1 instance parameter)
-  withOverApp (info.numParams + 1) do
-    let appStx ← withAppArg delab
-    `($(appStx).$(mkIdent f):ident)
+partial def delabProjectionApp : Delab := whenPPOption getPPStructureProjections do
+  let (field, arity, _) ← projInfo
+  withOverApp arity do
+    let stx ← withAppArg <| withoutParentProjections delab
+    `($(stx).$(mkIdent field):ident)
+where
+  /--
+  If this is a projection that could delaborate using dot notation,
+  returns the field name, the arity of the projector, and whether this is a parent projection.
+  Otherwise it fails.
+  -/
+  projInfo : DelabM (Name × Nat × Bool) := do
+    let .app fn _ ← getExpr | failure
+    let .const c@(.str _ field) _ := fn.getAppFn | failure
+    let env ← getEnv
+    let some info := env.getProjectionFnInfo? c | failure
+    -- Don't delaborate for classes since the instance parameter is implicit.
+    guard <| !info.fromClass
+    -- If pp.explicit is true, and the structure has parameters, we should not
+    -- use field notation because we will not be able to see the parameters.
+    guard <| !(← getPPOption getPPExplicit) || info.numParams == 0
+    let arity := info.numParams + 1
+    let some (.ctorInfo cVal) := env.find? info.ctorName | failure
+    let isParentProj := (isSubobjectField? env cVal.induct field).isSome
+    return (field, arity, isParentProj)
+  /--
+  Consumes projections to parent structures.
+  For example, if the current expression is `o.toB.toA`, runs `d` with `o` as the current expression.
+  -/
+  withoutParentProjections {α} (d : DelabM α) : DelabM α :=
+    (do
+      let (_, arity, isParentProj) ← projInfo
+      guard isParentProj
+      guard <| (← getExpr).getAppNumArgs == arity
+      withAppArg <| withoutParentProjections d)
+    <|> d
 
 /--
 This delaborator tries to elide functions which are known coercions.