## Stream: new members

### Topic: Substituting variable in lamda abstraction in goal

#### Saif Ghobash (Dec 30 2020 at 16:04):

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 (Dec 30 2020 at 16:05):

dsimp only

Thank you!

#### Kevin Buzzard (Dec 30 2020 at 16:26):

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

#### Johan Commelin (Dec 30 2020 at 16:30):

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

#### Johan Commelin (Dec 30 2020 at 16:30):

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

#### Saif Ghobash (Dec 30 2020 at 17:13):

@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 (Dec 30 2020 at 17:15):

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 (Dec 30 2020 at 17:17):

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.

@Saif Ghobash

#### Saif Ghobash (Dec 30 2020 at 17:19):

@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 (Dec 30 2020 at 17:20):

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

#### Kevin Buzzard (Dec 30 2020 at 17:21):

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

#### Bryan Gin-ge Chen (Dec 30 2020 at 17:22):

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

#### Kevin Buzzard (Dec 30 2020 at 17:23):

oh that's an interesting idea!

Last updated: May 10 2021 at 17:39 UTC