typing superscripts

Stream: new members

[Notification Bot]

This topic was moved to #mathlib4 > A problem with lean by Floris van Doorn.

[tsuki hao]

Does anyone know how to input the superscript in lean?

[Johan Commelin]

You can write things like \^2

[tsuki hao]

Johan Commelin said:

You can write things like \^2

Thank you very much!

[tsuki hao]

'''
variable (a b c d e : ℝ )
example (h₀ : a ≤ b)(h₁ : b < c) (h₂ : c ≤ d) (h₃ : d < e) : a < e := by
apply lt_of_le_of_lt h₀
apply lt_of_lt_of_le h₁
apply le_trans h₂
apply le_refl
'''
Can someone tell me what should be written next for this code

[Martin Dvořák]

If you call exact? aka library_search it will give you that you can complete your proof by exact le_of_lt h₃ instead of your last line.
PS: When posting #mwe you should provide all imports and use #backticks instead of quotation marks.

[tsuki hao]

Martin Dvořák said:

If you do library_search it will give you that you can finish your proof by exact le_of_lt h₃ instead of your last line.
PS: When posting #mwe you should provide all imports and use #backticks instead of quotation marks.

Thanks for your help, I have solved this problem!

[tsuki hao]

'''
example (h : 1 ≤ a) (h' : b ≤ c) : 2 + a + exp b ≤ 3 * a + exp c := by
linarith [exp_le_exp.mpr h']
'''
I wrote this code according to the instructions on mathematics in lean, but it shows 'unknown identifier 'exp_le_exp.mpr', is it because I did not import a certain package?

[Scott Morrison]

@tsuki hao, you need to use #backticks in order to have readable code blocks, and you need to provide all the imports you are using, as per the instructions in #mwe.

[Scott Morrison]

The point is that to help you, we want to be able to copy and paste the code you provide into a new file, and immediately see the same error message as you are seeing.

[Eric Wieser]

It looks like you confused the backtick character, ` , with the single quote character, '