abbreviation "func" in mathlib

Stream: mathlib4

[Dexin Zhang]

The usual abbreviation of "function" should be "fun" instead of "func", but there are still some names using "func" in mathlib. (@Yaël Dillies raised me this question in #27099.) After a search in mathlib, I find the following names using "func":

Measure theory: docs#MeasureTheory.SimpleFunc
Algebra: docs#RatFunc, docs#MvRatFunc.rank_eq_max_lift
Category theory: docs#CategoryTheory.Arrow.leftFunc, docs#CategoryTheory.Arrow.rightFunc, docs#CategoryTheory.FreeMonoidalCategory.tensorFunc (here "func" is for "functor". I guess that is OK?)
Model theory: docs#FirstOrder.Language.Term.func, docs#FirstOrder.Language.Term.substFunc, docs#FirstOrder.ringFunc, docs#FirstOrder.Ring.addFunc etc
Set theory: docs#PSet.Func, docs#ZFSet.IsFunc

Especially in model theory "func" is almost always used instead of "fun", which might be inconsistent with the rest of mathlib. Should we change all those to "fun"? But I also feel these "func" as first-order function symbols could be distinguished from Lean functions.

[Yaël Dillies]

cc @Mario Carneiro for SimpleFunc

[Jovan Gerbscheid]

Isn't "fun" mostly used for lambda functions, like in fun x => f x + g x, or actual lean functions, like in Nat.card_fun?

[Mario Carneiro]

I have no objections to changing SimpleFunc to SimpleFun