Declaration silently not added to environment when using local notation

[alexjbest]

Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Checked that your issue isn't already filed.
  • Reduced the issue to a self-contained, reproducible test case.

Description

When using local notation some declarations can silently not be added to the environment

Steps to Reproduce

variable {ι E : Type} (I : ι)

local notation "ℝ" => ι

def ha (_I : ι) (_f : ℝ → E) : Prop := True

variable {f : ℝ → E}

theorem tndsto (h : ha I f) : True := trivial
#check tndsto

Expected behavior: tndsto should be added to the environment and be printed by #check

Actual behavior: Without error or warning on tndsto itself nothing happens and check fails

Reproduces how often: 100%

Versions

latest, cross platform

Additional Information

Came up in mathlib porting this is a minimized version of the issue observed in https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Lean.204.20doesn't.20add.20lemma.20to.20the.20environment
leanprover-community/mathlib4#4695

[digama0]

For cross referencing purposes: this is likely related to #2226 and may have the same root cause.