feat(algebra/monoid_algebra): define a non-commutative version of `li…

…ft` (#4725)

* [X] define `monoid_algebra.lift_c` and `add_monoid_algebra.lift_nc` to be generalizations of `(mv_)polynomial.eval₂` to `(add_)monoid_algebra`s.
* [X] use `to_additive` in many proofs about `add_monoid_algebra`;
* [X] define `finsupp.nontrivial`, use it for `(add_)monoid_algebra.nontrivial`;
* [X] copy more lemmas about `lift` from `monoid_algebra` to `add_monoid_algebra`;
* [X] use `@[ext]` on more powerful type-specific lemmas;
* [x] fix docstrings of `(add_)monoid_algebra.lift₂`;
* [x] fix compile failures.

src/algebra/algebra/basic.lean

@@ -452,12 +452,15 @@ ring_hom.coe_monoid_hom_injective.comp coe_ring_hom_injective
 theorem coe_add_monoid_hom_injective : function.injective (coe : (A →ₐ[R] B)  → (A →+ B)) :=
 ring_hom.coe_add_monoid_hom_injective.comp coe_ring_hom_injective
 
+protected lemma congr_fun {φ₁ φ₂ : A →ₐ[R] B} (H : φ₁ = φ₂) (x : A) : φ₁ x = φ₂ x := H ▸ rfl
+protected lemma congr_arg (φ : A →ₐ[R] B) {x y : A} (h : x = y) : φ x = φ y := h ▸ rfl
+
 @[ext]
 theorem ext {φ₁ φ₂ : A →ₐ[R] B} (H : ∀ x, φ₁ x = φ₂ x) : φ₁ = φ₂ :=
 coe_fn_inj $ funext H
 
 theorem ext_iff {φ₁ φ₂ : A →ₐ[R] B} : φ₁ = φ₂ ↔ ∀ x, φ₁ x = φ₂ x :=
-⟨by { rintro rfl x, refl }, ext⟩
+⟨alg_hom.congr_fun, ext⟩
 
 @[simp]
 theorem commutes (r : R) : φ (algebra_map R A r) = algebra_map R B r := φ.commutes' r

src/algebra/category/CommRing/adjunctions.lean

@@ -47,6 +47,6 @@ def adj : free ⊣ forget CommRing :=
 adjunction.mk_of_hom_equiv
 { hom_equiv := λ X R, hom_equiv,
   hom_equiv_naturality_left_symm' :=
-    by intros; ext; apply eval₂_cast_comp f (int.cast_ring_hom Y) g x }
+    λ _ _ Y f g, ring_hom.ext $ λ x, eval₂_cast_comp f (int.cast_ring_hom Y) g x }
 
 end CommRing