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 : Submodule ℝ E
hs : s ≠ ⊤
⊢ μ ↑s = 0

Tactic:
obtain ⟨x, hx⟩ : ∃ x, x ∉ s := by
    simpa only [Submodule.eq_top_iff', not_exists, Ne, not_forall] using hs
  obtain ⟨c, cpos, cone⟩ : ∃ c : ℝ, 0 < c ∧ c < 1 := ⟨1 / 2, by simp, by norm_num⟩
  have A : IsBounded (range fun n : ℕ => c ^ n • x) :=
    have : Tendsto (fun n : ℕ => c ^ n • x) atTop (𝓝 ((0 : ℝ) • x)) :=
      (tendsto_pow_atTop_nhds_zero_of_lt_one cpos.le cone).smul_const x
    isBounded_range_of_tendsto _ this
  apply addHaar_eq_zero_of_disjoint_translates μ _ A _
    (Submodule.closed_of_finiteDimensional s).measurableSet
  intro m n hmn
  simp only [Function.onFun, image_add_left, singleton_add, disjoint_left, mem_preimage,
    SetLike.mem_coe]
  intro y hym hyn
  have A : (c ^ n - c ^ m) • x ∈ s := by
    convert! s.sub_mem hym hyn using 1
    simp only [sub_smul, neg_sub_neg, add_sub_add_right_eq_sub]
  have H : c ^ n - c ^ m ≠ 0 := by
    simpa only [sub_eq_zero, Ne] using (pow_right_strictAnti₀ cpos cone).injective.ne hmn.symm
  have : x ∈ s := by
    convert! s.smul_mem (c ^ n - c ^ m)⁻¹ A
    rw [smul_smul, inv_mul_cancel₀ H, one_smul]
  exact hx this

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic

Goal state before:
pp: case refine_1
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
f_mble : AEMeasurable f μ
g_mble : AEMeasurable g μ
s : Set α
s_mble : NullMeasurableSet s μ
⊢ NullMeasurableSet (fun p ↦ Real.lt✝ (f p.1) p.2) (μ.prod volume)

Tactic:
exact nullMeasurableSet_lt (by fun_prop) measurable_snd.aemeasurable

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

Goal state before:
pp: case refine_1
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁶ : NormedField K
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace K E
b : Basis ι K E
inst✝³ : LinearOrder K
inst✝² : IsStrictOrderedRing K
inst✝¹ : FloorRing K
inst✝ : Fintype ι
q : E ⧸ span ℤ (Set.range ⇑b)
x✝¹ x✝ : E
h : x✝¹ ≈ x✝
⊢ fractRestrict b x✝¹ = fractRestrict b x✝

Tactic:
Subtype.mk.injEq,

Goal state after:
case refine_1
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁶ : NormedField K
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace K E
b : Basis ι K E
inst✝³ : LinearOrder K
inst✝² : IsStrictOrderedRing K
inst✝¹ : FloorRing K
inst✝ : Fintype ι
q : E ⧸ span ℤ (Set.range ⇑b)
x✝¹ x✝ : E
h : x✝¹ ≈ x✝
⊢ ↑(fractRestrict b x✝¹) = ↑(fractRestrict b x✝)
Module: Mathlib.Algebra.Module.ZLattice.Basic

Goal state before:
pp: case convert_1
E : Type u_1
ι : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
b : Basis ι ℝ E
inst✝ : Finite ι
h : Set.MapsTo ⇑b.equivFun ↑(span ℤ (Set.range ⇑b)) ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι)))
⊢ DiscreteTopology ↑↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι)))

pp: case convert_2
E : Type u_1
ι : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
b : Basis ι ℝ E
inst✝ : Finite ι
h : Set.MapsTo ⇑b.equivFun ↑(span ℤ (Set.range ⇑b)) ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι)))
⊢ Function.Injective
    (Set.MapsTo.restrict (⇑b.equivFun) (↑(span ℤ (Set.range ⇑b))) (↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι)))) h)

Tactic:
· exact discreteTopology_pi_basisFun

Goal state after:
case convert_2
E : Type u_1
ι : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
b : Basis ι ℝ E
inst✝ : Finite ι
h : Set.MapsTo ⇑b.equivFun ↑(span ℤ (Set.range ⇑b)) ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι)))
⊢ Function.Injective
    (Set.MapsTo.restrict (⇑b.equivFun) (↑(span ℤ (Set.range ⇑b))) (↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι)))) h)
Module: Mathlib.Analysis.BoxIntegral.Box.Basic

Goal state before:
pp: n : ℕ
I : Box (Fin (n + 1))
i : Fin (n + 1)
x : ℝ
hx : x ∈ Ioc (I.lower i) (I.upper i)
y : Fin n → ℝ
hy : y ∈ ↑(I.face i)
⊢ i.insertNth x y i ∈ Ioc (I.lower i) (I.upper i) ∧
    ∀ (i_1 : Fin n), i.insertNth x y (i.succAbove i_1) ∈ Ioc (I.lower (i.succAbove i_1)) (I.upper (i.succAbove i_1))

Tactic:
Fin.insertNth_apply_same,

Goal state after:
n : ℕ
I : Box (Fin (n + 1))
i : Fin (n + 1)
x : ℝ
hx : x ∈ Ioc (I.lower i) (I.upper i)
y : Fin n → ℝ
hy : y ∈ ↑(I.face i)
⊢ x ∈ Ioc (I.lower i) (I.upper i) ∧
    ∀ (i_1 : Fin n), i.insertNth x y (i.succAbove i_1) ∈ Ioc (I.lower (i.succAbove i_1)) (I.upper (i.succAbove i_1))
Module: Mathlib.Analysis.BoxIntegral.Partition.Basic

Goal state before:
pp: ι : Type u_1
I : Box ι
M : Type u_2
inst✝ : AddCommMonoid M
π : Prepartition I
πi : (J : Box ι) → Prepartition J
f : Box ι → M
⊢ ∑ J ∈ π.boxes.biUnion fun J ↦ (πi J).boxes, f J = ∑ J ∈ π.boxes, ∑ J' ∈ (πi J).boxes, f J'

Tactic:
refine Finset.sum_biUnion fun J₁ h₁ J₂ h₂ hne => Finset.disjoint_left.2 fun J' h₁' h₂' => ?_

Goal state after:
ι : Type u_1
I : Box ι
M : Type u_2
inst✝ : AddCommMonoid M
π : Prepartition I
πi : (J : Box ι) → Prepartition J
f : Box ι → M
J₁ : Box ι
h₁ : J₁ ∈ ↑π.boxes
J₂ : Box ι
h₂ : J₂ ∈ ↑π.boxes
hne : J₁ ≠ J₂
J' : Box ι
h₁' : J' ∈ (fun J ↦ (πi J).boxes) J₁
h₂' : J' ∈ (fun J ↦ (πi J).boxes) J₂
⊢ False
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
A : Tendsto (fun n ↦ μ (t \ closedBall 0 ↑n)) atTop (𝓝 (μ (⋂ n, t \ closedBall 0 ↑n)))
⊢ ⋂ n, t ∩ (closedBall 0 ↑n)ᶜ = ∅

Tactic:
← inter_iInter,

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
A : Tendsto (fun n ↦ μ (t \ closedBall 0 ↑n)) atTop (𝓝 (μ (⋂ n, t \ closedBall 0 ↑n)))
⊢ t ∩ ⋂ i, (closedBall 0 ↑i)ᶜ = ∅
Module: Mathlib.Analysis.InnerProductSpace.PiL2

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
𝕜 : Type u_3
inst✝⁷ : RCLike 𝕜
E : Type u_4
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
F : Type u_5
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
F' : Type u_6
inst✝² : NormedAddCommGroup F'
inst✝¹ : InnerProductSpace ℝ F'
inst✝ : Fintype ι
b b' : OrthonormalBasis ι 𝕜 E
i : ι
k : 𝕜
this : k = k • 1
h : (fun b i ↦ b.repr.symm (EuclideanSpace.single i 1)) b i = (fun b i ↦ b.repr.symm (EuclideanSpace.single i 1)) b' i
⊢ (↑b.repr.symm ∘ₗ ↑(WithLp.linearEquiv 2 𝕜 (ι → 𝕜)).symm) (k • Pi.single i 1) =
    (↑b'.repr.symm ∘ₗ ↑(WithLp.linearEquiv 2 𝕜 (ι → 𝕜)).symm) (k • Pi.single i 1)

Tactic:
simp only [LinearEquiv.comp_coe, map_smul, LinearEquiv.coe_coe, LinearEquiv.trans_apply,
          coe_symm_linearEquiv, PiLp.toLp_single,
          LinearIsometryEquiv.coe_symm_toLinearEquiv] at h ⊢

Goal state after:
ι : Type u_1
ι' : Type u_2
𝕜 : Type u_3
inst✝⁷ : RCLike 𝕜
E : Type u_4
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
F : Type u_5
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
F' : Type u_6
inst✝² : NormedAddCommGroup F'
inst✝¹ : InnerProductSpace ℝ F'
inst✝ : Fintype ι
b b' : OrthonormalBasis ι 𝕜 E
i : ι
k : 𝕜
this : k = k • 1
h : b.repr.symm (EuclideanSpace.single i 1) = b'.repr.symm (EuclideanSpace.single i 1)
⊢ k • b.repr.symm (PiLp.single 2 i 1) = k • b'.repr.symm (PiLp.single 2 i 1)
Module: Mathlib.Analysis.BoxIntegral.Partition.Split

Goal state before:
pp: ι : Type u_1
I : Box ι
i : ι
x : ℝ
⊢ (univ.pi fun i_1 ↦ Ioc (I.lower i_1) (update I.upper i (min x (I.upper i)) i_1)) = ↑I ∩ {y | y i ≤ x}

Tactic:
ext y

Goal state after:
ι : Type u_1
I : Box ι
i : ι
x : ℝ
y : ι → ℝ
⊢ (y ∈ univ.pi fun i_1 ↦ Ioc (I.lower i_1) (update I.upper i (min x (I.upper i)) i_1)) ↔ y ∈ ↑I ∩ {y | y i ≤ x}
Module: Mathlib.Analysis.BoxIntegral.Partition.Split

Goal state before:
pp: ι : Type u_1
I : Box ι
i : ι
x : ℝ
⊢ (univ.pi fun i_1 ↦ Ioc (update I.lower i (max x (I.lower i)) i_1) (I.upper i_1)) = ↑I ∩ {y | x < y i}

Tactic:
ext y

Goal state after:
ι : Type u_1
I : Box ι
i : ι
x : ℝ
y : ι → ℝ
⊢ (y ∈ univ.pi fun i_1 ↦ Ioc (update I.lower i (max x (I.lower i)) i_1) (I.upper i_1)) ↔ y ∈ ↑I ∩ {y | x < y i}
Module: Mathlib.Analysis.InnerProductSpace.PiL2

Goal state before:
pp: 𝕜 : Type u_3
inst✝⁴ : RCLike 𝕜
E : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : FiniteDimensional 𝕜 E
ι : Type u_7
inst✝ : Fintype ι
card_ι : finrank 𝕜 E = Fintype.card ι
v : ι → E
s : Set ι
hv : Orthonormal 𝕜 (s.domRestrict v)
hsv : Injective (s.domRestrict v)
hX✝ : Orthonormal 𝕜 Subtype.val
Y : Finset E
b₀ : OrthonormalBasis (↥Y) 𝕜 E
hX : range (s.domRestrict v) ⊆ ↑Y
hb₀ : ⇑b₀ = Subtype.val
⊢ finrank 𝕜 E = Y.card

Tactic:
exact Module.finrank_eq_card_finset_basis b₀.toBasis

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

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
𝕜 : Type u_3
inst✝⁸ : RCLike 𝕜
E : Type u_4
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace 𝕜 E
F : Type u_5
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace ℝ F
F' : Type u_6
inst✝³ : NormedAddCommGroup F'
inst✝² : InnerProductSpace ℝ F'
inst✝¹ : Fintype ι
v : Set E
A : ι → Submodule 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
b : OrthonormalBasis (↥(Classical.choose ⋯)) 𝕜 E := Classical.choose ⋯
⊢ OrthonormalBasis (Fin (finrank 𝕜 E)) 𝕜 E

Tactic:
rw [finrank_eq_card_basis b.toBasis]

Goal state after:
ι : Type u_1
ι' : Type u_2
𝕜 : Type u_3
inst✝⁸ : RCLike 𝕜
E : Type u_4
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace 𝕜 E
F : Type u_5
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace ℝ F
F' : Type u_6
inst✝³ : NormedAddCommGroup F'
inst✝² : InnerProductSpace ℝ F'
inst✝¹ : Fintype ι
v : Set E
A : ι → Submodule 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
b : OrthonormalBasis (↥(Classical.choose ⋯)) 𝕜 E := Classical.choose ⋯
⊢ OrthonormalBasis (Fin (Fintype.card ↥(Classical.choose ⋯))) 𝕜 E
Module: Mathlib.Analysis.InnerProductSpace.PiL2

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
𝕜 : Type u_3
inst✝⁸ : RCLike 𝕜
E : Type u_4
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace 𝕜 E
F : Type u_5
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace ℝ F
F' : Type u_6
inst✝³ : NormedAddCommGroup F'
inst✝² : InnerProductSpace ℝ F'
inst✝¹ : Fintype ι
v : Set E
A : ι → Submodule 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
⊢ OrthonormalBasis (Fin (finrank 𝕜 E)) 𝕜 E

Tactic:
by
  let b := Classical.choose (Classical.choose_spec <| exists_orthonormalBasis 𝕜 E)
  rw [finrank_eq_card_basis b.toBasis]
  exact b.reindex (Fintype.equivFinOfCardEq rfl)

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
⊢ (s ∩ ↑((↑n)⁻¹ • span ℤ (Set.range ⇑(Pi.basisFun ℝ ι)))).Finite

Tactic:
ZSpan.smul _ (inv_ne_zero (NeZero.ne _))

Goal state after:
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
s : Set (ι → ℝ)
F : (ι → ℝ) → ℝ
inst✝ : Fintype ι
B : Box ι
hB : hasIntegralVertices B
hs₀ : s ⊆ ↑B
⊢ (s ∩ ↑(span ℤ (Set.range ⇑((Pi.basisFun ℝ ι).isUnitSMul ⋯)))).Finite
Module: Mathlib.Analysis.BoxIntegral.UnitPartition

Goal state before:
pp: ι : Type u_1
s : Set (ι → ℝ)
F : (ι → ℝ) → ℝ
inst✝ : Fintype ι
hF : Continuous F
hs₁ : Bornology.IsBounded s
hs₂ : MeasurableSet s
hs₃ : volume (frontier s) = 0
B : Box ι
hB : hasIntegralVertices B
hs₀ : s ⊆ ↑B
ε : ℝ
hε : ε > 0
C₀ : ℝ
h₀ : ∀ x ∈ Box.Icc B, ‖F x‖ ≤ C₀
x : ι → ℝ
hx : x ∈ Box.Icc B
⊢ ‖s.indicator F x‖ ≤ max 0 C₀

Tactic:
Set.indicator

Goal state after:
ι : Type u_1
s : Set (ι → ℝ)
F : (ι → ℝ) → ℝ
inst✝ : Fintype ι
hF : Continuous F
hs₁ : Bornology.IsBounded s
hs₂ : MeasurableSet s
hs₃ : volume (frontier s) = 0
B : Box ι
hB : hasIntegralVertices B
hs₀ : s ⊆ ↑B
ε : ℝ
hε : ε > 0
C₀ : ℝ
h₀ : ∀ x ∈ Box.Icc B, ‖F x‖ ≤ C₀
x : ι → ℝ
hx : x ∈ Box.Icc B
⊢ ‖if x ∈ s then F x else 0‖ ≤ max 0 C₀
Module: Mathlib.Analysis.BoxIntegral.UnitPartition

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

Tactic:
filter_upwards [eventually_ge_atTop 1] with x hx
  rw [div_pow, mul_div, div_mul_cancel₀ _ (by positivity)]

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 π.iUnion * ↑ε

Tactic:
π.measure_iUnion_toReal,

Goal state after:
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)) ≤
    (∑ J ∈ π.boxes, μ.real ↑J) * ↑ε
Module: Mathlib.Algebra.Module.ZLattice.Covolume

Goal state before:
pp: E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : InnerProductSpace ℝ E
inst✝⁶ : FiniteDimensional ℝ E
inst✝⁵ : MeasurableSpace E
inst✝⁴ : BorelSpace E
L₁ L₂ : Submodule ℤ E
inst✝³ : DiscreteTopology ↥L₁
inst✝² : IsZLattice ℝ L₁
inst✝¹ : DiscreteTopology ↥L₂
inst✝ : IsZLattice ℝ L₂
h : L₁ ≤ L₂
⊢ covolume L₁ volume / covolume L₂ volume = ↑(L₁.toAddSubgroup.relIndex L₂.toAddSubgroup)

Tactic:
by
  let f := (EuclideanSpace.equiv _ ℝ).symm.trans
    (stdOrthonormalBasis ℝ E).repr.toContinuousLinearEquiv.symm
  have hf : MeasurePreserving f := (stdOrthonormalBasis ℝ E).measurePreserving_repr_symm.comp
    (EuclideanSpace.volume_preserving_symm_measurableEquiv_toLp _).symm
  rw [← covolume_comap L₁ volume volume hf, ← covolume_comap L₂ volume volume hf,
    covolume_div_covolume_eq_relIndex _ _ (fun _ h' ↦ h h'), ZLattice.comap_toAddSubgroup,
    ZLattice.comap_toAddSubgroup, Nat.cast_inj, LinearEquiv.toAddMonoidHom_commutes,
    AddSubgroup.comap_equiv_eq_map_symm', AddSubgroup.comap_equiv_eq_map_symm',
    AddSubgroup.relIndex_map_map_of_injective _ _ f.symm.injective]

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 : ℕ
⊢ ∑ k ∈ range (n + 1), (u (k + 1) - u k) • f (u k) ≤ (u 1 - u 0) • f (u 0) + C • ∑ k ∈ Ico (u 0 + 1) (u n + 1), f k

Tactic:
sum_range_succ',

Goal state after:
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 : ℕ
⊢ ∑ k ∈ range n, (u (k + 1 + 1) - u (k + 1)) • f (u (k + 1)) + (u (0 + 1) - u 0) • f (u 0) ≤
    (u 1 - u 0) • f (u 0) + C • ∑ k ∈ Ico (u 0 + 1) (u n + 1), f k
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 • (u (k + 1) - u k) • f (u (k + 1))
⊢ C • ∑ k ∈ range n, (u (k + 1) - u k) • f (u (k + 1)) = ∑ i ∈ range n, C • (u (i + 1) - u i) • f (u (i + 1))

Tactic:
simp [smul_sum]

Goal state after:
Module: Mathlib.Analysis.PSeries

Goal state before:
pp: m : ℕ
hm : m ≠ 0
k : ZMod m
⊢ ¬Summable ({n | ↑n = k}.indicator fun n ↦ 1 / ↑n)

Tactic:
have : NeZero m := ⟨hm⟩

Goal state after:
m : ℕ
hm : m ≠ 0
k : ZMod m
this : NeZero m
⊢ ¬Summable ({n | ↑n = k}.indicator fun n ↦ 1 / ↑n)
Module: Mathlib.Algebra.Module.ZLattice.Covolume

Goal state before:
pp: ι : Type u_1
inst✝³ : Fintype ι
L : Submodule ℤ (ι → ℝ)
inst✝² : DiscreteTopology ↥L
inst✝¹ : IsZLattice ℝ L
X : Set (ι → ℝ)
hX : ∀ ⦃x : ι → ℝ⦄ ⦃r : ℝ⦄, x ∈ X → 0 < r → r • x ∈ X
F : (ι → ℝ) → ℝ
h₁ : ∀ (x : ι → ℝ) ⦃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 {x | x ∈ X ∧ F x ≤ 1}) = 0
inst✝ : Nonempty ι
⊢ Free.ChooseBasisIndex ℤ ↥L ≃ ι

Tactic:
by
    refine Fintype.equivOfCardEq ?_
    rw [← finrank_eq_card_chooseBasisIndex, ZLattice.rank ℝ, finrank_fintype_fun_eq_card]

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
i j : σ
⊢ (Finsupp.single j 1) i ≠ 0 ↔ i = j

Tactic:
Finsupp.single_apply_ne_zero,

Goal state after:
σ : Type u_1
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
i j : σ
⊢ i = j ∧ 1 ≠ 0 ↔ i = j
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
hp : p.modMonomial (Finsupp.single i 1) + X i * p.divMonomial (Finsupp.single i 1) = p
hq : q.modMonomial (Finsupp.single i 1) + X i * q.divMonomial (Finsupp.single i 1) = q
⊢ X i ∣ p * q - p.modMonomial (Finsupp.single i 1) * q.modMonomial (Finsupp.single i 1)

Tactic:
· nth_rewrite 1 [← hp]
      nth_rewrite 1 [← hq]
      simp only [add_mul, mul_add, add_assoc, add_sub_cancel_left]
      simp only [← mul_assoc, mul_comm _ (X i)]
      simp only [mul_assoc, ← mul_add (X i)]
      apply dvd_mul_right

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

Goal state before:
pp: case cons.e_a.e_a
α : Type u_1
R : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Semiring R
f✝ : α → R
a : α
s : Finset α
has : a ∉ s
ih :
  ∀ (hc : (↑s).Pairwise (Commute on f✝)) (n : ℕ),
    (∑ i ∈ s, f✝ i) ^ n = ∑ k ∈ s.piAntidiag n, ↑(multinomial s k) * s.noncommProd (fun i ↦ f✝ i ^ k i) ⋯
hc : (↑(cons a s has)).Pairwise (Commute on f✝)
n : ℕ
p : ℕ × ℕ
hp : p ∈ antidiagonal n
f : α → ℕ
hf : s.sum f = p.2 ∧ ∀ (i : α), f i ≠ 0 → i ∈ s
⊢ ↑(multinomial s (f + fun i ↦ if i = a then p.1 else 0)) = ↑(multinomial s f)

Tactic:
rw [multinomial_congr]
    intro t ht
    rw [Pi.add_apply, if_neg, add_zero]
    exact ne_of_mem_of_not_mem ht has

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

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

Tactic:
rintro (_ | n)

Goal state after:
case empty.zero
α : Type u_1
R : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Semiring R
x : α → R
hc : (↑∅).Pairwise (Commute on x)
⊢ 0 ^ 0 = ∑ k, ↑(↑↑k).countPerms * (Multiset.map x ↑↑k).noncommProd ⋯

case empty.succ
α : Type u_1
R : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Semiring R
x : α → R
hc : (↑∅).Pairwise (Commute on x)
n : ℕ
⊢ 0 ^ (n + 1) = ∑ k, ↑(↑↑k).countPerms * (Multiset.map x ↑↑k).noncommProd ⋯
Module: Mathlib.Algebra.MvPolynomial.Division

Goal state before:
pp: case inr
σ : Type u_1
R : Type u_3
inst✝¹ : CommRing R
p q : MvPolynomial σ R
inst✝ : IsCancelMulZero R
n : σ →₀ ℕ
hR : Nontrivial R
d : ℕ
⊢ ∀ (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

Tactic:
induction d with

Goal state after:
Module: Mathlib.Order.GameAdd

Goal state before:
pp: case intro.intro.h
α : Type u_1
rα : α → α → Prop
a✝ a : α
h✝ : ∀ (y : α), rα y a → Acc rα y
iha : ∀ (y : α), rα y a → ∀ {b : α}, Acc rα b → Acc (Sym2.GameAdd rα) s(y, b)
b✝ b : α
hb : ∀ (y : α), rα y b → Acc rα y
ihb : ∀ (y : α), rα y b → Acc (Sym2.GameAdd rα) s(a, y)
c d : α
⊢ Sym2.GameAdd rα s(c, d) s(a, b) → Acc (Sym2.GameAdd rα) s(c, d)

Tactic:
rw [Sym2.GameAdd]

Goal state after:
case intro.intro.h
α : Type u_1
rα : α → α → Prop
a✝ a : α
h✝ : ∀ (y : α), rα y a → Acc rα y
iha : ∀ (y : α), rα y a → ∀ {b : α}, Acc rα b → Acc (Sym2.GameAdd rα) s(y, b)
b✝ b : α
hb : ∀ (y : α), rα y b → Acc rα y
ihb : ∀ (y : α), rα y b → Acc (Sym2.GameAdd rα) s(a, y)
c d : α
⊢ Sym2.lift₂ ⟨fun a₁ b₁ a₂ b₂ ↦ Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂), ⋯⟩ s(c, d)
      s(a, b) →
    Acc (Sym2.lift₂ ⟨fun a₁ b₁ a₂ b₂ ↦ Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂), ⋯⟩)
      s(c, d)
Module: Mathlib.Data.Finsupp.MonomialOrder.DegLex

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a✝ b✝ : α
h : a✝ < b✝
⊢ (fun a ↦ toDegLex (single a 1)) b✝ < (fun a ↦ toDegLex (single a 1)) a✝

Tactic:
simp only [lt_iff, ofDegLex_toDegLex, degree_single, lt_self_iff_false, Lex.single_lt_iff, h,
    and_self, or_true]

Goal state after:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Nat

Goal state before:
pp: s : Multiset ℕ
h : ∀ x ∈ s, Irreducible x
⊢ s.prod ≠ 0

Tactic:
rw [Ne, Multiset.prod_eq_zero_iff]

Goal state after:
s : Multiset ℕ
h : ∀ x ∈ s, Irreducible x
⊢ 0 ∉ s
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:
by
  classical
  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: n : ℕ
h0 : n ≠ 0
s : Finset ℕ
hs : s.val ≤ (normalizedFactors n).dedup
⊢ s.val.prod ≠ 0

Tactic:
rw [Ne, Multiset.prod_eq_zero_iff]

Goal state after:
n : ℕ
h0 : n ≠ 0
s : Finset ℕ
hs : s.val ≤ (normalizedFactors n).dedup
⊢ 0 ∉ s.val