chore: upstream orphaned tests from Std

tests/lean/run/decidability_timeout.lean

@@ -0,0 +1,6 @@
+
+-- Prior to leanprover/lean4#2552 there was a performance trap
+-- depending on the implementation details in `decidableBallLT`.
+-- We keep this example (which would have gone over maxHeartbeats)
+-- as a regression test for the instance.
+example : ∀ m, m < 25 → ∀ n, n < 25 → ∀ c, c < 25 → m ^ 2 + n ^ 2 + c ^ 2 ≠ 7 := by decide

tests/lean/run/ext.lean

@@ -0,0 +1,106 @@
+
+set_option linter.missingDocs false
+axiom mySorry {α : Sort _} : α
+
+structure A (n : Nat) where
+  a : Nat
+
+example (a b : A n) : a = b ∨ True := by
+  fail_if_success
+    apply Or.inl; ext
+  exact Or.inr trivial
+
+structure B (n) extends A n where
+  b : Nat
+  h : b > 0
+  i : Fin b
+
+@[ext] structure C (n) extends B n where
+  c : Nat
+
+example (a b : C n) : a = b := by
+  ext
+  guard_target = a.a = b.a; exact mySorry
+  guard_target = a.b = b.b; exact mySorry
+  guard_target = HEq a.i b.i; exact mySorry
+  guard_target = a.c = b.c; exact mySorry
+
+@[ext (flat := false)] structure C' (n) extends B n where
+  c : Nat
+
+example (a b : C' n) : a = b := by
+  ext
+  guard_target = a.toB = b.toB; exact mySorry
+  guard_target = a.c = b.c; exact mySorry
+
+example (f g : Nat × Nat → Nat) : f = g := by
+  ext ⟨x, y⟩
+  guard_target = f (x, y) = g (x, y); exact mySorry
+
+-- Check that we generate a warning if there are too many patterns.
+/-- warning: `ext` did not consume the patterns: [j] [linter.unusedRCasesPattern] -/
+#guard_msgs in
+example (f g : Nat → Nat) (h : f = g) : f = g := by
+  ext i j
+  exact h ▸ rfl
+
+-- allow more specific ext theorems
+@[ext high] theorem Fin.zero_ext (a b : Fin 0) : True → a = b := by cases a.isLt
+example (a b : Fin 0) : a = b := by ext; exact True.intro
+
+def Set (α : Type u) := α → Prop
+@[ext] structure LocalEquiv (α : Type u) (β : Type v) where
+  source : Set α
+@[ext] structure Pretrivialization {F : Type u} (proj : Z → β) extends LocalEquiv Z (β × F) where
+  baseSet : Set β
+  source_eq : source = baseSet ∘ proj
+
+structure MyUnit
+
+@[ext high] theorem MyUnit.ext1 (x y : MyUnit) (_h : 0 = 1) : x = y := rfl
+@[ext high] theorem MyUnit.ext2 (x y : MyUnit) (_h : 1 = 1) : x = y := rfl
+@[ext] theorem MyUnit.ext3 (x y : MyUnit) (_h : 2 = 1) : x = y := rfl
+
+example (x y : MyUnit) : x = y := by ext; rfl
+
+-- Check that we don't generate a warning when `x` only uses a pattern in one branch:
+example (f : ℕ × (ℕ → ℕ)) : f = f := by
+  ext x
+  · rfl
+  · guard_target = (f.2) x = (f.2) x
+    rfl
+
+example (f : Empty → Empty) : f = f := by
+  ext ⟨⟩
+
+@[ext] theorem ext_intros {n m : Nat} (w : ∀ n m : Nat, n = m) : n = m := by apply w
+
+#guard_msgs (drop warning) in
+example : 3 = 7 := by
+  ext : 1
+  rename_i n m
+  guard_target = n = m
+  admit
+
+#guard_msgs (drop warning) in
+example : 3 = 7 := by
+  ext n m : 1
+  guard_target = n = m
+  admit
+
+section erasing_ext_attribute
+
+def f (p : Int × Int) : Int × Int := (p.2, p.1)
+
+example : f ∘ f = id := by
+  ext ⟨a, b⟩
+  · simp [f]
+  · simp [f]
+
+attribute [-ext] Prod.ext
+
+example : f ∘ f = id := by
+  ext ⟨a, b⟩
+  simp [f]
+
+end erasing_ext_attribute

tests/lean/run/guard_expr.lean

@@ -0,0 +1,58 @@
+
+example (n : Nat) : Nat := by
+  guard_hyp n :ₛ Nat
+  let m : Nat := 1
+  guard_expr 1 =ₛ (by exact 1)
+  fail_if_success guard_expr 1 = (by exact 2)
+  guard_hyp m := 1
+  guard_hyp m : (fun x => x) Nat :=~ id 1
+  guard_target = Nat
+  have : 1 = 1 := by conv =>
+    guard_hyp m := 1
+    guard_expr ‹Nat› = m
+    fail_if_success guard_target = 1
+    lhs
+    guard_target = 1
+  exact 0
+
+-- Now with a generic type to test that default instances work correctly
+example [∀ n, OfNat α n] (n : α) : α := by
+  guard_hyp n
+  fail_if_success guard_hyp m
+  guard_hyp n :ₛ α
+  let q : α := 1
+  guard_expr (1 : α) =ₛ 1
+  fail_if_success guard_expr 1 =ₛ (2 : α)
+  fail_if_success guard_expr 1 =ₛ (by exact (2 : α))
+  guard_hyp q := 1
+  guard_hyp q : α := 1
+  guard_hyp q : (fun x => x) α :=~ id 1
+  guard_target = α
+  have : (1 : α) = 1 := by conv =>
+    guard_hyp q := 1
+    guard_expr ‹α› = q
+    fail_if_success guard_target = 1
+    lhs
+    guard_target = 1
+  exact 0
+
+#guard_expr 1 = 1
+#guard_expr 1 =ₛ 1
+#guard_expr 2 = 1 + 1
+
+section
+variable {α : Type} [∀ n, OfNat α n]
+#guard_expr (1 : α) = 1
+end
+
+#guard true
+#guard 2 == 1 + 1
+#guard 2 = 1 + 1
+
+instance (p : Bool → Prop) [DecidablePred p] : Decidable (∀ b, p b) :=
+  if h : p false ∧ p true then
+    isTrue (by { intro b; cases h; cases b <;> assumption })
+  else
+    isFalse (by { intro h'; simp [h'] at h })
+
+#guard ∀ (b : Bool), b = !!b

tests/lean/run/int_complement_shiftRight.lean

@@ -0,0 +1,15 @@
+
+-- complement
+#guard ~~~(-1:Int) = 0
+#guard ~~~(0:Int) = -1
+#guard ~~~(1:Int) = -2
+#guard ~~~(-2:Int) = 1
+
+-- shiftRight
+#guard (2:Int) >>> 1 = 1
+#guard (0:Int) >>> 1 = 0
+#guard ~~~(1:Int) >>> 1 = ~~~0
+#guard ~~~(0:Int) >>> 1 = ~~~0
+#guard ~~~(2:Int) >>> 1 = ~~~1
+#guard ~~~(4:Int) >>> 1 = ~~~2
+#guard ~~~(4:Int) >>> 2 = ~~~1

tests/lean/run/json.lean

@@ -0,0 +1,22 @@
+import Lean.Data.Json.Elab
+
+/-- info: {"lookACalc": 131,
+ "lemonCount": 100000000000000000000000000000000,
+ "isCool": true,
+ "isBug": null,
+ "hello": "world",
+ "cheese": ["edam", "cheddar", {"rank": 100.2, "kind": "spicy"}]}-/
+#guard_msgs in
+#eval json% {
+  hello : "world",
+  cheese : ["edam", "cheddar", {kind : "spicy", rank : 100.2}],
+  lemonCount : 100e30,
+  isCool : true,
+  isBug : null,
+  lookACalc: $(23 + 54 * 2)
+}
+
+-- See https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/json.20elaborator
+example : Lean.Json := Id.run do
+  let _x := true
+  return json% {"x" : 1}

tests/lean/run/left_right.lean

@@ -0,0 +1,66 @@
+
+/-- Construct a natural number using `left`. -/
+def zero : Nat := by
+  left
+
+example : zero = 0 := rfl
+
+/-- Construct a natural number using `right`. -/
+def two : Nat := by
+  right
+  exact 1
+
+example : two = 2 := rfl
+
+set_option linter.missingDocs false
+
+/--
+error: tactic 'left' failed,
+left tactic works for inductive types with exactly 2 constructors
+⊢ Unit
+-/
+#guard_msgs in
+example : Unit := by
+  left
+
+inductive F
+| a | b | c
+
+/--
+error: tactic 'left' failed,
+left tactic works for inductive types with exactly 2 constructors
+⊢ F
+-/
+#guard_msgs in
+example : F := by
+  left
+
+def G := Nat
+
+/-- Look through definitions. -/
+example : G := by
+  left
+
+/--
+error: tactic 'left' failed, target is not an inductive datatype
+⊢ Type
+-/
+#guard_msgs in
+example : Type := by
+  left
+
+example : Sum Nat (List Nat) := by
+  left
+  exact zero
+
+example : Sum Nat (List Nat) := by
+  right
+  exact [0]
+
+example : (1 = 1) ∨ (2 = 3) := by
+  left
+  rfl
+
+example : (1 = 2) ∨ (3 = 3) := by
+  right
+  rfl

tests/lean/run/omega_examples.lean

@@ -0,0 +1,57 @@
+
+-- Turn on `trace.omega` to get detailed information about the processing of hypotheses,
+-- and the justification of the contradiction found.
+-- set_option trace.omega true
+
+-- Inequalities
+example {x y : Nat} (_ : x + y > 10) (_ : x < 5) (_ : y < 5) : False := by omega
+
+-- Tightening inequalities over `Int` or `Nat`
+example {x y : Nat} (_ : x + y > 10) (_ : 2 * x < 11) (_ : y < 5) : False := by omega
+
+-- GCDs not dividing constant terms
+example {x y : Nat} (_ : 2 * x + 4 * y = 5) : False := by omega
+
+-- Eliminating variables even when no coefficient is ±1
+example {x y : Nat} (_ : 6 * x + 7 * y = 5) : False := by omega
+
+-- Case bashing on `Nat.sub`
+example {x y z : Nat} (_ : x - y - z = 0) (_ : x > y + z) : False := by omega
+
+-- Division with constant denominators
+example {x y : Nat} (_ : x / 2 - y / 3 < 1) (_ : 3 * x ≥ 2 * y + 4) : False := by omega
+
+-- Annoying casts
+example {x : Nat} : 1 < (1 + ((x + 1 : Nat) : Int) + 2) / 2 := by omega
+
+-- Divisibility
+example {x : Nat} (_ : 10000 ∣ x) (_ : ¬ 100 ∣ x) : False := by omega
+
+-- Mod
+example (x : Nat) : x % 1024 - x % 2048 = 0 := by omega
+
+-- Systems of equations
+example (a b c d e : Int)
+    (ha : 2 * a + b + c + d + e = 4)
+    (hb : a + 2 * b + c + d + e = 5)
+    (hc : a + b + 2 * c + d + e = 6)
+    (hd : a + b + c + 2 * d + e = 7)
+    (he : a + b + c + d + 2 * e = 8) : e = 3 := by omega
+
+-- Case bashing on disjunctions
+example (a b c d e : Int)
+    (ha : 2 * a + b + c + d + e = 4)
+    (hb : a + 2 * b + c + d + e = 5)
+    (hc : a + b + 2 * c + d + e = 6)
+    (hd : a + b + c + 2 * d + e = 7)
+    (he : a + b + c + d + 2 * e = 8 ∨ e = 3) : e = 3 := by omega
+
+-- Case bashing conjunctions in the goal
+example (ε : Int) (_ : ε > 0) : (ε - 2 ≤ ε / 3 + ε / 2 + ε / 2) ∧ (ε / 3 + ε / 4 + ε / 5 ≤ ε) := by
+  omega
+
+-- Fast results with duplicated hypotheses
+example {x : Int} (h₁ : 0 ≤ 2 * x + 1) (h₂ : 2 * x + 1 ≤ 0) : False := by
+  iterate 64 have := h₁
+  iterate 64 have := h₂
+  omega

tests/lean/run/rcases.lean

@@ -0,0 +1,211 @@
+import Lean.Elab.Tactic.Basic
+
+set_option linter.missingDocs false
+
+example (x : α × β × γ) : True := by
+  rcases x with ⟨a, b, c⟩
+  guard_hyp a : α
+  guard_hyp b : β
+  guard_hyp c : γ
+  trivial
+
+example (x : α × β × γ) : True := by
+  rcases x with ⟨(a : α) : id α, -, c : id γ⟩
+  guard_hyp a : α
+  fail_if_success have : β := by assumption
+  guard_hyp c : id γ
+  trivial
+
+example (x : (α × β) × γ) : True := by
+  fail_if_success rcases x with ⟨_a, b, c⟩
+  fail_if_success rcases x with ⟨⟨a:β, b⟩, c⟩
+  rcases x with ⟨⟨a:α, b⟩, c⟩
+  guard_hyp a : α
+  guard_hyp b : β
+  guard_hyp c : γ
+  trivial
+
+example : @Inhabited.{1} α × Option β ⊕ γ → True := by
+  rintro (⟨⟨a⟩, _ | b⟩ | c)
+  · guard_hyp a : α; trivial
+  · guard_hyp a : α; guard_hyp b : β; trivial
+  · guard_hyp c : γ; trivial
+
+example : cond false Nat Int → cond true Int Nat → Nat ⊕ Unit → True := by
+  rintro (x y : Int) (z | u)
+  · guard_hyp x : Int; guard_hyp y : Int; guard_hyp z : Nat; trivial
+  · guard_hyp x : Int; guard_hyp y : Int; guard_hyp u : Unit; trivial
+
+example (x y : Nat) (h : x = y) : True := by
+  rcases x with _|⟨⟩|z
+  · guard_hyp h : Nat.zero = y; trivial
+  · guard_hyp h : Nat.succ Nat.zero = y; trivial
+  · guard_hyp z : Nat
+    guard_hyp h : Nat.succ (Nat.succ z) = y; trivial
+
+example (h : x = 3) (h₂ : x < 4) : x < 4 := by
+  rcases h with ⟨⟩
+  guard_hyp h₂ : 3 < 4; guard_target = 3 < 4; exact h₂
+
+example (h : x = 3) (h₂ : x < 4) : x < 4 := by
+  rcases h with rfl
+  guard_hyp h₂ : 3 < 4; guard_target = 3 < 4; exact h₂
+
+example (h : 3 = x) (h₂ : x < 4) : x < 4 := by
+  rcases h with ⟨⟩
+  guard_hyp h₂ : 3 < 4; guard_target = 3 < 4; exact h₂
+
+example (h : 3 = x) (h₂ : x < 4) : x < 4 := by
+  rcases h with rfl
+  guard_hyp h₂ : 3 < 4; guard_target = 3 < 4; exact h₂
+
+example (s : α ⊕ Empty) : True := by
+  rcases s with s|⟨⟨⟩⟩
+  guard_hyp s : α; trivial
+
+example : True := by
+  obtain ⟨n : Nat, _h : n = n, -⟩ : ∃ n : Nat, n = n ∧ True
+  · exact ⟨0, rfl, trivial⟩
+  trivial
+
+example : True := by
+  obtain (h : True) | ⟨⟨⟩⟩ : True ∨ False
+  · exact Or.inl trivial
+  guard_hyp h : True; trivial
+
+example : True := by
+  obtain h | ⟨⟨⟩⟩ : True ∨ False := Or.inl trivial
+  guard_hyp h : True; trivial
+
+example : True := by
+  obtain ⟨h, h2⟩ := And.intro trivial trivial
+  guard_hyp h : True; guard_hyp h2 : True; trivial
+
+example : True := by
+  fail_if_success obtain ⟨h, h2⟩
+  trivial
+
+example (x y : α × β) : True := by
+  rcases x, y with ⟨⟨a, b⟩, c, d⟩
+  guard_hyp a : α; guard_hyp b : β
+  guard_hyp c : α; guard_hyp d : β
+  trivial
+
+example (x y : α ⊕ β) : True := by
+  rcases x, y with ⟨a|b, c|d⟩
+  · guard_hyp a : α; guard_hyp c : α; trivial
+  · guard_hyp a : α; guard_hyp d : β; trivial
+  · guard_hyp b : β; guard_hyp c : α; trivial
+  · guard_hyp b : β; guard_hyp d : β; trivial
+
+example (i j : Nat) : (Σ' x, i ≤ x ∧ x ≤ j) → i ≤ j := by
+  intro h
+  rcases h' : h with ⟨x, h₀, h₁⟩
+  guard_hyp h' : h = ⟨x, h₀, h₁⟩
+  apply Nat.le_trans h₀ h₁
+
+example (x : Quot fun _ _ : α => True) (h : x = x): x = x := by
+  rcases x with ⟨z⟩
+  guard_hyp z : α
+  guard_hyp h : Quot.mk (fun _ _ => True) z = Quot.mk (fun _ _ => True) z
+  guard_target = Quot.mk (fun _ _ => True) z = Quot.mk (fun _ _ => True) z
+  exact h
+
+example (n : Nat) : True := by
+  obtain _one_lt_n | _n_le_one : 1 < n + 1 ∨ n + 1 ≤ 1 := Nat.lt_or_ge 1 (n + 1)
+  {trivial}; trivial
+
+example (n : Nat) : True := by
+  obtain _one_lt_n | (_n_le_one : n + 1 ≤ 1) := Nat.lt_or_ge 1 (n + 1)
+  {trivial}; trivial
+
+open Lean Elab Tactic in
+/-- Asserts that the goal has `n` hypotheses. Used for testing. -/
+elab "check_num_hyps " n:num : tactic => liftMetaMAtMain fun _ => do
+  -- +1 because the _example recursion decl is in the list
+  guard $ (← getLCtx).foldl (fun i _ => i+1) 0 = n.1.toNat + 1
+
+example (h : ∃ x : Nat, x = x ∧ 1 = 1) : True := by
+  rcases h with ⟨-, _⟩
+  check_num_hyps 0
+  trivial
+
+example (h : ∃ x : Nat, x = x ∧ 1 = 1) : True := by
+  rcases h with ⟨-, _, h⟩
+  check_num_hyps 1
+  guard_hyp h : 1 = 1
+  trivial
+
+example (h : True ∨ True ∨ True) : True := by
+  rcases h with - | - | -
+  iterate 3 · check_num_hyps 0; trivial
+
+example (h : True ∨ True ∨ True) : True := by
+  rcases h with -|-|-
+  iterate 3 · check_num_hyps 0; trivial
+
+example : Bool → False → True
+| false => by rintro ⟨⟩
+| true => by rintro ⟨⟩
+
+example : (b : Bool) → cond b False False → True := by
+  rintro ⟨⟩ ⟨⟩
+
+structure Baz {α : Type _} (f : α → α) : Prop where
+  [inst : Nonempty α]
+  h : f ∘ f = id
+
+example {α} (f : α → α) (h : Baz f) : True := by rcases h with ⟨_⟩; trivial
+
+example {α} (f : α → α) (h : Baz f) : True := by rcases h with @⟨_, _⟩; trivial
+
+inductive Test : Nat → Prop
+  | a (n) : Test (2 + n)
+  | b {n} : n > 5 → Test (n * n)
+
+example {n} (h : Test n) : n = n := by
+  have : True := by
+    rcases h with (a | b)
+    · guard_hyp a : Nat
+      trivial
+    · guard_hyp b : ‹Nat› > 5
+      trivial
+  · rcases h with (a | @⟨n, b⟩)
+    · guard_hyp a : Nat
+      trivial
+    · guard_hyp b : n > 5
+      trivial
+
+example (h : a ≤ 2 ∨ 2 < a) : True := by
+  obtain ha1 | ha2 : a ≤ 2 ∨ 3 ≤ a := h
+  · guard_hyp ha1 : a ≤ 2; trivial
+  · guard_hyp ha2 : 3 ≤ a; trivial
+
+example (h : a ≤ 2 ∨ 2 < a) : True := by
+  obtain ha1 | ha2 : a ≤ 2 ∨ 3 ≤ a := id h
+  · guard_hyp ha1 : a ≤ 2; trivial
+  · guard_hyp ha2 : 3 ≤ a; trivial
+
+example (a : Nat) : True := by
+  rcases h : a with _ | n
+  · guard_hyp h : a = 0; trivial
+  · guard_hyp h : a = n + 1; trivial
+
+inductive BaseType : Type where
+  | one
+
+inductive BaseTypeHom : BaseType → BaseType → Type where
+  | loop : BaseTypeHom one one
+  | id (X : BaseType) : BaseTypeHom X X
+
+example : BaseTypeHom one one → Unit := by rintro ⟨_⟩ <;> constructor
+
+axiom test_sorry {α} : α
+example (b c : Nat) : True := by
+  obtain rfl : b = c ^ 2 := test_sorry
+  trivial
+
+example (b c : Nat) : True := by
+  obtain h : b = c ^ 2 := test_sorry
+  subst h
+  trivial

tests/lean/run/repeat.lean

@@ -0,0 +1,13 @@
+import Lean.Elab.Tactic.Basic
+import Lean.Meta.Tactic.Util
+
+open Lean Elab Tactic Meta
+
+elab "foo" : tactic => liftMetaTactic fun g => do
+  g.assign (← mkFreshExprMVar (← g.getType))
+  throwError ""
+
+#guard_msgs in
+example : True := by
+  repeat' foo
+  trivial

tests/lean/run/solve_by_elim.lean

@@ -0,0 +1,152 @@
+/-
+Copyright (c) 2021 Scott Morrison. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Scott Morrison
+-/
+
+import Lean.Meta.Tactic.Constructor
+import Lean.Elab.SyntheticMVars
+import Lean.Elab.Tactic.SolveByElim -- FIXME we need to make SolveByElimConfig builtin
+
+set_option autoImplicit true
+
+example (h : Nat) : Nat := by solve_by_elim
+example {α β : Type} (f : α → β) (a : α) : β := by solve_by_elim
+example {α β : Type} (f : α → α → β) (a : α) : β := by solve_by_elim
+example {α β γ : Type} (f : α → β) (g : β → γ) (a : α) : γ := by solve_by_elim
+example {α β γ : Type} (_f : α → β) (g : β → γ) (b : β) : γ := by solve_by_elim
+example {α : Nat → Type} (f : (n : Nat) → α n → α (n+1)) (a : α 0) : α 4 := by solve_by_elim
+
+example (h : Nat) : Nat := by solve_by_elim []
+example {α β : Type} (f : α → β) (a : α) : β := by solve_by_elim []
+example {α β : Type} (f : α → α → β) (a : α) : β := by solve_by_elim []
+example {α β γ : Type} (f : α → β) (g : β → γ) (a : α) : γ := by solve_by_elim []
+example {α β γ : Type} (_f : α → β) (g : β → γ) (b : β) : γ := by solve_by_elim []
+example {α : Nat → Type} (f : (n : Nat) → α n → α (n+1)) (a : α 0) : α 4 := by solve_by_elim []
+
+example {α β : Type} (f : α → β) (a : α) : β := by
+  fail_if_success solve_by_elim [-f]
+  fail_if_success solve_by_elim [-a]
+  fail_if_success solve_by_elim only [f]
+  solve_by_elim
+
+example {α β γ : Type} (f : α → β) (g : β → γ) (b : β) : γ := by
+  fail_if_success solve_by_elim [-g]
+  solve_by_elim [-f]
+
+example (h : Nat) : Nat := by solve_by_elim only [h]
+example {α β : Type} (f : α → β) (a : α) : β := by solve_by_elim only [f, a]
+example {α β : Type} (f : α → α → β) (a : α) : β := by solve_by_elim only [f, a]
+example {α β γ : Type} (f : α → β) (g : β → γ) (a : α) : γ := by solve_by_elim only [f, g, a]
+example {α β γ : Type} (_f : α → β) (g : β → γ) (b : β) : γ := by solve_by_elim only [g, b]
+example {α : Nat → Type} (f : (n : Nat) → α n → α (n+1)) (a : α 0) : α 4 := by
+  solve_by_elim only [f, a]
+
+set_option linter.unusedVariables false in
+example (h₁ h₂ : False) : True := by
+  -- 'It doesn't make sense to remove local hypotheses when using `only` without `*`.'
+  fail_if_success solve_by_elim only [-h₁]
+  -- 'It does make sense to use `*` without `only`.'
+  fail_if_success solve_by_elim [*, -h₁]
+  solve_by_elim only [*, -h₁]
+
+-- Verify that already assigned metavariables are skipped.
+example (P₁ P₂ : α → Prop) (f : ∀ (a : α), P₁ a → P₂ a → β)
+    (a : α) (ha₁ : P₁ a) (ha₂ : P₂ a) : β := by
+  solve_by_elim
+
+example {X : Type} (x : X) : x = x := by
+  fail_if_success solve_by_elim (config := {constructor := false}) only -- needs the `rfl` lemma
+  solve_by_elim
+
+-- Needs to apply `rfl` twice, with different implicit arguments each time.
+-- A naive implementation of solve_by_elim would get stuck.
+example {X : Type} (x y : X) (p : Prop) (h : x = x → y = y → p) : p := by solve_by_elim
+
+example : True := by
+  fail_if_success solve_by_elim (config := {constructor := false}) only -- needs the `trivial` lemma
+  solve_by_elim
+
+-- Requires backtracking.
+example (P₁ P₂ : α → Prop) (f : ∀ (a: α), P₁ a → P₂ a → β)
+    (a : α) (_ha₁ : P₁ a)
+    (a' : α) (ha'₁ : P₁ a') (ha'₂ : P₂ a') : β := by
+  fail_if_success solve_by_elim (config := .noBackTracking)
+  solve_by_elim
+
+attribute [symm] Eq.symm in
+example {α : Type} {a b : α → Prop} (h₀ : b = a) (y : α) : a y = b y := by
+  fail_if_success solve_by_elim (config := {symm := false})
+  solve_by_elim
+
+example (P : True → False) : 3 = 7 := by
+  fail_if_success solve_by_elim (config := {exfalso := false})
+  solve_by_elim
+
+-- Verifying that `solve_by_elim` acts only on the main goal.
+example (n : Nat) : Nat × Nat := by
+  constructor
+  solve_by_elim
+  solve_by_elim
+
+-- Verifying that `solve_by_elim*` acts on all remaining goals.
+example (n : Nat) : Nat × Nat := by
+  constructor
+  solve_by_elim*
+
+open Lean Elab Tactic in
+/--
+`fconstructor` is like `constructor`
+(it calls `apply` using the first matching constructor of an inductive datatype)
+except that it does not reorder goals.
+-/
+elab "fconstructor" : tactic => withMainContext do
+  let mvarIds' ← (← getMainGoal).constructor {newGoals := .all}
+  Term.synthesizeSyntheticMVarsNoPostponing
+  replaceMainGoal mvarIds'
+
+-- Verifying that `solve_by_elim*` backtracks when given multiple goals.
+example (n m : Nat) (f : Nat → Nat → Prop) (h : f n m) : ∃ p : Nat × Nat, f p.1 p.2 := by
+  fconstructor
+  fconstructor
+  solve_by_elim*
+
+-- test that metavariables created for implicit arguments don't get stuck
+example (P : Nat → Type) (f : {n : Nat} → P n) : P 2 × P 3 := by
+  fconstructor
+  solve_by_elim* only [f]
+
+example : 6 = 6 ∧ [7] = [7] := by
+  fconstructor
+  solve_by_elim* only [@rfl _]
+
+-- Test that `Config.intros` causes `solve_by_elim` to call `intro` on intermediate goals.
+example (P : Prop) : P → P := by
+  fail_if_success solve_by_elim (config := {intros := false})
+  solve_by_elim
+
+-- This worked in mathlib3 without the `@`, but now goes into a loop.
+-- If someone wants to diagnose this, please do!
+example (P Q : Prop) : P ∧ Q → P ∧ Q := by
+  solve_by_elim [And.imp, @id]
+
+section apply_assumption
+
+example {a b : Type} (h₀ : a → b) (h₁ : a) : b := by
+  apply_assumption
+  apply_assumption
+
+example {α : Type} {p : α → Prop} (h₀ : ∀ x, p x) (y : α) : p y := by
+  apply_assumption
+
+-- Check that `apply_assumption` uses `exfalso`.
+example {P Q : Prop} (p : P) (q : Q) (h : P → ¬ Q) : Nat := by
+  fail_if_success apply_assumption (config := {exfalso := false})
+  apply_assumption <;> assumption
+
+end apply_assumption
+
+example (x : (α × (β × γ))) : (α × β) × γ := by
+  rcases x with ⟨a, b, c⟩
+  fail_if_success solve_by_elim (config := {constructor := false})
+  solve_by_elim

tests/lean/run/symm.lean

@@ -0,0 +1,27 @@
+import Init.Tactics
+
+set_option autoImplicit true
+set_option linter.missingDocs false
+
+-- testing that the attribute is recognized
+@[symm] def eq_symm {α : Type} (a b : α) : a = b → b = a := Eq.symm
+
+example (a b : Nat) : a = b → b = a := by intros; symm; assumption
+example (a b : Nat) : a = b → True → b = a := by intro h _; symm at h; assumption
+
+def sameParity : Nat → Nat → Prop
+  | n, m => n % 2 = m % 2
+
+@[symm] def sameParity_symm (n m : Nat) : sameParity n m → sameParity m n := Eq.symm
+
+example (a b : Nat) : sameParity a b → sameParity b a := by intros; symm; assumption
+
+def MyEq (n m : Nat) := ∃ k, n + k = m ∧ m + k = n
+
+@[symm] theorem MyEq.symm {n m : Nat} (h : MyEq n m) : MyEq m n := by
+  rcases h with ⟨k, h1, h2⟩
+  exact ⟨k, h2, h1⟩
+
+example {n m : Nat} (h : MyEq n m) : MyEq m n := by
+  symm
+  assumption