no goals
R : Type ?u.1799446
M : Type ?u.1799449
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.1800097
M₂ : Type ?u.1800100
inst✝¹⁰ : CommSemiring R₂
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : Module R₂ M₂
R₃ : Type ?u.1800287
M₃ : Type ?u.1800290
inst✝⁷ : CommRing R₃
inst✝⁶ : AddCommGroup M₃
inst✝⁵ : Module R₃ M₃
V : Type ?u.1800878
K : Type ?u.1800881
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.1802095
inst✝¹ : AddCommMonoid M₂'
inst✝ : Module R₂ M₂'
B : BilinForm R₁ M₁
b : Nondegenerate B
φ ψ₁ ψ₂ : M₁ →ₗ[R₁] M₁
hψ₁ : IsAdjointPair B B ψ₁ φ
hψ₂ : IsAdjointPair B B ψ₂ φ
v w : M₁
⊢ bilin (compLeft B ψ₁) v w = bilin (compLeft B ψ₂) v w
rw [compLeft_apply, compLeft_apply, hψ₁, hψ₂]