lift unhappy with `let` or `set` values

Stream: mathlib4

[Yakov Pechersky]

import Mathlib.Data.Real.EReal

example {α : Type*} (f : α → EReal) (a : α) (ha : f a ≠ ⊤) (hb : f a ≠ ⊥) :
    ∃ x : ℝ, f a = x := by
  -- lift f a to ℝ -- lift tactic failed. When lifting an expression, a new variable name must be given
  let A := f a
  -- lift A to ℝ -- tactic 'subst' failed, invalid equality proof, it is not of the form (x = t) or (t = x)
  -- ↑A = A✝
  sorry

This was brought up by my try at writing proofs for https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/.60nsmul_sInf.60

[Floris van Doorn]

I think lift f a to ℝ with A is what you want

[Floris van Doorn]

This error has also bitten me before (it wasn't necessary to give a name in Lean 3). Should we improve the error message (by writing "... using lift ... to ... with ...") or should we just allow lift to create a new name?

[Yakov Pechersky]

Perhaps both? Ideally it can recognize if the user has already assigned a name to the value. And suggest otherwise?

[Floris van Doorn]

If the name is a variable, it already works by re-using that variable

example {α : Type*} (z : EReal) (ha : z ≠ ⊤) (hb : z ≠ ⊥) :
    ∃ x : ℝ, z = x := by
  lift z to ℝ

[Yakov Pechersky]

but not in the let A := f a case

[Floris van Doorn]

However, as your first message shows, there is a bug when the variable is actually a let variable

[Floris van Doorn]

I think in the let A := f a case it should just do the same as when doing lift f a. The problem with re-using the name A is that it loses information (i.e. the body of the old A).

[Kyle Miller]

If the old A is shadowed, then it's not completely lost.