leanprover-community / leanprover-community/mathlib4
`push_cast` doesn't run `rfl` after operation
Open
Nobody has claimed this yet.
t-meta
- Dominant language
- Lean
- Stars
- 4.1k
- Forks
- 1.7k
- PR merge metrics
- No merged PRs in 30d
Description
In mathlib3, this worked:
import tactic.norm_cast
import data.rat.basic
example (a b : ℤ) : ((a + b : ℤ) : ℚ) = (a:ℚ) + b := by push_cast
In mathlib4, I need rfl at the end:
import Mathlib.Tactic.NormCast
import Mathlib.Data.Rat.Basic
example (a b : ℤ) : ((a + b : ℤ) : ℚ) = (a:ℚ) + b := by push_cast ; rfl
Could we return to the mathlib3 behavior?
Contributor guide
First steps
- Read the whole issue, then the project's contributing guide.
- Comment on the issue to say you are picking it up — it saves two people doing the same work.
- Fork the repository and make your change on a branch.
- Open a pull request that references the issue number.
Research direction
Start by running the provided example with Mathlib.Tactic.NormCast and Mathlib.Data.Rat.Basic, then inspect the push_cast behavior exposed by the norm-cast tactic. Done means the example closes with by push_cast alone, matching the stated mathlib3 behavior.
Written by the indexing model from the issue text.
Assessment
- Domain
- tooling
- Issue type
- Bug
- Difficulty
- 3/5
- Estimated time
- 1-2 days
- Activity status
- Stale
- Clarity
- Mostly clear
- Newbie friendliness
- 48/100