mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K₁ K₂ : Submodule 𝕜 E
inst✝ : FiniteDimensional 𝕜 ↥K₂
h : K₁ ≤ K₂
this : FiniteDimensional 𝕜 ↥K₁
hd : finrank 𝕜 ↥(K₁ ⊔ K₁ᗮ ⊓ K₂) + finrank 𝕜 ↥(⊥ ⊓ K₂) = finrank 𝕜 ↥K₁ + finrank 𝕜 ↥(K₁ᗮ ⊓ K₂)
⊢ finrank 𝕜 ↥K₁ + finrank 𝕜 ↥(K₁ᗮ ⊓ K₂) = finrank 𝕜 ↥K₂

Tactic:
bot_inf_eq,

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K₁ K₂ : Submodule 𝕜 E
inst✝ : FiniteDimensional 𝕜 ↥K₂
h : K₁ ≤ K₂
this : FiniteDimensional 𝕜 ↥K₁
hd : finrank 𝕜 ↥(K₁ ⊔ K₁ᗮ ⊓ K₂) + finrank 𝕜 ↥⊥ = finrank 𝕜 ↥K₁ + finrank 𝕜 ↥(K₁ᗮ ⊓ K₂)
⊢ finrank 𝕜 ↥K₁ + finrank 𝕜 ↥(K₁ᗮ ⊓ K₂) = finrank 𝕜 ↥K₂
Module: Mathlib.Analysis.InnerProductSpace.Projection.Basic

Goal state before:
pp: case refine_1
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : K.HasOrthogonalProjection
v : E
h : K.starProjection v = 0
w : E
hw : w ∈ K
⊢ ⟪w, K.starProjection v⟫ = 0

Tactic:
h,

Goal state after:
case refine_1
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : K.HasOrthogonalProjection
v : E
h : K.starProjection v = 0
w : E
hw : w ∈ K
⊢ ⟪w, 0⟫ = 0
Module: Mathlib.Analysis.Normed.Lp.ProdLp

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : SeminormedAddCommGroup α
inst✝ : SeminormedAddCommGroup β
x y : WithLp 1 (α × β)
⊢ ↑(nndist x y) = ↑(nndist x.fst y.fst + nndist x.snd y.snd)

Tactic:
by
    push_cast
    exact prod_dist_eq_of_L1 _ _

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.ProdLp

Goal state before:
pp: p : ℝ≥0∞
hp : Fact (1 ≤ p)
α : Type u_4
β : Type u_5
inst✝⁶ : SeminormedAddCommGroup α
inst✝⁵ : SeminormedAddCommGroup β
R : Type u_6
inst✝⁴ : SeminormedRing R
inst✝³ : Module R α
inst✝² : Module R β
inst✝¹ : IsBoundedSMul R α
inst✝ : IsBoundedSMul R β
⊢ IsBoundedSMul R (α × β)

Tactic:
let := pseudoMetricSpaceToProd p α β

Goal state after:
p : ℝ≥0∞
hp : Fact (1 ≤ p)
α : Type u_4
β : Type u_5
inst✝⁶ : SeminormedAddCommGroup α
inst✝⁵ : SeminormedAddCommGroup β
R : Type u_6
inst✝⁴ : SeminormedRing R
inst✝³ : Module R α
inst✝² : Module R β
inst✝¹ : IsBoundedSMul R α
inst✝ : IsBoundedSMul R β
this : PseudoMetricSpace (α × β) := pseudoMetricSpaceToProd p α β
⊢ IsBoundedSMul R (α × β)
Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic

Goal state before:
pp: case hdiag
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
M : Matrix ι ι ℝ
hM : M.det ≠ 0
D : ι → ℝ
hD : (Matrix.diagonal D).det ≠ 0
⊢ Measure.map (⇑(toLin' (Matrix.diagonal D))) volume =
    ofReal |(Matrix.diagonal D).det⁻¹| •
      ofReal |(Matrix.diagonal D).det| • Measure.map (⇑(toLin' (Matrix.diagonal D))) volume

Tactic:
rw [smul_smul, ← ENNReal.ofReal_mul (abs_nonneg _), ← abs_mul, inv_mul_cancel₀ hD, abs_one,
      ENNReal.ofReal_one, one_smul]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
s : Set α
hf : Measurable f
hg : Measurable g
hs : MeasurableSet s
h : (fun x ↦ volume {a | x ∈ s ∧ a ∈ Ioo (f x) (g x)}) = s.indicator fun x ↦ ofReal (g x - f x)
⊢ ∫⁻ (x : α), volume {a | x ∈ s ∧ a ∈ Ioo (f x) (g x)} ∂μ = ∫⁻ (y : α) in s, ofReal ((g - f) y) ∂μ

Tactic:
h,

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
s : Set α
hf : Measurable f
hg : Measurable g
hs : MeasurableSet s
h : (fun x ↦ volume {a | x ∈ s ∧ a ∈ Ioo (f x) (g x)}) = s.indicator fun x ↦ ofReal (g x - f x)
⊢ lintegral μ (s.indicator fun x ↦ ofReal (g x - f x)) = ∫⁻ (y : α) in s, ofReal ((g - f) y) ∂μ
Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
f_mble : AEMeasurable f μ
g_mble : AEMeasurable g μ
s : Set α
s_mble : NullMeasurableSet s μ
⊢ NullMeasurableSet {p | p.1 ∈ s ∧ p.2 ∈ Ico (f p.1) (g p.1)} (μ.prod volume)

Tactic:
refine NullMeasurableSet.inter
          (s_mble.preimage quasiMeasurePreserving_fst) (NullMeasurableSet.inter ?_ ?_)
  · change NullMeasurableSet {p : α × ℝ | f p.fst ≤ p.snd} (μ.prod volume)
    rw [show {p : α × ℝ | f p.fst ≤ p.snd} = {p : α × ℝ | p.snd < f p.fst}ᶜ by
          ext p
          simp]
    exact (nullMeasurableSet_lt measurable_snd.aemeasurable (by fun_prop)).compl
  · exact nullMeasurableSet_lt measurable_snd.aemeasurable (by fun_prop)

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

Goal state before:
pp: case h
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁶ : NormedField K
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace K E
b : Basis ι K E
inst✝³ : LinearOrder K
inst✝² : IsStrictOrderedRing K
inst✝¹ : FloorRing K
inst✝ : Fintype ι
m v : E
h : v ∈ span ℤ (Set.range ⇑b)
i : ι
⊢ (b.repr v) i = (b.repr ↑⟨v, h⟩) i

Tactic:
coe_mk

Goal state after:
case h
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁶ : NormedField K
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace K E
b : Basis ι K E
inst✝³ : LinearOrder K
inst✝² : IsStrictOrderedRing K
inst✝¹ : FloorRing K
inst✝ : Fintype ι
m v : E
h : v ∈ span ℤ (Set.range ⇑b)
i : ι
⊢ (b.repr v) i = (b.repr v) i
Module: Mathlib.Algebra.Module.ZLattice.Basic

Goal state before:
pp: E : Type u_1
ι : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
b : Basis ι ℝ E
inst✝ : Fintype ι
⊢ {m | ∀ (i : ι), (b.repr m) i ∈ Set.Ico 0 1} ⊆ parallelepiped ⇑b

Tactic:
parallelepiped_basis_eq,

Goal state after:
E : Type u_1
ι : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
b : Basis ι ℝ E
inst✝ : Fintype ι
⊢ {m | ∀ (i : ι), (b.repr m) i ∈ Set.Ico 0 1} ⊆ {x | ∀ (i : ι), (b.repr x) i ∈ Set.Icc 0 1}
Module: Mathlib.Algebra.Module.ZLattice.Basic

Goal state before:
pp: E : Type u_1
ι : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
b : Basis ι ℝ E
inst✝ : Finite ι
x✝ : E
hx : x✝ ∈ span ℤ (Set.range ⇑b)
⊢ b.equivFun x✝ ∈ span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))

Tactic:
Basis.mem_span_iff_repr_mem

Goal state after:
E : Type u_1
ι : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
b : Basis ι ℝ E
inst✝ : Finite ι
x✝ : E
hx : ∀ (i : ι), (b.repr x✝) i ∈ Set.range ⇑(algebraMap ℤ ℝ)
⊢ ∀ (i : ι), ((Pi.basisFun ℝ ι).repr (b.equivFun x✝)) i ∈ Set.range ⇑(algebraMap ℤ ℝ)
Module: Mathlib.Algebra.Module.ZLattice.Basic

Goal state before:
pp: E : Type u_1
ι : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
b : Basis ι ℝ E
inst✝³ : Fintype ι
inst✝² : MeasurableSpace E
μ : Measure E
inst✝¹ : BorelSpace E
inst✝ : μ.IsAddHaarMeasure
this : FiniteDimensional ℝ E
x : E
hx : x ∈ parallelepiped ⇑b \ fundamentalDomain b
⊢ x ∈ ⋃ i, ↑(AffineSubspace.mk' (b i) (span ℝ (⇑b '' (Set.univ \ {i}))))

Tactic:
parallelepiped_basis_eq,

Goal state after:
E : Type u_1
ι : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
b : Basis ι ℝ E
inst✝³ : Fintype ι
inst✝² : MeasurableSpace E
μ : Measure E
inst✝¹ : BorelSpace E
inst✝ : μ.IsAddHaarMeasure
this : FiniteDimensional ℝ E
x : E
hx : x ∈ {x | ∀ (i : ι), (b.repr x) i ∈ Set.Icc 0 1} \ fundamentalDomain b
⊢ x ∈ ⋃ i, ↑(AffineSubspace.mk' (b i) (span ℝ (⇑b '' (Set.univ \ {i}))))
Module: Mathlib.Analysis.InnerProductSpace.PiL2

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_3
inst✝³ : RCLike 𝕜
E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : Fintype ι
b : OrthonormalBasis ι 𝕜 E
x : E
⊢ ∑ i, ‖⟪b i, x⟫‖ ^ 2 = √(∑ x_1, re (⟪x, b x_1⟫ * ⟪b x_1, x⟫)) ^ 2

Tactic:
simp_rw [inner_mul_symm_re_eq_norm, norm_mul, ← inner_conj_symm x, starRingEnd_apply,
    norm_star, ← pow_two]

Goal state after:
ι : Type u_1
𝕜 : Type u_3
inst✝³ : RCLike 𝕜
E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : Fintype ι
b : OrthonormalBasis ι 𝕜 E
x : E
⊢ ∑ i, ‖⟪b i, x⟫‖ ^ 2 = √(∑ x_1, ‖⟪b x_1, x⟫‖ ^ 2) ^ 2
Module: Mathlib.Analysis.BoxIntegral.Partition.Split

Goal state before:
pp: ι : Type u_1
I J Js : Box ι
s : Finset (ι × ℝ)
H : ∀ (i : ι), {(i, J.lower i), (i, J.upper i)} ⊆ s
HJs : Js ∈ splitMany I s
Hn : ¬Disjoint ↑J ↑Js
⊢ Js ≤ J

Tactic:
simp only [Finset.insert_subset_iff, Finset.singleton_subset_iff] at H

Goal state after:
ι : Type u_1
I J Js : Box ι
s : Finset (ι × ℝ)
HJs : Js ∈ splitMany I s
Hn : ¬Disjoint ↑J ↑Js
H : ∀ (i : ι), (i, J.lower i) ∈ s ∧ (i, J.upper i) ∈ s
⊢ Js ≤ J
Module: Mathlib.Analysis.InnerProductSpace.PiL2

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_3
inst✝⁵ : RCLike 𝕜
E : Type u_4
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : Fintype ι
inst✝¹ : FiniteDimensional 𝕜 E
n : ℕ
hn : finrank 𝕜 E = n
inst✝ : DecidableEq ι
V : ι → Submodule 𝕜 E
hV : IsInternal V
hV' : OrthogonalFamily 𝕜 (fun i ↦ ↥(V i)) fun i ↦ (V i).subtypeₗᵢ
i : ι
hi : V i ≠ ⊥
⊢ 0 < finrank 𝕜 ↥(V i)

Tactic:
by grind [finrank_eq_zero (S := V i)]

Goal state after:
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 ι
n : ι
⊢ gramSchmidt 𝕜 0 n = 0

Tactic:
gramSchmidt_def

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 ι
n : ι
⊢ 0 n - ∑ i < n, (𝕜 ∙ gramSchmidt 𝕜 0 i).starProjection (0 n) = 0
Module: Mathlib.Analysis.BoxIntegral.UnitPartition

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
x : ℝ
a : ℤ
h : 0 < ↑n
⊢ ↑a < x ↔ ↑(↑n * a + 1) ≤ ↑⌈↑n * x⌉

Tactic:
Int.cast_le,

Goal state after:
n : ℕ
inst✝ : NeZero n
x : ℝ
a : ℤ
h : 0 < ↑n
⊢ ↑a < x ↔ ↑n * a + 1 ≤ ⌈↑n * x⌉
Module: Mathlib.Analysis.BoxIntegral.UnitPartition

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
x : ℝ
a : ℤ
h : 0 < ↑n
⊢ x ≤ ↑a ↔ ↑⌈↑n * x⌉ ≤ ↑(↑n * a)

Tactic:
Int.cast_le,

Goal state after:
n : ℕ
inst✝ : NeZero n
x : ℝ
a : ℤ
h : 0 < ↑n
⊢ x ≤ ↑a ↔ ⌈↑n * x⌉ ≤ ↑n * a
Module: Mathlib.Analysis.BoxIntegral.UnitPartition

Goal state before:
pp: ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Finite ι
x y : ι → ℝ
hx : x ∈ (↑n)⁻¹ • span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))
hy : y ∈ (↑n)⁻¹ • span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))
h : index n x = index n y
⊢ x = y

Tactic:
← tag_index_eq_self_of_mem_smul_span n hx,

Goal state after:
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Finite ι
x y : ι → ℝ
hx : x ∈ (↑n)⁻¹ • span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))
hy : y ∈ (↑n)⁻¹ • span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))
h : index n x = index n y
⊢ tag n (index n x) = y
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
hf : Pairwise fun x1 x2 ↦ ⟪f x1, f x2⟫_𝕜 = 0
i : ι
⊢ gramSchmidt 𝕜 f i = f i

Tactic:
gramSchmidt_def

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
hf : Pairwise fun x1 x2 ↦ ⟪f x1, f x2⟫_𝕜 = 0
i : ι
⊢ f i - ∑ i_1 < i, (𝕜 ∙ gramSchmidt 𝕜 f i_1).starProjection (f i) = f i
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
n : ι
h₀ : LinearIndependent 𝕜 (f ∘ Subtype.val)
h : gramSchmidt 𝕜 f n = 0
⊢ gramSchmidt 𝕜 f n + ∑ i < n, (𝕜 ∙ gramSchmidt 𝕜 f i).starProjection (f n) ∈ span 𝕜 (gramSchmidt 𝕜 f '' Set.Iio n)

Tactic:
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
n : ι
h₀ : LinearIndependent 𝕜 (f ∘ Subtype.val)
h : gramSchmidt 𝕜 f n = 0
⊢ 0 + ∑ i < n, (𝕜 ∙ gramSchmidt 𝕜 f i).starProjection (f n) ∈ span 𝕜 (gramSchmidt 𝕜 f '' Set.Iio n)
Module: Mathlib.Analysis.BoxIntegral.Integrability

Goal state before:
pp: case hbc.refine_2
ι : Type u
E : Type v
inst✝³ : Fintype ι
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
l : IntegrationParams
hl : l.bRiemann = false
s : Set (ι → ℝ)
hs : MeasurableSet s
I : Box ι
y : E
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
ε : ℝ≥0
ε0 : 0 < ε
A : μ (s ∩ Box.Icc I) ≠ ∞
B : μ (s ∩ ↑I) ≠ ∞
F : Set (ι → ℝ)
hFs : F ⊆ s ∩ Box.Icc I
hFc : IsClosed F
hμF : μ ((s ∩ Box.Icc I) \ F) < ↑ε
U : Set (ι → ℝ)
hsU : s ∩ Box.Icc I ⊆ U
hUo : IsOpen U
hUt : μ U < ∞
hμU : μ (U \ (s ∩ Box.Icc I)) < ↑ε
rs : (ι → ℝ) → ↑(Set.Ioi 0)
hrsU : ∀ x ∈ s ∩ Box.Icc I, closedBall x ↑(rs x) ⊆ U
rs' : (ι → ℝ) → ↑(Set.Ioi 0)
hrs'F : ∀ x ∈ Box.Icc I \ s, closedBall x ↑(rs' x) ⊆ Fᶜ
r : (ι → ℝ) → ↑(Set.Ioi 0) := s.piecewise rs rs'
c : ℝ≥0
π : TaggedPrepartition I
hπ : l.MemBaseSet I c ((fun x ↦ r) c) π
hπp : π.IsPartition
t : Set (ι → ℝ) := (π.filter fun x ↦ π.tag x ∈ s).iUnion
htU : t ⊆ U ∩ ↑I
hμt : μ t ≠ ∞
x : ι → ℝ
hxt : x ∉ t
hxs : x ∈ s
hxI : x ∈ ↑I
J : Box ι
hJπ : J ∈ π.toPrepartition
hxJ : x ∈ J
hxF : π.tag J ∉ s
⊢ x ∈ closedBall (π.tag J) ↑(rs' (π.tag J))

Tactic:
simpa only [r, s.piecewise_eq_of_notMem _ _ hxF] using hπ.1 J hJπ (Box.coe_subset_Icc hxJ)

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

Goal state before:
pp: ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
s : Set (ι → ℝ)
F : (ι → ℝ) → ℝ
inst✝ : Fintype ι
B : Box ι
hB : hasIntegralVertices B
hs₀ : s ⊆ ↑B
⊢ integralSum (s.indicator F) volume.toBoxAdditive.toSMul (prepartition n B) =
    (∑' (x : ↑(s ∩ (↑n)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))))), F ↑x) / ↑n ^ card ι

Tactic:
by
  classical
  unfold integralSum
  have : Fintype ↑(s ∩ (n : ℝ)⁻¹ • L) := by
    apply Set.Finite.fintype
    rw [← coe_pointwise_smul, ZSpan.smul _ (inv_ne_zero (NeZero.ne _))]
    exact ZSpan.setFinite_inter _ (B.isBounded.subset hs₀)
  rw [tsum_fintype, Finset.sum_set_coe, Finset.sum_div, eq_comm]
  simp_rw [Set.indicator_apply, apply_ite, BoxAdditiveMap.toSMul_apply, Measure.toBoxAdditive_apply,
    smul_eq_mul, mul_zero, Finset.sum_ite, Finset.sum_const_zero, add_zero]
  refine Finset.sum_bij (fun x _ ↦ box n (index n x)) (fun _ hx ↦ Finset.mem_filter.mpr ?_)
    (fun _ hx _ hy h ↦ ?_) (fun I hI ↦ ?_) (fun _ hx ↦ ?_)
  · rw [Set.mem_toFinset] at hx
    refine ⟨mem_prepartition_boxes_iff.mpr
      ⟨index n _, mem_admissibleIndex_of_mem_box n hB (hs₀ hx.1), rfl⟩, ?_⟩
    simp_rw [prepartition_tag n (mem_admissibleIndex_of_mem_box n hB (hs₀ hx.1)),
      tag_index_eq_self_of_mem_smul_span n hx.2, hx.1]
  · rw [Set.mem_toFinset] at hx hy
    exact eq_of_mem_smul_span_of_index_eq_index n hx.2 hy.2 (box_injective n h)
  · rw [Finset.mem_filter] at hI
    refine ⟨(prepartition n B).tag I, Set.mem_toFinset.mpr ⟨hI.2, ?_⟩, box_index_tag_eq_self n hI.1⟩
    rw [← box_index_tag_eq_self n hI.1, prepartition_tag n
      (mem_admissibleIndex_of_mem_box n hB (hs₀ hI.2))]
    exact tag_mem_smul_span _ _
  · rw [Set.mem_toFinset] at hx
    rw [measureReal_def, volume_box,
      prepartition_tag n (mem_admissibleIndex_of_mem_box n hB (hs₀ hx.1)),
      tag_index_eq_self_of_mem_smul_span n hx.2, ENNReal.toReal_div,
      ENNReal.toReal_one, ENNReal.toReal_pow, ENNReal.toReal_natCast, mul_comm_div, one_mul]

Goal state after:
Module: Mathlib.LinearAlgebra.Orientation

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : PartialOrder R
inst✝² : IsStrictOrderedRing R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_4
⊢ map ι (LinearEquiv.refl R M) = Equiv.refl (Orientation R M ι)

Tactic:
rw [Orientation.map, AlternatingMap.domLCongr_refl, Module.Ray.map_refl]

Goal state after:
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:
simp [volumeForm, Or.by_cases]

Goal state after:
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:
volumeForm,

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
_i : Fact (finrank ℝ E = 0)
⊢ Nat.casesAuxOn (motive := fun a ↦ 0 = a → E [⋀^Fin 0]→ₗ[ℝ] ℝ) 0
      (fun h ↦
        ⋯.by_cases (fun x ↦ AlternatingMap.constOfIsEmpty ℝ E (Fin 0) 1) fun x ↦
          -AlternatingMap.constOfIsEmpty ℝ E (Fin 0) 1)
      (fun n h ↦
        Eq.rec (motive := fun x x_1 ↦ [_i : Fact (finrank ℝ E = x)] → Orientation ℝ E (Fin x) → E [⋀^Fin x]→ₗ[ℝ] ℝ)
          (fun [Fact (finrank ℝ E = n + 1)] o ↦ (Orientation.finOrthonormalBasis ⋯ ⋯ o).toBasis.det) ⋯
          (-positiveOrientation))
      ⋯ =
    -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:
volumeForm,

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
⊢ Nat.casesAuxOn (motive := fun a ↦ 0 = a → E [⋀^Fin 0]→ₗ[ℝ] ℝ) 0
      (fun h ↦
        ⋯.by_cases (fun x ↦ AlternatingMap.constOfIsEmpty ℝ E (Fin 0) 1) fun x ↦
          -AlternatingMap.constOfIsEmpty ℝ E (Fin 0) 1)
      (fun n h ↦
        Eq.rec (motive := fun x x_1 ↦ [_i : Fact (finrank ℝ E = x)] → Orientation ℝ E (Fin x) → E [⋀^Fin x]→ₗ[ℝ] ℝ)
          (fun [Fact (finrank ℝ E = n + 1)] o ↦ (Orientation.finOrthonormalBasis ⋯ ⋯ o).toBasis.det) ⋯ o)
      ⋯ =
    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:
volumeForm,

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
⊢ Nat.casesAuxOn (motive := fun a ↦ 0 = a → E [⋀^Fin 0]→ₗ[ℝ] ℝ) 0
      (fun h ↦
        ⋯.by_cases (fun x ↦ AlternatingMap.constOfIsEmpty ℝ E (Fin 0) 1) fun x ↦
          -AlternatingMap.constOfIsEmpty ℝ E (Fin 0) 1)
      (fun n h ↦
        Eq.rec (motive := fun x x_1 ↦ [_i : Fact (finrank ℝ E = x)] → Orientation ℝ E (Fin x) → E [⋀^Fin x]→ₗ[ℝ] ℝ)
          (fun [Fact (finrank ℝ E = n + 1)] o ↦ (Orientation.finOrthonormalBasis ⋯ ⋯ o).toBasis.det) ⋯ o)
      ⋯ =
    -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))
e : OrthonormalBasis (Fin n.succ) ℝ E := Orientation.finOrthonormalBasis ⋯ ⋯ o
h₁ : e.toBasis.orientation = o
h₂ : e.toBasis.orientation ≠ -o
⊢ (-o).volumeForm = -o.volumeForm

Tactic:
o.volumeForm_robust e h₁,

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))
e : OrthonormalBasis (Fin n.succ) ℝ E := Orientation.finOrthonormalBasis ⋯ ⋯ o
h₁ : e.toBasis.orientation = o
h₂ : e.toBasis.orientation ≠ -o
⊢ (-o).volumeForm = -e.toBasis.det
Module: Mathlib.Algebra.Module.ZLattice.Covolume

Goal state before:
pp: E : Type u_1
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
inst✝⁷ : FiniteDimensional ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
L : Submodule ℤ E
inst✝⁴ : DiscreteTopology ↥L
inst✝³ : IsZLattice ℝ L
μ : Measure E
inst✝² : μ.IsAddHaarMeasure
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Basis ι ℤ ↥L
b₀ : Basis ι ℝ E
⊢ covolume L μ = |b₀.det (Subtype.val ∘ ⇑b)| * μ.real (fundamentalDomain b₀)

Tactic:
by
  rw [covolume_eq_measure_fundamentalDomain L μ (isAddFundamentalDomain b μ),
    measureReal_fundamentalDomain _ _ b₀,
    measureReal_congr (fundamentalDomain_ae_parallelepiped b₀ μ)]
  congr
  ext
  exact b.ofZLatticeBasis_apply ℝ L _

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
p q : ℕ
⊢ (fun x ↦ x ^ p / x ^ q) =ᶠ[atBot] fun x ↦ x ^ (↑p - ↑q)

Tactic:
apply (eventually_lt_atBot (0 : 𝕜)).mono fun x hx => _

Goal state after:
𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
p q : ℕ
⊢ ∀ x < 0, (fun x ↦ x ^ p / x ^ q) x = (fun x ↦ x ^ (↑p - ↑q)) x
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:
intro k

Goal state after:
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 : ℕ
⊢ k ∈ range n → (u (k + 2) - u (k + 1)) • f (u (k + 1)) ≤ C • (u (k + 1) - u k) • f (u (k + 1))
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
n : ℕ
⊢ ∑ a ∈ range n.succ, (↑(u (a + 1)) - ↑(u a)) * f (u a) ≤
    (↑(u 1) - ↑(u 0)) * f (u 0) + ↑C * ∑ x ∈ Ico (u 0 + 1) (u n + 1), f x

Tactic:
simpa using Finset.sum_schlomilch_le hf h_pos h_nonneg hu h_succ_diff n

Goal state after:
Module: Mathlib.Analysis.PSeries

Goal state before:
pp: ⊢ ∀ (n : ℕ), 0 ≤ 1 / (↑n + 1)

Tactic:
exact fun i => by positivity

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Ideal

Goal state before:
pp: case mp
k : Type u_1
G : Type u_3
inst✝¹ : Monoid G
inst✝ : Semiring k
s : Set G
x : k[G]
RHS : Ideal k[G] :=
  { carrier := {p | ∀ m ∈ p.coeff.support, ∃ m' ∈ s, ∃ d, m = d * m'}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }
⊢ ⇑(of k G) '' s ⊆ ↑RHS

Tactic:
rintro _ ⟨i, hi, rfl⟩ m hm

Goal state after:
case mp
k : Type u_1
G : Type u_3
inst✝¹ : Monoid G
inst✝ : Semiring k
s : Set G
x : k[G]
RHS : Ideal k[G] :=
  { carrier := {p | ∀ m ∈ p.coeff.support, ∃ m' ∈ s, ∃ d, m = d * m'}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }
i : G
hi : i ∈ s
m : G
hm : m ∈ ((of k G) i).coeff.support
⊢ ∃ m' ∈ s, ∃ d, m = d * m'
Module: Mathlib.Algebra.MonoidAlgebra.Ideal

Goal state before:
pp: case mp
k : Type u_1
A : Type u_2
inst✝¹ : AddMonoid A
inst✝ : Semiring k
s : Set A
x : k[A]
RHS : Ideal k[A] :=
  { carrier := {p | ∀ m ∈ p.coeff.support, ∃ m' ∈ s, ∃ d, m = d + m'}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }
⊢ of' k A '' s ⊆ ↑RHS

Tactic:
rintro _ ⟨i, hi, rfl⟩ m hm

Goal state after:
case mp
k : Type u_1
A : Type u_2
inst✝¹ : AddMonoid A
inst✝ : Semiring k
s : Set A
x : k[A]
RHS : Ideal k[A] :=
  { carrier := {p | ∀ m ∈ p.coeff.support, ∃ m' ∈ s, ∃ d, m = d + m'}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }
i : A
hi : i ∈ s
m : A
hm : m ∈ (of' k A i).coeff.support
⊢ ∃ m' ∈ s, ∃ d, m = d + m'