mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple

Goal state before:
pp: case pos.inl
ι : 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)
n : ℕ
k : ι
x : ℕ
hk₁ : P.root k = P.root j + n • P.root ↑i
hk₂ : (e i ^ n).col (Sum.inr j) = x • Pi.single (Sum.inr k) 1
hki : k ≠ -↑i
l : ι
hl : P.root l = P.root j + (n + 1) • P.root ↑i
m : ↥b.support
⊢ (x • e i *ᵥ Pi.single (Sum.inr k) 1) (Sum.inl m) =
    ((x * (chainBotCoeff (↑i) k + 1)) • Pi.single (Sum.inr l) 1) (Sum.inl m)

pp: case pos.inr
ι : 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)
n : ℕ
k : ι
x : ℕ
hk₁ : P.root k = P.root j + n • P.root ↑i
hk₂ : (e i ^ n).col (Sum.inr j) = x • Pi.single (Sum.inr k) 1
hki : k ≠ -↑i
l : ι
hl : P.root l = P.root j + (n + 1) • P.root ↑i
m : ι
⊢ (x • e i *ᵥ Pi.single (Sum.inr k) 1) (Sum.inr m) =
    ((x * (chainBotCoeff (↑i) k + 1)) • Pi.single (Sum.inr l) 1) (Sum.inr m)

Tactic:
· simp [e, -indexNeg_neg, hki]

Goal state after:
case pos.inr
ι : 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)
n : ℕ
k : ι
x : ℕ
hk₁ : P.root k = P.root j + n • P.root ↑i
hk₂ : (e i ^ n).col (Sum.inr j) = x • Pi.single (Sum.inr k) 1
hki : k ≠ -↑i
l : ι
hl : P.root l = P.root j + (n + 1) • P.root ↑i
m : ι
⊢ (x • e i *ᵥ Pi.single (Sum.inr k) 1) (Sum.inr m) =
    ((x * (chainBotCoeff (↑i) k + 1)) • Pi.single (Sum.inr l) 1) (Sum.inr m)
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)
n : ℕ
k : ι
x : ℕ
hk₁ : P.root k = P.root j + n • P.root ↑i
hk₂ : (e i ^ n).col (Sum.inr j) = x • Pi.single (Sum.inr k) 1
hki : k ≠ -↑i
m : ι
hl : P.root m = P.root j + (n + 1) • P.root ↑i
⊢ P.root m = P.root ↑i + P.root k

Tactic:
rw [hl, hk₁]

Goal state after:
ι : 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)
n : ℕ
k : ι
x : ℕ
hk₁ : P.root k = P.root j + n • P.root ↑i
hk₂ : (e i ^ n).col (Sum.inr j) = x • Pi.single (Sum.inr k) 1
hki : k ≠ -↑i
m : ι
hl : P.root m = P.root j + (n + 1) • P.root ↑i
⊢ P.root j + (n + 1) • P.root ↑i = P.root ↑i + (P.root j + n • P.root ↑i)
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic

Goal state before:
pp: case mem.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✝⁴ : Finite ι
inst✝³ : IsDomain R
inst✝² : CharZero R
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
x : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R
i : ↥b.support
hu : h i ∈ range h ∪ range e ∪ range f
⊢ (ωConj b) (h i) ∈ lieAlgebra b

pp: case mem.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✝⁴ : Finite ι
inst✝³ : IsDomain R
inst✝² : CharZero R
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
x : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R
i : ↥b.support
hu : e i ∈ range h ∪ range e ∪ range f
⊢ (ωConj b) (e i) ∈ lieAlgebra b

pp: case mem.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✝⁴ : Finite ι
inst✝³ : IsDomain R
inst✝² : CharZero R
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
x : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R
i : ↥b.support
hu : f i ∈ range h ∪ range e ∪ range f
⊢ (ωConj b) (f i) ∈ lieAlgebra b

Tactic:
· rw [← neg_mem_iff]
      exact LieSubalgebra.subset_lieSpan <| by simp [ω_mul_h, mul_assoc]

Goal state after:
case mem.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✝⁴ : Finite ι
inst✝³ : IsDomain R
inst✝² : CharZero R
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
x : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R
i : ↥b.support
hu : e i ∈ range h ∪ range e ∪ range f
⊢ (ωConj b) (e i) ∈ lieAlgebra b

case mem.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✝⁴ : Finite ι
inst✝³ : IsDomain R
inst✝² : CharZero R
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
x : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R
i : ↥b.support
hu : f i ∈ range h ∪ range e ∪ range f
⊢ (ωConj b) (f i) ∈ lieAlgebra b
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple

Goal state before:
pp: case neg.inl
ι : 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)
n : ℕ
k : ι
x : ℕ
hk₁ : P.root k = P.root j + n • P.root ↑i
hk₂ : (e i ^ n).col (Sum.inr j) = x • Pi.single (Sum.inr k) 1
hki : k ≠ -↑i
hij : P.root j + (n + 1) • P.root ↑i ∉ range ⇑P.root
l : ↥b.support
⊢ (x • e i *ᵥ Pi.single (Sum.inr k) 1) (Sum.inl l) = 0 (Sum.inl l)

pp: case neg.inr
ι : 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)
n : ℕ
k : ι
x : ℕ
hk₁ : P.root k = P.root j + n • P.root ↑i
hk₂ : (e i ^ n).col (Sum.inr j) = x • Pi.single (Sum.inr k) 1
hki : k ≠ -↑i
hij : P.root j + (n + 1) • P.root ↑i ∉ range ⇑P.root
l : ι
⊢ (x • e i *ᵥ Pi.single (Sum.inr k) 1) (Sum.inr l) = 0 (Sum.inr l)

Tactic:
· simp [e, -indexNeg_neg, hki]

Goal state after:
case neg.inr
ι : 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)
n : ℕ
k : ι
x : ℕ
hk₁ : P.root k = P.root j + n • P.root ↑i
hk₂ : (e i ^ n).col (Sum.inr j) = x • Pi.single (Sum.inr k) 1
hki : k ≠ -↑i
hij : P.root j + (n + 1) • P.root ↑i ∉ range ⇑P.root
l : ι
⊢ (x • e i *ᵥ Pi.single (Sum.inr k) 1) (Sum.inr l) = 0 (Sum.inr l)
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Relations

Goal state before:
pp: case inr.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 j : ↥b.support
k : ι
l : ↥b.support
⊢ ⁅h j, e i⁆ (Sum.inr k) (Sum.inl l) = (b.cartanMatrix i j • e i) (Sum.inr k) (Sum.inl l)

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
k l : ι
⊢ ⁅h j, e i⁆ (Sum.inr k) (Sum.inr l) = (b.cartanMatrix i j • e i) (Sum.inr k) (Sum.inr l)

Tactic:
· simp only [h, e]
    aesop

Goal state after:
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
k l : ι
⊢ ⁅h j, e i⁆ (Sum.inr k) (Sum.inr l) = (b.cartanMatrix i j • e i) (Sum.inr k) (Sum.inr l)
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Relations

Goal state before:
pp: case calc_2
ι : 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
⊢ -(b.cartanMatrix i j • e i) * ω b = ω b * -b.cartanMatrix i j • f i

Tactic:
· rw [Matrix.mul_smul, ω_mul_f]
    simp [mul_assoc]

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
χ : ↥H → K
hχ : χ ≠ 0
⊢ ∀ {w : ↥b.support ⊕ ι → K}, w ≠ 0 → w ∈ genWeightSpace (↥b.support ⊕ ι → K) χ → ∃ i t, t • w = v b i

Tactic:
intro w hw₀ hw

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.IsRootSystem
inst✝ : P.IsCrystallographic
b : P.Base
χ : ↥H → K
hχ : χ ≠ 0
w : ↥b.support ⊕ ι → K
hw₀ : w ≠ 0
hw : w ∈ genWeightSpace (↥b.support ⊕ ι → K) χ
⊢ ∃ i t, t • w = v b i
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Relations

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✝¹⁰ : 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
this✝¹ : InvolutiveNeg ι := P.indexNeg
this✝ : Module.IsReflexive R M
this : IsAddTorsionFree M
l : ι
hki : -↑i ≠ ↑i
⊢ ⁅e i, f i⁆ (Sum.inr (-↑i)) (Sum.inr l) = h i (Sum.inr (-↑i)) (Sum.inr l)

Tactic:
have hx (x : ι) : ¬ (P.root x = P.root l - P.root i ∧ P.root (-i) = P.root i + P.root x) := by
        rintro ⟨-, contra⟩
        refine P.nsmul_notMem_range_root (n := 2) (i := -i) ⟨x, ?_⟩
        replace contra : P.root x = -(P.root i + P.root i) := by
          simpa [neg_eq_iff_add_eq_zero, ← add_assoc, add_eq_zero_iff_eq_neg'] using contra
        simp [contra, two_smul]
      have aux (x : ι) : ¬ P.root (-i) = P.root x - P.root i := by
        simp [P.ne_zero x, eq_comm]
      simp only [e, f, h, Ring.lie_def, Matrix.sub_apply, Matrix.mul_apply, Fintype.sum_sum_type,
        Matrix.fromBlocks_apply₂₁, Matrix.of_apply, hki, reduceIte, zero_mul, Finset.sum_const_zero,
        Matrix.fromBlocks_apply₂₂, mul_ite, ite_mul, mul_zero, ← ite_and, if_neg (hx _), add_zero,
        aux, zero_sub, Matrix.diagonal_apply]
      rw [Finset.sum_eq_single_of_mem i (Finset.mem_univ _) (by aesop)]
      simp [eq_comm, apply_ite ((-·) : R → R)]

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
U : LieSubmodule K (↥H) (↥b.support ⊕ ι → K)
hU : ∀ (χ : ↥H → K), χ ≠ 0 → genWeightSpace (↥U) χ = ⊥
⊢ U ≤ genWeightSpace (↥b.support ⊕ ι → K) 0

Tactic:
refine le_trans ?_ (map_genWeightSpace_le (f := U.incl))

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.IsRootSystem
inst✝ : P.IsCrystallographic
b : P.Base
U : LieSubmodule K (↥H) (↥b.support ⊕ ι → K)
hU : ∀ (χ : ↥H → K), χ ≠ 0 → genWeightSpace (↥U) χ = ⊥
⊢ U ≤ LieSubmodule.map U.incl (genWeightSpace (↥U) 0)
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
U : LieSubmodule K (↥H) (↥b.support ⊕ ι → K)
hU : ∀ (χ : ↥H → K), χ ≠ 0 → genWeightSpace (↥U) χ = ⊥
this : ⨆ χ, ⨆ (_ : χ ≠ 0), ⊥ = ⊥
⊢ genWeightSpace (↥U) 0 = ⨆ χ, genWeightSpace (↥U) χ

Tactic:
iSup_split_single _ 0,

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.IsRootSystem
inst✝ : P.IsCrystallographic
b : P.Base
U : LieSubmodule K (↥H) (↥b.support ⊕ ι → K)
hU : ∀ (χ : ↥H → K), χ ≠ 0 → genWeightSpace (↥U) χ = ⊥
this : ⨆ χ, ⨆ (_ : χ ≠ 0), ⊥ = ⊥
⊢ genWeightSpace (↥U) 0 = genWeightSpace (↥U) 0 ⊔ ⨆ i, ⨆ (_ : i ≠ 0), genWeightSpace (↥U) i
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}
hxy : IsReflective.coroot B ⋯ = IsReflective.coroot B ⋯
h1 : ∀ (z : M), (IsReflective.coroot B ⋯) z = (IsReflective.coroot B ⋯) z
h2x : 2 * (B ↑x) ↑y = (B ↑x) ↑x * (IsReflective.coroot B ⋯) ↑y
h2y : ∀ (z : M), (B ↑y) ↑y * (IsReflective.coroot B ⋯) z = 2 * (B ↑y) z
⊢ 2 * (B ↑x) ↑x = 2 * (B ↑y) ↑y

Tactic:
coroot_apply_self

Goal state after:
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}
hxy : IsReflective.coroot B ⋯ = IsReflective.coroot B ⋯
h1 : ∀ (z : M), (IsReflective.coroot B ⋯) z = (IsReflective.coroot B ⋯) z
h2x : 2 * (B ↑x) ↑y = (B ↑x) ↑x * 2
h2y : ∀ (z : M), (B ↑y) ↑y * (IsReflective.coroot B ⋯) z = 2 * (B ↑y) z
⊢ 2 * (B ↑x) ↑x = 2 * (B ↑y) ↑y
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}
hxy : IsReflective.coroot B ⋯ = IsReflective.coroot B ⋯
h1 : ∀ (z : M), (IsReflective.coroot B ⋯) z = (IsReflective.coroot B ⋯) z
h2x : 2 * (B ↑x) ↑y = (B ↑x) ↑x * 2
h2y : (B ↑y) ↑y * (IsReflective.coroot B ⋯) ↑x = 2 * (B ↑y) ↑x
⊢ 2 * (B ↑x) ↑x = 2 * (B ↑y) ↑y

Tactic:
coroot_apply_self

Goal state after:
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}
hxy : IsReflective.coroot B ⋯ = IsReflective.coroot B ⋯
h1 : ∀ (z : M), (IsReflective.coroot B ⋯) z = (IsReflective.coroot B ⋯) z
h2x : 2 * (B ↑x) ↑y = (B ↑x) ↑x * 2
h2y : (B ↑y) ↑y * 2 = 2 * (B ↑y) ↑x
⊢ 2 * (B ↑x) ↑x = 2 * (B ↑y) ↑y
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
contra : ¬∑ k, c k * ↑|b.cartanMatrix j k| = 0
aux : ∀ (k : ↥b.support), ⁅e j, u k⁆ = |b.cartanMatrix j k| • v b ↑j
this : ∑ i, ⁅e j, c i • u i⁆ ∈ U
⊢ v b ↑j ∈ U

Tactic:
lie_smul,

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.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
contra : ¬∑ k, c k * ↑|b.cartanMatrix j k| = 0
aux : ∀ (k : ↥b.support), ⁅e j, u k⁆ = |b.cartanMatrix j k| • v b ↑j
this : ∑ x, c x • ⁅e j, u x⁆ ∈ U
⊢ v b ↑j ∈ U
Module: Mathlib.LinearAlgebra.TensorPower.Symmetric

Goal state before:
pp: case add
R ι : Type u
inst✝² : CommSemiring R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
x y w✝ x✝ y✝ z✝ : ⨂[R] (x : ι), M
a✝¹ : AddConGen.Rel (Rel R ι M) w✝ x✝
a✝ : AddConGen.Rel (Rel R ι M) y✝ z✝
a_ih✝¹ : (addConGen (Rel R ι M)) (r • w✝) (r • x✝)
a_ih✝ : (addConGen (Rel R ι M)) (r • y✝) (r • z✝)
⊢ (addConGen (Rel R ι M)) (r • (w✝ + y✝)) (r • (x✝ + z✝))

Tactic:
rw [smul_add, smul_add]

Goal state after:
case add
R ι : Type u
inst✝² : CommSemiring R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
x y w✝ x✝ y✝ z✝ : ⨂[R] (x : ι), M
a✝¹ : AddConGen.Rel (Rel R ι M) w✝ x✝
a✝ : AddConGen.Rel (Rel R ι M) y✝ z✝
a_ih✝¹ : (addConGen (Rel R ι M)) (r • w✝) (r • x✝)
a_ih✝ : (addConGen (Rel R ι M)) (r • y✝) (r • z✝)
⊢ (addConGen (Rel R ι M)) (r • w✝ + r • y✝) (r • x✝ + r • z✝)
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
⊢ u - e u ∈ (↑e).fixedSubmodule ⊔ K ∙ (e u - u)

Tactic:
apply Submodule.mem_sup_right

Goal state after:
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
⊢ u - e u ∈ K ∙ (e u - u)
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
u : V
hu : u ∉ (↑e).fixedSubmodule
f : Dual K V
hfu : f u ≠ 0
hf : map f (↑e).fixedSubmodule = ⊥
v : V := (f u)⁻¹ • u
⊢ f v = 1

Tactic:
simp [v, inv_mul_cancel₀ hfu]

Goal state after:
Module: Mathlib.MeasureTheory.SetSemiring

Goal state before:
pp: α : Type u_1
C : Set (Set α)
j : Set α
J : Finset (Set α)
hC : IsSetSemiring C
hJ : ↑J ⊆ C
hj : j ∈ J
⊢ ↑(hC.disjointOfUnion hJ j) ⊆ C

Tactic:
by
  lift j to J using hj
  rw [hC.disjointOfUnion_coe hJ]
  exact (hC.exists_partition_disjointed hJ j).choose_spec

Goal state after:
Module: Mathlib.Topology.Order.WithTop

Goal state before:
pp: case inr.a
ι : Type u_1
inst✝¹ : Preorder ι
ts : TopologicalSpace ι
ht : OrderTopology ι
inst✝ : SecondCountableTopology ι
x₀ : ι
c : Set ι
c_count : c.Countable
hc : ts = generateFrom {s | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}
c' : Set ι
c'_count : c'.Countable
hc' : Dense c'
x₁ : ι := ⋯
d : Set (WithTop ι) := ⋯
⊢ instWithTopOfOrderTopology ≤ generateFrom {s | ∃ a ∈ d, s = Ioi a ∨ s = Iio a}

pp: case a
ι : Type u_1
inst✝¹ : Preorder ι
ts : TopologicalSpace ι
ht : OrderTopology ι
inst✝ : SecondCountableTopology ι
x₀ : ι
c : Set ι
c_count : c.Countable
hc : ts = generateFrom {s | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}
c' : Set ι
c'_count : c'.Countable
hc' : Dense c'
x₁ : ι := ⋯
d : Set (WithTop ι) := ⋯
⊢ generateFrom {s | ∃ a ∈ d, s = Ioi a ∨ s = Iio a} ≤ instWithTopOfOrderTopology

Tactic:
· apply le_generateFrom_iff_subset_isOpen.2
    grind [isOpen_Iio', isOpen_Ioi']

Goal state after:
case a
ι : Type u_1
inst✝¹ : Preorder ι
ts : TopologicalSpace ι
ht : OrderTopology ι
inst✝ : SecondCountableTopology ι
x₀ : ι
c : Set ι
c_count : c.Countable
hc : ts = generateFrom {s | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}
c' : Set ι
c'_count : c'.Countable
hc' : Dense c'
x₁ : ι := ⋯
d : Set (WithTop ι) := ⋯
⊢ generateFrom {s | ∃ a ∈ d, s = Ioi a ∨ s = Iio a} ≤ instWithTopOfOrderTopology