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

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝ : Preorder ι
s : Set (Filtration ι m)
i j : ι
hij : i ≤ j
⊢ (fun i ↦ sSup ((fun f ↦ ↑f i) '' s)) i ≤ (fun i ↦ sSup ((fun f ↦ ↑f i) '' s)) j

Tactic:
refine sSup_le fun m' hm' => ?_

Goal state after:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝ : Preorder ι
s : Set (Filtration ι m)
i j : ι
hij : i ≤ j
m' : MeasurableSpace Ω
hm' : m' ∈ (fun f ↦ ↑f i) '' s
⊢ m' ≤ (fun i ↦ sSup ((fun f ↦ ↑f i) '' s)) j
Module: Mathlib.Probability.Process.Filtration

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

Tactic:
refine sSup_le fun m' hm' => ?_

Goal state after:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝ : Preorder ι
s : Set (Filtration ι m)
i : ι
m' : MeasurableSpace Ω
hm' : m' ∈ (fun f ↦ ↑f i) '' s
⊢ m' ≤ m
Module: Mathlib.MeasureTheory.Function.ConvergenceInDistribution

Goal state before:
pp: ι : 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 → ℝ
M : ℝ
hF_bounded : ∀ (x y : E), dist (F x) (F y) ≤ M
L : NNReal
hF_lip : LipschitzWith L F
hF_cont : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] F
hL : 0 < L
ε : ℝ
hε : ε > 0
n : ι
h_int_Y : Integrable (fun x ↦ F (Y n x)) μ''
h_int_X : Integrable (fun x ↦ F (X n x)) μ''
h_int_sub : Integrable (fun a ↦ ‖F (Y n a) - F (X n a)‖) μ''
⊢ ↑L * (ε / 2 * μ''.real {x | ‖Y n x - X n x‖ < ε / 2}) + M * μ''.real {ω | ε / 2 ≤ ‖Y n ω - X n ω‖} ≤
    ↑L * (ε / 2) + M * μ''.real {ω | ε / 2 ≤ ‖Y n ω - X n ω‖}

Tactic:
gcongr

Goal state after:
case hbc
ι : 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 := ⋯
F : E → ℝ
M : ℝ
hF_bounded : ∀ (x y : E), dist (F x) (F y) ≤ M
L : NNReal
hF_lip : LipschitzWith L F
hF_cont : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] F
hL : 0 < L
ε : ℝ
hε : ε > 0
n : ι
h_int_Y : Integrable (fun x ↦ F (Y n x)) μ''
h_int_X : Integrable (fun x ↦ F (X n x)) μ''
h_int_sub : Integrable (fun a ↦ ‖F (Y n a) - F (X n a)‖) μ''
⊢ ε / 2 * μ''.real {x | ‖Y n x - X n x‖ < ε / 2} ≤ ε / 2
Module: Mathlib.Probability.Process.Filtration

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝¹ : LinearOrder ι
inst✝ : SuccOrder ι
𝓕 : Filtration ι m
⊢ 𝓕₊ = 𝓕

Tactic:
let := Preorder.topology ι

Goal state after:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝¹ : LinearOrder ι
inst✝ : SuccOrder ι
𝓕 : Filtration ι m
this : TopologicalSpace ι := Preorder.topology ι
⊢ 𝓕₊ = 𝓕
Module: Mathlib.Probability.Process.Filtration

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝ : PartialOrder ι
𝓕 : Filtration ι m
i : ι
hi : IsMax i
⊢ ↑𝓕₊ i = ↑𝓕 i

Tactic:
let := Preorder.topology ι

Goal state after:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝ : PartialOrder ι
𝓕 : Filtration ι m
i : ι
hi : IsMax i
this : TopologicalSpace ι := Preorder.topology ι
⊢ ↑𝓕₊ i = ↑𝓕 i
Module: Mathlib.Probability.Process.Filtration

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝ : LinearOrder ι
𝓕 : Filtration ι m
i : ι
hi : ∃ j > i, Set.Ioo i j = ∅
⊢ ↑𝓕₊ i = ↑𝓕 i

Tactic:
let := Preorder.topology ι

Goal state after:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝ : LinearOrder ι
𝓕 : Filtration ι m
i : ι
hi : ∃ j > i, Set.Ioo i j = ∅
this : TopologicalSpace ι := Preorder.topology ι
⊢ ↑𝓕₊ i = ↑𝓕 i
Module: Mathlib.Probability.Process.Filtration

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝¹ : LinearOrder ι
inst✝ : DenselyOrdered ι
𝓕 : Filtration ι m
i : ι
hi : ¬IsMax i
⊢ ↑𝓕₊ i = ⨅ j, ⨅ (_ : j > i), ↑𝓕 j

Tactic:
let := Preorder.topology ι

Goal state after:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝¹ : LinearOrder ι
inst✝ : DenselyOrdered ι
𝓕 : Filtration ι m
i : ι
hi : ¬IsMax i
this : TopologicalSpace ι := Preorder.topology ι
⊢ ↑𝓕₊ i = ⨅ j, ⨅ (_ : j > i), ↑𝓕 j
Module: Mathlib.Probability.Process.Filtration

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝ : PartialOrder ι
𝓕 : Filtration ι m
⊢ 𝓕 ≤ 𝓕₊

Tactic:
let := Preorder.topology ι

Goal state after:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝ : PartialOrder ι
𝓕 : Filtration ι m
this : TopologicalSpace ι := Preorder.topology ι
⊢ 𝓕 ≤ 𝓕₊
Module: Mathlib.Probability.Process.Filtration

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝ : PartialOrder ι
𝓕 : Filtration ι m
⊢ 𝓕₊₊ = 𝓕₊

Tactic:
let := Preorder.topology ι

Goal state after:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝ : PartialOrder ι
𝓕 : Filtration ι m
this : TopologicalSpace ι := Preorder.topology ι
⊢ 𝓕₊₊ = 𝓕₊
Module: Mathlib.Probability.Independence.Kernel.IndepFun

Goal state before:
pp: α : Type u_1
Ω : Type u_2
ι : Type u_3
β : Type u_4
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
mβ : MeasurableSpace β
X : ι → Ω → α
Y : ι → Ω → β
f : ι → Set Ω
t : ι → Set β
s : Finset ι
inst✝ : Finite ι
hY : ∀ (i : ι), Measurable (Y i)
hindep : iIndepFun (fun i ω ↦ (X i ω, Y i ω)) κ μ
hf : ∀ i ∈ s, MeasurableSet (f i)
hy✝ : ∀ᵐ (a : α) ∂μ, ∀ i ∉ s, (κ a) (Y i ⁻¹' t i) ≠ 0
ht : ∀ (i : ι), MeasurableSet (t i)
val✝ : Fintype ι
g : ι → Set Ω := fun i' ↦ if i' ∈ s then Y i' ⁻¹' t i' ∩ f i' else Y i' ⁻¹' t i'
hYt✝ : ∀ (i : ι), MeasurableSet (Y i ⁻¹' t i)
hg✝ : ∀ (i : ι), MeasurableSet (g i)
a : α
hy : ∀ i ∉ s, (κ a) (Y i ⁻¹' t i) ≠ 0
a✝ : IsProbabilityMeasure (κ a)
hYt : (κ a) (⋂ i, Y i ⁻¹' t i) = ∏ i, (κ a) (Y i ⁻¹' t i)
hg : (κ a) (⋂ i, g i) = ∏ i, (κ a) (g i)
⊢ (κ a)[⋂ i ∈ s, f i | ⋂ i, Y i ⁻¹' t i] = ((κ a) (⋂ i, Y i ⁻¹' t i))⁻¹ * (κ a) ((⋂ i, Y i ⁻¹' t i) ∩ ⋂ i ∈ s, f i)

Tactic:
by
      rw [cond_apply]; exact .iInter fun i ↦ hY i (ht i)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
g : α → β
hp_ne_top : p ≠ ∞
hg : MemLp g p μ
⊢ UnifTight (fun x ↦ g) p μ

Tactic:
by
  intro ε hε
  by_cases hε_top : ε = ∞
  · exact ⟨∅, (by simp), fun _ => hε_top.symm ▸ le_top⟩
  obtain ⟨s, _, hμs, hgε⟩ := hg.exists_eLpNorm_indicator_compl_lt hp_ne_top (coe_ne_zero.mpr hε.ne')
  exact ⟨s, ne_of_lt hμs, fun _ => hgε.le⟩

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
inst✝ : μ.InnerRegular
g : G
⊢ map (fun x ↦ x * g) μ = modularCharacterFun g • μ

Tactic:
rw [modularCharacterFun_eq_haarScalarFactor μ _]

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
inst✝ : μ.InnerRegular
g : G
⊢ map (fun x ↦ x * g) μ = (map (fun x ↦ x * g) μ).haarScalarFactor μ • μ
Module: Mathlib.MeasureTheory.Group.GeometryOfNumbers

Goal state before:
pp: 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
this : (⋂ n, (1 + u n) • ↑K ∩ (↑L \ {0})).Nonempty
⊢ ∃ x, x ≠ 0 ∧ ↑x ∈ s

Tactic:
NNReal.smul_def,

Goal state after:
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
this : (⋂ n, ↑(1 + u n) • ↑K ∩ (↑L \ {0})).Nonempty
⊢ ∃ x, x ≠ 0 ∧ ↑x ∈ s
Module: Mathlib.MeasureTheory.Group.GeometryOfNumbers

Goal state before:
pp: case refine_2
E : Type u_1
inst✝⁸ : MeasurableSpace E
μ : Measure E
F s : Set E
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : BorelSpace E
inst✝⁴ : FiniteDimensional ℝ E
inst✝³ : 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 : ℕ
⊢ μ s < μ ((1 + u n) • ↑K)

Tactic:
NNReal.smul_def,

Goal state after:
case refine_2
E : Type u_1
inst✝⁸ : MeasurableSpace E
μ : Measure E
F s : Set E
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : BorelSpace E
inst✝⁴ : FiniteDimensional ℝ E
inst✝³ : 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 : ℕ
⊢ μ s < μ (↑(1 + u n) • ↑K)
Module: Mathlib.MeasureTheory.Group.GeometryOfNumbers

Goal state before:
pp: case refine_2
E : Type u_1
inst✝⁸ : MeasurableSpace E
μ : Measure E
F s : Set E
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : BorelSpace E
inst✝⁴ : FiniteDimensional ℝ E
inst✝³ : 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 * μ s < ENNReal.ofReal ((1 + ↑(u n)) ^ finrank ℝ E) * μ s

Tactic:
gcongr

Goal state after:
case hinf
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 : ℕ
⊢ μ s ≠ ∞

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)
Module: Mathlib.MeasureTheory.Integral.Gamma

Goal state before:
pp: case e'_2
p : ℝ
hp : 0 < p
⊢ ∫ (x : ℝ) in Ioi 0, rexp (-x ^ p) = ∫ (x : ℝ) in Ioi 0, x ^ 0 * rexp (-x ^ p)

pp: case e'_3
p : ℝ
hp : 0 < p
⊢ Gamma (1 / p + 1) = 1 / p * Gamma ((0 + 1) / p)

Tactic:
· simp_rw [rpow_zero, one_mul]

Goal state after:
case e'_3
p : ℝ
hp : 0 < p
⊢ Gamma (1 / p + 1) = 1 / p * Gamma ((0 + 1) / p)
Module: Mathlib.MeasureTheory.Integral.Gamma

Goal state before:
pp: case e'_2
p b : ℝ
hp : 0 < p
hb : 0 < b
⊢ ∫ (x : ℝ) in Ioi 0, rexp (-b * x ^ p) = ∫ (x : ℝ) in Ioi 0, x ^ 0 * rexp (-b * x ^ p)

pp: case e'_3
p b : ℝ
hp : 0 < p
hb : 0 < b
⊢ b ^ (-1 / p) * Gamma (1 / p + 1) = b ^ (-(0 + 1) / p) * (1 / p) * Gamma ((0 + 1) / p)

Tactic:
· simp_rw [rpow_zero, one_mul]

Goal state after:
case e'_3
p b : ℝ
hp : 0 < p
hb : 0 < b
⊢ b ^ (-1 / p) * Gamma (1 / p + 1) = b ^ (-(0 + 1) / p) * (1 / p) * Gamma ((0 + 1) / p)
Module: Mathlib.MeasureTheory.Integral.Gamma

Goal state before:
pp: case e'_2
p : ℝ
hp : 1 ≤ p
⊢ ∫ (x : ℂ), rexp (-‖x‖ ^ p) = ∫ (x : ℂ), ‖x‖ ^ 0 * rexp (-‖x‖ ^ p)

pp: case e'_3
p : ℝ
hp : 1 ≤ p
⊢ π * Real.Gamma (2 / p + 1) = 2 * π / p * Real.Gamma ((0 + 2) / p)

Tactic:
· simp_rw [rpow_zero, one_mul]

Goal state after:
case e'_3
p : ℝ
hp : 1 ≤ p
⊢ π * Real.Gamma (2 / p + 1) = 2 * π / p * Real.Gamma ((0 + 2) / p)
Module: Mathlib.MeasureTheory.Integral.Gamma

Goal state before:
pp: case e'_2
p b : ℝ
hp : 1 ≤ p
hb : 0 < b
⊢ ∫ (x : ℂ), rexp (-b * ‖x‖ ^ p) = ∫ (x : ℂ), ‖x‖ ^ 0 * rexp (-b * ‖x‖ ^ p)

pp: case e'_3
p b : ℝ
hp : 1 ≤ p
hb : 0 < b
⊢ π * b ^ (-2 / p) * Real.Gamma (2 / p + 1) = 2 * π / p * b ^ (-(0 + 2) / p) * Real.Gamma ((0 + 2) / p)

Tactic:
· simp_rw [rpow_zero, one_mul]

Goal state after:
case e'_3
p b : ℝ
hp : 1 ≤ p
hb : 0 < b
⊢ π * b ^ (-2 / p) * Real.Gamma (2 / p + 1) = 2 * π / p * b ^ (-(0 + 2) / p) * Real.Gamma ((0 + 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 : α) in s, (ρ x).toReal * f x ∂μ = ∫ (x : α) in s, f x ∂ν

Tactic:
have h := setIntegral_withDensity_eq_setIntegral_toReal_smul₀ hρ_ae hρ_top f hs_meas

Goal state after:
α : 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
h : (∫ (x : α) in s, f x ∂μ.withDensity fun x ↦ ρ x) = ∫ (x : α) in s, (ρ x).toReal • f x ∂μ
⊢ ∫ (x : α) in s, (ρ x).toReal * f x ∂μ = ∫ (x : α) in s, f x ∂ν
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
B : ℝ → ℝ
hab : a ≤ b
hfc : ContinuousOn f (Icc a b)
hfd : DifferentiableOn ℝ f (Ioo a b)
hfB : ∀ᵐ (t : ℝ), t ∈ Ioo a b → ‖deriv f t‖ ≤ B t
hBi : IntervalIntegrable B volume a b
⊢ ‖f b - f a‖ ≤ ∫ (t : ℝ) in a..b, B t

Tactic:
wlog hE : CompleteSpace E generalizing E
  · set g : ℝ → UniformSpace.Completion E := (↑) ∘ f with hg
    have hgc : ContinuousOn g (Icc a b) :=
      (UniformSpace.Completion.continuous_coe E).comp_continuousOn hfc
    have hgd : DifferentiableOn ℝ g (Ioo a b) :=
      UniformSpace.Completion.toComplL.differentiable.comp_differentiableOn hfd
    have hdg t (ht : t ∈ Ioo a b) : deriv g t = deriv f t := by
      have : HasFDerivAt (𝕜 := ℝ) (↑) UniformSpace.Completion.toComplL (f t) := by
        rw [← UniformSpace.Completion.coe_toComplL (𝕜 := ℝ)]
        exact (UniformSpace.Completion.toComplL (E := E) (𝕜 := ℝ)).hasFDerivAt
      have hdft : HasDerivAt f (deriv f t) t := hfd.hasDerivAt <| Ioo_mem_nhds ht.1 ht.2
      rw [hg, (this.comp_hasDerivAt t hdft).deriv, UniformSpace.Completion.coe_toComplL]
    have hgn : ∀ᵐ t, t ∈ Ioo a b → ‖deriv g t‖ ≤ B t :=
      hfB.mono fun t htB ht ↦ by
        simpa only [hdg t ht, UniformSpace.Completion.norm_coe] using htB ht
    simpa [g, ← dist_eq_norm_sub] using this hgc hgd hgn inferInstance
  -- In a complete space, we have
  -- `‖f b - f a‖ = ‖∫ t in a..b, deriv f t‖ ≤ ∫ t in a..b, ‖deriv f t‖`
  have hfB' : (‖deriv f ·‖) ≤ᵐ[volume.restrict (uIoc a b)] B := by
    rwa [uIoc_of_le hab, ← Measure.restrict_congr_set Ioo_ae_eq_Ioc, EventuallyLE,
        ae_restrict_iff' measurableSet_Ioo]
  rw [← intervalIntegral.integral_eq_sub_of_hasDeriv_right (f' := deriv f)]
  · apply intervalIntegral.norm_integral_le_of_norm_le hab _ hBi
    rwa [← ae_restrict_iff' measurableSet_Ioc, ← uIoc_of_le hab]
  · rwa [uIcc_of_le hab]
  · rw [min_eq_left hab, max_eq_right hab]
    intro t ht
    exact hfd.hasDerivAt (isOpen_Ioo.mem_nhds ht) |>.hasDerivWithinAt
  · apply hBi.mono_fun (aestronglyMeasurable_deriv _ _)
    exact hfB'.trans <| .of_forall fun _ ↦ le_abs_self _

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

Goal state before:
pp: case mp.htc
α : 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:
filter_upwards [ae_restrict_mem A.compl]
      intro x hx
      simp only [Classical.not_not, mem_ofPred_eq, mem_compl_iff] at hx
      simp [hx]

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

Goal state before:
pp: E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
a b : E
C : ℝ
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hf : DiffContOnCl ℝ f s
hab : openSegment ℝ a b ⊆ s
hC : ∀ x ∈ s, ‖fderiv ℝ f x‖ ≤ C
hmem_s : ∀ t ∈ Ioo 0 1, (lineMap a b) t ∈ s
hC₀ : 0 ≤ C
hfc : ContinuousOn f (segment ℝ a b)
hfd : ∀ t ∈ Ioo 0 1, LineDifferentiableAt ℝ f ((lineMap a b) t) (b - a)
hfC : ∀ t ∈ Ioo 0 1, ‖lineDeriv ℝ f ((lineMap a b) t) (b - a)‖ ≤ C * ‖b - a‖
⊢ C * ‖b - a‖ * volume.real {t | t ∈ Ioo 0 1 ∧ lineDeriv ℝ f ((lineMap a b) t) (b - a) ≠ 0} ≤
    C * ‖b - a‖ * volume.real {t | t ∈ Ioo 0 1 ∧ fderiv ℝ f ((lineMap a b) t) ≠ 0}

Tactic:
gcongr

Goal state after:
case h₂
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
a b : E
C : ℝ
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hf : DiffContOnCl ℝ f s
hab : openSegment ℝ a b ⊆ s
hC : ∀ x ∈ s, ‖fderiv ℝ f x‖ ≤ C
hmem_s : ∀ t ∈ Ioo 0 1, (lineMap a b) t ∈ s
hC₀ : 0 ≤ C
hfc : ContinuousOn f (segment ℝ a b)
hfd : ∀ t ∈ Ioo 0 1, LineDifferentiableAt ℝ f ((lineMap a b) t) (b - a)
hfC : ∀ t ∈ Ioo 0 1, ‖lineDeriv ℝ f ((lineMap a b) t) (b - a)‖ ≤ C * ‖b - a‖
⊢ autoParam (volume {t | t ∈ Ioo 0 1 ∧ fderiv ℝ f ((lineMap a b) t) ≠ 0} ≠ ⊤) measureReal_mono._auto_1

case h₁
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
a b : E
C : ℝ
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hf : DiffContOnCl ℝ f s
hab : openSegment ℝ a b ⊆ s
hC : ∀ x ∈ s, ‖fderiv ℝ f x‖ ≤ C
hmem_s : ∀ t ∈ Ioo 0 1, (lineMap a b) t ∈ s
hC₀ : 0 ≤ C
hfc : ContinuousOn f (segment ℝ a b)
hfd : ∀ t ∈ Ioo 0 1, LineDifferentiableAt ℝ f ((lineMap a b) t) (b - a)
hfC : ∀ t ∈ Ioo 0 1, ‖lineDeriv ℝ f ((lineMap a b) t) (b - a)‖ ≤ C * ‖b - a‖
t : ℝ
a✝ : t ∈ Ioo 0 1
⊢ fderiv ℝ f ((lineMap a b) t) = 0 → lineDeriv ℝ f ((lineMap a b) t) (b - a) = 0
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 ∂μ)

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

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:
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,
      ⨅ (_ : Continuous f),
        ⨅ (_ : HasCompactSupport f), ⨅ (_ : EqOn f 1 k), ⨅ (_ : 0 ≤ f), ENNReal.ofReal (∫ (x : X), f x ∂μ) ≤
    μ k
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule

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

Tactic:
Nat.cast_sub (mem_range.mp hk),

Goal state after:
case e_a.e_a
f : ℝ → ℝ
N : ℕ
N_nonzero : 0 < N
a b : ℝ
k : ℕ
hk : k ∈ Finset.range (N - 1)
⊢ f (a + (↑(N - 1) - ↑k.succ + ↑1) * (b - a) / ↑N) = f (b + ↑(k + 1) * (a - b) / ↑N)