case a.h.h
R : Type u_4
A : Type u_1
B : Type ?u.473826
M : Type u_2
N : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Ring A
inst✝⁶ : Algebra R A
inst✝⁵ : Ring B
inst✝⁴ : Algebra R B
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
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.473826
M : Type u_2
N : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Ring A
inst✝⁶ : Algebra R A
inst✝⁵ : Ring B
inst✝⁴ : Algebra R B
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
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.473826
M : Type u_2
N : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Ring A
inst✝⁶ : Algebra R A
inst✝⁵ : Ring B
inst✝⁴ : Algebra R B
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
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, tmul_sub]