Jannis Limperg

I've seen these "no such file or directory" errors before when the VSCode extension compiles dependencies (on MacOS). However, I've not seen them in `lake build` or the Emacs mode...

Thanks for trying again! Let's see if this comes back once we turn `precompileModules` back on. (This is currently blocked on Lake).

+1 from the ICFP artifact evaluation committee. We'd very much appreciate finer-grained control here.

I was struggling with this in Aesop, so I love this PR! Once it lands, will there be an expectation that tactics may realise declarations with reserved names, but may...

> > Once it lands, will there be an expectation that tactics may realise declarations with reserved names, but may not otherwise add new declarations? > > It sounds reasonable,...

Minimised: ```lean import Mathlib.Data.Complex.Exponential open Real (cos) axiom MyDifferentiable : (ℝ → ℝ) → Prop axiom MyDifferentiable.cos {f : ℝ → ℝ} : MyDifferentiable f → MyDifferentiable fun x =>...

Thanks for reporting! This is either a core issue or a `to_additive` issue. Minimisation: In `Mathlib/Min1.lean`: ```lean import Mathlib.Tactic.ToAdditive class Inv (α : Type _) where /-- Invert an element...

Zulip discussion: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/simp.20tracing.20suggests.20private.20simp.20theorems

There's no conceptual reason, it's just a bunch of engineering effort. This features has been requested a few times and I'd also like to have it, so it's definitely going...

Whether the goal has changed is not so easy to detect. You can check for identity of metavariables, which is fast but unreliable. You can check for structural equality of...