. obtain ⟨w, hw1, hw0, hEQ⟩ := equivalent_weightedSumSquares_units_of_nondegenerate'' Q (by simp [h]) h.symm hQ have := HasseMinkowski_of_Equivalent (V := V) hEQ
  rw [this]
  rw [HasseMinkowski, Isotropic, EverywhereLocallyIsotropic, Isotropic]
  simp at *
  sorry
case pos
V : Type
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module ℚ V
V₂ : Type ?u.130041
inst✝⁴ : AddCommGroup V₂
inst✝³ : Module ℚ V₂
inst✝² : FiniteDimensional ℚ V
F : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
Q : QuadraticForm ℚ V
h : FiniteDimensional.finrank ℚ V = 2
hQ : BilinForm.Nondegenerate (↑associated Q)
⊢ HasseMinkowski Q

case neg
V : Type
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module ℚ V
V₂ : Type ?u.130041
inst✝⁴ : AddCommGroup V₂
inst✝³ : Module ℚ V₂
inst✝² : FiniteDimensional ℚ V
F : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
Q : QuadraticForm ℚ V
h : FiniteDimensional.finrank ℚ V = 2
hQ : ¬BilinForm.Nondegenerate (↑associated Q)
⊢ HasseMinkowski Q
case neg
V : Type
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module ℚ V
V₂ : Type ?u.130041
inst✝⁴ : AddCommGroup V₂
inst✝³ : Module ℚ V₂
inst✝² : FiniteDimensional ℚ V
F : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
Q : QuadraticForm ℚ V
h : FiniteDimensional.finrank ℚ V = 2
hQ : ¬BilinForm.Nondegenerate (↑associated Q)
⊢ HasseMinkowski Q