mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Invariant.Basic

Goal state before:
pp: case refine_2
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
h : G
⊢ (a - eval b r - h⁻¹ • if h • Q = Q then a else 0) ∈ h⁻¹ • Q

Tactic:
]

Goal state after:
case refine_2
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
h : G
⊢ (a - eval b r - h⁻¹ • if h • Q = Q then a else 0) ∈ h⁻¹ • Q
Module: Mathlib.RingTheory.Trace.Basic

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

Tactic:
]

Goal state after:
case neg.succ.hnc
K : Type u_4
L : Type u_5
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
H : ¬Algebra.IsSeparable K L
p : ℕ
hp : ExpChar K p
this✝ : p ≠ 0
x : L
h₀ : FiniteDimensional K L
hx : ¬IsSeparable K x
g : K[X]
hg₁ : g.Separable
n : ℕ
hg₂ : (expand K (p ^ (n + 1))) g = minpoly K x
h : p ^ (n + 1) ∣ g.natDegree * p ^ (n + 1) - 1
this : p ^ (n + 1) ∣ g.natDegree * p ^ (n + 1) - (g.natDegree * p ^ (n + 1) - 1)
⊢ g.natDegree * p ^ (n + 1) ≠ 0
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))
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
h : G
hh : h⁻¹ • Q = Q
⊢ eval b r ∈ Q

Tactic:
]

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))
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
h : G
hh : h⁻¹ • Q = Q
⊢ eval b r ∈ Q
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
H : ¬Algebra.IsSeparable K L
p : ℕ
hp : ExpChar K p
this✝¹ : p ≠ 0
x : L
h₀ : FiniteDimensional K L
hx : ¬IsSeparable K x
g : K[X]
hg₁ : g.Separable
n : ℕ
hg₂ : (expand K (p ^ (n + 1))) g = minpoly K x
h : p ^ (n + 1) ∣ g.natDegree * p ^ (n + 1) - 1
this✝ : p ^ (n + 1) ∣ g.natDegree * p ^ (n + 1) - (g.natDegree * p ^ (n + 1) - 1)
e : g.natDegree = 0
this : 0 = (minpoly K x).natDegree
⊢ False

Tactic:
]

Goal state after:
K : Type u_4
L : Type u_5
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
H : ¬Algebra.IsSeparable K L
p : ℕ
hp : ExpChar K p
this✝¹ : p ≠ 0
x : L
h₀ : FiniteDimensional K L
hx : ¬IsSeparable K x
g : K[X]
hg₁ : g.Separable
n : ℕ
hg₂ : (expand K (p ^ (n + 1))) g = minpoly K x
h : p ^ (n + 1) ∣ g.natDegree * p ^ (n + 1) - 1
this✝ : p ^ (n + 1) ∣ g.natDegree * p ^ (n + 1) - (g.natDegree * p ^ (n + 1) - 1)
e : g.natDegree = 0
this : 0 = (minpoly K x).natDegree
⊢ False
Module: Mathlib.RingTheory.Invariant.Basic

Goal state before:
pp: case neg
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
h : G
hh : ¬h⁻¹ • Q = Q
⊢ a - eval b r ∈ h⁻¹ • Q

Tactic:
]

Goal state after:
case neg
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
h : G
hh : ¬h⁻¹ • Q = Q
⊢ a - eval b r ∈ h⁻¹ • Q
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Fintype R
f g : R[X]
hf2 : f.degree = 2
hg2 : g.degree = 2
hR : Fintype.card R % 2 = 1
this : DecidableEq R := Classical.decEq R
hd : Disjoint (image (fun x ↦ eval x f) univ) (image (fun x ↦ eval x (-g)) univ)
⊢ 0 < 2

Tactic:
]

Goal state after:
R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Fintype R
f g : R[X]
hf2 : f.degree = 2
hg2 : g.degree = 2
hR : Fintype.card R % 2 = 1
this : DecidableEq R := Classical.decEq R
hd : Disjoint (image (fun x ↦ eval x f) univ) (image (fun x ↦ eval x (-g)) univ)
⊢ 0 < 2
Module: Mathlib.RingTheory.Trace.Basic

Goal state before:
pp: κ : Type w
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : Fintype κ
b : κ → B
P : Matrix κ κ A
α β : κ
⊢ ∑ y, ∑ x, ((traceForm A B) (b x * P.map (⇑(algebraMap A B)) x α)) (b y * P.map (⇑(algebraMap A B)) y β) =
    ∑ j, (Pᵀ * traceMatrix A b) α j * P j β

Tactic:
]

Goal state after:
κ : Type w
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : Fintype κ
b : κ → B
P : Matrix κ κ A
α β : κ
⊢ ∑ y, ∑ x, ((traceForm A B) (b x * P.map (⇑(algebraMap A B)) x α)) (b y * P.map (⇑(algebraMap A B)) y β) =
    ∑ j, (Pᵀ * traceMatrix A b) α j * P j β
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
b₀ : B
hx : ∀ (g : G), g • Q = Q → (algebraMap B (B ⧸ Q)) (g • b₀) = (algebraMap B (B ⧸ 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 else 0)
g : G
⊢ (algebraMap B (B ⧸ Q)) (if g • Q = Q then a else 0) * (algebraMap B (B ⧸ Q)) (g • b₀) =
    (algebraMap B (B ⧸ Q)) (if g • Q = Q then a * b₀ else 0)

Tactic:
]

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
b₀ : B
hx : ∀ (g : G), g • Q = Q → (algebraMap B (B ⧸ Q)) (g • b₀) = (algebraMap B (B ⧸ 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 else 0)
g : G
⊢ (algebraMap B (B ⧸ Q)) (if g • Q = Q then a else 0) * (algebraMap B (B ⧸ Q)) (g • b₀) =
    (algebraMap B (B ⧸ Q)) (if g • Q = Q then a * b₀ else 0)
Module: Mathlib.RingTheory.Trace.Basic

Goal state before:
pp: case e_f
κ : Type w
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : Fintype κ
b : κ → B
P : Matrix κ κ A
α β x : κ
⊢ ∑ x_1, ((traceForm A B) (b x_1 * P.map (⇑(algebraMap A B)) x_1 α)) (b x * P.map (⇑(algebraMap A B)) x β) =
    ∑ i, Pᵀ α i * traceMatrix A b i x * P x β

Tactic:
]

Goal state after:
case e_f
κ : Type w
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : Fintype κ
b : κ → B
P : Matrix κ κ A
α β x : κ
⊢ ∑ x_1, ((traceForm A B) (b x_1 * P.map (⇑(algebraMap A B)) x_1 α)) (b x * P.map (⇑(algebraMap A B)) x β) =
    ∑ i, Pᵀ α i * traceMatrix A b i x * P x β
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Fintype R
f g : R[X]
hf2 : f.degree = 2
hg2 : g.degree = 2
hR : Fintype.card R % 2 = 1
this : DecidableEq R := Classical.decEq R
hd : Disjoint (image (fun x ↦ eval x f) univ) (image (fun x ↦ eval x (-g)) univ)
⊢ f.natDegree * #(image (fun x ↦ eval x f) univ) + (-g).natDegree * #(image (fun x ↦ eval x (-g)) univ) =
    2 * (#(image (fun x ↦ eval x f) univ) + #(image (fun x ↦ eval x (-g)) univ))

Tactic:
]

Goal state after:
R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Fintype R
f g : R[X]
hf2 : f.degree = 2
hg2 : g.degree = 2
hR : Fintype.card R % 2 = 1
this : DecidableEq R := Classical.decEq R
hd : Disjoint (image (fun x ↦ eval x f) univ) (image (fun x ↦ eval x (-g)) univ)
⊢ f.natDegree * #(image (fun x ↦ eval x f) univ) + (-g).natDegree * #(image (fun x ↦ eval x (-g)) univ) =
    2 * (#(image (fun x ↦ eval x f) univ) + #(image (fun x ↦ eval x (-g)) univ))
Module: Mathlib.RingTheory.Trace.Basic

Goal state before:
pp: case e_f.e_f
κ : Type w
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : Fintype κ
b : κ → B
P : Matrix κ κ A
α β x y : κ
⊢ (trace A B) (P y α • b y * (b x * P.map (⇑(algebraMap A B)) x β)) = Pᵀ α y * traceMatrix A b y x * P x β

Tactic:
]

Goal state after:
case e_f.e_f
κ : Type w
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : Fintype κ
b : κ → B
P : Matrix κ κ A
α β x y : κ
⊢ (trace A B) (P y α • b y * (b x * P.map (⇑(algebraMap A B)) x β)) = Pᵀ α y * traceMatrix A b y x * P x β
Module: Mathlib.FieldTheory.Galois.IsGaloisGroup

Goal state before:
pp: G : Type u_1
K : Type u_3
L : Type u_4
inst✝⁵ : Group G
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : MulSemiringAction G L
inst✝ : IsGaloisGroup G K L
⊢ FixedPoints.intermediateField G ≤ ⊥

Tactic:
]

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
inst✝ : IsGaloisGroup G K L
⊢ FixedPoints.intermediateField G ≤ ⊥
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
b₀ : B
hx : ∀ (g : G), g • Q = Q → (algebraMap B (B ⧸ Q)) (g • b₀) = (algebraMap B (B ⧸ Q)) b₀
a b : B
ha1 : ∀ (g : G), g • a = a
ha2 : a ∉ Q
g : G
hb : (algebraMap B (B ⧸ Q)) (g • b) = (algebraMap B (B ⧸ Q)) (if g • Q = Q then a else 0)
hg : g • Q = Q
⊢ (algebraMap B (B ⧸ Q)) a * (algebraMap B (B ⧸ Q)) b₀ = (algebraMap B (B ⧸ Q)) a * (algebraMap B (B ⧸ Q)) b₀

Tactic:
]

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

Goal state before:
pp: case e_f.e_f
κ : Type w
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : Fintype κ
b : κ → B
P : Matrix κ κ A
α β x y : κ
⊢ P y α * (trace A B) (b y * P x β • b x) = P y α * traceMatrix A b y x * P x β

Tactic:
]

Goal state after:
case e_f.e_f
κ : Type w
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : Fintype κ
b : κ → B
P : Matrix κ κ A
α β x y : κ
⊢ P y α * (trace A B) (b y * P x β • b x) = P y α * traceMatrix A b y x * P x β
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:
]

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

Goal state before:
pp: case e_f.e_f
κ : Type w
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : Fintype κ
b : κ → B
P : Matrix κ κ A
α β x y : κ
⊢ P y α * (trace A B) (b y * P x β • b x) = P y α * (P x β * traceMatrix A b y x)

Tactic:
]

Goal state after:
case e_f.e_f
κ : Type w
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : Fintype κ
b : κ → B
P : Matrix κ κ A
α β x y : κ
⊢ P y α * (trace A B) (b y * P x β • b x) = P y α * (P x β * traceMatrix A b y x)
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Fintype R
f g : R[X]
hf2 : f.degree = 2
hg2 : g.degree = 2
hR : Fintype.card R % 2 = 1
this : DecidableEq R := Classical.decEq R
x a : R
left✝¹ : a ∈ univ
ha : eval a f = x
b : R
left✝ : b ∈ univ
hb : eval b (-g) = x
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: case inl
G : Type u_1
K : Type u_3
L : Type u_4
inst✝⁵ : Group G
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : MulSemiringAction G L
inst✝ : IsGaloisGroup G K L
val✝ : Fintype G
this : FaithfulSMul G L
⊢ Fintype.card G = finrank (↥(FixedPoints.intermediateField G)) L

Tactic:
]

Goal state after:
case inl
G : Type u_1
K : Type u_3
L : Type u_4
inst✝⁵ : Group G
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : MulSemiringAction G L
inst✝ : IsGaloisGroup G K L
val✝ : Fintype G
this : FaithfulSMul G L
⊢ Fintype.card G = finrank (↥(FixedPoints.intermediateField G)) L
Module: Mathlib.RingTheory.Invariant.Basic

Goal state before:
pp: case neg
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
b₀ : B
hx : ∀ (g : G), g • Q = Q → (algebraMap B (B ⧸ Q)) (g • b₀) = (algebraMap B (B ⧸ Q)) b₀
a b : B
ha1 : ∀ (g : G), g • a = a
ha2 : a ∉ Q
g : G
hb : (algebraMap B (B ⧸ Q)) (g • b) = (algebraMap B (B ⧸ Q)) (if g • Q = Q then a else 0)
hg : ¬g • Q = Q
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: case inr
G : Type u_1
K : Type u_3
L : Type u_4
inst✝⁵ : Group G
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : MulSemiringAction G L
inst✝ : IsGaloisGroup G K L
hG : Infinite G
⊢ finrank K L = 0

Tactic:
]

Goal state after:
case inr
G : Type u_1
K : Type u_3
L : Type u_4
inst✝⁵ : Group G
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : MulSemiringAction G L
inst✝ : IsGaloisGroup G K L
hG : Infinite G
⊢ finrank K L = 0
Module: Mathlib.RingTheory.Trace.Basic

Goal state before:
pp: κ : Type w
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : Fintype κ
b : κ → B
P : Matrix κ κ A
⊢ (P * traceMatrix A b * Pᵀ)ᵀ = (P * traceMatrix A b * Pᵀ)ᵀ

Tactic:
]

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

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

Tactic:
]

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

Goal state before:
pp: case pos
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
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: κ : Type w
A : Type u
B : Type v
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra A B
inst✝¹ : Fintype κ
inst✝ : DecidableEq κ
b : Basis κ A B
i j : κ
⊢ (trace A B) (b i * b j) = (trace A B) (b i * b j)

Tactic:
]

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
A : Subring B := (algebraMap R B).range
this✝⁴ : Algebra (FractionRing ↥A) (FractionRing B) := FractionRing.liftAlgebra (↥A) (FractionRing B)
this✝³ : MulSemiringAction G (FractionRing B) := IsFractionRing.mulSemiringAction G B (FractionRing B)
this✝² : Algebra R ↥A := (algebraMap R B).rangeRestrict.toAlgebra
this✝¹ : IsScalarTower R (↥A) B
this✝ : Module.Finite (↥A) B
this : IsGaloisGroup G (FractionRing ↥A) (FractionRing B)
⊢ finrank (FractionRing ↥A) (FractionRing B) ≠ 0

Tactic:
]

Goal state after:
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
A : Subring B := (algebraMap R B).range
this✝⁴ : Algebra (FractionRing ↥A) (FractionRing B) := FractionRing.liftAlgebra (↥A) (FractionRing B)
this✝³ : MulSemiringAction G (FractionRing B) := IsFractionRing.mulSemiringAction G B (FractionRing B)
this✝² : Algebra R ↥A := (algebraMap R B).rangeRestrict.toAlgebra
this✝¹ : IsScalarTower R (↥A) B
this✝ : Module.Finite (↥A) B
this : IsGaloisGroup G (FractionRing ↥A) (FractionRing B)
⊢ finrank (FractionRing ↥A) (FractionRing B) ≠ 0
Module: Mathlib.RingTheory.Trace.Basic

Goal state before:
pp: ι : Type w
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : Fintype ι
b : Basis ι A B
z : B
i : ι
⊢ ∑ j, of (fun i j ↦ ((traceForm A B) (b i)) (b j)) i j * replicateCol (Fin 1) (b.equivFun z) j 0 =
    (trace A B) (z * b i)

Tactic:
]

Goal state after:
ι : Type w
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : Fintype ι
b : Basis ι A B
z : B
i : ι
⊢ ∑ j, of (fun i j ↦ ((traceForm A B) (b i)) (b j)) i j * replicateCol (Fin 1) (b.equivFun z) j 0 =
    (trace A B) (z * b i)
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:
]

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.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 : eval b ((X - C b) ^ i * X ^ j) = eval b (map (↑↑f) ((X - C b) ^ i * X ^ j))
⊢ f b = b

Tactic:
]

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 : eval b ((X - C b) ^ i * X ^ j) = eval b (map (↑↑f) ((X - C b) ^ i * X ^ j))
⊢ f b = b
Module: Mathlib.FieldTheory.Galois.IsGaloisGroup

Goal state before:
pp: G : Type u_1
inst✝⁸ : Group G
A : Type u_5
B : Type u_6
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : IsDomain B
inst✝⁴ : Algebra A B
inst✝³ : FaithfulSMul A B
inst✝² : MulSemiringAction G B
inst✝¹ : IsGaloisGroup G A B
inst✝ : Finite G
this✝¹ : IsDomain A
this✝ : Algebra (FractionRing A) (FractionRing B) := FractionRing.liftAlgebra A (FractionRing B)
this : MulSemiringAction G (FractionRing B) := IsFractionRing.mulSemiringAction G B (FractionRing B)
⊢ finrank A B = finrank A B

Tactic:
]

Goal state after:
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
hu : orderOf u = p
⊢ u - 1 = 0

Tactic:
]

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
hu : orderOf u = p
⊢ u - 1 = 0
Module: Mathlib.RingTheory.Trace.Basic

Goal state before:
pp: ι : Type w
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : Fintype ι
b : Basis ι A B
z : B
i : ι
⊢ (trace A B) (∑ x, b.equivFun z x • (b i * b x)) = (trace A B) (z * b i)

Tactic:
]

Goal state after:
ι : Type w
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : Fintype ι
b : Basis ι A B
z : B
i : ι
⊢ (trace A B) (∑ x, b.equivFun z x • (b i * b x)) = (trace A B) (z * b i)
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
inst✝¹⁰ : CommRing A
inst✝⁹ : CommRing B
inst✝⁸ : IsDomain B
inst✝⁷ : Algebra A B
inst✝⁶ : FaithfulSMul A B
inst✝⁵ : MulSemiringAction G B
inst✝⁴ : MulSemiringAction G' B
inst✝³ : IsGaloisGroup G A B
inst✝² : IsGaloisGroup G' A B
inst✝¹ : Finite G
inst✝ : Finite G'
g : G'
x : B
⊢ g • x = g • x

Tactic:
]

Goal state after: