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

Goal state before:
pp: case refine_1
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
hI : IsLieAbelian ↥I
x : L
hx : x ∈ I
y : ↥I
this : ⁅⟨x, hx⟩, y⁆ = 0
⊢ ↑(((toEnd R L ↥I) x) y) = ↑(0 y)

Tactic:
rw [LieIdeal.coe_bracket_of_module] at this

Goal state after:
case refine_1
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
hI : IsLieAbelian ↥I
x : L
hx : x ∈ I
y : ↥I
this : ⁅↑⟨x, hx⟩, y⁆ = 0
⊢ ↑(((toEnd R L ↥I) x) y) = ↑(0 y)
Module: Mathlib.Algebra.Lie.Submodule

Goal state before:
pp: R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
N : LieSubmodule R L M
m : M
hm : m ∈ ↑N
N' : Submodule R M
hN' : ∀ p ∈ {x | ∃ s, (∃ x ∈ N, lieSpan R L {x} = s) ∧ ↑s = x}, p ≤ N'
⊢ m ∈ N'

Tactic:
replace hN' : ∀ m ∈ N, lieSpan R L {m} ≤ N' := by simpa using hN'

Goal state after:
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
N : LieSubmodule R L M
m : M
hm : m ∈ ↑N
N' : Submodule R M
hN' : ∀ m ∈ N, ↑(lieSpan R L {m}) ≤ N'
⊢ m ∈ N'
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
h : minpoly A x = 1
⊢ 1 = 0

Tactic:
simpa using congr_arg (Polynomial.aeval x) h

Goal state after:
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]
x✝ : minpoly A x ∣ p
q : A[X]
hq : p = minpoly A x * q
⊢ (Polynomial.aeval x) (minpoly A x * q) = 0

Tactic:
map_mul,

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]
x✝ : minpoly A x ∣ p
q : A[X]
hq : p = minpoly A x * q
⊢ (Polynomial.aeval x) (minpoly A x) * (Polynomial.aeval x) q = 0
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
a : A[X]
hx : IsIntegral A x
hamonic : a.Monic
ha : (Polynomial.aeval x) a = 0
left✝ : a ≠ 0
c : A[X]
hu : ¬IsUnit c
he : minpoly A x = a * c
hcm : c.Monic
⊢ 0 < c.natDegree

Tactic:
refine (lt_of_not_ge fun h => hu ?_)

Goal state after:
A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
a : A[X]
hx : IsIntegral A x
hamonic : a.Monic
ha : (Polynomial.aeval x) a = 0
left✝ : a ≠ 0
c : A[X]
hu : ¬IsUnit c
he : minpoly A x = a * c
hcm : c.Monic
h : c.natDegree ≤ 0
⊢ IsUnit c
Module: Mathlib.Algebra.Jordan.Basic

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

Tactic:
by
  rw [add_lie, add_lie]
  iterate 15 rw [lie_add]

Goal state after:
Module: Mathlib.RingTheory.PowerBasis

Goal state before:
pp: case inl
A : Type u_4
B : Type u_5
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
pb : PowerBasis A B
b : B
h✝ : Subsingleton B
⊢ ∃ a, b ≡ (algebraMap A B) a [SMOD Ideal.span {pb.gen}]

pp: case inr
A : Type u_4
B : Type u_5
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
pb : PowerBasis A B
b : B
h✝ : Nontrivial B
⊢ ∃ a, b ≡ (algebraMap A B) a [SMOD Ideal.span {pb.gen}]

Tactic:
· exact ⟨0, by rw [SModEq, Subsingleton.eq_zero b, map_zero]⟩

Goal state after:
case inr
A : Type u_4
B : Type u_5
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
pb : PowerBasis A B
b : B
h✝ : Nontrivial B
⊢ ∃ a, b ≡ (algebraMap A B) a [SMOD Ideal.span {pb.gen}]
Module: Mathlib.RingTheory.PowerBasis

Goal state before:
pp: S : Type u_2
inst✝² : Ring S
A : Type u_4
inst✝¹ : CommRing A
inst✝ : Algebra A S
pb : PowerBasis A S
⊢ (aeval pb.gen) (X ^ pb.dim) - ∑ x, (aeval pb.gen) (C ((pb.basis.repr (pb.gen ^ pb.dim)) x) * X ^ ↑x) = 0

Tactic:
map_mul,

Goal state after:
S : Type u_2
inst✝² : Ring S
A : Type u_4
inst✝¹ : CommRing A
inst✝ : Algebra A S
pb : PowerBasis A S
⊢ (aeval pb.gen) (X ^ pb.dim) -
      ∑ x, (aeval pb.gen) (C ((pb.basis.repr (pb.gen ^ pb.dim)) x)) * (aeval pb.gen) (X ^ ↑x) =
    0
Module: Mathlib.RingTheory.PowerBasis

Goal state before:
pp: case neg
S : Type u_2
inst✝⁴ : Ring S
A : Type u_4
inst✝³ : CommRing A
inst✝² : Algebra A S
S' : Type u_7
inst✝¹ : Ring S'
inst✝ : Algebra A S'
pb : PowerBasis A S
y : S'
hy : (aeval y) (minpoly A pb.gen) = 0
f : A[X]
h✝ : Nontrivial A
hf : ¬f %ₘ minpoly A pb.gen = 0
this : (f %ₘ minpoly A pb.gen).natDegree < pb.dim
⊢ ∑ x ∈ Finset.range pb.dim, ((pb.basis.constr A) fun i ↦ y ^ ↑i) ((f %ₘ minpoly A pb.gen).coeff x • pb.gen ^ x) =
    ∑ i ∈ Finset.range pb.dim, (f %ₘ minpoly A pb.gen).coeff i • y ^ i

Tactic:
refine Finset.sum_congr rfl fun i (hi : i ∈ Finset.range pb.dim) => ?_

Goal state after:
case neg
S : Type u_2
inst✝⁴ : Ring S
A : Type u_4
inst✝³ : CommRing A
inst✝² : Algebra A S
S' : Type u_7
inst✝¹ : Ring S'
inst✝ : Algebra A S'
pb : PowerBasis A S
y : S'
hy : (aeval y) (minpoly A pb.gen) = 0
f : A[X]
h✝ : Nontrivial A
hf : ¬f %ₘ minpoly A pb.gen = 0
this : (f %ₘ minpoly A pb.gen).natDegree < pb.dim
i : ℕ
hi : i ∈ Finset.range pb.dim
⊢ ((pb.basis.constr A) fun i ↦ y ^ ↑i) ((f %ₘ minpoly A pb.gen).coeff i • pb.gen ^ i) =
    (f %ₘ minpoly A pb.gen).coeff i • y ^ i
Module: Mathlib.FieldTheory.KummerPolynomial

Goal state before:
pp: K : Type u
inst✝ : Field K
n : ℕ
a : K
⊢ root (X ^ n - C a) ^ n = (of (X ^ n - C a)) a

Tactic:
rw [← sub_eq_zero, ← AdjoinRoot.eval₂_root, eval₂_sub, eval₂_C, eval₂_pow, eval₂_X]

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

Goal state before:
pp: R : Type u_1
inst✝² : CommMonoidWithZero R
inst✝¹ : IsCancelMulZero R
x y d : R
inst✝ : DecompositionMonoid R
hx : Squarefree x
h : d * d ∣ x * y
a✝ : Nontrivial R
a b : R
hb : b ∣ y
eq : d * d = a * b
ha : Squarefree a
c : R
hc : d = a * c
⊢ d ∣ y

Tactic:
rw [hc, mul_assoc, (mul_right_injective₀ ha.ne_zero).eq_iff] at eq

Goal state after:
R : Type u_1
inst✝² : CommMonoidWithZero R
inst✝¹ : IsCancelMulZero R
x y d : R
inst✝ : DecompositionMonoid R
hx : Squarefree x
h : d * d ∣ x * y
a✝ : Nontrivial R
a b : R
hb : b ∣ y
ha : Squarefree a
c : R
eq : c * (a * c) = b
hc : d = a * c
⊢ d ∣ y
Module: Mathlib.LinearAlgebra.AnnihilatingPolynomial

Goal state before:
pp: 𝕜 : 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
⊢ annIdealGenerator 𝕜 a = p

Tactic:
by_cases h : p = 0

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
⊢ annIdealGenerator 𝕜 a = p

case neg
𝕜 : 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 = p
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommSemiring S
inst✝² : Semiring T
inst✝¹ : Algebra S R
inst✝ : Algebra S T
p : R[X]
f g : AdjoinRoot p →ₐ[S] T
hAlg : f.comp (ofAlgHom S p) = g.comp (ofAlgHom S p)
hRoot : f (root p) = g (root p)
⊢ ↑f = ↑g

Tactic:
exact ringHom_ext congr(($hAlg).toRingHom) hRoot

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
inst✝¹ : Free R M
inst✝ : Module.Finite R M
f : M →ₗ[R] M
h : IsUnit (LinearMap.det f)
⊢ M ≃ₗ[R] M

Tactic:
by_cases hR : Nontrivial R
  · let ⟨ι, b⟩ := (Module.Free.exists_basis R M).some
    have : Finite ι := Module.Finite.finite_basis b
    have : Fintype ι := Fintype.ofFinite ι
    have : DecidableEq ι := Classical.typeDecidableEq ι
    exact LinearEquiv.ofIsUnitDet (v := b) (v' := b) (f := f) (by rwa [det_toMatrix b])
  · exact 1

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
f g✝ : R[X]
inst✝ : CommRing S
i : R →+* S
x : S
h : eval₂ i x f = 0
g : R[X]
H : g ∈ span {f}
y : R[X]
hy : g = f * y
⊢ (eval₂RingHom i x) (f * y) = 0

Tactic:
map_mul,

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst✝¹ : CommRing R
f g✝ : R[X]
inst✝ : CommRing S
i : R →+* S
x : S
h : eval₂ i x f = 0
g : R[X]
H : g ∈ span {f}
y : R[X]
hy : g = f * y
⊢ (eval₂RingHom i x) f * (eval₂RingHom i x) y = 0
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
⊢ (lift i a h) ((mk f) X) = a

Tactic:
lift_mk,

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
⊢ eval₂ i a X = a
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) ((mk f) (C x)) = i x

Tactic:
lift_mk,

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
⊢ eval₂ i a (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
N : Type u_5
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : N →ₗ[R] M
e e' : M ≃ₗ[R] N
⊢ Associated (LinearMap.det (f ∘ₗ ↑e)) (LinearMap.det (f ∘ₗ ↑e'))

Tactic:
by
  refine LinearMap.associated_det_of_eq_comp (e.trans e'.symm) _ _ ?_
  intro x
  simp only [LinearMap.comp_apply, LinearEquiv.coe_coe, LinearEquiv.trans_apply,
    LinearEquiv.apply_symm_apply]

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
f✝ g✝ : R[X]
inst✝⁵ : CommRing S
i : R →+* S
a : S
h : eval₂ i a f✝ = 0
inst✝⁴ : CommRing T
inst✝³ : CommRing U
inst✝² : Algebra R S
inst✝¹ : Algebra R T
inst✝ : Algebra R U
f : S →ₐ[R] T
g : T →ₐ[R] U
p : S[X]
q : T[X]
r : U[X]
hf : q ∣ Polynomial.map (↑f) p
hg : r ∣ Polynomial.map (↑g) q
⊢ Polynomial.map (↑g) q ∣ Polynomial.map (↑(g.comp f)) p

Tactic:
simpa [Polynomial.map_map] using! Polynomial.map_dvd g.toRingHom hf

Goal state after:
Module: Mathlib.RingTheory.AdjoinRoot

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

Tactic:
map_mul,

Goal state after:
case refine_1
K : Type u_5
inst✝ : Field K
f : K[X]
hf : f ≠ 0
f'_monic : (f * C f.leadingCoeff⁻¹).Monic
⊢ (aeval (root f)) f * (aeval (root f)) (C f.leadingCoeff⁻¹) = 0
Module: Mathlib.Algebra.Lie.Derivation.Basic

Goal state before:
pp: case lie
R : Type u_1
L : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
D1 D2 : LieDerivation R L M
s : Set L
h : Set.EqOn (⇑D1) (⇑D2) s
x✝ x y : L
hx✝ : x ∈ LieSubalgebra.lieSpan R L s
hy✝ : y ∈ LieSubalgebra.lieSpan R L s
hx : D1 x = D2 x
hy : D1 y = D2 y
⊢ D1 ⁅x, y⁆ = D2 ⁅x, y⁆

Tactic:
| lie x y _ _ hx hy =>

Goal state after:
Module: Mathlib.RingTheory.AdjoinRoot

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

Tactic:
simp [quotientEquivQuotientMinpolyMap, aeval_def]

Goal state after:
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
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)
⊢ q.natDegree < ((X - C (AdjoinRoot.root p)) * q).natDegree

Tactic:
Monic.natDegree_mul (monic_X_sub_C _) hqm

Goal state after:
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)
⊢ q.natDegree < (X - C (AdjoinRoot.root p)).natDegree + q.natDegree
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: case h
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
⊢ ∃ S x x_1, ∃ (_ : Module.Finite R S) (_ : Free R S) (_ : Nontrivial S), (Polynomial.map (algebraMap R S) p).Splits

Tactic:
by_cases hpu : IsUnit p
  · obtain rfl := hp.eq_one_of_isUnit hpu
    exact ⟨R, inferInstance, inferInstance, inferInstance, inferInstance, inferInstance, by simp⟩
  obtain ⟨q, hq⟩ : X - C (AdjoinRoot.root p) ∣ p.map (algebraMap _ _) := by
    simp [dvd_iff_isRoot, -AdjoinRoot.algebraMap_eq]
  have hqm : q.Monic := .of_mul_monic_left (monic_X_sub_C (.root _)) (hq ▸ hp.map _)
  have := hp.free_adjoinRoot
  have := hp.finite_adjoinRoot
  have : Nontrivial (AdjoinRoot p) := Ideal.Quotient.nontrivial_iff.mpr (by simpa)
  obtain ⟨S, _, _, _, _, _, hS⟩ := IH _
    (by rw [← hn, ← hp.natDegree_map (algebraMap R (AdjoinRoot p)), hq,
      Monic.natDegree_mul (monic_X_sub_C _) hqm]; simp) hqm rfl
  algebraize [(algebraMap (AdjoinRoot p) S).comp (algebraMap R (AdjoinRoot p))]
  refine ⟨S, ‹_›, ‹_›, .trans (AdjoinRoot p) _, .trans (S := AdjoinRoot p), ‹_›, ?_⟩
  rw [IsScalarTower.algebraMap_eq R (AdjoinRoot p), ← Polynomial.map_map, hq, Polynomial.map_mul]
  exact .mul (by simp) hS

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

Goal state before:
pp: case inl
R : Type u_1
x y : R
n m p : ℕ
inst✝ : Semiring R
hp : n + m ≤ p + 1
h_comm : Commute x y
hy : y ^ n = 0
x✝ : ℕ × ℕ
i j : ℕ
hij : i + j = p
hi : m ≤ i
⊢ x ^ m ∣ x ^ (i, j).1 * y ^ (i, j).2

Tactic:
exact dvd_mul_of_dvd_left (pow_dvd_pow x hi) _

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

Goal state before:
pp: R : Type u_1
L : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
N N' : LieSubmodule R L M
⊢ ⁅⊤, N⁆ ≤ N' ↔ N ≤ N'.normalizer

Tactic:
rw [lie_le_iff]; tauto

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✝ : IsArtinian R M
h_wf : WellFoundedGT (LieSubmodule R L M)ᵒᵈ
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → lowerCentralSeries R L M n = lowerCentralSeries R L M m
l : ℕ
hl : n ≤ l
m : ℕ
⊢ lowerCentralSeries R L M l ≤ lowerCentralSeries R L M m

Tactic:
rcases le_or_gt l m with h | h

Goal state after:
case inl
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✝ : IsArtinian R M
h_wf : WellFoundedGT (LieSubmodule R L M)ᵒᵈ
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → lowerCentralSeries R L M n = lowerCentralSeries R L M m
l : ℕ
hl : n ≤ l
m : ℕ
h : l ≤ m
⊢ lowerCentralSeries R L M l ≤ lowerCentralSeries R L M m

case inr
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✝ : IsArtinian R M
h_wf : WellFoundedGT (LieSubmodule R L M)ᵒᵈ
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → lowerCentralSeries R L M n = lowerCentralSeries R L M m
l : ℕ
hl : n ≤ l
m : ℕ
h : m < l
⊢ lowerCentralSeries R L M l ≤ lowerCentralSeries R L M m
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✝ : IsNoetherian R L
M : Type u_1
_i1 : AddCommGroup M
_i2 : Module R M
_i3 : LieRingModule L M
_i4 : LieModule R L M
L' : LieSubalgebra R (Module.End R M) := (toEnd R L M).range
h : ∀ (y : ↥L'), IsNilpotent ↑y
s : Set (LieSubalgebra R ↥L') := {K | IsEngelian R ↥K}
hs : s.Nonempty
this : ⊤ ∈ s
⊢ LieModule.IsNilpotent (↥L') M

Tactic:
rw [← isNilpotent_of_top_iff (R := R)]

Goal state after:
R : Type u₁
L : Type u₂
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsNoetherian R L
M : Type u_1
_i1 : AddCommGroup M
_i2 : Module R M
_i3 : LieRingModule L M
_i4 : LieModule R L M
L' : LieSubalgebra R (Module.End R M) := (toEnd R L M).range
h : ∀ (y : ↥L'), IsNilpotent ↑y
s : Set (LieSubalgebra R ↥L') := {K | IsEngelian R ↥K}
hs : s.Nonempty
this : ⊤ ∈ s
⊢ LieModule.IsNilpotent (↥⊤) M
Module: Mathlib.Algebra.Lie.Nilpotent

Goal state before:
pp: case h
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
L₂ : Type u_1
M₂ : Type u_2
inst✝⁶ : LieRing L₂
inst✝⁵ : LieAlgebra R L₂
inst✝⁴ : AddCommGroup M₂
inst✝³ : Module R M₂
inst✝² : LieRingModule L₂ M₂
f : L →ₗ⁅R⁆ L₂
g : M →ₗ[R] M₂
hfg : ∀ (x : L) (m : M), ⁅f x, g m⁆ = g ⁅x, m⁆
inst✝¹ : LieModule R L₂ M₂
hg_inj : Injective ⇑g
inst✝ : LieModule.IsNilpotent L₂ M₂
k : ℕ
hk : ↑(lowerCentralSeries R L₂ M₂ k) = ↑⊥
⊢ Submodule.map g ↑(lowerCentralSeries R L M k) = Submodule.map g ↑⊥

Tactic:
simpa [hk] using lieModule_lcs_map_le hfg k

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

Goal state before:
pp: F : Type u_1
inst✝³ : Field F
K₁ : Type u_3
inst✝² : Field K₁
inst✝¹ : Algebra F K₁
L : IntermediateField F K₁
inst✝ : Normal F ↥L
σ : Gal(K₁/F)
⊢ σ.restrictNormal ↥L = 1 ↔ ∀ x ∈ L, σ x = x

Tactic:
simp [AlgEquiv.ext_iff, Subtype.ext_iff, AlgEquiv.restrictNormal_apply]

Goal state after:
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₁⁻¹ * g₂) = 1

Tactic:
map_mul,

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₂ = 1
Module: Mathlib.RingTheory.Adjoin.Field

Goal state before:
pp: case refine_2
F : Type u_2
K : Type u_3
L : Type u_4
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra F K
inst✝ : Algebra F L
s✝ : Finset K
a : K
s : Finset K
x✝ : a ∉ s
ih : (∀ x ∈ s, IsIntegral F x ∧ (map (algebraMap F L) (minpoly F x)).Splits) → Nonempty (↥(Algebra.adjoin F ↑s) →ₐ[F] L)
H :
  (IsIntegral F a ∧ (map (algebraMap F L) (minpoly F a)).Splits) ∧
    ∀ x ∈ s, IsIntegral F x ∧ (map (algebraMap F L) (minpoly F x)).Splits
⊢ Nonempty (↥(Algebra.adjoin F ↑(insert a s)) →ₐ[F] L)

Tactic:
rcases H with ⟨⟨H1, H2⟩, H3⟩

Goal state after:
case refine_2
F : Type u_2
K : Type u_3
L : Type u_4
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra F K
inst✝ : Algebra F L
s✝ : Finset K
a : K
s : Finset K
x✝ : a ∉ s
ih : (∀ x ∈ s, IsIntegral F x ∧ (map (algebraMap F L) (minpoly F x)).Splits) → Nonempty (↥(Algebra.adjoin F ↑s) →ₐ[F] L)
H3 : ∀ x ∈ s, IsIntegral F x ∧ (map (algebraMap F L) (minpoly F x)).Splits
H1 : IsIntegral F a
H2 : (map (algebraMap F L) (minpoly F a)).Splits
⊢ Nonempty (↥(Algebra.adjoin F ↑(insert a s)) →ₐ[F] L)
Module: Mathlib.RingTheory.Adjoin.Field

Goal state before:
pp: case refine_2
F : Type u_2
K : Type u_3
L : Type u_4
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra F K
inst✝ : Algebra F L
s✝ : Finset K
a : K
s : Finset K
x✝ : a ∉ s
ih : (∀ x ∈ s, IsIntegral F x ∧ (map (algebraMap F L) (minpoly F x)).Splits) → Nonempty (↥(Algebra.adjoin F ↑s) →ₐ[F] L)
H3 : ∀ x ∈ s, IsIntegral F x ∧ (map (algebraMap F L) (minpoly F x)).Splits
H1 : IsIntegral F a
H2 : (map (algebraMap F L) (minpoly F a)).Splits
f : ↥(Algebra.adjoin F ↑s) →ₐ[F] L
⊢ Nonempty (↥(Algebra.adjoin F ↑(insert a s)) →ₐ[F] L)

Tactic:
choose H3 _ using H3

Goal state after:
case refine_2
F : Type u_2
K : Type u_3
L : Type u_4
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra F K
inst✝ : Algebra F L
s✝ : Finset K
a : K
s : Finset K
x✝ : a ∉ s
ih : (∀ x ∈ s, IsIntegral F x ∧ (map (algebraMap F L) (minpoly F x)).Splits) → Nonempty (↥(Algebra.adjoin F ↑s) →ₐ[F] L)
H1 : IsIntegral F a
H2 : (map (algebraMap F L) (minpoly F a)).Splits
f : ↥(Algebra.adjoin F ↑s) →ₐ[F] L
H3 : ∀ x ∈ s, IsIntegral F x
a✝ : ∀ x ∈ s, (map (algebraMap F L) (minpoly F x)).Splits
⊢ Nonempty (↥(Algebra.adjoin F ↑(insert a s)) →ₐ[F] L)
Module: Mathlib.FieldTheory.SplittingField.IsSplittingField

Goal state before:
pp: K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
p : K[X]
F : IntermediateField K L
h : (Polynomial.map (algebraMap K L) p).Splits
hF : ∀ x ∈ p.rootSet L, x ∈ F
⊢ (Polynomial.map (algebraMap K ↥F) p).Splits

Tactic:
by
  classical
  have := Splits.of_splits_map (f := p.map (algebraMap K F)) (algebraMap F L)
  rw [Polynomial.map_map, ← IsScalarTower.algebraMap_eq] at this
  exact this h (by simpa [rootSet_def] using hF)

Goal state after:
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs

Goal state before:
pp: case a.right
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
S T : Set E
⊢ T ⊆ ↑(adjoin F (S ∪ T))

Tactic:
exact subset_adjoin_of_subset_right _ _ Set.subset_union_right

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
S : Set E
⊢ restrictScalars F (adjoin (↥K) S) = adjoin F (↑K ∪ S)

Tactic:
rw [← adjoin_self _ K, adjoin_adjoin_left, adjoin_self _ K]

Goal state after: