Feedback on proof coding style

Stream: new members

[Alessandro D'Angelo]

Hi everyone! I'm new to Lean and have been learning by formalizing results from algebraic geometry. I've worked on Lemma 5.7 from Görtz-Wedhorn's "Algebraic Geometry" (2nd edition), which you can find here:
Lean file: https://github.com/ADA-Projects/Lean-AG/blob/main/GWchap5/gw_sect5-3.lean
Blueprint: https://ada-projects.github.io/Lean-AG/

I have two questions:

1. Does this result already exist in mathlib? I couldn't find it, but I may have missed something.
2. Any suggestions for making the proof more elegant? The current proof is quite lengthy—likely due to my inexperience with Lean proof style and the need to establish many "trivial" intermediate steps. I'd appreciate any feedback on improving the approach or making it more concise.

Thanks in advance for any insights!
P.S. Thanks to Pietro Monticone for the excellent Lean project template: https://github.com/pitmonticone/LeanProject

[Andrew Yang]

Welcome! One or two lemmas in your file is indeed in mathlib (e.g. docs#Topology.IsEmbedding.closure_eq_preimage_closure_image) but the majority is not, and they look really promising. I agree that the proof looks lengthy at places but it is already really impressive as a beginner. For the next step I would suggest you open PRs (following the contribution guideline) of chunks of your file (IMO a good first chunk is everything up to top_KrullDim_subspace_le) and I or other mathlib reviewers can give you fine-grained feedbacks to the code.

[Alessandro D'Angelo]

great! Thank you very much, will do!

[Rado Kirov]

OOC, why so many comments. Some are quite trivial, e.g.

    -- Step 2: `apply (WithBot.ne_bot_iff_exists).mpr`
    -- This applies the `←` direction of the key `iff` lemma.
    -- The goal becomes `topologicalKrullDim X ≠ ⊥`.
    apply (WithBot.ne_bot_iff_exists).mp

I think to anyone familiar with Lean just apply (WithBot.ne_bot_iff_exists).mp is enough for this line.

[Lawrence Wu (llllvvuu)]

Was this done with an agentic AI setup? If so, what was the setup if you don’t mind me asking?

[Rado Kirov]

The use of emojis in the README definitely look like telltale sign (not that using AI is a problem).

[Yan Yablonovskiy 🇺🇦]

I would say that its often nicer instead of

    constructor
    · -- Goal 1: Prove `↑y ∈ Y`. This is true by definition of the subtype Y.
      exact y.property
    · -- Goal 2: Prove `↑y ∈ closure ((↑) '' A)`.
      -- Apply the fact that any set is a subset of its closure.
      apply subset_closure
      -- Now, the goal is to prove that `↑y` is in the set itself.
      exact mem_image_of_mem Subtype.val hy_in_A

to have something like

exact ⟨ y.property,  subset_closure (mem_image_of_mem Subtype.val hy_in_A) ⟩

I would avoid using multiple new lines of apply followed by new lines of exact for shorter proofs. You should try go in and golf the LLM output as much as you can, because LLM can be very verbose and inefficient.

[Alessandro D'Angelo]

@Rado Kirov
Yeah the comments were more meant for myself, for learning. I've polished the file following mathlib guidelines, I'll push it soon.

@Lawrence Wu (llllvvuu)
Yes, I've used Gemini to help me with the Lean syntax that I still don't know well