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

Goal state before:
pp: case neg
R : Type u_4
inst✝⁶ : CommRing R
V : Type u_5
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : Module.Free R V
inst✝² : Module.Finite R V
ι : Type u_6
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Module.Basis ι R V
g : ↥(center (Matrix.SpecialLinearGroup ι R))
a✝ : Nontrivial R
hV : Nontrivial V
hι : ¬IsEmpty ι
this✝ : FaithfulSMul R V
g' : ↥(center (_root_.SpecialLinearGroup R V)) := (centerCongr (toLin_equiv b)) g
hgg' : ∀ (x : V), ↑↑↑g' x = ↑↑((toLin_equiv b) ↑g) x
x : V
this : ↑↑(centerEquivRootsOfUnity g') • x = ↑↑g' x
⊢ (↑↑(center_equiv_rootsOfUnity g) • LinearMap.id) x = ↑↑(center_equiv_rootsOfUnity g) • x

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
M : Type u_2
M' : Type u_3
P : Type u_4
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup M'
inst✝⁴ : AddCommGroup P
inst✝³ : CommRing R
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R P
Q : QuadraticMap R M P
⊢ 0 ∈ {x | Q x = 0 ∧ Q.polarBilin x = 0}

Tactic:
simp

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

Goal state before:
pp: case neg
ι : 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
i : ι
hi : ¬w i = 0
⊢ w i = |w i| * ↑(sign (w i))

Tactic:
simp

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
⊢ m = m' + (m - m')

Tactic:
simp

Goal state after:
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 =
    𝟙 ((𝟙_ (QuadraticModuleCat R)).toModuleCat ⊗ X.toModuleCat) ≫
      𝟙 ((𝟙_ (QuadraticModuleCat R)).toModuleCat ⊗ X.toModuleCat) ≫ (λ_ X.toModuleCat).hom

Tactic:
simp

Goal state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : Invertible 2
X : QuadraticModuleCat R
⊢ ModuleCat.ofHom (Hom.toIsometry (λ_ X).hom).toLinearMap = (λ_ 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 =
    𝟙 (X.toModuleCat ⊗ (𝟙_ (QuadraticModuleCat R)).toModuleCat) ≫
      𝟙 (X.toModuleCat ⊗ (𝟙_ (QuadraticModuleCat R)).toModuleCat) ≫ (ρ_ X.toModuleCat).hom

Tactic:
simp

Goal state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : Invertible 2
X : QuadraticModuleCat R
⊢ ModuleCat.ofHom (Hom.toIsometry (ρ_ X).hom).toLinearMap = (ρ_ X.toModuleCat).hom
Module: Mathlib.LinearAlgebra.QuadraticForm.TensorProduct.Isometries

Goal state before:
pp: R : Type uR
M₂ : Type uM₂
inst✝³ : CommRing R
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M₂
inst✝ : Invertible 2
Q₂ : QuadraticForm R M₂
m✝ : M₂
⊢ (comp Q₂ ↑(TensorProduct.lid R M₂)) (1 ⊗ₜ[R] m✝) = (QuadraticForm.tmul QuadraticMap.sq Q₂) (1 ⊗ₜ[R] m✝)

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : CommRing R
inst✝² : LinearOrder R
inst✝¹ : Module R M
Q : QuadraticForm R M
inst✝ : Module R M'
Q' : QuadraticForm R M'
h : Equivalent Q Q'
e : IsometryEquiv Q Q'
⊢ ∀ (m : M), (-Q') ((↑e.toLinearEquiv).toFun m) = (-Q) m

Tactic:
simp

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

Goal state before:
pp: case convert_8
𝕜 : Type u_4
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
ι : Type u_5
inst✝¹ : Fintype ι
w : ι → 𝕜
inst✝ : IsStrictOrderedRing 𝕜
p : Set ι := {i | 0 < w i}
m : Set ι := {i | w i ≤ 0}
this✝ : p.ncard + m.ncard = Nat.card ι
this : p.ncard ≤ sigPos (weightedSumSquares 𝕜 w)
⊢ sigPos (weightedSumSquares 𝕜 w) + m.ncard ≤ Nat.card ι

Tactic:
simpa using sigPos_add_finrank_le_of_nonpos <| negSemidef_spanSubset m (fun _ hi ↦ hi)

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

Goal state before:
pp: case e'_2
𝕜 : Type u_4
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
ι : Type u_5
inst✝¹ : Fintype ι
w : ι → 𝕜
inst✝ : IsStrictOrderedRing 𝕜
x✝ : ι → 𝕜
⊢ (-weightedSumSquares 𝕜 w) x✝ = (weightedSumSquares 𝕜 (-w)) x✝

Tactic:
simp

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

Goal state before:
pp: case e'_3
𝕜 : Type u_4
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
ι : Type u_5
inst✝¹ : Fintype ι
w : ι → 𝕜
inst✝ : IsStrictOrderedRing 𝕜
⊢ {i | w i < 0} = {i | 0 < (-w) i}

Tactic:
simp

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

Goal state before:
pp: case inl.inl
ι : 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.IsCrystallographic
b : P.Base
inst✝ : DecidableEq ι
d : ι → R
x y : Matrix ι ι R
i j : ↥b.support
⊢ fromBlocks 0 0 0 (x + y) (Sum.inl i) (Sum.inl j) = (fromBlocks 0 0 0 x + fromBlocks 0 0 0 y) (Sum.inl i) (Sum.inl j)

Tactic:
simp

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

Goal state before:
pp: case inl.inr
ι : 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.IsCrystallographic
b : P.Base
inst✝ : DecidableEq ι
d : ι → R
x y : Matrix ι ι R
i : ↥b.support
j : ι
⊢ fromBlocks 0 0 0 (x + y) (Sum.inl i) (Sum.inr j) = (fromBlocks 0 0 0 x + fromBlocks 0 0 0 y) (Sum.inl i) (Sum.inr j)

Tactic:
simp

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

Goal state before:
pp: case inr.inl
ι : 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.IsCrystallographic
b : P.Base
inst✝ : DecidableEq ι
d : ι → R
x y : Matrix ι ι R
i : ι
j : ↥b.support
⊢ fromBlocks 0 0 0 (x + y) (Sum.inr i) (Sum.inl j) = (fromBlocks 0 0 0 x + fromBlocks 0 0 0 y) (Sum.inr i) (Sum.inl j)

Tactic:
simp

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

Goal state before:
pp: case inr.inr
ι : 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.IsCrystallographic
b : P.Base
inst✝ : DecidableEq ι
d : ι → R
x y : Matrix ι ι R
i j : ι
⊢ fromBlocks 0 0 0 (x + y) (Sum.inr i) (Sum.inr j) = (fromBlocks 0 0 0 x + fromBlocks 0 0 0 y) (Sum.inr i) (Sum.inr j)

Tactic:
simp

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

Goal state before:
pp: case inl.inl
ι : 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.IsCrystallographic
b : P.Base
inst✝ : DecidableEq ι
d : ι → R
t : R
x : Matrix ι ι R
i j : ↥b.support
⊢ fromBlocks 0 0 0 (t • x) (Sum.inl i) (Sum.inl j) = ((RingHom.id R) t • fromBlocks 0 0 0 x) (Sum.inl i) (Sum.inl j)

Tactic:
simp

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

Goal state before:
pp: case inl.inr
ι : 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.IsCrystallographic
b : P.Base
inst✝ : DecidableEq ι
d : ι → R
t : R
x : Matrix ι ι R
i : ↥b.support
j : ι
⊢ fromBlocks 0 0 0 (t • x) (Sum.inl i) (Sum.inr j) = ((RingHom.id R) t • fromBlocks 0 0 0 x) (Sum.inl i) (Sum.inr j)

Tactic:
simp

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

Goal state before:
pp: case inr.inl
ι : 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.IsCrystallographic
b : P.Base
inst✝ : DecidableEq ι
d : ι → R
t : R
x : Matrix ι ι R
i : ι
j : ↥b.support
⊢ fromBlocks 0 0 0 (t • x) (Sum.inr i) (Sum.inl j) = ((RingHom.id R) t • fromBlocks 0 0 0 x) (Sum.inr i) (Sum.inl j)

Tactic:
simp

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

Goal state before:
pp: case inr.inr
ι : 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.IsCrystallographic
b : P.Base
inst✝ : DecidableEq ι
d : ι → R
t : R
x : Matrix ι ι R
i j : ι
⊢ fromBlocks 0 0 0 (t • x) (Sum.inr i) (Sum.inr j) = ((RingHom.id R) t • fromBlocks 0 0 0 x) (Sum.inr i) (Sum.inr j)

Tactic:
simp

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

Goal state before:
pp: case zero
ι : 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.IsCrystallographic
b : P.Base
i : ↥b.support
j : ↥b.support ⊕ ι
x : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R
⊢ 0 j (Sum.inl i) = 0

Tactic:
simp

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

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.IsCrystallographic
b : P.Base
inst✝⁴ : Finite ι
inst✝³ : IsDomain R
inst✝² : CharZero R
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i : ↥b.support
⊢ h i ∈ range h ∪ range e ∪ range f

Tactic:
simp

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

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.IsCrystallographic
b : P.Base
inst✝⁴ : Finite ι
inst✝³ : IsDomain R
inst✝² : CharZero R
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i : ↥b.support
⊢ e i ∈ range h ∪ range e ∪ range f

Tactic:
simp

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

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.IsCrystallographic
b : P.Base
inst✝⁴ : Finite ι
inst✝³ : IsDomain R
inst✝² : CharZero R
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i : ↥b.support
⊢ f i ∈ range h ∪ range e ∪ range f

Tactic:
simp

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 : ι
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.pairingIn ℤ k i = -1
⊢ (algebraMap ℤ R) (-1) = -1

Tactic:
simp

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

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
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
inst✝² : P.IsReduced
b : P.Base
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i : ↥b.support
j : ι
n✝ : ℕ
h : j ≠ -↑i
this✝¹ : Module.IsReflexive R M
this✝ : IsAddTorsionFree M
this : InvolutiveNeg ι := P.indexNeg
n : ℕ
⊢ e i *ᵥ e i ^ n *ᵥ Pi.single (Sum.inr j) 1 = e i *ᵥ (e i ^ n).col (Sum.inr j)

Tactic:
simp

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

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
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
inst✝² : P.IsReduced
b : P.Base
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i : ↥b.support
j : ι
h : j ≠ -↑i
this✝¹ : Module.IsReflexive R M
this✝ : IsAddTorsionFree M
this : InvolutiveNeg ι := P.indexNeg
aux : ∀ (n : ℕ), (e i ^ (n + 1)).col (Sum.inr j) = e i *ᵥ (e i ^ n).col (Sum.inr j)
⊢ P.root j = P.root j + 0 • P.root ↑i

Tactic:
simp

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

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.IsCrystallographic
b : P.Base
inst✝³ : Finite ι
inst✝² : IsDomain R
inst✝¹ : CharZero R
inst✝ : Fintype ι
i j : ↥b.support
⊢ ⁅e i, f j⁆ * ω b = -ω b * ⁅e j, f i⁆

Tactic:
by
  calc ⁅e i, f j⁆ * ω b = e i * f j * ω b - f j * e i * ω b := by rw [Ring.lie_def, sub_mul]
                      _ = e i * (f j * ω b) - f j * (e i * ω b) := by rw [mul_assoc, mul_assoc]
                      _ = e i * (ω b * e j) - f j * (ω b * f i) := by rw [← ω_mul_e, ← ω_mul_f]
                      _ = (e i * ω b) * e j - (f j * ω b) * f i := by rw [← mul_assoc, ← mul_assoc]
                      _ = (ω b * f i) * e j - (ω b * e j) * f i := by rw [← ω_mul_e, ← ω_mul_f]
                      _ = ω b * (f i * e j) - ω b * (e j * f i) := by rw [mul_assoc, mul_assoc]
                      _ = -ω b * ⁅e j, f i⁆ := ?_
  rw [Ring.lie_def, mul_sub, neg_mul, neg_mul, sub_neg_eq_add]
  abel

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

Goal state before:
pp: case zero
ι : 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
b : P.Base
inst✝ : DecidableEq ι
j : ι
x : ↥b.support ⊕ ι → R
⊢ 0 (Sum.inr j) = 0

Tactic:
simp

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

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.IsCrystallographic
b : P.Base
inst✝⁴ : Finite ι
inst✝³ : IsDomain R
inst✝² : CharZero R
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
x✝ : ↥(cartanSubalgebra' b)
d : ↥b.support ⊕ ι → R
hx' : Matrix.diagonal d ∈ lieAlgebra b
hx : ⟨Matrix.diagonal d, hx'⟩ ∈ cartanSubalgebra' b
⊢ ⨆ φ,
      ((LieModule.toEnd R (↥(cartanSubalgebra' b)) (↥b.support ⊕ ι → R))
            ⟨⟨Matrix.diagonal d, hx'⟩, hx⟩).maxGenEigenspace
        φ =
    ⊤

Tactic:
simp

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.IsCrystallographic
inst✝⁴ : P.IsReduced
inst✝³ : P.IsIrreducible
inst✝² : Finite ι
inst✝¹ : CharZero R
inst✝ : IsDomain R
⊢ ¬P.IsG2 ↔ P.IsNotG2

Tactic:
simp only [isG2_iff, isNotG2_iff, not_exists, Set.mem_insert_iff, mem_singleton_iff]

Goal state after:
ι : 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.IsCrystallographic
inst✝⁴ : P.IsReduced
inst✝³ : P.IsIrreducible
inst✝² : Finite ι
inst✝¹ : CharZero R
inst✝ : IsDomain R
⊢ (∀ (x x_1 : ι), ¬P.pairingIn ℤ x x_1 = -3) ↔
    ∀ (i j : ι),
      P.pairingIn ℤ i j = -2 ∨
        P.pairingIn ℤ i j = -1 ∨ P.pairingIn ℤ i j = 0 ∨ P.pairingIn ℤ i j = 1 ∨ P.pairingIn ℤ i j = 2
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic

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.IsCrystallographic
b : P.Base
inst✝⁴ : Finite ι
inst✝³ : IsDomain R
inst✝² : CharZero R
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
t : R
x : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R
⊢ ω b * t • x * ω b = (RingHom.id R) t • (ω b * x * ω b)

Tactic:
simp

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

Goal state before:
pp: case zero
ι : 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.IsCrystallographic
b : P.Base
inst✝⁴ : Finite ι
inst✝³ : IsDomain R
inst✝² : CharZero R
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
x : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R
⊢ (ωConj b) 0 ∈ lieAlgebra b

Tactic:
simp

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
inst✝ : P.IsIrreducible
⊢ P.pairingIn ℤ (long P) (short P) = -3

Tactic:
simp

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
⊢ (algebraMap ℤ R) (-3) = -3

Tactic:
simp

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

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.IsCrystallographic
b : P.Base
inst✝⁴ : Finite ι
inst✝³ : IsDomain R
inst✝² : CharZero R
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
N : LieSubmodule R (↥(lieAlgebra b)) (↥b.support ⊕ ι → R)
x : ↥b.support ⊕ ι → R
⊢ (Matrix.toLin' (ω b)) ((Matrix.toLin' (ω b)) x) = x

Tactic:
simp

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

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.IsCrystallographic
b : P.Base
inst✝⁴ : Finite ι
inst✝³ : IsDomain R
inst✝² : CharZero R
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
N : LieSubmodule R (↥(lieAlgebra b)) (↥b.support ⊕ ι → R)
e : Submodule R (↥b.support ⊕ ι → R) ≃o Submodule R (↥b.support ⊕ ι → R) :=
  orderIsoMapComapOfBijective (Matrix.toLin' (ω b)) ⋯
⊢ e.symm ↑N = ⊤ ↔ N = ⊤

Tactic:
simp

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

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.IsCrystallographic
b : P.Base
inst✝⁴ : Finite ι
inst✝³ : IsDomain R
inst✝² : CharZero R
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
N : LieSubmodule R (↥(lieAlgebra b)) (↥b.support ⊕ ι → R)
⊢ ωConjLieSubmodule N = ⊤ ↔ N = ⊤

Tactic:
rw [← LieSubmodule.toSubmodule_eq_top]
  let e : Submodule R (b.support ⊕ ι → R) ≃o Submodule R (b.support ⊕ ι → R) :=
    Submodule.orderIsoMapComapOfBijective (ω b).toLin' (Involutive.bijective fun x ↦ by simp)
  change e.symm N = ⊤ ↔ _
  simp

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

Goal state before:
pp: case inl
ι : 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✝ : DecidableEq M
⊢ longRoot P ∈ Set.range ⇑P.root

Tactic:
simp

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

Goal state before:
pp: case inr.inl
ι : 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✝ : DecidableEq M
⊢ -longRoot P ∈ Set.range ⇑P.root

Tactic:
simp

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

Goal state before:
pp: case inr.inr.inl
ι : 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✝ : DecidableEq M
⊢ shortRoot P ∈ Set.range ⇑P.root

Tactic:
simp

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

Goal state before:
pp: case inr.inr.inr.inl
ι : 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✝ : DecidableEq M
⊢ -shortRoot P ∈ Set.range ⇑P.root

Tactic:
simp

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

Goal state before:
pp: case inr.inr.inr.inr.inl
ι : 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✝ : DecidableEq M
⊢ shortAddLongRoot P ∈ Set.range ⇑P.root

Tactic:
simp

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

Goal state before:
pp: case inr.inr.inr.inr.inr.inl
ι : 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✝ : DecidableEq M
⊢ -shortAddLongRoot P ∈ Set.range ⇑P.root

Tactic:
simp

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

Goal state before:
pp: case inr.inr.inr.inr.inr.inr.inl
ι : 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✝ : DecidableEq M
⊢ twoShortAddLongRoot P ∈ Set.range ⇑P.root

Tactic:
simp

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

Goal state before:
pp: case inr.inr.inr.inr.inr.inr.inr.inl
ι : 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✝ : DecidableEq M
⊢ -twoShortAddLongRoot P ∈ Set.range ⇑P.root

Tactic:
simp

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

Goal state before:
pp: case inr.inr.inr.inr.inr.inr.inr.inr.inl
ι : 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✝ : DecidableEq M
⊢ threeShortAddLongRoot P ∈ Set.range ⇑P.root

Tactic:
simp

Goal state after: