mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Dynamics.Flow

Goal state before:
pp: τ : Type u_1
α : Type u_2
ϕ : τ → α → α
s : Set α
⊢ (∀ (t : τ), MapsTo (ϕ t) s s) ↔ ∀ (t : τ), ϕ t '' s ⊆ s

Tactic:
mapsTo_iff_image_subset

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

Goal state before:
pp: A : Type u_1
inst✝⁴ : TopologicalSpace A
inst✝³ : Inhabited A
G : Type u_2
inst✝² : Monoid G
inst✝¹ : IsLeftCancelMul G
inst✝ : DiscreteTopology A
p : Pattern A G
g : G
⊢ IsOpen[Pi.topologicalSpace] {x | p.mulOccursInAt x g}

Tactic:
simpa [mulOccursInAt_eq_cylinder] using isOpen_cylinder _ _

Goal state after:
Module: Mathlib.Dynamics.OmegaLimit

Goal state before:
pp: case mp
τ : Type u_1
α : Type u_2
β : Type u_3
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s₁ s₂ : Set α
y : β
⊢ ((∃ n ∈ 𝓝 y, ∀ᶠ (x : τ) in f, s₁ ∩ ϕ x ⁻¹' n = ∅) ∧ ∃ n ∈ 𝓝 y, ∀ᶠ (x : τ) in f, s₂ ∩ ϕ x ⁻¹' n = ∅) →
    ∃ n ∈ 𝓝 y, (∀ᶠ (x : τ) in f, s₁ ∩ ϕ x ⁻¹' n = ∅) ∧ ∀ᶠ (x : τ) in f, s₂ ∩ ϕ x ⁻¹' n = ∅

Tactic:
simp only [← subset_empty_iff]

Goal state after:
case mp
τ : Type u_1
α : Type u_2
β : Type u_3
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s₁ s₂ : Set α
y : β
⊢ ((∃ n ∈ 𝓝 y, ∀ᶠ (x : τ) in f, s₁ ∩ ϕ x ⁻¹' n ⊆ ∅) ∧ ∃ n ∈ 𝓝 y, ∀ᶠ (x : τ) in f, s₂ ∩ ϕ x ⁻¹' n ⊆ ∅) →
    ∃ n ∈ 𝓝 y, (∀ᶠ (x : τ) in f, s₁ ∩ ϕ x ⁻¹' n ⊆ ∅) ∧ ∀ᶠ (x : τ) in f, s₂ ∩ ϕ x ⁻¹' n ⊆ ∅
Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy

Goal state before:
pp: case inr
X : Type u_1
T : X → X
U : SetRel X X
F : Set X
m : ℕ
F_inv : MapsTo T F F
inst✝ : U.IsSymm
n : ℕ
s : Finset X
h : IsDynCoverOf T F U m ↑s
x✝ : Nonempty X
s_nemp : (↑s).Nonempty
x : X
x_F : x ∈ F
m_pos : m > 0
t : Fin n → ↥s
y : X
y_int : y ∈ ⋂ k, T^[m * ↑k] ⁻¹' ball (↑(t k)) (dynEntourage T U m)
z : X
z_int : z ∈ ⋂ k, T^[m * ↑k] ⁻¹' ball (↑(t k)) (dynEntourage T U m)
⊢ z ∈ ball y (dynEntourage T (U ○ U) (m * n))

Tactic:
simp only [ball, dynEntourage, Prod.map_iterate, mem_iInter, Set.mem_preimage, Prod.map_apply,
        mem_comp] at y_int z_int ⊢

Goal state after:
case inr
X : Type u_1
T : X → X
U : SetRel X X
F : Set X
m : ℕ
F_inv : MapsTo T F F
inst✝ : U.IsSymm
n : ℕ
s : Finset X
h : IsDynCoverOf T F U m ↑s
x✝ : Nonempty X
s_nemp : (↑s).Nonempty
x : X
x_F : x ∈ F
m_pos : m > 0
t : Fin n → ↥s
y z : X
y_int : ∀ (i : Fin n), ∀ i_1 < m, (T^[i_1] ↑(t i), T^[i_1] (T^[m * ↑i] y)) ∈ U
z_int : ∀ (i : Fin n), ∀ i_1 < m, (T^[i_1] ↑(t i), T^[i_1] (T^[m * ↑i] z)) ∈ U
⊢ ∀ i < m * n, ∃ b, (T^[i] y, b) ∈ U ∧ (b, T^[i] z) ∈ U
Module: Mathlib.Dynamics.TopologicalEntropy.Semiconj

Goal state before:
pp: case a
X : Type u_1
Y : Type u_2
u : UniformSpace Y
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F : Set X
this : UniformSpace X := ⋯
⊢ coverEntropyInf S F ≤ coverEntropyInf T (φ '' F)

Tactic:
· refine iSup₂_le fun U U_uni ↦ ?_
    simp only [uniformity_comap φ, mem_comap] at U_uni
    obtain ⟨V, V_uni, V_sub⟩ := U_uni
    obtain ⟨W, W_uni, W_symm, W_V⟩ := comp_symm_mem_uniformity_sets V_uni
    apply (coverEntropyInfEntourage_antitone S F ((preimage_mono W_V).trans V_sub)).trans
    apply (le_coverEntropyInfEntourage_image h F).trans
    exact coverEntropyInfEntourage_le_coverEntropyInf T (φ '' F) W_uni

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

Goal state before:
pp: case h
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : SigmaFinite μ
s : Set α
hμs : μ s ≠ ∞
t : Set α := ⋯
ht : t = toMeasurable μ s
ht_m : MeasurableSet t
hμt : μ t ≠ ∞
⊢ ν.withDensity (μ.rnDeriv ν) ≤ μ

Tactic:
apply withDensity_rnDeriv_le

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

Goal state before:
pp: case refine_3
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
mβ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
hμν : μ ≪ ν
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
s : Set α
x✝¹ : MeasurableSet s
x✝ : ν s < ∞
hs_eq : s = f ⁻¹' f '' s
this : SigmaFinite (map f ν)
⊢ ∫⁻ (a : β), (map f μ).rnDeriv (map f ν) a ∂map f (ν.restrict s) = μ s

Tactic:
rw [hs_eq, ← hf.restrict_map, Measure.setLIntegral_rnDeriv (hf.absolutelyContinuous_map hμν),
    hf.map_apply]

Goal state after:
Module: Mathlib.FieldTheory.AbelRuffini

Goal state before:
pp: F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
x y z : E
hx : x ∈ solvableByRad F E
hy : y ∈ solvableByRad F E
hz : z ∈ solvableByRad F E
hx' : Group.IsSolvable (minpoly F x).Gal
hy' : Group.IsSolvable (minpoly F y).Gal
hz' : z ∈ F⟮x, y⟯
p : F[X] := minpoly F x
q : F[X] := minpoly F y
hpq :
  (Polynomial.map (algebraMap F (p * q).SplittingField) (minpoly F x)).Splits ∧
    (Polynomial.map (algebraMap F (p * q).SplittingField) (minpoly F y)).Splits
f : ↥F⟮x, y⟯ →ₐ[F] (p * q).SplittingField
⊢ f ((aeval ⟨z, hz'⟩) (minpoly F z)) = 0

Tactic:
map_eq_zero

Goal state after:
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
x y z : E
hx : x ∈ solvableByRad F E
hy : y ∈ solvableByRad F E
hz : z ∈ solvableByRad F E
hx' : Group.IsSolvable (minpoly F x).Gal
hy' : Group.IsSolvable (minpoly F y).Gal
hz' : z ∈ F⟮x, y⟯
p : F[X] := minpoly F x
q : F[X] := minpoly F y
hpq :
  (Polynomial.map (algebraMap F (p * q).SplittingField) (minpoly F x)).Splits ∧
    (Polynomial.map (algebraMap F (p * q).SplittingField) (minpoly F y)).Splits
f : ↥F⟮x, y⟯ →ₐ[F] (p * q).SplittingField
⊢ (aeval ⟨z, hz'⟩) (minpoly F z) = 0
Module: Mathlib.ModelTheory.Algebra.Field.CharP

Goal state before:
pp: K : Type u_1
inst✝¹ : CommRing K
inst✝ : CompatibleRing K
n : ℕ
v : Empty → K
⊢ Formula.Realize (eqZero n) v ↔ ↑n = 0

Tactic:
simp [eqZero]

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : CompatibleRing K
⊢ ∀ φ ∈ Theory.field, K ⊨ φ

Tactic:
by
      simp only [Theory.field, Set.mem_range, exists_imp]
      rintro φ a rfl
      rw [a.realize_toSentence_iff_toProp (K := K)]
      cases a with
      | existsPairNE => exact exists_pair_ne K
      | existsInv => exact fun x hx0 => ⟨x⁻¹, mul_inv_cancel₀ hx0⟩
      | addAssoc => exact add_assoc
      | zeroAdd => exact zero_add
      | negAddCancel => exact neg_add_cancel
      | mulAssoc => exact mul_assoc
      | mulComm => exact mul_comm
      | oneMul => exact one_mul
      | leftDistrib => exact mul_add

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case e_v
L : Language
M : Type w
inst✝² : L.Structure M
α : Type u'
β : Type v'
inst✝¹ : L[[α]].Structure M
inst✝ : (L.lhomWithConstants α).IsExpansionOn M
n : ℕ
t : L[[α]].Term (β ⊕ Fin n)
v : β → M
xs : Fin n → M
x : α ⊕ β ⊕ Fin n
⊢ (Sum.elim (Sum.elim (fun a ↦ ↑(L.con a)) v) xs ∘ ⇑(Equiv.sumAssoc α β (Fin n)).symm) x =
    Sum.elim (fun a ↦ ↑(L.con a)) (Sum.elim v xs) x

Tactic:
rcases x with (a | (b | i))

Goal state after:
case e_v.inl
L : Language
M : Type w
inst✝² : L.Structure M
α : Type u'
β : Type v'
inst✝¹ : L[[α]].Structure M
inst✝ : (L.lhomWithConstants α).IsExpansionOn M
n : ℕ
t : L[[α]].Term (β ⊕ Fin n)
v : β → M
xs : Fin n → M
a : α
⊢ (Sum.elim (Sum.elim (fun a ↦ ↑(L.con a)) v) xs ∘ ⇑(Equiv.sumAssoc α β (Fin n)).symm) (Sum.inl a) =
    Sum.elim (fun a ↦ ↑(L.con a)) (Sum.elim v xs) (Sum.inl a)

case e_v.inr.inl
L : Language
M : Type w
inst✝² : L.Structure M
α : Type u'
β : Type v'
inst✝¹ : L[[α]].Structure M
inst✝ : (L.lhomWithConstants α).IsExpansionOn M
n : ℕ
t : L[[α]].Term (β ⊕ Fin n)
v : β → M
xs : Fin n → M
b : β
⊢ (Sum.elim (Sum.elim (fun a ↦ ↑(L.con a)) v) xs ∘ ⇑(Equiv.sumAssoc α β (Fin n)).symm) (Sum.inr (Sum.inl b)) =
    Sum.elim (fun a ↦ ↑(L.con a)) (Sum.elim v xs) (Sum.inr (Sum.inl b))

case e_v.inr.inr
L : Language
M : Type w
inst✝² : L.Structure M
α : Type u'
β : Type v'
inst✝¹ : L[[α]].Structure M
inst✝ : (L.lhomWithConstants α).IsExpansionOn M
n : ℕ
t : L[[α]].Term (β ⊕ Fin n)
v : β → M
xs : Fin n → M
i : Fin n
⊢ (Sum.elim (Sum.elim (fun a ↦ ↑(L.con a)) v) xs ∘ ⇑(Equiv.sumAssoc α β (Fin n)).symm) (Sum.inr (Sum.inr i)) =
    Sum.elim (fun a ↦ ↑(L.con a)) (Sum.elim v xs) (Sum.inr (Sum.inr i))
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case pos
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
n n' m : ℕ
v : α → M
k : ℕ
f✝ : L.BoundedFormula α (k + 1)
ih3 :
  ∀ {xs : Fin (k + 1 + n') → M},
    m ≤ k + 1 →
      ((mapTermRel (fun x t ↦ Term.liftAt n' m t) (fun x ↦ id) (fun x ↦ castLE ⋯) f✝).Realize v xs ↔
        f✝.Realize v (xs ∘ fun i ↦ if ↑i < m then castAdd n' i else i.addNat n'))
xs : Fin (k + n') → M
hmn : m ≤ k
h : k + 1 + n' = k + n' + 1
x : M
h✝ : k < m
⊢ k = k + n'

Tactic:
lia

Goal state after:
Module: Mathlib.ModelTheory.Substructures

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
ι : Type u_3
hι : Nonempty ι
S : ι → L.Substructure M
hS : Directed (fun x1 x2 ↦ x1 ≤ x2) S
x : M
⊢ x ∈ ⨆ i, S i ↔ ∃ i, x ∈ S i

Tactic:
refine ⟨?_, fun ⟨i, hi⟩ ↦ le_iSup S i hi⟩
  suffices x ∈ closure L (⋃ i, (S i : Set M)) → ∃ i, x ∈ S i by
    simpa only [closure_iUnion, closure_eq (S _)] using this
  refine fun hx ↦ closure_induction hx (fun _ ↦ mem_iUnion.1) (fun f v hC ↦ ?_)
  simp_rw [Set.mem_ofPred] at *
  have ⟨i, hi⟩ := hS.finite_le (fun i ↦ Classical.choose (hC i))
  refine ⟨i, (S i).fun_mem f v (fun j ↦ hi j (Classical.choose_spec (hC j)))⟩

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
L' : Language
M : Type w
inst✝² : L.Structure M
α : Type u'
inst✝¹ : L'.Structure M
φ : L →ᴸ L'
inst✝ : φ.IsExpansionOn M
ψ : L.Formula α
⊢ Set.ofPred (φ.onFormula ψ).Realize = Set.ofPred ψ.Realize

Tactic:
ext
  simp

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
n : ℕ
φ : L.BoundedFormula α n
v : α → M
⊢ φ.alls.Realize v ↔ ∀ (xs : Fin n → M), φ.Realize v xs

Tactic:
induction n with
  | zero => exact Unique.forall_iff.symm
  | succ n ih =>
    simp only [alls, ih, Realize]
    exact ⟨fun h xs => Fin.snoc_init_self xs ▸ h _ _, fun h xs x => h (Fin.snoc xs x)⟩

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
L' : Language
inst✝¹ : L'.Structure M
φ : L →ᴸ L'
inst✝ : φ.IsExpansionOn M
S : L'.Substructure M
n : ℕ
f : L.Functions n
x : Fin n → M
hx : ∀ (i : Fin n), x i ∈ ↑S
⊢ funMap f x ∈ ↑S

Tactic:
have h := S.fun_mem (φ.onFunction f) x hx

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
L' : Language
inst✝¹ : L'.Structure M
φ : L →ᴸ L'
inst✝ : φ.IsExpansionOn M
S : L'.Substructure M
n : ℕ
f : L.Functions n
x : Fin n → M
hx : ∀ (i : Fin n), x i ∈ ↑S
h : funMap (φ.onFunction f) x ∈ ↑S
⊢ funMap f x ∈ ↑S
Module: Mathlib.ModelTheory.Substructures

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
S : L.Substructure M
A : Set M
h : A ⊆ ↑S
⊢ (L.lhomWithConstants ↑A).substructureReduct (S.withConstants h) = S

Tactic:
ext
  simp

Goal state after:
Module: Mathlib.ModelTheory.Substructures

Goal state before:
pp: L : Language
M : Type w
N : Type u_1
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M →[L] N
⊢ f.range = Substructure.map f ⊤

Tactic:
ext
  simp

Goal state after:
Module: Mathlib.ModelTheory.Substructures

Goal state before:
pp: L : Language
M : Type w
N : Type u_1
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M →[L] N
p : L.Substructure N
⊢ f.range ≤ p ↔ comap f p = ⊤

Tactic:
rw [range_eq_map, map_le_iff_le_comap, eq_top_iff]

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₁
ι : Type u_2
f : ι → Set (α → M)
hf : ∀ (i : ι), A.Definable L (f i)
s : Finset ι
⊢ A.Definable L (⋃ i ∈ s, f i)

Tactic:
rw [← Finset.sup_set_eq_biUnion]

Goal state after:
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
ι : Type u_2
f : ι → Set (α → M)
hf : ∀ (i : ι), A.Definable L (f i)
s : Finset ι
⊢ A.Definable L (s.sup f)
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 : α → β
inst✝¹ : Finite α
inst✝ : Finite β
⊢ A.Definable L ((fun g ↦ g ∘ f) '' s)

Tactic:
cases nonempty_fintype α

Goal state after:
case intro
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 : α → β
inst✝¹ : Finite α
inst✝ : Finite β
val✝ : Fintype α
⊢ A.Definable L ((fun g ↦ g ∘ f) '' s)
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
inst✝ : DecidableEq α
φ : L.Formula α
⊢ M ⊨ φ.exClosure ↔ ∃ v, Realize (BoundedFormula.restrictFreeVar φ id) v

Tactic:
simp [Sentence.Realize, Formula.exClosure, Formula.realize_iExs]

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
r : L.Relations 2
⊢ M ⊨ r.transitive ↔ IsTrans M fun x y ↦ RelMap r ![x, y]

Tactic:
rw [isTrans_def]

Goal state after:
L : Language
M : Type w
inst✝ : L.Structure M
r : L.Relations 2
⊢ M ⊨ r.transitive ↔ ∀ ⦃a b c : M⦄, RelMap r ![a, b] → RelMap r ![b, c] → RelMap r ![a, c]
Module: Mathlib.ModelTheory.Algebra.Field.IsAlgClosed

Goal state before:
pp: case h2
p : ℕ
hp : Nat.Prime p ∨ p = 0
⊢ Cardinal.lift.{0, 0} Language.ring.card ≤ Cardinal.lift.{0, 0} (Order.succ ℵ₀)

pp: case hS
p : ℕ
hp : Nat.Prime p ∨ p = 0
⊢ (Theory.ACF p).IsSatisfiable

pp: case hT
p : ℕ
hp : Nat.Prime p ∨ p = 0
⊢ ∀ (M : (Theory.ACF p).ModelType), Infinite ↑M

Tactic:
· simp only [card_ring, lift_id']
    exact le_trans (le_of_lt (lt_aleph0_of_finite _)) (Order.le_succ _)

Goal state after:
case hS
p : ℕ
hp : Nat.Prime p ∨ p = 0
⊢ (Theory.ACF p).IsSatisfiable

case hT
p : ℕ
hp : Nat.Prime p ∨ p = 0
⊢ ∀ (M : (Theory.ACF p).ModelType), Infinite ↑M
Module: Mathlib.ModelTheory.Algebra.Field.IsAlgClosed

Goal state before:
pp: φ : Language.ring.Sentence
T0 : Finset Language.ring.Sentence
hT0 : ↑T0 ⊆ Theory.ACF 0
h : ↑T0 ⊨ᵇ φ
ψ : Language.ring.Sentence
hψ : ψ ∈ Theory.ACF 0
⊢ { s // ∀ q ∉ s, Theory.ACF ↑q ⊨ᵇ ψ }

Tactic:
rw [Theory.ACF, Theory.fieldOfChar, Set.union_right_comm, Set.mem_union, if_pos rfl,
      Set.mem_image] at hψ

Goal state after:
φ : Language.ring.Sentence
T0 : Finset Language.ring.Sentence
hT0 : ↑T0 ⊆ Theory.ACF 0
h : ↑T0 ⊨ᵇ φ
ψ : Language.ring.Sentence
hψ : ψ ∈ Theory.field ∪ genericMonicPolyHasRoot '' {n | 0 < n} ∨ ∃ x ∈ {q | Nat.Prime q}, ∼(eqZero x) = ψ
⊢ { s // ∀ q ∉ s, Theory.ACF ↑q ⊨ᵇ ψ }
Module: Mathlib.FieldTheory.Cardinality

Goal state before:
pp: case inl
α : Type u
h : Fintype α
⊢ Nonempty (Field α) ↔ ℵ₀ ≤ #α ∨ ∃ n, #α = ↑n ∧ IsPrimePow n

Tactic:
simpa only [Cardinal.mk_fintype, Nat.cast_inj, exists_eq_left',
      Cardinal.natCast_lt_aleph0.not_ge, false_or] using Fintype.nonempty_field_iff

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

Goal state before:
pp: case refine_2
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
inst✝³ : CharZero F
inst✝² : FiniteDimensional F K
inst✝¹ : IsGalois F K
a : F
ι : Type
inst✝ : Fintype ι
c : ι → F
hc : ∀ (x : ι), (c x)′ = 0
u : ι → K
v : K
h : ↑a = ∑ x, ↑(c x) * logDeriv (u x) + v′
this : CharZero K
c₀ : ι → F := fun i ↦ c i / ↑(Fintype.card Gal(K/F))
u₁ : ι → K := fun i ↦ ∏ x, x (u i)
ffb : fixedField ⊤ = ⊥
u₀ : ι → F
hu₀ : ∀ (i : ι), (algebraMap F K) (u₀ i) = u₁ i
v₁ : K := (∑ x, x v) / ↑(Fintype.card Gal(K/F))
v₀ : F
hv₀ : (algebraMap F K) v₀ = v₁
⊢ a = ∑ x, c₀ x * logDeriv (u₀ x) + v₀′

Tactic:
· -- Proving that this works is mostly straightforward algebraic manipulation,
      apply_fun (algebraMap F K)
      case inj =>
        exact FaithfulSMul.algebraMap_injective F K
      simp only [map_add, map_sum, map_mul, ← logDeriv_algebraMap, hu₀, ← deriv_algebraMap, hv₀]
      unfold u₁ v₁ c₀
      clear c₀ u₁ u₀ hu₀ v₁ v₀ hv₀
      push_cast
      rw [Derivation.leibniz_div_const, smul_eq_mul, inv_mul_eq_div]
      case h => simp
      simp only [map_sum, div_mul_eq_mul_div]
      rw [← sum_div, ← add_div]
      field_simp
      -- Here we rewrite logDeriv (∏ x : K ≃ₐ[F] K, x (u i)) to ∑ x : K ≃ₐ[F] K, logDeriv (x (u i))
      conv =>
        enter [2, 1, 2, i, 2]
        equals ∑ x : K ≃ₐ[F] K, logDeriv (x (u i)) =>
          by_cases h : u i = 0 <;>
          simp [logDeriv_prod, h]
      simp_rw [mul_sum]
      rw [sum_comm, ← sum_add_distrib]
      trans ∑ _ : (K ≃ₐ[F] K), a
      · simp [mul_comm]
      · rcongr e
        apply_fun e at h
        simp only [AlgEquiv.commutes, map_add, map_sum, map_mul] at h
        convert! h using 2
        · rcongr x
          simp [logDeriv, algEquiv_deriv']
        · rw [algEquiv_deriv']

Goal state after:
Module: Mathlib.FieldTheory.IntermediateField.ExtendRight

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝¹¹ : Field K
inst✝¹⁰ : Field L
inst✝⁹ : Algebra K L
F : IntermediateField K L
M : Type u_3
inst✝⁸ : Field M
inst✝⁷ : Algebra K M
inst✝⁶ : Algebra L M
inst✝⁵ : IsScalarTower K L M
R : Type u_4
S : Type u_5
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra S ↥F
inst✝¹ : Algebra S M
inst✝ : IsScalarTower S (↥F) M
s : S
x : ↥(F.extendRight M)
⊢ (algebraMap S M) s * ↑x ∈ F.extendRight M

Tactic:
exact (F.extendRight M).mul_mem (algebraMap_mem F M s) x.prop

Goal state after:
Module: Mathlib.FieldTheory.IsPerfectClosure

Goal state before:
pp: case pos
R : Type u_1
inst✝ : CommSemiring R
p : ℕ
x : R
hp : 1 < p
⊢ x ∈ pNilradical R p ↔ ∃ n, x ^ p ^ n = 0

pp: case neg
R : Type u_1
inst✝ : CommSemiring R
p : ℕ
x : R
hp : ¬1 < p
⊢ x ∈ pNilradical R p ↔ ∃ n, x ^ p ^ n = 0

Tactic:
· rw [pNilradical_eq_nilradical hp]
    refine ⟨fun ⟨n, h⟩ ↦ ⟨n, ?_⟩, fun ⟨n, h⟩ ↦ ⟨p ^ n, h⟩⟩
    rw [← Nat.sub_add_cancel ((n.lt_pow_self hp).le), pow_add, h, mul_zero]

Goal state after:
case neg
R : Type u_1
inst✝ : CommSemiring R
p : ℕ
x : R
hp : ¬1 < p
⊢ x ∈ pNilradical R p ↔ ∃ n, x ^ p ^ n = 0
Module: Mathlib.FieldTheory.Galois.Profinite

Goal state before:
pp: k✝ : Type u_1
K✝ : Type u_2
inst✝⁶ : Field k✝
inst✝⁵ : Field K✝
inst✝⁴ : Algebra k✝ K✝
k : Type u_3
K : Type u_4
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
inst✝ : IsGalois k K
g : ↑(limit (asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop
x : K
L : FiniteGaloisIntermediateField k K := adjoin k {x, toAlgEquivAux g x}
hx : x ∈ L.toIntermediateField
hx' : toAlgEquivAux g x ∈ L.toIntermediateField
⊢ toAlgEquivAux g⁻¹ (toAlgEquivAux g x) = x

Tactic:
simp only [toAlgEquivAux_eq_proj_of_mem _ _ L hx', map_inv, AlgEquiv.aut_inv,
      mk_toAlgEquivAux g x L hx' hx, AlgEquiv.symm_apply_apply]

Goal state after:
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
inst✝ : IsGalois k K
H : Set Gal(K/k)
L : FiniteGaloisIntermediateField k K
le : ↑L.fixingSubgroup ⊆ H
⊢ (fun a ↦ (mulEquivToLimit k K).toEquiv a) '' H ∈ nhds 1

Tactic:
rw [mem_nhds_iff]

Goal state after:
k : Type u_3
K : Type u_4
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
inst✝ : IsGalois k K
H : Set Gal(K/k)
L : FiniteGaloisIntermediateField k K
le : ↑L.fixingSubgroup ⊆ H
⊢ ∃ t ⊆ (fun a ↦ (mulEquivToLimit k K).toEquiv a) '' H, IsOpen t ∧ 1 ∈ t
Module: Mathlib.FieldTheory.IsRealClosed.Basic

Goal state before:
pp: R : Type u
inst✝¹ : Field R
inst✝ : IsRealClosed R
n : ℕ
ih : ∀ m < n, ∀ {x : R}, IsSquare x → m ≠ 0 → ∃ r, x = r ^ m
x : R
hn : n ≠ 0
m : ℕ
hm : n = m + m
s : R
hs : x = s * s
h : IsSquare s
⊢ m < n

Tactic:
lia

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

Goal state before:
pp: R : Type u
inst✝¹ : Field R
inst✝ : IsRealClosed R
n : ℕ
ih : ∀ m < n, ∀ {x : R}, IsSquare x → m ≠ 0 → ∃ r, x = r ^ m
x : R
hn : n ≠ 0
m : ℕ
hm : n = m + m
s : R
hs : x = s * s
h : IsSquare s
⊢ m ≠ 0

Tactic:
lia

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

Goal state before:
pp: R : Type u
inst✝¹ : Field R
inst✝ : IsRealClosed R
n : ℕ
ih : ∀ m < n, ∀ {x : R}, IsSquare x → m ≠ 0 → ∃ r, x = r ^ m
x : R
hn : n ≠ 0
m : ℕ
hm : n = m + m
s : R
hs : x = s * s
h : IsSquare (-s)
⊢ m < n

Tactic:
lia

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

Goal state before:
pp: R : Type u
inst✝¹ : Field R
inst✝ : IsRealClosed R
n : ℕ
ih : ∀ m < n, ∀ {x : R}, IsSquare x → m ≠ 0 → ∃ r, x = r ^ m
x : R
hn : n ≠ 0
m : ℕ
hm : n = m + m
s : R
hs : x = s * s
h : IsSquare (-s)
⊢ m ≠ 0

Tactic:
lia

Goal state after:
Module: Mathlib.GroupTheory.CosetCover

Goal state before:
pp: case right
G : Type u_1
inst✝ : Group G
ι : Type u_2
s : Finset ι
H : Subgroup G
g : ι → G
hcovers : ⋃ i ∈ s, g i • ↑H = Set.univ
hind : H.index = s.card
this : Fintype (G ⧸ H)
⊢ Fintype.card ↥s = Fintype.card (G ⧸ H)

Tactic:
· simp only [Fintype.card_coe, ← hind, index_eq_card, Nat.card_eq_fintype_card]

Goal state after:
Module: Mathlib.FieldTheory.JacobsonNoether

Goal state before:
pp: D : Type u_1
inst✝¹ : DivisionRing D
inst✝ : Algebra.IsAlgebraic (↥k) D
p : ℕ
hchar : ExpChar D p
a : D
hinsep : ∀ (x : D), IsSeparable (↥k) x → x ∈ k
this : IsPurelyInseparable (↥k) D → ∀ (x : D), ∃ n, x ^ p ^ n ∈ (algebraMap (↥k) D).range
⊢ ∃ n, a ^ p ^ n ∈ k

Tactic:
have pure : IsPurelyInseparable k D := ⟨Algebra.IsAlgebraic.isIntegral, fun x hx ↦ by
    rw [RingHom.mem_range, Subtype.exists]
    exact ⟨x, ⟨hinsep x hx, rfl⟩⟩⟩

Goal state after:
D : Type u_1
inst✝¹ : DivisionRing D
inst✝ : Algebra.IsAlgebraic (↥k) D
p : ℕ
hchar : ExpChar D p
a : D
hinsep : ∀ (x : D), IsSeparable (↥k) x → x ∈ k
this : IsPurelyInseparable (↥k) D → ∀ (x : D), ∃ n, x ^ p ^ n ∈ (algebraMap (↥k) D).range
pure : IsPurelyInseparable (↥k) D
⊢ ∃ n, a ^ p ^ n ∈ k
Module: Mathlib.FieldTheory.JacobsonNoether

Goal state before:
pp: D : Type u_1
inst✝¹ : DivisionRing D
inst✝ : Algebra.IsAlgebraic (↥k) D
p : ℕ
hchar : ExpChar D p
a : D
ha : a ∉ k
hinsep : ∀ (x : D), IsSeparable (↥k) x → x ∈ k
m : ℕ
hm : 1 ≤ m ∧ a ^ p ^ m ∈ k
n : ℕ
hn : p ^ m ≤ n
inter : (⇑((ad (↥k) D) a))^[p ^ m] = 0
⊢ (⇑((ad (↥k) D) a))^[n - p ^ m] ∘ (⇑((ad (↥k) D) a))^[p ^ m] = 0

Tactic:
inter,

Goal state after:
D : Type u_1
inst✝¹ : DivisionRing D
inst✝ : Algebra.IsAlgebraic (↥k) D
p : ℕ
hchar : ExpChar D p
a : D
ha : a ∉ k
hinsep : ∀ (x : D), IsSeparable (↥k) x → x ∈ k
m : ℕ
hm : 1 ≤ m ∧ a ^ p ^ m ∈ k
n : ℕ
hn : p ^ m ≤ n
inter : (⇑((ad (↥k) D) a))^[p ^ m] = 0
⊢ (⇑((ad (↥k) D) a))^[n - p ^ m] ∘ 0 = 0
Module: Mathlib.FieldTheory.JacobsonNoether

Goal state before:
pp: D : Type u_1
inst✝¹ : DivisionRing D
inst✝ : Algebra.IsAlgebraic (↥k) D
H : k ≠ ⊤
p : ℕ
hp : ExpChar D p
insep : ∀ (x : D), IsSeparable (↥k) x → x ∈ k
a : D
ha : a ∉ k
ha₀ : a ≠ 0
b : D
hb1 : ((ad (↥k) D) a) b ≠ 0
m : ℕ
hm2 : ∀ (n : ℕ), p ^ m ≤ n → (⇑((ad (↥k) D) a))^[n] = 0
h_exist : ∃ n, 0 < n ∧ (⇑((ad (↥k) D) a))^[n + 1] b = 0
t : ℕ := Nat.find h_exist - 1
ht : t = Nat.find h_exist - 1
h_pos : 0 < t
⊢ t < Nat.find h_exist

Tactic:
lia

Goal state after:
Module: Mathlib.FieldTheory.JacobsonNoether

Goal state before:
pp: D : Type u_1
inst✝¹ : DivisionRing D
inst✝ : Algebra.IsAlgebraic (↥k) D
H : k ≠ ⊤
p : ℕ
hp : ExpChar D p
insep : ∀ (x : D), IsSeparable (↥k) x → x ∈ k
a : D
ha : a ∉ k
ha₀ : a ≠ 0
b : D
hb1 : ((ad (↥k) D) a) b ≠ 0
m : ℕ
hm2 : ∀ (n : ℕ), p ^ m ≤ n → (⇑((ad (↥k) D) a))^[n] = 0
h_exist : ∃ n, 0 < n ∧ (⇑((ad (↥k) D) a))^[n + 1] b = 0
t : ℕ := Nat.find h_exist - 1
ht : t = Nat.find h_exist - 1
h_pos : 0 < t
⊢ Nat.find h_exist = t + 1

Tactic:
lia

Goal state after:
Module: Mathlib.FieldTheory.KummerExtension

Goal state before:
pp: case one
K : Type u
inst✝ : Field K
hn : Odd 1
a : K
ha : ∀ (p : ℕ), Nat.Prime p → p ∣ 1 → ∀ (b : K), b ^ p ≠ a
⊢ Irreducible (X ^ 1 - C a)

Tactic:
simpa using irreducible_X_sub_C a

Goal state after: