mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Group.AddCircle

Goal state before:
pp: case refine_3
T : ℝ
hT : Fact (0 < T)
I : Set (AddCircle T)
u x : AddCircle T
hu : IsOfFinAddOrder u
G : AddSubgroup (AddCircle T) := AddSubgroup.zmultiples u
n : ℕ := addOrderOf u
B : Set (AddCircle T) := ball x (T / (2 * ↑n))
hI : I =ᵐ[volume] B
hn : 1 ≤ ↑n
⊢ ∀ (g : ↥G), QuasiMeasurePreserving (fun x ↦ g +ᵥ x) volume volume

pp: case refine_4
T : ℝ
hT : Fact (0 < T)
I : Set (AddCircle T)
u x : AddCircle T
hu : IsOfFinAddOrder u
G : AddSubgroup (AddCircle T) := AddSubgroup.zmultiples u
n : ℕ := addOrderOf u
B : Set (AddCircle T) := ball x (T / (2 * ↑n))
hI : I =ᵐ[volume] B
hn : 1 ≤ ↑n
⊢ volume univ ≤ ∑' (g : ↥G), volume (g +ᵥ I)

Tactic:
· -- `∀ (g : G), QuasiMeasurePreserving (VAdd.vadd g) volume volume`
    exact fun g => quasiMeasurePreserving_add_left (G := AddCircle T) volume g

Goal state after:
case refine_4
T : ℝ
hT : Fact (0 < T)
I : Set (AddCircle T)
u x : AddCircle T
hu : IsOfFinAddOrder u
G : AddSubgroup (AddCircle T) := AddSubgroup.zmultiples u
n : ℕ := addOrderOf u
B : Set (AddCircle T) := ball x (T / (2 * ↑n))
hI : I =ᵐ[volume] B
hn : 1 ≤ ↑n
⊢ volume univ ≤ ∑' (g : ↥G), volume (g +ᵥ I)
Module: Mathlib.Dynamics.Ergodic.Conservative

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
μ : Measure α
hf : Conservative f μ
n : ℕ
⊢ Conservative f^[n] μ

Tactic:
rcases n with - | n

Goal state after:
case zero
α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
μ : Measure α
hf : Conservative f μ
⊢ Conservative f^[0] μ

case succ
α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
μ : Measure α
hf : Conservative f μ
n : ℕ
⊢ Conservative f^[n + 1] μ
Module: Mathlib.Dynamics.Ergodic.AddCircle

Goal state before:
pp: T : ℝ
hT : Fact (0 < T)
n : ℤ
hn✝ : 1 < |n|
s : Set (AddCircle T)
hs : MeasurableSet s
hs' : (fun y ↦ n • y) ⁻¹' s = s
u : ℕ → AddCircle T := fun j ↦ ↑(1 / ↑(n.natAbs ^ j) * T)
hn : 1 < n.natAbs
hu₀ : ∀ (j : ℕ), addOrderOf (u j) = n.natAbs ^ j
hnu : ∀ (j : ℕ), n ^ j • u j = 0
hu₁ : ∀ (j : ℕ), u j +ᵥ s =ᵐ[volume] s
hu₂ : Tendsto (fun j ↦ addOrderOf (u j)) atTop atTop
⊢ s =ᵐ[volume] ∅ ∨ s =ᵐ[volume] univ

Tactic:
exact ae_empty_or_univ_of_forall_vadd_ae_eq_self hs.nullMeasurableSet hu₁ hu₂

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
ν : Measure α
inst✝¹ : μ.HaveLebesgueDecomposition ν
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
hf : AEMeasurable f ν
hf_ne_zero : ∀ᵐ (x : α) ∂ν, f x ≠ 0
hf_ne_top : ∀ᵐ (x : α) ∂ν, f x ≠ ∞
this : SigmaFinite (ν.withDensity f)
s : Set α
hs : MeasurableSet s
⊢ AEMeasurable f (ν.restrict s)

Tactic:
· exact hf.restrict

Goal state after:
Module: Mathlib.Dynamics.OmegaLimit

Goal state before:
pp: τ : Type u_1
α : Type u_2
β : Type u_3
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
c : Set β
hc₁ : IsCompact c
n : Set β
hn₁ : IsOpen[inst✝] n
hn₂ : ω f ϕ s ⊆ n
v : Set τ
hv₁ : v ∈ f
hv₂ : closure[inst✝] (image2 ϕ v s) ⊆ c
k : Set β := closure[inst✝] (image2 ϕ v s)
hk : IsCompact (k \ n)
j : Set τ → Set β := fun u ↦ (closure[inst✝] (image2 ϕ (u ∩ v) s))ᶜ
hj₁ : ∀ u ∈ f, IsOpen[inst✝] (j u)
hj₂ : k \ n ⊆ ⋃ u ∈ f, j u
g : Set (Set τ)
hg₁ : ∀ u ∈ g, u ∈ f
hg₂ : g.Finite
hg₃ : k \ n ⊆ ⋃ i ∈ g, j i
w : Set τ := (⋂ u ∈ g, u) ∩ v
⊢ w ∈ f

Tactic:
simpa [w, *]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : μ.HaveLebesgueDecomposition ν
inst✝ : SFinite ν
hμν : μ ≪ ν
s : Set α
⊢ ∫⁻ (x : α) in s, μ.rnDeriv ν x ∂ν = μ s

Tactic:
rw [← withDensity_apply' _ s, Measure.withDensity_rnDeriv_eq _ _ hμν]

Goal state after:
Module: Mathlib.ModelTheory.Basic

Goal state before:
pp: L : Language
⊢ L.card = (sum fun l ↦ lift.{v, u} #(L.Functions l)) + sum fun l ↦ lift.{u, v} #(L.Relations l)

Tactic:
simp only [card, mk_sum, mk_sigma, lift_sum]

Goal state after:
Module: Mathlib.ModelTheory.LanguageMap

Goal state before:
pp: L : Language
L' : Language
M : Type w
inst✝ : L.Structure M
α : Type w'
ie : IsEmpty α
⊢ LHom.sumInl.sumElim (LHom.sumInl.comp (LHom.ofIsEmpty (constantsOn α) L)) = LHom.id L[[α]]

Tactic:
exact _root_.trans (congr rfl (Subsingleton.elim _ _)) LHom.sumElim_inl_inr

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case func.zero.inr
L : Language
M : Type w
inst✝² : L.Structure M
α : Type u'
β : Type v'
inst✝¹ : L[[α]].Structure M
inst✝ : (L.lhomWithConstants α).IsExpansionOn M
v : β → M
ts : Fin 0 → L[[α]].Term β
ih : ∀ (a : Fin 0), realize (Sum.elim (fun a ↦ ↑(L.con a)) v) (ts a).constantsToVars = realize v (ts a)
val✝ : (constantsOn α).Functions 0
⊢ realize (Sum.elim (fun a ↦ ↑(L.con a)) v) (func (Sum.inr val✝) ts).constantsToVars =
    realize v (func (Sum.inr val✝) ts)

Tactic:
simp only [realize, constantsToVars, Sum.elim_inl, funMap_eq_coe_constants]
        rfl

Goal state after:
Module: Mathlib.ModelTheory.Substructures

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
s : Set M
⊢ lift.{max u w, w} #↑(range (Term.realize Subtype.val)) ≤ #(L.Term ↑s)

Tactic:
rw [← Cardinal.lift_id'.{w, max u w} #(L.Term s)]

Goal state after:
L : Language
M : Type w
inst✝ : L.Structure M
s : Set M
⊢ lift.{max u w, w} #↑(range (Term.realize Subtype.val)) ≤ lift.{w, max u w} #(L.Term ↑s)
Module: Mathlib.ModelTheory.Substructures

Goal state before:
pp: case refine_2
L : Language
M : Type w
inst✝ : L.Structure M
s : Set M
h : ∀ {n : ℕ} (f : L.Functions n), ClosedUnder f s
⊢ s ∈ (closure L).closed

Tactic:
have h' : closure L s = ⟨s, h⟩ := closure_eq_of_le (refl _) subset_closure
    exact congr_arg _ h'

Goal state after:
Module: Mathlib.ModelTheory.Substructures

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
A s : Set M
⊢ A ⊆ ↑((closure L[[↑A]]).toFun s)

Tactic:
intro a ha

Goal state after:
L : Language
M : Type w
inst✝ : L.Structure M
A s : Set M
a : M
ha : a ∈ A
⊢ a ∈ ↑((closure L[[↑A]]).toFun s)
Module: Mathlib.ModelTheory.Definability

Goal state before:
pp: M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
β : Type u_1
s : Set (β → M)
h : A.Definable L s
f : α ≃ β
⊢ (fun g ↦ g ∘ ⇑f.symm) ⁻¹' s = (fun g ↦ g ∘ ⇑f) '' s

Tactic:
image_eq_preimage_of_inverse

Goal state after:
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
β : Type u_1
s : Set (β → M)
h : A.Definable L s
f : α ≃ β
⊢ (fun g ↦ g ∘ ⇑f.symm) ⁻¹' s = ?m.39 ⁻¹' s

case h₁
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
β : Type u_1
s : Set (β → M)
h : A.Definable L s
f : α ≃ β
⊢ Function.LeftInverse ?m.39 fun g ↦ g ∘ ⇑f

case h₂
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
β : Type u_1
s : Set (β → M)
h : A.Definable L s
f : α ≃ β
⊢ Function.RightInverse ?m.39 fun g ↦ g ∘ ⇑f

M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
β : Type u_1
s : Set (β → M)
h : A.Definable L s
f : α ≃ β
⊢ (α → M) → β → M
Module: Mathlib.ModelTheory.Skolem

Goal state before:
pp: L : Language
⊢ ℵ₀ ≤ #((i : ℕ) × L.BoundedFormula Empty (i + 1))

Tactic:
exact infinite_iff.1 (Infinite.of_injective (fun n => ⟨n, ⊥⟩) fun x y xy =>
      (Sigma.mk.inj_iff.1 xy).1)

Goal state after:
Module: Mathlib.RingTheory.Nullstellensatz

Goal state before:
pp: k : Type u_1
K : Type u_2
inst✝² : Field k
inst✝¹ : Field K
inst✝ : Algebra k K
σ : Type u_3
x : σ → K
⊢ (vanishingIdeal k {x}).IsPrime

Tactic:
convert! RingHom.ker_isPrime (aeval (R := k) x)

Goal state after:
k : Type u_1
K : Type u_2
inst✝² : Field k
inst✝¹ : Field K
inst✝ : Algebra k K
σ : Type u_3
x : σ → K
⊢ vanishingIdeal k {x} = RingHom.ker (aeval x)
Module: Mathlib.FieldTheory.Finite.Extension

Goal state before:
pp: k : Type u_1
inst✝⁴ : Field k
inst✝³ : Finite k
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : CharP k p
n : ℕ
inst✝ : NeZero n
i : ℕ
x : Extension k p n
⊢ (frob k p n ^ i) x = x ^ Nat.card k ^ i

Tactic:
induction i generalizing x with
  | zero => simp
  | succ i ih =>
      rw [pow_add, pow_one, AlgEquiv.mul_apply, ih, frob_apply, ← pow_mul, ← Nat.pow_add_one']

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

Goal state before:
pp: K : Type u_1
σ : Type u_2
inst✝² : Fintype K
inst✝¹ : Fintype σ
inst✝ : CommRing K
a : σ → K
⊢ (eval a) (indicator a) = 1

Tactic:
nontriviality
  have : 0 < Fintype.card K - 1 := tsub_pos_of_lt Fintype.one_lt_card
  simp only [indicator, map_prod, map_sub, map_one, map_pow, eval_X, eval_C, sub_self,
    zero_pow this.ne', sub_zero, Finset.prod_const_one]

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

Goal state before:
pp: σ K : Type u
inst✝ : Fintype K
m : ℕ
⊢ DecidablePred fun x ↦ x ∈ {n | ∀ (i : σ), n i ≤ m}

Tactic:
simp only [Set.mem_ofPred_eq]; infer_instance

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

Goal state before:
pp: case h
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Finite L
this✝ : Finite K
this : Fintype K
x : L
hx :
  Ideal.span {X ^ finrank K L - 1} =
    (toSpanSingleton K[X] (AEval' (frobeniusAlgHom K L).toLinearMap)
        ((AEval'.of (frobeniusAlgHom K L).toLinearMap) x)).ker
⊢ LinearIndependent K fun σ ↦ σ x

Tactic:
rw [← linearIndependent_equiv ((finCongr <| natDegree_X_pow_sub_C (R := K)).trans <|
    .ofBijective _ <| bijective_frobeniusAlgEquivOfAlgebraic_pow K L)]

Goal state after:
case h
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Finite L
this✝ : Finite K
this : Fintype K
x : L
hx :
  Ideal.span {X ^ finrank K L - 1} =
    (toSpanSingleton K[X] (AEval' (frobeniusAlgHom K L).toLinearMap)
        ((AEval'.of (frobeniusAlgHom K L).toLinearMap) x)).ker
⊢ LinearIndependent K
    ((fun σ ↦ σ x) ∘ ⇑((finCongr ⋯).trans (Equiv.ofBijective (fun n ↦ frobeniusAlgEquivOfAlgebraic K L ^ ↑n) ⋯)))

K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Finite L
this✝ : Finite K
this : Fintype K
x : L
hx :
  Ideal.span {X ^ finrank K L - 1} =
    (toSpanSingleton K[X] (AEval' (frobeniusAlgHom K L).toLinearMap)
        ((AEval'.of (frobeniusAlgHom K L).toLinearMap) x)).ker
⊢ K
Module: Mathlib.FieldTheory.Galois.Profinite

Goal state before:
pp: k : Type u_3
K : Type u_4
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
L : IntermediateField k K
inst✝ : Normal k ↥L
N : Set Gal(↥L/k)
L' : IntermediateField k ↥L
left✝ : FiniteDimensional k ↥L'
hO : ↑L'.fixingSubgroup ⊆ N
⊢ ⇑(AlgEquiv.restrictNormalHom ↥L) ⁻¹' N ∈ nhds 1

Tactic:
have := Module.Finite.equiv <| AlgEquiv.toLinearEquiv <| IntermediateField.liftAlgEquiv L'

Goal state after:
k : Type u_3
K : Type u_4
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
L : IntermediateField k K
inst✝ : Normal k ↥L
N : Set Gal(↥L/k)
L' : IntermediateField k ↥L
left✝ : FiniteDimensional k ↥L'
hO : ↑L'.fixingSubgroup ⊆ N
this : Module.Finite k ↥(IntermediateField.lift L')
⊢ ⇑(AlgEquiv.restrictNormalHom ↥L) ⁻¹' N ∈ nhds 1
Module: Mathlib.FieldTheory.IsPerfectClosure

Goal state before:
pp: case neg
R : Type u_1
inst✝ : CommSemiring R
p : ℕ
x : R
hp : ¬1 < p
x✝ : ∃ n, x ^ p ^ n = 0
n : ℕ
h : x ^ p ^ n = 0
⊢ x = 0

Tactic:
rcases Nat.le_one_iff_eq_zero_or_eq_one.1 (not_lt.1 hp) with hp | hp

Goal state after:
case neg.inl
R : Type u_1
inst✝ : CommSemiring R
p : ℕ
x : R
hp✝ : ¬1 < p
x✝ : ∃ n, x ^ p ^ n = 0
n : ℕ
h : x ^ p ^ n = 0
hp : p = 0
⊢ x = 0

case neg.inr
R : Type u_1
inst✝ : CommSemiring R
p : ℕ
x : R
hp✝ : ¬1 < p
x✝ : ∃ n, x ^ p ^ n = 0
n : ℕ
h : x ^ p ^ n = 0
hp : p = 1
⊢ x = 0
Module: Mathlib.FieldTheory.IsPerfectClosure

Goal state before:
pp: case refine_2
K : Type u_1
L : Type u_2
inst✝² : CommSemiring K
inst✝¹ : CommSemiring L
i : K →+* L
p : ℕ
inst✝ : IsPRadical i p
x : K
h : x ∈ pNilradical K p
⊢ x ∈ Ideal.comap i (pNilradical L p)

Tactic:
simp only [Ideal.mem_comap, mem_pNilradical] at h ⊢

Goal state after:
case refine_2
K : Type u_1
L : Type u_2
inst✝² : CommSemiring K
inst✝¹ : CommSemiring L
i : K →+* L
p : ℕ
inst✝ : IsPRadical i p
x : K
h : ∃ n, x ^ p ^ n = 0
⊢ ∃ n, i x ^ p ^ n = 0
Module: Mathlib.FieldTheory.IsPerfectClosure

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝³ : CommSemiring K
inst✝² : CommSemiring L
i : K →+* L
p : ℕ
inst✝¹ : ExpChar L p
inst✝ : PerfectRing L p
x : K
h : x ∈ pNilradical K p
⊢ x ∈ ker i

Tactic:
obtain ⟨n, h⟩ := mem_pNilradical.1 h

Goal state after:
K : Type u_1
L : Type u_2
inst✝³ : CommSemiring K
inst✝² : CommSemiring L
i : K →+* L
p : ℕ
inst✝¹ : ExpChar L p
inst✝ : PerfectRing L p
x : K
h✝ : x ∈ pNilradical K p
n : ℕ
h : x ^ p ^ n = 0
⊢ x ∈ ker i
Module: Mathlib.FieldTheory.IsPerfectClosure

Goal state before:
pp: K : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : CommRing K
inst✝⁷ : CommRing L
inst✝⁶ : CommRing M
inst✝⁵ : CommRing N
i : K →+* L
j : K →+* M
k : K →+* N
f : L →+* M
g : L →+* N
p : ℕ
inst✝⁴ : ExpChar M p
inst✝³ : ExpChar K p
inst✝² : PerfectRing M p
inst✝¹ : IsPRadical i p
inst✝ : ExpChar L p
x1 x2 : L
n1 : ℕ
y1 : K
h1 : i y1 = x1 ^ p ^ n1
n2 : ℕ
y2 : K
h2 : i y2 = x2 ^ p ^ n2
⊢ i (y1 ^ p ^ n2 + y2 ^ p ^ n1) = (x1 + x2) ^ p ^ (n1 + n2)

Tactic:
by rw [map_add,
        map_pow, map_pow, h1, h2, ← pow_mul, ← pow_add, ← pow_mul, ← pow_add,
        add_comm n2, add_pow_expChar_pow]

Goal state after:
Module: Mathlib.FieldTheory.IsPerfectClosure

Goal state before:
pp: K : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst✝¹¹ : CommRing K
inst✝¹⁰ : CommRing L
inst✝⁹ : CommRing M
inst✝⁸ : CommRing N
i : K →+* L
j : K →+* M
g : L →+* N
p : ℕ
inst✝⁷ : ExpChar M p
inst✝⁶ : ExpChar K p
inst✝⁵ : PerfectRing M p
inst✝⁴ : IsPRadical i p
inst✝³ : ExpChar L p
inst✝² : ExpChar N p
inst✝¹ : IsPRadical g p
inst✝ : IsPRadical (g.comp i) p
⊢ (lift g (lift i j p) p).comp (g.comp i) = (lift (g.comp i) j p).comp (g.comp i)

Tactic:
← RingHom.comp_assoc _ _ (lift g _ p),

Goal state after:
K : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst✝¹¹ : CommRing K
inst✝¹⁰ : CommRing L
inst✝⁹ : CommRing M
inst✝⁸ : CommRing N
i : K →+* L
j : K →+* M
g : L →+* N
p : ℕ
inst✝⁷ : ExpChar M p
inst✝⁶ : ExpChar K p
inst✝⁵ : PerfectRing M p
inst✝⁴ : IsPRadical i p
inst✝³ : ExpChar L p
inst✝² : ExpChar N p
inst✝¹ : IsPRadical g p
inst✝ : IsPRadical (g.comp i) p
⊢ ((lift g (lift i j p) p).comp g).comp i = (lift (g.comp i) j p).comp (g.comp i)
Module: Mathlib.FieldTheory.PerfectClosure

Goal state before:
pp: K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
n : ℕ
x : K
⊢ (⇑(frobenius (PerfectClosure K p) p))^[n] (mk K p (n, x)) = (of K p) x

Tactic:
by
  induction n with
  | zero => rfl
  | succ n ih => rw [iterate_succ_apply, ← ih, frobenius_mk, mk_succ_pow]

Goal state after:
Module: Mathlib.FieldTheory.Isaacs

Goal state before:
pp: F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
alg : Algebra.IsAlgebraic F E
h : ∀ (x : E), ∃ y, (aeval y) (minpoly F x) = 0
S : Finset E
p : K[X] := ∏ x ∈ S, Polynomial.map (algebraMap F K) (minpoly F x)
K' : Type u_3 := p.SplittingField
⊢ ↥(adjoin F ↑S) →ₐ[F] K

Tactic:
have splits s (hs : s ∈ S) : ((minpoly F s).map (algebraMap F K')).Splits := by
    apply (SplittingField.splits p).of_dvd (map_ne_zero (Finset.prod_ne_zero_iff.mpr
      fun _ _ ↦ Polynomial.map_ne_zero (minpoly.ne_zero <| alg.isIntegral.1 _))) ?_
    rw [IsScalarTower.algebraMap_eq F K K', ← Polynomial.map_map, map_dvd_map']
    exact Finset.dvd_prod_of_mem _ hs

Goal state after:
F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
alg : Algebra.IsAlgebraic F E
h : ∀ (x : E), ∃ y, (aeval y) (minpoly F x) = 0
S : Finset E
p : K[X] := ∏ x ∈ S, Polynomial.map (algebraMap F K) (minpoly F x)
K' : Type u_3 := p.SplittingField
splits : ∀ s ∈ S, (Polynomial.map (algebraMap F K') (minpoly F s)).Splits
⊢ ↥(adjoin F ↑S) →ₐ[F] K
Module: Mathlib.FieldTheory.PerfectClosure

Goal state before:
pp: K : Type u
inst✝⁵ : CommRing K
p : ℕ
inst✝⁴ : Fact (Nat.Prime p)
inst✝³ : CharP K p
L : Type v
inst✝² : CommSemiring L
inst✝¹ : CharP L p
inst✝ : PerfectRing L p
f : PerfectClosure K p →+* L
⊢ (fun f ↦
        { toFun := fun e ↦ e.liftOn (fun x ↦ (⇑(frobeniusEquiv L p).symm)^[x.1] (f x.2)) ⋯, map_one' := ⋯,
          map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ })
      ((fun f ↦ f.comp (of K p)) f) =
    f

Tactic:
by
    ext ⟨n, x⟩
    simp only [quot_mk_eq_mk, RingHom.comp_apply, RingHom.coe_mk, MonoidHom.coe_mk, OneHom.coe_mk,
      liftOn_mk]
    apply (injective_frobenius L p).iterate n
    rw [← f.map_iterate_frobenius, iterate_frobenius_mk,
      RightInverse.iterate (frobenius_apply_frobeniusEquiv_symm L p) n]

Goal state after:
Module: Mathlib.RingTheory.Algebraic.LinearIndependent

Goal state before:
pp: F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
x : E
H : ∀ (p : F[X]), (aeval x) p = 0 → p = 0
s : Finset F
m : F → F
i : F
hi : i ∈ s
hnz : ∀ (a : F), x - (algebraMap F E) a ≠ 0
b : E := ∏ j ∈ s, (x - (algebraMap F E) j)
h1 : ∀ i ∈ s, m i • (b * (x - (algebraMap F E) i)⁻¹) = m i • ∏ j ∈ s.erase i, (x - (algebraMap F E) j)
hm : ∑ x_1 ∈ s, m x_1 • ∏ j ∈ s.erase x_1, (x - (algebraMap F E) j) = 0
p : F[X] := ∑ i ∈ s, C (m i) * ∏ j ∈ s.erase i, (X - C j)
⊢ (aeval x) p = ∑ x_1 ∈ s, m x_1 • ∏ j ∈ s.erase x_1, (x - (algebraMap F E) j)

Tactic:
p,

Goal state after:
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
x : E
H : ∀ (p : F[X]), (aeval x) p = 0 → p = 0
s : Finset F
m : F → F
i : F
hi : i ∈ s
hnz : ∀ (a : F), x - (algebraMap F E) a ≠ 0
b : E := ∏ j ∈ s, (x - (algebraMap F E) j)
h1 : ∀ i ∈ s, m i • (b * (x - (algebraMap F E) i)⁻¹) = m i • ∏ j ∈ s.erase i, (x - (algebraMap F E) j)
hm : ∑ x_1 ∈ s, m x_1 • ∏ j ∈ s.erase x_1, (x - (algebraMap F E) j) = 0
p : F[X] := ∑ i ∈ s, C (m i) * ∏ j ∈ s.erase i, (X - C j)
⊢ (aeval x) (∑ i ∈ s, C (m i) * ∏ j ∈ s.erase i, (X - C j)) =
    ∑ x_1 ∈ s, m x_1 • ∏ j ∈ s.erase x_1, (x - (algebraMap F E) j)
Module: Mathlib.RingTheory.Algebraic.LinearIndependent

Goal state before:
pp: F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
x : E
H : ∀ (p : F[X]), (aeval x) p = 0 → p = 0
s : Finset F
m : F → F
i : F
hi : i ∈ s
hnz : ∀ (a : F), x - (algebraMap F E) a ≠ 0
b : E := ∏ j ∈ s, (x - (algebraMap F E) j)
h1 : ∀ i ∈ s, m i • (b * (x - (algebraMap F E) i)⁻¹) = m i • ∏ j ∈ s.erase i, (x - (algebraMap F E) j)
p : F[X] := ∑ i ∈ s, C (m i) * ∏ j ∈ s.erase i, (X - C j)
h2 : ∀ j ∈ s.erase i, m j * ∏ x ∈ s.erase j, (i - x) = 0
hm : (aeval i) p = 0
⊢ m i = 0

Tactic:
p,

Goal state after:
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
x : E
H : ∀ (p : F[X]), (aeval x) p = 0 → p = 0
s : Finset F
m : F → F
i : F
hi : i ∈ s
hnz : ∀ (a : F), x - (algebraMap F E) a ≠ 0
b : E := ∏ j ∈ s, (x - (algebraMap F E) j)
h1 : ∀ i ∈ s, m i • (b * (x - (algebraMap F E) i)⁻¹) = m i • ∏ j ∈ s.erase i, (x - (algebraMap F E) j)
p : F[X] := ∑ i ∈ s, C (m i) * ∏ j ∈ s.erase i, (X - C j)
h2 : ∀ j ∈ s.erase i, m j * ∏ x ∈ s.erase j, (i - x) = 0
hm : (aeval i) (∑ i ∈ s, C (m i) * ∏ j ∈ s.erase i, (X - C j)) = 0
⊢ m i = 0
Module: Mathlib.FieldTheory.KummerExtension

Goal state before:
pp: K : Type u
inst✝ : Field K
n : ℕ
ζ : K
hζ : IsPrimitiveRoot ζ n
α a : K
hn : 0 < n
e : α ^ n = a
⊢ X ^ n - C a = ∏ i ∈ Finset.range n, (X - C (ζ ^ i * α))

Tactic:
(X_pow_sub_C_splits_of_isPrimitiveRoot hζ e).eq_prod_roots_of_monic
    (monic_X_pow_sub_C _ hn.ne'),

Goal state after:
K : Type u
inst✝ : Field K
n : ℕ
ζ : K
hζ : IsPrimitiveRoot ζ n
α a : K
hn : 0 < n
e : α ^ n = a
⊢ (Multiset.map (fun x ↦ X - C x) (X ^ n - C a).roots).prod = ∏ i ∈ Finset.range n, (X - C (ζ ^ i * α))
Module: Mathlib.FieldTheory.KummerExtension

Goal state before:
pp: K : Type u
inst✝⁴ : Field K
n : ℕ
hζ : (primitiveRoots n K).Nonempty
a : K
H : Irreducible (X ^ n - C a)
L : Type u_1
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : IsSplittingField K L (X ^ n - C a)
α : L
inst✝ : NeZero n
σ : Gal(L/K)
ζ : K
hζ'✝ : ζ ∈ primitiveRoots n K
hζ' : IsPrimitiveRoot ζ n
hn : 0 < n
hα : ∃ a_1 < n, (algebraMap K L) ζ ^ a_1 * rootOfSplitsXPowSubC ⋯ a L = α
⊢ (autEquivRootsOfUnity ⋯ H L) σ • α = σ α

Tactic:
obtain ⟨i, _, rfl⟩ := hα

Goal state after:
K : Type u
inst✝⁴ : Field K
n : ℕ
hζ : (primitiveRoots n K).Nonempty
a : K
H : Irreducible (X ^ n - C a)
L : Type u_1
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : IsSplittingField K L (X ^ n - C a)
inst✝ : NeZero n
σ : Gal(L/K)
ζ : K
hζ'✝ : ζ ∈ primitiveRoots n K
hζ' : IsPrimitiveRoot ζ n
hn : 0 < n
i : ℕ
left✝ : i < n
⊢ (autEquivRootsOfUnity ⋯ H L) σ • ((algebraMap K L) ζ ^ i * rootOfSplitsXPowSubC ⋯ a L) =
    σ ((algebraMap K L) ζ ^ i * rootOfSplitsXPowSubC ⋯ a L)
Module: Mathlib.FieldTheory.KummerExtension

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : FiniteDimensional K L
hK : (primitiveRoots (finrank K L) K).Nonempty
this : NeZero (finrank K L)
tfae_1_to_3 : IsGalois K L ∧ IsCyclic Gal(L/K) → ∃ α, α ^ finrank K L ∈ Set.range ⇑(algebraMap K L) ∧ K⟮α⟯ = ⊤
tfae_3_to_2 :
  (∃ α, α ^ finrank K L ∈ Set.range ⇑(algebraMap K L) ∧ K⟮α⟯ = ⊤) →
    ∃ a, Irreducible (X ^ finrank K L - C a) ∧ IsSplittingField K L (X ^ finrank K L - C a)
⊢ [IsGalois K L ∧ IsCyclic Gal(L/K),
      ∃ a, Irreducible (X ^ finrank K L - C a) ∧ IsSplittingField K L (X ^ finrank K L - C a),
      ∃ α, α ^ finrank K L ∈ Set.range ⇑(algebraMap K L) ∧ K⟮α⟯ = ⊤].TFAE

Tactic:
tfae_have 2 → 1
  | ⟨a, H, inst⟩ => ⟨isGalois_of_isSplittingField_X_pow_sub_C hK H L,
      isCyclic_of_isSplittingField_X_pow_sub_C hK H L⟩

Goal state after:
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : FiniteDimensional K L
hK : (primitiveRoots (finrank K L) K).Nonempty
this : NeZero (finrank K L)
tfae_1_to_3 : IsGalois K L ∧ IsCyclic Gal(L/K) → ∃ α, α ^ finrank K L ∈ Set.range ⇑(algebraMap K L) ∧ K⟮α⟯ = ⊤
tfae_3_to_2 :
  (∃ α, α ^ finrank K L ∈ Set.range ⇑(algebraMap K L) ∧ K⟮α⟯ = ⊤) →
    ∃ a, Irreducible (X ^ finrank K L - C a) ∧ IsSplittingField K L (X ^ finrank K L - C a)
tfae_2_to_1 :
  (∃ a, Irreducible (X ^ finrank K L - C a) ∧ IsSplittingField K L (X ^ finrank K L - C a)) →
    IsGalois K L ∧ IsCyclic Gal(L/K)
⊢ [IsGalois K L ∧ IsCyclic Gal(L/K),
      ∃ a, Irreducible (X ^ finrank K L - C a) ∧ IsSplittingField K L (X ^ finrank K L - C a),
      ∃ α, α ^ finrank K L ∈ Set.range ⇑(algebraMap K L) ∧ K⟮α⟯ = ⊤].TFAE
Module: Mathlib.GroupTheory.CosetCover

Goal state before:
pp: k : Type u_1
E : Type u_2
inst✝³ : DivisionRing k
inst✝² : Infinite k
inst✝¹ : AddCommGroup E
inst✝ : Module k E
s : Finset (Subspace k E)
hs : ⊤ ∉ s
hcovers : ⋃ p ∈ s, ↑p = Set.univ
p : Subspace k E
hp : p ∈ s
hfi : (Submodule.toAddSubgroup p).FiniteIndex
⊢ False

Tactic:
have : Finite (E ⧸ p) := AddSubgroup.finite_quotient_of_finiteIndex

Goal state after:
k : Type u_1
E : Type u_2
inst✝³ : DivisionRing k
inst✝² : Infinite k
inst✝¹ : AddCommGroup E
inst✝ : Module k E
s : Finset (Subspace k E)
hs : ⊤ ∉ s
hcovers : ⋃ p ∈ s, ↑p = Set.univ
p : Subspace k E
hp : p ∈ s
hfi : (Submodule.toAddSubgroup p).FiniteIndex
this : Finite (E ⧸ p)
⊢ False
Module: Mathlib.FieldTheory.NormalizedTrace

Goal state before:
pp: F : Type u_1
K : Type u_2
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Algebra F K
inst✝¹ : CharZero F
inst✝ : Algebra.IsIntegral F K
m : F
a : K
E : IntermediateField F K := F⟮a⟯
this : FiniteDimensional F ↥F⟮a⟯
ha : a ∈ E
hma : m • a ∈ E
a' : ↥E := ⟨a, ha⟩
ma' : ↥E := ⟨m • a, hma⟩
⊢ normalizedTraceAux F (↥E) ma' = m • (↑(Module.finrank F ↥E))⁻¹ • (trace F ↥E) a'

Tactic:
normalizedTraceAux_eq_of_finiteDimensional F ma',

Goal state after:
F : Type u_1
K : Type u_2
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Algebra F K
inst✝¹ : CharZero F
inst✝ : Algebra.IsIntegral F K
m : F
a : K
E : IntermediateField F K := F⟮a⟯
this : FiniteDimensional F ↥F⟮a⟯
ha : a ∈ E
hma : m • a ∈ E
a' : ↥E := ⟨a, ha⟩
ma' : ↥E := ⟨m • a, hma⟩
⊢ (↑(Module.finrank F ↥E))⁻¹ • (trace F ↥E) ma' = m • (↑(Module.finrank F ↥E))⁻¹ • (trace F ↥E) a'