R : Type u_1
inst✝¹⁴ : CommSemiring R
R' : Type ?u.650481
inst✝¹³ : Monoid R'
R'' : Type ?u.650487
inst✝¹² : Semiring R''
M : Type u_2
N : Type u_4
P : Type u_3
Q : Type ?u.650502
S : Type ?u.650505
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : AddCommMonoid N
inst✝⁹ : AddCommMonoid P
inst✝⁸ : AddCommMonoid Q
inst✝⁷ : AddCommMonoid S
inst✝⁶ : Module R M
inst✝⁵ : Module R N
inst✝⁴ : Module R P
inst✝³ : Module R Q
inst✝² : Module R S
inst✝¹ : DistribMulAction R' M
inst✝ : Module R'' M
f✝ f : M →ₗ[R] N →ₗ[R] P
m : M
n : N
⊢ ↑(↑(↑(LinearMap.comp LinearMap.lflip (LinearMap.flip LinearMap.id)) m) n) f = ↑(↑f m) n
R : Type u_1
inst✝¹⁴ : CommSemiring R
R' : Type ?u.650481
inst✝¹³ : Monoid R'
R'' : Type ?u.650487
inst✝¹² : Semiring R''
M : Type u_2
N : Type u_4
P : Type u_3
Q : Type ?u.650502
S : Type ?u.650505
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : AddCommMonoid N
inst✝⁹ : AddCommMonoid P
inst✝⁸ : AddCommMonoid Q
inst✝⁷ : AddCommMonoid S
inst✝⁶ : Module R M
inst✝⁵ : Module R N
inst✝⁴ : Module R P
inst✝³ : Module R Q
inst✝² : Module R S
inst✝¹ : DistribMulAction R' M
inst✝ : Module R'' M
f✝ f : M →ₗ[R] N →ₗ[R] P
m : M
n : N
⊢ ↑(↑(uncurry R M N P) f) (m ⊗ₜ[R] n) = ↑(↑f m) n
rw [uncurry, LinearMap.flip_apply, lift.tmul]
no goals
R : Type u_1
inst✝¹⁴ : CommSemiring R
R' : Type ?u.650481
inst✝¹³ : Monoid R'
R'' : Type ?u.650487
inst✝¹² : Semiring R''
M : Type u_2
N : Type u_4
P : Type u_3
Q : Type ?u.650502
S : Type ?u.650505
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : AddCommMonoid N
inst✝⁹ : AddCommMonoid P
inst✝⁸ : AddCommMonoid Q
inst✝⁷ : AddCommMonoid S
inst✝⁶ : Module R M
inst✝⁵ : Module R N
inst✝⁴ : Module R P
inst✝³ : Module R Q
inst✝² : Module R S
inst✝¹ : DistribMulAction R' M
inst✝ : Module R'' M
f✝ f : M →ₗ[R] N →ₗ[R] P
m : M
n : N
⊢ ↑(↑(↑(LinearMap.comp LinearMap.lflip (LinearMap.flip LinearMap.id)) m) n) f = ↑(↑f m) n
rfl