mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.AlgebraicIndependent.Transcendental

Goal state before:
pp: ι : Type u_1
R : Type u_3
A : Type v
x : ι → A
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
hx : AlgebraicIndependent R x
inst✝ : Nontrivial A
s : Set ι
i : ι
⊢ Transcendental (↥(adjoin R (x '' s))) (x i) ↔ i ∉ s

Tactic:
rw [← Set.disjoint_singleton_right]
  convert! ← hx.adjoin_iff_disjoint (t := { i })
  rw [algebraicIndependent_singleton_iff ⟨i, rfl⟩]

Goal state after:
Module: Mathlib.RingTheory.AlgebraicIndependent.Basic

Goal state before:
pp: R : Type u_2
A : Type v
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
⊢ AlgebraicIndependent R Subtype.val ↔ Injective ⇑(algebraMap R A)

Tactic:
by simp

Goal state after:
Module: Mathlib.RingTheory.AlgebraicIndependent.Basic

Goal state before:
pp: R : Type u_2
A : Type v
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
s : Set A
H : ∀ t ⊆ s, t.Finite → AlgebraicIndependent R Subtype.val
p : MvPolynomial A R
hp : p ∈ supported R s
⊢ p ∈ supported R ↑p.vars

Tactic:
by simp

Goal state after:
Module: Mathlib.FieldTheory.AlgebraicClosure

Goal state before:
pp: F : Type u_1
E : Type u_2
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
K : Type u_3
inst✝¹ : Field K
inst✝ : Algebra F K
i : E ≃ₐ[F] K
x : K
h : x ∈ algebraicClosure F K
⊢ ↑↑i (↑i.symm x) = x

Tactic:
by simp

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.FixingSubgroup

Goal state before:
pp: M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s : Set α
a : α
a_in_s : a ∈ s
b : α
b_in_orbit : b ∈ orbit (↥(fixingSubgroup M sᶜ)) a
g : M
g_fixing : g ∈ fixingSubgroup M sᶜ
g_eq : g • a = b
⊢ b ∈ s

Tactic:
rw [mem_fixingSubgroup_compl_iff_movedBy_subset] at g_fixing

Goal state after:
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s : Set α
a : α
a_in_s : a ∈ s
b : α
b_in_orbit : b ∈ orbit (↥(fixingSubgroup M sᶜ)) a
g : M
g_fixing : (fixedBy α g)ᶜ ⊆ s
g_eq : g • a = b
⊢ b ∈ s
Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

Goal state before:
pp: R : Type u_1
S : Type v
A : Type w
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : CommRing A
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R A
inst✝³ : Algebra S A
inst✝² : IsScalarTower R S A
inst✝¹ : IsDomain S
inst✝ : NoZeroDivisors A
ι : Type u_2
v : ι → A
hv : IsTranscendenceBasis R v
H : ∀ (i : ι), IsAlgebraic S (v i)
Rv : Subalgebra R A := adjoin R (range v)
Sv : Subalgebra S A := adjoin S (range v)
⊢ Algebra.IsAlgebraic S ↥Sv

Tactic:
simpa [Sv, ← Subalgebra.isAlgebraic_iff, isAlgebraic_adjoin_iff]

Goal state after:
Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

Goal state before:
pp: R : Type u_1
A : Type w
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : FaithfulSMul R A
inst✝ : IsDomain A
s B : Set A
hB : (matroid R A).IsBasis B s
⊢ (matroid R A).closure B = ↑(algebraicClosure (↥(adjoin R s)) A)

Tactic:
hB.1.1.1.closure_eq_setOfPred_isBasis_insert,

Goal state after:
R : Type u_1
A : Type w
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : FaithfulSMul R A
inst✝ : IsDomain A
s B : Set A
hB : (matroid R A).IsBasis B s
⊢ {x | (matroid R A).IsBasis B (insert x B)} = ↑(algebraicClosure (↥(adjoin R s)) A)
Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

Goal state before:
pp: R : Type u_1
A : Type w
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : FaithfulSMul R A
inst✝ : IsDomain A
s : Set A
⊢ (matroid R A).Spanning s ↔ Algebra.IsAlgebraic (↥(adjoin R s)) A

Tactic:
Matroid.spanning_iff,

Goal state after:
R : Type u_1
A : Type w
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : FaithfulSMul R A
inst✝ : IsDomain A
s : Set A
⊢ (matroid R A).closure s = (matroid R A).E ∧ s ⊆ (matroid R A).E ↔ Algebra.IsAlgebraic (↥(adjoin R s)) A
Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

Goal state before:
pp: R : Type u_1
A : Type w
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : FaithfulSMul R A
inst✝ : Subsingleton A
s : Set A
⊢ (matroid R A).Spanning s ↔ s = univ

Tactic:
Matroid.spanning_iff,

Goal state after:
R : Type u_1
A : Type w
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : FaithfulSMul R A
inst✝ : Subsingleton A
s : Set A
⊢ (matroid R A).closure s = (matroid R A).E ∧ s ⊆ (matroid R A).E ↔ s = univ
Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

Goal state before:
pp: R : Type u_1
S : Type v
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsDomain R
fin : FiniteType R S
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] S
surj : Surjective ⇑f
⊢ lift.{v, u_1} (trdeg R (MvPolynomial (Fin n) R)) < lift.{u_1, v} ℵ₀

Tactic:
by simp

Goal state after:
Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

Goal state before:
pp: ι : Type u
R : Type u_1
A : Type w
x : ι → A
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : NoZeroDivisors A
inst✝¹ : FaithfulSMul R A
inst✝ : Finite ι
alg : Algebra.IsAlgebraic (↥(adjoin R (range x))) A
le : lift.{w, u} #ι ≤ lift.{u, w} (trdeg R A)
toFun✝ : ι → ↑(range x)
h : Injective toFun✝
this : Bijective (rangeFactorization x)
⊢ IsTranscendenceBasis R x

Tactic:
refine .of_subtype_range (fun _ _ ↦ (this.1 <| Subtype.ext ·)) ?_

Goal state after:
ι : Type u
R : Type u_1
A : Type w
x : ι → A
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : NoZeroDivisors A
inst✝¹ : FaithfulSMul R A
inst✝ : Finite ι
alg : Algebra.IsAlgebraic (↥(adjoin R (range x))) A
le : lift.{w, u} #ι ≤ lift.{u, w} (trdeg R A)
toFun✝ : ι → ↑(range x)
h : Injective toFun✝
this : Bijective (rangeFactorization x)
⊢ IsTranscendenceBasis R Subtype.val
Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

Goal state before:
pp: ι : Type u
R : Type u_1
A : Type w
x : ι → A
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : NoZeroDivisors A
inst✝¹ : FaithfulSMul R A
inst✝ : Algebra.IsAlgebraic (↥(adjoin R (range x))) A
fin : trdeg R A < ℵ₀
le : lift.{w, u} #ι ≤ lift.{u, w} (trdeg R A)
⊢ lift.{u, w} ℵ₀ = lift.{w, u} ℵ₀

Tactic:
by simp

Goal state after:
Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

Goal state before:
pp: ι : Type u
R : Type u_1
A : Type w
x : ι → A
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : Nontrivial R
inst✝¹ : NoZeroDivisors A
inst✝ : Finite ι
hx : AlgebraicIndependent R x
le : lift.{u, w} (trdeg R A) ≤ lift.{w, u} #ι
⊢ lift.{w, u} #ι < lift.{u, w} ℵ₀

Tactic:
by simp

Goal state after:
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: F : Type u
inst✝¹ : Field F
q : ℕ
inst✝ : ExpChar F q
g : F[X]
h1 : g.Separable
n : ℕ
hm : ((expand F (q ^ n)) g).Monic
hi : Irreducible ((expand F (q ^ n)) g)
h : ((expand F (q ^ n)) g).natSepDegree = 1
⊢ g.natDegree = 1

Tactic:
rwa [natSepDegree_expand _ q, h1.natSepDegree_eq_natDegree] at h

Goal state after:
Module: Mathlib.Topology.Algebra.FilterBasis

Goal state before:
pp: G : Type u
inst✝ : Group G
B : GroupFilterBasis G
⊢ ∀ {x y : Set G}, x ∈ {{1}} → y ∈ {{1}} → ∃ z ∈ {{1}}, z ⊆ x ∩ y

Tactic:
by simp

Goal state after:
Module: Mathlib.Topology.Algebra.FilterBasis

Goal state before:
pp: G : Type u
inst✝ : Group G
B : GroupFilterBasis G
⊢ ∀ {U : Set G}, U ∈ {{1}} → 1 ∈ U

Tactic:
by simp

Goal state after:
Module: Mathlib.Topology.Algebra.FilterBasis

Goal state before:
pp: G : Type u
inst✝ : Group G
B : GroupFilterBasis G
⊢ ∀ {U : Set G}, U ∈ {{1}} → ∃ V ∈ {{1}}, V * V ⊆ U

Tactic:
by simp

Goal state after:
Module: Mathlib.Topology.Algebra.FilterBasis

Goal state before:
pp: G : Type u
inst✝ : Group G
B : GroupFilterBasis G
⊢ ∀ {U : Set G}, U ∈ {{1}} → ∃ V ∈ {{1}}, V ⊆ (fun x ↦ x⁻¹) ⁻¹' U

Tactic:
by simp

Goal state after:
Module: Mathlib.Topology.Algebra.FilterBasis

Goal state before:
pp: G : Type u
inst✝ : Group G
B : GroupFilterBasis G
⊢ ∀ (x₀ : G) {U : Set G}, U ∈ {{1}} → ∃ V ∈ {{1}}, V ⊆ (fun x ↦ x₀ * x * x₀⁻¹) ⁻¹' U

Tactic:
by simp

Goal state after:
Module: Mathlib.FieldTheory.SeparableClosure

Goal state before:
pp: F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
K : Type w
inst✝¹ : Field K
inst✝ : Algebra F K
i : E ≃ₐ[F] K
x : K
h : x ∈ separableClosure F K
⊢ ↑↑i (↑i.symm x) = x

Tactic:
by simp

Goal state after:
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: case refine_1
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Ring E
inst✝¹ : IsDomain E
inst✝ : Algebra F E
q : ℕ
hF : ExpChar F q
x : E
this✝ : ExpChar E q
this : ExpChar E[X] q
h✝ : (minpoly F x).natSepDegree = 1
n : ℕ
y : F
h : minpoly F x = X ^ q ^ n - C y
hx : (Polynomial.aeval x) (X ^ q ^ n - C y) = (Polynomial.aeval x) (minpoly F x)
⊢ ∃ n, Polynomial.map (algebraMap F E) (minpoly F x) = (X - C x) ^ q ^ n

Tactic:
minpoly.aeval,

Goal state after:
case refine_1
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Ring E
inst✝¹ : IsDomain E
inst✝ : Algebra F E
q : ℕ
hF : ExpChar F q
x : E
this✝ : ExpChar E q
this : ExpChar E[X] q
h✝ : (minpoly F x).natSepDegree = 1
n : ℕ
y : F
h : minpoly F x = X ^ q ^ n - C y
hx : (Polynomial.aeval x) (X ^ q ^ n - C y) = 0
⊢ ∃ n, Polynomial.map (algebraMap F E) (minpoly F x) = (X - C x) ^ q ^ n
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Ring E
inst✝¹ : IsDomain E
inst✝ : Algebra F E
q : ℕ
hF : ExpChar F q
x : E
this✝ : ExpChar E q
this : ExpChar E[X] q
x✝ : ∃ n, Polynomial.map (algebraMap F E) (minpoly F x) = (X - C x) ^ q ^ n
n : ℕ
h : (algebraMap F E) ((minpoly F x).coeff 0) = -1 * x ^ q ^ n
⊢ -(-1 * x ^ q ^ n) = x ^ q ^ n

Tactic:
neg_mul,

Goal state after:
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Ring E
inst✝¹ : IsDomain E
inst✝ : Algebra F E
q : ℕ
hF : ExpChar F q
x : E
this✝ : ExpChar E q
this : ExpChar E[X] q
x✝ : ∃ n, Polynomial.map (algebraMap F E) (minpoly F x) = (X - C x) ^ q ^ n
n : ℕ
h : (algebraMap F E) ((minpoly F x).coeff 0) = -1 * x ^ q ^ n
⊢ - -(1 * x ^ q ^ n) = x ^ q ^ n
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
α : E
halg : IsAlgebraic F α
⊢ (minpoly F α).natSepDegree = (minpoly F α).natDegree ↔ IsSeparable F α

Tactic:
natSepDegree_eq_natDegree_iff _ (minpoly.ne_zero halg.isIntegral),

Goal state after:
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
α : E
halg : IsAlgebraic F α
⊢ (minpoly F α).Separable ↔ IsSeparable F α
Module: Mathlib.Topology.Algebra.OpenSubgroup

Goal state before:
pp: case right
G : Type u_2
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalGroup G
inst✝ : CompactSpace G
W : Set G
WClopen : IsClopen W
einW : 1 ∈ W
V : Set G
hV : mulInvClosureNhd V W
S : Subgroup G := ⋯
this : IsOpen[inst✝²] (⋃ n, V ^ (n + 1))
mulVpow : ∀ (n : ℕ), W * V ^ (n + 1) ⊆ W
n : ℕ
x : G
xin : x ∈ V ^ (n + 1)
⊢ 1 * x = x

Tactic:
rw [one_mul]

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

Goal state before:
pp: case inr
F : Type u_1
E' : Type u_3
inst✝³ : Field F
inst✝² : Field E'
inst✝¹ : Algebra F E'
L : IntermediateField F E'
inst✝ : IsGalois F E'
this : ∀ (L : IntermediateField F E'), FiniteDimensional F ↥L → finrank F ↥L = L.fixingSubgroup.index
hnfd : ¬FiniteDimensional F ↥L
h : L.fixingSubgroup.FiniteIndex
L' : IntermediateField F ↥L
hfd : FiniteDimensional F ↥L'
hL' : L.fixingSubgroup.index < finrank F ↥L'
⊢ False

Tactic:
let i := (liftAlgEquiv L').toLinearEquiv

Goal state after:
case inr
F : Type u_1
E' : Type u_3
inst✝³ : Field F
inst✝² : Field E'
inst✝¹ : Algebra F E'
L : IntermediateField F E'
inst✝ : IsGalois F E'
this : ∀ (L : IntermediateField F E'), FiniteDimensional F ↥L → finrank F ↥L = L.fixingSubgroup.index
hnfd : ¬FiniteDimensional F ↥L
h : L.fixingSubgroup.FiniteIndex
L' : IntermediateField F ↥L
hfd : FiniteDimensional F ↥L'
hL' : L.fixingSubgroup.index < finrank F ↥L'
i : ↥L' ≃ₗ[F] ↥(lift L') := ↑(liftAlgEquiv L')
⊢ False
Module: Mathlib.LinearAlgebra.BilinearForm.DualLattice

Goal state before:
pp: R : Type ?u.5
S : Type ?u.7
M : Type ?u.9
inst✝⁸ : CommRing R
inst✝⁷ : Field S
inst✝⁶ : AddCommGroup M
inst✝⁵ : Algebra R S
inst✝⁴ : Module R M
inst✝³ : Module S M
inst✝² : IsScalarTower R S M
B : BilinForm S M
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R S
N : Submodule R M
x✝ : ↥(B.dualSubmodule N)
x y : ↥N
⊢ (algebraMap R S) (B.dualSubmoduleParing x✝ (x + y)) =
    (algebraMap R S) (B.dualSubmoduleParing x✝ x + B.dualSubmoduleParing x✝ y)

Tactic:
by simp

Goal state after:
Module: Mathlib.LinearAlgebra.BilinearForm.DualLattice

Goal state before:
pp: R : Type ?u.5
S : Type ?u.7
M : Type ?u.9
inst✝⁸ : CommRing R
inst✝⁷ : Field S
inst✝⁶ : AddCommGroup M
inst✝⁵ : Algebra R S
inst✝⁴ : Module R M
inst✝³ : Module S M
inst✝² : IsScalarTower R S M
B : BilinForm S M
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R S
N : Submodule R M
x y : ↥(B.dualSubmodule N)
z : ↥N
⊢ (algebraMap R S) ({ toFun := B.dualSubmoduleParing (x + y), map_add' := ⋯, map_smul' := ⋯ } z) =
    (algebraMap R S)
      (({ toFun := B.dualSubmoduleParing x, map_add' := ⋯, map_smul' := ⋯ } +
          { toFun := B.dualSubmoduleParing y, map_add' := ⋯, map_smul' := ⋯ })
        z)

Tactic:
by simp

Goal state after:
Module: Mathlib.LinearAlgebra.BilinearForm.DualLattice

Goal state before:
pp: case intro.a
R : Type u_4
S : Type u_2
M : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Field S
inst✝⁶ : AddCommGroup M
inst✝⁵ : Algebra R S
inst✝⁴ : Module R M
inst✝³ : Module S M
inst✝² : IsScalarTower R S M
B : BilinForm S M
ι : Type u_1
inst✝¹ : Finite ι
inst✝ : DecidableEq ι
hB : B.Nondegenerate
b : Basis ι S M
val✝ : Fintype ι
x : M
hx : x ∈ B.dualSubmodule (Submodule.span R (Set.range ⇑b))
⊢ x ∈ Submodule.span R (Set.range ⇑(B.dualBasis hB b))

Tactic:
← (B.dualBasis hB b).sum_repr x

Goal state after:
case intro.a
R : Type u_4
S : Type u_2
M : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Field S
inst✝⁶ : AddCommGroup M
inst✝⁵ : Algebra R S
inst✝⁴ : Module R M
inst✝³ : Module S M
inst✝² : IsScalarTower R S M
B : BilinForm S M
ι : Type u_1
inst✝¹ : Finite ι
inst✝ : DecidableEq ι
hB : B.Nondegenerate
b : Basis ι S M
val✝ : Fintype ι
x : M
hx : x ∈ B.dualSubmodule (Submodule.span R (Set.range ⇑b))
⊢ ∑ i, ((B.dualBasis hB b).repr x) i • (B.dualBasis hB b) i ∈ Submodule.span R (Set.range ⇑(B.dualBasis hB b))
Module: Mathlib.FieldTheory.Minpoly.MinpolyDiv

Goal state before:
pp: R : Type u_2
S : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type u_1
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : IsDomain T
inst✝ : DecidableEq T
x : S
σ₁ σ₂ : S →ₐ[R] T
⊢ ↑σ₂ ((aeval x) (minpoly R x)) = 0

Tactic:
minpoly.aeval,

Goal state after:
R : Type u_2
S : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type u_1
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : IsDomain T
inst✝ : DecidableEq T
x : S
σ₁ σ₂ : S →ₐ[R] T
⊢ ↑σ₂ 0 = 0
Module: Mathlib.RingTheory.Polynomial.GaussLemma

Goal state before:
pp: case mpr
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDomain R
⊢ (∀ (p : R[X]), p.Monic → (Irreducible p ↔ Irreducible (map (algebraMap R K) p))) → IsIntegrallyClosed R

Tactic:
intro H
    refine
      (isIntegrallyClosed_iff K).mpr fun {x} hx =>
        RingHom.mem_range.mp <| minpoly.mem_range_of_degree_eq_one R x ?_
    rw [← Monic.degree_map (minpoly.monic hx) (algebraMap R K)]
    apply
      degree_eq_one_of_irreducible_of_root ((H _ <| minpoly.monic hx).mp (minpoly.irreducible hx))
    rw [IsRoot, eval_map_algebraMap, minpoly.aeval R x]

Goal state after:
Module: Mathlib.FieldTheory.Minpoly.MinpolyDiv

Goal state before:
pp: R : Type u_2
S : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
hx : IsIntegral R x
i : ℕ
hi : i ≤ (minpolyDiv R x).natDegree
⊢ (minpolyDiv R x).coeff ((minpolyDiv R x).natDegree - i) - x ^ i ∈ Submodule.span R ((fun x_1 ↦ x ^ x_1) '' Set.Iio i)

Tactic:
by
  induction i with
  | zero => simp [(minpolyDiv_monic hx).leadingCoeff]
  | succ i IH =>
    rw [coeff_minpolyDiv, add_sub_assoc, pow_succ, ← sub_mul, Algebra.algebraMap_eq_smul_one]
    refine add_mem ?_ ?_
    · apply Submodule.smul_mem
      apply Submodule.subset_span
      exact ⟨0, Nat.zero_lt_succ _, pow_zero _⟩
    · rw [← tsub_tsub, tsub_add_cancel_of_le (le_tsub_of_add_le_left (b := 1) hi)]
      apply SetLike.le_def.mp ?_
        (Submodule.mul_mem_mul (IH ((Nat.le_succ _).trans hi))
          (Submodule.mem_span_singleton_self x))
      rw [Submodule.span_mul_span, Set.mul_singleton, Set.image_image]
      apply Submodule.span_mono
      rintro _ ⟨j, hj, rfl⟩
      rw [Set.mem_Iio] at hj
      exact ⟨j + 1, Nat.add_lt_of_lt_sub hj, pow_succ x j⟩

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

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : K[X]
h0 : p ≠ 0
h : IsUnit (integerNormalization R⁰ p).primPart
u : Rˣ
hu : C ↑u = (integerNormalization R⁰ p).primPart
c : R
c0 : c ∈ R⁰
hc : map (algebraMap R K) (integerNormalization R⁰ p) = C ((algebraMap R K) c) * p
⊢ C ((algebraMap R K) ((integerNormalization R⁰ p).content * ↑u)) =
    map (algebraMap R K) (C ((integerNormalization R⁰ p).content * ↑u))

Tactic:
by simp

Goal state after:
Module: Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed

Goal state before:
pp: case refine_4
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain R
inst✝³ : Algebra R S
inst✝² : IsIntegrallyClosed R
inst✝¹ : IsDomain S
inst✝ : IsTorsionFree R S
r : R
hr : r ≠ 0
s : S
hs : IsIntegral R s
K : Type u_1 := FractionRing R
L : Type u_2 := FractionRing S
this : Algebra K L := FractionRing.liftAlgebra R L
⊢ (Polynomial.aeval ((algebraMap S L) s))
      ((minpoly K ((algebraMap K L) ((algebraMap R K) r) * (algebraMap S L) s)).scaleRoots ((algebraMap R K) r)⁻¹) =
    0

Tactic:
nth_rw 1 [← inv_mul_cancel_left₀ (b := algebraMap S L s)
      (a := algebraMap K L (algebraMap R K r)) (by simpa), ← map_inv₀]

Goal state after:
case refine_4
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain R
inst✝³ : Algebra R S
inst✝² : IsIntegrallyClosed R
inst✝¹ : IsDomain S
inst✝ : IsTorsionFree R S
r : R
hr : r ≠ 0
s : S
hs : IsIntegral R s
K : Type u_1 := FractionRing R
L : Type u_2 := FractionRing S
this : Algebra K L := FractionRing.liftAlgebra R L
⊢ (Polynomial.aeval
        ((algebraMap K L) ((algebraMap R K) r)⁻¹ * ((algebraMap K L) ((algebraMap R K) r) * (algebraMap S L) s)))
      ((minpoly K ((algebraMap K L) ((algebraMap R K) r) * (algebraMap S L) s)).scaleRoots ((algebraMap R K) r)⁻¹) =
    0
Module: Mathlib.RingTheory.Trace.Defs

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a : R
⊢ (trace R R) a = a

Tactic:
by simp

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

Goal state before:
pp: k : Type u_1
K : Type u_2
R : Type u_3
inst✝⁶ : Field k
inst✝⁵ : Field K
inst✝⁴ : Algebra k K
inst✝³ : CommRing R
inst✝² : Algebra k R
inst✝¹ : IsPurelyInseparable k K
q : ℕ
inst✝ : ExpChar k q
a✝ : Nontrivial (R ⊗[k] K)
hq : Nat.Prime q
⊢ (algebraMap R (R ⊗[k] K)) 0 = 0 ^ q ^ 0

Tactic:
by simp

Goal state after:
Module: Mathlib.RingTheory.IsGaloisGroup.Defs

Goal state before:
pp: G : Type u_1
A : Type u_2
A' : Type u_3
B : Type u_4
inst✝⁵ : Group G
inst✝⁴ : CommSemiring A
inst✝³ : Semiring B
inst✝² : Algebra A B
inst✝¹ : MulSemiringAction G B
hA : IsGaloisGroup G A B
inst✝ : FaithfulSMul A B
x✝ : A
⊢ (fun x ↦ ⋯.choose) ((fun x ↦ ⟨(algebraMap A B) x, ⋯⟩) x✝) = x✝

Tactic:
by simp

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Basic

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
e : K ≃+* L
inst✝ : NumberField K
⊢ e.toAddMonoidHom 1 = 1

Tactic:
by simp

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Basic

Goal state before:
pp: K : Type u_1
inst✝ : Field K
x y : K
hx : x ∈ integralClosure ℤ K
hy : y ∈ integralClosure ℤ K
⊢ ⟨x, hx⟩ = ⟨y, hy⟩ ↔ x = y

Tactic:
by simp

Goal state after:
Module: Mathlib.Data.ZMod.ValMinAbs

Goal state before:
pp: case inr.refine_2
n : ℕ
a : ZMod n
ha : 2 * a.val ≠ n
h : NeZero n
⊢ -↑n < -a.valMinAbs * 2

Tactic:
neg_mul,

Goal state after:
case inr.refine_2
n : ℕ
a : ZMod n
ha : 2 * a.val ≠ n
h : NeZero n
⊢ -↑n < -(a.valMinAbs * 2)
Module: Mathlib.Data.ZMod.ValMinAbs

Goal state before:
pp: case pos
n : ℕ
a : ZMod n
h2a : 2 * a.val = n
⊢ (-a).valMinAbs.natAbs = a.valMinAbs.natAbs

Tactic:
a.neg_eq_self_iff.2 (Or.inr h2a)

Goal state after:
case pos
n : ℕ
a : ZMod n
h2a : 2 * a.val = n
⊢ a.valMinAbs.natAbs = a.valMinAbs.natAbs
Module: Mathlib.RingTheory.Trace.Basic

Goal state before:
pp: case neg.succ.hnc
K : Type u_4
L : Type u_5
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
H : ¬Algebra.IsSeparable K L
p : ℕ
hp : ExpChar K p
this : p ≠ 0
x : L
h₀ : FiniteDimensional K L
hx : ¬IsSeparable K x
g : K[X]
hg₁ : g.Separable
n : ℕ
hg₂ : (expand K (p ^ (n + 1))) g = minpoly K x
⊢ ¬p ^ (n + 1) ∣ ((expand K (p ^ (n + 1))) g).natDegree - 1

Tactic:
rw [natDegree_expand]
        intro h
        have := Nat.dvd_sub (dvd_mul_left (p ^ (n + 1)) g.natDegree) h
        rw [tsub_tsub_cancel_of_le, Nat.dvd_one] at this
        · obtain rfl : g = minpoly K x := by simpa [this] using hg₂
          cases hx hg₁
        · rw [Nat.one_le_iff_ne_zero]
          have : g.natDegree ≠ 0 := fun e ↦ by
            have := congr(natDegree $hg₂)
            rw [natDegree_expand, e, zero_mul] at this
            exact (minpoly.natDegree_pos (IsIntegral.isIntegral x)).ne this
          positivity

Goal state after:
Module: Mathlib.FieldTheory.Galois.IsGaloisGroup

Goal state before:
pp: G : Type u_1
K : Type u_3
L : Type u_4
inst✝⁵ : Group G
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : MulSemiringAction G L
inst✝ : IsGaloisGroup G K L
⊢ Nat.card G = finrank K L

Tactic:
rcases fintypeOrInfinite G with _ | hG

Goal state after:
case inl
G : Type u_1
K : Type u_3
L : Type u_4
inst✝⁵ : Group G
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : MulSemiringAction G L
inst✝ : IsGaloisGroup G K L
val✝ : Fintype G
⊢ Nat.card G = finrank K L

case inr
G : Type u_1
K : Type u_3
L : Type u_4
inst✝⁵ : Group G
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : MulSemiringAction G L
inst✝ : IsGaloisGroup G K L
hG : Infinite G
⊢ Nat.card G = finrank K L
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: K : Type u_1
inst✝² : CommRing K
inst✝¹ : IsDomain K
inst✝ : Fintype Kˣ
⊢ ∀ a ∈ univ.erase (-1), a * a⁻¹ = 1

Tactic:
by simp

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

Goal state before:
pp: K : Type u_1
inst✝² : CommRing K
inst✝¹ : IsDomain K
inst✝ : Fintype Kˣ
⊢ ∀ a ∈ univ.erase (-1), a⁻¹⁻¹ = a

Tactic:
by simp

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

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : Fintype K
inst✝ : DecidableEq K
i : ℕ
⊢ ↑1 ^ i = 1

Tactic:
by simp

Goal state after:
Module: Mathlib.Data.Int.Associated

Goal state before:
pp: b : ℤ
⊢ -b * ↑(-1) = b

Tactic:
by simp

Goal state after:
Module: Mathlib.Data.Int.Associated

Goal state before:
pp: a : ℤ
⊢ a = a * ↑1

Tactic:
by simp

Goal state after:
Module: Mathlib.Data.Int.Associated

Goal state before:
pp: a : ℤ
⊢ a = -(a * ↑(-1))

Tactic:
by simp

Goal state after:
Module: Mathlib.RingTheory.Int.Basic

Goal state before:
pp: case h
a b c : ℤ
h : a.gcd b = 1
heq : a * b = c ^ 2
h' : IsUnit (GCDMonoid.gcd a b)
d : ℤ
u : ℤˣ
hu : d ^ 2 * ↑u = a
⊢ d ^ 2 * ↑u = d ^ 2 ∨ d ^ 2 * ↑u = -d ^ 2

Tactic:
rcases Int.units_eq_one_or u with hu' | hu'

Goal state after:
case h.inl
a b c : ℤ
h : a.gcd b = 1
heq : a * b = c ^ 2
h' : IsUnit (GCDMonoid.gcd a b)
d : ℤ
u : ℤˣ
hu : d ^ 2 * ↑u = a
hu' : u = 1
⊢ d ^ 2 * ↑u = d ^ 2 ∨ d ^ 2 * ↑u = -d ^ 2

case h.inr
a b c : ℤ
h : a.gcd b = 1
heq : a * b = c ^ 2
h' : IsUnit (GCDMonoid.gcd a b)
d : ℤ
u : ℤˣ
hu : d ^ 2 * ↑u = a
hu' : u = -1
⊢ d ^ 2 * ↑u = d ^ 2 ∨ d ^ 2 * ↑u = -d ^ 2