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

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_top : p ≠ ∞
ε : ℝ
hε : 0 < ε
M : ℝ
hf : ∀ (x : α), ‖f x‖ < M
hM : M ≤ 0
⊢ ∃ δ,
    ∃ (_ : 0 < δ),
      ∀ (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator f) p μ ≤ ENNReal.ofReal ε

Tactic:
refine ⟨1, zero_lt_one, fun s _ _ => ?_⟩

Goal state after:
case pos
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_top : p ≠ ∞
ε : ℝ
hε : 0 < ε
M : ℝ
hf : ∀ (x : α), ‖f x‖ < M
hM : M ≤ 0
s : Set α
x✝¹ : MeasurableSet s
x✝ : μ s ≤ ENNReal.ofReal 1
⊢ eLpNorm (s.indicator f) p μ ≤ ENNReal.ofReal ε
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi₂ : ¬s ≤[i] 0
n : ℕ
hn : ¬s ≤[i \ ⋃ k, ⋃ (_ : k < n), s.restrictNonposSeq i k] 0
⊢ 0 < s (s.restrictNonposSeq i n)

Tactic:
cases n with
  | zero =>
    rw [restrictNonposSeq]; rw [← @Set.sdiff_empty _ i] at hi₂
    rcases someExistsOneDivLT_spec hi₂ with ⟨_, _, h⟩
    exact lt_trans Nat.one_div_pos_of_nat h
  | succ n =>
    rw [restrictNonposSeq_succ]
    have h₁ : ¬s ≤[i \ ⋃ (k : ℕ) (_ : k ≤ n), restrictNonposSeq s i k] 0 := by
      refine mt (restrict_le_zero_subset _ ?_ (by simp)) hn
      convert! measurable_of_not_restrict_le_zero _ hn using 3
      exact funext fun x => by rw [Nat.lt_succ_iff]
    rcases someExistsOneDivLT_spec h₁ with ⟨_, _, h⟩
    exact lt_trans Nat.one_div_pos_of_nat h

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

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
j : JordanDecomposition α
r : ℝ
hr : r < 0
⊢ (if 0 ≤ r then r.toNNReal • j else -((-r).toNNReal • j)).posPart = ((-r).toNNReal • j).negPart

Tactic:
if_neg (not_le.2 hr),

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
j : JordanDecomposition α
r : ℝ
hr : r < 0
⊢ (-((-r).toNNReal • j)).posPart = ((-r).toNNReal • j).negPart
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
j : JordanDecomposition α
r : ℝ
hr : r < 0
⊢ (if 0 ≤ r then r.toNNReal • j else -((-r).toNNReal • j)).negPart = ((-r).toNNReal • j).posPart

Tactic:
if_neg (not_le.2 hr),

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
j : JordanDecomposition α
r : ℝ
hr : r < 0
⊢ (-((-r).toNNReal • j)).negPart = ((-r).toNNReal • j).posPart
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn

Goal state before:
pp: case pos
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi : s i < 0
hi₁ : MeasurableSet i
h : ¬s ≤[i] 0
hn : ∀ (n : ℕ), ¬s ≤[i \ ⋃ l, ⋃ (_ : l < n), s.restrictNonposSeq i l] 0
⊢ ∃ j, MeasurableSet j ∧ j ⊆ i ∧ s ≤[j] 0 ∧ s j < 0

pp: case neg
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi : s i < 0
hi₁ : MeasurableSet i
h : ¬s ≤[i] 0
hn : ¬∀ (n : ℕ), ¬s ≤[i \ ⋃ l, ⋃ (_ : l < n), s.restrictNonposSeq i l] 0
⊢ ∃ j, MeasurableSet j ∧ j ⊆ i ∧ s ≤[j] 0 ∧ s j < 0

Tactic:
swap

Goal state after:
case neg
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi : s i < 0
hi₁ : MeasurableSet i
h : ¬s ≤[i] 0
hn : ¬∀ (n : ℕ), ¬s ≤[i \ ⋃ l, ⋃ (_ : l < n), s.restrictNonposSeq i l] 0
⊢ ∃ j, MeasurableSet j ∧ j ⊆ i ∧ s ≤[j] 0 ∧ s j < 0

case pos
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi : s i < 0
hi₁ : MeasurableSet i
h : ¬s ≤[i] 0
hn : ∀ (n : ℕ), ¬s ≤[i \ ⋃ l, ⋃ (_ : l < n), s.restrictNonposSeq i l] 0
⊢ ∃ j, MeasurableSet j ∧ j ⊆ i ∧ s ≤[j] 0 ∧ s j < 0
Module: Mathlib.MeasureTheory.Function.UniformIntegrable

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup β
p : ℝ≥0∞
inst✝ : IsFiniteMeasure μ
hp : 1 ≤ p
hp' : p ≠ ∞
f : ℕ → α → β
g : α → β
hf : ∀ (n : ℕ), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hg' : MemLp g p μ
hui : UnifIntegrable f p μ
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (g x))
ε : ℝ≥0∞
hε : ε > 0
h : ε = ∞
n : ℕ
x✝ : n ≥ 0
⊢ eLpNorm (f n - g) p μ ≤ ε

Tactic:
simp [h]

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

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
⊢ Injective toSignedMeasure

Tactic:
intro j₁ j₂ hj
  -- obtain the two Hahn decompositions from the Jordan decompositions
  obtain ⟨S, hS₁, hS₂, hS₃, hS₄, hS₅⟩ := j₁.exists_compl_positive_negative
  obtain ⟨T, hT₁, hT₂, hT₃, hT₄, hT₅⟩ := j₂.exists_compl_positive_negative
  rw [← hj] at hT₂ hT₃
  -- the symmetric differences of the two Hahn decompositions have measure zero
  obtain ⟨hST₁, -⟩ :=
    of_symmDiff_compl_positive_negative hS₁.compl hT₁.compl ⟨hS₃, (compl_compl S).symm ▸ hS₂⟩
      ⟨hT₃, (compl_compl T).symm ▸ hT₂⟩
  -- it suffices to show the Jordan decompositions have the same positive parts
  refine eq_of_posPart_eq_posPart ?_ hj
  ext1 i hi
  -- we see that the positive parts of the two Jordan decompositions are equal to their
  -- associated signed measures restricted on their associated Hahn decompositions
  have hμ₁ : j₁.posPart.real i = j₁.toSignedMeasure (i ∩ Sᶜ) := by
    rw [toSignedMeasure, toSignedMeasure_sub_apply (hi.inter hS₁.compl),
      measureReal_def (μ := j₁.negPart),
      show j₁.negPart (i ∩ Sᶜ) = 0 from
        nonpos_iff_eq_zero.1 (hS₅ ▸ measure_mono Set.inter_subset_right),
      ENNReal.toReal_zero, sub_zero]
    conv_lhs => rw [← Set.inter_union_compl i S]
    rw [measureReal_union, measureReal_def,
      show j₁.posPart (i ∩ S) = 0 from
        nonpos_iff_eq_zero.1 (hS₄ ▸ measure_mono Set.inter_subset_right),
      ENNReal.toReal_zero, zero_add]
    · refine
        Set.disjoint_of_subset_left Set.inter_subset_right
          (Set.disjoint_of_subset_right Set.inter_subset_right disjoint_compl_right)
    · exact hi.inter hS₁.compl
  have hμ₂ : j₂.posPart.real i = j₂.toSignedMeasure (i ∩ Tᶜ) := by
    rw [toSignedMeasure, toSignedMeasure_sub_apply (hi.inter hT₁.compl),
      measureReal_def (μ := j₂.negPart),
      show j₂.negPart (i ∩ Tᶜ) = 0 from
        nonpos_iff_eq_zero.1 (hT₅ ▸ measure_mono Set.inter_subset_right),
      ENNReal.toReal_zero, sub_zero]
    conv_lhs => rw [← Set.inter_union_compl i T]
    rw [measureReal_union, measureReal_def,
      show j₂.posPart (i ∩ T) = 0 from
        nonpos_iff_eq_zero.1 (hT₄ ▸ measure_mono Set.inter_subset_right),
      ENNReal.toReal_zero, zero_add]
    · exact
        Set.disjoint_of_subset_left Set.inter_subset_right
          (Set.disjoint_of_subset_right Set.inter_subset_right disjoint_compl_right)
    · exact hi.inter hT₁.compl
  -- since the two signed measures associated with the Jordan decompositions are the same,
  -- and the symmetric difference of the Hahn decompositions have measure zero, the result follows
  rw [← measureReal_eq_measureReal_iff, hμ₁, hμ₂, ← hj]
  exact of_inter_eq_of_symmDiff_eq_zero_positive hS₁.compl hT₁.compl hi hS₃ hT₃ hST₁

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

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi : s i < 0
hi₁ : MeasurableSet i
h : ¬s ≤[i] 0
hn : ∀ (n : ℕ), ¬s ≤[i \ ⋃ l, ⋃ (_ : l < n), s.restrictNonposSeq i l] 0
A : Set α := i \ ⋃ l, s.restrictNonposSeq i l
hA : A = i \ ⋃ l, s.restrictNonposSeq i l
bdd : ℕ → ℕ := fun n ↦ s.findExistsOneDivLT (i \ ⋃ k, ⋃ (_ : k ≤ n), s.restrictNonposSeq i k)
hn' : ∀ (n : ℕ), ¬s ≤[i \ ⋃ l, ⋃ (_ : l ≤ n), s.restrictNonposSeq i l] 0
h₁ : s i = s A + ∑' (l : ℕ), s (s.restrictNonposSeq i l)
h₂ : s A ≤ s i
h₃' : Summable fun n ↦ 1 / (↑(bdd n) + 1)
h₃ : Tendsto (fun n ↦ ↑(bdd n) + 1) atTop atTop
h₄ : ∀ (b : ℝ), ∃ i, ∀ (a : ℕ), i ≤ a → b ≤ ↑(bdd a)
A_meas : MeasurableSet A
E : Set α
hE₁ : MeasurableSet E
hE₂ : E ⊆ A
hE₃ : 0 E < s E
k : ℕ
hk : ∀ (a : ℕ), k ≤ a → max (1 / s E + 1) 1 ≤ ↑(bdd a)
⊢ ∃ k, 1 ≤ bdd k ∧ 1 / ↑(bdd k) < s E

Tactic:
refine ⟨k, ?_, ?_⟩

Goal state after:
case refine_1
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi : s i < 0
hi₁ : MeasurableSet i
h : ¬s ≤[i] 0
hn : ∀ (n : ℕ), ¬s ≤[i \ ⋃ l, ⋃ (_ : l < n), s.restrictNonposSeq i l] 0
A : Set α := i \ ⋃ l, s.restrictNonposSeq i l
hA : A = i \ ⋃ l, s.restrictNonposSeq i l
bdd : ℕ → ℕ := fun n ↦ s.findExistsOneDivLT (i \ ⋃ k, ⋃ (_ : k ≤ n), s.restrictNonposSeq i k)
hn' : ∀ (n : ℕ), ¬s ≤[i \ ⋃ l, ⋃ (_ : l ≤ n), s.restrictNonposSeq i l] 0
h₁ : s i = s A + ∑' (l : ℕ), s (s.restrictNonposSeq i l)
h₂ : s A ≤ s i
h₃' : Summable fun n ↦ 1 / (↑(bdd n) + 1)
h₃ : Tendsto (fun n ↦ ↑(bdd n) + 1) atTop atTop
h₄ : ∀ (b : ℝ), ∃ i, ∀ (a : ℕ), i ≤ a → b ≤ ↑(bdd a)
A_meas : MeasurableSet A
E : Set α
hE₁ : MeasurableSet E
hE₂ : E ⊆ A
hE₃ : 0 E < s E
k : ℕ
hk : ∀ (a : ℕ), k ≤ a → max (1 / s E + 1) 1 ≤ ↑(bdd a)
⊢ 1 ≤ bdd k

case refine_2
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi : s i < 0
hi₁ : MeasurableSet i
h : ¬s ≤[i] 0
hn : ∀ (n : ℕ), ¬s ≤[i \ ⋃ l, ⋃ (_ : l < n), s.restrictNonposSeq i l] 0
A : Set α := i \ ⋃ l, s.restrictNonposSeq i l
hA : A = i \ ⋃ l, s.restrictNonposSeq i l
bdd : ℕ → ℕ := fun n ↦ s.findExistsOneDivLT (i \ ⋃ k, ⋃ (_ : k ≤ n), s.restrictNonposSeq i k)
hn' : ∀ (n : ℕ), ¬s ≤[i \ ⋃ l, ⋃ (_ : l ≤ n), s.restrictNonposSeq i l] 0
h₁ : s i = s A + ∑' (l : ℕ), s (s.restrictNonposSeq i l)
h₂ : s A ≤ s i
h₃' : Summable fun n ↦ 1 / (↑(bdd n) + 1)
h₃ : Tendsto (fun n ↦ ↑(bdd n) + 1) atTop atTop
h₄ : ∀ (b : ℝ), ∃ i, ∀ (a : ℕ), i ≤ a → b ≤ ↑(bdd a)
A_meas : MeasurableSet A
E : Set α
hE₁ : MeasurableSet E
hE₂ : E ⊆ A
hE₃ : 0 E < s E
k : ℕ
hk : ∀ (a : ℕ), k ≤ a → max (1 / s E + 1) 1 ≤ ↑(bdd a)
⊢ 1 / ↑(bdd k) < s E
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan

Goal state before:
pp: case mp.refine_1
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
μ : VectorMeasure α ℝ≥0∞
u : Set α
hmeas : MeasurableSet u
hu₁ : ∀ t ⊆ u, s t = 0
hu₂ : ∀ t ⊆ uᶜ, μ t = 0
i : Set α
hi₁ : MeasurableSet i
hi₂ : 0 ≤[i] s
hi₃ : s ≤[iᶜ] 0
hpos : s.toJordanDecomposition.posPart = s.toMeasureOfZeroLE i hi₁ hi₂
hneg : s.toJordanDecomposition.negPart = s.toMeasureOfLEZero iᶜ ⋯ hi₃
⊢ s.totalVariation u = 0

Tactic:
rw [totalVariation, Measure.add_apply, hpos, hneg, toMeasureOfZeroLE_apply _ _ _ hmeas,
        toMeasureOfLEZero_apply _ _ _ hmeas]
      simp [hu₁ _ Set.inter_subset_right]

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

Goal state before:
pp: case pos
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
𝕜 : Type u_3
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : SMulCommClass ℝ 𝕜 E
f : α → E
r : 𝕜
hf : ¬Integrable f μ
hr : r = 0
⊢ μ.withDensityᵥ 0 = 0

Tactic:
withDensityᵥ_zero

Goal state after:
case pos
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
𝕜 : Type u_3
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : SMulCommClass ℝ 𝕜 E
f : α → E
r : 𝕜
hf : ¬Integrable f μ
hr : r = 0
⊢ 0 = 0
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
⊢ 0 = μ.withDensityᵥ 0

Tactic:
withDensityᵥ_zero

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
⊢ 0 = 0
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real

Goal state before:
pp: case pos
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
R : ℝ≥0
f : α → ℝ
hbdd : ∀ᵐ (x : α) ∂μ, |f x| ≤ ↑R
hnm : m ≤ m0
⊢ ∀ᵐ (x : α) ∂μ, |μ[f | m] x| ≤ ↑R

pp: case neg
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
R : ℝ≥0
f : α → ℝ
hbdd : ∀ᵐ (x : α) ∂μ, |f x| ≤ ↑R
hnm : ¬m ≤ m0
⊢ ∀ᵐ (x : α) ∂μ, |μ[f | m] x| ≤ ↑R

Tactic:
swap

Goal state after:
case neg
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
R : ℝ≥0
f : α → ℝ
hbdd : ∀ᵐ (x : α) ∂μ, |f x| ≤ ↑R
hnm : ¬m ≤ m0
⊢ ∀ᵐ (x : α) ∂μ, |μ[f | m] x| ≤ ↑R

case pos
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
R : ℝ≥0
f : α → ℝ
hbdd : ∀ᵐ (x : α) ∂μ, |f x| ≤ ↑R
hnm : m ≤ m0
⊢ ∀ᵐ (x : α) ∂μ, |μ[f | m] x| ≤ ↑R
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real

Goal state before:
pp: case pos
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
R : ℝ≥0
f : α → ℝ
hbdd : ∀ᵐ (x : α) ∂μ, |f x| ≤ ↑R
hnm : m ≤ m0
hfint : Integrable f μ
⊢ ∀ᵐ (x : α) ∂μ, |μ[f | m] x| ≤ ↑R

pp: case neg
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
R : ℝ≥0
f : α → ℝ
hbdd : ∀ᵐ (x : α) ∂μ, |f x| ≤ ↑R
hnm : m ≤ m0
hfint : ¬Integrable f μ
⊢ ∀ᵐ (x : α) ∂μ, |μ[f | m] x| ≤ ↑R

Tactic:
swap

Goal state after:
case neg
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
R : ℝ≥0
f : α → ℝ
hbdd : ∀ᵐ (x : α) ∂μ, |f x| ≤ ↑R
hnm : m ≤ m0
hfint : ¬Integrable f μ
⊢ ∀ᵐ (x : α) ∂μ, |μ[f | m] x| ≤ ↑R

case pos
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
R : ℝ≥0
f : α → ℝ
hbdd : ∀ᵐ (x : α) ∂μ, |f x| ≤ ↑R
hnm : m ≤ m0
hfint : Integrable f μ
⊢ ∀ᵐ (x : α) ∂μ, |μ[f | m] x| ≤ ↑R
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
f : α → E
hfint : Integrable f μ
⊢ Integrable (fun x ↦ ‖f x‖ ^ 1) μ

Tactic:
simpa using hfint.norm

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

Goal state before:
pp: Ω : Type u_1
inst✝ : MeasurableSpace Ω
this : {μ | IsFiniteMeasure μ} = (fun μ ↦ μ univ) ⁻¹' Ico 0 ∞
⊢ MeasurableSet {μ | IsFiniteMeasure μ}

Tactic:
rw [this]
    exact Measure.measurable_coe MeasurableSet.univ measurableSet_Ico

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

Goal state before:
pp: case pos
Ω : Type u_1
inst✝² : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
γ : Type u_2
F : Filter γ
μs : γ → FiniteMeasure Ω
μs_lim : Tendsto (fun i ↦ (μs i).normalize) F (𝓝 μ.normalize)
mass_lim : Tendsto (fun i ↦ (μs i).mass) F (𝓝 μ.mass)
f : Ω →ᵇ ℝ≥0
h_mass : μ.mass = 0
⊢ Tendsto (fun i ↦ (μs i).testAgainstNN f) F (𝓝 (μ.testAgainstNN f))

Tactic:
simp only [μ.mass_zero_iff.mp h_mass, zero_testAgainstNN_apply, zero_mass] at mass_lim ⊢
    exact tendsto_zero_testAgainstNN_of_tendsto_zero_mass mass_lim f

Goal state after:
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
s : Set α
hs : MeasurableSet s
f : α → E
hfint : Integrable f μ
⊢ Integrable (fun x ↦ ‖f x‖ ^ 1) μ

Tactic:
simpa using hfint.norm

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

Goal state before:
pp: Ω : Type u_1
inst✝² : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
γ : Type u_2
F : Filter γ
μs : γ → FiniteMeasure Ω
μs_lim : Tendsto (fun i ↦ (μs i).normalize) F (𝓝 μ.normalize)
mass_lim : Tendsto (fun i ↦ (μs i).mass) F (𝓝 μ.mass)
f : Ω →ᵇ ℝ≥0
⊢ Tendsto (fun i ↦ (μs i).testAgainstNN f) F (𝓝 (μ.testAgainstNN f))

Tactic:
by_cases h_mass : μ.mass = 0
  · simp only [μ.mass_zero_iff.mp h_mass, zero_testAgainstNN_apply, zero_mass] at mass_lim ⊢
    exact tendsto_zero_testAgainstNN_of_tendsto_zero_mass mass_lim f
  simp_rw [fun i ↦ (μs i).testAgainstNN_eq_mass_mul f, μ.testAgainstNN_eq_mass_mul f]
  rw [ProbabilityMeasure.tendsto_nhds_iff_toFiniteMeasure_tendsto_nhds] at μs_lim
  rw [tendsto_iff_forall_testAgainstNN_tendsto] at μs_lim
  have lim_pair :
    Tendsto (fun i ↦ (⟨(μs i).mass, (μs i).normalize.toFiniteMeasure.testAgainstNN f⟩ : ℝ≥0 × ℝ≥0))
      F (𝓝 ⟨μ.mass, μ.normalize.toFiniteMeasure.testAgainstNN f⟩) :=
    (Prod.tendsto_iff _ _).mpr ⟨mass_lim, μs_lim f⟩
  exact tendsto_mul.comp lim_pair

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

Goal state before:
pp: case pos
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
S : Set (Measure 𝓧)
inst✝⁴ : TopologicalSpace 𝓧
inst✝³ : TopologicalSpace 𝓨
inst✝² : MeasurableSpace 𝓨
inst✝¹ : OpensMeasurableSpace 𝓨
inst✝ : T2Space 𝓨
hS : ∀ (ε : ENNReal), 0 < ε → ∃ K, IsCompact K ∧ ∀ μ ∈ S, μ Kᶜ ≤ ε
f : 𝓧 → 𝓨
hf : Continuous[inst✝⁴, inst✝³] f
ε : ENNReal
hε : 0 < ε
K : Set 𝓧
hK_compact : IsCompact K
hKS : ∀ μ ∈ S, μ Kᶜ ≤ ε
μ : Measure 𝓧
hμS : μ ∈ S
hf_meas : AEMeasurable f μ
⊢ (Measure.map f μ) (f '' K)ᶜ ≤ ε

pp: case neg
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
S : Set (Measure 𝓧)
inst✝⁴ : TopologicalSpace 𝓧
inst✝³ : TopologicalSpace 𝓨
inst✝² : MeasurableSpace 𝓨
inst✝¹ : OpensMeasurableSpace 𝓨
inst✝ : T2Space 𝓨
hS : ∀ (ε : ENNReal), 0 < ε → ∃ K, IsCompact K ∧ ∀ μ ∈ S, μ Kᶜ ≤ ε
f : 𝓧 → 𝓨
hf : Continuous[inst✝⁴, inst✝³] f
ε : ENNReal
hε : 0 < ε
K : Set 𝓧
hK_compact : IsCompact K
hKS : ∀ μ ∈ S, μ Kᶜ ≤ ε
μ : Measure 𝓧
hμS : μ ∈ S
hf_meas : ¬AEMeasurable f μ
⊢ (Measure.map f μ) (f '' K)ᶜ ≤ ε

Tactic:
swap

Goal state after:
case neg
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
S : Set (Measure 𝓧)
inst✝⁴ : TopologicalSpace 𝓧
inst✝³ : TopologicalSpace 𝓨
inst✝² : MeasurableSpace 𝓨
inst✝¹ : OpensMeasurableSpace 𝓨
inst✝ : T2Space 𝓨
hS : ∀ (ε : ENNReal), 0 < ε → ∃ K, IsCompact K ∧ ∀ μ ∈ S, μ Kᶜ ≤ ε
f : 𝓧 → 𝓨
hf : Continuous[inst✝⁴, inst✝³] f
ε : ENNReal
hε : 0 < ε
K : Set 𝓧
hK_compact : IsCompact K
hKS : ∀ μ ∈ S, μ Kᶜ ≤ ε
μ : Measure 𝓧
hμS : μ ∈ S
hf_meas : ¬AEMeasurable f μ
⊢ (Measure.map f μ) (f '' K)ᶜ ≤ ε

case pos
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
S : Set (Measure 𝓧)
inst✝⁴ : TopologicalSpace 𝓧
inst✝³ : TopologicalSpace 𝓨
inst✝² : MeasurableSpace 𝓨
inst✝¹ : OpensMeasurableSpace 𝓨
inst✝ : T2Space 𝓨
hS : ∀ (ε : ENNReal), 0 < ε → ∃ K, IsCompact K ∧ ∀ μ ∈ S, μ Kᶜ ≤ ε
f : 𝓧 → 𝓨
hf : Continuous[inst✝⁴, inst✝³] f
ε : ENNReal
hε : 0 < ε
K : Set 𝓧
hK_compact : IsCompact K
hKS : ∀ μ ∈ S, μ Kᶜ ≤ ε
μ : Measure 𝓧
hμS : μ ∈ S
hf_meas : AEMeasurable f μ
⊢ (Measure.map f μ) (f '' K)ᶜ ≤ ε
Module: Mathlib.MeasureTheory.Measure.FiniteMeasure

Goal state before:
pp: Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
p : FiniteMeasure Ω × FiniteMeasure Ω
⊢ ContinuousAt (fun p ↦ p.1 + p.2) p

Tactic:
apply tendsto_iff_forall_lintegral_tendsto.2 (fun g ↦ ?_)

Goal state after:
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
p : FiniteMeasure Ω × FiniteMeasure Ω
g : Ω →ᵇ ℝ≥0
⊢ Tendsto (fun i ↦ ∫⁻ (x : Ω), ↑(g x) ∂↑(i.1 + i.2)) (𝓝 p) (𝓝 (∫⁻ (x : Ω), ↑(g x) ∂↑((fun p ↦ p.1 + p.2) p)))
Module: Mathlib.MeasureTheory.Measure.FiniteMeasure

Goal state before:
pp: Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
p : ℝ≥0 × FiniteMeasure Ω
g : Ω →ᵇ ℝ
A : Tendsto (fun i ↦ i.1) (𝓝 p) (𝓝 p.1)
B : Tendsto (fun i ↦ ∫ (x : Ω), g x ∂↑i.2) (𝓝 p) (𝓝 (∫ (x : Ω), g x ∂↑p.2))
⊢ Tendsto (fun i ↦ ∫ (x : Ω), g x ∂↑(i.1 • i.2)) (𝓝 p) (𝓝 (∫ (x : Ω), g x ∂↑((fun p ↦ p.1 • p.2) p)))

Tactic:
convert! A.smul B with q <;> simp

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

Goal state before:
pp: case refine_2
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
hp : 1 ≤ p
f : ℕ → α → E
hf₁ : ∀ (i : ℕ), AEStronglyMeasurable (f i) μ
hf₂ : UnifIntegrable f p μ
hf₃ : ∃ C, ∀ (i : ℕ), eLpNorm (f i) p μ ≤ ↑C
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ₁ : 0 < δ
hδ₂ :
  ∀ (i : ℕ) (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε
n : ℕ
s : Set α
hs : MeasurableSet s
hle : μ s ≤ ENNReal.ofReal δ
⊢ ∑ i ∈ Finset.range n, eLpNorm (s.indicator ((↑n)⁻¹ • f i)) p μ ≤ ENNReal.ofReal ε

Tactic:
have this i : s.indicator ((n : ℝ)⁻¹ • f i) = (↑n : ℝ)⁻¹ • s.indicator (f i) :=
      indicator_const_smul _ _ _

Goal state after:
case refine_2
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
hp : 1 ≤ p
f : ℕ → α → E
hf₁ : ∀ (i : ℕ), AEStronglyMeasurable (f i) μ
hf₂ : UnifIntegrable f p μ
hf₃ : ∃ C, ∀ (i : ℕ), eLpNorm (f i) p μ ≤ ↑C
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ₁ : 0 < δ
hδ₂ :
  ∀ (i : ℕ) (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε
n : ℕ
s : Set α
hs : MeasurableSet s
hle : μ s ≤ ENNReal.ofReal δ
this : ∀ (i : ℕ), s.indicator ((↑n)⁻¹ • f i) = (↑n)⁻¹ • s.indicator (f i)
⊢ ∑ i ∈ Finset.range n, eLpNorm (s.indicator ((↑n)⁻¹ • f i)) p μ ≤ ENNReal.ofReal ε
Module: Mathlib.MeasureTheory.Measure.FiniteMeasure

Goal state before:
pp: case pos
Ω : Type u_1
Ω' : Type u_2
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSpace Ω'
f : Ω → Ω'
μ : FiniteMeasure Ω
hf : AEMeasurable f ↑μ
⊢ (Measure.map f ↑μ) univ ≤ ↑μ univ

pp: case neg
Ω : Type u_1
Ω' : Type u_2
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSpace Ω'
f : Ω → Ω'
μ : FiniteMeasure Ω
hf : ¬AEMeasurable f ↑μ
⊢ (Measure.map f ↑μ) univ ≤ ↑μ univ

Tactic:
· rw [Measure.map_apply_of_aemeasurable hf MeasurableSet.univ]
    exact measure_mono (subset_univ _)

Goal state after:
case neg
Ω : Type u_1
Ω' : Type u_2
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSpace Ω'
f : Ω → Ω'
μ : FiniteMeasure Ω
hf : ¬AEMeasurable f ↑μ
⊢ (Measure.map f ↑μ) univ ≤ ↑μ univ
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 : α
ha : (κ a) (⋂ i ∈ ∅, univ) = ∏ i ∈ ∅, (κ a) univ
⊢ (κ a) univ = 1

Tactic:
by simpa using ha

Goal state after:
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
⊢ ∀ᵐ (a : α) ∂μ, (κ a) (⋂ i ∈ s, f i) = ∏ i ∈ s, (κ a) (f i)

Tactic:
let f' := Function.extend g f fun _ => ∅

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 ↦ ∅
⊢ ∀ᵐ (a : α) ∂μ, (κ a) (⋂ i ∈ s, f i) = ∏ i ∈ s, (κ a) (f i)
Module: Mathlib.Probability.Independence.Kernel.IndepFun

Goal state before:
pp: α : Type u_1
Ω : Type u_2
β : Type u_4
β' : Type u_5
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
⊢ IndepFun f g κ μ ↔
    ∀ (s : Set β) (t : Set β'),
      MeasurableSet s → MeasurableSet t → ∀ᵐ (a : α) ∂μ, (κ a) (f ⁻¹' s ∩ g ⁻¹' t) = (κ a) (f ⁻¹' s) * (κ a) (g ⁻¹' t)

Tactic:
constructor <;> intro h
  · refine fun s t hs ht => h (f ⁻¹' s) (g ⁻¹' t) ⟨s, hs, rfl⟩ ⟨t, ht, rfl⟩
  · rintro _ _ ⟨s, hs, rfl⟩ ⟨t, ht, rfl⟩; exact h s t hs ht

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

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
_mΩ : MeasurableSpace Ω
μ : Measure Ω
β : ι → Type u_10
mβ : (i : ι) → MeasurableSpace (β i)
f g : (i : ι) → Ω → β i
h : ∀ (i : ι), f i =ᵐ[μ] g i
⊢ ∀ (i : ι), ∀ᵐ (a : Unit) ∂Measure.dirac (), f i =ᵐ[(Kernel.const Unit μ) a] g i

Tactic:
simp [h]

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

Goal state before:
pp: case refine_1.h
Ω : Type u_10
Ω' : Type u_11
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
μ : Measure Ω
ν : Measure Ω'
inst✝³ : IsProbabilityMeasure μ
inst✝² : IsProbabilityMeasure ν
𝓧 : Type u_12
𝓨 : Type u_13
inst✝¹ : MeasurableSpace 𝓧
inst✝ : MeasurableSpace 𝓨
X : Ω → 𝓧
Y : Ω' → 𝓨
mX : AEMeasurable X μ
mY : AEMeasurable Y ν
this : (fun ω ↦ AEMeasurable.mk X mX ω.1) ⟂ᵢ[μ.prod ν] fun ω ↦ AEMeasurable.mk Y mY ω.2
⊢ AEMeasurable.mk X mX =ᵐ[Measure.map Prod.fst (μ.prod ν)] X

Tactic:
rw [measurePreserving_fst.map_eq]
      exact (AEMeasurable.ae_eq_mk mX).symm

Goal state after: