mathlib-initiative/mathlib-tactics huggingface dataset:
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
E : Type u_5
inst✝⁶ : Field E
inst✝⁵ : Algebra K E
inst✝⁴ : Algebra E L
inst✝³ : IsScalarTower K E L
inst✝² : Finite G
inst✝¹ : IsGaloisGroup (↥H) E L
inst✝ : IsGalois K E
⊢ H.Normal

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝¹ : GroupWithZero K
inst✝ : Fintype K
a : K
⊢ a ^ q = a

Tactic:
by

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

Goal state before:
pp: G : Type u_1
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
N : Subgroup G
inst✝⁷ : N.Normal
inst✝⁶ : MulSemiringAction G C
hG : IsGaloisGroup G A C
inst✝⁵ : MulSemiringAction G B
inst✝⁴ : MulSemiringAction (G ⧸ N) B
inst✝³ : SMulCommClass (G ⧸ N) A B
inst✝² : SMulDistribClass G B C
inst✝¹ : IsScalarTower G (G ⧸ N) B
inst✝ : IsGaloisGroup (↥N) B C
g₁✝ g₂✝ : G ⧸ N
g₁ g₂ : G
h : ∀ (a : B), Quotient.mk'' g₁ • a = Quotient.mk'' g₂ • a
this : FaithfulSMul A C
⊢ ∀ (g : G), (∀ (x : B), g • x = x) → g ∈ N

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝¹ : GroupWithZero K
inst✝ : Fintype K
n : ℕ
a : K
⊢ a ^ q ^ n = a

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : Fintype K
p : ℕ
inst✝ : CharP K p
hp : Fact (Nat.Prime p)
this : Module (ZMod p) K :=
  let __src := (ZMod.castHom ⋯ K).toModule;
  __src
h : q = 1
⊢ 0 = 1

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : Fintype K
p : ℕ
inst✝ : CharP K p
⊢ ∃ n, Nat.Prime p ∧ q = p ^ ↑n

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
⊢ IsPrimePow q

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
⊢ ↑q = 0

Tactic:
by

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

Goal state before:
pp: 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))
⊢ ∀ (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

Tactic:
by

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
inst✝¹ : FiniteDimensional K L
inst✝ : Algebra.IsSeparable K L
pb : PowerBasis K L
i : Fin pb.dim
⊢ pb.basis.traceDual i = (minpolyDiv K pb.gen).coeff ↑i / (aeval pb.gen) (derivative (minpoly K pb.gen))

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
i : ℕ
⊢ (∀ (x : Kˣ), x ^ i = 1) ↔ q - 1 ∣ i

Tactic:
by

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

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 : ℕ
⊢ ∀ (x y : Kˣ), ↑(x * y) ^ i = ↑x ^ i * ↑y ^ i

Tactic:
by

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 : ℕ
φ : Kˣ →* K := { toFun := fun x ↦ ↑x ^ i, map_one' := ⋯, map_mul' := ⋯ }
⊢ Decidable (φ = 1)

Tactic:
by

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

Goal state before:
pp: G : Type u_1
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
N : Subgroup G
inst✝⁷ : N.Normal
inst✝⁶ : MulSemiringAction G C
hG : IsGaloisGroup G A C
inst✝⁵ : MulSemiringAction G B
inst✝⁴ : MulSemiringAction (G ⧸ N) B
inst✝³ : SMulCommClass (G ⧸ N) A B
inst✝² : SMulDistribClass G B C
inst✝¹ : IsScalarTower G (G ⧸ N) B
inst✝ : IsGaloisGroup (↥N) B C
g₁✝ g₂✝ : G ⧸ N
g₁ g₂ : G
h : ∀ (a : B), Quotient.mk'' g₁ • a = Quotient.mk'' g₂ • a
⊢ Quotient.mk'' g₁ = Quotient.mk'' g₂

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.FreeModule.Determinant

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Module.Free R M
inst✝¹ : Module.Finite R M
inst✝ : Nontrivial M
⊢ LinearMap.det 0 = 0

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: a b : ℤ
⊢ a.natAbs = b.natAbs ↔ Associated a b

Tactic:
by

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

Goal state before:
pp: a b : ℕ
h : b ≤ a
⊢ (↑a - ↑b).natAbs = a - b

Tactic:
by

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

Goal state before:
pp: a b : ℕ
h : a ≤ b
⊢ (↑a - ↑b).natAbs = b - a

Tactic:
by

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

Goal state before:
pp: a b : ℤ
⊢ IsCoprime a b ↔ a.natAbs.Coprime b.natAbs

Tactic:
by

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

Goal state before:
pp: a : ℤ
m n : ℕ
⊢ a.gcd (↑m * ↑n) ≠ 1 ↔ a.gcd ↑m ≠ 1 ∨ a.gcd ↑n ≠ 1

Tactic:
by

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

Goal state before:
pp: a b c : ℤ
h : a.gcd b = 1
heq : a * b = c ^ 2
⊢ IsUnit (GCDMonoid.gcd a b)

Tactic:
by

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

Goal state before:
pp: a b c : ℤ
h : a.gcd b = 1
heq : a * b = c ^ 2
⊢ ∃ a0, a = a0 ^ 2 ∨ a = -a0 ^ 2

Tactic:
by

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

Goal state before:
pp: a b : ℤ
⊢ (EuclideanDomain.gcd a b).natAbs = a.gcd b

Tactic:
by

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

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

Tactic:
by

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 : ℕ
φ : Kˣ →* K := { toFun := fun x ↦ ↑x ^ i, map_one' := ⋯, map_mul' := ⋯ }
this✝ : Decidable (φ = 1)
this : q - 1 ∣ i ↔ φ = 1
⊢ ↑(if φ = 1 then Fintype.card Kˣ else 0) = if q - 1 ∣ i then -1 else 0

Tactic:
by

Goal state after:
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:
by

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 : ℕ
φ : Kˣ →* K := { toFun := fun x ↦ ↑x ^ i, map_one' := ⋯, map_mul' := ⋯ }
this : Decidable (φ = 1)
⊢ ↑(if φ = 1 then Fintype.card Kˣ else 0) = if q - 1 ∣ i then -1 else 0

Tactic:
by

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

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

Tactic:
by

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 : ℕ
⊢ ∑ x, ↑x ^ i = if q - 1 ∣ i then -1 else 0

Tactic:
by

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

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

Tactic:
by

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
⊢ ¬q - 1 ∣ i

Tactic:
by

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' := ⋯ }
⊢ map φ univ = univ \ {0}

Tactic:
by

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

Goal state before:
pp: G : Type u_1
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
N : Subgroup G
inst✝⁷ : N.Normal
inst✝⁶ : MulSemiringAction G C
hG : IsGaloisGroup G A C
inst✝⁵ : MulSemiringAction G B
inst✝⁴ : MulSemiringAction (G ⧸ N) B
inst✝³ : SMulCommClass (G ⧸ N) A B
inst✝² : SMulDistribClass G B C
inst✝¹ : IsScalarTower G (G ⧸ N) B
inst✝ : IsGaloisGroup (↥N) B C
x : B
h : ∀ (g : G ⧸ N), g • x = x
⊢ ∃ a, (algebraMap A B) a = x

Tactic:
by

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 = ∑ x ∈ univ \ {0}, x ^ i

Tactic:
by

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

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

Tactic:
by

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 ∈ univ \ {0}, x ^ i = ∑ x, ↑x ^ i

Tactic:
by

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

Goal state before:
pp: n : ℤ
hn : n.natAbs ≠ 1
⊢ ∃ p, Prime p ∧ p ∣ n

Tactic:
by

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

Goal state before:
pp: a : ℤ
⊢ Ideal.span {↑a.natAbs} = Ideal.span {a}

Tactic:
by

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:
by

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

Goal state before:
pp: m : ℤ
⊢ IsCoprime 2 m ↔ Odd m

Tactic:
by

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

Goal state before:
pp: m : ℤ
⊢ IsCoprime m 2 ↔ Odd m

Tactic:
by

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
⊢ ∑ x, x ^ i = 0

Tactic:
by

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

Goal state before:
pp: K : Type u_1
R : Type u_2
inst✝³ : Field K
inst✝² : Fintype K
inst✝¹ : CommRing R
inst✝ : Algebra K R
x✝¹ x✝ : R
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
by

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

Goal state before:
pp: K : Type u_1
R : Type u_2
inst✝³ : Field K
inst✝² : Fintype K
inst✝¹ : CommRing R
inst✝ : Algebra K R
x✝ : K
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
by

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

Goal state before:
pp: K : Type u_1
R : Type u_2
inst✝⁵ : Field K
inst✝⁴ : Fintype K
inst✝³ : CommRing R
inst✝² : Algebra K R
p : ℕ
inst✝¹ : ExpChar R p
inst✝ : PerfectRing R p
⊢ Function.Bijective ⇑(frobeniusAlgHom K R)

Tactic:
by

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
⊢ (algebraMap B C) ((quotientMulEquiv G G' A B C N) ↑g • x) = g • (algebraMap B C) x

Tactic:
by

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

Goal state before:
pp: a b c : ℤ
hab : IsCoprime a b
k : ℕ
hk : Odd k
h : a * b = c ^ k
⊢ ∃ d, a = d ^ k

Tactic:
by

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

Goal state before:
pp: a b c : ℤ
hab : IsCoprime a b
k : ℕ
hk : Odd k
h : a * b = c ^ k
⊢ b * a = c ^ k

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝⁴ : Field K
inst✝³ : Fintype K
L : Type u_3
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Finite L
this : Fintype L
m : ℕ
lt : m < Module.finrank K L
pos : 0 < m
eq : frobeniusAlgHom K L ^ m = 1
x : L
x✝ : x ∈ univ.val
⊢ x ∈ (X ^ q ^ m - X).roots

Tactic:
by

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'
inst✝³ : MulSemiringAction G C
inst✝² : IsGaloisGroup G A C
inst✝¹ : MulSemiringAction G' B
inst✝ : IsGaloisGroup G' A B
g : G
x : B
⊢ (algebraMap B C) ((restrictHom G G' A B C) g • x) = g • (algebraMap B C) x

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝⁴ : Field K
inst✝³ : Fintype K
L : Type u_3
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Finite L
⊢ frobeniusAlgHom K L ^ Module.finrank K L = 1 ∧ ∀ m < Module.finrank K L, 0 < m → frobeniusAlgHom K L ^ m ≠ 1

Tactic:
by

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'
inst✝³ : MulSemiringAction G C
inst✝² : IsGaloisGroup G A C
inst✝¹ : MulSemiringAction G' B
inst✝ : IsGaloisGroup G' A B
⊢ Function.Surjective ⇑(restrictHom G G' A B C)

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝⁴ : Field K
inst✝³ : Fintype K
L : Type u_3
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Finite L
⊢ orderOf (frobeniusAlgEquivOfAlgebraic K L) = Module.finrank K L

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝⁴ : Field K
inst✝³ : Fintype K
L : Type u_3
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Finite L
e : Fin (Module.finrank K L) ≃ ↥(Submonoid.powers (frobeniusAlgHom K L)) := (finCongr ⋯).symm.trans (finEquivPowers ⋯)
⊢ Module.finrank K L = Nat.card (Fin (Module.finrank K L))

Tactic:
by

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'
inst✝³ : MulSemiringAction G C
inst✝² : IsGaloisGroup G A C
inst✝¹ : MulSemiringAction G' B
inst✝ : IsGaloisGroup G' A B
g : G
I : Ideal C
⊢ (restrictHom G G' A B C) g • Ideal.under B I = Ideal.under B (g • I)

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝⁴ : Field K
inst✝³ : Fintype K
L : Type u_3
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Finite L
⊢ Function.Bijective (⇑(Algebra.IsAlgebraic.algEquivEquivAlgHom K L) ∘ fun n ↦ frobeniusAlgEquivOfAlgebraic K L ^ ↑n)

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝⁴ : Field K
inst✝³ : Fintype K
L : Type u_3
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Finite L
x : L
⊢ ((aeval (frobeniusAlgHom K L).toLinearMap) (X ^ Module.finrank K L - 1)) x = 0 x

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝⁴ : Field K
inst✝³ : Fintype K
L : Type u_3
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Finite L
⊢ LinearIndependent K fun i ↦ (frobeniusAlgHom K L).toLinearMap ^ ↑i

Tactic:
by

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

Goal state before:
pp: K' : Type u_3
inst✝ : Field K'
p : ℕ
hp : 1 < p
⊢ X.degree < (X ^ p).degree

Tactic:
by

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

Goal state before:
pp: K' : Type u_3
inst✝ : Field K'
p : ℕ
hp : 1 < p
⊢ (X ^ p - X).natDegree = p

Tactic:
by

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
H : Subgroup G
F : IntermediateField K L
N : Subgroup G
inst✝³ : N.Normal
inst✝² : IsGaloisGroup (↥N) (↥F) L
E : IntermediateField K L
hE : IsGaloisGroup (↥H) (↥E) L
inst✝¹ : Finite G
inst✝ : IsGaloisGroup G K L
h : E ≤ F
this✝³ : Algebra ↥E ↥F := (IntermediateField.inclusion h).toAlgebra
this✝² : SMul G ↥F := smulOfNormal G (↥F) L N
this✝¹ : SMulDistribClass G (↥F) L
this✝ : MulSemiringAction G ↥F := mulSemiringActionOfSmulDistribClass (↥F) L G
this : IsScalarTower (↥E) (↥F) L
⊢ ∀ (m : ↥(Subgroup.map (QuotientGroup.mk' N) H)) (n : ↥E) (a : ↥F), m • n • a = n • m • a

Tactic:
by

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 ^ q - X).roots.toFinset = univ

Tactic:
by

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
H : Subgroup G
F : IntermediateField K L
N : Subgroup G
inst✝³ : N.Normal
inst✝² : IsGaloisGroup (↥N) (↥F) L
E : IntermediateField K L
hE : IsGaloisGroup (↥H) (↥E) L
inst✝¹ : Finite G
inst✝ : IsGaloisGroup G K L
h✝ : E ≤ F
this✝³ : Algebra ↥E ↥F := (IntermediateField.inclusion h✝).toAlgebra
this✝² : SMul G ↥F := smulOfNormal G (↥F) L N
this✝¹ : SMulDistribClass G (↥F) L
this✝ : MulSemiringAction G ↥F := mulSemiringActionOfSmulDistribClass (↥F) L G
this : IsScalarTower (↥E) (↥F) L
x : ↥F
h : ∀ (g : ↥(Subgroup.map (QuotientGroup.mk' N) H)), g • x = x
⊢ ∀ (g : ↥H), g • (algebraMap (↥F) L) x = (algebraMap (↥F) L) x

Tactic:
by

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
H : Subgroup G
F : IntermediateField K L
N : Subgroup G
inst✝³ : N.Normal
inst✝² : IsGaloisGroup (↥N) (↥F) L
E : IntermediateField K L
hE : IsGaloisGroup (↥H) (↥E) L
inst✝¹ : Finite G
inst✝ : IsGaloisGroup G K L
h✝ : E ≤ F
this✝³ : Algebra ↥E ↥F := (IntermediateField.inclusion h✝).toAlgebra
this✝² : SMul G ↥F := smulOfNormal G (↥F) L N
this✝¹ : SMulDistribClass G (↥F) L
this✝ : MulSemiringAction G ↥F := mulSemiringActionOfSmulDistribClass (↥F) L G
this : IsScalarTower (↥E) (↥F) L
x : ↥F
h : ∀ (g : ↥(Subgroup.map (QuotientGroup.mk' N) H)), g • x = x
a : ↥E
ha : (algebraMap (↥E) L) a = (algebraMap (↥F) L) x
⊢ (algebraMap (↥F) L) ((algebraMap ↥E ↥F) a) = (algebraMap (↥F) L) x

Tactic:
by

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
H : Subgroup G
F : IntermediateField K L
N : Subgroup G
inst✝³ : N.Normal
inst✝² : IsGaloisGroup (↥N) (↥F) L
E : IntermediateField K L
hE : IsGaloisGroup (↥H) (↥E) L
inst✝¹ : Finite G
inst✝ : IsGaloisGroup G K L
h✝ : E ≤ F
this✝³ : Algebra ↥E ↥F := (IntermediateField.inclusion h✝).toAlgebra
this✝² : SMul G ↥F := smulOfNormal G (↥F) L N
this✝¹ : SMulDistribClass G (↥F) L
this✝ : MulSemiringAction G ↥F := mulSemiringActionOfSmulDistribClass (↥F) L G
this : IsScalarTower (↥E) (↥F) L
x : ↥F
h : ∀ (g : ↥(Subgroup.map (QuotientGroup.mk' N) H)), g • x = x
⊢ ∃ a, (algebraMap ↥E ↥F) a = x

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
⊢ (X ^ q - X).roots = univ.val

Tactic:
by

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

Goal state before:
pp: 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)
b : B ⧸ Q
hx : ∀ (g : ↥(MulAction.stabilizer G Q)), ((Ideal.Quotient.stabilizerHom Q P G) g) b = b
⊢ f ((algebraMap (B ⧸ Q) L) b) = (algebraMap (B ⧸ Q) L) b

Tactic:
by

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

Goal state before:
pp: 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✝¹² : MulSemiringAction G B
inst✝¹¹ : SMulCommClass G A B
P : Ideal A
Q : Ideal B
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✝¹ : IsFractionRing (A ⧸ P) K
inst✝ : IsFractionRing (B ⧸ Q) L
σ : ↥(MulAction.stabilizer G Q)
x : B
⊢ ((stabilizerHom G P Q K L) σ) ((algebraMap (B ⧸ Q) L) ((Ideal.Quotient.mk Q) x)) =
    (algebraMap (B ⧸ Q) L) ((Ideal.Quotient.mk Q) (↑σ • x))

Tactic:
by

Goal state after: