mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Lie.Derivation.BaseChange

Goal state before:
pp: case refine_2
R : Type u_1
inst✝⁴ : CommRing R
A : Type u_2
inst✝³ : CommRing A
inst✝² : Algebra R A
L : Type u_3
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x✝³ x✝² : LieDerivation R L L
z x✝¹ x✝ : A ⊗[R] L
hx :
  { toFun := ⇑(LinearMap.lTensor A ↑⁅x✝³, x✝²⁆), map_add' := ⋯, map_smul' := ⋯, leibniz' := ⋯ } x✝¹ =
    ⁅{ toFun := ⇑(LinearMap.lTensor A ↑x✝³), map_add' := ⋯, map_smul' := ⋯, leibniz' := ⋯ },
        { toFun := ⇑(LinearMap.lTensor A ↑x✝²), map_add' := ⋯, map_smul' := ⋯, leibniz' := ⋯ }⁆
      x✝¹
hy :
  { toFun := ⇑(LinearMap.lTensor A ↑⁅x✝³, x✝²⁆), map_add' := ⋯, map_smul' := ⋯, leibniz' := ⋯ } x✝ =
    ⁅{ toFun := ⇑(LinearMap.lTensor A ↑x✝³), map_add' := ⋯, map_smul' := ⋯, leibniz' := ⋯ },
        { toFun := ⇑(LinearMap.lTensor A ↑x✝²), map_add' := ⋯, map_smul' := ⋯, leibniz' := ⋯ }⁆
      x✝
⊢ { toFun := ⇑(LinearMap.lTensor A ↑⁅x✝³, x✝²⁆), map_add' := ⋯, map_smul' := ⋯, leibniz' := ⋯ } (x✝¹ + x✝) =
    ⁅{ toFun := ⇑(LinearMap.lTensor A ↑x✝³), map_add' := ⋯, map_smul' := ⋯, leibniz' := ⋯ },
        { toFun := ⇑(LinearMap.lTensor A ↑x✝²), map_add' := ⋯, map_smul' := ⋯, leibniz' := ⋯ }⁆
      (x✝¹ + x✝)

Tactic:
simp_all [sub_add_sub_comm]

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Grading

Goal state before:
pp: case refine_1
M : Type u_1
ι : Type u_2
R : Type u_3
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
i : ι
x : R[M]
hx : 0 ∈ gradeBy R (⇑f) i
⊢ (decomposeAux f) ↑⟨0, hx⟩ = (DirectSum.of (fun i ↦ ↥(gradeBy R (⇑f) i)) i) ⟨0, hx⟩

Tactic:
symm

Goal state after:
case refine_1
M : Type u_1
ι : Type u_2
R : Type u_3
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
i : ι
x : R[M]
hx : 0 ∈ gradeBy R (⇑f) i
⊢ (DirectSum.of (fun i ↦ ↥(gradeBy R (⇑f) i)) i) ⟨0, hx⟩ = (decomposeAux f) ↑⟨0, hx⟩
Module: Mathlib.Algebra.Lie.LieTheorem

Goal state before:
pp: R : Type u_1
L : Type u_2
A : Type u_3
V : Type u_4
inst✝¹⁹ : CommRing R
inst✝¹⁸ : IsPrincipalIdealRing R
inst✝¹⁷ : IsDomain R
inst✝¹⁶ : CharZero R
inst✝¹⁵ : LieRing L
inst✝¹⁴ : LieAlgebra R L
inst✝¹³ : LieRing A
inst✝¹² : LieAlgebra R A
inst✝¹¹ : Bracket L A
inst✝¹⁰ : Bracket A L
inst✝⁹ : AddCommGroup V
inst✝⁸ : Module R V
inst✝⁷ : Module.Free R V
inst✝⁶ : Module.Finite R V
inst✝⁵ : LieRingModule L V
inst✝⁴ : LieModule R L V
inst✝³ : LieRingModule A V
inst✝² : LieModule R A V
inst✝¹ : IsLieTower L A V
inst✝ : IsLieTower A L V
χ : A → R
z : L
v : V
hv : ∀ (x : A), ⁅x, v⁆ = χ x • v
a : A
hv' : v ≠ 0
U' : ℕ →o Submodule R V :=
  { toFun := fun n ↦ Submodule.span R {x | ∃ i < n, ((toEnd R L V) z ^ i) v = x}, monotone' := ⋯ }
map_U'_le : ∀ (n : ℕ), Submodule.map ((toEnd R L V) z) (U' n) ≤ U' (n + 1)
n : ℕ
hn :
  ∀ (w : A),
    ∀ a < n + 1, (T χ w) (((toEnd R L V) z ^ a) v) ∈ Submodule.span R {x | ∃ i < n, ((toEnd R L V) z ^ i) v = x}
w : A
⊢ ∀ a < n + 1 + 1, (T χ w) (((toEnd R L V) z ^ a) v) ∈ Submodule.span R {x | ∃ i < n + 1, ((toEnd R L V) z ^ i) v = x}

Tactic:
intro m hm

Goal state after:
R : Type u_1
L : Type u_2
A : Type u_3
V : Type u_4
inst✝¹⁹ : CommRing R
inst✝¹⁸ : IsPrincipalIdealRing R
inst✝¹⁷ : IsDomain R
inst✝¹⁶ : CharZero R
inst✝¹⁵ : LieRing L
inst✝¹⁴ : LieAlgebra R L
inst✝¹³ : LieRing A
inst✝¹² : LieAlgebra R A
inst✝¹¹ : Bracket L A
inst✝¹⁰ : Bracket A L
inst✝⁹ : AddCommGroup V
inst✝⁸ : Module R V
inst✝⁷ : Module.Free R V
inst✝⁶ : Module.Finite R V
inst✝⁵ : LieRingModule L V
inst✝⁴ : LieModule R L V
inst✝³ : LieRingModule A V
inst✝² : LieModule R A V
inst✝¹ : IsLieTower L A V
inst✝ : IsLieTower A L V
χ : A → R
z : L
v : V
hv : ∀ (x : A), ⁅x, v⁆ = χ x • v
a : A
hv' : v ≠ 0
U' : ℕ →o Submodule R V :=
  { toFun := fun n ↦ Submodule.span R {x | ∃ i < n, ((toEnd R L V) z ^ i) v = x}, monotone' := ⋯ }
map_U'_le : ∀ (n : ℕ), Submodule.map ((toEnd R L V) z) (U' n) ≤ U' (n + 1)
n : ℕ
hn :
  ∀ (w : A),
    ∀ a < n + 1, (T χ w) (((toEnd R L V) z ^ a) v) ∈ Submodule.span R {x | ∃ i < n, ((toEnd R L V) z ^ i) v = x}
w : A
m : ℕ
hm : m < n + 1 + 1
⊢ (T χ w) (((toEnd R L V) z ^ m) v) ∈ Submodule.span R {x | ∃ i < n + 1, ((toEnd R L V) z ^ i) v = x}
Module: Mathlib.Algebra.Lie.LieTheorem

Goal state before:
pp: case inr
R : Type u_1
L : Type u_2
A : Type u_3
V : Type u_4
inst✝¹⁹ : CommRing R
inst✝¹⁸ : IsPrincipalIdealRing R
inst✝¹⁷ : IsDomain R
inst✝¹⁶ : CharZero R
inst✝¹⁵ : LieRing L
inst✝¹⁴ : LieAlgebra R L
inst✝¹³ : LieRing A
inst✝¹² : LieAlgebra R A
inst✝¹¹ : Bracket L A
inst✝¹⁰ : Bracket A L
inst✝⁹ : AddCommGroup V
inst✝⁸ : Module R V
inst✝⁷ : Module.Free R V
inst✝⁶ : Module.Finite R V
inst✝⁵ : LieRingModule L V
inst✝⁴ : LieModule R L V
inst✝³ : LieRingModule A V
inst✝² : LieModule R A V
inst✝¹ : IsLieTower L A V
inst✝ : IsLieTower A L V
χ : A → R
z : L
v : V
hv : ∀ (x : A), ⁅x, v⁆ = χ x • v
a : A
hv' : v ≠ 0
U' : ℕ →o Submodule R V :=
  { toFun := fun n ↦ Submodule.span R {x | ∃ i < n, ((toEnd R L V) z ^ i) v = x}, monotone' := ⋯ }
map_U'_le : ∀ (n : ℕ), Submodule.map ((toEnd R L V) z) (U' n) ≤ U' (n + 1)
n : ℕ
hn :
  ∀ (w : A),
    ∀ a < n + 1, (T χ w) (((toEnd R L V) z ^ a) v) ∈ Submodule.span R {x | ∃ i < n, ((toEnd R L V) z ^ i) v = x}
w : A
hm : n + 1 < n + 1 + 1
H : ∀ (w : A), ⁅w, ((toEnd R L V) z ^ n) v⁆ = (T χ w) (((toEnd R L V) z ^ n) v) + χ w • ((toEnd R L V) z ^ n) v
⊢ (T χ w) (((toEnd R L V) z ^ (n + 1)) v) ∈ Submodule.span R {x | ∃ i < n + 1, ((toEnd R L V) z ^ i) v = x}

Tactic:
rw [T, LinearMap.sub_apply, pow_succ', Module.End.mul_apply, LieModule.toEnd_apply_apply,
        LieModule.toEnd_apply_apply, LinearMap.smul_apply, Module.End.one_apply, leibniz_lie,
        lie_swap_lie w z, H, H, lie_add, lie_smul, add_sub_assoc, add_sub_assoc, sub_self, add_zero]

Goal state after:
case inr
R : Type u_1
L : Type u_2
A : Type u_3
V : Type u_4
inst✝¹⁹ : CommRing R
inst✝¹⁸ : IsPrincipalIdealRing R
inst✝¹⁷ : IsDomain R
inst✝¹⁶ : CharZero R
inst✝¹⁵ : LieRing L
inst✝¹⁴ : LieAlgebra R L
inst✝¹³ : LieRing A
inst✝¹² : LieAlgebra R A
inst✝¹¹ : Bracket L A
inst✝¹⁰ : Bracket A L
inst✝⁹ : AddCommGroup V
inst✝⁸ : Module R V
inst✝⁷ : Module.Free R V
inst✝⁶ : Module.Finite R V
inst✝⁵ : LieRingModule L V
inst✝⁴ : LieModule R L V
inst✝³ : LieRingModule A V
inst✝² : LieModule R A V
inst✝¹ : IsLieTower L A V
inst✝ : IsLieTower A L V
χ : A → R
z : L
v : V
hv : ∀ (x : A), ⁅x, v⁆ = χ x • v
a : A
hv' : v ≠ 0
U' : ℕ →o Submodule R V :=
  { toFun := fun n ↦ Submodule.span R {x | ∃ i < n, ((toEnd R L V) z ^ i) v = x}, monotone' := ⋯ }
map_U'_le : ∀ (n : ℕ), Submodule.map ((toEnd R L V) z) (U' n) ≤ U' (n + 1)
n : ℕ
hn :
  ∀ (w : A),
    ∀ a < n + 1, (T χ w) (((toEnd R L V) z ^ a) v) ∈ Submodule.span R {x | ∃ i < n, ((toEnd R L V) z ^ i) v = x}
w : A
hm : n + 1 < n + 1 + 1
H : ∀ (w : A), ⁅w, ((toEnd R L V) z ^ n) v⁆ = (T χ w) (((toEnd R L V) z ^ n) v) + χ w • ((toEnd R L V) z ^ n) v
⊢ -((T χ ⁅z, w⁆) (((toEnd R L V) z ^ n) v) + χ ⁅z, w⁆ • ((toEnd R L V) z ^ n) v) +
      ⁅z, (T χ w) (((toEnd R L V) z ^ n) v)⁆ ∈
    Submodule.span R {x | ∃ i < n + 1, ((toEnd R L V) z ^ i) v = x}
Module: Mathlib.GroupTheory.Perm.Cycle.Concrete

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x y : α
hy : y ∈ p.toList x
⊢ (p.toList x).next y hy = p y

Tactic:
rw [mem_toList_iff] at hy
  obtain ⟨k, hk, hk'⟩ := hy.left.exists_pow_eq_of_mem_support hy.right
  rw [← getElem_toList p x k (by simpa using hk)] at hk'
  simp_rw [← hk']
  rw [next_getElem _ (nodup_toList _ _), getElem_toList, getElem_toList, ← mul_apply, ← pow_succ']
  simp_rw [length_toList]
  rw [← pow_mod_orderOf_cycleOf_apply p (k + 1), IsCycle.orderOf]
  exact isCycle_cycleOf _ (mem_support.mp hy.right)

Goal state after:
Module: Mathlib.Algebra.Lie.Loop

Goal state before:
pp: R : Type u_1
A : Type u_2
L : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
inst✝² : AddCommGroup A
inst✝¹ : DistribSMul A R
inst✝ : SMulCommClass A R R
Φ : LinearMap.BilinForm R L
r : R
x : loopAlgebra R A L
⊢ { toFun := fun g ↦ ((toFinsupp R A L) g).sum fun a v ↦ a • (Φ (((toFinsupp R A L) (r • x)) (-a))) v, map_add' := ⋯,
      map_smul' := ⋯ } =
    (RingHom.id R) r •
      { toFun := fun g ↦ ((toFinsupp R A L) g).sum fun a v ↦ a • (Φ (((toFinsupp R A L) x) (-a))) v, map_add' := ⋯,
        map_smul' := ⋯ }

Tactic:
ext; simp [-smul_eq_mul, smul_comm]

Goal state after:
Module: Mathlib.Algebra.Lie.Extension

Goal state before:
pp: R : Type u_1
L : Type u_3
M : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
inst✝² : LieRing M
inst✝¹ : LieAlgebra R M
inst✝ : IsLieAbelian M
E : Extension R M L
s₁ s₂ : L →ₗ[R] E.L
hs₁ : LeftInverse ⇑E.proj ⇑s₁
hs₂ : LeftInverse ⇑E.proj ⇑s₂
x y : L
s : L → E.L
hs : ∀ (b : L), E.proj (s b) = b
s' : L → E.L
h : LeftInverse (⇑E.proj) s'
⊢ s x - s' x ∈ E.proj.ker

Tactic:
by rw [LieHom.mem_ker, map_sub, sub_eq_zero, h, hs]

Goal state after:
Module: Mathlib.Algebra.Lie.Extension

Goal state before:
pp: R : Type u_1
L : Type u_3
M : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
inst✝² : LieRing M
inst✝¹ : LieAlgebra R M
inst✝ : IsLieAbelian M
E : Extension R M L
s₁ s₂ : L →ₗ[R] E.L
hs₁ : LeftInverse ⇑E.proj ⇑s₁
hs₂ : LeftInverse ⇑E.proj ⇑s₂
x y : L
s : L → E.L
hs : ∀ (b : L), E.proj (s b) = b
s' : L → E.L
h : LeftInverse (⇑E.proj) s'
⊢ s' y - s y ∈ E.proj.ker

Tactic:
by rw [LieHom.mem_ker, map_sub, sub_eq_zero, h, hs]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Correctness

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n) (Fin n) R
p : ℕ
i : Fin n
hEq1 : Eq1 A p
k : Fin n
⊢ ∑ α ∈ S p k, bminor A k k α = ∑ i ∈ Finset.image (Fin.cons k) (S p k), pminor A i

Tactic:
symm

Goal state after:
R : Type u_1
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n) (Fin n) R
p : ℕ
i : Fin n
hEq1 : Eq1 A p
k : Fin n
⊢ ∑ i ∈ Finset.image (Fin.cons k) (S p k), pminor A i = ∑ α ∈ S p k, bminor A k k α
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Correctness

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n) (Fin n) R
p : ℕ
i j : Fin n
⊢ ∑ x ∈ S p i ×ˢ Finset.Ioi i, bminor A i x.2 x.1 * A x.2 j =
    ∑ x ∈ S (p + 1) i ×ˢ Finset.univ, bminor A i (x.1 x.2) (x.2.removeNth x.1) * A (x.1 x.2) j

Tactic:
symm

Goal state after:
R : Type u_1
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n) (Fin n) R
p : ℕ
i j : Fin n
⊢ ∑ x ∈ S (p + 1) i ×ˢ Finset.univ, bminor A i (x.1 x.2) (x.2.removeNth x.1) * A (x.1 x.2) j =
    ∑ x ∈ S p i ×ˢ Finset.Ioi i, bminor A i x.2 x.1 * A x.2 j
Module: Mathlib.Algebra.Lie.LieTheorem

Goal state before:
pp: case inr
k : Type u_1
inst✝¹² : Field k
V : Type u_3
inst✝¹¹ : AddCommGroup V
inst✝¹⁰ : Module k V
inst✝⁹ : CharZero k
inst✝⁸ : Module.Finite k V
inst✝⁷ : Nontrivial V
L : Type u_4
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra k L
inst✝⁴ : LieRingModule L V
inst✝³ : LieModule k L V
inst✝² : IsSolvable L
inst✝¹ : IsTriangularizable k L V
inst✝ : Module.Finite k L
A : Submodule k L
hA : IsCoatom A
hAL : ↑(derivedSeries k L 1) ≤ A
⊢ ∃ χ, Nontrivial ↥(weightSpace V ⇑χ)

Tactic:
lift A to LieIdeal k L

Goal state after:
k : Type u_1
inst✝¹² : Field k
V : Type u_3
inst✝¹¹ : AddCommGroup V
inst✝¹⁰ : Module k V
inst✝⁹ : CharZero k
inst✝⁸ : Module.Finite k V
inst✝⁷ : Nontrivial V
L : Type u_4
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra k L
inst✝⁴ : LieRingModule L V
inst✝³ : LieModule k L V
inst✝² : IsSolvable L
inst✝¹ : IsTriangularizable k L V
inst✝ : Module.Finite k L
A : Submodule k L
hA : IsCoatom A
hAL : ↑(derivedSeries k L 1) ≤ A
⊢ ∀ {x m : L}, m ∈ A → ⁅x, m⁆ ∈ A

case inr
k : Type u_1
inst✝¹² : Field k
V : Type u_3
inst✝¹¹ : AddCommGroup V
inst✝¹⁰ : Module k V
inst✝⁹ : CharZero k
inst✝⁸ : Module.Finite k V
inst✝⁷ : Nontrivial V
L : Type u_4
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra k L
inst✝⁴ : LieRingModule L V
inst✝³ : LieModule k L V
inst✝² : IsSolvable L
inst✝¹ : IsTriangularizable k L V
inst✝ : Module.Finite k L
A : LieSubmodule k L L
hA : IsCoatom ↑A
hAL : ↑(derivedSeries k L 1) ≤ ↑A
⊢ ∃ χ, Nontrivial ↥(weightSpace V ⇑χ)
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: ⊢ A 1 = !![2]

Tactic:
decide

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: ⊢ A 2 = !![2, -1; -1, 2]

Tactic:
decide

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: ⊢ A 3 = !![2, -1, 0; -1, 2, -1; 0, -1, 2]

Tactic:
decide

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: ⊢ B 1 = A 1

Tactic:
decide

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: ⊢ C 1 = A 1

Tactic:
decide

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: ⊢ D 1 = A 1

Tactic:
decide

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: ⊢ D 2 = !![2, 0; 0, 2]

Tactic:
decide

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: ⊢ B 2 = !![2, -2; -1, 2]

Tactic:
decide

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: ⊢ C 2 = !![2, -1; -2, 2]

Tactic:
decide

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: ⊢ D 3 = !![2, -1, -1; -1, 2, 0; -1, 0, 2]

Tactic:
decide

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: ⊢ (reindex ((↑[0, 1]).formPerm ⋯) ((↑[0, 1]).formPerm ⋯)) (D 3) = A 3

Tactic:
decide

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: ⊢ D 4 = !![2, -1, 0, 0; -1, 2, -1, -1; 0, -1, 2, 0; 0, -1, 0, 2]

Tactic:
decide

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: case «0»
⊢ E₆ ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) = 2

Tactic:
decide

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: case «1»
⊢ E₆ ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) = 2

Tactic:
decide

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: case «2»
⊢ E₆ ((fun i ↦ i) ⟨2, ⋯⟩) ((fun i ↦ i) ⟨2, ⋯⟩) = 2

Tactic:
decide

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: case «3»
⊢ E₆ ((fun i ↦ i) ⟨3, ⋯⟩) ((fun i ↦ i) ⟨3, ⋯⟩) = 2

Tactic:
decide

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: case «4»
⊢ E₆ ((fun i ↦ i) ⟨4, ⋯⟩) ((fun i ↦ i) ⟨4, ⋯⟩) = 2

Tactic:
decide

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: case «5»
⊢ E₆ ((fun i ↦ i) ⟨5, ⋯⟩) ((fun i ↦ i) ⟨5, ⋯⟩) = 2

Tactic:
decide

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: case «0»
⊢ E₇ ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) = 2

Tactic:
decide

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: case «1»
⊢ E₇ ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) = 2

Tactic:
decide

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: case «2»
⊢ E₇ ((fun i ↦ i) ⟨2, ⋯⟩) ((fun i ↦ i) ⟨2, ⋯⟩) = 2

Tactic:
decide

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: case «3»
⊢ E₇ ((fun i ↦ i) ⟨3, ⋯⟩) ((fun i ↦ i) ⟨3, ⋯⟩) = 2

Tactic:
decide

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: case «4»
⊢ E₇ ((fun i ↦ i) ⟨4, ⋯⟩) ((fun i ↦ i) ⟨4, ⋯⟩) = 2

Tactic:
decide

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: case «5»
⊢ E₇ ((fun i ↦ i) ⟨5, ⋯⟩) ((fun i ↦ i) ⟨5, ⋯⟩) = 2

Tactic:
decide

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: case «6»
⊢ E₇ ((fun i ↦ i) ⟨6, ⋯⟩) ((fun i ↦ i) ⟨6, ⋯⟩) = 2

Tactic:
decide

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: case «0»
⊢ E₈ ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) = 2

Tactic:
decide

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: case «1»
⊢ E₈ ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) = 2

Tactic:
decide

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: case «2»
⊢ E₈ ((fun i ↦ i) ⟨2, ⋯⟩) ((fun i ↦ i) ⟨2, ⋯⟩) = 2

Tactic:
decide

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: case «3»
⊢ E₈ ((fun i ↦ i) ⟨3, ⋯⟩) ((fun i ↦ i) ⟨3, ⋯⟩) = 2

Tactic:
decide

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: case «4»
⊢ E₈ ((fun i ↦ i) ⟨4, ⋯⟩) ((fun i ↦ i) ⟨4, ⋯⟩) = 2

Tactic:
decide

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: case «5»
⊢ E₈ ((fun i ↦ i) ⟨5, ⋯⟩) ((fun i ↦ i) ⟨5, ⋯⟩) = 2

Tactic:
decide

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: case «6»
⊢ E₈ ((fun i ↦ i) ⟨6, ⋯⟩) ((fun i ↦ i) ⟨6, ⋯⟩) = 2

Tactic:
decide

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: case «7»
⊢ E₈ ((fun i ↦ i) ⟨7, ⋯⟩) ((fun i ↦ i) ⟨7, ⋯⟩) = 2

Tactic:
decide

Goal state after:
Module: Mathlib.Algebra.LinearRecurrence

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
E : LinearRecurrence R
u : ↥E.solSpace
n : ℕ
⊢ ↑((fun u ↦ ⟨E.mkSol u, ⋯⟩) ((fun u x ↦ ↑u ↑x) u)) n = ↑u n

Tactic:
symm

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
E : LinearRecurrence R
u : ↥E.solSpace
n : ℕ
⊢ ↑u n = ↑((fun u ↦ ⟨E.mkSol u, ⋯⟩) ((fun u x ↦ ↑u ↑x) u)) n
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: case «0»
⊢ F₄ ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) = 2

Tactic:
decide

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: case «1»
⊢ F₄ ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) = 2

Tactic:
decide

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: case «2»
⊢ F₄ ((fun i ↦ i) ⟨2, ⋯⟩) ((fun i ↦ i) ⟨2, ⋯⟩) = 2

Tactic:
decide

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: case «3»
⊢ F₄ ((fun i ↦ i) ⟨3, ⋯⟩) ((fun i ↦ i) ⟨3, ⋯⟩) = 2

Tactic:
decide

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: case «0»
⊢ G₂ ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) = 2

Tactic:
decide

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: case «1»
⊢ G₂ ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) = 2

Tactic:
decide

Goal state after:
Module: Mathlib.Algebra.Lie.Weights.IsSimple

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : CharZero K
inst✝¹ : IsKilling K L
inst✝ : IsTriangularizable K (↥H) L
I : LieIdeal K L
x : L
hxI : x ∈ ↑↑(LieSubmodule.restr I H)
hxH : x ∈ ↑↑H.toLieSubmodule
f : ↥LieSubalgebra.root → LieIdeal K ↥H := fun α ↦ corootSpace ⇑↑α
span_I_roots : LieIdeal K ↥H := ⨆ α ∈ I.rootSet, f α
span_compl_roots : LieIdeal K ↥H := ⨆ β, ⨆ (_ : β ∉ I.rootSet), f β
h_split : span_I_roots ⊔ span_compl_roots = ⨆ α, f α
⊢ ⨆ α, f α = ⊤

Tactic:
eq_top_iff,

Goal state after:
K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : CharZero K
inst✝¹ : IsKilling K L
inst✝ : IsTriangularizable K (↥H) L
I : LieIdeal K L
x : L
hxI : x ∈ ↑↑(LieSubmodule.restr I H)
hxH : x ∈ ↑↑H.toLieSubmodule
f : ↥LieSubalgebra.root → LieIdeal K ↥H := fun α ↦ corootSpace ⇑↑α
span_I_roots : LieIdeal K ↥H := ⨆ α ∈ I.rootSet, f α
span_compl_roots : LieIdeal K ↥H := ⨆ β, ⨆ (_ : β ∉ I.rootSet), f β
h_split : span_I_roots ⊔ span_compl_roots = ⨆ α, f α
⊢ ⊤ ≤ ⨆ α, f α
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: ⊢ E₆ᵀ = E₆

Tactic:
decide

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: ⊢ E₇ᵀ = E₇

Tactic:
decide

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: ⊢ E₈ᵀ = E₈

Tactic:
decide

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: ⊢ G₂.det = 1

Tactic:
decide

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: ⊢ F₄.det = 1

Tactic:
decide

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: ⊢ E₈.det = 1

Tactic:
by
  simp only [E₈, norm_det]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: ⊢ ∀ ⦃i j : Fin 6⦄, j < i → E₆ i j = 0 ∨ E₆ i j = -1

Tactic:
decide

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: ⊢ ∀ ⦃i j : Fin 7⦄, j < i → E₇ i j = 0 ∨ E₇ i j = -1

Tactic:
decide

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: ⊢ ∀ ⦃i j : Fin 8⦄, j < i → E₈ i j = 0 ∨ E₈ i j = -1

Tactic:
decide

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: ⊢ ¬F₄.IsSimplyLaced

Tactic:
decide

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: ⊢ ¬G₂.IsSimplyLaced

Tactic:
decide

Goal state after:
Module: Mathlib.RingTheory.FractionalIdeal.Inverse

Goal state before:
pp: K : Type u_3
inst✝⁴ : Field K
R₁ : Type u_4
inst✝³ : CommRing R₁
inst✝² : IsDomain R₁
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
x y : K
⊢ spanSingleton R₁⁰ x * spanSingleton R₁⁰ y⁻¹ = spanSingleton R₁⁰ (x / y)

Tactic:
spanSingleton_mul_spanSingleton,

Goal state after:
K : Type u_3
inst✝⁴ : Field K
R₁ : Type u_4
inst✝³ : CommRing R₁
inst✝² : IsDomain R₁
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
x y : K
⊢ spanSingleton R₁⁰ (x * y⁻¹) = spanSingleton R₁⁰ (x / y)
Module: Mathlib.RingTheory.FractionalIdeal.Inverse

Goal state before:
pp: K : Type u_3
inst✝⁴ : Field K
R₁ : Type u_4
inst✝³ : CommRing R₁
inst✝² : IsDomain R₁
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
x : K
hx : x ≠ 0
⊢ spanSingleton R₁⁰ x * spanSingleton R₁⁰ x⁻¹ = 1

Tactic:
spanSingleton_mul_spanSingleton,

Goal state after:
K : Type u_3
inst✝⁴ : Field K
R₁ : Type u_4
inst✝³ : CommRing R₁
inst✝² : IsDomain R₁
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
x : K
hx : x ≠ 0
⊢ spanSingleton R₁⁰ (x * x⁻¹) = 1
Module: Mathlib.RingTheory.FractionalIdeal.Inverse

Goal state before:
pp: K : Type u_3
inst✝⁴ : Field K
R₁ : Type u_6
inst✝³ : CommRing R₁
inst✝² : Algebra R₁ K
inst✝¹ : IsLocalization R₁⁰ K
I : FractionalIdeal R₁⁰ K
inst✝ : (↑I).IsPrincipal
h : I ≠ 0
⊢ spanSingleton R₁⁰ (generator ↑I) * spanSingleton R₁⁰ (generator ↑I)⁻¹ = 1

Tactic:
spanSingleton_mul_spanSingleton,

Goal state after:
K : Type u_3
inst✝⁴ : Field K
R₁ : Type u_6
inst✝³ : CommRing R₁
inst✝² : Algebra R₁ K
inst✝¹ : IsLocalization R₁⁰ K
I : FractionalIdeal R₁⁰ K
inst✝ : (↑I).IsPrincipal
h : I ≠ 0
⊢ spanSingleton R₁⁰ (generator ↑I * (generator ↑I)⁻¹) = 1