Merge branch 'congr' into convert

src/Init.lean

@@ -33,3 +33,4 @@ import Init.SizeOfLemmas
 import Init.BinderPredicates
 import Init.Ext
 import Init.Omega
+import Init.Congr!

src/Init/Congr!.lean

@@ -0,0 +1,183 @@
+/-
+Copyright (c) 2023 Kyle Miller. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kyle Miller
+-/
+prelude
+import Init.RCases
+
+namespace Lean.Parser.Tactic
+
+open Lean
+
+/--
+Equates pieces of the left-hand side of a goal to corresponding pieces of the right-hand side by
+recursively applying congruence lemmas. For example, with `⊢ f as = g bs` we could get
+two goals `⊢ f = g` and `⊢ as = bs`.
+
+Syntax:
+```
+congr!
+congr! n
+congr! with x y z
+congr! n with x y z
+```
+Here, `n` is a natural number and `x`, `y`, `z` are `rintro` patterns (like `h`, `rfl`, `⟨x, y⟩`,
+`_`, `-`, `(h | h)`, etc.).
+
+The `congr!` tactic is similar to `congr` but is more insistent in trying to equate left-hand sides
+to right-hand sides of goals. Here is a list of things it can try:
+
+- If `R` in `⊢ R x y` is a reflexive relation, it will convert the goal to `⊢ x = y` if possible.
+  The list of reflexive relations is maintained using the `@[refl]` attribute.
+  As a special case, `⊢ p ↔ q` is converted to `⊢ p = q` during congruence processing and then
+  returned to `⊢ p ↔ q` form at the end.
+
+- If there is a user congruence lemma associated to the goal (for instance, a `@[congr]`-tagged
+  lemma applying to `⊢ List.map f xs = List.map g ys`), then it will use that.
+
+- It uses a congruence lemma generator at least as capable as the one used by `congr` and `simp`.
+  If there is a subexpression that can be rewritten by `simp`, then `congr!` should be able
+  to generate an equality for it.
+
+- It can do congruences of pi types using lemmas like `implies_congr` and `pi_congr`.
+
+- Before applying congruences, it will run the `intros` tactic automatically.
+  The introduced variables can be given names using a `with` clause.
+  This helps when congruence lemmas provide additional assumptions in hypotheses.
+
+- When there is an equality between functions, so long as at least one is obviously a lambda, we
+  apply `funext` or `hfunext`, which allows for congruence of lambda bodies.
+
+- It can try to close goals using a few strategies, including checking
+  definitional equality, trying to apply `Subsingleton.elim` or `proof_irrel_heq`, and using the
+  `assumption` tactic.
+
+The optional parameter is the depth of the recursive applications.
+This is useful when `congr!` is too aggressive in breaking down the goal.
+For example, given `⊢ f (g (x + y)) = f (g (y + x))`,
+`congr!` produces the goals `⊢ x = y` and `⊢ y = x`,
+while `congr! 2` produces the intended `⊢ x + y = y + x`.
+
+The `congr!` tactic also takes a configuration option, for example
+```lean
+congr! (config := {transparency := .default}) 2
+```
+This overrides the default, which is to apply congruence lemmas at reducible transparency.
+
+The `congr!` tactic is aggressive with equating two sides of everything. There is a predefined
+configuration that uses a different strategy:
+Try
+```lean
+congr! (config := .unfoldSameFun)
+```
+This only allows congruences between functions applications of definitionally equal functions,
+and it applies congruence lemmas at default transparency (rather than just reducible).
+This is somewhat like `congr`.
+
+See `Congr!.Config` for all options.
+-/
+syntax (name := congr!) "congr!" (Parser.Tactic.config)? (ppSpace num)?
+  (" with" (ppSpace colGt rintroPat)*)? : tactic
+
+/--
+The `exact e` and `refine e` tactics require a term `e` whose type is
+definitionally equal to the goal. `convert e` is similar to `refine e`,
+but the type of `e` is not required to exactly match the
+goal. Instead, new goals are created for differences between the type
+of `e` and the goal using the same strategies as the `congr!` tactic.
+For example, in the proof state
+
+```lean
+n : ℕ,
+e : Prime (2 * n + 1)
+⊢ Prime (n + n + 1)
+```
+
+the tactic `convert e using 2` will change the goal to
+
+```lean
+⊢ n + n = 2 * n
+```
+
+In this example, the new goal can be solved using `ring`.
+
+The `using 2` indicates it should iterate the congruence algorithm up to two times,
+where `convert e` would use an unrestricted number of iterations and lead to two
+impossible goals: `⊢ HAdd.hAdd = HMul.hMul` and `⊢ n = 2`.
+
+A variant configuration is `convert (config := .unfoldSameFun) e`, which only equates function
+applications for the same function (while doing so at the higher `default` transparency).
+This gives the same goal of `⊢ n + n = 2 * n` without needing `using 2`.
+
+The `convert` tactic applies congruence lemmas eagerly before reducing,
+therefore it can fail in cases where `exact` succeeds:
+```lean
+def p (n : ℕ) := True
+example (h : p 0) : p 1 := by exact h -- succeeds
+example (h : p 0) : p 1 := by convert h -- fails, with leftover goal `1 = 0`
+```
+Limiting the depth of recursion can help with this. For example, `convert h using 1` will work
+in this case.
+
+The syntax `convert ← e` will reverse the direction of the new goals
+(producing `⊢ 2 * n = n + n` in this example).
+
+Internally, `convert e` works by creating a new goal asserting that
+the goal equals the type of `e`, then simplifying it using
+`congr!`. The syntax `convert e using n` can be used to control the
+depth of matching (like `congr! n`). In the example, `convert e using 1`
+would produce a new goal `⊢ n + n + 1 = 2 * n + 1`.
+
+Refer to the `congr!` tactic to understand the congruence operations. One of its many
+features is that if `x y : t` and an instance `Subsingleton t` is in scope,
+then any goals of the form `x = y` are solved automatically.
+
+Like `congr!`, `convert` takes an optional `with` clause of `rintro` patterns,
+for example `convert e using n with x y z`.
+
+The `convert` tactic also takes a configuration option, for example
+```lean
+convert (config := {transparency := .default}) h
+```
+These are passed to `congr!`. See `Congr!.Config` for options.
+-/
+syntax (name := convert) "convert" (Parser.Tactic.config)? " ←"? ppSpace term (" using " num)?
+  (" with" (ppSpace colGt rintroPat)*)? : tactic
+
+
+/--
+`convert_to g using n` attempts to change the current goal to `g`, but unlike `change`,
+it will generate equality proof obligations using `congr! n` to resolve discrepancies.
+`convert_to g` defaults to using `congr! 1`.
+`convert_to` is similar to `convert`, but `convert_to` takes a type (the desired subgoal) while
+`convert` takes a proof term.
+That is, `convert_to g using n` is equivalent to `convert (?_ : g) using n`.
+
+The syntax for `convert_to` is the same as for `convert`, and it has variations such as
+`convert_to ← g` and `convert_to (config := {transparency := .default}) g`.
+-/
+syntax (name := convertTo) "convert_to" (Parser.Tactic.config)? " ←"? ppSpace term (" using " num)?
+  (" with" (ppSpace colGt rintroPat)*)? : tactic
+
+macro_rules
+| `(tactic| convert_to $[$cfg]? $[←%$sym]? $term $[with $ps?*]?) =>
+  `(tactic| convert $[$cfg]? $[←%$sym]? (?_ : $term) using 1 $[with $ps?*]?)
+| `(tactic| convert_to $[$cfg]? $[←%$sym]? $term using $n $[with $ps?*]?) =>
+  `(tactic| convert $[$cfg]? $[←%$sym]? (?_ : $term) using $n $[with $ps?*]?)
+
+/--
+`ac_change g using n` is `convert_to g using n` followed by `ac_rfl`. It is useful for
+rearranging/reassociating e.g. sums:
+```lean
+example (a b c d e f g N : ℕ) : (a + b) + (c + d) + (e + f) + g ≤ N := by
+  ac_change a + d + e + f + c + g + b ≤ _
+  -- ⊢ a + d + e + f + c + g + b ≤ N
+```
+-/
+syntax (name := acChange) "ac_change " term (" using " num)? : tactic
+
+macro_rules
+| `(tactic| ac_change $t $[using $n]?) => `(tactic| convert_to $t:term $[using $n]? <;> try ac_rfl)
+
+end Lean.Parser.Tactic

src/Init/PropLemmas.lean

@@ -23,6 +23,20 @@ set_option linter.missingDocs true -- keep it documented
 @[simp] theorem eq_true_eq_id : Eq True = id := by
   funext _; simp only [true_iff, id.def, eq_iff_iff]
 
+theorem proof_irrel_heq {p q : Prop} (hp : p) (hq : q) : HEq hp hq := by
+  cases propext (iff_of_true hp hq); rfl
+
+theorem hfunext {α α' : Sort u} {β : α → Sort v} {β' : α' → Sort v} {f : ∀a, β a} {f' : ∀a, β' a}
+    (hα : α = α') (h : ∀a a', HEq a a' → HEq (f a) (f' a')) : HEq f f' := by
+  subst hα
+  have : ∀a, HEq (f a) (f' a) := λ a => h a a (HEq.refl a)
+  have : β = β' := by funext a
+                      exact type_eq_of_heq (this a)
+  subst this
+  apply heq_of_eq
+  funext a
+  exact eq_of_heq (this a)
+
 /-! ## not -/
 
 theorem not_not_em (a : Prop) : ¬¬(a ∨ ¬a) := fun h => h (.inr (h ∘ .inl))

src/Init/SimpLemmas.lean

@@ -45,7 +45,7 @@ theorem implies_dep_congr_ctx {p₁ p₂ q₁ : Prop} (h₁ : p₁ = p₂) {q₂
 theorem implies_congr_ctx {p₁ p₂ q₁ q₂ : Prop} (h₁ : p₁ = p₂) (h₂ : p₂ → q₁ = q₂) : (p₁ → q₁) = (p₂ → q₂) :=
   implies_dep_congr_ctx h₁ h₂
 
-theorem forall_congr {α : Sort u} {p q : α → Prop} (h : ∀ a, p a = q a) : (∀ a, p a) = (∀ a, q a) :=
+theorem forall_congr {α : Sort u} {p q : α → Sort v} (h : ∀ a, p a = q a) : (∀ a, p a) = (∀ a, q a) :=
   (funext h : p = q) ▸ rfl
 
 theorem forall_prop_domain_congr {p₁ p₂ : Prop} {q₁ : p₁ → Prop} {q₂ : p₂ → Prop}

src/Init/Tactics.lean

@@ -950,7 +950,6 @@ while `congr 2` produces the intended `⊢ x + y = y + x`.
 -/
 syntax (name := congr) "congr" (ppSpace num)? : tactic
 
-
 /--
 In tactic mode, `if h : t then tac1 else tac2` can be used as alternative syntax for:
 ```

src/Lean/Elab/Tactic.lean

@@ -38,3 +38,6 @@ import Lean.Elab.Tactic.Symm
 import Lean.Elab.Tactic.SolveByElim
 import Lean.Elab.Tactic.LibrarySearch
 import Lean.Elab.Tactic.ShowTerm
+import Lean.Elab.Tactic.Rfl
+import Lean.Elab.Tactic.Congr!
+import Lean.Elab.Tactic.Convert

src/Lean/Elab/Tactic/Congr!.lean

@@ -0,0 +1,37 @@
+/-
+Copyright (c) 2023 Kyle Miller. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kyle Miller
+-/
+prelude
+import Init.Congr!
+import Lean.Meta.Tactic.Congr!
+
+/-!
+# The `congr!` tactic
+
+This is a more powerful version of the `congr` tactic that knows about more congruence lemmas and
+can apply to more situations. It is similar to the `congr'` tactic from Mathlib 3.
+
+The `congr!` tactic is used by the `convert` and `convert_to` tactics.
+
+See the syntax docstring for more details.
+-/
+
+open Lean Elab Tactic Meta.Tactic.Congr!
+
+namespace Lean.Elab.Tactic
+
+declare_config_elab Congr!.elabConfig Config
+
+@[builtin_tactic «congr!»] def evalCongr! : Tactic := fun stx =>
+  match stx with
+  | `(tactic| congr! $[$cfg:config]? $[$n]? $[with $ps?*]?) => do
+    let config ← Congr!.elabConfig (mkOptionalNode cfg)
+    let patterns := (Lean.Elab.Tactic.RCases.expandRIntroPats (ps?.getD #[])).toList
+    liftMetaTactic fun g ↦
+      let depth := n.map (·.getNat)
+      g.congrN! depth config patterns
+  | _                     => throwUnsupportedSyntax
+
+end Lean.Elab.Tactic

src/Lean/Elab/Tactic/Congr.lean

@@ -9,7 +9,6 @@ import Lean.Elab.Tactic.Basic
 
 namespace Lean.Elab.Tactic
 
-namespace Lean.Elab.Tactic
 @[builtin_tactic Parser.Tactic.congr] def evalCongr : Tactic := fun stx =>
   match stx with
   | `(tactic| congr $[$n?]?) =>
@@ -19,5 +18,3 @@ namespace Lean.Elab.Tactic
   | _ => throwUnsupportedSyntax
 
 end Lean.Elab.Tactic
-
-

src/Lean/Elab/Tactic/Conv/Congr.lean

@@ -176,6 +176,7 @@ private def extCore (mvarId : MVarId) (userName? : Option Name) : MetaM MVarId :
     let lhs := (← instantiateMVars lhs).cleanupAnnotations
     if let .forallE n d b bi := lhs then
       let u ← getLevel d
+      let v ← getLevel b
       let p : Expr := .lam n d b bi
       let userName ← if let some userName := userName? then pure userName else mkFreshBinderNameForTactic n
       let (q, h, mvarNew) ← withLocalDecl userName bi d fun a => do
@@ -187,7 +188,7 @@ private def extCore (mvarId : MVarId) (userName? : Option Name) : MetaM MVarId :
         unless (← isDefEqGuarded rhs rhs') do
           throwError "invalid 'ext' conv tactic, failed to resolve{indentExpr rhs}\n=?={indentExpr rhs'}"
         return (q, h, mvarNew)
-      let proof := mkApp4 (mkConst ``forall_congr [u]) d p q h
+      let proof := mkApp4 (mkConst ``forall_congr [u, v]) d p q h
       mvarId.assign proof
       return mvarNew.mvarId!
     else if let some mvarId ← extLetBodyCongr? mvarId lhs rhs then

src/Lean/Elab/Tactic/Convert.lean

@@ -0,0 +1,34 @@
+/-
+Copyright (c) 2022 Scott Morrison. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Scott Morrison
+-/
+import Lean.Meta.Tactic.Convert
+import Lean.Elab.Tactic.Congr!
+
+open Lean Meta Tactic Congr!
+
+namespace Lean.Elab.Tactic
+
+@[builtin_tactic «convert»] def evalConvert : Tactic := fun stx =>
+  match stx with
+  | `(tactic| convert $[$cfg:config]? $[←%$sym]? $term $[using $n]? $[with $ps?*]?) =>
+    withMainContext do
+      let config ← Congr!.elabConfig (mkOptionalNode cfg)
+      let patterns := (Lean.Elab.Tactic.RCases.expandRIntroPats (ps?.getD #[])).toList
+      let expectedType ← mkFreshExprMVar (mkSort (← getLevel (← getMainTarget)))
+      let (e, gs) ←
+        withCollectingNewGoalsFrom (allowNaturalHoles := true) (tagSuffix := `convert) do
+          -- Allow typeclass inference failures since these will be inferred by unification
+          -- or else become new goals
+          withTheReader Term.Context (fun ctx => { ctx with ignoreTCFailures := true }) do
+            let t ← elabTermEnsuringType (mayPostpone := true) term expectedType
+            -- Process everything so that tactics get run, but again allow TC failures
+            Term.synthesizeSyntheticMVars (mayPostpone := false) (ignoreStuckTC := true)
+            -- Use a type hint to ensure we collect goals from the type too
+            mkExpectedTypeHint t (← inferType t)
+      liftMetaTactic fun g ↦
+        return (← g.convert e sym.isSome (n.map (·.getNat)) config patterns) ++ gs
+  | _                     => throwUnsupportedSyntax
+
+end Lean.Elab.Tactic

src/Lean/Elab/Tactic/Rfl.lean

@@ -0,0 +1,26 @@
+/-
+Copyright (c) 2022 Newell Jensen. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Newell Jensen, Thomas Murrills
+-/
+prelude
+import Lean.Meta.Tactic.Rfl
+import Lean.Elab.Tactic.Basic
+
+/-!
+# `rfl` tactic extension for reflexive relations
+
+This extends the `rfl` tactic so that it works on any reflexive relation,
+provided the reflexivity lemma has been marked as `@[refl]`.
+-/
+
+namespace Lean.Elab.Tactic.Rfl
+
+/--
+This tactic applies to a goal whose target has the form `x ~ x`, where `~` is a reflexive
+relation, that is, a relation which has a reflexive lemma tagged with the attribute [refl].
+-/
+elab_rules : tactic
+  | `(tactic| rfl) => withMainContext do liftMetaFinishingTactic (·.applyRfl)
+
+end Lean.Elab.Tactic.Rfl

src/Lean/Meta/CongrTheorems.lean

@@ -4,329 +4,5 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import Lean.Meta.AppBuilder
-import Lean.Class
-
-namespace Lean.Meta
-
-inductive CongrArgKind where
-  /-- It is a parameter for the congruence theorem, the parameter occurs in the left and right hand sides. -/
-  | fixed
-  /--
-  It is not a parameter for the congruence theorem, the theorem was specialized for this parameter.
-  This only happens if the parameter is a subsingleton/proposition, and other parameters depend on it. -/
-  | fixedNoParam
-  /--
-  The lemma contains three parameters for this kind of argument `a_i`, `b_i` and `eq_i : a_i = b_i`.
-  `a_i` and `b_i` represent the left and right hand sides, and `eq_i` is a proof for their equality. -/
-  | eq
-  /--
-  The congr-simp theorems contains only one parameter for this kind of argument, and congr theorems contains two.
-  They correspond to arguments that are subsingletons/propositions. -/
-  | cast
-  /--
-  The lemma contains three parameters for this kind of argument `a_i`, `b_i` and `eq_i : HEq a_i b_i`.
-  `a_i` and `b_i` represent the left and right hand sides, and `eq_i` is a proof for their heterogeneous equality. -/
-  | heq
-  /--
-  For congr-simp theorems only.  Indicates a decidable instance argument.
-  The lemma contains two arguments [a_i : Decidable ...] [b_i : Decidable ...] -/
-  | subsingletonInst
-  deriving Inhabited, Repr
-
-structure CongrTheorem where
-  type     : Expr
-  proof    : Expr
-  argKinds : Array CongrArgKind
-
-private def addPrimeToFVarUserNames (ys : Array Expr) (lctx : LocalContext) : LocalContext := Id.run do
-  let mut lctx := lctx
-  for y in ys do
-    let decl := lctx.getFVar! y
-    lctx := lctx.setUserName decl.fvarId (decl.userName.appendAfter "'")
-  return lctx
-
-private def setBinderInfosD (ys : Array Expr) (lctx : LocalContext) : LocalContext := Id.run do
-  let mut lctx := lctx
-  for y in ys do
-    let decl := lctx.getFVar! y
-    lctx := lctx.setBinderInfo decl.fvarId BinderInfo.default
-  return lctx
-
-partial def mkHCongrWithArity (f : Expr) (numArgs : Nat) : MetaM CongrTheorem := do
-  let fType ← inferType f
-  forallBoundedTelescope fType numArgs fun xs _ =>
-  forallBoundedTelescope fType numArgs fun ys _ => do
-    if xs.size != numArgs then
-      throwError "failed to generate hcongr theorem, insufficient number of arguments"
-    else
-      let lctx := addPrimeToFVarUserNames ys (← getLCtx) |> setBinderInfosD ys |> setBinderInfosD xs
-      withLCtx lctx (← getLocalInstances) do
-      withNewEqs xs ys fun eqs argKinds => do
-        let mut hs := #[]
-        for x in xs, y in ys, eq in eqs do
-          hs := hs.push x |>.push y |>.push eq
-        let lhs := mkAppN f xs
-        let rhs := mkAppN f ys
-        let congrType ← mkForallFVars hs (← mkHEq lhs rhs)
-        return {
-          type  := congrType
-          proof := (← mkProof congrType)
-          argKinds
-        }
-where
-  withNewEqs {α} (xs ys : Array Expr) (k : Array Expr → Array CongrArgKind → MetaM α) : MetaM α :=
-    let rec loop (i : Nat) (eqs : Array Expr) (kinds : Array CongrArgKind) := do
-      if  i < xs.size then
-        let x := xs[i]!
-        let y := ys[i]!
-        let xType := (← inferType x).consumeTypeAnnotations
-        let yType := (← inferType y).consumeTypeAnnotations
-        if xType == yType then
-          withLocalDeclD ((`e).appendIndexAfter (i+1)) (← mkEq x y) fun h =>
-            loop (i+1) (eqs.push h) (kinds.push CongrArgKind.eq)
-        else
-          withLocalDeclD ((`e).appendIndexAfter (i+1)) (← mkHEq x y) fun h =>
-            loop (i+1) (eqs.push h) (kinds.push CongrArgKind.heq)
-      else
-        k eqs kinds
-    loop 0 #[] #[]
-
-  mkProof (type : Expr) : MetaM Expr := do
-    if let some (_, lhs, _) := type.eq? then
-      mkEqRefl lhs
-    else if let some (_, lhs, _, _) := type.heq? then
-      mkHEqRefl lhs
-    else
-      forallBoundedTelescope type (some 1) fun a type =>
-      let a := a[0]!
-      forallBoundedTelescope type (some 1) fun b motive =>
-      let b := b[0]!
-      let type := type.bindingBody!.instantiate1 a
-      withLocalDeclD motive.bindingName! motive.bindingDomain! fun eqPr => do
-      let type := type.bindingBody!
-      let motive := motive.bindingBody!
-      let minor ← mkProof type
-      let mut major := eqPr
-      if (← whnf (← inferType eqPr)).isHEq then
-        major ← mkEqOfHEq major
-      let motive ← mkLambdaFVars #[b] motive
-      mkLambdaFVars #[a, b, eqPr] (← mkEqNDRec motive minor major)
-
-def mkHCongr (f : Expr) : MetaM CongrTheorem := do
-  mkHCongrWithArity f (← getFunInfo f).getArity
-
-/--
-  Ensure that all dependencies for `congr_arg_kind::Eq` are `congr_arg_kind::Fixed`.
--/
-private def fixKindsForDependencies (info : FunInfo) (kinds : Array CongrArgKind) : Array CongrArgKind := Id.run do
-  let mut kinds := kinds
-  for i in [:info.paramInfo.size] do
-    for j in [i+1:info.paramInfo.size] do
-      if info.paramInfo[j]!.backDeps.contains i then
-        if kinds[j]! matches CongrArgKind.eq || kinds[j]! matches CongrArgKind.fixed then
-          -- We must fix `i` because there is a `j` that depends on `i` and `j` is not cast-fixed.
-          kinds := kinds.set! i CongrArgKind.fixed
-          break
-  return kinds
-
-/--
-  (Try to) cast expression `e` to the given type using the equations `eqs`.
-  `deps` contains the indices of the relevant equalities.
-  Remark: deps is sorted. -/
-private partial def mkCast (e : Expr) (type : Expr) (deps : Array Nat) (eqs : Array (Option Expr)) : MetaM Expr := do
-  let rec go (i : Nat) (type : Expr) : MetaM Expr := do
-     if i < deps.size then
-       match eqs[deps[i]!]! with
-       | none => go (i+1) type
-       | some major =>
-         let some (_, lhs, rhs) := (← inferType major).eq? | unreachable!
-         if (← dependsOn type major.fvarId!) then
-           let motive ← mkLambdaFVars #[rhs, major] type
-           let typeNew := type.replaceFVar rhs lhs |>.replaceFVar major (← mkEqRefl lhs)
-           let minor ← go (i+1) typeNew
-           mkEqRec motive minor major
-         else
-           let motive ← mkLambdaFVars #[rhs] type
-           let typeNew := type.replaceFVar rhs lhs
-           let minor ← go (i+1) typeNew
-           mkEqNDRec motive minor major
-     else
-       return e
-  go 0 type
-
-private def hasCastLike (kinds : Array CongrArgKind) : Bool :=
-  kinds.any fun kind => kind matches CongrArgKind.cast || kind matches CongrArgKind.subsingletonInst
-
-private def withNext (type : Expr) (k : Expr → Expr → MetaM α) : MetaM α := do
-  forallBoundedTelescope type (some 1) fun xs type => k xs[0]! type
-
-/--
-  Test whether we should use `subsingletonInst` kind for instances which depend on `eq`.
-  (Otherwise `fixKindsForDependencies`will downgrade them to Fixed -/
-private def shouldUseSubsingletonInst (info : FunInfo) (kinds : Array CongrArgKind) (i : Nat) : Bool := Id.run do
-  if info.paramInfo[i]!.isDecInst then
-    for j in info.paramInfo[i]!.backDeps do
-      if kinds[j]! matches CongrArgKind.eq then
-        return true
-  return false
-
-/--
-If `f` is a class constructor, return a bitmask `m` s.t. `m[i]` is true if the `i`-th parameter
-corresponds to a subobject field.
-
-We use this function to implement the special support for class constructors at `getCongrSimpKinds`.
-See issue #1808
--/
-private def getClassSubobjectMask? (f : Expr) : MetaM (Option (Array Bool)) := do
-  let .const declName _ := f | return none
-  let .ctorInfo val ← getConstInfo declName | return none
-  unless isClass (← getEnv) val.induct do return none
-  forallTelescopeReducing val.type fun xs _ => do
-    let env ← getEnv
-    let mut mask := #[]
-    for i in [:xs.size] do
-      if i < val.numParams then
-        mask := mask.push false
-      else
-        let localDecl ← xs[i]!.fvarId!.getDecl
-        mask := mask.push (isSubobjectField? env val.induct localDecl.userName).isSome
-    return some mask
-
-/-- Compute `CongrArgKind`s for a simp congruence theorem. -/
-def getCongrSimpKinds (f : Expr) (info : FunInfo) : MetaM (Array CongrArgKind) := do
-  /-
-  The default `CongrArgKind` is `eq`, which allows `simp` to rewrite this
-  argument. However, if there are references from `i` to `j`, we cannot
-  rewrite both `i` and `j`. So we must change the `CongrArgKind` at
-  either `i` or `j`. In principle, if there is a dependency with `i`
-  appearing after `j`, then we set `j` to `fixed` (or `cast`). But there is
-  an optimization: if `i` is a subsingleton, we can fix it instead of
-  `j`, since all subsingletons are equal anyway. The fixing happens in
-  two loops: one for the special cases, and one for the general case.
-
-  This method has special support for class constructors.
-  For this kind of function, we treat subobject fields as regular parameters instead of instance implicit ones.
-  We added this feature because of issue #1808
-  -/
-  let mut result := #[]
-  let mask? ← getClassSubobjectMask? f
-  for i in [:info.paramInfo.size] do
-    if info.resultDeps.contains i then
-      result := result.push .fixed
-    else if info.paramInfo[i]!.isProp then
-      result := result.push .cast
-    else if info.paramInfo[i]!.isInstImplicit then
-      if let some mask := mask? then
-        if h : i < mask.size then
-          if mask[i] then
-            -- Parameter is a subobect field of a class constructor. See comment above.
-            result := result.push .eq
-            continue
-      if shouldUseSubsingletonInst info result i then
-        result := result.push .subsingletonInst
-      else
-        result := result.push .fixed
-    else
-      result := result.push .eq
-  return fixKindsForDependencies info result
-
-/--
-  Create a congruence theorem that is useful for the simplifier and `congr` tactic.
--/
-partial def mkCongrSimpCore? (f : Expr) (info : FunInfo) (kinds : Array CongrArgKind) (subsingletonInstImplicitRhs : Bool := true) : MetaM (Option CongrTheorem) := do
-  if let some result ← mk? f info kinds then
-    return some result
-  else if hasCastLike kinds then
-    -- Simplify kinds and try again
-    let kinds := kinds.map fun kind =>
-      if kind matches CongrArgKind.cast || kind matches CongrArgKind.subsingletonInst then CongrArgKind.fixed else kind
-    mk? f info kinds
-  else
-    return none
-where
-  /--
-    Create a congruence theorem that is useful for the simplifier.
-    In this kind of theorem, if the i-th argument is a `cast` argument, then the theorem
-    contains an input `a_i` representing the i-th argument in the left-hand-side, and
-    it appears with a cast (e.g., `Eq.drec ... a_i ...`) in the right-hand-side.
-    The idea is that the right-hand-side of this theorem "tells" the simplifier
-    how the resulting term looks like. -/
-  mk? (f : Expr) (info : FunInfo) (kinds : Array CongrArgKind) : MetaM (Option CongrTheorem) := do
-    try
-      let fType ← inferType f
-      forallBoundedTelescope fType kinds.size fun lhss _ => do
-        if lhss.size != kinds.size then return none
-        let rec go (i : Nat) (rhss : Array Expr) (eqs : Array (Option Expr)) (hyps : Array Expr) : MetaM CongrTheorem := do
-          if i == kinds.size then
-            let lhs := mkAppN f lhss
-            let rhs := mkAppN f rhss
-            let type ← mkForallFVars hyps (← mkEq lhs rhs)
-            let proof ← mkProof type kinds
-            return { type, proof, argKinds := kinds }
-          else
-            let hyps := hyps.push lhss[i]!
-            match kinds[i]! with
-            | .heq | .fixedNoParam => unreachable!
-            | .eq =>
-              let localDecl ← lhss[i]!.fvarId!.getDecl
-              withLocalDecl localDecl.userName localDecl.binderInfo localDecl.type fun rhs => do
-              withLocalDeclD (localDecl.userName.appendBefore "e_") (← mkEq lhss[i]! rhs) fun eq => do
-                go (i+1) (rhss.push rhs) (eqs.push eq) (hyps.push rhs |>.push eq)
-            | .fixed => go (i+1) (rhss.push lhss[i]!) (eqs.push none) hyps
-            | .cast =>
-              let rhsType := (← inferType lhss[i]!).replaceFVars (lhss[:rhss.size]) rhss
-              let rhs ← mkCast lhss[i]! rhsType info.paramInfo[i]!.backDeps eqs
-              go (i+1) (rhss.push rhs) (eqs.push none) hyps
-            | .subsingletonInst =>
-              -- The `lhs` does not need to instance implicit since it can be inferred from the LHS
-              withNewBinderInfos #[(lhss[i]!.fvarId!, .implicit)] do
-                let rhsType := (← inferType lhss[i]!).replaceFVars (lhss[:rhss.size]) rhss
-                let rhsBi   := if subsingletonInstImplicitRhs then .instImplicit else .implicit
-                withLocalDecl (← lhss[i]!.fvarId!.getDecl).userName rhsBi rhsType fun rhs =>
-                  go (i+1) (rhss.push rhs) (eqs.push none) (hyps.push rhs)
-        return some (← go 0 #[] #[] #[])
-    catch _ =>
-      return none
-
-  mkProof (type : Expr) (kinds : Array CongrArgKind) : MetaM Expr := do
-    let rec go (i : Nat) (type : Expr) : MetaM Expr := do
-      if i == kinds.size then
-        let some (_, lhs, _) := type.eq? | unreachable!
-        mkEqRefl lhs
-      else
-        withNext type fun lhs type => do
-        match kinds[i]! with
-        | .heq | .fixedNoParam => unreachable!
-        | .fixed => mkLambdaFVars #[lhs] (← go (i+1) type)
-        | .cast => mkLambdaFVars #[lhs] (← go (i+1) type)
-        | .eq =>
-          let typeSub := type.bindingBody!.bindingBody!.instantiate #[(← mkEqRefl lhs), lhs]
-          withNext type fun rhs type =>
-          withNext type fun heq type => do
-            let motive ← mkLambdaFVars #[rhs, heq] type
-            let proofSub ← go (i+1) typeSub
-            mkLambdaFVars #[lhs, rhs, heq] (← mkEqRec motive proofSub heq)
-        | .subsingletonInst =>
-          let typeSub := type.bindingBody!.instantiate #[lhs]
-          withNext type fun rhs type => do
-            let motive ← mkLambdaFVars #[rhs] type
-            let proofSub ← go (i+1) typeSub
-            let heq ← mkAppM ``Subsingleton.elim #[lhs, rhs]
-            mkLambdaFVars #[lhs, rhs] (← mkEqNDRec motive proofSub heq)
-     go 0 type
-
-/--
-Create a congruence theorem for `f`. The theorem is used in the simplifier.
-
-If `subsingletonInstImplicitRhs = true`, the the `rhs` corresponding to `[Decidable p]` parameters
-is marked as instance implicit. It forces the simplifier to compute the new instance when applying
-the congruence theorem.
-For the `congr` tactic we set it to `false`.
--/
-def mkCongrSimp? (f : Expr) (subsingletonInstImplicitRhs : Bool := true) : MetaM (Option CongrTheorem) := do
-  let f := (← instantiateMVars f).cleanupAnnotations
-  let info ← getFunInfo f
-  mkCongrSimpCore? f info (← getCongrSimpKinds f info) (subsingletonInstImplicitRhs := subsingletonInstImplicitRhs)
-
-end Lean.Meta
+import Lean.Meta.CongrTheorems.Basic
+import Lean.Meta.CongrTheorems.Rich

src/Lean/Meta/CongrTheorems/Basic.lean

@@ -0,0 +1,332 @@
+/-
+Copyright (c) 2021 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import Lean.Meta.AppBuilder
+import Lean.Class
+
+namespace Lean.Meta
+
+inductive CongrArgKind where
+  /-- It is a parameter for the congruence theorem, the parameter occurs in the left and right hand sides. -/
+  | fixed
+  /--
+  It is not a parameter for the congruence theorem, the theorem was specialized for this parameter.
+  This only happens if the parameter is a subsingleton/proposition, and other parameters depend on it. -/
+  | fixedNoParam
+  /--
+  The lemma contains three parameters for this kind of argument `a_i`, `b_i` and `eq_i : a_i = b_i`.
+  `a_i` and `b_i` represent the left and right hand sides, and `eq_i` is a proof for their equality. -/
+  | eq
+  /--
+  The congr-simp theorems contains only one parameter for this kind of argument, and congr theorems contains two.
+  They correspond to arguments that are subsingletons/propositions. -/
+  | cast
+  /--
+  The lemma contains three parameters for this kind of argument `a_i`, `b_i` and `eq_i : HEq a_i b_i`.
+  `a_i` and `b_i` represent the left and right hand sides, and `eq_i` is a proof for their heterogeneous equality. -/
+  | heq
+  /--
+  For congr-simp theorems only.  Indicates a decidable instance argument.
+  The lemma contains two arguments [a_i : Decidable ...] [b_i : Decidable ...] -/
+  | subsingletonInst
+  deriving Inhabited, Repr
+
+structure CongrTheorem where
+  type     : Expr
+  proof    : Expr
+  argKinds : Array CongrArgKind
+
+private def addPrimeToFVarUserNames (ys : Array Expr) (lctx : LocalContext) : LocalContext := Id.run do
+  let mut lctx := lctx
+  for y in ys do
+    let decl := lctx.getFVar! y
+    lctx := lctx.setUserName decl.fvarId (decl.userName.appendAfter "'")
+  return lctx
+
+private def setBinderInfosD (ys : Array Expr) (lctx : LocalContext) : LocalContext := Id.run do
+  let mut lctx := lctx
+  for y in ys do
+    let decl := lctx.getFVar! y
+    lctx := lctx.setBinderInfo decl.fvarId BinderInfo.default
+  return lctx
+
+partial def mkHCongrWithArity (f : Expr) (numArgs : Nat) : MetaM CongrTheorem := do
+  let fType ← inferType f
+  forallBoundedTelescope fType numArgs fun xs _ =>
+  forallBoundedTelescope fType numArgs fun ys _ => do
+    if xs.size != numArgs then
+      throwError "failed to generate hcongr theorem, insufficient number of arguments"
+    else
+      let lctx := addPrimeToFVarUserNames ys (← getLCtx) |> setBinderInfosD ys |> setBinderInfosD xs
+      withLCtx lctx (← getLocalInstances) do
+      withNewEqs xs ys fun eqs argKinds => do
+        let mut hs := #[]
+        for x in xs, y in ys, eq in eqs do
+          hs := hs.push x |>.push y |>.push eq
+        let lhs := mkAppN f xs
+        let rhs := mkAppN f ys
+        let congrType ← mkForallFVars hs (← mkHEq lhs rhs)
+        return {
+          type  := congrType
+          proof := (← mkProof congrType)
+          argKinds
+        }
+where
+  withNewEqs {α} (xs ys : Array Expr) (k : Array Expr → Array CongrArgKind → MetaM α) : MetaM α :=
+    let rec loop (i : Nat) (eqs : Array Expr) (kinds : Array CongrArgKind) := do
+      if  i < xs.size then
+        let x := xs[i]!
+        let y := ys[i]!
+        let xType := (← inferType x).consumeTypeAnnotations
+        let yType := (← inferType y).consumeTypeAnnotations
+        if xType == yType then
+          withLocalDeclD ((`e).appendIndexAfter (i+1)) (← mkEq x y) fun h =>
+            loop (i+1) (eqs.push h) (kinds.push CongrArgKind.eq)
+        else
+          withLocalDeclD ((`e).appendIndexAfter (i+1)) (← mkHEq x y) fun h =>
+            loop (i+1) (eqs.push h) (kinds.push CongrArgKind.heq)
+      else
+        k eqs kinds
+    loop 0 #[] #[]
+
+  mkProof (type : Expr) : MetaM Expr := do
+    if let some (_, lhs, _) := type.eq? then
+      mkEqRefl lhs
+    else if let some (_, lhs, _, _) := type.heq? then
+      mkHEqRefl lhs
+    else
+      forallBoundedTelescope type (some 1) fun a type =>
+      let a := a[0]!
+      forallBoundedTelescope type (some 1) fun b motive =>
+      let b := b[0]!
+      let type := type.bindingBody!.instantiate1 a
+      withLocalDeclD motive.bindingName! motive.bindingDomain! fun eqPr => do
+      let type := type.bindingBody!
+      let motive := motive.bindingBody!
+      let minor ← mkProof type
+      let mut major := eqPr
+      if (← whnf (← inferType eqPr)).isHEq then
+        major ← mkEqOfHEq major
+      let motive ← mkLambdaFVars #[b] motive
+      mkLambdaFVars #[a, b, eqPr] (← mkEqNDRec motive minor major)
+
+def mkHCongr (f : Expr) : MetaM CongrTheorem := do
+  mkHCongrWithArity f (← getFunInfo f).getArity
+
+/--
+  Ensure that all dependencies for `congr_arg_kind::Eq` are `congr_arg_kind::Fixed`.
+-/
+private def fixKindsForDependencies (info : FunInfo) (kinds : Array CongrArgKind) : Array CongrArgKind := Id.run do
+  let mut kinds := kinds
+  for i in [:info.paramInfo.size] do
+    for j in [i+1:info.paramInfo.size] do
+      if info.paramInfo[j]!.backDeps.contains i then
+        if kinds[j]! matches CongrArgKind.eq || kinds[j]! matches CongrArgKind.fixed then
+          -- We must fix `i` because there is a `j` that depends on `i` and `j` is not cast-fixed.
+          kinds := kinds.set! i CongrArgKind.fixed
+          break
+  return kinds
+
+/--
+  (Try to) cast expression `e` to the given type using the equations `eqs`.
+  `deps` contains the indices of the relevant equalities.
+  Remark: deps is sorted. -/
+private partial def mkCast (e : Expr) (type : Expr) (deps : Array Nat) (eqs : Array (Option Expr)) : MetaM Expr := do
+  let rec go (i : Nat) (type : Expr) : MetaM Expr := do
+     if i < deps.size then
+       match eqs[deps[i]!]! with
+       | none => go (i+1) type
+       | some major =>
+         let some (_, lhs, rhs) := (← inferType major).eq? | unreachable!
+         if (← dependsOn type major.fvarId!) then
+           let motive ← mkLambdaFVars #[rhs, major] type
+           let typeNew := type.replaceFVar rhs lhs |>.replaceFVar major (← mkEqRefl lhs)
+           let minor ← go (i+1) typeNew
+           mkEqRec motive minor major
+         else
+           let motive ← mkLambdaFVars #[rhs] type
+           let typeNew := type.replaceFVar rhs lhs
+           let minor ← go (i+1) typeNew
+           mkEqNDRec motive minor major
+     else
+       return e
+  go 0 type
+
+private def hasCastLike (kinds : Array CongrArgKind) : Bool :=
+  kinds.any fun kind => kind matches CongrArgKind.cast || kind matches CongrArgKind.subsingletonInst
+
+private def withNext (type : Expr) (k : Expr → Expr → MetaM α) : MetaM α := do
+  forallBoundedTelescope type (some 1) fun xs type => k xs[0]! type
+
+/--
+  Test whether we should use `subsingletonInst` kind for instances which depend on `eq`.
+  (Otherwise `fixKindsForDependencies`will downgrade them to Fixed -/
+private def shouldUseSubsingletonInst (info : FunInfo) (kinds : Array CongrArgKind) (i : Nat) : Bool := Id.run do
+  if info.paramInfo[i]!.isDecInst then
+    for j in info.paramInfo[i]!.backDeps do
+      if kinds[j]! matches CongrArgKind.eq then
+        return true
+  return false
+
+/--
+If `f` is a class constructor, return a bitmask `m` s.t. `m[i]` is true if the `i`-th parameter
+corresponds to a subobject field.
+
+We use this function to implement the special support for class constructors at `getCongrSimpKinds`.
+See issue #1808
+-/
+private def getClassSubobjectMask? (f : Expr) : MetaM (Option (Array Bool)) := do
+  let .const declName _ := f | return none
+  let .ctorInfo val ← getConstInfo declName | return none
+  unless isClass (← getEnv) val.induct do return none
+  forallTelescopeReducing val.type fun xs _ => do
+    let env ← getEnv
+    let mut mask := #[]
+    for i in [:xs.size] do
+      if i < val.numParams then
+        mask := mask.push false
+      else
+        let localDecl ← xs[i]!.fvarId!.getDecl
+        mask := mask.push (isSubobjectField? env val.induct localDecl.userName).isSome
+    return some mask
+
+/-- Compute `CongrArgKind`s for a simp congruence theorem. -/
+def getCongrSimpKinds (f : Expr) (info : FunInfo) : MetaM (Array CongrArgKind) := do
+  /-
+  The default `CongrArgKind` is `eq`, which allows `simp` to rewrite this
+  argument. However, if there are references from `i` to `j`, we cannot
+  rewrite both `i` and `j`. So we must change the `CongrArgKind` at
+  either `i` or `j`. In principle, if there is a dependency with `i`
+  appearing after `j`, then we set `j` to `fixed` (or `cast`). But there is
+  an optimization: if `i` is a subsingleton, we can fix it instead of
+  `j`, since all subsingletons are equal anyway. The fixing happens in
+  two loops: one for the special cases, and one for the general case.
+
+  This method has special support for class constructors.
+  For this kind of function, we treat subobject fields as regular parameters instead of instance implicit ones.
+  We added this feature because of issue #1808
+  -/
+  let mut result := #[]
+  let mask? ← getClassSubobjectMask? f
+  for i in [:info.paramInfo.size] do
+    if info.resultDeps.contains i then
+      result := result.push .fixed
+    else if info.paramInfo[i]!.isProp then
+      result := result.push .cast
+    else if info.paramInfo[i]!.isInstImplicit then
+      if let some mask := mask? then
+        if h : i < mask.size then
+          if mask[i] then
+            -- Parameter is a subobect field of a class constructor. See comment above.
+            result := result.push .eq
+            continue
+      if shouldUseSubsingletonInst info result i then
+        result := result.push .subsingletonInst
+      else
+        result := result.push .fixed
+    else
+      result := result.push .eq
+  return fixKindsForDependencies info result
+
+/--
+  Create a congruence theorem that is useful for the simplifier and `congr` tactic.
+-/
+partial def mkCongrSimpCore? (f : Expr) (info : FunInfo) (kinds : Array CongrArgKind) (subsingletonInstImplicitRhs : Bool := true) : MetaM (Option CongrTheorem) := do
+  if let some result ← mk? f info kinds then
+    return some result
+  else if hasCastLike kinds then
+    -- Simplify kinds and try again
+    let kinds := kinds.map fun kind =>
+      if kind matches CongrArgKind.cast || kind matches CongrArgKind.subsingletonInst then CongrArgKind.fixed else kind
+    mk? f info kinds
+  else
+    return none
+where
+  /--
+    Create a congruence theorem that is useful for the simplifier.
+    In this kind of theorem, if the i-th argument is a `cast` argument, then the theorem
+    contains an input `a_i` representing the i-th argument in the left-hand-side, and
+    it appears with a cast (e.g., `Eq.drec ... a_i ...`) in the right-hand-side.
+    The idea is that the right-hand-side of this theorem "tells" the simplifier
+    how the resulting term looks like. -/
+  mk? (f : Expr) (info : FunInfo) (kinds : Array CongrArgKind) : MetaM (Option CongrTheorem) := do
+    try
+      let fType ← inferType f
+      forallBoundedTelescope fType kinds.size fun lhss _ => do
+        if lhss.size != kinds.size then return none
+        let rec go (i : Nat) (rhss : Array Expr) (eqs : Array (Option Expr)) (hyps : Array Expr) : MetaM CongrTheorem := do
+          if i == kinds.size then
+            let lhs := mkAppN f lhss
+            let rhs := mkAppN f rhss
+            let type ← mkForallFVars hyps (← mkEq lhs rhs)
+            let proof ← mkProof type kinds
+            return { type, proof, argKinds := kinds }
+          else
+            let hyps := hyps.push lhss[i]!
+            match kinds[i]! with
+            | .heq | .fixedNoParam => unreachable!
+            | .eq =>
+              let localDecl ← lhss[i]!.fvarId!.getDecl
+              withLocalDecl localDecl.userName localDecl.binderInfo localDecl.type fun rhs => do
+              withLocalDeclD (localDecl.userName.appendBefore "e_") (← mkEq lhss[i]! rhs) fun eq => do
+                go (i+1) (rhss.push rhs) (eqs.push eq) (hyps.push rhs |>.push eq)
+            | .fixed => go (i+1) (rhss.push lhss[i]!) (eqs.push none) hyps
+            | .cast =>
+              let rhsType := (← inferType lhss[i]!).replaceFVars (lhss[:rhss.size]) rhss
+              let rhs ← mkCast lhss[i]! rhsType info.paramInfo[i]!.backDeps eqs
+              go (i+1) (rhss.push rhs) (eqs.push none) hyps
+            | .subsingletonInst =>
+              -- The `lhs` does not need to instance implicit since it can be inferred from the LHS
+              withNewBinderInfos #[(lhss[i]!.fvarId!, .implicit)] do
+                let rhsType := (← inferType lhss[i]!).replaceFVars (lhss[:rhss.size]) rhss
+                let rhsBi   := if subsingletonInstImplicitRhs then .instImplicit else .implicit
+                withLocalDecl (← lhss[i]!.fvarId!.getDecl).userName rhsBi rhsType fun rhs =>
+                  go (i+1) (rhss.push rhs) (eqs.push none) (hyps.push rhs)
+        return some (← go 0 #[] #[] #[])
+    catch _ =>
+      return none
+
+  mkProof (type : Expr) (kinds : Array CongrArgKind) : MetaM Expr := do
+    let rec go (i : Nat) (type : Expr) : MetaM Expr := do
+      if i == kinds.size then
+        let some (_, lhs, _) := type.eq? | unreachable!
+        mkEqRefl lhs
+      else
+        withNext type fun lhs type => do
+        match kinds[i]! with
+        | .heq | .fixedNoParam => unreachable!
+        | .fixed => mkLambdaFVars #[lhs] (← go (i+1) type)
+        | .cast => mkLambdaFVars #[lhs] (← go (i+1) type)
+        | .eq =>
+          let typeSub := type.bindingBody!.bindingBody!.instantiate #[(← mkEqRefl lhs), lhs]
+          withNext type fun rhs type =>
+          withNext type fun heq type => do
+            let motive ← mkLambdaFVars #[rhs, heq] type
+            let proofSub ← go (i+1) typeSub
+            mkLambdaFVars #[lhs, rhs, heq] (← mkEqRec motive proofSub heq)
+        | .subsingletonInst =>
+          let typeSub := type.bindingBody!.instantiate #[lhs]
+          withNext type fun rhs type => do
+            let motive ← mkLambdaFVars #[rhs] type
+            let proofSub ← go (i+1) typeSub
+            let heq ← mkAppM ``Subsingleton.elim #[lhs, rhs]
+            mkLambdaFVars #[lhs, rhs] (← mkEqNDRec motive proofSub heq)
+     go 0 type
+
+/--
+Create a congruence theorem for `f`. The theorem is used in the simplifier.
+
+If `subsingletonInstImplicitRhs = true`, the the `rhs` corresponding to `[Decidable p]` parameters
+is marked as instance implicit. It forces the simplifier to compute the new instance when applying
+the congruence theorem.
+For the `congr` tactic we set it to `false`.
+-/
+def mkCongrSimp? (f : Expr) (subsingletonInstImplicitRhs : Bool := true) : MetaM (Option CongrTheorem) := do
+  let f := (← instantiateMVars f).cleanupAnnotations
+  let info ← getFunInfo f
+  mkCongrSimpCore? f info (← getCongrSimpKinds f info) (subsingletonInstImplicitRhs := subsingletonInstImplicitRhs)
+
+end Lean.Meta

src/Lean/Meta/CongrTheorems/Rich.lean

@@ -0,0 +1,266 @@
+/-
+Copyright (c) 2023 Kyle Miller. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kyle Miller
+-/
+prelude
+import Lean.Meta.CongrTheorems.Basic
+import Lean.Meta.Tactic.Apply
+import Lean.Meta.Tactic.Cleanup
+import Lean.Meta.Tactic.Cases
+import Lean.Meta.Tactic.Refl
+import Lean.Class
+
+namespace Lean.Meta
+
+initialize registerTraceClass `Meta.CongrTheorems
+
+/-- Generates a congruence lemma for a function `f` for `numArgs` of its arguments.
+The only `Lean.Meta.CongrArgKind` kinds that appear in such a lemma
+are `.eq`, `.heq`, and `.subsingletonInst`.
+The resulting lemma proves either an `Eq` or a `HEq` depending on whether the types
+of the LHS and RHS are equal or not.
+
+This function is a wrapper around `Lean.Meta.mkHCongrWithArity`.
+It transforms the resulting congruence lemma by trying to automatically prove hypotheses
+using subsingleton lemmas, and if they are so provable they are recorded with `.subsingletonInst`.
+Note that this is slightly abusing `.subsingletonInst` since
+(1) the argument might not be for a `Decidable` instance and
+(2) the argument might not even be an instance. -/
+def mkHCongrWithArity' (f : Expr) (numArgs : Nat) : MetaM CongrTheorem := do
+  let thm ← mkHCongrWithArity f numArgs
+  process thm thm.type thm.argKinds.toList #[] #[] #[]
+where
+  /-- Process the congruence theorem by trying to pre-prove arguments using `prove`. -/
+  process (cthm : CongrTheorem) (type : Expr) (argKinds : List CongrArgKind)
+      (argKinds' : Array CongrArgKind) (params args : Array Expr) : MetaM CongrTheorem := do
+    match argKinds with
+    | [] =>
+      if params.size == args.size then
+        return cthm
+      else
+        let pf' ← mkLambdaFVars params (mkAppN cthm.proof args)
+        return {proof := pf', type := ← inferType pf', argKinds := argKinds'}
+    | argKind :: argKinds =>
+      match argKind with
+      | .eq | .heq =>
+        forallBoundedTelescope type (some 3) fun params' type' => do
+          let #[x, y, eq] := params' | unreachable!
+          -- See if we can prove `eq` from previous parameters.
+          let g := (← mkFreshExprMVar (← inferType eq)).mvarId!
+          let g ← g.clear eq.fvarId!
+          if (← observing? <| prove g params).isSome then
+            process cthm type' argKinds (argKinds'.push .subsingletonInst)
+              (params := params ++ #[x, y]) (args := args ++ #[x, y, .mvar g])
+          else
+            process cthm type' argKinds (argKinds'.push argKind)
+              (params := params ++ params') (args := args ++ params')
+      | _ => panic! "Unexpected CongrArgKind"
+  /-- Close the goal given only the fvars in `params`, or else fails. -/
+  prove (g : MVarId) (params : Array Expr) : MetaM Unit := do
+    -- Prune the local context.
+    let g ← g.cleanup
+    -- Substitute equalities that come from only this congruence lemma.
+    let [g] ← g.casesRec fun localDecl => do
+      return (localDecl.type.isEq || localDecl.type.isHEq) && params.contains localDecl.toExpr
+      | failure
+    try g.refl; return catch _ => pure ()
+    try g.hrefl; return catch _ => pure ()
+    if ← g.proofIrrelHeq then return
+    -- Make the goal be an eq and then try `Subsingleton.elim`
+    let g ← g.heqOfEq
+    if ← g.subsingletonElim then return
+    -- We have no more tricks.
+    failure
+
+/--
+`mkRichHCongr fType funInfo fixedFun fixedParams forceHEq`
+create a congruence lemma to prove that `Eq/HEq (f a₁ ... aₙ) (f' a₁' ... aₙ')`.
+The functions have type `fType` and the number of arguments is governed by the `funInfo` data.
+Each argument produces an `Eq/HEq aᵢ aᵢ'` hypothesis, but we also provide these hypotheses
+the additional facts that the preceding equalities have been proved (unlike in `mkHCongrWithArity`).
+The first two arguments of the resulting theorem are for `f` and `f'`, followed by a proof
+of `f = f'`, unless `fixedFun` is `true` (see below).
+
+When including hypotheses about previous hypotheses, we make use of dependency information
+and only include relevant equalities.
+
+The argument `fty` denotes the type of `f`. The arity of the resulting congruence lemma is
+controlled by the size of the `info` array.
+
+For the purpose of generating nicer lemmas (to help `to_additive` for example),
+this function supports generating lemmas where certain parameters
+are meant to be fixed:
+
+* If `fixedFun` is `false` (the default) then the lemma starts with three arguments for `f`, `f'`,
+and `h : f = f'`. Otherwise, if `fixedFun` is `true` then the lemma starts with just `f`.
+
+* If the `fixedParams` argument has `true` for a particular argument index, then this is a hint
+that the congruence lemma may use the same parameter for both sides of the equality. There is
+no guarantee -- it respects it if the types are equal for that parameter (i.e., if the parameter
+does not depend on non-fixed parameters).
+
+If `forceHEq` is `true` then the conclusion of the generated theorem is a `HEq`.
+Otherwise it might be an `Eq` if the equality is homogeneous.
+
+This is the interpretation of the `CongrArgKind`s in the generated congruence theorem:
+* `.eq` corresponds to having three arguments `(x : α) (x' : α) (h : x = x')`.
+  Note that `h` might have additional hypotheses.
+* `.heq` corresponds to having three arguments `(x : α) (x' : α') (h : HEq x x')`
+  Note that `h` might have additional hypotheses.
+* `.fixed` corresponds to having a single argument `(x : α)` that is fixed between the LHS and RHS
+* `.subsingletonInst` corresponds to having two arguments `(x : α) (x' : α')` for which the
+  congruence generator was able to prove that `HEq x x'` already. This is a slight abuse of
+  this `CongrArgKind` since this is used even for types that are not subsingleton typeclasses.
+
+Note that the first entry in this array is for the function itself.
+-/
+partial def mkRichHCongr (fType : Expr) (info : FunInfo)
+    (fixedFun : Bool := false) (fixedParams : Array Bool := #[])
+    (forceHEq : Bool := false) :
+    MetaM CongrTheorem := do
+  trace[Meta.CongrTheorems] "ftype: {fType}"
+  trace[Meta.CongrTheorems] "deps: {info.paramInfo.map (fun p => p.backDeps)}"
+  trace[Meta.CongrTheorems] "fixedFun={fixedFun}, fixedParams={fixedParams}"
+  doubleTelescope fType info.getArity fixedParams fun xs ys fixedParams => do
+    trace[Meta.CongrTheorems] "xs = {xs}"
+    trace[Meta.CongrTheorems] "ys = {ys}"
+    trace[Meta.CongrTheorems] "computed fixedParams={fixedParams}"
+    let lctx := (← getLCtx) -- checkpoint for a local context that only has the parameters
+    withLocalDeclD `f fType fun ef => withLocalDeclD `f' fType fun pef' => do
+    let ef' := if fixedFun then ef else pef'
+    withLocalDeclD `e (← mkEq ef ef') fun ee => do
+    withNewEqs xs ys fixedParams fun kinds eqs => do
+      let fParams := if fixedFun then #[ef] else #[ef, ef', ee]
+      let mut hs := fParams     -- parameters to the basic congruence lemma
+      let mut hs' := fParams    -- parameters to the richer congruence lemma
+      let mut vals' := fParams  -- how to calculate the basic parameters from the richer ones
+      for i in [0 : info.getArity] do
+        hs := hs.push xs[i]!
+        hs' := hs'.push xs[i]!
+        vals' := vals'.push xs[i]!
+        if let some (eq, eq', val) := eqs[i]! then
+          -- Not a fixed argument
+          hs := hs.push ys[i]! |>.push eq
+          hs' := hs'.push ys[i]! |>.push eq'
+          vals' := vals'.push ys[i]! |>.push val
+      -- Generate the theorem with respect to the simpler hypotheses
+      let mkConcl := if forceHEq then mkHEq else mkEqHEq
+      let congrType ← mkForallFVars hs (← mkConcl (mkAppN ef xs) (mkAppN ef' ys))
+      trace[Meta.CongrTheorems] "simple congrType: {congrType}"
+      let some proof ← withLCtx lctx (← getLocalInstances) <| trySolve congrType
+        | throwError "Internal error when constructing congruence lemma proof"
+      -- At this point, `mkLambdaFVars hs' (mkAppN proof vals')` is the richer proof.
+      -- We try to precompute some of the arguments using `trySolve`.
+      let mut hs'' := #[] -- eq' parameters that are actually used beyond those in `fParams`
+      let mut pfVars := #[] -- eq' parameters that can be solved for already
+      let mut pfVals := #[] -- the values to use for these parameters
+      let mut kinds' : Array CongrArgKind := #[if fixedFun then .fixed else .eq]
+      for i in [0 : info.getArity] do
+        hs'' := hs''.push xs[i]!
+        if let some (_, eq', _) := eqs[i]! then
+          -- Not a fixed argument
+          hs'' := hs''.push ys[i]!
+          let pf? ← withLCtx lctx (← getLocalInstances) <| trySolve (← inferType eq')
+          if let some pf := pf? then
+            pfVars := pfVars.push eq'
+            pfVals := pfVals.push pf
+            kinds' := kinds'.push .subsingletonInst
+          else
+            hs'' := hs''.push eq'
+            kinds' := kinds'.push kinds[i]!
+        else
+          kinds' := kinds'.push .fixed
+      trace[Meta.CongrTheorems] "CongrArgKinds: {repr kinds'}"
+      -- Take `proof`, abstract the pfVars and provide the solved-for proofs (as an
+      -- optimization for proof term size) then abstract the remaining variables.
+      -- The `usedOnly` probably has no affect.
+      -- Note that since we are doing `proof.beta vals'` there is technically some quadratic
+      -- complexity, but it shouldn't be too bad since they're some applications of just variables.
+      let proof' ← mkLambdaFVars fParams (← mkLambdaFVars (usedOnly := true) hs''
+                    (mkAppN (← mkLambdaFVars pfVars (proof.beta vals')) pfVals))
+      let congrType' ← inferType proof'
+      trace[Meta.CongrTheorems] "rich congrType: {congrType'}"
+      return {proof := proof', type := congrType', argKinds := kinds'}
+where
+  /-- Similar to doing `forallBoundedTelescope` twice, but makes use of the `fixed` array, which
+  is used as a hint for whether both variables should be the same. This is only a hint though,
+  since we respect it only if the binding domains are equal.
+  We affix `'` to the second list of variables, and all the variables are introduced
+  with default binder info. Calls `k` with the xs, ys, and a revised `fixed` array -/
+  doubleTelescope {α} (fty : Expr) (numVars : Nat) (fixed : Array Bool)
+      (k : Array Expr → Array Expr → Array Bool → MetaM α) : MetaM α := do
+    let rec loop (i : Nat)
+        (ftyx ftyy : Expr) (xs ys : Array Expr) (fixed' : Array Bool) : MetaM α := do
+      if i < numVars then
+        let ftyx ← whnf ftyx
+        let ftyy ← whnf ftyy
+        unless ftyx.isForall do
+          throwError "doubleTelescope: function doesn't have enough parameters"
+        withLocalDeclD ftyx.bindingName! ftyx.bindingDomain! fun fvarx => do
+          let ftyx' := ftyx.bindingBody!.instantiate1 fvarx
+          if fixed.getD i false && ftyx.bindingDomain! == ftyy.bindingDomain! then
+            -- Fixed: use the same variable for both
+            let ftyy' := ftyy.bindingBody!.instantiate1 fvarx
+            loop (i + 1) ftyx' ftyy' (xs.push fvarx) (ys.push fvarx) (fixed'.push true)
+          else
+            -- Not fixed: use different variables
+            let yname := ftyy.bindingName!.appendAfter "'"
+            withLocalDeclD yname ftyy.bindingDomain! fun fvary => do
+              let ftyy' := ftyy.bindingBody!.instantiate1 fvary
+              loop (i + 1) ftyx' ftyy' (xs.push fvarx) (ys.push fvary) (fixed'.push false)
+      else
+        k xs ys fixed'
+    loop 0 fty fty #[] #[] #[]
+  /-- Introduce variables for equalities between the arrays of variables. Uses `fixedParams`
+  to control whether to introduce an equality for each pair. The array of triples passed to `k`
+  consists of (1) the simple congr lemma HEq arg, (2) the richer HEq arg, and (3) how to
+  compute 1 in terms of 2. -/
+  withNewEqs {α} (xs ys : Array Expr) (fixedParams : Array Bool)
+      (k : Array CongrArgKind → Array (Option (Expr × Expr × Expr)) → MetaM α) : MetaM α :=
+    let rec loop (i : Nat)
+        (kinds : Array CongrArgKind) (eqs : Array (Option (Expr × Expr × Expr))) := do
+      if i < xs.size then
+        let x := xs[i]!
+        let y := ys[i]!
+        if fixedParams[i]! then
+          loop (i+1) (kinds.push .fixed) (eqs.push none)
+        else
+          let deps := info.paramInfo[i]!.backDeps.filterMap (fun j => eqs[j]!)
+          let eq' ← mkForallFVars (deps.map fun (eq, _, _) => eq) (← mkEqHEq x y)
+          withLocalDeclD ((`e).appendIndexAfter (i+1)) (← mkEqHEq x y) fun h =>
+          withLocalDeclD ((`e').appendIndexAfter (i+1)) eq' fun h' => do
+            let v := mkAppN h' (deps.map fun (_, _, val) => val)
+            let kind := if (← inferType h).eq?.isSome then .eq else .heq
+            loop (i+1) (kinds.push kind) (eqs.push (h, h', v))
+      else
+        k kinds eqs
+    loop 0 #[] #[]
+  /-- Given a type that is a bunch of equalities implying a goal (for example, a basic
+  congruence lemma), prove it if possible. Basic congruence lemmas should be provable by this.
+  There are some extra tricks for handling arguments to richer congruence lemmas. -/
+  trySolveCore (mvarId : MVarId) : MetaM Unit := do
+    -- First cleanup the context since we're going to do `substEqs` and we don't want to
+    -- accidentally use variables not actually used by the theorem.
+    let mvarId ← mvarId.cleanup
+    let (_, mvarId) ← mvarId.intros
+    let mvarId := (← mvarId.substEqs).getD mvarId
+    try mvarId.refl; return catch _ => pure ()
+    try mvarId.hrefl; return catch _ => pure ()
+    if ← mvarId.proofIrrelHeq then return
+    -- Make the goal be an eq and then try `Subsingleton.elim`
+    let mvarId ← mvarId.heqOfEq
+    if ← mvarId.subsingletonElim then return
+    -- We have no more tricks.
+    throwError "was not able to solve for proof"
+  /-- Driver for `trySolveCore`. -/
+  trySolve (ty : Expr) : MetaM (Option Expr) := observing? do
+    let mvar ← mkFreshExprMVar ty
+    trace[Meta.CongrTheorems] "trySolve {mvar.mvarId!}"
+    -- The proofs we generate shouldn't require unfolding anything.
+    withReducible <| trySolveCore mvar.mvarId!
+    trace[Meta.CongrTheorems] "trySolve success!"
+    let pf ← instantiateMVars mvar
+    return pf
+
+end Lean.Meta

src/Lean/Meta/Tactic.lean

@@ -38,3 +38,5 @@ import Lean.Meta.Tactic.Symm
 import Lean.Meta.Tactic.Backtrack
 import Lean.Meta.Tactic.SolveByElim
 import Lean.Meta.Tactic.FunInd
+import Lean.Meta.Tactic.Rfl
+import Lean.Meta.Tactic.Convert

src/Lean/Meta/Tactic/Apply.lean

@@ -193,6 +193,11 @@ def apply (mvarId : MVarId) (e : Expr) (cfg : ApplyConfig := {}) : MetaM (List M
 def _root_.Lean.MVarId.applyConst (mvar : MVarId) (c : Name) (cfg : ApplyConfig := {}) : MetaM (List MVarId) := do
   mvar.apply (← mkConstWithFreshMVarLevels c) cfg
 
+end Meta
+
+open Meta
+namespace MVarId
+
 partial def splitAndCore (mvarId : MVarId) : MetaM (List MVarId) :=
   mvarId.withContext do
     mvarId.checkNotAssigned `splitAnd
@@ -219,14 +224,14 @@ partial def splitAndCore (mvarId : MVarId) : MetaM (List MVarId) :=
 /--
 Apply `And.intro` as much as possible to goal `mvarId`.
 -/
-abbrev _root_.Lean.MVarId.splitAnd (mvarId : MVarId) : MetaM (List MVarId) :=
+abbrev splitAnd (mvarId : MVarId) : MetaM (List MVarId) :=
   splitAndCore mvarId
 
-@[deprecated MVarId.splitAnd]
-def splitAnd (mvarId : MVarId) : MetaM (List MVarId) :=
+@[deprecated splitAnd]
+def _root_.Lean.Meta.splitAnd (mvarId : MVarId) : MetaM (List MVarId) :=
   mvarId.splitAnd
 
-def _root_.Lean.MVarId.exfalso (mvarId : MVarId) : MetaM MVarId :=
+def exfalso (mvarId : MVarId) : MetaM MVarId :=
   mvarId.withContext do
     mvarId.checkNotAssigned `exfalso
     let target ← instantiateMVars (← mvarId.getType)
@@ -240,7 +245,7 @@ Apply the `n`-th constructor of the target type,
 checking that it is an inductive type,
 and that there are the expected number of constructors.
 -/
-def _root_.Lean.MVarId.nthConstructor
+def nthConstructor
     (name : Name) (idx : Nat) (expected? : Option Nat := none) (goal : MVarId) :
     MetaM (List MVarId) := do
   goal.withContext do
@@ -256,4 +261,68 @@ def _root_.Lean.MVarId.nthConstructor
         else
           throwTacticEx name goal s!"index {idx} out of bounds, only {ival.ctors.length} constructors"
 
-end Lean.Meta
+/--
+Try to convert an `Iff` into an `Eq` by applying `iff_of_eq`.
+If successful, returns the new goal, and otherwise returns the original `MVarId`.
+
+This may be regarded as being a special case of `Lean.MVarId.liftReflToEq`, specifically for `Iff`.
+-/
+def iffOfEq (mvarId : MVarId) : MetaM MVarId := do
+  let res ← observing? do
+    let [mvarId] ← mvarId.apply (mkConst ``iff_of_eq []) | failure
+    return mvarId
+  return res.getD mvarId
+
+/--
+Try to convert an `Eq` into an `Iff` by applying `propext`.
+If successful, then returns then new goal, otherwise returns the original `MVarId`.
+-/
+def propext (mvarId : MVarId) : MetaM MVarId := do
+  let res ← observing? do
+    -- Avoid applying `propext` if the target is not an equality of `Prop`s.
+    -- We don't want a unification specializing `Sort*` to `Prop`.
+    let tgt ← withReducible mvarId.getType'
+    let some (ty, _, _) := tgt.eq? | failure
+    guard ty.isProp
+    let [mvarId] ← mvarId.apply (mkConst ``propext []) | failure
+    return mvarId
+  return res.getD mvarId
+
+/--
+Try to close the goal using `proof_irrel_heq`. Returns whether or not it succeeds.
+
+We need to be somewhat careful not to assign metavariables while doing this, otherwise we might
+specialize `Sort _` to `Prop`.
+-/
+def proofIrrelHeq (mvarId : MVarId) : MetaM Bool :=
+  mvarId.withContext do
+    let res ← observing? do
+      mvarId.checkNotAssigned `proofIrrelHeq
+      let tgt ← withReducible mvarId.getType'
+      let some (_, lhs, _, rhs) := tgt.heq? | failure
+      -- Note: `mkAppM` uses `withNewMCtxDepth`, which prevents `Sort _` from specializing to `Prop`
+      let pf ← mkAppM ``proof_irrel_heq #[lhs, rhs]
+      mvarId.assign pf
+      return true
+    return res.getD false
+
+/--
+Try to close the goal using `Subsingleton.elim`. Returns whether or not it succeeds.
+
+We are careful to apply `Subsingleton.elim` in a way that does not assign any metavariables.
+This is to prevent the `Subsingleton Prop` instance from being used as justification to specialize
+`Sort _` to `Prop`.
+-/
+def subsingletonElim (mvarId : MVarId) : MetaM Bool :=
+  mvarId.withContext do
+    let res ← observing? do
+      mvarId.checkNotAssigned `subsingletonElim
+      let tgt ← withReducible mvarId.getType'
+      let some (_, lhs, rhs) := tgt.eq? | failure
+      -- Note: `mkAppM` uses `withNewMCtxDepth`, which prevents `Sort _` from specializing to `Prop`
+      let pf ← mkAppM ``Subsingleton.elim #[lhs, rhs]
+      mvarId.assign pf
+      return true
+    return res.getD false
+
+end Lean.MVarId

src/Lean/Meta/Tactic/Congr!.lean

@@ -0,0 +1,643 @@
+/-
+Copyright (c) 2023 Kyle Miller. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kyle Miller
+-/
+prelude
+import Lean.Elab.Tactic.Config
+import Lean.Elab.Tactic.RCases
+import Lean.Meta.CongrTheorems.Rich
+import Lean.Meta.Tactic.Assumption
+import Lean.Elab.Tactic.Rfl
+
+/-!
+# The `congr!` tactic
+
+This is a more powerful version of the `congr` tactic that knows about more congruence lemmas and
+can apply to more situations. It is similar to the `congr'` tactic from Mathlib 3.
+
+The `congr!` tactic is used by the `convert` and `convert_to` tactics.
+
+See the syntax docstring for more details.
+-/
+
+namespace Lean.Meta.Tactic.Congr!
+
+open Lean Meta Elab Tactic
+
+initialize registerTraceClass `congr!
+initialize registerTraceClass `congr!.synthesize
+
+/-- The configuration for the `congr!` tactic. -/
+structure Config where
+  /-- If `closePre := true`, then try to close goals before applying congruence lemmas
+  using tactics such as `rfl` and `assumption.  These tactics are applied with the
+  transparency level specified by `preTransparency`, which is `.reducible` by default. -/
+  closePre : Bool := true
+  /-- If `closePost := true`, then try to close goals that remain after no more congruence
+  lemmas can be applied, using the same tactics as `closePre`. These tactics are applied
+  with current tactic transparency level. -/
+  closePost : Bool := true
+  /-- The transparency level to use when applying a congruence theorem.
+  By default this is `.reducible`, which prevents unfolding of most definitions. -/
+  transparency : TransparencyMode := TransparencyMode.reducible
+  /-- The transparency level to use when trying to close goals before applying congruence lemmas.
+  This includes trying to prove the goal by `rfl` and using the `assumption` tactic.
+  By default this is `.reducible`, which prevents unfolding of most definitions. -/
+  preTransparency : TransparencyMode := TransparencyMode.reducible
+  /-- For passes that synthesize a congruence lemma using one side of the equality,
+  we run the pass both for the left-hand side and the right-hand side. If `preferLHS` is `true`
+  then we start with the left-hand side.
+
+  This can be used to control which side's definitions are expanded when applying the
+  congruence lemma (if `preferLHS = true` then the RHS can be expanded). -/
+  preferLHS : Bool := true
+  /-- Allow both sides to be partial applications.
+  When false, given an equality `f a b = g x y z` this means we never consider
+  proving `f a = g x y`.
+
+  In this case, we might still consider `f = g x` if a pass generates a congruence lemma using the
+  left-hand side. Use `sameFun := true` to ensure both sides are applications
+  of the same function (making it be similar to the `congr` tactic). -/
+  partialApp : Bool := true
+  /-- Whether to require that both sides of an equality be applications of defeq functions.
+  That is, if true, `f a = g x` is only considered if `f` and `g` are defeq (making it be similar
+  to the `congr` tactic). -/
+  sameFun : Bool := false
+  /-- The maximum number of arguments to consider when doing congruence of function applications.
+  For example, with `f a b c = g w x y z`, setting `maxArgs := some 2` means it will only consider
+  either `f a b = g w x y` and `c = z` or `f a = g w x`, `b = y`, and `c = z`. Setting
+  `maxArgs := none` (the default) means no limit.
+
+  When the functions are dependent, `maxArgs` can prevent congruence from working at all.
+  In `Fintype.card α = Fintype.card β`, one needs to have `maxArgs` at `2` or higher since
+  there is a `Fintype` instance argument that depends on the first.
+
+  When there aren't such dependency issues, setting `maxArgs := some 1` causes `congr!` to
+  do congruence on a single argument at a time. This can be used in conjunction with the
+  iteration limit to control exactly how many arguments are to be processed by congruence. -/
+  maxArgs : Option Nat := none
+  /-- For type arguments that are implicit or have forward dependencies, whether or not `congr!`
+  should generate equalities even if the types do not look plausibly equal.
+
+  We have a heuristic in the main congruence generator that types
+  `α` and `β` are *plausibly equal* according to the following algorithm:
+
+  - If the types are both propositions, they are plausibly equal (`Iff`s are plausible).
+  - If the types are from different universes, they are not plausibly equal.
+  - Suppose in whnf we have `α = f a₁ ... aₘ` and `β = g b₁ ... bₘ`. If `f` is not definitionally
+    equal to `g` or `m ≠ n`, then `α` and `β` are not plausibly equal.
+  - If there is some `i` such that `aᵢ` and `bᵢ` are not plausibly equal, then `α` and `β` are
+    not plausibly equal.
+  - Otherwise, `α` and `β` are plausibly equal.
+
+  The purpose of this is to prevent considering equalities like `ℕ = ℤ` while allowing equalities
+  such as `Fin n = Fin m` or `Subtype p = Subtype q` (so long as these are subtypes of the
+  same type).
+
+  The way this is implemented is that when the congruence generator is comparing arguments when
+  looking at an equality of function applications, it marks a function parameter as "fixed" if the
+  provided arguments are types that are not plausibly equal. The effect of this is that congruence
+  succeeds only if those arguments are defeq at `transparency` transparency. -/
+  typeEqs : Bool := false
+  /-- As a last pass, perform eta expansion of both sides of an equality. For example,
+  this transforms a bare `HAdd.hAdd` into `fun x y => x + y`. -/
+  etaExpand : Bool := false
+  /-- Whether to use the congruence generator that is used by `simp` and `congr`. This generator
+  is more strict, and it does not respect all configuration settings. It does respect
+  `preferLHS`, `partialApp` and `maxArgs` and transparency settings. It acts as if `sameFun := true`
+  and it ignores `typeEqs`. -/
+  useCongrSimp : Bool := false
+
+/-- A configuration option that makes `congr!` do the sorts of aggressive unfoldings that `congr`
+does while also similarly preventing `congr!` from considering partial applications or congruences
+between different functions being applied. -/
+def Config.unfoldSameFun : Congr!.Config where
+  partialApp := false
+  sameFun := true
+  transparency := .default
+  preTransparency := .default
+
+/-- Whether the given number of arguments is allowed to be considered. -/
+def Config.numArgsOk (config : Config) (numArgs : Nat) : Bool :=
+  numArgs ≤ config.maxArgs.getD numArgs
+
+/-- According to the configuration, how many of the arguments in `numArgs` should be considered. -/
+def Config.maxArgsFor (config : Config) (numArgs : Nat) : Nat :=
+  min numArgs (config.maxArgs.getD numArgs)
+
+/--
+Asserts the given congruence theorem as fresh hypothesis, and then applies it.
+Return the `fvarId` for the new hypothesis and the new subgoals.
+
+We apply it with transparency settings specified by `Congr!.Config.transparency`.
+-/
+private def applyCongrThm?
+    (config : Congr!.Config) (mvarId : MVarId) (congrThmType congrThmProof : Expr) :
+    MetaM (List MVarId) := do
+  trace[congr!] "trying to apply congr lemma {congrThmType}"
+  try
+    let mvarId ← mvarId.assert (← mkFreshUserName `h_congr_thm) congrThmType congrThmProof
+    let (fvarId, mvarId) ← mvarId.intro1P
+    let mvarIds ← withTransparency config.transparency <|
+      mvarId.apply (mkFVar fvarId) { synthAssignedInstances := false }
+    mvarIds.mapM fun mvarId => mvarId.tryClear fvarId
+  catch e =>
+    withTraceNode `congr! (fun _ => pure m!"failed to apply congr lemma") do
+      trace[congr!] "{e.toMessageData}"
+    throw e
+
+/-- Returns whether or not it's reasonable to consider an equality between types `ty1` and `ty2`.
+The heuristic is the following:
+
+- If `ty1` and `ty2` are in `Prop`, then yes.
+- If in whnf both `ty1` and `ty2` have the same head and if (recursively) it's reasonable to
+  consider an equality between corresponding type arguments, then yes.
+- Otherwise, no.
+
+This helps keep congr from going too far and generating hypotheses like `ℝ = ℤ`.
+
+To keep things from going out of control, there is a `maxDepth`. Additionally, if we do the check
+with `maxDepth = 0` then the heuristic answers "no". -/
+def Congr!.plausiblyEqualTypes (ty1 ty2 : Expr) (maxDepth : Nat := 5) : MetaM Bool :=
+  match maxDepth with
+  | 0 => return false
+  | maxDepth + 1 => do
+    -- Props are plausibly equal
+    if (← isProp ty1) && (← isProp ty2) then
+      return true
+    -- Types from different type universes are not plausibly equal.
+    -- This is redundant, but it saves carrying out the remaining checks.
+    unless ← withNewMCtxDepth <| isDefEq (← inferType ty1) (← inferType ty2) do
+      return false
+    -- Now put the types into whnf, check they have the same head, and then recurse on arguments
+    let ty1 ← whnfD ty1
+    let ty2 ← whnfD ty2
+    unless ← withNewMCtxDepth <| isDefEq ty1.getAppFn ty2.getAppFn do
+      return false
+    for arg1 in ty1.getAppArgs, arg2 in ty2.getAppArgs do
+      if (← isType arg1) && (← isType arg2) then
+        unless ← plausiblyEqualTypes arg1 arg2 maxDepth do
+          return false
+    return true
+
+/--
+This is like `Lean.MVarId.hcongr?` but (1) looks at both sides when generating the congruence lemma
+and (2) inserts additional hypotheses from equalities from previous arguments.
+
+It uses `Lean.Meta.mkRichHCongr` to generate the congruence lemmas.
+
+If the goal is an `Eq`, it uses `eq_of_heq` first.
+
+As a backup strategy, it uses the LHS/RHS method like in `Lean.MVarId.congrSimp?`
+(where `Congr!.Config.preferLHS` determines which side to try first). This uses a particular side
+of the target, generates the congruence lemma, then tries applying it. This can make progress
+with higher transparency settings. To help the unifier, in this mode it assumes both sides have the
+exact same function.
+-/
+partial
+def _root_.Lean.MVarId.smartHCongr? (config : Congr!.Config) (mvarId : MVarId) :
+    MetaM (Option (List MVarId)) :=
+  mvarId.withContext do
+    mvarId.checkNotAssigned `congr!
+    commitWhenSome? do
+      let mvarId ← mvarId.eqOfHEq
+      let some (_, lhs, _, rhs) := (← withReducible mvarId.getType').heq? | return none
+      if let some mvars ← loop mvarId 0 lhs rhs [] [] then
+        return mvars
+      -- The "correct" behavior failed. However, it's often useful
+      -- to apply congruence lemmas while unfolding definitions, which is what the
+      -- basic `congr` tactic does due to limitations in how congruence lemmas are generated.
+      -- We simulate this behavior here by generating congruence lemmas for the LHS and RHS and
+      -- then applying them.
+      trace[congr!] "Default smartHCongr? failed, trying LHS/RHS method"
+      let (fst, snd) := if config.preferLHS then (lhs, rhs) else (rhs, lhs)
+      if let some mvars ← forSide mvarId fst then
+        return mvars
+      else if let some mvars ← forSide mvarId snd then
+        return mvars
+      else
+        return none
+where
+  loop (mvarId : MVarId) (numArgs : Nat) (lhs rhs : Expr) (lhsArgs rhsArgs : List Expr) :
+      MetaM (Option (List MVarId)) :=
+    match lhs.cleanupAnnotations, rhs.cleanupAnnotations with
+    | .app f a, .app f' b => do
+      if not (config.numArgsOk (numArgs + 1)) then
+        return none
+      let lhsArgs' := a :: lhsArgs
+      let rhsArgs' := b :: rhsArgs
+      -- We try to generate a theorem for the maximal number of arguments
+      if let some mvars ← loop mvarId (numArgs + 1) f f' lhsArgs' rhsArgs' then
+        return mvars
+      -- That failing, we now try for the present number of arguments.
+      if not config.partialApp && f.isApp && f'.isApp then
+        -- It's a partial application on both sides though.
+        return none
+      -- The congruence generator only handles the case where both functions have
+      -- definitionally equal types.
+      unless ← withNewMCtxDepth <| isDefEq (← inferType f) (← inferType f') do
+        return none
+      let funDefEq ← withReducible <| withNewMCtxDepth <| isDefEq f f'
+      if config.sameFun && not funDefEq then
+        return none
+      let info ← getFunInfoNArgs f (numArgs + 1)
+      let mut fixed : Array Bool := #[]
+      for larg in lhsArgs', rarg in rhsArgs', pinfo in info.paramInfo do
+        if !config.typeEqs && (!pinfo.isExplicit || pinfo.hasFwdDeps) then
+          -- When `typeEqs = false` then for non-explicit arguments or
+          -- arguments with forward dependencies, we want type arguments
+          -- to be plausibly equal.
+          if ← isType larg then
+            -- ^ since `f` and `f'` have defeq types, this implies `isType rarg`.
+            unless ← Congr!.plausiblyEqualTypes larg rarg do
+              fixed := fixed.push true
+              continue
+        fixed := fixed.push (← withReducible <| withNewMCtxDepth <| isDefEq larg rarg)
+      let cthm ← mkRichHCongr (forceHEq := true) (← inferType f) info
+                  (fixedFun := funDefEq) (fixedParams := fixed)
+      -- Now see if the congruence theorem actually applies in this situation by applying it!
+      let (congrThm', congrProof') :=
+        if funDefEq then
+          (cthm.type.bindingBody!.instantiate1 f, cthm.proof.beta #[f])
+        else
+          (cthm.type.bindingBody!.bindingBody!.instantiateRev #[f, f'],
+           cthm.proof.beta #[f, f'])
+      observing? <| applyCongrThm? config mvarId congrThm' congrProof'
+    | _, _ => return none
+  forSide (mvarId : MVarId) (side : Expr) : MetaM (Option (List MVarId)) := do
+    let side := side.cleanupAnnotations
+    if not side.isApp then return none
+    let numArgs := config.maxArgsFor side.getAppNumArgs
+    if not config.partialApp && numArgs < side.getAppNumArgs then
+        return none
+    let mut f := side
+    for _ in [:numArgs] do
+      f := f.appFn!'
+    let info ← getFunInfoNArgs f numArgs
+    let mut fixed : Array Bool := #[]
+    if !config.typeEqs then
+      -- We need some strategy for fixed parameters to keep `forSide` from applying
+      -- in cases where `Congr!.possiblyEqualTypes` suggested not to in the previous pass.
+      for pinfo in info.paramInfo, arg in side.getAppArgs do
+        if pinfo.isProp || !(← isType arg) then
+          fixed := fixed.push false
+        else if pinfo.isExplicit && !pinfo.hasFwdDeps then
+          -- It's fine generating equalities for explicit type arguments without forward
+          -- dependencies. Only allowing these is a little strict, because an argument
+          -- might be something like `Fin n`. We might consider being able to generate
+          -- congruence lemmas that only allow equalities where they can plausibly go,
+          -- but that would take looking at a whole application tree.
+          fixed := fixed.push false
+        else
+          fixed := fixed.push true
+    let cthm ← mkRichHCongr (forceHEq := true) (← inferType f) info
+                (fixedFun := true) (fixedParams := fixed)
+    let congrThm' := cthm.type.bindingBody!.instantiate1 f
+    let congrProof' := cthm.proof.beta #[f]
+    observing? <| applyCongrThm? config mvarId congrThm' congrProof'
+
+/--
+Like `Lean.MVarId.congr?` but instead of using only the congruence lemma associated to the LHS,
+it tries the RHS too, in the order specified by `config.preferLHS`.
+
+It uses `Lean.Meta.mkCongrSimp?` to generate a congruence lemma, like in the `congr` tactic.
+
+Applies the congruence generated congruence lemmas according to `config`.
+-/
+def _root_.Lean.MVarId.congrSimp? (config : Congr!.Config) (mvarId : MVarId) :
+    MetaM (Option (List MVarId)) :=
+  mvarId.withContext do
+    unless config.useCongrSimp do return none
+    mvarId.checkNotAssigned `congrSimp?
+    let some (_, lhs, rhs) := (← withReducible mvarId.getType').eq? | return none
+    let (fst, snd) := if config.preferLHS then (lhs, rhs) else (rhs, lhs)
+    if let some mvars ← forSide mvarId fst then
+      return mvars
+    else if let some mvars ← forSide mvarId snd then
+      return mvars
+    else
+      return none
+where
+  forSide (mvarId : MVarId) (side : Expr) : MetaM (Option (List MVarId)) :=
+    commitWhenSome? do
+      let side := side.cleanupAnnotations
+      if not side.isApp then return none
+      let numArgs := config.maxArgsFor side.getAppNumArgs
+      if not config.partialApp && numArgs < side.getAppNumArgs then
+        return none
+      let mut f := side
+      for _ in [:numArgs] do
+        f := f.appFn!'
+      let some congrThm ← mkCongrSimpNArgs f numArgs
+        | return none
+      observing? <| applyCongrThm? config mvarId congrThm.type congrThm.proof
+  /-- Like `mkCongrSimp?` but takes in a specific arity. -/
+  mkCongrSimpNArgs (f : Expr) (nArgs : Nat) : MetaM (Option CongrTheorem) := do
+    let f := (← instantiateMVars f).cleanupAnnotations
+    let info ← getFunInfoNArgs f nArgs
+    mkCongrSimpCore? f info
+      (← getCongrSimpKinds f info) (subsingletonInstImplicitRhs := false)
+
+/--
+Try applying user-provided congruence lemmas. If any are applicable,
+returns a list of new goals.
+
+Tries a congruence lemma associated to the LHS and then, if that failed, the RHS.
+-/
+def _root_.Lean.MVarId.userCongr? (config : Congr!.Config) (mvarId : MVarId) :
+    MetaM (Option (List MVarId)) :=
+  mvarId.withContext do
+    mvarId.checkNotAssigned `userCongr?
+    let some (lhs, rhs) := (← withReducible mvarId.getType').eqOrIff? | return none
+    let (fst, snd) := if config.preferLHS then (lhs, rhs) else (rhs, lhs)
+    if let some mvars ← forSide fst then
+      return mvars
+    else if let some mvars ← forSide snd then
+      return mvars
+    else
+      return none
+where
+  forSide (side : Expr) : MetaM (Option (List MVarId)) := do
+    let side := side.cleanupAnnotations
+    if not side.isApp then return none
+    let some name := side.getAppFn.constName? | return none
+    let congrTheorems := (← getSimpCongrTheorems).get name
+    -- Note: congruence theorems are provided in decreasing order of priority.
+    for congrTheorem in congrTheorems do
+      let res ← observing? do
+        let cinfo ← getConstInfo congrTheorem.theoremName
+        let us ← cinfo.levelParams.mapM fun _ => mkFreshLevelMVar
+        let proof := mkConst congrTheorem.theoremName us
+        let ptype ← instantiateTypeLevelParams cinfo us
+        applyCongrThm? config mvarId ptype proof
+      if let some mvars := res then
+        return mvars
+    return none
+
+/--
+Try to apply `forall_congr`. This is similar to `Lean.MVar.congrImplies?`.
+-/
+def _root_.Lean.MVarId.congrPi? (mvarId : MVarId) : MetaM (Option (List MVarId)) :=
+  observing? do withReducible <| mvarId.apply (← mkConstWithFreshMVarLevels ``forall_congr)
+
+/--
+Try to apply `funext`, but only if it is an equality of two functions where at least one is
+a lambda expression.
+
+One thing this check prevents is accidentally applying `funext` to a set equality, but also when
+doing congruence we don't want to apply `funext` unnecessarily.
+-/
+def _root_.Lean.MVarId.obviousFunext? (mvarId : MVarId) : MetaM (Option (List MVarId)) :=
+  mvarId.withContext <| observing? do
+    let some (_, lhs, rhs) := (← withReducible mvarId.getType').eq? | failure
+    if not lhs.cleanupAnnotations.isLambda && not rhs.cleanupAnnotations.isLambda then failure
+    mvarId.apply (← mkConstWithFreshMVarLevels ``funext)
+
+/--
+Try to apply `hfunext`, returning the new goals if it succeeds.
+Like `Lean.MVarId.obviousFunext?`, we only do so if at least one side of the `HEq` is a lambda.
+This prevents unfolding of things like `Set`.
+
+Need to have `Mathlib.Logic.Function.Basic` imported for this to succeed.
+-/
+def _root_.Lean.MVarId.obviousHfunext? (mvarId : MVarId) : MetaM (Option (List MVarId)) :=
+  mvarId.withContext <| observing? do
+    let some (_, lhs, _, rhs) := (← withReducible mvarId.getType').heq? | failure
+    if not lhs.cleanupAnnotations.isLambda && not rhs.cleanupAnnotations.isLambda then failure
+    mvarId.apply (← mkConstWithFreshMVarLevels ``hfunext)
+
+/-- Like `implies_congr` but provides an additional assumption to the second hypothesis.
+This is a non-dependent version of `pi_congr` that allows the domains to be different. -/
+private theorem implies_congr' {α α' : Sort u} {β β' : Sort v} (h : α = α') (h' : α' → β = β') :
+    (α → β) = (α' → β') := by
+  cases h
+  show (∀ (x : α), (fun _ => β) x) = _
+  rw [funext h']
+
+/-- A version of `Lean.MVarId.congrImplies?` that uses `implies_congr'`
+instead of `implies_congr`. -/
+def _root_.Lean.MVarId.congrImplies?' (mvarId : MVarId) : MetaM (Option (List MVarId)) :=
+  observing? do
+    let [mvarId₁, mvarId₂] ← mvarId.apply (← mkConstWithFreshMVarLevels ``implies_congr')
+      | throwError "unexpected number of goals"
+    return [mvarId₁, mvarId₂]
+
+/--
+Try to apply `Subsingleton.helim` if the goal is a `HEq`. Tries synthesizing a `Subsingleton`
+instance for both the LHS and the RHS.
+
+If successful, this reduces proving `@HEq α x β y` to proving `α = β`.
+-/
+def _root_.Lean.MVarId.subsingletonHelim? (mvarId : MVarId) : MetaM (Option (List MVarId)) :=
+  mvarId.withContext <| observing? do
+    mvarId.checkNotAssigned `subsingletonHelim
+    let some (α, lhs, β, rhs) := (← withReducible mvarId.getType').heq? | failure
+    let eqmvar ← mkFreshExprSyntheticOpaqueMVar (← mkEq α β) (← mvarId.getTag)
+    -- First try synthesizing using the left-hand side for the Subsingleton instance
+    if let some pf ← observing? (mkAppM ``Subsingleton.helim #[eqmvar, lhs, rhs]) then
+      mvarId.assign pf
+      return [eqmvar.mvarId!]
+    let eqsymm ← mkAppM ``Eq.symm #[eqmvar]
+    -- Second try synthesizing using the right-hand side for the Subsingleton instance
+    if let some pf ← observing? (mkAppM ``Subsingleton.helim #[eqsymm, rhs, lhs]) then
+      mvarId.assign (← mkAppM ``HEq.symm #[pf])
+      return [eqmvar.mvarId!]
+    failure
+
+open Lean.MVarId
+
+/--
+A list of all the congruence strategies used by `Lean.MVarId.congrCore!`.
+-/
+def _root_.Lean.MVarId.congrPasses! :
+    List (String × (Congr!.Config → MVarId → MetaM (Option (List MVarId)))) :=
+  [("user congr", userCongr?),
+   ("hcongr lemma", smartHCongr?),
+   ("congr simp lemma", congrSimp?),
+   ("Subsingleton.helim", fun _ => subsingletonHelim?),
+   ("obvious funext", fun _ => obviousFunext?),
+   ("obvious hfunext", fun _ => obviousHfunext?),
+   ("congr_implies", fun _ => congrImplies?'),
+   ("congr_pi", fun _ => congrPi?)]
+
+structure CongrState where
+  /-- Accumulated goals that `congr!` could not handle. -/
+  goals : Array MVarId
+  /-- Patterns to use when doing intro. -/
+  patterns : List (TSyntax `rcasesPat)
+
+abbrev CongrMetaM := StateRefT CongrState MetaM
+
+/-- Pop the next pattern from the current state. -/
+def CongrMetaM.nextPattern : CongrMetaM (Option (TSyntax `rcasesPat)) := do
+  modifyGet fun s =>
+    if let p :: ps := s.patterns then
+      (p, {s with patterns := ps})
+    else
+      (none, s)
+
+private theorem heq_imp_of_eq_imp {p : HEq x y → Prop} (h : (he : x = y) → p (heq_of_eq he))
+    (he : HEq x y) : p he := by
+  cases he
+  exact h rfl
+
+private theorem eq_imp_of_iff_imp {p : x = y → Prop} (h : (he : x ↔ y) → p (propext he))
+    (he : x = y) : p he := by
+  cases he
+  exact h Iff.rfl
+
+/--
+Does `Lean.MVarId.intros` but then cleans up the introduced hypotheses, removing anything
+that is trivial. If there are any patterns in the current `CongrMetaM` state then instead
+of `Lean.MVarId.intros` it does `Std.Tactic.RCases.rintro`.
+
+Cleaning up includes:
+- deleting hypotheses of the form `HEq x x`, `x = x`, and `x ↔ x`.
+- deleting Prop hypotheses that are already in the local context.
+- converting `HEq x y` to `x = y` if possible.
+- converting `x = y` to `x ↔ y` if possible.
+-/
+partial
+def _root_.Lean.MVarId.introsClean (mvarId : MVarId) : CongrMetaM (List MVarId) :=
+  loop mvarId
+where
+  heqImpOfEqImp (mvarId : MVarId) : MetaM (Option MVarId) :=
+    observing? <| withReducible do
+      let [mvarId] ← mvarId.apply (← mkConstWithFreshMVarLevels ``heq_imp_of_eq_imp) | failure
+      return mvarId
+  eqImpOfIffImp (mvarId : MVarId) : MetaM (Option MVarId) :=
+    observing? <| withReducible do
+      let [mvarId] ← mvarId.apply (← mkConstWithFreshMVarLevels ``eq_imp_of_iff_imp) | failure
+      return mvarId
+  loop (mvarId : MVarId) : CongrMetaM (List MVarId) :=
+    mvarId.withContext do
+      let ty ← withReducible <| mvarId.getType'
+      if ty.isForall then
+        let mvarId := (← heqImpOfEqImp mvarId).getD mvarId
+        let mvarId := (← eqImpOfIffImp mvarId).getD mvarId
+        let ty ← withReducible <| mvarId.getType'
+        if ty.isArrow then
+          if ← (isTrivialType ty.bindingDomain!
+                <||> (← getLCtx).anyM (fun decl => do
+                        return (← instantiateMVars decl.type) == ty.bindingDomain!)) then
+            -- Don't intro, clear it
+            let mvar ← mkFreshExprSyntheticOpaqueMVar ty.bindingBody! (← mvarId.getTag)
+            mvarId.assign <| .lam .anonymous ty.bindingDomain! mvar .default
+            return ← loop mvar.mvarId!
+        if let some patt ← CongrMetaM.nextPattern then
+          let gs ← Term.TermElabM.run' <| Lean.Elab.Tactic.RCases.rintro #[patt] none mvarId
+          List.join <$> gs.mapM loop
+        else
+          let (_, mvarId) ← mvarId.intro1
+          loop mvarId
+      else
+        return [mvarId]
+  isTrivialType (ty : Expr) : MetaM Bool := do
+    unless ← Meta.isProp ty do
+      return false
+    let ty ← instantiateMVars ty
+    if let some (lhs, rhs) := ty.eqOrIff? then
+      if lhs.cleanupAnnotations == rhs.cleanupAnnotations then
+        return true
+    if let some (α, lhs, β, rhs) := ty.heq? then
+      if α.cleanupAnnotations == β.cleanupAnnotations
+          && lhs.cleanupAnnotations == rhs.cleanupAnnotations then
+        return true
+    return false
+
+/-- Convert a goal into an `Eq` goal if possible (since we have a better shot at those).
+Also, if `tryClose := true`, then try to close the goal using an assumption, `Subsingleton.Elim`,
+or definitional equality. -/
+def _root_.Lean.MVarId.preCongr! (mvarId : MVarId) (tryClose : Bool) : MetaM (Option MVarId) := do
+  -- Next, turn `HEq` and `Iff` into `Eq`
+  let mvarId ← mvarId.heqOfEq
+  if tryClose then
+    -- This is a good time to check whether we have a relevant hypothesis.
+    if ← mvarId.assumptionCore then return none
+  let mvarId ← mvarId.iffOfEq
+  if tryClose then
+    -- Now try definitional equality. No need to try `mvarId.hrefl` since we already did `heqOfEq`.
+    -- We allow synthetic opaque metavariables to be assigned to fill in `x = _` goals that might
+    -- appear (for example, due to using `convert` with placeholders).
+    try withAssignableSyntheticOpaque mvarId.refl; return none catch _ => pure ()
+    -- Now we go for (heterogenous) equality via subsingleton considerations
+    if ← mvarId.subsingletonElim then return none
+    if ← mvarId.proofIrrelHeq then return none
+  return some mvarId
+
+def _root_.Lean.MVarId.congrCore! (config : Congr!.Config) (mvarId : MVarId) :
+    MetaM (Option (List MVarId)) := do
+  mvarId.checkNotAssigned `congr!
+  let s ← saveState
+  /- We do `liftReflToEq` here rather than in `preCongr!` since we don't want to commit to it
+     if there are no relevant congr lemmas. -/
+  let mvarId ← mvarId.liftReflToEq
+  for (passName, pass) in congrPasses! do
+    try
+      if let some mvarIds ← pass config mvarId then
+        trace[congr!] "pass succeeded: {passName}"
+        return mvarIds
+    catch e =>
+      throwTacticEx `congr! mvarId
+        m!"internal error in congruence pass {passName}, {e.toMessageData}"
+    if ← mvarId.isAssigned then
+      throwTacticEx `congr! mvarId
+        s!"congruence pass {passName} assigned metavariable but failed"
+  restoreState s
+  trace[congr!] "no passes succeeded"
+  return none
+
+/-- A pass to clean up after `Lean.MVarId.preCongr!` and `Lean.MVarId.congrCore!`. -/
+def _root_.Lean.MVarId.postCongr! (config : Congr!.Config) (mvarId : MVarId) : MetaM (Option MVarId) := do
+  let some mvarId ← mvarId.preCongr! config.closePost | return none
+  -- Convert `p = q` to `p ↔ q`, which is likely the more useful form:
+  let mvarId ← mvarId.propext
+  if config.closePost then
+    -- `preCongr` sees `p = q`, but now we've put it back into `p ↔ q` form.
+    if ← mvarId.assumptionCore then return none
+  if config.etaExpand then
+    if let some (_, lhs, rhs) := (← withReducible mvarId.getType').eq? then
+      let lhs' ← Meta.etaExpand lhs
+      let rhs' ← Meta.etaExpand rhs
+      return ← mvarId.change (← mkEq lhs' rhs')
+  return mvarId
+
+/-- A more insistent version of `Lean.MVarId.congrN`.
+See the documentation on the `congr!` syntax.
+
+The `depth?` argument controls the depth of the recursion. If `none`, then it uses a reasonably
+large bound that is linear in the expression depth. -/
+def _root_.Lean.MVarId.congrN! (mvarId : MVarId)
+    (depth? : Option Nat := none) (config : Congr!.Config := {})
+    (patterns : List (TSyntax `rcasesPat) := []) :
+    MetaM (List MVarId) := do
+  let ty ← withReducible <| mvarId.getType'
+  -- A reasonably large yet practically bounded default recursion depth.
+  let defaultDepth := min 1000000 (8 * (1 + ty.approxDepth.toNat))
+  let depth := depth?.getD defaultDepth
+  let (_, s) ← go depth depth mvarId |>.run {goals := #[], patterns := patterns}
+  return s.goals.toList
+where
+  post (mvarId : MVarId) : CongrMetaM Unit := do
+    for mvarId in ← mvarId.introsClean do
+      if let some mvarId ← mvarId.postCongr! config then
+        modify (fun s => {s with goals := s.goals.push mvarId})
+      else
+        trace[congr!] "Dispatched goal by post-processing step."
+  go (depth : Nat) (n : Nat) (mvarId : MVarId) : CongrMetaM Unit := do
+    for mvarId in ← mvarId.introsClean do
+      if let some mvarId ← withTransparency config.preTransparency <|
+                              mvarId.preCongr! config.closePre then
+        match n with
+          | 0 =>
+            trace[congr!] "At level {depth - n}, doing post-processing. {mvarId}"
+            post mvarId
+          | n + 1 =>
+            trace[congr!] "At level {depth - n}, trying congrCore!. {mvarId}"
+            if let some mvarIds ← mvarId.congrCore! config then
+              mvarIds.forM (go depth n)
+            else
+              post mvarId
+
+end Lean.Meta.Tactic.Congr!

src/Lean/Meta/Tactic/Congr.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import Lean.Meta.CongrTheorems
+import Lean.Meta.CongrTheorems.Basic
 import Lean.Meta.Tactic.Assert
 import Lean.Meta.Tactic.Apply
 import Lean.Meta.Tactic.Clear

src/Lean/Meta/Tactic/Convert.lean

@@ -0,0 +1,32 @@
+/-
+Copyright (c) 2022 Scott Morrison. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Scott Morrison
+-/
+import Lean.Meta.Tactic.Congr!
+
+/-!
+# The `convert` tactic.
+-/
+
+open Lean Meta Elab Tactic
+
+/--
+Close the goal `g` using `Eq.mp v e`,
+where `v` is a metavariable asserting that the type of `g` and `e` are equal.
+Then call `MVarId.congrN!` (also using local hypotheses and reflexivity) on `v`,
+and return the resulting goals.
+
+With `sym = true`, reverses the equality in `v`, and uses `Eq.mpr v e` instead.
+With `depth = some n`, calls `MVarId.congrN! n` instead, with `n` as the max recursion depth.
+-/
+def Lean.MVarId.convert (e : Expr) (sym : Bool)
+    (depth : Option Nat := none) (config : Congr!.Config := {})
+    (patterns : List (TSyntax `rcasesPat) := []) (g : MVarId) :
+    MetaM (List MVarId) := do
+  let src ← inferType e
+  let tgt ← g.getType
+  let v ← mkFreshExprMVar (← mkAppM ``Eq (if sym then #[src, tgt] else #[tgt, src]))
+  g.assign (← mkAppM (if sym then ``Eq.mp else ``Eq.mpr) #[v, e])
+  let m := v.mvarId!
+  m.congrN! depth config patterns

src/Lean/Meta/Tactic/NormCast.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Paul-Nicolas Madelaine, Robert Y. Lewis, Mario Carneiro, Gabriel Ebner
 -/
 prelude
-import Lean.Meta.CongrTheorems
+import Lean.Meta.CongrTheorems.Basic
 import Lean.Meta.Tactic.Simp.Attr
 import Lean.Meta.CoeAttr
 

src/Lean/Meta/Tactic/Rfl.lean

@@ -0,0 +1,103 @@
+/-
+Copyright (c) 2022 Newell Jensen. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Newell Jensen, Thomas Murrills
+-/
+prelude
+import Lean.Meta.Tactic.Apply
+import Lean.Elab.Tactic.Basic
+
+/-!
+# `rfl` tactic extension for reflexive relations
+
+This extends the `rfl` tactic so that it works on any reflexive relation,
+provided the reflexivity lemma has been marked as `@[refl]`.
+-/
+
+namespace Lean.Meta.Rfl
+
+open Lean Meta
+
+/-- Discrimation tree settings for the `refl` extension. -/
+def reflExt.config : WhnfCoreConfig := {}
+
+/-- Environment extensions for `refl` lemmas -/
+initialize reflExt :
+    SimpleScopedEnvExtension (Name × Array DiscrTree.Key) (DiscrTree Name) ←
+  registerSimpleScopedEnvExtension {
+    addEntry := fun dt (n, ks) => dt.insertCore ks n
+    initial := {}
+  }
+
+initialize registerBuiltinAttribute {
+  name := `refl
+  descr := "reflexivity relation"
+  add := fun decl _ kind => MetaM.run' do
+    let declTy := (← getConstInfo decl).type
+    let (_, _, targetTy) ← withReducible <| forallMetaTelescopeReducing declTy
+    let fail := throwError
+      "@[refl] attribute only applies to lemmas proving x ∼ x, got {declTy}"
+    let .app (.app rel lhs) rhs := targetTy | fail
+    unless ← withNewMCtxDepth <| isDefEq lhs rhs do fail
+    let key ← DiscrTree.mkPath rel reflExt.config
+    reflExt.add (decl, key) kind
+}
+
+open Elab Tactic
+
+/-- `MetaM` version of the `rfl` tactic.
+
+This tactic applies to a goal whose target has the form `x ~ x`, where `~` is a reflexive
+relation, that is, a relation which has a reflexive lemma tagged with the attribute [refl].
+-/
+def _root_.Lean.MVarId.applyRfl (goal : MVarId) : MetaM Unit := do
+  let .app (.app rel _) _ ← whnfR <|← instantiateMVars <|← goal.getType
+    | throwError "reflexivity lemmas only apply to binary relations, not{
+        indentExpr (← goal.getType)}"
+  let s ← saveState
+  let mut ex? := none
+  for lem in ← (reflExt.getState (← getEnv)).getMatch rel reflExt.config do
+    try
+      let gs ← goal.apply (← mkConstWithFreshMVarLevels lem)
+      if gs.isEmpty then return () else
+        logError <| MessageData.tagged `Tactic.unsolvedGoals <| m!"unsolved goals\n{
+          goalsToMessageData gs}"
+    catch e =>
+      ex? := ex? <|> (some (← saveState, e)) -- stash the first failure of `apply`
+    s.restore
+  if let some (sErr, e) := ex? then
+    sErr.restore
+    throw e
+  else
+    throwError "rfl failed, no lemma with @[refl] applies"
+
+/-- Helper theorem for `Lean.MVarId.liftReflToEq`. -/
+private theorem rel_of_eq_and_refl {α : Sort _} {R : α → α → Prop}
+    {x y : α} (hxy : x = y) (h : R x x) : R x y :=
+  hxy ▸ h
+
+/--
+Convert a goal of the form `x ~ y` into the form `x = y`, where `~` is a reflexive
+relation, that is, a relation which has a reflexive lemma tagged with the attribute `[refl]`.
+If this can't be done, returns the original `MVarId`.
+-/
+def _root_.Lean.MVarId.liftReflToEq (mvarId : MVarId) : MetaM MVarId := do
+  mvarId.checkNotAssigned `liftReflToEq
+  let .app (.app rel _) _ ← withReducible mvarId.getType' | return mvarId
+  if rel.isAppOf `Eq then
+    -- No need to lift Eq to Eq
+    return mvarId
+  for lem in ← (reflExt.getState (← getEnv)).getMatch rel reflExt.config do
+    let res ← observing? do
+      -- First create an equality relating the LHS and RHS
+      -- and reduce the goal to proving that LHS is related to LHS.
+      let [mvarIdEq, mvarIdR] ← mvarId.apply (← mkConstWithFreshMVarLevels ``rel_of_eq_and_refl)
+        | failure
+      -- Then fill in the proof of the latter by reflexivity.
+      let [] ← mvarIdR.apply (← mkConstWithFreshMVarLevels lem) | failure
+      return mvarIdEq
+    if let some mvarIdEq := res then
+      return mvarIdEq
+  return mvarId
+
+end Lean.Meta.Rfl

src/Lean/Meta/Tactic/Simp/Types.lean

@@ -5,7 +5,7 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Lean.Meta.AppBuilder
-import Lean.Meta.CongrTheorems
+import Lean.Meta.CongrTheorems.Basic
 import Lean.Meta.Eqns
 import Lean.Meta.Tactic.Replace
 import Lean.Meta.Tactic.Simp.SimpTheorems

tests/lean/run/congr!.lean

@@ -0,0 +1,261 @@
+-- Everything should be built-in, but we still need this import in order to use `config`.
+-- Moving `Lean.Meta.Tactic.Congr!.Config` to `Init/MetaTypes.lean` and an update-stage0 should hopefully fix this?
+import Lean.Meta.Tactic.Congr!
+
+private axiom test_sorry : ∀ {α}, α
+set_option autoImplicit true
+
+-- Useful for debugging the generated congruence theorems
+set_option trace.Meta.CongrTheorems true
+
+theorem ex1 (a b c : Nat) (h : a = b) : a + c = b + c := by
+  congr!
+
+theorem ex2 (a b : Nat) (h : a = b) : ∀ c, a + c = b + c := by
+  congr!
+
+theorem ex3 (a b : Nat) (h : a = b) : (fun c => a + c) = (fun c => b + c) := by
+  congr!
+
+theorem ex4 (a b : Nat) : Fin (a + b) = Fin (b + a) := by
+  congr! 1
+  guard_target = a + b = b + a
+  apply Nat.add_comm
+
+theorem ex5 : ((a : Nat) → Fin (a + 1)) = ((a : Nat) → Fin (1 + a)) := by
+  congr! 2 with a
+  guard_target = a + 1 = 1 + a
+  apply Nat.add_comm
+
+theorem ex6 : ((a : Nat) × Fin (a + 1)) = ((a : Nat) × Fin (1 + a)) := by
+  congr! 3 with a
+  guard_target = a + 1 = 1 + a
+  apply Nat.add_comm
+
+theorem ex7 (p : Prop) (h1 h2 : p) : h1 = h2 := by
+  congr!
+
+theorem ex8 (p q : Prop) (h1 : p) (h2 : q) : HEq h1 h2 := by
+  congr!
+
+attribute [local refl] Nat.le_refl in
+theorem ex9 (a b : Nat) (h : a = b) : a + 1 ≤ b + 1 := by
+  congr!
+
+theorem ex10 (x y : Unit) : x = y := by
+  congr!
+
+theorem ex11 (p q r : Nat → Prop) (h : q = r) : (∀ n, p n → q n) ↔ (∀ n, p n → r n) := by
+  congr!
+
+theorem ex12 (p q : Prop) (h : p ↔ q) : p = q := by
+  congr!
+
+theorem ex13 (x y : α) (h : x = y) (f : α → Nat) : f x = f y := by
+  congr!
+
+theorem ex14 {α : Type} (f : Nat → Nat) (h : ∀ x, f x = 0) (z : α) (hz : HEq z 0) :
+    HEq f (fun (_ : α) => z) := by
+  congr!
+  · guard_target = Nat = α
+    exact type_eq_of_heq hz.symm
+  next n x _ =>
+    guard_target = HEq (f n) z
+    rw [h]
+    exact hz.symm
+
+theorem ex15 (p q : Nat → Prop) :
+    (∀ ε > 0, p ε) ↔ ∀ ε > 0, q ε := by
+  congr! 2 with ε hε
+  guard_hyp hε : ε > 0
+  guard_target = p ε ↔ q ε
+  exact test_sorry
+
+/- Congruence here is OK since `Fin m = Fin n` is plausible to prove. -/
+example (m n : Nat) (h : m = n) (x : Fin m) (y : Fin n) : HEq (x + x) (y + y) := by
+  congr!
+  guard_target = HEq x y
+  exact test_sorry
+  guard_target = HEq x y
+  exact test_sorry
+
+/- Props are types, but prop equalities are totally plausible. -/
+example (p q r : Prop) : p ∧ q ↔ p ∧ r := by
+  congr!
+  guard_target = q ↔ r
+  exact test_sorry
+
+/- Congruence here is not OK by default since `α = β` is not generally plausible. -/
+example (α β) [inst1 : Add α] [inst2 : Add β] (x : α) (y : β) : HEq (x + x) (y + y) := by
+  congr!
+  guard_target = HEq (x + x) (y + y)
+  -- But with typeEqs we can get it to generate the congruence anyway:
+  have : α = β := test_sorry
+  have : HEq inst1 inst2 := test_sorry
+  congr! (config := { typeEqs := true })
+  guard_target = HEq x y
+  exact test_sorry
+  guard_target = HEq x y
+  exact test_sorry
+
+example (prime : Nat → Prop) (n : Nat) :
+    prime (2 * n + 1) = prime (n + n + 1) := by
+  congr!
+  · guard_target =ₛ (HMul.hMul : Nat → Nat → Nat) = HAdd.hAdd
+    exact test_sorry
+  · guard_target = 2 = n
+    exact test_sorry
+
+example (prime : Nat → Prop) (n : Nat) :
+    prime (2 * n + 1) = prime (n + n + 1) := by
+  congr! (config := {etaExpand := true})
+  · guard_target =ₛ (fun (x y : Nat) => x * y) = (fun (x y : Nat) => x + y)
+    exact test_sorry
+  · guard_target = 2 = n
+    exact test_sorry
+
+example (prime : Nat → Prop) (n : Nat) :
+    prime (2 * n + 1) = prime (n + n + 1) := by
+  congr! 2
+  guard_target = 2 * n = n + n
+  exact test_sorry
+
+example (prime : Nat → Prop) (n : Nat) :
+    prime (2 * n + 1) = prime (n + n + 1) := by
+  congr! (config := .unfoldSameFun)
+  guard_target = 2 * n = n + n
+  exact test_sorry
+
+opaque partiallyApplied (p : Prop) [Decidable p] : Nat → Nat
+
+-- Partially applied dependent functions
+example : partiallyApplied (True ∧ True) = partiallyApplied True := by
+  congr!
+  decide
+
+inductive walk (α : Type) : α → α → Type
+  | nil (n : α) : walk α n n
+
+def walk.map (f : α → β) (w : walk α x y) : walk β (f x) (f y) :=
+  match x, y, w with
+  | _, _, .nil n => .nil (f n)
+
+example (w : walk α x y) (w' : walk α x' y') (f : α → β) : HEq (w.map f) (w'.map f) := by
+  congr!
+  guard_target = x = x'
+  exact test_sorry
+  guard_target = y = y'
+  exact test_sorry
+  -- get x = y and y = y' in context for `HEq w w'` goal.
+  have : x = x' := by assumption
+  have : y = y' := by assumption
+  guard_target = HEq w w'
+  exact test_sorry
+
+example (w : walk α x y) (w' : walk α x' y') (f : α → β) : HEq (w.map f) (w'.map f) := by
+  congr! with rfl rfl
+  guard_target = x = x'
+  exact test_sorry
+  guard_target = y = y'
+  exact test_sorry
+  guard_target = w = w'
+  exact test_sorry
+
+def MySet (α : Type _) := α → Prop
+def MySet.image (f : α → β) (s : MySet α) : MySet β := fun y => ∃ x, s x ∧ f x = y
+
+-- Testing for equality between what are technically partially applied functions
+example (s t : MySet α) (f g : α → β) (h1 : s = t) (h2 : f = g) :
+    MySet.image f s = MySet.image g t := by
+  congr!
+
+
+example (c : Prop → Prop → Prop → Prop) (x x' y z z' : Prop)
+    (h₀ : x ↔ x') (h₁ : z ↔ z') : c x y z ↔ c x' y z' := by
+  congr!
+
+example {α β γ δ} {F : ∀{α β}, (α → β) → γ → δ} {f g : α → β} {s : γ} (h : ∀ (x : α), f x = g x) :
+    F f s = F g s := by
+  congr!
+  funext
+  apply h
+
+example {α β : Type _} {f : _ → β} {x y : {x : {x : α // x = x} // x = x} } (h : x.1 = y.1) :
+    f x = f y := by
+  congr! 1
+  ext1
+  exact h
+
+example {α β : Type _} {F : _ → β} {f g : {f : α → β // f = f} }
+    (h : ∀ x : α, (f : α → β) x = (g : α → β) x) :
+    F f = F g := by
+  congr!
+  ext x
+  apply h
+
+example {ls : List Nat} {f g : Nat → Nat} {h : ∀ x, f x = g x} :
+    ls.map (fun x => f x + 3) = ls.map (fun x => g x + 3) := by
+  congr! 3 with x -- it's a little too powerful and will get to `f = g`
+  exact h x
+
+-- succeed when either `ext` or `congr` can close the goal
+example : () = () := by congr!
+example : 0 = 0 := by congr!
+
+example {α} (a : α) : a = a := by congr!
+
+example {α} (a b : α) (h : false) : a = b := by
+  fail_if_success { congr! }
+  cases h
+
+def g (x : Nat) : Nat := x + 1
+
+example (x y z : Nat) (h : x = z) (hy : y = 2) : 1 + x + y = g z + 2 := by
+  congr!
+  guard_target = HAdd.hAdd 1 = g
+  funext
+  simp [g, Nat.add_comm]
+
+example (Fintype : Type → Type)
+    (α β : Type) (inst : Fintype α) (inst' : Fintype β) : HEq inst inst' := by
+  congr!
+  guard_target = HEq inst inst'
+  exact test_sorry
+
+/- Here, `Fintype` is a subsingleton class so the `HEq` reduces to `Fintype α = Fintype β`.
+Since these are explicit type arguments with no forward dependencies, this reduces to `α = β`.
+Generating a type equality seems like the right thing to do in this context.
+Usually `HEq inst inst'` wouldn't be generated as a subgoal with the default `typeEqs := false`. -/
+example (Fintype : Type → Type) [∀ γ, Subsingleton (Fintype γ)]
+    (α β : Type) (inst : Fintype α) (inst' : Fintype β) : HEq inst inst' := by
+  congr!
+  guard_target = α = β
+  exact test_sorry
+
+example : n = m → 3 + n = m + 3 := by
+  congr! 0 with rfl
+  guard_target = 3 + n = n + 3
+  apply Nat.add_comm
+
+example (x y x' y' : Nat) (hx : x = x') (hy : y = y') : x + y = x' + y' := by
+  congr! (config := { closePre := false, closePost := false })
+  exact hx
+  exact hy
+
+example (x y x' : Nat) (hx : id x = id x') : x + y = x' + y := by
+  congr!
+
+example (x y x' : Nat) (hx : id x = id x') : x + y = x' + y := by
+  congr! (config := { closePost := false })
+  exact hx
+
+example : { f : Nat → Nat // f = id } :=
+  ⟨?_, by
+    -- prevents `rfl` from solving for `?m` in `?m = id`:
+    congr! (config := { closePre := false, closePost := false })
+    ext x
+    exact Nat.zero_add x⟩
+
+-- Regression test. From fixing a "declaration has metavariables" bug
+example (h : z = y) : (x = y ∨ x = z) → x = y := by
+  congr! with (rfl|rfl)

tests/lean/run/convert.lean

@@ -0,0 +1,118 @@
+-- Everything should be built-in, but we still need this import in order to use `config`.
+-- Moving `Lean.Meta.Tactic.Congr!.Config` to `Init/MetaTypes.lean` and an update-stage0 should hopefully fix this?
+import Lean.Meta.Tactic.Congr!
+
+private axiom test_sorry : ∀ {α}, α
+set_option autoImplicit true
+
+namespace Tests
+
+example (P : Prop) (h : P) : P := by convert h
+
+example (α β : Type) (h : α = β) (b : β) : α := by
+  convert b
+
+example (α β : Type) (h : ∀ α β : Type, α = β) (b : β) : α := by
+  convert b
+  apply h
+
+example (m n : Nat) (h : m = n) (b : Fin n) : Nat × Nat × Nat × Fin m := by
+  convert (37, 57, 2, b)
+
+example (α β : Type) (h : α = β) (b : β) : Nat × α := by
+  -- type eq ok since arguments to `Prod` are explicit
+  convert (37, b)
+
+example (α β : Type) (h : β = α) (b : β) : Nat × α := by
+  convert ← (37, b)
+
+example (α β : Type) (h : α = β) (b : β) : Nat × Nat × Nat × α := by
+  convert (37, 57, 2, b)
+
+example (α β : Type) (h : α = β) (b : β) : Nat × Nat × Nat × α := by
+  convert (37, 57, 2, b) using 2
+  guard_target = (Nat × α) = (Nat × β)
+  congr!
+
+section convert_to
+
+class AddCommMonoid (α) extends Add α where
+  add_comm : ∀ x y : α, x + y = y + x
+
+open AddCommMonoid
+
+example {α} [AddCommMonoid α] {a b c d : α} (H : a = c) (H' : b = d) : a + b = d + c := by
+  convert_to c + d = _ using 2
+  rw [add_comm]
+
+example {α} [AddCommMonoid α] {a b c d : α} (H : a = c) (H' : b = d) : a + b = d + c := by
+  convert_to c + d = _ -- defaults to `using 1`
+  congr 2
+  rw [add_comm]
+
+-- Check that `using 1` gives the same behavior as the default.
+example {α} [AddCommMonoid α] {a b c d : α} (H : a = c) (H' : b = d) : a + b = d + c := by
+  convert_to c + d = _ using 1
+  congr 2
+  rw [add_comm]
+
+end convert_to
+
+example (prime : Nat → Prop) (n : Nat) (h : prime (2 * n + 1)) :
+    prime (n + n + 1) := by
+  convert h
+  · guard_target = (HAdd.hAdd : Nat → Nat → Nat) = HMul.hMul
+    exact test_sorry
+  · guard_target = n = 2
+    exact test_sorry
+
+example (prime : Nat → Prop) (n : Nat) (h : prime (2 * n + 1)) :
+    prime (n + n + 1) := by
+  convert (config := .unfoldSameFun) h
+  guard_target = n + n = 2 * n
+  exact test_sorry
+
+example (p q : Nat → Prop) (h : ∀ ε > 0, p ε) :
+    ∀ ε > 0, q ε := by
+  convert h using 2 with ε hε
+  guard_hyp hε : ε > 0
+  guard_target = q ε ↔ p ε
+  exact test_sorry
+
+class Fintype (α : Type _) where
+  card : Nat
+
+axiom Fintype.foo (α : Type _) [Fintype α] : Fintype.card α = 2
+
+axiom Fintype.foo' (α : Type _) [Fintype α] [Fintype (Option α)] : Fintype.card α = 2
+
+axiom instFintypeBool : Fintype Bool
+
+/- Would be "failed to synthesize instance Fintype ?m" without allowing TC failure. -/
+example : @Fintype.card Bool instFintypeBool = 2 := by
+  convert Fintype.foo _
+
+example : @Fintype.card Bool instFintypeBool = 2 := by
+  convert Fintype.foo' _ using 1
+  guard_target = Fintype (Option Bool)
+  exact test_sorry
+
+example : True := by
+  convert_to ?x + ?y = ?z
+  case x => exact 1
+  case y => exact 2
+  case z => exact 3
+  all_goals try infer_instance
+  · simp
+  · simp
+
+example [Fintype α] [Fintype β] : Fintype.card α = Fintype.card β := by
+  congr!
+  guard_target = Fintype.card α = Fintype.card β
+  congr! (config := {typeEqs := true})
+  · guard_target = α = β
+    exact test_sorry
+  · rename_i inst1 inst2 h
+    guard_target = HEq inst1 inst2
+    have : Subsingleton (Fintype α) := test_sorry
+    congr!