mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.PullOut

Goal state before:
pp: case neg
Ω : Type u_1
m mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace ℝ F
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace ℝ G
inst✝² : CompleteSpace G
B : F →L[ℝ] E →L[ℝ] G
inst✝¹ : CompleteSpace E
hm : m ≤ mΩ
inst✝ : IsFiniteMeasure μ
f : Ω → F
g : Ω → E
hf : StronglyMeasurable f
hg : Integrable g μ
c : ℝ
hf_bound : ∀ᵐ (ω : Ω) ∂μ, ‖f ω‖ ≤ c
fs : ℕ → SimpleFunc Ω F := hf.approxBounded c
hfs_tendsto : ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun x ↦ (fs x) ω) atTop (𝓝 (f ω))
hμ : ¬μ = 0
this : (ae μ).NeBot
hc : 0 ≤ c
hfs_bound : ∀ (n : ℕ) (ω : Ω), ‖(fs n) ω‖ ≤ c
⊢ μ[fun ω ↦ (B (f ω)) (g ω) | m] =ᵐ[μ] fun ω ↦ (B (f ω)) (μ[g | m] ω)

Tactic:
have : μ[fun ω ↦ B (f ω) (μ[g | m] ω) | m] = fun ω ↦ B (f ω) (μ[g | m] ω) := by
    refine condExp_of_stronglyMeasurable hm ?_ ?_
    · exact Continuous.comp_stronglyMeasurable (g := (fun z : F × E ↦ B z.1 z.2)) (by fun_prop)
        (hf.prodMk stronglyMeasurable_condExp)
    · exact B.integrable_of_bilin_of_bdd_left c (hf.mono hm).aestronglyMeasurable hf_bound
        integrable_condExp

Goal state after:
case neg
Ω : Type u_1
m mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace ℝ F
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace ℝ G
inst✝² : CompleteSpace G
B : F →L[ℝ] E →L[ℝ] G
inst✝¹ : CompleteSpace E
hm : m ≤ mΩ
inst✝ : IsFiniteMeasure μ
f : Ω → F
g : Ω → E
hf : StronglyMeasurable f
hg : Integrable g μ
c : ℝ
hf_bound : ∀ᵐ (ω : Ω) ∂μ, ‖f ω‖ ≤ c
fs : ℕ → SimpleFunc Ω F := hf.approxBounded c
hfs_tendsto : ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun x ↦ (fs x) ω) atTop (𝓝 (f ω))
hμ : ¬μ = 0
this✝ : (ae μ).NeBot
hc : 0 ≤ c
hfs_bound : ∀ (n : ℕ) (ω : Ω), ‖(fs n) ω‖ ≤ c
this : μ[fun ω ↦ (B (f ω)) (μ[g | m] ω) | m] = fun ω ↦ (B (f ω)) (μ[g | m] ω)
⊢ μ[fun ω ↦ (B (f ω)) (g ω) | m] =ᵐ[μ] fun ω ↦ (B (f ω)) (μ[g | m] ω)
Module: Mathlib.MeasureTheory.Covering.LiminfLimsup

Goal state before:
pp: case inr
α : Type u_1
inst✝⁵ : PseudoMetricSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : IsUnifLocDoublingMeasure μ
p : ℕ → Prop
s : ℕ → Set α
M : ℝ
hM : 0 < M
r₁ r₂ : ℕ → ℝ
hr : Tendsto r₁ atTop (𝓝[>] 0)
R₁ : ℕ → ℝ := fun i ↦ max 0 (r₁ i)
R₂ : ℕ → ℝ := fun i ↦ max 0 (r₂ i)
hRp : 0 ≤ R₁
hMr : ∀ᶠ (i : ℕ) in atTop, M * R₁ i ≤ R₂ i
hM' : M < 1
⊢ blimsup (fun i ↦ cthickening (max 0 (r₁ i)) (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (s i)))
      atTop p ≤ᵐ[μ]
    blimsup (fun i ↦ cthickening (max 0 (r₂ i)) (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (s i)))
      atTop p

Tactic:
have hs : ∀ i, IsClosed (closure (s i)) := fun i => isClosed_closure

Goal state after:
case inr
α : Type u_1
inst✝⁵ : PseudoMetricSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : IsUnifLocDoublingMeasure μ
p : ℕ → Prop
s : ℕ → Set α
M : ℝ
hM : 0 < M
r₁ r₂ : ℕ → ℝ
hr : Tendsto r₁ atTop (𝓝[>] 0)
R₁ : ℕ → ℝ := fun i ↦ max 0 (r₁ i)
R₂ : ℕ → ℝ := fun i ↦ max 0 (r₂ i)
hRp : 0 ≤ R₁
hMr : ∀ᶠ (i : ℕ) in atTop, M * R₁ i ≤ R₂ i
hM' : M < 1
hs :
  ∀ (i : ℕ),
    IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
      (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s i))
⊢ blimsup (fun i ↦ cthickening (max 0 (r₁ i)) (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (s i)))
      atTop p ≤ᵐ[μ]
    blimsup (fun i ↦ cthickening (max 0 (r₂ i)) (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (s i)))
      atTop p
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : TopologicalSpace M
inst✝¹ : T2Space M
inst✝ : ContinuousSub M
v : VectorMeasure α M
s : ℕ → Set α
hm : Antitone s
hs : ∀ (i : ℕ), MeasurableSet (s i)
I : ∀ (n : ℕ), v (s n) = v univ - v (s n)ᶜ
⊢ v (⋂ n, s n) = v univ - v (⋃ n, (s n)ᶜ)

Tactic:
rw [← of_compl (MeasurableSet.iUnion (fun n ↦ (hs n).compl))]

Goal state after:
α : Type u_1
m : MeasurableSpace α
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : TopologicalSpace M
inst✝¹ : T2Space M
inst✝ : ContinuousSub M
v : VectorMeasure α M
s : ℕ → Set α
hm : Antitone s
hs : ∀ (i : ℕ), MeasurableSet (s i)
I : ∀ (n : ℕ), v (s n) = v univ - v (s n)ᶜ
⊢ v (⋂ n, s n) = v (⋃ b, (s b)ᶜ)ᶜ
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
inst✝² : MeasurableSpace β
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
f : α → β
hf : ¬Measurable f
⊢ map 0 f = 0

Tactic:
· exact dif_neg hf

Goal state after:
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: case e'_6
α : Type u_1
β : Type u_2
m mα : MeasurableSpace α
inst✝² : MeasurableSpace β
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
v✝ v : VectorMeasure α M
i : Set α
hi : MeasurableSet i
f : ℕ → Set α
hf₁ : ∀ (i : ℕ), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
⊢ (if MeasurableSet (⋃ i, f i) then v (⋃ i_1, f i_1 ∩ i) else 0) = v (⋃ i_1, f i_1 ∩ i)

Tactic:
if_pos (MeasurableSet.iUnion hf₁)

Goal state after:
case e'_6
α : Type u_1
β : Type u_2
m mα : MeasurableSpace α
inst✝² : MeasurableSpace β
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
v✝ v : VectorMeasure α M
i : Set α
hi : MeasurableSet i
f : ℕ → Set α
hf₁ : ∀ (i : ℕ), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
⊢ v (⋃ i_1, f i_1 ∩ i) = v (⋃ i_1, f i_1 ∩ i)
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : MeasurableSpace α
j : JordanDecomposition α
S : Set α
hS₁ : MeasurableSet S
hS₂ : j.posPart S = 0
hS₃ : j.negPart Sᶜ = 0
A : Set α
hA : MeasurableSet A
hA₁ : A ⊆ Sᶜ
⊢ 0 A ≤ j.toSignedMeasure A

Tactic:
rw [toSignedMeasure, toSignedMeasure_sub_apply hA, measureReal_def (μ := j.negPart),
      show j.negPart A = 0 from nonpos_iff_eq_zero.1 (hS₃ ▸ measure_mono hA₁), ENNReal.toReal_zero,
      sub_zero]

Goal state after:
case refine_2
α : Type u_1
inst✝ : MeasurableSpace α
j : JordanDecomposition α
S : Set α
hS₁ : MeasurableSet S
hS₂ : j.posPart S = 0
hS₃ : j.negPart Sᶜ = 0
A : Set α
hA : MeasurableSet A
hA₁ : A ⊆ Sᶜ
⊢ 0 A ≤ j.posPart.real A
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan

Goal state before:
pp: case refine_1
α : Type u_1
inst✝ : MeasurableSpace α
s✝ s : SignedMeasure α
i : Set α := ⋯.choose
hi : MeasurableSet ⋯.choose ∧ 0 ≤[⋯.choose] s ∧ s ≤[⋯.chooseᶜ] 0
⊢ (s.toMeasureOfZeroLE i ⋯ ⋯) iᶜ = 0

Tactic:
rw [toMeasureOfZeroLE_apply _ _ hi.1 hi.1.compl]; simp

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ✝ : Measure α
s : SignedMeasure α
μ : Measure α
inst✝ : s.HaveLebesgueDecomposition μ
r : ℝ
hr : r < 0
⊢ (r • s).toJordanDecomposition.negPart.HaveLebesgueDecomposition μ

Tactic:
by
          rw [toJordanDecomposition_smul_real, JordanDecomposition.real_smul_negPart_neg _ _ hr]
          infer_instance

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm

Goal state before:
pp: α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup E
f : α → E
hf : MemLp f ∞ μ
⊢ ∀ᶠ (x : ℝ) in map (fun i ↦ ‖f i‖ₑ.toReal) (ae μ), (fun x1 x2 ↦ x1 ≤ x2) x (lpNorm f ∞ μ)

Tactic:
simpa [-toReal_enorm, lpNorm] using! ae_le_lpNorm_exponent_top hf

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

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
f : ι → α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
h : ∀ (ε : ℝ), 0 < ε → ∃ C, 0 < C ∧ ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε
hpzero : p ≠ 0
hμ : ¬μ univ = 0
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hCpos : 0 < C
hC : ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal (ε / 2)
i : ι
s : Set α
hs : MeasurableSet s
hμs : μ s ≤ ENNReal.ofReal ((ε / (2 * ↑C)) ^ p.toReal)
⊢ eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε

Tactic:
by_cases hμs' : μ s = 0

Goal state after:
case pos
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
f : ι → α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
h : ∀ (ε : ℝ), 0 < ε → ∃ C, 0 < C ∧ ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε
hpzero : p ≠ 0
hμ : ¬μ univ = 0
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hCpos : 0 < C
hC : ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal (ε / 2)
i : ι
s : Set α
hs : MeasurableSet s
hμs : μ s ≤ ENNReal.ofReal ((ε / (2 * ↑C)) ^ p.toReal)
hμs' : μ s = 0
⊢ eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε

case neg
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
f : ι → α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
h : ∀ (ε : ℝ), 0 < ε → ∃ C, 0 < C ∧ ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε
hpzero : p ≠ 0
hμ : ¬μ univ = 0
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hCpos : 0 < C
hC : ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal (ε / 2)
i : ι
s : Set α
hs : MeasurableSet s
hμs : μ s ≤ ENNReal.ofReal ((ε / (2 * ↑C)) ^ p.toReal)
hμs' : ¬μ s = 0
⊢ eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real

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

Tactic:
hc

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
hb : μ[-f | m] a ≤ μ[fun a ↦ |f a| | m] a
hc : μ[-f | m] a = (-μ[f | m]) a
⊢ |μ[f | m]| a ≤ μ[|f| | m] a
Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure

Goal state before:
pp: Ω : Type u_1
inst✝¹ : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
inst✝ : TopologicalSpace Ω
f : Ω →ᵇ ℝ≥0
⊢ μ.mass • μ.normalize.toFiniteMeasure.testAgainstNN f = μ.mass * μ.normalize.toFiniteMeasure.testAgainstNN f

Tactic:
smul_eq_mul

Goal state after:
Ω : Type u_1
inst✝¹ : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
inst✝ : TopologicalSpace Ω
f : Ω →ᵇ ℝ≥0
⊢ μ.mass * μ.normalize.toFiniteMeasure.testAgainstNN f = μ.mass * μ.normalize.toFiniteMeasure.testAgainstNN f
Module: Mathlib.MeasureTheory.Measure.FiniteMeasure

Goal state before:
pp: Ω : Type u_1
inst✝¹⁰ : MeasurableSpace Ω
R : Type u_2
inst✝⁹ : SMul R ℝ≥0
inst✝⁸ : SMul R ℝ≥0∞
inst✝⁷ : IsScalarTower R ℝ≥0 ℝ≥0∞
inst✝⁶ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst✝⁵ : TopologicalSpace Ω
inst✝⁴ : OpensMeasurableSpace Ω
inst✝³ : IsScalarTower R ℝ≥0 ℝ≥0
inst✝² : PseudoMetricSpace R
inst✝¹ : Zero R
inst✝ : IsBoundedSMul R ℝ≥0
μ : FiniteMeasure Ω
c : R
f : Ω →ᵇ ℝ≥0
⊢ ∫⁻ (ω : Ω), (c • 1) • ↑(f ω) ∂↑μ = (c • 1) • ∫⁻ (ω : Ω), ↑(f ω) ∂↑μ

Tactic:
smul_eq_mul

Goal state after:
Ω : Type u_1
inst✝¹⁰ : MeasurableSpace Ω
R : Type u_2
inst✝⁹ : SMul R ℝ≥0
inst✝⁸ : SMul R ℝ≥0∞
inst✝⁷ : IsScalarTower R ℝ≥0 ℝ≥0∞
inst✝⁶ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst✝⁵ : TopologicalSpace Ω
inst✝⁴ : OpensMeasurableSpace Ω
inst✝³ : IsScalarTower R ℝ≥0 ℝ≥0
inst✝² : PseudoMetricSpace R
inst✝¹ : Zero R
inst✝ : IsBoundedSMul R ℝ≥0
μ : FiniteMeasure Ω
c : R
f : Ω →ᵇ ℝ≥0
⊢ ∫⁻ (ω : Ω), c • 1 * ↑(f ω) ∂↑μ = c • 1 * ∫⁻ (ω : Ω), ↑(f ω) ∂↑μ
Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure

Goal state before:
pp: case e'_3
Ω : Type u_1
Ω' : Type u_2
inst✝⁵ : MeasurableSpace Ω
inst✝⁴ : MeasurableSpace Ω'
inst✝³ : TopologicalSpace Ω
inst✝² : OpensMeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω'
inst✝ : BorelSpace Ω'
ι : Type u_3
L : Filter ι
νs : ι → ProbabilityMeasure Ω
ν : ProbabilityMeasure Ω
lim : ∀ (f : Ω →ᵇ ℝ≥0), Tendsto (fun i ↦ ∫⁻ (ω : Ω), ↑(f ω) ∂↑(νs i)) L (𝓝 (∫⁻ (ω : Ω), ↑(f ω) ∂↑ν))
f : Ω → Ω'
f_cont : Continuous[inst✝³, inst✝¹] f
g : Ω' →ᵇ ℝ≥0
x✝ : ι
⊢ ∫⁻ (ω : Ω'), ↑(g ω) ∂↑((νs x✝).map ⋯) =
    ∫⁻ (ω : Ω), ↑((g.compContinuous { toFun := f, continuous_toFun := f_cont }) ω) ∂↑(νs x✝)

Tactic:
simp only [map, compContinuous_apply, ContinuousMap.coe_mk]

Goal state after:
case e'_3
Ω : Type u_1
Ω' : Type u_2
inst✝⁵ : MeasurableSpace Ω
inst✝⁴ : MeasurableSpace Ω'
inst✝³ : TopologicalSpace Ω
inst✝² : OpensMeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω'
inst✝ : BorelSpace Ω'
ι : Type u_3
L : Filter ι
νs : ι → ProbabilityMeasure Ω
ν : ProbabilityMeasure Ω
lim : ∀ (f : Ω →ᵇ ℝ≥0), Tendsto (fun i ↦ ∫⁻ (ω : Ω), ↑(f ω) ∂↑(νs i)) L (𝓝 (∫⁻ (ω : Ω), ↑(f ω) ∂↑ν))
f : Ω → Ω'
f_cont : Continuous[inst✝³, inst✝¹] f
g : Ω' →ᵇ ℝ≥0
x✝ : ι
⊢ ∫⁻ (ω : Ω'), ↑(g ω) ∂↑⟨Measure.map f ↑(νs x✝), ⋯⟩ = ∫⁻ (ω : Ω), ↑(g (f ω)) ∂↑(νs x✝)
Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure

Goal state before:
pp: case e'_5
Ω : Type u_1
Ω' : Type u_2
inst✝⁵ : MeasurableSpace Ω
inst✝⁴ : MeasurableSpace Ω'
inst✝³ : TopologicalSpace Ω
inst✝² : OpensMeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω'
inst✝ : BorelSpace Ω'
ι : Type u_3
L : Filter ι
νs : ι → ProbabilityMeasure Ω
ν : ProbabilityMeasure Ω
lim : ∀ (f : Ω →ᵇ ℝ≥0), Tendsto (fun i ↦ ∫⁻ (ω : Ω), ↑(f ω) ∂↑(νs i)) L (𝓝 (∫⁻ (ω : Ω), ↑(f ω) ∂↑ν))
f : Ω → Ω'
f_cont : Continuous[inst✝³, inst✝¹] f
g : Ω' →ᵇ ℝ≥0
⊢ ∫⁻ (ω : Ω'), ↑(g ω) ∂↑(ν.map ⋯) = ∫⁻ (ω : Ω), ↑((g.compContinuous { toFun := f, continuous_toFun := f_cont }) ω) ∂↑ν

Tactic:
simp only [map, compContinuous_apply, ContinuousMap.coe_mk]

Goal state after:
case e'_5
Ω : Type u_1
Ω' : Type u_2
inst✝⁵ : MeasurableSpace Ω
inst✝⁴ : MeasurableSpace Ω'
inst✝³ : TopologicalSpace Ω
inst✝² : OpensMeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω'
inst✝ : BorelSpace Ω'
ι : Type u_3
L : Filter ι
νs : ι → ProbabilityMeasure Ω
ν : ProbabilityMeasure Ω
lim : ∀ (f : Ω →ᵇ ℝ≥0), Tendsto (fun i ↦ ∫⁻ (ω : Ω), ↑(f ω) ∂↑(νs i)) L (𝓝 (∫⁻ (ω : Ω), ↑(f ω) ∂↑ν))
f : Ω → Ω'
f_cont : Continuous[inst✝³, inst✝¹] f
g : Ω' →ᵇ ℝ≥0
⊢ ∫⁻ (ω : Ω'), ↑(g ω) ∂↑⟨Measure.map f ↑ν, ⋯⟩ = ∫⁻ (ω : Ω), ↑(g (f ω)) ∂↑ν
Module: Mathlib.MeasureTheory.Function.UniformIntegrable

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

Tactic:
smul_eq_mul

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

Goal state before:
pp: case mpr
Ω : Type u_1
inst✝⁴ : MeasurableSpace Ω
inst✝³ : TopologicalSpace Ω
inst✝² : OpensMeasurableSpace Ω
ι : Type u_2
L : Filter ι
μ : Measure Ω
μs : ι → Measure Ω
inst✝¹ : IsProbabilityMeasure μ
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)
⊢ (∀ (G : Set Ω), IsOpen[inst✝³] G → μ G ≤ liminf (fun i ↦ (μs i) G) L) →
    ∀ (F : Set Ω), IsClosed[inst✝³] F → limsup (fun i ↦ (μs i) F) L ≤ μ F

Tactic:
intro h F F_closed

Goal state after:
case mpr
Ω : Type u_1
inst✝⁴ : MeasurableSpace Ω
inst✝³ : TopologicalSpace Ω
inst✝² : OpensMeasurableSpace Ω
ι : Type u_2
L : Filter ι
μ : Measure Ω
μs : ι → Measure Ω
inst✝¹ : IsProbabilityMeasure μ
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)
h : ∀ (G : Set Ω), IsOpen[inst✝³] G → μ G ≤ liminf (fun i ↦ (μs i) G) L
F : Set Ω
F_closed : IsClosed[inst✝³] F
⊢ limsup (fun i ↦ (μs i) F) L ≤ μ F
Module: Mathlib.MeasureTheory.Measure.FiniteMeasure

Goal state before:
pp: case e'_3
Ω : Type u_1
Ω' : Type u_2
inst✝⁵ : MeasurableSpace Ω
inst✝⁴ : MeasurableSpace Ω'
inst✝³ : TopologicalSpace Ω
inst✝² : OpensMeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω'
inst✝ : BorelSpace Ω'
ι : Type u_3
L : Filter ι
νs : ι → FiniteMeasure Ω
ν : FiniteMeasure Ω
lim : ∀ (f : Ω →ᵇ ℝ≥0), Tendsto (fun i ↦ ∫⁻ (x : Ω), ↑(f x) ∂↑(νs i)) L (𝓝 (∫⁻ (x : Ω), ↑(f x) ∂↑ν))
f : Ω → Ω'
f_cont : Continuous[inst✝³, inst✝¹] f
g : Ω' →ᵇ ℝ≥0
x✝ : ι
⊢ ∫⁻ (x : Ω'), ↑(g x) ∂↑((νs x✝).map f) =
    ∫⁻ (x : Ω), ↑((g.compContinuous { toFun := f, continuous_toFun := f_cont }) x) ∂↑(νs x✝)

Tactic:
simp only [map, compContinuous_apply, ContinuousMap.coe_mk]

Goal state after:
case e'_3
Ω : Type u_1
Ω' : Type u_2
inst✝⁵ : MeasurableSpace Ω
inst✝⁴ : MeasurableSpace Ω'
inst✝³ : TopologicalSpace Ω
inst✝² : OpensMeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω'
inst✝ : BorelSpace Ω'
ι : Type u_3
L : Filter ι
νs : ι → FiniteMeasure Ω
ν : FiniteMeasure Ω
lim : ∀ (f : Ω →ᵇ ℝ≥0), Tendsto (fun i ↦ ∫⁻ (x : Ω), ↑(f x) ∂↑(νs i)) L (𝓝 (∫⁻ (x : Ω), ↑(f x) ∂↑ν))
f : Ω → Ω'
f_cont : Continuous[inst✝³, inst✝¹] f
g : Ω' →ᵇ ℝ≥0
x✝ : ι
⊢ ∫⁻ (x : Ω'), ↑(g x) ∂↑⟨Measure.map f ↑(νs x✝), ⋯⟩ = ∫⁻ (x : Ω), ↑(g (f x)) ∂↑(νs x✝)
Module: Mathlib.MeasureTheory.Measure.FiniteMeasure

Goal state before:
pp: case e'_5
Ω : Type u_1
Ω' : Type u_2
inst✝⁵ : MeasurableSpace Ω
inst✝⁴ : MeasurableSpace Ω'
inst✝³ : TopologicalSpace Ω
inst✝² : OpensMeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω'
inst✝ : BorelSpace Ω'
ι : Type u_3
L : Filter ι
νs : ι → FiniteMeasure Ω
ν : FiniteMeasure Ω
lim : ∀ (f : Ω →ᵇ ℝ≥0), Tendsto (fun i ↦ ∫⁻ (x : Ω), ↑(f x) ∂↑(νs i)) L (𝓝 (∫⁻ (x : Ω), ↑(f x) ∂↑ν))
f : Ω → Ω'
f_cont : Continuous[inst✝³, inst✝¹] f
g : Ω' →ᵇ ℝ≥0
⊢ ∫⁻ (x : Ω'), ↑(g x) ∂↑(ν.map f) = ∫⁻ (x : Ω), ↑((g.compContinuous { toFun := f, continuous_toFun := f_cont }) x) ∂↑ν

Tactic:
simp only [map, compContinuous_apply, ContinuousMap.coe_mk]

Goal state after:
case e'_5
Ω : Type u_1
Ω' : Type u_2
inst✝⁵ : MeasurableSpace Ω
inst✝⁴ : MeasurableSpace Ω'
inst✝³ : TopologicalSpace Ω
inst✝² : OpensMeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω'
inst✝ : BorelSpace Ω'
ι : Type u_3
L : Filter ι
νs : ι → FiniteMeasure Ω
ν : FiniteMeasure Ω
lim : ∀ (f : Ω →ᵇ ℝ≥0), Tendsto (fun i ↦ ∫⁻ (x : Ω), ↑(f x) ∂↑(νs i)) L (𝓝 (∫⁻ (x : Ω), ↑(f x) ∂↑ν))
f : Ω → Ω'
f_cont : Continuous[inst✝³, inst✝¹] f
g : Ω' →ᵇ ℝ≥0
⊢ ∫⁻ (x : Ω'), ↑(g x) ∂↑⟨Measure.map f ↑ν, ⋯⟩ = ∫⁻ (x : Ω), ↑(g (f x)) ∂↑ν
Module: Mathlib.Probability.Independence.Kernel.Indep

Goal state before:
pp: case inr.inl
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m' _mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst✝ : IsZeroOrMarkovKernel κ
s t : Set Ω
a✝ : s ∈ {s | MeasurableSet s}
h : IsMarkovKernel κ
a : α
ht : t = ∅
⊢ (κ a) (s ∩ t) = (κ a) s * (κ a) t

Tactic:
ht,

Goal state after:
case inr.inl
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m' _mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst✝ : IsZeroOrMarkovKernel κ
s t : Set Ω
a✝ : s ∈ {s | MeasurableSet s}
h : IsMarkovKernel κ
a : α
ht : t = ∅
⊢ (κ a) (s ∩ ∅) = (κ a) s * (κ a) ∅
Module: Mathlib.Probability.Independence.Kernel.Indep

Goal state before:
pp: case inr.inr
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m' _mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst✝ : IsZeroOrMarkovKernel κ
s t : Set Ω
a✝ : s ∈ {s | MeasurableSet s}
h : IsMarkovKernel κ
a : α
ht : t = univ
⊢ (κ a) (s ∩ t) = (κ a) s * (κ a) t

Tactic:
ht,

Goal state after:
case inr.inr
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m' _mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst✝ : IsZeroOrMarkovKernel κ
s t : Set Ω
a✝ : s ∈ {s | MeasurableSet s}
h : IsMarkovKernel κ
a : α
ht : t = univ
⊢ (κ a) (s ∩ univ) = (κ a) s * (κ a) univ
Module: Mathlib.MeasureTheory.Measure.Portmanteau

Goal state before:
pp: case h
Ω : Type u_1
inst✝³ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : Measure Ω
μs : ℕ → Measure Ω
inst✝ : ∀ (i : ℕ), IsProbabilityMeasure (μs i)
f : Ω →ᵇ ℝ
f_nn : 0 ≤ f
h_opens : ∀ (G : Set Ω), IsOpen[inst✝²] G → μ G ≤ liminf (fun i ↦ (μs i) G) atTop
same : ∫⁻ (x : Ω), ENNReal.ofReal (f x) ∂μ ≤ liminf (fun i ↦ ∫⁻ (x : Ω), ENNReal.ofReal (f x) ∂μs i) atTop
obs : ∀ (i : ℕ), ∫⁻ (x : Ω), ↑‖f x‖₊ ∂μs i ≤ ↑‖f‖₊
x : ℝ≥0∞
hx : ∀ᶠ (n : ℕ) in atTop, x ≤ ∫⁻ (x : Ω), ENNReal.ofReal (f x) ∂μs n
⊢ x ≤ ↑‖f‖₊

Tactic:
obtain ⟨i, hi⟩ := hx.exists

Goal state after:
case h
Ω : Type u_1
inst✝³ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : Measure Ω
μs : ℕ → Measure Ω
inst✝ : ∀ (i : ℕ), IsProbabilityMeasure (μs i)
f : Ω →ᵇ ℝ
f_nn : 0 ≤ f
h_opens : ∀ (G : Set Ω), IsOpen[inst✝²] G → μ G ≤ liminf (fun i ↦ (μs i) G) atTop
same : ∫⁻ (x : Ω), ENNReal.ofReal (f x) ∂μ ≤ liminf (fun i ↦ ∫⁻ (x : Ω), ENNReal.ofReal (f x) ∂μs i) atTop
obs : ∀ (i : ℕ), ∫⁻ (x : Ω), ↑‖f x‖₊ ∂μs i ≤ ↑‖f‖₊
x : ℝ≥0∞
hx : ∀ᶠ (n : ℕ) in atTop, x ≤ ∫⁻ (x : Ω), ENNReal.ofReal (f x) ∂μs n
i : ℕ
hi : x ≤ ∫⁻ (x : Ω), ENNReal.ofReal (f x) ∂μs i
⊢ x ≤ ↑‖f‖₊
Module: Mathlib.MeasureTheory.Measure.Portmanteau

Goal state before:
pp: Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ : ProbabilityMeasure Ω
μs : ℕ → ProbabilityMeasure Ω
G : Set Ω
h_opens : μ G ≤ liminf (fun i ↦ (μs i) G) atTop
G_open : IsOpen[inst✝¹] G
aux : ↑(liminf (fun i ↦ (μs i) G) atTop) = liminf (ENNReal.ofNNReal ∘ fun i ↦ (μs i) G) atTop
obs : ↑(μ G) ≤ ↑(liminf (fun i ↦ (μs i) G) atTop)
⊢ ↑μ G ≤ liminf (fun i ↦ ↑(μs i) G) atTop

Tactic:
simp only [ProbabilityMeasure.ennreal_coeFn_eq_coeFn_toMeasure, aux] at obs

Goal state after:
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ : ProbabilityMeasure Ω
μs : ℕ → ProbabilityMeasure Ω
G : Set Ω
h_opens : μ G ≤ liminf (fun i ↦ (μs i) G) atTop
G_open : IsOpen[inst✝¹] G
aux : ↑(liminf (fun i ↦ (μs i) G) atTop) = liminf (ENNReal.ofNNReal ∘ fun i ↦ (μs i) G) atTop
obs : ↑μ G ≤ liminf (ENNReal.ofNNReal ∘ fun i ↦ (μs i) G) atTop
⊢ ↑μ G ≤ liminf (fun i ↦ ↑(μs i) G) atTop
Module: Mathlib.Probability.Independence.Basic

Goal state before:
pp: case right
Ω : Type u_1
ι : Type u_2
_mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : Fintype ι
β : ι → Type u_11
m : (i : ι) → MeasurableSpace (β i)
f : (i : ι) → Ω → β i
hf : ∀ (i : ι), AEMeasurable (f i) μ
h :
  ∀ (S : Finset ι) {sets : (i : ι) → Set (β i)},
    (∀ i ∈ S, MeasurableSet (sets i)) → μ (⋂ i ∈ S, f i ⁻¹' sets i) = ∏ i ∈ S, μ (f i ⁻¹' sets i)
this : IsProbabilityMeasure μ
s : (i : ι) → Set (β i)
hm : ∀ (i : ι), MeasurableSet (s i)
⊢ μ (⋂ i, f i ⁻¹' s i) = (Measure.map (fun ω i ↦ f i ω) μ) (univ.pi s)

Tactic:
· rw [Measure.map_apply_of_aemeasurable (aemeasurable_pi_lambda _ fun x ↦ hf x)
        (.univ_pi hm)]
      congr with x
      simp

Goal state after: