mathlib-initiative/mathlib-tactics huggingface dataset:
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
lip : LipschitzWith 1 m₀
m₁ : MeasuredSets μ → E := C'_dense.extend m₀
m₁_lip : LipschitzWith 1 m₁
hBound : ∀ (s : MeasuredSets μ), ‖m₁ s‖ₑ ≤ μ ↑s
s t : MeasuredSets μ
h : Disjoint ↑s ↑t
ε : ℝ≥0∞
εpos : ε > 0
δ : ℝ≥0∞
δpos : 0 < δ
hδ : 8 * δ = ε
s' : Set α
s'C : s' ∈ C
hs' : μ (s' ∆ ↑s) < δ
t' : Set α
t'C : t' ∈ C
ht' : μ (t' ∆ ↑t) < δ
It : ‖m t' - m₁ t‖ₑ < δ
hμ' : μ (s' ∩ t') < 2 * δ
s'' : Set α := s' \ t'
s''C : s'' ∈ C
hs'' : μ (s'' ∆ ↑s) < 3 * δ
Is : ‖m s'' - m₁ s‖ₑ < 3 * δ
Ist : ‖m (s'' ∪ t') - m₁ ⟨↑s ∪ ↑t, ⋯⟩‖ₑ < 4 * δ
⊢ ‖m (s'' ∪ t') - m s'' - m t'‖ₑ + ‖m₁ ⟨↑s ∪ ↑t, ⋯⟩ - m (s'' ∪ t')‖ₑ + ‖m s'' - m₁ s‖ₑ + ‖m t' - m₁ t‖ₑ =
    ‖m₁ ⟨↑s ∪ ↑t, ⋯⟩ - m (s'' ∪ t')‖ₑ + ‖m s'' - m₁ s‖ₑ + ‖m t' - m₁ t‖ₑ

Tactic:
addContent_union hC s''C t'C Set.disjoint_sdiff_left

Goal state after:
α : 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
lip : LipschitzWith 1 m₀
m₁ : MeasuredSets μ → E := C'_dense.extend m₀
m₁_lip : LipschitzWith 1 m₁
hBound : ∀ (s : MeasuredSets μ), ‖m₁ s‖ₑ ≤ μ ↑s
s t : MeasuredSets μ
h : Disjoint ↑s ↑t
ε : ℝ≥0∞
εpos : ε > 0
δ : ℝ≥0∞
δpos : 0 < δ
hδ : 8 * δ = ε
s' : Set α
s'C : s' ∈ C
hs' : μ (s' ∆ ↑s) < δ
t' : Set α
t'C : t' ∈ C
ht' : μ (t' ∆ ↑t) < δ
It : ‖m t' - m₁ t‖ₑ < δ
hμ' : μ (s' ∩ t') < 2 * δ
s'' : Set α := s' \ t'
s''C : s'' ∈ C
hs'' : μ (s'' ∆ ↑s) < 3 * δ
Is : ‖m s'' - m₁ s‖ₑ < 3 * δ
Ist : ‖m (s'' ∪ t') - m₁ ⟨↑s ∪ ↑t, ⋯⟩‖ₑ < 4 * δ
⊢ ‖m s'' + m t' - m s'' - m t'‖ₑ + ‖m₁ ⟨↑s ∪ ↑t, ⋯⟩ - (m s'' + m t')‖ₑ + ‖m s'' - m₁ s‖ₑ + ‖m t' - m₁ t‖ₑ =
    ‖m₁ ⟨↑s ∪ ↑t, ⋯⟩ - (m s'' + m t')‖ₑ + ‖m s'' - m₁ s‖ₑ + ‖m t' - m₁ t‖ₑ
Module: Mathlib.MeasureTheory.VectorMeasure.Variation.Semivariation

Goal state before:
pp: case inr
X : Type u_1
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
mX : MeasurableSpace X
μ : VectorMeasure X E
s : Set X
hs : MeasurableSet s
h's : μ.semivariation s = ∞
t : Set X
ts : t ⊆ s
t_meas : MeasurableSet t
ht : 2 * ‖μ s‖ₑ + 2 < 2 * ‖μ t‖ₑ
h't : 1 + ‖μ s‖ₑ ≤ ‖μ t‖ₑ
hI : μ.semivariation (s \ t) = ∞
⊢ 1 ≤ ‖μ (s \ (s \ t))‖ₑ

Tactic:
simp only [_root_.sdiff_sdiff_right_self, ts, inf_of_le_right]

Goal state after:
case inr
X : Type u_1
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
mX : MeasurableSpace X
μ : VectorMeasure X E
s : Set X
hs : MeasurableSet s
h's : μ.semivariation s = ∞
t : Set X
ts : t ⊆ s
t_meas : MeasurableSet t
ht : 2 * ‖μ s‖ₑ + 2 < 2 * ‖μ t‖ₑ
h't : 1 + ‖μ s‖ₑ ≤ ‖μ t‖ₑ
hI : μ.semivariation (s \ t) = ∞
⊢ 1 ≤ ‖μ t‖ₑ
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
⊢ ∫ᵛ (x : X), f x ∂[B; -μ] = -∫ᵛ (x : X), f x ∂[B; μ]

Tactic:
by
  simp [integral, ← setToFun_neg', FunLike.coe_neg]

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
hμ : μ.Integrable f
hν : ν.Integrable f
⊢ ∫ᵛ (x : X), f x ∂[B; μ] + ∫ᵛ (x : X), f x ∂[B; -ν] = ∫ᵛ (x : X), f x ∂[B; μ] - ∫ᵛ (x : X), f x ∂[B; ν]

Tactic:
integral_neg_vectorMeasure,

Goal state after:
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
hμ : μ.Integrable f
hν : ν.Integrable f
⊢ ∫ᵛ (x : X), f x ∂[B; μ] + -∫ᵛ (x : X), f x ∂[B; ν] = ∫ᵛ (x : X), f x ∂[B; μ] - ∫ᵛ (x : X), f x ∂[B; ν]
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
⊢ ∫ᵛ (x : X), f x ∂[-B; μ] = -∫ᵛ (x : X), f x ∂[B; μ]

Tactic:
by
  simp [integral, ← setToFun_neg', FunLike.coe_neg]

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 C : E →L[ℝ] F →L[ℝ] G
hB : μ.Integrable f
⊢ ∫ᵛ (x : X), f x ∂[B; μ] + ∫ᵛ (x : X), f x ∂[-C; μ] = ∫ᵛ (x : X), f x ∂[B; μ] - ∫ᵛ (x : X), f x ∂[C; μ]

Tactic:
integral_neg_cbm,

Goal state after:
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 C : E →L[ℝ] F →L[ℝ] G
hB : μ.Integrable f
⊢ ∫ᵛ (x : X), f x ∂[B; μ] + -∫ᵛ (x : X), f x ∂[C; μ] = ∫ᵛ (x : X), f x ∂[B; μ] - ∫ᵛ (x : X), f x ∂[C; μ]
Module: Mathlib.MeasureTheory.VectorMeasure.Integral

Goal state before:

Tactic:
∫ᵛ 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 f) _
    _ = 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:
congr with x; congr; exact Unique.uniq _ x

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

Goal state before:
pp: case hbc.h
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✝ : IsFiniteMeasure μ.variation
C : ℝ
h : ∀ᵐ (x : X) ∂μ.variation, ‖f x‖ ≤ C
⊢ ∀ᵐ (a : X) ∂μ.variation, ENNReal.ofReal ‖f a‖ ≤ ENNReal.ofReal C

Tactic:
filter_upwards [h] with x hx using ENNReal.ofReal_mono hx

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_9
inst✝ : MeasurableSpace β
φ : X → β
hφ : MeasurableEmbedding φ
f : β → E
⊢ ∫ᵛ (y : β), f y ∂[B; μ.map φ] = ∫ᵛ (x : X), f (φ x) ∂[B; μ]

Tactic:
by_cases hfm : AEStronglyMeasurable f (μ.variation.map φ)
  · by_cases h'fm : μ.Integrable (f ∘ φ)
    · apply integral_map hφ.measurable hfm h'fm
    · rw [integral_undef, integral_undef]
      · exact h'fm
      · rwa [hφ.integrable_map_vectorMeasure]
  · rw [integral_non_aestronglyMeasurable, integral_non_aestronglyMeasurable]
    · rwa [hφ.aestronglyMeasurable_map_iff] at hfm
    · rwa [hφ.variation_map]

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

Goal state before:
pp: case mpr.refine_2
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
i : ↑hs.basisSet
z : ι → ℕ
hz : z ∈ closure (hs.basisSet \ {↑i})
z' : ι → ℕ
hz' : z' ∈ closure (hs.basisSet \ {↑i})
n : ℕ
heq : hs.floor (x + ↑i + n • ↑i + z') i = hs.floor hs.base i
⊢ hs.floor x i < 0

Tactic:
hs.floor_add_of_mem_closure sdiff_subset (notMem_sdiff_of_mem (mem_singleton i.1)) hz',

Goal state after:
case mpr.refine_2
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
i : ↑hs.basisSet
z : ι → ℕ
hz : z ∈ closure (hs.basisSet \ {↑i})
z' : ι → ℕ
hz' : z' ∈ closure (hs.basisSet \ {↑i})
n : ℕ
heq : hs.floor (x + ↑i + n • ↑i) i = hs.floor hs.base i
⊢ hs.floor x i < 0
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 : ↑i ∉ hs.periods
hi' : 0 < hs.floor x i
⊢ x + ∑ j ∈ Finset.univ.erase i, (-hs.floor x j).toNat • ↑j =
    hs.base + ↑i + ((hs.floor x i).toNat - 1) • ↑i + ∑ j ∈ Finset.univ.erase i, (hs.floor x j).toNat • ↑j

Tactic:
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]

Goal state after:
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 : ↑i ∉ hs.periods
hi' : 0 < hs.floor x i
⊢ x + ∑ x_1, (-hs.floor x x_1).toNat • ↑x_1 = hs.fract x + ∑ x_1, (hs.floor x x_1).toNat • ↑x_1
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: case mpr.refine_2
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
i : ↑hs.basisSet
hi : ↑i ∉ hs.periods
z : ι → ℕ
hz : z ∈ closure (hs.basisSet \ {↑i})
z' : ι → ℕ
hz' : z' ∈ closure (hs.basisSet \ {↑i})
n : ℕ
heq : hs.floor (x + z') i = hs.floor (hs.base + ↑i + n • ↑i) i
⊢ 0 < hs.floor x i

Tactic:
hs.floor_add_of_mem_closure sdiff_subset (notMem_sdiff_of_mem (mem_singleton i.1)) hz',

Goal state after:
case mpr.refine_2
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
i : ↑hs.basisSet
hi : ↑i ∉ hs.periods
z : ι → ℕ
hz : z ∈ closure (hs.basisSet \ {↑i})
z' : ι → ℕ
hz' : z' ∈ closure (hs.basisSet \ {↑i})
n : ℕ
heq : hs.floor x i = hs.floor (hs.base + ↑i + n • ↑i) i
⊢ 0 < hs.floor x i
Module: Mathlib.NumberTheory.AbelSummation

Goal state before:
pp: a b : ℝ
k : ℕ
hk : k ∈ Ico (⌊a⌋₊ + 1) ⌊b⌋₊
⊢ k ∈ Set.Ico (⌊a⌋₊ + 1) ⌊b⌋₊

Tactic:
rwa [← Finset.coe_Ico]

Goal state after:
Module: Mathlib.NumberTheory.Basic

Goal state before:
pp: case zero
R : Type u_1
inst✝ : CommRing R
p : ℕ
a b : R
h : ↑p ∣ a - b
⊢ ↑p ^ (0 + 1) ∣ a ^ p ^ 0 - b ^ p ^ 0

Tactic:
pow_one,

Goal state after:
case zero
R : Type u_1
inst✝ : CommRing R
p : ℕ
a b : R
h : ↑p ∣ a - b
⊢ ↑p ∣ a ^ p ^ 0 - b ^ p ^ 0
Module: Mathlib.NumberTheory.Basic

Goal state before:
pp: case zero
R : Type u_1
inst✝ : CommRing R
p : ℕ
a b : R
h : ↑p ∣ a - b
⊢ ↑p ∣ a ^ 1 - b ^ 1

Tactic:
pow_one,

Goal state after:
case zero
R : Type u_1
inst✝ : CommRing R
p : ℕ
a b : R
h : ↑p ∣ a - b
⊢ ↑p ∣ a - b ^ 1
Module: Mathlib.NumberTheory.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
p : ℕ
a b : R
h : ↑p ∣ a - b
k : ℕ
ih : ↑p ^ (k + 1) ∣ a ^ p ^ k - b ^ p ^ k
f : R →+* R ⧸ span {↑p} := mk (span {↑p})
r : R
⊢ ↑p ∣ r ↔ f r = 0

Tactic:
rw [eq_zero_iff_mem, mem_span_singleton]

Goal state after:
Module: Mathlib.NumberTheory.Basic

Goal state before:
pp: case succ
R : Type u_1
inst✝ : CommRing R
p : ℕ
a b : R
k : ℕ
ih : ↑p ^ (k + 1) ∣ a ^ p ^ k - b ^ p ^ k
f : R →+* R ⧸ span {↑p} := mk (span {↑p})
h : f a = f b
hf : ∀ (r : R), ↑p ∣ r ↔ f r = 0
⊢ ↑p * (f b ^ p ^ k) ^ (p - 1) = 0

Tactic:
mul_eq_zero_of_left

Goal state after:
case succ
R : Type u_1
inst✝ : CommRing R
p : ℕ
a b : R
k : ℕ
ih : ↑p ^ (k + 1) ∣ a ^ p ^ k - b ^ p ^ k
f : R →+* R ⧸ span {↑p} := mk (span {↑p})
h : f a = f b
hf : ∀ (r : R), ↑p ∣ r ↔ f r = 0
⊢ 0 = 0

case succ.h
R : Type u_1
inst✝ : CommRing R
p : ℕ
a b : R
k : ℕ
ih : ↑p ^ (k + 1) ∣ a ^ p ^ k - b ^ p ^ k
f : R →+* R ⧸ span {↑p} := mk (span {↑p})
h : f a = f b
hf : ∀ (r : R), ↑p ∣ r ↔ f r = 0
⊢ ↑p = 0
Module: Mathlib.NumberTheory.AbelSummation

Goal state before:
pp: case inl
𝕜 : 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⌋₊
⊢ ∑ 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

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⌋₊
⊢ ∑ 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:
· rw [hb, Ioc_eq_empty_of_le le_rfl, sum_empty, ← sub_mul,
      integralmulsum c hf_diff hf_int _ _ ⌊b⌋₊ hab (hb ▸ aux1) aux2 le_rfl le_rfl, sub_self]

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⌋₊
⊢ ∑ 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
Module: Mathlib.RingTheory.ZMod.UnitsCyclic

Goal state before:
pp: case refine_1
p : ℕ
hp : Nat.Prime p
m : ℕ
hm0 : m ≠ 0
hpm : m + 2 ≤ p * m
a : ℤ
ha : ¬↑p ∣ a
n✝ n : ℕ
this : Fact (Nat.Prime p)
⊢ ↑p * ↑p ^ m * ↑p ∣ (↑p ^ m) ^ p

Tactic:
rw [← pow_succ', ← pow_succ, ← pow_mul, mul_comm]

Goal state after:
case refine_1
p : ℕ
hp : Nat.Prime p
m : ℕ
hm0 : m ≠ 0
hpm : m + 2 ≤ p * m
a : ℤ
ha : ¬↑p ∣ a
n✝ n : ℕ
this : Fact (Nat.Prime p)
⊢ ↑p ^ (m + 1 + 1) ∣ ↑p ^ (p * m)
Module: Mathlib.RingTheory.MvPowerSeries.Derivative

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
i : σ
f g : MvPolynomial σ R
⊢ pderivFun i (↑f * ↑g) = ↑f * ↑((pderiv i) g) + ↑g * ↑((pderiv i) f)

Tactic:
rw [← coe_mul, pderivFun_coe, pderiv_mul, add_comm, mul_comm _ g, ← coe_mul, ← coe_mul,
    MvPolynomial.coe_add]

Goal state after:
Module: Mathlib.RingTheory.PowerSeries.Derivative

Goal state before:
pp: case succ
R : Type u_1
inst✝ : CommSemiring R
f : R⟦X⟧
n : ℕ
ih : ∀ (k : ℕ), (coeff k) ((⇑(d⁄dX R))^[n] f) = ↑((k + 1).ascFactorial n) * (coeff (k + n)) f
k : ℕ
⊢ ↑((k + 1 + 1).ascFactorial n) * (coeff (k + 1 + n)) f * (↑k + 1) =
    ↑((k + 1 + n) * (k + 1).ascFactorial n) * (coeff (k + (n + 1))) f

Tactic:
← Nat.succ_ascFactorial

Goal state after:
case succ
R : Type u_1
inst✝ : CommSemiring R
f : R⟦X⟧
n : ℕ
ih : ∀ (k : ℕ), (coeff k) ((⇑(d⁄dX R))^[n] f) = ↑((k + 1).ascFactorial n) * (coeff (k + n)) f
k : ℕ
⊢ ↑((k + 1 + 1).ascFactorial n) * (coeff (k + 1 + n)) f * (↑k + 1) =
    ↑((k + 1) * (k + 1).succ.ascFactorial n) * (coeff (k + (n + 1))) f
Module: Mathlib.NumberTheory.AbelSummation

Goal state before:
pp: case inr.hbc
𝕜 : 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⌋₊
this :
  ∑ k ∈ Ioc ⌊a⌋₊ (⌊b⌋₊ - 1), (f ↑(k + 1) - f ↑k) * ∑ n ∈ Icc 0 k, c n =
    ∑ k ∈ Ico (⌊a⌋₊ + 1) ⌊b⌋₊, ∫ (t : ℝ) in ↑k..↑(k + 1), deriv f t * ∑ n ∈ Icc 0 ⌊t⌋₊, c n
⊢ IntervalIntegrable (fun x ↦ deriv f x * ∑ x ∈ Icc 0 ⌊x⌋₊, c x) volume (↑⌊b⌋₊) b

Tactic:
rw [intervalIntegrable_iff_integrableOn_Icc_of_le aux5]

Goal state after:
case inr.hbc
𝕜 : 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⌋₊
this :
  ∑ k ∈ Ioc ⌊a⌋₊ (⌊b⌋₊ - 1), (f ↑(k + 1) - f ↑k) * ∑ n ∈ Icc 0 k, c n =
    ∑ k ∈ Ico (⌊a⌋₊ + 1) ⌊b⌋₊, ∫ (t : ℝ) in ↑k..↑(k + 1), deriv f t * ∑ n ∈ Icc 0 ⌊t⌋₊, c n
⊢ IntegrableOn (fun x ↦ deriv f x * ∑ x ∈ Icc 0 ⌊x⌋₊, c x) (Set.Icc (↑⌊b⌋₊) b) volume
Module: Mathlib.NumberTheory.PrimeCounting

Goal state before:
pp: n : ℕ
⊢ n.primesBelow = filter Prime (Ico 1 n)

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

Goal state after:
Module: Mathlib.NumberTheory.BernoulliPolynomials

Goal state before:
pp: case succ
n d : ℕ
hd : ∀ m < d + 1, (bernoulli m).comp (1 + X) = bernoulli m + m • X ^ (m - 1)
⊢ (bernoulli (d + 1)).comp (1 + X) = bernoulli (d + 1) + (d + 1) • X ^ (d + 1 - 1)

Tactic:
rw [← smul_right_inj (show d + 2 ≠ 0 by positivity), ← smul_comp, smul_add]

Goal state after:
case succ
n d : ℕ
hd : ∀ m < d + 1, (bernoulli m).comp (1 + X) = bernoulli m + m • X ^ (m - 1)
⊢ ((d + 2) • bernoulli (d + 1)).comp (1 + X) = (d + 2) • bernoulli (d + 1) + (d + 2) • (d + 1) • X ^ (d + 1 - 1)
Module: Mathlib.NumberTheory.AbelSummation

Goal state before:
pp: case neg
𝕜 : 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
⊢ IntegrableOn (fun t ↦ g t * ∑ k ∈ Icc m ⌊t⌋₊, c k) K volume

Tactic:
rw [Set.not_nonempty_iff_eq_empty.mp hK₃]

Goal state after:
case neg
𝕜 : 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
⊢ IntegrableOn (fun t ↦ g t * ∑ k ∈ Icc m ⌊t⌋₊, c k) ∅ volume
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: p d : ℕ
inst✝ : Fact (Nat.Prime p)
hd : d ≥ 2
hcase : ¬(p = 2 ∧ d = 2)
hp2 : 2 ≤ p
n m : ℕ
hm : Nat.le 2 m
IH : ¬(p = 2 ∧ m = 2) → m + 1 ≤ p ^ (m - 1)
hne' : ¬(p = 2 ∧ m.succ = 2)
hm2 : ¬(p = 2 ∧ m = 2)
⊢ p ^ (m - 1 + 1 - 1) * p = p ^ (m - 1 + 1)

Tactic:
exact pow_succ ..

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

Goal state before:
pp: case pos
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Ring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
b : Fq[X]
A : Fin m.succ → Fq[X]
hA : ∀ (i : Fin m.succ), (A i).degree < b.degree
hb : b ≠ 0
f : Fin m.succ → Fin d → Fq := fun i j ↦ (A i).coeff (b.natDegree - ↑j.succ)
this : Fintype.card (Fin d → Fq) < Fintype.card (Fin m.succ)
i₀ i₁ : Fin m.succ
i_ne : i₀ ≠ i₁
i_eq : f i₀ = f i₁
j : ℕ
hj : b.natDegree - d ≤ j
hbj : b.degree ≤ ↑j
⊢ (A i₁ - A i₀).degree < b.degree

Tactic:
exact lt_of_le_of_lt (degree_sub_le _ _) (max_lt (hA _) (hA _))

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
⊢ ψ x = 0 ↔ x < 2

Tactic:
by
  refine ⟨fun h₀ ↦ ?_, psi_eq_zero_of_lt_two⟩
  by_contra! contra
  replace contra : 2 ∈ Ioc 0 ⌊x⌋₊ := by rw [mem_Ioc, le_floor_iff (by grind)]; grind
  have : Λ 2 ≤ ψ x := single_le_sum (fun n _ ↦ vonMangoldt_nonneg (n := n)) contra
  have := vonMangoldt_pos_iff.mpr prime_two.isPrimePow
  linarith

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: n : ℕ
⊢ n.lcmUpto = ∏ p ∈ n.primesLE, p ^ ⌊Real.log ↑n / Real.log ↑p⌋₊

Tactic:
lcmUpto_eq_prod_pow_log,

Goal state after:
n : ℕ
⊢ ∏ p ∈ n.primesLE, p ^ log p n = ∏ p ∈ n.primesLE, p ^ ⌊Real.log ↑n / Real.log ↑p⌋₊
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: n : ℕ
⊢ ψ ↑n = log ↑n.lcmUpto

Tactic:
lcmUpto_eq_prod_pow_log,

Goal state after:
n : ℕ
⊢ ψ ↑n = log ↑(∏ p ∈ n.primesLE, p ^ Nat.log p n)
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
m n : ℕ
hm : x - ↑m ∈ maximalIdeal ℤ_[p]
hn : x - ↑n ∈ maximalIdeal ℤ_[p]
⊢ ↑m = ↑n

Tactic:
rw [maximalIdeal_eq_span_p] at hm hn

Goal state after:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
m n : ℕ
hm : x - ↑m ∈ Ideal.span {↑p}
hn : x - ↑n ∈ Ideal.span {↑p}
⊢ ↑m = ↑n
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
N₁ N₂ N₃ N₅ N₇ : ℕ
N : ℕ := N₁ + N₂ + N₃ + N₅ + N₇
h7 : ψ (x ^ (↑7)⁻¹) = ∑ k ∈ Icc 1 N, b x (7 * k)
h5 : ψ (x ^ (↑5)⁻¹) = ∑ k ∈ Icc 1 N, b x (5 * k)
h3 : ψ (x ^ (↑3)⁻¹) = ∑ k ∈ Icc 1 (2 * N), b x (3 * k)
h2 : ψ (x ^ (↑2)⁻¹) = ∑ k ∈ Icc 1 (3 * N), b x (2 * k)
h1 : ψ (x ^ (↑1)⁻¹) = ∑ k ∈ Icc 1 (1 + 6 * N), b x (1 * k)
this : ∑ n ∈ Icc 1 N, c x n ≤ ∑ n ∈ Icc 1 N, b x (5 * n)
n : ℕ
hn : 1 ≤ n ∧ n ≤ N
⊢ b x (7 * n) ≤ b x (6 * n - 1) - b x (6 * n) + b x (6 * n + 1)

Tactic:
linarith [(b_antitone x hx (by grind) (by grind) (by lia) : b x (6 * n) ≤ b x (6 * n - 1)),
      (b_antitone x hx (by grind) (by grind) (by lia) : b x (7 * n) ≤ b x (6 * n + 1))]

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

Goal state before:
pp: case inr.mp
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
H : ‖↑x.zmodRepr‖ ≠ ‖x‖
this : ‖x - ↑x.zmodRepr‖ < 1
h : ‖↑x.zmodRepr‖ = 1
⊢ ‖x‖ = 1

Tactic:
rw [← h] at this ⊢

Goal state after:
case inr.mp
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
H : ‖↑x.zmodRepr‖ ≠ ‖x‖
this : ‖x - ↑x.zmodRepr‖ < ‖↑x.zmodRepr‖
h : ‖↑x.zmodRepr‖ = 1
⊢ ‖x‖ = ‖↑x.zmodRepr‖
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: case inr.mpr
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
H : ‖↑x.zmodRepr‖ ≠ ‖x‖
this : ‖x - ↑x.zmodRepr‖ < 1
h : ‖x‖ = 1
⊢ ‖↑x.zmodRepr‖ = 1

Tactic:
rw [← h] at this ⊢

Goal state after:
case inr.mpr
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
H : ‖↑x.zmodRepr‖ ≠ ‖x‖
this : ‖x - ↑x.zmodRepr‖ < ‖x‖
h : ‖x‖ = 1
⊢ ‖↑x.zmodRepr‖ = ‖x‖
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: case hy₂
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
⊢ ↑(n % p + p * (n / p)) - ↑(n % p) ∈ maximalIdeal ℤ_[p]

Tactic:
simp [maximalIdeal_eq_span_p, Ideal.mem_span_singleton]

Goal state after: