chore: fix diamonds for Real/Complex Algebra instances

Mathlib/Algebra/Algebra/Defs.lean

@@ -104,6 +104,7 @@ class Algebra (R : Type u) (A : Type v) [CommSemiring R] [Semiring A] extends SM
 end Prio
 
 /-- Embedding `R →+* A` given by `Algebra` structure. -/
+@[implicit_reducible]
 def algebraMap (R : Type u) (A : Type v) [CommSemiring R] [Semiring A] [Algebra R A] : R →+* A :=
   Algebra.algebraMap
 
@@ -350,7 +351,8 @@ This is the algebra version of `Module.compHom`.
 -/
 abbrev compHom : Algebra S A where
   __ := Module.compHom A f
-  algebraMap := (algebraMap R A).comp f
+  algebraMap.__ := (algebraMap R A).comp f
+  algebraMap.toFun x := algebraMap R A (f x)
   commutes' _ _ := Algebra.commutes _ _
   smul_def' _ _ := Algebra.smul_def _ _
 

Mathlib/Algebra/Algebra/Pi.lean

@@ -36,7 +36,8 @@ variable (A : ι → Type*)
 variable [CommSemiring R] [∀ i, Semiring (A i)] [∀ i, Algebra R (A i)]
 
 instance algebra : Algebra R (Π i, A i) where
-  algebraMap := Pi.ringHom fun i ↦ algebraMap R (A i)
+  algebraMap.__ := Pi.ringHom fun i ↦ algebraMap R (A i)
+  algebraMap.toFun x i := algebraMap R (A i) x
   commutes' := fun a f ↦ by ext; simp [Algebra.commutes]
   smul_def' := fun a f ↦ by ext; simp [Algebra.smul_def]
 

Mathlib/Algebra/Algebra/Prod.lean

@@ -37,7 +37,8 @@ variable (R A B)
 open Algebra
 
 instance algebra : Algebra R (A × B) where
-  algebraMap := RingHom.prod (algebraMap R A) (algebraMap R B)
+  algebraMap.__ := RingHom.prod (algebraMap R A) (algebraMap R B)
+  algebraMap.toFun x := (algebraMap R A x, algebraMap R B x)
   commutes' := by
     rintro r ⟨a, b⟩
     dsimp

Mathlib/Analysis/Complex/Basic.lean

@@ -64,7 +64,6 @@ instance : DenselyNormedField ℂ where
     let ⟨x, h⟩ := exists_between hr
     ⟨x, by rwa [norm_real, Real.norm_of_nonneg (h₀.trans_lt h.1).le]⟩
 
-set_option backward.isDefEq.respectTransparency false in
 instance {R : Type*} [NormedField R] [NormedAlgebra R ℝ] : NormedAlgebra R ℂ where
   norm_smul_le r x := by
     rw [← algebraMap_smul ℝ r x, real_smul, norm_mul, norm_real, norm_algebraMap']

Mathlib/Data/Complex/Basic.lean

@@ -77,7 +77,7 @@ theorem range_im : range im = univ :=
   im_surjective.range_eq
 
 /-- The natural inclusion of the real numbers into the complex numbers. -/
-@[coe]
+@[coe, implicit_reducible]
 def ofReal (r : ℝ) : ℂ :=
   ⟨r, 0⟩
 instance : Coe ℝ ℂ :=
@@ -561,6 +561,7 @@ theorem add_conj (z : ℂ) : z + conj z = (2 * z.re : ℝ) :=
   Complex.ext_iff.2 <| by simp [two_mul, ofReal]
 
 /-- The coercion `ℝ → ℂ` as a `RingHom`. -/
+@[implicit_reducible]
 def ofRealHom : ℝ →+* ℂ where
   toFun x := (x : ℂ)
   map_one' := ofReal_one

Mathlib/LinearAlgebra/Complex/Module.lean

@@ -98,7 +98,8 @@ instance (priority := 100) instModule [Semiring R] [Module R ℝ] : Module R ℂ
 
 -- priority manually adjusted in https://github.com/leanprover-community/mathlib4/pull/11980
 instance (priority := 95) instAlgebraOfReal [CommSemiring R] [Algebra R ℝ] : Algebra R ℂ where
-  algebraMap := Complex.ofRealHom.comp (algebraMap R ℝ)
+  algebraMap.__ := Complex.ofRealHom.comp (algebraMap R ℝ)
+  algebraMap.toFun x := algebraMap R ℝ x
   smul_def' := fun r x => by ext <;> simp [smul_re, smul_im, Algebra.smul_def]
   commutes' := fun r ⟨xr, xi⟩ => by ext <;> simp [Algebra.commutes]
 
@@ -166,15 +167,18 @@ instance (priority := 900) Algebra.complexToReal {A : Type*} [Semiring A] [Algeb
     Algebra ℝ A :=
   .restrictScalars ℝ ℂ A
 
--- try to make sure we're not introducing diamonds but we will need
--- `reducible_and_instances` which currently fails https://github.com/leanprover-community/mathlib4/issues/10906
-example : Prod.algebra ℝ ℂ ℂ = (Prod.algebra ℂ ℂ ℂ).complexToReal := rfl
+-- make sure that there's no semireducible steps in the definition of the algebraMap
+example (x : ℝ) : (algebraMap ℝ ℂ x).re  = x := by
+  with_reducible_and_instances exact rfl
 
--- try to make sure we're not introducing diamonds but we will need
--- `reducible_and_instances` which currently fails https://github.com/leanprover-community/mathlib4/issues/10906
+-- try to make sure we're not introducing diamonds
+example : Prod.algebra ℝ ℂ ℂ = (Prod.algebra ℂ ℂ ℂ).complexToReal := by
+  with_reducible_and_instances rfl
+
+-- try to make sure we're not introducing diamonds
 example {ι : Type*} [Fintype ι] :
-    Pi.algebra (R := ℝ) ι (fun _ ↦ ℂ) = (Pi.algebra (R := ℂ) ι (fun _ ↦ ℂ)).complexToReal :=
-  rfl
+    Pi.algebra (R := ℝ) ι (fun _ ↦ ℂ) = (Pi.algebra (R := ℂ) ι (fun _ ↦ ℂ)).complexToReal := by
+  with_reducible_and_instances rfl
 
 example {A : Type*} [Ring A] [inst : Algebra ℂ A] :
     (inst.complexToReal).toModule = (inst.toModule).complexToReal := by

MathlibTest/instance_diamonds.lean

@@ -27,13 +27,11 @@ open scoped Polynomial
 example : (SubNegMonoid.toZSMul : SMul ℤ ℂ) = (Complex.SMul.instSMulRealComplex : SMul ℤ ℂ) := by
   with_reducible_and_instances rfl
 
-set_option backward.isDefEq.respectTransparency false in
 example : Module.restrictScalars ℝ ℂ ℂ = Complex.instModule := by
   with_reducible_and_instances rfl
 
--- fails `with_reducible_and_instances` https://github.com/leanprover-community/mathlib4/issues/10906
 example : Algebra.restrictScalars ℝ ℂ ℂ = Complex.instAlgebraOfReal := by
-  rfl
+  with_reducible_and_instances rfl
 
 example (α β : Type _) [AddMonoid α] [AddMonoid β] :
     (Prod.instSMul : SMul ℕ (α × β)) = AddMonoid.toNSMul := by
@@ -57,7 +55,6 @@ open scoped TensorProduct
 
 open Complex
 
-set_option backward.isDefEq.respectTransparency false in
 /- `TensorProduct.Algebra.module` forms a diamond with `instSMulOfMul` and
 `algebra.tensor_product.tensor_product.semiring`. Given a commutative semiring `A` over a
 commutative semiring `R`, we get two mathematically different scalar actions of `A ⊗[R] A` on
@@ -259,9 +256,9 @@ that at least some potential diamonds are avoided. -/
 
 section complexToReal
 
--- fails `with_reducible_and_instances` https://github.com/leanprover-community/mathlib4/issues/10906
 -- the two ways to get `Algebra ℝ ℂ` are definitionally equal
-example : (Algebra.id ℂ).complexToReal = Complex.instAlgebraOfReal := rfl
+example : (Algebra.id ℂ).complexToReal = Complex.instAlgebraOfReal := by
+  with_reducible_and_instances rfl
 
 -- fails `with_reducible_and_instances` https://github.com/leanprover-community/mathlib4/issues/10906
 /- The complexification of an `ℝ`-algebra `A` (i.e., `ℂ ⊗[ℝ] A`) is a `ℂ`-algebra. Viewing this