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

Goal state before:
pp: κ : Type u_2
Z : Type u_3
Y : κ → Type u_6
mY : (j : κ) → MeasurableSpace (Y j)
inst✝⁹ : (j : κ) → TopologicalSpace (Y j)
inst✝⁸ : ∀ (j : κ), BorelSpace (Y j)
inst✝⁷ : ∀ (j : κ), HasOuterApproxClosed (Y j)
mZ : MeasurableSpace Z
inst✝⁶ : TopologicalSpace Z
inst✝⁵ : BorelSpace Z
inst✝⁴ : HasOuterApproxClosed Z
inst✝³ : Fintype κ
μ : Measure Z
ν : Measure ((j : κ) → Y j)
ξ : Measure (Z × ((j : κ) → Y j))
inst✝² : IsFiniteMeasure μ
inst✝¹ : IsFiniteMeasure ν
inst✝ : IsFiniteMeasure ξ
h :
  ∀ (f : Z →ᵇ ℝ) (g : (j : κ) → Y j →ᵇ ℝ),
    ∫ (p : Z × ((j : κ) → Y j)), f p.1 * ∏ j, (g j) (p.2 j) ∂ξ =
      (∫ (z : Z), f z ∂μ) * ∫ (y : (j : κ) → Y j), ∏ j, (g j) (y j) ∂ν
f : Z →ᵇ ℝ
g : (j : κ) → Y j →ᵇ ℝ
⊢ ∫ (z : Z × ((j : κ) → Y j)), f z.1 * ∏ j, (g j) (z.2 j) ∂μ.prod ν =
    ∫ (p : Z × ((j : κ) → Y j)), f p.1 * ∏ j, (g j) (p.2 j) ∂μ.prod ν

Tactic:
]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.PreVariation

Goal state before:
pp: X : Type u_1
inst✝ : MeasurableSpace X
f : Set X → ℝ≥0∞
s : ℕ → Set X
hs : ∀ (i : ℕ), MeasurableSet (s i)
hs' : Pairwise (Disjoint on s)
P : (i : ℕ) → Finpartition ⟨s i, ⋯⟩
n : ℕ
s' : ℕ → Subtype MeasurableSet := fun i ↦ ⟨s i, ⋯⟩
hs_disj : (↑(Finset.range n)).PairwiseDisjoint s'
Q : Finpartition ((Finset.range n).sup fun i ↦ ⟨s i, ⋯⟩) := Finpartition.combine P ⋯
⊢ ⋃ x ∈ Finset.range n, ↑(s' x) ⊆ ↑⟨⋃ i, s i, ⋯⟩

Tactic:
]

Goal state after:
X : Type u_1
inst✝ : MeasurableSpace X
f : Set X → ℝ≥0∞
s : ℕ → Set X
hs : ∀ (i : ℕ), MeasurableSet (s i)
hs' : Pairwise (Disjoint on s)
P : (i : ℕ) → Finpartition ⟨s i, ⋯⟩
n : ℕ
s' : ℕ → Subtype MeasurableSet := fun i ↦ ⟨s i, ⋯⟩
hs_disj : (↑(Finset.range n)).PairwiseDisjoint s'
Q : Finpartition ((Finset.range n).sup fun i ↦ ⟨s i, ⋯⟩) := Finpartition.combine P ⋯
⊢ ⋃ x ∈ Finset.range n, ↑(s' x) ⊆ ↑⟨⋃ i, s i, ⋯⟩
Module: Mathlib.MeasureTheory.Measure.HasOuterApproxClosedProd

Goal state before:
pp: Z : Type u_3
T : Type u_4
mZ : MeasurableSpace Z
inst✝⁷ : TopologicalSpace Z
inst✝⁶ : BorelSpace Z
inst✝⁵ : HasOuterApproxClosed Z
mT : MeasurableSpace T
inst✝⁴ : TopologicalSpace T
inst✝³ : BorelSpace T
inst✝² : HasOuterApproxClosed T
μ ν : Measure (Z × T)
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h : ∀ (f : Z →ᵇ ℝ) (g : T →ᵇ ℝ), ∫ (p : Z × T), f p.1 * g p.2 ∂μ = ∫ (p : Z × T), f p.1 * g p.2 ∂ν
e : Z × T ≃ᵐ (Unit → Z) × (Unit → T) :=
  ((MeasurableEquiv.funUnique Unit Z).prodCongr (MeasurableEquiv.funUnique Unit T)).symm
⊢ Measure.map (⇑e) μ = Measure.map (⇑e) ν

Tactic:
]

Goal state after:
Z : Type u_3
T : Type u_4
mZ : MeasurableSpace Z
inst✝⁷ : TopologicalSpace Z
inst✝⁶ : BorelSpace Z
inst✝⁵ : HasOuterApproxClosed Z
mT : MeasurableSpace T
inst✝⁴ : TopologicalSpace T
inst✝³ : BorelSpace T
inst✝² : HasOuterApproxClosed T
μ ν : Measure (Z × T)
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h : ∀ (f : Z →ᵇ ℝ) (g : T →ᵇ ℝ), ∫ (p : Z × T), f p.1 * g p.2 ∂μ = ∫ (p : Z × T), f p.1 * g p.2 ∂ν
e : Z × T ≃ᵐ (Unit → Z) × (Unit → T) :=
  ((MeasurableEquiv.funUnique Unit Z).prodCongr (MeasurableEquiv.funUnique Unit T)).symm
⊢ Measure.map (⇑e) μ = Measure.map (⇑e) ν
Module: Mathlib.MeasureTheory.Measure.LevyConvergence

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : ℕ → Measure E
inst✝ : ∀ (i : ℕ), IsProbabilityMeasure (μ i)
f : E → ℂ
hf : ContinuousAt f 0
h : ∀ (t : E), Tendsto (fun n ↦ charFun (μ n) t) atTop (𝓝 (f t))
z : E
hz : ‖z‖ = 1
h_le_4 : ∀ (n : ℕ) (r : ℝ), 0 < r → 2⁻¹ * r * ‖∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - charFun (μ n) (t • z)‖ ≤ 4
h_le :
  ∀ (n : ℕ) (r : ℝ),
    0 < r → (μ n).real {x | r < |⟪z, x⟫|} ≤ 2⁻¹ * r * ‖∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - charFun (μ n) (t • z)‖
h_limsup_le :
  ∀ (r : ℝ),
    0 < r →
      limsup (fun n ↦ (μ n).real {x | r < |⟪z, x⟫|}) atTop ≤ 2⁻¹ * r * ‖∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - f (t • z)‖
ε : ℝ
hε : ε > 0
hf0 : f 0 = 1
hf_tendsto : ∀ (ε : ℝ), 0 < ε → ∃ δ, 0 < δ ∧ ∀ ⦃x : E⦄, ‖x‖ < δ → ‖1 - f x‖ < ε
δ : ℝ
hδ : 0 < δ
hδ_lt : ∀ ⦃x : E⦄, ‖x‖ < δ → ‖1 - f x‖ < ε / 4
r : ℝ
hrδ : 4 * δ⁻¹ ≤ r
hr : 0 < r
hr' : -(2 * r⁻¹) ≤ 2 * r⁻¹
x : ℝ
hx : x ∈ Set.Ioc (-(2 * r⁻¹)) (2 * r⁻¹)
⊢ (δ / 2)⁻¹ < r

Tactic:
]

Goal state after:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : ℕ → Measure E
inst✝ : ∀ (i : ℕ), IsProbabilityMeasure (μ i)
f : E → ℂ
hf : ContinuousAt f 0
h : ∀ (t : E), Tendsto (fun n ↦ charFun (μ n) t) atTop (𝓝 (f t))
z : E
hz : ‖z‖ = 1
h_le_4 : ∀ (n : ℕ) (r : ℝ), 0 < r → 2⁻¹ * r * ‖∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - charFun (μ n) (t • z)‖ ≤ 4
h_le :
  ∀ (n : ℕ) (r : ℝ),
    0 < r → (μ n).real {x | r < |⟪z, x⟫|} ≤ 2⁻¹ * r * ‖∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - charFun (μ n) (t • z)‖
h_limsup_le :
  ∀ (r : ℝ),
    0 < r →
      limsup (fun n ↦ (μ n).real {x | r < |⟪z, x⟫|}) atTop ≤ 2⁻¹ * r * ‖∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - f (t • z)‖
ε : ℝ
hε : ε > 0
hf0 : f 0 = 1
hf_tendsto : ∀ (ε : ℝ), 0 < ε → ∃ δ, 0 < δ ∧ ∀ ⦃x : E⦄, ‖x‖ < δ → ‖1 - f x‖ < ε
δ : ℝ
hδ : 0 < δ
hδ_lt : ∀ ⦃x : E⦄, ‖x‖ < δ → ‖1 - f x‖ < ε / 4
r : ℝ
hrδ : 4 * δ⁻¹ ≤ r
hr : 0 < r
hr' : -(2 * r⁻¹) ≤ 2 * r⁻¹
x : ℝ
hx : x ∈ Set.Ioc (-(2 * r⁻¹)) (2 * r⁻¹)
⊢ (δ / 2)⁻¹ < r
Module: Mathlib.MeasureTheory.Measure.HasOuterApproxClosedProd

Goal state before:
pp: Z : Type u_3
T : Type u_4
mZ : MeasurableSpace Z
inst✝⁷ : TopologicalSpace Z
inst✝⁶ : BorelSpace Z
inst✝⁵ : HasOuterApproxClosed Z
mT : MeasurableSpace T
inst✝⁴ : TopologicalSpace T
inst✝³ : BorelSpace T
inst✝² : HasOuterApproxClosed T
μ ν : Measure (Z × T)
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h : ∀ (f : Z →ᵇ ℝ) (g : T →ᵇ ℝ), ∫ (p : Z × T), f p.1 * g p.2 ∂μ = ∫ (p : Z × T), f p.1 * g p.2 ∂ν
e : Z × T ≃ᵐ (Unit → Z) × (Unit → T) :=
  ((MeasurableEquiv.funUnique Unit Z).prodCongr (MeasurableEquiv.funUnique Unit T)).symm
f : Unit → Z →ᵇ ℝ
g : Unit → T →ᵇ ℝ
⊢ ∫ (x : Z × T), (∏ i, (f i) ((e x).1 i)) * ∏ j, (g j) ((e x).2 j) ∂μ =
    ∫ (x : Z × T), (∏ i, (f i) ((e x).1 i)) * ∏ j, (g j) ((e x).2 j) ∂ν

Tactic:
]

Goal state after:
Z : Type u_3
T : Type u_4
mZ : MeasurableSpace Z
inst✝⁷ : TopologicalSpace Z
inst✝⁶ : BorelSpace Z
inst✝⁵ : HasOuterApproxClosed Z
mT : MeasurableSpace T
inst✝⁴ : TopologicalSpace T
inst✝³ : BorelSpace T
inst✝² : HasOuterApproxClosed T
μ ν : Measure (Z × T)
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h : ∀ (f : Z →ᵇ ℝ) (g : T →ᵇ ℝ), ∫ (p : Z × T), f p.1 * g p.2 ∂μ = ∫ (p : Z × T), f p.1 * g p.2 ∂ν
e : Z × T ≃ᵐ (Unit → Z) × (Unit → T) :=
  ((MeasurableEquiv.funUnique Unit Z).prodCongr (MeasurableEquiv.funUnique Unit T)).symm
f : Unit → Z →ᵇ ℝ
g : Unit → T →ᵇ ℝ
⊢ ∫ (x : Z × T), (∏ i, (f i) ((e x).1 i)) * ∏ j, (g j) ((e x).2 j) ∂μ =
    ∫ (x : Z × T), (∏ i, (f i) ((e x).1 i)) * ∏ j, (g j) ((e x).2 j) ∂ν
Module: Mathlib.MeasureTheory.Measure.HasOuterApproxClosedProd

Goal state before:
pp: Z : Type u_3
T : Type u_4
mZ : MeasurableSpace Z
inst✝⁸ : TopologicalSpace Z
inst✝⁷ : BorelSpace Z
inst✝⁶ : HasOuterApproxClosed Z
mT : MeasurableSpace T
inst✝⁵ : TopologicalSpace T
inst✝⁴ : BorelSpace T
inst✝³ : HasOuterApproxClosed T
μ : Measure Z
ν : Measure T
ξ : Measure (Z × T)
inst✝² : IsFiniteMeasure μ
inst✝¹ : IsFiniteMeasure ν
inst✝ : IsFiniteMeasure ξ
h : ∀ (f : Z →ᵇ ℝ) (g : T →ᵇ ℝ), ∫ (p : Z × T), f p.1 * g p.2 ∂ξ = (∫ (z : Z), f z ∂μ) * ∫ (t : T), g t ∂ν
f : Z →ᵇ ℝ
g : T →ᵇ ℝ
⊢ ∫ (z : Z × T), f z.1 * g z.2 ∂μ.prod ν = ∫ (p : Z × T), f p.1 * g p.2 ∂μ.prod ν

Tactic:
]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.PreVariation

Goal state before:
pp: X : Type u_1
inst✝ : MeasurableSpace X
f : Set X → ℝ≥0∞
s : ℕ → Set X
hs : ∀ (i : ℕ), MeasurableSet (s i)
hs' : Pairwise (Disjoint on s)
n : ℕ
hn : ¬n = 0
ε' : ℝ≥0
hε' : 0 < ε'
hsnetop : preVariationFun f (⋃ i, s i) < ∞
ε : ℝ≥0 := ε' / ↑n
hε : 0 < ε
hs'' : ∀ (i : ℕ), preVariationFun f (s i) ≠ ∞
P : (i : ℕ) → Finpartition ⟨s i, ⋯⟩
hP : ∀ (i : ℕ), preVariationFun f (s i) ≤ ∑ p ∈ (P i).parts, f ↑p + ↑ε
⊢ ∑ x ∈ Finset.range n, ∑ p ∈ (P x).parts, f ↑p + ∑ x ∈ Finset.range n, ↑ε =
    ∑ i ∈ Finset.range n, ∑ p ∈ (P i).parts, f ↑p + ↑ε'

Tactic:
]

Goal state after:
X : Type u_1
inst✝ : MeasurableSpace X
f : Set X → ℝ≥0∞
s : ℕ → Set X
hs : ∀ (i : ℕ), MeasurableSet (s i)
hs' : Pairwise (Disjoint on s)
n : ℕ
hn : ¬n = 0
ε' : ℝ≥0
hε' : 0 < ε'
hsnetop : preVariationFun f (⋃ i, s i) < ∞
ε : ℝ≥0 := ε' / ↑n
hε : 0 < ε
hs'' : ∀ (i : ℕ), preVariationFun f (s i) ≠ ∞
P : (i : ℕ) → Finpartition ⟨s i, ⋯⟩
hP : ∀ (i : ℕ), preVariationFun f (s i) ≤ ∑ p ∈ (P i).parts, f ↑p + ↑ε
⊢ ∑ x ∈ Finset.range n, ∑ p ∈ (P x).parts, f ↑p + ∑ x ∈ Finset.range n, ↑ε =
    ∑ i ∈ Finset.range n, ∑ p ∈ (P i).parts, f ↑p + ↑ε'
Module: Mathlib.MeasureTheory.Measure.LevyConvergence

Goal state before:
pp: case refine_1
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : ℕ → Measure E
inst✝ : ∀ (i : ℕ), IsProbabilityMeasure (μ i)
f : E → ℂ
hf : ContinuousAt f 0
h : ∀ (t : E), Tendsto (fun n ↦ charFun (μ n) t) atTop (𝓝 (f t))
z : E
hz : ‖z‖ = 1
h_le_4 : ∀ (n : ℕ) (r : ℝ), 0 < r → 2⁻¹ * r * ‖∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - charFun (μ n) (t • z)‖ ≤ 4
h_le :
  ∀ (n : ℕ) (r : ℝ),
    0 < r → (μ n).real {x | r < |⟪z, x⟫|} ≤ 2⁻¹ * r * ‖∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - charFun (μ n) (t • z)‖
h_limsup_le :
  ∀ (r : ℝ),
    0 < r →
      limsup (fun n ↦ (μ n).real {x | r < |⟪z, x⟫|}) atTop ≤ 2⁻¹ * r * ‖∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - f (t • z)‖
ε : ℝ
hε : ε > 0
hf0 : f 0 = 1
hf_tendsto : ∀ (ε : ℝ), 0 < ε → ∃ δ, 0 < δ ∧ ∀ ⦃x : E⦄, ‖x‖ < δ → ‖1 - f x‖ < ε
δ : ℝ
hδ : 0 < δ
hδ_lt : ∀ ⦃x : E⦄, ‖x‖ < δ → ‖1 - f x‖ < ε / 4
r : ℝ
hrδ : 4 * δ⁻¹ ≤ r
hr : 0 < r
hr' : -(2 * r⁻¹) ≤ 2 * r⁻¹
h_le_Ioc : ∀ x ∈ Set.Ioc (-(2 * r⁻¹)) (2 * r⁻¹), ‖1 - f (x • z)‖ ≤ ε / 4
⊢ 2⁻¹ * r * ‖∫ (t : ℝ) in -(2 * r⁻¹)..2 * r⁻¹, 1 - f (t • z)‖ < ε

Tactic:
]

Goal state after:
case refine_1
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : ℕ → Measure E
inst✝ : ∀ (i : ℕ), IsProbabilityMeasure (μ i)
f : E → ℂ
hf : ContinuousAt f 0
h : ∀ (t : E), Tendsto (fun n ↦ charFun (μ n) t) atTop (𝓝 (f t))
z : E
hz : ‖z‖ = 1
h_le_4 : ∀ (n : ℕ) (r : ℝ), 0 < r → 2⁻¹ * r * ‖∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - charFun (μ n) (t • z)‖ ≤ 4
h_le :
  ∀ (n : ℕ) (r : ℝ),
    0 < r → (μ n).real {x | r < |⟪z, x⟫|} ≤ 2⁻¹ * r * ‖∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - charFun (μ n) (t • z)‖
h_limsup_le :
  ∀ (r : ℝ),
    0 < r →
      limsup (fun n ↦ (μ n).real {x | r < |⟪z, x⟫|}) atTop ≤ 2⁻¹ * r * ‖∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - f (t • z)‖
ε : ℝ
hε : ε > 0
hf0 : f 0 = 1
hf_tendsto : ∀ (ε : ℝ), 0 < ε → ∃ δ, 0 < δ ∧ ∀ ⦃x : E⦄, ‖x‖ < δ → ‖1 - f x‖ < ε
δ : ℝ
hδ : 0 < δ
hδ_lt : ∀ ⦃x : E⦄, ‖x‖ < δ → ‖1 - f x‖ < ε / 4
r : ℝ
hrδ : 4 * δ⁻¹ ≤ r
hr : 0 < r
hr' : -(2 * r⁻¹) ≤ 2 * r⁻¹
h_le_Ioc : ∀ x ∈ Set.Ioc (-(2 * r⁻¹)) (2 * r⁻¹), ‖1 - f (x • z)‖ ≤ ε / 4
⊢ 2⁻¹ * r * ‖∫ (t : ℝ) in -(2 * r⁻¹)..2 * r⁻¹, 1 - f (t • z)‖ < ε
Module: Mathlib.MeasureTheory.Measure.LevyConvergence

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : ℕ → Measure E
inst✝ : ∀ (i : ℕ), IsProbabilityMeasure (μ i)
f : E → ℂ
hf : ContinuousAt f 0
h : ∀ (t : E), Tendsto (fun n ↦ charFun (μ n) t) atTop (𝓝 (f t))
z : E
hz : ‖z‖ = 1
h_le_4 : ∀ (n : ℕ) (r : ℝ), 0 < r → 2⁻¹ * r * ‖∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - charFun (μ n) (t • z)‖ ≤ 4
h_le :
  ∀ (n : ℕ) (r : ℝ),
    0 < r → (μ n).real {x | r < |⟪z, x⟫|} ≤ 2⁻¹ * r * ‖∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - charFun (μ n) (t • z)‖
h_limsup_le :
  ∀ (r : ℝ),
    0 < r →
      limsup (fun n ↦ (μ n).real {x | r < |⟪z, x⟫|}) atTop ≤ 2⁻¹ * r * ‖∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - f (t • z)‖
ε : ℝ
hε : ε > 0
hf0 : f 0 = 1
hf_tendsto : ∀ (ε : ℝ), 0 < ε → ∃ δ, 0 < δ ∧ ∀ ⦃x : E⦄, ‖x‖ < δ → ‖1 - f x‖ < ε
δ : ℝ
hδ : 0 < δ
hδ_lt : ∀ ⦃x : E⦄, ‖x‖ < δ → ‖1 - f x‖ < ε / 4
r : ℝ
hrδ : 4 * δ⁻¹ ≤ r
hr : 0 < r
hr' : -(2 * r⁻¹) ≤ 2 * r⁻¹
h_le_Ioc : ∀ x ∈ Set.Ioc (-(2 * r⁻¹)) (2 * r⁻¹), ‖1 - f (x • z)‖ ≤ ε / 4
⊢ 2⁻¹ * r * ∫ (x : ℝ) in -(2 * r⁻¹)..2 * r⁻¹, ‖1 - f (x • z)‖ ≤
    2⁻¹ * r * ∫ (t : ℝ) in -(2 * r⁻¹)..2 * r⁻¹, ‖1 - f (t • z)‖

Tactic:
]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.HasOuterApproxClosedProd

Goal state before:
pp: ι : Type u_1
κ : Type u_2
X : ι → Type u_5
Y : κ → Type u_6
mX : (i : ι) → MeasurableSpace (X i)
inst✝¹⁰ : (i : ι) → TopologicalSpace (X i)
inst✝⁹ : ∀ (i : ι), BorelSpace (X i)
inst✝⁸ : ∀ (i : ι), HasOuterApproxClosed (X i)
mY : (j : κ) → MeasurableSpace (Y j)
inst✝⁷ : (j : κ) → TopologicalSpace (Y j)
inst✝⁶ : ∀ (j : κ), BorelSpace (Y j)
inst✝⁵ : ∀ (j : κ), HasOuterApproxClosed (Y j)
inst✝⁴ : Finite ι
inst✝³ : Finite κ
μ : Measure ((i : ι) → X i)
ν : Measure ((j : κ) → Y j)
ξ : Measure (((i : ι) → X i) × ((j : κ) → Y j))
inst✝² : IsFiniteMeasure μ
inst✝¹ : IsFiniteMeasure ν
inst✝ : IsFiniteMeasure ξ
h :
  ∀ (f : ((i : ι) → X i) →ᵇ ℝ) (g : ((j : κ) → Y j) →ᵇ ℝ),
    ∫ (p : ((i : ι) → X i) × ((j : κ) → Y j)), f p.1 * g p.2 ∂ξ =
      (∫ (x : (i : ι) → X i), f x ∂μ) * ∫ (y : (j : κ) → Y j), g y ∂ν
f : ((i : ι) → X i) →ᵇ ℝ
g : ((j : κ) → Y j) →ᵇ ℝ
⊢ ∫ (z : ((i : ι) → X i) × ((j : κ) → Y j)), f z.1 * g z.2 ∂μ.prod ν =
    ∫ (p : ((i : ι) → X i) × ((j : κ) → Y j)), f p.1 * g p.2 ∂μ.prod ν

Tactic:
]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.LevyConvergence

Goal state before:
pp: case hbc
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : ℕ → Measure E
inst✝ : ∀ (i : ℕ), IsProbabilityMeasure (μ i)
f : E → ℂ
hf : ContinuousAt f 0
h : ∀ (t : E), Tendsto (fun n ↦ charFun (μ n) t) atTop (𝓝 (f t))
z : E
hz : ‖z‖ = 1
h_le_4 : ∀ (n : ℕ) (r : ℝ), 0 < r → 2⁻¹ * r * ‖∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - charFun (μ n) (t • z)‖ ≤ 4
h_le :
  ∀ (n : ℕ) (r : ℝ),
    0 < r → (μ n).real {x | r < |⟪z, x⟫|} ≤ 2⁻¹ * r * ‖∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - charFun (μ n) (t • z)‖
h_limsup_le :
  ∀ (r : ℝ),
    0 < r →
      limsup (fun n ↦ (μ n).real {x | r < |⟪z, x⟫|}) atTop ≤ 2⁻¹ * r * ‖∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - f (t • z)‖
ε : ℝ
hε : ε > 0
hf0 : f 0 = 1
hf_tendsto : ∀ (ε : ℝ), 0 < ε → ∃ δ, 0 < δ ∧ ∀ ⦃x : E⦄, ‖x‖ < δ → ‖1 - f x‖ < ε
δ : ℝ
hδ : 0 < δ
hδ_lt : ∀ ⦃x : E⦄, ‖x‖ < δ → ‖1 - f x‖ < ε / 4
r : ℝ
hrδ : 4 * δ⁻¹ ≤ r
hr : 0 < r
hr' : -(2 * r⁻¹) ≤ 2 * r⁻¹
h_le_Ioc : ∀ x ∈ Set.Ioc (-(2 * r⁻¹)) (2 * r⁻¹), ‖1 - f (x • z)‖ ≤ ε / 4
⊢ ∫ (x : ℝ) in Set.Ioc (-(2 * r⁻¹)) (2 * r⁻¹), ‖1 - f (x • z)‖ ∂volume ≤ ∫ (t : ℝ) in -(2 * r⁻¹)..2 * r⁻¹, ε / 4

Tactic:
intervalIntegral.integral_of_le hr'

Goal state after:
case hbc
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : ℕ → Measure E
inst✝ : ∀ (i : ℕ), IsProbabilityMeasure (μ i)
f : E → ℂ
hf : ContinuousAt f 0
h : ∀ (t : E), Tendsto (fun n ↦ charFun (μ n) t) atTop (𝓝 (f t))
z : E
hz : ‖z‖ = 1
h_le_4 : ∀ (n : ℕ) (r : ℝ), 0 < r → 2⁻¹ * r * ‖∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - charFun (μ n) (t • z)‖ ≤ 4
h_le :
  ∀ (n : ℕ) (r : ℝ),
    0 < r → (μ n).real {x | r < |⟪z, x⟫|} ≤ 2⁻¹ * r * ‖∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - charFun (μ n) (t • z)‖
h_limsup_le :
  ∀ (r : ℝ),
    0 < r →
      limsup (fun n ↦ (μ n).real {x | r < |⟪z, x⟫|}) atTop ≤ 2⁻¹ * r * ‖∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - f (t • z)‖
ε : ℝ
hε : ε > 0
hf0 : f 0 = 1
hf_tendsto : ∀ (ε : ℝ), 0 < ε → ∃ δ, 0 < δ ∧ ∀ ⦃x : E⦄, ‖x‖ < δ → ‖1 - f x‖ < ε
δ : ℝ
hδ : 0 < δ
hδ_lt : ∀ ⦃x : E⦄, ‖x‖ < δ → ‖1 - f x‖ < ε / 4
r : ℝ
hrδ : 4 * δ⁻¹ ≤ r
hr : 0 < r
hr' : -(2 * r⁻¹) ≤ 2 * r⁻¹
h_le_Ioc : ∀ x ∈ Set.Ioc (-(2 * r⁻¹)) (2 * r⁻¹), ‖1 - f (x • z)‖ ≤ ε / 4
⊢ ∫ (x : ℝ) in Set.Ioc (-(2 * r⁻¹)) (2 * r⁻¹), ‖1 - f (x • z)‖ ∂volume ≤
    ∫ (x : ℝ) in Set.Ioc (-(2 * r⁻¹)) (2 * r⁻¹), ε / 4 ∂volume
Module: Mathlib.MeasureTheory.Measure.LevyConvergence

Goal state before:
pp: case hbc
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : ℕ → Measure E
inst✝ : ∀ (i : ℕ), IsProbabilityMeasure (μ i)
f : E → ℂ
hf : ContinuousAt f 0
h : ∀ (t : E), Tendsto (fun n ↦ charFun (μ n) t) atTop (𝓝 (f t))
z : E
hz : ‖z‖ = 1
h_le_4 : ∀ (n : ℕ) (r : ℝ), 0 < r → 2⁻¹ * r * ‖∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - charFun (μ n) (t • z)‖ ≤ 4
h_le :
  ∀ (n : ℕ) (r : ℝ),
    0 < r → (μ n).real {x | r < |⟪z, x⟫|} ≤ 2⁻¹ * r * ‖∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - charFun (μ n) (t • z)‖
h_limsup_le :
  ∀ (r : ℝ),
    0 < r →
      limsup (fun n ↦ (μ n).real {x | r < |⟪z, x⟫|}) atTop ≤ 2⁻¹ * r * ‖∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - f (t • z)‖
ε : ℝ
hε : ε > 0
hf0 : f 0 = 1
hf_tendsto : ∀ (ε : ℝ), 0 < ε → ∃ δ, 0 < δ ∧ ∀ ⦃x : E⦄, ‖x‖ < δ → ‖1 - f x‖ < ε
δ : ℝ
hδ : 0 < δ
hδ_lt : ∀ ⦃x : E⦄, ‖x‖ < δ → ‖1 - f x‖ < ε / 4
r : ℝ
hrδ : 4 * δ⁻¹ ≤ r
hr : 0 < r
hr' : -(2 * r⁻¹) ≤ 2 * r⁻¹
h_le_Ioc : ∀ x ∈ Set.Ioc (-(2 * r⁻¹)) (2 * r⁻¹), ‖1 - f (x • z)‖ ≤ ε / 4
⊢ ∫ (x : ℝ) in Set.Ioc (-(2 * r⁻¹)) (2 * r⁻¹), ‖1 - f (x • z)‖ ∂volume ≤
    ∫ (x : ℝ) in Set.Ioc (-(2 * r⁻¹)) (2 * r⁻¹), ε / 4 ∂volume

Tactic:
]

Goal state after:
case hbc
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : ℕ → Measure E
inst✝ : ∀ (i : ℕ), IsProbabilityMeasure (μ i)
f : E → ℂ
hf : ContinuousAt f 0
h : ∀ (t : E), Tendsto (fun n ↦ charFun (μ n) t) atTop (𝓝 (f t))
z : E
hz : ‖z‖ = 1
h_le_4 : ∀ (n : ℕ) (r : ℝ), 0 < r → 2⁻¹ * r * ‖∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - charFun (μ n) (t • z)‖ ≤ 4
h_le :
  ∀ (n : ℕ) (r : ℝ),
    0 < r → (μ n).real {x | r < |⟪z, x⟫|} ≤ 2⁻¹ * r * ‖∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - charFun (μ n) (t • z)‖
h_limsup_le :
  ∀ (r : ℝ),
    0 < r →
      limsup (fun n ↦ (μ n).real {x | r < |⟪z, x⟫|}) atTop ≤ 2⁻¹ * r * ‖∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - f (t • z)‖
ε : ℝ
hε : ε > 0
hf0 : f 0 = 1
hf_tendsto : ∀ (ε : ℝ), 0 < ε → ∃ δ, 0 < δ ∧ ∀ ⦃x : E⦄, ‖x‖ < δ → ‖1 - f x‖ < ε
δ : ℝ
hδ : 0 < δ
hδ_lt : ∀ ⦃x : E⦄, ‖x‖ < δ → ‖1 - f x‖ < ε / 4
r : ℝ
hrδ : 4 * δ⁻¹ ≤ r
hr : 0 < r
hr' : -(2 * r⁻¹) ≤ 2 * r⁻¹
h_le_Ioc : ∀ x ∈ Set.Ioc (-(2 * r⁻¹)) (2 * r⁻¹), ‖1 - f (x • z)‖ ≤ ε / 4
⊢ ∫ (x : ℝ) in Set.Ioc (-(2 * r⁻¹)) (2 * r⁻¹), ‖1 - f (x • z)‖ ∂volume ≤
    ∫ (x : ℝ) in Set.Ioc (-(2 * r⁻¹)) (2 * r⁻¹), ε / 4 ∂volume
Module: Mathlib.MeasureTheory.Measure.PreVariation

Goal state before:
pp: X : Type u_1
inst✝ : MeasurableSpace X
f : Set X → ℝ≥0∞
hf : IsSigmaSubadditiveSetFun f
hf' : f ∅ = 0
s : ℕ → Set X
hs : ∀ (i : ℕ), MeasurableSet (s i)
hs' : Pairwise (Disjoint on s)
b : ℝ≥0∞
Q : Finpartition ⟨⋃ i, s i, ⋯⟩
hQ : b < ∑ p ∈ Q.parts, f ↑p
s' : ℕ → Subtype MeasurableSet := fun i ↦ ⟨s i, ⋯⟩
P : (i : ℕ) → Finpartition (s' i) := fun i ↦ Q.restrict ⋯
q : Subtype MeasurableSet
hq : q ∈ Q.parts
⊢ ↑q = ↑q ∩ ⋃ i, s i

Tactic:
]

Goal state after:
X : Type u_1
inst✝ : MeasurableSpace X
f : Set X → ℝ≥0∞
hf : IsSigmaSubadditiveSetFun f
hf' : f ∅ = 0
s : ℕ → Set X
hs : ∀ (i : ℕ), MeasurableSet (s i)
hs' : Pairwise (Disjoint on s)
b : ℝ≥0∞
Q : Finpartition ⟨⋃ i, s i, ⋯⟩
hQ : b < ∑ p ∈ Q.parts, f ↑p
s' : ℕ → Subtype MeasurableSet := fun i ↦ ⟨s i, ⋯⟩
P : (i : ℕ) → Finpartition (s' i) := fun i ↦ Q.restrict ⋯
q : Subtype MeasurableSet
hq : q ∈ Q.parts
⊢ ↑q = ↑q ∩ ⋃ i, s i
Module: Mathlib.MeasureTheory.Measure.HasOuterApproxClosedProd

Goal state before:
pp: ι : Type u_1
T : Type u_4
X : ι → Type u_5
mX : (i : ι) → MeasurableSpace (X i)
inst✝⁹ : (i : ι) → TopologicalSpace (X i)
inst✝⁸ : ∀ (i : ι), BorelSpace (X i)
inst✝⁷ : ∀ (i : ι), HasOuterApproxClosed (X i)
mT : MeasurableSpace T
inst✝⁶ : TopologicalSpace T
inst✝⁵ : BorelSpace T
inst✝⁴ : HasOuterApproxClosed T
inst✝³ : Finite ι
μ : Measure ((i : ι) → X i)
ν : Measure T
ξ : Measure (((i : ι) → X i) × T)
inst✝² : IsFiniteMeasure μ
inst✝¹ : IsFiniteMeasure ν
inst✝ : IsFiniteMeasure ξ
h :
  ∀ (f : ((i : ι) → X i) →ᵇ ℝ) (g : T →ᵇ ℝ),
    ∫ (p : ((i : ι) → X i) × T), f p.1 * g p.2 ∂ξ = (∫ (x : (i : ι) → X i), f x ∂μ) * ∫ (t : T), g t ∂ν
f : ((i : ι) → X i) →ᵇ ℝ
g : T →ᵇ ℝ
⊢ ∫ (z : ((i : ι) → X i) × T), f z.1 * g z.2 ∂μ.prod ν = ∫ (p : ((i : ι) → X i) × T), f p.1 * g p.2 ∂μ.prod ν

Tactic:
]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.LevyConvergence

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : ℕ → Measure E
inst✝ : ∀ (i : ℕ), IsProbabilityMeasure (μ i)
f : E → ℂ
hf : ContinuousAt f 0
h : ∀ (t : E), Tendsto (fun n ↦ charFun (μ n) t) atTop (𝓝 (f t))
z : E
hz : ‖z‖ = 1
h_le_4 : ∀ (n : ℕ) (r : ℝ), 0 < r → 2⁻¹ * r * ‖∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - charFun (μ n) (t • z)‖ ≤ 4
h_le :
  ∀ (n : ℕ) (r : ℝ),
    0 < r → (μ n).real {x | r < |⟪z, x⟫|} ≤ 2⁻¹ * r * ‖∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - charFun (μ n) (t • z)‖
h_limsup_le :
  ∀ (r : ℝ),
    0 < r →
      limsup (fun n ↦ (μ n).real {x | r < |⟪z, x⟫|}) atTop ≤ 2⁻¹ * r * ‖∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - f (t • z)‖
ε : ℝ
hε : ε > 0
hf0 : f 0 = 1
hf_tendsto : ∀ (ε : ℝ), 0 < ε → ∃ δ, 0 < δ ∧ ∀ ⦃x : E⦄, ‖x‖ < δ → ‖1 - f x‖ < ε
δ : ℝ
hδ : 0 < δ
hδ_lt : ∀ ⦃x : E⦄, ‖x‖ < δ → ‖1 - f x‖ < ε / 4
r : ℝ
hrδ : 4 * δ⁻¹ ≤ r
hr : 0 < r
hr' : -(2 * r⁻¹) ≤ 2 * r⁻¹
h_le_Ioc : ∀ x ∈ Set.Ioc (-(2 * r⁻¹)) (2 * r⁻¹), ‖1 - f (x • z)‖ ≤ ε / 4
⊢ ∀ (x : E), Tendsto (fun i ↦ charFun (μ i) x) atTop (𝓝 (f x))

Tactic:
]

Goal state after:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : ℕ → Measure E
inst✝ : ∀ (i : ℕ), IsProbabilityMeasure (μ i)
f : E → ℂ
hf : ContinuousAt f 0
h : ∀ (t : E), Tendsto (fun n ↦ charFun (μ n) t) atTop (𝓝 (f t))
z : E
hz : ‖z‖ = 1
h_le_4 : ∀ (n : ℕ) (r : ℝ), 0 < r → 2⁻¹ * r * ‖∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - charFun (μ n) (t • z)‖ ≤ 4
h_le :
  ∀ (n : ℕ) (r : ℝ),
    0 < r → (μ n).real {x | r < |⟪z, x⟫|} ≤ 2⁻¹ * r * ‖∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - charFun (μ n) (t • z)‖
h_limsup_le :
  ∀ (r : ℝ),
    0 < r →
      limsup (fun n ↦ (μ n).real {x | r < |⟪z, x⟫|}) atTop ≤ 2⁻¹ * r * ‖∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - f (t • z)‖
ε : ℝ
hε : ε > 0
hf0 : f 0 = 1
hf_tendsto : ∀ (ε : ℝ), 0 < ε → ∃ δ, 0 < δ ∧ ∀ ⦃x : E⦄, ‖x‖ < δ → ‖1 - f x‖ < ε
δ : ℝ
hδ : 0 < δ
hδ_lt : ∀ ⦃x : E⦄, ‖x‖ < δ → ‖1 - f x‖ < ε / 4
r : ℝ
hrδ : 4 * δ⁻¹ ≤ r
hr : 0 < r
hr' : -(2 * r⁻¹) ≤ 2 * r⁻¹
h_le_Ioc : ∀ x ∈ Set.Ioc (-(2 * r⁻¹)) (2 * r⁻¹), ‖1 - f (x • z)‖ ≤ ε / 4
⊢ ∀ (x : E), Tendsto (fun i ↦ charFun (μ i) x) atTop (𝓝 (f x))