mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue

Goal state before:
pp: case pos
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : SignedMeasure α
f : α → ℝ
htμ : t ⟂ᵥ μ.toENNRealVectorMeasure
hadd : s = t + μ.withDensityᵥ f
hfi : Integrable f μ
⊢ t = s.singularPart μ

Tactic:
refine eq_singularPart' t hfi.1.measurable_mk (hfi.congr hfi.1.ae_eq_mk) htμ ?_
    convert! hadd using 2
    exact WithDensityᵥEq.congr_ae hfi.1.ae_eq_mk.symm

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

Goal state before:
pp: Ω : Type u_1
inst✝⁴ : TopologicalSpace Ω
inst✝³ : MeasurableSpace Ω
inst✝² : OpensMeasurableSpace Ω
ι : Type u_2
L : Filter ι
inst✝¹ : L.IsCountablyGenerated
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
c : ℝ≥0
E : Set Ω
E_mble : MeasurableSet E
fs : ι → Ω →ᵇ ℝ≥0
fs_bdd : ∀ᶠ (i : ι) in L, ∀ᵐ (ω : Ω) ∂μ, (fs i) ω ≤ c
fs_lim : ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun i ↦ (fs i) ω) L (𝓝 (E.indicator (fun x ↦ 1) ω))
ω : Ω
⊢ E.indicator (fun x ↦ 1) ω = ↑(E.indicator (fun x ↦ 1) ω)

Tactic:
by simp only [ENNReal.coe_indicator, ENNReal.coe_one]

Goal state after:
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
s t : SignedMeasure α
μ : Measure α
inst✝¹ : s.HaveLebesgueDecomposition μ
inst✝ : t.HaveLebesgueDecomposition μ
⊢ (s + t).singularPart μ = s.singularPart μ + t.singularPart μ

Tactic:
refine
    (eq_singularPart _ (s.rnDeriv μ + t.rnDeriv μ)
        ((mutuallySingular_singularPart s μ).add_left (mutuallySingular_singularPart t μ))
        ?_).symm
  rw [withDensityᵥ_add (integrable_rnDeriv s μ) (integrable_rnDeriv t μ), add_assoc,
    add_comm (t.singularPart μ), add_assoc, add_comm _ (t.singularPart μ),
    singularPart_add_withDensity_rnDeriv_eq, ← add_assoc,
    singularPart_add_withDensity_rnDeriv_eq]

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

Goal state before:
pp: case neg
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : HasOuterApproxClosed X
F : Set X
hF : IsClosed[inst✝¹] F
n : ℕ
x : X
hxF : x ∉ F
⊢ F.indicator (fun x ↦ 1) x ≤ (hF.apprSeq n) x

Tactic:
· simp only [hxF, not_false_eq_true, indicator_of_notMem, zero_le]

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

Goal state before:
pp: case neg
X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : HasOuterApproxClosed X
F : Set X
hF : IsClosed[inst✝³] F
inst✝¹ : MeasurableSpace X
inst✝ : OpensMeasurableSpace X
μ : Measure X
n : ℕ
x : X
hxF : x ∉ F
⊢ F.indicator (fun x ↦ 1) x ≤ (fun a ↦ ↑((hF.apprSeq n) a)) x

Tactic:
· simp only [hxF, not_false_eq_true, indicator_of_notMem, zero_le]

Goal state after:
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real

Goal state before:
pp: α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : Lattice E
inst✝² : HasSolidNorm E
inst✝¹ : IsOrderedAddMonoid E
inst✝ : IsOrderedModule ℝ E
f : α → E
hfint : Integrable f μ
h1 : μ[f | m] ≤ᵐ[μ] μ[fun a ↦ |f a| | m]
h2 : μ[-f | m] ≤ᵐ[μ] μ[fun a ↦ |f a| | m]
a : α
ha : μ[f | m] a ≤ μ[fun a ↦ |f a| | m] a
hb : μ[-f | m] a ≤ μ[fun a ↦ |f a| | m] a
hc : μ[-f | m] a = (-μ[f | m]) a
⊢ |μ[f | m]| a ≤ μ[|f| | m] a

Tactic:
exact abs_le'.2 ⟨ha, hc.symm.le.trans hb⟩

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

Goal state before:
pp: Ω : Type u_1
inst✝ : MeasurableSpace Ω
μ : FiniteMeasure Ω
⊢ μ.mass = 0 ↔ μ = 0

Tactic:
refine ⟨fun μ_mass => ?_, fun hμ => by simp only [hμ, zero_mass]⟩

Goal state after:
Ω : Type u_1
inst✝ : MeasurableSpace Ω
μ : FiniteMeasure Ω
μ_mass : μ.mass = 0
⊢ μ = 0
Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure

Goal state before:
pp: Ω : Type u_1
inst✝ : MeasurableSpace Ω
⊢ MeasurableSet {μ | IsProbabilityMeasure μ}

Tactic:
suffices { μ : Measure Ω | IsProbabilityMeasure μ } = (fun μ => μ univ) ⁻¹' {1} by
    rw [this]
    exact Measure.measurable_coe MeasurableSet.univ (measurableSet_singleton 1)
  ext _
  apply isProbabilityMeasure_iff

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

Goal state before:
pp: Ω : Type u_1
inst✝ : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
nonzero : μ ≠ 0
s : Set Ω
_s_mble : MeasurableSet s
⊢ ↑μ.normalize s = (μ.mass⁻¹ • ↑μ) s

Tactic:
← μ.normalize.ennreal_coeFn_eq_coeFn_toMeasure s,

Goal state after:
Ω : Type u_1
inst✝ : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
nonzero : μ ≠ 0
s : Set Ω
_s_mble : MeasurableSet s
⊢ ↑(μ.normalize s) = (μ.mass⁻¹ • ↑μ) s
Module: Mathlib.MeasureTheory.Function.UniformIntegrable

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
inst✝ : Finite ι
hp_one : 1 ≤ p
hp_top : p ≠ ∞
hf : ∀ (i : ι), MemLp (f i) p μ
val✝ : Fintype ι
hι : ¬Nonempty ι
⊢ ∃ C, ∀ (i : ι), eLpNorm (f i) p μ ≤ ↑C

Tactic:
· exact ⟨0, fun i => False.elim <| hι <| Nonempty.intro i⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
hp : p ≠ 0
hp' : p ≠ ∞
hf : ∀ (i : ι), StronglyMeasurable (f i)
ε : ℝ
hε : 0 < ε
hfu : UnifIntegrable f p μ
M : ℝ≥0
hM : ∀ (i : ι), eLpNorm (f i) p μ ≤ ↑M
ℐ : ℝ≥0 → ι
δ : ℝ≥0
hδpos : 0 < ↑δ
hδ :
  ∀ (i : ι) (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal ↑δ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε
hℐ : ∀ (C : ℝ≥0), ENNReal.ofReal ↑δ < μ {x | C ≤ ‖f (ℐ C) x‖₊}
this :
  ↑(2 * max M 1 * δ⁻¹ ^ (1 / p.toReal) * δ ^ (1 / p.toReal)) ≤ eLpNorm (f (ℐ (2 * max M 1 * δ⁻¹ ^ (1 / p.toReal)))) p μ
⊢ False

Tactic:
mul_assoc,

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
hp : p ≠ 0
hp' : p ≠ ∞
hf : ∀ (i : ι), StronglyMeasurable (f i)
ε : ℝ
hε : 0 < ε
hfu : UnifIntegrable f p μ
M : ℝ≥0
hM : ∀ (i : ι), eLpNorm (f i) p μ ≤ ↑M
ℐ : ℝ≥0 → ι
δ : ℝ≥0
hδpos : 0 < ↑δ
hδ :
  ∀ (i : ι) (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal ↑δ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε
hℐ : ∀ (C : ℝ≥0), ENNReal.ofReal ↑δ < μ {x | C ≤ ‖f (ℐ C) x‖₊}
this :
  ↑(2 * max M 1 * (δ⁻¹ ^ (1 / p.toReal) * δ ^ (1 / p.toReal))) ≤
    eLpNorm (f (ℐ (2 * max M 1 * δ⁻¹ ^ (1 / p.toReal)))) p μ
⊢ False
Module: Mathlib.MeasureTheory.Measure.Portmanteau

Goal state before:
pp: case refine_2
Ω : Type u_1
inst✝³ : PseudoMetricSpace Ω
inst✝² : MeasurableSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : Measure Ω
inst✝ : SFinite μ
s : Set Ω
Rs : ℕ → ℝ
left✝ : StrictAnti Rs
Rs_pos : ∀ (n : ℕ), 0 < Rs n
Rs_lim : Tendsto Rs atTop (𝓝 0)
obs : ∀ (n : ℕ), ∃ r ∈ Ioo 0 (Rs n), μ (frontier (Metric.thickening r s)) = 0
⊢ ∀ (n : ℕ), 0 < (fun n ↦ ⋯.choose) n ∧ μ (frontier (Metric.thickening ((fun n ↦ ⋯.choose) n) s)) = 0

Tactic:
· exact fun n ↦ ⟨(obs n).choose_spec.1.1, (obs n).choose_spec.2⟩

Goal state after:
Module: Mathlib.Probability.Independence.Basic

Goal state before:
pp: case refine_2
Ω : Type u_10
Ω' : Type u_11
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
μ : Measure Ω
ν : Measure Ω'
inst✝³ : IsProbabilityMeasure μ
inst✝² : IsProbabilityMeasure ν
𝓧 : Type u_12
𝓨 : Type u_13
inst✝¹ : MeasurableSpace 𝓧
inst✝ : MeasurableSpace 𝓨
X : Ω → 𝓧
Y : Ω' → 𝓨
mX : AEMeasurable X μ
mY : AEMeasurable Y ν
this : (fun ω ↦ AEMeasurable.mk X mX ω.1) ⟂ᵢ[μ.prod ν] fun ω ↦ AEMeasurable.mk Y mY ω.2
⊢ (fun ω ↦ AEMeasurable.mk Y mY ω.2) =ᵐ[μ.prod ν] fun ω ↦ Y ω.2

Tactic:
· rw [← Function.comp_def, ← Function.comp_def]
    apply ae_eq_comp
    · exact measurable_snd.aemeasurable
    · rw [measurePreserving_snd.map_eq]
      exact (AEMeasurable.ae_eq_mk mY).symm

Goal state after:
Module: Mathlib.Probability.Independence.Kernel.IndepFun

Goal state before:
pp: case refine_1
α : Type u_1
Ω : Type u_2
β : Type u_4
β' : Type u_5
γ : Type u_6
γ' : Type u_7
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
mγ : MeasurableSpace γ
mγ' : MeasurableSpace γ'
φ : β → γ
ψ : β' → γ'
hfg : IndepFun f g κ μ
hf : AEMeasurable f (⇑κ ∘ₘ μ)
hg : AEMeasurable g (⇑κ ∘ₘ μ)
hφ : AEMeasurable φ (Measure.map f (⇑κ ∘ₘ μ))
hψ : AEMeasurable ψ (Measure.map g (⇑κ ∘ₘ μ))
h : IndepFun (AEMeasurable.mk φ hφ ∘ f) (AEMeasurable.mk ψ hψ ∘ g) κ μ
hφ_ae : ∀ᵐ (x : Ω) ∂⇑κ ∘ₘ μ, φ (f x) = AEMeasurable.mk φ hφ (f x)
hψ_ae : ∀ᵐ (x : Ω) ∂⇑κ ∘ₘ μ, ψ (g x) = AEMeasurable.mk ψ hψ (g x)
⊢ ∀ᵐ (a : α) ∂μ, AEMeasurable.mk φ hφ ∘ f =ᵐ[κ a] φ ∘ f

Tactic:
filter_upwards [Measure.ae_ae_of_ae_comp (hφ_ae)] with a haφ
    filter_upwards [haφ] with ω hωφ
    simp [hωφ]

Goal state after:
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:
rw [covariance_comm, covariance_add_const_left hY c, covariance_comm]

Goal state after:
Module: Mathlib.Probability.Moments.Variance

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_2
s : Finset ι
X : ι → Ω → ℝ
inst✝ : IsFiniteMeasure μ
hX : ∀ i ∈ s, MemLp (X i) 2 μ
i : ι
hi : i ∈ s
⊢ cov[X i, ∑ i ∈ s, X i; μ] = ∑ j ∈ s, cov[X i, X j; μ]

Tactic:
rw [covariance_sum_right' (by simpa) (hX i hi)]

Goal state after:
Module: Mathlib.Probability.Moments.Variance

Goal state before:
pp: case pos
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
X : Ω → ℝ
hm : AEStronglyMeasurable X μ
hX : ¬MemLp X 2 μ
hint : Integrable X μ
⊢ ∫ (a : Ω), (X a - ∫ (x : Ω), X x ∂μ) ^ 2 ∂μ ≤ ∫ (x : Ω), (X ^ 2) x ∂μ

Tactic:
· rw [integral_undef]
      · exact integral_nonneg fun a => sq_nonneg _
      intro h
      have A : MemLp (X - fun ω : Ω => μ[X]) 2 μ :=
        (memLp_two_iff_integrable_sq (by fun_prop)).2 h
      have B : MemLp (fun _ : Ω => μ[X]) 2 μ := memLp_const _
      apply hX
      convert! A.add B
      simp

Goal state after:
Module: Mathlib.Probability.HasLaw

Goal state before:
pp: Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
X : Ω → 𝓧
μ : Measure 𝓧
P : Measure Ω
hX : HasLaw X μ P
p : 𝓧 → Prop
hp : MeasurableSet {x | p x}
⊢ P {ω | p (X ω)} = (map X P) {x | p x}

Tactic:
map_apply_of_aemeasurable hX.aemeasurable hp

Goal state after:
Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
X : Ω → 𝓧
μ : Measure 𝓧
P : Measure Ω
hX : HasLaw X μ P
p : 𝓧 → Prop
hp : MeasurableSet {x | p x}
⊢ P {ω | p (X ω)} = P (X ⁻¹' {x | p x})
Module: Mathlib.Probability.IdentDistrib

Goal state before:
pp: case hg
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace γ
inst✝² : MeasurableSpace δ
μ : Measure γ
μ' : Measure δ
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure μ'
X : γ → α
X' : δ → α
Y : γ → β
Y' : δ → β
h_indep : X ⟂ᵢ[μ] Y
h_ident : IdentDistrib (fun ω ↦ (X ω, Y ω)) (fun ω ↦ (X' ω, Y' ω)) μ μ'
⊢ AEMeasurable Y' μ'

Tactic:
exact measurable_snd.aemeasurable.comp_aemeasurable h_ident.aemeasurable_snd

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

Goal state before:
pp: R : Type u_2
inst✝⁷ : Ring R
inst✝⁶ : LinearOrder R
inst✝⁵ : FloorRing R
inst✝⁴ : TopologicalSpace R
inst✝³ : OrderTopology R
inst✝² : MeasurableSpace R
inst✝¹ : IsStrictOrderedRing R
inst✝ : BorelSpace R
s : Set R
hs : MeasurableSet s
⊢ MeasurableSet (⋃ m, (fun x ↦ x + ↑m) ⁻¹' s ∩ Ico 0 1)

Tactic:
exact MeasurableSet.iUnion fun m => (measurable_add_const _ hs).inter measurableSet_Ico

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

Goal state before:
pp: case pos
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝ : Preorder ι
s : Set (Filtration ι m)
i : ι
h_nonempty : s.Nonempty
⊢ sInf ((fun f ↦ ↑f i) '' s) ≤ m

Tactic:
obtain ⟨f, hf_mem⟩ := h_nonempty

Goal state after:
case pos
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝ : Preorder ι
s : Set (Filtration ι m)
i : ι
f : Filtration ι m
hf_mem : f ∈ s
⊢ sInf ((fun f ↦ ↑f i) '' s) ≤ m
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) * (b ^ (p⁻¹ * q) * x✝ ^ q * rexp (-(b * x✝ ^ p)))

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:
mul_assoc,

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) * (b ^ (p⁻¹ * q) * (x✝ ^ q * rexp (-(b * x✝ ^ p))))

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.MeasureTheory.Integral.Gamma

Goal state before:
pp: p q b : ℝ
hp : 0 < p
hq : -1 < q
hb : 0 < b
⊢ (b ^ p⁻¹)⁻¹ * (b ^ (-p⁻¹ * q) * (1 / p * Gamma ((q + 1) / p))) = b ^ (-(q + 1) / p) * (1 / p) * Gamma ((q + 1) / p)

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

Tactic:
mul_assoc,

Goal state after:
p q b : ℝ
hp : 0 < p
hq : -1 < q
hb : 0 < b
⊢ (b ^ p⁻¹)⁻¹ * (b ^ (-p⁻¹ * q) * (1 / p * Gamma ((q + 1) / p))) = b ^ (-(q + 1) / p) * (1 / p * Gamma ((q + 1) / p))

p q b : ℝ
hp : 0 < p
hq : -1 < q
hb : 0 < b
⊢ 0 < p
Module: Mathlib.MeasureTheory.Integral.Gamma

Goal state before:
pp: p q b : ℝ
hp : 1 ≤ p
hq : -2 < q
hb : 0 < b
⊢ 2 * π * ∫ (x : ℝ) in Ioi 0, x ^ (q + 1) * rexp (-b * x ^ p) =
    2 * π / p * b ^ (-(q + 2) / p) * Real.Gamma ((q + 2) / p)

Tactic:
rw [_root_.integral_rpow_mul_exp_neg_mul_rpow (by linarith) (by linarith) hb, add_assoc,
        one_add_one_eq_two]

Goal state after:
p q b : ℝ
hp : 1 ≤ p
hq : -2 < q
hb : 0 < b
⊢ 2 * π * (b ^ (-(q + 2) / p) * (1 / p) * Real.Gamma ((q + 2) / p)) =
    2 * π / p * b ^ (-(q + 2) / p) * Real.Gamma ((q + 2) / p)
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
x : α
hx : (fun x ↦ (ρ x).toReal) x = g x
⊢ (fun a ↦ f a * g a) x = (fun a ↦ (ρ a).toReal * f a) x

Tactic:
simp [hx, mul_comm]

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
hν0' : (ν s).toReal ≠ 0
hνfin : ν s ≠ ⊤
hν0'' : ν s ≠ 0
x : α
hx : (fun x ↦ (ρ x).toReal) x = g x
⊢ (fun x ↦ (ρ x).toReal * f x) x = (fun x ↦ f x * g x) x

Tactic:
simp [hx, mul_comm]

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:
by
  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.LebesgueNormedSpace

Goal state before:
pp: case mp.ht
α : 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' : g =ᵐ[μ.withDensity fun x ↦ ↑(f x)] g'
A : MeasurableSet {x | f x ≠ 0}
⊢ ∀ᵐ (x : α) ∂μ.restrict {x | f x ≠ 0}, (fun x ↦ ↑(f x) • g x) x = (fun x ↦ ↑(f x) • g' x) x

Tactic:
rw [EventuallyEq, ae_withDensity_iff hf.coe_nnreal_ennreal] at hg'
      rw [ae_restrict_iff' A]
      filter_upwards [hg']
      intro a ha h'a
      have : (f a : ℝ≥0∞) ≠ 0 := by simpa only [Ne, ENNReal.coe_eq_zero] using h'a
      rw [ha this]

Goal state after:
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
⊢ μ k ≤
    ⨅ f,
      ⨅ (_ : Continuous f),
        ⨅ (_ : HasCompactSupport f), ⨅ (_ : EqOn f 1 k), ⨅ (_ : 0 ≤ f), ENNReal.ofReal (∫ (x : X), f x ∂μ)

Tactic:
simp only [le_iInf_iff]
    intro f f_cont f_comp fk f_nonneg
    apply (f_cont.integrable_of_hasCompactSupport f_comp).measure_le_integral
    · exact Eventually.of_forall f_nonneg
    · exact fun x hx ↦ by simp [fk hx]

Goal state after:
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
⊢ |ddg x| ≤ ζ / 2 * (x - a) ^ 1

Tactic:
simp_rw [pow_one, ddg, abs_mul, abs_div, abs_two]

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 * |iteratedDerivWithin 2 f (Set.Icc a b) x| ≤ ζ / 2 * (x - a)
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)
x : X
h : ¬f x = 0
⊢ ↑(f x) = ↑((⇑g₁ + ⇑g₂) x) * ↑(f x)

Tactic:
rw [sum_g (mem_of_subset_of_mem subset_closure (mem_support.mpr h))]

Goal state after:
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)
x : X
h : ¬f x = 0
⊢ ↑(f x) = ↑(1 x) * ↑(f x)
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)
μ : (i : ι) → Measure (E i)
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
t : PiLp 2 E
⊢ charFun (Measure.map (toLp 2) (Measure.pi μ)) t = ∏ i, charFun (μ i) (t.ofLp i)

Tactic:
simp_rw [charFun, PiLp.inner_apply, ← MeasurableEquiv.coe_toLp, ← integral_fintype_prod_eq_prod,
    integral_map_equiv]

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)
μ : (i : ι) → Measure (E i)
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
t : PiLp 2 E
⊢ ∫ (x : (i : ι) → E i),
      cexp (↑(∑ i, ⟪((MeasurableEquiv.toLp 2 ((i : ι) → E i)) x).ofLp i, t.ofLp i⟫) * I) ∂Measure.pi μ =
    ∫ (x : (i : ι) → E i), ∏ i, cexp (↑⟪x i, t.ofLp i⟫ * I) ∂Measure.pi μ
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 : ν = Measure.pi μ
⊢ ∀ (t : WithLp 2 ((i : ι) → E i)), charFun (Measure.map (toLp 2) ν) t = ∏ i, charFun (μ i) (t.ofLp i)

Tactic:
rw [h]; exact charFun_pi

Goal state after: