no goals
R : Type ?u.1050969
M : Type ?u.1050972
inst✝²² : Semiring R
inst✝²¹ : AddCommMonoid M
inst✝²⁰ : Module R M
R₁ : Type u_1
M₁ : Type u_2
inst✝¹⁹ : Ring R₁
inst✝¹⁸ : AddCommGroup M₁
inst✝¹⁷ : Module R₁ M₁
R₂ : Type ?u.1051620
M₂ : Type ?u.1051623
inst✝¹⁶ : CommSemiring R₂
inst✝¹⁵ : AddCommMonoid M₂
inst✝¹⁴ : Module R₂ M₂
R₃ : Type ?u.1051810
M₃ : Type ?u.1051813
inst✝¹³ : CommRing R₃
inst✝¹² : AddCommGroup M₃
inst✝¹¹ : Module R₃ M₃
V : Type ?u.1052401
K : Type ?u.1052404
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.1053618
M₂'' : Type ?u.1053621
inst✝⁷ : AddCommMonoid M₂'
inst✝⁶ : AddCommMonoid M₂''
inst✝⁵ : Module R₂ M₂'
inst✝⁴ : Module R₂ M₂''
F : BilinForm R M
M' : Type ?u.1053932
inst✝³ : AddCommMonoid M'
inst✝² : Module R M'
B' : BilinForm R M'
f f' : M →ₗ[R] M'
g g' : M' →ₗ[R] M
M₁' : Type u_3
inst✝¹ : AddCommGroup 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.sub_apply, LinearMap.sub_apply, sub_left, sub_right, h, h']