chore: remove unnecessary outParam

[JovanGerb]

I spotted an outParam in an instance argument of a class. The purpose of outParam is to fill in the value during type class search. However, since this is an instance argument, it must already have been synthesised at this point, so this has no purpose.

---

[JovanGerb]

!bench

[leanprover-bot]

Here are the benchmark results for commit 9681402caf32c1b0af2884db81b2bf890fd86a59. There were no significant changes against commit 712ef83de510992c182a0fcf289ab2a2e496ac28.

[JovanGerb]

Files in the namespace Mathlib.LinearAlgebra.AffineSpace, and files containing the name AddTorsor have all sped up by about 0.5% due to this change :)

The reason is that the outParam label causes the type class search to abstract away this argument, and at the end of the type class search, check that it matches with unification. By removing this outParam, it acts like a normal argument.

[github-actions[bot]]

🚀 Pull request has been placed on the maintainer queue by YaelDillies.

[mattrobball]

bors merge

[MichaelStollBayreuth]

General information:
  lint:                                                -1.5075 * 10⁹ (-0.0126%)
  build:                                               -9.1613 * 10⁹ (-0.00783%)

Files that got slower by at least 10⁹ instructions:
  Mathlib.Analysis.NormedSpace.PiTensorProduct.InjectiveSeminorm:
                                                       +1.8527 * 10⁹ (+0.666%)

No file got slower by at least 10%.

Files that got faster by at least 10⁹ instructions:
  Mathlib.Geometry.Manifold.VectorBundle.FiberwiseLinear:
                                                       -1.6580 * 10⁹ (-1.93%)
  Mathlib.RingTheory.Localization.Basic:               -1.1318 * 10⁹ (-1.02%)

No file got faster by at leat 10%.

[mathlib-bors[bot]]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style