mathlib-initiative/mathlib-tactics huggingface dataset:
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
inst✝ : Nontrivial R
x : S
hx : IsIntegral R x
f : R[X]
this : (minpoly R x).Monic
| (aeval x) f

Tactic:
← modByMonic_add_div f (minpoly R x)

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : Ring S
inst✝¹ : Algebra R S
inst✝ : Nontrivial R
x : S
hx : IsIntegral R x
f : R[X]
this : (minpoly R x).Monic
| (aeval x) (f %ₘ minpoly R x + minpoly R x * (f /ₘ minpoly R x))
Module: Mathlib.FieldTheory.KummerPolynomial

Goal state before:
pp: K : Type u
inst✝ : Field K
n : ℕ
hn : n ≠ 1
H : Irreducible (X ^ n - 0)
⊢ False

Tactic:
sub_zero

Goal state after:
K : Type u
inst✝ : Field K
n : ℕ
hn : n ≠ 1
H : Irreducible (X ^ n)
⊢ False
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: R : Type u
inst✝¹ : CommSemiring R
inst✝ : Subsingleton R
f : R[X]
⊢ f.Separable

Tactic:
simp [Separable, IsCoprime, eq_iff_true_of_subsingleton]

Goal state after:
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: F : Type u
inst✝ : Field F
f : F[X]
hf : Irreducible f
h : derivative f ≠ 0
g : F[X]
hg1 : g ∈ nonunits F[X]
_hg2 : g ≠ 0
x✝ : g ∣ f
hg4 : g ∣ derivative f
p : F[X]
hg3 : f = g * p
u : F[X]ˣ
hu : ↑u = p
| f

Tactic:
hg3,

Goal state after:
F : Type u
inst✝ : Field F
f : F[X]
hf : Irreducible f
h : derivative f ≠ 0
g : F[X]
hg1 : g ∈ nonunits F[X]
_hg2 : g ≠ 0
x✝ : g ∣ f
hg4 : g ∣ derivative f
p : F[X]
hg3 : f = g * p
u : F[X]ˣ
hu : ↑u = p
| g * p
Module: Mathlib.LinearAlgebra.Determinant

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b : Basis ι R M
f : Matrix ι ι R
⊢ LinearMap.det ((toLin b b) f) = f.det

Tactic:
by
  rw [← LinearMap.det_toMatrix b, LinearMap.toMatrix_toLin]

Goal state after:
Module: Mathlib.FieldTheory.Perfect

Goal state before:
pp: R : Type u_1
p m n : ℕ
inst✝² : CommSemiring R
inst✝¹ : ExpChar R p
inst✝ : PerfectRing R p
x : R
⊢ (iterateFrobeniusEquiv R p (m + n)) ((iterateFrobeniusEquiv R p (m + n)).symm x) =
    (iterateFrobeniusEquiv R p (m + n)) ((iterateFrobeniusEquiv R p m).symm ((iterateFrobeniusEquiv R p n).symm x))

Tactic:
by rw [RingEquiv.apply_symm_apply, add_comm,
    iterateFrobeniusEquiv_add_apply, RingEquiv.apply_symm_apply, RingEquiv.apply_symm_apply]

Goal state after:
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:
rw [← Function.comp_apply (f := (⇑(frobenius R p))^[n]),
          ← Function.comp_apply (f := (⇑(frobenius S p))^[n]),
          ← Function.Commute.comp_iterate, ← Function.Commute.comp_iterate]
      · simp
      all_goals rw [← coe_frobeniusEquiv]; simp [Function.Commute, Function.Semiconj]

Goal state after:
Module: Mathlib.FieldTheory.Perfect

Goal state before:
pp: K : Type u_1
p : ℕ
inst✝² : Field K
inst✝¹ : ExpChar K p
inst✝ : PerfectRing K p
⊢ PerfectField K

Tactic:
by
  obtain hp | ⟨hp⟩ := ‹ExpChar K p›
  · exact ⟨Irreducible.separable⟩
  refine PerfectField.mk fun hf ↦ ?_
  rcases separable_or p hf with h | ⟨-, g, -, rfl⟩
  · assumption
  · exfalso; revert hf; have := Fact.mk hp; simp

Goal state after:
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]
⊢ Multiset.map (⇑(frobenius R p)) ((expand R p) f).roots ≤ p • f.roots

Tactic:
rw [← iterateFrobenius_one]

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
p : ℕ
inst✝ : ExpChar R p
f : R[X]
⊢ Multiset.map (⇑(iterateFrobenius R p 1)) ((expand R p) f).roots ≤ p • f.roots
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]

Goal state after:
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
p : ℕ
inst✝¹ : ExpChar R p
f : R[X]
inst✝ : DecidableEq R
⊢ Finset.image (⇑(iterateFrobenius R p 1)) ((expand R p) f).roots.toFinset ⊆ f.roots.toFinset
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: F : Type u
inst✝¹ : Field F
inst✝ : CharZero F
f : F[X]
hf : Irreducible f
⊢ f.Separable

Tactic:
rw [separable_iff_derivative_ne_zero hf, Ne, ← degree_eq_bot, degree_derivative]

Goal state after:
F : Type u
inst✝¹ : Field F
inst✝ : CharZero F
f : F[X]
hf : Irreducible f
⊢ ¬↑(f.natDegree - 1) = ⊥

F : Type u
inst✝¹ : Field F
inst✝ : CharZero F
f : F[X]
hf : Irreducible f
⊢ f.natDegree ≠ 0
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f g : R[X]
⊢ f ∣ g - 0 ↔ f ∣ g

Tactic:
sub_zero

Goal state after:
R : Type u_1
inst✝ : CommRing R
f g : R[X]
⊢ f ∣ g ↔ f ∣ g
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : CommRing R
f : R[X]
inst✝ : IsDomain R
hf : f.degree ≠ 0
p : R
hp : f ∣ C p
h : ¬f = 0
⊢ p = 0

Tactic:
contrapose! hf with h_contra
    rw [← degree_C h_contra]
    apply le_antisymm (degree_le_of_dvd hp (by rwa [Ne, C_eq_zero])) _
    rwa [degree_C h_contra, zero_le_degree_iff]

Goal state after:
Module: Mathlib.LinearAlgebra.Determinant

Goal state before:
pp: case pos
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)
hR : Nontrivial R
⊢ M ≃ₗ[R] M

pp: case neg
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)
hR : ¬Nontrivial R
⊢ M ≃ₗ[R] M

Tactic:
· 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])

Goal state after:
case neg
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)
hR : ¬Nontrivial R
⊢ M ≃ₗ[R] M
Module: Mathlib.RingTheory.Nilpotent.Exp

Goal state before:
pp: case inl
A : Type u_1
inst✝⁴ : Ring A
inst✝³ : Module ℚ A
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module A M
inst✝ : Module ℚ M
a : A
m : M
k : ℕ
h : a ^ k • m = 0
hn : IsNilpotent a
h₀ : nilpotencyClass a ≤ k
⊢ ∑ i ∈ range k, ((↑i !)⁻¹ • a ^ i) • m = ∑ i ∈ range k, (↑i !)⁻¹ • a ^ i • m

Tactic:
smul_assoc

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

Goal state before:
pp: A : Type u_1
inst✝⁴ : Ring A
inst✝³ : Module ℚ A
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module A M
inst✝ : Module ℚ M
a : A
m : M
k : ℕ
h : a ^ k • m = 0
hn : IsNilpotent a
h₀ : k < nilpotencyClass a
this : ∑ i ∈ Ico k (nilpotencyClass a), ((↑i !)⁻¹ • a ^ i) • m = 0
⊢ ∑ k ∈ range k, ((↑k !)⁻¹ • a ^ k) • m = ∑ i ∈ range k, (↑i !)⁻¹ • a ^ i • m

Tactic:
smul_assoc

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
R : Type u_6
S : Type u_7
T : Type u_8
U : Type u_9
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing T
inst✝³ : Algebra R S
inst✝² : Algebra R T
inst✝¹ : CommRing U
inst✝ : Algebra R U
p✝ p : S[X]
q : (T ⊗[R] S)[X]
h : Polynomial.map includeRight.toRingHom p = q
⊢ q ∣ Polynomial.map (↑includeRight) p

Tactic:
by exact h.symm.dvd

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

Goal state before:
pp: A : Type u_1
inst✝¹ : Ring A
inst✝ : Module ℚ A
a b : A
h₁ : Commute a b
n₁ : ℕ
hn₁ : a ^ n₁ = 0
n₂ : ℕ
hn₂ : b ^ n₂ = 0
N : ℕ := max n₁ n₂
h₄ : a ^ (N + 1) = 0
h₅ : b ^ (N + 1) = 0
R2N : Finset ℕ := range (2 * N + 1)
hR2N : R2N = range (2 * N + 1)
RN : Finset ℕ := range (N + 1)
hRN : RN = range (N + 1)
i : ℕ
hi : i ∈ R2N
j : ℕ
hj : j ≤ i
this : (↑i !)⁻¹ * ↑(i.choose j) = (↑j !)⁻¹ * (↑(i - j)!)⁻¹
⊢ (i.choose j • (↑i !)⁻¹) • (a ^ j * b ^ (i - j)) = ↑(i.choose j) • (↑i !)⁻¹ • (a ^ j * b ^ (i - j))

Tactic:
smul_assoc

Goal state after:
A : Type u_1
inst✝¹ : Ring A
inst✝ : Module ℚ A
a b : A
h₁ : Commute a b
n₁ : ℕ
hn₁ : a ^ n₁ = 0
n₂ : ℕ
hn₂ : b ^ n₂ = 0
N : ℕ := max n₁ n₂
h₄ : a ^ (N + 1) = 0
h₅ : b ^ (N + 1) = 0
R2N : Finset ℕ := range (2 * N + 1)
hR2N : R2N = range (2 * N + 1)
RN : Finset ℕ := range (N + 1)
hRN : RN = range (N + 1)
i : ℕ
hi : i ∈ R2N
j : ℕ
hj : j ≤ i
this : (↑i !)⁻¹ * ↑(i.choose j) = (↑j !)⁻¹ * (↑(i - j)!)⁻¹
⊢ i.choose j • (↑i !)⁻¹ • (a ^ j * b ^ (i - j)) = ↑(i.choose j) • (↑i !)⁻¹ • (a ^ j * b ^ (i - j))
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 : (aeval x) P = 0
⊢ x - 0 = x

Tactic:
sub_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 : (aeval x) P = 0
⊢ x = x
Module: Mathlib.Algebra.Lie.Solvable

Goal state before:
pp: R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I J : LieIdeal R L
k l : ℕ
D₁ : LieIdeal R L →o LieIdeal R L := { toFun := fun I ↦ ⁅I, I⁆, monotone' := ⋯ }
h₁ : ∀ (n₁ n₂ : ℕ) (a₁ a₂ : LieIdeal R L), (⇑D₁)^[n₁ + n₂] (a₁ ⊔ a₂) ≤ (⇑D₁)^[n₁] a₁ ⊔ (⇑D₁)^[n₂] a₂
⊢ D (k + l) (I + J) ≤ D k I + D l J

Tactic:
exact h₁ k l I J

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

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
h : H.normalizer = H
m✝ : L ⧸ H.toLieSubmodule
x : L
hx : Quot.mk (⇑(↑H.toLieSubmodule).quotientRel) x ∈ LieModule.maxTrivSubmodule R (↥H) (L ⧸ H.toLieSubmodule)
this : x ∈ H
⊢ Submodule.Quotient.mk x = 0

Tactic:
Submodule.Quotient.mk_eq_zero,

Goal state after:
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
h : H.normalizer = H
m✝ : L ⧸ H.toLieSubmodule
x : L
hx : Quot.mk (⇑(↑H.toLieSubmodule).quotientRel) x ∈ LieModule.maxTrivSubmodule R (↥H) (L ⧸ H.toLieSubmodule)
this : x ∈ H
⊢ x ∈ ↑H.toLieSubmodule
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
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
⊢ s ⊆ {x | ∃ x_1 ∈ baseChange A I, ∃ n ∈ baseChange A N, ⁅x_1, n⁆ = x}

Tactic:
rintro - ⟨x, hx, m, hm, rfl⟩

Goal state after:
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
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 : L
hx : x ∈ I
m : M
hm : m ∈ N
⊢ 1 ⊗ₜ[R] ⁅x, m⁆ ∈ {x | ∃ x_1 ∈ baseChange A I, ∃ n ∈ baseChange A N, ⁅x_1, n⁆ = x}
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 | ∃ x_1 ∈ baseChange A I, ∃ n ∈ baseChange A N, ⁅x_1, n⁆ = x} ⊆ ↑(Submodule.span A s)

Tactic:
rintro - ⟨x, hx, m, hm, rfl⟩

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 ∈ baseChange A I
m : A ⊗[R] M
hm : m ∈ baseChange A N
⊢ ⁅x, m⁆ ∈ ↑(Submodule.span A s)
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 ≤ lowerCentralSeries R L M 1 ⊓ maxTrivSubmodule R L M
⊢ False

Tactic:
suffices ¬ Nontrivial (lowerCentralSeriesLast R L M) by
    exact this (nontrivial_lowerCentralSeriesLast R L M)

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 ≤ lowerCentralSeries R L M 1 ⊓ maxTrivSubmodule R L M
⊢ ¬Nontrivial ↥(lowerCentralSeriesLast R L M)
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:
by
  simp [AlgEquiv.ext_iff, Subtype.ext_iff, AlgEquiv.restrictNormal_apply]

Goal state after:
Module: Mathlib.FieldTheory.Fixed

Goal state before:
pp: case inr
G : Type u
inst✝³ : Group G
F : Type v
inst✝² : Field F
inst✝¹ : MulSemiringAction G F
inst✝ : Fintype G
x : F
f g : Polynomial ↥(subfield G F)
hf : f.Monic
hg : g.Monic
hfg : f * g = 1 * minpoly G F x
hf2 : f ∣ minpoly G F x
hg2 : g ∣ minpoly G F x
this : Polynomial.eval₂ (subfield G F).subtype x g = 0
hg3 : g = minpoly G F x
⊢ f = 1

Tactic:
hg3,

Goal state after:
case inr
G : Type u
inst✝³ : Group G
F : Type v
inst✝² : Field F
inst✝¹ : MulSemiringAction G F
inst✝ : Fintype G
x : F
f g : Polynomial ↥(subfield G F)
hf : f.Monic
hg : g.Monic
hfg : f * minpoly G F x = 1 * minpoly G F x
hf2 : f ∣ minpoly G F x
hg2 : g ∣ minpoly G F x
this : Polynomial.eval₂ (subfield G F).subtype x g = 0
hg3 : g = minpoly G F x
⊢ f = 1
Module: Mathlib.FieldTheory.Fixed

Goal state before:
pp: G : Type u_2
F : Type u_3
inst✝³ : Group G
inst✝² : Field F
inst✝¹ : MulSemiringAction G F
inst✝ : Finite G
⊢ Function.Surjective ⇑(MulSemiringAction.toAlgAut G (↥(subfield G F)) F)

Tactic:
let f : G →* F ≃ₐ[FixedPoints.subfield G F] F :=
    MulSemiringAction.toAlgAut G (FixedPoints.subfield G F) F
  let Q := G ⧸ f.ker
  let _ : MulSemiringAction Q F := MulSemiringAction.compHom _ (QuotientGroup.kerLift f)
  have : FaithfulSMul Q F := ⟨fun {q₁ q₂} ↦ by
    induction q₁, q₂ using Quotient.inductionOn₂ with | _ g₁ g₂
    intro h
    rwa [QuotientGroup.eq, MonoidHom.mem_ker, map_mul, map_inv, inv_mul_eq_one, AlgEquiv.ext_iff]⟩
  intro f
  obtain ⟨q, hq⟩ := (toAlgAut_bijective Q F).surjective
    (AlgEquiv.ofRingEquiv (f := f) (fun ⟨x, hx⟩ ↦ f.commutes' ⟨x, fun g ↦ hx g⟩))
  revert hq
  refine QuotientGroup.induction_on q (fun g hg ↦ ⟨g, ?_⟩)
  rwa [AlgEquiv.ext_iff] at hg ⊢

Goal state after:
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
S : IntermediateField F E
h : S.FG
⊢ S.FG

Tactic:
by
  obtain ⟨t, ht⟩ := h
  exact ⟨t, (eq_adjoin_of_eq_algebra_adjoin _ _ _ ht.symm).symm⟩

Goal state after:
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
this :
  (Polynomial.map (algebraMap (↥F) L) (Polynomial.map (algebraMap K ↥F) p)).Splits →
    (∀ a ∈ (Polynomial.map (algebraMap (↥F) L) (Polynomial.map (algebraMap K ↥F) p)).roots,
        a ∈ (algebraMap (↥F) L).range) →
      (Polynomial.map (algebraMap K ↥F) p).Splits
⊢ (Polynomial.map (algebraMap K ↥F) p).Splits

Tactic:
rw [Polynomial.map_map, ← IsScalarTower.algebraMap_eq] at this

Goal state after:
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
this :
  (Polynomial.map (algebraMap K L) p).Splits →
    (∀ a ∈ (Polynomial.map (algebraMap K L) p).roots, a ∈ (algebraMap (↥F) L).range) →
      (Polynomial.map (algebraMap K ↥F) p).Splits
⊢ (Polynomial.map (algebraMap K ↥F) p).Splits
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 (IntermediateField F E)
hS : S.Nonempty
x : IntermediateField F E
a✝ : x ∈ S
⊢ x.toSubfield = Subfield.closure ↑x

Tactic:
exact x.toSubfield.closure_eq.symm

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
⊢ lift ⊤ = K

Tactic:
rw [lift, ← AlgHom.fieldRange_eq_map, fieldRange_val]

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

Goal state before:
pp: case h
k : Type u
inst✝¹ : Field k
inst✝ : IsAlgClosed k
x : k
n : ℕ
hn : 0 < n
this : (X ^ n - C x).degree ≠ 0
z : k
hz : z ^ n - x = 0
⊢ z ^ n = x

Tactic:
exact sub_eq_zero.1 hz

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

Goal state before:
pp: 𝕜 : Type u
A : Type v
inst✝³ : Field 𝕜
inst✝² : Ring A
inst✝¹ : Algebra 𝕜 A
inst✝ : IsAlgClosed 𝕜
a : A
p : 𝕜[X]
hnon : (σ a).Nonempty
⊢ σ ((aeval a) p) = (fun k ↦ eval k p) '' σ a

Tactic:
nontriviality A
  refine Or.elim (le_or_gt (degree p) 0) (fun h => ?_) (map_polynomial_aeval_of_degree_pos a p)
  rw [eq_C_of_degree_le_zero h]
  simp only [eval_C, aeval_C, scalar_eq, Set.Nonempty.image_const hnon]

Goal state after:
Module: Mathlib.LinearAlgebra.Eigenspace.Pi

Goal state before:
pp: case inr
ι : Type u_1
R : Type u_2
M : Type u_4
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ι → End R M
μ : ι → R
p : Submodule R M
hfp : ∀ (i : ι), MapsTo ⇑(f i) ↑p ↑p
h✝ : Nonempty ι
⊢ ⨅ x, p ⊓ (f x).maxGenEigenspace (μ x) =
    Submodule.map p.subtype (⨅ i, maxGenEigenspace (LinearMap.restrict (f i) ⋯) (μ i))

Tactic:
p.inf_genEigenspace _ (hfp _),

Goal state after:
case inr
ι : Type u_1
R : Type u_2
M : Type u_4
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ι → End R M
μ : ι → R
p : Submodule R M
hfp : ∀ (i : ι), MapsTo ⇑(f i) ↑p ↑p
h✝ : Nonempty ι
⊢ ⨅ x, Submodule.map p.subtype ((genEigenspace (LinearMap.restrict (f x) ⋯) (μ x)) ⊤) =
    Submodule.map p.subtype (⨅ i, maxGenEigenspace (LinearMap.restrict (f i) ⋯) (μ i))
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic

Goal state before:
pp: F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α : E
⊢ (aeval (AdjoinSimple.gen F α)) (minpoly F α) = 0

Tactic:
by
  ext
  convert! minpoly.aeval F α
  conv in aeval α => rw [← AdjoinSimple.algebraMap_gen F α]
  exact (aeval_algebraMap_apply E (AdjoinSimple.gen F α) _).symm

Goal state after:
Module: Mathlib.LinearAlgebra.Eigenspace.Triangularizable

Goal state before:
pp: case h
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
hg₀ : g (m.sum fun _μ mμ ↦ mμ) = g (m μ)
hg₁ : MapsTo ⇑g ↑p ↑p
hg₂ : MapsTo ⇑g ↑((f.genEigenspace μ) k) ↑((f.genEigenspace μ) k)
this : iSupIndep fun x ↦ (f.genEigenspace x) k
aux : ∀ μ' ∈ m.support.erase μ, (f.genEigenspace μ') ↑l₀ ≤ (f.genEigenspace μ') k
⊢ (m.support.erase μ).SupIndep fun i ↦ LinearMap.ker ((f - (algebraMap K (End K V)) i) ^ l₀)

Tactic:
· have := this.supIndep' (m.support.erase μ)
      apply this.antitone_fun
      intro μ' hμ'
      rw [Algebra.algebraMap_eq_smul_one, ← End.genEigenspace_nat]
      apply aux μ' hμ'

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

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
h e f : L
m : M
μ : R
t : IsSl2Triple h e f
P : t.HasPrimitiveVectorWith m μ
inst✝³ : IsNoetherian R M
inst✝² : IsTorsionFree R M
inst✝¹ : IsDomain R
inst✝ : CharZero R
this✝ : ∃ n, ((toEnd R L M) f ^ n) m = 0
n : ℕ
hn₁ : ¬((toEnd R L M) f ^ n) m = 0
hn₂ : ((toEnd R L M) f ^ (n + 1)) m = 0
this : ((↑n + 1) * (μ - ↑n)) • ((toEnd R L M) f ^ n) m = 0
⊢ μ = ↑n

Tactic:
smul_eq_zero_iff_left hn₁,

Goal state after:
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
h e f : L
m : M
μ : R
t : IsSl2Triple h e f
P : t.HasPrimitiveVectorWith m μ
inst✝³ : IsNoetherian R M
inst✝² : IsTorsionFree R M
inst✝¹ : IsDomain R
inst✝ : CharZero R
this✝ : ∃ n, ((toEnd R L M) f ^ n) m = 0
n : ℕ
hn₁ : ¬((toEnd R L M) f ^ n) m = 0
hn₂ : ((toEnd R L M) f ^ (n + 1)) m = 0
this : (↑n + 1) * (μ - ↑n) = 0
⊢ μ = ↑n
Module: Mathlib.Algebra.Lie.Weights.Basic

Goal state before:
pp: R : 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✝¹ : LieRing.IsNilpotent L
inst✝ : IsNoetherian R M
χ : L → R
x : L
⊢ _root_.IsNilpotent ((toEnd R L ↥(genWeightSpace M χ)) x - (algebraMap R (Module.End R ↥(genWeightSpace M χ))) (χ x))

Tactic:
have : toEnd R L (genWeightSpace M χ) x - algebraMap R _ (χ x) =
      (toEnd R L M x - algebraMap R _ (χ x)).restrict
        (fun m hm ↦ sub_mem (LieSubmodule.lie_mem _ hm) (Submodule.smul_mem _ _ hm)) := by
    rfl
  obtain ⟨k, hk⟩ := exists_genWeightSpace_le_ker_of_isNoetherian M χ x
  use k
  ext ⟨m, hm⟩
  simp only [this, Module.End.pow_restrict _, LinearMap.zero_apply, ZeroMemClass.coe_zero,
    ZeroMemClass.coe_eq_zero]
  exact ZeroMemClass.coe_eq_zero.mp (hk hm)

Goal state after: