R : Type u₁
inst✝⁴ : Semiring R
S : Type u₂
inst✝³ : CommSemiring S
A : Type u₃
inst✝² : Semiring A
inst✝¹ : Algebra S A
r : R → R → Prop
T : Type u₄
inst✝ : Semiring T
s : A → A → Prop
⊢ ↑{
        toRingHom :=
          {
            toMonoidHom :=
              {
                toOneHom :=
                  { toFun := fun x => { toQuot := Quot.mk (Rel s) x },
                    map_one' := (_ : { toQuot := Quot.mk (Rel s) 1 } = 1) },
                map_mul' :=
                  (_ :
                    ∀ (a a_1 : A),
                      { toQuot := Quot.mk (Rel s) (a * a_1) } =
                        { toQuot := Quot.mk (Rel s) a } * { toQuot := Quot.mk (Rel s) a_1 }) },
            map_zero' :=
              (_ :
                OneHom.toFun
                    (↑{
                        toOneHom :=
                          { toFun := fun x => { toQuot := Quot.mk (Rel s) x },
                            map_one' := (_ : { toQuot := Quot.mk (Rel s) 1 } = 1) },
                        map_mul' :=
                          (_ :
                            ∀ (a a_1 : A),
                              { toQuot := Quot.mk (Rel s) (a * a_1) } =
                                { toQuot := Quot.mk (Rel s) a } * { toQuot := Quot.mk (Rel s) a_1 }) })
                    0 =
                  0),
            map_add' :=
              (_ :
                ∀ (x y : A),
                  OneHom.toFun
                      (↑{
                          toOneHom :=
                            { toFun := fun x => { toQuot := Quot.mk (Rel s) x },
                              map_one' := (_ : { toQuot := Quot.mk (Rel s) 1 } = 1) },
                          map_mul' :=
                            (_ :
                              ∀ (a a_1 : A),
                                { toQuot := Quot.mk (Rel s) (a * a_1) } =
                                  { toQuot := Quot.mk (Rel s) a } * { toQuot := Quot.mk (Rel s) a_1 }) })
                      (x + y) =
                    OneHom.toFun
                        (↑{
                            toOneHom :=
                              { toFun := fun x => { toQuot := Quot.mk (Rel s) x },
                                map_one' := (_ : { toQuot := Quot.mk (Rel s) 1 } = 1) },
                            map_mul' :=
                              (_ :
                                ∀ (a a_1 : A),
                                  { toQuot := Quot.mk (Rel s) (a * a_1) } =
                                    { toQuot := Quot.mk (Rel s) a } * { toQuot := Quot.mk (Rel s) a_1 }) })
                        x +
                      OneHom.toFun
                        (↑{
                            toOneHom :=
                              { toFun := fun x => { toQuot := Quot.mk (Rel s) x },
                                map_one' := (_ : { toQuot := Quot.mk (Rel s) 1 } = 1) },
                            map_mul' :=
                              (_ :
                                ∀ (a a_1 : A),
                                  { toQuot := Quot.mk (Rel s) (a * a_1) } =
                                    { toQuot := Quot.mk (Rel s) a } * { toQuot := Quot.mk (Rel s) a_1 }) })
                        y) },
        commutes' :=
          (_ :
            ∀ (r : S),
              OneHom.toFun
                  (↑↑{
                        toMonoidHom :=
                          {
                            toOneHom :=
                              { toFun := fun x => { toQuot := Quot.mk (Rel s) x },
                                map_one' := (_ : { toQuot := Quot.mk (Rel s) 1 } = 1) },
                            map_mul' :=
                              (_ :
                                ∀ (a a_1 : A),
                                  { toQuot := Quot.mk (Rel s) (a * a_1) } =
                                    { toQuot := Quot.mk (Rel s) a } * { toQuot := Quot.mk (Rel s) a_1 }) },
                        map_zero' :=
                          (_ :
                            OneHom.toFun
                                (↑{
                                    toOneHom :=
                                      { toFun := fun x => { toQuot := Quot.mk (Rel s) x },
                                        map_one' := (_ : { toQuot := Quot.mk (Rel s) 1 } = 1) },
                                    map_mul' :=
                                      (_ :
                                        ∀ (a a_1 : A),
                                          { toQuot := Quot.mk (Rel s) (a * a_1) } =
                                            { toQuot := Quot.mk (Rel s) a } * { toQuot := Quot.mk (Rel s) a_1 }) })
                                0 =
                              0),
                        map_add' :=
                          (_ :
                            ∀ (x y : A),
                              OneHom.toFun
                                  (↑{
                                      toOneHom :=
                                        { toFun := fun x => { toQuot := Quot.mk (Rel s) x },
                                          map_one' := (_ : { toQuot := Quot.mk (Rel s) 1 } = 1) },
                                      map_mul' :=
                                        (_ :
                                          ∀ (a a_1 : A),
                                            { toQuot := Quot.mk (Rel s) (a * a_1) } =
                                              { toQuot := Quot.mk (Rel s) a } * { toQuot := Quot.mk (Rel s) a_1 }) })
                                  (x + y) =
                                OneHom.toFun
                                    (↑{
                                        toOneHom :=
                                          { toFun := fun x => { toQuot := Quot.mk (Rel s) x },
                                            map_one' := (_ : { toQuot := Quot.mk (Rel s) 1 } = 1) },
                                        map_mul' :=
                                          (_ :
                                            ∀ (a a_1 : A),
                                              { toQuot := Quot.mk (Rel s) (a * a_1) } =
                                                { toQuot := Quot.mk (Rel s) a } * { toQuot := Quot.mk (Rel s) a_1 }) })
                                    x +
                                  OneHom.toFun
                                    (↑{
                                        toOneHom :=
                                          { toFun := fun x => { toQuot := Quot.mk (Rel s) x },
                                            map_one' := (_ : { toQuot := Quot.mk (Rel s) 1 } = 1) },
                                        map_mul' :=
                                          (_ :
                                            ∀ (a a_1 : A),
                                              { toQuot := Quot.mk (Rel s) (a * a_1) } =
                                                { toQuot := Quot.mk (Rel s) a } * { toQuot := Quot.mk (Rel s) a_1 }) })
                                    y) })
                  (↑(algebraMap S A) r) =
                ↑(algebraMap S (RingQuot s)) r) } =
    {
      toMonoidHom :=
        {
          toOneHom :=
            { toFun := fun x => { toQuot := Quot.mk (Rel s) x },
              map_one' := (_ : { toQuot := Quot.mk (Rel s) 1 } = 1) },
          map_mul' :=
            (_ :
              ∀ (a a_1 : A),
                { toQuot := Quot.mk (Rel s) (a * a_1) } =
                  { toQuot := Quot.mk (Rel s) a } * { toQuot := Quot.mk (Rel s) a_1 }) },
      map_zero' := (_ : { toQuot := Quot.mk (Rel s) 0 } = 0),
      map_add' :=
        (_ :
          ∀ (a a_1 : A),
            { toQuot := Quot.mk (Rel s) (a + a_1) } =
              { toQuot := Quot.mk (Rel s) a } + { toQuot := Quot.mk (Rel s) a_1 }) }
R : Type u₁
inst✝⁴ : Semiring R
S : Type u₂
inst✝³ : CommSemiring S
A : Type u₃
inst✝² : Semiring A
inst✝¹ : Algebra S A
r : R → R → Prop
T : Type u₄
inst✝ : Semiring T
s : A → A → Prop
⊢ ↑(mkAlgHom S s) = mkRingHom s
simp_rw [mkAlgHom_def, mkRingHom_def]
no goals
R : Type u₁
inst✝⁴ : Semiring R
S : Type u₂
inst✝³ : CommSemiring S
A : Type u₃
inst✝² : Semiring A
inst✝¹ : Algebra S A
r : R → R → Prop
T : Type u₄
inst✝ : Semiring T
s : A → A → Prop
⊢ ↑{
        toRingHom :=
          {
            toMonoidHom :=
              {
                toOneHom :=
                  { toFun := fun x => { toQuot := Quot.mk (Rel s) x },
                    map_one' := (_ : { toQuot := Quot.mk (Rel s) 1 } = 1) },
                map_mul' :=
                  (_ :
                    ∀ (a a_1 : A),
                      { toQuot := Quot.mk (Rel s) (a * a_1) } =
                        { toQuot := Quot.mk (Rel s) a } * { toQuot := Quot.mk (Rel s) a_1 }) },
            map_zero' :=
              (_ :
                OneHom.toFun
                    (↑{
                        toOneHom :=
                          { toFun := fun x => { toQuot := Quot.mk (Rel s) x },
                            map_one' := (_ : { toQuot := Quot.mk (Rel s) 1 } = 1) },
                        map_mul' :=
                          (_ :
                            ∀ (a a_1 : A),
                              { toQuot := Quot.mk (Rel s) (a * a_1) } =
                                { toQuot := Quot.mk (Rel s) a } * { toQuot := Quot.mk (Rel s) a_1 }) })
                    0 =
                  0),
            map_add' :=
              (_ :
                ∀ (x y : A),
                  OneHom.toFun
                      (↑{
                          toOneHom :=
                            { toFun := fun x => { toQuot := Quot.mk (Rel s) x },
                              map_one' := (_ : { toQuot := Quot.mk (Rel s) 1 } = 1) },
                          map_mul' :=
                            (_ :
                              ∀ (a a_1 : A),
                                { toQuot := Quot.mk (Rel s) (a * a_1) } =
                                  { toQuot := Quot.mk (Rel s) a } * { toQuot := Quot.mk (Rel s) a_1 }) })
                      (x + y) =
                    OneHom.toFun
                        (↑{
                            toOneHom :=
                              { toFun := fun x => { toQuot := Quot.mk (Rel s) x },
                                map_one' := (_ : { toQuot := Quot.mk (Rel s) 1 } = 1) },
                            map_mul' :=
                              (_ :
                                ∀ (a a_1 : A),
                                  { toQuot := Quot.mk (Rel s) (a * a_1) } =
                                    { toQuot := Quot.mk (Rel s) a } * { toQuot := Quot.mk (Rel s) a_1 }) })
                        x +
                      OneHom.toFun
                        (↑{
                            toOneHom :=
                              { toFun := fun x => { toQuot := Quot.mk (Rel s) x },
                                map_one' := (_ : { toQuot := Quot.mk (Rel s) 1 } = 1) },
                            map_mul' :=
                              (_ :
                                ∀ (a a_1 : A),
                                  { toQuot := Quot.mk (Rel s) (a * a_1) } =
                                    { toQuot := Quot.mk (Rel s) a } * { toQuot := Quot.mk (Rel s) a_1 }) })
                        y) },
        commutes' :=
          (_ :
            ∀ (r : S),
              OneHom.toFun
                  (↑↑{
                        toMonoidHom :=
                          {
                            toOneHom :=
                              { toFun := fun x => { toQuot := Quot.mk (Rel s) x },
                                map_one' := (_ : { toQuot := Quot.mk (Rel s) 1 } = 1) },
                            map_mul' :=
                              (_ :
                                ∀ (a a_1 : A),
                                  { toQuot := Quot.mk (Rel s) (a * a_1) } =
                                    { toQuot := Quot.mk (Rel s) a } * { toQuot := Quot.mk (Rel s) a_1 }) },
                        map_zero' :=
                          (_ :
                            OneHom.toFun
                                (↑{
                                    toOneHom :=
                                      { toFun := fun x => { toQuot := Quot.mk (Rel s) x },
                                        map_one' := (_ : { toQuot := Quot.mk (Rel s) 1 } = 1) },
                                    map_mul' :=
                                      (_ :
                                        ∀ (a a_1 : A),
                                          { toQuot := Quot.mk (Rel s) (a * a_1) } =
                                            { toQuot := Quot.mk (Rel s) a } * { toQuot := Quot.mk (Rel s) a_1 }) })
                                0 =
                              0),
                        map_add' :=
                          (_ :
                            ∀ (x y : A),
                              OneHom.toFun
                                  (↑{
                                      toOneHom :=
                                        { toFun := fun x => { toQuot := Quot.mk (Rel s) x },
                                          map_one' := (_ : { toQuot := Quot.mk (Rel s) 1 } = 1) },
                                      map_mul' :=
                                        (_ :
                                          ∀ (a a_1 : A),
                                            { toQuot := Quot.mk (Rel s) (a * a_1) } =
                                              { toQuot := Quot.mk (Rel s) a } * { toQuot := Quot.mk (Rel s) a_1 }) })
                                  (x + y) =
                                OneHom.toFun
                                    (↑{
                                        toOneHom :=
                                          { toFun := fun x => { toQuot := Quot.mk (Rel s) x },
                                            map_one' := (_ : { toQuot := Quot.mk (Rel s) 1 } = 1) },
                                        map_mul' :=
                                          (_ :
                                            ∀ (a a_1 : A),
                                              { toQuot := Quot.mk (Rel s) (a * a_1) } =
                                                { toQuot := Quot.mk (Rel s) a } * { toQuot := Quot.mk (Rel s) a_1 }) })
                                    x +
                                  OneHom.toFun
                                    (↑{
                                        toOneHom :=
                                          { toFun := fun x => { toQuot := Quot.mk (Rel s) x },
                                            map_one' := (_ : { toQuot := Quot.mk (Rel s) 1 } = 1) },
                                        map_mul' :=
                                          (_ :
                                            ∀ (a a_1 : A),
                                              { toQuot := Quot.mk (Rel s) (a * a_1) } =
                                                { toQuot := Quot.mk (Rel s) a } * { toQuot := Quot.mk (Rel s) a_1 }) })
                                    y) })
                  (↑(algebraMap S A) r) =
                ↑(algebraMap S (RingQuot s)) r) } =
    {
      toMonoidHom :=
        {
          toOneHom :=
            { toFun := fun x => { toQuot := Quot.mk (Rel s) x },
              map_one' := (_ : { toQuot := Quot.mk (Rel s) 1 } = 1) },
          map_mul' :=
            (_ :
              ∀ (a a_1 : A),
                { toQuot := Quot.mk (Rel s) (a * a_1) } =
                  { toQuot := Quot.mk (Rel s) a } * { toQuot := Quot.mk (Rel s) a_1 }) },
      map_zero' := (_ : { toQuot := Quot.mk (Rel s) 0 } = 0),
      map_add' :=
        (_ :
          ∀ (a a_1 : A),
            { toQuot := Quot.mk (Rel s) (a + a_1) } =
              { toQuot := Quot.mk (Rel s) a } + { toQuot := Quot.mk (Rel s) a_1 }) }
rfl