-- Mathlib/LinearAlgebra/QuadraticForm/Basic.lean
theorem map_sum {ι} [DecidableEq ι] (Q : QuadraticMap R M N) (s : Finset ι) (f : ι → M) :
    Q (∑ i ∈ s, f i) = ∑ i ∈ s, Q (f i)
      + ∑ ij ∈ s.sym2 with ¬ ij.IsDiag, polarSym2 Q (ij.map f)

Proof state:
case cons
R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
ι : Type u_8
inst✝ : DecidableEq ι
Q : QuadraticMap R M N
f : ι → M
a : ι
s : Finset ι
ha : a ∉ s
ih :
  Q (∑ i ∈ s, f i) =
    ∑ i ∈ s, Q (f i) + ∑ ij ∈ Finset.filter (fun ij => ¬ij.IsDiag) s.sym2, polarSym2 (⇑Q) (Sym2.map f ij)
⊢ Q (∑ i ∈ Finset.cons a s ha, f i) =
    ∑ i ∈ Finset.cons a s ha, Q (f i) +
      ∑ ij ∈ Finset.filter (fun ij => ¬ij.IsDiag) (Finset.cons a s ha).sym2, polarSym2 (⇑Q) (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.isDiag_iff_proj_eq, not_true, if_false, zero_add,
  Sym2.map_pair_eq, polarSym2_sym2Mk, ← polarBilin_apply_apply, _root_.map_sum,
  polarBilin_apply_apply]

Result:
case cons
R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
ι : Type u_8
inst✝ : DecidableEq ι
Q : QuadraticMap R M N
f : ι → M
a : ι
s : Finset ι
ha : a ∉ s
ih :
  Q (∑ i ∈ s, f i) =
    ∑ i ∈ s, Q (f i) + ∑ ij ∈ Finset.filter (fun ij => ¬ij.IsDiag) s.sym2, polarSym2 (⇑Q) (Sym2.map f ij)
⊢ Q (f a) +
      (∑ i ∈ s, Q (f i) +
        ((∑ a ∈ s.sym2, if ¬a.IsDiag then polarSym2 (⇑Q) (Sym2.map f a) else 0) + ∑ x ∈ s, polar (⇑Q) (f a) (f x))) =
    Q (f a) +
      (∑ i ∈ s, Q (f i) +
        ((∑ x ∈ s, if ¬a = x then polar (⇑Q) (f a) (f x) else 0) +
          ∑ a ∈ s.sym2, if ¬a.IsDiag then polarSym2 (⇑Q) (Sym2.map f a) else 0))

Proof state:
case cons.e_a.e_a
R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
ι : Type u_8
inst✝ : DecidableEq ι
Q : QuadraticMap R M N
f : ι → M
a : ι
s : Finset ι
ha : a ∉ s
ih :
  Q (∑ i ∈ s, f i) =
    ∑ i ∈ s, Q (f i) + ∑ ij ∈ Finset.filter (fun ij => ¬ij.IsDiag) s.sym2, polarSym2 (⇑Q) (Sym2.map f ij)
⊢ (∑ x ∈ s, polar (⇑Q) (f a) (f x) + ∑ a ∈ s.sym2, if ¬a.IsDiag then polarSym2 (⇑Q) (Sym2.map f a) else 0) =
    (∑ x ∈ s, if ¬a = x then polar (⇑Q) (f a) (f x) else 0) +
      ∑ a ∈ s.sym2, if ¬a.IsDiag then polarSym2 (⇑Q) (Sym2.map f a) else 0

Tactic:
congr! with i hi

Result:
case cons.e_a.e_a.h.e'_5.a
R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
ι : Type u_8
inst✝ : DecidableEq ι
Q : QuadraticMap R M N
f : ι → M
a : ι
s : Finset ι
ha : a ∉ s
ih :
  Q (∑ i ∈ s, f i) =
    ∑ i ∈ s, Q (f i) + ∑ ij ∈ Finset.filter (fun ij => ¬ij.IsDiag) s.sym2, polarSym2 (⇑Q) (Sym2.map f ij)
i : ι
hi : i ∈ s
⊢ polar (⇑Q) (f a) (f i) = if ¬a = i then polar (⇑Q) (f a) (f i) else 0

Proof state:
case empty
R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
ι : Type u_8
inst✝ : DecidableEq ι
Q : QuadraticMap R M N
f : ι → M
⊢ Q (∑ i ∈ ∅, f i) =
    ∑ i ∈ ∅, Q (f i) + ∑ ij ∈ Finset.filter (fun ij => ¬ij.IsDiag) ∅.sym2, polarSym2 (⇑Q) (Sym2.map f ij)

Tactic:
simp

Result:
no goals

Proof state:
case cons.e_a.e_a
R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
ι : Type u_8
inst✝ : DecidableEq ι
Q : QuadraticMap R M N
f : ι → M
a : ι
s : Finset ι
ha : a ∉ s
ih :
  Q (∑ i ∈ s, f i) =
    ∑ i ∈ s, Q (f i) + ∑ ij ∈ Finset.filter (fun ij => ¬ij.IsDiag) s.sym2, polarSym2 (⇑Q) (Sym2.map f ij)
⊢ (∑ a ∈ s.sym2, if ¬a.IsDiag then polarSym2 (⇑Q) (Sym2.map f a) else 0) + ∑ x ∈ s, polar (⇑Q) (f a) (f x) =
    (∑ x ∈ s, if ¬a = x then polar (⇑Q) (f a) (f x) else 0) +
      ∑ a ∈ s.sym2, if ¬a.IsDiag then polarSym2 (⇑Q) (Sym2.map f a) else 0

Tactic:
rw [add_comm]

Result:
case cons.e_a.e_a
R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
ι : Type u_8
inst✝ : DecidableEq ι
Q : QuadraticMap R M N
f : ι → M
a : ι
s : Finset ι
ha : a ∉ s
ih :
  Q (∑ i ∈ s, f i) =
    ∑ i ∈ s, Q (f i) + ∑ ij ∈ Finset.filter (fun ij => ¬ij.IsDiag) s.sym2, polarSym2 (⇑Q) (Sym2.map f ij)
⊢ (∑ x ∈ s, polar (⇑Q) (f a) (f x) + ∑ a ∈ s.sym2, if ¬a.IsDiag then polarSym2 (⇑Q) (Sym2.map f a) else 0) =
    (∑ x ∈ s, if ¬a = x then polar (⇑Q) (f a) (f x) else 0) +
      ∑ a ∈ s.sym2, if ¬a.IsDiag then polarSym2 (⇑Q) (Sym2.map f a) else 0

Proof state:
case cons.e_a.e_a.h.e'_5.a
R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
ι : Type u_8
inst✝ : DecidableEq ι
Q : QuadraticMap R M N
f : ι → M
a : ι
s : Finset ι
ha : a ∉ s
ih :
  Q (∑ i ∈ s, f i) =
    ∑ i ∈ s, Q (f i) + ∑ ij ∈ Finset.filter (fun ij => ¬ij.IsDiag) s.sym2, polarSym2 (⇑Q) (Sym2.map f ij)
i : ι
hi : i ∈ s
⊢ polar (⇑Q) (f a) (f i) = if ¬a = i then polar (⇑Q) (f a) (f i) else 0

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

Result:
no goals

Proof state:
R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
ι : Type u_8
inst✝ : DecidableEq ι
Q : QuadraticMap R M N
s : Finset ι
f : ι → M
⊢ Q (∑ i ∈ s, f i) =
    ∑ i ∈ s, Q (f i) + ∑ ij ∈ Finset.filter (fun ij => ¬ij.IsDiag) s.sym2, polarSym2 (⇑Q) (Sym2.map f ij)

Tactic:
induction s using Finset.cons_induction with
| empty => simp
| cons a s ha ih =>
  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.isDiag_iff_proj_eq, not_true, if_false, zero_add,
    Sym2.map_pair_eq, polarSym2_sym2Mk, ← polarBilin_apply_apply, _root_.map_sum,
    polarBilin_apply_apply]
  congr 2
  rw [add_comm]
  congr! with i hi
  rw [if_pos (ne_of_mem_of_not_mem hi ha).symm]

Result:
no goals

Proof state:
case cons
R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
ι : Type u_8
inst✝ : DecidableEq ι
Q : QuadraticMap R M N
f : ι → M
a : ι
s : Finset ι
ha : a ∉ s
ih :
  Q (∑ i ∈ s, f i) =
    ∑ i ∈ s, Q (f i) + ∑ ij ∈ Finset.filter (fun ij => ¬ij.IsDiag) s.sym2, polarSym2 (⇑Q) (Sym2.map f ij)
⊢ Q (f a) +
      (∑ i ∈ s, Q (f i) +
        ((∑ a ∈ s.sym2, if ¬a.IsDiag then polarSym2 (⇑Q) (Sym2.map f a) else 0) + ∑ x ∈ s, polar (⇑Q) (f a) (f x))) =
    Q (f a) +
      (∑ i ∈ s, Q (f i) +
        ((∑ x ∈ s, if ¬a = x then polar (⇑Q) (f a) (f x) else 0) +
          ∑ a ∈ s.sym2, if ¬a.IsDiag then polarSym2 (⇑Q) (Sym2.map f a) else 0))

Tactic:
congr 2

Result:
case cons.e_a.e_a
R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
ι : Type u_8
inst✝ : DecidableEq ι
Q : QuadraticMap R M N
f : ι → M
a : ι
s : Finset ι
ha : a ∉ s
ih :
  Q (∑ i ∈ s, f i) =
    ∑ i ∈ s, Q (f i) + ∑ ij ∈ Finset.filter (fun ij => ¬ij.IsDiag) s.sym2, polarSym2 (⇑Q) (Sym2.map f ij)
⊢ (∑ a ∈ s.sym2, if ¬a.IsDiag then polarSym2 (⇑Q) (Sym2.map f a) else 0) + ∑ x ∈ s, polar (⇑Q) (f a) (f x) =
    (∑ x ∈ s, if ¬a = x then polar (⇑Q) (f a) (f x) else 0) +
      ∑ a ∈ s.sym2, if ¬a.IsDiag then polarSym2 (⇑Q) (Sym2.map f a) else 0