mathlib-initiative/mathlib-tactics huggingface dataset:
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✝³ : PartialOrder E
inst✝² : ClosedIciTopology E
inst✝¹ : IsOrderedAddMonoid E
inst✝ : IsOrderedModule ℝ E
f : α → E
c : E
hc : 0 ≤ c
hfc : ∀ᵐ (x : α) ∂μ, f x ≤ c
hm : m ≤ m0
hfint : Integrable f μ
hsig : SigmaFinite (μ.trim hm)
n : ℕ
h1 : (μ.restrict (spanningSets (μ.trim hm) n))[f | m] =ᵐ[μ.restrict (spanningSets (μ.trim hm) n)] μ[f | m]
h2 :
  (μ.restrict (spanningSets (μ.trim hm) n))[f | m] ≤ᵐ[μ.restrict (spanningSets (μ.trim hm) n)]
    (μ.restrict (spanningSets (μ.trim hm) n))[fun x ↦ c | m]
a : α
⊢ (μ.restrict (spanningSets (μ.trim hm) n))[f | m] a = μ[f | m] a →
    (μ.restrict (spanningSets (μ.trim hm) n))[f | m] a ≤ (μ.restrict (spanningSets (μ.trim hm) n))[fun x ↦ c | m] a →
      μ[f | m] a ≤ c

Tactic:
ha

Goal state after:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : PartialOrder E
inst✝² : ClosedIciTopology E
inst✝¹ : IsOrderedAddMonoid E
inst✝ : IsOrderedModule ℝ E
f : α → E
c : E
hc : 0 ≤ c
hfc : ∀ᵐ (x : α) ∂μ, f x ≤ c
hm : m ≤ m0
hfint : Integrable f μ
hsig : SigmaFinite (μ.trim hm)
n : ℕ
h1 : (μ.restrict (spanningSets (μ.trim hm) n))[f | m] =ᵐ[μ.restrict (spanningSets (μ.trim hm) n)] μ[f | m]
h2 :
  (μ.restrict (spanningSets (μ.trim hm) n))[f | m] ≤ᵐ[μ.restrict (spanningSets (μ.trim hm) n)]
    (μ.restrict (spanningSets (μ.trim hm) n))[fun x ↦ c | m]
a : α
ha : (μ.restrict (spanningSets (μ.trim hm) n))[f | m] a = μ[f | m] a
⊢ (μ.restrict (spanningSets (μ.trim hm) n))[f | m] a ≤ (μ.restrict (spanningSets (μ.trim hm) n))[fun x ↦ c | m] a →
    μ[f | m] a ≤ c
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 : α
⊢ μ[f | m] a ≤ μ[fun a ↦ |f a| | m] a →
    μ[-f | m] a ≤ μ[fun a ↦ |f a| | m] a → μ[-f | m] a = (-μ[f | m]) a → |μ[f | m]| a ≤ μ[|f| | m] a

Tactic:
ha

Goal state after:
α : 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
⊢ μ[-f | m] a ≤ μ[fun a ↦ |f a| | m] a → μ[-f | m] a = (-μ[f | m]) a → |μ[f | m]| a ≤ μ[|f| | m] a
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real

Goal state before:
pp: case pos
α : 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
hm : m ≤ m0
hsig : ¬SigmaFinite (μ.trim hm)
⊢ ∫ (x : α), |μ[f | m] x| ∂μ ≤ ∫ (x : α), |f x| ∂μ

pp: case neg
α : 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
hm : m ≤ m0
hsig : SigmaFinite (μ.trim hm)
⊢ ∫ (x : α), |μ[f | m] x| ∂μ ≤ ∫ (x : α), |f x| ∂μ

Tactic:
· simpa [condExp_of_not_sigmaFinite hm hsig] using integral_nonneg (fun x => abs_nonneg f x)

Goal state after:
case neg
α : 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
hm : m ≤ m0
hsig : SigmaFinite (μ.trim hm)
⊢ ∫ (x : α), |μ[f | m] x| ∂μ ≤ ∫ (x : α), |f x| ∂μ
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real

Goal state before:
pp: case pos
α : 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
s : Set α
hs : MeasurableSet s
f : α → E
hm : m ≤ m0
hfint : Integrable f μ
hsig : ¬SigmaFinite (μ.trim hm)
⊢ ∫ (x : α) in s, |μ[f | m] x| ∂μ ≤ ∫ (x : α) in s, |f x| ∂μ

pp: case neg
α : 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
s : Set α
hs : MeasurableSet s
f : α → E
hm : m ≤ m0
hfint : Integrable f μ
hsig : SigmaFinite (μ.trim hm)
⊢ ∫ (x : α) in s, |μ[f | m] x| ∂μ ≤ ∫ (x : α) in s, |f x| ∂μ

Tactic:
· simpa [condExp_of_not_sigmaFinite hm hsig] using integral_nonneg (fun x => abs_nonneg f x)

Goal state after:
case neg
α : 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
s : Set α
hs : MeasurableSet s
f : α → E
hm : m ≤ m0
hfint : Integrable f μ
hsig : SigmaFinite (μ.trim hm)
⊢ ∫ (x : α) in s, |μ[f | m] x| ∂μ ≤ ∫ (x : α) in s, |f x| ∂μ
Module: Mathlib.MeasureTheory.Measure.HasOuterApproxClosed

Goal state before:
pp: case h_univ
Ω : Type u_1
inst✝⁴ : MeasurableSpace Ω
inst✝³ : TopologicalSpace Ω
inst✝² : HasOuterApproxClosed Ω
inst✝¹ : BorelSpace Ω
μ ν : Measure Ω
inst✝ : IsFiniteMeasure μ
h : ∀ (f : Ω →ᵇ ℝ≥0), ∫⁻ (x : Ω), ↑(f x) ∂μ = ∫⁻ (x : Ω), ↑(f x) ∂ν
key : ∀ {F : Set Ω}, IsClosed[inst✝³] F → μ F = ν F
⊢ μ univ = ν univ

Tactic:
exact key isClosed_univ

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

Goal state before:
pp: Ω : Type u_1
inst✝ : MeasurableSpace Ω
ι : Type u_3
μ : FiniteMeasure Ω
T : Finset ι
s : ι → Set Ω
hd : (↑T).Pairwise (Disjoint on s)
hm : ∀ (i : ι), MeasurableSet (s i)
t : Set Ω
ht : MeasurableSet t
⊢ ((↑μ).restrict (⋃ i ∈ T, s i)) t = ∑ c ∈ T, ((↑μ).restrict (s c)) t

Tactic:
rw [Measure.restrict_biUnion_finset hd hm]

Goal state after:
Ω : Type u_1
inst✝ : MeasurableSpace Ω
ι : Type u_3
μ : FiniteMeasure Ω
T : Finset ι
s : ι → Set Ω
hd : (↑T).Pairwise (Disjoint on s)
hm : ∀ (i : ι), MeasurableSet (s i)
t : Set Ω
ht : MeasurableSet t
⊢ (Measure.sum fun i ↦ (↑μ).restrict (s ↑i)) t = ∑ c ∈ T, ((↑μ).restrict (s c)) t
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∞
κ : Type u_4
u : Filter κ
inst✝¹ : u.NeBot
inst✝ : u.IsCountablyGenerated
fn : ι → α → β
hUI : UnifIntegrable fn p μ
hfn : ∀ (i : ι), AEStronglyMeasurable (fn i) μ
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδ' :
  ∀ (i : ι) (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (fn i)) p μ ≤ ENNReal.ofReal ε
x✝ : ↑{g | ∃ ni, ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ fn (ni n) x) u (𝓝 (g x))}
t : Set α
ht : MeasurableSet t
ht' : μ t ≤ ENNReal.ofReal δ
f : α → β
s : κ → ι
hs : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ fn (s n) x) u (𝓝 (f x))
a : α
⊢ Tendsto (fun n ↦ fn (s n) a) u (𝓝 (f a)) → Tendsto (fun x ↦ t.indicator (fn (s x)) a) u (𝓝 (t.indicator f a))

Tactic:
ha

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup β
p : ℝ≥0∞
κ : Type u_4
u : Filter κ
inst✝¹ : u.NeBot
inst✝ : u.IsCountablyGenerated
fn : ι → α → β
hUI : UnifIntegrable fn p μ
hfn : ∀ (i : ι), AEStronglyMeasurable (fn i) μ
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδ' :
  ∀ (i : ι) (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (fn i)) p μ ≤ ENNReal.ofReal ε
x✝ : ↑{g | ∃ ni, ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ fn (ni n) x) u (𝓝 (g x))}
t : Set α
ht : MeasurableSet t
ht' : μ t ≤ ENNReal.ofReal δ
f : α → β
s : κ → ι
hs : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ fn (s n) x) u (𝓝 (f x))
a : α
ha : Tendsto (fun n ↦ fn (s n) a) u (𝓝 (f a))
⊢ Tendsto (fun x ↦ t.indicator (fn (s x)) a) u (𝓝 (t.indicator f a))
Module: Mathlib.MeasureTheory.Measure.FiniteMeasure

Goal state before:

Tactic:
f ω
     _ ≤ g ω + nndist (f ω) (g ω) := NNReal.le_add_nndist (f ω) (g ω)
     _ ≤ g ω + nndist f g := (add_le_add_iff_left (g ω)).mpr (le_dist ω)

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

Goal state before:
pp: case pos
α : 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 ≠ ∞
val✝ : Fintype ι
hι : Nonempty ι
h✝ : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hf : ∀ (i : ι), eLpNorm (f i) p μ < ∞
C : ℝ≥0∞ := (Finset.image (fun i ↦ eLpNorm (f i) p μ) Finset.univ).max' ⋯
⊢ ∃ C, ∀ (i : ι), eLpNorm (f i) p μ ≤ ↑C

Tactic:
refine ⟨C.toNNReal, fun i => ?_⟩

Goal state after:
case pos
α : 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 ≠ ∞
val✝ : Fintype ι
hι : Nonempty ι
h✝ : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hf : ∀ (i : ι), eLpNorm (f i) p μ < ∞
C : ℝ≥0∞ := (Finset.image (fun i ↦ eLpNorm (f i) p μ) Finset.univ).max' ⋯
i : ι
⊢ eLpNorm (f i) p μ ≤ ↑C.toNNReal
Module: Mathlib.MeasureTheory.Function.UniformIntegrable

Goal state before:
pp: case pos
α : 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 ≠ ∞
val✝ : Fintype ι
hι : Nonempty ι
h✝ : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hf : ∀ (i : ι), eLpNorm (f i) p μ < ∞
C : ℝ≥0∞ := (Finset.image (fun i ↦ eLpNorm (f i) p μ) Finset.univ).max' ⋯
i : ι
y : ℝ≥0∞
hy : ∃ a ∈ Finset.univ, eLpNorm (f a) p μ = y
⊢ y < ∞

Tactic:
obtain ⟨i, -, rfl⟩ := hy

Goal state after:
case pos
α : 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 ≠ ∞
val✝ : Fintype ι
hι : Nonempty ι
h✝ : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hf : ∀ (i : ι), eLpNorm (f i) p μ < ∞
C : ℝ≥0∞ := (Finset.image (fun i ↦ eLpNorm (f i) p μ) Finset.univ).max' ⋯
i✝ i : ι
⊢ eLpNorm (f i) p μ < ∞
Module: Mathlib.MeasureTheory.Function.UniformIntegrable

Goal state before:
pp: case pos
α : 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 ≠ ∞
val✝ : Fintype ι
hι : Nonempty ι
h✝ : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hf : ∀ (i : ι), eLpNorm (f i) p μ < ∞
C : ℝ≥0∞ := (Finset.image (fun i ↦ eLpNorm (f i) p μ) Finset.univ).max' ⋯
i : ι
⊢ C ≠ ∞

Tactic:
· refine ne_of_lt ((Finset.max'_lt_iff _ _).2 fun y hy => ?_)
      rw [Finset.mem_image] at hy
      obtain ⟨i, -, rfl⟩ := hy
      exact hf i

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

Goal state before:
pp: case pos
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : α → E
p : ℝ≥0∞
hp : 1 ≤ p
hf : MemLp f p μ
h✝ : NeZero μ
hp' : 0 < p
hm : m ≤ m0
hsig : SigmaFinite (μ.trim hm)
hpt : p ≠ ∞
⊢ lpNorm μ[f | m] p μ ≤ lpNorm f p μ

Tactic:
lpNorm_eq_integral_norm_rpow_toReal hp'.ne.symm hpt hf.1,

Goal state after:
case pos
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : α → E
p : ℝ≥0∞
hp : 1 ≤ p
hf : MemLp f p μ
h✝ : NeZero μ
hp' : 0 < p
hm : m ≤ m0
hsig : SigmaFinite (μ.trim hm)
hpt : p ≠ ∞
⊢ lpNorm μ[f | m] p μ ≤ (∫ (x : α), ‖f x‖ ^ p.toReal ∂μ) ^ p.toReal⁻¹
Module: Mathlib.MeasureTheory.Measure.FiniteMeasure

Goal state before:
pp: Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
γ : Type u_2
F : Filter γ
μs : γ → FiniteMeasure Ω
μ : FiniteMeasure Ω
h : ∀ (f : Ω →ᵇ ℝ≥0), Tendsto (fun i ↦ ∫⁻ (x : Ω), ↑(f x) ∂↑(μs i)) F (𝓝 (∫⁻ (x : Ω), ↑(f x) ∂↑μ))
f : Ω →ᵇ ℝ
f_pos : Ω →ᵇ ℝ≥0 := f.nnrealPart
_def_f_pos : f_pos = f.nnrealPart
f_neg : Ω →ᵇ ℝ≥0 := (-f).nnrealPart
_def_f_neg : f_neg = (-f).nnrealPart
tends_pos : Tendsto (ENNReal.toReal ∘ fun i ↦ ∫⁻ (x : Ω), ↑(f_pos x) ∂↑(μs i)) F (𝓝 (∫⁻ (x : Ω), ↑(f_pos x) ∂↑μ).toReal)
tends_neg : Tendsto (ENNReal.toReal ∘ fun i ↦ ∫⁻ (x : Ω), ↑(f_neg x) ∂↑(μs i)) F (𝓝 (∫⁻ (x : Ω), ↑(f_neg x) ∂↑μ).toReal)
⊢ Tendsto (fun i ↦ ∫ (x : Ω), ↑(f_pos x) ∂↑(μs i) - ∫ (x : Ω), ↑(f_neg x) ∂↑(μs i)) F
    (𝓝 (∫ (x : Ω), ↑(f_pos x) ∂↑μ - ∫ (x : Ω), ↑(f_neg x) ∂↑μ))

Tactic:
have aux :
    ∀ g : Ω →ᵇ ℝ≥0,
      (ENNReal.toReal ∘ fun i : γ ↦ ∫⁻ x : Ω, ↑(g x) ∂(μs i : Measure Ω)) =
        fun i : γ ↦ (∫⁻ x : Ω, ↑(g x) ∂(μs i : Measure Ω)).toReal :=
    fun _ ↦ rfl

Goal state after:
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
γ : Type u_2
F : Filter γ
μs : γ → FiniteMeasure Ω
μ : FiniteMeasure Ω
h : ∀ (f : Ω →ᵇ ℝ≥0), Tendsto (fun i ↦ ∫⁻ (x : Ω), ↑(f x) ∂↑(μs i)) F (𝓝 (∫⁻ (x : Ω), ↑(f x) ∂↑μ))
f : Ω →ᵇ ℝ
f_pos : Ω →ᵇ ℝ≥0 := f.nnrealPart
_def_f_pos : f_pos = f.nnrealPart
f_neg : Ω →ᵇ ℝ≥0 := (-f).nnrealPart
_def_f_neg : f_neg = (-f).nnrealPart
tends_pos : Tendsto (ENNReal.toReal ∘ fun i ↦ ∫⁻ (x : Ω), ↑(f_pos x) ∂↑(μs i)) F (𝓝 (∫⁻ (x : Ω), ↑(f_pos x) ∂↑μ).toReal)
tends_neg : Tendsto (ENNReal.toReal ∘ fun i ↦ ∫⁻ (x : Ω), ↑(f_neg x) ∂↑(μs i)) F (𝓝 (∫⁻ (x : Ω), ↑(f_neg x) ∂↑μ).toReal)
aux :
  ∀ (g : Ω →ᵇ ℝ≥0),
    (ENNReal.toReal ∘ fun i ↦ ∫⁻ (x : Ω), ↑(g x) ∂↑(μs i)) = fun i ↦ (∫⁻ (x : Ω), ↑(g x) ∂↑(μs i)).toReal
⊢ Tendsto (fun i ↦ ∫ (x : Ω), ↑(f_pos x) ∂↑(μs i) - ∫ (x : Ω), ↑(f_neg x) ∂↑(μs i)) F
    (𝓝 (∫ (x : Ω), ↑(f_pos x) ∂↑μ - ∫ (x : Ω), ↑(f_neg x) ∂↑μ))
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 Ω)
h : ⇑κ =ᵐ[μ] ⇑η
a✝² : Finset ι
a✝¹ : ι → Set Ω
a✝ : ∀ i ∈ a✝², a✝¹ i ∈ π i
h' : ∀ᵐ (a : α) ∂μ, (κ a) (⋂ i ∈ a✝², a✝¹ i) = ∏ i ∈ a✝², (κ a) (a✝¹ i)
a : α
⊢ κ a = η a → (κ a) (⋂ i ∈ a✝², a✝¹ i) = ∏ i ∈ a✝², (κ a) (a✝¹ i) → (η a) (⋂ i ∈ a✝², a✝¹ i) = ∏ i ∈ a✝², (η a) (a✝¹ i)

Tactic:
ha

Goal state after:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ η : Kernel α Ω
μ : Measure α
π : ι → Set (Set Ω)
h : ⇑κ =ᵐ[μ] ⇑η
a✝² : Finset ι
a✝¹ : ι → Set Ω
a✝ : ∀ i ∈ a✝², a✝¹ i ∈ π i
h' : ∀ᵐ (a : α) ∂μ, (κ a) (⋂ i ∈ a✝², a✝¹ i) = ∏ i ∈ a✝², (κ a) (a✝¹ i)
a : α
ha : κ a = η a
⊢ (κ a) (⋂ i ∈ a✝², a✝¹ i) = ∏ i ∈ a✝², (κ a) (a✝¹ i) → (η a) (⋂ i ∈ a✝², a✝¹ i) = ∏ i ∈ a✝², (η a) (a✝¹ i)
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 Ω)
h : ⇑κ =ᵐ[μ] ⇑η
a✝² : Finset ι
a✝¹ : ι → Set Ω
a✝ : ∀ i ∈ a✝², a✝¹ i ∈ π i
h' : ∀ᵐ (a : α) ∂μ, (η a) (⋂ i ∈ a✝², a✝¹ i) = ∏ i ∈ a✝², (η a) (a✝¹ i)
a : α
⊢ κ a = η a → (η a) (⋂ i ∈ a✝², a✝¹ i) = ∏ i ∈ a✝², (η a) (a✝¹ i) → (κ a) (⋂ i ∈ a✝², a✝¹ i) = ∏ i ∈ a✝², (κ a) (a✝¹ i)

Tactic:
ha

Goal state after:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ η : Kernel α Ω
μ : Measure α
π : ι → Set (Set Ω)
h : ⇑κ =ᵐ[μ] ⇑η
a✝² : Finset ι
a✝¹ : ι → Set Ω
a✝ : ∀ i ∈ a✝², a✝¹ i ∈ π i
h' : ∀ᵐ (a : α) ∂μ, (η a) (⋂ i ∈ a✝², a✝¹ i) = ∏ i ∈ a✝², (η a) (a✝¹ i)
a : α
ha : κ a = η a
⊢ (η a) (⋂ i ∈ a✝², a✝¹ i) = ∏ i ∈ a✝², (η a) (a✝¹ i) → (κ a) (⋂ i ∈ a✝², a✝¹ i) = ∏ i ∈ a✝², (κ a) (a✝¹ i)
Module: Mathlib.Probability.Independence.Kernel.Indep

Goal state before:
pp: α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ η : Kernel α Ω
μ : Measure α
s1 s2 : Set (Set Ω)
h : ⇑κ =ᵐ[μ] ⇑η
a✝³ a✝² : Set Ω
a✝¹ : a✝³ ∈ s1
a✝ : a✝² ∈ s2
h' : ∀ᵐ (a : α) ∂μ, (κ a) (a✝³ ∩ a✝²) = (κ a) a✝³ * (κ a) a✝²
a : α
⊢ κ a = η a → (κ a) (a✝³ ∩ a✝²) = (κ a) a✝³ * (κ a) a✝² → (η a) (a✝³ ∩ a✝²) = (η a) a✝³ * (η a) a✝²

Tactic:
ha

Goal state after:
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ η : Kernel α Ω
μ : Measure α
s1 s2 : Set (Set Ω)
h : ⇑κ =ᵐ[μ] ⇑η
a✝³ a✝² : Set Ω
a✝¹ : a✝³ ∈ s1
a✝ : a✝² ∈ s2
h' : ∀ᵐ (a : α) ∂μ, (κ a) (a✝³ ∩ a✝²) = (κ a) a✝³ * (κ a) a✝²
a : α
ha : κ a = η a
⊢ (κ a) (a✝³ ∩ a✝²) = (κ a) a✝³ * (κ a) a✝² → (η a) (a✝³ ∩ a✝²) = (η a) a✝³ * (η a) a✝²
Module: Mathlib.Probability.Independence.Kernel.Indep

Goal state before:
pp: α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ η : Kernel α Ω
μ : Measure α
s1 s2 : Set (Set Ω)
h : ⇑κ =ᵐ[μ] ⇑η
a✝³ a✝² : Set Ω
a✝¹ : a✝³ ∈ s1
a✝ : a✝² ∈ s2
h' : ∀ᵐ (a : α) ∂μ, (η a) (a✝³ ∩ a✝²) = (η a) a✝³ * (η a) a✝²
a : α
⊢ κ a = η a → (η a) (a✝³ ∩ a✝²) = (η a) a✝³ * (η a) a✝² → (κ a) (a✝³ ∩ a✝²) = (κ a) a✝³ * (κ a) a✝²

Tactic:
ha

Goal state after:
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ η : Kernel α Ω
μ : Measure α
s1 s2 : Set (Set Ω)
h : ⇑κ =ᵐ[μ] ⇑η
a✝³ a✝² : Set Ω
a✝¹ : a✝³ ∈ s1
a✝ : a✝² ∈ s2
h' : ∀ᵐ (a : α) ∂μ, (η a) (a✝³ ∩ a✝²) = (η a) a✝³ * (η a) a✝²
a : α
ha : κ a = η a
⊢ (η a) (a✝³ ∩ a✝²) = (η a) a✝³ * (η a) a✝² → (κ a) (a✝³ ∩ a✝²) = (κ a) a✝³ * (κ a) a✝²
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 Ω)
h : iIndepSets π κ μ
a : α
⊢ (κ a) (⋂ i ∈ ∅, univ) = ∏ i ∈ ∅, (κ a) univ → IsProbabilityMeasure (κ a)

Tactic:
ha

Goal state after:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
π : ι → Set (Set Ω)
h : iIndepSets π κ μ
a : α
ha : (κ a) (⋂ i ∈ ∅, univ) = ∏ i ∈ ∅, (κ a) univ
⊢ IsProbabilityMeasure (κ a)
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 Ω)
s : ι → Set Ω
inst✝ : Fintype ι
h : iIndepSets π κ μ
hs : ∀ (i : ι), s i ∈ π i
a : α
⊢ (κ a) (⋂ i ∈ Finset.univ, s i) = ∏ i, (κ a) (s i) → (κ a) (⋂ i, s i) = ∏ i, (κ a) (s i)

Tactic:
ha

Goal state after:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
π : ι → Set (Set Ω)
s : ι → Set Ω
inst✝ : Fintype ι
h : iIndepSets π κ μ
hs : ∀ (i : ι), s i ∈ π i
a : α
ha : (κ a) (⋂ i ∈ Finset.univ, s i) = ∏ i, (κ a) (s i)
⊢ (κ a) (⋂ i, s i) = ∏ i, (κ a) (s i)
Module: Mathlib.Probability.Independence.Kernel.Indep

Goal state before:
pp: α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
m : ι → MeasurableSpace Ω
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
s : ι → Set Ω
inst✝ : Fintype ι
h : iIndep m κ μ
hs : ∀ (i : ι), MeasurableSet (s i)
a : α
⊢ (κ a) (⋂ i ∈ Finset.univ, s i) = ∏ i, (κ a) (s i) → (κ a) (⋂ i, s i) = ∏ i, (κ a) (s i)

Tactic:
ha

Goal state after:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
m : ι → MeasurableSpace Ω
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
s : ι → Set Ω
inst✝ : Fintype ι
h : iIndep m κ μ
hs : ∀ (i : ι), MeasurableSet (s i)
a : α
ha : (κ a) (⋂ i ∈ Finset.univ, s i) = ∏ i, (κ a) (s i)
⊢ (κ a) (⋂ i, s i) = ∏ i, (κ a) (s i)
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 Ω)
ι' : Type u_5
g : ι' → ι
hg : Function.Injective g
h : iIndepSets π κ μ
s : Finset ι'
f : ι' → Set Ω
hf : ∀ i ∈ s, f i ∈ (π ∘ g) i
f' : ι → Set Ω := Function.extend g f fun x ↦ ∅
f'_apply : ∀ (x : ι'), f' (g x) = f x
hf' : ∀ i ∈ Finset.image g s, f' i ∈ π i
a : α
⊢ (κ a) (⋂ i ∈ Finset.image g s, f' i) = ∏ i ∈ Finset.image g s, (κ a) (f' i) →
    (κ a) (⋂ i ∈ s, f i) = ∏ i ∈ s, (κ a) (f i)

Tactic:
ha

Goal state after:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
π : ι → Set (Set Ω)
ι' : Type u_5
g : ι' → ι
hg : Function.Injective g
h : iIndepSets π κ μ
s : Finset ι'
f : ι' → Set Ω
hf : ∀ i ∈ s, f i ∈ (π ∘ g) i
f' : ι → Set Ω := Function.extend g f fun x ↦ ∅
f'_apply : ∀ (x : ι'), f' (g x) = f x
hf' : ∀ i ∈ Finset.image g s, f' i ∈ π i
a : α
ha : (κ a) (⋂ i ∈ Finset.image g s, f' i) = ∏ i ∈ Finset.image g s, (κ a) (f' i)
⊢ (κ a) (⋂ i ∈ s, f i) = ∏ i ∈ s, (κ a) (f i)
Module: Mathlib.MeasureTheory.Measure.FiniteMeasure

Goal state before:
pp: case hf
Ω' : Type u_2
inst✝⁶ : MeasurableSpace Ω'
inst✝⁵ : TopologicalSpace Ω'
inst✝⁴ : BorelSpace Ω'
Ω : Type u_3
inst✝³ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : BorelSpace Ω
inst✝ : NormalSpace Ω'
f : Ω → Ω'
hf : IsClosedEmbedding f
M : Set (FiniteMeasure Ω') := {μ | μ (range f)ᶜ = 0}
A : IsEmbedding Subtype.val
μ : FiniteMeasure Ω
s : Set Ω
hs : MeasurableSet s
⊢ ∀ (s : Set Ω), MeasurableSet s → MeasurableSet (f '' s)

pp: case hs
Ω' : Type u_2
inst✝⁶ : MeasurableSpace Ω'
inst✝⁵ : TopologicalSpace Ω'
inst✝⁴ : BorelSpace Ω'
Ω : Type u_3
inst✝³ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : BorelSpace Ω
inst✝ : NormalSpace Ω'
f : Ω → Ω'
hf : IsClosedEmbedding f
M : Set (FiniteMeasure Ω') := {μ | μ (range f)ᶜ = 0}
A : IsEmbedding Subtype.val
μ : FiniteMeasure Ω
s : Set Ω
hs : MeasurableSet s
⊢ MeasurableSet s

Tactic:
· exact fun t ht ↦ hf.measurableEmbedding.measurableSet_image' ht

Goal state after:
case hs
Ω' : Type u_2
inst✝⁶ : MeasurableSpace Ω'
inst✝⁵ : TopologicalSpace Ω'
inst✝⁴ : BorelSpace Ω'
Ω : Type u_3
inst✝³ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : BorelSpace Ω
inst✝ : NormalSpace Ω'
f : Ω → Ω'
hf : IsClosedEmbedding f
M : Set (FiniteMeasure Ω') := {μ | μ (range f)ᶜ = 0}
A : IsEmbedding Subtype.val
μ : FiniteMeasure Ω
s : Set Ω
hs : MeasurableSet s
⊢ MeasurableSet s
Module: Mathlib.Probability.Independence.Kernel.Indep

Goal state before:
pp: α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
s₁ s₂ : Set (Set Ω)
h : IndepSets s₁ s₂ κ μ
t1 t2 : Set Ω
ht1 : t1 ∈ s₂
ht2 : t2 ∈ s₁
a : α
⊢ (κ a) (t2 ∩ t1) = (κ a) t2 * (κ a) t1 → (κ a) (t1 ∩ t2) = (κ a) t1 * (κ a) t2

Tactic:
ha

Goal state after:
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
s₁ s₂ : Set (Set Ω)
h : IndepSets s₁ s₂ κ μ
t1 t2 : Set Ω
ht1 : t1 ∈ s₂
ht2 : t2 ∈ s₁
a : α
ha : (κ a) (t2 ∩ t1) = (κ a) t2 * (κ a) t1
⊢ (κ a) (t1 ∩ t2) = (κ a) t1 * (κ a) t2