no goals
R : Type u_1
M : Type u_2
inst✝²⁰ : Semiring R
inst✝¹⁹ : AddCommMonoid M
inst✝¹⁸ : Module R M
R₁ : Type ?u.1034553
M₁ : Type ?u.1034556
inst✝¹⁷ : Ring R₁
inst✝¹⁶ : AddCommGroup M₁
inst✝¹⁵ : Module R₁ M₁
R₂ : Type ?u.1035165
M₂ : Type ?u.1035168
inst✝¹⁴ : CommSemiring R₂
inst✝¹³ : AddCommMonoid M₂
inst✝¹² : Module R₂ M₂
R₃ : Type ?u.1035355
M₃ : Type ?u.1035358
inst✝¹¹ : CommRing R₃
inst✝¹⁰ : AddCommGroup M₃
inst✝⁹ : Module R₃ M₃
V : Type ?u.1035946
K : Type ?u.1035949
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.1037163
M₂'' : Type ?u.1037166
inst✝⁵ : AddCommMonoid M₂'
inst✝⁴ : AddCommMonoid M₂''
inst✝³ : Module R₂ M₂'
inst✝² : Module R₂ M₂''
F : BilinForm R M
M' : Type u_3
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
B' : BilinForm R M'
f f' : M →ₗ[R] M'
g g' : M' →ₗ[R] M
h : IsAdjointPair B B' f g
h' : IsAdjointPair B B' f' g'
x : M
y : M'
⊢ bilin B' (↑(f + f') x) y = bilin B x (↑(g + g') y)
rw [LinearMap.add_apply, LinearMap.add_apply, add_left, add_right, h, h']