mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.PSeries

Goal state before:
pp: M : Type u_1
inst✝² : AddCommMonoid M
inst✝¹ : PartialOrder M
inst✝ : IsOrderedAddMonoid M
f : ℕ → M
u : ℕ → ℕ
C : ℕ
hf : ∀ ⦃m n : ℕ⦄, 1 < m → m ≤ n → f n ≤ f m
h_pos : ∀ (n : ℕ), 0 < u n
h_nonneg : ∀ (n : ℕ), 0 ≤ f n
hu : Monotone u
h_succ_diff : SuccDiffBounded C u
n : ℕ
⊢ ∀ k ∈ range n, (u (k + 2) - u (k + 1)) • f (u (k + 1)) ≤ C • (u (k + 1) - u k) • f (u (k + 1))

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.PSeries

Goal state before:
pp: M : Type u_1
inst✝² : AddCommMonoid M
inst✝¹ : PartialOrder M
inst✝ : IsOrderedAddMonoid M
f : ℕ → M
u : ℕ → ℕ
C : ℕ
hf : ∀ ⦃m n : ℕ⦄, 1 < m → m ≤ n → f n ≤ f m
h_pos : ∀ (n : ℕ), 0 < u n
h_nonneg : ∀ (n : ℕ), 0 ≤ f n
hu : Monotone u
h_succ_diff : SuccDiffBounded C u
n : ℕ
⊢ ∑ k ∈ range (n + 1), (u (k + 1) - u k) • f (u k) ≤ (u 1 - u 0) • f (u 0) + C • ∑ k ∈ Ico (u 0 + 1) (u n + 1), f k

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Asymptotics.SpecificAsymptotics

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
u : ℕ → E
l : E
h : Tendsto u atTop (𝓝 l)
⊢ Tendsto (fun n ↦ (↑n)⁻¹ • ∑ i ∈ Finset.range n, u i) atTop (𝓝 l)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.PSeries

Goal state before:
pp: M : Type u_1
inst✝² : AddCommMonoid M
inst✝¹ : PartialOrder M
inst✝ : IsOrderedAddMonoid M
f : ℕ → M
hf : ∀ ⦃m n : ℕ⦄, 1 < m → m ≤ n → f n ≤ f m
n : ℕ
⊢ ∑ k ∈ range (n + 1), 2 ^ k • f (2 ^ k) ≤ f 1 + 2 • ∑ k ∈ Ico 2 (2 ^ n + 1), f k

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.PSeries

Goal state before:
pp: u : ℕ → ℕ
f : ℕ → ℝ≥0∞
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
h_pos : ∀ (n : ℕ), 0 < u n
hu : StrictMono u
n k : ℕ
⊢ ↑(u (k + 1)) - ↑(u k) = ↑(u (k + 1) - u k)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.PSeries

Goal state before:
pp: u : ℕ → ℕ
f : ℕ → ℝ≥0∞
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
h_pos : ∀ (n : ℕ), 0 < u n
hu : StrictMono u
⊢ ∑' (k : ℕ), f k ≤ ∑ k ∈ range (u 0), f k + ∑' (k : ℕ), (↑(u (k + 1)) - ↑(u k)) * f (u k)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.PSeries

Goal state before:
pp: f : ℕ → ℝ≥0∞
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
⊢ ∑' (k : ℕ), f k ≤ f 0 + ∑' (k : ℕ), 2 ^ k * f (2 ^ k)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.ZLattice.Covolume

Goal state before:
pp: E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
L : Submodule ℤ E
inst✝⁵ : DiscreteTopology ↥L
inst✝⁴ : IsZLattice ℝ L
ι : Type u_2
inst✝³ : Fintype ι
b : Basis ι ℤ ↥L
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
s : Set E
hs₁ : Bornology.IsBounded s
hs₂ : MeasurableSet s
hs₃ : volume (frontier (⇑(Basis.ofZLatticeBasis ℝ L b).equivFun '' s)) = 0
⊢ Tendsto (fun n ↦ ↑(Nat.card ↑(s ∩ (↑n)⁻¹ • ↑L)) / ↑n ^ card ι) atTop
    (𝓝 (volume.real (⇑(Basis.ofZLatticeBasis ℝ L b).equivFun '' s)))

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.PSeries

Goal state before:
pp: u : ℕ → ℕ
f : ℕ → ℝ≥0∞
C : ℕ
hf : ∀ ⦃m n : ℕ⦄, 1 < m → m ≤ n → f n ≤ f m
h_pos : ∀ (n : ℕ), 0 < u n
h_nonneg : ∀ (n : ℕ), 0 ≤ f n
hu : Monotone u
h_succ_diff : SuccDiffBounded C u
⊢ ∑' (k : ℕ), (↑(u (k + 1)) - ↑(u k)) * f (u k) ≤ (↑(u 1) - ↑(u 0)) * f (u 0) + ↑C * ∑' (k : ℕ), f k

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.ZLattice.Covolume

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
ι : Type u_2
inst✝ : Fintype ι
X : Set E
hX : ∀ ⦃x : E⦄ ⦃r : ℝ⦄, x ∈ X → 0 < r → r • x ∈ X
F : E → ℝ
hF₁ : ∀ (x : E) ⦃r : ℝ⦄, 0 ≤ r → F (r • x) = r ^ card ι * F x
c : ℝ
hc : 0 < c
⊢ c • {x | x ∈ X ∧ F x ≤ 1} = {x | x ∈ X ∧ F x ≤ c ^ card ι}

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.PSeries

Goal state before:
pp: f : ℕ → ℝ≥0∞
hf : ∀ ⦃m n : ℕ⦄, 1 < m → m ≤ n → f n ≤ f m
⊢ ∑' (k : ℕ), 2 ^ k * f (2 ^ k) ≤ f 1 + 2 * ∑' (k : ℕ), f k

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.PSeries

Goal state before:
pp: C : ℕ
u : ℕ → ℕ
f : ℕ → ℝ≥0
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
h_pos : ∀ (n : ℕ), 0 < u n
hu_strict : StrictMono u
hC_nonzero : C ≠ 0
h_succ_diff : SuccDiffBounded C u
⊢ (Summable fun k ↦ (↑(u (k + 1)) - ↑(u k)) * f (u k)) ↔ Summable f

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.PSeries

Goal state before:
pp: f : ℕ → ℝ≥0
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
⊢ SuccDiffBounded 2 fun x ↦ 2 ^ x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.PSeries

Goal state before:
pp: f : ℕ → ℝ≥0
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
⊢ (Summable fun k ↦ 2 ^ k * f (2 ^ k)) ↔ Summable f

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.PSeries

Goal state before:
pp: C : ℕ
u : ℕ → ℕ
h_pos : ∀ (n : ℕ), 0 < u n
hu_strict : StrictMono u
hC_nonzero : C ≠ 0
h_succ_diff : SuccDiffBounded C u
f : ℕ → ℝ≥0
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
k : ℕ
⊢ ↑(u (k + 1)) - ↑(u k) = ↑(↑(u (k + 1)) - ↑(u k))

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.PSeries

Goal state before:
pp: C : ℕ
u : ℕ → ℕ
f : ℕ → ℝ
h_nonneg : ∀ (n : ℕ), 0 ≤ f n
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
h_pos : ∀ (n : ℕ), 0 < u n
hu_strict : StrictMono u
hC_nonzero : C ≠ 0
h_succ_diff : SuccDiffBounded C u
⊢ (Summable fun k ↦ (↑(u (k + 1)) - ↑(u k)) * f (u k)) ↔ Summable f

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.PSeries

Goal state before:
pp: f : ℕ → ℝ
h_nonneg : ∀ (n : ℕ), 0 ≤ f n
h_mono : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
⊢ SuccDiffBounded 2 fun x ↦ 2 ^ x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.PSeries

Goal state before:
pp: f : ℕ → ℝ
h_nonneg : ∀ (n : ℕ), 0 ≤ f n
h_mono : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
⊢ (Summable fun k ↦ 2 ^ k * f (2 ^ k)) ↔ Summable f

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.PSeries

Goal state before:
pp: f : ℕ → ℝ
n : ℕ
hn : ∀ (b : ℕ), n ≤ b → 0 b ≤ f b
m : ℕ
hm : ∀ (b : ℕ), m ≤ b → f (b + 1) ≤ f b
⊢ 1 < 2

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.PSeries

Goal state before:
pp: f : ℕ → ℝ
n : ℕ
hn : ∀ (b : ℕ), n ≤ b → 0 b ≤ f b
m : ℕ
hm : ∀ (b : ℕ), m ≤ b → f (b + 1) ≤ f b
h_pow : Filter.Tendsto (fun n ↦ 2 ^ n) Filter.atTop Filter.atTop
a✝ : ℕ
hk : n + m ≤ 2 ^ a✝
⊢ 2 ^ a✝ * f (2 ^ a✝) = 2 ^ a✝ * f (max (2 ^ a✝) (n + m))

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.PSeries

Goal state before:
pp: f : ℕ → ℝ
n : ℕ
hn : ∀ (b : ℕ), n ≤ b → 0 b ≤ f b
m : ℕ
hm : ∀ (b : ℕ), m ≤ b → f (b + 1) ≤ f b
a✝ : ℕ
hk : n + m ≤ a✝
⊢ f a✝ = f (max a✝ (n + m))

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.PSeries

Goal state before:
pp: f : ℕ → ℝ
n : ℕ
hn : ∀ (b : ℕ), n ≤ b → 0 b ≤ f b
m : ℕ
hm : ∀ (b : ℕ), m ≤ b → f (b + 1) ≤ f b
m✝ n✝ : ℕ
a✝¹ : 0 < m✝
a✝ : m✝ ≤ n✝
⊢ ∀ n_1 ≥ n + m, f (n_1 + 1) ≤ f n_1

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.PSeries

Goal state before:
pp: f : ℕ → ℝ
n : ℕ
hn : ∀ (b : ℕ), n ≤ b → 0 b ≤ f b
m : ℕ
hm : ∀ (b : ℕ), m ≤ b → f (b + 1) ≤ f b
m✝ n✝ : ℕ
a✝¹ : 0 < m✝
a✝ : m✝ ≤ n✝
⊢ max m✝ (n + m) ∈ {x | n + m ≤ x}

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.PSeries

Goal state before:
pp: f : ℕ → ℝ
n : ℕ
hn : ∀ (b : ℕ), n ≤ b → 0 b ≤ f b
m : ℕ
hm : ∀ (b : ℕ), m ≤ b → f (b + 1) ≤ f b
m✝ n✝ : ℕ
a✝¹ : 0 < m✝
a✝ : m✝ ≤ n✝
⊢ max n✝ (n + m) ∈ {x | n + m ≤ x}

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.PSeries

Goal state before:
pp: f : ℕ → ℝ
n : ℕ
hn : ∀ (b : ℕ), n ≤ b → 0 b ≤ f b
m : ℕ
hm : ∀ (b : ℕ), m ≤ b → f (b + 1) ≤ f b
m✝ n✝ : ℕ
a✝¹ : 0 < m✝
a✝ : m✝ ≤ n✝
⊢ max m✝ (n + m) ≤ max n✝ (n + m)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.PSeries

Goal state before:
pp: f : ℕ → ℝ
h_nonneg : 0 ≤ᶠ[Filter.atTop] f
h_mono : ∀ᶠ (k : ℕ) in Filter.atTop, f (k + 1) ≤ f k
⊢ (Summable fun k ↦ 2 ^ k * f (2 ^ k)) ↔ Summable f

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Asymptotics.SpecificAsymptotics

Goal state before:
pp: E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
D : Type u_2
inst✝ : TopologicalSpace D
f : D → E
hf : Continuous[inst✝, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
⊢ Bornology.IsBounded (range f) ↔ f =O[cocompact D] 1

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.PSeries

Goal state before:
pp: p : ℝ
hp : p < 0
this : ¬Summable fun n ↦ (↑n ^ p)⁻¹
⊢ (Summable fun n ↦ (↑n ^ p)⁻¹) ↔ 1 < p

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Asymptotics.SpecificAsymptotics

Goal state before:
pp: E : Type u_1
inst✝⁶ : SeminormedAddCommGroup E
β : Type u_3
inst✝⁵ : TopologicalSpace β
inst✝⁴ : LinearOrder β
inst✝³ : OrderClosedTopology β
inst✝² : CompactIccSpace β
inst✝¹ : NoMaxOrder β
inst✝ : NoMinOrder β
f : β → E
hf : Continuous[inst✝⁵, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
⊢ Bornology.IsBounded (range f) ↔ f =O[atTop] 1 ∧ f =O[atBot] 1

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.PSeries

Goal state before:
pp: p : ℝ
⊢ (Summable fun n ↦ (↑n ^ p)⁻¹) ↔ 1 < p

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.PSeries

Goal state before:
pp: p : ℝ
⊢ (Summable fun n ↦ ↑n ^ p) ↔ p < -1

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.PSeries

Goal state before:
pp: p : ℝ
⊢ (Summable fun n ↦ 1 / ↑n ^ p) ↔ 1 < p

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.PSeries

Goal state before:
pp: p : ℕ
⊢ (Summable fun n ↦ (↑n ^ p)⁻¹) ↔ 1 < p

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.PSeries

Goal state before:
pp: p : ℕ
⊢ (Summable fun n ↦ 1 / ↑n ^ p) ↔ 1 < p

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Asymptotics.SpecificAsymptotics

Goal state before:
pp: E : Type u_1
inst✝⁸ : SeminormedAddCommGroup E
β : Type u_3
inst✝⁷ : TopologicalSpace β
inst✝⁶ : LinearOrder β
inst✝⁵ : OrderClosedTopology β
inst✝⁴ : CompactIccSpace β
inst✝³ : NoMaxOrder β
inst✝² : NoMinOrder β
inst✝¹ : AddCommGroup β
inst✝ : IsOrderedAddMonoid β
f : β → E
hf : Continuous[inst✝⁷, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
heven : Function.Even f
h : f =O[atTop] 1
⊢ f =O[atBot] 1

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.PSeries

Goal state before:
pp: b : ℝ
hb : 1 < b
⊢ Summable fun n ↦ |↑n| ^ (-b)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.PSeries

Goal state before:
pp: ⊢ ¬Summable fun n ↦ (↑n)⁻¹

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.PSeries

Goal state before:
pp: ⊢ ¬Summable fun n ↦ 1 / ↑n

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.PSeries

Goal state before:
pp: i : ℕ
⊢ 0 ≤ 1 / (↑i + 1)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.PSeries

Goal state before:
pp: ⊢ Tendsto (fun n ↦ ∑ i ∈ Finset.range n, 1 / (↑i + 1)) atTop atTop

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.BoxIntegral.Basic

Goal state before:
pp: ι : Type u
E : Type v
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : Fintype ι
l : IntegrationParams
inst✝¹ : CompleteSpace E
I : Box ι
f : (ι → ℝ) → E
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
hc : ∀ᵐ (x : ι → ℝ) ∂μ.restrict (Box.Icc I), ContinuousWithinAt f (Box.Icc I) x
ε : ℝ
ε0 : ε > 0
ε₁ : ℝ
ε₁0 : 0 < ε₁
hε₁ : 2 * μ.toBoxAdditive I * ε₁ < ε
C : ℝ
hC : ∀ x ∈ Box.Icc I, ‖f x‖ ≤ C
C0 : 0 ≤ C
ε₂ : ℝ
ε₂0 : 0 < ε₂
hε₂ : 4 * C * ε₂ < ε
ε₂0' : ENNReal.ofReal ε₂ ≠ 0
D : Set (ι → ℝ) := {x | x ∈ Box.Icc I ∧ ¬ContinuousWithinAt f (Box.Icc I) x}
μ' : Measure (ι → ℝ) := μ.restrict (Box.Icc I)
μ'D : μ' D = 0
U : Set (ι → ℝ)
UD : U ⊇ D
Uopen : IsOpen U
hU : μ' U < ENNReal.ofReal ε₂
comp : IsCompact (Box.Icc I \ U)
this : ∀ x ∈ Box.Icc I \ U, oscillationWithin f (Box.Icc I) x < ENNReal.ofReal ε₁
r : ℝ
r0 : r > 0
hr : ∀ x ∈ Box.Icc I \ U, ediam (f '' (eball x (ENNReal.ofReal r) ∩ Box.Icc I)) ≤ ENNReal.ofReal ε₁
c₁ c₂ : ℝ≥0
π₁ π₂ : TaggedPrepartition I
h₁ : l.MemBaseSet I c₁ ((fun x x_1 ↦ ⟨r / 2, ⋯⟩) c₁) π₁
h₁p : π₁.IsPartition
h₂ : l.MemBaseSet I c₂ ((fun x x_1 ↦ ⟨r / 2, ⋯⟩) c₂) π₂
h₂p : π₂.IsPartition
μI : μ ↑I < ∞
t₁ : Box ι → ι → ℝ := fun J ↦ (π₁.infPrepartition π₂.toPrepartition).tag J
t₂ : Box ι → ι → ℝ := fun J ↦ (π₂.infPrepartition π₁.toPrepartition).tag J
B : Finset (Box ι) := (π₁.toPrepartition ⊓ π₂.toPrepartition).boxes
B' : Finset (Box ι) := {J ∈ B | ↑J ⊆ U}
hB' : B' ⊆ B
μJ_ne_top : ∀ J ∈ B, μ ↑J ≠ ∞
un : ∀ S ⊆ B, ⋃ J ∈ S, ↑J ⊆ ↑I
J : Box ι
hJ : J ∈ B ∧ (J ∈ B → ¬↑J ⊆ U)
x : ι → ℝ
xJ : x ∈ J
xnU : x ∉ U
hx : x ∈ Box.Icc I \ U
⊢ edist (f (t₁ J)) (f (t₂ J)) ≤ ediam (f '' (Metric.ball x r ∩ Box.Icc I))

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.PSeries

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
k n✝ : ℕ
hk : k ≠ 0
h : k ≤ n✝
n : ℕ
hn : k ≤ n
IH : ∑ i ∈ Ioc k n, (↑i ^ 2)⁻¹ ≤ (↑k)⁻¹ - (↑n)⁻¹
⊢ 0 < ↑n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.ZLattice.Summable

Goal state before:
pp: E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : FiniteDimensional ℝ E
L : Submodule ℤ E
inst✝ : DiscreteTopology ↥L
ι : Type u_2
b : Basis ι ℤ ↥L
this :
  ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [FiniteDimensional ℝ E] {L : Submodule ℤ E}
    [inst_3 : DiscreteTopology ↥L] {ι : Type u_2} (b : Basis ι ℤ ↥L),
    IsZLattice ℝ L → ∃ ε, 0 < ε ∧ ∀ (x : ↥L) (i : ι), ε * ↑|(b.repr x) i| ≤ ‖x‖
H : ¬IsZLattice ℝ L
E' : Submodule ℝ E := Submodule.span ℝ ↑L
L' : Submodule ℤ ↥E' := ZLattice.comap ℝ L E'.subtype
⊢ Continuous ⇑E'.subtype

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.PSeries

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
k n : ℕ
hk : k ≠ 0
h : k ≤ n
⊢ ∑ i ∈ Ioc k n, (↑i ^ 2)⁻¹ ≤ (↑k)⁻¹ - (↑n)⁻¹

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.ZLattice.Summable

Goal state before:
pp: E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : FiniteDimensional ℝ E
L : Submodule ℤ E
inst✝ : DiscreteTopology ↥L
ι : Type u_2
b : Basis ι ℤ ↥L
this :
  ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [FiniteDimensional ℝ E] {L : Submodule ℤ E}
    [inst_3 : DiscreteTopology ↥L] {ι : Type u_2} (b : Basis ι ℤ ↥L),
    IsZLattice ℝ L → ∃ ε, 0 < ε ∧ ∀ (x : ↥L) (i : ι), ε * ↑|(b.repr x) i| ≤ ‖x‖
H : ¬IsZLattice ℝ L
E' : Submodule ℝ E := Submodule.span ℝ ↑L
L' : Submodule ℤ ↥E' := ZLattice.comap ℝ L E'.subtype
inst : DiscreteTopology ↥L'
e : ↥L' ≃ₗ[ℤ] ↥L := Submodule.comapSubtypeEquivOfLe ⋯
⊢ Submodule.map E'.subtype (Submodule.span ℝ ↑L') = Submodule.map E'.subtype ⊤

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.PSeries

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
k n : ℕ
⊢ ∑ i ∈ Ioo k n, (↑i ^ 2)⁻¹ ≤ ∑ i ∈ Ioc k (max (k + 1) n), (↑i ^ 2)⁻¹

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.ZLattice.Summable

Goal state before:
pp: E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
L : Submodule ℤ E
inst✝¹ : DiscreteTopology ↥L
ι : Type u_2
b : Basis ι ℤ ↥L
this :
  ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [FiniteDimensional ℝ E] {L : Submodule ℤ E}
    [inst_3 : DiscreteTopology ↥L] {ι : Type u_2} (b : Basis ι ℤ ↥L),
    IsZLattice ℝ L → ∃ ε, 0 < ε ∧ ∀ (x : ↥L) (i : ι), ε * ↑|(b.repr x) i| ≤ ‖x‖
H✝ : ¬IsZLattice ℝ L
E' : Submodule ℝ E := Submodule.span ℝ ↑L
L' : Submodule ℤ ↥E' := ZLattice.comap ℝ L E'.subtype
inst✝ : DiscreteTopology ↥L'
e : ↥L' ≃ₗ[ℤ] ↥L := Submodule.comapSubtypeEquivOfLe ⋯
inst : IsZLattice ℝ L'
ε : ℝ
hε : 0 < ε
H : ∀ (x : ↥L') (i : ι), ε * ↑|((b.map e.symm).repr x) i| ≤ ‖x‖
x : ↥L
i : ι
⊢ ε * ↑|(b.repr x) i| ≤ ‖x‖

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.ZLattice.Summable

Goal state before:
pp: E✝ : Type u_1
inst✝⁴ : NormedAddCommGroup E✝
L✝ : Submodule ℤ E✝
ι✝ : Type u_2
b✝ : Basis ι✝ ℤ ↥L✝
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : FiniteDimensional ℝ E
L : Submodule ℤ E
inst✝ : DiscreteTopology ↥L
ι : Type u_2
b : Basis ι ℤ ↥L
H : IsZLattice ℝ L
this✝ : Finite ι
b' : Basis ι ℝ E := Basis.ofZLatticeBasis ℝ L b
e : E ≃L[ℝ] ι → ℝ := (b'.repr ≪≫ₗ Finsupp.linearEquivFunOnFinite ℝ ℝ ι).toContinuousLinearEquiv
this : IsOpen (⇑e ⁻¹' Set.univ.pi fun x ↦ Set.Ioo (-1) 1)
⊢ 0 ∈ ⇑e ⁻¹' Set.univ.pi fun x ↦ Set.Ioo (-1) 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.ZLattice.Summable

Goal state before:
pp: E✝ : Type u_1
inst✝⁴ : NormedAddCommGroup E✝
L✝ : Submodule ℤ E✝
ι✝ : Type u_2
b✝ : Basis ι✝ ℤ ↥L✝
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : FiniteDimensional ℝ E
L : Submodule ℤ E
inst✝ : DiscreteTopology ↥L
ι : Type u_2
b : Basis ι ℤ ↥L
H : IsZLattice ℝ L
this✝ : Finite ι
b' : Basis ι ℝ E := Basis.ofZLatticeBasis ℝ L b
e : E ≃L[ℝ] ι → ℝ := (b'.repr ≪≫ₗ Finsupp.linearEquivFunOnFinite ℝ ℝ ι).toContinuousLinearEquiv
this : IsOpen (⇑e ⁻¹' Set.univ.pi fun x ↦ Set.Ioo (-1) 1)
ε : ℝ
hε : ε > 0
hε' : Metric.ball 0 ε ⊆ ⇑e ⁻¹' Set.univ.pi fun x ↦ Set.Ioo (-1) 1
⊢ 0 < ε / 2

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.PSeries

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
k n : ℕ
⊢ ∑ i ∈ Ioc k (max (k + 1) n), (↑i ^ 2)⁻¹ ≤ ((↑k + 1) ^ 2)⁻¹ + ∑ i ∈ Ioc k.succ (max (k + 1) n), (↑i ^ 2)⁻¹

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.PSeries

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
k n : ℕ
⊢ ((↑k + 1) ^ 2)⁻¹ + ∑ i ∈ Ioc k.succ (max (k + 1) n), (↑i ^ 2)⁻¹ ≤ ((↑k + 1) ^ 2)⁻¹ + (↑k + 1)⁻¹

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.PSeries

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
k n : ℕ
⊢ 1 ≤ ↑k + 1

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.PSeries

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
k n : ℕ
⊢ ((↑k + 1) ^ 2)⁻¹ + (↑k + 1)⁻¹ ≤ 1 / (↑k + 1) + 1 / (↑k + 1)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.PSeries

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
k n : ℕ
⊢ 1 / (↑k + 1) + 1 / (↑k + 1) = 2 / (↑k + 1)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.PSeries

Goal state before:
pp: m : ℕ
hm : m ≠ 0
k : ZMod m
this : NeZero m
n : ℕ
⊢ {n | ↑n = k - 1}.indicator (fun n ↦ 1 / ↑(n + 1)) n = if ↑n = k - 1 then 1 / (↑n + 1) else 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.BoxIntegral.Basic

Goal state before:
pp: ι : Type u
E : Type v
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : Fintype ι
l : IntegrationParams
inst✝¹ : CompleteSpace E
I : Box ι
f : (ι → ℝ) → E
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
hc : ∀ᵐ (x : ι → ℝ) ∂μ.restrict (Box.Icc I), ContinuousWithinAt f (Box.Icc I) x
ε : ℝ
ε0 : ε > 0
ε₁ : ℝ
ε₁0 : 0 < ε₁
hε₁ : 2 * μ.toBoxAdditive I * ε₁ < ε
C : ℝ
hC : ∀ x ∈ Box.Icc I, ‖f x‖ ≤ C
C0 : 0 ≤ C
ε₂ : ℝ
ε₂0 : 0 < ε₂
hε₂ : 4 * C * ε₂ < ε
ε₂0' : ENNReal.ofReal ε₂ ≠ 0
D : Set (ι → ℝ) := {x | x ∈ Box.Icc I ∧ ¬ContinuousWithinAt f (Box.Icc I) x}
μ' : Measure (ι → ℝ) := μ.restrict (Box.Icc I)
μ'D : μ' D = 0
U : Set (ι → ℝ)
UD : U ⊇ D
Uopen : IsOpen U
hU : μ' U < ENNReal.ofReal ε₂
comp : IsCompact (Box.Icc I \ U)
this : ∀ x ∈ Box.Icc I \ U, oscillationWithin f (Box.Icc I) x < ENNReal.ofReal ε₁
r : ℝ
r0 : r > 0
hr : ∀ x ∈ Box.Icc I \ U, ediam (f '' (eball x (ENNReal.ofReal r) ∩ Box.Icc I)) ≤ ENNReal.ofReal ε₁
c₁ c₂ : ℝ≥0
π₁ π₂ : TaggedPrepartition I
h₁ : l.MemBaseSet I c₁ ((fun x x_1 ↦ ⟨r / 2, ⋯⟩) c₁) π₁
h₁p : π₁.IsPartition
h₂ : l.MemBaseSet I c₂ ((fun x x_1 ↦ ⟨r / 2, ⋯⟩) c₂) π₂
h₂p : π₂.IsPartition
μI : μ ↑I < ∞
t₁ : Box ι → ι → ℝ := fun J ↦ (π₁.infPrepartition π₂.toPrepartition).tag J
t₂ : Box ι → ι → ℝ := fun J ↦ (π₂.infPrepartition π₁.toPrepartition).tag J
B : Finset (Box ι) := (π₁.toPrepartition ⊓ π₂.toPrepartition).boxes
B' : Finset (Box ι) := {J ∈ B | ↑J ⊆ U}
hB' : B' ⊆ B
μJ_ne_top : ∀ J ∈ B, μ ↑J ≠ ∞
un : ∀ S ⊆ B, ⋃ J ∈ S, ↑J ⊆ ↑I
⊢ ∀ J ∈ B \ B', ‖μ.toBoxAdditive J • (f (t₁ J) - f (t₂ J))‖ ≤ μ.toBoxAdditive J * ε₁

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.ZLattice.Summable

Goal state before:
pp: E✝ : Type u_1
inst✝⁴ : NormedAddCommGroup E✝
L✝ : Submodule ℤ E✝
ι✝ : Type u_2
b✝ : Basis ι✝ ℤ ↥L✝
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : FiniteDimensional ℝ E
L : Submodule ℤ E
inst✝ : DiscreteTopology ↥L
ι : Type u_2
b : Basis ι ℤ ↥L
H : IsZLattice ℝ L
this✝ : Finite ι
b' : Basis ι ℝ E := Basis.ofZLatticeBasis ℝ L b
e : E ≃L[ℝ] ι → ℝ := (b'.repr ≪≫ₗ Finsupp.linearEquivFunOnFinite ℝ ℝ ι).toContinuousLinearEquiv
this : IsOpen (⇑e ⁻¹' Set.univ.pi fun x ↦ Set.Ioo (-1) 1)
ε : ℝ
hε : ε > 0
hε' : Metric.ball 0 ε ⊆ ⇑e ⁻¹' Set.univ.pi fun x ↦ Set.Ioo (-1) 1
x : ↥L
i : ι
hx : ¬x = 0
⊢ ‖↑x‖ ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.ZLattice.Summable

Goal state before:
pp: E✝ : Type u_1
inst✝⁴ : NormedAddCommGroup E✝
L✝ : Submodule ℤ E✝
ι✝ : Type u_2
b✝ : Basis ι✝ ℤ ↥L✝
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : FiniteDimensional ℝ E
L : Submodule ℤ E
inst✝ : DiscreteTopology ↥L
ι : Type u_2
b : Basis ι ℤ ↥L
H : IsZLattice ℝ L
this✝ : Finite ι
b' : Basis ι ℝ E := Basis.ofZLatticeBasis ℝ L b
e : E ≃L[ℝ] ι → ℝ := (b'.repr ≪≫ₗ Finsupp.linearEquivFunOnFinite ℝ ℝ ι).toContinuousLinearEquiv
this : IsOpen (⇑e ⁻¹' Set.univ.pi fun x ↦ Set.Ioo (-1) 1)
ε : ℝ
hε : ε > 0
hε' : Metric.ball 0 ε ⊆ ⇑e ⁻¹' Set.univ.pi fun x ↦ Set.Ioo (-1) 1
x : ↥L
i : ι
hx✝ : ¬x = 0
hx : ‖↑x‖ ≠ 0
⊢ (ε / 2) • ‖x‖⁻¹ • ↑x ∈ Metric.ball 0 ε

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.PSeries

Goal state before:
pp: m : ℕ
hm : m ≠ 0
k : ZMod m
this : NeZero m
h✝ : ∀ (n : ℕ), {n | ↑n = k - 1}.indicator (fun n ↦ 1 / ↑(n + 1)) n = if ↑n = k - 1 then 1 / (↑n + 1) else 0
n₁ n₂ : ℕ
h : n₁ ≤ n₂
⊢ 1 / ↑(n₂ + 1) ≤ 1 / ↑(n₁ + 1)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.ZLattice.Summable

Goal state before:
pp: E✝ : Type u_1
inst✝⁴ : NormedAddCommGroup E✝
L✝ : Submodule ℤ E✝
ι✝ : Type u_2
b✝ : Basis ι✝ ℤ ↥L✝
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : FiniteDimensional ℝ E
L : Submodule ℤ E
inst✝ : DiscreteTopology ↥L
ι : Type u_2
b : Basis ι ℤ ↥L
H : IsZLattice ℝ L
this✝ : Finite ι
b' : Basis ι ℝ E := Basis.ofZLatticeBasis ℝ L b
e : E ≃L[ℝ] ι → ℝ := (b'.repr ≪≫ₗ Finsupp.linearEquivFunOnFinite ℝ ℝ ι).toContinuousLinearEquiv
this : IsOpen (⇑e ⁻¹' Set.univ.pi fun x ↦ Set.Ioo (-1) 1)
ε : ℝ
hε : ε > 0
hε' : Metric.ball 0 ε ⊆ ⇑e ⁻¹' Set.univ.pi fun x ↦ Set.Ioo (-1) 1
x : ↥L
i : ι
hx✝ : ¬x = 0
hx : ‖↑x‖ ≠ 0
⊢ |ε / 2 * (‖x‖⁻¹ * ↑((b.repr x) i))| < 1

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.PSeries

Goal state before:
pp: m : ℕ
hm : m ≠ 0
k : ZMod m
⊢ ¬Summable ({n | ↑n = k}.indicator fun n ↦ 1 / ↑n)

Tactic:
have : NeZero m := ⟨hm⟩ -- instance is needed below
  rw [← summable_nat_add_iff 1] -- shift by one to avoid non-monotonicity at zero
  have h (n : ℕ) : {n : ℕ | (n : ZMod m) = k - 1}.indicator (fun n : ℕ ↦ (1 / (n + 1 :) : ℝ)) n =
      if (n : ZMod m) = k - 1 then (1 / (n + 1) : ℝ) else (0 : ℝ) := by
    simp only [indicator_apply, mem_ofPred_eq, cast_add, cast_one]
  simp_rw [indicator_apply, mem_ofPred, cast_add, cast_one, ← eq_sub_iff_add_eq, ← h]
  rw [summable_indicator_mod_iff (fun n₁ n₂ h ↦ by gcongr) (k - 1)]
  exact mt (summable_nat_add_iff (f := fun n : ℕ ↦ 1 / (n : ℝ)) 1).mp not_summable_one_div_natCast

Goal state after:
Module: Mathlib.Analysis.PSeries

Goal state before:
pp: m : ℕ
hm : m ≠ 0
k : ZMod m
⊢ ¬Summable ({n | ↑n = k}.indicator fun n ↦ 1 / ↑n)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.PSeries

Goal state before:
pp: a s : ℝ
⊢ Nat.cast =ᶠ[atTop] fun n ↦ ‖↑n‖

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.PSeries

Goal state before:
pp: a s : ℝ
hnorm : Tendsto (fun n ↦ ‖↑n‖) atTop atTop
⊢ (fun n ↦ |↑n + a|) ~[atTop] fun x ↦ ↑x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.PSeries

Goal state before:
pp: a s : ℝ
hnorm : Tendsto (fun n ↦ ‖↑n‖) atTop atTop
h_abs : (fun n ↦ |↑n + a|) ~[atTop] fun x ↦ ↑x
n : ℕ
⊢ 0 n ≤ ↑n

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.PSeries

Goal state before:
pp: a s : ℝ
⊢ (Summable fun n ↦ 1 / |↑n + a| ^ s) ↔ 1 < s

Tactic:
by

Goal state after: