mathlib-initiative/mathlib-tactics huggingface dataset:
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 : Set E
ht : MeasurableSet t
h''t : μ t ≠ ∞
ε : ℝ≥0∞
εpos : 0 < ε
h't : μ t ≠ 0
n : ℕ
npos : 0 < n
hn : μ (t \ closedBall 0 ↑n) < ε / 2 * μ t
L : Tendsto (fun r ↦ μ (s ∩ ({x} + r • (t ∩ closedBall 0 ↑n))) / μ ({x} + r • t)) (𝓝[>] 0) (𝓝 0)
r : ℝ
hr : μ (s ∩ ({x} + r • (t ∩ closedBall 0 ↑n))) / μ ({x} + r • t) < ε / 2
rpos : 0 < r
I : μ (s ∩ ({x} + r • t)) ≤ μ (s ∩ ({x} + r • (t ∩ closedBall 0 ↑n))) + μ ({x} + r • (t \ closedBall 0 ↑n))
⊢ μ (s ∩ ({x} + r • (t ∩ closedBall 0 ↑n))) / μ ({x} + r • t) + μ ({x} + r • (t \ closedBall 0 ↑n)) / μ ({x} + r • t) <
    ε / 2 + ε / 2

Tactic:
apply ENNReal.add_lt_add hr _

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 : Set E
ht : MeasurableSet t
h''t : μ t ≠ ∞
ε : ℝ≥0∞
εpos : 0 < ε
h't : μ t ≠ 0
n : ℕ
npos : 0 < n
hn : μ (t \ closedBall 0 ↑n) < ε / 2 * μ t
L : Tendsto (fun r ↦ μ (s ∩ ({x} + r • (t ∩ closedBall 0 ↑n))) / μ ({x} + r • t)) (𝓝[>] 0) (𝓝 0)
r : ℝ
hr : μ (s ∩ ({x} + r • (t ∩ closedBall 0 ↑n))) / μ ({x} + r • t) < ε / 2
rpos : 0 < r
I : μ (s ∩ ({x} + r • t)) ≤ μ (s ∩ ({x} + r • (t ∩ closedBall 0 ↑n))) + μ ({x} + r • (t \ closedBall 0 ↑n))
⊢ μ ({x} + r • (t \ closedBall 0 ↑n)) / μ ({x} + r • t) < ε / 2
Module: Mathlib.Analysis.BoxIntegral.Partition.Split

Goal state before:
pp: ι : Type u_1
I : Box ι
i : ι
x : ℝ
⊢ I.splitLower i x = ⊥ ↔ x ≤ I.lower i

Tactic:
rw [splitLower, mk'_eq_bot, exists_update_iff I.upper fun j y => y ≤ I.lower j]
  simp [(I.lower_lt_upper _).not_ge]

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

Goal state before:
pp: E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Set E
hs : DiscreteTopology ↥(span ℤ s)
F : Submodule ℝ E := span ℝ s
⊢ Set.finrank ℝ s = Set.finrank ℤ s

Tactic:
let L : Submodule ℤ (span ℝ s) := comap (F.restrictScalars ℤ).subtype (span ℤ s)

Goal state after:
E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Set E
hs : DiscreteTopology ↥(span ℤ s)
F : Submodule ℝ E := span ℝ s
L : Submodule ℤ ↥(span ℝ s) := comap (Submodule.restrictScalars ℤ F).subtype (span ℤ s)
⊢ Set.finrank ℝ s = Set.finrank ℤ s
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 ι
A : ι → Submodule 𝕜 E
inst✝¹ : DecidableEq ι
h : IsInternal A
α : ι → Type u_7
inst✝ : (i : ι) → Fintype (α i)
hV : OrthogonalFamily 𝕜 (fun i ↦ ↥(A i)) fun i ↦ (A i).subtypeₗᵢ
v : (i : ι) → OrthonormalBasis (α i) 𝕜 ↥(A i)
a : (i : ι) × α i
⊢ (collectedOrthonormalBasis hV h v) a ∈ A a.fst

Tactic:
simp [DirectSum.IsInternal.collectedOrthonormalBasis]

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

Goal state before:
pp: ι : Type u_1
inst✝ : Fintype ι
I : Box ι
⊢ (volume (univ.pi fun i ↦ Ioc (I.lower i) (I.upper i))).toReal = ∏ i, (I.upper i - I.lower i)

Tactic:
Real.volume_pi_Ioc_toReal I.lower_le_upper

Goal state after:
ι : Type u_1
inst✝ : Fintype ι
I : Box ι
⊢ ∏ i, (I.upper i - I.lower i) = ∏ i, (I.upper i - I.lower i)
Module: Mathlib.Analysis.BoxIntegral.UnitPartition

Goal state before:
pp: ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
ν : ι → ℤ
⊢ ∏ i, volume (Set.Ioc ((box n ν).lower i) ((box n ν).upper i)) = 1 / ↑n ^ card ι

Tactic:
Real.volume_Ioc,

Goal state after:
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
ν : ι → ℤ
⊢ ∏ x, ENNReal.ofReal ((box n ν).upper x - (box n ν).lower x) = 1 / ↑n ^ card ι
Module: Mathlib.LinearAlgebra.Orientation

Goal state before:
pp: case h
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
inst✝ : IsEmpty ι
f : M ≃ₗ[R] M
g : M [⋀^ι]→ₗ[R] R
hg : g ≠ 0
⊢ (map ι f) (rayOfNeZero R g hg) = rayOfNeZero R g hg

Tactic:
rw [Orientation.map_apply]

Goal state after:
case h
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
inst✝ : IsEmpty ι
f : M ≃ₗ[R] M
g : M [⋀^ι]→ₗ[R] R
hg : g ≠ 0
⊢ rayOfNeZero R (g.compLinearMap ↑f.symm) ⋯ = rayOfNeZero R g hg
Module: Mathlib.LinearAlgebra.Orientation

Goal state before:
pp: R : Type u_1
inst✝⁷ : CommRing R
inst✝⁶ : LinearOrder R
inst✝⁵ : IsStrictOrderedRing R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
ι : Type u_3
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Nonempty ι
e : Basis ι R M
x : Orientation R M ι
⊢ (e.adjustToOrientation x).orientation = x

Tactic:
by
  rw [adjustToOrientation]
  split_ifs with h
  · exact h
  · rw [orientation_neg_single, eq_comm, ← orientation_ne_iff_eq_neg, ne_comm]
    exact h

Goal state after:
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
v : Fin (n✝ + 1) → E
⊢ |o.volumeForm v| = |b.toBasis.det v|

Tactic:
· rw [o.volumeForm_robust (b.adjustToOrientation o) (b.orientation_adjustToOrientation o),
      b.abs_det_adjustToOrientation]

Goal state after:
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)) ≤
    μ.real ↑I * ↑ε

Tactic:
rw [← hπp.iUnion_eq, π.measure_iUnion_toReal, sum_mul, integralSum]
    refine dist_sum_sum_le_of_le _ fun J _ => ?_; dsimp
    rw [dist_eq_norm, ← smul_sub, norm_smul, Real.norm_eq_abs, abs_of_nonneg measureReal_nonneg]
    gcongr
    rw [← dist_eq_norm']; exact hNxε _

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
⊢ (fun n ↦ ∑ i ∈ Finset.range n, f i) =o[atTop] fun n ↦ ∑ i ∈ Finset.range n, g i

Tactic:
have A : ∀ i, ‖g i‖ = g i := fun i => Real.norm_of_nonneg (hg i)
  have B : ∀ n, ‖∑ i ∈ range n, g i‖ = ∑ i ∈ range n, g i := fun n => by
    rwa [Real.norm_eq_abs, abs_sum_of_nonneg']
  apply isLittleO_iff.2 fun ε εpos => _
  intro ε εpos
  obtain ⟨N, hN⟩ : ∃ N : ℕ, ∀ b : ℕ, N ≤ b → ‖f b‖ ≤ ε / 2 * g b := by
    simpa only [A, eventually_atTop] using isLittleO_iff.mp h (half_pos εpos)
  have : (fun _ : ℕ => ∑ i ∈ range N, f i) =o[atTop] fun n : ℕ => ∑ i ∈ range n, g i := by
    apply isLittleO_const_left.2
    exact Or.inr (h'g.congr fun n => (B n).symm)
  filter_upwards [isLittleO_iff.1 this (half_pos εpos), Ici_mem_atTop N] with n hn Nn
  calc
    ‖∑ i ∈ range n, f i‖ = ‖(∑ i ∈ range N, f i) + ∑ i ∈ Ico N n, f i‖ := by
      rw [sum_range_add_sum_Ico _ Nn]
    _ ≤ ‖∑ i ∈ range N, f i‖ + ‖∑ i ∈ Ico N n, f i‖ := norm_add_le _ _
    _ ≤ ‖∑ i ∈ range N, f i‖ + ∑ i ∈ Ico N n, ε / 2 * g i :=
      (add_le_add le_rfl (norm_sum_le_of_le _ fun i hi => hN _ (mem_Ico.1 hi).1))
    _ ≤ ‖∑ i ∈ range N, f i‖ + ∑ i ∈ range n, ε / 2 * g i := by
      gcongr
      · exact fun i _ _ ↦ mul_nonneg (half_pos εpos).le (hg i)
      · rw [range_eq_Ico]
        exact Ico_subset_Ico zero_le le_rfl
    _ ≤ ε / 2 * ‖∑ i ∈ range n, g i‖ + ε / 2 * ∑ i ∈ range n, g i := by rw [← mul_sum]; gcongr
    _ = ε * ‖∑ i ∈ range n, g i‖ := by
      simp only [B]
      ring

Goal state after:
Module: Mathlib.Analysis.PSeries

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

Tactic:
exact sum_schlomilch_le' hf h_pos hu n

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✝¹ : AddCommMonoid V
inst✝ : SMulWithZero R V
f : R[G]
x : P → V
p : P
hp : ((↑f.coeff.support).smulAntidiagonal (Function.support x) p).Finite
s : Set (G × P) := ↑(Finset.SMulAntidiagonal p hp)
x✝¹ : G × P
h₁ : x✝¹ ∈ s
x✝ : G × P
h₂ : x✝ ∈ s
h : x✝¹.1 = x✝.1
⊢ x✝¹ = x✝

Tactic:
by
    rw [Finset.mem_coe, mem_smulAntidiagonal_of_group] at h₁ h₂
    aesop

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

Goal state before:
pp: case inl
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : FiniteDimensional ℝ E
L : Submodule ℤ E
inst✝ : DiscreteTopology ↥L
r : ℝ
hr : r < -↑(finrank ℤ ↥L)
x : E
h✝ : Subsingleton ↥L
⊢ Summable fun z ↦ ‖↑z - x‖ ^ r

pp: case inr
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : FiniteDimensional ℝ E
L : Submodule ℤ E
inst✝ : DiscreteTopology ↥L
r : ℝ
hr : r < -↑(finrank ℤ ↥L)
x : E
h✝ : Nontrivial ↥L
⊢ Summable fun z ↦ ‖↑z - x‖ ^ r

Tactic:
· exact .of_finite

Goal state after:
case inr
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : FiniteDimensional ℝ E
L : Submodule ℤ E
inst✝ : DiscreteTopology ↥L
r : ℝ
hr : r < -↑(finrank ℤ ↥L)
x : E
h✝ : Nontrivial ↥L
⊢ Summable fun z ↦ ‖↑z - x‖ ^ r
Module: Mathlib.Algebra.Module.ZLattice.Summable

Goal state before:
pp: E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : FiniteDimensional ℝ E
L : Submodule ℤ E
inst✝ : DiscreteTopology ↥L
n : ℤ
hn : n < -↑(finrank ℤ ↥L)
⊢ Summable fun z ↦ ‖z‖ ^ n

Tactic:
by
  simpa using summable_norm_sub_zpow L n hn 0

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

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

Tactic:
rw [binomial_eq_choose h, binomial_eq_choose h, mul_comm (f a).succ, Function.update_self,
    Function.update_of_ne h.symm]

Goal state after:
α : Type u_1
f : α → ℕ
a b : α
inst✝ : DecidableEq α
h : a ≠ b
⊢ (f a + f b).succ * (f a + f b).choose (f a) = ((f a).succ + f b).choose (f a).succ * (f a).succ
Module: Mathlib.Algebra.MvPolynomial.Expand

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
p : ℕ
d : σ →₀ ℕ
r : R
⊢ (expand p) ((monomial d) r) = (monomial (p • d)) r

Tactic:
rw [expand, bind₁_monomial, monomial_eq, Finsupp.prod_of_support_subset _ Finsupp.support_smul]
  · simp [pow_mul]
  · simp

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

Goal state before:
pp: case cons.e_a.e_a
m' : Multiset ℕ
x : ℕ
m : Multiset ℕ
hind : (m + m').multinomial = (m + m').sum.choose m.sum * m.multinomial * m'.multinomial
⊢ (x + (m.sum + m'.sum)).choose x * (m.sum + m'.sum).choose m.sum =
    (x + (m.sum + m'.sum)).choose (x + m.sum) * (x + m.sum).choose x

Tactic:
rw [← Nat.choose_symm (Nat.le_add_right _ _), add_tsub_cancel_left, eq_comm,
      Nat.choose_mul (Nat.le_add_right _ _), ← Nat.choose_symm (Nat.le_add_right x _)]

Goal state after:
case cons.e_a.e_a
m' : Multiset ℕ
x : ℕ
m : Multiset ℕ
hind : (m + m').multinomial = (m + m').sum.choose m.sum * m.multinomial * m'.multinomial
⊢ (x + (m.sum + m'.sum)).choose (x + (m.sum + m'.sum) - x) * (x + (m.sum + m'.sum) - x).choose (x + m.sum - x) =
    (x + (m.sum + m'.sum)).choose (m.sum + m'.sum) * (m.sum + m'.sum).choose m.sum
Module: Mathlib.Algebra.MvPolynomial.NoZeroDivisors

Goal state before:
pp: case hp
R : Type u_1
σ : Type u_2
n : σ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
inst✝ : NoZeroDivisors R
hp : p ≠ 0
hq : q ≠ 0
⊢ (optionEquivLeft R { b // b ≠ n }) ((renameEquiv R (optionSubtypeNe n).symm) p) ≠ 0

Tactic:
simpa [-renameEquiv_apply, EmbeddingLike.map_eq_zero_iff]

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

Goal state before:
pp: case hq
R : Type u_1
σ : Type u_2
n : σ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
inst✝ : NoZeroDivisors R
hp : p ≠ 0
hq : q ≠ 0
⊢ (optionEquivLeft R { b // b ≠ n }) ((renameEquiv R (optionSubtypeNe n).symm) q) ≠ 0

Tactic:
simpa [-renameEquiv_apply, EmbeddingLike.map_eq_zero_iff]

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

Goal state before:
pp: R : Type u_1
σ : Type u_2
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
f : MvPolynomial σ R
a : R
ha : a ≠ 0
hf : f ∣ C a
this : f.totalDegree = 0
⊢ coeff 0 f ∣ a ∧ f = C (coeff 0 f)

Tactic:
by
      rw [totalDegree_eq_zero_iff_eq_C] at this
      refine ⟨?_, this⟩
      rw [this, C_dvd_iff_dvd_coeff] at hf
      simpa using hf 0

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

Goal state before:

Tactic:
dist (∑ J ∈ π.boxes with tag π J ∉ s, vol J (f (tag π J)))
      (∑ J ∈ π.boxes with tag π J ∉ s, g J)
      ≤ ∑ J ∈ π.boxes with tag π J ∉ s, ε' * B J := dist_sum_sum_le_of_le _ fun J hJ ↦ by
      rw [Finset.mem_filter] at hJ; obtain ⟨hJ, hJs⟩ := hJ
      refine Hδ₂ c _ ⟨π.tag_mem_Icc _, hJs⟩ _ ε'0 _ (π.le_of_mem' _ hJ) ?_ (fun hH => hπδ.2 hH J hJ)
        fun hD => (Finset.le_sup hJ).trans (hπδ.3 hD)
      convert! hπδ.1 J hJ using 3; exact (if_neg hJs).symm
    _ ≤ ∑ J ∈ π.boxes, ε' * B J := by
      gcongr
      · exact fun _ _ _ ↦ mul_nonneg ε'0.le (hB0 _)
      · apply filter_subset
    _ = B I * ε' := by rw [← mul_sum, B.sum_partition_boxes le_rfl hπp, mul_comm]
    _ ≤ ε / 2 := hεI.le

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

Goal state before:
pp: case mpr
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
hf : f.support.Nonempty
⊢ m.degree f ∈ f.support

Tactic:
degree

Goal state after:
case mpr
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
hf : f.support.Nonempty
⊢ m.toSyn.symm (f.support.sup ⇑m.toSyn) ∈ f.support
Module: Mathlib.Data.Sym.Card

Goal state before:
pp: α : Type u_2
inst✝¹ : Fintype α
k : ℕ
inst✝ : Fintype (Sym α k)
⊢ Fintype.card (Sym α k) = (Fintype.card α + k - 1).choose k

Tactic:
card_sym_eq_multichoose,

Goal state after:
α : Type u_2
inst✝¹ : Fintype α
k : ℕ
inst✝ : Fintype (Sym α k)
⊢ (Fintype.card α).multichoose k = (Fintype.card α + k - 1).choose k
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
⊢ m.degree (m.leadingTerm f) = m.degree f

Tactic:
simp only [leadingTerm, degree_monomial, leadingCoeff_eq_zero_iff, ite_eq_right_iff]
  simp_intro h

Goal state after:
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: case some
n k : ℕ
pk : Prime k
dk : k ∣ n
dkk : ¬k * k ∣ n
this : ∀ (p : ℕ), Prime p → p * p ∣ n → k * (p * p) ∣ n
d : ℕ
H1 : Prime d
H2 : k * (d * d) ∣ n
H3 : ∀ (p : ℕ), Prime p → k * (p * p) ∣ n → d ≤ p
⊢ n.MinSqFacProp (some d)

Tactic:
exact ⟨H1, dvd_trans (dvd_mul_left _ _) H2, fun p pp dp => H3 _ pp (this _ pp dp)⟩

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
hf : m.leadingCoeff f ∈ R⁰
h0 : f = 0 ∨ g = 0
⊢ m.withBotDegree (f * g) = m.withBotDegree f + m.withBotDegree g

Tactic:
rcases h0 with h0 | h0 <;> simp [h0]

Goal state after:
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: case mpr
n : ℕ
h0 : n ≠ 0
a : ℕ
⊢ (∃ a_1 ∈ (normalizedFactors n).toFinset.powerset, a_1.val.prod = a) → (a ∣ n ∧ n ≠ 0) ∧ Squarefree a

Tactic:
rintro ⟨s, hs, rfl⟩
      rw [Finset.mem_powerset, ← Finset.val_le_iff, Multiset.toFinset_val] at hs
      have hs0 : s.val.prod ≠ 0 := by
        rw [Ne, Multiset.prod_eq_zero_iff]
        intro con
        apply
          not_irreducible_zero
            (irreducible_of_normalized_factor 0 (Multiset.mem_dedup.1 (Multiset.mem_of_le hs con)))
      rw [(prod_normalizedFactors h0).symm.dvd_iff_dvd_right]
      refine ⟨⟨Multiset.prod_dvd_prod_of_le (le_trans hs (Multiset.dedup_le _)), h0⟩, ?_⟩
      have h :=
        UniqueFactorizationMonoid.factors_unique irreducible_of_normalized_factor
          (fun x hx =>
            irreducible_of_normalized_factor x
              (Multiset.mem_of_le (le_trans hs (Multiset.dedup_le _)) hx))
          (prod_normalizedFactors hs0)
      rw [associated_eq_eq, Multiset.rel_eq] at h
      rw [UniqueFactorizationMonoid.squarefree_iff_nodup_normalizedFactors hs0, h]
      apply s.nodup

Goal state after:
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: n : ℕ
h0 : n ≠ 0
x : Finset ℕ
hx : x ⊆ (normalizedFactors n).toFinset
y : Finset ℕ
hy : y ⊆ (normalizedFactors n).toFinset
h : x.val.prod = y.val.prod
z : ℕ
hz : z ∈ y.val
⊢ z ∈ normalizedFactors ?m.439

Tactic:
rw [← Multiset.mem_toFinset]
        apply hy hz

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

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f g : MvPolynomial σ R
⊢ m.toSyn (m.degree (m.sPolynomial f g)) ≤ m.toSyn (m.degree f ⊔ m.degree g)

Tactic:
wlog! +distrib h0 : f ≠ 0 ∧ g ≠ 0

Goal state after:
case inr
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f g : MvPolynomial σ R
this :
  ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommRing R] (f g : MvPolynomial σ R),
    f ≠ 0 ∧ g ≠ 0 → m.toSyn (m.degree (m.sPolynomial f g)) ≤ m.toSyn (m.degree f ⊔ m.degree g)
h0 : f = 0 ∨ g = 0
⊢ m.toSyn (m.degree (m.sPolynomial f g)) ≤ m.toSyn (m.degree f ⊔ m.degree g)

σ✝ : Type u_1
m✝ : MonomialOrder σ✝
R✝ : Type u_2
inst✝¹ : CommRing R✝
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f g : MvPolynomial σ R
h0 : f ≠ 0 ∧ g ≠ 0
⊢ m.toSyn (m.degree (m.sPolynomial f g)) ≤ m.toSyn (m.degree f ⊔ m.degree g)
Module: Mathlib.NumberTheory.ArithmeticFunction.Defs

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
⊢ f * 1 = f

Tactic:
by
    ext x
    simp_all [← map_div_left_divisors, sum_eq_single 1]

Goal state after:
Module: Mathlib.NumberTheory.ArithmeticFunction.Defs

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
f : ℕ → R
hf : Invertible (f 1)
n : ℕ
hn0 : n ≠ 0
hn1 : n ≠ 1
⊢ (if n = 0 then 0
    else
      if n = 1 then ⅟(f 1)
      else
        -⅟(f 1) *
          ∑ d,
            have this := ⋯;
            f (n / ↑d) * dirichletInverseFun f hf ↑d) =
    -⅟(f 1) * ∑ d ∈ n.properDivisors, f (n / d) * dirichletInverseFun f hf d

Tactic:
if_neg hn0,

Goal state after:
R : Type u_1
inst✝ : Ring R
f : ℕ → R
hf : Invertible (f 1)
n : ℕ
hn0 : n ≠ 0
hn1 : n ≠ 1
⊢ (if n = 1 then ⅟(f 1)
    else
      -⅟(f 1) *
        ∑ d,
          have this := ⋯;
          f (n / ↑d) * dirichletInverseFun f hf ↑d) =
    -⅟(f 1) * ∑ d ∈ n.properDivisors, f (n / d) * dirichletInverseFun f hf d
Module: Mathlib.NumberTheory.ArithmeticFunction.Misc

Goal state before:
pp: case cons
ι : Type u_2
f : ι → ℕ
a : ι
s : Finset ι
ha : a ∉ s
ih : (↑s).Pairwise (Coprime on f) → ω (∏ i ∈ s, f i) = ∑ i ∈ s, ω (f i)
h : (↑(cons a s ha)).Pairwise (Coprime on f)
⊢ (↑s).Pairwise (Coprime on f)

Tactic:
exact fun x hx y hy hxy => h (by simp [hx]) (by simp [hy]) hxy

Goal state after:
Module: Mathlib.NumberTheory.ArithmeticFunction.Misc

Goal state before:
pp: case e_s.mp
R : Type u_2
inst✝ : Semiring R
f g : ArithmeticFunction R
N n a✝¹ : ℕ
hn : 0 < n ∧ n ≤ N
a✝ : 0 < a✝¹
left✝ : a✝¹ ≤ N
h : n * a✝¹ ≤ N
⊢ a✝¹ ≤ n * a✝¹ / n

Tactic:
Nat.mul_div_cancel_left _ (by lia)

Goal state after:
case e_s.mp
R : Type u_2
inst✝ : Semiring R
f g : ArithmeticFunction R
N n a✝¹ : ℕ
hn : 0 < n ∧ n ≤ N
a✝ : 0 < a✝¹
left✝ : a✝¹ ≤ N
h : n * a✝¹ ≤ N
⊢ a✝¹ ≤ a✝¹
Module: Mathlib.NumberTheory.ArithmeticFunction.Defs

Goal state before:
pp: case neg
R : Type u_1
inst✝ : CommMonoidWithZero R
f : ArithmeticFunction R
hf : f.IsMultiplicative
g : ArithmeticFunction R
hg : g.IsMultiplicative
h : ∀ (p i : ℕ), Nat.Prime p → f (p ^ i) = g (p ^ i)
n : ℕ
hn : ¬n = 0
⊢ (n.factorization.prod fun p k ↦ f (p ^ k)) = g n

Tactic:
multiplicative_factorization g hg hn

Goal state after:
case neg
R : Type u_1
inst✝ : CommMonoidWithZero R
f : ArithmeticFunction R
hf : f.IsMultiplicative
g : ArithmeticFunction R
hg : g.IsMultiplicative
h : ∀ (p i : ℕ), Nat.Prime p → f (p ^ i) = g (p ^ i)
n : ℕ
hn : ¬n = 0
⊢ (n.factorization.prod fun p k ↦ f (p ^ k)) = n.factorization.prod fun p k ↦ g (p ^ k)
Module: Mathlib.Algebra.Order.Disjointed

Goal state before:
pp: case neg
α : Type u_1
ι : Type u_2
inst✝⁵ : GeneralizedBooleanAlgebra α
inst✝⁴ : LinearOrder ι
inst✝³ : LocallyFiniteOrderBot ι
inst✝² : Add ι
inst✝¹ : One ι
inst✝ : SuccAddOrder ι
f : ι → α
i : ι
hi : ¬IsMax i
⊢ (partialSups f) (i + 1) = (partialSups f) i ⊔ disjointed f (i + 1)

Tactic:
· rw [← Order.succ_eq_add_one, disjointed_succ _ hi]
    simp

Goal state after:
Module: Mathlib.Algebra.Order.Field.GeomSum

Goal state before:
pp: case inr
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
x : K
m n : ℕ
hx : 0 ≤ x
h'x : x < 1
hmn : n < m
⊢ ∑ i ∈ Ico m n, x ^ i ≤ x ^ m / (1 - x)

Tactic:
rw [Ico_eq_empty, sum_empty]

Goal state after:
case inr
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
x : K
m n : ℕ
hx : 0 ≤ x
h'x : x < 1
hmn : n < m
⊢ 0 ≤ x ^ m / (1 - x)

case inr
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
x : K
m n : ℕ
hx : 0 ≤ x
h'x : x < 1
hmn : n < m
⊢ ¬m < n
Module: Mathlib.NumberTheory.ArithmeticFunction.Defs

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
f : ArithmeticFunction R
hf : f.IsMultiplicative
k : ℕ
⊢ (f ^ k).IsMultiplicative

Tactic:
by
  induction k
  case zero => simp
  case succ k hk =>
    rw [pow_succ]
    exact hk.mul hf

Goal state after:
Module: Mathlib.Algebra.Order.Archimedean.Class

Goal state before:
pp: case mk
M : Type u_1
inst✝⁵ : CommGroup M
inst✝⁴ : LinearOrder M
inst✝³ : IsOrderedMonoid M
N : Type u_2
inst✝² : CommGroup N
inst✝¹ : LinearOrder N
inst✝ : IsOrderedMonoid N
f : M →*o N
h : Function.Injective ⇑f
b : MulArchimedeanClass M
a : M
⊢ (orderHom f) (mk a) = (orderHom f) b → mk a = b

Tactic:
induction b using ind with | mk b
   =>  _ 

Goal state after:
case mk.mk
M : Type u_1
inst✝⁵ : CommGroup M
inst✝⁴ : LinearOrder M
inst✝³ : IsOrderedMonoid M
N : Type u_2
inst✝² : CommGroup N
inst✝¹ : LinearOrder N
inst✝ : IsOrderedMonoid N
f : M →*o N
h : Function.Injective ⇑f
a b : M
⊢ (orderHom f) (mk a) = (orderHom f) (mk b) → mk a = mk b