awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Signature
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
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
⊢ 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))

Tactic:
refine .and ?_ (IsometryEquiv.map_posDef_iff _).symm
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Signature
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
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
⊢ 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
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Signature
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
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')
⊢ ∀ (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:
rw [eq_iff_eq_cancel_right]

Premises used: eq_iff_eq_cancel_right
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Signature
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
⊢ 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:
(e.finrank_map_eq _).symm

Premises used: Set.Mem, QuadraticMap.IsometryEquiv.toLinearEquiv, Submodule.map, LinearEquiv.finrank_map_eq, Eq.symm
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Signature
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
⊢ 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:
exact (e.finrank_map_eq _).symm

Premises used: QuadraticMap.IsometryEquiv.toLinearEquiv, LinearEquiv.finrank_map_eq, Eq.symm
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Signature
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'
⊢ Module.finrank R M = Module.finrank R M'

Tactic:
e.toLinearEquiv.finrank_eq

Premises used: LinearEquiv.finrank_eq, QuadraticMap.IsometryEquiv.toLinearEquiv
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Signature
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'
⊢ Module.finrank R M = Module.finrank R M'

Tactic:
exact e.toLinearEquiv.finrank_eq

Premises used: LinearEquiv.finrank_eq, QuadraticMap.IsometryEquiv.toLinearEquiv
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Signature
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'
h : Equivalent Q Q'
e : IsometryEquiv Q Q'
⊢ ∀ (m : M),
    Eq.{u_1 + 1} (α := R) ((-Q' : (a : M') → R) ((↑e.toLinearEquiv : M →ₗ[R] M').toFun m) : R)
      ((-Q : (a : M) → R) m : R)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Signature
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 : 𝕜)
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
⊢ sigPos Q + Module.finrank.{u_4, u_2} 𝕜 ↥V ≤ Module.finrank 𝕜 M

Tactic:
obtain ⟨Vp, hr, hVp⟩ := exists_finrank_eq_sigPos_and_posDef Q

Premises used: exists_finrank_eq_sigPos_and_posDef
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Signature
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
rw : Module.finrank.{u_4, u_2} 𝕜 ↥Vp + Module.finrank.{u_4, u_2} 𝕜 ↥V ≤ Module.finrank 𝕜 M
⊢ sigPos Q + Module.finrank.{u_4, u_2} 𝕜 ↥V ≤ Module.finrank 𝕜 M

Tactic:
rw [← hr]
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Signature
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
hdisjoint : Disjoint Vp V
⊢ Module.finrank.{u_4, u_2} 𝕜 ↥Vp + Module.finrank.{u_4, u_2} 𝕜 ↥V ≤ Module.finrank 𝕜 M

Tactic:
apply Submodule.finrank_add_finrank_le_of_disjoint

Premises used: Submodule.finrank_add_finrank_le_of_disjoint
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Signature
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
hdisjoint : ∀ (hx' : ¬x = 0), False
⊢ x = 0

Tactic:
by_contra hx'
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Signature
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
⊢ Subtype.mk (p := fun (x : M) ↦ x ∈ Vp) x ⋯ ≠ 0

Tactic:
simpa using hx'
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Signature
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
⊢ LT.lt.{u_4} (α := 𝕜) (0 : 𝕜)
    ((QuadraticMap.restrict Q Vp : (a : ↥Vp) → 𝕜) (Subtype.mk (p := fun (x : M) ↦ x ∈ Vp) x ⋯) : 𝕜)

Tactic:
have := hVp ⟨x, hWp hx⟩ (by simpa using hx')
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Signature
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 ⋯) : 𝕜)
⊢ LE.le.{u_4} (α := 𝕜) ((Q : (a : M) → 𝕜) x : 𝕜) (0 : 𝕜)

Tactic:
have := hV x (hWm hx)
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Signature
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_1 :
  LT.lt.{u_4} (α := 𝕜) (0 : 𝕜)
    ((QuadraticMap.restrict Q Vp : (a : ↥Vp) → 𝕜) (Subtype.mk (p := fun (x : M) ↦ x ∈ Vp) x ⋯) : 𝕜)
this : LE.le.{u_4} (α := 𝕜) ((Q : (a : M) → 𝕜) x : 𝕜) (0 : 𝕜)
⊢ False

Tactic:
grind [restrict_apply]

Premises used: QuadraticMap.restrict_apply
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Signature
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
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))
⊢ 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) :
      𝕜)

Tactic:
rw [restrict_apply, weightedSumSquares_apply]

Premises used: QuadraticMap.weightedSumSquares_apply, QuadraticMap.restrict_apply
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Signature
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)
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)
⊢ 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:
apply sum_pos'

Premises used: Finset.sum_pos'
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Signature
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)
⊢ 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:
_
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Signature
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)
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)
⊢ 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
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Signature
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
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:
smul_nonneg (hs i hi).le (mul_self_nonneg _)

Premises used: mul_self_nonneg, smul_nonneg, LT.lt.le
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Signature
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
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:
exact smul_nonneg (hs i hi).le (mul_self_nonneg _)

Premises used: mul_self_nonneg, smul_nonneg, LT.lt.le
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Signature
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
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:
simp [Pi.mem_spanSubset_iff.mp hv i hi]

Premises used: Pi.mem_spanSubset_iff, Iff.mp
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Signature
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
⊢ ∃ (x : ι), ¬v x = 0

Tactic:
simp only [ne_eq, Submodule.mk_eq_zero, funext_iff, not_forall, Pi.zero_apply] at hv'

Premises used: funext_iff, Pi.zero_apply, ne_eq, Classical.not_forall, Submodule.mk_eq_zero
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Signature
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
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)
⊢ ∃ (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'
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Signature
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)

Tactic:
⟨i, mem_univ _, ?_⟩

Premises used: Finset.mem_univ, And.intro, Exists.intro
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Signature
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
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)
⊢ ∃ (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:
refine ⟨i, mem_univ _, ?_⟩