mathlib-initiative/mathlib-tactics huggingface dataset:
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
⊢ mean μ u F (g • s) ≤ mean μ u F (h • s) + 0

Tactic:
refine le_of_tendsto_of_tendsto
    (hfoel.tendsto_nhds_mean (g • s))
    (hfoel.tendsto_nhds_mean (h • s) |>.add <| hfoel.tendsto_meas_smul_symmDiff_smul g⁻¹ h⁻¹) ?_

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
⊢ (fun i ↦ μ (g • s ∩ F i) / μ (F i)) ≤ᶠ[↑u] fun x ↦ μ (h • s ∩ F x) / μ (F x) + μ ((g⁻¹ • F x) ∆ (h⁻¹ • F x)) / μ (F x)
Module: Mathlib.MeasureTheory.Function.UnifTight

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
hp_top : p ≠ ∞
n : ℕ
h : ∀ {f : Fin n → α → β}, (∀ (i : Fin n), MemLp (f i) p μ) → UnifTight f p μ
f : Fin (n + 1) → α → β
hfLp : ∀ (i : Fin (n + 1)), MemLp (f i) p μ
ε : ℝ≥0
hε : 0 < ε
hε_top : ¬↑ε = ∞
g : Fin n → α → β := fun k ↦ f k.castSucc
hgLp : ∀ (i : Fin n), MemLp (g i) p μ
S : Set α
hμS : μ S ≠ ∞
hFε : ∀ (i : Fin n), eLpNorm (Sᶜ.indicator (g i)) p μ ≤ ↑ε
s : Set α
left✝ : MeasurableSet s
hμs : μ s < ∞
hfε : eLpNorm (sᶜ.indicator (f (Fin.last n))) p μ < ↑ε
hi : n ≤ ↑(Fin.last n)
⊢ eLpNorm (Sᶜ.indicator (sᶜ.indicator (f (Fin.last n)))) p μ ≤ ↑ε

Tactic:
exact (eLpNorm_indicator_le _).trans hfε.le

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

Goal state before:
pp: R r : ℝ
hr : r < R
z : ℂ
⊢ ContinuousOn (fun w ↦ (circleMap z R w.2 - w.1)⁻¹ ^ 2) (closedBall z r ×ˢ univ)

Tactic:
by
  simp_rw [← one_div]
  apply_rules [ContinuousOn.pow, ContinuousOn.div, continuousOn_const]
  · exact ((continuous_circleMap z R).comp_continuousOn continuousOn_snd).sub continuousOn_fst
  · rintro ⟨a, b⟩ ⟨ha, -⟩
    have ha2 : a ∈ ball z R := closedBall_subset_ball hr ha
    exact sub_ne_zero.2 (circleMap_ne_mem_ball ha2 b)

Goal state after:
Module: Mathlib.MeasureTheory.Function.UnifTight

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup β
μ : Measure α
p : ℝ≥0∞
f : ℕ → α → β
g : α → β
hp : 1 ≤ p
hp' : p ≠ ∞
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hg : MemLp g p μ
hui : UnifIntegrable f p μ
hut : UnifTight f p μ
hfg : TendstoInMeasure μ f atTop g
ns : ℕ → ℕ
hns : Tendsto ns atTop atTop
ms : ℕ → ℕ
left✝ : StrictMono ms
hms' : ∀ᵐ (x : α) ∂μ, Tendsto (fun i ↦ f (ns (ms i)) x) atTop (𝓝 (g x))
⊢ ∃ ms, Tendsto (fun n ↦ eLpNorm (f (ns (ms n)) - g) p μ) atTop (𝓝 0)

Tactic:
exact ⟨ms,
    tendsto_Lp_of_tendsto_ae hp hp' (fun _ => hf _) hg
      (fun ε hε => -- `UnifIntegrable` on a subsequence
        let ⟨δ, hδ, hδ'⟩ := hui hε
        ⟨δ, hδ, fun i s hs hμs => hδ' _ s hs hμs⟩)
      (fun ε hε => -- `UnifTight` on a subsequence
        let ⟨s, hμs, hfε⟩ := hut hε
        ⟨s, hμs, fun i => hfε _⟩)
      hms'⟩

Goal state after:
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)
⊢ HasCompactSupport ((↑f).comp ↑g).toFun

Tactic:
apply IsCompact.of_isClosed_subset (g.isCompact_preimage_of_isClosed f.2 (isClosed_tsupport _))
      (isClosed_tsupport (f ∘ g))
    intro x hx
    rw [tsupport, Set.mem_preimage, _root_.mem_closure_iff]
    intro o ho hgxo
    rw [tsupport, _root_.mem_closure_iff] at hx
    obtain ⟨y, hy⟩ := hx (g ⁻¹' o) (IsOpen.preimage g.1.2 ho) hgxo
    exact ⟨g y, hy⟩

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

Goal state before:
pp: p q b : ℝ
hp : 0 < p
hq : -1 < q
hb : 0 < b
x✝ : ℝ
hx : x✝ ∈ Ioi 0
⊢ x✝ ^ q * rexp (-b * x✝ ^ p) = b ^ (-p⁻¹ * q + p⁻¹ * q) * (x✝ ^ q * rexp (-(b * x✝ ^ p)))

pp: case hx
p q b : ℝ
hp : 0 < p
hq : -1 < q
hb : 0 < b
x✝ : ℝ
hx : x✝ ∈ Ioi 0
⊢ 0 < b

pp: p q b : ℝ
hp : 0 < p
hq : -1 < q
hb : 0 < b
x✝ : ℝ
hx : x✝ ∈ Ioi 0
⊢ p ≠ 0

pp: case hx
p q b : ℝ
hp : 0 < p
hq : -1 < q
hb : 0 < b
x✝ : ℝ
hx : x✝ ∈ Ioi 0
⊢ 0 ≤ b

pp: case hx
p q b : ℝ
hp : 0 < p
hq : -1 < q
hb : 0 < b
x✝ : ℝ
hx : x✝ ∈ Ioi 0
⊢ 0 ≤ b

pp: p q b : ℝ
hp : 0 < p
hq : -1 < q
hb : 0 < b
x✝ : ℝ
hx : x✝ ∈ Ioi 0
⊢ 0 ≤ b ^ p⁻¹

pp: p q b : ℝ
hp : 0 < p
hq : -1 < q
hb : 0 < b
x✝ : ℝ
hx : x✝ ∈ Ioi 0
⊢ 0 ≤ b ^ p⁻¹

Tactic:
neg_mul p⁻¹,

Goal state after:
p q b : ℝ
hp : 0 < p
hq : -1 < q
hb : 0 < b
x✝ : ℝ
hx : x✝ ∈ Ioi 0
⊢ x✝ ^ q * rexp (-b * x✝ ^ p) = b ^ (-(p⁻¹ * q) + p⁻¹ * q) * (x✝ ^ q * rexp (-(b * x✝ ^ p)))

case hx
p q b : ℝ
hp : 0 < p
hq : -1 < q
hb : 0 < b
x✝ : ℝ
hx : x✝ ∈ Ioi 0
⊢ 0 < b

p q b : ℝ
hp : 0 < p
hq : -1 < q
hb : 0 < b
x✝ : ℝ
hx : x✝ ∈ Ioi 0
⊢ p ≠ 0

case hx
p q b : ℝ
hp : 0 < p
hq : -1 < q
hb : 0 < b
x✝ : ℝ
hx : x✝ ∈ Ioi 0
⊢ 0 ≤ b

case hx
p q b : ℝ
hp : 0 < p
hq : -1 < q
hb : 0 < b
x✝ : ℝ
hx : x✝ ∈ Ioi 0
⊢ 0 ≤ b

p q b : ℝ
hp : 0 < p
hq : -1 < q
hb : 0 < b
x✝ : ℝ
hx : x✝ ∈ Ioi 0
⊢ 0 ≤ b ^ p⁻¹

p q b : ℝ
hp : 0 < p
hq : -1 < q
hb : 0 < b
x✝ : ℝ
hx : x✝ ∈ Ioi 0
⊢ 0 ≤ b ^ p⁻¹
Module: Mathlib.Topology.ContinuousMap.CompactlySupported

Goal state before:
pp: case inl
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : TopologicalSpace α
Λ : (α →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
a : ℝ
f : α →C_c ℝ
ha : 0 ≤ a
⊢ ↑(Λ (a • f).nnrealPart) - ↑(Λ (a • -f).nnrealPart) = a * (↑(Λ f.nnrealPart) - ↑(Λ (-f).nnrealPart))

Tactic:
nnrealPart_smul_pos f ha,

Goal state after:
case inl
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : TopologicalSpace α
Λ : (α →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
a : ℝ
f : α →C_c ℝ
ha : 0 ≤ a
⊢ ↑(Λ (a.toNNReal • f.nnrealPart)) - ↑(Λ (a • -f).nnrealPart) = a * (↑(Λ f.nnrealPart) - ↑(Λ (-f).nnrealPart))
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 : E
ω : E → E →L[𝕜] F
γ : Path a b
h : CurveIntegrable ω γ
⊢ CurveIntegrable ω γ.symm

Tactic:
by
  simpa [CurveIntegrable] using! (h.comp_sub_left 1).neg.symm

Goal state after:
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
inst✝ : NormedSpace ℝ E
ω : E → E →L[𝕜] F
a b : E
t : ℝ
ht : t ∈ I
⊢ curveIntegralFun ω (Path.segment a b) t = (ω ((lineMap a b) t)) (b - a)

Tactic:
have := Path.eqOn_extend_segment a b

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
inst✝ : NormedSpace ℝ E
ω : E → E →L[𝕜] F
a b : E
t : ℝ
ht : t ∈ I
this : EqOn ⇑(Path.segment a b).extend ⇑(lineMap a b) I
⊢ curveIntegralFun ω (Path.segment a b) t = (ω ((lineMap a b) t)) (b - a)
Module: Mathlib.MeasureTheory.Integral.MeanValue

Goal state before:
pp: α : 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 : g =ᵐ[μ.restrict s] 0
hν0 : ∫ (x : α) in s, 1 ∂ν = 0
c : α
hc : c ∈ s
heq_zero : ∫ (x : α) in s, f x * g x ∂μ = 0
⊢ ∫ (x : α) in s, f x ∂ν = 0

Tactic:
rw [← heq, heq_zero]

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

Goal state before:
pp: α : 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
c : α
hc : c ∈ s
⊢ ∫ (x : α) in s, f x ∂ν = 0

Tactic:
rw [hν0, setIntegral_eq_zero_iff_of_nonneg_ae hg0 hg] at hg1
        have heq_zero : ∫ x in s, f x * g x ∂μ = 0 := by
          have heq_ae : (fun x ↦ f x * g x) =ᵐ[μ.restrict s] 0 := by
            apply hg1.mono
            intro x hx
            simp [hx]
          simpa using! integral_congr_ae heq_ae
        rw [← heq, heq_zero]

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

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

Tactic:
intro k

Goal state after:
case e_a.e_a
f : ℝ → ℝ
N : ℕ
N_nonzero : 0 < N
a b : ℝ
k : ℕ
⊢ k ∈ Finset.range (N - 1) → f (a + (↑(N - 1 - 1 - k) + 1) * (b - a) / ↑N) = f (b + (↑k + 1) * (a - b) / ↑N)
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule

Goal state before:
pp: f : ℝ → ℝ
N : ℕ
a h : ℝ
N_nonzero : 0 < N
h_f_int : IntervalIntegrable f volume a (a + ↑N * h)
⊢ ∀ k < N, IntervalIntegrable f volume (a + ↑k * h) (a + ↑(k + 1) * h)

Tactic:
intro k

Goal state after:
f : ℝ → ℝ
N : ℕ
a h : ℝ
N_nonzero : 0 < N
h_f_int : IntervalIntegrable f volume a (a + ↑N * h)
k : ℕ
⊢ k < N → IntervalIntegrable f volume (a + ↑k * h) (a + ↑(k + 1) * h)
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule

Goal state before:
pp: case inl
f : ℝ → ℝ
N : ℕ
a h : ℝ
N_nonzero : 0 < N
h_f_int : IntervalIntegrable f volume a (a + ↑N * h)
k : ℕ
hk : k < N
h_neg : h ≤ 0
⊢ ∀ {k : ℕ}, k ≤ N → a + ↑k * h ∈ [[a, a + ↑N * h]]

Tactic:
intro k

Goal state after:
case inl
f : ℝ → ℝ
N : ℕ
a h : ℝ
N_nonzero : 0 < N
h_f_int : IntervalIntegrable f volume a (a + ↑N * h)
k✝ : ℕ
hk : k✝ < N
h_neg : h ≤ 0
k : ℕ
⊢ k ≤ N → a + ↑k * h ∈ [[a, a + ↑N * h]]
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule

Goal state before:
pp: case inr
f : ℝ → ℝ
N : ℕ
a h : ℝ
N_nonzero : 0 < N
h_f_int : IntervalIntegrable f volume a (a + ↑N * h)
k : ℕ
hk : k < N
h_pos : 0 ≤ h
⊢ ∀ {k : ℕ}, k ≤ N → a + ↑k * h ∈ [[a, a + ↑N * h]]

Tactic:
intro k

Goal state after:
case inr
f : ℝ → ℝ
N : ℕ
a h : ℝ
N_nonzero : 0 < N
h_f_int : IntervalIntegrable f volume a (a + ↑N * h)
k✝ : ℕ
hk : k✝ < N
h_pos : 0 ≤ h
k : ℕ
⊢ k ≤ N → a + ↑k * h ∈ [[a, a + ↑N * h]]
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
⊢ |trapezoidal_error f 1 a b| ≤ ζ / 12 * (b - a) ^ 3

Tactic:
let ddg (t : ℝ) := ((t - a) / 2) * (iteratedDerivWithin 2 f (Icc a b) t)

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
⊢ |trapezoidal_error f 1 a b| ≤ ζ / 12 * (b - a) ^ 3
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| ≤ ζ
N : ℕ
N_nonzero : 0 < N
h : ℝ := (b - a) / ↑N
ak : ℕ → ℝ := fun k ↦ a + ↑k * h
h0 : ∀ (k : ℕ), ak (k + 1) - ak k = h
hab : 0 < b - a
hpos : 0 < h
hb : b = a + ↑N * h
⊢ ∀ k ∈ Finset.range N, |trapezoidal_error f 1 (ak k) (ak (k + 1))| ≤ ζ / 12 * h ^ 3

Tactic:
intro k

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| ≤ ζ
N : ℕ
N_nonzero : 0 < N
h : ℝ := (b - a) / ↑N
ak : ℕ → ℝ := fun k ↦ a + ↑k * h
h0 : ∀ (k : ℕ), ak (k + 1) - ak k = h
hab : 0 < b - a
hpos : 0 < h
hb : b = a + ↑N * h
k : ℕ
⊢ k ∈ Finset.range N → |trapezoidal_error f 1 (ak k) (ak (k + 1))| ≤ ζ / 12 * h ^ 3
Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic

Goal state before:
pp: case neg
X : Type u_1
inst✝² : TopologicalSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
K₁ K₂ : Compacts X
disj : Disjoint ↑K₁ ↑K₂
b : ℝ≥0
f : X →C_c ℝ≥0
hf : f ∈ {f | ∀ x ∈ K₁ ⊔ K₂, 1 ≤ f x}
Λf_eq_b : Λ f = b
hsuppf : ∀ x ∈ K₁ ⊔ K₂, x ∈ support ⇑f
hsubsuppf : ↑K₁ ∪ ↑K₂ ⊆ tsupport ⇑f
g₁ g₂ : X →C_c ℝ≥0
hg₁ : EqOn (⇑g₁) 1 K₁.carrier
hg₂ : EqOn (⇑g₂) 1 K₂.carrier
sum_g : EqOn (⇑(g₁ + g₂)) 1 (tsupport f.toFun)
x : X
h : ¬f x = 0
⊢ ↑(f x) = ↑((⇑g₁ + ⇑g₂) x) * ↑(f x)

Tactic:
· simp only [CompactlySupportedContinuousMap.coe_add, ContinuousMap.toFun_eq_coe,
        CompactlySupportedContinuousMap.coe_toContinuousMap] at sum_g
      rw [sum_g (mem_of_subset_of_mem subset_closure (mem_support.mpr h))]
      simp only [Pi.one_apply, NNReal.coe_one, one_mul]

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
b : ℝ≥0∞
hb : ∀ (i : Compacts X), b ≤ ⨅ (_ : ↑K ⊆ interior ↑i), ↑(rieszContentAux Λ i)
this : b < ∞
ε : ℝ≥0
hε : 0 < ↑ε
⊢ ↑b.toNNReal ≤ ↑(sInf (⇑Λ '' {f | ∀ x ∈ K, 1 ≤ f x})) + ↑ε

Tactic:
obtain ⟨f, hfleoneonK, hfle⟩ := exists_lt_rieszContentAux_add_pos Λ K (Real.toNNReal_pos.mpr hε)

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
b : ℝ≥0∞
hb : ∀ (i : Compacts X), b ≤ ⨅ (_ : ↑K ⊆ interior ↑i), ↑(rieszContentAux Λ i)
this : b < ∞
ε : ℝ≥0
hε : 0 < ↑ε
f : X →C_c ℝ≥0
hfleoneonK : ∀ x ∈ K, 1 ≤ f x
hfle : Λ f < rieszContentAux Λ K + (↑ε).toNNReal
⊢ ↑b.toNNReal ≤ ↑(sInf (⇑Λ '' {f | ∀ x ∈ K, 1 ≤ f x})) + ↑ε
Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic

Goal state before:
pp: case neg
X : Type u_1
inst✝⁴ : TopologicalSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
inst✝³ : T2Space X
inst✝² : LocallyCompactSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
f : X →C_c ℝ≥0
hf : ∀ (x : X), f x ≤ 1
K : Set X
hK : IsCompact K
h : tsupport ⇑f ⊆ K
ε : ℝ≥0
hε : 0 < ε
g : X →C_c ℝ≥0
hg :
  (∀ x ∈ { carrier := K, isCompact' := hK }, 1 ≤ g x) ∧ Λ g < rieszContentAux Λ { carrier := K, isCompact' := hK } + ε
x : X
hx : x ∉ tsupport ⇑f
⊢ f x ≤ g x

Tactic:
· rw [image_eq_zero_of_notMem_tsupport hx]
    exact zero_le

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

Goal state before:
pp: X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : T2Space X
inst✝² : LocallyCompactSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
f : X →C_c ℝ≥0
⊢ ∫⁻ (x : X), ↑(f x) ∂rieszMeasure Λ = ↑(Λ f)

Tactic:
rw [lintegral_coe_eq_integral, ← ENNReal.ofNNReal_toNNReal]

Goal state after:
X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : T2Space X
inst✝² : LocallyCompactSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
f : X →C_c ℝ≥0
⊢ ↑(∫ (a : X), ↑(f a) ∂rieszMeasure Λ).toNNReal = ↑(Λ f)

case hfi
X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : T2Space X
inst✝² : LocallyCompactSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
f : X →C_c ℝ≥0
⊢ Integrable (fun x ↦ ↑(f x)) (rieszMeasure Λ)
Module: Mathlib.MeasureTheory.MeasurableSpace.Card

Goal state before:
pp: α : Type u
s : Set (Set α)
i : Ordinal.{u_1}
t : Set α
p : Set α → Prop
hs : ∀ t ∈ s, p t
h0 : p ∅
hc : ∀ (u : Set α), p u → (∃ j < i, u ∈ generateMeasurableRec s j) → p uᶜ
hn : ∀ (f : ℕ → Set α), (∀ (n : ℕ), p (f n) ∧ ∃ j < i, f n ∈ generateMeasurableRec s j) → p (⋃ n, f n)
⊢ ∀ k ≤ i, ∀ t ∈ generateMeasurableRec s k, p t

Tactic:
intro k

Goal state after:
α : Type u
s : Set (Set α)
i : Ordinal.{u_1}
t : Set α
p : Set α → Prop
hs : ∀ t ∈ s, p t
h0 : p ∅
hc : ∀ (u : Set α), p u → (∃ j < i, u ∈ generateMeasurableRec s j) → p uᶜ
hn : ∀ (f : ℕ → Set α), (∀ (n : ℕ), p (f n) ∧ ∃ j < i, f n ∈ generateMeasurableRec s j) → p (⋃ n, f n)
k : Ordinal.{u_1}
⊢ k ≤ i → ∀ t ∈ generateMeasurableRec s k, p t
Module: Mathlib.MeasureTheory.MeasurableSpace.Card

Goal state before:
pp: α : Type u
s : Set (Set α)
i : Ordinal.{u_1}
t : Set α
p : Set α → Prop
hs : ∀ t ∈ s, p t
h0 : p ∅
hc : ∀ (u : Set α), p u → (∃ j < i, u ∈ generateMeasurableRec s j) → p uᶜ
hn : ∀ (f : ℕ → Set α), (∀ (n : ℕ), p (f n) ∧ ∃ j < i, f n ∈ generateMeasurableRec s j) → p (⋃ n, f n)
k : Ordinal.{u_1}
⊢ ∀ (x : Ordinal.{u_1}),
    (∀ y < x, y ≤ i → ∀ t ∈ generateMeasurableRec s y, p t) → x ≤ i → ∀ t ∈ generateMeasurableRec s x, p t

Tactic:
intro k

Goal state after:
α : Type u
s : Set (Set α)
i : Ordinal.{u_1}
t : Set α
p : Set α → Prop
hs : ∀ t ∈ s, p t
h0 : p ∅
hc : ∀ (u : Set α), p u → (∃ j < i, u ∈ generateMeasurableRec s j) → p uᶜ
hn : ∀ (f : ℕ → Set α), (∀ (n : ℕ), p (f n) ∧ ∃ j < i, f n ∈ generateMeasurableRec s j) → p (⋃ n, f n)
k✝ k : Ordinal.{u_1}
⊢ (∀ y < k, y ≤ i → ∀ t ∈ generateMeasurableRec s y, p t) → k ≤ i → ∀ t ∈ generateMeasurableRec s k, p t
Module: Mathlib.MeasureTheory.Measure.FiniteMeasureExt

Goal state before:
pp: E : Type u_1
𝕜 : Type u_2
inst✝⁷ : RCLike 𝕜
inst✝⁶ : MeasurableSpace E
inst✝⁵ : PseudoEMetricSpace E
inst✝⁴ : BorelSpace E
inst✝³ : CompleteSpace E
inst✝² : SecondCountableTopology E
P P' : Measure E
inst✝¹ : IsFiniteMeasure P
inst✝ : IsFiniteMeasure P'
A : StarSubalgebra 𝕜 (E →ᵇ 𝕜)
hA : (StarSubalgebra.map (toContinuousMapStarₐ 𝕜) A).SeparatesPoints
heq : ∀ g ∈ A, ∫ (x : E), g x ∂P = ∫ (x : E), g x ∂P'
A_toReal : Subalgebra ℝ (E →ᵇ ℝ) :=
  Subalgebra.comap (AlgHom.compLeftContinuousBounded ℝ ofRealAm ⋯) (Subalgebra.restrictScalars ℝ A.toSubalgebra)
⊢ (Subalgebra.map (toContinuousMapₐ ℝ) A_toReal).SeparatesPoints

Tactic:
rw [RCLike.restrict_toContinuousMap_eq_toContinuousMapStar_restrict]

Goal state after:
E : Type u_1
𝕜 : Type u_2
inst✝⁷ : RCLike 𝕜
inst✝⁶ : MeasurableSpace E
inst✝⁵ : PseudoEMetricSpace E
inst✝⁴ : BorelSpace E
inst✝³ : CompleteSpace E
inst✝² : SecondCountableTopology E
P P' : Measure E
inst✝¹ : IsFiniteMeasure P
inst✝ : IsFiniteMeasure P'
A : StarSubalgebra 𝕜 (E →ᵇ 𝕜)
hA : (StarSubalgebra.map (toContinuousMapStarₐ 𝕜) A).SeparatesPoints
heq : ∀ g ∈ A, ∫ (x : E), g x ∂P = ∫ (x : E), g x ∂P'
A_toReal : Subalgebra ℝ (E →ᵇ ℝ) :=
  Subalgebra.comap (AlgHom.compLeftContinuousBounded ℝ ofRealAm ⋯) (Subalgebra.restrictScalars ℝ A.toSubalgebra)
⊢ (Subalgebra.comap (AlgHom.compLeftContinuous ℝ ofRealAm ⋯)
      (Subalgebra.restrictScalars ℝ (StarSubalgebra.map (toContinuousMapStarₐ 𝕜) A).toSubalgebra)).SeparatesPoints
Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : SecondCountableTopology E
μ : Measure E
inst✝ : IsFiniteMeasure μ
n : ℕ
t : E
hint : MemLp id (↑n) μ
x : Fin n → E
h : innerₗ E = ContinuousLinearMap.toLinearMap₁₂ (innerSL ℝ)
hint' : ∀ (k : ℕ), ↑k ≤ ↑n → Integrable (fun x ↦ ‖x‖ ^ k * ‖1 x‖) μ
⊢ ((-(Real.pi⁻¹ * 2⁻¹)) ^ n •
        iteratedFDeriv ℝ n (fourierIntegral Real.fourierChar μ (innerₗ E) 1) (-((Real.pi⁻¹ * 2⁻¹) • t)))
      x =
    I ^ n * ∫ (y : E), ↑(∏ i, ⟪y, x i⟫) * cexp (↑⟪y, t⟫ * I) ∂μ

Tactic:
h,

Goal state after:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : SecondCountableTopology E
μ : Measure E
inst✝ : IsFiniteMeasure μ
n : ℕ
t : E
hint : MemLp id (↑n) μ
x : Fin n → E
h : innerₗ E = ContinuousLinearMap.toLinearMap₁₂ (innerSL ℝ)
hint' : ∀ (k : ℕ), ↑k ≤ ↑n → Integrable (fun x ↦ ‖x‖ ^ k * ‖1 x‖) μ
⊢ ((-(Real.pi⁻¹ * 2⁻¹)) ^ n •
        iteratedFDeriv ℝ n (fourierIntegral Real.fourierChar μ (ContinuousLinearMap.toLinearMap₁₂ (innerSL ℝ)) 1)
          (-((Real.pi⁻¹ * 2⁻¹) • t)))
      x =
    I ^ n * ∫ (y : E), ↑(∏ i, ⟪y, x i⟫) * cexp (↑⟪y, t⟫ * I) ∂μ
Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic

Goal state before:
pp: E : Type u_4
F : Type u_5
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedAddCommGroup F
inst✝¹⁰ : InnerProductSpace ℝ E
inst✝⁹ : InnerProductSpace ℝ F
mE : MeasurableSpace E
mF : MeasurableSpace F
inst✝⁸ : CompleteSpace E
inst✝⁷ : CompleteSpace F
inst✝⁶ : SecondCountableTopology E
inst✝⁵ : SecondCountableTopology F
inst✝⁴ : BorelSpace E
inst✝³ : BorelSpace F
μ : Measure E
ν : Measure F
ξ : Measure (E × F)
inst✝² : IsFiniteMeasure μ
inst✝¹ : IsFiniteMeasure ν
inst✝ : IsFiniteMeasure ξ
h : ∀ (t : WithLp 2 (E × F)), charFun (Measure.map (toLp 2) ξ) t = charFun μ t.ofLp.1 * charFun ν t.ofLp.2
t : WithLp 2 (E × F)
⊢ charFun (Measure.map (toLp 2) ξ) t = charFun (Measure.map (toLp 2) (μ.prod ν)) t

Tactic:
h,

Goal state after:
E : Type u_4
F : Type u_5
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedAddCommGroup F
inst✝¹⁰ : InnerProductSpace ℝ E
inst✝⁹ : InnerProductSpace ℝ F
mE : MeasurableSpace E
mF : MeasurableSpace F
inst✝⁸ : CompleteSpace E
inst✝⁷ : CompleteSpace F
inst✝⁶ : SecondCountableTopology E
inst✝⁵ : SecondCountableTopology F
inst✝⁴ : BorelSpace E
inst✝³ : BorelSpace F
μ : Measure E
ν : Measure F
ξ : Measure (E × F)
inst✝² : IsFiniteMeasure μ
inst✝¹ : IsFiniteMeasure ν
inst✝ : IsFiniteMeasure ξ
h : ∀ (t : WithLp 2 (E × F)), charFun (Measure.map (toLp 2) ξ) t = charFun μ t.ofLp.1 * charFun ν t.ofLp.2
t : WithLp 2 (E × F)
⊢ charFun μ t.ofLp.1 * charFun ν t.ofLp.2 = charFun (Measure.map (toLp 2) (μ.prod ν)) t
Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic

Goal state before:
pp: ι : Type u_6
inst✝⁷ : Fintype ι
E : ι → Type u_7
inst✝⁶ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁵ : (i : ι) → InnerProductSpace ℝ (E i)
mE : (i : ι) → MeasurableSpace (E i)
inst✝⁴ : ∀ (i : ι), CompleteSpace (E i)
inst✝³ : ∀ (i : ι), SecondCountableTopology (E i)
inst✝² : ∀ (i : ι), BorelSpace (E i)
μ : (i : ι) → Measure (E i)
ν : Measure ((i : ι) → E i)
inst✝¹ : ∀ (i : ι), IsFiniteMeasure (μ i)
inst✝ : IsFiniteMeasure ν
h : ∀ (t : WithLp 2 ((i : ι) → E i)), charFun (Measure.map (toLp 2) ν) t = ∏ i, charFun (μ i) (t.ofLp i)
t : WithLp 2 ((i : ι) → E i)
⊢ charFun (Measure.map (toLp 2) ν) t = charFun (Measure.map (toLp 2) (Measure.pi μ)) t

Tactic:
h,

Goal state after:
ι : Type u_6
inst✝⁷ : Fintype ι
E : ι → Type u_7
inst✝⁶ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁵ : (i : ι) → InnerProductSpace ℝ (E i)
mE : (i : ι) → MeasurableSpace (E i)
inst✝⁴ : ∀ (i : ι), CompleteSpace (E i)
inst✝³ : ∀ (i : ι), SecondCountableTopology (E i)
inst✝² : ∀ (i : ι), BorelSpace (E i)
μ : (i : ι) → Measure (E i)
ν : Measure ((i : ι) → E i)
inst✝¹ : ∀ (i : ι), IsFiniteMeasure (μ i)
inst✝ : IsFiniteMeasure ν
h : ∀ (t : WithLp 2 ((i : ι) → E i)), charFun (Measure.map (toLp 2) ν) t = ∏ i, charFun (μ i) (t.ofLp i)
t : WithLp 2 ((i : ι) → E i)
⊢ ∏ i, charFun (μ i) (t.ofLp i) = charFun (Measure.map (toLp 2) (Measure.pi μ)) t