# Zulip Chat Archive

## Stream: general

### Topic: rw / simp difference

#### Sebastien Gouezel (May 22 2019 at 06:38):

I just encountered a very weird behavior. I have at the end of a proof a line

simp [written_in_ext_chart_at, ext_chart_at, local_equiv.to_inv, mem_some_chart_at_source]

With this line, the proof works, but I get red squiggles under the name of the theorem, with the error message

type mismatch at application @written_in_ext_chart_at k _inst_1 (@tangent_space_at k _inst_1 E _inst_2 H _inst_3 I M _inst_4 _inst_5 _inst_6 x) _inst_2 H _inst_3 I M _inst_4 _inst_5 _inst_6_1 E' _inst_7 H' _inst_8 I' M' _inst_9 _inst_10 _inst_11 term _inst_11 has type @manifold.smooth 1 k _inst_1 E' _inst_7 H' _inst_8 I'_1 M' _inst_9 _inst_10 but is expected to have type @manifold.smooth 1 k _inst_1 E' _inst_7 H' _inst_8 I' M' _inst_9 _inst_10 types contain aliased name(s): I' remark: the tactic `dedup` can be used to rename aliases

Except that I can't see any place where I would have introduced two different variables `I'`

. What is funny is that if I replace my `simp`

line with the two lines

rw written_in_ext_chart_at, simp [written_in_ext_chart_at, ext_chart_at, local_equiv.to_inv, mem_some_chart_at_source]

then the error goes away. Highly non-minimal example at https://github.com/sgouezel/mathlib/blob/b87ee06fe4385c12fa2e53b867913b62feb609fb/src/geometry/manifolds/mderiv.lean#L599

I am afraid it indicates there is something fishy in the way I define stuff (or, at the very least, something that Lean doesn't like very much). The motivation for the definitions as they are is at https://github.com/sgouezel/mathlib/blob/b87ee06fe4385c12fa2e53b867913b62feb609fb/src/geometry/manifolds/mderiv.lean#L154 (and I can explain here on Zulip if needed).

Last updated: May 15 2021 at 23:13 UTC