-- Mathlib/LinearAlgebra/QuadraticForm/IsometryEquiv.lean
theorem equivalent_weightedSumSquares_units_of_nondegenerate' (Q : QuadraticForm K V)
    (hQ : (associated (R := K) Q).SeparatingLeft) :
    ∃ w : Fin (Module.finrank K V) → Kˣ, Equivalent Q (weightedSumSquares K w)

Proof state:
case intro
K : Type u_3
V : Type u_8
inst✝⁴ : Field K
inst✝³ : Invertible 2
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
Q : QuadraticForm K V
hQ : LinearMap.SeparatingLeft (associated Q)
v : Basis (Fin (Module.finrank K V)) K V
hv₁ : LinearMap.IsOrthoᵢ ((associatedHom K) Q) ⇑v
⊢ ∃ w, Equivalent Q (weightedSumSquares K w)

Tactic:
have hv₂ := hv₁.not_isOrtho_basis_self_of_separatingLeft hQ

Result:
case intro
K : Type u_3
V : Type u_8
inst✝⁴ : Field K
inst✝³ : Invertible 2
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
Q : QuadraticForm K V
hQ : LinearMap.SeparatingLeft (associated Q)
v : Basis (Fin (Module.finrank K V)) K V
hv₁ : LinearMap.IsOrthoᵢ ((associatedHom K) Q) ⇑v
hv₂ : ∀ (i : Fin (Module.finrank K V)), ¬LinearMap.IsOrtho ((associatedHom K) Q) (v i) (v i)
⊢ ∃ w, Equivalent Q (weightedSumSquares K w)

Proof state:
K : Type u_3
V : Type u_8
inst✝⁴ : Field K
inst✝³ : Invertible 2
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
Q : QuadraticForm K V
hQ : LinearMap.SeparatingLeft (associated Q)
⊢ ∃ w, Equivalent Q (weightedSumSquares K w)

Tactic:
obtain ⟨v, hv₁⟩ := exists_orthogonal_basis (associated_isSymm K Q)

Result:
case intro
K : Type u_3
V : Type u_8
inst✝⁴ : Field K
inst✝³ : Invertible 2
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
Q : QuadraticForm K V
hQ : LinearMap.SeparatingLeft (associated Q)
v : Basis (Fin (Module.finrank K V)) K V
hv₁ : LinearMap.IsOrthoᵢ ((associatedHom K) Q) ⇑v
⊢ ∃ w, Equivalent Q (weightedSumSquares K w)

Proof state:
case intro
K : Type u_3
V : Type u_8
inst✝⁴ : Field K
inst✝³ : Invertible 2
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
Q : QuadraticForm K V
hQ : LinearMap.SeparatingLeft (associated Q)
v : Basis (Fin (Module.finrank K V)) K V
hv₁ : LinearMap.IsOrthoᵢ ((associatedHom K) Q) ⇑v
hv₂ : ∀ (i : Fin (Module.finrank K V)), ¬LinearMap.IsOrtho ((associatedHom K) Q) (v i) (v i)
⊢ ∃ w, Equivalent Q (weightedSumSquares K w)

Tactic:
simp_rw [LinearMap.IsOrtho, associated_eq_self_apply] at hv₂

Result:
case intro
K : Type u_3
V : Type u_8
inst✝⁴ : Field K
inst✝³ : Invertible 2
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
Q : QuadraticForm K V
hQ : LinearMap.SeparatingLeft (associated Q)
v : Basis (Fin (Module.finrank K V)) K V
hv₁ : LinearMap.IsOrthoᵢ ((associatedHom K) Q) ⇑v
hv₂ : ∀ (i : Fin (Module.finrank K V)), ¬Q (v i) = 0
⊢ ∃ w, Equivalent Q (weightedSumSquares K w)

Proof state:
case intro
K : Type u_3
V : Type u_8
inst✝⁴ : Field K
inst✝³ : Invertible 2
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
Q : QuadraticForm K V
hQ : LinearMap.SeparatingLeft (associated Q)
v : Basis (Fin (Module.finrank K V)) K V
hv₁ : LinearMap.IsOrthoᵢ ((associatedHom K) Q) ⇑v
hv₂ : ∀ (i : Fin (Module.finrank K V)), ¬Q (v i) = 0
⊢ ∃ w, Equivalent Q (weightedSumSquares K w)

Tactic:
exact ⟨fun i => Units.mk0 _ (hv₂ i), ⟨Q.isometryEquivWeightedSumSquares v hv₁⟩⟩

Result:
no goals