Adam Topaz

`lake new foo math` can cause a mismatch in Lean4 versions.

3

`lake new foo math` creates a folder `foo` with a `lean-toolchain` file based on the version of Lean used to invoke `lake`, while also adding `mathlib4` as a dependency. The...

feat(ring_theory/valuation/valuation_subring): Supremum of families of valuation rings.

1

Adds two definitions: - The supremum of a directed family of valuation rings, as a valuation ring. - The supremum of a family of valuation rings which are bounded below...

--- [](https://gitpod.io/from-referrer/)

The function `TacticInfo.getUsedConstantsAsSet` previously simply looked at the mvarids in the goals before a given tactic, check if they had an assignment, and collect the used constants from those assignments....