awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Real (goal)
Goal:
ι : Type u_1
inst : Fintype ι
w : ι → ℝ
u : (i : ι) → ℝˣ := fun (i : ι) ↦ if h : w i = 0 then 1 else Units.mk0 (w i) h
hu : ∀ (i : ι), 1 / √|(↑(u i) : ℝ)| ≠ 0
i : ι
⊢ w i / |(↑(u i) : ℝ)| = (↑((sign : (a : ℝ) → SignType) (w i)) : ℝ)
have pos : ∀ (hi : w i = 0), w i / |(↑(u i) : ℝ)| = (↑((sign : (a : ℝ) → SignType) (w i)) : ℝ)
Tactic: by_cases hi : w i = 0
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Real (goal)
Goal:
ι : Type u_1
inst : Fintype ι
w : ι → ℝ
u : (i : ι) → ℝˣ := fun (i : ι) ↦ if h : w i = 0 then 1 else Units.mk0 (w i) h
hu : ∀ (i : ι), 1 / √|(↑(u i) : ℝ)| ≠ 0
i : ι
pos : ∀ (hi : w i = 0), w i / |(↑(u i) : ℝ)| = (↑((sign : (a : ℝ) → SignType) (w i)) : ℝ)
⊢ w i / |(↑(u i) : ℝ)| = (↑((sign : (a : ℝ) → SignType) (w i)) : ℝ)
have neg : ∀ (hi : ¬w i = 0), w i / |(↑(u i) : ℝ)| = (↑((sign : (a : ℝ) → SignType) (w i)) : ℝ)
Tactic: by_cases hi : w i = 0
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Real (goal)
Goal:
ι : Type u_1
inst : Fintype ι
w : ι → ℝ
u : (i : ι) → ℝˣ := fun (i : ι) ↦ if h : w i = 0 then 1 else Units.mk0 (w i) h
hu : ∀ (i : ι), 1 / √|(↑(u i) : ℝ)| ≠ 0
i : ι
hi : ¬w i = 0
⊢ w i / |(↑(u i) : ℝ)| = (↑((sign : (a : ℝ) → SignType) (w i)) : ℝ)
have neg : w i / |w i| = (↑((sign : (a : ℝ) → SignType) (w i)) : ℝ)
Tactic: simp only [hi, ↓reduceDIte, Units.val_mk0, u]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Real (goal)
Goal:
ι : Type u_1
inst : Fintype ι
w : ι → ℝ
u : (i : ι) → ℝˣ := fun (i : ι) ↦ if h : w i = 0 then 1 else Units.mk0 (w i) h
hu : ∀ (i : ι), 1 / √|(↑(u i) : ℝ)| ≠ 0
i : ι
hi : ¬w i = 0
⊢ w i / |w i| = (↑((sign : (a : ℝ) → SignType) (w i)) : ℝ)
have neg : w i = |w i| * (↑((sign : (a : ℝ) → SignType) (w i)) : ℝ)
Tactic: field_simp
-- 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
hu : ∀ (i : ι), 1 / √|(↑(u i) : ℝ)| ≠ 0
⊢ QuadraticMap.IsometryEquiv (M₂ := ι → ℝ) (weightedSumSquares ℝ w)
    (weightedSumSquares (S := ℝ) ℝ fun (i : ι) ↦ (↑((sign : (a : ℝ) → SignType) (w i)) : ℝ))
have hwu : ∀ (i : ι), w i / |(↑(u i) : ℝ)| = (↑((sign : (a : ℝ) → SignType) (w i)) : ℝ)
Tactic: have hwu : ∀ i, w i / |(u i : ℝ)| = sign (w i) := fun i ↦ by
    by_cases hi : w i = 0
    · simp [hi]
    · simp only [hi, ↓reduceDIte, Units.val_mk0, u]; field_simp; simp
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Real (goal)
Goal:
ι : Type u_1
inst : Fintype ι
w : ι → ℝ
u : (i : ι) → ℝˣ := fun (i : ι) ↦ if h : w i = 0 then 1 else Units.mk0 (w i) h
hu : ∀ (i : ι), 1 / √|(↑(u i) : ℝ)| ≠ 0
hwu : ∀ (i : ι), w i / |(↑(u i) : ℝ)| = (↑((sign : (a : ℝ) → SignType) (w i)) : ℝ)
⊢ QuadraticMap.IsometryEquiv (M₂ := ι → ℝ) (weightedSumSquares ℝ w)
    (weightedSumSquares (S := ℝ) ℝ fun (i : ι) ↦ (↑((sign : (a : ℝ) → SignType) (w i)) : ℝ))
have h : (weightedSumSquares (S := ℝ) ℝ fun (i : ι) ↦ (↑((sign : (a : ℝ) → SignType) (w i)) : ℝ)) =
  basisRepr (weightedSumSquares ℝ w) (Basis.unitsSMul (Pi.basisFun ℝ ι) fun (i : ι) ↦ Units.mk0 (1 / √|(↑(u i) : ℝ)|) sorry)
Tactic: convert!
    QuadraticMap.isometryEquivBasisRepr (weightedSumSquares ℝ w)
      ((Pi.basisFun ℝ ι).unitsSMul fun i => .mk0 _ (hu i))
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Real (goal)
Goal:
ι : Type u_1
inst : Fintype ι
w : ι → ℝ
u : (i : ι) → ℝˣ := fun (i : ι) ↦ if h : w i = 0 then 1 else Units.mk0 (w i) h
hu : ∀ (i : ι), 1 / √|(↑(u i) : ℝ)| ≠ 0
hwu : ∀ (i : ι), w i / |(↑(u i) : ℝ)| = (↑((sign : (a : ℝ) → SignType) (w i)) : ℝ)
⊢ (weightedSumSquares (S := ℝ) ℝ fun (i : ι) ↦ (↑((sign : (a : ℝ) → SignType) (w i)) : ℝ)) =
    basisRepr (weightedSumSquares ℝ w)
      (Basis.unitsSMul (Pi.basisFun ℝ ι) fun (i : ι) ↦ Units.mk0 (1 / √|(↑(u i) : ℝ)|) ⋯)
have h : ∀ (v : ι → ℝ),
  Eq (α := ℝ)
    ((weightedSumSquares (S := ℝ) ℝ fun (i : ι) ↦ (↑((sign : (a : ℝ) → SignType) (w i)) : ℝ) : (a : ι → ℝ) → ℝ) v : ℝ)
    ((basisRepr (weightedSumSquares ℝ w)
            (Basis.unitsSMul (Pi.basisFun ℝ ι) fun (i : ι) ↦ Units.mk0 (1 / √|(↑(u i) : ℝ)|) sorry) :
          (a : ι → ℝ) → ℝ)
        v :
      ℝ)
Tactic: ext1 v
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Real (goal)
Goal:
ι : Type u_1
inst : Fintype ι
w : ι → ℝ
u : (i : ι) → ℝˣ := fun (i : ι) ↦ if h : w i = 0 then 1 else Units.mk0 (w i) h
hu : ∀ (i : ι), 1 / √|(↑(u i) : ℝ)| ≠ 0
hwu : ∀ (i : ι), w i / |(↑(u i) : ℝ)| = (↑((sign : (a : ℝ) → SignType) (w i)) : ℝ)
v : ι → ℝ
⊢ Eq (α := ℝ)
    ((weightedSumSquares (S := ℝ) ℝ fun (i : ι) ↦ (↑((sign : (a : ℝ) → SignType) (w i)) : ℝ) : (a : ι → ℝ) → ℝ) v : ℝ)
    ((basisRepr (weightedSumSquares ℝ w)
            (Basis.unitsSMul (Pi.basisFun ℝ ι) fun (i : ι) ↦ Units.mk0 (1 / √|(↑(u i) : ℝ)|) ⋯) :
          (a : ι → ℝ) → ℝ)
        v :
      ℝ)
have h : Eq (α := ℝ) (∑ i : ι, w i / |(↑(u i) : ℝ)| * HPow.hPow (β := ℕ) (v i) 2)
  (∑ i : ι, w i * (HPow.hPow (β := ℕ) (v i) 2 * |(↑(u i) : ℝ)|⁻¹))
Tactic: suffices ∑ i, (w i / |(u i : ℝ)|) * v i ^ 2 = ∑ i, w i * (v i ^ 2 * |(u i : ℝ)|⁻¹) by
    simpa [basisRepr_apply, Basis.unitsSMul_apply, ← _root_.sq, mul_pow, ← hwu, Pi.single_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Real (goal)
Goal:
ι : Type u_1
inst : Fintype ι
w : ι → ℝ
u : (i : ι) → ℝˣ := fun (i : ι) ↦ if h : w i = 0 then 1 else Units.mk0 (w i) h
hu : ∀ (i : ι), 1 / √|(↑(u i) : ℝ)| ≠ 0
hwu : ∀ (i : ι), w i / |(↑(u i) : ℝ)| = (↑((sign : (a : ℝ) → SignType) (w i)) : ℝ)
v : ι → ℝ
⊢ Eq (α := ℝ)
    ((weightedSumSquares (S := ℝ) ℝ fun (i : ι) ↦ (↑((sign : (a : ℝ) → SignType) (w i)) : ℝ) : (a : ι → ℝ) → ℝ) v : ℝ)
    ((basisRepr (weightedSumSquares ℝ w)
            (Basis.unitsSMul (Pi.basisFun ℝ ι) fun (i : ι) ↦ Units.mk0 (1 / √|(↑(u i) : ℝ)|) ⋯) :
          (a : ι → ℝ) → ℝ)
        v :
      ℝ)
have h : Eq (α := ℝ) (∑ i : ι, w i / |(↑(u i) : ℝ)| * HPow.hPow (β := ℕ) (v i) 2)
  (∑ i : ι, w i * (HPow.hPow (β := ℕ) (v i) 2 * |(↑(u i) : ℝ)|⁻¹))
Tactic: classical
  suffices ∑ i, (w i / |(u i : ℝ)|) * v i ^ 2 = ∑ i, w i * (v i ^ 2 * |(u i : ℝ)|⁻¹) by
    simpa [basisRepr_apply, Basis.unitsSMul_apply, ← _root_.sq, mul_pow, ← hwu, Pi.single_apply]
  exact sum_congr rfl fun j _ ↦ by ring
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Real (goal)
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)
⊢ Eq (α := ℝ) ((fun (x : Fin (finrank ℝ M)) ↦ ((↑(w x) : ℝ) : ℝ)) i) (-1) ∨
    Eq (α := ℝ) ((fun (x : Fin (finrank ℝ M)) ↦ ((↑(w x) : ℝ) : ℝ)) i) 1
have zero : ∀ (hi : w i = zero),
  Eq (α := ℝ) ((fun (x : Fin (finrank ℝ M)) ↦ ((↑(w x) : ℝ) : ℝ)) i) (-1) ∨
    Eq (α := ℝ) ((fun (x : Fin (finrank ℝ M)) ↦ ((↑(w x) : ℝ) : ℝ)) i) 1
Tactic: cases hi : w i
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Real (goal)
Goal:
M : Type u_2
inst : AddCommGroup M
inst_1 : Module ℝ M
inst_2 : FiniteDimensional ℝ M
Q : QuadraticForm ℝ M
hQ :
  LinearMap.SeparatingLeft.{0, 0, 0, 0, u_2, u_2} (R := ℝ) (R₁ := ℝ) (R₂ := ℝ) (M := ℝ) (M₁ := M) (M₂ := M) (I₁ :=
    RingHom.id ℝ) (I₂ := RingHom.id ℝ) ((associated : (a : QuadraticMap ℝ M ℝ) → LinearMap.BilinMap ℝ M ℝ) Q)
w : Fin (finrank ℝ M) → SignType
hw₀ : ∀ (i : Fin (finrank ℝ M)), w i ≠ 0
hw :
  Equivalent (M₂ := Fin (finrank ℝ M) → ℝ) Q (weightedSumSquares (S := ℝ) ℝ fun (i : Fin (finrank ℝ M)) ↦ (↑(w i) : ℝ))
i : Fin (finrank ℝ M)
zero :
  ∀ (hi : w i = SignType.zero),
    Eq (α := ℝ) ((fun (x : Fin (finrank ℝ M)) ↦ ((↑(w x) : ℝ) : ℝ)) i) (-1) ∨
      Eq (α := ℝ) ((fun (x : Fin (finrank ℝ M)) ↦ ((↑(w x) : ℝ) : ℝ)) i) 1
⊢ Eq (α := ℝ) ((fun (x : Fin (finrank ℝ M)) ↦ ((↑(w x) : ℝ) : ℝ)) i) (-1) ∨
    Eq (α := ℝ) ((fun (x : Fin (finrank ℝ M)) ↦ ((↑(w x) : ℝ) : ℝ)) i) 1
have neg : ∀ (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: cases hi : w i
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Real (goal)
Goal:
M : Type u_2
inst : AddCommGroup M
inst_1 : Module ℝ M
inst_2 : FiniteDimensional ℝ M
Q : QuadraticForm ℝ M
hQ :
  LinearMap.SeparatingLeft.{0, 0, 0, 0, u_2, u_2} (R := ℝ) (R₁ := ℝ) (R₂ := ℝ) (M := ℝ) (M₁ := M) (M₂ := M) (I₁ :=
    RingHom.id ℝ) (I₂ := RingHom.id ℝ) ((associated : (a : QuadraticMap ℝ M ℝ) → LinearMap.BilinMap ℝ M ℝ) Q)
w : Fin (finrank ℝ M) → SignType
hw₀ : ∀ (i : Fin (finrank ℝ M)), w i ≠ 0
hw :
  Equivalent (M₂ := Fin (finrank ℝ M) → ℝ) Q (weightedSumSquares (S := ℝ) ℝ fun (i : Fin (finrank ℝ M)) ↦ (↑(w i) : ℝ))
i : Fin (finrank ℝ M)
zero :
  ∀ (hi : w i = SignType.zero),
    Eq (α := ℝ) ((fun (x : Fin (finrank ℝ M)) ↦ ((↑(w x) : ℝ) : ℝ)) i) (-1) ∨
      Eq (α := ℝ) ((fun (x : Fin (finrank ℝ M)) ↦ ((↑(w x) : ℝ) : ℝ)) i) 1
neg :
  ∀ (hi : w i = SignType.neg),
    Eq (α := ℝ) ((fun (x : Fin (finrank ℝ M)) ↦ ((↑(w x) : ℝ) : ℝ)) i) (-1) ∨
      Eq (α := ℝ) ((fun (x : Fin (finrank ℝ M)) ↦ ((↑(w x) : ℝ) : ℝ)) i) 1
⊢ Eq (α := ℝ) ((fun (x : Fin (finrank ℝ M)) ↦ ((↑(w x) : ℝ) : ℝ)) i) (-1) ∨
    Eq (α := ℝ) ((fun (x : Fin (finrank ℝ M)) ↦ ((↑(w x) : ℝ) : ℝ)) i) 1
have pos : ∀ (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: cases hi : w i
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Real (goal)
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)
⊢ 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
have zero : ∀ (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: cases h : w i
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Real (goal)
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
⊢ 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
have neg : ∀ (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: cases h : w i
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Real (goal)
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
⊢ 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
have pos : ∀ (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: cases h : w i
-- 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'
V : Submodule R M
⊢ 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}
have 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
Tactic: simp only [mem_filter, mem_Iic]
-- 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'
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
have refine : Module.finrank.{u_1, u_2} R ↥⊥ ≤ Module.finrank R M
Tactic: refine ⟨?_, ⟨⊥, rfl, fun x hx' ↦ (hx' <| Subsingleton.elim x 0).elim⟩⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Signature (hypothesis)
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
have a : Nontrivial R
Tactic: nontriviality R
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Signature (goal)
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)
have 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)
Tactic: refine ⟨(mem_filter.mp <| max'_mem _ _).2, ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Signature (goal)
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 ≤ sigPos Q
have 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}
Tactic: apply le_max'
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Signature (goal)
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 ∈
    {r ∈ Iic (Module.finrank R M) |
      ∃ (V : Submodule R M), Module.finrank.{u_1, u_2} R ↥V = r ∧ (QuadraticMap.restrict Q V).PosDef}
have 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
Tactic: rw [mem_filter, mem_Iic]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Signature (goal)
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)
have 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)
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⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Signature (goal)
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)
have refine₁ : ∀ (V : Submodule R M) (hV : (QuadraticMap.restrict Q V).PosDef), Module.finrank.{u_1, u_2} R ↥V ≤ 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⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Signature (goal)
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
⊢ IsGreatest {r : ℕ | ∃ (V : Submodule R M), Module.finrank.{u_1, u_2} R ↥V = r ∧ (QuadraticMap.restrict Q V).PosDef}
    (sigPos Q)
have 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}
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⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Signature (goal)
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}
⊢ IsGreatest {r : ℕ | ∃ (V : Submodule R M), Module.finrank.{u_1, u_2} R ↥V = r ∧ (QuadraticMap.restrict Q V).PosDef}
    (sigPos Q)
have 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
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⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Signature (goal)
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.{u_1, u_2} R ↥V ∧ (QuadraticMap.restrict Q V).PosDef
have left : Module.finrank.{u_1, u_2} R ↥V = Module.finrank.{u_1, u_2} R ↥V
Tactic: tauto
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Signature (goal)
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
⊢ sigNeg (-Q) = sigPos Q
have rw : sigPos (- -Q) = sigPos Q
Tactic: rw [← sigPos_neg, neg_neg]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Signature (goal)
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
⊢ sigNeg (-Q) = sigPos Q
have rw₁ : sigPos Q = sigPos Q
Tactic: rw [← sigPos_neg, neg_neg]
-- 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'
h : Equivalent Q Q'
⊢ sigPos Q = sigPos Q'
have obtain : ∀ (e : IsometryEquiv Q Q'), sigPos Q = sigPos Q'
Tactic: obtain ⟨e⟩ := h
Cleared hypotheses: h
-- 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'
⊢ {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 : ∀ (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
Tactic: congr! with j