mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Order.UpperLower

Goal state before:
pp: ι : Type u_1
inst✝ : Fintype ι
s : Set (ι → ℝ)
x : ι → ℝ
f : (δ : ℝ) → 0 < δ → ι → ℝ
hf₀ : ∀ (δ : ℝ) (a : 0 < δ), closedBall (f δ a) (δ / 4) ⊆ closedBall x δ
hf₁ : ∀ (δ : ℝ) (a : 0 < δ), closedBall (f δ a) (δ / 4) ⊆ interior s
H : Tendsto (fun r ↦ volume (closure s ∩ closedBall x r) / volume (closedBall x r)) (𝓝[>] 0) (𝓝 0)
ε : ℕ → ℝ
hε' : ∀ (n : ℕ), 0 < ε n
hε₀ : Tendsto ε atTop (𝓝[>] 0)
⊢ False

Tactic:
refine not_eventually.2
    (Frequently.of_forall fun _ ↦ lt_irrefl <| ENNReal.ofReal <| 4⁻¹ ^ Fintype.card ι)
    ((Filter.Tendsto.eventually_lt (H.comp hε₀) tendsto_const_nhds ?_).mono fun n ↦
      lt_of_le_of_lt ?_)

Goal state after:
case refine_1
ι : Type u_1
inst✝ : Fintype ι
s : Set (ι → ℝ)
x : ι → ℝ
f : (δ : ℝ) → 0 < δ → ι → ℝ
hf₀ : ∀ (δ : ℝ) (a : 0 < δ), closedBall (f δ a) (δ / 4) ⊆ closedBall x δ
hf₁ : ∀ (δ : ℝ) (a : 0 < δ), closedBall (f δ a) (δ / 4) ⊆ interior s
H : Tendsto (fun r ↦ volume (closure s ∩ closedBall x r) / volume (closedBall x r)) (𝓝[>] 0) (𝓝 0)
ε : ℕ → ℝ
hε' : ∀ (n : ℕ), 0 < ε n
hε₀ : Tendsto ε atTop (𝓝[>] 0)
⊢ 0 < ENNReal.ofReal (4⁻¹ ^ Fintype.card ι)

case refine_2
ι : Type u_1
inst✝ : Fintype ι
s : Set (ι → ℝ)
x : ι → ℝ
f : (δ : ℝ) → 0 < δ → ι → ℝ
hf₀ : ∀ (δ : ℝ) (a : 0 < δ), closedBall (f δ a) (δ / 4) ⊆ closedBall x δ
hf₁ : ∀ (δ : ℝ) (a : 0 < δ), closedBall (f δ a) (δ / 4) ⊆ interior s
H : Tendsto (fun r ↦ volume (closure s ∩ closedBall x r) / volume (closedBall x r)) (𝓝[>] 0) (𝓝 0)
ε : ℕ → ℝ
hε' : ∀ (n : ℕ), 0 < ε n
hε₀ : Tendsto ε atTop (𝓝[>] 0)
n : ℕ
⊢ ENNReal.ofReal (4⁻¹ ^ Fintype.card ι) ≤
    ((fun r ↦ volume (closure s ∩ closedBall x r) / volume (closedBall x r)) ∘ ε) n
Module: Mathlib.MeasureTheory.VectorMeasure.Variation.Basic

Goal state before:
pp: X : Type u_1
V : Type u_2
mX : MeasurableSpace X
inst✝ : NormedAddCommGroup V
μ : VectorMeasure X V
⊢ (-μ).variation = μ.variation

Tactic:
by simp [variation]

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

Goal state before:
pp: α : Type u_1
hα : MeasurableSpace α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
μ : Measure α
m : Set α → E
hm : ∀ (s : Set α), ‖m s‖ₑ ≤ μ s
inst✝ : IsFiniteMeasure μ
h'm : ∀ (s t : Set α), MeasurableSet s → MeasurableSet t → Disjoint s t → m (s ∪ t) = m s + m t
h''m : ∀ (s : Set α), ¬MeasurableSet s → m s = 0
f : ℕ → Set α
f_meas : ∀ (i : ℕ), MeasurableSet (f i)
f_disj : Pairwise (Function.onFun Disjoint f)
⊢ Filter.Tendsto (fun e ↦ ‖∑ i ∈ Finset.range e, m (f i) - m (⋃ i, f i)‖) Filter.atTop (nhds 0)

Tactic:
simp_rw [norm_sub_rev, ← toReal_enorm, ← ENNReal.toReal_zero]

Goal state after:
α : Type u_1
hα : MeasurableSpace α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
μ : Measure α
m : Set α → E
hm : ∀ (s : Set α), ‖m s‖ₑ ≤ μ s
inst✝ : IsFiniteMeasure μ
h'm : ∀ (s t : Set α), MeasurableSet s → MeasurableSet t → Disjoint s t → m (s ∪ t) = m s + m t
h''m : ∀ (s : Set α), ¬MeasurableSet s → m s = 0
f : ℕ → Set α
f_meas : ∀ (i : ℕ), MeasurableSet (f i)
f_disj : Pairwise (Function.onFun Disjoint f)
⊢ Filter.Tendsto (fun e ↦ ‖m (⋃ i, f i) - ∑ i ∈ Finset.range e, m (f i)‖ₑ.toReal) Filter.atTop (nhds (ENNReal.toReal 0))
Module: Mathlib.MeasureTheory.VectorMeasure.AddContent

Goal state before:
pp: α : Type u_1
hα : MeasurableSpace α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
μ : Measure α
inst✝ : IsFiniteMeasure μ
C : Set (Set α)
m : AddContent E C
hC : IsSetRing C
hCmeas : ∀ s ∈ C, MeasurableSet s
hm : ∀ s ∈ C, ‖m s‖ₑ ≤ μ s
h'C : ∀ (t : Set α) (ε : ℝ≥0∞), MeasurableSet t → 0 < ε → ∃ s ∈ C, μ (s ∆ t) < ε
C' : Set (MeasuredSets μ) := {s | ∃ c ∈ C, ↑s = c}
C'C : ∀ s ∈ C', ↑s ∈ C
C'_dense : Dense C'
m₀ : ↑C' → E := fun x ↦ m ↑↑x
s t : ↑C'
this : edist s t = edist ↑s ↑t
⊢ NullMeasurableSet (↑↑s) μ

Tactic:
exact s.1.2.nullMeasurableSet

Goal state after:
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
f g : X → E
s : Set X
inst✝³ : NormedSpace ℝ E
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedSpace ℝ G
B : E →L[ℝ] F →L[ℝ] G
inst✝ : DecidablePred fun x ↦ x ∈ s
hs : MeasurableSet s
hf : μ.IntegrableOn f s
hg : μ.IntegrableOn g sᶜ
⊢ ∫ᵛ (x : X), s.indicator f x ∂[B; μ] + ∫ᵛ (x : X), sᶜ.indicator g x ∂[B; μ] =
    ∫ᵛ (x : X) in s, f x ∂[B; μ] + ∫ᵛ (x : X) in sᶜ, g x ∂[B; μ]

Tactic:
integral_indicator hs,

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
f g : X → E
s : Set X
inst✝³ : NormedSpace ℝ E
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedSpace ℝ G
B : E →L[ℝ] F →L[ℝ] G
inst✝ : DecidablePred fun x ↦ x ∈ s
hs : MeasurableSet s
hf : μ.IntegrableOn f s
hg : μ.IntegrableOn g sᶜ
⊢ ∫ᵛ (x : X) in s, f x ∂[B; μ] + ∫ᵛ (x : X), sᶜ.indicator g x ∂[B; μ] =
    ∫ᵛ (x : X) in s, f x ∂[B; μ] + ∫ᵛ (x : X) in sᶜ, g x ∂[B; μ]
Module: Mathlib.MeasureTheory.VectorMeasure.AddContent

Goal state before:
pp: α : Type u_1
hα : MeasurableSpace α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
μ : Measure α
inst✝ : IsFiniteMeasure μ
C : Set (Set α)
m : AddContent E C
hC : IsSetSemiring C
hm : ∀ s ∈ C, ‖m s‖ₑ ≤ μ s
h'C : hα = generateFrom C
M : ∀ s ∈ C, MeasurableSet s
D : Set (Set α)
DC : D ⊆ C
D_count : D.Countable
hD : ∀ s ∈ C, s ≤ᵐ[μ] ⋃₀ D
MD : MeasurableSet (⋃₀ D)
μ' : Measure α := μ.restrict (⋃₀ D)
⊢ ∃ m', (∀ s ∈ C, m' s = m s) ∧ ∀ (s : Set α), ‖m' s‖ₑ ≤ μ' s

Tactic:
apply exists_extension_of_isSetSemiring_of_le_measure_of_generateFrom_of_cover hC
      (fun s hs ↦ ?_) h'C ?_
    · exact ⟨D, D_count, DC, by simp [μ', Measure.restrict_apply' MD]⟩
    · apply (hm s hs).trans
      simp only [Measure.restrict_apply' MD, μ']
      apply measure_mono_ae
      nth_rewrite 1 [← Set.inter_self s]
      exact ae_le_set_inter Filter.EventuallyLE.rfl (hD s hs)

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

Goal state before:
pp: M : Type u_1
inst✝¹ : AddCommMonoid M
inst✝ : IsCancelAdd M
a : M
t : Finset M
ih : ∀ m < t.card, ∀ (a : M) (t : Finset M), t.card = m → IsProperSemilinearSet (a +ᵥ ↑(closure ↑t))
t' : Finset M
ht' : t' ⊆ t
f : M → ℕ
i : M
hi : i ∈ t'
hfi : 0 < f i
heq : ∑ x ∈ t', f x • x = ∑ x ∈ t \ t', f x • x
g : M → ℕ
ih' :
  ∀ m < g i,
    ∀ (g : M → ℕ),
      g i = m → a +ᵥ ∑ a ∈ t, g a • a ∈ ⋃ j ∈ t', ⋃ k ∈ Finset.range (f j), (a + k • j) +ᵥ ↑(closure ↑(t.erase j))
hfg : ∀ j ∈ t', f j ≤ g j
⊢ ∑ a ∈ t', g a • a + ∑ a ∈ t \ t', g a • a = ∑ x ∈ t ∩ t', (g x - f x) • x + ∑ x ∈ t with x ∉ t', (g x + f x) • x

Tactic:
Finset.inter_eq_right.2 ht',

Goal state after:
M : Type u_1
inst✝¹ : AddCommMonoid M
inst✝ : IsCancelAdd M
a : M
t : Finset M
ih : ∀ m < t.card, ∀ (a : M) (t : Finset M), t.card = m → IsProperSemilinearSet (a +ᵥ ↑(closure ↑t))
t' : Finset M
ht' : t' ⊆ t
f : M → ℕ
i : M
hi : i ∈ t'
hfi : 0 < f i
heq : ∑ x ∈ t', f x • x = ∑ x ∈ t \ t', f x • x
g : M → ℕ
ih' :
  ∀ m < g i,
    ∀ (g : M → ℕ),
      g i = m → a +ᵥ ∑ a ∈ t, g a • a ∈ ⋃ j ∈ t', ⋃ k ∈ Finset.range (f j), (a + k • j) +ᵥ ↑(closure ↑(t.erase j))
hfg : ∀ j ∈ t', f j ≤ g j
⊢ ∑ a ∈ t', g a • a + ∑ a ∈ t \ t', g a • a = ∑ x ∈ t', (g x - f x) • x + ∑ x ∈ t with x ∉ t', (g x + f x) • x
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Definability

Goal state before:
pp: case all
α : Type u_1
A : Set ℕ
inst✝ : Finite α
n✝ : ℕ
this : Fintype α
n : ℕ
φ : presburger[[↑A]].BoundedFormula α (n + 1)
ih : IsSemilinearSet {v | φ.Realize (v ∘ Sum.inl) (v ∘ Sum.inr)}
⊢ IsSemilinearSet {v | ∀ (x : ℕ), φ.Realize (v ∘ Sum.inl) (Fin.snoc (v ∘ Sum.inr) x)}

Tactic:
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.Complexity

Goal state before:
pp: case imp
L : Language
α : Type u'
n : ℕ
φ : L.BoundedFormula α (n + 1)
con : (∀' ∼φ).IsQF
h₂✝ : ⊥.IsQF
⊢ False

Tactic:
exact not_all_isQF _ con

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_le_dom : f.dom ≤ g.dom
le_cod : f.cod ≤ g.cod
h_eq : ∀ (x : ↥f.dom), (inclusion le_cod) (f.toEquiv x) = g.toEquiv ((inclusion dom_le_dom) x)
x✝ : ↥f.dom
⊢ g.cod.subtype (g.toEquiv ((inclusion dom_le_dom) x✝)) = (f.cod.subtype.comp f.toEquiv.toEmbedding) x✝

Tactic:
rw [← h_eq]

Goal state after:
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f g : M ≃ₚ[L] N
dom_le_dom : f.dom ≤ g.dom
le_cod : f.cod ≤ g.cod
h_eq : ∀ (x : ↥f.dom), (inclusion le_cod) (f.toEquiv x) = g.toEquiv ((inclusion dom_le_dom) x)
x✝ : ↥f.dom
⊢ g.cod.subtype ((inclusion le_cod) (f.toEquiv x✝)) = (f.cod.subtype.comp f.toEquiv.toEmbedding) x✝
Module: Mathlib.ModelTheory.Types

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

Tactic:
exact p.isMaximal.1.mono (union_subset p.subset hp)

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

Goal state before:
pp: case neg
m n : ℕ
hm : ¬m = 0
⊢ liouville (m * n) = liouville m * liouville n

Tactic:
by_cases hn : n = 0

Goal state after:
case pos
m n : ℕ
hm : ¬m = 0
hn : n = 0
⊢ liouville (m * n) = liouville m * liouville n

case neg
m n : ℕ
hm : ¬m = 0
hn : ¬n = 0
⊢ liouville (m * n) = liouville m * liouville n
Module: Mathlib.RingTheory.ZMod.UnitsCyclic

Goal state before:
pp: p : ℕ
hp : Nat.Prime p
hp2 : p ≠ 2
n : ℕ
this : Fact (Nat.Prime p)
⊢ IsCyclic (ZMod (p ^ n))ˣ

Tactic:
rcases n with _ | n

Goal state after:
case zero
p : ℕ
hp : Nat.Prime p
hp2 : p ≠ 2
this : Fact (Nat.Prime p)
⊢ IsCyclic (ZMod (p ^ 0))ˣ

case succ
p : ℕ
hp : Nat.Prime p
hp2 : p ≠ 2
this : Fact (Nat.Prime p)
n : ℕ
⊢ IsCyclic (ZMod (p ^ (n + 1)))ˣ
Module: Mathlib.RingTheory.MvPowerSeries.Derivative

Goal state before:
pp: σ : Type u_1
R : Type u_2
i : σ
inst✝ : Field R
f : MvPowerSeries σ R
⊢ (pderiv R i) f⁻¹ = -f⁻¹ ^ 2 * (pderiv R i) f

Tactic:
by
  by_cases h : constantCoeff f = 0
  · suffices f⁻¹ = 0 by
      rw [this, pow_two, zero_mul, neg_zero, zero_mul, map_zero]
    rwa [MvPowerSeries.inv_eq_zero]
  apply Derivation.leibniz_of_mul_eq_one
  exact MvPowerSeries.inv_mul_cancel (h := h)

Goal state after:
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‖₊ = ‖x‖₊ * ‖y‖₊
x : E
y : F
⊢ ‖B.flip y‖₊ * ‖x‖₊ ≤ ‖(B x) y‖₊

Tactic:
rw [hB, mul_comm]

Goal state after:
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‖₊ = ‖x‖₊ * ‖y‖₊
x : E
y : F
⊢ ‖x‖₊ * ‖B.flip y‖₊ ≤ ‖x‖₊ * ‖y‖₊
Module: Mathlib.NumberTheory.PrimeCounting

Goal state before:
pp: n : ℕ
⊢ n.primesLE = filter Prime (Icc 1 n)

Tactic:
by
  ext p
  simp +contextual [primesLE_eq_filter_range, Nat.Prime.one_le]

Goal state after:
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: case succ.succ
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
⊢ (algebraMap ℚ A) (bernoulli (n + 1 + 1) / ((↑(n + 1) + 1) * ↑(n + 1)!)) * ((algebraMap ℚ A) (↑0 + 1)⁻¹ - 1) +
      (algebraMap ℚ A) (∑ x ∈ antidiagonal (n + 1), bernoulli x.1 / ↑x.1! * ((↑x.2 + 1) * ↑x.2!)⁻¹) =
    if n + 1 + 1 = 1 then 1 else 0

Tactic:
if_neg n.succ_succ_ne_one

Goal state after:
case succ.succ
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
⊢ (algebraMap ℚ A) (bernoulli (n + 1 + 1) / ((↑(n + 1) + 1) * ↑(n + 1)!)) * ((algebraMap ℚ A) (↑0 + 1)⁻¹ - 1) +
      (algebraMap ℚ A) (∑ x ∈ antidiagonal (n + 1), bernoulli x.1 / ↑x.1! * ((↑x.2 + 1) * ↑x.2!)⁻¹) =
    0
Module: Mathlib.NumberTheory.Bertrand

Goal state before:
pp: case hf
x : ℝ
x_large : 512 ≤ x
f : ℝ → ℝ := ⋯
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
⊢ ConcaveOn ℝ (Set.Ioi 0.5) fun x ↦ log x + √(2 * x) * log (2 * x)

pp: case hg
x : ℝ
x_large : 512 ≤ x
f : ℝ → ℝ := ⋯
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
⊢ ConvexOn ℝ (Set.Ioi 0.5) (HMul.hMul (log 4 / 3))

Tactic:
· apply ConcaveOn.add
      · exact strictConcaveOn_log_Ioi.concaveOn.subset
          (Set.Ioi_subset_Ioi (by norm_num)) (convex_Ioi 0.5)
      convert!
        ((strictConcaveOn_sqrt_mul_log_Ioi.concaveOn.comp_linearMap ((2 : ℝ) • LinearMap.id)))
        using 1
      ext x
      simp only [Set.mem_Ioi, Set.mem_preimage, LinearMap.smul_apply,
        LinearMap.id_coe, id_eq, smul_eq_mul]
      rw [← mul_lt_mul_iff_right₀ (two_pos)]
      norm_num1
      rfl

Goal state after:
case hg
x : ℝ
x_large : 512 ≤ x
f : ℝ → ℝ := ⋯
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
⊢ ConvexOn ℝ (Set.Ioi 0.5) (HMul.hMul (log 4 / 3))
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: n p : ℕ
hne : ∀ (m : ℕ), ↑m ! ≠ 0
⊢ ∑ k ∈ range n, ↑k ^ p = ∑ i ∈ range (p + 1), bernoulli i * ↑((p + 1).choose i) * ↑n ^ (p + 1 - i) / (↑p + 1)

Tactic:
have h_cauchy :
    ((mk fun p => bernoulli p / p !) * mk fun q => coeff (q + 1) (exp ℚ ^ n)) =
      mk fun p => ∑ i ∈ range (p + 1),
          bernoulli i * (p + 1).choose i * (n : ℚ) ^ (p + 1 - i) / (p + 1)! := by
    ext q : 1
    let f a b := bernoulli a / a ! * coeff (b + 1) (exp ℚ ^ n)
    -- key step: use `PowerSeries.coeff_mul` and then rewrite sums
    simp only [f, coeff_mul, coeff_mk, sum_antidiagonal_eq_sum_range_succ f]
    apply sum_congr rfl
    intro m h
    simp only [exp_pow_eq_rescale_exp, rescale, RingHom.coe_mk]
    -- manipulate factorials and binomial coefficients
    have h : m < q + 1 := by simpa using h
    rw [choose_eq_factorial_div_factorial h.le, eq_comm, div_eq_iff (hne q.succ), succ_eq_add_one,
      mul_assoc _ _ (q.succ ! : ℚ), mul_comm _ (q.succ ! : ℚ), ← mul_assoc, div_mul_eq_mul_div]
    simp only [MonoidHom.coe_mk, OneHom.coe_mk, coeff_exp, Algebra.algebraMap_self, one_div,
      map_inv₀, map_natCast, coeff_mk]
    rw [mul_comm ((n : ℚ) ^ (q - m + 1)), ← mul_assoc _ _ ((n : ℚ) ^ (q - m + 1)), ← one_div,
      mul_one_div, div_div, tsub_add_eq_add_tsub (le_of_lt_succ h), cast_div, cast_mul]
    · ring
    · exact factorial_mul_factorial_dvd_factorial h.le
    · simp [factorial_ne_zero]

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)!
⊢ ∑ k ∈ range n, ↑k ^ p = ∑ i ∈ range (p + 1), bernoulli i * ↑((p + 1).choose i) * ↑n ^ (p + 1 - i) / (↑p + 1)
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:
rw [rpow_natCast, ← pow_mul, ← 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.ClassNumber.AdmissibleAbsoluteValue

Goal state before:
pp: R : Type u_1
inst✝ : EuclideanDomain R
abv : AbsoluteValue R ℤ
h : abv.IsAdmissible
this : DecidableEq R
n : ℕ
ih :
  ∀ {ε : ℝ},
    0 < ε →
      ∀ {b : R},
        b ≠ 0 →
          ∀ (A : Fin (h.card ε ^ n).succ → Fin n → R),
            ∃ i₀ i₁, i₀ ≠ i₁ ∧ ∀ (k : Fin n), ↑(abv (A i₁ k % b - A i₀ k % b)) < abv b • ε
ε : ℝ
hε : 0 < ε
b : R
hb : b ≠ 0
A : Fin (h.card ε ^ (n + 1)).succ → Fin (n + 1) → R
M : ℕ := h.card ε
t : Fin (M ^ n.succ).succ → Fin M
ht : ∀ (i₀ i₁ : Fin (M ^ n.succ).succ), t i₀ = t i₁ → ↑(abv (A i₁ 0 % b - A i₀ 0 % b)) < abv b • ε
s : Fin M
hs : M ^ n < {x | t x = s}.card
⊢ ∃ s, Function.Injective s ∧ ∀ (i₀ i₁ : Fin (M ^ n).succ), ↑(abv (A (s i₁) 0 % b - A (s i₀) 0 % b)) < abv b • ε

Tactic:
have : (M ^ n).succ ≤ (Finset.toList {x | t x = s}).length := by
      rwa [Finset.length_toList]

Goal state after:
R : Type u_1
inst✝ : EuclideanDomain R
abv : AbsoluteValue R ℤ
h : abv.IsAdmissible
this✝ : DecidableEq R
n : ℕ
ih :
  ∀ {ε : ℝ},
    0 < ε →
      ∀ {b : R},
        b ≠ 0 →
          ∀ (A : Fin (h.card ε ^ n).succ → Fin n → R),
            ∃ i₀ i₁, i₀ ≠ i₁ ∧ ∀ (k : Fin n), ↑(abv (A i₁ k % b - A i₀ k % b)) < abv b • ε
ε : ℝ
hε : 0 < ε
b : R
hb : b ≠ 0
A : Fin (h.card ε ^ (n + 1)).succ → Fin (n + 1) → R
M : ℕ := h.card ε
t : Fin (M ^ n.succ).succ → Fin M
ht : ∀ (i₀ i₁ : Fin (M ^ n.succ).succ), t i₀ = t i₁ → ↑(abv (A i₁ 0 % b - A i₀ 0 % b)) < abv b • ε
s : Fin M
hs : M ^ n < {x | t x = s}.card
this : (M ^ n).succ ≤ {x | t x = s}.toList.length
⊢ ∃ s, Function.Injective s ∧ ∀ (i₀ i₁ : Fin (M ^ n).succ), ↑(abv (A (s i₁) 0 % b - A (s i₀) 0 % b)) < abv b • ε
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: p M N : ℕ
inst✝ : Fact (Nat.Prime p)
hM : M ≠ 0
hv : M.factorization p ≤ N
⊢ pIntegral p (↑p ^ N / ↑M)

Tactic:
set e := M.factorization p

Goal state after:
p M N : ℕ
inst✝ : Fact (Nat.Prime p)
hM : M ≠ 0
e : ℕ := M.factorization p
hv : e ≤ N
⊢ pIntegral p (↑p ^ N / ↑M)
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: n : ℕ
⊢ n.lcmUpto = ∏ p ∈ n.primesLE, p ^ log p n

Tactic:
rw [lcmUpto_eq_prod]
  exact Finset.prod_congr rfl fun p hp ↦ congrArg (p ^ ·) <|
    factorization_lcmUpto n <| prime_of_mem_primesLE hp

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: n p : ℕ
hp : p ∈ n.primesLE
k : ℕ
hk : k ∈ Icc 1 (Nat.log p n)
⊢ Λ p = log ↑p

Tactic:
vonMangoldt_apply_prime <| prime_of_mem_primesLE hp

Goal state after:
n p : ℕ
hp : p ∈ n.primesLE
k : ℕ
hk : k ∈ Icc 1 (Nat.log p n)
⊢ log ↑p = log ↑p
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 ℤ
I : ↥(Ideal S)⁰
⊢ ∃ b, ∀ (z : ℤ), (∃ b ∈ ↑I, b ≠ 0 ∧ abv ((Algebra.norm R) b) = z) → b ≤ z

Tactic:
use 0
      rintro _ ⟨b, _, _, rfl⟩
      apply abv.nonneg

Goal state after:
Module: Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree

Goal state before:
pp: Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
b : Fq[X]
hb : b ≠ 0
ε : ℝ
hε : 0 < ε
A : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊).succ → Fq[X]
hbε : 0 < cardPowDegree b • ε
one_lt_q : 1 < Fintype.card Fq
one_lt_q' : 1 < ↑(Fintype.card Fq)
q_pos : 0 < Fintype.card Fq
q_pos' : 0 < ↑(Fintype.card Fq)
le_b : ⌈-log ε / log ↑(Fintype.card Fq)⌉₊ < b.natDegree
i₀ i₁ : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊).succ
i_ne : i₀ ≠ i₁
deg_lt : (A i₁ % b - A i₀ % b).degree < ↑(b.natDegree - ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)
h : ¬A i₁ % b = A i₀ % b
h' : A i₁ % b - A i₀ % b ≠ 0
⊢ ↑(b.natDegree - ⌈-log ε / log ↑(Fintype.card Fq)⌉₊) ≤ ↑b.natDegree - -log ε / log ↑(Fintype.card Fq)

Tactic:
Nat.cast_sub le_b.le

Goal state after:
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
b : Fq[X]
hb : b ≠ 0
ε : ℝ
hε : 0 < ε
A : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊).succ → Fq[X]
hbε : 0 < cardPowDegree b • ε
one_lt_q : 1 < Fintype.card Fq
one_lt_q' : 1 < ↑(Fintype.card Fq)
q_pos : 0 < Fintype.card Fq
q_pos' : 0 < ↑(Fintype.card Fq)
le_b : ⌈-log ε / log ↑(Fintype.card Fq)⌉₊ < b.natDegree
i₀ i₁ : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊).succ
i_ne : i₀ ≠ i₁
deg_lt : (A i₁ % b - A i₀ % b).degree < ↑(b.natDegree - ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)
h : ¬A i₁ % b = A i₀ % b
h' : A i₁ % b - A i₀ % b ≠ 0
⊢ ↑b.natDegree - ↑⌈-log ε / log ↑(Fintype.card Fq)⌉₊ ≤ ↑b.natDegree - -log ε / log ↑(Fintype.card Fq)
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 ℤ
I : ↥(Ideal S)⁰
b : S
b_mem : b ∈ ↑I
b_ne_zero : b ≠ 0
min : ∀ (z : ℤ), (∃ b ∈ ↑I, b ≠ 0 ∧ abv ((Algebra.norm R) b) = z) → abv ((Algebra.norm R) b) ≤ z
c : S
hc : c ∈ ↑I
⊢ abv ((Algebra.norm R) c) < abv ((Algebra.norm R) b) → c = 0

Tactic:
lt

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : EuclideanDomain R
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : Algebra R S
abv : AbsoluteValue R ℤ
I : ↥(Ideal S)⁰
b : S
b_mem : b ∈ ↑I
b_ne_zero : b ≠ 0
min : ∀ (z : ℤ), (∃ b ∈ ↑I, b ≠ 0 ∧ abv ((Algebra.norm R) b) = z) → abv ((Algebra.norm R) b) ≤ z
c : S
hc : c ∈ ↑I
lt : abv ((Algebra.norm R) c) < abv ((Algebra.norm R) b)
⊢ c = 0
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 ℤ
I : ↥(Ideal S)⁰
b : S
b_mem : b ∈ ↑I
b_ne_zero : b ≠ 0
min : ∀ (z : ℤ), (∃ b ∈ ↑I, b ≠ 0 ∧ abv ((Algebra.norm R) b) = z) → abv ((Algebra.norm R) b) ≤ z
c : S
hc : c ∈ ↑I
c_ne_zero : c ≠ 0
⊢ abv ((Algebra.norm R) b) ≤ abv ((Algebra.norm R) c)

Tactic:
exact min _ ⟨c, hc, c_ne_zero, rfl⟩

Goal state after:
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)⁻¹)

Tactic:
theta_eq_zero_of_le_one (rpow_le_one hx h (by positivity))

Goal state after:
case inl
x : ℝ
hx : 0 ≤ x
n m : ℕ
hnm : n ≤ m
hn : 1 ≤ n
hm : 1 ≤ m
h : x ≤ 1
⊢ 0 ≤ θ (x ^ (↑n)⁻¹)
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
⊢ 0 ≤ θ (x ^ (↑n)⁻¹)

Tactic:
theta_eq_zero_of_le_one (rpow_le_one hx h (by positivity))

Goal state after:
case inl
x : ℝ
hx : 0 ≤ x
n m : ℕ
hnm : n ≤ m
hn : 1 ≤ n
hm : 1 ≤ m
h : x ≤ 1
⊢ 0 ≤ 0
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:

Tactic:
theta_eq_zero_of_le_one (rpow_le_one hx h (by positivity))

Goal state after:
Module: Mathlib.NumberTheory.FunctionField

Goal state before:
pp: F : Type u_1
K : Type u_2
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Algebra F[X] K
inst✝¹ : Algebra F⟮X⟯ K
inst✝ : IsScalarTower F[X] F⟮X⟯ K
hinj : Function.Injective ⇑(algebraMap F[X] K)
⊢ Function.Injective ⇑(algebraMap F[X] ↥(ringOfIntegers F K))

Tactic:
rw [injective_iff_map_eq_zero (algebraMap F[X] (↥(ringOfIntegers F K)))]

Goal state after:
F : Type u_1
K : Type u_2
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Algebra F[X] K
inst✝¹ : Algebra F⟮X⟯ K
inst✝ : IsScalarTower F[X] F⟮X⟯ K
hinj : Function.Injective ⇑(algebraMap F[X] K)
⊢ ∀ (a : F[X]), (algebraMap F[X] ↥(ringOfIntegers F K)) a = 0 → a = 0