mathlib-initiative/mathlib-tactics huggingface dataset:
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 : (i : ι) → Ω → β i
hf_indep : iIndepFun f κ μ
hf_meas : ∀ (i : ι), Measurable (f i)
i✝ j✝ k l : ι
hik : i✝ ≠ k
hil : i✝ ≠ l
hjk : j✝ ≠ k
hjl : j✝ ≠ l
g : (i j : ι) → ((x : ↥{i, j}) → β ↑x) → β i × β j := fun i j v ↦ (v ⟨i, ⋯⟩, v ⟨j, ⋯⟩)
i j : ι
⊢ Measurable (g i j)

Tactic:
fun_prop

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)) μ''
⊢ AEStronglyMeasurable (fun a ↦ F (Y n a) - F (X n a)) μ''

Tactic:
fun_prop

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)‖) μ''
⊢ AEMeasurable (Y n) μ''

Tactic:
fun_prop

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)‖) μ''
⊢ AEStronglyMeasurable F (Measure.map (Y n) μ'')

Tactic:
fun_prop

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)‖) μ''
⊢ AEMeasurable (X n) μ''

Tactic:
fun_prop

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)‖) μ''
⊢ AEStronglyMeasurable F (Measure.map (X n) μ'')

Tactic:
fun_prop

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)‖) μ''
⊢ AEMeasurable (fun x ↦ ‖Y n x - X n x‖) μ''

Tactic:
fun_prop

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)‖) μ''
⊢ AEMeasurable (fun x ↦ ε / 2) μ''

Tactic:
fun_prop

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

Goal state before:
pp: α : Type u_2
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
r : ℝ≥0∞
s : ℕ → Set α
hs : ∀ (n : ℕ), MeasurableSet (s n)
hr₀ : r ≠ 0
hr : ∀ (n : ℕ), r ≤ μ (s n)
M : (α → ℝ) → Set α := fun f ↦ {x | eLpNormEssSup f μ < ↑‖f x‖₊}
⊢ ∃ t, t.Infinite ∧ ∀ ⦃u : Set ℕ⦄, u ⊆ t → u.Finite → 0 < μ (⋂ n ∈ u, s n)

Tactic:
let N : Set α := ⋃ u : Finset ℕ, M (Set.indicator (⋂ n ∈ u, s n) 1)

Goal state after:
α : Type u_2
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
r : ℝ≥0∞
s : ℕ → Set α
hs : ∀ (n : ℕ), MeasurableSet (s n)
hr₀ : r ≠ 0
hr : ∀ (n : ℕ), r ≤ μ (s n)
M : (α → ℝ) → Set α := fun f ↦ {x | eLpNormEssSup f μ < ↑‖f x‖₊}
N : Set α := ⋃ u, M ((⋂ n ∈ u, s n).indicator 1)
⊢ ∃ t, t.Infinite ∧ ∀ ⦃u : Set ℕ⦄, u ⊆ t → u.Finite → 0 < μ (⋂ n ∈ u, s n)
Module: Mathlib.MeasureTheory.Function.ConvergenceInDistribution

Goal state before:
pp: case refine_3
ι : 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
h_le :
  ∀ (n : ι),
    |∫ (ω : E), F ω ∂Measure.map (Y n) μ'' - ∫ (ω : E), F ω ∂Measure.map Z μ'| ≤
      ↑L * (ε / 2) + M * μ''.real {ω | ε / 2 ≤ ‖Y n ω - X n ω‖} +
        |∫ (ω : E), F ω ∂Measure.map (X n) μ'' - ∫ (ω : E), F ω ∂Measure.map Z μ'|
hXZ : Tendsto (fun n ↦ ⟨Measure.map (X n) μ'', ⋯⟩) l (𝓝 ⟨Measure.map Z μ', ⋯⟩)
⊢ Tendsto (fun n ↦ |∫ (ω : E), F ω ∂Measure.map (X n) μ'' - ∫ (ω : E), F ω ∂Measure.map Z μ'|) l (𝓝 0)

Tactic:
tendsto_iff_forall_lipschitz_integral_tendsto

Goal state after:
case refine_3
ι : 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
h_le :
  ∀ (n : ι),
    |∫ (ω : E), F ω ∂Measure.map (Y n) μ'' - ∫ (ω : E), F ω ∂Measure.map Z μ'| ≤
      ↑L * (ε / 2) + M * μ''.real {ω | ε / 2 ≤ ‖Y n ω - X n ω‖} +
        |∫ (ω : E), F ω ∂Measure.map (X n) μ'' - ∫ (ω : E), F ω ∂Measure.map Z μ'|
hXZ :
  ∀ (f : E → ℝ),
    (∃ C, ∀ (x y : E), dist (f x) (f y) ≤ C) →
      (∃ L, LipschitzWith L f) →
        Tendsto (fun i ↦ ∫ (ω : E), f ω ∂↑⟨Measure.map (X i) μ'', ⋯⟩) l (𝓝 (∫ (ω : E), f ω ∂↑⟨Measure.map Z μ', ⋯⟩))
⊢ Tendsto (fun n ↦ |∫ (ω : E), F ω ∂Measure.map (X n) μ'' - ∫ (ω : E), F ω ∂Measure.map Z μ'|) l (𝓝 0)
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) μ''
hX : ∀ (i : ι), AEMeasurable (X i) μ''
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    fun x ↦ (x, c)

Tactic:
fun_prop

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
Z : Ω' → E
l : Filter ι
inst✝³ : SeminormedAddCommGroup E
inst✝² : SecondCountableTopology E
inst✝¹ : BorelSpace E
X Y : ι → Ω'' → E
inst✝ : l.IsCountablyGenerated
c : E
hXZ : TendstoInDistribution X l Z (fun x ↦ μ'') μ'
hY_tendsto : TendstoInMeasure μ'' Y l fun x ↦ c
hY : ∀ (i : ι), AEMeasurable (Y i) μ''
⊢ Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun x ↦ x.1 + x.2

Tactic:
fun_prop

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

Goal state before:
pp: case pos
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝² : Preorder ι
E : Type u_4
inst✝¹ : Zero E
inst✝ : TopologicalSpace E
ℱ : Filtration ι m
f : ι → Ω → E
μ : Measure Ω
h : ∃ g, StronglyMeasurable g ∧ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun n ↦ f n ω) atTop (𝓝 (g ω))
⊢ StronglyMeasurable (Classical.choose h)

pp: case neg
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝² : Preorder ι
E : Type u_4
inst✝¹ : Zero E
inst✝ : TopologicalSpace E
ℱ : Filtration ι m
f : ι → Ω → E
μ : Measure Ω
h : ¬∃ g, StronglyMeasurable g ∧ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun n ↦ f n ω) atTop (𝓝 (g ω))
⊢ StronglyMeasurable 0

Tactic:
exacts [(Classical.choose_spec h).1, stronglyMeasurable_zero]

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 : ι
⊢ Measurable ⇑(MeasurableEquiv.piCongrLeft (fun i_1 ↦ X ↑i_1) (Equiv.IicFinsetSet i))

Tactic:
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 : ι
⊢ Measurable ⇑(MeasurableEquiv.piCongrLeft (fun i_1 ↦ X ↑i_1) (Equiv.IicFinsetSet i).symm)

Tactic:
fun_prop

Goal state after:
Module: Mathlib.MeasureTheory.Function.SpecialFunctions.Sinc

Goal state before:
pp: μ : Measure ℝ
inst✝ : IsFiniteMeasure μ
⊢ Integrable (fun x ↦ 1) μ

Tactic:
fun_prop

Goal state after:
Module: Mathlib.MeasureTheory.Function.SpecialFunctions.Sinc

Goal state before:
pp: μ : Measure ℝ
inst✝ : IsFiniteMeasure μ
⊢ AEStronglyMeasurable sinc μ

Tactic:
fun_prop

Goal state after:
Module: Mathlib.MeasureTheory.Function.SpecialFunctions.Inner

Goal state before:
pp: α : Type u_1
𝕜 : Type u_2
E : Type u_3
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
m : MeasurableSpace α
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
inst✝ : SecondCountableTopology E
μ : MeasureTheory.Measure α
f g : α → E
hf : AEMeasurable f μ
hg : AEMeasurable g μ
⊢ AEMeasurable (fun x ↦ ⟪f x, g x⟫) μ

Tactic:
fun_prop

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

Goal state before:
pp: M : Type u_1
F : Type u_2
inst✝³ : Monoid M
mM : MeasurableSpace M
inst✝² : MeasurableMul₂ M
inst✝¹ : NormedAddCommGroup F
μ ν : Measure M
f : M → F
inst✝ : SFinite ν
hf : AEStronglyMeasurable f (μ ∗ₘ ν)
⊢ AEMeasurable (fun x ↦ x.1 * x.2) (μ.prod ν)

Tactic:
fun_prop

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

Goal state before:
pp: M : Type u_1
F : Type u_2
inst✝³ : Monoid M
mM : MeasurableSpace M
inst✝² : MeasurableMul₂ M
inst✝¹ : NormedAddCommGroup F
μ ν : Measure M
f : M → F
inst✝ : SFinite ν
hf : AEStronglyMeasurable f (μ ∗ₘ ν)
⊢ Measurable fun x ↦ x.1 * x.2

Tactic:
fun_prop

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

Goal state before:
pp: M : Type u_1
F : Type u_2
inst✝⁵ : Monoid M
mM : MeasurableSpace M
inst✝⁴ : MeasurableMul₂ M
inst✝³ : NormedAddCommGroup F
μ ν : Measure M
f : M → F
inst✝² : NormedSpace ℝ F
inst✝¹ : SFinite μ
inst✝ : SFinite ν
hf : Integrable f (μ ∗ₘ ν)
⊢ AEMeasurable (fun x ↦ x.1 * x.2) (μ.prod ν)

Tactic:
fun_prop

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
inst✝ : SMulInvariantMeasure G X μ
hfoel : IsFoelner G μ (↑u) F
g h : G
s : Set X
⊢ mean μ u F (g • s) = mean μ u F (h • s)

Tactic:
suffices hle : ∀ g h, mean μ u F (g • s) ≤ mean μ u F (h • s) by
    exact le_antisymm (hle g h) (hle h g)
  intro g h
  rw [← add_zero <| mean μ u F (h • s)]
  refine le_of_tendsto_of_tendsto
    (hfoel.tendsto_nhds_mean (g • s))
    (hfoel.tendsto_nhds_mean (h • s) |>.add <| hfoel.tendsto_meas_smul_symmDiff_smul g⁻¹ h⁻¹) ?_
  filter_upwards [hfoel.eventually_meas_ne_zero] with i hi
  rw [← tsub_le_iff_left, ← ENNReal.sub_div <| fun _ _ ↦ hi]
  refine ENNReal.div_le_div_right (le_trans ?_ (measure_mono <| @inter_subset_right _ s _)) _
  simpa [inter_symmDiff_distrib_left, ← measure_inter_inv_smul] using le_measure_symmDiff

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

Goal state before:
pp: case refine_1
G : Type u_1
inst✝⁶ : TopologicalSpace G
inst✝⁵ : Group G
inst✝⁴ : IsTopologicalGroup G
inst✝³ : LocallyCompactSpace G
inst✝² : MeasurableSpace G
inst✝¹ : BorelSpace G
μ : Measure G
inst✝ : μ.IsHaarMeasure
g : G
ν : Measure G := haar
f : G → ℝ
f_cont : Continuous f
f_comp : HasCompactSupport ⇑{ toFun := f, continuous_toFun := f_cont }
f_nonneg : 0 ≤ { toFun := f, continuous_toFun := f_cont }
f_one : { toFun := f, continuous_toFun := f_cont } 1 ≠ 0
int_f_ne_zero : ∀ (μ₀ : Measure G) [μ₀.IsHaarMeasure], ∫ (x : G), f x ∂μ₀ ≠ 0
⊢ Continuous fun x ↦ f (x * g)

pp: case refine_2
G : Type u_1
inst✝⁶ : TopologicalSpace G
inst✝⁵ : Group G
inst✝⁴ : IsTopologicalGroup G
inst✝³ : LocallyCompactSpace G
inst✝² : MeasurableSpace G
inst✝¹ : BorelSpace G
μ : Measure G
inst✝ : μ.IsHaarMeasure
g : G
ν : Measure G := haar
f : G → ℝ
f_cont : Continuous f
f_comp : HasCompactSupport ⇑{ toFun := f, continuous_toFun := f_cont }
f_nonneg : 0 ≤ { toFun := f, continuous_toFun := f_cont }
f_one : { toFun := f, continuous_toFun := f_cont } 1 ≠ 0
int_f_ne_zero : ∀ (μ₀ : Measure G) [μ₀.IsHaarMeasure], ∫ (x : G), f x ∂μ₀ ≠ 0
⊢ HasCompactSupport fun x ↦ f (x * g)

Tactic:
· exact Continuous.comp' f_cont (continuous_mul_const g)

Goal state after:
case refine_2
G : Type u_1
inst✝⁶ : TopologicalSpace G
inst✝⁵ : Group G
inst✝⁴ : IsTopologicalGroup G
inst✝³ : LocallyCompactSpace G
inst✝² : MeasurableSpace G
inst✝¹ : BorelSpace G
μ : Measure G
inst✝ : μ.IsHaarMeasure
g : G
ν : Measure G := haar
f : G → ℝ
f_cont : Continuous f
f_comp : HasCompactSupport ⇑{ toFun := f, continuous_toFun := f_cont }
f_nonneg : 0 ≤ { toFun := f, continuous_toFun := f_cont }
f_one : { toFun := f, continuous_toFun := f_cont } 1 ≠ 0
int_f_ne_zero : ∀ (μ₀ : Measure G) [μ₀.IsHaarMeasure], ∫ (x : G), f x ∂μ₀ ≠ 0
⊢ HasCompactSupport fun x ↦ f (x * g)
Module: Mathlib.MeasureTheory.Integral.CircleTransform

Goal state before:
pp: case hg.hf
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
hR : 0 < R
f : ℂ → E
z w : ℂ
hf : ContinuousOn f (sphere z R)
hw : w ∈ ball z R
⊢ Continuous fun x ↦ circleMap 0 R x * I

Tactic:
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)) μ
hfnEcε : eLpNorm (Eᶜ.indicator (f n)) p μ ≤ ε / 3
hmfngEc : AEStronglyMeasurable (Eᶜ.indicator (f n - g)) μ
hfngEcε : eLpNorm (Eᶜ.indicator (f n - g)) p μ ≤ ε / 3 + ε / 3
⊢ eLpNorm (f n - g) p μ = eLpNorm (Eᶜ.indicator (f n - g) + E.indicator (f n - g)) p μ

Tactic:
congr; exact (E.indicator_compl_add_self _).symm

Goal state after:
Module: Mathlib.Topology.Homotopy.Affine

Goal state before:
pp: X : Type u_1
E : Type u_2
inst✝⁵ : TopologicalSpace X
inst✝⁴ : AddCommGroup E
inst✝³ : TopologicalSpace E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : Module ℝ E
inst✝ : ContinuousSMul ℝ E
f g : C(X, E)
⊢ Continuous fun x ↦ ↑x.1 • (g x.2 - f x.2) + f x.2

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Topology.ContinuousMap.CompactlySupported

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁷ : TopologicalSpace α
inst✝⁶ : R1Space α
inst✝⁵ : Group α
inst✝⁴ : TopologicalSpace β
inst✝³ : R1Space β
inst✝² : Group β
inst✝¹ : ContinuousMul β
inst✝ : NormedAddCommGroup γ
φ : α →* β
hφ : Topology.IsClosedEmbedding ⇑φ
f : β →C_c γ
b : β
⊢ Continuous fun a ↦ f (b * φ a)

Tactic:
fun_prop

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 c : E
ω : E → E →L[𝕜] F
γab : Path a b
γbc : Path b c
t : ℝ
ht₀ : 0 < t
ht : t < 1 / 2
⊢ curveIntegralFun ω (γab.trans γbc) t = 2 • curveIntegralFun ω γab (2 * t)

Tactic:
exact curveIntegralFun_trans_of_lt_half ω γab γbc ht

Goal state after: