mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Probability.Independence.Integration

Goal state before:
pp: Ω : Type u_1
Mf mΩ : MeasurableSpace Ω
μ : Measure Ω
hMf : Mf ≤ mΩ
c : ℝ≥0∞
T : Set Ω
h_meas_T : MeasurableSet T
h_ind : IndepSets {s | MeasurableSet s} {T} μ
h_mul_indicator : ∀ (g : Ω → ℝ≥0∞), Measurable g → Measurable fun a ↦ g a * T.indicator (fun x ↦ c) a
⊢ ∀ {f : Ω → ℝ≥0∞},
    Measurable f →
      ∫⁻ (ω : Ω), f ω * T.indicator (fun x ↦ c) ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), T.indicator (fun x ↦ c) ω ∂μ

Tactic:
apply @Measurable.ennreal_induction _ Mf

Goal state after:
case indicator
Ω : Type u_1
Mf mΩ : MeasurableSpace Ω
μ : Measure Ω
hMf : Mf ≤ mΩ
c : ℝ≥0∞
T : Set Ω
h_meas_T : MeasurableSet T
h_ind : IndepSets {s | MeasurableSet s} {T} μ
h_mul_indicator : ∀ (g : Ω → ℝ≥0∞), Measurable g → Measurable fun a ↦ g a * T.indicator (fun x ↦ c) a
⊢ ∀ (c_1 : ℝ≥0∞) ⦃s : Set Ω⦄,
    MeasurableSet s →
      ∫⁻ (ω : Ω), s.indicator (fun x ↦ c_1) ω * T.indicator (fun x ↦ c) ω ∂μ =
        (∫⁻ (ω : Ω), s.indicator (fun x ↦ c_1) ω ∂μ) * ∫⁻ (ω : Ω), T.indicator (fun x ↦ c) ω ∂μ

case add
Ω : Type u_1
Mf mΩ : MeasurableSpace Ω
μ : Measure Ω
hMf : Mf ≤ mΩ
c : ℝ≥0∞
T : Set Ω
h_meas_T : MeasurableSet T
h_ind : IndepSets {s | MeasurableSet s} {T} μ
h_mul_indicator : ∀ (g : Ω → ℝ≥0∞), Measurable g → Measurable fun a ↦ g a * T.indicator (fun x ↦ c) a
⊢ ∀ ⦃f g : Ω → ℝ≥0∞⦄,
    Disjoint (Function.support f) (Function.support g) →
      Measurable f →
        Measurable g →
          ∫⁻ (ω : Ω), f ω * T.indicator (fun x ↦ c) ω ∂μ =
              (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), T.indicator (fun x ↦ c) ω ∂μ →
            ∫⁻ (ω : Ω), g ω * T.indicator (fun x ↦ c) ω ∂μ =
                (∫⁻ (ω : Ω), g ω ∂μ) * ∫⁻ (ω : Ω), T.indicator (fun x ↦ c) ω ∂μ →
              ∫⁻ (ω : Ω), (f + g) ω * T.indicator (fun x ↦ c) ω ∂μ =
                (∫⁻ (ω : Ω), (f + g) ω ∂μ) * ∫⁻ (ω : Ω), T.indicator (fun x ↦ c) ω ∂μ

case iSup
Ω : Type u_1
Mf mΩ : MeasurableSpace Ω
μ : Measure Ω
hMf : Mf ≤ mΩ
c : ℝ≥0∞
T : Set Ω
h_meas_T : MeasurableSet T
h_ind : IndepSets {s | MeasurableSet s} {T} μ
h_mul_indicator : ∀ (g : Ω → ℝ≥0∞), Measurable g → Measurable fun a ↦ g a * T.indicator (fun x ↦ c) a
⊢ ∀ ⦃f : ℕ → Ω → ℝ≥0∞⦄,
    (∀ (n : ℕ), Measurable (f n)) →
      Monotone f →
        (∀ (n : ℕ),
            ∫⁻ (ω : Ω), f n ω * T.indicator (fun x ↦ c) ω ∂μ =
              (∫⁻ (ω : Ω), f n ω ∂μ) * ∫⁻ (ω : Ω), T.indicator (fun x ↦ c) ω ∂μ) →
          ∫⁻ (ω : Ω), (fun x ↦ ⨆ n, f n x) ω * T.indicator (fun x ↦ c) ω ∂μ =
            (∫⁻ (ω : Ω), (fun x ↦ ⨆ n, f n x) ω ∂μ) * ∫⁻ (ω : Ω), T.indicator (fun x ↦ c) ω ∂μ
Module: Mathlib.Probability.Moments.Variance

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
hX : AEStronglyMeasurable X μ
c : ℝ
⊢ Var[fun ω ↦ X ω - c; μ] = Var[X; μ]

Tactic:
sub_eq_add_neg,

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
hX : AEStronglyMeasurable X μ
c : ℝ
⊢ Var[fun ω ↦ X ω + -c; μ] = Var[X; μ]
Module: Mathlib.Probability.Moments.Variance

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
⊢ Var[X - Y; μ] = Var[X; μ] - 2 * cov[X, Y; μ] + Var[Y; μ]

Tactic:
sub_eq_add_neg,

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
⊢ Var[X + -Y; μ] = Var[X; μ] - 2 * cov[X, Y; μ] + Var[Y; μ]
Module: Mathlib.Probability.Moments.Covariance

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y Z : Ω → ℝ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
hZ : MemLp Z 2 μ
⊢ cov[X - Y, Z; μ] = cov[X, Z; μ] - cov[Y, Z; μ]

Tactic:
sub_eq_add_neg,

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y Z : Ω → ℝ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
hZ : MemLp Z 2 μ
⊢ cov[X + -Y, Z; μ] = cov[X, Z; μ] + -cov[Y, Z; μ]
Module: Mathlib.Probability.Moments.Variance

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
inst✝ : MeasurableSingletonClass Ω
x : Ω
⊢ Var[X; Measure.dirac x] = 0

Tactic:
variance_eq_integral

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
inst✝ : MeasurableSingletonClass Ω
x : Ω
⊢ ∫ (ω : Ω), (X ω - ∫ (x : Ω), X x ∂Measure.dirac x) ^ 2 ∂Measure.dirac x = 0

Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
inst✝ : MeasurableSingletonClass Ω
x : Ω
⊢ AEMeasurable X (Measure.dirac x)
Module: Mathlib.Probability.Moments.Covariance

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y Z : Ω → ℝ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
hZ : MemLp Z 2 μ
⊢ cov[X, Y - Z; μ] = cov[X, Y; μ] - cov[X, Z; μ]

Tactic:
sub_eq_add_neg,

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y Z : Ω → ℝ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
hZ : MemLp Z 2 μ
⊢ cov[X, Y + -Z; μ] = cov[X, Y; μ] + -cov[X, Z; μ]
Module: Mathlib.Probability.Moments.Covariance

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_2
X : ι → Ω → ℝ
s : Finset ι
inst✝ : IsFiniteMeasure μ
ι' : Type u_3
Y : ι' → Ω → ℝ
t : Finset ι'
hX : ∀ i ∈ s, MemLp (X i) 2 μ
hY : ∀ i ∈ t, MemLp (Y i) 2 μ
⊢ MemLp (∑ j ∈ t, Y j) 2 μ

Tactic:
exact memLp_finsetSum' t hY

Goal state after:
Module: Mathlib.Probability.Moments.Variance

Goal state before:
pp: case e'_3
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
hX : AEStronglyMeasurable X μ
c : ℝ≥0
hc : c ≠ 0
A : ↑c ≠ 0
B : AEStronglyMeasurable (fun x ↦ ∫ (x : Ω), X x ∂μ) μ
⊢ μ {ω | ↑c ≤ |X ω - ∫ (x : Ω), X x ∂μ|} = μ {x | ↑c ≤ ‖(X - fun x ↦ ∫ (x : Ω), X x ∂μ) x‖ₑ}

pp: case e'_4
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
hX : AEStronglyMeasurable X μ
c : ℝ≥0
hc : c ≠ 0
A : ↑c ≠ 0
B : AEStronglyMeasurable (fun x ↦ ∫ (x : Ω), X x ∂μ) μ
⊢ eVar[X; μ] / ↑c ^ 2 = (↑c)⁻¹ ^ ENNReal.toReal 2 * eLpNorm (X - fun x ↦ ∫ (x : Ω), X x ∂μ) 2 μ ^ ENNReal.toReal 2

Tactic:
· norm_cast

Goal state after:
case e'_4
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
hX : AEStronglyMeasurable X μ
c : ℝ≥0
hc : c ≠ 0
A : ↑c ≠ 0
B : AEStronglyMeasurable (fun x ↦ ∫ (x : Ω), X x ∂μ) μ
⊢ eVar[X; μ] / ↑c ^ 2 = (↑c)⁻¹ ^ ENNReal.toReal 2 * eLpNorm (X - fun x ↦ ∫ (x : Ω), X x ∂μ) 2 μ ^ ENNReal.toReal 2
Module: Mathlib.Probability.Moments.Variance

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X Y : Ω → ℝ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
h : X ⟂ᵢ[μ] Y
⊢ Var[X + Y; μ] = Var[X; μ] + Var[Y; μ]

Tactic:
by_cases h' : X =ᵐ[μ] 0

Goal state after:
case pos
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X Y : Ω → ℝ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
h : X ⟂ᵢ[μ] Y
h' : X =ᵐ[μ] 0
⊢ Var[X + Y; μ] = Var[X; μ] + Var[Y; μ]

case neg
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X Y : Ω → ℝ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
h : X ⟂ᵢ[μ] Y
h' : ¬X =ᵐ[μ] 0
⊢ Var[X + Y; μ] = Var[X; μ] + Var[Y; μ]
Module: Mathlib.Probability.Moments.Variance

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_3
X : ι → Ω → ℝ
s : Finset ι
hs : ∀ i ∈ s, MemLp (X i) 2 μ
h : (↑s).Pairwise fun i j ↦ X i ⟂ᵢ[μ] X j
⊢ Var[∑ i ∈ s, X i; μ] = ∑ i ∈ s, Var[X i; μ]

Tactic:
by
  by_cases h'' : ∀ i ∈ s, X i =ᵐ[μ] 0
  · rw [variance_congr (Y := 0), variance_zero]
    · symm
      refine Finset.sum_eq_zero fun i hi ↦ ?_
      simp [variance_congr (h'' i hi)]
    · have := fun (i : s) ↦ h'' i.1 i.2
      filter_upwards [ae_all_iff.2 this] with ω hω
      simp only [Finset.sum_apply, Pi.zero_apply]
      exact Finset.sum_eq_zero fun i hi ↦ hω ⟨i, hi⟩
  obtain ⟨j, hj1, hj2⟩ := not_forall₂.1 h''
  obtain rfl | h' := s.eq_singleton_or_nontrivial hj1
  · simp
  obtain ⟨k, hk1, hk2⟩ := h'.exists_ne j
  have := (hs j hj1).isProbabilityMeasure_of_indepFun (X j) (X k) (by simp) (by simp) hj2
    (h hj1 hk1 hk2.symm)
  rw [variance_sum' hs]
  refine Finset.sum_congr rfl (fun i hi ↦ ?_)
  rw [← covariance_self (hs i hi).aemeasurable]
  refine Finset.sum_eq_single_of_mem i hi fun j hj1 hj2 ↦ ?_
  exact (h hi hj1 hj2.symm).covariance_eq_zero (hs i hi) (hs j hj1)

Goal state after:
Module: Mathlib.Probability.IdentDistrib

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace γ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
inst✝² : NormedAddCommGroup γ
inst✝¹ : NormedSpace ℝ γ
inst✝ : BorelSpace γ
h : IdentDistrib f g μ ν
hf : ¬AEStronglyMeasurable f μ
⊢ 0 = ∫ (x : β), g x ∂ν

Tactic:
h.aestronglyMeasurable_iff

Goal state after:
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace γ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
inst✝² : NormedAddCommGroup γ
inst✝¹ : NormedSpace ℝ γ
inst✝ : BorelSpace γ
h : IdentDistrib f g μ ν
hf : ¬AEStronglyMeasurable g ν
⊢ 0 = ∫ (x : β), g x ∂ν
Module: Mathlib.Probability.Independence.Integration

Goal state before:
pp: Ω : Type u_1
𝕜 : Type u_2
inst✝¹ : RCLike 𝕜
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_3
inst✝ : Fintype ι
𝓧 : ι → Type u_4
m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)
X : (i : ι) → Ω → 𝓧 i
f : (i : ι) → 𝓧 i → 𝕜
hX : iIndepFun X μ
mX : ∀ (i : ι), AEMeasurable (X i) μ
hf : ∀ (i : ι), AEStronglyMeasurable (f i) (Measure.map (X i) μ)
this : IsProbabilityMeasure μ
⊢ (∫ (y : (x : ι) → 𝓧 x), ∏ i, f i (y i) ∂Measure.pi fun i ↦ Measure.map (X i) μ) = ∏ i, ∫ (ω : Ω), f i (X i ω) ∂μ

pp: case hφ
Ω : Type u_1
𝕜 : Type u_2
inst✝¹ : RCLike 𝕜
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_3
inst✝ : Fintype ι
𝓧 : ι → Type u_4
m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)
X : (i : ι) → Ω → 𝓧 i
f : (i : ι) → 𝓧 i → 𝕜
hX : iIndepFun X μ
mX : ∀ (i : ι), AEMeasurable (X i) μ
hf : ∀ (i : ι), AEStronglyMeasurable (f i) (Measure.map (X i) μ)
this : IsProbabilityMeasure μ
⊢ AEMeasurable (fun ω x ↦ X x ω) μ

pp: case hfm
Ω : Type u_1
𝕜 : Type u_2
inst✝¹ : RCLike 𝕜
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_3
inst✝ : Fintype ι
𝓧 : ι → Type u_4
m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)
X : (i : ι) → Ω → 𝓧 i
f : (i : ι) → 𝓧 i → 𝕜
hX : iIndepFun X μ
mX : ∀ (i : ι), AEMeasurable (X i) μ
hf : ∀ (i : ι), AEStronglyMeasurable (f i) (Measure.map (X i) μ)
this : IsProbabilityMeasure μ
⊢ AEStronglyMeasurable (fun x ↦ ∏ i, f i (x i)) (Measure.map (fun ω x ↦ X x ω) μ)

Tactic:
integral_fintype_prod_eq_prod

Goal state after:
Ω : Type u_1
𝕜 : Type u_2
inst✝¹ : RCLike 𝕜
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_3
inst✝ : Fintype ι
𝓧 : ι → Type u_4
m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)
X : (i : ι) → Ω → 𝓧 i
f : (i : ι) → 𝓧 i → 𝕜
hX : iIndepFun X μ
mX : ∀ (i : ι), AEMeasurable (X i) μ
hf : ∀ (i : ι), AEStronglyMeasurable (f i) (Measure.map (X i) μ)
this : IsProbabilityMeasure μ
⊢ ∏ i, ∫ (x : 𝓧 i), f i x ∂Measure.map (X i) μ = ∏ i, ∫ (ω : Ω), f i (X i ω) ∂μ

case hφ
Ω : Type u_1
𝕜 : Type u_2
inst✝¹ : RCLike 𝕜
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_3
inst✝ : Fintype ι
𝓧 : ι → Type u_4
m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)
X : (i : ι) → Ω → 𝓧 i
f : (i : ι) → 𝓧 i → 𝕜
hX : iIndepFun X μ
mX : ∀ (i : ι), AEMeasurable (X i) μ
hf : ∀ (i : ι), AEStronglyMeasurable (f i) (Measure.map (X i) μ)
this : IsProbabilityMeasure μ
⊢ AEMeasurable (fun ω x ↦ X x ω) μ

case hfm
Ω : Type u_1
𝕜 : Type u_2
inst✝¹ : RCLike 𝕜
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_3
inst✝ : Fintype ι
𝓧 : ι → Type u_4
m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)
X : (i : ι) → Ω → 𝓧 i
f : (i : ι) → 𝓧 i → 𝕜
hX : iIndepFun X μ
mX : ∀ (i : ι), AEMeasurable (X i) μ
hf : ∀ (i : ι), AEStronglyMeasurable (f i) (Measure.map (X i) μ)
this : IsProbabilityMeasure μ
⊢ AEStronglyMeasurable (fun x ↦ ∏ i, f i (x i)) (Measure.map (fun ω x ↦ X x ω) μ)
Module: Mathlib.Probability.IdentDistrib

Goal state before:
pp: case pos
α : Type u_1
inst✝⁴ : MeasurableSpace α
E : Type u_5
inst✝³ : MeasurableSpace E
inst✝² : NormedAddCommGroup E
inst✝¹ : BorelSpace E
μ : Measure α
inst✝ : IsFiniteMeasure μ
ι : Type u_6
f : ι → α → E
j : ι
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
hℒp : MemLp (f j) p μ
hfmeas : ∀ (i : ι), StronglyMeasurable (f i)
hf : ∀ (i : ι), IdentDistrib (f i) (f j) μ μ
ε : ℝ
hε : 0 < ε
hι : Nonempty ι
C : ℝ
hC₁ : 0 < C
hC₂ : eLpNorm ({x | C ≤ ↑‖f j x‖₊}.indicator (f j)) p μ ≤ ENNReal.ofReal ε
i : ι
this✝ : {x | ⟨C, ⋯⟩ ≤ ‖f i x‖₊} = {x | C ≤ ‖f i x‖}
F : E → ℝ := fun x ↦ if ⟨C, ⋯⟩ ≤ ‖x‖₊ then ‖x‖ else 0
F_meas : Measurable F
this : ∀ (k : ι), (fun x ↦ {x | C ≤ ‖f k x‖}.indicator (fun a ↦ ‖f k a‖) x) = F ∘ f k
⊢ eLpNorm F p (Measure.map (f i) μ) = eLpNorm (F ∘ f j) p μ

Tactic:
(hf i).map_eq,

Goal state after:
case pos
α : Type u_1
inst✝⁴ : MeasurableSpace α
E : Type u_5
inst✝³ : MeasurableSpace E
inst✝² : NormedAddCommGroup E
inst✝¹ : BorelSpace E
μ : Measure α
inst✝ : IsFiniteMeasure μ
ι : Type u_6
f : ι → α → E
j : ι
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
hℒp : MemLp (f j) p μ
hfmeas : ∀ (i : ι), StronglyMeasurable (f i)
hf : ∀ (i : ι), IdentDistrib (f i) (f j) μ μ
ε : ℝ
hε : 0 < ε
hι : Nonempty ι
C : ℝ
hC₁ : 0 < C
hC₂ : eLpNorm ({x | C ≤ ↑‖f j x‖₊}.indicator (f j)) p μ ≤ ENNReal.ofReal ε
i : ι
this✝ : {x | ⟨C, ⋯⟩ ≤ ‖f i x‖₊} = {x | C ≤ ‖f i x‖}
F : E → ℝ := fun x ↦ if ⟨C, ⋯⟩ ≤ ‖x‖₊ then ‖x‖ else 0
F_meas : Measurable F
this : ∀ (k : ι), (fun x ↦ {x | C ≤ ‖f k x‖}.indicator (fun a ↦ ‖f k a‖) x) = F ∘ f k
⊢ eLpNorm F p (Measure.map (f j) μ) = eLpNorm (F ∘ f j) p μ
Module: Mathlib.Probability.Independence.Integration

Goal state before:
pp: Ω : Type u_5
𝓧 : Type u_6
m mΩ : MeasurableSpace Ω
P : Measure Ω
m𝓧 : MeasurableSpace 𝓧
X : Ω → 𝓧
A : Set Ω
E : Type u_7
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
hm : m ≤ mΩ
f : 𝓧 → E
hA1 : Indep m (MeasurableSpace.comap X m𝓧) P
hX : AEMeasurable X P
hA2 : MeasurableSet A
hf : AEStronglyMeasurable f (Measure.map X P)
⊢ ∫ (ω : Ω), id (A.indicator 1 ω) • f (X ω) ∂P = P.real A • ∫ (ω : Ω), f (X ω) ∂P

Tactic:
by
    rw [IndepFun.integral_fun_comp_smul_comp _ _ hX (by fun_prop) hf]
    · simp [hm A hA2]
    · exact hA1.indicator_indepFun 1 hA2
    · exact (aemeasurable_indicator_const_iff 1).2 (hm A hA2).nullMeasurableSet

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

Goal state before:
pp: ι : Type u_1
E : Type u_2
Ω' : Type u_3
Ω'' : Type u_4
m' : MeasurableSpace Ω'
μ' : Measure Ω'
inst✝⁵ : IsProbabilityMeasure μ'
m'' : MeasurableSpace Ω''
μ'' : Measure Ω''
inst✝⁴ : IsProbabilityMeasure μ''
mE : MeasurableSpace E
l : Filter ι
inst✝³ : SeminormedAddCommGroup E
inst✝² : SecondCountableTopology E
inst✝¹ : BorelSpace E
X : ι → Ω'' → E
inst✝ : l.IsCountablyGenerated
Y : ι → Ω'' → E
Z : Ω' → E
hXZ : TendstoInDistribution X l Z (fun x ↦ μ'') μ'
hXY : TendstoInMeasure μ'' (Y - X) l 0
hY : ∀ (i : ι), AEMeasurable (Y i) μ''
hZ : AEMeasurable Z μ'
hX : ∀ (i : ι), AEMeasurable (X i) μ''
hE : Nonempty E
x₀ : E := hE.some
F : E → ℝ
M : ℝ
hF_bounded : ∀ (x y : E), dist (F x) (F y) ≤ M
L : NNReal
hF_lip : LipschitzWith L F
hF_cont : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] F
hL : 0 < L
ε : ℝ
hε : ε > 0
n : ι
h_int_Y : Integrable (fun x ↦ F (Y n x)) μ''
h_int_X : Integrable (fun x ↦ F (X n x)) μ''
h_int_sub : Integrable (fun a ↦ ‖F (Y n a) - F (X n a)‖) μ''
⊢ ↑L * (ε / 2) * μ''.real {x | ‖Y n x - X n x‖ < ε / 2} + M * μ''.real {ω | ε / 2 ≤ ‖Y n ω - X n ω‖} ≤
    ↑L * (ε / 2) + M * μ''.real {ω | ε / 2 ≤ ‖Y n ω - X n ω‖}

Tactic:
rw [mul_assoc]
      gcongr
      grw [measureReal_le_one, mul_one]

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

Goal state before:
pp: α : Type u_1
Ω : Type u_2
ι : Type u_3
β : Type u_4
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
mβ : MeasurableSpace β
X : ι → Ω → α
Y : ι → Ω → β
f : ι → Set Ω
t : ι → Set β
s : Finset ι
inst✝ : Finite ι
hY : ∀ (i : ι), Measurable (Y i)
hindep : iIndepFun (fun i ω ↦ (X i ω, Y i ω)) κ μ
hf : ∀ i ∈ s, MeasurableSet (f i)
hy✝ : ∀ᵐ (a : α) ∂μ, ∀ i ∉ s, (κ a) (Y i ⁻¹' t i) ≠ 0
ht : ∀ (i : ι), MeasurableSet (t i)
val✝ : Fintype ι
g : ι → Set Ω := fun i' ↦ if i' ∈ s then Y i' ⁻¹' t i' ∩ f i' else Y i' ⁻¹' t i'
hYt✝ : ∀ (i : ι), MeasurableSet (Y i ⁻¹' t i)
hg✝ : ∀ (i : ι), MeasurableSet (g i)
a : α
hy : ∀ i ∉ s, (κ a) (Y i ⁻¹' t i) ≠ 0
a✝ : IsProbabilityMeasure (κ a)
hYt : (κ a) (⋂ i, Y i ⁻¹' t i) = ∏ i, (κ a) (Y i ⁻¹' t i)
hg : (κ a) (⋂ i, g i) = ∏ i, (κ a) (g i)
⊢ ((⋂ i, Y i ⁻¹' t i) ∩ ⋂ i, if i ∈ s then f i else univ) = ⋂ i, Y i ⁻¹' t i ∩ if i ∈ s then f i else univ

Tactic:
by rw [Set.iInter_inter_distrib]

Goal state after:
Module: Mathlib.MeasureTheory.Group.GeometryOfNumbers

Goal state before:
pp: E : Type u_1
inst✝⁶ : MeasurableSpace E
μ : Measure E
F s : Set E
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : BorelSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : μ.IsAddHaarMeasure
L : AddSubgroup E
inst✝ : Countable ↥L
fund : IsAddFundamentalDomain (↥L) F μ
h_symm : ∀ x ∈ s, -x ∈ s
h_conv : Convex ℝ s
h✝ : μ F * 2 ^ finrank ℝ E < μ s
h_vol : μ F < μ (2⁻¹ • s)
x y : ↥L
hxy : x ≠ y
h : ¬Disjoint (x +ᵥ 2⁻¹ • s) (y +ᵥ 2⁻¹ • s)
v : E
hv : 2 • v ∈ s
w : E
hw : 2 • w ∈ s
hvw : w - v = ↑(x - y)
⊢ 2⁻¹ • (2 • w - 2 • v) ∈ s

Tactic:
sub_eq_add_neg,

Goal state after:
E : Type u_1
inst✝⁶ : MeasurableSpace E
μ : Measure E
F s : Set E
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : BorelSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : μ.IsAddHaarMeasure
L : AddSubgroup E
inst✝ : Countable ↥L
fund : IsAddFundamentalDomain (↥L) F μ
h_symm : ∀ x ∈ s, -x ∈ s
h_conv : Convex ℝ s
h✝ : μ F * 2 ^ finrank ℝ E < μ s
h_vol : μ F < μ (2⁻¹ • s)
x y : ↥L
hxy : x ≠ y
h : ¬Disjoint (x +ᵥ 2⁻¹ • s) (y +ᵥ 2⁻¹ • s)
v : E
hv : 2 • v ∈ s
w : E
hw : 2 • w ∈ s
hvw : w - v = ↑(x - y)
⊢ 2⁻¹ • (2 • w + -(2 • v)) ∈ s
Module: Mathlib.Topology.ContinuousMap.CompactlySupported

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : TopologicalSpace α
Λ : (α →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
f g : α →C_c ℝ
h : α →C_c ℝ≥0
hh : (f + g).nnrealPart + h = f.nnrealPart + g.nnrealPart ∧ (-f + -g).nnrealPart + h = (-f).nnrealPart + (-g).nnrealPart
⊢ ↑(Λ (f + g).nnrealPart) - ↑(Λ (-g + -f).nnrealPart) =
    ↑(Λ f.nnrealPart) - ↑(Λ (-f).nnrealPart) + (↑(Λ g.nnrealPart) - ↑(Λ (-g).nnrealPart))

Tactic:
rw [← add_zero ((Λ (f + g).nnrealPart).toReal - (Λ (-g + -f).nnrealPart).toReal),
          ← sub_self (Λ h).toReal, sub_add_sub_comm, ← NNReal.coe_add, ← NNReal.coe_add,
          ← map_add, ← map_add, hh.1, add_comm (-g) (-f), hh.2]

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : TopologicalSpace α
Λ : (α →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
f g : α →C_c ℝ
h : α →C_c ℝ≥0
hh : (f + g).nnrealPart + h = f.nnrealPart + g.nnrealPart ∧ (-f + -g).nnrealPart + h = (-f).nnrealPart + (-g).nnrealPart
⊢ ↑(Λ (f.nnrealPart + g.nnrealPart)) - ↑(Λ ((-f).nnrealPart + (-g).nnrealPart)) =
    ↑(Λ f.nnrealPart) - ↑(Λ (-f).nnrealPart) + (↑(Λ g.nnrealPart) - ↑(Λ (-g).nnrealPart))
Module: Mathlib.MeasureTheory.Integral.Indicator

Goal state before:
pp: case refine_4
α : Type u_1
inst✝¹ : MeasurableSpace α
A : Set α
ι : Type u_2
L : Filter ι
inst✝ : L.IsCountablyGenerated
As : ι → Set α
μ : Measure α
A_mble : MeasurableSet A
As_mble : ∀ (i : ι), MeasurableSet (As i)
B : Set α
B_mble : MeasurableSet B
B_finmeas : μ B ≠ ∞
As_le_B : ∀ᶠ (i : ι) in L, As i ⊆ B
h_lim : ∀ᵐ (x : α) ∂μ, ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A
⊢ ∀ᵐ (a : α) ∂μ, Tendsto (fun n ↦ (As n).indicator 1 a) L (𝓝 (A.indicator 1 a))

Tactic:
· simpa only [Pi.one_def, tendsto_indicator_const_apply_iff_eventually] using h_lim

Goal state after:
Module: Mathlib.MeasureTheory.Integral.CurveIntegral.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
a b : E
ω₁ ω₂ : E → E →L[𝕜] F
γ : Path a b
h₁ : CurveIntegrable ω₁ γ
h₂ : CurveIntegrable ω₂ γ
⊢ curveIntegral (ω₁ - ω₂) γ = ∫ᶜ (x : E) in γ, ω₁ x - ∫ᶜ (x : E) in γ, ω₂ x

Tactic:
sub_eq_add_neg,

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
a b : E
ω₁ ω₂ : E → E →L[𝕜] F
γ : Path a b
h₁ : CurveIntegrable ω₁ γ
h₂ : CurveIntegrable ω₂ γ
⊢ curveIntegral (ω₁ + -ω₂) γ = ∫ᶜ (x : E) in γ, ω₁ x - ∫ᶜ (x : E) in γ, ω₂ x
Module: Mathlib.MeasureTheory.Integral.CurveIntegral.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
a b : E
ω₁ ω₂ : E → E →L[𝕜] F
γ : Path a b
h₁ : CurveIntegrable ω₁ γ
h₂ : CurveIntegrable ω₂ γ
⊢ curveIntegral (ω₁ + -ω₂) γ = ∫ᶜ (x : E) in γ, ω₁ x - ∫ᶜ (x : E) in γ, ω₂ x

Tactic:
sub_eq_add_neg,

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
a b : E
ω₁ ω₂ : E → E →L[𝕜] F
γ : Path a b
h₁ : CurveIntegrable ω₁ γ
h₂ : CurveIntegrable ω₂ γ
⊢ curveIntegral (ω₁ + -ω₂) γ = ∫ᶜ (x : E) in γ, ω₁ x + -∫ᶜ (x : E) in γ, ω₂ x
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral

Goal state before:
pp: E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
a : E
r : ℝ
hr : 0 ≤ r
hdf : ∀ᶠ (x : E) in 𝓝 a, DifferentiableAt ℝ f x
hderiv : fderiv ℝ f =O[𝓝 a] fun x ↦ ‖x - a‖ ^ r
C : ℝ
hC₀ : C > 0
hC : ∀ᶠ (x : E) in 𝓝 a, ‖fderiv ℝ f x‖ ≤ C * ‖‖x - a‖ ^ r‖
ε : ℝ
hε₀ : ε > 0
hε : ∀ y ∈ ball a ε, DifferentiableAt ℝ f y ∧ ‖fderiv ℝ f y‖ ≤ C * ‖‖y - a‖ ^ r‖
⊢ ∀ᶠ (x : E) in 𝓝 a, ‖f x - f a‖ ≤ C * ‖‖x - a‖ ^ (r + 1)‖

Tactic:
rw [eventually_nhds_iff_ball]

Goal state after:
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
a : E
r : ℝ
hr : 0 ≤ r
hdf : ∀ᶠ (x : E) in 𝓝 a, DifferentiableAt ℝ f x
hderiv : fderiv ℝ f =O[𝓝 a] fun x ↦ ‖x - a‖ ^ r
C : ℝ
hC₀ : C > 0
hC : ∀ᶠ (x : E) in 𝓝 a, ‖fderiv ℝ f x‖ ≤ C * ‖‖x - a‖ ^ r‖
ε : ℝ
hε₀ : ε > 0
hε : ∀ y ∈ ball a ε, DifferentiableAt ℝ f y ∧ ‖fderiv ℝ f y‖ ≤ C * ‖‖y - a‖ ^ r‖
⊢ ∃ ε > 0, ∀ y ∈ ball a ε, ‖f y - f a‖ ≤ C * ‖‖y - a‖ ^ (r + 1)‖
Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
s₀ s₁ t : Set X
s₀_compact : IsCompact s₀
s₁_compact : IsCompact s₁
t_compact : IsCompact t
disj : Disjoint s₀ s₁
hst : s₀ ∪ s₁ ⊆ t
so : Fin 2 → Set X := fun j ↦ if j = 0 then s₀ᶜ else s₁ᶜ
hso : so = fun j ↦ if j = 0 then s₀ᶜ else s₁ᶜ
⊢ ∃ f₀ f₁, EqOn (⇑f₀) 1 s₀ ∧ EqOn (⇑f₁) 1 s₁ ∧ EqOn (⇑(f₀ + f₁)) 1 t

Tactic:
have soopen (j : Fin 2) : IsOpen (so j) := by
    fin_cases j
    · simp only [hso, Fin.zero_eta, Fin.isValue, ↓reduceIte, isOpen_compl_iff]
      exact IsCompact.isClosed <| s₀_compact
    · simp only [hso, Fin.isValue, Fin.mk_one, one_ne_zero, ↓reduceIte, isOpen_compl_iff]
      exact IsCompact.isClosed <| s₁_compact

Goal state after:
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
s₀ s₁ t : Set X
s₀_compact : IsCompact s₀
s₁_compact : IsCompact s₁
t_compact : IsCompact t
disj : Disjoint s₀ s₁
hst : s₀ ∪ s₁ ⊆ t
so : Fin 2 → Set X := fun j ↦ if j = 0 then s₀ᶜ else s₁ᶜ
hso : so = fun j ↦ if j = 0 then s₀ᶜ else s₁ᶜ
soopen : ∀ (j : Fin 2), IsOpen (so j)
⊢ ∃ f₀ f₁, EqOn (⇑f₀) 1 s₀ ∧ EqOn (⇑f₁) 1 s₁ ∧ EqOn (⇑(f₀ + f₁)) 1 t