mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.PowerBasis

Goal state before:
pp: case mpr
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
x y : S
d : ℕ
hd : d ≠ 0
⊢ (∃ f, f.natDegree < d ∧ y = (aeval x) f) → ∃ f, f.degree < ↑d ∧ y = (aeval x) f

Tactic:
rintro ⟨f, h, hy⟩
    refine ⟨f, ?_, hy⟩
    by_cases hf : f = 0
    · simp only [hf, natDegree_zero, Polynomial.degree_zero] at h ⊢
      first | exact lt_of_le_of_ne (Nat.zero_le d) hd.symm | exact WithBot.bot_lt_coe d
    simpa [degree_eq_natDegree hf] using h

Goal state after:
Module: Mathlib.RingTheory.PowerBasis

Goal state before:
pp: case inr.e_a
A : Type u_4
B : Type u_5
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
pb : PowerBasis A B
b : B
h✝ : Nontrivial B
H : (pb.basis.repr b) ⟨0, ⋯⟩ • pb.basis ⟨0, ⋯⟩ + ∑ x ∈ univ.erase ⟨0, ⋯⟩, (pb.basis.repr b) x • pb.basis x = b
i : Fin pb.dim
hi : i ∈ univ.erase ⟨0, ⋯⟩
⊢ (algebraMap A B) ((pb.basis.repr b) i) * (fun i ↦ pb.gen ^ ↑i) i ∈ Ideal.span {pb.gen}

Tactic:
refine Ideal.mul_mem_left _ _ <| Ideal.pow_mem_of_mem _ (Ideal.subset_span (by simp)) _ <|
      Nat.pos_of_ne_zero <| fun h ↦ notMem_erase i univ <| Fin.eq_mk_iff_val_eq.2 h ▸ hi

Goal state after:
Module: Mathlib.RingTheory.PowerBasis

Goal state before:
pp: case pos
S : Type u_2
inst✝² : Ring S
A : Type u_4
inst✝¹ : CommRing A
inst✝ : Algebra A S
pb : PowerBasis A S
h✝ : Nontrivial A
k : Fin pb.dim
h : ↑k + 1 = pb.dim
⊢ pb.gen ^ (↑k + 1) = ∑ x, -pb.minpolyGen.coeff ↑x • pb.gen ^ ↑x

Tactic:
h,

Goal state after:
case pos
S : Type u_2
inst✝² : Ring S
A : Type u_4
inst✝¹ : CommRing A
inst✝ : Algebra A S
pb : PowerBasis A S
h✝ : Nontrivial A
k : Fin pb.dim
h : ↑k + 1 = pb.dim
⊢ pb.gen ^ pb.dim = ∑ x, -pb.minpolyGen.coeff ↑x • pb.gen ^ ↑x
Module: Mathlib.RingTheory.PowerBasis

Goal state before:
pp: case neg.e_a
S : Type u_2
inst✝⁴ : Ring S
A : Type u_4
inst✝³ : CommRing A
inst✝² : Algebra A S
S' : Type u_7
inst✝¹ : Ring S'
inst✝ : Algebra A S'
pb : PowerBasis A S
y : S'
hy : (aeval y) (minpoly A pb.gen) = 0
f : A[X]
h✝ : Nontrivial A
hf : ¬f %ₘ minpoly A pb.gen = 0
this : (f %ₘ minpoly A pb.gen).natDegree < pb.dim
i : ℕ
hi : i < pb.dim
⊢ ((pb.basis.constr A) fun i ↦ y ^ ↑i) (pb.gen ^ ↑⟨i, hi⟩) = y ^ ↑⟨i, hi⟩

Tactic:
← pb.basis_eq_pow ⟨i, hi⟩,

Goal state after:
case neg.e_a
S : Type u_2
inst✝⁴ : Ring S
A : Type u_4
inst✝³ : CommRing A
inst✝² : Algebra A S
S' : Type u_7
inst✝¹ : Ring S'
inst✝ : Algebra A S'
pb : PowerBasis A S
y : S'
hy : (aeval y) (minpoly A pb.gen) = 0
f : A[X]
h✝ : Nontrivial A
hf : ¬f %ₘ minpoly A pb.gen = 0
this : (f %ₘ minpoly A pb.gen).natDegree < pb.dim
i : ℕ
hi : i < pb.dim
⊢ ((pb.basis.constr A) fun i ↦ y ^ ↑i) (pb.basis ⟨i, hi⟩) = y ^ ↑⟨i, hi⟩
Module: Mathlib.RingTheory.PowerBasis

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
B : PowerBasis R S
i : Fin B.dim
⊢ B.gen ^ ↑i ∈ ↑(Subalgebra.toSubmodule R[B.gen])

Tactic:
exact Subalgebra.pow_mem _ (subset_adjoin (Set.mem_singleton _)) _

Goal state after:
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
a : R
⊢ IsCoprime (X + C a) (derivative X + derivative (C a))

Tactic:
derivative_X,

Goal state after:
R : Type u
inst✝ : CommSemiring R
a : R
⊢ IsCoprime (X + C a) (1 + derivative (C a))
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: case inr
R : Type u
inst✝ : CommRing R
n : ℕ
u : Rˣ
hn : IsUnit ↑n
a✝ : Nontrivial R
hpos : n > 0
n' : R
hn' : n' * ↑n = 1
⊢ -C ↑u⁻¹ * (X ^ n - C ↑u) + C ↑u⁻¹ * C n' * X * (C ↑n * X ^ (n - 1) * derivative X) = 1

Tactic:
derivative_X,

Goal state after:
case inr
R : Type u
inst✝ : CommRing R
n : ℕ
u : Rˣ
hn : IsUnit ↑n
a✝ : Nontrivial R
hpos : n > 0
n' : R
hn' : n' * ↑n = 1
⊢ -C ↑u⁻¹ * (X ^ n - C ↑u) + C ↑u⁻¹ * C n' * X * (C ↑n * X ^ (n - 1) * 1) = 1
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hsep : p.Separable
⊢ p.roots.Nodup

Tactic:
classical
  exact Multiset.nodup_iff_count_le_one.mpr (count_roots_le_one hsep)

Goal state after:
Module: Mathlib.FieldTheory.Perfect

Goal state before:
pp: R : Type u_2
S : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
p : ℕ
inst✝³ : ExpChar R p
inst✝² : PerfectRing R p
inst✝¹ : ExpChar S p
inst✝ : PerfectRing S p
f : R →+* S
x : R
⊢ (frobeniusEquiv S p) (f ((frobeniusEquiv R p).symm x)) = (frobeniusEquiv S p) ((frobeniusEquiv S p).symm (f x))

Tactic:
simp [← RingHom.map_frobenius]

Goal state after:
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: F : Type u
inst✝ : Field F
p : ℕ
HF : CharP F p
f : F[X]
n : ℕ
hp : 0 < p
hf : IsUnit ((expand F (p ^ n)) f)
hn : n ≠ 0
hf2 : derivative ((expand F (p ^ n)) f) = 0
⊢ IsUnit f

Tactic:
isUnit_iff

Goal state after:
F : Type u
inst✝ : Field F
p : ℕ
HF : CharP F p
f : F[X]
n : ℕ
hp : 0 < p
hf : ∃ r, IsUnit r ∧ C r = (expand F (p ^ n)) f
hn : n ≠ 0
hf2 : derivative ((expand F (p ^ n)) f) = 0
⊢ IsUnit f
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: F : Type u
inst✝ : Field F
p : ℕ
HF : CharP F p
f : F[X]
n : ℕ
hp : 0 < p
hn : n ≠ 0
hf2 : derivative ((expand F (p ^ n)) f) = 0
r : F
hr : IsUnit r
hrf : C r = (expand F (p ^ n)) f
⊢ IsUnit f

Tactic:
rw [eq_comm, expand_eq_C (pow_pos hp _)] at hrf

Goal state after:
F : Type u
inst✝ : Field F
p : ℕ
HF : CharP F p
f : F[X]
n : ℕ
hp : 0 < p
hn : n ≠ 0
hf2 : derivative ((expand F (p ^ n)) f) = 0
r : F
hr : IsUnit r
hrf : f = C r
⊢ IsUnit f
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: case inl
F✝ : Type u
inst✝¹ : Field F✝
p✝ : ℕ
F : Type u
inst✝ : Field F
p : ℕ
HF : CharP F p
hp : 0 < p
n₁ : ℕ
g₂ : F[X]
hg₂ : g₂.Separable
k : ℕ
hg₁ : ((expand F (p ^ k)) g₂).Separable
hf : Irreducible ((expand F (p ^ n₁)) ((expand F (p ^ k)) g₂))
h : IsUnit g₂
⊢ n₁ = n₁ + k ∧ (expand F (p ^ k)) g₂ = g₂

Tactic:
isUnit_iff

Goal state after:
case inl
F✝ : Type u
inst✝¹ : Field F✝
p✝ : ℕ
F : Type u
inst✝ : Field F
p : ℕ
HF : CharP F p
hp : 0 < p
n₁ : ℕ
g₂ : F[X]
hg₂ : g₂.Separable
k : ℕ
hg₁ : ((expand F (p ^ k)) g₂).Separable
hf : Irreducible ((expand F (p ^ n₁)) ((expand F (p ^ k)) g₂))
h : ∃ r, IsUnit r ∧ C r = g₂
⊢ n₁ = n₁ + k ∧ (expand F (p ^ k)) g₂ = g₂
Module: Mathlib.LinearAlgebra.AnnihilatingPolynomial

Goal state before:
pp: case pos
𝕜 : Type u_1
A : Type u_2
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
h : annIdealGenerator 𝕜 a = 0
⊢ Ideal.span {annIdealGenerator 𝕜 a} = annIdeal 𝕜 a

Tactic:
h,

Goal state after:
case pos
𝕜 : Type u_1
A : Type u_2
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
h : annIdealGenerator 𝕜 a = 0
⊢ Ideal.span {0} = annIdeal 𝕜 a
Module: Mathlib.LinearAlgebra.AnnihilatingPolynomial

Goal state before:
pp: case pos
𝕜 : Type u_1
A : Type u_2
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
h : annIdealGenerator 𝕜 a = 0
⊢ annIdealGenerator 𝕜 a = minpoly 𝕜 a

Tactic:
h,

Goal state after:
case pos
𝕜 : Type u_1
A : Type u_2
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
h : annIdealGenerator 𝕜 a = 0
⊢ 0 = minpoly 𝕜 a
Module: Mathlib.LinearAlgebra.AnnihilatingPolynomial

Goal state before:
pp: case pos
𝕜 : Type u_1
A : Type u_2
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
p : 𝕜[X]
p_monic : p.Monic
p_gen : Ideal.span {p} = annIdeal 𝕜 a
h : p = 0
⊢ annIdealGenerator 𝕜 a = p

Tactic:
h,

Goal state after:
case pos
𝕜 : Type u_1
A : Type u_2
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
p : 𝕜[X]
p_monic : p.Monic
p_gen : Ideal.span {p} = annIdeal 𝕜 a
h : p = 0
⊢ annIdealGenerator 𝕜 a = 0
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: case h
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
i : F →+* K
f : F[X]
sep : f.Separable
sp : (map i f).Splits
s : Multiset K
h : map i f = C (map i f).leadingCoeff * (Multiset.map (fun x ↦ X - C x) s).prod
⊢ map i f = C (i f.leadingCoeff) * ∏ a ∈ s.toFinset, (X - C a)

Tactic:
h,

Goal state after:
case h
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
i : F →+* K
f : F[X]
sep : f.Separable
sp : (map i f).Splits
s : Multiset K
h : map i f = C (map i f).leadingCoeff * (Multiset.map (fun x ↦ X - C x) s).prod
⊢ C (map i f).leadingCoeff * (Multiset.map (fun x ↦ X - C x) s).prod =
    C (i f.leadingCoeff) * ∏ a ∈ s.toFinset, (X - C a)
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
f g✝ : R[X]
inst✝ : CommRing S
i : R →+* S
x : S
h : eval₂ i x f = 0
g : R[X]
H : g ∈ span {f}
y : R[X]
hy : g = f * y
⊢ eval₂ i x f * eval₂ i x y = 0

Tactic:
h,

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
f g✝ : R[X]
inst✝ : CommRing S
i : R →+* S
x : S
h : eval₂ i x f = 0
g : R[X]
H : g ∈ span {f}
y : R[X]
hy : g = f * y
⊢ 0 * eval₂ i x y = 0
Module: Mathlib.LinearAlgebra.Determinant

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
M' : Type u_3
inst✝³ : AddCommGroup M'
inst✝² : Module R M'
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
e : Basis ι R M
v : ι → M
i j : ι
h : v i = v j
hij : i ≠ j
⊢ (e.toMatrix (update v i (v i))).det = 0

Tactic:
h,

Goal state after:
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
M' : Type u_3
inst✝³ : AddCommGroup M'
inst✝² : Module R M'
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
e : Basis ι R M
v : ι → M
i j : ι
h : v i = v j
hij : i ≠ j
⊢ (e.toMatrix (update v i (v j))).det = 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
f✝ g : R[X]
inst✝⁵ : CommRing S
i : R →+* S
a : S
h✝ : eval₂ i a f✝ = 0
inst✝⁴ : CommRing T
inst✝³ : CommRing U
inst✝² : Algebra R S
inst✝¹ : Algebra R T
inst✝ : Algebra R U
f : S ≃ₐ[R] T
p : S[X]
q : T[X]
h : Associated (Polynomial.map (↑f) p) q
this : (↑f.toRingEquiv.symm).comp ↑f = RingHom.id S
⊢ Associated (Polynomial.map (↑f.symm) q) p

Tactic:
simpa [Polynomial.map_map, -RingEquiv.symm_mk, this]
        using! associated_map_map f.symm.toRingHom h.symm

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
⊢ IsSemisimpleModule R[X] (AEval' f) ↔ ∀ (p : ↥f.invtSubmodule), ∃ q, IsCompl p q

Tactic:
isSemisimpleModule_iff,

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
⊢ ComplementedLattice (Submodule R[X] (AEval' f)) ↔ ∀ (p : ↥f.invtSubmodule), ∃ q, IsCompl p q
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
g : R[X]
hg : g.Monic
x : Fin g.natDegree → R
i : Fin g.natDegree
a✝ : Nontrivial R
⊢ (∑ i, (monomial ↑i) (x i)).degree < g.degree

Tactic:
simp_rw [← C_mul_X_pow_eq_monomial]
            exact (degree_eq_natDegree <| hg.ne_zero).symm ▸ degree_sum_fin_lt _

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
e : Submodule R[X] (AEval' (LinearMap.restrict f hp)) ≃o ↑(Iic ((AEval.mapSubmodule R M f) ⟨p, hp⟩)) :=
  (Submodule.orderIsoMapComap (AEval.restrict_equiv_mapSubmodule f p hp)).trans
    ((AEval.mapSubmodule R M f) ⟨p, hp⟩).mapIic
⊢ IsSemisimpleModule R[X] (AEval' (LinearMap.restrict f hp)) ↔
    ∀ q ∈ f.invtSubmodule, q ≤ p → ∃ r ≤ p, r ∈ f.invtSubmodule ∧ Disjoint q r ∧ q ⊔ r = p

Tactic:
isSemisimpleModule_iff,

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
e : Submodule R[X] (AEval' (LinearMap.restrict f hp)) ≃o ↑(Iic ((AEval.mapSubmodule R M f) ⟨p, hp⟩)) :=
  (Submodule.orderIsoMapComap (AEval.restrict_equiv_mapSubmodule f p hp)).trans
    ((AEval.mapSubmodule R M f) ⟨p, hp⟩).mapIic
⊢ ComplementedLattice (Submodule R[X] (AEval' (LinearMap.restrict f hp))) ↔
    ∀ q ∈ f.invtSubmodule, q ≤ p → ∃ r ≤ p, r ∈ f.invtSubmodule ∧ Disjoint q r ∧ q ⊔ r = p
Module: Mathlib.LinearAlgebra.Determinant

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
e : Basis ι R M
v : ι → M
hli : LinearIndependent R v
hsp : ⊤ ≤ span R (Set.range v)
i : ι
⊢ ∀ (i_1 : ι),
    (e.det v • (Basis.mk hli hsp).coord i) ((Basis.mk hli hsp) i_1) =
      ((↑e.det).toLinearMap v i) ((Basis.mk hli hsp) i_1)

Tactic:
intro k

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
e : Basis ι R M
v : ι → M
hli : LinearIndependent R v
hsp : ⊤ ≤ span R (Set.range v)
i k : ι
⊢ (e.det v • (Basis.mk hli hsp).coord i) ((Basis.mk hli hsp) k) = ((↑e.det).toLinearMap v i) ((Basis.mk hli hsp) k)
Module: Mathlib.LinearAlgebra.Determinant

Goal state before:
pp: 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)
⊢ LinearMap.det e = LinearMap.det (e.restrict he) * LinearMap.det (W.mapQ W e he)

Tactic:
let bQ : Basis n R (V ⧸ W) := Module.Free.chooseBasis R (V ⧸ W)

Goal state after:
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)
⊢ LinearMap.det e = LinearMap.det (e.restrict he) * LinearMap.det (W.mapQ W e he)
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
M₂ : Type u_3
inst✝¹ : AddCommGroup M₂
inst✝ : Module R M₂
g : End R M₂
e✝ : M ≃ₗ[R] M₂
he : ↑e✝ ∘ₗ f = g ∘ₗ ↑e✝
e : AEval' f ≃ₗ[R[X]] AEval' g := LinearEquiv.ofAEval f (e✝ ≪≫ₗ AEval'.of g) ⋯
⊢ IsSemisimpleModule R[X] (AEval' f) ↔ IsSemisimpleModule R[X] (AEval' g)

Tactic:
isSemisimpleModule_iff,

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
M₂ : Type u_3
inst✝¹ : AddCommGroup M₂
inst✝ : Module R M₂
g : End R M₂
e✝ : M ≃ₗ[R] M₂
he : ↑e✝ ∘ₗ f = g ∘ₗ ↑e✝
e : AEval' f ≃ₗ[R[X]] AEval' g := LinearEquiv.ofAEval f (e✝ ≪≫ₗ AEval'.of g) ⋯
⊢ ComplementedLattice (Submodule R[X] (AEval' f)) ↔ ComplementedLattice (Submodule R[X] (AEval' g))
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)
⊢ (↑r !)⁻¹ • a ^ (r - k) • a ^ k • m = 0

Tactic:
h,

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
r : ℕ
h₂ : r ∈ Ico k (nilpotencyClass a)
⊢ (↑r !)⁻¹ • a ^ (r - k) • 0 = 0
Module: Mathlib.RingTheory.Nilpotent.Exp

Goal state before:
pp: case calc_2
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 : ℕ
hi : i ∈ R2N
j : ℕ
hj : j ≤ i
⊢ (↑i !)⁻¹ * ↑(i.choose j) = (↑j !)⁻¹ * (↑(i - j)!)⁻¹

Tactic:
Nat.choose_eq_factorial_div_factorial hj,

Goal state after:
case calc_2
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 : ℕ
hi : i ∈ R2N
j : ℕ
hj : j ≤ i
⊢ (↑i !)⁻¹ * ↑(i ! / (j ! * (i - j)!)) = (↑j !)⁻¹ * (↑(i - j)!)⁻¹
Module: Mathlib.Algebra.Lie.AdjointAction.Derivation

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
h : LieAlgebra.center R L = ⊥
D : LieDerivation R L L
hD : D ∈ LieModule.maxTrivSubmodule R L (LieDerivation R L L)
x : L
this : D x ∈ LieAlgebra.center R L
⊢ D x = 0 x

Tactic:
h,

Goal state after:
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
h : LieAlgebra.center R L = ⊥
D : LieDerivation R L L
hD : D ∈ LieModule.maxTrivSubmodule R L (LieDerivation R L L)
x : L
this : D x ∈ ⊥
⊢ D x = 0 x
Module: Mathlib.Dynamics.Newton

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : R[X]
x : S
h : (aeval x) P = 0
⊢ x - Ring.inverse ((aeval x) (derivative P)) * (aeval x) P = x

Tactic:
h,

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : R[X]
x : S
h : (aeval x) P = 0
⊢ x - Ring.inverse ((aeval x) (derivative P)) * 0 = x
Module: Mathlib.Algebra.Ring.Divisibility.Lemmas

Goal state before:
pp: R : Type u_1
x y : R
n m p : ℕ
inst✝ : Ring R
hp : n + m ≤ p + 1
h_comm : Commute x y
h : (x - y) ^ n = 0
⊢ (-1) ^ n * (x - y) ^ n = 0

Tactic:
h,

Goal state after:
R : Type u_1
x y : R
n m p : ℕ
inst✝ : Ring R
hp : n + m ≤ p + 1
h_comm : Commute x y
h : (x - y) ^ n = 0
⊢ (-1) ^ n * 0 = 0
Module: Mathlib.Algebra.Lie.Solvable

Goal state before:
pp: case succ.inl
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I J : LieIdeal R L
h₁ : I ≤ J
k : ℕ
ih : ∀ {l : ℕ}, l ≤ k → D k I ≤ D l J
l : ℕ
h₂ : l ≤ k + 1
h : l = k.succ
⊢ D (k + 1) I ≤ D l J

Tactic:
h,

Goal state after:
case succ.inl
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I J : LieIdeal R L
h₁ : I ≤ J
k : ℕ
ih : ∀ {l : ℕ}, l ≤ k → D k I ≤ D l J
l : ℕ
h₂ : l ≤ k + 1
h : l = k.succ
⊢ D (k + 1) I ≤ D k.succ J
Module: Mathlib.RingTheory.Nilpotent.Exp

Goal state before:
pp: A : Type u_1
inst✝⁵ : Ring A
inst✝⁴ : Module ℚ A
B : Type u_2
F : Type u_3
inst✝³ : Ring B
inst✝² : FunLike F A B
inst✝¹ : RingHomClass F A B
inst✝ : Module ℚ B
a : A
ha : IsNilpotent a
f : F
⊢ f (exp a) = exp (f a)

Tactic:
obtain ⟨k, hk⟩ := ha

Goal state after:
A : Type u_1
inst✝⁵ : Ring A
inst✝⁴ : Module ℚ A
B : Type u_2
F : Type u_3
inst✝³ : Ring B
inst✝² : FunLike F A B
inst✝¹ : RingHomClass F A B
inst✝ : Module ℚ B
a : A
f : F
k : ℕ
hk : a ^ k = 0
⊢ f (exp a) = exp (f a)
Module: Mathlib.Algebra.Lie.BaseChange

Goal state before:
pp: case refine_3.refine_2.refine_3
R : Type u_1
A : Type u_2
L : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x z₁ z₂ : A ⊗[R] L
h₁ : ((bracket' R A L L) z₁) z₁ = 0
h₂ : ((bracket' R A L L) z₂) z₂ = 0
a₁ : A
l₁ : L
⊢ ∀ (x y : A ⊗[R] L),
    ((bracket' R A L L) (a₁ ⊗ₜ[R] l₁)) x + ((bracket' R A L L) x) (a₁ ⊗ₜ[R] l₁) = 0 →
      ((bracket' R A L L) (a₁ ⊗ₜ[R] l₁)) y + ((bracket' R A L L) y) (a₁ ⊗ₜ[R] l₁) = 0 →
        ((bracket' R A L L) (a₁ ⊗ₜ[R] l₁)) (x + y) + ((bracket' R A L L) (x + y)) (a₁ ⊗ₜ[R] l₁) = 0

Tactic:
intro y₁ y₂ hy₁ hy₂
        simp only [hy₁, hy₂, add_add_add_comm, add_zero, LinearMap.add_apply, map_add]

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

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
⊢ idealizer I = normalizer I

Tactic:
by
  ext x; exact forall_congr' fun y ↦ by simp only [← lie_skew x y, neg_mem_iff]

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

Goal state before:
pp: R : Type u
L : Type v
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : L' →ₗ⁅R⁆ L
hL : ∃ k, derivedSeries R L k = ⊥
h : Injective ⇑f
⊢ ∀ (a : ℕ), derivedSeries R L a = ⊥ → derivedSeries R L' a = ⊥

Tactic:
intro k

Goal state after:
R : Type u
L : Type v
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : L' →ₗ⁅R⁆ L
hL : ∃ k, derivedSeries R L k = ⊥
h : Injective ⇑f
k : ℕ
⊢ derivedSeries R L k = ⊥ → derivedSeries R L' k = ⊥
Module: Mathlib.Algebra.Lie.Solvable

Goal state before:
pp: R : Type u
L : Type v
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : L' →ₗ⁅R⁆ L
hL' : ∃ k, derivedSeries R L' k = ⊥
h : Surjective ⇑f
⊢ ∀ (a : ℕ), derivedSeries R L' a = ⊥ → derivedSeries R L a = ⊥

Tactic:
intro k

Goal state after:
R : Type u
L : Type v
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : L' →ₗ⁅R⁆ L
hL' : ∃ k, derivedSeries R L' k = ⊥
h : Surjective ⇑f
k : ℕ
⊢ derivedSeries R L' k = ⊥ → derivedSeries R L k = ⊥
Module: Mathlib.Algebra.Lie.Solvable

Goal state before:
pp: R : Type u
L : Type v
M : Type w
L' : Type w₁
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
I J : LieIdeal R L
f : L' →ₗ⁅R⁆ L
inst✝ : IsNoetherian R L
⊢ IsSolvable ↥(radical R L)

Tactic:
have hwf := LieSubmodule.wellFoundedGT_of_noetherian R L L

Goal state after:
R : Type u
L : Type v
M : Type w
L' : Type w₁
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
I J : LieIdeal R L
f : L' →ₗ⁅R⁆ L
inst✝ : IsNoetherian R L
hwf : WellFoundedGT (LieSubmodule R L L)
⊢ IsSolvable ↥(radical R L)
Module: Mathlib.Algebra.Lie.Nilpotent

Goal state before:
pp: R : Type u
L : Type v
M : Type w
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
⊢ Antitone (lowerCentralSeries R L M)

Tactic:
intro l k

Goal state after:
R : Type u
L : Type v
M : Type w
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
l k : ℕ
⊢ l ≤ k → lowerCentralSeries R L M k ≤ lowerCentralSeries R L M l
Module: Mathlib.Algebra.Lie.Engel

Goal state before:
pp: case succ.refine_1
R : Type u₁
L : Type u₂
M : Type u₄
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
I : LieIdeal R L
x : L
hxI : R ∙ x ⊔ (LieIdeal.toLieSubalgebra R L I).toSubmodule = ⊤
n i j : ℕ
hxn : (toEnd R L M) x ^ n = 0
hIM : lowerCentralSeries R L M i ≤ I.lcs M j
l : ℕ
ih : ↑(⊤.lcs M (i + l)) ≤ Submodule.map ((toEnd R L M) x ^ l) ↑(I.lcs M j) ⊔ ↑(I.lcs M (j + 1))
⊢ Submodule.map ((toEnd R L M) x ^ (l + 1)) ↑(I.lcs M j) ⊔ Submodule.map ((toEnd R L M) x) ↑(I.lcs M (j + 1)) ≤
    Submodule.map ((toEnd R L M) x ^ (l + 1)) ↑(I.lcs M j) ⊔ ↑(I.lcs M (j + 1))

Tactic:
coe_map_toEnd_le

Goal state after:
case succ.refine_1
R : Type u₁
L : Type u₂
M : Type u₄
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
I : LieIdeal R L
x : L
hxI : R ∙ x ⊔ (LieIdeal.toLieSubalgebra R L I).toSubmodule = ⊤
n i j : ℕ
hxn : (toEnd R L M) x ^ n = 0
hIM : lowerCentralSeries R L M i ≤ I.lcs M j
l : ℕ
ih : ↑(⊤.lcs M (i + l)) ≤ Submodule.map ((toEnd R L M) x ^ l) ↑(I.lcs M j) ⊔ ↑(I.lcs M (j + 1))
⊢ Submodule.map ((toEnd R L M) x ^ (l + 1)) ↑(I.lcs M j) ⊔ ↑(I.lcs M (j + 1)) ≤
    Submodule.map ((toEnd R L M) x ^ (l + 1)) ↑(I.lcs M j) ⊔ ↑(I.lcs M (j + 1))