no goals
R : Type ?u.1067797
M : Type ?u.1067800
inst✝²² : Semiring R
inst✝²¹ : AddCommMonoid M
inst✝²⁰ : Module R M
R₁ : Type ?u.1067836
M₁ : Type ?u.1067839
inst✝¹⁹ : Ring R₁
inst✝¹⁸ : AddCommGroup M₁
inst✝¹⁷ : Module R₁ M₁
R₂ : Type u_1
M₂ : Type u_2
inst✝¹⁶ : CommSemiring R₂
inst✝¹⁵ : AddCommMonoid M₂
inst✝¹⁴ : Module R₂ M₂
R₃ : Type ?u.1068638
M₃ : Type ?u.1068641
inst✝¹³ : CommRing R₃
inst✝¹² : AddCommGroup M₃
inst✝¹¹ : Module R₃ M₃
V : Type ?u.1069229
K : Type ?u.1069232
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_3
M₂'' : Type ?u.1070449
inst✝⁷ : AddCommMonoid M₂'
inst✝⁶ : AddCommMonoid M₂''
inst✝⁵ : Module R₂ M₂'
inst✝⁴ : Module R₂ M₂''
F : BilinForm R M
M' : Type ?u.1070760
inst✝³ : AddCommMonoid M'
inst✝² : Module R M'
B' : BilinForm R M'
f f' : M →ₗ[R] M'
g g' : M' →ₗ[R] M
M₁' : Type ?u.1071197
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₂
c : R₂
h : IsAdjointPair B₂ B₂' f₂ g₂
x : M₂
y : M₂'
⊢ bilin B₂' (↑(c • f₂) x) y = bilin B₂ x (↑(c • g₂) y)
rw [LinearMap.smul_apply, LinearMap.smul_apply, smul_left, smul_right, h]