mathlib-initiative/mathlib-tactics huggingface dataset:
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 i = P.root l
h₂ : P.root k - P.root j = P.root m
h₃ : P.root k + P.root i - P.root j ∈ range ⇑P.root
hki' : P.pairingIn ℤ k i < 0
hkj' : 0 < P.pairingIn ℤ k j
this✝² : Module.IsReflexive R M := Module.IsReflexive.of_isPerfPair P.toLinearMap
him_mem : P.root i + P.root m ∈ range ⇑P.root
hjl_mem : P.root j + P.root (-l) ∈ range ⇑P.root
hjk_mem : P.root j + P.root (-k) ∈ range ⇑P.root
this✝¹ : InvolutiveNeg ι := P.indexNeg
this✝ : P.IsNotG2
this : IsAddTorsionFree M
hkj_ne : k ≠ j ∧ P.root k ≠ -P.root j
hlj_mem : P.root l - P.root j ∈ range ⇑P.root
hmi : P.pairingIn ℤ m i = 0
hlj : P.pairingIn ℤ l j ≠ 0
aux₀ : P.pairingIn ℤ j i = P.pairingIn ℤ k i
aux₁ : P.pairingIn ℤ i j = -1
aux₂ : P.pairingIn ℤ k j = 2
B : RootPositiveForm ℤ P
⊢ B.rootLength i = B.rootLength j ∧ B.rootLength j < B.rootLength k

Tactic:
by

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 i = P.root l
h₂ : P.root k - P.root j = P.root m
h₃ : P.root k + P.root i - P.root j ∈ range ⇑P.root
hki' : P.pairingIn ℤ k i < 0
hkj' : 0 < P.pairingIn ℤ k j
this✝³ : Module.IsReflexive R M := Module.IsReflexive.of_isPerfPair P.toLinearMap
him_mem : P.root i + P.root m ∈ range ⇑P.root
hjl_mem : P.root j + P.root (-l) ∈ range ⇑P.root
hjk_mem : P.root j + P.root (-k) ∈ range ⇑P.root
this✝² : InvolutiveNeg ι := P.indexNeg
this✝¹ : P.IsNotG2
this✝ : IsAddTorsionFree M
hkj_ne : k ≠ j ∧ P.root k ≠ -P.root j
hlj_mem : P.root l - P.root j ∈ range ⇑P.root
hmi : P.pairingIn ℤ m i = 0
hlj : P.pairingIn ℤ l j ≠ 0
aux₀ : P.pairingIn ℤ j i = P.pairingIn ℤ k i
aux₁ : P.pairingIn ℤ i j = -1
aux₂ : P.pairingIn ℤ k j = 2
B : RootPositiveForm ℤ P
aux₃ : B.rootLength i = B.rootLength j
aux₄ : B.rootLength j < B.rootLength k
this : P.pairingIn ℤ j i = -1
⊢ P.pairingIn ℤ k i = -1

Tactic:
by

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 i = P.root l
h₂ : P.root k - P.root j = P.root m
h₃ : P.root k + P.root i - P.root j ∈ range ⇑P.root
hki' : P.pairingIn ℤ k i < 0
hkj' : 0 < P.pairingIn ℤ k j
this✝² : Module.IsReflexive R M := Module.IsReflexive.of_isPerfPair P.toLinearMap
him_mem : P.root i + P.root m ∈ range ⇑P.root
hjl_mem : P.root j + P.root (-l) ∈ range ⇑P.root
hjk_mem : P.root j + P.root (-k) ∈ range ⇑P.root
this✝¹ : InvolutiveNeg ι := P.indexNeg
this✝ : P.IsNotG2
this : IsAddTorsionFree M
hkj_ne : k ≠ j ∧ P.root k ≠ -P.root j
hlj_mem : P.root l - P.root j ∈ range ⇑P.root
hmi : P.pairingIn ℤ m i = 0
hlj : P.pairingIn ℤ l j ≠ 0
aux₀ : P.pairingIn ℤ j i = P.pairingIn ℤ k i
aux₁ : P.pairingIn ℤ i j = -1
aux₂ : P.pairingIn ℤ k j = 2
B : RootPositiveForm ℤ P
aux₃ : B.rootLength i = B.rootLength j
aux₄ : B.rootLength j < B.rootLength k
⊢ (B.toInvariantForm.form (P.root i)) (P.root i) = (B.toInvariantForm.form (P.root j)) (P.root j)

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
K : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : Field K
inst✝⁹ : CharZero K
inst✝⁸ : DecidableEq ι
inst✝⁷ : Fintype ι
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module K M
inst✝⁴ : AddCommGroup N
inst✝³ : Module K N
P : RootPairing ι K M N
inst✝² : P.IsCrystallographic
b : P.Base
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
_i : InvolutiveNeg ι := P.indexNeg
hωu : ∀ (i : ↥b.support), ω b *ᵥ u i = u i
hωv : ∀ (i : ι), ω b *ᵥ v b i = v b (-i)
j k l m : ι
hm : P.root m = P.root l + P.root k
hk : ∀ {U : LieSubmodule K (↥(lieAlgebra b)) (↥b.support ⊕ ι → K)}, (∀ (k : ↥b.support), u k ∈ U) → v b k ∈ U
hl : l ∈ b.support
U : LieSubmodule K (↥(lieAlgebra b)) (↥b.support ⊕ ι → K)
aux : ∀ (k : ↥b.support), u k ∈ U
e' : ↥(lieAlgebra b) := ⟨e ⟨l, hl⟩, ⋯⟩
this : ⁅e', v b k⁆ = (↑(chainBotCoeff l k) + 1) • v b m
⊢ (↑(chainBotCoeff l k) + 1) • v b m ∈ U

Tactic:
by

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

Goal state before:
pp: ι : 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
hij : i ≠ j
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
hij' : ↑i ≠ ↑j
this : InvolutiveNeg ι := P.indexNeg
k l : ι
h₃ : l ≠ ↑j
h₄ : l ≠ -↑i
h₅ : P.root l + P.root ↑i - P.root ↑j ∈ range ⇑P.root
h₆ : P.root l + P.root ↑i ∉ range ⇑P.root
⊢ P.root l - P.root ↑j ∉ range ⇑P.root

Tactic:
b.root_sub_mem_iff_root_add_mem i j l hij' i.property j.property h₃ _ h₅

Goal state after:
ι : 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
hij : i ≠ j
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
hij' : ↑i ≠ ↑j
this : InvolutiveNeg ι := P.indexNeg
k l : ι
h₃ : l ≠ ↑j
h₄ : l ≠ -↑i
h₅ : P.root l + P.root ↑i - P.root ↑j ∈ range ⇑P.root
h₆ : P.root l + P.root ↑i ∉ range ⇑P.root
⊢ P.root l + P.root ↑i ∉ range ⇑P.root

ι : 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
hij : i ≠ j
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
hij' : ↑i ≠ ↑j
this : InvolutiveNeg ι := P.indexNeg
k l : ι
h₃ : l ≠ ↑j
h₄ : l ≠ -↑i
h₅ : P.root l + P.root ↑i - P.root ↑j ∈ range ⇑P.root
h₆ : P.root l + P.root ↑i ∉ range ⇑P.root
⊢ P.root l ≠ -P.root ↑i
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple

Goal state before:
pp: ι : Type u_1
K : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : Field K
inst✝⁹ : CharZero K
inst✝⁸ : DecidableEq ι
inst✝⁷ : Fintype ι
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module K M
inst✝⁴ : AddCommGroup N
inst✝³ : Module K N
P : RootPairing ι K M N
inst✝² : P.IsCrystallographic
b : P.Base
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
_i : InvolutiveNeg ι := P.indexNeg
hωu : ∀ (i : ↥b.support), ω b *ᵥ u i = u i
hωv : ∀ (i : ι), ω b *ᵥ v b i = v b (-i)
j k l m : ι
hm : P.root m = P.root l + P.root k
hk : ∀ {U : LieSubmodule K (↥(lieAlgebra b)) (↥b.support ⊕ ι → K)}, (∀ (k : ↥b.support), u k ∈ U) → v b k ∈ U
hl : l ∈ b.support
U : LieSubmodule K (↥(lieAlgebra b)) (↥b.support ⊕ ι → K)
aux : ∀ (k : ↥b.support), u k ∈ U
e' : ↥(lieAlgebra b) := ⟨e ⟨l, hl⟩, ⋯⟩
this : (↑(chainBotCoeff l k) + 1) • v b m ∈ U
⊢ ↑(chainBotCoeff l k) + 1 ≠ 0

Tactic:
by

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 i = P.root l
h₂ : P.root k - P.root j = P.root m
h₃ : P.root k + P.root i - P.root j ∈ range ⇑P.root
hki' : P.pairingIn ℤ k i < 0
hkj' : 0 < P.pairingIn ℤ k j
this✝² : Module.IsReflexive R M := Module.IsReflexive.of_isPerfPair P.toLinearMap
him_mem : P.root i + P.root m ∈ range ⇑P.root
hjl_mem : P.root j + P.root (-l) ∈ range ⇑P.root
hjk_mem : P.root j + P.root (-k) ∈ range ⇑P.root
this✝¹ : InvolutiveNeg ι := P.indexNeg
this✝ : P.IsNotG2
this : IsAddTorsionFree M
hkj_ne : k ≠ j ∧ P.root k ≠ -P.root j
hlj_mem : P.root l - P.root j ∈ range ⇑P.root
hmi : P.pairingIn ℤ m i = 0
hlj : P.pairingIn ℤ l j ≠ 0
aux₀ : P.pairingIn ℤ j i = P.pairingIn ℤ k i
aux₁ : P.pairingIn ℤ i j = -1
aux₂ : P.pairingIn ℤ k j = 2
B : RootPositiveForm ℤ P
aux₃ : B.rootLength i = B.rootLength j
aux₄ : B.rootLength j < B.rootLength k
⊢ P.pairingIn ℤ k i = -1

Tactic:
by

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

Goal state before:
pp: ι : 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
hij : i ≠ j
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
hij' : ↑i ≠ ↑j
this : InvolutiveNeg ι := P.indexNeg
k l : ι
h₃ : l ≠ ↑j
h₄ : l ≠ -↑i
h₅ : P.root l + P.root ↑i - P.root ↑j ∈ range ⇑P.root
h₆ : P.root l + P.root ↑i ∉ range ⇑P.root
⊢ P.root l - P.root ↑j ∉ range ⇑P.root

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
K : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : Field K
inst✝⁹ : CharZero K
inst✝⁸ : DecidableEq ι
inst✝⁷ : Fintype ι
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module K M
inst✝⁴ : AddCommGroup N
inst✝³ : Module K N
P : RootPairing ι K M N
inst✝² : P.IsCrystallographic
b : P.Base
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
U : LieSubmodule K (↥(lieAlgebra b)) (↥b.support ⊕ ι → K)
i : ι
hi : v b i ∈ U
⊢ U = ⊤

Tactic:
by

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 i = P.root l
h₂ : P.root k - P.root j = P.root m
h₃ : P.root k + P.root i - P.root j ∈ range ⇑P.root
hki' : P.pairingIn ℤ k i < 0
hkj' : 0 < P.pairingIn ℤ k j
⊢ have this := ⋯;
  P.root i + P.root m ∈ range ⇑P.root →
    P.root j + P.root (-l) ∈ range ⇑P.root →
      P.root j + P.root (-k) ∈ range ⇑P.root → ¬(chainBotCoeff i m = 1 ∧ chainBotCoeff j (-l) = 0)

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
K : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : Field K
inst✝⁷ : CharZero K
inst✝⁶ : DecidableEq ι
inst✝⁵ : Fintype ι
inst✝⁴ : AddCommGroup M
inst✝³ : Module K M
inst✝² : AddCommGroup N
inst✝¹ : Module K N
P : RootPairing ι K M N
inst✝ : P.IsCrystallographic
b : P.Base
w : ↥b.support ⊕ ι → K
hw : w ∈ ↑(genWeightSpace (↥b.support ⊕ ι → K) 0)
i : ι
⊢ ∀ (x : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) K) (hx : x ∈ lieAlgebra b), ⟨x, hx⟩ ∈ H → ∃ k, (toLin' x ^ k) w = 0

Tactic:
by

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 i = P.root l
h₂ : P.root k - P.root j = P.root m
h₃ : P.root k + P.root i - P.root j ∈ range ⇑P.root
⊢ (chainBotCoeff i m + 1) * (chainTopCoeff j k + 1) = (chainTopCoeff j l + 1) * (chainBotCoeff i k + 1)

Tactic:
have := chainBotCoeff_mul_chainTopCoeff.isNotG2 hi hj hij h₁ h₂ h₃

Goal state after:
ι : 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 i = P.root l
h₂ : P.root k - P.root j = P.root m
h₃ : P.root k + P.root i - P.root j ∈ range ⇑P.root
this : P.IsNotG2
⊢ (chainBotCoeff i m + 1) * (chainTopCoeff j k + 1) = (chainTopCoeff j l + 1) * (chainBotCoeff i k + 1)
Module: Mathlib.LinearAlgebra.RootSystem.OfBilinear

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsReflexive R M
B : M →ₗ[R] M →ₗ[R] R
hNB : B.Nondegenerate
hSB : B.IsSymm
h2 : IsRegular 2
x y : ↑{x | B.IsReflective x}
⊢ { toFun := fun x ↦ IsReflective.coroot B ⋯, inj' := ⋯ } y -
      ((Dual.eval R M) ((Embedding.subtype fun x ↦ B.IsReflective x) x))
          ({ toFun := fun x ↦ IsReflective.coroot B ⋯, inj' := ⋯ } y) •
        { toFun := fun x ↦ IsReflective.coroot B ⋯, inj' := ⋯ } x =
    { toFun := fun x ↦ IsReflective.coroot B ⋯, inj' := ⋯ }
      ({ toFun := fun y ↦ ⟨(Module.reflection ⋯) ↑y, ⋯⟩, invFun := fun y ↦ ⟨(Module.reflection ⋯) ↑y, ⋯⟩, left_inv := ⋯,
          right_inv := ⋯ }
        y)

Tactic:
by

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 i = P.root l
h₂ : P.root k - P.root j = P.root m
h₃ : P.root k + P.root i - P.root j ∈ range ⇑P.root
this✝¹ : P.IsNotG2
this✝ : InvolutiveNeg ι := P.indexNeg
this : (chainBotCoeff i m + 1) * (chainBotCoeff j (-k) + 1) = (chainBotCoeff j (-l) + 1) * (chainBotCoeff i k + 1)
⊢ (chainBotCoeff i m + 1) * (chainTopCoeff j k + 1) = (chainTopCoeff j l + 1) * (chainBotCoeff i k + 1)

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
K : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : Field K
inst✝⁷ : CharZero K
inst✝⁶ : DecidableEq ι
inst✝⁵ : Fintype ι
inst✝⁴ : AddCommGroup M
inst✝³ : Module K M
inst✝² : AddCommGroup N
inst✝¹ : Module K N
P : RootPairing ι K M N
inst✝ : P.IsCrystallographic
b : P.Base
w : ↥b.support ⊕ ι → K
i : ι
hw : ∀ (x : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) K) (hx : x ∈ lieAlgebra b), ⟨x, hx⟩ ∈ H → ∃ k, (toLin' x ^ k) w = 0
⊢ ∃ j, P.pairingIn ℤ i ↑j ≠ 0

Tactic:
by

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

Goal state before:
pp: ι : 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
hij : i ≠ j
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
hij' : ↑i ≠ ↑j
this : InvolutiveNeg ι := P.indexNeg
k l : ι
h₃ : l ≠ ↑j
h₄ : l ≠ -↑i
h₅ : P.root l + P.root ↑i - P.root ↑j ∈ range ⇑P.root
h₆ : P.root l + P.root ↑i ∉ range ⇑P.root
h₇ : P.root l - P.root ↑j ∉ range ⇑P.root
x : ι
hx : P.root x = P.root ↑i + P.root l
⊢ P.root x = P.root l + P.root ↑i

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.SModEq.Pow

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I J : Ideal R
p : ℕ
hpI : ↑p ∈ I
x y : R
h : x - y ∈ J
hJI : J ≤ I
h₁ : (Ideal.Quotient.mk I) x = (Ideal.Quotient.mk I) y
⊢ ↑p = 0

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.SModEq.Pow

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I J : Ideal R
p : ℕ
hpI : ↑p ∈ I
x y : R
h : x - y ∈ J
hJI : J ≤ I
h₁ : (Ideal.Quotient.mk I) x = (Ideal.Quotient.mk I) y
h₂ : ↑p = 0
x✝¹ : ℕ
x✝ : x✝¹ ∈ Finset.range p
⊢ (Ideal.Quotient.mk I) y ^ (x✝¹ + (p - 1 - x✝¹)) = (Ideal.Quotient.mk I) y ^ (p - 1)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.SModEq.Pow

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I J : Ideal R
p : ℕ
hpI : ↑p ∈ I
x y : R
h : x ≡ y [SMOD J]
hJI : J ≤ I
⊢ x ^ p ≡ y ^ p [SMOD J * I]

Tactic:
by

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

Goal state before:
pp: ι : 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
hij : i ≠ j
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
hij' : ↑i ≠ ↑j
this : InvolutiveNeg ι := P.indexNeg
k l : ι
h₃ : l ≠ ↑j
h₄ : l ≠ -↑i
h₅ : P.root l + P.root ↑i - P.root ↑j ∈ range ⇑P.root
h₆ : P.root l + P.root ↑i ∉ range ⇑P.root
h₇ : P.root l - P.root ↑j ∉ range ⇑P.root
⊢ ∀ x ∈ Finset.univ, ¬(P.root x = P.root ↑i + P.root l ∧ P.root k = P.root x - P.root ↑j)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.SModEq.Pow

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : Ideal R
p : ℕ
hpI : ↑p ∈ I
x y : R
h : x ≡ y [SMOD I]
m : ℕ
⊢ x ^ p ^ m ≡ y ^ p ^ m [SMOD I ^ (m + 1)]

Tactic:
by

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 i = P.root l
h₂ : P.root k - P.root j = P.root m
h₃ : P.root k + P.root i - P.root j ∈ range ⇑P.root
this✝ : P.IsNotG2
this : InvolutiveNeg ι := P.indexNeg
⊢ P.root i + P.root m ∈ range ⇑P.root

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.SesquilinearForm.Star

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : StarRing R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
B : M →ₗ⋆[R] M →ₗ[R] R
ι : Type u_4
b : Basis ι R M
h : ∀ (i j : ι), star ((B (b i)) (b j)) = (B (b j)) (b i)
x y : M
⊢ x ∈ Submodule.span R (Set.range ⇑b)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.SesquilinearForm.Star

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : StarRing R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
B : M →ₗ⋆[R] M →ₗ[R] R
ι : Type u_4
b : Basis ι R M
h : ∀ (i j : ι), star ((B (b i)) (b j)) = (B (b j)) (b i)
x y : M
fx : M → R
tx : Finset M
ix : ↑tx ⊆ Set.range ⇑b
hx : ∑ a ∈ tx, fx a • a = x
⊢ y ∈ Submodule.span R (Set.range ⇑b)

Tactic:
by

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

Goal state before:
pp: ι : 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
hij : i ≠ j
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
hij' : ↑i ≠ ↑j
this : InvolutiveNeg ι := P.indexNeg
k l : ι
h₃ : l ≠ ↑j
h₄ : l ≠ -↑i
h₅ : P.root l + P.root ↑i - P.root ↑j ∈ range ⇑P.root
h₆ : P.root l + P.root ↑i ∉ range ⇑P.root
h₇ : P.root l - P.root ↑j ∉ range ⇑P.root
aux₃ : ∀ x ∈ Finset.univ, ¬(P.root x = P.root ↑i + P.root l ∧ P.root k = P.root x - P.root ↑j)
⊢ ∀ x ∈ Finset.univ, ¬(P.root x = P.root l - P.root ↑j ∧ P.root k = P.root ↑i + P.root x)

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
K : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : Field K
inst✝⁷ : CharZero K
inst✝⁶ : DecidableEq ι
inst✝⁵ : Fintype ι
inst✝⁴ : AddCommGroup M
inst✝³ : Module K M
inst✝² : AddCommGroup N
inst✝¹ : Module K N
P : RootPairing ι K M N
inst✝ : P.IsCrystallographic
b : P.Base
i : ↥b.support
x : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) K
property✝ : x ∈ lieAlgebra b
hx : ⟨x, property✝⟩ ∈ H
j : ↥b.support ⊕ ι
⊢ (((toEnd K (↥H) (↥b.support ⊕ ι → K)) ⟨⟨x, property✝⟩, hx⟩ - 0 ⟨⟨x, property✝⟩, hx⟩ • 1) ^ 1) (u i) j = 0 j

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.SesquilinearForm.Star

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : StarRing R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
B : M →ₗ⋆[R] M →ₗ[R] R
ι : Type u_4
b : Basis ι R M
⊢ (∀ (i j : ι), star ((B (b i)) (b j)) = (B (b j)) (b i)) → B.IsSymm

Tactic:
by

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 i = P.root l
h₂ : P.root k - P.root j = P.root m
h₃ : P.root k + P.root i - P.root j ∈ range ⇑P.root
this✝ : P.IsNotG2
this : InvolutiveNeg ι := P.indexNeg
him_mem : P.root i + P.root m ∈ range ⇑P.root
hik_mem : P.root k + P.root i ∈ range ⇑P.root
⊢ P.root j + P.root (-k) ∈ range ⇑P.root

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
K : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : Field K
inst✝⁷ : CharZero K
inst✝⁶ : DecidableEq ι
inst✝⁵ : Fintype ι
inst✝⁴ : AddCommGroup M
inst✝³ : Module K M
inst✝² : AddCommGroup N
inst✝¹ : Module K N
P : RootPairing ι K M N
inst✝ : P.IsCrystallographic
b : P.Base
⊢ ↑(genWeightSpace (↥b.support ⊕ ι → K) 0) = span K (range u)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.SesquilinearForm.Star

Goal state before:
pp: R : Type u_1
M : Type u_2
n : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : StarRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Fintype n
inst✝ : DecidableEq n
B : M →ₗ⋆[R] M →ₗ[R] R
b : Basis n R M
⊢ B.IsSymm ↔ ((toMatrix₂ b b) B).IsHermitian

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
K : Type u_2
M : Type u_3
N : Type u_4
inst✝¹² : Field K
inst✝¹¹ : CharZero K
inst✝¹⁰ : DecidableEq ι
inst✝⁹ : Fintype ι
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module K M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module K N
P : RootPairing ι K M N
inst✝⁴ : P.IsRootSystem
inst✝³ : P.IsCrystallographic
b : P.Base
inst✝² : P.IsReduced
inst✝¹ : P.IsIrreducible
inst✝ : Nonempty ι
U : LieSubmodule K (↥(lieAlgebra b)) (↥b.support ⊕ ι → K)
hU : U ≠ ⊥
this : ∃ i, v b i ∈ U
⊢ U = ⊤

Tactic:
by

Goal state after: