mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.ContinuousMap.CompactlySupported

Goal state before:
pp: case inl
α : Type u_2
inst✝ : TopologicalSpace α
f : α →C_c ℝ
a : ℝ
ha : a ≤ 0
x : α
hfx : 0 ≤ f x
⊢ max (a * f x) 0 = max (-a) 0 * max (-f x) 0

pp: case inr
α : Type u_2
inst✝ : TopologicalSpace α
f : α →C_c ℝ
a : ℝ
ha : a ≤ 0
x : α
hfx : f x ≤ 0
⊢ max (a * f x) 0 = max (-a) 0 * max (-f x) 0

Tactic:
· simp [mul_nonpos_iff, ha, hfx]

Goal state after:
case inr
α : Type u_2
inst✝ : TopologicalSpace α
f : α →C_c ℝ
a : ℝ
ha : a ≤ 0
x : α
hfx : f x ≤ 0
⊢ max (a * f x) 0 = max (-a) 0 * max (-f x) 0
Module: Mathlib.MeasureTheory.Integral.MeanValue

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
s : Set α
f g : α → ℝ
μ : Measure α
hs_conn : IsConnected s
hs_meas : MeasurableSet s
hf : ContinuousOn f s
hg : IntegrableOn g s μ
hfg : IntegrableOn (fun x ↦ f x * g x) s μ
hg0 : ∀ᵐ (x : α) ∂μ.restrict s, 0 ≤ g x
ρ : α → ENNReal := fun x ↦ ENNReal.ofReal (g x)
ν : Measure α := μ.withDensity ρ
hρ_ae : AEMeasurable ρ (μ.restrict s)
hρ_top : ∀ᵐ (x : α) ∂μ.restrict s, ρ x < ⊤
h_toReal_ae : (fun x ↦ (ρ x).toReal) =ᵐ[μ.restrict s] g
heq : ∫ (x : α) in s, f x * g x ∂μ = ∫ (x : α) in s, f x ∂ν
h : (∫ (x : α) in s, 1 ∂μ.withDensity fun x ↦ ρ x) = ∫ (x : α) in s, (ρ x).toReal • 1 ∂μ
⊢ ∫ (x : α) in s, (ρ x).toReal ∂μ = ∫ (x : α) in s, 1 ∂ν

Tactic:
by simp [ν, h]

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

Goal state before:
pp: case f_int
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
r : ENNReal
hr : r < μ U
K : Set X
KU : K ⊆ U
K_comp : IsCompact K
hK : r < μ K
f : X → ℝ
f_cont : Continuous f
fU : EqOn (⇑{ toFun := f, continuous_toFun := f_cont }) 0 Uᶜ
fK : EqOn (⇑{ toFun := f, continuous_toFun := f_cont }) 1 K
f_range : ∀ (x : X), { toFun := f, continuous_toFun := f_cont } x ∈ Icc 0 1
⊢ ∀ᵐ (ω : X) ∂μ, f ω ∈ Icc 0 1

Tactic:
filter_upwards [] with x using f_range x

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 + ε') ≤ ε
⊢ range ⇑f ⊆ Ioo a (a + (b - a))

Tactic:
simp [hab.2]

Goal state after:
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 ^ ℵ₀

pp: case 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 ^ ℵ₀
⊢ #↑(range fun f ↦ ⋃ n, ↑(f n)) ≤ max (#↑s) 2 ^ ℵ₀

Tactic:
· rw [mk_singleton]
    exact one_lt_aleph0.le.trans B

Goal state after:
case 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 ^ ℵ₀
⊢ #↑(range fun f ↦ ⋃ n, ↑(f n)) ≤ max (#↑s) 2 ^ ℵ₀
Module: Mathlib.Topology.Separation.CompletelyRegular

Goal state before:
pp: X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : T35Space X
a : X
⊢ ∀ ⦃a₂ : X⦄, stoneCechUnit a = stoneCechUnit a₂ → a = a₂

Tactic:
b

Goal state after:
X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : T35Space X
a b : X
⊢ stoneCechUnit a = stoneCechUnit b → a = b
Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic

Goal state before:
pp: case refine_1
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
mE : MeasurableSpace E
inst✝⁴ : BorelSpace E
inst✝³ : SecondCountableTopology E
inst✝² : CompleteSpace E
μ ν : Measure E
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h : charFunDual μ = charFunDual ν
⊢ ∀ (v : E), v ≠ 0 → (ContinuousLinearMap.toLinearMap₁₂ ⋯.toContinuousLinearMap) v ≠ 0

Tactic:
exact fun v hv ↦ DFunLike.ne_iff.mpr <| SeparatingDual.exists_ne_zero hv

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

Goal state before:
pp: Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : PseudoEMetricSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ ν : Measure Ω
hLP : levyProkhorovEDist μ ν = 0
s : Set Ω
s_mble : MeasurableSet s
h_finite : ∃ δ > 0, ν (thickening δ s) ≠ ∞
x : ℝ≥0∞
hx : x ∈ Ioo 0 1
⊢ x.toReal ∈ Ioi 0

Tactic:
exact toReal_pos hx.1.ne' <| ne_top_of_lt hx.2

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

Goal state before:
pp: α : Type u_1
inst✝³ : MeasurableSpace α
β : Type u_2
inst✝² : MeasurableSpace β
μ : ProbabilityMeasure α
ν : ProbabilityMeasure β
α' : Type u_3
inst✝¹ : MeasurableSpace α'
β' : Type u_4
inst✝ : MeasurableSpace β'
f : α → α'
g : β → β'
f_mble : Measurable f
g_mble : Measurable g
⊢ (μ.map ⋯).prod (ν.map ⋯) = (μ.prod ν).map ⋯

Tactic:
apply Subtype.ext
  simp only [val_eq_to_measure, toMeasure_prod, toMeasure_map]
  rw [Measure.map_prod_map _ _ f_mble g_mble]

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
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✝⁸ : MeasurableSpace A
inst✝⁷ : BorelSpace A
μA : Measure A
hμA : μA.IsHaarMeasure
inst✝⁶ : IsTopologicalGroup C
inst✝⁵ : LocallyCompactSpace B
inst✝⁴ : MeasurableSpace C
inst✝³ : BorelSpace C
μC : Measure C
hμC : μC.IsHaarMeasure
inst✝² : T2Space B
inst✝¹ : MeasurableSpace B
inst✝ : BorelSpace B
f : CompactlySupportedContinuousMap B ℝ
⊢ ∫ (b : B), f b ∂H.inducedMeasure μA μC = (H.integrate μA μC) f

Tactic:
apply RealRMK.integral_rieszMeasure

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
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✝⁹ : MeasurableSpace A
inst✝⁸ : BorelSpace A
μA : Measure A
hμA : μA.IsHaarMeasure
inst✝⁷ : IsTopologicalGroup C
inst✝⁶ : LocallyCompactSpace B
inst✝⁵ : MeasurableSpace C
inst✝⁴ : BorelSpace C
μC : Measure C
hμC : μC.IsHaarMeasure
inst✝³ : T2Space B
inst✝² : MeasurableSpace B
inst✝¹ : BorelSpace B
U : Set B
hU : IsOpen U
inst✝ : DiscreteTopology A
h✝ : μC Set.univ * μA {1} < (H.inducedMeasure μA μC) U
ho : 0 < μA {1}
ht : μA {1} < ⊤
K : Set B
hKU : K ⊆ U
hK : IsCompact K
f : C(B, ℝ)
hf1 : Set.EqOn (⇑f) 1 K
hf2 : IsCompact (tsupport ⇑f)
hf3 : tsupport ⇑f ⊆ U
hf4 : ∀ (x : B), f x ∈ Set.Icc 0 1
h :
  μC Set.univ * μA {1} <
    ENNReal.ofReal (∫ (c : C), ((H.pushforward μA) { toContinuousMap := f, hasCompactSupport' := hf2 }) c ∂μC)
hc : Set.InjOn (⇑ψ) U
b : B
a : A
ha : a ∈ Function.support fun a ↦ f (b * φ a)
⊢ ∀ ⦃y : A⦄, (y ∈ Function.support fun a ↦ f (b * φ a)) → a = y

Tactic:
b

Goal state after:
A : Type u_1
B : Type u_2
C : Type u_3
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✝⁹ : MeasurableSpace A
inst✝⁸ : BorelSpace A
μA : Measure A
hμA : μA.IsHaarMeasure
inst✝⁷ : IsTopologicalGroup C
inst✝⁶ : LocallyCompactSpace B
inst✝⁵ : MeasurableSpace C
inst✝⁴ : BorelSpace C
μC : Measure C
hμC : μC.IsHaarMeasure
inst✝³ : T2Space B
inst✝² : MeasurableSpace B
inst✝¹ : BorelSpace B
U : Set B
hU : IsOpen U
inst✝ : DiscreteTopology A
h✝ : μC Set.univ * μA {1} < (H.inducedMeasure μA μC) U
ho : 0 < μA {1}
ht : μA {1} < ⊤
K : Set B
hKU : K ⊆ U
hK : IsCompact K
f : C(B, ℝ)
hf1 : Set.EqOn (⇑f) 1 K
hf2 : IsCompact (tsupport ⇑f)
hf3 : tsupport ⇑f ⊆ U
hf4 : ∀ (x : B), f x ∈ Set.Icc 0 1
h :
  μC Set.univ * μA {1} <
    ENNReal.ofReal (∫ (c : C), ((H.pushforward μA) { toContinuousMap := f, hasCompactSupport' := hf2 }) c ∂μC)
hc : Set.InjOn (⇑ψ) U
b✝ : B
a : A
ha : a ∈ Function.support fun a ↦ f (b✝ * φ a)
b : A
⊢ (b ∈ Function.support fun a ↦ f (b✝ * φ a)) → a = b
Module: Mathlib.MeasureTheory.Measure.IntegralCharFun

Goal state before:
pp: E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
mE : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
μ : Measure E
inst✝ : IsProbabilityMeasure μ
L : StrongDual ℝ E
r : ℝ
hr : 0 < r
⊢ μ.real {x | r < |L x|} ≤ 2⁻¹ * r * ‖∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - charFunDual μ (t • L)‖

Tactic:
have : IsProbabilityMeasure (μ.map L) := Measure.isProbabilityMeasure_map (by fun_prop)
  convert! measureReal_abs_gt_le_integral_charFun (μ := μ.map L) hr with x
  · rw [map_measureReal_apply (by fun_prop)]
    · simp
    · exact MeasurableSet.preimage measurableSet_Ioi (by fun_prop)
  · rw [charFun_map_eq_charFunDual_smul]

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

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

Tactic:
have h₁ (x : ι → ℝ) : 0 ≤ ∑ i, |x i| ^ p := by positivity
  have h₂ : ∀ x : ι → ℝ, 0 ≤ (∑ i, |x i| ^ p) ^ (1 / p) := fun x => rpow_nonneg (h₁ x) _
  obtain hr | hr := le_or_gt r 0
  · have : {x : ι → ℝ | (∑ i, |x i| ^ p) ^ (1 / p) < r} = ∅ := by
      ext x
      refine ⟨fun hx => ?_, fun hx => hx.elim⟩
      exact not_le.mpr (lt_of_lt_of_le (Set.mem_ofPred.mp hx) hr) (h₂ x)
    rw [this, measure_empty, ← zero_eq_ofReal.mpr hr, zero_pow Fin.pos'.ne', zero_mul]
  · rw [← volume_sum_rpow_lt_one _ hp, ← ofReal_pow (le_of_lt hr), ← finrank_pi ℝ]
    convert! addHaar_smul_of_nonneg volume (le_of_lt hr) {x : ι → ℝ | ∑ i, |x i| ^ p < 1} using 2
    simp_rw [← Set.preimage_smul_inv₀ (ne_of_gt hr), Set.preimage_ofPred_eq, Pi.smul_apply,
      smul_eq_mul, abs_mul, mul_rpow (abs_nonneg _) (abs_nonneg _), abs_inv,
      inv_rpow (abs_nonneg _), ← Finset.mul_sum, abs_eq_self.mpr (le_of_lt hr),
      inv_mul_lt_iff₀ (rpow_pos_of_pos hr _), mul_one, ← rpow_lt_rpow_iff
      (rpow_nonneg (h₁ _) _) (le_of_lt hr) (by linarith : 0 < p), ← rpow_mul
      (h₁ _), div_mul_cancel₀ _ (ne_of_gt (by linarith) : p ≠ 0), Real.rpow_one]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace ℝ F
a b c : E
s : Set E
ω : E → E →L[𝕜] F
dω : E → E →L[ℝ] E →L[𝕜] F
hs : Convex ℝ s
hω : ∀ x ∈ s, HasFDerivWithinAt ω (dω x) s x
hdω : ∀ a ∈ s, ∀ x ∈ tangentConeAt ℝ s a, ∀ y ∈ tangentConeAt ℝ s a, ((dω a) x) y = ((dω a) y) x
ha : a ∈ s
hb : b ∈ s
hc : c ∈ s
⊢ ∫ᶜ (x : E) in Path.segment a b, ω x + ∫ᶜ (x : E) in Path.segment b c, ω x = ∫ᶜ (x : E) in Path.segment a c, ω x

Tactic:
set φ := ContinuousMap.Homotopy.affine (Path.segment a b : C(I, E)) (Path.segment a c)

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
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)
⊢ ∫ᶜ (x : E) in Path.segment a b, ω x + ∫ᶜ (x : E) in Path.segment b c, ω x = ∫ᶜ (x : E) in Path.segment a c, ω x
Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls

Goal state before:
pp: case e'_3
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : Nonempty ι
p : ℝ
hp : 1 ≤ p
r : ℝ
h₁ : ∀ (x : ι → ℂ), 0 ≤ ∑ i, ‖x i‖ ^ p
h₂ : ∀ (x : ι → ℂ), 0 ≤ (∑ i, ‖x i‖ ^ p) ^ (1 / p)
hr : 0 < r
⊢ ENNReal.ofReal (r ^ (2 * card ι)) = ENNReal.ofReal (r ^ finrank ℝ (ι → ℂ))

Tactic:
simp_rw [finrank_pi_fintype ℝ, Complex.finrank_real_complex, Finset.sum_const, smul_eq_mul,
        mul_comm, Fintype.card]

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

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : ℕ → Measure E
inst✝ : ∀ (i : ℕ), IsProbabilityMeasure (μ i)
f : E → ℂ
hf : ContinuousAt f 0
h : ∀ (t : E), Tendsto (fun n ↦ charFun (μ n) t) atTop (𝓝 (f t))
z : E
hz : ‖z‖ = 1
h_le_4 : ∀ (n : ℕ) (r : ℝ), 0 < r → 2⁻¹ * r * ‖∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - charFun (μ n) (t • z)‖ ≤ 4
h_le :
  ∀ (n : ℕ) (r : ℝ),
    0 < r → (μ n).real {x | r < |⟪z, x⟫|} ≤ 2⁻¹ * r * ‖∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - charFun (μ n) (t • z)‖
r : ℝ
hr : 0 < r
⊢ limsup (fun n ↦ (μ n).real {x | r < |⟪z, x⟫|}) atTop ≤
    limsup (fun n ↦ 2⁻¹ * r * ‖∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - charFun (μ n) (t • z)‖) atTop

Tactic:
refine limsup_le_limsup (.of_forall fun n ↦ h_le n r hr) ?_ ?_

Goal state after:
case refine_1
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : ℕ → Measure E
inst✝ : ∀ (i : ℕ), IsProbabilityMeasure (μ i)
f : E → ℂ
hf : ContinuousAt f 0
h : ∀ (t : E), Tendsto (fun n ↦ charFun (μ n) t) atTop (𝓝 (f t))
z : E
hz : ‖z‖ = 1
h_le_4 : ∀ (n : ℕ) (r : ℝ), 0 < r → 2⁻¹ * r * ‖∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - charFun (μ n) (t • z)‖ ≤ 4
h_le :
  ∀ (n : ℕ) (r : ℝ),
    0 < r → (μ n).real {x | r < |⟪z, x⟫|} ≤ 2⁻¹ * r * ‖∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - charFun (μ n) (t • z)‖
r : ℝ
hr : 0 < r
⊢ IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) atTop fun n ↦ (μ n).real {x | r < |⟪z, x⟫|}

case refine_2
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : ℕ → Measure E
inst✝ : ∀ (i : ℕ), IsProbabilityMeasure (μ i)
f : E → ℂ
hf : ContinuousAt f 0
h : ∀ (t : E), Tendsto (fun n ↦ charFun (μ n) t) atTop (𝓝 (f t))
z : E
hz : ‖z‖ = 1
h_le_4 : ∀ (n : ℕ) (r : ℝ), 0 < r → 2⁻¹ * r * ‖∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - charFun (μ n) (t • z)‖ ≤ 4
h_le :
  ∀ (n : ℕ) (r : ℝ),
    0 < r → (μ n).real {x | r < |⟪z, x⟫|} ≤ 2⁻¹ * r * ‖∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - charFun (μ n) (t • z)‖
r : ℝ
hr : 0 < r
⊢ IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) atTop fun n ↦
    2⁻¹ * r * ‖∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - charFun (μ n) (t • z)‖
Module: Mathlib.MeasureTheory.Measure.ResolventTransform

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra ℝ A
inst✝ : NormedAlgebra 𝕜 A
m𝕜 : MeasurableSpace 𝕜
x✝ : A
⊢ resolventTransform 0 x✝ = 0 x✝

Tactic:
simp [resolventTransform_def]

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

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝⁵ : NormedField 𝕜
inst✝⁴ : NormedRing A
inst✝³ : NormedAlgebra ℝ A
inst✝² : NormedAlgebra 𝕜 A
m𝕜 : MeasurableSpace 𝕜
inst✝¹ : MeasurableSingletonClass 𝕜
inst✝ : CompleteSpace A
x : 𝕜
a : A
⊢ resolventTransform (dirac x) a = resolvent a x

Tactic:
simp [resolventTransform_def]

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

Goal state before:
pp: case h
E : Type u_1
inst✝³ : MeasurableSpace E
inst✝² : TopologicalSpace E
inst✝¹ : T2Space E
inst✝ : BorelSpace E
S : Set (ProbabilityMeasure E)
hS : IsTightMeasureSet {x | ∃ μ ∈ S, ↑μ = x}
u : ℕ → ℝ≥0
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
K : ℕ → Set E
K_comp : ∀ (n : ℕ), IsCompact (K n)
hK : ∀ (n : ℕ), ∀ μ ∈ S, μ (K n)ᶜ ≤ u n
K' : ℕ → Set E := fun n ↦ ⋃ i ∈ Iic n, K i
a : ℕ
⊢ ∀ ⦃b : ℕ⦄, a ≤ b → ∀ i ≤ a, K i ⊆ ⋃ i, ⋃ (_ : i ≤ b), K i

Tactic:
b

Goal state after:
case h
E : Type u_1
inst✝³ : MeasurableSpace E
inst✝² : TopologicalSpace E
inst✝¹ : T2Space E
inst✝ : BorelSpace E
S : Set (ProbabilityMeasure E)
hS : IsTightMeasureSet {x | ∃ μ ∈ S, ↑μ = x}
u : ℕ → ℝ≥0
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
K : ℕ → Set E
K_comp : ∀ (n : ℕ), IsCompact (K n)
hK : ∀ (n : ℕ), ∀ μ ∈ S, μ (K n)ᶜ ≤ u n
K' : ℕ → Set E := fun n ↦ ⋃ i ∈ Iic n, K i
a b : ℕ
⊢ a ≤ b → ∀ i ≤ a, K i ⊆ ⋃ i, ⋃ (_ : i ≤ b), K i
Module: Mathlib.MeasureTheory.SpecificCodomains.WithLp

Goal state before:
pp: X : Type u_1
mX : MeasurableSpace X
μ : Measure X
p q : ℝ≥0∞
inst✝² : Fact (1 ≤ q)
E : Type u_2
F : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
f : X → WithLp q (E × F)
⊢ MemLp f p μ ↔ MemLp (fun x ↦ (f x).fst) p μ ∧ MemLp (fun x ↦ (f x).snd) p μ

Tactic:
← WithLp.ofLp_fst,

Goal state after:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
p q : ℝ≥0∞
inst✝² : Fact (1 ≤ q)
E : Type u_2
F : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
f : X → WithLp q (E × F)
⊢ MemLp f p μ ↔ MemLp (fun x ↦ (f x).ofLp.1) p μ ∧ MemLp (fun x ↦ (f x).snd) p μ
Module: Mathlib.MeasureTheory.VectorMeasure.Variation.Basic

Goal state before:
pp: X : Type u_1
V : Type u_2
mX : MeasurableSpace X
inst✝² : TopologicalSpace V
inst✝¹ : ENormedAddCommMonoid V
inst✝ : T2Space V
μ : VectorMeasure X V
s : Set X
m : Measure X
hs : MeasurableSet s
h : ∀ (E : Set X), MeasurableSet E → E ⊆ s → ‖μ E‖ₑ ≤ m E
i : Finpartition ⟨s, ⋯⟩
a : Subtype MeasurableSet
ha : a ∈ ↑i.parts
⊢ ∀ ⦃y : Subtype MeasurableSet⦄, y ∈ ↑i.parts → a ≠ y → Function.onFun Disjoint Subtype.val a y

Tactic:
b

Goal state after:
X : Type u_1
V : Type u_2
mX : MeasurableSpace X
inst✝² : TopologicalSpace V
inst✝¹ : ENormedAddCommMonoid V
inst✝ : T2Space V
μ : VectorMeasure X V
s : Set X
m : Measure X
hs : MeasurableSet s
h : ∀ (E : Set X), MeasurableSet E → E ⊆ s → ‖μ E‖ₑ ≤ m E
i : Finpartition ⟨s, ⋯⟩
a : Subtype MeasurableSet
ha : a ∈ ↑i.parts
b : Subtype MeasurableSet
⊢ b ∈ ↑i.parts → a ≠ b → Function.onFun Disjoint Subtype.val a b
Module: Mathlib.MeasureTheory.VectorMeasure.Variation.Basic

Goal state before:
pp: case a
X : Type u_1
V : Type u_2
mX : MeasurableSpace X
inst✝² : TopologicalSpace V
inst✝¹ : ENormedAddCommMonoid V
inst✝ : T2Space V
μ : VectorMeasure X V
s : Set X
hs : MeasurableSet s
⊢ (μ.restrict s).variation ≤ μ.variation.restrict s

Tactic:
apply variation_le_of_forall_enorm_le (fun t ht ↦ ?_)

Goal state after:
X : Type u_1
V : Type u_2
mX : MeasurableSpace X
inst✝² : TopologicalSpace V
inst✝¹ : ENormedAddCommMonoid V
inst✝ : T2Space V
μ : VectorMeasure X V
s : Set X
hs : MeasurableSet s
t : Set X
ht : MeasurableSet t
⊢ ‖(μ.restrict s) t‖ₑ ≤ (μ.variation.restrict s) t
Module: Mathlib.MeasureTheory.VectorMeasure.Variation.Basic

Goal state before:
pp: case a
X : Type u_1
V : Type u_2
mX : MeasurableSpace X
inst✝² : TopologicalSpace V
inst✝¹ : ENormedAddCommMonoid V
inst✝ : T2Space V
μ : VectorMeasure X V
s : Set X
hs : MeasurableSet s
⊢ (μ.restrict s).variation ≤ μ.variation.restrict s

pp: case a
X : Type u_1
V : Type u_2
mX : MeasurableSpace X
inst✝² : TopologicalSpace V
inst✝¹ : ENormedAddCommMonoid V
inst✝ : T2Space V
μ : VectorMeasure X V
s : Set X
hs : MeasurableSet s
⊢ μ.variation.restrict s ≤ (μ.restrict s).variation

Tactic:
· apply variation_le_of_forall_enorm_le (fun t ht ↦ ?_)
    simp only [ht, Measure.restrict_apply, VectorMeasure.restrict_apply, hs]
    apply enorm_measure_le_variation

Goal state after:
case a
X : Type u_1
V : Type u_2
mX : MeasurableSpace X
inst✝² : TopologicalSpace V
inst✝¹ : ENormedAddCommMonoid V
inst✝ : T2Space V
μ : VectorMeasure X V
s : Set X
hs : MeasurableSet s
⊢ μ.variation.restrict s ≤ (μ.restrict s).variation
Module: Mathlib.MeasureTheory.VectorMeasure.Variation.Basic

Goal state before:
pp: X : Type u_1
V : Type u_2
mX : MeasurableSpace X
inst✝³ : TopologicalSpace V
inst✝² : ENormedAddCommMonoid V
inst✝¹ : T2Space V
μ : VectorMeasure X V
Y : Type u_3
inst✝ : MeasurableSpace Y
φ : X → Y
hφ : MeasurableEmbedding φ
s : Set Y
hs : MeasurableSet s
this : (μ.map φ).variation s = (μ.map φ).variation (s ∩ Set.range φ)
⊢ μ.variation (φ ⁻¹' s) ≤ (Measure.comap φ (μ.map φ).variation) (φ ⁻¹' s)

Tactic:
apply variation_le_of_forall_enorm_le (fun t ht ↦ ?_)

Goal state after:
X : Type u_1
V : Type u_2
mX : MeasurableSpace X
inst✝³ : TopologicalSpace V
inst✝² : ENormedAddCommMonoid V
inst✝¹ : T2Space V
μ : VectorMeasure X V
Y : Type u_3
inst✝ : MeasurableSpace Y
φ : X → Y
hφ : MeasurableEmbedding φ
s : Set Y
hs : MeasurableSet s
this : (μ.map φ).variation s = (μ.map φ).variation (s ∩ Set.range φ)
t : Set X
ht : MeasurableSet t
⊢ ‖μ t‖ₑ ≤ (Measure.comap φ (μ.map φ).variation) t
Module: Mathlib.MeasureTheory.VectorMeasure.AddContent

Goal state before:
pp: α : Type u_1
hα : MeasurableSpace α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
μ : Measure α
m : Set α → E
hm : ∀ (s : Set α), ‖m s‖ₑ ≤ μ s
inst✝ : IsFiniteMeasure μ
h'm : ∀ (s t : Set α), MeasurableSet s → MeasurableSet t → Disjoint s t → m (s ∪ t) = m s + m t
h''m : ∀ (s : Set α), ¬MeasurableSet s → m s = 0
f : ℕ → Set α
f_meas : ∀ (i : ℕ), MeasurableSet (f i)
f_disj : Pairwise (Function.onFun Disjoint f)
⊢ ∑' (x : ℕ), ‖m (f x)‖ₑ < ⊤

Tactic:
calc ∑' i, ‖m (f i)‖ₑ
      _ ≤ ∑' i, μ (f i) := by gcongr; apply hm
      _ = μ (⋃ i, f i) := (measure_iUnion f_disj f_meas).symm
      _ < ⊤ := measure_lt_top μ (⋃ i, f i)

Goal state after:
Module: Mathlib.MeasureTheory.VectorMeasure.BoundedVariation

Goal state before:
pp: case pos
α : Type u_1
inst✝⁸ : LinearOrder α
inst✝⁷ : DenselyOrdered α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : OrderTopology α
inst✝⁴ : SecondCountableTopology α
inst✝³ : CompactIccSpace α
hα : MeasurableSpace α
inst✝² : BorelSpace α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : CompleteSpace E
f : α → E
a : α
hf : BoundedVariationOn f univ
ha : IsBot a
h : ∃ x, IsBot x
heqa : h.choose = a
A : ⋯.choose {a} = 0
⊢ ⋯.choose ∈ {a}

Tactic:
simp [heqa]

Goal state after:
Module: Mathlib.MeasureTheory.VectorMeasure.SetIntegral

Goal state before:
pp: X : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
mX : MeasurableSpace X
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedAddCommGroup G
μ : VectorMeasure X F
f : X → E
s t : Set X
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedSpace ℝ F
inst✝ : NormedSpace ℝ G
B : E →L[ℝ] F →L[ℝ] G
hs : MeasurableSet s
ht : MeasurableSet t
⊢ ∫ᵛ (x : X) in s, t.indicator f x ∂[B; μ] = ∫ᵛ (x : X) in s ∩ t, f x ∂[B; μ]

Tactic:
by
  rw [integral_indicator ht, μ.restrict_restrict ht hs, Set.inter_comm]

Goal state after:
Module: Mathlib.MeasureTheory.VectorMeasure.BoundedVariation

Goal state before:
pp: α : Type u_1
inst✝⁸ : LinearOrder α
inst✝⁷ : DenselyOrdered α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : OrderTopology α
inst✝⁴ : SecondCountableTopology α
inst✝³ : CompactIccSpace α
hα : MeasurableSpace α
inst✝² : BorelSpace α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : CompleteSpace E
f : α → E
hf : BoundedVariationOn f univ
a : α
this : Nonempty α
hlim : Tendsto f atBot (𝓝 (atBot.limUnder f))
u : ℕ → α
u_anti : Antitone u
hu : Tendsto u atTop atBot
x : α
hx : x ≤ a
⊢ x ∈ ⋃ n, Icc (u n) a

Tactic:
simpa [hx] using (hu.eventually (Iic_mem_atBot x)).exists

Goal state after: