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

Goal state before:
pp: R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
s : Set L
⊢ s ⊆ ↑(comap f (lieSpan R L₂ (⇑f '' s)))

Tactic:
change s ⊆ f ⁻¹' (lieSpan R L₂ (f '' s))

Goal state after:
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
s : Set L
⊢ s ⊆ ⇑f ⁻¹' ↑(lieSpan R L₂ (⇑f '' s))
Module: Mathlib.Algebra.Lie.Submodule

Goal state before:
pp: R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
N N' : LieSubmodule R L M
⊢ ∀ (x y : L) (m : ↥N), ⟨⁅x, ↑⟨⁅y, ↑m⁆, ⋯⟩⁆, ⋯⟩ = ⟨⁅⁅x, y⁆, ↑m⁆, ⋯⟩ + ⟨⁅y, ↑⟨⁅x, ↑m⁆, ⋯⟩⁆, ⋯⟩

Tactic:
intro x y m; apply SetCoe.ext; apply leibniz_lie

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

Goal state before:
pp: R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
S : Set (LieSubmodule R L M)
⊢ ↑(sInf S) = ⋂ s ∈ S, ↑s

Tactic:
by
  rw [← LieSubmodule.coe_toSubmodule, sInf_toSubmodule, Submodule.coe_sInf]
  ext m
  simp only [mem_iInter, mem_ofPred_eq, forall_apply_eq_imp_iff₂, exists_imp,
    and_imp, SetLike.mem_coe, mem_toSubmodule]

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

Goal state before:
pp: case refine_3
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
N : LieSubmodule R L M
inst✝¹ : LieAlgebra R L
I : LieIdeal R L
inst✝ : LieModule R L M
s : Set M := {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}
y : L
m' : M
hm' : m' ∈ Submodule.span R s
m₁ m₂ : M
hx✝ : m₁ ∈ Submodule.span R s
hy✝ : m₂ ∈ Submodule.span R s
hm₁ : ⁅y, m₁⁆ ∈ Submodule.span R s
⊢ ⁅y, m₂⁆ ∈ Submodule.span R s → ⁅y, m₁ + m₂⁆ ∈ Submodule.span R s

Tactic:
hm₂

Goal state after:
case refine_3
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
N : LieSubmodule R L M
inst✝¹ : LieAlgebra R L
I : LieIdeal R L
inst✝ : LieModule R L M
s : Set M := {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}
y : L
m' : M
hm' : m' ∈ Submodule.span R s
m₁ m₂ : M
hx✝ : m₁ ∈ Submodule.span R s
hy✝ : m₂ ∈ Submodule.span R s
hm₁ : ⁅y, m₁⁆ ∈ Submodule.span R s
hm₂ : ⁅y, m₂⁆ ∈ Submodule.span R s
⊢ ⁅y, m₁ + m₂⁆ ∈ Submodule.span R s
Module: Mathlib.Algebra.Lie.Submodule

Goal state before:
pp: R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
s : Set M
⊢ Submodule.span R s ≤ ↑(lieSpan R L s)

Tactic:
rw [Submodule.span_le]
  apply subset_lieSpan

Goal state after:
Module: Mathlib.FieldTheory.Minpoly.Basic

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
⊢ (Polynomial.aeval x)
      (if hx : IsIntegral A x then ⋯.min (fun x_1 ↦ x_1.Monic ∧ eval₂ (algebraMap A B) x x_1 = 0) hx else 0) =
    0

Tactic:
split_ifs with hx

Goal state after:
case pos
A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
hx : IsIntegral A x
⊢ (Polynomial.aeval x) (⋯.min (fun x_1 ↦ x_1.Monic ∧ eval₂ (algebraMap A B) x x_1 = 0) hx) = 0

case neg
A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
hx : ¬IsIntegral A x
⊢ (Polynomial.aeval x) 0 = 0
Module: Mathlib.Algebra.Lie.Submodule

Goal state before:
pp: R : Type u
L : Type v
M : Type w
N : Type w₁
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : LieRingModule L N
f : M →ₗ⁅R,L⁆ N
⊢ ↑f.range = ↑⊤ ↔ Function.Surjective ⇑f

Tactic:
coe_range,

Goal state after:
R : Type u
L : Type v
M : Type w
N : Type w₁
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : LieRingModule L N
f : M →ₗ⁅R,L⁆ N
⊢ Set.range ⇑f = ↑⊤ ↔ Function.Surjective ⇑f
Module: Mathlib.FieldTheory.Minpoly.Basic

Goal state before:
pp: case neg
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : Ring B
inst✝¹ : Algebra A B
x : B
inst✝ : Nontrivial B
this : Nontrivial A
hx : ¬IsIntegral A x
⊢ ¬IsUnit (minpoly A x)

Tactic:
rw [eq_zero hx]

Goal state after:
case neg
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : Ring B
inst✝¹ : Algebra A B
x : B
inst✝ : Nontrivial B
this : Nontrivial A
hx : ¬IsIntegral A x
⊢ ¬IsUnit 0
Module: Mathlib.Algebra.Lie.Submodule

Goal state before:
pp: R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
N : LieSubmodule R L M
⊢ N.incl.range = N

Tactic:
simp only [← toSubmodule_inj, LieModuleHom.toSubmodule_range, incl_coe]

Goal state after:
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
N : LieSubmodule R L M
⊢ (↑N).subtype.range = ↑N
Module: Mathlib.FieldTheory.Minpoly.Basic

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
p : A[X]
pmonic : p.Monic
hp : (Polynomial.aeval x) p = 0
⊢ (if hx : IsIntegral A x then ⋯.min (fun x_1 ↦ x_1.Monic ∧ eval₂ (algebraMap A B) x x_1 = 0) hx else 0).degree ≤
    p.degree

Tactic:
split_ifs with hx

Goal state after:
case pos
A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
p : A[X]
pmonic : p.Monic
hp : (Polynomial.aeval x) p = 0
hx : IsIntegral A x
⊢ (⋯.min (fun x_1 ↦ x_1.Monic ∧ eval₂ (algebraMap A B) x x_1 = 0) hx).degree ≤ p.degree

case neg
A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
p : A[X]
pmonic : p.Monic
hp : (Polynomial.aeval x) p = 0
hx : ¬IsIntegral A x
⊢ degree 0 ≤ p.degree
Module: Mathlib.FieldTheory.Minpoly.Field

Goal state before:
pp: F : Type u_3
E : Type u_4
A : Type u_5
inst✝⁶ : Field F
inst✝⁵ : Field E
inst✝⁴ : CommRing A
inst✝³ : Algebra F E
inst✝² : Algebra E A
inst✝¹ : Algebra F A
inst✝ : IsScalarTower F E A
a : A
ha : IsIntegral F a
h : minpoly E a ∈ lifts (algebraMap F E)
⊢ map (algebraMap F E) (minpoly F a) = minpoly E a

Tactic:
refine eq_of_monic_of_dvd_of_natDegree_le (minpoly.monic ha.tower_top)
    ((algebraMap F E).injective.monic_map_iff.mp <| minpoly.monic ha)
    (minpoly.dvd E a (by simp)) ?_

Goal state after:
F : Type u_3
E : Type u_4
A : Type u_5
inst✝⁶ : Field F
inst✝⁵ : Field E
inst✝⁴ : CommRing A
inst✝³ : Algebra F E
inst✝² : Algebra E A
inst✝¹ : Algebra F A
inst✝ : IsScalarTower F E A
a : A
ha : IsIntegral F a
h : minpoly E a ∈ lifts (algebraMap F E)
⊢ (map (algebraMap F E) (minpoly F a)).natDegree ≤ (minpoly E a).natDegree
Module: Mathlib.FieldTheory.Minpoly.Basic

Goal state before:
pp: case refine_2
A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
a : A
hf : Injective ⇑(algebraMap A B)
a✝ : Nontrivial A
q : A[X]
hl : q.degree < (X - C a).degree
h0 : ¬q = 0
⊢ (Polynomial.aeval ((algebraMap A B) a)) q ≠ 0

Tactic:
rw [← natDegree_lt_natDegree_iff h0, natDegree_X_sub_C, Nat.lt_one_iff] at hl

Goal state after:
case refine_2
A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
a : A
hf : Injective ⇑(algebraMap A B)
a✝ : Nontrivial A
q : A[X]
hl : q.natDegree = 0
h0 : ¬q = 0
⊢ (Polynomial.aeval ((algebraMap A B) a)) q ≠ 0
Module: Mathlib.LinearAlgebra.SModEq.Basic

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
U : Submodule R M
x y : M
⊢ x ≡ y [SMOD U] ↔ x - y ∈ U

Tactic:
SModEq.def,

Goal state after:
R : Type u_1
inst✝² : Ring R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
U : Submodule R M
x y : M
⊢ Submodule.Quotient.mk x = Submodule.Quotient.mk y ↔ x - y ∈ U
Module: Mathlib.LinearAlgebra.SModEq.Basic

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
⊢ x ≡ y [SMOD ⊥] ↔ x = y

Tactic:
SModEq.def,

Goal state after:
R : Type u_1
inst✝² : Ring R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
⊢ Submodule.Quotient.mk x = Submodule.Quotient.mk y ↔ x = y
Module: Mathlib.LinearAlgebra.SModEq.Basic

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
U : Submodule R M
x : M
⊢ x ≡ 0 [SMOD U] ↔ x ∈ U

Tactic:
SModEq.def,

Goal state after:
R : Type u_1
inst✝² : Ring R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
U : Submodule R M
x : M
⊢ Submodule.Quotient.mk x = Submodule.Quotient.mk 0 ↔ x ∈ U
Module: Mathlib.LinearAlgebra.SModEq.Basic

Goal state before:
pp: case refine_1
R : Type u_1
inst✝² : Ring R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
U : Submodule R M
x y : M
h : x +ᵥ ↑U ⊆ y +ᵥ ↑U
⊢ x - y ∈ U

pp: case refine_2
R : Type u_1
inst✝² : Ring R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
U : Submodule R M
x y : M
h : x - y ∈ U
⊢ x +ᵥ ↑U ⊆ y +ᵥ ↑U

Tactic:
· rw [Set.vadd_set_subset_iff_subset_neg_vadd_set, vadd_vadd, neg_add_eq_sub] at h
    simpa [Set.mem_vadd_set_iff_neg_vadd_mem] using h U.zero_mem

Goal state after:
case refine_2
R : Type u_1
inst✝² : Ring R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
U : Submodule R M
x y : M
h : x - y ∈ U
⊢ x +ᵥ ↑U ⊆ y +ᵥ ↑U
Module: Mathlib.RingTheory.Polynomial.Ideal

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
x : R
y : R[X]
⊢ y ∈ RingHom.ker (evalRingHom x) ↔ y ∈ Ideal.span {X - C x}

Tactic:
simp [Ideal.mem_span_singleton, dvd_iff_isRoot, RingHom.mem_ker]

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Ideal

Goal state before:
pp: case mp
R : Type u_1
S : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
x : S
I : Ideal R
y : ↥R[x]
⊢ y ∈ Ideal.map (algebraMap R ↥R[x]) I → ∃ p, (∀ (i : ℕ), p.coeff i ∈ I) ∧ (aeval x) p = ↑y

Tactic:
intro H
    induction H using Submodule.span_induction with
    | mem a ha =>
      obtain ⟨a, ha, rfl⟩ := ha
      exact ⟨C a, fun i ↦ by rw [coeff_C]; aesop, aeval_C _ _⟩
    | zero => exact ⟨0, by simp, aeval_zero _⟩
    | add a b ha hb ha' hb' =>
      obtain ⟨a, ha, ha'⟩ := ha'
      obtain ⟨b, hb, hb'⟩ := hb'
      exact ⟨a + b, fun i ↦ by simpa using add_mem (ha i) (hb i), by simp [ha', hb']⟩
    | smul a b hb hb' =>
      obtain ⟨b', hb, hb'⟩ := hb'
      have ⟨p, hp⟩ := adjoin_eq_exists_aeval R x a
      refine ⟨p * b', fun i ↦ ?_, by simp [hp, hb']⟩
      rw [coeff_mul]
      exact sum_mem fun i hi ↦ Ideal.mul_mem_left _ _ (hb _)

Goal state after:
Module: Mathlib.RingTheory.PowerBasis

Goal state before:
pp: S : Type u_2
inst✝² : Ring S
A : Type u_4
inst✝¹ : CommRing A
inst✝ : Algebra A S
pb : PowerBasis A S
p : A[X]
ne_zero : p ≠ 0
root : (aeval pb.gen) p = 0
⊢ pb.dim ≤ p.natDegree

Tactic:
refine le_of_not_gt fun hlt => ne_zero ?_
  rw [p.as_sum_range' _ hlt, Finset.sum_range]
  refine Fintype.sum_eq_zero _ fun i => ?_
  simp_rw [aeval_eq_sum_range' hlt, Finset.sum_range, ← pb.basis_eq_pow] at root
  have := Fintype.linearIndependent_iff.1 pb.basis.linearIndependent _ root
  rw [this, monomial_zero_right]

Goal state after:
Module: Mathlib.Algebra.Squarefree.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommMonoidWithZero R
inst✝ : IsCancelMulZero R
y p : R
k : ℕ
hp : Prime p
x' : R
hx : Squarefree (p * x')
h : p ^ (k + 1) ∣ p * x' * y
hx' : ¬p ∣ x'
⊢ p ^ k ∣ x' * y

Tactic:
rw [pow_succ', mul_assoc] at h

Goal state after:
R : Type u_1
inst✝¹ : CommMonoidWithZero R
inst✝ : IsCancelMulZero R
y p : R
k : ℕ
hp : Prime p
x' : R
hx : Squarefree (p * x')
h : p * p ^ k ∣ p * (x' * y)
hx' : ¬p ∣ x'
⊢ p ^ k ∣ x' * y
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: R : Type u
inst✝ : CommRing R
n : ℕ
a b c : R
hn : ↑n = 0
hb : IsUnit b
⊢ (C a * X ^ n + C b * X + C c).Separable

Tactic:
set f := C a * X ^ n + C b * X + C c

Goal state after:
R : Type u
inst✝ : CommRing R
n : ℕ
a b c : R
hn : ↑n = 0
hb : IsUnit b
f : R[X] := C a * X ^ n + C b * X + C c
⊢ f.Separable
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:
exact Multiset.nodup_iff_count_le_one.mpr (count_roots_le_one hsep)

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]
hf : Irreducible f
⊢ f.Separable ∨ ¬f.Separable ∧ ∃ g, Irreducible g ∧ (expand F p) g = f

Tactic:
by
  classical
  exact if H : derivative f = 0 then by
    rcases p.eq_zero_or_pos with (rfl | hp)
    · have := CharP.charP_to_charZero F
      have := derivative_eq_zero.1 H
      have := (natDegree_pos_iff_degree_pos.mpr <| degree_pos_of_irreducible hf).ne'
      contradiction
    have := isLocalHom_expand F hp
    exact
      Or.inr
        ⟨by rw [separable_iff_derivative_ne_zero hf, Classical.not_not, H], contract p f,
          Irreducible.of_map (by rwa [← expand_contract p H hp.ne'] at hf),
          expand_contract p H hp.ne'⟩
  else Or.inl <| (separable_iff_derivative_ne_zero hf).2 H

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

Tactic:
(AEval.mapSubmodule R M f).symm.complementedLattice_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 ↥((Algebra.lsmul R R M) f).invtSubmodule ↔ ∀ (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)) %ₘ g).coeff ↑i = x i

Tactic:
rw [(modByMonic_eq_self_iff hg).mpr, finsetSum_coeff]

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
g : R[X]
hg : g.Monic
x : Fin g.natDegree → R
i : Fin g.natDegree
a✝ : Nontrivial R
⊢ ∑ b, ((monomial ↑b) (x b)).coeff ↑i = x i

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
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
p : Submodule R M
hp₁ : p ∈ f.invtSubmodule
hs : IsSemisimple (LinearMap.restrict f hp₁)
hp₂ : Module.Finite R ↥p
⊢ LinearMap.restrict f hp₁ = 0

Tactic:
replace hn : IsNilpotent (f.restrict hp₁) := isNilpotent.restrict hp₁ hn

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
hs : IsSemisimple (LinearMap.restrict f hp₁)
hp₂ : Module.Finite R ↥p
hn : IsNilpotent (LinearMap.restrict f hp₁)
⊢ LinearMap.restrict f hp₁ = 0
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
⊢ exp a = ∑ i ∈ range k, (↑i !)⁻¹ • a ^ i

Tactic:
by
  have h₁ : ∑ i ∈ range k, (i.factorial : ℚ)⁻¹ • (a ^ i) =
      ∑ i ∈ range (nilpotencyClass a), (i.factorial : ℚ)⁻¹ • (a ^ i) +
        ∑ i ∈ Ico (nilpotencyClass a) k, (i.factorial : ℚ)⁻¹ • (a ^ i) :=
    (sum_range_add_sum_Ico _ (csInf_le' h)).symm
  suffices ∑ i ∈ Ico (nilpotencyClass a) k, (i.factorial : ℚ)⁻¹ • (a ^ i) = 0 by
    dsimp [exp]
    rw [h₁, this, add_zero]
  exact sum_eq_zero fun _ h₂ => by
    rw [pow_eq_zero_of_le (mem_Ico.1 h₂).1 (pow_nilpotencyClass ⟨k, h⟩), smul_zero]

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
⊢ exp (a + b) = exp a * exp b

Tactic:
have h₅ : b ^ (N + 1) = 0 := pow_eq_zero_of_le (by omega) hn₂

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
⊢ exp (a + b) = exp a * exp b
Module: Mathlib.Algebra.Lie.TensorProduct

Goal state before:
pp: R : Type u
inst✝⁶ : CommRing R
L : Type v
M : Type w
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
N : LieSubmodule R L M
⊢ Submodule.span R {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x} = (↑(toModuleHom R L M) ∘ₗ ↑(mapIncl I N)).range

Tactic:
LinearMap.range_comp,

Goal state after:
R : Type u
inst✝⁶ : CommRing R
L : Type v
M : Type w
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
N : LieSubmodule R L M
⊢ Submodule.span R {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x} = Submodule.map (↑(toModuleHom R L M)) (↑(mapIncl I N)).range
Module: Mathlib.RingTheory.Nilpotent.Exp

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module ℚ M
inst✝ : Module ℚ N
fM : End R M
fN : End R N
g : M →ₗ[R] N
h : fN ∘ₗ g = g ∘ₗ fM
m : M
k : ℕ
hfM : fM ^ k = 0
l : ℕ
hfN : fN ^ l = 0
kl : ℕ := max k l
⊢ (exp fN ∘ₗ g) m = (g ∘ₗ exp fM) m

Tactic:
replace hfM : fM ^ kl = 0 := pow_eq_zero_of_le (by omega) hfM

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module ℚ M
inst✝ : Module ℚ N
fM : End R M
fN : End R N
g : M →ₗ[R] N
h : fN ∘ₗ g = g ∘ₗ fM
m : M
k l : ℕ
hfN : fN ^ l = 0
kl : ℕ := max k l
hfM : fM ^ kl = 0
⊢ (exp fN ∘ₗ g) m = (g ∘ₗ exp fM) m
Module: Mathlib.Algebra.Lie.TensorProduct

Goal state before:
pp: case h.left
R : Type u
inst✝⁶ : CommRing R
L : Type v
M : Type w
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
N : LieSubmodule R L M
x : L
hx : x ∈ I
n : M
hn : n ∈ N
⊢ x ⊗ₜ[R] n ∈ {t | ∃ m n, ↑(incl I) m ⊗ₜ[R] ↑N.incl n = t}

pp: case h.right
R : Type u
inst✝⁶ : CommRing R
L : Type v
M : Type w
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
N : LieSubmodule R L M
x : L
hx : x ∈ I
n : M
hn : n ∈ N
⊢ ↑(toModuleHom R L M) (x ⊗ₜ[R] n) = ⁅↑⟨x, hx⟩, ↑⟨n, hn⟩⁆

Tactic:
· use ⟨x, hx⟩, ⟨n, hn⟩; rfl

Goal state after:
case h.right
R : Type u
inst✝⁶ : CommRing R
L : Type v
M : Type w
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
N : LieSubmodule R L M
x : L
hx : x ∈ I
n : M
hn : n ∈ N
⊢ ↑(toModuleHom R L M) (x ⊗ₜ[R] n) = ⁅↑⟨x, hx⟩, ↑⟨n, hn⟩⁆
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
y₁ y₂ : A ⊗[R] L
⊢ ((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₁)) y₂ + ((bracket' R A L L) y₂) (a₁ ⊗ₜ[R] l₁) = 0 →
      ((bracket' R A L L) (a₁ ⊗ₜ[R] l₁)) (y₁ + y₂) + ((bracket' R A L L) (y₁ + y₂)) (a₁ ⊗ₜ[R] l₁) = 0

Tactic:
hy₁

Goal state after:
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
y₁ y₂ : A ⊗[R] L
hy₁ : ((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₁)) y₂ + ((bracket' R A L L) y₂) (a₁ ⊗ₜ[R] l₁) = 0 →
    ((bracket' R A L L) (a₁ ⊗ₜ[R] l₁)) (y₁ + y₂) + ((bracket' R A L L) (y₁ + y₂)) (a₁ ⊗ₜ[R] l₁) = 0
Module: Mathlib.Algebra.Lie.BaseChange

Goal state before:
pp: case refine_3.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
y₁ y₂ : A ⊗[R] L
⊢ ((bracket' R A L L) y₁) z₂ + ((bracket' R A L L) z₂) y₁ = 0 →
    ((bracket' R A L L) y₂) z₂ + ((bracket' R A L L) z₂) y₂ = 0 →
      ((bracket' R A L L) (y₁ + y₂)) z₂ + ((bracket' R A L L) z₂) (y₁ + y₂) = 0

Tactic:
hy₁

Goal state after:
case refine_3.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
y₁ y₂ : A ⊗[R] L
hy₁ : ((bracket' R A L L) y₁) z₂ + ((bracket' R A L L) z₂) y₁ = 0
⊢ ((bracket' R A L L) y₂) z₂ + ((bracket' R A L L) z₂) y₂ = 0 →
    ((bracket' R A L L) (y₁ + y₂)) z₂ + ((bracket' R A L L) z₂) (y₁ + y₂) = 0
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
H : LieSubalgebra R L
x y : L
hx : x ∈ H.normalizer
hy : y ∈ H
⊢ ⁅x, y⁆ ∈ H

Tactic:
by
  rw [← lie_skew, neg_mem_iff (G := L)]
  exact hx ⟨y, hy⟩

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

Goal state before:
pp: R : Type u₁
L : Type u₂
L₂ : Type u₃
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
hf : Surjective ⇑f
h : LieAlgebra.IsEngelian R L
M : Type u₄
_i1 : AddCommGroup M
_i2 : Module R M
_i3 : LieRingModule L₂ M
_i4 : LieModule R L₂ M
h' : ∀ (x : L₂), IsNilpotent ((toEnd R L₂ M) x)
⊢ LieModule.IsNilpotent L₂ M

Tactic:
let : LieRingModule L M := LieRingModule.compLieHom M f

Goal state after:
R : Type u₁
L : Type u₂
L₂ : Type u₃
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
hf : Surjective ⇑f
h : LieAlgebra.IsEngelian R L
M : Type u₄
_i1 : AddCommGroup M
_i2 : Module R M
_i3 : LieRingModule L₂ M
_i4 : LieModule R L₂ M
h' : ∀ (x : L₂), IsNilpotent ((toEnd R L₂ M) x)
this : LieRingModule L M := LieRingModule.compLieHom M f
⊢ LieModule.IsNilpotent L₂ M
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
inst✝ : LieModule R L M
N : LieSubmodule R L M
h₁ : N ≤ maxTrivSubmodule R L M
h₂ : IsNilpotent L (M ⧸ N)
⊢ IsNilpotent L M

Tactic:
rw [isNilpotent_iff R L] at h₂ ⊢

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
inst✝ : LieModule R L M
N : LieSubmodule R L M
h₁ : N ≤ maxTrivSubmodule R L M
h₂ : ∃ k, lowerCentralSeries R L (M ⧸ N) k = ⊥
⊢ ∃ k, lowerCentralSeries R L M k = ⊥
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra

Goal state before:
pp: K : Type u_3
L : Type u_4
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
E1 E2 : IntermediateField K L
inst✝ : Algebra.IsAlgebraic K ↥E1
⊢ (E1 ⊔ E2).toSubalgebra = E1.toSubalgebra ⊔ E2.toSubalgebra

Tactic:
have := sup_toSubalgebra_of_isAlgebraic_right E2 E1
  rwa [sup_comm (a := E1), sup_comm (a := E1.toSubalgebra)]

Goal state after: