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

Goal state before:
pp: α : Type u_1
inst✝⁸ : LinearOrder α
inst✝⁷ : DenselyOrdered α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : OrderTopology α
inst✝⁴ : SecondCountableTopology α
inst✝³ : CompactIccSpace α
hα : MeasurableSpace α
inst✝² : BorelSpace α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : CompleteSpace E
f : α → E
hf : BoundedVariationOn f univ
a : α
this : hf.vectorMeasure (Iic a) = Function.rightLim f a - atBot.limUnder f
⊢ hf.vectorMeasure (Iio a) = Function.leftLim f a - atBot.limUnder f

Tactic:
rw [← Iio_union_Icc_eq_Iic le_rfl, VectorMeasure.of_union (by simp) measurableSet_Iio
    measurableSet_Icc, hf.vectorMeasure_Icc le_rfl] at this

Goal state after:
α : Type u_1
inst✝⁸ : LinearOrder α
inst✝⁷ : DenselyOrdered α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : OrderTopology α
inst✝⁴ : SecondCountableTopology α
inst✝³ : CompactIccSpace α
hα : MeasurableSpace α
inst✝² : BorelSpace α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : CompleteSpace E
f : α → E
hf : BoundedVariationOn f univ
a : α
this :
  hf.vectorMeasure (Iio a) + (Function.rightLim f a - Function.leftLim f a) = Function.rightLim f a - atBot.limUnder f
⊢ hf.vectorMeasure (Iio a) = Function.leftLim f a - atBot.limUnder f
Module: Mathlib.MeasureTheory.VectorMeasure.Variation.Semivariation

Goal state before:
pp: X : Type u_1
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
mX : MeasurableSpace X
μ : VectorMeasure X E
s t : Set X
⊢ μ.semivariation (s ∪ t) ≤ μ.semivariation s + μ.semivariation t

Tactic:
simp only [semivariation, iSup_le_iff]
  intro ℓ hℓ
  apply (measure_union_le _ _).trans
  gcongr <;> apply le_biSup _ hℓ

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

Goal state before:
pp: M : Type u_1
N : Type u_2
F : Type u_5
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : FunLike F M N
inst✝ : AddMonoidHomClass F M N
f : F
S : Set (Set M)
hS : S.Finite
hS' : ∀ t ∈ S, IsLinearSet t
⊢ IsSemilinearSet (⇑f '' ⋃₀ S)

Tactic:
sUnion_eq_biUnion,

Goal state after:
M : Type u_1
N : Type u_2
F : Type u_5
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : FunLike F M N
inst✝ : AddMonoidHomClass F M N
f : F
S : Set (Set M)
hS : S.Finite
hS' : ∀ t ∈ S, IsLinearSet t
⊢ IsSemilinearSet (⇑f '' ⋃ i ∈ S, i)
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs

Goal state before:
pp: case mp.refine_2
S : Finset (Set ℕ)
k p : Set ℕ → ℕ
hS : ∀ t ∈ S, p t > 0
hS' : ∀ t ∈ S, ∀ x ≥ k t, x ∈ t ↔ x + p t ∈ t
x : ℕ
hx : x ≥ S.sup k
t : Set ℕ
ht : t ∈ S
m : ℕ
⊢ x ∈ t ↔ x + m * p t ∈ t

Tactic:
induction m with grind [Finset.sup_le_iff]

Goal state after:
Module: Mathlib.MeasureTheory.VectorMeasure.Integral

Goal state before:
pp: X : Type u_2
E : Type u_4
F : Type u_5
G : Type u_6
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace ℝ G
f : X → E
B : E →L[ℝ] F →L[ℝ] G
inst✝¹ : MeasurableSpace X
inst✝ : CompleteSpace G
a : X
v : F
hfm : StronglyMeasurable f
⊢ ∫ᵛ (x : X), f x ∂[B; dirac a v] = (B (f a)) v

Tactic:
by
  borelize E
  have : IsFiniteMeasure ((dirac a v).transpose B).variation := by
    have : ‖B.flip v‖ₑ • Measure.dirac a = ‖B.flip v‖₊ • Measure.dirac a := rfl
    simp only [transpose_dirac, variation_dirac, this]
    infer_instance
  calc
    ∫ᵛ x, f x ∂[B; VectorMeasure.dirac a v] = ∫ᵛ _, f a ∂[B; VectorMeasure.dirac a v] := by
      apply integral_congr_ae
      simp only [variation_dirac]
      exact Measure.ae_smul_measure (ae_eq_dirac' hfm.measurable) _
    _ = B (f a) v := by simp

Goal state after:
Module: Mathlib.MeasureTheory.VectorMeasure.Integral

Goal state before:
pp: X : Type u_2
E : Type u_4
F : Type u_5
G : Type u_6
mX : MeasurableSpace X
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace ℝ G
f : X → E
μ : VectorMeasure X F
B : E →L[ℝ] F →L[ℝ] G
inst✝¹ : Unique X
inst✝ : CompleteSpace G
⊢ ∫ᵛ (x : X), f x ∂[B; μ] = ∫ᵛ (x : X), f default ∂[B; μ]

Tactic:
by congr with x; congr; exact Unique.uniq _ x

Goal state after:
Module: Mathlib.MeasureTheory.VectorMeasure.Integral

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

Tactic:
by
  refine tendsto_integral_of_L1 f hfi hFi ?_
  simp_rw [eLpNorm_one_eq_lintegral_enorm, Pi.sub_apply] at hF
  exact hF

Goal state after:
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Definability

Goal state before:
pp: α : Type u_1
A : Set ℕ
inst✝ : Finite α
n : ℕ
φ : presburger[[↑A]].BoundedFormula α n
this : Fintype α
⊢ IsSemilinearSet {v | φ.Realize (v ∘ Sum.inl) (v ∘ Sum.inr)}

Tactic:
induction φ with simp only [BoundedFormula.Realize]
  | equal t₁ t₂ =>
    rcases term_realize_eq_add_dotProduct t₁ with ⟨k₁, u₁, ht₁⟩
    rcases term_realize_eq_add_dotProduct t₂ with ⟨k₂, u₂, ht₂⟩
    convert! Nat.isSemilinearSet_setOfPred_mulVec_eq ![k₁] ![k₂] (.of ![u₁]) (.of ![u₂])
    simp [ht₁, ht₂]
  | rel f => nomatch f
  | falsum => exact .empty
  | imp _ _ ih₁ ih₂ =>
    convert! (ih₂.compl.inter ih₁).compl using 1
    simp [ofPred_inter_eq_sep, imp_iff_not_or, compl_ofPred]
  | @all n φ ih =>
    let e := (Equiv.sumAssoc α (Fin n) (Fin 1)).trans (Equiv.sumCongr (.refl α) finSumFinEquiv)
    rw [← isSemilinearSet_image_iff (LinearEquiv.funCongrLeft ℕ ℕ e)] at ih
    convert! ih.compl.proj.compl using 1
    simp_rw [compl_ofPred, not_exists, Fin.forall_fin_succ_pi, Fin.forall_fin_zero_pi,
      mem_compl_iff, mem_image, not_not, ← LinearEquiv.eq_symm_apply, LinearEquiv.funCongrLeft_symm,
      exists_eq_right, mem_ofPred, LinearEquiv.funCongrLeft_apply, LinearMap.funLeft,
      LinearMap.coe_mk, AddHom.coe_mk]
    congr! 4
    ext i
    cases i using Fin.lastCases <;> simp [e]

Goal state after:
Module: Mathlib.ModelTheory.Equivalence

Goal state before:
pp: L : Language
T : L.Theory
α : Type w
n : ℕ
φ ψ θ : L.BoundedFormula α n
h₁ : φ ⟹[T] ψ
h₂ : φ ⟹[T] θ
M : T.ModelType
v : α → ↑M
xs : Fin n → ↑M
⊢ (φ ⟹ ψ ⊓ θ).Realize v xs

Tactic:
by
  simp only [BoundedFormula.realize_imp, BoundedFormula.realize_inf]
  exact fun h => ⟨h₁ M v xs h, h₂ M v xs h⟩

Goal state after:
Module: Mathlib.ModelTheory.Equivalence

Goal state before:
pp: L : Language
T : L.Theory
α : Type w
n : ℕ
φ ψ : L.BoundedFormula α n
h : φ ⇔[T] ψ
M : T.ModelType
v : α → ↑M
xs : Fin n → ↑M
⊢ ψ.Realize v xs ↔ φ.Realize v xs

Tactic:
Iff.comm,

Goal state after:
L : Language
T : L.Theory
α : Type w
n : ℕ
φ ψ : L.BoundedFormula α n
h : φ ⇔[T] ψ
M : T.ModelType
v : α → ↑M
xs : Fin n → ↑M
⊢ φ.Realize v xs ↔ ψ.Realize v xs
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: M : Type u_1
ι : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : Finite ι
F : Type u_5
inst✝¹ : FunLike F (ι → ℕ) M
inst✝ : AddMonoidHomClass F (ι → ℕ) M
f : F
S : Set (Set M)
hS : S.Finite
hS' : ∀ t ∈ S, IsLinearSet t
⊢ IsSemilinearSet (⇑f ⁻¹' ⋃₀ S)

Tactic:
sUnion_eq_biUnion,

Goal state after:
M : Type u_1
ι : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : Finite ι
F : Type u_5
inst✝¹ : FunLike F (ι → ℕ) M
inst✝ : AddMonoidHomClass F (ι → ℕ) M
f : F
S : Set (Set M)
hS : S.Finite
hS' : ∀ t ∈ S, IsLinearSet t
⊢ IsSemilinearSet (⇑f ⁻¹' ⋃ i ∈ S, i)
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: ι : Type u_3
inst✝ : Finite ι
s₁ s₂ : Set (ι → ℕ)
hs₁ : ∃ v n A, s₁ = {x | ∃ x_1, v + A *ᵥ x_1 = x}
hs₂ : ∃ v n A, s₂ = {x | ∃ x_1, v + A *ᵥ x_1 = x}
this : Fintype ι
⊢ IsSemilinearSet (s₁ ∩ s₂)

Tactic:
rcases hs₁ with ⟨u, n, A, rfl⟩

Goal state after:
ι : Type u_3
inst✝ : Finite ι
s₂ : Set (ι → ℕ)
hs₂ : ∃ v n A, s₂ = {x | ∃ x_1, v + A *ᵥ x_1 = x}
this : Fintype ι
u : ι → ℕ
n : ℕ
A : Matrix ι (Fin n) ℕ
⊢ IsSemilinearSet ({x | ∃ x_1, u + A *ᵥ x_1 = x} ∩ s₂)
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: ι : Type u_3
inst✝ : Finite ι
this : Fintype ι
u : ι → ℕ
n : ℕ
A : Matrix ι (Fin n) ℕ
v : ι → ℕ
m : ℕ
B : Matrix ι (Fin m) ℕ
⊢ IsSemilinearSet
    {x | u + A *ᵥ (x ∘ Sum.inl) ∘ Sum.inr = (x ∘ Sum.inl) ∘ Sum.inl ∧ v + B *ᵥ x ∘ Sum.inr = (x ∘ Sum.inl) ∘ Sum.inl}

Tactic:
convert!
    isSemilinearSet_setOfPred_mulVec_eq (κ := (ι ⊕ Fin n) ⊕ Fin m) (Sum.elim u v) 0
      (fromBlocks (fromCols 0 A) 0 0 B) (fromBlocks (fromCols 1 0) 0 (fromCols 1 0) 0)

Goal state after:
ι : Type u_3
inst✝ : Finite ι
this : Fintype ι
u : ι → ℕ
n : ℕ
A : Matrix ι (Fin n) ℕ
v : ι → ℕ
m : ℕ
B : Matrix ι (Fin m) ℕ
x✝ : (ι ⊕ Fin n) ⊕ Fin m → ℕ
⊢ u + A *ᵥ (x✝ ∘ Sum.inl) ∘ Sum.inr = (x✝ ∘ Sum.inl) ∘ Sum.inl ∧ v + B *ᵥ x✝ ∘ Sum.inr = (x✝ ∘ Sum.inl) ∘ Sum.inl ↔
    Sum.elim u v + fromBlocks (fromCols 0 A) 0 0 B *ᵥ x✝ = 0 + fromBlocks (fromCols 1 0) 0 (fromCols 1 0) 0 *ᵥ x✝
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: 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 : AddMonoidHom.mrange f = ⊤
⊢ IsSemilinearSet (s₁' ∩ s₂')

Tactic:
rw [AddMonoidHom.mrange_eq_top] at hf

Goal state after:
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₁' ∩ s₂')
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: ι : Type u_3
s : Set (ι → ℕ)
hs : LinearIndepOn ℕ id s
t : Finset (ι → ℕ)
f : (ι → ℕ) → ℤ
ht : ↑t ⊆ s
hf : ∀ i ∉ t, f i = 0
heq : ∑ i ∈ t, f i • toRatVec i = 0
i : ι → ℕ
hi : i ∈ t
⊢ f i = 0

Tactic:
linearIndepOn_iff_linearIndepOn_finset

Goal state after:
ι : Type u_3
s : Set (ι → ℕ)
hs : ∀ (t : Finset (ι → ℕ)), ↑t ⊆ s → LinearIndepOn ℕ id ↑t
t : Finset (ι → ℕ)
f : (ι → ℕ) → ℤ
ht : ↑t ⊆ s
hf : ∀ i ∉ t, f i = 0
heq : ∑ i ∈ t, f i • toRatVec i = 0
i : ι → ℕ
hi : i ∈ t
⊢ f i = 0
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 : ℕ
F : L.Functions n
i : ι
x : Fin n → G i
⊢ (funMap F fun a ↦ ⟦Structure.Sigma.mk f i (x a)⟧) = ⟦Structure.Sigma.mk f i (funMap F x)⟧

Tactic:
simp only [funMap_quotient_mk', Quotient.eq]
  obtain ⟨k, ik, jk⟩ :=
    directed_of (· ≤ ·) i (Classical.choose (Finite.bddAbove_range fun _ : Fin n => i))
  refine ⟨k, jk, ik, ?_⟩
  simp only [Embedding.map_fun, comp_unify]
  rfl

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 : ℕ
F : L.Functions n
i : ι
x : Fin n → G i
⊢ (funMap F fun a ↦ ⟦Structure.Sigma.mk f i (x a)⟧) = ⟦Structure.Sigma.mk f i (funMap F x)⟧

Tactic:
by
  simp only [funMap_quotient_mk', Quotient.eq]
  obtain ⟨k, ik, jk⟩ :=
    directed_of (· ≤ ·) i (Classical.choose (Finite.bddAbove_range fun _ : Fin n => i))
  refine ⟨k, jk, ik, ?_⟩
  simp only [Embedding.map_fun, comp_unify]
  rfl

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

Goal state before:
pp: ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
⊢ x + ∑ i, (-hs.floor x i).toNat • ↑i = hs.fract x + ∑ i, (hs.floor x i).toNat • ↑i

Tactic:
simp only [fract]
  rw [tsub_add_cancel_of_le (hs.floor_toNat_sum_le x)]

Goal state after:
Module: Mathlib.MeasureTheory.VectorMeasure.WithDensityVec

Goal state before:
pp: case hm
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‖ₑ + ρ)
I3 :
  ∑ i ∈ g.range, ‖i‖ₑ * ((μ.transpose B).restrict s).variation (⇑g ⁻¹' {i}) ≤
    ∑ i ∈ g.range.sigma P, ‖i.fst‖ₑ * ‖((μ.transpose B).restrict s) i.snd‖ₑ + ↑δ
⊢ ∀ b ∈ g.range.sigma P, MeasurableSet b.snd

Tactic:
· rintro ⟨i, p⟩ hip
        simp only [Finset.mem_sigma, SimpleFunc.mem_range, mem_range] at hip
        exact Pmeas i p hip.2

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

Goal state before:
pp: ι : Type u_3
inst✝ : Finite ι
S : Set (Set (ι → ℕ))
hS : S.Finite
hS' : ∀ t ∈ S, IsProperLinearSet t
hs : IsSemilinearSet (⋃₀ S)
⊢ IsSemilinearSet (⋃₀ S)ᶜ

Tactic:
sUnion_eq_biUnion,

Goal state after:
ι : Type u_3
inst✝ : Finite ι
S : Set (Set (ι → ℕ))
hS : S.Finite
hS' : ∀ t ∈ S, IsProperLinearSet t
hs : IsSemilinearSet (⋃₀ S)
⊢ IsSemilinearSet (⋃ i ∈ S, i)ᶜ
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: 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 : AddMonoidHom.mrange f = ⊤
⊢ IsSemilinearSet (s₁' \ s₂')

Tactic:
rw [AddMonoidHom.mrange_eq_top] at hf

Goal state after:
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₁' \ s₂')
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: M : Type u_1
inst✝¹ : AddCommMonoid M
s : Set M
inst✝ : AddMonoid.FG M
hs : IsSemilinearSet s
⊢ IsSemilinearSet sᶜ

Tactic:
rw [compl_eq_univ_sdiff]
  exact sdiff .univ hs

Goal state after:
Module: Mathlib.ModelTheory.Topology.Types

Goal state before:
pp: case refine_2
L : Language
T : L.Theory
α : Type u_1
F : Ultrafilter (T.CompleteType α)
a✝ : ↑F ≤ Filter.principal univ
⊢ IsMaximal {φ | T.typesWith φ ∈ F}

pp: case refine_3
L : Language
T : L.Theory
α : Type u_1
F : Ultrafilter (T.CompleteType α)
a✝ : ↑F ≤ Filter.principal univ
⊢ { toTheory := {φ | T.typesWith φ ∈ F}, subset' := ⋯, isMaximal' := ?refine_2 } ∈ univ ∧
    ↑F ≤ nhds { toTheory := {φ | T.typesWith φ ∈ F}, subset' := ⋯, isMaximal' := ?refine_2 }

Tactic:
· rw [Theory.IsMaximal, Theory.isSatisfiable_iff_isFinitelySatisfiable]
    refine ⟨?_, ?_⟩
    · rw[Theory.IsFinitelySatisfiable]
      intro x hx
      have : ∀ φ ∈ x, T.typesWith φ ∈ F.toFilter := by intro φ hφ; exact hx hφ
      rw [← Filter.biInter_finset_mem x] at this
      obtain ⟨T, T_inter⟩ := F.neBot.nonempty_of_mem this
      have subset : (x : Set _) ⊆ T.toTheory := by rwa [Set.mem_iInter₂] at T_inter
      exact T.isMaximal.1.mono subset
    · intro φ
      simp only [mem_ofPred_eq, typesWith_not]
      exact Ultrafilter.mem_or_compl_mem F (T.typesWith φ)

Goal state after:
case refine_3
L : Language
T : L.Theory
α : Type u_1
F : Ultrafilter (T.CompleteType α)
a✝ : ↑F ≤ Filter.principal univ
⊢ { toTheory := {φ | T.typesWith φ ∈ F}, subset' := ⋯, isMaximal' := ⋯ } ∈ univ ∧
    ↑F ≤ nhds { toTheory := {φ | T.typesWith φ ∈ F}, subset' := ⋯, isMaximal' := ⋯ }
Module: Mathlib.NumberTheory.AlmostPrime

Goal state before:
pp: case mpr
n : ℕ
⊢ Prime n → IsAlmostPrime 1 n

Tactic:
exact fun h ↦ ⟨h.ne_zero, ArithmeticFunction.cardFactors_eq_one_iff_prime.mpr h⟩

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
u v : R
p : ℕ
hp : Nat.Prime p
hvu : v ∣ u
hpuv : ↑p * u * v ∣ u ^ p
x : R
⊢ ∃ y,
    1 +
        ((u * x) ^ 1 * ↑(p.choose 1) +
          ∑ x_1 ∈ ((Finset.range (p + 1)).erase 0).erase 1, (u * x) ^ x_1 * ↑(p.choose x_1)) =
      1 + ↑p * u * (x + v * y)

Tactic:
← Finset.sum_erase_add (a := p) _ _ (by -- aesop works but is slow
      simp only [Finset.mem_erase]
      rw [← and_assoc, and_comm (a := ¬ _), ← Nat.two_le_iff]
      simp [hp.two_le])

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
u v : R
p : ℕ
hp : Nat.Prime p
hvu : v ∣ u
hpuv : ↑p * u * v ∣ u ^ p
x : R
⊢ ∃ y,
    1 +
        ((u * x) ^ 1 * ↑(p.choose 1) +
          (∑ x_1 ∈ (((Finset.range (p + 1)).erase 0).erase 1).erase p, (u * x) ^ x_1 * ↑(p.choose x_1) +
            (u * x) ^ p * ↑(p.choose p))) =
      1 + ↑p * u * (x + v * y)
Module: Mathlib.NumberTheory.AbelSummation

Goal state before:
pp: case inr
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
a b : ℝ
ha : 0 ≤ a
hab : a ≤ b
hf_diff : ∀ t ∈ Set.Icc a b, DifferentiableAt ℝ f t
hf_int : IntegrableOn (deriv f) (Set.Icc a b) volume
aux1 : ↑⌊a⌋₊ ≤ a
aux2 : b ≤ ↑⌊b⌋₊ + 1
hb : ⌊a⌋₊ < ⌊b⌋₊
aux3 : a ≤ ↑⌊a⌋₊ + 1
aux4 : ↑⌊a⌋₊ + 1 ≤ b
aux5 : ↑⌊b⌋₊ ≤ b
aux6 : a ≤ ↑⌊b⌋₊
⊢ ∑ k ∈ Ioc ⌊a⌋₊ ⌊b⌋₊, f ↑k * c k =
    f b * ∑ k ∈ Icc 0 ⌊b⌋₊, c k - f a * ∑ k ∈ Icc 0 ⌊a⌋₊, c k - ∫ (x : ℝ) in a..b, deriv f x * ∑ k ∈ Icc 0 ⌊x⌋₊, c k

Tactic:
← smul_eq_mul,

Goal state after:
case inr
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
a b : ℝ
ha : 0 ≤ a
hab : a ≤ b
hf_diff : ∀ t ∈ Set.Icc a b, DifferentiableAt ℝ f t
hf_int : IntegrableOn (deriv f) (Set.Icc a b) volume
aux1 : ↑⌊a⌋₊ ≤ a
aux2 : b ≤ ↑⌊b⌋₊ + 1
hb : ⌊a⌋₊ < ⌊b⌋₊
aux3 : a ≤ ↑⌊a⌋₊ + 1
aux4 : ↑⌊a⌋₊ + 1 ≤ b
aux5 : ↑⌊b⌋₊ ≤ b
aux6 : a ≤ ↑⌊b⌋₊
⊢ ∑ x ∈ Ioc ⌊a⌋₊ ⌊b⌋₊, f ↑x • c x =
    f b • ∑ k ∈ Icc 0 ⌊b⌋₊, c k - f a • ∑ k ∈ Icc 0 ⌊a⌋₊, c k - ∫ (x : ℝ) in a..b, deriv f x • ∑ k ∈ Icc 0 ⌊x⌋₊, c k
Module: Mathlib.RingTheory.ZMod.UnitsCyclic

Goal state before:
pp: case neg.inr.inl
n : ℕ
h0 : ¬2 * n = 0
h1 : ¬2 * n = 1
h2 : ¬2 * n = 2
h4 : ¬2 * n = 4
hn✝ : Even (2 * n)
hn : Odd n
⊢ IsCyclic (ZMod (2 * n))ˣ ↔
    (∃ x x_1, Nat.Prime x ∧ Odd x ∧ 1 ≤ x_1 ∧ 2 * n = x ^ x_1) ∨
      ∃ x x_1, Nat.Prime x ∧ Odd x ∧ 1 ≤ x_1 ∧ 2 * n = 2 * x ^ x_1

Tactic:
rw [isCyclic_units_two_mul_iff_of_odd _ hn, isCyclic_units_iff_of_odd hn, or_iff_right]

Goal state after:
case neg.inr.inl
n : ℕ
h0 : ¬2 * n = 0
h1 : ¬2 * n = 1
h2 : ¬2 * n = 2
h4 : ¬2 * n = 4
hn✝ : Even (2 * n)
hn : Odd n
⊢ (∃ p m, Nat.Prime p ∧ Odd p ∧ n = p ^ m) ↔ ∃ x x_1, Nat.Prime x ∧ Odd x ∧ 1 ≤ x_1 ∧ 2 * n = 2 * x ^ x_1

case neg.inr.inl
n : ℕ
h0 : ¬2 * n = 0
h1 : ¬2 * n = 1
h2 : ¬2 * n = 2
h4 : ¬2 * n = 4
hn✝ : Even (2 * n)
hn : Odd n
⊢ ¬∃ x x_1, Nat.Prime x ∧ Odd x ∧ 1 ≤ x_1 ∧ 2 * n = x ^ x_1
Module: Mathlib.NumberTheory.PrimeCounting

Goal state before:
pp: n : ℕ
⊢ #({p ∈ range n | Prime p}) = count Prime n

Tactic:
exact (count_eq_card_filter_range Prime n).symm

Goal state after:
Module: Mathlib.NumberTheory.BernoulliPolynomials

Goal state before:
pp: case a
n x✝¹ : ℕ
a✝¹ : x✝¹ ∈ range (n + 1 - 0)
x✝ : ℕ
a✝ : x✝ ∈ range (n + 1 - x✝¹)
| (monomial x✝¹) (↑((n + 1 - x✝¹).choose x✝) * _root_.bernoulli x✝ * ↑((n + 1).choose x✝¹))

Tactic:
← smul_eq_mul,

Goal state after:
case a
n x✝¹ : ℕ
a✝¹ : x✝¹ ∈ range (n + 1 - 0)
x✝ : ℕ
a✝ : x✝ ∈ range (n + 1 - x✝¹)
| (monomial x✝¹) ((↑((n + 1 - x✝¹).choose x✝) * _root_.bernoulli x✝) • ↑((n + 1).choose x✝¹))
Module: Mathlib.NumberTheory.Primorial

Goal state before:
pp: n : ℕ
⊢ n#.primeFactors = n.primesLE

Tactic:
rw [primorial_eq_prod_primesLE]

Goal state after:
n : ℕ
⊢ (∏ p ∈ n.primesLE, p).primeFactors = n.primesLE
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: case inr
n : ℕ
hn : n ≠ 1
hgt : 1 < n
x✝ : Even n ∨ Odd n
⊢ bernoulli n = bernoulli' n

Tactic:
cases n.even_or_odd with

Goal state after:
Module: Mathlib.NumberTheory.Primorial

Goal state before:
pp: n : ℕ
⊢ Squarefree (n#)

Tactic:
rw [primorial_eq_prod_primesLE]

Goal state after:
n : ℕ
⊢ Squarefree (∏ p ∈ n.primesLE, p)
Module: Mathlib.NumberTheory.Bertrand

Goal state before:
pp: n : ℕ
n_large : 2 < n
no_prime : ∀ (p : ℕ), Nat.Prime p → n < p → 2 * n < p
n_pos : 0 < n
n2_pos : 1 ≤ 2 * n
S : Finset ℕ := {p ∈ Finset.range (2 * n / 3 + 1) | Nat.Prime p}
f : ℕ → ℕ := fun x ↦ x ^ n.centralBinom.factorization x
this : ∏ x ∈ S, f x = ∏ x ∈ Finset.range (2 * n / 3 + 1), f x
⊢ ∏ x ∈ S, f x ≤ (2 * n) ^ (2 * n).sqrt * 4 ^ (2 * n / 3)

Tactic:
←
    Finset.prod_filter_mul_prod_filter_not S (· ≤ sqrt (2 * n))

Goal state after:
n : ℕ
n_large : 2 < n
no_prime : ∀ (p : ℕ), Nat.Prime p → n < p → 2 * n < p
n_pos : 0 < n
n2_pos : 1 ≤ 2 * n
S : Finset ℕ := {p ∈ Finset.range (2 * n / 3 + 1) | Nat.Prime p}
f : ℕ → ℕ := fun x ↦ x ^ n.centralBinom.factorization x
this : ∏ x ∈ S, f x = ∏ x ∈ Finset.range (2 * n / 3 + 1), f x
⊢ (∏ x ∈ S with x ≤ (2 * n).sqrt, f x) * ∏ x ∈ S with ¬x ≤ (2 * n).sqrt, f x ≤ (2 * n) ^ (2 * n).sqrt * 4 ^ (2 * n / 3)
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: n p : ℕ
f : ℕ → ℚ := fun i ↦ bernoulli i * ↑(p.succ.succ.choose i) * ↑n ^ (p.succ.succ - i) / ↑p.succ.succ
f' : ℕ → ℚ := fun i ↦ bernoulli' i * ↑(p.succ.succ.choose i) * ↑n ^ (p.succ.succ - i) / ↑p.succ.succ
hle : 1 ≤ n + 1
hne : ↑p + 1 + 1 ≠ 0
r : ℚ
⊢ r * (↑p + 1 + 1) * ↑n ^ p.succ / (↑p + 1 + 1) = r * ↑n ^ p.succ

Tactic:
rw [mul_div_right_comm, mul_div_cancel_right₀ _ hne]

Goal state after:
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: k m p : ℕ
hm_lt : m < k
inst✝ : Fact (Nat.Prime p)
ih : pIntegral p (bernoulli (2 * m) + vonStaudtIndicator (2 * m) p / ↑p)
hp_ne : ↑p ≠ 0
P : ℚ := ↑p ^ (2 * k - 2 * m - 1)
hpow : ↑p ^ (2 * k - 2 * m) = P * ↑p
hdecomp :
  bernoulli (2 * m) * ↑((2 * k + 1).choose (2 * m)) * ↑p ^ (2 * k - 2 * m) / (2 * ↑k + 1) =
    (bernoulli (2 * m) + vonStaudtIndicator (2 * m) p / ↑p) * ↑((2 * k + 1).choose (2 * m)) * ↑p ^ (2 * k - 2 * m) /
        (2 * ↑k + 1) -
      vonStaudtIndicator (2 * m) p * ↑((2 * k + 1).choose (2 * m)) * P / (2 * ↑k + 1)
⊢ pIntegral p (bernoulli (2 * m) * ↑((2 * k + 1).choose (2 * m)) * ↑p ^ (2 * k - 2 * m) / (2 * ↑k + 1))

Tactic:
rw [hdecomp]

Goal state after:
k m p : ℕ
hm_lt : m < k
inst✝ : Fact (Nat.Prime p)
ih : pIntegral p (bernoulli (2 * m) + vonStaudtIndicator (2 * m) p / ↑p)
hp_ne : ↑p ≠ 0
P : ℚ := ↑p ^ (2 * k - 2 * m - 1)
hpow : ↑p ^ (2 * k - 2 * m) = P * ↑p
hdecomp :
  bernoulli (2 * m) * ↑((2 * k + 1).choose (2 * m)) * ↑p ^ (2 * k - 2 * m) / (2 * ↑k + 1) =
    (bernoulli (2 * m) + vonStaudtIndicator (2 * m) p / ↑p) * ↑((2 * k + 1).choose (2 * m)) * ↑p ^ (2 * k - 2 * m) /
        (2 * ↑k + 1) -
      vonStaudtIndicator (2 * m) p * ↑((2 * k + 1).choose (2 * m)) * P / (2 * ↑k + 1)
⊢ pIntegral p
    ((bernoulli (2 * m) + vonStaudtIndicator (2 * m) p / ↑p) * ↑((2 * k + 1).choose (2 * m)) * ↑p ^ (2 * k - 2 * m) /
        (2 * ↑k + 1) -
      vonStaudtIndicator (2 * m) p * ↑((2 * k + 1).choose (2 * m)) * P / (2 * ↑k + 1))