mathlib-initiative/mathlib-tactics huggingface dataset:
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, 1 ∈ V ∧ IsOpen[inst✝⁴] V ∧ ∀ x ∈ V, ∀ y ∈ V, ∀ (m : ℤ), g ^ m ≠ a * x / y

Tactic:
← interior_compl,

Goal state after:
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 ∈ interior (range fun x ↦ g ^ x)ᶜ
⊢ ∃ V, 1 ∈ V ∧ IsOpen[inst✝⁴] V ∧ ∀ x ∈ V, ∀ y ∈ V, ∀ (m : ℤ), g ^ m ≠ a * x / y
Module: Mathlib.Dynamics.Ergodic.Conservative

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : NullMeasurableSet s μ
⊢ ∀ᵐ (x : α) ∂μ, ∀ (k : ℕ), f^[k] x ∈ s → ∃ᶠ (n : ℕ) in atTop, f^[n] x ∈ s

Tactic:
refine ae_all_iff.2 fun k => ?_
  refine (hf.ae_mem_imp_frequently_image_mem
    (hs.preimage <| hf.toQuasiMeasurePreserving.iterate k)).mono fun x hx hk => ?_
  rw [← map_add_atTop_eq_nat k, frequently_map]
  refine (hx hk).mono fun n hn => ?_
  rwa [add_comm, iterate_add_apply]

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
f : α → ℝ≥0∞
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hfν : AEMeasurable f ν
hf_ne_top : ∀ᵐ (x : α) ∂μ, f x ≠ ∞
μ' : Measure α := ν.withDensity (μ.rnDeriv ν)
⊢ (μ.withDensity f).rnDeriv ν =ᵐ[ν] fun x ↦ f x * μ.rnDeriv ν x

Tactic:
have hμ'ν : μ' ≪ ν := withDensity_absolutelyContinuous _ _

Goal state after:
α : Type u_1
m : MeasurableSpace α
f : α → ℝ≥0∞
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hfν : AEMeasurable f ν
hf_ne_top : ∀ᵐ (x : α) ∂μ, f x ≠ ∞
μ' : Measure α := ν.withDensity (μ.rnDeriv ν)
hμ'ν : μ' ≪ ν
⊢ (μ.withDensity f).rnDeriv ν =ᵐ[ν] fun x ↦ f x * μ.rnDeriv ν x
Module: Mathlib.Dynamics.OmegaLimit

Goal state before:
pp: τ : Type u_1
α : Type u_2
β : Type u_3
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
v : Set τ
hv : v ∈ f
⊢ ω f ϕ s = ⋂ u, closure[inst✝] (image2 ϕ (↑u ∩ v) s)

Tactic:
rw [omegaLimit_eq_biInter_inter _ _ _ hv]
  apply biInter_eq_iInter

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 α
u : Set τ
hu : u ∈ f
a✝ : β
hx : a✝ ∈ ⋂ u, closure[inst✝] (image2 ϕ (↑u) s)
⊢ a✝ ∈ closure[inst✝] (image2 ϕ u s)

Tactic:
rw [mem_iInter] at hx

Goal state after:
τ : Type u_1
α : Type u_2
β : Type u_3
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
u : Set τ
hu : u ∈ f
a✝ : β
hx : ∀ (i : ↑f.sets), a✝ ∈ closure[inst✝] (image2 ϕ (↑i) s)
⊢ a✝ ∈ closure[inst✝] (image2 ϕ u s)
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)
this : ⋃ u ∈ f, j u = ⋃ u, j ↑u
⊢ ⋂ i, k \ j ↑i ⊆ n

Tactic:
omegaLimit_eq_iInter_inter _ _ _ hv₁

Goal state after:
τ : 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
v : Set τ
hn₂ : ⋂ u, closure[inst✝] (image2 ϕ (↑u ∩ v) s) ⊆ n
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)
this : ⋃ u ∈ f, j u = ⋃ u, j ↑u
⊢ ⋂ i, k \ j ↑i ⊆ n
Module: Mathlib.Dynamics.OmegaLimit

Goal state before:
pp: τ : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
inst✝ : f.NeBot
c : Set β
hc₁ : IsCompact c
hs : s.Nonempty
v : Set τ
hv₁ : v ∈ f
hv₂ : closure[inst✝¹] (image2 ϕ v s) ⊆ c
⊢ (ω f ϕ s).Nonempty

Tactic:
omegaLimit_eq_iInter_inter _ _ _ hv₁

Goal state after:
τ : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
inst✝ : f.NeBot
c : Set β
hc₁ : IsCompact c
hs : s.Nonempty
v : Set τ
hv₁ : v ∈ f
hv₂ : closure[inst✝¹] (image2 ϕ v s) ⊆ c
⊢ (⋂ u, closure[inst✝¹] (image2 ϕ (↑u ∩ v) s)).Nonempty
Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy

Goal state before:
pp: X : Type u_1
T : X → X
U : SetRel X X
n : ℕ
F : Set X
s t : Finset X
hs : IsDynNetIn T F U n ↑s
ht : IsDynCoverOf T F U n ↑t
⊢ s.card ≤ t.card

Tactic:
have (x : X) (x_s : x ∈ s) : ∃ z ∈ t, z ∈ ball x (dynEntourage T U n) := by
    simpa using! ht (hs.1 x_s)
  choose! F s_t using this
  apply Finset.card_le_card_of_injOn F fun x x_s ↦ (s_t x x_s).1
  exact fun x x_s y y_s Fx_Fy ↦
    PairwiseDisjoint.elim_set hs.2 x_s y_s (F x) (s_t x x_s).2 (Fx_Fy ▸ (s_t y y_s).2)

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SFinite ν
s : Set α
⊢ ∫ (x : α) in s, (μ.rnDeriv ν x).toReal ∂ν = (ν.withDensity (μ.rnDeriv ν)).real s

Tactic:
by
  rw [integral_toReal (Measure.measurable_rnDeriv _ _).aemeasurable, measureReal_def]
  · rw [ENNReal.toReal_eq_toReal_iff, ← withDensity_apply' _ s]
    simp
  · exact ae_restrict_of_ae (Measure.rnDeriv_lt_top _ _)

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν κ : Measure α
inst✝² : SigmaFinite μ
inst✝¹ : SigmaFinite ν
inst✝ : SigmaFinite κ
hμν : μ ≪ ν
⊢ μ.rnDeriv ν * ν.rnDeriv κ =ᵐ[κ] μ.rnDeriv κ

Tactic:
by
  refine (rnDeriv_withDensity_left ?_ ?_).symm.trans ?_
  · exact (Measure.measurable_rnDeriv _ _).aemeasurable
  · exact rnDeriv_ne_top _ _
  · rw [Measure.withDensity_rnDeriv_eq _ _ hμν]

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

Goal state before:
pp: case a
X : Type u_1
inst✝ : UniformSpace X
T : X → X
F : Set X
U : Set (X × X)
U_uni : U ∈ 𝓤 X
⊢ netEntropyEntourage T F U ≤ coverEntropy T F

Tactic:
· apply (netEntropyEntourage_antitone T F SetRel.symmetrize_subset_self).trans
    apply (le_iSup₂ (SetRel.symmetrize U) (symmetrize_mem_uniformity U_uni)).trans'
    exact netEntropyEntourage_le_coverEntropyEntourage T F

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

Goal state before:
pp: X : Type u_1
ι : Type u_2
inst✝ : UniformSpace X
T : X → X
F : ι → Set X
s : Finset ι
⊢ coverEntropy T (⋃ i ∈ s, F i) = ⨆ i ∈ s, coverEntropy T (F i)

Tactic:
have := map_finset_sup (coverEntropySupBotHom T) s F
  rw [s.sup_set_eq_biUnion, s.sup_eq_iSup, coverEntropySupBotHom, SupBotHom.coe_mk,
    SupHom.coe_mk] at this
  rw [this]
  congr

Goal state after:
Module: Mathlib.ModelTheory.Basic

Goal state before:
pp: L : Language
L' : Language
i : ℕ
⊢ #((L.sum L').Functions i) = lift.{u', u} #(L.Functions i) + lift.{u, u'} #(L'.Functions i)

Tactic:
simp [Language.sum]

Goal state after:
Module: Mathlib.ModelTheory.Basic

Goal state before:
pp: L : Language
L' : Language
i : ℕ
⊢ #((L.sum L').Relations i) = lift.{v', v} #(L.Relations i) + lift.{v, v'} #(L'.Relations i)

Tactic:
simp [Language.sum]

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
⊢ solvableByRad F E ≤ algebraicClosure F E

Tactic:
refine solvableByRad_le fun x n hn hx ↦ ?_
  rw [mem_algebraicClosure_iff] at hx ⊢
  obtain ⟨p, h1, h2⟩ := hx
  refine ⟨p.comp (X ^ n), ⟨fun h ↦ h1 (leadingCoeff_eq_zero.mp ?_), ?_⟩⟩
  · rwa [← leadingCoeff_eq_zero, leadingCoeff_comp, leadingCoeff_X_pow, one_pow, mul_one] at h
    rwa [natDegree_X_pow]
  · simpa [aeval_comp]

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] := ⋯
q : F[X] := ⋯
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
⊢ (algebraMap (↥F⟮x, y⟯) E) ((aeval ⟨z, hz'⟩) (minpoly F z)) = (algebraMap (↥F⟮x, y⟯) E) 0

Tactic:
simp [← aeval_algebraMap_apply]

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case func
L : Language
L' : Language
M : Type w
inst✝¹ : L.Structure M
β : Type v'
inst✝ : L'.Structure M
c : {n : ℕ} → L.Functions n → L'.Term (Fin n)
hc : ∀ {n : ℕ} (g : L.Functions n) (y : Fin n → M), realize y g.term = realize y (c g)
v : β → M
l✝ : ℕ
f : L.Functions l✝
ts : Fin l✝ → L.Term β
ih : ∀ (a : Fin l✝), realize v ((ts a).substFunc fun {n} ↦ c) = realize v (ts a)
⊢ realize v ((func f ts).substFunc fun {n} ↦ c) = realize v (func f ts)

Tactic:
simp [← ih, ← hc]

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case var
L : Language
M : Type w
inst✝² : L.Structure M
α : Type u'
β : Type v'
inst✝¹ : L[[α]].Structure M
inst✝ : (L.lhomWithConstants α).IsExpansionOn M
v : β → M
ab : α ⊕ β
⊢ realize v (var ab).varsToConstants = realize (Sum.elim (fun a ↦ ↑(L.con a)) v) (var ab)

Tactic:
rcases ab with a | b <;> simp [Language.con]

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
n : ℕ
l : List (L.BoundedFormula α n)
v : α → M
xs : Fin n → M
⊢ (List.foldr (fun x1 x2 ↦ x1 ⊓ x2) ⊤ l).Realize v xs ↔ ∀ φ ∈ l, φ.Realize v xs

Tactic:
by
  induction l with
  | nil => simp
  | cons φ l ih => simp [ih]

Goal state after:
Module: Mathlib.ModelTheory.Ultraproducts

Goal state before:
pp: case e'_3.e'_3
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst✝ : (a : α) → L.Structure (M a)
β : Type u_3
x : β → (a : α) → M a
t : L.Term β
a : α
⊢ Term.realize (fun i ↦ x i a) t = Term.realize x t a

Tactic:
induction t with
  | var => rfl
  | func _ _ t_ih => simp only [Term.realize, t_ih]; rfl

Goal state after:
Module: Mathlib.ModelTheory.Encoding

Goal state before:
pp: case refine_2.refine_2.inl.inl
L : Language
α : Type u'
a b : α
h :
  Sum.elim (fun i ↦ ⟨0, var (Sum.inl i)⟩) (fun F ↦ ⟨1, func F.snd fun x ↦ var (Sum.inr 0)⟩) (Sum.inl a) =
    Sum.elim (fun i ↦ ⟨0, var (Sum.inl i)⟩) (fun F ↦ ⟨1, func F.snd fun x ↦ var (Sum.inr 0)⟩) (Sum.inl b)
⊢ Sum.inl a = Sum.inl b

Tactic:
simp only [Sum.elim_inl, Sigma.mk.inj_iff, heq_eq_eq, var.injEq, Sum.inl.injEq, true_and]
          at h

Goal state after:
case refine_2.refine_2.inl.inl
L : Language
α : Type u'
a b : α
h : a = b
⊢ Sum.inl a = Sum.inl b
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
β : Type v'
g : α ≃ β
k : ℕ
φ : L.BoundedFormula α k
v : β → M
xs : Fin k → M
⊢ (mapTermRel (fun n ↦ ⇑(Term.relabelEquiv (g.sumCongr (_root_.Equiv.refl (Fin n))))) (fun n ↦ id) (fun x ↦ id)
          φ).Realize
      v xs ↔
    φ.Realize (v ∘ ⇑g) xs

Tactic:
refine realize_mapTermRel_id (fun n t xs => ?_) fun _ _ _ => rfl

Goal state after:
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
β : Type v'
g : α ≃ β
k : ℕ
φ : L.BoundedFormula α k
v : β → M
xs✝ : Fin k → M
n : ℕ
t : L.Term (α ⊕ Fin n)
xs : Fin n → M
⊢ realize (Sum.elim v xs) ((Term.relabelEquiv (g.sumCongr (_root_.Equiv.refl (Fin n)))) t) =
    realize (Sum.elim (v ∘ ⇑g) xs) t
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case equal
L : Language
L' : Language
M : Type w
inst✝² : L.Structure M
α : Type u'
inst✝¹ : L'.Structure M
φ : L →ᴸ L'
inst✝ : φ.IsExpansionOn M
n : ℕ
v : α → M
n✝ : ℕ
t₁✝ t₂✝ : L.Term (α ⊕ Fin n✝)
xs : Fin n✝ → M
⊢ (φ.onBoundedFormula (equal t₁✝ t₂✝)).Realize v xs ↔ (equal t₁✝ t₂✝).Realize v xs

Tactic:
simp only [onBoundedFormula, realize_bdEqual, realize_onTerm]; rfl

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
v : α → M
R : L.Relations 2
t₁ t₂ : L.Term α
⊢ (R.formula₂ t₁ t₂).Realize v ↔ RelMap R ![Term.realize v t₁, Term.realize v t₂]

Tactic:
rw [Relations.formula₂, realize_rel, iff_eq_eq]
  refine congr rfl (funext (Fin.cases ?_ ?_))
  · simp only [Matrix.cons_val_zero]
  · simp only [Matrix.cons_val_succ, Matrix.cons_val_fin_one, forall_const]

Goal state after:
Module: Mathlib.ModelTheory.Substructures

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

Tactic:
by
  refine closure_eq_of_le ((A.subset_union_right).trans subset_closure) ?_
  rw [← (L.lhomWithConstants A).substructureReduct.le_iff_le]
  simp only [subset_closure, reduct_withConstants, closure_le, LHom.coe_substructureReduct,
    Set.union_subset_iff, and_true]
  exact subset_closure_withConstants

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
N : Type u_1
inst✝³ : L.Structure M
inst✝² : L.Structure N
F : Type u_4
inst✝¹ : EquivLike F M N
inst✝ : L.StrongHomClass F M N
g : F
φ : L.Sentence
⊢ M ⊨ φ ↔ N ⊨ φ

Tactic:
by
  rw [Sentence.Realize, Sentence.Realize, ← realize_formula g,
    Unique.eq_default (g ∘ default)]

Goal state after:
Module: Mathlib.ModelTheory.Satisfiability

Goal state before:
pp: L : Language
ι : Type u_1
T : ι → L.Theory
h : ∀ (s : Finset ι), IsSatisfiable (⋃ i ∈ s, T i)
s : Finset L.Sentence
hs : ↑s ⊆ ⋃ i, T i
⊢ IsSatisfiable ↑s

Tactic:
Set.iUnion_eq_iUnion_finset

Goal state after:
L : Language
ι : Type u_1
T : ι → L.Theory
h : ∀ (s : Finset ι), IsSatisfiable (⋃ i ∈ s, T i)
s : Finset L.Sentence
hs : ↑s ⊆ ⋃ t, ⋃ i ∈ t, T i
⊢ IsSatisfiable ↑s
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.field ∪ genericMonicPolyHasRoot '' {n | 0 < n}
q : Nat.Primes
a✝ : q ∉ ∅
⊢ ψ ∈ Theory.ACF ↑q

Tactic:
rw [Theory.ACF, Theory.fieldOfChar, Set.union_right_comm]

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}
q : Nat.Primes
a✝ : q ∉ ∅
⊢ ψ ∈
    Theory.field ∪ genericMonicPolyHasRoot '' {n | 0 < n} ∪
      if ↑q = 0 then (fun q ↦ ∼(eqZero q)) '' {q | Nat.Prime q} else if Nat.Prime ↑q then {eqZero ↑q} else {⊥}
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}).IsMaximal

Tactic:
convert! RingHom.ker_isMaximal_of_surjective (aeval (R := K) x) ?_
  · ext; simp
  · intro z; use C z; simp

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Divisibility

Goal state before:
pp: a b : Cardinal.{u_1}
hb : b ≠ 0
hdiv : a ∣ b
⊢ a ≤ b

Tactic:
obtain ⟨b, rfl⟩ := hdiv
  apply le_mul_right
  simp_all

Goal state after:
Module: Mathlib.FieldTheory.FinTrdeg

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : FinTrdeg K L
ι : Type u_3
x : ι → L
hx : IsTranscendenceBasis K x
⊢ Finite ι

Tactic:
rw [← Cardinal.mk_lt_aleph0_iff, ← Cardinal.lift_lt_aleph0,
    hx.lift_cardinalMk_eq_trdeg, Cardinal.lift_lt_aleph0]

Goal state after:
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : FinTrdeg K L
ι : Type u_3
x : ι → L
hx : IsTranscendenceBasis K x
⊢ Algebra.trdeg K L < Cardinal.aleph0
Module: Mathlib.FieldTheory.Finite.Extension

Goal state before:
pp: k : Type u_1
inst✝¹ : Field k
inst✝ : Finite k
f : k[X]
hi : Irreducible f
n : ℕ
hdvd : f.natDegree ∣ n
a : AdjoinRoot f := AdjoinRoot.root f
this✝¹ : NeZero f.natDegree
this✝ : Fact (Irreducible f)
p : ℕ
hp : CharP k p
this : Fact (Nat.Prime p)
e : AdjoinRoot f ≃ₐ[k] Extension k p f.natDegree := algEquivExtension k p f.natDegree (AdjoinRoot f) ⋯
⊢ e a ^ Nat.card k ^ f.natDegree - e a = 0

Tactic:
have := Fintype.ofFinite (Extension k p f.natDegree)

Goal state after:
k : Type u_1
inst✝¹ : Field k
inst✝ : Finite k
f : k[X]
hi : Irreducible f
n : ℕ
hdvd : f.natDegree ∣ n
a : AdjoinRoot f := AdjoinRoot.root f
this✝² : NeZero f.natDegree
this✝¹ : Fact (Irreducible f)
p : ℕ
hp : CharP k p
this✝ : Fact (Nat.Prime p)
e : AdjoinRoot f ≃ₐ[k] Extension k p f.natDegree := algEquivExtension k p f.natDegree (AdjoinRoot f) ⋯
this : Fintype (Extension k p f.natDegree)
⊢ e a ^ Nat.card k ^ f.natDegree - e a = 0
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
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
ffb : fixedField ⊤ = ⊥
i : ι
| logDeriv (∏ x, x (u i))

Tactic:
equals ∑ x : K ≃ₐ[F] K, logDeriv (x (u i)) =>
          by_cases h : u i = 0 <;>
          simp [logDeriv_prod, h]

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

Goal state before:
pp: case e_f
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
ffb : fixedField ⊤ = ⊥
e : Gal(K/F)
⊢ ↑a = ∑ x, ↑(c x) * logDeriv (e (u x)) + (e v)′

Tactic:
apply_fun e at h

Goal state after:
case e_f
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
this : CharZero K
ffb : fixedField ⊤ = ⊥
e : Gal(K/F)
h : e ↑a = e (∑ x, ↑(c x) * logDeriv (u x) + v′)
⊢ ↑a = ∑ x, ↑(c x) * logDeriv (e (u x)) + (e v)′
Module: Mathlib.FieldTheory.CardinalEmb

Goal state before:
pp: F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst✝ : Algebra.IsAlgebraic F E
i j : (Module.rank F E).ord.ToType
h : i < j
least : ∀ (i : (Module.rank F E).ord.ToType), IsLeast {k | b k ∉ adjoin F (⇑b ∘ φ '' Iio i)} (φ i)
this : φ j ≤ φ i
⊢ False

Tactic:
obtain eq | lt := this.eq_or_lt

Goal state after:
case inl
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst✝ : Algebra.IsAlgebraic F E
i j : (Module.rank F E).ord.ToType
h : i < j
least : ∀ (i : (Module.rank F E).ord.ToType), IsLeast {k | b k ∉ adjoin F (⇑b ∘ φ '' Iio i)} (φ i)
this : φ j ≤ φ i
eq : φ j = φ i
⊢ False

case inr
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst✝ : Algebra.IsAlgebraic F E
i j : (Module.rank F E).ord.ToType
h : i < j
least : ∀ (i : (Module.rank F E).ord.ToType), IsLeast {k | b k ∉ adjoin F (⇑b ∘ φ '' Iio i)} (φ i)
this : φ j ≤ φ i
lt : φ j < φ i
⊢ False
Module: Mathlib.FieldTheory.IsPerfectClosure

Goal state before:
pp: K : Type u_1
L : Type u_2
M : Type u_3
inst✝⁶ : CommRing K
inst✝⁵ : CommRing L
inst✝⁴ : CommRing M
i : K →+* L
j : K →+* M
p : ℕ
inst✝³ : ExpChar M p
inst✝² : ExpChar K p
inst✝¹ : PerfectRing M p
inst✝ : IsPRadical i p
x : L
n : ℕ
y : K
n' : ℕ := (Classical.choose ⋯).1
h' : i (Classical.choose ⋯).2 = x ^ p ^ n'
h✝ : (Classical.choose ⋯).2 ^ p ^ n - y ^ p ^ n' ∈ RingHom.ker i
m : ℕ
h : ((Classical.choose ⋯).2 ^ p ^ n - y ^ p ^ n') ^ p ^ m = 0
⊢ (iterateFrobeniusEquiv M p n').symm (j (Classical.choose ⋯).2) = (iterateFrobeniusEquiv M p n).symm (j y)

Tactic:
refine (iterateFrobeniusEquiv M p (m + n + n')).injective ?_

Goal state after:
K : Type u_1
L : Type u_2
M : Type u_3
inst✝⁶ : CommRing K
inst✝⁵ : CommRing L
inst✝⁴ : CommRing M
i : K →+* L
j : K →+* M
p : ℕ
inst✝³ : ExpChar M p
inst✝² : ExpChar K p
inst✝¹ : PerfectRing M p
inst✝ : IsPRadical i p
x : L
n : ℕ
y : K
n' : ℕ := (Classical.choose ⋯).1
h' : i (Classical.choose ⋯).2 = x ^ p ^ n'
h✝ : (Classical.choose ⋯).2 ^ p ^ n - y ^ p ^ n' ∈ RingHom.ker i
m : ℕ
h : ((Classical.choose ⋯).2 ^ p ^ n - y ^ p ^ n') ^ p ^ m = 0
⊢ (iterateFrobeniusEquiv M p (m + n + n')) ((iterateFrobeniusEquiv M p n').symm (j (Classical.choose ⋯).2)) =
    (iterateFrobeniusEquiv M p (m + n + n')) ((iterateFrobeniusEquiv M p n).symm (j y))
Module: Mathlib.FieldTheory.PerfectClosure

Goal state before:
pp: K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x : ℕ × K
⊢ (⇑(frobenius K p))^[(x.1, 1).1 + 0] (0, 1).2 = (⇑(frobenius K p))^[(0, 1).1 + 0] (x.1, 1).2

Tactic:
simp_rw [← coe_iterateFrobenius, map_one]

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
splits : ∀ s ∈ S, (Polynomial.map (algebraMap F K') (minpoly F s)).Splits
K₀ : IntermediateField F K' := restrictScalars F ⊥
FS : IntermediateField F E := adjoin F ↑S
Ω : Type (max u_2 u_3) := ↥FS →ₐ[F] K'
this : FiniteDimensional F ↥(adjoin F ↑S)
M : Ω → Submodule F ↥FS := fun ω ↦ Subalgebra.toSubmodule (comap ω K₀).toSubalgebra
x✝ : ↥FS
α : E
hα : α ∈ FS
β : K
hβ : (aeval β) (minpoly F α) = 0
⊢ ∃ i, ⟨α, hα⟩ ∈ ↑(M i)

Tactic:
let ϕ : F⟮α⟯ →ₐ[F] K' := (IsScalarTower.toAlgHom _ _ _).comp
        ((AdjoinRoot.liftAlgHom _ _ _ hβ).comp
        (adjoinRootEquivAdjoin F <| (alg.isIntegral).1 _).symm.toAlgHom)

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
K₀ : IntermediateField F K' := restrictScalars F ⊥
FS : IntermediateField F E := adjoin F ↑S
Ω : Type (max u_2 u_3) := ↥FS →ₐ[F] K'
this : FiniteDimensional F ↥(adjoin F ↑S)
M : Ω → Submodule F ↥FS := fun ω ↦ Subalgebra.toSubmodule (comap ω K₀).toSubalgebra
x✝ : ↥FS
α : E
hα : α ∈ FS
β : K
hβ : (aeval β) (minpoly F α) = 0
ϕ : ↥F⟮α⟯ →ₐ[F] K' :=
  (IsScalarTower.toAlgHom F K K').comp
    ((AdjoinRoot.liftAlgHom (minpoly F α) (Algebra.ofId F K) β hβ).comp ↑(adjoinRootEquivAdjoin F ⋯).symm)
⊢ ∃ i, ⟨α, hα⟩ ∈ ↑(M i)