mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.RootSystem.Finite.G2

Goal state before:
pp: case h₈
ι : 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 : ι
h₁ : ¬P.root i = longRoot P
h₂ : ¬P.root i = -longRoot P
h₃ : ¬P.root i = shortRoot P
h₄ : ¬P.root i = -shortRoot P
h₅ : ¬P.root i = shortAddLongRoot P
h₆ : ¬P.root i = -shortAddLongRoot P
h₇ : ¬P.root i = twoShortAddLongRoot P
h₈ : ¬P.root i = -twoShortAddLongRoot P
h₉ : ¬P.root i = threeShortAddLongRoot P
h₁₀ : ¬P.root i = -threeShortAddLongRoot P
h₁₁ : ¬P.root i = threeShortAddTwoLongRoot P
h₁₂ : ¬P.root i = -threeShortAddTwoLongRoot P
ha :
  (P.pairingIn ℤ i (short P), P.pairingIn ℤ (short P) i) ∈
    {(0, 0), (1, 1), (-1, -1), (1, 2), (2, 1), (-1, -2), (-2, -1), (1, 3), (3, 1), (-1, -3), (-3, -1)}
hb :
  (P.pairingIn ℤ i (long P), P.pairingIn ℤ (long P) i) ∈
    {(0, 0), (1, 1), (-1, -1), (1, 2), (2, 1), (-1, -2), (-2, -1), (1, 3), (3, 1), (-1, -3), (-3, -1)}
hc :
  (P.pairingIn ℤ i (shortAddLong P), P.pairingIn ℤ (shortAddLong P) i) ∈
    {(0, 0), (1, 1), (-1, -1), (1, 2), (2, 1), (-1, -2), (-2, -1), (1, 3), (3, 1), (-1, -3), (-3, -1)}
hd :
  (P.pairingIn ℤ i (twoShortAddLong P), P.pairingIn ℤ (twoShortAddLong P) i) ∈
    {(0, 0), (1, 1), (-1, -1), (1, 2), (2, 1), (-1, -2), (-2, -1), (1, 3), (3, 1), (-1, -3), (-3, -1)}
he :
  (P.pairingIn ℤ i (threeShortAddLong P), P.pairingIn ℤ (threeShortAddLong P) i) ∈
    {(0, 0), (1, 1), (-1, -1), (1, 2), (2, 1), (-1, -2), (-2, -1), (1, 3), (3, 1), (-1, -3), (-3, -1)}
hf :
  (P.pairingIn ℤ i (threeShortAddTwoLong P), P.pairingIn ℤ (threeShortAddTwoLong P) i) ∈
    {(0, 0), (1, 1), (-1, -1), (1, 2), (2, 1), (-1, -2), (-2, -1), (1, 3), (3, 1), (-1, -3), (-3, -1)}
⊢ P.pairingIn ℤ (threeShortAddTwoLong P) i = 3 * P.pairingIn ℤ (short P) i + 2 * P.pairingIn ℤ (long P) i

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✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : IsDomain R
inst✝ : P.IsIrreducible
⊢ {long P, short P}.Nonempty

Tactic:
simp

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 : ↥b.support
inst✝¹ : P.IsReduced
inst✝ : DecidableEq ι
⊢ b.cartanMatrix i i • e i = 2 • e i

Tactic:
simp

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 : ↥b.support
inst✝¹ : P.IsReduced
inst✝ : DecidableEq ι
⊢ -b.cartanMatrix i i • f i = -(2 • f i)

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✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : IsDomain R
inst✝ : P.IsIrreducible
this : LinearIndependent R ![shortRoot P, longRoot P]
⊢ ⊤ ≤ Submodule.span R (Set.range ![shortRoot P, longRoot P])

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✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : IsDomain R
inst✝ : P.IsIrreducible
i : ι
hi : P.root i ∉ allRoots P
this✝ : Fintype ι
B : P.InvariantForm
h₂ : (B.form (P.root i)) (P.root (long P)) = 0
h₁ : (B.form (P.root i)) (P.root (short P)) = 0
this : Module.IsReflexive R M
x : M
⊢ x ∈ Submodule.span R {longRoot P, shortRoot P}

Tactic:
simp

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

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.EmbeddedG2
inst✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : IsDomain R
inst✝ : P.IsIrreducible
i : ι
hi : P.root i ∉ allRoots P
this✝ : Fintype ι
B : P.InvariantForm
h₂ : (B.form (P.root i)) (P.root (long P)) = 0
h₁ : (B.form (P.root i)) (P.root (short P)) = 0
this : Module.IsReflexive R M
x : M
⊢ (B.form (P.root i)) 0 = 0

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✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : IsDomain R
inst✝ : P.IsIrreducible
i : ι
⊢ (fun x ↦ Exists.choose ⋯) ((fun i ↦ ⟨P.root i, ⋯⟩) i) = i

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✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : IsDomain R
inst✝ : P.IsIrreducible
⊢ (allRoots P).length = 12

Tactic:
simp

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

Goal state before:
pp: case 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
hij : i ≠ j
hij' : ↑i ≠ ↑j
this : InvolutiveNeg ι := P.indexNeg
k : ι
hk : k ≠ ↑i
⊢ 0 - ∑ x, 0 = 0

Tactic:
simp

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

Goal state before:
pp: ι : Type u_1
K : Type u_2
M : Type u_3
N : Type u_4
inst✝¹¹ : Fintype ι
inst✝¹⁰ : DecidableEq ι
inst✝⁹ : Field K
inst✝⁸ : CharZero K
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module K M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module K N
P : RootPairing ι K M N
inst✝³ : P.IsReduced
inst✝² : P.IsCrystallographic
inst✝¹ : P.IsIrreducible
inst✝ : P.IsRootSystem
b : P.Base
h₀ : ↥b.support → ↥(lieAlgebra b) := fun i ↦ ⟨h i, ⋯⟩
e₀ : ↥b.support → ↥(lieAlgebra b) := fun i ↦ ⟨e i, ⋯⟩
f₀ : ↥b.support → ↥(lieAlgebra b) := fun i ↦ ⟨f i, ⋯⟩
⊢ range e₀ ∪ range f₀ ⊆ range h₀ ∪ (range e₀ ∪ range f₀)

Tactic:
simp

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

Goal state before:
pp: case h₁
ι : 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 : ι
_i : InvolutiveNeg ι := ⋯
hωu : ∀ (i : ↥b.support), ω b *ᵥ u i = u i
hωv : ∀ (i : ι), ω b *ᵥ v b i = v b (-i)
⊢ ∀ i ∈ b.support, ∀ {U : LieSubmodule K (↥(lieAlgebra b)) (↥b.support ⊕ ι → K)}, v b i ∈ U → ∃ j, u j ∈ U

Tactic:
intro j

Goal state after:
case h₁
ι : 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 : ι
_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 : ι
⊢ j ∈ b.support → ∀ {U : LieSubmodule K (↥(lieAlgebra b)) (↥b.support ⊕ ι → K)}, v b j ∈ U → ∃ j, u j ∈ U
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Relations

Goal state before:
pp: case 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
hij : i ≠ j
this : InvolutiveNeg ι := P.indexNeg
k : ι
aux : ⁅e i, f j⁆ (Sum.inr k) (Sum.inr (-↑i)) = (⁅e i, f j⁆ * ω b) (Sum.inr k) (Sum.inr ↑i)
⊢ (0 ⬝ᵥ fun j ↦ (-ω b)ᵀ j (Sum.inr k)) = 0 (Sum.inr k)

Tactic:
simp

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

Goal state before:
pp: ι : Type u_1
K : Type u_2
M : Type u_3
N : Type u_4
inst✝¹¹ : Fintype ι
inst✝¹⁰ : DecidableEq ι
inst✝⁹ : Field K
inst✝⁸ : CharZero K
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module K M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module K N
P : RootPairing ι K M N
inst✝³ : P.IsReduced
inst✝² : P.IsCrystallographic
inst✝¹ : P.IsIrreducible
inst✝ : P.IsRootSystem
b : P.Base
h₀ : ↥b.support → ↥(lieAlgebra b) := fun i ↦ ⟨h i, ⋯⟩
e₀ : ↥b.support → ↥(lieAlgebra b) := fun i ↦ ⟨e i, ⋯⟩
f₀ : ↥b.support → ↥(lieAlgebra b) := fun i ↦ ⟨f i, ⋯⟩
i : ↥b.support
hef : h₀ i = ⁅e₀ i, f₀ i⁆
⊢ e₀ i ∈ range e₀ ∪ range f₀

Tactic:
simp

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

Goal state before:
pp: ι : Type u_1
K : Type u_2
M : Type u_3
N : Type u_4
inst✝¹¹ : Fintype ι
inst✝¹⁰ : DecidableEq ι
inst✝⁹ : Field K
inst✝⁸ : CharZero K
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module K M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module K N
P : RootPairing ι K M N
inst✝³ : P.IsReduced
inst✝² : P.IsCrystallographic
inst✝¹ : P.IsIrreducible
inst✝ : P.IsRootSystem
b : P.Base
h₀ : ↥b.support → ↥(lieAlgebra b) := fun i ↦ ⟨h i, ⋯⟩
e₀ : ↥b.support → ↥(lieAlgebra b) := fun i ↦ ⟨e i, ⋯⟩
f₀ : ↥b.support → ↥(lieAlgebra b) := fun i ↦ ⟨f i, ⋯⟩
i : ↥b.support
hef : h₀ i = ⁅e₀ i, f₀ i⁆
⊢ f₀ i ∈ range e₀ ∪ range f₀

Tactic:
simp

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

Goal state before:
pp: case h₂
ι : 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 : ι
_i : InvolutiveNeg ι := ⋯
hωu : ∀ (i : ↥b.support), ω b *ᵥ u i = u i
hωv : ∀ (i : ι), ω b *ᵥ v b i = v b (-i)
⊢ ∀ (i j k : ι),
    P.root k = P.root i + P.root j →
      (∀ {U : LieSubmodule K (↥(lieAlgebra b)) (↥b.support ⊕ ι → K)}, v b i ∈ U → ∃ j, u j ∈ U) →
        j ∈ b.support → ∀ {U : LieSubmodule K (↥(lieAlgebra b)) (↥b.support ⊕ ι → K)}, v b k ∈ U → ∃ j, u j ∈ U

Tactic:
intro j

Goal state after:
case h₂
ι : 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 : ι
_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 : ι
⊢ ∀ (j_1 k : ι),
    P.root k = P.root j + P.root j_1 →
      (∀ {U : LieSubmodule K (↥(lieAlgebra b)) (↥b.support ⊕ ι → K)}, v b j ∈ U → ∃ j, u j ∈ U) →
        j_1 ∈ b.support → ∀ {U : LieSubmodule K (↥(lieAlgebra b)) (↥b.support ⊕ ι → K)}, v b k ∈ U → ∃ j, u j ∈ U
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basis

Goal state before:
pp: ι : Type u_1
K : Type u_2
M : Type u_3
N : Type u_4
inst✝¹¹ : Fintype ι
inst✝¹⁰ : DecidableEq ι
inst✝⁹ : Field K
inst✝⁸ : CharZero K
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module K M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module K N
P : RootPairing ι K M N
inst✝³ : P.IsReduced
inst✝² : P.IsCrystallographic
inst✝¹ : P.IsIrreducible
inst✝ : P.IsRootSystem
b : P.Base
i j : ↥b.support
hij : i ≠ j
⊢ ⁅⟨e i, ⋯⟩, ⟨f j, ⋯⟩⁆ = 0

Tactic:
by simp [Subtype.ext_iff, lie_e_f_ne hij]

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 : InvolutiveNeg ι := P.indexNeg
hωu : ∀ (i : ↥b.support), ω b *ᵥ u i = u i
hωv : ∀ (i : ι), ω b *ᵥ v b i = v b (-i)
aux : ∀ (k : ↥b.support), u k ∈ U
⊢ ∀ (j : ι), v b j ∈ U

Tactic:
intro j

Goal state after:
ι : 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 : InvolutiveNeg ι := P.indexNeg
hωu : ∀ (i : ↥b.support), ω b *ᵥ u i = u i
hωv : ∀ (i : ι), ω b *ᵥ v b i = v b (-i)
aux : ∀ (k : ↥b.support), u k ∈ U
j : ι
⊢ v b j ∈ U
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple

Goal state before:
pp: case h₀
ι : 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 ι := ⋯
hωu : ∀ (i : ↥b.support), ω b *ᵥ u i = u i
hωv : ∀ (i : ι), ω b *ᵥ v b i = v b (-i)
j : ι
⊢ ∀ (i : ι),
    (∀ {U : LieSubmodule K (↥(lieAlgebra b)) (↥b.support ⊕ ι → K)}, (∀ (k : ↥b.support), u k ∈ U) → v b i ∈ U) →
      ∀ {U : LieSubmodule K (↥(lieAlgebra b)) (↥b.support ⊕ ι → K)},
        (∀ (k : ↥b.support), u k ∈ U) → v b ((P.reflectionPerm i) i) ∈ U

Tactic:
intro j

Goal state after:
case h₀
ι : 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✝ j : ι
⊢ (∀ {U : LieSubmodule K (↥(lieAlgebra b)) (↥b.support ⊕ ι → K)}, (∀ (k : ↥b.support), u k ∈ U) → v b j ∈ U) →
    ∀ {U : LieSubmodule K (↥(lieAlgebra b)) (↥b.support ⊕ ι → K)},
      (∀ (k : ↥b.support), u k ∈ U) → v b ((P.reflectionPerm j) j) ∈ U
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:
simp

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:
simp

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)
U' : LieSubmodule K (↥H) (↥b.support ⊕ ι → K) := { toSubmodule := ↑U, lie_mem := ⋯ }
hU : ↑U ≤ span K (range u)
x : ↥b.support ⊕ ι → K
hx : x ∈ U
c : ↥b.support → K
hc : ∑ i, c i • u i = x
hCM : c ≠ 0
j : ↥b.support
this : ∑ k, c k * ↑|b.cartanMatrix j k| = 0
⊢ ((b.cartanMatrix.map abs).map Int.cast *ᵥ c) j = 0 j

Tactic:
by
    simpa [mulVec_eq_sum, -Base.cartanMatrix_map_abs]

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

Goal state before:
pp: κ : Type uκ
R : Type uR
M : Type uM
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis κ R M
x✝ : κ
⊢ (⇑(((lift R) (Finsupp.linearCombination R (FreeAlgebra.ι R) ∘ₗ ↑b.repr)).comp ((FreeAlgebra.lift R) (⇑(ι R) ∘ ⇑b))) ∘
        FreeAlgebra.ι R)
      x✝ =
    (⇑(AlgHom.id R (FreeAlgebra R κ)) ∘ FreeAlgebra.ι R) x✝

Tactic:
simp

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

Goal state before:
pp: κ : Type uκ
R : Type uR
M : Type uM
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis κ R M
i : κ
⊢ ((lift ((b.constr R) MvPolynomial.X)).comp (MvPolynomial.aeval fun i ↦ (ι R M) (b i))) (MvPolynomial.X i) =
    (AlgHom.id R (MvPolynomial κ R)) (MvPolynomial.X i)

Tactic:
simp

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

Goal state before:
pp: κ : Type uκ
R : Type uR
M : Type uM
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis κ R M
i : κ
⊢ ((((FreeAlgebra.lift R) (⇑(ι R) ∘ ⇑b)).comp
            ((lift R) (Finsupp.linearCombination R (FreeAlgebra.ι R) ∘ₗ ↑b.repr))).toLinearMap ∘ₗ
        ι R)
      (b i) =
    ((AlgHom.id R (TensorAlgebra R M)).toLinearMap ∘ₗ ι R) (b i)

Tactic:
simp

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

Goal state before:
pp: κ : Type uκ
R : Type uR
M : Type uM
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis κ R M
i : κ
⊢ (↑((MvPolynomial.aeval fun i ↦ (ι R M) (b i)).comp (lift ((b.constr R) MvPolynomial.X))) ∘ₗ ι R M) (b i) =
    (↑(AlgHom.id R (SymmetricAlgebra R M)) ∘ₗ ι R M) (b i)

Tactic:
simp

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

Goal state before:
pp: κ : Type uκ
R : Type uR
M : Type uM
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis κ R M
i : κ
⊢ (Finsupp.linearCombination R (FreeAlgebra.ι R) ∘ₗ ↑b.repr) (b i) = FreeAlgebra.ι R i

Tactic:
simp

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

Goal state before:
pp: κ : Type uκ
R : Type uR
M : Type uM
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis κ R M
i : κ
⊢ ((b.constr R) MvPolynomial.X) (b i) = MvPolynomial.X i

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.SymmetricAlgebra.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x✝ : M
⊢ (ι R M) x✝ = (↑(AlgHom.id R (SymmetricAlgebra R M)) ∘ₗ ι R M) x✝

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.SymmetricAlgebra.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_3
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
f : M →ₗ[R] A
h : IsSymmetricAlgebra f
a : M
⊢ h.equiv (h.equiv.symm (f a)) = h.equiv ((SymmetricAlgebra.ι R M) a)

Tactic:
simp

Goal state after:
Module: Mathlib.Logic.Godel.GodelBetaFunction

Goal state before:
pp: m : ℕ
a : Fin m → ℕ
i : Fin m
⊢ i ∈ Finset.univ

Tactic:
simp

Goal state after:
Module: Mathlib.Logic.Godel.GodelBetaFunction

Goal state before:
pp: l : List ℕ
i : Fin l.length
⊢ i ∈ Finset.univ

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.Transvection.Generation

Goal state before:
pp: K : Type u_1
inst✝³ : DivisionRing K
V : Type u_2
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Module.Finite K V
e f : V ≃ₗ[K] V
hf : f ∈ dilatransvections K V
⊢ e = f⁻¹ * (f * e)

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.Transvection.Generation

Goal state before:
pp: K : Type u_1
inst✝³ : DivisionRing K
V : Type u_2
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Module.Finite K V
e f : V ≃ₗ[K] V
hf : f ∈ dilatransvections K V
⊢ e = e * f * f⁻¹

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.Transvection.Generation

Goal state before:
pp: K : Type u_1
inst✝³ : DivisionRing K
V : Type u_2
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Module.Finite K V
e f✝ : V ≃ₗ[K] V
f : Dual K V
u : V
hf : (↑e).fixedSubmodule ⊔ K ∙ (e u - u) ≤ ker f
⊢ -1 • (e u - u) = u - e u

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.Transvection.Generation

Goal state before:
pp: case hfv'
K : Type u_1
inst✝³ : DivisionRing K
V : Type u_2
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Module.Finite K V
e : V ≃ₗ[K] V
f : Dual K V
u : V
hf : (↑e).fixedSubmodule ⊔ K ∙ (e u - u) ≤ ker f
hfu : f u = 1
⊢ e u - u ∈ K ∙ (e u - u)

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.Transvection.Generation

Goal state before:
pp: K : Type u_1
inst✝³ : DivisionRing K
V : Type u_2
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Module.Finite K V
W : Submodule K V
v : V
hW : 1 < finrank K (V ⧸ W)
htop : W ⊔ K ∙ v = ⊤
h1 : finrank K (V ⧸ W) + finrank K ↥W = finrank K V
⊢ {v}.toFinset.card ≤ 1

Tactic:
simp

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.Projective

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : ↥J) → α ↑j)
h : IsEmpty ((i : ι) → α i)
hP : IsProjectiveMeasureFamily P
I : Finset ι
i : ι
hi : IsEmpty (α i)
this : IsEmpty ((j : ↥(insert i I)) → α ↑j)
⊢ Measure.map (Finset.restrict₂ ⋯) 0 = 0

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.Transvection.Generation

Goal state before:
pp: K : Type u_1
inst✝³ : DivisionRing K
V : Type u_2
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Module.Finite K V
n✝ : ℕ
e : V ≃ₗ[K] V
he : e.fixedReduce = 1
n : ℕ
h : finrank K (V ⧸ (↑e).fixedSubmodule) = n + 2
hind :
  ∀ {e : V ≃ₗ[K] V},
    e.fixedReduce = 1 → finrank K (V ⧸ (↑e).fixedSubmodule) = n + 1 → e ∈ transvections K V ^ n * dilatransvections K V
f : Dual K V
v : V
hf : (↑e).fixedSubmodule ≤ ker f
hv : f v = 1
hv_notMem : v ∉ (↑e).fixedSubmodule
hv' : v - e v ∈ (↑e).fixedSubmodule
t : V ≃ₗ[K] V := auxTransvection ⋯
ht : t = auxTransvection ⋯
⊢ t⁻¹ * (t * e) = e

Tactic:
simp

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.Cylinders

Goal state before:
pp: case a
ι : Type u_2
α : ι → Type u_1
inst✝ : (i : ι) → MeasurableSpace (α i)
s : Finset ι
t : (i : ι) → Set (α i)
h : ∀ (i : ι), MeasurableSet (t i)
⊢ (↑s).pi t ∈ {t | MeasurableSet t}

Tactic:
exact MeasurableSet.pi (Finset.countable_toSet _) (fun i _ ↦ h i)

Goal state after: