simp? infelicity

Stream: mathlib4

[Dominic Steinitz]

At the behest of the linter I am removing simp. I replace simp? with what I am told but then get an error :-(

An easy solution is at hand without using simp but nonetheless my conscience pricked me to report this infelicity.

import Mathlib

variable
  {EB : Type*} [NormedAddCommGroup EB] [InnerProductSpace ℝ EB]
  {HB : Type*} [TopologicalSpace HB] {IB : ModelWithCorners ℝ EB HB}
  {B : Type*} [TopologicalSpace B] [ChartedSpace HB B]

example (x : B)
  (φ : TangentSpace IB x →L[ℝ] TangentSpace IB x →L[ℝ] ℝ)
  (r s : TangentSpace IB x) :
  φ (r + s) (r + s) = (φ r) r + (φ r) s + (φ s) r + (φ s) s := by
  simp?
  exact Eq.symm (add_assoc ((φ r) r + (φ r) s) ((φ s) r) ((φ s) s))

example (x : B)
  (φ : TangentSpace IB x →L[ℝ] TangentSpace IB x →L[ℝ] ℝ)
  (r s : TangentSpace IB x) :
  φ (r + s) (r + s) = (φ r) r + (φ r) s + (φ s) r + (φ s) s := by
  simp only [map_add, ContinuousLinearMap.add_apply]
  exact Eq.symm (add_assoc ((φ r) r + (φ r) s) ((φ s) r) ((φ s) s))

example (x : B)
  (φ : TangentSpace IB x →L[ℝ] TangentSpace IB x →L[ℝ] ℝ)
  (r s : TangentSpace IB x) :
  φ (r + s) (r + s) = (φ r) r + (φ r) s + (φ s) r + (φ s) s := by
  calc φ (r + s) (r + s) = φ (r + s) r +  φ (r + s) s :=
         ContinuousLinearMap.map_add (φ (r + s)) r s
       _ = φ r r + φ s r + φ (r + s) s := by rw [ContinuousLinearMap.map_add₂ φ r s r]
       _ = φ r r + φ s r +  φ r s + φ s s := by
        rw [ContinuousLinearMap.map_add₂ φ r s s]
        exact Eq.symm (add_assoc ((φ r) r + (φ s) r) ((φ r) s) ((φ s) s))
       _ = (φ r) r + (φ r) s + (φ s) r + (φ s) s :=
        add_add_add_comm' ((φ r) r) ((φ s) r) ((φ r) s) ((φ s) s)

[Dominic Steinitz]

lol - by rw [ContinuousLinearMap.map_add₂ φ r s r] works for me locally but not in the lean playground.

[Eric Wieser]

What version are you on locally?

[Dominic Steinitz]

Eric Wieser said:

What version are you on locally?

0e708caf75 * origin/update-dependencies-bot-use-only origin/staging chore(Tactic/Translate/ToDual): fix typo in nameDict (#33701)

[Eric Wieser]

This might be a difference in the lakefile then?

[Eric Wieser]

These theorems are in the wrong generality, let me fix that...

[Eric Wieser]

#33750

[Eric Wieser]

Regarding simp?, using simp only [map_add, (ContinuousLinearMap.add_apply)] instead of simp only [map_add, ContinuousLinearMap.add_apply] works

[Eric Wieser]

(that is, you need to add ()s that simp? is not showing)

[Dominic Steinitz]

Interesting - what do the surrounding ( ... ) do?

[Eric Wieser]

They turn off some special behavior that simp has that makes simp [foo, bar] mean the same as simp [@foo, @bar]

[Eric Wieser]

So () means "don't insert an @", roughly

[Eric Wieser]

I don't know why simp has this behavior, I would guess that @Kyle Miller does

[Eric Wieser]

We ran into problems like this all the time during the port, it's interesting to see that some remain

[Dominic Steinitz]

Thanks for the explanation and speedy fix :-)