# Zulip Chat Archive

## Stream: new members

### Topic: Coercion issues

#### Jack J Garzella (Apr 30 2020 at 03:12):

I'm trying to prove the following statement

```
lemma power_inverse :
∀ (a : real) (b : nat)
(ha : 0 ≤ a),
(a ^ (1 / b)) ^ b = a :=
```

and it looks to me from the docs that `real.rpow_mul`

is a lemma that I might want to use. But when I tried to start the proof as follows:

```
begin
rw [(eq.symm (real.rpow_mul ha (1 / b) b))],
...
end
```

it seems that lean can't figure out the coersions of `1/b`

and `b`

and I get a `rewrite tactic failed, did not find instance of the pattern in the target expression \n (a ^ (1 / ↑b)) ^ ↑b`

. But if I replace the `b`

with `↑b`

, then it gives me a `don't know how to synthesize placeholder`

error.

Can anyone help me deal with these coercions? Or, is there a more automatic way to do things like this that I'm missing?

#### Alex J. Best (Apr 30 2020 at 03:19):

Whenever you get stuck with coercions like this its important to work out exactly what types everything is.

You can do this in a couple of ways, by setting `set_option pp.all true`

will show you everything, but in this case you can also add `dsimp [(^)],`

to see what `^`

is being used here. In either case you'll see its taking real to a `nat`

power, which is not what you intended. `1/b`

is being interpreted as the nat `1/b`

(likely just 0).

#### Alex J. Best (Apr 30 2020 at 03:22):

So a corrected (but not completely correct yet) statement would be

```
lemma power_inverse :
∀ (a : real) (b : nat)
(ha : 0 ≤ a),
(a ^ (1 / (b : ℝ))) ^ (b : ℝ) = a :=
begin
intros,
rw [← real.rpow_mul ha],
end
```

#### Jack J Garzella (Apr 30 2020 at 16:06):

Thanks so much! All of this was extremely helpful! I've now successfully proven my lemma, which looks like this:

```
lemma power_inverse :
∀ (a : real) (b : nat)
(ha : 0 ≤ a) (hb : (b : ℝ) ≠ 0),
(a ^ (1 / (b : ℝ))) ^ (b : ℝ) = a :=
begin
intros,
rw [←real.rpow_mul ha],
simp,
calc a ^ ((↑b)⁻¹ * ↑b) = a ^ ((1 : ℝ)) : by rw [field.inv_mul_cancel hb]
... = a : by simp
end
```

The proof I used though is a bit verbose, and I'd like to make it shorter. In particular,

1) I can't figure out how to get `simp`

to use the `field.inv_mul_cancel`

lemma (which is marked `@[simp]`

)

2) It might be nice to have `hb`

be of type `b ≠ 0`

rather than `(b : ℝ) ≠ 0`

, but I don't know how to easily make `b`

promote it's type.

How might I go about solving these?

#### Alex J. Best (Apr 30 2020 at 16:25):

Well if you want to make it short you can just use an explicit chain of rewrites in place of invoking simp, and not use a calc block (but calc blocks look nice)

```
lemma power_inverse :
∀ (a : real) (b : nat)
(ha : 0 ≤ a) (hb : (b : ℝ) ≠ 0),
(a ^ (1 / (b : ℝ))) ^ (b : ℝ) = a :=
begin
intros,
rw [←real.rpow_mul ha, one_div_eq_inv, inv_mul_cancel hb, real.rpow_one],
end
```

#### Alex J. Best (Apr 30 2020 at 16:45):

If you want simp to use `inv_mul_cancel`

I believe you'll need to supply `hb`

to simp,

```
lemma power_inverse :
∀ (a : real) (b : nat)
(ha : 0 ≤ a) (hb : (b : ℝ) ≠ 0),
(a ^ (1 / (b : ℝ))) ^ (b : ℝ) = a :=
begin
intros,
rw [←real.rpow_mul ha],
simp [hb],
end
```

#### Alex J. Best (Apr 30 2020 at 16:46):

Though in fact simp uses a different lemma `inv_mul_cancel'`

in this case instead of the one you has in mind, which applies instead to groups with zero, rather than just division rings.

#### Kevin Buzzard (Apr 30 2020 at 17:32):

```
import analysis.calculus.specific_functions
lemma power_inverse :
∀ (a : real) (b : nat)
(ha : 0 ≤ a) (hb : (b : ℝ) ≠ 0),
(a ^ (1 / (b : ℝ))) ^ (b : ℝ) = a :=
λ _ _ ha hb, by simp [(real.rpow_mul ha _ _).symm, hb]
```

Last updated: May 13 2021 at 04:21 UTC