Substituting variable in lamda abstraction in goal

Stream: new members

[Saif Ghobash]

I have the following hypothesis and goal,

1 goal
ω: ℚ
hωpos: ω > 0
N: ℕ
H1_h: 1 / ω < ↑N
n: ℕ
hnN: n > N
⊢ abs ((λ (n : ℕ), 1 / ↑n) n) < ω

I would like to substitute the n in the lambda abstraction with the n in my hypothesis

[Adam Topaz]

dsimp only

[Saif Ghobash]

Thank you!

[Kevin Buzzard]

I am always embarrassed by how difficult it is to prove that 1/n tends to 0 from first principles in Lean :-)

[Johan Commelin]

@Saif Ghobash Are writing some form of lecture notes accompanied by Lean proofs?

[Johan Commelin]

If so, you might be interested in lean_formatter and possibly also the framework used by "Mathematics in Lean".

[Saif Ghobash]

@Johan Commelin I am an undergraduate rewriting my professors lecture notes in lean as a way to learn lean and study for my real analysis finals. :smile:

[Kevin Buzzard]

That's a great way to do it. You should make a little repo where you put up stuff. I was working on some undergraduate problem sheets for analysis with some Imperial first year undergraduates -- I wasn't teaching the course, we were just goofing around. https://github.com/ImperialCollegeLondon/M40002

[Kevin Buzzard]

You should just make a github project for your class, with mathlib as a dependency, and then within src set up a nice directory structure (lectures, problem sheets, exam questions, whatever) and start dumping Lean files in the directories and showing other kids in your class. Explain in your README how to install your project (just copy what I wrote mutatis mutandis) and see if other people contribute.

[Kevin Buzzard]

@Saif Ghobash

[Saif Ghobash]

@Kevin Buzzard I might just do that, it was actually a lot of your posts on the Xena website that made me want to get into Lean in the first place :smiley: , the website has been a fantastic resource

[Kevin Buzzard]

let me know what you want me to write about. I've been neglecting it recently.

[Kevin Buzzard]

I've got a deadline of NYE to submit a paper but can think about a new year post

[Bryan Gin-ge Chen]

Since you've been working on some mathlib PRs recently, maybe you could write about one of those?

[Kevin Buzzard]

oh that's an interesting idea!