## 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