feat(Algebra/Adjoin): CoeDep instances for Algebra.adjoin on singletons (leanprover-community#36439)

It is a common occurrence that I need to consider an element `x` or some polynomial evaluated in `x`, `p.eval x` as an element of `Algebra.adjoin R {x}`.

This makes it so that we can write
- `(x : adjoin R {x})` instead of `⟨x, self_mem_adjoin_singleton A x⟩`
- `(p.eval x : adjoin R {x})` instead of `⟨p.aeval x, aeval_mem_adjoin_singleton A x⟩`

This is particularly useful when we need to write the type anyways, so that we need not to write `(⟨p.aeval x, aeval_mem_adjoin_singleton A x⟩ : adjoin R {x})` anymore.

Co-authored-by: María Inés de Frutos Fernández <[mariaines.dff@gmail.com](mailto:mariaines.dff@gmail.com)>
Co-authored-by: Xavier Genereux <xaviergenereux@hotmail.com>

Author: 2 people

Mathlib/Algebra/Algebra/Subalgebra/Lattice.lean

@@ -517,6 +517,34 @@ theorem subset_adjoin : s ⊆ adjoin R s :=
 @[aesop 80% (rule_sets := [SetLike])]
 theorem mem_adjoin_of_mem {s : Set A} {x : A} (hx : x ∈ s) : x ∈ adjoin R s := subset_adjoin hx
 
+/-
+The following set-up allows one to write `xₖ : R[x₁, ..., xₙ]` instead of
+`(⟨xₖ, "membership proof"⟩ : R[x₁, ..., xₙ])`.
+
+The idea is to recurse through the list of `x₁, ..., xₙ` until we find the appropriate `xₖ`.
+By design, it only triggers if the set is of the form `insert x₁ (insert x₂ (...(s)))` or
+`{x₁, ..., xₙ}`.
+-/
+
+variable {α : Type*}
+
+/-- Supporting class for coercions `xₖ : R[x₁, ..., xₙ]`. -/
+class CoeAdjoinAux (x : α) (s : Set α) : Prop where mem : x ∈ s
+
+scoped instance (x : α) : CoeAdjoinAux x {x} := ⟨Set.mem_singleton x⟩
+
+scoped instance (x : α) (s : Set α) : CoeAdjoinAux x (insert x s) := ⟨Set.mem_insert x s⟩
+
+scoped instance (x y : α) (s : Set α) [CoeAdjoinAux x s] : CoeAdjoinAux x (insert y s) :=
+  ⟨Set.mem_insert_of_mem y CoeAdjoinAux.mem⟩
+
+/-- Enables notation `xₖ : R[x₁, ..., xₙ]` instead of
+`(⟨xₖ, "membership proof"⟩ : R[x₁, ..., xₙ])`. -/
+scoped instance {A B : Type*} [CommSemiring A] [Semiring B] [Algebra A B]
+    (s : Set B) (x : B) [CoeAdjoinAux x s] :
+    CoeDep B x (adjoin A s) where
+  coe := ⟨x, mem_adjoin_of_mem CoeAdjoinAux.mem⟩
+
 theorem adjoin_le {S : Subalgebra R A} (H : s ⊆ S) : adjoin R s ≤ S :=
   Algebra.gc.l_le H
 

Mathlib/RingTheory/Adjoin/Polynomial/Basic.lean

@@ -57,6 +57,10 @@ theorem adjoin_singleton_eq_range_aeval (x : A) :
 theorem _root_.Polynomial.aeval_mem_adjoin_singleton : aeval x p ∈ adjoin R {x} := by
   simp [adjoin_singleton_eq_range_aeval]
 
+instance {A B : Type*} [CommSemiring A] [Semiring B] [Algebra A B] (x : B) (p : Polynomial A) :
+    CoeDep B (p.aeval x) (Algebra.adjoin A {x}) where
+  coe := ⟨p.aeval x, aeval_mem_adjoin_singleton A x⟩
+
 theorem adjoin_mem_exists_aeval {a : A} (h : a ∈ R[x]) :
     ∃ p : R[X], aeval x p = a := by
   rw [Algebra.adjoin_singleton_eq_range_aeval] at h
@@ -74,9 +78,7 @@ Proving a fact about `a : adjoin R {x}` is the same as proving it for
 `aeval x p` where `p`is an arbitrary polynomial. -/
 @[elab_as_elim]
 theorem adjoin_singleton_induction {M : (adjoin R {x}) → Prop}
-    (a : adjoin R {x}) (f : ∀ (p : Polynomial R),
-    M (⟨aeval x p, aeval_mem_adjoin_singleton R x⟩ : adjoin R {x})) :
-    M a := by
+    (a : adjoin R {x}) (f : ∀ (p : Polynomial R), M (aeval x p : adjoin R {x})) : M a := by
   obtain ⟨p, hp⟩ := Algebra.adjoin_eq_exists_aeval _ x a
   grind