mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Function.SpecialFunctions.Inner

Goal state before:
pp: α : Type u_1
𝕜 : Type u_2
E : Type u_3
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
m : MeasurableSpace α
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
inst✝ : SecondCountableTopology E
μ : MeasureTheory.Measure α
f g : α → E
hf : AEMeasurable f μ
hg : AEMeasurable g μ
⊢ AEMeasurable (fun x ↦ ⟪f x, g x⟫) μ

Tactic:
by
  fun_prop

Goal state after:
Module: Mathlib.MeasureTheory.Group.FoelnerFilter

Goal state before:
pp: G : Type u_1
X : Type u_2
inst✝² : MeasurableSpace X
μ : Measure X
inst✝¹ : Group G
inst✝ : MulAction G X
ι : Type u_3
u : Ultrafilter ι
F : ι → Set X
hfoel : IsFoelner G μ (↑u) F
s : Set X
i : ι
⊢ μ (F i) ≠ 0 → μ (F i) ≠ ∞ → μ (s ∩ F i) / μ (F i) ∈ Icc 0 1

Tactic:
hi

Goal state after:
G : Type u_1
X : Type u_2
inst✝² : MeasurableSpace X
μ : Measure X
inst✝¹ : Group G
inst✝ : MulAction G X
ι : Type u_3
u : Ultrafilter ι
F : ι → Set X
hfoel : IsFoelner G μ (↑u) F
s : Set X
i : ι
hi : μ (F i) ≠ 0
⊢ μ (F i) ≠ ∞ → μ (s ∩ F i) / μ (F i) ∈ Icc 0 1
Module: Mathlib.MeasureTheory.Group.IntegralConvolution

Goal state before:
pp: M : Type u_1
F : Type u_2
inst✝⁵ : Monoid M
mM : MeasurableSpace M
inst✝⁴ : MeasurableMul₂ M
inst✝³ : NormedAddCommGroup F
μ ν : Measure M
f : M → F
inst✝² : NormedSpace ℝ F
inst✝¹ : SFinite μ
inst✝ : SFinite ν
hf : Integrable f (μ ∗ₘ ν)
⊢ ∫ (x : M), f x ∂μ ∗ₘ ν = ∫ (x : M), ∫ (y : M), f (x * y) ∂ν ∂μ

Tactic:
by
  unfold Measure.mconv
  rw [integral_map (by fun_prop) hf.1, integral_prod]
  exact (integrable_map_measure hf.1 (by fun_prop)).mp hf

Goal state after:
Module: Mathlib.MeasureTheory.Group.FoelnerFilter

Goal state before:
pp: G : Type u_1
X : Type u_2
inst✝² : MeasurableSpace X
μ : Measure X
inst✝¹ : Group G
inst✝ : MulAction G X
ι : Type u_3
u : Ultrafilter ι
F : ι → Set X
hfoel : IsFoelner G μ (↑u) F
i : ι
⊢ μ (F i) ≠ 0 → μ (F i) ≠ ∞ → μ (univ ∩ F i) / μ (F i) = 1

Tactic:
hi

Goal state after:
G : Type u_1
X : Type u_2
inst✝² : MeasurableSpace X
μ : Measure X
inst✝¹ : Group G
inst✝ : MulAction G X
ι : Type u_3
u : Ultrafilter ι
F : ι → Set X
hfoel : IsFoelner G μ (↑u) F
i : ι
hi : μ (F i) ≠ 0
⊢ μ (F i) ≠ ∞ → μ (univ ∩ F i) / μ (F i) = 1
Module: Mathlib.MeasureTheory.Group.FoelnerFilter

Goal state before:
pp: G : Type u_1
X : Type u_2
inst✝² : MeasurableSpace X
μ : Measure X
inst✝¹ : Group G
inst✝ : MulAction G X
ι : Type u_3
u : Ultrafilter ι
F : ι → Set X
hfoel : IsFoelner G μ (↑u) F
⊢ mean μ u F univ = 1

Tactic:
by
  refine tendsto_nhds_unique_of_eventuallyEq (hfoel.tendsto_nhds_mean _) tendsto_const_nhds ?_
  filter_upwards [hfoel.eventually_meas_ne_zero, hfoel.eventually_meas_ne_top] with i hi hi'
  simp [ENNReal.div_self hi hi']

Goal state after:
Module: Mathlib.MeasureTheory.Group.FoelnerFilter

Goal state before:
pp: G : Type u_1
X : Type u_2
inst✝² : MeasurableSpace X
μ : Measure X
inst✝¹ : Group G
inst✝ : MulAction G X
ι : Type u_3
u : Ultrafilter ι
F : ι → Set X
hfoel : IsFoelner G μ (↑u) F
s t : Set X
ht : MeasurableSet t
hdisj : Disjoint s t
i : ι
⊢ MeasurableSet (F i) → μ ((s ∪ t) ∩ F i) / μ (F i) = μ (s ∩ F i) / μ (F i) + μ (t ∩ F i) / μ (F i)

Tactic:
hi

Goal state after:
G : Type u_1
X : Type u_2
inst✝² : MeasurableSpace X
μ : Measure X
inst✝¹ : Group G
inst✝ : MulAction G X
ι : Type u_3
u : Ultrafilter ι
F : ι → Set X
hfoel : IsFoelner G μ (↑u) F
s t : Set X
ht : MeasurableSet t
hdisj : Disjoint s t
i : ι
hi : MeasurableSet (F i)
⊢ μ ((s ∪ t) ∩ F i) / μ (F i) = μ (s ∩ F i) / μ (F i) + μ (t ∩ F i) / μ (F i)
Module: Mathlib.MeasureTheory.Group.FoelnerFilter

Goal state before:
pp: G : Type u_1
X : Type u_2
inst✝³ : MeasurableSpace X
μ : Measure X
inst✝² : Group G
inst✝¹ : MulAction G X
ι : Type u_3
u : Ultrafilter ι
F : ι → Set X
inst✝ : SMulInvariantMeasure G X μ
hfoel : IsFoelner G μ (↑u) F
g✝ h✝ : G
s : Set X
g h : G
i : ι
⊢ μ (F i) ≠ 0 → μ (g • s ∩ F i) / μ (F i) ≤ μ (h • s ∩ F i) / μ (F i) + μ ((g⁻¹ • F i) ∆ (h⁻¹ • F i)) / μ (F i)

Tactic:
hi

Goal state after:
G : Type u_1
X : Type u_2
inst✝³ : MeasurableSpace X
μ : Measure X
inst✝² : Group G
inst✝¹ : MulAction G X
ι : Type u_3
u : Ultrafilter ι
F : ι → Set X
inst✝ : SMulInvariantMeasure G X μ
hfoel : IsFoelner G μ (↑u) F
g✝ h✝ : G
s : Set X
g h : G
i : ι
hi : μ (F i) ≠ 0
⊢ μ (g • s ∩ F i) / μ (F i) ≤ μ (h • s ∩ F i) / μ (F i) + μ ((g⁻¹ • F i) ∆ (h⁻¹ • F i)) / μ (F i)
Module: Mathlib.MeasureTheory.Group.ModularCharacter

Goal state before:
pp: case refine_2
G : Type u_1
inst✝⁶ : TopologicalSpace G
inst✝⁵ : Group G
inst✝⁴ : IsTopologicalGroup G
inst✝³ : LocallyCompactSpace G
inst✝² : MeasurableSpace G
inst✝¹ : BorelSpace G
μ : Measure G
inst✝ : μ.IsHaarMeasure
g : G
ν : Measure G := haar
f : G → ℝ
f_cont : Continuous f
f_comp : HasCompactSupport ⇑{ toFun := f, continuous_toFun := f_cont }
f_nonneg : 0 ≤ { toFun := f, continuous_toFun := f_cont }
f_one : { toFun := f, continuous_toFun := f_cont } 1 ≠ 0
int_f_ne_zero : ∀ (μ₀ : Measure G) [μ₀.IsHaarMeasure], ∫ (x : G), f x ∂μ₀ ≠ 0
⊢ HasCompactSupport fun x ↦ f (x * g)

Tactic:
have j : (fun x ↦ f (x * g)) = (f ∘ (Homeomorph.mulRight g)) := rfl
      rw [j]
      exact HasCompactSupport.comp_homeomorph f_comp _

Goal state after:
Module: Mathlib.MeasureTheory.Group.ModularCharacter

Goal state before:
pp: G : Type u_1
inst✝⁶ : TopologicalSpace G
inst✝⁵ : Group G
inst✝⁴ : IsTopologicalGroup G
inst✝³ : LocallyCompactSpace G
inst✝² : MeasurableSpace G
inst✝¹ : BorelSpace G
μ : Measure G
inst✝ : μ.IsHaarMeasure
g : G
ν : Measure G := haar
f : G → ℝ
f_cont : Continuous f
f_comp : HasCompactSupport ⇑{ toFun := f, continuous_toFun := f_cont }
f_nonneg : 0 ≤ { toFun := f, continuous_toFun := f_cont }
f_one : { toFun := f, continuous_toFun := f_cont } 1 ≠ 0
int_f_ne_zero : ∀ (μ₀ : Measure G) [μ₀.IsHaarMeasure], ∫ (x : G), f x ∂μ₀ ≠ 0
t : ∫ (x : G), f (x * g) ∂ν = ∫ (x : G), f (x * g) ∂ν.haarScalarFactor μ • μ
r : ↑(ν.haarScalarFactor μ) / ↑(ν.haarScalarFactor μ) = 1
⊢ (∫ (x : G), f (x * g) ∂ν.haarScalarFactor μ • μ) / ∫ (x : G), f x ∂ν.haarScalarFactor μ • μ =
    (ν.haarScalarFactor μ • ∫ (x : G), f (x * g) ∂μ) / ν.haarScalarFactor μ • ∫ (x : G), f x ∂μ

Tactic:
by
    rw [integral_smul_nnreal_measure, integral_smul_nnreal_measure]

Goal state after:
Module: Mathlib.MeasureTheory.Group.GeometryOfNumbers

Goal state before:
pp: case refine_1
E : Type u_1
inst✝⁶ : MeasurableSpace E
μ : Measure E
F s : Set E
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : BorelSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : μ.IsAddHaarMeasure
L : AddSubgroup E
inst✝ : Countable ↥L
fund : IsAddFundamentalDomain (↥L) F μ
h_symm : ∀ x ∈ s, -x ∈ s
h_conv : Convex ℝ s
h✝ : μ F * 2 ^ finrank ℝ E < μ s
h_vol : μ F < μ (2⁻¹ • s)
x y : ↥L
hxy : x ≠ y
h : ¬Disjoint (x +ᵥ 2⁻¹ • s) (y +ᵥ 2⁻¹ • s)
v : E
hv : 2 • v ∈ s
w : E
hw : 2 • w ∈ s
hvw : w - v = ↑(x - y)
⊢ 0 ≤ 2⁻¹

Tactic:
norm_num

Goal state after:
Module: Mathlib.MeasureTheory.Group.GeometryOfNumbers

Goal state before:
pp: case refine_2
E : Type u_1
inst✝⁶ : MeasurableSpace E
μ : Measure E
F s : Set E
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : BorelSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : μ.IsAddHaarMeasure
L : AddSubgroup E
inst✝ : Countable ↥L
fund : IsAddFundamentalDomain (↥L) F μ
h_symm : ∀ x ∈ s, -x ∈ s
h_conv : Convex ℝ s
h✝ : μ F * 2 ^ finrank ℝ E < μ s
h_vol : μ F < μ (2⁻¹ • s)
x y : ↥L
hxy : x ≠ y
h : ¬Disjoint (x +ᵥ 2⁻¹ • s) (y +ᵥ 2⁻¹ • s)
v : E
hv : 2 • v ∈ s
w : E
hw : 2 • w ∈ s
hvw : w - v = ↑(x - y)
⊢ 0 ≤ 2⁻¹

Tactic:
norm_num

Goal state after:
Module: Mathlib.MeasureTheory.Group.GeometryOfNumbers

Goal state before:
pp: case refine_3
E : Type u_1
inst✝⁶ : MeasurableSpace E
μ : Measure E
F s : Set E
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : BorelSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : μ.IsAddHaarMeasure
L : AddSubgroup E
inst✝ : Countable ↥L
fund : IsAddFundamentalDomain (↥L) F μ
h_symm : ∀ x ∈ s, -x ∈ s
h_conv : Convex ℝ s
h✝ : μ F * 2 ^ finrank ℝ E < μ s
h_vol : μ F < μ (2⁻¹ • s)
x y : ↥L
hxy : x ≠ y
h : ¬Disjoint (x +ᵥ 2⁻¹ • s) (y +ᵥ 2⁻¹ • s)
v : E
hv : 2 • v ∈ s
w : E
hw : 2 • w ∈ s
hvw : w - v = ↑(x - y)
⊢ 2⁻¹ + 2⁻¹ = 1

Tactic:
norm_num

Goal state after:
Module: Mathlib.MeasureTheory.Integral.CircleTransform

Goal state before:
pp: R r : ℝ
hr : r < R
hr' : 0 ≤ r
z : ℂ
⊢ ∃ x,
    ∀ (y : ↑(closedBall z r ×ˢ [[0, 2 * π]])),
      ‖circleTransformBoundingFunction R z ↑y‖ ≤ ‖circleTransformBoundingFunction R z ↑x‖

Tactic:
have cts := continuousOn_norm_circleTransformBoundingFunction hr z

Goal state after:
R r : ℝ
hr : r < R
hr' : 0 ≤ r
z : ℂ
cts : ContinuousOn ((fun x ↦ ‖x‖) ∘ circleTransformBoundingFunction R z) (closedBall z r ×ˢ univ)
⊢ ∃ x,
    ∀ (y : ↑(closedBall z r ×ˢ [[0, 2 * π]])),
      ‖circleTransformBoundingFunction R z ↑y‖ ≤ ‖circleTransformBoundingFunction R z ↑x‖
Module: Mathlib.Topology.ContinuousMap.CompactlySupported

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁴ : TopologicalSpace α
δ : Type u_5
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : TopologicalSpace δ
inst✝ : Zero δ
f : γ →C_c δ
g : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
x : β
hx : ∀ (o : Set β), IsOpen o → x ∈ o → (o ∩ Function.support (⇑f ∘ ⇑g)).Nonempty
o : Set γ
ho : IsOpen o
hgxo : g x ∈ o
⊢ (o ∩ Function.support f.toFun).Nonempty

Tactic:
obtain ⟨y, hy⟩ := hx (g ⁻¹' o) (IsOpen.preimage g.1.2 ho) hgxo

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁴ : TopologicalSpace α
δ : Type u_5
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : TopologicalSpace δ
inst✝ : Zero δ
f : γ →C_c δ
g : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
x : β
hx : ∀ (o : Set β), IsOpen o → x ∈ o → (o ∩ Function.support (⇑f ∘ ⇑g)).Nonempty
o : Set γ
ho : IsOpen o
hgxo : g x ∈ o
y : β
hy : y ∈ ⇑g ⁻¹' o ∩ Function.support (⇑f ∘ ⇑g)
⊢ (o ∩ Function.support f.toFun).Nonempty
Module: Mathlib.Topology.ContinuousMap.CompactlySupported

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : TopologicalSpace α
Λ : (α →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
f g : α →C_c ℝ
h : α →C_c ℝ≥0
hh : (f + g).nnrealPart + h = f.nnrealPart + g.nnrealPart ∧ (-f + -g).nnrealPart + h = (-f).nnrealPart + (-g).nnrealPart
⊢ ↑(Λ (f.nnrealPart + g.nnrealPart)) - ↑(Λ ((-f + -g).nnrealPart + h)) =
    ↑(Λ f.nnrealPart) - ↑(Λ (-f).nnrealPart) + (↑(Λ g.nnrealPart) - ↑(Λ (-g).nnrealPart))

Tactic:
hh.2

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : TopologicalSpace α
Λ : (α →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
f g : α →C_c ℝ
h : α →C_c ℝ≥0
hh : (f + g).nnrealPart + h = f.nnrealPart + g.nnrealPart ∧ (-f + -g).nnrealPart + h = (-f).nnrealPart + (-g).nnrealPart
⊢ ↑(Λ (f.nnrealPart + g.nnrealPart)) - ↑(Λ ((-f).nnrealPart + (-g).nnrealPart)) =
    ↑(Λ f.nnrealPart) - ↑(Λ (-f).nnrealPart) + (↑(Λ g.nnrealPart) - ↑(Λ (-g).nnrealPart))
Module: Mathlib.MeasureTheory.Integral.Indicator

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
A : Set α
ι : Type u_2
L : Filter ι
inst✝ : L.IsCountablyGenerated
As : ι → Set α
μ : Measure α
A_mble : MeasurableSet A
As_mble : ∀ (i : ι), MeasurableSet (As i)
B : Set α
B_mble : MeasurableSet B
B_finmeas : μ B ≠ ∞
As_le_B : ∀ᶠ (i : ι) in L, As i ⊆ B
h_lim : ∀ᵐ (x : α) ∂μ, ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A
i : ι
⊢ As i ⊆ B → ∀ᵐ (a : α) ∂μ, (As i).indicator 1 a ≤ B.indicator 1 a

Tactic:
hi

Goal state after:
α : Type u_1
inst✝¹ : MeasurableSpace α
A : Set α
ι : Type u_2
L : Filter ι
inst✝ : L.IsCountablyGenerated
As : ι → Set α
μ : Measure α
A_mble : MeasurableSet A
As_mble : ∀ (i : ι), MeasurableSet (As i)
B : Set α
B_mble : MeasurableSet B
B_finmeas : μ B ≠ ∞
As_le_B : ∀ᶠ (i : ι) in L, As i ⊆ B
h_lim : ∀ᵐ (x : α) ∂μ, ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A
i : ι
hi : As i ⊆ B
⊢ ∀ᵐ (a : α) ∂μ, (As i).indicator 1 a ≤ B.indicator 1 a
Module: Mathlib.MeasureTheory.Integral.Indicator

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
A : Set α
ι : Type u_2
L : Filter ι
inst✝ : L.IsCountablyGenerated
As : ι → Set α
μ : Measure α
A_mble : MeasurableSet A
As_mble : ∀ (i : ι), MeasurableSet (As i)
B : Set α
B_mble : MeasurableSet B
B_finmeas : μ B ≠ ∞
As_le_B : ∀ᶠ (i : ι) in L, As i ⊆ B
h_lim : ∀ᵐ (x : α) ∂μ, ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A
i : ι
hi : As i ⊆ B
x : α
⊢ (As i).indicator 1 x ≤ B.indicator 1 x

Tactic:
hi

Goal state after:
α : Type u_1
inst✝¹ : MeasurableSpace α
A : Set α
ι : Type u_2
L : Filter ι
inst✝ : L.IsCountablyGenerated
As : ι → Set α
μ : Measure α
A_mble : MeasurableSet A
As_mble : ∀ (i : ι), MeasurableSet (As i)
B : Set α
B_mble : MeasurableSet B
B_finmeas : μ B ≠ ∞
As_le_B : ∀ᶠ (i : ι) in L, As i ⊆ B
h_lim : ∀ᵐ (x : α) ∂μ, ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A
i : ι
hi : As i ⊆ B
x : α
⊢ B.indicator 1 x ≤ B.indicator 1 x
Module: Mathlib.MeasureTheory.Integral.CurveIntegral.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
a b c : E
t : ℝ
ω : E → E →L[𝕜] F
γab : Path a b
γbc : Path b c
ht₀ : 1 / 2 < t
⊢ -curveIntegralFun ω (γab.trans γbc).symm (1 - t) = 2 • curveIntegralFun ω γbc (2 * t - 1)

Tactic:
Path.trans_symm,

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
a b c : E
t : ℝ
ω : E → E →L[𝕜] F
γab : Path a b
γbc : Path b c
ht₀ : 1 / 2 < t
⊢ -curveIntegralFun ω (γbc.symm.trans γab.symm) (1 - t) = 2 • curveIntegralFun ω γbc (2 * t - 1)
Module: Mathlib.MeasureTheory.Integral.CurveIntegral.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
a b c : E
ω : E → E →L[𝕜] F
γab : Path a b
γbc : Path b c
h₁ : CurveIntegrable ω γab
h₂ : CurveIntegrable ω γbc
instF : NormedSpace ℝ F := NormedSpace.restrictScalars ℝ 𝕜 F
⊢ (∫ (x : ℝ) in 2 * 0..2 * (1 / 2), curveIntegralFun ω γab x) +
      ∫ (x : ℝ) in 2 * (1 / 2) - 1..2 * 1 - 1, curveIntegralFun ω γbc x =
    (∫ (t : ℝ) in 0..1, curveIntegralFun (fun x ↦ ω x) γab t) + ∫ (t : ℝ) in 0..1, curveIntegralFun (fun x ↦ ω x) γbc t

Tactic:
norm_num

Goal state after:
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral

Goal state before:
pp: E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
a b : E
C : ℝ
hfc : ContinuousOn f (segment ℝ a b)
hfd : ∀ t ∈ Ioo 0 1, LineDifferentiableAt ℝ f ((lineMap a b) t) (b - a)
hf' : ∀ᵐ (t : ℝ), t ∈ Ioo 0 1 → ‖lineDeriv ℝ f ((lineMap a b) t) (b - a)‖ ≤ C
⊢ ‖f b - f a‖ ≤ C * volume.real {t | t ∈ Ioo 0 1 ∧ lineDeriv ℝ f ((lineMap a b) t) (b - a) ≠ 0}

Tactic:
set g : ℝ → F := fun t ↦ f (lineMap a b t)
  have hgc : ContinuousOn g (Icc 0 1) := by
    refine hfc.comp ?_ ?_
    · exact AffineMap.lineMap_continuous.continuousOn
    · simp [segment_eq_image_lineMap, mapsTo_image]
  have hdg (t : ℝ) (ht : t ∈ Ioo 0 1) : HasDerivAt g (lineDeriv ℝ f (lineMap a b t) (b - a)) t := by
    have := (hfd t ht).hasLineDerivAt.scomp_of_eq (𝕜 := ℝ) t ((hasDerivAt_id t).sub_const t)
    simpa [g, lineMap_apply_module', Function.comp_def, sub_smul, add_comm _ a] using this
  suffices ‖g 1 - g 0‖ ≤ C * volume.real {t ∈ Ioo 0 1 | deriv g t ≠ 0} by
    convert! this using 1
    · simp [g]
    · congr 2 with t
      simp +contextual [(hdg _ _).deriv]
  apply norm_sub_le_mul_volume_of_norm_deriv_le_of_le zero_le_one hgc
  · exact fun t ht ↦ (hdg t ht).differentiableAt.differentiableWithinAt
  · exact hf'.mono fun t ht ht_mem ↦ by simpa only [(hdg t ht_mem).deriv] using ht ht_mem

Goal state after:
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral

Goal state before:
pp: E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
a b : E
C : ℝ
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hf : DiffContOnCl ℝ f s
hab : openSegment ℝ a b ⊆ s
hC : ∀ x ∈ s, ‖fderiv ℝ f x‖ ≤ C
hmem_s : ∀ t ∈ Ioo 0 1, (lineMap a b) t ∈ s
⊢ 1 / 2 ∈ Ioo 0 1

Tactic:
norm_num

Goal state after:
Module: Mathlib.MeasureTheory.Integral.CurveIntegral.Poincare

Goal state before:
pp: E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace ℝ F
a✝ b✝ c d : E
γ₁ : Path a✝ b✝
γ₂ : Path c d
s : Set (↑I × ↑I)
t : Set E
ω : E → E →L[ℝ] F
dω : E → E →L[ℝ] E →L[ℝ] F
φ : (↑γ₁).Homotopy ↑γ₂
hs : s.Countable
hφt : ∀ a ∈ Ioo 0 1, ∀ b ∈ Ioo 0 1, φ (a, b) ∈ t
hω : ∀ a ∈ Ioo 0 1, ∀ b ∈ Ioo 0 1, (a, b) ∉ s → HasFDerivWithinAt ω (dω (φ (a, b))) t (φ (a, b))
hωc : ContinuousOn ω (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t)
hdω_symm :
  ∀ a ∈ Ioo 0 1,
    ∀ b ∈ Ioo 0 1,
      (a, b) ∉ s →
        ∀ u ∈ tangentConeAt ℝ t (φ (a, b)),
          ∀ v ∈ tangentConeAt ℝ t (φ (a, b)), ((dω (φ (a, b))) u) v = ((dω (φ (a, b))) v) u
U : Set (ℝ × ℝ) := Ioo 0 1 ×ˢ Ioo 0 1
hU : U = Ioo 0 1 ×ˢ Ioo 0 1
hinterior : interior (Icc 0 1) = U
hunique : UniqueDiffOn ℝ (Icc 0 1)
hUopen : IsOpen U
hU_subset : U ⊆ Icc 0 1
hclosure : closure U = Icc 0 1
ψ : ℝ × ℝ → E := fun xy ↦ Set.IccExtend ⋯ (⇑(φ.extend xy.1)) xy.2
hcontdiff : ContDiffOn ℝ 2 ψ (Icc 0 1)
hψ : ψ = fun xy ↦ Set.IccExtend ⋯ (⇑(φ.extend xy.1)) xy.2
hψφ : ∀ (a b : ↑I), ψ (↑a, ↑b) = φ (a, b)
hψ_cont : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ψ
a b : { x // x ∈ I }
ha : (↑a, ↑b).1 ∈ Ioo 0 1
hb : (↑a, ↑b).2 ∈ Ioo 0 1
⊢ ψ (↑a, ↑b) ∈ t

Tactic:
simpa [hψφ] using hφt a ha b hb

Goal state after:
Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
K : Compacts X
V : Set X
hVcp : IsCompact V
hKsubintV : K.carrier ⊆ interior V
⊢ IsCompact (closure (interior V))

Tactic:
apply IsCompact.of_isClosed_subset hVcp isClosed_closure

Goal state after:
X : Type u_1
inst✝² : TopologicalSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
K : Compacts X
V : Set X
hVcp : IsCompact V
hKsubintV : K.carrier ⊆ interior V
⊢ closure (interior V) ⊆ V
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule

Goal state before:
pp: f : ℝ → ℝ
ζ a b : ℝ
a_lt_b : a < b
h_df : DifferentiableOn ℝ f (Set.Icc a b)
h_ddf : DifferentiableOn ℝ (_root_.derivWithin f (Set.Icc a b)) (Set.Icc a b)
fpp_bound : ∀ (x : ℝ), |iteratedDerivWithin 2 f (Set.Icc a b) x| ≤ ζ
g : ℝ → ℝ := fun t ↦ trapezoidal_error f 1 a t
dg : ℝ → ℝ := fun t ↦ 1 / 2 * (f a + f t) + (t - a) / 2 * _root_.derivWithin f (Set.Icc a b) t - f t
ddg : ℝ → ℝ := fun t ↦ (t - a) / 2 * iteratedDerivWithin 2 f (Set.Icc a b) t
h_dg : ∀ y ∈ Set.Icc a b, HasDerivWithinAt g (dg y) (Set.Icc a b) y
h_ddg : ∀ y ∈ Set.Icc a b, HasDerivWithinAt dg (ddg y) (Set.Icc a b) y
x : ℝ
hx : x ∈ Set.Icc a b
⊢ |x - a| / 2 * ζ ≤ ζ / 2 * (x - a)

Tactic:
abs_of_nonneg (sub_nonneg.mpr hx.1),

Goal state after:
f : ℝ → ℝ
ζ a b : ℝ
a_lt_b : a < b
h_df : DifferentiableOn ℝ f (Set.Icc a b)
h_ddf : DifferentiableOn ℝ (_root_.derivWithin f (Set.Icc a b)) (Set.Icc a b)
fpp_bound : ∀ (x : ℝ), |iteratedDerivWithin 2 f (Set.Icc a b) x| ≤ ζ
g : ℝ → ℝ := fun t ↦ trapezoidal_error f 1 a t
dg : ℝ → ℝ := fun t ↦ 1 / 2 * (f a + f t) + (t - a) / 2 * _root_.derivWithin f (Set.Icc a b) t - f t
ddg : ℝ → ℝ := fun t ↦ (t - a) / 2 * iteratedDerivWithin 2 f (Set.Icc a b) t
h_dg : ∀ y ∈ Set.Icc a b, HasDerivWithinAt g (dg y) (Set.Icc a b) y
h_ddg : ∀ y ∈ Set.Icc a b, HasDerivWithinAt dg (ddg y) (Set.Icc a b) y
x : ℝ
hx : x ∈ Set.Icc a b
⊢ (x - a) / 2 * ζ ≤ ζ / 2 * (x - a)
Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real

Goal state before:
pp: X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : T2Space X
inst✝² : MeasurableSpace X
inst✝¹ : BorelSpace X
Λ : (X →C_c ℝ) →ₚ[ℝ] ℝ
inst✝ : LocallyCompactSpace X
f : X →C_c ℝ
hf : ∀ (x : X), 0 ≤ f x
K : Set X
hK : IsCompact K
hfK : ∀ x ∈ K, f x = 1
p : NNReal
hp : Λ f = ↑p
⊢ f.nnrealPart.toReal = f

Tactic:
ext z

Goal state after:
X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : T2Space X
inst✝² : MeasurableSpace X
inst✝¹ : BorelSpace X
Λ : (X →C_c ℝ) →ₚ[ℝ] ℝ
inst✝ : LocallyCompactSpace X
f : X →C_c ℝ
hf : ∀ (x : X), 0 ≤ f x
K : Set X
hK : IsCompact K
hfK : ∀ x ∈ K, f x = 1
p : NNReal
hp : Λ f = ↑p
z : X
⊢ f.nnrealPart.toReal z = f z
Module: Mathlib.MeasureTheory.Integral.TorusIntegral

Goal state before:
pp: n : ℕ
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
𝕜 : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : SMulCommClass 𝕜 ℂ E
a : 𝕜
f : (Fin n → ℂ) → E
c : Fin n → ℂ
R : Fin n → ℝ
⊢ (∯ (x : Fin n → ℂ) in T(c, R), a • f x) = a • ∯ (x : Fin n → ℂ) in T(c, R), f x

Tactic:
simp only [torusIntegral, integral_smul, ← smul_comm a (_ : ℂ) (_ : E)]

Goal state after:
Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
f : X →C_c ℝ
a ε : ℝ
hε : 0 < ε
N : ℕ
hf : range ⇑f ⊆ Ioo a (a + ↑N * ε)
b : ℝ := a + ↑N * ε
y : Fin N → ℝ := fun n ↦ a + ε * (↑↑n + 1)
hy : ∀ {n m : Fin N}, n < m → y n + ε ≤ y m
E : Fin N → Set X := fun n ↦ ⇑f ⁻¹' Ioc (y n - ε) (y n) ∩ tsupport ⇑f
⊢ ∃ E,
    tsupport ⇑f = ⋃ j, E j ∧
      univ.PairwiseDisjoint E ∧
        (∀ (n : Fin N), ∀ x ∈ E n, a + ε * ↑↑n < f x ∧ f x ≤ a + ε * (↑↑n + 1)) ∧ ∀ (n : Fin N), MeasurableSet (E n)

Tactic:
use E

Goal state after:
case h
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
f : X →C_c ℝ
a ε : ℝ
hε : 0 < ε
N : ℕ
hf : range ⇑f ⊆ Ioo a (a + ↑N * ε)
b : ℝ := ⋯
y : Fin N → ℝ := ⋯
hy : ∀ {n m : Fin N}, n < m → y n + ε ≤ y m
E : Fin N → Set X := ⋯
⊢ tsupport ⇑f = ⋃ j, E j ∧
    univ.PairwiseDisjoint E ∧
      (∀ (n : Fin N), ∀ x ∈ E n, a + ε * ↑↑n < f x ∧ f x ≤ a + ε * (↑↑n + 1)) ∧ ∀ (n : Fin N), MeasurableSet (E n)
Module: Mathlib.MeasureTheory.MeasurableSpace.Card

Goal state before:
pp: α : Type u
s : Set (Set α)
i j : Ordinal.{u_1}
h : j < i
t : Set α
ht : t ∈ generateMeasurableRec s j
⊢ tᶜ ∈ generateMeasurableRec s i

Tactic:
by
  unfold generateMeasurableRec
  exact mem_union_left _ (mem_union_right _ ⟨t, mem_iUnion₂.2 ⟨j, h, ht⟩, rfl⟩)

Goal state after:
Module: Mathlib.MeasureTheory.MeasurableSpace.Card

Goal state before:
pp: α : Type u
s : Set (Set α)
i✝¹ i✝ i : Ordinal.{v}
IH : ∀ y < i, y ≤ ω_ 1 → #↑(generateMeasurableRec s y) ≤ max (#↑s) 2 ^ ℵ₀
⊢ i ≤ ω_ 1 → #↑(generateMeasurableRec s i) ≤ max (#↑s) 2 ^ ℵ₀

Tactic:
hi

Goal state after:
α : Type u
s : Set (Set α)
i✝¹ i✝ i : Ordinal.{v}
IH : ∀ y < i, y ≤ ω_ 1 → #↑(generateMeasurableRec s y) ≤ max (#↑s) 2 ^ ℵ₀
hi : i ≤ ω_ 1
⊢ #↑(generateMeasurableRec s i) ≤ max (#↑s) 2 ^ ℵ₀