awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 = neg
⊢ Eq (α := ℝ) ((fun (x : Fin (finrank ℝ M)) ↦ ((↑(w x) : ℝ) : ℝ)) i) (-1) ∨
    Eq (α := ℝ) ((fun (x : Fin (finrank ℝ M)) ↦ ((↑(w x) : ℝ) : ℝ)) i) 1

Tactic:
simp_all
-- 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 = pos
⊢ Eq (α := ℝ) ((fun (x : Fin (finrank ℝ M)) ↦ ((↑(w x) : ℝ) : ℝ)) i) (-1) ∨
    Eq (α := ℝ) ((fun (x : Fin (finrank ℝ M)) ↦ ((↑(w x) : ℝ) : ℝ)) i) 1

Tactic:
simp_all
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Real
Goal:
M : Type u_2
inst : AddCommGroup M
inst_1 : Module ℝ M
inst_2 : FiniteDimensional ℝ M
Q : QuadraticForm ℝ M
⊢ ∃ (w : Fin (finrank ℝ M) → SignType),
    Equivalent (M₂ := Fin (finrank ℝ M) → ℝ) Q
      (weightedSumSquares (S := ℝ) ℝ fun (i : Fin (finrank ℝ M)) ↦ (↑(w i) : ℝ))

Tactic:
let ⟨w, ⟨hw₁⟩⟩ := Q.equivalent_weightedSumSquares
  ⟨sign ∘ w, ⟨hw₁.trans (isometryEquivSignWeightedSumSquares w)⟩⟩

Premises used: SignType.cast, Real, Function.comp, Exists, QuadraticForm.equivalent_weightedSumSquares, _private.0.QuadraticForm.equivalent_signType_weighted_sum_squared.match_1, Nonempty.intro, QuadraticMap.weightedSumSquares, QuadraticForm.isometryEquivSignWeightedSumSquares, Exists.intro, DFunLike.coe, SignType.sign, QuadraticMap.IsometryEquiv.trans, QuadraticMap.Equivalent
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Real
Goal:
M : Type u_2
inst : AddCommGroup M
inst_1 : Module ℝ M
inst_2 : FiniteDimensional ℝ M
Q : QuadraticForm ℝ M
w : Fin (finrank ℝ M) → SignType
hw :
  Equivalent (M₂ := Fin (finrank ℝ M) → ℝ) Q (weightedSumSquares (S := ℝ) ℝ fun (i : Fin (finrank ℝ M)) ↦ (↑(w i) : ℝ))
i : Fin (finrank ℝ M)
zero :
  ∀ (h : w i = SignType.zero),
    Eq (α := ℝ) ((fun (x : Fin (finrank ℝ M)) ↦ ((↑(w x) : ℝ) : ℝ)) i) (-1) ∨
      Eq (α := ℝ) ((fun (x : Fin (finrank ℝ M)) ↦ ((↑(w x) : ℝ) : ℝ)) i) 0 ∨
        Eq (α := ℝ) ((fun (x : Fin (finrank ℝ M)) ↦ ((↑(w x) : ℝ) : ℝ)) i) 1
neg :
  ∀ (h : w i = SignType.neg),
    Eq (α := ℝ) ((fun (x : Fin (finrank ℝ M)) ↦ ((↑(w x) : ℝ) : ℝ)) i) (-1) ∨
      Eq (α := ℝ) ((fun (x : Fin (finrank ℝ M)) ↦ ((↑(w x) : ℝ) : ℝ)) i) 0 ∨
        Eq (α := ℝ) ((fun (x : Fin (finrank ℝ M)) ↦ ((↑(w x) : ℝ) : ℝ)) i) 1
pos :
  ∀ (h : w i = SignType.pos),
    Eq (α := ℝ) ((fun (x : Fin (finrank ℝ M)) ↦ ((↑(w x) : ℝ) : ℝ)) i) (-1) ∨
      Eq (α := ℝ) ((fun (x : Fin (finrank ℝ M)) ↦ ((↑(w x) : ℝ) : ℝ)) i) 0 ∨
        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) 0 ∨
      Eq (α := ℝ) ((fun (x : Fin (finrank ℝ M)) ↦ ((↑(w x) : ℝ) : ℝ)) i) 1

Tactic:
cases h : 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
w : Fin (finrank ℝ M) → SignType
hw :
  Equivalent (M₂ := Fin (finrank ℝ M) → ℝ) Q (weightedSumSquares (S := ℝ) ℝ fun (i : Fin (finrank ℝ M)) ↦ (↑(w i) : ℝ))
i : Fin (finrank ℝ M)
h : w i = zero
⊢ Eq (α := ℝ) ((fun (x : Fin (finrank ℝ M)) ↦ ((↑(w x) : ℝ) : ℝ)) i) (-1) ∨
    Eq (α := ℝ) ((fun (x : Fin (finrank ℝ M)) ↦ ((↑(w x) : ℝ) : ℝ)) i) 0 ∨
      Eq (α := ℝ) ((fun (x : Fin (finrank ℝ M)) ↦ ((↑(w x) : ℝ) : ℝ)) i) 1

Tactic:
simp [h]
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Real
Goal:
M : Type u_2
inst : AddCommGroup M
inst_1 : Module ℝ M
inst_2 : FiniteDimensional ℝ M
Q : QuadraticForm ℝ M
w : Fin (finrank ℝ M) → SignType
hw :
  Equivalent (M₂ := Fin (finrank ℝ M) → ℝ) Q (weightedSumSquares (S := ℝ) ℝ fun (i : Fin (finrank ℝ M)) ↦ (↑(w i) : ℝ))
i : Fin (finrank ℝ M)
h : w i = neg
⊢ Eq (α := ℝ) ((fun (x : Fin (finrank ℝ M)) ↦ ((↑(w x) : ℝ) : ℝ)) i) (-1) ∨
    Eq (α := ℝ) ((fun (x : Fin (finrank ℝ M)) ↦ ((↑(w x) : ℝ) : ℝ)) i) 0 ∨
      Eq (α := ℝ) ((fun (x : Fin (finrank ℝ M)) ↦ ((↑(w x) : ℝ) : ℝ)) i) 1

Tactic:
simp [h]
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Real
Goal:
M : Type u_2
inst : AddCommGroup M
inst_1 : Module ℝ M
inst_2 : FiniteDimensional ℝ M
Q : QuadraticForm ℝ M
w : Fin (finrank ℝ M) → SignType
hw :
  Equivalent (M₂ := Fin (finrank ℝ M) → ℝ) Q (weightedSumSquares (S := ℝ) ℝ fun (i : Fin (finrank ℝ M)) ↦ (↑(w i) : ℝ))
i : Fin (finrank ℝ M)
h : w i = pos
⊢ Eq (α := ℝ) ((fun (x : Fin (finrank ℝ M)) ↦ ((↑(w x) : ℝ) : ℝ)) i) (-1) ∨
    Eq (α := ℝ) ((fun (x : Fin (finrank ℝ M)) ↦ ((↑(w x) : ℝ) : ℝ)) i) 0 ∨
      Eq (α := ℝ) ((fun (x : Fin (finrank ℝ M)) ↦ ((↑(w x) : ℝ) : ℝ)) i) 1

Tactic:
simp [h]
-- 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'
V : Submodule R M
e : IsometryEquiv Q Q'
⊢ PosDef (M := ↥(Submodule.map (↑e.toLinearEquiv : M →ₗ[R] M') V))
      (restrict Q' (Submodule.map (↑e.toLinearEquiv : M →ₗ[R] M') V)) ↔
    (restrict Q V).PosDef

Tactic:
simp [PosDef, -Submodule.mem_map_equiv]

Premises used: QuadraticMap.PosDef, Submodule.mem_map_equiv
-- 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'
V : Submodule R M
e : IsometryEquiv Q Q'
⊢ PosDef (M := ↥(Submodule.map (↑e.toLinearEquiv : M →ₗ[R] M') V))
      (restrict (-Q') (Submodule.map (↑e.toLinearEquiv : M →ₗ[R] M') V)) ↔
    (restrict (-Q) V).PosDef

Tactic:
simp [PosDef, -Submodule.mem_map_equiv]

Premises used: QuadraticMap.PosDef, Submodule.mem_map_equiv
-- 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'
V : Submodule R M
simp :
  Module.finrank.{u_1, u_2} R ↥⊥ ≤ Module.finrank R M ∧
    ∃ (V : Submodule R M),
      Module.finrank.{u_1, u_2} R ↥V = Module.finrank.{u_1, u_2} R ↥⊥ ∧ (QuadraticMap.restrict Q V).PosDef
⊢ Module.finrank.{u_1, u_2} R ↥⊥ ∈
    {r ∈ Iic (Module.finrank R M) |
      ∃ (V : Submodule R M), Module.finrank.{u_1, u_2} R ↥V = r ∧ (QuadraticMap.restrict Q V).PosDef}

Tactic:
simp only [mem_filter, mem_Iic]

Premises used: Finset.mem_Iic, Finset.mem_filter
-- 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'
V : Submodule R M
⊢ Module.finrank.{u_1, u_2} R ↥⊥ ≤ Module.finrank R M ∧
    ∃ (V : Submodule R M),
      Module.finrank.{u_1, u_2} R ↥V = Module.finrank.{u_1, u_2} R ↥⊥ ∧ (QuadraticMap.restrict Q V).PosDef

Tactic:
⟨?_, ⟨⊥, rfl, fun x hx' ↦ (hx' <| Subsingleton.elim x 0).elim⟩⟩

Premises used: False.elim, Bot.bot, And.intro, Exists.intro, Subsingleton.elim, OfNat.ofNat, rfl
-- 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'
V : Submodule R M
refine : Module.finrank.{u_1, u_2} R ↥⊥ ≤ Module.finrank R M
⊢ Module.finrank.{u_1, u_2} R ↥⊥ ≤ Module.finrank R M ∧
    ∃ (V : Submodule R M),
      Module.finrank.{u_1, u_2} R ↥V = Module.finrank.{u_1, u_2} R ↥⊥ ∧ (QuadraticMap.restrict Q V).PosDef

Tactic:
refine ⟨?_, ⟨⊥, rfl, fun x hx' ↦ (hx' <| Subsingleton.elim x 0).elim⟩⟩
-- 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'
V : Submodule R M
⊢ Nontrivial R

Tactic:
nontriviality R
-- 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'
V : Submodule R M
h : Nontrivial R
⊢ Module.finrank.{u_1, u_2} R ↥⊥ ≤ Module.finrank R M

Tactic:
simp [finrank_bot]

Premises used: finrank_bot
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Signature
Goal:
R : Type u_1
M : Type u_2
inst : AddCommGroup M
inst_1 : CommRing R
inst_2 : LinearOrder R
inst_3 : Module R M
Q : QuadraticForm R M
⊢ sigPos Q ≤ Module.finrank R M

Tactic:
mem_Iic.mp <| mem_of_mem_filter _ <| max'_mem _ _

Premises used: Finset.max'_mem, Finset.mem_Iic, Finset.mem_of_mem_filter, Iff.mp
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Signature
Goal:
R : Type u_1
M : Type u_2
inst : AddCommGroup M
inst_1 : CommRing R
inst_2 : LinearOrder R
inst_3 : Module R M
Q : QuadraticForm R M
⊢ sigPos Q ≤ Module.finrank R M

Tactic:
exact mem_Iic.mp <| mem_of_mem_filter _ <| max'_mem _ _

Premises used: Finset.max'_mem, Finset.mem_Iic, Finset.mem_of_mem_filter, Iff.mp
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Signature
Goal:
R : Type u_1
M : Type u_2
inst : AddCommGroup M
inst_1 : CommRing R
inst_2 : LinearOrder R
inst_3 : Module R M
Q : QuadraticForm R M
⊢ sigPos Q ≤ Module.finrank R M

Tactic:
classical
  exact mem_Iic.mp <| mem_of_mem_filter _ <| max'_mem _ _

Premises used: Finset.max'_mem, Finset.mem_Iic, Finset.mem_of_mem_filter, Iff.mp
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Signature
Goal:
R : Type u_1
M : Type u_2
inst : AddCommGroup M
inst_1 : CommRing R
inst_2 : LinearOrder R
inst_3 : Module R M
Q : QuadraticForm R M
inst_4 : Module.Finite R M
inst_5 : StrongRankCondition R
⊢ IsGreatest {r : ℕ | ∃ (V : Submodule R M), Module.finrank.{u_1, u_2} R ↥V = r ∧ (QuadraticMap.restrict Q V).PosDef}
    (sigPos Q)

Tactic:
⟨(mem_filter.mp <| max'_mem _ _).2, ?_⟩

Premises used: Finset.max'_mem, IsGreatest, And.right, And.intro, Iff.mp, Finset.mem_filter
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Signature
Goal:
R : Type u_1
M : Type u_2
inst : AddCommGroup M
inst_1 : CommRing R
inst_2 : LinearOrder R
inst_3 : Module R M
Q : QuadraticForm R M
inst_4 : Module.Finite R M
inst_5 : StrongRankCondition R
refine :
  Membership.mem (γ := Set ℕ)
    (upperBounds
      {r : ℕ | ∃ (V : Submodule R M), Module.finrank.{u_1, u_2} R ↥V = r ∧ (QuadraticMap.restrict Q V).PosDef})
    (sigPos Q)
⊢ IsGreatest {r : ℕ | ∃ (V : Submodule R M), Module.finrank.{u_1, u_2} R ↥V = r ∧ (QuadraticMap.restrict Q V).PosDef}
    (sigPos Q)

Tactic:
refine ⟨(mem_filter.mp <| max'_mem _ _).2, ?_⟩
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Signature
Goal:
R : Type u_1
M : Type u_2
inst : AddCommGroup M
inst_1 : CommRing R
inst_2 : LinearOrder R
inst_3 : Module R M
Q : QuadraticForm R M
inst_4 : Module.Finite R M
inst_5 : StrongRankCondition R
V : Submodule R M
hV : (QuadraticMap.restrict Q V).PosDef
H2 :
  Module.finrank.{u_1, u_2} R ↥V ∈
    {r ∈ Iic (Module.finrank R M) |
      ∃ (V : Submodule R M), Module.finrank.{u_1, u_2} R ↥V = r ∧ (QuadraticMap.restrict Q V).PosDef}
⊢ Module.finrank.{u_1, u_2} R ↥V ≤ sigPos Q

Tactic:
apply le_max'

Premises used: Finset.le_max'
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Signature
Goal:
R : Type u_1
M : Type u_2
inst : AddCommGroup M
inst_1 : CommRing R
inst_2 : LinearOrder R
inst_3 : Module R M
Q : QuadraticForm R M
inst_4 : Module.Finite R M
inst_5 : StrongRankCondition R
V : Submodule R M
hV : (QuadraticMap.restrict Q V).PosDef
H2 :
  Module.finrank.{u_1, u_2} R ↥V ≤ Module.finrank R M ∧
    ∃ (V_1 : Submodule R M),
      Module.finrank.{u_1, u_2} R ↥V_1 = Module.finrank.{u_1, u_2} R ↥V ∧ (QuadraticMap.restrict Q V_1).PosDef
⊢ Module.finrank.{u_1, u_2} R ↥V ∈
    {r ∈ Iic (Module.finrank R M) |
      ∃ (V : Submodule R M), Module.finrank.{u_1, u_2} R ↥V = r ∧ (QuadraticMap.restrict Q V).PosDef}

Tactic:
rw [mem_filter, mem_Iic]

Premises used: Finset.mem_Iic, Finset.mem_filter
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Signature
Goal:
R : Type u_1
M : Type u_2
inst : AddCommGroup M
inst_1 : CommRing R
inst_2 : LinearOrder R
inst_3 : Module R M
Q : QuadraticForm R M
inst_4 : Module.Finite R M
inst_5 : StrongRankCondition R
V : Submodule R M
hV : (QuadraticMap.restrict Q V).PosDef
⊢ Module.finrank.{u_1, u_2} R ↥V ≤ Module.finrank R M ∧
    ∃ (V_1 : Submodule R M),
      Module.finrank.{u_1, u_2} R ↥V_1 = Module.finrank.{u_1, u_2} R ↥V ∧ (QuadraticMap.restrict Q V_1).PosDef

Tactic:
⟨V.finrank_le, V, rfl, hV⟩

Premises used: And.intro, Exists.intro, Submodule.finrank_le, rfl
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Signature
Goal:
R : Type u_1
M : Type u_2
inst : AddCommGroup M
inst_1 : CommRing R
inst_2 : LinearOrder R
inst_3 : Module R M
Q : QuadraticForm R M
inst_4 : Module.Finite R M
inst_5 : StrongRankCondition R
V : Submodule R M
hV : (QuadraticMap.restrict Q V).PosDef
⊢ Module.finrank.{u_1, u_2} R ↥V ≤ Module.finrank R M ∧
    ∃ (V_1 : Submodule R M),
      Module.finrank.{u_1, u_2} R ↥V_1 = Module.finrank.{u_1, u_2} R ↥V ∧ (QuadraticMap.restrict Q V_1).PosDef

Tactic:
exact ⟨V.finrank_le, V, rfl, hV⟩
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Signature
Goal:
R : Type u_1
M : Type u_2
inst : AddCommGroup M
inst_1 : CommRing R
inst_2 : LinearOrder R
inst_3 : Module R M
Q : QuadraticForm R M
inst_4 : Module.Finite R M
inst_5 : StrongRankCondition R
refine :
  Membership.mem (γ := Set ℕ)
    (upperBounds
      {r : ℕ | ∃ (V : Submodule R M), Module.finrank.{u_1, u_2} R ↥V = r ∧ (QuadraticMap.restrict Q V).PosDef})
    (sigPos Q)
refine₁ : ∀ (V : Submodule R M) (hV : (QuadraticMap.restrict Q V).PosDef), Module.finrank.{u_1, u_2} R ↥V ≤ sigPos Q
H2 :
  ∀ (V : Submodule R M) (hV : (QuadraticMap.restrict Q V).PosDef),
    Module.finrank.{u_1, u_2} R ↥V ∈
      {r ∈ Iic (Module.finrank R M) |
        ∃ (V : Submodule R M), Module.finrank.{u_1, u_2} R ↥V = r ∧ (QuadraticMap.restrict Q V).PosDef}
H2₁ :
  ∀ (V : Submodule R M) (hV : (QuadraticMap.restrict Q V).PosDef),
    Module.finrank.{u_1, u_2} R ↥V ≤ Module.finrank R M ∧
      ∃ (V_1 : Submodule R M),
        Module.finrank.{u_1, u_2} R ↥V_1 = Module.finrank.{u_1, u_2} R ↥V ∧ (QuadraticMap.restrict Q V_1).PosDef
⊢ IsGreatest {r : ℕ | ∃ (V : Submodule R M), Module.finrank.{u_1, u_2} R ↥V = r ∧ (QuadraticMap.restrict Q V).PosDef}
    (sigPos Q)

Tactic:
classical
  refine ⟨(mem_filter.mp <| max'_mem _ _).2, ?_⟩
  rintro _ ⟨V, rfl, hV⟩
  apply le_max'
  rw [mem_filter, mem_Iic]
  exact ⟨V.finrank_le, V, rfl, hV⟩

Premises used: Finset.mem_Iic, Finset.le_max', Finset.mem_filter, rfl
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Signature
Goal:
R : Type u_1
M : Type u_2
inst : AddCommGroup M
inst_1 : CommRing R
inst_2 : LinearOrder R
inst_3 : Module R M
Q : QuadraticForm R M
inst_4 : Module.Finite R M
inst_5 : StrongRankCondition R
⊢ ∃ (V : Submodule R M), Module.finrank.{u_1, u_2} R ↥V = sigPos Q ∧ (QuadraticMap.restrict Q V).PosDef

Tactic:
(sigPos_isGreatest Q).1

Premises used: sigPos_isGreatest, Set.Mem, setOf, And.left
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Signature
Goal:
R : Type u_1
M : Type u_2
inst : AddCommGroup M
inst_1 : CommRing R
inst_2 : LinearOrder R
inst_3 : Module R M
Q : QuadraticForm R M
inst_4 : Module.Finite R M
inst_5 : StrongRankCondition R
V : Submodule R M
hV : (QuadraticMap.restrict Q V).PosDef
left : Module.finrank.{u_1, u_2} R ↥V = Module.finrank.{u_1, u_2} R ↥V
right : (QuadraticMap.restrict Q V).PosDef
left₁ left₂ left₃ left₄ : Module.finrank.{u_1, u_2} R ↥V = Module.finrank.{u_1, u_2} R ↥V
⊢ Module.finrank.{u_1, u_2} R ↥V = Module.finrank.{u_1, u_2} R ↥V ∧ (QuadraticMap.restrict Q V).PosDef

Tactic:
tauto
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Signature
Goal:
R : Type u_1
M : Type u_2
inst : AddCommGroup M
inst_1 : CommRing R
inst_2 : LinearOrder R
inst_3 : Module R M
Q : QuadraticForm R M
inst_4 : Module.Finite R M
inst_5 : StrongRankCondition R
⊢ IsGreatest {r : ℕ | ∃ (V : Submodule R M), Module.finrank.{u_1, u_2} R ↥V = r ∧ (QuadraticMap.restrict (-Q) V).PosDef}
    (sigNeg Q)

Tactic:
sigPos_isGreatest (-Q)

Premises used: sigPos_isGreatest, sigNeg, Neg.neg
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Signature
Goal:
R : Type u_1
M : Type u_2
inst : AddCommGroup M
inst_1 : CommRing R
inst_2 : LinearOrder R
inst_3 : Module R M
Q : QuadraticForm R M
inst_4 : Module.Finite R M
inst_5 : StrongRankCondition R
⊢ ∃ (V : Submodule R M), Module.finrank.{u_1, u_2} R ↥V = sigNeg Q ∧ (QuadraticMap.restrict (-Q) V).PosDef

Tactic:
exists_finrank_eq_sigPos_and_posDef (-Q)

Premises used: exists_finrank_eq_sigPos_and_posDef, sigNeg, Neg.neg
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Signature
Goal:
R : Type u_1
M : Type u_2
inst : AddCommGroup M
inst_1 : CommRing R
inst_2 : LinearOrder R
inst_3 : Module R M
Q : QuadraticForm R M
inst_4 : Module.Finite R M
inst_5 : StrongRankCondition R
V : Submodule R M
hV : (QuadraticMap.restrict (-Q) V).PosDef
⊢ Module.finrank.{u_1, u_2} R ↥V ≤ sigNeg Q

Tactic:
le_sigPos_of_posDef (-Q) hV

Premises used: le_sigPos_of_posDef, sigNeg, Neg.neg
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Signature
Goal:
R : Type u_1
M : Type u_2
inst : AddCommGroup M
inst_1 : CommRing R
inst_2 : LinearOrder R
inst_3 : Module R M
Q : QuadraticForm R M
⊢ sigPos (-Q) = sigNeg Q

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Signature
Goal:
R : Type u_1
M : Type u_2
inst : AddCommGroup M
inst_1 : CommRing R
inst_2 : LinearOrder R
inst_3 : Module R M
Q : QuadraticForm R M
rw : sigPos (- -Q) = sigPos Q
rw₁ rw₂ : sigPos Q = sigPos Q
⊢ sigNeg (-Q) = sigPos Q

Tactic:
rw [← sigPos_neg, neg_neg]

Premises used: neg_neg, sigPos_neg
-- 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'
obtain : ∀ (e : IsometryEquiv Q Q'), sigPos Q = sigPos Q'
⊢ sigPos Q = sigPos Q'

Tactic:
obtain ⟨e⟩ := h
-- 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'
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
h₁ : Module.finrank R M = Module.finrank R M'
⊢ {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'
      ⋯

Tactic:
congr! with 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'
j : ℕ
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))
⊢ (∃ (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

Tactic:
apply (Submodule.orderIsoMapComap e.toLinearEquiv).exists_congr

Premises used: Submodule.orderIsoMapComap, QuadraticMap.IsometryEquiv.toLinearEquiv, RelIso.toEquiv, Equiv.exists_congr
-- 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
⊢ 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:
.and ?_ (IsometryEquiv.map_posDef_iff _).symm

Premises used: QuadraticMap.IsometryEquiv.map_posDef_iff, Iff.and, Iff.symm