Tactics can modify the elaborated types of theorems with let rec

Prerequisites

Please put an X between the brackets as you perform the following steps:

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

Tactics within a proof can change the type of a theorem with let rec in.

Steps to Reproduce

import Mathlib

theorem ohno :
  ¬ ((let rec recur (n : Nat) : List Nat :=
      match n with
      | 0 => [1]
      | (Nat.succ n) => recur n
    recur 0 = [1])) ∧ True := by
        -- sorry
        refine Decidable.byContradiction fun h_contra => ?_
        apply h_contra
        constructor
        intro h
        apply_mod_cast h_contra
        any_goals tauto
        simp

theorem a : False := by
  have := ohno
  simp [ohno.recur] at this

Expected behavior: swapping the "proof" of ohno for "sorry" should not change the type of "ohno",

Actual behavior: when "ohno" is sorried out the type includes ohno.recur (and the following theorem is provable (ie ohno is false)). But when it is not sorried out Lean accepts the proof, which is fairly unintuitive.

on latest, I couldn't get rid of the Mathlib import easily but hopefully this is clear enough

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

Start by running the issue's minimal reproduction and compare the elaborated type of ohno with and without its proof replaced by sorry. Investigate the interaction between let rec, theorem elaboration, and tactics; done means both forms preserve the same theorem type and the later ohno.recur use cannot change provability.