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

Goal state before:
pp: case h'
α : Type u_1
inst✝⁹ : MeasurableSpace α
β : Type u_2
inst✝⁸ : MeasurableSpace β
inst✝⁷ : TopologicalSpace α
inst✝⁶ : TopologicalSpace β
inst✝⁵ : SecondCountableTopology α
inst✝⁴ : SecondCountableTopology β
inst✝³ : PseudoMetrizableSpace α
inst✝² : PseudoMetrizableSpace β
inst✝¹ : OpensMeasurableSpace α
inst✝ : OpensMeasurableSpace β
μ : ProbabilityMeasure α × ProbabilityMeasure β
S : Set (Set (α × β)) :=
  {t | ∃ a b, MeasurableSet a ∧ μ.1 (frontier a) = 0 ∧ MeasurableSet b ∧ μ.2 (frontier b) = 0 ∧ t = a ×ˢ b}
this : IsPiSystem S
a : Set α
b : Set β
ameas : MeasurableSet a
ha : μ.1 (frontier a) = 0
bmeas : MeasurableSet b
hb : μ.2 (frontier b) = 0
⊢ Tendsto (fun i ↦ (i.1.prod i.2) (a ×ˢ b)) (𝓝 μ) (𝓝 (((fun μ ↦ μ.1.prod μ.2) μ) (a ×ˢ b)))

Tactic:
simp only [prod_prod]

Goal state after:
case h'
α : Type u_1
inst✝⁹ : MeasurableSpace α
β : Type u_2
inst✝⁸ : MeasurableSpace β
inst✝⁷ : TopologicalSpace α
inst✝⁶ : TopologicalSpace β
inst✝⁵ : SecondCountableTopology α
inst✝⁴ : SecondCountableTopology β
inst✝³ : PseudoMetrizableSpace α
inst✝² : PseudoMetrizableSpace β
inst✝¹ : OpensMeasurableSpace α
inst✝ : OpensMeasurableSpace β
μ : ProbabilityMeasure α × ProbabilityMeasure β
S : Set (Set (α × β)) :=
  {t | ∃ a b, MeasurableSet a ∧ μ.1 (frontier a) = 0 ∧ MeasurableSet b ∧ μ.2 (frontier b) = 0 ∧ t = a ×ˢ b}
this : IsPiSystem S
a : Set α
b : Set β
ameas : MeasurableSet a
ha : μ.1 (frontier a) = 0
bmeas : MeasurableSet b
hb : μ.2 (frontier b) = 0
⊢ Tendsto (fun i ↦ i.1 a * i.2 b) (𝓝 μ) (𝓝 (μ.1 a * μ.2 b))
Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric

Goal state before:
pp: case refine_4
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : PseudoMetricSpace Ω
inst✝ : OpensMeasurableSpace Ω
μs : ℕ → LevyProkhorov (ProbabilityMeasure Ω)
ν : LevyProkhorov (ProbabilityMeasure Ω)
hμs : Tendsto μs atTop (𝓝 ν)
P : ProbabilityMeasure Ω := ν.toMeasure
Ps : ℕ → ProbabilityMeasure Ω := toMeasure ∘ μs
f✝ f : Ω →ᵇ ℝ
f_nn : 0 ≤ f
f_zero : ¬‖f‖ = 0
norm_f_pos : 0 < ‖f‖
δ : ℝ
δ_pos : 0 < δ
εs : ℕ → ℝ
left✝ : StrictAnti εs
εs_lim : Tendsto εs atTop (𝓝 0)
ε_of_room : Tendsto (fun x ↦ dist (μs x) ν + εs x) atTop (𝓝 0)
ε_of_room' : Tendsto (fun n ↦ dist (μs n) ν + εs n) atTop (𝓝[>] 0)
key :
  Tendsto (fun x ↦ ∫ (t : ℝ) in Ioc 0 ‖f‖, (↑P).real (thickening (dist (μs x) ν + εs x) {a | t ≤ f a})) atTop
    (𝓝 (∫ (t : ℝ) in Ioc 0 ‖f‖, (↑P).real {a | t ≤ f a}))
aux : ∀ (z : ℝ), Iio (z + δ / 2) ∈ 𝓝 z
n : ℕ
εs_pos : 0 < εs n
hn :
  ∫ (t : ℝ) in Ioc 0 ‖f‖, (↑P).real (thickening (dist (μs n) ν + εs n) {a | t ≤ f a}) <
    (∫ (t : ℝ) in Ioc 0 ‖f‖, (↑P).real {a | t ≤ f a}) + δ / 2
hn' : dist (μs n) ν + εs n < ‖f‖⁻¹ * δ / 2
bound :
  ∫ (ω : Ω), f ω ∂↑(Ps n) ≤
    (∫ (t : ℝ) in Ioc 0 ‖f‖, (↑P).real (thickening (dist (μs n) ν + εs n) {a | t ≤ f a})) + (dist (μs n) ν + εs n) * ‖f‖
⊢ (∫ (t : ℝ) in Ioc 0 ‖f‖, (↑P).real {a | t ≤ f a}) + δ / 2 + (dist (μs n) ν + εs n) * ‖f‖ ≤ ∫ (x : Ω), f x ∂↑P + δ

Tactic:
BoundedContinuousFunction.integral_eq_integral_meas_le _ _ <| .of_forall f_nn,

Goal state after:
case refine_4
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : PseudoMetricSpace Ω
inst✝ : OpensMeasurableSpace Ω
μs : ℕ → LevyProkhorov (ProbabilityMeasure Ω)
ν : LevyProkhorov (ProbabilityMeasure Ω)
hμs : Tendsto μs atTop (𝓝 ν)
P : ProbabilityMeasure Ω := ν.toMeasure
Ps : ℕ → ProbabilityMeasure Ω := toMeasure ∘ μs
f✝ f : Ω →ᵇ ℝ
f_nn : 0 ≤ f
f_zero : ¬‖f‖ = 0
norm_f_pos : 0 < ‖f‖
δ : ℝ
δ_pos : 0 < δ
εs : ℕ → ℝ
left✝ : StrictAnti εs
εs_lim : Tendsto εs atTop (𝓝 0)
ε_of_room : Tendsto (fun x ↦ dist (μs x) ν + εs x) atTop (𝓝 0)
ε_of_room' : Tendsto (fun n ↦ dist (μs n) ν + εs n) atTop (𝓝[>] 0)
key :
  Tendsto (fun x ↦ ∫ (t : ℝ) in Ioc 0 ‖f‖, (↑P).real (thickening (dist (μs x) ν + εs x) {a | t ≤ f a})) atTop
    (𝓝 (∫ (t : ℝ) in Ioc 0 ‖f‖, (↑P).real {a | t ≤ f a}))
aux : ∀ (z : ℝ), Iio (z + δ / 2) ∈ 𝓝 z
n : ℕ
εs_pos : 0 < εs n
hn :
  ∫ (t : ℝ) in Ioc 0 ‖f‖, (↑P).real (thickening (dist (μs n) ν + εs n) {a | t ≤ f a}) <
    (∫ (t : ℝ) in Ioc 0 ‖f‖, (↑P).real {a | t ≤ f a}) + δ / 2
hn' : dist (μs n) ν + εs n < ‖f‖⁻¹ * δ / 2
bound :
  ∫ (ω : Ω), f ω ∂↑(Ps n) ≤
    (∫ (t : ℝ) in Ioc 0 ‖f‖, (↑P).real (thickening (dist (μs n) ν + εs n) {a | t ≤ f a})) + (dist (μs n) ν + εs n) * ‖f‖
⊢ (∫ (t : ℝ) in Ioc 0 ‖f‖, (↑P).real {a | t ≤ f a}) + δ / 2 + (dist (μs n) ν + εs n) * ‖f‖ ≤
    (∫ (t : ℝ) in Ioc 0 ‖f‖, (↑P).real {a | t ≤ f a}) + δ
Module: Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar

Goal state before:
pp: G : Type u_1
inst✝⁷ : Group G
inst✝⁶ : TopologicalSpace G
inst✝⁵ : MeasurableSpace G
inst✝⁴ : BorelSpace G
inst✝³ : IsTopologicalGroup G
inst✝² : LocallyCompactSpace G
μ : Measure G
inst✝¹ : μ.IsHaarMeasure
inst✝ : μ.Regular
f : G → ℝ
φ : G ≃ₜ* G
e : G ≃ᵐ G := φ.toHomeomorph.toMeasurableEquiv
⊢ ∫ (a : G), f a ∂comap (⇑φ) μ = mulEquivHaarChar φ • ∫ (a : G), f a ∂μ

Tactic:
change ∫ a, f a ∂(comap e μ) = mulEquivHaarChar φ • ∫ a, f a ∂μ

Goal state after:
G : Type u_1
inst✝⁷ : Group G
inst✝⁶ : TopologicalSpace G
inst✝⁵ : MeasurableSpace G
inst✝⁴ : BorelSpace G
inst✝³ : IsTopologicalGroup G
inst✝² : LocallyCompactSpace G
μ : Measure G
inst✝¹ : μ.IsHaarMeasure
inst✝ : μ.Regular
f : G → ℝ
φ : G ≃ₜ* G
e : G ≃ᵐ G := φ.toHomeomorph.toMeasurableEquiv
⊢ ∫ (a : G), f a ∂comap (⇑e) μ = mulEquivHaarChar φ • ∫ (a : G), f a ∂μ
Module: Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar

Goal state before:
pp: G : Type u_1
inst✝⁶ : Group G
inst✝⁵ : TopologicalSpace G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
inst✝² : IsTopologicalGroup G
inst✝¹ : LocallyCompactSpace G
inst✝ : CompactSpace G
φ : G ≃ₜ* G
μ : Measure G := haarMeasure { carrier := univ, isCompact' := ⋯, interior_nonempty' := ⋯ }
hμ : μ univ = 1
| (μ.haarScalarFactor (map (⇑φ) μ) • map (⇑φ) μ) univ

Tactic:
Measure.smul_apply

Goal state after:
G : Type u_1
inst✝⁶ : Group G
inst✝⁵ : TopologicalSpace G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
inst✝² : IsTopologicalGroup G
inst✝¹ : LocallyCompactSpace G
inst✝ : CompactSpace G
φ : G ≃ₜ* G
μ : Measure G := haarMeasure { carrier := univ, isCompact' := ⋯, interior_nonempty' := ⋯ }
hμ : μ univ = 1
| μ.haarScalarFactor (map (⇑φ) μ) • (map (⇑φ) μ) univ
Module: Mathlib.MeasureTheory.Integral.CurveIntegral.Poincare

Goal state before:
pp: case s
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 (ℝ × ℝ) := ⋯
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 := ⋯
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 := ⋯
s' : Set (ℝ × ℝ) := ⋯
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 := ⋯
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 := ⋯
f : ℝ × ℝ → F := ⋯
hf : ∀ a ∈ Icc 0 1, f a = (ω (ψ a)) (derivWithin (ψ ∘ fun x ↦ (a.1, x)) I a.2)
g : ℝ × ℝ → F := ⋯
hg : ∀ a ∈ Icc 0 1, g a = (ω (ψ a)) (-derivWithin (ψ ∘ fun x ↦ (x, a.2)) I a.1)
dη : ℝ × ℝ → ℝ × ℝ →L[ℝ] ℝ × ℝ →L[ℝ] F := ⋯
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 := ⋯
hf' : ∀ a ∈ U \ s', HasFDerivAt f (f' a) a
g' : ℝ × ℝ → ℝ × ℝ →L[ℝ] F := ⋯
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
hηc : ContinuousOn η (Icc 0 1)
⊢ Set (ℝ × ℝ)

Tactic:
exact s'

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})
⊢ IsPiSystem π

Tactic:
rintro - ⟨-, ⟨s₁, hs₁, rfl⟩, -, ⟨t₁, ht₁, rfl⟩, rfl⟩ -
      ⟨-, ⟨s₂, hs₂, rfl⟩, -, ⟨t₂, ht₂, rfl⟩, rfl⟩ -

Goal state after:
ι : 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})
s₁ : (i : ι) → Set (X i)
hs₁ : s₁ ∈ univ.pi fun x ↦ {s | IsClosed[inst✝⁸ x] s}
t₁ : (i : κ) → Set (Y i)
ht₁ : t₁ ∈ univ.pi fun x ↦ {t | IsClosed[inst✝⁵ x] t}
s₂ : (i : ι) → Set (X i)
hs₂ : s₂ ∈ univ.pi fun x ↦ {s | IsClosed[inst✝⁸ x] s}
t₂ : (i : κ) → Set (Y i)
ht₂ : t₂ ∈ univ.pi fun x ↦ {t | IsClosed[inst✝⁵ x] t}
⊢ (fun s t ↦ s ×ˢ t) (univ.pi s₁) (univ.pi t₁) ∩ (fun s t ↦ s ×ˢ t) (univ.pi s₂) (univ.pi t₂) ∈ π
Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls

Goal state before:
pp: case e'_2
ι : 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)
x✝ : ι → ℝ
⊢ ∑ i, |x✝ i| ^ p < 1 ↔ (∑ i, |x✝ i| ^ p) ^ (1 / p) < 1

Tactic:
rw [rpow_lt_one_iff' _ (one_div_pos.mpr h₁)]

Goal state after:
ι : 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)
x✝ : ι → ℝ
⊢ 0 ≤ ∑ i, |x✝ i| ^ p
Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls

Goal state before:
pp: case e'_2
ι : 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)
x✝ : ι → ℂ
⊢ ∑ i, ‖x✝ i‖ ^ p < 1 ↔ (∑ i, ‖x✝ i‖ ^ p) ^ (1 / p) < 1

Tactic:
rw [rpow_lt_one_iff' _ (one_div_pos.mpr h₁)]

Goal state after:
ι : 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)
x✝ : ι → ℂ
⊢ 0 ≤ ∑ i, ‖x✝ i‖ ^ p
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:
finrank_pi_fintype,

Goal state after:
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 = ↑(∑ i, finrank ℝ ℂ) / p + 1
Module: Mathlib.MeasureTheory.Measure.MeasuredSets

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
C : Set (Set α)
hC : IsSetRing C
h'C : ∃ D, D.Countable ∧ D ⊆ C ∧ μ (⋃₀ D)ᶜ = 0
h : mα = generateFrom C
s✝ : Set α
hs✝ : MeasurableSet s✝
ε✝ : ℝ≥0∞
hε : 0 < ε✝
s : Set α
hs : MeasurableSet s
h's : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ t ∈ C, μ (t ∆ s) < ε
ε : ℝ≥0∞
εpos : 0 < ε
t : Set α
tC : t ∈ C
ht : μ (t ∆ s) < ε / 2
D : Set (Set α)
D_count : D.Countable
DC : D ⊆ C
hD : μ (⋃₀ D)ᶜ = 0
Dne : D.Nonempty
f : ℕ → Set α
hf : D = range f
fC : ∀ (n : ℕ), accumulate f n ∈ C
this : Tendsto (fun n ↦ μ (accumulate f n)ᶜ) atTop (𝓝 0)
n : ℕ
hn : μ (accumulate f n)ᶜ < ε / 2
⊢ ∃ t' ∈ C, μ t'ᶜ < ε / 2

Tactic:
exact ⟨accumulate f n, fC n, hn⟩

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 + ↑ε
⊢ ∑ i ∈ Finset.range n, (∑ p ∈ (P i).parts, f ↑p + ↑ε) = ∑ i ∈ Finset.range n, ∑ p ∈ (P i).parts, f ↑p + ↑ε'

Tactic:
rw [Finset.sum_add_distrib]; norm_cast
      simp [show n * ε = ε' by field]

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

Goal state before:
pp: case h₁
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 := ⋯
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 + ↑ε
⊢ ∑ i ∈ Finset.range n, ∑ p ∈ (P i).parts, f ↑p ≤ preVariationFun f (⋃ i, s i)

Tactic:
exact sum_le_preVariationFun_iUnion' f hs hs' P n

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)
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 := ⋯
L : Tendsto id (↑f) (𝓝 μ)
n : ℕ
h : Monotone K
this : Tendsto (fun m ↦ ∑ i ∈ Finset.range (m + 1), ↑(ν i) (K n)ᶜ) atTop (𝓝 (∑' (i : ℕ), ↑(ν i) (K n)ᶜ))
m : ℕ
hm : n ≤ m
i : ℕ
hi : i ≤ m
h'i : i ≤ n
⊢ (K n)ᶜ ⊆ ((partialSups K) i)ᶜ

Tactic:
Monotone.partialSups_eq h

Goal state after:
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)
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), ⋯⟩
L : Tendsto id (↑f) (𝓝 μ)
n : ℕ
h : Monotone K
this : Tendsto (fun m ↦ ∑ i ∈ Finset.range (m + 1), ↑(ν i) (K n)ᶜ) atTop (𝓝 (∑' (i : ℕ), ↑(ν i) (K n)ᶜ))
m : ℕ
hm : n ≤ m
i : ℕ
hi : i ≤ m
h'i : i ≤ n
⊢ (K n)ᶜ ⊆ (K i)ᶜ
Module: Mathlib.MeasureTheory.Measure.ResolventTransform

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : HereditarilyLindelofSpace 𝕜
inst✝⁵ : CompleteSpace 𝕜
inst✝⁴ : MeasurableSpace 𝕜
inst✝³ : BorelSpace 𝕜
inst✝² : RCLike A
inst✝¹ : NormedAlgebra 𝕜 A
μ : Measure 𝕜
inst✝ : IsFiniteMeasure μ
a : A
ha : a ∉ ⇑(algebraMap 𝕜 A) '' μ.support
h : μ.support.Nonempty
this : 0 < infDist a (⇑(algebraMap 𝕜 A) '' μ.support)
s : Set A := ball a (infDist a (⇑(algebraMap 𝕜 A) '' μ.support) / 2)
hs_z : s ∈ 𝓝 a
hs_μ : s ⊆ (⇑(algebraMap 𝕜 A) '' μ.support)ᶜ
resolvent_meas : ∀ᶠ (w : A) in 𝓝 a, AEStronglyMeasurable (resolvent w) μ
x : 𝕜
hx : x ∈ μ.support
w : A
hw : w ∈ s
⊢ ‖(algebraMap 𝕜 A) x - a‖ - ‖a - w‖ ≤ ‖(algebraMap 𝕜 A) x - w‖

Tactic:
grw [norm_sub_le_norm_add]

Goal state after:
𝕜 : Type u_1
A : Type u_2
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : HereditarilyLindelofSpace 𝕜
inst✝⁵ : CompleteSpace 𝕜
inst✝⁴ : MeasurableSpace 𝕜
inst✝³ : BorelSpace 𝕜
inst✝² : RCLike A
inst✝¹ : NormedAlgebra 𝕜 A
μ : Measure 𝕜
inst✝ : IsFiniteMeasure μ
a : A
ha : a ∉ ⇑(algebraMap 𝕜 A) '' μ.support
h : μ.support.Nonempty
this : 0 < infDist a (⇑(algebraMap 𝕜 A) '' μ.support)
s : Set A := ball a (infDist a (⇑(algebraMap 𝕜 A) '' μ.support) / 2)
hs_z : s ∈ 𝓝 a
hs_μ : s ⊆ (⇑(algebraMap 𝕜 A) '' μ.support)ᶜ
resolvent_meas : ∀ᶠ (w : A) in 𝓝 a, AEStronglyMeasurable (resolvent w) μ
x : 𝕜
hx : x ∈ μ.support
w : A
hw : w ∈ s
⊢ ‖(algebraMap 𝕜 A) x - a + (a - w)‖ ≤ ‖(algebraMap 𝕜 A) x - w‖
Module: Mathlib.MeasureTheory.Measure.LevyConvergence

Goal state before:
pp: E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
ι : Type u_2
𝓕 : Filter ι
μ₀ : ProbabilityMeasure E
μ✝ : ι → ProbabilityMeasure E
h : ∀ (t : E), Tendsto (fun n ↦ charFun (↑(μ✝ n)) t) 𝓕 (𝓝 (charFun (↑μ₀) t))
g : E →ᵇ ℂ
w : AddMonoidAlgebra ℂ E
hw : ⇑g = fun x ↦ w.coeff.sum fun a z ↦ z * ↑(probChar (((innerₗ E) x) a))
μ : Measure E
hμ : IsProbabilityMeasure μ
⊢ ∫ (x : E), w.coeff.sum fun a z ↦ z * ↑(probChar (((innerₗ E) x) a)) ∂μ =
    w.coeff.sum fun a z ↦ z * ∫ (x : E), ↑(probChar (((innerₗ E) x) a)) ∂μ

Tactic:
Finsupp.sum

Goal state after:
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
ι : Type u_2
𝓕 : Filter ι
μ₀ : ProbabilityMeasure E
μ✝ : ι → ProbabilityMeasure E
h : ∀ (t : E), Tendsto (fun n ↦ charFun (↑(μ✝ n)) t) 𝓕 (𝓝 (charFun (↑μ₀) t))
g : E →ᵇ ℂ
w : AddMonoidAlgebra ℂ E
hw : ⇑g = fun x ↦ w.coeff.sum fun a z ↦ z * ↑(probChar (((innerₗ E) x) a))
μ : Measure E
hμ : IsProbabilityMeasure μ
⊢ ∫ (x : E), ∑ x_1 ∈ w.coeff.support, w.coeff x_1 * ↑(probChar (((innerₗ E) x) x_1)) ∂μ =
    ∑ x ∈ w.coeff.support, w.coeff x * ∫ (x_1 : E), ↑(probChar (((innerₗ E) x_1) x)) ∂μ
Module: Mathlib.MeasureTheory.Measure.SubFinite

Goal state before:
pp: case refine_2
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
inst✝ : IsFiniteMeasure (μ.withDensity g)
hf : Measurable f
hg : Measurable g
⊢ μ.withDensity f - μ.withDensity g ≤ μ.withDensity (f - g)

Tactic:
refine sub_le_of_le_add ?_
    rw [← withDensity_add_right _ hg]
    exact withDensity_mono (ae_of_all _ fun x ↦ le_tsub_add)

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsZeroOneMeasure μ
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
hμs : μ s = 1
hμt : μ t = 1
⊢ μ (s ∩ t) = 1

Tactic:
have : μ (s ∩ t) ≤ μ s := measure_mono inter_subset_left

Goal state after:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsZeroOneMeasure μ
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
hμs : μ s = 1
hμt : μ t = 1
this : μ (s ∩ t) ≤ μ s
⊢ μ (s ∩ t) = 1