Theorem: LinearMap.baseChange_comp (AntLorentz/BaseChange.lean)

State before:
R✝ : Type ?u.401799
M✝ : Type ?u.401802
inst✝¹⁶ : CommRing R✝
inst✝¹⁵ : AddCommGroup M✝
inst✝¹⁴ : Module R✝ M✝
M₂ : Type ?u.402563
inst✝¹³ : AddCommGroup M₂
inst✝¹² : Module R✝ M₂
A✝ : Type ?u.403266
inst✝¹¹ : Semiring A✝
inst✝¹⁰ : Algebra R✝ A✝
inst✝⁹ : Invertible 2
B : Type u_1
R : Type u_2
A : Type u_3
M : Type u_4
N : Type u_5
inst✝⁸ : CommRing R
inst✝⁷ : Ring A
inst✝⁶ : Algebra R A
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid B
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R B
f : M →ₗ[R] N
g : N →ₗ[R] B
⊢ comp (baseChange A g) (baseChange A f) = baseChange A (comp g f)
Tactic:
ext
State after:
case a.h.h
R✝ : Type ?u.401799
M✝ : Type ?u.401802
inst✝¹⁶ : CommRing R✝
inst✝¹⁵ : AddCommGroup M✝
inst✝¹⁴ : Module R✝ M✝
M₂ : Type ?u.402563
inst✝¹³ : AddCommGroup M₂
inst✝¹² : Module R✝ M₂
A✝ : Type ?u.403266
inst✝¹¹ : Semiring A✝
inst✝¹⁰ : Algebra R✝ A✝
inst✝⁹ : Invertible 2
B : Type u_1
R : Type u_2
A : Type u_3
M : Type u_4
N : Type u_5
inst✝⁸ : CommRing R
inst✝⁷ : Ring A
inst✝⁶ : Algebra R A
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid B
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R B
f : M →ₗ[R] N
g : N →ₗ[R] B
x✝ : M
⊢ ↑(↑(AlgebraTensorModule.curry (comp (baseChange A g) (baseChange A f))) 1) x✝ =
    ↑(↑(AlgebraTensorModule.curry (baseChange A (comp g f))) 1) x✝

State before:
case a.h.h
R✝ : Type ?u.401799
M✝ : Type ?u.401802
inst✝¹⁶ : CommRing R✝
inst✝¹⁵ : AddCommGroup M✝
inst✝¹⁴ : Module R✝ M✝
M₂ : Type ?u.402563
inst✝¹³ : AddCommGroup M₂
inst✝¹² : Module R✝ M₂
A✝ : Type ?u.403266
inst✝¹¹ : Semiring A✝
inst✝¹⁰ : Algebra R✝ A✝
inst✝⁹ : Invertible 2
B : Type u_1
R : Type u_2
A : Type u_3
M : Type u_4
N : Type u_5
inst✝⁸ : CommRing R
inst✝⁷ : Ring A
inst✝⁶ : Algebra R A
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid B
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R B
f : M →ₗ[R] N
g : N →ₗ[R] B
x✝ : M
⊢ ↑(↑(AlgebraTensorModule.curry (comp (baseChange A g) (baseChange A f))) 1) x✝ =
    ↑(↑(AlgebraTensorModule.curry (baseChange A (comp g f))) 1) x✝
Tactic:
simp
State after:
no goals