[GOAL]
R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalSemiring A
inst✝² : Module R A
inst✝¹ : SMulCommClass R A A
inst✝ : IsScalarTower R A A
src✝ : A →ₗ[R] A →ₗ[R] A := mul R A
⊢ MulActionHom.toFun
      { toFun := src✝.toFun,
        map_smul' :=
          (_ :
            ∀ (r : R) (x : A), AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) }
      0 =
    0
[PROOFSTEP]
ext a
[GOAL]
case h
R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalSemiring A
inst✝² : Module R A
inst✝¹ : SMulCommClass R A A
inst✝ : IsScalarTower R A A
src✝ : A →ₗ[R] A →ₗ[R] A := mul R A
a : A
⊢ ↑(MulActionHom.toFun
          { toFun := src✝.toFun,
            map_smul' :=
              (_ :
                ∀ (r : R) (x : A),
                  AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) }
          0)
      a =
    ↑0 a
[PROOFSTEP]
exact zero_mul a
[GOAL]
R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalSemiring A
inst✝² : Module R A
inst✝¹ : SMulCommClass R A A
inst✝ : IsScalarTower R A A
src✝ : A →ₗ[R] A →ₗ[R] A := mul R A
⊢ ∀ (x y : A),
    MulActionHom.toFun
        {
            toMulActionHom :=
              { toFun := src✝.toFun,
                map_smul' :=
                  (_ :
                    ∀ (r : R) (x : A),
                      AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) },
            map_zero' :=
              (_ :
                MulActionHom.toFun
                    { toFun := src✝.toFun,
                      map_smul' :=
                        (_ :
                          ∀ (r : R) (x : A),
                            AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) }
                    0 =
                  0),
            map_add' :=
              (_ :
                ∀ (x y : A),
                  AddHom.toFun src✝.toAddHom (x + y) =
                    AddHom.toFun src✝.toAddHom x + AddHom.toFun src✝.toAddHom y) }.toMulActionHom
        (x * y) =
      MulActionHom.toFun
          {
              toMulActionHom :=
                { toFun := src✝.toFun,
                  map_smul' :=
                    (_ :
                      ∀ (r : R) (x : A),
                        AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) },
              map_zero' :=
                (_ :
                  MulActionHom.toFun
                      { toFun := src✝.toFun,
                        map_smul' :=
                          (_ :
                            ∀ (r : R) (x : A),
                              AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) }
                      0 =
                    0),
              map_add' :=
                (_ :
                  ∀ (x y : A),
                    AddHom.toFun src✝.toAddHom (x + y) =
                      AddHom.toFun src✝.toAddHom x + AddHom.toFun src✝.toAddHom y) }.toMulActionHom
          x *
        MulActionHom.toFun
          {
              toMulActionHom :=
                { toFun := src✝.toFun,
                  map_smul' :=
                    (_ :
                      ∀ (r : R) (x : A),
                        AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) },
              map_zero' :=
                (_ :
                  MulActionHom.toFun
                      { toFun := src✝.toFun,
                        map_smul' :=
                          (_ :
                            ∀ (r : R) (x : A),
                              AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) }
                      0 =
                    0),
              map_add' :=
                (_ :
                  ∀ (x y : A),
                    AddHom.toFun src✝.toAddHom (x + y) =
                      AddHom.toFun src✝.toAddHom x + AddHom.toFun src✝.toAddHom y) }.toMulActionHom
          y
[PROOFSTEP]
intro a b
[GOAL]
R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalSemiring A
inst✝² : Module R A
inst✝¹ : SMulCommClass R A A
inst✝ : IsScalarTower R A A
src✝ : A →ₗ[R] A →ₗ[R] A := mul R A
a b : A
⊢ MulActionHom.toFun
      {
          toMulActionHom :=
            { toFun := src✝.toFun,
              map_smul' :=
                (_ :
                  ∀ (r : R) (x : A),
                    AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) },
          map_zero' :=
            (_ :
              MulActionHom.toFun
                  { toFun := src✝.toFun,
                    map_smul' :=
                      (_ :
                        ∀ (r : R) (x : A),
                          AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) }
                  0 =
                0),
          map_add' :=
            (_ :
              ∀ (x y : A),
                AddHom.toFun src✝.toAddHom (x + y) =
                  AddHom.toFun src✝.toAddHom x + AddHom.toFun src✝.toAddHom y) }.toMulActionHom
      (a * b) =
    MulActionHom.toFun
        {
            toMulActionHom :=
              { toFun := src✝.toFun,
                map_smul' :=
                  (_ :
                    ∀ (r : R) (x : A),
                      AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) },
            map_zero' :=
              (_ :
                MulActionHom.toFun
                    { toFun := src✝.toFun,
                      map_smul' :=
                        (_ :
                          ∀ (r : R) (x : A),
                            AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) }
                    0 =
                  0),
            map_add' :=
              (_ :
                ∀ (x y : A),
                  AddHom.toFun src✝.toAddHom (x + y) =
                    AddHom.toFun src✝.toAddHom x + AddHom.toFun src✝.toAddHom y) }.toMulActionHom
        a *
      MulActionHom.toFun
        {
            toMulActionHom :=
              { toFun := src✝.toFun,
                map_smul' :=
                  (_ :
                    ∀ (r : R) (x : A),
                      AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) },
            map_zero' :=
              (_ :
                MulActionHom.toFun
                    { toFun := src✝.toFun,
                      map_smul' :=
                        (_ :
                          ∀ (r : R) (x : A),
                            AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) }
                    0 =
                  0),
            map_add' :=
              (_ :
                ∀ (x y : A),
                  AddHom.toFun src✝.toAddHom (x + y) =
                    AddHom.toFun src✝.toAddHom x + AddHom.toFun src✝.toAddHom y) }.toMulActionHom
        b
[PROOFSTEP]
ext c
[GOAL]
case h
R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalSemiring A
inst✝² : Module R A
inst✝¹ : SMulCommClass R A A
inst✝ : IsScalarTower R A A
src✝ : A →ₗ[R] A →ₗ[R] A := mul R A
a b c : A
⊢ ↑(MulActionHom.toFun
          {
              toMulActionHom :=
                { toFun := src✝.toFun,
                  map_smul' :=
                    (_ :
                      ∀ (r : R) (x : A),
                        AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) },
              map_zero' :=
                (_ :
                  MulActionHom.toFun
                      { toFun := src✝.toFun,
                        map_smul' :=
                          (_ :
                            ∀ (r : R) (x : A),
                              AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) }
                      0 =
                    0),
              map_add' :=
                (_ :
                  ∀ (x y : A),
                    AddHom.toFun src✝.toAddHom (x + y) =
                      AddHom.toFun src✝.toAddHom x + AddHom.toFun src✝.toAddHom y) }.toMulActionHom
          (a * b))
      c =
    ↑(MulActionHom.toFun
            {
                toMulActionHom :=
                  { toFun := src✝.toFun,
                    map_smul' :=
                      (_ :
                        ∀ (r : R) (x : A),
                          AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) },
                map_zero' :=
                  (_ :
                    MulActionHom.toFun
                        { toFun := src✝.toFun,
                          map_smul' :=
                            (_ :
                              ∀ (r : R) (x : A),
                                AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) }
                        0 =
                      0),
                map_add' :=
                  (_ :
                    ∀ (x y : A),
                      AddHom.toFun src✝.toAddHom (x + y) =
                        AddHom.toFun src✝.toAddHom x + AddHom.toFun src✝.toAddHom y) }.toMulActionHom
            a *
          MulActionHom.toFun
            {
                toMulActionHom :=
                  { toFun := src✝.toFun,
                    map_smul' :=
                      (_ :
                        ∀ (r : R) (x : A),
                          AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) },
                map_zero' :=
                  (_ :
                    MulActionHom.toFun
                        { toFun := src✝.toFun,
                          map_smul' :=
                            (_ :
                              ∀ (r : R) (x : A),
                                AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) }
                        0 =
                      0),
                map_add' :=
                  (_ :
                    ∀ (x y : A),
                      AddHom.toFun src✝.toAddHom (x + y) =
                        AddHom.toFun src✝.toAddHom x + AddHom.toFun src✝.toAddHom y) }.toMulActionHom
            b)
      c
[PROOFSTEP]
exact mul_assoc a b c
[GOAL]
R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalSemiring A
inst✝² : Module R A
inst✝¹ : SMulCommClass R A A
inst✝ : IsScalarTower R A A
a b : A
⊢ Commute (mulLeft R a) (mulRight R b)
[PROOFSTEP]
ext c
[GOAL]
case h
R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalSemiring A
inst✝² : Module R A
inst✝¹ : SMulCommClass R A A
inst✝ : IsScalarTower R A A
a b c : A
⊢ ↑(mulLeft R a * mulRight R b) c = ↑(mulRight R b * mulLeft R a) c
[PROOFSTEP]
exact (mul_assoc a c b).symm
[GOAL]
R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalSemiring A
inst✝² : Module R A
inst✝¹ : SMulCommClass R A A
inst✝ : IsScalarTower R A A
a b : A
⊢ mulLeft R (a * b) = comp (mulLeft R a) (mulLeft R b)
[PROOFSTEP]
ext
[GOAL]
case h
R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalSemiring A
inst✝² : Module R A
inst✝¹ : SMulCommClass R A A
inst✝ : IsScalarTower R A A
a b x✝ : A
⊢ ↑(mulLeft R (a * b)) x✝ = ↑(comp (mulLeft R a) (mulLeft R b)) x✝
[PROOFSTEP]
simp only [mulLeft_apply, comp_apply, mul_assoc]
[GOAL]
R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalSemiring A
inst✝² : Module R A
inst✝¹ : SMulCommClass R A A
inst✝ : IsScalarTower R A A
a b : A
⊢ mulRight R (a * b) = comp (mulRight R b) (mulRight R a)
[PROOFSTEP]
ext
[GOAL]
case h
R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalSemiring A
inst✝² : Module R A
inst✝¹ : SMulCommClass R A A
inst✝ : IsScalarTower R A A
a b x✝ : A
⊢ ↑(mulRight R (a * b)) x✝ = ↑(comp (mulRight R b) (mulRight R a)) x✝
[PROOFSTEP]
simp only [mulRight_apply, comp_apply, mul_assoc]
[GOAL]
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
src✝ : A →ₗ[R] A →ₗ[R] A := mul R A
⊢ AddHom.toFun src✝.toAddHom 1 = 1
[PROOFSTEP]
ext a
[GOAL]
case h
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
src✝ : A →ₗ[R] A →ₗ[R] A := mul R A
a : A
⊢ ↑(AddHom.toFun src✝.toAddHom 1) a = ↑1 a
[PROOFSTEP]
exact one_mul a
[GOAL]
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
src✝ : A →ₗ[R] A →ₗ[R] A := mul R A
⊢ ∀ (x y : A),
    OneHom.toFun { toFun := src✝.toFun, map_one' := (_ : AddHom.toFun src✝.toAddHom 1 = 1) } (x * y) =
      OneHom.toFun { toFun := src✝.toFun, map_one' := (_ : AddHom.toFun src✝.toAddHom 1 = 1) } x *
        OneHom.toFun { toFun := src✝.toFun, map_one' := (_ : AddHom.toFun src✝.toAddHom 1 = 1) } y
[PROOFSTEP]
intro a b
[GOAL]
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
src✝ : A →ₗ[R] A →ₗ[R] A := mul R A
a b : A
⊢ OneHom.toFun { toFun := src✝.toFun, map_one' := (_ : AddHom.toFun src✝.toAddHom 1 = 1) } (a * b) =
    OneHom.toFun { toFun := src✝.toFun, map_one' := (_ : AddHom.toFun src✝.toAddHom 1 = 1) } a *
      OneHom.toFun { toFun := src✝.toFun, map_one' := (_ : AddHom.toFun src✝.toAddHom 1 = 1) } b
[PROOFSTEP]
ext c
[GOAL]
case h
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
src✝ : A →ₗ[R] A →ₗ[R] A := mul R A
a b c : A
⊢ ↑(OneHom.toFun { toFun := src✝.toFun, map_one' := (_ : AddHom.toFun src✝.toAddHom 1 = 1) } (a * b)) c =
    ↑(OneHom.toFun { toFun := src✝.toFun, map_one' := (_ : AddHom.toFun src✝.toAddHom 1 = 1) } a *
          OneHom.toFun { toFun := src✝.toFun, map_one' := (_ : AddHom.toFun src✝.toAddHom 1 = 1) } b)
      c
[PROOFSTEP]
exact mul_assoc a b c
[GOAL]
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
src✝ : A →ₗ[R] A →ₗ[R] A := mul R A
⊢ OneHom.toFun
      (↑{ toOneHom := { toFun := src✝.toFun, map_one' := (_ : AddHom.toFun src✝.toAddHom 1 = 1) },
          map_mul' :=
            (_ :
              ∀ (a b : A),
                OneHom.toFun { toFun := src✝.toFun, map_one' := (_ : AddHom.toFun src✝.toAddHom 1 = 1) } (a * b) =
                  OneHom.toFun { toFun := src✝.toFun, map_one' := (_ : AddHom.toFun src✝.toAddHom 1 = 1) } a *
                    OneHom.toFun { toFun := src✝.toFun, map_one' := (_ : AddHom.toFun src✝.toAddHom 1 = 1) } b) })
      0 =
    0
[PROOFSTEP]
ext a
[GOAL]
case h
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
src✝ : A →ₗ[R] A →ₗ[R] A := mul R A
a : A
⊢ ↑(OneHom.toFun
          (↑{ toOneHom := { toFun := src✝.toFun, map_one' := (_ : AddHom.toFun src✝.toAddHom 1 = 1) },
              map_mul' :=
                (_ :
                  ∀ (a b : A),
                    OneHom.toFun { toFun := src✝.toFun, map_one' := (_ : AddHom.toFun src✝.toAddHom 1 = 1) } (a * b) =
                      OneHom.toFun { toFun := src✝.toFun, map_one' := (_ : AddHom.toFun src✝.toAddHom 1 = 1) } a *
                        OneHom.toFun { toFun := src✝.toFun, map_one' := (_ : AddHom.toFun src✝.toAddHom 1 = 1) } b) })
          0)
      a =
    ↑0 a
[PROOFSTEP]
exact zero_mul a
[GOAL]
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
src✝ : A →ₗ[R] A →ₗ[R] A := mul R A
⊢ ∀ (r : R),
    OneHom.toFun
        (↑↑{
              toMonoidHom :=
                { toOneHom := { toFun := src✝.toFun, map_one' := (_ : AddHom.toFun src✝.toAddHom 1 = 1) },
                  map_mul' :=
                    (_ :
                      ∀ (a b : A),
                        OneHom.toFun { toFun := src✝.toFun, map_one' := (_ : AddHom.toFun src✝.toAddHom 1 = 1) }
                            (a * b) =
                          OneHom.toFun { toFun := src✝.toFun, map_one' := (_ : AddHom.toFun src✝.toAddHom 1 = 1) } a *
                            OneHom.toFun { toFun := src✝.toFun, map_one' := (_ : AddHom.toFun src✝.toAddHom 1 = 1) }
                              b) },
              map_zero' :=
                (_ :
                  OneHom.toFun
                      (↑{ toOneHom := { toFun := src✝.toFun, map_one' := (_ : AddHom.toFun src✝.toAddHom 1 = 1) },
                          map_mul' :=
                            (_ :
                              ∀ (a b : A),
                                OneHom.toFun { toFun := src✝.toFun, map_one' := (_ : AddHom.toFun src✝.toAddHom 1 = 1) }
                                    (a * b) =
                                  OneHom.toFun
                                      { toFun := src✝.toFun, map_one' := (_ : AddHom.toFun src✝.toAddHom 1 = 1) } a *
                                    OneHom.toFun
                                      { toFun := src✝.toFun, map_one' := (_ : AddHom.toFun src✝.toAddHom 1 = 1) } b) })
                      0 =
                    0),
              map_add' :=
                (_ :
                  ∀ (x y : A),
                    AddHom.toFun src✝.toAddHom (x + y) = AddHom.toFun src✝.toAddHom x + AddHom.toFun src✝.toAddHom y) })
        (↑(algebraMap R A) r) =
      ↑(algebraMap R (End R A)) r
[PROOFSTEP]
intro r
[GOAL]
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
src✝ : A →ₗ[R] A →ₗ[R] A := mul R A
r : R
⊢ OneHom.toFun
      (↑↑{
            toMonoidHom :=
              { toOneHom := { toFun := src✝.toFun, map_one' := (_ : AddHom.toFun src✝.toAddHom 1 = 1) },
                map_mul' :=
                  (_ :
                    ∀ (a b : A),
                      OneHom.toFun { toFun := src✝.toFun, map_one' := (_ : AddHom.toFun src✝.toAddHom 1 = 1) } (a * b) =
                        OneHom.toFun { toFun := src✝.toFun, map_one' := (_ : AddHom.toFun src✝.toAddHom 1 = 1) } a *
                          OneHom.toFun { toFun := src✝.toFun, map_one' := (_ : AddHom.toFun src✝.toAddHom 1 = 1) } b) },
            map_zero' :=
              (_ :
                OneHom.toFun
                    (↑{ toOneHom := { toFun := src✝.toFun, map_one' := (_ : AddHom.toFun src✝.toAddHom 1 = 1) },
                        map_mul' :=
                          (_ :
                            ∀ (a b : A),
                              OneHom.toFun { toFun := src✝.toFun, map_one' := (_ : AddHom.toFun src✝.toAddHom 1 = 1) }
                                  (a * b) =
                                OneHom.toFun { toFun := src✝.toFun, map_one' := (_ : AddHom.toFun src✝.toAddHom 1 = 1) }
                                    a *
                                  OneHom.toFun
                                    { toFun := src✝.toFun, map_one' := (_ : AddHom.toFun src✝.toAddHom 1 = 1) } b) })
                    0 =
                  0),
            map_add' :=
              (_ :
                ∀ (x y : A),
                  AddHom.toFun src✝.toAddHom (x + y) = AddHom.toFun src✝.toAddHom x + AddHom.toFun src✝.toAddHom y) })
      (↑(algebraMap R A) r) =
    ↑(algebraMap R (End R A)) r
[PROOFSTEP]
ext a
[GOAL]
case h
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
src✝ : A →ₗ[R] A →ₗ[R] A := mul R A
r : R
a : A
⊢ ↑(OneHom.toFun
          (↑↑{
                toMonoidHom :=
                  { toOneHom := { toFun := src✝.toFun, map_one' := (_ : AddHom.toFun src✝.toAddHom 1 = 1) },
                    map_mul' :=
                      (_ :
                        ∀ (a b : A),
                          OneHom.toFun { toFun := src✝.toFun, map_one' := (_ : AddHom.toFun src✝.toAddHom 1 = 1) }
                              (a * b) =
                            OneHom.toFun { toFun := src✝.toFun, map_one' := (_ : AddHom.toFun src✝.toAddHom 1 = 1) } a *
                              OneHom.toFun { toFun := src✝.toFun, map_one' := (_ : AddHom.toFun src✝.toAddHom 1 = 1) }
                                b) },
                map_zero' :=
                  (_ :
                    OneHom.toFun
                        (↑{ toOneHom := { toFun := src✝.toFun, map_one' := (_ : AddHom.toFun src✝.toAddHom 1 = 1) },
                            map_mul' :=
                              (_ :
                                ∀ (a b : A),
                                  OneHom.toFun
                                      { toFun := src✝.toFun, map_one' := (_ : AddHom.toFun src✝.toAddHom 1 = 1) }
                                      (a * b) =
                                    OneHom.toFun
                                        { toFun := src✝.toFun, map_one' := (_ : AddHom.toFun src✝.toAddHom 1 = 1) } a *
                                      OneHom.toFun
                                        { toFun := src✝.toFun, map_one' := (_ : AddHom.toFun src✝.toAddHom 1 = 1) }
                                        b) })
                        0 =
                      0),
                map_add' :=
                  (_ :
                    ∀ (x y : A),
                      AddHom.toFun src✝.toAddHom (x + y) =
                        AddHom.toFun src✝.toAddHom x + AddHom.toFun src✝.toAddHom y) })
          (↑(algebraMap R A) r))
      a =
    ↑(↑(algebraMap R (End R A)) r) a
[PROOFSTEP]
exact (Algebra.smul_def r a).symm
[GOAL]
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : A
⊢ mulLeft R a = 0 ↔ a = 0
[PROOFSTEP]
constructor
[GOAL]
case mp
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : A
⊢ mulLeft R a = 0 → a = 0
[PROOFSTEP]
intro h
[GOAL]
case mpr
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : A
⊢ a = 0 → mulLeft R a = 0
[PROOFSTEP]
intro h
[GOAL]
case mp
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : A
h : mulLeft R a = 0
⊢ a = 0
[PROOFSTEP]
rw [← mul_one a, ← @mulLeft_apply R _ _ _ _ _ _ a 1, h, LinearMap.zero_apply]
[GOAL]
case mpr
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : A
h : a = 0
⊢ mulLeft R a = 0
[PROOFSTEP]
rw [h]
[GOAL]
case mpr
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : A
h : a = 0
⊢ mulLeft R 0 = 0
[PROOFSTEP]
exact mulLeft_zero_eq_zero
[GOAL]
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : A
⊢ mulRight R a = 0 ↔ a = 0
[PROOFSTEP]
constructor
[GOAL]
case mp
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : A
⊢ mulRight R a = 0 → a = 0
[PROOFSTEP]
intro h
[GOAL]
case mpr
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : A
⊢ a = 0 → mulRight R a = 0
[PROOFSTEP]
intro h
[GOAL]
case mp
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : A
h : mulRight R a = 0
⊢ a = 0
[PROOFSTEP]
rw [← one_mul a, ← @mulRight_apply R _ _ _ _ _ _ a 1, h, LinearMap.zero_apply]
[GOAL]
case mpr
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : A
h : a = 0
⊢ mulRight R a = 0
[PROOFSTEP]
rw [h]
[GOAL]
case mpr
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : A
h : a = 0
⊢ mulRight R 0 = 0
[PROOFSTEP]
exact mulRight_zero_eq_zero
[GOAL]
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
⊢ mulLeft R 1 = id
[PROOFSTEP]
ext
[GOAL]
case h
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x✝ : A
⊢ ↑(mulLeft R 1) x✝ = ↑id x✝
[PROOFSTEP]
simp only [LinearMap.id_coe, one_mul, id.def, mulLeft_apply]
[GOAL]
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
⊢ mulRight R 1 = id
[PROOFSTEP]
ext
[GOAL]
case h
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x✝ : A
⊢ ↑(mulRight R 1) x✝ = ↑id x✝
[PROOFSTEP]
simp only [LinearMap.id_coe, mul_one, id.def, mulRight_apply]
[GOAL]
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : A
n : ℕ
⊢ mulLeft R a ^ n = mulLeft R (a ^ n)
[PROOFSTEP]
simpa only [mulLeft, ← Algebra.coe_lmul_eq_mul] using ((Algebra.lmul R A).map_pow a n).symm
[GOAL]
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : A
n : ℕ
⊢ mulRight R a ^ n = mulRight R (a ^ n)
[PROOFSTEP]
simp only [mulRight, ← Algebra.coe_lmul_eq_mul]
[GOAL]
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : A
n : ℕ
⊢ ↑(flip (mul R A)) a ^ n = ↑(flip (mul R A)) (a ^ n)
[PROOFSTEP]
exact LinearMap.coe_injective (((mulRight R a).coe_pow n).symm ▸ mul_right_iterate a n)
[GOAL]
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : NoZeroDivisors A
x : A
hx : x ≠ 0
⊢ Function.Injective ↑(mulLeft R x)
[PROOFSTEP]
letI : Nontrivial A := ⟨⟨x, 0, hx⟩⟩
[GOAL]
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : NoZeroDivisors A
x : A
hx : x ≠ 0
this : Nontrivial A := { exists_pair_ne := Exists.intro x (Exists.intro 0 hx) }
⊢ Function.Injective ↑(mulLeft R x)
[PROOFSTEP]
letI := NoZeroDivisors.to_isDomain A
[GOAL]
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : NoZeroDivisors A
x : A
hx : x ≠ 0
this✝ : Nontrivial A := { exists_pair_ne := Exists.intro x (Exists.intro 0 hx) }
this : IsDomain A := NoZeroDivisors.to_isDomain A
⊢ Function.Injective ↑(mulLeft R x)
[PROOFSTEP]
exact mul_right_injective₀ hx
[GOAL]
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : NoZeroDivisors A
x : A
hx : x ≠ 0
⊢ Function.Injective ↑(mulRight R x)
[PROOFSTEP]
letI : Nontrivial A := ⟨⟨x, 0, hx⟩⟩
[GOAL]
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : NoZeroDivisors A
x : A
hx : x ≠ 0
this : Nontrivial A := { exists_pair_ne := Exists.intro x (Exists.intro 0 hx) }
⊢ Function.Injective ↑(mulRight R x)
[PROOFSTEP]
letI := NoZeroDivisors.to_isDomain A
[GOAL]
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : NoZeroDivisors A
x : A
hx : x ≠ 0
this✝ : Nontrivial A := { exists_pair_ne := Exists.intro x (Exists.intro 0 hx) }
this : IsDomain A := NoZeroDivisors.to_isDomain A
⊢ Function.Injective ↑(mulRight R x)
[PROOFSTEP]
exact mul_left_injective₀ hx
[GOAL]
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : NoZeroDivisors A
x : A
hx : x ≠ 0
⊢ Function.Injective ↑(↑(mul R A) x)
[PROOFSTEP]
letI : Nontrivial A := ⟨⟨x, 0, hx⟩⟩
[GOAL]
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : NoZeroDivisors A
x : A
hx : x ≠ 0
this : Nontrivial A := { exists_pair_ne := Exists.intro x (Exists.intro 0 hx) }
⊢ Function.Injective ↑(↑(mul R A) x)
[PROOFSTEP]
letI := NoZeroDivisors.to_isDomain A
[GOAL]
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : NoZeroDivisors A
x : A
hx : x ≠ 0
this✝ : Nontrivial A := { exists_pair_ne := Exists.intro x (Exists.intro 0 hx) }
this : IsDomain A := NoZeroDivisors.to_isDomain A
⊢ Function.Injective ↑(↑(mul R A) x)
[PROOFSTEP]
exact mul_right_injective₀ hx
