# Zulip Chat Archive

## Stream: new members

### Topic: simp attribute

#### Damiano Testa (Mar 02 2022 at 07:56):

Dear All,

this question is mostly for my own education about `simp`

.

With my very limited understanding of how `simp`

works, I would have thought that the lemma below would not fire with `simp`

, due to the hypothesis `h`

.

```
@[simp]
lemma to_nat_pred_coe_of_pos {i : ℤ} (h : 0 < i) : ((i.to_nat - 1 : ℕ) : ℤ) = i - 1 :=
```

~~I tried proving this lemma using ~~`by simp [h]`

and I could not get it to work.

Proving this lemma using `by simp [h]`

works, but `by simp`

does not.

However, the `simp`

attribute is in data.int.basic.

What is the `simp`

attribute doing in this case?

Thanks!

#### Johan Commelin (Mar 02 2022 at 08:04):

It means that `simp`

will try to use the lemma `to_nat_pred_coe_of_pos`

. But it can only use if after it knows how to prove `h`

. So you either pass it `h`

directly, like you did. Or you hope that other simp lemmas can provide a proof of `h`

, recursively. The latter will be unlikely for a generic `0 < i`

proof. But if `i = 1`

, then it will probably work.

#### Damiano Testa (Mar 02 2022 at 08:07):

Ah, thanks for the explanation! I had not realized about the specific number case!

Last updated: Dec 20 2023 at 11:08 UTC