awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
ι : Type u_8
Q : QuadraticMap R M N
g : ι → M
l : ι → R
p : Sym2 ι
mk :
  ∀ (fst snd : ι),
    polarSym2 (⇑Q : (a : M) → N) (Sym2.map (l • g) (Quot.mk (Sym2.Rel ι) (fst, snd))) =
      HSMul.hSMul (β := N) (Sym2.map l (Quot.mk (Sym2.Rel ι) (fst, snd))).mul
        (polarSym2 (⇑Q : (a : M) → N) (Sym2.map g (Quot.mk (Sym2.Rel ι) (fst, snd))))
⊢ polarSym2 (⇑Q : (a : M) → N) (Sym2.map (l • g) p) =
    HSMul.hSMul (β := N) (Sym2.map l p).mul (polarSym2 (⇑Q : (a : M) → N) (Sym2.map g p))

Tactic:
obtain ⟨_, _⟩ := p
-- 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
ι : Type u_8
Q : QuadraticMap R M N
g : ι → M
l : ι → R
p : Sym2 ι
fst snd : ι
⊢ polarSym2 (⇑Q : (a : M) → N) (Sym2.map (l • g) (Quot.mk (Sym2.Rel ι) (fst, snd))) =
    HSMul.hSMul (β := N) (Sym2.map l (Quot.mk (Sym2.Rel ι) (fst, snd))).mul
      (polarSym2 (⇑Q : (a : M) → N) (Sym2.map g (Quot.mk (Sym2.Rel ι) (fst, snd))))

Tactic:
simp [← smul_assoc, mul_comm]

Premises used: smul_assoc, mul_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 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
Q : QuadraticMap R M N
inst_5 : CommSemiring S
inst_6 : Algebra S R
inst_7 : Module S M
inst_8 : IsScalarTower S R M
inst_9 : Module S N
inst_10 : IsScalarTower S R N
a : S
x y : M
rw :
  polar (⇑Q : (a : M) → N) (HSMul.hSMul.{u_3, u_4, u_4} (α := R) ((algebraMap S R : (a : S) → R) a : R) x) y =
    HSMul.hSMul (β := N) a (polar (⇑Q : (a : M) → N) x y)
rw₁ :
  HSMul.hSMul.{u_3, u_5, u_5} (α := R) (β := N) ((algebraMap S R : (a : S) → R) a : R) (polar (⇑Q : (a : M) → N) x y) =
    HSMul.hSMul (β := N) a (polar (⇑Q : (a : M) → N) x y)
rw₂ rw₃ : HSMul.hSMul (β := N) a (polar (⇑Q : (a : M) → N) x y) = HSMul.hSMul (β := N) a (polar (⇑Q : (a : M) → N) x y)
⊢ polar (⇑Q : (a : M) → N) (a • x) y = HSMul.hSMul (β := N) a (polar (⇑Q : (a : M) → N) x y)

Tactic:
rw [← IsScalarTower.algebraMap_smul R a x, polar_smul_left, algebraMap_smul]

Premises used: algebraMap_smul, QuadraticMap.polar_smul_left, IsScalarTower.algebraMap_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 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
Q : QuadraticMap R M N
inst_5 : CommSemiring S
inst_6 : Algebra S R
inst_7 : Module S M
inst_8 : IsScalarTower S R M
inst_9 : Module S N
inst_10 : IsScalarTower S R N
a : S
x y : M
rw :
  polar (⇑Q : (a : M) → N) x (HSMul.hSMul.{u_3, u_4, u_4} (α := R) ((algebraMap S R : (a : S) → R) a : R) y) =
    HSMul.hSMul (β := N) a (polar (⇑Q : (a : M) → N) x y)
rw₁ :
  HSMul.hSMul.{u_3, u_5, u_5} (α := R) (β := N) ((algebraMap S R : (a : S) → R) a : R) (polar (⇑Q : (a : M) → N) x y) =
    HSMul.hSMul (β := N) a (polar (⇑Q : (a : M) → N) x y)
rw₂ rw₃ : HSMul.hSMul (β := N) a (polar (⇑Q : (a : M) → N) x y) = HSMul.hSMul (β := N) a (polar (⇑Q : (a : M) → N) x y)
⊢ polar (⇑Q : (a : M) → N) x (a • y) = HSMul.hSMul (β := N) a (polar (⇑Q : (a : M) → N) x y)

Tactic:
rw [← IsScalarTower.algebraMap_smul R a y, polar_smul_right, algebraMap_smul]

Premises used: algebraMap_smul, IsScalarTower.algebraMap_smul, QuadraticMap.polar_smul_right
-- 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 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
Q : QuadraticMap R M N
inst_5 : CommSemiring S
inst_6 : Algebra S R
inst_7 : Module S M
inst_8 : IsScalarTower S R M
inst_9 : Module S N
inst_10 : IsScalarTower S R N
toFun : M → N
toFun_smul : ∀ (a : R) (x : M), toFun (a • x) = (a * a) • toFun x
polar_add_left : ∀ (x x' y : M), polar toFun (x + x') y = polar toFun x y + polar toFun x' y
polar_smul_left : ∀ (a : R) (x y : M), polar toFun (a • x) y = a • polar toFun x y
x x_1 x_2 : M
simp_rw : polar toFun (x_1 + x_2) x = polar toFun x_1 x + polar toFun x_2 x
⊢ polar toFun x (x_1 + x_2) = polar toFun x x_1 + polar toFun x x_2

Tactic:
simp_rw [polar_comm _ x, polar_add_left]

Premises used: QuadraticMap.polar_comm
-- 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 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
Q : QuadraticMap R M N
inst_5 : CommSemiring S
inst_6 : Algebra S R
inst_7 : Module S M
inst_8 : IsScalarTower S R M
inst_9 : Module S N
inst_10 : IsScalarTower S R N
toFun : M → N
toFun_smul : ∀ (a : R) (x : M), toFun (a • x) = (a * a) • toFun x
polar_add_left : ∀ (x x' y : M), polar toFun (x + x') y = polar toFun x y + polar toFun x' y
polar_smul_left : ∀ (a : R) (x y : M), polar toFun (a • x) y = a • polar toFun x y
x : R
x_1 x_2 : M
rw : polar toFun (x • x_2) x_1 = x • polar toFun x_1 x_2
rw₁ : x • polar toFun x_2 x_1 = x • polar toFun x_1 x_2
rw₂ rw₃ : x • polar toFun x_1 x_2 = x • polar toFun x_1 x_2
⊢ polar toFun x_1 (x • x_2) = x • polar toFun x_1 x_2

Tactic:
rw [polar_comm, polar_smul_left, polar_comm]

Premises used: QuadraticMap.polar_comm
-- 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 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
Q : QuadraticMap R M N
inst_5 : CommSemiring S
inst_6 : Algebra S R
inst_7 : Module S M
inst_8 : IsScalarTower S R M
inst_9 : Module S N
inst_10 : IsScalarTower S R N
toFun : M → N
toFun_smul : ∀ (a : R) (x : M), toFun (a • x) = (a * a) • toFun x
polar_add_left : ∀ (x x' y : M), polar toFun (x + x') y = polar toFun x y + polar toFun x' y
polar_smul_left : ∀ (a : R) (x y : M), polar toFun (a • x) y = a • polar toFun x y
x x_1 : M
simp : toFun (x + x_1) = toFun x + toFun x_1 + polar toFun x x_1
⊢ toFun (x + x_1) =
    HAdd.hAdd (β := N) (toFun x + toFun x_1)
      ((((LinearMap.mk₂ R (polar toFun) polar_add_left polar_smul_left ⋯ ⋯ : (a : M) → M →ₗ[R] N) x : M →ₗ[R] N) :
            (a : M) → N)
          x_1 :
        N)

Tactic:
simp only [LinearMap.mk₂_apply]

Premises used: LinearMap.mk₂_apply
-- 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 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
Q : QuadraticMap R M N
inst_5 : CommSemiring S
inst_6 : Algebra S R
inst_7 : Module S M
inst_8 : IsScalarTower S R M
inst_9 : Module S N
inst_10 : IsScalarTower S R N
toFun : M → N
toFun_smul : ∀ (a : R) (x : M), toFun (a • x) = (a * a) • toFun x
polar_add_left : ∀ (x x' y : M), polar toFun (x + x') y = polar toFun x y + polar toFun x' y
polar_smul_left : ∀ (a : R) (x y : M), polar toFun (a • x) y = a • polar toFun x y
x x_1 : M
rw : toFun (x + x_1) = toFun x + toFun x_1 + (toFun (x + x_1) - toFun x - toFun x_1)
rw₁ : toFun (x + x_1) = toFun x + toFun x_1 + (toFun (x + x_1) - (toFun x + toFun x_1))
rw₂ rw₃ : toFun (x + x_1) = toFun (x + x_1)
⊢ toFun (x + x_1) = toFun x + toFun x_1 + polar toFun x x_1

Tactic:
rw [polar, sub_sub, add_sub_cancel]

Premises used: QuadraticMap.polar, sub_sub, add_sub_cancel
-- 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
ι : Type u_8
inst_5 : DecidableEq ι
Q : QuadraticMap R M N
f : ι → M
⊢ (Q : (a : M) → N) (∑ i ∈ ∅, f i) =
    HAdd.hAdd (α := N) (∑ i ∈ ∅, (Q : (a : M) → N) (f i))
      (∑ ij ∈ Finset.sym2 ∅ with ¬ij.IsDiag, polarSym2 (⇑Q : (a : M) → N) (Sym2.map f ij))

Tactic:
simp
-- 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
ι : Type u_8
inst_5 : DecidableEq ι
Q : QuadraticMap R M N
f : ι → M
a : ι
s : Finset ι
ha : a ∉ s
ih :
  (Q : (a : M) → N) (∑ i ∈ s, f i) =
    HAdd.hAdd (α := N) (∑ i ∈ s, (Q : (a : M) → N) (f i))
      (∑ ij ∈ s.sym2 with ¬ij.IsDiag, polarSym2 (⇑Q : (a : M) → N) (Sym2.map f ij))
cons :
  HAdd.hAdd (α := N) ((Q : (a : M) → N) (f a) : N)
      (∑ i ∈ s, (Q : (a : M) → N) (f i) +
        HAdd.hAdd (α := N) (∑ a ∈ s.sym2, if ¬a.IsDiag then polarSym2 (⇑Q : (a : M) → N) (Sym2.map f a) else 0)
          (∑ x ∈ s, polar (⇑Q : (a : M) → N) (f a) (f x))) =
    HAdd.hAdd (α := N) ((Q : (a : M) → N) (f a) : N)
      (∑ i ∈ s, (Q : (a : M) → N) (f i) +
        HAdd.hAdd (α := N) (∑ x ∈ s, if ¬a = x then polar (⇑Q : (a : M) → N) (f a) (f x) else 0)
          (∑ a ∈ s.sym2, if ¬a.IsDiag then polarSym2 (⇑Q : (a : M) → N) (Sym2.map f a) else 0))
⊢ (Q : (a : M) → N) (∑ i ∈ Finset.cons a s ha, f i) =
    HAdd.hAdd (α := N) (∑ i ∈ Finset.cons a s ha, (Q : (a : M) → N) (f i))
      (∑ ij ∈ (Finset.cons a s ha).sym2 with ¬ij.IsDiag, polarSym2 (⇑Q : (a : M) → N) (Sym2.map f ij))

Tactic:
simp_rw [Finset.sum_cons, QuadraticMap.map_add, ih, add_assoc, Finset.sym2_cons,
      Finset.sum_filter, Finset.sum_disjUnion, Finset.sum_map, Finset.sum_cons,
      Sym2.mkEmbedding_apply, Sym2.mk_isDiag_iff, not_true, if_false, zero_add,
      Sym2.map_mk, polarSym2_sym2Mk, ← polarBilin_apply_apply, _root_.map_sum,
      polarBilin_apply_apply]

Premises used: Finset.sum_cons, add_assoc, Finset.sum_map, if_false, Sym2.mkEmbedding_apply, Finset.sum_disjUnion, QuadraticMap.map_add, map_sum, zero_add, Finset.sym2_cons, Sym2.map_mk, QuadraticMap.polarSym2_sym2Mk, Sym2.mk_isDiag_iff, not_true, Finset.sum_filter, 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 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
ι : Type u_8
inst_5 : DecidableEq ι
Q : QuadraticMap R M N
f : ι → M
a : ι
s : Finset ι
ha : a ∉ s
ih :
  (Q : (a : M) → N) (∑ i ∈ s, f i) =
    HAdd.hAdd (α := N) (∑ i ∈ s, (Q : (a : M) → N) (f i))
      (∑ ij ∈ s.sym2 with ¬ij.IsDiag, polarSym2 (⇑Q : (a : M) → N) (Sym2.map f ij))
cons :
  HAdd.hAdd (α := N) (∑ a ∈ s.sym2, if ¬a.IsDiag then polarSym2 (⇑Q : (a : M) → N) (Sym2.map f a) else 0)
      (∑ x ∈ s, polar (⇑Q : (a : M) → N) (f a) (f x)) =
    HAdd.hAdd (α := N) (∑ x ∈ s, if ¬a = x then polar (⇑Q : (a : M) → N) (f a) (f x) else 0)
      (∑ a ∈ s.sym2, if ¬a.IsDiag then polarSym2 (⇑Q : (a : M) → N) (Sym2.map f a) else 0)
⊢ HAdd.hAdd (α := N) ((Q : (a : M) → N) (f a) : N)
      (∑ i ∈ s, (Q : (a : M) → N) (f i) +
        HAdd.hAdd (α := N) (∑ a ∈ s.sym2, if ¬a.IsDiag then polarSym2 (⇑Q : (a : M) → N) (Sym2.map f a) else 0)
          (∑ x ∈ s, polar (⇑Q : (a : M) → N) (f a) (f x))) =
    HAdd.hAdd (α := N) ((Q : (a : M) → N) (f a) : N)
      (∑ i ∈ s, (Q : (a : M) → N) (f i) +
        HAdd.hAdd (α := N) (∑ x ∈ s, if ¬a = x then polar (⇑Q : (a : M) → N) (f a) (f x) else 0)
          (∑ a ∈ s.sym2, if ¬a.IsDiag then polarSym2 (⇑Q : (a : M) → N) (Sym2.map f a) else 0))

Tactic:
congr 2
-- 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
ι : Type u_8
inst_5 : DecidableEq ι
Q : QuadraticMap R M N
f : ι → M
a : ι
s : Finset ι
ha : a ∉ s
ih :
  (Q : (a : M) → N) (∑ i ∈ s, f i) =
    HAdd.hAdd (α := N) (∑ i ∈ s, (Q : (a : M) → N) (f i))
      (∑ ij ∈ s.sym2 with ¬ij.IsDiag, polarSym2 (⇑Q : (a : M) → N) (Sym2.map f ij))
cons :
  HAdd.hAdd (α := N) (∑ x ∈ s, polar (⇑Q : (a : M) → N) (f a) (f x))
      (∑ a ∈ s.sym2, if ¬a.IsDiag then polarSym2 (⇑Q : (a : M) → N) (Sym2.map f a) else 0) =
    HAdd.hAdd (α := N) (∑ x ∈ s, if ¬a = x then polar (⇑Q : (a : M) → N) (f a) (f x) else 0)
      (∑ a ∈ s.sym2, if ¬a.IsDiag then polarSym2 (⇑Q : (a : M) → N) (Sym2.map f a) else 0)
⊢ HAdd.hAdd (α := N) (∑ a ∈ s.sym2, if ¬a.IsDiag then polarSym2 (⇑Q : (a : M) → N) (Sym2.map f a) else 0)
      (∑ x ∈ s, polar (⇑Q : (a : M) → N) (f a) (f x)) =
    HAdd.hAdd (α := N) (∑ x ∈ s, if ¬a = x then polar (⇑Q : (a : M) → N) (f a) (f x) else 0)
      (∑ a ∈ s.sym2, if ¬a.IsDiag then polarSym2 (⇑Q : (a : M) → N) (Sym2.map f a) else 0)

Tactic:
rw [add_comm]

Premises used: add_comm
-- 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
ι : Type u_8
inst_5 : DecidableEq ι
Q : QuadraticMap R M N
f : ι → M
a : ι
s : Finset ι
ha : a ∉ s
ih :
  (Q : (a : M) → N) (∑ i ∈ s, f i) =
    HAdd.hAdd (α := N) (∑ i ∈ s, (Q : (a : M) → N) (f i))
      (∑ ij ∈ s.sym2 with ¬ij.IsDiag, polarSym2 (⇑Q : (a : M) → N) (Sym2.map f ij))
cons :
  ∀ (i : ι) (hi : i ∈ s),
    Eq.{u_5 + 1} (α := N) (polar (⇑Q : (a : M) → N) (f a) (f i))
      (if ¬a = i then polar (⇑Q : (a : M) → N) (f a) (f i) else 0)
⊢ HAdd.hAdd (α := N) (∑ x ∈ s, polar (⇑Q : (a : M) → N) (f a) (f x))
      (∑ a ∈ s.sym2, if ¬a.IsDiag then polarSym2 (⇑Q : (a : M) → N) (Sym2.map f a) else 0) =
    HAdd.hAdd (α := N) (∑ x ∈ s, if ¬a = x then polar (⇑Q : (a : M) → N) (f a) (f x) else 0)
      (∑ a ∈ s.sym2, if ¬a.IsDiag then polarSym2 (⇑Q : (a : M) → N) (Sym2.map f a) else 0)

Tactic:
congr! with i hi
-- 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
ι : Type u_8
inst_5 : DecidableEq ι
Q : QuadraticMap R M N
f : ι → M
a : ι
s : Finset ι
ha : a ∉ s
ih :
  (Q : (a : M) → N) (∑ i ∈ s, f i) =
    HAdd.hAdd (α := N) (∑ i ∈ s, (Q : (a : M) → N) (f i))
      (∑ ij ∈ s.sym2 with ¬ij.IsDiag, polarSym2 (⇑Q : (a : M) → N) (Sym2.map f ij))
i : ι
hi : i ∈ s
cons cons₁ : Eq.{u_5 + 1} (α := N) (polar (⇑Q : (a : M) → N) (f a) (f i)) (polar (⇑Q : (a : M) → N) (f a) (f i))
⊢ Eq.{u_5 + 1} (α := N) (polar (⇑Q : (a : M) → N) (f a) (f i))
    (if ¬a = i then polar (⇑Q : (a : M) → N) (f a) (f i) else 0)

Tactic:
rw [if_pos (ne_of_mem_of_not_mem hi ha).symm]

Premises used: Ne.symm, if_pos, ne_of_mem_of_not_mem
-- 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
ι : Type u_8
Q : QuadraticMap R M N
f : ι → M
⊢ (Q : (a : M) → N) (∑ i ∈ ∅, f i) =
    HSub.hSub (α := N) (∑ ij ∈ Finset.sym2 ∅, polarSym2 (⇑Q : (a : M) → N) (Sym2.map f ij))
      (∑ i ∈ ∅, (Q : (a : M) → N) (f i))

Tactic:
simp
-- 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
ι : Type u_8
Q : QuadraticMap R M N
f : ι → M
a : ι
s : Finset ι
ha : a ∉ s
ih :
  (Q : (a : M) → N) (∑ i ∈ s, f i) =
    HSub.hSub (α := N) (∑ ij ∈ s.sym2, polarSym2 (⇑Q : (a : M) → N) (Sym2.map f ij)) (∑ i ∈ s, (Q : (a : M) → N) (f i))
cons :
  HAdd.hAdd (α := N) ((Q : (a : M) → N) (f a) : N)
      (HSub.hSub (α := N) (∑ ij ∈ s.sym2, polarSym2 (⇑Q : (a : M) → N) (Sym2.map f ij))
          (∑ i ∈ s, (Q : (a : M) → N) (f i)) +
        ∑ x ∈ s, polar (⇑Q : (a : M) → N) (f a) (f x)) =
    HSMul.hSMul (α := ℕ) (β := N) 2 ((Q : (a : M) → N) (f a) : N) + ∑ x ∈ s, polar (⇑Q : (a : M) → N) (f a) (f x) +
        ∑ ij ∈ s.sym2, polarSym2 (⇑Q : (a : M) → N) (Sym2.map f ij) -
      HAdd.hAdd (α := N) (β := N) ((Q : (a : M) → N) (f a) : N) (∑ i ∈ s, (Q : (a : M) → N) (f i) : N)
⊢ (Q : (a : M) → N) (∑ i ∈ Finset.cons a s ha, f i) =
    HSub.hSub (α := N) (∑ ij ∈ (Finset.cons a s ha).sym2, polarSym2 (⇑Q : (a : M) → N) (Sym2.map f ij))
      (∑ i ∈ Finset.cons a s ha, (Q : (a : M) → N) (f i))

Tactic:
simp_rw [Finset.sum_cons, QuadraticMap.map_add Q, ih, add_assoc, Finset.sym2_cons,
      Finset.sum_disjUnion, Finset.sum_map, Finset.sum_cons, Sym2.mkEmbedding_apply,
      Sym2.map_mk, polarSym2_sym2Mk, ← polarBilin_apply_apply, _root_.map_sum,
      polarBilin_apply_apply, polar_self]

Premises used: Finset.sum_cons, add_assoc, Finset.sum_map, Sym2.mkEmbedding_apply, QuadraticMap.polar_self, Finset.sum_disjUnion, QuadraticMap.map_add, map_sum, Finset.sym2_cons, Sym2.map_mk, QuadraticMap.polarSym2_sym2Mk, DFunLike.coe, 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 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
ι : Type u_8
Q : QuadraticMap R M N
f : ι → M
a : ι
s : Finset ι
ha : a ∉ s
ih :
  (Q : (a : M) → N) (∑ i ∈ s, f i) =
    HSub.hSub (α := N) (∑ ij ∈ s.sym2, polarSym2 (⇑Q : (a : M) → N) (Sym2.map f ij)) (∑ i ∈ s, (Q : (a : M) → N) (f i))
⊢ HAdd.hAdd (α := N) ((Q : (a : M) → N) (f a) : N)
      (HSub.hSub (α := N) (∑ ij ∈ s.sym2, polarSym2 (⇑Q : (a : M) → N) (Sym2.map f ij))
          (∑ i ∈ s, (Q : (a : M) → N) (f i)) +
        ∑ x ∈ s, polar (⇑Q : (a : M) → N) (f a) (f x)) =
    HSMul.hSMul (α := ℕ) (β := N) 2 ((Q : (a : M) → N) (f a) : N) + ∑ x ∈ s, polar (⇑Q : (a : M) → N) (f a) (f x) +
        ∑ ij ∈ s.sym2, polarSym2 (⇑Q : (a : M) → N) (Sym2.map f ij) -
      HAdd.hAdd (α := N) (β := N) ((Q : (a : M) → N) (f a) : N) (∑ i ∈ s, (Q : (a : M) → N) (f i) : N)

Tactic:
abel_nf
-- 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
ι : Type u_8
Q : QuadraticMap R M N
s : Finset ι
f : ι → M
empty :
  (Q : (a : M) → N) (∑ i ∈ ∅, f i) =
    HSub.hSub (α := N) (∑ ij ∈ Finset.sym2 ∅, polarSym2 (⇑Q : (a : M) → N) (Sym2.map f ij))
      (∑ i ∈ ∅, (Q : (a : M) → N) (f i))
cons :
  ∀ (a : ι) (s : Finset ι) (ha : a ∉ s)
    (ih :
      (Q : (a : M) → N) (∑ i ∈ s, f i) =
        HSub.hSub (α := N) (∑ ij ∈ s.sym2, polarSym2 (⇑Q : (a : M) → N) (Sym2.map f ij))
          (∑ i ∈ s, (Q : (a : M) → N) (f i))),
    (Q : (a : M) → N) (∑ i ∈ Finset.cons a s ha, f i) =
      HSub.hSub (α := N) (∑ ij ∈ (Finset.cons a s ha).sym2, polarSym2 (⇑Q : (a : M) → N) (Sym2.map f ij))
        (∑ i ∈ Finset.cons a s ha, (Q : (a : M) → N) (f i))
⊢ (Q : (a : M) → N) (∑ i ∈ s, f i) =
    HSub.hSub (α := N) (∑ ij ∈ s.sym2, polarSym2 (⇑Q : (a : M) → N) (Sym2.map f ij)) (∑ i ∈ s, (Q : (a : M) → N) (f i))

Tactic:
induction s using Finset.cons_induction with
  | empty => simp
  | cons a s ha ih =>
    simp_rw [Finset.sum_cons, QuadraticMap.map_add Q, ih, add_assoc, Finset.sym2_cons,
      Finset.sum_disjUnion, Finset.sum_map, Finset.sum_cons, Sym2.mkEmbedding_apply,
      Sym2.map_mk, polarSym2_sym2Mk, ← polarBilin_apply_apply, _root_.map_sum,
      polarBilin_apply_apply, polar_self]
    abel_nf

Premises used: Finset.sum_cons, add_assoc, Finset.sum_map, Sym2.mkEmbedding_apply, QuadraticMap.polar_self, Finset.sum_disjUnion, QuadraticMap.map_add, map_sum, Finset.sym2_cons, Sym2.map_mk, QuadraticMap.polarSym2_sym2Mk, DFunLike.coe, QuadraticMap.polarBilin_apply_apply
-- 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 : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : Monoid S
inst_6 : Monoid T
inst_7 : DistribMulAction S N
inst_8 : DistribMulAction T N
inst_9 : SMulCommClass S R N
inst_10 : SMulCommClass T R N
a : S
Q : QuadraticMap R M N
b : R
x : M
rw :
  HSMul.hSMul (β := N) a ((Q : (a : M) → N) (b • x) : N) =
    (b * b) • HSMul.hSMul (β := (a : M) → N) a (⇑Q : (a : M) → N) x
rw₁ :
  a • HSMul.hSMul (β := N) (b * b) ((Q : (a : M) → N) x : N) =
    (b * b) • HSMul.hSMul (β := (a : M) → N) a (⇑Q : (a : M) → N) x
rw₂ :
  a • HSMul.hSMul (β := N) (b * b) ((Q : (a : M) → N) x : N) =
    (b * b) • HSMul.hSMul (β := N) a ((Q : (a : M) → N) x : N)
rw₃ rw₄ :
  (b * b) • HSMul.hSMul (β := N) a ((Q : (a : M) → N) x : N) =
    (b * b) • HSMul.hSMul (β := N) a ((Q : (a : M) → N) x : N)
⊢ HSMul.hSMul (β := (a : M) → N) a (⇑Q : (a : M) → N) (b • x) =
    (b * b) • HSMul.hSMul (β := (a : M) → N) a (⇑Q : (a : M) → N) x

Tactic:
rw [Pi.smul_apply, Q.map_smul, Pi.smul_apply, smul_comm]

Premises used: QuadraticMap.map_smul, SMulCommClass.smul_comm, Pi.smul_apply
-- 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 : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : Monoid S
inst_6 : Monoid T
inst_7 : DistribMulAction S N
inst_8 : DistribMulAction T N
inst_9 : SMulCommClass S R N
inst_10 : SMulCommClass T R N
a : S
Q : QuadraticMap R M N
B : BilinMap R M N
h :
  ∀ (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)
this : SMulCommClass R S N := ⋯
⊢ ∀ (x y : M),
    HSMul.hSMul (β := (a : M) → N) a (⇑Q : (a : M) → N) (x + y) =
      HAdd.hAdd (β := N)
        (HSMul.hSMul (β := (a : M) → N) a (⇑Q : (a : M) → N) x + HSMul.hSMul (β := (a : M) → N) a (⇑Q : (a : M) → N) y)
        ((((a • B : (a : M) → M →ₗ[R] N) x : M →ₗ[R] N) : (a : M) → N) y : N)

Tactic:
simp [h]
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basic
Goal:
S : Type u_1
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
inst_5 : Monoid S
inst_6 : DistribMulAction S N
inst_7 : SMulCommClass S R N
a : S
Q : QuadraticMap R M N
⊢ (⇑(a • Q) : (a : M) → N) = HSMul.hSMul (β := (a : M) → N) a (⇑Q : (a : M) → N)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basic
Goal:
S : Type u_1
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
inst_5 : Monoid S
inst_6 : DistribMulAction S N
inst_7 : SMulCommClass S R N
a : S
Q : QuadraticMap R M N
x : M
⊢ (a • Q : (a : M) → N) x = HSMul.hSMul (β := N) a ((Q : (a : M) → N) x : N)

Tactic:
rfl

Premises used: rfl
-- 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 : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
a : R
x : M
⊢ 0 = HSMul.hSMul (β := N) (a * a) 0

Tactic:
simp only [smul_zero]

Premises used: smul_zero
-- 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 : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
x x_1 : M
⊢ 0 = HAdd.hAdd (β := N) (HAdd.hAdd (α := N) 0 0) ((((0 : (a : M) → M →ₗ[R] N) x : M →ₗ[R] N) : (a : M) → N) x_1 : N)

Tactic:
simp only [add_zero, LinearMap.zero_apply]

Premises used: LinearMap.zero_apply, add_zero
-- 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
⊢ Eq (α := (a : M) → N) (⇑0 : (a : M) → N) 0

Tactic:
rfl

Premises used: 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
x : M
⊢ Eq.{u_5 + 1} (α := N) ((0 : (a : M) → N) x : N) (0 : N)

Tactic:
rfl

Premises used: rfl