rw / simp difference

Stream: general

[Sebastien Gouezel]

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).