mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.QuadraticForm.Basis

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : DecidableEq ι
Q : QuadraticMap R M N
bm : Basis ι R M
x : M
⊢ (linearCombination R (⇑Q ∘ ⇑bm)) (bm.repr x * bm.repr x) +
      ∑ p ∈ (bm.repr x).support.sym2 with ¬p.IsDiag,
        (Sym2.map (⇑(bm.repr x)) p).mul • polarSym2 (⇑Q) (Sym2.map (⇑bm) p) =
    Q x

Tactic:
rw [← apply_linearCombination, Basis.linearCombination_repr]

Goal state after:
Module: Mathlib.LinearAlgebra.QuadraticForm.Basis

Goal state before:
pp: case inl
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁵ : LinearOrder ι
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
bm : Basis ι R M
Q₁ Q₂ : QuadraticMap R M N
i j : ι
h : i < j
⊢ (((Q₁ + Q₂).toBilin bm) (bm i)) (bm j) = ((Q₁.toBilin bm + Q₂.toBilin bm) (bm i)) (bm j)

pp: case inr.inl
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁵ : LinearOrder ι
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
bm : Basis ι R M
Q₁ Q₂ : QuadraticMap R M N
i : ι
⊢ (((Q₁ + Q₂).toBilin bm) (bm i)) (bm i) = ((Q₁.toBilin bm + Q₂.toBilin bm) (bm i)) (bm i)

pp: case inr.inr
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁵ : LinearOrder ι
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
bm : Basis ι R M
Q₁ Q₂ : QuadraticMap R M N
i j : ι
h : j < i
⊢ (((Q₁ + Q₂).toBilin bm) (bm i)) (bm j) = ((Q₁.toBilin bm + Q₂.toBilin bm) (bm i)) (bm j)

Tactic:
· simp [h.ne, h, toBilin_apply, polar_add]

Goal state after:
case inr.inl
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁵ : LinearOrder ι
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
bm : Basis ι R M
Q₁ Q₂ : QuadraticMap R M N
i : ι
⊢ (((Q₁ + Q₂).toBilin bm) (bm i)) (bm i) = ((Q₁.toBilin bm + Q₂.toBilin bm) (bm i)) (bm i)

case inr.inr
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁵ : LinearOrder ι
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
bm : Basis ι R M
Q₁ Q₂ : QuadraticMap R M N
i j : ι
h : j < i
⊢ (((Q₁ + Q₂).toBilin bm) (bm i)) (bm j) = ((Q₁.toBilin bm + Q₂.toBilin bm) (bm i)) (bm j)
Module: Mathlib.LinearAlgebra.QuadraticForm.Real

Goal state before:
pp: ι : Type u_1
inst✝ : Fintype ι
w : ι → ℝ
u : ι → ℝˣ := fun i ↦ if h : w i = 0 then 1 else Units.mk0 (w i) h
hu : ∀ (i : ι), 1 / √|↑(u i)| ≠ 0
hwu : ∀ (i : ι), w i / |↑(u i)| = ↑(sign (w i))
v : ι → ℝ
j : ι
x✝ : j ∈ univ
⊢ w j / |↑(u j)| * v j ^ 2 = w j * (v j ^ 2 * |↑(u j)|⁻¹)

Tactic:
ring

Goal state after:
Module: Mathlib.LinearAlgebra.QuadraticForm.Radical

Goal state before:
pp: R : Type u_1
M : Type u_2
P : Type u_4
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup P
inst✝² : CommRing R
inst✝¹ : Module R M
inst✝ : Module R P
Q : QuadraticMap R M P
N : Submodule R M
hN : N ≤ Q.radical
m m' : M
hmm' : m - m' ∈ N
⊢ Q m' + Q (m - m') + polar (⇑Q) m' (m - m') = Q m'

Tactic:
(hN hmm').1,

Goal state after:
R : Type u_1
M : Type u_2
P : Type u_4
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup P
inst✝² : CommRing R
inst✝¹ : Module R M
inst✝ : Module R P
Q : QuadraticMap R M P
N : Submodule R M
hN : N ≤ Q.radical
m m' : M
hmm' : m - m' ∈ N
⊢ Q m' + 0 + polar (⇑Q) m' (m - m') = Q m'
Module: Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat.Monoidal

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : Invertible 2
X Y Z : QuadraticModuleCat R
⊢ (α_ X.toModuleCat Y.toModuleCat Z.toModuleCat).hom =
    (𝟙 (ModuleCat.of R ↑(X ⊗ Y).toModuleCat ⊗ ModuleCat.of R ↑Z.toModuleCat) ≫
        (𝟙 (ModuleCat.of R ↑X.toModuleCat ⊗ ModuleCat.of R ↑Y.toModuleCat) ⊗ₘ 𝟙 (ModuleCat.of R ↑Z.toModuleCat))) ≫
      (α_ (ModuleCat.of R ↑X.toModuleCat) (ModuleCat.of R ↑Y.toModuleCat) (ModuleCat.of R ↑Z.toModuleCat)).hom ≫
        𝟙 (ModuleCat.of R ↑X.toModuleCat ⊗ ModuleCat.of R ↑Y.toModuleCat ⊗ ModuleCat.of R ↑Z.toModuleCat) ≫
          𝟙 (ModuleCat.of R ↑X.toModuleCat ⊗ ModuleCat.of R ↑(Y ⊗ Z).toModuleCat)

Tactic:
dsimp only [toModuleCat_tensor, ModuleCat.of_coe]

Goal state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : Invertible 2
X Y Z : QuadraticModuleCat R
⊢ (α_ X.toModuleCat Y.toModuleCat Z.toModuleCat).hom =
    (𝟙 ((X.toModuleCat ⊗ Y.toModuleCat) ⊗ Z.toModuleCat) ≫ (𝟙 (X.toModuleCat ⊗ Y.toModuleCat) ⊗ₘ 𝟙 Z.toModuleCat)) ≫
      (α_ X.toModuleCat Y.toModuleCat Z.toModuleCat).hom ≫
        𝟙 (X.toModuleCat ⊗ Y.toModuleCat ⊗ Z.toModuleCat) ≫ 𝟙 (X.toModuleCat ⊗ Y.toModuleCat ⊗ Z.toModuleCat)
Module: Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat.Monoidal

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : Invertible 2
X : QuadraticModuleCat R
⊢ ModuleCat.ofHom (Hom.toIsometry (λ_ X).hom).toLinearMap =
    𝟙 (ModuleCat.of R ↑(𝟙_ (QuadraticModuleCat R)).toModuleCat ⊗ ModuleCat.of R ↑X.toModuleCat) ≫
      𝟙 (𝟙_ (ModuleCat R)) ▷ ModuleCat.of R ↑X.toModuleCat ≫ (λ_ (ModuleCat.of R ↑X.toModuleCat)).hom

Tactic:
dsimp only [toModuleCat_tensor, ModuleCat.of_coe]

Goal state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : Invertible 2
X : QuadraticModuleCat R
⊢ ModuleCat.ofHom (Hom.toIsometry (λ_ X).hom).toLinearMap =
    𝟙 ((𝟙_ (QuadraticModuleCat R)).toModuleCat ⊗ X.toModuleCat) ≫
      𝟙 (𝟙_ (ModuleCat R)) ▷ X.toModuleCat ≫ (λ_ X.toModuleCat).hom
Module: Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat.Monoidal

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : Invertible 2
X : QuadraticModuleCat R
⊢ ModuleCat.ofHom (Hom.toIsometry (ρ_ X).hom).toLinearMap =
    𝟙 (ModuleCat.of R ↑X.toModuleCat ⊗ ModuleCat.of R ↑(𝟙_ (QuadraticModuleCat R)).toModuleCat) ≫
      ModuleCat.of R ↑X.toModuleCat ◁ 𝟙 (𝟙_ (ModuleCat R)) ≫ (ρ_ (ModuleCat.of R ↑X.toModuleCat)).hom

Tactic:
dsimp only [toModuleCat_tensor, ModuleCat.of_coe]

Goal state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : Invertible 2
X : QuadraticModuleCat R
⊢ ModuleCat.ofHom (Hom.toIsometry (ρ_ X).hom).toLinearMap =
    𝟙 (X.toModuleCat ⊗ (𝟙_ (QuadraticModuleCat R)).toModuleCat) ≫
      X.toModuleCat ◁ 𝟙 (𝟙_ (ModuleCat R)) ≫ (ρ_ X.toModuleCat).hom
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Lemmas

Goal state before:
pp: case e'_3
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : CharZero R
inst✝⁶ : IsDomain R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
P : RootPairing ι R M N
inst✝¹ : Finite ι
inst✝ : P.IsCrystallographic
b : P.Base
i j k : ι
hij : i ≠ j
hi : i ∈ b.support
hj : j ∈ b.support
hkj : k ≠ j
hk' : P.root k + P.root i ∈ range ⇑P.root
hm : P.pairingIn ℤ j k ≤ 0
l : ι
hl : P.root l = P.root k + P.root i - P.root j
hli : l ≠ i
hkl : P.pairingIn ℤ l k ≤ 0
hki : P.pairing k i = -1
⊢ 1 = -1 + 2

Tactic:
ring

Goal state after:
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Lemmas

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : CharZero R
inst✝⁸ : IsDomain R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
inst✝³ : Finite ι
inst✝² : P.IsCrystallographic
b : P.Base
i j k l m : ι
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
hi : i ∈ b.support
hj : j ∈ b.support
hij : i ≠ j
h₂ : P.root k - P.root j = P.root m
this✝ : Module.IsReflexive R M
this : IsAddTorsionFree M
contra : P.IsG2
n : ι
h₃ : P.root n = P.root k + P.root i - P.root j
x y : ℤ
h₀ : x • P.root i + y • P.root j = P.root k
s : Set ℤ := {-3, -1, 0, 1, 3}
A : ℤ := P.pairingIn ℤ j i
hki : P.root k ≠ P.root i
hki' : P.root k ≠ -P.root i
hli : P.root l ≠ P.root i
hli' : P.root l ≠ -P.root i
hmi : P.root m ≠ P.root i
hmi' : P.root m ≠ -P.root i
hni : P.root n ≠ P.root i
hni' : P.root n ≠ -P.root i
h₁ : P.root l = (x + 1) • P.root i + y • P.root j
⊢ 2 * (x + 1) + A * y = (x + 1) * 2 + y * P.pairingIn ℤ j i

Tactic:
ring

Goal state after:
Module: Mathlib.LinearAlgebra.RootSystem.Finite.G2

Goal state before:
pp: ι : 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✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : IsDomain R
i j : ι
inst✝ : P.IsNotG2
this : InvolutiveNeg ι := P.indexNeg
h : P.root i + P.root (-j) ∈ Set.range ⇑P.root
⊢ chainTopCoeff i j = if P.pairingIn ℤ i j = 0 then 1 else 0

Tactic:
simpa using P.chainBotCoeff_if_one_zero h

Goal state after:
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Lemmas

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : CharZero R
inst✝⁸ : IsDomain R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
inst✝³ : Finite ι
inst✝² : P.IsCrystallographic
b : P.Base
i j k l m : ι
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
hi : i ∈ b.support
hj : j ∈ b.support
hij : i ≠ j
this✝ : Module.IsReflexive R M
this : IsAddTorsionFree M
contra : P.IsG2
n : ι
h₃ : P.root n = P.root k + P.root i - P.root j
x y : ℤ
h₀ : x • P.root i + y • P.root j = P.root k
s : Set ℤ := {-3, -1, 0, 1, 3}
A : ℤ := P.pairingIn ℤ j i
hki : P.root k ≠ P.root i
hki' : P.root k ≠ -P.root i
hli : P.root l ≠ P.root i
hli' : P.root l ≠ -P.root i
hmi : P.root m ≠ P.root i
hmi' : P.root m ≠ -P.root i
hni : P.root n ≠ P.root i
hni' : P.root n ≠ -P.root i
h₁ : 2 * (x + 1) + A * y ∈ s
h₂ : P.root m = x • P.root i + (y - 1) • P.root j
⊢ 2 * x + A * (y - 1) = x * 2 + (y - 1) * P.pairingIn ℤ j i

Tactic:
ring

Goal state after:
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Lemmas

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : CharZero R
inst✝⁸ : IsDomain R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
inst✝³ : Finite ι
inst✝² : P.IsCrystallographic
b : P.Base
i j k l m : ι
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
hi : i ∈ b.support
hj : j ∈ b.support
hij : i ≠ j
this✝ : Module.IsReflexive R M
this : IsAddTorsionFree M
contra : P.IsG2
n : ι
x y : ℤ
h₀ : x • P.root i + y • P.root j = P.root k
s : Set ℤ := {-3, -1, 0, 1, 3}
A : ℤ := P.pairingIn ℤ j i
hki : P.root k ≠ P.root i
hki' : P.root k ≠ -P.root i
hli : P.root l ≠ P.root i
hli' : P.root l ≠ -P.root i
hmi : P.root m ≠ P.root i
hmi' : P.root m ≠ -P.root i
hni : P.root n ≠ P.root i
hni' : P.root n ≠ -P.root i
h₁ : 2 * (x + 1) + A * y ∈ s
h₂ : 2 * x + A * (y - 1) ∈ s
h₃ : P.root n = (x + 1) • P.root i + (y - 1) • P.root j
⊢ 2 * (x + 1) + A * (y - 1) = (x + 1) * 2 + (y - 1) * P.pairingIn ℤ j i

Tactic:
ring

Goal state after:
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Lemmas

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : CharZero R
inst✝⁸ : IsDomain R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
inst✝³ : Finite ι
inst✝² : P.IsCrystallographic
b : P.Base
i j k l m : ι
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
hi : i ∈ b.support
hj : j ∈ b.support
hij : i ≠ j
this✝ : Module.IsReflexive R M
this : IsAddTorsionFree M
contra : P.IsG2
n : ι
x y : ℤ
h₀ : x • P.root i + y • P.root j = P.root k
s : Set ℤ := {-3, -1, 0, 1, 3}
A : ℤ := P.pairingIn ℤ j i
hki : P.root k ≠ P.root i
hki' : P.root k ≠ -P.root i
hli : P.root l ≠ P.root i
hli' : P.root l ≠ -P.root i
hmi : P.root m ≠ P.root i
hmi' : P.root m ≠ -P.root i
hni : P.root n ≠ P.root i
hni' : P.root n ≠ -P.root i
h₁ : 2 * (x + 1) + A * y ∈ s
h₂ : 2 * x + A * (y - 1) ∈ s
h₃ : 2 * (x + 1) + A * (y - 1) ∈ s
⊢ 2 * x + A * y = x * 2 + y * P.pairingIn ℤ j i

Tactic:
ring

Goal state after:
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Relations

Goal state before:
pp: case inr.inr.inr
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁹ : Finite ι
inst✝⁸ : CommRing R
inst✝⁷ : IsDomain R
inst✝⁶ : CharZero R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
P : RootPairing ι R M N
inst✝¹ : P.IsCrystallographic
b : P.Base
inst✝ : Fintype ι
i j : ↥b.support
k l : ι
hkl : k ≠ l
hkil : P.root k = P.root ↑i + P.root l
⊢ (↑(P.pairingIn ℤ ↑i ↑j) + ↑(P.pairingIn ℤ l ↑j)) * (↑(chainBotCoeff (↑i) l) + 1) -
      (↑(chainBotCoeff (↑i) l) + 1) * ↑(P.pairingIn ℤ l ↑j) =
    ↑(P.pairingIn ℤ ↑i ↑j) * ↑(chainBotCoeff (↑i) l) + ↑(P.pairingIn ℤ ↑i ↑j)

Tactic:
ring

Goal state after:
Module: Mathlib.LinearAlgebra.RootSystem.Finite.G2

Goal state before:
pp: ι : 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✝ : P.EmbeddedG2
B : P.InvariantForm
⊢ (B.form (threeShortAddTwoLongRoot P)) (threeShortAddTwoLongRoot P) = (B.form (longRoot P)) (longRoot P)

Tactic:
simp [threeShortAddTwoLongRoot, threeShortAddTwoLong]

Goal state after:
Module: Mathlib.LinearAlgebra.RootSystem.Finite.G2

Goal state before:
pp: case calc_3
ι : 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✝³ : P.EmbeddedG2
inst✝² : Finite ι
inst✝¹ : CharZero R
inst✝ : IsDomain R
i : ι
this : Fintype ι
B : P.InvariantForm
⊢ 2 * (B.form (P.root i)) (shortRoot P) + 2 * (B.form (P.root i)) (longRoot P) =
    P.pairing i (short P) * (B.form (shortRoot P)) (shortRoot P) +
      P.pairing i (long P) * (B.form (longRoot P)) (longRoot P)

Tactic:
B.two_mul_apply_root_root,

Goal state after:
case calc_3
ι : 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✝³ : P.EmbeddedG2
inst✝² : Finite ι
inst✝¹ : CharZero R
inst✝ : IsDomain R
i : ι
this : Fintype ι
B : P.InvariantForm
⊢ P.pairing i (short P) * (B.form (P.root (short P))) (P.root (short P)) + 2 * (B.form (P.root i)) (longRoot P) =
    P.pairing i (short P) * (B.form (shortRoot P)) (shortRoot P) +
      P.pairing i (long P) * (B.form (longRoot P)) (longRoot P)
Module: Mathlib.LinearAlgebra.RootSystem.Finite.G2

Goal state before:
pp: case calc_4
ι : 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✝³ : P.EmbeddedG2
inst✝² : Finite ι
inst✝¹ : CharZero R
inst✝ : IsDomain R
i : ι
this : Fintype ι
B : P.InvariantForm
⊢ P.pairing i (short P) * (B.form (shortRoot P)) (shortRoot P) +
      P.pairing i (long P) * (3 * (B.form (shortRoot P)) (shortRoot P)) =
    (P.pairing i (short P) + 3 * P.pairing i (long P)) * (B.form (shortRoot P)) (shortRoot P)

Tactic:
ring

Goal state after:
Module: Mathlib.LinearAlgebra.RootSystem.Finite.G2

Goal state before:
pp: case calc_3
ι : 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✝³ : P.EmbeddedG2
inst✝² : Finite ι
inst✝¹ : CharZero R
inst✝ : IsDomain R
i : ι
this : Fintype ι
B : P.InvariantForm
⊢ 2 * (2 * (B.form (P.root i)) (shortRoot P)) + 2 * (B.form (P.root i)) (longRoot P) =
    2 * P.pairing i (short P) * (B.form (shortRoot P)) (shortRoot P) +
      P.pairing i (long P) * (B.form (longRoot P)) (longRoot P)

Tactic:
B.two_mul_apply_root_root,

Goal state after:
case calc_3
ι : 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✝³ : P.EmbeddedG2
inst✝² : Finite ι
inst✝¹ : CharZero R
inst✝ : IsDomain R
i : ι
this : Fintype ι
B : P.InvariantForm
⊢ 2 * (P.pairing i (short P) * (B.form (P.root (short P))) (P.root (short P))) + 2 * (B.form (P.root i)) (longRoot P) =
    2 * P.pairing i (short P) * (B.form (shortRoot P)) (shortRoot P) +
      P.pairing i (long P) * (B.form (longRoot P)) (longRoot P)
Module: Mathlib.LinearAlgebra.RootSystem.Finite.G2

Goal state before:
pp: case calc_3
ι : 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✝³ : P.EmbeddedG2
inst✝² : Finite ι
inst✝¹ : CharZero R
inst✝ : IsDomain R
i : ι
this : Fintype ι
B : P.InvariantForm
⊢ 2 * (P.pairing i (short P) * (B.form (P.root (short P))) (P.root (short P))) + 2 * (B.form (P.root i)) (longRoot P) =
    2 * P.pairing i (short P) * (B.form (shortRoot P)) (shortRoot P) +
      P.pairing i (long P) * (B.form (longRoot P)) (longRoot P)

Tactic:
B.two_mul_apply_root_root,

Goal state after:
case calc_3
ι : 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✝³ : P.EmbeddedG2
inst✝² : Finite ι
inst✝¹ : CharZero R
inst✝ : IsDomain R
i : ι
this : Fintype ι
B : P.InvariantForm
⊢ 2 * (P.pairing i (short P) * (B.form (P.root (short P))) (P.root (short P))) +
      P.pairing i (long P) * (B.form (P.root (long P))) (P.root (long P)) =
    2 * P.pairing i (short P) * (B.form (shortRoot P)) (shortRoot P) +
      P.pairing i (long P) * (B.form (longRoot P)) (longRoot P)
Module: Mathlib.LinearAlgebra.RootSystem.Finite.G2

Goal state before:
pp: case calc_4
ι : 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✝³ : P.EmbeddedG2
inst✝² : Finite ι
inst✝¹ : CharZero R
inst✝ : IsDomain R
i : ι
this : Fintype ι
B : P.InvariantForm
⊢ 2 * P.pairing i (short P) * (B.form (shortRoot P)) (shortRoot P) +
      P.pairing i (long P) * (3 * (B.form (shortRoot P)) (shortRoot P)) =
    (2 * P.pairing i (short P) + 3 * P.pairing i (long P)) * (B.form (shortRoot P)) (shortRoot P)

Tactic:
ring

Goal state after:
Module: Mathlib.LinearAlgebra.RootSystem.Finite.G2

Goal state before:
pp: case calc_2
ι : 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✝³ : P.EmbeddedG2
inst✝² : Finite ι
inst✝¹ : CharZero R
inst✝ : IsDomain R
i : ι
this : Fintype ι
B : P.InvariantForm
⊢ 2 * (3 * (B.form (P.root i)) (shortRoot P)) + 2 * (B.form (P.root i)) (longRoot P) =
    3 * (2 * (B.form (P.root i)) (shortRoot P)) + 2 * (B.form (P.root i)) (longRoot P)

Tactic:
ring

Goal state after:
Module: Mathlib.LinearAlgebra.RootSystem.Finite.G2

Goal state before:
pp: case calc_3
ι : 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✝³ : P.EmbeddedG2
inst✝² : Finite ι
inst✝¹ : CharZero R
inst✝ : IsDomain R
i : ι
this : Fintype ι
B : P.InvariantForm
⊢ 3 * (2 * (B.form (P.root i)) (shortRoot P)) + 2 * (B.form (P.root i)) (longRoot P) =
    P.pairing i (short P) * (B.form (longRoot P)) (longRoot P) +
      P.pairing i (long P) * (B.form (longRoot P)) (longRoot P)

Tactic:
B.two_mul_apply_root_root,

Goal state after:
case calc_3
ι : 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✝³ : P.EmbeddedG2
inst✝² : Finite ι
inst✝¹ : CharZero R
inst✝ : IsDomain R
i : ι
this : Fintype ι
B : P.InvariantForm
⊢ 3 * (P.pairing i (short P) * (B.form (P.root (short P))) (P.root (short P))) + 2 * (B.form (P.root i)) (longRoot P) =
    P.pairing i (short P) * (B.form (longRoot P)) (longRoot P) +
      P.pairing i (long P) * (B.form (longRoot P)) (longRoot P)
Module: Mathlib.LinearAlgebra.RootSystem.Finite.G2

Goal state before:
pp: case calc_3
ι : 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✝³ : P.EmbeddedG2
inst✝² : Finite ι
inst✝¹ : CharZero R
inst✝ : IsDomain R
i : ι
this : Fintype ι
B : P.InvariantForm
⊢ 3 * (P.pairing i (short P) * (B.form (P.root (short P))) (P.root (short P))) + 2 * (B.form (P.root i)) (longRoot P) =
    P.pairing i (short P) * (B.form (longRoot P)) (longRoot P) +
      P.pairing i (long P) * (B.form (longRoot P)) (longRoot P)

Tactic:
B.two_mul_apply_root_root,

Goal state after:
case calc_3
ι : 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✝³ : P.EmbeddedG2
inst✝² : Finite ι
inst✝¹ : CharZero R
inst✝ : IsDomain R
i : ι
this : Fintype ι
B : P.InvariantForm
⊢ 3 * (P.pairing i (short P) * (B.form (P.root (short P))) (P.root (short P))) +
      P.pairing i (long P) * (B.form (P.root (long P))) (P.root (long P)) =
    P.pairing i (short P) * (B.form (longRoot P)) (longRoot P) +
      P.pairing i (long P) * (B.form (longRoot P)) (longRoot P)
Module: Mathlib.LinearAlgebra.RootSystem.Finite.G2

Goal state before:
pp: case calc_3
ι : 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✝³ : P.EmbeddedG2
inst✝² : Finite ι
inst✝¹ : CharZero R
inst✝ : IsDomain R
i : ι
this : Fintype ι
B : P.InvariantForm
⊢ 3 * (P.pairing i (short P) * (B.form (P.root (short P))) (P.root (short P))) +
      P.pairing i (long P) * (3 * (B.form (shortRoot P)) (shortRoot P)) =
    P.pairing i (short P) * (3 * (B.form (shortRoot P)) (shortRoot P)) +
      P.pairing i (long P) * (3 * (B.form (shortRoot P)) (shortRoot P))

Tactic:
ring

Goal state after:
Module: Mathlib.LinearAlgebra.RootSystem.Finite.G2

Goal state before:
pp: case calc_4
ι : 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✝³ : P.EmbeddedG2
inst✝² : Finite ι
inst✝¹ : CharZero R
inst✝ : IsDomain R
i : ι
this : Fintype ι
B : P.InvariantForm
⊢ P.pairing i (short P) * (B.form (longRoot P)) (longRoot P) +
      P.pairing i (long P) * (B.form (longRoot P)) (longRoot P) =
    (P.pairing i (short P) + P.pairing i (long P)) * (B.form (longRoot P)) (longRoot P)

Tactic:
ring

Goal state after:
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Relations

Goal state before:
pp: case inl.inl
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : Finite ι
inst✝⁹ : CommRing R
inst✝⁸ : IsDomain R
inst✝⁷ : CharZero R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
P : RootPairing ι R M N
inst✝² : P.IsCrystallographic
b : P.Base
inst✝¹ : Fintype ι
i : ↥b.support
inst✝ : P.IsReduced
k : ι
hki : k ≠ ↑i
hki' : k ≠ (P.reflectionPerm ↑i) ↑i
h_lin_ind : LinearIndependent R ![P.root ↑i, P.root k]
x : ι
hx : P.root k = P.root ↑i + P.root x
y : ι
hy : P.root k = P.root y - P.root ↑i
h_lin_ind_x : LinearIndependent R ![P.root ↑i, P.root x]
h_lin_ind_y : LinearIndependent R ![P.root ↑i, P.root y]
hx' : chainBotCoeff (↑i) k = chainBotCoeff (↑i) x + 1
hy' : chainTopCoeff (↑i) k = chainTopCoeff (↑i) y + 1
⊢ (↑(chainBotCoeff (↑i) x) + 1) * (↑(chainTopCoeff (↑i) y) + ↑1 + 1) -
      (↑(chainTopCoeff (↑i) y) + 1) * (↑(chainBotCoeff (↑i) x) + ↑1 + 1) =
    ↑(chainBotCoeff (↑i) x) + ↑1 - (↑(chainTopCoeff (↑i) y) + ↑1)

Tactic:
ring

Goal state after: