mathlib-initiative/mathlib-tactics huggingface dataset:
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 ι
i j : ↥b.support
k : ι
⊢ h i (Sum.inl j) (Sum.inr k) = Matrix.diagonal (0 ⊕ᵥ fun x ↦ ↑(P.pairingIn ℤ x ↑i)) (Sum.inl j) (Sum.inr k)

Tactic:
simp [h, Matrix.diagonal_apply]

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 ι
i : ↥b.support
j : ι
k : ↥b.support
⊢ h i (Sum.inr j) (Sum.inl k) = Matrix.diagonal (0 ⊕ᵥ fun x ↦ ↑(P.pairingIn ℤ x ↑i)) (Sum.inr j) (Sum.inl k)

Tactic:
simp [h, Matrix.diagonal_apply]

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 ι
i : ↥b.support
j k : ι
⊢ h i (Sum.inr j) (Sum.inr k) = Matrix.diagonal (0 ⊕ᵥ fun x ↦ ↑(P.pairingIn ℤ x ↑i)) (Sum.inr j) (Sum.inr k)

Tactic:
simp [h, Matrix.diagonal_apply]

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 : ι
hij : i ≠ j
hi : i ∈ b.support
hj : j ∈ b.support
l : ι
hli : l ≠ i
hkj : l ≠ j
hk' : P.root l + P.root i ∈ range ⇑P.root
hm : P.pairingIn ℤ j l ≤ 0
hl : P.root l = P.root l + P.root i - P.root j
⊢ i = j

Tactic:
simpa [add_sub_assoc, sub_eq_zero] using hl

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
⊢ P.pairing k i = -1

Tactic:
← P.algebraMap_pairingIn ℤ,

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 : ι
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) (P.pairingIn ℤ k i) = -1
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic

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.IsCrystallographic
b : P.Base
inst✝⁴ : Finite ι
inst✝³ : IsDomain R
inst✝² : CharZero R
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
i j : ι
k : ↥b.support
h : P.root i = P.root j + P.root ↑k
l : ↥b.support
⊢ ⁅f k, v b i⁆ (Sum.inl l) = ((↑(chainTopCoeff (↑k) i) + 1) • v b j) (Sum.inl l)

Tactic:
replace h : i ≠ k := by rintro rfl; exact P.ne_zero j <| by simpa using h
    simp [f, h]

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
inst✝ : P.IsG2
i j : ι
h : P.root i ≠ P.root j
h' : P.root i ≠ -P.root j
this :
  ¬∀ (i j : ι),
      P.pairingIn ℤ i j = P.pairingIn ℤ j i ∨
        P.pairingIn ℤ i j = 2 * P.pairingIn ℤ j i ∨ P.pairingIn ℤ j i = 2 * P.pairingIn ℤ i j
aux₁ :
  P.pairingIn ℤ i j = P.pairingIn ℤ j i ∨
    P.pairingIn ℤ i j = 3 * P.pairingIn ℤ j i ∨ P.pairingIn ℤ j i = 3 * P.pairingIn ℤ i j
aux₂ :
  (P.pairingIn ℤ i j, P.pairingIn ℤ j 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 ℤ i j ∈ {-3, -1, 0, 1, 3}

Tactic:
simp only [mem_insert_iff, mem_singleton_iff, Prod.mk_zero_zero, Prod.mk_eq_zero,
      Prod.mk_one_one, Prod.mk_eq_one, Prod.mk.injEq] at aux₂ ⊢

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
inst✝ : P.IsG2
i j : ι
h : P.root i ≠ P.root j
h' : P.root i ≠ -P.root j
this :
  ¬∀ (i j : ι),
      P.pairingIn ℤ i j = P.pairingIn ℤ j i ∨
        P.pairingIn ℤ i j = 2 * P.pairingIn ℤ j i ∨ P.pairingIn ℤ j i = 2 * P.pairingIn ℤ i j
aux₁ :
  P.pairingIn ℤ i j = P.pairingIn ℤ j i ∨
    P.pairingIn ℤ i j = 3 * P.pairingIn ℤ j i ∨ P.pairingIn ℤ j i = 3 * P.pairingIn ℤ i j
aux₂ :
  P.pairingIn ℤ i j = 0 ∧ P.pairingIn ℤ j i = 0 ∨
    P.pairingIn ℤ i j = 1 ∧ P.pairingIn ℤ j i = 1 ∨
      P.pairingIn ℤ i j = -1 ∧ P.pairingIn ℤ j i = -1 ∨
        P.pairingIn ℤ i j = 1 ∧ P.pairingIn ℤ j i = 2 ∨
          P.pairingIn ℤ i j = 2 ∧ P.pairingIn ℤ j i = 1 ∨
            P.pairingIn ℤ i j = -1 ∧ P.pairingIn ℤ j i = -2 ∨
              P.pairingIn ℤ i j = -2 ∧ P.pairingIn ℤ j i = -1 ∨
                P.pairingIn ℤ i j = 1 ∧ P.pairingIn ℤ j i = 3 ∨
                  P.pairingIn ℤ i j = 3 ∧ P.pairingIn ℤ j i = 1 ∨
                    P.pairingIn ℤ i j = -1 ∧ P.pairingIn ℤ j i = -3 ∨ P.pairingIn ℤ i j = -3 ∧ P.pairingIn ℤ j i = -1
⊢ P.pairingIn ℤ i j = -3 ∨
    P.pairingIn ℤ i j = -1 ∨ P.pairingIn ℤ i j = 0 ∨ P.pairingIn ℤ i j = 1 ∨ P.pairingIn ℤ i j = 3
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
⊢ P.pairing (long P) (short P) = -3

Tactic:
← P.algebraMap_pairingIn ℤ,

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.EmbeddedG2
⊢ (algebraMap ℤ R) (P.pairingIn ℤ (long P) (short P)) = -3
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
⊢ P.pairing (short P) (long P) = -1

Tactic:
← P.algebraMap_pairingIn ℤ,

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.EmbeddedG2
inst✝² : Finite ι
inst✝¹ : CharZero R
inst✝ : IsDomain R
⊢ (algebraMap ℤ R) (P.pairingIn ℤ (short P) (long P)) = -1
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple

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✝⁹ : 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
this✝¹ : Module.IsReflexive R M
this✝ : IsAddTorsionFree M
this : InvolutiveNeg ι := P.indexNeg
case_inl : ∀ (j : ↥b.support), (e i ^ 2).col (Sum.inl j) = 0
j : ι
hij : (e i).col (Sum.inr j) = u i
⊢ (e i ^ (2 + 1)).col (Sum.inr j) = 0

Tactic:
rw [pow_succ, ← Matrix.mulVec_single_one, ← Matrix.mulVec_mulVec]

Goal state after:
case h
ι : 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
this✝¹ : Module.IsReflexive R M
this✝ : IsAddTorsionFree M
this : InvolutiveNeg ι := P.indexNeg
case_inl : ∀ (j : ↥b.support), (e i ^ 2).col (Sum.inl j) = 0
j : ι
hij : (e i).col (Sum.inr j) = u i
⊢ e i ^ 2 *ᵥ e i *ᵥ Pi.single (Sum.inr j) 1 = 0
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
hki : P.pairingIn ℤ k i = 0
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✝¹ : P.IsNotG2
this✝ : InvolutiveNeg ι := P.indexNeg
this : IsAddTorsionFree M
n : ι
hn : P.root n = P.root k + P.root i - P.root j
hnk_ne : n ≠ k
hkj_ne : k ≠ j ∧ P.root k ≠ -P.root j
hnk_notMem : P.root n - P.root k ∉ range ⇑P.root
⊢ P.pairing k i = 0

Tactic:
← P.algebraMap_pairingIn ℤ,

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
hki : P.pairingIn ℤ k i = 0
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✝¹ : P.IsNotG2
this✝ : InvolutiveNeg ι := P.indexNeg
this : IsAddTorsionFree M
n : ι
hn : P.root n = P.root k + P.root i - P.root j
hnk_ne : n ≠ k
hkj_ne : k ≠ j ∧ P.root k ≠ -P.root j
hnk_notMem : P.root n - P.root k ∉ range ⇑P.root
⊢ (algebraMap ℤ R) (P.pairingIn ℤ k i) = 0
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
hki : P.pairingIn ℤ k i = 0
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✝¹ : P.IsNotG2
this✝ : InvolutiveNeg ι := P.indexNeg
this : IsAddTorsionFree M
n : ι
hn : P.root n = P.root k + P.root i - P.root j
hnk_ne : n ≠ k
hkj_ne : k ≠ j ∧ P.root k ≠ -P.root j
hnk_notMem : P.root n - P.root k ∉ range ⇑P.root
aux₀ : P.pairingIn ℤ j i = -P.pairingIn ℤ m i
aux₁ : P.pairingIn ℤ j i = 0
key₁ : P.pairingIn ℤ i k = 0
key₂ : P.pairingIn ℤ i m = 0
key₃ : P.pairingIn ℤ j k = 2
⊢ P.pairing j i = 0

Tactic:
← P.algebraMap_pairingIn ℤ,

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
hki : P.pairingIn ℤ k i = 0
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✝¹ : P.IsNotG2
this✝ : InvolutiveNeg ι := P.indexNeg
this : IsAddTorsionFree M
n : ι
hn : P.root n = P.root k + P.root i - P.root j
hnk_ne : n ≠ k
hkj_ne : k ≠ j ∧ P.root k ≠ -P.root j
hnk_notMem : P.root n - P.root k ∉ range ⇑P.root
aux₀ : P.pairingIn ℤ j i = -P.pairingIn ℤ m i
aux₁ : P.pairingIn ℤ j i = 0
key₁ : P.pairingIn ℤ i k = 0
key₂ : P.pairingIn ℤ i m = 0
key₃ : P.pairingIn ℤ j k = 2
⊢ (algebraMap ℤ R) (P.pairingIn ℤ j i) = 0
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 : ↥b.support
inst✝ : P.IsReduced
this✝¹ : InvolutiveNeg ι := P.indexNeg
this✝ : Module.IsReflexive R M
this : IsAddTorsionFree M
k l : ι
⊢ ⁅e i, f i⁆ (Sum.inr k) (Sum.inr l) = h i (Sum.inr k) (Sum.inr l)

Tactic:
· rcases eq_or_ne k i with rfl | hki
    · have hx (x : ι) : ¬ (P.root x = P.root i + P.root l ∧ P.root i = P.root x - P.root i) := by
        rintro ⟨-, contra⟩
        refine P.nsmul_notMem_range_root (n := 2) (i := i) ⟨x, ?_⟩
        rwa [eq_sub_iff_add_eq, ← two_smul ℕ, eq_comm] at contra
      simp only [e, f, h, P.ne_zero, P.ne_neg, Ring.lie_def, Fintype.sum_sum_type, Matrix.sub_apply,
        Matrix.mul_apply, Matrix.fromBlocks_apply₂₁, Matrix.of_apply, Matrix.fromBlocks_apply₂₂,
        left_eq_add, zero_mul, mul_zero, ite_mul, mul_ite, ← ite_and]
      rw [Finset.sum_eq_single_of_mem i (Finset.mem_univ _) (by aesop)]
      simp [hx, eq_comm]
    rcases eq_or_ne k (-i) with rfl | hki'
    · 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)]
    rcases eq_or_ne k l with rfl | hkl
    · exact lie_e_f_same_aux i k hki hki'
    · simp_all [h, e, f]

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' : Type u_4
inst✝¹ : CommSemiring A'
inst✝ : Algebra R A'
g : M →ₗ[R] A'
a : M
⊢ (h.lift g) (f a) = g a

Tactic:
by simp [lift]

Goal state after:
Module: Mathlib.LinearAlgebra.TensorPower.Symmetric

Goal state before:
pp: R ι : Type u
inst✝² : CommSemiring R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ Submodule.span R (Set.range ⇑((mk R ι M).compMultilinearMap (PiTensorProduct.tprod R))) = ⊤

Tactic:
LinearMap.coe_compMultilinearMap,

Goal state after:
R ι : Type u
inst✝² : CommSemiring R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ Submodule.span R (Set.range (⇑(mk R ι M) ∘ ⇑(PiTensorProduct.tprod R))) = ⊤
Module: Mathlib.MeasureTheory.Category.MeasCat

Goal state before:
pp: μ : MeasureTheory.Measure (MeasureTheory.Measure ℝ≥0∞)
⊢ ∫⁻ (x : ℝ≥0∞), x ∂μ.join = ∫⁻ (x : ℝ≥0∞), x ∂Measure.map (fun m ↦ ∫⁻ (x : ℝ≥0∞), x ∂m) μ

Tactic:
rw [Measure.lintegral_join, lintegral_map] <;>
        apply_rules [Measurable.aemeasurable, measurable_id, Measure.measurable_lintegral]

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
s : Set ((i : ι) → α i)
hs : s ∈ measurableCylinders α
⊢ sᶜ ∈ measurableCylinders α

Tactic:
rw [mem_measurableCylinders] at hs ⊢

Goal state after:
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
s : Set ((i : ι) → α i)
hs : ∃ s_1 S, MeasurableSet S ∧ s = cylinder s_1 S
⊢ ∃ s_1 S, MeasurableSet S ∧ sᶜ = cylinder s_1 S
Module: Mathlib.MeasureTheory.Constructions.Cylinders

Goal state before:
pp: case a
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
i : ι
t : (i : ι) → Set (α i)
ht : ∀ (i : ι), MeasurableSet (t i)
⊢ ∃ s S, MeasurableSet S ∧ eval i ⁻¹' t i = cylinder s S

Tactic:
refine ⟨{i}, {f | f ⟨i, Finset.mem_singleton_self i⟩ ∈ t i}, measurable_pi_apply _ (ht i), ?_⟩

Goal state after:
case a
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
i : ι
t : (i : ι) → Set (α i)
ht : ∀ (i : ι), MeasurableSet (t i)
⊢ eval i ⁻¹' t i = cylinder {i} {f | f ⟨i, ⋯⟩ ∈ t i}
Module: Mathlib.MeasureTheory.SetSemiring

Goal state before:
pp: case inr.inr
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : Nonempty α
u v : α
huv : u ≤ v
u' v' : α
hu'v' : u' ≤ v'
hu : u < u'
hv : v' < v
a : Set α
ha : a ∈ ↑{Set.Ioc u u', Set.Ioc v' v}
b : Set α
hb : b ∈ ↑{Set.Ioc u u', Set.Ioc v' v}
⊢ a ≠ b → Function.onFun Disjoint id a b

Tactic:
hab

Goal state after:
case inr.inr
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : Nonempty α
u v : α
huv : u ≤ v
u' v' : α
hu'v' : u' ≤ v'
hu : u < u'
hv : v' < v
a : Set α
ha : a ∈ ↑{Set.Ioc u u', Set.Ioc v' v}
b : Set α
hb : b ∈ ↑{Set.Ioc u u', Set.Ioc v' v}
hab : a ≠ b
⊢ Function.onFun Disjoint id a b
Module: Mathlib.MeasureTheory.Measure.AddContent

Goal state before:
pp: α : Type u_1
C : Set (Set α)
G : Type u_2
inst✝ : AddCommMonoid G
m : AddContent G C
hC : IsSetSemiring C
J J' : Finset (Set α)
hJ : ↑J ⊆ C
hJdisj : (↑J).PairwiseDisjoint id
hJ' : ↑J' ⊆ C
hJ'disj : (↑J').PairwiseDisjoint id
h : ⋃₀ ↑J = ⋃₀ ↑J'
s : Set α
hs : s ∈ J
⊢ s ⊆ ⋃₀ ↑J

Tactic:
exact subset_sUnion_of_mem hs

Goal state after:
Module: Mathlib.MeasureTheory.Measure.AddContent

Goal state before:
pp: α : Type u_1
C : Set (Set α)
G : Type u_2
inst✝ : AddCommMonoid G
m : AddContent G C
hC : IsSetSemiring C
J J' : Finset (Set α)
hJ : ↑J ⊆ C
hJdisj : (↑J).PairwiseDisjoint id
hJ' : ↑J' ⊆ C
hJ'disj : (↑J').PairwiseDisjoint id
h : ⋃₀ ↑J = ⋃₀ ↑J'
t : Set α
ht : t ∈ J'
this : t = ⋃ s ∈ J, s ∩ t
⊢ t ∈ C

Tactic:
exact hJ' ht

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 : V ≃ₗ[K] V
f g : Dual K V
v : V
a b : K
hv : LinearIndependent K ![(↑e).fixedSubmodule.mkQ v, e.fixedReduce ((↑e).fixedSubmodule.mkQ v)]
hf : (↑e).fixedSubmodule ⊔ K ∙ (e v - v) ≤ ker f
hfv : f v = 1
hg : (↑e).fixedSubmodule ⊔ K ∙ (e v - v) ≤ ker (f + g)
hfgv : (f + g) v = 1
hg0 : g ≠ 0
hne_top : (↑e).fixedSubmodule ⊔ K ∙ (e v - v) ⊔ K ∙ v < ⊤
ha : ∀ (v_1 : V), (auxTransvection hf * e) v_1 - a • v_1 ∈ (↑e).fixedSubmodule ⊔ K ∙ v
hb : ∀ (v_1 : V), (auxTransvection hg * e) v_1 - b • v_1 ∈ (↑e).fixedSubmodule ⊔ K ∙ v
c : K := b - a
hc : c = b - a
key : ∀ (x : V), g (e x) • (v - e v) - c • x ∈ (↑e).fixedSubmodule ⊔ K ∙ v
hc0 : c ≠ 0
x : V
a✝ : x ∈ ⊤
h1 : g (e x) • (v - e v) ∈ K ∙ (e v - v)
hle : (↑e).fixedSubmodule ⊔ K ∙ v ≤ (↑e).fixedSubmodule ⊔ K ∙ (e v - v) ⊔ K ∙ v
⊢ c • x ∈ (↑e).fixedSubmodule ⊔ K ∙ (e v - v) ⊔ K ∙ v

Tactic:
show c • x = g (e x) • (v - e v) - (g (e x) • (v - e v) - c • x) by abel

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 : V ≃ₗ[K] V
f g : Dual K V
v : V
a b : K
hv : LinearIndependent K ![(↑e).fixedSubmodule.mkQ v, e.fixedReduce ((↑e).fixedSubmodule.mkQ v)]
hf : (↑e).fixedSubmodule ⊔ K ∙ (e v - v) ≤ ker f
hfv : f v = 1
hg : (↑e).fixedSubmodule ⊔ K ∙ (e v - v) ≤ ker (f + g)
hfgv : (f + g) v = 1
hg0 : g ≠ 0
hne_top : (↑e).fixedSubmodule ⊔ K ∙ (e v - v) ⊔ K ∙ v < ⊤
ha : ∀ (v_1 : V), (auxTransvection hf * e) v_1 - a • v_1 ∈ (↑e).fixedSubmodule ⊔ K ∙ v
hb : ∀ (v_1 : V), (auxTransvection hg * e) v_1 - b • v_1 ∈ (↑e).fixedSubmodule ⊔ K ∙ v
c : K := b - a
hc : c = b - a
key : ∀ (x : V), g (e x) • (v - e v) - c • x ∈ (↑e).fixedSubmodule ⊔ K ∙ v
hc0 : c ≠ 0
x : V
a✝ : x ∈ ⊤
h1 : g (e x) • (v - e v) ∈ K ∙ (e v - v)
hle : (↑e).fixedSubmodule ⊔ K ∙ v ≤ (↑e).fixedSubmodule ⊔ K ∙ (e v - v) ⊔ K ∙ v
⊢ g (e x) • (v - e v) - (g (e x) • (v - e v) - c • x) ∈ (↑e).fixedSubmodule ⊔ K ∙ (e v - v) ⊔ K ∙ v
Module: Mathlib.Topology.Order.WithTop

Goal state before:
pp: ι : Type u_1
inst✝² : LinearOrder ι
inst✝¹ : TopologicalSpace ι
inst✝ : OrderTopology ι
⊢ IsOpen[TopologicalSpace.instWithTopOfOrderTopology] (Iio ⊤)

Tactic:
exact isOpen_Iio

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

Goal state before:
pp: ι : Type u_1
inst✝² : LinearOrder ι
inst✝¹ : TopologicalSpace ι
inst✝ : OrderTopology ι
d a : ι
⊢ Tendsto (untopD d) (𝓝 ↑a) (𝓝 (untopD d ↑a))

Tactic:
nhds_coe,

Goal state after:
ι : Type u_1
inst✝² : LinearOrder ι
inst✝¹ : TopologicalSpace ι
inst✝ : OrderTopology ι
d a : ι
⊢ Tendsto (untopD d) (Filter.map some (𝓝 a)) (𝓝 (untopD d ↑a))
Module: Mathlib.Topology.Order.WithTop

Goal state before:
pp: ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : TopologicalSpace ι
inst✝¹ : OrderTopology ι
inst✝ : NoMaxOrder ι
⊢ Tendsto some atTop (𝓝 ⊤)

Tactic:
obtain (h | h) := isEmpty_or_nonempty ι
  · simpa using Subsingleton.elim ..
  rw [tendsto_nhds_top_iff]
  intro i
  filter_upwards [atTop_basis_Ioi.mem_of_mem (i := i) trivial]
  simp

Goal state after: