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

Goal state before:
pp: R : Type u_3
S : Type u
A : Type v
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✝² : Nontrivial R
inst✝¹ : FaithfulSMul R S
inst✝ : FaithfulSMul S A
⊢ lift.{v, u} (⨆ ι, #↑↑ι) + lift.{u, v} (⨆ ι, #↑↑ι) ≤ lift.{u, v} (⨆ ι, #↑↑ι)

Tactic:
lift_iSup bddAbove_of_small

Goal state after:
R : Type u_3
S : Type u
A : Type v
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✝² : Nontrivial R
inst✝¹ : FaithfulSMul R S
inst✝ : FaithfulSMul S A
⊢ (⨆ i, lift.{v, u} #↑↑i) + ⨆ i, lift.{u, v} #↑↑i ≤ ⨆ i, lift.{u, v} #↑↑i
Module: Mathlib.RingTheory.AlgebraicIndependent.Basic

Goal state before:
pp: ι : Type u
R : Type u_2
A : Type v
x : ι → A
inst✝⁹ : CommRing R
inst✝⁸ : CommRing A
inst✝⁷ : Algebra R A
S : Type u_3
B : Type u_4
FRS : Type u_5
FAB : Type u_6
inst✝⁶ : CommRing S
inst✝⁵ : CommRing B
inst✝⁴ : Algebra S B
inst✝³ : FunLike FRS R S
inst✝² : RingHomClass FRS R S
inst✝¹ : FunLike FAB A B
inst✝ : RingHomClass FAB A B
f : FRS
g : FAB
H : AlgebraicIndependent S (⇑g ∘ x)
hf : Injective ⇑f
h : (algebraMap S B).comp ↑f = (↑g).comp (algebraMap R A)
⊢ AlgebraicIndependent R x

Tactic:
rw [algebraicIndependent_iff] at H ⊢
  intro p hp
  have := H (p.map f) <| by
    have : (g : A →+* B) _ = _ := congr(g $hp)
    rwa [map_zero, map_aeval, ← h, ← eval₂Hom_map_hom, ← aeval_eq_eval₂Hom] at this
  exact map_injective (f : R →+* S) hf (by rwa [map_zero])

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

Goal state before:
pp: F : Type u_1
inst✝ : CommSemiring F
f : F[X]
hf : HasSeparableContraction 1 f
⊢ hf.degree = f.natDegree

Tactic:
by
  let ⟨a, ha⟩ := hf.dvd_degree'
  rw [← ha, one_pow a, mul_one]

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

Goal state before:
pp: R : Type u_2
A : Type v
A' : Type v'
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : CommRing A'
inst✝¹ : Algebra R A
inst✝ : Algebra R A'
f : A →ₐ[R] A'
hf : Injective ⇑f
a✝ : Nontrivial R
⊢ lift.{v', v} (⨆ ι, #↑↑ι) ≤ lift.{v, v'} (trdeg R A')

Tactic:
lift_iSup bddAbove_of_small

Goal state after:
R : Type u_2
A : Type v
A' : Type v'
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : CommRing A'
inst✝¹ : Algebra R A
inst✝ : Algebra R A'
f : A →ₐ[R] A'
hf : Injective ⇑f
a✝ : Nontrivial R
⊢ ⨆ i, lift.{v', v} #↑↑i ≤ lift.{v, v'} (trdeg R A')
Module: Mathlib.RingTheory.AlgebraicIndependent.Basic

Goal state before:
pp: R : Type u_2
A : Type v
A' : Type v'
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : CommRing A'
inst✝¹ : Algebra R A
inst✝ : Algebra R A'
f : A →ₐ[R] A'
hf : Surjective ⇑f
a✝ : Nontrivial R
⊢ lift.{v, v'} (⨆ ι, #↑↑ι) ≤ lift.{v', v} (trdeg R A)

Tactic:
lift_iSup bddAbove_of_small

Goal state after:
R : Type u_2
A : Type v
A' : Type v'
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : CommRing A'
inst✝¹ : Algebra R A
inst✝ : Algebra R A'
f : A →ₐ[R] A'
hf : Surjective ⇑f
a✝ : Nontrivial R
⊢ ⨆ i, lift.{v, v'} #↑↑i ≤ lift.{v', v} (trdeg R 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 t : Set A
h✝ : AlgebraicIndepOn R _root_.id s ∧ s ⊆ t
alg : ∀ a ∈ t, IsAlgebraic (↥(adjoin R s)) a
a : A
ha : a ∉ s
h : AlgebraicIndepOn R _root_.id (insert a s) ∧ insert a s ⊆ t
⊢ IsAlgebraic (↥(adjoin R (_root_.id '' s))) (_root_.id a)

Tactic:
rw [image_id]

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 t : Set A
h✝ : AlgebraicIndepOn R _root_.id s ∧ s ⊆ t
alg : ∀ a ∈ t, IsAlgebraic (↥(adjoin R s)) a
a : A
ha : a ∉ s
h : AlgebraicIndepOn R _root_.id (insert a s) ∧ insert a s ⊆ t
⊢ IsAlgebraic (↥(adjoin R s)) (_root_.id a)
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: F : Type u
inst✝ : Field F
f g : F[X]
h : ¬f = 0 ∧ ¬g = 0
H : ∀ (a : AlgebraicClosure F), f ≠ 0 ∧ (aeval a) f = 0 → ∀ (b : AlgebraicClosure F), g ≠ 0 ∧ (aeval b) g = 0 → a ≠ b
u : F[X]
hu : Irreducible u
x✝¹ : u ∣ f
x✝ : u ∣ g
v : F[X]
hf : f = u * v
w : F[X]
hg : g = u * w
x : AlgebraicClosure F
hx : (aeval x) u = 0
⊢ (aeval x) f = 0

Tactic:
by simpa only [map_mul, hx, zero_mul] using congr(aeval x $hf)

Goal state after:
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: F : Type u
inst✝¹ : Field F
q : ℕ
inst✝ : ExpChar F q
n : ℕ
y : F
⊢ ((expand F (q ^ n)) X - C y).natSepDegree = 1

Tactic:
← expand_C (q ^ n),

Goal state after:
F : Type u
inst✝¹ : Field F
q : ℕ
inst✝ : ExpChar F q
n : ℕ
y : F
⊢ ((expand F (q ^ n)) X - (expand F (q ^ n)) (C y)).natSepDegree = 1
Module: Mathlib.FieldTheory.Galois.Basic

Goal state before:
pp: F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
H : Subgroup Gal(E/F)
K : IntermediateField F E
x✝¹ x✝ : ↥K.fixingSubgroup
⊢ (let __src := (↑(x✝¹ * x✝)).toRingEquiv;
    { toEquiv := __src.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }) =
    (let __src := (↑x✝¹).toRingEquiv;
      { toEquiv := __src.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }) *
      let __src := (↑x✝).toRingEquiv;
      { toEquiv := __src.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }

Tactic:
ext; rfl

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

Goal state before:
pp: case hmul_left
R✝ : Type u
inst✝¹ : Ring R✝
B✝ : RingFilterBasis R✝
R : Type u
inst✝ : Ring R
B : RingFilterBasis R
B' : AddGroupFilterBasis R := ⋯
this✝ : TopologicalSpace R := ⋯
basis : (𝓝 0).HasBasis (fun V ↦ V ∈ B') id
basis' : (𝓝 0 ×ˢ 𝓝 0).HasBasis (fun i ↦ i.1 ∈ B' ∧ i.2 ∈ B') fun i ↦ id i.1 ×ˢ id i.2
this : IsTopologicalAddGroup R
⊢ ∀ (x₀ : R), Tendsto (fun x ↦ x₀ * x) (𝓝 0) (𝓝 0)

pp: case hmul_right
R✝ : Type u
inst✝¹ : Ring R✝
B✝ : RingFilterBasis R✝
R : Type u
inst✝ : Ring R
B : RingFilterBasis R
B' : AddGroupFilterBasis R := ⋯
this✝ : TopologicalSpace R := ⋯
basis : (𝓝 0).HasBasis (fun V ↦ V ∈ B') id
basis' : (𝓝 0 ×ˢ 𝓝 0).HasBasis (fun i ↦ i.1 ∈ B' ∧ i.2 ∈ B') fun i ↦ id i.1 ×ˢ id i.2
this : IsTopologicalAddGroup R
⊢ ∀ (x₀ : R), Tendsto (fun x ↦ x * x₀) (𝓝 0) (𝓝 0)

Tactic:
· intro x₀
    rw [basis.tendsto_iff basis]
    intro U
    simpa using! B.mul_left x₀

Goal state after:
case hmul_right
R✝ : Type u
inst✝¹ : Ring R✝
B✝ : RingFilterBasis R✝
R : Type u
inst✝ : Ring R
B : RingFilterBasis R
B' : AddGroupFilterBasis R := ⋯
this✝ : TopologicalSpace R := ⋯
basis : (𝓝 0).HasBasis (fun V ↦ V ∈ B') id
basis' : (𝓝 0 ×ˢ 𝓝 0).HasBasis (fun i ↦ i.1 ∈ B' ∧ i.2 ∈ B') fun i ↦ id i.1 ×ˢ id i.2
this : IsTopologicalAddGroup R
⊢ ∀ (x₀ : R), Tendsto (fun x ↦ x * x₀) (𝓝 0) (𝓝 0)
Module: Mathlib.FieldTheory.Galois.Basic

Goal state before:
pp: F : Type u_1
inst✝⁴ : Field F
E : Type u_2
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : IsGalois F E
inst✝ : FiniteDimensional F E
x : E
⊢ x ∈ ⊥ ↔ ∀ (f : Gal(E/F)), f x = x

Tactic:
← fixedField_top,

Goal state after:
F : Type u_1
inst✝⁴ : Field F
E : Type u_2
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : IsGalois F E
inst✝ : FiniteDimensional F E
x : E
⊢ x ∈ fixedField ⊤ ↔ ∀ (f : Gal(E/F)), f x = x
Module: Mathlib.FieldTheory.SeparableClosure

Goal state before:
pp: case refine_2
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✝
K : IntermediateField F E
x : E
hx :
  x ∈
    IntermediateField.restrictScalars F
      (separableClosure (↥(IntermediateField.restrictScalars F (separableClosure (↥K) E))) E)
⊢ x ∈ IntermediateField.restrictScalars F (separableClosure (↥K) E)

Tactic:
obtain ⟨x, rfl⟩ := (separableClosure.separableClosure_eq_bot K E).le hx

Goal state after:
case refine_2
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✝
K : IntermediateField F E
x : ↥(separableClosure (↥K) E)
hx :
  (Algebra.ofId (↥(separableClosure (↥K) E)) E).toRingHom x ∈
    IntermediateField.restrictScalars F
      (separableClosure (↥(IntermediateField.restrictScalars F (separableClosure (↥K) E))) E)
⊢ (Algebra.ofId (↥(separableClosure (↥K) E)) E).toRingHom x ∈
    IntermediateField.restrictScalars F (separableClosure (↥K) E)
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
inst✝¹ : Algebra K E
inst✝ : IsScalarTower F K E
x : E
hx : x ∈ (separableClosureOperator F E) (IntermediateField.restrictScalars F (separableClosure K E))
⊢ x ∈ IntermediateField.restrictScalars F (separableClosure K E)

Tactic:
obtain ⟨x, rfl⟩ := (separableClosure.separableClosure_eq_bot K E).le hx

Goal state after:
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
inst✝¹ : Algebra K E
inst✝ : IsScalarTower F K E
x : ↥(separableClosure K E)
hx :
  (Algebra.ofId (↥(separableClosure K E)) E).toRingHom x ∈
    (separableClosureOperator F E) (IntermediateField.restrictScalars F (separableClosure K E))
⊢ (Algebra.ofId (↥(separableClosure K E)) E).toRingHom x ∈ IntermediateField.restrictScalars F (separableClosure K E)
Module: Mathlib.FieldTheory.Galois.Basic

Goal state before:
pp: K : Type u_3
L : Type u_4
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
E : IntermediateField K L
σ : Gal(L/K)
⊢ (map (↑σ) E).fixingSubgroup = MulAut.conj σ • E.fixingSubgroup

Tactic:
ext τ

Goal state after:
K : Type u_3
L : Type u_4
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
E : IntermediateField K L
σ τ : Gal(L/K)
⊢ τ ∈ (map (↑σ) E).fixingSubgroup ↔ τ ∈ MulAut.conj σ • E.fixingSubgroup
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 : Type v
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsSeparable F E
hfd : FiniteDimensional F E
L : IntermediateField F E
x : E
h : finSepDegree F ↥L = finrank F ↥L
M : IntermediateField (↥L) E := (↥L)⟮x⟯
heq : finSepDegree F ↥L * finSepDegree ↥L ↥M = finrank F ↥L * finrank ↥L ↥M
⊢ finSepDegree F ↥(IntermediateField.restrictScalars F M) = finrank F ↥(IntermediateField.restrictScalars F M)

Tactic:
rwa [finSepDegree_mul_finSepDegree_of_isAlgebraic F L M,
    Module.finrank_mul_finrank F L M] at heq

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

Goal state before:
pp: F : Type u_1
E' : Type u_3
inst✝³ : Field F
inst✝² : Field E'
inst✝¹ : Algebra F E'
inst✝ : IsGalois F E'
L : IntermediateField F E'
hnfd : FiniteDimensional F ↥L
E : IntermediateField F E' := normalClosure F (↥L) E'
hle : L ≤ E
L' : IntermediateField F ↥E := restrict hle
h : finrank F ↥L' = L'.fixingSubgroup.index
⊢ map (IsScalarTower.toAlgHom F (↥E) E') L' = L

Tactic:
exact lift_restrict hle

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

Goal state before:
pp: R : Type u_1
S : Type u_3
M : Type u_2
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
N₁ N₂ : Submodule R M
⊢ N₁ ≤ B.flip.dualSubmodule N₂ ↔ N₂ ≤ B.dualSubmodule N₁

Tactic:
change (∀ (x : M), x ∈ N₁ → _) ↔ ∀ (x : M), x ∈ N₂ → _

Goal state after:
R : Type u_1
S : Type u_3
M : Type u_2
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
N₁ N₂ : Submodule R M
⊢ (∀ x ∈ N₁, x ∈ B.flip.dualSubmodule N₂) ↔ ∀ x ∈ N₂, x ∈ B.dualSubmodule N₁
Module: Mathlib.RingTheory.Polynomial.GaussLemma

Goal state before:
pp: case refine_1
R : Type u_1
inst✝² : CommRing R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
f : R[X]
hf : f.Monic
g : K[X]
hg : g.Monic
hd : g ∣ map (algebraMap R K) f
a : g.SplittingField
ha : a ∈ (map (algebraMap K g.SplittingField) g).roots
⊢ map (algebraMap K g.SplittingField) g ∣ map (algebraMap K g.SplittingField) (map (algebraMap R K) f)

Tactic:
exact map_dvd (algebraMap K g.SplittingField) hd

Goal state after:
Module: Mathlib.FieldTheory.IsSepClosed

Goal state before:
pp: k : Type u
inst✝¹ : Field k
inst✝ : IsSepClosed k
n : ℕ
a b c : k
hn : ↑n = 0
hn' : 2 ≤ n
hb : b ≠ 0
f : k[X] := C a * X ^ n + C b * X + C c
hdeg : f.degree ≠ 0
hsep : f.Separable
⊢ ∃ x, a * x ^ n + b * x + c = 0

Tactic:
obtain ⟨x, hx⟩ := exists_root f hdeg hsep

Goal state after:
k : Type u
inst✝¹ : Field k
inst✝ : IsSepClosed k
n : ℕ
a b c : k
hn : ↑n = 0
hn' : 2 ≤ n
hb : b ≠ 0
f : k[X] := C a * X ^ n + C b * X + C c
hdeg : f.degree ≠ 0
hsep : f.Separable
x : k
hx : f.IsRoot x
⊢ ∃ x, a * x ^ n + b * x + c = 0
Module: Mathlib.FieldTheory.IsSepClosed

Goal state before:
pp: k : Type u
inst✝⁴ : Field k
K : Type v
inst✝³ : Field K
inst✝² : IsSepClosed k
inst✝¹ : Algebra k K
inst✝ : Algebra.IsSeparable k K
x : K
hq : (minpoly k x).leadingCoeff = 1
hsep : IsSeparable k x
⊢ (algebraMap k K) (-(minpoly k x).coeff 0) = x

Tactic:
have h : (minpoly k x).degree = 1 :=
    degree_eq_one_of_irreducible k (minpoly.irreducible (Algebra.IsSeparable.isIntegral k x)) hsep

Goal state after:
k : Type u
inst✝⁴ : Field k
K : Type v
inst✝³ : Field K
inst✝² : IsSepClosed k
inst✝¹ : Algebra k K
inst✝ : Algebra.IsSeparable k K
x : K
hq : (minpoly k x).leadingCoeff = 1
hsep : IsSeparable k x
h : (minpoly k x).degree = 1
⊢ (algebraMap k K) (-(minpoly k x).coeff 0) = x
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✝ : IsGCDMonoid R
p : R[X]
hp : p.IsPrimitive
hi : Irreducible p
a b : K[X]
hab : map (algebraMap R K) p = a * b
c : R
c0 : c ≠ 0
hc : map (algebraMap R K) (integerNormalization R⁰ a) = C ((algebraMap R K) c) * a
d : R
d0 : d ≠ 0
hd : map (algebraMap R K) (integerNormalization R⁰ b) = C ((algebraMap R K) d) * b
hcd0 : ¬C (c * d) = 0
⊢ map (algebraMap R K) (C c) * map (algebraMap R K) (C d) * map (algebraMap R K) p =
    C ((algebraMap R K) c) * a * map (algebraMap R K) (integerNormalization R⁰ b)

Tactic:
hd,

Goal state after:
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✝ : IsGCDMonoid R
p : R[X]
hp : p.IsPrimitive
hi : Irreducible p
a b : K[X]
hab : map (algebraMap R K) p = a * b
c : R
c0 : c ≠ 0
hc : map (algebraMap R K) (integerNormalization R⁰ a) = C ((algebraMap R K) c) * a
d : R
d0 : d ≠ 0
hd : map (algebraMap R K) (integerNormalization R⁰ b) = C ((algebraMap R K) d) * b
hcd0 : ¬C (c * d) = 0
⊢ map (algebraMap R K) (C c) * map (algebraMap R K) (C d) * map (algebraMap R K) p =
    C ((algebraMap R K) c) * a * (C ((algebraMap R K) d) * b)
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✝ : IsGCDMonoid R
p q : R[X]
hp : p.IsPrimitive
h_dvd : map (algebraMap R K) p ∣ map (algebraMap R K) q
⊢ p ∣ q

Tactic:
by
  rcases h_dvd with ⟨r, hr⟩
  obtain ⟨r, rfl⟩ := (mul_map_mem_lifts_iff hp).mp ⟨q, mul_comm _ r ▸ hr⟩
  use r
  simpa [← Polynomial.map_mul, (map_injective _ (FaithfulSMul.algebraMap_injective R K)).eq_iff]
    using hr

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

Goal state before:
pp: A : Type u_1
B : Type u_2
G : Type u_3
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
inst✝³ : Group G
inst✝² : MulSemiringAction G B
inst✝¹ : IsInvariant A B G
inst✝ : Finite G
⊢ Algebra.IsIntegral A B

Tactic:
cases nonempty_fintype G
  refine ⟨fun b ↦ ?_⟩
  obtain ⟨p, hp1, -, hp2⟩ := Polynomial.lifts_and_natDegree_eq_and_monic
    (charpoly_mem_lifts A B G b) (monic_charpoly G b)
  exact ⟨p, hp2, by rw [← eval_map, hp1, eval_charpoly]⟩

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

Goal state before:
pp: K : Type u_4
L : Type u_5
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
F : Type u_6
inst✝¹ : Field F
inst✝ : Algebra K F
x : L
hf : (Polynomial.map (algebraMap K F) (minpoly K x)).Splits
⊢ (algebraMap K F) ((Algebra.trace K ↥K⟮x⟯) (gen K x)) = ((minpoly K x).aroots F).sum

Tactic:
by
  have injKxL := (algebraMap K⟮x⟯ L).injective
  by_cases hx : IsIntegral K x; swap
  · simp [minpoly.eq_zero hx, trace_gen_eq_zero hx, aroots_def]
  rw [← adjoin.powerBasis_gen hx, (adjoin.powerBasis hx).trace_gen_eq_sum_roots] <;>
    rw [adjoin.powerBasis_gen hx, ← minpoly.algebraMap_eq injKxL] <;>
    try simp only [AdjoinSimple.algebraMap_gen _ _]
  exact hf

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

Goal state before:
pp: case pos
B : Type u_2
inst✝⁴ : CommRing B
G : Type u_3
inst✝³ : Group G
inst✝² : Finite G
inst✝¹ : MulSemiringAction G B
Q : Ideal B
inst✝ : Q.IsPrime
val✝ : Fintype G
P : Ideal B := {g | g • Q ≠ Q}.inf fun g ↦ g • Q
h1 : ¬P ≤ Q
b : B
hbQ : b ∉ Q
hbP : ∀ (g : G), g • Q ≠ Q → b ∈ g • Q
f : B[X] := MulSemiringAction.charpoly G b
q : (B ⧸ Q)[X]
hq : map (algebraMap B (B ⧸ Q)) f = X ^ rootMultiplicity 0 (map (algebraMap B (B ⧸ Q)) f) * q
hq0 : ¬X ∣ q
j : ℕ := rootMultiplicity 0 (map (algebraMap B (B ⧸ Q)) f)
k : ℕ := q.natDegree
r : B[X] := ∑ i ∈ Finset.range (k + 1), (monomial i) (f.coeff (i + j))
n : ℕ
hn : n ≤ k
⊢ (algebraMap B (B ⧸ Q)) (f.coeff (n + j)) = q.coeff n

Tactic:
← Polynomial.coeff_map,

Goal state after:
case pos
B : Type u_2
inst✝⁴ : CommRing B
G : Type u_3
inst✝³ : Group G
inst✝² : Finite G
inst✝¹ : MulSemiringAction G B
Q : Ideal B
inst✝ : Q.IsPrime
val✝ : Fintype G
P : Ideal B := {g | g • Q ≠ Q}.inf fun g ↦ g • Q
h1 : ¬P ≤ Q
b : B
hbQ : b ∉ Q
hbP : ∀ (g : G), g • Q ≠ Q → b ∈ g • Q
f : B[X] := MulSemiringAction.charpoly G b
q : (B ⧸ Q)[X]
hq : map (algebraMap B (B ⧸ Q)) f = X ^ rootMultiplicity 0 (map (algebraMap B (B ⧸ Q)) f) * q
hq0 : ¬X ∣ q
j : ℕ := rootMultiplicity 0 (map (algebraMap B (B ⧸ Q)) f)
k : ℕ := q.natDegree
r : B[X] := ∑ i ∈ Finset.range (k + 1), (monomial i) (f.coeff (i + j))
n : ℕ
hn : n ≤ k
⊢ (map (algebraMap B (B ⧸ Q)) f).coeff (n + j) = q.coeff n
Module: Mathlib.Data.ZMod.ValMinAbs

Goal state before:
pp: case zero
a : ℕ
ha : 0 / 2 < a
ha' : a < 0
⊢ (↑a).valMinAbs = ↑a - ↑0

Tactic:
cases not_lt_bot ha'

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

Goal state before:
pp: case refine_1
B : Type u_2
inst✝⁴ : CommRing B
G : Type u_3
inst✝³ : Group G
inst✝² : Finite G
inst✝¹ : MulSemiringAction G B
Q : Ideal B
inst✝ : Q.IsPrime
val✝ : Fintype G
P : Ideal B := {g | g • Q ≠ Q}.inf fun g ↦ g • Q
h1 : ¬P ≤ Q
b : B
hbQ : b ∉ Q
hbP : ∀ (g : G), g • Q ≠ Q → b ∈ g • Q
f : B[X] := MulSemiringAction.charpoly G b
q : (B ⧸ Q)[X]
hq : map (algebraMap B (B ⧸ Q)) f = X ^ rootMultiplicity 0 (map (algebraMap B (B ⧸ Q)) f) * q
hq0 : ¬X ∣ q
j : ℕ := rootMultiplicity 0 (map (algebraMap B (B ⧸ Q)) f)
k : ℕ := q.natDegree
r : B[X] := ∑ i ∈ Finset.range (k + 1), (monomial i) (f.coeff (i + j))
hr✝ : map (algebraMap B (B ⧸ Q)) r = q
hf : eval b f = 0
hr : eval b r ∈ Q
a : B := f.coeff j
ha : ∀ (g : G), g • a = a
hr' : ∀ (g : G), g • Q ≠ Q → a - eval b r ∈ g • Q
⊢ ¬(algebraMap B (B ⧸ Q)) a = 0

Tactic:
← Polynomial.coeff_map,

Goal state after:
case refine_1
B : Type u_2
inst✝⁴ : CommRing B
G : Type u_3
inst✝³ : Group G
inst✝² : Finite G
inst✝¹ : MulSemiringAction G B
Q : Ideal B
inst✝ : Q.IsPrime
val✝ : Fintype G
P : Ideal B := {g | g • Q ≠ Q}.inf fun g ↦ g • Q
h1 : ¬P ≤ Q
b : B
hbQ : b ∉ Q
hbP : ∀ (g : G), g • Q ≠ Q → b ∈ g • Q
f : B[X] := MulSemiringAction.charpoly G b
q : (B ⧸ Q)[X]
hq : map (algebraMap B (B ⧸ Q)) f = X ^ rootMultiplicity 0 (map (algebraMap B (B ⧸ Q)) f) * q
hq0 : ¬X ∣ q
j : ℕ := rootMultiplicity 0 (map (algebraMap B (B ⧸ Q)) f)
k : ℕ := q.natDegree
r : B[X] := ∑ i ∈ Finset.range (k + 1), (monomial i) (f.coeff (i + j))
hr✝ : map (algebraMap B (B ⧸ Q)) r = q
hf : eval b f = 0
hr : eval b r ∈ Q
a : B := f.coeff j
ha : ∀ (g : G), g • a = a
hr' : ∀ (g : G), g • Q ≠ Q → a - eval b r ∈ g • Q
⊢ ¬(map (algebraMap B (B ⧸ Q)) f).coeff j = 0
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: K : Type u_1
inst✝³ : Ring K
inst✝² : NoZeroDivisors K
inst✝¹ : Nontrivial K
G : Subgroup Kˣ
inst✝ : Fintype ↥G
n : ℕ := Fintype.card ↥G
nzero : ↑(Fintype.card ↥G) = 0
p : ℕ
char_p : CharP K p
hd : p ∣ n
pprime : Nat.Prime p
fact_pprime : Fact (Nat.Prime p)
x : ↥G
hx : orderOf x = p
u : K := ↑↑x
⊢ orderOf ↑x = p

Tactic:
Subgroup.orderOf_coe

Goal state after:
K : Type u_1
inst✝³ : Ring K
inst✝² : NoZeroDivisors K
inst✝¹ : Nontrivial K
G : Subgroup Kˣ
inst✝ : Fintype ↥G
n : ℕ := Fintype.card ↥G
nzero : ↑(Fintype.card ↥G) = 0
p : ℕ
char_p : CharP K p
hd : p ∣ n
pprime : Nat.Prime p
fact_pprime : Fact (Nat.Prime p)
x : ↥G
hx : orderOf x = p
u : K := ↑↑x
⊢ orderOf x = p
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
H : Subgroup G
hGKL : IsGaloisGroup G K L
inst✝³ : Finite G
B : Type u_5
inst✝² : CommSemiring B
inst✝¹ : Algebra B L
inst✝ : IsGaloisGroup (↥H) B L
⊢ fixingSubgroup G ↑(FixedPoints.intermediateField ↥H) = H

Tactic:
fixingSubgroup_fixedPoints

Goal state after:
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
H : Subgroup G
hGKL : IsGaloisGroup G K L
inst✝³ : Finite G
B : Type u_5
inst✝² : CommSemiring B
inst✝¹ : Algebra B L
inst✝ : IsGaloisGroup (↥H) B L
⊢ H = H
Module: Mathlib.RingTheory.Int.Basic

Goal state before:
pp: case inl
m : ℤ
p : ℕ
hp : Nat.Prime p
h : ↑p ∣ 2 * m ^ 2
hp2 : p ∣ Int.natAbs 2
⊢ p = 2

Tactic:
exact le_antisymm (Nat.le_of_dvd zero_lt_two hp2) (Nat.Prime.two_le hp)

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

Goal state before:
pp: case succ
p a m d : ℕ
hd : (1 + p * a) ^ p ^ m = p ^ m * d + 1
⊢ ((1 + p * a) ^ p ^ m) ^ p ≡ 1 [MOD p ^ m * p]

Tactic:
hd,

Goal state after:
case succ
p a m d : ℕ
hd : (1 + p * a) ^ p ^ m = p ^ m * d + 1
⊢ (p ^ m * d + 1) ^ p ≡ 1 [MOD p ^ m * p]
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: case inr.inr
n p k : ℕ
inst✝ : Fact (Nat.Prime p)
hn : n = p ^ k
hn0 : n ≠ 0
this : NeZero n
a : ℕ
ha : (orderOf ↑a).Coprime n
h : ¬(a - 1).Coprime (p ^ k)
ha0 : 1 ≤ a
⊢ a ^ p ^ k ≡ 1 [MOD p ^ k]

Tactic:
obtain ⟨b, hb⟩ := not_imp_comm.mp (Nat.Prime.coprime_pow_of_not_dvd Fact.out) h

Goal state after:
case inr.inr
n p k : ℕ
inst✝ : Fact (Nat.Prime p)
hn : n = p ^ k
hn0 : n ≠ 0
this : NeZero n
a : ℕ
ha : (orderOf ↑a).Coprime n
h : ¬(a - 1).Coprime (p ^ k)
ha0 : 1 ≤ a
b : ℕ
hb : a - 1 = p * b
⊢ a ^ p ^ k ≡ 1 [MOD p ^ k]
Module: Mathlib.LinearAlgebra.FreeModule.Finite.Quotient

Goal state before:
pp: M : Type u_3
inst✝² : AddCommGroup M
inst✝¹ : Free ℤ M
inst✝ : Module.Finite ℤ M
N : Submodule ℤ M
h : finrank ℤ ↥N = finrank ℤ M
b : Basis (Free.ChooseBasisIndex ℤ M) ℤ M := Free.chooseBasis ℤ M
a : Free.ChooseBasisIndex ℤ M → ℤ := smithNormalFormCoeffs b h
⊢ Finite (M ⧸ N)

Tactic:
let e := N.quotientEquivPiZMod b h

Goal state after:
M : Type u_3
inst✝² : AddCommGroup M
inst✝¹ : Free ℤ M
inst✝ : Module.Finite ℤ M
N : Submodule ℤ M
h : finrank ℤ ↥N = finrank ℤ M
b : Basis (Free.ChooseBasisIndex ℤ M) ℤ M := Free.chooseBasis ℤ M
a : Free.ChooseBasisIndex ℤ M → ℤ := smithNormalFormCoeffs b h
e : M ⧸ N ≃+ ((i : Free.ChooseBasisIndex ℤ M) → ZMod (smithNormalFormCoeffs b h i).natAbs) := N.quotientEquivPiZMod b h
⊢ Finite (M ⧸ N)
Module: Mathlib.LinearAlgebra.FreeModule.Finite.Quotient

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : IsDomain R
inst✝⁵ : IsPrincipalIdealRing R
inst✝⁴ : Finite ι
F : Type u_4
inst✝³ : CommRing F
inst✝² : Algebra F R
inst✝¹ : Module F M
inst✝ : IsScalarTower F R M
b : Basis ι R M
N : Submodule R M
h : finrank R ↥N = finrank R M
this : Fintype ι
⊢ (M ⧸ N) ≃ₗ[F] ⨁ (i : ι), R ⧸ Ideal.span {smithNormalFormCoeffs b h i}

Tactic:
exact ((N.quotientEquivPiSpan b _).restrictScalars F).trans
    (DirectSum.linearEquivFunOnFintype _ _ _).symm

Goal state after: