Regression in v4.33.0-rc1: `simp` changes the type of hoisted proof

Prerequisites

• 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

When updating DyLean to v4.33.0-rc1, I noticed the following regression:
when writing a proof inside a function definition, it seems that Lean hoists the proof in an auxiliary ._proof_1 theorem, however when proving this theorem using simp, the type of the hoisted theorem can change. See the example below.

opaque Bytes: Type
opaque Bytes.length: Bytes → Nat

axiom foo
  {a: Type}
  (f: a → Bytes)
  (len: Nat)
  (h: ∀ x, (f x).length = len) 
  : a

def f {len: Nat} (b: { b: Bytes // b.length = len}): Bytes :=
  b.val

noncomputable
def bar (len: Nat) : ({ b: Bytes // b.length = len}) :=
  foo f len (by
    simp [f]
    -- fix: instead use grind [f]
  )


set_option linter.tacticCheckInstances true

/--
warning: produced tactic goal is not type-correct at `.implicit` transparency; consider using propositional rewriting or marking some of the following as `@[implicit_reducible]`:
  f
Full error:
  Application type mismatch: The argument
    bar._proof_1 len
  has type
    ∀ (x : { a // a.length = len }), @Eq Nat x.val.length len
  but is expected to have type
    ∀ (x : { b // b.length = len }), @Eq Nat (f x).length len
  in the application
    foo f len ⋯

Note: This linter can be disabled with `set_option linter.tacticCheckInstances false`
-/
#guard_msgs in
example (len: Nat): bar len = bar len := by
  unfold bar
  rfl

-- diagnostic: bar._proof_1 has the wrong type!
-- should be: .................................................. : (f x).length = len -/
/-- info: bar._proof_1 (len : Nat) (x : { a // a.length = len }) : x.val.length = len -/
#guard_msgs in
#check bar._proof_1

Context

Unlikely to stem from #13895? Because adding the option set_option backward.isDefEq.respectTransparency.types false does not fix the issue.

Steps to Reproduce

Expected behavior: using simp or any other tactic does not change the type of the hoisted theorem

Actual behavior: using simp changes the type of the hoisted theorem, and leaks the definition of f

Versions

• "4.33.0-rc1"
• "4.34.0, commit 323137b022369d56a044ae5af01d1efd55872361" (on live.lean-lang.org)

Impact

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

Start with the minimal Lean reproduction in the issue and compare the generated bar._proof_1 type with the expected (f x).length = len type. Investigate the interaction between simp, proof hoisting, and transparency, then validate the fix by running the reproduction and confirming that #check bar._proof_1 reports the expected type without leaking f.