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

Goal state before:
pp: case refine_2
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
hGKL : IsGaloisGroup G K L
hHFL : IsGaloisGroup (↥H) (↥F) L
x : L
hx : x ∈ F
⊢ x ∈ FixedPoints.intermediateField ↥H

Tactic:
·

Goal state after:
case refine_2
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
hGKL : IsGaloisGroup G K L
hHFL : IsGaloisGroup (↥H) (↥F) L
x : L
hx : x ∈ F
⊢ x ∈ FixedPoints.intermediateField ↥H
Module: Mathlib.FieldTheory.Finite.Basic

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

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

Tactic:
·

Goal state after:
case pos
K : Type u_1
inst✝³ : Ring K
inst✝² : NoZeroDivisors K
G : Subgroup Kˣ
inst✝¹ : Fintype ↥G
inst✝ : Decidable (G = ⊥)
G_bot : G = ⊥
⊢ ∑ x, ↑↑x = if G = ⊥ then 1 else 0
Module: Mathlib.RingTheory.Trace.Basic

Goal state before:
pp: case refine_2
K : Type u_4
L : Type u_5
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
pb : PowerBasis K L
inst✝ : Algebra.IsSeparable K L
this : FiniteDimensional K L
e : Fin pb.dim ≃ (L →ₐ[K] AlgebraicClosure L) := (Fintype.equivFinOfCardEq ?refine_1).symm
⊢ (algebraMap K (AlgebraicClosure L)) (traceMatrix K ⇑pb.basis).det ≠ 0

pp: case refine_1
K : Type u_4
L : Type u_5
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
pb : PowerBasis K L
inst✝ : Algebra.IsSeparable K L
this : FiniteDimensional K L
⊢ Fintype.card (L →ₐ[K] AlgebraicClosure L) = pb.dim

Tactic:
·

Goal state after:
case refine_2
K : Type u_4
L : Type u_5
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
pb : PowerBasis K L
inst✝ : Algebra.IsSeparable K L
this : FiniteDimensional K L
e : Fin pb.dim ≃ (L →ₐ[K] AlgebraicClosure L) := (Fintype.equivFinOfCardEq ?refine_1).symm
⊢ (algebraMap K (AlgebraicClosure L)) (traceMatrix K ⇑pb.basis).det ≠ 0
Module: Mathlib.FieldTheory.Finite.Basic

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

Tactic:
·

Goal state after:
case neg
K : Type u_1
inst✝³ : Ring K
inst✝² : NoZeroDivisors K
G : Subgroup Kˣ
inst✝¹ : Fintype ↥G
inst✝ : Decidable (G = ⊥)
G_bot : ¬G = ⊥
⊢ ∑ x, ↑↑x = if G = ⊥ then 1 else 0
Module: Mathlib.RingTheory.Trace.Basic

Goal state before:
pp: case refine_1
K : Type u_4
L : Type u_5
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
pb : PowerBasis K L
inst✝ : Algebra.IsSeparable K L
this : FiniteDimensional K L
⊢ Fintype.card (L →ₐ[K] AlgebraicClosure L) = pb.dim

Tactic:
·

Goal state after:
case refine_1
K : Type u_4
L : Type u_5
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
pb : PowerBasis K L
inst✝ : Algebra.IsSeparable K L
this : FiniteDimensional K L
⊢ Fintype.card (L →ₐ[K] AlgebraicClosure L) = pb.dim
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: K : Type u_1
inst✝² : CommRing K
inst✝¹ : NoZeroDivisors K
G : Subgroup Kˣ
inst✝ : Fintype ↥G
k : ℕ
k_pos : k ≠ 0
k_lt_card_G : k < Nat.card ↥G
a✝ : Nontrivial K
this : IsDomain K
a : ↥G
ha : a ^ k ≠ 1
⊢ Multiset.map (fun x ↦ ↑↑x ^ k) univ.val = Multiset.map (fun x ↦ (↑↑x * ↑↑a) ^ k) univ.val

Tactic:
have as_comp :
      (fun x : ↥G => (((x : Kˣ) : K) * ((a : Kˣ) : K)) ^ k)
        = (fun x : ↥G => ((x : Kˣ) : K) ^ k) ∘ fun x : ↥G => x * a := by
      funext x
      simp only [Function.comp_apply, Subgroup.coe_mul, Units.val_mul]

Goal state after:
K : Type u_1
inst✝² : CommRing K
inst✝¹ : NoZeroDivisors K
G : Subgroup Kˣ
inst✝ : Fintype ↥G
k : ℕ
k_pos : k ≠ 0
k_lt_card_G : k < Nat.card ↥G
a✝ : Nontrivial K
this : IsDomain K
a : ↥G
ha : a ^ k ≠ 1
as_comp : (fun x ↦ (↑↑x * ↑↑a) ^ k) = (fun x ↦ ↑↑x ^ k) ∘ fun x ↦ x * a
⊢ Multiset.map (fun x ↦ ↑↑x ^ k) univ.val = Multiset.map (fun x ↦ (↑↑x * ↑↑a) ^ k) univ.val
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
⊢ (∀ (y : C), (∃ y_1, (algebraMap B C) y_1 = y) → g • y = y) →
    ∀ (y : L), (∃ y_1, (algebraMap (FractionRing B) L) y_1 = y) → g • y = y

pp: case refine_2
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
⊢ (∀ (y : L), (∃ y_1, (algebraMap (FractionRing B) L) y_1 = y) → g • y = y) →
    ∀ (y : C), (∃ y_1, (algebraMap B C) y_1 = y) → g • y = y

Tactic:
·

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
⊢ (∀ (y : C), (∃ y_1, (algebraMap B C) y_1 = y) → g • y = y) →
    ∀ (y : L), (∃ y_1, (algebraMap (FractionRing B) L) y_1 = y) → g • y = y
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
ι : Type w
inst✝² : Algebra.IsSeparable K L
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Basis ι K L
this : FiniteDimensional K L
pb : PowerBasis K L := Field.powerBasisOfFiniteOfSeparable K L
⊢ b.toMatrix ⇑pb.basis * pb.basis.toMatrix ⇑b = 1

pp: K : Type u_4
L : Type u_5
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
ι : Type w
inst✝² : Algebra.IsSeparable K L
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Basis ι K L
this : FiniteDimensional K L
pb : PowerBasis K L := Field.powerBasisOfFiniteOfSeparable K L
⊢ (pb.basis.toMatrix ⇑b * (pb.basis.toMatrix ⇑b)ᵀ).det * ((LinearMap.BilinForm.toMatrix pb.basis) (traceForm K L)).det ≠
    0

Tactic:
·

Goal state after:
K : Type u_4
L : Type u_5
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
ι : Type w
inst✝² : Algebra.IsSeparable K L
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Basis ι K L
this : FiniteDimensional K L
pb : PowerBasis K L := Field.powerBasisOfFiniteOfSeparable K L
⊢ b.toMatrix ⇑pb.basis * pb.basis.toMatrix ⇑b = 1
Module: Mathlib.RingTheory.Trace.Basic

Goal state before:
pp: case refine_1
K : Type u_4
L : Type u_5
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
ι : Type w
inst✝² : Algebra.IsSeparable K L
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Basis ι K L
this : FiniteDimensional K L
pb : PowerBasis K L := Field.powerBasisOfFiniteOfSeparable K L
⊢ (pb.basis.toMatrix ⇑b * (pb.basis.toMatrix ⇑b)ᵀ).det * ((b.toMatrix ⇑pb.basis)ᵀ * b.toMatrix ⇑pb.basis).det = 1

pp: case refine_2
K : Type u_4
L : Type u_5
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
ι : Type w
inst✝² : Algebra.IsSeparable K L
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Basis ι K L
this : FiniteDimensional K L
pb : PowerBasis K L := Field.powerBasisOfFiniteOfSeparable K L
⊢ ((LinearMap.BilinForm.toMatrix pb.basis) (traceForm K L)).det ≠ 0

Tactic:
·

Goal state after:
case refine_1
K : Type u_4
L : Type u_5
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
ι : Type w
inst✝² : Algebra.IsSeparable K L
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Basis ι K L
this : FiniteDimensional K L
pb : PowerBasis K L := Field.powerBasisOfFiniteOfSeparable K L
⊢ (pb.basis.toMatrix ⇑b * (pb.basis.toMatrix ⇑b)ᵀ).det * ((b.toMatrix ⇑pb.basis)ᵀ * b.toMatrix ⇑pb.basis).det = 1
Module: Mathlib.FieldTheory.Galois.IsGaloisGroup

Goal state before:
pp: case refine_2
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
⊢ (∀ (y : L), (∃ y_1, (algebraMap (FractionRing B) L) y_1 = y) → g • y = y) →
    ∀ (y : C), (∃ y_1, (algebraMap B C) y_1 = y) → g • y = y

Tactic:
·

Goal state after:
case refine_2
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
⊢ (∀ (y : L), (∃ y_1, (algebraMap (FractionRing B) L) y_1 = y) → g • y = y) →
    ∀ (y : C), (∃ y_1, (algebraMap B C) y_1 = y) → g • y = y
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
tfae_1_to_3 : Algebra.IsSeparable K L → (traceForm K L).Nondegenerate
tfae_3_to_2 : (traceForm K L).Nondegenerate → Algebra.trace K L ≠ 0
tfae_2_to_1 : Algebra.trace K L ≠ 0 → Algebra.IsSeparable K L
⊢ [Algebra.IsSeparable K L, Algebra.trace K L ≠ 0, (traceForm K L).Nondegenerate].TFAE

Tactic:
tfae_finish

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
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
F : IntermediateField K L := (IsScalarTower.toAlgHom K E L).fieldRange
⊢ H.Normal

Tactic:
have : IsGalois K F := .of_algEquiv (IsScalarTower.toAlgHom K E L).equivFieldRange

Goal state after:
G : Type u_1
K : Type u_3
L : Type u_4
inst✝¹¹ : Group G
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : Algebra K L
inst✝⁷ : MulSemiringAction G L
H : Subgroup G
hGKL : IsGaloisGroup G K L
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
F : IntermediateField K L := (IsScalarTower.toAlgHom K E L).fieldRange
this : IsGalois K ↥F
⊢ H.Normal
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 j : Fin pb.dim
this :
  ∑ x, x pb.gen ^ ↑j / x ((aeval pb.gen) (derivative (minpoly K pb.gen))) * x ((minpolyDiv K pb.gen).coeff ↑i) =
    if j = i then 1 else 0
⊢ (algebraMap K (AlgebraicClosure K))
      (((traceForm K L) ((minpolyDiv K pb.gen).coeff ↑i / (aeval pb.gen) (derivative (minpoly K pb.gen))))
        (pb.basis j)) =
    (algebraMap K (AlgebraicClosure K)) (if j = i then 1 else 0)

Tactic:
PowerBasis.coe_basis

Goal state after:
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 j : Fin pb.dim
this :
  ∑ x, x pb.gen ^ ↑j / x ((aeval pb.gen) (derivative (minpoly K pb.gen))) * x ((minpolyDiv K pb.gen).coeff ↑i) =
    if j = i then 1 else 0
⊢ (algebraMap K (AlgebraicClosure K))
      (((traceForm K L) ((minpolyDiv K pb.gen).coeff ↑i / (aeval pb.gen) (derivative (minpoly K pb.gen))))
        ((fun i ↦ pb.gen ^ ↑i) j)) =
    (algebraMap K (AlgebraicClosure K)) (if j = i then 1 else 0)
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
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
h✝ : ¬g • Q = Q
⊢ X - C ((algebraMap B (B ⧸ Q)) 0) = X

Tactic:
·

Goal state after:
case neg
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
h✝ : ¬g • Q = Q
⊢ X - C ((algebraMap B (B ⧸ Q)) 0) = X
Module: Mathlib.FieldTheory.Finite.Basic

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

pp: case neg
K : Type u_1
inst✝¹ : GroupWithZero K
inst✝ : Fintype K
a : K
h : ¬a = 0
⊢ a ^ q = a

Tactic:
·

Goal state after:
case pos
K : Type u_1
inst✝¹ : GroupWithZero K
inst✝ : Fintype K
a : K
h : a = 0
⊢ a ^ q = a
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:
simp [← fixingSubgroup_range_algebraMap G A B C N, mem_fixingSubgroup_iff, ← algebraMap.smul',
        (FaithfulSMul.algebraMap_injective B C).eq_iff]

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

Goal state before:
pp: case mp
K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
i : ℕ
x : Kˣ
hx : ∀ (x_1 : Kˣ), x_1 ∈ Subgroup.zpowers x
⊢ (∀ (x : Kˣ), x ^ i = 1) → x ^ i = 1

pp: case mpr
K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
i : ℕ
x : Kˣ
hx : ∀ (x_1 : Kˣ), x_1 ∈ Subgroup.zpowers x
⊢ x ^ i = 1 → ∀ (x : Kˣ), x ^ i = 1

Tactic:
·

Goal state after:
case mp
K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
i : ℕ
x : Kˣ
hx : ∀ (x_1 : Kˣ), x_1 ∈ Subgroup.zpowers x
⊢ (∀ (x : Kˣ), x ^ i = 1) → x ^ i = 1
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: case mpr
K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
i : ℕ
x : Kˣ
hx : ∀ (x_1 : Kˣ), x_1 ∈ Subgroup.zpowers x
⊢ x ^ i = 1 → ∀ (x : Kˣ), x ^ i = 1

Tactic:
·

Goal state after:
case mpr
K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
i : ℕ
x : Kˣ
hx : ∀ (x_1 : Kˣ), x_1 ∈ Subgroup.zpowers x
⊢ x ^ i = 1 → ∀ (x : Kˣ), x ^ i = 1
Module: Mathlib.Data.Int.Associated

Goal state before:
pp: case mp
a b : ℤ
⊢ a = b ∨ a = -b → Associated a b

pp: case mpr
a b : ℤ
⊢ Associated a b → a = b ∨ a = -b

Tactic:
·

Goal state after:
case mp
a b : ℤ
⊢ a = b ∨ a = -b → Associated a b
Module: Mathlib.Data.Int.Associated

Goal state before:
pp: case mp.inl
a : ℤ
⊢ Associated a a

pp: case mp.inr
b : ℤ
⊢ Associated (-b) b

Tactic:
·

Goal state after:
case mp.inl
a : ℤ
⊢ Associated a a
Module: Mathlib.Data.Int.Associated

Goal state before:
pp: case mp.inr
b : ℤ
⊢ Associated (-b) b

Tactic:
·

Goal state after:
case mp.inr
b : ℤ
⊢ Associated (-b) b
Module: Mathlib.Data.Int.Associated

Goal state before:
pp: case mpr
a b : ℤ
⊢ Associated a b → a = b ∨ a = -b

Tactic:
·

Goal state after:
case mpr
a b : ℤ
⊢ Associated a b → a = b ∨ a = -b
Module: Mathlib.Data.Int.Associated

Goal state before:
pp: case mpr.inl
a : ℤ
⊢ a = a * ↑1 ∨ a = -(a * ↑1)

pp: case mpr.inr
a : ℤ
⊢ a = a * ↑(-1) ∨ a = -(a * ↑(-1))

Tactic:
·

Goal state after:
case mpr.inl
a : ℤ
⊢ a = a * ↑1 ∨ a = -(a * ↑1)
Module: Mathlib.Data.Int.Associated

Goal state before:
pp: case mpr.inr
a : ℤ
⊢ a = a * ↑(-1) ∨ a = -(a * ↑(-1))

Tactic:
·

Goal state after:
case mpr.inr
a : ℤ
⊢ a = a * ↑(-1) ∨ a = -(a * ↑(-1))
Module: Mathlib.RingTheory.Int.Basic

Goal state before:
pp: case h.inl
a b c : ℤ
h : a.gcd b = 1
heq : a * b = c ^ 2
h' : IsUnit (GCDMonoid.gcd a b)
d : ℤ
u : ℤˣ
hu : d ^ 2 * ↑u = a
hu' : u = 1
⊢ d ^ 2 * ↑u = d ^ 2 ∨ d ^ 2 * ↑u = -d ^ 2

Tactic:
·

Goal state after:
case h.inl
a b c : ℤ
h : a.gcd b = 1
heq : a * b = c ^ 2
h' : IsUnit (GCDMonoid.gcd a b)
d : ℤ
u : ℤˣ
hu : d ^ 2 * ↑u = a
hu' : u = 1
⊢ d ^ 2 * ↑u = d ^ 2 ∨ d ^ 2 * ↑u = -d ^ 2
Module: Mathlib.RingTheory.Int.Basic

Goal state before:
pp: case h.inr
a b c : ℤ
h : a.gcd b = 1
heq : a * b = c ^ 2
h' : IsUnit (GCDMonoid.gcd a b)
d : ℤ
u : ℤˣ
hu : d ^ 2 * ↑u = a
hu' : u = -1
⊢ d ^ 2 * ↑u = d ^ 2 ∨ d ^ 2 * ↑u = -d ^ 2

Tactic:
·

Goal state after:
case h.inr
a b c : ℤ
h : a.gcd b = 1
heq : a * b = c ^ 2
h' : IsUnit (GCDMonoid.gcd a b)
d : ℤ
u : ℤˣ
hu : d ^ 2 * ↑u = a
hu' : u = -1
⊢ d ^ 2 * ↑u = d ^ 2 ∨ d ^ 2 * ↑u = -d ^ 2
Module: Mathlib.FieldTheory.Finite.Basic

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

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

Goal state after:
case neg
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
⊢ ↑0 = 0
Module: Mathlib.RingTheory.Int.Basic

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

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

Tactic:
·

Goal state after:
case a
a b : ℤ
⊢ ↑(EuclideanDomain.gcd a b).natAbs ∣ ↑(a.gcd b)
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:
·

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
⊢ ↑(Fintype.card Kˣ) = -1
Module: Mathlib.RingTheory.Int.Basic

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

Tactic:
·

Goal state after:
case a
a b : ℤ
⊢ ↑(a.gcd b) ∣ ↑(EuclideanDomain.gcd a b).natAbs
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: case pos
K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
i : ℕ
h : i < q - 1
hi : i = 0
⊢ ∑ x, x ^ i = 0

pp: case neg
K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
i : ℕ
h : i < q - 1
hi : ¬i = 0
⊢ ∑ x, x ^ i = 0

Tactic:
·

Goal state after:
case pos
K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
i : ℕ
h : i < q - 1
hi : i = 0
⊢ ∑ x, x ^ i = 0
Module: Mathlib.RingTheory.Int.Basic

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

pp: case inr
m : ℤ
p : ℕ
hp : Nat.Prime p
h : ↑p ∣ 2 * m ^ 2
hpp : p ∣ (m ^ 2).natAbs
⊢ p = 2 ∨ p ∣ m.natAbs

Tactic:
·

Goal state after:
case inl
m : ℤ
p : ℕ
hp : Nat.Prime p
h : ↑p ∣ 2 * m ^ 2
hp2 : p ∣ Int.natAbs 2
⊢ p = 2 ∨ p ∣ m.natAbs
Module: Mathlib.RingTheory.Int.Basic

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

Tactic:
·

Goal state after:
case inr
m : ℤ
p : ℕ
hp : Nat.Prime p
h : ↑p ∣ 2 * m ^ 2
hpp : p ∣ (m ^ 2).natAbs
⊢ p = 2 ∨ p ∣ m.natAbs
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: case refine_1
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
x : L
⊢ (frobeniusAlgHom K L ^ Module.finrank K L) x = 1 x

pp: case refine_2
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
⊢ False

Tactic:
·

Goal state after:
case refine_1
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
x : L
⊢ (frobeniusAlgHom K L ^ Module.finrank K L) x = 1 x
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: case inl
hp : Fact (Nat.Prime 2)
x : ZMod 2
⊢ ∃ a b, a ^ 2 + b ^ 2 = x

pp: case inr
p : ℕ
hp : Fact (Nat.Prime p)
x : ZMod p
hp_odd : p % 2 = 1
⊢ ∃ a b, a ^ 2 + b ^ 2 = x

Tactic:
·

Goal state after:
case inl
hp : Fact (Nat.Prime 2)
x : ZMod 2
⊢ ∃ a b, a ^ 2 + b ^ 2 = x