rw [QuadraticForm.Isotropic]
case mp
V : Type
inst✝⁴ : AddCommGroup V
inst✝³ : Module ℚ V
inst✝² : FiniteDimensional ℚ V
F✝ : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
hV : Module.rank ℚ V = 0
F : QuadraticForm ℚ V
a✝ : ¬EverywhereLocallyIsotropic F
⊢ ¬Isotropic F
case mp
V : Type
inst✝⁴ : AddCommGroup V
inst✝³ : Module ℚ V
inst✝² : FiniteDimensional ℚ V
F✝ : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
hV : Module.rank ℚ V = 0
F : QuadraticForm ℚ V
a✝ : ¬EverywhereLocallyIsotropic F
⊢ ¬¬Anisotropic F