mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Measure.Portmanteau

Goal state before:
pp: Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : SecondCountableTopology Ω
S : Set (Set Ω)
ν : ProbabilityMeasure Ω
h : ∀ (u : Set Ω), IsOpen[inst✝¹] u → ∀ x ∈ u, ∃ s ∈ S, s ∈ 𝓝 x ∧ s ⊆ u
G : Set Ω
hG : IsOpen[inst✝¹] G
r : ℝ≥0
hr : r < ν G
s : ↑G → Set Ω
hsS : ∀ (x : ↑G), s x ∈ S
hs_nhds : ∀ (x : ↑G), s x ∈ 𝓝 ↑x
hsG : ∀ (x : ↑G), s x ⊆ G
T₀ : Set ↑G
T₀_count : T₀.Countable
hT₀ : ⋃ i ∈ T₀, interior (s i) = ⋃ i, interior (s i)
⊢ G ⊆ ⋃ i, interior (s i)

Tactic:
intro y hy

Goal state after:
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : SecondCountableTopology Ω
S : Set (Set Ω)
ν : ProbabilityMeasure Ω
h : ∀ (u : Set Ω), IsOpen[inst✝¹] u → ∀ x ∈ u, ∃ s ∈ S, s ∈ 𝓝 x ∧ s ⊆ u
G : Set Ω
hG : IsOpen[inst✝¹] G
r : ℝ≥0
hr : r < ν G
s : ↑G → Set Ω
hsS : ∀ (x : ↑G), s x ∈ S
hs_nhds : ∀ (x : ↑G), s x ∈ 𝓝 ↑x
hsG : ∀ (x : ↑G), s x ⊆ G
T₀ : Set ↑G
T₀_count : T₀.Countable
hT₀ : ⋃ i ∈ T₀, interior (s i) = ⋃ i, interior (s i)
y : Ω
hy : y ∈ G
⊢ y ∈ ⋃ i, interior (s i)
Module: Mathlib.Probability.Moments.Covariance

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
hY : Integrable Y μ
c : ℝ
⊢ cov[X, fun ω ↦ Y ω - c; μ] = cov[X, Y; μ]

Tactic:
by
  simp [sub_eq_add_neg, hY]

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

Goal state before:
pp: case inr
ι : Type u_1
E : Type u_2
Ω' : Type u_3
Ω'' : Type u_4
m' : MeasurableSpace Ω'
μ' : Measure Ω'
inst✝⁵ : IsProbabilityMeasure μ'
m'' : MeasurableSpace Ω''
μ'' : Measure Ω''
inst✝⁴ : IsProbabilityMeasure μ''
mE : MeasurableSpace E
l : Filter ι
inst✝³ : SeminormedAddCommGroup E
inst✝² : SecondCountableTopology E
inst✝¹ : BorelSpace E
X : ι → Ω'' → E
inst✝ : l.IsCountablyGenerated
Y : ι → Ω'' → E
Z : Ω' → E
hXZ : TendstoInDistribution X l Z (fun x ↦ μ'') μ'
hXY : TendstoInMeasure μ'' (Y - X) l 0
hY : ∀ (i : ι), AEMeasurable (Y i) μ''
hZ : AEMeasurable Z μ'
hX : ∀ (i : ι), AEMeasurable (X i) μ''
hE : Nonempty E
x₀ : E := hE.some
⊢ Tendsto (fun n ↦ ⟨Measure.map (Y n) μ'', ⋯⟩) l (𝓝 ⟨Measure.map Z μ', ⋯⟩)

Tactic:
suffices ∀ (F : E → ℝ) (hF_bounded : ∃ (C : ℝ), ∀ x y, dist (F x) (F y) ≤ C)
      (hF_lip : ∃ L, LipschitzWith L F),
      Tendsto (fun n ↦ ∫ ω, F ω ∂(μ''.map (Y n))) l (𝓝 (∫ ω, F ω ∂(μ'.map Z))) by
    rwa [tendsto_iff_forall_lipschitz_integral_tendsto]

Goal state after:
case inr
ι : Type u_1
E : Type u_2
Ω' : Type u_3
Ω'' : Type u_4
m' : MeasurableSpace Ω'
μ' : Measure Ω'
inst✝⁵ : IsProbabilityMeasure μ'
m'' : MeasurableSpace Ω''
μ'' : Measure Ω''
inst✝⁴ : IsProbabilityMeasure μ''
mE : MeasurableSpace E
l : Filter ι
inst✝³ : SeminormedAddCommGroup E
inst✝² : SecondCountableTopology E
inst✝¹ : BorelSpace E
X : ι → Ω'' → E
inst✝ : l.IsCountablyGenerated
Y : ι → Ω'' → E
Z : Ω' → E
hXZ : TendstoInDistribution X l Z (fun x ↦ μ'') μ'
hXY : TendstoInMeasure μ'' (Y - X) l 0
hY : ∀ (i : ι), AEMeasurable (Y i) μ''
hZ : AEMeasurable Z μ'
hX : ∀ (i : ι), AEMeasurable (X i) μ''
hE : Nonempty E
x₀ : E := hE.some
⊢ ∀ (F : E → ℝ),
    (∃ C, ∀ (x y : E), dist (F x) (F y) ≤ C) →
      (∃ L, LipschitzWith L F) →
        Tendsto (fun n ↦ ∫ (ω : E), F ω ∂Measure.map (Y n) μ'') l (𝓝 (∫ (ω : E), F ω ∂Measure.map Z μ'))
Module: Mathlib.MeasureTheory.Function.UnifTight

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : ι → α → β
p : ℝ≥0∞
hf : UnifTight f p μ
ε : ℝ≥0∞
hε : ε ≠ 0
⊢ ∀ᶠ (s : Set α) in μ.cofinite.smallSets, ∀ (i : ι), eLpNorm (s.indicator (f i)) p μ ≤ ε

Tactic:
by
  by_cases hε_top : ε = ∞
  · subst hε_top; simp
  rcases hf (pos_iff_ne_zero.2 (toNNReal_ne_zero.mpr ⟨hε,hε_top⟩)) with ⟨s, hμs, hfs⟩
  refine (eventually_smallSets' ?_).2 ⟨sᶜ, ?_, fun i ↦ (coe_toNNReal hε_top) ▸ hfs i⟩
  · intro s t hst ht i
    exact (eLpNorm_mono <| norm_indicator_le_of_subset hst _).trans (ht i)
  · rwa [Measure.compl_mem_cofinite, lt_top_iff_ne_top]

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) ∂ν) / ∫ (x : G), f x ∂ν = (∫ (x : G), f (x * g) ∂ν.haarScalarFactor μ • μ) / ∫ (x : G), f x ∂ν

Tactic:
rw [t]

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
⊢ (ν.haarScalarFactor μ • ∫ (x : G), f (x * g) ∂μ) / ∫ (x : G), f x ∂ν.haarScalarFactor μ • μ =
    (ν.haarScalarFactor μ • ∫ (x : G), f (x * g) ∂μ) / ν.haarScalarFactor μ • ∫ (x : G), f x ∂μ

Tactic:
integral_smul_nnreal_measure

Goal state after:
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
⊢ (ν.haarScalarFactor μ • ∫ (x : G), f (x * g) ∂μ) / ν.haarScalarFactor μ • ∫ (x : G), f x ∂μ =
    (ν.haarScalarFactor μ • ∫ (x : G), f (x * g) ∂μ) / ν.haarScalarFactor μ • ∫ (x : G), f x ∂μ
Module: Mathlib.MeasureTheory.Group.GeometryOfNumbers

Goal state before:
pp: case bc
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✝³ : Nontrivial E
inst✝² : μ.IsAddHaarMeasure
L : AddSubgroup E
inst✝¹ : Countable ↥L
inst✝ : DiscreteTopology ↥L
fund : IsAddFundamentalDomain (↥L) F μ
h_symm : ∀ x ∈ s, -x ∈ s
h_conv : Convex ℝ s
h_cpt : IsCompact s
h : μ F * 2 ^ finrank ℝ E ≤ μ s
h_mes : μ s ≠ 0
h_nemp : s.Nonempty
u : ℕ → ℝ≥0 := ⋯
K : ConvexBody E := ⋯
S : ℕ → ConvexBody E := ⋯
Z : ℕ → Set E := ⋯
h_zero : 0 ∈ K
h_clos : IsClosed (↑L \ {0})
n : ℕ
⊢ 1 < ENNReal.ofReal ((1 + ↑(u n)) ^ finrank ℝ E)

Tactic:
ofReal_pow (by positivity)

Goal state after:
case bc
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✝³ : Nontrivial E
inst✝² : μ.IsAddHaarMeasure
L : AddSubgroup E
inst✝¹ : Countable ↥L
inst✝ : DiscreteTopology ↥L
fund : IsAddFundamentalDomain (↥L) F μ
h_symm : ∀ x ∈ s, -x ∈ s
h_conv : Convex ℝ s
h_cpt : IsCompact s
h : μ F * 2 ^ finrank ℝ E ≤ μ s
h_mes : μ s ≠ 0
h_nemp : s.Nonempty
u : ℕ → ℝ≥0 := ⋯.choose
K : ConvexBody E := { carrier := s, convex' := h_conv, isCompact' := h_cpt, nonempty' := h_nemp }
S : ℕ → ConvexBody E := fun n ↦ (1 + u n) • K
Z : ℕ → Set E := fun n ↦ ↑(S n) ∩ (↑L \ {0})
h_zero : 0 ∈ K
h_clos : IsClosed (↑L \ {0})
n : ℕ
⊢ 1 < ENNReal.ofReal (1 + ↑(u n)) ^ finrank ℝ E
Module: Mathlib.MeasureTheory.Integral.Indicator

Goal state before:
pp: case refine_2
α : 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
⊢ ∀ᶠ (n : ι) in L, ∀ᵐ (a : α) ∂μ, (As n).indicator 1 a ≤ B.indicator 1 a

pp: case refine_3
α : 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
⊢ ∫⁻ (a : α), B.indicator 1 a ∂μ ≠ ∞

pp: case refine_4
α : 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
⊢ ∀ᵐ (a : α) ∂μ, Tendsto (fun n ↦ (As n).indicator 1 a) L (𝓝 (A.indicator 1 a))

Tactic:
· filter_upwards [As_le_B] with i hi
    exact Eventually.of_forall fun x ↦ by grw [hi]

Goal state after:
case refine_3
α : 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
⊢ ∫⁻ (a : α), B.indicator 1 a ∂μ ≠ ∞

case refine_4
α : 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
⊢ ∀ᵐ (a : α) ∂μ, Tendsto (fun n ↦ (As n).indicator 1 a) L (𝓝 (A.indicator 1 a))
Module: Mathlib.MeasureTheory.Integral.Indicator

Goal state before:
pp: case refine_3
α : 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
⊢ ∫⁻ (a : α), B.indicator 1 a ∂μ ≠ ∞

Tactic:
← lintegral_indicator_one B_mble

Goal state after:
case refine_3
α : 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 : ∫⁻ (a : α), B.indicator 1 a ∂μ ≠ ∞
As_le_B : ∀ᶠ (i : ι) in L, As i ⊆ B
h_lim : ∀ᵐ (x : α) ∂μ, ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A
⊢ ∫⁻ (a : α), B.indicator 1 a ∂μ ≠ ∞
Module: Mathlib.MeasureTheory.Integral.Gamma

Goal state before:
pp: case e_a
p q : ℝ
hp : 1 ≤ p
hq : -2 < q
x : ℝ
hx : x ∈ Ioi 0
⊢ x * |x| ^ q * rexp (-|x| ^ p) = x ^ (q + 1) * rexp (-x ^ p)

Tactic:
mem_Ioi

Goal state after:
case e_a
p q : ℝ
hp : 1 ≤ p
hq : -2 < q
x : ℝ
hx : 0 < x
⊢ x * |x| ^ q * rexp (-|x| ^ p) = x ^ (q + 1) * rexp (-x ^ p)
Module: Mathlib.MeasureTheory.Integral.Gamma

Goal state before:
pp: case e_a
p q b : ℝ
hp : 1 ≤ p
hq : -2 < q
hb : 0 < b
x : ℝ
hx : x ∈ Ioi 0
⊢ x * |x| ^ q * rexp (-b * |x| ^ p) = x ^ (q + 1) * rexp (-b * x ^ p)

Tactic:
mem_Ioi

Goal state after:
case e_a
p q b : ℝ
hp : 1 ≤ p
hq : -2 < q
hb : 0 < b
x : ℝ
hx : 0 < x
⊢ x * |x| ^ q * rexp (-b * |x| ^ p) = x ^ (q + 1) * rexp (-b * x ^ 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
ω : E → E →L[𝕜] F
γbc : Path b c
γab : Path a b
h : CurveIntegrable ω γbc
⊢ IntervalIntegrable (curveIntegralFun ω (γab.trans γbc)) volume (1 / 2) 1

Tactic:
refine .congr_ae ?_ (curveIntegralFun_trans_aeeq_right _ _ _).symm
  simpa [ofNat_smul_eq_nsmul] using! h.comp_sub_right 1 |>.comp_mul_left (c := 2) |>.smul (2 : 𝕜)

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 ∂ν
⊢ ∃ c ∈ s, ∫ (x : α) in s, f x * g x ∂μ = f c * ∫ (x : α) in s, g x ∂μ

Tactic:
by_cases hν0 : ∫ x in s, (1 : ℝ) ∂ν = 0

Goal state after:
case pos
α : 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 ∈ s, ∫ (x : α) in s, f x * g x ∂μ = f c * ∫ (x : α) in s, g x ∂μ

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
⊢ ∃ c ∈ s, ∫ (x : α) in s, f x * g x ∂μ = f c * ∫ (x : α) in s, g x ∂μ
Module: Mathlib.MeasureTheory.Integral.LebesgueNormedSpace

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : SecondCountableTopology E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : Measurable g'
hg' : (fun x ↦ ↑(f x) • g x) =ᵐ[μ] g'
x : α
hx : ↑(f x) • g x = g' x
h'x : ↑(f x) ≠ 0
⊢ g x = (↑(f x))⁻¹ • g' x

Tactic:
← hx,

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : SecondCountableTopology E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : Measurable g'
hg' : (fun x ↦ ↑(f x) • g x) =ᵐ[μ] g'
x : α
hx : ↑(f x) • g x = g' x
h'x : ↑(f x) ≠ 0
⊢ g x = (↑(f x))⁻¹ • ↑(f x) • g x
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
K1 K2 : Compacts X
ε : ℝ≥0
εpos : 0 < ε
f1 : X →C_c ℝ≥0
f_test_function_K1 : (∀ x ∈ K1, 1 ≤ f1 x) ∧ Λ f1 < rieszContentAux Λ K1 + ε / 2
f2 : X →C_c ℝ≥0
f_test_function_K2 : (∀ x ∈ K2, 1 ≤ f2 x) ∧ Λ f2 < rieszContentAux Λ K2 + ε / 2
f_test_function_union : ∀ x ∈ K1 ⊔ K2, 1 ≤ (f1 + f2) x
⊢ Λ (f1 + f2) < rieszContentAux Λ K1 + rieszContentAux Λ K2 + ε

Tactic:
rw [map_add]

Goal state after:
X : Type u_1
inst✝² : TopologicalSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
K1 K2 : Compacts X
ε : ℝ≥0
εpos : 0 < ε
f1 : X →C_c ℝ≥0
f_test_function_K1 : (∀ x ∈ K1, 1 ≤ f1 x) ∧ Λ f1 < rieszContentAux Λ K1 + ε / 2
f2 : X →C_c ℝ≥0
f_test_function_K2 : (∀ x ∈ K2, 1 ≤ f2 x) ∧ Λ f2 < rieszContentAux Λ K2 + ε / 2
f_test_function_union : ∀ x ∈ K1 ⊔ K2, 1 ≤ (f1 + f2) x
⊢ Λ f1 + Λ f2 < rieszContentAux Λ K1 + rieszContentAux Λ K2 + ε
Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic

Goal state before:
pp: case h.refine_3
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
s₀ s₁ t : Set X
s₀_compact : IsCompact s₀
s₁_compact : IsCompact s₁
t_compact : IsCompact t
disj : Disjoint s₀ s₁
hst : s₀ ∪ s₁ ⊆ t
so : Fin 2 → Set X := fun j ↦ if j = 0 then s₀ᶜ else s₁ᶜ
hso : so = fun j ↦ if j = 0 then s₀ᶜ else s₁ᶜ
soopen : ∀ (j : Fin 2), IsOpen (so j)
hsot : t ⊆ ⋃ j, so j
f : Fin 2 → C(X, ℝ)
f_supp_in_so : ∀ (i : Fin 2), tsupport ⇑(f i) ⊆ so i
sum_f_one_on_t : EqOn (∑ i, ⇑(f i)) 1 t
f_in_icc : ∀ (i : Fin 2) (x : X), (f i) x ∈ Icc 0 1
f_hcs : ∀ (i : Fin 2), HasCompactSupport ⇑(f i)
sum_one_x : ∀ x ∈ t, (f 0) x + (f 1) x = 1
x : X
hx : x ∈ t
⊢ (f 0) x + (f 1) x = 1

Tactic:
exact sum_one_x x hx

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

Goal state before:
pp: case inl
f : ℝ → ℝ
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_lt : a < b
⊢ |trapezoidal_error f N a b| ≤ (b - a) ^ 3 * ζ / (12 * ↑N ^ 2)

Tactic:
exact trapezoidal_error_le_of_lt h_lt h_df h_ddf fpp_bound N_nonzero

Goal state after:
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)
⊢ t ∈ generateMeasurableRec s i → p t

Tactic:
suffices H : ∀ k ≤ i, ∀ t ∈ generateMeasurableRec s k, p t from H i le_rfl t
  intro k
  apply WellFoundedLT.induction k
  intro k IH hk t
  replace IH := fun j hj => IH j hj (hj.le.trans hk)
  unfold generateMeasurableRec
  rintro (((ht | rfl) | ht) | ⟨f, rfl⟩)
  · exact hs t ht
  · exact h0
  · simp_rw [mem_image, mem_iUnion₂] at ht
    obtain ⟨u, ⟨⟨j, hj, hj'⟩, rfl⟩⟩ := ht
    exact hc u (IH j hj u hj') ⟨j, hj.trans_le hk, hj'⟩
  · apply hn
    intro n
    obtain ⟨j, hj, hj'⟩ := mem_iUnion₂.1 (f n).2
    use IH j hj _ hj', j, hj.trans_le hk

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

Goal state before:
pp: case inr
α : Type u
s : Set (Set α)
i : Ordinal.{v}
this : ∀ i ≤ ω_ 1, #↑(generateMeasurableRec s i) ≤ max (#↑s) 2 ^ ℵ₀
hi : ω_ 1 < i
⊢ #↑(generateMeasurableRec s (ω_ 1)) ≤ max (#↑s) 2 ^ ℵ₀

Tactic:
exact this _ le_rfl

Goal state after:
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 ℝ
μ : 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)
⊢ ∫ (x : X), f x ∂μ + ε' * (2 * μ.real K + |a| + b + ε') ≤ ∫ (x : X), f x ∂μ + ε

Tactic:
by simp [hε'.2]

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

Goal state before:
pp: E : Type u_3
inst✝³ : MeasurableSpace E
μ : Measure E
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : BorelSpace E
r t : E
⊢ charFun (Measure.map (fun x ↦ r + x) μ) t = charFun μ t * cexp (↑⟪r, t⟫ * I)

Tactic:
simp_rw [add_comm r]
  exact charFun_map_add_const _ _

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

Goal state before:
pp: Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : PseudoMetricSpace Ω
inst✝ : OpensMeasurableSpace Ω
μs : ℕ → LevyProkhorov (ProbabilityMeasure Ω)
ν : LevyProkhorov (ProbabilityMeasure Ω)
hμs : Tendsto μs atTop (𝓝 ν)
P : ProbabilityMeasure Ω := ν.toMeasure
Ps : ℕ → ProbabilityMeasure Ω := toMeasure ∘ μs
f✝ f : Ω →ᵇ ℝ
f_nn : 0 ≤ f
f_zero : ¬‖f‖ = 0
norm_f_pos : 0 < ‖f‖
δ : ℝ
δ_pos : 0 < δ
εs : ℕ → ℝ
left✝ : StrictAnti εs
εs_pos : ∀ (n : ℕ), 0 < εs n
εs_lim : Tendsto εs atTop (𝓝 0)
ε_of_room : Tendsto (fun x ↦ dist (μs x) ν + εs x) atTop (𝓝 (0 + 0))
n : ℕ
⊢ dist (μs n) ν + εs n ∈ Ioi 0

Tactic:
mem_Ioi

Goal state after:
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : PseudoMetricSpace Ω
inst✝ : OpensMeasurableSpace Ω
μs : ℕ → LevyProkhorov (ProbabilityMeasure Ω)
ν : LevyProkhorov (ProbabilityMeasure Ω)
hμs : Tendsto μs atTop (𝓝 ν)
P : ProbabilityMeasure Ω := ν.toMeasure
Ps : ℕ → ProbabilityMeasure Ω := toMeasure ∘ μs
f✝ f : Ω →ᵇ ℝ
f_nn : 0 ≤ f
f_zero : ¬‖f‖ = 0
norm_f_pos : 0 < ‖f‖
δ : ℝ
δ_pos : 0 < δ
εs : ℕ → ℝ
left✝ : StrictAnti εs
εs_pos : ∀ (n : ℕ), 0 < εs n
εs_lim : Tendsto εs atTop (𝓝 0)
ε_of_room : Tendsto (fun x ↦ dist (μs x) ν + εs x) atTop (𝓝 (0 + 0))
n : ℕ
⊢ 0 < dist (μs n) ν + εs n
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
g : G
⊢ μ.addHaarScalarFactor ((DomMulAct.mk g)⁻¹ • μ) = (distribHaarChar A) g

Tactic:
by
  rw [← addHaarScalarFactor_domSMul _ _ (DomMulAct.mk g)]
  simp_rw [← mul_smul, mul_inv_cancel, one_smul]
  exact addHaarScalarFactor_smul_eq_distribHaarChar ..

Goal state after: