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

Goal state before:
pp: case inl
A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
p : A[X]
hm : p.Monic
hp : (Polynomial.aeval x) p = 0
hl : ∀ (q : A[X]), q.degree < p.degree → q = 0 ∨ (Polynomial.aeval x) q ≠ 0
a✝ : Nontrivial A
hx : IsIntegral A x
h : minpoly A x %ₘ p = 0
⊢ p = minpoly A x

pp: case inr
A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
p : A[X]
hm : p.Monic
hp : (Polynomial.aeval x) p = 0
hl : ∀ (q : A[X]), q.degree < p.degree → q = 0 ∨ (Polynomial.aeval x) q ≠ 0
a✝ : Nontrivial A
hx : IsIntegral A x
h : (Polynomial.aeval x) (minpoly A x %ₘ p) ≠ 0
⊢ p = minpoly A x

Tactic:
swap

Goal state after:
case inr
A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
p : A[X]
hm : p.Monic
hp : (Polynomial.aeval x) p = 0
hl : ∀ (q : A[X]), q.degree < p.degree → q = 0 ∨ (Polynomial.aeval x) q ≠ 0
a✝ : Nontrivial A
hx : IsIntegral A x
h : (Polynomial.aeval x) (minpoly A x %ₘ p) ≠ 0
⊢ p = minpoly A x

case inl
A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
p : A[X]
hm : p.Monic
hp : (Polynomial.aeval x) p = 0
hl : ∀ (q : A[X]), q.degree < p.degree → q = 0 ∨ (Polynomial.aeval x) q ≠ 0
a✝ : Nontrivial A
hx : IsIntegral A x
h : minpoly A x %ₘ p = 0
⊢ p = minpoly A x
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]
pmonic : p.Monic
hp : (Polynomial.aeval x) p = 0
pmin : ∀ (q : A[X]), q.Monic → (Polynomial.aeval x) q = 0 → p.degree ≤ q.degree
hx : IsIntegral A x
hnz : ¬minpoly A x - p = 0
⊢ False

Tactic:
apply degree_le_of_ne_zero A x hnz (by simp [hp]) |>.not_gt

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]
pmonic : p.Monic
hp : (Polynomial.aeval x) p = 0
pmin : ∀ (q : A[X]), q.Monic → (Polynomial.aeval x) q = 0 → p.degree ≤ q.degree
hx : IsIntegral A x
hnz : ¬minpoly A x - p = 0
⊢ (minpoly A x - p).degree < (minpoly A x).degree
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]
monic : p.Monic
hp0 : (Polynomial.aeval x) p = 0
n : ℕ
hpn : p.degree = ↑n
ind : LinearIndependent A fun i ↦ x ^ ↑i
q : A[X]
lt : q.degree < p.degree
ne : ¬q = 0
hq : (Polynomial.aeval x) q = 0
i : ℕ
⊢ q.coeff i = coeff 0 i

Tactic:
rw [q.as_sum_range' _ ((natDegree_lt_iff_degree_lt ne).mpr (hpn ▸ lt))] at hq

Goal state after:
A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
p : A[X]
monic : p.Monic
hp0 : (Polynomial.aeval x) p = 0
n : ℕ
hpn : p.degree = ↑n
ind : LinearIndependent A fun i ↦ x ^ ↑i
q : A[X]
lt : q.degree < p.degree
ne : ¬q = 0
hq : (Polynomial.aeval x) (∑ i ∈ Finset.range n, (monomial i) (q.coeff i)) = 0
i : ℕ
⊢ q.coeff i = coeff 0 i
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
hx : IsIntegral A x
ndeg_eq_zero : (minpoly A x).natDegree = 0
⊢ minpoly A x = 1

Tactic:
eq_C_of_natDegree_eq_zero ndeg_eq_zero

Goal state after:
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : Ring B
inst✝¹ : Algebra A B
x : B
inst✝ : Nontrivial B
hx : IsIntegral A x
ndeg_eq_zero : (minpoly A x).natDegree = 0
⊢ C ((minpoly A x).coeff 0) = 1
Module: Mathlib.FieldTheory.Minpoly.Field

Goal state before:
pp: case pos.refine_1
A : Type u_1
inst✝² : Field A
B : Type u_3
inst✝¹ : CommRing B
inst✝ : Algebra A B
x : B
a : A
hx : IsIntegral A x
⊢ (Polynomial.aeval (x + (algebraMap A B) a)) ((minpoly A x).comp (X - C a)) = 0

pp: case pos.refine_2
A : Type u_1
inst✝² : Field A
B : Type u_3
inst✝¹ : CommRing B
inst✝ : Algebra A B
x : B
a : A
hx : IsIntegral A x
q : A[X]
qmo : q.Monic
hq : (Polynomial.aeval (x + (algebraMap A B) a)) q = 0
⊢ ((minpoly A x).comp (X - C a)).degree ≤ q.degree

Tactic:
· simp [aeval_comp]

Goal state after:
case pos.refine_2
A : Type u_1
inst✝² : Field A
B : Type u_3
inst✝¹ : CommRing B
inst✝ : Algebra A B
x : B
a : A
hx : IsIntegral A x
q : A[X]
qmo : q.Monic
hq : (Polynomial.aeval (x + (algebraMap A B) a)) q = 0
⊢ ((minpoly A x).comp (X - C a)).degree ≤ q.degree
Module: Mathlib.FieldTheory.Minpoly.Field

Goal state before:
pp: case pos.refine_1
A : Type u_1
inst✝² : Field A
B : Type u_3
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
hx : IsIntegral A x
⊢ (Polynomial.aeval (-x)) ((-1) ^ (minpoly A x).natDegree * (minpoly A x).comp (-X)) = 0

pp: case pos.refine_2
A : Type u_1
inst✝² : Field A
B : Type u_3
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
hx : IsIntegral A x
q : A[X]
qmo : q.Monic
hq : (Polynomial.aeval (-x)) q = 0
⊢ ((-1) ^ (minpoly A x).natDegree * (minpoly A x).comp (-X)).degree ≤ q.degree

Tactic:
· simp [aeval_comp]

Goal state after:
case pos.refine_2
A : Type u_1
inst✝² : Field A
B : Type u_3
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
hx : IsIntegral A x
q : A[X]
qmo : q.Monic
hq : (Polynomial.aeval (-x)) q = 0
⊢ ((-1) ^ (minpoly A x).natDegree * (minpoly A x).comp (-X)).degree ≤ q.degree
Module: Mathlib.FieldTheory.Minpoly.Field

Goal state before:
pp: case refine_2
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : CommRing L
inst✝¹ : IsDomain L
inst✝ : Algebra K L
σ : L ≃ₐ[K] L
hσ : IsOfFinOrder σ
⊢ ∀ (q : K[X]), q.Monic → (Polynomial.aeval σ.toLinearMap) q = 0 → (X ^ orderOf σ - C 1).degree ≤ q.degree

Tactic:
intro q hq hs
    rw [degree_eq_natDegree hq.ne_zero, degree_X_pow_sub_C hσ.orderOf_pos, Nat.cast_le, ← not_lt]
    intro H
    rw [aeval_eq_sum_range' H, ← Fin.sum_univ_eq_sum_range] at hs
    simp_rw [← AlgEquiv.pow_toLinearMap] at hs
    apply hq.ne_zero
    simpa using Fintype.linearIndependent_iff.mp
      (((linearIndependent_algHom_toLinearMap' K L L).comp _ AlgEquiv.coe_toAlgHom_injective).comp _
        (Subtype.val_injective.comp ((finEquivPowers hσ).injective)))
      (q.coeff ∘ (↑)) hs ⟨_, H⟩

Goal state after:
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 : ℕ
this : (Set.range fun i ↦ x ^ ↑i) = (fun i ↦ x ^ i) '' ↑(Finset.range d)
⊢ y ∈ Submodule.span R (Set.range fun i ↦ x ^ ↑i) ↔ ∃ f, f.degree < ↑d ∧ y = (aeval x) f

Tactic:
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.Polynomial.Quotient

Goal state before:
pp: case neg
R : Type u_1
inst✝ : CommRing R
I : Ideal R
a : R[X]
ha : a ∈ map C I
n : ℕ
x✝ : n ∈ a.support
m : ℕ
h : ¬m = 0
⊢ (if m = 0 then (Quotient.mk I) (a.coeff n) else 0) = coeff 0 m

Tactic:
simp [h]

Goal state after:
Module: Mathlib.RingTheory.PowerBasis

Goal state before:
pp: case pos
S : Type u_2
inst✝² : Ring S
K : Type u_6
inst✝¹ : Field K
inst✝ : Algebra K S
x : S
h : IsIntegral K x
⊢ LinearIndependent K fun i ↦ x ^ ↑i

pp: case neg
S : Type u_2
inst✝² : Ring S
K : Type u_6
inst✝¹ : Field K
inst✝ : Algebra K S
x : S
h : ¬IsIntegral K x
⊢ LinearIndependent K fun i ↦ x ^ ↑i

Tactic:
swap

Goal state after:
case neg
S : Type u_2
inst✝² : Ring S
K : Type u_6
inst✝¹ : Field K
inst✝ : Algebra K S
x : S
h : ¬IsIntegral K x
⊢ LinearIndependent K fun i ↦ x ^ ↑i

case pos
S : Type u_2
inst✝² : Ring S
K : Type u_6
inst✝¹ : Field K
inst✝ : Algebra K S
x : S
h : IsIntegral K x
⊢ LinearIndependent K fun i ↦ x ^ ↑i
Module: Mathlib.RingTheory.Norm.Defs

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : Ring S
inst✝¹ : Algebra R S
ι : Type w
inst✝ : Fintype ι
b : Basis ι R S
x : R
this : DecidableEq ι
⊢ ((toMatrix b b) ((lmul R S) ((algebraMap R S) x))).det = x ^ Fintype.card ι

Tactic:
lmul_algebraMap

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : Ring S
inst✝¹ : Algebra R S
ι : Type w
inst✝ : Fintype ι
b : Basis ι R S
x : R
this : DecidableEq ι
⊢ ((toMatrix b b) ((lsmul R R S) x)).det = x ^ Fintype.card ι
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
r : R
⊢ IsCoprime (C r) 0 ↔ IsUnit r

Tactic:
isCoprime_zero_right,

Goal state after:
R : Type u
inst✝ : CommSemiring R
r : R
⊢ IsUnit (C r) ↔ IsUnit r
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
    · rw [natDegree_eq_zero_iff_degree_le_zero, degree_le_zero_iff] at hn
      rw [hn, separable_C, isUnit_iff_ne_zero, Classical.not_not] at h1
      have hf0 : f ≠ 0 := hf.ne_zero
      rw [h1, C_0] at hn
      exact absurd hn hf0
    have hg1 : g.natDegree * p = N.succ := by rwa [← natDegree_expand, hgf]
    have hg2 : g.natDegree ≠ 0 := by
      intro this
      rw [this, zero_mul] at hg1
      cases hg1
    have hg3 : g.natDegree < N.succ := by
      rw [← mul_one g.natDegree, ← hg1]
      exact Nat.mul_lt_mul_of_pos_left hp.one_lt hg2.bot_lt
    rcases ih _ hg3 hg rfl with ⟨n, g, hg4, rfl⟩
    refine ⟨n + 1, g, hg4, ?_⟩
    rw [← hgf, expand_expand, pow_succ']

Goal state after:
Module: Mathlib.FieldTheory.Separable

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

Tactic:
isCoprime_zero_right,

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

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
p : ℕ
inst✝¹ : ExpChar R p
f : R[X]
inst✝ : DecidableEq R
⊢ Finset.image (⇑(frobenius R p)) ((expand R p) f).roots.toFinset ⊆ f.roots.toFinset

Tactic:
rw [← iterateFrobenius_one]
  convert! ← roots_expand_pow_image_iterateFrobenius_subset p 1 f
  apply pow_one

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
inst✝¹ : IsDomain R
inst✝ : Free R M
f : M →ₗ[R] M
hf : LinearMap.det f = 0
h : f.range = ⊤
⊢ False

Tactic:
obtain ⟨g, hg⟩ := f.exists_rightInverse_of_surjective h

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsDomain R
inst✝ : Free R M
f : M →ₗ[R] M
hf : LinearMap.det f = 0
h : f.range = ⊤
g : M →ₗ[R] M
hg : f ∘ₗ g = id
⊢ False
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:
rootSet_def,

Goal state after:
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.aroots K).toFinset = p.natDegree
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: F : Type u
inst✝² : Field F
K : Type v
inst✝¹ : Field K
inst✝ : Algebra F K
f : F[X]
hf : f ≠ 0
h : (map (algebraMap F K) f).Splits
⊢ Fintype.card ↑(f.rootSet K) = f.natDegree ↔ f.Separable

Tactic:
rootSet_def,

Goal state after:
F : Type u
inst✝² : Field F
K : Type v
inst✝¹ : Field K
inst✝ : Algebra F K
f : F[X]
hf : f ≠ 0
h : (map (algebraMap F K) f).Splits
⊢ Fintype.card ↑↑(f.aroots K).toFinset = f.natDegree ↔ f.Separable
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 ι
f : M ≃ₗ[R] M'
v : Basis ι R M
v' : Basis ι R M'
⊢ IsUnit ((toMatrix v v') ↑f).det

Tactic:
by
  apply isUnit_det_of_left_inverse
  simpa using (LinearMap.toMatrix_comp v v' v f.symm f).symm

Goal state after:
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: S : Type u_2
inst✝⁴ : CommRing S
K : Type u_4
L : Type u_5
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K S
inst✝ : Algebra K L
pb : PowerBasis K S
h_sep : IsSeparable K pb.gen
h_splits : (Polynomial.map (algebraMap K L) (minpoly K pb.gen)).Splits
⊢ #((minpoly K pb.gen).aroots L).toFinset = (Polynomial.map (algebraMap K L) (minpoly K pb.gen)).roots.card

Tactic:
Multiset.toFinset_card_of_nodup

Goal state after:
S : Type u_2
inst✝⁴ : CommRing S
K : Type u_4
L : Type u_5
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K S
inst✝ : Algebra K L
pb : PowerBasis K S
h_sep : IsSeparable K pb.gen
h_splits : (Polynomial.map (algebraMap K L) (minpoly K pb.gen)).Splits
⊢ ((minpoly K pb.gen).aroots L).card = (Polynomial.map (algebraMap K L) (minpoly K pb.gen)).roots.card

S : Type u_2
inst✝⁴ : CommRing S
K : Type u_4
L : Type u_5
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K S
inst✝ : Algebra K L
pb : PowerBasis K S
h_sep : IsSeparable K pb.gen
h_splits : (Polynomial.map (algebraMap K L) (minpoly K pb.gen)).Splits
⊢ ((minpoly K pb.gen).aroots L).Nodup
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
f : M →ₗ[R] M'
v : Basis ι R M
v' : Basis ι R M'
h : IsUnit ((toMatrix v v') f).det
x : M
⊢ ((toLin v v) (((toMatrix v v') f)⁻¹ * (toMatrix v v') f)) x = x

Tactic:
simp [h]

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
M' : Type u_3
inst✝³ : AddCommGroup M'
inst✝² : Module R M'
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
e : Basis ι R M
f : M →ₗ[R] M'
v : Basis ι R M
v' : Basis ι R M'
h : IsUnit ((toMatrix v v') f).det
x : M'
⊢ ((toLin v' v') ((toMatrix v v') f * ((toMatrix v v') f)⁻¹)) x = x

Tactic:
simp [h]

Goal state after:
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: case e'_2
R : Type u_1
inst✝ : CommRing R
r : R
⊢ (of (C r * X - 1)) r * root (C r * X - 1) = eval₂ (of (C r * X - 1)) (root (C r * X - 1)) (C r * X)

Tactic:
simp only [eval₂_mul, eval₂_C, eval₂_X, eval₂_one]

Goal state after:
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: case e'_3
R : Type u_1
inst✝ : CommRing R
r : R
⊢ 1 = eval₂ (of (C r * X - 1)) (root (C r * X - 1)) 1

Tactic:
simp only [eval₂_mul, eval₂_C, eval₂_X, eval₂_one]

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
μ : R
this : ∀ (p : Submodule R M), p ≤ Submodule.comap (f - (algebraMap R (End R M)) μ) p ↔ p ≤ Submodule.comap f p
⊢ (f - (algebraMap R (End R M)) μ).IsFinitelySemisimple ↔ f.IsFinitelySemisimple

Tactic:
isFinitelySemisimple_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
μ : R
this : ∀ (p : Submodule R M), p ≤ Submodule.comap (f - (algebraMap R (End R M)) μ) p ↔ p ≤ Submodule.comap f p
⊢ (∀ p ∈ (f - (algebraMap R (End R M)) μ).invtSubmodule,
      Module.Finite R ↥p →
        ∀ q ∈ (f - (algebraMap R (End R M)) μ).invtSubmodule,
          q ≤ p → ∃ r ≤ p, r ∈ (f - (algebraMap R (End R M)) μ).invtSubmodule ∧ Disjoint q r ∧ q ⊔ r = p) ↔
    ∀ p ∈ f.invtSubmodule,
      Module.Finite R ↥p → ∀ q ∈ f.invtSubmodule, q ≤ p → ∃ r ≤ p, r ∈ f.invtSubmodule ∧ Disjoint q r ∧ q ⊔ r = 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 : IsTorsionBySet K[X] (AEval K M f) ↑(Ideal.span {p})
R : Type u_3 := K[X] ⧸ Ideal.span {p}
this✝² : IsReduced R
this✝¹ : FiniteDimensional K R
this✝ : IsArtinianRing R
this : IsSemisimpleRing R
⊢ f.IsSemisimple

Tactic:
let : Module R (AEval' f) := Module.IsTorsionBySet.module hpf

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}
this✝³ : IsReduced R
this✝² : FiniteDimensional K R
this✝¹ : IsArtinianRing R
this✝ : IsSemisimpleRing R
this : Module R (AEval' f) := hpf.module
⊢ f.IsSemisimple
Module: Mathlib.Dynamics.Newton

Goal state before:
pp: case e'_4
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : R[X]
x : S
h : IsNilpotent ((aeval x) P)
h' : IsUnit ((aeval x) (derivative P))
n : ℕ
ih : (aeval x) P ^ 2 ^ n ∣ (aeval (P.newtonMap^[n] x)) P
d : S
hd :
  (aeval
        (P.newtonMap^[n] x +
          -Ring.inverse ((aeval (P.newtonMap^[n] x)) (derivative P)) * (aeval (P.newtonMap^[n] x)) P))
      P =
    (aeval (P.newtonMap^[n] x)) P +
        eval (P.newtonMap^[n] x) (derivative (map (algebraMap R S) P)) *
          (-Ring.inverse ((aeval (P.newtonMap^[n] x)) (derivative P)) * (aeval (P.newtonMap^[n] x)) P) +
      d * (-Ring.inverse ((aeval (P.newtonMap^[n] x)) (derivative P)) * (aeval (P.newtonMap^[n] x)) P) ^ 2
this : IsUnit ((aeval (P.newtonMap^[n] x)) (derivative P))
⊢ (aeval (P.newtonMap^[n] x)) P +
      eval (P.newtonMap^[n] x) (derivative (map (algebraMap R S) P)) *
        (-Ring.inverse ((aeval (P.newtonMap^[n] x)) (derivative P)) * (aeval (P.newtonMap^[n] x)) P) =
    0

Tactic:
rw [derivative_map, eval_map_algebraMap, ← mul_assoc, mul_neg, Ring.mul_inverse_cancel _ this,
        neg_mul, one_mul, add_neg_cancel]

Goal state after:
Module: Mathlib.Dynamics.Newton

Goal state before:
pp: case refine_2
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : R[X]
x : S
h : IsNilpotent ((aeval x) P)
h' : IsUnit ((aeval x) (derivative P))
r₁ r₂ : S
x✝¹ : IsNilpotent (r₁ - x) ∧ (aeval r₁) P = 0
x✝ : IsNilpotent (r₂ - x) ∧ (aeval r₂) P = 0
hr₁ : IsNilpotent (r₁ - x)
hr₁' : (aeval r₁) P = 0
hr₂ : IsNilpotent (r₂ - x)
hr₂' : (aeval r₂) P = 0
⊢ r₁ = r₂

Tactic:
· -- Uniqueness
    have ⟨u, hu⟩ := binomExpansion (P.map (algebraMap R S)) r₁ (r₂ - r₁)
    suffices IsUnit (aeval r₁ (derivative P) + u * (r₂ - r₁)) by
      rwa [derivative_map, eval_map_algebraMap, eval_map_algebraMap, eval_map_algebraMap,
        add_sub_cancel, hr₂', hr₁', zero_add, pow_two, ← mul_assoc, ← add_mul, eq_comm,
        this.mul_right_eq_zero, sub_eq_zero, eq_comm] at hu
    have : IsUnit (aeval r₁ (derivative P)) :=
      isUnit_aeval_of_isUnit_aeval_of_isNilpotent_sub h' hr₁
    rw [← sub_sub_sub_cancel_right r₂ r₁ x]
    refine IsNilpotent.isUnit_add_left_of_commute ?_ this (Commute.all _ _)
    exact (Commute.all _ _).isNilpotent_mul_left <| (Commute.all _ _).isNilpotent_sub hr₂ hr₁

Goal state after:
Module: Mathlib.Algebra.Ring.Divisibility.Lemmas

Goal state before:
pp: case inl
R : Type u_1
inst✝¹ : Ring R
inst✝ : LinearOrder R
x y : R
h : |x| = x
⊢ Associated |x| y ↔ Associated x y

Tactic:
simp [h]

Goal state after:
Module: Mathlib.Algebra.Ring.Divisibility.Lemmas

Goal state before:
pp: case inr
R : Type u_1
inst✝¹ : Ring R
inst✝ : LinearOrder R
x y : R
h : |x| = -x
⊢ Associated |x| y ↔ Associated x y

Tactic:
simp [h]

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

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

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
⊢ ∀ (x y : A ⊗[R] L),
    ((bracket' R A L L) x) z₂ + ((bracket' R A L L) z₂) x = 0 →
      ((bracket' R A L L) y) z₂ + ((bracket' R A L L) z₂) y = 0 →
        ((bracket' R A L L) (x + y)) z₂ + ((bracket' R A L L) z₂) (x + y) = 0

Tactic:
· intro a₁ l₁; refine z₂.induction_on ?_ ?_ ?_
      · simp only [map_zero, add_zero, LinearMap.zero_apply]
      · intro a₂ l₂
        simp only [← lie_skew l₂ l₁, mul_comm a₁ a₂, TensorProduct.tmul_neg, bracket'_tmul,
          add_neg_cancel]
      · intro y₁ y₂ hy₁ hy₂
        simp only [hy₁, hy₂, add_add_add_comm, add_zero, LinearMap.add_apply, map_add]

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
⊢ ∀ (x y : A ⊗[R] L),
    ((bracket' R A L L) x) z₂ + ((bracket' R A L L) z₂) x = 0 →
      ((bracket' R A L L) y) z₂ + ((bracket' R A L L) z₂) y = 0 →
        ((bracket' R A L L) (x + y)) z₂ + ((bracket' R A L L) z₂) (x + y) = 0
Module: Mathlib.Algebra.Lie.BaseChange

Goal state before:
pp: 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
R : Type u_5
A : Type u_6
B : Type u_7
L : Type u_8
L' : Type u_9
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : A →ₐ[R] B
g : L →ₗ⁅R⁆ L'
x y x✝² y✝ : A ⊗[R] L
x✝¹ : A
x✝ : L
h :
  (TensorProduct.map f.toLinearMap ↑g) (((LieAlgebra.ExtendScalars.bracket'✝ R A L L) x✝²) (x✝¹ ⊗ₜ[R] x✝)) =
    ((LieAlgebra.ExtendScalars.bracket'✝ R B L' L') ((TensorProduct.map f.toLinearMap ↑g) x✝²))
      ((TensorProduct.map f.toLinearMap ↑g) (x✝¹ ⊗ₜ[R] x✝))
⊢ (TensorProduct.map f.toLinearMap ↑g) (((LieAlgebra.ExtendScalars.bracket'✝ R A L L) y✝) (x✝¹ ⊗ₜ[R] x✝)) =
      ((LieAlgebra.ExtendScalars.bracket'✝ R B L' L') ((TensorProduct.map f.toLinearMap ↑g) y✝))
        ((TensorProduct.map f.toLinearMap ↑g) (x✝¹ ⊗ₜ[R] x✝)) →
    (TensorProduct.map f.toLinearMap ↑g) (((LieAlgebra.ExtendScalars.bracket'✝ R A L L) (x✝² + y✝)) (x✝¹ ⊗ₜ[R] x✝)) =
      ((LieAlgebra.ExtendScalars.bracket'✝ R B L' L') ((TensorProduct.map f.toLinearMap ↑g) (x✝² + y✝)))
        ((TensorProduct.map f.toLinearMap ↑g) (x✝¹ ⊗ₜ[R] x✝))

Tactic:
simp [h]

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 = ⊥
⊢ N ⊓ lcs k N = ⊥

Tactic:
simp [h]

Goal state after: