map to quotient ring diamond

Stream: mathlib4

[Kevin Buzzard]

I'm not sure if this is important. If $I$ is an ideal of a commutative ring $R$ then $R/I$ is an $R$-algebra and there's also a bespoke coercion $R\to R/I$. If you open scoped algebraMap then you get a second coercion $R\to R/I$ which is defeq but only after some unfolding. However I'm not convinced that the typeclass inference system will be stuck on this so maybe it doesn't matter?

import Mathlib.RingTheory.Ideal.QuotientOperations

variable (R : Type*) [CommRing R] (I : Ideal R)

#synth Algebra R (R ⧸ I) -- works

#synth Coe R (R ⧸ I) -- Ideal.Quotient.instCoeQuotient, i.e. it's Ideal.Quotient.mk

example (r : R) : (r : R ⧸ I) = 37 := sorry -- ⊢ (Ideal.Quotient.mk I) r = 37

open scoped algebraMap -- gives a coercion for *any* Algebra structure including Algebra R (R ⧸ I)

variable (A B : Type*) [CommRing A] [CommRing B] [Algebra A B]

#synth CoeHTCT A B -- algebraMap.coeHTCT A B, and it's Algebra.cast

example (a : A) : (a : B) = 37 := sorry -- ⊢ Algebra.cast a = b

-- does this matter?
example (r : R) : (Algebra.cast r : R ⧸ I) = (Ideal.Quotient.mk I) r := rfl -- works
example (r : R) : (Algebra.cast r : R ⧸ I) = (Ideal.Quotient.mk I) r := by with_reducible_and_instances rfl -- fails

[Kevin Buzzard]

The reason this is affecting me now is that there is currently two normal forms for the coercion, so I'm having to write duplicate lemmas, e.g.

lemma _root_.Ideal.Quotient.coe_eq_coe_iff_sub_mem {R : Type*} [CommRing R] {I : Ideal R}
    (x y : R) : (Algebra.cast x : R ⧸ I) = y ↔ x - y ∈ I := Ideal.Quotient.mk_eq_mk_iff_sub_mem _ _