Declaration silently not added to environment when using local notation

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
https://github.com/leanprover-community/mathlib4/pull/4695

Start with the self-contained reproduction and the #check tndsto entry point. Trace how the declaration is processed when local notation appears in its type, then verify that tndsto is added to the environment and printed successfully by #check without warnings or errors.