mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber

Goal state before:
pp: case mp
f : CircleDeg1Lift
hf : Continuous ⇑f
m : ℤ
h : τ f = ↑m
⊢ ∃ x, f x = x + τ f

Tactic:
exact f.exists_eq_add_translationNumber hf

Goal state after:
Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber

Goal state before:
pp: f : CircleDeg1Lift
hf : Continuous ⇑f
n : ℕ
⊢ Continuous ⇑(f ^ n)

Tactic:
rw [coe_pow]
  exact hf.iterate n

Goal state after:
Module: Mathlib.Dynamics.Ergodic.Action.OfMinimal

Goal state before:
pp: G : Type u_1
inst✝⁵ : Group G
inst✝⁴ : TopologicalSpace G
inst✝³ : IsTopologicalGroup G
inst✝² : MeasurableSpace G
inst✝¹ : OpensMeasurableSpace G
μ : Measure G
inst✝ : μ.IsOpenPosMeasure
g : G
hg : Ergodic (fun x ↦ g * x) μ
a : G
h : a ∉ closure[inst✝⁴] (range fun x ↦ g ^ x)
V : Set G
hV₁ : 1 ∈ V
hVo : IsOpen[inst✝⁴] V
hV : ∀ x ∈ V, ∀ y ∈ V, ∀ (m : ℤ), g ^ m ≠ a * x / y
s : Set G := ⋃ m, g ^ m • V
hso : IsOpen[inst✝⁴] s
⊢ 1 ∈ g ^ 0 • V

Tactic:
by simpa

Goal state after:
Module: Mathlib.Topology.Instances.AddCircle.DenseSubgroup

Goal state before:
pp: p : ℝ
inst✝ : Fact (0 < p)
a : AddCircle p
⊢ (DenseRange fun x ↦ x • a) ↔ addOrderOf a = 0

Tactic:
rcases QuotientAddGroup.mk_surjective a with ⟨a, rfl⟩

Goal state after:
p : ℝ
inst✝ : Fact (0 < p)
a : ℝ
⊢ (DenseRange fun x ↦ x • ↑a) ↔ addOrderOf ↑a = 0
Module: Mathlib.Dynamics.Ergodic.Conservative

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : NullMeasurableSet s μ
h0 : μ s ≠ 0
t : ℕ → Set α := fun n ↦ s ∩ f^[n] ⁻¹' s
H : {n | μ (s ∩ f^[n] ⁻¹' s) ≠ 0}.Finite
⊢ 0 ∈ {n | μ (s ∩ f^[n] ⁻¹' s) ≠ 0}

Tactic:
by simpa

Goal state after:
Module: Mathlib.Dynamics.SymbolicDynamics.Basic

Goal state before:
pp: case mpr
A : Type u_1
inst✝² : Inhabited A
G : Type u_2
inst✝¹ : Monoid G
inst✝ : IsLeftCancelMul G
p : Pattern A G
g : G
x : G → A
⊢ x ∈ cylinder (Finset.image (fun x ↦ g * x) p.support) (p.mulShift g) → x ∈ {x | p.mulOccursInAt x g}

Tactic:
intro H u hu
    -- H gives equality with the translated pattern on the image
    have hx : x (g * u) = p.mulShift g (g * u) :=
      H (g * u) (Finset.mem_image_of_mem (g * ·) hu)
    -- rewrite the RHS by the “apply_of_mem” lemma
    simpa [Pattern.mulShift_apply_mul_left_of_mem (p := p) (v := g) (w := u) hu] using hx

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
⊢ ∀ᵐ (x : α) ∂ν.singularPart μ, μ.rnDeriv ν x = 0

Tactic:
refine rnDeriv_eq_zero_of_mutuallySingular (mutuallySingular_singularPart ν μ).symm ?_
  exact (Measure.singularPart_le _ _).absolutelyContinuous

Goal state after:
Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy

Goal state before:
pp: X : Type u_1
T : X → X
F : Set X
U : SetRel X X
n : ℕ
h_fin : coverMincard T F U n < ⊤
k : ℕ
k_min : ↑k = coverMincard T F U n
⊢ ∃ s, IsDynCoverOf T F U n ↑s ∧ ↑(#s) = coverMincard T F U n

Tactic:
← k_min

Goal state after:
X : Type u_1
T : X → X
F : Set X
U : SetRel X X
n : ℕ
h_fin : coverMincard T F U n < ⊤
k : ℕ
k_min : ↑k = coverMincard T F U n
⊢ ∃ s, IsDynCoverOf T F U n ↑s ∧ ↑(#s) = ↑k
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν ν' : Measure α
inst✝² : SigmaFinite μ
inst✝¹ : SigmaFinite ν
inst✝ : SigmaFinite ν'
hνν' : ν ⟂ₘ ν'
h_ac : ν ≪ ν + ν'
h₁ :
  (μ.singularPart ν' + ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν') =ᵐ[ν + ν']
    (μ.singularPart ν').rnDeriv (ν + ν') + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν')
h₂ :
  (μ.singularPart ν' + ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν =ᵐ[ν]
    (μ.singularPart ν').rnDeriv ν + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν
h₃ : (μ.singularPart ν').rnDeriv (ν + ν') =ᵐ[ν] (μ.singularPart ν').rnDeriv ν
h₄ : (ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν') =ᵐ[ν] 0
h₅ : (ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν =ᵐ[ν] 0
x : α
hx₃ : (μ.singularPart ν').rnDeriv (ν + ν') x = (μ.singularPart ν').rnDeriv ν x
hx₄ : (ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν') x = 0 x
hx₅ : (ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν x = 0 x
⊢ ((μ.singularPart ν').rnDeriv (ν + ν') + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν')) x =
    ((μ.singularPart ν').rnDeriv ν + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν) x

Tactic:
rw [Pi.add_apply, Pi.add_apply, hx₃, hx₄, hx₅]

Goal state after:
Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy

Goal state before:
pp: X : Type u_1
T : X → X
F : Set X
U : SetRel X X
n : ℕ
h_fin : coverMincard T F U n < ⊤
k : ℕ
k_min : ↑k = ⨅ x, ↑(#↑x)
this : Nonempty { s // IsDynCoverOf T F U n ↑s }
key : ⨅ s, ↑(#↑s) ∈ range fun s ↦ ↑(#↑s)
⊢ ∃ s, IsDynCoverOf T F U n ↑s ∧ #s = k

Tactic:
rw [← k_min, mem_range, Subtype.exists] at key

Goal state after:
X : Type u_1
T : X → X
F : Set X
U : SetRel X X
n : ℕ
h_fin : coverMincard T F U n < ⊤
k : ℕ
k_min : ↑k = ⨅ x, ↑(#↑x)
this : Nonempty { s // IsDynCoverOf T F U n ↑s }
key : ∃ a, ∃ (b : IsDynCoverOf T F U n ↑a), ↑(#↑⟨a, b⟩) = ↑k
⊢ ∃ s, IsDynCoverOf T F U n ↑s ∧ #s = k
Module: Mathlib.FieldTheory.IsAlgClosed.Classification

Goal state before:
pp: R : Type u
K : Type v
inst✝⁴ : CommRing R
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsAlgClosed K
ι : Type w
v : ι → K
inst✝ : Nontrivial R
hv : IsTranscendenceBasis R v
hR : #R ≤ ℵ₀
hK : ℵ₀ < #K
h : Cardinal.lift.{max u v, w} #ι < ℵ₀
⊢ Cardinal.lift.{max v w, u} #R ≤ ℵ₀

Tactic:
by simpa

Goal state after:
Module: Mathlib.FieldTheory.IsAlgClosed.Classification

Goal state before:
pp: R : Type u
K : Type v
inst✝⁴ : CommRing R
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsAlgClosed K
ι : Type w
v : ι → K
inst✝ : Nontrivial R
hv : IsTranscendenceBasis R v
hR : #R ≤ ℵ₀
hK : ℵ₀ < #K
this✝ : ℵ₀ ≤ Cardinal.lift.{max u v, w} #ι
this : Cardinal.lift.{max u w, v} #K = Cardinal.lift.{max u v, w} #ι
⊢ Cardinal.lift.{u, max v w} (Cardinal.lift.{w, v} #K) = Cardinal.lift.{u, max v w} (Cardinal.lift.{v, w} #ι)

Tactic:
by simpa

Goal state after:
Module: Mathlib.ModelTheory.Basic

Goal state before:
pp: L : Language
L' : Language
M : Type w
N : Type w'
inst✝³ : L.Structure M
inst✝² : L.Structure N
P : Type u_1
inst✝¹ : L.Structure P
Q : Type u_2
inst✝ : L.Structure Q
a : Language.empty.Structure M
⊢ a = default

Tactic:
ext _ f <;> exact Empty.elim f

Goal state after:
Module: Mathlib.ModelTheory.Algebra.Ring.Basic

Goal state before:
pp: α : Type u_1
R : Type u_2
inst✝⁵ : Add R
inst✝⁴ : Mul R
inst✝³ : Neg R
inst✝² : One R
inst✝¹ : Zero R
inst✝ : CompatibleRing R
x y : ring.Term α
v : α → R
⊢ Term.realize v (x + y) = Term.realize v x + Term.realize v y

Tactic:
simp [add_def, funMap_add]

Goal state after:
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: case inr
M : Type w
α : Type u'
β : Type v'
n m : ℕ
g : α → β ⊕ Fin n
v : β → M
xs : Fin (n + m) → M
x : Fin m
⊢ (Sum.elim v xs ∘ relabelAux g m) (Sum.inr x) = Sum.elim (Sum.elim v (xs ∘ castAdd m) ∘ g) (xs ∘ natAdd n) (Sum.inr x)

Tactic:
simp [BoundedFormula.relabelAux]

Goal state after:
Module: Mathlib.ModelTheory.Substructures

Goal state before:
pp: L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝³ : L.Structure M
inst✝² : L.Structure N
inst✝¹ : L.Structure P
S : L.Substructure M
s : Set M
inst✝ : IsEmpty L.Constants
⊢ IsEmpty ↥⊥

Tactic:
refine (isEmpty_subtype _).2 (fun x => ?_)

Goal state after:
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝³ : L.Structure M
inst✝² : L.Structure N
inst✝¹ : L.Structure P
S : L.Substructure M
s : Set M
inst✝ : IsEmpty L.Constants
x : M
⊢ x ∉ ⊥
Module: Mathlib.ModelTheory.ElementarySubstructures

Goal state before:
pp: L : Language
M : Type u_1
inst✝ : L.Structure M
S : L.ElementarySubstructure M
D : Set M
x : M
hx : x ∈ D
φ : L[[↑↑S]].Formula (Fin 1)
hφ : {x | x 0 ∈ D} = ofPred φ.Realize
hφx : φ.Realize ![x]
ψ : L[[↑↑S]].Sentence := iExs (Fin 1) (relabel Sum.inr φ)
hψM : M ⊨ ψ
v' : Fin 1 → ↥S
hv' :
  (BoundedFormula.constantsVarsEquiv φ).Realize (⇑S.subtype ∘ Sum.elim (fun a ↦ ↑(L.con a)) v') (⇑S.subtype ∘ default)
⊢ φ.Realize (Subtype.val ∘ v')

Tactic:
simp only [Formula.Realize, ← BoundedFormula.realize_constantsVarsEquiv]

Goal state after:
L : Language
M : Type u_1
inst✝ : L.Structure M
S : L.ElementarySubstructure M
D : Set M
x : M
hx : x ∈ D
φ : L[[↑↑S]].Formula (Fin 1)
hφ : {x | x 0 ∈ D} = ofPred φ.Realize
hφx : φ.Realize ![x]
ψ : L[[↑↑S]].Sentence := iExs (Fin 1) (relabel Sum.inr φ)
hψM : M ⊨ ψ
v' : Fin 1 → ↥S
hv' :
  (BoundedFormula.constantsVarsEquiv φ).Realize (⇑S.subtype ∘ Sum.elim (fun a ↦ ↑(L.con a)) v') (⇑S.subtype ∘ default)
⊢ (BoundedFormula.constantsVarsEquiv φ).Realize (Sum.elim (fun a ↦ ↑(L.con a)) (Subtype.val ∘ v')) default
Module: Mathlib.ModelTheory.ElementarySubstructures

Goal state before:
pp: L : Language
M : Type u_1
inst✝ : L.Structure M
S : L.ElementarySubstructure M
D : Set M
x : M
hx : x ∈ D
φ : L[[↑↑S]].Formula (Fin 1)
hφ : {x | x 0 ∈ D} = ofPred φ.Realize
hφx : φ.Realize ![x]
ψ : L[[↑↑S]].Sentence := iExs (Fin 1) (relabel Sum.inr φ)
hψM : M ⊨ ψ
v' : Fin 1 → ↥S
hv' : φ.Realize v'
hv'' : φ.Realize (Subtype.val ∘ v')
⊢ ↑(v' 0) ∈ D

Tactic:
change (Subtype.val ∘ v') ∈ {x | x 0 ∈ D}

Goal state after:
L : Language
M : Type u_1
inst✝ : L.Structure M
S : L.ElementarySubstructure M
D : Set M
x : M
hx : x ∈ D
φ : L[[↑↑S]].Formula (Fin 1)
hφ : {x | x 0 ∈ D} = ofPred φ.Realize
hφx : φ.Realize ![x]
ψ : L[[↑↑S]].Sentence := iExs (Fin 1) (relabel Sum.inr φ)
hψM : M ⊨ ψ
v' : Fin 1 → ↥S
hv' : φ.Realize v'
hv'' : φ.Realize (Subtype.val ∘ v')
⊢ Subtype.val ∘ v' ∈ {x | x 0 ∈ D}
Module: Mathlib.ModelTheory.Definability

Goal state before:
pp: M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
f : (α → M) → M
h : A.TermDefinable L f
⊢ A.Definable L (Function.tupleGraph f)

Tactic:
by
  obtain ⟨φ, rfl⟩ := h
  use (φ.relabel some).equal (Term.var none)
  ext
  simp [Function.tupleGraph]

Goal state after:
Module: Mathlib.ModelTheory.Definability

Goal state before:
pp: M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
B : Set M
f : (α → M) → M
h : A.TermDefinable L f
hAB : A ⊆ B
⊢ B.TermDefinable L f

Tactic:
← termDefinable_empty_withConstants_iff

Goal state after:
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
B : Set M
f : (α → M) → M
h : ∅.TermDefinable L[[↑A]] f
hAB : A ⊆ B
⊢ ∅.TermDefinable L[[↑B]] f
Module: Mathlib.FieldTheory.AxGrothendieck

Goal state before:
pp: case intro
ι : Type u_1
K : Type u_2
R : Type u_3
inst✝⁴ : Field K
inst✝³ : Finite K
inst✝² : CommRing R
inst✝¹ : Finite ι
inst✝ : Algebra K R
alg : Algebra.IsAlgebraic K R
ps : ι → MvPolynomial ι R
S : Set (ι → R)
hm : Set.MapsTo (fun v i ↦ (eval v) (ps i)) S S
hinj : Set.InjOn (fun v i ↦ (eval v) (ps i)) S
is_int : ∀ (x : R), IsIntegral K x
v : ι → R
hvS : v ∈ S
val✝ : Fintype ι
⊢ v ∈ (fun v i ↦ (eval v) (ps i)) '' S

Tactic:
let s : Finset R :=
    (Finset.biUnion (univ : Finset ι) fun i => (ps i).support.image fun x => coeff x (ps i)) ∪
      (univ : Finset ι).image v

Goal state after:
case intro
ι : Type u_1
K : Type u_2
R : Type u_3
inst✝⁴ : Field K
inst✝³ : Finite K
inst✝² : CommRing R
inst✝¹ : Finite ι
inst✝ : Algebra K R
alg : Algebra.IsAlgebraic K R
ps : ι → MvPolynomial ι R
S : Set (ι → R)
hm : Set.MapsTo (fun v i ↦ (eval v) (ps i)) S S
hinj : Set.InjOn (fun v i ↦ (eval v) (ps i)) S
is_int : ∀ (x : R), IsIntegral K x
v : ι → R
hvS : v ∈ S
val✝ : Fintype ι
s : Finset R := (univ.biUnion fun i ↦ image (fun x ↦ coeff x (ps i)) (ps i).support) ∪ image v univ
⊢ v ∈ (fun v i ↦ (eval v) (ps i)) '' S
Module: Mathlib.FieldTheory.Finite.Extension

Goal state before:
pp: case e'_3
k : Type u_1
inst✝⁵ : Field k
inst✝⁴ : Finite k
p : ℕ
inst✝³ : Fact (Nat.Prime p)
inst✝² : CharP k p
n : ℕ
inst✝¹ : NeZero n
inst✝ : Algebra (ZMod p) k
this : Algebra (ZMod p) k := ZMod.algebra k p
⊢ inst✝ = this

Tactic:
subsingleton

Goal state after:
Module: Mathlib.FieldTheory.Differential.Liouville

Goal state before:
pp: F : Type u_1
K : Type u_2
inst✝¹² : Field F
inst✝¹¹ : Field K
inst✝¹⁰ : Differential F
inst✝⁹ : Differential K
inst✝⁸ : Algebra F K
inst✝⁷ : DifferentialAlgebra F K
A : Type u_3
inst✝⁶ : Field A
inst✝⁵ : Algebra K A
inst✝⁴ : Algebra F A
inst✝³ : Differential A
inst✝² : IsScalarTower F K A
inst✝¹ : ContainConstants F K
inst1 : IsLiouville F K
inst2 : IsLiouville K A
a : F
ι : Type
inst✝ : Fintype ι
c : ι → F
hc✝ : ∀ (x : ι), (c x)′ = 0
u : ι → A
v : A
h : ↑a = ∑ x, ↑(c x) * logDeriv (u x) + v′
ι₀ : Type
w✝ : Fintype ι₀
c₀✝ : ι₀ → K
hc₀ : ∀ (x : ι₀), (c₀✝ x)′ = 0
u₀ : ι₀ → K
v₀ : K
h₀ : ↑a = ∑ x, c₀✝ x * logDeriv (u₀ x) + v₀′
c₀ : ι₀ → F
hc : ∀ (x : ι₀), (algebraMap F K) (c₀ x) = c₀✝ x
x✝ : ι₀
⊢ (c₀ x✝)′ = 0

Tactic:
apply_fun ((↑) : F → K)

Goal state after:
F : Type u_1
K : Type u_2
inst✝¹² : Field F
inst✝¹¹ : Field K
inst✝¹⁰ : Differential F
inst✝⁹ : Differential K
inst✝⁸ : Algebra F K
inst✝⁷ : DifferentialAlgebra F K
A : Type u_3
inst✝⁶ : Field A
inst✝⁵ : Algebra K A
inst✝⁴ : Algebra F A
inst✝³ : Differential A
inst✝² : IsScalarTower F K A
inst✝¹ : ContainConstants F K
inst1 : IsLiouville F K
inst2 : IsLiouville K A
a : F
ι : Type
inst✝ : Fintype ι
c : ι → F
hc✝ : ∀ (x : ι), (c x)′ = 0
u : ι → A
v : A
h : ↑a = ∑ x, ↑(c x) * logDeriv (u x) + v′
ι₀ : Type
w✝ : Fintype ι₀
c₀✝ : ι₀ → K
hc₀ : ∀ (x : ι₀), (c₀✝ x)′ = 0
u₀ : ι₀ → K
v₀ : K
h₀ : ↑a = ∑ x, c₀✝ x * logDeriv (u₀ x) + v₀′
c₀ : ι₀ → F
hc : ∀ (x : ι₀), (algebraMap F K) (c₀ x) = c₀✝ x
x✝ : ι₀
⊢ ↑(c₀ x✝)′ = ↑0

case inj
F : Type u_1
K : Type u_2
inst✝¹² : Field F
inst✝¹¹ : Field K
inst✝¹⁰ : Differential F
inst✝⁹ : Differential K
inst✝⁸ : Algebra F K
inst✝⁷ : DifferentialAlgebra F K
A : Type u_3
inst✝⁶ : Field A
inst✝⁵ : Algebra K A
inst✝⁴ : Algebra F A
inst✝³ : Differential A
inst✝² : IsScalarTower F K A
inst✝¹ : ContainConstants F K
inst1 : IsLiouville F K
inst2 : IsLiouville K A
a : F
ι : Type
inst✝ : Fintype ι
c : ι → F
hc✝ : ∀ (x : ι), (c x)′ = 0
u : ι → A
v : A
h : ↑a = ∑ x, ↑(c x) * logDeriv (u x) + v′
ι₀ : Type
w✝ : Fintype ι₀
c₀✝ : ι₀ → K
hc₀ : ∀ (x : ι₀), (c₀✝ x)′ = 0
u₀ : ι₀ → K
v₀ : K
h₀ : ↑a = ∑ x, c₀✝ x * logDeriv (u₀ x) + v₀′
c₀ : ι₀ → F
hc : ∀ (x : ι₀), (algebraMap F K) (c₀ x) = c₀✝ x
x✝ : ι₀
⊢ Function.Injective Algebra.cast
Module: Mathlib.FieldTheory.IsPerfectClosure

Goal state before:
pp: case refine_1
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 ∈ Ideal.comap i (pNilradical L p)
n : ℕ
h : i x ^ p ^ n = 0
⊢ ∃ n, x ^ p ^ n = 0

Tactic:
obtain ⟨m, h⟩ := mem_pNilradical.1 <| ker_le i p ((map_pow i x _).symm ▸ h)

Goal state after:
case refine_1
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 ∈ Ideal.comap i (pNilradical L p)
n : ℕ
h✝ : i x ^ p ^ n = 0
m : ℕ
h : (x ^ p ^ n) ^ p ^ m = 0
⊢ ∃ n, x ^ p ^ n = 0
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
s : E
hs : s ∈ S
⊢ Polynomial.map (algebraMap F K') (minpoly F s) ∣ Polynomial.map (algebraMap K p.SplittingField) p

Tactic:
rw [IsScalarTower.algebraMap_eq F K K', ← Polynomial.map_map, map_dvd_map']

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
s : E
hs : s ∈ S
⊢ Polynomial.map (algebraMap F K) (minpoly F s) ∣ p
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
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x✝ : PerfectClosure K p
x : ℕ × K
⊢ (of K p) x.2 = (⇑(frobenius (PerfectClosure K p) p))^[x.1] (mk K p x)

Tactic:
iterate_frobenius_mk K p x.1 x.2

Goal state after:
K : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x✝ : PerfectClosure K p
x : ℕ × K
⊢ (of K p) x.2 = (of K p) x.2
Module: Mathlib.GroupTheory.CosetCover

Goal state before:
pp: case mpr
G : Type u_1
inst✝¹ : Group G
D H : Subgroup G
inst✝ : D.FiniteIndex
hD_le_H : D ≤ H
t : Set ↥H
ht : IsComplement t ↑(D.subgroupOf H) ∧ 1 ∈ t
hf : t.Finite
x : G
hx : x ∈ H
⊢ ∃ y ∈ t, ∃ d ∈ D, ↑y * d = x

Tactic:
exact ⟨_, (ht.1.toLeftFun ⟨x, hx⟩).2, _,
      ht.1.inv_toLeftFun_mul_mem ⟨x, hx⟩, mul_inv_cancel_left _ _⟩

Goal state after:
Module: Mathlib.FieldTheory.PerfectClosure

Goal state before:
pp: K : Type u
inst✝² : Field K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
e : PerfectClosure K p
x✝ : ℕ × K
m : ℕ
x : K
H : mk K p (m, x) ≠ 0
this : ¬(⇑(frobenius K p))^[(0, 0).1] (m, x).2 = (⇑(frobenius K p))^[(m, x).1] (0, 0).2
⊢ (⇑(frobenius K p))^[(0, 1).1]
      ((m, x).1 + ((m, x).1, (m, x).2⁻¹).1,
          (⇑(frobenius K p))^[((m, x).1, (m, x).2⁻¹).1] (m, x).2 *
            (⇑(frobenius K p))^[(m, x).1] ((m, x).1, (m, x).2⁻¹).2).2 =
    (⇑(frobenius K
            p))^[((m, x).1 + ((m, x).1, (m, x).2⁻¹).1,
            (⇑(frobenius K p))^[((m, x).1, (m, x).2⁻¹).1] (m, x).2 *
              (⇑(frobenius K p))^[(m, x).1] ((m, x).1, (m, x).2⁻¹).2).1]
      (0, 1).2

Tactic:
simp only [iterate_map_one, iterate_map_zero, iterate_zero_apply, ← iterate_map_mul] at this ⊢

Goal state after:
K : Type u
inst✝² : Field K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
e : PerfectClosure K p
x✝ : ℕ × K
m : ℕ
x : K
H : mk K p (m, x) ≠ 0
this : ¬x = 0
⊢ (⇑(frobenius K p))^[m] (x * x⁻¹) = 1
Module: Mathlib.GroupTheory.CosetCover

Goal state before:
pp: case pos
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq (Subgroup G)
n : ℕ
ih :
  ∀ m < n,
    ∀ {ι : Type u_2} {H : ι → Subgroup G} {g : ι → G} {s : Finset ι},
      ⋃ i ∈ s, g i • ↑(H i) = Set.univ →
        ∀ j ∈ s,
          ⋃ i ∈ {x ∈ s | H x = H j}, g i • ↑(H i) ≠ Set.univ →
            m = (Finset.image H s).card → ∃ i ∈ s, H i ≠ H j ∧ (H i).FiniteIndex
ι : Type u_2
H : ι → Subgroup G
g : ι → G
s : Finset ι
j : ι
hj : j ∈ s
hcovers'✝ : ⋃ i ∈ {x ∈ s | H x = H j}, g i • ↑(H i) ≠ Set.univ
hn : n = (Finset.image H s).card
x : G
hx : ∀ (y : G), y • ↑(H j) ⊆ ⋃ i ∈ {x ∈ s | H x ≠ H j}, (y * x⁻¹ * g i) • ↑(H i)
κ : Type u_2 := ↥({x ∈ s | H x ≠ H j}) × Option ↥({x ∈ s | H x = H j})
f : κ → G :=
  fun x_1 ↦
    match x_1 with
    | (k₁, some k₂) => g ↑k₂ * x⁻¹ * g ↑k₁
    | (k₁, none) => g ↑k₁
K : κ → Subgroup G := fun k ↦ H ↑k.1
hK' : ∀ (k : κ), K k ∈ (Finset.image H s).erase (H j)
hK : ∀ (k : κ), K k ≠ H j
hcovers : ⋃ k ∈ Finset.univ, f k • ↑(K k) = Set.univ
k : κ
hcovers' : ⋃ i ∈ {x | K x = K k}, f i • ↑(K i) = Set.univ
⊢ ∃ i ∈ s, H i ≠ H j ∧ (H i).FiniteIndex

Tactic:
Set.iUnion₂_congr fun i hi => by rw [(Finset.mem_filter.mp hi).right]

Goal state after:
case pos
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq (Subgroup G)
n : ℕ
ih :
  ∀ m < n,
    ∀ {ι : Type u_2} {H : ι → Subgroup G} {g : ι → G} {s : Finset ι},
      ⋃ i ∈ s, g i • ↑(H i) = Set.univ →
        ∀ j ∈ s,
          ⋃ i ∈ {x ∈ s | H x = H j}, g i • ↑(H i) ≠ Set.univ →
            m = (Finset.image H s).card → ∃ i ∈ s, H i ≠ H j ∧ (H i).FiniteIndex
ι : Type u_2
H : ι → Subgroup G
g : ι → G
s : Finset ι
j : ι
hj : j ∈ s
hcovers'✝ : ⋃ i ∈ {x ∈ s | H x = H j}, g i • ↑(H i) ≠ Set.univ
hn : n = (Finset.image H s).card
x : G
hx : ∀ (y : G), y • ↑(H j) ⊆ ⋃ i ∈ {x ∈ s | H x ≠ H j}, (y * x⁻¹ * g i) • ↑(H i)
κ : Type u_2 := ↥({x ∈ s | H x ≠ H j}) × Option ↥({x ∈ s | H x = H j})
f : κ → G :=
  fun x_1 ↦
    match x_1 with
    | (k₁, some k₂) => g ↑k₂ * x⁻¹ * g ↑k₁
    | (k₁, none) => g ↑k₁
K : κ → Subgroup G := fun k ↦ H ↑k.1
hK' : ∀ (k : κ), K k ∈ (Finset.image H s).erase (H j)
hK : ∀ (k : κ), K k ≠ H j
hcovers : ⋃ k ∈ Finset.univ, f k • ↑(K k) = Set.univ
k : κ
hcovers' : ⋃ i ∈ {x | K x = K k}, f i • ↑(K k) = Set.univ
⊢ ∃ i ∈ s, H i ≠ H j ∧ (H i).FiniteIndex
Module: Mathlib.GroupTheory.CosetCover

Goal state before:
pp: case pos
G : Type u_1
inst✝ : Group G
ι : Type u_2
H : ι → Subgroup G
g : ι → G
s : Finset ι
hcovers : ⋃ i ∈ s, g i • ↑(H i) = Set.univ
j : ι
hj : j ∈ s
hcovers' : ⋃ i ∈ {x ∈ s | H x = H j}, g i • ↑(H i) = Set.univ
⊢ ∃ k ∈ s, (H k).FiniteIndex

Tactic:
Set.iUnion₂_congr fun i hi => by rw [(Finset.mem_filter.mp hi).right]

Goal state after:
case pos
G : Type u_1
inst✝ : Group G
ι : Type u_2
H : ι → Subgroup G
g : ι → G
s : Finset ι
hcovers : ⋃ i ∈ s, g i • ↑(H i) = Set.univ
j : ι
hj : j ∈ s
hcovers' : ⋃ i ∈ {x ∈ s | H x = H j}, g i • ↑(H j) = Set.univ
⊢ ∃ k ∈ s, (H k).FiniteIndex
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:
rw [(X_pow_sub_C_splits_of_isPrimitiveRoot hζ e).eq_prod_roots_of_monic
    (monic_X_pow_sub_C _ hn.ne'), ← nthRoots, hζ.nthRoots_eq e, Multiset.map_map]

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) ∘ fun x ↦ ζ ^ x * α) (Multiset.range n)).prod =
    ∏ i ∈ Finset.range n, (X - C (ζ ^ i * α))
Module: Mathlib.FieldTheory.NormalizedTrace

Goal state before:
pp: F : Type u_3
E : Type u_4
K : Type u_5
inst✝¹² : Field F
inst✝¹¹ : Field E
inst✝¹⁰ : Field K
inst✝⁹ : Algebra F E
inst✝⁸ : Algebra E K
inst✝⁷ : Algebra F K
inst✝⁶ : IsScalarTower F E K
inst✝⁵ : Algebra.IsIntegral F E
inst✝⁴ : Algebra.IsIntegral F K
inst✝³ : CharZero F
inst✝² : FiniteDimensional F E
inst✝¹ : Algebra.IsIntegral E K
inst✝ : CharZero E
a : K
this : FiniteDimensional E ↥E⟮a⟯
⊢ (normalizedTrace F E) ((↑(Module.finrank E ↥E⟮a⟯))⁻¹ • (trace E ↥E⟮a⟯) (AdjoinSimple.gen E a)) =
    (normalizedTrace F K) a

Tactic:
map_smul,

Goal state after:
F : Type u_3
E : Type u_4
K : Type u_5
inst✝¹² : Field F
inst✝¹¹ : Field E
inst✝¹⁰ : Field K
inst✝⁹ : Algebra F E
inst✝⁸ : Algebra E K
inst✝⁷ : Algebra F K
inst✝⁶ : IsScalarTower F E K
inst✝⁵ : Algebra.IsIntegral F E
inst✝⁴ : Algebra.IsIntegral F K
inst✝³ : CharZero F
inst✝² : FiniteDimensional F E
inst✝¹ : Algebra.IsIntegral E K
inst✝ : CharZero E
a : K
this : FiniteDimensional E ↥E⟮a⟯
⊢ (↑(Module.finrank E ↥E⟮a⟯))⁻¹ • (normalizedTrace F E) ((trace E ↥E⟮a⟯) (AdjoinSimple.gen E a)) =
    (normalizedTrace F K) a
Module: Mathlib.FieldTheory.PurelyInseparable.Exponent

Goal state before:
pp: K : Type u_2
L : Type u_3
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsPurelyInseparable K L
a : L
this : (aeval a) (X ^ ringExpChar K ^ elemExponent K a - C (elemReduct K a)) = 0
⊢ (algebraMap K L) (elemReduct K a) = a ^ ringExpChar K ^ elemExponent K a

Tactic:
rwa [map_sub, aeval_C, map_pow, aeval_X, sub_eq_zero, eq_comm] at this

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

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
i : E →ₐ[F] K
x : E
⊢ x ∈ comap i (perfectClosure F K) ↔ x ∈ perfectClosure F E

Tactic:
exact map_mem_perfectClosure_iff i

Goal state after: