R : Type u
inst✝¹⁰ : CommSemiring R
A : Type v₁
inst✝⁹ : Semiring A
inst✝⁸ : Algebra R A
B : Type v₂
inst✝⁷ : Semiring B
inst✝⁶ : Algebra R B
S : Type ?u.721832
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra R S
inst✝³ : Algebra S A
inst✝² : IsScalarTower R S A
C : Type v₃
inst✝¹ : Semiring C
inst✝ : Algebra R C
g h : A ⊗[R] B →ₐ[R] C
H : ∀ (a : A) (b : B), ↑g (a ⊗ₜ[R] b) = ↑h (a ⊗ₜ[R] b)
⊢ AlgHom.toLinearMap g = AlgHom.toLinearMap h
R : Type u
inst✝¹⁰ : CommSemiring R
A : Type v₁
inst✝⁹ : Semiring A
inst✝⁸ : Algebra R A
B : Type v₂
inst✝⁷ : Semiring B
inst✝⁶ : Algebra R B
S : Type ?u.721832
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra R S
inst✝³ : Algebra S A
inst✝² : IsScalarTower R S A
C : Type v₃
inst✝¹ : Semiring C
inst✝ : Algebra R C
g h : A ⊗[R] B →ₐ[R] C
H : ∀ (a : A) (b : B), ↑g (a ⊗ₜ[R] b) = ↑h (a ⊗ₜ[R] b)
⊢ g = h
apply @AlgHom.toLinearMap_injective R (A ⊗[R] B) C _ _ _ _ _ _ _ _
case a.h.h
R : Type u
inst✝¹⁰ : CommSemiring R
A : Type v₁
inst✝⁹ : Semiring A
inst✝⁸ : Algebra R A
B : Type v₂
inst✝⁷ : Semiring B
inst✝⁶ : Algebra R B
S : Type ?u.721832
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra R S
inst✝³ : Algebra S A
inst✝² : IsScalarTower R S A
C : Type v₃
inst✝¹ : Semiring C
inst✝ : Algebra R C
g h : A ⊗[R] B →ₐ[R] C
H : ∀ (a : A) (b : B), ↑g (a ⊗ₜ[R] b) = ↑h (a ⊗ₜ[R] b)
x✝¹ : A
x✝ : B
⊢ ↑(↑(AlgebraTensorModule.curry (AlgHom.toLinearMap g)) x✝¹) x✝ =
    ↑(↑(AlgebraTensorModule.curry (AlgHom.toLinearMap h)) x✝¹) x✝
R : Type u
inst✝¹⁰ : CommSemiring R
A : Type v₁
inst✝⁹ : Semiring A
inst✝⁸ : Algebra R A
B : Type v₂
inst✝⁷ : Semiring B
inst✝⁶ : Algebra R B
S : Type ?u.721832
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra R S
inst✝³ : Algebra S A
inst✝² : IsScalarTower R S A
C : Type v₃
inst✝¹ : Semiring C
inst✝ : Algebra R C
g h : A ⊗[R] B →ₐ[R] C
H : ∀ (a : A) (b : B), ↑g (a ⊗ₜ[R] b) = ↑h (a ⊗ₜ[R] b)
⊢ AlgHom.toLinearMap g = AlgHom.toLinearMap h
ext
no goals
case a.h.h
R : Type u
inst✝¹⁰ : CommSemiring R
A : Type v₁
inst✝⁹ : Semiring A
inst✝⁸ : Algebra R A
B : Type v₂
inst✝⁷ : Semiring B
inst✝⁶ : Algebra R B
S : Type ?u.721832
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra R S
inst✝³ : Algebra S A
inst✝² : IsScalarTower R S A
C : Type v₃
inst✝¹ : Semiring C
inst✝ : Algebra R C
g h : A ⊗[R] B →ₐ[R] C
H : ∀ (a : A) (b : B), ↑g (a ⊗ₜ[R] b) = ↑h (a ⊗ₜ[R] b)
x✝¹ : A
x✝ : B
⊢ ↑(↑(AlgebraTensorModule.curry (AlgHom.toLinearMap g)) x✝¹) x✝ =
    ↑(↑(AlgebraTensorModule.curry (AlgHom.toLinearMap h)) x✝¹) x✝
simp [H]