no goals
R : Type u_1
R₁ : Type ?u.311393
R₂ : Type ?u.311396
R₃ : Type ?u.311399
M : Type u_2
M₁ : Type u_3
M₂ : Type ?u.311408
Mₗ₁ : Type ?u.311411
Mₗ₁' : Type ?u.311414
Mₗ₂ : Type ?u.311417
Mₗ₂' : Type ?u.311420
K : Type ?u.311423
K₁ : Type ?u.311426
K₂ : Type ?u.311429
V : Type ?u.311432
V₁ : Type ?u.311435
V₂ : Type ?u.311438
n : Type ?u.311441
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
I : R →+* R
B F : M →ₗ[R] M →ₛₗ[I] R
B' : M₁ →ₗ[R] M₁ →ₛₗ[I] R
B'' : M₂ →ₗ[R] M₂ →ₛₗ[I] R
f f' : M →ₗ[R] M₁
g g' : M₁ →ₗ[R] M
h : IsAdjointPair B B' f g
h' : IsAdjointPair B B' f' g'
x : M
x✝ : M₁
⊢ ↑(↑B' (↑(f + f') x)) x✝ = ↑(↑B x) (↑(g + g') x✝)
rw [f.add_apply, g.add_apply, B'.map_add₂, (B x).map_add, h, h']