leanprover-community/physlib

Remove `erw`s

Open

#385 opened on Mar 10, 2025

View on GitHub
 (1 comment) (0 reactions) (0 assignees)Lean (139 forks)auto 404
good first issuehelp-wanted

Repository metrics

Stars
 (642 stars)
PR merge metrics
 (PR metrics pending)

Description

There are lots of erw [...] in PhysLean. These are slow, and thus it is beneficial for them to be removed.

To remove an erw [...] usually means changing the corresponding lemma to simp-normal form.

Contributor guide

Research direction
Search the codebase for `erw` patterns. For each, identify the lemma being used and consider if it can be made `simp` normal. Then replace `erw` with `simp` or `rw` as appropriate. Ensure changes pass the test suite.
Tech stack
None
Domain
performance
Issue type
Refactor
DifficultyEstimated implementation difficulty for a new contributor, from 1 for very small changes to 5 for expert-level work.
2
Estimated timeA rough time range for an experienced contributor to investigate, implement, test, and prepare a pull request.
Half day
Activity statusHow available the issue appears right now: fresh, active, stale, blocked, or waiting on maintainer input.
Active
ClarityHow clearly the issue explains the expected change, acceptance criteria, and next step.
Clear
Prerequisites
Lean
Newbie friendlinessA 1-100 score estimating how approachable this issue is for first-time contributors.
70