mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Measure.AddContent

Goal state before:
pp: case succ.inr
α : Type u_1
C : Set (Set α)
s t : Set α
I✝ : Finset (Set α)
G✝ : Type u_2
inst✝² : AddCommMonoid G✝
m m' : AddContent G✝ C
inst✝¹ : LinearOrder α
G : Type u_3
inst✝ : AddCommGroup G
f : α → G
n : ℕ
ih :
  ∀ (I : Finset (Set α)),
    ↑I ⊆ {s | ∃ u v, u ≤ v ∧ s = Set.Ioc u v} →
      (↑I).PairwiseDisjoint id →
        ⋃₀ ↑I ∈ {s | ∃ u v, u ≤ v ∧ s = Set.Ioc u v} → #I = n → onIocAux f (⋃₀ ↑I) = ∑ u ∈ I, onIocAux f u
I : Finset (Set α)
hI : ↑I ⊆ {s | ∃ u v, u ≤ v ∧ s = Set.Ioc u v}
h'I : (↑I).PairwiseDisjoint id
hn : #I = n + 1
u v : α
huv✝ : u ≤ v
h'uv : ⋃₀ ↑I = Set.Ioc u v
huv : u < v
this : v ∈ ⋃₀ ↑I
u' : α
uu' : u ≤ u'
hu'v' : u' ≤ v
tI : Set.Ioc u' v ∈ I
ht : v ∈ Set.Ioc u' v
left✝ : v ≤ v
I' : Finset (Set α) := I.erase (Set.Ioc u' v)
⊢ f v - f u = ∑ u ∈ I, onIocAux f u

Tactic:
have I'I : I' ⊆ I := erase_subset (Set.Ioc u' v) I

Goal state after:
case succ.inr
α : Type u_1
C : Set (Set α)
s t : Set α
I✝ : Finset (Set α)
G✝ : Type u_2
inst✝² : AddCommMonoid G✝
m m' : AddContent G✝ C
inst✝¹ : LinearOrder α
G : Type u_3
inst✝ : AddCommGroup G
f : α → G
n : ℕ
ih :
  ∀ (I : Finset (Set α)),
    ↑I ⊆ {s | ∃ u v, u ≤ v ∧ s = Set.Ioc u v} →
      (↑I).PairwiseDisjoint id →
        ⋃₀ ↑I ∈ {s | ∃ u v, u ≤ v ∧ s = Set.Ioc u v} → #I = n → onIocAux f (⋃₀ ↑I) = ∑ u ∈ I, onIocAux f u
I : Finset (Set α)
hI : ↑I ⊆ {s | ∃ u v, u ≤ v ∧ s = Set.Ioc u v}
h'I : (↑I).PairwiseDisjoint id
hn : #I = n + 1
u v : α
huv✝ : u ≤ v
h'uv : ⋃₀ ↑I = Set.Ioc u v
huv : u < v
this : v ∈ ⋃₀ ↑I
u' : α
uu' : u ≤ u'
hu'v' : u' ≤ v
tI : Set.Ioc u' v ∈ I
ht : v ∈ Set.Ioc u' v
left✝ : v ≤ v
I' : Finset (Set α) := I.erase (Set.Ioc u' v)
I'I : I' ⊆ I
⊢ f v - f u = ∑ u ∈ I, onIocAux f u
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.PullOut

Goal state before:
pp: Ω : 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Ω
f : SimpleFunc Ω F
g : Ω → E
hg : Integrable g μ
this :
  ∀ (s : Set Ω) (c : F) (f : Ω → E),
    (fun ω ↦ (B (s.indicator (Function.const Ω c) ω)) (f ω)) = s.indicator fun ω ↦ (B c) (f ω)
g₁ g₂ : SimpleFunc Ω F
x✝ : Disjoint (Function.support ⇑g₁) (Function.support ⇑g₂)
h_eq₁ : μ[fun ω ↦ (B (g₁ ω)) (g ω) | m] =ᵐ[μ] fun ω ↦ (B (g₁ ω)) (μ[g | m] ω)
h_eq₂ : μ[fun ω ↦ (B (g₂ ω)) (g ω) | m] =ᵐ[μ] fun ω ↦ (B (g₂ ω)) (μ[g | m] ω)
h_add : ⇑(g₁ + g₂) = ⇑g₁ + ⇑g₂
⊢ μ[fun ω ↦ (B (g₁ ω + g₂ ω)) (g ω) | m] =ᵐ[μ] μ[fun ω ↦ (B (g₁ ω)) (g ω) | m] + μ[fun ω ↦ (B (g₂ ω)) (g ω) | m]

Tactic:
by
        simp_rw [B.map_add]
        obtain ⟨C₁, hC₁⟩ := @SimpleFunc.exists_forall_norm_le _ _ m _ g₁
        obtain ⟨C₂, hC₂⟩ := @SimpleFunc.exists_forall_norm_le _ _ m _ g₂
        exact condExp_add
          (B.integrable_of_bilin_of_bdd_left C₁ (g₁.stronglyMeasurable.mono hm).aestronglyMeasurable
            (ae_of_all _ hC₁) hg)
          (B.integrable_of_bilin_of_bdd_left C₂ (g₂.stronglyMeasurable.mono hm).aestronglyMeasurable
            (ae_of_all _ hC₂) hg) m

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 β
f : ι → α → β
p : ℝ≥0∞
hf : UnifIntegrable f p μ
E : Set α
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ_pos : 0 < δ
hδε :
  ∀ (i : ι) (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε
i : ι
s : Set α
hs : MeasurableSet s
hμs : μ (toMeasurable μ (s ∩ E)) ≤ ENNReal.ofReal δ
⊢ eLpNorm (s.indicator (f i)) p (μ.restrict E) ≤ ENNReal.ofReal ε

Tactic:
calc
    eLpNorm (indicator s (f i)) p (μ.restrict E) = eLpNorm (f i) p (μ.restrict (s ∩ E)) := by
      rw [eLpNorm_indicator_eq_eLpNorm_restrict hs, μ.restrict_restrict hs]
    _ ≤ eLpNorm (f i) p (μ.restrict (toMeasurable μ (s ∩ E))) :=
      eLpNorm_mono_measure _ <| Measure.restrict_mono (subset_toMeasurable _ _) le_rfl
    _ = eLpNorm (indicator (toMeasurable μ (s ∩ E)) (f i)) p μ :=
      (eLpNorm_indicator_eq_eLpNorm_restrict (measurableSet_toMeasurable _ _)).symm
    _ ≤ ENNReal.ofReal ε := hδε i _ (measurableSet_toMeasurable _ _) hμs

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

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
n m : ℕ
h : n < m
⊢ s.restrictNonposSeq i n ∩ s.restrictNonposSeq i m = ∅

Tactic:
Set.eq_empty_iff_forall_notMem

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
n m : ℕ
h : n < m
⊢ ∀ (x : α), x ∉ s.restrictNonposSeq i n ∩ s.restrictNonposSeq i m
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan

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

Tactic:
if_pos hr

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

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

Tactic:
if_pos hr

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

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α := ⋯.choose
⊢ ∃ i,
    ∃ (hi₁ : MeasurableSet i) (hi₂ : 0 ≤[i] s) (hi₃ : s ≤[iᶜ] 0),
      s.toJordanDecomposition.posPart = s.toMeasureOfZeroLE i hi₁ hi₂ ∧
        s.toJordanDecomposition.negPart = s.toMeasureOfLEZero iᶜ ⋯ hi₃

Tactic:
obtain ⟨hi₁, hi₂, hi₃⟩ := s.exists_compl_positive_negative.choose_spec

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α := ⋯.choose
hi₁ : MeasurableSet ⋯.choose
hi₂ : 0 ≤[⋯.choose] s
hi₃ : s ≤[⋯.chooseᶜ] 0
⊢ ∃ i,
    ∃ (hi₁ : MeasurableSet i) (hi₂ : 0 ≤[i] s) (hi₃ : s ≤[iᶜ] 0),
      s.toJordanDecomposition.posPart = s.toMeasureOfZeroLE i hi₁ hi₂ ∧
        s.toJordanDecomposition.negPart = s.toMeasureOfLEZero iᶜ ⋯ hi₃
Module: Mathlib.MeasureTheory.VectorMeasure.WithDensity

Goal state before:
pp: case pos
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
i : Set α
hi₁ : MeasurableSet i
hi₂ : μ i = 0
⊢ (μ.withDensityᵥ f) i = 0

Tactic:
rw [withDensityᵥ_apply hf hi₁, Measure.restrict_zero_set hi₂, integral_zero_measure]

Goal state after:
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 : ε < ∞
hμ : ¬μ = 0
hε' : 0 < ε.toReal / 3
hdivp : 0 ≤ 1 / p.toReal
hpow : 0 < measureUnivNNReal μ ^ (1 / p.toReal)
δ₁ : ℝ
hδ₁ : 0 < δ₁
heLpNorm₁ :
  ∀ (i : ℕ) (s : Set α),
    MeasurableSet s → μ s ≤ ENNReal.ofReal δ₁ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal (ε.toReal / 3)
δ₂ : ℝ
hδ₂ : 0 < δ₂
heLpNorm₂ :
  ∀ (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ₂ → eLpNorm (s.indicator g) p μ ≤ ENNReal.ofReal (ε.toReal / 3)
t : Set α
htm : MeasurableSet t
ht₁ : μ t ≤ ENNReal.ofReal (min δ₁ δ₂)
N n : ℕ
hN : ∀ x ∈ tᶜ, dist (g x) (f n x) < ε.toReal / (3 * ↑(measureUnivNNReal μ) ^ (1 / p.toReal))
hn : n ≥ N
hnf : eLpNorm (t.indicator (f n)) p μ ≤ ENNReal.ofReal (ε.toReal / 3)
hng : eLpNorm (t.indicator g) p μ ≤ ENNReal.ofReal (ε.toReal / 3)
this✝ : 0 ≤ ε.toReal / (3 * ↑(measureUnivNNReal μ) ^ (1 / p.toReal))
this :
  eLpNorm (tᶜ.indicator (f n - g)) p μ ≤
    ENNReal.ofReal (ε.toReal / (3 * ↑(measureUnivNNReal μ) ^ (1 / p.toReal))) * μ tᶜ ^ (1 / p.toReal)
⊢ (μ tᶜ).toReal ^ (1 / p.toReal) ≤ ↑(measureUnivNNReal μ) ^ (1 / p.toReal)

Tactic:
gcongr
        refine (ENNReal.toReal_le_of_le_ofReal (measureUnivNNReal_pos hμ).le ?_)
        rw [ENNReal.ofReal_coe_nnreal, coe_measureUnivNNReal]
        exact measure_mono (Set.subset_univ _)

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
r : ℝ≥0
⊢ (r • s).singularPart μ = r • s.singularPart μ

Tactic:
by
  rw [singularPart, singularPart, smul_sub, ← toSignedMeasure_smul, ← toSignedMeasure_smul]
  conv_lhs =>
    congr
    · congr
      · rw [toJordanDecomposition_smul, JordanDecomposition.smul_posPart, singularPart_smul]
    · congr
      rw [toJordanDecomposition_smul, JordanDecomposition.smul_negPart, singularPart_smul]

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

Goal state before:
pp: case inr
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
r : ℝ
hr : r < 0
⊢ ((-r).toNNReal • s.toJordanDecomposition.negPart.singularPart μ).toSignedMeasure -
      ((-r).toNNReal • s.toJordanDecomposition.posPart.singularPart μ).toSignedMeasure =
    r •
      ((s.toJordanDecomposition.posPart.singularPart μ).toSignedMeasure -
        (s.toJordanDecomposition.negPart.singularPart μ).toSignedMeasure)

Tactic:
rw [toSignedMeasure_smul, toSignedMeasure_smul, ← neg_sub, ← smul_sub, NNReal.smul_def,
      ← neg_smul, Real.coe_toNNReal _ (le_of_lt (neg_pos.mpr hr)), neg_neg]

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
c : ComplexMeasure α
μ : Measure α
⊢ Integrable (c.rnDeriv μ) μ

Tactic:
← memLp_one_iff_integrable,

Goal state after:
α : Type u_1
m : MeasurableSpace α
c : ComplexMeasure α
μ : Measure α
⊢ MemLp (c.rnDeriv μ) 1 μ
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
hfint : ¬Integrable f μ
⊢ ∫ (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
f : α → E
hfint : Integrable f μ
⊢ ∫ (x : α), ‖μ[f | m] x‖ ∂μ ≤ ∫ (x : α), ‖f x‖ ∂μ

Tactic:
· simpa [condExp_of_not_integrable hfint] using integral_nonneg (fun x => norm_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
f : α → E
hfint : Integrable f μ
⊢ ∫ (x : α), ‖μ[f | m] x‖ ∂μ ≤ ∫ (x : α), ‖f x‖ ∂μ
Module: Mathlib.MeasureTheory.Measure.FiniteMeasure

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
Heval : ∀ {u : Set α} {v : Set β}, MeasurableSet u → MeasurableSet v → Measurable fun a ↦ ↑a.1 u * ↑a.2 v
⊢ ∀ (s : Set (α × β)) (x : Set α),
    MeasurableSet x → ∀ (x_1 : Set β), MeasurableSet x_1 → x ×ˢ x_1 = s → Measurable fun a ↦ ((↑a.1).prod ↑a.2) s

Tactic:
intro _ _ Hu _ Hv Heq

Goal state after:
α : Type u_3
β : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
Heval : ∀ {u : Set α} {v : Set β}, MeasurableSet u → MeasurableSet v → Measurable fun a ↦ ↑a.1 u * ↑a.2 v
s✝ : Set (α × β)
x✝¹ : Set α
Hu : MeasurableSet x✝¹
x✝ : Set β
Hv : MeasurableSet x✝
Heq : x✝¹ ×ˢ x✝ = s✝
⊢ Measurable fun a ↦ ((↑a.1).prod ↑a.2) s✝
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
s : Set α
hs : MeasurableSet s
f : α → E
hfint : ¬Integrable f μ
⊢ ∫ (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
s : Set α
hs : MeasurableSet s
f : α → E
hfint : Integrable f μ
⊢ ∫ (x : α) in s, ‖μ[f | m] x‖ ∂μ ≤ ∫ (x : α) in s, ‖f x‖ ∂μ

Tactic:
· simpa [condExp_of_not_integrable hfint] using integral_nonneg (fun x => norm_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
s : Set α
hs : MeasurableSet s
f : α → E
hfint : Integrable f μ
⊢ ∫ (x : α) in s, ‖μ[f | m] x‖ ∂μ ≤ ∫ (x : α) in s, ‖f x‖ ∂μ
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
p : ℝ≥0∞
hp : 1 ≤ p
hf : MemLp f p μ
⊢ MemLp μ[f | m] p μ

Tactic:
have hp' : 0 < p := zero_lt_one.trans_le hp
  by_cases! hpt : p ≠ ⊤
  · rw [← integrable_norm_rpow_iff integrable_condExp.1 hp'.ne.symm hpt]
    have hp : 1 ≤ p.toReal := by
      rwa [← ENNReal.toReal_one, ENNReal.toReal_le_toReal ENNReal.one_ne_top hpt]
    have := Integrable.norm_condExp_rpow_le (m := m) hp <|
      (integrable_norm_rpow_iff hf.1 hp'.ne.symm hpt).2 hf
    refine Integrable.mono_nonneg integrable_condExp ?_ ?_ this
    · fun_prop (discharger := simp)
    · filter_upwards with a; positivity
  · simp_all only
    exact memLp_top_of_bound integrable_condExp.1 (essSup (‖f ·‖) μ) hf.ae_norm_condExp_le_essSup

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 : ι → α → β
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
δ : ℝ
hδpos : 0 < δ
hδ :
  ∀ (i : ι) (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε
⊢ ∃ C, ∀ (i : ι), μ {x | C ≤ ‖f i x‖₊} ≤ ENNReal.ofReal δ

Tactic:
by_contra! hcon
    choose ℐ hℐ using hcon
    lift δ to ℝ≥0 using hδpos.le
    have : ∀ C : ℝ≥0, C • (δ : ℝ≥0∞) ^ (1 / p.toReal) ≤ eLpNorm (f (ℐ C)) p μ := by
      intro C
      calc
        C • (δ : ℝ≥0∞) ^ (1 / p.toReal) ≤ C • μ { x | C ≤ ‖f (ℐ C) x‖₊ } ^ (1 / p.toReal) := by
          rw [ENNReal.smul_def, ENNReal.smul_def, smul_eq_mul, smul_eq_mul]
          simp_rw [ENNReal.ofReal_coe_nnreal] at hℐ
          refine mul_le_mul' le_rfl
            (ENNReal.rpow_le_rpow (hℐ C).le (one_div_nonneg.2 ENNReal.toReal_nonneg))
        _ ≤ eLpNorm ({ x | C ≤ ‖f (ℐ C) x‖₊ }.indicator (f (ℐ C))) p μ := by
          refine le_eLpNorm_of_bddBelow hp hp' _
            (measurableSet_le measurable_const (hf _).nnnorm.measurable)
            (Eventually.of_forall fun x hx => ?_)
          rwa [nnnorm_indicator_eq_indicator_nnnorm, Set.indicator_of_mem hx]
        _ ≤ eLpNorm (f (ℐ C)) p μ := eLpNorm_indicator_le _
    specialize this (2 * max M 1 * δ⁻¹ ^ (1 / p.toReal))
    rw [← ENNReal.coe_rpow_of_nonneg _ (one_div_nonneg.2 ENNReal.toReal_nonneg), ← ENNReal.coe_smul,
      smul_eq_mul, mul_assoc, NNReal.inv_rpow,
      inv_mul_cancel₀ (NNReal.rpow_pos (NNReal.coe_pos.1 hδpos)).ne.symm, mul_one, ENNReal.coe_mul,
      ← NNReal.inv_rpow] at this
    refine (lt_of_le_of_lt (le_trans
      (hM <| ℐ <| 2 * max M 1 * δ⁻¹ ^ (1 / p.toReal)) (le_max_left (M : ℝ≥0∞) 1))
        (lt_of_lt_of_le ?_ this)).ne rfl
    rw [← ENNReal.coe_one, ← ENNReal.coe_max, ← ENNReal.coe_mul, ENNReal.coe_lt_coe]
    exact lt_two_mul_self (lt_max_of_lt_right one_pos)

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

Goal state before:
pp: case refine_1
α : 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) (⋂ i ∈ a✝², a✝¹ i) = ∏ i ∈ a✝², (η a) (a✝¹ i)

Tactic:
filter_upwards [h, h'] with a ha h'a
    simpa [ha] using h'a

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

Goal state before:
pp: case refine_2
α : 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) (⋂ i ∈ a✝², a✝¹ i) = ∏ i ∈ a✝², (κ a) (a✝¹ i)

Tactic:
filter_upwards [h, h'] with a ha h'a
    simpa [ha] using h'a

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

Goal state before:
pp: case refine_1
α : 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✝²

Tactic:
filter_upwards [h, h'] with a ha h'a
    simpa [ha] using h'a

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

Goal state before:
pp: case refine_2
α : 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✝²

Tactic:
filter_upwards [h, h'] with a ha h'a
    simpa [ha] using h'a

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∞
κ : Type u_4
u : Filter κ
inst✝¹ : u.NeBot
inst✝ : u.IsCountablyGenerated
fn : ι → α → β
hUI : UniformIntegrable fn p μ
⊢ UniformIntegrable (fun f ↦ ↑f) p μ

Tactic:
by
  refine ⟨fun ⟨f, s, hs⟩ => ?_, hUI.2.1.unifIntegrable_of_tendstoInMeasure u (fun i => hUI.1 i), ?_⟩
  · exact hs.aestronglyMeasurable (fun n => hUI.1 (s n))
  · obtain ⟨C, hC⟩ := hUI.2.2
    exact ⟨C, fun ⟨f, s, hs⟩ => eLpNorm_le_of_tendstoInMeasure
      (Eventually.of_forall fun n => hC (s n)) hs (fun n => hUI.1 (s n))⟩

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

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

Tactic:
exact h s t hs ht

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

Goal state before:
pp: α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → Set (Set Ω)
s' : Set (Set Ω)
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
u : Set ι
t1 t2 : Set Ω
ht1 : t1 ∈ ⋂ n ∈ u, s n
ht2 : t2 ∈ s'
n : ι
hn : n ∈ u
h : IndepSets (s n) s' κ μ
⊢ ∀ᵐ (a : α) ∂μ, (κ a) (t1 ∩ t2) = (κ a) t1 * (κ a) t2

Tactic:
exact h t1 t2 (Set.biInter_subset_of_mem hn ht1) ht2

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

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
x✝ : MeasurableSpace Ω
π : ι → Set (Set Ω)
μ : Measure Ω
⊢ iIndepSets π μ ↔ ∀ (s : Finset ι) {f : ι → Set Ω}, (∀ i ∈ s, f i ∈ π i) → μ (⋂ i ∈ s, f i) = ∏ i ∈ s, μ (f i)

Tactic:
by
  simp only [iIndepSets, Kernel.iIndepSets, ae_dirac_eq, Filter.eventually_pure, Kernel.const_apply]

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

Goal state before:
pp: α : Type u_1
Ω : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
β : ι → Type u_8
mβ : (i : ι) → MeasurableSpace (β i)
f g : (i : ι) → Ω → β i
h : ∀ (i : ι), ∀ᵐ (a : α) ∂μ, f i =ᵐ[κ a] g i
h' : iIndepFun g κ μ
⊢ iIndepFun f κ μ

Tactic:
refine h'.congr' fun i ↦ ?_
    filter_upwards [h i] with a ha using ha.symm

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

Goal state before:
pp: Ω : Type u_1
β : Type u_6
β' : Type u_7
_mΩ : MeasurableSpace Ω
μ : Measure Ω
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
hf : AEMeasurable f μ
hg : AEMeasurable g μ
σf : SigmaFinite (Measure.map f μ)
σg : SigmaFinite (Measure.map g μ)
⊢ f ⟂ᵢ[μ] g ↔ Measure.map (fun ω ↦ (f ω, g ω)) μ = (Measure.map f μ).prod (Measure.map g μ)

Tactic:
rw [indepFun_iff_measure_inter_preimage_eq_mul]
  have h₀ {s : Set β} {t : Set β'} (hs : MeasurableSet s) (ht : MeasurableSet t) :
      μ (f ⁻¹' s) * μ (g ⁻¹' t) = μ.map f s * μ.map g t ∧
      μ (f ⁻¹' s ∩ g ⁻¹' t) = μ.map (fun ω ↦ (f ω, g ω)) (s ×ˢ t) :=
    ⟨by rw [Measure.map_apply_of_aemeasurable hf hs, Measure.map_apply_of_aemeasurable hg ht],
      (Measure.map_apply_of_aemeasurable (hf.prodMk hg) (hs.prod ht)).symm⟩
  constructor
  · refine fun h ↦ (Measure.prod_eq fun s t hs ht ↦ ?_).symm
    rw [← (h₀ hs ht).1, ← (h₀ hs ht).2, h s t hs ht]
  · intro h s t hs ht
    rw [(h₀ hs ht).1, (h₀ hs ht).2, h, Measure.prod_prod]

Goal state after:
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 β'
inst✝ : IsZeroOrMarkovKernel κ
hf : Measurable f
hg : Measurable g
⊢ IndepFun f g κ μ ↔ ∀ (s : Set β) (t : Set β'), MeasurableSet s → MeasurableSet t → IndepSet (f ⁻¹' s) (g ⁻¹' t) κ μ

Tactic:
by
  refine indepFun_iff_measure_inter_preimage_eq_mul.trans ?_
  constructor <;> intro h s t hs ht <;> specialize h s t hs ht
  · rwa [indepSet_iff_measure_inter_eq_mul (hf hs) (hg ht) κ μ]
  · rwa [← indepSet_iff_measure_inter_eq_mul (hf hs) (hg ht) κ μ]

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

Goal state before:
pp: α : Type u_1
ι : Type u_3
_mα : MeasurableSpace α
Ω : Type u_4
m : ι → MeasurableSpace Ω
m' m0 : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst✝ : IsZeroOrMarkovKernel κ
h_indep : ∀ (i : ι), Indep (m i) m' κ μ
h_le : ∀ (i : ι), m i ≤ m0
h_le' : m' ≤ m0
hm : Directed (fun x1 x2 ↦ x1 ≤ x2) m
p : ι → Set (Set Ω) := fun n ↦ {t | MeasurableSet t}
hp : ∀ (n : ι), IsPiSystem (p n)
h_gen_n : ∀ (n : ι), m n = generateFrom (p n)
hp_supr_pi : IsPiSystem (⋃ n, p n)
p' : Set (Set Ω) := {t | MeasurableSet t}
hp'_pi : IsPiSystem p'
h_gen' : m' = generateFrom p'
⊢ Indep (⨆ i, m i) m' κ μ

Tactic:
have h_pi_system_indep : IndepSets (⋃ n, p n) p' κ μ := by
    refine IndepSets.iUnion ?_
    conv at h_indep =>
      intro i
      rw [h_gen_n i, h_gen']
    exact fun n => (h_indep n).indepSets

Goal state after:
α : Type u_1
ι : Type u_3
_mα : MeasurableSpace α
Ω : Type u_4
m : ι → MeasurableSpace Ω
m' m0 : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst✝ : IsZeroOrMarkovKernel κ
h_indep : ∀ (i : ι), Indep (m i) m' κ μ
h_le : ∀ (i : ι), m i ≤ m0
h_le' : m' ≤ m0
hm : Directed (fun x1 x2 ↦ x1 ≤ x2) m
p : ι → Set (Set Ω) := fun n ↦ {t | MeasurableSet t}
hp : ∀ (n : ι), IsPiSystem (p n)
h_gen_n : ∀ (n : ι), m n = generateFrom (p n)
hp_supr_pi : IsPiSystem (⋃ n, p n)
p' : Set (Set Ω) := {t | MeasurableSet t}
hp'_pi : IsPiSystem p'
h_gen' : m' = generateFrom p'
h_pi_system_indep : IndepSets (⋃ n, p n) p' κ μ
⊢ Indep (⨆ i, m i) m' κ μ