awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Radical
Goal:
R : Type u_1
M : Type u_2
P : Type u_4
inst : AddCommGroup M
inst_1 : AddCommGroup P
inst_2 : CommRing R
inst_3 : Module R M
inst_4 : Module R P
Q : QuadraticMap R M P
inst_5 : Invertible (α := R) 2
rw :
  LinearMap.IsRefl.{u_1, u_1, u_4, u_2} (R := R) (R₁ := R) (M := P) (M₁ := M) (I₁ := RingHom.id R) (I₂ := RingHom.id R)
    ((associated : (a : QuadraticMap R M P) → LinearMap.BilinMap R M P) Q)
⊢ LinearMap.Nondegenerate.{u_1, u_1, u_1, u_4, u_2, u_2} (R := R) (R₁ := R) (R₂ := R) (M := P) (M₁ := M) (M₂ := M)
      (I₁ := RingHom.id R) (I₂ := RingHom.id R) ((associated : (a : QuadraticMap R M P) → LinearMap.BilinMap R M P) Q) ↔
    Nondegenerate.{u_1, u_2, u_4} (R := R) (M := M) (P := P) (Q := Q)

Tactic:
rw [nondegenerate_iff_radical_eq_bot, radical_eq_ker_associated,
    LinearMap.IsRefl.nondegenerate_iff_separatingLeft, LinearMap.separatingLeft_iff_ker_eq_bot]

Premises used: QuadraticMap.radical_eq_ker_associated, QuadraticMap.nondegenerate_iff_radical_eq_bot, LinearMap.separatingLeft_iff_ker_eq_bot, LinearMap.IsRefl.nondegenerate_iff_separatingLeft
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Radical
Goal:
R : Type u_1
M : Type u_2
P : Type u_4
inst : AddCommGroup M
inst_1 : AddCommGroup P
inst_2 : CommRing R
inst_3 : Module R M
inst_4 : Module R P
Q : QuadraticMap R M P
inst_5 : Invertible (α := R) 2
⊢ LinearMap.IsRefl.{u_1, u_1, u_4, u_2} (R := R) (R₁ := R) (M := P) (M₁ := M) (I₁ := RingHom.id R) (I₂ := RingHom.id R)
    ((associated : (a : QuadraticMap R M P) → LinearMap.BilinMap R M P) Q)

Tactic:
fun x y ↦ (congr_arg (· x y) (associated_flip R Q)).trans

Premises used: LinearMap.IsRefl
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Radical
Goal:
R : Type u_1
M : Type u_2
P : Type u_4
inst : AddCommGroup M
inst_1 : AddCommGroup P
inst_2 : CommRing R
inst_3 : Module R M
inst_4 : Module R P
Q : QuadraticMap R M P
inst_5 : Invertible (α := R) 2
⊢ LinearMap.IsRefl.{u_1, u_1, u_4, u_2} (R := R) (R₁ := R) (M := P) (M₁ := M) (I₁ := RingHom.id R) (I₂ := RingHom.id R)
    ((associated : (a : QuadraticMap R M P) → LinearMap.BilinMap R M P) Q)

Tactic:
exact fun x y ↦ (congr_arg (· x y) (associated_flip R Q)).trans

Premises used: congr_arg, QuadraticMap.associated_flip, Eq.trans
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Radical
Goal:
R : Type u_1
M : Type u_2
P : Type u_4
inst : AddCommGroup M
inst_1 : AddCommGroup P
inst_2 : CommRing R
inst_3 : Module R M
inst_4 : Module R P
Q : QuadraticMap R M P
inst_5 : Invertible (α := R) 2
rw : LinearMap.IsRefl Q.polarBilin
⊢ LinearMap.Nondegenerate Q.polarBilin ↔ Nondegenerate.{u_1, u_2, u_4} (R := R) (M := M) (P := P) (Q := Q)

Tactic:
rw [nondegenerate_iff_radical_eq_bot, radical_eq_ker_polarBilin,
    LinearMap.IsRefl.nondegenerate_iff_separatingLeft, LinearMap.separatingLeft_iff_ker_eq_bot]

Premises used: QuadraticMap.radical_eq_ker_polarBilin, QuadraticMap.nondegenerate_iff_radical_eq_bot, LinearMap.separatingLeft_iff_ker_eq_bot, LinearMap.IsRefl.nondegenerate_iff_separatingLeft
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Radical
Goal:
R : Type u_1
M : Type u_2
P : Type u_4
inst : AddCommGroup M
inst_1 : AddCommGroup P
inst_2 : CommRing R
inst_3 : Module R M
inst_4 : Module R P
Q : QuadraticMap R M P
inst_5 : Invertible (α := R) 2
⊢ LinearMap.IsRefl Q.polarBilin

Tactic:
fun x y ↦ (polar_comm Q y x).trans

Premises used: QuadraticMap.polar_comm, LinearMap.IsRefl, QuadraticMap.polar, DFunLike.coe, Eq.trans
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Radical
Goal:
R : Type u_1
M : Type u_2
P : Type u_4
inst : AddCommGroup M
inst_1 : AddCommGroup P
inst_2 : CommRing R
inst_3 : Module R M
inst_4 : Module R P
Q : QuadraticMap R M P
inst_5 : Invertible (α := R) 2
⊢ LinearMap.IsRefl Q.polarBilin

Tactic:
exact fun x y ↦ (polar_comm Q y x).trans

Premises used: QuadraticMap.polar_comm, DFunLike.coe, Eq.trans
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Radical
Goal:
𝕜 : Type u_1
ι : Type u_2
inst : Field 𝕜
inst_1 : NeZero.{u_1} (R := 𝕜) 2
inst_2 : Fintype ι
w : ι → 𝕜
h :
  ∀ (v : ι → 𝕜),
    Membership.mem (γ := Submodule 𝕜 (ι → 𝕜))
        (radical (R := 𝕜) (M := ι → 𝕜) (P := 𝕜) (weightedSumSquares 𝕜 w) : Submodule 𝕜 (ι → 𝕜)) v ↔
      Membership.mem (γ := Submodule 𝕜 (ι → 𝕜)) (Pi.spanSubset 𝕜 {i : ι | w i = 0}) v
⊢ Eq (α := Submodule 𝕜 (ι → 𝕜)) (radical (R := 𝕜) (M := ι → 𝕜) (P := 𝕜) (weightedSumSquares 𝕜 w) : Submodule 𝕜 (ι → 𝕜))
    (Pi.spanSubset 𝕜 {i : ι | w i = 0} : Submodule 𝕜 (ι → 𝕜))

Tactic:
ext v
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Radical
Goal:
𝕜 : Type u_1
ι : Type u_2
inst : Field 𝕜
inst_1 : NeZero.{u_1} (R := 𝕜) 2
inst_2 : Fintype ι
w v : ι → 𝕜
h :
  (Eq.{u_1 + 1} (α := 𝕜) (∑ x : ι, w x * HPow.hPow (β := ℕ) (v x) 2) 0 ∧
      ∀ (n : ι → 𝕜),
        HAdd.hAdd (α := 𝕜) (∑ x : ι, w x * HPow.hPow (β := ℕ) (v x) 2) (∑ x : ι, w x * (2 * v x * n x)) = 0) ↔
    ∀ i ∉ {i : ι | w i = 0}, v i = 0
⊢ Membership.mem (γ := Submodule 𝕜 (ι → 𝕜))
      (radical (R := 𝕜) (M := ι → 𝕜) (P := 𝕜) (weightedSumSquares 𝕜 w) : Submodule 𝕜 (ι → 𝕜)) v ↔
    Membership.mem (γ := Submodule 𝕜 (ι → 𝕜)) (Pi.spanSubset 𝕜 {i : ι | w i = 0}) v

Tactic:
simp only [mem_radical_iff', weightedSumSquares_apply, ← pow_two, smul_eq_mul, Pi.add_apply,
    add_sq, mul_add, sum_add_distrib, add_eq_right, Pi.mem_spanSubset_iff]

Premises used: pow_two, add_sq, Finset.sum_add_distrib, Pi.mem_spanSubset_iff, Pi.add_apply, QuadraticMap.weightedSumSquares_apply, add_eq_right, mul_add, smul_eq_mul, QuadraticMap.mem_radical_iff'
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Radical
Goal:
𝕜 : Type u_1
ι : Type u_2
inst : Field 𝕜
inst_1 : NeZero.{u_1} (R := 𝕜) 2
inst_2 : Fintype ι
w v : ι → 𝕜
h :
  (Eq.{u_1 + 1} (α := 𝕜) (∑ x : ι, w x * HPow.hPow (β := ℕ) (v x) 2) 0 ∧
      ∀ (n : ι → 𝕜),
        HAdd.hAdd (α := 𝕜) (∑ x : ι, w x * HPow.hPow (β := ℕ) (v x) 2) (∑ x : ι, w x * (2 * v x * n x)) = 0) →
    ∀ i ∉ {i : ι | w i = 0}, v i = 0
h₁ :
  (∀ i ∉ {i : ι | w i = 0}, v i = 0) →
    Eq.{u_1 + 1} (α := 𝕜) (∑ x : ι, w x * HPow.hPow (β := ℕ) (v x) 2) 0 ∧
      ∀ (n : ι → 𝕜), HAdd.hAdd (α := 𝕜) (∑ x : ι, w x * HPow.hPow (β := ℕ) (v x) 2) (∑ x : ι, w x * (2 * v x * n x)) = 0
⊢ (Eq.{u_1 + 1} (α := 𝕜) (∑ x : ι, w x * HPow.hPow (β := ℕ) (v x) 2) 0 ∧
      ∀ (n : ι → 𝕜),
        HAdd.hAdd (α := 𝕜) (∑ x : ι, w x * HPow.hPow (β := ℕ) (v x) 2) (∑ x : ι, w x * (2 * v x * n x)) = 0) ↔
    ∀ i ∉ {i : ι | w i = 0}, v i = 0

Tactic:
constructor
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Radical
Goal:
𝕜 : Type u_1
ι : Type u_2
inst : Field 𝕜
inst_1 : NeZero.{u_1} (R := 𝕜) 2
inst_2 : Fintype ι
w v : ι → 𝕜
hv : Eq.{u_1 + 1} (α := 𝕜) (∑ x : ι, w x * HPow.hPow (β := ℕ) (v x) 2) 0
hvv' :
  ∀ (n : ι → 𝕜), HAdd.hAdd (α := 𝕜) (∑ x : ι, w x * HPow.hPow (β := ℕ) (v x) 2) (∑ x : ι, w x * (2 * v x * n x)) = 0
i : ι
⊢ i ∉ {i : ι | w i = 0} → v i = 0

Tactic:
simpa [hv, Pi.single_apply, NeZero.ne, or_iff_not_imp_left] using hvv' (Pi.single i 1)

Premises used: Pi.single_apply, Pi.single, Classical.or_iff_not_imp_left, OfNat.ofNat, NeZero.ne
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Radical
Goal:
𝕜 : Type u_1
ι : Type u_2
inst : Field 𝕜
inst_1 : NeZero.{u_1} (R := 𝕜) 2
inst_2 : Fintype ι
w v : ι → 𝕜
h : ∀ i ∉ {i : ι | w i = 0}, v i = 0
⊢ ∀ (x : ι), Membership.mem (γ := Finset ι) univ x → w x * HPow.hPow (β := ℕ) (v x) 2 = 0

Tactic:
grind
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Radical
Goal:
𝕜 : Type u_1
ι : Type u_2
inst : Field 𝕜
inst_1 : NeZero.{u_1} (R := 𝕜) 2
inst_2 : Fintype ι
w v_1 : ι → 𝕜
h : ∀ i ∉ {i : ι | w i = 0}, v_1 i = 0
v : ι → 𝕜
⊢ ∀ (x : ι), Membership.mem (γ := Finset ι) univ x → w x * HPow.hPow (β := ℕ) (v_1 x) 2 + w x * (2 * v_1 x * v x) = 0

Tactic:
grind
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Radical
Goal:
𝕜 : Type u_1
ι : Type u_2
inst : Field 𝕜
inst_1 : NeZero.{u_1} (R := 𝕜) 2
inst_2 : Fintype ι
w v : ι → 𝕜
⊢ (∀ i ∉ {i : ι | w i = 0}, v i = 0) →
    Eq.{u_1 + 1} (α := 𝕜) (∑ x : ι, w x * HPow.hPow (β := ℕ) (v x) 2) 0 ∧
      ∀ (n : ι → 𝕜), HAdd.hAdd (α := 𝕜) (∑ x : ι, w x * HPow.hPow (β := ℕ) (v x) 2) (∑ x : ι, w x * (2 * v x * n x)) = 0

Tactic:
simpa only [← sum_add_distrib]
      using fun h ↦ ⟨sum_eq_zero (by grind), fun v ↦ sum_eq_zero (by grind)⟩

Premises used: Finset.sum_add_distrib
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Radical
Goal:
𝕜 : Type u_1
ι : Type u_2
inst : Field 𝕜
inst_1 : NeZero.{u_1} (R := 𝕜) 2
inst_2 : Fintype ι
w : ι → 𝕜
h :
  ∀ (v : ι → 𝕜),
    Membership.mem (γ := Submodule 𝕜 (ι → 𝕜))
        (radical (R := 𝕜) (M := ι → 𝕜) (P := 𝕜) (weightedSumSquares 𝕜 w) : Submodule 𝕜 (ι → 𝕜)) v ↔
      Membership.mem (γ := Submodule 𝕜 (ι → 𝕜)) (Pi.spanSubset 𝕜 {i : ι | w i = 0}) v
h₁ :
  ∀ (v : ι → 𝕜),
    (Eq.{u_1 + 1} (α := 𝕜) (∑ x : ι, w x * HPow.hPow (β := ℕ) (v x) 2) 0 ∧
        ∀ (n : ι → 𝕜),
          HAdd.hAdd (α := 𝕜) (∑ x : ι, w x * HPow.hPow (β := ℕ) (v x) 2) (∑ x : ι, w x * (2 * v x * n x)) = 0) ↔
      ∀ i ∉ {i : ι | w i = 0}, v i = 0
h₂ :
  ∀ (v : ι → 𝕜),
    (Eq.{u_1 + 1} (α := 𝕜) (∑ x : ι, w x * HPow.hPow (β := ℕ) (v x) 2) 0 ∧
        ∀ (n : ι → 𝕜),
          HAdd.hAdd (α := 𝕜) (∑ x : ι, w x * HPow.hPow (β := ℕ) (v x) 2) (∑ x : ι, w x * (2 * v x * n x)) = 0) →
      ∀ i ∉ {i : ι | w i = 0}, v i = 0
h₃ h₄ :
  ∀ (v : ι → 𝕜),
    (∀ i ∉ {i : ι | w i = 0}, v i = 0) →
      Eq.{u_1 + 1} (α := 𝕜) (∑ x : ι, w x * HPow.hPow (β := ℕ) (v x) 2) 0 ∧
        ∀ (n : ι → 𝕜),
          HAdd.hAdd (α := 𝕜) (∑ x : ι, w x * HPow.hPow (β := ℕ) (v x) 2) (∑ x : ι, w x * (2 * v x * n x)) = 0
⊢ Eq (α := Submodule 𝕜 (ι → 𝕜)) (radical (R := 𝕜) (M := ι → 𝕜) (P := 𝕜) (weightedSumSquares 𝕜 w) : Submodule 𝕜 (ι → 𝕜))
    (Pi.spanSubset 𝕜 {i : ι | w i = 0} : Submodule 𝕜 (ι → 𝕜))

Tactic:
classical
  ext v
  simp only [mem_radical_iff', weightedSumSquares_apply, ← pow_two, smul_eq_mul, Pi.add_apply,
    add_sq, mul_add, sum_add_distrib, add_eq_right, Pi.mem_spanSubset_iff]
  constructor
  · rintro ⟨hv, hvv'⟩ i
    simpa [hv, Pi.single_apply, NeZero.ne, or_iff_not_imp_left] using hvv' (Pi.single i 1)
  · simpa only [← sum_add_distrib]
      using fun h ↦ ⟨sum_eq_zero (by grind), fun v ↦ sum_eq_zero (by grind)⟩

Premises used: pow_two, add_sq, Finset.sum_add_distrib, Pi.single_apply, Pi.mem_spanSubset_iff, Pi.add_apply, QuadraticMap.weightedSumSquares_apply, Classical.or_iff_not_imp_left, add_eq_right, mul_add, smul_eq_mul, QuadraticMap.mem_radical_iff', NeZero.ne
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Radical
Goal:
𝕜 : Type u_1
ι : Type u_2
inst : Field 𝕜
inst_1 : NeZero.{u_1} (R := 𝕜) 2
inst_2 : Fintype ι
w : ι → 𝕜
M : Type u_3
inst_3 : AddCommGroup M
inst_4 : Module 𝕜 M
Q : QuadraticForm 𝕜 M
hQ : Equivalent Q (weightedSumSquares 𝕜 w)
rw :
  Module.finrank 𝕜 ↥(radical (R := 𝕜) (M := ι → 𝕜) (P := 𝕜) (weightedSumSquares 𝕜 w) : Submodule 𝕜 (ι → 𝕜)) =
    Set.ncard.{u_2} (α := ι) {i : ι | w i = 0}
rw₁ : Module.finrank 𝕜 ↥(Pi.spanSubset 𝕜 {i : ι | w i = 0}) = Set.ncard.{u_2} (α := ι) {i : ι | w i = 0}
rw₂ rw₃ : Set.ncard.{u_2} (α := ι) {i : ι | w i = 0} = Set.ncard.{u_2} (α := ι) {i : ι | w i = 0}
⊢ Module.finrank.{u_1, u_3} 𝕜 ↥(radical (P := 𝕜) Q) = Set.ncard.{u_2} (α := ι) {i : ι | w i = 0}

Tactic:
rw [hQ.rank_radical_eq, radical_weightedSumSquares, Pi.dim_spanSubset]

Premises used: QuadraticMap.Equivalent.rank_radical_eq, Pi.dim_spanSubset, QuadraticForm.radical_weightedSumSquares
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Real
Goal:
ι : Type u_1
inst : Fintype ι
w : ι → ℝ
u : (i : ι) → ℝˣ := fun (i : ι) ↦ if h : w i = 0 then 1 else Units.mk0 (w i) h
i : ι
this : (↑(u i) : ℝ) ≠ 0
⊢ 1 / √|(↑(u i) : ℝ)| ≠ 0

Tactic:
positivity
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Real
Goal:
ι : Type u_1
inst : Fintype ι
w : ι → ℝ
u : (i : ι) → ℝˣ := fun (i : ι) ↦ if h : w i = 0 then 1 else Units.mk0 (w i) h
⊢ ∀ (i : ι), 1 / √|(↑(u i) : ℝ)| ≠ 0

Tactic:
have hu : ∀ i : ι, 1 / √|(u i : ℝ)| ≠ 0 := fun i ↦
    have : (u i : ℝ) ≠ 0 := (u i).ne_zero
    by positivity
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Real
Goal:
ι : Type u_1
inst : Fintype ι
w : ι → ℝ
u : (i : ι) → ℝˣ := fun (i : ι) ↦ if h : w i = 0 then 1 else Units.mk0 (w i) h
hu : ∀ (i : ι), 1 / √|(↑(u i) : ℝ)| ≠ 0
i : ι
pos : ∀ (hi : w i = 0), w i / |(↑(u i) : ℝ)| = (↑((sign : (a : ℝ) → SignType) (w i)) : ℝ)
neg : ∀ (hi : ¬w i = 0), w i / |(↑(u i) : ℝ)| = (↑((sign : (a : ℝ) → SignType) (w i)) : ℝ)
⊢ w i / |(↑(u i) : ℝ)| = (↑((sign : (a : ℝ) → SignType) (w i)) : ℝ)

Tactic:
by_cases hi : w i = 0
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Real
Goal:
ι : Type u_1
inst : Fintype ι
w : ι → ℝ
u : (i : ι) → ℝˣ := fun (i : ι) ↦ if h : w i = 0 then 1 else Units.mk0 (w i) h
hu : ∀ (i : ι), 1 / √|(↑(u i) : ℝ)| ≠ 0
i : ι
hi : w i = 0
⊢ w i / |(↑(u i) : ℝ)| = (↑((sign : (a : ℝ) → SignType) (w i)) : ℝ)

Tactic:
simp [hi]
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Real
Goal:
ι : Type u_1
inst : Fintype ι
w : ι → ℝ
u : (i : ι) → ℝˣ := fun (i : ι) ↦ if h : w i = 0 then 1 else Units.mk0 (w i) h
hu : ∀ (i : ι), 1 / √|(↑(u i) : ℝ)| ≠ 0
i : ι
hi : ¬w i = 0
neg : w i / |w i| = (↑((sign : (a : ℝ) → SignType) (w i)) : ℝ)
⊢ w i / |(↑(u i) : ℝ)| = (↑((sign : (a : ℝ) → SignType) (w i)) : ℝ)

Tactic:
simp only [hi, ↓reduceDIte, Units.val_mk0, u]

Premises used: reduceDIte, Units.val_mk0
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Real
Goal:
ι : Type u_1
inst : Fintype ι
w : ι → ℝ
u : (i : ι) → ℝˣ := fun (i : ι) ↦ if h : w i = 0 then 1 else Units.mk0 (w i) h
hu : ∀ (i : ι), 1 / √|(↑(u i) : ℝ)| ≠ 0
i : ι
hi : ¬w i = 0
neg : w i = |w i| * (↑((sign : (a : ℝ) → SignType) (w i)) : ℝ)
⊢ w i / |w i| = (↑((sign : (a : ℝ) → SignType) (w i)) : ℝ)

Tactic:
field_simp
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Real
Goal:
ι : Type u_1
inst : Fintype ι
w : ι → ℝ
u : (i : ι) → ℝˣ := fun (i : ι) ↦ if h : w i = 0 then 1 else Units.mk0 (w i) h
hu : ∀ (i : ι), 1 / √|(↑(u i) : ℝ)| ≠ 0
i : ι
hi : ¬w i = 0
⊢ w i = |w i| * (↑((sign : (a : ℝ) → SignType) (w i)) : ℝ)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Real
Goal:
ι : Type u_1
inst : Fintype ι
w : ι → ℝ
u : (i : ι) → ℝˣ := fun (i : ι) ↦ if h : w i = 0 then 1 else Units.mk0 (w i) h
hu : ∀ (i : ι), 1 / √|(↑(u i) : ℝ)| ≠ 0
⊢ ∀ (i : ι), w i / |(↑(u i) : ℝ)| = (↑((sign : (a : ℝ) → SignType) (w i)) : ℝ)

Tactic:
have hwu : ∀ i, w i / |(u i : ℝ)| = sign (w i) := fun i ↦ by
    by_cases hi : w i = 0
    · simp [hi]
    · simp only [hi, ↓reduceDIte, Units.val_mk0, u]; field_simp; simp
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Real
Goal:
ι : Type u_1
inst : Fintype ι
w : ι → ℝ
u : (i : ι) → ℝˣ := fun (i : ι) ↦ if h : w i = 0 then 1 else Units.mk0 (w i) h
hu : ∀ (i : ι), 1 / √|(↑(u i) : ℝ)| ≠ 0
hwu : ∀ (i : ι), w i / |(↑(u i) : ℝ)| = (↑((sign : (a : ℝ) → SignType) (w i)) : ℝ)
h :
  (weightedSumSquares (S := ℝ) ℝ fun (i : ι) ↦ (↑((sign : (a : ℝ) → SignType) (w i)) : ℝ)) =
    basisRepr (weightedSumSquares ℝ w)
      (Basis.unitsSMul (Pi.basisFun ℝ ι) fun (i : ι) ↦ Units.mk0 (1 / √|(↑(u i) : ℝ)|) ⋯)
⊢ QuadraticMap.IsometryEquiv (M₂ := ι → ℝ) (weightedSumSquares ℝ w)
    (weightedSumSquares (S := ℝ) ℝ fun (i : ι) ↦ (↑((sign : (a : ℝ) → SignType) (w i)) : ℝ))

Tactic:
convert!
    QuadraticMap.isometryEquivBasisRepr (weightedSumSquares ℝ w)
      ((Pi.basisFun ℝ ι).unitsSMul fun i => .mk0 _ (hu i))

Premises used: Units.val, Real, QuadraticMap.isometryEquivBasisRepr, abs, Module.Basis.unitsSMul, HDiv.hDiv, Units.mk0, QuadraticMap.weightedSumSquares, Real.sqrt, Pi.basisFun, OfNat.ofNat
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Real
Goal:
ι : Type u_1
inst : Fintype ι
w : ι → ℝ
u : (i : ι) → ℝˣ := fun (i : ι) ↦ if h : w i = 0 then 1 else Units.mk0 (w i) h
hu : ∀ (i : ι), 1 / √|(↑(u i) : ℝ)| ≠ 0
hwu : ∀ (i : ι), w i / |(↑(u i) : ℝ)| = (↑((sign : (a : ℝ) → SignType) (w i)) : ℝ)
h :
  ∀ (v : ι → ℝ),
    Eq (α := ℝ)
      ((weightedSumSquares (S := ℝ) ℝ fun (i : ι) ↦ (↑((sign : (a : ℝ) → SignType) (w i)) : ℝ) : (a : ι → ℝ) → ℝ) v : ℝ)
      ((basisRepr (weightedSumSquares ℝ w)
              (Basis.unitsSMul (Pi.basisFun ℝ ι) fun (i : ι) ↦ Units.mk0 (1 / √|(↑(u i) : ℝ)|) ⋯) :
            (a : ι → ℝ) → ℝ)
          v :
        ℝ)
⊢ (weightedSumSquares (S := ℝ) ℝ fun (i : ι) ↦ (↑((sign : (a : ℝ) → SignType) (w i)) : ℝ)) =
    basisRepr (weightedSumSquares ℝ w)
      (Basis.unitsSMul (Pi.basisFun ℝ ι) fun (i : ι) ↦ Units.mk0 (1 / √|(↑(u i) : ℝ)|) ⋯)

Tactic:
ext1 v
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Real
Goal:
ι : Type u_1
inst : Fintype ι
w : ι → ℝ
u : (i : ι) → ℝˣ := fun (i : ι) ↦ if h : w i = 0 then 1 else Units.mk0 (w i) h
hu : ∀ (i : ι), 1 / √|(↑(u i) : ℝ)| ≠ 0
hwu : ∀ (i : ι), w i / |(↑(u i) : ℝ)| = (↑((sign : (a : ℝ) → SignType) (w i)) : ℝ)
v : ι → ℝ
this :
  Eq (α := ℝ) (∑ i : ι, w i / |(↑(u i) : ℝ)| * HPow.hPow (β := ℕ) (v i) 2)
    (∑ i : ι, w i * (HPow.hPow (β := ℕ) (v i) 2 * |(↑(u i) : ℝ)|⁻¹))
⊢ Eq (α := ℝ)
    ((weightedSumSquares (S := ℝ) ℝ fun (i : ι) ↦ (↑((sign : (a : ℝ) → SignType) (w i)) : ℝ) : (a : ι → ℝ) → ℝ) v : ℝ)
    ((basisRepr (weightedSumSquares ℝ w)
            (Basis.unitsSMul (Pi.basisFun ℝ ι) fun (i : ι) ↦ Units.mk0 (1 / √|(↑(u i) : ℝ)|) ⋯) :
          (a : ι → ℝ) → ℝ)
        v :
      ℝ)

Tactic:
simpa [basisRepr_apply, Basis.unitsSMul_apply, ← _root_.sq, mul_pow, ← hwu, Pi.single_apply]

Premises used: Pi.single_apply, sq, mul_pow, Module.Basis.unitsSMul_apply, QuadraticMap.basisRepr_apply
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Real
Goal:
ι : Type u_1
inst : Fintype ι
w : ι → ℝ
u : (i : ι) → ℝˣ := fun (i : ι) ↦ if h : w i = 0 then 1 else Units.mk0 (w i) h
hu : ∀ (i : ι), 1 / √|(↑(u i) : ℝ)| ≠ 0
hwu : ∀ (i : ι), w i / |(↑(u i) : ℝ)| = (↑((sign : (a : ℝ) → SignType) (w i)) : ℝ)
v : ι → ℝ
h :
  Eq (α := ℝ) (∑ i : ι, w i / |(↑(u i) : ℝ)| * HPow.hPow (β := ℕ) (v i) 2)
    (∑ i : ι, w i * (HPow.hPow (β := ℕ) (v i) 2 * |(↑(u i) : ℝ)|⁻¹))
⊢ Eq (α := ℝ)
    ((weightedSumSquares (S := ℝ) ℝ fun (i : ι) ↦ (↑((sign : (a : ℝ) → SignType) (w i)) : ℝ) : (a : ι → ℝ) → ℝ) v : ℝ)
    ((basisRepr (weightedSumSquares ℝ w)
            (Basis.unitsSMul (Pi.basisFun ℝ ι) fun (i : ι) ↦ Units.mk0 (1 / √|(↑(u i) : ℝ)|) ⋯) :
          (a : ι → ℝ) → ℝ)
        v :
      ℝ)

Tactic:
suffices ∑ i, (w i / |(u i : ℝ)|) * v i ^ 2 = ∑ i, w i * (v i ^ 2 * |(u i : ℝ)|⁻¹) by
    simpa [basisRepr_apply, Basis.unitsSMul_apply, ← _root_.sq, mul_pow, ← hwu, Pi.single_apply]
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Real
Goal:
ι : Type u_1
inst : Fintype ι
w : ι → ℝ
u : (i : ι) → ℝˣ := fun (i : ι) ↦ if h : w i = 0 then 1 else Units.mk0 (w i) h
hu : ∀ (i : ι), 1 / √|(↑(u i) : ℝ)| ≠ 0
hwu : ∀ (i : ι), w i / |(↑(u i) : ℝ)| = (↑((sign : (a : ℝ) → SignType) (w i)) : ℝ)
v : ι → ℝ
j : ι
h : Membership.mem (γ := Finset ι) univ j
⊢ w j / |(↑(u j) : ℝ)| * HPow.hPow (β := ℕ) (v j) 2 = w j * (HPow.hPow (β := ℕ) (v j) 2 * |(↑(u j) : ℝ)|⁻¹)

Tactic:
ring
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Real
Goal:
ι : Type u_1
inst : Fintype ι
w : ι → ℝ
u : (i : ι) → ℝˣ := fun (i : ι) ↦ if h : w i = 0 then 1 else Units.mk0 (w i) h
hu : ∀ (i : ι), 1 / √|(↑(u i) : ℝ)| ≠ 0
hwu : ∀ (i : ι), w i / |(↑(u i) : ℝ)| = (↑((sign : (a : ℝ) → SignType) (w i)) : ℝ)
v : ι → ℝ
⊢ Eq (α := ℝ) (∑ i : ι, w i / |(↑(u i) : ℝ)| * HPow.hPow (β := ℕ) (v i) 2)
    (∑ i : ι, w i * (HPow.hPow (β := ℕ) (v i) 2 * |(↑(u i) : ℝ)|⁻¹))

Tactic:
exact sum_congr rfl fun j _ ↦ by ring

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Real
Goal:
ι : Type u_1
inst : Fintype ι
w : ι → ℝ
u : (i : ι) → ℝˣ := fun (i : ι) ↦ if h : w i = 0 then 1 else Units.mk0 (w i) h
hu : ∀ (i : ι), 1 / √|(↑(u i) : ℝ)| ≠ 0
hwu : ∀ (i : ι), w i / |(↑(u i) : ℝ)| = (↑((sign : (a : ℝ) → SignType) (w i)) : ℝ)
v : ι → ℝ
h h₁ h₂ :
  Eq (α := ℝ) (∑ i : ι, w i / |(↑(u i) : ℝ)| * HPow.hPow (β := ℕ) (v i) 2)
    (∑ i : ι, w i * (HPow.hPow (β := ℕ) (v i) 2 * |(↑(u i) : ℝ)|⁻¹))
⊢ Eq (α := ℝ)
    ((weightedSumSquares (S := ℝ) ℝ fun (i : ι) ↦ (↑((sign : (a : ℝ) → SignType) (w i)) : ℝ) : (a : ι → ℝ) → ℝ) v : ℝ)
    ((basisRepr (weightedSumSquares ℝ w)
            (Basis.unitsSMul (Pi.basisFun ℝ ι) fun (i : ι) ↦ Units.mk0 (1 / √|(↑(u i) : ℝ)|) ⋯) :
          (a : ι → ℝ) → ℝ)
        v :
      ℝ)

Tactic:
classical
  suffices ∑ i, (w i / |(u i : ℝ)|) * v i ^ 2 = ∑ i, w i * (v i ^ 2 * |(u i : ℝ)|⁻¹) by
    simpa [basisRepr_apply, Basis.unitsSMul_apply, ← _root_.sq, mul_pow, ← hwu, Pi.single_apply]
  exact sum_congr rfl fun j _ ↦ by ring

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Real
Goal:
M : Type u_2
inst : AddCommGroup M
inst_1 : Module ℝ M
inst_2 : FiniteDimensional ℝ M
Q : QuadraticForm ℝ M
hQ :
  LinearMap.SeparatingLeft.{0, 0, 0, 0, u_2, u_2} (R := ℝ) (R₁ := ℝ) (R₂ := ℝ) (M := ℝ) (M₁ := M) (M₂ := M) (I₁ :=
    RingHom.id ℝ) (I₂ := RingHom.id ℝ) ((associated : (a : QuadraticMap ℝ M ℝ) → LinearMap.BilinMap ℝ M ℝ) Q)
⊢ ∃ (w : Fin (finrank ℝ M) → SignType),
    (∀ (i : Fin (finrank ℝ M)), w i ≠ 0) ∧
      Equivalent (M₂ := Fin (finrank ℝ M) → ℝ) Q
        (weightedSumSquares (S := ℝ) ℝ fun (i : Fin (finrank ℝ M)) ↦ (↑(w i) : ℝ))

Tactic:
let ⟨w, ⟨hw₁⟩⟩ := Q.equivalent_weightedSumSquares_units_of_nondegenerate' hQ
  ⟨sign ∘ ((↑) : ℝˣ → ℝ) ∘ w, fun i => sign_ne_zero.2 (w i).ne_zero,
    ⟨hw₁.trans (isometryEquivSignWeightedSumSquares (((↑) : ℝˣ → ℝ) ∘ w))⟩⟩

Premises used: Iff.mpr, SignType.cast, Units.val, Real, Function.comp, Exists, Units.ne_zero, _private.0.QuadraticForm.equivalent_sign_ne_zero_weighted_sum_squared.match_1, Nonempty.intro, And, QuadraticMap.weightedSumSquares, QuadraticForm.isometryEquivSignWeightedSumSquares, And.intro, Exists.intro, DFunLike.coe, SignType.sign, QuadraticMap.IsometryEquiv.trans, QuadraticMap.Equivalent, sign_ne_zero, QuadraticForm.equivalent_weightedSumSquares_units_of_nondegenerate'
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Real
Goal:
M : Type u_2
inst : AddCommGroup M
inst_1 : Module ℝ M
inst_2 : FiniteDimensional ℝ M
Q : QuadraticForm ℝ M
hQ :
  LinearMap.SeparatingLeft.{0, 0, 0, 0, u_2, u_2} (R := ℝ) (R₁ := ℝ) (R₂ := ℝ) (M := ℝ) (M₁ := M) (M₂ := M) (I₁ :=
    RingHom.id ℝ) (I₂ := RingHom.id ℝ) ((associated : (a : QuadraticMap ℝ M ℝ) → LinearMap.BilinMap ℝ M ℝ) Q)
w : Fin (finrank ℝ M) → SignType
hw₀ : ∀ (i : Fin (finrank ℝ M)), w i ≠ 0
hw :
  Equivalent (M₂ := Fin (finrank ℝ M) → ℝ) Q (weightedSumSquares (S := ℝ) ℝ fun (i : Fin (finrank ℝ M)) ↦ (↑(w i) : ℝ))
i : Fin (finrank ℝ M)
zero :
  ∀ (hi : w i = SignType.zero),
    Eq (α := ℝ) ((fun (x : Fin (finrank ℝ M)) ↦ ((↑(w x) : ℝ) : ℝ)) i) (-1) ∨
      Eq (α := ℝ) ((fun (x : Fin (finrank ℝ M)) ↦ ((↑(w x) : ℝ) : ℝ)) i) 1
neg :
  ∀ (hi : w i = SignType.neg),
    Eq (α := ℝ) ((fun (x : Fin (finrank ℝ M)) ↦ ((↑(w x) : ℝ) : ℝ)) i) (-1) ∨
      Eq (α := ℝ) ((fun (x : Fin (finrank ℝ M)) ↦ ((↑(w x) : ℝ) : ℝ)) i) 1
pos :
  ∀ (hi : w i = SignType.pos),
    Eq (α := ℝ) ((fun (x : Fin (finrank ℝ M)) ↦ ((↑(w x) : ℝ) : ℝ)) i) (-1) ∨
      Eq (α := ℝ) ((fun (x : Fin (finrank ℝ M)) ↦ ((↑(w x) : ℝ) : ℝ)) i) 1
⊢ Eq (α := ℝ) ((fun (x : Fin (finrank ℝ M)) ↦ ((↑(w x) : ℝ) : ℝ)) i) (-1) ∨
    Eq (α := ℝ) ((fun (x : Fin (finrank ℝ M)) ↦ ((↑(w x) : ℝ) : ℝ)) i) 1

Tactic:
cases hi : w i
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Real
Goal:
M : Type u_2
inst : AddCommGroup M
inst_1 : Module ℝ M
inst_2 : FiniteDimensional ℝ M
Q : QuadraticForm ℝ M
hQ :
  LinearMap.SeparatingLeft.{0, 0, 0, 0, u_2, u_2} (R := ℝ) (R₁ := ℝ) (R₂ := ℝ) (M := ℝ) (M₁ := M) (M₂ := M) (I₁ :=
    RingHom.id ℝ) (I₂ := RingHom.id ℝ) ((associated : (a : QuadraticMap ℝ M ℝ) → LinearMap.BilinMap ℝ M ℝ) Q)
w : Fin (finrank ℝ M) → SignType
hw₀ : ∀ (i : Fin (finrank ℝ M)), w i ≠ 0
hw :
  Equivalent (M₂ := Fin (finrank ℝ M) → ℝ) Q (weightedSumSquares (S := ℝ) ℝ fun (i : Fin (finrank ℝ M)) ↦ (↑(w i) : ℝ))
i : Fin (finrank ℝ M)
hi : w i = zero
⊢ Eq (α := ℝ) ((fun (x : Fin (finrank ℝ M)) ↦ ((↑(w x) : ℝ) : ℝ)) i) (-1) ∨
    Eq (α := ℝ) ((fun (x : Fin (finrank ℝ M)) ↦ ((↑(w x) : ℝ) : ℝ)) i) 1

Tactic:
simp_all