I have the following fact in my proof: `"n = 2^multiplicity 2 n * k"`

Further down, I would like to replace `n`

in a goal with `2^multiplicity 2 n * k`

. However, both `unfolding n`

and `apply (unfold n)`

go into an infinite loop. How do I avoid that?

```
apply (subst n)
```

if you need to direct it more:

```
apply (subst [(asm)][(position)] n)
```

(asm) = substitute in assumpition

(position) = substitute at position e.g. (1), (10), ...

Rewrite is nicer to use (you can write a pattern instead of referring to the position), but not part of Main. See https://isabelle.in.tum.de/dist/library/HOL/HOL-ex/Rewrite_Examples.html for examples

Last updated: Aug 13 2022 at 05:18 UTC