mathlib-initiative/mathlib-tactics huggingface dataset:
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✝³ : TopologicalSpace β
inst✝² : AddMonoid β
inst✝¹ : StarAddMonoid β
inst✝ : ContinuousStar β
f : α →C_c β
⊢ (Function.support fun x ↦ star (f x)) = Function.support ⇑f

Tactic:
ext x

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : AddMonoid β
inst✝¹ : StarAddMonoid β
inst✝ : ContinuousStar β
f : α →C_c β
x : α
⊢ (x ∈ Function.support fun x ↦ star (f x)) ↔ x ∈ Function.support ⇑f
Module: Mathlib.Topology.ContinuousMap.CompactlySupported

Goal state before:
pp: case refine_2
α : Type u_2
inst✝ : TopologicalSpace α
f₁ f₂ : α →C_c ℝ≥0
h : f₁ ≤ f₂
⊢ f₁ + { toContinuousMap := f₂.toContinuousMap - f₁.toContinuousMap, hasCompactSupport' := ⋯ } = f₂

Tactic:
ext x

Goal state after:
case refine_2
α : Type u_2
inst✝ : TopologicalSpace α
f₁ f₂ : α →C_c ℝ≥0
h : f₁ ≤ f₂
x : α
⊢ ↑((f₁ + { toContinuousMap := f₂.toContinuousMap - f₁.toContinuousMap, hasCompactSupport' := ⋯ }) x) = ↑(f₂ x)
Module: Mathlib.Topology.ContinuousMap.CompactlySupported

Goal state before:
pp: α : Type u_2
inst✝ : TopologicalSpace α
f : α →C_c ℝ
hf : 0 ≤ f
⊢ (-f).nnrealPart = 0

Tactic:
ext x

Goal state after:
α : Type u_2
inst✝ : TopologicalSpace α
f : α →C_c ℝ
hf : 0 ≤ f
x : α
⊢ ↑((-f).nnrealPart x) = ↑(0 x)
Module: Mathlib.Topology.ContinuousMap.CompactlySupported

Goal state before:
pp: α : Type u_2
inst✝ : TopologicalSpace α
f : α →C_c ℝ
a : ℝ
ha : 0 ≤ a
⊢ (a • f).nnrealPart = a.toNNReal • f.nnrealPart

Tactic:
ext x

Goal state after:
α : Type u_2
inst✝ : TopologicalSpace α
f : α →C_c ℝ
a : ℝ
ha : 0 ≤ a
x : α
⊢ ↑((a • f).nnrealPart x) = ↑((a.toNNReal • f.nnrealPart) x)
Module: Mathlib.Topology.ContinuousMap.CompactlySupported

Goal state before:
pp: α : Type u_2
inst✝ : TopologicalSpace α
f : α →C_c ℝ
a : ℝ
ha : a ≤ 0
⊢ (a • f).nnrealPart = (-a).toNNReal • (-f).nnrealPart

Tactic:
ext x

Goal state after:
α : Type u_2
inst✝ : TopologicalSpace α
f : α →C_c ℝ
a : ℝ
ha : a ≤ 0
x : α
⊢ ↑((a • f).nnrealPart x) = ↑(((-a).toNNReal • (-f).nnrealPart) x)
Module: Mathlib.Topology.ContinuousMap.CompactlySupported

Goal state before:
pp: case h
α : Type u_2
inst✝ : TopologicalSpace α
f g : α →C_c ℝ
h : α →C_c ℝ≥0
hh : (f + g).nnrealPart + h = f.nnrealPart + g.nnrealPart
⊢ (-f + -g).nnrealPart + h = (-f).nnrealPart + (-g).nnrealPart

Tactic:
ext x

Goal state after:
case h
α : Type u_2
inst✝ : TopologicalSpace α
f g : α →C_c ℝ
h : α →C_c ℝ≥0
hh : (f + g).nnrealPart + h = f.nnrealPart + g.nnrealPart
x : α
⊢ ↑(((-f + -g).nnrealPart + h) x) = ↑(((-f).nnrealPart + (-g).nnrealPart) x)
Module: Mathlib.Topology.ContinuousMap.CompactlySupported

Goal state before:
pp: α : Type u_2
inst✝ : TopologicalSpace α
f : α →C_c ℝ
⊢ f.nnrealPart.toReal - (-f).nnrealPart.toReal = f

Tactic:
ext x

Goal state after:
α : Type u_2
inst✝ : TopologicalSpace α
f : α →C_c ℝ
x : α
⊢ (f.nnrealPart.toReal - (-f).nnrealPart.toReal) x = f x
Module: Mathlib.Topology.ContinuousMap.CompactlySupported

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : TopologicalSpace α
f g : α →C_c ℝ≥0
⊢ (f + g).toReal = f.toReal + g.toReal

Tactic:
ext x

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : TopologicalSpace α
f g : α →C_c ℝ≥0
x : α
⊢ (f + g).toReal x = (f.toReal + g.toReal) x
Module: Mathlib.Topology.ContinuousMap.CompactlySupported

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : TopologicalSpace α
a : ℝ≥0
f : α →C_c ℝ≥0
⊢ (a • f).toReal = (RingHom.id ℝ≥0) a • f.toReal

Tactic:
ext x

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : TopologicalSpace α
a : ℝ≥0
f : α →C_c ℝ≥0
x : α
⊢ (a • f).toReal x = ((RingHom.id ℝ≥0) a • f.toReal) x
Module: Mathlib.Topology.ContinuousMap.CompactlySupported

Goal state before:
pp: α : Type u_2
inst✝ : TopologicalSpace α
f : α →C_c ℝ≥0
⊢ f.toReal.nnrealPart = f

Tactic:
ext x

Goal state after:
α : Type u_2
inst✝ : TopologicalSpace α
f : α →C_c ℝ≥0
x : α
⊢ ↑(f.toReal.nnrealPart x) = ↑(f x)
Module: Mathlib.Topology.ContinuousMap.CompactlySupported

Goal state before:
pp: α : Type u_2
inst✝ : TopologicalSpace α
f : α →C_c ℝ≥0
⊢ (-f.toReal).nnrealPart = 0

Tactic:
ext x

Goal state after:
α : Type u_2
inst✝ : TopologicalSpace α
f : α →C_c ℝ≥0
x : α
⊢ ↑((-f.toReal).nnrealPart x) = ↑(0 x)
Module: Mathlib.Topology.ContinuousMap.CompactlySupported

Goal state before:
pp: α : Type u_2
inst✝ : TopologicalSpace α
Λ₁ Λ₂ : (α →C_c ℝ) →ₚ[ℝ] ℝ
h : Λ₁ = Λ₂
⊢ toNNRealLinear Λ₁ = toNNRealLinear Λ₂

Tactic:
by rw [h]

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
⊢ curveIntegralFun ω (γab.trans γbc) =ᵐ[volume.restrict (Ι (1 / 2) 1)] fun t ↦ 2 • curveIntegralFun ω γbc (2 * t - 1)

Tactic:
rw [uIoc_of_le (by linarith), ← restrict_Ioo_eq_restrict_Ioc]

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
a b c : E
ω : E → E →L[𝕜] F
γab : Path a b
γbc : Path b c
⊢ curveIntegralFun ω (γab.trans γbc) =ᵐ[volume.restrict (Ioo (1 / 2) 1)] fun t ↦ 2 • curveIntegralFun ω γbc (2 * t - 1)
Module: Mathlib.MeasureTheory.Integral.CurveIntegral.Basic

Goal state before:
pp: case inr
𝕜 : 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 : E
ω : E → E →L[𝕜] F
γ : Path a b
𝕝 : Type u_4
inst✝² : RCLike 𝕝
inst✝¹ : NormedSpace 𝕝 F
inst✝ : SMulCommClass 𝕜 𝕝 F
c : 𝕝
hc : c ≠ 0
⊢ CurveIntegrable (c • ω) γ ↔ c = 0 ∨ CurveIntegrable ω γ

Tactic:
simp only [hc, false_or]
    refine ⟨fun h ↦ ?_, .smul⟩
    simpa [hc] using h.smul (c := c⁻¹)

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

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
K : Compacts X
ε : ℝ≥0
εpos : 0 < ε
⊢ ∃ f, (∀ x ∈ K, 1 ≤ f x) ∧ Λ f < rieszContentAux Λ K + ε

Tactic:
by
  --choose a test function `f` s.t. `Λf = α < λ(K) + ε`
  obtain ⟨α, ⟨⟨f, f_hyp⟩, α_hyp⟩⟩ :=
    exists_lt_of_csInf_lt (rieszContentAux_image_nonempty Λ K)
      (lt_add_of_pos_right (rieszContentAux Λ K) εpos)
  refine ⟨f, f_hyp.left, ?_⟩
  rw [f_hyp.right]
  exact α_hyp

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

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
K₁ K₂ : Compacts X
disj : Disjoint ↑K₁ ↑K₂
b : ℝ≥0
f : X →C_c ℝ≥0
hf : f ∈ {f | ∀ x ∈ K₁ ⊔ K₂, 1 ≤ f x}
Λf_eq_b : Λ f = b
hsuppf : ∀ x ∈ K₁ ⊔ K₂, x ∈ support ⇑f
hsubsuppf : ↑K₁ ∪ ↑K₂ ⊆ tsupport ⇑f
g₁ g₂ : X →C_c ℝ≥0
hg₁ : EqOn (⇑g₁) 1 K₁.carrier
hg₂ : EqOn (⇑g₂) 1 K₂.carrier
sum_g : EqOn (⇑(g₁ + g₂)) 1 (tsupport f.toFun)
⊢ f = g₁ * f + g₂ * f

Tactic:
ext x

Goal state after:
X : Type u_1
inst✝² : TopologicalSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
K₁ K₂ : Compacts X
disj : Disjoint ↑K₁ ↑K₂
b : ℝ≥0
f : X →C_c ℝ≥0
hf : f ∈ {f | ∀ x ∈ K₁ ⊔ K₂, 1 ≤ f x}
Λf_eq_b : Λ f = b
hsuppf : ∀ x ∈ K₁ ⊔ K₂, x ∈ support ⇑f
hsubsuppf : ↑K₁ ∪ ↑K₂ ⊆ tsupport ⇑f
g₁ g₂ : X →C_c ℝ≥0
hg₁ : EqOn (⇑g₁) 1 K₁.carrier
hg₂ : EqOn (⇑g₂) 1 K₂.carrier
sum_g : EqOn (⇑(g₁ + g₂)) 1 (tsupport f.toFun)
x : X
⊢ ↑(f x) = ↑((g₁ * f + g₂ * f) x)
Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real

Goal state before:
pp: case calc_1.e_6
X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : T2Space X
inst✝² : MeasurableSpace X
inst✝¹ : BorelSpace X
Λ : (X →C_c ℝ) →ₚ[ℝ] ℝ
inst✝ : LocallyCompactSpace X
f : X →C_c ℝ
μ : Measure X := ⋯
K : Set X := ⋯
ε : ℝ
hε : 0 < ε
a b : ℝ
hab : a < b ∧ range ⇑f ⊆ Ioo a b
N : ℕ
hN : 0 < N
ε' : ℝ := ⋯
hε' : 0 < ε' ∧ ε' * (2 * μ.real K + |a| + b + ε') ≤ ε
E : Fin N → Set X
hE :
  tsupport ⇑f = ⋃ j, E j ∧
    univ.PairwiseDisjoint E ∧
      (∀ (n : Fin N), ∀ x ∈ E n, a + ε' * ↑↑n < f x ∧ f x ≤ a + ε' * (↑↑n + 1)) ∧ ∀ (n : Fin N), MeasurableSet (E n)
y : Fin N → ℝ := ⋯
hE' : ∀ (n : Fin N), μ (E n) ≠ ∞
V : Fin N → Opens X
hV : ∀ (n : Fin N), E n ⊆ ↑(V n) ∧ (∀ x ∈ V n, f x < y n + ε') ∧ μ ↑(V n) ≤ μ (E n) + ENNReal.ofReal (ε' / ↑N)
g : Fin N → X →C_c ℝ
hg :
  (∀ (n : Fin N), tsupport ⇑(g n) ⊆ (V n).carrier) ∧
    EqOn (∑ n, ⇑(g n)) 1 (tsupport f.toFun) ∧
      (∀ (n : Fin N) (x : X), (g n) x ∈ Icc 0 1) ∧ ∀ (n : Fin N), HasCompactSupport ⇑(g n)
⊢ f = ∑ n, g n • f

Tactic:
ext x

Goal state after:
case calc_1.e_6
X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : T2Space X
inst✝² : MeasurableSpace X
inst✝¹ : BorelSpace X
Λ : (X →C_c ℝ) →ₚ[ℝ] ℝ
inst✝ : LocallyCompactSpace X
f : X →C_c ℝ
μ : Measure X := rieszMeasure Λ
K : Set X := tsupport ⇑f
ε : ℝ
hε : 0 < ε
a b : ℝ
hab : a < b ∧ range ⇑f ⊆ Ioo a b
N : ℕ
hN : 0 < N
ε' : ℝ := (b - a) / ↑N
hε' : 0 < ε' ∧ ε' * (2 * μ.real K + |a| + b + ε') ≤ ε
E : Fin N → Set X
hE :
  tsupport ⇑f = ⋃ j, E j ∧
    univ.PairwiseDisjoint E ∧
      (∀ (n : Fin N), ∀ x ∈ E n, a + ε' * ↑↑n < f x ∧ f x ≤ a + ε' * (↑↑n + 1)) ∧ ∀ (n : Fin N), MeasurableSet (E n)
y : Fin N → ℝ := fun n ↦ a + ε' * (↑↑n + 1)
hE' : ∀ (n : Fin N), μ (E n) ≠ ∞
V : Fin N → Opens X
hV : ∀ (n : Fin N), E n ⊆ ↑(V n) ∧ (∀ x ∈ V n, f x < y n + ε') ∧ μ ↑(V n) ≤ μ (E n) + ENNReal.ofReal (ε' / ↑N)
g : Fin N → X →C_c ℝ
hg :
  (∀ (n : Fin N), tsupport ⇑(g n) ⊆ (V n).carrier) ∧
    EqOn (∑ n, ⇑(g n)) 1 (tsupport f.toFun) ∧
      (∀ (n : Fin N) (x : X), (g n) x ∈ Icc 0 1) ∧ ∀ (n : Fin N), HasCompactSupport ⇑(g n)
x : X
⊢ f x = (∑ n, g n • f) x
Module: Mathlib.Topology.Separation.CompletelyRegular

Goal state before:
pp: X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : NormalSpace X
inst✝ : R0Space X
x : X
K : Set X
hK : IsClosed[inst✝²] K
hx : x ∉ K
cx : IsClosed[inst✝²] (closure[inst✝²] {x})
⊢ Disjoint (closure[inst✝²] {x}) K

Tactic:
Set.disjoint_iff

Goal state after:
X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : NormalSpace X
inst✝ : R0Space X
x : X
K : Set X
hK : IsClosed[inst✝²] K
hx : x ∉ K
cx : IsClosed[inst✝²] (closure[inst✝²] {x})
⊢ closure[inst✝²] {x} ∩ K ⊆ ∅
Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real

Goal state before:
pp: case calc_3
X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : T2Space X
inst✝² : MeasurableSpace X
inst✝¹ : BorelSpace X
Λ : (X →C_c ℝ) →ₚ[ℝ] ℝ
inst✝ : LocallyCompactSpace X
f : X →C_c ℝ
μ : Measure X := rieszMeasure Λ
K : Set X := tsupport ⇑f
ε : ℝ
hε : 0 < ε
a b : ℝ
hab : a < b ∧ range ⇑f ⊆ Ioo a b
N : ℕ
hN : 0 < N
ε' : ℝ := (b - a) / ↑N
hε' : 0 < ε' ∧ ε' * (2 * μ.real K + |a| + b + ε') ≤ ε
E : Fin N → Set X
hE :
  tsupport ⇑f = ⋃ j, E j ∧
    univ.PairwiseDisjoint E ∧
      (∀ (n : Fin N), ∀ x ∈ E n, a + ε' * ↑↑n < f x ∧ f x ≤ a + ε' * (↑↑n + 1)) ∧ ∀ (n : Fin N), MeasurableSet (E n)
y : Fin N → ℝ := fun n ↦ a + ε' * (↑↑n + 1)
hE' : ∀ (n : Fin N), μ (E n) ≠ ∞
V : Fin N → Opens X
hV : ∀ (n : Fin N), E n ⊆ ↑(V n) ∧ (∀ x ∈ V n, f x < y n + ε') ∧ μ ↑(V n) ≤ μ (E n) + ENNReal.ofReal (ε' / ↑N)
g : Fin N → X →C_c ℝ
hg :
  (∀ (n : Fin N), tsupport ⇑(g n) ⊆ (V n).carrier) ∧
    EqOn (∑ n, ⇑(g n)) 1 (tsupport f.toFun) ∧
      (∀ (n : Fin N) (x : X), (g n) x ∈ Icc 0 1) ∧ ∀ (n : Fin N), HasCompactSupport ⇑(g n)
⊢ ∑ n, (|a| + y n + ε') * Λ (g n) - |a| * ∑ n, Λ (g n) ≤
    ∑ n, (|a| + y n + ε') * (μ.real (E n) + ε' / ↑N) - |a| * ∑ n, Λ (g n)

Tactic:
gcongr with n hn
    · calc
        _ ≤ |a| + a := neg_le_iff_add_nonneg'.mp <| neg_abs_le a
        _ ≤ |a| + a + ε' * (n + 1) := (le_add_iff_nonneg_right (|a| + a)).mpr <| Left.mul_nonneg
          (le_of_lt hε'.1) <| Left.add_nonneg (Nat.cast_nonneg' n) (zero_le_one' ℝ)
        _ ≤ _ := by rw [← add_assoc, le_add_iff_nonneg_right]; exact le_of_lt hε'.1
    · calc
        _ ≤ μ.real (V n) := by
          apply (ENNReal.ofReal_le_iff_le_toReal _).mp
          · exact le_rieszMeasure_tsupport_subset Λ (fun x ↦ hg.2.2.1 n x) (hg.1 n)
          · rw [← lt_top_iff_ne_top]
            apply lt_of_le_of_lt (hV n).2.2
            rw [WithTop.add_lt_top]
            exact ⟨WithTop.lt_top_iff_ne_top.mpr (hE' n), ENNReal.ofReal_lt_top⟩
        _ ≤ _ := by
          rw [← ENNReal.toReal_ofReal (div_nonneg (le_of_lt hε'.1) (Nat.cast_nonneg _))]
          apply ENNReal.toReal_le_add (hV n).2.2 (hE' n)
          · finiteness

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

Goal state before:
pp: case calc_5
X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : T2Space X
inst✝² : MeasurableSpace X
inst✝¹ : BorelSpace X
Λ : (X →C_c ℝ) →ₚ[ℝ] ℝ
inst✝ : LocallyCompactSpace X
f : X →C_c ℝ
μ : Measure X := rieszMeasure Λ
K : Set X := tsupport ⇑f
ε : ℝ
hε : 0 < ε
a b : ℝ
hab : a < b ∧ range ⇑f ⊆ Ioo a b
N : ℕ
hN : 0 < N
ε' : ℝ := (b - a) / ↑N
hε' : 0 < ε' ∧ ε' * (2 * μ.real K + |a| + b + ε') ≤ ε
E : Fin N → Set X
hE :
  tsupport ⇑f = ⋃ j, E j ∧
    univ.PairwiseDisjoint E ∧
      (∀ (n : Fin N), ∀ x ∈ E n, a + ε' * ↑↑n < f x ∧ f x ≤ a + ε' * (↑↑n + 1)) ∧ ∀ (n : Fin N), MeasurableSet (E n)
y : Fin N → ℝ := fun n ↦ a + ε' * (↑↑n + 1)
hE' : ∀ (n : Fin N), μ (E n) ≠ ∞
V : Fin N → Opens X
hV : ∀ (n : Fin N), E n ⊆ ↑(V n) ∧ (∀ x ∈ V n, f x < y n + ε') ∧ μ ↑(V n) ≤ μ (E n) + ENNReal.ofReal (ε' / ↑N)
g : Fin N → X →C_c ℝ
hg :
  (∀ (n : Fin N), tsupport ⇑(g n) ⊆ (V n).carrier) ∧
    EqOn (∑ n, ⇑(g n)) 1 (tsupport f.toFun) ∧
      (∀ (n : Fin N) (x : X), (g n) x ∈ Icc 0 1) ∧ ∀ (n : Fin N), HasCompactSupport ⇑(g n)
⊢ ∑ n, (|a| + y n + ε') * (μ.real (E n) + ε' / ↑N) - |a| * μ.real K =
    ∑ n, (y n - ε') * μ.real (E n) + 2 * ε' * μ.real K + ε' / ↑N * ∑ n, (|a| + y n + ε')

Tactic:
have (n : Fin N) : (|a| + y n + ε') * μ.real (E n) =
        (|a| + 2 * ε') * μ.real (E n) + (y n - ε') * μ.real (E n) := by linarith
    simp_rw [mul_add, this]
    have : ∑ i, μ.real (E i) = μ.real K := by
      suffices h : μ K = ∑ i, (μ (E i)) by
        simp only [measureReal_def, h]
        exact Eq.symm <| ENNReal.toReal_sum <| fun n _ ↦ hE' n
      dsimp [K]; rw [hE.1]
      rw [measure_iUnion (fun m n hmn ↦ hE.2.1 trivial trivial hmn) hE.2.2.2]
      exact tsum_fintype fun b ↦ μ (E b)
    rw [Finset.sum_add_distrib, Finset.sum_add_distrib, ← Finset.mul_sum, this, ← Finset.sum_mul]
    linarith

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

Goal state before:
pp: case h1
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : PseudoEMetricSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ ν : Measure Ω
hLP : levyProkhorovEDist μ ν = 0
s : Set Ω
s_mble : MeasurableSet s
h_finite : ∃ δ > 0, ν (thickening δ s) ≠ ∞
⊢ Tendsto ENNReal.toReal (𝓝[>] 0) (𝓝 0)

Tactic:
exact tendsto_nhdsWithin_of_tendsto_nhds (continuousAt_toReal zero_ne_top).tendsto

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

Goal state before:
pp: Ω : Type u_1
inst✝⁴ : MeasurableSpace Ω
inst✝³ : PseudoEMetricSpace Ω
inst✝² : OpensMeasurableSpace Ω
μ ν : Measure Ω
inst✝¹ : IsProbabilityMeasure μ
inst✝ : IsProbabilityMeasure ν
δ : ℝ
δ_nn : 0 ≤ δ
h : ∀ (ε : ℝ) (B : Set Ω), δ < ε → MeasurableSet B → μ B ≤ ν (thickening ε B) + ENNReal.ofReal ε
ε : ℝ≥0∞
B : Set Ω
ε_gt : ENNReal.ofReal δ < ε
ε_lt_top : ε < ∞
B_mble : MeasurableSet B
ε_gt' : δ < ε.toReal
⊢ μ B ≤ ν (thickening ε.toReal B) + ε

Tactic:
convert! h ε.toReal B ε_gt' B_mble

Goal state after:
Ω : Type u_1
inst✝⁴ : MeasurableSpace Ω
inst✝³ : PseudoEMetricSpace Ω
inst✝² : OpensMeasurableSpace Ω
μ ν : Measure Ω
inst✝¹ : IsProbabilityMeasure μ
inst✝ : IsProbabilityMeasure ν
δ : ℝ
δ_nn : 0 ≤ δ
h : ∀ (ε : ℝ) (B : Set Ω), δ < ε → MeasurableSet B → μ B ≤ ν (thickening ε B) + ENNReal.ofReal ε
ε : ℝ≥0∞
B : Set Ω
ε_gt : ENNReal.ofReal δ < ε
ε_lt_top : ε < ∞
B_mble : MeasurableSet B
ε_gt' : δ < ε.toReal
⊢ ε = ENNReal.ofReal ε.toReal
Module: Mathlib.MeasureTheory.Measure.FiniteMeasurePi

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝⁵ : Fintype ι
inst✝⁴ : (i : ι) → MeasurableSpace (α i)
inst✝³ : (i : ι) → TopologicalSpace (α i)
inst✝² : ∀ (i : ι), SecondCountableTopology (α i)
inst✝¹ : ∀ (i : ι), PseudoMetrizableSpace (α i)
inst✝ : ∀ (i : ι), OpensMeasurableSpace (α i)
μ : (i : ι) → ProbabilityMeasure (α i)
S : Set (Set ((i : ι) → α i)) :=
  {t | ∃ s, t = univ.pi s ∧ (∀ (i : ι), MeasurableSet (s i)) ∧ ∀ (i : ι), (μ i) (frontier (s i)) = 0}
this✝ : IsPiSystem S
this : (i : ι) → PseudoMetricSpace (α i) := fun i ↦ pseudoMetrizableSpacePseudoMetric (α i)
u : Set ((i : ι) → α i)
u_open : IsOpen[Pi.topologicalSpace] u
x : (i : ι) → α i
xu : x ∈ u
ε : ℝ
εpos : ε > 0
hε : ball x ε ⊆ u
r : ι → ℝ
rpos : ∀ (i : ι), r i ∈ Ioo 0 ε
hr : ∀ (i : ι), ↑(μ i) (frontier (thickening (r i) {x i})) = 0
⊢ (univ.pi fun i ↦ ball (x i) ε) ⊆ u

Tactic:
rwa [← ball_pi _ εpos]

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

Goal state before:
pp: Ω : 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 : Ω →ᵇ ℝ), 0 ≤ f → limsup (fun i ↦ ∫ (x : Ω), f x ∂↑(Ps i)) atTop ≤ ∫ (x : Ω), f x ∂↑P

Tactic:
intro f f_nn

Goal state after:
Ω : 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
⊢ limsup (fun i ↦ ∫ (x : Ω), f x ∂↑(Ps i)) atTop ≤ ∫ (x : Ω), f x ∂↑P
Module: Mathlib.MeasureTheory.Measure.Haar.Extension

Goal state before:
pp: A : Type u_1
B : Type u_2
C : Type u_3
E : Type u_4
inst✝¹¹ : Group A
inst✝¹⁰ : Group B
inst✝⁹ : Group C
inst✝⁸ : TopologicalSpace A
inst✝⁷ : TopologicalSpace B
inst✝⁶ : TopologicalSpace C
φ : A →* B
ψ : B →* C
H : IsSES φ ψ
inst✝⁵ : IsTopologicalGroup A
inst✝⁴ : IsTopologicalGroup B
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace A
inst✝¹ : BorelSpace A
μA : Measure A
hμA : μA.IsHaarMeasure
inst✝ : NormedSpace ℝ E
f : CompactlySupportedContinuousMap B E
b : B
h : (Function.invFun (⇑ψ) (ψ b))⁻¹ * b ∈ φ.range
⊢ ∫ (a : A), (H.pullback f (Function.invFun (⇑ψ) (ψ b))) a ∂μA = ∫ (a : A), (H.pullback f b) a ∂μA

Tactic:
obtain ⟨a, ha⟩ := h

Goal state after:
A : Type u_1
B : Type u_2
C : Type u_3
E : Type u_4
inst✝¹¹ : Group A
inst✝¹⁰ : Group B
inst✝⁹ : Group C
inst✝⁸ : TopologicalSpace A
inst✝⁷ : TopologicalSpace B
inst✝⁶ : TopologicalSpace C
φ : A →* B
ψ : B →* C
H : IsSES φ ψ
inst✝⁵ : IsTopologicalGroup A
inst✝⁴ : IsTopologicalGroup B
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace A
inst✝¹ : BorelSpace A
μA : Measure A
hμA : μA.IsHaarMeasure
inst✝ : NormedSpace ℝ E
f : CompactlySupportedContinuousMap B E
b : B
a : A
ha : φ a = (Function.invFun (⇑ψ) (ψ b))⁻¹ * b
⊢ ∫ (a : A), (H.pullback f (Function.invFun (⇑ψ) (ψ b))) a ∂μA = ∫ (a : A), (H.pullback f b) a ∂μA
Module: Mathlib.MeasureTheory.Measure.Haar.Extension

Goal state before:
pp: A : Type u_1
B : Type u_2
C : Type u_3
E : Type u_4
inst✝¹³ : Group A
inst✝¹² : Group B
inst✝¹¹ : Group C
inst✝¹⁰ : TopologicalSpace A
inst✝⁹ : TopologicalSpace B
inst✝⁸ : TopologicalSpace C
φ : A →* B
ψ : B →* C
H : IsSES φ ψ
inst✝⁷ : IsTopologicalGroup A
inst✝⁶ : IsTopologicalGroup B
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : MeasurableSpace A
inst✝³ : BorelSpace A
μA : Measure A
hμA : μA.IsHaarMeasure
inst✝² : NormedSpace ℝ E
inst✝¹ : IsTopologicalGroup C
inst✝ : LocallyCompactSpace B
f : CompactlySupportedContinuousMap B E
this : UniformSpace B := IsTopologicalGroup.rightUniformSpace B
ε : ℝ
hε : ε > 0
U₀ : Set B
hU₀ : IsCompact U₀
K : Set B
hK : IsCompact K
hf₀ : ∀ x ∉ K, f x = 0
S : Set A := ⇑φ ⁻¹' (U₀⁻¹ * K)
hSc : IsCompact S
δ : ℝ
hδ0 : δ > 0
hδ : ENNReal.ofReal δ * μA S < ENNReal.ofReal ε
hS : ∀ {x : B}, x ∈ U₀ → ∀ {y : A}, y ∉ S → (H.pullback f x) y = 0
ha : ∀ r ∈ uniformity E, ∀ᶠ (x : B × B) in uniformity B, (f x.1, f x.2) ∈ r
U : Set B
hU : U ∈ nhds 1
hf : (fun p ↦ p.2 * p.1⁻¹) ⁻¹' U ⊆ {x | (fun x ↦ (f x.1, f x.2) ∈ {p | dist p.1 p.2 < δ}) x}
t : B
ht : t ∈ U⁻¹
b : B
hb : U₀ ∈ nhds b
htb : (fun x1 x2 ↦ x1 * x2) t b ∈ U₀
h : ∀ a ∈ S, edist ((H.pullback f (t * b)) a) ((H.pullback f b) a) ≤ ENNReal.ofReal δ
⊢ ∫⁻ (x : A) in S, ENNReal.ofReal δ ∂μA < ENNReal.ofReal ε

Tactic:
rwa [lintegral_const, restrict_apply_univ]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Haar.Extension

Goal state before:
pp: A : Type u_1
B : Type u_2
C : Type u_3
E : Type u_4
inst✝¹⁵ : Group A
inst✝¹⁴ : Group B
inst✝¹³ : Group C
inst✝¹² : TopologicalSpace A
inst✝¹¹ : TopologicalSpace B
inst✝¹⁰ : TopologicalSpace C
φ : A →* B
ψ : B →* C
H : IsSES φ ψ
inst✝⁹ : IsTopologicalGroup A
inst✝⁸ : IsTopologicalGroup B
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : MeasurableSpace A
inst✝⁵ : BorelSpace A
μA : Measure A
hμA : μA.IsHaarMeasure
inst✝⁴ : NormedSpace ℝ E
inst✝³ : IsTopologicalGroup C
inst✝² : LocallyCompactSpace B
inst✝¹ : MeasurableSpace C
inst✝ : BorelSpace C
μC : Measure C
hμC : μC.IsHaarMeasure
x : ℝ
f : CompactlySupportedContinuousMap B E
⊢ ∫ (c : C), ((H.pushforward μA) (x • f)) c ∂μC = (RingHom.id ℝ) x • ∫ (c : C), ((H.pushforward μA) f) c ∂μC

Tactic:
rw [map_smul]
    exact integral_smul x (H.pushforward μA f)

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

Goal state before:
pp: E : Type u_1
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module ℝ E
inst✝⁵ : FiniteDimensional ℝ E
mE : MeasurableSpace E
tE : TopologicalSpace E
inst✝⁴ : IsTopologicalAddGroup E
inst✝³ : BorelSpace E
inst✝² : T2Space E
inst✝¹ : ContinuousSMul ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
g : E → ℝ
h1 : g 0 = 0
h2 : ∀ (x : E), g (-x) = g x
h3 : ∀ (x y : E), g (x + y) ≤ g x + g y
h4 : ∀ {x : E}, g x = 0 → x = 0
h5 : ∀ (r : ℝ) (x : E), g (r • x) ≤ |r| * g x
p : ℝ
hp : 0 < p
F : Type u_1 := E
⊢ μ {x | g x < 1} = ENNReal.ofReal ((∫ (x : E), Real.exp (-g x ^ p) ∂μ) / Real.Gamma (↑(finrank ℝ E) / p + 1))

Tactic:
let p : AddGroupNorm F := ⟨⟨g, h1, h3, h2⟩, fun x hx ↦ h4 hx⟩

Goal state after:
E : Type u_1
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module ℝ E
inst✝⁵ : FiniteDimensional ℝ E
mE : MeasurableSpace E
tE : TopologicalSpace E
inst✝⁴ : IsTopologicalAddGroup E
inst✝³ : BorelSpace E
inst✝² : T2Space E
inst✝¹ : ContinuousSMul ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
g : E → ℝ
h1 : g 0 = 0
h2 : ∀ (x : E), g (-x) = g x
h3 : ∀ (x y : E), g (x + y) ≤ g x + g y
h4 : ∀ {x : E}, g x = 0 → x = 0
h5 : ∀ (r : ℝ) (x : E), g (r • x) ≤ |r| * g x
p✝ : ℝ
hp : 0 < p✝
F : Type u_1 := E
p : AddGroupNorm F := { toFun := g, map_zero' := h1, add_le' := h3, neg' := h2, eq_zero_of_map_eq_zero' := ⋯ }
⊢ μ {x | g x < 1} = ENNReal.ofReal ((∫ (x : E), Real.exp (-g x ^ p✝) ∂μ) / Real.Gamma (↑(finrank ℝ E) / p✝ + 1))