mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

Goal state before:
pp: ι : Type u
R : Type u_1
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : FaithfulSMul R S
inst✝ : NoZeroDivisors S
s : Set ι
i j : ι
v : ι → S
hj✝ : j ∈ insert i s
H₁ : IsTranscendenceBasis R fun x ↦ v ↑x
this✝² : Nontrivial ↥(adjoin R (v '' (insert i s \ {j})))
this✝¹ : Nontrivial S
this✝ : IsDomain S
H₂ : v j ∈ (matroid R S).closure (v '' (insert i s \ {j}))
this : Nontrivial R
inj : InjOn v s
H' : (matroid R S).IsBase (v '' s)
hj : j ∈ s
Hj : v j ∉ (matroid R S).closure (v '' s \ {v j})
hi : i ∉ s
ne : v i ≠ v j
his : v i ∈ v '' s
⊢ v '' (insert i s \ {j}) ⊆ v '' s \ {v j}

Tactic:
rintro x ⟨k, ⟨rfl | hks, hkj⟩, rfl⟩

Goal state after:
case inl
ι : Type u
R : Type u_1
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : FaithfulSMul R S
inst✝ : NoZeroDivisors S
s : Set ι
j : ι
v : ι → S
H₁ : IsTranscendenceBasis R fun x ↦ v ↑x
this✝² : Nontrivial S
this✝¹ : IsDomain S
this✝ : Nontrivial R
inj : InjOn v s
H' : (matroid R S).IsBase (v '' s)
hj✝ : j ∈ s
Hj : v j ∉ (matroid R S).closure (v '' s \ {v j})
k : ι
hkj : k ∉ {j}
hj : j ∈ insert k s
this : Nontrivial ↥(adjoin R (v '' (insert k s \ {j})))
H₂ : v j ∈ (matroid R S).closure (v '' (insert k s \ {j}))
hi : k ∉ s
ne : v k ≠ v j
his : v k ∈ v '' s
⊢ v k ∈ v '' s \ {v j}

case inr
ι : Type u
R : Type u_1
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : FaithfulSMul R S
inst✝ : NoZeroDivisors S
s : Set ι
i j : ι
v : ι → S
hj✝ : j ∈ insert i s
H₁ : IsTranscendenceBasis R fun x ↦ v ↑x
this✝² : Nontrivial ↥(adjoin R (v '' (insert i s \ {j})))
this✝¹ : Nontrivial S
this✝ : IsDomain S
H₂ : v j ∈ (matroid R S).closure (v '' (insert i s \ {j}))
this : Nontrivial R
inj : InjOn v s
H' : (matroid R S).IsBase (v '' s)
hj : j ∈ s
Hj : v j ∉ (matroid R S).closure (v '' s \ {v j})
hi : i ∉ s
ne : v i ≠ v j
his : v i ∈ v '' s
k : ι
hkj : k ∉ {j}
hks : k ∈ s
⊢ v k ∈ v '' s \ {v j}
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: case prime
F : Type u
inst✝¹ : Field F
f : F[X]
q : ℕ
inst✝ : ExpChar F q
hm : f.Monic
h : f.natSepDegree = 1
n : ℕ
y : F
hi : Irreducible (X ^ (q ^ n.pred * q) - C y)
hf : f = X ^ q ^ n - C y
hq : Nat.Prime q
hchar✝ : CharP F q
hn : ¬n = 0
x✝ : y ∈ (frobenius F q).range
z : F
hy : (frobenius F q) z = y
this : ExpChar F[X] q
⊢ False

Tactic:
pow_mul,

Goal state after:
case prime
F : Type u
inst✝¹ : Field F
f : F[X]
q : ℕ
inst✝ : ExpChar F q
hm : f.Monic
h : f.natSepDegree = 1
n : ℕ
y : F
hi : Irreducible ((X ^ q ^ n.pred) ^ q - C y)
hf : f = X ^ q ^ n - C y
hq : Nat.Prime q
hchar✝ : CharP F q
hn : ¬n = 0
x✝ : y ∈ (frobenius F q).range
z : F
hy : (frobenius F q) z = y
this : ExpChar F[X] q
⊢ False
Module: Mathlib.Topology.Algebra.FilterBasis

Goal state before:
pp: G : Type u
inst✝ : Group G
t : TopologicalSpace G
F : GroupFilterBasis G
hG : F.topology = t
⊢ T2Space G ↔ ⋂₀ F.sets = {1}

Tactic:
by
  have : IsTopologicalGroup G := hG ▸ F.isTopologicalGroup
  rw [IsTopologicalGroup.t2Space_iff_one_closed, ← closure_eq_iff_isClosed,
    R0Space.closure_singleton, ← hG, F.nhds_one_eq, FilterBasis.ker_filter]

Goal state after:
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✝¹ : IsGalois F E
inst✝ : Finite Gal(E/F)
H : ¬FiniteDimensional F E
K : IntermediateField F E
h₁ : FiniteDimensional F ↥K
h₂ : Nat.card Gal(E/F) < finrank F ↥K
K' : IntermediateField F E := normalClosure F (↥K) E
this : IsGalois F ↥K'
⊢ False

Tactic:
have := Nat.card_le_card_of_surjective _
    (AlgEquiv.restrictNormalHom_surjective (F := F) (K₁ := K') (E := E))

Goal state after:
F : Type u_1
inst✝⁴ : Field F
E : Type u_2
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : IsGalois F E
inst✝ : Finite Gal(E/F)
H : ¬FiniteDimensional F E
K : IntermediateField F E
h₁ : FiniteDimensional F ↥K
h₂ : Nat.card Gal(E/F) < finrank F ↥K
K' : IntermediateField F E := normalClosure F (↥K) E
this✝ : IsGalois F ↥K'
this : Nat.card Gal(↥K'/F) ≤ Nat.card Gal(E/F)
⊢ False
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: case refine_2
F : Type u
inst✝¹ : Field F
f : F[X]
q : ℕ
inst✝ : ExpChar F q
hm✝ : f.Monic
x✝ : ∃ m n y, m ≠ 0 ∧ f = (X ^ q ^ n - C y) ^ m
m n : ℕ
y : F
hm : m ≠ 0
h : f = (X ^ q ^ n - C y) ^ m
⊢ (if False then 0 else (X ^ q ^ n - C y).natSepDegree) = 1

Tactic:
ite_false,

Goal state after:
case refine_2
F : Type u
inst✝¹ : Field F
f : F[X]
q : ℕ
inst✝ : ExpChar F q
hm✝ : f.Monic
x✝ : ∃ m n y, m ≠ 0 ∧ f = (X ^ q ^ n - C y) ^ m
m n : ℕ
y : F
hm : m ≠ 0
h : f = (X ^ q ^ n - C y) ^ m
⊢ (X ^ q ^ n - C y).natSepDegree = 1
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
H : Subgroup Gal(L/K)
left✝ : H ∈ fixedByFinite K L
a : Gal(L/K)
haH : a ∈ (fun g ↦ g.carrier) H
b : Gal(L/K)
hbH : b ∈ (fun g ↦ g.carrier) H
⊢ (fun x1 x2 ↦ x1 * x2) a b ∈ (fun g ↦ g.carrier) H

Tactic:
exact H.mul_mem haH hbH

Goal state after:
Module: Mathlib.Topology.Algebra.OpenSubgroup

Goal state before:
pp: case h.nhds
G : Type u_1
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : IsTopologicalGroup G
inst✝ : CompactSpace G
W : Set G
WClopen : IsClopen W
S : Set G
Smemnhds : S ∈ 𝓝 1
mulclose : W * S ⊆ W
U : Set G
UsubS : U ⊆ S
Uopen : IsOpen[inst✝³] U
onememU : 1 ∈ U
⊢ U ∩ U⁻¹ ∈ 𝓝 1

pp: case inv
G : Type u_1
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : IsTopologicalGroup G
inst✝ : CompactSpace G
W : Set G
WClopen : IsClopen W
S : Set G
Smemnhds : S ∈ 𝓝 1
mulclose : W * S ⊆ W
U : Set G
UsubS : U ⊆ S
Uopen : IsOpen[inst✝³] U
onememU : 1 ∈ U
⊢ (U ∩ U⁻¹)⁻¹ = U ∩ U⁻¹

pp: case h.isOpen
G : Type u_1
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : IsTopologicalGroup G
inst✝ : CompactSpace G
W : Set G
WClopen : IsClopen W
S : Set G
Smemnhds : S ∈ 𝓝 1
mulclose : W * S ⊆ W
U : Set G
UsubS : U ⊆ S
Uopen : IsOpen[inst✝³] U
onememU : 1 ∈ U
⊢ IsOpen[inst✝³] (U ∩ U⁻¹)

pp: case h.mul
G : Type u_1
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : IsTopologicalGroup G
inst✝ : CompactSpace G
W : Set G
WClopen : IsClopen W
S : Set G
Smemnhds : S ∈ 𝓝 1
mulclose : W * S ⊆ W
U : Set G
UsubS : U ⊆ S
Uopen : IsOpen[inst✝³] U
onememU : 1 ∈ U
⊢ W * (U ∩ U⁻¹) ⊆ W

Tactic:
· simp [Uopen.mem_nhds onememU, inv_mem_nhds_one]

Goal state after:
case inv
G : Type u_1
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : IsTopologicalGroup G
inst✝ : CompactSpace G
W : Set G
WClopen : IsClopen W
S : Set G
Smemnhds : S ∈ 𝓝 1
mulclose : W * S ⊆ W
U : Set G
UsubS : U ⊆ S
Uopen : IsOpen[inst✝³] U
onememU : 1 ∈ U
⊢ (U ∩ U⁻¹)⁻¹ = U ∩ U⁻¹

case h.isOpen
G : Type u_1
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : IsTopologicalGroup G
inst✝ : CompactSpace G
W : Set G
WClopen : IsClopen W
S : Set G
Smemnhds : S ∈ 𝓝 1
mulclose : W * S ⊆ W
U : Set G
UsubS : U ⊆ S
Uopen : IsOpen[inst✝³] U
onememU : 1 ∈ U
⊢ IsOpen[inst✝³] (U ∩ U⁻¹)

case h.mul
G : Type u_1
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : IsTopologicalGroup G
inst✝ : CompactSpace G
W : Set G
WClopen : IsClopen W
S : Set G
Smemnhds : S ∈ 𝓝 1
mulclose : W * S ⊆ W
U : Set G
UsubS : U ⊆ S
Uopen : IsOpen[inst✝³] U
onememU : 1 ∈ U
⊢ W * (U ∩ U⁻¹) ⊆ W
Module: Mathlib.Topology.Algebra.Group.ClosedSubgroup

Goal state before:
pp: G : Type u
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : SeparatelyContinuousMul G
H : Subgroup G
h : IsClosed ↑H
⊢ IsClosed ↑H.normalCore

Tactic:
rw [normalCore_eq_iInf_comap_conj]

Goal state after:
G : Type u
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : SeparatelyContinuousMul G
H : Subgroup G
h : IsClosed ↑H
⊢ IsClosed ↑(⨅ g, comap (↑(MulAut.conj g)) H)
Module: Mathlib.FieldTheory.Galois.Basic

Goal state before:
pp: case mp
F : Type u_1
E : Type u_2
E' : Type u_3
inst✝⁷ : Field F
inst✝⁶ : Field E
inst✝⁵ : Field E'
inst✝⁴ : Algebra F E
inst✝³ : Algebra F E'
inst✝² : Algebra E E'
inst✝¹ : IsScalarTower F E E'
L : IntermediateField F E
inst✝ : Normal F E
f : Gal(E'/F)
⊢ (∀ x ∈ map (IsScalarTower.toAlgHom F E E') L, f x = x) → ∀ x ∈ L, ((restrictNormalHom E) f) x = x

pp: case mpr
F : Type u_1
E : Type u_2
E' : Type u_3
inst✝⁷ : Field F
inst✝⁶ : Field E
inst✝⁵ : Field E'
inst✝⁴ : Algebra F E
inst✝³ : Algebra F E'
inst✝² : Algebra E E'
inst✝¹ : IsScalarTower F E E'
L : IntermediateField F E
inst✝ : Normal F E
f : Gal(E'/F)
⊢ (∀ x ∈ L, ((restrictNormalHom E) f) x = x) → ∀ x ∈ map (IsScalarTower.toAlgHom F E E') L, f x = x

Tactic:
· rintro h x hx
    change f.restrictNormal E x = x
    apply_fun _ using (algebraMap E E').injective
    rw [AlgEquiv.restrictNormal_commutes]
    exact h _ ⟨x, hx, rfl⟩

Goal state after:
case mpr
F : Type u_1
E : Type u_2
E' : Type u_3
inst✝⁷ : Field F
inst✝⁶ : Field E
inst✝⁵ : Field E'
inst✝⁴ : Algebra F E
inst✝³ : Algebra F E'
inst✝² : Algebra E E'
inst✝¹ : IsScalarTower F E E'
L : IntermediateField F E
inst✝ : Normal F E
f : Gal(E'/F)
⊢ (∀ x ∈ L, ((restrictNormalHom E) f) x = x) → ∀ x ∈ map (IsScalarTower.toAlgHom F E E') L, f x = 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
a✝ : Nontrivial S
this : (minpolyDiv R x).leadingCoeff * (X - C x).leadingCoeff = 1
⊢ (minpolyDiv R x).Monic

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
a✝ : Nontrivial S
this : (minpolyDiv R x * (X - C x)).leadingCoeff = (map (algebraMap R S) (minpoly R x)).leadingCoeff
⊢ (minpolyDiv R x).leadingCoeff * (X - C x).leadingCoeff ≠ 0

Tactic:
· simpa using! this

Goal state after:
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
this : (minpolyDiv R x * (X - C x)).leadingCoeff = (map (algebraMap R S) (minpoly R x)).leadingCoeff
⊢ (minpolyDiv R x).leadingCoeff * (X - C x).leadingCoeff ≠ 0
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✝ : IsIntegrallyClosed R
p : R[X]
h : p.Monic
hp : Irreducible p
a b : K[X]
hₐ : ¬IsUnit a
a' : R[X]
ha : Polynomial.map (algebraMap R K) a' * C a.leadingCoeff = a
b' : R[X]
H : Polynomial.map (algebraMap R K) p = Polynomial.map (algebraMap R K) (a' * b')
hb : Polynomial.map (algebraMap R K) b' * C b.leadingCoeff = b
this : a.leadingCoeff * b.leadingCoeff = 1
⊢ C 1 = 1

Tactic:
C_1

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsIntegrallyClosed R
p : R[X]
h : p.Monic
hp : Irreducible p
a b : K[X]
hₐ : ¬IsUnit a
a' : R[X]
ha : Polynomial.map (algebraMap R K) a' * C a.leadingCoeff = a
b' : R[X]
H : Polynomial.map (algebraMap R K) p = Polynomial.map (algebraMap R K) (a' * b')
hb : Polynomial.map (algebraMap R K) b' * C b.leadingCoeff = b
this : a.leadingCoeff * b.leadingCoeff = 1
⊢ 1 = 1
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✝ : IsIntegrallyClosed R
p : R[X]
h : p.Monic
hp : Irreducible p
a b : K[X]
hₐ : ¬IsUnit a
a' : R[X]
ha : Polynomial.map (algebraMap R K) a' * C a.leadingCoeff = a
b' : R[X]
H : Polynomial.map (algebraMap R K) p = Polynomial.map (algebraMap R K) (a' * b')
hb : Polynomial.map (algebraMap R K) b' * C b.leadingCoeff = b
this : a.leadingCoeff * b.leadingCoeff = 1
h_contra : IsUnit a'
⊢ C 1 = 1

Tactic:
C_1

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsIntegrallyClosed R
p : R[X]
h : p.Monic
hp : Irreducible p
a b : K[X]
hₐ : ¬IsUnit a
a' : R[X]
ha : Polynomial.map (algebraMap R K) a' * C a.leadingCoeff = a
b' : R[X]
H : Polynomial.map (algebraMap R K) p = Polynomial.map (algebraMap R K) (a' * b')
hb : Polynomial.map (algebraMap R K) b' * C b.leadingCoeff = b
this : a.leadingCoeff * b.leadingCoeff = 1
h_contra : IsUnit a'
⊢ 1 = 1
Module: Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain R
inst✝³ : Algebra R S
inst✝² : IsIntegrallyClosed R
inst✝¹ : IsDomain S
inst✝ : IsTorsionFree R S
x✝ x : S
B : PowerBasis R S
hint : IsIntegral R x
hx : B.gen ∈ R[x]
⊢ PowerBasis R S

Tactic:
apply PowerBasis.ofAdjoinEqTop' hint
  exact PowerBasis.adjoin_eq_top_of_gen_mem_adjoin hx

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✝ : IsGCDMonoid R
f : R[X]
hf : f.IsPrimitive
g : K[X]
this : NormalizedGCDMonoid R := ⋯.some
x✝ : g * map (algebraMap R K) f ∈ lifts (algebraMap R K)
k : R[X]
hk : map (algebraMap R K) k = g * map (algebraMap R K) f
g' : R[X] := integerNormalization R⁰ g
b : R
hb₁ : b ∈ R⁰
hb₂ : map (algebraMap R K) g' = b • g
g'_mul_f : (g' * f).content = (b • k).content
h : Associated (g'.content * f.content) (b * k.content)
⊢ g ∈ lifts (algebraMap R K)

Tactic:
hf.content_eq_one,

Goal state after:
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✝ : IsGCDMonoid R
f : R[X]
hf : f.IsPrimitive
g : K[X]
this : NormalizedGCDMonoid R := ⋯.some
x✝ : g * map (algebraMap R K) f ∈ lifts (algebraMap R K)
k : R[X]
hk : map (algebraMap R K) k = g * map (algebraMap R K) f
g' : R[X] := integerNormalization R⁰ g
b : R
hb₁ : b ∈ R⁰
hb₂ : map (algebraMap R K) g' = b • g
g'_mul_f : (g' * f).content = (b • k).content
h : Associated (g'.content * 1) (b * k.content)
⊢ g ∈ lifts (algebraMap R K)
Module: Mathlib.FieldTheory.Galois.Infinite

Goal state before:
pp: 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
h : IsOpen L.fixingSubgroup.carrier
S : Set Gal(K/k)
gp : Subgroup Gal(K/k)
eq : (fun g ↦ g.carrier) gp = S
M : IntermediateField k K
sub : (fun g ↦ g.carrier) M.fixingSubgroup ⊆ (↑(IntermediateFieldEquivClosedSubgroup.toFun L)).carrier
hM : M ∈ finiteExts k K
eq' : M.fixingSubgroup = gp
this : FiniteDimensional k ↥M
⊢ FiniteDimensional k ↥L

Tactic:
let L' : FiniteGaloisIntermediateField k K := {
    normalClosure k M K with
    finiteDimensional := normalClosure.is_finiteDimensional k M K
    isGalois := IsGalois.normalClosure k M K }

Goal state after:
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
h : IsOpen L.fixingSubgroup.carrier
S : Set Gal(K/k)
gp : Subgroup Gal(K/k)
eq : (fun g ↦ g.carrier) gp = S
M : IntermediateField k K
sub : (fun g ↦ g.carrier) M.fixingSubgroup ⊆ (↑(IntermediateFieldEquivClosedSubgroup.toFun L)).carrier
hM : M ∈ finiteExts k K
eq' : M.fixingSubgroup = gp
this : FiniteDimensional k ↥M
L' : FiniteGaloisIntermediateField k K :=
  let __src := normalClosure k (↥M) K;
  { toIntermediateField := __src, finiteDimensional := ⋯, isGalois := ⋯ }
⊢ FiniteDimensional k ↥L
Module: Mathlib.FieldTheory.PurelyInseparable.Basic

Goal state before:
pp: case h
F : Type u
E : Type v
inst✝⁸ : Field F
inst✝⁷ : Field E
inst✝⁶ : Algebra F E
K : Type w
inst✝⁵ : Field K
inst✝⁴ : Algebra F K
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
p : ℕ
inst✝ : ExpChar A p
x y : A
n : ℕ
hx : x ^ p ^ n ∈ (algebraMap R A).rangeS
m : ℕ
hy : y ^ p ^ m ∈ (algebraMap R A).rangeS
⊢ x ^ (p ^ n * p ^ m) * y ^ (p ^ n * p ^ m) ∈ (algebraMap R A).rangeS

Tactic:
pow_mul,

Goal state after:
case h
F : Type u
E : Type v
inst✝⁸ : Field F
inst✝⁷ : Field E
inst✝⁶ : Algebra F E
K : Type w
inst✝⁵ : Field K
inst✝⁴ : Algebra F K
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
p : ℕ
inst✝ : ExpChar A p
x y : A
n : ℕ
hx : x ^ p ^ n ∈ (algebraMap R A).rangeS
m : ℕ
hy : y ^ p ^ m ∈ (algebraMap R A).rangeS
⊢ (x ^ p ^ n) ^ p ^ m * y ^ (p ^ n * p ^ m) ∈ (algebraMap R A).rangeS
Module: Mathlib.FieldTheory.PurelyInseparable.Basic

Goal state before:
pp: case h
F : Type u
E : Type v
inst✝⁸ : Field F
inst✝⁷ : Field E
inst✝⁶ : Algebra F E
K : Type w
inst✝⁵ : Field K
inst✝⁴ : Algebra F K
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
p : ℕ
inst✝ : ExpChar A p
x y : A
n : ℕ
hx : x ^ p ^ n ∈ (algebraMap R A).rangeS
m : ℕ
hy : y ^ p ^ m ∈ (algebraMap R A).rangeS
⊢ x ^ (p ^ n * p ^ m) + y ^ (p ^ n * p ^ m) ∈ (algebraMap R A).rangeS

Tactic:
pow_mul,

Goal state after:
case h
F : Type u
E : Type v
inst✝⁸ : Field F
inst✝⁷ : Field E
inst✝⁶ : Algebra F E
K : Type w
inst✝⁵ : Field K
inst✝⁴ : Algebra F K
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
p : ℕ
inst✝ : ExpChar A p
x y : A
n : ℕ
hx : x ^ p ^ n ∈ (algebraMap R A).rangeS
m : ℕ
hy : y ^ p ^ m ∈ (algebraMap R A).rangeS
⊢ (x ^ p ^ n) ^ p ^ m + y ^ (p ^ n * p ^ m) ∈ (algebraMap R A).rangeS
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
K : Type w
inst✝⁵ : Field K
inst✝⁴ : Algebra F K
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
p : ℕ
inst✝ : ExpChar A p
x : R
⊢ (algebraMap R A) x ^ p ^ 0 ∈ (algebraMap R A).rangeS

Tactic:
rw [pow_zero, pow_one]

Goal state after:
F : Type u
E : Type v
inst✝⁸ : Field F
inst✝⁷ : Field E
inst✝⁶ : Algebra F E
K : Type w
inst✝⁵ : Field K
inst✝⁴ : Algebra F K
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
p : ℕ
inst✝ : ExpChar A p
x : R
⊢ (algebraMap R A) x ∈ (algebraMap R A).rangeS
Module: Mathlib.FieldTheory.PurelyInseparable.Basic

Goal state before:
pp: case inl.add
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
x y : R ⊗[k] K
h : ∃ n, x ^ q ^ n ∈ (algebraMap R (R ⊗[k] K)).range
h' : ∃ n, y ^ q ^ n ∈ (algebraMap R (R ⊗[k] K)).range
⊢ ∃ n, (x + y) ^ q ^ n ∈ (algebraMap R (R ⊗[k] K)).range

Tactic:
have : ExpChar (R ⊗[k] K) q := expChar_of_injective_ringHom (algebraMap k _).injective q

Goal state after:
case inl.add
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
x y : R ⊗[k] K
h : ∃ n, x ^ q ^ n ∈ (algebraMap R (R ⊗[k] K)).range
h' : ∃ n, y ^ q ^ n ∈ (algebraMap R (R ⊗[k] K)).range
this : ExpChar (R ⊗[k] K) q
⊢ ∃ n, (x + y) ^ q ^ n ∈ (algebraMap R (R ⊗[k] K)).range
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
⊢ (Algebra.trace K L) x = finrank (↥K⟮x⟯) L • (Algebra.trace K ↥K⟮x⟯) (AdjoinSimple.gen K x)

Tactic:
rw [← trace_trace (S := K⟮x⟯)]
  conv in x => rw [← AdjoinSimple.algebraMap_gen K x]
  rw [trace_algebraMap, LinearMap.map_smul_of_tower]

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

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
a : ZMod n
⊢ ↑a.val - ↑n ≤ 0

Tactic:
sub_nonpos,

Goal state after:
n : ℕ
inst✝ : NeZero n
a : ZMod n
⊢ ↑a.val ≤ ↑n
Module: Mathlib.Data.ZMod.ValMinAbs

Goal state before:
pp: n a : ℕ
inst✝ : NeZero n
ha : (↑a).valMinAbs = ↑a
⊢ a ≤ n / 2

Tactic:
rw [← Int.natAbs_natCast a, ← ha]

Goal state after:
n a : ℕ
inst✝ : NeZero n
ha : (↑a).valMinAbs = ↑a
⊢ (↑a).valMinAbs.natAbs ≤ n / 2
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 < (-g).degree

Tactic:
rw [degree_neg, hg2]

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.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 u = p

Tactic:
rwa [orderOf_units, Subgroup.orderOf_coe]

Goal state after:
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
this : IntermediateField.restrictScalars K (FixedPoints.intermediateField ↥H) = IntermediateField.restrictScalars K ⊥
⊢ x ∈ FixedPoints.intermediateField ↥H

Tactic:
rw [restrictScalars_bot_eq_self] at this

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
this : IntermediateField.restrictScalars K (FixedPoints.intermediateField ↥H) = F
⊢ x ∈ FixedPoints.intermediateField ↥H
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
⊢ fixingSubgroup G (Set.range ⇑(algebraMap B C)) = H

Tactic:
have : IsDomain B := (FaithfulSMul.algebraMap_injective B C).isDomain
  have : IsDomain A := (FaithfulSMul.algebraMap_injective A C).isDomain
  let K := FractionRing A
  let L := FractionRing C
  let : MulSemiringAction G L := IsFractionRing.mulSemiringAction G C L
  have : IsGaloisGroup H (FractionRing B) L := IsGaloisGroup.toFractionRing H B C
  rw [← fixingSubgroup_range_algebraMap' G K L H (FractionRing B)]
  ext g
  simp only [mem_fixingSubgroup_iff, Set.mem_range]
  refine ⟨?_, ?_⟩
  · rintro h _ ⟨x, rfl⟩
    have {x} : g • (algebraMap B L) x = (algebraMap B L) x := by
      rw [IsScalarTower.algebraMap_apply B C L, ← algebraMap.smul', h _ ⟨x, rfl⟩]
    obtain ⟨a, b, _, rfl⟩ := IsFractionRing.div_surjective B x
    simp only [map_div₀, ← IsScalarTower.algebraMap_apply, smul_div₀', this]
  · rintro h _ ⟨x, rfl⟩
    apply FaithfulSMul.algebraMap_injective C L
    rw [algebraMap.smul']
    apply h
    use algebraMap B (FractionRing B) x
    rw [← IsScalarTower.algebraMap_apply, ← IsScalarTower.algebraMap_apply]

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

Goal state before:
pp: case mpr
K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
i : ℕ
x : Kˣ
h : x ^ i = 1
hx : ∀ (x_1 : Kˣ), x_1 ∈ Submonoid.powers x
j : ℕ
⊢ x ^ (i * j) = 1

Tactic:
pow_mul,

Goal state after:
case mpr
K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
i : ℕ
x : Kˣ
h : x ^ i = 1
hx : ∀ (x_1 : Kˣ), x_1 ∈ Submonoid.powers x
j : ℕ
⊢ (x ^ i) ^ j = 1