awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basic
Goal:
R : Type u_3
M : Type u_4
N : Type u_5
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
toFun : M → N
toFun_smul : ∀ (a : R) (x : M), toFun (a • x) = (a * a) • toFun x
exists_companion' :
  ∃ (B : BilinMap R M N),
    ∀ (x y : M),
      toFun (x + y) =
        HAdd.hAdd (β := N) (toFun x + toFun y) ((((B : (a : M) → M →ₗ[R] N) x : M →ₗ[R] N) : (a : M) → N) y : N)
⊢ (⇑{ toFun := toFun, toFun_smul := toFun_smul, exists_companion' := exists_companion' : QuadraticMap R M N } :
      (a : M) → N) =
    toFun

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basic
Goal:
R : Type u_3
M : Type u_4
N : Type u_5
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
Q Q' : QuadraticMap R M N
H : ∀ (x : M), Eq.{u_5 + 1} (α := N) ((Q : (a : M) → N) x : N) ((Q' : (a : M) → N) x : N)
⊢ Q = Q'

Tactic:
DFunLike.ext _ _ H

Premises used: DFunLike.ext
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basic
Goal:
R : Type u_3
M : Type u_4
N : Type u_5
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
Q Q' : QuadraticMap R M N
h : Q = Q'
x : M
⊢ Eq.{u_5 + 1} (α := N) ((Q : (a : M) → N) x : N) ((Q' : (a : M) → N) x : N)

Tactic:
DFunLike.congr_fun h _

Premises used: DFunLike.congr_fun
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basic
Goal:
R : Type u_3
M : Type u_4
N : Type u_5
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
Q : QuadraticMap R M N
Q' : M → N
h : Q' = (⇑Q : (a : M) → N)
⊢ (⇑(Q.copy Q' h) : (a : M) → N) = Q'

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basic
Goal:
R : Type u_3
M : Type u_4
N : Type u_5
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
Q : QuadraticMap R M N
Q' : M → N
h : Q' = (⇑Q : (a : M) → N)
⊢ Q.copy Q' h = Q

Tactic:
DFunLike.ext' h

Premises used: DFunLike.ext'
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basic
Goal:
R : Type u_3
M : Type u_4
N : Type u_5
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
Q : QuadraticMap R M N
a : R
x : M
⊢ (Q : (a : M) → N) (a • x) = HSMul.hSMul (β := N) (a * a) ((Q : (a : M) → N) x : N)

Tactic:
Q.toFun_smul a x

Premises used: QuadraticMap.toFun_smul
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basic
Goal:
R : Type u_3
M : Type u_4
N : Type u_5
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
Q : QuadraticMap R M N
⊢ ∃ (B : BilinMap R M N),
    ∀ (x y : M),
      (Q : (a : M) → N) (x + y) =
        HAdd.hAdd (β := N) (HAdd.hAdd (α := N) (β := N) ((Q : (a : M) → N) x : N) ((Q : (a : M) → N) y : N))
          ((((B : (a : M) → M →ₗ[R] N) x : M →ₗ[R] N) : (a : M) → N) y : N)

Tactic:
Q.exists_companion'

Premises used: QuadraticMap.exists_companion'
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basic
Goal:
R : Type u_3
M : Type u_4
N : Type u_5
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
Q : QuadraticMap R M N
x y z : M
obtain :
  ∀ (B : BilinMap R M N)
    (h :
      ∀ (x y : M),
        (Q : (a : M) → N) (x + y) =
          HAdd.hAdd (β := N) (HAdd.hAdd (α := N) (β := N) ((Q : (a : M) → N) x : N) ((Q : (a : M) → N) y : N))
            ((((B : (a : M) → M →ₗ[R] N) x : M →ₗ[R] N) : (a : M) → N) y : N)),
    HAdd.hAdd (α := N) ((Q : (a : M) → N) (x + y + z) : N)
        (HAdd.hAdd (β := N) (HAdd.hAdd (α := N) (β := N) ((Q : (a : M) → N) x : N) ((Q : (a : M) → N) y : N))
          ((Q : (a : M) → N) z : N)) =
      HAdd.hAdd (β := N) (HAdd.hAdd (α := N) (β := N) ((Q : (a : M) → N) (x + y) : N) ((Q : (a : M) → N) (y + z) : N))
        ((Q : (a : M) → N) (z + x) : N)
⊢ HAdd.hAdd (α := N) ((Q : (a : M) → N) (x + y + z) : N)
      (HAdd.hAdd (β := N) (HAdd.hAdd (α := N) (β := N) ((Q : (a : M) → N) x : N) ((Q : (a : M) → N) y : N))
        ((Q : (a : M) → N) z : N)) =
    HAdd.hAdd (β := N) (HAdd.hAdd (α := N) (β := N) ((Q : (a : M) → N) (x + y) : N) ((Q : (a : M) → N) (y + z) : N))
      ((Q : (a : M) → N) (z + x) : N)

Tactic:
obtain ⟨B, h⟩ := Q.exists_companion

Premises used: QuadraticMap.exists_companion
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basic
Goal:
R : Type u_3
M : Type u_4
N : Type u_5
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
Q : QuadraticMap R M N
x y z : M
B : BilinMap R M N
h :
  ∀ (x y : M),
    (Q : (a : M) → N) (x + y) =
      HAdd.hAdd (β := N) (HAdd.hAdd (α := N) (β := N) ((Q : (a : M) → N) x : N) ((Q : (a : M) → N) y : N))
        ((((B : (a : M) → M →ₗ[R] N) x : M →ₗ[R] N) : (a : M) → N) y : N)
rw :
  HAdd.hAdd (α := N) ((Q : (a : M) → N) (x + y + z) : N)
      (HAdd.hAdd (β := N) (HAdd.hAdd (α := N) (β := N) ((Q : (a : M) → N) x : N) ((Q : (a : M) → N) y : N))
        ((Q : (a : M) → N) z : N)) =
    HAdd.hAdd (β := N) (HAdd.hAdd (α := N) (β := N) ((Q : (a : M) → N) (x + y) : N) ((Q : (a : M) → N) (y + z) : N))
      ((Q : (a : M) → N) (x + z) : N)
⊢ HAdd.hAdd (α := N) ((Q : (a : M) → N) (x + y + z) : N)
      (HAdd.hAdd (β := N) (HAdd.hAdd (α := N) (β := N) ((Q : (a : M) → N) x : N) ((Q : (a : M) → N) y : N))
        ((Q : (a : M) → N) z : N)) =
    HAdd.hAdd (β := N) (HAdd.hAdd (α := N) (β := N) ((Q : (a : M) → N) (x + y) : N) ((Q : (a : M) → N) (y + z) : N))
      ((Q : (a : M) → N) (z + x) : N)

Tactic:
rw [add_comm z x]

Premises used: add_comm
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basic
Goal:
R : Type u_3
M : Type u_4
N : Type u_5
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
Q : QuadraticMap R M N
x y z : M
B : BilinMap R M N
h :
  ∀ (x y : M),
    (Q : (a : M) → N) (x + y) =
      HAdd.hAdd (β := N) (HAdd.hAdd (α := N) (β := N) ((Q : (a : M) → N) x : N) ((Q : (a : M) → N) y : N))
        ((((B : (a : M) → M →ₗ[R] N) x : M →ₗ[R] N) : (a : M) → N) y : N)
simp :
  HAdd.hAdd (β := N)
          (HAdd.hAdd (β := N) (HAdd.hAdd (α := N) (β := N) ((Q : (a : M) → N) x : N) ((Q : (a : M) → N) y : N))
            ((((B : (a : M) → M →ₗ[R] N) x : M →ₗ[R] N) : (a : M) → N) y : N))
          ((Q : (a : M) → N) z : N) +
        HAdd.hAdd (α := N) (β := N) ((((B : (a : M) → M →ₗ[R] N) x : M →ₗ[R] N) : (a : M) → N) z : N)
          ((((B : (a : M) → M →ₗ[R] N) y : M →ₗ[R] N) : (a : M) → N) z : N) +
      HAdd.hAdd (β := N) (HAdd.hAdd (α := N) (β := N) ((Q : (a : M) → N) x : N) ((Q : (a : M) → N) y : N))
        ((Q : (a : M) → N) z : N) =
    HAdd.hAdd (β := N) (HAdd.hAdd (α := N) (β := N) ((Q : (a : M) → N) x : N) ((Q : (a : M) → N) y : N))
          ((((B : (a : M) → M →ₗ[R] N) x : M →ₗ[R] N) : (a : M) → N) y : N) +
        HAdd.hAdd (β := N) (HAdd.hAdd (α := N) (β := N) ((Q : (a : M) → N) y : N) ((Q : (a : M) → N) z : N))
          ((((B : (a : M) → M →ₗ[R] N) y : M →ₗ[R] N) : (a : M) → N) z : N) +
      HAdd.hAdd (β := N) (HAdd.hAdd (α := N) (β := N) ((Q : (a : M) → N) x : N) ((Q : (a : M) → N) z : N))
        ((((B : (a : M) → M →ₗ[R] N) x : M →ₗ[R] N) : (a : M) → N) z : N)
⊢ HAdd.hAdd (α := N) ((Q : (a : M) → N) (x + y + z) : N)
      (HAdd.hAdd (β := N) (HAdd.hAdd (α := N) (β := N) ((Q : (a : M) → N) x : N) ((Q : (a : M) → N) y : N))
        ((Q : (a : M) → N) z : N)) =
    HAdd.hAdd (β := N) (HAdd.hAdd (α := N) (β := N) ((Q : (a : M) → N) (x + y) : N) ((Q : (a : M) → N) (y + z) : N))
      ((Q : (a : M) → N) (x + z) : N)

Tactic:
simp only [h, LinearMap.map_add₂]

Premises used: LinearMap.map_add₂
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basic
Goal:
R : Type u_3
M : Type u_4
N : Type u_5
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
Q : QuadraticMap R M N
x y z : M
B : BilinMap R M N
h :
  ∀ (x y : M),
    (Q : (a : M) → N) (x + y) =
      HAdd.hAdd (β := N) (HAdd.hAdd (α := N) (β := N) ((Q : (a : M) → N) x : N) ((Q : (a : M) → N) y : N))
        ((((B : (a : M) → M →ₗ[R] N) x : M →ₗ[R] N) : (a : M) → N) y : N)
⊢ HAdd.hAdd (β := N)
          (HAdd.hAdd (β := N) (HAdd.hAdd (α := N) (β := N) ((Q : (a : M) → N) x : N) ((Q : (a : M) → N) y : N))
            ((((B : (a : M) → M →ₗ[R] N) x : M →ₗ[R] N) : (a : M) → N) y : N))
          ((Q : (a : M) → N) z : N) +
        HAdd.hAdd (α := N) (β := N) ((((B : (a : M) → M →ₗ[R] N) x : M →ₗ[R] N) : (a : M) → N) z : N)
          ((((B : (a : M) → M →ₗ[R] N) y : M →ₗ[R] N) : (a : M) → N) z : N) +
      HAdd.hAdd (β := N) (HAdd.hAdd (α := N) (β := N) ((Q : (a : M) → N) x : N) ((Q : (a : M) → N) y : N))
        ((Q : (a : M) → N) z : N) =
    HAdd.hAdd (β := N) (HAdd.hAdd (α := N) (β := N) ((Q : (a : M) → N) x : N) ((Q : (a : M) → N) y : N))
          ((((B : (a : M) → M →ₗ[R] N) x : M →ₗ[R] N) : (a : M) → N) y : N) +
        HAdd.hAdd (β := N) (HAdd.hAdd (α := N) (β := N) ((Q : (a : M) → N) y : N) ((Q : (a : M) → N) z : N))
          ((((B : (a : M) → M →ₗ[R] N) y : M →ₗ[R] N) : (a : M) → N) z : N) +
      HAdd.hAdd (β := N) (HAdd.hAdd (α := N) (β := N) ((Q : (a : M) → N) x : N) ((Q : (a : M) → N) z : N))
        ((((B : (a : M) → M →ₗ[R] N) x : M →ₗ[R] N) : (a : M) → N) z : N)

Tactic:
abel
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basic
Goal:
R : Type u_3
M : Type u_4
N : Type u_5
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
Q : QuadraticMap R M N
x : M
rw :
  HSMul.hSMul (β := N) (HMul.hMul (α := R) 2 2) ((Q : (a : M) → N) x : N) =
    HSMul.hSMul.{u_3, u_5, u_5} (α := R) (β := N) (↑4 : R) ((Q : (a : M) → N) x : N)
⊢ (Q : (a : M) → N) (x + x) = HSMul.hSMul (α := ℕ) (β := N) 4 ((Q : (a : M) → N) x : N)

Tactic:
rw [← two_smul R x, Q.map_smul, ← Nat.cast_smul_eq_nsmul R]

Premises used: QuadraticMap.map_smul, two_smul, Nat.cast_smul_eq_nsmul
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basic
Goal:
R : Type u_3
M : Type u_4
N : Type u_5
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
Q : QuadraticMap R M N
x : M
⊢ HSMul.hSMul (β := N) (HMul.hMul (α := R) 2 2) ((Q : (a : M) → N) x : N) =
    HSMul.hSMul.{u_3, u_5, u_5} (α := R) (β := N) (↑4 : R) ((Q : (a : M) → N) x : N)

Tactic:
norm_num
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basic
Goal:
R : Type u_3
M : Type u_4
N : Type u_5
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
Q : QuadraticMap R M N
rw : Eq.{u_5 + 1} (α := N) ((Q : (a : M) → N) (HSMul.hSMul.{u_3, u_4, u_4} (α := R) (β := M) 0 0) : N) (0 : N)
rw₁ : HSMul.hSMul (β := N) (HMul.hMul (α := R) 0 0) ((Q : (a : M) → N) 0 : N) = 0
rw₂ : HSMul.hSMul.{u_3, u_5, u_5} (α := R) (β := N) 0 ((Q : (a : M) → N) 0 : N) = 0
rw₃ rw₄ : Eq.{u_5 + 1} (α := N) 0 0
⊢ Eq.{u_5 + 1} (α := N) ((Q : (a : M) → N) 0 : N) (0 : N)

Tactic:
rw [← @zero_smul R _ _ _ _ (0 : M), Q.map_smul, zero_mul, zero_smul]

Premises used: QuadraticMap.map_smul, MulZeroClass.zero_mul, zero_smul, OfNat.ofNat
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basic
Goal:
S : Type u_1
T : Type u_2
R : Type u_3
M : Type u_4
N : Type u_5
P : Type u_6
A : Type u_7
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
Q : QuadraticMap R M N
⊢ ZeroHomClass (QuadraticMap R M N) M N

Tactic:
{ QuadraticMap.instFunLike (R := R) (M := M) (N := N) with map_zero := QuadraticMap.map_zero }

Premises used: QuadraticMap.map_zero, QuadraticMap.instFunLike, ZeroHomClass.mk
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basic
Goal:
S : Type u_1
R : Type u_3
M : Type u_4
N : Type u_5
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
Q : QuadraticMap R M N
inst_5 : CommSemiring S
inst_6 : Algebra S R
inst_7 : SMul S M
inst_8 : IsScalarTower S R M
inst_9 : Module S N
inst_10 : IsScalarTower S R N
a : S
x : M
rw :
  (Q : (a : M) → N) (HSMul.hSMul.{u_3, u_4, u_4} (α := R) ((algebraMap S R : (a : S) → R) a : R) x) =
    HSMul.hSMul (β := N) (a * a) ((Q : (a : M) → N) x : N)
rw₁ :
  HSMul.hSMul (β := N)
      (HMul.hMul (α := R) (β := R) ((algebraMap S R : (a : S) → R) a : R) ((algebraMap S R : (a : S) → R) a : R))
      ((Q : (a : M) → N) x : N) =
    HSMul.hSMul (β := N) (a * a) ((Q : (a : M) → N) x : N)
rw₂ :
  HSMul.hSMul.{u_3, u_5, u_5} (α := R) (β := N) ((algebraMap S R : (a : S) → R) (a * a) : R) ((Q : (a : M) → N) x : N) =
    HSMul.hSMul (β := N) (a * a) ((Q : (a : M) → N) x : N)
rw₃ rw₄ :
  HSMul.hSMul (β := N) (a * a) ((Q : (a : M) → N) x : N) = HSMul.hSMul (β := N) (a * a) ((Q : (a : M) → N) x : N)
⊢ (Q : (a : M) → N) (a • x) = HSMul.hSMul (β := N) (a * a) ((Q : (a : M) → N) x : N)

Tactic:
rw [← IsScalarTower.algebraMap_smul R a x, Q.map_smul, ← map_mul, algebraMap_smul]

Premises used: QuadraticMap.map_smul, algebraMap_smul, IsScalarTower.algebraMap_smul, map_mul
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basic
Goal:
R : Type u_3
M : Type u_4
N : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
Q : QuadraticMap R M N
x : M
rw :
  Eq.{u_5 + 1} (α := N) ((Q : (a : M) → N) (HSMul.hSMul.{u_3, u_4, u_4} (α := R) (-1) x) : N) ((Q : (a : M) → N) x : N)
rw₁ : HSMul.hSMul (β := N) (HMul.hMul (α := R) (-1) (-1)) ((Q : (a : M) → N) x : N) = (Q : (a : M) → N) x
rw₂ : HSMul.hSMul.{u_3, u_5, u_5} (α := R) (β := N) (- -1) ((Q : (a : M) → N) x : N) = (Q : (a : M) → N) x
rw₃ : HSMul.hSMul.{u_3, u_5, u_5} (α := R) (β := N) 1 ((Q : (a : M) → N) x : N) = (Q : (a : M) → N) x
rw₄ rw₅ : Eq.{u_5 + 1} (α := N) ((Q : (a : M) → N) x : N) ((Q : (a : M) → N) x : N)
⊢ Eq.{u_5 + 1} (α := N) ((Q : (a : M) → N) (-x) : N) ((Q : (a : M) → N) x : N)

Tactic:
rw [← @neg_one_smul R _ _ _ _ x, Q.map_smul, neg_one_mul, neg_neg, one_smul]

Premises used: neg_one_smul, QuadraticMap.map_smul, neg_one_mul, neg_neg, one_smul
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basic
Goal:
R : Type u_3
M : Type u_4
N : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
Q : QuadraticMap R M N
x y : M
rw : Eq.{u_5 + 1} (α := N) ((Q : (a : M) → N) (-(y - x)) : N) ((Q : (a : M) → N) (y - x) : N)
rw₁ rw₂ : Eq.{u_5 + 1} (α := N) ((Q : (a : M) → N) (y - x) : N) ((Q : (a : M) → N) (y - x) : N)
⊢ Eq.{u_5 + 1} (α := N) ((Q : (a : M) → N) (x - y) : N) ((Q : (a : M) → N) (y - x) : N)

Tactic:
rw [← neg_sub, Q.map_neg]

Premises used: neg_sub, QuadraticMap.map_neg
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basic
Goal:
R : Type u_3
M : Type u_4
N : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
Q : QuadraticMap R M N
y : M
⊢ Eq.{u_5 + 1} (α := N) (polar (⇑Q : (a : M) → N) 0 y) 0

Tactic:
simp only [polar, zero_add, QuadraticMap.map_zero, sub_zero, sub_self]

Premises used: sub_self, sub_zero, QuadraticMap.map_zero, QuadraticMap.polar, zero_add
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basic
Goal:
R : Type u_3
M : Type u_4
N : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
Q : QuadraticMap R M N
x x' y : M
⊢ polar (⇑Q : (a : M) → N) (x + x') y =
    HAdd.hAdd (α := N) (polar (⇑Q : (a : M) → N) x y) (polar (⇑Q : (a : M) → N) x' y)

Tactic:
polar_add_left_iff.mpr <| Q.map_add_add_add_map x x' y

Premises used: Iff.mpr, QuadraticMap.polar_add_left_iff, QuadraticMap.map_add_add_add_map
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basic
Goal:
R : Type u_3
M : Type u_4
N : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
Q : QuadraticMap R M N
a : R
x y : M
obtain :
  ∀ (B : BilinMap R M N)
    (h :
      ∀ (x y : M),
        (Q : (a : M) → N) (x + y) =
          HAdd.hAdd (β := N) (HAdd.hAdd (α := N) (β := N) ((Q : (a : M) → N) x : N) ((Q : (a : M) → N) y : N))
            ((((B : (a : M) → M →ₗ[R] N) x : M →ₗ[R] N) : (a : M) → N) y : N)),
    polar (⇑Q : (a : M) → N) (a • x) y = HSMul.hSMul (β := N) a (polar (⇑Q : (a : M) → N) x y)
⊢ polar (⇑Q : (a : M) → N) (a • x) y = HSMul.hSMul (β := N) a (polar (⇑Q : (a : M) → N) x y)

Tactic:
obtain ⟨B, h⟩ := Q.exists_companion

Premises used: QuadraticMap.exists_companion
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basic
Goal:
R : Type u_3
M : Type u_4
N : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
Q : QuadraticMap R M N
x y : M
rw :
  Eq.{u_5 + 1} (α := N) (polar (⇑Q : (a : M) → N) (HSMul.hSMul.{u_3, u_4, u_4} (α := R) (-1) x) y)
    (-polar (⇑Q : (a : M) → N) x y)
rw₁ : HSMul.hSMul.{u_3, u_5, u_5} (α := R) (β := N) (-1) (polar (⇑Q : (a : M) → N) x y) = -polar (⇑Q : (a : M) → N) x y
rw₂ rw₃ : Eq.{u_5 + 1} (α := N) (-polar (⇑Q : (a : M) → N) x y) (-polar (⇑Q : (a : M) → N) x y)
⊢ Eq.{u_5 + 1} (α := N) (polar (⇑Q : (a : M) → N) (-x) y) (-polar (⇑Q : (a : M) → N) x y)

Tactic:
rw [← neg_one_smul R x, polar_smul_left, neg_one_smul]

Premises used: neg_one_smul, QuadraticMap.polar_smul_left
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basic
Goal:
R : Type u_3
M : Type u_4
N : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
Q : QuadraticMap R M N
x x' y : M
rw :
  polar (⇑Q : (a : M) → N) (x + -x') y =
    HSub.hSub (α := N) (polar (⇑Q : (a : M) → N) x y) (polar (⇑Q : (a : M) → N) x' y)
rw₁ :
  polar (⇑Q : (a : M) → N) (x + -x') y =
    HAdd.hAdd (α := N) (polar (⇑Q : (a : M) → N) x y) (-polar (⇑Q : (a : M) → N) x' y)
rw₂ :
  HAdd.hAdd (α := N) (polar (⇑Q : (a : M) → N) x y) (polar (⇑Q : (a : M) → N) (-x') y) =
    HAdd.hAdd (α := N) (polar (⇑Q : (a : M) → N) x y) (-polar (⇑Q : (a : M) → N) x' y)
rw₃ rw₄ :
  HAdd.hAdd (α := N) (polar (⇑Q : (a : M) → N) x y) (-polar (⇑Q : (a : M) → N) x' y) =
    HAdd.hAdd (α := N) (polar (⇑Q : (a : M) → N) x y) (-polar (⇑Q : (a : M) → N) x' y)
⊢ polar (⇑Q : (a : M) → N) (x - x') y =
    HSub.hSub (α := N) (polar (⇑Q : (a : M) → N) x y) (polar (⇑Q : (a : M) → N) x' y)

Tactic:
rw [sub_eq_add_neg, sub_eq_add_neg, polar_add_left, polar_neg_left]

Premises used: QuadraticMap.polar_neg_left, sub_eq_add_neg, QuadraticMap.polar_add_left
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basic
Goal:
R : Type u_3
M : Type u_4
N : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
Q : QuadraticMap R M N
y : M
⊢ Eq.{u_5 + 1} (α := N) (polar (⇑Q : (a : M) → N) y 0) 0

Tactic:
simp only [add_zero, polar, QuadraticMap.map_zero, sub_self]

Premises used: sub_self, QuadraticMap.map_zero, QuadraticMap.polar, add_zero
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basic
Goal:
R : Type u_3
M : Type u_4
N : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
Q : QuadraticMap R M N
x y y' : M
rw :
  polar (⇑Q : (a : M) → N) (y + y') x =
    HAdd.hAdd (α := N) (polar (⇑Q : (a : M) → N) x y) (polar (⇑Q : (a : M) → N) x y')
rw₁ :
  polar (⇑Q : (a : M) → N) (y + y') x =
    HAdd.hAdd (α := N) (polar (⇑Q : (a : M) → N) y x) (polar (⇑Q : (a : M) → N) x y')
rw₂ :
  polar (⇑Q : (a : M) → N) (y + y') x =
    HAdd.hAdd (α := N) (polar (⇑Q : (a : M) → N) y x) (polar (⇑Q : (a : M) → N) y' x)
rw₃ rw₄ :
  HAdd.hAdd (α := N) (polar (⇑Q : (a : M) → N) y x) (polar (⇑Q : (a : M) → N) y' x) =
    HAdd.hAdd (α := N) (polar (⇑Q : (a : M) → N) y x) (polar (⇑Q : (a : M) → N) y' x)
⊢ polar (⇑Q : (a : M) → N) x (y + y') =
    HAdd.hAdd (α := N) (polar (⇑Q : (a : M) → N) x y) (polar (⇑Q : (a : M) → N) x y')

Tactic:
rw [polar_comm Q x, polar_comm Q x, polar_comm Q x, polar_add_left]

Premises used: QuadraticMap.polar_add_left, QuadraticMap.polar_comm, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basic
Goal:
R : Type u_3
M : Type u_4
N : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
Q : QuadraticMap R M N
a : R
x y : M
rw : polar (⇑Q : (a : M) → N) (a • y) x = HSMul.hSMul (β := N) a (polar (⇑Q : (a : M) → N) x y)
rw₁ : polar (⇑Q : (a : M) → N) (a • y) x = HSMul.hSMul (β := N) a (polar (⇑Q : (a : M) → N) y x)
rw₂ rw₃ : HSMul.hSMul (β := N) a (polar (⇑Q : (a : M) → N) y x) = HSMul.hSMul (β := N) a (polar (⇑Q : (a : M) → N) y x)
⊢ polar (⇑Q : (a : M) → N) x (a • y) = HSMul.hSMul (β := N) a (polar (⇑Q : (a : M) → N) x y)

Tactic:
rw [polar_comm Q x, polar_comm Q x, polar_smul_left]

Premises used: QuadraticMap.polar_comm, QuadraticMap.polar_smul_left, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basic
Goal:
R : Type u_3
M : Type u_4
N : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
Q : QuadraticMap R M N
x y : M
rw :
  Eq.{u_5 + 1} (α := N) (polar (⇑Q : (a : M) → N) x (HSMul.hSMul.{u_3, u_4, u_4} (α := R) (-1) y))
    (-polar (⇑Q : (a : M) → N) x y)
rw₁ : HSMul.hSMul.{u_3, u_5, u_5} (α := R) (β := N) (-1) (polar (⇑Q : (a : M) → N) x y) = -polar (⇑Q : (a : M) → N) x y
rw₂ rw₃ : Eq.{u_5 + 1} (α := N) (-polar (⇑Q : (a : M) → N) x y) (-polar (⇑Q : (a : M) → N) x y)
⊢ Eq.{u_5 + 1} (α := N) (polar (⇑Q : (a : M) → N) x (-y)) (-polar (⇑Q : (a : M) → N) x y)

Tactic:
rw [← neg_one_smul R y, polar_smul_right, neg_one_smul]

Premises used: neg_one_smul, QuadraticMap.polar_smul_right
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basic
Goal:
R : Type u_3
M : Type u_4
N : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
Q : QuadraticMap R M N
x y y' : M
rw :
  polar (⇑Q : (a : M) → N) x (y + -y') =
    HSub.hSub (α := N) (polar (⇑Q : (a : M) → N) x y) (polar (⇑Q : (a : M) → N) x y')
rw₁ :
  polar (⇑Q : (a : M) → N) x (y + -y') =
    HAdd.hAdd (α := N) (polar (⇑Q : (a : M) → N) x y) (-polar (⇑Q : (a : M) → N) x y')
rw₂ :
  HAdd.hAdd (α := N) (polar (⇑Q : (a : M) → N) x y) (polar (⇑Q : (a : M) → N) x (-y')) =
    HAdd.hAdd (α := N) (polar (⇑Q : (a : M) → N) x y) (-polar (⇑Q : (a : M) → N) x y')
rw₃ rw₄ :
  HAdd.hAdd (α := N) (polar (⇑Q : (a : M) → N) x y) (-polar (⇑Q : (a : M) → N) x y') =
    HAdd.hAdd (α := N) (polar (⇑Q : (a : M) → N) x y) (-polar (⇑Q : (a : M) → N) x y')
⊢ polar (⇑Q : (a : M) → N) x (y - y') =
    HSub.hSub (α := N) (polar (⇑Q : (a : M) → N) x y) (polar (⇑Q : (a : M) → N) x y')

Tactic:
rw [sub_eq_add_neg, sub_eq_add_neg, polar_add_right, polar_neg_right]

Premises used: sub_eq_add_neg, QuadraticMap.polar_neg_right, QuadraticMap.polar_add_right
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basic
Goal:
R : Type u_3
M : Type u_4
N : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
Q : QuadraticMap R M N
x : M
rw :
  HSMul.hSMul (α := ℕ) (β := N) 4 ((Q : (a : M) → N) x : N) =
    HSMul.hSMul (β := N) (HMul.hMul (α := ℕ) 2 2) ((Q : (a : M) → N) x : N)
⊢ polar (⇑Q : (a : M) → N) x x = HSMul.hSMul (α := ℕ) (β := N) 2 ((Q : (a : M) → N) x : N)

Tactic:
rw [polar, map_add_self, sub_sub, sub_eq_iff_eq_add, ← two_smul ℕ, ← two_smul ℕ, ← mul_smul]

Premises used: QuadraticMap.map_add_self, two_smul, QuadraticMap.polar, sub_sub, sub_eq_iff_eq_add, Nat, SemigroupAction.mul_smul
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basic
Goal:
R : Type u_3
M : Type u_4
N : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
Q : QuadraticMap R M N
x : M
⊢ HSMul.hSMul (α := ℕ) (β := N) 4 ((Q : (a : M) → N) x : N) =
    HSMul.hSMul (β := N) (HMul.hMul (α := ℕ) 2 2) ((Q : (a : M) → N) x : N)

Tactic:
simp