mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Probability.Process.Filtration

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝ : PartialOrder ι
𝓕 : Filtration ι m
this : TopologicalSpace ι := Preorder.topology ι
i j : ι
hij : i ≤ j
⊢ (fun i ↦ if (𝓝[>] i).NeBot then ⨅ j, ⨅ (_ : j > i), ↑𝓕 j else ↑𝓕 i) i ≤
    (fun i ↦ if (𝓝[>] i).NeBot then ⨅ j, ⨅ (_ : j > i), ↑𝓕 j else ↑𝓕 i) j

Tactic:
simp only [gt_iff_lt]
      split_ifs with hi hj hj
      · exact le_iInf₂ fun k hkj ↦ iInf₂_le k (hij.trans_lt hkj)
      · obtain rfl | hj := eq_or_ne j i
        · contradiction
        · exact iInf₂_le j (lt_of_le_of_ne hij hj.symm)
      · exact le_iInf₂ fun k hk ↦ 𝓕.mono (hij.trans hk.le)
      · exact 𝓕.mono hij

Goal state after:
Module: Mathlib.Probability.Process.Filtration

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝ : PartialOrder ι
𝓕 : Filtration ι m
this✝ : TopologicalSpace ι := Preorder.topology ι
this : OrderTopology ι
i : ι
hne : (𝓝[>] i).NeBot
u : ι
hu : u > i
hiou : Set.Ioo i u ∈ 𝓝[>] i
v : ι
hv : v ∈ Set.Ioo i u
⊢ ⨅ j, ⨅ (_ : j > i), ↑𝓕₊ j ≤ ↑𝓕 u

Tactic:
have hle₁ : (⨅ j > i, 𝓕₊ j) ≤ 𝓕₊ v := iInf₂_le_of_le v hv.1 le_rfl

Goal state after:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝ : PartialOrder ι
𝓕 : Filtration ι m
this✝ : TopologicalSpace ι := Preorder.topology ι
this : OrderTopology ι
i : ι
hne : (𝓝[>] i).NeBot
u : ι
hu : u > i
hiou : Set.Ioo i u ∈ 𝓝[>] i
v : ι
hv : v ∈ Set.Ioo i u
hle₁ : ⨅ j, ⨅ (_ : j > i), ↑𝓕₊ j ≤ ↑𝓕₊ v
⊢ ⨅ j, ⨅ (_ : j > i), ↑𝓕₊ j ≤ ↑𝓕 u
Module: Mathlib.Probability.Process.Filtration

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
β : ι → Type u_3
inst✝³ : (i : ι) → TopologicalSpace (β i)
inst✝² : ∀ (i : ι), MetrizableSpace (β i)
mβ : (i : ι) → MeasurableSpace (β i)
inst✝¹ : ∀ (i : ι), BorelSpace (β i)
inst✝ : Preorder ι
u : (i : ι) → Ω → β i
hum : ∀ (i : ι), StronglyMeasurable (u i)
i : ι
⊢ ⨆ j, ⨆ (_ : j ≤ i), MeasurableSpace.comap (u j) (mβ j) = ⨆ a, MeasurableSpace.comap (u ↑a) inferInstance

Tactic:
iSup_subtype'

Goal state after:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
β : ι → Type u_3
inst✝³ : (i : ι) → TopologicalSpace (β i)
inst✝² : ∀ (i : ι), MetrizableSpace (β i)
mβ : (i : ι) → MeasurableSpace (β i)
inst✝¹ : ∀ (i : ι), BorelSpace (β i)
inst✝ : Preorder ι
u : (i : ι) → Ω → β i
hum : ∀ (i : ι), StronglyMeasurable (u i)
i : ι
⊢ ⨆ x, MeasurableSpace.comap (u ↑x) (mβ ↑x) = ⨆ a, MeasurableSpace.comap (u ↑a) inferInstance
Module: Mathlib.MeasureTheory.Function.Intersectivity

Goal state before:
pp: α : Type u_2
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
r : ℝ≥0∞
s : ℕ → Set α
hs : ∀ (n : ℕ), MeasurableSet (s n)
hr₀ : r ≠ 0
hr : ∀ (n : ℕ), r ≤ μ (s n)
M : (α → ℝ) → Set α := fun f ↦ {x | eLpNormEssSup f μ < ↑‖f x‖₊}
N : Set α := ⋃ u, M ((⋂ n ∈ u, s n).indicator 1)
hN₀ : μ N = 0
hN₁ : ∀ (u : Finset ℕ), ((⋂ n ∈ u, s n) \ N).Nonempty → 0 < μ (⋂ n ∈ u, s n)
f : ℕ → α → ℝ≥0∞ := fun n ↦ (↑(n + 1))⁻¹ • ∑ k ∈ Finset.range (n + 1), (s k).indicator 1
hfapp : ∀ (n : ℕ) (a : α), f n a = (↑(n + 1))⁻¹ * ∑ k ∈ Finset.range (n + 1), (s k).indicator 1 a
hf : ∀ (n : ℕ), Measurable (f n)
hf₁ : ∀ (n : ℕ), f n ≤ 1
n : ℕ
⊢ r ≤ (↑(n + 1))⁻¹ * ∫⁻ (a : α), ∑ i ∈ Finset.range (n + 1), (s i).indicator 1 a ∂μ

Tactic:
lintegral_finsetSum _ fun _ _ ↦ measurable_one.indicator (hs _)

Goal state after:
α : Type u_2
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
r : ℝ≥0∞
s : ℕ → Set α
hs : ∀ (n : ℕ), MeasurableSet (s n)
hr₀ : r ≠ 0
hr : ∀ (n : ℕ), r ≤ μ (s n)
M : (α → ℝ) → Set α := fun f ↦ {x | eLpNormEssSup f μ < ↑‖f x‖₊}
N : Set α := ⋃ u, M ((⋂ n ∈ u, s n).indicator 1)
hN₀ : μ N = 0
hN₁ : ∀ (u : Finset ℕ), ((⋂ n ∈ u, s n) \ N).Nonempty → 0 < μ (⋂ n ∈ u, s n)
f : ℕ → α → ℝ≥0∞ := fun n ↦ (↑(n + 1))⁻¹ • ∑ k ∈ Finset.range (n + 1), (s k).indicator 1
hfapp : ∀ (n : ℕ) (a : α), f n a = (↑(n + 1))⁻¹ * ∑ k ∈ Finset.range (n + 1), (s k).indicator 1 a
hf : ∀ (n : ℕ), Measurable (f n)
hf₁ : ∀ (n : ℕ), f n ≤ 1
n : ℕ
⊢ r ≤ (↑(n + 1))⁻¹ * ∑ b ∈ Finset.range (n + 1), ∫⁻ (a : α), (s b).indicator 1 a ∂μ
Module: Mathlib.MeasureTheory.Function.Intersectivity

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : IsFiniteMeasure μ
r : ℝ≥0∞
inst✝ : Infinite ι
s : ι → Set α
hs : ∀ (i : ι), MeasurableSet (s i)
hr₀ : r ≠ 0
hr : ∀ (i : ι), r ≤ μ (s i)
⊢ ∃ t, t.Infinite ∧ ∀ ⦃u : Set ι⦄, u ⊆ t → u.Finite → 0 < μ (⋂ i ∈ u, s i)

Tactic:
by
  obtain ⟨t, ht, h⟩ := bergelson' (fun n ↦ hs <| Infinite.natEmbedding _ n) hr₀ (fun n ↦ hr _)
  refine ⟨_, ht.image <| (Infinite.natEmbedding _).injective.injOn, fun u hut hu ↦
    (h (preimage_subset_of_surjOn (Infinite.natEmbedding _).injective hut) <| hu.preimage
    (Embedding.injective _).injOn).trans_le <| measure_mono <| subset_iInter₂ fun i hi ↦ ?_⟩
  obtain ⟨n, -, rfl⟩ := hut hi
  exact iInter₂_subset n hi

Goal state after:
Module: Mathlib.Topology.ContinuousMap.CompactlySupported

Goal state before:
pp: α : Type u_2
inst✝ : TopologicalSpace α
f : α →C_c ℝ
a : ℝ
ha : 0 ≤ a
x : α
⊢ ↑((a • f).nnrealPart x) = ↑((a.toNNReal • f.nnrealPart) x)

Tactic:
simp only [nnrealPart_apply, coe_smul, Pi.smul_apply, Real.coe_toNNReal', smul_eq_mul,
    NNReal.coe_mul, ha, sup_of_le_left]

Goal state after:
α : Type u_2
inst✝ : TopologicalSpace α
f : α →C_c ℝ
a : ℝ
ha : 0 ≤ a
x : α
⊢ max (a * f x) 0 = a * max (f x) 0
Module: Mathlib.MeasureTheory.Integral.Gamma

Goal state before:
pp: p q b : ℝ
hp : 0 < p
hq : -1 < q
hb : 0 < b
⊢ (b ^ p⁻¹)⁻¹ • ∫ (x : ℝ) in Ioi (b ^ p⁻¹ * 0), b ^ (-p⁻¹ * q) * (x ^ q * rexp (-x ^ p)) =
    (b ^ p⁻¹)⁻¹ * ∫ (x : ℝ) in Ioi 0, b ^ (-p⁻¹ * q) * (x ^ q * rexp (-x ^ p))

pp: p q b : ℝ
hp : 0 < p
hq : -1 < q
hb : 0 < b
⊢ 0 < b ^ p⁻¹

Tactic:
mul_zero,

Goal state after:
p q b : ℝ
hp : 0 < p
hq : -1 < q
hb : 0 < b
⊢ (b ^ p⁻¹)⁻¹ • ∫ (x : ℝ) in Ioi 0, b ^ (-p⁻¹ * q) * (x ^ q * rexp (-x ^ p)) =
    (b ^ p⁻¹)⁻¹ * ∫ (x : ℝ) in Ioi 0, b ^ (-p⁻¹ * q) * (x ^ q * rexp (-x ^ p))

p q b : ℝ
hp : 0 < p
hq : -1 < q
hb : 0 < b
⊢ 0 < b ^ p⁻¹
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 : t < 1 / 2
instE : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
H₁ : ⇑(γab.trans γbc).extend =ᶠ[𝓝 t] fun s ↦ γab.extend (2 * s)
⊢ Icc (2 * 0) (2 * 1) =ᶠ[𝓝 (2 * t)] I

Tactic:
mul_zero,

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 : t < 1 / 2
instE : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
H₁ : ⇑(γab.trans γbc).extend =ᶠ[𝓝 t] fun s ↦ γab.extend (2 * s)
⊢ Icc 0 (2 * 1) =ᶠ[𝓝 (2 * t)] I
Module: Mathlib.MeasureTheory.Integral.CurveIntegral.Basic

Goal state before:
pp: case inl
𝕜 : 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 : t < 1 / 2
instE : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
H₁ : ⇑(γab.trans γbc).extend =ᶠ[𝓝 t] fun s ↦ γab.extend (2 * s)
ht₀ : t < 0
⊢ 𝓝[Icc 0 2] (2 * t) = 𝓝[I] (2 * t)

pp: case inr.inl
𝕜 : 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
instE : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
ht : 0 < 1 / 2
H₁ : ⇑(γab.trans γbc).extend =ᶠ[𝓝 0] fun s ↦ γab.extend (2 * s)
⊢ 𝓝[Icc 0 2] (2 * 0) = 𝓝[I] (2 * 0)

pp: case inr.inr
𝕜 : 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 : t < 1 / 2
instE : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
H₁ : ⇑(γab.trans γbc).extend =ᶠ[𝓝 t] fun s ↦ γab.extend (2 * s)
ht₀ : 0 < t
⊢ 𝓝[Icc 0 2] (2 * t) = 𝓝[I] (2 * t)

Tactic:
· rw [notMem_closure_iff_nhdsWithin_eq_bot.mp, notMem_closure_iff_nhdsWithin_eq_bot.mp] <;>
        simp_intro h <;> linarith

Goal state after:
case inr.inl
𝕜 : 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
instE : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
ht : 0 < 1 / 2
H₁ : ⇑(γab.trans γbc).extend =ᶠ[𝓝 0] fun s ↦ γab.extend (2 * s)
⊢ 𝓝[Icc 0 2] (2 * 0) = 𝓝[I] (2 * 0)

case inr.inr
𝕜 : 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 : t < 1 / 2
instE : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
H₁ : ⇑(γab.trans γbc).extend =ᶠ[𝓝 t] fun s ↦ γab.extend (2 * s)
ht₀ : 0 < t
⊢ 𝓝[Icc 0 2] (2 * t) = 𝓝[I] (2 * t)
Module: Mathlib.MeasureTheory.Integral.MeanValue

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
s : Set α
f g : α → ℝ
μ : Measure α
hs_conn : IsConnected s
hs_meas : MeasurableSet s
hf : ContinuousOn f s
hg : IntegrableOn g s μ
hfg : IntegrableOn (fun x ↦ f x * g x) s μ
hg0 : ∀ᵐ (x : α) ∂μ.restrict s, 0 ≤ g x
ρ : α → ENNReal := fun x ↦ ENNReal.ofReal (g x)
ν : Measure α := μ.withDensity ρ
hρ_ae : AEMeasurable ρ (μ.restrict s)
hρ_top : ∀ᵐ (x : α) ∂μ.restrict s, ρ x < ⊤
h_toReal_ae : (fun x ↦ (ρ x).toReal) =ᵐ[μ.restrict s] g
heq : ∫ (x : α) in s, f x * g x ∂μ = ∫ (x : α) in s, f x ∂ν
hg1 : ∫ (x : α) in s, g x ∂μ = ∫ (x : α) in s, 1 ∂ν
hν0 : ¬∫ (x : α) in s, 1 ∂ν = 0
hν0' : (ν s).toReal ≠ 0
hνfin : ν s ≠ ⊤
hν0'' : ν s ≠ 0
hint : IntegrableOn f s ν
c : α
hc : c ∈ s
h_ave : f c = ⨍ (x : α) in s, f x ∂ν
⊢ ∫ (x : α) in s, f x * g x ∂μ = f c * ∫ (x : α) in s, g x ∂μ

Tactic:
calc
      _ = ∫ x in s, f x ∂ν := heq
      _ = f c * ∫ x in s, (1 : ℝ) ∂ν := by
        rw [h_ave]
        simp only [setAverage_eq, smul_eq_mul, integral_const, MeasurableSet.univ,
          measureReal_restrict_apply, Set.univ_inter, mul_one]
        rw [measureReal_def]
        field_simp
      _ = _ := by simp [hg1]

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

Goal state before:
pp: case neg.inr
a b : ℝ
f g : ℝ → ℝ
μ : Measure ℝ
hf : ContinuousOn f [[a, b]]
hg : IntervalIntegrable g μ a b
hg0 : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), 0 ≤ g x
h : ¬a = b
this :
  ∀ {a b : ℝ},
    ContinuousOn f [[a, b]] →
      IntervalIntegrable g μ a b →
        (∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), 0 ≤ g x) →
          ¬a = b → a < b → ∃ c ∈ [[a, b]], ∫ (x : ℝ) in a..b, f x * g x ∂μ = f c * ∫ (x : ℝ) in a..b, g x ∂μ
hab : ¬a < b
⊢ ∃ c ∈ [[a, b]], ∫ (x : ℝ) in a..b, f x * g x ∂μ = f c * ∫ (x : ℝ) in a..b, g x ∂μ

Tactic:
simp only [not_lt] at hab

Goal state after:
case neg.inr
a b : ℝ
f g : ℝ → ℝ
μ : Measure ℝ
hf : ContinuousOn f [[a, b]]
hg : IntervalIntegrable g μ a b
hg0 : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), 0 ≤ g x
h : ¬a = b
this :
  ∀ {a b : ℝ},
    ContinuousOn f [[a, b]] →
      IntervalIntegrable g μ a b →
        (∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), 0 ≤ g x) →
          ¬a = b → a < b → ∃ c ∈ [[a, b]], ∫ (x : ℝ) in a..b, f x * g x ∂μ = f c * ∫ (x : ℝ) in a..b, g x ∂μ
hab : b ≤ a
⊢ ∃ c ∈ [[a, b]], ∫ (x : ℝ) in a..b, f x * g x ∂μ = f c * ∫ (x : ℝ) in a..b, g x ∂μ
Module: Mathlib.MeasureTheory.Integral.Regular

Goal state before:
pp: case a
X : Type u_1
inst✝⁶ : TopologicalSpace X
inst✝⁵ : MeasurableSpace X
inst✝⁴ : BorelSpace X
k : Set X
hk : IsCompact k
μ : Measure X
inst✝³ : IsFiniteMeasureOnCompacts μ
inst✝² : μ.InnerRegularCompactLTTop
inst✝¹ : LocallyCompactSpace X
inst✝ : RegularSpace X
f : X → ℝ
f_cont : Continuous f
⊢ HasCompactSupport f → EqOn f 1 k → 0 ≤ f → μ k ≤ ENNReal.ofReal (∫ (x : X), f x ∂μ)

Tactic:
f_comp

Goal state after:
case a
X : Type u_1
inst✝⁶ : TopologicalSpace X
inst✝⁵ : MeasurableSpace X
inst✝⁴ : BorelSpace X
k : Set X
hk : IsCompact k
μ : Measure X
inst✝³ : IsFiniteMeasureOnCompacts μ
inst✝² : μ.InnerRegularCompactLTTop
inst✝¹ : LocallyCompactSpace X
inst✝ : RegularSpace X
f : X → ℝ
f_cont : Continuous f
f_comp : HasCompactSupport f
⊢ EqOn f 1 k → 0 ≤ f → μ k ≤ ENNReal.ofReal (∫ (x : X), f x ∂μ)
Module: Mathlib.MeasureTheory.Integral.Regular

Goal state before:
pp: case hs
X : Type u_1
inst✝⁶ : TopologicalSpace X
inst✝⁵ : MeasurableSpace X
inst✝⁴ : BorelSpace X
inst✝³ : T2Space X
U : Set X
hU : IsOpen U
μ : Measure X
inst✝² : IsFiniteMeasure μ
inst✝¹ : μ.InnerRegularCompactLTTop
inst✝ : NormalSpace X
r : ENNReal
hr : r < μ U
K : Set X
KU : K ⊆ U
K_comp : IsCompact K
hK : r < μ K
f : X → ℝ
f_cont : Continuous f
fU : EqOn (⇑{ toFun := f, continuous_toFun := f_cont }) 0 Uᶜ
fK : EqOn (⇑{ toFun := f, continuous_toFun := f_cont }) 1 K
f_range : ∀ (x : X), { toFun := f, continuous_toFun := f_cont } x ∈ Icc 0 1
⊢ ∀ x ∈ K, 1 ≤ f x

Tactic:
intro x hx
      apply Eq.ge
      exact fK hx

Goal state after:
Module: Mathlib.Order.Interval.Set.Union

Goal state before:
pp: case succ
X : Type u_1
inst✝ : LinearOrder X
a : ℕ → X
N : ℕ
ih : Ioc (a 0) (a N) ⊆ ⋃ i ∈ Finset.range N, Ioc (a i) (a (i + 1))
⊢ Ioc (a 0) (a (N + 1)) ⊆ ⋃ i ∈ Finset.range (N + 1), Ioc (a i) (a (i + 1))

Tactic:
calc
    _ ⊆ Ioc (a 0) (a N) ∪ Ioc (a N) (a (N + 1)) := Ioc_subset_Ioc_union_Ioc
    _ ⊆ _ := by simpa [Finset.range_add_one] using
                  union_subset_union_right (Ioc (a N) (a (N + 1))) ih

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

Goal state before:
pp: f : ℝ → ℝ
N : ℕ
a h : ℝ
N_nonzero : 0 < N
⊢ h / 2 *
      (f (a + ↑0 * h) + f (a + (↑(N - 1) + 1) * h) +
        ∑ x ∈ Finset.range (N - 1), (f (a + ↑(x + 1) * h) + f (a + (↑x + 1) * h))) =
    h * ((f a + f (a + ↑N * h)) / 2 + ∑ x ∈ Finset.range (N - 1), f (a + (↑x + 1) * h))

Tactic:
simp_rw [Nat.cast_sub N_nonzero, Nat.cast_add, Nat.cast_one, ← two_mul, ← mul_sum]

Goal state after:
f : ℝ → ℝ
N : ℕ
a h : ℝ
N_nonzero : 0 < N
⊢ h / 2 * (f (a + ↑0 * h) + f (a + (↑N - 1 + 1) * h) + 2 * ∑ i ∈ Finset.range (N - 1), f (a + (↑i + 1) * h)) =
    h * ((f a + f (a + ↑N * h)) / 2 + ∑ x ∈ Finset.range (N - 1), f (a + (↑x + 1) * h))
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)
n m : Fin N
h : n < m
⊢ a + ε * ↑↑m + ε = a + ε * (↑↑m + 1)

Tactic:
mul_add,

Goal state after:
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)
n m : Fin N
h : n < m
⊢ a + ε * ↑↑m + ε = a + (ε * ↑↑m + ε * 1)
Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝ : IsProbabilityMeasure P
X : Ω → ℝ
hX : AEMeasurable X P
h0 : ∫ (x : Ω), X x ∂P = 0
h1 : ∫ (x : Ω), (X ^ 2) x ∂P = 1
⊢ (fun t ↦ charFun (Measure.map X P) t - (1 - ↑t ^ 2 / 2)) =o[𝓝 0] fun t ↦ t ^ 2

Tactic:
simp_rw [← taylorWithinEval_charFun_two_zero' (by fun_prop) h0 h1]

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝ : IsProbabilityMeasure P
X : Ω → ℝ
hX : AEMeasurable X P
h0 : ∫ (x : Ω), X x ∂P = 0
h1 : ∫ (x : Ω), (X ^ 2) x ∂P = 1
⊢ (fun t ↦ charFun (Measure.map X P) t - taylorWithinEval (charFun (Measure.map X P)) 2 univ 0 t) =o[𝓝 0] fun t ↦ t ^ 2
Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic

Goal state before:
pp: case refine_2
E : Type u_3
inst✝⁷ : MeasurableSpace E
μ ν : Measure E
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace ℝ E
inst✝⁴ : BorelSpace E
inst✝³ : SecondCountableTopology E
inst✝² : CompleteSpace E
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h : ∀ (x : E), ∫ (v : E), (innerProbChar x) v ∂μ = ∫ (v : E), (innerProbChar x) v ∂ν
⊢ Continuous fun p ↦ ((innerₗ E) p.1) p.2

Tactic:
· exact continuous_inner

Goal state after:
Module: Mathlib.Topology.Separation.CompletelyRegular

Goal state before:
pp: X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : NormalSpace X
inst✝ : R0Space X
⊢ CompletelyRegularSpace X

Tactic:
by
  rw [completelyRegularSpace_iff]
  intro x K hK hx
  have cx : IsClosed (closure {x}) := isClosed_closure
  have d : Disjoint (closure {x}) K := by
    rw [Set.disjoint_iff]
    intro a ⟨hax, haK⟩
    exact hx ((specializes_iff_mem_closure.mpr hax).symm.mem_closed hK haK)
  let ⟨⟨f, cf⟩, hfx, hfK, hficc⟩ := exists_continuous_zero_one_of_isClosed cx hK d
  let g : X → I := fun x => ⟨f x, hficc x⟩
  have cg : Continuous g := cf.subtype_mk hficc
  have hgx : g x = 0 := Subtype.ext (hfx (subset_closure (mem_singleton x)))
  have hgK : EqOn g 1 K := fun k hk => Subtype.ext (hfK hk)
  exact ⟨g, cg, hgx, hgK⟩

Goal state after:
Module: Mathlib.Topology.Separation.CompletelyRegular

Goal state before:
pp: ι : Type u_1
X : Type u_2
t : ι → TopologicalSpace X
ht : ∀ (i : ι), CompletelyRegularSpace X
this : TopologicalSpace X := ⨅ i, t i
x✝ : X
I' : Finset ι
V U : ↥I' → Set X
hUV : ∀ (i : ↥I'), U i ⊆ V i
fs : ↥I' → X → ↑I
hfs : ∀ (i : ↥I'), Continuous[t ↑i, _] (fs i)
hxfs : ∀ (i : ↥I'), fs i x✝ = 0
hfsU : ∀ (i : ↥I') ⦃x : X⦄, x ∈ (U i)ᶜ → fs i x = ⊤
x : X
i : ↥I'
hxi : x ∈ (V i)ᶜ
⊢ ?m.318 ∈ (U i)ᶜ

Tactic:
tauto_set

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

Goal state before:
pp: case calc_5
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 ℝ
μ : Measure X := rieszMeasure Λ
K : Set X := tsupport ⇑f
ε : ℝ
hε : 0 < ε
a b : ℝ
hab : a < b ∧ range ⇑f ⊆ Ioo a b
N : ℕ
hN : 0 < N
ε' : ℝ := (b - a) / ↑N
hε' : 0 < ε' ∧ ε' * (2 * μ.real K + |a| + b + ε') ≤ ε
E : Fin N → Set X
hE :
  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)
y : Fin N → ℝ := fun n ↦ a + ε' * (↑↑n + 1)
hE' : ∀ (n : Fin N), μ (E n) ≠ ∞
V : Fin N → Opens X
hV : ∀ (n : Fin N), E n ⊆ ↑(V n) ∧ (∀ x ∈ V n, f x < y n + ε') ∧ μ ↑(V n) ≤ μ (E n) + ENNReal.ofReal (ε' / ↑N)
g : Fin N → X →C_c ℝ
hg :
  (∀ (n : Fin N), tsupport ⇑(g n) ⊆ (V n).carrier) ∧
    EqOn (∑ n, ⇑(g n)) 1 (tsupport f.toFun) ∧
      (∀ (n : Fin N) (x : X), (g n) x ∈ Icc 0 1) ∧ ∀ (n : Fin N), HasCompactSupport ⇑(g n)
this : ∀ (n : Fin N), (|a| + y n + ε') * μ.real (E n) = (|a| + 2 * ε') * μ.real (E n) + (y n - ε') * μ.real (E n)
⊢ ∑ n, (|a| + y n + ε') * (μ.real (E n) + ε' / ↑N) - |a| * μ.real K =
    ∑ n, (y n - ε') * μ.real (E n) + 2 * ε' * μ.real K + ε' / ↑N * ∑ n, (|a| + y n + ε')

Tactic:
mul_add,

Goal state after:
case calc_5
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 ℝ
μ : Measure X := rieszMeasure Λ
K : Set X := tsupport ⇑f
ε : ℝ
hε : 0 < ε
a b : ℝ
hab : a < b ∧ range ⇑f ⊆ Ioo a b
N : ℕ
hN : 0 < N
ε' : ℝ := (b - a) / ↑N
hε' : 0 < ε' ∧ ε' * (2 * μ.real K + |a| + b + ε') ≤ ε
E : Fin N → Set X
hE :
  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)
y : Fin N → ℝ := fun n ↦ a + ε' * (↑↑n + 1)
hE' : ∀ (n : Fin N), μ (E n) ≠ ∞
V : Fin N → Opens X
hV : ∀ (n : Fin N), E n ⊆ ↑(V n) ∧ (∀ x ∈ V n, f x < y n + ε') ∧ μ ↑(V n) ≤ μ (E n) + ENNReal.ofReal (ε' / ↑N)
g : Fin N → X →C_c ℝ
hg :
  (∀ (n : Fin N), tsupport ⇑(g n) ⊆ (V n).carrier) ∧
    EqOn (∑ n, ⇑(g n)) 1 (tsupport f.toFun) ∧
      (∀ (n : Fin N) (x : X), (g n) x ∈ Icc 0 1) ∧ ∀ (n : Fin N), HasCompactSupport ⇑(g n)
this : ∀ (n : Fin N), (|a| + y n + ε') * μ.real (E n) = (|a| + 2 * ε') * μ.real (E n) + (y n - ε') * μ.real (E n)
⊢ ∑ x, ((|a| + y x + ε') * μ.real (E x) + (|a| + y x + ε') * (ε' / ↑N)) - |a| * μ.real K =
    ∑ n, (y n - ε') * μ.real (E n) + 2 * ε' * μ.real K + ε' / ↑N * ∑ n, (|a| + y n + ε')
Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic

Goal state before:
pp: E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
mE : MeasurableSpace E
inst✝⁴ : BorelSpace E
inst✝³ : SecondCountableTopology E
inst✝² : CompleteSpace E
μ ν : Measure E
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h : charFunDual μ = charFunDual ν
⊢ μ = ν

Tactic:
refine ext_of_integral_char_eq continuous_probChar probChar_ne_one
    ?_ ?_ (fun L ↦ funext_iff.mp h L)
  · exact fun v hv ↦ DFunLike.ne_iff.mpr <| SeparatingDual.exists_ne_zero hv
  · exact isBoundedBilinearMap_apply.symm.continuous

Goal state after:
Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric

Goal state before:
pp: case refine_1
Ω : Type u_1
inst✝³ : MeasurableSpace Ω
inst✝² : PseudoEMetricSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
inst✝ : BorelSpace Ω
μ ν : LevyProkhorov (ProbabilityMeasure Ω)
h : dist μ ν = 0
⊢ inst✝³ = MeasurableSpace.generateFrom {s | IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s}

Tactic:
rw [BorelSpace.measurable_eq (α := Ω), borel_eq_generateFrom_isClosed]

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

Goal state before:

Tactic:
rieszMeasure Λ univ
  _ ≤ ENNReal.ofReal (Λ o) :=
    rieszMeasure_le_of_eq_one _ (fun x ↦ zero_le_one) isCompact_univ (fun x hx ↦ rfl)
  _ < ⊤ := by simp

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Haar.DistribChar

Goal state before:
pp: G : Type u_1
A : Type u_2
inst✝¹⁰ : Group G
inst✝⁹ : AddCommGroup A
inst✝⁸ : DistribMulAction G A
inst✝⁷ : TopologicalSpace A
inst✝⁶ : IsTopologicalAddGroup A
inst✝⁵ : LocallyCompactSpace A
inst✝⁴ : ContinuousConstSMul G A
inst✝³ : MeasurableSpace A
inst✝² : BorelSpace A
μ : Measure A
inst✝¹ : μ.IsAddHaarMeasure
inst✝ : μ.Regular
s : Set A
hs₀ : μ s ≠ 0
hs : μ s ≠ ∞
g : G
⊢ ↑((distribHaarChar A) g) = ↑((distribHaarChar A) g) * μ s / μ s

Tactic:
ENNReal.mul_div_cancel_right

Goal state after:
G : Type u_1
A : Type u_2
inst✝¹⁰ : Group G
inst✝⁹ : AddCommGroup A
inst✝⁸ : DistribMulAction G A
inst✝⁷ : TopologicalSpace A
inst✝⁶ : IsTopologicalAddGroup A
inst✝⁵ : LocallyCompactSpace A
inst✝⁴ : ContinuousConstSMul G A
inst✝³ : MeasurableSpace A
inst✝² : BorelSpace A
μ : Measure A
inst✝¹ : μ.IsAddHaarMeasure
inst✝ : μ.Regular
s : Set A
hs₀ : μ s ≠ 0
hs : μ s ≠ ∞
g : G
⊢ ↑((distribHaarChar A) g) = ↑((distribHaarChar A) g)

case hb₀
G : Type u_1
A : Type u_2
inst✝¹⁰ : Group G
inst✝⁹ : AddCommGroup A
inst✝⁸ : DistribMulAction G A
inst✝⁷ : TopologicalSpace A
inst✝⁶ : IsTopologicalAddGroup A
inst✝⁵ : LocallyCompactSpace A
inst✝⁴ : ContinuousConstSMul G A
inst✝³ : MeasurableSpace A
inst✝² : BorelSpace A
μ : Measure A
inst✝¹ : μ.IsAddHaarMeasure
inst✝ : μ.Regular
s : Set A
hs₀ : μ s ≠ 0
hs : μ s ≠ ∞
g : G
⊢ μ s ≠ 0

case hb
G : Type u_1
A : Type u_2
inst✝¹⁰ : Group G
inst✝⁹ : AddCommGroup A
inst✝⁸ : DistribMulAction G A
inst✝⁷ : TopologicalSpace A
inst✝⁶ : IsTopologicalAddGroup A
inst✝⁵ : LocallyCompactSpace A
inst✝⁴ : ContinuousConstSMul G A
inst✝³ : MeasurableSpace A
inst✝² : BorelSpace A
μ : Measure A
inst✝¹ : μ.IsAddHaarMeasure
inst✝ : μ.Regular
s : Set A
hs₀ : μ s ≠ 0
hs : μ s ≠ ∞
g : G
⊢ μ s ≠ ∞