awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Radical (goal)
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
m : M
h :
  HSub.hSub (β := P) (HSub.hSub (α := P) (β := P) ((Q : (a : M) → P) (m + m) : P) ((Q : (a : M) → P) m : P))
      ((Q : (a : M) → P) m : P) =
    0
h₁ :
  ∀
    (h :
      HSub.hSub (β := P)
          (HSub.hSub (α := P) (β := P) ((Q : (a : M) → P) (HSMul.hSMul.{u_1, u_2, u_2} (α := R) 2 m) : P)
            ((Q : (a : M) → P) m : P))
          ((Q : (a : M) → P) m : P) =
        0),
    Eq.{u_4 + 1} (α := P) ((Q : (a : M) → P) m : P) (0 : P)
h₂ :
  ∀
    (h :
      HSub.hSub (β := P)
          (HSub.hSub (β := P) (HSMul.hSMul (β := P) (HMul.hMul (α := R) 2 2) ((Q : (a : M) → P) m : P))
            ((Q : (a : M) → P) m : P))
          ((Q : (a : M) → P) m : P) =
        0),
    Eq.{u_4 + 1} (α := P) ((Q : (a : M) → P) m : P) (0 : P)
h₃ :
  ∀
    (h :
      HSMul.hSMul (β := P) (HMul.hMul (α := R) 2 2) ((Q : (a : M) → P) m : P) -
          HAdd.hAdd (α := P) (β := P) ((Q : (a : M) → P) m : P) ((Q : (a : M) → P) m : P) =
        0),
    Eq.{u_4 + 1} (α := P) ((Q : (a : M) → P) m : P) (0 : P)
h₄ :
  ∀
    (h :
      HSMul.hSMul (β := P) (HMul.hMul (α := R) 2 2) ((Q : (a : M) → P) m : P) -
          HSMul.hSMul.{u_1, u_4, u_4} (α := R) (β := P) 2 ((Q : (a : M) → P) m : P) =
        0),
    Eq.{u_4 + 1} (α := P) ((Q : (a : M) → P) m : P) (0 : P)
h₅ :
  ∀
    (h :
      HSMul.hSMul.{u_1, u_4, u_4} (α := R) 2
            (HSMul.hSMul.{u_1, u_4, u_4} (α := R) (β := P) 2 ((Q : (a : M) → P) m : P)) -
          HSMul.hSMul.{u_1, u_4, u_4} (α := R) (β := P) 2 ((Q : (a : M) → P) m : P) =
        0),
    Eq.{u_4 + 1} (α := P) ((Q : (a : M) → P) m : P) (0 : P)
h₆ :
  ∀
    (h :
      HSMul.hSMul.{u_1, u_4, u_4} (α := R) 2
          (HSub.hSub (β := P) (HSMul.hSMul.{u_1, u_4, u_4} (α := R) (β := P) 2 ((Q : (a : M) → P) m : P))
            ((Q : (a : M) → P) m : P)) =
        0),
    Eq.{u_4 + 1} (α := P) ((Q : (a : M) → P) m : P) (0 : P)
⊢ Eq.{u_4 + 1} (α := P) ((Q : (a : M) → P) m : P) (0 : P)
have h₇ : ∀
  (h :
    HSub.hSub (β := P) (HSMul.hSMul.{u_1, u_4, u_4} (α := R) (β := P) 2 ((Q : (a : M) → P) m : P))
        ((Q : (a : M) → P) m : P) =
      0),
  Eq.{u_4 + 1} (α := P) ((Q : (a : M) → P) m : P) (0 : P)
Tactic: rwa [← two_smul R, QuadraticMap.map_smul, sub_sub, ← two_smul R, mul_smul, ← smul_sub,
    (isUnit_of_invertible 2).smul_eq_zero, two_smul, add_sub_cancel_right] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Radical (goal)
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
m : M
h :
  HSub.hSub (β := P) (HSub.hSub (α := P) (β := P) ((Q : (a : M) → P) (m + m) : P) ((Q : (a : M) → P) m : P))
      ((Q : (a : M) → P) m : P) =
    0
h₁ :
  ∀
    (h :
      HSub.hSub (β := P)
          (HSub.hSub (α := P) (β := P) ((Q : (a : M) → P) (HSMul.hSMul.{u_1, u_2, u_2} (α := R) 2 m) : P)
            ((Q : (a : M) → P) m : P))
          ((Q : (a : M) → P) m : P) =
        0),
    Eq.{u_4 + 1} (α := P) ((Q : (a : M) → P) m : P) (0 : P)
h₂ :
  ∀
    (h :
      HSub.hSub (β := P)
          (HSub.hSub (β := P) (HSMul.hSMul (β := P) (HMul.hMul (α := R) 2 2) ((Q : (a : M) → P) m : P))
            ((Q : (a : M) → P) m : P))
          ((Q : (a : M) → P) m : P) =
        0),
    Eq.{u_4 + 1} (α := P) ((Q : (a : M) → P) m : P) (0 : P)
h₃ :
  ∀
    (h :
      HSMul.hSMul (β := P) (HMul.hMul (α := R) 2 2) ((Q : (a : M) → P) m : P) -
          HAdd.hAdd (α := P) (β := P) ((Q : (a : M) → P) m : P) ((Q : (a : M) → P) m : P) =
        0),
    Eq.{u_4 + 1} (α := P) ((Q : (a : M) → P) m : P) (0 : P)
h₄ :
  ∀
    (h :
      HSMul.hSMul (β := P) (HMul.hMul (α := R) 2 2) ((Q : (a : M) → P) m : P) -
          HSMul.hSMul.{u_1, u_4, u_4} (α := R) (β := P) 2 ((Q : (a : M) → P) m : P) =
        0),
    Eq.{u_4 + 1} (α := P) ((Q : (a : M) → P) m : P) (0 : P)
h₅ :
  ∀
    (h :
      HSMul.hSMul.{u_1, u_4, u_4} (α := R) 2
            (HSMul.hSMul.{u_1, u_4, u_4} (α := R) (β := P) 2 ((Q : (a : M) → P) m : P)) -
          HSMul.hSMul.{u_1, u_4, u_4} (α := R) (β := P) 2 ((Q : (a : M) → P) m : P) =
        0),
    Eq.{u_4 + 1} (α := P) ((Q : (a : M) → P) m : P) (0 : P)
h₆ :
  ∀
    (h :
      HSMul.hSMul.{u_1, u_4, u_4} (α := R) 2
          (HSub.hSub (β := P) (HSMul.hSMul.{u_1, u_4, u_4} (α := R) (β := P) 2 ((Q : (a : M) → P) m : P))
            ((Q : (a : M) → P) m : P)) =
        0),
    Eq.{u_4 + 1} (α := P) ((Q : (a : M) → P) m : P) (0 : P)
h₇ :
  ∀
    (h :
      HSub.hSub (β := P) (HSMul.hSMul.{u_1, u_4, u_4} (α := R) (β := P) 2 ((Q : (a : M) → P) m : P))
          ((Q : (a : M) → P) m : P) =
        0),
    Eq.{u_4 + 1} (α := P) ((Q : (a : M) → P) m : P) (0 : P)
⊢ Eq.{u_4 + 1} (α := P) ((Q : (a : M) → P) m : P) (0 : P)
have h₈ : ∀
  (h :
    HSub.hSub (β := P) (HAdd.hAdd (α := P) (β := P) ((Q : (a : M) → P) m : P) ((Q : (a : M) → P) m : P))
        ((Q : (a : M) → P) m : P) =
      0),
  Eq.{u_4 + 1} (α := P) ((Q : (a : M) → P) m : P) (0 : P)
Tactic: rwa [← two_smul R, QuadraticMap.map_smul, sub_sub, ← two_smul R, mul_smul, ← smul_sub,
    (isUnit_of_invertible 2).smul_eq_zero, two_smul, add_sub_cancel_right] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Radical (goal)
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
m : M
h :
  HSub.hSub (β := P) (HSub.hSub (α := P) (β := P) ((Q : (a : M) → P) (m + m) : P) ((Q : (a : M) → P) m : P))
      ((Q : (a : M) → P) m : P) =
    0
h₁ :
  ∀
    (h :
      HSub.hSub (β := P)
          (HSub.hSub (α := P) (β := P) ((Q : (a : M) → P) (HSMul.hSMul.{u_1, u_2, u_2} (α := R) 2 m) : P)
            ((Q : (a : M) → P) m : P))
          ((Q : (a : M) → P) m : P) =
        0),
    Eq.{u_4 + 1} (α := P) ((Q : (a : M) → P) m : P) (0 : P)
h₂ :
  ∀
    (h :
      HSub.hSub (β := P)
          (HSub.hSub (β := P) (HSMul.hSMul (β := P) (HMul.hMul (α := R) 2 2) ((Q : (a : M) → P) m : P))
            ((Q : (a : M) → P) m : P))
          ((Q : (a : M) → P) m : P) =
        0),
    Eq.{u_4 + 1} (α := P) ((Q : (a : M) → P) m : P) (0 : P)
h₃ :
  ∀
    (h :
      HSMul.hSMul (β := P) (HMul.hMul (α := R) 2 2) ((Q : (a : M) → P) m : P) -
          HAdd.hAdd (α := P) (β := P) ((Q : (a : M) → P) m : P) ((Q : (a : M) → P) m : P) =
        0),
    Eq.{u_4 + 1} (α := P) ((Q : (a : M) → P) m : P) (0 : P)
h₄ :
  ∀
    (h :
      HSMul.hSMul (β := P) (HMul.hMul (α := R) 2 2) ((Q : (a : M) → P) m : P) -
          HSMul.hSMul.{u_1, u_4, u_4} (α := R) (β := P) 2 ((Q : (a : M) → P) m : P) =
        0),
    Eq.{u_4 + 1} (α := P) ((Q : (a : M) → P) m : P) (0 : P)
h₅ :
  ∀
    (h :
      HSMul.hSMul.{u_1, u_4, u_4} (α := R) 2
            (HSMul.hSMul.{u_1, u_4, u_4} (α := R) (β := P) 2 ((Q : (a : M) → P) m : P)) -
          HSMul.hSMul.{u_1, u_4, u_4} (α := R) (β := P) 2 ((Q : (a : M) → P) m : P) =
        0),
    Eq.{u_4 + 1} (α := P) ((Q : (a : M) → P) m : P) (0 : P)
h₆ :
  ∀
    (h :
      HSMul.hSMul.{u_1, u_4, u_4} (α := R) 2
          (HSub.hSub (β := P) (HSMul.hSMul.{u_1, u_4, u_4} (α := R) (β := P) 2 ((Q : (a : M) → P) m : P))
            ((Q : (a : M) → P) m : P)) =
        0),
    Eq.{u_4 + 1} (α := P) ((Q : (a : M) → P) m : P) (0 : P)
h₇ :
  ∀
    (h :
      HSub.hSub (β := P) (HSMul.hSMul.{u_1, u_4, u_4} (α := R) (β := P) 2 ((Q : (a : M) → P) m : P))
          ((Q : (a : M) → P) m : P) =
        0),
    Eq.{u_4 + 1} (α := P) ((Q : (a : M) → P) m : P) (0 : P)
h₈ :
  ∀
    (h :
      HSub.hSub (β := P) (HAdd.hAdd (α := P) (β := P) ((Q : (a : M) → P) m : P) ((Q : (a : M) → P) m : P))
          ((Q : (a : M) → P) m : P) =
        0),
    Eq.{u_4 + 1} (α := P) ((Q : (a : M) → P) m : P) (0 : P)
⊢ Eq.{u_4 + 1} (α := P) ((Q : (a : M) → P) m : P) (0 : P)
have h₉ : ∀ (h : Eq.{u_4 + 1} (α := P) ((Q : (a : M) → P) m : P) (0 : P)), Eq.{u_4 + 1} (α := P) ((Q : (a : M) → P) m : P) (0 : P)
Tactic: rwa [← two_smul R, QuadraticMap.map_smul, sub_sub, ← two_smul R, mul_smul, ← smul_sub,
    (isUnit_of_invertible 2).smul_eq_zero, two_smul, add_sub_cancel_right] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Radical (goal)
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
⊢ Q.radical =
    LinearMap.ker (R₂ := R) (M₂ := M →ₗ[R] P) (τ₁₂ := RingHom.id R)
      ((associated : (a : QuadraticMap R M P) → LinearMap.BilinMap R M P) Q)
have rw : LinearMap.ker Q.polarBilin =
  LinearMap.ker (R₂ := R) (M₂ := M →ₗ[R] P) (τ₁₂ := RingHom.id R)
    ((associated : (a : QuadraticMap R M P) → LinearMap.BilinMap R M P) Q)
Tactic: rw [radical_eq_ker_polarBilin]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Radical (goal)
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.ker Q.polarBilin =
    LinearMap.ker (R₂ := R) (M₂ := M →ₗ[R] P) (τ₁₂ := RingHom.id R)
      ((associated : (a : QuadraticMap R M P) → LinearMap.BilinMap R M P) Q)
have h : ∀ (m : M),
  m ∈ LinearMap.ker Q.polarBilin ↔
    Membership.mem (γ := Submodule R M)
      (LinearMap.ker (R₂ := R) (M₂ := M →ₗ[R] P) (τ₁₂ := RingHom.id R)
        ((associated : (a : QuadraticMap R M P) → LinearMap.BilinMap R M P) Q))
      m
Tactic: ext m
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Radical (goal)
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
⊢ Nondegenerate.{u_1, u_2, u_4} (R := R) (M := M) (P := P) (Q := Q) ↔ Q.radical = ⊥
have refine : ∀ (h : Q.radical = ⊥), Module.rank R ↥(LinearMap.ker Q.polarBilin) ≤ 1
Tactic: refine ⟨Nondegenerate.radical_eq_bot, fun h ↦ ⟨h, ?_⟩⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Radical (goal)
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
h : Q.radical = ⊥
⊢ Module.rank R ↥(LinearMap.ker Q.polarBilin) ≤ 1
have rw : Module.rank R ↥⊥ ≤ 1
Tactic: rw [← QuadraticMap.radical_eq_ker_polarBilin, h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Radical (hypothesis)
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
h : Q.radical = ⊥
⊢ Module.rank R ↥⊥ ≤ 1
have a : Nontrivial R
Tactic: nontriviality R
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Radical (goal)
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.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)
have 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)
Tactic: rw [nondegenerate_iff_radical_eq_bot, radical_eq_ker_associated,
    LinearMap.IsRefl.nondegenerate_iff_separatingLeft, LinearMap.separatingLeft_iff_ker_eq_bot]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Radical (goal)
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.Nondegenerate Q.polarBilin ↔ Nondegenerate.{u_1, u_2, u_4} (R := R) (M := M) (P := P) (Q := Q)
have rw : LinearMap.IsRefl Q.polarBilin
Tactic: rw [nondegenerate_iff_radical_eq_bot, radical_eq_ker_polarBilin,
    LinearMap.IsRefl.nondegenerate_iff_separatingLeft, LinearMap.separatingLeft_iff_ker_eq_bot]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Radical (goal)
Goal:
𝕜 : Type u_1
ι : Type u_2
inst : Field 𝕜
inst_1 : NeZero.{u_1} (R := 𝕜) 2
inst_2 : Fintype ι
w : ι → 𝕜
⊢ Eq (α := Submodule 𝕜 (ι → 𝕜)) (radical (R := 𝕜) (M := ι → 𝕜) (P := 𝕜) (weightedSumSquares 𝕜 w) : Submodule 𝕜 (ι → 𝕜))
    (Pi.spanSubset 𝕜 {i : ι | w i = 0} : Submodule 𝕜 (ι → 𝕜))
have h : ∀ (v : ι → 𝕜),
  Membership.mem (γ := Submodule 𝕜 (ι → 𝕜))
      (radical (R := 𝕜) (M := ι → 𝕜) (P := 𝕜) (weightedSumSquares 𝕜 w) : Submodule 𝕜 (ι → 𝕜)) v ↔
    Membership.mem (γ := Submodule 𝕜 (ι → 𝕜)) (Pi.spanSubset 𝕜 {i : ι | w i = 0}) v
Tactic: ext v
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Radical (goal)
Goal:
𝕜 : Type u_1
ι : Type u_2
inst : Field 𝕜
inst_1 : NeZero.{u_1} (R := 𝕜) 2
inst_2 : Fintype ι
w v : ι → 𝕜
⊢ Membership.mem (γ := Submodule 𝕜 (ι → 𝕜))
      (radical (R := 𝕜) (M := ι → 𝕜) (P := 𝕜) (weightedSumSquares 𝕜 w) : Submodule 𝕜 (ι → 𝕜)) v ↔
    Membership.mem (γ := Submodule 𝕜 (ι → 𝕜)) (Pi.spanSubset 𝕜 {i : ι | w i = 0}) v
have 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
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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Radical (goal)
Goal:
𝕜 : Type u_1
ι : Type u_2
inst : Field 𝕜
inst_1 : NeZero.{u_1} (R := 𝕜) 2
inst_2 : Fintype ι
w 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
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Radical (goal)
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
⊢ (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
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Radical (goal)
Goal:
𝕜 : Type u_1
ι : Type u_2
inst : Field 𝕜
inst_1 : NeZero.{u_1} (R := 𝕜) 2
inst_2 : Fintype ι
w : ι → 𝕜
⊢ Eq (α := Submodule 𝕜 (ι → 𝕜)) (radical (R := 𝕜) (M := ι → 𝕜) (P := 𝕜) (weightedSumSquares 𝕜 w) : Submodule 𝕜 (ι → 𝕜))
    (Pi.spanSubset 𝕜 {i : ι | w i = 0} : Submodule 𝕜 (ι → 𝕜))
have h : ∀ (v : ι → 𝕜),
  Membership.mem (γ := Submodule 𝕜 (ι → 𝕜))
      (radical (R := 𝕜) (M := ι → 𝕜) (P := 𝕜) (weightedSumSquares 𝕜 w) : Submodule 𝕜 (ι → 𝕜)) v ↔
    Membership.mem (γ := Submodule 𝕜 (ι → 𝕜)) (Pi.spanSubset 𝕜 {i : ι | w i = 0}) v
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)⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Radical (goal)
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 𝕜 (ι → 𝕜))
have 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
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)⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Radical (goal)
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
⊢ Eq (α := Submodule 𝕜 (ι → 𝕜)) (radical (R := 𝕜) (M := ι → 𝕜) (P := 𝕜) (weightedSumSquares 𝕜 w) : Submodule 𝕜 (ι → 𝕜))
    (Pi.spanSubset 𝕜 {i : ι | w i = 0} : Submodule 𝕜 (ι → 𝕜))
have 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
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)⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Radical (goal)
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
⊢ Eq (α := Submodule 𝕜 (ι → 𝕜)) (radical (R := 𝕜) (M := ι → 𝕜) (P := 𝕜) (weightedSumSquares 𝕜 w) : Submodule 𝕜 (ι → 𝕜))
    (Pi.spanSubset 𝕜 {i : ι | w i = 0} : Submodule 𝕜 (ι → 𝕜))
have 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
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)⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Radical (goal)
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)
⊢ Module.finrank.{u_1, u_3} 𝕜 ↥(radical (P := 𝕜) Q) = Set.ncard.{u_2} (α := ι) {i : ι | w i = 0}
have rw : Module.finrank 𝕜 ↥(radical (R := 𝕜) (M := ι → 𝕜) (P := 𝕜) (weightedSumSquares 𝕜 w) : Submodule 𝕜 (ι → 𝕜)) =
  Set.ncard.{u_2} (α := ι) {i : ι | w i = 0}
Tactic: rw [hQ.rank_radical_eq, radical_weightedSumSquares, Pi.dim_spanSubset]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Radical (goal)
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}
⊢ Module.finrank.{u_1, u_3} 𝕜 ↥(radical (P := 𝕜) Q) = Set.ncard.{u_2} (α := ι) {i : ι | w i = 0}
have rw₁ : Module.finrank 𝕜 ↥(Pi.spanSubset 𝕜 {i : ι | w i = 0}) = Set.ncard.{u_2} (α := ι) {i : ι | w i = 0}
Tactic: rw [hQ.rank_radical_eq, radical_weightedSumSquares, Pi.dim_spanSubset]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Radical (goal)
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}
⊢ Module.finrank.{u_1, u_3} 𝕜 ↥(radical (P := 𝕜) Q) = Set.ncard.{u_2} (α := ι) {i : ι | w i = 0}
have rw₂ : Set.ncard.{u_2} (α := ι) {i : ι | w i = 0} = Set.ncard.{u_2} (α := ι) {i : ι | w i = 0}
Tactic: rw [hQ.rank_radical_eq, radical_weightedSumSquares, Pi.dim_spanSubset]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Real (hypothesis)
Goal:
ι : Type u_1
inst : Fintype ι
w : ι → ℝ
u : (i : ι) → ℝˣ := fun (i : ι) ↦ if h : w i = 0 then 1 else Units.mk0 (w i) h
⊢ QuadraticMap.IsometryEquiv (M₂ := ι → ℝ) (weightedSumSquares ℝ w)
    (weightedSumSquares (S := ℝ) ℝ fun (i : ι) ↦ (↑((sign : (a : ℝ) → SignType) (w i)) : ℝ))
have hu : ∀ (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