awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basic (goal)
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
⊢ 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)
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basic (goal)
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
⊢ 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)
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basic (goal)
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
⊢ ((((((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))
have 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)
Tactic: simp only [associated_apply, BilinMap.toQuadraticMap_apply, map_add, LinearMap.add_apply,
    Module.End.smul_def, map_sub]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basic (goal)
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
⊢ 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)
have 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
Tactic: rw [associated_toQuadraticMap, ← h x y, ← two_smul R, invOf_smul_eq_iff, two_smul, two_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basic (goal)
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
⊢ 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)
have 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
Tactic: rw [associated_toQuadraticMap, ← h x y, ← two_smul R, invOf_smul_eq_iff, two_smul, two_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basic (goal)
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
⊢ 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)
have 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
Tactic: rw [associated_toQuadraticMap, ← h x y, ← two_smul R, invOf_smul_eq_iff, two_smul, two_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basic (goal)
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
⊢ 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)
have 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)
Tactic: rw [associated_toQuadraticMap, ← h x y, ← two_smul R, invOf_smul_eq_iff, two_smul, two_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basic (goal)
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)
⊢ 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)
have 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)
Tactic: rw [associated_toQuadraticMap, ← h x y, ← two_smul R, invOf_smul_eq_iff, two_smul, two_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basic (goal)
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)
⊢ 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)
have 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)
Tactic: rw [associated_toQuadraticMap, ← h x y, ← two_smul R, invOf_smul_eq_iff, two_smul, two_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basic (goal)
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
hB₁ : LinearMap.flip B₁ = B₁
⊢ ((associatedHom S : QuadraticMap R M N →ₗ[S] BilinMap R M N) : (a : QuadraticMap R M N) → BilinMap R M N)
      B₁.toQuadraticMap =
    B₁
have h : ∀ (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)
                    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: ext _ y
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basic (goal)
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
hB₁ : LinearMap.flip B₁ = B₁
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)
                    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)
have h : 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
Tactic: rw [associated_toQuadraticMap, ← LinearMap.flip_apply _ y, hB₁, invOf_smul_eq_iff, two_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basic (goal)
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
hB₁ : LinearMap.flip B₁ = B₁
x y : M
h :
  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
⊢ 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)
have h₁ : 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)
      ((((LinearMap.flip 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
Tactic: rw [associated_toQuadraticMap, ← LinearMap.flip_apply _ y, hB₁, invOf_smul_eq_iff, two_smul]