mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: case refine_1
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h : μ.toSignedMeasure = ν.toSignedMeasure
i : Set α
hi : MeasurableSet i
this : μ.toSignedMeasure i = ν.toSignedMeasure i
⊢ μ i = ν i

Tactic:
rwa [toSignedMeasure_apply_measurable hi, toSignedMeasure_apply_measurable hi,
        measureReal_eq_measureReal_iff] at this

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

Goal state before:
pp: α : 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
f : α → β
hf : Measurable f
⊢ ∀ ⦃f_1 : ℕ → Set β⦄,
    (∀ (i : ℕ), MeasurableSet (f_1 i)) →
      Pairwise (Disjoint on f_1) →
        HasSum (fun i ↦ if MeasurableSet (f_1 i) then v (f ⁻¹' f_1 i) else 0)
          (if MeasurableSet (⋃ i, f_1 i) then v (f ⁻¹' ⋃ i, f_1 i) else 0)

Tactic:
intro g

Goal state after:
α : 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
f : α → β
hf : Measurable f
g : ℕ → Set β
⊢ (∀ (i : ℕ), MeasurableSet (g i)) →
    Pairwise (Disjoint on g) →
      HasSum (fun i ↦ if MeasurableSet (g i) then v (f ⁻¹' g i) else 0)
        (if MeasurableSet (⋃ i, g i) then v (f ⁻¹' ⋃ i, g i) else 0)
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: case pos
α : Type u_1
mα : MeasurableSpace α
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
i : Set α
hi : MeasurableSet i
j : Set α
hj : MeasurableSet j
⊢ (restrict 0 i) j = 0 j

Tactic:
rw [restrict_apply 0 hi hj, zero_apply, zero_apply]

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
s : Set α
x : α
m : M
hx : x ∉ s
⊢ (dirac x m).restrict s = 0

Tactic:
by
  classical
  by_cases hs : MeasurableSet s
  · simp [restrict_dirac, hs, hx]
  · simp [restrict, hs]

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
v : VectorMeasure α M
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
u : Set α
hu : MeasurableSet u
⊢ ((v.restrict t).restrict s) u = (v.restrict (s ∩ t)) u

Tactic:
simp [restrict_apply, hs, hu, ht, Set.inter_assoc]

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

Goal state before:
pp: case refine_1
α : 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
⊢ ENNReal.toReal 0 - j.negPart.real A ≤ 0 A

Tactic:
ENNReal.toReal_zero,

Goal state after:
case refine_1
α : 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 - j.negPart.real A ≤ 0 A
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.posPart.real A - ENNReal.toReal 0

Tactic:
ENNReal.toReal_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 - 0
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝⁴ : TopologicalSpace M
inst✝³ : AddCommMonoid M
inst✝² : PartialOrder M
inst✝¹ : IsOrderedAddMonoid M
inst✝ : OrderClosedTopology M
v w : VectorMeasure α M
f : ℕ → Set α
hf₁ : ∀ (n : ℕ), MeasurableSet (f n)
hf₂ : ∀ (n : ℕ), v ≤[f n] w
a : Set α
ha₁ : MeasurableSet a
ha₂ : a ⊆ ⋃ n, f n
ha₃ : ⋃ n, a ∩ disjointed f n = a
⊢ v a ≤ w a

Tactic:
have ha₄ : Pairwise (Disjoint on fun n => a ∩ disjointed f n) :=
    (disjoint_disjointed _).mono fun i j => Disjoint.mono inf_le_right inf_le_right

Goal state after:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝⁴ : TopologicalSpace M
inst✝³ : AddCommMonoid M
inst✝² : PartialOrder M
inst✝¹ : IsOrderedAddMonoid M
inst✝ : OrderClosedTopology M
v w : VectorMeasure α M
f : ℕ → Set α
hf₁ : ∀ (n : ℕ), MeasurableSet (f n)
hf₂ : ∀ (n : ℕ), v ≤[f n] w
a : Set α
ha₁ : MeasurableSet a
ha₂ : a ⊆ ⋃ n, f n
ha₃ : ⋃ n, a ∩ disjointed f n = a
ha₄ : Pairwise (Disjoint on fun n ↦ a ∩ disjointed f n)
⊢ v a ≤ w a
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
j₁ j₂ : JordanDecomposition α
hj : j₁.toSignedMeasure = j₂.toSignedMeasure
S : Set α
hS₁ : MeasurableSet S
hS₂ : j₁.toSignedMeasure ≤[S] 0
hS₃ : 0 ≤[Sᶜ] j₁.toSignedMeasure
hS₄ : j₁.posPart S = 0
hS₅ : j₁.negPart Sᶜ = 0
T : Set α
hT₁ : MeasurableSet T
hT₂ : j₁.toSignedMeasure ≤[T] 0
hT₃ : 0 ≤[Tᶜ] j₁.toSignedMeasure
hT₄ : j₂.posPart T = 0
hT₅ : j₂.negPart Tᶜ = 0
hST₁ : j₁.toSignedMeasure (symmDiff Sᶜ Tᶜ) = 0
i : Set α
hi : MeasurableSet i
⊢ j₁.posPart.real i = j₁.posPart.real (i ∩ Sᶜ) - ENNReal.toReal 0

Tactic:
ENNReal.toReal_zero,

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
j₁ j₂ : JordanDecomposition α
hj : j₁.toSignedMeasure = j₂.toSignedMeasure
S : Set α
hS₁ : MeasurableSet S
hS₂ : j₁.toSignedMeasure ≤[S] 0
hS₃ : 0 ≤[Sᶜ] j₁.toSignedMeasure
hS₄ : j₁.posPart S = 0
hS₅ : j₁.negPart Sᶜ = 0
T : Set α
hT₁ : MeasurableSet T
hT₂ : j₁.toSignedMeasure ≤[T] 0
hT₃ : 0 ≤[Tᶜ] j₁.toSignedMeasure
hT₄ : j₂.posPart T = 0
hT₅ : j₂.negPart Tᶜ = 0
hST₁ : j₁.toSignedMeasure (symmDiff Sᶜ Tᶜ) = 0
i : Set α
hi : MeasurableSet i
⊢ j₁.posPart.real i = j₁.posPart.real (i ∩ Sᶜ) - 0
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
j₁ j₂ : JordanDecomposition α
hj : j₁.toSignedMeasure = j₂.toSignedMeasure
S : Set α
hS₁ : MeasurableSet S
hS₂ : j₁.toSignedMeasure ≤[S] 0
hS₃ : 0 ≤[Sᶜ] j₁.toSignedMeasure
hS₄ : j₁.posPart S = 0
hS₅ : j₁.negPart Sᶜ = 0
T : Set α
hT₁ : MeasurableSet T
hT₂ : j₁.toSignedMeasure ≤[T] 0
hT₃ : 0 ≤[Tᶜ] j₁.toSignedMeasure
hT₄ : j₂.posPart T = 0
hT₅ : j₂.negPart Tᶜ = 0
hST₁ : j₁.toSignedMeasure (symmDiff Sᶜ Tᶜ) = 0
i : Set α
hi : MeasurableSet i
hμ₁ : j₁.posPart.real i = j₁.toSignedMeasure (i ∩ Sᶜ)
⊢ j₂.posPart.real i = j₂.posPart.real (i ∩ Tᶜ) - ENNReal.toReal 0

Tactic:
ENNReal.toReal_zero,

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
j₁ j₂ : JordanDecomposition α
hj : j₁.toSignedMeasure = j₂.toSignedMeasure
S : Set α
hS₁ : MeasurableSet S
hS₂ : j₁.toSignedMeasure ≤[S] 0
hS₃ : 0 ≤[Sᶜ] j₁.toSignedMeasure
hS₄ : j₁.posPart S = 0
hS₅ : j₁.negPart Sᶜ = 0
T : Set α
hT₁ : MeasurableSet T
hT₂ : j₁.toSignedMeasure ≤[T] 0
hT₃ : 0 ≤[Tᶜ] j₁.toSignedMeasure
hT₄ : j₂.posPart T = 0
hT₅ : j₂.negPart Tᶜ = 0
hST₁ : j₁.toSignedMeasure (symmDiff Sᶜ Tᶜ) = 0
i : Set α
hi : MeasurableSet i
hμ₁ : j₁.posPart.real i = j₁.toSignedMeasure (i ∩ Sᶜ)
⊢ j₂.posPart.real i = j₂.posPart.real (i ∩ Tᶜ) - 0
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
s : SignedMeasure α
i j : Set α
hi : 0 ≤[i] s
hi₁ : MeasurableSet i
⊢ (s.toMeasureOfZeroLE i hi₁ hi) univ < ∞

Tactic:
by
    rw [toMeasureOfZeroLE_apply s hi hi₁ MeasurableSet.univ]
    exact ENNReal.coe_lt_top

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
⊢ μ.toSignedMeasure ≤ ν.toSignedMeasure ↔ μ ≤ ν

Tactic:
by
  rw [Measure.le_iff, VectorMeasure.le_iff]
  congrm ∀ s, (hs : MeasurableSet s) → ?_
  simp_rw [toSignedMeasure_apply_measurable hs, real_def]
  apply ENNReal.toReal_le_toReal <;> finiteness

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
⊢ lpNorm f 0 μ = 0

Tactic:
simp [lpNorm]

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

Goal state before:
pp: α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
inst✝ : NormedAddCommGroup E
f : α → E
⊢ lpNorm f p 0 = 0

Tactic:
simp [lpNorm]

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

Goal state before:
pp: α : Type u_1
E : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
⊢ lpNorm 0 p μ = 0

Tactic:
simp [lpNorm]

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

Goal state before:
pp: α : Type u_1
E : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
⊢ lpNorm (fun x ↦ 0) p μ = 0

Tactic:
simp [lpNorm]

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
s t : SignedMeasure α
μ : Measure α
f : α → ℝ
hf : Measurable f
hfi : Integrable f μ
hadd : s = t + μ.withDensityᵥ f
htμ' : t ⟂ᵥ μ.toENNRealVectorMeasure
htμ : t.toJordanDecomposition.posPart ⟂ₘ μ ∧ t.toJordanDecomposition.negPart ⟂ₘ μ
⊢ s.toJordanDecomposition.posPart.HaveLebesgueDecomposition μ

Tactic:
use ⟨t.toJordanDecomposition.posPart, fun x => ENNReal.ofReal (f x)⟩
        refine ⟨hf.ennreal_ofReal, htμ.1, ?_⟩
        rw [toJordanDecomposition_eq_of_eq_add_withDensity hf hfi htμ' hadd]

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

Goal state before:
pp: X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : HasOuterApproxClosed X
F : Set X
hF : IsClosed[inst✝³] F
inst✝¹ : MeasurableSpace X
inst✝ : OpensMeasurableSpace X
μ : Measure X
n : ℕ
⊢ μ F = ∫⁻ (x : X), F.indicator (fun x ↦ 1) x ∂μ

pp: X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : HasOuterApproxClosed X
F : Set X
hF : IsClosed[inst✝³] F
inst✝¹ : MeasurableSpace X
inst✝ : OpensMeasurableSpace X
μ : Measure X
n : ℕ
⊢ ∫⁻ (x : X), F.indicator (fun x ↦ 1) x ∂μ ≤ ∫⁻ (x : X), ↑((hF.apprSeq n) x) ∂μ

Tactic:
· rw [lintegral_indicator hF.measurableSet]
    simp only [lintegral_one, MeasurableSet.univ, Measure.restrict_apply, univ_inter]

Goal state after:
X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : HasOuterApproxClosed X
F : Set X
hF : IsClosed[inst✝³] F
inst✝¹ : MeasurableSpace X
inst✝ : OpensMeasurableSpace X
μ : Measure X
n : ℕ
⊢ ∫⁻ (x : X), F.indicator (fun x ↦ 1) x ∂μ ≤ ∫⁻ (x : X), ↑((hF.apprSeq n) 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
f : α → E
hm : ¬m ≤ m0
⊢ ∫ (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
⊢ ∫ (x : α), |μ[f | m] x| ∂μ ≤ ∫ (x : α), |f x| ∂μ

Tactic:
· simpa [condExp_of_not_le hm] 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
⊢ ∫ (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
⊢ ∫ (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
⊢ ∫ (x : α) in s, |μ[f | m] x| ∂μ ≤ ∫ (x : α) in s, |f x| ∂μ

Tactic:
· simpa [condExp_of_not_le hm] 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
⊢ ∫ (x : α) in s, |μ[f | m] x| ∂μ ≤ ∫ (x : α) in s, |f x| ∂μ
Module: Mathlib.MeasureTheory.Measure.FiniteMeasure

Goal state before:
pp: Ω : Type u_1
inst✝ : MeasurableSpace Ω
μ : FiniteMeasure Ω
hμ : μ = 0
⊢ μ.mass = 0

Tactic:
simp only [hμ, zero_mass]

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

Goal state before:
pp: case hf
α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
s✝ : Set (α × β)
u : Set α
Hu : MeasurableSet u
v : Set β
Hv : MeasurableSet v
Heq : u ×ˢ v = s✝
⊢ Measurable fun a ↦ ↑a.1 u

pp: case hg
α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
s✝ : Set (α × β)
u : Set α
Hu : MeasurableSet u
v : Set β
Hv : MeasurableSet v
Heq : u ×ˢ v = s✝
⊢ Measurable fun a ↦ ↑a.2 v

Tactic:
· exact (Measure.measurable_coe Hu).comp (measurable_subtype_coe.comp measurable_fst)

Goal state after:
case hg
α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
s✝ : Set (α × β)
u : Set α
Hu : MeasurableSet u
v : Set β
Hv : MeasurableSet v
Heq : u ×ˢ v = s✝
⊢ Measurable fun a ↦ ↑a.2 v
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 • ↑(f ω) ∂↑μ = c • ∫⁻ (ω : Ω), ↑(f ω) ∂↑μ

Tactic:
simp_rw [← smul_one_smul ℝ≥0∞ c (f _ : ℝ≥0∞), ← smul_one_smul ℝ≥0∞ c (lintegral _ _ : ℝ≥0∞),
    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.FiniteMeasure

Goal state before:
pp: Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
⊢ Continuous[instTopologicalSpace, _] fun μ ↦ μ.mass

Tactic:
simp_rw [← testAgainstNN_one]; exact continuous_testAgainstNN_eval 1

Goal state after:
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 : ι → α → β
inst✝ : IsFiniteMeasure μ
hp : 1 ≤ p
hp' : p ≠ ∞
hf : ∀ (i : ι), StronglyMeasurable (f i)
h : ∀ (ε : ℝ), 0 < ε → ∃ C, ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε
C : ℝ≥0
hC : ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal 1
i : ι
⊢ eLpNorm (f i) p μ ≤
    eLpNorm ({x | ‖f i x‖₊ < C}.indicator (f i)) p μ + eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ

Tactic:
refine le_trans (eLpNorm_mono_enorm fun x => ?_) (eLpNorm_add_le
        (StronglyMeasurable.aestronglyMeasurable
          ((hf i).indicator ((hf i).nnnorm.measurableSet_lt stronglyMeasurable_const)))
        (StronglyMeasurable.aestronglyMeasurable
          ((hf i).indicator (stronglyMeasurable_const.measurableSet_le (hf i).nnnorm))) hp)
      rw [Pi.add_apply, Set.indicator_apply]
      split_ifs with hx
      · rw [Set.indicator_of_notMem, add_zero]
        simpa using hx
      · rw [Set.indicator_of_mem, zero_add]
        simpa using hx

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

Goal state before:
pp: Ω : 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
⊢ ∀ (f_1 : Ω' →ᵇ ℝ≥0),
    Tendsto (fun i ↦ ∫⁻ (ω : Ω'), ↑(f_1 ω) ∂↑((νs i).map ⋯)) L (𝓝 (∫⁻ (ω : Ω'), ↑(f_1 ω) ∂↑(ν.map ⋯)))

Tactic:
intro g

Goal state after:
Ω : 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
⊢ Tendsto (fun i ↦ ∫⁻ (ω : Ω'), ↑(g ω) ∂↑((νs i).map ⋯)) L (𝓝 (∫⁻ (ω : Ω'), ↑(g ω) ∂↑(ν.map ⋯)))
Module: Mathlib.MeasureTheory.Measure.FiniteMeasure

Goal state before:
pp: Ω : Type u_1
Ω' : Type u_2
inst✝⁶ : MeasurableSpace Ω
inst✝⁵ : MeasurableSpace Ω'
inst✝⁴ : TopologicalSpace Ω
inst✝³ : TopologicalSpace Ω'
inst✝² : BorelSpace Ω
inst✝¹ : BorelSpace Ω'
inst✝ : NormalSpace Ω'
f : Ω → Ω'
hf : IsClosedEmbedding f
μ : FiniteMeasure Ω'
hμ : μ ∈ {μ | μ (range f)ᶜ = 0}
⊢ ∀ (f_1 : Ω →ᵇ ℝ),
    Tendsto (fun i ↦ ∫ (x : Ω), f_1 x ∂↑(comap f i)) (𝓝[{μ | μ (range f)ᶜ = 0}] μ) (𝓝 (∫ (x : Ω), f_1 x ∂↑(comap f μ)))

Tactic:
intro g

Goal state after:
Ω : Type u_1
Ω' : Type u_2
inst✝⁶ : MeasurableSpace Ω
inst✝⁵ : MeasurableSpace Ω'
inst✝⁴ : TopologicalSpace Ω
inst✝³ : TopologicalSpace Ω'
inst✝² : BorelSpace Ω
inst✝¹ : BorelSpace Ω'
inst✝ : NormalSpace Ω'
f : Ω → Ω'
hf : IsClosedEmbedding f
μ : FiniteMeasure Ω'
hμ : μ ∈ {μ | μ (range f)ᶜ = 0}
g : Ω →ᵇ ℝ
⊢ Tendsto (fun i ↦ ∫ (x : Ω), g x ∂↑(comap f i)) (𝓝[{μ | μ (range f)ᶜ = 0}] μ) (𝓝 (∫ (x : Ω), g x ∂↑(comap f μ)))
Module: Mathlib.MeasureTheory.Measure.FiniteMeasure

Goal state before:
pp: Ω : 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
⊢ ∀ (f_1 : Ω' →ᵇ ℝ≥0),
    Tendsto (fun i ↦ ∫⁻ (x : Ω'), ↑(f_1 x) ∂↑((νs i).map f)) L (𝓝 (∫⁻ (x : Ω'), ↑(f_1 x) ∂↑(ν.map f)))

Tactic:
intro g

Goal state after:
Ω : 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
⊢ Tendsto (fun i ↦ ∫⁻ (x : Ω'), ↑(g x) ∂↑((νs i).map f)) L (𝓝 (∫⁻ (x : Ω'), ↑(g x) ∂↑(ν.map f)))
Module: Mathlib.Probability.Independence.Kernel.IndepFun

Goal state before:
pp: case inr
α : Type u_1
Ω : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
β : ι → Type u_8
m : (i : ι) → MeasurableSpace (β i)
f : (i : ι) → Ω → β i
S T : Finset ι
hST : Disjoint S T
hf_Indep : iIndepFun f κ μ
hf_meas : ∀ (i : ι), Measurable (f i)
hμ : μ ≠ 0
η : Kernel α Ω
η_eq : ⇑κ =ᵐ[μ] ⇑η
hη : IsMarkovKernel η
πSβ : Set (Set ((i : ↥S) → β ↑i)) := univ.pi '' univ.pi fun i ↦ {s | MeasurableSet s}
πS : Set (Set Ω) := {s | ∃ t ∈ πSβ, (fun a i ↦ f (↑i) a) ⁻¹' t = s}
hπS_pi : IsPiSystem πS
hπS_gen : MeasurableSpace.comap (fun a i ↦ f (↑i) a) MeasurableSpace.pi = generateFrom πS
πTβ : Set (Set ((i : ↥T) → β ↑i)) := univ.pi '' univ.pi fun i ↦ {s | MeasurableSet s}
πT : Set (Set Ω) := {s | ∃ t ∈ πTβ, (fun a i ↦ f (↑i) a) ⁻¹' t = s}
hπT_pi : IsPiSystem πT
hπT_gen : MeasurableSpace.comap (fun a i ↦ f (↑i) a) MeasurableSpace.pi = generateFrom πT
⊢ IndepSets πS πT η μ

Tactic:
rintro _ _ ⟨s, ⟨sets_s, hs1, hs2⟩, rfl⟩ ⟨t, ⟨sets_t, ht1, ht2⟩, rfl⟩

Goal state after:
case inr
α : Type u_1
Ω : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
β : ι → Type u_8
m : (i : ι) → MeasurableSpace (β i)
f : (i : ι) → Ω → β i
S T : Finset ι
hST : Disjoint S T
hf_Indep : iIndepFun f κ μ
hf_meas : ∀ (i : ι), Measurable (f i)
hμ : μ ≠ 0
η : Kernel α Ω
η_eq : ⇑κ =ᵐ[μ] ⇑η
hη : IsMarkovKernel η
πSβ : Set (Set ((i : ↥S) → β ↑i)) := univ.pi '' univ.pi fun i ↦ {s | MeasurableSet s}
πS : Set (Set Ω) := {s | ∃ t ∈ πSβ, (fun a i ↦ f (↑i) a) ⁻¹' t = s}
hπS_pi : IsPiSystem πS
hπS_gen : MeasurableSpace.comap (fun a i ↦ f (↑i) a) MeasurableSpace.pi = generateFrom πS
πTβ : Set (Set ((i : ↥T) → β ↑i)) := univ.pi '' univ.pi fun i ↦ {s | MeasurableSet s}
πT : Set (Set Ω) := {s | ∃ t ∈ πTβ, (fun a i ↦ f (↑i) a) ⁻¹' t = s}
hπT_pi : IsPiSystem πT
hπT_gen : MeasurableSpace.comap (fun a i ↦ f (↑i) a) MeasurableSpace.pi = generateFrom πT
s : Set ((i : ↥S) → β ↑i)
sets_s : (i : ↥S) → Set (β ↑i)
hs1 : sets_s ∈ univ.pi fun i ↦ {s | MeasurableSet s}
hs2 : univ.pi sets_s = s
t : Set ((i : ↥T) → β ↑i)
sets_t : (i : ↥T) → Set (β ↑i)
ht1 : sets_t ∈ univ.pi fun i ↦ {s | MeasurableSet s}
ht2 : univ.pi sets_t = t
⊢ ∀ᵐ (a : α) ∂μ,
    (η a) ((fun a i ↦ f (↑i) a) ⁻¹' s ∩ (fun a i ↦ f (↑i) a) ⁻¹' t) =
      (η a) ((fun a i ↦ f (↑i) a) ⁻¹' s) * (η a) ((fun a i ↦ f (↑i) a) ⁻¹' t)