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

Goal state before:
pp: case iSup
Ω : 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_1 : ℕ → Ω → ℝ≥0∞⦄,
    (∀ (n : ℕ), Measurable (f_1 n)) →
      Monotone f_1 →
        (∀ (n : ℕ), ∫⁻ (ω : Ω), f ω * f_1 n ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), f_1 n ω ∂μ) →
          ∫⁻ (ω : Ω), f ω * (fun x ↦ ⨆ n, f_1 n x) ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), (fun x ↦ ⨆ n, f_1 n x) ω ∂μ

Tactic:
· intro f' h_meas_f' h_mono_f' h_ind_f'
    have h_measM_f' : ∀ n, Measurable (f' n) := fun n => (h_meas_f' n).mono hMg le_rfl
    simp_rw [mul_iSup]
    rw [lintegral_iSup, lintegral_iSup h_measM_f' h_mono_f', mul_iSup]
    · simp_rw [← h_ind_f']
    · exact fun n => h_measM_f.mul (h_measM_f' n)
    · exact fun n m (h_le : n ≤ m) a => mul_le_mul_right (h_mono_f' h_le a) _

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

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

Tactic:
rw [variance_const_add (by fun_prop) c, variance_fun_neg]

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

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_5
F : Type u_6
G : Type u_7
inst✝⁹ : TopologicalSpace E
inst✝⁸ : ContinuousENorm E
inst✝⁷ : MeasurableSpace E
inst✝⁶ : OpensMeasurableSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousENorm F
inst✝³ : MeasurableSpace F
inst✝² : OpensMeasurableSpace F
inst✝¹ : TopologicalSpace G
inst✝ : ContinuousENorm G
X : Ω → E
Y : Ω → F
hXY : X ⟂ᵢ[μ] Y
hX : Integrable X μ
hY : Integrable Y μ
B : E → F → G
cB : Continuous (Function.uncurry B)
C : ℝ≥0
hB : ∀ (x : E) (y : F), ‖B x y‖ₑ ≤ ↑C * ‖x‖ₑ * ‖y‖ₑ
⊢ HasFiniteIntegral (fun ω ↦ B (X ω) (Y ω)) μ

Tactic:
unfold HasFiniteIntegral

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_5
F : Type u_6
G : Type u_7
inst✝⁹ : TopologicalSpace E
inst✝⁸ : ContinuousENorm E
inst✝⁷ : MeasurableSpace E
inst✝⁶ : OpensMeasurableSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousENorm F
inst✝³ : MeasurableSpace F
inst✝² : OpensMeasurableSpace F
inst✝¹ : TopologicalSpace G
inst✝ : ContinuousENorm G
X : Ω → E
Y : Ω → F
hXY : X ⟂ᵢ[μ] Y
hX : Integrable X μ
hY : Integrable Y μ
B : E → F → G
cB : Continuous (Function.uncurry B)
C : ℝ≥0
hB : ∀ (x : E) (y : F), ‖B x y‖ₑ ≤ ↑C * ‖x‖ₑ * ‖y‖ₑ
⊢ ∫⁻ (a : Ω), ‖(fun ω ↦ B (X ω) (Y ω)) a‖ₑ ∂μ < ∞
Module: Mathlib.Probability.Independence.Integration

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_5
F : Type u_6
G : Type u_7
inst✝⁸ : TopologicalSpace E
inst✝⁷ : ContinuousENorm E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : OpensMeasurableSpace E
inst✝⁴ : NormedAddGroup F
inst✝³ : MeasurableSpace F
inst✝² : OpensMeasurableSpace F
inst✝¹ : TopologicalSpace G
inst✝ : ContinuousENorm G
X : Ω → E
Y : Ω → F
hXY : X ⟂ᵢ[μ] Y
B : E → F → G
c : ℝ≥0
hc : c ≠ 0
hB : ∀ (x : E) (y : F), ↑c * ‖x‖ₑ * ‖y‖ₑ ≤ ‖B x y‖ₑ
h'XY : Integrable (fun ω ↦ B (X ω) (Y ω)) μ
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
h'Y : ¬Y =ᵐ[μ] 0
I : ∫⁻ (ω : Ω), ‖Y ω‖ₑ ∂μ ≠ 0
H : ∫⁻ (a : Ω), ‖X a‖ₑ ∂μ = ∞
⊢ False

Tactic:
have J : (‖X ·‖ₑ) ⟂ᵢ[μ] (‖Y ·‖ₑ) := hXY.comp measurable_enorm measurable_enorm

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_5
F : Type u_6
G : Type u_7
inst✝⁸ : TopologicalSpace E
inst✝⁷ : ContinuousENorm E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : OpensMeasurableSpace E
inst✝⁴ : NormedAddGroup F
inst✝³ : MeasurableSpace F
inst✝² : OpensMeasurableSpace F
inst✝¹ : TopologicalSpace G
inst✝ : ContinuousENorm G
X : Ω → E
Y : Ω → F
hXY : X ⟂ᵢ[μ] Y
B : E → F → G
c : ℝ≥0
hc : c ≠ 0
hB : ∀ (x : E) (y : F), ↑c * ‖x‖ₑ * ‖y‖ₑ ≤ ‖B x y‖ₑ
h'XY : Integrable (fun ω ↦ B (X ω) (Y ω)) μ
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
h'Y : ¬Y =ᵐ[μ] 0
I : ∫⁻ (ω : Ω), ‖Y ω‖ₑ ∂μ ≠ 0
H : ∫⁻ (a : Ω), ‖X a‖ₑ ∂μ = ∞
J : (fun x ↦ ‖X x‖ₑ) ⟂ᵢ[μ] fun x ↦ ‖Y x‖ₑ
⊢ False
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✝¹ : NormedAddCommGroup γ
inst✝ : BorelSpace γ
p : ℝ≥0∞
h : IdentDistrib f g μ ν
hf : MemLp f p μ
⊢ MemLp g p ν

Tactic:
refine ⟨h.aestronglyMeasurable_snd hf.aestronglyMeasurable, ?_⟩

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
inst✝¹ : NormedAddCommGroup γ
inst✝ : BorelSpace γ
p : ℝ≥0∞
h : IdentDistrib f g μ ν
hf : MemLp f p μ
⊢ eLpNorm g p ν < ∞
Module: Mathlib.MeasureTheory.Function.ConvergenceInDistribution

Goal state before:
pp: ι : Type u_1
E : Type u_2
Ω' : Type u_3
m' : MeasurableSpace Ω'
μ' : Measure Ω'
inst✝³ : IsProbabilityMeasure μ'
mE : MeasurableSpace E
Z : Ω' → E
l : Filter ι
inst✝² : TopologicalSpace E
inst✝¹ : l.IsCountablyGenerated
inst✝ : OpensMeasurableSpace E
X : ι → Ω' → E
hX₁ : ∀ (i : ι), AEMeasurable (X i) μ'
hZ : AEMeasurable Z μ'
hX₂ : ∀ᵐ (ω : Ω') ∂μ', Tendsto (fun i ↦ X i ω) l (𝓝 (Z ω))
f : BoundedContinuousFunction E NNReal
i : ι
| ∫⁻ (ω : E), ↑(f ω) ∂Measure.map (X i) μ'

Tactic:
rw [lintegral_map' (by fun_prop) (hX₁ i)]

Goal state after:
ι : Type u_1
E : Type u_2
Ω' : Type u_3
m' : MeasurableSpace Ω'
μ' : Measure Ω'
inst✝³ : IsProbabilityMeasure μ'
mE : MeasurableSpace E
Z : Ω' → E
l : Filter ι
inst✝² : TopologicalSpace E
inst✝¹ : l.IsCountablyGenerated
inst✝ : OpensMeasurableSpace E
X : ι → Ω' → E
hX₁ : ∀ (i : ι), AEMeasurable (X i) μ'
hZ : AEMeasurable Z μ'
hX₂ : ∀ᵐ (ω : Ω') ∂μ', Tendsto (fun i ↦ X i ω) l (𝓝 (Z ω))
f : BoundedContinuousFunction E NNReal
i : ι
| ∫⁻ (a : Ω'), ↑(f (X i a)) ∂μ'
Module: Mathlib.MeasureTheory.Function.ConvergenceInDistribution

Goal state before:
pp: ι : Type u_1
E : Type u_2
Ω' : Type u_3
m' : MeasurableSpace Ω'
μ' : Measure Ω'
inst✝⁴ : IsProbabilityMeasure μ'
mE : MeasurableSpace E
Z : Ω' → E
l : Filter ι
inst✝³ : PseudoEMetricSpace E
inst✝² : BorelSpace E
inst✝¹ : l.IsCountablyGenerated
inst✝ : l.NeBot
X : ι → Ω' → E
h : TendstoInMeasure μ' X l Z
hX : ∀ (i : ι), AEMeasurable (X i) μ'
hZ : AEMeasurable Z μ'
ns : ℕ → ι
hns : Tendsto ns atTop l
⊢ ∃ ms, Tendsto (fun n ↦ ⟨Measure.map (X (ns (ms n))) μ', ⋯⟩) atTop (𝓝 ⟨Measure.map Z μ', ⋯⟩)

Tactic:
obtain ⟨ms, hms1, hms2⟩ := h.comp hns |>.exists_seq_tendsto_ae'

Goal state after:
ι : Type u_1
E : Type u_2
Ω' : Type u_3
m' : MeasurableSpace Ω'
μ' : Measure Ω'
inst✝⁴ : IsProbabilityMeasure μ'
mE : MeasurableSpace E
Z : Ω' → E
l : Filter ι
inst✝³ : PseudoEMetricSpace E
inst✝² : BorelSpace E
inst✝¹ : l.IsCountablyGenerated
inst✝ : l.NeBot
X : ι → Ω' → E
h : TendstoInMeasure μ' X l Z
hX : ∀ (i : ι), AEMeasurable (X i) μ'
hZ : AEMeasurable Z μ'
ns : ℕ → ι
hns : Tendsto ns atTop l
ms : ℕ → ℕ
hms1 : Tendsto ms atTop atTop
hms2 : ∀ᵐ (x : Ω') ∂μ', Tendsto (fun i ↦ (X ∘ ns) (ms i) x) atTop (𝓝 (Z x))
⊢ ∃ ms, Tendsto (fun n ↦ ⟨Measure.map (X (ns (ms n))) μ', ⋯⟩) atTop (𝓝 ⟨Measure.map Z μ', ⋯⟩)
Module: Mathlib.Probability.IdentDistrib

Goal state before:
pp: α : 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 μ
hf : ∀ (i : ι), IdentDistrib (f i) (f j) μ μ
hfmeas : ∀ (i : ι), AEStronglyMeasurable (f i) μ
⊢ UniformIntegrable f p μ

Tactic:
set g : ι → α → E := fun i => (hfmeas i).choose

Goal state after:
α : 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 μ
hf : ∀ (i : ι), IdentDistrib (f i) (f j) μ μ
hfmeas : ∀ (i : ι), AEStronglyMeasurable (f i) μ
g : ι → α → E := fun i ↦ Exists.choose ⋯
⊢ UniformIntegrable f p μ
Module: Mathlib.Probability.Process.Filtration

Goal state before:
pp: case neg
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝ : PartialOrder ι
𝓕 : Filtration ι m
this : TopologicalSpace ι := Preorder.topology ι
i j : ι
hij : i ≤ j
hi : (𝓝[>] i).NeBot
hj : ¬(𝓝[>] j).NeBot
⊢ ⨅ j, ⨅ (_ : i < j), ↑𝓕 j ≤ ↑𝓕 j

Tactic:
obtain rfl | hj := eq_or_ne j i
        · contradiction
        · exact iInf₂_le j (lt_of_le_of_ne hij hj.symm)

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)
⊢ (κ a)[⋂ i ∈ s, f i | ⋂ i, Y i ⁻¹' t i] = ∏ i ∈ s, (κ a)[f i | Y i ⁻¹' t i]

Tactic:
calc
    _ = (κ 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 (⇑(Equiv.piCongrLeft (fun i_1 ↦ X ↑i_1) (Equiv.IicFinsetSet i)) ∘ frestrictLe i)
      MeasurableSpace.pi ≤
    MeasurableSpace.comap (frestrictLe i) MeasurableSpace.pi

Tactic:
← MeasurableEquiv.coe_piCongrLeft,

Goal state after:
case a
ι : Type u_2
inst✝² : Preorder ι
X : ι → Type u_4
inst✝¹ : (i : ι) → MeasurableSpace (X i)
inst✝ : LocallyFiniteOrderBot ι
i : ι
⊢ MeasurableSpace.comap (⇑(MeasurableEquiv.piCongrLeft (fun i_1 ↦ X ↑i_1) (Equiv.IicFinsetSet i)) ∘ frestrictLe i)
      MeasurableSpace.pi ≤
    MeasurableSpace.comap (frestrictLe i) MeasurableSpace.pi
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 (⇑(Equiv.piCongrLeft (fun i_1 ↦ X ↑i_1) (Equiv.IicFinsetSet i).symm) ∘ restrictLe i)
      MeasurableSpace.pi ≤
    ↑piLE i

Tactic:
← MeasurableEquiv.coe_piCongrLeft,

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

Goal state before:
pp: case neg.refine_1
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : ι → α → β
p : ℝ≥0∞
hf : UnifTight f p μ
ε : ℝ≥0∞
hε : ε ≠ 0
hε_top : ¬ε = ∞
s : Set α
hμs : μ s ≠ ∞
hfs : ∀ (i : ι), eLpNorm (sᶜ.indicator (f i)) p μ ≤ ↑ε.toNNReal
⊢ ∀ ⦃s t : Set α⦄,
    s ⊆ t → (∀ (i : ι), eLpNorm (t.indicator (f i)) p μ ≤ ε) → ∀ (i : ι), eLpNorm (s.indicator (f i)) p μ ≤ ε

Tactic:
intro s t hst ht i
    exact (eLpNorm_mono <| norm_indicator_le_of_subset hst _).trans (ht i)

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

Goal state before:
pp: G : Type u_1
X : Type u_2
inst✝² : MeasurableSpace X
μ : Measure X
inst✝¹ : Group G
inst✝ : MulAction G X
ι : Type u_3
u : Ultrafilter ι
F : ι → Set X
hfoel : IsFoelner G μ (↑u) F
s : Set X
i : ι
hi : μ (F i) ≠ 0
⊢ μ (F i) ≠ ∞ → μ (s ∩ F i) / μ (F i) ∈ Icc 0 1

Tactic:
hi'

Goal state after:
G : Type u_1
X : Type u_2
inst✝² : MeasurableSpace X
μ : Measure X
inst✝¹ : Group G
inst✝ : MulAction G X
ι : Type u_3
u : Ultrafilter ι
F : ι → Set X
hfoel : IsFoelner G μ (↑u) F
s : Set X
i : ι
hi : μ (F i) ≠ 0
hi' : μ (F i) ≠ ∞
⊢ μ (s ∩ F i) / μ (F i) ∈ Icc 0 1
Module: Mathlib.MeasureTheory.Group.FoelnerFilter

Goal state before:
pp: G : Type u_1
X : Type u_2
inst✝² : MeasurableSpace X
μ : Measure X
inst✝¹ : Group G
inst✝ : MulAction G X
ι : Type u_3
u : Ultrafilter ι
F : ι → Set X
hfoel : IsFoelner G μ (↑u) F
i : ι
hi : μ (F i) ≠ 0
⊢ μ (F i) ≠ ∞ → μ (univ ∩ F i) / μ (F i) = 1

Tactic:
hi'

Goal state after:
G : Type u_1
X : Type u_2
inst✝² : MeasurableSpace X
μ : Measure X
inst✝¹ : Group G
inst✝ : MulAction G X
ι : Type u_3
u : Ultrafilter ι
F : ι → Set X
hfoel : IsFoelner G μ (↑u) F
i : ι
hi : μ (F i) ≠ 0
hi' : μ (F i) ≠ ∞
⊢ μ (univ ∩ F i) / μ (F i) = 1
Module: Mathlib.MeasureTheory.Group.FoelnerFilter

Goal state before:
pp: case h.refine_1
G : Type u_1
X : Type u_2
inst✝⁴ : MeasurableSpace X
μ : Measure X
inst✝³ : Group G
inst✝² : MulAction G X
ι : Type u_3
l : Filter ι
F : ι → Set X
inst✝¹ : SMulInvariantMeasure G X μ
inst✝ : l.NeBot
hfoel : IsFoelner G μ l F
⊢ mean μ (Ultrafilter.of l) F univ = 1

pp: case h.refine_2
G : Type u_1
X : Type u_2
inst✝⁴ : MeasurableSpace X
μ : Measure X
inst✝³ : Group G
inst✝² : MulAction G X
ι : Type u_3
l : Filter ι
F : ι → Set X
inst✝¹ : SMulInvariantMeasure G X μ
inst✝ : l.NeBot
hfoel : IsFoelner G μ l F
⊢ ∀ (s t : Set X),
    MeasurableSet t →
      Disjoint s t → mean μ (Ultrafilter.of l) F (s ∪ t) = mean μ (Ultrafilter.of l) F s + mean μ (Ultrafilter.of l) F t

pp: case h.refine_3
G : Type u_1
X : Type u_2
inst✝⁴ : MeasurableSpace X
μ : Measure X
inst✝³ : Group G
inst✝² : MulAction G X
ι : Type u_3
l : Filter ι
F : ι → Set X
inst✝¹ : SMulInvariantMeasure G X μ
inst✝ : l.NeBot
hfoel : IsFoelner G μ l F
⊢ ∀ (g : G) (s : Set X), mean μ (Ultrafilter.of l) F (g • s) = mean μ (Ultrafilter.of l) F s

Tactic:
· exact (hfoel.mono <| Ultrafilter.of_le l).mean_univ_eq_one

Goal state after:
case h.refine_2
G : Type u_1
X : Type u_2
inst✝⁴ : MeasurableSpace X
μ : Measure X
inst✝³ : Group G
inst✝² : MulAction G X
ι : Type u_3
l : Filter ι
F : ι → Set X
inst✝¹ : SMulInvariantMeasure G X μ
inst✝ : l.NeBot
hfoel : IsFoelner G μ l F
⊢ ∀ (s t : Set X),
    MeasurableSet t →
      Disjoint s t → mean μ (Ultrafilter.of l) F (s ∪ t) = mean μ (Ultrafilter.of l) F s + mean μ (Ultrafilter.of l) F t

case h.refine_3
G : Type u_1
X : Type u_2
inst✝⁴ : MeasurableSpace X
μ : Measure X
inst✝³ : Group G
inst✝² : MulAction G X
ι : Type u_3
l : Filter ι
F : ι → Set X
inst✝¹ : SMulInvariantMeasure G X μ
inst✝ : l.NeBot
hfoel : IsFoelner G μ l F
⊢ ∀ (g : G) (s : Set X), mean μ (Ultrafilter.of l) F (g • s) = mean μ (Ultrafilter.of l) F s
Module: Mathlib.MeasureTheory.Integral.Indicator

Goal state before:
pp: α : Type u_1
inst✝² : MeasurableSpace α
A : Set α
ι : Type u_2
L : Filter ι
inst✝¹ : L.IsCountablyGenerated
As : ι → Set α
μ : Measure α
inst✝ : IsFiniteMeasure μ
As_mble : ∀ (i : ι), MeasurableSet (As i)
h_lim : ∀ (x : α), ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A
⊢ Tendsto (fun i ↦ μ (As i)) L (𝓝 (μ A))

Tactic:
by
  rcases L.eq_or_neBot with rfl | _
  · exact tendsto_bot
  apply tendsto_measure_of_ae_tendsto_indicator_of_isFiniteMeasure L ?_ As_mble (ae_of_all μ h_lim)
  exact measurableSet_of_tendsto_indicator L As_mble h_lim

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

Goal state before:
pp: case e'_3
p : ℝ
hp : 1 ≤ p
⊢ π * Real.Gamma (2 / p + 1) = 2 * π / p * Real.Gamma (2 / p)

Tactic:
Real.Gamma_add_one (div_ne_zero two_ne_zero (by linarith))

Goal state after:
case e'_3
p : ℝ
hp : 1 ≤ p
⊢ π * (2 / p * Real.Gamma (2 / p)) = 2 * π / p * Real.Gamma (2 / p)
Module: Mathlib.MeasureTheory.Integral.Gamma

Goal state before:
pp: case e'_3
p b : ℝ
hp : 1 ≤ p
hb : 0 < b
⊢ π * b ^ (-2 / p) * Real.Gamma (2 / p + 1) = 2 * π / p * b ^ (-2 / p) * Real.Gamma (2 / p)

Tactic:
Real.Gamma_add_one (div_ne_zero two_ne_zero (by linarith))

Goal state after:
case e'_3
p b : ℝ
hp : 1 ≤ p
hb : 0 < b
⊢ π * b ^ (-2 / p) * (2 / p * Real.Gamma (2 / p)) = 2 * π / p * b ^ (-2 / p) * Real.Gamma (2 / p)
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
instF : NormedSpace ℝ F := NormedSpace.restrictScalars ℝ 𝕜 F
⊢ (∫ (x : ℝ) in 2 * 0..2 * (1 / 2), curveIntegralFun ω γab x) +
      ∫ (x : ℝ) in 2 * (1 / 2) - 1..2 * 1 - 1, curveIntegralFun ω γbc x =
    ∫ᶜ (x : E) in γab, ω x + ∫ᶜ (x : E) in γbc, ω x

Tactic:
simp only [curveIntegral_def]

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 c : E
ω : E → E →L[𝕜] F
γab : Path a b
γbc : Path b c
h₁ : CurveIntegrable ω γab
h₂ : CurveIntegrable ω γbc
instF : NormedSpace ℝ F := NormedSpace.restrictScalars ℝ 𝕜 F
⊢ (∫ (x : ℝ) in 2 * 0..2 * (1 / 2), curveIntegralFun ω γab x) +
      ∫ (x : ℝ) in 2 * (1 / 2) - 1..2 * 1 - 1, curveIntegralFun ω γbc x =
    (∫ (t : ℝ) in 0..1, curveIntegralFun (fun x ↦ ω x) γab t) + ∫ (t : ℝ) in 0..1, curveIntegralFun (fun x ↦ ω x) γbc t
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 ∈ Ι a b, 0 ≤ g x
⊢ ∃ c ∈ [[a, b]], ∫ (x : ℝ) in a..b, f x * g x ∂μ = f c * ∫ (x : ℝ) in a..b, g x ∂μ

Tactic:
have hg0_ae : ∀ᵐ x ∂(μ.restrict (Ι a b)), 0 ≤ g x := by
    rw [ae_restrict_iff' measurableSet_uIoc]
    exact ae_of_all μ hg0

Goal state after:
a b : ℝ
f g : ℝ → ℝ
μ : Measure ℝ
hf : ContinuousOn f [[a, b]]
hg : IntervalIntegrable g μ a b
hg0 : ∀ x ∈ Ι a b, 0 ≤ g x
hg0_ae : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), 0 ≤ g x
⊢ ∃ c ∈ [[a, b]], ∫ (x : ℝ) in a..b, f x * g x ∂μ = f c * ∫ (x : ℝ) in a..b, g x ∂μ
Module: Mathlib.MeasureTheory.Integral.Regular

Goal state before:
pp: case hs
X : Type u_1
inst✝⁶ : TopologicalSpace X
inst✝⁵ : MeasurableSpace X
inst✝⁴ : BorelSpace X
inst✝³ : T2Space X
U : Set X
hU : IsOpen U
μ : Measure X
inst✝² : IsFiniteMeasure μ
inst✝¹ : μ.InnerRegularCompactLTTop
inst✝ : NormalSpace X
r : ENNReal
hr : r < μ U
K : Set X
KU : K ⊆ U
K_comp : IsCompact K
hK : r < μ K
f : X → ℝ
f_cont : Continuous f
fU : EqOn (⇑{ toFun := f, continuous_toFun := f_cont }) 0 Uᶜ
fK : EqOn (⇑{ toFun := f, continuous_toFun := f_cont }) 1 K
f_range : ∀ (x : X), { toFun := f, continuous_toFun := f_cont } x ∈ Icc 0 1
⊢ ∀ x ∈ K, 1 ≤ f x

Tactic:
· intro x hx
      apply Eq.ge
      exact fK hx

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

Goal state before:
pp: case e_a
n : ℕ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : (Fin (n + 1) → ℂ) → E
c : Fin (n + 1) → ℂ
R : Fin (n + 1) → ℝ
hf : TorusIntegrable f c R
i : Fin (n + 1)
e : ℝ × (Fin n → ℝ) ≃ᵐ (Fin (n + 1) → ℝ) := (MeasurableEquiv.piFinSuccAbove (fun x ↦ ℝ) i).symm
hem : MeasurePreserving (⇑e) volume volume
heπ : (⇑e ⁻¹' Icc 0 fun x ↦ 2 * π) = Icc 0 (2 * π) ×ˢ Icc 0 fun x ↦ 2 * π
θ : ℝ
x✝¹ : θ ∈ Icc 0 (2 * π)
Θ : Fin n → ℝ
x✝ : Θ ∈ Icc 0 fun x ↦ 2 * π
⊢ (fun i_1 ↦ c i_1 + ↑(R i_1) * cexp (↑(i.insertNth θ Θ i_1) * I)) =
    i.insertNth (circleMap (c i) (R i) θ) fun i_1 ↦ c (i.succAbove i_1) + ↑(R (i.succAbove i_1)) * cexp (↑(Θ i_1) * I)

Tactic:
simp only [funext_iff, i.forall_iff_succAbove, circleMap, Fin.insertNth_apply_same,
      Fin.insertNth_apply_succAbove, imp_true_iff, and_self_iff]

Goal state after:
Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real

Goal state before:
pp: case h.refine_2
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
f : X →C_c ℝ
a ε : ℝ
hε : 0 < ε
N : ℕ
hf : range ⇑f ⊆ Ioo a (a + ↑N * ε)
b : ℝ := a + ↑N * ε
y : Fin N → ℝ := fun n ↦ a + ε * (↑↑n + 1)
hy : ∀ {n m : Fin N}, n < m → y n + ε ≤ y m
E : Fin N → Set X := fun n ↦ ⇑f ⁻¹' Ioc (y n - ε) (y n) ∩ tsupport ⇑f
m : Fin N
a✝¹ : m ∈ univ
n : Fin N
a✝ : n ∈ univ
hmn : m ≠ n
x : X
hx : x ∈ {a | (y m - ε < f a ∧ f a ≤ y m) ∧ a ∈ tsupport ⇑f}
⊢ x ∉ {a | (y n - ε < f a ∧ f a ≤ y n) ∧ a ∈ tsupport ⇑f}

Tactic:
rw [mem_ofPred_eq, and_assoc] at hx

Goal state after:
case h.refine_2
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
f : X →C_c ℝ
a ε : ℝ
hε : 0 < ε
N : ℕ
hf : range ⇑f ⊆ Ioo a (a + ↑N * ε)
b : ℝ := a + ↑N * ε
y : Fin N → ℝ := fun n ↦ a + ε * (↑↑n + 1)
hy : ∀ {n m : Fin N}, n < m → y n + ε ≤ y m
E : Fin N → Set X := fun n ↦ ⇑f ⁻¹' Ioc (y n - ε) (y n) ∩ tsupport ⇑f
m : Fin N
a✝¹ : m ∈ univ
n : Fin N
a✝ : n ∈ univ
hmn : m ≠ n
x : X
hx : y m - ε < f x ∧ f x ≤ y m ∧ x ∈ tsupport ⇑f
⊢ x ∉ {a | (y n - ε < f a ∧ f a ≤ y n) ∧ a ∈ tsupport ⇑f}
Module: Mathlib.MeasureTheory.MeasurableSpace.Card

Goal state before:
pp: case refine_2
α : Type u
s : Set (Set α)
t : Set α
ht : t ∈ generateMeasurableRec s (ω_ 1)
⊢ ∃ i, ∃ (_ : i < ω_ 1), ∅ ∈ generateMeasurableRec s i

pp: case refine_3
α : Type u
s : Set (Set α)
t : Set α
ht : t ∈ generateMeasurableRec s (ω_ 1)
⊢ ∀ (u : Set α),
    (∃ i, ∃ (_ : i < ω_ 1), u ∈ generateMeasurableRec s i) →
      (∃ j < ω_ 1, u ∈ generateMeasurableRec s j) → ∃ i, ∃ (_ : i < ω_ 1), uᶜ ∈ generateMeasurableRec s i

pp: case refine_4
α : Type u
s : Set (Set α)
t : Set α
ht : t ∈ generateMeasurableRec s (ω_ 1)
⊢ ∀ (f : ℕ → Set α),
    (∀ (n : ℕ),
        (∃ i, ∃ (_ : i < ω_ 1), f n ∈ generateMeasurableRec s i) ∧ ∃ j < ω_ 1, f n ∈ generateMeasurableRec s j) →
      ∃ i, ∃ (_ : i < ω_ 1), ⋃ n, f n ∈ generateMeasurableRec s i

Tactic:
· exact ⟨0, omega_pos 1, empty_mem_generateMeasurableRec s 0⟩

Goal state after:
case refine_3
α : Type u
s : Set (Set α)
t : Set α
ht : t ∈ generateMeasurableRec s (ω_ 1)
⊢ ∀ (u : Set α),
    (∃ i, ∃ (_ : i < ω_ 1), u ∈ generateMeasurableRec s i) →
      (∃ j < ω_ 1, u ∈ generateMeasurableRec s j) → ∃ i, ∃ (_ : i < ω_ 1), uᶜ ∈ generateMeasurableRec s i

case refine_4
α : Type u
s : Set (Set α)
t : Set α
ht : t ∈ generateMeasurableRec s (ω_ 1)
⊢ ∀ (f : ℕ → Set α),
    (∀ (n : ℕ),
        (∃ i, ∃ (_ : i < ω_ 1), f n ∈ generateMeasurableRec s i) ∧ ∃ j < ω_ 1, f n ∈ generateMeasurableRec s j) →
      ∃ i, ∃ (_ : i < ω_ 1), ⋃ n, f n ∈ generateMeasurableRec s i