New here, figuring out if there any use for things I wrote

Stream: new members

[Ilmari Kangasniemi]

Hi,

Just signed up here for the first time. I got curious about formal verification like 1-1.5 months ago, tried the natural numbers game, and went through some of Mathematics in Lean. After that, I decided to stress-test my ability to use the language by verifying this (a topological lemma I've needed not too long ago, though in lesser generality):

variable {X Y : Type*} [TopologicalSpace X] [PseudoMetricSpace Y]

def PreimageBall (f : X → Y) (x : X) (r : ℝ) : Set X :=
  connectedComponentIn (f⁻¹' (ball (f x) r)) x

theorem nhds_basis_closure_PreimageBall [T2Space X]
    [LocallyCompactSpace X] [LocallyConnectedSpace X] [MetricSpace Z] {x : X} {f : X → Z}
    (f_cont : Continuous f) (x_isol : connectedComponentIn (f⁻¹' {f x}) x = {x})
    : (𝓝 x).HasBasis (fun r ↦ 0 < r) (fun (r : ℝ) ↦ closure (PreimageBall f x r)) := by
  ...

It certainly took longer than expected to verify, and on the way I had to type up various other topological lemmas (I think the trickiest one was that the intersection of a directed family of compact connected sets in a Hausdorff space is connected).

Is there any potential use for these things that I've typed? I've never contributed to any open-source libraries, and I don't know what are your quality standards for mathlib and if what I wrote has any chance of passing those (nor if some of these results are already in there under a guise that I can't recognize). I'm wondering that the above one that I set as an "end-goal" to myself might be too niche (it's probably not in full generality), but some of the ones I assembled on the way could be useful if they aren't in there already.

A couple of the main questions that have arisen from this experiment:

• How do you generally handle imports and figuring out what to import? I tried importing just the things I need at the start, but I kept running into trouble when I tried that. Eventually I just imported all of mathlib, but that's probably not the right call.
• It seems to me that VSCode starts slowing down heavily once a file gets larger, to the point that it might be eating up some of my spacebar presses. Is this natural/is there ways to mitigate this?

-Ilmari

[Johan Commelin]

@Ilmari Kangasniemi Welcome! Is your code available in a public place, so that we can look at some of your helper lemmas and/or proofs?

Regarding imports: You can import Mathlib, and then trim down the needed imports when you are done. There is even a tool for that: lake exe shake.

Regarding slow downs: Large files shouldn't be too much of a problem. (Depends on "large", I guess. But ~3000 loc should be fine for example.) How large is your file? What does cause slowdowns is large proofs. People are working hard on solving that. But in the mean time, we often try to keep proofs < 100 loc (and generally < 30 loc). So splitting up a lemma into more helper lemmas might be a workaround for the slowdowns you are seeing.

[Kevin Buzzard]

One criterion for "do we want this lemma in mathlib" is "are there mathematicians who need this lemma in real life", so if you're that mathematician then this is an argument for PRing your lemma to mathlib. The PR process is long and complex, for precisely the reason you isolate (quality standards are high) however the community is very open to helping newcomers getting their code to reach this standard (experts frequently suggest rewrites and don't demand any credit; this is the culture here). As Johan suggests, perhaps the first step is that the community looks at your code as it is now and makes suggestions about what if anything needs to be changed in order to make it appropriate for mathlib.

[Kevin Buzzard]

Regarding slowdowns -- ten small lemmas is much better than one lemma of ten times the size. There is a certain art to pulling out sublemmas and finding the right abstractions.

[Ilmari Kangasniemi]

Hi,

I'll attach the file here. I'm open to hearing about all the blunders I made in it.

EarlyTests.lean

Based on those standards of large, the file is overall not yet particularly large then, since it's around 550 lines with comments. I've already tried to chop up everything into as discrete and reusable parts as possible, but the main chunk is still around 100 lines. I also wonder if the slowdowns are due to me using a lot of 'have' -statements in the longer proofs (most of the shorter parts I've tried to compress into proof terms).

Thanks for mentioning the shake -command, I'll look into it.

-Ilmari

[Kevin Buzzard]

This whole file compiles for me in about two seconds! An initial glance indicates that it looks very nice.

The reason you couldn't deduce the set version from the lattice version in your first few lemmas is that you have a typo in le_of_le_sup_Disjoint_right(and le_of_le_sup_Disjoint_left) : it should be {s a b : α}, not Set α. Then

theorem le_of_le_sup_Disjoint_right [DistribLattice α][OrderBot α]
    {s a b : α}(ssup : s ≤ a ⊔ b) (dsb : Disjoint s b) : s ≤ a :=
  calc
    s ≤ (a ⊔ s) ⊓ (a ⊔ b) := le_inf le_sup_right ssup
    _ ≤ a ⊔ s ⊓ b := le_sup_inf
    _ = a ⊔ ⊥ := by rw[disjoint_iff.mp dsb]
    _ ≤ a := sup_le (le_refl a) bot_le

theorem subset_of_subset_union_disjoint_right {S A B : Set α}
    (Su : S ⊆ A ∪ B) (dSB : Disjoint S B) : S ⊆ A :=
  le_of_le_sup_Disjoint_right Su dSB

[Ilmari Kangasniemi]

That's a good blunder to catch - missed that when copying over the definitions when I realized that it probably already works at the lattice level instead of set level. Tested and it works with that issue fixed. The subset versions are then probably pointless as they're essentially aliases. (Even then I don't know if these should already exist somewhere; they feel like they're a basic set theory tool that should be implemented pretty early, but some ctrl+space -searching with "disjoint" didn't lead me anywhere.)