chore: fix diamonds around R and C structures

[sgouezel]

The following examples fail on master, work with the PR:

example : (Semiring.toNatAlgebra : Algebra ℕ ℂ) = Complex.instAlgebraOfReal := by
  with_reducible_and_instances rfl

example : (Ring.toIntAlgebra ℂ : Algebra ℤ ℂ) = Complex.instAlgebraOfReal := by
  with_reducible_and_instances rfl

example : Module.restrictScalars ℝ ℂ ℂ = Complex.instModule := by
  with_reducible_and_instances rfl

example : (instInnerProductSpaceRealComplex.toSMul : SMul ℝ ℂ) = Complex.instRCLike.toSMul := by
  with_reducible_and_instances rfl

example {F : Type*} [NormedAddCommGroup F] [NormedSpace ℂ F] : SMulCommClass ℂ ℝ F :=
  inferInstance

The PR makes a few algebra maps implicit-reducible. This is necessary to get rid of the diamonds as these maps show up in the instances. This has no noticeable performance impact: implicit-reducible only matters for instances, and there it tends to help unification.

---

• depends on: [Merged by Bors] - chore: make .id and .comp implicit-reducible #38618
• depends on: [Merged by Bors] - chore: export algebraMap from Algebra instead of having a def #38430
• depends on: chore: fix implicit-reducible diamond in uniform convergence #38481

[mathlib-bors]

This pull request is now in draft mode. No active bors state needed cleanup.

While this PR remains draft, bors will ignore commands on this PR. Mark it ready for review before using commands like bors r+ or bors try.

[github-actions]

PR summary 5b5173e00f

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ ofFun

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

---

No changes to technical debt.

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[sgouezel]

!radar

[leanprover-radar]

Benchmark results for 3c79bc9 against 79540a7 are in. There are significant results. @sgouezel

• ✅ build//instructions: -135.5G (-0.08%)

Large changes (1✅)

• ✅ build/module/Mathlib.Algebra.Category.CommAlgCat.Monoidal//instructions: -83.0G (-33.10%)

Medium changes (2✅)

• ✅ build/module/Mathlib.Algebra.Category.BialgCat.Monoidal//instructions: -11.5G (-17.62%)
• ✅ build/module/Mathlib.AlgebraicGeometry.GammaSpecAdjunction//instructions: -5.7G (-5.78%)

Small changes (10✅, 2🟥)

• 🟥 build/module/Mathlib.Algebra.Ring.TransferInstance//instructions: +253.0M (+2.43%)
• ✅ build/module/Mathlib.AlgebraicGeometry.SpreadingOut//instructions: -609.4M (-2.19%)
• ✅ build/module/Mathlib.AlgebraicGeometry.ValuativeCriterion//instructions: -699.9M (-2.90%)
• 🟥 build/module/Mathlib.Data.Matrix.Auto//instructions: +131.3M (+3.53%)
• ✅ build/module/Mathlib.FieldTheory.CardinalEmb//instructions: -2.2G (-1.81%)
• ✅ build/module/Mathlib.FieldTheory.Extension//instructions: -2.3G (-2.98%)
• ✅ build/module/Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits//instructions: -916.0M (-3.41%)
• ✅ build/module/Mathlib.RingTheory.Bialgebra.Hom//instructions: -889.5M (-3.17%)
• ✅ build/module/Mathlib.RingTheory.Etale.QuasiFinite//instructions: -9.5G (-3.29%)
• ✅ build/module/Mathlib.RingTheory.GradedAlgebra.AlgHom//instructions: -949.4M (-3.24%)
• ✅ build/module/Mathlib.RingTheory.TensorProduct.Maps//instructions: -9.0G (-4.62%)
• ✅ build/module/Mathlib.RingTheory.WittVector.IsPoly//instructions: -651.2M (-2.36%)

[mathlib-dependent-issues]

This PR/issue depends on:

• [Merged by Bors] - chore: make .id and .comp implicit-reducible #38618
• [Merged by Bors] - chore: export algebraMap from Algebra instead of having a def #38430
• chore: fix implicit-reducible diamond in uniform convergence #38481
  By Dependent Issues (🤖). Happy coding!

[mathlib-merge-conflicts]

This pull request has conflicts, please merge master and resolve them.

[sgouezel]

!radar

[leanprover-radar]

Benchmark results for eae998b against 5b5173e are in. There are significant results. @sgouezel

• 🟥 main exited with code 1

No significant changes detected.

[sgouezel]

!radar

[leanprover-radar]

Benchmark results for dc8867d against 5b5173e are in. No significant results found. @sgouezel

• ✅ build//instructions: -25.6G (-0.01%)

Small changes (6✅, 1🟥)

• ✅ build/module/Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order//instructions: -2.2G (-1.46%)
• ✅ build/module/Mathlib.Analysis.Complex.Harmonic.Analytic//instructions: -563.5M (-2.11%)
• ✅ build/module/Mathlib.Analysis.Distribution.TemperedDistribution//instructions: -3.0G (-2.78%)
• ✅ build/module/Mathlib.NumberTheory.ModularForms.Basic//instructions: -1.0G (-2.58%)
• ✅ build/module/Mathlib.NumberTheory.ModularForms.CuspFormSubmodule//instructions: -210.9M (-1.63%)
• 🟥 build/module/Mathlib.Util.AliasIn//instructions: +105.5M (+3.41%) (reduced significance based on absolute threshold)
• ✅ build/module/Mathlib.Util.TransImports//instructions: -93.0M (-3.41%)