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

Goal state before:
pp: case e'_2
L₁ : Type u_1
L₂ : Type u_2
M : Type u_3
inst✝⁶ : Bracket L₁ L₂
inst✝⁵ : Bracket L₁ M
inst✝⁴ : Bracket L₂ M
inst✝³ : Bracket L₂ L₁
inst✝² : AddCommGroup M
inst✝¹ : IsLieTower L₁ L₂ M
inst✝ : IsLieTower L₂ L₁ M
x : L₁
y : L₂
m : M
h1 : ⁅x, ⁅y, m⁆⁆ = ⁅⁅x, y⁆, m⁆ + ⁅y, ⁅x, m⁆⁆
h2 : ⁅y, ⁅x, m⁆⁆ = ⁅⁅y, x⁆, m⁆ + ⁅x, ⁅y, m⁆⁆
⊢ ⁅⁅x, y⁆, m⁆ = ⁅⁅x, y⁆, m⁆ + ⁅y, ⁅x, m⁆⁆ - ⁅y, ⁅x, m⁆⁆

Tactic:
simp only [add_sub_cancel_right, sub_add_cancel_right]

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

Goal state before:
pp: case e'_3
L₁ : Type u_1
L₂ : Type u_2
M : Type u_3
inst✝⁶ : Bracket L₁ L₂
inst✝⁵ : Bracket L₁ M
inst✝⁴ : Bracket L₂ M
inst✝³ : Bracket L₂ L₁
inst✝² : AddCommGroup M
inst✝¹ : IsLieTower L₁ L₂ M
inst✝ : IsLieTower L₂ L₁ M
x : L₁
y : L₂
m : M
h1 : ⁅x, ⁅y, m⁆⁆ = ⁅⁅x, y⁆, m⁆ + ⁅y, ⁅x, m⁆⁆
h2 : ⁅y, ⁅x, m⁆⁆ = ⁅⁅y, x⁆, m⁆ + ⁅x, ⁅y, m⁆⁆
⊢ -⁅⁅y, x⁆, m⁆ = ⁅x, ⁅y, m⁆⁆ - (⁅⁅y, x⁆, m⁆ + ⁅x, ⁅y, m⁆⁆)

Tactic:
simp only [add_sub_cancel_right, sub_add_cancel_right]

Goal state after:
Module: Mathlib.RingTheory.Artinian.Module

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsArtinian R M
f : Module.End R M
⊢ ∀ᶠ (n : ℕ) in atTop, Codisjoint (f ^ n).ker (f ^ n).range

Tactic:
by
  obtain ⟨n, hn : ∀ m, n ≤ m → LinearMap.range (f ^ n) = LinearMap.range (f ^ m)⟩ :=
    IsArtinian.monotone_stabilizes f.iterateRange
  refine eventually_atTop.mpr ⟨n, fun m hm ↦ codisjoint_iff.mpr ?_⟩
  simp_rw [← hn _ hm, Submodule.eq_top_iff', Submodule.mem_sup]
  intro x
  rsuffices ⟨y, hy⟩ : ∃ y, (f ^ m) ((f ^ n) y) = (f ^ m) x
  · exact ⟨x - (f ^ n) y, by simp [hy], (f ^ n) y, by simp⟩
  -- Note: https://github.com/leanprover-community/mathlib4/pull/8386 had to change `mem_range` into `mem_range (f := _)`
  simp_rw [f.pow_apply n, f.pow_apply m, ← iterate_add_apply, ← f.pow_apply (m + n),
    ← f.pow_apply m, ← mem_range (f := _), ← hn _ (n.le_add_left m), hn _ hm]
  exact LinearMap.mem_range_self (f ^ m) x

Goal state after:
Module: Mathlib.RingTheory.Artinian.Module

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsArtinianRing R
⊢ {I | I.IsMaximal}.Finite

Tactic:
have ⟨s, H⟩ := Finset.exists_inf_le (Subtype.val (p := fun I : Ideal R ↦ I.IsMaximal))

Goal state after:
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsArtinianRing R
s : Finset { I // I.IsMaximal }
H : ∀ (a : { I // I.IsMaximal }), s.inf Subtype.val ≤ ↑a
⊢ {I | I.IsMaximal}.Finite
Module: Mathlib.RingTheory.Artinian.Module

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
inst✝ : IsArtinianRing R
Jac : Ideal R := Ring.jacobson R
n : ℕ
hn✝ : ∀ (m : ℕ), n ≤ m → { toFun := fun x ↦ Jac ^ x, monotone' := ⋯ } n = { toFun := fun x ↦ Jac ^ x, monotone' := ⋯ } m
hn : Jac * Jac ^ n = Jac ^ n
ne✝ : ¬Ring.jacobson R ^ n = 0
N : Ideal R
eq : Jac * N = N
ne : N ≠ ⊥
min : ∀ x ∈ {N | Jac * N = N ∧ N ≠ ⊥}, ¬x < N
this : Jac ^ n * N = N
I : R → Submodule R R := fun x ↦ Submodule.map (LinearMap.toSpanSingleton R R x) (Jac ^ n)
hI : ∀ (x : R), I x ≤ Ideal.span {x}
⊢ ∃ x ∈ N, I x ≠ ⊥

Tactic:
contrapose! ne
      rw [← this, ← le_bot_iff, Ideal.mul_le]
      refine fun ri hi rn hn ↦ ?_
      rw [← ne rn hn]
      exact ⟨ri, hi, rfl⟩

Goal state after:
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' : LieSubalgebra R L
⊢ ∀ (t : R) (x y : ↥L'), ⁅x, t • y⁆ = t • ⁅x, y⁆

Tactic:
{

Goal state after:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
L' : LieSubalgebra R L
⊢ ∀ (t : R) (x y : ↥L'), ⁅x, t • y⁆ = t • ⁅x, y⁆
Module: Mathlib.Algebra.Lie.IdealOperations

Goal state before:
pp: case mp
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
x : L
hx : x ∈ I
n : M
hn : n ∈ N
⊢ ∃ x_1 ∈ I, ∃ n_1 ∈ N, ⁅x_1, n_1⁆ = ⁅↑⟨x, hx⟩, ↑⟨n, hn⟩⁆

Tactic:
exact ⟨x, hx, n, hn, rfl⟩

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
m : M
s : Set (LieSubmodule R L M)
hdir : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s
hsup : m ∈ ↑(sSup s)
hne : Nonempty ↑s
this : ↑(⨆ i, ↑i) = ⋃ i ∈ s, ↑i
⊢ sSup s = ⨆ i, ↑i

Tactic:
sSup_eq_iSup,

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
m : M
s : Set (LieSubmodule R L M)
hdir : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s
hsup : m ∈ ↑(sSup s)
hne : Nonempty ↑s
this : ↑(⨆ i, ↑i) = ⋃ i ∈ s, ↑i
⊢ ⨆ a ∈ s, a = ⨆ i, ↑i
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
M' : LieSubmodule R L M
⊢ M' ≤ LieSubmodule.comap f ⊥ ↔ LieSubmodule.map f M' ≤ ⊥

Tactic:
LieSubmodule.map_le_iff_le_comap

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
M' : LieSubmodule R L M
⊢ M' ≤ LieSubmodule.comap f ⊥ ↔ M' ≤ LieSubmodule.comap f ⊥
Module: Mathlib.FieldTheory.Minpoly.Field

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝³ : Field A
inst✝² : Ring B
inst✝¹ : Algebra A B
inst✝ : Nontrivial B
p q : A[X]
hi : Irreducible p
b : B
hfa : (Polynomial.aeval b) p = 0
⊢ (Polynomial.aeval b) q = 0 ↔ p ∣ q

Tactic:
by
  refine ⟨fun hga ↦ dvd_trans ?_ (minpoly.dvd A b hga), ?_⟩
  · rw [← minpoly.eq_of_irreducible hi hfa]
    exact dvd_mul_right _ _
  · rintro ⟨g, rfl⟩
    simp [hfa]

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

Goal state before:
pp: A : Type u_1
inst✝¹ : NonUnitalNonAssocCommRing A
inst✝ : IsCommJordan A
a b c : A
⊢ 0 = ⁅L (a + b + c), L ((a + b + c) * (a + b + c))⁆

Tactic:
rw [(commute_lmul_lmul_sq (a + b + c)).lie_eq]

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
a✝ : Nontrivial A
⊢ pb.minpolyGen = minpoly A pb.gen

Tactic:
refine minpoly.unique' A _ pb.minpolyGen_monic pb.aeval_minpolyGen fun q hq =>
    or_iff_not_imp_left.2 fun hn0 h0 => ?_

Goal state after:
S : Type u_2
inst✝² : Ring S
A : Type u_4
inst✝¹ : CommRing A
inst✝ : Algebra A S
pb : PowerBasis A S
a✝ : Nontrivial A
q : A[X]
hq : q.degree < pb.minpolyGen.degree
hn0 : ¬q = 0
h0 : (aeval pb.gen) q = 0
⊢ False
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) = y ^ i

Tactic:
rw [← Fin.val_mk hi, ← pb.basis_eq_pow ⟨i, hi⟩, Basis.constr_basis]

Goal state after:
Module: Mathlib.RingTheory.PowerBasis

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁹ : CommRing R
inst✝⁸ : Ring S
inst✝⁷ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
K : Type u_6
inst✝³ : Field K
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
⊢ ((pb.basis.constr A) fun i ↦ y ^ ↑i).toFun 0 = 0

Tactic:
convert! pb.constr_pow_algebraMap hy 0 using 2 <;> rw [map_zero]

Goal state after:
Module: Mathlib.RingTheory.PowerBasis

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : Ring S
inst✝⁸ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : Algebra A B
K : Type u_6
inst✝⁴ : Field K
inst✝³ : Algebra A S
S' : Type u_7
inst✝² : Ring S'
inst✝¹ : Algebra A S'
inst✝ : IsDomain B
pb : PowerBasis A S
x : B
⊢ (aeval x) (minpoly A pb.gen) = 0 ↔ (Equiv.refl B) x ∈ (minpoly A pb.gen).aroots B

Tactic:
by
    rw [Equiv.refl_apply, mem_roots_iff_aeval_eq_zero]
    · simp
    · exact map_monic_ne_zero (minpoly.monic pb.isIntegral_gen)

Goal state after:
Module: Mathlib.FieldTheory.KummerPolynomial

Goal state before:
pp: K : Type u
inst✝ : Field K
a : K
H : Irreducible (X ^ 0 - C a)
⊢ False

Tactic:
pow_zero,

Goal state after:
K : Type u
inst✝ : Field K
a : K
H : Irreducible (1 - C a)
⊢ False
Module: Mathlib.Algebra.Squarefree.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Monoid R
x : R
n : ℕ
h : Squarefree (x ^ n)
h' : 2 ≤ n
⊢ x * x ∣ x ^ n

Tactic:
← sq

Goal state after:
R : Type u_1
inst✝ : Monoid R
x : R
n : ℕ
h : Squarefree (x ^ n)
h' : 2 ≤ n
⊢ x ^ 2 ∣ x ^ n
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
f g : R[X]
hf : f.Separable
hfg : g ∣ f
⊢ g.Separable

Tactic:
by
  rcases hfg with ⟨f', rfl⟩
  exact Separable.of_mul_left hf

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

Goal state before:
pp: case mpr
R : Type u_1
inst✝² : CommMonoidWithZero R
inst✝¹ : UniqueFactorizationMonoid R
inst✝ : NormalizationMonoid R
x : R
x0 : x ≠ 0
this : Nontrivial R
h : ∀ (a : R), Multiset.count a (normalizedFactors x) ≤ 1
a : R
⊢ emultiplicity a x ≤ 1 ∨ IsUnit a

Tactic:
· rw [or_iff_not_imp_right]
    intro hu
    rcases eq_or_ne a 0 with rfl | h0
    · simp [x0]
    rcases WfDvdMonoid.exists_irreducible_factor hu h0 with ⟨b, hib, hdvd⟩
    apply le_trans (emultiplicity_le_emultiplicity_of_dvd_left hdvd)
    rw [emultiplicity_eq_count_normalizedFactors hib x0]
    exact_mod_cast h (normalize b)

Goal state after:
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p q : R[X]
hsep : p.Separable
hq : 1 < emultiplicity q p
⊢ q * q ∣ p

Tactic:
← sq

Goal state after:
R : Type u
inst✝ : CommSemiring R
p q : R[X]
hsep : p.Separable
hq : 1 < emultiplicity q p
⊢ q ^ 2 ∣ p
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : Nontrivial R
ι : Type u_1
f : ι → R
s : Finset ι
x y : ι
hfs : ((X - C (f y)) * (X - C (f y)) * ∏ x ∈ (s.erase x).erase y, (X - C (f x))).Separable
hx : x ∈ s
hy : y ∈ s
hfxy : f x = f y
hxy : ¬x = y
⊢ False

Tactic:
← sq

Goal state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : Nontrivial R
ι : Type u_1
f : ι → R
s : Finset ι
x y : ι
hfs : ((X - C (f y)) ^ 2 * ∏ x ∈ (s.erase x).erase y, (X - C (f x))).Separable
hx : x ∈ s
hy : y ∈ s
hfxy : f x = f y
hxy : ¬x = y
⊢ False
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: F : Type u
inst✝ : Field F
f : F[X]
hf : Irreducible f
h : derivative f ≠ 0
g : F[X]
hg1 : g ∈ nonunits F[X]
_hg2 : g ≠ 0
x✝ : g ∣ f
hg4 : g ∣ derivative f
p : F[X]
hg3 : f = g * p
u : F[X]ˣ
hu : ↑u = p
⊢ f ∣ derivative f

Tactic:
by
        conv_lhs => rw [hg3, ← hu]
        rwa [Units.mul_right_dvd]

Goal state after:
Module: Mathlib.LinearAlgebra.Determinant

Goal state before:
pp: M : Type u_2
inst✝³ : AddCommGroup M
A : Type u_5
inst✝² : CommRing A
inst✝¹ : Module A M
inst✝ : Free A M
c : A
f : M →ₗ[A] M
⊢ LinearMap.det (c • f) = c ^ finrank A M * LinearMap.det f

Tactic:
by
  nontriviality A
  by_cases H : ∃ s : Finset M, Nonempty (Basis s A M)
  · have : Module.Finite A M := by
      rcases H with ⟨s, ⟨hs⟩⟩
      exact Module.Finite.of_basis hs
    simp only [← det_toMatrix (Module.finBasis A M), map_smul, Fintype.card_fin, Matrix.det_smul]
  · classical
      have : Module.finrank A M = 0 := finrank_eq_zero_of_not_exists_basis H
      simp [coe_det, H, this]

Goal state after:
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: case h.inl
F : Type u
inst✝ : Field F
p : ℕ
HF : CharP F p
hp : Nat.Prime p
N : ℕ
ih : ∀ m < N, ∀ {f : F[X]}, Irreducible f → f.natDegree = m → ∃ n g, g.Separable ∧ (expand F (p ^ n)) g = f
f : F[X]
hf : Irreducible f
hn : f.natDegree = N
h : f.Separable
⊢ (expand F (p ^ 0)) f = f

Tactic:
pow_zero,

Goal state after:
case h.inl
F : Type u
inst✝ : Field F
p : ℕ
HF : CharP F p
hp : Nat.Prime p
N : ℕ
ih : ∀ m < N, ∀ {f : F[X]}, Irreducible f → f.natDegree = m → ∃ n g, g.Separable ∧ (expand F (p ^ n)) g = f
f : F[X]
hf : Irreducible f
hn : f.natDegree = N
h : f.Separable
⊢ (expand F 1) f = f
Module: Mathlib.FieldTheory.Perfect

Goal state before:
pp: R : Type u_1
p : ℕ
inst✝² : CommSemiring R
inst✝¹ : ExpChar R p
inst✝ : PerfectRing R p
x : R
⊢ x ^ p ^ 0 = x

Tactic:
pow_zero,

Goal state after:
R : Type u_1
p : ℕ
inst✝² : CommSemiring R
inst✝¹ : ExpChar R p
inst✝ : PerfectRing R p
x : R
⊢ x ^ 1 = x
Module: Mathlib.LinearAlgebra.Determinant

Goal state before:
pp: case pos.hM'M
M : Type u_2
inst✝⁴ : AddCommGroup M
A : Type u_5
inst✝³ : CommRing A
inst✝² : Module A M
N : Type u_7
inst✝¹ : AddCommGroup N
inst✝ : Module A N
f : M →ₗ[A] M
e : M ≃ₗ[A] N
s : Finset M
b : Basis (↥s) A M
⊢ (toMatrix b b) ↑(e ≪≫ₗ e.symm) = 1

Tactic:
e.self_trans_symm,

Goal state after:
case pos.hM'M
M : Type u_2
inst✝⁴ : AddCommGroup M
A : Type u_5
inst✝³ : CommRing A
inst✝² : Module A M
N : Type u_7
inst✝¹ : AddCommGroup N
inst✝ : Module A N
f : M →ₗ[A] M
e : M ≃ₗ[A] N
s : Finset M
b : Basis (↥s) A M
⊢ (toMatrix b b) ↑(LinearEquiv.refl A M) = 1
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: case inr
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
hg₁ : ((expand F (p ^ 0)) g₂).Separable
hf : Irreducible ((expand F (p ^ n₁)) ((expand F (p ^ 0)) g₂))
⊢ n₁ = n₁ ∧ (expand F (p ^ 0)) g₂ = g₂

Tactic:
pow_zero,

Goal state after:
case inr
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
hg₁ : ((expand F (p ^ 0)) g₂).Separable
hf : Irreducible ((expand F (p ^ n₁)) ((expand F (p ^ 0)) g₂))
⊢ n₁ = n₁ ∧ (expand F 1) g₂ = g₂
Module: Mathlib.LinearAlgebra.AnnihilatingPolynomial

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : Field 𝕜
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module 𝕜 M
f : Module.End 𝕜 M
⊢ Ideal.span {minpoly 𝕜 f} = Module.annihilator 𝕜[X] (Module.AEval' f)

Tactic:
← annIdealGenerator_eq_minpoly,

Goal state after:
𝕜 : Type u_1
inst✝² : Field 𝕜
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module 𝕜 M
f : Module.End 𝕜 M
⊢ Ideal.span {annIdealGenerator 𝕜 f} = Module.annihilator 𝕜[X] (Module.AEval' 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₂ (↑(Algebra.ofId R S)) pb.gen f = (aeval pb.gen) f

Tactic:
Polynomial.aeval_def,

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
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₂ (↑(Algebra.ofId R S)) pb.gen f = eval₂ (algebraMap R S) pb.gen f
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : Ideal R
f p : R[X]
⊢ (quotMapOfEquivQuotMapCMapMk I f).symm
      ((quotMapCMapSpanMkEquivQuotMapCQuotMapMk I f).symm
        ((Ideal.Quotient.mk (Ideal.map (Ideal.Quotient.mk (Ideal.map C I)) (span {f})))
          ((Ideal.Quotient.mk (Ideal.map C I)) p))) =
    (Ideal.Quotient.mk (Ideal.map (of f) I)) ((mk f) p)

Tactic:
←
    RingHom.comp_apply,

Goal state after:
R : Type u_1
inst✝ : CommRing R
I : Ideal R
f p : R[X]
⊢ (quotMapOfEquivQuotMapCMapMk I f).symm
      ((quotMapCMapSpanMkEquivQuotMapCQuotMapMk I f).symm
        (((Ideal.Quotient.mk (Ideal.map (Ideal.Quotient.mk (Ideal.map C I)) (span {f}))).comp
            (Ideal.Quotient.mk (Ideal.map C I)))
          p)) =
    (Ideal.Quotient.mk (Ideal.map (of f) I)) ((mk f) p)
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 : IsTorsionBy K[X] (AEval K M f) p
⊢ f.IsSemisimple

Tactic:
← isTorsionBySet_singleton_iff,

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) {p}
⊢ f.IsSemisimple
Module: Mathlib.Algebra.Lie.Derivation.Basic

Goal state before:
pp: case mem
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
D1 D2 : LieDerivation R L M
s : Set L
h : Set.EqOn (⇑D1) (⇑D2) s
x✝ x : L
hx : x ∈ s
⊢ D1 x = D2 x

Tactic:
exact h hx

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

Goal state before:
pp: case add
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
D1 D2 : LieDerivation R L M
s : Set L
h : Set.EqOn (⇑D1) (⇑D2) s
x✝ x y : L
hx✝ : x ∈ LieSubalgebra.lieSpan R L s
hy✝ : y ∈ LieSubalgebra.lieSpan R L s
hx : D1 x = D2 x
hy : D1 y = D2 y
⊢ D1 (x + y) = D2 (x + y)

Tactic:
simp [hx, hy]

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

Goal state before:
pp: case lie
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
D1 D2 : LieDerivation R L M
s : Set L
h : Set.EqOn (⇑D1) (⇑D2) s
x✝ x y : L
hx✝ : x ∈ LieSubalgebra.lieSpan R L s
hy✝ : y ∈ LieSubalgebra.lieSpan R L s
hx : D1 x = D2 x
hy : D1 y = D2 y
⊢ D1 ⁅x, y⁆ = D2 ⁅x, y⁆

Tactic:
simp [hx, hy]

Goal state after:
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
pb : PowerBasis R S
I : Ideal R
g : R[X]
⊢ (pb.quotientEquivQuotientMinpolyMap I).symm
      ((Ideal.Quotient.mk (span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R pb.gen)}))
        (Polynomial.map (Ideal.Quotient.mk I) g)) =
    (Ideal.Quotient.mk (Ideal.map (algebraMap R S) I)) ((aeval pb.gen) g)

Tactic:
by
  simp [quotientEquivQuotientMinpolyMap, aeval_def]

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

Goal state before:
pp: case succ
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
k : ℕ
ih : derivedSeries R (↥I) k = comap I.incl (derivedSeriesOfIdeal R L k I)
⊢ derivedSeries R (↥I) (k + 1) = comap I.incl (derivedSeriesOfIdeal R L (k + 1) I)

Tactic:
simp only [derivedSeries_def, derivedSeriesOfIdeal_succ] at ih ⊢; rw [ih]
    exact comap_bracket_incl_of_le I (derivedSeriesOfIdeal_le_self I k)
      (derivedSeriesOfIdeal_le_self I k)

Goal state after:
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
n : ℕ
h : derivedSeries R L 1 = ⊤
⊢ derivedSeries R L n = ⊤

Tactic:
by
  cases n
  · rfl
  · rwa [derivedSeries_succ_eq_top_iff]

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

Goal state before:
pp: case h_2
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
h : IsSolvable ↥I
x✝ k✝ : ℕ
heq✝ : derivedLengthOfIdeal R L I = k✝.succ
⊢ derivedSeriesOfIdeal R L k✝ I = ⊥ ↔ I = ⊥

Tactic:
· rename_i k h
    obtain ⟨_, h₂⟩ := (derivedSeries_of_derivedLength_succ R L I k).mp h
    have h₃ : I ≠ ⊥ := by rintro rfl; apply h₂; apply derivedSeries_of_bot_eq_bot
    simp only [h₂, h₃]

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

Goal state before:
pp: case succ
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
x y : L
m : M
k : ℕ
ih : (⇑((toEnd R L M) x ∘ₗ (toEnd R L M) y))^[k] m ∈ lowerCentralSeries R L M (2 * k)
hk : 2 * k.succ = 2 * k + 1 + 1
⊢ ⁅y, (⇑((toEnd R L M) x) ∘ ⇑((toEnd R L M) y))^[k] m⁆ ∈ ⁅⊤, lowerCentralSeries R L M (2 * k)⁆

Tactic:
exact LieSubmodule.lie_mem_lie (LieSubmodule.mem_top y) ih

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

Goal state before:
pp: case refine_2.refine_2
R : Type u_1
A : Type u_2
L : 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✝¹ : CommRing A
inst✝ : Algebra R A
I : LieIdeal R L
N : LieSubmodule R L M
s : Set (A ⊗[R] M) := {m | ∃ x ∈ I, ∃ n ∈ N, 1 ⊗ₜ[R] ⁅x, n⁆ = m}
this : ⇑((TensorProduct.mk R A M) 1) '' {m | ∃ x ∈ I, ∃ n ∈ N, ⁅x, n⁆ = m} = s
x : A ⊗[R] L
hx : x ∈ Submodule.span A ↑(Submodule.map ((TensorProduct.mk R A L) 1) ↑I)
m : A ⊗[R] M
hm : m ∈ Submodule.span A ↑(Submodule.map ((TensorProduct.mk R A M) 1) ↑N)
⊢ ∀ (x y : A ⊗[R] L) (z : A ⊗[R] M),
    x ∈ Submodule.span A ↑(Submodule.map ((TensorProduct.mk R A L) 1) ↑I) →
      y ∈ Submodule.span A ↑(Submodule.map ((TensorProduct.mk R A L) 1) ↑I) →
        z ∈ Submodule.span A ↑(Submodule.map ((TensorProduct.mk R A M) 1) ↑N) →
          ⁅x, z⁆ ∈ Submodule.span A s → ⁅y, z⁆ ∈ Submodule.span A s → ⁅x + y, z⁆ ∈ Submodule.span A s

Tactic:
{

Goal state after:
case refine_2.refine_2
R : Type u_1
A : Type u_2
L : 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✝¹ : CommRing A
inst✝ : Algebra R A
I : LieIdeal R L
N : LieSubmodule R L M
s : Set (A ⊗[R] M) := {m | ∃ x ∈ I, ∃ n ∈ N, 1 ⊗ₜ[R] ⁅x, n⁆ = m}
this : ⇑((TensorProduct.mk R A M) 1) '' {m | ∃ x ∈ I, ∃ n ∈ N, ⁅x, n⁆ = m} = s
x : A ⊗[R] L
hx : x ∈ Submodule.span A ↑(Submodule.map ((TensorProduct.mk R A L) 1) ↑I)
m : A ⊗[R] M
hm : m ∈ Submodule.span A ↑(Submodule.map ((TensorProduct.mk R A M) 1) ↑N)
⊢ ∀ (x y : A ⊗[R] L) (z : A ⊗[R] M),
    x ∈ Submodule.span A ↑(Submodule.map ((TensorProduct.mk R A L) 1) ↑I) →
      y ∈ Submodule.span A ↑(Submodule.map ((TensorProduct.mk R A L) 1) ↑I) →
        z ∈ Submodule.span A ↑(Submodule.map ((TensorProduct.mk R A M) 1) ↑N) →
          ⁅x, z⁆ ∈ Submodule.span A s → ⁅y, z⁆ ∈ Submodule.span A s → ⁅x + y, z⁆ ∈ Submodule.span A s