A problem in mathematics in lean

Stream: new members

[tsuki hao]

'''
example (h₀ : d ≤ e) : c + exp (a + d) ≤ c + exp (a + e) := by
sorry
'''
Can someone tell me how to complete the above code

[Kevin Buzzard]

Can you please post a #mwe using #backticks ? That's the best way to ask a question here.

[Notification Bot]

This topic was moved here from #lean4 > A problem in mathematics in lean by Yury G. Kudryashov.

[Yury G. Kudryashov]

As far as I understand, #lean4 is for questions that may need attention of core developers.

[tsuki hao]

Kevin Buzzard said:

Can you please post a #mwe using #backticks ? That's the best way to ask a question here.

Thanks for the reminder, my problem is this

example (h₀ : d ≤ e) : c + exp (a + d) ≤ c + exp (a + e) := by
sorry

[tsuki hao]

Yury G. Kudryashov said:

As far as I understand, #lean4 is for questions that may need attention of core developers.

Sorry, besides, can I ask you where I should be asking

[Yury G. Kudryashov]

#new members, #general , or #maths (I can't formulate exact rules; we'll move if we think a thread is more appropriate in another stream)

[Yury G. Kudryashov]

A #mwe includes all required imports, opens, and variables (if any)

[Yury G. Kudryashov]

Try gcongr or mono*. Should just work.

[tsuki hao]

Yury G. Kudryashov said:

#new members, #general , or #maths (I can't formulate exact rules; we'll move if we think a thread is more appropriate in another stream)

Thank you very much!