## Stream: new members

### Topic: real.exp_log

#### Jalex Stark (Apr 30 2020 at 14:47):

I feel like this error message is telling me that the elaborator can't unify \R with \R:

import analysis.calculus.specific_functions

example (x : ℝ) (hx : 0 < x) : real.log x < x := begin
suffices key : real.log x < real.exp (real.log x),
rw real.exp_log hx,
end


(edited to make the error a bit more explicit)

#### Kevin Buzzard (Apr 30 2020 at 14:52):

I think it's OK, the LHS of real.exp_log hx is real.exp (real.log x) and it can't find it in your goal (because the goal is real.log x < x)

#### Kevin Buzzard (Apr 30 2020 at 14:52):

The suffices puts the new goal key at the end, not the start, so the rewrite is still trying to work on real.log x < x (and I think rw only works on the first goal)

#### Jalex Stark (Apr 30 2020 at 14:53):

oof, thanks. maybe i need more coffee

#### Kevin Buzzard (Apr 30 2020 at 14:53):

  suffices key : real.log x < real.exp (real.log x),
{ rwa real.exp_log hx at key},


#### Kevin Buzzard (Apr 30 2020 at 14:54):

I always think it's a bit dirty using rwa like that.

#### Jalex Stark (Apr 30 2020 at 14:55):

because the rw and the a get applied in different places?

right :-)

#### Kevin Buzzard (Apr 30 2020 at 14:55):

but it's perfectly fine Lean code

#### Kevin Buzzard (Apr 30 2020 at 14:55):

Maybe sneaky is a better word :-)

#### Jalex Stark (Apr 30 2020 at 14:56):

yeah i agree that its better than rw ... at key, exact key  which appears too many times in my codewars solutions

#### Jalex Stark (Apr 30 2020 at 14:56):

i think i forgot about rwa when I went through a phase of leaning on nonterminal simps

#### Mario Carneiro (Apr 30 2020 at 15:07):

I think that a "dirty" use of rwa thm at h would be if the assumption being referred to is not the rewritten h

#### Patrick Massot (Apr 30 2020 at 15:08):

I thought this is what they meant.

#### Patrick Massot (Apr 30 2020 at 15:08):

How can you have a dirty rwa otherwise?

#### Mario Carneiro (Apr 30 2020 at 15:09):

example (red herring : ℕ) (h : red = 0) (h2 : red = herring) : red = 0 :=
by rwa h at h2


#### Reid Barton (Apr 30 2020 at 15:10):

Then the rw part would be useless, right?

#### Mario Carneiro (Apr 30 2020 at 15:11):

I expect that an edge case exists, but yes, in almost all cases

#### Mario Carneiro (Apr 30 2020 at 15:12):

There are two ways you can use rwa normally: to rewrite a hypothesis to match the goal, or to rewrite the goal to match a hypothesis. I would call neither of these uses sneaky. I usually use the former, which is clearly marked since it uses an at h clause

#### Mario Carneiro (Apr 30 2020 at 15:15):

Here is another sneaky use, where the hypothesis being used is h before the rewrite:

example (red herring : ℕ) (h : red = 0) (h2 : red = herring) (dep : h = h) : red = 0 :=
by rwa h2 at h


deleting dep breaks the proof

#### Reid Barton (Apr 30 2020 at 15:18):

This is like a doubly red herring.

Last updated: May 13 2021 at 23:16 UTC