mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.VectorMeasure.SetIntegral

Goal state before:
pp: X : Type u_2
E : Type u_3
F✝ : Type u_4
G : Type u_5
mX : MeasurableSpace X
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F✝
inst✝³ : NormedAddCommGroup G
μ : VectorMeasure X F✝
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedSpace ℝ F✝
inst✝ : NormedSpace ℝ G
B : E →L[ℝ] F✝ →L[ℝ] G
ι : Type u_7
f : X → E
hfi : AEStronglyMeasurable f μ.variation
F : ι → X → E
l : Filter ι
hFi : ∀ᶠ (i : ι) in l, μ.Integrable (F i)
s : Set X
hF : Tendsto (fun i ↦ eLpNorm (fun x ↦ F i x - f x) 1 μ.variation) l (𝓝 0)
i : ι
⊢ (μ.restrict s).variation ≤ μ.variation

Tactic:
variation_restrict_le

Goal state after:
X : Type u_2
E : Type u_3
F✝ : Type u_4
G : Type u_5
mX : MeasurableSpace X
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F✝
inst✝³ : NormedAddCommGroup G
μ : VectorMeasure X F✝
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedSpace ℝ F✝
inst✝ : NormedSpace ℝ G
B : E →L[ℝ] F✝ →L[ℝ] G
ι : Type u_7
f : X → E
hfi : AEStronglyMeasurable f μ.variation
F : ι → X → E
l : Filter ι
hFi : ∀ᶠ (i : ι) in l, μ.Integrable (F i)
s : Set X
hF : Tendsto (fun i ↦ eLpNorm (fun x ↦ F i x - f x) 1 μ.variation) l (𝓝 0)
i : ι
⊢ μ.variation.restrict s ≤ μ.variation
Module: Mathlib.MeasureTheory.VectorMeasure.WithDensityVec

Goal state before:
pp: X : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
mX : MeasurableSpace X
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace ℝ G
μ : VectorMeasure X F
f : X → E
B : E →L[ℝ] F →L[ℝ] G
inst✝ : CompleteSpace G
hf : μ.Integrable f
hB : ∀ (x : E) (y : F), ‖(B x) y‖₊ = ‖B.flip y‖₊ * ‖x‖₊
s : Set X
hs : MeasurableSet s
ε : NNReal
εpos : 0 < ε
δ : NNReal := ε / 3
δpos : 0 < δ
g : X →ₛ E
hg : eLpNorm (f - ⇑g) 1 (μ.transpose B).variation ≤ ↑δ
gmem : MemLp (⇑g) 1 μ.variation
I1 : ∫⁻ (a : X) in s, ‖f a‖ₑ ∂(μ.transpose B).variation ≤ ∫⁻ (a : X) in s, ‖g a‖ₑ ∂(μ.transpose B).variation + ↑δ
I2 :
  ∫⁻ (a : X) in s, ‖g a‖ₑ ∂(μ.transpose B).variation =
    ∑ i ∈ g.range, ‖i‖ₑ * ((μ.transpose B).restrict s).variation (⇑g ⁻¹' {i})
ρ : ℝ≥0∞
ρpos : ρ > 0
hρ : ∑ i ∈ g.range, ‖i‖ₑ * ρ ≤ ↑δ
P : E → Finset (Set X)
Pg : ∀ (i : E), ∀ t ∈ P i, t ⊆ ⇑g ⁻¹' {i}
Pdisj : ∀ (i : E), (↑(P i)).PairwiseDisjoint id
Pmeas : ∀ (i : E), ∀ t ∈ P i, MeasurableSet t
hP :
  ∀ (i : E),
    ‖i‖ₑ * ((μ.transpose B).restrict s).variation (⇑g ⁻¹' {i}) ≤
      ‖i‖ₑ * (∑ p ∈ P i, ‖((μ.transpose B).restrict s) p‖ₑ + ρ)
⊢ ∑ i ∈ g.range, ‖i‖ₑ * ((μ.transpose B).restrict s).variation (⇑g ⁻¹' {i}) ≤
    ∑ i ∈ g.range, ‖i‖ₑ * (∑ p ∈ P i, ‖((μ.transpose B).restrict s) p‖ₑ + ρ)

Tactic:
gcongr 1 with i hi
      exact hP i

Goal state after:
Module: Mathlib.ModelTheory.FinitelyGenerated

Goal state before:
pp: case mpr
L : Language
M : Type u_1
inst✝ : L.Structure M
N : L.Substructure M
n : ℕ
s : Fin n → M
hs : (closure L).toFun (range s) = N
⊢ ∃ S, S.Finite ∧ (closure L).toFun S = N

Tactic:
exact ⟨range s, finite_range s, hs⟩

Goal state after:
Module: Mathlib.ModelTheory.FinitelyGenerated

Goal state before:
pp: L : Language
M : Type u_1
inst✝¹ : L.Structure M
N : Type u_2
inst✝ : L.Structure N
f : M →[L] N
s : L.Substructure M
hs : s.FG
t : Set M
ht : t.Finite ∧ (closure L).toFun t = s
⊢ Substructure.map f ((closure L).toFun t) = Substructure.map f s

Tactic:
ht.2

Goal state after:
L : Language
M : Type u_1
inst✝¹ : L.Structure M
N : Type u_2
inst✝ : L.Structure N
f : M →[L] N
s : L.Substructure M
hs : s.FG
t : Set M
ht : t.Finite ∧ (closure L).toFun t = s
⊢ Substructure.map f s = Substructure.map f s
Module: Mathlib.ModelTheory.FinitelyGenerated

Goal state before:
pp: L : Language
M : Type u_1
inst✝¹ : L.Structure M
N : Type u_2
inst✝ : L.Structure N
f : M →[L] N
s : L.Substructure M
hs : s.CG
t : Set M
ht : t.Countable ∧ (closure L).toFun t = s
⊢ Substructure.map f ((closure L).toFun t) = Substructure.map f s

Tactic:
ht.2

Goal state after:
L : Language
M : Type u_1
inst✝¹ : L.Structure M
N : Type u_2
inst✝ : L.Structure N
f : M →[L] N
s : L.Substructure M
hs : s.CG
t : Set M
ht : t.Countable ∧ (closure L).toFun t = s
⊢ Substructure.map f s = Substructure.map f s
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: case hs₁
M : Type u_1
inst✝ : AddCommMonoid M
P : AddSubmonoid M
s₁' s₂' : Set ↥P
hs₁' : IsSemilinearSet s₁'
hs₁ : IsSemilinearSet (Subtype.val '' s₁')
hs₂' : IsSemilinearSet s₂'
hs₂ : IsSemilinearSet (Subtype.val '' s₂')
n : ℕ
f : (Fin n → ℕ) →+ ↥P
hf : Function.Surjective ⇑f
⊢ IsSemilinearSet s₁'

Tactic:
assumption

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

Goal state before:
pp: case hs₂
M : Type u_1
inst✝ : AddCommMonoid M
P : AddSubmonoid M
s₁' s₂' : Set ↥P
hs₁' : IsSemilinearSet s₁'
hs₁ : IsSemilinearSet (Subtype.val '' s₁')
hs₂' : IsSemilinearSet s₂'
hs₂ : IsSemilinearSet (Subtype.val '' s₂')
n : ℕ
f : (Fin n → ℕ) →+ ↥P
hf : Function.Surjective ⇑f
⊢ IsSemilinearSet s₂'

Tactic:
assumption

Goal state after:
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)
inst✝ : Nonempty ι
n : ℕ
R : L.Relations n
x y : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
xy : x ≈ y
⊢ RelMap R x = RelMap R y

Tactic:
obtain ⟨i, hx, hy, h⟩ := exists_unify_eq G f xy
    refine _root_.trans (relMap_equiv_unify G f R x i hx)
      (_root_.trans ?_ (symm (relMap_equiv_unify G f R y i hy)))
    rw [h]

Goal state after:
Module: Mathlib.ModelTheory.PartialEquiv

Goal state before:
pp: L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f g : M ≃ₚ[L] N
dom_f : L.Substructure M
cod_f : L.Substructure N
equiv_f : ↥dom_f ≃[L] ↥cod_f
le_fg : { dom := dom_f, cod := cod_f, toEquiv := equiv_f } ≤ g
le_gf : g ≤ { dom := dom_f, cod := cod_f, toEquiv := equiv_f }
⊢ { dom := dom_f, cod := cod_f, toEquiv := equiv_f } = g

Tactic:
cases _root_.le_antisymm (dom_le_dom le_fg) (dom_le_dom le_gf)

Goal state after:
case refl
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f g : M ≃ₚ[L] N
cod_f : L.Substructure N
equiv_f : ↥g.1 ≃[L] ↥cod_f
le_fg : { dom := g.1, cod := cod_f, toEquiv := equiv_f } ≤ g
le_gf : g ≤ { dom := g.1, cod := cod_f, toEquiv := equiv_f }
⊢ { dom := g.1, cod := cod_f, toEquiv := equiv_f } = g
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
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

Tactic:
conv_rhs => rw [← (f j).toNat_sub_toNat_neg]

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).toNat - ↑(-f j).toNat) • toRatVec j
Module: Mathlib.ModelTheory.PartialEquiv

Goal state before:
pp: case h
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
g : M ≃ₚ[L] N
cod_f : L.Substructure N
equiv_f : ↥g.1 ≃[L] ↥cod_f
h :
  ∀ (x : M) (h : x ∈ { dom := g.1, cod := cod_f, toEquiv := equiv_f }.dom),
    { dom := g.1, cod := cod_f, toEquiv := equiv_f }.cod.subtype
        ({ dom := g.1, cod := cod_f, toEquiv := equiv_f }.toEquiv ⟨x, h⟩) =
      g.cod.subtype (g.toEquiv ⟨x, ⋯⟩)
x : M
hx : x ∈ { dom := g.1, cod := cod_f, toEquiv := equiv_f }.dom
⊢ (g.cod.subtype.comp (g.toEquiv.toEmbedding.comp (inclusion ⋯))) ⟨x, hx⟩ =
    ({ dom := g.1, cod := cod_f, toEquiv := equiv_f }.cod.subtype.comp
        { dom := g.1, cod := cod_f, toEquiv := equiv_f }.toEquiv.toEmbedding)
      ⟨x, hx⟩

pp: case h
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
g : M ≃ₚ[L] N
cod_f : L.Substructure N
equiv_f : ↥g.1 ≃[L] ↥cod_f
h :
  ∀ (x : M) (h : x ∈ { dom := g.1, cod := cod_f, toEquiv := equiv_f }.dom),
    { dom := g.1, cod := cod_f, toEquiv := equiv_f }.cod.subtype
        ({ dom := g.1, cod := cod_f, toEquiv := equiv_f }.toEquiv ⟨x, h⟩) =
      g.cod.subtype (g.toEquiv ⟨x, ⋯⟩)
x : M
hx : x ∈ g.dom
⊢ ({ dom := g.1, cod := cod_f, toEquiv := equiv_f }.cod.subtype.comp
        ({ dom := g.1, cod := cod_f, toEquiv := equiv_f }.toEquiv.toEmbedding.comp (inclusion ⋯)))
      ⟨x, hx⟩ =
    (g.cod.subtype.comp g.toEquiv.toEmbedding) ⟨x, hx⟩

Tactic:
· exact (h x hx).symm

Goal state after:
case h
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
g : M ≃ₚ[L] N
cod_f : L.Substructure N
equiv_f : ↥g.1 ≃[L] ↥cod_f
h :
  ∀ (x : M) (h : x ∈ { dom := g.1, cod := cod_f, toEquiv := equiv_f }.dom),
    { dom := g.1, cod := cod_f, toEquiv := equiv_f }.cod.subtype
        ({ dom := g.1, cod := cod_f, toEquiv := equiv_f }.toEquiv ⟨x, h⟩) =
      g.cod.subtype (g.toEquiv ⟨x, ⋯⟩)
x : M
hx : x ∈ g.dom
⊢ ({ dom := g.1, cod := cod_f, toEquiv := equiv_f }.cod.subtype.comp
        ({ dom := g.1, cod := cod_f, toEquiv := equiv_f }.toEquiv.toEmbedding.comp (inclusion ⋯)))
      ⟨x, hx⟩ =
    (g.cod.subtype.comp g.toEquiv.toEmbedding) ⟨x, hx⟩
Module: Mathlib.ModelTheory.PartialEquiv

Goal state before:
pp: L : Language
M : Type w
N : Type w'
inst✝⁴ : L.Structure M
inst✝³ : L.Structure N
ι : Type u_1
inst✝² : Preorder ι
inst✝¹ : Nonempty ι
inst✝ : IsDirectedOrder ι
S : ι →o M ≃ₚ[L] N
i : ι
⊢ (partialEquivLimit S).toEquiv.toEmbedding.comp (inclusion ⋯) = (inclusion ⋯).comp (S i).toEquiv.toEmbedding

Tactic:
simp only [partialEquivLimit, Equiv.comp_toEmbedding, Embedding.comp_assoc]

Goal state after:
L : Language
M : Type w
N : Type w'
inst✝⁴ : L.Structure M
inst✝³ : L.Structure N
ι : Type u_1
inst✝² : Preorder ι
inst✝¹ : Nonempty ι
inst✝ : IsDirectedOrder ι
S : ι →o M ≃ₚ[L] N
i : ι
⊢ (Equiv_iSup { toFun := fun i ↦ (S i).cod, monotone' := ⋯ }).toEmbedding.comp
      ((equiv_lift L ι (fun i ↦ ↥(S i).dom) (fun x x_1 hij ↦ inclusion ⋯) (fun i ↦ ↥(S i).cod)
              (fun x x_1 hij ↦ inclusion ⋯) (fun i ↦ (S i).toEquiv) ⋯).toEmbedding.comp
        ((Equiv_iSup { toFun := fun i ↦ (S i).dom, monotone' := ⋯ }).symm.toEmbedding.comp (inclusion ⋯))) =
    (inclusion ⋯).comp (S i).toEquiv.toEmbedding
Module: Mathlib.ModelTheory.PartialEquiv

Goal state before:
pp: L : Language
M : Type w
N : Type w'
inst✝⁴ : L.Structure M
inst✝³ : L.Structure N
ι : Type u_1
inst✝² : Preorder ι
inst✝¹ : Nonempty ι
inst✝ : IsDirectedOrder ι
S : ι →o M ≃ₚ[L] N
i : ι
⊢ (partialEquivLimit S).cod.subtype.comp ((partialEquivLimit S).toEquiv.toEmbedding.comp (inclusion ⋯)) =
    (S i).cod.subtype.comp (S i).toEquiv.toEmbedding

Tactic:
simp only [partialEquivLimit_comp_inclusion]

Goal state after:
L : Language
M : Type w
N : Type w'
inst✝⁴ : L.Structure M
inst✝³ : L.Structure N
ι : Type u_1
inst✝² : Preorder ι
inst✝¹ : Nonempty ι
inst✝ : IsDirectedOrder ι
S : ι →o M ≃ₚ[L] N
i : ι
⊢ (partialEquivLimit S).cod.subtype.comp ((inclusion ⋯).comp (S i).toEquiv.toEmbedding) =
    (S i).cod.subtype.comp (S i).toEquiv.toEmbedding
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: case e'_2.a
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
hx₁ : hs.fract x = hs.base
hx₂ : ∀ (i : ↑hs.basisSet), 0 ≤ hs.floor x i ∧ (↑i ∉ hs.periods → hs.floor x i = 0)
i : ↑hs.basisSet
a✝ : i ∈ Finset.univ
⊢ (if ↑i ∈ hs.periods then (hs.floor x i).toNat • ↑i else 0) = (hs.floor x i).toNat • ↑i

pp: case e'_3.a
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
hx₁ : hs.fract x = hs.base
hx₂ : ∀ (i : ↑hs.basisSet), 0 ≤ hs.floor x i ∧ (↑i ∉ hs.periods → hs.floor x i = 0)
i : ↑hs.basisSet
a✝ : i ∈ Finset.univ
⊢ 0 = (-hs.floor x i).toNat • ↑i

Tactic:
· split_ifs with hi
      · simp
      · simp [(hx₂ i).2 hi]

Goal state after:
case e'_3.a
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
hx₁ : hs.fract x = hs.base
hx₂ : ∀ (i : ↑hs.basisSet), 0 ≤ hs.floor x i ∧ (↑i ∉ hs.periods → hs.floor x i = 0)
i : ↑hs.basisSet
a✝ : i ∈ Finset.univ
⊢ 0 = (-hs.floor x i).toNat • ↑i
Module: Mathlib.ModelTheory.Fraisse

Goal state before:
pp: case mpr
L : Language
M : Type w
inst✝ : L.Structure M
h : Countable M
N : Bundled L.Structure
⊢ ⟦N⟧ ∈ Quotient.mk' '' L.age M → ⟦N⟧ ∈ range fun s ↦ ⟦{ α := ↥((closure L).toFun ↑s), str := inferInstance }⟧

Tactic:
· simp only [mem_range, Quotient.eq]
    rintro ⟨P, ⟨⟨s, hs⟩, ⟨PM⟩⟩, hP2⟩
    refine ⟨s.image PM, Setoid.trans (b := P) ?_ <| Quotient.exact hP2⟩
    rw [← Embedding.coe_toHom, Finset.coe_image, closure_image PM.toHom, hs, ← Hom.range_eq_map]
    exact ⟨PM.equivRange.symm⟩

Goal state after:
Module: Mathlib.Order.CountableDenseLinearOrder

Goal state before:
pp: case intro.intro
α : Type u_1
β : Type u_2
inst✝¹¹ : LinearOrder α
inst✝¹⁰ : LinearOrder β
inst✝⁹ : Countable α
inst✝⁸ : DenselyOrdered α
inst✝⁷ : NoMinOrder α
inst✝⁶ : NoMaxOrder α
inst✝⁵ : Nonempty α
inst✝⁴ : Countable β
inst✝³ : DenselyOrdered β
inst✝² : NoMinOrder β
inst✝¹ : NoMaxOrder β
inst✝ : Nonempty β
val✝¹ : Encodable α
val✝ : Encodable β
⊢ Nonempty (α ≃o β)

Tactic:
let to_cofinal : α ⊕ β → Cofinal (PartialIso α β) := fun p ↦
    Sum.recOn p (definedAtLeft β) (definedAtRight α)

Goal state after:
case intro.intro
α : Type u_1
β : Type u_2
inst✝¹¹ : LinearOrder α
inst✝¹⁰ : LinearOrder β
inst✝⁹ : Countable α
inst✝⁸ : DenselyOrdered α
inst✝⁷ : NoMinOrder α
inst✝⁶ : NoMaxOrder α
inst✝⁵ : Nonempty α
inst✝⁴ : Countable β
inst✝³ : DenselyOrdered β
inst✝² : NoMinOrder β
inst✝¹ : NoMaxOrder β
inst✝ : Nonempty β
val✝¹ : Encodable α
val✝ : Encodable β
to_cofinal : α ⊕ β → Cofinal (PartialIso α β) := fun p ↦ Sum.recOn p (definedAtLeft β) (definedAtRight α)
⊢ Nonempty (α ≃o β)
Module: Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt

Goal state before:
pp: ⊢ log * ↑μ = Λ

Tactic:
← vonMangoldt_mul_zeta,

Goal state after:
⊢ Λ * ↑ζ * ↑μ = Λ
Module: Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt

Goal state before:
pp: n : ℕ
this : ∑ i ∈ n.divisors, ↑(μ i) * -Real.log ↑(n / i) = ∑ i ∈ n.divisors, (↑(μ i) * Real.log ↑i - ↑(μ i) * Real.log ↑n)
⊢ ∑ d ∈ n.divisors, ↑(μ d) * Real.log ↑d =
    ∑ x ∈ n.divisors, ↑(μ x) * Real.log ↑x - ↑(∑ x ∈ n.divisors, μ x) * Real.log ↑n

Tactic:
← coe_mul_zeta_apply,

Goal state after:
n : ℕ
this : ∑ i ∈ n.divisors, ↑(μ i) * -Real.log ↑(n / i) = ∑ i ∈ n.divisors, (↑(μ i) * Real.log ↑i - ↑(μ i) * Real.log ↑n)
⊢ ∑ d ∈ n.divisors, ↑(μ d) * Real.log ↑d = ∑ x ∈ n.divisors, ↑(μ x) * Real.log ↑x - ↑((μ * ↑ζ) n) * Real.log ↑n
Module: Mathlib.RingTheory.MvPowerSeries.Derivative

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
i : σ
f : MvPowerSeries σ R
n : σ →₀ ℕ
⊢ (trunc R n) (pderivFun i f) = (pderiv i) ((trunc R (n + single i 1)) f)

Tactic:
by
  ext
  rw [coeff_trunc]
  split_ifs with h
  · rw [coeff_pderivFun, coeff_pderiv, coeff_trunc, if_pos (add_lt_add_left h _)]
  · rw [coeff_pderiv, coeff_trunc, if_neg ((add_lt_add_iff_right _).not.mpr h), zero_mul]

Goal state after:
Module: Mathlib.RingTheory.ZMod.UnitsCyclic

Goal state before:
pp: case neg.inr.inr.ha
n : ℕ
h0 : ¬2 * (2 * n) = 0
h1 : ¬2 * (2 * n) = 1
h2 : ¬2 * (2 * n) = 2
h4 : ¬2 * (2 * n) = 4
hn✝ : Even (2 * (2 * n))
hn : Even (2 * n)
⊢ ¬IsCyclic (ZMod (2 * (2 * n)))ˣ

Tactic:
rw [← mul_assoc, show 2 * 2 = 4 from rfl, isCyclic_units_four_mul_iff]

Goal state after:
case neg.inr.inr.ha
n : ℕ
h0 : ¬2 * (2 * n) = 0
h1 : ¬2 * (2 * n) = 1
h2 : ¬2 * (2 * n) = 2
h4 : ¬2 * (2 * n) = 4
hn✝ : Even (2 * (2 * n))
hn : Even (2 * n)
⊢ ¬(n = 0 ∨ n = 1)
Module: Mathlib.RingTheory.PowerSeries.Exp

Goal state before:
pp: A : Type u_1
inst✝¹ : Ring A
inst✝ : Algebra ℚ A
⊢ constantCoeff (exp A) = 1

Tactic:
← coeff_zero_eq_constantCoeff_apply,

Goal state after:
A : Type u_1
inst✝¹ : Ring A
inst✝ : Algebra ℚ A
⊢ (coeff 0) (exp A) = 1
Module: Mathlib.NumberTheory.BernoulliPolynomials

Goal state before:
pp: ⊢ eval (1 / 4) (bernoulli 3) = 3 / 64

Tactic:
Polynomial.bernoulli,

Goal state after:
⊢ eval (1 / 4) (∑ i ∈ range (3 + 1), (monomial (3 - i)) (_root_.bernoulli i * ↑(Nat.choose 3 i))) = 3 / 64
Module: Mathlib.NumberTheory.PrimeCounting

Goal state before:
pp: ⊢ Function.Surjective π

Tactic:
suffices Function.Surjective (π ∘ fun n => n - 1) from this.of_comp

Goal state after:
⊢ Function.Surjective (π ∘ fun n ↦ n - 1)
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: n : ℕ
⊢ ↑(n.choose 0) / (↑n - ↑n + 1) * (1 - ∑ k ∈ range n, ↑(n.choose k) / (↑n - ↑k + 1) * bernoulli' k) +
      ∑ x ∈ range n, ↑(n.choose (n - x)) / (↑n - ↑x + 1) * bernoulli' x =
    1

Tactic:
choose_zero_right,

Goal state after:
n : ℕ
⊢ ↑1 / (↑n - ↑n + 1) * (1 - ∑ k ∈ range n, ↑(n.choose k) / (↑n - ↑k + 1) * bernoulli' k) +
      ∑ x ∈ range n, ↑(n.choose (n - x)) / (↑n - ↑x + 1) * bernoulli' x =
    1
Module: Mathlib.NumberTheory.BernoulliPolynomials

Goal state before:
pp: n d : ℕ
hd : ∀ m < d + 1, (bernoulli m).comp (1 + X) = bernoulli m + m • X ^ (m - 1)
x✝ : ℕ
a✝ : x✝ ∈ range (d + 1)
⊢ x✝ ∈ range (d + 1)

Tactic:
assumption

Goal state after:
Module: Mathlib.NumberTheory.BernoulliPolynomials

Goal state before:
pp: case succ
n i : ℕ
⊢ ((bernoulli (n + 1)).comp (-X)).coeff i = ((-1) ^ (n + 1) • (bernoulli (n + 1) + (n + 1) • X ^ (n + 1 - 1))).coeff i

Tactic:
rw [← neg_one_mul, ← C_1, ← C_neg, Polynomial.comp_C_mul_X_coeff, coeff_smul, coeff_add,
    coeff_smul, coeff_bernoulli, coeff_X_pow]

Goal state after:
case succ
n i : ℕ
⊢ (if i ≤ n + 1 then _root_.bernoulli (n + 1 - i) * ↑((n + 1).choose i) else 0) * (-1) ^ i =
    (-1) ^ (n + 1) •
      ((if i ≤ n + 1 then _root_.bernoulli (n + 1 - i) * ↑((n + 1).choose i) else 0) +
        (n + 1) • if i = n + 1 - 1 then 1 else 0)
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: n : ℕ
this : ∑ i ∈ range n, ↑((n + 2).choose (i + 2)) * bernoulli (i + 2) = ↑n / 2
⊢ ∑ k ∈ range (n + 1 + 1), ↑((n + 1 + 1).choose k) * bernoulli k = if n + 1 + 1 = 1 then 1 else 0

Tactic:
by
    simp only [this, sum_range_succ', cast_succ, bernoulli_one, bernoulli_zero, choose_one_right,
      mul_one, choose_zero_right, cast_zero, if_false, zero_add, succ_succ_ne_one]
    ring

Goal state after:
Module: Mathlib.NumberTheory.Bertrand

Goal state before:
pp: case refine_2
x : ℝ
x_large : 512 ≤ x
f : ℝ → ℝ := fun x ↦ log x + √(2 * x) * log (2 * x) - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ √(2 * x) / 4 ^ (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = log (x * (2 * x) ^ √(2 * x) / 4 ^ (x / 3))
h5 : 0 < x
h : ConcaveOn ℝ (Set.Ioi 0.5) f
this : √(2 * 512) = 32
⊢ 2 ^ 9 * 2 ^ (10 * 32) ≤ 4 ^ (512 / 3)

Tactic:
← pow_add

Goal state after:
case refine_2
x : ℝ
x_large : 512 ≤ x
f : ℝ → ℝ := fun x ↦ log x + √(2 * x) * log (2 * x) - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ √(2 * x) / 4 ^ (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = log (x * (2 * x) ^ √(2 * x) / 4 ^ (x / 3))
h5 : 0 < x
h : ConcaveOn ℝ (Set.Ioi 0.5) f
this : √(2 * 512) = 32
⊢ 2 ^ (9 + 10 * 32) ≤ 4 ^ (512 / 3)
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
⊢ ∑ p ∈ Ioc 0 ⌊x⌋₊ with Nat.Prime p, log ↑p = ∑ p ∈ Icc 0 ⌊x⌋₊ with Nat.Prime p, log ↑p

Tactic:
sum_filter,

Goal state after:
x : ℝ
⊢ (∑ a ∈ Ioc 0 ⌊x⌋₊, if Nat.Prime a then log ↑a else 0) = ∑ p ∈ Icc 0 ⌊x⌋₊ with Nat.Prime p, log ↑p
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
⊢ (∑ a ∈ Ioc 0 ⌊x⌋₊, if Nat.Prime a then log ↑a else 0) = ∑ p ∈ Icc 0 ⌊x⌋₊ with Nat.Prime p, log ↑p

Tactic:
sum_filter,

Goal state after:
x : ℝ
⊢ (∑ a ∈ Ioc 0 ⌊x⌋₊, if Nat.Prime a then log ↑a else 0) = ∑ a ∈ Icc 0 ⌊x⌋₊, if Nat.Prime a then log ↑a else 0
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: R : Type u_1
inst✝ : AddCommMonoid R
f : ℕ → R
x : ℝ
hx : 0 ≤ x
N : ℕ
hN : ⌊log x / log 2⌋₊ ≤ N
⊢ (∑ x ∈ Icc 1 N ×ˢ filter Nat.Prime (Ioc 0 ⌊x⌋₊) with
      match x with
      | (k, p) => p ≤ ⌊x ^ (↑k)⁻¹⌋₊,
      match x with
      | (k, p) => f (p ^ k)) =
    ∑ k ∈ Icc 1 N, ∑ p ∈ Ioc 0 ⌊x ^ (1 / ↑k)⌋₊ with Nat.Prime p, f (p ^ k)

Tactic:
sum_filter,

Goal state after:
R : Type u_1
inst✝ : AddCommMonoid R
f : ℕ → R
x : ℝ
hx : 0 ≤ x
N : ℕ
hN : ⌊log x / log 2⌋₊ ≤ N
⊢ (∑ a ∈ Icc 1 N ×ˢ filter Nat.Prime (Ioc 0 ⌊x⌋₊),
      if
          match a with
          | (k, p) => p ≤ ⌊x ^ (↑k)⁻¹⌋₊ then
        match a with
        | (k, p) => f (p ^ k)
      else 0) =
    ∑ k ∈ Icc 1 N, ∑ p ∈ Ioc 0 ⌊x ^ (1 / ↑k)⌋₊ with Nat.Prime p, f (p ^ k)
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
⊢ ∑ n ∈ Ioc 0 ⌊x⌋₊, Λ n - ∑ p ∈ Ioc 0 ⌊x⌋₊ with Nat.Prime p, log ↑p = ∑ n ∈ Ioc 0 ⌊x⌋₊ with ¬Nat.Prime n, Λ n

Tactic:
sum_filter,

Goal state after:
x : ℝ
⊢ (∑ n ∈ Ioc 0 ⌊x⌋₊, Λ n - ∑ a ∈ Ioc 0 ⌊x⌋₊, if Nat.Prime a then log ↑a else 0) =
    ∑ n ∈ Ioc 0 ⌊x⌋₊ with ¬Nat.Prime n, Λ n
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
⊢ (∑ n ∈ Ioc 0 ⌊x⌋₊, Λ n - ∑ a ∈ Ioc 0 ⌊x⌋₊, if Nat.Prime a then log ↑a else 0) =
    ∑ n ∈ Ioc 0 ⌊x⌋₊ with ¬Nat.Prime n, Λ n

Tactic:
sum_filter,

Goal state after:
x : ℝ
⊢ (∑ n ∈ Ioc 0 ⌊x⌋₊, Λ n - ∑ a ∈ Ioc 0 ⌊x⌋₊, if Nat.Prime a then log ↑a else 0) =
    ∑ a ∈ Ioc 0 ⌊x⌋₊, if ¬Nat.Prime a then Λ a else 0
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: case inl
x : ℝ
hx : 0 ≤ x
n m : ℕ
hnm : n ≤ m
hn : 1 ≤ n
hm : 1 ≤ m
h : x ≤ 1
⊢ θ (x ^ (↑m)⁻¹) ≤ θ (x ^ (↑n)⁻¹)

pp: case inr
x : ℝ
hx : 0 ≤ x
n m : ℕ
hnm : n ≤ m
hn : 1 ≤ n
hm : 1 ≤ m
h : 1 < x
⊢ θ (x ^ (↑m)⁻¹) ≤ θ (x ^ (↑n)⁻¹)

Tactic:
· repeat rw [theta_eq_zero_of_le_one (rpow_le_one hx h (by positivity))]

Goal state after:
case inr
x : ℝ
hx : 0 ≤ x
n m : ℕ
hnm : n ≤ m
hn : 1 ≤ n
hm : 1 ≤ m
h : 1 < x
⊢ θ (x ^ (↑m)⁻¹) ≤ θ (x ^ (↑n)⁻¹)
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: case h.right
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
r : ℚ
hr : ‖↑x - ↑r‖ < 1
H : ‖↑r‖ ≤ 1
n : ℕ
hnp : ↑n < ↑p
hn : ‖↑r - ↑↑↑n‖ < 1
⊢ max ‖↑x - ↑r‖ ‖↑r - ↑n‖ < 1

Tactic:
apply max_lt hr

Goal state after:
case h.right
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
r : ℚ
hr : ‖↑x - ↑r‖ < 1
H : ‖↑r‖ ≤ 1
n : ℕ
hnp : ↑n < ↑p
hn : ‖↑r - ↑↑↑n‖ < 1
⊢ ‖↑r - ↑n‖ < 1
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: a b : ℝ
hab : a ≤ b
one_lt : 1 < a
⊢ ∫ (x : ℝ) in a..b, 1 / log x ^ 2 ≤ (b - a) / log a ^ 2

Tactic:
calc
  _ ≤ ∫ x in a..b, 1 / log a ^ 2 := by
      refine intervalIntegral.integral_mono_on hab ?_ (by simp) fun x ⟨_, _⟩ ↦ by gcongr <;> bound
      apply intervalIntegrable_one_div_log_sq <;> linarith
  _ ≤ _ := by simp [field]

Goal state after:
Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter

Goal state before:
pp: L : Type u
inst✝² : CommRing L
inst✝¹ : IsDomain L
n : ℕ
inst✝ : NeZero n
g : L ≃+* L
c : ZMod (Nat.card ↥(rootsOfUnity n L))
ζ : ↥(rootsOfUnity n L)
hc : g ↑↑ζ = ↑(↑ζ ^ c.val)
⊢ ↑(↑ζ ^ c.val) = ↑(↑ζ ^ (χ₀ n g).val)

Tactic:
rw [← toFun_spec g ζ, hc]

Goal state after:
Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter

Goal state before:
pp: case pos
p : ℕ
inst✝³ : Fact (Nat.Prime p)
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
H : ∀ (i : ℕ), ∃ ζ, IsPrimitiveRoot ζ (p ^ i)
x✝ : ∀ (i : ℕ), HasEnoughRootsOfUnity L (p ^ i)
⊢ Continuous ⇑((cyclotomicCharacter L p).comp (MulSemiringAction.toRingAut Gal(L/K) L))

Tactic:
choose ζ hζ using H

Goal state after:
case pos
p : ℕ
inst✝³ : Fact (Nat.Prime p)
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x✝ : ∀ (i : ℕ), HasEnoughRootsOfUnity L (p ^ i)
ζ : ℕ → L
hζ : ∀ (i : ℕ), IsPrimitiveRoot (ζ i) (p ^ i)
⊢ Continuous ⇑((cyclotomicCharacter L p).comp (MulSemiringAction.toRingAut Gal(L/K) L))