no goals
R : Type u_1
R₁ : Type ?u.317511
R₂ : Type ?u.317514
R₃ : Type ?u.317517
M : Type u_4
M₁ : Type u_2
M₂ : Type u_3
Mₗ₁ : Type ?u.317529
Mₗ₁' : Type ?u.317532
Mₗ₂ : Type ?u.317535
Mₗ₂' : Type ?u.317538
K : Type ?u.317541
K₁ : Type ?u.317544
K₂ : Type ?u.317547
V : Type ?u.317550
V₁ : Type ?u.317553
V₂ : Type ?u.317556
n : Type ?u.317559
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
f' : M₁ →ₗ[R] M₂
g' : M₂ →ₗ[R] M₁
h : IsAdjointPair B B' f g
h' : IsAdjointPair B' B'' f' g'
x✝¹ : M
x✝ : M₂
⊢ ↑(↑B'' (↑(LinearMap.comp f' f) x✝¹)) x✝ = ↑(↑B x✝¹) (↑(LinearMap.comp g g') x✝)
rw [LinearMap.comp_apply, LinearMap.comp_apply, h', h]