# Zulip Chat Archive

## Stream: general

### Topic: function with random definition

#### Kevin Buzzard (Nov 02 2019 at 13:51):

import tactic.tauto /- f A → B g ↓ ↓ h C → D j -/ def random {A B C D : Type} (f : A → B) (g : A → C) (h : B → D) (j : C → D) : A → D := by tauto -- ! /- Solve the maze! (start here) -> [add two] -> (could go this way) ↓ ↓ (or this way) -> [add one] -> (get to here) -/ #eval random (λ x, x + 2) id id (λ x, x + 1) 0 -- random{1,2}

#### Mario Carneiro (Nov 02 2019 at 13:52):

it commutes!

#### Kevin Buzzard (Nov 02 2019 at 13:52):

It shouldn't do -- did I make an error?

#### Kevin Buzzard (Nov 02 2019 at 13:53):

These are types not props

#### Mario Carneiro (Nov 02 2019 at 13:54):

my mistake, I thought you used x+1+2 and x+2+1

#### Kevin Buzzard (Nov 02 2019 at 13:55):

rofl I just permuted the inputs and got it to give a different answer :D

#### Mario Carneiro (Nov 02 2019 at 13:55):

I don't think `tauto`

was designed for diagram chasing

#### Kevin Buzzard (Nov 02 2019 at 13:55):

I was overjoyed when I found that it did it!

#### Mario Carneiro (Nov 02 2019 at 13:55):

I think `solve_by_elim`

will do though

#### Kevin Buzzard (Nov 02 2019 at 13:56):

I'm making a whole bunch of definitions in tactic mode for the natural number game, and tauto is my big reveal like simp is for proving a+b+c+d+e=e+d+c+b+a

#### Kevin Buzzard (Nov 02 2019 at 13:57):

I am using these ideas to teach mathematicians about intro, apply, have and exact in a context where they are not freaking out about $P\implies Q$ being a function

#### Kevin Buzzard (Nov 02 2019 at 14:00):

We saw Antoine making a classic mathematician's error yesterday -- he had `f : X -> Y, A B : X, h : A = B, |- f A = f B`

and wanted to `rw f`

instead of `rw h`

. We can't tell the difference between = and -> in the sense that we do not look out carefully for it.

#### Kevin Buzzard (Nov 02 2019 at 14:01):

`rw`

does something which in the CS world is all very interesting and there's lots of theory and what have you, but to a mathematician a rewrite is an invisible step, because once A=B then A can be replaced by B at any stage in the future, immediately, and without question -- no justification needed.

#### Kevin Buzzard (Nov 02 2019 at 14:01):

so mathematicians know that `rw`

is for something something which isn't really there. And then if P implies Q and we know P then of course we know Q, that argument isn't really there either, it's just obvious from the logic

#### Mario Carneiro (Nov 02 2019 at 14:01):

not invisible exactly, mathematicians are familiar with equality chains

#### Kevin Buzzard (Nov 02 2019 at 14:01):

so it must be `rw`

as well.

#### Kevin Buzzard (Nov 02 2019 at 14:02):

Yes, and we're familiar with implies chains.

#### Kevin Buzzard (Nov 02 2019 at 14:02):

But when you *watch mathematicians doing mathematics* they write chains of arguments, and sometimes they're rewriting = and sometimes they're applying P -> Q and both of these (completely different) things are just so completely embedded in a mathematician that they find it hard to tell them apart, they're just both doing something trivial and obvious

#### Kevin Buzzard (Nov 02 2019 at 14:04):

I have this every year with schoolkids, they show up here and I ask them to prove $\sqrt{2}+\sqrt{6}<\sqrt{15}$ and they just square both sides, press on, end up deducing 48<49, say this is true so they're done, and *they don't even write the connector from each line to the next*. They are not trained to do this at school.

#### Kevin Buzzard (Nov 02 2019 at 14:05):

At school, they are given an equation and told to prove another equation, and they do it using three rewrites, each of which generates a new equation, and I've looked at the mark sheets for these things because my sons have been doing them and the mark scheme is "one point for each of the intermediate equations". No mention at all of the underlying logic.

#### Kevin Buzzard (Nov 02 2019 at 14:06):

And similarly they might be asked to prove P -> Q and they prove P -> A -> B -> C -> Q and they get one point for each of A, B, C so *they just write "P, A, B, C, Q, done" and get full marks

#### Kevin Buzzard (Nov 02 2019 at 14:06):

and then they show up at Imperial with top marks for their school exams and they don't know the difference between P -> Q and P = Q.

#### Kevin Buzzard (Nov 02 2019 at 20:06):

I think

`solve_by_elim`

will do though

OK so I can't get anything to work for this one:

example (A B C D E F G H I J K L : Type) (f1 : A → B) (f2 : B → E) (f3 : E → D) (f4 : D → A) (f5 : E → F) (f6 : F → C) (f7 : B → C) (f8 : F → G) (f9 : G → J) (f10 : I → J) (f11 : J → I) (f12 : I → H) (f13 : E → H) (f14 : H → K) (f15 : I → L) : A → L := begin intro a, apply f15, apply f11, apply f9, apply f8, apply f5, apply f2, apply f1, assumption, end

Is there one tactic which solves this example? I'm happy to put move everything before or after the colon if it helps. I couldn't get either `tauto`

or `solve_by_elim`

to work. Note: they are types not props.

#### Kevin Buzzard (Nov 02 2019 at 20:07):

It's just a maze. There a some loops (e.g. f1,f2,f3,f4)

#### Kevin Buzzard (Nov 02 2019 at 20:09):

Oh I've just noticed that I can't even solve it if I change them all to Props! `tauto!`

just sits there, `tauto`

fails, `solve_by_elim`

fails :-/

#### Bryan Gin-ge Chen (Nov 02 2019 at 20:19):

How about this?

import tactic.basic example (A B C D E F G H I J K L : Type) (f1 : A → B) (f2 : B → E) (f3 : E → D) (f4 : D → A) (f5 : E → F) (f6 : F → C) (f7 : B → C) (f8 : F → G) (f9 : G → J) (f10 : I → J) (f11 : J → I) (f12 : I → H) (f13 : E → H) (f14 : H → K) (f15 : I → L) : A → L := begin intro a, repeat {assumption <|> apply_assumption}, end

#### Kevin Buzzard (Nov 02 2019 at 20:21):

I am pretty sure that if I permute f1-f15 then you will get lost.

#### Kevin Buzzard (Nov 02 2019 at 20:22):

And if that's not true then I'm pretty sure I could generate a level which was solvable but for which this tactic wouldn't work.

#### Kevin Buzzard (Nov 02 2019 at 20:23):

What do I need? a SAT solver? An SMT solver? I am just indicating how clueless I am here.

#### Kevin Buzzard (Nov 02 2019 at 20:23):

An ATP? How do I solve it in Isabelle?

#### Kevin Buzzard (Nov 02 2019 at 20:25):

Current version of challenge:

example (A B C D E F G H I J K L : Type) (f_for_Bryan : L → L) (f1 : A → B) (f2 : B → E) (f3 : E → D) (f4 : D → A) (f5 : E → F) (f6 : F → C) (f7 : B → C) (f8 : F → G) (f9 : G → J) (f10 : I → J) (f11 : J → I) (f12 : I → H) (f13 : E → H) (f14 : H → K) (f15 : I → L) : A → L := begin intro a, repeat {assumption <|> apply_assumption}, -- hangs forever end

#### Kevin Buzzard (Nov 02 2019 at 20:26):

I will grudgingly accept one-tactic answer which works for Props only, and I'm happy with intros or reverts before the tactic.

#### Bryan Gin-ge Chen (Nov 02 2019 at 20:35):

Not quite the same thing, but I think `tfae`

is supposed to do something like this to prove `iff`

s. There are some tests in @Simon Hudon's PR #1600 for `tfae`

which are kind of reminiscent of your examples.

Presumably someone well-versed in the mysteries of meta code could write something like Dijkstra's algorithm or some other pathfinding algorithm for these challenges?

#### Kevin Buzzard (Nov 02 2019 at 20:44):

`cc`

works for Props. Feature request: make `cc`

work for types :D

#### Jesse Michael Han (Nov 02 2019 at 20:49):

you could hack it by using `cc`

to find a proof for the `nonempty`

versions of your hypotheses, then fold over the proof to figure out how to produce the required term

#### Kevin Buzzard (Nov 02 2019 at 20:57):

that might be asking a bit much for my users :D They've only just learnt `apply`

#### Antoine Chambert-Loir (Nov 02 2019 at 21:39):

What puzzled me (and still puzzles me) in the way tactics are taught in the natural number game is that I did not understand precisely on what expression they act and by what kind of magic they progressively build a term of the correct type.

#### Kevin Buzzard (Nov 02 2019 at 21:44):

I am teaching it in a completely different way to Theorem Proving In Lean, just for an experiment really. Computer scientists are terrified by `rw`

because it is a very complex tactic, replacing entire subterms of a term by other subterms whilst trying to remain consistent and typecheck. On the other hand if a mathematician knows A=B then they can just change every A to a B without even feeling like they are doing anything.

#### Kevin Buzzard (Nov 02 2019 at 21:45):

`rw`

always acts on the goal. Should I say this more explicitly? I must say Antoine, your feedback has been invaluable so far, because I know I can trust you as a mathematician, so if you find something difficult I can be confident that you understand the mathematics and the problem is the explanation.

#### Bryan Gin-ge Chen (Nov 02 2019 at 22:06):

I did not understand precisely on what expression [tactics] act and by what kind of magic they progressively build a term of the correct type.

This is not something I understand too well either, but let me try anyway. Tactics operate on the "tactic state", which includes:

- the "environment" (containing all declarations like `def`

and `theorem`

),

- the "local context" (containing a list of the hypotheses available in the current proof), and

- all current goals.

All this state is wrapped in some functional programming construct called a "monad" (which allows for e.g. backtracking and error-handling) to make it convenient to manipulate via Lean code (tactics are "just" functions involving this "tactic monad").

For more info, there's the tactic writing tutorial in the mathlib docs with pointers to some more sources.

#### Kevin Buzzard (Nov 02 2019 at 23:06):

Ha ha so one answer to Antoine's question is that it all works via the magic of category theory

#### tirima (Nov 02 2019 at 23:16):

World 4, level 8 in 25 `rw`

instead of 27:

rw one_eq_succ_zero, rw pow_succ, rw pow_succ, rw pow_succ, rw pow_succ, rw pow_succ, rw pow_succ, rw pow_zero, rw pow_zero, rw pow_zero, rw one_mul, rw one_mul, rw one_mul, rw mul_add, rw add_mul, rw add_mul, rw mul_comm b, rw add_assoc, rw ← add_assoc (a*b), rw succ_mul, rw ←one_eq_succ_zero, rw one_mul, rw add_mul, rw add_assoc (a*a), rw add_comm (b*b),

#### Scott Morrison (Nov 09 2019 at 00:06):

We really need to get `rewrite_search`

into mathlib... :-)

#### Kevin Buzzard (Nov 09 2019 at 07:15):

Isn't this `simp`

?

#### Sebastian Ullrich (Nov 09 2019 at 11:16):

Am I doing this right? 3fsdr0.jpg

#### Sebastian Ullrich (Nov 09 2019 at 11:17):

(No, I don't think I am...)

#### Kevin Buzzard (Nov 09 2019 at 11:38):

`simp`

is magic as far as I am concerned. I know that in the case above it's `ring`

I need, but that's because I read the spoiler on Twitter

#### Kevin Buzzard (Nov 09 2019 at 11:40):

I remember Patrick a while ago saying "ha ha I remember the days when I just tried `simp`

on every goal" and I'm like "yeah, that's me now"

#### Kevin Buzzard (Nov 09 2019 at 11:40):

I remember when someone told me that it worked best on equalities. That was a big step forward.

#### Bryan Gin-ge Chen (Nov 09 2019 at 14:55):

The first proof I wrote for that one used `simp`

:

lemma add_squared (a b : mynat) : (a + b) ^ (succ(1)) = a ^ (succ(1)) + b^(succ(1)) + (succ(1))*a*b := begin simp [pow_succ, pow_one, mul_add, succ_mul], end

Then I read the twitter stuff and thought that maybe `simp`

was against the spirit of the question or something so I tried again.

`simp`

is magic as far as I am concerned.

Didn't you just say "we don't have tactics sophisticated enough to be called black boxes" ? :stuck_out_tongue_wink:

#### Kevin Buzzard (Nov 09 2019 at 17:41):

Ha ha, you are absolutely right :D I guess I was thinking more about "mathematical" tactics, like `ring`

, `linarith`

and `norm_num`

. Whilst of course I could never have written any of these myself, the *mathematical* jobs they achieve are exactly the sort of things which mathematicians (e.g. by the time they arrive at my university) are told are "trivial". To put it another way, these complicated tactics fill in gaps which mathematicians are under no obligation to justify on paper: "One readily checks that $(aX+bY+cX^2+dY^3)*(eX^2+f+gY)=aeX^3+\cdots$", etc. All of `simp`

, `tauto`

, `cc`

, `finish`

, `abel`

, `omega`

or whatever are black magic in the sense that I don't know the algorithms they're using, all I know is that they sometimes work for me.

I guess this leads to a more general point. Part of the reason I have no idea what `cc`

does is that the documentation, "Tries to prove the main goal using congruence closure", means absolutely nothing to me (and probably to most mathematicians). All the tactics which I do think of as black boxes -- perhaps there should be examples of the kind of question they are expected to solve somewhere? My own personal documentation for `simp`

is "tries to prove X=Y by randomly rewriting results of the form A=B which have been tagged with `simp`

". I have no idea what the strategy is but at least it felt like an insight when I realised that this was what it was doing.

#### Bryan Gin-ge Chen (Nov 09 2019 at 18:53):

I do think the question of what counts as "trivial" (and how far we are from being able to do trivial things trivially in Lean+mathlib) is very interesting. But that probably deserves its own topic.

On your second paragraph: the mathlib tactics have pretty good docs all in one place here (it looks like they mostly have examples, too). We should probably add links to the "extra" doc page you wrote for `simp`

and the one Patrick wrote for `cc`

, since those are a bit harder to find.

#### Nish (Jun 21 2020 at 05:06):

Improved to 19 (we were supposed to have access to `two_eq_succ_one`

, right?)

```
rw two_eq_succ_one,
rw pow_succ,
rw pow_succ,
rw pow_succ,
rw pow_one,
rw pow_one,
rw pow_one,
rw succ_mul,
rw one_mul,
rw add_mul,
rw add_mul,
rw mul_add,
rw mul_add,
rw mul_comm b a,
rw add_assoc,
rw add_assoc,
rw add_comm (a * b) (b * b),
rw ← add_assoc (a * b) (b * b) (a * b),
rw add_comm (a * b) (b * b),
rw add_assoc (b * b) (a * b) (a * b),
refl,
```

#### David Chew (Jun 21 2020 at 13:25):

20 steps with only auto selection, to match @Nish (I counted 20 steps in theirs)

```
rw add_comm,
rw two_eq_succ_one,
rw pow_succ,
rw pow_succ,
rw pow_succ,
rw pow_one,
rw pow_one,
rw pow_one,
rw mul_add,
rw succ_mul,
rw one_mul,
rw add_mul,
rw add_mul,
rw add_mul,
rw add_assoc,
rw add_comm,
rw mul_comm,
rw ← add_assoc,
rw add_assoc,
rw add_comm,
refl,
```

#### David Chew (Jun 21 2020 at 13:35):

Improved to 19 steps

```
rw add_comm,
rw two_eq_succ_one,
rw pow_succ,
rw pow_succ,
rw pow_succ,
rw pow_one,
rw pow_one,
rw pow_one,
rw mul_add,
rw succ_mul,
rw one_mul,
rw add_mul,
rw add_mul,
rw add_mul,
rw mul_comm a b,
rw ← add_assoc,
rw add_comm,
rw add_assoc,
rw ← add_assoc,
refl,
```

#### Kevin Buzzard (Jun 21 2020 at 13:53):

now can you prove you can't do it in 18? ;-)

#### Learning Balance (Jul 02 2020 at 08:19):

Kevin Buzzard said:

now can you prove you can't do it in 18? ;-)

This would suggest you can't prove such a thing. ;-)

```
rw add_right_comm,
rw two_eq_succ_one,
rw succ_mul,
rw pow_succ,
rw add_mul,
rw ← add_assoc,
rw pow_succ,
rw pow_one,
rw pow_one,
rw one_mul,
rw ← mul_add,
rw pow_succ,
rw pow_one,
rw add_mul,
rw mul_add b a b,
rw add_assoc,
rw mul_comm a b,
refl,
```

#### Kevin Buzzard (Jul 02 2020 at 08:26):

It's like the Rubik's cube

#### John Cremona (Jul 06 2020 at 09:44):

I did this in 21, and I'm only a couple of days into all this:

rw two_eq_succ_one,

rw pow_succ,

rw pow_succ,

rw pow_succ,

rw pow_one,

rw pow_one,

rw pow_one,

rw succ_eq_add_one,

rw add_mul,

rw add_mul,

rw one_mul,

rw add_mul,

rw mul_add,

rw mul_add,

rw add_right_comm,

rw add_comm (b*a),

rw mul_comm b a,

rw add_assoc (a*a),

rw add_assoc (a*a),

rw add_assoc (b*b),

refl,

#### Johan Commelin (Jul 06 2020 at 09:51):

@John Cremona Welcome!

(Note that you can use #backticks to get syntax highlighting of the code.)

#### Kevin Buzzard (Jul 06 2020 at 10:04):

@John Cremona I remember you mentioning to me a couple of years ago that you had embarked upon a proof from first principles that given $g\in G$ ($G$ a group), the map from $\mathbb{Z}$ to $G$ sending $n$ to $g^n$ was a group homomorphism, and that it had been much more painful than you had expected. Me and some young mathematicians were working on this last Thursday at Xena and came up with a much more conceptual proof, involving first defining a function which given a bijection $A\to A$ and an integer $n$ returns the $$n$$th iterate of this bijection; we proved $$f^{[n+m]=f^{[n]}\circ f^{[m]}$$ by some sort of general induction principle we had lying around. Having set up the basic API for this function we could do stuff like the group theory question easily. I mention all this because as I'm sure you know, you can solve the level above very quickly with `ring`

, although I think that trying to figure out the actual minimum number of moves might be a hard problem.

#### John Cremona (Jul 06 2020 at 10:06):

You are wrong in saying that I know how to solve this in any other way! I know precisely 0 beyind what I have learned so far in the Natural Number Game, and I have not finished that yet.

#### John Cremona (Jul 06 2020 at 10:09):

By the way, I think the list of streams in this zulip chat is totally chaotic and unhelpful, e.g. the vast number of subtopics under "new members" most of which are not at all suitable reading for newbies. For a start it would be good to have a thread for beginners' help specifically for the Natural Number Game where any replies of the form "all you need to do is <something more advanced than has so far been introduced in the NNG>" is banned.

#### Scott Morrison (Jul 06 2020 at 10:23):

You're certainly right that we should try to move some of the traffic in "new members" out to the other streams.

#### Alex J. Best (Jul 06 2020 at 10:39):

Maybe we should replace it with a "Getting started" or "First proofs in lean" stream, I think half the problem is that a lot of people self-identify as "new members" even if they've used lean for quite a while and therefore post questions in there that are really quite advanced.

#### Johan Commelin (Jul 06 2020 at 10:47):

Proposal:

`introductions`

: people write a short intro, other people say hi and welcome.`getting started`

: questions by people who just started using lean; answers shouldn't assume anything advanced`new members`

get's banned, because it currently is one big grabbag.

We could even add a dedicated `natural number game`

stream, if people like this.

#### Kenny Lau (Jul 06 2020 at 10:58):

what's the difference between 2 and 3

#### John Cremona (Jul 06 2020 at 10:58):

Certainly at the moment I feel much too intimidated to ask for any help since I'm sure the answers are all obvious. In fact so far I have come up with the answers myself (after a while) and then they seem obvious to me too. Usually.

#### Alex J. Best (Jul 06 2020 at 11:07):

@John Cremona don't feel any pressure to do this, this community really is very question friendly! Maybe because lean still pretty new and comparatively small scale a lot of answers to basic questions just aren't out there in an easy to find manner, so asking here is really the quickest way to go, and there are lots of people happy to answer "obvious" questions.

#### Johan Commelin (Jul 06 2020 at 11:39):

@John Cremona I will echo what Alex said. If you want an answer fast, just ask. There is soooo much new stuff that you need to wrap your head around, and usually there will be someone that can answer your question in 5 minutes, and it takes them 10 seconds, whereas it might take a newcomer 5 hours to figure it out alone...

#### Johan Commelin (Jul 06 2020 at 11:40):

So, we love to answer easy questions.

#### Gunjeet Singh (Jul 16 2020 at 07:48):

i did that Boss_Boss Power level in 20 steps... will try further to get it to 18 (if that's even possible :)

rw two_eq_succ_one,

rw pow_succ,

rw pow_succ,

rw pow_succ,

rw mul_assoc (succ 1) a b,

rw succ_mul,

rw one_mul,

rw pow_one,

rw pow_one,

rw pow_one,

rw mul_add,

rw add_mul,

rw add_mul,

rw add_comm (a*b) (b*b),

rw add_assoc (a*a) ,

rw ← add_assoc (b*a),

rw add_comm (b*a),

rw add_assoc (b*b),

rw ← add_assoc(a*a),

rw add_comm (b*a) (a*b),

refl,

#### Kenny Lau (Jul 16 2020 at 08:01):

#### Julian Berman (Jul 22 2020 at 22:19):

Kevin Buzzard said:

I remember Patrick a while ago saying "ha ha I remember the days when I just tried

`simp`

on every goal" and I'm like "yeah, that's me now"

I'm here from the future as a new user just going over the number game tut again and this line speaks to me (especially considering how many times out of laziness I just typed it into this same exercise just to have it lazily sort the terms for me)

#### Kevin Buzzard (Jul 22 2020 at 23:00):

I made a bad job of that whole `simp`

stuff. If you play the complex number game you'll see me explaining `simp`

much better.

#### PsyMar#2210 (Feb 09 2021 at 14:31):

Got it in 17 rws. took about... 5-10 minutes, though my hungry cat says longer.

rw two_eq_succ_one,

rw pow_succ,

rw pow_succ,

rw pow_succ,

rw succ_mul,

rw pow_one,

rw pow_one,

rw pow_one,

rw one_mul,

rw add_mul,

rw mul_add,

rw mul_add,

rw mul_comm b a,

rw ← add_assoc,

rw add_right_comm (a * a) (b * b) ((a + a) * b),

rw add_mul,

rw ← add_assoc,

refl,

#### Kevin Buzzard (Feb 09 2021 at 15:11):

Nice!

#### Michael (Aug 03 2021 at 13:23):

Hello, I have just started the natural number game today and I have managed World 4, Level 8 in 19 `rw`

:

```
rw two_eq_succ_one,
rw pow_succ,
rw pow_one,
rw pow_succ,
rw pow_one,
rw pow_succ,
rw pow_one,
rw succ_mul,
rw one_mul,
rw mul_add,
rw add_mul,
rw add_mul,
rw add_mul,
rw add_assoc,
rw add_comm (a * b) (b * b),
rw add_comm (b * a),
rw add_assoc,
rw mul_comm b a,
rw add_assoc,
refl,
```

I have seen in the thread that someone else has managed this too but I thought I would share my proof anyway.

#### Kevin Buzzard (Aug 03 2021 at 17:41):

I should have a leaderboard :-) Well done!

#### Anindya Banerjee (Aug 04 2021 at 20:03):

Hello, I started the natural number game recently and thus far have managed to work up to Power World. I wonder about the following solution to Power World, Level 8:

rw two_eq_succ_one,

rw pow_succ,

repeat {rw pow_one},

rw mul_add,

repeat {rw pow_succ},

repeat {rw pow_one},

ring,

I must admit that I don't understand the very last step ("ring") in the proof, although Lean seems to accept it.

Thanks in advance for any suggestions.

#### Eric Rodriguez (Aug 04 2021 at 20:15):

`ring`

is a tactic that solves goals that are true in all (commutative?) rings, and the goal at the end is one of those things

#### Anindya Banerjee (Aug 04 2021 at 20:34):

Thank you.

I have another question with Level 9 of Function World, for which my attempt is:

intros a:A, have b:=f1 a, have e:=f2 b, have f:=f5 e,

have g:=f8 f, have j:=f9 g, have i:=f11 j,

apply f15, exact i,

Here Lean reports:

26:19: goal

no goals

and

24:8: error:

invalid 'begin-end' expression, ',' expected

24:12: error:

sync

I am trying to understand the error.

Thanks in advance.

#### Eric Rodriguez (Aug 04 2021 at 20:57):

the error is the fact you said `intros a:A`

instead of just `intros a`

. as Lean knows that the next thing you're `intro`

ing, there's no need to tell it what type it is; it'll figure it out for you, and therefore the tactic gets confused as to why you're trying to tell it.

#### Eric Rodriguez (Aug 04 2021 at 20:58):

(this isn't always true - sometimes you will want to say, but it's true in most cases)

#### xp2_882030kgz010602 (Apr 24 2022 at 15:23):

I somehow got 18 rewrites. I wasn't even trying for a record.

```
rw two_eq_succ_one,
rw pow_succ,
rw pow_succ,
rw pow_succ,
rw pow_one,
rw pow_one,
rw pow_one,
rw succ_mul,
rw one_mul,
rw mul_add,
rw add_mul,
rw add_mul,
rw add_mul,
rw add_assoc,
rw add_assoc,
rw mul_comm b,
rw add_comm (b*b) (a*b+a*b),
rw ←add_assoc (a*b),
refl,
```

#### Aaron Bies (Apr 24 2022 at 17:21):

I had not realized you can define functions in tactic mode and it actually tells you your assumptions and goals

This is the funniest thing to me, more programming languages should do this

#### Aaron Bies (Apr 24 2022 at 18:19):

I understand why this works, but it still feels illegal

```
def what {α β γ : Type} (f : α → β) (g : β → γ) (x : α) : γ :=
by solve_by_elim
```

#### Jason Rute (Apr 24 2022 at 21:33):

Aaron, even without tactic mode, if you use an underscore for each yet-to-be-written term, you can get the same effect in term mode (i.e. having Lean tell you your goals and assumptions). Every functional language should have a language server which does this!

#### Kyle Miller (Apr 24 2022 at 21:59):

Lean also has "holes".

```
def what {α β γ : Type} (f : α → β) (g : β → γ) (x : α) : γ := {! !}
```

Try doing the "use `library_search`

to complete the goal" hole command.

#### Tariq Erwa (Apr 28 2022 at 12:32):

My attempt at Power World level 8 @ 25 rewrites

```
rw two_eq_succ_one,
rw pow_succ,
rw pow_one,
rw mul_add,
rw add_mul,
rw add_assoc,
rw add_comm,
rw add_mul,
rw ← add_assoc,
rw ← mul_one (b*a),
rw mul_comm b a,
rw add_assoc,
rw add_comm,
rw ← mul_succ,
rw mul_comm (a*b) (succ 1),
rw ← add_comm (a*a) (b*b),
rw ← pow_one a,
rw ← pow_one b,
rw ← pow_add a 1 1,
rw ← pow_add b 1 1,
rw ← succ_eq_add_one,
rw pow_one,
rw pow_one,
rw ← mul_assoc,
rw ← two_eq_succ_one,
refl,
```

#### Omar Hidmi (Oct 04 2022 at 13:13):

My answer to Power world level 8 in 15 rows:

rw two_eq_succ_one,

rw one_eq_succ_zero,

repeat {rw pow_succ},

repeat {rw pow_one},

rw succ_mul,

repeat {rw pow_zero},

repeat {rw one_mul},

rw mul_add,

repeat {rw add_mul},

repeat {rw add_assoc},

rw mul_comm b,

rw succ_mul,

rw zero_mul,

rw zero_add,

simp,

#### Sergey Kaunov (Feb 03 2023 at 07:11):

just wanted to share my solution, but looks like I'm a cheater...

```
rw two_eq_succ_one,
rw one_eq_succ_zero,
repeat {rw pow_succ},
repeat {rw pow_zero}, simp,
rw mul_add, rw add_mul, simp, repeat {rw ← add_assoc}, repeat {rw mul_add},
repeat {rw ← one_eq_succ_zero}, rw succ_eq_add_one, repeat {rw mul_add}, repeat {rw mul_one},
repeat {rw ← add_assoc},
simp,
```

#### Kevin Buzzard (Feb 03 2023 at 08:17):

`simp`

is probably doing several rewrites at once

Last updated: Aug 03 2023 at 10:10 UTC