chore(diamonds): appropriate transparency levels for diamond checks (#…

…10910)

Currently, we have multiple "no-diamond" tests of the form
```lean
example : x = y := rfl
```
where `X` and `Y` are instances of some `class`. The problem is that since `simp` and type class synthesis operate at `reducible_and_instances` transparency this check means little.

We went through all the mentions of diamonds and either added `with_reducible_and_instancse` or added a reference to the issue #10906.



Co-authored-by: Kevin Buzzard <k.buzzard@imperial.ac.uk>

Mathlib/Algebra/Algebra/NonUnitalSubalgebra.lean

@@ -999,10 +999,9 @@ variable (R A : Type*) [CommSemiring R] [NonUnitalSemiring A] [Module R A] [IsSc
   [SMulCommClass R A A]
 
 -- no instance diamond, as the `npow` field isn't present in the non-unital case.
-example :
-    center.instNonUnitalCommSemiring.toNonUnitalSemiring =
-      NonUnitalSubsemiringClass.toNonUnitalSemiring (center R A) :=
-  rfl
+example : center.instNonUnitalCommSemiring.toNonUnitalSemiring =
+    NonUnitalSubsemiringClass.toNonUnitalSemiring (center R A) := by
+  with_reducible_and_instances rfl
 
 @[simp]
 theorem center_eq_top (A : Type*) [NonUnitalCommSemiring A] [Module R A] [IsScalarTower R A A]

Mathlib/Algebra/FreeAlgebra.lean

@@ -266,7 +266,8 @@ instance instAlgebra {A} [CommSemiring A] [Algebra R A] : Algebra R (FreeAlgebra
     exact Quot.sound Rel.central_scalar
   smul_def' _ _ := rfl
 
--- verify there is no diamond
+-- verify there is no diamond at `default` transparency but we will need
+-- `reducible_and_instances` which currently fails #10906
 variable (S : Type) [CommSemiring S] in
 example : (algebraNat : Algebra ℕ (FreeAlgebra S X)) = instAlgebra _ _ := rfl
 
@@ -287,7 +288,8 @@ instance {R S A} [CommSemiring R] [CommSemiring S] [CommSemiring A] [Algebra R A
 instance {S : Type*} [CommRing S] : Ring (FreeAlgebra S X) :=
   Algebra.semiringToRing S
 
--- verify there is no diamond
+-- verify there is no diamond but we will need
+-- `reducible_and_instances` which currently fails #10906
 variable (S : Type) [CommRing S] in
 example : (algebraInt _ : Algebra ℤ (FreeAlgebra S X)) = instAlgebra _ _ := rfl
 

Mathlib/Data/Complex/Module.lean

@@ -185,14 +185,19 @@ instance (priority := 900) Algebra.complexToReal {A : Type*} [Semiring A] [Algeb
     Algebra ℝ A :=
   RestrictScalars.algebra ℝ ℂ A
 
--- try to make sure we're not introducing diamonds.
+-- try to make sure we're not introducing diamonds but we will need
+-- `reducible_and_instances` which currently fails #10906
 example : Prod.algebra ℝ ℂ ℂ = (Prod.algebra ℂ ℂ ℂ).complexToReal := rfl
+
+-- try to make sure we're not introducing diamonds but we will need
+-- `reducible_and_instances` which currently fails #10906
 example {ι : Type*} [Fintype ι] :
     Pi.algebra (R := ℝ) ι (fun _ ↦ ℂ) = (Pi.algebra (R := ℂ) ι (fun _ ↦ ℂ)).complexToReal :=
   rfl
+
 example {A : Type*} [Ring A] [inst : Algebra ℂ A] :
     (inst.complexToReal).toModule = (inst.toModule).complexToReal :=
-  rfl
+  by with_reducible_and_instances rfl
 
 @[simp, norm_cast]
 theorem Complex.coe_smul {E : Type*} [AddCommGroup E] [Module ℂ E] (x : ℝ) (y : E) :

Mathlib/Data/ZMod/IntUnitsPower.lean

@@ -57,7 +57,8 @@ Notably this is satisfied by `R ∈ {ℕ, ℤ, ZMod 2}`. -/
 instance Int.instUnitsPow : Pow ℤˣ R where
   pow u r := Additive.toMul (r • Additive.ofMul u)
 
--- The above instance forms no typeclass diamonds with the standard power operators
+-- The above instances form no typeclass diamonds with the standard power operators
+-- but we will need `reducible_and_instances` which currently fails #10906
 example : Int.instUnitsPow = Monoid.toNatPow := rfl
 example : Int.instUnitsPow = DivInvMonoid.Pow := rfl
 

Mathlib/GroupTheory/GroupAction/Opposite.lean

@@ -237,8 +237,8 @@ instance SMulCommClass.opposite_mid {M N} [Mul N] [SMul M N] [IsScalarTower M N
 
 -- The above instance does not create an unwanted diamond, the two paths to
 -- `MulAction αᵐᵒᵖ αᵐᵒᵖ` are defeq.
-example [Monoid α] : Monoid.toMulAction αᵐᵒᵖ = MulOpposite.mulAction α αᵐᵒᵖ :=
-  rfl
+example [Monoid α] : Monoid.toMulAction αᵐᵒᵖ = MulOpposite.mulAction α αᵐᵒᵖ := by
+  with_reducible_and_instances rfl
 
 /-- `Monoid.toOppositeMulAction` is faithful on cancellative monoids. -/
 @[to_additive "`AddMonoid.toOppositeAddAction` is faithful on cancellative monoids."]

Mathlib/GroupTheory/Submonoid/Center.lean

@@ -72,9 +72,8 @@ instance center.commMonoid : CommMonoid (center M) :=
   { (center M).toMonoid, Subsemigroup.center.commSemigroup with }
 
 -- no instance diamond, unlike the primed version
-example :
-    center.commMonoid.toMonoid = Submonoid.toMonoid (center M) :=
-  rfl
+example : center.commMonoid.toMonoid = Submonoid.toMonoid (center M) := by
+  with_reducible_and_instances rfl
 
 @[to_additive]
 theorem mem_center_iff {z : M} : z ∈ center M ↔ ∀ g, g * z = z * g := by

Mathlib/LinearAlgebra/CliffordAlgebra/Basic.lean

@@ -88,7 +88,9 @@ instance (priority := 900) instAlgebra' {R A M} [CommSemiring R] [AddCommGroup M
   RingQuot.instAlgebra _
 
 -- verify there are no diamonds
+-- but doesn't work at `reducible_and_instances` #10906
 example : (algebraNat : Algebra ℕ (CliffordAlgebra Q)) = instAlgebra' _ := rfl
+-- but doesn't work at `reducible_and_instances` #10906
 example : (algebraInt _ : Algebra ℤ (CliffordAlgebra Q)) = instAlgebra' _ := rfl
 
 -- shortcut instance, as the other instance is slow

Mathlib/LinearAlgebra/TensorAlgebra/Basic.lean

@@ -77,6 +77,7 @@ instance instAlgebra {R A M} [CommSemiring R] [AddCommMonoid M] [CommSemiring A]
   RingQuot.instAlgebra _
 
 -- verify there is no diamond
+-- but doesn't work at `reducible_and_instances` #10906
 example : (algebraNat : Algebra ℕ (TensorAlgebra R M)) = instAlgebra := rfl
 
 instance {R S A M} [CommSemiring R] [CommSemiring S] [AddCommMonoid M] [CommSemiring A]
@@ -97,6 +98,7 @@ instance {S : Type*} [CommRing S] [Module S M] : Ring (TensorAlgebra S M) :=
   RingQuot.instRing (Rel S M)
 
 -- verify there is no diamond
+-- but doesn't work at `reducible_and_instances` #10906
 variable (S M : Type) [CommRing S] [AddCommGroup M] [Module S M] in
 example : (algebraInt _ : Algebra ℤ (TensorAlgebra S M)) = instAlgebra := rfl
 

Mathlib/MeasureTheory/Function/LpSpace.lean

@@ -458,11 +458,11 @@ instance instNormedAddCommGroup [hp : Fact (1 ≤ p)] : NormedAddCommGroup (Lp E
 #align measure_theory.Lp.normed_add_comm_group MeasureTheory.Lp.instNormedAddCommGroup
 
 -- check no diamond is created
-example [Fact (1 ≤ p)] : PseudoEMetricSpace.toEDist = (Lp.instEDist : EDist (Lp E p μ)) :=
-  rfl
+example [Fact (1 ≤ p)] : PseudoEMetricSpace.toEDist = (Lp.instEDist : EDist (Lp E p μ)) := by
+  with_reducible_and_instances rfl
 
-example [Fact (1 ≤ p)] : SeminormedAddGroup.toNNNorm = (Lp.instNNNorm : NNNorm (Lp E p μ)) :=
-  rfl
+example [Fact (1 ≤ p)] : SeminormedAddGroup.toNNNorm = (Lp.instNNNorm : NNNorm (Lp E p μ)) := by
+  with_reducible_and_instances rfl
 
 section BoundedSMul
 

Mathlib/NumberTheory/Cyclotomic/Basic.lean

@@ -573,9 +573,8 @@ instance CyclotomicField.algebraBase : Algebra A (CyclotomicField n K) :=
   SplittingField.algebra' (cyclotomic n K)
 #align cyclotomic_field.algebra_base CyclotomicField.algebraBase
 
-/-- Ensure there are no diamonds when `A = ℤ`. -/
-example : algebraInt (CyclotomicField n ℚ) = CyclotomicField.algebraBase _ _ _ :=
-  rfl
+/-- Ensure there are no diamonds when `A = ℤ` but there are `reducible_and_instances` #10906 -/
+example : algebraInt (CyclotomicField n ℚ) = CyclotomicField.algebraBase _ _ _ := rfl
 
 instance CyclotomicField.algebra' {R : Type*} [CommRing R] [Algebra R K] :
     Algebra R (CyclotomicField n K) :=
@@ -622,8 +621,8 @@ instance algebraBase : Algebra A (CyclotomicRing n A K) :=
 #align cyclotomic_ring.algebra_base CyclotomicRing.algebraBase
 
 -- Ensure that there is no diamonds with ℤ.
-example {n : ℕ+} : CyclotomicRing.algebraBase n ℤ ℚ = algebraInt _ :=
-  rfl
+-- but there is at `reducible_and_instances` #10906
+example {n : ℕ+} : CyclotomicRing.algebraBase n ℤ ℚ = algebraInt _ := rfl
 
 instance : NoZeroSMulDivisors A (CyclotomicRing n A K) :=
   (adjoin A _).noZeroSMulDivisors_bot

Mathlib/NumberTheory/NumberField/Basic.lean

@@ -95,7 +95,7 @@ instance inst_ringOfIntegersAlgebra [Algebra K L] : Algebra (𝓞 K) (𝓞 L) :=
         Subtype.ext <| by simp only [Subalgebra.coe_mul, map_mul, Subtype.coe_mk] }
 #align number_field.ring_of_integers_algebra NumberField.inst_ringOfIntegersAlgebra
 
--- no diamond
+-- diamond at `reducible_and_instances` #10906
 example : Algebra.id (𝓞 K) = inst_ringOfIntegersAlgebra K K := rfl
 
 namespace RingOfIntegers

Mathlib/RingTheory/NonUnitalSubring/Basic.lean

@@ -624,10 +624,9 @@ section NonUnitalRing
 variable [NonUnitalRing R]
 
 -- no instance diamond, unlike the unital version
-example :
-    (center.instNonUnitalCommRing _).toNonUnitalRing =
-      NonUnitalSubringClass.toNonUnitalRing (center R) :=
-  rfl
+example : (center.instNonUnitalCommRing _).toNonUnitalRing =
+      NonUnitalSubringClass.toNonUnitalRing (center R) := by
+  with_reducible_and_instances rfl
 
 theorem mem_center_iff {z : R} : z ∈ center R ↔ ∀ g, g * z = z * g := Subsemigroup.mem_center_iff
 

Mathlib/RingTheory/NonUnitalSubsemiring/Basic.lean

@@ -516,7 +516,7 @@ section NonUnitalSemiring
 example {R} [NonUnitalSemiring R] :
     (center.instNonUnitalCommSemiring _).toNonUnitalSemiring =
       NonUnitalSubsemiringClass.toNonUnitalSemiring (center R) :=
-  rfl
+  by with_reducible_and_instances rfl
 
 theorem mem_center_iff {R} [NonUnitalSemiring R] {z : R} : z ∈ center R ↔ ∀ g, g * z = z * g := by
   rw [← Semigroup.mem_center_iff]

Mathlib/RingTheory/Subsemiring/Basic.lean

@@ -753,8 +753,8 @@ instance center.commSemiring {R} [Semiring R] : CommSemiring (center R) :=
 
 -- no instance diamond, unlike the primed version
 example {R} [Semiring R] :
-    center.commSemiring.toSemiring = Subsemiring.toSemiring (center R) :=
-  rfl
+    center.commSemiring.toSemiring = Subsemiring.toSemiring (center R) := by
+  with_reducible_and_instances rfl
 
 theorem mem_center_iff {R} [Semiring R] {z : R} : z ∈ center R ↔ ∀ g, g * z = z * g :=
   Subsemigroup.mem_center_iff

Mathlib/RingTheory/TensorProduct.lean

@@ -570,7 +570,9 @@ theorem intCast_def' (z : ℤ) : (z : A ⊗[R] B) = (1 : A) ⊗ₜ (z : B) := by
   rw [intCast_def, ← zsmul_one, smul_tmul, zsmul_one]
 
 -- verify there are no diamonds
-example : (instRing : Ring (A ⊗[R] B)).toAddCommGroup = addCommGroup := rfl
+example : (instRing : Ring (A ⊗[R] B)).toAddCommGroup = addCommGroup := by
+  with_reducible_and_instances rfl
+-- fails at `with_reducible_and_instances rfl` #10906
 example : (algebraInt _ : Algebra ℤ (ℤ ⊗[ℤ] B)) = leftAlgebra := rfl
 
 end Ring

test/instance_diamonds.lean

@@ -22,30 +22,31 @@ section SMul
 
 open scoped Polynomial
 
-example : (SubNegMonoid.SMulInt : SMul ℤ ℂ) = (Complex.instSMulRealComplex : SMul ℤ ℂ) :=
-  rfl
+example : (SubNegMonoid.SMulInt : SMul ℤ ℂ) = (Complex.instSMulRealComplex : SMul ℤ ℂ) := by
+  with_reducible_and_instances rfl
 
-example : RestrictScalars.module ℝ ℂ ℂ = Complex.instModule :=
-  rfl
+example : RestrictScalars.module ℝ ℂ ℂ = Complex.instModule := by
+  with_reducible_and_instances rfl
 
-example : RestrictScalars.algebra ℝ ℂ ℂ = Complex.instAlgebraComplexInstSemiringComplex :=
+-- fails `with_reducible_and_instances` #10906
+example : RestrictScalars.algebra ℝ ℂ ℂ = Complex.instAlgebraComplexInstSemiringComplex := by
   rfl
 
 example (α β : Type _) [AddMonoid α] [AddMonoid β] :
-    (Prod.smul : SMul ℕ (α × β)) = AddMonoid.toNatSMul :=
-  rfl
+    (Prod.smul : SMul ℕ (α × β)) = AddMonoid.toNatSMul := by
+  with_reducible_and_instances rfl
 
 example (α β : Type _) [SubNegMonoid α] [SubNegMonoid β] :
-    (Prod.smul : SMul ℤ (α × β)) = SubNegMonoid.SMulInt :=
-  rfl
+    (Prod.smul : SMul ℤ (α × β)) = SubNegMonoid.SMulInt := by
+  with_reducible_and_instances rfl
 
 example (α : Type _) (β : α → Type _) [∀ a, AddMonoid (β a)] :
-    (Pi.instSMul : SMul ℕ (∀ a, β a)) = AddMonoid.toNatSMul :=
-  rfl
+    (Pi.instSMul : SMul ℕ (∀ a, β a)) = AddMonoid.toNatSMul := by
+  with_reducible_and_instances rfl
 
 example (α : Type _) (β : α → Type _) [∀ a, SubNegMonoid (β a)] :
-    (Pi.instSMul : SMul ℤ (∀ a, β a)) = SubNegMonoid.SMulInt :=
-  rfl
+    (Pi.instSMul : SMul ℤ (∀ a, β a)) = SubNegMonoid.SMulInt := by
+  with_reducible_and_instances rfl
 
 namespace TensorProduct
 
@@ -88,13 +89,16 @@ end TensorProduct
 section Units
 
 example (α : Type _) [Monoid α] :
-    (Units.instMulAction : MulAction αˣ (α × α)) = Prod.mulAction := rfl
+    (Units.instMulAction : MulAction αˣ (α × α)) = Prod.mulAction := by
+  with_reducible_and_instances rfl
 
 example (R α : Type _) (β : α → Type _) [Monoid R] [∀ i, MulAction R (β i)] :
-    (Units.instMulAction : MulAction Rˣ (∀ i, β i)) = Pi.mulAction _ := rfl
+    (Units.instMulAction : MulAction Rˣ (∀ i, β i)) = Pi.mulAction _ := by
+  with_reducible_and_instances rfl
 
 example (R α : Type _) [Monoid R] [Semiring α] [DistribMulAction R α] :
-    (Units.instDistribMulAction : DistribMulAction Rˣ α[X]) = Polynomial.distribMulAction := rfl
+    (Units.instDistribMulAction : DistribMulAction Rˣ α[X]) = Polynomial.distribMulAction := by
+  with_reducible_and_instances rfl
 
 /-!
 TODO: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/units.2Emul_action'.20diamond/near/246402813
@@ -122,8 +126,8 @@ example (R : Type _) [h : StrictOrderedSemiring R] :
       @OrderedAddCommMonoid.toAddCommMonoid (WithTop R)
         (@WithTop.orderedAddCommMonoid R
           (@OrderedCancelAddCommMonoid.toOrderedAddCommMonoid R
-            (@StrictOrderedSemiring.toOrderedCancelAddCommMonoid R h))) :=
-  rfl
+            (@StrictOrderedSemiring.toOrderedCancelAddCommMonoid R h))) := by
+  with_reducible_and_instances rfl
 
 end WithTop
 
@@ -132,9 +136,9 @@ end WithTop
 
 section Multiplicative
 
-example :
-    @Monoid.toMulOneClass (Multiplicative ℕ) CommMonoid.toMonoid = Multiplicative.mulOneClass :=
-  rfl
+example : @Monoid.toMulOneClass (Multiplicative ℕ) CommMonoid.toMonoid =
+    Multiplicative.mulOneClass := by
+  with_reducible_and_instances rfl
 
 end Multiplicative
 
@@ -198,15 +202,18 @@ example [CommSemiring R] [Nontrivial R] :
   simp_rw [SMul.ext_iff, @SMul.smul_eq_hSMul _ _ (_), Function.funext_iff, Polynomial.ext_iff] at h
   simpa using h X 1 1 0
 
+-- fails `with_reducible_and_instances` #10906
 /-- `Polynomial.hasSMulPi'` is consistent with `Polynomial.hasSMulPi`. -/
 example [CommSemiring R] [Nontrivial R] :
     Polynomial.hasSMulPi' _ _ _ = (Polynomial.hasSMulPi _ _ : SMul R[X] (R → R[X])) :=
   rfl
 
+-- fails `with_reducible_and_instances` #10906
 /-- `Polynomial.algebraOfAlgebra` is consistent with `algebraNat`. -/
 example [Semiring R] : (Polynomial.algebraOfAlgebra : Algebra ℕ R[X]) = algebraNat :=
   rfl
 
+-- fails `with_reducible_and_instances` #10906
 /-- `Polynomial.algebraOfAlgebra` is consistent with `algebraInt`. -/
 example [Ring R] : (Polynomial.algebraOfAlgebra : Algebra ℤ R[X]) = algebraInt _ :=
   rfl
@@ -236,14 +243,14 @@ variable {p : ℕ} [Fact p.Prime]
 
 example :
     @EuclideanDomain.toCommRing _ (@Field.toEuclideanDomain _ (ZMod.instFieldZMod p)) =
-      ZMod.commRing p :=
-  rfl
+      ZMod.commRing p := by
+  with_reducible_and_instances rfl
 
-example (n : ℕ) : ZMod.commRing (n + 1) = Fin.instCommRing (n + 1) :=
-  rfl
+example (n : ℕ) : ZMod.commRing (n + 1) = Fin.instCommRing (n + 1) := by
+  with_reducible_and_instances rfl
 
-example : ZMod.commRing 0 = Int.instCommRingInt :=
-  rfl
+example : ZMod.commRing 0 = Int.instCommRingInt := by
+  with_reducible_and_instances rfl
 
 end ZMod
 
@@ -258,15 +265,17 @@ that at least some potential diamonds are avoided. -/
 
 section complexToReal
 
+-- fails `with_reducible_and_instances` #10906
 -- the two ways to get `Algebra ℝ ℂ` are definitionally equal
 example : (Algebra.id ℂ).complexToReal = Complex.instAlgebraComplexInstSemiringComplex := rfl
 
+-- fails `with_reducible_and_instances` #10906
 /- The complexification of an `ℝ`-algebra `A` (i.e., `ℂ ⊗[ℝ] A`) is a `ℂ`-algebra. Viewing this
 as an `ℝ`-algebra by restricting scalars agrees with the existing `ℝ`-algebra structure on the
 tensor product. -/
 open Algebra TensorProduct in
 example {A : Type*} [Ring A] [Algebra ℝ A]:
-    (leftAlgebra : Algebra ℂ (ℂ ⊗[ℝ] A)).complexToReal = leftAlgebra :=
+    (leftAlgebra : Algebra ℂ (ℂ ⊗[ℝ] A)).complexToReal = leftAlgebra := by
   rfl
 
 end complexToReal

test/instance_diamonds/normed.lean

@@ -4,5 +4,4 @@ import Mathlib.Analysis.Complex.Basic
 example :
     (NonUnitalNormedRing.toNormedAddCommGroup : NormedAddCommGroup ℂ) =
       Complex.instNormedAddCommGroupComplex := by
-  with_reducible_and_instances
-    rfl
+  with_reducible_and_instances rfl