Style for long proofs in instances

Stream: mathlib4

[Christian K]

Hello,
I want to prove that the Nucleus in Mathlib is a CompleteSemilatticeInf. I implemented it like this:

variable {s : Set (Nucleus X)}

def sInf_fun (s : Set (Nucleus X)) (x : X) := sInf {j x | j ∈ s}

def sInf_fun_increasing : ∀ (x : X), x ≤ sInf_fun s x := by
  simp [sInf_fun, le_apply]

def sInf_fun_idempotent : ∀ (x : X), sInf_fun s (sInf_fun s x) ≤ sInf_fun s x := by
  intro x
  simp only [sInf_fun, le_sInf_iff, Set.mem_setOf_eq, forall_exists_index, and_imp,
    forall_apply_eq_imp_iff₂, sInf_le_iff, lowerBounds]
  intro a ha b h
  rw [← idempotent]
  apply le_trans (h a ha)
  refine OrderHomClass.GCongr.mono a ?_
  simp_all [sInf_le_iff, lowerBounds]

def sInf_preserves_inf : ∀ (x y : X), sInf_fun s (x ⊓ y) = sInf_fun s x ⊓ sInf_fun s y := by
  simp only [sInf_fun, InfHomClass.map_inf]
  intro x y
  apply le_antisymm
  · simp_all only [le_inf_iff, le_sInf_iff, Set.mem_setOf_eq, sInf_le_iff, lowerBounds,
    forall_exists_index, and_imp, forall_apply_eq_imp_iff₂, implies_true, and_self]
  · simp [le_sInf_iff]
    intro a ha
    apply And.intro
    · apply inf_le_of_left_le
      simp_all [sInf_le_iff, lowerBounds]
    · apply inf_le_of_right_le
      simp_all [sInf_le_iff, lowerBounds]

instance : InfSet (Nucleus X) where
  sInf s := ⟨⟨sInf_fun s, sInf_preserves_inf⟩, sInf_fun_idempotent, sInf_fun_increasing⟩

This seems rather ugly to me, but I'm not sure how to do this differently. I separted the proofs into their own lemmas, because they are to big to be done inline at the sInf instance. Can these proofs be golfed considerably and(are there any helpful resources for me to learn how to shorten these? proofs)?. In general, what is the idiomatic way to handle such a case where the proofs are to big to fit in the instance definition?

[Michael Rothgang]

I noticed a few details which might be helpful (even thought they may not fully answer your question):

• side comment: I suspect most of your defs should be lemmas. (If you run #lint after your code, a defLemma linter should complain.)
• are all these simp_alls necessary, or does simp also work?
• if the latter; simp and exact can usually be combined into simpa or simpa using: for example simp [foo]; exact bar can usually become simpa [foo] using bar

[Michael Rothgang]

Since you're asking about idiomatic code, let me also mention the mathlib convention "hypotheses left of colon": instead of having a conclusion "\forall x, ... and starting your proofs with intro x, it's shorter to make x` part of the hypotheses.

[Michael Rothgang]

A few more comments:

• can refine OrderHomClass.GCongr.mono a ?_ just become gcongr?
• the first subgoal in sInf_preserves_inf is a terminal simp: unless it's slow, you don't need to squeeze it (i.e. writing simp or simp_all is just fine)
• if you just want shorter code: apply And.intro should be equivalent to constructor or refine \<?_, ?_\> (these should be the correct angular brackets; cannot type them into zulip right now); if one proof is short you can also "inline" it (i.e. write refine \<by simp, ?_\>)

[Michael Rothgang]

Finally: writing out lemmas needed for these instances seems useful (particularly if you want to use those results separately, at some point in the future, or anticipate somebody wanting to do so).

I have a number of comments now. Let me emphasize that all these are about style: your code works already; these are just things I'd do to make it more mathlib-ready.

[Christian K]

Thank you very much for your detailed comments, they are very helpful to me! I implemented them and created a PR.