no goals
R : Type u_1
M : Type u_2
inst✝²⁴ : Semiring R
inst✝²³ : AddCommMonoid M
inst✝²² : Module R M
R₁ : Type ?u.1104318
M₁ : Type ?u.1104321
inst✝²¹ : Ring R₁
inst✝²⁰ : AddCommGroup M₁
inst✝¹⁹ : Module R₁ M₁
R₂ : Type ?u.1104930
M₂ : Type ?u.1104933
inst✝¹⁸ : CommSemiring R₂
inst✝¹⁷ : AddCommMonoid M₂
inst✝¹⁶ : Module R₂ M₂
R₃ : Type ?u.1105120
M₃ : Type ?u.1105123
inst✝¹⁵ : CommRing R₃
inst✝¹⁴ : AddCommGroup M₃
inst✝¹³ : Module R₃ M₃
V : Type ?u.1105711
K : Type ?u.1105714
inst✝¹² : Field K
inst✝¹¹ : AddCommGroup V
inst✝¹⁰ : Module K V
B : BilinForm R M
B₁ : BilinForm R₁ M₁
B₂ : BilinForm R₂ M₂
M₂' : Type ?u.1106928
M₂'' : Type ?u.1106931
inst✝⁹ : AddCommMonoid M₂'
inst✝⁸ : AddCommMonoid M₂''
inst✝⁷ : Module R₂ M₂'
inst✝⁶ : Module R₂ M₂''
F : BilinForm R M
M' : Type ?u.1107242
inst✝⁵ : AddCommMonoid M'
inst✝⁴ : Module R M'
B' : BilinForm R M'
f✝ f'✝ : M →ₗ[R] M'
g✝ g'✝ : M' →ₗ[R] M
M₁' : Type ?u.1107679
inst✝³ : AddCommGroup M₁'
inst✝² : Module R₁ M₁'
B₁' : BilinForm R₁ M₁'
f₁ f₁' : M₁ →ₗ[R₁] M₁'
g₁ g₁' : M₁' →ₗ[R₁] M₁
B₂' : BilinForm R₂ M₂'
f₂ f₂' : M₂ →ₗ[R₂] M₂'
g₂ g₂' : M₂' →ₗ[R₂] M₂
M'' : Type ?u.1110158
inst✝¹ : AddCommMonoid M''
inst✝ : Module R M''
B'' : BilinForm R M''
f g f' g' : Module.End R M
h : IsAdjointPair B B f g
h' : IsAdjointPair B B f' g'
x y : M
⊢ bilin B (↑(f * f') x) y = bilin B x (↑(g' * g) y)
rw [LinearMap.mul_apply, LinearMap.mul_apply, h, h']