From 92affa07e5fbd29d6c360f10e56b2375a1e3816c Mon Sep 17 00:00:00 2001
From: Kyle Miller <kmill31415@gmail.com>
Date: Wed, 1 Mar 2023 22:15:13 +0000
Subject: [PATCH 01/11] Adding Congr! and making convert tactic use it

---
 Mathlib/Tactic/Congr!.lean  | 218 ++++++++++++++++++++++++++++++++++++
 Mathlib/Tactic/Convert.lean |  15 +--
 2 files changed, 226 insertions(+), 7 deletions(-)
 create mode 100644 Mathlib/Tactic/Congr!.lean

diff --git a/Mathlib/Tactic/Congr!.lean b/Mathlib/Tactic/Congr!.lean
new file mode 100644
index 0000000000000..afc7d37609b3a
--- /dev/null
+++ b/Mathlib/Tactic/Congr!.lean
@@ -0,0 +1,218 @@
+/-
+Copyright (c) 2023 Kyle Miller. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kyle Miller
+-/
+import Lean
+import Mathlib.Tactic.Relation.Rfl
+
+/-!
+# The `congr!` tactic
+
+This is a more powerful version of the `congr` tactic.
+-/
+
+open Lean Meta Elab Tactic
+
+/--
+Asserts the given congruence theorem as fresh hypothesis, and then applies it.
+Return the `fvarId` for the new hypothesis and the new subgoals.
+-/
+private def applyCongrThm? (mvarId : MVarId) (congrThmType congrThmProof : Expr) :
+    MetaM (List MVarId) := do
+  let mvarId ← mvarId.assert (← mkFreshUserName `h_congr_thm) congrThmType congrThmProof
+  let (fvarId, mvarId) ← mvarId.intro1P
+  let mvarIds ← mvarId.apply (mkFVar fvarId) { synthAssignedInstances := false }
+  mvarIds.mapM fun mvarId => mvarId.tryClear fvarId
+
+/--
+Try applying user-provided congruence lemmas. If any are applicable,
+returns a list of new goals.
+-/
+def Lean.MVarId.userCongr? (mvarId : MVarId) : MetaM (Option (List MVarId)) :=
+  mvarId.withContext do
+    mvarId.checkNotAssigned `userCongr?
+    let some (lhs, _) := (← mvarId.getType').eqOrIff? | return none
+    let some name := lhs.getAppFn.cleanupAnnotations.constName? | return none
+    let congrTheorems := (← getSimpCongrTheorems).get name
+    -- Note: congruence theorems are in 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? mvarId ptype proof
+      if let some mvars := res then
+        return mvars
+    return none
+
+/--
+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`.
+-/
+def Lean.MVarId.iffOfEq (mvarId : MVarId) : MetaM MVarId :=
+  mvarId.withContext do
+    let some [mvarId] ← observing? do mvarId.apply (mkConst `iff_of_eq []) | return mvarId
+    return 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 Lean.MVarId.propext (mvarId : MVarId) : MetaM MVarId :=
+  mvarId.withContext do
+    let some [mvarId] ← observing? do mvarId.apply (mkConst ``propext []) | return mvarId
+    return mvarId
+
+/-- Helper theorem for `LEan.MVar.liftReflToEq`. -/
+theorem Lean.MVarId.rel_of_eq_and_refl {R : α → α → Prop} (hxy : x = y) (h : R x x) :
+    R x y := hxy ▸ h
+
+/--
+Use a `refl`-tagged lemma to convert the goal into an `Eq`. If this can't be done, returns
+the original `MVarId`.
+-/
+def Lean.MVarId.liftReflToEq (mvarId : MVarId) : MetaM MVarId := do
+  mvarId.checkNotAssigned `liftReflToEq
+  let tgt ← withReducible <| mvarId.getType'
+  let .app (.app rel _) _ := tgt | return mvarId
+  if rel.isAppOf `Eq then
+    -- No need to lift Eq to Eq
+    return mvarId
+  let reflLemmas ← (Mathlib.Tactic.reflExt.getState (← getEnv)).getMatch rel
+  for lem in reflLemmas 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 ``Lean.MVarId.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 mvarId := res then
+      return mvarId
+  return mvarId
+
+/--
+Try to close the goal using `Subsingleton.elim`. Returns whether or not it succeeds.
+-/
+def Lean.MVarId.subsingletonElim (mvarId : MVarId) : MetaM Bool := do
+  let some [] ← observing? do mvarId.apply (mkConst ``Subsingleton.elim [← mkFreshLevelMVar])
+    | return false
+  return true
+
+def Lean.MVarId.proofIrrelHeq (mvarId : MVarId) : MetaM Bool := do
+  let some [] ← observing? do mvarId.apply (mkConst `proof_irrel_heq [])
+    | return false
+  return true
+
+/--
+Try to apply `pi_congr`. This is similar to `Lean.MVar.congrImplies?`.
+-/
+def Lean.MVarId.congrPi? (mvarId : MVarId) : MetaM (Option (List MVarId)) :=
+  observing? do mvarId.apply (← mkConstWithFreshMVarLevels `pi_congr)
+
+/--
+Try to apply `funext`, but only if it is obviously an equality of two functions
+(we do not want this to apply to equalities of sets).
+"Obvious" means that the type of the terms being equated is a pi type.
+-/
+def Lean.MVarId.obviousFunext? (mvarId : MVarId) : MetaM (Option (List MVarId)) :=
+  observing? do
+    let tgt ← mvarId.getType'
+    let some (ty, _, _) := tgt.eq? | failure
+    let .forallE .. ← Lean.instantiateMVars ty | failure
+    mvarId.apply (← mkConstWithFreshMVarLevels ``funext)
+
+/--
+Try to apply `Function.hfunext`, returning the new goals if it succeeds.
+Like `Lean.MVarId.obviousFunext?`, we only do so if both sides of the `HEq` are terms
+of pi types. This is to prevent unfolding of things like `Set`.
+-/
+def Lean.MVarId.obviousHfunext? (mvarId : MVarId) : MetaM (Option (List MVarId)) :=
+  observing? do
+    let tgt ← mvarId.getType'
+    let some (ty1, ty2, _, _) := tgt.heq? | failure
+    let .forallE .. ← Lean.instantiateMVars ty1 | failure
+    let .forallE .. ← Lean.instantiateMVars ty2 | failure
+    mvarId.apply (← mkConstWithFreshMVarLevels `Function.hfunext)
+
+/-- The list of passes used by `Lean.MVarId.congrCore!`. -/
+def Lean.MVarId.congrPasses! : List (MVarId → MetaM (Option (List MVarId))) :=
+  [userCongr?, congr?, hcongr?, obviousFunext?, obviousHfunext?, congrImplies?, congrPi?]
+
+/-- Convert a goal into an `Eq` goal if possible (since we have a better shot at those).
+Also try to dispatch the goal using an assumption, `Subsingleton.Elim`, or definitional equality. -/
+def Lean.MVarId.preCongr! (mvarId : MVarId) : MetaM (Option MVarId) := do
+  -- User congr lemmas might have created additional hypotheses.
+  let (_, mvarId) ← mvarId.intros
+  -- Next, turn `HEq` and `Iff` into `Eq`
+  let mvarId ← mvarId.heqOfEq
+  -- This is a good time to check whether we have a relevant hypothesis.
+  if ← mvarId.assumptionCore then return none
+  let mvarId ← mvarId.iffOfEq
+  -- Now try definitional equality. No need to try `mvarId.hrefl` since we already did  `heqOfEq`.
+  try withReducible 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 Lean.MVarId.congrCore! (mvarId : MVarId) : MetaM (List MVarId) := do
+  /- We do `liftReflToEq` here rather than in `preCongr!` since we don't want it to stick
+     if there are no relevant congr lemmas. -/
+  let mvarId ← mvarId.liftReflToEq
+  for pass in congrPasses! do
+    if let some mvarIds ← pass mvarId then
+      return mvarIds
+  throwTacticEx `congr! mvarId "failed to apply congruence"
+
+/-- A pass to clean up after `Lean.MVarId.preCongr!` and `Lean.MVarId.congrCore!`. -/
+def Lean.MVarId.postCongr! (mvarId : MVarId) : MetaM (Option MVarId) := do
+  let some mvarId ← mvarId.preCongr! | return none
+  -- Convert `p = q` to `p ↔ q`, which is likely the more useful form:
+  let mvarId ← mvarId.propext
+  if ← mvarId.assumptionCore then return none
+  return some mvarId
+
+/-- A more insistent version of `Lean.MVarId.congrN`. -/
+def Lean.MVarId.congrN! (mvarId : MVarId) (depth : Nat := 1000000) : MetaM (List MVarId) := do
+  let (_, s) ← go depth mvarId |>.run #[]
+  return s.toList
+where
+  post (mvarId : MVarId) : StateRefT (Array MVarId) MetaM Unit := do
+    let some mvarId ← mvarId.postCongr! | return
+    modify (·.push mvarId)
+  go (n : Nat) (mvarId : MVarId) : StateRefT (Array MVarId) MetaM Unit := do
+    let some mvarId ← mvarId.preCongr! | return
+    match n with
+      | 0 => post mvarId
+      | n + 1 =>
+        let some mvarIds ← observing? (m := MetaM) mvarId.congrCore!
+          | post mvarId
+        mvarIds.forM (go n)
+
+/--
+Apply congruence (recursively) to goals that have some notion of a left-hand side and a
+right-hand side, for example `⊢ f as = f bs` or `⊢ R (f as) (f bs)` where `R` is a reflexive
+relation. It also applies functional extensionality and propositional extensionality lemmas, as
+well as using `Subsingleton.elim` and `assumption` to dispatch goals.
+
+In general, `congr!` aims be able to break up equalities to navigate into arbitrary subterms.
+Everything `simp` is able to rewrite should be doable using `congr!` and `rw`.
+
+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`.
+-/
+syntax (name := congr!) "congr! " (num)? : tactic
+
+elab_rules : tactic
+| `(tactic| congr! $[$n]?) =>
+  let hugeDepth := 1000000
+  let depth := n.map (·.getNat) |>.getD hugeDepth
+  liftMetaTactic fun g ↦ g.congrN! depth
diff --git a/Mathlib/Tactic/Convert.lean b/Mathlib/Tactic/Convert.lean
index 4355efacdc37b..027db14bcab4f 100644
--- a/Mathlib/Tactic/Convert.lean
+++ b/Mathlib/Tactic/Convert.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
 import Lean
+import Mathlib.Tactic.Congr!
 
 /-!
 # The `convert` tactic.
@@ -14,11 +15,11 @@ 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.congr` (also using local hypotheses and reflexivity) on `v`,
+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` instead, with `n` as the max recursion depth.
+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) (g : MVarId) :
     MetaM (List MVarId) := do
@@ -27,7 +28,7 @@ def Lean.MVarId.convert (e : Expr) (sym : Bool) (depth : Option Nat := none) (g
   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!
-  try m.congrN (depth.getD 1000000)
+  try m.congrN! (depth.getD 1000000)
   catch _ => return [m]
 
 /--
@@ -67,8 +68,8 @@ The syntax `convert ← e` will reverse the direction of the new goals
 
 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
+`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`.
 -/
 syntax (name := convert) "convert " "← "? term (" using " num)? : tactic
@@ -88,8 +89,8 @@ elab_rules : 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`.
+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`.

From f294a37f0457eb4736102f3f74cf0f2e2b4965b7 Mon Sep 17 00:00:00 2001
From: Kyle Miller <kmill31415@gmail.com>
Date: Thu, 2 Mar 2023 00:38:10 +0000
Subject: [PATCH 02/11] some fixes

---
 Mathlib/Algebra/Associated.lean               |  2 +-
 Mathlib/Algebra/BigOperators/Basic.lean       |  1 -
 Mathlib/Algebra/BigOperators/Intervals.lean   |  4 ++--
 Mathlib/Algebra/GroupPower/Lemmas.lean        |  1 -
 .../Algebra/GroupWithZero/Units/Basic.lean    |  3 ---
 Mathlib/Algebra/IndicatorFunction.lean        |  2 +-
 Mathlib/Combinatorics/SimpleGraph/Basic.lean  | 12 ++++------
 .../Combinatorics/SimpleGraph/Coloring.lean   |  2 --
 .../SimpleGraph/Connectivity.lean             |  6 ++---
 Mathlib/Combinatorics/Young/YoungDiagram.lean |  2 +-
 Mathlib/Data/Dfinsupp/Basic.lean              |  4 ++--
 Mathlib/Data/Fin/Tuple/Basic.lean             |  4 +---
 Mathlib/Data/Finset/Basic.lean                |  7 +++---
 Mathlib/Data/Finset/Lattice.lean              |  1 -
 Mathlib/Data/Finset/PiInduction.lean          |  3 +--
 Mathlib/Data/Fintype/Basic.lean               |  4 +---
 Mathlib/Data/Fintype/Option.lean              |  3 +--
 .../Data/Int/ConditionallyCompleteOrder.lean  |  2 --
 Mathlib/Data/Int/Parity.lean                  |  1 -
 Mathlib/Data/List/Sublists.lean               |  2 +-
 Mathlib/Data/ZMod/Defs.lean                   |  2 +-
 Mathlib/Logic/Equiv/Basic.lean                |  3 +--
 Mathlib/MeasureTheory/MeasurableSpace.lean    |  4 ++--
 Mathlib/Order/CompleteLattice.lean            |  2 +-
 Mathlib/Order/Filter/Bases.lean               |  1 -
 Mathlib/Order/PartialSups.lean                |  2 +-
 Mathlib/SetTheory/Ordinal/NaturalOps.lean     |  2 +-
 Mathlib/Tactic/Congr!.lean                    | 23 ++++++++++---------
 Mathlib/Topology/Basic.lean                   |  3 +--
 .../Topology/ContinuousFunction/Basic.lean    |  3 +--
 Mathlib/Topology/ContinuousOn.lean            |  3 +--
 Mathlib/Topology/Homeomorph.lean              |  2 +-
 .../Topology/OmegaCompletePartialOrder.lean   |  1 -
 Mathlib/Topology/Order/Basic.lean             |  6 ++---
 Mathlib/Topology/UniformSpace/Equiv.lean      |  2 +-
 35 files changed, 48 insertions(+), 77 deletions(-)

diff --git a/Mathlib/Algebra/Associated.lean b/Mathlib/Algebra/Associated.lean
index c95eef3094dd4..74bd183a9eee6 100644
--- a/Mathlib/Algebra/Associated.lean
+++ b/Mathlib/Algebra/Associated.lean
@@ -86,7 +86,7 @@ theorem comap_prime (hinv : ∀ a, g (f a : β) = a) (hp : Prime (f p)) : Prime
               simp).imp
           _ _ <;>
       · intro h
-        convert ← map_dvd g h; funext c; rw [hinv, hinv]⟩
+        convert ← map_dvd g h using 2; rw [hinv, hinv]⟩
 #align comap_prime comap_prime
 
 theorem MulEquiv.prime_iff (e : α ≃* β) : Prime p ↔ Prime (e p) :=
diff --git a/Mathlib/Algebra/BigOperators/Basic.lean b/Mathlib/Algebra/BigOperators/Basic.lean
index 403a9604df2a9..a76b3cd14b860 100644
--- a/Mathlib/Algebra/BigOperators/Basic.lean
+++ b/Mathlib/Algebra/BigOperators/Basic.lean
@@ -402,7 +402,6 @@ theorem _root_.Equiv.Perm.prod_comp (σ : Equiv.Perm α) (s : Finset α) (f : α
 theorem _root_.Equiv.Perm.prod_comp' (σ : Equiv.Perm α) (s : Finset α) (f : α → α → β)
     (hs : { a | σ a ≠ a } ⊆ s) : (∏ x in s, f (σ x) x) = ∏ x in s, f x (σ.symm x) := by
   convert σ.prod_comp s (fun x => f x (σ.symm x)) hs
-  ext
   rw [Equiv.symm_apply_apply]
 #align equiv.perm.prod_comp' Equiv.Perm.prod_comp'
 #align equiv.perm.sum_comp' Equiv.Perm.sum_comp'
diff --git a/Mathlib/Algebra/BigOperators/Intervals.lean b/Mathlib/Algebra/BigOperators/Intervals.lean
index bbc4835f1cb6a..bc171a0a1553d 100644
--- a/Mathlib/Algebra/BigOperators/Intervals.lean
+++ b/Mathlib/Algebra/BigOperators/Intervals.lean
@@ -44,8 +44,8 @@ theorem prod_Ico_add' [OrderedCancelAddCommMonoid α] [ExistsAddOfLE α] [Locall
 @[to_additive]
 theorem prod_Ico_add [OrderedCancelAddCommMonoid α] [ExistsAddOfLE α] [LocallyFiniteOrder α]
     (f : α → β) (a b c : α) : (∏ x in Ico a b, f (c + x)) = ∏ x in Ico (a + c) (b + c), f x := by
-  convert prod_Ico_add' f a b c
-  simp_rw [add_comm]
+  convert prod_Ico_add' f a b c using 2
+  rw [add_comm]
 #align finset.prod_Ico_add Finset.prod_Ico_add
 #align finset.sum_Ico_add Finset.sum_Ico_add
 
diff --git a/Mathlib/Algebra/GroupPower/Lemmas.lean b/Mathlib/Algebra/GroupPower/Lemmas.lean
index 1055add514528..c4bf65f026dc2 100644
--- a/Mathlib/Algebra/GroupPower/Lemmas.lean
+++ b/Mathlib/Algebra/GroupPower/Lemmas.lean
@@ -759,7 +759,6 @@ theorem pow_right_injective {x : ℤ} (h : 1 < x.natAbs) :
   suffices Function.Injective (natAbs ∘ ((· ^ ·) x : ℕ → ℤ)) by
     exact Function.Injective.of_comp this
   convert Nat.pow_right_injective h
-  ext n
   rw [Function.comp_apply, natAbs_pow]
 #align int.pow_right_injective Int.pow_right_injective
 
diff --git a/Mathlib/Algebra/GroupWithZero/Units/Basic.lean b/Mathlib/Algebra/GroupWithZero/Units/Basic.lean
index fd91c87d83836..8f34204d671bf 100644
--- a/Mathlib/Algebra/GroupWithZero/Units/Basic.lean
+++ b/Mathlib/Algebra/GroupWithZero/Units/Basic.lean
@@ -167,9 +167,6 @@ theorem isUnit_ring_inverse {a : M₀} : IsUnit (Ring.inverse a) ↔ IsUnit a :=
   ⟨fun h => by
     cases subsingleton_or_nontrivial M₀
     · convert h
-      -- Porting note:
-      -- This is needed due to a regression in `convert` noted in https://github.com/leanprover-community/mathlib4/issues/739
-      exact Subsingleton.elim _ _
     · contrapose h
       rw [Ring.inverse_non_unit _ h]
       exact not_isUnit_zero
diff --git a/Mathlib/Algebra/IndicatorFunction.lean b/Mathlib/Algebra/IndicatorFunction.lean
index 9133957da1f70..7692d3e3801f4 100644
--- a/Mathlib/Algebra/IndicatorFunction.lean
+++ b/Mathlib/Algebra/IndicatorFunction.lean
@@ -252,7 +252,7 @@ theorem mulIndicator_inter_mulSupport (s : Set α) (f : α → M) :
 theorem comp_mulIndicator (h : M → β) (f : α → M) {s : Set α} {x : α} [DecidablePred (· ∈ s)] :
     h (s.mulIndicator f x) = s.piecewise (h ∘ f) (const α (h 1)) x := by
   letI := Classical.decPred (· ∈ s)
-  convert s.apply_piecewise f (const α 1) (fun _ => h) (x := x)
+  convert s.apply_piecewise f (const α 1) (fun _ => h) (x := x) using 2
 #align set.comp_mul_indicator Set.comp_mulIndicator
 #align set.comp_indicator Set.comp_indicator
 
diff --git a/Mathlib/Combinatorics/SimpleGraph/Basic.lean b/Mathlib/Combinatorics/SimpleGraph/Basic.lean
index 2397dd05de4c7..683e52d886a4a 100644
--- a/Mathlib/Combinatorics/SimpleGraph/Basic.lean
+++ b/Mathlib/Combinatorics/SimpleGraph/Basic.lean
@@ -1855,17 +1855,13 @@ def mapEdgeSet : G.edgeSet ≃ G'.edgeSet
   left_inv := by
     rintro ⟨e, h⟩
     simp [Hom.mapEdgeSet, Sym2.map_map, RelEmbedding.toRelHom]
-    apply congr_fun
-    convert Sym2.map_id (α := V)
-    apply congr_arg -- porting note: `convert` tactic did not do enough `congr`
-    exact funext fun _ => RelIso.symm_apply_apply _ _
+    convert congr_fun Sym2.map_id e
+    exact RelIso.symm_apply_apply _ _
   right_inv := by
     rintro ⟨e, h⟩
     simp [Hom.mapEdgeSet, Sym2.map_map, RelEmbedding.toRelHom]
-    apply congr_fun
-    convert Sym2.map_id (α := W)
-    apply congr_arg -- porting note: `convert` tactic did not do enough `congr`
-    exact funext fun _ => RelIso.apply_symm_apply _ _
+    convert congr_fun Sym2.map_id e
+    exact RelIso.apply_symm_apply _ _
 #align simple_graph.iso.map_edge_set SimpleGraph.Iso.mapEdgeSet
 
 /-- A graph isomorphism induces an equivalence of neighbor sets. -/
diff --git a/Mathlib/Combinatorics/SimpleGraph/Coloring.lean b/Mathlib/Combinatorics/SimpleGraph/Coloring.lean
index b3d35213c5f77..e6e56f36714a2 100644
--- a/Mathlib/Combinatorics/SimpleGraph/Coloring.lean
+++ b/Mathlib/Combinatorics/SimpleGraph/Coloring.lean
@@ -118,8 +118,6 @@ theorem Coloring.card_colorClasses_le [Fintype α] [Fintype C.colorClasses] :
   -- porting note: brute force instance declaration `[Fintype (Setoid.classes (Setoid.ker C))]`
   haveI : Fintype (Setoid.classes (Setoid.ker C)) := by assumption
   convert Setoid.card_classes_ker_le C
-  -- porting note: convert would have handled this already in Lean 3:
-  apply Subsingleton.elim
 #align simple_graph.coloring.card_color_classes_le SimpleGraph.Coloring.card_colorClasses_le
 
 theorem Coloring.not_adj_of_mem_colorClass {c : α} {v w : V} (hv : v ∈ C.colorClass c)
diff --git a/Mathlib/Combinatorics/SimpleGraph/Connectivity.lean b/Mathlib/Combinatorics/SimpleGraph/Connectivity.lean
index 23f7a147665d5..e6f04377e8967 100644
--- a/Mathlib/Combinatorics/SimpleGraph/Connectivity.lean
+++ b/Mathlib/Combinatorics/SimpleGraph/Connectivity.lean
@@ -2242,10 +2242,8 @@ theorem coe_finsetWalkLength_eq (n : ℕ) (u v : V) :
     ext p
     simp only [mem_neighborSet, Finset.coe_map, Embedding.coeFn_mk, Set.unionᵢ_coe_set,
       Set.mem_unionᵢ, Set.mem_image, Finset.mem_coe, Set.mem_setOf_eq]
-    -- porting note: using `apply iff_of_eq` to help `congr`
-    apply iff_of_eq; congr with w
-    apply iff_of_eq; congr with h
-    apply iff_of_eq; congr with q
+    congr!
+    rename_i w _ q
     have := Set.ext_iff.mp (ih w v) q
     simp only [Finset.mem_coe, Set.mem_setOf_eq] at this
     rw [← this]
diff --git a/Mathlib/Combinatorics/Young/YoungDiagram.lean b/Mathlib/Combinatorics/Young/YoungDiagram.lean
index 692831728d1bc..e59877f7d4f04 100644
--- a/Mathlib/Combinatorics/Young/YoungDiagram.lean
+++ b/Mathlib/Combinatorics/Young/YoungDiagram.lean
@@ -356,7 +356,7 @@ theorem mk_mem_col_iff {μ : YoungDiagram} {i j : ℕ} : (i, j) ∈ μ.col j ↔
 #align young_diagram.mk_mem_col_iff YoungDiagram.mk_mem_col_iff
 
 protected theorem exists_not_mem_col (μ : YoungDiagram) (j : ℕ) : ∃ i, (i, j) ∉ μ.cells := by
-  convert μ.transpose.exists_not_mem_row j
+  convert μ.transpose.exists_not_mem_row j using 1
   simp
 #align young_diagram.exists_not_mem_col YoungDiagram.exists_not_mem_col
 
diff --git a/Mathlib/Data/Dfinsupp/Basic.lean b/Mathlib/Data/Dfinsupp/Basic.lean
index 4996687fd8553..95596f1a40c9c 100644
--- a/Mathlib/Data/Dfinsupp/Basic.lean
+++ b/Mathlib/Data/Dfinsupp/Basic.lean
@@ -1476,9 +1476,9 @@ theorem sigmaCurry_apply [∀ i j, Zero (δ i j)] (f : Π₀ i : Σi, _, δ i.1
     case h₁ =>
       rw [@mem_image _ _ (fun a b ↦ Classical.propDecidable (a = b))]
       refine' ⟨⟨i, j⟩, _, rfl⟩
-      convert (mem_support_toFun f _).2 h <;> apply Subsingleton.elim
+      convert (mem_support_toFun f _).2 h
     · rw [mem_preimage]
-      convert (mem_support_toFun f _).2 h <;> apply Subsingleton.elim
+      convert (mem_support_toFun f _).2 h
 #align dfinsupp.sigma_curry_apply Dfinsupp.sigmaCurry_apply
 
 @[simp]
diff --git a/Mathlib/Data/Fin/Tuple/Basic.lean b/Mathlib/Data/Fin/Tuple/Basic.lean
index ab440e8d22476..d152e25f1b9fb 100644
--- a/Mathlib/Data/Fin/Tuple/Basic.lean
+++ b/Mathlib/Data/Fin/Tuple/Basic.lean
@@ -164,9 +164,7 @@ theorem consCases_cons {P : (∀ i : Fin n.succ, α i) → Sort v} (h : ∀ x₀
 @[elab_as_elim]
 def consInduction {α : Type _} {P : ∀ {n : ℕ}, (Fin n → α) → Sort v} (h0 : P Fin.elim0)
     (h : ∀ {n} (x₀) (x : Fin n → α), P x → P (Fin.cons x₀ x)) : ∀ {n : ℕ} (x : Fin n → α), P x
-  | 0, x => by
-    convert h0
-    simp
+  | 0, x => by convert h0
   | n + 1, x => consCases (fun x₀ x ↦ h _ _ <| consInduction h0 h _) x
 #align fin.cons_induction Fin.consInductionₓ -- Porting note: universes
 
diff --git a/Mathlib/Data/Finset/Basic.lean b/Mathlib/Data/Finset/Basic.lean
index 1c6ea8e913ae6..dc9c08c46b446 100644
--- a/Mathlib/Data/Finset/Basic.lean
+++ b/Mathlib/Data/Finset/Basic.lean
@@ -2940,11 +2940,10 @@ theorem nonempty_range_succ : (range <| n + 1).Nonempty :=
 #align finset.nonempty_range_succ Finset.nonempty_range_succ
 
 @[simp]
-theorem range_filter_eq {n m : ℕ} : (range n).filter (· = m) = if m < n then {m} else ∅ :=
-  by
-  convert filter_eq (range n) m
+theorem range_filter_eq {n m : ℕ} : (range n).filter (· = m) = if m < n then {m} else ∅ := by
+  convert filter_eq (range n) m using 2
   · ext
-    simp_rw [@eq_comm _ m]
+    rw [eq_comm]
   · simp
 #align finset.range_filter_eq Finset.range_filter_eq
 
diff --git a/Mathlib/Data/Finset/Lattice.lean b/Mathlib/Data/Finset/Lattice.lean
index b2cea7381b019..359d1bf0d95fa 100644
--- a/Mathlib/Data/Finset/Lattice.lean
+++ b/Mathlib/Data/Finset/Lattice.lean
@@ -1451,7 +1451,6 @@ theorem max_erase_ne_self {s : Finset α} : (s.erase x).max ≠ x := by
 theorem min_erase_ne_self {s : Finset α} : (s.erase x).min ≠ x := by
   -- Porting note: old proof `convert @max_erase_ne_self αᵒᵈ _ _ _`
   convert @max_erase_ne_self αᵒᵈ _ (toDual x) (s.map toDual.toEmbedding)
-  · funext _ _; simp only [eq_iff_true_of_subsingleton]
   · ext; simp only [mem_map_equiv]; exact Iff.rfl
 #align finset.min_erase_ne_self Finset.min_erase_ne_self
 
diff --git a/Mathlib/Data/Finset/PiInduction.lean b/Mathlib/Data/Finset/PiInduction.lean
index badcfd89312fe..a6d79df7c36bd 100644
--- a/Mathlib/Data/Finset/PiInduction.lean
+++ b/Mathlib/Data/Finset/PiInduction.lean
@@ -47,7 +47,7 @@ theorem induction_on_pi_of_choice (r : ∀ i, α i → Finset (α i) → Prop)
   cases nonempty_fintype ι
   induction' hs : univ.sigma f using Finset.strongInductionOn with s ihs generalizing f; subst s
   cases' eq_empty_or_nonempty (univ.sigma f) with he hne
-  · convert h0
+  · convert h0 using 1
     simpa [funext_iff] using he
   · rcases sigma_nonempty.1 hne with ⟨i, -, hi⟩
     rcases H_ex i (f i) hi with ⟨x, x_mem, hr⟩
@@ -118,4 +118,3 @@ theorem induction_on_pi_min [∀ i, LinearOrder (α i)] {p : (∀ i, Finset (α
 #align finset.induction_on_pi_min Finset.induction_on_pi_min
 
 end Finset
-
diff --git a/Mathlib/Data/Fintype/Basic.lean b/Mathlib/Data/Fintype/Basic.lean
index c84e711838a9d..ed42f26e104f9 100644
--- a/Mathlib/Data/Fintype/Basic.lean
+++ b/Mathlib/Data/Fintype/Basic.lean
@@ -1048,9 +1048,7 @@ noncomputable def finsetEquivSet [Fintype α] : Finset α ≃ Set α
     where
   toFun := (↑)
   invFun := by classical exact fun s => s.toFinset
-  left_inv s := by
-    { classical convert Finset.toFinset_coe s
-      simp }
+  left_inv s := by convert Finset.toFinset_coe s
   right_inv s := by classical exact s.coe_toFinset
 #align fintype.finset_equiv_set Fintype.finsetEquivSet
 
diff --git a/Mathlib/Data/Fintype/Option.lean b/Mathlib/Data/Fintype/Option.lean
index 15565ee52e9bf..b0b2496a057ba 100644
--- a/Mathlib/Data/Fintype/Option.lean
+++ b/Mathlib/Data/Fintype/Option.lean
@@ -98,12 +98,11 @@ theorem induction_empty_option {P : ∀ (α : Type u) [Fintype α], Prop}
     (h_empty : P PEmpty) (h_option : ∀ (α) [Fintype α], P α → P (Option α)) (α : Type u)
     [h_fintype : Fintype α] : P α := by
   obtain ⟨p⟩ :=
-    let f_empty := (fun i => by convert h_empty; simp)
+    let f_empty := fun i => by convert h_empty
     let h_option : ∀ {α : Type u} [Fintype α] [DecidableEq α],
           (∀ (h : Fintype α), P α) → ∀ (h : Fintype (Option α)), P (Option α)  := by
       rintro α hα - Pα hα'
       convert h_option α (Pα _)
-      simp
     @truncRecEmptyOption (fun α => ∀ h, @P α h) (@fun α β e hα hβ => @of_equiv α β hβ e (hα _))
       f_empty h_option α _ (Classical.decEq α)
   · exact p _
diff --git a/Mathlib/Data/Int/ConditionallyCompleteOrder.lean b/Mathlib/Data/Int/ConditionallyCompleteOrder.lean
index 40ff3f9c32c2f..7840341cfd690 100644
--- a/Mathlib/Data/Int/ConditionallyCompleteOrder.lean
+++ b/Mathlib/Data/Int/ConditionallyCompleteOrder.lean
@@ -68,7 +68,6 @@ theorem csupₛ_eq_greatest_of_bdd {s : Set ℤ} [DecidablePred (· ∈ s)] (b :
   have : s.Nonempty ∧ BddAbove s := ⟨Hinh, b, Hb⟩
   simp only [supₛ, this, and_self, dite_true]
   convert (coe_greatestOfBdd_eq Hb (Classical.choose_spec (⟨b, Hb⟩ : BddAbove s)) Hinh).symm
-  simp
 #align int.cSup_eq_greatest_of_bdd Int.csupₛ_eq_greatest_of_bdd
 
 @[simp]
@@ -86,7 +85,6 @@ theorem cinfₛ_eq_least_of_bdd {s : Set ℤ} [DecidablePred (· ∈ s)] (b : 
   have : s.Nonempty ∧ BddBelow s := ⟨Hinh, b, Hb⟩
   simp only [infₛ, this, and_self, dite_true]
   convert (coe_leastOfBdd_eq Hb (Classical.choose_spec (⟨b, Hb⟩ : BddBelow s)) Hinh).symm
-  simp
 #align int.cInf_eq_least_of_bdd Int.cinfₛ_eq_least_of_bdd
 
 @[simp]
diff --git a/Mathlib/Data/Int/Parity.lean b/Mathlib/Data/Int/Parity.lean
index 3601a4ba91876..89992a0aefcb9 100644
--- a/Mathlib/Data/Int/Parity.lean
+++ b/Mathlib/Data/Int/Parity.lean
@@ -74,7 +74,6 @@ theorem even_or_odd (n : ℤ) : Even n ∨ Odd n :=
 theorem even_or_odd' (n : ℤ) : ∃ k, n = 2 * k ∨ n = 2 * k + 1 := by
   rw [exists_or]
   convert even_or_odd n
-  funext i
   rw [two_mul]
 #align int.even_or_odd' Int.even_or_odd'
 
diff --git a/Mathlib/Data/List/Sublists.lean b/Mathlib/Data/List/Sublists.lean
index 8fb00648feab8..0caf911aac847 100644
--- a/Mathlib/Data/List/Sublists.lean
+++ b/Mathlib/Data/List/Sublists.lean
@@ -397,7 +397,7 @@ alias nodup_sublists' ↔ nodup.of_sublists' nodup.sublists'
 
 theorem nodup_sublistsLen (n : ℕ) {l : List α} (h : Nodup l) : (sublistsLen n l).Nodup := by
   have : Pairwise (. ≠ .) l.sublists' := Pairwise.imp
-    (fun h => Lex.to_ne (by convert h; funext _ _; simp[swap, eq_comm])) h.sublists'
+    (fun h => Lex.to_ne (by convert h using 3; simp [swap, eq_comm])) h.sublists'
   exact this.sublist (sublistsLen_sublist_sublists' _ _)
 
 #align list.nodup_sublists_len List.nodup_sublistsLen
diff --git a/Mathlib/Data/ZMod/Defs.lean b/Mathlib/Data/ZMod/Defs.lean
index 7eff03f4f36b2..4ee1c794b9bb9 100644
--- a/Mathlib/Data/ZMod/Defs.lean
+++ b/Mathlib/Data/ZMod/Defs.lean
@@ -111,7 +111,7 @@ instance infinite : Infinite (ZMod 0) :=
 theorem card (n : ℕ) [Fintype (ZMod n)] : Fintype.card (ZMod n) = n := by
   cases n with
   | zero => exact (not_finite (ZMod 0)).elim
-  | succ n => convert Fintype.card_fin (n + 1); apply Subsingleton.elim
+  | succ n => convert Fintype.card_fin (n + 1)
 #align zmod.card ZMod.card
 
 /- We define each field by cases, to ensure that the eta-expanded `ZMod.commRing` is defeq to the
diff --git a/Mathlib/Logic/Equiv/Basic.lean b/Mathlib/Logic/Equiv/Basic.lean
index e65cd452e0963..a082f899256b5 100644
--- a/Mathlib/Logic/Equiv/Basic.lean
+++ b/Mathlib/Logic/Equiv/Basic.lean
@@ -1102,8 +1102,7 @@ theorem subtypeEquiv_refl {p : α → Prop} (h : ∀ a, p a ↔ p (Equiv.refl _
 theorem subtypeEquiv_symm {p : α → Prop} {q : β → Prop} (e : α ≃ β) (h : ∀ a : α, p a ↔ q (e a)) :
     (e.subtypeEquiv h).symm =
       e.symm.subtypeEquiv fun a => by
-        convert (h <| e.symm a).symm
-        exact (e.apply_symm_apply a).symm :=
+        convert (h <| e.symm a).symm :=
   rfl
 #align equiv.subtype_equiv_symm Equiv.subtypeEquiv_symm
 
diff --git a/Mathlib/MeasureTheory/MeasurableSpace.lean b/Mathlib/MeasureTheory/MeasurableSpace.lean
index c2c3f9fa2fe98..aecf77c0e598d 100644
--- a/Mathlib/MeasureTheory/MeasurableSpace.lean
+++ b/Mathlib/MeasureTheory/MeasurableSpace.lean
@@ -271,8 +271,8 @@ for functions between empty types. -/
 theorem measurable_const' {f : β → α} (hf : ∀ x y, f x = f y) : Measurable f := by
   nontriviality β
   inhabit β
-  convert @measurable_const α β ‹_› ‹_› (f default)
-  exact funext fun x => hf x default
+  convert @measurable_const α β ‹_› ‹_› (f default) using 2
+  apply hf
 #align measurable_const' measurable_const'
 
 theorem measurable_of_countable [Countable α] [MeasurableSingletonClass α] (f : α → β) :
diff --git a/Mathlib/Order/CompleteLattice.lean b/Mathlib/Order/CompleteLattice.lean
index 5e29e5cebdbca..7574d6ba50590 100644
--- a/Mathlib/Order/CompleteLattice.lean
+++ b/Mathlib/Order/CompleteLattice.lean
@@ -664,7 +664,7 @@ theorem Equiv.supᵢ_comp {g : ι' → α} (e : ι ≃ ι') : (⨆ x, g (e x)) =
 protected theorem Function.Surjective.supᵢ_congr {g : ι' → α} (h : ι → ι') (h1 : Surjective h)
     (h2 : ∀ x, g (h x) = f x) : (⨆ x, f x) = ⨆ y, g y := by
   convert h1.supᵢ_comp g
-  exact (funext h2).symm
+  exact (h2 _).symm
 #align function.surjective.supr_congr Function.Surjective.supᵢ_congr
 
 protected theorem Equiv.supᵢ_congr {g : ι' → α} (e : ι ≃ ι') (h : ∀ x, g (e x) = f x) :
diff --git a/Mathlib/Order/Filter/Bases.lean b/Mathlib/Order/Filter/Bases.lean
index f62b9b9ca661e..4075c5509fc7b 100644
--- a/Mathlib/Order/Filter/Bases.lean
+++ b/Mathlib/Order/Filter/Bases.lean
@@ -964,7 +964,6 @@ theorem map_sigma_mk_comap {π : α → Type _} {π' : β → Type _} {f : α 
     map (Sigma.mk a) (comap (g a) l) = comap (Sigma.map f g) (map (Sigma.mk (f a)) l) := by
   refine' (((basis_sets _).comap _).map _).eq_of_same_basis _
   convert ((basis_sets l).map (Sigma.mk (f a))).comap (Sigma.map f g)
-  ext1 s
   apply image_sigmaMk_preimage_sigmaMap hf
 #align filter.map_sigma_mk_comap Filter.map_sigma_mk_comap
 
diff --git a/Mathlib/Order/PartialSups.lean b/Mathlib/Order/PartialSups.lean
index ac3d2bc5cf206..3df1295a2f543 100644
--- a/Mathlib/Order/PartialSups.lean
+++ b/Mathlib/Order/PartialSups.lean
@@ -110,7 +110,7 @@ theorem partialSups_mono : Monotone (partialSups : (ℕ → α) → ℕ →o α)
 -/
 def partialSups.gi : GaloisInsertion (partialSups : (ℕ → α) → ℕ →o α) (↑) where
   choice f h :=
-    ⟨f, by convert (partialSups f).monotone; exact (le_partialSups f).antisymm h⟩
+    ⟨f, by convert (partialSups f).monotone using 1; exact (le_partialSups f).antisymm h⟩
   gc f g := by
     refine' ⟨(le_partialSups f).trans, fun h => _⟩
     convert partialSups_mono h
diff --git a/Mathlib/SetTheory/Ordinal/NaturalOps.lean b/Mathlib/SetTheory/Ordinal/NaturalOps.lean
index 6f7a67e1559dd..23f5ea76da91d 100644
--- a/Mathlib/SetTheory/Ordinal/NaturalOps.lean
+++ b/Mathlib/SetTheory/Ordinal/NaturalOps.lean
@@ -287,7 +287,7 @@ theorem nadd_zero : a ♯ 0 = a := by
   induction' a using Ordinal.induction with a IH
   rw [nadd_def, blsub_zero, max_zero_right]
   convert blsub_id a
-  ext (b hb)
+  rename_i hb
   exact IH _ hb
 #align ordinal.nadd_zero Ordinal.nadd_zero
 
diff --git a/Mathlib/Tactic/Congr!.lean b/Mathlib/Tactic/Congr!.lean
index afc7d37609b3a..b92c9639d7f9b 100644
--- a/Mathlib/Tactic/Congr!.lean
+++ b/Mathlib/Tactic/Congr!.lean
@@ -115,28 +115,29 @@ def Lean.MVarId.congrPi? (mvarId : MVarId) : MetaM (Option (List MVarId)) :=
   observing? do mvarId.apply (← mkConstWithFreshMVarLevels `pi_congr)
 
 /--
-Try to apply `funext`, but only if it is obviously an equality of two functions
-(we do not want this to apply to equalities of sets).
+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.
 "Obvious" means that the type of the terms being equated is a pi type.
 -/
 def Lean.MVarId.obviousFunext? (mvarId : MVarId) : MetaM (Option (List MVarId)) :=
   observing? do
     let tgt ← mvarId.getType'
-    let some (ty, _, _) := tgt.eq? | failure
-    let .forallE .. ← Lean.instantiateMVars ty | failure
+    let some (_, lhs, rhs) := tgt.eq? | failure
+    if not lhs.isLambda && not rhs.isLambda then failure
     mvarId.apply (← mkConstWithFreshMVarLevels ``funext)
 
 /--
 Try to apply `Function.hfunext`, returning the new goals if it succeeds.
-Like `Lean.MVarId.obviousFunext?`, we only do so if both sides of the `HEq` are terms
-of pi types. This is to prevent unfolding of things like `Set`.
+Like `Lean.MVarId.obviousFunext?`, we only do so if at least one side of the `HEq` is a
+lambda. This is to prevent unfolding of things like `Set`.
 -/
 def Lean.MVarId.obviousHfunext? (mvarId : MVarId) : MetaM (Option (List MVarId)) :=
   observing? do
     let tgt ← mvarId.getType'
-    let some (ty1, ty2, _, _) := tgt.heq? | failure
-    let .forallE .. ← Lean.instantiateMVars ty1 | failure
-    let .forallE .. ← Lean.instantiateMVars ty2 | failure
+    let some (_, _, lhs, rhs) := tgt.heq? | failure
+    if not lhs.isLambda && not rhs.isLambda then failure
     mvarId.apply (← mkConstWithFreshMVarLevels `Function.hfunext)
 
 /-- The list of passes used by `Lean.MVarId.congrCore!`. -/
@@ -154,7 +155,7 @@ def Lean.MVarId.preCongr! (mvarId : MVarId) : MetaM (Option MVarId) := do
   if ← mvarId.assumptionCore then return none
   let mvarId ← mvarId.iffOfEq
   -- Now try definitional equality. No need to try `mvarId.hrefl` since we already did  `heqOfEq`.
-  try withReducible mvarId.refl; return none catch _ => pure ()
+  try 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
@@ -186,7 +187,7 @@ where
     let some mvarId ← mvarId.postCongr! | return
     modify (·.push mvarId)
   go (n : Nat) (mvarId : MVarId) : StateRefT (Array MVarId) MetaM Unit := do
-    let some mvarId ← mvarId.preCongr! | return
+    let some mvarId ← withReducible mvarId.preCongr! | return
     match n with
       | 0 => post mvarId
       | n + 1 =>
diff --git a/Mathlib/Topology/Basic.lean b/Mathlib/Topology/Basic.lean
index 1adef3b72f552..fda52a0db4fd5 100644
--- a/Mathlib/Topology/Basic.lean
+++ b/Mathlib/Topology/Basic.lean
@@ -945,8 +945,7 @@ theorem IsOpen.eventually_mem {a : α} {s : Set α} (hs : IsOpen s) (ha : a ∈
 for a variant using open sets around `a` instead. -/
 theorem nhds_basis_opens' (a : α) :
     (𝓝 a).HasBasis (fun s : Set α => s ∈ 𝓝 a ∧ IsOpen s) fun x => x := by
-  convert nhds_basis_opens a
-  ext s
+  convert nhds_basis_opens a using 2
   exact and_congr_left_iff.2 IsOpen.mem_nhds_iff
 #align nhds_basis_opens' nhds_basis_opens'
 
diff --git a/Mathlib/Topology/ContinuousFunction/Basic.lean b/Mathlib/Topology/ContinuousFunction/Basic.lean
index 9317af6db3e2b..a9f2f4be3b631 100644
--- a/Mathlib/Topology/ContinuousFunction/Basic.lean
+++ b/Mathlib/Topology/ContinuousFunction/Basic.lean
@@ -363,8 +363,7 @@ noncomputable def liftCover : C(α, β) := by
   refine' ⟨Set.liftCover S (fun i => φ i) hφ H, continuous_subtype_nhds_cover hS _⟩
   intro i
   convert (φ i).continuous
-  ext x
-  exact Set.liftCover_coe x
+  apply Set.liftCover_coe
 #align continuous_map.lift_cover ContinuousMap.liftCover
 
 variable {S φ hφ hS}
diff --git a/Mathlib/Topology/ContinuousOn.lean b/Mathlib/Topology/ContinuousOn.lean
index df88cb5693201..aa4236f26d05b 100644
--- a/Mathlib/Topology/ContinuousOn.lean
+++ b/Mathlib/Topology/ContinuousOn.lean
@@ -1204,7 +1204,7 @@ theorem IsOpen.ite' {s s' t : Set α} (hs : IsOpen s) (hs' : IsOpen s')
   classical
     simp only [isOpen_iff_continuous_mem, Set.ite] at *
     convert continuous_piecewise (fun x hx => propext (ht x hx)) hs.continuousOn hs'.continuousOn
-    ext x
+    rename_i x
     by_cases hx : x ∈ t <;> simp [hx]
 #align is_open.ite' IsOpen.ite'
 
@@ -1290,4 +1290,3 @@ theorem continuousWithinAt_prod_iff {f : α → β × γ} {s : Set α} {x : α}
       ContinuousWithinAt (Prod.fst ∘ f) s x ∧ ContinuousWithinAt (Prod.snd ∘ f) s x :=
   ⟨fun h => ⟨h.fst, h.snd⟩, fun ⟨h1, h2⟩ => h1.prod h2⟩
 #align continuous_within_at_prod_iff continuousWithinAt_prod_iff
-
diff --git a/Mathlib/Topology/Homeomorph.lean b/Mathlib/Topology/Homeomorph.lean
index d4e2480e895fa..7cf48ecb0e9bf 100644
--- a/Mathlib/Topology/Homeomorph.lean
+++ b/Mathlib/Topology/Homeomorph.lean
@@ -187,7 +187,7 @@ def changeInv (f : α ≃ₜ β) (g : β → α) (hg : Function.RightInverse g f
   { toFun := f
     invFun := g
     left_inv := by convert f.left_inv
-    right_inv := by convert f.right_inv
+    right_inv := by convert f.right_inv using 1
     continuous_toFun := f.continuous
     continuous_invFun := by convert f.symm.continuous }
 #align homeomorph.change_inv Homeomorph.changeInv
diff --git a/Mathlib/Topology/OmegaCompletePartialOrder.lean b/Mathlib/Topology/OmegaCompletePartialOrder.lean
index 9d2c4738c15ed..68ffd89247359 100644
--- a/Mathlib/Topology/OmegaCompletePartialOrder.lean
+++ b/Mathlib/Topology/OmegaCompletePartialOrder.lean
@@ -64,7 +64,6 @@ theorem IsOpen.inter (s t : Set α) : IsOpen α s → IsOpen α t → IsOpen α
 theorem isOpen_unionₛ (s : Set (Set α)) (hs : ∀ t ∈ s, IsOpen α t) : IsOpen α (⋃₀ s) := by
   simp only [IsOpen] at hs⊢
   convert CompleteLattice.supₛ_continuous' (setOf ⁻¹' s) hs
-  ext1
   simp only [supₛ_apply, setOf_bijective.surjective.exists, exists_prop, mem_preimage,
     SetCoe.exists, supᵢ_Prop_eq, mem_setOf_eq, mem_unionₛ]
 #align Scott.is_open_sUnion Scott.isOpen_unionₛ
diff --git a/Mathlib/Topology/Order/Basic.lean b/Mathlib/Topology/Order/Basic.lean
index 64246c7a98a65..ea3d5f3fcc79c 100644
--- a/Mathlib/Topology/Order/Basic.lean
+++ b/Mathlib/Topology/Order/Basic.lean
@@ -1088,7 +1088,7 @@ theorem nhdsWithin_Ici_basis' [TopologicalSpace α] [LinearOrder α] [OrderTopol
 theorem nhdsWithin_Iic_basis' [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a : α}
     (ha : ∃ l, l < a) : (𝓝[≤] a).HasBasis (fun l => l < a) fun l => Ioc l a := by
   convert @nhdsWithin_Ici_basis' αᵒᵈ _ _ _ (toDual a) ha
-  exact funext fun x => (@dual_Ico _ _ _ _).symm
+  exact (@dual_Ico _ _ _ _).symm
 #align nhds_within_Iic_basis' nhdsWithin_Iic_basis'
 
 theorem nhdsWithin_Ici_basis [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [NoMaxOrder α]
@@ -1658,8 +1658,8 @@ theorem nhdsWithin_Iio_basis' {a : α} (h : ∃ b, b < a) : (𝓝[<] a).HasBasis
   ⟨fun _ => mem_nhdsWithin_Iio_iff_exists_Ioo_subset' h⟩
 
 theorem nhdsWithin_Iio_eq_bot_iff {a : α} : 𝓝[<] a = ⊥ ↔ IsBot a ∨ ∃ b, b ⋖ a := by
-    convert nhdsWithin_Ioi_eq_bot_iff (a := OrderDual.toDual a)
-    exact funext <| fun _ => propext ofDual_covby_ofDual_iff
+    convert nhdsWithin_Ioi_eq_bot_iff (a := OrderDual.toDual a) using 4
+    exact ofDual_covby_ofDual_iff
 
 open List in
 /-- The following statements are equivalent:
diff --git a/Mathlib/Topology/UniformSpace/Equiv.lean b/Mathlib/Topology/UniformSpace/Equiv.lean
index b3df76008b37d..b69d8866123f2 100644
--- a/Mathlib/Topology/UniformSpace/Equiv.lean
+++ b/Mathlib/Topology/UniformSpace/Equiv.lean
@@ -201,7 +201,7 @@ def changeInv (f : α ≃ᵤ β) (g : β → α) (hg : Function.RightInverse g f
   { toFun := f
     invFun := g
     left_inv := by convert f.left_inv
-    right_inv := by convert f.right_inv
+    right_inv := by convert f.right_inv using 1
     uniformContinuous_toFun := f.uniformContinuous
     uniformContinuous_invFun := by convert f.symm.uniformContinuous }
 #align uniform_equiv.change_inv UniformEquiv.changeInv

From 6664fd81e89affb1968a7b9cb192925b65dfaaf2 Mon Sep 17 00:00:00 2001
From: Kyle Miller <kmill31415@gmail.com>
Date: Thu, 2 Mar 2023 00:48:01 +0000
Subject: [PATCH 03/11] lint

---
 Mathlib.lean | 1 +
 1 file changed, 1 insertion(+)

diff --git a/Mathlib.lean b/Mathlib.lean
index 9e351f69fa64b..9302c84c6e14d 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -1106,6 +1106,7 @@ import Mathlib.Tactic.Clear!
 import Mathlib.Tactic.ClearExcept
 import Mathlib.Tactic.Clear_
 import Mathlib.Tactic.Coe
+import Mathlib.Tactic.Congr!
 import Mathlib.Tactic.Constructor
 import Mathlib.Tactic.Continuity
 import Mathlib.Tactic.Contrapose

From 10d83753dada5533872ef5cd3a298635298f081f Mon Sep 17 00:00:00 2001
From: Kyle Miller <kmill31415@gmail.com>
Date: Thu, 2 Mar 2023 17:33:14 +0100
Subject: [PATCH 04/11] fix rest of mathlib, augment documentation

---
 Mathlib/Data/Finite/Basic.lean           |  6 +-
 Mathlib/GroupTheory/NoncommPiCoprod.lean |  1 -
 Mathlib/LinearAlgebra/Basis.lean         |  1 -
 Mathlib/Logic/Equiv/Basic.lean           |  7 ++-
 Mathlib/Tactic/Congr!.lean               | 71 +++++++++++++++++-------
 Mathlib/Tactic/Convert.lean              | 16 ++++--
 6 files changed, 69 insertions(+), 33 deletions(-)

diff --git a/Mathlib/Data/Finite/Basic.lean b/Mathlib/Data/Finite/Basic.lean
index d6a6a280f4fb9..6f2ad4792e8e6 100644
--- a/Mathlib/Data/Finite/Basic.lean
+++ b/Mathlib/Data/Finite/Basic.lean
@@ -140,13 +140,15 @@ instance Function.Embedding.finite {α β : Sort _} [Finite β] : Finite (α ↪
   · -- Porting note: infer_instance fails because it applies `Finite.of_fintype` and produces a
     -- "stuck at solving universe constraint" error.
     apply Finite.of_subsingleton
-   
+
   · refine' h.elim fun f => _
     haveI : Finite α := Finite.of_injective _ f.injective
     exact Finite.of_injective _ FunLike.coe_injective
 #align function.embedding.finite Function.Embedding.finite
 
-instance Equiv.finite_right {α β : Sort _} [Finite β] : Finite (α ≃ β) :=
+-- Porting note: we need explicit universe variables since otherwise the `convert` automation
+-- specializes to `β : Prop` due to a `Subsingleton.elim`.
+instance Equiv.finite_right {α : Sort u} {β : Sort v} [Finite β] : Finite (α ≃ β) :=
   Finite.of_injective Equiv.toEmbedding fun e₁ e₂ h => Equiv.ext <| by convert FunLike.congr_fun h
 #align equiv.finite_right Equiv.finite_right
 
diff --git a/Mathlib/GroupTheory/NoncommPiCoprod.lean b/Mathlib/GroupTheory/NoncommPiCoprod.lean
index f552cd75ac3ca..c31b380ba01dd 100644
--- a/Mathlib/GroupTheory/NoncommPiCoprod.lean
+++ b/Mathlib/GroupTheory/NoncommPiCoprod.lean
@@ -124,7 +124,6 @@ def noncommPiCoprod : (∀ i : ι, N i) →* M
       have := @Finset.noncommProd_mul_distrib _ _ _ Finset.univ (fun i => ϕ i (f i))
         (fun i => ϕ i (g i)) ?_ ?_ ?_
       · convert this
-        ext
         exact map_mul _ _ _
       · exact fun i _ j _ hij => hcomm hij _ _
       · exact fun i _ j _ hij => hcomm hij _ _
diff --git a/Mathlib/LinearAlgebra/Basis.lean b/Mathlib/LinearAlgebra/Basis.lean
index 729fae51c49f7..bcda12b4ad59d 100644
--- a/Mathlib/LinearAlgebra/Basis.lean
+++ b/Mathlib/LinearAlgebra/Basis.lean
@@ -825,7 +825,6 @@ theorem eq_bot_of_rank_eq_zero [NoZeroDivisors R] (b : Basis ι R M) (N : Submod
   simp only [Function.const_apply, Fin.default_eq_zero, Submodule.coe_mk, Finset.univ_unique,
     Function.comp_const, Finset.sum_singleton] at sum_eq
   convert (b.smul_eq_zero.mp sum_eq).resolve_right x_ne
-  rwa [Nat.lt_one_iff] at hi
 #align eq_bot_of_rank_eq_zero Basis.eq_bot_of_rank_eq_zero
 
 end NoZeroSMulDivisors
diff --git a/Mathlib/Logic/Equiv/Basic.lean b/Mathlib/Logic/Equiv/Basic.lean
index a082f899256b5..11bfc60eaf165 100644
--- a/Mathlib/Logic/Equiv/Basic.lean
+++ b/Mathlib/Logic/Equiv/Basic.lean
@@ -1098,11 +1098,14 @@ theorem subtypeEquiv_refl {p : α → Prop} (h : ∀ a, p a ↔ p (Equiv.refl _
   rfl
 #align equiv.subtype_equiv_refl Equiv.subtypeEquiv_refl
 
+-- Porting note: without giving explicit universe variables, `convert` specializes `β` to `Prop`.
 @[simp]
-theorem subtypeEquiv_symm {p : α → Prop} {q : β → Prop} (e : α ≃ β) (h : ∀ a : α, p a ↔ q (e a)) :
+theorem subtypeEquiv_symm {α : Sort u} {β : Sort v} {p : α → Prop} {q : β → Prop}
+    (e : α ≃ β) (h : ∀ a : α, p a ↔ q (e a)) :
     (e.subtypeEquiv h).symm =
       e.symm.subtypeEquiv fun a => by
-        convert (h <| e.symm a).symm :=
+        convert (h <| e.symm a).symm
+        exact (e.apply_symm_apply a).symm :=
   rfl
 #align equiv.subtype_equiv_symm Equiv.subtypeEquiv_symm
 
diff --git a/Mathlib/Tactic/Congr!.lean b/Mathlib/Tactic/Congr!.lean
index b92c9639d7f9b..3dbe198f5bd91 100644
--- a/Mathlib/Tactic/Congr!.lean
+++ b/Mathlib/Tactic/Congr!.lean
@@ -51,19 +51,21 @@ def Lean.MVarId.userCongr? (mvarId : MVarId) : MetaM (Option (List MVarId)) :=
 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`.
 -/
-def Lean.MVarId.iffOfEq (mvarId : MVarId) : MetaM MVarId :=
-  mvarId.withContext do
-    let some [mvarId] ← observing? do mvarId.apply (mkConst `iff_of_eq []) | return mvarId
+def Lean.MVarId.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 Lean.MVarId.propext (mvarId : MVarId) : MetaM MVarId :=
-  mvarId.withContext do
-    let some [mvarId] ← observing? do mvarId.apply (mkConst ``propext []) | return mvarId
+def Lean.MVarId.propext (mvarId : MVarId) : MetaM MVarId := do
+  let res ← observing? do
+    let [mvarId] ← mvarId.apply (mkConst `propext []) | failure
     return mvarId
+  return res.getD mvarId
 
 /-- Helper theorem for `LEan.MVar.liftReflToEq`. -/
 theorem Lean.MVarId.rel_of_eq_and_refl {R : α → α → Prop} (hxy : x = y) (h : R x x) :
@@ -99,14 +101,16 @@ def Lean.MVarId.liftReflToEq (mvarId : MVarId) : MetaM MVarId := do
 Try to close the goal using `Subsingleton.elim`. Returns whether or not it succeeds.
 -/
 def Lean.MVarId.subsingletonElim (mvarId : MVarId) : MetaM Bool := do
-  let some [] ← observing? do mvarId.apply (mkConst ``Subsingleton.elim [← mkFreshLevelMVar])
-    | return false
-  return true
+  let res ← observing? do
+    let [] ← mvarId.apply (mkConst ``Subsingleton.elim [← mkFreshLevelMVar]) | failure
+    return true
+  return res.getD false
 
 def Lean.MVarId.proofIrrelHeq (mvarId : MVarId) : MetaM Bool := do
-  let some [] ← observing? do mvarId.apply (mkConst `proof_irrel_heq [])
-    | return false
-  return true
+  let res ← observing? do
+    let [] ← mvarId.apply (mkConst `proof_irrel_heq []) | failure
+    return true
+  return res.getD false
 
 /--
 Try to apply `pi_congr`. This is similar to `Lean.MVar.congrImplies?`.
@@ -122,7 +126,7 @@ doing congruence we don't want to apply `funext` unnecessarily.
 "Obvious" means that the type of the terms being equated is a pi type.
 -/
 def Lean.MVarId.obviousFunext? (mvarId : MVarId) : MetaM (Option (List MVarId)) :=
-  observing? do
+  mvarId.withContext <| observing? do
     let tgt ← mvarId.getType'
     let some (_, lhs, rhs) := tgt.eq? | failure
     if not lhs.isLambda && not rhs.isLambda then failure
@@ -134,7 +138,7 @@ Like `Lean.MVarId.obviousFunext?`, we only do so if at least one side of the `HE
 lambda. This is to prevent unfolding of things like `Set`.
 -/
 def Lean.MVarId.obviousHfunext? (mvarId : MVarId) : MetaM (Option (List MVarId)) :=
-  observing? do
+  mvarId.withContext <| observing? do
     let tgt ← mvarId.getType'
     let some (_, _, lhs, rhs) := tgt.heq? | failure
     if not lhs.isLambda && not rhs.isLambda then failure
@@ -178,7 +182,8 @@ def Lean.MVarId.postCongr! (mvarId : MVarId) : MetaM (Option MVarId) := do
   if ← mvarId.assumptionCore then return none
   return some mvarId
 
-/-- A more insistent version of `Lean.MVarId.congrN`. -/
+/-- A more insistent version of `Lean.MVarId.congrN`.
+See the documentation on the `congr!` syntax. -/
 def Lean.MVarId.congrN! (mvarId : MVarId) (depth : Nat := 1000000) : MetaM (List MVarId) := do
   let (_, s) ← go depth mvarId |>.run #[]
   return s.toList
@@ -196,13 +201,37 @@ where
         mvarIds.forM (go n)
 
 /--
-Apply congruence (recursively) to goals that have some notion of a left-hand side and a
-right-hand side, for example `⊢ f as = f bs` or `⊢ R (f as) (f bs)` where `R` is a reflexive
-relation. It also applies functional extensionality and propositional extensionality lemmas, as
-well as using `Subsingleton.elim` and `assumption` to dispatch goals.
+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`.
+
+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.
+
+- Like `congr`, it makes use of the `Eq` and `HEq` congruence lemma generator internally used
+  by `simp`. Hence, one can equate any two pieces of an expression that is accessible to `simp`.
+
+- It uses `implies_congr` and `pi_congr` to do congruences of pi types.
+
+- Before applying congruences, it will run the `intros` tactic automatically.
+  The introduced variables can be given names using the `rename_i` tactic as needed.
+  This helps when user congruence lemmas are applied, since they often provide
+  additional hypotheses.
+
+- When there is an equality between functions, so long as at least one is obviously a lambda, we
+  apply `funext` or `Function.hfunext`, which allows for congruence of lambda bodies.
 
-In general, `congr!` aims be able to break up equalities to navigate into arbitrary subterms.
-Everything `simp` is able to rewrite should be doable using `congr!` and `rw`.
+In addition, `congr!` tries to dispatch 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.
diff --git a/Mathlib/Tactic/Convert.lean b/Mathlib/Tactic/Convert.lean
index 027db14bcab4f..d01a2f37b7448 100644
--- a/Mathlib/Tactic/Convert.lean
+++ b/Mathlib/Tactic/Convert.lean
@@ -36,7 +36,8 @@ 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. For example, in the proof state
+of `e` and the goal using the same strategies as the `congr!` tactic.
+For example, in the proof state
 
 ```lean
 n : ℕ,
@@ -59,9 +60,8 @@ 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`
 ```
-
-If `x y : t`, and an instance `Subsingleton t` is in scope, then any goals of the form
-`x = y` are solved automatically.
+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).
@@ -69,8 +69,12 @@ The syntax `convert ← e` will reverse the direction of the new goals
 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`.
+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.
 -/
 syntax (name := convert) "convert " "← "? term (" using " num)? : tactic
 

From cdc69bc585d3a3249a793edc320ca4570857edae Mon Sep 17 00:00:00 2001
From: Kyle Miller <kmill31415@gmail.com>
Date: Thu, 2 Mar 2023 17:48:32 +0100
Subject: [PATCH 05/11] more fixes after merge

---
 Mathlib/Topology/Algebra/InfiniteSum/Basic.lean | 9 +++------
 1 file changed, 3 insertions(+), 6 deletions(-)

diff --git a/Mathlib/Topology/Algebra/InfiniteSum/Basic.lean b/Mathlib/Topology/Algebra/InfiniteSum/Basic.lean
index 80eba038d9ad7..ba8a3e5840d45 100644
--- a/Mathlib/Topology/Algebra/InfiniteSum/Basic.lean
+++ b/Mathlib/Topology/Algebra/InfiniteSum/Basic.lean
@@ -95,7 +95,6 @@ theorem hasSum_zero : HasSum (fun _ => 0 : β → α) 0 := by simp [HasSum, tend
 
 theorem hasSum_empty [IsEmpty β] : HasSum f 0 := by
   convert @hasSum_zero α β _ _
-  simp only [eq_iff_true_of_subsingleton]
 #align has_sum_empty hasSum_empty
 
 theorem summable_zero : Summable (fun _ => 0 : β → α) :=
@@ -210,7 +209,6 @@ theorem hasSum_ite_eq (b : β) [DecidablePred (· = b)] (a : α) :
 
 theorem hasSum_pi_single [DecidableEq β] (b : β) (a : α) : HasSum (Pi.single b a) a := by
   convert hasSum_ite_eq b a
-  ext
   simp [Pi.single_apply]
 #align has_sum_pi_single hasSum_pi_single
 
@@ -450,7 +448,7 @@ theorem eq_add_of_hasSum_ite {α β : Type _} [TopologicalSpace α] [AddCommMono
     (hf' : HasSum (fun n => ite (n = b) 0 (f n)) a') : a = a' + f b := by
   refine' (add_zero a).symm.trans (hf.update' b 0 _)
   convert hf'
-  exact funext (update_apply f b 0)
+  apply update_apply
 #align eq_add_of_has_sum_ite eq_add_of_hasSum_ite
 
 end HasSum
@@ -842,7 +840,7 @@ theorem summable_iff_of_summable_sub (hfg : Summable fun b => f b - g b) :
 theorem HasSum.update (hf : HasSum f a₁) (b : β) [DecidableEq β] (a : α) :
     HasSum (update f b a) (a - f b + a₁) := by
   convert (hasSum_ite_eq b (a - f b)).add hf
-  ext b'
+  rename_i b'
   by_cases h : b' = b
   · rw [h, update_same]
     simp [eq_self_iff_true, if_true, sub_add_cancel]
@@ -982,7 +980,7 @@ theorem tendsto_sum_nat_add [T2Space α] (f : ℕ → α) :
     have h₁ : Tendsto (fun _ : ℕ => ∑' i, f i) atTop (𝓝 (∑' i, f i)) := tendsto_const_nhds
     simpa only [h₀, sub_self] using Tendsto.sub h₁ hf.hasSum.tendsto_sum_nat
   · convert tendsto_const_nhds (α := α) (β := ℕ) (a := 0) (f := atTop)
-    ext1 i
+    rename_i i
     rw [← summable_nat_add_iff i] at hf
     exact tsum_eq_zero_of_not_summable hf
 #align tendsto_sum_nat_add tendsto_sum_nat_add
@@ -1136,7 +1134,6 @@ theorem tendsto_tsum_compl_atTop_zero (f : β → α) :
     intro i _ j _ hij
     exact Subtype.ext hij
   · convert tendsto_const_nhds (α := α) (β := Finset β) (f := atTop) (a := 0)
-    ext s
     apply tsum_eq_zero_of_not_summable
     rwa [Finset.summable_compl_iff]
 #align tendsto_tsum_compl_at_top_zero tendsto_tsum_compl_atTop_zero

From 903214cce35fc5d0e86119c30f735e5c23ac5e26 Mon Sep 17 00:00:00 2001
From: Kyle Miller <kmill31415@gmail.com>
Date: Thu, 2 Mar 2023 19:00:14 +0100
Subject: [PATCH 06/11] fix test (different accounting in `using`)

---
 test/convert.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/test/convert.lean b/test/convert.lean
index 561ed77a9eb50..7565f67a2f016 100644
--- a/test/convert.lean
+++ b/test/convert.lean
@@ -55,7 +55,7 @@ example {α} [AddCommMonoid α] {a b c d : α} (H : a = c) (H' : b = d) : a + b
   rw [add_comm]
 
 example {α} [AddCommMonoid α] {a b c d : α} (H : a = c) (H' : b = d) : a + b = d + c := by
-  convert_to c + d = _ using 0
+  convert_to c + d = _ using 1
   congr 2
   rw [add_comm]
 

From 21a02962da095944518585753f83b4de8dcc68c6 Mon Sep 17 00:00:00 2001
From: Kyle Miller <kmill31415@gmail.com>
Date: Thu, 2 Mar 2023 21:13:56 +0100
Subject: [PATCH 07/11] docs, maybe a fix for the Subsingleton issue

---
 Mathlib/Tactic/Congr!.lean | 33 ++++++++++++++++++++------
 test/congr.lean            | 47 ++++++++++++++++++++++++++++++++++++++
 2 files changed, 73 insertions(+), 7 deletions(-)
 create mode 100644 test/congr.lean

diff --git a/Mathlib/Tactic/Congr!.lean b/Mathlib/Tactic/Congr!.lean
index 3dbe198f5bd91..37f6f8b3885b3 100644
--- a/Mathlib/Tactic/Congr!.lean
+++ b/Mathlib/Tactic/Congr!.lean
@@ -9,7 +9,12 @@ import Mathlib.Tactic.Relation.Rfl
 /-!
 # The `congr!` tactic
 
-This is a more powerful version of 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 Meta Elab Tactic
@@ -50,6 +55,8 @@ def Lean.MVarId.userCongr? (mvarId : MVarId) : MetaM (Option (List MVarId)) :=
 /--
 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 Lean.MVarId.iffOfEq (mvarId : MVarId) : MetaM MVarId := do
   let res ← observing? do
@@ -99,13 +106,25 @@ def Lean.MVarId.liftReflToEq (mvarId : MVarId) : MetaM MVarId := do
 
 /--
 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 Lean.MVarId.subsingletonElim (mvarId : MVarId) : MetaM Bool := do
-  let res ← observing? do
-    let [] ← mvarId.apply (mkConst ``Subsingleton.elim [← mkFreshLevelMVar]) | failure
-    return true
-  return res.getD false
+def Lean.MVarId.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
+      let pf ← withNewMCtxDepth <| mkAppM ``Subsingleton.elim #[lhs, rhs]
+      mvarId.assign pf
+      return true
+    return res.getD false
 
+/--
+Try to close the goal with using `proof_irrel_heq`. Returns whether or not it succeeds.
+-/
 def Lean.MVarId.proofIrrelHeq (mvarId : MVarId) : MetaM Bool := do
   let res ← observing? do
     let [] ← mvarId.apply (mkConst `proof_irrel_heq []) | failure
@@ -121,9 +140,9 @@ def Lean.MVarId.congrPi? (mvarId : MVarId) : MetaM (Option (List MVarId)) :=
 /--
 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.
-"Obvious" means that the type of the terms being equated is a pi type.
 -/
 def Lean.MVarId.obviousFunext? (mvarId : MVarId) : MetaM (Option (List MVarId)) :=
   mvarId.withContext <| observing? do
diff --git a/test/congr.lean b/test/congr.lean
new file mode 100644
index 0000000000000..af75411edb217
--- /dev/null
+++ b/test/congr.lean
@@ -0,0 +1,47 @@
+import Mathlib.Tactic.Congr!
+import Std.Tactic.GuardExpr
+import Mathlib.Algebra.Group.Basic
+
+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
+  rename_i 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
+  rename_i 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!
+
+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!
+  rename_i n
+  guard_target = q n ↔ r n -- it won't use h itself
+  rw [h]

From 3f3b4fa33abbe21e36c317c9ba070b3fa8897168 Mon Sep 17 00:00:00 2001
From: Kyle Miller <kmill31415@gmail.com>
Date: Thu, 2 Mar 2023 21:26:15 +0100
Subject: [PATCH 08/11] revert impact of Subsingleton regression

---
 Mathlib/Data/Finite/Basic.lean | 4 +---
 Mathlib/Logic/Equiv/Basic.lean | 4 +---
 2 files changed, 2 insertions(+), 6 deletions(-)

diff --git a/Mathlib/Data/Finite/Basic.lean b/Mathlib/Data/Finite/Basic.lean
index 6f2ad4792e8e6..724b9ff1261c5 100644
--- a/Mathlib/Data/Finite/Basic.lean
+++ b/Mathlib/Data/Finite/Basic.lean
@@ -146,9 +146,7 @@ instance Function.Embedding.finite {α β : Sort _} [Finite β] : Finite (α ↪
     exact Finite.of_injective _ FunLike.coe_injective
 #align function.embedding.finite Function.Embedding.finite
 
--- Porting note: we need explicit universe variables since otherwise the `convert` automation
--- specializes to `β : Prop` due to a `Subsingleton.elim`.
-instance Equiv.finite_right {α : Sort u} {β : Sort v} [Finite β] : Finite (α ≃ β) :=
+instance Equiv.finite_right {α β : Sort _} [Finite β] : Finite (α ≃ β) :=
   Finite.of_injective Equiv.toEmbedding fun e₁ e₂ h => Equiv.ext <| by convert FunLike.congr_fun h
 #align equiv.finite_right Equiv.finite_right
 
diff --git a/Mathlib/Logic/Equiv/Basic.lean b/Mathlib/Logic/Equiv/Basic.lean
index 11bfc60eaf165..e65cd452e0963 100644
--- a/Mathlib/Logic/Equiv/Basic.lean
+++ b/Mathlib/Logic/Equiv/Basic.lean
@@ -1098,10 +1098,8 @@ theorem subtypeEquiv_refl {p : α → Prop} (h : ∀ a, p a ↔ p (Equiv.refl _
   rfl
 #align equiv.subtype_equiv_refl Equiv.subtypeEquiv_refl
 
--- Porting note: without giving explicit universe variables, `convert` specializes `β` to `Prop`.
 @[simp]
-theorem subtypeEquiv_symm {α : Sort u} {β : Sort v} {p : α → Prop} {q : β → Prop}
-    (e : α ≃ β) (h : ∀ a : α, p a ↔ q (e a)) :
+theorem subtypeEquiv_symm {p : α → Prop} {q : β → Prop} (e : α ≃ β) (h : ∀ a : α, p a ↔ q (e a)) :
     (e.subtypeEquiv h).symm =
       e.symm.subtypeEquiv fun a => by
         convert (h <| e.symm a).symm

From f95400cbe5a1ce68378bbc30119bfacb074a312c Mon Sep 17 00:00:00 2001
From: Kyle Miller <kmill31415@gmail.com>
Date: Thu, 2 Mar 2023 21:28:06 +0100
Subject: [PATCH 09/11] remove unnecessary withNewMCtxDepth

---
 Mathlib/Tactic/Congr!.lean | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/Mathlib/Tactic/Congr!.lean b/Mathlib/Tactic/Congr!.lean
index 37f6f8b3885b3..4c721c249fb0a 100644
--- a/Mathlib/Tactic/Congr!.lean
+++ b/Mathlib/Tactic/Congr!.lean
@@ -117,7 +117,8 @@ def Lean.MVarId.subsingletonElim (mvarId : MVarId) : MetaM Bool :=
       mvarId.checkNotAssigned `subsingletonElim
       let tgt ← withReducible <| mvarId.getType'
       let some (_, lhs, rhs) := tgt.eq? | failure
-      let pf ← withNewMCtxDepth <| mkAppM ``Subsingleton.elim #[lhs, rhs]
+      -- Note: `mkAppM` uses `withNewMCtxDepth`, which we depend on.
+      let pf ← mkAppM ``Subsingleton.elim #[lhs, rhs]
       mvarId.assign pf
       return true
     return res.getD false

From 673430bc100c78d9ac18341ed5067bfcefe38bde Mon Sep 17 00:00:00 2001
From: Kyle Miller <kmill31415@gmail.com>
Date: Thu, 2 Mar 2023 21:50:17 +0100
Subject: [PATCH 10/11] fix unification bugs

---
 Mathlib/Tactic/Congr!.lean | 30 ++++++++++++++++++++++--------
 test/congr.lean            |  6 ++++++
 2 files changed, 28 insertions(+), 8 deletions(-)

diff --git a/Mathlib/Tactic/Congr!.lean b/Mathlib/Tactic/Congr!.lean
index 4c721c249fb0a..f45e77e214f7a 100644
--- a/Mathlib/Tactic/Congr!.lean
+++ b/Mathlib/Tactic/Congr!.lean
@@ -70,7 +70,12 @@ If successful, then returns then new goal, otherwise returns the original `MVarI
 -/
 def Lean.MVarId.propext (mvarId : MVarId) : MetaM MVarId := do
   let res ← observing? do
-    let [mvarId] ← mvarId.apply (mkConst `propext []) | failure
+    -- 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
 
@@ -112,12 +117,12 @@ This is to prevent the `Subsingleton Prop` instance from being used as justifica
 `Sort _` to `Prop`.
 -/
 def Lean.MVarId.subsingletonElim (mvarId : MVarId) : MetaM Bool :=
-  mvarId.withContext <| do
+  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 we depend on.
+      -- Note: `mkAppM` uses `withNewMCtxDepth`, which we depend on to avoid unification.
       let pf ← mkAppM ``Subsingleton.elim #[lhs, rhs]
       mvarId.assign pf
       return true
@@ -125,12 +130,21 @@ def Lean.MVarId.subsingletonElim (mvarId : MVarId) : MetaM Bool :=
 
 /--
 Try to close the goal with 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 Lean.MVarId.proofIrrelHeq (mvarId : MVarId) : MetaM Bool := do
-  let res ← observing? do
-    let [] ← mvarId.apply (mkConst `proof_irrel_heq []) | failure
-    return true
-  return res.getD false
+def Lean.MVarId.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 we depend on to avoid unification.
+      let pf ← mkAppM `proof_irrel_heq #[lhs, rhs]
+      mvarId.assign pf
+      return true
+    return res.getD false
 
 /--
 Try to apply `pi_congr`. This is similar to `Lean.MVar.congrImplies?`.
diff --git a/test/congr.lean b/test/congr.lean
index af75411edb217..11a6ab879d829 100644
--- a/test/congr.lean
+++ b/test/congr.lean
@@ -45,3 +45,9 @@ theorem ex11 (p q r : Nat → Prop) (h : q = r) : (∀ n, p n → q n) ↔ (∀
   rename_i n
   guard_target = q n ↔ r n -- it won't use h itself
   rw [h]
+
+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!

From 1d555251e53c29cd3d2dcd8db4cae853d153d7a5 Mon Sep 17 00:00:00 2001
From: Kyle Miller <kmill31415@gmail.com>
Date: Thu, 2 Mar 2023 22:10:39 +0000
Subject: [PATCH 11/11] address failed test

---
 Mathlib/Tactic/Congr!.lean | 11 +++++++----
 test/congr.lean            | 10 ++++++++++
 2 files changed, 17 insertions(+), 4 deletions(-)

diff --git a/Mathlib/Tactic/Congr!.lean b/Mathlib/Tactic/Congr!.lean
index f45e77e214f7a..ec1df7e481c45 100644
--- a/Mathlib/Tactic/Congr!.lean
+++ b/Mathlib/Tactic/Congr!.lean
@@ -5,6 +5,7 @@ Authors: Kyle Miller
 -/
 import Lean
 import Mathlib.Tactic.Relation.Rfl
+import Std.Logic
 
 /-!
 # The `congr!` tactic
@@ -60,7 +61,7 @@ This may be regarded as being a special case of `Lean.MVarId.liftReflToEq`, spec
 -/
 def Lean.MVarId.iffOfEq (mvarId : MVarId) : MetaM MVarId := do
   let res ← observing? do
-    let [mvarId] ← mvarId.apply (mkConst `iff_of_eq []) | failure
+    let [mvarId] ← mvarId.apply (mkConst ``iff_of_eq []) | failure
     return mvarId
   return res.getD mvarId
 
@@ -139,9 +140,9 @@ def Lean.MVarId.proofIrrelHeq (mvarId : MVarId) : MetaM Bool :=
     let res ← observing? do
       mvarId.checkNotAssigned `proofIrrelHeq
       let tgt ← withReducible <| mvarId.getType'
-      let some (_, _, lhs, rhs) := tgt.heq? | failure
+      let some (_, lhs, _, rhs) := tgt.heq? | failure
       -- Note: `mkAppM` uses `withNewMCtxDepth`, which we depend on to avoid unification.
-      let pf ← mkAppM `proof_irrel_heq #[lhs, rhs]
+      let pf ← mkAppM ``proof_irrel_heq #[lhs, rhs]
       mvarId.assign pf
       return true
     return res.getD false
@@ -170,11 +171,13 @@ def Lean.MVarId.obviousFunext? (mvarId : MVarId) : MetaM (Option (List MVarId))
 Try to apply `Function.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 is to prevent unfolding of things like `Set`.
+
+Need to have `Mathlib.Logic.Function.Basic` imported for this to succeed.
 -/
 def Lean.MVarId.obviousHfunext? (mvarId : MVarId) : MetaM (Option (List MVarId)) :=
   mvarId.withContext <| observing? do
     let tgt ← mvarId.getType'
-    let some (_, _, lhs, rhs) := tgt.heq? | failure
+    let some (_, lhs, _, rhs) := tgt.heq? | failure
     if not lhs.isLambda && not rhs.isLambda then failure
     mvarId.apply (← mkConstWithFreshMVarLevels `Function.hfunext)
 
diff --git a/test/congr.lean b/test/congr.lean
index 11a6ab879d829..764b6dbd966f5 100644
--- a/test/congr.lean
+++ b/test/congr.lean
@@ -51,3 +51,13 @@ theorem ex12 (p q : Prop) (h : p ↔ q) : p = q := by
 
 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