chore(analysis/normed_space/basic): implicit args

[urkud]

Arguments to these iffs should be implicit.

TO CONTRIBUTORS:

Make sure you have:

• reviewed and applied the coding style: coding, naming
• reviewed and applied the documentation requirements
• for tactics:
  • added or adapted documentation in tactics.md
  • write an example of use of the new feature in tactics.lean
• make sure definitions and lemmas are put in the right files
• make sure definitions and lemmas are not redundant

If this PR is related to a discussion on Zulip, please include a link in the discussion.

For reviewers: code review check list

[PatrickMassot]

I wonder if we could have a linter detecting this: if a lemma is an iff or equality, then check that every variable that appears on both sides is implicit.

[gebner]

@PatrickMassot I added your idea to our grand linter todo list #1924.