mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.BoxIntegral.Box.SubboxInduction

Goal state before:
pp: case neg
ι : Type u_1
I✝ J I : Box ι
s : Set ι
i : ι
h✝ : i ∉ s
⊢ I.lower i < (I.lower i + I.upper i) / 2

Tactic:
simp only [left_lt_add_div_two, add_div_two_lt_right, I.lower_lt_upper]

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

Goal state before:
pp: case refine_1.refine_1
K : Type u_1
inst✝⁹ : NormedField K
inst✝⁸ : LinearOrder K
inst✝⁷ : IsStrictOrderedRing K
inst✝⁶ : HasSolidNorm K
inst✝⁵ : FloorRing K
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
inst✝² : FiniteDimensional K E
inst✝¹ : ProperSpace E
L : Submodule ℤ E
inst✝ : DiscreteTopology ↥L
hs : IsZLattice K L
s : Set E
h_incl : s ⊆ ↑L
h_span : span K s = span K ↑L
h_lind : LinearIndependent K Subtype.val
b : Basis { x // x ∈ s } K E := Basis.mk h_lind ⋯
this✝ : Fintype ↑s
this : (fundamentalDomain b ∩ ↑L).Finite
x : E
h_mem : x ∈ ↑L
⊢ fract b x ∈ fundamentalDomain b

pp: case refine_1.refine_2
K : Type u_1
inst✝⁹ : NormedField K
inst✝⁸ : LinearOrder K
inst✝⁷ : IsStrictOrderedRing K
inst✝⁶ : HasSolidNorm K
inst✝⁵ : FloorRing K
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
inst✝² : FiniteDimensional K E
inst✝¹ : ProperSpace E
L : Submodule ℤ E
inst✝ : DiscreteTopology ↥L
hs : IsZLattice K L
s : Set E
h_incl : s ⊆ ↑L
h_span : span K s = span K ↑L
h_lind : LinearIndependent K Subtype.val
b : Basis { x // x ∈ s } K E := Basis.mk h_lind ⋯
this✝ : Fintype ↑s
this : (fundamentalDomain b ∩ ↑L).Finite
x : E
h_mem : x ∈ ↑L
⊢ fract b x ∈ ↑L

Tactic:
· exact fract_mem_fundamentalDomain b x

Goal state after:
case refine_1.refine_2
K : Type u_1
inst✝⁹ : NormedField K
inst✝⁸ : LinearOrder K
inst✝⁷ : IsStrictOrderedRing K
inst✝⁶ : HasSolidNorm K
inst✝⁵ : FloorRing K
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
inst✝² : FiniteDimensional K E
inst✝¹ : ProperSpace E
L : Submodule ℤ E
inst✝ : DiscreteTopology ↥L
hs : IsZLattice K L
s : Set E
h_incl : s ⊆ ↑L
h_span : span K s = span K ↑L
h_lind : LinearIndependent K Subtype.val
b : Basis { x // x ∈ s } K E := Basis.mk h_lind ⋯
this✝ : Fintype ↑s
this : (fundamentalDomain b ∩ ↑L).Finite
x : E
h_mem : x ∈ ↑L
⊢ fract b x ∈ ↑L
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' : Box ι
hJ' : J' ∈ (splitCenter J).biUnionTagged πi
⊢ ∃ n, ∀ (i : ι), J'.upper i - J'.lower i = (J.upper i - J.lower i) / 2 ^ n

Tactic:
rcases (splitCenter J).mem_biUnionTagged.1 hJ' with ⟨J₁, h₁, h₂⟩

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
J₁ : Box ι
h₁ : J₁ ∈ splitCenter J
h₂ : J' ∈ πi J₁
⊢ ∃ 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: case refine_1
ι : Type u_1
I : Box ι
inst✝ : Finite ι
π : Prepartition I
t : Finset (ι × ℝ)
ht : ∀ (I_1 J : Box ι), J ∈ π.boxes → ∀ J' ∈ splitMany I_1 t, ¬Disjoint ↑J ↑J' → J' ≤ J
J : Box ι
hJ : J ∈ π
⊢ (splitMany I t).restrict J ≤ ((splitMany I t).filter fun J ↦ ↑J ⊆ π.iUnion).restrict J

pp: case refine_2
ι : Type u_1
I : Box ι
inst✝ : Finite ι
π : Prepartition I
t : Finset (ι × ℝ)
ht : ∀ (I_1 J : Box ι), J ∈ π.boxes → ∀ J' ∈ splitMany I_1 t, ¬Disjoint ↑J ↑J' → J' ≤ J
J : Box ι
hJ : J ∈ (splitMany I t).filter fun J ↦ ↑J ⊆ π.iUnion
⊢ ∃ I' ∈ π, J ≤ I'

Tactic:
· refine ofWithBot_mono ?_
    simp only [Finset.mem_image, mem_boxes, mem_filter]
    rintro _ ⟨J₁, h₁, rfl⟩ hne
    refine ⟨_, ⟨J₁, ⟨h₁, Subset.trans ?_ (π.subset_iUnion hJ)⟩, rfl⟩, le_rfl⟩
    exact ht I J hJ J₁ h₁ (mt disjoint_iff.1 hne)

Goal state after:
case refine_2
ι : Type u_1
I : Box ι
inst✝ : Finite ι
π : Prepartition I
t : Finset (ι × ℝ)
ht : ∀ (I_1 J : Box ι), J ∈ π.boxes → ∀ J' ∈ splitMany I_1 t, ¬Disjoint ↑J ↑J' → J' ≤ J
J : Box ι
hJ : J ∈ (splitMany I t).filter fun J ↦ ↑J ⊆ π.iUnion
⊢ ∃ I' ∈ π, J ≤ I'
Module: Mathlib.Analysis.BoxIntegral.Partition.Split

Goal state before:
pp: ι : Type u_1
inst✝ : Finite ι
I : Box ι
π : Prepartition I
h : π.IsPartition
s : Finset (ι × ℝ)
hs : π ⊓ splitMany I s = (splitMany I s).filter fun J ↦ ↑J ⊆ π.iUnion
⊢ splitMany I s ≤ π

Tactic:
rwa [h.iUnion_eq, filter_of_true, inf_eq_right] at hs

Goal state after:
case hp
ι : Type u_1
inst✝ : Finite ι
I : Box ι
π : Prepartition I
h : π.IsPartition
s : Finset (ι × ℝ)
hs : π ⊓ splitMany I s = (splitMany I s).filter fun J ↦ ↑J ⊆ ↑I
⊢ ∀ J ∈ splitMany I s, ↑J ⊆ ↑I
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 = ⨅ S ∈ Filter.map f (𝓝 x), ediam S

Tactic:
oscillationWithin,

Goal state after:
E : Type u
F : Type v
inst✝¹ : PseudoEMetricSpace F
inst✝ : TopologicalSpace E
f : E → F
D : Set E
x : E
hD : D ∈ 𝓝 x
⊢ ⨅ S ∈ Filter.map f (𝓝[D] x), ediam S = ⨅ S ∈ Filter.map f (𝓝 x), ediam S
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
hf : ContinuousWithinAt f D x
ε : ℝ≥0∞
hε : 0 < ε
this : eball (f x) (ε / 2) ∈ Filter.map f (𝓝[D] x)
⊢ oscillationWithin f D x ≤ ε

Tactic:
refine (biInf_le ediam this).trans (le_of_le_of_eq ediam_eball_le ?_)

Goal state after:
E : Type u
F : Type v
inst✝¹ : PseudoEMetricSpace F
inst✝ : TopologicalSpace E
f : E → F
D : Set E
x : E
hf : ContinuousWithinAt f D x
ε : ℝ≥0∞
hε : 0 < ε
this : eball (f x) (ε / 2) ∈ Filter.map f (𝓝[D] x)
⊢ 2 * (ε / 2) = ε
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
xD : x ∈ D
hf : oscillationWithin f D x = 0
ε : ℝ≥0∞
ε0 : ε > oscillationWithin f D x
⊢ ∀ᶠ (x_1 : E) in 𝓝[D] x, edist (f x_1) (f x) < ε

Tactic:
oscillationWithin,

Goal state after:
E : Type u
F : Type v
inst✝¹ : PseudoEMetricSpace F
inst✝ : TopologicalSpace E
f : E → F
D : Set E
x : E
xD : x ∈ D
hf : oscillationWithin f D x = 0
ε : ℝ≥0∞
ε0 : ε > ⨅ S ∈ Filter.map f (𝓝[D] x), ediam S
⊢ ∀ᶠ (x_1 : E) in 𝓝[D] x, edist (f x_1) (f x) < ε
Module: Mathlib.Analysis.InnerProductSpace.PiL2

Goal state before:
pp: ι : Type u_1
inst✝ : Fintype ι
b : OrthonormalBasis ι ℝ ℝ
this : Unique ι
⊢ b default = 1 ∨ b default = -1

Tactic:
have : ‖b default‖ = 1 := b.orthonormal.1 _

Goal state after:
ι : Type u_1
inst✝ : Fintype ι
b : OrthonormalBasis ι ℝ ℝ
this✝ : Unique ι
this : ‖b default‖ = 1
⊢ b default = 1 ∨ b default = -1
Module: Mathlib.Analysis.BoxIntegral.UnitPartition

Goal state before:
pp: case refine_2
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
s : Set (ι → ℝ)
hs₁ : NullMeasurableSet s volume
hs₂ : volume s ≠ ⊤
x✝¹ x✝ : ι → ℤ
h : x✝¹ ≠ x✝
⊢ Function.onFun (AEDisjoint volume) (fun ν ↦ ↑(box n ν) ∩ s) x✝¹ x✝

pp: case refine_3
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
s : Set (ι → ℝ)
hs₁ : NullMeasurableSet s volume
hs₂ : volume s ≠ ⊤
⊢ volume (⋃ i, ↑(box n i) ∩ s) ≠ ⊤

pp: case refine_4
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
s : Set (ι → ℝ)
hs₁ : NullMeasurableSet s volume
hs₂ : volume s ≠ ⊤
x✝ : ι → ℤ
hν : x✝ ∈ {ν | ↑(box n ν) ⊆ s}
⊢ x✝ ∈ {i | 1 / ↑n ^ card ι ≤ volume (↑(box n i) ∩ s)}

Tactic:
· exact ((Disjoint.inter_right _ (disjoint.mp h)).inter_left _).aedisjoint

Goal state after:
case refine_3
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
s : Set (ι → ℝ)
hs₁ : NullMeasurableSet s volume
hs₂ : volume s ≠ ⊤
⊢ volume (⋃ i, ↑(box n i) ∩ s) ≠ ⊤

case refine_4
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
s : Set (ι → ℝ)
hs₁ : NullMeasurableSet s volume
hs₂ : volume s ≠ ⊤
x✝ : ι → ℤ
hν : x✝ ∈ {ν | ↑(box n ν) ⊆ s}
⊢ x✝ ∈ {i | 1 / ↑n ^ card ι ≤ volume (↑(box n i) ∩ s)}
Module: Mathlib.Analysis.BoxIntegral.UnitPartition

Goal state before:
pp: case refine_2
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
B : Box ι
x : ι → ℝ
hx : x ∈ B
l u : ι → ℤ
hl : ∀ (i : ι), B.lower i = ↑(l i)
hu : ∀ (i : ι), B.upper i = ↑(u i)
i : ι
⊢ (↑⌈↑n * x i⌉ - 1 + 1) / ↑n ≤ ↑(u i)

Tactic:
exact (mem_admissibleIndex_of_mem_box_aux₂ n (x i) (u i)).mp ((hu i) ▸ (hx i).2)

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : WellFoundedLT ι
f : ι → E
n : ι
h₀ : LinearIndependent 𝕜 (f ∘ Subtype.val)
⊢ gramSchmidt 𝕜 f n ≠ 0

Tactic:
by
  by_contra h
  have h₁ : f n ∈ span 𝕜 (f '' Set.Iio n) := by
    rw [← span_gramSchmidt_Iio 𝕜 f n, gramSchmidt_def' 𝕜 f, h, zero_add]
    apply Submodule.sum_mem _ _
    intro a ha
    simp only [starProjection_singleton]
    apply Submodule.smul_mem _ _ _
    rw [Finset.mem_Iio] at ha
    exact subset_span ⟨a, ha, by rfl⟩
  have h₂ : (f ∘ ((↑) : Set.Iic n → ι)) ⟨n, le_refl n⟩ ∈
      span 𝕜 (f ∘ ((↑) : Set.Iic n → ι) '' Set.Iio ⟨n, le_refl n⟩) := by
    rw [image_comp]
    simpa using h₁
  apply LinearIndependent.notMem_span_image h₀ _ h₂
  simp only [Set.mem_Iio, lt_self_iff_false, not_false_iff]

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

Goal state before:
pp: ι : Type u
E : Type v
inst✝³ : Fintype ι
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
l : IntegrationParams
I : Box ι
f : (ι → ℝ) → E
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
hl : l.bRiemann = false
ε : ℝ≥0
ε0 : 0 < ε
δ : ℕ → ℝ≥0
δ0 : ∀ (i : ℕ), 0 < δ i
c✝ : ℝ≥0
hδc : HasSum δ c✝
hcε : c✝ < ε
this : Fact (μ ↑I < ∞)
hf : (μ.restrict ↑I) {x | f x ≠ 0} = 0
N : (ι → ℝ) → ℕ := fun x ↦ ⌈‖f x‖⌉₊
N0 : ∀ {x : ι → ℝ}, N x = 0 ↔ f x = 0
U : ℕ → Set (ι → ℝ)
hNU : ∀ (n : ℕ), N ⁻¹' {n} ⊆ U n
hUo : ∀ (n : ℕ), IsOpen (U n)
r : (ι → ℝ) → ↑(Set.Ioi 0)
hrU : ∀ (x : ι → ℝ), closedBall x ↑(r x) ⊆ U (N x)
c : ℝ≥0
π : TaggedPrepartition I
hπ : l.MemBaseSet I c ((fun x ↦ r) c) π
x✝ : π.IsPartition
n : ℕ
m : ℝ≥0∞ := μ (π.filter fun J ↦ N (π.tag J) = n).iUnion
hμU : ∀ (n : ℕ), μ (U n ∩ ↑I) < ↑(δ n) / ↑n
⊢ (π.filter fun J ↦ N (π.tag J) = n).iUnion ⊆ U n ∩ ↑I

Tactic:
simp only [Set.subset_def, TaggedPrepartition.mem_iUnion, TaggedPrepartition.mem_filter]

Goal state after:
ι : Type u
E : Type v
inst✝³ : Fintype ι
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
l : IntegrationParams
I : Box ι
f : (ι → ℝ) → E
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
hl : l.bRiemann = false
ε : ℝ≥0
ε0 : 0 < ε
δ : ℕ → ℝ≥0
δ0 : ∀ (i : ℕ), 0 < δ i
c✝ : ℝ≥0
hδc : HasSum δ c✝
hcε : c✝ < ε
this : Fact (μ ↑I < ∞)
hf : (μ.restrict ↑I) {x | f x ≠ 0} = 0
N : (ι → ℝ) → ℕ := fun x ↦ ⌈‖f x‖⌉₊
N0 : ∀ {x : ι → ℝ}, N x = 0 ↔ f x = 0
U : ℕ → Set (ι → ℝ)
hNU : ∀ (n : ℕ), N ⁻¹' {n} ⊆ U n
hUo : ∀ (n : ℕ), IsOpen (U n)
r : (ι → ℝ) → ↑(Set.Ioi 0)
hrU : ∀ (x : ι → ℝ), closedBall x ↑(r x) ⊆ U (N x)
c : ℝ≥0
π : TaggedPrepartition I
hπ : l.MemBaseSet I c ((fun x ↦ r) c) π
x✝ : π.IsPartition
n : ℕ
m : ℝ≥0∞ := μ (π.filter fun J ↦ N (π.tag J) = n).iUnion
hμU : ∀ (n : ℕ), μ (U n ∩ ↑I) < ↑(δ n) / ↑n
⊢ ∀ (x : ι → ℝ), (∃ J, (J ∈ π ∧ N (π.tag J) = n) ∧ x ∈ J) → x ∈ U n ∩ ↑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
μ : 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) μ
⊢ HasIntegral I l g μ.toBoxAdditive.toSMul (∫ (a : ι → ℝ) in ↑I, g a ∂μ)

Tactic:
set f : ℕ → SimpleFunc (ι → ℝ) E :=
    SimpleFunc.approxOn g hg.measurable (range g ∪ {0}) 0 (by simp)

Goal state after:
ι : 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 ⋯
⊢ HasIntegral I l g μ.toBoxAdditive.toSMul (∫ (a : ι → ℝ) in ↑I, g a ∂μ)
Module: Mathlib.LinearAlgebra.Orientation

Goal state before:
pp: case neg
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 ι
h✝ : ¬e.orientation = x
⊢ (e.unitsSMul (Function.update 1 (Classical.arbitrary ι) (-1))).det = e.det ∨
    (e.unitsSMul (Function.update 1 (Classical.arbitrary ι) (-1))).det = -e.det

Tactic:
· right
    simp only [e.det_unitsSMul, Finset.mem_univ, Finset.prod_update_of_mem,
      Pi.one_apply, Finset.prod_const_one, mul_one, inv_neg, inv_one, Units.val_neg, Units.val_one]
    ext
    simp

Goal state after:
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 ι
inst✝ : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
h : Integrable I l f vol
ε : ℝ
ε0 : 0 < ε
⊢ ∃ ia,
    (∀ (c : ℝ≥0), l.RCond (ia c)) ∧
      ∀
        x ∈
          {π | ∃ c, l.MemBaseSet I c (ia c) π} ×ˢ {π | ∃ c, l.MemBaseSet I c (ia c) π} ∩ {π | π.1.iUnion = π.2.iUnion},
        (integralSum f vol x.1, integralSum f vol x.2) ∈ {p | dist p.1 p.2 ≤ ε}

Tactic:
replace ε0 := half_pos ε0

Goal state after:
ι : Type u
E : Type v
F : Type w
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
I : Box ι
inst✝ : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
h : Integrable I l f vol
ε : ℝ
ε0 : 0 < ε / 2
⊢ ∃ ia,
    (∀ (c : ℝ≥0), l.RCond (ia c)) ∧
      ∀
        x ∈
          {π | ∃ c, l.MemBaseSet I c (ia c) π} ×ˢ {π | ∃ c, l.MemBaseSet I c (ia c) π} ∩ {π | π.1.iUnion = π.2.iUnion},
        (integralSum f vol x.1, integralSum f vol x.2) ∈ {p | dist p.1 p.2 ≤ ε}
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 ι
π : TaggedPrepartition I
inst✝¹ : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
c : ℝ≥0
ε : ℝ
inst✝ : CompleteSpace F
h : Integrable I l f vol
h0 : 0 < ε
hπ : l.MemBaseSet I c (h.convergenceR ε c) π
π₀ : Prepartition I
hU : π.iUnion = π₀.iUnion
δ : ℝ
δ0 : 0 < δ
δ' : ℝ := δ / (↑(#π₀.boxes) + 1)
H0 : 0 < ↑(#π₀.boxes) + 1
δ'0 : 0 < δ'
C : ℝ≥0 := max π₀.distortion π₀.compl.distortion
πi : (J : Box ι) → TaggedPrepartition J
hπip : ∀ J ∈ π₀, (πi J).IsPartition
hπiδ' : ∀ J ∈ π₀, dist (integralSum f vol (πi J)) (integral J l f vol) ≤ δ'
hπiC : ∀ J ∈ π₀, l.MemBaseSet J C (h.convergenceR δ' C) (πi J)
this✝ : l.MemBaseSet I C (h.convergenceR δ' C) (π₀.biUnionTagged πi)
hU' : π.iUnion = (π₀.biUnionTagged πi).iUnion
this : dist (integralSum f vol π) (integralSum f vol (π₀.biUnionTagged πi)) ≤ ε + δ'
⊢ dist (integralSum f vol π) (∑ J ∈ π₀.boxes, integral J l f vol) ≤ ε + δ

Tactic:
integralSum_biUnionTagged

Goal state after:
ι : Type u
E : Type v
F : Type w
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
I : Box ι
π : TaggedPrepartition I
inst✝¹ : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
c : ℝ≥0
ε : ℝ
inst✝ : CompleteSpace F
h : Integrable I l f vol
h0 : 0 < ε
hπ : l.MemBaseSet I c (h.convergenceR ε c) π
π₀ : Prepartition I
hU : π.iUnion = π₀.iUnion
δ : ℝ
δ0 : 0 < δ
δ' : ℝ := δ / (↑(#π₀.boxes) + 1)
H0 : 0 < ↑(#π₀.boxes) + 1
δ'0 : 0 < δ'
C : ℝ≥0 := max π₀.distortion π₀.compl.distortion
πi : (J : Box ι) → TaggedPrepartition J
hπip : ∀ J ∈ π₀, (πi J).IsPartition
hπiδ' : ∀ J ∈ π₀, dist (integralSum f vol (πi J)) (integral J l f vol) ≤ δ'
hπiC : ∀ J ∈ π₀, l.MemBaseSet J C (h.convergenceR δ' C) (πi J)
this✝ : l.MemBaseSet I C (h.convergenceR δ' C) (π₀.biUnionTagged πi)
hU' : π.iUnion = (π₀.biUnionTagged πi).iUnion
this : dist (integralSum f vol π) (∑ J ∈ π₀.boxes, integralSum f vol (πi J)) ≤ ε + δ'
⊢ dist (integralSum f vol π) (∑ J ∈ π₀.boxes, integral J l f vol) ≤ ε + δ
Module: Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace

Goal state before:
pp: ι : Type u_1
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace ℝ F
inst✝³ : MeasurableSpace F
inst✝² : BorelSpace F
inst✝¹ : Fintype ι
inst✝ : FiniteDimensional ℝ F
b : OrthonormalBasis ι ℝ F
this : Fact (finrank ℝ F = finrank ℝ F)
o : Orientation ℝ F (Fin (finrank ℝ F)) := (stdOrthonormalBasis ℝ F).toBasis.orientation
⊢ o.volumeForm.measure (parallelepiped ⇑b) = 1

Tactic:
exact o.measure_orthonormalBasis b

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

Goal state before:
pp: α : Type u_1
u v : α → ℝ
l : Filter α
hv : 0 ≤ v
h : u ~[l] v
r : ℝ
φ : α → ℝ
hφ : Tendsto φ l (𝓝 1)
huφv : u =ᶠ[l] φ * v
⊢ ∃ φ, ∃ (_ : Tendsto φ l (𝓝 1)), u ^ r =ᶠ[l] φ * v ^ r

Tactic:
have hφr : Tendsto ((fun x ↦ x ^ r) ∘ φ) l (𝓝 1) := by
    rw [← Real.one_rpow r]
    exact Tendsto.comp (Real.continuousAt_rpow_const _ _ (by left; norm_num)) hφ

Goal state after:
α : Type u_1
u v : α → ℝ
l : Filter α
hv : 0 ≤ v
h : u ~[l] v
r : ℝ
φ : α → ℝ
hφ : Tendsto φ l (𝓝 1)
huφv : u =ᶠ[l] φ * v
hφr : Tendsto ((fun x ↦ x ^ r) ∘ φ) l (𝓝 1)
⊢ ∃ φ, ∃ (_ : Tendsto φ l (𝓝 1)), u ^ r =ᶠ[l] φ * v ^ r
Module: Mathlib.Algebra.Module.ZLattice.Covolume

Goal state before:
pp: ι : Type u_2
inst✝² : Fintype ι
L : Submodule ℤ (ι → ℝ)
inst✝¹ : DiscreteTopology ↥L
inst✝ : IsZLattice ℝ L
b : Basis ι ℤ ↥L
s : Set (ι → ℝ)
⊢ volume (⇑(Basis.ofZLatticeBasis ℝ L b).equivFun '' s) = volume s / ENNReal.ofReal (covolume L volume)

Tactic:
rw [LinearEquiv.image_eq_preimage_symm, Measure.addHaar_preimage_linearEquiv,
    LinearEquiv.symm_symm, covolume_eq_det_inv L b, ENNReal.div_eq_inv_mul,
    ENNReal.ofReal_inv_of_pos (abs_pos.2 (LinearEquiv.det _).ne_zero), inv_inv, LinearEquiv.coe_det]

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
inst✝ : Nonempty ι
X : Set E
hX : ∀ ⦃x : E⦄ ⦃r : ℝ⦄, x ∈ X → 0 < r → r • x ∈ X
F : E → ℝ
h₁ : ∀ (x : E) ⦃r : ℝ⦄, 0 ≤ r → F (r • x) = r ^ card ι * F x
h₂ : Bornology.IsBounded {x | x ∈ X ∧ F x ≤ 1}
h₃ : MeasurableSet {x | x ∈ X ∧ F x ≤ 1}
h₄ : volume (frontier (⇑(Basis.ofZLatticeBasis ℝ L b).equivFun '' {x | x ∈ X ∧ F x ≤ 1})) = 0
c : ℝ
hc : 0 < c
aux₁ : ↑(card ι) ≠ 0
aux₂ : 0 < c ^ (↑(card ι))⁻¹
⊢ ((fun x ↦
          ↑(Nat.card
                ↑(⇑(Basis.ofZLatticeBasis ℝ L b).equivFun '' {x | x ∈ X ∧ F x ≤ 1} ∩
                    x⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))))) /
            x ^ card ι) ∘
        fun x ↦ x ^ (↑(card ι))⁻¹)
      c =
    ↑(Nat.card ↑({x | x ∈ X ∧ F x ≤ c} ∩ ↑L)) / c

Tactic:
have aux₃ : (c ^ (card ι : ℝ)⁻¹)⁻¹ ≠ 0 := inv_ne_zero aux₂.ne'

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
inst✝ : Nonempty ι
X : Set E
hX : ∀ ⦃x : E⦄ ⦃r : ℝ⦄, x ∈ X → 0 < r → r • x ∈ X
F : E → ℝ
h₁ : ∀ (x : E) ⦃r : ℝ⦄, 0 ≤ r → F (r • x) = r ^ card ι * F x
h₂ : Bornology.IsBounded {x | x ∈ X ∧ F x ≤ 1}
h₃ : MeasurableSet {x | x ∈ X ∧ F x ≤ 1}
h₄ : volume (frontier (⇑(Basis.ofZLatticeBasis ℝ L b).equivFun '' {x | x ∈ X ∧ F x ≤ 1})) = 0
c : ℝ
hc : 0 < c
aux₁ : ↑(card ι) ≠ 0
aux₂ : 0 < c ^ (↑(card ι))⁻¹
aux₃ : (c ^ (↑(card ι))⁻¹)⁻¹ ≠ 0
⊢ ((fun x ↦
          ↑(Nat.card
                ↑(⇑(Basis.ofZLatticeBasis ℝ L b).equivFun '' {x | x ∈ X ∧ F x ≤ 1} ∩
                    x⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))))) /
            x ^ card ι) ∘
        fun x ↦ x ^ (↑(card ι))⁻¹)
      c =
    ↑(Nat.card ↑({x | x ∈ X ∧ F x ≤ c} ∩ ↑L)) / c
Module: Mathlib.Analysis.PSeries

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

Tactic:
rcases le_or_gt 0 p with hp | hp

Goal state after:
case inl
p : ℝ
hp : 0 ≤ p
⊢ (Summable fun n ↦ (↑n ^ p)⁻¹) ↔ 1 < p

case inr
p : ℝ
hp : p < 0
⊢ (Summable fun n ↦ (↑n ^ p)⁻¹) ↔ 1 < p
Module: Mathlib.Analysis.PSeries

Goal state before:
pp: case hdb
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
k n : ℕ
A : 1 ≤ ↑k + 1
⊢ ↑k + 1 ≤ (↑k + 1) ^ 2

Tactic:
simpa using pow_right_mono₀ A one_le_two

Goal state after:
Module: Mathlib.Analysis.PSeries

Goal state before:
pp: m : ℕ
hm : m ≠ 0
k : ZMod m
this : NeZero m
h : ∀ (n : ℕ), {n | ↑n = k - 1}.indicator (fun n ↦ 1 / ↑(n + 1)) n = if ↑n = k - 1 then 1 / (↑n + 1) else 0
⊢ ¬Summable fun n ↦ {n | ↑n = k - 1}.indicator (fun n ↦ 1 / ↑(n + 1)) n

Tactic:
rw [summable_indicator_mod_iff (fun n₁ n₂ h ↦ by gcongr) (k - 1)]

Goal state after:
m : ℕ
hm : m ≠ 0
k : ZMod m
this : NeZero m
h : ∀ (n : ℕ), {n | ↑n = k - 1}.indicator (fun n ↦ 1 / ↑(n + 1)) n = if ↑n = k - 1 then 1 / (↑n + 1) else 0
⊢ ¬Summable fun n ↦ 1 / ↑(n + 1)
Module: Mathlib.Algebra.MvPolynomial.Division

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

Tactic:
· exact dvd_mul_of_dvd_right h p

Goal state after:
Module: Mathlib.Data.Finsupp.MonomialOrder.DegLex

Goal state before:
pp: σ : Type u_2
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
a b : σ
⊢ degLex.toSyn (single a 1) ≤ degLex.toSyn (single b 1) ↔ b ≤ a

Tactic:
rw [MonomialOrder.degLex_le_iff, DegLex.single_le_iff]

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

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
hfg : m.leadingCoeff f * m.leadingCoeff g ≠ 0
⊢ m.degree f + m.degree g ∈ (f * g).support

Tactic:
rw [mem_support_iff, coeff_mul_of_degree_add]

Goal state after:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
hfg : m.leadingCoeff f * m.leadingCoeff g ≠ 0
⊢ m.leadingCoeff f * m.leadingCoeff g ≠ 0
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
hg : IsRegular (m.leadingCoeff g)
⊢ m.leadingCoeff (f * g) = m.leadingCoeff f * m.leadingCoeff g

Tactic:
by
  by_cases hf : f = 0
  · simp [hf]
  · simp only [leadingCoeff, degree_mul_of_isRegular_right hf hg, coeff_mul_of_degree_add]

Goal state after: