awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basic (goal)
Goal:
R : Type u_3
M : Type u_4
N : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
Q : QuadraticMap R M N
inst_5 : Invertible (α := R) 2
x y : M
simp_rw :
  LinearMap.IsOrtho.{u_3, u_3, u_3, u_5, u_4, u_4} (R := R) (R₁ := R) (R₂ := R) (M := N) (I₁ := RingHom.id R) (I₂ :=
      RingHom.id R) ((associated : (a : QuadraticMap R M N) → BilinMap R M N) Q) x y ↔
    (Q : (a : M) → N) (x + y) = HAdd.hAdd (α := N) (β := N) ((Q : (a : M) → N) x : N) ((Q : (a : M) → N) y : N)
simp_rw₁ :
  Eq.{u_5 + 1} (α := N)
      ((((((associated : (a : QuadraticMap R M N) → BilinMap R M N) Q : BilinMap R M N) : (a : M) → M →ₗ[R] N) x :
              M →ₗ[R] N) :
            (a : M) → N)
          y :
        N)
      (0 : N) ↔
    (Q : (a : M) → N) (x + y) = HAdd.hAdd (α := N) (β := N) ((Q : (a : M) → N) x : N) ((Q : (a : M) → N) y : N)
simp_rw₂ :
  HSMul.hSMul (α := Module.End R N) (@Invertible.invOf _ Module.End.instMul Module.End.instOne 2 _)
        (HSub.hSub (β := N) (HSub.hSub (α := N) (β := N) ((Q : (a : M) → N) (x + y) : N) ((Q : (a : M) → N) x : N))
          ((Q : (a : M) → N) y : N)) =
      0 ↔
    (Q : (a : M) → N) (x + y) = HAdd.hAdd (α := N) (β := N) ((Q : (a : M) → N) x : N) ((Q : (a : M) → N) y : N)
simp_rw₃ :
  HSub.hSub (β := N) (HSub.hSub (α := N) (β := N) ((Q : (a : M) → N) (x + y) : N) ((Q : (a : M) → N) x : N))
        ((Q : (a : M) → N) y : N) =
      HSMul.hSMul (α := Module.End R N) (β := N) 2 0 ↔
    (Q : (a : M) → N) (x + y) = HAdd.hAdd (α := N) (β := N) ((Q : (a : M) → N) x : N) ((Q : (a : M) → N) y : N)
⊢ LinearMap.IsOrtho.{u_3, u_3, u_3, u_5, u_4, u_4} (R := R) (R₁ := R) (R₂ := R) (M := N) (I₁ := RingHom.id R) (I₂ :=
      RingHom.id R) ((associated : (a : QuadraticMap R M N) → BilinMap R M N) Q) x y ↔
    Q.IsOrtho x y
have simp_rw₄ : HSub.hSub (β := N) (HSub.hSub (α := N) (β := N) ((Q : (a : M) → N) (x + y) : N) ((Q : (a : M) → N) x : N))
      ((Q : (a : M) → N) y : N) =
    0 ↔
  (Q : (a : M) → N) (x + y) = HAdd.hAdd (α := N) (β := N) ((Q : (a : M) → N) x : N) ((Q : (a : M) → N) y : N)
Tactic: simp_rw [isOrtho_def, LinearMap.isOrtho_def, associated_apply, invOf_smul_eq_iff,
    smul_zero, sub_sub, sub_eq_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basic (goal)
Goal:
R : Type u_3
M : Type u_4
N : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
Q : QuadraticMap R M N
inst_5 : Invertible (α := R) 2
x y : M
simp_rw :
  LinearMap.IsOrtho.{u_3, u_3, u_3, u_5, u_4, u_4} (R := R) (R₁ := R) (R₂ := R) (M := N) (I₁ := RingHom.id R) (I₂ :=
      RingHom.id R) ((associated : (a : QuadraticMap R M N) → BilinMap R M N) Q) x y ↔
    (Q : (a : M) → N) (x + y) = HAdd.hAdd (α := N) (β := N) ((Q : (a : M) → N) x : N) ((Q : (a : M) → N) y : N)
simp_rw₁ :
  Eq.{u_5 + 1} (α := N)
      ((((((associated : (a : QuadraticMap R M N) → BilinMap R M N) Q : BilinMap R M N) : (a : M) → M →ₗ[R] N) x :
              M →ₗ[R] N) :
            (a : M) → N)
          y :
        N)
      (0 : N) ↔
    (Q : (a : M) → N) (x + y) = HAdd.hAdd (α := N) (β := N) ((Q : (a : M) → N) x : N) ((Q : (a : M) → N) y : N)
simp_rw₂ :
  HSMul.hSMul (α := Module.End R N) (@Invertible.invOf _ Module.End.instMul Module.End.instOne 2 _)
        (HSub.hSub (β := N) (HSub.hSub (α := N) (β := N) ((Q : (a : M) → N) (x + y) : N) ((Q : (a : M) → N) x : N))
          ((Q : (a : M) → N) y : N)) =
      0 ↔
    (Q : (a : M) → N) (x + y) = HAdd.hAdd (α := N) (β := N) ((Q : (a : M) → N) x : N) ((Q : (a : M) → N) y : N)
simp_rw₃ :
  HSub.hSub (β := N) (HSub.hSub (α := N) (β := N) ((Q : (a : M) → N) (x + y) : N) ((Q : (a : M) → N) x : N))
        ((Q : (a : M) → N) y : N) =
      HSMul.hSMul (α := Module.End R N) (β := N) 2 0 ↔
    (Q : (a : M) → N) (x + y) = HAdd.hAdd (α := N) (β := N) ((Q : (a : M) → N) x : N) ((Q : (a : M) → N) y : N)
simp_rw₄ :
  HSub.hSub (β := N) (HSub.hSub (α := N) (β := N) ((Q : (a : M) → N) (x + y) : N) ((Q : (a : M) → N) x : N))
        ((Q : (a : M) → N) y : N) =
      0 ↔
    (Q : (a : M) → N) (x + y) = HAdd.hAdd (α := N) (β := N) ((Q : (a : M) → N) x : N) ((Q : (a : M) → N) y : N)
⊢ LinearMap.IsOrtho.{u_3, u_3, u_3, u_5, u_4, u_4} (R := R) (R₁ := R) (R₂ := R) (M := N) (I₁ := RingHom.id R) (I₂ :=
      RingHom.id R) ((associated : (a : QuadraticMap R M N) → BilinMap R M N) Q) x y ↔
    Q.IsOrtho x y
have simp_rw₅ : HSub.hSub (α := N) ((Q : (a : M) → N) (x + y) : N)
      (HAdd.hAdd (α := N) (β := N) ((Q : (a : M) → N) x : N) ((Q : (a : M) → N) y : N)) =
    0 ↔
  (Q : (a : M) → N) (x + y) = HAdd.hAdd (α := N) (β := N) ((Q : (a : M) → N) x : N) ((Q : (a : M) → N) y : N)
Tactic: simp_rw [isOrtho_def, LinearMap.isOrtho_def, associated_apply, invOf_smul_eq_iff,
    smul_zero, sub_sub, sub_eq_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basic (goal)
Goal:
R : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Invertible (α := R) 2
Q : QuadraticMap R M R
hB : Q.Anisotropic
x : M
hx :
  ∀ (y : M),
    Eq.{u_3 + 1} (α := R)
      (((((((associated'.{u_3, u_4, u_3} (R := R) (M := M) (N := R) : QuadraticMap R M R →ₗ[ℤ] BilinMap R M R) :
                        (a : QuadraticMap R M R) → BilinMap R M R)
                      Q :
                    BilinMap R M R) :
                  (a : M) → M →ₗ[R] R)
                x :
              M →ₗ[R] R) :
            (a : M) → R)
          y :
        R)
      (0 : R)
⊢ Eq.{u_3 + 1} (α := R) ((Q : (a : M) → R) x : R) (0 : R)
have rw : Eq.{u_3 + 1} (α := R) ((Q : (a : M) → R) x : R)
  (((((((associated'.{u_3, u_4, u_3} (R := R) (M := M) (N := R) : QuadraticMap R M R →ₗ[ℤ] BilinMap R M R) :
                    (a : QuadraticMap R M R) → BilinMap R M R)
                  Q :
                BilinMap R M R) :
              (a : M) → M →ₗ[R] R)
            x :
          M →ₗ[R] R) :
        (a : M) → R)
      x :
    R)
Tactic: rw [← hx x]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basic (hypothesis)
Goal:
M : Type u_4
N : Type u_5
R₂ : Type u
inst : CommSemiring R₂
inst_1 : AddCommMonoid M
inst_2 : Module R₂ M
inst_3 : PartialOrder N
inst_4 : AddCommMonoid N
inst_5 : Module R₂ N
Q : QuadraticMap R₂ M N
hQ : Q.PosDef
x : M
hQx : Eq.{u_5 + 1} (α := N) ((Q : (a : M) → N) x : N) (0 : N)
hx : ¬x = 0
⊢ LT.lt.{u_5} (α := N) 0 0
have this : LT.lt.{u_5} (α := N) (0 : N) ((Q : (a : M) → N) x : N)
Tactic: have := hQ _ hx
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basic (goal)
Goal:
M : Type u_4
N : Type u_5
R₂ : Type u
inst : CommSemiring R₂
inst_1 : AddCommMonoid M
inst_2 : Module R₂ M
inst_3 : PartialOrder N
inst_4 : AddCommMonoid N
inst_5 : Module R₂ N
Q : QuadraticMap R₂ M N
hQ : Q.PosDef
x : M
⊢ LE.le.{u_5} (α := N) ((Q : (a : M) → N) x : N) (0 : N) ↔ x = 0
have refine : ∀ (h : LE.le.{u_5} (α := N) ((Q : (a : M) → N) x : N) (0 : N)), x = 0
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ by simp [h]⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basic (hypothesis)
Goal:
M : Type u_4
N : Type u_5
R₂ : Type u
inst : CommSemiring R₂
inst_1 : AddCommMonoid M
inst_2 : Module R₂ M
inst_3 : PartialOrder N
inst_4 : AddCommMonoid N
inst_5 : Module R₂ N
Q : QuadraticMap R₂ M N
hQ : Q.PosDef
x : M
h : LE.le.{u_5} (α := N) ((Q : (a : M) → N) x : N) (0 : N)
⊢ x = 0
have this : Eq.{u_5 + 1} (α := N) ((Q : (a : M) → N) x : N) (0 : N)
Tactic: have : Q x = 0 := le_antisymm h (hQ.nonneg x)
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basic (goal)
Goal:
M : Type u_4
N : Type u_5
R₂ : Type u
inst : CommSemiring R₂
inst_1 : AddCommMonoid M
inst_2 : Module R₂ M
inst_3 : PartialOrder N
inst_4 : AddCommMonoid N
inst_5 : Module R₂ N
Q : QuadraticMap R₂ M N
hQ : Q.PosDef
x : M
h : LE.le.{u_5} (α := N) ((Q : (a : M) → N) x : N) (0 : N)
this : Eq.{u_5 + 1} (α := N) ((Q : (a : M) → N) x : N) (0 : N)
⊢ x = 0
have rwa : x = x
Tactic: rwa [← hQ.anisotropic]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basic (goal)
Goal:
R : Type u_3
n : Type w
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing R
inst_3 : Invertible (α := R) 2
Q : QuadraticForm R (n → R)
⊢ Q.toMatrix'.IsSymm
have a : ∀ (i j : n), Q.toMatrix'.transpose i j = Q.toMatrix' i j
Tactic: ext i j
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basic (goal)
Goal:
R : Type u_3
n : Type w
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing R
inst_3 : Invertible (α := R) 2
Q : QuadraticForm R (n → R)
i j : n
⊢ Q.toMatrix'.transpose i j = Q.toMatrix' i j
have a : Eq.{u_3 + 1} (α := R)
  (Matrix.transpose
      (((LinearMap.toMatrix₂' R : ((n → R) →ₗ[R] (n → R) →ₗ[R] R) ≃ₗ[R] Matrix n n R) :
          (a : (n → R) →ₗ[R] (n → R) →ₗ[R] R) → Matrix n n R)
        (((QuadraticMap.associated (R := R) (M := n → R) (N := R) :
              QuadraticMap R (n → R) R →ₗ[R] BilinMap R (n → R) R) :
            (a : QuadraticMap R (n → R) R) → BilinMap R (n → R) R)
          Q))
      i j :
    R)
  (((LinearMap.toMatrix₂' R : ((n → R) →ₗ[R] (n → R) →ₗ[R] R) ≃ₗ[R] Matrix n n R) :
        (a : (n → R) →ₗ[R] (n → R) →ₗ[R] R) → Matrix n n R)
      (((QuadraticMap.associated (R := R) (M := n → R) (N := R) : QuadraticMap R (n → R) R →ₗ[R] BilinMap R (n → R) R) :
          (a : QuadraticMap R (n → R) R) → BilinMap R (n → R) R)
        Q)
      i j :
    R)
Tactic: rw [toMatrix', Matrix.transpose_apply, LinearMap.toMatrix₂'_apply, LinearMap.toMatrix₂'_apply,
    ← QuadraticMap.associated_isSymm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basic (goal)
Goal:
R : Type u_3
n : Type w
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing R
inst_3 : Invertible (α := R) 2
Q : QuadraticForm R (n → R)
i j : n
a :
  Eq.{u_3 + 1} (α := R)
    (Matrix.transpose
        (((LinearMap.toMatrix₂' R : ((n → R) →ₗ[R] (n → R) →ₗ[R] R) ≃ₗ[R] Matrix n n R) :
            (a : (n → R) →ₗ[R] (n → R) →ₗ[R] R) → Matrix n n R)
          (((QuadraticMap.associated (R := R) (M := n → R) (N := R) :
                QuadraticMap R (n → R) R →ₗ[R] BilinMap R (n → R) R) :
              (a : QuadraticMap R (n → R) R) → BilinMap R (n → R) R)
            Q))
        i j :
      R)
    (((LinearMap.toMatrix₂' R : ((n → R) →ₗ[R] (n → R) →ₗ[R] R) ≃ₗ[R] Matrix n n R) :
          (a : (n → R) →ₗ[R] (n → R) →ₗ[R] R) → Matrix n n R)
        (((QuadraticMap.associated (R := R) (M := n → R) (N := R) :
              QuadraticMap R (n → R) R →ₗ[R] BilinMap R (n → R) R) :
            (a : QuadraticMap R (n → R) R) → BilinMap R (n → R) R)
          Q)
        i j :
      R)
⊢ Q.toMatrix'.transpose i j = Q.toMatrix' i j
have a₁ : Eq.{u_3 + 1} (α := R)
  (((LinearMap.toMatrix₂' R : ((n → R) →ₗ[R] (n → R) →ₗ[R] R) ≃ₗ[R] Matrix n n R) :
        (a : (n → R) →ₗ[R] (n → R) →ₗ[R] R) → Matrix n n R)
      (((QuadraticMap.associated (R := R) (M := n → R) (N := R) : QuadraticMap R (n → R) R →ₗ[R] BilinMap R (n → R) R) :
          (a : QuadraticMap R (n → R) R) → BilinMap R (n → R) R)
        Q)
      j i :
    R)
  (((LinearMap.toMatrix₂' R : ((n → R) →ₗ[R] (n → R) →ₗ[R] R) ≃ₗ[R] Matrix n n R) :
        (a : (n → R) →ₗ[R] (n → R) →ₗ[R] R) → Matrix n n R)
      (((QuadraticMap.associated (R := R) (M := n → R) (N := R) : QuadraticMap R (n → R) R →ₗ[R] BilinMap R (n → R) R) :
          (a : QuadraticMap R (n → R) R) → BilinMap R (n → R) R)
        Q)
      i j :
    R)
Tactic: rw [toMatrix', Matrix.transpose_apply, LinearMap.toMatrix₂'_apply, LinearMap.toMatrix₂'_apply,
    ← QuadraticMap.associated_isSymm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basic (goal)
Goal:
R : Type u_3
n : Type w
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing R
inst_3 : Invertible (α := R) 2
Q : QuadraticForm R (n → R)
i j : n
a :
  Eq.{u_3 + 1} (α := R)
    (Matrix.transpose
        (((LinearMap.toMatrix₂' R : ((n → R) →ₗ[R] (n → R) →ₗ[R] R) ≃ₗ[R] Matrix n n R) :
            (a : (n → R) →ₗ[R] (n → R) →ₗ[R] R) → Matrix n n R)
          (((QuadraticMap.associated (R := R) (M := n → R) (N := R) :
                QuadraticMap R (n → R) R →ₗ[R] BilinMap R (n → R) R) :
              (a : QuadraticMap R (n → R) R) → BilinMap R (n → R) R)
            Q))
        i j :
      R)
    (((LinearMap.toMatrix₂' R : ((n → R) →ₗ[R] (n → R) →ₗ[R] R) ≃ₗ[R] Matrix n n R) :
          (a : (n → R) →ₗ[R] (n → R) →ₗ[R] R) → Matrix n n R)
        (((QuadraticMap.associated (R := R) (M := n → R) (N := R) :
              QuadraticMap R (n → R) R →ₗ[R] BilinMap R (n → R) R) :
            (a : QuadraticMap R (n → R) R) → BilinMap R (n → R) R)
          Q)
        i j :
      R)
a₁ :
  Eq.{u_3 + 1} (α := R)
    (((LinearMap.toMatrix₂' R : ((n → R) →ₗ[R] (n → R) →ₗ[R] R) ≃ₗ[R] Matrix n n R) :
          (a : (n → R) →ₗ[R] (n → R) →ₗ[R] R) → Matrix n n R)
        (((QuadraticMap.associated (R := R) (M := n → R) (N := R) :
              QuadraticMap R (n → R) R →ₗ[R] BilinMap R (n → R) R) :
            (a : QuadraticMap R (n → R) R) → BilinMap R (n → R) R)
          Q)
        j i :
      R)
    (((LinearMap.toMatrix₂' R : ((n → R) →ₗ[R] (n → R) →ₗ[R] R) ≃ₗ[R] Matrix n n R) :
          (a : (n → R) →ₗ[R] (n → R) →ₗ[R] R) → Matrix n n R)
        (((QuadraticMap.associated (R := R) (M := n → R) (N := R) :
              QuadraticMap R (n → R) R →ₗ[R] BilinMap R (n → R) R) :
            (a : QuadraticMap R (n → R) R) → BilinMap R (n → R) R)
          Q)
        i j :
      R)
⊢ Q.toMatrix'.transpose i j = Q.toMatrix' i j
have a₂ : Eq.{u_3 + 1} (α := R)
  (((((((QuadraticMap.associated (R := R) (M := n → R) (N := R) : QuadraticMap R (n → R) R →ₗ[R] BilinMap R (n → R) R) :
                    (a : QuadraticMap R (n → R) R) → BilinMap R (n → R) R)
                  Q :
                BilinMap R (n → R) R) :
              (a : n → R) → (n → R) →ₗ[R] R)
            (Pi.single (M := fun (a : n) ↦ R) j 1) :
          (n → R) →ₗ[R] R) :
        (a : n → R) → R)
      (Pi.single (M := fun (a : n) ↦ R) i 1) :
    R)
  (((LinearMap.toMatrix₂' R : ((n → R) →ₗ[R] (n → R) →ₗ[R] R) ≃ₗ[R] Matrix n n R) :
        (a : (n → R) →ₗ[R] (n → R) →ₗ[R] R) → Matrix n n R)
      (((QuadraticMap.associated (R := R) (M := n → R) (N := R) : QuadraticMap R (n → R) R →ₗ[R] BilinMap R (n → R) R) :
          (a : QuadraticMap R (n → R) R) → BilinMap R (n → R) R)
        Q)
      i j :
    R)
Tactic: rw [toMatrix', Matrix.transpose_apply, LinearMap.toMatrix₂'_apply, LinearMap.toMatrix₂'_apply,
    ← QuadraticMap.associated_isSymm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basic (goal)
Goal:
R : Type u_3
N : Type u_5
n : Type w
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing R
inst_3 : Invertible (α := R) 2
inst_4 : AddCommGroup N
inst_5 : Module R N
b : Basis n R N
Q : QuadraticForm R N
⊢ (toMatrix b Q).IsSymm
have a : ∀ (i j : n), (toMatrix b Q).transpose i j = toMatrix b Q i j
Tactic: ext i j
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basic (goal)
Goal:
R : Type u_3
N : Type u_5
n : Type w
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing R
inst_3 : Invertible (α := R) 2
inst_4 : AddCommGroup N
inst_5 : Module R N
b : Basis n R N
Q : QuadraticForm R N
i j : n
⊢ (toMatrix b Q).transpose i j = toMatrix b Q i j
have a : Eq.{u_3 + 1} (α := R)
  (Matrix.transpose
      ((LinearMap.toMatrix₂ b b : (a : N →ₗ[R] N →ₗ[R] R) → Matrix n n R)
        (((QuadraticMap.associated.{u_3, u_5, u_3} (R := R) (M := N) (N := R) :
              QuadraticMap R N R →ₗ[R] BilinMap R N R) :
            (a : QuadraticMap R N R) → BilinMap R N R)
          Q))
      i j :
    R)
  ((LinearMap.toMatrix₂ b b : (a : N →ₗ[R] N →ₗ[R] R) → Matrix n n R)
      (((QuadraticMap.associated.{u_3, u_5, u_3} (R := R) (M := N) (N := R) : QuadraticMap R N R →ₗ[R] BilinMap R N R) :
          (a : QuadraticMap R N R) → BilinMap R N R)
        Q)
      i j :
    R)
Tactic: rw [toMatrix, Matrix.transpose_apply, LinearMap.toMatrix₂_apply, LinearMap.toMatrix₂_apply,
    ← QuadraticMap.associated_isSymm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basic (goal)
Goal:
R : Type u_3
N : Type u_5
n : Type w
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing R
inst_3 : Invertible (α := R) 2
inst_4 : AddCommGroup N
inst_5 : Module R N
b : Basis n R N
Q : QuadraticForm R N
i j : n
a :
  Eq.{u_3 + 1} (α := R)
    (Matrix.transpose
        ((LinearMap.toMatrix₂ b b : (a : N →ₗ[R] N →ₗ[R] R) → Matrix n n R)
          (((QuadraticMap.associated.{u_3, u_5, u_3} (R := R) (M := N) (N := R) :
                QuadraticMap R N R →ₗ[R] BilinMap R N R) :
              (a : QuadraticMap R N R) → BilinMap R N R)
            Q))
        i j :
      R)
    ((LinearMap.toMatrix₂ b b : (a : N →ₗ[R] N →ₗ[R] R) → Matrix n n R)
        (((QuadraticMap.associated.{u_3, u_5, u_3} (R := R) (M := N) (N := R) :
              QuadraticMap R N R →ₗ[R] BilinMap R N R) :
            (a : QuadraticMap R N R) → BilinMap R N R)
          Q)
        i j :
      R)
⊢ (toMatrix b Q).transpose i j = toMatrix b Q i j
have a₁ : Eq.{u_3 + 1} (α := R)
  ((LinearMap.toMatrix₂ b b : (a : N →ₗ[R] N →ₗ[R] R) → Matrix n n R)
      (((QuadraticMap.associated.{u_3, u_5, u_3} (R := R) (M := N) (N := R) : QuadraticMap R N R →ₗ[R] BilinMap R N R) :
          (a : QuadraticMap R N R) → BilinMap R N R)
        Q)
      j i :
    R)
  ((LinearMap.toMatrix₂ b b : (a : N →ₗ[R] N →ₗ[R] R) → Matrix n n R)
      (((QuadraticMap.associated.{u_3, u_5, u_3} (R := R) (M := N) (N := R) : QuadraticMap R N R →ₗ[R] BilinMap R N R) :
          (a : QuadraticMap R N R) → BilinMap R N R)
        Q)
      i j :
    R)
Tactic: rw [toMatrix, Matrix.transpose_apply, LinearMap.toMatrix₂_apply, LinearMap.toMatrix₂_apply,
    ← QuadraticMap.associated_isSymm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basic (goal)
Goal:
R : Type u_3
N : Type u_5
n : Type w
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing R
inst_3 : Invertible (α := R) 2
inst_4 : AddCommGroup N
inst_5 : Module R N
b : Basis n R N
Q : QuadraticForm R N
i j : n
a :
  Eq.{u_3 + 1} (α := R)
    (Matrix.transpose
        ((LinearMap.toMatrix₂ b b : (a : N →ₗ[R] N →ₗ[R] R) → Matrix n n R)
          (((QuadraticMap.associated.{u_3, u_5, u_3} (R := R) (M := N) (N := R) :
                QuadraticMap R N R →ₗ[R] BilinMap R N R) :
              (a : QuadraticMap R N R) → BilinMap R N R)
            Q))
        i j :
      R)
    ((LinearMap.toMatrix₂ b b : (a : N →ₗ[R] N →ₗ[R] R) → Matrix n n R)
        (((QuadraticMap.associated.{u_3, u_5, u_3} (R := R) (M := N) (N := R) :
              QuadraticMap R N R →ₗ[R] BilinMap R N R) :
            (a : QuadraticMap R N R) → BilinMap R N R)
          Q)
        i j :
      R)
a₁ :
  Eq.{u_3 + 1} (α := R)
    ((LinearMap.toMatrix₂ b b : (a : N →ₗ[R] N →ₗ[R] R) → Matrix n n R)
        (((QuadraticMap.associated.{u_3, u_5, u_3} (R := R) (M := N) (N := R) :
              QuadraticMap R N R →ₗ[R] BilinMap R N R) :
            (a : QuadraticMap R N R) → BilinMap R N R)
          Q)
        j i :
      R)
    ((LinearMap.toMatrix₂ b b : (a : N →ₗ[R] N →ₗ[R] R) → Matrix n n R)
        (((QuadraticMap.associated.{u_3, u_5, u_3} (R := R) (M := N) (N := R) :
              QuadraticMap R N R →ₗ[R] BilinMap R N R) :
            (a : QuadraticMap R N R) → BilinMap R N R)
          Q)
        i j :
      R)
⊢ (toMatrix b Q).transpose i j = toMatrix b Q i j
have a₂ : Eq.{u_3 + 1} (α := R)
  (((((((QuadraticMap.associated.{u_3, u_5, u_3} (R := R) (M := N) (N := R) : QuadraticMap R N R →ₗ[R] BilinMap R N R) :
                    (a : QuadraticMap R N R) → BilinMap R N R)
                  Q :
                BilinMap R N R) :
              (a : N) → N →ₗ[R] R)
            ((b : (a : n) → N) j) :
          N →ₗ[R] R) :
        (a : N) → R)
      ((b : (a : n) → N) i : N) :
    R)
  ((LinearMap.toMatrix₂ b b : (a : N →ₗ[R] N →ₗ[R] R) → Matrix n n R)
      (((QuadraticMap.associated.{u_3, u_5, u_3} (R := R) (M := N) (N := R) : QuadraticMap R N R →ₗ[R] BilinMap R N R) :
          (a : QuadraticMap R N R) → BilinMap R N R)
        Q)
      i j :
    R)
Tactic: rw [toMatrix, Matrix.transpose_apply, LinearMap.toMatrix₂_apply, LinearMap.toMatrix₂_apply,
    ← QuadraticMap.associated_isSymm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basic (goal)
Goal:
R : Type u_3
n : Type w
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing R
inst_3 : Invertible (α := R) 2
Q : QuadraticForm R (n → R)
⊢ discr (N := n → R) (n := n) (Pi.basisFun R n) Q = Q.discr'
have rw : Matrix.det.{u_3, w} (n := n) (toMatrix (N := n → R) (Pi.basisFun R n) Q) = Q.discr'
Tactic: rw [discr, discr', toMatrix_eq_toMatrix']
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basic (goal)
Goal:
R : Type u_3
n : Type w
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing R
inst_3 : Invertible (α := R) 2
Q : QuadraticForm R (n → R)
rw : Matrix.det.{u_3, w} (n := n) (toMatrix (N := n → R) (Pi.basisFun R n) Q) = Q.discr'
⊢ discr (N := n → R) (n := n) (Pi.basisFun R n) Q = Q.discr'
have rw₁ : Matrix.det.{u_3, w} (n := n) (toMatrix (N := n → R) (Pi.basisFun R n) Q) = Q.toMatrix'.det
Tactic: rw [discr, discr', toMatrix_eq_toMatrix']
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basic (goal)
Goal:
R : Type u_3
n : Type w
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing R
inst_3 : Invertible (α := R) 2
Q : QuadraticForm R (n → R)
rw : Matrix.det.{u_3, w} (n := n) (toMatrix (N := n → R) (Pi.basisFun R n) Q) = Q.discr'
rw₁ : Matrix.det.{u_3, w} (n := n) (toMatrix (N := n → R) (Pi.basisFun R n) Q) = Q.toMatrix'.det
⊢ discr (N := n → R) (n := n) (Pi.basisFun R n) Q = Q.discr'
have rw₂ : Q.toMatrix'.det = Q.toMatrix'.det
Tactic: rw [discr, discr', toMatrix_eq_toMatrix']
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basic (goal)
Goal:
R : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
htwo : Invertible (α := R) 2
B : BilinForm R M
hB₁ : B ≠ 0
hB₂ : IsSymm B
⊢ ∃ (x : M), ¬IsOrtho B x x
have lift : ∀ (Q : QuadraticMap R M R)
  (hB₁ :
    Ne (α := BilinForm R M)
      (((QuadraticMap.associatedHom.{0, u_3, u_4, u_3} ℕ (R := R) (M := M) (N := R) :
              QuadraticMap R M R →ₗ[ℕ] BilinMap R M R) :
            (a : QuadraticMap R M R) → BilinMap R M R)
          Q :
        BilinMap R M R)
      (0 : BilinForm R M)),
  ∃ (x : M),
    ¬IsOrtho.{u_3, u_3, u_3, u_3, u_4, u_4} (R := R) (R₁ := R) (R₂ := R) (M := R) (I₁ := RingHom.id R) (I₂ :=
        RingHom.id R)
        (((QuadraticMap.associatedHom.{0, u_3, u_4, u_3} ℕ (R := R) (M := M) (N := R) :
              QuadraticMap R M R →ₗ[ℕ] BilinMap R M R) :
            (a : QuadraticMap R M R) → BilinMap R M R)
          Q)
        x x
Tactic: lift B to QuadraticForm R M using hB₂ with Q
Cleared hypotheses: hB₁, hB₂
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basic (goal)
Goal:
R : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
htwo : Invertible (α := R) 2
B : BilinForm R M
Q : QuadraticMap R M R
hB₁ :
  Ne (α := BilinForm R M)
    (((QuadraticMap.associatedHom.{0, u_3, u_4, u_3} ℕ (R := R) (M := M) (N := R) :
            QuadraticMap R M R →ₗ[ℕ] BilinMap R M R) :
          (a : QuadraticMap R M R) → BilinMap R M R)
        Q :
      BilinMap R M R)
    (0 : BilinForm R M)
⊢ ∃ (x : M),
    ¬IsOrtho.{u_3, u_3, u_3, u_3, u_4, u_4} (R := R) (R₁ := R) (R₂ := R) (M := R) (I₁ := RingHom.id R) (I₂ :=
        RingHom.id R)
        (((QuadraticMap.associatedHom.{0, u_3, u_4, u_3} ℕ (R := R) (M := M) (N := R) :
              QuadraticMap R M R →ₗ[ℕ] BilinMap R M R) :
            (a : QuadraticMap R M R) → BilinMap R M R)
          Q)
        x x
have obtain : ∀ (x : M) (hx : Ne.{u_3 + 1} (α := R) ((Q : (a : M) → R) x : R) (0 : R)),
  ∃ (x : M),
    ¬IsOrtho.{u_3, u_3, u_3, u_3, u_4, u_4} (R := R) (R₁ := R) (R₂ := R) (M := R) (I₁ := RingHom.id R) (I₂ :=
        RingHom.id R)
        (((QuadraticMap.associatedHom.{0, u_3, u_4, u_3} ℕ (R := R) (M := M) (N := R) :
              QuadraticMap R M R →ₗ[ℕ] BilinMap R M R) :
            (a : QuadraticMap R M R) → BilinMap R M R)
          Q)
        x x
Tactic: obtain ⟨x, hx⟩ := QuadraticMap.exists_quadraticMap_ne_zero hB₁