mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.FieldTheory.Minpoly.Basic

Goal state before:
pp: A : Type u_1
B : Type u_2
B' : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
f : B →ₐ[A] B'
hf : Injective ⇑f
x : B
⊢ minpoly A (f x) = minpoly A x

Tactic:
classical
  simp_rw [minpoly, isIntegral_algHom_iff _ hf, ← Polynomial.aeval_def, aeval_algHom,
    AlgHom.comp_apply, _root_.map_eq_zero_iff f hf]

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
hx : (minpoly A x).degree = 1
⊢ IsIntegral A x

Tactic:
by_contra h

Goal state after:
A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
hx : (minpoly A x).degree = 1
h : ¬IsIntegral A x
⊢ False
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
hx : (minpoly A x).degree = 1
h : IsIntegral A x
key : x = -(algebraMap A B) ((minpoly A x).coeff 0)
⊢ x ∈ (algebraMap A B).range

Tactic:
← map_neg

Goal state after:
A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
hx : (minpoly A x).degree = 1
h : IsIntegral A x
key : x = (algebraMap A B) (-(minpoly A x).coeff 0)
⊢ x ∈ (algebraMap A B).range
Module: Mathlib.FieldTheory.Minpoly.Field

Goal state before:
pp: R : Type u_3
S : Type u_4
K : Type u_5
L : Type u_6
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Field K
inst✝⁷ : Ring L
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R K
inst✝⁴ : Algebra S L
inst✝³ : Algebra K L
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R K L
inst✝ : IsScalarTower R S L
s : S
⊢ (Polynomial.aeval ((algebraMap S L) s)) (map (algebraMap R K) (minpoly R s)) = 0

Tactic:
rw [← map_aeval_eq_aeval_map, minpoly.aeval, map_zero]

Goal state after:
case h
R : Type u_3
S : Type u_4
K : Type u_5
L : Type u_6
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Field K
inst✝⁷ : Ring L
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R K
inst✝⁴ : Algebra S L
inst✝³ : Algebra K L
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R K L
inst✝ : IsScalarTower R S L
s : S
⊢ (algebraMap K L).comp (algebraMap R K) = (algebraMap S L).comp (algebraMap R S)
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
x : B
p : A[X]
⊢ minpoly A x ∣ p ↔ ∃ a, a • minpoly A x = p

Tactic:
dvd_iff_exists_eq_mul_left,

Goal state after:
A : Type u_1
B : Type u_2
inst✝² : Field A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
p : A[X]
⊢ (∃ c, p = c * minpoly A x) ↔ ∃ a, a • minpoly A x = p
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.natDegree = 0
h0 : ¬q = 0
⊢ (Polynomial.aeval ((algebraMap A B) a)) q ≠ 0

Tactic:
rw [eq_C_of_natDegree_eq_zero hl] at h0 ⊢

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 : ¬C (q.coeff 0) = 0
⊢ (Polynomial.aeval ((algebraMap A B) a)) (C (q.coeff 0)) ≠ 0
Module: Mathlib.RingTheory.Polynomial.Quotient

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : Ideal R[X]
i : R →+* ↥((Quotient.mk I).comp C).range := ((Quotient.mk I).comp C).rangeRestrict
hi' : RingHom.ker (mapRingHom i) ≤ I
x : R[X] ⧸ I
hx' : x ∈ ((Quotient.mk I).comp C).range
hx : C ⟨x, hx'⟩ ∈ map (mapRingHom ((Quotient.mk I).comp C).rangeRestrict) I
⊢ ⟨x, hx'⟩ = 0

Tactic:
obtain ⟨y, rfl⟩ := RingHom.mem_range.1 hx'

Goal state after:
R : Type u_1
inst✝ : CommRing R
I : Ideal R[X]
i : R →+* ↥((Quotient.mk I).comp C).range := ((Quotient.mk I).comp C).rangeRestrict
hi' : RingHom.ker (mapRingHom i) ≤ I
y : R
hx' : ((Quotient.mk I).comp C) y ∈ ((Quotient.mk I).comp C).range
hx : C ⟨((Quotient.mk I).comp C) y, hx'⟩ ∈ map (mapRingHom ((Quotient.mk I).comp C).rangeRestrict) I
⊢ ⟨((Quotient.mk I).comp C) y, hx'⟩ = 0
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
this : ¬IsUnit (X ^ p - C a)
g : K[X]
hg : Irreducible g
hg' : g ∣ X ^ p - C a
⊢ g.natDegree = p

Tactic:
by_contra h

Goal state after:
K : Type u
inst✝ : Field K
p : ℕ
hp : Nat.Prime p
a : K
ha : ∀ (b : K), b ^ p ≠ a
this : ¬IsUnit (X ^ p - C a)
g : K[X]
hg : Irreducible g
hg' : g ∣ X ^ p - C a
h : ¬g.natDegree = p
⊢ False
Module: Mathlib.Algebra.Squarefree.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommMonoidWithZero R
inst✝ : WfDvdMonoid R
r : R
hr : ∃ x, Irreducible x
⊢ Squarefree r ↔ ∀ (x : R), Irreducible x → ¬x * x ∣ r

Tactic:
by
  rw [irreducible_sq_not_dvd_iff_eq_zero_and_no_irreducibles_or_squarefree, ← not_exists]
  simp only [hr, not_true, false_or, and_false]

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

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

Tactic:
have := ha.1
        contradiction

Goal state after:
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: case neg
R : Type u
inst✝¹ : CommRing R
inst✝ : Nontrivial R
p : R[X]
hsep : p.Separable
x : R
hp : ¬p = 0
⊢ multiplicity (X - C x) p ≤ 1

Tactic:
← Nat.cast_le (α := ℕ∞),

Goal state after:
case neg
R : Type u
inst✝¹ : CommRing R
inst✝ : Nontrivial R
p : R[X]
hsep : p.Separable
x : R
hp : ¬p = 0
⊢ ↑(multiplicity (X - C x) p) ≤ ↑1
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: case h.inr
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
h1 : ¬f.Separable
g : F[X]
hg : Irreducible g
hgf : (expand F p) g = f
⊢ ∃ n g, g.Separable ∧ (expand F (p ^ n)) g = f

Tactic:
rcases N with - | N

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

case h.inr.succ
F : Type u
inst✝ : Field F
p : ℕ
HF : CharP F p
hp : Nat.Prime p
f : F[X]
hf : Irreducible f
h1 : ¬f.Separable
g : F[X]
hg : Irreducible g
hgf : (expand F p) g = f
N : ℕ
ih : ∀ m < N + 1, ∀ {f : F[X]}, Irreducible f → f.natDegree = m → ∃ n g, g.Separable ∧ (expand F (p ^ n)) g = f
hn : f.natDegree = N + 1
⊢ ∃ n g, g.Separable ∧ (expand F (p ^ n)) g = f
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
inst✝¹ : Module.Finite R M
inst✝ : Free R M
f : M →ₗ[R] M
⊢ IsUnit f ↔ IsUnit (LinearMap.det f)

Tactic:
by
  let b := Module.Free.chooseBasis R M
  rw [← isUnit_toMatrix_iff b, ← det_toMatrix b, Matrix.isUnit_iff_isUnit_det (toMatrix b b f)]

Goal state after:
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
p : 𝕜[X]
p_monic : p.Monic
hp : (aeval a) p = 0
⊢ False

Tactic:
refine p_monic.ne_zero (Ideal.mem_bot.mp ?_)

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
p : 𝕜[X]
p_monic : p.Monic
hp : (aeval a) p = 0
⊢ p ∈ ⊥
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 = 0

Tactic:
annIdealGenerator_eq_zero_iff,

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
⊢ annIdeal 𝕜 a = ⊥
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
f : R[X]
inst✝ : IsDomain R
h : f.degree ≠ 0
⊢ Nontrivial (AdjoinRoot f)

Tactic:
simp only [AdjoinRoot, Quotient.nontrivial_iff, Ne, span_singleton_eq_top,
    Polynomial.isUnit_iff, not_exists, not_and]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
f : R[X]
inst✝ : IsDomain R
h : f.degree ≠ 0
⊢ ∀ (x : R), IsUnit x → ¬C x = f
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: A₁ : Type u_1
B₁ : Type u_2
A₂ : Type u_3
B₂ : Type u_4
inst✝⁵ : Field A₁
inst✝⁴ : Ring B₁
inst✝³ : Field A₂
inst✝² : Ring B₂
inst✝¹ : Algebra A₁ B₁
inst✝ : Algebra A₂ B₂
e₁ : A₁ ≃+* A₂
e₂ : B₁ ≃+* B₂
he : (algebraMap A₂ B₂).comp ↑e₁ = (↑e₂).comp (algebraMap A₁ B₁)
x✝ : B₁
h : IsSeparable A₁ x✝
this✝¹ : Algebra A₁ A₂ := e₁.toRingHom.toAlgebra
this✝ : Algebra A₂ B₁ :=
  let __src := (algebraMap A₁ B₁).comp e₁.symm.toRingHom;
  { smul := fun a b ↦ ((algebraMap A₁ B₁).comp e₁.symm.toRingHom) a * b,
    algebraMap := (algebraMap A₁ B₁).comp e₁.symm.toRingHom, commutes' := ⋯, smul_def' := ⋯ }
this : IsScalarTower A₁ A₂ B₁
x : A₂
⊢ e₂.toFun ((algebraMap A₂ B₁) x) = (algebraMap A₂ B₂) x

Tactic:
simpa [RingHom.algebraMap_toAlgebra] using! DFunLike.congr_fun he.symm (e₁.symm x)

Goal state after:
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
f : R[X]
inst✝ : CommRing S
i : R →+* S
a : S
h : eval₂ i a f = 0
x : R
⊢ (lift i a h) ((of f) x) = i x

Tactic:
← mk_C x,

Goal state after:
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
f : R[X]
inst✝ : CommRing S
i : R →+* S
a : S
h : eval₂ i a f = 0
x : R
⊢ (lift i a h) ((mk f) (C x)) = i x
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
u : ι → M
i : ι
c : R
x : M
⊢ ((e.toMatrix u).updateCol i ⇑(c • e.repr x)).det = c * ((e.toMatrix u).updateCol i ⇑(e.repr x)).det

Tactic:
apply det_updateCol_smul

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
v : ι → M
hli : LinearIndependent R v
hsp : ⊤ ≤ span R (Set.range v)
i : ι
⊢ e.det v • (Basis.mk hli hsp).coord i = (↑e.det).toLinearMap v i

Tactic:
apply (Basis.mk hli hsp).ext
  intro k
  rcases eq_or_ne k i with (rfl | hik) <;>
    simp only [smul_eq_mul, coe_mk, LinearMap.smul_apply,
      MultilinearMap.toLinearMap_apply]
  · rw [mk_coord_apply_eq, mul_one, update_eq_self]
    congr
  · rw [mk_coord_apply_ne hik, mul_zero, eq_comm]
    exact e.det.map_eq_zero_of_eq _ (by simp [hik]) hik

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
g : R[X]
inst✝ : Field K
f : K[X]
hf : f ≠ 0
⊢ Basis (Fin f.natDegree) K (AdjoinRoot f)

Tactic:
let f' := f * C f.leadingCoeff⁻¹
  have deg_f' : f'.natDegree = f.natDegree := by
    rw [natDegree_mul hf, natDegree_C, add_zero]
    · rwa [Ne, C_eq_zero, inv_eq_zero, leadingCoeff_eq_zero]
  have minpoly_eq : minpoly K (root f) = f' := minpoly_root hf
  apply Basis.mk (v := fun i : Fin f.natDegree ↦ root f ^ i.val)
  · rw [← deg_f', ← minpoly_eq]
    exact linearIndependent_pow (root f)
  · rintro y -
    rw [← deg_f', ← minpoly_eq]
    apply (isIntegral_root hf).mem_span_pow
    obtain ⟨g⟩ := y
    use g
    rw [aeval_eq]
    rfl

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

Tactic:
have h₄ : a ^ (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
⊢ exp (a + b) = exp a * exp b
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 : (aeval f) p = 0
⊢ f.IsSemisimple

Tactic:
rw [← RingHom.mem_ker, ← AEval.annihilator_eq_ker_aeval (M := M), mem_annihilator,
      ← IsTorsionBy, ← isTorsionBySet_singleton_iff, isTorsionBySet_iff_is_torsion_by_span] at hpf
  let R := K[X] ⧸ Ideal.span {p}
  have : IsReduced R :=
    (Ideal.isRadical_iff_quotient_reduced _).mp (isRadical_iff_span_singleton.mp hp.isRadical)
  have : FiniteDimensional K R := (AdjoinRoot.powerBasis hp.ne_zero).finite
  have : IsArtinianRing R := .of_finite K R
  have : IsSemisimpleRing R := IsArtinianRing.isSemisimpleRing_of_isReduced R
  let : Module R (AEval' f) := Module.IsTorsionBySet.module hpf
  let e : AEval' f →ₛₗ[Ideal.Quotient.mk (Ideal.span {p})] AEval' f :=
    { AddMonoidHom.id _ with map_smul' := fun _ _ ↦ rfl }
  exact (e.isSemisimpleModule_iff_of_bijective bijective_id).mpr inferInstance

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

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

Tactic:
rw [n.choose_symm_of_eq_add (mem_antidiagonal.1 hij).symm]

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

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
D1 : LieDerivation R L L
⊢ ∀ (y : LieDerivation R L L), ↑(D1 + y) = ↑D1 + ↑y

Tactic:
D2

Goal state after:
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
D1 D2 : LieDerivation R L L
⊢ ↑(D1 + D2) = ↑D1 + ↑D2
Module: Mathlib.Algebra.Lie.Derivation.Basic

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
D1 : R
⊢ ∀ (x : LieDerivation R L L), ↑(D1 • x) = (RingHom.id R) D1 • ↑x

Tactic:
D2

Goal state after:
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
D1 : R
D2 : LieDerivation R L L
⊢ ↑(D1 • D2) = (RingHom.id R) D1 • ↑D2
Module: Mathlib.Algebra.Lie.Derivation.Basic

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
D1 : LieDerivation R L L
⊢ ∀ {y : LieDerivation R L L}, ↑⁅D1, y⁆ = ⁅↑D1, ↑y⁆

Tactic:
D2

Goal state after:
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
D1 D2 : LieDerivation R L L
⊢ ↑⁅D1, D2⁆ = ⁅↑D1, ↑D2⁆
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: n : ℕ
IH :
  ∀ m < n,
    ∀ {R : Type u} [inst : CommRing R] [Nontrivial R] {p : R[X]},
      p.Monic →
        p.natDegree = m →
          ∃ S x x_1,
            ∃ (_ : Module.Finite R S) (_ : Free R S) (_ : Nontrivial S), (Polynomial.map (algebraMap R S) p).Splits
R : Type u
inst✝¹ : CommRing R
inst✝ : Nontrivial R
p : R[X]
hp : p.Monic
hn : p.natDegree = n
hpu : ¬IsUnit p
⊢ X - C (AdjoinRoot.root p) ∣ Polynomial.map (algebraMap R (AdjoinRoot p)) p

Tactic:
simp [dvd_iff_isRoot, -AdjoinRoot.algebraMap_eq]

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

Goal state before:
pp: A : Type u_1
inst✝¹ : Ring A
inst✝ : Module ℚ A
a b : A
h₁ : Commute a b
n₁ : ℕ
hn₁ : a ^ n₁ = 0
n₂ : ℕ
hn₂ : b ^ n₂ = 0
N : ℕ := max n₁ n₂
h₄ : a ^ (N + 1) = 0
h₅ : b ^ (N + 1) = 0
R2N : Finset ℕ := range (2 * N + 1)
hR2N : R2N = range (2 * N + 1)
RN : Finset ℕ := range (N + 1)
hRN : RN = range (N + 1)
s₁ :
  ∑ i ∈ R2N, (↑i !)⁻¹ • (a + b) ^ i =
    ∑ ij ∈ R2N ×ˢ R2N with ij.1 + ij.2 ≤ 2 * N, ((↑ij.1!)⁻¹ * (↑ij.2!)⁻¹) • (a ^ ij.1 * b ^ ij.2)
i : ℕ × ℕ
hi : i ∈ R2N ×ˢ R2N ∧ ¬i.1 + i.2 ≤ 2 * N
x✝ : N + 1 ≤ i.1 ∨ i.1 < N + 1
⊢ ((↑i.1!)⁻¹ * (↑i.2!)⁻¹) • (a ^ i.1 * b ^ i.2) = 0

Tactic:
cases le_or_gt (N + 1) i.1 with

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

Goal state before:
pp: A : Type u_1
inst✝¹ : Ring A
inst✝ : Module ℚ A
a b : A
h₁ : Commute a b
n₁ : ℕ
hn₁ : a ^ n₁ = 0
n₂ : ℕ
hn₂ : b ^ n₂ = 0
N : ℕ := max n₁ n₂
h₄ : a ^ (N + 1) = 0
h₅ : b ^ (N + 1) = 0
R2N : Finset ℕ := range (2 * N + 1)
hR2N : R2N = range (2 * N + 1)
RN : Finset ℕ := range (N + 1)
hRN : RN = range (N + 1)
s₁ : ∑ i ∈ R2N, (↑i !)⁻¹ • (a + b) ^ i = ∑ x ∈ R2N ×ˢ R2N, ((↑x.1!)⁻¹ * (↑x.2!)⁻¹) • (a ^ x.1 * b ^ x.2)
z₁ : ∑ ij ∈ R2N ×ˢ R2N with ¬ij.1 + ij.2 ≤ 2 * N, ((↑ij.1!)⁻¹ * (↑ij.2!)⁻¹) • (a ^ ij.1 * b ^ ij.2) = 0
split₁ :
  ∑ x ∈ R2N ×ˢ R2N with x.1 + x.2 ≤ 2 * N, ((↑x.1!)⁻¹ * (↑x.2!)⁻¹) • (a ^ x.1 * b ^ x.2) =
    ∑ x ∈ R2N ×ˢ R2N, ((↑x.1!)⁻¹ * (↑x.2!)⁻¹) • (a ^ x.1 * b ^ x.2)
i : ℕ × ℕ
hi : i ∈ R2N ×ˢ R2N ∧ (i.1 ≤ N → N < i.2)
x✝ : N + 1 ≤ i.1 ∨ i.1 < N + 1
⊢ ((↑i.1!)⁻¹ * (↑i.2!)⁻¹) • (a ^ i.1 * b ^ i.2) = 0

Tactic:
cases le_or_gt (N + 1) i.1 with

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

Goal state before:
pp: R : Type u_4
B : Type u_5
inst✝⁵ : CommRing R
inst✝⁴ : NonUnitalNonAssocRing B
inst✝³ : Module R B
inst✝² : SMulCommClass R B B
inst✝¹ : IsScalarTower R B B
inst✝ : Module ℚ B
D : B →ₗ[R] B
h_der : ∀ (x y : B), D (x * y) = x * D y + D x * y
h_nil : IsNilpotent D
x y : B
DL : End R (B ⊗[R] B) := LinearMap.lTensor B D
DR : End R (B ⊗[R] B) := LinearMap.rTensor B D
h_nilL : IsNilpotent DL
h_nilR : IsNilpotent DR
h_comm : Commute DL DR
m : B ⊗[R] B →ₗ[R] B := LinearMap.mul' R B
hm : m = LinearMap.mul' R B
this : exp D ∘ₗ m = m ∘ₗ exp (DL + DR)
⊢ (exp D) (x * y) = m ((exp (DL + DR)) (x ⊗ₜ[R] y))

Tactic:
simpa using! LinearMap.congr_fun this (x ⊗ₜ[R] y)

Goal state after:
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'
N N₁ N₂ : LieSubmodule R L M
t : R
m : M
hm : m ∈ {m | ∀ (x : L), ⁅x, m⁆ ∈ N}
x : L
⊢ ⁅x, t • m⁆ ∈ N

Tactic:
by rw [lie_smul]; exact N.smul_mem' t (hm x)

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

Goal state before:
pp: R : Type u₁
L : Type u₂
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : Subsingleton L
⊢ IsEngelian R L

Tactic:
intro M _i1 _i2 _i3 _i4 _h

Goal state after:
R : Type u₁
L : Type u₂
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : Subsingleton L
M : Type u_1
_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
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:
{ intros; simp [add_mem, Submodule.smul_mem, *] }

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

Goal state before:
pp: case refine_2.refine_3
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 : A ⊗[R] L) (y 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 M) 1) ↑N) →
        z ∈ Submodule.span A ↑(Submodule.map ((TensorProduct.mk R A M) 1) ↑N) →
          ⁅x, y⁆ ∈ Submodule.span A s → ⁅x, z⁆ ∈ Submodule.span A s → ⁅x, y + z⁆ ∈ Submodule.span A s

Tactic:
{ intros; simp [add_mem, Submodule.smul_mem, *] }

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

Goal state before:
pp: case refine_2.refine_4
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)
⊢ ∀ (r : A) (x : A ⊗[R] L) (y : 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 M) 1) ↑N) →
        ⁅x, y⁆ ∈ Submodule.span A s → ⁅r • x, y⁆ ∈ Submodule.span A s

Tactic:
{ intros; simp [add_mem, Submodule.smul_mem, *] }

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

Goal state before:
pp: case refine_2.refine_5
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)
⊢ ∀ (r : A) (x : A ⊗[R] L) (y : 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 M) 1) ↑N) →
        ⁅x, y⁆ ∈ Submodule.span A s → ⁅x, r • y⁆ ∈ Submodule.span A s

Tactic:
{ intros; simp [add_mem, Submodule.smul_mem, *] }

Goal state after: