mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Definability

Goal state before:
pp: α : Type u_1
A : Set ℕ
inst✝ : Finite α
n✝ : ℕ
this : Fintype α
n : ℕ
φ : presburger[[↑A]].BoundedFormula α (n + 1)
e : (α ⊕ Fin n) ⊕ Fin 1 ≃ α ⊕ Fin (n + 1) :=
  (Equiv.sumAssoc α (Fin n) (Fin 1)).trans ((_root_.Equiv.refl α).sumCongr finSumFinEquiv)
ih : IsSemilinearSet (⇑(LinearEquiv.funCongrLeft ℕ ℕ e) '' {v | φ.Realize (v ∘ Sum.inl) (v ∘ Sum.inr)})
⊢ {v | ∀ (x : ℕ), φ.Realize (v ∘ Sum.inl) (Fin.snoc (v ∘ Sum.inr) x)} =
    {a |
      ∀ (a_1 : ℕ),
        φ.Realize ((LinearEquiv.funCongrLeft ℕ ℕ e.symm) (Sum.elim a (Fin.cons a_1 finZeroElim)) ∘ Sum.inl)
          ((LinearEquiv.funCongrLeft ℕ ℕ e.symm) (Sum.elim a (Fin.cons a_1 finZeroElim)) ∘ Sum.inr)}

Tactic:
LinearEquiv.funCongrLeft_apply,

Goal state after:
α : Type u_1
A : Set ℕ
inst✝ : Finite α
n✝ : ℕ
this : Fintype α
n : ℕ
φ : presburger[[↑A]].BoundedFormula α (n + 1)
e : (α ⊕ Fin n) ⊕ Fin 1 ≃ α ⊕ Fin (n + 1) :=
  (Equiv.sumAssoc α (Fin n) (Fin 1)).trans ((_root_.Equiv.refl α).sumCongr finSumFinEquiv)
ih : IsSemilinearSet (⇑(LinearEquiv.funCongrLeft ℕ ℕ e) '' {v | φ.Realize (v ∘ Sum.inl) (v ∘ Sum.inr)})
⊢ {v | ∀ (x : ℕ), φ.Realize (v ∘ Sum.inl) (Fin.snoc (v ∘ Sum.inr) x)} =
    {a |
      ∀ (a_1 : ℕ),
        φ.Realize ((LinearMap.funLeft ℕ ℕ ⇑e.symm) (Sum.elim a (Fin.cons a_1 finZeroElim)) ∘ Sum.inl)
          ((LinearMap.funLeft ℕ ℕ ⇑e.symm) (Sum.elim a (Fin.cons a_1 finZeroElim)) ∘ Sum.inr)}
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: ι : Type u_1
inst✝ : Finite ι
s : Set (ι → ℕ)
hs : IsSlice s
h : ∀ (a : ι → ℕ) (t : Finset ι), (∀ x ∈ s, ∀ i ∉ t, x i = a i) → IsSemilinearSet s
⊢ IsSemilinearSet s

Tactic:
have := Fintype.ofFinite ι

Goal state after:
ι : Type u_1
inst✝ : Finite ι
s : Set (ι → ℕ)
hs : IsSlice s
h : ∀ (a : ι → ℕ) (t : Finset ι), (∀ x ∈ s, ∀ i ∉ t, x i = a i) → IsSemilinearSet s
this : Fintype ι
⊢ IsSemilinearSet s
Module: Mathlib.ModelTheory.Complexity

Goal state before:
pp: L : Language
α : Type u'
n : ℕ
M : Type u_1
inst✝⁴ : L.Structure M
N : Type u_2
inst✝³ : L.Structure N
F : Type u_3
inst✝² : FunLike F M N
inst✝¹ : EmbeddingLike F M N
inst✝ : L.StrongHomClass F M N
φ : L.BoundedFormula α n
hU : φ.IsUniversal
f : F
v : α → M
xs : Fin n → M
⊢ φ.Realize (⇑f ∘ v) (⇑f ∘ xs) → φ.Realize v xs

Tactic:
by
  induction hU with
  | of_isQF hQF => simp [hQF.realize_embedding]
  | all _ ih =>
    simp only [realize_all, Nat.succ_eq_add_one]
    refine fun h a => ih ?_
    rw [Fin.comp_snoc]
    exact h (f a)

Goal state after:
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: ι : Type u_3
inst✝ : Finite ι
s₁ s₂ : Set (ι → ℕ)
hs₁ : IsLinearSet s₁
hs₂ : IsLinearSet s₂
⊢ IsSemilinearSet (s₁ ∩ s₂)

Tactic:
have := Fintype.ofFinite ι

Goal state after:
ι : Type u_3
inst✝ : Finite ι
s₁ s₂ : Set (ι → ℕ)
hs₁ : IsLinearSet s₁
hs₂ : IsLinearSet s₂
this : Fintype ι
⊢ IsSemilinearSet (s₁ ∩ s₂)
Module: Mathlib.ModelTheory.DirectLimit

Goal state before:
pp: case mk.mk
L : Language
ι : Type v
inst✝³ : Preorder ι
G : ι → Type w
inst✝² : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst✝¹ : IsDirectedOrder ι
inst✝ : DirectedSystem G fun i j h ↦ ⇑(f i j h)
i fst✝¹ : ι
snd✝¹ : G fst✝¹
hx : ⟨fst✝¹, snd✝¹⟩.fst ≤ i
fst✝ : ι
snd✝ : G fst✝
hy : ⟨fst✝, snd✝⟩.fst ≤ i
j : ι
w✝¹ : fst✝¹ ≤ j
w✝ : fst✝ ≤ j
h✝ : (f fst✝¹ j w✝¹) snd✝¹ = (f fst✝ j w✝) snd✝
k : ι
ik : i ≤ k
jk : j ≤ k
h : (f j k jk) ((f fst✝¹ j w✝¹) snd✝¹) = (f j k jk) ((f fst✝ j w✝) snd✝)
⊢ (f i k ik) ((f ⟨fst✝¹, snd✝¹⟩.fst i hx) ⟨fst✝¹, snd✝¹⟩.snd) = (f i k ik) ((f ⟨fst✝, snd✝⟩.fst i hy) ⟨fst✝, snd✝⟩.snd)

Tactic:
rw [DirectedSystem.map_map, DirectedSystem.map_map] at *

Goal state after:
case mk.mk
L : Language
ι : Type v
inst✝³ : Preorder ι
G : ι → Type w
inst✝² : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst✝¹ : IsDirectedOrder ι
inst✝ : DirectedSystem G fun i j h ↦ ⇑(f i j h)
i fst✝¹ : ι
snd✝¹ : G fst✝¹
hx : ⟨fst✝¹, snd✝¹⟩.fst ≤ i
fst✝ : ι
snd✝ : G fst✝
hy : ⟨fst✝, snd✝⟩.fst ≤ i
j : ι
w✝¹ : fst✝¹ ≤ j
w✝ : fst✝ ≤ j
h✝ : (f fst✝¹ j w✝¹) snd✝¹ = (f fst✝ j w✝) snd✝
k : ι
ik : i ≤ k
jk : j ≤ k
h : (f fst✝¹ k ⋯) snd✝¹ = (f fst✝ k ⋯) snd✝
⊢ (f ⟨fst✝¹, snd✝¹⟩.fst k ⋯) ⟨fst✝¹, snd✝¹⟩.snd = (f ⟨fst✝, snd✝⟩.fst k ⋯) ⟨fst✝, snd✝⟩.snd
Module: Mathlib.ModelTheory.DirectLimit

Goal state before:
pp: L : Language
ι : Type v
inst✝³ : Preorder ι
G : ι → Type w
inst✝² : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst✝¹ : IsDirectedOrder ι
inst✝ : DirectedSystem G fun i j h ↦ ⇑(f i j h)
n : ℕ
F : L.Functions n
x : Fin n → Σˣ f
i j : ι
hi : i ∈ upperBounds (range (Sigma.fst ∘ x))
hj : j ∈ upperBounds (range (Sigma.fst ∘ x))
k : ι
ik : i ≤ k
jk : j ≤ k
⊢ funMap F (⇑(f i k ik) ∘ unify f x i hi) = (f j k jk) (funMap F (unify f x j hj))

Tactic:
(f j k jk).map_fun,

Goal state after:
L : Language
ι : Type v
inst✝³ : Preorder ι
G : ι → Type w
inst✝² : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst✝¹ : IsDirectedOrder ι
inst✝ : DirectedSystem G fun i j h ↦ ⇑(f i j h)
n : ℕ
F : L.Functions n
x : Fin n → Σˣ f
i j : ι
hi : i ∈ upperBounds (range (Sigma.fst ∘ x))
hj : j ∈ upperBounds (range (Sigma.fst ∘ x))
k : ι
ik : i ≤ k
jk : j ≤ k
⊢ funMap F (⇑(f i k ik) ∘ unify f x i hi) = funMap F (⇑(f j k jk) ∘ unify f x j hj)
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: ι : Type u_3
s : Set (ι → ℕ)
t : Finset (ι → ℕ)
hs : ∀ (f g : (ι → ℕ) → ℕ), ∑ i ∈ t, f i • id i = ∑ i ∈ t, g i • id i → ∀ i ∈ t, f i = g i
f : (ι → ℕ) → ℤ
ht : ↑t ⊆ s
hf : ∀ i ∉ t, f i = 0
heq : ∑ i ∈ t, f i • toRatVec i = 0
i : ι → ℕ
hi : i ∈ t
⊢ ∑ x ∈ t, (toRatVec ((Int.toNat ∘ f) x • id x) - toRatVec ((Int.toNat ∘ (fun x ↦ -x) ∘ f) x • id x)) =
    ∑ i ∈ t, f i • toRatVec i

Tactic:
refine Finset.sum_congr rfl fun j hj => ?_

Goal state after:
ι : Type u_3
s : Set (ι → ℕ)
t : Finset (ι → ℕ)
hs : ∀ (f g : (ι → ℕ) → ℕ), ∑ i ∈ t, f i • id i = ∑ i ∈ t, g i • id i → ∀ i ∈ t, f i = g i
f : (ι → ℕ) → ℤ
ht : ↑t ⊆ s
hf : ∀ i ∉ t, f i = 0
heq : ∑ i ∈ t, f i • toRatVec i = 0
i : ι → ℕ
hi : i ∈ t
j : ι → ℕ
hj : j ∈ t
⊢ toRatVec ((Int.toNat ∘ f) j • id j) - toRatVec ((Int.toNat ∘ (fun x ↦ -x) ∘ f) j • id j) = f j • toRatVec j
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
⊢ hs.fundamentalDomain.Finite

Tactic:
have := Fintype.ofFinite ι

Goal state after:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
this : Fintype ι
⊢ hs.fundamentalDomain.Finite
Module: Mathlib.ModelTheory.PartialEquiv

Goal state before:
pp: L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
g : L.FGEquiv M N
H : L.IsExtensionPair M N
X : Set M
left✝ : X.Countable
X_gen : (closure L).toFun X = ⊤
x✝ : Countable ↑X
⊢ ∃ f, ↑g ≤ f.toPartialEquiv

Tactic:
have _ : Encodable (↑X : Type _) := Encodable.ofCountable _

Goal state after:
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
g : L.FGEquiv M N
H : L.IsExtensionPair M N
X : Set M
left✝ : X.Countable
X_gen : (closure L).toFun X = ⊤
x✝¹ : Countable ↑X
x✝ : Encodable ↑X
⊢ ∃ f, ↑g ≤ f.toPartialEquiv
Module: Mathlib.ModelTheory.PartialEquiv

Goal state before:
pp: L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
g : L.FGEquiv M N
ext_dom : L.IsExtensionPair M N
ext_cod : L.IsExtensionPair N M
X : Set M
X_count : X.Countable
X_gen : (closure L).toFun X = ⊤
Y : Set N
Y_count : Y.Countable
Y_gen : (closure L).toFun Y = ⊤
x✝ : Countable ↑X
⊢ ∃ f, ↑g ≤ f.toEmbedding.toPartialEquiv

Tactic:
have _ : Encodable (↑X : Type _) := Encodable.ofCountable _

Goal state after:
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
g : L.FGEquiv M N
ext_dom : L.IsExtensionPair M N
ext_cod : L.IsExtensionPair N M
X : Set M
X_count : X.Countable
X_gen : (closure L).toFun X = ⊤
Y : Set N
Y_count : Y.Countable
Y_gen : (closure L).toFun Y = ⊤
x✝¹ : Countable ↑X
x✝ : Encodable ↑X
⊢ ∃ f, ↑g ≤ f.toEmbedding.toPartialEquiv
Module: Mathlib.ModelTheory.Fraisse

Goal state before:
pp: case mp
L : Language
ι : Type w
inst✝⁴ : Preorder ι
inst✝³ : IsDirectedOrder ι
inst✝² : Nonempty ι
G : ι → Type (max w w')
inst✝¹ : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst✝ : DirectedSystem G fun i j h ↦ ⇑(f i j h)
M : Bundled L.Structure
Mfg : Structure.FG L ↑M
e : ↑M ↪[L] DirectLimit G f
s : Finset (DirectLimit G f)
hs : (closure L).toFun ↑s = e.toHom.range
out : Quotient (DirectLimit.setoid G f) → Structure.Sigma f := Quotient.out
⊢ ∃ i, M ∈ L.age (G i)

Tactic:
obtain ⟨i, hi⟩ := Finset.exists_le (s.image (Sigma.fst ∘ out))

Goal state after:
case mp
L : Language
ι : Type w
inst✝⁴ : Preorder ι
inst✝³ : IsDirectedOrder ι
inst✝² : Nonempty ι
G : ι → Type (max w w')
inst✝¹ : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst✝ : DirectedSystem G fun i j h ↦ ⇑(f i j h)
M : Bundled L.Structure
Mfg : Structure.FG L ↑M
e : ↑M ↪[L] DirectLimit G f
s : Finset (DirectLimit G f)
hs : (closure L).toFun ↑s = e.toHom.range
out : Quotient (DirectLimit.setoid G f) → Structure.Sigma f := Quotient.out
i : ι
hi : ∀ i_1 ∈ Finset.image (Sigma.fst ∘ out) s, i_1 ≤ i
⊢ ∃ i, M ∈ L.age (G i)
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
i : ι → ℕ
hi : i ∈ hs.fundamentalDomain \ {hs.base}
⊢ IsSemilinearSet {a | (a ∘ Sum.inl) ∘ Sum.inl + a ∘ Sum.inr = i + (a ∘ Sum.inl) ∘ Sum.inr}

Tactic:
have := Fintype.ofFinite ι

Goal state after:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
i : ι → ℕ
hi : i ∈ hs.fundamentalDomain \ {hs.base}
this : Fintype ι
⊢ IsSemilinearSet {a | (a ∘ Sum.inl) ∘ Sum.inl + a ∘ Sum.inr = i + (a ∘ Sum.inl) ∘ Sum.inr}
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
i : ↑hs.basisSet
⊢ IsSemilinearSet
    {a |
      ((a ∘ Sum.inl) ∘ Sum.inl) ∘ Sum.inl + ↑i + ((a ∘ Sum.inl) ∘ Sum.inl) ∘ Sum.inr + a ∘ Sum.inr =
        hs.base + (a ∘ Sum.inl) ∘ Sum.inr}

Tactic:
have := Fintype.ofFinite ι

Goal state after:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
i : ↑hs.basisSet
this : Fintype ι
⊢ IsSemilinearSet
    {a |
      ((a ∘ Sum.inl) ∘ Sum.inl) ∘ Sum.inl + ↑i + ((a ∘ Sum.inl) ∘ Sum.inl) ∘ Sum.inr + a ∘ Sum.inr =
        hs.base + (a ∘ Sum.inl) ∘ Sum.inr}
Module: Mathlib.ModelTheory.Fraisse

Goal state before:
pp: case mp
L : Language
M : Type w
inst✝ : L.Structure M
M_CG : Structure.CG L M
M_homog : L.IsUltrahomogeneous M
f : M ≃ₚ[L] M
f_FG : f.dom.FG
m : M
S : L.Substructure M := f.dom ⊔ (closure L).toFun {m}
dom_le_S : f.dom ≤ S
f' : ↥S ↪[L] M
eq_f' : f.cod.subtype.comp f.toEquiv.toEmbedding = f'.comp (Substructure.inclusion dom_le_S)
⊢ ∃ g, m ∈ (↑g).dom ∧ ⟨f, f_FG⟩ ≤ g

Tactic:
refine ⟨⟨⟨S, f'.toHom.range, f'.equivRange⟩, f_FG.sup (fg_closure_singleton _)⟩,
      subset_closure.trans (le_sup_right : _ ≤ S) (mem_singleton m), ⟨dom_le_S, ?_⟩⟩

Goal state after:
case mp
L : Language
M : Type w
inst✝ : L.Structure M
M_CG : Structure.CG L M
M_homog : L.IsUltrahomogeneous M
f : M ≃ₚ[L] M
f_FG : f.dom.FG
m : M
S : L.Substructure M := f.dom ⊔ (closure L).toFun {m}
dom_le_S : f.dom ≤ S
f' : ↥S ↪[L] M
eq_f' : f.cod.subtype.comp f.toEquiv.toEmbedding = f'.comp (Substructure.inclusion dom_le_S)
⊢ (↑⟨{ dom := S, cod := f'.toHom.range, toEquiv := f'.equivRange }, ⋯⟩).cod.subtype.comp
      ((↑⟨{ dom := S, cod := f'.toHom.range, toEquiv := f'.equivRange }, ⋯⟩).toEquiv.toEmbedding.comp
        (Substructure.inclusion dom_le_S)) =
    (↑⟨f, f_FG⟩).cod.subtype.comp (↑⟨f, f_FG⟩).toEquiv.toEmbedding
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: case mpr
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
⊢ (∃ i,
      ↑i ∉ hs.periods ∧
        ∃ y ∈ closure {↑i},
          ∃ z ∈ closure (hs.basisSet \ {↑i}), ∃ z' ∈ closure (hs.basisSet \ {↑i}), x + z' = hs.base + ↑i + y + z) →
    hs.fract x = hs.base ∧ ∃ i, ↑i ∉ hs.periods ∧ 0 < hs.floor x i

Tactic:
intro ⟨i, hi, y, hy, z, hz, z', hz', heq⟩

Goal state after:
case mpr
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
i : ↑hs.basisSet
hi : ↑i ∉ hs.periods
y : ι → ℕ
hy : y ∈ closure {↑i}
z : ι → ℕ
hz : z ∈ closure (hs.basisSet \ {↑i})
z' : ι → ℕ
hz' : z' ∈ closure (hs.basisSet \ {↑i})
heq : x + z' = hs.base + ↑i + y + z
⊢ hs.fract x = hs.base ∧ ∃ i, ↑i ∉ hs.periods ∧ 0 < hs.floor x i
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
i : ↑hs.basisSet
hi : i ∈ {i | ↑i ∉ hs.periods}
⊢ IsSemilinearSet
    {a |
      ((a ∘ Sum.inl) ∘ Sum.inl) ∘ Sum.inl + a ∘ Sum.inr =
        hs.base + ↑i + ((a ∘ Sum.inl) ∘ Sum.inl) ∘ Sum.inr + (a ∘ Sum.inl) ∘ Sum.inr}

Tactic:
have := Fintype.ofFinite ι

Goal state after:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
i : ↑hs.basisSet
hi : i ∈ {i | ↑i ∉ hs.periods}
this : Fintype ι
⊢ IsSemilinearSet
    {a |
      ((a ∘ Sum.inl) ∘ Sum.inl) ∘ Sum.inl + a ∘ Sum.inr =
        hs.base + ↑i + ((a ∘ Sum.inl) ∘ Sum.inl) ∘ Sum.inr + (a ∘ Sum.inl) ∘ Sum.inr}
Module: Mathlib.Topology.Baire.LocallyCompactRegular

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
s : Set X
inst✝¹ : R1Space X
inst✝ : LocallyCompactSpace X
f : ℕ → Set X
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
U : Set X
U_open : IsOpen U
U_nonempty : U.Nonempty
K : ℕ → PositiveCompacts X
hK_anti : ∀ (n : ℕ), K (n + 1) ≤ K n
hKf : ∀ (n : ℕ), closure ↑(K (n + 1)) ⊆ f n
hKU : closure ↑(K 0) ⊆ U
⊢ (U ∩ ⋂ n, f n).Nonempty

Tactic:
have hK_subset : (⋂ n, closure (K n) : Set X) ⊆ U ∩ ⋂ n, f n := fun x hx ↦ by
    simp only [mem_iInter, mem_inter_iff] at hx ⊢
    exact ⟨hKU <| hx 0, fun n ↦ hKf n <| hx (n + 1)⟩

Goal state after:
X : Type u_1
inst✝² : TopologicalSpace X
s : Set X
inst✝¹ : R1Space X
inst✝ : LocallyCompactSpace X
f : ℕ → Set X
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
U : Set X
U_open : IsOpen U
U_nonempty : U.Nonempty
K : ℕ → PositiveCompacts X
hK_anti : ∀ (n : ℕ), K (n + 1) ≤ K n
hKf : ∀ (n : ℕ), closure ↑(K (n + 1)) ⊆ f n
hKU : closure ↑(K 0) ⊆ U
hK_subset : ⋂ n, closure ↑(K n) ⊆ U ∩ ⋂ n, f n
⊢ (U ∩ ⋂ n, f n).Nonempty
Module: Mathlib.RingTheory.ZMod.UnitsCyclic

Goal state before:
pp: case hfin
p : ℕ
hp : Nat.Prime p
m : ℕ
hm0 : m ≠ 0
hpm : m + 2 ≤ p * m
a : ℤ
ha : ¬↑p ∣ a
n✝ n : ℕ
this✝ : Fact (Nat.Prime p)
this : ∀ (m_1 : ℕ), ∃ y, (1 + ↑p ^ m * ↑a) ^ p ^ m_1 = 1 + ↑p ^ m_1 * ↑p ^ m * (↑a + ↑p * y)
y : ZMod (p ^ (n + 1 + m))
hy : (1 + ↑p ^ m * ↑a) ^ p ^ (n + 1) = 1 + ↑p ^ (n + 1) * ↑p ^ m * (↑a + ↑p * y)
⊢ 1 + ↑p ^ (n + 1 + m) * (↑a + ↑p * y) = 1

Tactic:
← Nat.cast_pow

Goal state after:
case hfin
p : ℕ
hp : Nat.Prime p
m : ℕ
hm0 : m ≠ 0
hpm : m + 2 ≤ p * m
a : ℤ
ha : ¬↑p ∣ a
n✝ n : ℕ
this✝ : Fact (Nat.Prime p)
this : ∀ (m_1 : ℕ), ∃ y, (1 + ↑p ^ m * ↑a) ^ p ^ m_1 = 1 + ↑p ^ m_1 * ↑p ^ m * (↑a + ↑p * y)
y : ZMod (p ^ (n + 1 + m))
hy : (1 + ↑p ^ m * ↑a) ^ p ^ (n + 1) = 1 + ↑p ^ (n + 1) * ↑p ^ m * (↑a + ↑p * y)
⊢ 1 + ↑(p ^ (n + 1 + m)) * (↑a + ↑p * y) = 1
Module: Mathlib.RingTheory.ZMod.UnitsCyclic

Goal state before:
pp: case succ
p : ℕ
hp : Nat.Prime p
hp2 : p ≠ 2
this✝¹ : Fact (Nat.Prime p)
n : ℕ
a : ZMod (p ^ (n + 1)) := 1 + ↑p
ha_def : a = 1 + ↑p
ha : IsUnit a
ha' : orderOf ha.unit = p ^ n
b : (ZMod (p ^ (n + 1)))ˣ
hc : orderOf ((unitsMap ⋯) b) = p - 1
this✝ : p - 1 ∣ orderOf b
k : ℕ := orderOf b / (p - 1)
this : orderOf (b ^ k) = p - 1
⊢ ∃ g, orderOf g = Nat.card (ZMod (p ^ (n + 1)))ˣ

Tactic:
use ha.unit * b ^ k

Goal state after:
case h
p : ℕ
hp : Nat.Prime p
hp2 : p ≠ 2
this✝¹ : Fact (Nat.Prime p)
n : ℕ
a : ZMod (p ^ (n + 1)) := ⋯
ha_def : a = 1 + ↑p
ha : IsUnit a
ha' : orderOf ha.unit = p ^ n
b : (ZMod (p ^ (n + 1)))ˣ
hc : orderOf ((unitsMap ⋯) b) = p - 1
this✝ : p - 1 ∣ orderOf b
k : ℕ := ⋯
this : orderOf (b ^ k) = p - 1
⊢ orderOf (ha.unit * b ^ k) = Nat.card (ZMod (p ^ (n + 1)))ˣ
Module: Mathlib.NumberTheory.BernoulliPolynomials

Goal state before:
pp: n : ℕ
⊢ ∑ x ∈ range (n + 1),
      ↑((n + 1).choose x) • ∑ i ∈ range (x + 1), (monomial i) (_root_.bernoulli (x - i) * ↑(x.choose i)) =
    (monomial n) (↑n + 1)

Tactic:
Finset.smul_sum,

Goal state after:
n : ℕ
⊢ ∑ x ∈ range (n + 1),
      ∑ x_1 ∈ range (x + 1), ↑((n + 1).choose x) • (monomial x_1) (_root_.bernoulli (x - x_1) * ↑(x.choose x_1)) =
    (monomial n) (↑n + 1)
Module: Mathlib.NumberTheory.PrimeCounting

Goal state before:
pp: a k : ℕ
h0 : a ≠ 0
h1 : a ≤ k
n : ℕ
⊢ π (k + n) ≤ π k + φ a * (n / a + 1)

Tactic:
rw [primeCounting_eq_primeCounting'_succ]

Goal state after:
a k : ℕ
h0 : a ≠ 0
h1 : a ≤ k
n : ℕ
⊢ π' (k + n + 1) ≤ π k + φ a * (n / a + 1)
Module: Mathlib.NumberTheory.Primorial

Goal state before:
pp: n : ℕ
hn1 : n ≠ 1
hn : Odd n
⊢ (n + 1)# = n#

Tactic:
refine prod_congr ?_ fun _ _ ↦ rfl
  rw [range_add_one, filter_insert, if_neg fun h ↦ not_even_iff_odd.2 hn _]
  exact fun h ↦ h.even_sub_one <| mt succ.inj hn1

Goal state after:
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: n p : ℕ
hne : ∀ (m : ℕ), ↑m ! ≠ 0
h_cauchy :
  ((PowerSeries.mk fun p ↦ bernoulli p / ↑p !) * PowerSeries.mk fun q ↦ (coeff (q + 1)) (exp ℚ ^ n)) =
    PowerSeries.mk fun p ↦ ∑ i ∈ range (p + 1), bernoulli i * ↑((p + 1).choose i) * ↑n ^ (p + 1 - i) / ↑(p + 1)!
this :
  (PowerSeries.mk fun p ↦ ∑ k ∈ range n, ↑k ^ p * (algebraMap ℚ ℚ) (↑p !)⁻¹) =
    PowerSeries.mk fun p ↦ ∑ i ∈ range (p + 1), bernoulli i * ↑((p + 1).choose i) * ↑n ^ (p + 1 - i) / ↑(p + 1)!
⊢ ∑ k ∈ range n, ↑k ^ p = (∑ i ∈ range (p + 1), bernoulli i * ↑((p + 1).choose i) * ↑n ^ (p + 1 - i) / ↑(p + 1)!) * ↑p !

Tactic:
rw [← div_eq_iff (hne p), div_eq_mul_inv, sum_mul]

Goal state after:
n p : ℕ
hne : ∀ (m : ℕ), ↑m ! ≠ 0
h_cauchy :
  ((PowerSeries.mk fun p ↦ bernoulli p / ↑p !) * PowerSeries.mk fun q ↦ (coeff (q + 1)) (exp ℚ ^ n)) =
    PowerSeries.mk fun p ↦ ∑ i ∈ range (p + 1), bernoulli i * ↑((p + 1).choose i) * ↑n ^ (p + 1 - i) / ↑(p + 1)!
this :
  (PowerSeries.mk fun p ↦ ∑ k ∈ range n, ↑k ^ p * (algebraMap ℚ ℚ) (↑p !)⁻¹) =
    PowerSeries.mk fun p ↦ ∑ i ∈ range (p + 1), bernoulli i * ↑((p + 1).choose i) * ↑n ^ (p + 1 - i) / ↑(p + 1)!
⊢ ∑ i ∈ range n, ↑i ^ p * (↑p !)⁻¹ =
    ∑ i ∈ range (p + 1), bernoulli i * ↑((p + 1).choose i) * ↑n ^ (p + 1 - i) / ↑(p + 1)!
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: p l : ℕ
inst✝ : Fact (Nat.Prime p)
v : ℕ
hv : v ∈ Ico 1 p
⊢ (↑(Units.mk0 ↑v ⋯)).val = v

Tactic:
by simp [ZMod.val_cast_of_lt (Finset.mem_Ico.mp hv).2]

Goal state after:
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
h : ‖↑r‖ ≤ 1
n : ℤ := modPart p r
⊢ ‖⟨↑r, h⟩ - ↑(modPart p r)‖ < 1

Tactic:
norm_lt_one_iff_dvd,

Goal state after:
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
h : ‖↑r‖ ≤ 1
n : ℤ := modPart p r
⊢ ↑p ∣ ⟨↑r, h⟩ - ↑(modPart p r)
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: ⊢ ∃ C, ∀ (x : ℝ), ψ x - θ x ≤ C * √x

Tactic:
use (log 4 + 4) * 3

Goal state after:
case h
⊢ ∀ (x : ℝ), ψ x - θ x ≤ (log 4 + 4) * 3 * √x
Module: Mathlib.NumberTheory.ClassNumber.Finite

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁸ : EuclideanDomain R
inst✝⁷ : CommRing S
inst✝⁶ : IsDomain S
inst✝⁵ : Algebra R S
abv : AbsoluteValue R ℤ
ι : Type u_5
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
bS : Basis ι R S
adm : abv.IsAdmissible
inst✝² : Infinite R
inst✝¹ : DecidableEq R
inst✝ : Algebra.IsAlgebraic R S
a b : S
hb : b ≠ 0
⊢ ∃ q, ∃ r ∈ finsetApprox bS adm, abv ((Algebra.norm R) (r • a - q * b)) < abv ((Algebra.norm R) b)

Tactic:
by
  obtain ⟨a', b', hb', h⟩ := Algebra.IsAlgebraic.exists_smul_eq_mul R a hb
  obtain ⟨q, r, hr, hqr⟩ := exists_mem_finsetApprox bS adm a' hb'
  refine ⟨q, r, hr, ?_⟩
  refine
    lt_of_mul_lt_mul_left ?_ (show 0 ≤ abv (Algebra.norm R (algebraMap R S b')) from abv.nonneg _)
  refine
    lt_of_le_of_lt (le_of_eq ?_)
      (mul_lt_mul hqr le_rfl (abv.pos ((Algebra.norm_ne_zero_iff_of_basis bS).mpr hb))
        (abv.nonneg _))
  rw [← abv.map_mul, ← map_mul, ← abv.map_mul, ← map_mul, ← Algebra.smul_def,
    smul_sub b', sub_mul, smul_comm, h, mul_comm b a', Algebra.smul_mul_assoc r a' b,
    Algebra.smul_mul_assoc b' q b]

Goal state after:
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: case inr
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
h : x.zmodRepr = 0
⊢ ‖↑x.zmodRepr‖ = ‖x‖ ↔ ‖x‖ = 1 ∨ x = 0

Tactic:
· rw [eq_comm, h]
    simp [← norm_natCast_zmodRepr_eq_one_iff, h]

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx : 2 ≤ x
a : ℕ → ℝ := (Set.ofPred Nat.Prime).indicator fun n ↦ log ↑n
⊢ (log x)⁻¹ * ∑ k ∈ Icc 0 ⌊x⌋₊, a k - ∫ (x : ℝ) in 2..x, deriv (fun n ↦ (log n)⁻¹) x * ∑ k ∈ Icc 0 ⌊x⌋₊, a k =
    θ x / log x + ∫ (t : ℝ) in 2..x, θ t / (t * log t ^ 2)

pp: case hf_diff
x : ℝ
hx : 2 ≤ x
a : ℕ → ℝ := (Set.ofPred Nat.Prime).indicator fun n ↦ log ↑n
⊢ ∀ t ∈ Set.Icc 2 x, DifferentiableAt ℝ (fun n ↦ (log n)⁻¹) t

pp: case hf_int
x : ℝ
hx : 2 ≤ x
a : ℕ → ℝ := (Set.ofPred Nat.Prime).indicator fun n ↦ log ↑n
⊢ IntegrableOn (deriv fun n ↦ (log n)⁻¹) (Set.Icc 2 x) volume

Tactic:
· -- Rewrite the derivative inside the integral
    have int_deriv (f : ℝ → ℝ) :
        ∫ u in 2..x, deriv (fun x ↦ (log x)⁻¹) u * f u =
        ∫ u in 2..x, f u * -(u * log u ^ 2)⁻¹ :=
      intervalIntegral.integral_congr fun u _ ↦ by simp [field]
    rw [int_deriv]
    simp [a, Set.indicator_apply, sum_filter, theta_eq_sum_Icc]
    grind

Goal state after:
case hf_diff
x : ℝ
hx : 2 ≤ x
a : ℕ → ℝ := (Set.ofPred Nat.Prime).indicator fun n ↦ log ↑n
⊢ ∀ t ∈ Set.Icc 2 x, DifferentiableAt ℝ (fun n ↦ (log n)⁻¹) t

case hf_int
x : ℝ
hx : 2 ≤ x
a : ℕ → ℝ := (Set.ofPred Nat.Prime).indicator fun n ↦ log ↑n
⊢ IntegrableOn (deriv fun n ↦ (log n)⁻¹) (Set.Icc 2 x) volume
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
a✝ : 4 ≤ x
⊢ ‖∫ (t : ℝ) in 2..x, θ t / (t * log t ^ 2)‖ ≤ log 4 * ‖∫ (t : ℝ) in 2..x, 1 / log t ^ 2‖

Tactic:
simp_rw [norm_eq_abs]

Goal state after:
x : ℝ
a✝ : 4 ≤ x
⊢ |∫ (t : ℝ) in 2..x, θ t / (t * log t ^ 2)| ≤ log 4 * |∫ (t : ℝ) in 2..x, 1 / log t ^ 2|
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
a✝ : 4 ≤ x
⊢ IntegrableOn (fun x ↦ θ x / (x * log x ^ 2)) (Set.uIoc 2 x) volume

Tactic:
Set.uIoc_of_le (by linarith),

Goal state after:
x : ℝ
a✝ : 4 ≤ x
⊢ IntegrableOn (fun x ↦ θ x / (x * log x ^ 2)) (Set.Ioc 2 x) volume
Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter

Goal state before:
pp: L : Type u
inst✝³ : CommRing L
inst✝² : IsDomain L
g : L ≃+* L
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : ∀ (i : ℕ), HasEnoughRootsOfUnity L (p ^ i)
k i : ℕ
hi : k ≤ k + i
ζ : L
hζ : IsPrimitiveRoot ζ (p ^ (k + i))
h : IsPrimitiveRoot (ζ ^ p ^ i) (p ^ k)
h_unit : ⋯.unit = ⋯.unit ^ p ^ i
H₁ : g ζ = ↑(⋯.unit ^ aux g (p ^ (k + i)))
H₂ : ↑(p ^ i) * ↑(p ^ k) ∣ ↑(p ^ i) * (aux g (p ^ (k + i)) - aux g (p ^ k))
⊢ ↑p ^ k ∣ aux g (p ^ (k + i)) - aux g (p ^ k)

Tactic:
mul_dvd_mul_iff_left (by simp [NeZero.ne p]),

Goal state after:
L : Type u
inst✝³ : CommRing L
inst✝² : IsDomain L
g : L ≃+* L
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : ∀ (i : ℕ), HasEnoughRootsOfUnity L (p ^ i)
k i : ℕ
hi : k ≤ k + i
ζ : L
hζ : IsPrimitiveRoot ζ (p ^ (k + i))
h : IsPrimitiveRoot (ζ ^ p ^ i) (p ^ k)
h_unit : ⋯.unit = ⋯.unit ^ p ^ i
H₁ : g ζ = ↑(⋯.unit ^ aux g (p ^ (k + i)))
H₂ : ↑(p ^ k) ∣ aux g (p ^ (k + i)) - aux g (p ^ k)
⊢ ↑p ^ k ∣ aux g (p ^ (k + i)) - aux g (p ^ k)
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: case hbc
x : ℝ
hx : 1 ≤ x
⊢ #({a ∈ ⌊x⌋₊.primesLE | ↑a ≤ √x}) ≤ #(Icc 1 ⌊√x⌋₊)

Tactic:
refine card_le_card fun p hp ↦ ?_

Goal state after:
case hbc
x : ℝ
hx : 1 ≤ x
p : ℕ
hp : p ∈ {a ∈ ⌊x⌋₊.primesLE | ↑a ≤ √x}
⊢ p ∈ Icc 1 ⌊√x⌋₊