Theorem: QuadraticForm.equivalent_weightedSumSquares_units_of_nondegenerate'' (AntLorentz/Diagonalize.lean)

State before:
ι : Type ?u.120511
R✝ : Type ?u.120514
K : Type ?u.120517
M✝ : Type ?u.120520
M₁ : Type ?u.120523
M₂ : Type ?u.120526
M₃ : Type ?u.120529
V : Type u_1
R : Type ?u.120535
M : Type ?u.120538
inst✝⁶ : Field R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : FiniteDimensional R M
inst✝² : Invertible 2
Q✝ : QuadraticForm R M
inst✝¹ : AddCommGroup V
inst✝ : Module ℚ V
a : ℕ
Q : QuadraticForm ℚ V
h : 0 < FiniteDimensional.finrank ℚ V
ha : a = FiniteDimensional.finrank ℚ V
hQ : BilinForm.Nondegenerate (↑associated Q)
⊢ ∃ w hw1 hw0, Equivalent Q (weightedSumSquares ℚ w)
Tactic:
sorry
State after:
no goals