case intro
S : Type ?u.150446
R : Type u_1
R₁ : Type ?u.150452
M : Type u_2
inst✝³ : Ring R
inst✝² : CommRing R₁
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
a : R
x y : M
B : BilinForm R M
h : ∀ (x y : M), ↑Q (x + y) = ↑Q x + ↑Q y + BilinForm.bilin B x y
⊢ polar (↑Q) (a • x) y = a * polar (↑Q) x y
S : Type ?u.150446
R : Type u_1
R₁ : Type ?u.150452
M : Type u_2
inst✝³ : Ring R
inst✝² : CommRing R₁
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
a : R
x y : M
⊢ polar (↑Q) (a • x) y = a * polar (↑Q) x y
obtain ⟨B, h⟩ := Q.exists_companion
no goals
case intro
S : Type ?u.150446
R : Type u_1
R₁ : Type ?u.150452
M : Type u_2
inst✝³ : Ring R
inst✝² : CommRing R₁
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
a : R
x y : M
B : BilinForm R M
h : ∀ (x y : M), ↑Q (x + y) = ↑Q x + ↑Q y + BilinForm.bilin B x y
⊢ polar (↑Q) (a • x) y = a * polar (↑Q) x y
simp_rw [polar, h, Q.map_smul, BilinForm.smul_left, sub_sub, add_sub_cancel']