mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.NumberField.Basic

Goal state before:
pp: K✝ : Type u_1
L✝ : Type u_2
inst✝³ : Field K✝
inst✝² : Field L✝
K : Type u_3
L : Type u_4
inst✝¹ : Field K
inst✝ : Field L
f : K →+* L
⊢ ↑⟨f ↑0, ⋯⟩ = ↑0

Tactic:
;

Goal state after:
K✝ : Type u_1
L✝ : Type u_2
inst✝³ : Field K✝
inst✝² : Field L✝
K : Type u_3
L : Type u_4
inst✝¹ : Field K
inst✝ : Field L
f : K →+* L
⊢ ↑⟨f ↑0, ⋯⟩ = ↑0
Module: Mathlib.NumberTheory.NumberField.Basic

Goal state before:
pp: K✝ : Type u_1
L✝ : Type u_2
inst✝³ : Field K✝
inst✝² : Field L✝
K : Type u_3
L : Type u_4
inst✝¹ : Field K
inst✝ : Field L
f : K →+* L
x y : 𝓞 K
⊢ ↑⟨f ↑(x + y), ⋯⟩ = ↑(⟨f ↑x, ⋯⟩ + ⟨f ↑y, ⋯⟩)

Tactic:
;

Goal state after:
K✝ : Type u_1
L✝ : Type u_2
inst✝³ : Field K✝
inst✝² : Field L✝
K : Type u_3
L : Type u_4
inst✝¹ : Field K
inst✝ : Field L
f : K →+* L
x y : 𝓞 K
⊢ ↑⟨f ↑(x + y), ⋯⟩ = ↑(⟨f ↑x, ⋯⟩ + ⟨f ↑y, ⋯⟩)
Module: Mathlib.NumberTheory.NumberField.Basic

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

Tactic:
;

Goal state after:
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : NumberField K
M : Type u_3
inst✝ : AddZeroClass M
f : M →+ K
h : ∀ (x : M), IsIntegral ℤ (f x)
⊢ ⟨0, ⋯⟩ = 0
Module: Mathlib.NumberTheory.NumberField.Basic

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

Tactic:
;

Goal state after:
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : NumberField K
M : Type u_3
inst✝ : AddZeroClass M
f : M →+ K
h : ∀ (x : M), IsIntegral ℤ (f x)
x y : M
⊢ ⟨f x + f y, ⋯⟩ = ⟨f x, ⋯⟩ + ⟨f y, ⋯⟩
Module: Mathlib.NumberTheory.NumberField.Basic

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : NumberField K
M : Type u_3
inst✝ : MulOneClass M
f : M →* K
h : ∀ (x : M), IsIntegral ℤ (f x)
⊢ ⟨1, ⋯⟩ = 1

Tactic:
;

Goal state after:
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : NumberField K
M : Type u_3
inst✝ : MulOneClass M
f : M →* K
h : ∀ (x : M), IsIntegral ℤ (f x)
⊢ ⟨1, ⋯⟩ = 1
Module: Mathlib.NumberTheory.NumberField.Basic

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : NumberField K
M : Type u_3
inst✝ : MulOneClass M
f : M →* K
h : ∀ (x : M), IsIntegral ℤ (f x)
x y : M
⊢ ⟨f x * f y, ⋯⟩ = ⟨f x, ⋯⟩ * ⟨f y, ⋯⟩

Tactic:
;

Goal state after:
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : NumberField K
M : Type u_3
inst✝ : MulOneClass M
f : M →* K
h : ∀ (x : M), IsIntegral ℤ (f x)
x y : M
⊢ ⟨f x * f y, ⋯⟩ = ⟨f x, ⋯⟩ * ⟨f y, ⋯⟩
Module: Mathlib.RingTheory.Trace.Basic

Goal state before:
pp: case pos
K : Type u_4
L : Type u_5
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
F : Type u_6
inst✝¹ : Field F
inst✝ : Algebra K F
x : L
hf : (Polynomial.map (algebraMap K F) (minpoly K x)).Splits
injKxL : Function.Injective ⇑(algebraMap (↥K⟮x⟯) L)
hx : IsIntegral K x
⊢ (algebraMap K F) ((Algebra.trace K ↥K⟮x⟯) (gen K x)) = ((minpoly K x).aroots F).sum

pp: case neg
K : Type u_4
L : Type u_5
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
F : Type u_6
inst✝¹ : Field F
inst✝ : Algebra K F
x : L
hf : (Polynomial.map (algebraMap K F) (minpoly K x)).Splits
injKxL : Function.Injective ⇑(algebraMap (↥K⟮x⟯) L)
hx : ¬IsIntegral K x
⊢ (algebraMap K F) ((Algebra.trace K ↥K⟮x⟯) (gen K x)) = ((minpoly K x).aroots F).sum

Tactic:
;

Goal state after:
case pos
K : Type u_4
L : Type u_5
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
F : Type u_6
inst✝¹ : Field F
inst✝ : Algebra K F
x : L
hf : (Polynomial.map (algebraMap K F) (minpoly K x)).Splits
injKxL : Function.Injective ⇑(algebraMap (↥K⟮x⟯) L)
hx : IsIntegral K x
⊢ (algebraMap K F) ((Algebra.trace K ↥K⟮x⟯) (gen K x)) = ((minpoly K x).aroots F).sum

case neg
K : Type u_4
L : Type u_5
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
F : Type u_6
inst✝¹ : Field F
inst✝ : Algebra K F
x : L
hf : (Polynomial.map (algebraMap K F) (minpoly K x)).Splits
injKxL : Function.Injective ⇑(algebraMap (↥K⟮x⟯) L)
hx : ¬IsIntegral K x
⊢ (algebraMap K F) ((Algebra.trace K ↥K⟮x⟯) (gen K x)) = ((minpoly K x).aroots F).sum
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
x : L
⊢ (algebraMap ℕ K) (finrank (↥K⟮x⟯) L) * -(minpoly K x).nextCoeff = ↑(finrank (↥K⟮x⟯) L) * -(minpoly K x).nextCoeff

Tactic:
;

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
x : L
⊢ (algebraMap ℕ K) (finrank (↥K⟮x⟯) L) * -(minpoly K x).nextCoeff = ↑(finrank (↥K⟮x⟯) L) * -(minpoly K x).nextCoeff
Module: Mathlib.RingTheory.Trace.Basic

Goal state before:
pp: case e_6
A : Type u_7
B : Type u_8
C : Type u_9
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing C
inst✝¹ : Algebra A B
inst✝ : Algebra A C
e : B ≃ₐ[A] C
x : B
⊢ (lmul A C) (e x) = (↑e).conj ((lmul A B) x)

Tactic:
;

Goal state after:
case e_6
A : Type u_7
B : Type u_8
C : Type u_9
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing C
inst✝¹ : Algebra A B
inst✝ : Algebra A C
e : B ≃ₐ[A] C
x : B
⊢ (lmul A C) (e x) = (↑e).conj ((lmul A B) x)
Module: Mathlib.RingTheory.Trace.Basic

Goal state before:
pp: case e_6
A : Type u_7
B : Type u_8
C : Type u_9
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing C
inst✝¹ : Algebra A B
inst✝ : Algebra A C
e : B ≃ₐ[A] C
x : B
x✝ : C
⊢ ((lmul A C) (e x)) x✝ = ((↑e).conj ((lmul A B) x)) x✝

Tactic:
;

Goal state after:
case e_6
A : Type u_7
B : Type u_8
C : Type u_9
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing C
inst✝¹ : Algebra A B
inst✝ : Algebra A C
e : B ≃ₐ[A] C
x : B
x✝ : C
⊢ ((lmul A C) (e x)) x✝ = ((↑e).conj ((lmul A B) x)) x✝
Module: Mathlib.Data.ZMod.ValMinAbs

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
x : ZMod n
⊢ (0 ≤ if x.val ≤ n / 2 then ↑x.val else ↑x.val - ↑n) ↔ x.val ≤ n / 2

Tactic:
;

Goal state after:
n : ℕ
inst✝ : NeZero n
x : ZMod n
⊢ (0 ≤ if x.val ≤ n / 2 then ↑x.val else ↑x.val - ↑n) ↔ x.val ≤ n / 2
Module: Mathlib.Data.ZMod.ValMinAbs

Goal state before:
pp: case neg
n : ℕ
inst✝ : NeZero n
x : ZMod n
h : ¬x.val ≤ n / 2
⊢ 0 ≤ ↑x.val - ↑n ↔ x.val ≤ n / 2

Tactic:
· exact iff_of_false (sub_lt_zero.2 <| Int.ofNat_lt.2 x.val_lt).not_ge h

Goal state after:
Module: Mathlib.Data.ZMod.ValMinAbs

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
x : ZMod n
⊢ (if ↑x.val * 2 ≤ ↑n then ↑x.val else ↑x.val - ↑n) * 2 ∈ Set.Ioc (-↑n) ↑n

Tactic:
;

Goal state after:
n : ℕ
inst✝ : NeZero n
x : ZMod n
⊢ (if ↑x.val * 2 ≤ ↑n then ↑x.val else ↑x.val - ↑n) * 2 ∈ Set.Ioc (-↑n) ↑n
Module: Mathlib.Data.ZMod.ValMinAbs

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
x : ZMod n
⊢ x = ↑x.valMinAbs ∧ x.valMinAbs * 2 ∈ Set.Ioc (-↑n) ↑n

Tactic:
;

Goal state after:
n : ℕ
inst✝ : NeZero n
x : ZMod n
⊢ x = ↑x.valMinAbs ∧ x.valMinAbs * 2 ∈ Set.Ioc (-↑n) ↑n
Module: Mathlib.Data.ZMod.ValMinAbs

Goal state before:
pp: n : ℕ
a b : ZMod n
h : a.valMinAbs = -b.valMinAbs
⊢ a = -b

Tactic:
by
  rcases eq_zero_or_neZero n with rfl | hn <;> simp_all [valMinAbs_spec]

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

Goal state before:
pp: A₁ : Type u_7
B₁ : Type u_8
A₂ : Type u_9
B₂ : Type u_10
inst✝⁵ : CommRing A₁
inst✝⁴ : CommRing B₁
inst✝³ : CommRing A₂
inst✝² : CommRing B₂
inst✝¹ : Algebra A₁ B₁
inst✝ : Algebra A₂ B₂
e₁ : A₁ ≃+* A₂
e₂ : B₁ ≃+* B₂
he : (algebraMap A₂ B₂).comp ↑e₁ = (↑e₂).comp (algebraMap A₁ B₁)
x : B₁
this : Algebra A₁ B₂ := ((↑e₂).comp (algebraMap A₁ B₁)).toAlgebra
⊢ (trace A₁ B₁) x = e₁.symm ((trace A₂ B₂) (e₂ x))

Tactic:
let e' : B₁ ≃ₐ[A₁] B₂ := { e₂ with commutes' := fun _ ↦ rfl }

Goal state after:
A₁ : Type u_7
B₁ : Type u_8
A₂ : Type u_9
B₂ : Type u_10
inst✝⁵ : CommRing A₁
inst✝⁴ : CommRing B₁
inst✝³ : CommRing A₂
inst✝² : CommRing B₂
inst✝¹ : Algebra A₁ B₁
inst✝ : Algebra A₂ B₂
e₁ : A₁ ≃+* A₂
e₂ : B₁ ≃+* B₂
he : (algebraMap A₂ B₂).comp ↑e₁ = (↑e₂).comp (algebraMap A₁ B₁)
x : B₁
this : Algebra A₁ B₂ := ((↑e₂).comp (algebraMap A₁ B₁)).toAlgebra
e' : B₁ ≃ₐ[A₁] B₂ := { toEquiv := e₂.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
⊢ (trace A₁ B₁) x = e₁.symm ((trace A₂ B₂) (e₂ x))
Module: Mathlib.RingTheory.Trace.Basic

Goal state before:
pp: case hfg
K : Type u_4
L : Type u_5
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
E : Type u_7
inst✝¹ : Field E
inst✝ : Algebra K E
pb : PowerBasis K L
hE : (Polynomial.map (algebraMap K E) (minpoly K pb.gen)).Splits
hfx : IsSeparable K pb.gen
this✝ : DecidableEq E := Classical.decEq E
this : Fintype (L →ₐ[K] E) := PowerBasis.AlgHom.fintype pb
x : { x // x ∈ (minpoly K pb.gen).aroots E }
⊢ ?f✝ x = _root_.id ↑x

Tactic:
;

Goal state after:
case hfg
K : Type u_4
L : Type u_5
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
E : Type u_7
inst✝¹ : Field E
inst✝ : Algebra K E
pb : PowerBasis K L
hE : (Polynomial.map (algebraMap K E) (minpoly K pb.gen)).Splits
hfx : IsSeparable K pb.gen
this✝ : DecidableEq E := Classical.decEq E
this : Fintype (L →ₐ[K] E) := PowerBasis.AlgHom.fintype pb
x : { x // x ∈ (minpoly K pb.gen).aroots E }
⊢ ?f✝ x = _root_.id ↑x
Module: Mathlib.RingTheory.Trace.Basic

Goal state before:
pp: case pos
K : Type u_4
L : Type u_5
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
H : ¬Algebra.IsSeparable K L
p : ℕ
hp : ExpChar K p
this : p ≠ 0
x : L
h₀ : FiniteDimensional K L
⊢ (trace K L) x = 0 x

pp: case neg
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
⊢ (trace K L) x = 0 x

Tactic:
;

Goal state after:
case pos
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
⊢ (trace K L) x = 0 x

case neg
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
⊢ (trace K L) x = 0 x
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
κ' : Type u_7
b : Basis κ A B
f : κ ≃ κ'
x y : κ'
⊢ traceMatrix A (⇑(b.reindex f)) x y = (reindex f f) (traceMatrix A ⇑b) x y

Tactic:
;

Goal state after:
κ : Type w
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
κ' : Type u_7
b : Basis κ A B
f : κ ≃ κ'
x y : κ'
⊢ traceMatrix A (⇑(b.reindex f)) x y = (reindex f f) (traceMatrix A ⇑b) x y
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: 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
α β : κ
⊢ (fun y ↦ ∑ x, ((traceForm A B) (b x * P.map (⇑(algebraMap A B)) x α)) (b y * P.map (⇑(algebraMap A B)) y β)) = fun j ↦
    (Pᵀ * traceMatrix A b) α j * P j β

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
α β : κ
⊢ (fun y ↦ ∑ x, ((traceForm A B) (b x * P.map (⇑(algebraMap A B)) x α)) (b y * P.map (⇑(algebraMap A B)) y β)) = fun j ↦
    (Pᵀ * traceMatrix A b) α j * P j β
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 : κ
⊢ (fun x_1 ↦ ((traceForm A B) (b x_1 * P.map (⇑(algebraMap A B)) x_1 α)) (b x * P.map (⇑(algebraMap A B)) x β)) =
    fun i ↦ Pᵀ α i * traceMatrix A b i 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 : κ
⊢ (fun x_1 ↦ ((traceForm A B) (b x_1 * P.map (⇑(algebraMap A B)) x_1 α)) (b x * P.map (⇑(algebraMap A B)) x β)) =
    fun i ↦ Pᵀ α i * traceMatrix A b i x * P x β
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
E : Type z
inst✝⁴ : Field E
inst✝³ : Algebra K E
inst✝² : Module.Finite K L
inst✝¹ : Algebra.IsSeparable K L
inst✝ : IsAlgClosed E
b : κ → L
i j : κ
⊢ (traceMatrix K b).map (⇑(algebraMap K E)) i j = (embeddingsMatrix K E b * (embeddingsMatrix K E b)ᵀ) i j

Tactic:
;

Goal state after:
K : Type u_4
L : Type u_5
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Algebra K L
κ : Type w
E : Type z
inst✝⁴ : Field E
inst✝³ : Algebra K E
inst✝² : Module.Finite K L
inst✝¹ : Algebra.IsSeparable K L
inst✝ : IsAlgClosed E
b : κ → L
i j : κ
⊢ (traceMatrix K b).map (⇑(algebraMap K E)) i j = (embeddingsMatrix K E b * (embeddingsMatrix K E b)ᵀ) i j
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
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
⊢ f b = b

Tactic:
by
  by_cases ha : b = 0
  · rw [ha, map_zero]
  have hf := congrArg (eval b) (congrArg (Polynomial.mapAlgHom f.toAlgHom) h)
  rw [coe_mapAlgHom, map_map, f.toAlgHom.comp_algebraMap, h] at hf
  simp_rw [Polynomial.map_mul, Polynomial.map_pow, Polynomial.map_sub, map_X, map_C,
    eval_mul, eval_pow, eval_sub, eval_X, eval_C, sub_self, zero_pow hi, zero_mul,
    zero_eq_mul, or_iff_left (pow_ne_zero j ha), pow_eq_zero_iff hi, sub_eq_zero] at hf
  exact hf.symm

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
hGKL : IsGaloisGroup G K L
this : FaithfulSMul G L
x✝ : G
⊢ x✝ ∈ fixingSubgroup G ↑⊤ ↔ x✝ ∈ ⊥

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
hGKL : IsGaloisGroup G K L
this : FaithfulSMul G L
x✝ : G
⊢ x✝ ∈ fixingSubgroup G ↑⊤ ↔ 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
hGKL : IsGaloisGroup G K L
x✝ : L
⊢ x✝ ∈ FixedPoints.intermediateField ↥⊤ ↔ x✝ ∈ 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
hGKL : IsGaloisGroup G K L
x✝ : L
⊢ x✝ ∈ FixedPoints.intermediateField ↥⊤ ↔ x✝ ∈ FixedPoints.intermediateField G
Module: Mathlib.FieldTheory.Galois.IsGaloisGroup

Goal state before:
pp: G : Type u_1
inst✝¹⁰ : Group G
inst✝⁹ : Finite G
A : Type u_5
B : Type u_6
C : Type u_7
H : Subgroup G
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
inst✝⁶ : CommRing C
inst✝⁵ : IsDomain C
inst✝⁴ : Algebra A C
inst✝³ : FaithfulSMul A C
inst✝² : MulSemiringAction G C
hGAC : IsGaloisGroup G A C
inst✝¹ : Algebra B C
inst✝ : FaithfulSMul B C
hH : IsGaloisGroup (↥H) B C
this✝ : IsDomain B
this : IsDomain A
⊢ fixingSubgroup G (Set.range ⇑(algebraMap B C)) = H

Tactic:
let K := FractionRing A

Goal state after:
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
⊢ fixingSubgroup G (Set.range ⇑(algebraMap B C)) = H
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

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
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
H₁ : (traceForm K L).Nondegenerate
H₂ : Algebra.trace K L = 0
x✝ y✝ : L
⊢ ((traceForm K L) x✝) y✝ = (0 x✝) y✝

Tactic:
;

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
tfae_1_to_3 : Algebra.IsSeparable K L → (traceForm K L).Nondegenerate
H₁ : (traceForm K L).Nondegenerate
H₂ : Algebra.trace K L = 0
x✝ y✝ : L
⊢ ((traceForm K L) x✝) y✝ = (0 x✝) y✝
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

case neg
K : Type u_1
inst✝¹ : GroupWithZero K
inst✝ : Fintype K
a : K
h : ¬a = 0
⊢ a ^ q = a
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
⊢ 0 ^ q = 0

Tactic:
;

Goal state after:
case pos
K : Type u_1
inst✝¹ : GroupWithZero K
inst✝ : Fintype K
a : K
h : a = 0
⊢ 0 ^ q = 0
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
h : ∀ (x : Kˣ), x ^ i = 1
⊢ 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
h : ∀ (x : Kˣ), x ^ i = 1
⊢ x ^ i = 1
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

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

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

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.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
⊢ 1 ≤ q

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
⊢ 1 ≤ q
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 := ⋯
this : Decidable (φ = 1)
⊢ ∀ (a : Kˣ), a ^ i = 1 ↔ φ a = 1 a

Tactic:
;

Goal state after:
K : Type u_1
inst✝² : Field K
inst✝¹ : Fintype K
inst✝ : DecidableEq K
i : ℕ
φ : Kˣ →* K := ⋯
this : Decidable (φ = 1)
⊢ ∀ (a : Kˣ), a ^ i = 1 ↔ φ a = 1 a
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)
x : Kˣ
⊢ x ^ i = 1 ↔ φ x = 1 x

Tactic:
;

Goal state after:
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)
x : Kˣ
⊢ x ^ i = 1 ↔ φ x = 1 x
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
i : ℕ
hi : ¬i = 0
h : q - 1 ∣ i
⊢ q - 1 ≤ i

Tactic:
;

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
i : ℕ
hi : ¬i = 0
h : q - 1 ∣ i
⊢ q - 1 ≤ i
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: case hnc
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}
⊢ ¬q - 1 ∣ i

Tactic:
;

Goal state after:
case hnc
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}
⊢ ¬q - 1 ∣ i
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 : ℤ
hd : Associated (d ^ k) a
⊢ ∃ d, a = d ^ k

Tactic:
replace hd := hd.symm

Goal state after:
a b c : ℤ
hab : IsCoprime a b
k : ℕ
hk : Odd k
h : a * b = c ^ k
d : ℤ
hd : Associated a (d ^ k)
⊢ ∃ d, a = d ^ k
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
inst✝² : Fintype K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
n : ℕ
hcard : q = p ^ n
x : K
⊢ (frobenius K p ^ n) x = 1 x

Tactic:
;

Goal state after:
K : Type u_1
inst✝³ : Field K
inst✝² : Fintype K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
n : ℕ
hcard : q = p ^ n
x : K
⊢ (frobenius K p ^ n) x = 1 x
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: case h
hp : Fact (Nat.Prime 2)
⊢ ∃ b, 0 ^ 2 + b ^ 2 = (fun i ↦ i) ⟨0, ⋯⟩

Tactic:
;

Goal state after:
case h
hp : Fact (Nat.Prime 2)
⊢ ∃ b, 0 ^ 2 + b ^ 2 = (fun i ↦ i) ⟨0, ⋯⟩