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

Goal state before:
pp: case pos
E : Type u
F : Type v
inst✝¹ : PseudoEMetricSpace F
inst✝ : PseudoEMetricSpace E
K : Set E
f : E → F
D : Set E
ε : ℝ≥0∞
comp : IsCompact K
hK : ∀ x ∈ K, oscillationWithin f D x < ε
S : ℝ → Set E := fun r ↦ {x | ∃ a > r, ediam (f '' (eball x (ENNReal.ofReal a) ∩ D)) ≤ ε}
S_open : ∀ r > 0, IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (S r)
S_cover : K ⊆ ⋃ r, ⋃ (_ : r > 0), S r
S_antitone : ∀ (r₁ r₂ : ℝ), r₁ ≤ r₂ → S r₂ ⊆ S r₁
T : Set ℝ
Tb : T ⊆ Real.lt✝ 0
Tfin : T.Finite
hT : K ⊆ ⋃ i ∈ T, S i
T_nonempty : T.Nonempty
⊢ ∃ r > 0, K ⊆ S r

Tactic:
use Tfin.isWF.min T_nonempty, Tb (Tfin.isWF.min_mem T_nonempty)
      intro x hx
      obtain ⟨r, hr⟩ := mem_iUnion.1 (hT hx)
      simp only [mem_iUnion, exists_prop] at hr
      exact (S_antitone _ r (IsWF.min_le Tfin.isWF T_nonempty hr.1)) hr.2

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✝ : ι
G : Type u
inst✝ : AddCommGroup G
I₀ : Box (Fin (n + 1))
i : Fin (n + 1)
f : ℝ → Box (Fin n) → G
fb : ↑(Set.Icc (I₀.lower i) (I₀.upper i)) → Fin n →ᵇᵃ[↑(I₀.face i)] G
hf : ∀ (x : ℝ) (hx : x ∈ Set.Icc (I₀.lower i) (I₀.upper i)) (J : Box (Fin n)), f x J = (fb ⟨x, hx⟩) J
⊢ ∀ (I : Box (Fin (n + 1))),
    ↑I ≤ ↑I₀ →
      ∀ {i_1 : Fin (n + 1)} {x : ℝ},
        x ∈ Set.Ioo (I.lower i_1) (I.upper i_1) →
          Option.elim' 0 (fun J ↦ f (J.upper i) (J.face i) - f (J.lower i) (J.face i)) (I.splitLower i_1 x) +
              Option.elim' 0 (fun J ↦ f (J.upper i) (J.face i) - f (J.lower i) (J.face i)) (I.splitUpper i_1 x) =
            f (I.upper i) (I.face i) - f (I.lower i) (I.face i)

Tactic:
by
      intro J hJ j x
      rw [WithTop.coe_le_coe] at hJ
      refine i.succAboveCases (fun hx => ?_) (fun j hx => ?_) j
      · simp only [Box.splitLower_def hx, Box.splitUpper_def hx, update_self, ← WithBot.some_eq_coe,
          Option.elim', Box.face, Function.comp_def, update_of_ne (Fin.succAbove_ne _ _)]
        abel
      · have : (J.face i : WithTop (Box (Fin n))) ≤ I₀.face i :=
          WithTop.coe_le_coe.2 (face_mono hJ i)
        rw [le_iff_Icc, @Box.Icc_eq_pi _ I₀] at hJ
        rw [hf _ (hJ J.upper_mem_Icc _ trivial), hf _ (hJ J.lower_mem_Icc _ trivial),
          ← (fb _).map_split_add this j x, ← (fb _).map_split_add this j x]
        have hx' : x ∈ Ioo ((J.face i).lower j) ((J.face i).upper j) := hx
        simp only [Box.splitLower_def hx, Box.splitUpper_def hx, Box.splitLower_def hx',
          Box.splitUpper_def hx', ← WithBot.some_eq_coe, Option.elim', Box.face_mk,
          update_of_ne (Fin.succAbove_ne _ _).symm, sub_add_sub_comm,
          update_comp_eq_of_injective _ (Fin.strictMono_succAbove i).injective j x, ← hf]
        simp only [Box.face]

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
this : Fintype ↑(s ∩ (↑n)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))))
⊢ ∑ J ∈ (prepartition n B).boxes, (volume.toBoxAdditive.toSMul J) (s.indicator F ((prepartition n B).tag J)) =
    (∑' (x : ↑(s ∩ (↑n)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))))), F ↑x) / ↑n ^ card ι

Tactic:
tsum_fintype,

Goal state after:
ι : 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 ℝ ι))))
⊢ ∑ J ∈ (prepartition n B).boxes, (volume.toBoxAdditive.toSMul J) (s.indicator F ((prepartition n B).tag J)) =
    (∑ b, F ↑b) / ↑n ^ card ι
Module: Mathlib.Analysis.BoxIntegral.Basic

Goal state before:
pp: ι : Type u
E : Type v
F : Type w
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
I : Box ι
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
π₁ π₂ : TaggedPrepartition I
h : Disjoint π₁.iUnion π₂.iUnion
⊢ integralSum f vol (π₁.disjUnion π₂ h) = integralSum f vol π₁ + integralSum f vol π₂

Tactic:
refine (Prepartition.sum_disj_union_boxes h _).trans
      (congr_arg₂ (· + ·) (sum_congr rfl fun J hJ => ?_) (sum_congr rfl fun J hJ => ?_))

Goal state after:
case refine_1
ι : Type u
E : Type v
F : Type w
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
I : Box ι
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
π₁ π₂ : TaggedPrepartition I
h : Disjoint π₁.iUnion π₂.iUnion
J : Box ι
hJ : J ∈ π₁.boxes
⊢ (vol J) (f ((π₁.disjUnion π₂ h).tag J)) = (vol J) (f (π₁.tag J))

case refine_2
ι : Type u
E : Type v
F : Type w
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
I : Box ι
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
π₁ π₂ : TaggedPrepartition I
h : Disjoint π₁.iUnion π₂.iUnion
J : Box ι
hJ : J ∈ π₂.boxes
⊢ (vol J) (f ((π₁.disjUnion π₂ h).tag J)) = (vol J) (f (π₂.tag J))
Module: Mathlib.Analysis.InnerProductSpace.Orientation

Goal state before:
pp: case pos
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = n + 1)
o : Orientation ℝ E (Fin (n + 1))
v : Fin (n + 1) → E
hv : Pairwise fun i j ↦ ⟪v i, v j⟫ = 0
this : FiniteDimensional ℝ E
hdim : finrank ℝ E = Fintype.card (Fin n.succ)
b : OrthonormalBasis (Fin n.succ) ℝ E := gramSchmidtOrthonormalBasis hdim v
hb : b.toBasis.det v = ∏ i, ⟪b i, v i⟫
i : Fin (n + 1)
hi : v i = 0
⊢ 0 = ∏ i, ‖v i‖

pp: case pos
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = n + 1)
o : Orientation ℝ E (Fin (n + 1))
v : Fin (n + 1) → E
hv : Pairwise fun i j ↦ ⟪v i, v j⟫ = 0
this : FiniteDimensional ℝ E
hdim : finrank ℝ E = Fintype.card (Fin n.succ)
b : OrthonormalBasis (Fin n.succ) ℝ E := gramSchmidtOrthonormalBasis hdim v
hb : b.toBasis.det v = ∏ i, ⟪b i, v i⟫
i : Fin (n + 1)
hi : v i = 0
⊢ |⟪b i, v i⟫| = 0

Tactic:
Finset.prod_eq_zero (Finset.mem_univ i)

Goal state after:
case pos
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = n + 1)
o : Orientation ℝ E (Fin (n + 1))
v : Fin (n + 1) → E
hv : Pairwise fun i j ↦ ⟪v i, v j⟫ = 0
this : FiniteDimensional ℝ E
hdim : finrank ℝ E = Fintype.card (Fin n.succ)
b : OrthonormalBasis (Fin n.succ) ℝ E := gramSchmidtOrthonormalBasis hdim v
hb : b.toBasis.det v = ∏ i, ⟪b i, v i⟫
i : Fin (n + 1)
hi : v i = 0
⊢ 0 = 0

case pos
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = n + 1)
o : Orientation ℝ E (Fin (n + 1))
v : Fin (n + 1) → E
hv : Pairwise fun i j ↦ ⟪v i, v j⟫ = 0
this : FiniteDimensional ℝ E
hdim : finrank ℝ E = Fintype.card (Fin n.succ)
b : OrthonormalBasis (Fin n.succ) ℝ E := gramSchmidtOrthonormalBasis hdim v
hb : b.toBasis.det v = ∏ i, ⟪b i, v i⟫
i : Fin (n + 1)
hi : v i = 0
⊢ ‖v i‖ = 0

case pos
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = n + 1)
o : Orientation ℝ E (Fin (n + 1))
v : Fin (n + 1) → E
hv : Pairwise fun i j ↦ ⟪v i, v j⟫ = 0
this : FiniteDimensional ℝ E
hdim : finrank ℝ E = Fintype.card (Fin n.succ)
b : OrthonormalBasis (Fin n.succ) ℝ E := gramSchmidtOrthonormalBasis hdim v
hb : b.toBasis.det v = ∏ i, ⟪b i, v i⟫
i : Fin (n + 1)
hi : v i = 0
⊢ |⟪b i, v i⟫| = 0
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
⊢ Summable ({n | ↑n = ↑k ∧ k ≤ n}.indicator f) ↔ Summable fun n ↦ f (m * n + k)

Tactic:
have hg' : ∀ n ∉ range g, {n : ℕ | (n : ZMod m) = k ∧ k ≤ n}.indicator f n = 0 := by
      intro n hn
      contrapose! hn
      exact (Nat.range_mul_add m k).symm ▸ mem_of_indicator_ne_zero 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
hg' : ∀ n ∉ range g, {n | ↑n = ↑k ∧ k ≤ n}.indicator f n = 0
⊢ Summable ({n | ↑n = ↑k ∧ k ≤ n}.indicator f) ↔ Summable fun n ↦ f (m * n + k)
Module: Mathlib.Analysis.SumOverResidueClass

Goal state before:
pp: R : Type u_1
inst✝⁵ : AddCommGroup R
inst✝⁴ : UniformSpace R
inst✝³ : IsUniformAddGroup R
inst✝² : CompleteSpace R
inst✝¹ : T0Space R
f : ℕ → R
hf : Summable f
N : ℕ
inst✝ : NeZero N
⊢ ∑' (b : ZMod N) (c : ℕ), f (N.residueClassesEquiv.symm (b, c)) = ∑ j, ∑' (m : ℕ), f (j.val + N * m)

pp: R : Type u_1
inst✝⁵ : AddCommGroup R
inst✝⁴ : UniformSpace R
inst✝³ : IsUniformAddGroup R
inst✝² : CompleteSpace R
inst✝¹ : T0Space R
f : ℕ → R
hf : Summable f
N : ℕ
inst✝ : NeZero N
⊢ Summable fun c ↦ f (N.residueClassesEquiv.symm c)

Tactic:
tsum_fintype,

Goal state after:
R : Type u_1
inst✝⁵ : AddCommGroup R
inst✝⁴ : UniformSpace R
inst✝³ : IsUniformAddGroup R
inst✝² : CompleteSpace R
inst✝¹ : T0Space R
f : ℕ → R
hf : Summable f
N : ℕ
inst✝ : NeZero N
⊢ ∑ b, ∑' (c : ℕ), f (N.residueClassesEquiv.symm (b, c)) = ∑ j, ∑' (m : ℕ), f (j.val + N * m)

R : Type u_1
inst✝⁵ : AddCommGroup R
inst✝⁴ : UniformSpace R
inst✝³ : IsUniformAddGroup R
inst✝² : CompleteSpace R
inst✝¹ : T0Space R
f : ℕ → R
hf : Summable f
N : ℕ
inst✝ : NeZero N
⊢ Summable fun c ↦ f (N.residueClassesEquiv.symm c)
Module: Mathlib.Analysis.PSeries

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

Tactic:
rw [sum_range_succ, ← sum_Ico_consecutive]

Goal state after:
M : Type u_1
inst✝² : AddCommMonoid M
inst✝¹ : PartialOrder M
inst✝ : IsOrderedAddMonoid M
f : ℕ → M
u : ℕ → ℕ
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
h_pos : ∀ (n : ℕ), 0 < u n
hu : Monotone u
n : ℕ
ihn : ∑ k ∈ Ico (u 0) (u n), f k ≤ ∑ k ∈ range n, (u (k + 1) - u k) • f (u k)
this : ∑ k ∈ Ico (u n) (u (n + 1)), f k ≤ (u (n + 1) - u n) • f (u n)
⊢ ∑ i ∈ Ico (u 0) ?n, f i + ∑ i ∈ Ico ?n (u (n + 1)), f i ≤
    ∑ x ∈ range n, (u (x + 1) - u x) • f (u x) + (u (n + 1) - u n) • f (u n)

case n
M : Type u_1
inst✝² : AddCommMonoid M
inst✝¹ : PartialOrder M
inst✝ : IsOrderedAddMonoid M
f : ℕ → M
u : ℕ → ℕ
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
h_pos : ∀ (n : ℕ), 0 < u n
hu : Monotone u
n : ℕ
ihn : ∑ k ∈ Ico (u 0) (u n), f k ≤ ∑ k ∈ range n, (u (k + 1) - u k) • f (u k)
this : ∑ k ∈ Ico (u n) (u (n + 1)), f k ≤ (u (n + 1) - u n) • f (u n)
⊢ ℕ

case hmn
M : Type u_1
inst✝² : AddCommMonoid M
inst✝¹ : PartialOrder M
inst✝ : IsOrderedAddMonoid M
f : ℕ → M
u : ℕ → ℕ
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
h_pos : ∀ (n : ℕ), 0 < u n
hu : Monotone u
n : ℕ
ihn : ∑ k ∈ Ico (u 0) (u n), f k ≤ ∑ k ∈ range n, (u (k + 1) - u k) • f (u k)
this : ∑ k ∈ Ico (u n) (u (n + 1)), f k ≤ (u (n + 1) - u n) • f (u n)
⊢ u 0 ≤ ?n

case hnk
M : Type u_1
inst✝² : AddCommMonoid M
inst✝¹ : PartialOrder M
inst✝ : IsOrderedAddMonoid M
f : ℕ → M
u : ℕ → ℕ
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
h_pos : ∀ (n : ℕ), 0 < u n
hu : Monotone u
n : ℕ
ihn : ∑ k ∈ Ico (u 0) (u n), f k ≤ ∑ k ∈ range n, (u (k + 1) - u k) • f (u k)
this : ∑ k ∈ Ico (u n) (u (n + 1)), f k ≤ (u (n + 1) - u n) • f (u n)
⊢ ?n ≤ u (n + 1)
Module: Mathlib.Analysis.PSeries

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

Tactic:
rw [sum_range_succ, ← sum_Ico_consecutive]

Goal state after:
M : Type u_1
inst✝² : AddCommMonoid M
inst✝¹ : PartialOrder M
inst✝ : IsOrderedAddMonoid M
f : ℕ → M
u : ℕ → ℕ
hf : ∀ ⦃m n : ℕ⦄, 1 < m → m ≤ n → f n ≤ f m
h_pos : ∀ (n : ℕ), 0 < u n
hu : Monotone u
n : ℕ
ihn : ∑ k ∈ range n, (u (k + 1) - u k) • f (u (k + 1)) ≤ ∑ k ∈ Ico (u 0 + 1) (u n + 1), f k
this : (u (n + 1) - u n) • f (u (n + 1)) ≤ ∑ k ∈ Ico (u n + 1) (u (n + 1) + 1), f k
⊢ ∑ x ∈ range n, (u (x + 1) - u x) • f (u (x + 1)) + (u (n + 1) - u n) • f (u (n + 1)) ≤
    ∑ i ∈ Ico (u 0 + 1) ?n, f i + ∑ i ∈ Ico ?n (u (n + 1) + 1), f i

case n
M : Type u_1
inst✝² : AddCommMonoid M
inst✝¹ : PartialOrder M
inst✝ : IsOrderedAddMonoid M
f : ℕ → M
u : ℕ → ℕ
hf : ∀ ⦃m n : ℕ⦄, 1 < m → m ≤ n → f n ≤ f m
h_pos : ∀ (n : ℕ), 0 < u n
hu : Monotone u
n : ℕ
ihn : ∑ k ∈ range n, (u (k + 1) - u k) • f (u (k + 1)) ≤ ∑ k ∈ Ico (u 0 + 1) (u n + 1), f k
this : (u (n + 1) - u n) • f (u (n + 1)) ≤ ∑ k ∈ Ico (u n + 1) (u (n + 1) + 1), f k
⊢ ℕ

case hmn
M : Type u_1
inst✝² : AddCommMonoid M
inst✝¹ : PartialOrder M
inst✝ : IsOrderedAddMonoid M
f : ℕ → M
u : ℕ → ℕ
hf : ∀ ⦃m n : ℕ⦄, 1 < m → m ≤ n → f n ≤ f m
h_pos : ∀ (n : ℕ), 0 < u n
hu : Monotone u
n : ℕ
ihn : ∑ k ∈ range n, (u (k + 1) - u k) • f (u (k + 1)) ≤ ∑ k ∈ Ico (u 0 + 1) (u n + 1), f k
this : (u (n + 1) - u n) • f (u (n + 1)) ≤ ∑ k ∈ Ico (u n + 1) (u (n + 1) + 1), f k
⊢ u 0 + 1 ≤ ?n

case hnk
M : Type u_1
inst✝² : AddCommMonoid M
inst✝¹ : PartialOrder M
inst✝ : IsOrderedAddMonoid M
f : ℕ → M
u : ℕ → ℕ
hf : ∀ ⦃m n : ℕ⦄, 1 < m → m ≤ n → f n ≤ f m
h_pos : ∀ (n : ℕ), 0 < u n
hu : Monotone u
n : ℕ
ihn : ∑ k ∈ range n, (u (k + 1) - u k) • f (u (k + 1)) ≤ ∑ k ∈ Ico (u 0 + 1) (u n + 1), f k
this : (u (n + 1) - u n) • f (u (n + 1)) ≤ ∑ k ∈ Ico (u n + 1) (u (n + 1) + 1), f k
⊢ ?n ≤ u (n + 1) + 1
Module: Mathlib.Analysis.PSeries

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

Tactic:
· suffices ¬Summable (fun n => ((n : ℝ) ^ p)⁻¹ : ℕ → ℝ) by
      have : ¬1 < p := fun hp₁ => hp.not_ge (zero_le_one.trans hp₁.le)
      simpa only [this, iff_false]
    intro h
    obtain ⟨k : ℕ, hk₁ : ((k : ℝ) ^ p)⁻¹ < 1, hk₀ : k ≠ 0⟩ :=
      ((h.tendsto_cofinite_zero.eventually (gt_mem_nhds zero_lt_one)).and
          (eventually_cofinite_ne 0)).exists
    apply hk₀
    rw [← pos_iff_ne_zero, ← @Nat.cast_pos ℝ] at hk₀
    simpa [inv_lt_one₀ (rpow_pos_of_pos hk₀ _), one_lt_rpow_iff_of_pos hk₀, hp,
      hp.not_gt, hk₀] using hk₁

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

Goal state before:
pp: case inr
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'
⊢ ∃ ε, 0 < ε ∧ ∀ (x : ↥L) (i : ι), ε * ↑|(b.repr x) i| ≤ ‖x‖

Tactic:
obtain ⟨ε, hε, H⟩ := this (b.map e.symm) inst

Goal state after:
case inr
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‖
⊢ ∃ ε, 0 < ε ∧ ∀ (x : ↥L) (i : ι), ε * ↑|(b.repr x) i| ≤ ‖x‖
Module: Mathlib.Analysis.PSeries

Goal state before:
pp: α : Type u_1
x : α
inst✝ : RCLike α
q k : ℕ
hq : 1 < q
⊢ Summable fun n ↦ ‖x‖ / ‖(↑n + ↑k) ^ q‖

Tactic:
apply Summable.const_div

Goal state after:
α : Type u_1
x : α
inst✝ : RCLike α
q k : ℕ
hq : 1 < q
⊢ Summable fun x ↦ 1 / ‖(↑x + ↑k) ^ q‖
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
this✝ : ∀ J ∈ B', ‖μ.toBoxAdditive J • (f (t₁ J) - f (t₂ J))‖ ≤ μ.toBoxAdditive J * (2 * C)
this : (∑ J ∈ B', μ ↑J).toReal ≤ ε₂
⊢ (∑ a ∈ B', μ ↑a).toReal * (2 * C) ≤ ε / 2

Tactic:
linarith [mul_le_mul_of_nonneg_right this <| (mul_nonneg_iff_of_pos_left two_pos).2 C0]

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
⊢ (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) =
    ↑s.multinomial * s.prod fun r m ↦ a r ^ m

Tactic:
simp_rw [eq_indicator_self_iff]
    split_ifs with hs'
    · rw [prod_of_support_subset _ hs' _ (by simp), Finsupp.multinomial_of_support_subset hs']
    · rw [Finset.subset_iff] at hs'
      simp only [Finsupp.mem_support_iff, ne_eq, not_forall, Decidable.not_not] at hs'
      obtain ⟨i, hsi, hai⟩ := hs'
      rw [← mul_prod_erase _ i _ (by simpa), hai, zero_pow hsi, zero_mul, mul_zero]

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

Goal state before:
pp: R : Type u_1
σ : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Fintype σ
d : σ →₀ ℕ
n : ℕ
⊢ coeff d ((∑ i, X i) ^ n) = ↑(if (d.sum fun x m ↦ m) = n then d.multinomial else 0)

Tactic:
have : (∑ i, X i : MvPolynomial σ R) = ∑ i, (1 : σ → R) i • X i := by simp

Goal state after:
R : Type u_1
σ : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Fintype σ
d : σ →₀ ℕ
n : ℕ
this : ∑ i, X i = ∑ i, 1 i • X i
⊢ coeff d ((∑ i, X i) ^ n) = ↑(if (d.sum fun x m ↦ m) = n then d.multinomial else 0)
Module: Mathlib.Algebra.MvPolynomial.Division

Goal state before:
pp: case mpr.inr
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
r : R
i j : σ →₀ ℕ
hij : i ≤ j
d : R
⊢ (monomial j) (r * d) = (monomial i) r * (monomial (j - i)) d

Tactic:
monomial_mul,

Goal state after:
case mpr.inr
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
r : R
i j : σ →₀ ℕ
hij : i ≤ j
d : R
⊢ (monomial j) (r * d) = (monomial (i + (j - i))) (r * d)
Module: Mathlib.Algebra.MvPolynomial.Division

Goal state before:
pp: case inr.succ.refine_1
σ : Type u_1
R : Type u_3
inst✝¹ : CommRing R
p✝ q✝ : MvPolynomial σ R
inst✝ : IsCancelMulZero R
n✝ : σ →₀ ℕ
hR : Nontrivial R
d : ℕ
hd :
  ∀ (n : σ →₀ ℕ),
    Finsupp.degree n = d →
      ∀ (p q : MvPolynomial σ R), p ∣ (monomial n) 1 * q ↔ ∃ m r, m ≤ n ∧ r ∣ q ∧ p = (monomial m) 1 * r
n : σ →₀ ℕ
hn : Finsupp.degree n = d + 1
p q : MvPolynomial σ R
hp : p ∣ (monomial n) 1 * q
⊢ ∃ m r, m ≤ n ∧ r ∣ q ∧ p = (monomial m) 1 * r

Tactic:
obtain ⟨i, hi⟩ : n.support.Nonempty := by
        rw [Finsupp.support_nonempty_iff]
        intro hn'
        simp [hn'] at hn

Goal state after:
case inr.succ.refine_1
σ : Type u_1
R : Type u_3
inst✝¹ : CommRing R
p✝ q✝ : MvPolynomial σ R
inst✝ : IsCancelMulZero R
n✝ : σ →₀ ℕ
hR : Nontrivial R
d : ℕ
hd :
  ∀ (n : σ →₀ ℕ),
    Finsupp.degree n = d →
      ∀ (p q : MvPolynomial σ R), p ∣ (monomial n) 1 * q ↔ ∃ m r, m ≤ n ∧ r ∣ q ∧ p = (monomial m) 1 * r
n : σ →₀ ℕ
hn : Finsupp.degree n = d + 1
p q : MvPolynomial σ R
hp : p ∣ (monomial n) 1 * q
i : σ
hi : i ∈ n.support
⊢ ∃ m r, m ≤ n ∧ r ∣ q ∧ p = (monomial m) 1 * r
Module: Mathlib.Algebra.MvPolynomial.Expand

Goal state before:
pp: R : Type u_1
σ : Type u_2
inst✝ : CommRing R
p : ℕ
hp : p ≠ 0
⊢ IsLocalHom (expand p)

Tactic:
refine ⟨fun f hf => ?_⟩

Goal state after:
R : Type u_1
σ : Type u_2
inst✝ : CommRing R
p : ℕ
hp : p ≠ 0
f : MvPolynomial σ R
hf : IsUnit ((expand p) f)
⊢ IsUnit f
Module: Mathlib.Data.Nat.Choose.Multinomial

Goal state before:
pp: α : Type u_1
R : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Semiring R
x : α → R
s : Finset α
hc : (↑s).Pairwise (Commute on x)
⊢ ∀ (n : ℕ), s.sum x ^ n = ∑ k, ↑(↑↑k).countPerms * (Multiset.map x ↑↑k).noncommProd ⋯

Tactic:
by
  induction s using Finset.induction with
  | empty =>
    rw [sum_empty]
    rintro (_ | n)
    · rw [_root_.pow_zero, Fintype.sum_subsingleton]
      swap
      · exact ⟨0, by simp [eq_iff_true_of_subsingleton]⟩
      convert! (@one_mul R _ _).symm
      convert! @Nat.cast_one R _
      simp
    · rw [_root_.pow_succ, mul_zero]
      have : IsEmpty (Finset.sym (∅ : Finset α) n.succ) := Finset.instIsEmpty
      apply (Fintype.sum_empty _).symm
  | insert a s ha ih => ?_
  intro n; specialize ih (hc.mono <| s.subset_insert a)
  rw [sum_insert ha, (Commute.sum_right s _ _ _).add_pow, sum_range]; swap
  · exact fun _ hb => hc (mem_insert_self a s) (mem_insert_of_mem hb)
      (ne_of_mem_of_not_mem hb ha).symm
  · simp_rw [ih, mul_sum, sum_mul, sum_sigma', univ_sigma_univ]
    refine (Fintype.sum_equiv (symInsertEquiv ha) _ _ fun m => ?_).symm
    rw [m.1.1.countPerms_filter_ne a]
    conv in m.1.1.map _ => rw [← m.1.1.filter_add_not (a = ·), Multiset.map_add]
    simp_rw [Multiset.noncommProd_add, m.1.1.filter_eq, Multiset.map_replicate, m.1.2]
    rw [Multiset.noncommProd_eq_pow_card _ _ _ fun _ => Multiset.eq_of_mem_replicate]
    rw [Multiset.card_replicate, Nat.cast_mul, mul_assoc, Nat.cast_comm]
    congr 1; simp_rw [← mul_assoc, Nat.cast_comm]; rfl

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

Goal state before:
pp: case trans
m : Multiset ℕ
l✝ l'✝ l l' l'' : List ℕ
h : l.Perm l'
h' : l'.Perm l''
ih : l.multinomial = l'.multinomial
ih' : l'.multinomial = l''.multinomial
⊢ l.multinomial = l''.multinomial

Tactic:
rw [ih, ih']

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: case pos
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
b : σ →₀ ℕ
hb : b ∈ (f + g).support
hf : b ∈ f.support
⊢ m.toSyn b ≤ m.toSyn (m.degree f)

Tactic:
exact m.le_degree hf

Goal state after:
Module: Mathlib.Algebra.NonAssoc.LieAdmissible.Defs

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝¹ : CommRing R
inst✝ : LieAdmissibleRing L
x y z : L
⊢ ⁅x + y, z⁆ = ⁅x, z⁆ + ⁅y, z⁆

Tactic:
simp only [Ring.lie_def, mul_add, add_mul]

Goal state after:
R : Type u_1
L : Type u_2
inst✝¹ : CommRing R
inst✝ : LieAdmissibleRing L
x y z : L
⊢ x * z + y * z - (z * x + z * y) = x * z - z * x + (y * z - z * y)