mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: case neg
F : Type u
inst✝ : Field F
f g : F[X]
h : ¬f * g = 0
⊢ (f * g).natSepDegree = f.natSepDegree + g.natSepDegree ↔ f = 0 ∧ g = 0 ∨ IsCoprime f g

Tactic:
simp_rw [natSepDegree_eq_of_isAlgClosed (AlgebraicClosure F), aroots_mul h, Multiset.toFinset_add,
    Finset.card_union_eq_card_add_card, Finset.disjoint_iff_ne, Multiset.mem_toFinset, mem_aroots]
  rw [mul_eq_zero, not_or] at h
  refine ⟨fun H ↦ .inr (isCoprime_of_irreducible_dvd (not_and.2 fun _ ↦ h.2)
    fun u hu ⟨v, hf⟩ ⟨w, hg⟩ ↦ ?_), ?_⟩
  · obtain ⟨x, hx⟩ := IsAlgClosed.exists_aeval_eq_zero
      (AlgebraicClosure F) _ (degree_pos_of_irreducible hu).ne'
    exact H x ⟨h.1, by simpa only [map_mul, hx, zero_mul] using congr(aeval x $hf)⟩
      x ⟨h.2, by simpa only [map_mul, hx, zero_mul] using congr(aeval x $hg)⟩ rfl
  rintro (⟨rfl, rfl⟩ | hc)
  · exact (h.1 rfl).elim
  rintro x hf _ hg rfl
  obtain ⟨u, v, hfg⟩ := hc
  simpa only [map_add, map_mul, map_one, hf.2, hg.2, mul_zero, add_zero,
    zero_ne_one] using congr(aeval x $hfg)

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

Goal state before:
pp: case hopen
G : Type u
inst✝ : Group G
B : GroupFilterBasis G
x₀ : G
⊢ ∀ (a : G),
    ∀ i ∈ B.toFilterBasis,
      ∀ᶠ (x : G) in map (fun y ↦ a * y) B.filter, (fun y ↦ a * y) '' id i ∈ map (fun y ↦ x * y) B.filter

Tactic:
intro a U U_in
    rcases GroupFilterBasis.mul U_in with ⟨V, V_in, hVU⟩
    filter_upwards [image_mem_map (B.mem_filter_of_mem V_in)]
    rintro _ ⟨x, hx, rfl⟩
    calc
      (a * x) • V ∈ (a * x) • B.filter := smul_set_mem_smul_filter <| B.mem_filter_of_mem V_in
      _ = a • x • V := smul_smul .. |>.symm
      _ ⊆ a • (V * V) := smul_set_mono <| smul_set_subset_smul hx
      _ ⊆ a • U := smul_set_mono hVU

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
inst✝ : Algebra.EssFiniteType F E
d : Finset E → ℕ := fun s ↦ finInsepDegree (↥(adjoin F ↑s)) E
s : Finset E
hs : adjoin F ↑s = ⊤
⊢ Algebra.IsIntegral (↥⊤) E

Tactic:
refine Algebra.isIntegral_of_surjective topEquiv.surjective

Goal state after:
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
p : F[X]
hFE : FiniteDimensional F E
sp : Polynomial.IsSplittingField F E p
hp : p.Separable
K : Type u_3
inst✝³ : Field K
inst✝² : Algebra F K
inst✝¹ : Algebra K E
inst✝ : IsScalarTower F K E
x : E
hx : x ∈ p.aroots E
h : IsIntegral K x
h1 : p ≠ 0
h2 : minpoly K x ∣ Polynomial.map (algebraMap F K) p
⊢ Nat.card (↥(IntermediateField.restrictScalars F K⟮x⟯) →ₐ[F] E) = Nat.card (K →ₐ[F] E) * finrank K ↥K⟮x⟯

Tactic:
let key_equiv : (K⟮x⟯.restrictScalars F →ₐ[F] E) ≃
      Σ f : K →ₐ[F] E, @AlgHom K K⟮x⟯ E _ _ _ _ (RingHom.toAlgebra f) := by
    change (K⟮x⟯ →ₐ[F] E) ≃ Σ f : K →ₐ[F] E, _
    exact algHomEquivSigma

Goal state after:
F : Type u_1
inst✝⁶ : Field F
E : Type u_2
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
p : F[X]
hFE : FiniteDimensional F E
sp : Polynomial.IsSplittingField F E p
hp : p.Separable
K : Type u_3
inst✝³ : Field K
inst✝² : Algebra F K
inst✝¹ : Algebra K E
inst✝ : IsScalarTower F K E
x : E
hx : x ∈ p.aroots E
h : IsIntegral K x
h1 : p ≠ 0
h2 : minpoly K x ∣ Polynomial.map (algebraMap F K) p
key_equiv : (↥(IntermediateField.restrictScalars F K⟮x⟯) →ₐ[F] E) ≃ (f : K →ₐ[F] E) × (↥K⟮x⟯ →ₐ[K] E) :=
  id algHomEquivSigma
⊢ Nat.card (↥(IntermediateField.restrictScalars F K⟮x⟯) →ₐ[F] E) = Nat.card (K →ₐ[F] E) * finrank K ↥K⟮x⟯
Module: Mathlib.Topology.Algebra.OpenSubgroup

Goal state before:
pp: case succ
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 := { carrier := ⋃ n, V ^ (n + 1), mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }
this : IsOpen[inst✝²] (⋃ n, V ^ (n + 1))
n : ℕ
ih : W * V ^ (n + 1) ⊆ W
⊢ W * V ^ (n + 1 + 1) ⊆ W

Tactic:
rw [pow_succ, ← mul_assoc]

Goal state after:
case succ
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 := { carrier := ⋃ n, V ^ (n + 1), mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }
this : IsOpen[inst✝²] (⋃ n, V ^ (n + 1))
n : ℕ
ih : W * V ^ (n + 1) ⊆ W
⊢ W * V ^ (n + 1) * V ⊆ W
Module: Mathlib.FieldTheory.KrullTopology

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Algebra.IsIntegral K L
σ τ : Gal(L/K)
h_diff : σ ≠ τ
⊢ σ⁻¹ * τ ≠ 1

Tactic:
Ne,

Goal state after:
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Algebra.IsIntegral K L
σ τ : Gal(L/K)
h_diff : σ ≠ τ
⊢ ¬σ⁻¹ * τ = 1
Module: Mathlib.FieldTheory.Galois.Infinite

Goal state before:
pp: case a
k : Type u_1
K : Type u_2
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
L : IntermediateField k K
inst✝ : IsGalois k K
x : K
hx : ∀ f ∈ L.fixingSubgroup, f x = x
mem : x ∈ (adjoin ↥L {x}).toIntermediateField
this✝ : IntermediateField.fixedField ⊤ = ⊥
this : ⟨x, mem⟩ ∈ ⊥
y : ↥L
hy : (algebraMap ↥L ↥(adjoin ↥L {x}).toIntermediateField) y = ⟨x, mem⟩
⊢ x ∈ L

Tactic:
obtain ⟨rfl⟩ : y = x := congrArg Subtype.val hy

Goal state after:
case a
k : Type u_1
K : Type u_2
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
L : IntermediateField k K
inst✝ : IsGalois k K
y : ↥L
hx : ∀ f ∈ L.fixingSubgroup, f ↑y = ↑y
mem : ↑y ∈ (adjoin ↥L {↑y}).toIntermediateField
this✝ : IntermediateField.fixedField ⊤ = ⊥
this : ⟨↑y, mem⟩ ∈ ⊥
hy : (algebraMap ↥L ↥(adjoin ↥L {↑y}).toIntermediateField) y = ⟨↑y, mem⟩
⊢ ↑y ∈ L
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
inst✝ : Nontrivial S
⊢ (minpolyDiv R x).natDegree < (minpoly R x).natDegree

Tactic:
by
  rw [← natDegree_minpolyDiv_succ hx]
  exact Nat.lt_succ_self _

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
⊢ ∃ x, a * x ^ n + b * x + c = 0

Tactic:
let f : k[X] := C a * X ^ n + C b * X + C c
  -- Specify `n := 0` below, otherwise Lean unfolds `0` to `Zero.zero`.
  have hdeg : f.degree ≠ 0 := degree_ne_of_natDegree_ne (n := 0) <| by
    have : C 0 * X ^ n + C b * X = 0 * X ^ n + C b * X := by grind
    by_cases ha : a = 0
    · grind [zero_add]
    · grind [natDegree_add_eq_left_of_natDegree_lt]
  have hsep : f.Separable := separable_C_mul_X_pow_add_C_mul_X_add_C a b c hn hb.isUnit
  obtain ⟨x, hx⟩ := exists_root f hdeg hsep
  exact ⟨x, by simpa [f] using hx⟩

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✝ : 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 * d ≠ 0
⊢ IsUnit a ∨ IsUnit b

Tactic:
Ne,

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 * d = 0
⊢ IsUnit a ∨ IsUnit 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 : 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
h1 : C c * C d * p = integerNormalization R⁰ a * integerNormalization R⁰ b
this : NormalizedGCDMonoid R
⊢ Associated (c * d) (integerNormalization R⁰ a * integerNormalization R⁰ b).content

Tactic:
← h1,

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
h1 : C c * C d * p = integerNormalization R⁰ a * integerNormalization R⁰ b
this : NormalizedGCDMonoid R
⊢ Associated (c * d) (C c * C d * p).content
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
this : NormalizedGCDMonoid R
u : Rˣ
h1 : C (c * d) * (C ↑u * (integerNormalization R⁰ b).primPart * (integerNormalization R⁰ a).primPart) = C (c * d) * p
hu : c * d * ↑u = (integerNormalization R⁰ a).content * (integerNormalization R⁰ b).content
⊢ a ≠ 0 ∧ b ≠ 0

Tactic:
Ne,

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
this : NormalizedGCDMonoid R
u : Rˣ
h1 : C (c * d) * (C ↑u * (integerNormalization R⁰ b).primPart * (integerNormalization R⁰ a).primPart) = C (c * d) * p
hu : c * d * ↑u = (integerNormalization R⁰ a).content * (integerNormalization R⁰ b).content
⊢ ¬a = 0 ∧ b ≠ 0
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
this : NormalizedGCDMonoid R
u : Rˣ
h1 : C (c * d) * (C ↑u * (integerNormalization R⁰ b).primPart * (integerNormalization R⁰ a).primPart) = C (c * d) * p
hu : c * d * ↑u = (integerNormalization R⁰ a).content * (integerNormalization R⁰ b).content
⊢ ¬a = 0 ∧ b ≠ 0

Tactic:
Ne,

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
this : NormalizedGCDMonoid R
u : Rˣ
h1 : C (c * d) * (C ↑u * (integerNormalization R⁰ b).primPart * (integerNormalization R⁰ a).primPart) = C (c * d) * p
hu : c * d * ↑u = (integerNormalization R⁰ a).content * (integerNormalization R⁰ b).content
⊢ ¬a = 0 ∧ ¬b = 0
Module: Mathlib.NumberTheory.NumberField.Basic

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : NumberField K
M : Type u_3
inst✝ : AddZeroClass M
f : M →+ K
h : ∀ (x : M), IsIntegral ℤ (f x)
x y : M
⊢ restrict (⇑f) h (x + y) = restrict (⇑f) h x + restrict (⇑f) h y

Tactic:
by simp only [restrict, map_add]; rfl

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

Goal state before:
pp: G : Type u_1
inst✝⁹ : Group G
B : Type u_3
C : Type u_4
inst✝⁸ : Semiring C
inst✝⁷ : MulSemiringAction G C
N : Subgroup G
inst✝⁶ : CommSemiring B
inst✝⁵ : Algebra B C
inst✝⁴ : FaithfulSMul B C
inst✝³ : MulSemiringAction G B
inst✝² : SMulDistribClass G B C
inst✝¹ : IsGaloisGroup (↥N) B C
inst✝ : N.Normal
g : G
b : B
⊢ ↑g • b = g • b

Tactic:
let := mulSemiringActionOfNormal G B C N

Goal state after:
G : Type u_1
inst✝⁹ : Group G
B : Type u_3
C : Type u_4
inst✝⁸ : Semiring C
inst✝⁷ : MulSemiringAction G C
N : Subgroup G
inst✝⁶ : CommSemiring B
inst✝⁵ : Algebra B C
inst✝⁴ : FaithfulSMul B C
inst✝³ : MulSemiringAction G B
inst✝² : SMulDistribClass G B C
inst✝¹ : IsGaloisGroup (↥N) B C
inst✝ : N.Normal
g : G
b : B
this : MulSemiringAction G B := mulSemiringActionOfNormal G B C N
⊢ ↑g • b = g • b
Module: Mathlib.RingTheory.Trace.Basic

Goal state before:
pp: case pos
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
injKxL : Function.Injective ⇑(algebraMap (↥K⟮x⟯) L)
hx : IsIntegral K x
⊢ (algebraMap K F) ((Algebra.trace K ↥K⟮x⟯) (adjoin.powerBasis hx).gen) = ((minpoly K x).aroots F).sum

Tactic:
(adjoin.powerBasis hx).trace_gen_eq_sum_roots

Goal state after:
case pos
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
injKxL : Function.Injective ⇑(algebraMap (↥K⟮x⟯) L)
hx : IsIntegral K x
⊢ ((minpoly K (adjoin.powerBasis hx).gen).aroots F).sum = ((minpoly K x).aroots F).sum

case pos
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
injKxL : Function.Injective ⇑(algebraMap (↥K⟮x⟯) L)
hx : IsIntegral K x
⊢ (Polynomial.map (algebraMap K F) (minpoly K (adjoin.powerBasis hx).gen)).Splits
Module: Mathlib.RingTheory.Invariant.Basic

Goal state before:
pp: 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 : ¬(algebraMap B (B ⧸ Q)) b = 0
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 : (algebraMap B (B ⧸ Q)) (eval b f) = (algebraMap B (B ⧸ Q)) 0
⊢ (algebraMap B (B ⧸ Q)) (eval b r) = 0

Tactic:
rw [← Polynomial.eval₂_at_apply, ← Polynomial.eval_map] at hf ⊢

Goal state after:
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 : ¬(algebraMap B (B ⧸ Q)) b = 0
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 ((algebraMap B (B ⧸ Q)) b) (map (algebraMap B (B ⧸ Q)) f) = (algebraMap B (B ⧸ Q)) 0
⊢ eval ((algebraMap B (B ⧸ Q)) b) (map (algebraMap B (B ⧸ Q)) r) = 0
Module: Mathlib.Data.ZMod.ValMinAbs

Goal state before:
pp: p q : ℕ
hp : Fact (Nat.Prime p)
hq : Fact (Nat.Prime q)
hpq : p ≠ q
⊢ ↑q ≠ ↑0

Tactic:
Ne,

Goal state after:
p q : ℕ
hp : Fact (Nat.Prime p)
hq : Fact (Nat.Prime q)
hpq : p ≠ q
⊢ ¬↑q = ↑0
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
E : Type u_7
inst✝⁴ : Field E
inst✝³ : Algebra K E
inst✝² : IsAlgClosed E
inst✝¹ : FiniteDimensional K L
inst✝ : Algebra.IsSeparable K L
x : L
⊢ (algebraMap K E) ((Algebra.trace K L) x) = ∑ σ, σ x

Tactic:
by
  have hx := Algebra.IsSeparable.isIntegral K x
  let pb := adjoin.powerBasis hx
  rw [trace_eq_trace_adjoin K x, Algebra.smul_def, map_mul, ← adjoin.powerBasis_gen hx,
    trace_eq_sum_embeddings_gen E pb (IsAlgClosed.splits _), ← Algebra.smul_def,
    algebraMap_smul]
  · exact (sum_embeddings_eq_finrank_mul L E pb).symm
  · have := Algebra.isSeparable_tower_bot_of_isSeparable K K⟮x⟯ L
    exact Algebra.IsSeparable.isSeparable K _

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

Goal state before:
pp: G : Type u_1
inst✝⁷ : Group G
R : Type u_5
B : Type u_6
inst✝⁶ : CommRing R
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : Module.Finite R B
inst✝² : IsDomain B
inst✝¹ : MulSemiringAction G B
inst✝ : IsGaloisGroup G R B
⊢ Finite G

Tactic:
by
  let A : Subring B := (algebraMap R B).range
  let := FractionRing.liftAlgebra A (FractionRing B)
  let := IsFractionRing.mulSemiringAction G B (FractionRing B)
  let : Algebra R A := (algebraMap R B).rangeRestrict.toAlgebra
  have : IsScalarTower R A B := IsScalarTower.of_algebraMap_eq' rfl
  have : Module.Finite A B := Module.Finite.of_restrictScalars_finite R A B
  have := IsGaloisGroup.to_isFractionRing_of_isIntegral G A B (FractionRing A) (FractionRing B)
  apply Nat.finite_of_card_ne_zero
  rw [card_eq_finrank G (FractionRing A) (FractionRing B)]
  exact Module.finrank_pos.ne'

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

Goal state before:
pp: G : Type u_1
inst✝¹⁰ : Group G
inst✝⁹ : Finite G
A : Type u_5
B : Type u_6
C : Type u_7
H : Subgroup G
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
inst✝⁶ : CommRing C
inst✝⁵ : IsDomain C
inst✝⁴ : Algebra A C
inst✝³ : FaithfulSMul A C
inst✝² : MulSemiringAction G C
hGAC : IsGaloisGroup G A C
inst✝¹ : Algebra B C
inst✝ : FaithfulSMul B C
hH : IsGaloisGroup (↥H) B C
this✝² : IsDomain B
this✝¹ : IsDomain A
K : Type u_5 := FractionRing A
L : Type u_7 := FractionRing C
this✝ : MulSemiringAction G L := IsFractionRing.mulSemiringAction G C L
this : IsGaloisGroup (↥H) (FractionRing B) L
g : G
h : ∀ (y : C), (∃ y_1, (algebraMap B C) y_1 = y) → g • y = y
x✝ : FractionRing B
x : B
⊢ g • (algebraMap B L) x = (algebraMap B L) x

Tactic:
rw [IsScalarTower.algebraMap_apply B C L, ← algebraMap.smul', h _ ⟨x, rfl⟩]

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

Goal state before:
pp: case pos
K : Type u_1
inst✝² : Field K
inst✝¹ : Fintype K
inst✝ : DecidableEq K
i : ℕ
φ : Kˣ →* K := { toFun := fun x ↦ ↑x ^ i, map_one' := ⋯, map_mul' := ⋯ }
this✝ : Decidable (φ = 1)
this : q - 1 ∣ i ↔ φ = 1
h✝ : φ = 1
⊢ ↑(Fintype.card Kˣ) = -1

Tactic:
Fintype.card_units,

Goal state after:
case pos
K : Type u_1
inst✝² : Field K
inst✝¹ : Fintype K
inst✝ : DecidableEq K
i : ℕ
φ : Kˣ →* K := { toFun := fun x ↦ ↑x ^ i, map_one' := ⋯, map_mul' := ⋯ }
this✝ : Decidable (φ = 1)
this : q - 1 ∣ i ↔ φ = 1
h✝ : φ = 1
⊢ ↑(q - 1) = -1
Module: Mathlib.RingTheory.Int.Basic

Goal state before:
pp: case a
a b : ℤ
⊢ ↑(a.gcd b) ∣ ↑(EuclideanDomain.gcd a b).natAbs

Tactic:
rw [Int.dvd_natAbs]
    exact EuclideanDomain.dvd_gcd (Int.gcd_dvd_left ..) (Int.gcd_dvd_right ..)

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

Goal state before:
pp: G : Type u_1
G' : Type u_2
inst✝¹⁹ : Group G
inst✝¹⁸ : Group G'
A : Type u_5
B : Type u_6
C : Type u_7
inst✝¹⁷ : CommRing A
inst✝¹⁶ : CommRing B
inst✝¹⁵ : CommRing C
inst✝¹⁴ : IsDomain C
inst✝¹³ : Algebra A B
inst✝¹² : Algebra A C
inst✝¹¹ : Algebra B C
inst✝¹⁰ : FaithfulSMul A B
inst✝⁹ : FaithfulSMul B C
inst✝⁸ : IsScalarTower A B C
inst✝⁷ : Finite G
inst✝⁶ : Finite G'
N : Subgroup G
inst✝⁵ : N.Normal
inst✝⁴ : MulSemiringAction G C
inst✝³ : IsGaloisGroup G A C
inst✝² : IsGaloisGroup (↥N) B C
inst✝¹ : MulSemiringAction G' B
inst✝ : IsGaloisGroup G' A B
g : G
x : B
this : IsDomain B
⊢ (algebraMap B C) ((quotientMulEquiv G G' A B C N) ↑g • x) = g • (algebraMap B C) x

Tactic:
let := mulSemiringActionOfNormal G B C N

Goal state after:
G : Type u_1
G' : Type u_2
inst✝¹⁹ : Group G
inst✝¹⁸ : Group G'
A : Type u_5
B : Type u_6
C : Type u_7
inst✝¹⁷ : CommRing A
inst✝¹⁶ : CommRing B
inst✝¹⁵ : CommRing C
inst✝¹⁴ : IsDomain C
inst✝¹³ : Algebra A B
inst✝¹² : Algebra A C
inst✝¹¹ : Algebra B C
inst✝¹⁰ : FaithfulSMul A B
inst✝⁹ : FaithfulSMul B C
inst✝⁸ : IsScalarTower A B C
inst✝⁷ : Finite G
inst✝⁶ : Finite G'
N : Subgroup G
inst✝⁵ : N.Normal
inst✝⁴ : MulSemiringAction G C
inst✝³ : IsGaloisGroup G A C
inst✝² : IsGaloisGroup (↥N) B C
inst✝¹ : MulSemiringAction G' B
inst✝ : IsGaloisGroup G' A B
g : G
x : B
this✝ : IsDomain B
this : MulSemiringAction G B := mulSemiringActionOfNormal G B C N
⊢ (algebraMap B C) ((quotientMulEquiv G G' A B C N) ↑g • x) = g • (algebraMap B C) x