-- 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)
    ((((⋯.choose (p := fun (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)) :
                (a : M) → M →ₗ[R] N)
              x :
            M →ₗ[R] N) :
          (a : M) → N)
        y :
      N)
    (polar (⇑Q : (a : M) → N) x y : N)
rw₁ :
  (((⋯.choose (p := fun (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)) :
              (a : M) → M →ₗ[R] N)
            x :
          M →ₗ[R] N) :
        (a : M) → N)
      y =
    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)
rw₂ :
  (((⋯.choose (p := fun (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)) :
              (a : M) → M →ₗ[R] N)
            x :
          M →ₗ[R] N) :
        (a : M) → N)
      y =
    HSub.hSub (β := N)
      (HSub.hSub (β := N)
        (HAdd.hAdd (β := N) (HAdd.hAdd (α := N) (β := N) ((Q : (a : M) → N) x : N) ((Q : (a : M) → N) y : N))
          ((((⋯.choose (p := fun (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)) :
                      (a : M) → M →ₗ[R] N)
                    x :
                  M →ₗ[R] N) :
                (a : M) → N)
              y :
            N))
        ((Q : (a : M) → N) x : N))
      ((Q : (a : M) → N) y : N)
rw₃ :
  (((⋯.choose (p := fun (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)) :
              (a : M) → M →ₗ[R] N)
            x :
          M →ₗ[R] N) :
        (a : M) → N)
      y =
    HAdd.hAdd (β := N) (HAdd.hAdd (α := N) (β := N) ((Q : (a : M) → N) x : N) ((Q : (a : M) → N) y : N))
        ((((⋯.choose (p := fun (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)) :
                    (a : M) → M →ₗ[R] N)
                  x :
                M →ₗ[R] N) :
              (a : M) → N)
            y :
          N) -
      HAdd.hAdd (α := N) (β := N) ((Q : (a : M) → N) x : N) ((Q : (a : M) → N) y : N)
rw₄ rw₅ :
  Eq.{u_5 + 1} (α := N)
    ((((⋯.choose (p := fun (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)) :
                (a : M) → M →ₗ[R] N)
              x :
            M →ₗ[R] N) :
          (a : M) → N)
        y :
      N)
    ((((⋯.choose (p := fun (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)) :
                (a : M) → M →ₗ[R] N)
              x :
            M →ₗ[R] N) :
          (a : M) → N)
        y :
      N)
⊢ Eq.{u_5 + 1} (α := N)
    ((((⋯.choose (p := fun (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)) :
                (a : M) → M →ₗ[R] N)
              x :
            M →ₗ[R] N) :
          (a : M) → N)
        y :
      N)
    ((((Q.polarBilin : (a : M) → M →ₗ[R] N) x : M →ₗ[R] N) : (a : M) → N) y : N)

Tactic:
rw [polarBilin_apply_apply, polar, Q.exists_companion.choose_spec, sub_sub,
      add_sub_cancel_left]

Premises used: Exists.choose_spec, add_sub_cancel_left, QuadraticMap.polar, sub_sub, QuadraticMap.exists_companion, QuadraticMap.polarBilin_apply_apply