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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
hn : IsNilpotent f
hs : f.IsSemisimple
n : ℕ
h0 : f ^ n = 0
⊢ (aeval f) X = 0

Tactic:
]

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
hn : IsNilpotent f
hs : f.IsSemisimple
n : ℕ
h0 : f ^ n = 0
⊢ (aeval f) X = 0
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
g : R[X]
pb : PowerBasis R S
h₁ : (aeval (root g)) (minpoly R pb.gen) = 0
h₂ : (aeval pb.gen) g = 0
x✝ : AdjoinRoot g
x : R[X]
⊢ (mk g) x = (mk g) x

Tactic:
]

Goal state after:
Module: Mathlib.LinearAlgebra.Semisimple

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
hn : IsNilpotent f
hs : f.IsSemisimple
n : ℕ
h0 : (aeval f) (X ^ n) = 0
⊢ (aeval f) X = 0

Tactic:
]

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
hn : IsNilpotent f
hs : f.IsSemisimple
n : ℕ
h0 : (aeval f) (X ^ n) = 0
⊢ (aeval f) X = 0
Module: Mathlib.LinearAlgebra.Semisimple

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
hn : IsNilpotent f
hs : f.IsSemisimple
n : ℕ
h0 : X ^ n ∈ annihilator R[X] (AEval R M f)
⊢ X ∈ annihilator R[X] (AEval R M f)

Tactic:
]

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
hn : IsNilpotent f
hs : f.IsSemisimple
n : ℕ
h0 : X ^ n ∈ annihilator R[X] (AEval R M f)
⊢ X ∈ annihilator R[X] (AEval R M f)
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
g : R[X]
pb : PowerBasis R S
h₁ : (aeval (root g)) (minpoly R pb.gen) = 0
h₂ : (aeval pb.gen) g = 0
a✝ : Nontrivial S
f : R[X]
_hf : f.natDegree < pb.dim
⊢ eval₂ (algebraMap R S) pb.gen f = eval₂ (algebraMap R S) pb.gen f

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.Nilpotent.Exp

Goal state before:
pp: A : Type u_1
inst✝¹ : Ring A
inst✝ : Module ℚ A
a : A
k : ℕ
h : a ^ k = 0
h₁ :
  ∑ i ∈ range k, (↑i !)⁻¹ • a ^ i =
    ∑ i ∈ range (nilpotencyClass a), (↑i !)⁻¹ • a ^ i + ∑ i ∈ Ico (nilpotencyClass a) k, (↑i !)⁻¹ • a ^ i
this : ∑ i ∈ Ico (nilpotencyClass a) k, (↑i !)⁻¹ • a ^ i = 0
⊢ ∑ i ∈ range (nilpotencyClass a), (↑i !)⁻¹ • a ^ i = ∑ i ∈ range (nilpotencyClass a), (↑i !)⁻¹ • a ^ i

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.Nilpotent.Exp

Goal state before:
pp: A : Type u_1
inst✝¹ : Ring A
inst✝ : Module ℚ A
a : A
k : ℕ
h : a ^ k = 0
h₁ :
  ∑ i ∈ range k, (↑i !)⁻¹ • a ^ i =
    ∑ i ∈ range (nilpotencyClass a), (↑i !)⁻¹ • a ^ i + ∑ i ∈ Ico (nilpotencyClass a) k, (↑i !)⁻¹ • a ^ i
x✝ : ℕ
h₂ : x✝ ∈ Ico (nilpotencyClass a) k
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
L : Type u_6
F : Type u_7
inst✝³ : Field F
inst✝² : CommRing L
inst✝¹ : IsDomain L
inst✝ : Algebra F L
f : F[X]
hf : f ≠ 0
x : L
⊢ x ∈ f.aroots L ↔ x ∈ f.aroots L

pp: R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
L : Type u_6
F : Type u_7
inst✝³ : Field F
inst✝² : CommRing L
inst✝¹ : IsDomain L
inst✝ : Algebra F L
f : F[X]
hf : f ≠ 0
x : L
⊢ f * C f.leadingCoeff⁻¹ ≠ 0

Tactic:
]

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
L : Type u_6
F : Type u_7
inst✝³ : Field F
inst✝² : CommRing L
inst✝¹ : IsDomain L
inst✝ : Algebra F L
f : F[X]
hf : f ≠ 0
x : L
⊢ f * C f.leadingCoeff⁻¹ ≠ 0
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst✝ : CommRing R
I : Ideal R
f : R[X]
⊢ Ideal.map ((Ideal.Quotient.mk (span {f})).comp C) I = Ideal.map ((Ideal.Quotient.mk (span {f})).comp C) I

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : Ideal R
f : R[X]
x : AdjoinRoot f
⊢ (quotEquivOfEq ⋯) ((Ideal.Quotient.mk (Ideal.map (Ideal.Quotient.mk (span {f})) (Ideal.map C I))) x) =
    (Ideal.Quotient.mk (Ideal.map (of f) I)) x

Tactic:
]

Goal state after:
R : Type u_1
inst✝ : CommRing R
I : Ideal R
f : R[X]
x : AdjoinRoot f
⊢ (quotEquivOfEq ⋯) ((Ideal.Quotient.mk (Ideal.map (Ideal.Quotient.mk (span {f})) (Ideal.map C I))) x) =
    (Ideal.Quotient.mk (Ideal.map (of f) I)) x
Module: Mathlib.RingTheory.Nilpotent.Exp

Goal state before:
pp: case inr
A : Type u_1
inst✝⁴ : Ring A
inst✝³ : Module ℚ A
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module A M
inst✝ : Module ℚ M
a : A
m : M
k : ℕ
h : a ^ k • m = 0
hn : IsNilpotent a
h₀ : k < nilpotencyClass a
⊢ ∑ k ∈ range k, ((↑k !)⁻¹ • a ^ k) • m + ∑ k ∈ Ico k (nilpotencyClass a), ((↑k !)⁻¹ • a ^ k) • m =
    ∑ i ∈ range k, (↑i !)⁻¹ • a ^ i • m

Tactic:
]

Goal state after:
case inr
A : Type u_1
inst✝⁴ : Ring A
inst✝³ : Module ℚ A
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module A M
inst✝ : Module ℚ M
a : A
m : M
k : ℕ
h : a ^ k • m = 0
hn : IsNilpotent a
h₀ : k < nilpotencyClass a
⊢ ∑ k ∈ range k, ((↑k !)⁻¹ • a ^ k) • m + ∑ k ∈ Ico k (nilpotencyClass a), ((↑k !)⁻¹ • a ^ k) • m =
    ∑ i ∈ range k, (↑i !)⁻¹ • a ^ i • m
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst✝ : CommRing R
I : Ideal R
f : R[X]
⊢ span {(Ideal.Quotient.mk (Ideal.map C I)) f} = span {(Ideal.Quotient.mk (Ideal.map C I)) f}

Tactic:
]

Goal state after:
Module: Mathlib.LinearAlgebra.Semisimple

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
p : Submodule R M
hp : p ∈ f.invtSubmodule
hf : IsSemisimpleModule R[X] (AEval' f)
⊢ IsSemisimpleModule R[X] (AEval' (LinearMap.restrict f hp))

Tactic:
]

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
p : Submodule R M
hp : p ∈ f.invtSubmodule
hf : IsSemisimpleModule R[X] (AEval' f)
⊢ IsSemisimpleModule R[X] (AEval' (LinearMap.restrict f hp))
Module: Mathlib.RingTheory.Nilpotent.Exp

Goal state before:
pp: case inr
A : Type u_1
inst✝⁴ : Ring A
inst✝³ : Module ℚ A
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module A M
inst✝ : Module ℚ M
a : A
m : M
k : ℕ
h : a ^ k • m = 0
hn : IsNilpotent a
h₀ : k < nilpotencyClass a
r : ℕ
h₂ : r ∈ Ico k (nilpotencyClass a)
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.Nilpotent.Exp

Goal state before:
pp: A : Type u_1
inst✝¹ : Ring A
inst✝ : Module ℚ A
a b : A
h₁ : Commute a b
n₁ : ℕ
hn₁ : a ^ n₁ = 0
n₂ : ℕ
hn₂ : b ^ n₂ = 0
N : ℕ := max n₁ n₂
h₄ : a ^ (N + 1) = 0
h₅ : b ^ (N + 1) = 0
⊢ ∑ i ∈ range (2 * N + 1), (↑i !)⁻¹ • (a + b) ^ i = (∑ i ∈ range (N + 1), (↑i !)⁻¹ • a ^ i) * exp b

Tactic:
exp_eq_sum h₅

Goal state after:
A : Type u_1
inst✝¹ : Ring A
inst✝ : Module ℚ A
a b : A
h₁ : Commute a b
n₁ : ℕ
hn₁ : a ^ n₁ = 0
n₂ : ℕ
hn₂ : b ^ n₂ = 0
N : ℕ := max n₁ n₂
h₄ : a ^ (N + 1) = 0
h₅ : b ^ (N + 1) = 0
⊢ ∑ i ∈ range (2 * N + 1), (↑i !)⁻¹ • (a + b) ^ i =
    (∑ i ∈ range (N + 1), (↑i !)⁻¹ • a ^ i) * ∑ i ∈ range (N + 1), (↑i !)⁻¹ • b ^ i
Module: Mathlib.RingTheory.Nilpotent.Exp

Goal state before:
pp: A : Type u_1
inst✝¹ : Ring A
inst✝ : Module ℚ A
a b : A
h₁ : Commute a b
n₁ : ℕ
hn₁ : a ^ n₁ = 0
n₂ : ℕ
hn₂ : b ^ n₂ = 0
N : ℕ := max n₁ n₂
h₄ : a ^ (N + 1) = 0
h₅ : b ^ (N + 1) = 0
⊢ ∑ i ∈ range (2 * N + 1), (↑i !)⁻¹ • (a + b) ^ i =
    (∑ i ∈ range (N + 1), (↑i !)⁻¹ • a ^ i) * ∑ i ∈ range (N + 1), (↑i !)⁻¹ • b ^ i

Tactic:
]

Goal state after:
A : Type u_1
inst✝¹ : Ring A
inst✝ : Module ℚ A
a b : A
h₁ : Commute a b
n₁ : ℕ
hn₁ : a ^ n₁ = 0
n₂ : ℕ
hn₂ : b ^ n₂ = 0
N : ℕ := max n₁ n₂
h₄ : a ^ (N + 1) = 0
h₅ : b ^ (N + 1) = 0
⊢ ∑ i ∈ range (2 * N + 1), (↑i !)⁻¹ • (a + b) ^ i =
    (∑ i ∈ range (N + 1), (↑i !)⁻¹ • a ^ i) * ∑ i ∈ range (N + 1), (↑i !)⁻¹ • b ^ i
Module: Mathlib.LinearAlgebra.Semisimple

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
p : Submodule R M
hp : p ∈ f.invtSubmodule
hf : f.IsFinitelySemisimple
q : Submodule R ↥p
hq₁ : q ∈ invtSubmodule (LinearMap.restrict f hp)
hq₂ : Module.Finite R ↥q
this : Submodule.map p.subtype q ∈ f.invtSubmodule
e : ↥q ≃ₗ[R] ↥(Submodule.map p.subtype q) := p.equivSubtypeMap q
⊢ IsSemisimple (LinearMap.restrict f this)

Tactic:
]

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
p : Submodule R M
hp : p ∈ f.invtSubmodule
hf : f.IsFinitelySemisimple
q : Submodule R ↥p
hq₁ : q ∈ invtSubmodule (LinearMap.restrict f hp)
hq₂ : Module.Finite R ↥q
this : Submodule.map p.subtype q ∈ f.invtSubmodule
e : ↥q ≃ₗ[R] ↥(Submodule.map p.subtype q) := p.equivSubtypeMap q
⊢ IsSemisimple (LinearMap.restrict f this)
Module: Mathlib.LinearAlgebra.Determinant

Goal state before:
pp: case inr.inl
R : Type u_6
V : Type u_7
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : Module.Finite R V
W : Submodule R V
inst✝² : Free R ↥W
inst✝¹ : Module.Finite R ↥W
inst✝ : Free R (V ⧸ W)
e : V →ₗ[R] V
he : W ≤ comap e W
m : Type u_7 := Free.ChooseBasisIndex R ↥W
bW : Basis m R ↥W := Free.chooseBasis R ↥W
n : Type u_7 := Free.ChooseBasisIndex R (V ⧸ W)
bQ : Basis n R (V ⧸ W) := Free.chooseBasis R (V ⧸ W)
b : Basis (m ⊕ n) R V := bW.sumQuot bQ
A : Matrix m m R := (toMatrix bW bW) (e.restrict he)
B : Matrix m n R := of fun i l ↦ ((bW.sumQuot bQ).repr (e ((bW.sumQuot bQ) (Sum.inr l)))) (Sum.inl i)
D : Matrix n n R := (toMatrix bQ bQ) (W.mapQ W e he)
j : n
k : m
⊢ e ↑(bW k) ∈ W

Tactic:
]

Goal state after:
case inr.inl
R : Type u_6
V : Type u_7
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : Module.Finite R V
W : Submodule R V
inst✝² : Free R ↥W
inst✝¹ : Module.Finite R ↥W
inst✝ : Free R (V ⧸ W)
e : V →ₗ[R] V
he : W ≤ comap e W
m : Type u_7 := Free.ChooseBasisIndex R ↥W
bW : Basis m R ↥W := Free.chooseBasis R ↥W
n : Type u_7 := Free.ChooseBasisIndex R (V ⧸ W)
bQ : Basis n R (V ⧸ W) := Free.chooseBasis R (V ⧸ W)
b : Basis (m ⊕ n) R V := bW.sumQuot bQ
A : Matrix m m R := (toMatrix bW bW) (e.restrict he)
B : Matrix m n R := of fun i l ↦ ((bW.sumQuot bQ).repr (e ((bW.sumQuot bQ) (Sum.inr l)))) (Sum.inl i)
D : Matrix n n R := (toMatrix bQ bQ) (W.mapQ W e he)
j : n
k : m
⊢ e ↑(bW k) ∈ W
Module: Mathlib.LinearAlgebra.Semisimple

Goal state before:
pp: M✝ : Type u_2
inst✝⁵ : AddCommGroup M✝
K✝ : Type u_3
inst✝⁴ : Field K✝
inst✝³ : Module K✝ M✝
f✝ : End K✝ M✝
M : Type u_2
inst✝² : AddCommGroup M
K : Type u_3
inst✝¹ : Field K
inst✝ : Module K M
f : End K M
t : K
h : f.IsSemisimple
ht : t ≠ 0
⊢ f.IsSemisimple

Tactic:
]

Goal state after:
M✝ : Type u_2
inst✝⁵ : AddCommGroup M✝
K✝ : Type u_3
inst✝⁴ : Field K✝
inst✝³ : Module K✝ M✝
f✝ : End K✝ M✝
M : Type u_2
inst✝² : AddCommGroup M
K : Type u_3
inst✝¹ : Field K
inst✝ : Module K M
f : End K M
t : K
h : f.IsSemisimple
ht : t ≠ 0
⊢ f.IsSemisimple
Module: Mathlib.LinearAlgebra.Semisimple

Goal state before:
pp: M : Type u_2
inst✝² : AddCommGroup M
K : Type u_3
inst✝¹ : Field K
inst✝ : Module K M
f : End K M
p : K[X]
hp : Squarefree p
hpf : IsTorsionBySet K[X] (AEval K M f) ↑(Ideal.span {p})
⊢ f.IsSemisimple

Tactic:
]

Goal state after:
M : Type u_2
inst✝² : AddCommGroup M
K : Type u_3
inst✝¹ : Field K
inst✝ : Module K M
f : End K M
p : K[X]
hp : Squarefree p
hpf : IsTorsionBySet K[X] (AEval K M f) ↑(Ideal.span {p})
⊢ f.IsSemisimple
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : Ideal R
f p : R[X]
⊢ (Ideal.Quotient.mk (Ideal.map (of f) I)) ((mk f) p) = (Ideal.Quotient.mk (Ideal.map (of f) I)) ((mk f) p)

Tactic:
]

Goal state after:
Module: Mathlib.LinearAlgebra.Semisimple

Goal state before:
pp: M : Type u_2
inst✝³ : AddCommGroup M
K : Type u_3
inst✝² : Field K
inst✝¹ : Module K M
f : End K M
inst✝ : FiniteDimensional K M
hf : f.IsSemisimple
⊢ (annihilator K[X] (AEval' f)).IsRadical

Tactic:
]

Goal state after:
M : Type u_2
inst✝³ : AddCommGroup M
K : Type u_3
inst✝² : Field K
inst✝¹ : Module K M
f : End K M
inst✝ : FiniteDimensional K M
hf : f.IsSemisimple
⊢ (annihilator K[X] (AEval' f)).IsRadical
Module: Mathlib.LinearAlgebra.Semisimple

Goal state before:
pp: M : Type u_2
inst✝³ : AddCommGroup M
K : Type u_3
inst✝² : Field K
inst✝¹ : Module K M
f : End K M
inst✝ : FiniteDimensional K M
hf : f.IsSemisimple
p : K[X]
R : Type u_3 := K[X] ⧸ Ideal.span {minpoly K f}
this✝ : Module.Finite K R
this : IsReduced R
a : K[X]
h : a ∈ RingHom.ker (aeval f)
⊢ (aeval f) a = 0

Tactic:
]

Goal state after:
M : Type u_2
inst✝³ : AddCommGroup M
K : Type u_3
inst✝² : Field K
inst✝¹ : Module K M
f : End K M
inst✝ : FiniteDimensional K M
hf : f.IsSemisimple
p : K[X]
R : Type u_3 := K[X] ⧸ Ideal.span {minpoly K f}
this✝ : Module.Finite K R
this : IsReduced R
a : K[X]
h : a ∈ RingHom.ker (aeval f)
⊢ (aeval f) a = 0
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst✝ : CommRing R
I✝ : Ideal R
f✝ f : R[X]
I : Ideal R
x : R
this : (algebraMap R (AdjoinRoot f ⧸ Ideal.map (of f) I)) x = (Ideal.Quotient.mk (Ideal.map (of f) I)) ((mk f) (C x))
⊢ (Ideal.Quotient.mk (span {Polynomial.map (Ideal.Quotient.mk I) f})) (C ((Ideal.Quotient.mk I) x)) =
    ((algebraMap (R ⧸ I)[X] ((R ⧸ I)[X] ⧸ span {Polynomial.map (Ideal.Quotient.mk I) f})).comp
        (algebraMap R (R ⧸ I)[X]))
      x

Tactic:
]

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst✝ : CommRing R
I✝ : Ideal R
f✝ f : R[X]
I : Ideal R
x : R
this : (algebraMap R (AdjoinRoot f ⧸ Ideal.map (of f) I)) x = (Ideal.Quotient.mk (Ideal.map (of f) I)) ((mk f) (C x))
⊢ (Ideal.Quotient.mk (span {Polynomial.map (Ideal.Quotient.mk I) f})) (C ((Ideal.Quotient.mk I) x)) =
    ((algebraMap (R ⧸ I)[X] ((R ⧸ I)[X] ⧸ span {Polynomial.map (Ideal.Quotient.mk I) f})).comp
        (algebraMap R (R ⧸ I)[X]))
      x
Module: Mathlib.LinearAlgebra.Semisimple

Goal state before:
pp: M : Type u_2
inst✝³ : AddCommGroup M
K : Type u_3
inst✝² : Field K
inst✝¹ : Module K M
f : End K M
inst✝ : FiniteDimensional K M
hf : f.IsSemisimple
p : K[X]
R : Type u_3 := K[X] ⧸ Ideal.span {minpoly K f}
this✝ : Module.Finite K R
this : IsReduced R
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.Nilpotent.Exp

Goal state before:
pp: case calc_1
A : Type u_1
inst✝¹ : Ring A
inst✝ : Module ℚ A
a b : A
h₁ : Commute a b
n₁ : ℕ
hn₁ : a ^ n₁ = 0
n₂ : ℕ
hn₂ : b ^ n₂ = 0
N : ℕ := max n₁ n₂
h₄ : a ^ (N + 1) = 0
h₅ : b ^ (N + 1) = 0
R2N : Finset ℕ := range (2 * N + 1)
hR2N : R2N = range (2 * N + 1)
RN : Finset ℕ := range (N + 1)
hRN : RN = range (N + 1)
i : ℕ
x✝ : i ∈ R2N
⊢ (↑i !)⁻¹ • ∑ m ∈ range (i + 1), a ^ m * b ^ (i - m) * ↑(i.choose m) =
    (↑i !)⁻¹ • ∑ j ∈ range (i + 1), a ^ j * b ^ (i - j) * ↑(i.choose j)

Tactic:
]

Goal state after:
Module: Mathlib.LinearAlgebra.Semisimple

Goal state before:
pp: M : Type u_2
inst✝³ : AddCommGroup M
K : Type u_3
inst✝² : Field K
inst✝¹ : Module K M
f : End K M
inst✝ : FiniteDimensional K M
hf : f.IsSemisimple
a : End K M
ha : a ∈ (aeval f).range
⊢ a.IsSemisimple

Tactic:
]

Goal state after:
M : Type u_2
inst✝³ : AddCommGroup M
K : Type u_3
inst✝² : Field K
inst✝¹ : Module K M
f : End K M
inst✝ : FiniteDimensional K M
hf : f.IsSemisimple
a : End K M
ha : a ∈ (aeval f).range
⊢ a.IsSemisimple
Module: Mathlib.LinearAlgebra.Determinant

Goal state before:
pp: case inr.inr
R : Type u_6
V : Type u_7
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : Module.Finite R V
W : Submodule R V
inst✝² : Free R ↥W
inst✝¹ : Module.Finite R ↥W
inst✝ : Free R (V ⧸ W)
e : V →ₗ[R] V
he : W ≤ comap e W
m : Type u_7 := Free.ChooseBasisIndex R ↥W
bW : Basis m R ↥W := Free.chooseBasis R ↥W
n : Type u_7 := Free.ChooseBasisIndex R (V ⧸ W)
bQ : Basis n R (V ⧸ W) := Free.chooseBasis R (V ⧸ W)
b : Basis (m ⊕ n) R V := bW.sumQuot bQ
A : Matrix m m R := (toMatrix bW bW) (e.restrict he)
B : Matrix m n R := of fun i l ↦ ((bW.sumQuot bQ).repr (e ((bW.sumQuot bQ) (Sum.inr l)))) (Sum.inl i)
D : Matrix n n R := (toMatrix bQ bQ) (W.mapQ W e he)
j l : n
⊢ (bQ.repr (W.mkQ (e ((bW.sumQuot bQ) (Sum.inr l))))) j =
    (bQ.repr (Submodule.Quotient.mk (e ((bW.sumQuot bQ) (Sum.inr l))))) j

Tactic:
]

Goal state after:
case inr.inr
R : Type u_6
V : Type u_7
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : Module.Finite R V
W : Submodule R V
inst✝² : Free R ↥W
inst✝¹ : Module.Finite R ↥W
inst✝ : Free R (V ⧸ W)
e : V →ₗ[R] V
he : W ≤ comap e W
m : Type u_7 := Free.ChooseBasisIndex R ↥W
bW : Basis m R ↥W := Free.chooseBasis R ↥W
n : Type u_7 := Free.ChooseBasisIndex R (V ⧸ W)
bQ : Basis n R (V ⧸ W) := Free.chooseBasis R (V ⧸ W)
b : Basis (m ⊕ n) R V := bW.sumQuot bQ
A : Matrix m m R := (toMatrix bW bW) (e.restrict he)
B : Matrix m n R := of fun i l ↦ ((bW.sumQuot bQ).repr (e ((bW.sumQuot bQ) (Sum.inr l)))) (Sum.inl i)
D : Matrix n n R := (toMatrix bQ bQ) (W.mapQ W e he)
j l : n
⊢ (bQ.repr (W.mkQ (e ((bW.sumQuot bQ) (Sum.inr l))))) j =
    (bQ.repr (Submodule.Quotient.mk (e ((bW.sumQuot bQ) (Sum.inr l))))) j
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f g : R[X]
I : Ideal R
⊢ (Ideal.Quotient.mk (span {Polynomial.map (Ideal.Quotient.mk I) f})) (Polynomial.map (Ideal.Quotient.mk I) g) =
    (Ideal.Quotient.mk (span {Polynomial.map (Ideal.Quotient.mk I) f})) (Polynomial.map (Ideal.Quotient.mk I) g)

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f g : R[X]
I : Ideal R
⊢ (Ideal.Quotient.mk (Ideal.map (of f) I)) ((mk f) g) = (Ideal.Quotient.mk (Ideal.map (of f) I)) ((mk f) g)

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Lie.Derivation.Basic

Goal state before:
pp: case mk
R : Type u_1
L : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
D D1 D2✝ : LieDerivation R L M
a b : L
D2 : LieDerivation R L M
toLinearMap✝ : L →ₗ[R] M
leibniz'✝ : ∀ (a b : L), toLinearMap✝ ⁅a, b⁆ = ⁅a, toLinearMap✝ b⁆ - ⁅b, toLinearMap✝ a⁆
h : (fun D ↦ D.toFun) { toLinearMap := toLinearMap✝, leibniz' := leibniz'✝ } = (fun D ↦ D.toFun) D2
⊢ { toLinearMap := toLinearMap✝, leibniz' := leibniz'✝ } = D2

Tactic:
cases D2

Goal state after:
case mk.mk
R : Type u_1
L : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
D D1 D2 : LieDerivation R L M
a b : L
toLinearMap✝¹ : L →ₗ[R] M
leibniz'✝¹ : ∀ (a b : L), toLinearMap✝¹ ⁅a, b⁆ = ⁅a, toLinearMap✝¹ b⁆ - ⁅b, toLinearMap✝¹ a⁆
toLinearMap✝ : L →ₗ[R] M
leibniz'✝ : ∀ (a b : L), toLinearMap✝ ⁅a, b⁆ = ⁅a, toLinearMap✝ b⁆ - ⁅b, toLinearMap✝ a⁆
h :
  (fun D ↦ D.toFun) { toLinearMap := toLinearMap✝¹, leibniz' := leibniz'✝¹ } =
    (fun D ↦ D.toFun) { toLinearMap := toLinearMap✝, leibniz' := leibniz'✝ }
⊢ { toLinearMap := toLinearMap✝¹, leibniz' := leibniz'✝¹ } = { toLinearMap := toLinearMap✝, leibniz' := leibniz'✝ }
Module: Mathlib.Algebra.Lie.Derivation.Basic

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
D : LieDerivation R L L
a b : L
⊢ ⁅a, D b⁆ + ⁅D a, b⁆ = ⁅a, D b⁆ + ⁅D a, b⁆

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: case refine_1
R✝ : Type u_1
S✝ : Type u_2
T✝ : Type u_3
U✝ : Type u_4
K : Type u_5
R : Type u_6
S : Type u_7
T : Type u_8
U : Type u_9
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing T
inst✝³ : Algebra R S
inst✝² : Algebra R T
inst✝¹ : CommRing U
inst✝ : Algebra R U
p✝ p : S[X]
q : (T ⊗[R] S)[X]
h : Polynomial.map includeRight.toRingHom p = q
⊢ eval₂
      ((↑(Algebra.TensorProduct.map (AlgHom.id T T) (AlgHom.restrictScalars R (ofId S (AdjoinRoot p))))).comp
        ↑includeRight)
      (1 ⊗ₜ[R] root p) p =
    0

Tactic:
]

Goal state after:
case refine_1
R✝ : Type u_1
S✝ : Type u_2
T✝ : Type u_3
U✝ : Type u_4
K : Type u_5
R : Type u_6
S : Type u_7
T : Type u_8
U : Type u_9
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing T
inst✝³ : Algebra R S
inst✝² : Algebra R T
inst✝¹ : CommRing U
inst✝ : Algebra R U
p✝ p : S[X]
q : (T ⊗[R] S)[X]
h : Polynomial.map includeRight.toRingHom p = q
⊢ eval₂
      ((↑(Algebra.TensorProduct.map (AlgHom.id T T) (AlgHom.restrictScalars R (ofId S (AdjoinRoot p))))).comp
        ↑includeRight)
      (1 ⊗ₜ[R] root p) p =
    0
Module: Mathlib.Algebra.Lie.Derivation.Basic

Goal state before:
pp: case succ
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
D : LieDerivation R L L
a b : L
n : ℕ
ih : (⇑D)^[n] ⁅a, b⁆ = ∑ ij ∈ antidiagonal n, n.choose ij.1 • ⁅(⇑D)^[ij.1] a, (⇑D)^[ij.2] b⁆
⊢ (⇑D)^[n + 1] ⁅a, b⁆ =
    ∑ ij ∈ antidiagonal n, n.choose ij.1 • ⁅(⇑D)^[ij.1] a, (⇑D)^[ij.2 + 1] b⁆ +
      ∑ ij ∈ antidiagonal n, n.choose ij.2 • ⁅(⇑D)^[ij.1 + 1] a, (⇑D)^[ij.2] b⁆

Tactic:
]

Goal state after:
case succ
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
D : LieDerivation R L L
a b : L
n : ℕ
ih : (⇑D)^[n] ⁅a, b⁆ = ∑ ij ∈ antidiagonal n, n.choose ij.1 • ⁅(⇑D)^[ij.1] a, (⇑D)^[ij.2] b⁆
⊢ (⇑D)^[n + 1] ⁅a, b⁆ =
    ∑ ij ∈ antidiagonal n, n.choose ij.1 • ⁅(⇑D)^[ij.1] a, (⇑D)^[ij.2 + 1] b⁆ +
      ∑ ij ∈ antidiagonal n, n.choose ij.2 • ⁅(⇑D)^[ij.1 + 1] a, (⇑D)^[ij.2] b⁆
Module: Mathlib.Algebra.Lie.Derivation.Basic

Goal state before:
pp: case succ
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
D : LieDerivation R L L
a b : L
n : ℕ
ih : (⇑D)^[n] ⁅a, b⁆ = ∑ ij ∈ antidiagonal n, n.choose ij.1 • ⁅(⇑D)^[ij.1] a, (⇑D)^[ij.2] b⁆
x✝ : ℕ × ℕ
i j : ℕ
hij : (i, j) ∈ antidiagonal n
⊢ n.choose (i, j).2 • ⁅D ((⇑D)^[(i, j).1] a), (⇑D)^[(i, j).2] b⁆ =
    n.choose (i, j).2 • ⁅D ((⇑D)^[(i, j).1] a), (⇑D)^[(i, j).2] b⁆

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: case refine_1
R✝ : Type u_1
S✝ : Type u_2
T✝ : Type u_3
U✝ : Type u_4
K : Type u_5
R : Type u_6
S : Type u_7
T : Type u_8
U : Type u_9
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing T
inst✝³ : Algebra R S
inst✝² : Algebra R T
inst✝¹ : CommRing U
inst✝ : Algebra R U
p✝ p : S[X]
q : (T ⊗[R] S)[X]
h : Polynomial.map includeRight.toRingHom p = q
⊢ ↑includeRight (eval (root p) (Polynomial.map (of p) p)) = 0

Tactic:
]

Goal state after:
case refine_1
R✝ : Type u_1
S✝ : Type u_2
T✝ : Type u_3
U✝ : Type u_4
K : Type u_5
R : Type u_6
S : Type u_7
T : Type u_8
U : Type u_9
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing T
inst✝³ : Algebra R S
inst✝² : Algebra R T
inst✝¹ : CommRing U
inst✝ : Algebra R U
p✝ p : S[X]
q : (T ⊗[R] S)[X]
h : Polynomial.map includeRight.toRingHom p = q
⊢ ↑includeRight (eval (root p) (Polynomial.map (of p) p)) = 0