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 : 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
hsne : s.Nonempty
hd : Disjoint s (a • V)
hgs : (fun x ↦ g * x) ⁻¹' s = s
⊢ False

Tactic:
cases hg.measure_self_or_compl_eq_zero hso.measurableSet hgs with
  | inl h => exact hso.measure_ne_zero _ hsne h
  | inr h =>
    refine (hVo.smul a).measure_ne_zero μ (.image _ ⟨1, hV₁⟩) (measure_mono_null ?_ h)
    rwa [disjoint_right] at hd

Goal state after:
Module: Mathlib.Dynamics.FixedPoints.Support

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
f g : X → X
hf : HasCompactFixedSupport f
hg : HasCompactFixedSupport g
⊢ HasCompactFixedSupport (f ∘ g)

Tactic:
by
  rw [HasCompactFixedSupport_iff'] at *
  obtain ⟨K, hK₁, hK₂, hf⟩ := hf
  obtain ⟨L, hL₁, hL₂, hg⟩ := hg
  refine ⟨K ∪ L, hK₁.union hL₁, hK₂.union hL₂, ?_⟩
  grw [← inter_subset_fixedPoints_comp, Set.compl_inter, hf, hg]

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 α
y : β
h : ∀ i ∈ f, ∀ t ∈ 𝓝 y, (t ∩ image2 ϕ i s).Nonempty
n✝ : Set β
hn : n✝ ∈ 𝓝 y
U✝ : Set τ
hu : U✝ ∈ f
w✝¹ : τ
ht : w✝¹ ∈ U✝
w✝ : α
hx : w✝ ∈ s
left✝ : ϕ w✝¹ w✝ ∈ n✝
⊢ w✝ ∈ ϕ w✝¹ ⁻¹' n✝

Tactic:
rwa [mem_preimage]

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν ν' : Measure α
inst✝¹ : μ.HaveLebesgueDecomposition ν'
inst✝ : SigmaFinite ν'
h : μ ⟂ₘ ν
hνν' : ν ≪ ν'
t : Set α := h.nullSet
⊢ μ.rnDeriv ν' =ᵐ[ν] 0

Tactic:
have ht : MeasurableSet t := h.measurableSet_nullSet

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ ν ν' : Measure α
inst✝¹ : μ.HaveLebesgueDecomposition ν'
inst✝ : SigmaFinite ν'
h : μ ⟂ₘ ν
hνν' : ν ≪ ν'
t : Set α := h.nullSet
ht : MeasurableSet t
⊢ μ.rnDeriv ν' =ᵐ[ν] 0
Module: Mathlib.Dynamics.OmegaLimit

Goal state before:
pp: τ : Type u_1
inst✝² : TopologicalSpace τ
inst✝¹ : AddCommGroup τ
α : Type u_2
inst✝ : TopologicalSpace α
f : Filter τ
ϕ : Flow τ α
s : Set α
hf : ∀ (t : τ), Tendsto (fun x ↦ t + x) f f
x✝ : α
h : ∀ n ∈ 𝓝 x✝, ∀ {U : Set τ}, U ∈ f → ∃ x ∈ U, (ϕ.toFun x '' ω f ϕ.toFun s ∩ n).Nonempty
n : Set α
hn : n ∈ 𝓝 x✝
u : Set τ
hu : u ∈ f
⊢ ∃ x ∈ u, (ϕ.toFun x '' s ∩ n).Nonempty

Tactic:
rcases mem_nhds_iff.mp hn with ⟨o, ho₁, ho₂, ho₃⟩

Goal state after:
τ : Type u_1
inst✝² : TopologicalSpace τ
inst✝¹ : AddCommGroup τ
α : Type u_2
inst✝ : TopologicalSpace α
f : Filter τ
ϕ : Flow τ α
s : Set α
hf : ∀ (t : τ), Tendsto (fun x ↦ t + x) f f
x✝ : α
h : ∀ n ∈ 𝓝 x✝, ∀ {U : Set τ}, U ∈ f → ∃ x ∈ U, (ϕ.toFun x '' ω f ϕ.toFun s ∩ n).Nonempty
n : Set α
hn : n ∈ 𝓝 x✝
u : Set τ
hu : u ∈ f
o : Set α
ho₁ : o ⊆ n
ho₂ : IsOpen[inst✝] o
ho₃ : x✝ ∈ o
⊢ ∃ x ∈ u, (ϕ.toFun x '' s ∩ n).Nonempty
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : SigmaFinite ν
⊢ ∫ (x : α), (μ.rnDeriv ν x).toReal ∂ν = (μ Set.univ - (μ.singularPart ν) Set.univ).toReal

Tactic:
← Measure.sub_apply .univ (Measure.singularPart_le μ ν),

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : SigmaFinite ν
⊢ ∫ (x : α), (μ.rnDeriv ν x).toReal ∂ν = ((μ - μ.singularPart ν) Set.univ).toReal
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
a : α
ha1 : ν.rnDeriv (μ + ν) a = (μ.rnDeriv ν a + 1)⁻¹
ha2 : μ.rnDeriv (μ + ν) a = μ.rnDeriv ν a / (μ.rnDeriv ν a + 1)
ha_lt_top : μ.rnDeriv ν a < ∞
⊢ μ.rnDeriv ν a = μ.rnDeriv (μ + ν) a / ν.rnDeriv (μ + ν) a

Tactic:
rw [ha1, ha2, ENNReal.div_eq_inv_mul, inv_inv, ENNReal.div_eq_inv_mul, ← mul_assoc,
      ENNReal.mul_inv_cancel, one_mul]

Goal state after:
case h0
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
a : α
ha1 : ν.rnDeriv (μ + ν) a = (μ.rnDeriv ν a + 1)⁻¹
ha2 : μ.rnDeriv (μ + ν) a = μ.rnDeriv ν a / (μ.rnDeriv ν a + 1)
ha_lt_top : μ.rnDeriv ν a < ∞
⊢ μ.rnDeriv ν a + 1 ≠ 0

case ht
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
a : α
ha1 : ν.rnDeriv (μ + ν) a = (μ.rnDeriv ν a + 1)⁻¹
ha2 : μ.rnDeriv (μ + ν) a = μ.rnDeriv ν a / (μ.rnDeriv ν a + 1)
ha_lt_top : μ.rnDeriv ν a < ∞
⊢ μ.rnDeriv ν a + 1 ≠ ∞
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: α : 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 < ∞
⊢ s = f ⁻¹' f '' s

Tactic:
hf.injective.preimage_image

Goal state after:
α : 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 < ∞
⊢ s = s
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
⊢ (map f μ).singularPart (map f ν) = map f (μ.singularPart ν)

Tactic:
have h_add : μ.map f = (μ.singularPart ν).map f
      + (ν.map f).withDensity ((μ.map f).rnDeriv (ν.map f)) := by
    conv_lhs => rw [μ.haveLebesgueDecomposition_add ν]
    rw [Measure.map_add _ _ hf.measurable, ← hf.map_withDensity_rnDeriv μ ν]

Goal state after:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
h_add : map f μ = map f (μ.singularPart ν) + (map f ν).withDensity ((map f μ).rnDeriv (map f ν))
⊢ (map f μ).singularPart (map f ν) = map f (μ.singularPart ν)
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 u v, w} #ι ≤ ℵ₀

Tactic:
by simpa using le_of_lt h

Goal state after:
Module: Mathlib.FieldTheory.AbelRuffini

Goal state before:
pp: F : Type u_3
inst✝¹ : Field F
E : Type u_4
inst✝ : Field E
i : F →+* E
n : ℕ
a : F
ha : a ≠ 0
h : (map i (X ^ n - C a)).Splits
ha' : i a ≠ 0
hn : ¬n = 0
hn' : 0 < n
hn'' : (X ^ n - C a).degree ≠ 0
b : E
hb : b ^ n = i a
hb' : b ≠ 0
s : Multiset E := (map i (X ^ n - C a)).roots
hs : map i (X ^ n - C a) = (Multiset.map (fun x ↦ X - C x) s).prod
hs' : s.card = n
⊢ C 1 = 1

Tactic:
C_1

Goal state after:
F : Type u_3
inst✝¹ : Field F
E : Type u_4
inst✝ : Field E
i : F →+* E
n : ℕ
a : F
ha : a ≠ 0
h : (map i (X ^ n - C a)).Splits
ha' : i a ≠ 0
hn : ¬n = 0
hn' : 0 < n
hn'' : (X ^ n - C a).degree ≠ 0
b : E
hb : b ^ n = i a
hb' : b ≠ 0
s : Multiset E := (map i (X ^ n - C a)).roots
hs : map i (X ^ n - C a) = (Multiset.map (fun x ↦ X - C x) s).prod
hs' : s.card = n
⊢ 1 = 1
Module: Mathlib.ModelTheory.Basic

Goal state before:
pp: L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M ≃[L] N
x✝ : M
⊢ f.symm (f x✝) = (refl L M) x✝

Tactic:
symm_apply_apply,

Goal state after:
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M ≃[L] N
x✝ : M
⊢ x✝ = (refl L M) x✝
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 : E
hx : x ∈ solvableByRad F E
n : ℕ
hn : n ≠ 0
hα : Group.IsSolvable (minpoly F (x ^ n)).Gal
p : F[X] := minpoly F (x ^ n)
hp : p.comp (X ^ n) ≠ 0
⊢ (aeval x) (p.comp (X ^ n)) = 0

Tactic:
aeval_comp,

Goal state after:
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
x : E
hx : x ∈ solvableByRad F E
n : ℕ
hn : n ≠ 0
hα : Group.IsSolvable (minpoly F (x ^ n)).Gal
p : F[X] := minpoly F (x ^ n)
hp : p.comp (X ^ n) ≠ 0
⊢ (aeval ((aeval x) (X ^ n))) p = 0
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: L : Language
L' : Language
M : Type w
α : Type u'
β : Type v'
γ : Type u_1
n x✝¹ n' m : ℕ
φ : L.BoundedFormula α x✝¹
x✝ : ℕ
⊢ x✝ + 1 + n' ≤ x✝ + n' + 1

Tactic:
by rw [add_assoc, add_comm 1, add_assoc]

Goal state after:
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: L : Language
L' : Language
α : Type u'
n : ℕ
L'' : Language
φ : L' →ᴸ L''
ψ : L →ᴸ L'
f : L.BoundedFormula α n
⊢ (φ.comp ψ).onBoundedFormula f = (φ.onBoundedFormula ∘ ψ.onBoundedFormula) f

Tactic:
induction f with
  | falsum => rfl
  | equal => simp [Term.bdEqual]
  | rel => simp only [onBoundedFormula, comp_onRelation, comp_onTerm, Function.comp_apply]; rfl
  | imp _ _ ih1 ih2 =>
    simp only [onBoundedFormula, Function.comp_apply, ih1, ih2]
  | all _ ih3 => simp only [ih3, onBoundedFormula, Function.comp_apply]

Goal state after:
Module: Mathlib.ModelTheory.Ultraproducts

Goal state before:
pp: α : 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 β
⊢ Term.realize (fun i ↦ Quotient.mk' (x i)) t = Quotient.mk' fun a ↦ Term.realize (fun i ↦ x i a) t

Tactic:
by
  convert!
    @Term.realize_quotient_mk' L _ ((u : Filter α).productSetoid M)
      (Ultraproduct.setoidPrestructure M u) _ t x using 2
  ext a
  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: L : Language
α : Type u'
l : List ((n : ℕ) × L.BoundedFormula α n)
⊢ ∀ (φ : (n : ℕ) × L.BoundedFormula α n) (l' : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)),
    listDecode (φ.snd.listEncode ++ l') = φ :: listDecode l'

Tactic:
rintro ⟨n, φ⟩

Goal state after:
L : Language
α : Type u'
l : List ((n : ℕ) × L.BoundedFormula α n)
n : ℕ
φ : L.BoundedFormula α n
⊢ ∀ (l' : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)),
    listDecode (⟨n, φ⟩.snd.listEncode ++ l') = ⟨n, φ⟩ :: listDecode l'
Module: Mathlib.ModelTheory.Definability

Goal state before:
pp: M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
s : Set (α → M)
φ : L[[↑A]].Formula α
hφ : s = ofPred φ.Realize
v : α → M
⊢ v ∈ (ofPred φ.Realize)ᶜ ↔ v ∈ ofPred φ.not.Realize

Tactic:
compl_ofPred,

Goal state after:
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
s : Set (α → M)
φ : L[[↑A]].Formula α
hφ : s = ofPred φ.Realize
v : α → M
⊢ v ∈ {a | ¬φ.Realize a} ↔ v ∈ ofPred φ.not.Realize
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 ⊨ ψ
⊢ (D ∩ ↑S).Nonempty

Tactic:
have hψS : ψ.Realize S := by
    rwa [← Formula.realize_equivSentence_symm_con, ← S.subtype.map_formula,
      Formula.realize_equivSentence_symm]

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 ⊨ ψ
hψS : ↥S ⊨ ψ
⊢ (D ∩ ↑S).Nonempty
Module: Mathlib.ModelTheory.Satisfiability

Goal state before:
pp: L : Language
T : L.Theory
h : T.IsFinitelySatisfiable
M : Finset ↑T → Type (max u v) := fun T0 ↦ ↑(Nonempty.some ⋯)
M' : Type (max u v) := (↑(Ultrafilter.of Filter.atTop)).Product M
⊢ M' ⊨ T

Tactic:
refine ⟨fun φ hφ => ?_⟩

Goal state after:
L : Language
T : L.Theory
h : T.IsFinitelySatisfiable
M : Finset ↑T → Type (max u v) := fun T0 ↦ ↑(Nonempty.some ⋯)
M' : Type (max u v) := (↑(Ultrafilter.of Filter.atTop)).Product M
φ : L.Sentence
hφ : φ ∈ T
⊢ M' ⊨ φ
Module: Mathlib.ModelTheory.Definability

Goal state before:
pp: M : Type w
L : Language
inst✝ : L.Structure M
α : Type u₁
f : (α → M) → M
⊢ (∃ φ, f = fun v ↦ Term.realize v φ) ↔ ∃ φ, f = fun v ↦ Term.realize v φ

Tactic:
Equiv.exists_congr_left (LEquiv.addEmptyConstants L (∅ : Set M)).onTerm

Goal state after:
M : Type w
L : Language
inst✝ : L.Structure M
α : Type u₁
f : (α → M) → M
⊢ (∃ φ, f = fun v ↦ Term.realize v φ) ↔ ∃ b, f = fun v ↦ Term.realize v ((LEquiv.addEmptyConstants L ↑∅).onTerm.symm b)
Module: Mathlib.ModelTheory.Satisfiability

Goal state before:
pp: L : Language
T : L.Theory
κ : Cardinal.{w}
M : Type w'
inst✝² : L.Structure M
inst✝¹ : M ⊨ T
inst✝ : Infinite M
N : ((L.lhomWithConstants (Quotient.out κ)).onTheory T ∪ L.distinctConstantsTheory Set.univ).ModelType
this : ↑N ⊨ L.distinctConstantsTheory Set.univ
⊢ lift.{max (max u v) w, w} #(Quotient.out κ) ≤ #↑N

Tactic:
← mk_univ

Goal state after:
L : Language
T : L.Theory
κ : Cardinal.{w}
M : Type w'
inst✝² : L.Structure M
inst✝¹ : M ⊨ T
inst✝ : Infinite M
N : ((L.lhomWithConstants (Quotient.out κ)).onTheory T ∪ L.distinctConstantsTheory Set.univ).ModelType
this : ↑N ⊨ L.distinctConstantsTheory Set.univ
⊢ lift.{max (max u v) w, w} #↑Set.univ ≤ #↑N
Module: Mathlib.ModelTheory.Algebra.Field.IsAlgClosed

Goal state before:
pp: p✝ : ℕ
K : Type u_2
inst✝¹ : Field K
inst✝ : CompatibleRing K
h : K ⊨ Theory.ACF p✝
p : K[X]
hpm : p.Monic
⊢ Irreducible p → ∃ x, eval x p = 0

Tactic:
hpi

Goal state after:
p✝ : ℕ
K : Type u_2
inst✝¹ : Field K
inst✝ : CompatibleRing K
h : K ⊨ Theory.ACF p✝
p : K[X]
hpm : p.Monic
hpi : Irreducible p
⊢ ∃ x, eval x p = 0
Module: Mathlib.RingTheory.MvPolynomial.FreeCommRing

Goal state before:
pp: ι : Type u_1
κ : Type u_2
R : Type u_3
inst✝² : DecidableEq κ
inst✝¹ : CommRing R
inst✝ : DecidableEq R
monoms : ι → Finset (κ →₀ ℕ)
p : { p // ∀ (i : ι), (p i).support ⊆ monoms i }
⊢ (fun p ↦
        ⟨fun i ↦
          AddMonoidAlgebra.ofCoeff
            { support := {m ∈ monoms i | ∃ (hm : m ∈ monoms i), p ⟨i, ⟨m, hm⟩⟩ ≠ 0},
              toFun := fun m ↦ if hm : m ∈ monoms i then p ⟨i, ⟨m, hm⟩⟩ else 0, mem_support_toFun := ⋯ },
          ⋯⟩)
      ((fun p i ↦ coeff (↑i.snd) (↑p i.fst)) p) =
    p

Tactic:
by
      ext i m
      simp only [coeff, ne_eq, exists_prop, dite_eq_ite, Finsupp.coe_mk, ite_eq_left_iff]
      intro hm
      have : m ∉ (p.1 i).support := fun h => hm (p.2 i h)
      simpa [coeff, eq_comm, MvPolynomial.mem_support_iff] using this

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

Goal state before:
pp: ι : Type u_1
K : Type u_2
inst✝¹ : Field K
inst✝ : CompatibleRing K
S : Finset (MvPolynomial ι K)
⊢ (⋃ p ∈ S, (fun m ↦ coeff m p) '' ↑p.support).Definable ring (zeroLocus K (Ideal.span ↑S))

Tactic:
Set.definable_iff_exists_formula_sum

Goal state after:
ι : Type u_1
K : Type u_2
inst✝¹ : Field K
inst✝ : CompatibleRing K
S : Finset (MvPolynomial ι K)
⊢ ∃ φ, zeroLocus K (Ideal.span ↑S) = {v | φ.Realize (Sum.elim Subtype.val v)}
Module: Mathlib.ModelTheory.Satisfiability

Goal state before:
pp: case refine_2
L : Language
T : L.Theory
α : Type w
φ : L.Formula α
h : (L.lhomWithConstants α).onTheory T ⊨ᵇ Formula.equivSentence φ
M : T.ModelType
v : α → ↑M
this : (constantsOn α).Structure ↑M := constantsOn.structure v
⊢ φ.Realize v

Tactic:
have : M ⊨ (L.lhomWithConstants α).onTheory T := (LHom.onTheory_model _ _).2 inferInstance

Goal state after:
case refine_2
L : Language
T : L.Theory
α : Type w
φ : L.Formula α
h : (L.lhomWithConstants α).onTheory T ⊨ᵇ Formula.equivSentence φ
M : T.ModelType
v : α → ↑M
this✝ : (constantsOn α).Structure ↑M := constantsOn.structure v
this : ↑M ⊨ (L.lhomWithConstants α).onTheory T
⊢ φ.Realize v
Module: Mathlib.ModelTheory.Satisfiability

Goal state before:
pp: L : Language
T : L.Theory
α : Type w
φ : L.Formula α
h : (L.lhomWithConstants α).onTheory T ⊨ᵇ Formula.equivSentence φ
M : Type u_1
inst✝² : L.Structure M
inst✝¹ : M ⊨ T
inst✝ : Nonempty M
v : α → M
this : (constantsOn α).Structure M := constantsOn.structure v
⊢ φ.Realize v

Tactic:
have : M ⊨ (L.lhomWithConstants α).onTheory T := (LHom.onTheory_model _ _).2 inferInstance

Goal state after:
L : Language
T : L.Theory
α : Type w
φ : L.Formula α
h : (L.lhomWithConstants α).onTheory T ⊨ᵇ Formula.equivSentence φ
M : Type u_1
inst✝² : L.Structure M
inst✝¹ : M ⊨ T
inst✝ : Nonempty M
v : α → M
this✝ : (constantsOn α).Structure M := constantsOn.structure v
this : M ⊨ (L.lhomWithConstants α).onTheory T
⊢ φ.Realize v
Module: Mathlib.ModelTheory.Satisfiability

Goal state before:
pp: case refine_2
L : Language
T : L.Theory
α : Type w
n : ℕ
φ : L.BoundedFormula α n
⊢ T ⊨ᵇ φ → ∀ (M : T.ModelType) (v : α ⊕ Fin n → ↑M), φ.Realize (v ∘ Sum.inl) (v ∘ Sum.inr)

Tactic:
exact fun h M v => h M _ _

Goal state after:
Module: Mathlib.FieldTheory.AxGrothendieck

Goal state before:
pp: ι : 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
⊢ Set.SurjOn (fun v i ↦ (eval v) (ps i)) S S

Tactic:
have is_int : ∀ x : R, IsIntegral K x := fun x => isAlgebraic_iff_isIntegral.1
    (alg.isAlgebraic x)
  classical
  intro v hvS
  cases nonempty_fintype ι
  /- `s` is the set of all coefficients of the polynomial, as well as all of
    the coordinates of `v`, the point I am trying to find the preimage of. -/
  let s : Finset R :=
    (Finset.biUnion (univ : Finset ι) fun i => (ps i).support.image fun x => coeff x (ps i)) ∪
      (univ : Finset ι).image v
  have hv : ∀ i, v i ∈ Algebra.adjoin K (s : Set R) := fun j =>
    Algebra.subset_adjoin (mem_union_right _ (mem_image.2 ⟨j, mem_univ _, rfl⟩))
  have hs₁ : ∀ (i : ι) (k : ι →₀ ℕ),
      k ∈ (ps i).support → coeff k (ps i) ∈ Algebra.adjoin K (s : Set R) :=
    fun i k hk => Algebra.subset_adjoin
      (mem_union_left _ (mem_biUnion.2 ⟨i, mem_univ _, mem_image_of_mem _ hk⟩))
  have := isNoetherian_adjoin_finset s fun x _ => is_int x
  have : Finite (Algebra.adjoin K (s : Set R)) := Module.finite_of_finite K
  -- The restriction of the polynomial map, `ps`, to the subalgebra generated by `s`
  let S' : Set (ι → Algebra.adjoin K (s : Set R)) :=
    (fun v => Subtype.val ∘ v) ⁻¹' S
  let res : S' → S' := fun x => ⟨fun i =>
    ⟨eval (fun j : ι => (x.1 j : R)) (ps i), eval_mem (hs₁ _) fun i => (x.1 i).2⟩,
      hm x.2⟩
  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
  rcases hres_surj ⟨fun i => ⟨v i, hv i⟩, hvS⟩ with ⟨⟨w, hwS'⟩, hw⟩
  refine ⟨fun i => w i, hwS', ?_⟩
  simpa [Subtype.ext_iff, funext_iff] using hw

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

Goal state before:
pp: n m : ℕ
k : Cardinal.{u_1}
hk : ↑m = ↑n * k
this : ↑n = 0 ∨ k = 0 ∨ ↑n < ℵ₀ ∧ k < ℵ₀
⊢ n ∣ m

Tactic:
rcases this with (h | h | ⟨-, hk'⟩)

Goal state after:
case inl
n m : ℕ
k : Cardinal.{u_1}
hk : ↑m = ↑n * k
h : ↑n = 0
⊢ n ∣ m

case inr.inl
n m : ℕ
k : Cardinal.{u_1}
hk : ↑m = ↑n * k
h : k = 0
⊢ n ∣ m

case inr.inr
n m : ℕ
k : Cardinal.{u_1}
hk : ↑m = ↑n * k
hk' : k < ℵ₀
⊢ n ∣ m
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✝
hS : (↑c).Definable ring S
⊢ Set.MapsTo (fun v i ↦ (eval v) (ps i)) S S →
    Set.InjOn (fun v i ↦ (eval v) (ps i)) S → Set.SurjOn (fun v i ↦ (eval v) (ps i)) S S

Tactic:
Set.definable_iff_exists_formula_sum

Goal state after:
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✝
hS : ∃ φ, S = {v | φ.Realize (Sum.elim Subtype.val v)}
⊢ Set.MapsTo (fun v i ↦ (eval v) (ps i)) S S →
    Set.InjOn (fun v i ↦ (eval v) (ps i)) S → Set.SurjOn (fun v i ↦ (eval v) (ps i)) S S
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✝² : CommSemiring K
inst✝¹ : CommSemiring L
inst✝ : CommSemiring M
i : K →+* L
j : K →+* M
f : L →+* M
p : ℕ
x : K
h : x ∈ RingHom.ker (RingHom.id K)
⊢ x ∈ pNilradical K p

Tactic:
by convert! Ideal.zero_mem _

Goal state after:
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 : x ^ (p ^ n' * p ^ n) = i y ^ p ^ n'
⊢ (iterateFrobeniusEquiv M p n').symm (j (Classical.choose ⋯).2) = (iterateFrobeniusEquiv M p n).symm (j y)

Tactic:
pow_mul,

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 : (x ^ p ^ n') ^ p ^ n = i y ^ p ^ n'
⊢ (iterateFrobeniusEquiv M p n').symm (j (Classical.choose ⋯).2) = (iterateFrobeniusEquiv M p n).symm (j y)
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
⊢ j ((Classical.choose ⋯).2 ^ (p ^ n * p ^ m) - y ^ p ^ (n' + m)) = 0

Tactic:
pow_mul,

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
⊢ j (((Classical.choose ⋯).2 ^ p ^ n) ^ p ^ m - y ^ p ^ (n' + m)) = 0