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

Goal state before:
pp: case refine_2
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
s : S
p : R[X]
hp : (Polynomial.aeval s) p = 0
h₀ : p ≠ 0
pmin : ∀ (q : R[X]), q.Monic → (Polynomial.aeval s) q = 0 → p.degree ≤ q.degree
x✝ : C p.leadingCoeff ∣ p
q : R[X]
hMul : p = C p.leadingCoeff * q
⊢ (Polynomial.aeval s) q = 0

pp: case refine_3
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
s : S
p : R[X]
hp : (Polynomial.aeval s) p = 0
h₀ : p ≠ 0
pmin : ∀ (q : R[X]), q.Monic → (Polynomial.aeval s) q = 0 → p.degree ≤ q.degree
x✝ : C p.leadingCoeff ∣ p
q : R[X]
hMul : p = C p.leadingCoeff * q
⊢ ∀ (Q : R[X]), Q.Monic → (Polynomial.aeval s) Q = 0 → q.degree ≤ Q.degree

Tactic:
· have := congrArg (Polynomial.aeval s) hMul
      simp only [hp, h₀, map_mul, aeval_C, zero_eq_mul, FaithfulSMul.algebraMap_eq_zero_iff,
        leadingCoeff_eq_zero, false_or] at this
      exact this

Goal state after:
case refine_3
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
s : S
p : R[X]
hp : (Polynomial.aeval s) p = 0
h₀ : p ≠ 0
pmin : ∀ (q : R[X]), q.Monic → (Polynomial.aeval s) q = 0 → p.degree ≤ q.degree
x✝ : C p.leadingCoeff ∣ p
q : R[X]
hMul : p = C p.leadingCoeff * q
⊢ ∀ (Q : R[X]), Q.Monic → (Polynomial.aeval s) Q = 0 → q.degree ≤ Q.degree
Module: Mathlib.FieldTheory.Galois.Infinite

Goal state before:
pp: k : Type u_1
K : Type u_2
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
H : ClosedSubgroup Gal(K/k)
inst✝ : IsGalois k K
σ : Gal(K/k)
hσ : σ ∈ (fixedField ↑H).fixingSubgroup
h : σ ∉ ↑H
b : Set Gal(K/k)
sub : b ⊆ (fun y ↦ σ * y) ⁻¹' (↑H).carrierᶜ
gp : Subgroup Gal(K/k)
L : IntermediateField k K
eq : (fun g ↦ g.carrier) L.fixingSubgroup = b
hL : L ∈ finiteExts k K
eq' : L.fixingSubgroup = gp
this : FiniteDimensional k ↥L
L' : FiniteGaloisIntermediateField k K := ⋯
compl : σ • L'.fixingSubgroup.carrier ⊆ (↑H).carrierᶜ
fix : ∀ x ∈ lift (fixedField (Subgroup.map (restrictNormalHom ↥L'.toIntermediateField) ↑H)), σ x = x
⊢ ∀ y ∈ ↑(fixedField (Subgroup.map (restrictNormalHom ↥L'.toIntermediateField) ↑H)),
    (restrictNormalHom ↥L'.toIntermediateField) σ • y = y

Tactic:
intro y hy

Goal state after:
k : Type u_1
K : Type u_2
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
H : ClosedSubgroup Gal(K/k)
inst✝ : IsGalois k K
σ : Gal(K/k)
hσ : σ ∈ (fixedField ↑H).fixingSubgroup
h : σ ∉ ↑H
b : Set Gal(K/k)
sub : b ⊆ (fun y ↦ σ * y) ⁻¹' (↑H).carrierᶜ
gp : Subgroup Gal(K/k)
L : IntermediateField k K
eq : (fun g ↦ g.carrier) L.fixingSubgroup = b
hL : L ∈ finiteExts k K
eq' : L.fixingSubgroup = gp
this : FiniteDimensional k ↥L
L' : FiniteGaloisIntermediateField k K :=
  let __src := normalClosure k (↥L) K;
  { toIntermediateField := __src, finiteDimensional := ⋯, isGalois := ⋯ }
compl : σ • L'.fixingSubgroup.carrier ⊆ (↑H).carrierᶜ
fix : ∀ x ∈ lift (fixedField (Subgroup.map (restrictNormalHom ↥L'.toIntermediateField) ↑H)), σ x = x
y : ↥L'.toIntermediateField
hy : y ∈ ↑(fixedField (Subgroup.map (restrictNormalHom ↥L'.toIntermediateField) ↑H))
⊢ (restrictNormalHom ↥L'.toIntermediateField) σ • y = y
Module: Mathlib.FieldTheory.Galois.Infinite

Goal state before:
pp: case h
k : Type u_1
K : Type u_2
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
H : ClosedSubgroup Gal(K/k)
inst✝ : IsGalois k K
σ : Gal(K/k)
hσ : σ ∈ (fixedField ↑H).fixingSubgroup
h✝ : σ ∉ ↑H
b : Set Gal(K/k)
sub : b ⊆ (fun y ↦ σ * y) ⁻¹' (↑H).carrierᶜ
gp : Subgroup Gal(K/k)
L : IntermediateField k K
eq✝ : (fun g ↦ g.carrier) L.fixingSubgroup = b
hL : L ∈ finiteExts k K
eq' : L.fixingSubgroup = gp
this : FiniteDimensional k ↥L
L' : FiniteGaloisIntermediateField k K := ⋯
compl : σ • L'.fixingSubgroup.carrier ⊆ (↑H).carrierᶜ
fix : ∀ x ∈ lift (fixedField (Subgroup.map (restrictNormalHom ↥L'.toIntermediateField) ↑H)), σ x = x
h : Gal(K/k)
mem : h ∈ ↑↑H
eq : (restrictNormalHom ↥L'.toIntermediateField) h = (restrictNormalHom ↥L'.toIntermediateField) σ
⊢ ∀ y ∈ ↑L'.toIntermediateField, (σ⁻¹ * h) • y = y

Tactic:
intro y hy

Goal state after:
case h
k : Type u_1
K : Type u_2
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
H : ClosedSubgroup Gal(K/k)
inst✝ : IsGalois k K
σ : Gal(K/k)
hσ : σ ∈ (fixedField ↑H).fixingSubgroup
h✝ : σ ∉ ↑H
b : Set Gal(K/k)
sub : b ⊆ (fun y ↦ σ * y) ⁻¹' (↑H).carrierᶜ
gp : Subgroup Gal(K/k)
L : IntermediateField k K
eq✝ : (fun g ↦ g.carrier) L.fixingSubgroup = b
hL : L ∈ finiteExts k K
eq' : L.fixingSubgroup = gp
this : FiniteDimensional k ↥L
L' : FiniteGaloisIntermediateField k K :=
  let __src := normalClosure k (↥L) K;
  { toIntermediateField := __src, finiteDimensional := ⋯, isGalois := ⋯ }
compl : σ • L'.fixingSubgroup.carrier ⊆ (↑H).carrierᶜ
fix : ∀ x ∈ lift (fixedField (Subgroup.map (restrictNormalHom ↥L'.toIntermediateField) ↑H)), σ x = x
h : Gal(K/k)
mem : h ∈ ↑↑H
eq : (restrictNormalHom ↥L'.toIntermediateField) h = (restrictNormalHom ↥L'.toIntermediateField) σ
y : K
hy : y ∈ ↑L'.toIntermediateField
⊢ (σ⁻¹ * h) • y = y
Module: Mathlib.FieldTheory.Minpoly.MinpolyDiv

Goal state before:
pp: K : Type u_2
L : Type u_3
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Algebra K L
E : Type u_1
inst✝⁴ : Field E
inst✝³ : Algebra K E
inst✝² : IsAlgClosed E
inst✝¹ : FiniteDimensional K L
inst✝ : Algebra.IsSeparable K L
x : L
hxL : K[x] = ⊤
r : ℕ
hr : r < finrank K L
this : Function.Injective fun σ ↦ σ x
⊢ ∑ σ, map (↑σ) ((x ^ r / (aeval x) (derivative (minpoly K x))) • minpolyDiv K x) - X ^ r = 0

Tactic:
apply Polynomial.eq_zero_of_natDegree_lt_card_of_eval_eq_zero _ this

Goal state after:
case heval
K : Type u_2
L : Type u_3
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Algebra K L
E : Type u_1
inst✝⁴ : Field E
inst✝³ : Algebra K E
inst✝² : IsAlgClosed E
inst✝¹ : FiniteDimensional K L
inst✝ : Algebra.IsSeparable K L
x : L
hxL : K[x] = ⊤
r : ℕ
hr : r < finrank K L
this : Function.Injective fun σ ↦ σ x
⊢ ∀ (i : L →ₐ[K] E),
    eval (i x) (∑ σ, map (↑σ) ((x ^ r / (aeval x) (derivative (minpoly K x))) • minpolyDiv K x) - X ^ r) = 0

case hcard
K : Type u_2
L : Type u_3
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Algebra K L
E : Type u_1
inst✝⁴ : Field E
inst✝³ : Algebra K E
inst✝² : IsAlgClosed E
inst✝¹ : FiniteDimensional K L
inst✝ : Algebra.IsSeparable K L
x : L
hxL : K[x] = ⊤
r : ℕ
hr : r < finrank K L
this : Function.Injective fun σ ↦ σ x
⊢ (∑ σ, map (↑σ) ((x ^ r / (aeval x) (derivative (minpoly K x))) • minpolyDiv K x) - X ^ r).natDegree <
    Fintype.card (L →ₐ[K] E)
Module: Mathlib.FieldTheory.Minpoly.MinpolyDiv

Goal state before:
pp: case hcard.refine_2
K : Type u_2
L : Type u_3
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Algebra K L
E : Type u_1
inst✝⁴ : Field E
inst✝³ : Algebra K E
inst✝² : IsAlgClosed E
inst✝¹ : FiniteDimensional K L
inst✝ : Algebra.IsSeparable K L
x : L
hxL : K[x] = ⊤
r : ℕ
hr : r < finrank K L
this : Function.Injective fun σ ↦ σ x
⊢ r < Fintype.card (L →ₐ[K] E)

Tactic:
AlgHom.card

Goal state after:
case hcard.refine_2
K : Type u_2
L : Type u_3
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Algebra K L
E : Type u_1
inst✝⁴ : Field E
inst✝³ : Algebra K E
inst✝² : IsAlgClosed E
inst✝¹ : FiniteDimensional K L
inst✝ : Algebra.IsSeparable K L
x : L
hxL : K[x] = ⊤
r : ℕ
hr : r < finrank K L
this : Function.Injective fun σ ↦ σ x
⊢ r < finrank K L
Module: Mathlib.FieldTheory.PurelyInseparable.Basic

Goal state before:
pp: F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
q : ℕ
hF : ExpChar F q
⊢ IsPurelyInseparable F E ↔ ∀ (x : E), ∃ n y, minpoly F x = X ^ q ^ n - C y

Tactic:
simp_rw [isPurelyInseparable_iff_natSepDegree_eq_one,
    minpoly.natSepDegree_eq_one_iff_eq_X_pow_sub_C q]

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

Goal state before:
pp: F : Type u
inst✝² : Field F
K : Type w
inst✝¹ : Field K
inst✝ : Algebra F K
⊢ Algebra.IsSeparable F K ↔ finInsepDegree F K = 1

Tactic:
← separableClosure.eq_top_iff,

Goal state after:
F : Type u
inst✝² : Field F
K : Type w
inst✝¹ : Field K
inst✝ : Algebra F K
⊢ separableClosure F K = ⊤ ↔ finInsepDegree F K = 1
Module: Mathlib.RingTheory.DedekindDomain.IntegralClosure

Goal state before:
pp: case refine_1
A : Type u_1
K : Type u_2
inst✝¹⁴ : CommRing A
inst✝¹³ : Field K
inst✝¹² : Algebra A K
inst✝¹¹ : IsFractionRing A K
L : Type u_3
inst✝¹⁰ : Field L
C : Type u_4
inst✝⁹ : CommRing C
inst✝⁸ : Algebra K L
inst✝⁷ : Algebra A L
inst✝⁶ : IsScalarTower A K L
inst✝⁵ : Algebra C L
inst✝⁴ : IsIntegralClosure C A L
inst✝³ : Algebra A C
inst✝² : IsScalarTower A C L
inst✝¹ : IsDomain A
inst✝ : Algebra.IsAlgebraic K L
this✝¹ : IsDomain C
this✝ : IsTorsionFree A L
this : IsTorsionFree A C
x : A
hx : x ∈ ↑A⁰
⊢ IsUnit ((algebraMap C L) ↑⟨(algebraMap A C) x, ⋯⟩)

Tactic:
rw [isUnit_iff_ne_zero, map_ne_zero_iff _ (IsIntegralClosure.algebraMap_injective C A L),
      Subtype.coe_mk, map_ne_zero_iff _ (FaithfulSMul.algebraMap_injective A C)]

Goal state after:
case refine_1
A : Type u_1
K : Type u_2
inst✝¹⁴ : CommRing A
inst✝¹³ : Field K
inst✝¹² : Algebra A K
inst✝¹¹ : IsFractionRing A K
L : Type u_3
inst✝¹⁰ : Field L
C : Type u_4
inst✝⁹ : CommRing C
inst✝⁸ : Algebra K L
inst✝⁷ : Algebra A L
inst✝⁶ : IsScalarTower A K L
inst✝⁵ : Algebra C L
inst✝⁴ : IsIntegralClosure C A L
inst✝³ : Algebra A C
inst✝² : IsScalarTower A C L
inst✝¹ : IsDomain A
inst✝ : Algebra.IsAlgebraic K L
this✝¹ : IsDomain C
this✝ : IsTorsionFree A L
this : IsTorsionFree A C
x : A
hx : x ∈ ↑A⁰
⊢ x ≠ 0
Module: Mathlib.RingTheory.Invariant.Basic

Goal state before:
pp: B : Type u_2
G : Type u_3
inst✝³ : CommRing B
inst✝² : Group G
inst✝¹ : MulSemiringAction G B
inst✝ : Fintype G
b : B
⊢ eval b X - eval b (C b) = 0

Tactic:
eval_C,

Goal state after:
B : Type u_2
G : Type u_3
inst✝³ : CommRing B
inst✝² : Group G
inst✝¹ : MulSemiringAction G B
inst✝ : Fintype G
b : B
⊢ eval b X - b = 0
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
inst✝ : SMulCommClass G A B
P✝ Q✝ : Ideal B
hP✝ : P✝.IsPrime
hQ✝ : Q✝.IsPrime
hPQ✝ : Ideal.under A P✝ = Ideal.under A Q✝
val✝ : Fintype G
P Q : Ideal B
hP : P.IsPrime
hQ : Q.IsPrime
hPQ : Ideal.under A P = Ideal.under A Q
b : B
hb : b ∈ ↑Q
a : A
ha : (algebraMap A B) a = ∏ g, g • b
⊢ ∏ g, g • b ∈ Q

Tactic:
hQ.prod_mem_iff

Goal state after:
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
inst✝ : SMulCommClass G A B
P✝ Q✝ : Ideal B
hP✝ : P✝.IsPrime
hQ✝ : Q✝.IsPrime
hPQ✝ : Ideal.under A P✝ = Ideal.under A Q✝
val✝ : Fintype G
P Q : Ideal B
hP : P.IsPrime
hQ : Q.IsPrime
hPQ : Ideal.under A P = Ideal.under A Q
b : B
hb : b ∈ ↑Q
a : A
ha : (algebraMap A B) a = ∏ g, g • b
⊢ ∃ i ∈ Finset.univ, i • b ∈ Q
Module: Mathlib.RingTheory.Trace.Basic

Goal state before:
pp: R : Type u_1
inst✝⁷ : CommRing R
L : Type u_5
inst✝⁶ : Field L
F : Type u_6
inst✝⁵ : Field F
inst✝⁴ : Algebra R L
inst✝³ : Algebra L F
inst✝² : Algebra R F
inst✝¹ : IsScalarTower R L F
inst✝ : FiniteDimensional L F
x : F
hx : IsIntegral R x
hx' : IsIntegral L x
⊢ IsIntegral R ((trace L F) x)

Tactic:
rw [← isIntegral_algebraMap_iff (algebraMap L (AlgebraicClosure F)).injective, trace_eq_sum_roots]

Goal state after:
R : Type u_1
inst✝⁷ : CommRing R
L : Type u_5
inst✝⁶ : Field L
F : Type u_6
inst✝⁵ : Field F
inst✝⁴ : Algebra R L
inst✝³ : Algebra L F
inst✝² : Algebra R F
inst✝¹ : IsScalarTower R L F
inst✝ : FiniteDimensional L F
x : F
hx : IsIntegral R x
hx' : IsIntegral L x
⊢ IsIntegral R (finrank (↥L⟮x⟯) F • ((minpoly L x).aroots (AlgebraicClosure F)).sum)

R : Type u_1
inst✝⁷ : CommRing R
L : Type u_5
inst✝⁶ : Field L
F : Type u_6
inst✝⁵ : Field F
inst✝⁴ : Algebra R L
inst✝³ : Algebra L F
inst✝² : Algebra R F
inst✝¹ : IsScalarTower R L F
inst✝ : FiniteDimensional L F
x : F
hx : IsIntegral R x
hx' : IsIntegral L x
⊢ (Polynomial.map (algebraMap L (AlgebraicClosure F)) (minpoly L x)).Splits
Module: Mathlib.RingTheory.Trace.Basic

Goal state before:
pp: R : Type u_1
inst✝⁷ : CommRing R
L : Type u_5
inst✝⁶ : Field L
F : Type u_6
inst✝⁵ : Field F
inst✝⁴ : Algebra R L
inst✝³ : Algebra L F
inst✝² : Algebra R F
inst✝¹ : IsScalarTower R L F
inst✝ : FiniteDimensional L F
x : F
hx : IsIntegral R x
hx' : IsIntegral L x
⊢ ∀ x_1 ∈ (minpoly L x).aroots (AlgebraicClosure F), IsIntegral R x_1

Tactic:
intro y hy

Goal state after:
R : Type u_1
inst✝⁷ : CommRing R
L : Type u_5
inst✝⁶ : Field L
F : Type u_6
inst✝⁵ : Field F
inst✝⁴ : Algebra R L
inst✝³ : Algebra L F
inst✝² : Algebra R F
inst✝¹ : IsScalarTower R L F
inst✝ : FiniteDimensional L F
x : F
hx : IsIntegral R x
hx' : IsIntegral L x
y : AlgebraicClosure F
hy : y ∈ (minpoly L x).aroots (AlgebraicClosure F)
⊢ IsIntegral R y
Module: Mathlib.RingTheory.Trace.Basic

Goal state before:
pp: case pos.succ
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
h₀ : FiniteDimensional K L
x : ↥(separableClosure K L)
n : ℕ
hn : finrank (↥(separableClosure K L)) L = p ^ (n + 1)
⊢ (trace K ↥(separableClosure K L)) (finrank (↥(separableClosure K L)) L • x) =
    0 ((algebraMap (↥(separableClosure K L)) L) x)

Tactic:
cases hp with

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✝¹ : Finite G
inst✝ : IsGaloisGroup G K L
⊢ IsGalois (↥(FixedPoints.intermediateField G)) L

Tactic:
exact IsGalois.of_fixed_field L G

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

Goal state before:
pp: case neg
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : NoZeroDivisors B
b : B
i j : ℕ
p : A[X]
h : map (algebraMap A B) p = (X - C b) ^ i * X ^ j
f : B ≃ₐ[A] B
hi : i ≠ 0
ha : ¬b = 0
hf : (b - eval b (C b)) ^ i * b ^ j = (b - eval b (C (↑↑f b))) ^ i * b ^ j
⊢ f b = b

Tactic:
eval_C,

Goal state after:
case neg
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : NoZeroDivisors B
b : B
i j : ℕ
p : A[X]
h : map (algebraMap A B) p = (X - C b) ^ i * X ^ j
f : B ≃ₐ[A] B
hi : i ≠ 0
ha : ¬b = 0
hf : (b - b) ^ i * b ^ j = (b - ↑↑f b) ^ i * b ^ j
⊢ f b = b
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: K : Type u_1
inst✝³ : Ring K
inst✝² : NoZeroDivisors K
G : Subgroup Kˣ
inst✝¹ : Fintype ↥G
inst✝ : Decidable (G = ⊥)
⊢ ∑ x, ↑↑x = if G = ⊥ then 1 else 0

Tactic:
by_cases G_bot : G = ⊥
  · subst G_bot
    simp only [univ_unique, sum_singleton, ↓reduceIte, Units.val_eq_one, OneMemClass.coe_eq_one]
    rw [Set.default_coe_singleton]
    rfl
  · simp only [G_bot, ite_false]
    exact sum_subgroup_units_eq_zero G_bot

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

Goal state before:
pp: case refine_1
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
⊢ g • (algebraMap (FractionRing B) L) x = (algebraMap (FractionRing B) L) x

Tactic:
have {x} : g • (algebraMap B L) x = (algebraMap B L) x := by
      rw [IsScalarTower.algebraMap_apply B C L, ← algebraMap.smul', h _ ⟨x, rfl⟩]

Goal state after:
case refine_1
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
this : ∀ {x : B}, g • (algebraMap B L) x = (algebraMap B L) x
⊢ g • (algebraMap (FractionRing B) L) x = (algebraMap (FractionRing B) L) x
Module: Mathlib.RingTheory.Invariant.Basic

Goal state before:
pp: case intro
A : Type u_1
B : Type u_2
inst✝¹⁸ : CommRing A
inst✝¹⁷ : CommRing B
inst✝¹⁶ : Algebra A B
G : Type u_3
inst✝¹⁵ : Group G
inst✝¹⁴ : Finite G
inst✝¹³ : MulSemiringAction G B
inst✝¹² : SMulCommClass G A B
P : Ideal A
Q : Ideal B
inst✝¹¹ : Q.IsPrime
inst✝¹⁰ : Q.LiesOver P
K : Type u_4
L : Type u_5
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : Algebra (A ⧸ P) K
inst✝⁶ : Algebra (B ⧸ Q) L
inst✝⁵ : Algebra (A ⧸ P) L
inst✝⁴ : IsScalarTower (A ⧸ P) (B ⧸ Q) L
inst✝³ : Algebra K L
inst✝² : IsScalarTower (A ⧸ P) K L
inst✝¹ : Algebra.IsInvariant A B G
inst✝ : Module.IsTorsionFree (B ⧸ Q) L
f : Gal(L/K)
val✝ : Fintype G
b₀ : B
hx :
  ∀ (g : ↥(MulAction.stabilizer G Q)),
    ((Ideal.Quotient.stabilizerHom Q P G) g) ((Ideal.Quotient.mk Q) b₀) = (Ideal.Quotient.mk Q) b₀
a b : B
ha1 : ∀ (g : G), g • a = a
ha2 : a ∉ Q
hb : ∀ (g : G), (algebraMap B (B ⧸ Q)) (g • b) = (algebraMap B (B ⧸ Q)) (if g • Q = Q then a * b₀ else 0)
M : A[X]
key : map (algebraMap (A ⧸ P) (B ⧸ Q)) (map (algebraMap A (A ⧸ P)) M) = ∏ i, map (algebraMap B (B ⧸ Q)) (X - C (i • b))
key₀ :
  ∀ (g : G),
    map (algebraMap B (B ⧸ Q)) (X - C (g • b)) = if g • Q = Q then X - C ((algebraMap B (B ⧸ Q)) (a * b₀)) else X
⊢ f ((algebraMap (B ⧸ Q) L) ((algebraMap B (B ⧸ Q)) b₀)) = (algebraMap (B ⧸ Q) L) ((algebraMap B (B ⧸ Q)) b₀)

Tactic:
simp only [key₀, Finset.prod_ite, Finset.prod_const] at key

Goal state after:
case intro
A : Type u_1
B : Type u_2
inst✝¹⁸ : CommRing A
inst✝¹⁷ : CommRing B
inst✝¹⁶ : Algebra A B
G : Type u_3
inst✝¹⁵ : Group G
inst✝¹⁴ : Finite G
inst✝¹³ : MulSemiringAction G B
inst✝¹² : SMulCommClass G A B
P : Ideal A
Q : Ideal B
inst✝¹¹ : Q.IsPrime
inst✝¹⁰ : Q.LiesOver P
K : Type u_4
L : Type u_5
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : Algebra (A ⧸ P) K
inst✝⁶ : Algebra (B ⧸ Q) L
inst✝⁵ : Algebra (A ⧸ P) L
inst✝⁴ : IsScalarTower (A ⧸ P) (B ⧸ Q) L
inst✝³ : Algebra K L
inst✝² : IsScalarTower (A ⧸ P) K L
inst✝¹ : Algebra.IsInvariant A B G
inst✝ : Module.IsTorsionFree (B ⧸ Q) L
f : Gal(L/K)
val✝ : Fintype G
b₀ : B
hx :
  ∀ (g : ↥(MulAction.stabilizer G Q)),
    ((Ideal.Quotient.stabilizerHom Q P G) g) ((Ideal.Quotient.mk Q) b₀) = (Ideal.Quotient.mk Q) b₀
a b : B
ha1 : ∀ (g : G), g • a = a
ha2 : a ∉ Q
hb : ∀ (g : G), (algebraMap B (B ⧸ Q)) (g • b) = (algebraMap B (B ⧸ Q)) (if g • Q = Q then a * b₀ else 0)
M : A[X]
key₀ :
  ∀ (g : G),
    map (algebraMap B (B ⧸ Q)) (X - C (g • b)) = if g • Q = Q then X - C ((algebraMap B (B ⧸ Q)) (a * b₀)) else X
key :
  map (algebraMap (A ⧸ P) (B ⧸ Q)) (map (algebraMap A (A ⧸ P)) M) =
    (X - C ((algebraMap B (B ⧸ Q)) (a * b₀))) ^ {x | x • Q = Q}.card * X ^ {x | ¬x • Q = Q}.card
⊢ f ((algebraMap (B ⧸ Q) L) ((algebraMap B (B ⧸ Q)) b₀)) = (algebraMap (B ⧸ Q) L) ((algebraMap B (B ⧸ Q)) b₀)
Module: Mathlib.RingTheory.Int.Basic

Goal state before:
pp: m n : ℤ
p : ℕ
hp : Nat.Prime p
h : ↑p ∣ m * n
⊢ ↑p ∣ m ∨ ↑p ∣ n

Tactic:
rw [Int.natCast_dvd, Int.natCast_dvd]

Goal state after:
m n : ℤ
p : ℕ
hp : Nat.Prime p
h : ↑p ∣ m * n
⊢ p ∣ m.natAbs ∨ p ∣ n.natAbs
Module: Mathlib.RingTheory.Int.Basic

Goal state before:
pp: n : ℤ
k p : ℕ
hp : Nat.Prime p
h : ↑p ∣ n ^ k
⊢ ↑p ∣ n

Tactic:
by
  rw [Int.natCast_dvd]
  exact Int.Prime.dvd_pow hp h

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
i : ℕ
h : i < q - 1
hi : ¬i = 0
hiq : ¬q - 1 ∣ i
φ : Kˣ ↪ K := { toFun := fun x ↦ ↑x, inj' := ⋯ }
this : map φ univ = univ \ {0}
⊢ ∑ x, ↑x ^ i = 0

Tactic:
rw [sum_pow_units K i, if_neg]; exact hiq

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
aux : X ^ q - X ≠ 0
x : K
⊢ (X ^ q - X).IsRoot x

Tactic:
IsRoot.def,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
aux : X ^ q - X ≠ 0
x : K
⊢ eval x (X ^ q - X) = 0
Module: Mathlib.RingTheory.Invariant.Basic

Goal state before:
pp: case intro
A : Type u_1
B : Type u_2
k : Type u_3
inst✝¹³ : CommRing A
inst✝¹² : CommRing B
inst✝¹¹ : Algebra A B
G : Type u_4
inst✝¹⁰ : Finite G
inst✝⁹ : Group G
inst✝⁸ : MulSemiringAction G B
inst✝⁷ : Algebra.IsInvariant A B G
P✝ : Ideal A
Q : Ideal B
inst✝⁶ : Q.LiesOver P✝
inst✝⁵ : CommRing k
inst✝⁴ : Algebra (A ⧸ P✝) k
inst✝³ : Algebra (B ⧸ Q) k
inst✝² : IsScalarTower (A ⧸ P✝) (B ⧸ Q) k
inst✝¹ : IsDomain k
inst✝ : FaithfulSMul (B ⧸ Q) k
σ : k →ₐ[A ⧸ P✝] k
f : B ⧸ Q →ₐ[A ⧸ P✝] k := IsScalarTower.toAlgHom (A ⧸ P✝) (B ⧸ Q) k
hf : Function.Injective ⇑f
x : B
val✝ : Fintype G
algInst✝¹ : Algebra A k := ((algebraMap (A ⧸ P✝) k).comp (algebraMap A (A ⧸ P✝))).toAlgebra
algInst✝ : Algebra B k := ((algebraMap (B ⧸ Q) k).comp (algebraMap B (B ⧸ Q))).toAlgebra
scalarTowerInst✝¹ : IsScalarTower A (A ⧸ P✝) k := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap A k))
scalarTowerInst✝ : IsScalarTower B (B ⧸ Q) k := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap B k))
this✝² : IsScalarTower A (B ⧸ Q) k
this✝¹ : IsScalarTower A B k
P : Polynomial A
hp : (Polynomial.mapRingHom (algebraMap A B)) P = MulSemiringAction.charpoly G x
this✝ : (Polynomial.aeval x) P = 0
this : (Polynomial.aeval (σ ((algebraMap (B ⧸ Q) k) ((mk Q) x)))) (MulSemiringAction.charpoly G x) = 0
⊢ (σ.comp f).toRingHom ((mk Q) x) ∈ f.range

Tactic:
obtain ⟨τ, hτ⟩ : ∃ τ : G, σ (algebraMap _ _ x) = algebraMap _ _ (τ • x) := by
    simpa [MulSemiringAction.charpoly, sub_eq_zero, Finset.prod_eq_zero_iff] using! this

Goal state after:
case intro
A : Type u_1
B : Type u_2
k : Type u_3
inst✝¹³ : CommRing A
inst✝¹² : CommRing B
inst✝¹¹ : Algebra A B
G : Type u_4
inst✝¹⁰ : Finite G
inst✝⁹ : Group G
inst✝⁸ : MulSemiringAction G B
inst✝⁷ : Algebra.IsInvariant A B G
P✝ : Ideal A
Q : Ideal B
inst✝⁶ : Q.LiesOver P✝
inst✝⁵ : CommRing k
inst✝⁴ : Algebra (A ⧸ P✝) k
inst✝³ : Algebra (B ⧸ Q) k
inst✝² : IsScalarTower (A ⧸ P✝) (B ⧸ Q) k
inst✝¹ : IsDomain k
inst✝ : FaithfulSMul (B ⧸ Q) k
σ : k →ₐ[A ⧸ P✝] k
f : B ⧸ Q →ₐ[A ⧸ P✝] k := IsScalarTower.toAlgHom (A ⧸ P✝) (B ⧸ Q) k
hf : Function.Injective ⇑f
x : B
val✝ : Fintype G
algInst✝¹ : Algebra A k := ((algebraMap (A ⧸ P✝) k).comp (algebraMap A (A ⧸ P✝))).toAlgebra
algInst✝ : Algebra B k := ((algebraMap (B ⧸ Q) k).comp (algebraMap B (B ⧸ Q))).toAlgebra
scalarTowerInst✝¹ : IsScalarTower A (A ⧸ P✝) k := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap A k))
scalarTowerInst✝ : IsScalarTower B (B ⧸ Q) k := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap B k))
this✝² : IsScalarTower A (B ⧸ Q) k
this✝¹ : IsScalarTower A B k
P : Polynomial A
hp : (Polynomial.mapRingHom (algebraMap A B)) P = MulSemiringAction.charpoly G x
this✝ : (Polynomial.aeval x) P = 0
this : (Polynomial.aeval (σ ((algebraMap (B ⧸ Q) k) ((mk Q) x)))) (MulSemiringAction.charpoly G x) = 0
τ : G
hτ : σ ((algebraMap B k) x) = (algebraMap B k) (τ • x)
⊢ (σ.comp f).toRingHom ((mk Q) x) ∈ f.range