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

Goal state before:
pp: case pos.inl
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 : emultiplicity a x ≤ 1
⊢ Multiset.count (normalize a) (normalizedFactors x) ≤ 1

Tactic:
emultiplicity_eq_count_normalizedFactors ha x0

Goal state after:
case pos.inl
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 : ↑(Multiset.count (normalize a) (normalizedFactors x)) ≤ 1
⊢ Multiset.count (normalize a) (normalizedFactors x) ≤ 1
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: 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
hg1 : g.natDegree * p = N.succ
this : g.natDegree = 0
⊢ False

Tactic:
rw [this, zero_mul] at hg1

Goal state after:
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
hg1 : 0 = N.succ
this : g.natDegree = 0
⊢ False
Module: Mathlib.FieldTheory.Perfect

Goal state before:
pp: 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
⊢ f ((⇑(frobenius R p))^[n] ((⇑(frobeniusEquiv R p).symm)^[n] x)) =
    (⇑(frobenius S p))^[n] ((⇑(frobeniusEquiv S p).symm)^[n] (f x))

Tactic:
← Function.comp_apply (f := (⇑(frobenius R p))^[n]),

Goal state after:
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
⊢ f (((⇑(frobenius R p))^[n] ∘ (⇑(frobeniusEquiv R p).symm)^[n]) x) =
    (⇑(frobenius S p))^[n] ((⇑(frobeniusEquiv S p).symm)^[n] (f x))
Module: Mathlib.FieldTheory.Perfect

Goal state before:
pp: R : Type u_2
p : ℕ
inst✝³ : CommSemiring R
inst✝² : Fact (Nat.Prime p)
inst✝¹ : CharP R p
inst✝ : PerfectRing R p
f : R[X]
⊢ ¬Irreducible ((expand R p) f)

Tactic:
polynomial_expand_eq

Goal state after:
R : Type u_2
p : ℕ
inst✝³ : CommSemiring R
inst✝² : Fact (Nat.Prime p)
inst✝¹ : CharP R p
inst✝ : PerfectRing R p
f : R[X]
⊢ ¬Irreducible (map (↑(frobeniusEquiv R p).symm) f ^ p)
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 : ((expand F (p ^ n)) f).Separable
hn : n ≠ 0
⊢ (expand F (p ^ n)) (derivative f) * 0 = 0

Tactic:
mul_zero

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

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
p n : ℕ
inst✝¹ : ExpChar R p
inst✝ : PerfectRing R p
y : R
H : ((expand R (p ^ n)) (X - C y)).roots = p ^ n • {(iterateFrobeniusEquiv R p n).symm y}
⊢ (X ^ p ^ n - C y).roots = p ^ n • {(iterateFrobeniusEquiv R p n).symm y}

Tactic:
map_sub,

Goal state after:
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
p n : ℕ
inst✝¹ : ExpChar R p
inst✝ : PerfectRing R p
y : R
H : ((expand R (p ^ n)) X - (expand R (p ^ n)) (C y)).roots = p ^ n • {(iterateFrobeniusEquiv R p n).symm y}
⊢ (X ^ p ^ n - C y).roots = p ^ n • {(iterateFrobeniusEquiv R p n).symm y}
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
g : R[X]
hg : g.Monic
f : AdjoinRoot g
⊢ (mk g) ((modByMonicHom hg) f) = f

Tactic:
induction f using AdjoinRoot.induction_on

Goal state after:
case ih
R : Type u_1
inst✝ : CommRing R
g : R[X]
hg : g.Monic
p✝ : R[X]
⊢ (mk g) ((modByMonicHom hg) ((mk g) p✝)) = (mk g) p✝
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: case h₀
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst✝ : CommRing R
g : R[X]
hg : g.Monic
i j : Fin g.natDegree
a✝ : j ∈ Finset.univ
hj : j ≠ i
⊢ (monomial ↑j) (Pi.single i 1 j) = (monomial ?m.66) 0

pp: R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst✝ : CommRing R
g : R[X]
hg : g.Monic
i j : Fin g.natDegree
a✝ : j ∈ Finset.univ
hj : j ≠ i
⊢ ℕ

Tactic:
Pi.single_eq_of_ne hj

Goal state after:
case h₀
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst✝ : CommRing R
g : R[X]
hg : g.Monic
i j : Fin g.natDegree
a✝ : j ∈ Finset.univ
hj : j ≠ i
⊢ (monomial ↑j) 0 = (monomial ?m.66) 0

R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst✝ : CommRing R
g : R[X]
hg : g.Monic
i j : Fin g.natDegree
a✝ : j ∈ Finset.univ
hj : j ≠ i
⊢ ℕ
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: case refine_2
K : Type u_5
inst✝ : Field K
f : K[X]
hf : f ≠ 0
f'_monic : (f * C f.leadingCoeff⁻¹).Monic
⊢ ∀ (q : K[X]), q.Monic → (aeval (root f)) q = 0 → (f * C f.leadingCoeff⁻¹).degree ≤ q.degree

Tactic:
intro q q_monic q_aeval

Goal state after:
case refine_2
K : Type u_5
inst✝ : Field K
f : K[X]
hf : f ≠ 0
f'_monic : (f * C f.leadingCoeff⁻¹).Monic
q : K[X]
q_monic : q.Monic
q_aeval : (aeval (root f)) q = 0
⊢ (f * C f.leadingCoeff⁻¹).degree ≤ q.degree
Module: Mathlib.LinearAlgebra.Determinant

Goal state before:
pp: case inr.inl
R : Type u_6
V : Type u_7
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : Module.Finite R V
W : Submodule R V
inst✝² : Free R ↥W
inst✝¹ : Module.Finite R ↥W
inst✝ : Free R (V ⧸ W)
e : V →ₗ[R] V
he : W ≤ comap e W
m : Type u_7 := Free.ChooseBasisIndex R ↥W
bW : Basis m R ↥W := Free.chooseBasis R ↥W
n : Type u_7 := Free.ChooseBasisIndex R (V ⧸ W)
bQ : Basis n R (V ⧸ W) := Free.chooseBasis R (V ⧸ W)
b : Basis (m ⊕ n) R V := bW.sumQuot bQ
A : Matrix m m R := (toMatrix bW bW) (e.restrict he)
B : Matrix m n R := of fun i l ↦ ((bW.sumQuot bQ).repr (e ((bW.sumQuot bQ) (Sum.inr l)))) (Sum.inl i)
D : Matrix n n R := (toMatrix bQ bQ) (W.mapQ W e he)
j : n
k : m
⊢ (toMatrix b b) e (Sum.inr j) (Sum.inl k) = fromBlocks A B 0 D (Sum.inr j) (Sum.inl k)

Tactic:
suffices W.mkQ (e (bW k)) = 0 by simp [LinearMap.toMatrix_apply, b, this]
      rw [← LinearMap.mem_ker, Submodule.ker_mkQ]
      exact he (Submodule.coe_mem (bW k))

Goal state after:
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
⊢ (ad R L).IsIdealMorphism

Tactic:
simp_rw [LieHom.isIdealMorphism_iff, lie_der_ad_eq_ad_der]

Goal state after:
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
⊢ ∀ (x : LieDerivation R L L) (y : L), ∃ z, (ad R L) (x y) = (ad R L) z
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) ((Ideal.Quotient.mk (Ideal.map (algebraMap R S) I)) ((aeval pb.gen) g)) =
    (Ideal.Quotient.mk (span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R pb.gen)}))
      (Polynomial.map (Ideal.Quotient.mk I) g)

Tactic:
PowerBasis.quotientEquivQuotientMinpolyMap,

Goal state after:
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]
⊢ ((ofRingEquiv ⋯).trans (quotEquivQuotMap (minpoly R pb.gen) I))
      ((Ideal.Quotient.mk (Ideal.map (algebraMap R S) I)) ((aeval pb.gen) g)) =
    (Ideal.Quotient.mk (span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R pb.gen)}))
      (Polynomial.map (Ideal.Quotient.mk I) g)
Module: Mathlib.Dynamics.Newton

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : R[X]
x : S
h : IsUnit ((aeval x) (derivative P))
⊢ (aeval x) P = (aeval x) (derivative P) * 0 ↔ (aeval x) P = 0

Tactic:
mul_zero

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : R[X]
x : S
h : IsUnit ((aeval x) (derivative P))
⊢ (aeval x) P = 0 ↔ (aeval x) P = 0
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: case neg
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
q : (AdjoinRoot p)[X]
hq : Polynomial.map (algebraMap R (AdjoinRoot p)) p = (X - C (AdjoinRoot.root p)) * q
hqm : q.Monic
this✝¹ : Free R (AdjoinRoot p)
this✝ : Module.Finite R (AdjoinRoot p)
this : Nontrivial (AdjoinRoot p)
S : Type u
w✝⁴ : CommRing S
w✝³ : Algebra (AdjoinRoot p) S
w✝² : Module.Finite (AdjoinRoot p) S
w✝¹ : Free (AdjoinRoot p) S
w✝ : Nontrivial S
hS : (Polynomial.map (algebraMap (AdjoinRoot p) S) q).Splits
algInst✝ : Algebra R S := ((algebraMap (AdjoinRoot p) S).comp (algebraMap R (AdjoinRoot p))).toAlgebra
scalarTowerInst✝ : IsScalarTower R (AdjoinRoot p) S := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap R S))
⊢ ∃ S x x_1, ∃ (_ : Module.Finite R S) (_ : Free R S) (_ : Nontrivial S), (Polynomial.map (algebraMap R S) p).Splits

Tactic:
refine ⟨S, ‹_›, ‹_›, .trans (AdjoinRoot p) _, .trans (S := AdjoinRoot p), ‹_›, ?_⟩

Goal state after:
case neg
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
q : (AdjoinRoot p)[X]
hq : Polynomial.map (algebraMap R (AdjoinRoot p)) p = (X - C (AdjoinRoot.root p)) * q
hqm : q.Monic
this✝¹ : Free R (AdjoinRoot p)
this✝ : Module.Finite R (AdjoinRoot p)
this : Nontrivial (AdjoinRoot p)
S : Type u
w✝⁴ : CommRing S
w✝³ : Algebra (AdjoinRoot p) S
w✝² : Module.Finite (AdjoinRoot p) S
w✝¹ : Free (AdjoinRoot p) S
w✝ : Nontrivial S
hS : (Polynomial.map (algebraMap (AdjoinRoot p) S) q).Splits
algInst✝ : Algebra R S := ((algebraMap (AdjoinRoot p) S).comp (algebraMap R (AdjoinRoot p))).toAlgebra
scalarTowerInst✝ : IsScalarTower R (AdjoinRoot p) S := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap R S))
⊢ (Polynomial.map (algebraMap R S) p).Splits
Module: Mathlib.LinearAlgebra.JordanChevalley

Goal state before:
pp: K : Type u_1
V : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
P : K[X]
k✝ : ℕ
sep : P.Separable
nil : minpoly K f ∣ P ^ k✝
ff : ↥K[f] := ⟨f, ⋯⟩
P' : K[X] := derivative P
nil' : IsNilpotent ((aeval ff) P)
sep' : IsUnit ((aeval ff) P')
s : End K V
mem : s ∈ K[f]
hss : (aeval ⟨s, mem⟩) P = 0
k : ℕ
hk : (ff - ⟨s, mem⟩) ^ k = 0
⊢ (aeval s) P = 0

Tactic:
Subtype.ext_iff,

Goal state after:
K : Type u_1
V : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
P : K[X]
k✝ : ℕ
sep : P.Separable
nil : minpoly K f ∣ P ^ k✝
ff : ↥K[f] := ⟨f, ⋯⟩
P' : K[X] := derivative P
nil' : IsNilpotent ((aeval ff) P)
sep' : IsUnit ((aeval ff) P')
s : End K V
mem : s ∈ K[f]
hss : ↑((aeval ⟨s, mem⟩) P) = ↑0
k : ℕ
hk : (ff - ⟨s, mem⟩) ^ k = 0
⊢ (aeval s) P = 0
Module: Mathlib.Algebra.Lie.AdjointAction.JordanChevalley

Goal state before:
pp: K : Type u_1
V : Type u_2
inst✝⁴ : Field K
inst✝³ : PerfectField K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
n s : Module.End K V
hc : Commute n s
hn : IsNilpotent n
hs : s.IsSemisimple
⊢ (ad K (Module.End K V)) s ∈ K[(ad K (Module.End K V)) (n + s)]

Tactic:
obtain ⟨n', hn'_adj, s', hs'_adj, hn'_nil, hs'_ss, h_jc⟩ :=
    (ad K _ (n + s)).exists_isNilpotent_isSemisimple
  have hc' : Commute n' s' :=
    Algebra.commute_of_mem_adjoin_singleton_of_commute hs'_adj
      (Algebra.commute_of_mem_adjoin_self hn'_adj).symm
  obtain ⟨-, hs_eq⟩ := Module.End.isNilpotent_isSemisimple_unique hn'_nil hs'_ss
    (LieAlgebra.ad_nilpotent_of_nilpotent (R := K) hn)
    (LieAlgebra.ad_isSemisimple_of_isSemisimple hs) hc'
    (LieAlgebra.commute_ad_of_commute hc) (h_jc.symm.trans (map_add (ad K _) n s))
  rwa [hs_eq] at hs'_adj

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
⊢ (-1) ^ n * 0 = 0

Tactic:
mul_zero

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
⊢ 0 = 0
Module: Mathlib.Algebra.Lie.BaseChange

Goal state before:
pp: case refine_1
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
N : LieSubmodule R L M
x : A ⊗[R] L
c : ↑↑(Submodule.map ((TensorProduct.mk R A M) 1) ↑N) →₀ A
hm : (Finsupp.linearCombination A Subtype.val) c ∈ Submodule.span A ↑(Submodule.map ((TensorProduct.mk R A M) 1) ↑N)
a : A
y : L
⊢ ⁅a ⊗ₜ[R] y, (Finsupp.linearCombination A Subtype.val) c⁆ ∈ Submodule.baseChange A ↑N

Tactic:
change toEnd A (A ⊗[R] L) (A ⊗[R] M) _ _ ∈ _
        simp_rw [Finsupp.linearCombination_apply, Finsupp.sum, map_sum, map_smul, toEnd_apply_apply]
        refine Submodule.sum_mem _ fun ⟨_, n, hn, h⟩ _ ↦ Submodule.smul_mem _ _ ?_
        rw [Subtype.coe_mk, ← h]
        exact Submodule.tmul_mem_baseChange_of_mem _ (N.lie_mem hn)

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

Goal state before:
pp: case succ
R : Type u₁
L : Type u₂
M : Type u₄
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
I : LieIdeal R L
x : L
hxI : R ∙ x ⊔ (LieIdeal.toLieSubalgebra R L I).toSubmodule = ⊤
n i j : ℕ
hxn : (toEnd R L M) x ^ n = 0
hIM : lowerCentralSeries R L M i ≤ I.lcs M j
l : ℕ
ih : ↑(⊤.lcs M (i + l)) ≤ Submodule.map ((toEnd R L M) x ^ l) ↑(I.lcs M j) ⊔ ↑(I.lcs M (j + 1))
⊢ ↑(⊤.lcs M (i + (l + 1))) ≤ Submodule.map ((toEnd R L M) x ^ (l + 1)) ↑(I.lcs M j) ⊔ ↑(I.lcs M (j + 1))

Tactic:
| succ l ih =>

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

Tactic:
LieSubmodule.comap_incl_eq_bot,

Goal state after:
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
N : LieSubmodule R L M
k : ℕ
⊢ N ⊓ LieSubmodule.lcs k N = ⊥ ↔ LieSubmodule.lcs k N = ⊥
Module: Mathlib.Algebra.Lie.BaseChange

Goal state before:
pp: case 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 ∈ baseChange A I
m : A ⊗[R] M
hm : m ∈ baseChange A N
⊢ ⁅x, m⁆ ∈ ↑(Submodule.span A s)

Tactic:
mem_baseChange_iff

Goal state after:
case 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, m⁆ ∈ ↑(Submodule.span A s)
Module: Mathlib.Algebra.Lie.Engel

Goal state before:
pp: case succ
R : Type u₁
L : Type u₂
M : Type u₄
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
I : LieIdeal R L
x : L
hxI : R ∙ x ⊔ (LieIdeal.toLieSubalgebra R L I).toSubmodule = ⊤
hIM : LieModule.IsNilpotent (↥I) M
n : ℕ
hn : (toEnd R L M) x ^ n = 0
k : ℕ
hk : lowerCentralSeries R (↥I) M k = ⊥
hk' : I.lcs M k = ⊥
l : ℕ
ih : lowerCentralSeries R L M (l * n) ≤ I.lcs M l
⊢ lowerCentralSeries R L M ((l + 1) * n) ≤ I.lcs M (l + 1)

Tactic:
| succ l ih =>

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
inst✝ : LieModule R L M
N : LieSubmodule R L M
h₁ : N ≤ maxTrivSubmodule R L M
k : ℕ
hk : lowerCentralSeries R L (M ⧸ N) k = ⊥
this : ⁅⊤, lowerCentralSeries R L M k⁆ ≤ ⊥
⊢ ⁅⊤, lowerCentralSeries R L M k⁆ = ⊥

Tactic:
le_bot_iff

Goal state after:
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
N : LieSubmodule R L M
h₁ : N ≤ maxTrivSubmodule R L M
k : ℕ
hk : lowerCentralSeries R L (M ⧸ N) k = ⊥
this : ⁅⊤, lowerCentralSeries R L M k⁆ = ⊥
⊢ ⁅⊤, lowerCentralSeries R L M k⁆ = ⊥
Module: Mathlib.Algebra.Lie.Nilpotent

Goal state before:
pp: R : Type u
L : Type v
M : Type w
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
inst✝ : IsNilpotent L M
h : Disjoint (lowerCentralSeries R L M 1) (maxTrivSubmodule R L M)
a✝ : Nontrivial M
contra : ¬IsTrivial L M
this : lowerCentralSeriesLast R L M ≤ ⊥
⊢ ¬Nontrivial ↥(lowerCentralSeriesLast R L M)

Tactic:
le_bot_iff

Goal state after:
R : Type u
L : Type v
M : Type w
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
inst✝ : IsNilpotent L M
h : Disjoint (lowerCentralSeries R L M 1) (maxTrivSubmodule R L M)
a✝ : Nontrivial M
contra : ¬IsTrivial L M
this : lowerCentralSeriesLast R L M = ⊥
⊢ ¬Nontrivial ↥(lowerCentralSeriesLast R L M)
Module: Mathlib.Algebra.Lie.Nilpotent

Goal state before:
pp: case mpr
R : Type u
L : Type v
L' : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
e : L ≃ₗ⁅R⁆ L'
h : LieRing.IsNilpotent L'
⊢ LieRing.IsNilpotent L

Tactic:
exact e.injective.lieAlgebra_isNilpotent

Goal state after:
Module: Mathlib.RingTheory.Adjoin.Singleton

Goal state before:
pp: A : Type u_1
B : Type u_2
C : Type u_3
inst✝⁶ : CommSemiring A
inst✝⁵ : CommSemiring B
inst✝⁴ : CommSemiring C
inst✝³ : Algebra A B
inst✝² : Algebra B C
inst✝¹ : Algebra A C
inst✝ : IsScalarTower A B C
b : B
⊢ Function.Surjective ⇑(adjoinAlgebraMap b)

Tactic:
intro c

Goal state after:
A : Type u_1
B : Type u_2
C : Type u_3
inst✝⁶ : CommSemiring A
inst✝⁵ : CommSemiring B
inst✝⁴ : CommSemiring C
inst✝³ : Algebra A B
inst✝² : Algebra B C
inst✝¹ : Algebra A C
inst✝ : IsScalarTower A B C
b : B
c : ↥A[(algebraMap B C) b]
⊢ ∃ a, (adjoinAlgebraMap b) a = c
Module: Mathlib.FieldTheory.Fixed

Goal state before:
pp: case h
G : Type u_2
F : Type u_3
inst✝³ : Group G
inst✝² : Field F
inst✝¹ : MulSemiringAction G F
inst✝ : Finite G
f : G →* Gal(F/↥(subfield G F)) := MulSemiringAction.toAlgAut G (↥(subfield G F)) F
Q : Type u_2 := G ⧸ f.ker
x✝ : MulSemiringAction Q F := MulSemiringAction.compHom F (QuotientGroup.kerLift f)
g₁ g₂ : G
h : ∀ (a : F), ⟦g₁⟧ • a = ⟦g₂⟧ • a
⊢ (f g₁)⁻¹ * f g₂ = 1

Tactic:
inv_mul_eq_one,

Goal state after:
case h
G : Type u_2
F : Type u_3
inst✝³ : Group G
inst✝² : Field F
inst✝¹ : MulSemiringAction G F
inst✝ : Finite G
f : G →* Gal(F/↥(subfield G F)) := MulSemiringAction.toAlgAut G (↥(subfield G F)) F
Q : Type u_2 := G ⧸ f.ker
x✝ : MulSemiringAction Q F := MulSemiringAction.compHom F (QuotientGroup.kerLift f)
g₁ g₂ : G
h : ∀ (a : F), ⟦g₁⟧ • a = ⟦g₂⟧ • a
⊢ f g₁ = f g₂
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs

Goal state before:
pp: F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
K : IntermediateField F E
⊢ map K.val ⊤ = K

Tactic:
← AlgHom.fieldRange_eq_map,

Goal state after:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
K : IntermediateField F E
⊢ K.val.fieldRange = K
Module: Mathlib.LinearAlgebra.Eigenspace.Triangularizable

Goal state before:
pp: case pos
K : Type u_1
V : Type u_2
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
p : Submodule K V
f : End K V
inst✝ : FiniteDimensional K V
h : ∀ x ∈ p, f x ∈ p
k : ℕ∞
m : K →₀ V
hm₂ : ∀ (i : K), m i ∈ (f.genEigenspace i) k
hm₀ : (m.sum fun _i xi ↦ xi) ∈ p
hm₁ : (m.sum fun _i xi ↦ xi) ∈ ⨆ μ, (f.genEigenspace μ) k
μ : K
hμ : μ ∈ m.support
l : K → ℕ
hlk : ∀ (i : K), ↑(l i) ≤ k
hl : ∀ (i : K), m i ∈ ((f - i • 1) ^ l i).ker
l₀ : ℕ := m.support.sup l
h_comm : ∀ (μ₁ μ₂ : K), Commute ((f - (algebraMap K (End K V)) μ₁) ^ l₀) ((f - (algebraMap K (End K V)) μ₂) ^ l₀)
g : End K V := (m.support.erase μ).noncommProd (fun μ₁ ↦ (f - (algebraMap K (End K V)) μ₁) ^ l₀) ⋯
⊢ m μ ∈ p

Tactic:
have hfg : Commute f g := Finset.noncommProd_commute _ _ _ _ fun μ' _ ↦
    (Commute.sub_right rfl <| Algebra.commute_algebraMap_right _ _).pow_right _

Goal state after:
case pos
K : Type u_1
V : Type u_2
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
p : Submodule K V
f : End K V
inst✝ : FiniteDimensional K V
h : ∀ x ∈ p, f x ∈ p
k : ℕ∞
m : K →₀ V
hm₂ : ∀ (i : K), m i ∈ (f.genEigenspace i) k
hm₀ : (m.sum fun _i xi ↦ xi) ∈ p
hm₁ : (m.sum fun _i xi ↦ xi) ∈ ⨆ μ, (f.genEigenspace μ) k
μ : K
hμ : μ ∈ m.support
l : K → ℕ
hlk : ∀ (i : K), ↑(l i) ≤ k
hl : ∀ (i : K), m i ∈ ((f - i • 1) ^ l i).ker
l₀ : ℕ := m.support.sup l
h_comm : ∀ (μ₁ μ₂ : K), Commute ((f - (algebraMap K (End K V)) μ₁) ^ l₀) ((f - (algebraMap K (End K V)) μ₂) ^ l₀)
g : End K V := (m.support.erase μ).noncommProd (fun μ₁ ↦ (f - (algebraMap K (End K V)) μ₁) ^ l₀) ⋯
hfg : Commute f g
⊢ m μ ∈ p
Module: Mathlib.FieldTheory.IsAlgClosed.Basic

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : IsAlgClosed K
inst✝ : CharZero K
f g : K[X]
hf0 : f ≠ 0
⊢ (∀ (x : K), f.IsRoot x → g.IsRoot x) ↔ f ∣ derivative f * g

Tactic:
by
  refine ⟨?_, isRoot_of_isRoot_of_dvd_derivative_mul hf0⟩
  by_cases hg0 : g = 0
  · simp [hg0]
  by_cases hdf0 : derivative f = 0
  · rw [eq_C_of_derivative_eq_zero hdf0]
    simp only [derivative_C, zero_mul, dvd_zero, implies_true]
  have hdg : f.derivative * g ≠ 0 := mul_ne_zero hdf0 hg0
  classical rw [IsAlgClosed.dvd_iff_roots_le_roots hf0 hdg, Multiset.le_iff_count]
  simp only [count_roots, rootMultiplicity_mul hdg]
  refine forall_imp fun a => ?_
  by_cases haf : f.eval a = 0
  · have h0 : 0 < f.rootMultiplicity a := (rootMultiplicity_pos hf0).2 haf
    rw [derivative_rootMultiplicity_of_root haf]
    intro h
    calc rootMultiplicity a f
        = rootMultiplicity a f - 1 + 1 := (Nat.sub_add_cancel (Nat.succ_le_iff.1 h0)).symm
      _ ≤ rootMultiplicity a f - 1 + rootMultiplicity a g := add_le_add le_rfl (Nat.succ_le_iff.1
        ((rootMultiplicity_pos hg0).2 (h haf)))
  · simp [haf, rootMultiplicity_eq_zero haf]

Goal state after: