[GOAL]
ι : Type u_1
R : Type u_2
K : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
V : Type u_8
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : AddCommMonoid M₃
inst✝³ : Module R M
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R M₃
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
Q₃ : QuadraticForm R M₃
f g : IsometryEquiv Q₁ Q₂
⊢ (fun f => ↑f.toLinearEquiv) f = (fun f => ↑f.toLinearEquiv) g →
    (fun f => ↑(LinearEquiv.symm f.toLinearEquiv)) f = (fun f => ↑(LinearEquiv.symm f.toLinearEquiv)) g → f = g
[PROOFSTEP]
cases f
[GOAL]
case mk
ι : Type u_1
R : Type u_2
K : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
V : Type u_8
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : AddCommMonoid M₃
inst✝³ : Module R M
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R M₃
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
Q₃ : QuadraticForm R M₃
g : IsometryEquiv Q₁ Q₂
toLinearEquiv✝ : M₁ ≃ₗ[R] M₂
map_app'✝ : ∀ (m : M₁), ↑Q₂ (AddHom.toFun toLinearEquiv✝.toAddHom m) = ↑Q₁ m
⊢ (fun f => ↑f.toLinearEquiv) { toLinearEquiv := toLinearEquiv✝, map_app' := map_app'✝ } =
      (fun f => ↑f.toLinearEquiv) g →
    (fun f => ↑(LinearEquiv.symm f.toLinearEquiv)) { toLinearEquiv := toLinearEquiv✝, map_app' := map_app'✝ } =
        (fun f => ↑(LinearEquiv.symm f.toLinearEquiv)) g →
      { toLinearEquiv := toLinearEquiv✝, map_app' := map_app'✝ } = g
[PROOFSTEP]
cases g
[GOAL]
case mk.mk
ι : Type u_1
R : Type u_2
K : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
V : Type u_8
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : AddCommMonoid M₃
inst✝³ : Module R M
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R M₃
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
Q₃ : QuadraticForm R M₃
toLinearEquiv✝¹ : M₁ ≃ₗ[R] M₂
map_app'✝¹ : ∀ (m : M₁), ↑Q₂ (AddHom.toFun toLinearEquiv✝¹.toAddHom m) = ↑Q₁ m
toLinearEquiv✝ : M₁ ≃ₗ[R] M₂
map_app'✝ : ∀ (m : M₁), ↑Q₂ (AddHom.toFun toLinearEquiv✝.toAddHom m) = ↑Q₁ m
⊢ (fun f => ↑f.toLinearEquiv) { toLinearEquiv := toLinearEquiv✝¹, map_app' := map_app'✝¹ } =
      (fun f => ↑f.toLinearEquiv) { toLinearEquiv := toLinearEquiv✝, map_app' := map_app'✝ } →
    (fun f => ↑(LinearEquiv.symm f.toLinearEquiv)) { toLinearEquiv := toLinearEquiv✝¹, map_app' := map_app'✝¹ } =
        (fun f => ↑(LinearEquiv.symm f.toLinearEquiv)) { toLinearEquiv := toLinearEquiv✝, map_app' := map_app'✝ } →
      { toLinearEquiv := toLinearEquiv✝¹, map_app' := map_app'✝¹ } =
        { toLinearEquiv := toLinearEquiv✝, map_app' := map_app'✝ }
[PROOFSTEP]
simp (config := { contextual := true })
[GOAL]
ι : Type u_1
R : Type u_2
K : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
V : Type u_8
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : AddCommMonoid M₃
inst✝³ : Module R M
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R M₃
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
Q₃ : QuadraticForm R M₃
f : IsometryEquiv Q₁ Q₂
src✝ : M₂ ≃ₗ[R] M₁ := LinearEquiv.symm f.toLinearEquiv
⊢ ∀ (m : M₂),
    ↑Q₁
        (AddHom.toFun
          (↑{ toLinearMap := ↑src✝, invFun := src✝.invFun,
                left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
                right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }).toAddHom
          m) =
      ↑Q₂ m
[PROOFSTEP]
intro m
[GOAL]
ι : Type u_1
R : Type u_2
K : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
V : Type u_8
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : AddCommMonoid M₃
inst✝³ : Module R M
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R M₃
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
Q₃ : QuadraticForm R M₃
f : IsometryEquiv Q₁ Q₂
src✝ : M₂ ≃ₗ[R] M₁ := LinearEquiv.symm f.toLinearEquiv
m : M₂
⊢ ↑Q₁
      (AddHom.toFun
        (↑{ toLinearMap := ↑src✝, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
              right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }).toAddHom
        m) =
    ↑Q₂ m
[PROOFSTEP]
rw [← f.map_app]
[GOAL]
ι : Type u_1
R : Type u_2
K : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
V : Type u_8
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : AddCommMonoid M₃
inst✝³ : Module R M
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R M₃
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
Q₃ : QuadraticForm R M₃
f : IsometryEquiv Q₁ Q₂
src✝ : M₂ ≃ₗ[R] M₁ := LinearEquiv.symm f.toLinearEquiv
m : M₂
⊢ ↑Q₂
      (↑f
        (AddHom.toFun
          (↑{ toLinearMap := ↑src✝, invFun := src✝.invFun,
                left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
                right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }).toAddHom
          m)) =
    ↑Q₂ m
[PROOFSTEP]
congr
[GOAL]
case h.e_6.h
ι : Type u_1
R : Type u_2
K : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
V : Type u_8
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : AddCommMonoid M₃
inst✝³ : Module R M
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R M₃
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
Q₃ : QuadraticForm R M₃
f : IsometryEquiv Q₁ Q₂
src✝ : M₂ ≃ₗ[R] M₁ := LinearEquiv.symm f.toLinearEquiv
m : M₂
⊢ ↑f
      (AddHom.toFun
        (↑{ toLinearMap := ↑src✝, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
              right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }).toAddHom
        m) =
    m
[PROOFSTEP]
exact f.toLinearEquiv.apply_symm_apply m
[GOAL]
ι : Type u_1
R : Type u_2
K : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
V : Type u_8
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : AddCommMonoid M₃
inst✝³ : Module R M
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R M₃
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
Q₃ : QuadraticForm R M₃
f : IsometryEquiv Q₁ Q₂
g : IsometryEquiv Q₂ Q₃
src✝ : M₁ ≃ₗ[R] M₃ := LinearEquiv.trans f.toLinearEquiv g.toLinearEquiv
⊢ ∀ (m : M₁),
    ↑Q₃
        (AddHom.toFun
          (↑{ toLinearMap := ↑src✝, invFun := src✝.invFun,
                left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
                right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }).toAddHom
          m) =
      ↑Q₁ m
[PROOFSTEP]
intro m
[GOAL]
ι : Type u_1
R : Type u_2
K : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
V : Type u_8
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : AddCommMonoid M₃
inst✝³ : Module R M
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R M₃
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
Q₃ : QuadraticForm R M₃
f : IsometryEquiv Q₁ Q₂
g : IsometryEquiv Q₂ Q₃
src✝ : M₁ ≃ₗ[R] M₃ := LinearEquiv.trans f.toLinearEquiv g.toLinearEquiv
m : M₁
⊢ ↑Q₃
      (AddHom.toFun
        (↑{ toLinearMap := ↑src✝, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
              right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }).toAddHom
        m) =
    ↑Q₁ m
[PROOFSTEP]
rw [← f.map_app, ← g.map_app]
[GOAL]
ι : Type u_1
R : Type u_2
K : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
V : Type u_8
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : AddCommMonoid M₃
inst✝³ : Module R M
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R M₃
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
Q₃ : QuadraticForm R M₃
f : IsometryEquiv Q₁ Q₂
g : IsometryEquiv Q₂ Q₃
src✝ : M₁ ≃ₗ[R] M₃ := LinearEquiv.trans f.toLinearEquiv g.toLinearEquiv
m : M₁
⊢ ↑Q₃
      (AddHom.toFun
        (↑{ toLinearMap := ↑src✝, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
              right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }).toAddHom
        m) =
    ↑Q₃ (↑g (↑f m))
[PROOFSTEP]
rfl
[GOAL]
ι : Type u_1
R : Type u_2
K : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
V : Type u_8
inst✝⁹ : Semiring R
inst✝⁸ : AddCommMonoid M
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : AddCommMonoid M₃
inst✝⁴ : Module R M
inst✝³ : Module R M₁
inst✝² : Module R M₂
inst✝¹ : Module R M₃
inst✝ : Fintype ι
v : Basis ι R M
Q : QuadraticForm R M
f : M₁ ≃ₗ[R] M
src✝ : M ≃ₗ[R] M₁ := LinearEquiv.symm f
⊢ ∀ (m : M),
    ↑(comp Q ↑f)
        (AddHom.toFun
          (↑{ toLinearMap := ↑src✝, invFun := src✝.invFun,
                left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
                right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }).toAddHom
          m) =
      ↑Q m
[PROOFSTEP]
intro
[GOAL]
ι : Type u_1
R : Type u_2
K : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
V : Type u_8
inst✝⁹ : Semiring R
inst✝⁸ : AddCommMonoid M
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : AddCommMonoid M₃
inst✝⁴ : Module R M
inst✝³ : Module R M₁
inst✝² : Module R M₂
inst✝¹ : Module R M₃
inst✝ : Fintype ι
v : Basis ι R M
Q : QuadraticForm R M
f : M₁ ≃ₗ[R] M
src✝ : M ≃ₗ[R] M₁ := LinearEquiv.symm f
m✝ : M
⊢ ↑(comp Q ↑f)
      (AddHom.toFun
        (↑{ toLinearMap := ↑src✝, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
              right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }).toAddHom
        m✝) =
    ↑Q m✝
[PROOFSTEP]
simp only [comp_apply, LinearEquiv.coe_coe, LinearEquiv.toFun_eq_coe, LinearEquiv.apply_symm_apply, f.apply_symm_apply]
[GOAL]
ι : Type u_1
R : Type u_2
K : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
V : Type u_8
inst✝¹³ : Semiring R
inst✝¹² : AddCommMonoid M
inst✝¹¹ : AddCommMonoid M₁
inst✝¹⁰ : AddCommMonoid M₂
inst✝⁹ : AddCommMonoid M₃
inst✝⁸ : Module R M
inst✝⁷ : Module R M₁
inst✝⁶ : Module R M₂
inst✝⁵ : Module R M₃
inst✝⁴ : Fintype ι
v✝ : Basis ι R M
inst✝³ : Field K
inst✝² : Invertible 2
inst✝¹ : AddCommGroup V
inst✝ : Module K V
Q : QuadraticForm K V
v : Basis (Fin (FiniteDimensional.finrank K V)) K V
hv₁ : BilinForm.iIsOrtho (↑associated Q) ↑v
⊢ IsometryEquiv Q (weightedSumSquares K fun i => ↑Q (↑v i))
[PROOFSTEP]
let iso := Q.isometryEquivBasisRepr v
[GOAL]
ι : Type u_1
R : Type u_2
K : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
V : Type u_8
inst✝¹³ : Semiring R
inst✝¹² : AddCommMonoid M
inst✝¹¹ : AddCommMonoid M₁
inst✝¹⁰ : AddCommMonoid M₂
inst✝⁹ : AddCommMonoid M₃
inst✝⁸ : Module R M
inst✝⁷ : Module R M₁
inst✝⁶ : Module R M₂
inst✝⁵ : Module R M₃
inst✝⁴ : Fintype ι
v✝ : Basis ι R M
inst✝³ : Field K
inst✝² : Invertible 2
inst✝¹ : AddCommGroup V
inst✝ : Module K V
Q : QuadraticForm K V
v : Basis (Fin (FiniteDimensional.finrank K V)) K V
hv₁ : BilinForm.iIsOrtho (↑associated Q) ↑v
iso : IsometryEquiv Q (basisRepr Q v) := isometryEquivBasisRepr Q v
⊢ IsometryEquiv Q (weightedSumSquares K fun i => ↑Q (↑v i))
[PROOFSTEP]
refine' ⟨iso, fun m => _⟩
[GOAL]
ι : Type u_1
R : Type u_2
K : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
V : Type u_8
inst✝¹³ : Semiring R
inst✝¹² : AddCommMonoid M
inst✝¹¹ : AddCommMonoid M₁
inst✝¹⁰ : AddCommMonoid M₂
inst✝⁹ : AddCommMonoid M₃
inst✝⁸ : Module R M
inst✝⁷ : Module R M₁
inst✝⁶ : Module R M₂
inst✝⁵ : Module R M₃
inst✝⁴ : Fintype ι
v✝ : Basis ι R M
inst✝³ : Field K
inst✝² : Invertible 2
inst✝¹ : AddCommGroup V
inst✝ : Module K V
Q : QuadraticForm K V
v : Basis (Fin (FiniteDimensional.finrank K V)) K V
hv₁ : BilinForm.iIsOrtho (↑associated Q) ↑v
iso : IsometryEquiv Q (basisRepr Q v) := isometryEquivBasisRepr Q v
m : V
⊢ ↑(weightedSumSquares K fun i => ↑Q (↑v i)) (AddHom.toFun iso.toAddHom m) = ↑Q m
[PROOFSTEP]
convert iso.map_app m
[GOAL]
case h.e'_2.h.e'_5
ι : Type u_1
R : Type u_2
K : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
V : Type u_8
inst✝¹³ : Semiring R
inst✝¹² : AddCommMonoid M
inst✝¹¹ : AddCommMonoid M₁
inst✝¹⁰ : AddCommMonoid M₂
inst✝⁹ : AddCommMonoid M₃
inst✝⁸ : Module R M
inst✝⁷ : Module R M₁
inst✝⁶ : Module R M₂
inst✝⁵ : Module R M₃
inst✝⁴ : Fintype ι
v✝ : Basis ι R M
inst✝³ : Field K
inst✝² : Invertible 2
inst✝¹ : AddCommGroup V
inst✝ : Module K V
Q : QuadraticForm K V
v : Basis (Fin (FiniteDimensional.finrank K V)) K V
hv₁ : BilinForm.iIsOrtho (↑associated Q) ↑v
iso : IsometryEquiv Q (basisRepr Q v) := isometryEquivBasisRepr Q v
m : V
⊢ (weightedSumSquares K fun i => ↑Q (↑v i)) = basisRepr Q v
[PROOFSTEP]
rw [basisRepr_eq_of_iIsOrtho _ _ hv₁]
[GOAL]
ι : Type u_1
R : Type u_2
K : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
V : Type u_8
inst✝¹⁴ : Semiring R
inst✝¹³ : AddCommMonoid M
inst✝¹² : AddCommMonoid M₁
inst✝¹¹ : AddCommMonoid M₂
inst✝¹⁰ : AddCommMonoid M₃
inst✝⁹ : Module R M
inst✝⁸ : Module R M₁
inst✝⁷ : Module R M₂
inst✝⁶ : Module R M₃
inst✝⁵ : Fintype ι
v : Basis ι R M
inst✝⁴ : Field K
inst✝³ : Invertible 2
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
Q : QuadraticForm K V
hQ : Nondegenerate (↑associated Q)
⊢ ∃ w, Equivalent Q (weightedSumSquares K w)
[PROOFSTEP]
obtain ⟨v, hv₁⟩ := exists_orthogonal_basis (associated_isSymm K Q)
[GOAL]
case intro
ι : Type u_1
R : Type u_2
K : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
V : Type u_8
inst✝¹⁴ : Semiring R
inst✝¹³ : AddCommMonoid M
inst✝¹² : AddCommMonoid M₁
inst✝¹¹ : AddCommMonoid M₂
inst✝¹⁰ : AddCommMonoid M₃
inst✝⁹ : Module R M
inst✝⁸ : Module R M₁
inst✝⁷ : Module R M₂
inst✝⁶ : Module R M₃
inst✝⁵ : Fintype ι
v✝ : Basis ι R M
inst✝⁴ : Field K
inst✝³ : Invertible 2
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
Q : QuadraticForm K V
hQ : Nondegenerate (↑associated Q)
v : Basis (Fin (FiniteDimensional.finrank K V)) K V
hv₁ : iIsOrtho (↑(associatedHom K) Q) ↑v
⊢ ∃ w, Equivalent Q (weightedSumSquares K w)
[PROOFSTEP]
have hv₂ := hv₁.not_isOrtho_basis_self_of_nondegenerate hQ
[GOAL]
case intro
ι : Type u_1
R : Type u_2
K : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
V : Type u_8
inst✝¹⁴ : Semiring R
inst✝¹³ : AddCommMonoid M
inst✝¹² : AddCommMonoid M₁
inst✝¹¹ : AddCommMonoid M₂
inst✝¹⁰ : AddCommMonoid M₃
inst✝⁹ : Module R M
inst✝⁸ : Module R M₁
inst✝⁷ : Module R M₂
inst✝⁶ : Module R M₃
inst✝⁵ : Fintype ι
v✝ : Basis ι R M
inst✝⁴ : Field K
inst✝³ : Invertible 2
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
Q : QuadraticForm K V
hQ : Nondegenerate (↑associated Q)
v : Basis (Fin (FiniteDimensional.finrank K V)) K V
hv₁ : iIsOrtho (↑(associatedHom K) Q) ↑v
hv₂ : ∀ (i : Fin (FiniteDimensional.finrank K V)), ¬IsOrtho (↑(associatedHom K) Q) (↑v i) (↑v i)
⊢ ∃ w, Equivalent Q (weightedSumSquares K w)
[PROOFSTEP]
simp_rw [IsOrtho, associated_eq_self_apply] at hv₂ 
[GOAL]
case intro
ι : Type u_1
R : Type u_2
K : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
V : Type u_8
inst✝¹⁴ : Semiring R
inst✝¹³ : AddCommMonoid M
inst✝¹² : AddCommMonoid M₁
inst✝¹¹ : AddCommMonoid M₂
inst✝¹⁰ : AddCommMonoid M₃
inst✝⁹ : Module R M
inst✝⁸ : Module R M₁
inst✝⁷ : Module R M₂
inst✝⁶ : Module R M₃
inst✝⁵ : Fintype ι
v✝ : Basis ι R M
inst✝⁴ : Field K
inst✝³ : Invertible 2
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
Q : QuadraticForm K V
hQ : Nondegenerate (↑associated Q)
v : Basis (Fin (FiniteDimensional.finrank K V)) K V
hv₁ : iIsOrtho (↑(associatedHom K) Q) ↑v
hv₂ : ∀ (i : Fin (FiniteDimensional.finrank K V)), ¬↑Q (↑v i) = 0
⊢ ∃ w, Equivalent Q (weightedSumSquares K w)
[PROOFSTEP]
exact ⟨fun i => Units.mk0 _ (hv₂ i), ⟨Q.isometryEquivWeightedSumSquares v hv₁⟩⟩
