awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basic
Goal:
ι : Type u_8
inst : Fintype ι
R : Type u_9
M : Type u_10
inst_1 : CommRing R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : Invertible (α := R) 2
Q : QuadraticForm R M
v : Basis ι R M
hv₂ :
  LinearMap.IsOrthoᵢ.{u_9, u_9, u_9, u_10, u_8} (R := R) (R₁ := R) (M := R) (M₁ := M) (n := ι) (I₁ := RingHom.id R)
    (I₁' := RingHom.id R)
    (((associated.{u_9, u_10, u_9} (R := R) (M := M) (N := R) : QuadraticMap R M R →ₗ[R] BilinMap R M R) :
        (a : QuadraticMap R M R) → BilinMap R M R)
      Q)
    (⇑v : (a : ι) → M)
H :
  ∀ (w : ι → R),
    Eq.{u_9 + 1} (α := R) ((basisRepr Q v : (a : ι → R) → R) w : R)
      ((weightedSumSquares (S := R) R fun (i : ι) ↦ (Q : (a : M) → R) ((v : (a : ι) → M) i : M) : (a : ι → R) → R) w :
        R)
⊢ basisRepr Q v = weightedSumSquares (S := R) R fun (i : ι) ↦ (Q : (a : M) → R) ((v : (a : ι) → M) i : M)

Tactic:
ext w
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basic
Goal:
ι : Type u_8
inst : Fintype ι
R : Type u_9
M : Type u_10
inst_1 : CommRing R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : Invertible (α := R) 2
Q : QuadraticForm R M
v : Basis ι R M
hv₂ :
  LinearMap.IsOrthoᵢ.{u_9, u_9, u_9, u_10, u_8} (R := R) (R₁ := R) (M := R) (M₁ := M) (n := ι) (I₁ := RingHom.id R)
    (I₁' := RingHom.id R)
    (((associated.{u_9, u_10, u_9} (R := R) (M := M) (N := R) : QuadraticMap R M R →ₗ[R] BilinMap R M R) :
        (a : QuadraticMap R M R) → BilinMap R M R)
      Q)
    (⇑v : (a : ι) → M)
w : ι → R
H :
  Eq.{u_9 + 1} (α := R)
    (∑ x : ι,
      (((((associatedHom.{u_9, u_9, u_10, u_9} R (R := R) (M := M) (N := R) : QuadraticMap R M R →ₗ[R] BilinMap R M R) :
                    (a : QuadraticMap R M R) → BilinMap R M R)
                  Q :
                BilinMap R M R) :
              (a : M) → M →ₗ[R] R)
            (∑ i : ι, HSMul.hSMul (β := M) (w i) ((v : (a : ι) → M) i : M)) :
          (a : M) → R)
        (HSMul.hSMul (β := M) (w x) ((v : (a : ι) → M) x : M)))
    (∑ i : ι, HSMul.hSMul (α := R) ((Q : (a : M) → R) ((v : (a : ι) → M) i : M) : R) (w i * w i))
⊢ Eq.{u_9 + 1} (α := R) ((basisRepr Q v : (a : ι → R) → R) w : R)
    ((weightedSumSquares (S := R) R fun (i : ι) ↦ (Q : (a : M) → R) ((v : (a : ι) → M) i : M) : (a : ι → R) → R) w : R)

Tactic:
rw [basisRepr_apply, ← @associated_eq_self_apply R, map_sum, weightedSumSquares_apply]

Premises used: QuadraticMap.associated_eq_self_apply, map_sum, QuadraticMap.weightedSumSquares_apply, QuadraticMap.basisRepr_apply
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basic
Goal:
ι : Type u_8
inst : Fintype ι
R : Type u_9
M : Type u_10
inst_1 : CommRing R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : Invertible (α := R) 2
Q : QuadraticForm R M
v : Basis ι R M
hv₂ :
  LinearMap.IsOrthoᵢ.{u_9, u_9, u_9, u_10, u_8} (R := R) (R₁ := R) (M := R) (M₁ := M) (n := ι) (I₁ := RingHom.id R)
    (I₁' := RingHom.id R)
    (((associated.{u_9, u_10, u_9} (R := R) (M := M) (N := R) : QuadraticMap R M R →ₗ[R] BilinMap R M R) :
        (a : QuadraticMap R M R) → BilinMap R M R)
      Q)
    (⇑v : (a : ι) → M)
w : ι → R
⊢ Eq.{u_9 + 1} (α := R)
    (∑ x : ι,
      (((((associatedHom.{u_9, u_9, u_10, u_9} R (R := R) (M := M) (N := R) : QuadraticMap R M R →ₗ[R] BilinMap R M R) :
                    (a : QuadraticMap R M R) → BilinMap R M R)
                  Q :
                BilinMap R M R) :
              (a : M) → M →ₗ[R] R)
            (∑ i : ι, HSMul.hSMul (β := M) (w i) ((v : (a : ι) → M) i : M)) :
          (a : M) → R)
        (HSMul.hSMul (β := M) (w x) ((v : (a : ι) → M) x : M)))
    (∑ i : ι, HSMul.hSMul (α := R) ((Q : (a : M) → R) ((v : (a : ι) → M) i : M) : R) (w i * w i))

Tactic:
sum_congr rfl fun j hj => ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basic
Goal:
ι : Type u_8
inst : Fintype ι
R : Type u_9
M : Type u_10
inst_1 : CommRing R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : Invertible (α := R) 2
Q : QuadraticForm R M
v : Basis ι R M
hv₂ :
  LinearMap.IsOrthoᵢ.{u_9, u_9, u_9, u_10, u_8} (R := R) (R₁ := R) (M := R) (M₁ := M) (n := ι) (I₁ := RingHom.id R)
    (I₁' := RingHom.id R)
    (((associated.{u_9, u_10, u_9} (R := R) (M := M) (N := R) : QuadraticMap R M R →ₗ[R] BilinMap R M R) :
        (a : QuadraticMap R M R) → BilinMap R M R)
      Q)
    (⇑v : (a : ι) → M)
w : ι → R
H :
  ∀ (j : ι) (hj : Membership.mem (γ := Finset ι) univ j),
    (((((associatedHom.{u_9, u_9, u_10, u_9} R (R := R) (M := M) (N := R) : QuadraticMap R M R →ₗ[R] BilinMap R M R) :
                    (a : QuadraticMap R M R) → BilinMap R M R)
                  Q :
                BilinMap R M R) :
              (a : M) → M →ₗ[R] R)
            (∑ i : ι, HSMul.hSMul (β := M) (w i) ((v : (a : ι) → M) i : M)) :
          (a : M) → R)
        (HSMul.hSMul (β := M) (w j) ((v : (a : ι) → M) j : M)) =
      HSMul.hSMul (α := R) ((Q : (a : M) → R) ((v : (a : ι) → M) j : M) : R) (w j * w j)
⊢ Eq.{u_9 + 1} (α := R)
    (∑ x : ι,
      (((((associatedHom.{u_9, u_9, u_10, u_9} R (R := R) (M := M) (N := R) : QuadraticMap R M R →ₗ[R] BilinMap R M R) :
                    (a : QuadraticMap R M R) → BilinMap R M R)
                  Q :
                BilinMap R M R) :
              (a : M) → M →ₗ[R] R)
            (∑ i : ι, HSMul.hSMul (β := M) (w i) ((v : (a : ι) → M) i : M)) :
          (a : M) → R)
        (HSMul.hSMul (β := M) (w x) ((v : (a : ι) → M) x : M)))
    (∑ i : ι, HSMul.hSMul (α := R) ((Q : (a : M) → R) ((v : (a : ι) → M) i : M) : R) (w i * w i))

Tactic:
refine sum_congr rfl fun j hj => ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basic
Goal:
ι : Type u_8
inst : Fintype ι
R : Type u_9
M : Type u_10
inst_1 : CommRing R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : Invertible (α := R) 2
Q : QuadraticForm R M
v : Basis ι R M
hv₂ :
  LinearMap.IsOrthoᵢ.{u_9, u_9, u_9, u_10, u_8} (R := R) (R₁ := R) (M := R) (M₁ := M) (n := ι) (I₁ := RingHom.id R)
    (I₁' := RingHom.id R)
    (((associated.{u_9, u_10, u_9} (R := R) (M := M) (N := R) : QuadraticMap R M R →ₗ[R] BilinMap R M R) :
        (a : QuadraticMap R M R) → BilinMap R M R)
      Q)
    (⇑v : (a : ι) → M)
w : ι → R
j : ι
hj : Membership.mem (γ := Finset ι) univ j
H :
  ((((((associatedHom.{u_9, u_9, u_10, u_9} R (R := R) (M := M) (N := R) : QuadraticMap R M R →ₗ[R] BilinMap R M R) :
                    (a : QuadraticMap R M R) → BilinMap R M R)
                  Q :
                BilinMap R M R) :
              (a : M) → M →ₗ[R] R)
            (HSMul.hSMul (β := M) (w j) ((v : (a : ι) → M) j : M)) :
          M →ₗ[R] R) :
        (a : M) → R)
      (HSMul.hSMul (β := M) (w j) ((v : (a : ι) → M) j : M)) =
    HSMul.hSMul (α := R)
      (((((((associatedHom.{u_9, u_9, u_10, u_9} R (R := R) (M := M) (N := R) :
                          QuadraticMap R M R →ₗ[R] BilinMap R M R) :
                        (a : QuadraticMap R M R) → BilinMap R M R)
                      Q :
                    BilinMap R M R) :
                  (a : M) → M →ₗ[R] R)
                ((v : (a : ι) → M) j) :
              M →ₗ[R] R) :
            (a : M) → R)
          ((v : (a : ι) → M) j : M) :
        R)
      (w j * w j)
H₁ :
  ∀ (b : ι),
    Membership.mem (γ := Finset ι) univ b →
      b ≠ j →
        Eq.{u_9 + 1} (α := R)
          (((((((associatedHom.{u_9, u_9, u_10, u_9} R (R := R) (M := M) (N := R) :
                              QuadraticMap R M R →ₗ[R] BilinMap R M R) :
                            (a : QuadraticMap R M R) → BilinMap R M R)
                          Q :
                        BilinMap R M R) :
                      (a : M) → M →ₗ[R] R)
                    (HSMul.hSMul (β := M) (w b) ((v : (a : ι) → M) b : M)) :
                  M →ₗ[R] R) :
                (a : M) → R)
              (HSMul.hSMul (β := M) (w j) ((v : (a : ι) → M) j : M)) :
            R)
          (0 : R)
⊢ (((((associatedHom.{u_9, u_9, u_10, u_9} R (R := R) (M := M) (N := R) : QuadraticMap R M R →ₗ[R] BilinMap R M R) :
                  (a : QuadraticMap R M R) → BilinMap R M R)
                Q :
              BilinMap R M R) :
            (a : M) → M →ₗ[R] R)
          (∑ i : ι, HSMul.hSMul (β := M) (w i) ((v : (a : ι) → M) i : M)) :
        (a : M) → R)
      (HSMul.hSMul (β := M) (w j) ((v : (a : ι) → M) j : M)) =
    HSMul.hSMul (α := R) ((Q : (a : M) → R) ((v : (a : ι) → M) j : M) : R) (w j * w j)

Tactic:
rw [← @associated_eq_self_apply R, LinearMap.map_sum₂, sum_eq_single_of_mem j hj]

Premises used: Finset.sum_eq_single_of_mem, QuadraticMap.associated_eq_self_apply, LinearMap.map_sum₂
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basic
Goal:
ι : Type u_8
inst : Fintype ι
R : Type u_9
M : Type u_10
inst_1 : CommRing R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : Invertible (α := R) 2
Q : QuadraticForm R M
v : Basis ι R M
hv₂ :
  LinearMap.IsOrthoᵢ.{u_9, u_9, u_9, u_10, u_8} (R := R) (R₁ := R) (M := R) (M₁ := M) (n := ι) (I₁ := RingHom.id R)
    (I₁' := RingHom.id R)
    (((associated.{u_9, u_10, u_9} (R := R) (M := M) (N := R) : QuadraticMap R M R →ₗ[R] BilinMap R M R) :
        (a : QuadraticMap R M R) → BilinMap R M R)
      Q)
    (⇑v : (a : ι) → M)
w : ι → R
j : ι
hj : Membership.mem (γ := Finset ι) univ j
H :
  w j *
      (w j *
        HSMul.hSMul (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
          (HSub.hSub (β := R)
            (HSub.hSub (α := R) (β := R)
              ((Q : (a : M) → R) (HAdd.hAdd (α := M) (β := M) ((v : (a : ι) → M) j : M) ((v : (a : ι) → M) j : M)) : R)
              ((Q : (a : M) → R) ((v : (a : ι) → M) j : M) : R))
            ((Q : (a : M) → R) ((v : (a : ι) → M) j : M) : R))) =
    HSMul.hSMul (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
        (HSub.hSub (β := R)
          (HSub.hSub (α := R) (β := R)
            ((Q : (a : M) → R) (HAdd.hAdd (α := M) (β := M) ((v : (a : ι) → M) j : M) ((v : (a : ι) → M) j : M)) : R)
            ((Q : (a : M) → R) ((v : (a : ι) → M) j : M) : R))
          ((Q : (a : M) → R) ((v : (a : ι) → M) j : M) : R)) *
      (w j * w j)
⊢ ((((((associatedHom.{u_9, u_9, u_10, u_9} R (R := R) (M := M) (N := R) : QuadraticMap R M R →ₗ[R] BilinMap R M R) :
                    (a : QuadraticMap R M R) → BilinMap R M R)
                  Q :
                BilinMap R M R) :
              (a : M) → M →ₗ[R] R)
            (HSMul.hSMul (β := M) (w j) ((v : (a : ι) → M) j : M)) :
          M →ₗ[R] R) :
        (a : M) → R)
      (HSMul.hSMul (β := M) (w j) ((v : (a : ι) → M) j : M)) =
    HSMul.hSMul (α := R)
      (((((((associatedHom.{u_9, u_9, u_10, u_9} R (R := R) (M := M) (N := R) :
                          QuadraticMap R M R →ₗ[R] BilinMap R M R) :
                        (a : QuadraticMap R M R) → BilinMap R M R)
                      Q :
                    BilinMap R M R) :
                  (a : M) → M →ₗ[R] R)
                ((v : (a : ι) → M) j) :
              M →ₗ[R] R) :
            (a : M) → R)
          ((v : (a : ι) → M) j : M) :
        R)
      (w j * w j)

Tactic:
rw [map_smul, LinearMap.map_smul₂, smul_eq_mul, associated_apply, smul_eq_mul,
      smul_eq_mul, Module.End.smul_def, half_moduleEnd_apply_eq_half_smul]

Premises used: Module.End.smul_def, QuadraticMap.associated_apply, QuadraticMap.half_moduleEnd_apply_eq_half_smul, LinearMap.map_smul₂, smul_eq_mul, map_smul
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basic
Goal:
ι : Type u_8
inst : Fintype ι
R : Type u_9
M : Type u_10
inst_1 : CommRing R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : Invertible (α := R) 2
Q : QuadraticForm R M
v : Basis ι R M
hv₂ :
  LinearMap.IsOrthoᵢ.{u_9, u_9, u_9, u_10, u_8} (R := R) (R₁ := R) (M := R) (M₁ := M) (n := ι) (I₁ := RingHom.id R)
    (I₁' := RingHom.id R)
    (((associated.{u_9, u_10, u_9} (R := R) (M := M) (N := R) : QuadraticMap R M R →ₗ[R] BilinMap R M R) :
        (a : QuadraticMap R M R) → BilinMap R M R)
      Q)
    (⇑v : (a : ι) → M)
w : ι → R
j : ι
hj : Membership.mem (γ := Finset ι) univ j
⊢ w j *
      (w j *
        HSMul.hSMul (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
          (HSub.hSub (β := R)
            (HSub.hSub (α := R) (β := R)
              ((Q : (a : M) → R) (HAdd.hAdd (α := M) (β := M) ((v : (a : ι) → M) j : M) ((v : (a : ι) → M) j : M)) : R)
              ((Q : (a : M) → R) ((v : (a : ι) → M) j : M) : R))
            ((Q : (a : M) → R) ((v : (a : ι) → M) j : M) : R))) =
    HSMul.hSMul (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
        (HSub.hSub (β := R)
          (HSub.hSub (α := R) (β := R)
            ((Q : (a : M) → R) (HAdd.hAdd (α := M) (β := M) ((v : (a : ι) → M) j : M) ((v : (a : ι) → M) j : M)) : R)
            ((Q : (a : M) → R) ((v : (a : ι) → M) j : M) : R))
          ((Q : (a : M) → R) ((v : (a : ι) → M) j : M) : R)) *
      (w j * w j)

Tactic:
ring_nf
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basic
Goal:
ι : Type u_8
inst : Fintype ι
R : Type u_9
M : Type u_10
inst_1 : CommRing R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : Invertible (α := R) 2
Q : QuadraticForm R M
v : Basis ι R M
hv₂ :
  LinearMap.IsOrthoᵢ.{u_9, u_9, u_9, u_10, u_8} (R := R) (R₁ := R) (M := R) (M₁ := M) (n := ι) (I₁ := RingHom.id R)
    (I₁' := RingHom.id R)
    (((associated.{u_9, u_10, u_9} (R := R) (M := M) (N := R) : QuadraticMap R M R →ₗ[R] BilinMap R M R) :
        (a : QuadraticMap R M R) → BilinMap R M R)
      Q)
    (⇑v : (a : ι) → M)
w : ι → R
j : ι
hj : Membership.mem (γ := Finset ι) univ j
i : ι
H :
  Membership.mem (γ := Finset ι) univ i →
    i ≠ j →
      Eq.{u_9 + 1} (α := R)
        (((((((associatedHom.{u_9, u_9, u_10, u_9} R (R := R) (M := M) (N := R) :
                            QuadraticMap R M R →ₗ[R] BilinMap R M R) :
                          (a : QuadraticMap R M R) → BilinMap R M R)
                        Q :
                      BilinMap R M R) :
                    (a : M) → M →ₗ[R] R)
                  (HSMul.hSMul (β := M) (w i) ((v : (a : ι) → M) i : M)) :
                M →ₗ[R] R) :
              (a : M) → R)
            (HSMul.hSMul (β := M) (w j) ((v : (a : ι) → M) j : M)) :
          R)
        (0 : R)
⊢ Membership.mem (γ := Finset ι) univ i →
    i ≠ j →
      Eq.{u_9 + 1} (α := R)
        (((((((associatedHom.{u_9, u_9, u_10, u_9} R (R := R) (M := M) (N := R) :
                            QuadraticMap R M R →ₗ[R] BilinMap R M R) :
                          (a : QuadraticMap R M R) → BilinMap R M R)
                        Q :
                      BilinMap R M R) :
                    (a : M) → M →ₗ[R] R)
                  (HSMul.hSMul (β := M) (w i) ((v : (a : ι) → M) i : M)) :
                M →ₗ[R] R) :
              (a : M) → R)
            (HSMul.hSMul (β := M) (w j) ((v : (a : ι) → M) j : M)) :
          R)
        (0 : R)

Tactic:
_
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basic
Goal:
ι : Type u_8
inst : Fintype ι
R : Type u_9
M : Type u_10
inst_1 : CommRing R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : Invertible (α := R) 2
Q : QuadraticForm R M
v : Basis ι R M
hv₂ :
  LinearMap.IsOrthoᵢ.{u_9, u_9, u_9, u_10, u_8} (R := R) (R₁ := R) (M := R) (M₁ := M) (n := ι) (I₁ := RingHom.id R)
    (I₁' := RingHom.id R)
    (((associated.{u_9, u_10, u_9} (R := R) (M := M) (N := R) : QuadraticMap R M R →ₗ[R] BilinMap R M R) :
        (a : QuadraticMap R M R) → BilinMap R M R)
      Q)
    (⇑v : (a : ι) → M)
w : ι → R
j : ι
hj : Membership.mem (γ := Finset ι) univ j
i : ι
h : Membership.mem (γ := Finset ι) univ i
hij : i ≠ j
H : w j • HSMul.hSMul (β := R) (w i) 0 = 0
⊢ Eq.{u_9 + 1} (α := R)
    (((((((associatedHom.{u_9, u_9, u_10, u_9} R (R := R) (M := M) (N := R) : QuadraticMap R M R →ₗ[R] BilinMap R M R) :
                      (a : QuadraticMap R M R) → BilinMap R M R)
                    Q :
                  BilinMap R M R) :
                (a : M) → M →ₗ[R] R)
              (HSMul.hSMul (β := M) (w i) ((v : (a : ι) → M) i : M)) :
            M →ₗ[R] R) :
          (a : M) → R)
        (HSMul.hSMul (β := M) (w j) ((v : (a : ι) → M) j : M)) :
      R)
    (0 : R)

Tactic:
rw [map_smul, LinearMap.map_smul₂, hv₂ hij]

Premises used: LinearMap.map_smul₂, map_smul
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basic
Goal:
ι : Type u_8
inst : Fintype ι
R : Type u_9
M : Type u_10
inst_1 : CommRing R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : Invertible (α := R) 2
Q : QuadraticForm R M
v : Basis ι R M
hv₂ :
  LinearMap.IsOrthoᵢ.{u_9, u_9, u_9, u_10, u_8} (R := R) (R₁ := R) (M := R) (M₁ := M) (n := ι) (I₁ := RingHom.id R)
    (I₁' := RingHom.id R)
    (((associated.{u_9, u_10, u_9} (R := R) (M := M) (N := R) : QuadraticMap R M R →ₗ[R] BilinMap R M R) :
        (a : QuadraticMap R M R) → BilinMap R M R)
      Q)
    (⇑v : (a : ι) → M)
w : ι → R
j : ι
hj : Membership.mem (γ := Finset ι) univ j
i : ι
h : Membership.mem (γ := Finset ι) univ i
hij : i ≠ j
⊢ w j • HSMul.hSMul (β := R) (w i) 0 = 0

Tactic:
module
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basis
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
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
f : ι →₀ R
g : ι → R → M
⊢ (Q : (a : M) → N) (f.sum g) =
    HSub.hSub (α := N)
      (∑ p ∈ f.support.sym2,
        polarSym2.{u_3, u_4} (M := M) (⇑Q : (a : M) → N) (Sym2.map (fun (i : ι) ↦ g i ((f : (a : ι) → R) i)) p))
      (f.sum fun (i : ι) (a : R) ↦ (Q : (a : M) → N) (g i a))

Tactic:
Q.map_sum' ..

Premises used: Finsupp.sum, QuadraticMap.map_sum'
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basis
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
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
g : ι → M
l : ι →₀ R
simp_rw :
  HSub.hSub (α := N)
      (∑ p ∈ l.support.sym2,
        polarSym2.{u_3, u_4} (M := M) (⇑Q : (a : M) → N)
          (Sym2.map (fun (i : ι) ↦ HSMul.hSMul.{u_2, u_3, u_3} (α := R) ((l : (a : ι) → R) i : R) (g i)) p))
      (l.sum fun (i : ι) (a : R) ↦ a • HSMul.hSMul (β := N) a ((Q : (a : M) → N) (g i) : N)) =
    HSub.hSub (α := N)
      (sum (l.sym2Mul : Finsupp.{u_1, u_2} (Sym2 ι) R) fun (i : Sym2 ι) (a : R) ↦
        HSMul.hSMul (β := N) a ((polarSym2 (⇑Q : (a : M) → N) ∘ Sym2.map g) i))
      ((l * l).sum fun (i : ι) (a : R) ↦ HSMul.hSMul (β := N) a (((⇑Q : (a : M) → N) ∘ g) i))
⊢ (Q : (a : M) → N) ((linearCombination R g : (a : ι →₀ R) → M) l : M) =
    HSub.hSub (α := N) (β := N)
      ((linearCombination R (polarSym2 (⇑Q : (a : M) → N) ∘ Sym2.map g) : (a : Sym2 ι →₀ R) → N)
          (l.sym2Mul : Finsupp.{u_1, u_2} (Sym2 ι) R) :
        N)
      ((linearCombination R ((⇑Q : (a : M) → N) ∘ g) : (a : ι →₀ R) → N) (l * l) : N)

Tactic:
simp_rw [linearCombination_apply, map_finsuppSum', Q.map_smul, mul_smul]

Premises used: QuadraticMap.map_smul, Finsupp.linearCombination_apply, QuadraticMap.map_finsuppSum', SemigroupAction.mul_smul
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basis
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
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
g : ι → M
l : ι →₀ R
⊢ ∀ i ∈ l.support, HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := N) 0 (((⇑Q : (a : M) → N) ∘ g) i) = 0

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basis
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
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
g : ι → M
l : ι →₀ R
⊢ ∀ i ∈ l.support.sym2,
    HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := N) 0 ((polarSym2 (⇑Q : (a : M) → N) ∘ Sym2.map g) i) = 0

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basis
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
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
g : ι → M
l : ι →₀ R
rw :
  HSub.hSub (α := N)
      (∑ p ∈ l.support.sym2,
        polarSym2.{u_3, u_4} (M := M) (⇑Q : (a : M) → N)
          (Sym2.map (fun (i : ι) ↦ HSMul.hSMul.{u_2, u_3, u_3} (α := R) ((l : (a : ι) → R) i : R) (g i)) p))
      (l.sum fun (i : ι) (a : R) ↦ a • HSMul.hSMul (β := N) a ((Q : (a : M) → N) (g i) : N)) =
    HSub.hSub (α := N)
      (∑ x ∈ l.support.sym2,
        HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := N) ((l.sym2Mul : (a : Sym2 ι) → R) x : R)
          ((polarSym2 (⇑Q : (a : M) → N) ∘ Sym2.map g) x))
      (∑ x ∈ l.support,
        HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := N) ((l * l : (a : ι) → R) x : R) (((⇑Q : (a : M) → N) ∘ g) x))
⊢ HSub.hSub (α := N)
      (∑ p ∈ l.support.sym2,
        polarSym2.{u_3, u_4} (M := M) (⇑Q : (a : M) → N)
          (Sym2.map (fun (i : ι) ↦ HSMul.hSMul.{u_2, u_3, u_3} (α := R) ((l : (a : ι) → R) i : R) (g i)) p))
      (l.sum fun (i : ι) (a : R) ↦ a • HSMul.hSMul (β := N) a ((Q : (a : M) → N) (g i) : N)) =
    HSub.hSub (α := N)
      (sum (l.sym2Mul : Finsupp.{u_1, u_2} (Sym2 ι) R) fun (i : Sym2 ι) (a : R) ↦
        HSMul.hSMul (β := N) a ((polarSym2 (⇑Q : (a : M) → N) ∘ Sym2.map g) i))
      ((l * l).sum fun (i : ι) (a : R) ↦ HSMul.hSMul (β := N) a (((⇑Q : (a : M) → N) ∘ g) i))

Tactic:
rw [(l * l).sum_of_support_subset support_mul_subset_left _ <| by simp,
    l.sym2Mul.sum_of_support_subset support_sym2Mul_subset _ <| by simp]

Premises used: HMul.hMul, Finsupp.support_sym2Mul_subset, Finsupp.sym2Mul, Finsupp.support_mul_subset_left, Finsupp.sum_of_support_subset
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basis
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
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
g : ι → M
l : ι →₀ R
⊢ HSub.hSub (α := N)
      (∑ p ∈ l.support.sym2,
        polarSym2.{u_3, u_4} (M := M) (⇑Q : (a : M) → N)
          (Sym2.map (fun (i : ι) ↦ HSMul.hSMul.{u_2, u_3, u_3} (α := R) ((l : (a : ι) → R) i : R) (g i)) p))
      (l.sum fun (i : ι) (a : R) ↦ a • HSMul.hSMul (β := N) a ((Q : (a : M) → N) (g i) : N)) =
    HSub.hSub (α := N)
      (∑ x ∈ l.support.sym2,
        HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := N) ((l.sym2Mul : (a : Sym2 ι) → R) x : R)
          ((polarSym2 (⇑Q : (a : M) → N) ∘ Sym2.map g) x))
      (∑ x ∈ l.support,
        HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := N) ((l * l : (a : ι) → R) x : R) (((⇑Q : (a : M) → N) ∘ g) x))

Tactic:
simp [Finsupp.sum, ← polarSym2_map_smul, mul_smul]

Premises used: Finsupp.sum, QuadraticMap.polarSym2_map_smul, SemigroupAction.mul_smul
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basis
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
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
bm : Basis ι R M
x : M
rw :
  Eq.{u_4 + 1} (α := N)
    ((Q : (a : M) → N)
        ((linearCombination R (⇑bm : (a : ι) → M) : (a : ι →₀ R) → M) ((bm.repr : (a : M) → ι →₀ R) x : ι →₀ R) : M) :
      N)
    ((Q : (a : M) → N) x : N)
rw₁ rw₂ : Eq.{u_4 + 1} (α := N) ((Q : (a : M) → N) x : N) ((Q : (a : M) → N) x : N)
⊢ HSub.hSub (α := N) (β := N)
      ((linearCombination R
              (Function.comp.{u_1 + 1, u_3 + 1, u_4 + 1} (β := Sym2 M) (polarSym2 (⇑Q : (a : M) → N))
                (Sym2.map (⇑bm : (a : ι) → M))) :
            (a : Sym2 ι →₀ R) → N)
          (sym2Mul ((bm.repr : (a : M) → ι →₀ R) x) : Finsupp.{u_1, u_2} (Sym2 ι) R) :
        N)
      ((linearCombination R
              (Function.comp.{u_1 + 1, u_3 + 1, u_4 + 1} (β := M) (⇑Q : (a : M) → N) (⇑bm : (a : ι) → M)) :
            (a : ι →₀ R) → N)
          (HMul.hMul (α := ι →₀ R) (β := ι →₀ R) ((bm.repr : (a : M) → ι →₀ R) x : ι →₀ R)
            ((bm.repr : (a : M) → ι →₀ R) x : ι →₀ R)) :
        N) =
    (Q : (a : M) → N) x

Tactic:
rw [← apply_linearCombination', Basis.linearCombination_repr]

Premises used: Module.Basis.linearCombination_repr, QuadraticMap.apply_linearCombination'