mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: case refine_2.refine_2
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ
F : α → ℝ
hf : ∀ (n : ℕ), Integrable (f n) μ
hF : Integrable F μ
h_mono : ∀ᵐ (x : α) ∂μ, Monotone fun n ↦ f n x
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (F x))
f' : ℕ → α → ℝ := fun n x ↦ f n x - f 0 x
hf'_nonneg : ∀ (i : ℕ), ∀ᵐ (a : α) ∂μ, 0 ≤ f' i a
hf'_meas : ∀ (n : ℕ), Integrable (f' n) μ
hF_ge : 0 ≤ᵐ[μ] fun x ↦ (F - f 0) x
h_cont : ContinuousAt ENNReal.toReal (∫⁻ (a : α), ENNReal.ofReal ((F - f 0) a) ∂μ)
⊢ ∀ᵐ (x : α) ∂μ, Monotone fun n ↦ ENNReal.ofReal (f' n x)

Tactic:
filter_upwards [h_mono] with x hx n m hnm

Goal state after:
α : Type u_1
m✝ : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ
F : α → ℝ
hf : ∀ (n : ℕ), Integrable (f n) μ
hF : Integrable F μ
h_mono : ∀ᵐ (x : α) ∂μ, Monotone fun n ↦ f n x
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (F x))
f' : ℕ → α → ℝ := fun n x ↦ f n x - f 0 x
hf'_nonneg : ∀ (i : ℕ), ∀ᵐ (a : α) ∂μ, 0 ≤ f' i a
hf'_meas : ∀ (n : ℕ), Integrable (f' n) μ
hF_ge : 0 ≤ᵐ[μ] fun x ↦ (F - f 0) x
h_cont : ContinuousAt ENNReal.toReal (∫⁻ (a : α), ENNReal.ofReal ((F - f 0) a) ∂μ)
x : α
hx : Monotone fun n ↦ f n x
n m : ℕ
hnm : n ≤ m
⊢ (fun n ↦ ENNReal.ofReal (f' n x)) n ≤ (fun n ↦ ENNReal.ofReal (f' n x)) m
Module: Mathlib.Topology.Algebra.ContinuousAffineMap

Goal state before:
pp: case refine_1
R : Type u_1
V : Type u_2
W : Type u_3
P : Type u_4
Q : Type u_5
inst✝¹² : Ring R
inst✝¹¹ : AddCommGroup V
inst✝¹⁰ : Module R V
inst✝⁹ : TopologicalSpace P
inst✝⁸ : AddTorsor V P
inst✝⁷ : AddCommGroup W
inst✝⁶ : Module R W
inst✝⁵ : TopologicalSpace Q
inst✝⁴ : AddTorsor W Q
inst✝³ : TopologicalSpace V
inst✝² : IsTopologicalAddTorsor P
inst✝¹ : TopologicalSpace W
inst✝ : IsTopologicalAddTorsor Q
f : P →ᴬ[R] Q
h : f.contLinear = 0
x✝ : V
⊢ (↑f).linear x✝ = 0 x✝

Tactic:
rw [← coe_contLinear_eq_linear, h]; rfl

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

Goal state before:
pp: case f_nn
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ
F : α → ℝ
hf_int : ∀ (n : ℕ), Integrable (f n) μ
hF_int : Integrable F μ
hf_tendsto : Tendsto (fun i ↦ ∫ (a : α), f i a ∂μ) atTop (𝓝 (∫ (a : α), F a ∂μ))
hf_mono : ∀ᵐ (a : α) ∂μ, Monotone fun i ↦ f i a
hf_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f i a ≤ F a
f' : ℕ → α → ℝ≥0∞ := fun n a ↦ ENNReal.ofReal (f n a - f 0 a)
F' : α → ℝ≥0∞ := fun a ↦ ENNReal.ofReal (F a - f 0 a)
i : ℕ
⊢ 0 ≤ᵐ[μ] fun a ↦ f i a - f 0 a

Tactic:
· filter_upwards [hf_mono] with a h_mono
      simp [h_mono zero_le]

Goal state after:
Module: Mathlib.Analysis.Normed.Module.RieszLemma

Goal state before:
pp: F : Type u_3
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x : F
s : Set F
hx : x ∈ s
⊢ closedBall x (infDist x sᶜ) ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s

Tactic:
rcases eq_or_ne (infDist x sᶜ) 0 with h₀ | h₀
  · rw [h₀, closedBall_zero']
    exact closure_mono (singleton_subset_iff.2 hx)
  · rw [← closure_ball x h₀]
    exact closure_mono ball_infDist_compl_subset

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Bochner.SumMeasure

Goal state before:
pp: ι : Type u_1
X : Type u_2
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
μ : ι → Measure X
f : X → E
inst✝ : NormedSpace ℝ E
hf : Integrable f (Measure.sum μ)
hfi : ∀ (i : ι), Integrable f (μ i)
ε : ℝ≥0
ε0 : 0 < ↑ε
hf_lt : ∫⁻ (x : X), ‖f x‖ₑ ∂Measure.sum μ < ∞
hmem : ∀ᶠ (y : ℝ≥0∞) in 𝓝 (∫⁻ (x : X), ‖f x‖ₑ ∂Measure.sum μ), ∫⁻ (x : X), ‖f x‖ₑ ∂Measure.sum μ < y + ↑ε
s : Finset ι
hs : ∫⁻ (x : X), ‖f x‖ₑ ∂Measure.sum μ < ∑ b ∈ s, (fun i ↦ ∫⁻ (a : X), ‖f a‖ₑ ∂μ i) b + ↑ε
ν : Measure X
hν : ∑ i ∈ s, μ i + ν = Measure.sum μ
⊢ ↑(nndist (∫ (x : X), f x ∂∑ i ∈ s, μ i) (∫ (x : X), f x ∂Measure.sum μ)) < ↑ε

Tactic:
← hν

Goal state after:
ι : Type u_1
X : Type u_2
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
μ : ι → Measure X
f : X → E
inst✝ : NormedSpace ℝ E
hf : Integrable f (Measure.sum μ)
hfi : ∀ (i : ι), Integrable f (μ i)
ε : ℝ≥0
ε0 : 0 < ↑ε
hf_lt : ∫⁻ (x : X), ‖f x‖ₑ ∂Measure.sum μ < ∞
hmem : ∀ᶠ (y : ℝ≥0∞) in 𝓝 (∫⁻ (x : X), ‖f x‖ₑ ∂Measure.sum μ), ∫⁻ (x : X), ‖f x‖ₑ ∂Measure.sum μ < y + ↑ε
s : Finset ι
hs : ∫⁻ (x : X), ‖f x‖ₑ ∂Measure.sum μ < ∑ b ∈ s, (fun i ↦ ∫⁻ (a : X), ‖f a‖ₑ ∂μ i) b + ↑ε
ν : Measure X
hν : ∑ i ∈ s, μ i + ν = Measure.sum μ
⊢ ↑(nndist (∫ (x : X), f x ∂∑ i ∈ s, μ i) (∫ (x : X), f x ∂(∑ i ∈ s, μ i + ν))) < ↑ε
Module: Mathlib.Topology.Algebra.Indicator

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f : α → β
s : Set α
inst✝ : One β
hf : ContinuousOn f (interior s)
x : α
hx : x ∉ frontier s
⊢ ContinuousAt (s.mulIndicator f) x

Tactic:
← Set.mem_compl_iff,

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f : α → β
s : Set α
inst✝ : One β
hf : ContinuousOn f (interior s)
x : α
hx : x ∈ (frontier s)ᶜ
⊢ ContinuousAt (s.mulIndicator f) x
Module: Mathlib.Topology.ContinuousMap.Bounded.Basic

Goal state before:
pp: case neg
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : PseudoMetricSpace β
f g : α →ᵇ β
C : ℝ
inst✝ : CompactSpace α
C0 : 0 < C
h : ¬Nonempty α
⊢ (∀ (x : α), dist (f x) (g x) < C) → dist f g < C

Tactic:
rintro -

Goal state after:
case neg
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : PseudoMetricSpace β
f g : α →ᵇ β
C : ℝ
inst✝ : CompactSpace α
C0 : 0 < C
h : ¬Nonempty α
⊢ dist f g < C
Module: Mathlib.Topology.MetricSpace.ThickenedIndicator

Goal state before:
pp: case h
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x y : α
key : ∀ (x : α), thickenedIndicatorAux δ E x ≤ 1
⊢ ↑(thickenedIndicatorAux δ E x).toNNReal + ↑(thickenedIndicatorAux δ E y).toNNReal ≤ 1 + 1

Tactic:
apply add_le_add <;>
      · norm_cast
        exact (toNNReal_le_toNNReal (lt_of_le_of_lt (key _) one_lt_top).ne one_ne_top).mpr (key _)

Goal state after:
Module: Mathlib.Topology.MetricSpace.ThickenedIndicator

Goal state before:
pp: α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x : α
x_mem : x ∈ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E
⊢ (thickenedIndicator δ_pos E) x = 1

Tactic:
thickenedIndicator_apply,

Goal state after:
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x : α
x_mem : x ∈ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E
⊢ (thickenedIndicatorAux δ E x).toNNReal = 1
Module: Mathlib.Topology.MetricSpace.ThickenedIndicator

Goal state before:
pp: α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x : α
x_out : x ∉ thickening δ E
⊢ (thickenedIndicator δ_pos E) x = 0

Tactic:
thickenedIndicator_apply,

Goal state after:
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x : α
x_out : x ∉ thickening δ E
⊢ (thickenedIndicatorAux δ E x).toNNReal = 0
Module: Mathlib.Topology.MetricSpace.ThickenedIndicator

Goal state before:
pp: α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x y : α
h : infEDist x E ≤ infEDist y E
⊢ ENNReal.ofReal |↑((thickenedIndicator δ_pos E) x) - ↑((thickenedIndicator δ_pos E) y)| ≤ ↑δ.toNNReal⁻¹ * edist x y

Tactic:
thickenedIndicator_apply,

Goal state after:
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x y : α
h : infEDist x E ≤ infEDist y E
⊢ ENNReal.ofReal |↑(thickenedIndicatorAux δ E x).toNNReal - ↑(thickenedIndicatorAux δ E y).toNNReal| ≤
    ↑δ.toNNReal⁻¹ * edist x y
Module: Mathlib.MeasureTheory.Integral.SetToL1

Goal state before:
pp: α : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C C' : ℝ
c : ℝ≥0
hT : DominatedFinMeasAdditive μ T C
hT_smul : DominatedFinMeasAdditive (c • μ) T C'
f : α → E
⊢ setToFun μ T hT f = setToFun (c • μ) T hT_smul f

Tactic:
by
  rw! [ENNReal.smul_def]
  apply setToFun_congr_smul_measure _ (by simp)

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

Goal state before:
pp: case pos
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
r : ℝ≥0
hfint : Integrable f μ
hfint' : ∫ (a : α), max (-f a) 0 ∂μ ≤ ∫ (a : α), max (f a) 0 ∂μ
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ ↑r
hr : ¬r = 0
hμ this : IsFiniteMeasure μ
hposbdd : ∫ (ω : α), max (f ω) 0 ∂μ ≤ μ.real univ • ↑r
⊢ ∫ (a : α), max (f a) 0 ∂μ + ∫ (a : α), max (f a) 0 ∂μ ≤ 2 * (μ univ).toReal * ↑r

Tactic:
← two_mul,

Goal state after:
case pos
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
r : ℝ≥0
hfint : Integrable f μ
hfint' : ∫ (a : α), max (-f a) 0 ∂μ ≤ ∫ (a : α), max (f a) 0 ∂μ
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ ↑r
hr : ¬r = 0
hμ this : IsFiniteMeasure μ
hposbdd : ∫ (ω : α), max (f ω) 0 ∂μ ≤ μ.real univ • ↑r
⊢ 2 * ∫ (a : α), max (f a) 0 ∂μ ≤ 2 * (μ univ).toReal * ↑r
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: case pos
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
r : ℝ≥0
hfint : Integrable f μ
hfint' : ∫ (a : α), ↑(-f a).toNNReal ∂μ ≤ ∫ (a : α), ↑(f a).toNNReal ∂μ
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ ↑r
hr : ¬r = 0
hμ this : IsFiniteMeasure μ
hposbdd : ∫ (ω : α), max (f ω) 0 ∂μ ≤ μ.real univ • ↑r
⊢ Integrable (fun a ↦ ↑(-f a).toNNReal) μ

Tactic:
· exact hfint.neg.sup (integrable_zero _ _ μ)

Goal state after:
Module: Mathlib.Topology.Order.LeftRightLim

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : LinearOrder α
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : Monotone f
x y : α
h : x ≤ y
this✝ : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
⊢ leftLim f x ≤ f y

Tactic:
rcases eq_or_neBot (𝓝[<] x) with h' | h'

Goal state after:
case inl
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder α
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : Monotone f
x y : α
h : x ≤ y
this✝ : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
h' : 𝓝[<] x = ⊥
⊢ leftLim f x ≤ f y

case inr
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder α
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : Monotone f
x y : α
h : x ≤ y
this✝ : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
h' : (𝓝[<] x).NeBot
⊢ leftLim f x ≤ f y
Module: Mathlib.Topology.Order.LeftRightLim

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : ConditionallyCompleteLinearOrder β
inst✝³ : TopologicalSpace β
inst✝² : OrderTopology β
f : α → β
hf : Monotone f
x : α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
⊢ ContinuousWithinAt f (Iio x) x ↔ leftLim f x = f x

Tactic:
rcases eq_or_neBot (𝓝[<] x) with h' | h'

Goal state after:
case inl
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : ConditionallyCompleteLinearOrder β
inst✝³ : TopologicalSpace β
inst✝² : OrderTopology β
f : α → β
hf : Monotone f
x : α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
h' : 𝓝[<] x = ⊥
⊢ ContinuousWithinAt f (Iio x) x ↔ leftLim f x = f x

case inr
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : ConditionallyCompleteLinearOrder β
inst✝³ : TopologicalSpace β
inst✝² : OrderTopology β
f : α → β
hf : Monotone f
x : α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
h' : (𝓝[<] x).NeBot
⊢ ContinuousWithinAt f (Iio x) x ↔ leftLim f x = f x
Module: Mathlib.MeasureTheory.Measure.Stieltjes

Goal state before:
pp: R : Type u_1
inst✝⁴ : LinearOrder R
inst✝³ : TopologicalSpace R
inst✝² : OrderTopology R
inst✝¹ : DenselyOrdered R
inst✝ : NoMaxOrder R
f : StieltjesFunction R
x : R
⊢ ⨅ r, ↑f ↑r = ↑f x

Tactic:
suffices Function.rightLim f x = ⨅ r : Ioi x, f r by rw [← this, f.rightLim_eq]
  rw [f.mono.rightLim_eq_sInf, sInf_image']

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

Goal state before:
pp: case pos.convert_4
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
inst✝¹ : CompleteSpace E
hT : DominatedFinMeasAdditive μ T C
ι : Type u_7
inst✝ : Countable ι
f : ι → α → E
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hf' : ∑' (i : ι), ∫⁻ (a : α), ‖f i a‖ₑ ∂μ ≠ ∞
hF : CompleteSpace F
hf'' : ∀ (i : ι), AEMeasurable (fun x ↦ ‖f i x‖ₑ) μ
hhh : ∀ᵐ (a : α) ∂μ, Summable fun n ↦ ↑‖f n a‖₊
⊢ ∫⁻ (a : α), ‖∑' (n : ι), ‖f n a‖‖ₑ ∂μ < ∞

Tactic:
have : ∫⁻ a, ∑' n, ‖f n a‖ₑ ∂μ < ⊤ := by rwa [lintegral_tsum hf'', lt_top_iff_ne_top]

Goal state after:
case pos.convert_4
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
inst✝¹ : CompleteSpace E
hT : DominatedFinMeasAdditive μ T C
ι : Type u_7
inst✝ : Countable ι
f : ι → α → E
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hf' : ∑' (i : ι), ∫⁻ (a : α), ‖f i a‖ₑ ∂μ ≠ ∞
hF : CompleteSpace F
hf'' : ∀ (i : ι), AEMeasurable (fun x ↦ ‖f i x‖ₑ) μ
hhh : ∀ᵐ (a : α) ∂μ, Summable fun n ↦ ↑‖f n a‖₊
this : ∫⁻ (a : α), ∑' (n : ι), ‖f n a‖ₑ ∂μ < ∞
⊢ ∫⁻ (a : α), ‖∑' (n : ι), ‖f n a‖‖ₑ ∂μ < ∞
Module: Mathlib.MeasureTheory.Integral.SetToL1

Goal state before:
pp: α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
β : Type u_7
mβ : MeasurableSpace β
inst✝ : SFinite μ
hT : DominatedFinMeasAdditive μ T C
h'T : ∀ (s : Set (β × α)), MeasurableSet s → StronglyMeasurable fun x ↦ T (Prod.mk x ⁻¹' s)
f : β → α → E
hf : StronglyMeasurable (Function.uncurry f)
hF : CompleteSpace F
this✝² : MeasurableSpace E := ⋯
this✝¹ : BorelSpace E
this✝ : SeparableSpace ↑(range (Function.uncurry f) ∪ {0})
s : ℕ → SimpleFunc (β × α) E := ⋯
s' : ℕ → β → SimpleFunc α E := ⋯
f' : ℕ → β → F := ⋯
n : ℕ
this : ∀ (x : β), {x ∈ (s' n x).range | x ≠ 0} ⊆ (s n).range
x : E
x✝ : x ∈ (s n).range
⊢ StronglyMeasurable fun a ↦ T (Prod.mk a ⁻¹' ⇑(s n) ⁻¹' {x})

Tactic:
apply h'T

Goal state after:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
β : Type u_7
mβ : MeasurableSpace β
inst✝ : SFinite μ
hT : DominatedFinMeasAdditive μ T C
h'T : ∀ (s : Set (β × α)), MeasurableSet s → StronglyMeasurable fun x ↦ T (Prod.mk x ⁻¹' s)
f : β → α → E
hf : StronglyMeasurable (Function.uncurry f)
hF : CompleteSpace F
this✝² : MeasurableSpace E := ⋯
this✝¹ : BorelSpace E
this✝ : SeparableSpace ↑(range (Function.uncurry f) ∪ {0})
s : ℕ → SimpleFunc (β × α) E := ⋯
s' : ℕ → β → SimpleFunc α E := ⋯
f' : ℕ → β → F := ⋯
n : ℕ
this : ∀ (x : β), {x ∈ (s' n x).range | x ≠ 0} ⊆ (s n).range
x : E
x✝ : x ∈ (s n).range
⊢ MeasurableSet (⇑(s n) ⁻¹' {x})
Module: Mathlib.MeasureTheory.Measure.Stieltjes

Goal state before:
pp: R : Type u_1
inst✝³ : LinearOrder R
inst✝² : TopologicalSpace R
f : StieltjesFunction R
inst✝¹ : OrderTopology R
inst✝ : CompactIccSpace R
a b : R
c d : ℕ → R
ss : Icc a b ⊆ ⋃ i, Iotop (c i) (d i)
⊢ ofReal (↑f b - ↑f a) ≤ ∑' (i : ℕ), ofReal (↑f (d i) - ↑f (c i))

Tactic:
suffices
    ∀ (s : Finset ℕ) (b), Icc a b ⊆ (⋃ i ∈ (s : Set ℕ), Iotop (c i) (d i)) →
      (ofReal (f b - f a) : ℝ≥0∞) ≤ ∑ i ∈ s, ofReal (f (d i) - f (c i)) by
    rcases isCompact_Icc.elim_finite_subcover_image
        (fun (i : ℕ) (_ : i ∈ univ) => @isOpen_Iotop _ _ _ _ (c i) (d i)) (by simpa using ss) with
      ⟨s, _, hf, hs⟩
    have e : ⋃ i ∈ (hf.toFinset : Set ℕ), Iotop (c i) (d i) = ⋃ i ∈ s, Iotop (c i) (d i) := by
      simp only [Finset.set_biUnion_coe,
        Finite.mem_toFinset]
    rw [ENNReal.tsum_eq_iSup_sum]
    refine le_trans ?_ (le_iSup _ hf.toFinset)
    exact this hf.toFinset _ (by simpa only [e])

Goal state after:
R : Type u_1
inst✝³ : LinearOrder R
inst✝² : TopologicalSpace R
f : StieltjesFunction R
inst✝¹ : OrderTopology R
inst✝ : CompactIccSpace R
a b : R
c d : ℕ → R
ss : Icc a b ⊆ ⋃ i, Iotop (c i) (d i)
⊢ ∀ (s : Finset ℕ) (b : R),
    Icc a b ⊆ ⋃ i ∈ ↑s, Iotop (c i) (d i) → ofReal (↑f b - ↑f a) ≤ ∑ i ∈ s, ofReal (↑f (d i) - ↑f (c i))
Module: Mathlib.MeasureTheory.Measure.Stieltjes

Goal state before:
pp: case a
R : Type u_1
inst✝³ : LinearOrder R
inst✝² : TopologicalSpace R
f : StieltjesFunction R
inst✝¹ : OrderTopology R
inst✝ : CompactIccSpace R
a : R
c d : ℕ → R
s✝ s : Finset ℕ
IH :
  ∀ t ⊂ s,
    ∀ (b : R), Icc a b ⊆ ⋃ i ∈ ↑t, Iotop (c i) (d i) → ofReal (↑f b - ↑f a) ≤ ∑ i ∈ t, ofReal (↑f (d i) - ↑f (c i))
b : R
ab : a ≤ b
i : ℕ
cv : Icc a b ⊆ Iotop (c i) (d i) ∪ ⋃ x ∈ ↑(s.erase i), Iotop (c x) (d x)
is : i ∈ s
bcd : b ∈ Ioc (c i) (d i)
⊢ Icc a (c i) ⊆ ⋃ i_1 ∈ ↑(s.erase i), Iotop (c i_1) (d i_1)

Tactic:
rintro x ⟨h₁, h₂⟩

Goal state after:
case a
R : Type u_1
inst✝³ : LinearOrder R
inst✝² : TopologicalSpace R
f : StieltjesFunction R
inst✝¹ : OrderTopology R
inst✝ : CompactIccSpace R
a : R
c d : ℕ → R
s✝ s : Finset ℕ
IH :
  ∀ t ⊂ s,
    ∀ (b : R), Icc a b ⊆ ⋃ i ∈ ↑t, Iotop (c i) (d i) → ofReal (↑f b - ↑f a) ≤ ∑ i ∈ t, ofReal (↑f (d i) - ↑f (c i))
b : R
ab : a ≤ b
i : ℕ
cv : Icc a b ⊆ Iotop (c i) (d i) ∪ ⋃ x ∈ ↑(s.erase i), Iotop (c x) (d x)
is : i ∈ s
bcd : b ∈ Ioc (c i) (d i)
x : R
h₁ : a ≤ x
h₂ : x ≤ c i
⊢ x ∈ ⋃ i_1 ∈ ↑(s.erase i), Iotop (c i_1) (d i_1)
Module: Mathlib.MeasureTheory.Measure.Content

Goal state before:
pp: G : Type w
inst✝ : TopologicalSpace G
μ : Content G
U : Opens G
hU : μ.innerContent U ≠ ∞
ε : ℝ≥0
hε : ε ≠ 0
⊢ ∃ K, ↑K ⊆ ↑U ∧ μ.innerContent U ≤ μ K + ↑ε

Tactic:
have h'ε := ENNReal.coe_ne_zero.2 hε

Goal state after:
G : Type w
inst✝ : TopologicalSpace G
μ : Content G
U : Opens G
hU : μ.innerContent U ≠ ∞
ε : ℝ≥0
hε : ε ≠ 0
h'ε : ↑ε ≠ 0
⊢ ∃ K, ↑K ⊆ ↑U ∧ μ.innerContent U ≤ μ K + ↑ε
Module: Mathlib.MeasureTheory.Measure.Content

Goal state before:
pp: case inr
G : Type w
inst✝ : TopologicalSpace G
μ : Content G
U✝ : Opens G
hU : μ.innerContent U✝ ≠ ∞
ε : ℝ≥0
hε : ε ≠ 0
h'ε : ↑ε ≠ 0
h : ↑ε < μ.innerContent U✝
U : Compacts G
h1U : ↑U ⊆ ↑U✝
h2U : μ.innerContent U✝ - ↑ε < μ U
⊢ μ.innerContent U✝ - ↑ε ≤ μ U

Tactic:
exact le_of_lt h2U

Goal state after:
Module: Mathlib.MeasureTheory.Group.FundamentalDomain

Goal state before:
pp: G : Type u_1
α : Type u_3
inst✝⁵ : Group G
inst✝⁴ : MulAction G α
inst✝³ : MeasurableSpace α
s t : Set α
μ : Measure α
inst✝² : MeasurableConstSMul G α
inst✝¹ : SMulInvariantMeasure G α μ
inst✝ : Countable G
hs : IsFundamentalDomain G s μ
ht : IsFundamentalDomain G t μ
f : α → ℝ≥0∞
hf : ∀ (g : G) (x : α), f (g • x) = f x
⊢ ∑' (g : G), ∫⁻ (x : α) in s ∩ g • t, f x ∂μ = ∑' (g : G), ∫⁻ (x : α) in g • t ∩ s, f (g⁻¹ • x) ∂μ

Tactic:
by simp only [hf, inter_comm]

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

Goal state before:
pp: G : Type w
inst✝ : TopologicalSpace G
μ : Content G
H : μ.ContentRegular
K : Compacts G
ε : ℝ≥0
hε : ε ≠ 0
hc : ∀ (x : Compacts G), K.carrier ⊆ interior x.carrier → μ K + ↑ε < μ x
lower_bound_iInf : μ K + ↑ε ≤ ⨅ K', ⨅ (_ : ↑K ⊆ interior ↑K'), μ K'
⊢ False

Tactic:
← H

Goal state after:
G : Type w
inst✝ : TopologicalSpace G
μ : Content G
H : μ.ContentRegular
K : Compacts G
ε : ℝ≥0
hε : ε ≠ 0
hc : ∀ (x : Compacts G), K.carrier ⊆ interior x.carrier → μ K + ↑ε < μ x
lower_bound_iInf : μ K + ↑ε ≤ μ K
⊢ False
Module: Mathlib.MeasureTheory.Integral.Bochner.Set

Goal state before:
pp: X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
μ : Measure X
inst✝ : PartialOrder E
f : X → E
hf : AEStronglyMeasurable f μ
⊢ ∫ (x : X) in {x | f x < 0}, f x ∂μ = ∫ (x : X) in {x | f x ≤ 0}, f x ∂μ

Tactic:
have h_union : {x | f x ≤ 0} = {x | f x < 0} ∪ {x | f x = 0} := by
    simp_rw [le_iff_lt_or_eq, ofPred_or]
  rw [h_union]
  have B : NullMeasurableSet {x | f x = 0} μ :=
    hf.nullMeasurableSet_eq_fun aestronglyMeasurable_zero
  symm
  refine integral_union_eq_left_of_ae ?_
  filter_upwards [ae_restrict_mem₀ B] with x hx using hx

Goal state after:
Module: Mathlib.MeasureTheory.Group.FundamentalDomain

Goal state before:
pp: G : Type u_1
α : Type u_3
E : Type u_5
inst✝⁷ : Group G
inst✝⁶ : MulAction G α
inst✝⁵ : MeasurableSpace α
inst✝⁴ : NormedAddCommGroup E
s t : Set α
μ : Measure α
inst✝³ : MeasurableConstSMul G α
inst✝² : SMulInvariantMeasure G α μ
inst✝¹ : Countable G
inst✝ : NormedSpace ℝ E
hs : IsFundamentalDomain G s μ
ht : IsFundamentalDomain G t μ
f : α → E
hf : ∀ (g : G) (x : α), f (g • x) = f x
hfs : IntegrableOn f s μ
hft : IntegrableOn f t μ
⊢ ∑' (g : G), ∫ (x : α) in s ∩ g • t, f x ∂μ = ∑' (g : G), ∫ (x : α) in g • t ∩ s, f (g⁻¹ • x) ∂μ

Tactic:
by simp only [hf, inter_comm]

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

Goal state before:
pp: G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
K : Compacts G
V : Set G
hV : (interior V).Nonempty
s : Finset G
h1s : ↑K ⊆ ⋃ g ∈ s, (fun h ↦ g * h) ⁻¹' ↑K₀
h2s : s.card = index ↑K ↑K₀
t : Finset G
h1t : ↑K₀ ⊆ ⋃ g ∈ t, (fun h ↦ g * h) ⁻¹' V
h2t : t.card = index (↑K₀) V
g₁ : G
hg₁ : g₁ ∈ s
⊢ (fun h ↦ g₁ * h) ⁻¹' ↑K₀ ⊆ ⋃ g ∈ t * s, (fun h ↦ g * h) ⁻¹' V

Tactic:
rw [preimage_subset_iff]

Goal state after:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
K : Compacts G
V : Set G
hV : (interior V).Nonempty
s : Finset G
h1s : ↑K ⊆ ⋃ g ∈ s, (fun h ↦ g * h) ⁻¹' ↑K₀
h2s : s.card = index ↑K ↑K₀
t : Finset G
h1t : ↑K₀ ⊆ ⋃ g ∈ t, (fun h ↦ g * h) ⁻¹' V
h2t : t.card = index (↑K₀) V
g₁ : G
hg₁ : g₁ ∈ s
⊢ ∀ (a : G), g₁ * a ∈ ↑K₀ → a ∈ ⋃ g ∈ t * s, (fun h ↦ g * h) ⁻¹' V
Module: Mathlib.MeasureTheory.Measure.Stieltjes

Goal state before:
pp: R : Type u_1
inst✝⁷ : LinearOrder R
inst✝⁶ : TopologicalSpace R
f : StieltjesFunction R
inst✝⁵ : OrderTopology R
inst✝⁴ : CompactIccSpace R
inst✝³ : MeasurableSpace R
inst✝² : BorelSpace R
inst✝¹ : SecondCountableTopology R
inst✝ : DenselyOrdered R
a : R
ha : ¬IsBot a
b : R
hb : b < a
u : ℕ → R
u_mono : StrictMono u
u_lim : Tendsto u atTop (𝓝 a)
u_lt_a : ∀ (n : ℕ), u n < a
A : {a} = ⋂ n, Ioc (u n) a
⊢ Tendsto (fun n ↦ f.measure (Ioc (u n) a)) atTop (𝓝 (f.measure {a}))

Tactic:
rw [A]

Goal state after:
R : Type u_1
inst✝⁷ : LinearOrder R
inst✝⁶ : TopologicalSpace R
f : StieltjesFunction R
inst✝⁵ : OrderTopology R
inst✝⁴ : CompactIccSpace R
inst✝³ : MeasurableSpace R
inst✝² : BorelSpace R
inst✝¹ : SecondCountableTopology R
inst✝ : DenselyOrdered R
a : R
ha : ¬IsBot a
b : R
hb : b < a
u : ℕ → R
u_mono : StrictMono u
u_lim : Tendsto u atTop (𝓝 a)
u_lt_a : ∀ (n : ℕ), u n < a
A : {a} = ⋂ n, Ioc (u n) a
⊢ Tendsto (fun n ↦ f.measure (Ioc (u n) a)) atTop (𝓝 (f.measure (⋂ n, Ioc (u n) a)))
Module: Mathlib.MeasureTheory.Measure.Stieltjes

Goal state before:
pp: case inr
R : Type u_1
inst✝⁷ : LinearOrder R
inst✝⁶ : TopologicalSpace R
f : StieltjesFunction R
inst✝⁵ : OrderTopology R
inst✝⁴ : CompactIccSpace R
inst✝³ : MeasurableSpace R
inst✝² : BorelSpace R
inst✝¹ : SecondCountableTopology R
inst✝ : DenselyOrdered R
a b : R
hab : a < b
A : Disjoint (Ioo a b) {b}
D : ↑f b - ↑f a = ↑f b - leftLim (↑f) b + (leftLim (↑f) b - ↑f a)
⊢ f.measure (Ioo a b) = ofReal (leftLim (↑f) b - ↑f a)

Tactic:
have := f.measure_Ioc a b

Goal state after:
case inr
R : Type u_1
inst✝⁷ : LinearOrder R
inst✝⁶ : TopologicalSpace R
f : StieltjesFunction R
inst✝⁵ : OrderTopology R
inst✝⁴ : CompactIccSpace R
inst✝³ : MeasurableSpace R
inst✝² : BorelSpace R
inst✝¹ : SecondCountableTopology R
inst✝ : DenselyOrdered R
a b : R
hab : a < b
A : Disjoint (Ioo a b) {b}
D : ↑f b - ↑f a = ↑f b - leftLim (↑f) b + (leftLim (↑f) b - ↑f a)
this : f.measure (Ioc a b) = ofReal (↑f b - ↑f a)
⊢ f.measure (Ioo a b) = ofReal (leftLim (↑f) b - ↑f a)