Theorem: QuadraticForm.ex (AntLorentz/HasseMinkowski2.lean)

State before:
V : Type
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)
⊢ Hasse_Minkowski Q
Tactic:
obtain ⟨w, hw1, hw0, hEQ⟩ := equivalent_weightedSumSquares_units_of_nondegenerate'' Q _ h.symm hQ
State after:
case intro.intro.intro
V : Type
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)
w : Fin 2 → ℤ
hw1 : w { val := 0, isLt := (_ : 0 < 2) } = 1
hw0 : ∀ (i : Fin 2), Squarefree (w i)
hEQ : Equivalent Q (weightedSumSquares ℚ w)
⊢ Hasse_Minkowski Q