mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Normed.Lp.ProdLp

Goal state before:
pp: p : ℝ≥0∞
𝕜 : Type u_1
α✝ : Type u_2
β✝ : Type u_3
hp : Fact (1 ≤ p)
inst✝³ : SeminormedAddCommGroup α✝
inst✝² : SeminormedAddCommGroup β✝
α : Type u_4
β : Type u_5
inst✝¹ : SeminormedAddCommGroup α
inst✝ : SeminormedAddCommGroup β
x y : α × β
⊢ ‖-toLp p x + toLp p y‖ = ‖toLp p (-x) + toLp p y‖

Tactic:
toLp_neg

Goal state after:
p : ℝ≥0∞
𝕜 : Type u_1
α✝ : Type u_2
β✝ : Type u_3
hp : Fact (1 ≤ p)
inst✝³ : SeminormedAddCommGroup α✝
inst✝² : SeminormedAddCommGroup β✝
α : Type u_4
β : Type u_5
inst✝¹ : SeminormedAddCommGroup α
inst✝ : SeminormedAddCommGroup β
x y : α × β
⊢ ‖-toLp p x + toLp p y‖ = ‖-toLp p x + toLp p y‖
Module: Mathlib.Analysis.Normed.Lp.ProdLp

Goal state before:
pp: p : ℝ≥0∞
𝕜 : Type u_1
α✝ : Type u_2
β✝ : Type u_3
hp : Fact (1 ≤ p)
inst✝³ : SeminormedAddCommGroup α✝
inst✝² : SeminormedAddCommGroup β✝
α : Type u_4
β : Type u_5
inst✝¹ : NormedAddCommGroup α
inst✝ : NormedAddCommGroup β
x y : α × β
⊢ ‖-toLp p x + toLp p y‖ = ‖toLp p (-x) + toLp p y‖

Tactic:
toLp_neg

Goal state after:
p : ℝ≥0∞
𝕜 : Type u_1
α✝ : Type u_2
β✝ : Type u_3
hp : Fact (1 ≤ p)
inst✝³ : SeminormedAddCommGroup α✝
inst✝² : SeminormedAddCommGroup β✝
α : Type u_4
β : Type u_5
inst✝¹ : NormedAddCommGroup α
inst✝ : NormedAddCommGroup β
x y : α × β
⊢ ‖-toLp p x + toLp p y‖ = ‖-toLp p x + toLp p y‖
Module: Mathlib.Analysis.Normed.Operator.Banach

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : CompleteSpace E
F : Type u_5
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
g : E →ₗ[𝕜] F
hg : IsClosed[instTopologicalSpaceProd] ↑g.graph
this : CompleteSpace ↥g.graph := completeSpace_coe_iff_isComplete.mpr (IsClosed.isComplete hg)
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    ⇑g

Tactic:
let φ₀ : E →ₗ[𝕜] E × F := LinearMap.id.prod g

Goal state after:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : CompleteSpace E
F : Type u_5
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
g : E →ₗ[𝕜] F
hg : IsClosed[instTopologicalSpaceProd] ↑g.graph
this : CompleteSpace ↥g.graph := completeSpace_coe_iff_isComplete.mpr (IsClosed.isComplete hg)
φ₀ : E →ₗ[𝕜] E × F := id.prod g
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    ⇑g
Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic

Goal state before:
pp: ι : Type u_1
inst✝ : Fintype ι
a b : ι → ℝ
h : a ≤ b
⊢ (volume (Icc a b)).toReal = ∏ i, (b i - a i)

Tactic:
simp only [volume_Icc_pi, ENNReal.toReal_prod, ENNReal.toReal_ofReal (sub_nonneg.2 (h _))]

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

Goal state before:
pp: case top.refine_1.inr
ι : Type u_2
β : ι → Type u_4
inst✝² : Fintype ι
inst✝¹ : (i : ι) → SeminormedAddCommGroup (β i)
inst✝ : DecidableEq ι
i : ι
b : β i
this : Nonempty ι
hp : Fact (1 ≤ ∞)
j : ι
hij : i ≠ j
⊢ ‖(single ∞ i b).ofLp j‖₊ ≤ ‖b‖₊

Tactic:
simp [hij]

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

Goal state before:
pp: p : ℝ≥0∞
𝕜 : Type u_1
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
inst✝² : Fact (1 ≤ p)
inst✝¹ : Fintype ι
inst✝ : (i : ι) → SeminormedAddCommGroup (α i)
x y : (i : ι) → α i
⊢ ‖-toLp p x + toLp p y‖ = ‖toLp p (-x) + toLp p y‖

Tactic:
toLp_neg

Goal state after:
p : ℝ≥0∞
𝕜 : Type u_1
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
inst✝² : Fact (1 ≤ p)
inst✝¹ : Fintype ι
inst✝ : (i : ι) → SeminormedAddCommGroup (α i)
x y : (i : ι) → α i
⊢ ‖-toLp p x + toLp p y‖ = ‖-toLp p x + toLp p y‖
Module: Mathlib.Analysis.Normed.Lp.PiLp

Goal state before:
pp: p : ℝ≥0∞
𝕜 : Type u_1
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
inst✝² : Fact (1 ≤ p)
inst✝¹ : Fintype ι
inst✝ : (i : ι) → NormedAddCommGroup (α i)
x y : (i : ι) → α i
⊢ ‖-toLp p x + toLp p y‖ = ‖toLp p (-x) + toLp p y‖

Tactic:
toLp_neg

Goal state after:
p : ℝ≥0∞
𝕜 : Type u_1
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
inst✝² : Fact (1 ≤ p)
inst✝¹ : Fintype ι
inst✝ : (i : ι) → NormedAddCommGroup (α i)
x y : (i : ι) → α i
⊢ ‖-toLp p x + toLp p y‖ = ‖-toLp p x + toLp p y‖
Module: Mathlib.Algebra.Module.ZLattice.Basic

Goal state before:
pp: ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Basis ι ℝ (ι → ℝ)
⊢ ENNReal.ofReal |(Pi.basisFun ℝ ι).det ⇑b| * volume (Set.univ.pi fun x ↦ Set.Ico 0 1) =
    ENNReal.ofReal |(Matrix.of ⇑b).det|

Tactic:
volume_pi,

Goal state after:
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Basis ι ℝ (ι → ℝ)
⊢ ENNReal.ofReal |(Pi.basisFun ℝ ι).det ⇑b| * (Measure.pi fun x ↦ volume) (Set.univ.pi fun x ↦ Set.Ico 0 1) =
    ENNReal.ofReal |(Matrix.of ⇑b).det|
Module: Mathlib.Analysis.BoxIntegral.Box.Basic

Goal state before:
pp: ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
r : ℝ
h : ∀ (i : ι), I.upper i - I.lower i = (J.upper i - J.lower i) / r
⊢ (Finset.univ.sup fun i ↦
      (Finset.univ.sup fun b ↦ Real.nnabs (J.upper b - J.lower b) / Real.nnabs r) /
        (Real.nnabs (J.upper i - J.lower i) / Real.nnabs r)) =
    Finset.univ.sup fun i ↦
      (Finset.univ.sup fun b ↦ Real.nnabs (J.upper b - J.lower b)) / Real.nnabs (J.upper i - J.lower i)

Tactic:
congr 1 with i

Goal state after:
case e_f
ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
r : ℝ
h : ∀ (i : ι), I.upper i - I.lower i = (J.upper i - J.lower i) / r
i : ι
⊢ ↑((Finset.univ.sup fun b ↦ Real.nnabs (J.upper b - J.lower b) / Real.nnabs r) /
        (Real.nnabs (J.upper i - J.lower i) / Real.nnabs r)) =
    ↑((Finset.univ.sup fun b ↦ Real.nnabs (J.upper b - J.lower b)) / Real.nnabs (J.upper i - J.lower i))
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
t_bound : t ⊆ closedBall 0 1
A : Tendsto (fun r ↦ μ (s ∩ ({x} + r • t)) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 0)
B : Tendsto (fun r ↦ μ (closedBall x r) / μ ({x} + r • u)) (𝓝[>] 0) (𝓝 (μ (closedBall x 1) / μ ({x} + u)))
C :
  Tendsto (fun r ↦ μ (s ∩ ({x} + r • t)) / μ (closedBall x r) * (μ (closedBall x r) / μ ({x} + r • u))) (𝓝[>] 0)
    (𝓝 (0 * (μ (closedBall x 1) / μ ({x} + u))))
⊢ Tendsto (fun r ↦ μ (s ∩ ({x} + r • t)) / μ ({x} + r • u)) (𝓝[>] 0) (𝓝 0)

Tactic:
simp only [zero_mul] at C

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
t_bound : t ⊆ closedBall 0 1
A : Tendsto (fun r ↦ μ (s ∩ ({x} + r • t)) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 0)
B : Tendsto (fun r ↦ μ (closedBall x r) / μ ({x} + r • u)) (𝓝[>] 0) (𝓝 (μ (closedBall x 1) / μ ({x} + u)))
C : Tendsto (fun r ↦ μ (s ∩ ({x} + r • t)) / μ (closedBall x r) * (μ (closedBall x r) / μ ({x} + r • u))) (𝓝[>] 0) (𝓝 0)
⊢ Tendsto (fun r ↦ μ (s ∩ ({x} + r • t)) / μ ({x} + r • u)) (𝓝[>] 0) (𝓝 0)
Module: Mathlib.Analysis.BoxIntegral.Partition.Basic

Goal state before:
pp: ι : Type u_1
I J : Box ι
π : Prepartition I
h : I ≤ J
⊢ ∀ a ∈ π.boxes, Option.toFinset (↑J ⊓ ↑a) = {a}

Tactic:
intro J' hJ'

Goal state after:
ι : Type u_1
I J : Box ι
π : Prepartition I
h : I ≤ J
J' : Box ι
hJ' : J' ∈ π.boxes
⊢ Option.toFinset (↑J ⊓ ↑J') = {J'}
Module: Mathlib.Analysis.BoxIntegral.Partition.SubboxInduction

Goal state before:
pp: ι : Type u_1
inst✝ : Fintype ι
I : Box ι
r : (ι → ℝ) → ↑(Ioi 0)
J : Box ι
x✝ : J ≤ I
πi : (J' : Box ι) → TaggedPrepartition J'
hP✝ : ∀ J' ∈ splitCenter J, (πi J').IsPartition
hHen : ∀ J' ∈ splitCenter J, (πi J').IsHenstock
hr : ∀ J' ∈ splitCenter J, (πi J').IsSubordinate r
a✝ : ∀ J' ∈ splitCenter J, (πi J').distortion = J'.distortion
n : Box ι → Box ι → ℕ
hn : ∀ J' ∈ splitCenter J, ∀ J ∈ πi J', ∀ (i : ι), J.upper i - J.lower i = (J'.upper i - J'.lower i) / 2 ^ n J' J
hP : ((splitCenter J).biUnionTagged πi).IsPartition
⊢ ∀ J' ∈ (splitCenter J).biUnionTagged πi, ∃ n, ∀ (i : ι), J'.upper i - J'.lower i = (J.upper i - J.lower i) / 2 ^ n

Tactic:
intro J' hJ'

Goal state after:
ι : Type u_1
inst✝ : Fintype ι
I : Box ι
r : (ι → ℝ) → ↑(Ioi 0)
J : Box ι
x✝ : J ≤ I
πi : (J' : Box ι) → TaggedPrepartition J'
hP✝ : ∀ J' ∈ splitCenter J, (πi J').IsPartition
hHen : ∀ J' ∈ splitCenter J, (πi J').IsHenstock
hr : ∀ J' ∈ splitCenter J, (πi J').IsSubordinate r
a✝ : ∀ J' ∈ splitCenter J, (πi J').distortion = J'.distortion
n : Box ι → Box ι → ℕ
hn : ∀ J' ∈ splitCenter J, ∀ J ∈ πi J', ∀ (i : ι), J.upper i - J.lower i = (J'.upper i - J'.lower i) / 2 ^ n J' J
hP : ((splitCenter J).biUnionTagged πi).IsPartition
J' : Box ι
hJ' : J' ∈ (splitCenter J).biUnionTagged πi
⊢ ∃ n, ∀ (i : ι), J'.upper i - J'.lower i = (J.upper i - J.lower i) / 2 ^ n
Module: Mathlib.Analysis.BoxIntegral.Partition.Split

Goal state before:
pp: ι : Type u_1
I : Box ι
i : ι
x : ℝ
y : ι → ℝ
⊢ (∀ (x : ι), I.lower x < y x) ∧ y i ≤ x ∧ y ≤ I.upper ↔ (∀ (x : ι), I.lower x < y x) ∧ y ≤ I.upper ∧ y i ≤ x

Tactic:
and_comm (a := y i ≤ x)

Goal state after:
ι : Type u_1
I : Box ι
i : ι
x : ℝ
y : ι → ℝ
⊢ (∀ (x : ι), I.lower x < y x) ∧ y ≤ I.upper ∧ y i ≤ x ↔ (∀ (x : ι), I.lower x < y x) ∧ y ≤ I.upper ∧ y i ≤ x
Module: Mathlib.Algebra.Module.ZLattice.Basic

Goal state before:
pp: E : Type u_1
F : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : TopologicalSpace F
L : Submodule ℤ E
inst✝¹ : DiscreteTopology ↥L
inst✝ : IsZLattice ℝ L
f : E → F
hf : Continuous f
hf' : ∀ (z w : E), w ∈ L → f (z + w) = f z
this : Free ℤ ↥L
b : Basis (Free.ChooseBasisIndex ℤ ↥L) ℤ ↥L := Free.chooseBasis ℤ ↥L
⊢ Set.range f ⊆ f '' ↑(Basis.ofZLatticeBasis ℝ L b).parallelepiped

Tactic:
rintro _ ⟨x, rfl⟩

Goal state after:
E : Type u_1
F : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : TopologicalSpace F
L : Submodule ℤ E
inst✝¹ : DiscreteTopology ↥L
inst✝ : IsZLattice ℝ L
f : E → F
hf : Continuous f
hf' : ∀ (z w : E), w ∈ L → f (z + w) = f z
this : Free ℤ ↥L
b : Basis (Free.ChooseBasisIndex ℤ ↥L) ℤ ↥L := Free.chooseBasis ℤ ↥L
x : E
⊢ f x ∈ f '' ↑(Basis.ofZLatticeBasis ℝ L b).parallelepiped
Module: Mathlib.Analysis.Oscillation

Goal state before:
pp: E : Type u
F : Type v
inst✝¹ : PseudoEMetricSpace F
inst✝ : TopologicalSpace E
f : E → F
x : E
hf : ContinuousAt f x
⊢ oscillation f x = 0

Tactic:
rw [← continuousWithinAt_univ f x] at hf

Goal state after:
E : Type u
F : Type v
inst✝¹ : PseudoEMetricSpace F
inst✝ : TopologicalSpace E
f : E → F
x : E
hf : ContinuousWithinAt f univ x
⊢ oscillation f x = 0
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
J : Box (Fin (n + 1))
hJ : ↑J ≤ ↑I₀
j : Fin (n + 1)
x : ℝ
⊢ x ∈ Set.Ioo (J.lower j) (J.upper j) →
    Option.elim' 0 (fun J ↦ f (J.upper i) (J.face i) - f (J.lower i) (J.face i)) (J.splitLower j x) +
        Option.elim' 0 (fun J ↦ f (J.upper i) (J.face i) - f (J.lower i) (J.face i)) (J.splitUpper j x) =
      f (J.upper i) (J.face i) - f (J.lower i) (J.face i)

Tactic:
rw [WithTop.coe_le_coe] at hJ

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✝ : ι
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
J : Box (Fin (n + 1))
hJ : J ≤ I₀
j : Fin (n + 1)
x : ℝ
⊢ x ∈ Set.Ioo (J.lower j) (J.upper j) →
    Option.elim' 0 (fun J ↦ f (J.upper i) (J.face i) - f (J.lower i) (J.face i)) (J.splitLower j x) +
        Option.elim' 0 (fun J ↦ f (J.upper i) (J.face i) - f (J.lower i) (J.face i)) (J.splitUpper j x) =
      f (J.upper i) (J.face i) - f (J.lower i) (J.face i)
Module: Mathlib.Analysis.BoxIntegral.UnitPartition

Goal state before:
pp: ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
ν : ι → ℤ
⊢ volume ↑(box n ν) = 1 / ↑n ^ card ι

Tactic:
volume_pi,

Goal state after:
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
ν : ι → ℤ
⊢ (Measure.pi fun x ↦ volume) ↑(box n ν) = 1 / ↑n ^ card ι
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:
mul_le_mul_iff_right₀ h

Goal state after:
n : ℕ
inst✝ : NeZero n
x : ℝ
a : ℤ
h : 0 < ↑n
⊢ x ≤ ↑a ↔ x ≤ ↑a
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
a : ι
ha : a ∈ Finset.Iio n
⊢ (⟪gramSchmidt 𝕜 f a, f n⟫_𝕜 / ↑(‖gramSchmidt 𝕜 f a‖ ^ 2)) • gramSchmidt 𝕜 f a ∈ span 𝕜 (gramSchmidt 𝕜 f '' Set.Iio n)

Tactic:
apply Submodule.smul_mem _ _ _

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
a : ι
ha : a ∈ Finset.Iio n
⊢ gramSchmidt 𝕜 f a ∈ span 𝕜 (gramSchmidt 𝕜 f '' Set.Iio n)
Module: Mathlib.Analysis.BoxIntegral.UnitPartition

Goal state before:
pp: ι : Type u_1
s : Set (ι → ℝ)
inst✝ : Fintype ι
x : ℝ
hx : 1 ≤ x
this : 0 < ⌊x⌋₊
⊢ ↑(Nat.card ↑(s ∩ (↑⌊x⌋₊)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))))) / ↑⌊x⌋₊ ^ card ι * (↑⌊x⌋₊ / x) ^ card ι =
    ↑(Nat.card ↑(s ∩ (↑⌊x⌋₊)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))))) / x ^ card ι

Tactic:
div_pow,

Goal state after:
ι : Type u_1
s : Set (ι → ℝ)
inst✝ : Fintype ι
x : ℝ
hx : 1 ≤ x
this : 0 < ⌊x⌋₊
⊢ ↑(Nat.card ↑(s ∩ (↑⌊x⌋₊)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))))) / ↑⌊x⌋₊ ^ card ι *
      (↑⌊x⌋₊ ^ card ι / x ^ card ι) =
    ↑(Nat.card ↑(s ∩ (↑⌊x⌋₊)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))))) / x ^ card ι
Module: Mathlib.Analysis.BoxIntegral.UnitPartition

Goal state before:
pp: ι : Type u_1
s : Set (ι → ℝ)
inst✝ : Fintype ι
x : ℝ
hx : 1 ≤ x
⊢ ↑(Nat.card ↑(s ∩ (↑⌈x⌉₊)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))))) / ↑⌈x⌉₊ ^ card ι * (↑⌈x⌉₊ / x) ^ card ι =
    ↑(Nat.card ↑(s ∩ (↑⌈x⌉₊)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))))) / x ^ card ι

Tactic:
div_pow,

Goal state after:
ι : Type u_1
s : Set (ι → ℝ)
inst✝ : Fintype ι
x : ℝ
hx : 1 ≤ x
⊢ ↑(Nat.card ↑(s ∩ (↑⌈x⌉₊)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))))) / ↑⌈x⌉₊ ^ card ι *
      (↑⌈x⌉₊ ^ card ι / x ^ card ι) =
    ↑(Nat.card ↑(s ∩ (↑⌈x⌉₊)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))))) / x ^ card ι
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
⊢ μ' D ≠ ∞

Tactic:
simp [μ'D]

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

Goal state before:
pp: ι : Type u_2
inst✝⁴ : Fintype ι
L₁ L₂ : Submodule ℤ (ι → ℝ)
inst✝³ : DiscreteTopology ↥L₁
inst✝² : IsZLattice ℝ L₁
inst✝¹ : DiscreteTopology ↥L₂
inst✝ : IsZLattice ℝ L₂
h : L₁ ≤ L₂
b₁ : Basis ι ℤ ↥L₁ := ⋯
b₂ : Basis ι ℤ ↥L₂ := ⋯
⊢ covolume L₁ volume / covolume L₂ volume = |(Basis.ofZLatticeBasis ℝ L₂ b₂).det ⇑(Basis.ofZLatticeBasis ℝ L₁ b₁)|

pp: ι : Type u_2
inst✝⁴ : Fintype ι
L₁ L₂ : Submodule ℤ (ι → ℝ)
inst✝³ : DiscreteTopology ↥L₁
inst✝² : IsZLattice ℝ L₁
inst✝¹ : DiscreteTopology ↥L₂
inst✝ : IsZLattice ℝ L₂
h : L₁ ≤ L₂
b₁ : Basis ι ℤ ↥L₁ := ⋯
b₂ : Basis ι ℤ ↥L₂ := ⋯
⊢ |(Basis.ofZLatticeBasis ℝ L₂ b₂).det ⇑(Basis.ofZLatticeBasis ℝ L₁ b₁)| = |↑(b₂.det fun i ↦ ⟨↑(b₁ i), ⋯⟩)|

Tactic:
· rw [← Basis.det_mul_det _ (Pi.basisFun ℝ ι) _, abs_mul, Pi.basisFun_det_apply,
      ← Basis.det_inv, Units.val_inv_eq_inv_val, IsUnit.unit_spec, Pi.basisFun_det_apply,
      covolume_eq_det _ b₁, covolume_eq_det _ b₂, mul_comm, abs_inv]
    congr 3 <;> ext <;> simp

Goal state after:
ι : Type u_2
inst✝⁴ : Fintype ι
L₁ L₂ : Submodule ℤ (ι → ℝ)
inst✝³ : DiscreteTopology ↥L₁
inst✝² : IsZLattice ℝ L₁
inst✝¹ : DiscreteTopology ↥L₂
inst✝ : IsZLattice ℝ L₂
h : L₁ ≤ L₂
b₁ : Basis ι ℤ ↥L₁ := ⋯
b₂ : Basis ι ℤ ↥L₂ := ⋯
⊢ |(Basis.ofZLatticeBasis ℝ L₂ b₂).det ⇑(Basis.ofZLatticeBasis ℝ L₁ b₁)| = |↑(b₂.det fun i ↦ ⟨↑(b₁ i), ⋯⟩)|
Module: Mathlib.Analysis.BoxIntegral.Integrability

Goal state before:
pp: case left
ι : 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
y : E
hy : HasIntegral I l f μ.toBoxAdditive.toSMul y
v : Set (ι → ℝ) := {x | ContinuousAt f x}
this : AEStronglyMeasurable f (μ.restrict v)
s : Set (ι → ℝ)
hs : MeasurableSet s
⊢ μ (s ∩ vᶜ) ≤ 0

Tactic:
s.inter_subset_right

Goal state after:
case left
ι : 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
y : E
hy : HasIntegral I l f μ.toBoxAdditive.toSMul y
v : Set (ι → ℝ) := {x | ContinuousAt f x}
this : AEStronglyMeasurable f (μ.restrict v)
s : Set (ι → ℝ)
hs : MeasurableSet s
⊢ μ vᶜ ≤ 0
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 : ℕ
⊢ ∑ k ∈ Ico (u 0) (u n), f k ≤ ∑ k ∈ range n, (u (k + 1) - u k) • f (u k)

Tactic:
induction n with
  | zero => simp
  | succ n ihn =>
    suffices (∑ k ∈ Ico (u n) (u (n + 1)), f k) ≤ (u (n + 1) - u n) • f (u n) by
      rw [sum_range_succ, ← sum_Ico_consecutive]
      · exact add_le_add ihn this
      exacts [hu n.zero_le, hu n.le_succ]
    have : ∀ k ∈ Ico (u n) (u (n + 1)), f k ≤ f (u n) := fun k hk =>
      hf (Nat.succ_le_of_lt (h_pos n)) (mem_Ico.mp hk).1
    convert! sum_le_sum this
    simp

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

Goal state before:
pp: case mp
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
D : Type u_2
inst✝ : TopologicalSpace D
f : D → E
hf : Continuous[inst✝, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
c : ℝ
hc : ∀ (a : D), ‖f a‖ ≤ c
⊢ ∃ c, ∀ᶠ (x : D) in cocompact D, ‖f x‖ ≤ c * ‖1 x‖

Tactic:
use c

Goal state after:
case h
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
D : Type u_2
inst✝ : TopologicalSpace D
f : D → E
hf : Continuous[inst✝, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
c : ℝ
hc : ∀ (a : D), ‖f a‖ ≤ c
⊢ ∀ᶠ (x : D) in cocompact D, ‖f x‖ ≤ c * ‖1 x‖
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
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Basis ι ℤ ↥L
n : ℕ
r : ℝ
s : ℕ → Finset (ι → ℤ) := fun n ↦ Fintype.piFinset fun i ↦ Icc (-↑n) ↑n
d : ℕ := Fintype.card ι
hr : r < -↑d
hr' : r < 0
hd : 1 ≤ d
hs0 : s 0 = {0}
hs : ∀ {a b : ℕ}, a ≤ b → s a ⊆ s b
k : ℕ
⊢ #(s (k + 1) \ s k) ≤ 2 * d * (2 * k + 3) ^ (d - 1)

Tactic:
simp only [le_add_iff_nonneg_right, zero_le, hs, card_sdiff_of_subset, s, Fintype.card_piFinset,
      Int.card_Icc, prod_const]

Goal state after:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
L : Submodule ℤ E
inst✝² : DiscreteTopology ↥L
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Basis ι ℤ ↥L
n : ℕ
r : ℝ
s : ℕ → Finset (ι → ℤ) := fun n ↦ Fintype.piFinset fun i ↦ Icc (-↑n) ↑n
d : ℕ := Fintype.card ι
hr : r < -↑d
hr' : r < 0
hd : 1 ≤ d
hs0 : s 0 = {0}
hs : ∀ {a b : ℕ}, a ≤ b → s a ⊆ s b
k : ℕ
⊢ (↑(k + 1) + 1 - -↑(k + 1)).toNat ^ #univ - (↑k + 1 - -↑k).toNat ^ #univ ≤ 2 * d * (2 * k + 3) ^ (d - 1)
Module: Mathlib.Algebra.MvPolynomial.Coeff

Goal state before:
pp: case pos
R : Type u_1
inst✝ : CommSemiring R
d : Fin 2 →₀ ℕ
n : ℕ
this : (d.sum fun x m ↦ m) = d 0 + d 1
hd : d 0 + d 1 = n
⊢ d.multinomial = n.choose (d 0)

pp: case neg
R : Type u_1
inst✝ : CommSemiring R
d : Fin 2 →₀ ℕ
n : ℕ
this : (d.sum fun x m ↦ m) = d 0 + d 1
hd : ¬d 0 + d 1 = n
⊢ 0 = 0

Tactic:
· rw [multinomial_eq_of_support_subset (Finset.subset_univ d.support), Finset.univ_fin2,
      Nat.binomial_eq_choose Fin.zero_ne_one, hd]

Goal state after:
case neg
R : Type u_1
inst✝ : CommSemiring R
d : Fin 2 →₀ ℕ
n : ℕ
this : (d.sum fun x m ↦ m) = d 0 + d 1
hd : ¬d 0 + d 1 = n
⊢ 0 = 0
Module: Mathlib.Data.Nat.Choose.Multinomial

Goal state before:
pp: case e_a
α : Type u_1
f : α →₀ ℕ
s : Finset α
h : f.support ⊆ s
⊢ ∏ i ∈ f.support, (f i)! = ∏ i ∈ s, (f i)!

Tactic:
· rw [Finset.prod_subset h]
    grind [Nat.factorial_eq_one]

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
i : σ
j : σ →₀ ℕ
r : R
⊢ X i ∣ (monomial j) r ↔ r = 0 ∨ j i ≠ 0

Tactic:
refine monomial_dvd_monomial.trans ?_
  simp_rw [one_dvd, and_true, Finsupp.single_le_iff, Nat.one_le_iff_ne_zero]

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

Goal state before:
pp: case refine_2
σ : Type u_1
R : Type u_3
inst✝ : CommRing R
i : σ
p r : MvPolynomial σ R
h : X i ∣ p - r
hr : ∀ n ∈ r.support, n i = 0
⊢ r = p.modMonomial (Finsupp.single i 1)

Tactic:
· obtain ⟨q, hq⟩ := h
    apply eq_modMonomial_single (q := q) _ hr
    rwa [← sub_eq_iff_eq_add]

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

Goal state before:
pp: case mp
σ : Type u_1
R : Type u_3
inst✝¹ : CommRing R
i : σ
p q : MvPolynomial σ R
inst✝ : IsCancelMulZero R
a✝ : Nontrivial R
h : X i ∣ p * q
⊢ X i ∣ p ∨ X i ∣ q

Tactic:
suffices (p.modMonomial (Finsupp.single i 1)) * (q.modMonomial (Finsupp.single i 1)) =
          (p * q).modMonomial (Finsupp.single i 1) by
      simp only [X_dvd_iff_modMonomial_eq_zero] at h ⊢
      rwa [h, mul_eq_zero] at this

Goal state after:
case mp
σ : Type u_1
R : Type u_3
inst✝¹ : CommRing R
i : σ
p q : MvPolynomial σ R
inst✝ : IsCancelMulZero R
a✝ : Nontrivial R
h : X i ∣ p * q
⊢ p.modMonomial (Finsupp.single i 1) * q.modMonomial (Finsupp.single i 1) = (p * q).modMonomial (Finsupp.single i 1)
Module: Mathlib.Algebra.MvPolynomial.Expand

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝¹ : CommSemiring R
p : ℕ
φ : MvPolynomial σ R
inst✝ : DecidableEq σ
⊢ (∑ x ∈ φ.support, (monomial (p • x)) (coeff x φ)).support ⊆ Finset.image (fun x ↦ p • x) φ.support

Tactic:
refine MvPolynomial.support_sum.trans ?_

Goal state after:
σ : Type u_1
R : Type u_3
inst✝¹ : CommSemiring R
p : ℕ
φ : MvPolynomial σ R
inst✝ : DecidableEq σ
⊢ (φ.support.biUnion fun x ↦ ((monomial (p • x)) (coeff x φ)).support) ⊆ Finset.image (fun x ↦ p • x) φ.support