case a.h.h
R : Type u_4
A : Type u_1
B : Type ?u.408400
M : Type u_2
N : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R B
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
r : R
f g : M →ₗ[R] N
x✝ : M
⊢ ↑(↑(AlgebraTensorModule.curry (baseChange A (f + g))) 1) x✝ =
    ↑(↑(AlgebraTensorModule.curry (baseChange A f + baseChange A g)) 1) x✝
R : Type u_4
A : Type u_1
B : Type ?u.408400
M : Type u_2
N : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R B
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
r : R
f g : M →ₗ[R] N
⊢ baseChange A (f + g) = baseChange A f + baseChange A g
ext
no goals
case a.h.h
R : Type u_4
A : Type u_1
B : Type ?u.408400
M : Type u_2
N : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R B
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
r : R
f g : M →ₗ[R] N
x✝ : M
⊢ ↑(↑(AlgebraTensorModule.curry (baseChange A (f + g))) 1) x✝ =
    ↑(↑(AlgebraTensorModule.curry (baseChange A f + baseChange A g)) 1) x✝
simp [baseChange_eq_ltensor, -baseChange_tmul]