mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic

Goal state before:
pp: case hmul
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
M : Matrix ι ι ℝ
hM : M.det ≠ 0
A B : Matrix ι ι ℝ
a✝¹ : A.det ≠ 0
a✝ : B.det ≠ 0
IHA : Measure.map (⇑(toLin' A)) volume = ofReal |A.det⁻¹| • volume
IHB : Measure.map (⇑(toLin' B)) volume = ofReal |B.det⁻¹| • volume
⊢ Measure.map (⇑(toLin' A ∘ₗ toLin' B)) volume = ofReal |(A * B).det⁻¹| • volume

Tactic:
det_mul,

Goal state after:
case hmul
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
M : Matrix ι ι ℝ
hM : M.det ≠ 0
A B : Matrix ι ι ℝ
a✝¹ : A.det ≠ 0
a✝ : B.det ≠ 0
IHA : Measure.map (⇑(toLin' A)) volume = ofReal |A.det⁻¹| • volume
IHB : Measure.map (⇑(toLin' B)) volume = ofReal |B.det⁻¹| • volume
⊢ Measure.map (⇑(toLin' A ∘ₗ toLin' B)) volume = ofReal |(A.det * B.det)⁻¹| • volume
Module: Mathlib.Algebra.Module.ZLattice.Basic

Goal state before:
pp: 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 ι
inst✝ : HasSolidNorm K
m : E
i : ι
x✝ : i ∈ Finset.univ
⊢ |Int.fract ((b.repr m) i)| ≤ |1|

Tactic:
abs_one,

Goal state after:
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 ι
inst✝ : HasSolidNorm K
m : E
i : ι
x✝ : i ∈ Finset.univ
⊢ |Int.fract ((b.repr m) i)| ≤ 1
Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
s : Set E
x : E
h : Tendsto (fun r ↦ μ (s ∩ closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 0)
t u : Set E
h'u : μ u ≠ 0
R : ℝ
Rpos : 0 < R
t_bound : t ⊆ closedBall 0 R
t' : Set E := R⁻¹ • t
ht' : t' = R⁻¹ • t
u' : Set E := R⁻¹ • u
hu' : u' = R⁻¹ • u
A : Tendsto (fun r ↦ μ (s ∩ ({x} + r • t')) / μ ({x} + r • u')) (𝓝[>] 0) (𝓝 0)
B : Tendsto (fun r ↦ R * r) (𝓝[>] 0) (𝓝[>] 0)
⊢ ∀ a ∈ Ioi 0,
    ((fun r ↦ μ (s ∩ ({x} + r • t')) / μ ({x} + r • u')) ∘ fun r ↦ R * r) a = μ (s ∩ ({x} + a • t)) / μ ({x} + a • u)

Tactic:
rintro r -

Goal state after:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
s : Set E
x : E
h : Tendsto (fun r ↦ μ (s ∩ closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 0)
t u : Set E
h'u : μ u ≠ 0
R : ℝ
Rpos : 0 < R
t_bound : t ⊆ closedBall 0 R
t' : Set E := R⁻¹ • t
ht' : t' = R⁻¹ • t
u' : Set E := R⁻¹ • u
hu' : u' = R⁻¹ • u
A : Tendsto (fun r ↦ μ (s ∩ ({x} + r • t')) / μ ({x} + r • u')) (𝓝[>] 0) (𝓝 0)
B : Tendsto (fun r ↦ R * r) (𝓝[>] 0) (𝓝[>] 0)
r : ℝ
⊢ ((fun r ↦ μ (s ∩ ({x} + r • t')) / μ ({x} + r • u')) ∘ fun r ↦ R * r) r = μ (s ∩ ({x} + r • t)) / μ ({x} + r • u)
Module: Mathlib.Analysis.BoxIntegral.Partition.Basic

Goal state before:
pp: ι : Type u_1
I J : Box ι
π : Prepartition I
πi : (J : Box ι) → Prepartition J
hJ : J ∈ π
⊢ (π.biUnion πi).restrict J = πi J

Tactic:
refine (eq_of_boxes_subset_iUnion_superset (fun J₁ h₁ => ?_) ?_).symm

Goal state after:
case refine_1
ι : Type u_1
I J : Box ι
π : Prepartition I
πi : (J : Box ι) → Prepartition J
hJ : J ∈ π
J₁ : Box ι
h₁ : J₁ ∈ (πi J).boxes
⊢ J₁ ∈ ((π.biUnion πi).restrict J).boxes

case refine_2
ι : Type u_1
I J : Box ι
π : Prepartition I
πi : (J : Box ι) → Prepartition J
hJ : J ∈ π
⊢ ((π.biUnion πi).restrict J).iUnion ⊆ (πi J).iUnion
Module: Mathlib.Analysis.BoxIntegral.Partition.Basic

Goal state before:
pp: ι : Type u_1
I : Box ι
inst✝ : Fintype ι
π : Prepartition I
πi : (J : Box ι) → Prepartition J
⊢ (π.biUnion πi).distortion = π.boxes.sup fun J ↦ (πi J).distortion

Tactic:
exact sup_biUnion _ _

Goal state after:
Module: Mathlib.Analysis.BoxIntegral.Partition.Tagged

Goal state before:
pp: ι : Type u_1
I : Box ι
inst✝ : Fintype ι
π : Prepartition I
πi : (J : Box ι) → TaggedPrepartition J
⊢ (π.biUnionTagged πi).distortion = π.boxes.sup fun J ↦ (πi J).distortion

Tactic:
exact sup_biUnion _ _

Goal state after:
Module: Mathlib.Analysis.BoxIntegral.Partition.Tagged

Goal state before:
pp: ι : Type u_1
I : Box ι
inst✝ : Fintype ι
π : TaggedPrepartition I
πi : (J : Box ι) → Prepartition J
⊢ (π.biUnionPrepartition πi).distortion = π.boxes.sup fun J ↦ (πi J).distortion

Tactic:
exact sup_biUnion _ _

Goal state after:
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
⊢ ⇑((EuclideanSpace.basisFun ι 𝕜).equiv b (Equiv.refl ι)) = fun x ↦ ∑ i, x.ofLp i • b i

Tactic:
simp_rw [← equiv_apply_euclideanSpace]

Goal state after:
Module: Mathlib.Analysis.BoxIntegral.Partition.Additive

Goal state before:
pp: case insert
ι : Type u_1
M : Type u_2
n : ℕ
N : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : AddCommMonoid N
I₀✝ : WithTop (Box ι)
I✝ : Box ι
i : ι
inst✝ : Finite ι
f : Box ι → M
I₀ : WithTop (Box ι)
hf :
  ∀ (I : Box ι),
    ↑I ≤ I₀ →
      ∀ {i : ι} {x : ℝ},
        x ∈ Set.Ioo (I.lower i) (I.upper i) →
          Option.elim' 0 f (I.splitLower i x) + Option.elim' 0 f (I.splitUpper i x) = f I
I : Box ι
hI : ↑I ≤ I₀
a : ι × ℝ
s : Finset (ι × ℝ)
a✝ : a ∉ s
ihs : ∑ J ∈ (splitMany I s).boxes, f J = f I
⊢ ∑ J ∈ (splitMany I s).boxes.biUnion fun J ↦ (split J a.1 a.2).boxes, f J = ∑ J ∈ (splitMany I s).boxes, f J

Tactic:
sum_biUnion_boxes

Goal state after:
case insert
ι : Type u_1
M : Type u_2
n : ℕ
N : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : AddCommMonoid N
I₀✝ : WithTop (Box ι)
I✝ : Box ι
i : ι
inst✝ : Finite ι
f : Box ι → M
I₀ : WithTop (Box ι)
hf :
  ∀ (I : Box ι),
    ↑I ≤ I₀ →
      ∀ {i : ι} {x : ℝ},
        x ∈ Set.Ioo (I.lower i) (I.upper i) →
          Option.elim' 0 f (I.splitLower i x) + Option.elim' 0 f (I.splitUpper i x) = f I
I : Box ι
hI : ↑I ≤ I₀
a : ι × ℝ
s : Finset (ι × ℝ)
a✝ : a ∉ s
ihs : ∑ J ∈ (splitMany I s).boxes, f J = f I
⊢ ∑ J ∈ (splitMany I s).boxes, ∑ J' ∈ (split J a.1 a.2).boxes, f J' = ∑ J ∈ (splitMany I s).boxes, f J
Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
s : Set E
x : E
h : Tendsto (fun r ↦ μ (s ∩ closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 1)
t : Set E
ht : MeasurableSet t
h't : μ t ≠ 0
h''t : μ t ≠ ∞
⊢ ∀ a ∈ Ioi 0, μ (toMeasurable μ s ∩ closedBall x a) / μ (closedBall x a) ≤ 1

Tactic:
rintro r -

Goal state after:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
s : Set E
x : E
h : Tendsto (fun r ↦ μ (s ∩ closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 1)
t : Set E
ht : MeasurableSet t
h't : μ t ≠ 0
h''t : μ t ≠ ∞
r : ℝ
⊢ μ (toMeasurable μ s ∩ closedBall x r) / μ (closedBall x r) ≤ 1
Module: Mathlib.Analysis.Oscillation

Goal state before:
pp: E : Type u
F : Type v
inst✝¹ : PseudoEMetricSpace F
inst✝ : TopologicalSpace E
f : E → F
D : Set E
x : E
hD : D ∈ 𝓝 x
⊢ oscillationWithin f D x = oscillation f x

Tactic:
rw [oscillation, oscillationWithin, nhdsWithin_eq_nhds.2 hD]

Goal state after:
Module: Mathlib.Analysis.BoxIntegral.Partition.Additive

Goal state before:
pp: ι : Type u_1
M : Type u_2
n : ℕ
N : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : AddCommMonoid N
I₀✝ : WithTop (Box ι)
I✝ : Box ι
i : ι
inst✝ : Finite ι
f : Box ι → M
I₀ : WithTop (Box ι)
hf : ∀ (I : Box ι), ↑I ≤ I₀ → ∀ (s : Finset (ι × ℝ)), ∑ J ∈ (splitMany I s).boxes, f J = f I
I : Box ι
hI : ↑I ≤ I₀
π : Prepartition I
hπ : π.IsPartition
Hle : ∀ J ∈ π, ↑J ≤ I₀
s : Finset (ι × ℝ)
hs : splitMany I s ≤ π
⊢ ∑ Ji ∈ π.boxes, f Ji = ∑ J ∈ π.boxes.biUnion fun J ↦ (splitMany J s).boxes, f J

Tactic:
sum_biUnion_boxes

Goal state after:
ι : Type u_1
M : Type u_2
n : ℕ
N : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : AddCommMonoid N
I₀✝ : WithTop (Box ι)
I✝ : Box ι
i : ι
inst✝ : Finite ι
f : Box ι → M
I₀ : WithTop (Box ι)
hf : ∀ (I : Box ι), ↑I ≤ I₀ → ∀ (s : Finset (ι × ℝ)), ∑ J ∈ (splitMany I s).boxes, f J = f I
I : Box ι
hI : ↑I ≤ I₀
π : Prepartition I
hπ : π.IsPartition
Hle : ∀ J ∈ π, ↑J ≤ I₀
s : Finset (ι × ℝ)
hs : splitMany I s ≤ π
⊢ ∑ Ji ∈ π.boxes, f Ji = ∑ J ∈ π.boxes, ∑ J' ∈ (splitMany J s).boxes, f J'
Module: Mathlib.Analysis.BoxIntegral.UnitPartition

Goal state before:
pp: ι : Type u_1
n : ℕ
inst✝ : NeZero n
ν ν' : ι → ℤ
x✝ : ∃ x ∈ ↑(box n ν), x ∈ ↑(box n ν')
x : ι → ℝ
hx : x ∈ ↑(box n ν)
hx' : x ∈ ↑(box n ν')
⊢ ν = ν'

Tactic:
← mem_box_iff_index.mp hx,

Goal state after:
ι : Type u_1
n : ℕ
inst✝ : NeZero n
ν ν' : ι → ℤ
x✝ : ∃ x ∈ ↑(box n ν), x ∈ ↑(box n ν')
x : ι → ℝ
hx : x ∈ ↑(box n ν)
hx' : x ∈ ↑(box n ν')
⊢ index n x = ν'
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_4
inst✝³ : LinearOrder ι
inst✝² : LocallyFiniteOrder ι
inst✝¹ : OrderBot ι
inst✝ : WellFoundedLT ι
f : ι → E
⊢ f ⊥ - ∑ i ∈ Ico ⊥ ⊥, (𝕜 ∙ gramSchmidt 𝕜 f i).starProjection (f ⊥) = f ⊥

Tactic:
Finset.Ico_self,

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
ι : Type u_4
inst✝³ : LinearOrder ι
inst✝² : LocallyFiniteOrder ι
inst✝¹ : OrderBot ι
inst✝ : WellFoundedLT ι
f : ι → E
⊢ f ⊥ - ∑ i ∈ ∅, (𝕜 ∙ gramSchmidt 𝕜 f i).starProjection (f ⊥) = f ⊥
Module: Mathlib.Analysis.InnerProductSpace.ProdL2

Goal state before:
pp: case e'_3
𝕜 : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
E : Type u_4
F : Type u_5
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 F
K : Submodule 𝕜 E
inst✝ : K.HasOrthogonalProjection
x : E
y : E ⧸ K
f : (E ⧸ K) ≃ₗ[𝕜] ↥Kᗮ := K.quotientEquivOfIsCompl Kᗮ ⋯
h : ‖Quotient.mk ↑(f y)‖ = sInf ((fun x ↦ ‖↑(f y) + x‖) '' ↑K.toAddSubgroup)
⊢ ⨅ x, ‖↑(f y) - ↑x‖ = sInf ((fun x ↦ ‖↑(f y) + x‖) '' ↑K.toAddSubgroup)

Tactic:
sInf_image',

Goal state after:
case e'_3
𝕜 : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
E : Type u_4
F : Type u_5
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 F
K : Submodule 𝕜 E
inst✝ : K.HasOrthogonalProjection
x : E
y : E ⧸ K
f : (E ⧸ K) ≃ₗ[𝕜] ↥Kᗮ := K.quotientEquivOfIsCompl Kᗮ ⋯
h : ‖Quotient.mk ↑(f y)‖ = sInf ((fun x ↦ ‖↑(f y) + x‖) '' ↑K.toAddSubgroup)
⊢ ⨅ x, ‖↑(f y) - ↑x‖ = ⨅ a, ‖↑(f y) + ↑a‖
Module: Mathlib.Analysis.SumOverResidueClass

Goal state before:
pp: R : Type u_1
inst✝² : AddCommGroup R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalAddGroup R
m : ℕ
hm : NeZero m
k : ℕ
f : ℕ → R
g : ℕ → ℕ := fun n ↦ m * n + k
hg : Function.Injective g
n : ℕ
⊢ n ∉ range g → {n | ↑n = ↑k ∧ k ≤ n}.indicator f n = 0

Tactic:
hn

Goal state after:
R : Type u_1
inst✝² : AddCommGroup R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalAddGroup R
m : ℕ
hm : NeZero m
k : ℕ
f : ℕ → R
g : ℕ → ℕ := fun n ↦ m * n + k
hg : Function.Injective g
n : ℕ
hn : n ∉ range g
⊢ {n | ↑n = ↑k ∧ k ≤ n}.indicator f n = 0
Module: Mathlib.Analysis.SumOverResidueClass

Goal state before:
pp: m : ℕ
inst✝ : NeZero m
f : ℕ → ℝ
hf : Antitone f
k l : ZMod m
hs : Summable ({n | ↑n = k}.indicator f)
⊢ Summable ({n | ↑n = l}.indicator f)

Tactic:
by
  by_cases! hf₀ : ∀ n, 0 ≤ f n -- the interesting case
  · rw [← ZMod.natCast_zmod_val k, summable_indicator_mod_iff_summable] at hs
    have hl : (l.val + m : ZMod m) = l := by
      simp only [ZMod.natCast_val, ZMod.cast_id', id_eq, CharP.cast_eq_zero, add_zero]
    rw [← hl, ← Nat.cast_add, summable_indicator_mod_iff_summable]
    exact hs.of_nonneg_of_le (fun _ ↦ hf₀ _)
      fun _ ↦ hf <| Nat.add_le_add Nat.le.refl (k.val_lt.trans_le <| m.le_add_left l.val).le
  · obtain ⟨n, hn⟩ := hf₀
    exact (not_summable_indicator_mod_of_antitone_of_neg hf hn k hs).elim

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

Goal state before:
pp: α : Type u_1
inst✝ : NormedAddCommGroup α
f : ℕ → α
g : ℕ → ℝ
h : f =o[atTop] g
hg : 0 ≤ g
h'g : Tendsto (fun n ↦ ∑ i ∈ Finset.range n, g i) atTop atTop
A : ∀ (i : ℕ), ‖g i‖ = g i
B : ∀ (n : ℕ), ‖∑ i ∈ Finset.range n, g i‖ = ∑ i ∈ Finset.range n, g i
ε : ℝ
εpos : 0 < ε
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → ‖f b‖ ≤ ε / 2 * g b
this : (fun x ↦ ∑ i ∈ Finset.range N, f i) =o[atTop] fun n ↦ ∑ i ∈ Finset.range n, g i
n : ℕ
⊢ ‖∑ i ∈ Finset.range N, f i‖ ≤ ε / 2 * ‖∑ i ∈ Finset.range n, g i‖ →
    n ∈ Set.Ici N → ‖∑ i ∈ Finset.range n, f i‖ ≤ ε * ‖∑ i ∈ Finset.range n, g i‖

Tactic:
hn

Goal state after:
α : Type u_1
inst✝ : NormedAddCommGroup α
f : ℕ → α
g : ℕ → ℝ
h : f =o[atTop] g
hg : 0 ≤ g
h'g : Tendsto (fun n ↦ ∑ i ∈ Finset.range n, g i) atTop atTop
A : ∀ (i : ℕ), ‖g i‖ = g i
B : ∀ (n : ℕ), ‖∑ i ∈ Finset.range n, g i‖ = ∑ i ∈ Finset.range n, g i
ε : ℝ
εpos : 0 < ε
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → ‖f b‖ ≤ ε / 2 * g b
this : (fun x ↦ ∑ i ∈ Finset.range N, f i) =o[atTop] fun n ↦ ∑ i ∈ Finset.range n, g i
n : ℕ
hn : ‖∑ i ∈ Finset.range N, f i‖ ≤ ε / 2 * ‖∑ i ∈ Finset.range n, g i‖
⊢ n ∈ Set.Ici N → ‖∑ i ∈ Finset.range n, f i‖ ≤ ε * ‖∑ i ∈ Finset.range n, g i‖
Module: Mathlib.Analysis.Asymptotics.SpecificAsymptotics

Goal state before:
pp: α : Type u_1
inst✝ : NormedAddCommGroup α
f : ℕ → α
g : ℕ → ℝ
h : f =o[atTop] g
hg : 0 ≤ g
h'g : Tendsto (fun n ↦ ∑ i ∈ Finset.range n, g i) atTop atTop
A : ∀ (i : ℕ), ‖g i‖ = g i
B : ∀ (n : ℕ), ‖∑ i ∈ Finset.range n, g i‖ = ∑ i ∈ Finset.range n, g i
ε : ℝ
εpos : 0 < ε
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → ‖f b‖ ≤ ε / 2 * g b
this : (fun x ↦ ∑ i ∈ Finset.range N, f i) =o[atTop] fun n ↦ ∑ i ∈ Finset.range n, g i
⊢ ∀ᶠ (x : ℕ) in atTop, ‖∑ i ∈ Finset.range x, f i‖ ≤ ε * ‖∑ i ∈ Finset.range x, g i‖

Tactic:
filter_upwards [isLittleO_iff.1 this (half_pos εpos), Ici_mem_atTop N] with n hn Nn

Goal state after:
α : Type u_1
inst✝ : NormedAddCommGroup α
f : ℕ → α
g : ℕ → ℝ
h : f =o[atTop] g
hg : 0 ≤ g
h'g : Tendsto (fun n ↦ ∑ i ∈ Finset.range n, g i) atTop atTop
A : ∀ (i : ℕ), ‖g i‖ = g i
B : ∀ (n : ℕ), ‖∑ i ∈ Finset.range n, g i‖ = ∑ i ∈ Finset.range n, g i
ε : ℝ
εpos : 0 < ε
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → ‖f b‖ ≤ ε / 2 * g b
this : (fun x ↦ ∑ i ∈ Finset.range N, f i) =o[atTop] fun n ↦ ∑ i ∈ Finset.range n, g i
n : ℕ
hn : ‖∑ i ∈ Finset.range N, f i‖ ≤ ε / 2 * ‖∑ i ∈ Finset.range n, g i‖
Nn : n ∈ Set.Ici N
⊢ ‖∑ i ∈ Finset.range n, f i‖ ≤ ε * ‖∑ i ∈ Finset.range n, g i‖
Module: Mathlib.Analysis.BoxIntegral.Integrability

Goal state before:
pp: ι : Type u
E : Type v
inst✝⁴ : Fintype ι
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
f : (ι → ℝ) → E
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
I : Box ι
hb : ∃ C, ∀ x ∈ Box.Icc I, ‖f x‖ ≤ C
hc : ∀ᵐ (x : ι → ℝ) ∂μ, ContinuousAt f x
l : IntegrationParams
⊢ HasIntegral I l f μ.toBoxAdditive.toSMul (∫ (x : ι → ℝ) in ↑I, f x ∂μ)

Tactic:
by
  obtain ⟨y, hy⟩ := integrable_of_bounded_and_ae_continuous l hb μ hc
  convert! hy
  refine HasIntegral.unique (IntegrableOn.hasBoxIntegral ?_ ⊥ rfl) (HasIntegral.mono hy bot_le)
  constructor
  · let v := {x : (ι → ℝ) | ContinuousAt f x}
    have : AEStronglyMeasurable f (μ.restrict v) :=
      (continuousOn_of_forall_continuousAt fun _ h ↦ h).aestronglyMeasurable
      (measurableSet_of_continuousAt f)
    refine this.mono_measure (Measure.le_iff.2 fun s hs ↦ ?_)
    repeat rw [μ.restrict_apply hs]
    apply le_of_le_of_eq <| μ.mono s.inter_subset_left
    refine measure_eq_measure_of_null_sdiff s.inter_subset_left ?_ |>.symm
    rw [sdiff_self_inter, Set.sdiff_eq, ← nonpos_iff_eq_zero]
    grw [s.inter_subset_right]
    exact hc.le
  · have : IsFiniteMeasure (μ.restrict (Box.Icc I)) :=
      { measure_univ_lt_top := by simp [I.isCompact_Icc.measure_lt_top (μ := μ)] }
    have : IsFiniteMeasure (μ.restrict I) :=
      isFiniteMeasure_of_le _ (μ.restrict_mono Box.coe_subset_Icc le_rfl)
    obtain ⟨C, hC⟩ := hb
    refine .of_bounded (C := C) (Filter.eventually_iff_exists_mem.2 ?_)
    use I, self_mem_ae_restrict I.measurableSet_coe, fun y hy ↦ hC y (I.coe_subset_Icc hy)

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
n : ℕ
⊢ 0 < n →
    ↑(Nat.card ↑(⇑(Basis.ofZLatticeBasis ℝ L b).equivFun '' s ∩ (↑n)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))))) /
        ↑n ^ card ι =
      ↑(Nat.card ↑(s ∩ (↑n)⁻¹ • ↑L)) / ↑n ^ card ι

Tactic:
hn

Goal state after:
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
⊢ ↑(Nat.card ↑(⇑(Basis.ofZLatticeBasis ℝ L b).equivFun '' s ∩ (↑n)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))))) /
      ↑n ^ card ι =
    ↑(Nat.card ↑(s ∩ (↑n)⁻¹ • ↑L)) / ↑n ^ card ι
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)
this : (fun n ↦ ∑ i ∈ Finset.range n, (u i - l)) =o[atTop] fun n ↦ ↑n
⊢ (fun x ↦ (↑x)⁻¹ • ∑ i ∈ Finset.range x, u i - l) =o[atTop] fun _x ↦ 1

Tactic:
apply ((isBigO_refl (fun n : ℕ => (n : ℝ)⁻¹) atTop).smul_isLittleO this).congr' _ _

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
u : ℕ → E
l : E
h : Tendsto u atTop (𝓝 l)
this : (fun n ↦ ∑ i ∈ Finset.range n, (u i - l)) =o[atTop] fun n ↦ ↑n
⊢ (fun x ↦ (↑x)⁻¹ • ∑ i ∈ Finset.range x, (u i - l)) =ᶠ[atTop] fun x ↦ (↑x)⁻¹ • ∑ i ∈ Finset.range x, u i - l

E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
u : ℕ → E
l : E
h : Tendsto u atTop (𝓝 l)
this : (fun n ↦ ∑ i ∈ Finset.range n, (u i - l)) =o[atTop] fun n ↦ ↑n
⊢ (fun x ↦ (↑x)⁻¹ • ↑x) =ᶠ[atTop] fun _x ↦ 1
Module: Mathlib.Analysis.PSeries

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

Tactic:
hn

Goal state after:
case refine_2
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
k n✝ : ℕ
hk : k ≠ 0
h : k ≤ n✝
n : ℕ
hn : k ≤ n
⊢ ∑ i ∈ Ioc k n, (↑i ^ 2)⁻¹ ≤ (↑k)⁻¹ - (↑n)⁻¹ → ∑ i ∈ Ioc k (n + 1), (↑i ^ 2)⁻¹ ≤ (↑k)⁻¹ - (↑(n + 1))⁻¹
Module: Mathlib.Analysis.PSeries

Goal state before:
pp: a s : ℝ
hnorm : Tendsto (fun n ↦ ‖↑n‖) atTop atTop
a✝ : ℕ
⊢ ⌈|a|⌉₊ < a✝ → ↑a✝ + ?m.78 = |↑a✝ + a|

Tactic:
hn

Goal state after:
a s : ℝ
hnorm : Tendsto (fun n ↦ ‖↑n‖) atTop atTop
a✝ : ℕ
hn : ⌈|a|⌉₊ < a✝
⊢ ↑a✝ + ?m.78 = |↑a✝ + a|
Module: Mathlib.Algebra.MonoidAlgebra.Ideal

Goal state before:
pp: 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' := ⋯ }
hx : x ∈ RHS
d : A
hd : d ∈ s
d2 : A
hi : d2 + d ∈ x.coeff.support
⊢ single (d2 + d) (x.coeff (d2 + d)) ∈ Ideal.span (of' k A '' s)

Tactic:
simpa using Ideal.mul_mem_left _ (.single d2 <| x.coeff (d2 + d))
      (b := of' k A d) (Ideal.subset_span <| Set.mem_image_of_mem _ hd)

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

Goal state before:
pp: G : Type u_1
P : Type u_2
R : Type u_3
V : Type u_4
inst✝³ : Group G
inst✝² : MulAction G P
inst✝¹ : Semiring R
inst✝ : Zero V
f : R[G]
x : P → V
p : P
gh : G × P
⊢ gh ∈ Finset.SMulAntidiagonal p ⋯ ↔ f.coeff gh.1 ≠ 0 ∧ x gh.2 ≠ 0 ∧ gh.2 = gh.1⁻¹ • p

Tactic:
by
  rw [Finset.mem_smulAntidiagonal, eq_inv_smul_iff, Function.mem_support, Finset.mem_coe,
    Finsupp.mem_support_iff]

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

Goal state before:
pp: case inj
ι : Type u_1
M : Type u_3
inst✝³ : DecidableEq ι
inst✝² : AddMonoid ι
inst✝¹ : Semiring M
inst✝ : (m : M) → Decidable (m ≠ 0)
f g : ⨁ (x : ι), M
⊢ Function.Injective AddMonoidAlgebra.toDirectSum

Tactic:
apply Function.LeftInverse.injective
    apply AddMonoidAlgebra.toDirectSum_toAddMonoidAlgebra

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Coeff

Goal state before:
pp: case h₁
R : Type u_1
σ : Type u_2
inst✝ : CommSemiring R
s : σ →₀ ℕ
a : σ →₀ R
n : ℕ
hs : (s.sum fun x m ↦ m) = n
⊢ ⇑s ∉ a.support.piAntidiag n →
    (if s = indicator a.support fun i x ↦ s i then ↑(Nat.multinomial a.support ⇑s) * ∏ x ∈ a.support, a x ^ s x
      else 0) =
      0

Tactic:
· simp_rw [ite_eq_right_iff]
    intro hs' hs''
    rw [eq_indicator_self_iff] at hs''
    exfalso
    rw [Finset.mem_piAntidiag, not_and_or] at hs'
    rcases hs' with hs' | hs'
    · apply hs'
      rw [← hs, sum_of_support_subset _ hs'' _ (by simp)]
    · grind

Goal state after:
Module: Mathlib.Data.Nat.Choose.Multinomial

Goal state before:
pp: α : Type u_1
s : Finset α
a : α
n : ℕ
inst✝ : DecidableEq α
⊢ multinomial s (Pi.single a n) = 1

Tactic:
rw [← Nat.mul_right_inj (prod_ne_zero_iff.mpr (fun _ _ ↦ factorial_ne_zero _)), mul_one,
    multinomial_spec, sum_pi_single']

Goal state after:
α : Type u_1
s : Finset α
a : α
n : ℕ
inst✝ : DecidableEq α
⊢ (if a ∈ s then n else 0)! = ∏ x ∈ s, (Pi.single a n x)!
Module: Mathlib.Data.Nat.Choose.Multinomial

Goal state before:
pp: α : Type u_1
f : α → ℕ
a b : α
inst✝ : DecidableEq α
h : a ≠ b
⊢ multinomial {a, b} f = (f a + f b).choose (f a)

Tactic:
simp [binomial_eq h, choose_eq_factorial_div_factorial (Nat.le_add_right _ _)]

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Coeff

Goal state before:
pp: R : Type u_1
σ : Type u_2
inst✝ : CommSemiring R
s : σ →₀ ℕ
a : σ →₀ R
n : ℕ
hs : (s.sum fun x m ↦ m) ≠ n
⊢ coeff s ((linearCombination R X) a ^ n) = 0

Tactic:
classical
  simp only [sum, linearCombination_apply, Finset.sum_pow_eq_sum_piAntidiag, coeff_sum, ← map_pow,
    ← C_eq_coe_nat, coeff_C_mul, smul_eq_C_mul, mul_pow, Finset.prod_mul_distrib, ← map_prod,
    coeff_prod_X_pow, mul_ite, mul_one, mul_zero]
  apply Finset.sum_eq_zero (fun x hx ↦ ?_)
  rw [if_neg]
  rintro ⟨rfl⟩
  apply hs
  simp only [Finset.mem_piAntidiag] at hx
  rw [sum_of_support_subset _ (support_indicator_subset a.support _) _ (by simp), ← hx.1]
  congr
  ext i
  by_cases hi : i ∈ a.support
  · simp [Finsupp.indicator_of_mem hi]
  · grind [Finsupp.indicator_of_notMem hi]

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Division

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : IsLeftCancelAdd R
i : σ
p q r : MvPolynomial σ R
h : p = X i * q + r
hr : ∀ n ∈ r.support, n i = 0
n : σ →₀ ℕ
⊢ coeff (Finsupp.single i 1 + n) r = 0

Tactic:
← notMem_support_iff

Goal state after:
σ : Type u_1
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : IsLeftCancelAdd R
i : σ
p q r : MvPolynomial σ R
h : p = X i * q + r
hr : ∀ n ∈ r.support, n i = 0
n : σ →₀ ℕ
⊢ Finsupp.single i 1 + n ∉ r.support
Module: Mathlib.Data.Nat.Choose.Multinomial

Goal state before:
pp: case empty
α : Type u_1
R : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Semiring R
f : α → R
hc : (↑∅).Pairwise (Commute on f)
n : ℕ
⊢ (∑ i ∈ ∅, f i) ^ n = ∑ k ∈ ∅.piAntidiag n, ↑(multinomial ∅ k) * ∅.noncommProd (fun i ↦ f i ^ k i) ⋯

Tactic:
cases n <;> simp

Goal state after: