mathlib-initiative/mathlib-tactics huggingface dataset:
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
x✝² : Encodable ↑X
x✝¹ : Countable ↑Y
x✝ : Encodable ↑Y
D : ↑X ⊕ ↑Y → Order.Cofinal (L.FGEquiv M N) :=
  fun p ↦ Sum.recOn p (fun x ↦ ext_dom.definedAtLeft ↑x) fun y ↦ ext_cod.definedAtRight ↑y
S : ℕ →o M ≃ₚ[L] N := { toFun := Subtype.val ∘ Order.sequenceOfCofinals g D, monotone' := ⋯ }
F : M ≃ₚ[L] N := partialEquivLimit S
x : M
hx : x ∈ X
⊢ x ∈ ↑F.dom

Tactic:
have := Order.sequenceOfCofinals.encode_mem g D (Sum.inl ⟨x, hx⟩)

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
x✝¹ : Countable ↑Y
x✝ : Encodable ↑Y
D : ↑X ⊕ ↑Y → Order.Cofinal (L.FGEquiv M N) :=
  fun p ↦ Sum.recOn p (fun x ↦ ext_dom.definedAtLeft ↑x) fun y ↦ ext_cod.definedAtRight ↑y
S : ℕ →o M ≃ₚ[L] N := { toFun := Subtype.val ∘ Order.sequenceOfCofinals g D, monotone' := ⋯ }
F : M ≃ₚ[L] N := partialEquivLimit S
x : M
hx : x ∈ X
this : Order.sequenceOfCofinals g D (Encodable.encode (Sum.inl ⟨x, hx⟩) + 1) ∈ D (Sum.inl ⟨x, hx⟩)
⊢ x ∈ ↑F.dom
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: case mpr
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x u : ι → ℕ
hu : u ∈ hs.fundamentalDomain
hu' : u ∉ {hs.base}
y : ι → ℕ
hy : y ∈ closure hs.basisSet
y' : ι → ℕ
hy' : y' ∈ closure hs.basisSet
heq : hs.fract x = hs.fract (u + y)
⊢ hs.fract x ≠ hs.base

Tactic:
hs.fract_add_of_mem_closure hy,

Goal state after:
case mpr
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x u : ι → ℕ
hu : u ∈ hs.fundamentalDomain
hu' : u ∉ {hs.base}
y : ι → ℕ
hy : y ∈ closure hs.basisSet
y' : ι → ℕ
hy' : y' ∈ closure hs.basisSet
heq : hs.fract x = hs.fract u
⊢ hs.fract x ≠ hs.base
Module: Mathlib.Order.CountableDenseLinearOrder

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : LinearOrder β
inst✝³ : DenselyOrdered β
inst✝² : NoMinOrder β
inst✝¹ : NoMaxOrder β
inst✝ : Nonempty β
f : PartialIso α β
a : α
h : ¬∃ b, (a, b) ∈ ↑f
y : β
hy : ∃ a_1 ∈ {p ∈ ↑f | a < p.1}, a_1.2 = y
p : α × β
hp1 : p ∈ {p ∈ ↑f | p.1 < a}
⊢ p.2 < y

Tactic:
rcases hy with ⟨q, hq1, rfl⟩

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : LinearOrder β
inst✝³ : DenselyOrdered β
inst✝² : NoMinOrder β
inst✝¹ : NoMaxOrder β
inst✝ : Nonempty β
f : PartialIso α β
a : α
h : ¬∃ b, (a, b) ∈ ↑f
p : α × β
hp1 : p ∈ {p ∈ ↑f | p.1 < a}
q : α × β
hq1 : q ∈ {p ∈ ↑f | a < p.1}
⊢ p.2 < q.2
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‖ₑ + ρ)
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‖ₑ + ↑δ
⊢ ∫⁻ (x : X) in ⋃ i ∈ g.range.sigma P, i.snd, ‖g x - f x‖ₑ ∂(μ.transpose B).variation +
      ∑ i ∈ g.range.sigma P, ‖∫ᵛ (x : X) in i.snd, f x ∂[B; μ.restrict s]‖ₑ ≤
    ∑ i ∈ g.range.sigma P, ‖∫ᵛ (x : X) in i.snd, f x ∂[B; μ.restrict s]‖ₑ +
      ∫⁻ (x : X), ‖g x - f x‖ₑ ∂(μ.transpose B).variation

Tactic:
by
      rw [add_comm]
      gcongr
      apply Measure.restrict_le_self

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

Goal state before:
pp: case mp.refine_4
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
hx : hs.fract x = hs.base
i : ↑hs.basisSet
hi : hs.floor x i < 0
⊢ x + ↑i + ((-hs.floor x i).toNat - 1) • ↑i + ∑ j ∈ Finset.univ.erase i, (-hs.floor x j).toNat • ↑j =
    hs.base + ∑ j ∈ Finset.univ.erase i, (hs.floor x j).toNat • ↑j

Tactic:
· rw [add_assoc x, ← succ_nsmul',
          tsub_add_cancel_of_le
            ((Int.le_toNat (neg_pos.2 hi).le).2 (le_neg.1 (Int.cast_le_neg_one_of_neg hi))),
          add_assoc x,
          Finset.add_sum_erase _ (fun j => (-hs.floor x j).toNat • j.1) (Finset.mem_univ i),
          ← add_zero (Finset.sum (Finset.univ.erase i) _),
          ← zero_nsmul i.1, ← Int.toNat_eq_zero.2 hi.le,
          Finset.sum_erase_add _ _ (Finset.mem_univ i), ← hx]
        exact hs.add_floor_neg_toNat_sum_eq x

Goal state after:
Module: Mathlib.ModelTheory.Order

Goal state before:
pp: L : Language
α : Type w
M : Type w'
n : ℕ
inst✝⁵ : L.IsOrdered
inst✝⁴ : L.Structure M
inst✝³ : LE M
inst✝² : Language.order.Structure M
inst✝¹ : Language.order.OrderedStructure M
inst✝ : L.orderLHom.IsExpansionOn M
x : Fin 2 → M
⊢ RelMap (L.orderLHom.onRelation leSymb) x ↔ x 0 ≤ x 1

Tactic:
LHom.IsExpansionOn.map_onRelation,

Goal state after:
L : Language
α : Type w
M : Type w'
n : ℕ
inst✝⁵ : L.IsOrdered
inst✝⁴ : L.Structure M
inst✝³ : LE M
inst✝² : Language.order.Structure M
inst✝¹ : Language.order.OrderedStructure M
inst✝ : L.orderLHom.IsExpansionOn M
x : Fin 2 → M
⊢ RelMap leSymb x ↔ x 0 ≤ x 1
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 : ↑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

Tactic:
refine ⟨?_, i, hi, ?_⟩

Goal state after:
case mpr.refine_1
ι : 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

case mpr.refine_2
ι : 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
⊢ 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 ι
⊢ hs.setOfFloorPos =
    ⋃ i ∈ {i | ↑i ∉ hs.periods},
      {x |
        ∃ y ∈ closure {↑i},
          ∃ z ∈ closure (hs.basisSet \ {↑i}), ∃ z' ∈ closure (hs.basisSet \ {↑i}), x + z' = hs.base + ↑i + y + z}

Tactic:
ext x
    simp only [setOfFloorPos, mem_iUnion, mem_ofPred_eq, exists_prop]
    constructor
    · intro ⟨hx, i, hi, hi'⟩
      refine ⟨i, hi, ((hs.floor x i).toNat - 1) • i.1, ?_,
          ∑ j ∈ Finset.univ.erase i, (hs.floor x j).toNat • j.1, ?_,
          ∑ j ∈ Finset.univ.erase i, (- hs.floor x j).toNat • j.1, ?_, ?_⟩
      · exact nsmul_mem (mem_closure_of_mem (mem_singleton i.1)) _
      · refine sum_mem fun j hj => nsmul_mem (mem_closure_of_mem ?_) _
        simpa [Subtype.val_inj] using hj
      · refine sum_mem fun j hj => nsmul_mem (mem_closure_of_mem ?_) _
        simpa [Subtype.val_inj] using hj
      · rw [add_assoc hs.base, ← succ_nsmul',
          tsub_add_cancel_of_le ((Int.le_toNat hi'.le).2 (Int.add_one_le_of_lt hi')),
          add_assoc hs.base,
          Finset.add_sum_erase _ (fun j => (hs.floor x j).toNat • j.1) (Finset.mem_univ i),
          ← add_zero (Finset.sum (Finset.univ.erase i) _),
          ← zero_nsmul i.1, ← Int.toNat_eq_zero.2 (neg_neg_iff_pos.2 hi').le,
          Finset.sum_erase_add _ _ (Finset.mem_univ i), ← hx]
        exact hs.add_floor_neg_toNat_sum_eq x
    · intro ⟨i, hi, y, hy, z, hz, z', hz', heq⟩
      refine ⟨?_, i, hi, ?_⟩
      · apply congr_arg hs.fract at heq
        rwa [hs.fract_add_of_mem_closure (closure_mono sdiff_subset hz'),
          hs.fract_add_of_mem_closure (closure_mono sdiff_subset hz),
          hs.fract_add_of_mem_closure (closure_mono (singleton_subset_iff.2 i.2) hy),
          hs.fract_add_of_mem_closure (mem_closure_of_mem i.2), hs.fract_base] at heq
      · rw [mem_closure_singleton] at hy
        rcases hy with ⟨n, rfl⟩
        apply congr_arg (hs.floor · i) at heq
        rw [hs.floor_add_of_mem_closure sdiff_subset (notMem_sdiff_of_mem (mem_singleton i.1)) hz,
          hs.floor_add_of_mem_closure sdiff_subset (notMem_sdiff_of_mem (mem_singleton i.1)) hz',
          add_assoc hs.base, ← succ_nsmul', hs.floor_add_nsmul_self, hs.floor_base, zero_add] at heq
        simp [heq]

Goal state after:
Module: Mathlib.ModelTheory.Types

Goal state before:
pp: L : Language
T : L.Theory
α : Type w
S : L[[α]].Theory
⊢ ((L.lhomWithConstants α).onTheory T ∪ S).IsSatisfiable ↔ ¬{p | S ⊆ ↑p} = ∅

Tactic:
← not_nonempty_iff_eq_empty,

Goal state after:
L : Language
T : L.Theory
α : Type w
S : L[[α]].Theory
⊢ ((L.lhomWithConstants α).onTheory T ∪ S).IsSatisfiable ↔ ¬¬{p | S ⊆ ↑p}.Nonempty
Module: Mathlib.ModelTheory.Topology.Types

Goal state before:
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' := ⋯ } ∈ univ ∧
    ↑F ≤ nhds { toTheory := {φ | T.typesWith φ ∈ F}, subset' := ⋯, isMaximal' := ⋯ }

Tactic:
refine ⟨mem_univ _, ?_⟩

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

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
a b : X
inst✝¹ : LinearOrder X
inst✝ : ClosedIciTopology X
⊢ IsLocallyClosed (Set.Ico a b)

Tactic:
← Set.Iio_inter_Ici

Goal state after:
X : Type u_1
inst✝² : TopologicalSpace X
a b : X
inst✝¹ : LinearOrder X
inst✝ : ClosedIciTopology X
⊢ IsLocallyClosed (Set.Iio b ∩ Set.Ici a)
Module: Mathlib.NumberTheory.AlmostPrime

Goal state before:
pp: p : ℕ
hp : Prime p
⊢ IsAlmostPrime 1 p

Tactic:
simpa using isAlmostPrime_one_iff.mpr hp

Goal state after:
Module: Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt

Goal state before:
pp: n : ℕ
⊢ ∑ i ∈ n.divisors, Λ i = Real.log ↑n

Tactic:
refine recOnPrimeCoprime ?_ ?_ ?_ n
  · simp
  · intro p k hp
    rw [sum_divisors_prime_pow hp, cast_pow, Real.log_pow, Finset.sum_range_succ', Nat.pow_zero,
      vonMangoldt_apply_one]
    simp [vonMangoldt_apply_pow (Nat.succ_ne_zero _), vonMangoldt_apply_prime hp]
  intro a b ha' hb' hab ha hb
  simp only [vonMangoldt_apply, ← sum_filter] at ha hb ⊢
  rw [mul_divisors_filter_prime_pow hab, filter_union,
    sum_union (disjoint_divisors_filter_isPrimePow hab), ha, hb, Nat.cast_mul,
    Real.log_mul (cast_ne_zero.2 (pos_of_gt ha').ne') (cast_ne_zero.2 (pos_of_gt hb').ne')]

Goal state after:
Module: Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt

Goal state before:
pp: n m : ℕ
mn : m ∣ n
⊢ ¬n = 0 → ↑(μ m) * -Real.log ↑(n / m) = ↑(μ m) * Real.log ↑m - ↑(μ m) * Real.log ↑n

Tactic:
hn

Goal state after:
n m : ℕ
mn : m ∣ n
hn : ¬n = 0
⊢ ↑(μ m) * -Real.log ↑(n / m) = ↑(μ m) * Real.log ↑m - ↑(μ m) * Real.log ↑n
Module: Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt

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

Tactic:
have : (∑ i ∈ n.divisors, (μ i : ℝ) * -Real.log (n / i : ℕ)) =
      ∑ i ∈ n.divisors, ((μ i : ℝ) * Real.log i - μ i * Real.log n) := by
    apply sum_congr rfl
    simp only [and_imp, Ne, mem_divisors]
    intro m mn hn
    have : (m : ℝ) ≠ 0 := by
      rw [cast_ne_zero]
      rintro rfl
      exact hn (by simpa using mn)
    rw [Nat.cast_div mn this, Real.log_div (cast_ne_zero.2 hn) this, neg_sub, mul_sub]

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 = ∑ i ∈ n.divisors, ↑(μ i) * -Real.log ↑(n / i)
Module: Mathlib.RingTheory.MvPowerSeries.Derivative

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
i : σ
f g : MvPowerSeries σ R
n : σ →₀ ℕ
h₁ : n < n + single i 1
h₂ : n + single i 1 < n + single i 1 + single i 1
⊢ (coeff n) (pderivFun i (f * g)) = (coeff n) (f • pderivFun i g + g • pderivFun i f)

Tactic:
have h₃ : n < n + single i 1 + single i 1 := lt_trans h₁ h₂

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
i : σ
f g : MvPowerSeries σ R
n : σ →₀ ℕ
h₁ : n < n + single i 1
h₂ : n + single i 1 < n + single i 1 + single i 1
h₃ : n < n + single i 1 + single i 1
⊢ (coeff n) (pderivFun i (f * g)) = (coeff n) (f • pderivFun i g + g • pderivFun i f)
Module: Mathlib.RingTheory.MvPowerSeries.Derivative

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
i : σ
r : R
f : MvPowerSeries σ R
⊢ pderivFun i (r • f) = r • pderivFun i f

Tactic:
rw [smul_eq_C_mul, smul_eq_C_mul, pderivFun_mul, pderivFun_C, smul_zero, add_zero, smul_eq_mul]

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

Goal state before:
pp: X : Type u_1
E : Type u_2
mX : MeasurableSpace X
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
μ : Measure X
f : X → E
hf : Integrable f μ
hE : Nontrivial E
this : IsFiniteMeasure (μ.withDensity fun x ↦ ‖f x‖ₑ)
I : VectorMeasure.Integrable (μ.withDensity fun x ↦ ‖f x‖ₑ).toSignedMeasure fun x ↦ ‖f x‖⁻¹ • f x
s : Set X
hs : MeasurableSet s
⊢ ∫ (x : X) in s, f x ∂μ =
    (withDensity (μ.withDensity fun x ↦ ‖f x‖ₑ).toSignedMeasure (fun x ↦ ‖f x‖⁻¹ • f x)
        (ContinuousLinearMap.lsmul ℝ ℝ).flip)
      s

Tactic:
withDensity_apply I,

Goal state after:
X : Type u_1
E : Type u_2
mX : MeasurableSpace X
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
μ : Measure X
f : X → E
hf : Integrable f μ
hE : Nontrivial E
this : IsFiniteMeasure (μ.withDensity fun x ↦ ‖f x‖ₑ)
I : VectorMeasure.Integrable (μ.withDensity fun x ↦ ‖f x‖ₑ).toSignedMeasure fun x ↦ ‖f x‖⁻¹ • f x
s : Set X
hs : MeasurableSet s
⊢ ∫ (x : X) in s, f x ∂μ = ∫ᵛ (x : X) in s, ‖f x‖⁻¹ • f x ∂<•(μ.withDensity fun x ↦ ‖f x‖ₑ).toSignedMeasure
Module: Mathlib.NumberTheory.PrimeCounting

Goal state before:
pp: ⊢ Tendsto π' atTop atTop

Tactic:
apply tendsto_atTop_atTop_of_monotone' monotone_primeCounting'

Goal state after:
⊢ ¬BddAbove (Set.range π')
Module: Mathlib.NumberTheory.BernoulliPolynomials

Goal state before:
pp: 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)

Tactic:
Finset.range_eq_Ico,

Goal state after:
n : ℕ
⊢ ∑ x ∈ Ico 0 (n + 1),
      ∑ x_1 ∈ Ico 0 (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.AbelSummation

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
m : ℕ
hf_diff : ∀ t ∈ Set.Icc 0 ↑m, DifferentiableAt ℝ f t
hf_int : IntegrableOn (deriv f) (Set.Icc 0 ↑m) volume
⊢ ∑ k ∈ Icc 0 m, f ↑k * c k = f ↑m * ∑ k ∈ Icc 0 m, c k - ∫ (t : ℝ) in Set.Ioc 0 ↑m, deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k

Tactic:
by
  convert! sum_mul_eq_sub_integral_mul c m.cast_nonneg hf_diff hf_int
  all_goals rw [Nat.floor_natCast]

Goal state after:
Module: Mathlib.NumberTheory.BernoulliPolynomials

Goal state before:
pp: n : ℕ
| ∑ x ∈ range (n + 1 - 0),
    ∑ x_1 ∈ range (n + 1 - x), (monomial x) (↑((n + 1).choose (x + x_1)) * ↑((x + x_1).choose x) * _root_.bernoulli x_1)

Tactic:
apply_congr
    · skip
    · conv =>
      apply_congr
      · skip
      · rw [← Nat.cast_mul, choose_mul (le_add_right _ _), Nat.cast_mul, add_tsub_cancel_left,
          mul_assoc, mul_comm, ← smul_eq_mul, ← smul_monomial]

Goal state after:
Module: Mathlib.NumberTheory.BernoulliPolynomials

Goal state before:
pp: n p x : ℕ
hx : x ∈ range (p + 1)
⊢ _root_.bernoulli (p.succ - (p + 1 - x)) = _root_.bernoulli x

pp: n p x : ℕ
hx : x ∈ range (p + 1)
⊢ ↑(p.succ.choose (p + 1 - x)) = ↑((p + 1).choose x)

Tactic:
· rw [Nat.sub_sub_self (mem_range_le hx)]

Goal state after:
n p x : ℕ
hx : x ∈ range (p + 1)
⊢ ↑(p.succ.choose (p + 1 - x)) = ↑((p + 1).choose x)
Module: Mathlib.NumberTheory.Bernoulli

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

Tactic:
refine Eq.trans ?_ (Eq.trans f ?_)

Goal state after:
case succ.succ.refine_1
n : ℕ
f :
  ∑ k ∈ range n, ↑(n.succ.succ.choose (k + 1 + 1)) * bernoulli' (k + 1 + 1) =
    ↑n + 1 + 1 - ↑(n.succ.succ.choose 0) * bernoulli' 0 - ↑(n.succ.succ.choose (0 + 1)) * bernoulli' (0 + 1)
⊢ ∑ i ∈ range n, ↑((n + 2).choose (i + 2)) * bernoulli (i + 2) =
    ∑ k ∈ range n, ↑(n.succ.succ.choose (k + 1 + 1)) * bernoulli' (k + 1 + 1)

case succ.succ.refine_2
n : ℕ
f :
  ∑ k ∈ range n, ↑(n.succ.succ.choose (k + 1 + 1)) * bernoulli' (k + 1 + 1) =
    ↑n + 1 + 1 - ↑(n.succ.succ.choose 0) * bernoulli' 0 - ↑(n.succ.succ.choose (0 + 1)) * bernoulli' (0 + 1)
⊢ ↑n + 1 + 1 - ↑(n.succ.succ.choose 0) * bernoulli' 0 - ↑(n.succ.succ.choose (0 + 1)) * bernoulli' (0 + 1) = ↑n / 2
Module: Mathlib.NumberTheory.Bertrand

Goal state before:
pp: 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))
⊢ 0 < 512

Tactic:
norm_num1

Goal state after:
Module: Mathlib.NumberTheory.Bertrand

Goal state before:
pp: 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
⊢ 1 - 2 / 3 = 1 / 3

Tactic:
norm_num1

Goal state after:
Module: Mathlib.NumberTheory.Bertrand

Goal state before:
pp: case e'_11
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✝
x : ℝ
⊢ 2 * 0.5 < 2 * x ↔ 1 < 2 * x

Tactic:
norm_num1

Goal state after:
case e'_11
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✝
x : ℝ
⊢ 1 < 2 * x ↔ 1 < 2 * x
Module: Mathlib.NumberTheory.Bertrand

Goal state before:
pp: 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
⊢ 1 ≤ 4

Tactic:
norm_num1

Goal state after:
Module: Mathlib.NumberTheory.Bertrand

Goal state before:
pp: 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
⊢ 0 ≤ 3

Tactic:
norm_num1

Goal state after:
Module: Mathlib.NumberTheory.AbelSummation

Goal state before:
pp: case pos
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
a : ℝ
m : ℕ
ha : 0 ≤ a
g : ℝ → 𝕜
hg : LocallyIntegrableOn g (Set.Ici a) volume
K : Set ℝ
hK₁ : K ⊆ Set.Ici a
hK₂ : IsCompact K
hK₃ : K.Nonempty
h_inf : a ≤ sInf K
⊢ Set.Icc (sInf K) (sSup K) ⊆ Set.Ici a

Tactic:
exact (Set.Icc_subset_Ici_iff (Real.sInf_le_sSup _ hK₂.bddBelow hK₂.bddAbove)).mpr h_inf

Goal state after:
Module: Mathlib.NumberTheory.Bertrand

Goal state before:
pp: 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
⊢ 0.5 < 18

Tactic:
norm_num1

Goal state after:
Module: Mathlib.NumberTheory.Bertrand

Goal state before:
pp: 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
⊢ 18 < 512

Tactic:
norm_num1

Goal state after:
Module: Mathlib.NumberTheory.Bertrand

Goal state before:
pp: 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
⊢ 0 < 6

Tactic:
norm_num1

Goal state after:
Module: Mathlib.NumberTheory.Bertrand

Goal state before:
pp: 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
⊢ 6 * 6 = 2 * 18

Tactic:
norm_num1

Goal state after:
Module: Mathlib.NumberTheory.Bertrand

Goal state before:
pp: 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 * 18) = 6
⊢ 0 < 18

Tactic:
norm_num1

Goal state after:
Module: Mathlib.NumberTheory.Bertrand

Goal state before:
pp: 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 * 18) = 6
⊢ 0 < 4 ^ (18 / 3)

Tactic:
norm_num1

Goal state after:
Module: Mathlib.NumberTheory.Bertrand

Goal state before:
pp: case refine_1
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 * 18) = 6
⊢ 4 ^ (18 / 3) ≤ 18 * (2 * 18) ^ 6

Tactic:
norm_num1

Goal state after: