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

Goal state before:
pp: case htc
τ : 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
i✝ : ↑f.sets
⊢ IsCompact (closure[inst✝¹] (image2 ϕ (↑i✝ ∩ v) s))

Tactic:
apply hc₁.of_isClosed_subset isClosed_closure

Goal state after:
case htc
τ : 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
i✝ : ↑f.sets
⊢ closure[inst✝¹] (image2 ϕ (↑i✝ ∩ v) s) ⊆ c
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 : ℕ
⊢ ∃ s, IsDynCoverOf T F U n ↑s

Tactic:
by
  obtain ⟨(V : SetRel X X), V_uni, V_symm, V_U⟩ := comp_symm_mem_uniformity_sets U_uni
  obtain ⟨s, _, s_cover⟩ := F_comp.elim_nhds_subcover (ball · V)
    fun (x : X) _ ↦ ball_mem_nhds x V_uni
  have : IsDynCoverOf T F V 1 s := .of_subset_iUnion_ball <| by simpa using s_cover
  obtain ⟨t, t_dyncover, t_card⟩ := this.iterate_le_pow F_inv n
  rw [one_mul n] at t_dyncover
  exact ⟨t, t_dyncover.of_entourage_subset V_U⟩

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
p : α → Prop
h✝ : ∀ᵐ (a : α) ∂μ, p a
h_ac : μ.withDensity (ν.rnDeriv μ) ≪ μ
a✝ : α
h : p a✝
⊢ μ.rnDeriv ν a✝ ≠ 0 → p a✝

Tactic:
_

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
p : α → Prop
h✝ : ∀ᵐ (a : α) ∂μ, p a
h_ac : μ.withDensity (ν.rnDeriv μ) ≪ μ
a✝¹ : α
h : p a✝¹
a✝ : μ.rnDeriv ν a✝¹ ≠ 0
⊢ p a✝¹
Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy

Goal state before:
pp: 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 < ⊤
s : Finset X
s_cover : IsDynCoverOf T F U m ↑s
s_coverMincard : ↑(#s) = coverMincard T F U m
⊢ coverMincard T F (U ○ U) (m * n) ≤ coverMincard T F U m ^ n

Tactic:
obtain ⟨t, t_cover, t_sn⟩ := s_cover.iterate_le_pow F_inv n

Goal state after:
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 < ⊤
s : Finset X
s_cover : IsDynCoverOf T F U m ↑s
s_coverMincard : ↑(#s) = coverMincard T F U m
t : Finset X
t_cover : IsDynCoverOf T F (U ○ U) (m * n) ↑t
t_sn : #t ≤ #s ^ n
⊢ coverMincard T F (U ○ U) (m * n) ≤ coverMincard T F U m ^ n
Module: Mathlib.Dynamics.TopologicalEntropy.Semiconj

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : UniformSpace X
inst✝ : UniformSpace Y
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
h' : UniformContinuous φ
F : Set X
⊢ coverEntropyInf S F ≤ coverEntropyInf S F

Tactic:
exact coverEntropyInf_antitone S F (uniformContinuous_iff_le_comap.1 h')

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
hμν : μ ≤ ν
inst✝ : SigmaFinite ν
⊢ μ.rnDeriv ν ≤ᵐ[ν] 1

Tactic:
refine ae_le_of_forall_setLIntegral_le_of_sigmaFinite (μ.measurable_rnDeriv ν) fun s _ _ ↦ ?_
  simp only [Pi.one_apply, MeasureTheory.setLIntegral_one]
  exact (Measure.setLIntegral_rnDeriv_le s).trans (hμν s)

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
V : Set (X × X)
V_uni : V ∈ 𝓤 X
V_symm : SetRel.IsSymm V
V_U : V ○ V ⊆ U
s : Finset X
s_cover : IsDynCoverOf T F V 1 ↑s
⊢ coverEntropyEntourage T F U < ⊤

Tactic:
apply (coverEntropyEntourage_antitone T F V_U).trans_lt

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
V : Set (X × X)
V_uni : V ∈ 𝓤 X
V_symm : SetRel.IsSymm V
V_U : V ○ V ⊆ U
s : Finset X
s_cover : IsDynCoverOf T F V 1 ↑s
⊢ (fun U ↦ coverEntropyEntourage T F U) (V ○ V) < ⊤
Module: Mathlib.Dynamics.TopologicalEntropy.Subset

Goal state before:
pp: X : Type u_1
T : X → X
F : Set X
inst✝ : UniformSpace X
h : Continuous T
⊢ coverEntropyInf T (closure F) = coverEntropyInf T F

Tactic:
refine (iSup₂_le fun U U_uni ↦ ?_).antisymm (coverEntropyInf_monotone T subset_closure)
  obtain ⟨V, V_uni, V_U⟩ := comp_mem_uniformity_sets U_uni
  exact le_iSup₂_of_le V V_uni ((coverEntropyInfEntourage_antitone T (closure F) V_U).trans
    (coverEntropyInfEntourage_closure h F V V_uni))

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

Tactic:
inv_inv,

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.FieldTheory.AbelRuffini

Goal state before:
pp: case h₂
F : Type u_1
inst✝ : Field F
s : Multiset F[X]
hs : ∀ p ∈ s, Group.IsSolvable p.Gal
p : F[X]
t : Multiset F[X]
hps : p ∈ s
⊢ t ⊆ s → Group.IsSolvable t.prod.Gal → Group.IsSolvable (insert p t).prod.Gal

Tactic:
_

Goal state after:
case h₂
F : Type u_1
inst✝ : Field F
s : Multiset F[X]
hs : ∀ p ∈ s, Group.IsSolvable p.Gal
p : F[X]
t : Multiset F[X]
hps : p ∈ s
a✝ : t ⊆ s
⊢ Group.IsSolvable t.prod.Gal → Group.IsSolvable (insert p t).prod.Gal
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 ν
s : Set β
hs : MeasurableSet s
a : α
ha : (map f μ).rnDeriv (map f ν) (f a) = μ.rnDeriv ν a
⊢ a ∈ f ⁻¹' s → μ.rnDeriv ν a = (map f μ).rnDeriv (map f ν) (f a)

Tactic:
_

Goal state after:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
s : Set β
hs : MeasurableSet s
a : α
ha : (map f μ).rnDeriv (map f ν) (f a) = μ.rnDeriv ν a
a✝ : a ∈ f ⁻¹' s
⊢ μ.rnDeriv ν a = (map f μ).rnDeriv (map f ν) (f a)
Module: Mathlib.FieldTheory.AbelRuffini

Goal state before:
pp: F : Type u_1
inst✝ : Field F
n : ℕ
a : F
h : (map (RingHom.id F) (X ^ n - 1)).Splits
ha : ¬a = 0
ha' : (algebraMap F (X ^ n - C a).SplittingField) a ≠ 0
hn : ¬n = 0
hn' : 0 < n
hn'' : X ^ n - C a ≠ 0
hn''' : X ^ n - 1 ≠ 0
mem_range : ∀ {c : (X ^ n - C a).SplittingField}, c ^ n = 1 → ∃ d, (algebraMap F (X ^ n - C a).SplittingField) d = c
σ✝ τ : (X ^ n - C a).Gal
b : (X ^ n - C a).SplittingField
hb : b ^ n = (algebraMap F (X ^ n - C a).SplittingField) a
hb' : b ≠ 0
σ : (X ^ n - C a).Gal
⊢ (algebraMap F (X ^ n - C a).SplittingField) a / (algebraMap F (X ^ n - C a).SplittingField) a = 1

Tactic:
div_self ha'

Goal state after:
F : Type u_1
inst✝ : Field F
n : ℕ
a : F
h : (map (RingHom.id F) (X ^ n - 1)).Splits
ha : ¬a = 0
ha' : (algebraMap F (X ^ n - C a).SplittingField) a ≠ 0
hn : ¬n = 0
hn' : 0 < n
hn'' : X ^ n - C a ≠ 0
hn''' : X ^ n - 1 ≠ 0
mem_range : ∀ {c : (X ^ n - C a).SplittingField}, c ^ n = 1 → ∃ d, (algebraMap F (X ^ n - C a).SplittingField) d = c
σ✝ τ : (X ^ n - C a).Gal
b : (X ^ n - C a).SplittingField
hb : b ^ n = (algebraMap F (X ^ n - C a).SplittingField) a
hb' : b ≠ 0
σ : (X ^ n - C a).Gal
⊢ 1 = 1
Module: Mathlib.ModelTheory.LanguageMap

Goal state before:
pp: L : Language
α : Type w'
β : Type u_1
f : α → β
⊢ (L.lhomWithConstantsMap f).comp LHom.sumInl = L.lhomWithConstants β

Tactic:
by ext <;> rfl

Goal state after:
Module: Mathlib.ModelTheory.Basic

Goal state before:
pp: L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
a₁✝ : M ≃[L] N
⊢ ∀ ⦃a₂ : M ≃[L] N⦄, a₁✝.toEmbedding = a₂.toEmbedding → a₁✝ = a₂

Tactic:
_

Goal state after:
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
a₁✝ a₂✝ : M ≃[L] N
⊢ a₁✝.toEmbedding = a₂✝.toEmbedding → a₁✝ = a₂✝
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case func.zero
L : Language
M : Type w
inst✝² : L.Structure M
α : Type u'
β : Type v'
inst✝¹ : L[[α]].Structure M
inst✝ : (L.lhomWithConstants α).IsExpansionOn M
v : β → M
f : L[[α]].Functions 0
ts : Fin 0 → L[[α]].Term β
ih : ∀ (a : Fin 0), realize (Sum.elim (fun a ↦ ↑(L.con a)) v) (ts a).constantsToVars = realize v (ts a)
⊢ realize (Sum.elim (fun a ↦ ↑(L.con a)) v) (func f ts).constantsToVars = realize v (func f ts)

Tactic:
cases f
      · simp only [realize, ih, constantsOn, constantsOnFunc, constantsToVars]
        -- Porting note: below lemma does not work with simp for some reason
        rw [withConstants_funMap_sumInl]
      · simp only [realize, constantsToVars, Sum.elim_inl, funMap_eq_coe_constants]
        rfl

Goal state after:
Module: Mathlib.ModelTheory.Substructures

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
s : Set M
⊢ ↑((closure L).toFun s) = range (Term.realize Subtype.val)

Tactic:
let S : L.Substructure M := ⟨range (Term.realize (L := L) ((↑) : s → M)), fun {n} f x hx => by
    simp only [mem_range] at *
    refine ⟨func f fun i => Classical.choose (hx i), ?_⟩
    simp only [Term.realize, fun i => Classical.choose_spec (hx i)]⟩

Goal state after:
L : Language
M : Type w
inst✝ : L.Structure M
s : Set M
S : L.Substructure M := { carrier := range (Term.realize Subtype.val), fun_mem := ⋯ }
⊢ ↑((closure L).toFun s) = range (Term.realize Subtype.val)
Module: Mathlib.ModelTheory.Substructures

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
s : Set M
S : L.Substructure M := { carrier := range (Term.realize Subtype.val), fun_mem := ⋯ }
⊢ ↑((closure L).toFun s) = ↑S

Tactic:
← SetLike.ext'_iff

Goal state after:
L : Language
M : Type w
inst✝ : L.Structure M
s : Set M
S : L.Substructure M := { carrier := range (Term.realize Subtype.val), fun_mem := ⋯ }
⊢ (closure L).toFun s = S
Module: Mathlib.ModelTheory.ElementaryMaps

Goal state before:
pp: case refine_3
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 : ℕ} (R : L.Relations l) (ts : Fin l → L.Term (Empty ⊕ Fin n✝)) (xs : Fin n✝ → M),
    (BoundedFormula.rel R ts).Realize (⇑f ∘ default) (⇑f ∘ xs) ↔ (BoundedFormula.rel R ts).Realize default xs

Tactic:
_

Goal state after:
case refine_3
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✝ : ℕ
⊢ ∀ (R : L.Relations l✝) (ts : Fin l✝ → L.Term (Empty ⊕ Fin n✝)) (xs : Fin n✝ → M),
    (BoundedFormula.rel R ts).Realize (⇑f ∘ default) (⇑f ∘ xs) ↔ (BoundedFormula.rel R ts).Realize default xs
Module: Mathlib.ModelTheory.ElementaryMaps

Goal state before:
pp: case refine_4
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✝ : ℕ
⊢ ∀ (f₁ f₂ : L.BoundedFormula Empty n✝),
    (∀ (xs : Fin n✝ → M), f₁.Realize (⇑f ∘ default) (⇑f ∘ xs) ↔ f₁.Realize default xs) →
      (∀ (xs : Fin n✝ → M), f₂.Realize (⇑f ∘ default) (⇑f ∘ xs) ↔ f₂.Realize default xs) →
        ∀ (xs : Fin n✝ → M), (f₁ ⟹ f₂).Realize (⇑f ∘ default) (⇑f ∘ xs) ↔ (f₁ ⟹ f₂).Realize default xs

Tactic:
_

Goal state after:
case refine_4
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✝ : ℕ
f₁✝ : L.BoundedFormula Empty n✝
⊢ ∀ (f₂ : L.BoundedFormula Empty n✝),
    (∀ (xs : Fin n✝ → M), f₁✝.Realize (⇑f ∘ default) (⇑f ∘ xs) ↔ f₁✝.Realize default xs) →
      (∀ (xs : Fin n✝ → M), f₂.Realize (⇑f ∘ default) (⇑f ∘ xs) ↔ f₂.Realize default xs) →
        ∀ (xs : Fin n✝ → M), (f₁✝ ⟹ f₂).Realize (⇑f ∘ default) (⇑f ∘ xs) ↔ (f₁✝ ⟹ f₂).Realize default xs
Module: Mathlib.ModelTheory.ElementaryMaps

Goal state before:
pp: case refine_4
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✝ : ℕ
f₁✝ : L.BoundedFormula Empty n✝
⊢ ∀ (f₂ : L.BoundedFormula Empty n✝),
    (∀ (xs : Fin n✝ → M), f₁✝.Realize (⇑f ∘ default) (⇑f ∘ xs) ↔ f₁✝.Realize default xs) →
      (∀ (xs : Fin n✝ → M), f₂.Realize (⇑f ∘ default) (⇑f ∘ xs) ↔ f₂.Realize default xs) →
        ∀ (xs : Fin n✝ → M), (f₁✝ ⟹ f₂).Realize (⇑f ∘ default) (⇑f ∘ xs) ↔ (f₁✝ ⟹ f₂).Realize default xs

Tactic:
_

Goal state after:
case refine_4
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✝ : ℕ
f₁✝ f₂✝ : L.BoundedFormula Empty n✝
⊢ (∀ (xs : Fin n✝ → M), f₁✝.Realize (⇑f ∘ default) (⇑f ∘ xs) ↔ f₁✝.Realize default xs) →
    (∀ (xs : Fin n✝ → M), f₂✝.Realize (⇑f ∘ default) (⇑f ∘ xs) ↔ f₂✝.Realize default xs) →
      ∀ (xs : Fin n✝ → M), (f₁✝ ⟹ f₂✝).Realize (⇑f ∘ default) (⇑f ∘ xs) ↔ (f₁✝ ⟹ f₂✝).Realize default xs
Module: Mathlib.ModelTheory.ElementaryMaps

Goal state before:
pp: case refine_4
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✝ : ℕ
f₁✝ f₂✝ : L.BoundedFormula Empty n✝
ih1 : ∀ (xs : Fin n✝ → M), f₁✝.Realize (⇑f ∘ default) (⇑f ∘ xs) ↔ f₁✝.Realize default xs
ih2 : ∀ (xs : Fin n✝ → M), f₂✝.Realize (⇑f ∘ default) (⇑f ∘ xs) ↔ f₂✝.Realize default xs
⊢ ∀ (xs : Fin n✝ → M), (f₁✝ ⟹ f₂✝).Realize (⇑f ∘ default) (⇑f ∘ xs) ↔ (f₁✝ ⟹ f₂✝).Realize default xs

Tactic:
_

Goal state after:
case refine_4
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✝ : ℕ
f₁✝ f₂✝ : L.BoundedFormula Empty n✝
ih1 : ∀ (xs : Fin n✝ → M), f₁✝.Realize (⇑f ∘ default) (⇑f ∘ xs) ↔ f₁✝.Realize default xs
ih2 : ∀ (xs : Fin n✝ → M), f₂✝.Realize (⇑f ∘ default) (⇑f ∘ xs) ↔ f₂✝.Realize default xs
xs✝ : Fin n✝ → M
⊢ (f₁✝ ⟹ f₂✝).Realize (⇑f ∘ default) (⇑f ∘ xs✝) ↔ (f₁✝ ⟹ f₂✝).Realize default xs✝
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case succ.mpr
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
n✝ : ℕ
v : α → M
n : ℕ
ih : ∀ {φ : L.BoundedFormula α n}, φ.exs.Realize v ↔ ∃ xs, φ.Realize v xs
φ : L.BoundedFormula α (n + 1)
⊢ (∃ xs, φ.Realize v xs) → ∃ xs a, φ.Realize v (snoc xs a)

Tactic:
· rintro ⟨xs, h⟩
      rw [← Fin.snoc_init_self xs] at h
      exact ⟨_, _, h⟩

Goal state after:
Module: Mathlib.ModelTheory.Definability

Goal state before:
pp: case mp
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
φ : L.Formula (↑A ⊕ α)
A0 : Finset M := Finset.image Subtype.val (BoundedFormula.freeVarFinset φ).toLeft
x✝ : α → M
⊢ BoundedFormula.Realize φ (Sum.elim Subtype.val x✝) default ↔
    (BoundedFormula.restrictFreeVar φ fun x ↦
          Sum.rec (motive := fun x ↦ x ∈ BoundedFormula.freeVarFinset φ → ↥A0 ⊕ α) (fun val hx ↦ Sum.inl ⟨↑val, ⋯⟩)
            (fun val x ↦ Sum.inr val) ↑x ⋯).Realize
      (Sum.elim Subtype.val x✝) default

Tactic:
exact iff_comm.1 <| BoundedFormula.realize_restrictFreeVar _ (by simp)

Goal state after:
Module: Mathlib.ModelTheory.Skolem

Goal state before:
pp: L : Language
| sum fun i ↦ lift.{u, max u v} #(L.BoundedFormula Empty (i + 1))

Tactic:
1,

Goal state after:
L : Language
| fun i ↦ lift.{u, max u v} #(L.BoundedFormula Empty (i + 1))
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 (κ →₀ ℕ)
f : (i : ι) × ↥(monoms i) ⊕ κ → R
i : ι
m : ↥(monoms i)
⊢ m ∈ (monoms i).attach →
    f (Sum.inl ⟨i, m⟩) * (lift f) ((↑m).prod fun j n ↦ of (Sum.inr j) ^ n) =
      if ∃ (h : ↑m ∈ monoms i), ¬f (Sum.inl ⟨i, ⟨↑m, ⋯⟩⟩) = 0 then
        (if h : ↑m ∈ monoms i then f (Sum.inl ⟨i, ⟨↑m, ⋯⟩⟩) else 0) * ∏ x ∈ (↑m).support, f (Sum.inr x) ^ ↑m x
      else 0

Tactic:
_

Goal state after:
ι : Type u_1
κ : Type u_2
R : Type u_3
inst✝² : DecidableEq κ
inst✝¹ : CommRing R
inst✝ : DecidableEq R
monoms : ι → Finset (κ →₀ ℕ)
f : (i : ι) × ↥(monoms i) ⊕ κ → R
i : ι
m : ↥(monoms i)
a✝ : m ∈ (monoms i).attach
⊢ f (Sum.inl ⟨i, m⟩) * (lift f) ((↑m).prod fun j n ↦ of (Sum.inr j) ^ n) =
    if ∃ (h : ↑m ∈ monoms i), ¬f (Sum.inl ⟨i, ⟨↑m, ⋯⟩⟩) = 0 then
      (if h : ↑m ∈ monoms i then f (Sum.inl ⟨i, ⟨↑m, ⋯⟩⟩) else 0) * ∏ x ∈ (↑m).support, f (Sum.inr x) ^ ↑m x
    else 0
Module: Mathlib.ModelTheory.Algebra.Field.IsAlgClosed

Goal state before:
pp: case inl
φ : 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
⊢ q ∉ ∅ → Theory.ACF ↑q ⊨ᵇ ψ

Tactic:
_

Goal state after:
case inl
φ : 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 ⊨ᵇ ψ
Module: Mathlib.ModelTheory.Satisfiability

Goal state before:
pp: L : Language
κ : Cardinal.{w}
T : L.Theory
h : κ.Categorical T
h1 : ℵ₀ ≤ κ
h2 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ
hS : T.IsSatisfiable
hT : ∀ (M : T.ModelType), Infinite ↑M
φ : L.Sentence
w✝ : T.ModelType
h✝ : #↑w✝ = κ
MF : T.ModelType
hMF : ¬↑MF ⊨ φ
MT : T.ModelType
hMT : ↑MT ⊨ φ
⊢ ↑MF ⊨ φ

Tactic:
have := hT MT

Goal state after:
L : Language
κ : Cardinal.{w}
T : L.Theory
h : κ.Categorical T
h1 : ℵ₀ ≤ κ
h2 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ
hS : T.IsSatisfiable
hT : ∀ (M : T.ModelType), Infinite ↑M
φ : L.Sentence
w✝ : T.ModelType
h✝ : #↑w✝ = κ
MF : T.ModelType
hMF : ¬↑MF ⊨ φ
MT : T.ModelType
hMT : ↑MT ⊨ φ
this : Infinite ↑MT
⊢ ↑MF ⊨ φ
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)
hS : c.Definable ring S
ps : ι → MvPolynomial ι K
⊢ 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:
let := Fintype.ofFinite ι

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)
hS : c.Definable ring S
ps : ι → MvPolynomial ι K
this : Fintype ι := Fintype.ofFinite ι
⊢ 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.FinTrdeg

Goal state before:
pp: case mp
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
E : IntermediateField K L
fg : ∃ S₀ M, Algebra.FiniteType K ↥S₀ ∧ IsLocalization M ↥E
alg : Algebra.IsAlgebraic (↥E) L
⊢ Algebra.trdeg K ↥E < Cardinal.aleph0

Tactic:
obtain ⟨S₀, M, fin, islocal⟩ := fg

Goal state after:
case mp
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
E : IntermediateField K L
alg : Algebra.IsAlgebraic (↥E) L
S₀ : Subalgebra K ↥E
M : Submonoid ↥S₀
fin : Algebra.FiniteType K ↥S₀
islocal : IsLocalization M ↥E
⊢ Algebra.trdeg K ↥E < Cardinal.aleph0
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:
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.Finite.Polynomial

Goal state before:
pp: case add
σ : Type u_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
f p✝ : MvPolynomial σ (ZMod p)
⊢ ∀ (q : MvPolynomial σ (ZMod p)),
    (frobenius (MvPolynomial σ (ZMod p)) p) p✝ = (expand p) p✝ →
      (frobenius (MvPolynomial σ (ZMod p)) p) q = (expand p) q →
        (frobenius (MvPolynomial σ (ZMod p)) p) p✝ + (frobenius (MvPolynomial σ (ZMod p)) p) q =
          (expand p) p✝ + (expand p) q

Tactic:
_

Goal state after:
case add
σ : Type u_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
f p✝ q✝ : MvPolynomial σ (ZMod p)
⊢ (frobenius (MvPolynomial σ (ZMod p)) p) p✝ = (expand p) p✝ →
    (frobenius (MvPolynomial σ (ZMod p)) p) q✝ = (expand p) q✝ →
      (frobenius (MvPolynomial σ (ZMod p)) p) p✝ + (frobenius (MvPolynomial σ (ZMod p)) p) q✝ =
        (expand p) p✝ + (expand p) q✝
Module: Mathlib.FieldTheory.Finite.Polynomial

Goal state before:
pp: case mul_X
σ : Type u_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
f p✝ : MvPolynomial σ (ZMod p)
⊢ ∀ (n : σ),
    (frobenius (MvPolynomial σ (ZMod p)) p) p✝ = (expand p) p✝ →
      (frobenius (MvPolynomial σ (ZMod p)) p) p✝ * (frobenius (MvPolynomial σ (ZMod p)) p) (X n) =
        (expand p) p✝ * X n ^ p

Tactic:
_

Goal state after:
case mul_X
σ : Type u_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
f p✝ : MvPolynomial σ (ZMod p)
n✝ : σ
⊢ (frobenius (MvPolynomial σ (ZMod p)) p) p✝ = (expand p) p✝ →
    (frobenius (MvPolynomial σ (ZMod p)) p) p✝ * (frobenius (MvPolynomial σ (ZMod p)) p) (X n✝) =
      (expand p) p✝ * X n✝ ^ p