awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : CommSemiring S
inst_6 : Algebra S R
inst_7 : Module S N
inst_8 : IsScalarTower S R N
inst_9 : Invertible (α := Module.End R N) 2
x x_1 : QuadraticMap R M N
x_2 x_3 : M
⊢ Eq.{u_5 + 1} (α := N)
    ((((HSMul.hSMul (α := Module.End R N) (@Invertible.invOf _ Module.End.instMul Module.End.instOne 2 _)
                  (x + x_1).polarBilin :
                (a : M) → M →ₗ[R] N)
              x_2 :
            M →ₗ[R] N) :
          (a : M) → N)
        x_3 :
      N)
    ((((HSMul.hSMul (α := Module.End R N) (@Invertible.invOf _ Module.End.instMul Module.End.instOne 2 _) x.polarBilin +
                  HSMul.hSMul (α := Module.End R N) (@Invertible.invOf _ Module.End.instMul Module.End.instOne 2 _)
                    x_1.polarBilin :
                (a : M) → M →ₗ[R] N)
              x_2 :
            M →ₗ[R] N) :
          (a : M) → N)
        x_3 :
      N)

Tactic:
simp [polar_add]

Premises used: QuadraticMap.polar_add
-- 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 : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : CommSemiring S
inst_6 : Algebra S R
inst_7 : Module S N
inst_8 : IsScalarTower S R N
inst_9 : Invertible (α := Module.End R N) 2
x : S
x_1 : QuadraticMap R M N
x_2 x_3 : M
⊢ Eq.{u_5 + 1} (α := N)
    ((((HSMul.hSMul (α := Module.End R N) (@Invertible.invOf _ Module.End.instMul Module.End.instOne 2 _)
                  (x • x_1).polarBilin :
                (a : M) → M →ₗ[R] N)
              x_2 :
            M →ₗ[R] N) :
          (a : M) → N)
        x_3 :
      N)
    ((((HSMul.hSMul (α := S) ((RingHom.id S : (a : S) → S) x : S)
                  (HSMul.hSMul (α := Module.End R N) (@Invertible.invOf _ Module.End.instMul Module.End.instOne 2 _)
                    x_1.polarBilin) :
                (a : M) → M →ₗ[R] N)
              x_2 :
            M →ₗ[R] N) :
          (a : M) → N)
        x_3 :
      N)

Tactic:
simp [polar_smul]

Premises used: QuadraticMap.polar_smul
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basic
Goal:
S : Type u_1
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
inst_5 : CommSemiring S
inst_6 : Algebra S R
inst_7 : Module S N
inst_8 : IsScalarTower S R N
inst_9 : Invertible (α := Module.End R N) 2
Q : QuadraticMap R M N
x y : M
⊢ ((((((associatedHom S : QuadraticMap R M N →ₗ[S] BilinMap R M N) : (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 =
    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))

Tactic:
rfl

Premises used: QuadraticMap.polar, rfl
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basic
Goal:
S : Type u_1
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
inst_5 : CommSemiring S
inst_6 : Algebra S R
inst_7 : Module S N
inst_8 : IsScalarTower S R N
inst_9 : Invertible (α := Module.End R N) 2
Q : QuadraticMap R M N
h :
  ∀ (x x_1 : M),
    Eq.{u_5 + 1} (α := N)
      ((((HSMul.hSMul (α := ℕ) (β := BilinMap R M N) 2
                    (((associatedHom S : QuadraticMap R M N →ₗ[S] BilinMap R M N) :
                          (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)
          x_1 :
        N)
      ((((Q.polarBilin : (a : M) → M →ₗ[R] N) x : M →ₗ[R] N) : (a : M) → N) x_1 : N)
⊢ HSMul.hSMul (α := ℕ) (β := BilinMap R M N) 2
      (((associatedHom S : QuadraticMap R M N →ₗ[S] BilinMap R M N) : (a : QuadraticMap R M N) → BilinMap R M N) Q :
        BilinMap R M N) =
    Q.polarBilin

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basic
Goal:
S : Type u_1
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
inst_5 : CommSemiring S
inst_6 : Algebra S R
inst_7 : Module S N
inst_8 : IsScalarTower S R N
inst_9 : Invertible (α := Module.End R N) 2
Q : QuadraticMap R M N
x x_1 : M
h :
  HSMul.hSMul (α := ℕ) (β := N) 2
      ((@Invertible.invOf _ Module.End.instMul Module.End.instOne 2 _ : (a : N) → N)
          (HSub.hSub (β := N) (HSub.hSub (α := N) (β := N) ((Q : (a : M) → N) (x + x_1) : N) ((Q : (a : M) → N) x : N))
            ((Q : (a : M) → N) x_1 : N)) :
        N) =
    polar (⇑Q : (a : M) → N) x x_1
⊢ Eq.{u_5 + 1} (α := N)
    ((((HSMul.hSMul (α := ℕ) (β := BilinMap R M N) 2
                  (((associatedHom S : QuadraticMap R M N →ₗ[S] BilinMap R M N) :
                        (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)
        x_1 :
      N)
    ((((Q.polarBilin : (a : M) → M →ₗ[R] N) x : M →ₗ[R] N) : (a : M) → N) x_1 : N)

Tactic:
dsimp
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basic
Goal:
S : Type u_1
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
inst_5 : CommSemiring S
inst_6 : Algebra S R
inst_7 : Module S N
inst_8 : IsScalarTower S R N
inst_9 : Invertible (α := Module.End R N) 2
Q : QuadraticMap R M N
x x_1 : M
h :
  Eq (α := N)
    ((HSMul.hSMul (α := ℕ) (β := N →ₗ[R] N) 2 (@Invertible.invOf _ Module.End.instMul Module.End.instOne 2 _) :
          (a : N) → N)
        (HSub.hSub (β := N) (HSub.hSub (α := N) (β := N) ((Q : (a : M) → N) (x + x_1) : N) ((Q : (a : M) → N) x : N))
          ((Q : (a : M) → N) x_1 : N)) :
      N)
    (polar (⇑Q : (a : M) → N) x x_1 : N)
h₁ :
  Eq (α := N)
    ((HMul.hMul (α := N →ₗ[R] N) (↑2 : N →ₗ[R] N) (@Invertible.invOf _ Module.End.instMul Module.End.instOne 2 _) :
          (a : N) → N)
        (HSub.hSub (β := N) (HSub.hSub (α := N) (β := N) ((Q : (a : M) → N) (x + x_1) : N) ((Q : (a : M) → N) x : N))
          ((Q : (a : M) → N) x_1 : N)) :
      N)
    (polar (⇑Q : (a : M) → N) x x_1 : N)
h₂ :
  Eq (α := N)
    ((HMul.hMul (α := N →ₗ[R] N) 2 (@Invertible.invOf _ Module.End.instMul Module.End.instOne 2 _) : (a : N) → N)
        (HSub.hSub (β := N) (HSub.hSub (α := N) (β := N) ((Q : (a : M) → N) (x + x_1) : N) ((Q : (a : M) → N) x : N))
          ((Q : (a : M) → N) x_1 : N)) :
      N)
    (polar (⇑Q : (a : M) → N) x x_1 : N)
h₃ :
  Eq (α := N)
    ((1 : (a : N) → N)
        (HSub.hSub (β := N) (HSub.hSub (α := N) (β := N) ((Q : (a : M) → N) (x + x_1) : N) ((Q : (a : M) → N) x : N))
          ((Q : (a : M) → N) x_1 : N)) :
      N)
    (polar (⇑Q : (a : M) → N) x x_1 : N)
h₄ :
  HSub.hSub (β := N) (HSub.hSub (α := N) (β := N) ((Q : (a : M) → N) (x + x_1) : N) ((Q : (a : M) → N) x : N))
      ((Q : (a : M) → N) x_1 : N) =
    polar (⇑Q : (a : M) → N) x x_1
h₅ h₆ :
  HSub.hSub (β := N) (HSub.hSub (α := N) (β := N) ((Q : (a : M) → N) (x + x_1) : N) ((Q : (a : M) → N) x : N))
      ((Q : (a : M) → N) x_1 : N) =
    HSub.hSub (β := N) (HSub.hSub (α := N) (β := N) ((Q : (a : M) → N) (x + x_1) : N) ((Q : (a : M) → N) x : N))
      ((Q : (a : M) → N) x_1 : N)
⊢ HSMul.hSMul (α := ℕ) (β := N) 2
      ((@Invertible.invOf _ Module.End.instMul Module.End.instOne 2 _ : (a : N) → N)
          (HSub.hSub (β := N) (HSub.hSub (α := N) (β := N) ((Q : (a : M) → N) (x + x_1) : N) ((Q : (a : M) → N) x : N))
            ((Q : (a : M) → N) x_1 : N)) :
        N) =
    polar (⇑Q : (a : M) → N) x x_1

Tactic:
rw [← LinearMap.smul_apply, nsmul_eq_mul, Nat.cast_ofNat, mul_invOf_self', Module.End.one_apply,
    polar]

Premises used: Nat.cast_ofNat, LinearMap.smul_apply, QuadraticMap.polar, Module.End.one_apply, nsmul_eq_mul, mul_invOf_self'
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basic
Goal:
S : Type u_1
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
inst_5 : CommSemiring S
inst_6 : Algebra S R
inst_7 : Module S N
inst_8 : IsScalarTower S R N
inst_9 : Invertible (α := Module.End R N) 2
Q : QuadraticMap R M N
x y : M
⊢ Eq.{u_5 + 1} (α := N)
    (((((((associatedHom S : QuadraticMap R M N →ₗ[S] BilinMap R M N) : (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)
    (((((((associatedHom S : QuadraticMap R M N →ₗ[S] BilinMap R M N) : (a : QuadraticMap R M N) → BilinMap R M N) Q :
                  BilinMap R M N) :
                (a : M) → M →ₗ[R] N)
              y :
            M →ₗ[R] N) :
          (a : M) → N)
        x :
      N)

Tactic:
simp only [associated_apply, sub_eq_add_neg, add_assoc, add_comm, add_left_comm]

Premises used: add_left_comm, add_assoc, QuadraticMap.associated_apply, sub_eq_add_neg, add_comm
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basic
Goal:
S : Type u_1
R : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : CommSemiring S
inst_4 : Algebra S R
Q : QuadraticForm R M
inst_5 : Invertible (α := R) 2
⊢ LinearMap.IsSymm.{u_3, u_4} (R := R) (M := M) (I := RingHom.id R)
    (((associatedHom.{u_1, u_3, u_4, u_3} S (R := R) (M := M) (N := R) : QuadraticMap R M R →ₗ[S] BilinMap R M R) :
        (a : QuadraticMap R M R) → BilinMap R M R)
      Q)

Tactic:
⟨QuadraticMap.associated_isSymm S Q⟩

Premises used: LinearMap.IsSymm.mk, QuadraticMap.associated_isSymm
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basic
Goal:
S : Type u_1
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
inst_5 : CommSemiring S
inst_6 : Algebra S R
inst_7 : Module S N
inst_8 : IsScalarTower S R N
inst_9 : Invertible (α := Module.End R N) 2
Q : QuadraticMap R M N
h :
  ∀ (x x_1 : M),
    Eq.{u_5 + 1} (α := N)
      (((((LinearMap.flip
                      (((associatedHom S : QuadraticMap R M N →ₗ[S] BilinMap R M N) :
                          (a : QuadraticMap R M N) → BilinMap R M N)
                        Q) :
                    M →ₗ[R] M →ₗ[R] N) :
                  (a : M) → M →ₗ[R] N)
                x :
              M →ₗ[R] N) :
            (a : M) → N)
          x_1 :
        N)
      (((((((associatedHom S : QuadraticMap R M N →ₗ[S] BilinMap R M N) : (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)
          x_1 :
        N)
⊢ Eq (α := M →ₗ[R] M →ₗ[R] N)
    (LinearMap.flip
        (((associatedHom S : QuadraticMap R M N →ₗ[S] BilinMap R M N) : (a : QuadraticMap R M N) → BilinMap R M N) Q) :
      M →ₗ[R] M →ₗ[R] N)
    (((associatedHom S : QuadraticMap R M N →ₗ[S] BilinMap R M N) : (a : QuadraticMap R M N) → BilinMap R M N) Q :
      BilinMap R M N)

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basic
Goal:
S : Type u_1
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
inst_5 : CommSemiring S
inst_6 : Algebra S R
inst_7 : Module S N
inst_8 : IsScalarTower S R N
inst_9 : Invertible (α := Module.End R N) 2
Q : QuadraticMap R M N
x x_1 : M
⊢ Eq.{u_5 + 1} (α := N)
    (((((LinearMap.flip
                    (((associatedHom S : QuadraticMap R M N →ₗ[S] BilinMap R M N) :
                        (a : QuadraticMap R M N) → BilinMap R M N)
                      Q) :
                  M →ₗ[R] M →ₗ[R] N) :
                (a : M) → M →ₗ[R] N)
              x :
            M →ₗ[R] N) :
          (a : M) → N)
        x_1 :
      N)
    (((((((associatedHom S : QuadraticMap R M N →ₗ[S] BilinMap R M N) : (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)
        x_1 :
      N)

Tactic:
simp only [LinearMap.flip_apply, associated_apply, add_comm, sub_eq_add_neg, add_left_comm,
    add_assoc]

Premises used: add_left_comm, add_assoc, QuadraticMap.associated_apply, sub_eq_add_neg, LinearMap.flip_apply, add_comm
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basic
Goal:
S : Type u_1
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
inst_5 : CommSemiring S
inst_6 : Algebra S R
inst_7 : Module S N
inst_8 : IsScalarTower S R N
inst_9 : Invertible (α := Module.End R N) 2
Q : QuadraticMap R M N
N' : Type u_8
inst_10 : AddCommGroup N'
inst_11 : Module R N'
f : N' →ₗ[R] M
h :
  ∀ (x x_1 : N'),
    Eq.{u_5 + 1} (α := N)
      (((((((associatedHom S : QuadraticMap R N' N →ₗ[S] BilinMap R N' N) : (a : QuadraticMap R N' N) → BilinMap R N' N)
                      (Q.comp f) :
                    BilinMap R N' N) :
                  (a : N') → N' →ₗ[R] N)
                x :
              N' →ₗ[R] N) :
            (a : N') → N)
          x_1 :
        N)
      ((((LinearMap.compl₁₂
                    (((associatedHom S : QuadraticMap R M N →ₗ[S] BilinMap R M N) :
                        (a : QuadraticMap R M N) → BilinMap R M N)
                      Q)
                    f f :
                  (a : N') → N' →ₗ[R] N)
                x :
              N' →ₗ[R] N) :
            (a : N') → N)
          x_1 :
        N)
⊢ Eq (α := BilinMap R N' N)
    (((associatedHom S : QuadraticMap R N' N →ₗ[S] BilinMap R N' N) : (a : QuadraticMap R N' N) → BilinMap R N' N)
        (Q.comp f) :
      BilinMap R N' N)
    (LinearMap.compl₁₂
        (((associatedHom S : QuadraticMap R M N →ₗ[S] BilinMap R M N) : (a : QuadraticMap R M N) → BilinMap R M N) Q) f
        f :
      N' →ₗ[R] N' →ₗ[R] N)

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basic
Goal:
S : Type u_1
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
inst_5 : CommSemiring S
inst_6 : Algebra S R
inst_7 : Module S N
inst_8 : IsScalarTower S R N
inst_9 : Invertible (α := Module.End R N) 2
Q : QuadraticMap R M N
N' : Type u_8
inst_10 : AddCommGroup N'
inst_11 : Module R N'
f : N' →ₗ[R] M
x x_1 : N'
⊢ Eq.{u_5 + 1} (α := N)
    (((((((associatedHom S : QuadraticMap R N' N →ₗ[S] BilinMap R N' N) : (a : QuadraticMap R N' N) → BilinMap R N' N)
                    (Q.comp f) :
                  BilinMap R N' N) :
                (a : N') → N' →ₗ[R] N)
              x :
            N' →ₗ[R] N) :
          (a : N') → N)
        x_1 :
      N)
    ((((LinearMap.compl₁₂
                  (((associatedHom S : QuadraticMap R M N →ₗ[S] BilinMap R M N) :
                      (a : QuadraticMap R M N) → BilinMap R M N)
                    Q)
                  f f :
                (a : N') → N' →ₗ[R] N)
              x :
            N' →ₗ[R] N) :
          (a : N') → N)
        x_1 :
      N)

Tactic:
simp only [associated_apply, comp_apply, map_add, LinearMap.compl₁₂_apply]

Premises used: QuadraticMap.associated_apply, QuadraticMap.comp_apply, map_add, LinearMap.compl₁₂_apply
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basic
Goal:
S : Type u_1
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
inst_5 : CommSemiring S
inst_6 : Algebra S R
inst_7 : Module S N
inst_8 : IsScalarTower S R N
inst_9 : Invertible (α := Module.End R N) 2
B : BilinMap R M N
x y : M
simp :
  HSub.hSub (β := N)
      (HSub.hSub (β := N)
        (HAdd.hAdd (α := N) (β := N)
            ((@Invertible.invOf _ Module.End.instMul Module.End.instOne 2 _ : (a : N) → N)
                ((((B : (a : M) → M →ₗ[R] N) x : M →ₗ[R] N) : (a : M) → N) x : N) :
              N)
            ((@Invertible.invOf _ Module.End.instMul Module.End.instOne 2 _ : (a : N) → N)
                ((((B : (a : M) → M →ₗ[R] N) y : M →ₗ[R] N) : (a : M) → N) x : N) :
              N) +
          HAdd.hAdd (α := N) (β := N)
            ((@Invertible.invOf _ Module.End.instMul Module.End.instOne 2 _ : (a : N) → N)
                ((((B : (a : M) → M →ₗ[R] N) x : M →ₗ[R] N) : (a : M) → N) y : N) :
              N)
            ((@Invertible.invOf _ Module.End.instMul Module.End.instOne 2 _ : (a : N) → N)
                ((((B : (a : M) → M →ₗ[R] N) y : M →ₗ[R] N) : (a : M) → N) y : N) :
              N))
        ((@Invertible.invOf _ Module.End.instMul Module.End.instOne 2 _ : (a : N) → N)
            ((((B : (a : M) → M →ₗ[R] N) x : M →ₗ[R] N) : (a : M) → N) x : N) :
          N))
      ((@Invertible.invOf _ Module.End.instMul Module.End.instOne 2 _ : (a : N) → N)
          ((((B : (a : M) → M →ₗ[R] N) y : M →ₗ[R] N) : (a : M) → N) y : N) :
        N) =
    HAdd.hAdd (α := N) (β := N)
      ((@Invertible.invOf _ Module.End.instMul Module.End.instOne 2 _ : (a : N) → N)
          ((((B : (a : M) → M →ₗ[R] N) x : M →ₗ[R] N) : (a : M) → N) y : N) :
        N)
      ((@Invertible.invOf _ Module.End.instMul Module.End.instOne 2 _ : (a : N) → N)
          ((((B : (a : M) → M →ₗ[R] N) y : M →ₗ[R] N) : (a : M) → N) x : N) :
        N)
⊢ ((((((associatedHom S : QuadraticMap R M N →ₗ[S] BilinMap R M N) : (a : QuadraticMap R M N) → BilinMap R M N)
                  B.toQuadraticMap :
                BilinMap R M N) :
              (a : M) → M →ₗ[R] N)
            x :
          M →ₗ[R] N) :
        (a : M) → N)
      y =
    HSMul.hSMul (α := Module.End R N) (@Invertible.invOf _ Module.End.instMul Module.End.instOne 2 _)
      (HAdd.hAdd (α := N) (β := N) ((((B : (a : M) → M →ₗ[R] N) x : M →ₗ[R] N) : (a : M) → N) y : N)
        ((((B : (a : M) → M →ₗ[R] N) y : M →ₗ[R] N) : (a : M) → N) x : N))

Tactic:
simp only [associated_apply, BilinMap.toQuadraticMap_apply, map_add, LinearMap.add_apply,
    Module.End.smul_def, map_sub]

Premises used: Module.End.smul_def, map_sub, LinearMap.add_apply, QuadraticMap.associated_apply, map_add, LinearMap.BilinMap.toQuadraticMap_apply
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basic
Goal:
S : Type u_1
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
inst_5 : CommSemiring S
inst_6 : Algebra S R
inst_7 : Module S N
inst_8 : IsScalarTower S R N
inst_9 : Invertible (α := Module.End R N) 2
B : BilinMap R M N
x y : M
⊢ HSub.hSub (β := N)
      (HSub.hSub (β := N)
        (HAdd.hAdd (α := N) (β := N)
            ((@Invertible.invOf _ Module.End.instMul Module.End.instOne 2 _ : (a : N) → N)
                ((((B : (a : M) → M →ₗ[R] N) x : M →ₗ[R] N) : (a : M) → N) x : N) :
              N)
            ((@Invertible.invOf _ Module.End.instMul Module.End.instOne 2 _ : (a : N) → N)
                ((((B : (a : M) → M →ₗ[R] N) y : M →ₗ[R] N) : (a : M) → N) x : N) :
              N) +
          HAdd.hAdd (α := N) (β := N)
            ((@Invertible.invOf _ Module.End.instMul Module.End.instOne 2 _ : (a : N) → N)
                ((((B : (a : M) → M →ₗ[R] N) x : M →ₗ[R] N) : (a : M) → N) y : N) :
              N)
            ((@Invertible.invOf _ Module.End.instMul Module.End.instOne 2 _ : (a : N) → N)
                ((((B : (a : M) → M →ₗ[R] N) y : M →ₗ[R] N) : (a : M) → N) y : N) :
              N))
        ((@Invertible.invOf _ Module.End.instMul Module.End.instOne 2 _ : (a : N) → N)
            ((((B : (a : M) → M →ₗ[R] N) x : M →ₗ[R] N) : (a : M) → N) x : N) :
          N))
      ((@Invertible.invOf _ Module.End.instMul Module.End.instOne 2 _ : (a : N) → N)
          ((((B : (a : M) → M →ₗ[R] N) y : M →ₗ[R] N) : (a : M) → N) y : N) :
        N) =
    HAdd.hAdd (α := N) (β := N)
      ((@Invertible.invOf _ Module.End.instMul Module.End.instOne 2 _ : (a : N) → N)
          ((((B : (a : M) → M →ₗ[R] N) x : M →ₗ[R] N) : (a : M) → N) y : N) :
        N)
      ((@Invertible.invOf _ Module.End.instMul Module.End.instOne 2 _ : (a : N) → N)
          ((((B : (a : M) → M →ₗ[R] N) y : M →ₗ[R] N) : (a : M) → N) x : N) :
        N)

Tactic:
abel_nf
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basic
Goal:
S : Type u_1
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
inst_5 : CommSemiring S
inst_6 : Algebra S R
inst_7 : Module S N
inst_8 : IsScalarTower S R N
inst_9 : Invertible (α := Module.End R N) 2
B₁ : BilinMap R M N
h :
  ∀ (x y : M),
    Eq.{u_5 + 1} (α := N) ((((B₁ : (a : M) → M →ₗ[R] N) x : M →ₗ[R] N) : (a : M) → N) y : N)
      ((((B₁ : (a : M) → M →ₗ[R] N) y : M →ₗ[R] N) : (a : M) → N) x : N)
x y : M
rw :
  HSMul.hSMul (α := Module.End R N) (@Invertible.invOf _ Module.End.instMul Module.End.instOne 2 _)
      (HAdd.hAdd (α := N) (β := N) ((((B₁ : (a : M) → M →ₗ[R] N) x : M →ₗ[R] N) : (a : M) → N) y : N)
        ((((B₁ : (a : M) → M →ₗ[R] N) y : M →ₗ[R] N) : (a : M) → N) x : N)) =
    (((B₁ : (a : M) → M →ₗ[R] N) x : M →ₗ[R] N) : (a : M) → N) y
rw₁ :
  HSMul.hSMul (α := Module.End R N) (@Invertible.invOf _ Module.End.instMul Module.End.instOne 2 _)
      (HAdd.hAdd (α := N) (β := N) ((((B₁ : (a : M) → M →ₗ[R] N) x : M →ₗ[R] N) : (a : M) → N) y : N)
        ((((B₁ : (a : M) → M →ₗ[R] N) x : M →ₗ[R] N) : (a : M) → N) y : N)) =
    (((B₁ : (a : M) → M →ₗ[R] N) x : M →ₗ[R] N) : (a : M) → N) y
rw₂ :
  HSMul.hSMul (α := Module.End R N) (@Invertible.invOf _ Module.End.instMul Module.End.instOne 2 _)
      (HSMul.hSMul.{u_3, u_5, u_5} (α := R) (β := N) 2
        ((((B₁ : (a : M) → M →ₗ[R] N) x : M →ₗ[R] N) : (a : M) → N) y : N)) =
    (((B₁ : (a : M) → M →ₗ[R] N) x : M →ₗ[R] N) : (a : M) → N) y
rw₃ :
  HSMul.hSMul.{u_3, u_5, u_5} (α := R) (β := N) 2 ((((B₁ : (a : M) → M →ₗ[R] N) x : M →ₗ[R] N) : (a : M) → N) y : N) =
    HSMul.hSMul (α := Module.End R N) (β := N) 2 ((((B₁ : (a : M) → M →ₗ[R] N) x : M →ₗ[R] N) : (a : M) → N) y : N)
rw₄ :
  HAdd.hAdd (α := N) (β := N) ((((B₁ : (a : M) → M →ₗ[R] N) x : M →ₗ[R] N) : (a : M) → N) y : N)
      ((((B₁ : (a : M) → M →ₗ[R] N) x : M →ₗ[R] N) : (a : M) → N) y : N) =
    HSMul.hSMul (α := Module.End R N) (β := N) 2 ((((B₁ : (a : M) → M →ₗ[R] N) x : M →ₗ[R] N) : (a : M) → N) y : N)
rw₅ rw₆ :
  HAdd.hAdd (α := N) (β := N) ((((B₁ : (a : M) → M →ₗ[R] N) x : M →ₗ[R] N) : (a : M) → N) y : N)
      ((((B₁ : (a : M) → M →ₗ[R] N) x : M →ₗ[R] N) : (a : M) → N) y : N) =
    HAdd.hAdd (α := N) (β := N) ((((B₁ : (a : M) → M →ₗ[R] N) x : M →ₗ[R] N) : (a : M) → N) y : N)
      ((((B₁ : (a : M) → M →ₗ[R] N) x : M →ₗ[R] N) : (a : M) → N) y : N)
⊢ Eq.{u_5 + 1} (α := N)
    (((((((associatedHom S : QuadraticMap R M N →ₗ[S] BilinMap R M N) : (a : QuadraticMap R M N) → BilinMap R M N)
                    B₁.toQuadraticMap :
                  BilinMap R M N) :
                (a : M) → M →ₗ[R] N)
              x :
            M →ₗ[R] N) :
          (a : M) → N)
        y :
      N)
    ((((B₁ : (a : M) → M →ₗ[R] N) x : M →ₗ[R] N) : (a : M) → N) y : N)

Tactic:
rw [associated_toQuadraticMap, ← h x y, ← two_smul R, invOf_smul_eq_iff, two_smul, two_smul]

Premises used: two_smul, QuadraticMap.associated_toQuadraticMap, invOf_smul_eq_iff