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

Goal state before:
pp: case refine_1
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
s : Set (ι → ℝ)
F : (ι → ℝ) → ℝ
inst✝ : Fintype ι
B : Box ι
hB : hasIntegralVertices B
hs₀ : s ⊆ ↑B
this : Fintype ↑(s ∩ (↑n)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))))
x✝ : ι → ℝ
hx : x✝ ∈ s ∩ (↑n)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι)))
⊢ (prepartition n B).tag (box n (index n x✝)) ∈ s

Tactic:
[

Goal state after:
case refine_1
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
s : Set (ι → ℝ)
F : (ι → ℝ) → ℝ
inst✝ : Fintype ι
B : Box ι
hB : hasIntegralVertices B
hs₀ : s ⊆ ↑B
this : Fintype ↑(s ∩ (↑n)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))))
x✝ : ι → ℝ
hx : x✝ ∈ s ∩ (↑n)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι)))
⊢ (prepartition n B).tag (box n (index n x✝)) ∈ s
Module: Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : WellFoundedLT ι
f : ι → E
i j : ι
hij : i ≤ j
⊢ gramSchmidt 𝕜 f i + ∑ i_1 < i, (𝕜 ∙ gramSchmidt 𝕜 f i_1).starProjection (f i) ∈ span 𝕜 (gramSchmidt 𝕜 f '' Set.Iic j)

Tactic:
[

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : WellFoundedLT ι
f : ι → E
i j : ι
hij : i ≤ j
⊢ gramSchmidt 𝕜 f i + ∑ i_1 < i, (𝕜 ∙ gramSchmidt 𝕜 f i_1).starProjection (f i) ∈ span 𝕜 (gramSchmidt 𝕜 f '' Set.Iic j)
Module: Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : WellFoundedLT ι
f : ι → E
j i : ι
hij : i ≤ j
⊢ f i - ∑ i_1 < i, (𝕜 ∙ gramSchmidt 𝕜 f i_1).starProjection (f i) ∈ span 𝕜 (f '' Set.Iic j)

Tactic:
[

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : WellFoundedLT ι
f : ι → E
j i : ι
hij : i ≤ j
⊢ f i - ∑ i_1 < i, (𝕜 ∙ gramSchmidt 𝕜 f i_1).starProjection (f i) ∈ span 𝕜 (f '' Set.Iic j)
Module: Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : WellFoundedLT ι
f : ι → E
h₀ : LinearIndependent 𝕜 f
⊢ LinearIndependent 𝕜 fun n ↦ (↑‖gramSchmidt 𝕜 f n‖)⁻¹ • gramSchmidt 𝕜 f n

Tactic:
have (i : ι) : IsUnit (‖gramSchmidt 𝕜 f i‖⁻¹ : 𝕜) :=
    isUnit_iff_ne_zero.mpr (by simp [gramSchmidt_ne_zero i h₀])

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : WellFoundedLT ι
f : ι → E
h₀ : LinearIndependent 𝕜 f
this : ∀ (i : ι), IsUnit (↑‖gramSchmidt 𝕜 f i‖)⁻¹
⊢ LinearIndependent 𝕜 fun n ↦ (↑‖gramSchmidt 𝕜 f n‖)⁻¹ • gramSchmidt 𝕜 f n
Module: Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho

Goal state before:
pp: case neg
𝕜 : Type u_1
E : Type u_2
inst✝⁷ : RCLike 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝⁴ : LinearOrder ι
inst✝³ : LocallyFiniteOrderBot ι
inst✝² : WellFoundedLT ι
inst✝¹ : Fintype ι
inst✝ : FiniteDimensional 𝕜 E
h : finrank 𝕜 E = Fintype.card ι
f : ι → E
i j : ι
hij : i < j
hi : ¬gramSchmidtNormed 𝕜 f j = 0
⊢ ⟪(gramSchmidtOrthonormalBasis h f) j, f i⟫_𝕜 = 0

Tactic:
simp [gramSchmidtOrthonormalBasis_apply h hi, gramSchmidtNormed, inner_smul_left,
      gramSchmidt_inv_triangular 𝕜 f hij]

Goal state after:
Module: Mathlib.LinearAlgebra.Orientation

Goal state before:
pp: R : Type u_1
inst✝⁸ : CommRing R
inst✝⁷ : PartialOrder R
inst✝⁶ : IsStrictOrderedRing R
M : Type u_2
N : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R M
inst✝² : Module R N
ι : Type u_4
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
e : Basis ι R M
f : M ≃ₗ[R] N
⊢ (e.map f).orientation = (Orientation.map ι f) e.orientation

Tactic:
[

Goal state after:
R : Type u_1
inst✝⁸ : CommRing R
inst✝⁷ : PartialOrder R
inst✝⁶ : IsStrictOrderedRing R
M : Type u_2
N : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R M
inst✝² : Module R N
ι : Type u_4
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
e : Basis ι R M
f : M ≃ₗ[R] N
⊢ (e.map f).orientation = (Orientation.map ι f) e.orientation
Module: Mathlib.LinearAlgebra.Orientation

Goal state before:
pp: R : Type u_1
inst✝⁸ : CommRing R
inst✝⁷ : PartialOrder R
inst✝⁶ : IsStrictOrderedRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
ι : Type u_4
ι' : Type u_5
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι'
inst✝ : DecidableEq ι'
e : Basis ι R M
eι : ι ≃ ι'
⊢ (e.reindex eι).orientation = (Orientation.reindex R M eι) e.orientation

Tactic:
[

Goal state after:
R : Type u_1
inst✝⁸ : CommRing R
inst✝⁷ : PartialOrder R
inst✝⁶ : IsStrictOrderedRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
ι : Type u_4
ι' : Type u_5
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι'
inst✝ : DecidableEq ι'
e : Basis ι R M
eι : ι ≃ ι'
⊢ (e.reindex eι).orientation = (Orientation.reindex R M eι) e.orientation
Module: Mathlib.Analysis.InnerProductSpace.Orientation

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
_i : Fact (finrank ℝ E = 0)
⊢ (-positiveOrientation).volumeForm = -AlternatingMap.constLinearEquivOfIsEmpty 1

Tactic:
[

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
_i : Fact (finrank ℝ E = 0)
⊢ (-positiveOrientation).volumeForm = -AlternatingMap.constLinearEquivOfIsEmpty 1
Module: Mathlib.Analysis.InnerProductSpace.Orientation

Goal state before:
pp: case zero
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
_i : Fact (finrank ℝ E = 0)
o : Orientation ℝ E (Fin 0)
b : OrthonormalBasis (Fin 0) ℝ E
hb : b.toBasis.orientation = o
this : o = positiveOrientation
⊢ o.volumeForm = b.toBasis.det

Tactic:
[

Goal state after:
case zero
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
_i : Fact (finrank ℝ E = 0)
o : Orientation ℝ E (Fin 0)
b : OrthonormalBasis (Fin 0) ℝ E
hb : b.toBasis.orientation = o
this : o = positiveOrientation
⊢ o.volumeForm = b.toBasis.det
Module: Mathlib.Analysis.InnerProductSpace.Orientation

Goal state before:
pp: case succ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n✝ : ℕ
_i : Fact (finrank ℝ E = n✝ + 1)
o : Orientation ℝ E (Fin (n✝ + 1))
b : OrthonormalBasis (Fin (n✝ + 1)) ℝ E
hb : b.toBasis.orientation = o
⊢ o.volumeForm = b.toBasis.det

Tactic:
[

Goal state after:
case succ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n✝ : ℕ
_i : Fact (finrank ℝ E = n✝ + 1)
o : Orientation ℝ E (Fin (n✝ + 1))
b : OrthonormalBasis (Fin (n✝ + 1)) ℝ E
hb : b.toBasis.orientation = o
⊢ o.volumeForm = b.toBasis.det
Module: Mathlib.Analysis.InnerProductSpace.Orientation

Goal state before:
pp: case zero
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
_i : Fact (finrank ℝ E = 0)
o : Orientation ℝ E (Fin 0)
b : OrthonormalBasis (Fin 0) ℝ E
hb : b.toBasis.orientation ≠ o
this : positiveOrientation ≠ o
⊢ o.volumeForm = -b.toBasis.det

Tactic:
[

Goal state after:
case zero
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
_i : Fact (finrank ℝ E = 0)
o : Orientation ℝ E (Fin 0)
b : OrthonormalBasis (Fin 0) ℝ E
hb : b.toBasis.orientation ≠ o
this : positiveOrientation ≠ o
⊢ o.volumeForm = -b.toBasis.det
Module: Mathlib.Analysis.InnerProductSpace.Orientation

Goal state before:
pp: case succ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = n + 1)
o : Orientation ℝ E (Fin (n + 1))
b : OrthonormalBasis (Fin (n + 1)) ℝ E
hb : b.toBasis.orientation ≠ o
e : OrthonormalBasis (Fin n.succ) ℝ E := Orientation.finOrthonormalBasis ⋯ ⋯ o
⊢ o.volumeForm = -b.toBasis.det

Tactic:
[

Goal state after:
case succ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = n + 1)
o : Orientation ℝ E (Fin (n + 1))
b : OrthonormalBasis (Fin (n + 1)) ℝ E
hb : b.toBasis.orientation ≠ o
e : OrthonormalBasis (Fin n.succ) ℝ E := Orientation.finOrthonormalBasis ⋯ ⋯ o
⊢ o.volumeForm = -b.toBasis.det
Module: Mathlib.LinearAlgebra.Orientation

Goal state before:
pp: case inl
R : Type u_1
inst✝⁶ : Field R
inst✝⁵ : LinearOrder R
inst✝⁴ : IsStrictOrderedRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : FiniteDimensional R M
x₁ x₂ : Orientation R M ι
h : Fintype.card ι = finrank R M
e : Basis ι R M
this : DecidableEq ι := Classical.decEq ι
h₁ : x₁ = e.orientation
⊢ x₁ = x₂ ∨ x₁ = -x₂

Tactic:
rcases e.orientation_eq_or_eq_neg x₂ with (h₂ | h₂)

Goal state after:
case inl.inl
R : Type u_1
inst✝⁶ : Field R
inst✝⁵ : LinearOrder R
inst✝⁴ : IsStrictOrderedRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : FiniteDimensional R M
x₁ x₂ : Orientation R M ι
h : Fintype.card ι = finrank R M
e : Basis ι R M
this : DecidableEq ι := Classical.decEq ι
h₁ : x₁ = e.orientation
h₂ : x₂ = e.orientation
⊢ x₁ = x₂ ∨ x₁ = -x₂

case inl.inr
R : Type u_1
inst✝⁶ : Field R
inst✝⁵ : LinearOrder R
inst✝⁴ : IsStrictOrderedRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : FiniteDimensional R M
x₁ x₂ : Orientation R M ι
h : Fintype.card ι = finrank R M
e : Basis ι R M
this : DecidableEq ι := Classical.decEq ι
h₁ : x₁ = e.orientation
h₂ : x₂ = -e.orientation
⊢ x₁ = x₂ ∨ x₁ = -x₂
Module: Mathlib.LinearAlgebra.Orientation

Goal state before:
pp: case inr
R : Type u_1
inst✝⁶ : Field R
inst✝⁵ : LinearOrder R
inst✝⁴ : IsStrictOrderedRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : FiniteDimensional R M
x₁ x₂ : Orientation R M ι
h : Fintype.card ι = finrank R M
e : Basis ι R M
this : DecidableEq ι := Classical.decEq ι
h₁ : x₁ = -e.orientation
⊢ x₁ = x₂ ∨ x₁ = -x₂

Tactic:
rcases e.orientation_eq_or_eq_neg x₂ with (h₂ | h₂)

Goal state after:
case inr.inl
R : Type u_1
inst✝⁶ : Field R
inst✝⁵ : LinearOrder R
inst✝⁴ : IsStrictOrderedRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : FiniteDimensional R M
x₁ x₂ : Orientation R M ι
h : Fintype.card ι = finrank R M
e : Basis ι R M
this : DecidableEq ι := Classical.decEq ι
h₁ : x₁ = -e.orientation
h₂ : x₂ = e.orientation
⊢ x₁ = x₂ ∨ x₁ = -x₂

case inr.inr
R : Type u_1
inst✝⁶ : Field R
inst✝⁵ : LinearOrder R
inst✝⁴ : IsStrictOrderedRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : FiniteDimensional R M
x₁ x₂ : Orientation R M ι
h : Fintype.card ι = finrank R M
e : Basis ι R M
this : DecidableEq ι := Classical.decEq ι
h₁ : x₁ = -e.orientation
h₂ : x₂ = -e.orientation
⊢ x₁ = x₂ ∨ x₁ = -x₂
Module: Mathlib.Analysis.BoxIntegral.Integrability

Goal state before:
pp: case refine_1
ι : Type u
E : Type v
inst✝⁴ : Fintype ι
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
I : Box ι
l : IntegrationParams
hl : l.bRiemann = false
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
g : (ι → ℝ) → E
hg : StronglyMeasurable g
this : SeparableSpace ↑(Set.range g ∪ {0})
hgi : IntegrableOn g (↑I) μ
f : ℕ → SimpleFunc (ι → ℝ) E := SimpleFunc.approxOn g ⋯ (Set.range g ∪ {0}) 0 ⋯
hfi : ∀ (n : ℕ), IntegrableOn (⇑(f n)) (↑I) μ
hfi' : ∀ (n : ℕ), BoxIntegral.Integrable I l (⇑(f n)) μ.toBoxAdditive.toSMul
hfg_mono : ∀ (x : ι → ℝ) {m n : ℕ}, m ≤ n → ‖(f n) x - g x‖ ≤ ‖(f m) x - g x‖
ε : ℝ≥0
ε0 : 0 < ε
ε0' : 0 < ↑ε
N₀ : ℕ
hN₀ : ∫ (x : ι → ℝ) in ↑I, ‖(f N₀) x - g x‖ ∂μ ≤ ↑ε
Nx : (ι → ℝ) → ℕ
hNx : ∀ (x : ι → ℝ), N₀ ≤ Nx x
hNxε : ∀ (x : ι → ℝ), dist ((f (Nx x)) x) (g x) ≤ ↑ε
δ : ℕ → ℝ≥0
δ0 : ∀ (i : ℕ), 0 < δ i
c✝ : ℝ≥0
hδc : HasSum δ c✝
hcε : c✝ < ε
r : ℝ≥0 → (ι → ℝ) → ↑(Set.Ioi 0) := fun c x ↦ ⋯.convergenceR (↑(δ (Nx x))) c x
c : ℝ≥0
π : TaggedPrepartition I
hπ : l.MemBaseSet I c (r c) π
hπp : π.IsPartition
⊢ dist (integralSum g μ.toBoxAdditive.toSMul π) (∑ J ∈ π.boxes, μ.real ↑J • (f (Nx (π.tag J))) (π.tag J)) ≤
    (∑ J ∈ π.boxes, μ.real ↑J) * ↑ε

Tactic:
sum_mul,

Goal state after:
case refine_1
ι : Type u
E : Type v
inst✝⁴ : Fintype ι
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
I : Box ι
l : IntegrationParams
hl : l.bRiemann = false
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
g : (ι → ℝ) → E
hg : StronglyMeasurable g
this : SeparableSpace ↑(Set.range g ∪ {0})
hgi : IntegrableOn g (↑I) μ
f : ℕ → SimpleFunc (ι → ℝ) E := SimpleFunc.approxOn g ⋯ (Set.range g ∪ {0}) 0 ⋯
hfi : ∀ (n : ℕ), IntegrableOn (⇑(f n)) (↑I) μ
hfi' : ∀ (n : ℕ), BoxIntegral.Integrable I l (⇑(f n)) μ.toBoxAdditive.toSMul
hfg_mono : ∀ (x : ι → ℝ) {m n : ℕ}, m ≤ n → ‖(f n) x - g x‖ ≤ ‖(f m) x - g x‖
ε : ℝ≥0
ε0 : 0 < ε
ε0' : 0 < ↑ε
N₀ : ℕ
hN₀ : ∫ (x : ι → ℝ) in ↑I, ‖(f N₀) x - g x‖ ∂μ ≤ ↑ε
Nx : (ι → ℝ) → ℕ
hNx : ∀ (x : ι → ℝ), N₀ ≤ Nx x
hNxε : ∀ (x : ι → ℝ), dist ((f (Nx x)) x) (g x) ≤ ↑ε
δ : ℕ → ℝ≥0
δ0 : ∀ (i : ℕ), 0 < δ i
c✝ : ℝ≥0
hδc : HasSum δ c✝
hcε : c✝ < ε
r : ℝ≥0 → (ι → ℝ) → ↑(Set.Ioi 0) := fun c x ↦ ⋯.convergenceR (↑(δ (Nx x))) c x
c : ℝ≥0
π : TaggedPrepartition I
hπ : l.MemBaseSet I c (r c) π
hπp : π.IsPartition
⊢ dist (integralSum g μ.toBoxAdditive.toSMul π) (∑ J ∈ π.boxes, μ.real ↑J • (f (Nx (π.tag J))) (π.tag J)) ≤
    ∑ i ∈ π.boxes, μ.real ↑i * ↑ε
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)
x : ι → ℝ
hx : x ∈ Box.Icc I \ U
this : oscillationWithin f (Box.Icc I) x = 0
⊢ oscillationWithin f (Box.Icc I) x < ENNReal.ofReal ε₁

Tactic:
this

Goal state after:
ι : 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)
x : ι → ℝ
hx : x ∈ Box.Icc I \ U
this : oscillationWithin f (Box.Icc I) x = 0
⊢ 0 < ENNReal.ofReal ε₁
Module: Mathlib.Analysis.SumOverResidueClass

Goal state before:
pp: m : ℕ
hm : NeZero m
f : ℕ → ℝ
hf : Antitone f
n : ℕ
hn : f n < 0
k : ZMod m
⊢ ¬Summable ({n | ↑n = k}.indicator f)

Tactic:
rw [← ZMod.natCast_zmod_val k, summable_indicator_mod_iff_summable]
  exact not_summable_of_antitone_of_neg
    (hf.comp_monotone <| (Covariant.monotone_of_const m).add_const k.val) <|
    (hf <| (Nat.le_mul_of_pos_left n Fin.pos').trans <| Nat.le_add_right ..).trans_lt hn

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

Goal state before:
pp: α : Type u_1
u v : α → ℝ
l : Filter α
hv : 0 ≤ v
h : u ~[l] v
r : ℝ
φ : α → ℝ
hφ : Tendsto φ l (𝓝 1)
huφv : u =ᶠ[l] φ * v
hφr : Tendsto ((fun x ↦ x ^ r) ∘ φ) l (𝓝 1)
| (fun x ↦ x ^ r) ∘ φ * v ^ r

Tactic:
change fun x ↦ φ x ^ r * v x ^ r

Goal state after:
α : Type u_1
u v : α → ℝ
l : Filter α
hv : 0 ≤ v
h : u ~[l] v
r : ℝ
φ : α → ℝ
hφ : Tendsto φ l (𝓝 1)
huφv : u =ᶠ[l] φ * v
hφr : Tendsto ((fun x ↦ x ^ r) ∘ φ) l (𝓝 1)
| fun x ↦ φ x ^ r * v x ^ r
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 : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
n : ℕ
⊢ ∑ k ∈ range (2 ^ n), f k ≤ f 0 + ∑ k ∈ range n, 2 ^ k • f (2 ^ k)

Tactic:
← le_sum_condensed' hf n,

Goal state after:
M : Type u_1
inst✝² : AddCommMonoid M
inst✝¹ : PartialOrder M
inst✝ : IsOrderedAddMonoid M
f : ℕ → M
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
n : ℕ
⊢ ∑ k ∈ range (2 ^ n), f k ≤ f 0 + ∑ k ∈ Ico 1 (2 ^ n), f k
Module: Mathlib.Algebra.Module.ZLattice.Covolume

Goal state before:
pp: case e_a
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
n : ℕ
hn : 0 < n
x : E
⊢ x ∈ s ∩ (↑n)⁻¹ • ↑L ↔
    (Basis.ofZLatticeBasis ℝ L b).equivFun.toEquiv x ∈
      ⇑(Basis.ofZLatticeBasis ℝ L b).equivFun '' s ∩ (↑n)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι)))

Tactic:
[

Goal state after:
case e_a
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
n : ℕ
hn : 0 < n
x : E
⊢ x ∈ s ∩ (↑n)⁻¹ • ↑L ↔
    (Basis.ofZLatticeBasis ℝ L b).equivFun.toEquiv x ∈
      ⇑(Basis.ofZLatticeBasis ℝ L b).equivFun '' s ∩ (↑n)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι)))
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
  rw [sum_range_succ', add_comm]
  gcongr
  suffices ∑ k ∈ range n, (u (k + 2) - u (k + 1)) • f (u (k + 1)) ≤
  C • ∑ k ∈ range n, ((u (k + 1) - u k) • f (u (k + 1))) by
    refine this.trans (nsmul_le_nsmul_right ?_ _)
    exact sum_schlomilch_le' hf h_pos hu n
  have : ∀ k ∈ range n, (u (k + 2) - u (k + 1)) • f (u (k + 1)) ≤
    C • ((u (k + 1) - u k) • f (u (k + 1))) := by
    intro k _
    rw [smul_smul]
    gcongr
    · exact h_nonneg (u (k + 1))
    exact mod_cast h_succ_diff k
  convert! sum_le_sum this
  simp [smul_sum]

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
x : E
⊢ x ∈ c • {x | x ∈ X ∧ F x ≤ 1} ↔ x ∈ {x | x ∈ X ∧ F x ≤ c ^ card ι}

Tactic:
[

Goal state after:
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
x : E
⊢ x ∈ c • {x | x ∈ X ∧ F x ≤ 1} ↔ x ∈ {x | x ∈ X ∧ F x ≤ c ^ card ι}
Module: Mathlib.Analysis.Asymptotics.SpecificAsymptotics

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

Tactic:
[

Goal state after:
case mpr
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
D : Type u_2
inst✝ : TopologicalSpace D
f : D → E
hf : Continuous[inst✝, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
h : f =O[cocompact D] 1
⊢ Bornology.IsBounded (range f)
Module: Mathlib.Analysis.PSeries

Goal state before:
pp: case mpr
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
h : ∑' (b : ℕ), ↑(f b) = ∞
⊢ ∑' (b : ℕ), ↑(↑(u (b + 1)) - ↑(u b)) * ↑(f (u b)) = ∞

Tactic:
· replace hf : ∀ m n, 0 < m → m ≤ n → (f n : ℝ≥0∞) ≤ f m := fun m n hm hmn =>
      ENNReal.coe_le_coe.2 (hf hm hmn)
    have : ∑ k ∈ range (u 0), (f k : ℝ≥0∞) ≠ ∞ := sum_ne_top.2 fun a _ => coe_ne_top
    simpa [h, add_eq_top, this] using le_tsum_schlomilch hf h_pos hu_strict

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
this : ∀ (k : ℕ), ↑(u (k + 1)) - ↑(u k) = ↑(↑(u (k + 1)) - ↑(u k))
⊢ (Summable fun k ↦ (↑(u (k + 1)) - ↑(u k)) * ↑(f (u k))) ↔ Summable fun i ↦ ↑(f i)

Tactic:
[

Goal state after:
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
this : ∀ (k : ℕ), ↑(u (k + 1)) - ↑(u k) = ↑(↑(u (k + 1)) - ↑(u k))
⊢ (Summable fun k ↦ (↑(u (k + 1)) - ↑(u k)) * ↑(f (u k))) ↔ Summable fun i ↦ ↑(f i)
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
this : ∀ (k : ℕ), ↑(u (k + 1)) - ↑(u k) = ↑(↑(u (k + 1)) - ↑(u k))
⊢ (Summable fun k ↦ (↑(u (k + 1)) - ↑(u k)) * ↑(f (u k))) ↔ Summable fun i ↦ ↑(f i)

Tactic:
this

Goal state after:
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
this : ∀ (k : ℕ), ↑(u (k + 1)) - ↑(u k) = ↑(↑(u (k + 1)) - ↑(u k))
⊢ (Summable fun k ↦ ↑(↑(u (k + 1)) - ↑(u k)) * ↑(f (u k))) ↔ Summable fun i ↦ ↑(f i)
Module: Mathlib.Analysis.PSeries

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

Tactic:
← summable_condensed_iff_of_nonneg

Goal state after:
case inl
p : ℝ
hp : 0 ≤ p
⊢ (Summable fun k ↦ 2 ^ k * (↑(2 ^ k) ^ p)⁻¹) ↔ 1 < p

case inl.h_nonneg
p : ℝ
hp : 0 ≤ p
⊢ ∀ (n : ℕ), 0 ≤ (↑n ^ p)⁻¹

case inl.h_mono
p : ℝ
hp : 0 ≤ p
⊢ ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → (↑n ^ p)⁻¹ ≤ (↑m ^ p)⁻¹
Module: Mathlib.Analysis.PSeries

Goal state before:
pp: case inl
p : ℝ
hp : 0 ≤ p
⊢ (Summable fun k ↦ 2 ^ k * (↑(2 ^ k) ^ p)⁻¹) ↔ 1 < p

Tactic:
[

Goal state after:
case inl
p : ℝ
hp : 0 ≤ p
⊢ (Summable fun k ↦ 2 ^ k * (↑(2 ^ k) ^ p)⁻¹) ↔ 1 < p
Module: Mathlib.Analysis.PSeries

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

Tactic:
[

Goal state after:
case hf₂
b : ℝ
hb : 1 < b
⊢ Summable fun n ↦ |↑(-↑n)| ^ (-b)
Module: Mathlib.Analysis.PSeries

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

Tactic:
[

Goal state after:
case hf₁
b : ℝ
hb : 1 < b
⊢ Summable fun n ↦ |↑↑n| ^ (-b)
Module: Mathlib.Analysis.PSeries

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

Tactic:
[

Goal state after:
case hf₂
b : ℝ
hb : 1 < b
⊢ Summable fun n ↦ |↑↑n| ^ (-b)