-- 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 : ι
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 = P.Polarization (P.root i) + P.Polarization (P.root i)

Tactic:
nth_rw 2 [hP]

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 =
    P.Polarization (P.root i) + ∑ j : ι, P.pairing i ((P.reflection_perm i) j) • P.coroot ((P.reflection_perm i) j)

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)
⊢ (P.RootForm (P.root i)) (P.root i) • P.coroot i = 2 • P.Polarization (P.root i)

Tactic:
rw [two_nsmul]

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 = P.Polarization (P.root i) + 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)
⊢ (P.RootForm (P.root i)) (P.root i) • P.coroot i =
    ∑ x : ι, P.pairing i x • P.coroot x +
      ∑ x : ι,
        (-(P.pairing i x • P.coroot x) + P.pairing i x • (P.toPerfectPairing (P.root i)) (P.coroot x) • P.coroot i)

Tactic:
rw [Finset.sum_add_distrib, ← add_assoc, ← sub_eq_iff_eq_add]

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 -
      ∑ x : ι, P.pairing i x • (P.toPerfectPairing (P.root i)) (P.coroot x) • P.coroot i =
    ∑ x : ι, P.pairing i x • P.coroot x + ∑ x : ι, -(P.pairing i x • P.coroot x)

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)
⊢ (P.RootForm (P.root i)) (P.root i) • P.coroot i -
      ∑ x : ι, P.pairing i x • (P.toPerfectPairing (P.root i)) (P.coroot x) • P.coroot i =
    ∑ x : ι, P.pairing i x • P.coroot x + ∑ x : ι, -(P.pairing i x • P.coroot x)

Tactic:
simp only [rootForm_apply_apply, LinearMap.coe_comp, comp_apply, Polarization_apply,
  root_coroot_eq_pairing, map_sum, LinearMapClass.map_smul, Finset.sum_neg_distrib, ← smul_assoc]

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 =
    ∑ x : ι, P.pairing i x • P.coroot x + -∑ x : ι, P.pairing i x • P.coroot x

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)
⊢ (P.RootForm (P.root i)) (P.root i) • P.coroot i =
    ∑ i_1 : ι, (P.coroot' i_1) (P.root i) • P.coroot i_1 +
      ∑ j : ι, P.pairing i ((P.reflection_perm i) j) • P.coroot ((P.reflection_perm i) j)

Tactic:
simp only [root_coroot'_eq_pairing, pairing_reflection_perm, pairing_reflection_perm_self_left,
  ← reflection_perm_coroot, smul_sub, neg_smul, sub_neg_eq_add]

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 =
    ∑ x : ι, P.pairing i x • P.coroot x +
      ∑ x : ι,
        (-(P.pairing i x • P.coroot x) + P.pairing i x • (P.toPerfectPairing (P.root i)) (P.coroot x) • P.coroot 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 =
    0

Tactic:
exact sub_eq_zero_of_eq rfl

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 : ι
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 =
    P.Polarization (P.root i) + ∑ j : ι, P.pairing i ((P.reflection_perm i) j) • P.coroot ((P.reflection_perm i) j)

Tactic:
rw [Polarization_apply]

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 =
    ∑ i_1 : ι, (P.coroot' i_1) (P.root i) • P.coroot i_1 +
      ∑ j : ι, P.pairing i ((P.reflection_perm i) j) • P.coroot ((P.reflection_perm i) j)