fix: `split at h` when `h` has forward dependencies

leanprover / lean4

Lean 4 programming language and theorem prover

https://lean-lang.org

Apache License 2.0

3.88k stars 329 forks source link

Closed leodemoura closed 2 weeks ago

leodemoura commented 2 weeks ago

We use an approach similar to the one used in simp.

closes #3731

leanprover-community-mathlib4-bot commented 2 weeks ago

Mathlib CI status (docs):

❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 7648bf255cfff9d679404b05f7aa8601044990ca --onto 3a457e6ad60272f03c3555e443379dbde10507ea. (2024-05-18 02:50:24)