mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Function.UnifTight

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup β
p : ℝ≥0∞
inst✝ : Subsingleton ι
hp_top : p ≠ ∞
f : ι → α → β
hf : ∀ (i : ι), MemLp (f i) p μ
ε : ℝ≥0
hε : 0 < ε
⊢ ∃ s, μ s ≠ ∞ ∧ ∀ (i : ι), eLpNorm (sᶜ.indicator (f i)) p μ ≤ ↑ε

Tactic:
by_cases hε_top : ε = ∞
  · exact ⟨∅, by simp, fun _ => hε_top.symm ▸ le_top⟩
  by_cases hι : Nonempty ι
  case neg => exact ⟨∅, (by simp), fun i => False.elim <| hι <| Nonempty.intro i⟩
  obtain ⟨i⟩ := hι
  obtain ⟨s, _, hμs, hfε⟩ := (hf i).exists_eLpNorm_indicator_compl_lt hp_top (coe_ne_zero.2 hε.ne')
  refine ⟨s, ne_of_lt hμs, fun j => ?_⟩
  convert! hfε.le

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 : E
ω₁ ω₂ : E → E →L[𝕜] F
γ : Path a b
⊢ curveIntegralFun (ω₁ + ω₂) γ = curveIntegralFun ω₁ γ + curveIntegralFun ω₂ γ

Tactic:
ext; simp [curveIntegralFun]

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 : E
γ : Path a b
⊢ curveIntegralFun 0 γ = 0

Tactic:
ext; simp [curveIntegralFun]

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 : E
ω : E → E →L[𝕜] F
γ : Path a b
⊢ curveIntegralFun (-ω) γ = -curveIntegralFun ω γ

Tactic:
ext; simp [curveIntegralFun]

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

Goal state before:
pp: a b : ℝ
f g : ℝ → ℝ
μ : Measure ℝ
hf : ContinuousOn f [[a, b]]
hg : IntervalIntegrable g μ a b
hg0 : ∀ x ∈ Ι a b, 0 ≤ g x
⊢ ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), 0 ≤ g x

Tactic:
rw [ae_restrict_iff' measurableSet_uIoc]

Goal state after:
a b : ℝ
f g : ℝ → ℝ
μ : Measure ℝ
hf : ContinuousOn f [[a, b]]
hg : IntervalIntegrable g μ a b
hg0 : ∀ x ∈ Ι a b, 0 ≤ g x
⊢ ∀ᵐ (x : ℝ) ∂μ, x ∈ Ι a b → 0 ≤ g x
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral

Goal state before:
pp: case hnorm
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
a b : E
C : ℝ
hfc : ContinuousOn f (segment ℝ a b)
hfd : ∀ t ∈ Ioo 0 1, LineDifferentiableAt ℝ f ((lineMap a b) t) (b - a)
hf' : ∀ᵐ (t : ℝ), t ∈ Ioo 0 1 → ‖lineDeriv ℝ f ((lineMap a b) t) (b - a)‖ ≤ C
g : ℝ → F := ⋯
hgc : ContinuousOn g (Icc 0 1)
hdg : ∀ t ∈ Ioo 0 1, HasDerivAt g (lineDeriv ℝ f ((lineMap a b) t) (b - a)) t
⊢ ∀ᵐ (t : ℝ), t ∈ Ioo 0 1 → ‖deriv g t‖ ≤ C

Tactic:
· exact hf'.mono fun t ht ht_mem ↦ by simpa only [(hdg t ht_mem).deriv] using ht ht_mem

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

Goal state before:
pp: case neg
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
h0 : ∀ (k : ℕ), ak (k + 1) - ak k = h
hab : 0 < b - a
hpos : 0 < h
hb : b = a + ↑N * h
k : ℕ
hk : k < N
h1 : a ≤ ak k
h2 : ak (k + 1) ≤ b
h3 : Set.Icc (ak k) (ak (k + 1)) ⊆ Set.Icc a b
h4 : ak k < ak (k + 1)
h5 :
  EqOn (_root_.derivWithin f (Set.Icc a b)) (_root_.derivWithin f (Set.Icc (ak k) (ak (k + 1))))
    (Set.Icc (ak k) (ak (k + 1)))
h6 :
  EqOn (iteratedDerivWithin 2 f (Set.Icc a b)) (iteratedDerivWithin 2 f (Set.Icc (ak k) (ak (k + 1))))
    (Set.Icc (ak k) (ak (k + 1)))
x : ℝ
hx : x ∉ Set.Icc (ak k) (ak (k + 1))
⊢ |iteratedDerivWithin 2 f (Set.Icc (ak k) (ak (k + 1))) x| ≤ ζ

Tactic:
· rw [iteratedDerivWithin_succ, derivWithin_zero_of_notMem_closure
        (by rwa [closure_Icc]), abs_zero]
      exact (abs_nonneg _).trans (fpp_bound 0)

Goal state after:
Module: Mathlib.MeasureTheory.Integral.TorusIntegral

Goal state before:
pp: n : ℕ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : (Fin (n + 1) → ℂ) → E
c : Fin (n + 1) → ℂ
R : Fin (n + 1) → ℝ
hf : TorusIntegrable f c R
i : Fin (n + 1)
e : ℝ × (Fin n → ℝ) ≃ᵐ (Fin (n + 1) → ℝ) := (MeasurableEquiv.piFinSuccAbove (fun x ↦ ℝ) i).symm
hem : MeasurePreserving (⇑e) volume volume
heπ : (⇑e ⁻¹' Icc 0 fun x ↦ 2 * π) = Icc 0 (2 * π) ×ˢ Icc 0 fun x ↦ 2 * π
⊢ ∫ (x : ℝ) in Icc 0 (2 * π),
      ∫ (y : Fin n → ℝ) in Icc 0 fun x ↦ 2 * π,
        (∏ i, ↑(R i) * cexp (↑(e (x, y) i) * I) * I) • f (torusMap c R (e (x, y))) =
    ∫ (θ : ℝ) in Icc 0 (2 * π),
      deriv (circleMap (c i) (R i)) θ •
        ∯ (y : Fin n → ℂ) in T(c ∘ i.succAbove, R ∘ i.succAbove), f (i.insertNth (circleMap (c i) (R i) θ) y)

pp: case hf
n : ℕ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : (Fin (n + 1) → ℂ) → E
c : Fin (n + 1) → ℂ
R : Fin (n + 1) → ℝ
hf : TorusIntegrable f c R
i : Fin (n + 1)
e : ℝ × (Fin n → ℝ) ≃ᵐ (Fin (n + 1) → ℝ) := (MeasurableEquiv.piFinSuccAbove (fun x ↦ ℝ) i).symm
hem : MeasurePreserving (⇑e) volume volume
heπ : (⇑e ⁻¹' Icc 0 fun x ↦ 2 * π) = Icc 0 (2 * π) ×ˢ Icc 0 fun x ↦ 2 * π
⊢ IntegrableOn (fun x ↦ (∏ i, ↑(R i) * cexp (↑(e x i) * I) * I) • f (torusMap c R (e x)))
    (Icc 0 (2 * π) ×ˢ Icc 0 fun x ↦ 2 * π) (volume.prod volume)

Tactic:
· refine setIntegral_congr_fun measurableSet_Icc fun θ _ => ?_
    simp +unfoldPartialApp only [e, torusIntegral, ← integral_smul,
      deriv_circleMap, i.prod_univ_succAbove _, smul_smul, torusMap, circleMap_zero]
    refine setIntegral_congr_fun measurableSet_Icc fun Θ _ => ?_
    simp only [MeasurableEquiv.piFinSuccAbove_symm_apply, i.insertNth_apply_same,
      i.insertNth_apply_succAbove, (· ∘ ·), Fin.insertNthEquiv, Equiv.coe_fn_mk]
    congr 2
    simp only [funext_iff, i.forall_iff_succAbove, circleMap, Fin.insertNth_apply_same,
      Fin.insertNth_apply_succAbove, imp_true_iff, and_self_iff]

Goal state after:
case hf
n : ℕ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : (Fin (n + 1) → ℂ) → E
c : Fin (n + 1) → ℂ
R : Fin (n + 1) → ℝ
hf : TorusIntegrable f c R
i : Fin (n + 1)
e : ℝ × (Fin n → ℝ) ≃ᵐ (Fin (n + 1) → ℝ) := (MeasurableEquiv.piFinSuccAbove (fun x ↦ ℝ) i).symm
hem : MeasurePreserving (⇑e) volume volume
heπ : (⇑e ⁻¹' Icc 0 fun x ↦ 2 * π) = Icc 0 (2 * π) ×ˢ Icc 0 fun x ↦ 2 * π
⊢ IntegrableOn (fun x ↦ (∏ i, ↑(R i) * cexp (↑(e x i) * I) * I) • f (torusMap c R (e x)))
    (Icc 0 (2 * π) ×ˢ Icc 0 fun x ↦ 2 * π) (volume.prod volume)
Module: Mathlib.MeasureTheory.MeasurableSpace.Card

Goal state before:
pp: case h1.h1.h2
α : Type u
s : Set (Set α)
i✝¹ i✝ i : Ordinal.{v}
IH : ∀ y < i, y ≤ ω_ 1 → #↑(generateMeasurableRec s y) ≤ max (#↑s) 2 ^ ℵ₀
hi : i ≤ ω_ 1
A : 𝔠 ≤ max (#↑s) 2 ^ ℵ₀
B : ℵ₀ ≤ max (#↑s) 2 ^ ℵ₀
C : #↑(⋃ j, ⋃ (_ : j < i), generateMeasurableRec s j) ≤ max (#↑s) 2 ^ ℵ₀
⊢ #↑{∅} ≤ max (#↑s) 2 ^ ℵ₀

Tactic:
rw [mk_singleton]

Goal state after:
case h1.h1.h2
α : Type u
s : Set (Set α)
i✝¹ i✝ i : Ordinal.{v}
IH : ∀ y < i, y ≤ ω_ 1 → #↑(generateMeasurableRec s y) ≤ max (#↑s) 2 ^ ℵ₀
hi : i ≤ ω_ 1
A : 𝔠 ≤ max (#↑s) 2 ^ ℵ₀
B : ℵ₀ ≤ max (#↑s) 2 ^ ℵ₀
C : #↑(⋃ j, ⋃ (_ : j < i), generateMeasurableRec s j) ≤ max (#↑s) 2 ^ ℵ₀
⊢ 1 ≤ max (#↑s) 2 ^ ℵ₀
Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : SecondCountableTopology E
μ : Measure E
inst✝ : IsFiniteMeasure μ
n : ℕ
t : E
hint : MemLp id (↑n) μ
x : Fin n → E
h : innerₗ E = ContinuousLinearMap.toLinearMap₁₂ (innerSL ℝ)
hint' : ∀ (k : ℕ), ↑k ≤ ↑n → Integrable (fun x ↦ ‖x‖ ^ k * ‖1 x‖) μ
⊢ (-((↑Real.pi)⁻¹ * 2⁻¹)) ^ n *
      fourierIntegral Real.fourierChar μ (ContinuousLinearMap.toLinearMap₁₂ (innerSL ℝ))
        (fun x_1 ↦ (fourierPowSMulRight (innerSL ℝ) 1 x_1 n) x) (-((Real.pi⁻¹ * 2⁻¹) • t)) =
    I ^ n * ∫ (y : E), (∏ i, ↑⟪y, x i⟫) * cexp (↑⟪y, t⟫ * I) ∂μ

Tactic:
simp only [fourierIntegral, Real.fourierChar, Circle.coe_exp, ofReal_mul,
    ofReal_ofNat, innerSL, map_neg, map_smul, ContinuousLinearMap.toLinearMap₁₂_apply_apply_apply,
    LinearMap.mkContinuous₂_apply, innerₛₗ_apply_apply, smul_eq_mul, neg_neg, AddChar.coe_mk,
    ofReal_inv, fourierPowSMulRight_apply, Pi.ofNat_apply, real_smul, ofReal_prod, mul_one,
    Circle.smul_def]

Goal state after:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : SecondCountableTopology E
μ : Measure E
inst✝ : IsFiniteMeasure μ
n : ℕ
t : E
hint : MemLp id (↑n) μ
x : Fin n → E
h : innerₗ E = ContinuousLinearMap.toLinearMap₁₂ (innerSL ℝ)
hint' : ∀ (k : ℕ), ↑k ≤ ↑n → Integrable (fun x ↦ ‖x‖ ^ k * ‖1 x‖) μ
⊢ (-((↑Real.pi)⁻¹ * 2⁻¹)) ^ n *
      ∫ (v : E),
        cexp (2 * ↑Real.pi * ((↑Real.pi)⁻¹ * 2⁻¹ * ↑⟪v, t⟫) * I) * ((-(2 * ↑Real.pi * I)) ^ n * ∏ i, ↑⟪v, x i⟫) ∂μ =
    I ^ n * ∫ (y : E), (∏ i, ↑⟪y, x i⟫) * cexp (↑⟪y, t⟫ * I) ∂μ
Module: Mathlib.MeasureTheory.Measure.DiracProba

Goal state before:
pp: case h
X : Type u_1
inst✝³ : MeasurableSpace X
inst✝² : TopologicalSpace X
inst✝¹ : OpensMeasurableSpace X
inst✝ : CompletelyRegularSpace X
x✝ : X
L : Filter X
h : ¬Tendsto id L (𝓝 x✝)
U : Set X
U_nhds : U ∈ 𝓝 x✝
hU : ∃ᶠ (x : X) in L, x ∉ U
Uint_nhds : interior U ∈ 𝓝 x✝
f : X →ᵇ ℝ≥0
fx_eq_one : f x✝ = 1
f_vanishes_outside : ∀ y ∈ (interior U)ᶜ, f y = 0
x : X
x_notin_U : x ∉ U
⊢ ↑0 ∉ Ioi 0

Tactic:
simp only [ENNReal.coe_zero, mem_Ioi, lt_self_iff_false, not_false_eq_true]

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
μ ν : Measure X
inst✝³ : LocallyCompactSpace X
inst✝² : ν.OuterRegular
inst✝¹ : IsFiniteMeasureOnCompacts ν
inst✝ : IsFiniteMeasureOnCompacts μ
hμν : ∀ (f : X →C_c ℝ), ∫ (x : X), f x ∂μ ≤ ∫ (x : X), f x ∂ν
K : Set X
hK : IsCompact K
ε : NNReal
hε : 0 < ε
hν : ν K < ∞
⊢ μ K ≤ ν K + ↑ε

Tactic:
have hνK : ν K ≠ ⊤ := hν.ne

Goal state after:
X : Type u_1
inst✝⁷ : TopologicalSpace X
inst✝⁶ : T2Space X
inst✝⁵ : MeasurableSpace X
inst✝⁴ : BorelSpace X
μ ν : Measure X
inst✝³ : LocallyCompactSpace X
inst✝² : ν.OuterRegular
inst✝¹ : IsFiniteMeasureOnCompacts ν
inst✝ : IsFiniteMeasureOnCompacts μ
hμν : ∀ (f : X →C_c ℝ), ∫ (x : X), f x ∂μ ≤ ∫ (x : X), f x ∂ν
K : Set X
hK : IsCompact K
ε : NNReal
hε : 0 < ε
hν : ν K < ∞
hνK : ν K ≠ ∞
⊢ μ K ≤ ν K + ↑ε
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
⊢ Continuous fun c ↦ ∫ (a : A), (H.pullback f (Function.invFun (⇑ψ) c)) a ∂μA

Tactic:
← H.isOpenQuotientMap.continuous_comp_iff,

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
inst✝¹ : IsTopologicalGroup C
inst✝ : LocallyCompactSpace B
f : CompactlySupportedContinuousMap B E
this : UniformSpace B := IsTopologicalGroup.rightUniformSpace B
⊢ Continuous ((fun c ↦ ∫ (a : A), (H.pullback f (Function.invFun (⇑ψ) c)) a ∂μA) ∘ ⇑ψ)
Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls

Goal state before:
pp: case inr
E : Type u_1
p : ℝ
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
hp : 0 < p
hE : Nontrivial E
this✝ : 0 < ↑(finrank ℝ E)
this :
  (∫ (y : ℝ) in Set.Ioi 0, y ^ (finrank ℝ E - 1) • Real.exp (-y ^ p)) / Real.Gamma (↑(finrank ℝ E) / p + 1) *
      ↑(finrank ℝ E) =
    1
⊢ μ (Metric.ball 0 1) = ENNReal.ofReal (μ.real (Metric.ball 0 1))

Tactic:
ofReal_measureReal _

Goal state after:
case inr
E : Type u_1
p : ℝ
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
hp : 0 < p
hE : Nontrivial E
this✝ : 0 < ↑(finrank ℝ E)
this :
  (∫ (y : ℝ) in Set.Ioi 0, y ^ (finrank ℝ E - 1) • Real.exp (-y ^ p)) / Real.Gamma (↑(finrank ℝ E) / p + 1) *
      ↑(finrank ℝ E) =
    1
⊢ μ (Metric.ball 0 1) = μ (Metric.ball 0 1)

E : Type u_1
p : ℝ
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
hp : 0 < p
hE : Nontrivial E
this✝ : 0 < ↑(finrank ℝ E)
this :
  (∫ (y : ℝ) in Set.Ioi 0, y ^ (finrank ℝ E - 1) • Real.exp (-y ^ p)) / Real.Gamma (↑(finrank ℝ E) / p + 1) *
      ↑(finrank ℝ E) =
    1
⊢ μ (Metric.ball 0 1) ≠ ∞
Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls

Goal state before:
pp: case e'_2
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
inst✝ : Nontrivial E
r : ℝ
F : Type u_1 := E
p : AddGroupNorm F := { toFun := g, map_zero' := h1, add_le' := h3, neg' := h2, eq_zero_of_map_eq_zero' := ⋯ }
this✝³ : NormedAddCommGroup F := p.toNormedAddCommGroup
this✝² : NormedSpace ℝ F := { toModule := inst✝⁷, norm_smul_le := ⋯ }
this✝¹ : TopologicalSpace F := PseudoMetricSpace.toUniformSpace.toTopologicalSpace
this✝ : MeasurableSpace F := borel F
this : BorelSpace F
φ : E ≃L[ℝ] F := (LinearEquiv.refl ℝ E).toContinuousLinearEquiv
ν : Measure F := map (⇑φ) μ
⊢ μ {x | g x ≤ r} = ν (Metric.closedBall 0 r)

Tactic:
rw [@Measure.map_apply E F mE _ μ φ _ _ measurableSet_closedBall]
    · congr!
      simp_rw [Metric.closedBall, dist_zero_right]
      rfl
    · refine @Continuous.measurable E F tE mE _ _ _ _ φ ?_
      exact @ContinuousLinearEquiv.continuous ℝ ℝ _ _ _ _ _ _ E tE _ F _ _ _ _ φ

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))
⊢ ∃ x ∈ {μ | μ.mass ≤ C ∧ ∀ (n : ℕ), μ (K n)ᶜ ≤ u n}, ↑f ≤ 𝓝 x

Tactic:
have B : (Measure.sum (fun n ↦ (ν n : Measure E))) univ ≤ C := by
    -- this follows from the corresponding result for finite sums, where we can use the
    -- continuity of the mass of a finite measure under weak convergence.
    simp only [MeasurableSet.univ, Measure.sum_apply]
    have : Tendsto (fun n ↦ ∑ i ∈ Finset.range (n + 1), (ν i : Measure E) univ) atTop
        (𝓝 (∑' i, (ν i : Measure E) univ)) :=
      (ENNReal.tendsto_nat_tsum _).comp (tendsto_add_atTop_nat 1)
    apply le_of_tendsto' this (fun n ↦ ?_)
    have : ∑ i ∈ Finset.range (n + 1), (ν i : Measure E) univ
        = (∑ i ∈ Finset.range (n + 1), ν i).toMeasure univ := by simp
    rw [this]
    suffices (∑ i ∈ Finset.range (n + 1), ν i).mass ≤ C by
      convert! ENNReal.coe_le_coe.2 this
      simp
    have : Tendsto (fun (μ : FiniteMeasure E) ↦
        (∑ i ∈ Finset.range (n + 1), μ.restrict (disjointed K i)).mass) f
        (𝓝 ((∑ i ∈ Finset.range (n + 1), ν i).mass)) := by
      apply Tendsto.mass
      exact tendsto_finsetSum _ (fun i hi ↦ hν i)
    apply le_of_tendsto this
    filter_upwards [hf] with μ hμ
    rw [I, restrict_mass]
    exact le_trans (apply_mono _ (subset_univ _)) hμ.1

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)
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
⊢ ∃ x ∈ {μ | μ.mass ≤ C ∧ ∀ (n : ℕ), μ (K n)ᶜ ≤ u n}, ↑f ≤ 𝓝 x
Module: Mathlib.MeasureTheory.Integral.CurveIntegral.Poincare

Goal state before:
pp: case refine_4
𝕜 : 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)
hφs : range ⇑φ ⊆ s
x : E
hx : x ∈ range ⇑φ
u : E
⊢ u ∈ tangentConeAt ℝ (range ⇑φ) x → ∀ v ∈ tangentConeAt ℝ (range ⇑φ) x, ((dω x) u) v = ((dω x) v) u

Tactic:
hu

Goal state after:
case refine_4
𝕜 : 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)
hφs : range ⇑φ ⊆ s
x : E
hx : x ∈ range ⇑φ
u : E
hu : u ∈ tangentConeAt ℝ (range ⇑φ) x
⊢ ∀ v ∈ tangentConeAt ℝ (range ⇑φ) x, ((dω x) u) v = ((dω x) v) u
Module: Mathlib.MeasureTheory.Measure.Prokhorov

Goal state before:
pp: case refine_2.inl
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 : NormalSpace E
this : (↑μ).InnerRegular
g : E → ℝ
g_cont : Continuous[inst✝², _] g
⊢ EqOn g 0 (K n) → 0 ≤ g → g ≤ 1 → ∫ (x : E), g x ∂↑μ ≤ ↑(u n)

Tactic:
gK

Goal state after:
case refine_2.inl
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 : NormalSpace E
this : (↑μ).InnerRegular
g : E → ℝ
g_cont : Continuous[inst✝², _] g
gK : EqOn g 0 (K n)
⊢ 0 ≤ g → g ≤ 1 → ∫ (x : E), g x ∂↑μ ≤ ↑(u n)
Module: Mathlib.MeasureTheory.Measure.SeparableMeasure

Goal state before:
pp: X : Type u_1
m : MeasurableSpace X
μ : Measure X
𝒜 : Set (Set X)
h𝒜 : μ.MeasureDense 𝒜
t : Set X
ht : t ∈ 𝒜
hμt : μ (∅ ∆ t) < ENNReal.ofReal 1
⊢ {s | s ∈ 𝒜 ∧ μ s ≠ ∞}.Nonempty

Tactic:
refine ⟨t, ht, ?_⟩

Goal state after:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
𝒜 : Set (Set X)
h𝒜 : μ.MeasureDense 𝒜
t : Set X
ht : t ∈ 𝒜
hμt : μ (∅ ∆ t) < ENNReal.ofReal 1
⊢ μ t ≠ ∞
Module: Mathlib.MeasureTheory.Measure.SeparableMeasure

Goal state before:
pp: X : Type u_1
m : MeasurableSpace X
μ : Measure X
𝒜 : Set (Set X)
h𝒜 : μ.MeasureDense 𝒜
s : Set (NullMeasurableSpace X μ)
hs : MeasurableSet s
hμs : μ.completion s ≠ ∞
ε : ℝ
ε_pos : 0 < ε
t : Set X
ht : t ∈ 𝒜
hμst : μ (toMeasurable μ s ∆ t) < ENNReal.ofReal ε
⊢ ∃ t ∈ 𝒜, μ.completion (s ∆ t) < ENNReal.ofReal ε

Tactic:
refine ⟨t, ht, ?_⟩

Goal state after:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
𝒜 : Set (Set X)
h𝒜 : μ.MeasureDense 𝒜
s : Set (NullMeasurableSpace X μ)
hs : MeasurableSet s
hμs : μ.completion s ≠ ∞
ε : ℝ
ε_pos : 0 < ε
t : Set X
ht : t ∈ 𝒜
hμst : μ (toMeasurable μ s ∆ t) < ENNReal.ofReal ε
⊢ μ.completion (s ∆ t) < ENNReal.ofReal ε