awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
hB₁ : LinearMap.flip B₁ = B₁
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)
⊢ ((associatedHom S : QuadraticMap R M N →ₗ[S] BilinMap R M N) : (a : QuadraticMap R M N) → BilinMap R M N)
      B₁.toQuadraticMap =
    B₁

Tactic:
ext _ y
-- 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
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
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
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) x : M →ₗ[R] N) : (a : M) → N) y : N)) =
    (((B₁ : (a : M) → M →ₗ[R] N) x : M →ₗ[R] N) : (a : M) → N) y
h₃ :
  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)
h₄ h₅ :
  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, ← LinearMap.flip_apply _ y, hB₁, invOf_smul_eq_iff, two_smul]

Premises used: two_smul, QuadraticMap.associated_toQuadraticMap, LinearMap.flip_apply, invOf_smul_eq_iff
-- 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
⊢ BilinMap.toQuadraticMap
      (((associatedHom S : QuadraticMap R M N →ₗ[S] BilinMap R M N) : (a : QuadraticMap R M N) → BilinMap R M N) Q) =
    Q

Tactic:
QuadraticMap.ext <| associated_eq_self_apply S Q

Premises used: QuadraticMap.ext, QuadraticMap.associated_eq_self_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
⊢ Function.RightInverse (α := BilinMap R M N)
    (⇑(associatedHom S : QuadraticMap R M N →ₗ[S] BilinMap R M N) : (a : QuadraticMap R M N) → BilinMap R M N)
    BilinMap.toQuadraticMap

Tactic:
toQuadraticMap_associated S

Premises used: Function.LeftInverse, QuadraticMap.toQuadraticMap_associated, Function.RightInverse
-- 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 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : Invertible (α := Module.End R N) 2
Q : QuadraticMap R M N
hB₁ :
  Ne (α := BilinMap R M N) ((associated' : (a : QuadraticMap R M N) → BilinMap R M N) Q : BilinMap R M N)
    (0 : BilinMap R M N)
rw : ¬∀ (x : M), Eq.{u_5 + 1} (α := N) ((Q : (a : M) → N) x : N) (0 : N)
⊢ ∃ (x : M), Ne.{u_5 + 1} (α := N) ((Q : (a : M) → N) x : N) (0 : N)

Tactic:
rw [← not_forall]

Premises used: Classical.not_forall
-- 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 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : Invertible (α := Module.End R N) 2
Q : QuadraticMap R M N
hB₁ :
  Ne (α := BilinMap R M N) ((associated' : (a : QuadraticMap R M N) → BilinMap R M N) Q : BilinMap R M N)
    (0 : BilinMap R M N)
h : ∀ (x : M), Eq.{u_5 + 1} (α := N) ((Q : (a : M) → N) x : N) (0 : N)
apply :
  Eq (α := BilinMap R M N) ((associated' : (a : QuadraticMap R M N) → BilinMap R M N) Q : BilinMap R M N)
    (0 : BilinMap R M N)
⊢ False

Tactic:
apply hB₁
-- 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 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : Invertible (α := Module.End R N) 2
Q : QuadraticMap R M N
hB₁ :
  Ne (α := BilinMap R M N) ((associated' : (a : QuadraticMap R M N) → BilinMap R M N) Q : BilinMap R M N)
    (0 : BilinMap R M N)
h : ∀ (x : M), Eq.{u_5 + 1} (α := N) ((Q : (a : M) → N) x : N) (0 : N)
rw : Eq (α := BilinMap R M N) ((associated' : (a : QuadraticMap R M N) → BilinMap R M N) 0) 0
rw₁ rw₂ : Eq (α := BilinMap R M N) 0 0
⊢ Eq (α := BilinMap R M N) ((associated' : (a : QuadraticMap R M N) → BilinMap R M N) Q : BilinMap R M N)
    (0 : BilinMap R M N)

Tactic:
rw [(QuadraticMap.ext h : Q = 0), map_zero]

Premises used: QuadraticMap.ext, map_zero
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basic
Goal:
S : Type u_1
R : Type u_3
M : Type u_4
N : Type u_5
inst : CommSemiring S
inst_1 : CommRing R
inst_2 : AddCommGroup M
inst_3 : Algebra S R
inst_4 : Module R M
inst_5 : AddCommGroup N
inst_6 : Module R N
inst_7 : Module S N
inst_8 : IsScalarTower S R N
inst_9 : Invertible (α := Module.End R N) 2
⊢ Eq (α := (a : QuadraticMap R M N) → BilinMap R M N)
    (⇑(associatedHom S : QuadraticMap R M N →ₗ[S] BilinMap R M N) : (a : QuadraticMap R M N) → BilinMap R M N)
    (⇑associated : (a : QuadraticMap R M N) → BilinMap R M N)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basic
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
f g : M →ₗ[R] R
h :
  ∀ (x x_1 : M),
    Eq.{u_3 + 1} (α := R)
      (((((((associated.{u_3, u_4, u_3} (R := R) (M := M) (N := R) : QuadraticMap R M R →ₗ[R] BilinMap R M R) :
                        (a : QuadraticMap R M R) → BilinMap R M R)
                      (linMulLin f g) :
                    BilinMap R M R) :
                  (a : M) → M →ₗ[R] R)
                x :
              M →ₗ[R] R) :
            (a : M) → R)
          x_1 :
        R)
      ((((HSMul.hSMul (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
                    (compl₁₂ (mul R R) f g + compl₁₂ (mul R R) g f) :
                  (a : M) → M →ₗ[R] R)
                x :
              M →ₗ[R] R) :
            (a : M) → R)
          x_1 :
        R)
⊢ ((associated.{u_3, u_4, u_3} (R := R) (M := M) (N := R) : QuadraticMap R M R →ₗ[R] BilinMap R M R) :
        (a : QuadraticMap R M R) → BilinMap R M R)
      (linMulLin f g) =
    HSMul.hSMul (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
      (compl₁₂ (mul R R) f g + compl₁₂ (mul R R) g f)

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basic
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
f g : M →ₗ[R] R
x x_1 : M
h :
  HAdd.hAdd (α := R) (β := R) ((f : (a : M) → R) x : R) ((f : (a : M) → R) x_1 : R) *
          HAdd.hAdd (α := R) (β := R) ((g : (a : M) → R) x : R) ((g : (a : M) → R) x_1 : R) -
        HMul.hMul (α := R) (β := R) ((f : (a : M) → R) x : R) ((g : (a : M) → R) x : R) -
      HMul.hMul (α := R) (β := R) ((f : (a : M) → R) x_1 : R) ((g : (a : M) → R) x_1 : R) =
    HSMul.hSMul (α := Module.End R R) 2
        (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _ *
          HMul.hMul (α := R) (β := R) ((f : (a : M) → R) x : R) ((g : (a : M) → R) x_1 : R)) +
      HSMul.hSMul (α := Module.End R R) 2
        (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _ *
          HMul.hMul (α := R) (β := R) ((g : (a : M) → R) x : R) ((f : (a : M) → R) x_1 : R))
⊢ Eq.{u_3 + 1} (α := R)
    (((((((associated.{u_3, u_4, u_3} (R := R) (M := M) (N := R) : QuadraticMap R M R →ₗ[R] BilinMap R M R) :
                      (a : QuadraticMap R M R) → BilinMap R M R)
                    (linMulLin f g) :
                  BilinMap R M R) :
                (a : M) → M →ₗ[R] R)
              x :
            M →ₗ[R] R) :
          (a : M) → R)
        x_1 :
      R)
    ((((HSMul.hSMul (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
                  (compl₁₂ (mul R R) f g + compl₁₂ (mul R R) g f) :
                (a : M) → M →ₗ[R] R)
              x :
            M →ₗ[R] R) :
          (a : M) → R)
        x_1 :
      R)

Tactic:
simp only [associated_apply, linMulLin_apply, map_add, smul_add, LinearMap.add_apply,
    LinearMap.smul_apply, compl₁₂_apply, mul_apply', smul_eq_mul, invOf_smul_eq_iff]

Premises used: QuadraticMap.linMulLin_apply, LinearMap.smul_apply, LinearMap.mul_apply', LinearMap.add_apply, QuadraticMap.associated_apply, map_add, LinearMap.compl₁₂_apply, invOf_smul_eq_iff, smul_eq_mul, smul_add
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basic
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
f g : M →ₗ[R] R
x x_1 : M
h :
  HAdd.hAdd (α := R) (β := R) ((f : (a : M) → R) x : R) ((f : (a : M) → R) x_1 : R) *
          HAdd.hAdd (α := R) (β := R) ((g : (a : M) → R) x : R) ((g : (a : M) → R) x_1 : R) -
        HMul.hMul (α := R) (β := R) ((f : (a : M) → R) x : R) ((g : (a : M) → R) x : R) -
      HMul.hMul (α := R) (β := R) ((f : (a : M) → R) x_1 : R) ((g : (a : M) → R) x_1 : R) =
    HMul.hMul (α := R) (β := R) ((f : (a : M) → R) x : R) ((g : (a : M) → R) x_1 : R) +
      HMul.hMul (α := R) (β := R) ((g : (a : M) → R) x : R) ((f : (a : M) → R) x_1 : R)
⊢ HAdd.hAdd (α := R) (β := R) ((f : (a : M) → R) x : R) ((f : (a : M) → R) x_1 : R) *
          HAdd.hAdd (α := R) (β := R) ((g : (a : M) → R) x : R) ((g : (a : M) → R) x_1 : R) -
        HMul.hMul (α := R) (β := R) ((f : (a : M) → R) x : R) ((g : (a : M) → R) x : R) -
      HMul.hMul (α := R) (β := R) ((f : (a : M) → R) x_1 : R) ((g : (a : M) → R) x_1 : R) =
    HSMul.hSMul (α := Module.End R R) 2
        (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _ *
          HMul.hMul (α := R) (β := R) ((f : (a : M) → R) x : R) ((g : (a : M) → R) x_1 : R)) +
      HSMul.hSMul (α := Module.End R R) 2
        (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _ *
          HMul.hMul (α := R) (β := R) ((g : (a : M) → R) x : R) ((f : (a : M) → R) x_1 : R))

Tactic:
simp only [Module.End.smul_def, Module.End.ofNat_apply, nsmul_eq_mul, Nat.cast_ofNat,
    mul_invOf_cancel_left']

Premises used: Nat.cast_ofNat, Module.End.smul_def, nsmul_eq_mul, Module.End.ofNat_apply, mul_invOf_cancel_left'
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basic
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
f g : M →ₗ[R] R
x x_1 : M
⊢ HAdd.hAdd (α := R) (β := R) ((f : (a : M) → R) x : R) ((f : (a : M) → R) x_1 : R) *
          HAdd.hAdd (α := R) (β := R) ((g : (a : M) → R) x : R) ((g : (a : M) → R) x_1 : R) -
        HMul.hMul (α := R) (β := R) ((f : (a : M) → R) x : R) ((g : (a : M) → R) x : R) -
      HMul.hMul (α := R) (β := R) ((f : (a : M) → R) x_1 : R) ((g : (a : M) → R) x_1 : R) =
    HMul.hMul (α := R) (β := R) ((f : (a : M) → R) x : R) ((g : (a : M) → R) x_1 : R) +
      HMul.hMul (α := R) (β := R) ((g : (a : M) → R) x : R) ((f : (a : M) → R) x_1 : R)

Tactic:
ring_nf
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basic
Goal:
R : Type u_3
inst : CommRing R
inst_1 : Invertible (α := R) 2
simp : Eq (α := BilinMap R R R) (compl₁₂ (mul R R) LinearMap.id LinearMap.id) (mul R R)
⊢ HSMul.hSMul (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
      (HAdd.hAdd (α := R →ₗ[R] R →ₗ[R] R) (compl₁₂ (mul R R) LinearMap.id LinearMap.id)
        (compl₁₂ (mul R R) LinearMap.id LinearMap.id)) =
    mul R R

Tactic:
simp only [smul_add, invOf_two_smul_add_invOf_two_smul]

Premises used: invOf_two_smul_add_invOf_two_smul, smul_add
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basic
Goal:
R : Type u_3
inst : CommRing R
inst_1 : Invertible (α := R) 2
⊢ Eq (α := BilinMap R R R) (compl₁₂ (mul R R) LinearMap.id LinearMap.id) (mul R R)

Tactic:
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
x y : M
⊢ Q.IsOrtho x y ↔
    (Q : (a : M) → N) (x + y) = HAdd.hAdd (α := N) (β := N) ((Q : (a : M) → N) x : N) ((Q : (a : M) → N) y : N)

Tactic:
Iff.rfl

Premises used: Iff.rfl, QuadraticMap.IsOrtho
-- 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
x y : M
⊢ IsOrtho.{u_3, u_4, u_5} (R := R) (N := N) 0 x y

Tactic:
(zero_add _).symm

Premises used: zero_add, Eq.symm, QuadraticMap.IsOrtho
-- 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
⊢ Q.IsOrtho 0 x

Tactic:
simp [isOrtho_def]

Premises used: QuadraticMap.isOrtho_def
-- 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
⊢ Q.IsOrtho x 0

Tactic:
simp [isOrtho_def]

Premises used: QuadraticMap.isOrtho_def
-- 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
hx₁ : ¬Q.IsOrtho x x
⊢ x ≠ 0

Tactic:
fun hx₂ => hx₁ (hx₂.symm ▸ .zero_left _)

Premises used: Eq.rec, QuadraticMap.IsOrtho.zero_left, OfNat.ofNat, Eq.symm, Not
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basic
Goal:
R : Type u_3
M : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : IsCancelAdd R
inst_4 : NoZeroDivisors R
inst_5 : CharZero R
B : BilinMap R M R
x y : M
h : LinearMap.IsSymm B
this : AddCancelMonoid R :=
  let __src := inst_3;
  let __src_1 : AddCommMonoid R := inferInstance;
  { toAddMonoid := __src_1.toAddMonoid, toIsLeftCancelAdd := ⋯, toIsRightCancelAdd := ⋯ }
simp_rw :
  HAdd.hAdd (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
          ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) y : R) +
        HAdd.hAdd (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) x : R)
          ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R) =
      HAdd.hAdd (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
        ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) y : R) ↔
    Eq.{u_3 + 1} (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R) (0 : R)
⊢ B.toQuadraticMap.IsOrtho x y ↔ LinearMap.IsOrtho B x y

Tactic:
simp_rw [isOrtho_def, LinearMap.isOrtho_def, B.toQuadraticMap_apply, map_add,
    LinearMap.add_apply, add_comm _ (B y y), add_add_add_comm _ _ (B y y), add_comm (B y y)]

Premises used: LinearMap.add_apply, QuadraticMap.isOrtho_def, map_add, add_comm, add_add_add_comm, LinearMap.BilinMap.toQuadraticMap_apply, DFunLike.coe, LinearMap.isOrtho_def
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basic
Goal:
R : Type u_3
M : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : IsCancelAdd R
inst_4 : NoZeroDivisors R
inst_5 : CharZero R
B : BilinMap R M R
x y : M
h : LinearMap.IsSymm B
this : AddCancelMonoid R :=
  let __src := inst_3;
  let __src_1 : AddCommMonoid R := inferInstance;
  { toAddMonoid := __src_1.toAddMonoid, toIsLeftCancelAdd := ⋯, toIsRightCancelAdd := ⋯ }
rw :
  HAdd.hAdd (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) x : R)
        ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R) =
      0 ↔
    Eq.{u_3 + 1} (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R) (0 : R)
rw₁ :
  HAdd.hAdd (α := R) (β := R)
        ((RingHom.id R : (a : R) → R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R) : R)
        ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R) =
      0 ↔
    Eq.{u_3 + 1} (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R) (0 : R)
rw₂ :
  HAdd.hAdd (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)
        ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R) =
      0 ↔
    Eq.{u_3 + 1} (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R) (0 : R)
rw₃ rw₄ :
  Eq.{u_3 + 1} (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R) (0 : R) ↔
    Eq.{u_3 + 1} (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R) (0 : R)
⊢ HAdd.hAdd (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
          ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) y : R) +
        HAdd.hAdd (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) x : R)
          ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R) =
      HAdd.hAdd (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
        ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) y : R) ↔
    Eq.{u_3 + 1} (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R) (0 : R)

Tactic:
rw [add_eq_left (a := B x x + B y y), ← h.eq, RingHom.id_apply, add_self_eq_zero]

Premises used: RingHom.id_apply, add_self_eq_zero, LinearMap.IsSymm.eq, add_eq_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 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
Q : QuadraticMap R M N
x y : M
simp_rw :
  LinearMap.IsOrtho Q.polarBilin 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) ((((Q.polarBilin : (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₂ :
  Eq.{u_5 + 1} (α := N) (polar (⇑Q : (a : M) → N) x y) 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)
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)
⊢ LinearMap.IsOrtho Q.polarBilin x y ↔ Q.IsOrtho x y

Tactic:
simp_rw [isOrtho_def, LinearMap.isOrtho_def, polarBilin_apply_apply, polar, sub_sub, sub_eq_zero]

Premises used: sub_eq_zero, QuadraticMap.isOrtho_def, QuadraticMap.polar, sub_sub, LinearMap.isOrtho_def, QuadraticMap.polarBilin_apply_apply
-- 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 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
Q : QuadraticMap R M N
x y : M
h : Q.IsOrtho x y
⊢ Eq.{u_5 + 1} (α := N) (polar (⇑Q : (a : M) → N) x y) 0

Tactic:
isOrtho_polarBilin.mpr h

Premises used: Iff.mpr, LinearMap.IsOrtho, QuadraticMap.polar, QuadraticMap.isOrtho_polarBilin