HEPLean / HepLean

A project to digitalise results from high energy physics into Lean.
https://heplean.github.io/HepLean/
Apache License 2.0
56 stars 4 forks source link

refactor: Multigoal proofs #123

Closed jstoobysmith closed 2 months ago

jstoobysmith commented 2 months ago

Refactor proofs with multiple goals using the linter described here:

https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/linting.20against.20.22multi-goal.20proofs.22/near/434773926