[GOAL]
R : Type u_1
A : Type u_2
inst✝² : Monoid R
inst✝¹ : NonUnitalNonAssocSemiring A
inst✝ : DistribMulAction R A
r₁ r₂ : R
⊢ 0 = r₁ • 0 + r₂ • 0 + 0 * 0
[PROOFSTEP]
simp only [smul_zero, add_zero, mul_zero]
[GOAL]
R : Type u_1
A : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid A
inst✝¹ : Mul A
inst✝ : SMulWithZero R A
a₁ a₂ : A
⊢ a₁ * a₂ = 0 • a₂ + 0 • a₁ + a₁ * a₂
[PROOFSTEP]
simp only [zero_smul, zero_add]
[GOAL]
R : Type u_1
A : Type u_2
inst✝² : Semiring R
inst✝¹ : NonUnitalNonAssocSemiring A
inst✝ : DistribMulAction R A
r : R
a : A
⊢ r • a + 0 • 0 + 0 * a = r • a
[PROOFSTEP]
rw [smul_zero, add_zero, zero_mul, add_zero]
[GOAL]
R : Type u_1
A : Type u_2
inst✝² : Semiring R
inst✝¹ : NonUnitalNonAssocSemiring A
inst✝ : DistribMulAction R A
r : R
a : A
⊢ 0 • 0 + r • a + a * 0 = r • a
[PROOFSTEP]
rw [smul_zero, zero_add, mul_zero, add_zero]
[GOAL]
R : Type u_1
A : Type u_2
inst✝² : Monoid R
inst✝¹ : NonUnitalNonAssocSemiring A
inst✝ : DistribMulAction R A
src✝¹ : One (Unitization R A) := instOne
src✝ : Mul (Unitization R A) := instMul
x : Unitization R A
⊢ 1 • x.snd + x.fst • 0 + 0 * x.snd = x.snd
[PROOFSTEP]
rw [one_smul, smul_zero, add_zero, zero_mul, add_zero]
[GOAL]
R : Type u_1
A : Type u_2
inst✝² : Monoid R
inst✝¹ : NonUnitalNonAssocSemiring A
inst✝ : DistribMulAction R A
src✝¹ : One (Unitization R A) := instOne
src✝ : Mul (Unitization R A) := instMul
x : Unitization R A
⊢ x.fst • 0 + 1 • x.snd + x.snd * 0 = x.snd
[PROOFSTEP]
rw [smul_zero, zero_add, one_smul, mul_zero, add_zero]
[GOAL]
R : Type u_1
A : Type u_2
inst✝² : Semiring R
inst✝¹ : NonUnitalNonAssocSemiring A
inst✝ : Module R A
src✝¹ : MulOneClass (Unitization R A) := instMulOneClass
src✝ : AddCommMonoid (Unitization R A) := instAddCommMonoid
x₁ x₂ x₃ : Unitization R A
⊢ x₁.fst • (x₂.snd + x₃.snd) + (x₂.fst + x₃.fst) • x₁.snd + x₁.snd * (x₂.snd + x₃.snd) =
    x₁.fst • x₂.snd + x₂.fst • x₁.snd + x₁.snd * x₂.snd + (x₁.fst • x₃.snd + x₃.fst • x₁.snd + x₁.snd * x₃.snd)
[PROOFSTEP]
simp only [smul_add, add_smul, mul_add]
[GOAL]
R : Type u_1
A : Type u_2
inst✝² : Semiring R
inst✝¹ : NonUnitalNonAssocSemiring A
inst✝ : Module R A
src✝¹ : MulOneClass (Unitization R A) := instMulOneClass
src✝ : AddCommMonoid (Unitization R A) := instAddCommMonoid
x₁ x₂ x₃ : Unitization R A
⊢ x₁.fst • x₂.snd + x₁.fst • x₃.snd + (x₂.fst • x₁.snd + x₃.fst • x₁.snd) + (x₁.snd * x₂.snd + x₁.snd * x₃.snd) =
    x₁.fst • x₂.snd + x₂.fst • x₁.snd + x₁.snd * x₂.snd + (x₁.fst • x₃.snd + x₃.fst • x₁.snd + x₁.snd * x₃.snd)
[PROOFSTEP]
abel
[GOAL]
R : Type u_1
A : Type u_2
inst✝² : Semiring R
inst✝¹ : NonUnitalNonAssocSemiring A
inst✝ : Module R A
src✝¹ : MulOneClass (Unitization R A) := instMulOneClass
src✝ : AddCommMonoid (Unitization R A) := instAddCommMonoid
x₁ x₂ x₃ : Unitization R A
⊢ x₁.fst • x₂.snd + x₁.fst • x₃.snd + (x₂.fst • x₁.snd + x₃.fst • x₁.snd) + (x₁.snd * x₂.snd + x₁.snd * x₃.snd) =
    x₁.fst • x₂.snd + x₂.fst • x₁.snd + x₁.snd * x₂.snd + (x₁.fst • x₃.snd + x₃.fst • x₁.snd + x₁.snd * x₃.snd)
[PROOFSTEP]
abel
[GOAL]
R : Type u_1
A : Type u_2
inst✝² : Semiring R
inst✝¹ : NonUnitalNonAssocSemiring A
inst✝ : Module R A
src✝¹ : MulOneClass (Unitization R A) := instMulOneClass
src✝ : AddCommMonoid (Unitization R A) := instAddCommMonoid
x₁ x₂ x₃ : Unitization R A
⊢ (x₁.fst + x₂.fst) • x₃.snd + x₃.fst • (x₁.snd + x₂.snd) + (x₁.snd + x₂.snd) * x₃.snd =
    x₁.fst • x₃.snd + x₃.fst • x₁.snd + x₁.snd * x₃.snd + (x₂.fst • x₃.snd + x₃.fst • x₂.snd + x₂.snd * x₃.snd)
[PROOFSTEP]
simp only [add_smul, smul_add, add_mul]
[GOAL]
R : Type u_1
A : Type u_2
inst✝² : Semiring R
inst✝¹ : NonUnitalNonAssocSemiring A
inst✝ : Module R A
src✝¹ : MulOneClass (Unitization R A) := instMulOneClass
src✝ : AddCommMonoid (Unitization R A) := instAddCommMonoid
x₁ x₂ x₃ : Unitization R A
⊢ x₁.fst • x₃.snd + x₂.fst • x₃.snd + (x₃.fst • x₁.snd + x₃.fst • x₂.snd) + (x₁.snd * x₃.snd + x₂.snd * x₃.snd) =
    x₁.fst • x₃.snd + x₃.fst • x₁.snd + x₁.snd * x₃.snd + (x₂.fst • x₃.snd + x₃.fst • x₂.snd + x₂.snd * x₃.snd)
[PROOFSTEP]
abel
[GOAL]
R : Type u_1
A : Type u_2
inst✝² : Semiring R
inst✝¹ : NonUnitalNonAssocSemiring A
inst✝ : Module R A
src✝¹ : MulOneClass (Unitization R A) := instMulOneClass
src✝ : AddCommMonoid (Unitization R A) := instAddCommMonoid
x₁ x₂ x₃ : Unitization R A
⊢ x₁.fst • x₃.snd + x₂.fst • x₃.snd + (x₃.fst • x₁.snd + x₃.fst • x₂.snd) + (x₁.snd * x₃.snd + x₂.snd * x₃.snd) =
    x₁.fst • x₃.snd + x₃.fst • x₁.snd + x₁.snd * x₃.snd + (x₂.fst • x₃.snd + x₃.fst • x₂.snd + x₂.snd * x₃.snd)
[PROOFSTEP]
abel
[GOAL]
R : Type u_1
A : Type u_2
inst✝² : Semiring R
inst✝¹ : NonUnitalNonAssocSemiring A
inst✝ : Module R A
src✝¹ : MulOneClass (Unitization R A) := instMulOneClass
src✝ : AddCommMonoid (Unitization R A) := instAddCommMonoid
x : Unitization R A
⊢ 0 • x.snd + x.fst • 0 + 0 * x.snd = 0
[PROOFSTEP]
rw [zero_smul, zero_add, smul_zero, zero_mul, add_zero]
[GOAL]
R : Type u_1
A : Type u_2
inst✝² : Semiring R
inst✝¹ : NonUnitalNonAssocSemiring A
inst✝ : Module R A
src✝¹ : MulOneClass (Unitization R A) := instMulOneClass
src✝ : AddCommMonoid (Unitization R A) := instAddCommMonoid
x : Unitization R A
⊢ x.fst • 0 + 0 • x.snd + x.snd * 0 = 0
[PROOFSTEP]
rw [smul_zero, zero_add, zero_smul, mul_zero, add_zero]
[GOAL]
R : Type u_1
A : Type u_2
inst✝⁴ : CommMonoid R
inst✝³ : NonUnitalSemiring A
inst✝² : DistribMulAction R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
src✝ : MulOneClass (Unitization R A) := instMulOneClass
x y z : Unitization R A
⊢ (x.fst * y.fst) • z.snd + z.fst • (x.fst • y.snd + y.fst • x.snd + x.snd * y.snd) +
      (x.fst • y.snd + y.fst • x.snd + x.snd * y.snd) * z.snd =
    x.fst • (y.fst • z.snd + z.fst • y.snd + y.snd * z.snd) + (y.fst * z.fst) • x.snd +
      x.snd * (y.fst • z.snd + z.fst • y.snd + y.snd * z.snd)
[PROOFSTEP]
simp only [smul_add, mul_add, add_mul, smul_smul, smul_mul_assoc, mul_smul_comm, mul_assoc]
[GOAL]
R : Type u_1
A : Type u_2
inst✝⁴ : CommMonoid R
inst✝³ : NonUnitalSemiring A
inst✝² : DistribMulAction R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
src✝ : MulOneClass (Unitization R A) := instMulOneClass
x y z : Unitization R A
⊢ (x.fst * y.fst) • z.snd + ((z.fst * x.fst) • y.snd + (z.fst * y.fst) • x.snd + z.fst • (x.snd * y.snd)) +
      (x.fst • (y.snd * z.snd) + y.fst • (x.snd * z.snd) + x.snd * (y.snd * z.snd)) =
    (x.fst * y.fst) • z.snd + (x.fst * z.fst) • y.snd + x.fst • (y.snd * z.snd) + (y.fst * z.fst) • x.snd +
      (y.fst • (x.snd * z.snd) + z.fst • (x.snd * y.snd) + x.snd * (y.snd * z.snd))
[PROOFSTEP]
rw [mul_comm z.1 x.1]
[GOAL]
R : Type u_1
A : Type u_2
inst✝⁴ : CommMonoid R
inst✝³ : NonUnitalSemiring A
inst✝² : DistribMulAction R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
src✝ : MulOneClass (Unitization R A) := instMulOneClass
x y z : Unitization R A
⊢ (x.fst * y.fst) • z.snd + ((x.fst * z.fst) • y.snd + (z.fst * y.fst) • x.snd + z.fst • (x.snd * y.snd)) +
      (x.fst • (y.snd * z.snd) + y.fst • (x.snd * z.snd) + x.snd * (y.snd * z.snd)) =
    (x.fst * y.fst) • z.snd + (x.fst * z.fst) • y.snd + x.fst • (y.snd * z.snd) + (y.fst * z.fst) • x.snd +
      (y.fst • (x.snd * z.snd) + z.fst • (x.snd * y.snd) + x.snd * (y.snd * z.snd))
[PROOFSTEP]
rw [mul_comm z.1 y.1]
[GOAL]
R : Type u_1
A : Type u_2
inst✝⁴ : CommMonoid R
inst✝³ : NonUnitalSemiring A
inst✝² : DistribMulAction R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
src✝ : MulOneClass (Unitization R A) := instMulOneClass
x y z : Unitization R A
⊢ (x.fst * y.fst) • z.snd + ((x.fst * z.fst) • y.snd + (y.fst * z.fst) • x.snd + z.fst • (x.snd * y.snd)) +
      (x.fst • (y.snd * z.snd) + y.fst • (x.snd * z.snd) + x.snd * (y.snd * z.snd)) =
    (x.fst * y.fst) • z.snd + (x.fst * z.fst) • y.snd + x.fst • (y.snd * z.snd) + (y.fst * z.fst) • x.snd +
      (y.fst • (x.snd * z.snd) + z.fst • (x.snd * y.snd) + x.snd * (y.snd * z.snd))
[PROOFSTEP]
abel
[GOAL]
R : Type u_1
A : Type u_2
inst✝⁴ : CommMonoid R
inst✝³ : NonUnitalSemiring A
inst✝² : DistribMulAction R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
src✝ : MulOneClass (Unitization R A) := instMulOneClass
x y z : Unitization R A
⊢ (x.fst * y.fst) • z.snd + ((x.fst * z.fst) • y.snd + (y.fst * z.fst) • x.snd + z.fst • (x.snd * y.snd)) +
      (x.fst • (y.snd * z.snd) + y.fst • (x.snd * z.snd) + x.snd * (y.snd * z.snd)) =
    (x.fst * y.fst) • z.snd + (x.fst * z.fst) • y.snd + x.fst • (y.snd * z.snd) + (y.fst * z.fst) • x.snd +
      (y.fst • (x.snd * z.snd) + z.fst • (x.snd * y.snd) + x.snd * (y.snd * z.snd))
[PROOFSTEP]
abel
[GOAL]
R : Type u_1
A : Type u_2
inst✝⁴ : CommMonoid R
inst✝³ : NonUnitalCommSemiring A
inst✝² : DistribMulAction R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
src✝ : Monoid (Unitization R A) := instMonoid
x₁ x₂ : Unitization R A
⊢ x₁.fst • x₂.snd + x₂.fst • x₁.snd + x₁.snd * x₂.snd = x₂.fst • x₁.snd + x₁.fst • x₂.snd + x₂.snd * x₁.snd
[PROOFSTEP]
rw [add_comm (x₁.1 • x₂.2), mul_comm]
[GOAL]
R : Type u_1
A : Type u_2
inst✝² : Star R
inst✝¹ : AddMonoid A
inst✝ : StarAddMonoid A
r : R
⊢ snd (inl (star r)) = snd (star (inl r))
[PROOFSTEP]
simp only [snd_star, star_zero, snd_inl]
[GOAL]
R : Type u_1
A : Type u_2
inst✝² : AddMonoid R
inst✝¹ : StarAddMonoid R
inst✝ : Star A
a : A
⊢ fst ↑(star a) = fst (star ↑a)
[PROOFSTEP]
simp only [fst_star, star_zero, fst_inr]
[GOAL]
R : Type u_1
A : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : StarRing R
inst✝³ : AddCommMonoid A
inst✝² : StarAddMonoid A
inst✝¹ : Module R A
inst✝ : StarModule R A
r : R
x : Unitization R A
⊢ fst (star (r • x)) = fst (star r • star x)
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
A : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : StarRing R
inst✝³ : AddCommMonoid A
inst✝² : StarAddMonoid A
inst✝¹ : Module R A
inst✝ : StarModule R A
r : R
x : Unitization R A
⊢ snd (star (r • x)) = snd (star r • star x)
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
A : Type u_2
inst✝⁷ : CommSemiring R
inst✝⁶ : StarRing R
inst✝⁵ : NonUnitalSemiring A
inst✝⁴ : StarRing A
inst✝³ : Module R A
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
inst✝ : StarModule R A
src✝ : StarAddMonoid (Unitization R A) := instStarAddMonoid
x y : Unitization R A
⊢ fst (star (x * y)) = fst (star y * star x)
[PROOFSTEP]
simp [-star_mul']
[GOAL]
R : Type u_1
A : Type u_2
inst✝⁷ : CommSemiring R
inst✝⁶ : StarRing R
inst✝⁵ : NonUnitalSemiring A
inst✝⁴ : StarRing A
inst✝³ : Module R A
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
inst✝ : StarModule R A
src✝ : StarAddMonoid (Unitization R A) := instStarAddMonoid
x y : Unitization R A
⊢ snd (star (x * y)) = snd (star y * star x)
[PROOFSTEP]
simp [-star_mul', add_comm (star x.fst • star y.snd)]
[GOAL]
S : Type u_1
R : Type u_2
A : Type u_3
inst✝⁸ : CommSemiring S
inst✝⁷ : CommSemiring R
inst✝⁶ : NonUnitalSemiring A
inst✝⁵ : Module R A
inst✝⁴ : IsScalarTower R A A
inst✝³ : SMulCommClass R A A
inst✝² : Algebra S R
inst✝¹ : DistribMulAction S A
inst✝ : IsScalarTower S R A
src✝ : S →+* Unitization R A := RingHom.comp (inlRingHom R A) (algebraMap S R)
s : S
x : (fun x => Unitization R A) s
⊢ ↑{ toMonoidHom := ↑src✝, map_zero' := (_ : OneHom.toFun (↑↑src✝) 0 = 0),
            map_add' :=
              (_ : ∀ (x y : S), OneHom.toFun (↑↑src✝) (x + y) = OneHom.toFun (↑↑src✝) x + OneHom.toFun (↑↑src✝) y) }
        s *
      x =
    x *
      ↑{ toMonoidHom := ↑src✝, map_zero' := (_ : OneHom.toFun (↑↑src✝) 0 = 0),
            map_add' :=
              (_ : ∀ (x y : S), OneHom.toFun (↑↑src✝) (x + y) = OneHom.toFun (↑↑src✝) x + OneHom.toFun (↑↑src✝) y) }
        s
[PROOFSTEP]
induction' x using Unitization.ind with r a
[GOAL]
case h
S : Type u_1
R : Type u_2
A : Type u_3
inst✝⁸ : CommSemiring S
inst✝⁷ : CommSemiring R
inst✝⁶ : NonUnitalSemiring A
inst✝⁵ : Module R A
inst✝⁴ : IsScalarTower R A A
inst✝³ : SMulCommClass R A A
inst✝² : Algebra S R
inst✝¹ : DistribMulAction S A
inst✝ : IsScalarTower S R A
src✝ : S →+* Unitization R A := RingHom.comp (inlRingHom R A) (algebraMap S R)
s : S
r : R
a : A
⊢ ↑{ toMonoidHom := ↑src✝, map_zero' := (_ : OneHom.toFun (↑↑src✝) 0 = 0),
            map_add' :=
              (_ : ∀ (x y : S), OneHom.toFun (↑↑src✝) (x + y) = OneHom.toFun (↑↑src✝) x + OneHom.toFun (↑↑src✝) y) }
        s *
      (inl r + ↑a) =
    (inl r + ↑a) *
      ↑{ toMonoidHom := ↑src✝, map_zero' := (_ : OneHom.toFun (↑↑src✝) 0 = 0),
            map_add' :=
              (_ : ∀ (x y : S), OneHom.toFun (↑↑src✝) (x + y) = OneHom.toFun (↑↑src✝) x + OneHom.toFun (↑↑src✝) y) }
        s
[PROOFSTEP]
show inl (algebraMap S R s) * _ = _ * inl (algebraMap S R s)
[GOAL]
case h
S : Type u_1
R : Type u_2
A : Type u_3
inst✝⁸ : CommSemiring S
inst✝⁷ : CommSemiring R
inst✝⁶ : NonUnitalSemiring A
inst✝⁵ : Module R A
inst✝⁴ : IsScalarTower R A A
inst✝³ : SMulCommClass R A A
inst✝² : Algebra S R
inst✝¹ : DistribMulAction S A
inst✝ : IsScalarTower S R A
src✝ : S →+* Unitization R A := RingHom.comp (inlRingHom R A) (algebraMap S R)
s : S
r : R
a : A
⊢ inl (↑(algebraMap S R) s) * (inl r + ↑a) = (inl r + ↑a) * inl (↑(algebraMap S R) s)
[PROOFSTEP]
rw [mul_add, add_mul, inl_mul_inl, inl_mul_inl, inl_mul_inr, inr_mul_inl, mul_comm]
[GOAL]
S : Type u_1
R : Type u_2
A : Type u_3
inst✝⁸ : CommSemiring S
inst✝⁷ : CommSemiring R
inst✝⁶ : NonUnitalSemiring A
inst✝⁵ : Module R A
inst✝⁴ : IsScalarTower R A A
inst✝³ : SMulCommClass R A A
inst✝² : Algebra S R
inst✝¹ : DistribMulAction S A
inst✝ : IsScalarTower S R A
src✝ : S →+* Unitization R A := RingHom.comp (inlRingHom R A) (algebraMap S R)
s : S
x : (fun x => Unitization R A) s
⊢ s • x =
    ↑{ toMonoidHom := ↑src✝, map_zero' := (_ : OneHom.toFun (↑↑src✝) 0 = 0),
            map_add' :=
              (_ : ∀ (x y : S), OneHom.toFun (↑↑src✝) (x + y) = OneHom.toFun (↑↑src✝) x + OneHom.toFun (↑↑src✝) y) }
        s *
      x
[PROOFSTEP]
induction' x using Unitization.ind with r a
[GOAL]
case h
S : Type u_1
R : Type u_2
A : Type u_3
inst✝⁸ : CommSemiring S
inst✝⁷ : CommSemiring R
inst✝⁶ : NonUnitalSemiring A
inst✝⁵ : Module R A
inst✝⁴ : IsScalarTower R A A
inst✝³ : SMulCommClass R A A
inst✝² : Algebra S R
inst✝¹ : DistribMulAction S A
inst✝ : IsScalarTower S R A
src✝ : S →+* Unitization R A := RingHom.comp (inlRingHom R A) (algebraMap S R)
s : S
r : R
a : A
⊢ s • (inl r + ↑a) =
    ↑{ toMonoidHom := ↑src✝, map_zero' := (_ : OneHom.toFun (↑↑src✝) 0 = 0),
            map_add' :=
              (_ : ∀ (x y : S), OneHom.toFun (↑↑src✝) (x + y) = OneHom.toFun (↑↑src✝) x + OneHom.toFun (↑↑src✝) y) }
        s *
      (inl r + ↑a)
[PROOFSTEP]
show _ = inl (algebraMap S R s) * _
[GOAL]
case h
S : Type u_1
R : Type u_2
A : Type u_3
inst✝⁸ : CommSemiring S
inst✝⁷ : CommSemiring R
inst✝⁶ : NonUnitalSemiring A
inst✝⁵ : Module R A
inst✝⁴ : IsScalarTower R A A
inst✝³ : SMulCommClass R A A
inst✝² : Algebra S R
inst✝¹ : DistribMulAction S A
inst✝ : IsScalarTower S R A
src✝ : S →+* Unitization R A := RingHom.comp (inlRingHom R A) (algebraMap S R)
s : S
r : R
a : A
⊢ s • (inl r + ↑a) = inl (↑(algebraMap S R) s) * (inl r + ↑a)
[PROOFSTEP]
rw [mul_add, smul_add, Algebra.algebraMap_eq_smul_one, inl_mul_inl, inl_mul_inr, smul_one_mul, inl_smul, inr_smul,
  smul_one_smul]
[GOAL]
S : Type u_1
R : Type u_2
A : Type u_3
inst✝¹³ : CommSemiring S
inst✝¹² : CommSemiring R
inst✝¹¹ : NonUnitalSemiring A
inst✝¹⁰ : Module R A
inst✝⁹ : SMulCommClass R A A
inst✝⁸ : IsScalarTower R A A
B : Type u_4
inst✝⁷ : Semiring B
inst✝⁶ : Algebra S B
inst✝⁵ : Algebra S R
inst✝⁴ : DistribMulAction S A
inst✝³ : IsScalarTower S R A
C : Type u_5
inst✝² : Semiring C
inst✝¹ : Algebra R C
F : Type u_6
inst✝ : AlgHomClass F S (Unitization R A) B
φ ψ : F
h : ∀ (a : A), ↑φ ↑a = ↑ψ ↑a
h' : ∀ (r : R), ↑φ (↑(algebraMap R (Unitization R A)) r) = ↑ψ (↑(algebraMap R (Unitization R A)) r)
⊢ φ = ψ
[PROOFSTEP]
refine FunLike.ext φ ψ (fun x ↦ ?_)
[GOAL]
S : Type u_1
R : Type u_2
A : Type u_3
inst✝¹³ : CommSemiring S
inst✝¹² : CommSemiring R
inst✝¹¹ : NonUnitalSemiring A
inst✝¹⁰ : Module R A
inst✝⁹ : SMulCommClass R A A
inst✝⁸ : IsScalarTower R A A
B : Type u_4
inst✝⁷ : Semiring B
inst✝⁶ : Algebra S B
inst✝⁵ : Algebra S R
inst✝⁴ : DistribMulAction S A
inst✝³ : IsScalarTower S R A
C : Type u_5
inst✝² : Semiring C
inst✝¹ : Algebra R C
F : Type u_6
inst✝ : AlgHomClass F S (Unitization R A) B
φ ψ : F
h : ∀ (a : A), ↑φ ↑a = ↑ψ ↑a
h' : ∀ (r : R), ↑φ (↑(algebraMap R (Unitization R A)) r) = ↑ψ (↑(algebraMap R (Unitization R A)) r)
x : Unitization R A
⊢ ↑φ x = ↑ψ x
[PROOFSTEP]
induction x using Unitization.ind
[GOAL]
case h
S : Type u_1
R : Type u_2
A : Type u_3
inst✝¹³ : CommSemiring S
inst✝¹² : CommSemiring R
inst✝¹¹ : NonUnitalSemiring A
inst✝¹⁰ : Module R A
inst✝⁹ : SMulCommClass R A A
inst✝⁸ : IsScalarTower R A A
B : Type u_4
inst✝⁷ : Semiring B
inst✝⁶ : Algebra S B
inst✝⁵ : Algebra S R
inst✝⁴ : DistribMulAction S A
inst✝³ : IsScalarTower S R A
C : Type u_5
inst✝² : Semiring C
inst✝¹ : Algebra R C
F : Type u_6
inst✝ : AlgHomClass F S (Unitization R A) B
φ ψ : F
h : ∀ (a : A), ↑φ ↑a = ↑ψ ↑a
h' : ∀ (r : R), ↑φ (↑(algebraMap R (Unitization R A)) r) = ↑ψ (↑(algebraMap R (Unitization R A)) r)
r✝ : R
a✝ : A
⊢ ↑φ (inl r✝ + ↑a✝) = ↑ψ (inl r✝ + ↑a✝)
[PROOFSTEP]
simp only [map_add, ← algebraMap_eq_inl, h, h']
[GOAL]
S : Type u_1
R : Type u_2
A : Type u_3
inst✝¹³ : CommSemiring S
inst✝¹² : CommSemiring R
inst✝¹¹ : NonUnitalSemiring A
inst✝¹⁰ : Module R A
inst✝⁹ : SMulCommClass R A A
inst✝⁸ : IsScalarTower R A A
B : Type u_4
inst✝⁷ : Semiring B
inst✝⁶ : Algebra S B
inst✝⁵ : Algebra S R
inst✝⁴ : DistribMulAction S A
inst✝³ : IsScalarTower S R A
C : Type u_5
inst✝² : Semiring C
inst✝¹ : Algebra R C
F : Type u_6
inst✝ : AlgHomClass F R (Unitization R A) C
φ ψ : F
h : ∀ (a : A), ↑φ ↑a = ↑ψ ↑a
r : R
⊢ ↑φ (↑(algebraMap R (Unitization R A)) r) = ↑ψ (↑(algebraMap R (Unitization R A)) r)
[PROOFSTEP]
simp only [AlgHomClass.commutes]
[GOAL]
S : Type u_1
R : Type u_2
A : Type u_3
inst✝¹² : CommSemiring S
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : NonUnitalSemiring A
inst✝⁹ : Module R A
inst✝⁸ : SMulCommClass R A A
inst✝⁷ : IsScalarTower R A A
B : Type u_4
inst✝⁶ : Semiring B
inst✝⁵ : Algebra S B
inst✝⁴ : Algebra S R
inst✝³ : DistribMulAction S A
inst✝² : IsScalarTower S R A
C : Type u_5
inst✝¹ : Semiring C
inst✝ : Algebra R C
φ : A →ₙₐ[R] C
⊢ (fun x => ↑(algebraMap R C) (fst x) + ↑φ (snd x)) 1 = 1
[PROOFSTEP]
simp only [fst_one, map_one, snd_one, φ.map_zero, add_zero]
[GOAL]
S : Type u_1
R : Type u_2
A : Type u_3
inst✝¹² : CommSemiring S
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : NonUnitalSemiring A
inst✝⁹ : Module R A
inst✝⁸ : SMulCommClass R A A
inst✝⁷ : IsScalarTower R A A
B : Type u_4
inst✝⁶ : Semiring B
inst✝⁵ : Algebra S B
inst✝⁴ : Algebra S R
inst✝³ : DistribMulAction S A
inst✝² : IsScalarTower S R A
C : Type u_5
inst✝¹ : Semiring C
inst✝ : Algebra R C
φ : A →ₙₐ[R] C
x y : Unitization R A
⊢ OneHom.toFun
      { toFun := fun x => ↑(algebraMap R C) (fst x) + ↑φ (snd x), map_one' := (_ : ↑(algebraMap R C) 1 + ↑φ 0 = 1) }
      (x * y) =
    OneHom.toFun
        { toFun := fun x => ↑(algebraMap R C) (fst x) + ↑φ (snd x), map_one' := (_ : ↑(algebraMap R C) 1 + ↑φ 0 = 1) }
        x *
      OneHom.toFun
        { toFun := fun x => ↑(algebraMap R C) (fst x) + ↑φ (snd x), map_one' := (_ : ↑(algebraMap R C) 1 + ↑φ 0 = 1) } y
[PROOFSTEP]
induction' x using Unitization.ind with x_r x_a
[GOAL]
case h
S : Type u_1
R : Type u_2
A : Type u_3
inst✝¹² : CommSemiring S
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : NonUnitalSemiring A
inst✝⁹ : Module R A
inst✝⁸ : SMulCommClass R A A
inst✝⁷ : IsScalarTower R A A
B : Type u_4
inst✝⁶ : Semiring B
inst✝⁵ : Algebra S B
inst✝⁴ : Algebra S R
inst✝³ : DistribMulAction S A
inst✝² : IsScalarTower S R A
C : Type u_5
inst✝¹ : Semiring C
inst✝ : Algebra R C
φ : A →ₙₐ[R] C
y : Unitization R A
x_r : R
x_a : A
⊢ OneHom.toFun
      { toFun := fun x => ↑(algebraMap R C) (fst x) + ↑φ (snd x), map_one' := (_ : ↑(algebraMap R C) 1 + ↑φ 0 = 1) }
      ((inl x_r + ↑x_a) * y) =
    OneHom.toFun
        { toFun := fun x => ↑(algebraMap R C) (fst x) + ↑φ (snd x), map_one' := (_ : ↑(algebraMap R C) 1 + ↑φ 0 = 1) }
        (inl x_r + ↑x_a) *
      OneHom.toFun
        { toFun := fun x => ↑(algebraMap R C) (fst x) + ↑φ (snd x), map_one' := (_ : ↑(algebraMap R C) 1 + ↑φ 0 = 1) } y
[PROOFSTEP]
induction' y using Unitization.ind with y_r y_a
[GOAL]
case h.h
S : Type u_1
R : Type u_2
A : Type u_3
inst✝¹² : CommSemiring S
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : NonUnitalSemiring A
inst✝⁹ : Module R A
inst✝⁸ : SMulCommClass R A A
inst✝⁷ : IsScalarTower R A A
B : Type u_4
inst✝⁶ : Semiring B
inst✝⁵ : Algebra S B
inst✝⁴ : Algebra S R
inst✝³ : DistribMulAction S A
inst✝² : IsScalarTower S R A
C : Type u_5
inst✝¹ : Semiring C
inst✝ : Algebra R C
φ : A →ₙₐ[R] C
x_r : R
x_a : A
y_r : R
y_a : A
⊢ OneHom.toFun
      { toFun := fun x => ↑(algebraMap R C) (fst x) + ↑φ (snd x), map_one' := (_ : ↑(algebraMap R C) 1 + ↑φ 0 = 1) }
      ((inl x_r + ↑x_a) * (inl y_r + ↑y_a)) =
    OneHom.toFun
        { toFun := fun x => ↑(algebraMap R C) (fst x) + ↑φ (snd x), map_one' := (_ : ↑(algebraMap R C) 1 + ↑φ 0 = 1) }
        (inl x_r + ↑x_a) *
      OneHom.toFun
        { toFun := fun x => ↑(algebraMap R C) (fst x) + ↑φ (snd x), map_one' := (_ : ↑(algebraMap R C) 1 + ↑φ 0 = 1) }
        (inl y_r + ↑y_a)
[PROOFSTEP]
simp only [fst_mul, fst_add, fst_inl, fst_inr, snd_mul, snd_add, snd_inl, snd_inr, add_zero, map_mul, zero_add, map_add,
  map_smul φ]
[GOAL]
case h.h
S : Type u_1
R : Type u_2
A : Type u_3
inst✝¹² : CommSemiring S
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : NonUnitalSemiring A
inst✝⁹ : Module R A
inst✝⁸ : SMulCommClass R A A
inst✝⁷ : IsScalarTower R A A
B : Type u_4
inst✝⁶ : Semiring B
inst✝⁵ : Algebra S B
inst✝⁴ : Algebra S R
inst✝³ : DistribMulAction S A
inst✝² : IsScalarTower S R A
C : Type u_5
inst✝¹ : Semiring C
inst✝ : Algebra R C
φ : A →ₙₐ[R] C
x_r : R
x_a : A
y_r : R
y_a : A
⊢ ↑(algebraMap R C) x_r * ↑(algebraMap R C) y_r + (x_r • ↑φ y_a + y_r • ↑φ x_a + ↑φ x_a * ↑φ y_a) =
    (↑(algebraMap R C) x_r + ↑φ x_a) * (↑(algebraMap R C) y_r + ↑φ y_a)
[PROOFSTEP]
rw [add_mul, mul_add, mul_add]
[GOAL]
case h.h
S : Type u_1
R : Type u_2
A : Type u_3
inst✝¹² : CommSemiring S
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : NonUnitalSemiring A
inst✝⁹ : Module R A
inst✝⁸ : SMulCommClass R A A
inst✝⁷ : IsScalarTower R A A
B : Type u_4
inst✝⁶ : Semiring B
inst✝⁵ : Algebra S B
inst✝⁴ : Algebra S R
inst✝³ : DistribMulAction S A
inst✝² : IsScalarTower S R A
C : Type u_5
inst✝¹ : Semiring C
inst✝ : Algebra R C
φ : A →ₙₐ[R] C
x_r : R
x_a : A
y_r : R
y_a : A
⊢ ↑(algebraMap R C) x_r * ↑(algebraMap R C) y_r + (x_r • ↑φ y_a + y_r • ↑φ x_a + ↑φ x_a * ↑φ y_a) =
    ↑(algebraMap R C) x_r * ↑(algebraMap R C) y_r + ↑(algebraMap R C) x_r * ↑φ y_a +
      (↑φ x_a * ↑(algebraMap R C) y_r + ↑φ x_a * ↑φ y_a)
[PROOFSTEP]
rw [← Algebra.commutes _ (φ x_a)]
[GOAL]
case h.h
S : Type u_1
R : Type u_2
A : Type u_3
inst✝¹² : CommSemiring S
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : NonUnitalSemiring A
inst✝⁹ : Module R A
inst✝⁸ : SMulCommClass R A A
inst✝⁷ : IsScalarTower R A A
B : Type u_4
inst✝⁶ : Semiring B
inst✝⁵ : Algebra S B
inst✝⁴ : Algebra S R
inst✝³ : DistribMulAction S A
inst✝² : IsScalarTower S R A
C : Type u_5
inst✝¹ : Semiring C
inst✝ : Algebra R C
φ : A →ₙₐ[R] C
x_r : R
x_a : A
y_r : R
y_a : A
⊢ ↑(algebraMap R C) x_r * ↑(algebraMap R C) y_r + (x_r • ↑φ y_a + y_r • ↑φ x_a + ↑φ x_a * ↑φ y_a) =
    ↑(algebraMap R C) x_r * ↑(algebraMap R C) y_r + ↑(algebraMap R C) x_r * ↑φ y_a +
      (↑(algebraMap R ((fun x => C) x_a)) y_r * ↑φ x_a + ↑φ x_a * ↑φ y_a)
[PROOFSTEP]
simp only [Algebra.algebraMap_eq_smul_one, smul_one_mul, add_assoc]
[GOAL]
S : Type u_1
R : Type u_2
A : Type u_3
inst✝¹² : CommSemiring S
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : NonUnitalSemiring A
inst✝⁹ : Module R A
inst✝⁸ : SMulCommClass R A A
inst✝⁷ : IsScalarTower R A A
B : Type u_4
inst✝⁶ : Semiring B
inst✝⁵ : Algebra S B
inst✝⁴ : Algebra S R
inst✝³ : DistribMulAction S A
inst✝² : IsScalarTower S R A
C : Type u_5
inst✝¹ : Semiring C
inst✝ : Algebra R C
φ : A →ₙₐ[R] C
⊢ OneHom.toFun
      (↑{
          toOneHom :=
            { toFun := fun x => ↑(algebraMap R C) (fst x) + ↑φ (snd x),
              map_one' := (_ : ↑(algebraMap R C) 1 + ↑φ 0 = 1) },
          map_mul' :=
            (_ :
              ∀ (x y : Unitization R A),
                OneHom.toFun
                    { toFun := fun x => ↑(algebraMap R C) (fst x) + ↑φ (snd x),
                      map_one' := (_ : ↑(algebraMap R C) 1 + ↑φ 0 = 1) }
                    (x * y) =
                  OneHom.toFun
                      { toFun := fun x => ↑(algebraMap R C) (fst x) + ↑φ (snd x),
                        map_one' := (_ : ↑(algebraMap R C) 1 + ↑φ 0 = 1) }
                      x *
                    OneHom.toFun
                      { toFun := fun x => ↑(algebraMap R C) (fst x) + ↑φ (snd x),
                        map_one' := (_ : ↑(algebraMap R C) 1 + ↑φ 0 = 1) }
                      y) })
      0 =
    0
[PROOFSTEP]
simp only [fst_zero, map_zero, snd_zero, φ.map_zero, add_zero]
[GOAL]
S : Type u_1
R : Type u_2
A : Type u_3
inst✝¹² : CommSemiring S
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : NonUnitalSemiring A
inst✝⁹ : Module R A
inst✝⁸ : SMulCommClass R A A
inst✝⁷ : IsScalarTower R A A
B : Type u_4
inst✝⁶ : Semiring B
inst✝⁵ : Algebra S B
inst✝⁴ : Algebra S R
inst✝³ : DistribMulAction S A
inst✝² : IsScalarTower S R A
C : Type u_5
inst✝¹ : Semiring C
inst✝ : Algebra R C
φ : A →ₙₐ[R] C
x y : Unitization R A
⊢ OneHom.toFun
      (↑{
          toOneHom :=
            { toFun := fun x => ↑(algebraMap R C) (fst x) + ↑φ (snd x),
              map_one' := (_ : ↑(algebraMap R C) 1 + ↑φ 0 = 1) },
          map_mul' :=
            (_ :
              ∀ (x y : Unitization R A),
                OneHom.toFun
                    { toFun := fun x => ↑(algebraMap R C) (fst x) + ↑φ (snd x),
                      map_one' := (_ : ↑(algebraMap R C) 1 + ↑φ 0 = 1) }
                    (x * y) =
                  OneHom.toFun
                      { toFun := fun x => ↑(algebraMap R C) (fst x) + ↑φ (snd x),
                        map_one' := (_ : ↑(algebraMap R C) 1 + ↑φ 0 = 1) }
                      x *
                    OneHom.toFun
                      { toFun := fun x => ↑(algebraMap R C) (fst x) + ↑φ (snd x),
                        map_one' := (_ : ↑(algebraMap R C) 1 + ↑φ 0 = 1) }
                      y) })
      (x + y) =
    OneHom.toFun
        (↑{
            toOneHom :=
              { toFun := fun x => ↑(algebraMap R C) (fst x) + ↑φ (snd x),
                map_one' := (_ : ↑(algebraMap R C) 1 + ↑φ 0 = 1) },
            map_mul' :=
              (_ :
                ∀ (x y : Unitization R A),
                  OneHom.toFun
                      { toFun := fun x => ↑(algebraMap R C) (fst x) + ↑φ (snd x),
                        map_one' := (_ : ↑(algebraMap R C) 1 + ↑φ 0 = 1) }
                      (x * y) =
                    OneHom.toFun
                        { toFun := fun x => ↑(algebraMap R C) (fst x) + ↑φ (snd x),
                          map_one' := (_ : ↑(algebraMap R C) 1 + ↑φ 0 = 1) }
                        x *
                      OneHom.toFun
                        { toFun := fun x => ↑(algebraMap R C) (fst x) + ↑φ (snd x),
                          map_one' := (_ : ↑(algebraMap R C) 1 + ↑φ 0 = 1) }
                        y) })
        x +
      OneHom.toFun
        (↑{
            toOneHom :=
              { toFun := fun x => ↑(algebraMap R C) (fst x) + ↑φ (snd x),
                map_one' := (_ : ↑(algebraMap R C) 1 + ↑φ 0 = 1) },
            map_mul' :=
              (_ :
                ∀ (x y : Unitization R A),
                  OneHom.toFun
                      { toFun := fun x => ↑(algebraMap R C) (fst x) + ↑φ (snd x),
                        map_one' := (_ : ↑(algebraMap R C) 1 + ↑φ 0 = 1) }
                      (x * y) =
                    OneHom.toFun
                        { toFun := fun x => ↑(algebraMap R C) (fst x) + ↑φ (snd x),
                          map_one' := (_ : ↑(algebraMap R C) 1 + ↑φ 0 = 1) }
                        x *
                      OneHom.toFun
                        { toFun := fun x => ↑(algebraMap R C) (fst x) + ↑φ (snd x),
                          map_one' := (_ : ↑(algebraMap R C) 1 + ↑φ 0 = 1) }
                        y) })
        y
[PROOFSTEP]
induction' x using Unitization.ind with x_r x_a
[GOAL]
case h
S : Type u_1
R : Type u_2
A : Type u_3
inst✝¹² : CommSemiring S
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : NonUnitalSemiring A
inst✝⁹ : Module R A
inst✝⁸ : SMulCommClass R A A
inst✝⁷ : IsScalarTower R A A
B : Type u_4
inst✝⁶ : Semiring B
inst✝⁵ : Algebra S B
inst✝⁴ : Algebra S R
inst✝³ : DistribMulAction S A
inst✝² : IsScalarTower S R A
C : Type u_5
inst✝¹ : Semiring C
inst✝ : Algebra R C
φ : A →ₙₐ[R] C
y : Unitization R A
x_r : R
x_a : A
⊢ OneHom.toFun
      (↑{
          toOneHom :=
            { toFun := fun x => ↑(algebraMap R C) (fst x) + ↑φ (snd x),
              map_one' := (_ : ↑(algebraMap R C) 1 + ↑φ 0 = 1) },
          map_mul' :=
            (_ :
              ∀ (x y : Unitization R A),
                OneHom.toFun
                    { toFun := fun x => ↑(algebraMap R C) (fst x) + ↑φ (snd x),
                      map_one' := (_ : ↑(algebraMap R C) 1 + ↑φ 0 = 1) }
                    (x * y) =
                  OneHom.toFun
                      { toFun := fun x => ↑(algebraMap R C) (fst x) + ↑φ (snd x),
                        map_one' := (_ : ↑(algebraMap R C) 1 + ↑φ 0 = 1) }
                      x *
                    OneHom.toFun
                      { toFun := fun x => ↑(algebraMap R C) (fst x) + ↑φ (snd x),
                        map_one' := (_ : ↑(algebraMap R C) 1 + ↑φ 0 = 1) }
                      y) })
      (inl x_r + ↑x_a + y) =
    OneHom.toFun
        (↑{
            toOneHom :=
              { toFun := fun x => ↑(algebraMap R C) (fst x) + ↑φ (snd x),
                map_one' := (_ : ↑(algebraMap R C) 1 + ↑φ 0 = 1) },
            map_mul' :=
              (_ :
                ∀ (x y : Unitization R A),
                  OneHom.toFun
                      { toFun := fun x => ↑(algebraMap R C) (fst x) + ↑φ (snd x),
                        map_one' := (_ : ↑(algebraMap R C) 1 + ↑φ 0 = 1) }
                      (x * y) =
                    OneHom.toFun
                        { toFun := fun x => ↑(algebraMap R C) (fst x) + ↑φ (snd x),
                          map_one' := (_ : ↑(algebraMap R C) 1 + ↑φ 0 = 1) }
                        x *
                      OneHom.toFun
                        { toFun := fun x => ↑(algebraMap R C) (fst x) + ↑φ (snd x),
                          map_one' := (_ : ↑(algebraMap R C) 1 + ↑φ 0 = 1) }
                        y) })
        (inl x_r + ↑x_a) +
      OneHom.toFun
        (↑{
            toOneHom :=
              { toFun := fun x => ↑(algebraMap R C) (fst x) + ↑φ (snd x),
                map_one' := (_ : ↑(algebraMap R C) 1 + ↑φ 0 = 1) },
            map_mul' :=
              (_ :
                ∀ (x y : Unitization R A),
                  OneHom.toFun
                      { toFun := fun x => ↑(algebraMap R C) (fst x) + ↑φ (snd x),
                        map_one' := (_ : ↑(algebraMap R C) 1 + ↑φ 0 = 1) }
                      (x * y) =
                    OneHom.toFun
                        { toFun := fun x => ↑(algebraMap R C) (fst x) + ↑φ (snd x),
                          map_one' := (_ : ↑(algebraMap R C) 1 + ↑φ 0 = 1) }
                        x *
                      OneHom.toFun
                        { toFun := fun x => ↑(algebraMap R C) (fst x) + ↑φ (snd x),
                          map_one' := (_ : ↑(algebraMap R C) 1 + ↑φ 0 = 1) }
                        y) })
        y
[PROOFSTEP]
induction' y using Unitization.ind with y_r y_a
[GOAL]
case h.h
S : Type u_1
R : Type u_2
A : Type u_3
inst✝¹² : CommSemiring S
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : NonUnitalSemiring A
inst✝⁹ : Module R A
inst✝⁸ : SMulCommClass R A A
inst✝⁷ : IsScalarTower R A A
B : Type u_4
inst✝⁶ : Semiring B
inst✝⁵ : Algebra S B
inst✝⁴ : Algebra S R
inst✝³ : DistribMulAction S A
inst✝² : IsScalarTower S R A
C : Type u_5
inst✝¹ : Semiring C
inst✝ : Algebra R C
φ : A →ₙₐ[R] C
x_r : R
x_a : A
y_r : R
y_a : A
⊢ OneHom.toFun
      (↑{
          toOneHom :=
            { toFun := fun x => ↑(algebraMap R C) (fst x) + ↑φ (snd x),
              map_one' := (_ : ↑(algebraMap R C) 1 + ↑φ 0 = 1) },
          map_mul' :=
            (_ :
              ∀ (x y : Unitization R A),
                OneHom.toFun
                    { toFun := fun x => ↑(algebraMap R C) (fst x) + ↑φ (snd x),
                      map_one' := (_ : ↑(algebraMap R C) 1 + ↑φ 0 = 1) }
                    (x * y) =
                  OneHom.toFun
                      { toFun := fun x => ↑(algebraMap R C) (fst x) + ↑φ (snd x),
                        map_one' := (_ : ↑(algebraMap R C) 1 + ↑φ 0 = 1) }
                      x *
                    OneHom.toFun
                      { toFun := fun x => ↑(algebraMap R C) (fst x) + ↑φ (snd x),
                        map_one' := (_ : ↑(algebraMap R C) 1 + ↑φ 0 = 1) }
                      y) })
      (inl x_r + ↑x_a + (inl y_r + ↑y_a)) =
    OneHom.toFun
        (↑{
            toOneHom :=
              { toFun := fun x => ↑(algebraMap R C) (fst x) + ↑φ (snd x),
                map_one' := (_ : ↑(algebraMap R C) 1 + ↑φ 0 = 1) },
            map_mul' :=
              (_ :
                ∀ (x y : Unitization R A),
                  OneHom.toFun
                      { toFun := fun x => ↑(algebraMap R C) (fst x) + ↑φ (snd x),
                        map_one' := (_ : ↑(algebraMap R C) 1 + ↑φ 0 = 1) }
                      (x * y) =
                    OneHom.toFun
                        { toFun := fun x => ↑(algebraMap R C) (fst x) + ↑φ (snd x),
                          map_one' := (_ : ↑(algebraMap R C) 1 + ↑φ 0 = 1) }
                        x *
                      OneHom.toFun
                        { toFun := fun x => ↑(algebraMap R C) (fst x) + ↑φ (snd x),
                          map_one' := (_ : ↑(algebraMap R C) 1 + ↑φ 0 = 1) }
                        y) })
        (inl x_r + ↑x_a) +
      OneHom.toFun
        (↑{
            toOneHom :=
              { toFun := fun x => ↑(algebraMap R C) (fst x) + ↑φ (snd x),
                map_one' := (_ : ↑(algebraMap R C) 1 + ↑φ 0 = 1) },
            map_mul' :=
              (_ :
                ∀ (x y : Unitization R A),
                  OneHom.toFun
                      { toFun := fun x => ↑(algebraMap R C) (fst x) + ↑φ (snd x),
                        map_one' := (_ : ↑(algebraMap R C) 1 + ↑φ 0 = 1) }
                      (x * y) =
                    OneHom.toFun
                        { toFun := fun x => ↑(algebraMap R C) (fst x) + ↑φ (snd x),
                          map_one' := (_ : ↑(algebraMap R C) 1 + ↑φ 0 = 1) }
                        x *
                      OneHom.toFun
                        { toFun := fun x => ↑(algebraMap R C) (fst x) + ↑φ (snd x),
                          map_one' := (_ : ↑(algebraMap R C) 1 + ↑φ 0 = 1) }
                        y) })
        (inl y_r + ↑y_a)
[PROOFSTEP]
simp only [fst_add, fst_inl, fst_inr, add_zero, map_add, snd_add, snd_inl, snd_inr, zero_add, φ.map_add]
[GOAL]
case h.h
S : Type u_1
R : Type u_2
A : Type u_3
inst✝¹² : CommSemiring S
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : NonUnitalSemiring A
inst✝⁹ : Module R A
inst✝⁸ : SMulCommClass R A A
inst✝⁷ : IsScalarTower R A A
B : Type u_4
inst✝⁶ : Semiring B
inst✝⁵ : Algebra S B
inst✝⁴ : Algebra S R
inst✝³ : DistribMulAction S A
inst✝² : IsScalarTower S R A
C : Type u_5
inst✝¹ : Semiring C
inst✝ : Algebra R C
φ : A →ₙₐ[R] C
x_r : R
x_a : A
y_r : R
y_a : A
⊢ ↑(algebraMap R C) x_r + ↑(algebraMap R C) y_r + (↑φ x_a + ↑φ y_a) =
    ↑(algebraMap R C) x_r + ↑φ x_a + (↑(algebraMap R C) y_r + ↑φ y_a)
[PROOFSTEP]
rw [add_add_add_comm]
[GOAL]
S : Type u_1
R : Type u_2
A : Type u_3
inst✝¹² : CommSemiring S
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : NonUnitalSemiring A
inst✝⁹ : Module R A
inst✝⁸ : SMulCommClass R A A
inst✝⁷ : IsScalarTower R A A
B : Type u_4
inst✝⁶ : Semiring B
inst✝⁵ : Algebra S B
inst✝⁴ : Algebra S R
inst✝³ : DistribMulAction S A
inst✝² : IsScalarTower S R A
C : Type u_5
inst✝¹ : Semiring C
inst✝ : Algebra R C
φ : A →ₙₐ[R] C
r : R
⊢ OneHom.toFun
      (↑↑{
            toMonoidHom :=
              {
                toOneHom :=
                  { toFun := fun x => ↑(algebraMap R C) (fst x) + ↑φ (snd x),
                    map_one' := (_ : ↑(algebraMap R C) 1 + ↑φ 0 = 1) },
                map_mul' :=
                  (_ :
                    ∀ (x y : Unitization R A),
                      OneHom.toFun
                          { toFun := fun x => ↑(algebraMap R C) (fst x) + ↑φ (snd x),
                            map_one' := (_ : ↑(algebraMap R C) 1 + ↑φ 0 = 1) }
                          (x * y) =
                        OneHom.toFun
                            { toFun := fun x => ↑(algebraMap R C) (fst x) + ↑φ (snd x),
                              map_one' := (_ : ↑(algebraMap R C) 1 + ↑φ 0 = 1) }
                            x *
                          OneHom.toFun
                            { toFun := fun x => ↑(algebraMap R C) (fst x) + ↑φ (snd x),
                              map_one' := (_ : ↑(algebraMap R C) 1 + ↑φ 0 = 1) }
                            y) },
            map_zero' := (_ : ↑(algebraMap R C) 0 + ↑φ 0 = 0),
            map_add' :=
              (_ :
                ∀ (x y : Unitization R A),
                  OneHom.toFun
                      (↑{
                          toOneHom :=
                            { toFun := fun x => ↑(algebraMap R C) (fst x) + ↑φ (snd x),
                              map_one' := (_ : ↑(algebraMap R C) 1 + ↑φ 0 = 1) },
                          map_mul' :=
                            (_ :
                              ∀ (x y : Unitization R A),
                                OneHom.toFun
                                    { toFun := fun x => ↑(algebraMap R C) (fst x) + ↑φ (snd x),
                                      map_one' := (_ : ↑(algebraMap R C) 1 + ↑φ 0 = 1) }
                                    (x * y) =
                                  OneHom.toFun
                                      { toFun := fun x => ↑(algebraMap R C) (fst x) + ↑φ (snd x),
                                        map_one' := (_ : ↑(algebraMap R C) 1 + ↑φ 0 = 1) }
                                      x *
                                    OneHom.toFun
                                      { toFun := fun x => ↑(algebraMap R C) (fst x) + ↑φ (snd x),
                                        map_one' := (_ : ↑(algebraMap R C) 1 + ↑φ 0 = 1) }
                                      y) })
                      (x + y) =
                    OneHom.toFun
                        (↑{
                            toOneHom :=
                              { toFun := fun x => ↑(algebraMap R C) (fst x) + ↑φ (snd x),
                                map_one' := (_ : ↑(algebraMap R C) 1 + ↑φ 0 = 1) },
                            map_mul' :=
                              (_ :
                                ∀ (x y : Unitization R A),
                                  OneHom.toFun
                                      { toFun := fun x => ↑(algebraMap R C) (fst x) + ↑φ (snd x),
                                        map_one' := (_ : ↑(algebraMap R C) 1 + ↑φ 0 = 1) }
                                      (x * y) =
                                    OneHom.toFun
                                        { toFun := fun x => ↑(algebraMap R C) (fst x) + ↑φ (snd x),
                                          map_one' := (_ : ↑(algebraMap R C) 1 + ↑φ 0 = 1) }
                                        x *
                                      OneHom.toFun
                                        { toFun := fun x => ↑(algebraMap R C) (fst x) + ↑φ (snd x),
                                          map_one' := (_ : ↑(algebraMap R C) 1 + ↑φ 0 = 1) }
                                        y) })
                        x +
                      OneHom.toFun
                        (↑{
                            toOneHom :=
                              { toFun := fun x => ↑(algebraMap R C) (fst x) + ↑φ (snd x),
                                map_one' := (_ : ↑(algebraMap R C) 1 + ↑φ 0 = 1) },
                            map_mul' :=
                              (_ :
                                ∀ (x y : Unitization R A),
                                  OneHom.toFun
                                      { toFun := fun x => ↑(algebraMap R C) (fst x) + ↑φ (snd x),
                                        map_one' := (_ : ↑(algebraMap R C) 1 + ↑φ 0 = 1) }
                                      (x * y) =
                                    OneHom.toFun
                                        { toFun := fun x => ↑(algebraMap R C) (fst x) + ↑φ (snd x),
                                          map_one' := (_ : ↑(algebraMap R C) 1 + ↑φ 0 = 1) }
                                        x *
                                      OneHom.toFun
                                        { toFun := fun x => ↑(algebraMap R C) (fst x) + ↑φ (snd x),
                                          map_one' := (_ : ↑(algebraMap R C) 1 + ↑φ 0 = 1) }
                                        y) })
                        y) })
      (↑(algebraMap R (Unitization R A)) r) =
    ↑(algebraMap R C) r
[PROOFSTEP]
simp only [algebraMap_eq_inl, fst_inl, snd_inl, φ.map_zero, add_zero]
[GOAL]
S : Type u_1
R : Type u_2
A : Type u_3
inst✝¹² : CommSemiring S
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : NonUnitalSemiring A
inst✝⁹ : Module R A
inst✝⁸ : SMulCommClass R A A
inst✝⁷ : IsScalarTower R A A
B : Type u_4
inst✝⁶ : Semiring B
inst✝⁵ : Algebra S B
inst✝⁴ : Algebra S R
inst✝³ : DistribMulAction S A
inst✝² : IsScalarTower S R A
C : Type u_5
inst✝¹ : Semiring C
inst✝ : Algebra R C
φ : A →ₙₐ[R] C
⊢ (fun φ => NonUnitalAlgHom.comp (↑φ) (inrNonUnitalAlgHom R A)) (NonUnitalAlgHom.toAlgHom φ) = φ
[PROOFSTEP]
ext
[GOAL]
case h
S : Type u_1
R : Type u_2
A : Type u_3
inst✝¹² : CommSemiring S
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : NonUnitalSemiring A
inst✝⁹ : Module R A
inst✝⁸ : SMulCommClass R A A
inst✝⁷ : IsScalarTower R A A
B : Type u_4
inst✝⁶ : Semiring B
inst✝⁵ : Algebra S B
inst✝⁴ : Algebra S R
inst✝³ : DistribMulAction S A
inst✝² : IsScalarTower S R A
C : Type u_5
inst✝¹ : Semiring C
inst✝ : Algebra R C
φ : A →ₙₐ[R] C
x✝ : A
⊢ ↑((fun φ => NonUnitalAlgHom.comp (↑φ) (inrNonUnitalAlgHom R A)) (NonUnitalAlgHom.toAlgHom φ)) x✝ = ↑φ x✝
[PROOFSTEP]
simp
[GOAL]
S : Type u_1
R : Type u_2
A : Type u_3
inst✝¹² : CommSemiring S
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : NonUnitalSemiring A
inst✝⁹ : Module R A
inst✝⁸ : SMulCommClass R A A
inst✝⁷ : IsScalarTower R A A
B : Type u_4
inst✝⁶ : Semiring B
inst✝⁵ : Algebra S B
inst✝⁴ : Algebra S R
inst✝³ : DistribMulAction S A
inst✝² : IsScalarTower S R A
C : Type u_5
inst✝¹ : Semiring C
inst✝ : Algebra R C
φ : Unitization R A →ₐ[R] C
⊢ NonUnitalAlgHom.comp (↑(NonUnitalAlgHom.toAlgHom ((fun φ => NonUnitalAlgHom.comp (↑φ) (inrNonUnitalAlgHom R A)) φ)))
      (inrNonUnitalAlgHom R A) =
    NonUnitalAlgHom.comp (↑φ) (inrNonUnitalAlgHom R A)
[PROOFSTEP]
ext
[GOAL]
case h
S : Type u_1
R : Type u_2
A : Type u_3
inst✝¹² : CommSemiring S
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : NonUnitalSemiring A
inst✝⁹ : Module R A
inst✝⁸ : SMulCommClass R A A
inst✝⁷ : IsScalarTower R A A
B : Type u_4
inst✝⁶ : Semiring B
inst✝⁵ : Algebra S B
inst✝⁴ : Algebra S R
inst✝³ : DistribMulAction S A
inst✝² : IsScalarTower S R A
C : Type u_5
inst✝¹ : Semiring C
inst✝ : Algebra R C
φ : Unitization R A →ₐ[R] C
x✝ : A
⊢ ↑(NonUnitalAlgHom.comp (↑(NonUnitalAlgHom.toAlgHom ((fun φ => NonUnitalAlgHom.comp (↑φ) (inrNonUnitalAlgHom R A)) φ)))
          (inrNonUnitalAlgHom R A))
      x✝ =
    ↑(NonUnitalAlgHom.comp (↑φ) (inrNonUnitalAlgHom R A)) x✝
[PROOFSTEP]
simp
[GOAL]
S : Type u_1
R : Type u_2
A : Type u_3
inst✝¹² : CommSemiring S
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : NonUnitalSemiring A
inst✝⁹ : Module R A
inst✝⁸ : SMulCommClass R A A
inst✝⁷ : IsScalarTower R A A
B : Type u_4
inst✝⁶ : Semiring B
inst✝⁵ : Algebra S B
inst✝⁴ : Algebra S R
inst✝³ : DistribMulAction S A
inst✝² : IsScalarTower S R A
C : Type u_5
inst✝¹ : Semiring C
inst✝ : Algebra R C
⊢ ↑(NonUnitalAlgHom.toAlgHom 0) = fst
[PROOFSTEP]
ext
[GOAL]
case h
S : Type u_1
R : Type u_2
A : Type u_3
inst✝¹² : CommSemiring S
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : NonUnitalSemiring A
inst✝⁹ : Module R A
inst✝⁸ : SMulCommClass R A A
inst✝⁷ : IsScalarTower R A A
B : Type u_4
inst✝⁶ : Semiring B
inst✝⁵ : Algebra S B
inst✝⁴ : Algebra S R
inst✝³ : DistribMulAction S A
inst✝² : IsScalarTower S R A
C : Type u_5
inst✝¹ : Semiring C
inst✝ : Algebra R C
x✝ : Unitization R A
⊢ ↑(NonUnitalAlgHom.toAlgHom 0) x✝ = fst x✝
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
A : Type u_2
C : Type u_3
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : StarRing R
inst✝⁹ : NonUnitalSemiring A
inst✝⁸ : StarRing A
inst✝⁷ : Module R A
inst✝⁶ : SMulCommClass R A A
inst✝⁵ : IsScalarTower R A A
inst✝⁴ : StarModule R A
inst✝³ : Semiring C
inst✝² : Algebra R C
inst✝¹ : StarRing C
inst✝ : StarModule R C
φ : A →⋆ₙₐ[R] C
x : Unitization R A
⊢ OneHom.toFun (↑↑↑(↑lift φ.toNonUnitalAlgHom)) (star x) = star (OneHom.toFun (↑↑↑(↑lift φ.toNonUnitalAlgHom)) x)
[PROOFSTEP]
induction x using Unitization.ind
[GOAL]
case h
R : Type u_1
A : Type u_2
C : Type u_3
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : StarRing R
inst✝⁹ : NonUnitalSemiring A
inst✝⁸ : StarRing A
inst✝⁷ : Module R A
inst✝⁶ : SMulCommClass R A A
inst✝⁵ : IsScalarTower R A A
inst✝⁴ : StarModule R A
inst✝³ : Semiring C
inst✝² : Algebra R C
inst✝¹ : StarRing C
inst✝ : StarModule R C
φ : A →⋆ₙₐ[R] C
r✝ : R
a✝ : A
⊢ OneHom.toFun (↑↑↑(↑lift φ.toNonUnitalAlgHom)) (star (inl r✝ + ↑a✝)) =
    star (OneHom.toFun (↑↑↑(↑lift φ.toNonUnitalAlgHom)) (inl r✝ + ↑a✝))
[PROOFSTEP]
simp [map_star]
[GOAL]
R : Type u_1
A : Type u_2
C : Type u_3
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : StarRing R
inst✝⁹ : NonUnitalSemiring A
inst✝⁸ : StarRing A
inst✝⁷ : Module R A
inst✝⁶ : SMulCommClass R A A
inst✝⁵ : IsScalarTower R A A
inst✝⁴ : StarModule R A
inst✝³ : Semiring C
inst✝² : Algebra R C
inst✝¹ : StarRing C
inst✝ : StarModule R C
φ : A →⋆ₙₐ[R] C
⊢ (fun φ => NonUnitalStarAlgHom.comp (StarAlgHom.toNonUnitalStarAlgHom φ) (inrNonUnitalStarAlgHom R A))
      ((fun φ =>
          { toAlgHom := ↑lift φ.toNonUnitalAlgHom,
            map_star' :=
              (_ :
                ∀ (x : Unitization R A),
                  OneHom.toFun (↑↑↑(↑lift φ.toNonUnitalAlgHom)) (star x) =
                    star (OneHom.toFun (↑↑↑(↑lift φ.toNonUnitalAlgHom)) x)) })
        φ) =
    φ
[PROOFSTEP]
ext
[GOAL]
case h
R : Type u_1
A : Type u_2
C : Type u_3
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : StarRing R
inst✝⁹ : NonUnitalSemiring A
inst✝⁸ : StarRing A
inst✝⁷ : Module R A
inst✝⁶ : SMulCommClass R A A
inst✝⁵ : IsScalarTower R A A
inst✝⁴ : StarModule R A
inst✝³ : Semiring C
inst✝² : Algebra R C
inst✝¹ : StarRing C
inst✝ : StarModule R C
φ : A →⋆ₙₐ[R] C
x✝ : A
⊢ ↑((fun φ => NonUnitalStarAlgHom.comp (StarAlgHom.toNonUnitalStarAlgHom φ) (inrNonUnitalStarAlgHom R A))
          ((fun φ =>
              { toAlgHom := ↑lift φ.toNonUnitalAlgHom,
                map_star' :=
                  (_ :
                    ∀ (x : Unitization R A),
                      OneHom.toFun (↑↑↑(↑lift φ.toNonUnitalAlgHom)) (star x) =
                        star (OneHom.toFun (↑↑↑(↑lift φ.toNonUnitalAlgHom)) x)) })
            φ))
      x✝ =
    ↑φ x✝
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
A : Type u_2
C : Type u_3
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : StarRing R
inst✝⁹ : NonUnitalSemiring A
inst✝⁸ : StarRing A
inst✝⁷ : Module R A
inst✝⁶ : SMulCommClass R A A
inst✝⁵ : IsScalarTower R A A
inst✝⁴ : StarModule R A
inst✝³ : Semiring C
inst✝² : Algebra R C
inst✝¹ : StarRing C
inst✝ : StarModule R C
φ : Unitization R A →⋆ₐ[R] C
⊢ ∀ (a : A),
    ↑((fun φ =>
              { toAlgHom := ↑lift φ.toNonUnitalAlgHom,
                map_star' :=
                  (_ :
                    ∀ (x : Unitization R A),
                      OneHom.toFun (↑↑↑(↑lift φ.toNonUnitalAlgHom)) (star x) =
                        star (OneHom.toFun (↑↑↑(↑lift φ.toNonUnitalAlgHom)) x)) })
            ((fun φ => NonUnitalStarAlgHom.comp (StarAlgHom.toNonUnitalStarAlgHom φ) (inrNonUnitalStarAlgHom R A)) φ))
        ↑a =
      ↑φ ↑a
[PROOFSTEP]
simp
