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

Goal state before:
pp: case mpr
Ω : Type u_1
β : Type u_6
β' : Type u_7
_mΩ : MeasurableSpace Ω
μ : Measure Ω
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
hf : AEMeasurable f μ
hg : AEMeasurable g μ
σf : SigmaFinite (Measure.map f μ)
σg : SigmaFinite (Measure.map g μ)
h₀ :
  ∀ {s : Set β} {t : Set β'},
    MeasurableSet s →
      MeasurableSet t →
        μ (f ⁻¹' s) * μ (g ⁻¹' t) = (Measure.map f μ) s * (Measure.map g μ) t ∧
          μ (f ⁻¹' s ∩ g ⁻¹' t) = (Measure.map (fun ω ↦ (f ω, g ω)) μ) (s ×ˢ t)
h : Measure.map (fun ω ↦ (f ω, g ω)) μ = (Measure.map f μ).prod (Measure.map g μ)
s : Set β
t : Set β'
hs : MeasurableSet s
ht : MeasurableSet t
⊢ μ (f ⁻¹' s ∩ g ⁻¹' t) = μ (f ⁻¹' s) * μ (g ⁻¹' t)

Tactic:
rw [(h₀ hs ht).1, (h₀ hs ht).2, h, Measure.prod_prod]

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

Goal state before:
pp: Ω : Type u_1
inst✝³ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
ι : Type u_2
μ : ProbabilityMeasure Ω
μs : ι → ProbabilityMeasure Ω
L : Filter ι
inst✝ : L.IsCountablyGenerated
h_opens : ∀ (G : Set Ω), IsOpen[inst✝²] G → μ G ≤ liminf (fun i ↦ (μs i) G) L
u : ℕ → ι
hu : Tendsto u atTop L
G : Set Ω
hG : IsOpen[inst✝²] G
⊢ IsBoundedUnder (fun x1 x2 ↦ x1 ≥ x2) L fun i ↦ (μs i) G

Tactic:
isBoundedDefault

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

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
mΩ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : ProbabilityMeasure Ω
μs : ι → ProbabilityMeasure Ω
L : Filter ι
inst✝ : L.IsCountablyGenerated
h : ∀ (F : Set Ω), IsClosed[inst✝²] F → limsup (fun i ↦ (μs i) F) L ≤ μ F
u : ℕ → ι
hu : Tendsto u atTop L
F : Set Ω
hF : IsClosed[inst✝²] F
⊢ IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) (map u atTop) fun i ↦ (μs i) F

Tactic:
isBoundedDefault

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

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
mΩ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : ProbabilityMeasure Ω
μs : ι → ProbabilityMeasure Ω
L : Filter ι
inst✝ : L.IsCountablyGenerated
h₁ : IsTightMeasureSet (range (ProbabilityMeasure.toMeasure ∘ μs))
h₂ : ∀ (F : Set Ω), IsCompact F → limsup (fun x ↦ (μs x) F) L ≤ μ F
h✝ : L.NeBot
F : Set Ω
hF_closed : IsClosed[inst✝²] F
ε : ℝ≥0
hε : 0 < ε
x✝ : ↑(μ F) < ∞
K : Set Ω
hKc : IsCompact K
hK_le : ∀ μ ∈ range (ProbabilityMeasure.toMeasure ∘ μs), μ Kᶜ ≤ ↑ε
⊢ IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) L fun i ↦ ↑((μs i) (F ∩ K))

Tactic:
isBoundedDefault

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

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
mΩ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : ProbabilityMeasure Ω
μs : ι → ProbabilityMeasure Ω
L : Filter ι
inst✝ : L.IsCountablyGenerated
h₁ : IsTightMeasureSet (range (ProbabilityMeasure.toMeasure ∘ μs))
h₂ : ∀ (F : Set Ω), IsCompact F → limsup (fun x ↦ (μs x) F) L ≤ μ F
h✝ : L.NeBot
F : Set Ω
hF_closed : IsClosed[inst✝²] F
ε : ℝ≥0
hε : 0 < ε
x✝ : ↑(μ F) < ∞
K : Set Ω
hKc : IsCompact K
hK_le : ∀ μ ∈ range (ProbabilityMeasure.toMeasure ∘ μs), μ Kᶜ ≤ ↑ε
⊢ IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) L fun i ↦ ↑((μs i) (F ∩ K))

Tactic:
isBoundedDefault

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

Goal state before:
pp: case hn
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m1 m2 m : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst✝ : IsZeroOrMarkovKernel κ
p1 p2 : Set (Set Ω)
h1 : m1 ≤ m
h2 : m2 ≤ m
hp1 : IsPiSystem p1
hp2 : IsPiSystem p2
hpm1 : m1 = generateFrom p1
hpm2 : m2 = generateFrom p2
hyp : IndepSets p1 p2 κ μ
h✝ : IsMarkovKernel κ
t1 t2 : Set Ω
ht2 : t2 ∈ {s | MeasurableSet s}
f : ℕ → Set Ω
hf_disj : Pairwise (Function.onFun Disjoint f)
hf_meas : ∀ (i : ℕ), MeasurableSet (f i)
h : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), (κ a) (f i ∩ t2) = (κ a) (f i) * (κ a) t2
a : α
ha : ∀ (i : ℕ), (κ a) (f i ∩ t2) = (κ a) (f i) * (κ a) t2
i j : ℕ
hij : i ≠ j
⊢ Disjoint (f i ∩ t2) (f j ∩ t2)

Tactic:
exact Disjoint.inter_left _ (Disjoint.inter_right _ (hf_disj hij))

Goal state after:
Module: Mathlib.Probability.Density

Goal state before:
pp: Ω : Type u_1
G : Type u_2
mΩ : MeasurableSpace Ω
ℙ : Measure Ω
inst✝⁷ : Group G
mG : MeasurableSpace G
inst✝⁶ : MeasurableMul₂ G
inst✝⁵ : MeasurableInv G
μ : Measure G
inst✝⁴ : μ.IsMulLeftInvariant
X Y : Ω → G
inst✝³ : SFinite μ
inst✝² : HasPDF X ℙ μ
inst✝¹ : HasPDF Y ℙ μ
inst✝ : IsFiniteMeasure ℙ
hXY : X ⟂ᵢ[ℙ] Y
⊢ (map X ℙ ∗ₘ map Y ℙ).rnDeriv μ =ᵐ[μ] pdf X ℙ μ ⋆ₘₗ[μ] pdf Y ℙ μ

Tactic:
apply rnDeriv_mconv <;> exact HasPDF.absolutelyContinuous

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

Goal state before:
pp: case indicator
Ω : Type u_1
Mf mΩ : MeasurableSpace Ω
μ : Measure Ω
hMf : Mf ≤ mΩ
c : ℝ≥0∞
T : Set Ω
h_meas_T : MeasurableSet T
h_ind : IndepSets {s | MeasurableSet s} {T} μ
h_mul_indicator : ∀ (g : Ω → ℝ≥0∞), Measurable g → Measurable fun a ↦ g a * T.indicator (fun x ↦ c) a
c' : ℝ≥0∞
s' : Set Ω
h_meas_s' : MeasurableSet s'
⊢ ∫⁻ (a : Ω) in s' ∩ T, c' * c ∂μ = (∫⁻ (a : Ω) in s', c' ∂μ) * ∫⁻ (ω : Ω), T.indicator (fun x ↦ c) ω ∂μ

Tactic:
lintegral_indicator h_meas_T

Goal state after:
case indicator
Ω : Type u_1
Mf mΩ : MeasurableSpace Ω
μ : Measure Ω
hMf : Mf ≤ mΩ
c : ℝ≥0∞
T : Set Ω
h_meas_T : MeasurableSet T
h_ind : IndepSets {s | MeasurableSet s} {T} μ
h_mul_indicator : ∀ (g : Ω → ℝ≥0∞), Measurable g → Measurable fun a ↦ g a * T.indicator (fun x ↦ c) a
c' : ℝ≥0∞
s' : Set Ω
h_meas_s' : MeasurableSet s'
⊢ ∫⁻ (a : Ω) in s' ∩ T, c' * c ∂μ = (∫⁻ (a : Ω) in s', c' ∂μ) * ∫⁻ (a : Ω) in T, c ∂μ
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Ω
π : ι → Set (Set Ω)
h_pi : ∀ (n : ι), IsPiSystem (π n)
h_generate : ∀ (i : ι), m i = generateFrom (π i)
h_ind : iIndepSets π κ μ
hμ : μ ≠ 0
η : Kernel α Ω
η_eq : ⇑κ =ᵐ[μ] ⇑η
hη : IsMarkovKernel η
s : Finset ι
f : ι → Set Ω
a : ι
S : Finset ι
ha_notin_S : a ∉ S
h_rec : (∀ i ∈ S, f i ∈ (fun x ↦ {s | MeasurableSet s}) i) → ∀ᵐ (a : α) ∂μ, (η a) (⋂ i ∈ S, f i) = ∏ i ∈ S, (η a) (f i)
hf_m : ∀ i ∈ insert a S, f i ∈ (fun x ↦ {s | MeasurableSet s}) i
hf_m_S : ∀ x ∈ S, MeasurableSet (f x)
p : Set (Set Ω) := piiUnionInter π ↑S
m_p : MeasurableSpace Ω := generateFrom p
hS_eq_generate : m_p = generateFrom p
h_indep : Indep m_p (m a) η μ
⊢ ∀ᵐ (a_1 : α) ∂μ, (η a_1) (⋂ i ∈ insert a S, f i) = ∏ i ∈ insert a S, (η a_1) (f i)

Tactic:
have h := h_indep.symm (f a) (⋂ n ∈ S, f n) (hf_m a (Finset.mem_insert_self a S)) ?_

Goal state after:
case inr.refine_2.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Ω
π : ι → Set (Set Ω)
h_pi : ∀ (n : ι), IsPiSystem (π n)
h_generate : ∀ (i : ι), m i = generateFrom (π i)
h_ind : iIndepSets π κ μ
hμ : μ ≠ 0
η : Kernel α Ω
η_eq : ⇑κ =ᵐ[μ] ⇑η
hη : IsMarkovKernel η
s : Finset ι
f : ι → Set Ω
a : ι
S : Finset ι
ha_notin_S : a ∉ S
h_rec : (∀ i ∈ S, f i ∈ (fun x ↦ {s | MeasurableSet s}) i) → ∀ᵐ (a : α) ∂μ, (η a) (⋂ i ∈ S, f i) = ∏ i ∈ S, (η a) (f i)
hf_m : ∀ i ∈ insert a S, f i ∈ (fun x ↦ {s | MeasurableSet s}) i
hf_m_S : ∀ x ∈ S, MeasurableSet (f x)
p : Set (Set Ω) := piiUnionInter π ↑S
m_p : MeasurableSpace Ω := generateFrom p
hS_eq_generate : m_p = generateFrom p
h_indep : Indep m_p (m a) η μ
h : ∀ᵐ (a_1 : α) ∂μ, (η a_1) (f a ∩ ⋂ n ∈ S, f n) = (η a_1) (f a) * (η a_1) (⋂ n ∈ S, f n)
⊢ ∀ᵐ (a_1 : α) ∂μ, (η a_1) (⋂ i ∈ insert a S, f i) = ∏ i ∈ insert a S, (η a_1) (f i)

case inr.refine_2.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Ω
π : ι → Set (Set Ω)
h_pi : ∀ (n : ι), IsPiSystem (π n)
h_generate : ∀ (i : ι), m i = generateFrom (π i)
h_ind : iIndepSets π κ μ
hμ : μ ≠ 0
η : Kernel α Ω
η_eq : ⇑κ =ᵐ[μ] ⇑η
hη : IsMarkovKernel η
s : Finset ι
f : ι → Set Ω
a : ι
S : Finset ι
ha_notin_S : a ∉ S
h_rec : (∀ i ∈ S, f i ∈ (fun x ↦ {s | MeasurableSet s}) i) → ∀ᵐ (a : α) ∂μ, (η a) (⋂ i ∈ S, f i) = ∏ i ∈ S, (η a) (f i)
hf_m : ∀ i ∈ insert a S, f i ∈ (fun x ↦ {s | MeasurableSet s}) i
hf_m_S : ∀ x ∈ S, MeasurableSet (f x)
p : Set (Set Ω) := piiUnionInter π ↑S
m_p : MeasurableSpace Ω := generateFrom p
hS_eq_generate : m_p = generateFrom p
h_indep : Indep m_p (m a) η μ
⊢ ⋂ n ∈ S, f n ∈ {s | MeasurableSet s}
Module: Mathlib.MeasureTheory.Measure.Portmanteau

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
inst✝⁴ : MeasurableSpace Ω
inst✝³ : TopologicalSpace Ω
inst✝² : SecondCountableTopology Ω
inst✝¹ : OpensMeasurableSpace Ω
S : Set (Set Ω)
hS : IsPiSystem S
μ : ι → ProbabilityMeasure Ω
ν : ProbabilityMeasure Ω
l : Filter ι
inst✝ : l.IsCountablyGenerated
hmeas : ∀ s ∈ S, MeasurableSet s
h : ∀ (u : Set Ω), IsOpen[inst✝³] u → ∀ x ∈ u, ∃ s ∈ S, s ∈ 𝓝 x ∧ s ⊆ u
h' : ∀ s ∈ S, Tendsto (fun i ↦ (μ i) s) l (𝓝 (ν s))
hl : l.NeBot
G : Set Ω
hG : IsOpen[inst✝³] G
⊢ IsBoundedUnder (fun x1 x2 ↦ x1 ≥ x2) l fun i ↦ (μ i) G

Tactic:
isBoundedDefault

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

Goal state before:
pp: case refine_1.compl
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m₁ m₂ x✝ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
h_indep : Indep m₁ m₂ κ μ
s t : Set Ω
hs : MeasurableSet s
ht : MeasurableSet t
s' t' : Set Ω
ht' : t' ∈ {s | MeasurableSet s}
u : Set Ω
ht✝ : MeasurableSet u
hu : u ∈ {s | MeasurableSet s}
⊢ uᶜ ∈ {s | MeasurableSet s}

Tactic:
| compl u _ hu =>

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

Goal state before:
pp: case refine_2.compl
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m₁ m₂ x✝ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
h_indep : Indep m₁ m₂ κ μ
s t : Set Ω
hs : MeasurableSet s
ht : MeasurableSet t
s' t' : Set Ω
hs' : s' ∈ {s_1 | MeasurableSet s_1}
u : Set Ω
ht✝ : MeasurableSet u
hu : u ∈ {s | MeasurableSet s}
⊢ uᶜ ∈ {s | MeasurableSet s}

Tactic:
| compl u _ hu =>

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

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
Y : Ω → ℝ
μ : Measure Ω
⊢ cov[0, Y; μ] = 0

Tactic:
by simp [covariance]

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

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
⊢ cov[X, 0; μ] = 0

Tactic:
by simp [covariance]

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

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
⊢ cov[X, Y; 0] = 0

Tactic:
by simp [covariance]

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

Goal state before:
pp: case pos
Ω : Type u_1
𝕜 : Type u_2
inst✝¹⁴ : RCLike 𝕜
mΩ : MeasurableSpace Ω
μ : Measure Ω
𝓧 : Type u_3
𝓨 : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
inst✝¹³ : MeasurableSpace 𝓧
inst✝¹² : MeasurableSpace 𝓨
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
inst✝⁹ : NormedSpace 𝕜 E
inst✝⁸ : CompleteSpace E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
inst✝⁵ : NormedSpace 𝕜 F
inst✝⁴ : CompleteSpace F
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace ℝ G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : CompleteSpace G
X : Ω → 𝓧
Y : Ω → 𝓨
f : 𝓧 → E
g : 𝓨 → F
hXY : X ⟂ᵢ[μ] Y
hX : AEMeasurable X μ
hY : AEMeasurable Y μ
hf : AEStronglyMeasurable f (Measure.map X μ)
hg : AEStronglyMeasurable g (Measure.map Y μ)
B : E →L[𝕜] F →L[𝕜] G
c : ℝ≥0
hc : c ≠ 0
hB : ∀ (x : E) (y : F), ↑c * ‖x‖ * ‖y‖ ≤ ‖(B x) y‖
this✝³ : MeasurableSpace E := borel E
this✝² : BorelSpace E
this✝¹ : MeasurableSpace F := borel F
this✝ : BorelSpace F
hfXgY : (f ∘ X) ⟂ᵢ[μ] g ∘ Y
hfX : AEStronglyMeasurable (f ∘ X) μ
hgY : AEStronglyMeasurable (g ∘ Y) μ
h'X : ∀ᵐ (ω : Ω) ∂μ, f (X ω) = 0
⊢ ∫ (ω : Ω), (B (f (X ω))) (g (Y ω)) ∂μ = (B (∫ (ω : Ω), f (X ω) ∂μ)) (∫ (ω : Ω), g (Y ω) ∂μ)

Tactic:
have h' : ∀ᵐ ω ∂μ, B (f (X ω)) (g (Y ω)) = 0 := by
      filter_upwards [h'X] with ω hω
      simp [hω]
    simp [integral_congr_ae h'X, integral_congr_ae h']

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

Goal state before:
pp: Ω : Type u_1
𝕜 : Type u_2
inst✝⁵ : RCLike 𝕜
mΩ : MeasurableSpace Ω
μ : Measure Ω
𝓧 : Type u_3
𝓨 : Type u_4
E : Type u_5
inst✝⁴ : MeasurableSpace 𝓧
inst✝³ : MeasurableSpace 𝓨
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace 𝕜 E
X : Ω → 𝓧
Y : Ω → 𝓨
f : 𝓧 → 𝕜
g : 𝓨 → E
hXY : X ⟂ᵢ[μ] Y
hX : AEMeasurable X μ
hY : AEMeasurable Y μ
hf : AEStronglyMeasurable f (Measure.map X μ)
hg : AEStronglyMeasurable g (Measure.map Y μ)
hE : CompleteSpace E
⊢ ∀ (x : 𝕜) (y : E), ↑1 * ‖x‖ * ‖y‖ ≤ ‖((ContinuousLinearMap.lsmul ℝ 𝕜) x) y‖

Tactic:
simp [norm_smul]

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

Goal state before:
pp: Ω : Type u_1
𝕜 : Type u_2
inst✝⁵ : RCLike 𝕜
mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_5
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
X : Ω → 𝕜
Y : Ω → E
hXY : X ⟂ᵢ[μ] Y
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
hE : CompleteSpace E
⊢ ∀ (x : 𝕜) (y : E), ↑1 * ‖x‖ * ‖y‖ ≤ ‖((ContinuousLinearMap.lsmul ℝ 𝕜) x) y‖

Tactic:
simp [norm_smul]

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
mY : MeasurableSpace Y
f : X → Y
g : X → Z
inst✝¹ : MeasurableSpace Z
inst✝ : MeasurableSingletonClass Z
hg : Measurable g
⊢ Function.FactorsThrough g f

Tactic:
refine fun x₁ x₂ h ↦ eq_of_mem_singleton ?_

Goal state after:
X : Type u_1
Y : Type u_2
Z : Type u_3
mY : MeasurableSpace Y
f : X → Y
g : X → Z
inst✝¹ : MeasurableSpace Z
inst✝ : MeasurableSingletonClass Z
hg : Measurable g
x₁ x₂ : X
h : f x₁ = f x₂
⊢ g x₁ ∈ {g x₂}
Module: Mathlib.Probability.Independence.Kernel.IndepFun

Goal state before:
pp: α : Type u_1
Ω : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
β : Type u_8
m : MeasurableSpace β
inst✝¹ : CommMonoid β
inst✝ : MeasurableMul₂ β
f : ι → Ω → β
hf_Indep : iIndepFun f κ μ
hf_meas : ∀ (i : ι), AEMeasurable (f i) (⇑κ ∘ₘ μ)
s : Finset ι
i : ι
hi : i ∉ s
⊢ IndepFun (∏ j ∈ s, f j) (f i) κ μ

Tactic:
have h : IndepFun (∏ j ∈ s, (hf_meas j).mk (f j)) ((hf_meas i).mk (f i)) κ μ := by
    refine iIndepFun.indepFun_finsetProd_of_notMem ?_ (fun i ↦ (hf_meas i).measurable_mk) hi
    exact iIndepFun.congr' hf_Indep fun i ↦ Measure.ae_ae_of_ae_comp (hf_meas i).ae_eq_mk
  refine IndepFun.congr' h ?_ ?_
  · have : ∀ᵐ a ∂μ, ∀ (i : s), f i =ᵐ[κ a] (hf_meas i).mk := by
      rw [ae_all_iff]
      exact fun i ↦ Measure.ae_ae_of_ae_comp (hf_meas i).ae_eq_mk
    filter_upwards [this] with a ha
    filter_upwards [ae_all_iff.2 ha] with ω hω
    simp only [Finset.prod_apply]
    exact Finset.prod_congr rfl fun i hi ↦ (hω ⟨i, hi⟩).symm
  · exact Measure.ae_ae_of_ae_comp (hf_meas i).ae_eq_mk.symm

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
⊢ Measurable Int.fract

Tactic:
by
  intro s hs
  rw [Int.preimage_fract]
  exact MeasurableSet.iUnion fun z => measurable_id.sub_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 j : ι
hij : i ≤ j
h_nonempty : s.Nonempty
f : Filtration ι m
hf_mem : f ∈ s
⊢ sInf ((fun f ↦ ↑f i) '' s) ≤ ↑f i

Tactic:
have hfi_mem : f i ∈ (fun g : Filtration ι m => g i) '' s := ⟨f, hf_mem, rfl⟩

Goal state after:
case pos
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝ : Preorder ι
s : Set (Filtration ι m)
i j : ι
hij : i ≤ j
h_nonempty : s.Nonempty
f : Filtration ι m
hf_mem : f ∈ s
hfi_mem : ↑f i ∈ (fun g ↦ ↑g i) '' s
⊢ sInf ((fun f ↦ ↑f i) '' s) ≤ ↑f i
Module: Mathlib.Probability.Process.Filtration

Goal state before:
pp: case pos
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝ : PartialOrder ι
𝓕 : Filtration ι m
this✝ : TopologicalSpace ι := Preorder.topology ι
this : OrderTopology ι
i : ι
hne : (𝓝[>] i).NeBot
⊢ ↑𝓕 i ≤ ↑𝓕₊ i

Tactic:
rightCont_eq_of_neBot_nhdsGT

Goal state after:
case pos
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝ : PartialOrder ι
𝓕 : Filtration ι m
this✝ : TopologicalSpace ι := Preorder.topology ι
this : OrderTopology ι
i : ι
hne : (𝓝[>] i).NeBot
⊢ ↑𝓕 i ≤ ⨅ j, ⨅ (_ : j > i), ↑𝓕 j
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)

Goal state after:
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
⊢ ∀ (x : ℝ), circleMap z R x ∈ sphere z R
Module: Mathlib.MeasureTheory.Function.UnifTight

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup β
μ : Measure α
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
f : ℕ → α → β
g : α → β
haef : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hg' : MemLp g p μ
hui : UnifIntegrable f p μ
hut : UnifTight f p μ
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (g x))
hf : ∀ (n : ℕ), StronglyMeasurable (AEStronglyMeasurable.mk (f n) ⋯)
hff' : ∀ (n : ℕ), f n =ᵐ[μ] AEStronglyMeasurable.mk (f n) ⋯
⊢ Tendsto (fun n ↦ eLpNorm (f n - g) p μ) atTop (𝓝 0)

Tactic:
have hui' := hui.ae_eq hff'

Goal state after:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup β
μ : Measure α
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
f : ℕ → α → β
g : α → β
haef : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hg' : MemLp g p μ
hui : UnifIntegrable f p μ
hut : UnifTight f p μ
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (g x))
hf : ∀ (n : ℕ), StronglyMeasurable (AEStronglyMeasurable.mk (f n) ⋯)
hff' : ∀ (n : ℕ), f n =ᵐ[μ] AEStronglyMeasurable.mk (f n) ⋯
hui' : UnifIntegrable (fun n ↦ AEStronglyMeasurable.mk (f n) ⋯) p μ
⊢ Tendsto (fun n ↦ eLpNorm (f n - g) p μ) atTop (𝓝 0)
Module: Mathlib.MeasureTheory.Integral.Gamma

Goal state before:
pp: p q : ℝ
hp : 1 ≤ p
hq : -2 < q
⊢ 2 * π * (1 / p * Real.Gamma ((q + 1 + 1) / p)) = 2 * π / p * Real.Gamma ((q + 2) / p)

Tactic:
add_assoc,

Goal state after:
p q : ℝ
hp : 1 ≤ p
hq : -2 < q
⊢ 2 * π * (1 / p * Real.Gamma ((q + (1 + 1)) / p)) = 2 * π / p * Real.Gamma ((q + 2) / p)
Module: Mathlib.MeasureTheory.Integral.Gamma

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

Tactic:
add_assoc,

Goal state after:
p q b : ℝ
hp : 1 ≤ p
hq : -2 < q
hb : 0 < b
⊢ 2 * π * (b ^ (-(q + (1 + 1)) / p) * (1 / p) * Real.Gamma ((q + (1 + 1)) / p)) =
    2 * π / p * b ^ (-(q + 2) / p) * Real.Gamma ((q + 2) / p)
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
hBi : IntervalIntegrable B volume a b
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
hfc : ContinuousOn f (Icc a b)
hfd : DifferentiableOn ℝ f (Ioo a b)
hfB : ∀ᵐ (t : ℝ), t ∈ Ioo a b → ‖deriv f t‖ ≤ B t
hE : CompleteSpace E
hfB' : (fun x ↦ ‖deriv f x‖) ≤ᵐ[volume.restrict (uIoc a b)] B
⊢ ‖∫ (y : ℝ) in a..b, deriv f y‖ ≤ ∫ (t : ℝ) in a..b, B t

Tactic:
apply intervalIntegral.norm_integral_le_of_norm_le hab _ hBi
    rwa [← ae_restrict_iff' measurableSet_Ioc, ← uIoc_of_le hab]

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

Goal state before:
pp: f : ℝ → ℝ
N : ℕ
a h : ℝ
N_nonzero : 0 < N
h_f_int : IntervalIntegrable f volume a (a + ↑N * h)
⊢ ∑ i ∈ Finset.range N, trapezoidal_error f 1 (a + ↑i * h) (a + (↑i + 1) * h) = trapezoidal_error f N a (a + ↑N * h)

Tactic:
unfold trapezoidal_error
  rw [sum_sub_distrib, sum_trapezoidal_integral_adjacent_intervals N_nonzero]
  norm_cast
  rw [sum_integral_adjacent_intervals]
  · simp
  · intro k hk
    suffices ∀ {k : ℕ}, k ≤ N → a + k * h ∈ [[a, a + N * h]] from
      IntervalIntegrable.mono h_f_int (Set.uIcc_subset_uIcc (this hk.le) (this hk)) le_rfl
    rcases le_total h 0 with h_neg | h_pos <;> intro k hk <;> rw [← Nat.cast_le (α := ℝ)] at hk
    · simpa [Set.mem_uIcc] using .inr
        ⟨mul_le_mul_of_nonpos_right hk h_neg, mul_nonpos_of_nonneg_of_nonpos k.cast_nonneg h_neg⟩
    · exact Set.mem_uIcc_of_le (le_add_of_nonneg_right (by positivity)) (by grw [hk])

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

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
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
⊢ rieszContentAux Λ K1 + ε / 2 + (rieszContentAux Λ K2 + ε / 2) = rieszContentAux Λ K1 + rieszContentAux Λ K2 + ε

Tactic:
add_assoc,

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
⊢ rieszContentAux Λ K1 + (ε / 2 + (rieszContentAux Λ K2 + ε / 2)) = rieszContentAux Λ K1 + rieszContentAux Λ K2 + ε
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
⊢ rieszContentAux Λ K1 + (rieszContentAux Λ K2 + ε / 2 + ε / 2) = rieszContentAux Λ K1 + rieszContentAux Λ K2 + ε

Tactic:
add_assoc,

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
⊢ rieszContentAux Λ K1 + (rieszContentAux Λ K2 + (ε / 2 + ε / 2)) = rieszContentAux Λ K1 + rieszContentAux Λ K2 + ε
Module: Mathlib.MeasureTheory.Integral.TorusIntegral

Goal state before:
pp: n : ℕ
E : Type u_1
inst✝ : NormedAddCommGroup E
f : (Fin n → ℂ) → E
c : Fin n → ℂ
⊢ IntegrableOn (fun θ ↦ f (const (Fin n → ℝ) c θ)) (Icc 0 fun x ↦ 2 * π) volume

Tactic:
apply torusIntegrable_const (f c) c 0

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

Goal state before:
pp: case refine_2
n : ℕ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
f : (Fin n → ℂ) → E
c : Fin n → ℂ
R : Fin n → ℝ
inst✝ : NormedSpace ℂ E
hf : TorusIntegrable f c R
⊢ ∀ᵐ (a : Fin n → ℝ) ∂volume.restrict (Icc 0 fun x ↦ 2 * π),
    ‖(∏ i, ↑(R i) * cexp (↑(a i) * I) * I) • f (torusMap c R a)‖ ≤ (∏ i, |R i|) * ‖f (torusMap c R a)‖

Tactic:
simp [norm_smul]

Goal state after: