mathlib-initiative/mathlib-tactics huggingface dataset:
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✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
a : E
s : Set E
ω : E → E →L[𝕜] F
hs : Convex ℝ s
hω : ∀ᶠ (x : E) in 𝓝[s] a, ContinuousWithinAt ω s x
ha : a ∈ s
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ₀ : δ > 0
hδ : ball a δ ∩ s ⊆ {z | ContinuousWithinAt ω s z ∧ dist (ω z) (ω a) ≤ ε}
b : E
hb : b ∈ ball a δ
hbs : b ∈ s
hsub : [a -[ℝ] b] ⊆ ball a δ ∩ s
⊢ ‖∫ᶜ (x : E) in Path.segment a b, ω x - (ω a) (b - a)‖ ≤ ε * ‖b - a‖

Tactic:
← curveIntegral_segment_const,

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
a : E
s : Set E
ω : E → E →L[𝕜] F
hs : Convex ℝ s
hω : ∀ᶠ (x : E) in 𝓝[s] a, ContinuousWithinAt ω s x
ha : a ∈ s
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ₀ : δ > 0
hδ : ball a δ ∩ s ⊆ {z | ContinuousWithinAt ω s z ∧ dist (ω z) (ω a) ≤ ε}
b : E
hb : b ∈ ball a δ
hbs : b ∈ s
hsub : [a -[ℝ] b] ⊆ ball a δ ∩ s
⊢ ‖∫ᶜ (x : E) in Path.segment a b, ω x - ∫ᶜ (x : E) in Path.segment a b, ω a‖ ≤ ε * ‖b - a‖
Module: Mathlib.MeasureTheory.Integral.Regular

Goal state before:
pp: case a
X : Type u_1
inst✝⁶ : TopologicalSpace X
inst✝⁵ : MeasurableSpace X
inst✝⁴ : BorelSpace X
inst✝³ : T2Space X
U : Set X
hU : IsOpen U
μ : Measure X
inst✝² : IsFiniteMeasure μ
inst✝¹ : μ.InnerRegularCompactLTTop
inst✝ : NormalSpace X
⊢ μ U ≤ ⨆ f, ⨆ (_ : Continuous f), ⨆ (_ : EqOn f 0 Uᶜ), ⨆ (_ : 0 ≤ f), ⨆ (_ : f ≤ 1), ENNReal.ofReal (∫ (x : X), f x ∂μ)

Tactic:
apply le_of_forall_lt (fun r hr ↦ ?_)
    simp only [lt_iSup_iff, exists_prop]
    obtain ⟨K, KU, K_comp, hK⟩ : ∃ K ⊆ U, IsCompact K ∧ r < μ K :=
      MeasurableSet.exists_lt_isCompact_of_ne_top hU.measurableSet (by simp) hr
    obtain ⟨⟨f, f_cont⟩, fU, fK, f_range⟩ : ∃ (f : C(X, ℝ)), EqOn f 0 Uᶜ ∧ EqOn f 1 K
        ∧ ∀ (x : X), f x ∈ Icc 0 1 := exists_continuous_zero_one_of_isClosed
      hU.isClosed_compl K_comp.isClosed (disjoint_compl_left_iff_subset.mpr KU)
    refine ⟨f, f_cont, fU, fun x ↦ (f_range x).1, fun x ↦ (f_range x).2, ?_⟩
    apply hK.trans_le
    apply Integrable.measure_le_integral
    · apply Integrable.of_mem_Icc 0 1 f_cont.aemeasurable
      filter_upwards [] with x using f_range x
    · filter_upwards [] with x using (f_range x).1
    · intro x hx
      apply Eq.ge
      exact fK hx

Goal state after:
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule

Goal state before:
pp: f : ℝ → ℝ
ζ a b : ℝ
a_lt_b : a < b
h_df : DifferentiableOn ℝ f (Set.Icc a b)
h_ddf : DifferentiableOn ℝ (_root_.derivWithin f (Set.Icc a b)) (Set.Icc a b)
fpp_bound : ∀ (x : ℝ), |iteratedDerivWithin 2 f (Set.Icc a b) x| ≤ ζ
N : ℕ
N_nonzero : 0 < N
h : ℝ := (b - a) / ↑N
ak : ℕ → ℝ := fun k ↦ a + ↑k * h
⊢ ∀ (k : ℕ), ak (k + 1) - ak k = h

Tactic:
simp [ak, ← sub_mul]

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
⊢ rieszContentAux Λ K₁ + rieszContentAux Λ K₂ ≤ b

Tactic:
have hsubsuppf : (K₁ : Set X) ∪ (K₂ : Set X) ⊆ tsupport f := subset_trans hsuppf subset_closure

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
⊢ rieszContentAux Λ K₁ + rieszContentAux Λ K₂ ≤ b
Module: Mathlib.MeasureTheory.MeasurableSpace.Invariants

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
f g : α → α
s : Set α
hs : MeasurableSet s
⊢ f ∘ g ⁻¹' s = s

Tactic:
preimage_comp,

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
f g : α → α
s : Set α
hs : MeasurableSet s
⊢ g ⁻¹' f ⁻¹' s = s
Module: Mathlib.MeasureTheory.MeasurableSpace.Invariants

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
β : Type u_2
inst✝ : MeasurableSpace β
fa : α → α
fb : β → β
g : α → β
hg : Measurable g
hfg : Semiconj g fa fb
s : Set β
hs : MeasurableSet s
⊢ fa ⁻¹' g ⁻¹' s = g ⁻¹' s

Tactic:
← preimage_comp,

Goal state after:
α : Type u_1
inst✝¹ : MeasurableSpace α
β : Type u_2
inst✝ : MeasurableSpace β
fa : α → α
fb : β → β
g : α → β
hg : Measurable g
hfg : Semiconj g fa fb
s : Set β
hs : MeasurableSet s
⊢ g ∘ fa ⁻¹' s = g ⁻¹' s
Module: Mathlib.MeasureTheory.MeasurableSpace.Invariants

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
β : Type u_2
inst✝ : MeasurableSpace β
fa : α → α
fb : β → β
g : α → β
hg : Measurable g
hfg : Semiconj g fa fb
s : Set β
hs : MeasurableSet s
⊢ fb ∘ g ⁻¹' s = g ⁻¹' s

Tactic:
preimage_comp,

Goal state after:
α : Type u_1
inst✝¹ : MeasurableSpace α
β : Type u_2
inst✝ : MeasurableSpace β
fa : α → α
fb : β → β
g : α → β
hg : Measurable g
hfg : Semiconj g fa fb
s : Set β
hs : MeasurableSet s
⊢ g ⁻¹' fb ⁻¹' s = g ⁻¹' s
Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic

Goal state before:
pp: case hfm
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
mE : MeasurableSpace E
μ : Measure E
inst✝ : OpensMeasurableSpace E
L : StrongDual ℝ E
⊢ AEStronglyMeasurable (fun x ↦ cexp (↑x * I)) (Measure.map (⇑L) μ)

Tactic:
· exact Measurable.aestronglyMeasurable <| by fun_prop

Goal state after:
Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic

Goal state before:
pp: case hfm
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
mE : MeasurableSpace E
μ : Measure E
inst✝ : OpensMeasurableSpace E
L : StrongDual ℝ E
u : ℝ
⊢ AEStronglyMeasurable (fun x ↦ cexp (↑u * ↑x * I)) (Measure.map (⇑L) μ)

Tactic:
· exact Measurable.aestronglyMeasurable <| by fun_prop

Goal state after:
Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic

Goal state before:
pp: ι : Type u_4
inst✝⁴ : Fintype ι
inst✝³ : DecidableEq ι
E : ι → Type u_5
inst✝² : (i : ι) → NormedAddCommGroup (E i)
inst✝¹ : (i : ι) → NormedSpace ℝ (E i)
mE : (i : ι) → MeasurableSpace (E i)
μ : (i : ι) → Measure (E i)
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
L : StrongDual ℝ ((i : ι) → E i)
⊢ ∫ (v : (i : ι) → E i), ∏ x, cexp (↑((L ∘SL ContinuousLinearMap.single ℝ E x) (v x)) * I) ∂Measure.pi μ =
    ∏ i, ∫ (v : E i), cexp (↑((L ∘SL ContinuousLinearMap.single ℝ E i) v) * I) ∂μ i

Tactic:
← integral_fintype_prod_eq_prod

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

Goal state before:
pp: 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)
this : ∀ (n : Fin N), (|a| + y n + ε') * μ.real (E n) = (|a| + 2 * ε') * μ.real (E n) + (y n - ε') * μ.real (E n)
h : μ K = ∑ i, μ (E i)
⊢ ∑ i, μ.real (E i) = μ.real K

Tactic:
simp only [measureReal_def, h]

Goal state after:
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)
this : ∀ (n : Fin N), (|a| + y n + ε') * μ.real (E n) = (|a| + 2 * ε') * μ.real (E n) + (y n - ε') * μ.real (E n)
h : μ K = ∑ i, μ (E i)
⊢ ∑ x, (μ (E x)).toReal = (∑ i, μ (E i)).toReal
Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric

Goal state before:
pp: case pos
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : PseudoEMetricSpace Ω
ε₁ ε₂ : ℝ≥0∞
μ ν : Measure Ω
h_le : ε₁ ≤ ε₂
B : Set Ω
hε₁ : μ B ≤ ν (thickening ε₁.toReal B) + ε₁
ε_top : ε₂ = ∞
⊢ μ B ≤ ν (thickening ε₂.toReal B) + ε₂

pp: case neg
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : PseudoEMetricSpace Ω
ε₁ ε₂ : ℝ≥0∞
μ ν : Measure Ω
h_le : ε₁ ≤ ε₂
B : Set Ω
hε₁ : μ B ≤ ν (thickening ε₁.toReal B) + ε₁
ε_top : ¬ε₂ = ∞
⊢ μ B ≤ ν (thickening ε₂.toReal B) + ε₂

Tactic:
· simp only [ε_top, toReal_top,
                add_top, le_top]

Goal state after:
case neg
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : PseudoEMetricSpace Ω
ε₁ ε₂ : ℝ≥0∞
μ ν : Measure Ω
h_le : ε₁ ≤ ε₂
B : Set Ω
hε₁ : μ B ≤ ν (thickening ε₁.toReal B) + ε₁
ε_top : ¬ε₂ = ∞
⊢ μ B ≤ ν (thickening ε₂.toReal B) + ε₂
Module: Mathlib.MeasureTheory.Measure.FiniteMeasurePi

Goal state before:
pp: case hx
ι : 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)) := ⋯
this✝ : IsPiSystem S
this : (i : ι) → PseudoMetricSpace (α 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
⊢ x ∈ univ.pi fun i ↦ ball (x i) (r i)

Tactic:
simpa using fun i ↦ (rpos i).1

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

Goal state before:
pp: case h
ι : 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)) := ⋯
this : IsPiSystem S
⊢ ∀ (u : Set ((i : ι) → α i)), IsOpen[Pi.topologicalSpace] u → ∀ x ∈ u, ∃ s ∈ S, s ∈ 𝓝 x ∧ s ⊆ u

Tactic:
let : ∀ i, PseudoMetricSpace (α i) :=
      fun i ↦ TopologicalSpace.pseudoMetrizableSpacePseudoMetric (α i)
    intro u u_open x xu
    obtain ⟨ε, εpos, hε⟩ : ∃ ε > 0, ball x ε ⊆ u := Metric.isOpen_iff.1 u_open x xu
    have A (i) : ∃ r ∈ Ioo 0 ε, (μ i : Measure (α i)) (frontier (Metric.thickening r {x i})) = 0 :=
      exists_null_frontier_thickening _ _ εpos
    choose! r rpos hr using A
    refine ⟨univ.pi (fun i ↦ ball (x i) (r i)), ⟨fun i ↦ ball (x i) (r i), rfl,
      fun i ↦ measurableSet_ball, fun i ↦ by simpa using hr i⟩, ?_, ?_⟩
    · apply IsOpen.mem_nhds
      · exact isOpen_set_pi finite_univ (by simp)
      · simpa using fun i ↦ (rpos i).1
    · calc univ.pi fun i ↦ ball (x i) (r i)
      _ ⊆ univ.pi fun i ↦ ball (x i) ε := by gcongr with i hi; exact (rpos i).2.le
      _ ⊆ u := by rwa [← ball_pi _ εpos]

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

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

pp: case neg
Ω : 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
⊢ limsup (fun i ↦ ∫ (x : Ω), f x ∂↑(Ps i)) atTop ≤ ∫ (x : Ω), f x ∂↑P

Tactic:
· simp only [norm_eq_zero] at f_zero
    simp [f_zero, limsup_const]

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

Goal state before:
pp: case e'_2
X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : T2Space X
inst✝² : MeasurableSpace X
inst✝¹ : BorelSpace X
μ : Measure X
inst✝ : IsFiniteMeasure μ
K : Set X
hK : IsCompact K
h : μ Kᶜ = 0
μ' : Measure ↑K := Measure.comap Subtype.val μ
ν' : Measure ↑K
ν'_reg : ν'.Regular
ν'_fin : IsFiniteMeasure ν'
hν' : ∀ (g : ↑K →ᵇ ℝ), ∫ (x : ↑K), g x ∂μ' = ∫ (x : ↑K), g x ∂ν'
g : X →ᵇ ℝ
⊢ ∫ (x : X), g x ∂μ = ∫ (x : ↑K), (g.compContinuous { toFun := Subtype.val, continuous_toFun := ⋯ }) x ∂μ'

pp: case e'_3
X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : T2Space X
inst✝² : MeasurableSpace X
inst✝¹ : BorelSpace X
μ : Measure X
inst✝ : IsFiniteMeasure μ
K : Set X
hK : IsCompact K
h : μ Kᶜ = 0
μ' : Measure ↑K := Measure.comap Subtype.val μ
ν' : Measure ↑K
ν'_reg : ν'.Regular
ν'_fin : IsFiniteMeasure ν'
hν' : ∀ (g : ↑K →ᵇ ℝ), ∫ (x : ↑K), g x ∂μ' = ∫ (x : ↑K), g x ∂ν'
g : X →ᵇ ℝ
⊢ ∫ (x : X), g x ∂Measure.map Subtype.val ν' =
    ∫ (x : ↑K), (g.compContinuous { toFun := Subtype.val, continuous_toFun := ⋯ }) x ∂ν'

Tactic:
· simp only [BoundedContinuousFunction.compContinuous_apply, ContinuousMap.coe_mk]
    rw [← integral_map (φ := Subtype.val) (by fun_prop) (by fun_prop)]
    simp only [map_comap_subtype_coe hK.measurableSet, μ', Measure.restrict_eq_self_of_ae_mem h]

Goal state after:
case e'_3
X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : T2Space X
inst✝² : MeasurableSpace X
inst✝¹ : BorelSpace X
μ : Measure X
inst✝ : IsFiniteMeasure μ
K : Set X
hK : IsCompact K
h : μ Kᶜ = 0
μ' : Measure ↑K := Measure.comap Subtype.val μ
ν' : Measure ↑K
ν'_reg : ν'.Regular
ν'_fin : IsFiniteMeasure ν'
hν' : ∀ (g : ↑K →ᵇ ℝ), ∫ (x : ↑K), g x ∂μ' = ∫ (x : ↑K), g x ∂ν'
g : X →ᵇ ℝ
⊢ ∫ (x : X), g x ∂Measure.map Subtype.val ν' =
    ∫ (x : ↑K), (g.compContinuous { toFun := Subtype.val, continuous_toFun := ⋯ }) x ∂ν'
Module: Mathlib.MeasureTheory.Measure.IntegralCharFun

Goal state before:
pp: μ : Measure ℝ
r : ℝ
inst✝ : IsFiniteMeasure μ
hr : 0 < r
h_int : Integrable (Function.uncurry fun x y ↦ cexp (↑x * ↑y * I)) ((volume.restrict (Set.uIoc (-r) r)).prod μ)
⊢ ∫ (y : ℝ), ∫ (x : ℝ) in -r..r, cexp (↑x * ↑y * I) ∂μ =
    ∫ (y : ℝ), if r * y = 0 then 2 * ↑r else ↑y⁻¹ * ∫ (x : ℝ) in -(y * r)..y * r, cexp (↑x * I) ∂μ

Tactic:
congr with y

Goal state after:
case e_f
μ : Measure ℝ
r : ℝ
inst✝ : IsFiniteMeasure μ
hr : 0 < r
h_int : Integrable (Function.uncurry fun x y ↦ cexp (↑x * ↑y * I)) ((volume.restrict (Set.uIoc (-r) r)).prod μ)
y : ℝ
⊢ ∫ (x : ℝ) in -r..r, cexp (↑x * ↑y * I) =
    if r * y = 0 then 2 * ↑r else ↑y⁻¹ * ∫ (x : ℝ) in -(y * r)..y * r, cexp (↑x * I)
Module: Mathlib.MeasureTheory.Measure.IntegralCharFun

Goal state before:
pp: μ : Measure ℝ
r : ℝ
inst✝ : IsFiniteMeasure μ
hr : 0 < r
h_int : Integrable (Function.uncurry fun x y ↦ cexp (↑x * ↑y * I)) ((volume.restrict (Set.uIoc (-r) r)).prod μ)
⊢ ∫ (y : ℝ), if r * y = 0 then 2 * ↑r else ↑y⁻¹ * ∫ (x : ℝ) in -(y * r)..y * r, cexp (↑x * I) ∂μ =
    ∫ (x : ℝ), 2 * ↑r * ↑(sinc (r * x)) ∂μ

Tactic:
congr with y

Goal state after:
case e_f
μ : Measure ℝ
r : ℝ
inst✝ : IsFiniteMeasure μ
hr : 0 < r
h_int : Integrable (Function.uncurry fun x y ↦ cexp (↑x * ↑y * I)) ((volume.restrict (Set.uIoc (-r) r)).prod μ)
y : ℝ
⊢ (if r * y = 0 then 2 * ↑r else ↑y⁻¹ * ∫ (x : ℝ) in -(y * r)..y * r, cexp (↑x * I)) = 2 * ↑r * ↑(sinc (r * y))
Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls

Goal state before:
pp: x : EuclideanSpace ℝ (Fin 2)
r : ℝ
⊢ volume (ball x r) = ENNReal.ofReal r ^ 2 * ENNReal.ofReal π

Tactic:
volume_ball_fin_two x r

Goal state after:
x : EuclideanSpace ℝ (Fin 2)
r : ℝ
⊢ ENNReal.ofReal r ^ 2 * ENNReal.ofReal π = ENNReal.ofReal r ^ 2 * ENNReal.ofReal π
Module: Mathlib.MeasureTheory.Measure.TightNormed

Goal state before:

Tactic:
⨆ μ ∈ S, μ {x | r < ‖x‖}
    _ ≤ ⨆ μ ∈ S, μ (⋃ i, {x : E | r / √(Fintype.card ι) < ‖⟪b i, x⟫_𝕜‖}) := by
      gcongr with μ hμS
      intro x hx
      simp only [Set.mem_ofPred_eq, Set.mem_iUnion] at hx ⊢
      have hx' : r < √(Fintype.card ι) * ⨆ i, ‖⟪b i, x⟫_𝕜‖ :=
        hx.trans_le (b.norm_le_card_mul_iSup_norm_inner x)
      rw [← div_lt_iff₀' (by positivity)] at hx'
      by_contra! h_le
      exact lt_irrefl (r / √(Fintype.card ι)) (hx'.trans_le (ciSup_le h_le))
    _ ≤ ⨆ μ ∈ S, ∑ i, μ {x : E | r / √(Fintype.card ι) < ‖⟪b i, x⟫_𝕜‖} := by
      gcongr with μ hμS
      exact measure_iUnion_fintype_le μ _
    _ ≤ ∑ i, ⨆ μ ∈ S, μ {x | r / √(Fintype.card ι) < ‖⟪b i, x⟫_𝕜‖} := by
      refine iSup_le fun μ ↦ (iSup_le fun hμS ↦ ?_)
      gcongr with i
      exact le_biSup (fun μ ↦ μ {x | r / √(Fintype.card ι) < ‖⟪b i, x⟫_𝕜‖}) hμS

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

Goal state before:
pp: E : Type u_1
mE : MeasurableSpace E
S : Set (Measure E)
inst✝³ : NormedAddCommGroup E
𝕜 : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
h : Tendsto (fun r ↦ ⨆ μ ∈ S, μ {x | r < ‖x‖}) atTop (𝓝 0)
y : E
this : ProperSpace E
hy : ¬y = 0
h' : Tendsto (fun r ↦ ⨆ μ ∈ S, μ {x | r * ‖y‖⁻¹ < ‖x‖}) atTop (𝓝 0)
r : ℝ
μ : Measure E
x : E
hx : x ∈ {x | r < ‖⟪y, x⟫_𝕜‖}
⊢ x ∈ {x | r * ‖y‖⁻¹ < ‖x‖}

Tactic:
simp only [Set.mem_ofPred_eq] at hx ⊢

Goal state after:
E : Type u_1
mE : MeasurableSpace E
S : Set (Measure E)
inst✝³ : NormedAddCommGroup E
𝕜 : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
h : Tendsto (fun r ↦ ⨆ μ ∈ S, μ {x | r < ‖x‖}) atTop (𝓝 0)
y : E
this : ProperSpace E
hy : ¬y = 0
h' : Tendsto (fun r ↦ ⨆ μ ∈ S, μ {x | r * ‖y‖⁻¹ < ‖x‖}) atTop (𝓝 0)
r : ℝ
μ : Measure E
x : E
hx : r < ‖⟪y, x⟫_𝕜‖
⊢ r * ‖y‖⁻¹ < ‖x‖
Module: Mathlib.MeasureTheory.Measure.MeasuredSets

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s t : MeasuredSets μ
⊢ μ ↑s - μ ↑t ≤ edist s t

Tactic:
exact sub_le_edist s t

Goal state after:
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 = ⋃ i, ↑q ∩ s i

Tactic:
← Set.inter_iUnion

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) × T)
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h :
  ∀ (f : ((i : ι) → X i) →ᵇ ℝ) (g : T →ᵇ ℝ),
    ∫ (p : ((i : ι) → X i) × T), f p.1 * g p.2 ∂μ = ∫ (p : ((i : ι) → X i) × T), f p.1 * g p.2 ∂ν
this : Fintype ι
f : (i : ι) → X i →ᵇ ℝ
g : T →ᵇ ℝ
⊢ ∫ (p : ((i : ι) → X i) × T), (∏ i, (f i) (p.1 i)) * g p.2 ∂μ =
    ∫ (p : ((i : ι) → X i) × T), (∏ i, (f i) (p.1 i)) * g p.2 ∂ν

Tactic:
convert! h (∏ i, (f i).compContinuous ⟨Function.eval i, by fun_prop⟩) g <;> simp

Goal state after:
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✝² : Finite κ
μ ν : Measure (Z × ((i : κ) → Y i))
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h :
  ∀ (f : Z →ᵇ ℝ) (g : ((j : κ) → Y j) →ᵇ ℝ),
    ∫ (p : Z × ((i : κ) → Y i)), f p.1 * g p.2 ∂μ = ∫ (p : Z × ((i : κ) → Y i)), f p.1 * g p.2 ∂ν
this : Fintype κ
⊢ μ = ν

Tactic:
refine ext_of_integral_mul_prod_boundedContinuousFunction fun f g ↦ ?_

Goal state after:
κ : 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✝² : Finite κ
μ ν : Measure (Z × ((i : κ) → Y i))
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h :
  ∀ (f : Z →ᵇ ℝ) (g : ((j : κ) → Y j) →ᵇ ℝ),
    ∫ (p : Z × ((i : κ) → Y i)), f p.1 * g p.2 ∂μ = ∫ (p : Z × ((i : κ) → Y i)), f p.1 * g p.2 ∂ν
this : Fintype κ
f : Z →ᵇ ℝ
g : (j : κ) → Y j →ᵇ ℝ
⊢ ∫ (p : Z × ((j : κ) → Y j)), f p.1 * ∏ j, (g j) (p.2 j) ∂μ =
    ∫ (p : Z × ((j : κ) → Y j)), f p.1 * ∏ j, (g j) (p.2 j) ∂ν