Replace default `.mk` for a class

Stream: lean4

[Calle Sönne]

If I have defined some class, is there anyway I can replace the default constructor .mk with a weaker lemma that's easier to verify? Or is it best to call the other lemma something different, like .mk'.

This is my specific case, in case someone wants to recommend a different approach:

/-- Definition of a Fibered category. -/
class IsFibered (p : 𝒳 ⥤ 𝒮) : Prop where
  (has_pullbacks {a : 𝒳} {R S : 𝒮} (_ : p.obj a = S) (f : R ⟶ S) :
    ∃ (b : 𝒳) (φ : b ⟶ a), IsPullback p f φ)

protected lemma IsFibered.mk' {p : 𝒳 ⥤ 𝒮} (h : ∀ (a : 𝒳) (R : 𝒮) (f : R ⟶ p.obj a),
    ∃ (b : 𝒳) (φ : b ⟶ a), IsPullback p f φ) : IsFibered p where
  has_pullbacks := @fun a R S ha f => by subst ha; apply h a R f

The difference between the two is quite small. Basically, in IsFibered.mk' one always takes S to be p.obj a, whereas in the definition of IsFibered one is allowed to give a different S together with a proof that S = p.obj a. The first definition is more flexible with equalities, which is convenient when using the class, whereas the latter is slightly more convenient to show when defining an instance.

[James Gallicchio]

I think my rule of thumb would be to name your weaker constructor something else? You can rename the default constructor (see the first code block here) if you really want this lemma to be named mk, but I don't think doing this will change what constructor is used for <> notation and the constructor tactic and so on

[Mario Carneiro]

if you search for mk' :: in mathlib you will see this is a pretty common technique

[Markus Himmel]

I think we often rename constructors in mathlib if the original constructor requires a lot of wrapping involving things like existentials or Nonempty. See for example docs#CategoryTheory.Limits.HasLimit and docs#CategoryTheory.Limits.HasLimit.mk

[James Gallicchio]

does that change what is used by <> and constructor?

[Calle Sönne]

James Gallicchio said:

I think my rule of thumb would be to name your weaker constructor something else? You can rename the default constructor (see the first code block here) if you really want this lemma to be named mk, but I don't think doing this will change what constructor is used for <> notation and the constructor tactic and so on

Okay thanks, I don't mind what constructor is used for the <> notation, so I will rename the "default" one to mk' then.

[Mario Carneiro]

James Gallicchio said:

does that change what is used by <> and constructor?

no

[Kevin Buzzard]

docs#Rat.mk is another home-rolled mk

[Kevin Buzzard]

Oh! It's not there any more? But the default constructor is still called mk'?

[Markus Himmel]

Are you thinking of docs#mkRat ?

[Yury G. Kudryashov]

Another approach is to use the version with seemingly weaker assumptions as the definition and make the original version a lemma.

[Calle Sönne]

Yury G. Kudryashov said:

Another approach is to use the version with seemingly weaker assumptions as the definition and make the original version a lemma.

This is what I ended up doing eventually! :)