Sebastien Gouezel
Sebastien Gouezel
Here is an example where instance search done by the first simp is done again by the second simp, without taking advantage of the cache. ```lean set_option trace.class_instances true lemma...
When trying to use relative imports, I realized that they did not work for files with more than 3 levels of subdirectories. Browing on Zulip, I found [a message from...
`apply_instance` fails to find an instance, although it finds one for another problem which is defeq to the first one, even with the flag `tactic.transparency.instances`. MWE, based on mathlib: ```lean...
We define functions of bounded variation. We show that such functions are a difference of monotone functions, and deduce that they are differentiable almost everywhere. This applies in particular to...
--- [](https://gitpod.io/from-referrer/)
MWE: ```lean import Std def foo : Nat → Nat := sorry theorem foo_eq_iff (z : Nat) : z = 17 ↔ foo z = 3 := sorry theorem fail...
Given ``` squeeze_simpa [model_with_corners.left_inv] using hx }, ``` if I click on the suggested output it erases the space between `hx` and `}`. This breaks mathlib style convention.
The current Lean 4 mechanism for including variables is the following: When starting the proof of a theorem (or the body of a definition, it doesn't make a difference), all...
We prove a version of Prokhorov theorem: given a sequence of compact sets `Kₙ` and a sequence `uₙ` tending to zero, the probability measures giving mass at most `uₙ` to...