simp_all does less than simp at hyp

Stream: general

[Johan Commelin]

Is this expected behaviour?

import Mathlib

universe r s u v w

namespace WeierstrassCurve

variable {R : Type r} {S : Type s} {A F : Type u} {B K : Type v} {L : Type w} [CommRing R]
  [CommRing S] [CommRing A] [CommRing B] [Field F] [Field K] [Field L] {W : Affine F}

open WeierstrassCurve Affine Point in
example {x₁ y₁ : F} {h₁ : W.Nonsingular x₁ y₁} (hy : y₁ ≠ W.negY x₁ y₁) :
    some h₁ + some h₁ = some (nonsingular_add h₁ h₁ fun hxy => hy hxy.right) := by
  simp_all    -- doesn't seem to do anything
  simp at hy  -- does do something!
  sorry

[Shreyas Srinivas]

It seems to be doing something on the hidden part of the goal according to the infoview (more visible with set_option pp.proofs true)

[Johan Commelin]

But why doesn't it also simp hy?

[Shreyas Srinivas]

I don't know that but I just wanted to point out that simp_all is doing something, not nothing

[Markus Himmel]

Yes, this is known/expected. simp_all/simp at * will leave hypotheses untouched in some cases if they appear in the goal or in other hypotheses. See lean4#5593.

[Johan Commelin]

Aha, thanks!