Lean 4 doesn't add lemma to the environment

Stream: mathlib4

[Yury G. Kudryashov]

In !4#4695, the first error happens because Lean doesn't add BoxIntegral.HasIntegral.tendsto to the environment. At least,

• whatsnew in says nothing about it;
• #check HasIntegral.tendsto fails.

[Alex J. Best]

I'm not sure why but the issue is caused by the local notation for $\mathbb R^n$ in

{f g : ℝⁿ → E}

if you look at the state in the tendsto theorem the type of f has sorries in and lean silently just ignores the theorem. If you replace the local notation with its definition of iota to R then everything goes through

[Alex J. Best]

I hope you don't mind but I made the change to not use the notation and did a couple more lemmas and pushed to the branch, you'll likely want to check what I pushed I just wanted to be sure that the next few lemmas were working ok after this change

[Yury G. Kudryashov]

Thank you!

[Yury G. Kudryashov]

I'm taking over this branch again.

[Scott Morrison]

Adding links to posterity: Alex minimised and reported this as https://github.com/leanprover/lean4/issues/2257.