commit: 0cc4c918008d64269460bdba41fbcd3df8445af6

[log]
author: Giles Shaw <62542365+gilesgshaw@users.noreply.github.com>

Tue Jul 22 14:21:48 2025 +0100
committer: GitHub <noreply@github.com>

Tue Jul 22 13:21:48 2025 +0000
tree: 127b7dc8dabd52fb5b7ca3edbd411da697675593
parent: 548d564c184687015dde1efb545c79038b8ea24e [diff]

fix: change the proof of Nat.zero_mod to rfl (#9391)

This PR replaces the proof of the simplification lemma `Nat.zero_mod`
with
`rfl` since it is, by design, a definitional equality. This solves an
issue
whereby the lemma could not be used by the simplifier when in 'dsimp'
mode.

Closes #9389

---------

Co-authored-by: Joachim Breitner <mail@joachim-breitner.de>

src/Init/Data/Nat/Div/Basic.lean[diff]
tests/lean/run/9389.lean[Added - diff]

2 files changed

tree: 127b7dc8dabd52fb5b7ca3edbd411da697675593

README.md

This is the repository for Lean 4.

About

Installation

See Setting Up Lean.

Contributing

Please read our Contribution Guidelines first.

Building from Source

See Building Lean.