mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
hf : AEMeasurable f ν
s : Set α
hs : MeasurableSet s
⊢ AEMeasurable (μ.rnDeriv ν) (ν.restrict s)

Tactic:
· exact (Measure.measurable_rnDeriv _ _).aemeasurable

Goal state after:
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
inter_nemp : (⋂ k, T^[m * ↑k] ⁻¹' ball (↑(t k)) (dynEntourage T U m)).Nonempty
⊢ ∃ y, ⋂ k, T^[m * ↑k] ⁻¹' ball (↑(t k)) (dynEntourage T U m) ⊆ ball y (dynEntourage T (U ○ U) (m * n))

Tactic:
· obtain ⟨y, y_int⟩ := inter_nemp
      refine ⟨y, fun z z_int ↦ ?_⟩
      simp only [ball, dynEntourage, Prod.map_iterate, mem_iInter, Set.mem_preimage, Prod.map_apply,
        mem_comp] at y_int z_int ⊢
      intro k k_mn
      replace k_mn := Nat.div_lt_of_lt_mul k_mn
      specialize z_int ⟨(k / m), k_mn⟩ (k % m) (Nat.mod_lt k m_pos)
      specialize y_int ⟨(k / m), k_mn⟩ (k % m) (Nat.mod_lt k m_pos)
      rw [← Function.iterate_add_apply T (k % m) (m * (k / m)), Nat.mod_add_div k m] at y_int z_int
      exact mem_comp_of_mem_ball y_int z_int

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

Goal state before:
pp: X : Type u_1
T : X → X
U : SetRel X X
F : Set X
inst✝ : UniformSpace X
F_comp : IsCompact F
F_inv : MapsTo T F F
U_uni : U ∈ 𝓤 X
n : ℕ
V : SetRel X X
V_uni : V ∈ 𝓤 X
V_symm : V.IsSymm
V_U : V ○ V ⊆ U
s : Finset X
left✝ : ∀ x ∈ s, x ∈ F
s_cover : F ⊆ ⋃ x ∈ s, ball x V
this : IsDynCoverOf T F V 1 ↑s
⊢ ∃ s, IsDynCoverOf T F U n ↑s

Tactic:
obtain ⟨t, t_dyncover, t_card⟩ := this.iterate_le_pow F_inv n

Goal state after:
X : Type u_1
T : X → X
U : SetRel X X
F : Set X
inst✝ : UniformSpace X
F_comp : IsCompact F
F_inv : MapsTo T F F
U_uni : U ∈ 𝓤 X
n : ℕ
V : SetRel X X
V_uni : V ∈ 𝓤 X
V_symm : V.IsSymm
V_U : V ○ V ⊆ U
s : Finset X
left✝ : ∀ x ∈ s, x ∈ F
s_cover : F ⊆ ⋃ x ∈ s, ball x V
this : IsDynCoverOf T F V 1 ↑s
t : Finset X
t_dyncover : IsDynCoverOf T F (V ○ V) (1 * n) ↑t
t_card : #t ≤ #s ^ n
⊢ ∃ s, IsDynCoverOf T F U n ↑s
Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy

Goal state before:
pp: case mp
X : Type u_1
T : X → X
F : Set X
U : SetRel X X
n : ℕ
h : netMaxcard T F U n < ⊤
k : ℕ
k_max : ↑k = ↑(sSup (Finset.card '' {s | IsDynNetIn T F U n ↑s}))
this : netMaxcard T F U n = sSup (WithTop.some '' Finset.card '' {s | IsDynNetIn T F U n ↑s})
h_bdda : BddAbove (Finset.card '' {s | IsDynNetIn T F U n ↑s})
h_nemp : (Finset.card '' {s | IsDynNetIn T F U n ↑s}).Nonempty
⊢ ∃ s, IsDynNetIn T F U n ↑s ∧ s.card = k

Tactic:
have key := Nat.sSup_mem h_nemp h_bdda

Goal state after:
case mp
X : Type u_1
T : X → X
F : Set X
U : SetRel X X
n : ℕ
h : netMaxcard T F U n < ⊤
k : ℕ
k_max : ↑k = ↑(sSup (Finset.card '' {s | IsDynNetIn T F U n ↑s}))
this : netMaxcard T F U n = sSup (WithTop.some '' Finset.card '' {s | IsDynNetIn T F U n ↑s})
h_bdda : BddAbove (Finset.card '' {s | IsDynNetIn T F U n ↑s})
h_nemp : (Finset.card '' {s | IsDynNetIn T F U n ↑s}).Nonempty
key : sSup (Finset.card '' {s | IsDynNetIn T F U n ↑s}) ∈ Finset.card '' {s | IsDynNetIn T F U n ↑s}
⊢ ∃ s, IsDynNetIn T F U n ↑s ∧ s.card = k
Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy

Goal state before:
pp: X : Type u_1
F : Set X
T : X → X
h : F.Nonempty
U : SetRel X X
⊢ netMaxcard T F U 0 = 1

Tactic:
by
  apply (iSup₂_le _).antisymm ((one_le_netMaxcard_iff T F U 0).2 h)
  intro s ⟨_, s_net⟩
  simp only [ball, dynEntourage_zero, preimage_univ] at s_net
  norm_cast
  refine Finset.card_le_one.2 fun x x_s y y_s ↦ ?_
  exact PairwiseDisjoint.elim_set s_net x_s y_s x (mem_univ x) (mem_univ x)

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

Goal state before:
pp: X : Type u_1
F : Set X
T : X → X
h : F.Nonempty
n : ℕ
⊢ netMaxcard T F univ n = 1

Tactic:
by
  apply (iSup₂_le _).antisymm ((one_le_netMaxcard_iff T F univ n).2 h)
  intro s ⟨_, s_net⟩
  simp only [ball, dynEntourage_univ, preimage_univ] at s_net
  norm_cast
  refine Finset.card_le_one.2 fun x x_s y y_s ↦ ?_
  exact PairwiseDisjoint.elim_set s_net x_s y_s x (mem_univ x) (mem_univ x)

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

Goal state before:
pp: case refine_1
α : Type u_1
m : MeasurableSpace α
μ ν κ : Measure α
inst✝² : SigmaFinite μ
inst✝¹ : SigmaFinite ν
inst✝ : SigmaFinite κ
hμν : μ ≪ ν
⊢ AEMeasurable (μ.rnDeriv ν) κ

pp: case refine_2
α : Type u_1
m : MeasurableSpace α
μ ν κ : Measure α
inst✝² : SigmaFinite μ
inst✝¹ : SigmaFinite ν
inst✝ : SigmaFinite κ
hμν : μ ≪ ν
⊢ ∀ᵐ (x : α) ∂ν, μ.rnDeriv ν x ≠ ∞

pp: case refine_3
α : Type u_1
m : MeasurableSpace α
μ ν κ : Measure α
inst✝² : SigmaFinite μ
inst✝¹ : SigmaFinite ν
inst✝ : SigmaFinite κ
hμν : μ ≪ ν
⊢ (ν.withDensity (μ.rnDeriv ν)).rnDeriv κ =ᵐ[κ] μ.rnDeriv κ

Tactic:
· exact (Measure.measurable_rnDeriv _ _).aemeasurable

Goal state after:
case refine_2
α : Type u_1
m : MeasurableSpace α
μ ν κ : Measure α
inst✝² : SigmaFinite μ
inst✝¹ : SigmaFinite ν
inst✝ : SigmaFinite κ
hμν : μ ≪ ν
⊢ ∀ᵐ (x : α) ∂ν, μ.rnDeriv ν x ≠ ∞

case refine_3
α : Type u_1
m : MeasurableSpace α
μ ν κ : Measure α
inst✝² : SigmaFinite μ
inst✝¹ : SigmaFinite ν
inst✝ : SigmaFinite κ
hμν : μ ≪ ν
⊢ (ν.withDensity (μ.rnDeriv ν)).rnDeriv κ =ᵐ[κ] μ.rnDeriv κ
Module: Mathlib.Dynamics.TopologicalEntropy.Subset

Goal state before:
pp: X : Type u_1
T : X → X
U : SetRel X X
⊢ Monotone fun F ↦ netEntropyEntourage T F U

Tactic:
by
  refine fun F G F_G ↦ ExpGrowth.expGrowthSup_monotone fun n ↦ ?_
  exact ENat.toENNReal_mono (netMaxcard_monotone_subset T U n F_G)

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
h_add : (μ + ν).rnDeriv (μ + ν) =ᵐ[ν] μ.rnDeriv (μ + ν) + ν.rnDeriv (μ + ν)
h_one_add : ∀ᵐ (x : α) ∂ν, (μ + ν).rnDeriv (μ + ν) x = (fun x ↦ 1) x
this : μ.rnDeriv (μ + ν) =ᵐ[ν] fun x ↦ 1 - (μ.rnDeriv ν x + 1)⁻¹
a : α
ha : μ.rnDeriv (μ + ν) a = 1 - (μ.rnDeriv ν a + 1)⁻¹
ha_lt_top : μ.rnDeriv ν a < ∞
h : (μ.rnDeriv ν a + 1) * (μ.rnDeriv ν a + 1)⁻¹ = μ.rnDeriv ν a * (μ.rnDeriv ν a + 1)⁻¹ + 1 * (μ.rnDeriv ν a + 1)⁻¹
⊢ 1 = μ.rnDeriv ν a * (μ.rnDeriv ν a + 1)⁻¹ + 1 * (μ.rnDeriv ν a + 1)⁻¹

Tactic:
rwa [ENNReal.mul_inv_cancel (by simp) (by simp [ha_lt_top.ne])] at h

Goal state after:
Module: Mathlib.ModelTheory.LanguageMap

Goal state before:
pp: case refine_2
L : Language
L' : Language
ϕ : L →ᴸ L'
inst✝³ : (n : ℕ) → (f : L'.Functions n) → Decidable (f ∈ Set.range fun f ↦ ϕ.onFunction f)
inst✝² : (n : ℕ) → (r : L'.Relations n) → Decidable (r ∈ Set.range fun r ↦ ϕ.onRelation r)
h : ϕ.Injective
M : Type u_1
inst✝¹ : Inhabited M
inst✝ : L.Structure M
this : L'.Structure M := ϕ.defaultExpansion M
n : ℕ
r : L.Relations n
xs : Fin n → M
hr : ϕ.onRelation r ∈ Set.range fun r ↦ ϕ.onRelation r
⊢ RelMap (Exists.choose hr) xs = RelMap r xs

Tactic:
h.onRelation hr.choose_spec

Goal state after:
case refine_2
L : Language
L' : Language
ϕ : L →ᴸ L'
inst✝³ : (n : ℕ) → (f : L'.Functions n) → Decidable (f ∈ Set.range fun f ↦ ϕ.onFunction f)
inst✝² : (n : ℕ) → (r : L'.Relations n) → Decidable (r ∈ Set.range fun r ↦ ϕ.onRelation r)
h : ϕ.Injective
M : Type u_1
inst✝¹ : Inhabited M
inst✝ : L.Structure M
this : L'.Structure M := ϕ.defaultExpansion M
n : ℕ
r : L.Relations n
xs : Fin n → M
hr : ϕ.onRelation r ∈ Set.range fun r ↦ ϕ.onRelation r
⊢ RelMap r xs = RelMap r xs
Module: Mathlib.ModelTheory.Algebra.Ring.Basic

Goal state before:
pp: α : Type u_1
⊢ (↑[Sum.inl ⟨2, add⟩, Sum.inl ⟨2, mul⟩, Sum.inl ⟨1, neg⟩, Sum.inl ⟨0, zero⟩, Sum.inl ⟨0, one⟩]).Nodup

Tactic:
dsimp [Language.Symbols]; decide

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

Goal state before:
pp: case func
α : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : CompatibleRing R
p : FreeCommRing α
v : α → R
l✝ : ℕ
f : ring.Functions l✝
a : Fin l✝ → ring.Term α
ih : ∀ (a_1 : Fin l✝), Term.realize v (a a_1) = (FreeCommRing.lift v) (Term.realize FreeCommRing.of (a a_1))
⊢ Term.realize v (func f a) = (FreeCommRing.lift v) (Term.realize FreeCommRing.of (func f a))

Tactic:
cases f <;>
    simp [ih]

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
l : ℕ
v : α → M
xs : Fin l → M
R : L.Relations 1
t : L.Term (α ⊕ Fin l)
⊢ (RelMap R fun i ↦ realize (Sum.elim v xs) (![t] i)) = RelMap R ![realize (Sum.elim v xs) t]

Tactic:
refine congr rfl (funext fun _ => ?_)

Goal state after:
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
l : ℕ
v : α → M
xs : Fin l → M
R : L.Relations 1
t : L.Term (α ⊕ Fin l)
x✝ : Fin 1
⊢ realize (Sum.elim v xs) (![t] x✝) = ![realize (Sum.elim v xs) t] x✝
Module: Mathlib.ModelTheory.Encoding

Goal state before:
pp: case func
L : Language
α : Type u'
l✝ : List (L.Term α)
n : ℕ
f : L.Functions n
ts : Fin n → L.Term α
ih : ∀ (a : Fin n) (l : List (α ⊕ (i : ℕ) × L.Functions i)), listDecode ((ts a).listEncode ++ l) = ts a :: listDecode l
l : List (α ⊕ (i : ℕ) × L.Functions i)
h : listDecode (flatMap (fun i ↦ (ts i).listEncode) (finRange n) ++ l) = List.map ts (finRange n) ++ listDecode l
⊢ (fun i ↦ (List.map ts (finRange n) ++ listDecode l)[↑i]) = ts ∧
    drop n (List.map ts (finRange n) ++ listDecode l) = listDecode l

Tactic:
refine ⟨funext (fun i => ?_), ?_⟩

Goal state after:
case func.refine_1
L : Language
α : Type u'
l✝ : List (L.Term α)
n : ℕ
f : L.Functions n
ts : Fin n → L.Term α
ih : ∀ (a : Fin n) (l : List (α ⊕ (i : ℕ) × L.Functions i)), listDecode ((ts a).listEncode ++ l) = ts a :: listDecode l
l : List (α ⊕ (i : ℕ) × L.Functions i)
h : listDecode (flatMap (fun i ↦ (ts i).listEncode) (finRange n) ++ l) = List.map ts (finRange n) ++ listDecode l
i : Fin n
⊢ (List.map ts (finRange n) ++ listDecode l)[↑i] = ts i

case func.refine_2
L : Language
α : Type u'
l✝ : List (L.Term α)
n : ℕ
f : L.Functions n
ts : Fin n → L.Term α
ih : ∀ (a : Fin n) (l : List (α ⊕ (i : ℕ) × L.Functions i)), listDecode ((ts a).listEncode ++ l) = ts a :: listDecode l
l : List (α ⊕ (i : ℕ) × L.Functions i)
h : listDecode (flatMap (fun i ↦ (ts i).listEncode) (finRange n) ++ l) = List.map ts (finRange n) ++ listDecode l
⊢ drop n (List.map ts (finRange n) ++ listDecode l) = listDecode l
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
v : α → M
R : L.Relations 1
t : L.Term α
⊢ (RelMap R fun i ↦ Term.realize v (![t] i)) = RelMap R ![Term.realize v t]

Tactic:
refine congr rfl (funext fun _ => ?_)

Goal state after:
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
v : α → M
R : L.Relations 1
t : L.Term α
x✝ : Fin 1
⊢ Term.realize v (![t] x✝) = ![Term.realize v t] x✝
Module: Mathlib.ModelTheory.ElementaryMaps

Goal state before:
pp: L : Language
M : Type u_1
N : Type u_2
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M ↪[L] N
htv :
  ∀ (n : ℕ) (φ : L.BoundedFormula Empty (n + 1)) (x : Fin n → M) (a : N),
    φ.Realize default (Fin.snoc (⇑f ∘ x) a) → ∃ b, φ.Realize default (Fin.snoc (⇑f ∘ x) (f b))
n✝ : ℕ
φ✝ : L.BoundedFormula Empty n✝
n : ℕ
φ : L.BoundedFormula Empty (n + 1)
ih : ∀ (xs : Fin (n + 1) → M), φ.Realize (⇑f ∘ default) (⇑f ∘ xs) ↔ φ.Realize default xs
xs : Fin n → M
a : N
ha : ¬φ.Realize (⇑f ∘ default) (Fin.snoc (⇑f ∘ xs) a)
⊢ ¬φ.Realize (⇑f ∘ default) (Fin.snoc (⇑f ∘ xs) a)

Tactic:
exact ha

Goal state after:
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 ⊨ ψ
⊢ (equivSentence.symm ψ).Realize fun a ↦ ↑(L.con a)

Tactic:
← S.subtype.map_formula,

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 ⊨ ψ
⊢ (equivSentence.symm ψ).Realize (⇑S.subtype ∘ fun a ↦ ↑(L.con a))
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 ℵ₀)

Tactic:
simp only [card_ring, lift_id']

Goal state after:
case h2
p : ℕ
hp : Nat.Prime p ∨ p = 0
⊢ 5 ≤ Order.succ ℵ₀
Module: Mathlib.ModelTheory.Satisfiability

Goal state before:
pp: L : Language
T : L.Theory
h : T.IsComplete
φ : L.Sentence
⊢ T ⊨ᵇ Formula.not φ ↔ ¬T ⊨ᵇ φ

Tactic:
rcases h.2 φ with hφ | hφn

Goal state after:
case inl
L : Language
T : L.Theory
h : T.IsComplete
φ : L.Sentence
hφ : T ⊨ᵇ φ
⊢ T ⊨ᵇ Formula.not φ ↔ ¬T ⊨ᵇ φ

case inr
L : Language
T : L.Theory
h : T.IsComplete
φ : L.Sentence
hφn : T ⊨ᵇ Formula.not φ
⊢ T ⊨ᵇ Formula.not φ ↔ ¬T ⊨ᵇ φ
Module: Mathlib.ModelTheory.Satisfiability

Goal state before:
pp: L : Language
T : L.Theory
h : T.IsComplete
φ : L.Sentence
M : Type u_1
inst✝² : L.Structure M
inst✝¹ : M ⊨ T
inst✝ : Nonempty M
⊢ M ⊨ φ ↔ T ⊨ᵇ φ

Tactic:
rcases h.2 φ with hφ | hφn

Goal state after:
case inl
L : Language
T : L.Theory
h : T.IsComplete
φ : L.Sentence
M : Type u_1
inst✝² : L.Structure M
inst✝¹ : M ⊨ T
inst✝ : Nonempty M
hφ : T ⊨ᵇ φ
⊢ M ⊨ φ ↔ T ⊨ᵇ φ

case inr
L : Language
T : L.Theory
h : T.IsComplete
φ : L.Sentence
M : Type u_1
inst✝² : L.Structure M
inst✝¹ : M ⊨ T
inst✝ : Nonempty M
hφn : T ⊨ᵇ Formula.not φ
⊢ M ⊨ φ ↔ T ⊨ᵇ φ
Module: Mathlib.GroupTheory.OreLocalization.Cardinality

Goal state before:
pp: R : Type u
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type v
inst✝¹ : MulAction R X
inst✝ : Finite ↥S
x : X
s : ↥S
⊢ ∃ a, (fun x ↦ x /ₒ 1) a = x /ₒ s

Tactic:
obtain ⟨i, j, hne, heq⟩ := Finite.exists_ne_map_eq_of_infinite (α := ℕ) (s ^ ·)

Goal state after:
R : Type u
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type v
inst✝¹ : MulAction R X
inst✝ : Finite ↥S
x : X
s : ↥S
i j : ℕ
hne : i ≠ j
heq : s ^ i = s ^ j
⊢ ∃ a, (fun x ↦ x /ₒ 1) a = x /ₒ s
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 ι
s : Finset R := (univ.biUnion fun i ↦ image (fun x ↦ coeff x (ps i)) (ps i).support) ∪ image v univ
hv : ∀ (i : ι), v i ∈ Algebra.adjoin K ↑s
hs₁ : ∀ (i : ι), ∀ k ∈ (ps i).support, coeff k (ps i) ∈ Algebra.adjoin K ↑s
this✝ : IsNoetherian K ↥(Algebra.adjoin K ↑s)
this : Finite ↥(Algebra.adjoin K ↑s)
S' : Set (ι → ↥(Algebra.adjoin K ↑s)) := (fun v ↦ Subtype.val ∘ v) ⁻¹' S
res : ↑S' → ↑S' := fun x ↦ ⟨fun i ↦ ⟨(eval fun j ↦ ↑(↑x j)) (ps i), ⋯⟩, ⋯⟩
⊢ v ∈ (fun v i ↦ (eval v) (ps i)) '' S

Tactic:
have hres_surj : Function.Surjective res := by
    rw [← Finite.injective_iff_surjective]
    intro x y hxy
    ext i
    simp only [Subtype.ext_iff, funext_iff] at hxy
    exact congr_fun (hinj x.2 y.2 (funext hxy)) i

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
hv : ∀ (i : ι), v i ∈ Algebra.adjoin K ↑s
hs₁ : ∀ (i : ι), ∀ k ∈ (ps i).support, coeff k (ps i) ∈ Algebra.adjoin K ↑s
this✝ : IsNoetherian K ↥(Algebra.adjoin K ↑s)
this : Finite ↥(Algebra.adjoin K ↑s)
S' : Set (ι → ↥(Algebra.adjoin K ↑s)) := (fun v ↦ Subtype.val ∘ v) ⁻¹' S
res : ↑S' → ↑S' := fun x ↦ ⟨fun i ↦ ⟨(eval fun j ↦ ↑(↑x j)) (ps i), ⋯⟩, ⋯⟩
hres_surj : Function.Surjective res
⊢ v ∈ (fun v i ↦ (eval v) (ps i)) '' S
Module: Mathlib.FieldTheory.AxGrothendieck

Goal state before:
pp: K : Type u_1
ι : Type u_2
inst✝³ : Field K
inst✝² : IsAlgClosed K
inst✝¹ : Finite ι
inst✝ : CompatibleRing K
c✝ : Set K
S : Set (ι → K)
ps : ι → MvPolynomial ι K
this✝ : Fintype ι := Fintype.ofFinite ι
p : ℕ := ringChar K
c : Finset K
left✝ : ↑c ⊆ c✝
φ : ring.Formula (↑↑c ⊕ ι)
hφ : S = {v | φ.Realize (Sum.elim Subtype.val v)}
this :
  ∀ (v : ↑↑c → K) (p : { p // ∀ (i : ι), (p i).support ⊆ (ps i).support }),
    have f := fun v i ↦ (eval v) (↑p i);
    have S := {x | φ.Realize (Sum.elim v x)};
    Set.MapsTo f S S → Set.InjOn f S → Set.SurjOn f S S
⊢ Set.MapsTo (fun v i ↦ (eval v) (ps i)) {v | φ.Realize (Sum.elim Subtype.val v)}
      {v | φ.Realize (Sum.elim Subtype.val v)} →
    Set.InjOn (fun v i ↦ (eval v) (ps i)) {v | φ.Realize (Sum.elim Subtype.val v)} →
      Set.SurjOn (fun v i ↦ (eval v) (ps i)) {v | φ.Realize (Sum.elim Subtype.val v)}
        {v | φ.Realize (Sum.elim Subtype.val v)}

Tactic:
exact this Subtype.val ⟨ps, fun i => Set.Subset.refl _⟩

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

Goal state before:
pp: R : Type u_1
inst✝⁶ : Field R
inst✝⁵ : Differential R
a b : R
F : Type u_2
inst✝⁴ : Field F
inst✝³ : Differential F
inst✝² : CharZero F
p : F[X]
inst✝¹ : Fact (Irreducible p)
inst✝ : Fact p.Monic
q : F[X]
⊢ p ∣
    (implicitDeriv
        ((AdjoinRoot.modByMonicHom ⋯)
          (-(aeval (AdjoinRoot.root p)) (mapCoeffs p) / (aeval (AdjoinRoot.root p)) (derivative p))))
      p

Tactic:
← AdjoinRoot.mk_eq_zero

Goal state after:
R : Type u_1
inst✝⁶ : Field R
inst✝⁵ : Differential R
a b : R
F : Type u_2
inst✝⁴ : Field F
inst✝³ : Differential F
inst✝² : CharZero F
p : F[X]
inst✝¹ : Fact (Irreducible p)
inst✝ : Fact p.Monic
q : F[X]
⊢ (AdjoinRoot.mk p)
      ((implicitDeriv
          ((AdjoinRoot.modByMonicHom ⋯)
            (-(aeval (AdjoinRoot.root p)) (mapCoeffs p) / (aeval (AdjoinRoot.root p)) (derivative p))))
        p) =
    0
Module: Mathlib.FieldTheory.Differential.Basic

Goal state before:
pp: R : Type u_1
inst✝⁶ : Field R
inst✝⁵ : Differential R
a b : R
F : Type u_2
inst✝⁴ : Field F
inst✝³ : Differential F
inst✝² : CharZero F
p : F[X]
inst✝¹ : Fact (Irreducible p)
inst✝ : Fact p.Monic
q : F[X]
⊢ (AdjoinRoot.mk p) (mapCoeffs p) +
      -(AdjoinRoot.mk p) (mapCoeffs p) / (AdjoinRoot.mk p) (derivative p) * (AdjoinRoot.mk p) (derivative p) =
    0

Tactic:
div_mul_cancel₀,

Goal state after:
R : Type u_1
inst✝⁶ : Field R
inst✝⁵ : Differential R
a b : R
F : Type u_2
inst✝⁴ : Field F
inst✝³ : Differential F
inst✝² : CharZero F
p : F[X]
inst✝¹ : Fact (Irreducible p)
inst✝ : Fact p.Monic
q : F[X]
⊢ (AdjoinRoot.mk p) (mapCoeffs p) + -(AdjoinRoot.mk p) (mapCoeffs p) = 0

case h
R : Type u_1
inst✝⁶ : Field R
inst✝⁵ : Differential R
a b : R
F : Type u_2
inst✝⁴ : Field F
inst✝³ : Differential F
inst✝² : CharZero F
p : F[X]
inst✝¹ : Fact (Irreducible p)
inst✝ : Fact p.Monic
q : F[X]
⊢ (AdjoinRoot.mk p) (derivative p) ≠ 0
Module: Mathlib.FieldTheory.Differential.Basic

Goal state before:
pp: R : Type u_1
inst✝⁷ : Field R
inst✝⁶ : Differential R
a b : R
F : Type u_2
inst✝⁵ : Field F
inst✝⁴ : Differential F
inst✝³ : CharZero F
K : Type u_3
inst✝² : Field K
inst✝¹ : Algebra F K
inst✝ : FiniteDimensional F K
⊢ Unique { _a // DifferentialAlgebra F K }

Tactic:
by
  let default : {_a : Differential K // DifferentialAlgebra F K} :=
      ⟨differentialFiniteDimensional F K, differentialAlgebraFiniteDimensional⟩
  refine ⟨⟨default⟩, fun ⟨a, ha⟩ ↦ ?_⟩
  ext x
  apply_fun (aeval x (mapCoeffs (minpoly F x)) + aeval x (derivative (minpoly F x)) * ·)
  · conv_lhs => apply (deriv_aeval_eq ..).symm
    conv_rhs => apply (@deriv_aeval_eq _ _ _ _ _ default.1 _ default.2 _ _).symm
    simp
  · apply (add_right_injective _).comp
    apply mul_right_injective₀
    rw [ne_eq, ← minpoly.dvd_iff]
    have : 0 < (minpoly F x).natDegree := Irreducible.natDegree_pos
      (minpoly.irreducible (Algebra.IsIntegral.isIntegral _))
    apply not_dvd_of_natDegree_lt
    · intro nh
      simp_all
    apply natDegree_derivative_lt
    exact Nat.ne_zero_of_lt this

Goal state after:
Module: Mathlib.FieldTheory.IsPerfectClosure

Goal state before:
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_bot hp, Ideal.mem_bot]

Goal state after:
case neg
R : Type u_1
inst✝ : CommSemiring R
p : ℕ
x : R
hp : ¬1 < p
⊢ x = 0 ↔ ∃ n, x ^ p ^ n = 0
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 : ℕ
ih : mk K p (n, 0) = 0
⊢ R K p (n, 0) (n + 1, 0)

Tactic:
have := R.intro (p := p) n (0 : K)

Goal state after:
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
n : ℕ
ih : mk K p (n, 0) = 0
this : R K p (n, 0) (n + 1, (frobenius K p) 0)
⊢ R K p (n, 0) (n + 1, 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
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
⊢ ∃ i, ⟨α, hα⟩ ∈ ↑(M i)

Tactic:
by
      have ⟨β, hβ⟩ := h α
      let ϕ : F⟮α⟯ →ₐ[F] K' := (IsScalarTower.toAlgHom _ _ _).comp
        ((AdjoinRoot.liftAlgHom _ _ _ hβ).comp
        (adjoinRootEquivAdjoin F <| (alg.isIntegral).1 _).symm.toAlgHom)
      have ⟨ω, hω⟩ := exists_algHom_adjoin_of_splits
        (fun s hs ↦ ⟨(alg.isIntegral).1 _, splits s hs⟩) ϕ (adjoin_simple_le_iff.mpr hα)
      refine ⟨ω, β, ((DFunLike.congr_fun hω <| AdjoinSimple.gen F α).trans ?_).symm⟩
      rw [AlgHom.comp_apply, AlgHom.comp_apply, AlgEquiv.coe_toAlgHom,
        adjoinRootEquivAdjoin_symm_apply_gen, AdjoinRoot.liftAlgHom_root]
      rfl

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
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] = 0

Tactic:
(Nat.sub_eq_iff_eq_add hn).1 rfl,

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 + p ^ m] = 0