mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Probability.Independence.Kernel.Indep

Goal state before:
pp: case inr.refine_1
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
m : ι → MeasurableSpace Ω
h_le : ∀ (i : ι), m i ≤ _mΩ
h_indep : iIndep m κ μ
S T : Set ι
hST : Disjoint S T
hμ : μ ≠ 0
η : Kernel α Ω
η_eq : ⇑κ =ᵐ[μ] ⇑η
hη : IsMarkovKernel η
⊢ IsPiSystem (piiUnionInter (fun n ↦ {s | MeasurableSet s}) S)

pp: case inr.refine_2
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
m : ι → MeasurableSpace Ω
h_le : ∀ (i : ι), m i ≤ _mΩ
h_indep : iIndep m κ μ
S T : Set ι
hST : Disjoint S T
hμ : μ ≠ 0
η : Kernel α Ω
η_eq : ⇑κ =ᵐ[μ] ⇑η
hη : IsMarkovKernel η
⊢ IsPiSystem (piiUnionInter (fun n ↦ {s | MeasurableSet s}) T)

pp: case inr.refine_3
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
m : ι → MeasurableSpace Ω
h_le : ∀ (i : ι), m i ≤ _mΩ
h_indep : iIndep m κ μ
S T : Set ι
hST : Disjoint S T
hμ : μ ≠ 0
η : Kernel α Ω
η_eq : ⇑κ =ᵐ[μ] ⇑η
hη : IsMarkovKernel η
⊢ IndepSets (piiUnionInter (fun n ↦ {s | MeasurableSet s}) S) (piiUnionInter (fun n ↦ {s | MeasurableSet s}) T) η μ

Tactic:
· exact isPiSystem_piiUnionInter _ (fun n => @isPiSystem_measurableSet Ω (m n)) _

Goal state after:
case inr.refine_2
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
m : ι → MeasurableSpace Ω
h_le : ∀ (i : ι), m i ≤ _mΩ
h_indep : iIndep m κ μ
S T : Set ι
hST : Disjoint S T
hμ : μ ≠ 0
η : Kernel α Ω
η_eq : ⇑κ =ᵐ[μ] ⇑η
hη : IsMarkovKernel η
⊢ IsPiSystem (piiUnionInter (fun n ↦ {s | MeasurableSet s}) T)

case inr.refine_3
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
m : ι → MeasurableSpace Ω
h_le : ∀ (i : ι), m i ≤ _mΩ
h_indep : iIndep m κ μ
S T : Set ι
hST : Disjoint S T
hμ : μ ≠ 0
η : Kernel α Ω
η_eq : ⇑κ =ᵐ[μ] ⇑η
hη : IsMarkovKernel η
⊢ IndepSets (piiUnionInter (fun n ↦ {s | MeasurableSet s}) S) (piiUnionInter (fun n ↦ {s | MeasurableSet s}) T) η μ
Module: Mathlib.Probability.Independence.Kernel.Indep

Goal state before:
pp: case inr.refine_2
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
m : ι → MeasurableSpace Ω
h_le : ∀ (i : ι), m i ≤ _mΩ
h_indep : iIndep m κ μ
S T : Set ι
hST : Disjoint S T
hμ : μ ≠ 0
η : Kernel α Ω
η_eq : ⇑κ =ᵐ[μ] ⇑η
hη : IsMarkovKernel η
⊢ IsPiSystem (piiUnionInter (fun n ↦ {s | MeasurableSet s}) T)

pp: case inr.refine_3
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
m : ι → MeasurableSpace Ω
h_le : ∀ (i : ι), m i ≤ _mΩ
h_indep : iIndep m κ μ
S T : Set ι
hST : Disjoint S T
hμ : μ ≠ 0
η : Kernel α Ω
η_eq : ⇑κ =ᵐ[μ] ⇑η
hη : IsMarkovKernel η
⊢ IndepSets (piiUnionInter (fun n ↦ {s | MeasurableSet s}) S) (piiUnionInter (fun n ↦ {s | MeasurableSet s}) T) η μ

Tactic:
· exact isPiSystem_piiUnionInter _ (fun n => @isPiSystem_measurableSet Ω (m n)) _

Goal state after:
case inr.refine_3
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
m : ι → MeasurableSpace Ω
h_le : ∀ (i : ι), m i ≤ _mΩ
h_indep : iIndep m κ μ
S T : Set ι
hST : Disjoint S T
hμ : μ ≠ 0
η : Kernel α Ω
η_eq : ⇑κ =ᵐ[μ] ⇑η
hη : IsMarkovKernel η
⊢ IndepSets (piiUnionInter (fun n ↦ {s | MeasurableSet s}) S) (piiUnionInter (fun n ↦ {s | MeasurableSet s}) T) η μ
Module: Mathlib.Probability.Density

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
inst✝ : IsFiniteMeasure ℙ
f : ℝ → ℝ
g : ℝ → ℝ≥0∞
hg : pdf X ℙ volume =ᵐ[volume] g
hgi : ∫⁻ (x : ℝ), ‖f x‖ₑ * g x ≠ ∞
⊢ (fun i ↦ ‖f i‖ₑ * ENNReal.ofReal (pdf X ℙ volume i).toReal) =ᵐ[volume] fun x ↦ ‖f x‖ₑ * ‖(pdf X ℙ volume x).toReal‖ₑ

Tactic:
refine .fun_mul (ae_eq_refl _) ?_

Goal state after:
Ω : Type u_1
m : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
inst✝ : IsFiniteMeasure ℙ
f : ℝ → ℝ
g : ℝ → ℝ≥0∞
hg : pdf X ℙ volume =ᵐ[volume] g
hgi : ∫⁻ (x : ℝ), ‖f x‖ₑ * g x ≠ ∞
⊢ (fun i ↦ ENNReal.ofReal (pdf X ℙ volume i).toReal) =ᵐ[volume] fun x ↦ ‖(pdf X ℙ volume x).toReal‖ₑ
Module: Mathlib.Probability.Independence.Kernel.Indep

Goal state before:
pp: α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
π : ι → Set (Set Ω)
a : ι
S : Finset ι
hp_ind : iIndepSets π κ μ
haS : a ∉ S
t1 t2 : Set Ω
s : Finset ι
hs_mem : s ⊆ S
ft1 : ι → Set Ω
hft1_mem : ∀ x ∈ s, ft1 x ∈ π x
ht1_eq : t1 = ⋂ x ∈ s, ft1 x
ht2_mem_pia : t2 ∈ π a
f : ι → Set Ω := fun n ↦ if n = a then t2 else if n ∈ s then ft1 n else univ
h_f_mem : ∀ n ∈ insert a s, f n ∈ π n
h_f_mem_pi : ∀ n ∈ s, f n ∈ π n
h_t1 : t1 = ⋂ n ∈ s, f n
h_μ_t1 : ∀ᵐ (a' : α) ∂μ, (κ a') t1 = ∏ n ∈ s, (κ a') (f n)
h_t2 : t2 = f a
h_t1_inter_t2 : t1 ∩ t2 = ⋂ n ∈ insert a s, f n
a' : α
ha' : (κ a') (⋂ i ∈ insert a s, f i) = ∏ i ∈ insert a s, (κ a') (f i)
⊢ (κ a') (t1 ∩ t2) = ∏ n ∈ insert a s, (κ a') (f n)

Tactic:
rw [h_t1_inter_t2, ← ha']

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

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hX : AEStronglyMeasurable X μ
hX_not : ¬MemLp X 2 μ
⊢ Var[X; μ] = 0

Tactic:
simp [variance, (evariance_eq_top_iff hX).mpr hX_not]

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 ω ↦ c + Y ω; μ] = cov[X, Y; μ]

Tactic:
by
  simp_rw [add_comm c]
  exact covariance_add_const_right hY c

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

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
f g : Ω → ℝ≥0∞
h_meas_f : AEMeasurable f μ
h_meas_g : AEMeasurable g μ
h_indep_fun : f ⟂ᵢ[μ] g
fg_ae : f * g =ᵐ[μ] AEMeasurable.mk f h_meas_f * AEMeasurable.mk g h_meas_g
⊢ ∫⁻ (ω : Ω), (f * g) ω ∂μ = (∫⁻ (a : Ω), AEMeasurable.mk f h_meas_f a ∂μ) * ∫⁻ (ω : Ω), g ω ∂μ

Tactic:
lintegral_congr_ae h_meas_g.ae_eq_mk,

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
f g : Ω → ℝ≥0∞
h_meas_f : AEMeasurable f μ
h_meas_g : AEMeasurable g μ
h_indep_fun : f ⟂ᵢ[μ] g
fg_ae : f * g =ᵐ[μ] AEMeasurable.mk f h_meas_f * AEMeasurable.mk g h_meas_g
⊢ ∫⁻ (ω : Ω), (f * g) ω ∂μ = (∫⁻ (a : Ω), AEMeasurable.mk f h_meas_f a ∂μ) * ∫⁻ (a : Ω), AEMeasurable.mk g h_meas_g a ∂μ
Module: Mathlib.Probability.Moments.Variance

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_3
X : ι → Ω → ℝ
s : Finset ι
hs : ∀ i ∈ s, MemLp (X i) 2 μ
h : (↑s).Pairwise fun i j ↦ X i ⟂ᵢ[μ] X j
h'' : ∀ i ∈ s, X i =ᵐ[μ] 0
this : ∀ (i : ↥s), X ↑i =ᵐ[μ] 0
ω : Ω
hω : ∀ (i : ↥s), X (↑i) ω = 0 ω
⊢ (∑ i ∈ s, X i) ω = 0 ω

Tactic:
simp only [Finset.sum_apply, Pi.zero_apply]

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_3
X : ι → Ω → ℝ
s : Finset ι
hs : ∀ i ∈ s, MemLp (X i) 2 μ
h : (↑s).Pairwise fun i j ↦ X i ⟂ᵢ[μ] X j
h'' : ∀ i ∈ s, X i =ᵐ[μ] 0
this : ∀ (i : ↥s), X ↑i =ᵐ[μ] 0
ω : Ω
hω : ∀ (i : ↥s), X (↑i) ω = 0 ω
⊢ ∑ c ∈ s, X c ω = 0
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.real {ω | p (X ω)} = μ.real {x | p x}

Tactic:
rw [← hX.map_eq, map_measureReal_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.real {ω | p (X ω)} = P.real (X ⁻¹' {x | p x})
Module: Mathlib.Probability.Moments.Variance

Goal state before:
pp: case refine_2
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
inst✝¹ : IsProbabilityMeasure μ
inst✝ : IsProbabilityMeasure ν
X : Ω → ℝ
Y : Ω' → ℝ
hfμ : MemLp X 2 μ
hgν : MemLp Y 2 ν
⊢ Var[X; μ] + Var[fun x ↦ Y x.2; μ.prod ν] = Var[X; μ] + Var[Y; ν]

Tactic:
measurePreserving_snd.variance_fun_comp hgν.aemeasurable

Goal state after:
case refine_2
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
inst✝¹ : IsProbabilityMeasure μ
inst✝ : IsProbabilityMeasure ν
X : Ω → ℝ
Y : Ω' → ℝ
hfμ : MemLp X 2 μ
hgν : MemLp Y 2 ν
⊢ Var[X; μ] + Var[Y; ν] = Var[X; μ] + Var[Y; ν]
Module: Mathlib.MeasureTheory.Function.ConvergenceInDistribution

Goal state before:
pp: ι : Type u_1
E : Type u_2
Ω' : Type u_3
Ω : ι → Type u_5
m : (i : ι) → MeasurableSpace (Ω i)
μ : (i : ι) → Measure (Ω i)
inst✝³ : ∀ (i : ι), IsProbabilityMeasure (μ i)
m' : MeasurableSpace Ω'
μ' : Measure Ω'
inst✝² : IsProbabilityMeasure μ'
mE : MeasurableSpace E
X : (i : ι) → Ω i → E
Z : Ω' → E
l : Filter ι
inst✝¹ : TopologicalSpace E
inst✝ : OpensMeasurableSpace E
i : ι
hX : ∀ (j : ι), IdentDistrib (X i) (X j) (μ i) (μ j)
hZ : IdentDistrib (X i) Z (μ i) μ'
⊢ Tendsto (fun n ↦ ⟨Measure.map (X n) (μ n), ⋯⟩) l (𝓝 ⟨Measure.map Z μ', ⋯⟩)

Tactic:
by
    convert! tendsto_const_nhds with j
    exact (hX j).map_eq.symm.trans hZ.map_eq

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

Goal state before:
pp: case h₂
ι : 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)‖) μ''
⊢ ∫ (a : Ω'') in {x | ε / 2 ≤ ‖Y n x - X n x‖}, ‖F (Y n a) - F (X n a)‖ ∂μ'' ≤
    ∫ (a : Ω'') in {x | ε / 2 ≤ ‖Y n x - X n x‖}, M ∂μ''

Tactic:
· refine setIntegral_mono h_int_sub.integrableOn integrableOn_const fun a ↦ ?_
        rw [← dist_eq_norm]
        convert!
          hF_bounded _
            _

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

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

Tactic:
have hf n : Measurable (f n) := by fun_prop (disch := exact hs _)

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

Goal state before:
pp: case hg.hg.hg
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
hR : 0 < R
f : ℂ → E
z w : ℂ
hf : ContinuousOn f (sphere z R)
hw : w ∈ ball z R
⊢ Continuous fun θ ↦ f (circleMap z R θ)

Tactic:
apply ContinuousOn.comp_continuous hf (continuous_circleMap z R)
    exact fun _ => (circleMap_mem_sphere _ hR.le) _

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

Goal state before:
pp: case h
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup β
μ : Measure α
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
f : ℕ → α → β
g : α → β
hf : ∀ (n : ℕ), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hg' : MemLp g p μ
hui : UnifIntegrable f p μ
hut : UnifTight f p μ
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (g x))
ε : ℝ≥0∞
hε : ε > 0
hfinε : ε ≠ ∞
hμ : μ ≠ 0
hε' : 0 < ε / 3
Eg : Set α
hmEg : MeasurableSet Eg
hμEg : μ Eg < ∞
hgε : eLpNorm (Egᶜ.indicator g) p μ < ε / 3
Ef : Set α
hmEf : MeasurableSet Ef
hμEf : μ Ef < ∞
hfε : ∀ (i : ℕ), eLpNorm (Efᶜ.indicator (f i)) p μ ≤ ε / 3
E : Set α := Ef ∪ Eg
hmE : MeasurableSet E
hfmE : μ E < ∞
hgE' : MemLp g p (μ.restrict E)
huiE : UnifIntegrable f p (μ.restrict E)
hfgE : ∀ᵐ (x : α) ∂μ.restrict E, Tendsto (fun n ↦ f n x) atTop (𝓝 (g x))
ffmE : Fact (μ E < ∞)
hInner : ∀ ε > 0, ∃ N, ∀ n ≥ N, eLpNorm (f n - g) p (μ.restrict E) ≤ ε
N : ℕ
hfngε : ∀ n ≥ N, eLpNorm (f n - g) p (μ.restrict E) ≤ ε / 3
n : ℕ
hn : n ≥ N
hmfngE : AEStronglyMeasurable (E.indicator (f n - g)) μ
hfngEε : eLpNorm (E.indicator (f n - g)) p μ ≤ ε / 3
hmgEc : AEStronglyMeasurable (Eᶜ.indicator g) μ
hgEcε : eLpNorm (Eᶜ.indicator g) p μ ≤ ε / 3
hmfnEc : AEStronglyMeasurable (Eᶜ.indicator (f n)) μ
hfnEcε : eLpNorm (Eᶜ.indicator (f n)) p μ ≤ ε / 3
hmfngEc : AEStronglyMeasurable (Eᶜ.indicator (f n - g)) μ
hfngEcε : eLpNorm (Eᶜ.indicator (f n - g)) p μ ≤ ε / 3 + ε / 3
⊢ eLpNorm (f n - g) p μ ≤ ε

Tactic:
calc
    eLpNorm (f n - g) p μ
      = eLpNorm (Eᶜ.indicator (f n - g) + E.indicator (f n - g)) p μ := by
        congr; exact (E.indicator_compl_add_self _).symm
    _ ≤ eLpNorm (indicator Eᶜ (f n - g)) p μ + eLpNorm (indicator E (f n - g)) p μ := by
        apply eLpNorm_add_le (by assumption) (by assumption) hp
    _ ≤ (ε / 3 + ε / 3) + ε / 3 := add_le_add hfngEcε hfngEε
    _ = ε := by simp only [ENNReal.add_thirds]

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 α
inst✝⁶ : TopologicalSpace β
x : α
R : Type u_5
inst✝⁵ : Semiring R
inst✝⁴ : NonUnitalNonAssocSemiring β
inst✝³ : IsTopologicalSemiring β
inst✝² : Module R β
inst✝¹ : ContinuousConstSMul R β
inst✝ : SMulCommClass R β β
r : R
f g : α →C_c β
⊢ r • f • g = f • r • g

Tactic:
ext
    simp only [smul_eq_mul, coe_smul, coe_mul, Pi.smul_apply, Pi.mul_apply]
    rw [← smul_eq_mul, ← smul_eq_mul, smul_comm]

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

Goal state before:
pp: α : Type u_2
inst✝ : TopologicalSpace α
r : ℝ≥0
f : α →C_c ℝ≥0
⊢ (r • f).toReal = r • f.toReal

Tactic:
by
  ext; simp [NNReal.smul_def]

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✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
a : E
s : Set E
ω : E → E →L[𝕜] F
hs : Convex ℝ s
hω : ∀ᶠ (x : E) in 𝓝[s] a, ContinuousWithinAt ω s x
ha : a ∈ s
⊢ HasFDerivWithinAt (fun x ↦ ∫ᶜ (x : E) in Path.segment a x, ω x) (ω a) s a

Tactic:
by
  /- Given `ε > 0`, take a number `δ > 0` such that `ω` is continuous on `ball a δ ∩ s`
  and `‖ω z - ω a‖ ≤ ε` on this set.
  Then for `b ∈ ball a δ ∩ s`, we have
  `‖(∫ᶜ x in .segment a b, ω x) - ω a (b - a)‖
    = ‖(∫ᶜ x in .segment a b, ω x) - ∫ᶜ x in .segment a b, ω a‖
    ≤ ∫ x in 0..1, ‖ω x - ω a‖ * ‖b - a‖
    ≤ ε * ‖b - a‖`
  -/
  simp only [hasFDerivWithinAt_iff_isLittleO, Path.segment_same, curveIntegral_refl, sub_zero,
    Asymptotics.isLittleO_iff]
  intro ε hε
  obtain ⟨δ, hδ₀, hδ⟩ : ∃ δ > 0,
      ball a δ ∩ s ⊆ {z | ContinuousWithinAt ω s z ∧ dist (ω z) (ω a) ≤ ε} := by
    rw [← Metric.mem_nhdsWithin_iff, ofPred_and, inter_mem_iff]
    exact ⟨hω, (hω.self_of_nhdsWithin ha).eventually <| closedBall_mem_nhds _ hε⟩
  rw [eventually_nhdsWithin_iff]
  filter_upwards [Metric.ball_mem_nhds _ hδ₀] with b hb hbs
  have hsub : [a -[ℝ] b] ⊆ ball a δ ∩ s :=
    ((convex_ball _ _).inter hs).segment_subset (by simp [*]) (by simp [*])
  rw [← curveIntegral_segment_const, ← curveIntegral_fun_sub]
  · refine norm_curveIntegral_segment_le fun z hz ↦ ?_
    simpa [dist_eq_norm] using (hδ (hsub hz)).2
  · rw [curveIntegrable_segment]
    refine ContinuousOn.intervalIntegrable_of_Icc zero_le_one fun t ht ↦ ?_
    refine ((hδ ?_).1.eval_const _).comp AffineMap.lineMap_continuous.continuousWithinAt ?_
    · exact hsub <| lineMap_mem_segment ℝ a b ht
    · rw [mapsTo_iff_image_subset, ← segment_eq_image_lineMap]
      exact hs.segment_subset ha hbs
  · rw [curveIntegrable_segment]
    exact intervalIntegrable_const

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

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
f : X →C_c ℝ
a ε : ℝ
hε : 0 < ε
N : ℕ
hf : range ⇑f ⊆ Ioo a (a + ↑N * ε)
b : ℝ := a + ↑N * ε
y : Fin N → ℝ := fun n ↦ a + ε * (↑↑n + 1)
hy : ∀ {n m : Fin N}, n < m → y n + ε ≤ y m
E : Fin N → Set X := fun n ↦ ⇑f ⁻¹' Ioc (y n - ε) (y n) ∩ tsupport ⇑f
⊢ range ⇑f ⊆ Ioc (a + ↑0 * ε) (a + ↑N * ε)

Tactic:
by
        intro _ hz
        simpa using Ioo_subset_Ioc_self (hf hz)

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

Goal state before:
pp: E : Type u_2
mE : MeasurableSpace E
μ : Measure E
inst✝² : SeminormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : BorelSpace E
r : ℝ
t : E
⊢ charFun (Measure.map (fun x ↦ r • x) μ) t = charFun μ (r • t)

Tactic:
rw [charFun_apply, charFun_apply,
    integral_map (by fun_prop) (by fun_prop)]

Goal state after:
E : Type u_2
mE : MeasurableSpace E
μ : Measure E
inst✝² : SeminormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : BorelSpace E
r : ℝ
t : E
⊢ ∫ (x : E), cexp (↑⟪r • x, t⟫ * I) ∂μ = ∫ (x : E), cexp (↑⟪x, r • t⟫ * I) ∂μ
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
inst✝³ : SecondCountableTopology E
inst✝² : CompleteSpace E
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h : ∀ (x : E), charFun μ x = charFun ν x
⊢ μ = ν

Tactic:
charFun_eq_integral_innerProbChar

Goal state after:
E : Type u_3
inst✝⁷ : MeasurableSpace E
μ ν : Measure E
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace ℝ E
inst✝⁴ : BorelSpace E
inst✝³ : SecondCountableTopology E
inst✝² : CompleteSpace E
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h : ∀ (x : E), ∫ (v : E), (innerProbChar x) v ∂μ = ∫ (v : E), (innerProbChar x) v ∂ν
⊢ μ = ν
Module: Mathlib.MeasureTheory.Integral.CurveIntegral.Poincare

Goal state before:
pp: case refine_1.a
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace ℝ F
a b c d : E
γ₁ : Path a b
γ₂ : Path c d
s : Set (↑I × ↑I)
t : Set E
ω : E → E →L[ℝ] F
dω : E → E →L[ℝ] E →L[ℝ] F
φ : (↑γ₁).Homotopy ↑γ₂
hs : s.Countable
hφt : ∀ a_1 ∈ Ioo 0 1, ∀ b_1 ∈ Ioo 0 1, φ (a_1, b_1) ∈ t
hω : ∀ a_1 ∈ Ioo 0 1, ∀ b_1 ∈ Ioo 0 1, (a_1, b_1) ∉ s → HasFDerivWithinAt ω (dω (φ (a_1, b_1))) t (φ (a_1, b_1))
hωc : ContinuousOn ω (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t)
hdω_symm :
  ∀ a_1 ∈ Ioo 0 1,
    ∀ b_1 ∈ Ioo 0 1,
      (a_1, b_1) ∉ s →
        ∀ u ∈ tangentConeAt ℝ t (φ (a_1, b_1)),
          ∀ v ∈ tangentConeAt ℝ t (φ (a_1, b_1)), ((dω (φ (a_1, b_1))) u) v = ((dω (φ (a_1, b_1))) v) u
U : Set (ℝ × ℝ) := ⋯
hU : U = Ioo 0 1 ×ˢ Ioo 0 1
hinterior : interior (Icc 0 1) = U
hunique : UniqueDiffOn ℝ (Icc 0 1)
hUopen : IsOpen U
hU_subset : U ⊆ Icc 0 1
hclosure : closure U = Icc 0 1
ψ : ℝ × ℝ → E := ⋯
hcontdiff : ContDiffOn ℝ 2 ψ (Icc 0 1)
hψ : ψ = fun xy ↦ Set.IccExtend ⋯ (⇑(φ.extend xy.1)) xy.2
hψφ : ∀ (a_1 b_1 : ↑I), ψ (↑a_1, ↑b_1) = φ (a_1, b_1)
hψ_cont : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ψ
hψUt : MapsTo ψ U t
dψ : ℝ × ℝ → ℝ × ℝ →L[ℝ] E := ⋯
s' : Set (ℝ × ℝ) := ⋯
hs' : s' = Prod.map Subtype.val Subtype.val '' s
hmem_s' : ∀ (x y : ↑I), (↑x, ↑y) ∈ s' ↔ (x, y) ∈ s
hs'c : s'.Countable
hdψ : ∀ a ∈ U, HasFDerivAt ψ (dψ a) a
d2ψ : ℝ × ℝ → ℝ × ℝ →L[ℝ] ℝ × ℝ →L[ℝ] E := ⋯
hd2ψ : ∀ a ∈ U, HasFDerivAt dψ (d2ψ a) a
hd2ψ_symm : ∀ a ∈ Icc 0 1, ∀ (x y : ℝ × ℝ), ((d2ψ a) x) y = ((d2ψ a) y) x
η : ℝ × ℝ → ℝ × ℝ →L[ℝ] F := ⋯
f : ℝ × ℝ → F := ⋯
hf : ∀ a ∈ Icc 0 1, f a = (ω (ψ a)) (derivWithin (ψ ∘ fun x ↦ (a.1, x)) I a.2)
g : ℝ × ℝ → F := ⋯
hg : ∀ a ∈ Icc 0 1, g a = (ω (ψ a)) (-derivWithin (ψ ∘ fun x ↦ (x, a.2)) I a.1)
dη : ℝ × ℝ → ℝ × ℝ →L[ℝ] ℝ × ℝ →L[ℝ] F := ⋯
x y : { x // x ∈ I }
haU : (↑x, ↑y) ∈ U
has : (↑x, ↑y) ∉ s'
⊢ projIcc 0 1 extend._proof_1 (↑x, ↑y).1 ∈ Ioo 0 1

Tactic:
simpa using haU.1

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

Goal state before:
pp: α : Type u_2
x✝¹ x✝ : LevyProkhorov α
μ ν : α
⊢ (ofMeasure μ).toMeasure = (ofMeasure ν).toMeasure → ofMeasure μ = ofMeasure ν

Tactic:
by congr!

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

Goal state before:

Tactic:
ball x.1 r ×ˢ ball x.2 r'
      _ ⊆ ball x.1 ε ×ˢ ball x.2 ε := by gcongr; exacts [hr.2.le, hr'.2.le]
      _ ⊆ _ := by rwa [ball_prod_same]

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

Goal state before:
pp: A : Type u_1
B : Type u_2
C : Type u_3
E : Type u_4
inst✝¹⁵ : Group A
inst✝¹⁴ : Group B
inst✝¹³ : Group C
inst✝¹² : TopologicalSpace A
inst✝¹¹ : TopologicalSpace B
inst✝¹⁰ : TopologicalSpace C
φ : A →* B
ψ : B →* C
H : IsSES φ ψ
inst✝⁹ : IsTopologicalGroup A
inst✝⁸ : IsTopologicalGroup B
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : MeasurableSpace A
inst✝⁵ : BorelSpace A
μA : Measure A
hμA : μA.IsHaarMeasure
inst✝⁴ : NormedSpace ℝ E
inst✝³ : IsTopologicalGroup C
inst✝² : LocallyCompactSpace B
inst✝¹ : MeasurableSpace C
inst✝ : BorelSpace C
μC : Measure C
hμC : μC.IsHaarMeasure
x : ℝ
f : CompactlySupportedContinuousMap B E
⊢ ∫ (c : C), ((H.pushforward μA) (x • f)) c ∂μC = (RingHom.id ℝ) x • ∫ (c : C), ((H.pushforward μA) f) c ∂μC

Tactic:
rw [map_smul]

Goal state after:
A : Type u_1
B : Type u_2
C : Type u_3
E : Type u_4
inst✝¹⁵ : Group A
inst✝¹⁴ : Group B
inst✝¹³ : Group C
inst✝¹² : TopologicalSpace A
inst✝¹¹ : TopologicalSpace B
inst✝¹⁰ : TopologicalSpace C
φ : A →* B
ψ : B →* C
H : IsSES φ ψ
inst✝⁹ : IsTopologicalGroup A
inst✝⁸ : IsTopologicalGroup B
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : MeasurableSpace A
inst✝⁵ : BorelSpace A
μA : Measure A
hμA : μA.IsHaarMeasure
inst✝⁴ : NormedSpace ℝ E
inst✝³ : IsTopologicalGroup C
inst✝² : LocallyCompactSpace B
inst✝¹ : MeasurableSpace C
inst✝ : BorelSpace C
μC : Measure C
hμC : μC.IsHaarMeasure
x : ℝ
f : CompactlySupportedContinuousMap B E
⊢ ∫ (c : C), (x • (H.pushforward μA) f) c ∂μC = (RingHom.id ℝ) x • ∫ (c : C), ((H.pushforward μA) f) c ∂μC