R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
m : M
⊢ ↑(RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m) =
    ↑{
          toAddHom :=
            { toFun := fun m => ↑(RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m),
              map_add' :=
                (_ :
                  ∀ (x y : M),
                    (fun m => ↑(RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m)) (x + y) =
                      (fun m => ↑(RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m)) x +
                        (fun m => ↑(RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m)) y) },
          map_smul' :=
            (_ :
              ∀ (r : R) (x : M),
                AddHom.toFun
                    { toFun := fun m => ↑(RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m),
                      map_add' :=
                        (_ :
                          ∀ (x y : M),
                            (fun m => ↑(RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m)) (x + y) =
                              (fun m => ↑(RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m)) x +
                                (fun m => ↑(RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m)) y) }
                    (r • x) =
                  ↑(RingHom.id R) r •
                    AddHom.toFun
                      { toFun := fun m => ↑(RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m),
                        map_add' :=
                          (_ :
                            ∀ (x y : M),
                              (fun m => ↑(RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m)) (x + y) =
                                (fun m => ↑(RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m)) x +
                                  (fun m => ↑(RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m)) y) }
                      x) }
      m
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
m : M
⊢ ↑(RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m) = ↑(ι R) m
rw [ι]
no goals
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
m : M
⊢ ↑(RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m) =
    ↑{
          toAddHom :=
            { toFun := fun m => ↑(RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m),
              map_add' :=
                (_ :
                  ∀ (x y : M),
                    (fun m => ↑(RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m)) (x + y) =
                      (fun m => ↑(RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m)) x +
                        (fun m => ↑(RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m)) y) },
          map_smul' :=
            (_ :
              ∀ (r : R) (x : M),
                AddHom.toFun
                    { toFun := fun m => ↑(RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m),
                      map_add' :=
                        (_ :
                          ∀ (x y : M),
                            (fun m => ↑(RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m)) (x + y) =
                              (fun m => ↑(RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m)) x +
                                (fun m => ↑(RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m)) y) }
                    (r • x) =
                  ↑(RingHom.id R) r •
                    AddHom.toFun
                      { toFun := fun m => ↑(RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m),
                        map_add' :=
                          (_ :
                            ∀ (x y : M),
                              (fun m => ↑(RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m)) (x + y) =
                                (fun m => ↑(RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m)) x +
                                  (fun m => ↑(RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m)) y) }
                      x) }
      m
rfl