case H
S : Type u_1
R : Type u_3
A : Type u_2
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.381212
inst✝¹ : Semiring C
inst✝ : Algebra R C
φ ψ : Unitization R A →ₐ[S] B
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
S : Type u_1
R : Type u_3
A : Type u_2
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.381212
inst✝¹ : Semiring C
inst✝ : Algebra R C
φ ψ : Unitization R A →ₐ[S] B
h : ∀ (a : A), ↑φ ↑a = ↑ψ ↑a
h' : ∀ (r : R), ↑φ (↑(algebraMap R (Unitization R A)) r) = ↑ψ (↑(algebraMap R (Unitization R A)) r)
⊢ φ = ψ
ext x
case H.h
S : Type u_1
R : Type u_3
A : Type u_2
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.381212
inst✝¹ : Semiring C
inst✝ : Algebra R C
φ ψ : Unitization R A →ₐ[S] B
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✝)
case H
S : Type u_1
R : Type u_3
A : Type u_2
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.381212
inst✝¹ : Semiring C
inst✝ : Algebra R C
φ ψ : Unitization R A →ₐ[S] B
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
induction x using Unitization.ind
no goals
case H.h
S : Type u_1
R : Type u_3
A : Type u_2
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.381212
inst✝¹ : Semiring C
inst✝ : Algebra R C
φ ψ : Unitization R A →ₐ[S] B
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✝)
simp only [map_add, ← algebraMap_eq_inl, h, h']