include in lean 4

Stream: lean4

[Connor Gordon]

Just for some practice, I'm trying to convert some simple exercises from a class I took in Lean 3 into Lean 4. We defined the following variables

variables {α β : Type*} [partial_order α] [partial_order β]
variable  {f : α → β}
variable  {g : β → α}
variable  mono_f : monotone f
variable  mono_g : monotone g
variable  adj1 : ∀ a b, f a ≤ b → a ≤ g b
variable  adj2 : ∀ a b, a ≤ g b → f a ≤ b

And then to include mono_f and mono_g as hypotheses in the following results, we used

include mono_f mono_g

This all worked fine in Lean 3, but Lean 4 does not seem to like this. Is there an analogue of this in Lean 4, or should I do something else?

[Patrick Massot]

It will get included. Everything gets included in Lean 4. It will even look like it includes too much (but things you don't use do not stay in the lemma).

[Connor Gordon]

Ah, I see. Thank you!