-- Mathlib/LinearAlgebra/QuadraticForm/Basis.lean
theorem toQuadraticMap_toBilin (Q : QuadraticMap R M N) (bm : Basis ι R M) :
    (Q.toBilin bm).toQuadraticMap = Q

Proof state:
case H
ι : Type u_4
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁵ : LinearOrder ι
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticMap R M N
bm : Basis ι R M
x : M
⊢ (Q.toBilin bm).toQuadraticMap x = Q x

Tactic:
rw [← bm.linearCombination_repr x, LinearMap.BilinMap.toQuadraticMap_apply,
    Finsupp.linearCombination_apply, Finsupp.sum]

Result:
case H
ι : Type u_4
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁵ : LinearOrder ι
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticMap R M N
bm : Basis ι R M
x : M
⊢ ((Q.toBilin bm) (∑ a ∈ (bm.repr x).support, (bm.repr x) a • bm a)) (∑ a ∈ (bm.repr x).support, (bm.repr x) a • bm a) =
    Q (∑ a ∈ (bm.repr x).support, (bm.repr x) a • bm a)

Proof state:
case H
ι : Type u_4
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁵ : LinearOrder ι
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticMap R M N
bm : Basis ι R M
x : M
⊢ ∑ x_1 ∈ (bm.repr x).support, (bm.repr x) x_1 • (bm.repr x) x_1 • Q (bm x_1) +
      ∑ a ∈ Finset.filter (fun a => a.1 < a.2) (bm.repr x).support.offDiag,
        (bm.repr x) a.1 • (bm.repr x) a.2 • polar (⇑Q) (bm a.1) (bm a.2) =
    ∑ i ∈ (bm.repr x).support, Q ((bm.repr x) i • bm i) +
      ∑ ij ∈ Finset.filter (fun ij => ¬ij.IsDiag) (bm.repr x).support.sym2,
        polarSym2 (⇑Q) (Sym2.map (fun a => (bm.repr x) a • bm a) ij)

Tactic:
simp_rw [← polar_smul_right _ (bm.repr x <| Prod.snd _),
  ← polar_smul_left _ (bm.repr x <| Prod.fst _)]

Result:
case H
ι : Type u_4
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁵ : LinearOrder ι
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticMap R M N
bm : Basis ι R M
x : M
⊢ ∑ x_1 ∈ (bm.repr x).support, (bm.repr x) x_1 • (bm.repr x) x_1 • Q (bm x_1) +
      ∑ x_1 ∈ Finset.filter (fun a => a.1 < a.2) (bm.repr x).support.offDiag,
        polar (⇑Q) ((bm.repr x) x_1.1 • bm x_1.1) ((bm.repr x) x_1.2 • bm x_1.2) =
    ∑ i ∈ (bm.repr x).support, Q ((bm.repr x) i • bm i) +
      ∑ ij ∈ Finset.filter (fun ij => ¬ij.IsDiag) (bm.repr x).support.sym2,
        polarSym2 (⇑Q) (Sym2.map (fun a => (bm.repr x) a • bm a) ij)

Proof state:
case H
ι : Type u_4
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁵ : LinearOrder ι
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticMap R M N
bm : Basis ι R M
x : M
⊢ ∑ x_1 ∈ (bm.repr x).support, (bm.repr x) x_1 • (bm.repr x) x_1 • Q (bm x_1) +
      ∑ x_1 ∈ Finset.filter (fun a => a.1 < a.2) (bm.repr x).support.offDiag,
        polar (⇑Q) ((bm.repr x) x_1.1 • bm x_1.1) ((bm.repr x) x_1.2 • bm x_1.2) =
    ∑ i ∈ (bm.repr x).support, Q ((bm.repr x) i • bm i) +
      ∑ ij ∈ Finset.filter (fun ij => ¬ij.IsDiag) (bm.repr x).support.sym2,
        polarSym2 (⇑Q) (Sym2.map (fun a => (bm.repr x) a • bm a) ij)

Tactic:
simp_rw [QuadraticMap.map_smul, mul_smul, Finset.sum_sym2_filter_not_isDiag]

Result:
case H
ι : Type u_4
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁵ : LinearOrder ι
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticMap R M N
bm : Basis ι R M
x : M
⊢ ∑ x_1 ∈ (bm.repr x).support, (bm.repr x) x_1 • (bm.repr x) x_1 • Q (bm x_1) +
      ∑ x_1 ∈ Finset.filter (fun a => a.1 < a.2) (bm.repr x).support.offDiag,
        polar (⇑Q) ((bm.repr x) x_1.1 • bm x_1.1) ((bm.repr x) x_1.2 • bm x_1.2) =
    ∑ x_1 ∈ (bm.repr x).support, (bm.repr x) x_1 • (bm.repr x) x_1 • Q (bm x_1) +
      ∑ i ∈ Finset.filter (fun a => a.1 < a.2) (bm.repr x).support.offDiag,
        polarSym2 (⇑Q) (Sym2.map (fun a => (bm.repr x) a • bm a) s(i.1, i.2))

Proof state:
case H.h
ι : Type u_4
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁵ : LinearOrder ι
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticMap R M N
bm : Basis ι R M
x✝ : M
x : ι × ι
hx : x.1 ∈ (bm.repr x✝).support ∧ x.2 ∈ (bm.repr x✝).support ∧ x.1 ≠ x.2
⊢ ¬x.1 = x.2

Tactic:
simpa using hx.2.2

Result:
no goals

Proof state:
case H.h
ι : Type u_4
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁵ : LinearOrder ι
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticMap R M N
bm : Basis ι R M
x : M
⊢ ∀ x_1 ∈ (bm.repr x).support.offDiag, ¬x_1.1 = x_1.2

Tactic:
intro x hx

Result:
case H.h
ι : Type u_4
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁵ : LinearOrder ι
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticMap R M N
bm : Basis ι R M
x✝ : M
x : ι × ι
hx : x ∈ (bm.repr x✝).support.offDiag
⊢ ¬x.1 = x.2

Proof state:
case H
ι : Type u_4
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁵ : LinearOrder ι
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticMap R M N
bm : Basis ι R M
x : M
⊢ (∑ x_1 ∈ (bm.repr x).support, (bm.repr x) x_1 • (bm.repr x) x_1 • Q (bm x_1) +
      ∑ x_1 ∈ (bm.repr x).support.offDiag,
        if x_1.1 = x_1.2 then (bm.repr x) x_1.1 • (bm.repr x) x_1.2 • Q (bm x_1.1)
        else if x_1.1 < x_1.2 then (bm.repr x) x_1.1 • (bm.repr x) x_1.2 • polar (⇑Q) (bm x_1.1) (bm x_1.2) else 0) =
    Q (∑ a ∈ (bm.repr x).support, (bm.repr x) a • bm a)

Tactic:
rw [Finset.sum_ite_of_false, QuadraticMap.map_sum, ← Finset.sum_filter]

Result:
case H
ι : Type u_4
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁵ : LinearOrder ι
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticMap R M N
bm : Basis ι R M
x : M
⊢ ∑ x_1 ∈ (bm.repr x).support, (bm.repr x) x_1 • (bm.repr x) x_1 • Q (bm x_1) +
      ∑ a ∈ Finset.filter (fun a => a.1 < a.2) (bm.repr x).support.offDiag,
        (bm.repr x) a.1 • (bm.repr x) a.2 • polar (⇑Q) (bm a.1) (bm a.2) =
    ∑ i ∈ (bm.repr x).support, Q ((bm.repr x) i • bm i) +
      ∑ ij ∈ Finset.filter (fun ij => ¬ij.IsDiag) (bm.repr x).support.sym2,
        polarSym2 (⇑Q) (Sym2.map (fun a => (bm.repr x) a • bm a) ij)

case H.h
ι : Type u_4
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁵ : LinearOrder ι
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticMap R M N
bm : Basis ι R M
x : M
⊢ ∀ x_1 ∈ (bm.repr x).support.offDiag, ¬x_1.1 = x_1.2

Proof state:
case H
ι : Type u_4
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁵ : LinearOrder ι
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticMap R M N
bm : Basis ι R M
x : M
⊢ ∑ x_1 ∈ (bm.repr x).support, (bm.repr x) x_1 • (bm.repr x) x_1 • Q (bm x_1) +
      ∑ x_1 ∈ Finset.filter (fun a => a.1 < a.2) (bm.repr x).support.offDiag,
        polar (⇑Q) ((bm.repr x) x_1.1 • bm x_1.1) ((bm.repr x) x_1.2 • bm x_1.2) =
    ∑ x_1 ∈ (bm.repr x).support, (bm.repr x) x_1 • (bm.repr x) x_1 • Q (bm x_1) +
      ∑ i ∈ Finset.filter (fun a => a.1 < a.2) (bm.repr x).support.offDiag,
        polarSym2 (⇑Q) (Sym2.map (fun a => (bm.repr x) a • bm a) s(i.1, i.2))

Tactic:
rfl

Result:
no goals