-- Mathlib/LinearAlgebra/RootSystem/Finite/CanonicalBilinear.lean
/-- This is SGA3 XXI Lemma 1.2.1 (10), key for proving nondegeneracy and positivity. -/
lemma rootForm_self_smul_coroot (i : ι) :
    (P.RootForm (P.root i) (P.root i)) • P.coroot i = 2 • P.Polarization (P.root i)

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
P : RootPairing ι R M N
inst✝ : Fintype ι
i : ι
⊢ ∑ x : ι, P.pairing i x • P.coroot x =
    ∑ j : ι, P.pairing i ((P.reflection_perm i) j) • P.coroot ((P.reflection_perm i) j)

Tactic:
exact (Fintype.sum_equiv (P.reflection_perm i)
      (fun j ↦ P.pairing i (P.reflection_perm i j) • P.coroot (P.reflection_perm i j))
      (fun j ↦ P.pairing i j • P.coroot j) (congrFun rfl)).symm

Result:
no goals

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
P : RootPairing ι R M N
inst✝ : Fintype ι
i : ι
⊢ (P.RootForm (P.root i)) (P.root i) • P.coroot i = 2 • P.Polarization (P.root i)

Tactic:
have hP : P.Polarization (P.root i) =
    ∑ j : ι, P.pairing i (P.reflection_perm i j) • P.coroot (P.reflection_perm i j) := by
  simp_rw [Polarization_apply, root_coroot'_eq_pairing]
  exact (Fintype.sum_equiv (P.reflection_perm i)
        (fun j ↦ P.pairing i (P.reflection_perm i j) • P.coroot (P.reflection_perm i j))
        (fun j ↦ P.pairing i j • P.coroot j) (congrFun rfl)).symm

Result:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
P : RootPairing ι R M N
inst✝ : Fintype ι
i : ι
hP : P.Polarization (P.root i) = ∑ j : ι, P.pairing i ((P.reflection_perm i) j) • P.coroot ((P.reflection_perm i) j)
⊢ (P.RootForm (P.root i)) (P.root i) • P.coroot i = 2 • P.Polarization (P.root i)

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
P : RootPairing ι R M N
inst✝ : Fintype ι
i : ι
hP : P.Polarization (P.root i) = ∑ j : ι, P.pairing i ((P.reflection_perm i) j) • P.coroot ((P.reflection_perm i) j)
⊢ (∑ i_1 : ι, (P.coroot' i_1) (P.root i) * (P.coroot' i_1) (P.root i)) • P.coroot i -
      ∑ x : ι, (P.pairing i x • P.pairing i x) • P.coroot i =
    ∑ x : ι, P.pairing i x • P.coroot x + -∑ x : ι, P.pairing i x • P.coroot x

Tactic:
rw [Finset.sum_smul, add_neg_eq_zero.mpr rfl]

Result:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
P : RootPairing ι R M N
inst✝ : Fintype ι
i : ι
hP : P.Polarization (P.root i) = ∑ j : ι, P.pairing i ((P.reflection_perm i) j) • P.coroot ((P.reflection_perm i) j)
⊢ ∑ i_1 : ι, ((P.coroot' i_1) (P.root i) * (P.coroot' i_1) (P.root i)) • P.coroot i -
      ∑ x : ι, (P.pairing i x • P.pairing i x) • P.coroot i =
    0

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
P : RootPairing ι R M N
inst✝ : Fintype ι
i : ι
⊢ P.Polarization (P.root i) = ∑ j : ι, P.pairing i ((P.reflection_perm i) j) • P.coroot ((P.reflection_perm i) j)

Tactic:
simp_rw [Polarization_apply, root_coroot'_eq_pairing]

Result:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
P : RootPairing ι R M N
inst✝ : Fintype ι
i : ι
⊢ ∑ x : ι, P.pairing i x • P.coroot x =
    ∑ j : ι, P.pairing i ((P.reflection_perm i) j) • P.coroot ((P.reflection_perm i) j)