no goals
R : Type u_1
R₁ : Type ?u.346295
R₂ : Type ?u.346298
R₃ : Type ?u.346301
M : Type u_2
M₁ : Type u_3
M₂ : Type ?u.346310
Mₗ₁ : Type ?u.346313
Mₗ₁' : Type ?u.346316
Mₗ₂ : Type ?u.346319
Mₗ₂' : Type ?u.346322
K : Type ?u.346325
K₁ : Type ?u.346328
K₂ : Type ?u.346331
V : Type ?u.346334
V₁ : Type ?u.346337
V₂ : Type ?u.346340
n : Type ?u.346343
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
c : R
h : IsAdjointPair B B' f g
x✝¹ : M
x✝ : M₁
⊢ ↑(↑B' (↑(c • f) x✝¹)) x✝ = ↑(↑B x✝¹) (↑(c • g) x✝)
simp [h _]