[GOAL]
I : Type u
R : Type u_1
f✝ : I → Type v
x y : (i : I) → f✝ i
i : I
r : CommSemiring R
s : (i : I) → Semiring (f✝ i)
inst✝ : (i : I) → Algebra R (f✝ i)
src✝ : R →+* (i : I) → f✝ i := Pi.ringHom fun i => algebraMap R (f✝ i)
a : R
f : (fun x => (i : I) → f✝ i) a
⊢ ↑{ toMonoidHom := ↑src✝, map_zero' := (_ : OneHom.toFun (↑↑src✝) 0 = 0),
            map_add' :=
              (_ : ∀ (x y : R), OneHom.toFun (↑↑src✝) (x + y) = OneHom.toFun (↑↑src✝) x + OneHom.toFun (↑↑src✝) y) }
        a *
      f =
    f *
      ↑{ toMonoidHom := ↑src✝, map_zero' := (_ : OneHom.toFun (↑↑src✝) 0 = 0),
            map_add' :=
              (_ : ∀ (x y : R), OneHom.toFun (↑↑src✝) (x + y) = OneHom.toFun (↑↑src✝) x + OneHom.toFun (↑↑src✝) y) }
        a
[PROOFSTEP]
ext
[GOAL]
case h
I : Type u
R : Type u_1
f✝ : I → Type v
x y : (i : I) → f✝ i
i : I
r : CommSemiring R
s : (i : I) → Semiring (f✝ i)
inst✝ : (i : I) → Algebra R (f✝ i)
src✝ : R →+* (i : I) → f✝ i := Pi.ringHom fun i => algebraMap R (f✝ i)
a : R
f : (fun x => (i : I) → f✝ i) a
x✝ : I
⊢ (↑{ toMonoidHom := ↑src✝, map_zero' := (_ : OneHom.toFun (↑↑src✝) 0 = 0),
              map_add' :=
                (_ : ∀ (x y : R), OneHom.toFun (↑↑src✝) (x + y) = OneHom.toFun (↑↑src✝) x + OneHom.toFun (↑↑src✝) y) }
          a *
        f)
      x✝ =
    (f *
        ↑{ toMonoidHom := ↑src✝, map_zero' := (_ : OneHom.toFun (↑↑src✝) 0 = 0),
              map_add' :=
                (_ : ∀ (x y : R), OneHom.toFun (↑↑src✝) (x + y) = OneHom.toFun (↑↑src✝) x + OneHom.toFun (↑↑src✝) y) }
          a)
      x✝
[PROOFSTEP]
simp [Algebra.commutes]
[GOAL]
I : Type u
R : Type u_1
f✝ : I → Type v
x y : (i : I) → f✝ i
i : I
r : CommSemiring R
s : (i : I) → Semiring (f✝ i)
inst✝ : (i : I) → Algebra R (f✝ i)
src✝ : R →+* (i : I) → f✝ i := Pi.ringHom fun i => algebraMap R (f✝ i)
a : R
f : (fun x => (i : I) → f✝ i) a
⊢ a • f =
    ↑{ toMonoidHom := ↑src✝, map_zero' := (_ : OneHom.toFun (↑↑src✝) 0 = 0),
            map_add' :=
              (_ : ∀ (x y : R), OneHom.toFun (↑↑src✝) (x + y) = OneHom.toFun (↑↑src✝) x + OneHom.toFun (↑↑src✝) y) }
        a *
      f
[PROOFSTEP]
ext
[GOAL]
case h
I : Type u
R : Type u_1
f✝ : I → Type v
x y : (i : I) → f✝ i
i : I
r : CommSemiring R
s : (i : I) → Semiring (f✝ i)
inst✝ : (i : I) → Algebra R (f✝ i)
src✝ : R →+* (i : I) → f✝ i := Pi.ringHom fun i => algebraMap R (f✝ i)
a : R
f : (fun x => (i : I) → f✝ i) a
x✝ : I
⊢ (a • f) x✝ =
    (↑{ toMonoidHom := ↑src✝, map_zero' := (_ : OneHom.toFun (↑↑src✝) 0 = 0),
              map_add' :=
                (_ : ∀ (x y : R), OneHom.toFun (↑↑src✝) (x + y) = OneHom.toFun (↑↑src✝) x + OneHom.toFun (↑↑src✝) y) }
          a *
        f)
      x✝
[PROOFSTEP]
simp [Algebra.smul_def]
[GOAL]
R : Type u
A : Type v
B : Type w
I✝ : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : A →ₐ[R] B
I : Type u_2
src✝ : (I → A) →+* I → B := RingHom.compLeft (↑f) I
c : R
⊢ OneHom.toFun
      (↑↑{
            toMonoidHom :=
              { toOneHom := { toFun := fun h => ↑f ∘ h, map_one' := (_ : OneHom.toFun (↑↑src✝) 1 = 1) },
                map_mul' :=
                  (_ :
                    ∀ (x y : I → A),
                      OneHom.toFun (↑↑src✝) (x * y) = OneHom.toFun (↑↑src✝) x * OneHom.toFun (↑↑src✝) y) },
            map_zero' := (_ : OneHom.toFun (↑↑src✝) 0 = 0),
            map_add' :=
              (_ :
                ∀ (x y : I → A), OneHom.toFun (↑↑src✝) (x + y) = OneHom.toFun (↑↑src✝) x + OneHom.toFun (↑↑src✝) y) })
      (↑(algebraMap R (I → A)) c) =
    ↑(algebraMap R (I → B)) c
[PROOFSTEP]
ext
[GOAL]
case h
R : Type u
A : Type v
B : Type w
I✝ : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : A →ₐ[R] B
I : Type u_2
src✝ : (I → A) →+* I → B := RingHom.compLeft (↑f) I
c : R
x✝ : I
⊢ OneHom.toFun
      (↑↑{
            toMonoidHom :=
              { toOneHom := { toFun := fun h => ↑f ∘ h, map_one' := (_ : OneHom.toFun (↑↑src✝) 1 = 1) },
                map_mul' :=
                  (_ :
                    ∀ (x y : I → A),
                      OneHom.toFun (↑↑src✝) (x * y) = OneHom.toFun (↑↑src✝) x * OneHom.toFun (↑↑src✝) y) },
            map_zero' := (_ : OneHom.toFun (↑↑src✝) 0 = 0),
            map_add' :=
              (_ :
                ∀ (x y : I → A), OneHom.toFun (↑↑src✝) (x + y) = OneHom.toFun (↑↑src✝) x + OneHom.toFun (↑↑src✝) y) })
      (↑(algebraMap R (I → A)) c) x✝ =
    ↑(algebraMap R (I → B)) c x✝
[PROOFSTEP]
exact f.commutes' c
[GOAL]
R : Type u_1
ι : Type u_2
A₁ : ι → Type u_3
A₂ : ι → Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : (i : ι) → Semiring (A₁ i)
inst✝² : (i : ι) → Semiring (A₂ i)
inst✝¹ : (i : ι) → Algebra R (A₁ i)
inst✝ : (i : ι) → Algebra R (A₂ i)
e : (i : ι) → A₁ i ≃ₐ[R] A₂ i
src✝ : ((i : ι) → A₁ i) ≃+* ((i : ι) → A₂ i) := RingEquiv.piCongrRight fun i => toRingEquiv (e i)
r : R
⊢ Equiv.toFun
      { toFun := fun x j => ↑(e j) (x j), invFun := fun x j => ↑(symm (e j)) (x j),
        left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
        right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
      (↑(algebraMap R ((i : ι) → A₁ i)) r) =
    ↑(algebraMap R ((i : ι) → A₂ i)) r
[PROOFSTEP]
ext i
[GOAL]
case h
R : Type u_1
ι : Type u_2
A₁ : ι → Type u_3
A₂ : ι → Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : (i : ι) → Semiring (A₁ i)
inst✝² : (i : ι) → Semiring (A₂ i)
inst✝¹ : (i : ι) → Algebra R (A₁ i)
inst✝ : (i : ι) → Algebra R (A₂ i)
e : (i : ι) → A₁ i ≃ₐ[R] A₂ i
src✝ : ((i : ι) → A₁ i) ≃+* ((i : ι) → A₂ i) := RingEquiv.piCongrRight fun i => toRingEquiv (e i)
r : R
i : ι
⊢ Equiv.toFun
      { toFun := fun x j => ↑(e j) (x j), invFun := fun x j => ↑(symm (e j)) (x j),
        left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
        right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
      (↑(algebraMap R ((i : ι) → A₁ i)) r) i =
    ↑(algebraMap R ((i : ι) → A₂ i)) r i
[PROOFSTEP]
simp
