minor bug in `lift` tactic

Stream: mathlib4

[Johan Commelin]

MWE

import Mathlib.Tactic.Lift

abbrev MyNat := ℕ

example (n : ℤ) (hn : n ≥ 0) : True := by
  lift n to MyNat using hn
  -- type of `n` is `ℕ` instead of `MyNat`, in the goal state
  trivial

[Johan Commelin]

This means that we can not use dot-notation on n for all the juicy decls in the MyNat namespace.

[Eric Wieser]

Does this work using def?

[Kevin Buzzard]

This works fine for me with example on a recent master...(oh I see, it's supposed to compile). The same phenomenon occurs with def.

[Vincent Beffara]

You can always do this

import Mathlib.Tactic.Lift

abbrev MyNat := ℕ

example (n : ℤ) (hn : n ≥ 0) : True := by
  lift n to MyNat using hn
  change MyNat at n
  trivial

but it's annoying

[Kevin Buzzard]

Right but I would imagine that this still counts as a minor bug.

[Johan Commelin]

Right, I am using change right now. But it shouldn't be needed.

[Kyle Miller]

I was trying to step through what lift roughly does, but the way I'm doing it preserves MyNat:

abbrev MyNat := ℕ

example (n : ℤ) (hn : n ≥ 0) : True := by
  have := @CanLift.prf ℤ MyNat _ _ _ n hn
  obtain ⟨n', hn'⟩ := this
  subst hn'
  /-
  n' : MyNat
  hn : ↑n' ≥ 0
  ⊢ True
  -/

I'm not sure what the deal is exactly.

[Kyle Miller]

I noticed that lift uses simp to substitute away the variable. That can be done more efficiently and accurately with subst

[Johan Commelin]

Filed as

lift tactic does not respect abbreviations #15865