fix: use pi_congr instead of forall_congr; deprecate the latter

This PR generalizes the `conv` and `simp` tactics to apply `pi_congr` instead
of `forall_congr`. The test case for #7507 has examples that work now, but only
worked at universe `v=0` before.

Since there are no more remaining uses of `forall_congr`, it is now deprecated.

Fixes #7507.

src/Init/SimpLemmas.lean

@@ -45,6 +45,10 @@ 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 pi_congr {α : Sort u} {β β' : α → Sort v} (h : ∀ a, β a = β' a) : (∀ a, β a) = ∀ a, β' a :=
+  (funext h : β = β') ▸ rfl
+
+@[deprecated pi_congr (since := "2025-03-20")]
 theorem forall_congr {α : Sort u} {p q : α → Prop} (h : ∀ a, p a = q a) : (∀ a, p a) = (∀ a, q a) :=
   (funext h : p = q) ▸ rfl
 
@@ -58,9 +62,6 @@ theorem forall_prop_congr_dom {p₁ p₂ : Prop} (h : p₁ = p₂) (q : p₁ →
     (∀ a : p₁, q a) = (∀ a : p₂, q (h.substr a)) :=
   h ▸ rfl
 
-theorem pi_congr {α : Sort u} {β β' : α → Sort v} (h : ∀ a, β a = β' a) : (∀ a, β a) = ∀ a, β' a :=
-  (funext h : β = β') ▸ rfl
-
 theorem let_congr {α : Sort u} {β : Sort v} {a a' : α} {b b' : α → β}
     (h₁ : a = a') (h₂ : ∀ x, b x = b' x) : (let x := a; b x) = (let x := a'; b' x) :=
   h₁ ▸ (funext h₂ : b = b') ▸ rfl

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

@@ -288,14 +288,15 @@ private def extCore (mvarId : MVarId) (userName? : Option Name) : MetaM MVarId :
       let u ← getLevel d
       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
+      let (q, h, v, mvarNew) ← withLocalDecl userName bi d fun a => do
         let pa := b.instantiate1 a
         let (qa, mvarNew) ← mkConvGoalFor pa
+        let v ← getLevel pa
         let q ← mkLambdaFVars #[a] qa
         let h ← mkLambdaFVars #[a] mvarNew
         resolveRhs "ext" rhs (← mkForallFVars #[a] qa)
-        return (q, h, mvarNew)
-      let proof := mkApp4 (mkConst ``forall_congr [u]) d p q h
+        return (q, h, v, mvarNew)
+      let proof := mkApp4 (mkConst ``pi_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/Meta/AppBuilder.lean

@@ -632,8 +632,8 @@ def mkImpCongrCtx (h₁ h₂ : Expr) : MetaM Expr :=
 def mkImpDepCongrCtx (h₁ h₂ : Expr) : MetaM Expr :=
   mkAppM ``implies_dep_congr_ctx #[h₁, h₂]
 
-def mkForallCongr (h : Expr) : MetaM Expr :=
-  mkAppM ``forall_congr #[h]
+def mkPiCongr (h : Expr) : MetaM Expr :=
+  mkAppM ``pi_congr #[h]
 
 /-- Returns instance for `[Monad m]` if there is one -/
 def isMonad? (m : Expr) : MetaM (Option Expr) :=

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

@@ -338,12 +338,11 @@ def simpForall (e : Expr) : SimpM Result := withParent e do
   trace[Debug.Meta.Tactic.simp] "forall {e}"
   if e.isArrow then
     simpArrow e
-  else if (← isProp e) then
-    /- The forall is a proposition. -/
+  else
     let domain := e.bindingDomain!
-    if (← isProp domain) then
+    if (← isProp e) && (← isProp domain) then
       /-
-      The domain of the forall is also a proposition, and we can use `forall_prop_domain_congr`
+      The domain and codomain of the forall are propositions, and we can use `forall_prop_domain_congr`
       IF we can simplify the domain.
       -/
       let rd ← simp domain
@@ -379,9 +378,7 @@ def simpForall (e : Expr) : SimpM Result := withParent e do
       let eNew ← mkForallFVars #[x] rb.expr
       match rb.proof? with
       | none   => return { expr := eNew }
-      | some h => return { expr := eNew, proof? := (← mkForallCongr (← mkLambdaFVars #[x] h)) }
-  else
-    return { expr := (← dsimp e) }
+      | some h => return { expr := eNew, proof? := (← mkPiCongr (← mkLambdaFVars #[x] h)) }
 
 def simpLet (e : Expr) : SimpM Result := do
   let .letE n t v b _ := e | unreachable!

tests/lean/run/7507.lean

@@ -0,0 +1,16 @@
+/-! Tests that conv and simp apply pi_congr rather than the less general forall_congr.
+    The following examples used to work only at v = 0.
+-/
+
+axiom f : Sort u → Sort v
+axiom g : Sort u → Sort v
+axiom fg.eq (α : Sort u) : f α = g α
+
+example : ((x:Sort u) → f.{u,v} x) = ((x : Sort u) → g.{u,v} x) :=
+  pi_congr fg.eq
+
+example : ((x:Sort u) → f.{u,v} x) = ((x : Sort u) → g.{u,v} x) := by
+  conv => lhs; ext; apply fg.eq
+
+example : ((x:Sort u) → f.{u,v} x) = ((x : Sort u) → g.{u,v} x) := by
+  simp only [fg.eq]