# Zulip Chat Archive

## Stream: maths

### Topic: Math education question (teaching textbook proofs in Lean)

#### Chris B (Oct 02 2019 at 18:58):

Hi. I'm from the computer science contingency of Lean users, but I'm going through 'Understanding Analysis' to try some very basic 'proper math' in Lean. Many of the proofs use arguments that are classics, but either aren't very Lean-friendly or aren't constructive. As an example, the proof of `irrat (sqrt 2)`

used in the book is the proof by contradiction/infinite descent.

Is the approach you guys have taken (or would take) for math education to say "Well here's how these are done in Lean/mathlib, the sooner you get used to doing things this way the better", or is it to try and power through the classic definitions in Lean? Or are you trying to give equal time to both approaches?

Thanks!

#### Chris Hughes (Oct 02 2019 at 19:21):

We certainly don't worry about being constructive. Usually

#### Chris Hughes (Oct 02 2019 at 19:23):

If something in mathlib differs from theclassical definition it's because it's in a greater generality, in which case the classical definition is better to formalize.

#### Johan Commelin (Oct 02 2019 at 19:40):

@Chris B What do you mean when you say "Many of the proofs ... either aren't very Lean-friendly"? If there are proofs in the library that can be optimized to become more Lean friendly, I think we very much welcome those.

#### Johan Commelin (Oct 02 2019 at 19:41):

Some of our contributors care more about being constructive than others. But in general, we unashamedly celebrate the axiom of choice.

#### Patrick Massot (Oct 02 2019 at 19:52):

Do you refer to https://www.amazon.com/Understanding-Analysis-Undergraduate-Texts-Mathematics/dp/1493927116?

#### Patrick Massot (Oct 02 2019 at 19:53):

Note that I don't understand your question either way.

#### Chris B (Oct 02 2019 at 19:55):

@Johan Commelin Sorry, I meant "the proofs in the textbook aren't always Lean-friendly" in that some of the things they take for granted don't seem trivial in Lean. I'm sure the ones in mathlib are great.

#### Patrick Massot (Oct 02 2019 at 19:58):

What is an example of a non-Lean friendly proof? I don't understand the issue with the irrationality of sqrt 2 example.

#### Johan Commelin (Oct 02 2019 at 19:58):

Aha... I see. And I'm sure there are also lots of proofs in mathlib that could be improved. But yes... most maths is not "designed to be formalised" to quote Mario out of context.

#### Chris B (Oct 02 2019 at 21:01):

@Patrick Massot Yes, that's the book. Maybe 'lean-aware' is a better choice of words than 'lean friendly'. The `irrat sqrt 2`

proof is simple, but it's not aware of the behavior/interaction between Lean's number types or the fact that rewriting terms in Lean is not always as easy as it is on paper, so as someone who's not super familiar with mathlib it's not trivial to recreate in terms of time and might end up brittle, ugly etc. On the other hand, there is also a definition of `irrat sqrt 2`

in mathlib that is different but was written by someone who IS aware of those things.

The question was whether educators who were using Lean and had a similar pair of proofs (one from mathlib and one from a textbook) were choosing to focus on one or the other.

#### Chris B (Oct 02 2019 at 21:03):

@Chris Hughes That's good to know going forward, thanks.

#### Patrick Massot (Oct 02 2019 at 21:26):

Maybe we should move this conversation to the "Lean for teaching" stream. When I use Lean for teaching I only use mathlib for its tactics and definition of real numbers. For instance I redefine limits of sequences and functions. I cannot expect my first year students to understand mathlib's use of filters and uniform spaces... This is the same reason we don't use Bourbaki for teaching. The good news is we can still use Lean (and mathlib tactics).

#### Chris B (Oct 02 2019 at 22:17):

Interesting, thanks for that insight.

#### Tim Daly (Oct 03 2019 at 02:37):

@Patrick Massot I understand, from a lecture by Kevin Buzzard, that you have written python code to convert lean-related material to an interactive webpage, a "literate form" of input involving latex. Where can I get this?

#### Jesse Michael Han (Oct 03 2019 at 03:18):

I believe it's https://github.com/leanprover-community/format_lean

#### Yufan Lou (Oct 17 2019 at 01:19):

@Patrick Massot

For instance I redefine limits of sequences and functions.

I want to show my friend in advanced calculus the power of LEAN but I haven't got the hang of it yet. Could you show me how you redefined the limits? Btw the theorem I am working on is

$\lim_{n\to\infty} C \cdot a_n = C \cdot \lim_{n\to\infty} a_n \text{ for } C \in \mathbb{R}$

#### Yufan Lou (Oct 17 2019 at 02:06):

I am trying to define it according to https://en.wikipedia.org/wiki/(%CE%B5,_%CE%B4)-definition_of_limit

#### Yufan Lou (Oct 17 2019 at 02:07):

But it involves an equation and I am kinda stuck on this

import data.real.basic def lim (x : ℝ) (c : ℝ) (f : ℝ → ℝ) : Prop := ∀ ε > 0, ∃ δ > 0, 0 < abs (x - c) < δ → abs (f x - )

#### Yufan Lou (Oct 17 2019 at 02:14):

Oh ok this seems to work

def lim (x : ℝ) (c : ℝ) (f : ℝ → ℝ) (L : ℝ) := ∀ ε > 0, ∃ δ > (0 : ℝ), 0 < abs (x - c) ∧ abs (x - c) < δ → abs (f x - L) < ε

#### Yufan Lou (Oct 17 2019 at 02:16):

lol how do I express infinity in this thing

#### Alex J. Best (Oct 17 2019 at 02:28):

There is a type `ennreal`

in mathlib that represents non-negative reals with a positive infinity, possibly this does what you want?

import data.real.ennreal open ennreal open_locale ennreal #check (∞ : ennreal)

#### Johan Commelin (Oct 17 2019 at 02:30):

@Yufan Lou There are two answers... the first (which is what mathlib does) is to step back, generalize everything and use so-called filters, instead of the epsilon-delta-sequence definition. The second would be to say that some statement is true for `x`

sufficiently close to infty, in other words, for `x`

sufficiently large.

#### Johan Commelin (Oct 17 2019 at 02:30):

Btw, the `0 < abs (x - c)`

doesn't seem very useful in your definition.

#### Johan Commelin (Oct 17 2019 at 02:31):

I personally don't think that using `ennreal`

would lead to a nice experience.

#### Johan Commelin (Oct 17 2019 at 02:33):

@Yufan Lou What do mathematicians actually mean when that say that `f`

has a limit as `x`

tends to infty? After all, they don't have $\infty \in \mathbb{R}$ either. So they must have explained somewhere what they mean when the abuse notation like this.

#### Yufan Lou (Oct 17 2019 at 02:37):

LOL That's a great question, but I don't have a mathematician around to ask

#### Yufan Lou (Oct 17 2019 at 02:38):

Oh wait there is a subsection defining the infinity case separately

#### Yufan Lou (Oct 17 2019 at 02:39):

Ah... that goes into metric space which I don't understand tho

#### Yufan Lou (Oct 17 2019 at 02:41):

The precise statement for limits at infinity is as follows:[16]

Suppose f is defined on a subset D of a metric space X with a metric d X ( x , y ) and maps into a metric space Y with a metric d Y ( x , y ) . Let L ∈ Y.

We say that

lim x → ∞ f ( x ) = L

if for every ε > 0 , there is a real number N > 0 such that there is an x ∈ D where d X ( x , 0 ) > N and such that if d X ( x , 0 ) > N and x ∈ D, then d Y ( f ( x ) , L ) < ε .

#### Yufan Lou (Oct 17 2019 at 02:42):

Ok metric space basically redefines absolute value aka "distance" right

#### Yufan Lou (Oct 17 2019 at 02:43):

if I only need real number I just replace d X with abs

#### Johan Commelin (Oct 17 2019 at 02:44):

Yep, that's right

#### Yufan Lou (Oct 17 2019 at 02:52):

Yeah!

def lim_inf (f : ℝ → ℝ) (L : ℝ) := ∀ ε > 0, ∃ N > (0 : ℝ), ∃ (x : ℝ) (H : abs (x - 0) > N), abs (f x - L) < ε

How to type the maths abs notation tho

#### Yufan Lou (Oct 17 2019 at 02:52):

Also wikipedia language so redundant

#### Johan Commelin (Oct 17 2019 at 02:53):

Try `\||`

I think

#### Yufan Lou (Oct 17 2019 at 02:56):

k

#### Johan Commelin (Oct 17 2019 at 02:56):

Btw, I think this is taking the limit at all infinities

#### Johan Commelin (Oct 17 2019 at 02:56):

You only want the positive one

#### Johan Commelin (Oct 17 2019 at 02:56):

In a general metric space you can't really talk of positive and negative infinity

#### Johan Commelin (Oct 17 2019 at 02:57):

But you want `x > N`

not `abs (x - 0) > N`

#### Yufan Lou (Oct 17 2019 at 02:57):

oh ok! thanks for simplifying :D

#### Yufan Lou (Oct 17 2019 at 02:59):

`\||`

gives me unexpected token tho

#### Yufan Lou (Oct 17 2019 at 03:00):

I still need the other abs right?

#### Johan Commelin (Oct 17 2019 at 03:06):

Search mathlib for `norm`

. You'll see the double-bar symbol show up a lot. But I forgot how to input it.

#### Yufan Lou (Oct 17 2019 at 03:06):

gotcha

#### Yufan Lou (Oct 17 2019 at 03:08):

I see it, it's the same, but I still get unexpected token

#### Yufan Lou (Oct 17 2019 at 03:08):

missing import?

#### Johan Commelin (Oct 17 2019 at 03:09):

Wouldn't think so...

#### Yufan Lou (Oct 17 2019 at 03:09):

also I cannot multiply a function directly with a real LOL

#### Johan Commelin (Oct 17 2019 at 03:10):

No... they are different things, right?

#### Johan Commelin (Oct 17 2019 at 03:10):

You can try `r \bu f`

#### Johan Commelin (Oct 17 2019 at 03:10):

Where `r`

is real and `f`

a function

#### Yufan Lou (Oct 17 2019 at 03:10):

I understand LOL just musing

#### Yufan Lou (Oct 17 2019 at 03:10):

oh! let me try

#### Johan Commelin (Oct 17 2019 at 03:11):

What does `example : normed_field real := by apply_instance`

give you? If it gives an error, then there is a missing import.

#### Yufan Lou (Oct 17 2019 at 03:12):

`unknown identifier 'normed_field'`

missing import it is

#### Johan Commelin (Oct 17 2019 at 03:12):

/me never really works with real numbers

#### Yufan Lou (Oct 17 2019 at 03:13):

`import analysis.normed_space.basic`

fixes it

#### Johan Commelin (Oct 17 2019 at 03:13):

Good

#### Yufan Lou (Oct 17 2019 at 03:14):

The name is kinda scary XD I hope it doesn't make proof harder to write

#### Johan Commelin (Oct 17 2019 at 03:15):

This is the line that you needed: https://github.com/leanprover-community/mathlib/blob/master/src/analysis/normed_space/basic.lean#L370

#### Johan Commelin (Oct 17 2019 at 03:15):

So that explains why the import fixes it

#### Yufan Lou (Oct 17 2019 at 03:15):

I see

#### Yufan Lou (Oct 17 2019 at 03:16):

Ahh I am getting `(deterministic) timeout`

on this theorem signature

example (a : ℝ → ℝ) (L : ℝ) (H : lim_inf a L) : ∀ (C : ℝ), lim_inf (C • a) (C * L) := sorry

#### Scott Morrison (Oct 17 2019 at 03:17):

Can you post a MWE (minimal working example, i.e. showing the imports) so someone can investigate for you?

#### Yufan Lou (Oct 17 2019 at 03:17):

$\lim_{n\to\infty} C \cdot a_n = C \cdot \lim_{n\to\infty} a_n \text{ for } C \in \mathbb{R}$

This was the theorem I was going for

#### Scott Morrison (Oct 17 2019 at 03:18):

I've never used this part of the library myself, but I do remember students seeing deterministic timeouts when working with normed_fields way too often, so it would be good to get to the bottom of this.

#### Scott Morrison (Oct 17 2019 at 03:18):

(I meant, show us exactly the code that produces the deterministic timeout, including the imports)

#### Yufan Lou (Oct 17 2019 at 03:18):

Ah, sorry, this is the code

import tactic.norm_num import data.real.basic import analysis.normed_space.basic def lim_inf (f : ℝ → ℝ) (L : ℝ) := ∀ ε > 0, ∃ N > (0 : ℝ), ∃ x > N, abs (f x - L) < ε example (a : ℝ → ℝ) (L : ℝ) (H : lim_inf a L) : ∀ (C : ℝ), lim_inf (C • a) (C * L) := sorry

#### Johan Commelin (Oct 17 2019 at 03:20):

@Yufan Lou What happens if you replace `C \bu a`

with `(\lambda x, C * a x)`

?

#### Yufan Lou (Oct 17 2019 at 03:21):

That fixes it

#### Scott Morrison (Oct 17 2019 at 03:23):

Doubling the timeout limit, it works, but is incredibly slow. :-(

#### Yufan Lou (Oct 17 2019 at 03:24):

:sweat: hopefully it's not something too complicated

#### Yufan Lou (Oct 17 2019 at 03:24):

meanwhile I'll continue with my proof I think

#### Yufan Lou (Oct 17 2019 at 03:31):

LOL how to prove `1 > 0`

#### Scott Morrison (Oct 17 2019 at 03:32):

@Yufan Lou , I posted an issue for you, I have to go soon but hopefully someone will sort it out: https://github.com/leanprover-community/mathlib/issues/1561

#### Scott Morrison (Oct 17 2019 at 03:32):

`by norm_num`

.

#### Yufan Lou (Oct 17 2019 at 03:33):

Ah Thank you!

#### Scott Morrison (Oct 17 2019 at 03:33):

Or `by linarith`

.

#### Scott Morrison (Oct 17 2019 at 03:33):

or `by simp`

:-)

#### Yufan Lou (Oct 17 2019 at 03:34):

How come I forgot `simp`

XD only tried `trivial`

#### Yufan Lou (Oct 17 2019 at 03:34):

Not trivial enough for Lean

#### Scott Morrison (Oct 17 2019 at 03:34):

(`simp`

can only handle the case in `nat`

; if you meant in the reals then use norm_num.)

#### Yufan Lou (Oct 17 2019 at 03:35):

Was about to say `simp`

gave me `0 < 1`

as a new goal LOL

#### Yufan Lou (Oct 17 2019 at 03:50):

Which tactic shall I use to factor `C * a 2 - C * L`

into `C * (a 2 - L)`

#### Yufan Lou (Oct 17 2019 at 03:57):

eh library_search to the rescue

#### Yufan Lou (Oct 17 2019 at 06:07):

ahhhh just realized this thing requires by case cuz C = 0 C not = 0

#### Johan Commelin (Oct 17 2019 at 06:11):

I can't parse the last part of your sentence

#### Yufan Lou (Oct 17 2019 at 06:14):

`by_cases C = 0 with Ceq0`

gives me `invalid 'begin-end' expression, ',' expected`

#### Yufan Lou (Oct 17 2019 at 06:16):

while `by_cases C = 0`

is fine

#### Johan Commelin (Oct 17 2019 at 06:16):

`by_cases hC : C = 0,`

#### Johan Commelin (Oct 17 2019 at 06:17):

Yeah, the syntax is not always uniform :sad:

#### Yufan Lou (Oct 17 2019 at 06:17):

Ah OK, that just means this needs update https://leanprover.github.io/reference/tactics.html#basic-tactics

#### Johan Commelin (Oct 17 2019 at 06:18):

Ok. @Jeremy Avigad :upper_right:

#### Floris van Doorn (Oct 17 2019 at 06:20):

As posted on the issue, the quick fix for the scalar multiplication is

import analysis.normed_space.basic attribute [instance, priority 900] algebra.has_scalar attribute [instance, priority 800] mul_action.to_has_scalar def lim_inf (f : ℝ → ℝ) (L : ℝ) := ∀ ε > 0, ∃ N > (0 : ℝ), ∃ x > N, abs (f x - L) < ε example (a : ℝ → ℝ) (L : ℝ) (H : lim_inf a L) : ∀ (C : ℝ), lim_inf (C • a) (C * L) := sorry

#### Yufan Lou (Oct 17 2019 at 06:25):

XD I see thanks

#### Yufan Lou (Oct 17 2019 at 06:31):

Well, thanks for the fix but the `C • a`

version feels at least 10x slower than than the lambda version

#### Yufan Lou (Oct 17 2019 at 06:31):

I am sticking with the lambda version for now

#### Yufan Lou (Oct 17 2019 at 07:17):

I need this lemma as my final step but I don't know how

example (C : ℝ) (x : ℝ) (ε : ℝ) (H : ε > 0) : ∥x∥ < ∥1 / C∥ * ε → ∥C∥ * ∥x∥ < ε := begin intros, simp at *, library_search end

#### Johan Commelin (Oct 17 2019 at 07:21):

Yeah, those things are really annoying

#### Johan Commelin (Oct 17 2019 at 07:22):

You'll need things like `norm_div`

and `norm_nonneg`

and `mul_lt_mul_left`

#### Yufan Lou (Oct 17 2019 at 07:27):

Hmm, let me try

#### Yufan Lou (Oct 17 2019 at 07:27):

What should I import

#### Johan Commelin (Oct 17 2019 at 07:27):

I would think most of those things are already there

#### Yufan Lou (Oct 17 2019 at 07:28):

huh, I have `import analysis.normed_space.basic`

but still `unknown identifier 'norm_div'`

#### Johan Commelin (Oct 17 2019 at 07:30):

`src/analysis/normed_space/basic.lean:@[simp] lemma norm_div {α : Type*} [normed_field α] (a b : α) : ∥a/b∥ = ∥a∥/∥b∥ :=`

#### Johan Commelin (Oct 17 2019 at 07:30):

You might need to prefix it with something

#### Johan Commelin (Oct 17 2019 at 07:30):

Or open a namespace

#### Yufan Lou (Oct 17 2019 at 07:30):

k

#### Johan Commelin (Oct 17 2019 at 07:30):

Are you using VScode?

#### Johan Commelin (Oct 17 2019 at 07:31):

If so, hit `Ctrl-P`

and then type `#norm_div`

. You'll likely see the full name of the lemma

#### Yufan Lou (Oct 17 2019 at 07:32):

found it, thank you!

#### Yufan Lou (Oct 17 2019 at 08:01):

OMGGGGG I actually finished this

#### Johan Commelin (Oct 17 2019 at 08:02):

Now go and read the wiki page on Stockholm syndrome

#### Yufan Lou (Oct 17 2019 at 08:03):

LOOOOOOOL

#### Yufan Lou (Oct 17 2019 at 08:07):

https://gist.github.com/louy2/4c5938960dd649d0e49aa53d3f56e07c

#### Yufan Lou (Oct 17 2019 at 08:08):

Comments welcome!

#### Kenny Lau (Oct 17 2019 at 08:22):

@Yufan Lou there is a proof without casing C=0

#### Kenny Lau (Oct 17 2019 at 08:25):

`let`

should be used when the object is not `Prop`

; otherwise use `have`

#### Yufan Lou (Oct 17 2019 at 08:31):

I chose `let`

where I couldn't figure out how to use `have`

#### Kenny Lau (Oct 17 2019 at 08:33):

theorem lim_inf_cons_mul_eq (a : ℝ → ℝ) (L : ℝ) (H : lim_inf a L) : ∀ (C : ℝ), lim_inf (λ x, C * a x) (C * L) := begin assume C : ℝ, unfold lim_inf at H ⊢, /- unfold definitions -/ assume (ε : ℝ) (Hε : ε > 0), by_cases HC : C = 0, { use [1, by norm_num], assume (x : ℝ) (Hx : x > 1), rw HC, /- ∥0 * a x - 0 * L∥ < ε -/ simpa using Hε }, { have HinvC : C⁻¹ ≠ 0, from inv_ne_zero HC, have HnC : ∥C⁻¹∥ > 0, from abs_pos_of_ne_zero HinvC, have HnCε : ∥C⁻¹∥ * ε > 0, from mul_pos' HnC Hε, specialize H (∥C⁻¹∥ * ε) HnCε, rcases H with ⟨N, HN, H⟩, use [N, HN], assume (x : ℝ) (Hx : x > N), specialize H x Hx, rw [← mul_sub, ← mul_lt_mul_left HnC, ← norm_mul, ← mul_assoc, inv_mul_cancel HC, one_mul], exact H } end

#### Yufan Lou (Oct 17 2019 at 08:36):

Ah! `specialize`

!

#### Yufan Lou (Oct 17 2019 at 08:37):

I fiddled with pattern matching for quite a while too... so `rcases`

is the answer

#### Yufan Lou (Oct 17 2019 at 08:37):

Thank you so much!

#### Johan Commelin (Oct 17 2019 at 08:48):

You can even merge those two lines if you want

#### Patrick Massot (Oct 17 2019 at 08:54):

What's the point of all these type ascriptions? Is it for readability?

#### Patrick Massot (Oct 17 2019 at 08:54):

Why specializing right before an exact?

#### Patrick Massot (Oct 17 2019 at 08:54):

Anyway, I did a quick compression pass, maybe you'll learn something by studying:

theorem lim_inf_cons_mul_eq (a : ℝ → ℝ) (L : ℝ) (H : lim_inf a L) : ∀ C, lim_inf (λ x, C * a x) (C * L) := begin intros C ε Hε, by_cases HC : C = 0, { use [1, by norm_num], intros, simpa [HC] using Hε }, { have HnC : ∥C⁻¹∥ > 0, from abs_pos_of_ne_zero (inv_ne_zero HC), have HnCε : ∥C⁻¹∥ * ε > 0, from mul_pos' HnC Hε, rcases H (∥C⁻¹∥ * ε) HnCε with ⟨N, HN, H⟩, use [N, HN], intros x Hx, rw [← mul_sub, ← mul_lt_mul_left HnC, ← norm_mul, ← mul_assoc, inv_mul_cancel HC, one_mul], exact H x Hx } end

#### Yufan Lou (Oct 17 2019 at 08:58):

Thanks! Yeah I had readability in mind. I want to share this with my maths friend and try to make it somewhat similar to what we would do by hand. So I wonder if the `rw`

at the end can be done with `calc`

.

#### Johan Commelin (Oct 17 2019 at 08:58):

@Yufan Lou In that case, you will love `show`

#### Johan Commelin (Oct 17 2019 at 08:59):

You can write `show this = what * the * goal looks like`

,

#### Yufan Lou (Oct 17 2019 at 08:59):

wow what LOL I couldn't tell what's different between `show`

and `have`

#### Johan Commelin (Oct 17 2019 at 09:00):

`have`

introduces a new assumption (but you have to prove it, of course)

#### Johan Commelin (Oct 17 2019 at 09:01):

`show`

restates the goal

#### Yufan Lou (Oct 17 2019 at 09:03):

Ahhhhhh I suspected that but didn't get it to work for some reason XD

#### Yufan Lou (Oct 17 2019 at 09:05):

"unification" :thinking: how far can I restate it

#### Yufan Lou (Oct 17 2019 at 09:05):

So far I have only read proofs where `show`

is at the end

#### Patrick Massot (Oct 17 2019 at 09:16):

Sure you can use a calc block, ending like

#### Patrick Massot (Oct 17 2019 at 09:16):

intros x Hx, calc ∥ C * a x - C * L∥ = ∥ C * (a x - L) ∥ : by rw mul_sub ... = ∥ C ∥ * ∥a x - L ∥ : norm_mul _ _ ... < ∥ C ∥ * (∥C⁻¹∥ * ε) : mul_lt_mul_of_pos_left (H x Hx) (abs_pos_of_ne_zero HC) ... = ε : by rw [← mul_assoc, ← norm_mul, mul_inv_cancel HC, norm_one, one_mul] }

#### Patrick Massot (Oct 17 2019 at 09:16):

or many variation, depending where you want to split steps.

#### Patrick Massot (Oct 17 2019 at 09:18):

But this is probably not so good if you want to impress people. Really Lean should need help in all those steps. Stating the steps is ok, by tactics should then crush the proofs. @Rob Lewis is that in scope for polya?

#### Yufan Lou (Oct 17 2019 at 09:34):

That's beautiful! Thank you! I can explain that Lean can help with all those, but I feel that without showing the steps my friends would just not know what Lean is doing.

#### Rob Lewis (Oct 17 2019 at 09:40):

Rob Lewis is that in scope for polya?

Depending what you have in the context, some of it is. But this looks primarily like a rewriting problem, not an arithmetic one.

#### Jeremy Avigad (Oct 17 2019 at 13:07):

@Johan Commelin @Yufan Lou I'll make the correction to the reference manual (I didn't think anyone was using it any more, but I guess people are still finding it). It may take a little while. I have lists of corrections to deal with for TPIL and Logic and Proof as well. I just need to find an afternoon to work through them all.

#### Kevin Buzzard (Oct 17 2019 at 22:10):

Thanks! Yeah I had readability in mind. I want to share this with my maths friend and try to make it somewhat similar to what we would do by hand. So I wonder if the

`rw`

at the end can be done with`calc`

.

@Yufan Lou if you want to make your code more appealing to your maths friends, you can try Patrick Massot's formatter. I used it to make this Lean proof of the sandwich theorem and I will be using it later on to make Lean notes for the course I am currently involved in. You click on stuff and it opens up Lean code -- click on the grey rectangles to view the tactic state at any point in the proof. In practice this just means adding a bunch of comments (in LaTeX) to your code.

Last updated: May 10 2021 at 08:14 UTC