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

Goal state before:
pp: F : Type u_1
inst✝⁴ : Field F
E : Type u_2
inst✝³ : Field E
inst✝² : Algebra F E
K : IntermediateField F E
inst✝¹ : FiniteDimensional F E
inst✝ : IsGalois F E
| finrank (↥(fixedField K.fixingSubgroup)) E

Tactic:
IntermediateField.finrank_fixedField_eq_card

Goal state after:
F : Type u_1
inst✝⁴ : Field F
E : Type u_2
inst✝³ : Field E
inst✝² : Algebra F E
K : IntermediateField F E
inst✝¹ : FiniteDimensional F E
inst✝ : IsGalois F E
| Nat.card ↥K.fixingSubgroup
Module: Mathlib.FieldTheory.SeparableClosure

Goal state before:
pp: F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.EssFiniteType F E
d : Finset E → ℕ := fun s ↦ finInsepDegree (↥(adjoin F ↑s)) E
s : Finset E
hs : adjoin F ↑s = ⊤
⊢ {s | IsTranscendenceBasis F Subtype.val}.Nonempty

Tactic:
have : Algebra.IsAlgebraic (Algebra.adjoin F (s : Set E)) E := by
      rw [← isAlgebraic_adjoin_iff_top, hs, Algebra.isAlgebraic_iff_isIntegral]
      refine Algebra.isIntegral_of_surjective topEquiv.surjective

Goal state after:
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.EssFiniteType F E
d : Finset E → ℕ := fun s ↦ finInsepDegree (↥(adjoin F ↑s)) E
s : Finset E
hs : adjoin F ↑s = ⊤
this : Algebra.IsAlgebraic (↥(Algebra.adjoin F ↑s)) E
⊢ {s | IsTranscendenceBasis F Subtype.val}.Nonempty
Module: Mathlib.FieldTheory.Galois.Basic

Goal state before:
pp: F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : FiniteDimensional F E
h : Nat.card Gal(E/F) = finrank F E
p : 0 < finrank (↥(fixedField ⊤)) E
⊢ Nat.card Gal(E/F) = finrank (↥(fixedField ⊤)) E

Tactic:
IntermediateField.finrank_fixedField_eq_card

Goal state after:
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : FiniteDimensional F E
h : Nat.card Gal(E/F) = finrank F E
p : 0 < finrank (↥(fixedField ⊤)) E
⊢ Nat.card Gal(E/F) = Nat.card ↥⊤
Module: Mathlib.FieldTheory.KrullTopology

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
E1 : IntermediateField K L
h_E1 : E1 ∈ finiteExts K L
E2 : IntermediateField K L
h_E2 : E2 ∈ finiteExts K L
this✝ : FiniteDimensional K ↥E1
this : FiniteDimensional K ↥E2
⊢ ∃ z ∈ (fun g ↦ g.carrier) '' fixedByFinite K L,
    z ⊆ (fun g ↦ g.carrier) E1.fixingSubgroup ∩ (fun g ↦ g.carrier) E2.fixingSubgroup

Tactic:
refine ⟨(E1 ⊔ E2).fixingSubgroup.carrier, ⟨_, ⟨_, E1.finiteDimensional_sup E2, rfl⟩, rfl⟩, ?_⟩

Goal state after:
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
E1 : IntermediateField K L
h_E1 : E1 ∈ finiteExts K L
E2 : IntermediateField K L
h_E2 : E2 ∈ finiteExts K L
this✝ : FiniteDimensional K ↥E1
this : FiniteDimensional K ↥E2
⊢ (E1 ⊔ E2).fixingSubgroup.carrier ⊆ (fun g ↦ g.carrier) E1.fixingSubgroup ∩ (fun g ↦ g.carrier) E2.fixingSubgroup
Module: Mathlib.FieldTheory.KrullTopology

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
U : Set Gal(L/K)
hU : U ∈ (galBasis K L).sets
⊢ U * U ⊆ U

Tactic:
by
      rcases hU with ⟨H, _, rfl⟩
      rintro x ⟨a, haH, b, hbH, rfl⟩
      exact H.mul_mem haH hbH

Goal state after:
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : FiniteDimensional F E
heq : finSepDegree F E = finrank F E
x : E
halg : IsAlgebraic F x
h : finSepDegree F ↥F⟮x⟯ < finrank F ↥F⟮x⟯
this : finSepDegree F ↥F⟮x⟯ * finSepDegree (↥F⟮x⟯) E < finrank F ↥F⟮x⟯ * finrank (↥F⟮x⟯) E
⊢ False

Tactic:
rw [finSepDegree_mul_finSepDegree_of_isAlgebraic F F⟮x⟯ E,
      Module.finrank_mul_finrank F F⟮x⟯ E] at this

Goal state after:
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : FiniteDimensional F E
heq : finSepDegree F E = finrank F E
x : E
halg : IsAlgebraic F x
h : finSepDegree F ↥F⟮x⟯ < finrank F ↥F⟮x⟯
this : finSepDegree F E < finrank F E
⊢ False
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: case refine_1
F : Type u_1
inst✝ : Field F
x✝ : PerfectField F
f : F[X]
hf : f.natSepDegree = 1
hf0 : f ≠ 0
u : F[X]ˣ
hu : (UniqueFactorizationMonoid.factors f).prod * ↑u = f
g : F[X]
h : g.Separable
hg : g ∈ UniqueFactorizationMonoid.factors f
key : g.natDegree ≤ f.natSepDegree
⊢ g.Splits

Tactic:
hf

Goal state after:
case refine_1
F : Type u_1
inst✝ : Field F
x✝ : PerfectField F
f : F[X]
hf : f.natSepDegree = 1
hf0 : f ≠ 0
u : F[X]ˣ
hu : (UniqueFactorizationMonoid.factors f).prod * ↑u = f
g : F[X]
h : g.Separable
hg : g ∈ UniqueFactorizationMonoid.factors f
key : g.natDegree ≤ 1
⊢ g.Splits
Module: Mathlib.LinearAlgebra.BilinearForm.DualLattice

Goal state before:
pp: R : Type ?u.5
S : Type ?u.7
M : Type ?u.9
inst✝⁸ : CommRing R
inst✝⁷ : Field S
inst✝⁶ : AddCommGroup M
inst✝⁵ : Algebra R S
inst✝⁴ : Module R M
inst✝³ : Module S M
inst✝² : IsScalarTower R S M
B : BilinForm S M
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R S
N : Submodule R M
x✝ : ↥(B.dualSubmodule N)
x y : ↥N
⊢ (algebraMap R S) (B.dualSubmoduleParing x✝ (x + y)) =
    (algebraMap R S) (B.dualSubmoduleParing x✝ x + B.dualSubmoduleParing x✝ y)

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.BilinearForm.DualLattice

Goal state before:
pp: R : Type ?u.5
S : Type ?u.7
M : Type ?u.9
inst✝⁸ : CommRing R
inst✝⁷ : Field S
inst✝⁶ : AddCommGroup M
inst✝⁵ : Algebra R S
inst✝⁴ : Module R M
inst✝³ : Module S M
inst✝² : IsScalarTower R S M
B : BilinForm S M
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R S
N : Submodule R M
x y : ↥(B.dualSubmodule N)
z : ↥N
⊢ (algebraMap R S) ({ toFun := B.dualSubmoduleParing (x + y), map_add' := ⋯, map_smul' := ⋯ } z) =
    (algebraMap R S)
      (({ toFun := B.dualSubmoduleParing x, map_add' := ⋯, map_smul' := ⋯ } +
          { toFun := B.dualSubmoduleParing y, map_add' := ⋯, map_smul' := ⋯ })
        z)

Tactic:
simp

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

Goal state before:
pp: case h.left
k : Type u_1
K : Type u_2
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
L : IntermediateField k K
inst✝ : IsGalois k K
σ : Gal(K/k)
h : σ ∈ (↑L.fixingSubgroup)ᶜ
y : K
yL : y ∈ ↑L
ne : y ∉ fun a ↦ σ • a = a
f : Gal(K/k)
⊢ f ∈ σ • ↑(adjoin k {y}).fixingSubgroup → f ∈ (↑L.fixingSubgroup)ᶜ

Tactic:
hf

Goal state after:
case h.left
k : Type u_1
K : Type u_2
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
L : IntermediateField k K
inst✝ : IsGalois k K
σ : Gal(K/k)
h : σ ∈ (↑L.fixingSubgroup)ᶜ
y : K
yL : y ∈ ↑L
ne : y ∉ fun a ↦ σ • a = a
f : Gal(K/k)
hf : f ∈ σ • ↑(adjoin k {y}).fixingSubgroup
⊢ f ∈ (↑L.fixingSubgroup)ᶜ
Module: Mathlib.FieldTheory.Minpoly.MinpolyDiv

Goal state before:
pp: R : Type u_2
S : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
⊢ eval x (minpolyDiv R x) = eval x (derivative (minpolyDiv R x * (X - C x)))

Tactic:
simp

Goal state after:
Module: Mathlib.FieldTheory.Minpoly.MinpolyDiv

Goal state before:
pp: R : Type u_2
S : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
i : ℕ
H : (minpolyDiv R x).coeff i ∉ R[x]
⊢ ∀ (j : ℕ), (minpolyDiv R x).coeff (i + j) ∉ R[x]

Tactic:
intro j

Goal state after:
R : Type u_2
S : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
i : ℕ
H : (minpolyDiv R x).coeff i ∉ R[x]
j : ℕ
⊢ (minpolyDiv R x).coeff (i + j) ∉ R[x]
Module: Mathlib.FieldTheory.Minpoly.MinpolyDiv

Goal state before:
pp: R : Type u_2
S : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
x : S
hx : IsIntegral R x
inst✝ : Nontrivial S
⊢ (minpolyDiv R x).natDegree + 1 = (minpolyDiv R x).natDegree + (X - C x).natDegree

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Polynomial.GaussLemma

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : K[X]
h0 : p ≠ 0
h : IsUnit (integerNormalization R⁰ p).primPart
u : Rˣ
hu : C ↑u = (integerNormalization R⁰ p).primPart
c : R
c0 : c ∈ R⁰
hc : map (algebraMap R K) (integerNormalization R⁰ p) = C ((algebraMap R K) c) * p
⊢ C ((algebraMap R K) ((integerNormalization R⁰ p).content * ↑u)) =
    map (algebraMap R K) (C ((integerNormalization R⁰ p).content * ↑u))

Tactic:
simp

Goal state after:
Module: Mathlib.FieldTheory.Minpoly.MinpolyDiv

Goal state before:
pp: case a.ind.refine_1
R : Type u_2
S : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
hx : IsIntegral R x
a✝ : Nontrivial S
i : ℕ
hi :
  ∀ m < i,
    m ∈ Set.Iio (minpoly R x).natDegree →
      m ∈ (fun x_1 ↦ x ^ x_1) ⁻¹' ↑(Submodule.span R (Set.range (minpolyDiv R x).coeff))
hi' : i ∈ Set.Iio (minpoly R x).natDegree
this : (minpolyDiv R x).coeff ((minpolyDiv R x).natDegree - i) ∈ Submodule.span R (Set.range (minpolyDiv R x).coeff)
⊢ Set.Iio i ⊆ (fun x_1 ↦ x ^ x_1) ⁻¹' ↑(Submodule.span R (Set.range (minpolyDiv R x).coeff))

Tactic:
intro j

Goal state after:
case a.ind.refine_1
R : Type u_2
S : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
hx : IsIntegral R x
a✝ : Nontrivial S
i : ℕ
hi :
  ∀ m < i,
    m ∈ Set.Iio (minpoly R x).natDegree →
      m ∈ (fun x_1 ↦ x ^ x_1) ⁻¹' ↑(Submodule.span R (Set.range (minpolyDiv R x).coeff))
hi' : i ∈ Set.Iio (minpoly R x).natDegree
this : (minpolyDiv R x).coeff ((minpolyDiv R x).natDegree - i) ∈ Submodule.span R (Set.range (minpolyDiv R x).coeff)
j : ℕ
⊢ j ∈ Set.Iio i → j ∈ (fun x_1 ↦ x ^ x_1) ⁻¹' ↑(Submodule.span R (Set.range (minpolyDiv R x).coeff))
Module: Mathlib.RingTheory.Trace.Defs

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a : R
⊢ (trace R R) a = a

Tactic:
simp

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

Goal state before:
pp: F : Type u
E : Type v
inst✝⁵ : Field F
inst✝⁴ : Field E
inst✝³ : Algebra F E
L : Type w
inst✝² : Field L
inst✝¹ : IsAlgClosed L
inst✝ : Nonempty (E →+* L)
h : Function.Injective fun f ↦ f.comp (algebraMap F E)
this : Algebra E L := (Classical.arbitrary (E →+* L)).toAlgebra
j : AlgebraicClosure E →ₐ[E] L := IsAlgClosed.lift
f g : Emb F E
x✝ : F
⊢ ((fun f ↦ f.comp (algebraMap F E)) (j.comp ↑f)) x✝ = ((fun f ↦ f.comp (algebraMap F E)) (j.comp ↑g)) x✝

Tactic:
simp

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

Goal state before:
pp: case neg
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
halg : ¬Algebra.IsAlgebraic F E
⊢ finSepDegree F E * finrank (↥(separableClosure F E)) E = finrank F E

Tactic:
finrank_of_infinite_dimensional (K := F) (V := E) fun _ ↦
      halg (Algebra.IsAlgebraic.of_finite F E),

Goal state after:
case neg
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
halg : ¬Algebra.IsAlgebraic F E
⊢ finSepDegree F E * finrank (↥(separableClosure F E)) E = 0
Module: Mathlib.FieldTheory.PurelyInseparable.Basic

Goal state before:
pp: k : Type u_1
K : Type u_2
R : Type u_3
inst✝⁶ : Field k
inst✝⁵ : Field K
inst✝⁴ : Algebra k K
inst✝³ : CommRing R
inst✝² : Algebra k R
inst✝¹ : IsPurelyInseparable k K
q : ℕ
inst✝ : ExpChar k q
a✝ : Nontrivial (R ⊗[k] K)
hq : Nat.Prime q
⊢ (algebraMap R (R ⊗[k] K)) 0 = 0 ^ q ^ 0

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.IsGaloisGroup.Defs

Goal state before:
pp: G : Type u_1
A : Type u_2
A' : Type u_3
B : Type u_4
inst✝⁵ : Group G
inst✝⁴ : CommSemiring A
inst✝³ : Semiring B
inst✝² : Algebra A B
inst✝¹ : MulSemiringAction G B
hA : IsGaloisGroup G A B
inst✝ : FaithfulSMul A B
x✝ : A
⊢ (fun x ↦ ⋯.choose) ((fun x ↦ ⟨(algebraMap A B) x, ⋯⟩) x✝) = x✝

Tactic:
simp

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Basic

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
e : K ≃+* L
inst✝ : NumberField K
⊢ e.toAddMonoidHom 1 = 1

Tactic:
simp

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Basic

Goal state before:
pp: K : Type u_1
inst✝ : Field K
x y : K
hx : x ∈ integralClosure ℤ K
hy : y ∈ integralClosure ℤ K
⊢ ⟨x, hx⟩ = ⟨y, hy⟩ ↔ x = y

Tactic:
simp

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Basic

Goal state before:
pp: z : ℤ
⊢ ↑(ringOfIntegersEquiv (ringOfIntegersEquiv.symm z)) = (algebraMap (𝓞 ℚ) ℚ) (ringOfIntegersEquiv.symm z)

Tactic:
simp

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

Goal state before:
pp: G : Type u_1
inst✝⁹ : Group G
H : Subgroup G
A : Type u_2
B : Type u_3
C : Type u_4
inst✝⁸ : CommSemiring A
inst✝⁷ : Semiring C
inst✝⁶ : Algebra A C
inst✝⁵ : MulSemiringAction G C
N : Subgroup G
inst✝⁴ : CommSemiring B
inst✝³ : Algebra B C
inst✝² : FaithfulSMul B C
inst✝¹ : IsGaloisGroup (↥N) B C
inst✝ : N.Normal
this : MulSemiringAction G B := mulSemiringActionOfNormal G B C N
q : G ⧸ N
x : B
g₁ g₂ : G
h : (QuotientGroup.leftRel N) g₁ g₂
⊢ g₁⁻¹ * g₂ ∈ ?m.186

Tactic:
← QuotientGroup.leftRel_apply

Goal state after:
G : Type u_1
inst✝⁹ : Group G
H : Subgroup G
A : Type u_2
B : Type u_3
C : Type u_4
inst✝⁸ : CommSemiring A
inst✝⁷ : Semiring C
inst✝⁶ : Algebra A C
inst✝⁵ : MulSemiringAction G C
N : Subgroup G
inst✝⁴ : CommSemiring B
inst✝³ : Algebra B C
inst✝² : FaithfulSMul B C
inst✝¹ : IsGaloisGroup (↥N) B C
inst✝ : N.Normal
this : MulSemiringAction G B := mulSemiringActionOfNormal G B C N
q : G ⧸ N
x : B
g₁ g₂ : G
h : (QuotientGroup.leftRel N) g₁ g₂
⊢ (QuotientGroup.leftRel ?m.193) g₁ g₂

G : Type u_1
inst✝⁹ : Group G
H : Subgroup G
A : Type u_2
B : Type u_3
C : Type u_4
inst✝⁸ : CommSemiring A
inst✝⁷ : Semiring C
inst✝⁶ : Algebra A C
inst✝⁵ : MulSemiringAction G C
N : Subgroup G
inst✝⁴ : CommSemiring B
inst✝³ : Algebra B C
inst✝² : FaithfulSMul B C
inst✝¹ : IsGaloisGroup (↥N) B C
inst✝ : N.Normal
this : MulSemiringAction G B := ⋯
q : G ⧸ N
x : B
g₁ g₂ : G
h : (QuotientGroup.leftRel N) g₁ g₂
⊢ Subgroup G
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:
simp

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

Goal state before:
pp: case zero
a : ZMod 0
⊢ a.valMinAbs * 2 = ↑0 ↔ 2 * a.val = 0

Tactic:
simp

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

Goal state before:
pp: case zero
a : ℕ
ha : a ≤ 0 / 2
⊢ (↑a).valMinAbs = ↑a

Tactic:
simp

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
κ' : 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:
simp

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ˣ
⊢ ∀ a ∈ univ.erase (-1), a * a⁻¹ = 1

Tactic:
simp

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ˣ
⊢ ∀ a ∈ univ.erase (-1), a⁻¹⁻¹ = a

Tactic:
simp

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

Goal state before:
pp: K : Type u_1
inst✝² : Ring K
inst✝¹ : NoZeroDivisors K
G : Subgroup Kˣ
inst✝ : Fintype ↥G
a : ↥G
ha : a ≠ 1
a_mul_emb : ↥G ↪ ↥G := mulLeftEmbedding a
⊢ map a_mul_emb univ = univ

Tactic:
simp

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
x✝ : L
⊢ x✝ ∈ FixedPoints.intermediateField ↥⊤ ↔ x✝ ∈ FixedPoints.intermediateField G

Tactic:
simp

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
B : Type u_5
inst✝² : CommSemiring B
inst✝¹ : Algebra B L
inst✝ : IsGaloisGroup (↥H) B L
x✝ : L
⊢ (∃ y, (algebraMap B L) y = x✝) → ∀ (m : ↥H), m • x✝ = x✝

Tactic:
rintro ⟨x, rfl⟩ h

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
B : Type u_5
inst✝² : CommSemiring B
inst✝¹ : Algebra B L
inst✝ : IsGaloisGroup (↥H) B L
x : B
h : ↥H
⊢ h • (algebraMap B L) x = (algebraMap B L) x
Module: Mathlib.FieldTheory.Finite.Basic

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

Tactic:
simp

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

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

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

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

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

Goal state after:
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 * ↑1 = d ^ 2 ∨ d ^ 2 * ↑1 = -d ^ 2

Tactic:
simp

Goal state after:
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 * ↑(-1) = d ^ 2 ∨ d ^ 2 * ↑(-1) = -d ^ 2

Tactic:
simp

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

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

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

Tactic:
simp

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

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

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

Tactic:
simp

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

Goal state before:
pp: case zero
p : ℕ
inst✝ : Fact (Nat.Prime p)
x : ZMod p
⊢ x ^ p ^ 0 = x

Tactic:
simp

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

Goal state before:
pp: n : ℕ
x✝ : ℤ
⊢ ((↑(quotientSpanNatEquivZMod n).symm).comp (castRingHom (ZMod n))) x✝ = (Ideal.Quotient.mk (Ideal.span {↑n})) x✝

Tactic:
simp

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

Goal state before:
pp: n x✝ : ℤ
⊢ ((↑n.quotientSpanEquivZMod.symm).comp (castRingHom (ZMod n.natAbs))) x✝ = (Ideal.Quotient.mk (Ideal.span {n})) x✝

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.Quotient.Pi

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝⁴ : CommRing R
Ms : ι → Type u_3
inst✝³ : (i : ι) → AddCommGroup (Ms i)
inst✝² : (i : ι) → Module R (Ms i)
p : (i : ι) → Submodule R (Ms i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
⊢ Function.RightInverse ⇑(piQuotientLift p (pi Set.univ p) (single R Ms) ⋯) ⇑(quotientPiLift p (fun i ↦ (p i).mkQ) ⋯)

Tactic:
rw [Function.rightInverse_iff_comp, ← coe_comp, ← @id_coe R]

Goal state after:
ι : Type u_1
R : Type u_2
inst✝⁴ : CommRing R
Ms : ι → Type u_3
inst✝³ : (i : ι) → AddCommGroup (Ms i)
inst✝² : (i : ι) → Module R (Ms i)
p : (i : ι) → Submodule R (Ms i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
⊢ ⇑(quotientPiLift p (fun i ↦ (p i).mkQ) ⋯ ∘ₗ piQuotientLift p (pi Set.univ p) (single R Ms) ⋯) = ⇑LinearMap.id
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: F : Type u_3
inst✝¹ : Field F
inst✝ : Finite F
hF : ringChar F ≠ 2
h : Function.Injective fun x ↦ x * x
⊢ -1 * -1 = 1 * 1

Tactic:
simp

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

Goal state before:
pp: F : Type u_3
inst✝¹ : Field F
inst✝ : Fintype F
n : ℕ+
hp : Nat.Prime (ringChar F)
h : Fintype.card F = ringChar F ^ ↑n
⊢ ringChar F = 2 ↔ ringChar F = 2 ∧ ↑n ≠ 0

Tactic:
simp

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

Goal state before:
pp: F : Type u_3
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
g : Fˣ
hg : ∀ (x : Fˣ), x ∈ Subgroup.zpowers g
n : ℕ
hodd : 2 * (Nat.card F / 2) = Nat.card F - 1
h : (fun x ↦ g ^ x) n ^ (Nat.card F / 2) = 1
key : 2 * (Nat.card F / 2) ∣ n * (Nat.card F / 2)
⊢ 0 < 2

Tactic:
simp

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

Goal state before:
pp: case mpr
F : Type u_3
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
y : F
ha : y * y ≠ 0
hy : y ≠ 0
⊢ y * y = ↑(Units.mk0 y hy) * ↑(Units.mk0 y hy)

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Ideal.Basis

Goal state before:
pp: ι : Type u_1
R : Type u_2
S : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain S
inst✝³ : Algebra R S
N : Type u_4
inst✝² : Semiring N
inst✝¹ : Module N S
inst✝ : SMulCommClass R N S
b : Basis ι R S
x : S
hx : x ≠ 0
i : ι
⊢ ((↑(b.constr N)).toFun (Subtype.val ∘ ⇑(basisSpanSingleton b hx))) (b i) = ((Algebra.lmul R S) x) (b i)

Tactic:
simp

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

Goal state before:
pp: case e_6
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring S
inst✝² : Algebra R S
inst✝¹ : Ring T
inst✝ : Algebra R T
e : S ≃ₐ[R] T
x : S
x✝ : T
⊢ ((lmul R T) (e x)) x✝ = (↑↑e ∘ₗ (lmul R S) x ∘ₗ ↑(↑e).symm) x✝

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.FiniteStability

Goal state before:
pp: R : Type w₁
inst✝⁵ : CommRing R
A : Type w₂
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
B : Type w₃
inst✝² : CommRing B
inst✝¹ : Algebra R B
inst✝ : FinitePresentation R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hsurj : Function.Surjective ⇑f
hfg : (RingHom.ker f.toRingHom).FG
g : B ⊗[R] MvPolynomial (Fin n) R →ₐ[B] B ⊗[R] A := TensorProduct.map (AlgHom.id B B) f
hgsurj : Function.Surjective ⇑g
hker_eq : RingHom.ker g = Ideal.map TensorProduct.includeRight (RingHom.ker f)
⊢ (RingHom.ker g).FG

Tactic:
rw [hker_eq]

Goal state after:
R : Type w₁
inst✝⁵ : CommRing R
A : Type w₂
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
B : Type w₃
inst✝² : CommRing B
inst✝¹ : Algebra R B
inst✝ : FinitePresentation R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hsurj : Function.Surjective ⇑f
hfg : (RingHom.ker f.toRingHom).FG
g : B ⊗[R] MvPolynomial (Fin n) R →ₐ[B] B ⊗[R] A := TensorProduct.map (AlgHom.id B B) f
hgsurj : Function.Surjective ⇑g
hker_eq : RingHom.ker g = Ideal.map TensorProduct.includeRight (RingHom.ker f)
⊢ (Ideal.map TensorProduct.includeRight (RingHom.ker f)).FG
Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm

Goal state before:
pp: S : Type u_1
inst✝¹ : CommRing S
P : Ideal S
P_prime : P.IsPrime
inst✝ : IsDedekindDomain S
hP : P ≠ ⊥
i : ℕ
a c : S
a_mem : a ∈ P ^ i
c_mem : c ∈ P ^ i
this : P ^ (i + 1) = span {a} ⊔ P ^ (i + 1)
⊢ 0 ∈ P ^ (i + 1)

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm

Goal state before:
pp: S : Type u_1
inst✝¹ : CommRing S
P : Ideal S
P_prime : P.IsPrime
inst✝ : IsDedekindDomain S
hP : P ≠ ⊥
i : ℕ
a c : S
a_mem : a ∈ P ^ i
c_mem : c ∈ P ^ i
this : P ^ (i + 1) = span {a} ⊔ P ^ (i + 1)
⊢ a + 0 = a

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm

Goal state before:
pp: case zero
S : Type u_1
inst✝¹ : CommRing S
P : Ideal S
P_prime : P.IsPrime
inst✝ : IsDedekindDomain S
hP : P ≠ ⊥
⊢ cardQuot (P ^ 0) = cardQuot P ^ 0

Tactic:
simp

Goal state after: