mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Instances.AddCircle.DenseSubgroup

Goal state before:
pp: a b : ℝ
⊢ Dense ↑(AddSubgroup.closure {a, b}) ↔ Irrational (a / b)

Tactic:
rcases eq_or_ne b 0 with rfl | hb

Goal state after:
case inl
a : ℝ
⊢ Dense ↑(AddSubgroup.closure {a, 0}) ↔ Irrational (a / 0)

case inr
a b : ℝ
hb : b ≠ 0
⊢ Dense ↑(AddSubgroup.closure {a, b}) ↔ Irrational (a / b)
Module: Mathlib.Dynamics.Ergodic.Conservative

Goal state before:
pp: case succ.refine_1
α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
μ : Measure α
hf : Conservative f μ
n : ℕ
s : Set α
hs : MeasurableSet s
hs0 : μ s ≠ 0
x : α
left✝ : x ∈ s
hx : {n | f^[n] x ∈ s}.Infinite
k : ℕ
hk : k ∈ {n | f^[n] x ∈ s}
l : ℕ
hl : l ∈ {n | f^[n] x ∈ s}
hkl : k < l
hn : k ≡ l [MOD n.succ]
m : ℕ := (l - k) / (n + 1)
this : l ≤ k
hm : m = 0
⊢ False

Tactic:
exact this.not_gt hkl

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : ν.HaveLebesgueDecomposition μ
inst✝ : SigmaFinite μ
hμν : μ ≪ ν
x : α
hx : 0 < (μ.withDensity (ν.rnDeriv μ)).rnDeriv μ x
hx2 : (μ.withDensity (ν.rnDeriv μ)).rnDeriv μ x = ν.rnDeriv μ x
⊢ 0 < ν.rnDeriv μ x

Tactic:
rwa [← hx2]

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

Goal state before:
pp: X : Type u_1
T : X → X
U : SetRel X X
inst✝ : UniformSpace X
h : UniformContinuous T
U_uni : U ∈ 𝓤 X
n : ℕ
⊢ dynEntourage T U n ∈ 𝓤 X

Tactic:
dynEntourage_eq_inter_Ico T U n

Goal state after:
X : Type u_1
T : X → X
U : SetRel X X
inst✝ : UniformSpace X
h : UniformContinuous T
U_uni : U ∈ 𝓤 X
n : ℕ
⊢ ⋂ k, (map T T)^[↑k] ⁻¹' U ∈ 𝓤 X
Module: Mathlib.Dynamics.TopologicalEntropy.DynamicalEntourage

Goal state before:
pp: X : Type u_1
U : SetRel X X
inst✝ : TopologicalSpace X
T : X → X
T_cont : Continuous[inst✝, inst✝] T
U_open : IsOpen[instTopologicalSpaceProd] U
n : ℕ
⊢ IsOpen[instTopologicalSpaceProd] (Dynamics.dynEntourage T U n)

Tactic:
dynEntourage_eq_inter_Ico T U n

Goal state after:
X : Type u_1
U : SetRel X X
inst✝ : TopologicalSpace X
T : X → X
T_cont : Continuous[inst✝, inst✝] T
U_open : IsOpen[instTopologicalSpaceProd] U
n : ℕ
⊢ IsOpen[instTopologicalSpaceProd] (⋂ k, (map T T)^[↑k] ⁻¹' U)
Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy

Goal state before:
pp: X : Type u_1
T : X → X
U : SetRel X X
n : ℕ
⊢ netMaxcard T ∅ U n = 0

Tactic:
by
  rw [netMaxcard, ← bot_eq_zero, iSup₂_eq_bot]
  intro s s_net
  replace s_net := subset_empty_iff.1 s_net.1
  norm_cast at s_net
  rw [s_net, Finset.card_empty, CharP.cast_eq_zero, bot_eq_zero']

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

Goal state before:
pp: case inr
X : Type u_1
Y : Type u_2
V : SetRel Y Y
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F : Set X
inst✝ : V.IsSymm
n : ℕ
h' : coverMincard T (φ '' F) V n < ⊤
t : Finset Y
t_cover : IsDynCoverOf T (φ '' F) V n ↑t
t_card : ↑t.card = coverMincard T (φ '' F) V n
s : Finset X
s_cover : IsDynCoverOf S F (map φ φ ⁻¹' (V ○ V)) n ↑s
s_card : s.card ≤ t.card
⊢ coverMincard S F (map φ φ ⁻¹' (V ○ V)) n ≤ coverMincard T (φ '' F) V n

Tactic:
rw [← t_card]

Goal state after:
case inr
X : Type u_1
Y : Type u_2
V : SetRel Y Y
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F : Set X
inst✝ : V.IsSymm
n : ℕ
h' : coverMincard T (φ '' F) V n < ⊤
t : Finset Y
t_cover : IsDynCoverOf T (φ '' F) V n ↑t
t_card : ↑t.card = coverMincard T (φ '' F) V n
s : Finset X
s_cover : IsDynCoverOf S F (map φ φ ⁻¹' (V ○ V)) n ↑s
s_card : s.card ≤ t.card
⊢ coverMincard S F (map φ φ ⁻¹' (V ○ V)) n ≤ ↑t.card
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
this :
  (μ.rnDeriv ν)⁻¹ =ᵐ[μ] (μ.rnDeriv (μ.withDensity (ν.rnDeriv μ)))⁻¹ ∧
    ν.rnDeriv μ =ᵐ[μ] (μ.withDensity (ν.rnDeriv μ)).rnDeriv μ
⊢ (μ.rnDeriv ν)⁻¹ =ᵐ[μ] ν.rnDeriv μ

Tactic:
by
    refine (this.1.trans (Filter.EventuallyEq.trans ?_ this.2.symm))
    exact Measure.inv_rnDeriv_aux (absolutelyContinuous_withDensity_rnDeriv hμν)
      (withDensity_absolutelyContinuous _ _)

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

Goal state before:
pp: X : Type u_1
T : X → X
F : Set X
U : SetRel X X
n : ℕ
⊢ coverMincard T F U n ≠ 0 ↔ F.Nonempty

Tactic:
nonempty_iff_ne_empty,

Goal state after:
X : Type u_1
T : X → X
F : Set X
U : SetRel X X
n : ℕ
⊢ coverMincard T F U n ≠ 0 ↔ F ≠ ∅
Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy

Goal state before:
pp: case inr.inr
X : Type u_1
T : X → X
U : SetRel X X
F : Set X
F_inv : MapsTo T F F
inst✝ : U.IsSymm
m n : ℕ
F_nonempty : F.Nonempty
hn : n ≠ 0
⊢ coverMincard T F (U ○ U) (m * n) ≤ coverMincard T F U m ^ n

Tactic:
rcases eq_top_or_lt_top (coverMincard T F U m) with h | h

Goal state after:
case inr.inr.inl
X : Type u_1
T : X → X
U : SetRel X X
F : Set X
F_inv : MapsTo T F F
inst✝ : U.IsSymm
m n : ℕ
F_nonempty : F.Nonempty
hn : n ≠ 0
h : coverMincard T F U m = ⊤
⊢ coverMincard T F (U ○ U) (m * n) ≤ coverMincard T F U m ^ n

case inr.inr.inr
X : Type u_1
T : X → X
U : SetRel X X
F : Set X
F_inv : MapsTo T F F
inst✝ : U.IsSymm
m n : ℕ
F_nonempty : F.Nonempty
hn : n ≠ 0
h : coverMincard T F U m < ⊤
⊢ coverMincard T F (U ○ U) (m * n) ≤ coverMincard T F U m ^ n
Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy

Goal state before:
pp: X : Type u_1
F : Set X
inst✝ : UniformSpace X
T : X → X
h : MapsTo T F F
U : Set (X × X)
U_uni : U ∈ 𝓤 X
V : Set (X × X)
V_uni : V ∈ 𝓤 X
V_symm : SetRel.IsSymm V
V_U : V ○ V ⊆ U
⊢ coverEntropyEntourage T F U ≤ coverEntropyInf T F

Tactic:
exact (coverEntropyEntourage_antitone T F V_U).trans <| le_iSup₂_of_le V V_uni <|
     coverEntropyEntourage_le_coverEntropyInfEntourage h

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

Goal state before:
pp: X : Type u_1
T : X → X
F G : Set X
U : SetRel X X
n : ℕ
hF : coverMincard T F U n < ⊤
hG : coverMincard T G U n < ⊤
s : Finset X
s_cover : IsDynCoverOf T F U n ↑s
s_coverMincard : ↑s.card = coverMincard T F U n
t : Finset X
t_cover : IsDynCoverOf T G U n ↑t
t_coverMincard : ↑t.card = coverMincard T G U n
⊢ IsDynCoverOf T (F ∪ G) U n ↑(s ∪ t)

Tactic:
s.coe_union t

Goal state after:
X : Type u_1
T : X → X
F G : Set X
U : SetRel X X
n : ℕ
hF : coverMincard T F U n < ⊤
hG : coverMincard T G U n < ⊤
s : Finset X
s_cover : IsDynCoverOf T F U n ↑s
s_coverMincard : ↑s.card = coverMincard T F U n
t : Finset X
t_cover : IsDynCoverOf T G U n ↑t
t_coverMincard : ↑t.card = coverMincard T G U n
⊢ IsDynCoverOf T (F ∪ G) U n (↑s ∪ ↑t)
Module: Mathlib.Dynamics.TopologicalEntropy.Subset

Goal state before:
pp: X : Type u_1
T : X → X
F G : Set X
U : SetRel X X
n : ℕ
hF : coverMincard T F U n < ⊤
hG : coverMincard T G U n < ⊤
s : Finset X
s_cover : IsDynCoverOf T F U n ↑s
s_coverMincard : ↑s.card = coverMincard T F U n
t : Finset X
t_cover : IsDynCoverOf T G U n ↑t
t_coverMincard : ↑t.card = coverMincard T G U n
⊢ IsDynCoverOf T (F ∪ G) U n (↑s ∪ ↑t)

Tactic:
exact s_cover.union t_cover

Goal state after:
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 + 1) / (μ.rnDeriv ν a + 1)⁻¹

Tactic:
ENNReal.div_eq_inv_mul,

Goal state after:
α : 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 + 1)⁻¹⁻¹ * (μ.rnDeriv ν a / (μ.rnDeriv ν a + 1))
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 + 1) * (μ.rnDeriv ν a / (μ.rnDeriv ν a + 1))

Tactic:
ENNReal.div_eq_inv_mul,

Goal state after:
α : 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 + 1) * ((μ.rnDeriv ν a + 1)⁻¹ * μ.rnDeriv ν a)
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 (i a⁻¹) * C (i a) = 1

Tactic:
rw [← C_mul, ← i.map_mul, inv_mul_cancel₀ ha, i.map_one, C_1]

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

Goal state before:
pp: K : Type u
L : Type v
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : IsAlgClosed K
inst✝² : IsAlgClosed L
p : ℕ
inst✝¹ : CharP K p
inst✝ : CharP L p
hK : ℵ₀ < #K
hKL : Nonempty (K ≃ L)
⊢ Nonempty (K ≃+* L)

Tactic:
by
  rcases CharP.char_is_prime_or_zero K p with (hp | hp)
  · have : Fact p.Prime := ⟨hp⟩
    exact ringEquiv_of_Cardinal_eq_of_charP p hK hKL
  · simp only [hp] at *
    let : CharZero K := CharP.charP_to_charZero K
    let : CharZero L := CharP.charP_to_charZero L
    exact ringEquiv_of_equiv_of_charZero hK hKL

Goal state after:
Module: Mathlib.FieldTheory.AbelRuffini

Goal state before:
pp: case neg.hq
F : Type u_1
inst✝ : Field F
n : ℕ
x : F
hx : ¬x = 0
⊢ Group.IsSolvable (map (algebraMap F (X ^ n - 1).SplittingField) (X ^ n - C x)).Gal

Tactic:
rw [Polynomial.map_sub, Polynomial.map_pow, map_X, map_C]

Goal state after:
case neg.hq
F : Type u_1
inst✝ : Field F
n : ℕ
x : F
hx : ¬x = 0
⊢ Group.IsSolvable (X ^ n - C ((algebraMap F (X ^ n - 1).SplittingField) x)).Gal
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: case func.zero.inl
L : Language
L' : Language
M : Type w
α : Type u'
β : Type v'
γ : Type u_1
_ts✝ : Fin 0 → L[[γ]].Term α
ih : ∀ (a : Fin 0), (_ts✝ a).constantsToVars.varsToConstants = _ts✝ a
val✝ : L.Functions 0
⊢ (func (Sum.inl val✝) _ts✝).constantsToVars.varsToConstants = func (Sum.inl val✝) _ts✝

pp: case func.zero.inr
L : Language
L' : Language
M : Type w
α : Type u'
β : Type v'
γ : Type u_1
_ts✝ : Fin 0 → L[[γ]].Term α
ih : ∀ (a : Fin 0), (_ts✝ a).constantsToVars.varsToConstants = _ts✝ a
val✝ : (constantsOn γ).Functions 0
⊢ (func (Sum.inr val✝) _ts✝).constantsToVars.varsToConstants = func (Sum.inr val✝) _ts✝

Tactic:
· simp [constantsToVars, varsToConstants, ih]

Goal state after:
case func.zero.inr
L : Language
L' : Language
M : Type w
α : Type u'
β : Type v'
γ : Type u_1
_ts✝ : Fin 0 → L[[γ]].Term α
ih : ∀ (a : Fin 0), (_ts✝ a).constantsToVars.varsToConstants = _ts✝ a
val✝ : (constantsOn γ).Functions 0
⊢ (func (Sum.inr val✝) _ts✝).constantsToVars.varsToConstants = func (Sum.inr val✝) _ts✝
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: case func.succ.inl
L : Language
L' : Language
M : Type w
α : Type u'
β : Type v'
γ : Type u_1
n✝ : ℕ
_ts✝ : Fin (n✝ + 1) → L[[γ]].Term α
ih : ∀ (a : Fin (n✝ + 1)), (_ts✝ a).constantsToVars.varsToConstants = _ts✝ a
val✝ : L.Functions (n✝ + 1)
⊢ (func (Sum.inl val✝) _ts✝).constantsToVars.varsToConstants = func (Sum.inl val✝) _ts✝

pp: case func.succ.inr
L : Language
L' : Language
M : Type w
α : Type u'
β : Type v'
γ : Type u_1
n✝ : ℕ
_ts✝ : Fin (n✝ + 1) → L[[γ]].Term α
ih : ∀ (a : Fin (n✝ + 1)), (_ts✝ a).constantsToVars.varsToConstants = _ts✝ a
f : (constantsOn γ).Functions (n✝ + 1)
⊢ (func (Sum.inr f) _ts✝).constantsToVars.varsToConstants = func (Sum.inr f) _ts✝

Tactic:
· simp [constantsToVars, varsToConstants, ih]

Goal state after:
case func.succ.inr
L : Language
L' : Language
M : Type w
α : Type u'
β : Type v'
γ : Type u_1
n✝ : ℕ
_ts✝ : Fin (n✝ + 1) → L[[γ]].Term α
ih : ∀ (a : Fin (n✝ + 1)), (_ts✝ a).constantsToVars.varsToConstants = _ts✝ a
f : (constantsOn γ).Functions (n✝ + 1)
⊢ (func (Sum.inr f) _ts✝).constantsToVars.varsToConstants = func (Sum.inr f) _ts✝
Module: Mathlib.FieldTheory.AbelRuffini

Goal state before:
pp: case inr
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
x z : E
hx : x ∈ solvableByRad F E
hz : z ∈ solvableByRad F E
hx' : Group.IsSolvable (minpoly F x).Gal
p : F[X] := minpoly F x
a : E
hy : a ∈ solvableByRad F E
hy' : Group.IsSolvable (minpoly F a).Gal
hz' : z ∈ F⟮x, a⟯
q : F[X] := minpoly F a
hpq :
  (Polynomial.map (algebraMap F (p * q).SplittingField) (minpoly F x)).Splits ∧
    (Polynomial.map (algebraMap F (p * q).SplittingField) (minpoly F a)).Splits
⊢ IsIntegral F a ∧ (Polynomial.map (algebraMap F (p * q).SplittingField) (minpoly F a)).Splits

Tactic:
exact ⟨isIntegral_of_mem_solvableByRad hy, hpq.2⟩

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
k : ℕ
l : List (L.BoundedFormula α k)
f : L.BoundedFormula α k
v : α → M
xs : Fin k → M
⊢ (List.foldr imp f l).Realize v xs = ((∀ i ∈ l, i.Realize v xs) → f.Realize v xs)

Tactic:
induction l

Goal state after:
case nil
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
k : ℕ
f : L.BoundedFormula α k
v : α → M
xs : Fin k → M
⊢ (List.foldr imp f []).Realize v xs = ((∀ i ∈ [], i.Realize v xs) → f.Realize v xs)

case cons
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
k : ℕ
f : L.BoundedFormula α k
v : α → M
xs : Fin k → M
head✝ : L.BoundedFormula α k
tail✝ : List (L.BoundedFormula α k)
tail_ih✝ : (List.foldr imp f tail✝).Realize v xs = ((∀ i ∈ tail✝, i.Realize v xs) → f.Realize v xs)
⊢ (List.foldr imp f (head✝ :: tail✝)).Realize v xs = ((∀ i ∈ head✝ :: tail✝, i.Realize v xs) → f.Realize v xs)
Module: Mathlib.ModelTheory.Ultraproducts

Goal state before:
pp: case all
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst✝¹ : (a : α) → L.Structure (M a)
inst✝ : ∀ (a : α), Nonempty (M a)
β : Type u_3
n : ℕ
x : β → (a : α) → M a
k : ℕ
φ : L.BoundedFormula β (k + 1)
ih :
  ∀ (v : Fin (k + 1) → (a : α) → M a),
    (φ.Realize (fun i ↦ Quotient.mk' (x i)) fun i ↦ Quotient.mk' (v i)) ↔
      ∀ᶠ (a : α) in ↑u, φ.Realize (fun i ↦ x i a) fun i ↦ v i a
v : Fin k → (a : α) → M a
⊢ ((∀' φ).Realize (fun i ↦ Quotient.mk' (x i)) fun i ↦ Quotient.mk' (v i)) ↔
    ∀ᶠ (a : α) in ↑u, (∀' φ).Realize (fun i ↦ x i a) fun i ↦ v i a

Tactic:
simp only [BoundedFormula.Realize]

Goal state after:
case all
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst✝¹ : (a : α) → L.Structure (M a)
inst✝ : ∀ (a : α), Nonempty (M a)
β : Type u_3
n : ℕ
x : β → (a : α) → M a
k : ℕ
φ : L.BoundedFormula β (k + 1)
ih :
  ∀ (v : Fin (k + 1) → (a : α) → M a),
    (φ.Realize (fun i ↦ Quotient.mk' (x i)) fun i ↦ Quotient.mk' (v i)) ↔
      ∀ᶠ (a : α) in ↑u, φ.Realize (fun i ↦ x i a) fun i ↦ v i a
v : Fin k → (a : α) → M a
⊢ (∀ (x_1 : Quotient ((↑u).productSetoid M)),
      φ.Realize (fun i ↦ Quotient.mk' (x i)) (Fin.snoc (fun i ↦ Quotient.mk' (v i)) x_1)) ↔
    ∀ᶠ (a : α) in ↑u, ∀ (x_1 : M a), φ.Realize (fun i ↦ x i a) (Fin.snoc (fun i ↦ v i a) x_1)
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
α : Type u_5
n : ℕ
φ : L.BoundedFormula α n
v : α → M
xs : Fin n → M
⊢ φ.Realize (⇑f ∘ v) (⇑f ∘ xs) ↔ φ.Realize v xs

Tactic:
← BoundedFormula.realize_restrictFreeVar' Set.Subset.rfl,

Goal state after:
L : Language
M : Type u_1
N : Type u_2
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M ↪ₑ[L] N
α : Type u_5
n : ℕ
φ : L.BoundedFormula α n
v : α → M
xs : Fin n → M
⊢ (φ.restrictFreeVar (Set.inclusion ⋯)).Realize ((⇑f ∘ v) ∘ Subtype.val) (⇑f ∘ xs) ↔ φ.Realize v xs
Module: Mathlib.ModelTheory.Substructures

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
s : Set M
x : M
⊢ x ∈ range (Term.realize Subtype.val) ↔ ∃ t, Term.realize Subtype.val t = x

Tactic:
mem_range

Goal state after:
L : Language
M : Type w
inst✝ : L.Structure M
s : Set M
x : M
⊢ (∃ y, Term.realize Subtype.val y = x) ↔ ∃ t, Term.realize Subtype.val t = x
Module: Mathlib.ModelTheory.Satisfiability

Goal state before:
pp: L : Language
ι : Type u_1
inst✝ : Nonempty ι
T : ι → L.Theory
h : Directed (fun x1 x2 ↦ x1 ⊆ x2) T
h' : ∀ (i : ι), (T i).IsSatisfiable
T0 : Finset L.Sentence
⊢ ↑T0 ⊆ ⋃ i, T i → IsSatisfiable ↑T0

Tactic:
hT0

Goal state after:
L : Language
ι : Type u_1
inst✝ : Nonempty ι
T : ι → L.Theory
h : Directed (fun x1 x2 ↦ x1 ⊆ x2) T
h' : ∀ (i : ι), (T i).IsSatisfiable
T0 : Finset L.Sentence
hT0 : ↑T0 ⊆ ⋃ i, T i
⊢ IsSatisfiable ↑T0
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 u v w, w} κ ≤ #↑(ModelType.reduct (L.lhomWithConstants (Quotient.out κ)) ⋯.bundled)

Tactic:
ModelType.reduct_Carrier,

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 u v w, w} κ ≤ #↑⋯.bundled
Module: Mathlib.ModelTheory.Algebra.Field.IsAlgClosed

Goal state before:
pp: K : Type u_1
inst✝¹ : CommRing K
inst✝ : Nontrivial K
n : ℕ
v : Fin (n + 1) → K
⊢ (lift v) (genericMonicPoly n) =
    eval (v (Fin.last n)) ↑(((monicEquivDegreeLT n).trans (degreeLTEquiv K n).toEquiv).symm (v ∘ Fin.castSucc))

Tactic:
simp [genericMonicPoly, monicEquivDegreeLT, degreeLTEquiv, eval_finsetSum]

Goal state after:
Module: Mathlib.ModelTheory.Definability

Goal state before:
pp: M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
f : M → M
φ : L[[↑A]].Term Unit
⊢ ∀ (b : M),
    f ((Equiv.funUnique Unit M).symm b ()) = Term.realize ((Equiv.funUnique Unit M).symm b) φ ↔
      f b = ((fun v ↦ Term.realize v φ) ∘ Function.const Unit) b

Tactic:
simp only [Equiv.funUnique_symm_apply, uniqueElim_const, Function.comp_apply]

Goal state after:
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
f : M → M
φ : L[[↑A]].Term Unit
⊢ ∀ (b : M), f b = Term.realize (uniqueElim b) φ ↔ f b = Term.realize (Function.const Unit b) φ
Module: Mathlib.ModelTheory.Definability

Goal state before:
pp: case h
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
β : Type u_1
g : α → (β → M) → M
φ : L[[↑A]].Term α
ψ : α → L[[↑A]].Term β
hψ : ∀ (i : α), g i = fun v ↦ Term.realize v (ψ i)
⊢ (fun b ↦ (fun v ↦ Term.realize v φ) fun x ↦ g x b) = fun v ↦ Term.realize v (φ.subst ψ)

Tactic:
simp [hψ]

Goal state after:
Module: Mathlib.ModelTheory.Satisfiability

Goal state before:
pp: case mp
L : Language
T : L.Theory
φ : L.Sentence
this : DecidableEq L.Sentence := Classical.decEq L.Sentence
h : ∀ (T0 : Finset L.Sentence), ↑T0 ⊆ T ∪ {Formula.not φ} → IsSatisfiable ↑T0
T0 : Finset L.Sentence
⊢ ↑T0 ⊆ T → (↑T0 ∪ {Formula.not φ}).IsSatisfiable

Tactic:
hT0

Goal state after:
case mp
L : Language
T : L.Theory
φ : L.Sentence
this : DecidableEq L.Sentence := Classical.decEq L.Sentence
h : ∀ (T0 : Finset L.Sentence), ↑T0 ⊆ T ∪ {Formula.not φ} → IsSatisfiable ↑T0
T0 : Finset L.Sentence
hT0 : ↑T0 ⊆ T
⊢ (↑T0 ∪ {Formula.not φ}).IsSatisfiable
Module: Mathlib.ModelTheory.Satisfiability

Goal state before:
pp: case mpr
L : Language
T : L.Theory
φ : L.Sentence
this : DecidableEq L.Sentence := Classical.decEq L.Sentence
h : ∀ (T0 : Finset L.Sentence), ↑T0 ⊆ T → (↑T0 ∪ {Formula.not φ}).IsSatisfiable
T0 : Finset L.Sentence
⊢ ↑T0 ⊆ T ∪ {Formula.not φ} → IsSatisfiable ↑T0

Tactic:
hT0

Goal state after:
case mpr
L : Language
T : L.Theory
φ : L.Sentence
this : DecidableEq L.Sentence := Classical.decEq L.Sentence
h : ∀ (T0 : Finset L.Sentence), ↑T0 ⊆ T → (↑T0 ∪ {Formula.not φ}).IsSatisfiable
T0 : Finset L.Sentence
hT0 : ↑T0 ⊆ T ∪ {Formula.not φ}
⊢ IsSatisfiable ↑T0
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:
by
  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.FieldTheory.IsPerfectClosure

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

Tactic:
by
  by_cases hp : 1 < p
  · 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]
  rw [pNilradical_eq_bot hp, Ideal.mem_bot]
  refine ⟨fun h ↦ ⟨0, by rw [pow_zero, pow_one, h]⟩, fun ⟨n, h⟩ ↦ ?_⟩
  rcases Nat.le_one_iff_eq_zero_or_eq_one.1 (not_lt.1 hp) with hp | hp
  · by_cases hn : n = 0
    · rwa [hn, pow_zero, pow_one] at h
    rw [hp, zero_pow hn, pow_zero] at h
    subsingleton [subsingleton_of_zero_eq_one h.symm]
  rwa [hp, one_pow, pow_one] at h

Goal state after:
Module: Mathlib.FieldTheory.IsPerfectClosure

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
p : ℕ
inst✝ : ExpChar R p
h : Function.Injective ⇑(frobenius R p)
x : R
x✝ : ∃ n, x ^ p ^ n = 0
n : ℕ
h✝ : x ^ p ^ n = 0
⊢ (⇑(frobenius R p))^[n] x = (⇑(frobenius R p))^[n] 0

Tactic:
by rwa [← coe_iterateFrobenius, map_zero]

Goal state after: