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

Goal state before:
pp: Ω : Type u_1
G : Type u_2
mΩ : MeasurableSpace Ω
ℙ : Measure Ω
inst✝⁷ : Group G
mG : MeasurableSpace G
inst✝⁶ : MeasurableMul₂ G
inst✝⁵ : MeasurableInv G
μ : Measure G
inst✝⁴ : μ.IsMulLeftInvariant
X Y : Ω → G
inst✝³ : SFinite μ
inst✝² : HasPDF X ℙ μ
inst✝¹ : HasPDF Y ℙ μ
inst✝ : IsFiniteMeasure ℙ
hXY : X ⟂ᵢ[ℙ] Y
⊢ (map (X * Y) ℙ).rnDeriv μ =ᵐ[μ] pdf X ℙ μ ⋆ₘₗ[μ] pdf Y ℙ μ

Tactic:
hXY.map_mul_eq_map_mconv_map₀ (HasPDF.aemeasurable' μ) (HasPDF.aemeasurable' μ)

Goal state after:
Ω : Type u_1
G : Type u_2
mΩ : MeasurableSpace Ω
ℙ : Measure Ω
inst✝⁷ : Group G
mG : MeasurableSpace G
inst✝⁶ : MeasurableMul₂ G
inst✝⁵ : MeasurableInv G
μ : Measure G
inst✝⁴ : μ.IsMulLeftInvariant
X Y : Ω → G
inst✝³ : SFinite μ
inst✝² : HasPDF X ℙ μ
inst✝¹ : HasPDF Y ℙ μ
inst✝ : IsFiniteMeasure ℙ
hXY : X ⟂ᵢ[ℙ] Y
⊢ (map X ℙ ∗ₘ map Y ℙ).rnDeriv μ =ᵐ[μ] pdf X ℙ μ ⋆ₘₗ[μ] pdf Y ℙ μ
Module: Mathlib.Probability.Independence.Integration

Goal state before:
pp: 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' : Ω → ℝ≥0∞
⊢ ∀ ⦃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) ω ∂μ

Tactic:
g

Goal state after:
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) ω ∂μ
Module: Mathlib.Probability.Independence.Integration

Goal state before:
pp: 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∞
a✝¹ : Disjoint (Function.support f') (Function.support g)
h_meas_f' : Measurable f'
a✝ : Measurable g
h_ind_f' :
  ∫⁻ (ω : Ω), f' ω * T.indicator (fun x ↦ c) ω ∂μ = (∫⁻ (ω : Ω), f' ω ∂μ) * ∫⁻ (ω : Ω), T.indicator (fun x ↦ c) ω ∂μ
h_ind_g :
  ∫⁻ (ω : Ω), g ω * T.indicator (fun x ↦ c) ω ∂μ = (∫⁻ (ω : Ω), g ω ∂μ) * ∫⁻ (ω : Ω), T.indicator (fun x ↦ c) ω ∂μ
h_measM_f' : Measurable f'
⊢ ∫⁻ (ω : Ω), (f' + g) ω * T.indicator (fun x ↦ c) ω ∂μ =
    (∫⁻ (ω : Ω), (f' + g) ω ∂μ) * ∫⁻ (ω : Ω), T.indicator (fun x ↦ c) ω ∂μ

Tactic:
Pi.add_apply,

Goal state after:
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∞
a✝¹ : Disjoint (Function.support f') (Function.support g)
h_meas_f' : Measurable f'
a✝ : Measurable g
h_ind_f' :
  ∫⁻ (ω : Ω), f' ω * T.indicator (fun x ↦ c) ω ∂μ = (∫⁻ (ω : Ω), f' ω ∂μ) * ∫⁻ (ω : Ω), T.indicator (fun x ↦ c) ω ∂μ
h_ind_g :
  ∫⁻ (ω : Ω), g ω * T.indicator (fun x ↦ c) ω ∂μ = (∫⁻ (ω : Ω), g ω ∂μ) * ∫⁻ (ω : Ω), T.indicator (fun x ↦ c) ω ∂μ
h_measM_f' : Measurable f'
⊢ ∫⁻ (ω : Ω), (f' ω + g ω) * T.indicator (fun x ↦ c) ω ∂μ =
    (∫⁻ (ω : Ω), f' ω + g ω ∂μ) * ∫⁻ (ω : Ω), T.indicator (fun x ↦ c) ω ∂μ
Module: Mathlib.Probability.Independence.Kernel.Indep

Goal state before:
pp: case refine_1.hC
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m₁ m₂ x✝ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
h_indep : Indep m₁ m₂ κ μ
s t✝ : Set Ω
hs : MeasurableSet s
ht✝¹ : MeasurableSet t✝
s' t' : Set Ω
ht' : t' ∈ {s | MeasurableSet s}
t : Set Ω
ht : t ∈ {s}
ht✝ : MeasurableSet t
⊢ t ∈ {s | MeasurableSet s}

Tactic:
| hC t ht =>

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

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hX : MemLp X 2 μ
this : eLpNorm (X - fun x ↦ ∫ (x : Ω), X x ∂μ) 2 μ ^ 2 < ∞
⊢ eVar[X; μ] < ∞

Tactic:
rw [eLpNorm_eq_lintegral_rpow_enorm_toReal two_ne_zero ENNReal.ofNat_ne_top, ← ENNReal.rpow_two]
    at this

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hX : MemLp X 2 μ
this : ((∫⁻ (x : Ω), ‖(X - fun x ↦ ∫ (x : Ω), X x ∂μ) x‖ₑ ^ ENNReal.toReal 2 ∂μ) ^ (1 / ENNReal.toReal 2)) ^ 2 < ∞
⊢ eVar[X; μ] < ∞
Module: Mathlib.Probability.Moments.Variance

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hXm : AEStronglyMeasurable X μ
hX : ¬MemLp X 2 μ
h : eVar[X; μ] < ∞
this : MemLp (fun ω ↦ X ω - ∫ (x : Ω), X x ∂μ) 2 μ
ω : Ω
⊢ X ω = ((fun ω ↦ X ω - ∫ (x : Ω), X x ∂μ) + fun x ↦ ∫ (x : Ω), X x ∂μ) ω

Tactic:
Pi.add_apply,

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hXm : AEStronglyMeasurable X μ
hX : ¬MemLp X 2 μ
h : eVar[X; μ] < ∞
this : MemLp (fun ω ↦ X ω - ∫ (x : Ω), X x ∂μ) 2 μ
ω : Ω
⊢ X ω = X ω - ∫ (x : Ω), X x ∂μ + ∫ (x : Ω), X x ∂μ
Module: Mathlib.Probability.Independence.Integration

Goal state before:
pp: case add
Ω : Type u_1
f : Ω → ℝ≥0∞
Mf Mg mΩ : MeasurableSpace Ω
μ : Measure Ω
hMf : Mf ≤ mΩ
hMg : Mg ≤ mΩ
h_ind : Indep Mf Mg μ
h_meas_f : Measurable f
h_measM_f : Measurable f
f' : Ω → ℝ≥0∞
⊢ ∀ ⦃g : Ω → ℝ≥0∞⦄,
    Disjoint (Function.support f') (Function.support g) →
      Measurable f' →
        Measurable g →
          ∫⁻ (ω : Ω), f ω * f' ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), f' ω ∂μ →
            ∫⁻ (ω : Ω), f ω * g ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), g ω ∂μ →
              ∫⁻ (ω : Ω), f ω * (f' + g) ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), (f' + g) ω ∂μ

Tactic:
g

Goal state after:
case add
Ω : Type u_1
f : Ω → ℝ≥0∞
Mf Mg mΩ : MeasurableSpace Ω
μ : Measure Ω
hMf : Mf ≤ mΩ
hMg : Mg ≤ mΩ
h_ind : Indep Mf Mg μ
h_meas_f : Measurable f
h_measM_f : Measurable f
f' g : Ω → ℝ≥0∞
⊢ Disjoint (Function.support f') (Function.support g) →
    Measurable f' →
      Measurable g →
        ∫⁻ (ω : Ω), f ω * f' ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), f' ω ∂μ →
          ∫⁻ (ω : Ω), f ω * g ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), g ω ∂μ →
            ∫⁻ (ω : Ω), f ω * (f' + g) ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), (f' + g) ω ∂μ
Module: Mathlib.Probability.Independence.Integration

Goal state before:
pp: case add
Ω : Type u_1
f : Ω → ℝ≥0∞
Mf Mg mΩ : MeasurableSpace Ω
μ : Measure Ω
hMf : Mf ≤ mΩ
hMg : Mg ≤ mΩ
h_ind : Indep Mf Mg μ
h_meas_f : Measurable f
h_measM_f : Measurable f
f' g : Ω → ℝ≥0∞
a✝¹ : Disjoint (Function.support f') (Function.support g)
h_measMg_f' : Measurable f'
a✝ : Measurable g
h_ind_f' : ∫⁻ (ω : Ω), f ω * f' ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), f' ω ∂μ
h_ind_g' : ∫⁻ (ω : Ω), f ω * g ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), g ω ∂μ
h_measM_f' : Measurable f'
⊢ ∫⁻ (ω : Ω), f ω * (f' + g) ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), (f' + g) ω ∂μ

Tactic:
Pi.add_apply,

Goal state after:
case add
Ω : Type u_1
f : Ω → ℝ≥0∞
Mf Mg mΩ : MeasurableSpace Ω
μ : Measure Ω
hMf : Mf ≤ mΩ
hMg : Mg ≤ mΩ
h_ind : Indep Mf Mg μ
h_meas_f : Measurable f
h_measM_f : Measurable f
f' g : Ω → ℝ≥0∞
a✝¹ : Disjoint (Function.support f') (Function.support g)
h_measMg_f' : Measurable f'
a✝ : Measurable g
h_ind_f' : ∫⁻ (ω : Ω), f ω * f' ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), f' ω ∂μ
h_ind_g' : ∫⁻ (ω : Ω), f ω * g ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), g ω ∂μ
h_measM_f' : Measurable f'
⊢ ∫⁻ (ω : Ω), f ω * (f' ω + g ω) ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), f' ω + g ω ∂μ
Module: Mathlib.Probability.Moments.Covariance

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

Tactic:
by
  simp [sub_eq_add_neg, hX]

Goal state after:
Module: Mathlib.Probability.IdentDistrib

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁶ : MeasurableSpace α
inst✝⁵ : MeasurableSpace β
inst✝⁴ : MeasurableSpace γ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
inst✝³ : ConditionallyCompleteLinearOrder γ
inst✝² : TopologicalSpace γ
inst✝¹ : OpensMeasurableSpace γ
inst✝ : OrderClosedTopology γ
h : IdentDistrib f g μ ν
⊢ essSup f μ = essSup g ν

Tactic:
have I : ∀ a, μ {x : α | a < f x} = ν {x : β | a < g x} := fun a =>
    h.measure_mem_eq measurableSet_Ioi

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁶ : MeasurableSpace α
inst✝⁵ : MeasurableSpace β
inst✝⁴ : MeasurableSpace γ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
inst✝³ : ConditionallyCompleteLinearOrder γ
inst✝² : TopologicalSpace γ
inst✝¹ : OpensMeasurableSpace γ
inst✝ : OrderClosedTopology γ
h : IdentDistrib f g μ ν
I : ∀ (a : γ), μ {x | a < f x} = ν {x | a < g x}
⊢ essSup f μ = essSup g ν
Module: Mathlib.Probability.IdentDistrib

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
ν : Measure β
f : α → ℝ≥0∞
g : β → ℝ≥0∞
h : IdentDistrib f g μ ν
⊢ ∫⁻ (a : ℝ≥0∞), id a ∂Measure.map f μ = ∫⁻ (x : β), id (g x) ∂ν

Tactic:
←
    lintegral_map' aemeasurable_id h.aemeasurable_snd,

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
ν : Measure β
f : α → ℝ≥0∞
g : β → ℝ≥0∞
h : IdentDistrib f g μ ν
⊢ ∫⁻ (a : ℝ≥0∞), id a ∂Measure.map f μ = ∫⁻ (a : ℝ≥0∞), id a ∂Measure.map g ν
Module: Mathlib.Probability.Process.Filtration

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
β : ι → Type u_3
inst✝³ : (i : ι) → TopologicalSpace (β i)
inst✝² : ∀ (i : ι), MetrizableSpace (β i)
mβ : (i : ι) → MeasurableSpace (β i)
inst✝¹ : ∀ (i : ι), BorelSpace (β i)
inst✝ : Preorder ι
u : (i : ι) → Ω → β i
hum : ∀ (i : ι), StronglyMeasurable (u i)
i : ι
⊢ ∀ i_1 ≤ i, MeasurableSpace.comap (u i_1) (mβ i_1) ≤ m

Tactic:
rintro j _ s ⟨t, ht, rfl⟩

Goal state after:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
β : ι → Type u_3
inst✝³ : (i : ι) → TopologicalSpace (β i)
inst✝² : ∀ (i : ι), MetrizableSpace (β i)
mβ : (i : ι) → MeasurableSpace (β i)
inst✝¹ : ∀ (i : ι), BorelSpace (β i)
inst✝ : Preorder ι
u : (i : ι) → Ω → β i
hum : ∀ (i : ι), StronglyMeasurable (u i)
i j : ι
j✝ : j ≤ i
t : Set (β j)
ht : MeasurableSet t
⊢ MeasurableSet (u j ⁻¹' t)
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
E' : Type u_6
mE' : MeasurableSpace E'
inst✝³ : SeminormedAddCommGroup E'
inst✝² : SecondCountableTopology E'
inst✝¹ : BorelSpace E'
inst✝ : l.IsCountablyGenerated
X : ι → Ω'' → E
Y : ι → Ω'' → E'
Z : Ω' → E
c : E'
hXZ : TendstoInDistribution X l Z (fun x ↦ μ'') μ'
hY : TendstoInMeasure μ'' Y l fun x ↦ c
hY_meas : ∀ (i : ι), AEMeasurable (Y i) μ''
⊢ TendstoInDistribution (fun n ω ↦ (X n ω, Y n ω)) l (fun ω ↦ (Z ω, c)) (fun x ↦ μ'') μ'

Tactic:
by
  have hX : ∀ i, AEMeasurable (X i) μ'' := hXZ.forall_aemeasurable
  refine tendstoInDistribution_of_tendstoInMeasure_sub (X := fun n ω ↦ (X n ω, c))
    (fun n ω ↦ (X n ω, Y n ω)) (fun ω ↦ (Z ω, c)) ?_ ?_ (fun i ↦ (hX i).prodMk (hY_meas i))
  · exact hXZ.continuous_comp (g := fun x ↦ (x, c)) (by fun_prop)
  · suffices TendstoInMeasure μ'' (fun n ω ↦ ((0 : E), Y n ω - c)) l 0 by
      convert! this with n ω
      simp
    simpa [tendstoInMeasure_iff_norm] using hY

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

Goal state before:

Tactic:
_ = (κ a (⋂ i, Y i ⁻¹' t i))⁻¹ * κ a ((⋂ i, Y i ⁻¹' t i) ∩ ⋂ i ∈ s, f i) := by
      rw [cond_apply]; exact .iInter fun i ↦ hY i (ht i)
    _ = (κ a (⋂ i, Y i ⁻¹' t i))⁻¹ * κ a (⋂ i, g i) := by
      congr 2
      calc
        _ = (⋂ i, Y i ⁻¹' t i) ∩ ⋂ i, if i ∈ s then f i else .univ := by
          congr 1
          simp only [Set.iInter_ite, Set.iInter_univ, Set.inter_univ]
        _ = ⋂ i, Y i ⁻¹' t i ∩ (if i ∈ s then f i else .univ) := by rw [Set.iInter_inter_distrib]
        _ = _ := Set.iInter_congr fun i ↦ by by_cases hi : i ∈ s <;> simp [hi, g]
    _ = (∏ i, κ a (Y i ⁻¹' t i))⁻¹ * κ a (⋂ i, g i) := by
      rw [hYt]
    _ = (∏ i, κ a (Y i ⁻¹' t i))⁻¹ * ∏ i, κ a (g i) := by
      rw [hg]
    _ = ∏ i, (κ a (Y i ⁻¹' t i))⁻¹ * κ a (g i) := by
      rw [Finset.prod_mul_distrib, ENNReal.prod_inv_distrib]
      exact fun _ _ i _ _ ↦ .inr <| measure_ne_top _ _
    _ = ∏ i, if i ∈ s then (κ a)[f i | Y i ⁻¹' t i] else 1 := by
      refine Finset.prod_congr rfl fun i _ ↦ ?_
      by_cases hi : i ∈ s
      · simp only [hi, ↓reduceIte, g, cond_apply (hY i (ht i))]
      · simp only [hi, ↓reduceIte, g, ENNReal.inv_mul_cancel (hy i hi) (measure_ne_top _ _)]
    _ = _ := by simp

Goal state after:
Module: Mathlib.Probability.Process.Filtration

Goal state before:
pp: case a
ι : Type u_2
inst✝² : Preorder ι
X : ι → Type u_4
inst✝¹ : (i : ι) → MeasurableSpace (X i)
inst✝ : LocallyFiniteOrderBot ι
i : ι
⊢ MeasurableSpace.comap (frestrictLe i)
      (MeasurableSpace.comap (⇑(MeasurableEquiv.piCongrLeft (fun i_1 ↦ X ↑i_1) (Equiv.IicFinsetSet i)))
        MeasurableSpace.pi) ≤
    MeasurableSpace.comap (frestrictLe i) MeasurableSpace.pi

Tactic:
exact MeasurableSpace.comap_mono <| Measurable.comap_le (by fun_prop)

Goal state after:
Module: Mathlib.Probability.Process.Filtration

Goal state before:
pp: case a
ι : Type u_2
inst✝² : Preorder ι
X : ι → Type u_4
inst✝¹ : (i : ι) → MeasurableSpace (X i)
inst✝ : LocallyFiniteOrderBot ι
i : ι
⊢ MeasurableSpace.comap (restrictLe i)
      (MeasurableSpace.comap (⇑(MeasurableEquiv.piCongrLeft (fun i_1 ↦ X ↑i_1) (Equiv.IicFinsetSet i).symm))
        MeasurableSpace.pi) ≤
    ↑piLE i

Tactic:
exact MeasurableSpace.comap_mono <| Measurable.comap_le (by fun_prop)

Goal state after:
Module: Mathlib.Probability.Process.Filtration

Goal state before:
pp: ι : Type u_2
inst✝² : Preorder ι
X : ι → Type u_4
inst✝¹ : (i : ι) → MeasurableSpace (X i)
inst✝ : LocallyFiniteOrderBot ι
i : ι
⊢ ↑piLE i = MeasurableSpace.comap (frestrictLe i) MeasurableSpace.pi

Tactic:
apply le_antisymm
  · simp_rw [piLE, ← piCongrLeft_comp_frestrictLe, ← MeasurableEquiv.coe_piCongrLeft, ← comap_comp]
    exact MeasurableSpace.comap_mono <| Measurable.comap_le (by fun_prop)
  · rw [← piCongrLeft_comp_restrictLe, ← MeasurableEquiv.coe_piCongrLeft, ← comap_comp]
    exact MeasurableSpace.comap_mono <| Measurable.comap_le (by fun_prop)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup β
μ : Measure α
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
f : ℕ → α → β
g : α → β
hf : ∀ (n : ℕ), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hg' : MemLp g p μ
hui : UnifIntegrable f p μ
hut : UnifTight f p μ
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (g x))
ε : ℝ≥0∞
hε : ε > 0
hfinε : ε ≠ ∞
hμ : μ ≠ 0
hε' : 0 < ε / 3
Eg : Set α
hmEg : MeasurableSet Eg
hμEg : μ Eg < ∞
hgε : eLpNorm (Egᶜ.indicator g) p μ < ε / 3
Ef : Set α
hmEf : MeasurableSet Ef
hμEf : μ Ef < ∞
hfε : ∀ (i : ℕ), eLpNorm (Efᶜ.indicator (f i)) p μ ≤ ε / 3
E : Set α := Ef ∪ Eg
hmE : MeasurableSet E
hfmE : μ E < ∞
hgE' : MemLp g p (μ.restrict E)
huiE : UnifIntegrable f p (μ.restrict E)
hfgE : ∀ᵐ (x : α) ∂μ.restrict E, Tendsto (fun n ↦ f n x) atTop (𝓝 (g x))
ffmE : Fact (μ E < ∞)
hInner : ∀ ε > 0, ∃ N, ∀ n ≥ N, eLpNorm (f n - g) p (μ.restrict E) ≤ ε
N : ℕ
hfngε : ∀ n ≥ N, eLpNorm (f n - g) p (μ.restrict E) ≤ ε / 3
n : ℕ
hn : n ≥ N
hmfngE : AEStronglyMeasurable (E.indicator (f n - g)) μ
hfngEε : eLpNorm (E.indicator (f n - g)) p μ ≤ ε / 3
hmgEc : AEStronglyMeasurable (Eᶜ.indicator g) μ
hgEcε : eLpNorm (Eᶜ.indicator g) p μ ≤ ε / 3
hmfnEc : AEStronglyMeasurable (Eᶜ.indicator (f n)) μ
⊢ eLpNorm (Eᶜ.indicator (f n)) p μ ≤ eLpNorm (Egᶜ.indicator (Efᶜ.indicator (f n))) p μ

Tactic:
by
        unfold E; rw [compl_union, inter_comm, ← indicator_indicator]

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

Goal state before:
pp: case hinf
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✝³ : Nontrivial E
inst✝² : μ.IsAddHaarMeasure
L : AddSubgroup E
inst✝¹ : Countable ↥L
inst✝ : DiscreteTopology ↥L
fund : IsAddFundamentalDomain (↥L) F μ
h_symm : ∀ x ∈ s, -x ∈ s
h_conv : Convex ℝ s
h_cpt : IsCompact s
h : μ F * 2 ^ finrank ℝ E ≤ μ s
h_mes : μ s ≠ 0
h_nemp : s.Nonempty
u : ℕ → ℝ≥0 := ⋯
K : ConvexBody E := ⋯
S : ℕ → ConvexBody E := ⋯
Z : ℕ → Set E := ⋯
h_zero : 0 ∈ K
h_clos : IsClosed (↑L \ {0})
n : ℕ
⊢ μ s ≠ ∞

pp: case bc
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✝³ : Nontrivial E
inst✝² : μ.IsAddHaarMeasure
L : AddSubgroup E
inst✝¹ : Countable ↥L
inst✝ : DiscreteTopology ↥L
fund : IsAddFundamentalDomain (↥L) F μ
h_symm : ∀ x ∈ s, -x ∈ s
h_conv : Convex ℝ s
h_cpt : IsCompact s
h : μ F * 2 ^ finrank ℝ E ≤ μ s
h_mes : μ s ≠ 0
h_nemp : s.Nonempty
u : ℕ → ℝ≥0 := ⋯
K : ConvexBody E := ⋯
S : ℕ → ConvexBody E := ⋯
Z : ℕ → Set E := ⋯
h_zero : 0 ∈ K
h_clos : IsClosed (↑L \ {0})
n : ℕ
⊢ 1 < ENNReal.ofReal ((1 + ↑(u n)) ^ finrank ℝ E)

Tactic:
· exact h_cpt.measure_ne_top

Goal state after:
case bc
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✝³ : Nontrivial E
inst✝² : μ.IsAddHaarMeasure
L : AddSubgroup E
inst✝¹ : Countable ↥L
inst✝ : DiscreteTopology ↥L
fund : IsAddFundamentalDomain (↥L) F μ
h_symm : ∀ x ∈ s, -x ∈ s
h_conv : Convex ℝ s
h_cpt : IsCompact s
h : μ F * 2 ^ finrank ℝ E ≤ μ s
h_mes : μ s ≠ 0
h_nemp : s.Nonempty
u : ℕ → ℝ≥0 := ⋯
K : ConvexBody E := ⋯
S : ℕ → ConvexBody E := ⋯
Z : ℕ → Set E := ⋯
h_zero : 0 ∈ K
h_clos : IsClosed (↑L \ {0})
n : ℕ
⊢ 1 < ENNReal.ofReal ((1 + ↑(u n)) ^ finrank ℝ E)
Module: Mathlib.MeasureTheory.Integral.Gamma

Goal state before:
pp: p q : ℝ
hp : 1 ≤ p
hq : -2 < q
⊢ ∫ (x : ℝ × ℝ) in Ioi 0 ×ˢ Ioo (-π) π, x.1 * (|x.1| ^ q * rexp (-|x.1| ^ p)) =
    ∫ (z : ℝ × ℝ) in Ioi 0 ×ˢ Ioo (-π) π, z.1 * |z.1| ^ q * rexp (-|z.1| ^ p) * 1 ∂volume.prod volume

Tactic:
volume_eq_prod

Goal state after:
p q : ℝ
hp : 1 ≤ p
hq : -2 < q
⊢ ∫ (x : ℝ × ℝ) in Ioi 0 ×ˢ Ioo (-π) π, x.1 * (|x.1| ^ q * rexp (-|x.1| ^ p)) ∂volume.prod volume =
    ∫ (z : ℝ × ℝ) in Ioi 0 ×ˢ Ioo (-π) π, z.1 * |z.1| ^ q * rexp (-|z.1| ^ p) * 1 ∂volume.prod volume
Module: Mathlib.MeasureTheory.Integral.Gamma

Goal state before:
pp: p q b : ℝ
hp : 1 ≤ p
hq : -2 < q
hb : 0 < b
⊢ ∫ (x : ℝ × ℝ) in Ioi 0 ×ˢ Ioo (-π) π, x.1 * (|x.1| ^ q * rexp (-b * |x.1| ^ p)) =
    ∫ (z : ℝ × ℝ) in Ioi 0 ×ˢ Ioo (-π) π, z.1 * |z.1| ^ q * rexp (-b * |z.1| ^ p) * 1 ∂volume.prod volume

Tactic:
volume_eq_prod

Goal state after:
p q b : ℝ
hp : 1 ≤ p
hq : -2 < q
hb : 0 < b
⊢ ∫ (x : ℝ × ℝ) in Ioi 0 ×ˢ Ioo (-π) π, x.1 * (|x.1| ^ q * rexp (-b * |x.1| ^ p)) ∂volume.prod volume =
    ∫ (z : ℝ × ℝ) in Ioi 0 ×ˢ Ioo (-π) π, z.1 * |z.1| ^ q * rexp (-b * |z.1| ^ p) * 1 ∂volume.prod volume
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 c : E
ω : E → E →L[𝕜] F
γab : Path a b
γbc : Path b c
h₁ : CurveIntegrable ω γab
h₂ : CurveIntegrable ω γbc
⊢ ∫ᶜ (x : E) in γab.trans γbc, ω x = ∫ᶜ (x : E) in γab, ω x + ∫ᶜ (x : E) in γbc, ω x

Tactic:
by
  let instF := NormedSpace.restrictScalars ℝ 𝕜 F
  rw [curveIntegral_def, ← intervalIntegral.integral_add_adjacent_intervals
    (h₁.intervalIntegrable_curveIntegralFun_trans_left γbc)
    (h₂.intervalIntegrable_curveIntegralFun_trans_right γab),
    intervalIntegral.integral_congr_ae_restrict (curveIntegralFun_trans_aeeq_left _ _ _),
    intervalIntegral.integral_congr_ae_restrict (curveIntegralFun_trans_aeeq_right _ _ _)]
  simp only [← ofNat_smul_eq_nsmul (R := ℝ)]
  rw [intervalIntegral.integral_smul, intervalIntegral.smul_integral_comp_mul_left,
    intervalIntegral.integral_smul,
    intervalIntegral.smul_integral_comp_mul_left (f := (curveIntegralFun ω γbc <| · - 1)),
    intervalIntegral.integral_comp_sub_right]
  simp only [curveIntegral_def]
  norm_num

Goal state after:
Module: Mathlib.MeasureTheory.Integral.MeanValue

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
s : Set α
f g : α → ℝ
μ : Measure α
hs_conn : IsConnected s
hs_meas : MeasurableSet s
hf : ContinuousOn f s
hg : IntegrableOn g s μ
hfg : IntegrableOn (fun x ↦ f x * g x) s μ
hg0 : ∀ᵐ (x : α) ∂μ.restrict s, 0 ≤ g x
ρ : α → ENNReal := fun x ↦ ENNReal.ofReal (g x)
ν : Measure α := μ.withDensity ρ
hρ_ae : AEMeasurable ρ (μ.restrict s)
hρ_top : ∀ᵐ (x : α) ∂μ.restrict s, ρ x < ⊤
h_toReal_ae : (fun x ↦ (ρ x).toReal) =ᵐ[μ.restrict s] g
heq : ∫ (x : α) in s, f x * g x ∂μ = ∫ (x : α) in s, f x ∂ν
hg1 : ∫ (x : α) in s, g x ∂μ = 0
hν0 : ∫ (x : α) in s, 1 ∂ν = 0
c : α
hc : c ∈ s
⊢ ∫ (x : α) in s, f x ∂ν = 0

Tactic:
setIntegral_eq_zero_iff_of_nonneg_ae hg0 hg

Goal state after:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
s : Set α
f g : α → ℝ
μ : Measure α
hs_conn : IsConnected s
hs_meas : MeasurableSet s
hf : ContinuousOn f s
hg : IntegrableOn g s μ
hfg : IntegrableOn (fun x ↦ f x * g x) s μ
hg0 : ∀ᵐ (x : α) ∂μ.restrict s, 0 ≤ g x
ρ : α → ENNReal := fun x ↦ ENNReal.ofReal (g x)
ν : Measure α := μ.withDensity ρ
hρ_ae : AEMeasurable ρ (μ.restrict s)
hρ_top : ∀ᵐ (x : α) ∂μ.restrict s, ρ x < ⊤
h_toReal_ae : (fun x ↦ (ρ x).toReal) =ᵐ[μ.restrict s] g
heq : ∫ (x : α) in s, f x * g x ∂μ = ∫ (x : α) in s, f x ∂ν
hg1 : g =ᵐ[μ.restrict s] 0
hν0 : ∫ (x : α) in s, 1 ∂ν = 0
c : α
hc : c ∈ s
⊢ ∫ (x : α) in s, f x ∂ν = 0
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.MeanValue

Goal state before:
pp: a b : ℝ
f g : ℝ → ℝ
μ : Measure ℝ
hf : ContinuousOn f [[a, b]]
hg : IntervalIntegrable g μ a b
hg0 : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), 0 ≤ g x
h : ¬a = b
this :
  ∀ {a b : ℝ},
    ContinuousOn f [[a, b]] →
      IntervalIntegrable g μ a b →
        (∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), 0 ≤ g x) →
          ¬a = b → a < b → ∃ c ∈ [[a, b]], ∫ (x : ℝ) in a..b, f x * g x ∂μ = f c * ∫ (x : ℝ) in a..b, g x ∂μ
hab : b ≤ a
⊢ ContinuousOn f [[b, a]]

Tactic:
rwa [uIcc_comm]

Goal state after:
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.MeanValue

Goal state before:
pp: a b : ℝ
f g : ℝ → ℝ
μ : Measure ℝ
hf : ContinuousOn f [[a, b]]
hg : IntervalIntegrable g μ a b
hg0 : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), 0 ≤ g x
h : ¬a = b
this :
  ∀ {a b : ℝ},
    ContinuousOn f [[a, b]] →
      IntervalIntegrable g μ a b →
        (∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), 0 ≤ g x) →
          ¬a = b → a < b → ∃ c ∈ [[a, b]], ∫ (x : ℝ) in a..b, f x * g x ∂μ = f c * ∫ (x : ℝ) in a..b, g x ∂μ
hab : b ≤ a
c : ℝ
c_in_uIcc : c ∈ [[b, a]]
that : ∫ (x : ℝ) in b..a, f x * g x ∂μ = f c * ∫ (x : ℝ) in b..a, g x ∂μ
⊢ c ∈ [[a, b]]

Tactic:
rwa [uIcc_comm]

Goal state after: