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

Goal state before:
pp: E : Type u_1
inst✝³ : MeasurableSpace E
inst✝² : TopologicalSpace E
inst✝¹ : T2Space E
inst✝ : BorelSpace E
u : ℕ → ℝ≥0
K : ℕ → Set E
C : ℝ≥0
hu : Tendsto u atTop (𝓝 0)
hK : ∀ (n : ℕ), IsCompact (K n)
h : NormalSpace E ∨ Monotone K
I :
  ∀ (μ : FiniteMeasure E) (n : ℕ),
    ∑ i ∈ Finset.range (n + 1), μ.restrict (disjointed K i) = μ.restrict ((partialSups K) n)
A : ∀ (n : ℕ), IsCompact ((partialSups K) n)
f : Ultrafilter (FiniteMeasure E)
hf : {μ | μ.mass ≤ C ∧ ∀ (n : ℕ), μ (K n)ᶜ ≤ u n} ∈ f
ν : ℕ → FiniteMeasure E
ν_reg : ∀ (n : ℕ), (↑(ν n)).InnerRegular
νK : ∀ (n : ℕ), (ν n) ((partialSups K) n)ᶜ = 0
hν : ∀ (n : ℕ), Tendsto (fun ρ ↦ ρ.restrict (disjointed K n)) (↑f) (𝓝 (ν n))
this✝¹ : Tendsto (fun n ↦ ∑ i ∈ Finset.range (n + 1), ↑(ν i) univ) atTop (𝓝 (∑' (i : ℕ), ↑(ν i) univ))
n : ℕ
this✝ : ∑ i ∈ Finset.range (n + 1), ↑(ν i) univ = ↑(∑ i ∈ Finset.range (n + 1), ν i) univ
this : (∑ i ∈ Finset.range (n + 1), ν i).mass ≤ C
⊢ ↑(∑ i ∈ Finset.range (n + 1), ν i) univ ≤ ↑C

Tactic:
by

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✝² : Fintype ι
inst✝¹ : Fintype κ
μ ν : Measure (((i : ι) → X i) × ((j : κ) → Y j))
inst✝ : IsFiniteMeasure μ
h :
  ∀ (f : (i : ι) → X i →ᵇ ℝ≥0) (g : (j : κ) → Y j →ᵇ ℝ≥0),
    ∫⁻ (p : ((i : ι) → X i) × ((j : κ) → Y j)), ↑(∏ i, (f i) (p.1 i)) * ↑(∏ j, (g j) (p.2 j)) ∂μ =
      ∫⁻ (p : ((i : ι) → X i) × ((j : κ) → Y j)), ↑(∏ i, (f i) (p.1 i)) * ↑(∏ j, (g j) (p.2 j)) ∂ν
hμν : μ univ = ν univ
this✝ : IsFiniteMeasure ν
π : Set (Set (((i : ι) → X i) × ((j : κ) → Y j))) :=
  image2 (fun s t ↦ s ×ˢ t) (univ.pi '' univ.pi fun x ↦ {s | IsClosed[inst✝⁸ x] s})
    (univ.pi '' univ.pi fun x ↦ {t | IsClosed[inst✝⁵ x] t})
hπ1 : IsPiSystem π
hπ2 : Prod.instMeasurableSpace = generateFrom π
s : (i : ι) → Set (X i)
t : (i : κ) → Set (Y i)
hs : ∀ (i : ι), IsClosed[inst✝⁸ i] (s i)
ht : ∀ (i : κ), IsClosed[inst✝⁵ i] (t i)
this :
  ∀ (p : ((i : ι) → X i) × ((j : κ) → Y j)),
    Tendsto (ofNNReal ∘ fun x ↦ (∏ c, (⋯.apprSeq x) (p.1 c)) * ∏ c, (⋯.apprSeq x) (p.2 c)) atTop
      (𝓝 ↑((∏ c, (s c).indicator (fun x ↦ 1) (p.1 c)) * ∏ c, (t c).indicator (fun x ↦ 1) (p.2 c)))
hp1 : ∀ (x : (i : ι) → X i), ∏ i, (s i).indicator (fun x ↦ 1) (x i) = (univ.pi s).indicator 1 x
y : (j : κ) → Y j
⊢ ∏ j, (t j).indicator (fun x ↦ 1) (y j) = (univ.pi t).indicator 1 y

Tactic:
by

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

Goal state before:
pp: E : Type u_1
inst✝³ : MeasurableSpace E
inst✝² : TopologicalSpace E
inst✝¹ : T2Space E
inst✝ : BorelSpace E
u : ℕ → ℝ≥0
K : ℕ → Set E
C : ℝ≥0
hu : Tendsto u atTop (𝓝 0)
hK : ∀ (n : ℕ), IsCompact (K n)
h : NormalSpace E ∨ Monotone K
I :
  ∀ (μ : FiniteMeasure E) (n : ℕ),
    ∑ i ∈ Finset.range (n + 1), μ.restrict (disjointed K i) = μ.restrict ((partialSups K) n)
A : ∀ (n : ℕ), IsCompact ((partialSups K) n)
f : Ultrafilter (FiniteMeasure E)
hf : {μ | μ.mass ≤ C ∧ ∀ (n : ℕ), μ (K n)ᶜ ≤ u n} ∈ f
ν : ℕ → FiniteMeasure E
ν_reg : ∀ (n : ℕ), (↑(ν n)).InnerRegular
νK : ∀ (n : ℕ), (ν n) ((partialSups K) n)ᶜ = 0
hν : ∀ (n : ℕ), Tendsto (fun ρ ↦ ρ.restrict (disjointed K n)) (↑f) (𝓝 (ν n))
this✝ : Tendsto (fun n ↦ ∑ i ∈ Finset.range (n + 1), ↑(ν i) univ) atTop (𝓝 (∑' (i : ℕ), ↑(ν i) univ))
n : ℕ
this : ∑ i ∈ Finset.range (n + 1), ↑(ν i) univ = ↑(∑ i ∈ Finset.range (n + 1), ν i) univ
⊢ Tendsto (fun μ ↦ (∑ i ∈ Finset.range (n + 1), μ.restrict (disjointed K i)).mass) (↑f)
    (𝓝 (∑ i ∈ Finset.range (n + 1), ν i).mass)

Tactic:
by

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

Goal state before:
pp: E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace ℝ F
a b c d : E
γ₁ : Path a b
γ₂ : Path c d
s : Set (↑I × ↑I)
t : Set E
ω : E → E →L[ℝ] F
dω : E → E →L[ℝ] E →L[ℝ] F
φ : (↑γ₁).Homotopy ↑γ₂
hs : s.Countable
hφt : ∀ a_1 ∈ Ioo 0 1, ∀ b_1 ∈ Ioo 0 1, φ (a_1, b_1) ∈ t
hω : ∀ a_1 ∈ Ioo 0 1, ∀ b_1 ∈ Ioo 0 1, (a_1, b_1) ∉ s → HasFDerivWithinAt ω (dω (φ (a_1, b_1))) t (φ (a_1, b_1))
hωc : ContinuousOn ω (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t)
hdω_symm :
  ∀ a_1 ∈ Ioo 0 1,
    ∀ b_1 ∈ Ioo 0 1,
      (a_1, b_1) ∉ s →
        ∀ u ∈ tangentConeAt ℝ t (φ (a_1, b_1)),
          ∀ v ∈ tangentConeAt ℝ t (φ (a_1, b_1)), ((dω (φ (a_1, b_1))) u) v = ((dω (φ (a_1, b_1))) v) u
U : Set (ℝ × ℝ) := Ioo 0 1 ×ˢ Ioo 0 1
hU : U = Ioo 0 1 ×ˢ Ioo 0 1
hinterior : interior (Icc 0 1) = U
hunique : UniqueDiffOn ℝ (Icc 0 1)
hUopen : IsOpen U
hU_subset : U ⊆ Icc 0 1
hclosure : closure U = Icc 0 1
ψ : ℝ × ℝ → E := fun xy ↦ Set.IccExtend ⋯ (⇑(φ.extend xy.1)) xy.2
hcontdiff : ContDiffOn ℝ 2 ψ (Icc 0 1)
hψ : ψ = fun xy ↦ Set.IccExtend ⋯ (⇑(φ.extend xy.1)) xy.2
hψφ : ∀ (a_1 b_1 : ↑I), ψ (↑a_1, ↑b_1) = φ (a_1, b_1)
hψ_cont : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ψ
hψUt : MapsTo ψ U t
dψ : ℝ × ℝ → ℝ × ℝ →L[ℝ] E := fderivWithin ℝ ψ (Icc 0 1)
s' : Set (ℝ × ℝ) := Prod.map Subtype.val Subtype.val '' s
hs' : s' = Prod.map Subtype.val Subtype.val '' s
hmem_s' : ∀ (x y : ↑I), (↑x, ↑y) ∈ s' ↔ (x, y) ∈ s
hs'c : s'.Countable
hdψ : ∀ a ∈ U, HasFDerivAt ψ (dψ a) a
d2ψ : ℝ × ℝ → ℝ × ℝ →L[ℝ] ℝ × ℝ →L[ℝ] E := fderivWithin ℝ dψ (Icc 0 1)
hd2ψ : ∀ a ∈ U, HasFDerivAt dψ (d2ψ a) a
hd2ψ_symm : ∀ a ∈ Icc 0 1, ∀ (x y : ℝ × ℝ), ((d2ψ a) x) y = ((d2ψ a) y) x
η : ℝ × ℝ → ℝ × ℝ →L[ℝ] F := fun a ↦ ω (ψ a) ∘SL dψ a
f : ℝ × ℝ → F := fun a ↦ (η a) (0, 1)
hf : ∀ a ∈ Icc 0 1, f a = (ω (ψ a)) (derivWithin (ψ ∘ fun x ↦ (a.1, x)) I a.2)
g : ℝ × ℝ → F := fun a ↦ -(η a) (1, 0)
hg : ∀ a ∈ Icc 0 1, g a = (ω (ψ a)) (-derivWithin (ψ ∘ fun x ↦ (x, a.2)) I a.1)
dη : ℝ × ℝ → ℝ × ℝ →L[ℝ] ℝ × ℝ →L[ℝ] F :=
  fun a ↦ (ContinuousLinearMap.compL ℝ (ℝ × ℝ) E F) (ω (ψ a)) ∘SL d2ψ a + (dω (ψ a)).bilinearComp (dψ a) (dψ a)
hdη : ∀ a ∈ U \ s', HasFDerivAt η (dη a) a
hdη_symm : ∀ a ∈ U \ s', ∀ (u v : ℝ × ℝ), ((dη a) u) v = ((dη a) v) u
f' : ℝ × ℝ → ℝ × ℝ →L[ℝ] F := fun a ↦ (ContinuousLinearMap.apply ℝ F) (0, 1) ∘SL dη a
hf' : ∀ a ∈ U \ s', HasFDerivAt f (f' a) a
g' : ℝ × ℝ → ℝ × ℝ →L[ℝ] F := fun a ↦ -(ContinuousLinearMap.apply ℝ F) (1, 0) ∘SL dη a
hg' : ∀ a ∈ U \ s', HasFDerivAt g (g' a) a
hf'g' : (fun a ↦ (f' a) (1, 0) + (g' a) (0, 1)) =ᵐ[volume.restrict (Icc 0 1)] 0
this : ∫ (a : ℝ × ℝ) in Icc 0 1, (f' a) (1, 0) + (g' a) (0, 1) = 0
⊢ (((∫ (x : ℝ) in 0..1, g (x, 1)) - ∫ (x : ℝ) in 0..1, g (x, 0)) + ∫ (y : ℝ) in 0..1, f (1, y)) -
      ∫ (y : ℝ) in 0..1, f (0, y) =
    0

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls

Goal state before:
pp: case e'_3.e'_6
ι : Type u_1
inst✝ : Fintype ι
p : ℝ
hp : 1 ≤ p
h₁ : 0 < p
this✝ : (ENNReal.ofReal p).toReal = p
h₂ : ∀ (x : ι → ℂ), 0 ≤ ∑ i, ‖x i‖ ^ p
eq_norm : ∀ (x : ι → ℂ), ‖toLp (ENNReal.ofReal p) x‖ = (∑ i, ‖x i‖ ^ p) ^ (1 / p)
this : Fact (1 ≤ ENNReal.ofReal p)
eq_zero : ∀ (x : ι → ℂ), (∑ i, ‖x i‖ ^ p) ^ (1 / p) = 0 ↔ x = 0
nm_zero : (∑ i, ‖0 i‖ ^ p) ^ (1 / p) = 0
nm_neg : ∀ (x : ι → ℂ), (∑ i, ‖(-x) i‖ ^ p) ^ (1 / p) = (∑ i, ‖x i‖ ^ p) ^ (1 / p)
nm_add : ∀ (x y : ι → ℂ), (∑ i, ‖(x + y) i‖ ^ p) ^ (1 / p) ≤ (∑ i, ‖x i‖ ^ p) ^ (1 / p) + (∑ i, ‖y i‖ ^ p) ^ (1 / p)
nm_smul : ∀ (r : ℝ) (x : ι → ℂ), (∑ i, ‖(r • x) i‖ ^ p) ^ (1 / p) ≤ ‖r‖ * (∑ i, ‖x i‖ ^ p) ^ (1 / p)
⊢ 2 * ↑(card ι) / p + 1 = ↑(finrank ℝ (ι → ℂ)) / p + 1

Tactic:
· rw [finrank_pi_fintype, Complex.finrank_real_complex, Finset.sum_const, smul_eq_mul,
      Nat.cast_mul, Nat.cast_ofNat, Fintype.card, mul_comm]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls

Goal state before:
pp: ι : Type u_1
inst✝ : Fintype ι
p : ℝ
hp : 1 ≤ p
⊢ volume {x | ∑ i, ‖x i‖ ^ p < 1} =
    ENNReal.ofReal ((π * Real.Gamma (2 / p + 1)) ^ card ι / Real.Gamma (2 * ↑(card ι) / p + 1))

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls

Goal state before:
pp: ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : Nonempty ι
p : ℝ
hp : 1 ≤ p
r : ℝ
x : ι → ℂ
⊢ 0 ≤ ∑ i, ‖x i‖ ^ p

Tactic:
by

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

Goal state before:
pp: E : Type u_1
inst✝³ : MeasurableSpace E
inst✝² : TopologicalSpace E
inst✝¹ : T2Space E
inst✝ : BorelSpace E
u : ℕ → ℝ≥0
K : ℕ → Set E
C : ℝ≥0
hu : Tendsto u atTop (𝓝 0)
hK : ∀ (n : ℕ), IsCompact (K n)
h : NormalSpace E ∨ Monotone K
I :
  ∀ (μ : FiniteMeasure E) (n : ℕ),
    ∑ i ∈ Finset.range (n + 1), μ.restrict (disjointed K i) = μ.restrict ((partialSups K) n)
A : ∀ (n : ℕ), IsCompact ((partialSups K) n)
f : Ultrafilter (FiniteMeasure E)
hf : {μ | μ.mass ≤ C ∧ ∀ (n : ℕ), μ (K n)ᶜ ≤ u n} ∈ f
ν : ℕ → FiniteMeasure E
ν_reg : ∀ (n : ℕ), (↑(ν n)).InnerRegular
νK : ∀ (n : ℕ), (ν n) ((partialSups K) n)ᶜ = 0
hν : ∀ (n : ℕ), Tendsto (fun ρ ↦ ρ.restrict (disjointed K n)) (↑f) (𝓝 (ν n))
⊢ (Measure.sum fun n ↦ ↑(ν n)) univ ≤ ↑C

Tactic:
by

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

Goal state before:
pp: E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace ℝ F
a b c d : E
γ₁ : Path a b
γ₂ : Path c d
s : Set (↑I × ↑I)
t : Set E
ω : E → E →L[ℝ] F
dω : E → E →L[ℝ] E →L[ℝ] F
φ : (↑γ₁).Homotopy ↑γ₂
hs : s.Countable
hφt : ∀ a_1 ∈ Ioo 0 1, ∀ b_1 ∈ Ioo 0 1, φ (a_1, b_1) ∈ t
hω : ∀ a_1 ∈ Ioo 0 1, ∀ b_1 ∈ Ioo 0 1, (a_1, b_1) ∉ s → HasFDerivWithinAt ω (dω (φ (a_1, b_1))) t (φ (a_1, b_1))
hωc : ContinuousOn ω (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t)
hdω_symm :
  ∀ a_1 ∈ Ioo 0 1,
    ∀ b_1 ∈ Ioo 0 1,
      (a_1, b_1) ∉ s →
        ∀ u ∈ tangentConeAt ℝ t (φ (a_1, b_1)),
          ∀ v ∈ tangentConeAt ℝ t (φ (a_1, b_1)), ((dω (φ (a_1, b_1))) u) v = ((dω (φ (a_1, b_1))) v) u
hcontdiff : ContDiffOn ℝ 2 (fun xy ↦ Set.IccExtend ⋯ (⇑(φ.extend xy.1)) xy.2) (Icc 0 1)
⊢ ∫ᶜ (x : E) in γ₁, ω x + ∫ᶜ (x : E) in φ.evalAt 1, ω x = ∫ᶜ (x : E) in γ₂, ω x + ∫ᶜ (x : E) in φ.evalAt 0, ω x

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls

Goal state before:
pp: ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : Nonempty ι
p : ℝ
hp : 1 ≤ p
r : ℝ
h₁ : ∀ (x : ι → ℂ), 0 ≤ ∑ i, ‖x i‖ ^ p
h₂ : ∀ (x : ι → ℂ), 0 ≤ (∑ i, ‖x i‖ ^ p) ^ (1 / p)
hr : r ≤ 0
⊢ {x | (∑ i, ‖x i‖ ^ p) ^ (1 / p) < r} = ∅

Tactic:
by

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

Goal state before:
pp: E : Type u_1
inst✝³ : MeasurableSpace E
inst✝² : TopologicalSpace E
inst✝¹ : T2Space E
inst✝ : BorelSpace E
u : ℕ → ℝ≥0
K : ℕ → Set E
C : ℝ≥0
hu : Tendsto u atTop (𝓝 0)
hK : ∀ (n : ℕ), IsCompact (K n)
h : NormalSpace E ∨ Monotone K
I :
  ∀ (μ : FiniteMeasure E) (n : ℕ),
    ∑ i ∈ Finset.range (n + 1), μ.restrict (disjointed K i) = μ.restrict ((partialSups K) n)
A : ∀ (n : ℕ), IsCompact ((partialSups K) n)
f : Ultrafilter (FiniteMeasure E)
hf : {μ | μ.mass ≤ C ∧ ∀ (n : ℕ), μ (K n)ᶜ ≤ u n} ∈ f
ν : ℕ → FiniteMeasure E
ν_reg : ∀ (n : ℕ), (↑(ν n)).InnerRegular
νK : ∀ (n : ℕ), (ν n) ((partialSups K) n)ᶜ = 0
hν : ∀ (n : ℕ), Tendsto (fun ρ ↦ ρ.restrict (disjointed K n)) (↑f) (𝓝 (ν n))
B : (Measure.sum fun n ↦ ↑(ν n)) univ ≤ ↑C
⊢ ↑C < ∞

Tactic:
by

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✝² : Fintype ι
inst✝¹ : Fintype κ
μ ν : Measure (((i : ι) → X i) × ((j : κ) → Y j))
inst✝ : IsFiniteMeasure μ
h :
  ∀ (f : (i : ι) → X i →ᵇ ℝ≥0) (g : (j : κ) → Y j →ᵇ ℝ≥0),
    ∫⁻ (p : ((i : ι) → X i) × ((j : κ) → Y j)), ↑(∏ i, (f i) (p.1 i)) * ↑(∏ j, (g j) (p.2 j)) ∂μ =
      ∫⁻ (p : ((i : ι) → X i) × ((j : κ) → Y j)), ↑(∏ i, (f i) (p.1 i)) * ↑(∏ j, (g j) (p.2 j)) ∂ν
hμν : μ univ = ν univ
this✝ : IsFiniteMeasure ν
π : Set (Set (((i : ι) → X i) × ((j : κ) → Y j))) :=
  image2 (fun s t ↦ s ×ˢ t) (univ.pi '' univ.pi fun x ↦ {s | IsClosed[inst✝⁸ x] s})
    (univ.pi '' univ.pi fun x ↦ {t | IsClosed[inst✝⁵ x] t})
hπ1 : IsPiSystem π
hπ2 : Prod.instMeasurableSpace = generateFrom π
s : (i : ι) → Set (X i)
t : (i : κ) → Set (Y i)
hs : ∀ (i : ι), IsClosed[inst✝⁸ i] (s i)
ht : ∀ (i : κ), IsClosed[inst✝⁵ i] (t i)
hp1 : ∀ (x : (i : ι) → X i), ∏ i, (s i).indicator (fun x ↦ 1) (x i) = (univ.pi s).indicator 1 x
hp2 : ∀ (y : (j : κ) → Y j), ∏ j, (t j).indicator (fun x ↦ 1) (y j) = (univ.pi t).indicator 1 y
this :
  ∀ (p : ((i : ι) → X i) × ((j : κ) → Y j)),
    Tendsto (ofNNReal ∘ fun x ↦ (∏ c, (⋯.apprSeq x) (p.1 c)) * ∏ c, (⋯.apprSeq x) (p.2 c)) atTop
      (𝓝 ↑((univ.pi s ×ˢ univ.pi t).indicator 1 p))
⊢ ∀ (x : ℕ), Measurable fun p ↦ ↑((∏ i, (⋯.apprSeq x) (p.1 i)) * ∏ j, (⋯.apprSeq x) (p.2 j))

Tactic:
by

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

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
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace ℝ F
a b c d : E
γ₁ : Path a b
γ₂ : Path c d
s : Set (↑I × ↑I)
t : Set E
ω : E → E →L[𝕜] F
dω : E → E →L[ℝ] E →L[𝕜] F
φ : (↑γ₁).Homotopy ↑γ₂
hs : s.Countable
hφt : ∀ a_1 ∈ Ioo 0 1, ∀ b_1 ∈ Ioo 0 1, φ (a_1, b_1) ∈ t
hω : ∀ a_1 ∈ Ioo 0 1, ∀ b_1 ∈ Ioo 0 1, (a_1, b_1) ∉ s → HasFDerivWithinAt ω (dω (φ (a_1, b_1))) t (φ (a_1, b_1))
hωc : ContinuousOn ω (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t)
hdω_symm :
  ∀ a_1 ∈ Ioo 0 1,
    ∀ b_1 ∈ Ioo 0 1,
      (a_1, b_1) ∉ s →
        ∀ u ∈ tangentConeAt ℝ t (φ (a_1, b_1)),
          ∀ v ∈ tangentConeAt ℝ t (φ (a_1, b_1)), ((dω (φ (a_1, b_1))) u) v = ((dω (φ (a_1, b_1))) v) u
hcontdiff : ContDiffOn ℝ 2 (fun xy ↦ Set.IccExtend ⋯ (⇑(φ.extend xy.1)) xy.2) (Icc 0 1)
⊢ ∫ᶜ (x : E) in γ₁, ω x + ∫ᶜ (x : E) in φ.evalAt 1, ω x = ∫ᶜ (x : E) in γ₂, ω x + ∫ᶜ (x : E) in φ.evalAt 0, ω x

Tactic:
by

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✝² : Fintype ι
inst✝¹ : Fintype κ
μ ν : Measure (((i : ι) → X i) × ((j : κ) → Y j))
inst✝ : IsFiniteMeasure μ
h :
  ∀ (f : (i : ι) → X i →ᵇ ℝ≥0) (g : (j : κ) → Y j →ᵇ ℝ≥0),
    ∫⁻ (p : ((i : ι) → X i) × ((j : κ) → Y j)), ↑(∏ i, (f i) (p.1 i)) * ↑(∏ j, (g j) (p.2 j)) ∂μ =
      ∫⁻ (p : ((i : ι) → X i) × ((j : κ) → Y j)), ↑(∏ i, (f i) (p.1 i)) * ↑(∏ j, (g j) (p.2 j)) ∂ν
hμν : μ univ = ν univ
this✝ : IsFiniteMeasure ν
π : Set (Set (((i : ι) → X i) × ((j : κ) → Y j))) :=
  image2 (fun s t ↦ s ×ˢ t) (univ.pi '' univ.pi fun x ↦ {s | IsClosed[inst✝⁸ x] s})
    (univ.pi '' univ.pi fun x ↦ {t | IsClosed[inst✝⁵ x] t})
hπ1 : IsPiSystem π
hπ2 : Prod.instMeasurableSpace = generateFrom π
s : (i : ι) → Set (X i)
t : (i : κ) → Set (Y i)
hs : ∀ (i : ι), IsClosed[inst✝⁸ i] (s i)
ht : ∀ (i : κ), IsClosed[inst✝⁵ i] (t i)
hp1 : ∀ (x : (i : ι) → X i), ∏ i, (s i).indicator (fun x ↦ 1) (x i) = (univ.pi s).indicator 1 x
hp2 : ∀ (y : (j : κ) → Y j), ∏ j, (t j).indicator (fun x ↦ 1) (y j) = (univ.pi t).indicator 1 y
this :
  ∀ (p : ((i : ι) → X i) × ((j : κ) → Y j)),
    Tendsto (ofNNReal ∘ fun x ↦ (∏ c, (⋯.apprSeq x) (p.1 c)) * ∏ c, (⋯.apprSeq x) (p.2 c)) atTop
      (𝓝 ↑((univ.pi s ×ˢ univ.pi t).indicator 1 p))
⊢ ∫⁻ (a : ((i : ι) → X i) × ((j : κ) → Y j)), 1 a ∂μ ≠ ∞

Tactic:
by

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

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
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace ℝ F
a b c d : E
γ₁ : Path a b
γ₂ : Path c d
t : Set E
ω : E → E →L[𝕜] F
dω : E → E →L[ℝ] E →L[𝕜] F
φ : (↑γ₁).Homotopy ↑γ₂
hφt : ∀ a_1 ∈ Ioo 0 1, ∀ b_1 ∈ Ioo 0 1, φ (a_1, b_1) ∈ t
hω : ∀ x ∈ t, HasFDerivWithinAt ω (dω x) t x
hωc : ContinuousOn ω (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t)
hdω_symm : ∀ x ∈ t, ∀ u ∈ tangentConeAt ℝ t x, ∀ v ∈ tangentConeAt ℝ t x, ((dω x) u) v = ((dω x) v) u
hcontdiff : ContDiffOn ℝ 2 (fun xy ↦ Set.IccExtend ⋯ (⇑(φ.extend xy.1)) xy.2) (Icc 0 1)
⊢ ∅.Countable

Tactic:
by

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

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
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace ℝ F
a b c : E
s : Set E
ω : E → E →L[𝕜] F
dω : E → E →L[ℝ] E →L[𝕜] F
hs : Convex ℝ s
hω : ∀ x ∈ s, HasFDerivWithinAt ω (dω x) s x
hdω : ∀ a ∈ s, ∀ x ∈ tangentConeAt ℝ s a, ∀ y ∈ tangentConeAt ℝ s a, ((dω a) x) y = ((dω a) y) x
ha : a ∈ s
hb : b ∈ s
hc : c ∈ s
φ : (↑(Path.segment a b)).Homotopy ↑(Path.segment a c) :=
  ContinuousMap.Homotopy.affine ↑(Path.segment a b) ↑(Path.segment a c)
⊢ range ⇑φ ⊆ s

Tactic:
by

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✝² : Fintype ι
inst✝¹ : Fintype κ
μ ν : Measure (((i : ι) → X i) × ((j : κ) → Y j))
inst✝ : IsFiniteMeasure μ
h :
  ∀ (f : (i : ι) → X i →ᵇ ℝ≥0) (g : (j : κ) → Y j →ᵇ ℝ≥0),
    ∫⁻ (p : ((i : ι) → X i) × ((j : κ) → Y j)), ↑(∏ i, (f i) (p.1 i)) * ↑(∏ j, (g j) (p.2 j)) ∂μ =
      ∫⁻ (p : ((i : ι) → X i) × ((j : κ) → Y j)), ↑(∏ i, (f i) (p.1 i)) * ↑(∏ j, (g j) (p.2 j)) ∂ν
hμν : μ univ = ν univ
this✝ : IsFiniteMeasure ν
π : Set (Set (((i : ι) → X i) × ((j : κ) → Y j))) :=
  image2 (fun s t ↦ s ×ˢ t) (univ.pi '' univ.pi fun x ↦ {s | IsClosed[inst✝⁸ x] s})
    (univ.pi '' univ.pi fun x ↦ {t | IsClosed[inst✝⁵ x] t})
hπ1 : IsPiSystem π
hπ2 : Prod.instMeasurableSpace = generateFrom π
s : (i : ι) → Set (X i)
t : (i : κ) → Set (Y i)
hs : ∀ (i : ι), IsClosed[inst✝⁸ i] (s i)
ht : ∀ (i : κ), IsClosed[inst✝⁵ i] (t i)
hp1 : ∀ (x : (i : ι) → X i), ∏ i, (s i).indicator (fun x ↦ 1) (x i) = (univ.pi s).indicator 1 x
hp2 : ∀ (y : (j : κ) → Y j), ∏ j, (t j).indicator (fun x ↦ 1) (y j) = (univ.pi t).indicator 1 y
this :
  ∀ (p : ((i : ι) → X i) × ((j : κ) → Y j)),
    Tendsto (ofNNReal ∘ fun x ↦ (∏ c, (⋯.apprSeq x) (p.1 c)) * ∏ c, (⋯.apprSeq x) (p.2 c)) atTop
      (𝓝 ↑((univ.pi s ×ˢ univ.pi t).indicator 1 p))
n : ℕ
ω : ((i : ι) → X i) × ((j : κ) → Y j)
⊢ ∀ i ∈ Finset.univ, 0 ≤ (⋯.apprSeq n) (ω.1 i)

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls

Goal state before:
pp: ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : Nonempty ι
p : ℝ
hp : 1 ≤ p
r : ℝ
h₁ : ∀ (x : ι → ℂ), 0 ≤ ∑ i, ‖x i‖ ^ p
h₂ : ∀ (x : ι → ℂ), 0 ≤ (∑ i, ‖x i‖ ^ p) ^ (1 / p)
hr : 0 < r
⊢ 0 < p

Tactic:
by

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✝² : Fintype ι
inst✝¹ : Fintype κ
μ ν : Measure (((i : ι) → X i) × ((j : κ) → Y j))
inst✝ : IsFiniteMeasure μ
h :
  ∀ (f : (i : ι) → X i →ᵇ ℝ≥0) (g : (j : κ) → Y j →ᵇ ℝ≥0),
    ∫⁻ (p : ((i : ι) → X i) × ((j : κ) → Y j)), ↑(∏ i, (f i) (p.1 i)) * ↑(∏ j, (g j) (p.2 j)) ∂μ =
      ∫⁻ (p : ((i : ι) → X i) × ((j : κ) → Y j)), ↑(∏ i, (f i) (p.1 i)) * ↑(∏ j, (g j) (p.2 j)) ∂ν
hμν : μ univ = ν univ
this✝ : IsFiniteMeasure ν
π : Set (Set (((i : ι) → X i) × ((j : κ) → Y j))) :=
  image2 (fun s t ↦ s ×ˢ t) (univ.pi '' univ.pi fun x ↦ {s | IsClosed[inst✝⁸ x] s})
    (univ.pi '' univ.pi fun x ↦ {t | IsClosed[inst✝⁵ x] t})
hπ1 : IsPiSystem π
hπ2 : Prod.instMeasurableSpace = generateFrom π
s : (i : ι) → Set (X i)
t : (i : κ) → Set (Y i)
hs : ∀ (i : ι), IsClosed[inst✝⁸ i] (s i)
ht : ∀ (i : κ), IsClosed[inst✝⁵ i] (t i)
hp1 : ∀ (x : (i : ι) → X i), ∏ i, (s i).indicator (fun x ↦ 1) (x i) = (univ.pi s).indicator 1 x
hp2 : ∀ (y : (j : κ) → Y j), ∏ j, (t j).indicator (fun x ↦ 1) (y j) = (univ.pi t).indicator 1 y
this :
  ∀ (p : ((i : ι) → X i) × ((j : κ) → Y j)),
    Tendsto (ofNNReal ∘ fun x ↦ (∏ c, (⋯.apprSeq x) (p.1 c)) * ∏ c, (⋯.apprSeq x) (p.2 c)) atTop
      (𝓝 ↑((univ.pi s ×ˢ univ.pi t).indicator 1 p))
n : ℕ
ω : ((i : ι) → X i) × ((j : κ) → Y j)
⊢ ∀ i ∈ Finset.univ, 0 ≤ (⋯.apprSeq n) (ω.2 i)

Tactic:
by

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

Goal state before:
pp: E : Type u_1
inst✝³ : MeasurableSpace E
inst✝² : TopologicalSpace E
inst✝¹ : T2Space E
inst✝ : BorelSpace E
u : ℕ → ℝ≥0
K : ℕ → Set E
C : ℝ≥0
hu : Tendsto u atTop (𝓝 0)
hK : ∀ (n : ℕ), IsCompact (K n)
h : NormalSpace E ∨ Monotone K
I :
  ∀ (μ : FiniteMeasure E) (n : ℕ),
    ∑ i ∈ Finset.range (n + 1), μ.restrict (disjointed K i) = μ.restrict ((partialSups K) n)
A : ∀ (n : ℕ), IsCompact ((partialSups K) n)
f : Ultrafilter (FiniteMeasure E)
hf : {μ | μ.mass ≤ C ∧ ∀ (n : ℕ), μ (K n)ᶜ ≤ u n} ∈ f
ν : ℕ → FiniteMeasure E
ν_reg : ∀ (n : ℕ), (↑(ν n)).InnerRegular
νK : ∀ (n : ℕ), (ν n) ((partialSups K) n)ᶜ = 0
hν : ∀ (n : ℕ), Tendsto (fun ρ ↦ ρ.restrict (disjointed K n)) (↑f) (𝓝 (ν n))
B : (Measure.sum fun n ↦ ↑(ν n)) univ ≤ ↑C
μ : FiniteMeasure E := ⟨Measure.sum fun n ↦ ↑(ν n), ⋯⟩
g : E →ᵇ ℝ
ε : ℝ
εpos : ε > 0
⊢ Tendsto (fun n ↦ ∫ (x : E), g x ∂∑ i ∈ Finset.range n, ↑(ν i)) atTop (𝓝 (∫ (x : E), g x ∂↑μ))

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls

Goal state before:
pp: ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : Nonempty ι
p : ℝ
hp : 1 ≤ p
r : ℝ
⊢ volume {x | (∑ i, ‖x i‖ ^ p) ^ (1 / p) < r} =
    ENNReal.ofReal r ^ (2 * card ι) *
      ENNReal.ofReal ((π * Real.Gamma (2 / p + 1)) ^ card ι / Real.Gamma (2 * ↑(card ι) / p + 1))

Tactic:
by

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

Goal state before:
pp: E : Type u_1
inst✝³ : MeasurableSpace E
inst✝² : TopologicalSpace E
inst✝¹ : T2Space E
inst✝ : BorelSpace E
u : ℕ → ℝ≥0
K : ℕ → Set E
C : ℝ≥0
hu : Tendsto u atTop (𝓝 0)
hK : ∀ (n : ℕ), IsCompact (K n)
h : NormalSpace E ∨ Monotone K
I :
  ∀ (μ : FiniteMeasure E) (n : ℕ),
    ∑ i ∈ Finset.range (n + 1), μ.restrict (disjointed K i) = μ.restrict ((partialSups K) n)
A : ∀ (n : ℕ), IsCompact ((partialSups K) n)
f : Ultrafilter (FiniteMeasure E)
hf : {μ | μ.mass ≤ C ∧ ∀ (n : ℕ), μ (K n)ᶜ ≤ u n} ∈ f
ν : ℕ → FiniteMeasure E
ν_reg : ∀ (n : ℕ), (↑(ν n)).InnerRegular
νK : ∀ (n : ℕ), (ν n) ((partialSups K) n)ᶜ = 0
hν : ∀ (n : ℕ), Tendsto (fun ρ ↦ ρ.restrict (disjointed K n)) (↑f) (𝓝 (ν n))
B : (Measure.sum fun n ↦ ↑(ν n)) univ ≤ ↑C
μ : FiniteMeasure E := ⟨Measure.sum fun n ↦ ↑(ν n), ⋯⟩
g : E →ᵇ ℝ
ε : ℝ
εpos : ε > 0
this : Tendsto (fun n ↦ ∫ (x : E), g x ∂∑ i ∈ Finset.range n, ↑(ν i)) atTop (𝓝 (∫ (x : E), g x ∂↑μ))
⊢ ε / 3 > 0

Tactic:
by

Goal state after: