no goals
R : Type u_1
R₁ : Type ?u.337838
R₂ : Type ?u.337841
R₃ : Type ?u.337844
M : Type u_2
M₁ : Type u_3
M₂ : Type ?u.337853
Mₗ₁ : Type ?u.337856
Mₗ₁' : Type ?u.337859
Mₗ₂ : Type ?u.337862
Mₗ₂' : Type ?u.337865
K : Type ?u.337868
K₁ : Type ?u.337871
K₂ : Type ?u.337874
V : Type ?u.337877
V₁ : Type ?u.337880
V₂ : Type ?u.337883
n : Type ?u.337886
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M₁
inst✝ : Module R M₁
B F : M →ₗ[R] M →ₗ[R] R
B' : M₁ →ₗ[R] M₁ →ₗ[R] 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.sub_apply, g.sub_apply, B'.map_sub₂, (B x).map_sub, h, h']