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

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
inst✝ : IsArtinianRing Rᵐᵒᵖ
x✝ : R
⊢ x✝ ∈ IsUnit.submonoid R ↔ x✝ ∈ R⁰

Tactic:
simp [IsUnit.mem_submonoid_iff, isUnit_iff_mem_nonZeroDivisors_of_mulOpposite]

Goal state after:
Module: Mathlib.Algebra.Homology.SpectralObject.SpectralSequence

Goal state before:
pp: C : Type u_1
ι : Type u_2
κ : Type u_3
inst✝³ : Category.{v_1, u_1} C
inst✝² : Abelian C
inst✝¹ : Preorder ι
X : SpectralObject C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
inst✝ : X.HasSpectralSequence data
r r' : ℤ
hrr' : r + 1 = r'
hr : r₀ ≤ r
pq pq' pq'' : κ
hpq : (c r).prev pq' = pq
hpq' : (c r).next pq' = pq''
i₀' i₀ i₁ i₂ i₃ i₃' : ι
hi₀' : i₀' = data.i₀ r' pq' ⋯
hi₀ : i₀ = data.i₀ r pq' ⋯
hi₁ : i₁ = data.i₁ pq'
hi₂ : i₂ = data.i₂ pq'
hi₃ : i₃ = data.i₃ r pq' ⋯
hi₃' : i₃' = data.i₃ r' pq' ⋯
n₀ n₁ n₂ : ℤ
hn₁' : n₁ = data.deg pq'
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ (X.spectralSequence data).iso r r' pq' ⋯ ⋯ =
    ((X.spectralSequence data).page r ⋯).homologyIsoSc' pq pq' pq'' hpq hpq' ≪≫
      (X.spectralSequenceHomologyData data r r' hrr' hr pq pq' pq'' hpq hpq' i₀' i₀ i₁ i₂ i₃ i₃' hi₀' hi₀ hi₁ hi₂ hi₃
              hi₃' n₀ n₁ n₂ hn₁' ⋯ ⋯).left.homologyIso ≪≫
        (X.spectralSequencePageXIso data r' ⋯ pq' i₀' i₁ i₂ i₃' hi₀' hi₁ hi₂ hi₃' n₀ n₁ n₂ hn₁' ⋯ ⋯).symm

Tactic:
by
  obtain rfl : n₀ = n₁ - 1 := by lia
  obtain rfl : n₂ = n₁ + 1 := by lia
  subst hpq hpq' hn₁' hi₀ hi₁ hi₂ hi₃ hi₀' hi₃'
  ext
  simp [spectralSequencePageXIso, spectralSequence, spectralSequenceHomologyData,
    SpectralSequence.homologyIso, SpectralSequence.homologyIso']

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

Goal state before:
pp: A : Type u_1
inst✝¹ : CommMagma A
inst✝ : IsCommJordan A
a b : A
⊢ a * (b * (a * a)) = a * (a * a * b)

Tactic:
mul_comm b (a * a)

Goal state after:
A : Type u_1
inst✝¹ : CommMagma A
inst✝ : IsCommJordan A
a b : A
⊢ a * (a * a * b) = a * (a * a * b)
Module: Mathlib.Algebra.Jordan.Basic

Goal state before:
pp: A : Type u_1
inst✝¹ : CommMagma A
inst✝ : IsCommJordan A
a b : A
⊢ b * (a * a) * a = a * a * b * a

Tactic:
mul_comm b (a * a)

Goal state after:
A : Type u_1
inst✝¹ : CommMagma A
inst✝ : IsCommJordan A
a b : A
⊢ a * a * b * a = a * a * b * a
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 : L
m : M
h : m ∈ (Submodule.toAddSubmonoid 0).carrier
⊢ ⁅x, m⁆ ∈ (Submodule.toAddSubmonoid 0).carrier

Tactic:
(Submodule.mem_bot R).1 h

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 N' : LieSubmodule R L M
x : L
m : M
h : m ∈ (Submodule.toAddSubmonoid 0).carrier
⊢ ⁅x, 0⁆ ∈ (Submodule.toAddSubmonoid 0).carrier
Module: Mathlib.Algebra.Lie.Abelian

Goal state before:
pp: case refine_2.mem.lie
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
s : Set L
h : ∀ x ∈ s, ∀ y ∈ s, ⁅x, y⁆ = 0
x✝¹ x✝ : ↥(lieSpan R L s)
x y w : L
hw : w ∈ s
u v : L
hx✝ : u ∈ lieSpan R L s
hy✝ : v ∈ lieSpan R L s
hu : ⁅⟨w, ⋯⟩, ⟨u, hx✝⟩⁆ = 0
hv : ⁅⟨w, ⋯⟩, ⟨v, hy✝⟩⁆ = 0
⊢ ⁅⟨w, ⋯⟩, ⟨⁅u, v⁆, ⋯⟩⁆ = 0

Tactic:
simp only [Subtype.ext_iff, coe_bracket, ZeroMemClass.coe_zero] at hu hv ⊢

Goal state after:
case refine_2.mem.lie
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
s : Set L
h : ∀ x ∈ s, ∀ y ∈ s, ⁅x, y⁆ = 0
x✝¹ x✝ : ↥(lieSpan R L s)
x y w : L
hw : w ∈ s
u v : L
hx✝ : u ∈ lieSpan R L s
hy✝ : v ∈ lieSpan R L s
hu : ⁅w, u⁆ = 0
hv : ⁅w, v⁆ = 0
⊢ ⁅w, ⁅u, v⁆⁆ = 0
Module: Mathlib.Algebra.Lie.Abelian

Goal state before:
pp: case refine_2.lie
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
s : Set L
h : ∀ x ∈ s, ∀ y ∈ s, ⁅x, y⁆ = 0
x✝¹ x✝ : ↥(lieSpan R L s)
x y : L
hy : y ∈ lieSpan R L s
u v : L
hx✝ : u ∈ lieSpan R L s
hy✝ : v ∈ lieSpan R L s
hu : ⁅⟨u, hx✝⟩, ⟨y, hy⟩⁆ = 0
hv : ⁅⟨v, hy✝⟩, ⟨y, hy⟩⁆ = 0
⊢ ⁅⟨⁅u, v⁆, ⋯⟩, ⟨y, hy⟩⁆ = 0

Tactic:
simp only [Subtype.ext_iff, coe_bracket, ZeroMemClass.coe_zero] at hu hv ⊢

Goal state after:
case refine_2.lie
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
s : Set L
h : ∀ x ∈ s, ∀ y ∈ s, ⁅x, y⁆ = 0
x✝¹ x✝ : ↥(lieSpan R L s)
x y : L
hy : y ∈ lieSpan R L s
u v : L
hx✝ : u ∈ lieSpan R L s
hy✝ : v ∈ lieSpan R L s
hu : ⁅u, y⁆ = 0
hv : ⁅v, y⁆ = 0
⊢ ⁅⁅u, v⁆, y⁆ = 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 N₂ : LieSubmodule R L M
⊢ Submodule.comap ↑N.incl ↑N₂ = ↑⊤ ↔ N ≤ N₂

Tactic:
LieSubmodule.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 N₂ : LieSubmodule R L M
⊢ Submodule.comap (↑N).subtype ↑N₂ = ↑⊤ ↔ N ≤ 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
inst✝ : Nontrivial B
⊢ ¬IsUnit (minpoly A x)

Tactic:
by
  have : Nontrivial A := (algebraMap A B).domain_nontrivial
  by_cases hx : IsIntegral A x
  · exact mt (monic hx).eq_one_of_isUnit (ne_one A x)
  · rw [eq_zero hx]
    exact not_isUnit_zero

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

Goal state before:
pp: A : Type u_1
inst✝³ : CommRing A
B : Type u_4
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : Nontrivial B
S : Subalgebra A B
x : B
int : IsIntegral (↥S) x
⊢ 2 ≤ (minpoly (↥S) x).natDegree ↔ x ∉ S

Tactic:
rw [two_le_natDegree_iff int, Iff.not]

Goal state after:
A : Type u_1
inst✝³ : CommRing A
B : Type u_4
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : Nontrivial B
S : Subalgebra A B
x : B
int : IsIntegral (↥S) x
⊢ x ∈ (algebraMap (↥S) B).range ↔ x ∈ S
Module: Mathlib.Algebra.Lie.IdealOperations

Goal state before:
pp: R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I₁ I₂ : LieIdeal R L
⊢ map I₁.incl (comap I₁.incl I₂) = I₁.incl.idealRange ⊓ I₂

Tactic:
rw [← map_comap_eq]

Goal state after:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I₁ I₂ : LieIdeal R L
⊢ I₁.incl.IsIdealMorphism
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
x y : S
d : ℕ
⊢ y ∈ Submodule.span R (Set.range fun i ↦ x ^ ↑i) ↔ ∃ f, f.degree < ↑d ∧ y = (aeval x) f

Tactic:
by
  have : (Set.range fun i : Fin d => x ^ (i : ℕ)) = (fun i : ℕ => x ^ i) '' ↑(Finset.range d) := by
    ext n
    simp_rw [Set.mem_range, Set.mem_image, Finset.mem_coe, Finset.mem_range]
    exact ⟨fun ⟨⟨i, hi⟩, hy⟩ => ⟨i, hi, hy⟩, fun ⟨i, hi, hy⟩ => ⟨⟨i, hi⟩, hy⟩⟩
  simp [this, mem_span_image_iff_linearCombination, degree_lt_iff_coeff_zero, eq_comm,
    exists_iff_exists_finsupp, coeff, aeval_def, eval₂_eq_sum, Polynomial.sum, mem_supported',
    Finsupp.sum, linearCombination, Algebra.smul_def, AddMonoidAlgebra.coeffEquiv.exists_congr_left]

Goal state after:
Module: Mathlib.RingTheory.PowerBasis

Goal state before:
pp: case inr
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
⊢ ((pb.basis.constr A) fun i ↦ y ^ ↑i) ((aeval pb.gen) f) = (aeval y) f

Tactic:
← aeval_modByMonic_eq_self_of_root (minpoly.aeval _ _),

Goal state after:
case inr
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
⊢ ((pb.basis.constr A) fun i ↦ y ^ ↑i) ((aeval pb.gen) (f %ₘ minpoly A pb.gen)) = (aeval y) f
Module: Mathlib.FieldTheory.KummerPolynomial

Goal state before:
pp: K : Type u
inst✝ : Field K
p : ℕ
hp : Nat.Prime p
a : K
ha : ∀ (b : K), b ^ p ≠ a
⊢ ¬IsUnit (X ^ p - C a)

Tactic:
Polynomial.isUnit_iff_degree_eq_zero,

Goal state after:
K : Type u
inst✝ : Field K
p : ℕ
hp : Nat.Prime p
a : K
ha : ∀ (b : K), b ^ p ≠ a
⊢ ¬(X ^ p - C a).degree = 0
Module: Mathlib.Algebra.Squarefree.Basic

Goal state before:
pp: case mul
R : Type u_1
inst✝¹ : CommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
z p : R
hz : z ≠ 0
hp : Irreducible p
ih : z ≠ 0 → ∃ y n, Squarefree y ∧ y ∣ z ∧ z ∣ y ^ n
hx : p * z ≠ 0
⊢ ∃ y n, Squarefree y ∧ y ∣ p * z ∧ p * z ∣ y ^ n

Tactic:
| mul z p hz hp ih =>

Goal state after:
Module: Mathlib.LinearAlgebra.Determinant

Goal state before:
pp: M : Type u_2
inst✝⁴ : AddCommGroup M
ι : Type u_4
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
A : Type u_5
inst✝¹ : CommRing A
inst✝ : Module A M
b : Basis ι A M
f : M →ₗ[A] M
⊢ (detAux (Trunc.mk b)) f = ((toMatrix b b) f).det

Tactic:
#adaptation_note /-- Proof repaired after leanprover/lean4#13492.
  The first line below was previously just `rw [detAux]`.
  The replacement proof is a short-term fix, and we request that the authors/maintainers of
  this file review the proof, and either approve it by removing this note, revise
  the proof or the prerequisites appropriately, or minimize a problem in lean4 that still
  needs addressing. -/
  simp only [detAux_def, Trunc.lift_mk]
  rfl

Goal state after:
Module: Mathlib.FieldTheory.Perfect

Goal state before:
pp: case h
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
n : ℕ
x : R
⊢ Function.Commute ⇑(frobenius S p) ⇑(frobeniusEquiv S p).symm

pp: case h
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
n : ℕ
x : R
⊢ Function.Commute ⇑(frobenius R p) ⇑(frobeniusEquiv R p).symm

Tactic:
all_goals rw [← coe_frobeniusEquiv]; simp [Function.Commute, Function.Semiconj]

Goal state after:
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: F : Type u
inst✝² : Field F
K : Type v
inst✝¹ : Field K
inst✝ : Algebra F K
p : F[X]
hsep : p.Separable
hsplit : (map (algebraMap F K) p).Splits
⊢ Fintype.card ↑(p.rootSet K) = p.natDegree

Tactic:
classical
  simp_rw [rootSet_def, Finset.coe_sort_coe, Fintype.card_coe]
  rw [Multiset.toFinset_card_of_nodup (nodup_roots hsep.map), ← hsplit.natDegree_eq_card_roots,
    natDegree_map]

Goal state after:
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
w : ι → Rˣ
⊢ e.det ⇑(e.unitsSMul w) = ∏ i, ↑(w i)

Tactic:
simp [det_apply]

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
inst✝ : CommRing R
I : Ideal R
f : R[X]
⊢ span {(Ideal.Quotient.mk (Ideal.map C I)) f} =
    Ideal.map (↑I.polynomialQuotientEquivQuotientPolynomial) (span {Polynomial.map (Ideal.Quotient.mk I) f})

Tactic:
map_span,

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 : R[X]
⊢ span {(Ideal.Quotient.mk (Ideal.map C I)) f} =
    span (⇑↑I.polynomialQuotientEquivQuotientPolynomial '' {Polynomial.map (Ideal.Quotient.mk I) 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
I : Ideal R
f : R[X]
⊢ Ideal.map (Ideal.Quotient.mk (Ideal.map C I)) (span {f}) = span {(Ideal.Quotient.mk (Ideal.map C I)) f}

Tactic:
map_span,

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 : R[X]
⊢ span (⇑(Ideal.Quotient.mk (Ideal.map C I)) '' {f}) = span {(Ideal.Quotient.mk (Ideal.map C I)) f}
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:
(Tactic.tacticLet__
 "let"
 (Term.letConfig [])
 (Term.letDecl
  (Term.letIdDecl
   (Term.letId `R)
   []
   []
   ":="
   («term_⧸_»
    (Polynomial.«term_[X]» `K "[X]")
    "⧸"
    (Term.app
     `Ideal.span
     [(choice
       («term{_}» "{" [`p] "}")
       (Term.structInst
        "{"
        []
        (Term.structInstFields [(Term.structInstField (Term.structInstLVal `p []) [])])
        (Term.optEllipsis [])
        []
        "}"))])))))

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})
R : Type u_3 := K[X] ⧸ Ideal.span {p}
⊢ f.IsSemisimple
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 + 1
⊢ (↑i !)⁻¹ • (a ^ j * b ^ (i - j) * ↑(i.choose j)) = ((↑j !)⁻¹ * (↑(i - j)!)⁻¹) • (a ^ j * b ^ (i - j))

Tactic:
replace hj := Nat.le_of_lt_succ 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 !)⁻¹ • (a ^ j * b ^ (i - j) * ↑(i.choose j)) = ((↑j !)⁻¹ * (↑(i - j)!)⁻¹) • (a ^ j * b ^ (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
x y z : L
⊢ -⁅z, ⁅x, y⁆⁆ = -⁅-⁅z, y⁆, x⁆ - -⁅-⁅z, x⁆, y⁆

Tactic:
leibniz_lie,

Goal state after:
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x y z : L
⊢ -(⁅⁅z, x⁆, y⁆ + ⁅x, ⁅z, y⁆⁆) = -⁅-⁅z, y⁆, x⁆ - -⁅-⁅z, x⁆, y⁆
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 = ⊥
⊢ LieModule.maxTrivSubmodule R L (LieDerivation R L L) = ⊥

Tactic:
refine (LieSubmodule.eq_bot_iff _).mpr fun D hD ↦ ext fun x ↦ ?_
  have : ad R L (D x) = 0 := by
    rw [LieModule.mem_maxTrivSubmodule] at hD
    simp [ad_apply_lieDerivation, hD]
  rw [← LieHom.mem_ker, ad_ker_eq_center, h, LieSubmodule.mem_bot] at this
  simp [this]

Goal state after:
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
⊢ x ^ m ∣ y ^ p

Tactic:
rw [← neg_neg y, neg_pow']

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
⊢ x ^ m ∣ (-y) ^ p * (-1) ^ p
Module: Mathlib.Algebra.Lie.Solvable

Goal state before:
pp: R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
k : ℕ
⊢ IsLieAbelian ↥(D k I) ↔ D 1 (D k I) = ⊥

Tactic:
abelian_iff_derived_one_eq_bot

Goal state after:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
k : ℕ
⊢ D 1 (D k I) = ⊥ ↔ D 1 (D k I) = ⊥
Module: Mathlib.Algebra.Lie.Solvable

Goal state before:
pp: R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
k l : ℕ
I J : LieIdeal R L
hI : derivedSeries R (↥I) k = ⊥
hJ : derivedSeries R (↥J) l = ⊥
⊢ derivedSeries R (↥(I + J)) (k + l) = ⊥

Tactic:
rw [LieIdeal.derivedSeries_eq_bot_iff] at hI hJ ⊢
  rw [← le_bot_iff]
  let D := derivedSeriesOfIdeal R L; change D k I = ⊥ at hI; change D l J = ⊥ at hJ
  calc
    D (k + l) (I + J) ≤ D k I + D l J := derivedSeriesOfIdeal_add_le_add I J k l
    _ ≤ ⊥ := by rw [hI, hJ]; simp

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

Goal state before:
pp: 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
N₁ N₂ : LieSubmodule R L M
h : N₁ ≤ N₂
m : M
hm : m ∈ N₁.normalizer
⊢ m ∈ N₂.normalizer

Tactic:
rw [mem_normalizer] at hm ⊢

Goal state after:
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
N₁ N₂ : LieSubmodule R L M
h : N₁ ≤ N₂
m : M
hm : ∀ (x : L), ⁅x, m⁆ ∈ N₁
⊢ ∀ (x : L), ⁅x, m⁆ ∈ N₂
Module: Mathlib.Algebra.Lie.Normalizer

Goal state before:
pp: R : Type u_1
L : Type u_2
M : Type u_3
M' : Type u_4
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
inst✝³ : AddCommGroup M'
inst✝² : Module R M'
inst✝¹ : LieRingModule L M'
inst✝ : LieModule R L M'
H : LieSubalgebra R L
y z : L
hy : y ∈ (↑H.toLieSubmodule.normalizer).carrier
hz : z ∈ (↑H.toLieSubmodule.normalizer).carrier
x : ↥H
⊢ ⁅↑x, ⁅y, z⁆⁆ ∈ H

Tactic:
leibniz_lie,

Goal state after:
R : Type u_1
L : Type u_2
M : Type u_3
M' : Type u_4
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
inst✝³ : AddCommGroup M'
inst✝² : Module R M'
inst✝¹ : LieRingModule L M'
inst✝ : LieModule R L M'
H : LieSubalgebra R L
y z : L
hy : y ∈ (↑H.toLieSubmodule.normalizer).carrier
hz : z ∈ (↑H.toLieSubmodule.normalizer).carrier
x : ↥H
⊢ ⁅⁅↑x, y⁆, z⁆ + ⁅y, ⁅↑x, z⁆⁆ ∈ H
Module: Mathlib.Algebra.Lie.BaseChange

Goal state before:
pp: case refine_2.refine_2.refine_2
R : Type u_1
A : Type u_2
L : Type u_3
M : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
x y : A ⊗[R] L
z : A ⊗[R] M
a₁ : A
l₁ : L
a₂ : A
l₂ : L
a₃ : A
l₃ : M
⊢ (a₁ * (a₂ * a₃)) ⊗ₜ[R] ⁅l₁, ⁅l₂, l₃⁆⁆ = (a₁ * (a₂ * a₃)) ⊗ₜ[R] ⁅⁅l₁, l₂⁆, l₃⁆ + (a₁ * (a₂ * a₃)) ⊗ₜ[R] ⁅l₂, ⁅l₁, l₃⁆⁆

Tactic:
leibniz_lie,

Goal state after:
case refine_2.refine_2.refine_2
R : Type u_1
A : Type u_2
L : Type u_3
M : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
x y : A ⊗[R] L
z : A ⊗[R] M
a₁ : A
l₁ : L
a₂ : A
l₂ : L
a₃ : A
l₃ : M
⊢ (a₁ * (a₂ * a₃)) ⊗ₜ[R] (⁅⁅l₁, l₂⁆, l₃⁆ + ⁅l₂, ⁅l₁, l₃⁆⁆) =
    (a₁ * (a₂ * a₃)) ⊗ₜ[R] ⁅⁅l₁, l₂⁆, l₃⁆ + (a₁ * (a₂ * a₃)) ⊗ₜ[R] ⁅l₂, ⁅l₁, l₃⁆⁆
Module: Mathlib.Algebra.Lie.Nilpotent

Goal state before:
pp: R₁ : Type u_1
R₂ : Type u_2
L : Type u_3
M : Type u_4
inst✝⁹ : CommRing R₁
inst✝⁸ : CommRing R₂
inst✝⁷ : AddCommGroup M
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R₁ L
inst✝⁴ : LieAlgebra R₂ L
inst✝³ : Module R₁ M
inst✝² : Module R₂ M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R₁ L M
k : ℕ
⊢ let I := lowerCentralSeries R₂ L M k;
  let S := {x | ∃ a, ∃ b ∈ I, ⁅a, b⁆ = x};
  ↑(Submodule.span R₁ S) ⊆ ↑(Submodule.span R₂ S)

Tactic:
by
  intro I S x hx
  simp only [SetLike.mem_coe] at hx ⊢
  induction hx using Submodule.closure_induction with
  | zero => exact Submodule.zero_mem _
  | add y z hy₁ hz₁ hy₂ hz₂ => exact Submodule.add_mem _ hy₂ hz₂
  | smul_mem c y hy =>
      obtain ⟨a, b, hb, rfl⟩ := hy
      rw [← smul_lie]
      exact Submodule.subset_span ⟨c • a, b, hb, rfl⟩

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

Goal state before:
pp: case refine_2
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
k : ℕ
N : LieSubmodule R L M
inst✝ : LieModule R L M
h : lcs k N = ⊥
⊢ lowerCentralSeries R L (↥N) k = ⊥

Tactic:
· rw [N.lowerCentralSeries_eq_lcs_comap, comap_incl_eq_bot]
    simp [h]

Goal state after:
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
N : LieSubmodule R L M
inst✝ : LieModule R L M
k : ℕ
⊢ comap N.incl (ucs k ⊥) = ucs k ⊥

Tactic:
induction k with
  | zero => exact N.ker_incl
  | succ k ih => simp [← ih]

Goal state after:
Module: Mathlib.FieldTheory.Fixed

Goal state before:
pp: G : Type u
inst✝² : Group G
F : Type v
inst✝¹ : Field F
inst✝ : MulSemiringAction G F
s✝ : Finset F
this : IsEmpty ↑↑∅
a : F
s : Finset F
has : a ∉ s
ih : LinearIndepOn (↥(subfield G F)) id ↑s → LinearIndepOn F ⇑(toFun G F) ↑s
hs : LinearIndepOn (↥(subfield G F)) id ↑(insert a s)
⊢ LinearIndepOn F ⇑(toFun G F) ↑(insert a s)

Tactic:
rw [coe_insert] at hs ⊢

Goal state after:
G : Type u
inst✝² : Group G
F : Type v
inst✝¹ : Field F
inst✝ : MulSemiringAction G F
s✝ : Finset F
this : IsEmpty ↑↑∅
a : F
s : Finset F
has : a ∉ s
ih : LinearIndepOn (↥(subfield G F)) id ↑s → LinearIndepOn F ⇑(toFun G F) ↑s
hs : LinearIndepOn (↥(subfield G F)) id (insert a ↑s)
⊢ LinearIndepOn F (⇑(toFun G F)) (insert a ↑s)
Module: Mathlib.RingTheory.Adjoin.Field

Goal state before:
pp: F : Type u_2
K : Type u_3
L : Type u_4
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra F K
inst✝ : Algebra F L
s : Finset K
⊢ (∀ x ∈ s, IsIntegral F x ∧ (map (algebraMap F L) (minpoly F x)).Splits) → Nonempty (↥(Algebra.adjoin F ↑s) →ₐ[F] L)

Tactic:
refine Finset.induction_on s (fun _ ↦ ?_) fun a s _ ih H ↦ ?_

Goal state after:
case refine_1
F : Type u_2
K : Type u_3
L : Type u_4
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra F K
inst✝ : Algebra F L
s : Finset K
x✝ : ∀ x ∈ ∅, IsIntegral F x ∧ (map (algebraMap F L) (minpoly F x)).Splits
⊢ Nonempty (↥(Algebra.adjoin F ↑∅) →ₐ[F] L)

case refine_2
F : Type u_2
K : Type u_3
L : Type u_4
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra F K
inst✝ : Algebra F L
s✝ : Finset K
a : K
s : Finset K
x✝ : a ∉ s
ih : (∀ x ∈ s, IsIntegral F x ∧ (map (algebraMap F L) (minpoly F x)).Splits) → Nonempty (↥(Algebra.adjoin F ↑s) →ₐ[F] L)
H : ∀ x ∈ insert a s, IsIntegral F x ∧ (map (algebraMap F L) (minpoly F x)).Splits
⊢ Nonempty (↥(Algebra.adjoin F ↑(insert a s)) →ₐ[F] L)
Module: Mathlib.RingTheory.Adjoin.Field

Goal state before:
pp: R : Type u_1
K : Type u_2
L : Type u_3
M : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : CommRing M
inst✝⁶ : Algebra R K
inst✝⁵ : Algebra R M
inst✝⁴ : Algebra K M
inst✝³ : IsScalarTower R K M
x : M
inst✝² : Algebra K L
inst✝¹ : Algebra R L
inst✝ : IsScalarTower R K L
int : IsIntegral R x
h : (Polynomial.map (algebraMap R L) (minpoly R x)).Splits
⊢ (Polynomial.map (algebraMap K L) (minpoly K x)).Splits

Tactic:
IsScalarTower.algebraMap_eq R K L

Goal state after:
R : Type u_1
K : Type u_2
L : Type u_3
M : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : CommRing M
inst✝⁶ : Algebra R K
inst✝⁵ : Algebra R M
inst✝⁴ : Algebra K M
inst✝³ : IsScalarTower R K M
x : M
inst✝² : Algebra K L
inst✝¹ : Algebra R L
inst✝ : IsScalarTower R K L
int : IsIntegral R x
h : (Polynomial.map ((algebraMap K L).comp (algebraMap R K)) (minpoly R x)).Splits
⊢ (Polynomial.map (algebraMap K L) (minpoly K x)).Splits