S : Type ?u.453261
R : Type u_1
R₁ : Type ?u.453267
M : Type u_2
inst✝⁷ : Ring R
inst✝⁶ : CommRing R₁
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module R₁ M
inst✝² : CommSemiring S
inst✝¹ : Algebra S R
inst✝ : Invertible 2
B₁ : BilinForm R M
Q✝ Q : QuadraticForm R M
hB₁ : ↑associated' Q ≠ 0
⊢ ¬∀ (x : M), ↑Q x = 0
S : Type ?u.453261
R : Type u_1
R₁ : Type ?u.453267
M : Type u_2
inst✝⁷ : Ring R
inst✝⁶ : CommRing R₁
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module R₁ M
inst✝² : CommSemiring S
inst✝¹ : Algebra S R
inst✝ : Invertible 2
B₁ : BilinForm R M
Q✝ Q : QuadraticForm R M
hB₁ : ↑associated' Q ≠ 0
⊢ ∃ x, ↑Q x ≠ 0
rw [← not_forall]
S : Type ?u.453261
R : Type u_1
R₁ : Type ?u.453267
M : Type u_2
inst✝⁷ : Ring R
inst✝⁶ : CommRing R₁
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module R₁ M
inst✝² : CommSemiring S
inst✝¹ : Algebra S R
inst✝ : Invertible 2
B₁ : BilinForm R M
Q✝ Q : QuadraticForm R M
hB₁ : ↑associated' Q ≠ 0
h : ∀ (x : M), ↑Q x = 0
⊢ False
S : Type ?u.453261
R : Type u_1
R₁ : Type ?u.453267
M : Type u_2
inst✝⁷ : Ring R
inst✝⁶ : CommRing R₁
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module R₁ M
inst✝² : CommSemiring S
inst✝¹ : Algebra S R
inst✝ : Invertible 2
B₁ : BilinForm R M
Q✝ Q : QuadraticForm R M
hB₁ : ↑associated' Q ≠ 0
⊢ ¬∀ (x : M), ↑Q x = 0
intro h
S : Type ?u.453261
R : Type u_1
R₁ : Type ?u.453267
M : Type u_2
inst✝⁷ : Ring R
inst✝⁶ : CommRing R₁
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module R₁ M
inst✝² : CommSemiring S
inst✝¹ : Algebra S R
inst✝ : Invertible 2
B₁ : BilinForm R M
Q✝ Q : QuadraticForm R M
hB₁ : ↑associated' Q ≠ 0
h : ∀ (x : M), ↑Q x = 0
⊢ ↑associated' Q = 0
S : Type ?u.453261
R : Type u_1
R₁ : Type ?u.453267
M : Type u_2
inst✝⁷ : Ring R
inst✝⁶ : CommRing R₁
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module R₁ M
inst✝² : CommSemiring S
inst✝¹ : Algebra S R
inst✝ : Invertible 2
B₁ : BilinForm R M
Q✝ Q : QuadraticForm R M
hB₁ : ↑associated' Q ≠ 0
h : ∀ (x : M), ↑Q x = 0
⊢ False
apply hB₁
no goals
S : Type ?u.453261
R : Type u_1
R₁ : Type ?u.453267
M : Type u_2
inst✝⁷ : Ring R
inst✝⁶ : CommRing R₁
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module R₁ M
inst✝² : CommSemiring S
inst✝¹ : Algebra S R
inst✝ : Invertible 2
B₁ : BilinForm R M
Q✝ Q : QuadraticForm R M
hB₁ : ↑associated' Q ≠ 0
h : ∀ (x : M), ↑Q x = 0
⊢ ↑associated' Q = 0
rw [(QuadraticForm.ext h : Q = 0), LinearMap.map_zero]