fix(to_fun): fix the @[to_fun] attribute when the proof is not by reflexivity (#32866)

This PR fixes the bug in `@[to_fun]` reported in https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/.60to_fun.60.20tactic/with/563623809

Author: JovanGerb

Mathlib/Tactic/ToFun.lean

@@ -46,7 +46,11 @@ initialize registerBuiltinAttribute {
       let r ← Push.pullCore .lambda type none
       if r.expr == type then
         throwError "`@[to_fun]` failed to eta-expand any part of `{.ofConstName src}`."
-      return (← r.mkCast value, levels)
+      -- Ensure that the returned `value` has type `r.expr`.
+      let value ← match r.proof? with
+        | none => mkExpectedTypeHint value r.expr
+        | some proof => mkAppOptM ``cast #[type, r.expr, proof, value]
+      return (value, levels)
   | _ => throwUnsupportedSyntax }
 
 end Mathlib.Tactic

MathlibTest/ToFun.lean

@@ -24,3 +24,17 @@ Look I am the doc-string of `foo`.
 run_meta
   let some doc  ← findDocString? (← getEnv) ``fun_foo | throwError "no docstring found"
   logInfo doc
+
+
+-- Test that it also works when the generated proof is not a `rfl` proof:
+
+@[to_additive (attr := push ← high)]
+lemma Pi.mul_def' {ι : Type*} {M : ι → Type*} [∀ i, Mul (M i)] (f g : ∀ i, M i) :
+    f * g = fun i ↦ f i * g i := (rfl)
+
+@[to_fun]
+theorem Function.mul_comm' (f g : ℝ → ℝ) : f * g = g * f := _root_.mul_comm f g
+
+/-- info: Function.fun_mul_comm' (f g : ℝ → ℝ) : (fun i => f i * g i) = fun i => g i * f i -/
+#guard_msgs in
+#check Function.fun_mul_comm'