awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Signature (goal)
Goal:
R : Type u_1
M : Type u_2
M' : Type u_3
inst : AddCommGroup M
inst_1 : AddCommGroup M'
inst_2 : CommRing R
inst_3 : LinearOrder R
inst_4 : Module R M
Q : QuadraticForm R M
inst_5 : Module R M'
Q' : QuadraticForm R M'
e : IsometryEquiv Q Q'
h :
  ∀ (j : ℕ),
    (∃ (V : Submodule R M), Module.finrank.{u_1, u_2} R ↥V = j ∧ (restrict Q V).PosDef) ↔
      ∃ (V : Submodule R M'), Module.finrank.{u_1, u_3} R ↥V = j ∧ (restrict Q' V).PosDef
⊢ {r ∈ Iic (Module.finrank R M) |
          ∃ (V : Submodule R M), Module.finrank.{u_1, u_2} R ↥V = r ∧ (restrict Q V).PosDef}.max'
      ⋯ =
    {r ∈ Iic (Module.finrank R M') |
          ∃ (V : Submodule R M'), Module.finrank.{u_1, u_3} R ↥V = r ∧ (restrict Q' V).PosDef}.max'
      ⋯
have h₁ : Module.finrank R M = Module.finrank R M'
Tactic: congr! with j
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Signature (goal)
Goal:
R : Type u_1
M : Type u_2
M' : Type u_3
inst : AddCommGroup M
inst_1 : AddCommGroup M'
inst_2 : CommRing R
inst_3 : LinearOrder R
inst_4 : Module R M
Q : QuadraticForm R M
inst_5 : Module R M'
Q' : QuadraticForm R M'
e : IsometryEquiv Q Q'
j : ℕ
⊢ (∃ (V : Submodule R M), Module.finrank.{u_1, u_2} R ↥V = j ∧ (restrict Q V).PosDef) ↔
    ∃ (V : Submodule R M'), Module.finrank.{u_1, u_3} R ↥V = j ∧ (restrict Q' V).PosDef
have h : ∀ (a : Submodule R M),
  Module.finrank.{u_1, u_2} R ↥a = j ∧ (restrict Q a).PosDef ↔
    Module.finrank.{u_1, u_3} R
          ↥(((Submodule.orderIsoMapComap e.toLinearEquiv).toEquiv (r := fun (x1 x2 : Submodule R M) ↦ x1 ≤ x2) (s :=
                    fun (x1 x2 : Submodule R M') ↦ x1 ≤ x2) :
                  (a : Submodule R M) → Submodule R M')
                a :
              Submodule R M') =
        j ∧
      PosDef (M :=
        ↥(((Submodule.orderIsoMapComap e.toLinearEquiv).toEquiv (r := fun (x1 x2 : Submodule R M) ↦ x1 ≤ x2) (s :=
                  fun (x1 x2 : Submodule R M') ↦ x1 ≤ x2) :
                (a : Submodule R M) → Submodule R M')
              a :
            Submodule R M'))
        (restrict Q'
          (((Submodule.orderIsoMapComap e.toLinearEquiv).toEquiv (r := fun (x1 x2 : Submodule R M) ↦ x1 ≤ x2) (s :=
                fun (x1 x2 : Submodule R M') ↦ x1 ≤ x2) :
              (a : Submodule R M) → Submodule R M')
            a))
Tactic: apply (Submodule.orderIsoMapComap e.toLinearEquiv).exists_congr
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Signature (goal)
Goal:
R : Type u_1
M : Type u_2
M' : Type u_3
inst : AddCommGroup M
inst_1 : AddCommGroup M'
inst_2 : CommRing R
inst_3 : LinearOrder R
inst_4 : Module R M
Q : QuadraticForm R M
inst_5 : Module R M'
Q' : QuadraticForm R M'
e : IsometryEquiv Q Q'
j : ℕ
V : Submodule R M
⊢ Module.finrank.{u_1, u_2} R ↥V = j ∧ (restrict Q V).PosDef ↔
    Module.finrank.{u_1, u_3} R
          ↥(((Submodule.orderIsoMapComap e.toLinearEquiv).toEquiv (r := fun (x1 x2 : Submodule R M) ↦ x1 ≤ x2) (s :=
                    fun (x1 x2 : Submodule R M') ↦ x1 ≤ x2) :
                  (a : Submodule R M) → Submodule R M')
                V :
              Submodule R M') =
        j ∧
      PosDef (M :=
        ↥(((Submodule.orderIsoMapComap e.toLinearEquiv).toEquiv (r := fun (x1 x2 : Submodule R M) ↦ x1 ≤ x2) (s :=
                  fun (x1 x2 : Submodule R M') ↦ x1 ≤ x2) :
                (a : Submodule R M) → Submodule R M')
              V :
            Submodule R M'))
        (restrict Q'
          (((Submodule.orderIsoMapComap e.toLinearEquiv).toEquiv (r := fun (x1 x2 : Submodule R M) ↦ x1 ≤ x2) (s :=
                fun (x1 x2 : Submodule R M') ↦ x1 ≤ x2) :
              (a : Submodule R M) → Submodule R M')
            V))
have h : Module.finrank.{u_1, u_2} R ↥V = j ↔
  Module.finrank.{u_1, u_3} R
      ↥(((Submodule.orderIsoMapComap e.toLinearEquiv).toEquiv (r := fun (x1 x2 : Submodule R M) ↦ x1 ≤ x2) (s :=
                fun (x1 x2 : Submodule R M') ↦ x1 ≤ x2) :
              (a : Submodule R M) → Submodule R M')
            V :
          Submodule R M') =
    j
Tactic: refine .and ?_ (IsometryEquiv.map_posDef_iff _).symm
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Signature (goal)
Goal:
R : Type u_1
M : Type u_2
M' : Type u_3
inst : AddCommGroup M
inst_1 : AddCommGroup M'
inst_2 : CommRing R
inst_3 : LinearOrder R
inst_4 : Module R M
Q : QuadraticForm R M
inst_5 : Module R M'
Q' : QuadraticForm R M'
e : IsometryEquiv Q Q'
j : ℕ
V : Submodule R M
⊢ Module.finrank.{u_1, u_2} R ↥V = j ↔
    Module.finrank.{u_1, u_3} R
        ↥(((Submodule.orderIsoMapComap e.toLinearEquiv).toEquiv (r := fun (x1 x2 : Submodule R M) ↦ x1 ≤ x2) (s :=
                  fun (x1 x2 : Submodule R M') ↦ x1 ≤ x2) :
                (a : Submodule R M) → Submodule R M')
              V :
            Submodule R M') =
      j
have h : ∀ (j : ℕ),
  Module.finrank.{u_1, u_2} R ↥V = j ↔
    Module.finrank.{u_1, u_3} R
        ↥(((Submodule.orderIsoMapComap e.toLinearEquiv).toEquiv (r := fun (x1 x2 : Submodule R M) ↦ x1 ≤ x2) (s :=
                  fun (x1 x2 : Submodule R M') ↦ x1 ≤ x2) :
                (a : Submodule R M) → Submodule R M')
              V :
            Submodule R M') =
      j
Tactic: revert j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Signature (goal)
Goal:
R : Type u_1
M : Type u_2
M' : Type u_3
inst : AddCommGroup M
inst_1 : AddCommGroup M'
inst_2 : CommRing R
inst_3 : LinearOrder R
inst_4 : Module R M
Q : QuadraticForm R M
inst_5 : Module R M'
Q' : QuadraticForm R M'
e : IsometryEquiv Q Q'
V : Submodule R M
⊢ ∀ (j : ℕ),
    Module.finrank.{u_1, u_2} R ↥V = j ↔
      Module.finrank.{u_1, u_3} R
          ↥(((Submodule.orderIsoMapComap e.toLinearEquiv).toEquiv (r := fun (x1 x2 : Submodule R M) ↦ x1 ≤ x2) (s :=
                    fun (x1 x2 : Submodule R M') ↦ x1 ≤ x2) :
                  (a : Submodule R M) → Submodule R M')
                V :
              Submodule R M') =
        j
have h : Module.finrank.{u_1, u_2} R ↥V =
  Module.finrank.{u_1, u_3} R
    ↥(((Submodule.orderIsoMapComap e.toLinearEquiv).toEquiv (r := fun (x1 x2 : Submodule R M) ↦ x1 ≤ x2) (s :=
              fun (x1 x2 : Submodule R M') ↦ x1 ≤ x2) :
            (a : Submodule R M) → Submodule R M')
          V :
        Submodule R M')
Tactic: rw [eq_iff_eq_cancel_right]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Signature (goal)
Goal:
M : Type u_2
inst : AddCommGroup M
𝕜 : Type u_4
inst_1 : Field 𝕜
inst_2 : LinearOrder 𝕜
inst_3 : Module 𝕜 M
Q : QuadraticForm 𝕜 M
inst_4 : FiniteDimensional 𝕜 M
V : Subspace 𝕜 M
hV : ∀ x ∈ V, LE.le.{u_4} (α := 𝕜) ((Q : (a : M) → 𝕜) x : 𝕜) (0 : 𝕜)
⊢ sigPos Q + Module.finrank.{u_4, u_2} 𝕜 ↥V ≤ Module.finrank 𝕜 M
have obtain : ∀ (Vp : Submodule 𝕜 M) (hr : Module.finrank.{u_4, u_2} 𝕜 ↥Vp = sigPos Q) (hVp : (QuadraticMap.restrict Q Vp).PosDef),
  sigPos Q + Module.finrank.{u_4, u_2} 𝕜 ↥V ≤ Module.finrank 𝕜 M
Tactic: obtain ⟨Vp, hr, hVp⟩ := exists_finrank_eq_sigPos_and_posDef Q
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Signature (goal)
Goal:
M : Type u_2
inst : AddCommGroup M
𝕜 : Type u_4
inst_1 : Field 𝕜
inst_2 : LinearOrder 𝕜
inst_3 : Module 𝕜 M
Q : QuadraticForm 𝕜 M
inst_4 : FiniteDimensional 𝕜 M
V : Subspace 𝕜 M
hV : ∀ x ∈ V, LE.le.{u_4} (α := 𝕜) ((Q : (a : M) → 𝕜) x : 𝕜) (0 : 𝕜)
Vp : Submodule 𝕜 M
hr : Module.finrank.{u_4, u_2} 𝕜 ↥Vp = sigPos Q
hVp : (QuadraticMap.restrict Q Vp).PosDef
⊢ sigPos Q + Module.finrank.{u_4, u_2} 𝕜 ↥V ≤ Module.finrank 𝕜 M
have rw : Module.finrank.{u_4, u_2} 𝕜 ↥Vp + Module.finrank.{u_4, u_2} 𝕜 ↥V ≤ Module.finrank 𝕜 M
Tactic: rw [← hr]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Signature (goal)
Goal:
M : Type u_2
inst : AddCommGroup M
𝕜 : Type u_4
inst_1 : Field 𝕜
inst_2 : LinearOrder 𝕜
inst_3 : Module 𝕜 M
Q : QuadraticForm 𝕜 M
inst_4 : FiniteDimensional 𝕜 M
V : Subspace 𝕜 M
hV : ∀ x ∈ V, LE.le.{u_4} (α := 𝕜) ((Q : (a : M) → 𝕜) x : 𝕜) (0 : 𝕜)
Vp : Submodule 𝕜 M
hr : Module.finrank.{u_4, u_2} 𝕜 ↥Vp = sigPos Q
hVp : (QuadraticMap.restrict Q Vp).PosDef
⊢ Module.finrank.{u_4, u_2} 𝕜 ↥Vp + Module.finrank.{u_4, u_2} 𝕜 ↥V ≤ Module.finrank 𝕜 M
have hdisjoint : Disjoint Vp V
Tactic: apply Submodule.finrank_add_finrank_le_of_disjoint
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Signature (goal)
Goal:
M : Type u_2
inst : AddCommGroup M
𝕜 : Type u_4
inst_1 : Field 𝕜
inst_2 : LinearOrder 𝕜
inst_3 : Module 𝕜 M
Q : QuadraticForm 𝕜 M
inst_4 : FiniteDimensional 𝕜 M
V : Subspace 𝕜 M
hV : ∀ x ∈ V, LE.le.{u_4} (α := 𝕜) ((Q : (a : M) → 𝕜) x : 𝕜) (0 : 𝕜)
Vp : Submodule 𝕜 M
hr : Module.finrank.{u_4, u_2} 𝕜 ↥Vp = sigPos Q
hVp : (QuadraticMap.restrict Q Vp).PosDef
W : Submodule 𝕜 M
hWp : W ≤ Vp
hWm : W ≤ V
x : M
hx : x ∈ W
⊢ x = 0
have hdisjoint : ∀ (hx' : ¬x = 0), False
Tactic: by_contra hx'
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Signature (hypothesis)
Goal:
M : Type u_2
inst : AddCommGroup M
𝕜 : Type u_4
inst_1 : Field 𝕜
inst_2 : LinearOrder 𝕜
inst_3 : Module 𝕜 M
Q : QuadraticForm 𝕜 M
inst_4 : FiniteDimensional 𝕜 M
V : Subspace 𝕜 M
hV : ∀ x ∈ V, LE.le.{u_4} (α := 𝕜) ((Q : (a : M) → 𝕜) x : 𝕜) (0 : 𝕜)
Vp : Submodule 𝕜 M
hr : Module.finrank.{u_4, u_2} 𝕜 ↥Vp = sigPos Q
hVp : (QuadraticMap.restrict Q Vp).PosDef
W : Submodule 𝕜 M
hWp : W ≤ Vp
hWm : W ≤ V
x : M
hx : x ∈ W
hx' : ¬x = 0
⊢ False
have this : LT.lt.{u_4} (α := 𝕜) (0 : 𝕜)
  ((QuadraticMap.restrict Q Vp : (a : ↥Vp) → 𝕜) (Subtype.mk (p := fun (x : M) ↦ x ∈ Vp) x sorry) : 𝕜)
Tactic: have := hVp ⟨x, hWp hx⟩ (by simpa using hx')
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Signature (hypothesis)
Goal:
M : Type u_2
inst : AddCommGroup M
𝕜 : Type u_4
inst_1 : Field 𝕜
inst_2 : LinearOrder 𝕜
inst_3 : Module 𝕜 M
Q : QuadraticForm 𝕜 M
inst_4 : FiniteDimensional 𝕜 M
V : Subspace 𝕜 M
hV : ∀ x ∈ V, LE.le.{u_4} (α := 𝕜) ((Q : (a : M) → 𝕜) x : 𝕜) (0 : 𝕜)
Vp : Submodule 𝕜 M
hr : Module.finrank.{u_4, u_2} 𝕜 ↥Vp = sigPos Q
hVp : (QuadraticMap.restrict Q Vp).PosDef
W : Submodule 𝕜 M
hWp : W ≤ Vp
hWm : W ≤ V
x : M
hx : x ∈ W
hx' : ¬x = 0
this :
  LT.lt.{u_4} (α := 𝕜) (0 : 𝕜)
    ((QuadraticMap.restrict Q Vp : (a : ↥Vp) → 𝕜) (Subtype.mk (p := fun (x : M) ↦ x ∈ Vp) x ⋯) : 𝕜)
⊢ False
have this₁ : LE.le.{u_4} (α := 𝕜) ((Q : (a : M) → 𝕜) x : 𝕜) (0 : 𝕜)
Tactic: have := hV x (hWm hx)
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Signature (goal)
Goal:
𝕜 : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
ι : Type u_5
inst_2 : Fintype ι
w : ι → 𝕜
inst_3 : IsStrictOrderedRing 𝕜
s : Set ι
hs : ∀ i ∈ s, 0 < w i
v : ι → 𝕜
hv : Membership.mem (γ := Submodule 𝕜 (ι → 𝕜)) (Pi.spanSubset 𝕜 s) v
hv' : Subtype.mk (p := fun (x : ι → 𝕜) ↦ Membership.mem (γ := Submodule 𝕜 (ι → 𝕜)) (Pi.spanSubset 𝕜 s) x) v hv ≠ 0
⊢ LT.lt.{u_4} (α := 𝕜) (0 : 𝕜)
    ((QuadraticMap.restrict (weightedSumSquares 𝕜 w) (Pi.spanSubset 𝕜 s) : (a : ↥(Pi.spanSubset 𝕜 s)) → 𝕜)
        (Subtype.mk (p := fun (x : ι → 𝕜) ↦ Membership.mem (γ := Submodule 𝕜 (ι → 𝕜)) (Pi.spanSubset 𝕜 s) x) v hv) :
      𝕜)
have rw : LT.lt.{u_4} (α := 𝕜) 0
  (∑ i : ι,
    w i •
      ((↑(Subtype.mk (p := fun (x : ι → 𝕜) ↦ Membership.mem (γ := Submodule 𝕜 (ι → 𝕜)) (Pi.spanSubset 𝕜 s) x) v hv) :
            ι → 𝕜)
          i *
        (↑(Subtype.mk (p := fun (x : ι → 𝕜) ↦ Membership.mem (γ := Submodule 𝕜 (ι → 𝕜)) (Pi.spanSubset 𝕜 s) x) v hv) :
            ι → 𝕜)
          i))
Tactic: rw [restrict_apply, weightedSumSquares_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Signature (goal)
Goal:
𝕜 : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
ι : Type u_5
inst_2 : Fintype ι
w : ι → 𝕜
inst_3 : IsStrictOrderedRing 𝕜
s : Set ι
hs : ∀ i ∈ s, 0 < w i
v : ι → 𝕜
hv : Membership.mem (γ := Submodule 𝕜 (ι → 𝕜)) (Pi.spanSubset 𝕜 s) v
hv' : Subtype.mk (p := fun (x : ι → 𝕜) ↦ Membership.mem (γ := Submodule 𝕜 (ι → 𝕜)) (Pi.spanSubset 𝕜 s) x) v hv ≠ 0
⊢ LT.lt.{u_4} (α := 𝕜) 0
    (∑ i : ι,
      w i •
        ((↑(Subtype.mk (p := fun (x : ι → 𝕜) ↦ Membership.mem (γ := Submodule 𝕜 (ι → 𝕜)) (Pi.spanSubset 𝕜 s) x) v hv) :
              ι → 𝕜)
            i *
          (↑(Subtype.mk (p := fun (x : ι → 𝕜) ↦ Membership.mem (γ := Submodule 𝕜 (ι → 𝕜)) (Pi.spanSubset 𝕜 s) x) v hv) :
              ι → 𝕜)
            i))
have h : ∀ (i : ι),
  Membership.mem (γ := Finset ι) univ i →
    0 ≤
      w i •
        ((↑(Subtype.mk (p := fun (x : ι → 𝕜) ↦ Membership.mem (γ := Submodule 𝕜 (ι → 𝕜)) (Pi.spanSubset 𝕜 s) x) v hv) :
              ι → 𝕜)
            i *
          (↑(Subtype.mk (p := fun (x : ι → 𝕜) ↦ Membership.mem (γ := Submodule 𝕜 (ι → 𝕜)) (Pi.spanSubset 𝕜 s) x) v hv) :
              ι → 𝕜)
            i)
Tactic: apply sum_pos'
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Signature (goal)
Goal:
𝕜 : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
ι : Type u_5
inst_2 : Fintype ι
w : ι → 𝕜
inst_3 : IsStrictOrderedRing 𝕜
s : Set ι
hs : ∀ i ∈ s, 0 < w i
v : ι → 𝕜
hv : Membership.mem (γ := Submodule 𝕜 (ι → 𝕜)) (Pi.spanSubset 𝕜 s) v
hv' : Subtype.mk (p := fun (x : ι → 𝕜) ↦ Membership.mem (γ := Submodule 𝕜 (ι → 𝕜)) (Pi.spanSubset 𝕜 s) x) v hv ≠ 0
h :
  ∀ (i : ι),
    Membership.mem (γ := Finset ι) univ i →
      0 ≤
        w i •
          ((↑(Subtype.mk (p := fun (x : ι → 𝕜) ↦ Membership.mem (γ := Submodule 𝕜 (ι → 𝕜)) (Pi.spanSubset 𝕜 s) x) v
                    hv) :
                ι → 𝕜)
              i *
            (↑(Subtype.mk (p := fun (x : ι → 𝕜) ↦ Membership.mem (γ := Submodule 𝕜 (ι → 𝕜)) (Pi.spanSubset 𝕜 s) x) v
                    hv) :
                ι → 𝕜)
              i)
⊢ LT.lt.{u_4} (α := 𝕜) 0
    (∑ i : ι,
      w i •
        ((↑(Subtype.mk (p := fun (x : ι → 𝕜) ↦ Membership.mem (γ := Submodule 𝕜 (ι → 𝕜)) (Pi.spanSubset 𝕜 s) x) v hv) :
              ι → 𝕜)
            i *
          (↑(Subtype.mk (p := fun (x : ι → 𝕜) ↦ Membership.mem (γ := Submodule 𝕜 (ι → 𝕜)) (Pi.spanSubset 𝕜 s) x) v hv) :
              ι → 𝕜)
            i))
have hs₁ : ∃ (i : ι),
  Membership.mem (γ := Finset ι) univ i ∧
    0 <
      w i •
        ((↑(Subtype.mk (p := fun (x : ι → 𝕜) ↦ Membership.mem (γ := Submodule 𝕜 (ι → 𝕜)) (Pi.spanSubset 𝕜 s) x) v hv) :
              ι → 𝕜)
            i *
          (↑(Subtype.mk (p := fun (x : ι → 𝕜) ↦ Membership.mem (γ := Submodule 𝕜 (ι → 𝕜)) (Pi.spanSubset 𝕜 s) x) v hv) :
              ι → 𝕜)
            i)
Tactic: apply sum_pos'
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Signature (goal)
Goal:
𝕜 : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
ι : Type u_5
inst_2 : Fintype ι
w : ι → 𝕜
inst_3 : IsStrictOrderedRing 𝕜
s : Set ι
hs : ∀ i ∈ s, 0 < w i
v : ι → 𝕜
hv : Membership.mem (γ := Submodule 𝕜 (ι → 𝕜)) (Pi.spanSubset 𝕜 s) v
hv' : Subtype.mk (p := fun (x : ι → 𝕜) ↦ Membership.mem (γ := Submodule 𝕜 (ι → 𝕜)) (Pi.spanSubset 𝕜 s) x) v hv ≠ 0
i : ι
h : Membership.mem (γ := Finset ι) univ i
⊢ 0 ≤
    w i •
      ((↑(Subtype.mk (p := fun (x : ι → 𝕜) ↦ Membership.mem (γ := Submodule 𝕜 (ι → 𝕜)) (Pi.spanSubset 𝕜 s) x) v hv) :
            ι → 𝕜)
          i *
        (↑(Subtype.mk (p := fun (x : ι → 𝕜) ↦ Membership.mem (γ := Submodule 𝕜 (ι → 𝕜)) (Pi.spanSubset 𝕜 s) x) v hv) :
            ι → 𝕜)
          i)
have pos : ∀ (hi : i ∈ s),
  0 ≤
    w i •
      ((↑(Subtype.mk (p := fun (x : ι → 𝕜) ↦ Membership.mem (γ := Submodule 𝕜 (ι → 𝕜)) (Pi.spanSubset 𝕜 s) x) v hv) :
            ι → 𝕜)
          i *
        (↑(Subtype.mk (p := fun (x : ι → 𝕜) ↦ Membership.mem (γ := Submodule 𝕜 (ι → 𝕜)) (Pi.spanSubset 𝕜 s) x) v hv) :
            ι → 𝕜)
          i)
Tactic: by_cases hi : i ∈ s
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Signature (goal)
Goal:
𝕜 : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
ι : Type u_5
inst_2 : Fintype ι
w : ι → 𝕜
inst_3 : IsStrictOrderedRing 𝕜
s : Set ι
hs : ∀ i ∈ s, 0 < w i
v : ι → 𝕜
hv : Membership.mem (γ := Submodule 𝕜 (ι → 𝕜)) (Pi.spanSubset 𝕜 s) v
hv' : Subtype.mk (p := fun (x : ι → 𝕜) ↦ Membership.mem (γ := Submodule 𝕜 (ι → 𝕜)) (Pi.spanSubset 𝕜 s) x) v hv ≠ 0
i : ι
h : Membership.mem (γ := Finset ι) univ i
pos :
  ∀ (hi : i ∈ s),
    0 ≤
      w i •
        ((↑(Subtype.mk (p := fun (x : ι → 𝕜) ↦ Membership.mem (γ := Submodule 𝕜 (ι → 𝕜)) (Pi.spanSubset 𝕜 s) x) v hv) :
              ι → 𝕜)
            i *
          (↑(Subtype.mk (p := fun (x : ι → 𝕜) ↦ Membership.mem (γ := Submodule 𝕜 (ι → 𝕜)) (Pi.spanSubset 𝕜 s) x) v hv) :
              ι → 𝕜)
            i)
⊢ 0 ≤
    w i •
      ((↑(Subtype.mk (p := fun (x : ι → 𝕜) ↦ Membership.mem (γ := Submodule 𝕜 (ι → 𝕜)) (Pi.spanSubset 𝕜 s) x) v hv) :
            ι → 𝕜)
          i *
        (↑(Subtype.mk (p := fun (x : ι → 𝕜) ↦ Membership.mem (γ := Submodule 𝕜 (ι → 𝕜)) (Pi.spanSubset 𝕜 s) x) v hv) :
            ι → 𝕜)
          i)
have neg : ∀ (hi : i ∉ s),
  0 ≤
    w i •
      ((↑(Subtype.mk (p := fun (x : ι → 𝕜) ↦ Membership.mem (γ := Submodule 𝕜 (ι → 𝕜)) (Pi.spanSubset 𝕜 s) x) v hv) :
            ι → 𝕜)
          i *
        (↑(Subtype.mk (p := fun (x : ι → 𝕜) ↦ Membership.mem (γ := Submodule 𝕜 (ι → 𝕜)) (Pi.spanSubset 𝕜 s) x) v hv) :
            ι → 𝕜)
          i)
Tactic: by_cases hi : i ∈ s
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Signature (hypothesis)
Goal:
𝕜 : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
ι : Type u_5
inst_2 : Fintype ι
w : ι → 𝕜
inst_3 : IsStrictOrderedRing 𝕜
s : Set ι
hs : ∀ i ∈ s, 0 < w i
v : ι → 𝕜
hv : Membership.mem (γ := Submodule 𝕜 (ι → 𝕜)) (Pi.spanSubset 𝕜 s) v
hv' : Subtype.mk (p := fun (x : ι → 𝕜) ↦ Membership.mem (γ := Submodule 𝕜 (ι → 𝕜)) (Pi.spanSubset 𝕜 s) x) v hv ≠ 0
⊢ ∃ (i : ι),
    Membership.mem (γ := Finset ι) univ i ∧
      0 <
        w i •
          ((↑(Subtype.mk (p := fun (x : ι → 𝕜) ↦ Membership.mem (γ := Submodule 𝕜 (ι → 𝕜)) (Pi.spanSubset 𝕜 s) x) v
                    hv) :
                ι → 𝕜)
              i *
            (↑(Subtype.mk (p := fun (x : ι → 𝕜) ↦ Membership.mem (γ := Submodule 𝕜 (ι → 𝕜)) (Pi.spanSubset 𝕜 s) x) v
                    hv) :
                ι → 𝕜)
              i)
have hv'₁ : ∃ (x : ι), ¬v x = 0
Tactic: simp only [ne_eq, Submodule.mk_eq_zero, funext_iff, not_forall, Pi.zero_apply] at hv'
Cleared hypotheses: hv'
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Signature (goal)
Goal:
𝕜 : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
ι : Type u_5
inst_2 : Fintype ι
w : ι → 𝕜
inst_3 : IsStrictOrderedRing 𝕜
s : Set ι
hs : ∀ i ∈ s, 0 < w i
v : ι → 𝕜
hv : Membership.mem (γ := Submodule 𝕜 (ι → 𝕜)) (Pi.spanSubset 𝕜 s) v
hv' : ∃ (x : ι), ¬v x = 0
⊢ ∃ (i : ι),
    Membership.mem (γ := Finset ι) univ i ∧
      0 <
        w i •
          ((↑(Subtype.mk (p := fun (x : ι → 𝕜) ↦ Membership.mem (γ := Submodule 𝕜 (ι → 𝕜)) (Pi.spanSubset 𝕜 s) x) v
                    hv) :
                ι → 𝕜)
              i *
            (↑(Subtype.mk (p := fun (x : ι → 𝕜) ↦ Membership.mem (γ := Submodule 𝕜 (ι → 𝕜)) (Pi.spanSubset 𝕜 s) x) v
                    hv) :
                ι → 𝕜)
              i)
have hs₁ : ∀ (i : ι) (hi : ¬v i = 0),
  ∃ (i : ι),
    Membership.mem (γ := Finset ι) univ i ∧
      0 <
        w i •
          ((↑(Subtype.mk (p := fun (x : ι → 𝕜) ↦ Membership.mem (γ := Submodule 𝕜 (ι → 𝕜)) (Pi.spanSubset 𝕜 s) x) v
                    hv) :
                ι → 𝕜)
              i *
            (↑(Subtype.mk (p := fun (x : ι → 𝕜) ↦ Membership.mem (γ := Submodule 𝕜 (ι → 𝕜)) (Pi.spanSubset 𝕜 s) x) v
                    hv) :
                ι → 𝕜)
              i)
Tactic: obtain ⟨i, hi⟩ := hv'
Cleared hypotheses: hv'
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Signature (goal)
Goal:
𝕜 : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
ι : Type u_5
inst_2 : Fintype ι
w : ι → 𝕜
inst_3 : IsStrictOrderedRing 𝕜
s : Set ι
hs : ∀ i ∈ s, 0 < w i
v : ι → 𝕜
hv : Membership.mem (γ := Submodule 𝕜 (ι → 𝕜)) (Pi.spanSubset 𝕜 s) v
i : ι
hi : ¬v i = 0
⊢ ∃ (i : ι),
    Membership.mem (γ := Finset ι) univ i ∧
      0 <
        w i •
          ((↑(Subtype.mk (p := fun (x : ι → 𝕜) ↦ Membership.mem (γ := Submodule 𝕜 (ι → 𝕜)) (Pi.spanSubset 𝕜 s) x) v
                    hv) :
                ι → 𝕜)
              i *
            (↑(Subtype.mk (p := fun (x : ι → 𝕜) ↦ Membership.mem (γ := Submodule 𝕜 (ι → 𝕜)) (Pi.spanSubset 𝕜 s) x) v
                    hv) :
                ι → 𝕜)
              i)
have hs₁ : 0 <
  w i •
    ((↑(Subtype.mk (p := fun (x : ι → 𝕜) ↦ Membership.mem (γ := Submodule 𝕜 (ι → 𝕜)) (Pi.spanSubset 𝕜 s) x) v hv) :
          ι → 𝕜)
        i *
      (↑(Subtype.mk (p := fun (x : ι → 𝕜) ↦ Membership.mem (γ := Submodule 𝕜 (ι → 𝕜)) (Pi.spanSubset 𝕜 s) x) v hv) :
          ι → 𝕜)
        i)
Tactic: refine ⟨i, mem_univ _, ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Signature (goal)
Goal:
𝕜 : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
ι : Type u_5
inst_2 : Fintype ι
w : ι → 𝕜
inst_3 : IsStrictOrderedRing 𝕜
s : Set ι
hs : ∀ i ∈ s, 0 < w i
v : ι → 𝕜
hv : Membership.mem (γ := Submodule 𝕜 (ι → 𝕜)) (Pi.spanSubset 𝕜 s) v
i : ι
hi : ¬v i = 0
⊢ i ∈ s
have contrapose : ∀ (hi : i ∉ s), v i = 0
Tactic: contrapose hi
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Signature (hypothesis)
Goal:
𝕜 : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
ι : Type u_5
inst_2 : Fintype ι
w : ι → 𝕜
inst_3 : IsStrictOrderedRing 𝕜
s : Set ι
hs : ∀ i ∈ s, 0 < w i
v : ι → 𝕜
hv : Membership.mem (γ := Submodule 𝕜 (ι → 𝕜)) (Pi.spanSubset 𝕜 s) v
i : ι
hi : ¬v i = 0
⊢ 0 <
    w i •
      ((↑(Subtype.mk (p := fun (x : ι → 𝕜) ↦ Membership.mem (γ := Submodule 𝕜 (ι → 𝕜)) (Pi.spanSubset 𝕜 s) x) v hv) :
            ι → 𝕜)
          i *
        (↑(Subtype.mk (p := fun (x : ι → 𝕜) ↦ Membership.mem (γ := Submodule 𝕜 (ι → 𝕜)) (Pi.spanSubset 𝕜 s) x) v hv) :
            ι → 𝕜)
          i)
have this : i ∈ s
Tactic: have : i ∈ s := by
      contrapose hi
      exact Pi.mem_spanSubset_iff.mp hv i hi
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Signature (goal)
Goal:
𝕜 : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
ι : Type u_5
inst_2 : Fintype ι
w : ι → 𝕜
inst_3 : IsStrictOrderedRing 𝕜
s : Set ι
hs : ∀ i ∈ s, w i ≤ 0
x : ι → 𝕜
hx : Membership.mem (γ := Submodule 𝕜 (ι → 𝕜)) (Pi.spanSubset 𝕜 s) x
⊢ LE.le.{u_4} (α := 𝕜) ((weightedSumSquares 𝕜 w : (a : ι → 𝕜) → 𝕜) x : 𝕜) (0 : 𝕜)
have simp : LE.le.{u_4} (α := 𝕜) (∑ x_1 : ι, w x_1 * (x x_1 * x x_1)) 0
Tactic: simp only [weightedSumSquares_apply, smul_eq_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Signature (goal)
Goal:
𝕜 : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
ι : Type u_5
inst_2 : Fintype ι
w : ι → 𝕜
inst_3 : IsStrictOrderedRing 𝕜
s : Set ι
hs : ∀ i ∈ s, w i ≤ 0
x : ι → 𝕜
hx : Membership.mem (γ := Submodule 𝕜 (ι → 𝕜)) (Pi.spanSubset 𝕜 s) x
⊢ LE.le.{u_4} (α := 𝕜) (∑ x_1 : ι, w x_1 * (x x_1 * x x_1)) 0
have h : ∀ (i : ι), Membership.mem (γ := Finset ι) univ i → w i * (x i * x i) ≤ 0
Tactic: apply sum_nonpos
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Signature (goal)
Goal:
𝕜 : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
ι : Type u_5
inst_2 : Fintype ι
w : ι → 𝕜
inst_3 : IsStrictOrderedRing 𝕜
s : Set ι
hs : ∀ i ∈ s, w i ≤ 0
x : ι → 𝕜
hx : Membership.mem (γ := Submodule 𝕜 (ι → 𝕜)) (Pi.spanSubset 𝕜 s) x
i : ι
h : Membership.mem (γ := Finset ι) univ i
⊢ w i * (x i * x i) ≤ 0
have pos : ∀ (hi : i ∈ s), w i * (x i * x i) ≤ 0
Tactic: by_cases hi : i ∈ s
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Signature (goal)
Goal:
𝕜 : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
ι : Type u_5
inst_2 : Fintype ι
w : ι → 𝕜
inst_3 : IsStrictOrderedRing 𝕜
s : Set ι
hs : ∀ i ∈ s, w i ≤ 0
x : ι → 𝕜
hx : Membership.mem (γ := Submodule 𝕜 (ι → 𝕜)) (Pi.spanSubset 𝕜 s) x
i : ι
h : Membership.mem (γ := Finset ι) univ i
pos : ∀ (hi : i ∈ s), w i * (x i * x i) ≤ 0
⊢ w i * (x i * x i) ≤ 0
have neg : ∀ (hi : i ∉ s), w i * (x i * x i) ≤ 0
Tactic: by_cases hi : i ∈ s
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Signature (goal)
Goal:
𝕜 : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
ι : Type u_5
inst_2 : Fintype ι
w : ι → 𝕜
inst_3 : IsStrictOrderedRing 𝕜
s : Set ι
hs : ∀ i ∈ s, w i ≤ 0
x : ι → 𝕜
hx : Membership.mem (γ := Submodule 𝕜 (ι → 𝕜)) (Pi.spanSubset 𝕜 s) x
i : ι
h : Membership.mem (γ := Finset ι) univ i
hi : i ∉ s
⊢ w i * (x i * x i) ≤ 0
have neg : w i * HMul.hMul (α := 𝕜) 0 0 ≤ 0
Tactic: rw [Pi.mem_spanSubset_iff.mp hx i hi, mul_zero, mul_zero]