mathlib-initiative/mathlib-tactics huggingface dataset:
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
⊢ minpoly K ((algebraMap S L) s) ∣ map (algebraMap R K) (minpoly R s)

Tactic:
by
  apply minpoly.dvd K (algebraMap S L s)
  rw [← map_aeval_eq_aeval_map, minpoly.aeval, map_zero]
  rw [← IsScalarTower.algebraMap_eq, ← IsScalarTower.algebraMap_eq]

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

Goal state before:
pp: case left
R : Type u
L : Type v
M : Type w
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
N N' : LieSubmodule R L M
inst✝ : LieAlgebra R L
I : LieIdeal R L
⊢ ⁅I, N ⊓ N'⁆ ≤ ⁅I, N⁆

Tactic:
apply mono_lie_right

Goal state after:
case left
R : Type u
L : Type v
M : Type w
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
N N' : LieSubmodule R L M
inst✝ : LieAlgebra R L
I : LieIdeal R L
⊢ N ⊓ N' ≤ N
Module: Mathlib.Algebra.Lie.IdealOperations

Goal state before:
pp: case right
R : Type u
L : Type v
M : Type w
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
N N' : LieSubmodule R L M
inst✝ : LieAlgebra R L
I : LieIdeal R L
⊢ ⁅I, N ⊓ N'⁆ ≤ ⁅I, N'⁆

Tactic:
apply mono_lie_right

Goal state after:
case right
R : Type u
L : Type v
M : Type w
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
N N' : LieSubmodule R L M
inst✝ : LieAlgebra R L
I : LieIdeal R L
⊢ N ⊓ N' ≤ N'
Module: Mathlib.Algebra.Lie.IdealOperations

Goal state before:
pp: R : Type u
L : Type v
M : Type w
M₂ : Type w₁
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : LieRingModule L M
inst✝⁵ : AddCommGroup M₂
inst✝⁴ : Module R M₂
inst✝³ : LieRingModule L M₂
N : LieSubmodule R L M
f : M →ₗ⁅R,L⁆ M₂
inst✝² : LieAlgebra R L
inst✝¹ : LieModule R L M₂
I : LieIdeal R L
inst✝ : LieModule R L M
⊢ map f ⁅I, N⁆ = ⁅I, map f N⁆

Tactic:
← toSubmodule_inj,

Goal state after:
R : Type u
L : Type v
M : Type w
M₂ : Type w₁
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : LieRingModule L M
inst✝⁵ : AddCommGroup M₂
inst✝⁴ : Module R M₂
inst✝³ : LieRingModule L M₂
N : LieSubmodule R L M
f : M →ₗ⁅R,L⁆ M₂
inst✝² : LieAlgebra R L
inst✝¹ : LieModule R L M₂
I : LieIdeal R L
inst✝ : LieModule R L M
⊢ ↑(map f ⁅I, N⁆) = ↑⁅I, map f N⁆
Module: Mathlib.FieldTheory.Minpoly.Field

Goal state before:
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:
have : (Polynomial.aeval x) ((-1) ^ q.natDegree * q.comp (-X)) = 0 := by
        simpa [aeval_comp] using hq
      have H := minpoly.min A x qmo.neg_one_pow_natDegree_mul_comp_neg_X this
      simp_all

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Ideal

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a : R
b : R[X]
P : R[X][X]
⊢ P ∈ Ideal.span {C (X - C a), X - C b} ↔ eval a (eval b P) = 0

Tactic:
rw [Ideal.mem_span_pair]

Goal state after:
R : Type u_1
inst✝ : CommRing R
a : R
b : R[X]
P : R[X][X]
⊢ (∃ a_1 b_1, a_1 * C (X - C a) + b_1 * (X - C b) = P) ↔ eval a (eval b P) = 0
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:
(commute_lmul_lmul_sq (a + b + c)).lie_eq

Goal state after:
A : Type u_1
inst✝¹ : NonUnitalNonAssocCommRing A
inst✝ : IsCommJordan A
a b c : A
⊢ 0 = 0
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
h : ¬∃ s, Nonempty (Basis (↥s) R S)
x : S
⊢ (norm R) x = 1

Tactic:
by rw [norm_apply, LinearMap.det]; split_ifs <;> trivial

Goal state after:
Module: Mathlib.LinearAlgebra.Determinant

Goal state before:
pp: A : Type u_5
inst✝⁴ : CommRing A
m : Type u_6
n : Type u_7
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
M : Matrix m n A
M' : Matrix n m A
N : Matrix n n A
hMM' : M * M' = 1
hM'M : M' * M = 1
⊢ (M * N * M').det = N.det

Tactic:
← det_comm' hM'M hMM',

Goal state after:
A : Type u_5
inst✝⁴ : CommRing A
m : Type u_6
n : Type u_7
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
M : Matrix m n A
M' : Matrix n m A
N : Matrix n n A
hMM' : M * M' = 1
hM'M : M' * M = 1
⊢ (M' * (M * N)).det = N.det
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
⊢ (if p = 0 then 0 else multiplicity (X - C x) p) ≤ 1

Tactic:
if_neg hp,

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.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
⊢ (X ^ p ^ n - C y).roots = p ^ n • {(iterateFrobeniusEquiv R p n).symm y}

Tactic:
have H := roots_expand_pow (p := p) (n := n) (f := X - C y)

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 - C y)).roots = p ^ n • Multiset.map (⇑(iterateFrobeniusEquiv R p n).symm) (X - C y).roots
⊢ (X ^ p ^ n - C y).roots = p ^ n • {(iterateFrobeniusEquiv R p n).symm y}
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
m : ℕ
⊢ ((X ^ p ^ n - C y) ^ m).roots = (m * p ^ n) • {(iterateFrobeniusEquiv R p n).symm y}

Tactic:
by
  rw [roots_pow, roots_X_pow_char_pow_sub_C, mul_smul]

Goal state after:
Module: Mathlib.FieldTheory.Perfect

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
p n : ℕ
inst✝² : ExpChar R p
f : R[X]
inst✝¹ : DecidableEq R
inst✝ : PerfectRing R p
⊢ ⇑(frobeniusEquiv R p).toEquiv '' ↑((expand R p) f).roots.toFinset = ↑f.roots.toFinset

Tactic:
by
    rw [← roots_expand_image_frobenius (p := p) (f := f)]
    simp

Goal state after:
Module: Mathlib.FieldTheory.Perfect

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
p n✝ : ℕ
inst✝² : ExpChar R p
f : R[X]
inst✝¹ : DecidableEq R
inst✝ : PerfectRing R p
n : ℕ
⊢ ⇑(iterateFrobeniusEquiv R p n).toEquiv '' ↑((expand R (p ^ n)) f).roots.toFinset = ↑f.roots.toFinset

Tactic:
← roots_expand_image_iterateFrobenius (p := p) (f := f) (n := n)

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
p n✝ : ℕ
inst✝² : ExpChar R p
f : R[X]
inst✝¹ : DecidableEq R
inst✝ : PerfectRing R p
n : ℕ
⊢ ⇑(iterateFrobeniusEquiv R p n).toEquiv '' ↑((expand R (p ^ n)) f).roots.toFinset =
    ↑(Finset.image (⇑(iterateFrobenius R p n)) ((expand R (p ^ n)) f).roots.toFinset)
Module: Mathlib.LinearAlgebra.AnnihilatingPolynomial

Goal state before:
pp: case neg
𝕜 : Type u_1
A : Type u_2
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
h : ¬annIdealGenerator 𝕜 a = 0
⊢ annIdealGenerator 𝕜 a = minpoly 𝕜 a

Tactic:
· exact minpoly.unique _ _ (monic_annIdealGenerator _ _ h) (annIdealGenerator_aeval_eq_zero _ _)
      fun q q_monic hq =>
        degree_annIdealGenerator_le_of_mem a q (mem_annIdeal_iff_aeval_eq_zero.mpr hq)
          q_monic.ne_zero

Goal state after:
Module: Mathlib.LinearAlgebra.Determinant

Goal state before:
pp: case neg
R : Type u_1
inst✝⁵ : CommRing R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
ι : Type u_4
inst✝² : Fintype ι
inst✝¹ : Free R M
inst✝ : Module.Finite R M
f : ι → M →ₗ[R] M
b : Basis (Free.ChooseBasisIndex R M) R M := Free.chooseBasis R M
B : Basis (Free.ChooseBasisIndex R M × ι) R (ι → M) :=
  (Pi.basis fun x ↦ b).reindex
    ((Equiv.sigmaEquivProd ι (Free.ChooseBasisIndex R M)).trans (Equiv.prodComm ι (Free.ChooseBasisIndex R M)))
i₁ : Free.ChooseBasisIndex R M
i₂ : ι
j₁ : Free.ChooseBasisIndex R M
j₂ : ι
h : ¬i₂ = j₂
⊢ (b.repr ((f i₂) 0)) i₁ = 0

Tactic:
simp only [map_zero, Finsupp.coe_zero, Pi.zero_apply]

Goal state after:
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: F : Type u_1
L : Type u_2
inst✝² : CommRing F
inst✝¹ : Ring L
inst✝ : Algebra F L
S : Subalgebra F L
⊢ (∀ (a : L) (b : a ∈ S), IsSeparable F ⟨a, b⟩) ↔ ∀ x ∈ S, IsSeparable F x

Tactic:
← isSeparable_map_iff S.val Subtype.val_injective,

Goal state after:
F : Type u_1
L : Type u_2
inst✝² : CommRing F
inst✝¹ : Ring L
inst✝ : Algebra F L
S : Subalgebra F L
⊢ (∀ (a : L) (b : a ∈ S), IsSeparable F (S.val ⟨a, b⟩)) ↔ ∀ x ∈ S, IsSeparable F x
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: case add
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
f : S[X]
p q : R[X]
a✝¹ : (aeval (root f)) p = (mk f) (Polynomial.map (algebraMap R S) p)
a✝ : (aeval (root f)) q = (mk f) (Polynomial.map (algebraMap R S) q)
⊢ (aeval (root f)) (p + q) = (mk f) (Polynomial.map (algebraMap R S) (p + q))

Tactic:
| add p q _ _ =>

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'
⊢ f (((toLin v' v) ((toMatrix v v') f)⁻¹) x) = ((toLin v' v') ((toMatrix v v') f * ((toMatrix v v') f)⁻¹)) x

Tactic:
by
        rw [toLin_mul v' v v', LinearMap.comp_apply, toLin_toMatrix v v']

Goal state after:
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: 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✝

Tactic:
modByMonicHom_mk hg,

Goal state after:
case ih
R : Type u_1
inst✝ : CommRing R
g : R[X]
hg : g.Monic
p✝ : R[X]
⊢ (mk g) (p✝ %ₘ g) = (mk g) 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 g : End K M
inst✝¹ : FiniteDimensional K M
inst✝ : PerfectField K
comm : Commute f g
hf : f.IsSemisimple
hg : g.IsSemisimple
a : End K M
ha : a ∈ K[f, g]
R : Type u_3 := K[X] ⧸ Ideal.span {minpoly K f}
S : Type u_3 := AdjoinRoot (map (algebraMap K R) (minpoly K g))
this✝⁴ : Module.Finite K R
this✝³ : Module.Finite R S
this✝² : Module.Finite K S
this✝¹ : IsArtinianRing R
this✝ : IsReduced R
this : IsReduced S
a✝ : R
p : K[X]
k : K
⊢ Commute
    ((Ideal.Quotient.liftₐ (Ideal.span {minpoly K f}) (aeval f) ⋯)
      (Quot.mk (⇑(Submodule.quotientRel (Ideal.span {minpoly K f}))) (C k)))
    g

Tactic:
simp [R, commute_algebraMap_left]

Goal state after:
Module: Mathlib.LinearAlgebra.JordanChevalley

Goal state before:
pp: case h
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] := ⋯
P' : K[X] := ⋯
⊢ (aeval ff) P ^ k = 0

Tactic:
obtain ⟨q, hq⟩ := nil

Goal state after:
case h
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
ff : ↥K[f] := ⟨f, ⋯⟩
P' : K[X] := derivative P
q : K[X]
hq : P ^ k = minpoly K f * q
⊢ (aeval ff) P ^ k = 0
Module: Mathlib.LinearAlgebra.JordanChevalley

Goal state before:
pp: case h
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
ff : ↥K[f] := ⟨f, ⋯⟩
P' : K[X] := derivative P
q : K[X]
hq : P ^ k = minpoly K f * q
⊢ ↑((aeval ff) (P ^ k)) = ↑0

Tactic:
simp [ff, hq]

Goal state after:
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 : IsNilpotent ((aeval x) P)
h' : IsUnit ((aeval x) (derivative P))
⊢ ∃! r, IsNilpotent (x - r) ∧ (aeval r) P = 0

Tactic:
by
  simp_rw [(neg_sub _ x).symm, isNilpotent_neg_iff]
  refine existsUnique_of_exists_of_unique ?_ fun r₁ r₂ ⟨hr₁, hr₁'⟩ ⟨hr₂, hr₂'⟩ ↦ ?_
  · -- Existence
    obtain ⟨n, hn⟩ := id h
    refine ⟨P.newtonMap^[n] x, isNilpotent_iterate_newtonMap_sub_of_isNilpotent h n, ?_⟩
    rw [← zero_dvd_iff, ← pow_eq_zero_of_le (n.lt_two_pow_self).le hn]
    exact aeval_pow_two_pow_dvd_aeval_iterate_newtonMap h h' n
  · -- 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.Lie.TensorProduct

Goal state before:
pp: R : Type u
inst✝⁶ : CommRing R
L : Type v
M : Type w
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
N : LieSubmodule R L M
⊢ ⁅I, N⁆ = ((toModuleHom R L M).comp (mapIncl I N)).range

Tactic:
← toSubmodule_inj,

Goal state after:
R : Type u
inst✝⁶ : CommRing R
L : Type v
M : Type w
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
N : LieSubmodule R L M
⊢ ↑⁅I, N⁆ = ↑((toModuleHom R L M).comp (mapIncl I N)).range
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✝⁷ : 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
⊢ baseChange A ⁅I, N⁆ = ⁅baseChange A I, baseChange A N⁆

Tactic:
← toSubmodule_inj,

Goal state after:
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
⊢ ↑(baseChange A ⁅I, N⁆) = ↑⁅baseChange A I, baseChange A N⁆
Module: Mathlib.Algebra.Polynomial.GroupRingAction

Goal state before:
pp: G : Type u_2
inst✝³ : Group G
inst✝² : Fintype G
R : Type u_3
inst✝¹ : CommRing R
inst✝ : MulSemiringAction G R
x : R
g : G
this : DecidableEq R := Classical.decEq R
g' : G ⧸ stabilizer G x
⊢ g • (X - C (ofQuotientStabilizer G x g')) = X - C (g • ofQuotientStabilizer G x g')

Tactic:
smul_sub,

Goal state after:
G : Type u_2
inst✝³ : Group G
inst✝² : Fintype G
R : Type u_3
inst✝¹ : CommRing R
inst✝ : MulSemiringAction G R
x : R
g : G
this : DecidableEq R := Classical.decEq R
g' : G ⧸ stabilizer G x
⊢ g • X - g • C (ofQuotientStabilizer G x g') = X - C (g • ofQuotientStabilizer G x g')
Module: Mathlib.Algebra.Lie.Nilpotent

Goal state before:
pp: R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
N₁ N₂ : LieSubmodule R L M
inst✝ : LieModule R L M
k : ℕ
⊢ lcs k N₁ ≤ N₂ ↔ N₁ ≤ ucs k N₂

Tactic:
convert! lcs_add_le_iff (R := R) (L := L) (M := M) 0 k

Goal state after:
case e'_1.e'_3.e'_10
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
N₁ N₂ : LieSubmodule R L M
inst✝ : LieModule R L M
k : ℕ
⊢ k = 0 + k
Module: Mathlib.FieldTheory.Fixed

Goal state before:
pp: G : Type u
inst✝² : Group G
F : Type v
inst✝¹ : Field F
inst✝ : MulSemiringAction G F
s : Finset F
⊢ LinearIndepOn (↥(subfield G F)) id ↑s → LinearIndepOn F ⇑(toFun G F) ↑s

Tactic:
classical
  have : IsEmpty ((∅ : Finset F) : Set F) := by simp
  refine Finset.induction_on s (fun _ => linearIndependent_empty_type) fun a s has ih hs => ?_
  rw [coe_insert] at hs ⊢
  rw [linearIndepOn_insert (mt mem_coe.1 has)] at hs
  rw [linearIndepOn_insert (mt mem_coe.1 has)]; refine ⟨ih hs.1, fun ha => ?_⟩
  rw [Finsupp.mem_span_image_iff_linearCombination] at ha; rcases ha with ⟨l, hl, hla⟩
  rw [Finsupp.linearCombination_apply_of_mem_supported F hl] at hla
  suffices ∀ i ∈ s, l i ∈ FixedPoints.subfield G F by
    replace hla := (sum_apply _ _ fun i => l i • toFun G F i).symm.trans (congr_fun hla 1)
    simp_rw [Pi.smul_apply, toFun_apply, one_smul] at hla
    refine hs.2 (hla ▸ Submodule.sum_mem _ fun c hcs => ?_)
    change (⟨l c, this c hcs⟩ : FixedPoints.subfield G F) • c ∈ _
    exact Submodule.smul_mem _ _ <| Submodule.subset_span <| by simpa
  intro i his g
  refine
    eq_of_sub_eq_zero
      (linearIndependent_iff'.1 (ih hs.1) s.attach (fun i => g • l i - l i) ?_ ⟨i, his⟩
          (mem_attach _ _) :
        _)
  refine (sum_attach s fun i ↦ (g • l i - l i) • MulAction.toFun G F i).trans ?_
  ext g'
  conv_lhs =>
    rw [Finset.sum_apply]
    congr
    · skip
    · ext
      rw [Pi.smul_apply, sub_smul, smul_eq_mul]
  rw [sum_sub_distrib, Pi.zero_apply, sub_eq_zero]
  conv_lhs =>
    congr
    · skip
    · ext x
      rw [toFun_apply, ← mul_inv_cancel_left g g', mul_smul, ← smul_mul', ← toFun_apply _ x]
  change
    (∑ x ∈ s, g • (fun y => l y • MulAction.toFun G F y) x (g⁻¹ * g')) =
      ∑ x ∈ s, (fun y => l y • MulAction.toFun G F y) x g'
  rw [← smul_sum, ← sum_apply _ _ fun y => l y • toFun G F y, ←
    sum_apply _ _ fun y => l y • toFun G F y]
  rw [hla, toFun_apply, toFun_apply, smul_smul, mul_inv_cancel_left]

Goal state after:
Module: Mathlib.FieldTheory.Normal.Defs

Goal state before:
pp: F : Type u_6
K : Type u_7
inst✝³ : Field F
inst✝² : Field K
inst✝¹ : Algebra F K
inst✝ : Normal F K
f : Gal(K/F)
x : K
⊢ (algebraMap K K) ((f.restrictNormal K) x) = (algebraMap K K) (f x)

Tactic:
rw [AlgEquiv.restrictNormal_commutes]

Goal state after:
F : Type u_6
K : Type u_7
inst✝³ : Field F
inst✝² : Field K
inst✝¹ : Algebra F K
inst✝ : Normal F K
f : Gal(K/F)
x : K
⊢ f ((algebraMap K K) x) = (algebraMap K K) (f x)
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra

Goal state before:
pp: F : Type u_1
inst✝⁴ : Field F
E : Type u_2
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : EssFiniteType F E
inst✝ : Algebra.IsAlgebraic F E
⊢ Module.Finite F E

Tactic:
obtain ⟨s, hs⟩ := fg_top F E

Goal state after:
F : Type u_1
inst✝⁴ : Field F
E : Type u_2
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : EssFiniteType F E
inst✝ : Algebra.IsAlgebraic F E
s : Finset E
hs : adjoin F ↑s = ⊤
⊢ Module.Finite F E
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
S : Set E
K : Subfield E
HF : Set.range ⇑(algebraMap F E) ⊆ ↑K
HS : S ⊆ ↑K
⊢ (adjoin F S).toSubfield ≤ K

Tactic:
simpa using ⟨HF, HS⟩

Goal state after:
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
L L' : IntermediateField F ↥K
⊢ lift (L ⊔ L') = lift L ⊔ lift L'

Tactic:
simp [lift, map_sup]

Goal state after:
Module: Mathlib.FieldTheory.IsAlgClosed.Spectrum

Goal state before:
pp: R : Type u
A : Type v
inst✝³ : CommRing R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : IsDomain R
p : R[X]
a : A
h : ¬IsUnit ((aeval a) (Multiset.map (fun x ↦ X - C x) p.roots).prod)
⊢ ∃ k ∈ σ a, eval k p = 0

Tactic:
rw [← Multiset.prod_toList, map_list_prod] at h
  replace h := mt List.prod_isUnit h
  simp only [not_forall, exists_prop, aeval_C, Multiset.mem_toList, List.mem_map, aeval_X,
    exists_exists_and_eq_and, Multiset.mem_map, map_sub] at h
  rcases h with ⟨r, r_mem, r_nu⟩
  exact ⟨r, by rwa [mem_iff, ← IsUnit.sub_iff], (mem_roots'.1 r_mem).2⟩

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

Goal state before:
pp: case h
k : Type u
inst✝² : Field k
k' : Type u
inst✝¹ : Field k'
e : k ≃+* k'
inst✝ : IsAlgClosed k
p : k'[X]
x : k
⊢ e.symm (eval (e x) p) = eval x (map e.symm.toRingHom p)

Tactic:
induction p using Polynomial.induction_on

Goal state after:
case h.C
k : Type u
inst✝² : Field k
k' : Type u
inst✝¹ : Field k'
e : k ≃+* k'
inst✝ : IsAlgClosed k
x : k
a✝ : k'
⊢ e.symm (eval (e x) (C a✝)) = eval x (map e.symm.toRingHom (C a✝))

case h.add
k : Type u
inst✝² : Field k
k' : Type u
inst✝¹ : Field k'
e : k ≃+* k'
inst✝ : IsAlgClosed k
x : k
p✝ q✝ : k'[X]
a✝¹ : e.symm (eval (e x) p✝) = eval x (map e.symm.toRingHom p✝)
a✝ : e.symm (eval (e x) q✝) = eval x (map e.symm.toRingHom q✝)
⊢ e.symm (eval (e x) (p✝ + q✝)) = eval x (map e.symm.toRingHom (p✝ + q✝))

case h.monomial
k : Type u
inst✝² : Field k
k' : Type u
inst✝¹ : Field k'
e : k ≃+* k'
inst✝ : IsAlgClosed k
x : k
n✝ : ℕ
a✝¹ : k'
a✝ : e.symm (eval (e x) (C a✝¹ * X ^ n✝)) = eval x (map e.symm.toRingHom (C a✝¹ * X ^ n✝))
⊢ e.symm (eval (e x) (C a✝¹ * X ^ (n✝ + 1))) = eval x (map e.symm.toRingHom (C a✝¹ * X ^ (n✝ + 1)))
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic

Goal state before:
pp: case refine_2
K : Type u_1
L : Type u_2
E : Type u_3
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Field E
inst✝³ : Algebra K L
inst✝² : Algebra K E
inst✝¹ : Algebra L E
inst✝ : IsScalarTower K L E
E' : IntermediateField L E
s : Finset E
hs : adjoin K ↑s = restrictScalars K E'
⊢ E' ≤ adjoin L ↑s

Tactic:
· rw [← restrictScalars_le_iff K, ← hs, adjoin_le_iff]
    exact subset_adjoin L _

Goal state after:
Module: Mathlib.FieldTheory.Extension

Goal state before:
pp: F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
c : Set (Lifts F E K)
hc : IsChain (fun x1 x2 ↦ x1 ≤ x2) c
⊢ ∀ (i : ↑(insert ⊥ c)), (↑i).carrier ≤ ⨆ i, (↑i).carrier

Tactic:
rintro ⟨i, rfl | hi⟩; exacts [bot_le, le_iSup_of_le ⟨i, hi⟩ le_rfl]

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

Goal state before:
pp: M : Type w
inst✝¹ : Field M
inst✝ : IsAlgClosed M
p : M[X]
hp : 0 < p.degree
x y : M
hy : eval y (p - C x) = 0
⊢ (fun x ↦ eval x p) y = x

Tactic:
by simpa [eval_sub, sub_eq_zero] using hy

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

Goal state before:
pp: case pos
K : Type u_1
inst✝² : Field K
inst✝¹ : IsAlgClosed K
inst✝ : CharZero K
f g : K[X]
hf0 : f ≠ 0
hg0 : ¬g = 0
hdf0 : ¬derivative f = 0
hdg : derivative f * g ≠ 0
a : K
haf : eval a f = 0
⊢ (f.IsRoot a → g.IsRoot a) → rootMultiplicity a f ≤ rootMultiplicity a (derivative f) + rootMultiplicity a g

Tactic:
have h0 : 0 < f.rootMultiplicity a := (rootMultiplicity_pos hf0).2 haf

Goal state after:
case pos
K : Type u_1
inst✝² : Field K
inst✝¹ : IsAlgClosed K
inst✝ : CharZero K
f g : K[X]
hf0 : f ≠ 0
hg0 : ¬g = 0
hdf0 : ¬derivative f = 0
hdg : derivative f * g ≠ 0
a : K
haf : eval a f = 0
h0 : 0 < rootMultiplicity a f
⊢ (f.IsRoot a → g.IsRoot a) → rootMultiplicity a f ≤ rootMultiplicity a (derivative f) + rootMultiplicity a g