From 056a9d193fadb2bb80c7daa62fc9cb34a0627214 Mon Sep 17 00:00:00 2001 From: Matthew Robert Ballard Date: Sat, 24 Feb 2024 22:44:03 +0000 Subject: [PATCH] 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 --- .../Algebra/Algebra/NonUnitalSubalgebra.lean | 7 +- Mathlib/Algebra/FreeAlgebra.lean | 6 +- Mathlib/Data/Complex/Module.lean | 9 ++- Mathlib/Data/ZMod/IntUnitsPower.lean | 3 +- Mathlib/GroupTheory/GroupAction/Opposite.lean | 4 +- Mathlib/GroupTheory/Submonoid/Center.lean | 5 +- .../LinearAlgebra/CliffordAlgebra/Basic.lean | 2 + .../LinearAlgebra/TensorAlgebra/Basic.lean | 2 + Mathlib/MeasureTheory/Function/LpSpace.lean | 8 +-- Mathlib/NumberTheory/Cyclotomic/Basic.lean | 9 ++- Mathlib/NumberTheory/NumberField/Basic.lean | 2 +- .../RingTheory/NonUnitalSubring/Basic.lean | 7 +- .../NonUnitalSubsemiring/Basic.lean | 2 +- Mathlib/RingTheory/Subsemiring/Basic.lean | 4 +- Mathlib/RingTheory/TensorProduct.lean | 4 +- test/instance_diamonds.lean | 65 +++++++++++-------- test/instance_diamonds/normed.lean | 3 +- 17 files changed, 80 insertions(+), 62 deletions(-) diff --git a/Mathlib/Algebra/Algebra/NonUnitalSubalgebra.lean b/Mathlib/Algebra/Algebra/NonUnitalSubalgebra.lean index fbdb6fafeaeadc..38c7ce516a3508 100644 --- a/Mathlib/Algebra/Algebra/NonUnitalSubalgebra.lean +++ b/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] diff --git a/Mathlib/Algebra/FreeAlgebra.lean b/Mathlib/Algebra/FreeAlgebra.lean index 7f7c969ab79219..aa04fbcd2ef210 100644 --- a/Mathlib/Algebra/FreeAlgebra.lean +++ b/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 diff --git a/Mathlib/Data/Complex/Module.lean b/Mathlib/Data/Complex/Module.lean index bfbf5f93b7e2a8..fb6e1fef5ca819 100644 --- a/Mathlib/Data/Complex/Module.lean +++ b/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) : diff --git a/Mathlib/Data/ZMod/IntUnitsPower.lean b/Mathlib/Data/ZMod/IntUnitsPower.lean index 3ff0f55e78dc70..4a84e5c74e4114 100644 --- a/Mathlib/Data/ZMod/IntUnitsPower.lean +++ b/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 diff --git a/Mathlib/GroupTheory/GroupAction/Opposite.lean b/Mathlib/GroupTheory/GroupAction/Opposite.lean index 45376cc60d9b24..0b78d64d5eefb8 100644 --- a/Mathlib/GroupTheory/GroupAction/Opposite.lean +++ b/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."] diff --git a/Mathlib/GroupTheory/Submonoid/Center.lean b/Mathlib/GroupTheory/Submonoid/Center.lean index 2adcd6bb92f3de..a7ee21f510fa18 100644 --- a/Mathlib/GroupTheory/Submonoid/Center.lean +++ b/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 diff --git a/Mathlib/LinearAlgebra/CliffordAlgebra/Basic.lean b/Mathlib/LinearAlgebra/CliffordAlgebra/Basic.lean index b7460d7515774e..b6f7822990687c 100644 --- a/Mathlib/LinearAlgebra/CliffordAlgebra/Basic.lean +++ b/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 diff --git a/Mathlib/LinearAlgebra/TensorAlgebra/Basic.lean b/Mathlib/LinearAlgebra/TensorAlgebra/Basic.lean index 5f8955de54a3b2..b488a21b59d8bb 100644 --- a/Mathlib/LinearAlgebra/TensorAlgebra/Basic.lean +++ b/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 diff --git a/Mathlib/MeasureTheory/Function/LpSpace.lean b/Mathlib/MeasureTheory/Function/LpSpace.lean index c459c668c9c33f..c88aaf1a9dc90e 100644 --- a/Mathlib/MeasureTheory/Function/LpSpace.lean +++ b/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 diff --git a/Mathlib/NumberTheory/Cyclotomic/Basic.lean b/Mathlib/NumberTheory/Cyclotomic/Basic.lean index 66aac019f52675..38082ca4c26132 100644 --- a/Mathlib/NumberTheory/Cyclotomic/Basic.lean +++ b/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 diff --git a/Mathlib/NumberTheory/NumberField/Basic.lean b/Mathlib/NumberTheory/NumberField/Basic.lean index 1295783da7b739..467ae087723daf 100644 --- a/Mathlib/NumberTheory/NumberField/Basic.lean +++ b/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 diff --git a/Mathlib/RingTheory/NonUnitalSubring/Basic.lean b/Mathlib/RingTheory/NonUnitalSubring/Basic.lean index 0924da997afb8b..bc58475e27b57a 100644 --- a/Mathlib/RingTheory/NonUnitalSubring/Basic.lean +++ b/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 diff --git a/Mathlib/RingTheory/NonUnitalSubsemiring/Basic.lean b/Mathlib/RingTheory/NonUnitalSubsemiring/Basic.lean index 00c9ba12d5f499..37143accbde934 100644 --- a/Mathlib/RingTheory/NonUnitalSubsemiring/Basic.lean +++ b/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] diff --git a/Mathlib/RingTheory/Subsemiring/Basic.lean b/Mathlib/RingTheory/Subsemiring/Basic.lean index 6bc2b61bc91753..fba1846dde5206 100644 --- a/Mathlib/RingTheory/Subsemiring/Basic.lean +++ b/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 diff --git a/Mathlib/RingTheory/TensorProduct.lean b/Mathlib/RingTheory/TensorProduct.lean index f4a120656b655e..a99101b390e893 100644 --- a/Mathlib/RingTheory/TensorProduct.lean +++ b/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 diff --git a/test/instance_diamonds.lean b/test/instance_diamonds.lean index 1db4b61effd72f..b3d427ac9c23d6 100644 --- a/test/instance_diamonds.lean +++ b/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 diff --git a/test/instance_diamonds/normed.lean b/test/instance_diamonds/normed.lean index 005213193103c5..4623decf516336 100644 --- a/test/instance_diamonds/normed.lean +++ b/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