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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : 0 ≤ᵐ[μ] f
hfm : AEStronglyMeasurable f μ
hfi : ∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ = ∞
a : α
h : 0 a ≤ f a
⊢ ENNReal.ofReal (f a) = ENNReal.ofReal ‖f a‖

Tactic:
Real.norm_eq_abs,

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : 0 ≤ᵐ[μ] f
hfm : AEStronglyMeasurable f μ
hfi : ∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ = ∞
a : α
h : 0 a ≤ f a
⊢ ENNReal.ofReal (f a) = ENNReal.ofReal |f a|
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: α : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteSpace E
f : α →ₛ E
hfi : Integrable (⇑f) μ
⊢ ∫ (x : α), f x ∂μ = ∑ x ∈ f.range, μ.real (⇑f ⁻¹' {x}) • x

Tactic:
rw [← f.integral_eq_integral hfi, SimpleFunc.integral, ← SimpleFunc.integral_eq]; rfl

Goal state after:
Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp

Goal state before:
pp: case inr
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
hp_ne_top : p ≠ ∞
P : (α → E) → Prop
h0P :
  ∀ (c : E) ⦃s : Set α⦄,
    MeasurableSet s → μ s < ∞ → ∀ {ε : ℝ≥0∞}, ε ≠ 0 → ∃ g, eLpNorm (g - s.indicator fun x ↦ c) p μ ≤ ε ∧ P g
h1P : ∀ (f g : α → E), P f → P g → P (f + g)
h2P : ∀ (f : α → E), P f → AEStronglyMeasurable f μ
f : α → E
hf : MemLp f p μ
ε : ℝ≥0∞
hε : ε ≠ 0
hp_pos : p ≠ 0
⊢ ∃ g, eLpNorm (f - g) p μ ≤ ε ∧ P g

Tactic:
suffices H : ∀ (f' : α →ₛ E) (δ : ℝ≥0∞) (hδ : δ ≠ 0), MemLp f' p μ →
      ∃ g, eLpNorm (⇑f' - g) p μ ≤ δ ∧ P g by
    obtain ⟨η, ηpos, hη⟩ := exists_Lp_half E μ p hε
    rcases hf.exists_simpleFunc_eLpNorm_sub_lt hp_ne_top ηpos.ne' with ⟨f', hf', f'_mem⟩
    rcases H f' η ηpos.ne' f'_mem with ⟨g, hg, Pg⟩
    refine ⟨g, ?_, Pg⟩
    convert!
      (hη _ _ (hf.aestronglyMeasurable.sub f'.aestronglyMeasurable)
          (f'.aestronglyMeasurable.sub (h2P g Pg)) hf'.le hg).le using 2
    simp only [sub_add_sub_cancel]

Goal state after:
case inr
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
hp_ne_top : p ≠ ∞
P : (α → E) → Prop
h0P :
  ∀ (c : E) ⦃s : Set α⦄,
    MeasurableSet s → μ s < ∞ → ∀ {ε : ℝ≥0∞}, ε ≠ 0 → ∃ g, eLpNorm (g - s.indicator fun x ↦ c) p μ ≤ ε ∧ P g
h1P : ∀ (f g : α → E), P f → P g → P (f + g)
h2P : ∀ (f : α → E), P f → AEStronglyMeasurable f μ
f : α → E
hf : MemLp f p μ
ε : ℝ≥0∞
hε : ε ≠ 0
hp_pos : p ≠ 0
⊢ ∀ (f' : α →ₛ E) (δ : ℝ≥0∞), δ ≠ 0 → MemLp (⇑f') p μ → ∃ g, eLpNorm (⇑f' - g) p μ ≤ δ ∧ P g
Module: Mathlib.Analysis.Normed.Group.AddTorsor

Goal state before:
pp: α : Type u_1
V✝ : Type u_2
P✝ : Type u_3
W : Type u_4
Q : Type u_5
inst✝⁷ : SeminormedAddCommGroup V✝
inst✝⁶ : PseudoMetricSpace P✝
inst✝⁵ : NormedAddTorsor V✝ P✝
inst✝⁴ : SeminormedAddCommGroup W
inst✝³ : PseudoMetricSpace Q
inst✝² : NormedAddTorsor W Q
V : Type u_6
P : Type u_7
inst✝¹ : SeminormedAddCommGroup V
inst✝ : AddTorsor V P
x y z : P
⊢ ‖x -ᵥ z‖ ≤ ‖x -ᵥ y‖ + ‖y -ᵥ z‖

Tactic:
by
    rw [← vsub_add_vsub_cancel]
    apply norm_add_le

Goal state after:
Module: Mathlib.Analysis.Normed.Group.AddTorsor

Goal state before:
pp: α : Type u_1
V✝ : Type u_2
P✝ : Type u_3
W : Type u_4
Q : Type u_5
inst✝⁷ : SeminormedAddCommGroup V✝
inst✝⁶ : PseudoMetricSpace P✝
inst✝⁵ : NormedAddTorsor V✝ P✝
inst✝⁴ : SeminormedAddCommGroup W
inst✝³ : PseudoMetricSpace Q
inst✝² : NormedAddTorsor W Q
V : Type u_6
P : Type u_7
inst✝¹ : NormedAddCommGroup V
inst✝ : AddTorsor V P
x y z : P
⊢ ‖x -ᵥ z‖ ≤ ‖x -ᵥ y‖ + ‖y -ᵥ z‖

Tactic:
by
    rw [← vsub_add_vsub_cancel]
    apply norm_add_le

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hfi : Integrable f μ
f_nn : 0 ≤ᵐ[μ] f
⊢ ENNReal.ofReal (∫ (x : α), f x ∂μ) = ∫⁻ (x : α), ENNReal.ofReal (f x) ∂μ

Tactic:
by
  have : f =ᵐ[μ] (‖f ·‖) := f_nn.mono fun _x hx ↦ (abs_of_nonneg hx).symm
  simp_rw [integral_congr_ae this, ofReal_integral_norm_eq_lintegral_enorm hfi,
    ← ofReal_norm]
  exact lintegral_congr_ae (this.symm.fun_comp ENNReal.ofReal)

Goal state after:
Module: Mathlib.Topology.Algebra.ContinuousAffineMap

Goal state before:
pp: 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
W₂ : Type u_6
Q₂ : Type u_7
W₃ : Type u_8
Q₃ : Type u_9
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
inst✝¹ : TopologicalSpace W₂
inst✝ : IsTopologicalAddTorsor Q₂
f : P →ᴬ[R] Q
⊢ Continuous ⇑(↑f).linear

Tactic:
rw [AffineMap.continuous_linear_iff]

Goal state after:
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
W₂ : Type u_6
Q₂ : Type u_7
W₃ : Type u_8
Q₃ : Type u_9
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
inst✝¹ : TopologicalSpace W₂
inst✝ : IsTopologicalAddTorsor Q₂
f : P →ᴬ[R] Q
⊢ Continuous ⇑↑f
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ
F : α → ℝ
hf : ∀ (n : ℕ), Integrable (f n) μ
hF : Integrable F μ
h_mono : ∀ᵐ (x : α) ∂μ, Antitone fun n ↦ f n x
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (F x))
this : Tendsto (fun n ↦ ∫ (x : α), -f n x ∂μ) atTop (𝓝 (∫ (x : α), -F x ∂μ))
⊢ Tendsto (fun n ↦ ∫ (x : α), - -f n x ∂μ) atTop (𝓝 (∫ (x : α), - -F x ∂μ))

Tactic:
convert! this.neg <;> rw [integral_neg]

Goal state after:
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:
compl_frontier_eq_union_interior

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 ∈ interior s ∪ interior sᶜ
⊢ ContinuousAt (s.mulIndicator f) x
Module: Mathlib.Analysis.Normed.Module.FiniteDimension

Goal state before:
pp: 𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type v
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type w
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : CompleteSpace 𝕜
inst✝ : FiniteDimensional 𝕜 E
f : E →ₗ[𝕜] F
hf : f.ker = ⊥
⊢ ∃ K > 0, AntilipschitzWith K ⇑f

Tactic:
cases subsingleton_or_nontrivial E
  · exact ⟨1, zero_lt_one, AntilipschitzWith.of_subsingleton⟩
  · rw [LinearMap.ker_eq_bot] at hf
    let e : E ≃L[𝕜] LinearMap.range f := (LinearEquiv.ofInjective f hf).toContinuousLinearEquiv
    exact ⟨_, e.nnnorm_symm_pos, e.antilipschitz⟩

Goal state after:
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 : ℝ
inst✝ : CompleteSpace F
hT : DominatedFinMeasAdditive μ T C
f : SimpleFunc α E
hf : Integrable (⇑f) μ
⊢ setToFun μ T hT ⇑f = ∑ x ∈ f.range, (T (⇑f ⁻¹' {x})) x

Tactic:
by
  have h'f : MemLp f 1 μ := memLp_one_iff_integrable.mpr hf
  let g := f.toLp h'f
  have A : f =ᵐ[μ] g := h'f.coeFn_toLp.symm
  rw [setToFun_congr_ae hT A, L1.setToFun_eq_setToL1 hT, L1.setToL1_eq_setToL1SCLM]
  apply (SimpleFunc.setToSimpleFunc_congr T (fun s ↦ hT.eq_zero_of_measure_zero) hT.1 hf _).symm
  grw [A, Lp.simpleFunc.toSimpleFunc_eq_toFun]

Goal state after:
Module: Mathlib.Topology.ContinuousMap.Bounded.Normed

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : SeminormedAddCommGroup β
f : α →ᵇ β
n : ℕ
⊢ ⇑(zsmulRec (fun x1 x2 ↦ x1 • x2) (Int.negSucc n) f) = Int.negSucc n • ⇑f

Tactic:
rw [zsmulRec, negSucc_zsmul, coe_neg, coe_nsmul]

Goal state after:
Module: Mathlib.Topology.ContinuousMap.Star

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝⁸ : TopologicalSpace X
inst✝⁷ : TopologicalSpace Y
𝕜 : Type u_3
inst✝⁶ : CommSemiring 𝕜
A : Type u_4
inst✝⁵ : TopologicalSpace A
inst✝⁴ : Semiring A
inst✝³ : IsTopologicalSemiring A
inst✝² : StarRing A
inst✝¹ : ContinuousStar A
inst✝ : Algebra 𝕜 A
f : X ≃ₜ Y
g : C(X, A)
⊢ (ContinuousMap.compStarAlgHom' 𝕜 A ↑f) ((ContinuousMap.compStarAlgHom' 𝕜 A ↑f.symm) g) = g

Tactic:
by
      simp only [ContinuousMap.compStarAlgHom'_apply, ContinuousMap.comp_assoc,
        symm_comp_toContinuousMap, ContinuousMap.comp_id]

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 : α), ↑(-f a).toNNReal ∂μ ≤ ∫ (a : α), ↑(f a).toNNReal ∂μ
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ ↑r
hr : ¬r = 0
hμ this : IsFiniteMeasure μ
hposbdd : ∫ (ω : α), max (f ω) 0 ∂μ ≤ μ.real univ • ↑r
⊢ ∫ (a : α), ‖f a‖ ∂μ ≤ (2 * μ univ * ↑r).toReal

Tactic:
Real.norm_eq_abs,

Goal state after:
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
⊢ ∫ (a : α), |f a| ∂μ ≤ (2 * μ univ * ↑r).toReal
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 : ℝ
hT : DominatedFinMeasAdditive μ T C
ι : Type u_7
l : Filter ι
inst✝ : l.IsCountablyGenerated
fs : ι → α → E
f : α → E
bound : α → ℝ
hfs_meas : ∀ᶠ (n : ι) in l, AEStronglyMeasurable (fs n) μ
h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a
bound_integrable : Integrable bound μ
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n ↦ fs n a) l (𝓝 (f a))
x : ℕ → ι
xl : Tendsto x atTop l
hxl : ∀ s ∈ l, ∃ a, ∀ b ≥ a, x b ∈ s
h : {x | (fun n ↦ AEStronglyMeasurable (fs n) μ) x} ∩ {x | (fun n ↦ ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a) x} ∈ l
⊢ Tendsto ((fun n ↦ setToFun μ T hT (fs n)) ∘ x) atTop (𝓝 (setToFun μ T hT f))

Tactic:
obtain ⟨k, h⟩ := hxl _ h

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 : ℝ
hT : DominatedFinMeasAdditive μ T C
ι : Type u_7
l : Filter ι
inst✝ : l.IsCountablyGenerated
fs : ι → α → E
f : α → E
bound : α → ℝ
hfs_meas : ∀ᶠ (n : ι) in l, AEStronglyMeasurable (fs n) μ
h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a
bound_integrable : Integrable bound μ
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n ↦ fs n a) l (𝓝 (f a))
x : ℕ → ι
xl : Tendsto x atTop l
hxl : ∀ s ∈ l, ∃ a, ∀ b ≥ a, x b ∈ s
h✝ : {x | (fun n ↦ AEStronglyMeasurable (fs n) μ) x} ∩ {x | (fun n ↦ ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a) x} ∈ l
k : ℕ
h : ∀ b ≥ k, x b ∈ {x | (fun n ↦ AEStronglyMeasurable (fs n) μ) x} ∩ {x | (fun n ↦ ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a) x}
⊢ Tendsto ((fun n ↦ setToFun μ T hT (fs n)) ∘ x) atTop (𝓝 (setToFun μ T hT f))
Module: Mathlib.Topology.Order.LeftRightLim

Goal state before:
pp: 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' : 𝓝[<] y = ⊥
⊢ rightLim f x ≤ leftLim f y

Tactic:
simpa [leftLim, h'] using rightLim_le hf h

Goal state after:
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
this : rightLim (↑f) x = ⨅ r, ↑f ↑r
⊢ ⨅ r, ↑f ↑r = ↑f x

Tactic:
by rw [← this, f.rightLim_eq]

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

Goal state before:
pp: f : StieltjesFunction ℝ
x y : ℝ
⊢ y ∈ ↑f '' Ioi x → ↑f x ≤ y

Tactic:
rintro ⟨y, hy_mem, rfl⟩

Goal state after:
f : StieltjesFunction ℝ
x y : ℝ
hy_mem : y ∈ Ioi x
⊢ ↑f x ≤ ↑f 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 : ℝ
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‖ₑ ∂μ ≠ ∞
⊢ (setToFun μ T hT fun a ↦ ∑' (i : ι), f i a) = ∑' (i : ι), setToFun μ T hT (f i)

Tactic:
by
  by_cases hF : CompleteSpace F; swap
  · simp [setToFun, hF]
  have hf'' i : AEMeasurable (‖f i ·‖ₑ) μ := (hf i).enorm
  have hhh : ∀ᵐ a : α ∂μ, Summable fun n => (‖f n a‖₊ : ℝ) := by
    rw [← lintegral_tsum hf''] at hf'
    refine (ae_lt_top' (AEMeasurable.tsum hf'') hf').mono ?_
    intro x hx
    rw [← ENNReal.tsum_coe_ne_top_iff_summable_coe]
    exact hx.ne
  convert!
    (MeasureTheory.hasSum_setToFun_of_dominated_convergence hT (fun i a => ‖f i a‖₊) hf _ hhh ⟨_, _⟩
        _).tsum_eq.symm
  · intro n
    filter_upwards with x
    rfl
  · fun_prop
  · dsimp [HasFiniteIntegral]
    have : ∫⁻ a, ∑' n, ‖f n a‖ₑ ∂μ < ⊤ := by rwa [lintegral_tsum hf'', lt_top_iff_ne_top]
    convert! this using 1
    apply lintegral_congr_ae
    simp_rw [← coe_nnnorm, ← NNReal.coe_tsum, enorm_eq_nnnorm, NNReal.nnnorm_eq]
    filter_upwards [hhh] with a ha
    exact ENNReal.coe_tsum (NNReal.summable_coe.mp ha)
  · filter_upwards [hhh] with x hx
    exact hx.of_norm.hasSum

Goal state after:
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)
this :
  ∀ (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))
⊢ ofReal (↑f b - ↑f a) ≤ ∑' (i : ℕ), ofReal (↑f (d i) - ↑f (c i))

Tactic:
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:
Module: Mathlib.MeasureTheory.Integral.Bochner.Set

Goal state before:
pp: case e'_5
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
f : X → E
μ : Measure X
ι : Type u_5
inst✝¹ : Preorder ι
inst✝ : atTop.IsCountablyGenerated
s : ι → Set X
hsm : ∀ (i : ι), MeasurableSet (s i)
h_anti : Antitone s
hne : atTop.NeBot
this✝ : IsDirectedOrder ι
i₀ : ι
hi₀ : IntegrableOn f (s i₀) μ
this :
  Tendsto (fun x ↦ ∫ (x : X) in s i₀, f x ∂μ - ∫ (x : X) in s i₀ \ s x, f x ∂μ) atTop
    (𝓝 (∫ (x : X) in s i₀, f x ∂μ - ∫ (x : X) in ⋃ i, s i₀ \ s i, f x ∂μ))
⊢ ∫ (x : X) in ⋂ n, s n, f x ∂μ = ∫ (x : X) in s i₀, f x ∂μ - ∫ (x : X) in ⋃ i, s i₀ \ s i, f x ∂μ

Tactic:
rw [← sdiff_iInter, setIntegral_sdiff _ hi₀ (iInter_subset _ _), sub_sub_cancel]

Goal state after:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
f : X → E
μ : Measure X
ι : Type u_5
inst✝¹ : Preorder ι
inst✝ : atTop.IsCountablyGenerated
s : ι → Set X
hsm : ∀ (i : ι), MeasurableSet (s i)
h_anti : Antitone s
hne : atTop.NeBot
this✝ : IsDirectedOrder ι
i₀ : ι
hi₀ : IntegrableOn f (s i₀) μ
this :
  Tendsto (fun x ↦ ∫ (x : X) in s i₀, f x ∂μ - ∫ (x : X) in s i₀ \ s x, f x ∂μ) atTop
    (𝓝 (∫ (x : X) in s i₀, f x ∂μ - ∫ (x : X) in ⋃ i, s i₀ \ s i, f x ∂μ))
⊢ MeasurableSet (⋂ i, s i)
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
f : X → E
s t : Set X
μ : Measure X
ht_eq : ∀ᵐ (x : X) ∂μ.restrict t, f x = 0
haux : StronglyMeasurable f
H : IntegrableOn f (s ∪ t) μ
k : Set X := f ⁻¹' {0}
hk : MeasurableSet k
h's : IntegrableOn f s μ
A : ∀ (u : Set X), ∫ (x : X) in u ∩ k, f x ∂μ = 0
⊢ ∫ (x : X) in s ∪ t, f x ∂μ = ∫ (x : X) in s, f x ∂μ

Tactic:
← integral_inter_add_sdiff hk h's,

Goal state after:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → E
s t : Set X
μ : Measure X
ht_eq : ∀ᵐ (x : X) ∂μ.restrict t, f x = 0
haux : StronglyMeasurable f
H : IntegrableOn f (s ∪ t) μ
k : Set X := f ⁻¹' {0}
hk : MeasurableSet k
h's : IntegrableOn f s μ
A : ∀ (u : Set X), ∫ (x : X) in u ∩ k, f x ∂μ = 0
⊢ ∫ (x : X) in s ∪ t, f x ∂μ = ∫ (x : X) in s ∩ k, f x ∂μ + ∫ (x : X) in s \ k, f x ∂μ
Module: Mathlib.MeasureTheory.Measure.Content

Goal state before:
pp: G : Type w
inst✝ : TopologicalSpace G
μ : Content G
f : G ≃ₜ G
h : ∀ ⦃K : Compacts G⦄, μ (Compacts.map ⇑f ⋯ K) = μ K
U : Opens G
⊢ μ.innerContent ((Opens.comap ↑f) U) = μ.innerContent U

Tactic:
by
  refine (Compacts.equiv f).surjective.iSup_congr _ fun K => iSup_congr_Prop image_subset_iff ?_
  intro hK
  simp only [Compacts.equiv]
  apply h

Goal state after:
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
f : X → E
s t : Set X
μ : Measure X
ht : NullMeasurableSet t μ
hts : s ⊆ t
h't : ∀ᵐ (x : X) ∂μ, x ∈ t \ s → f x = 0
h : IntegrableOn f t μ
f' : X → E := AEStronglyMeasurable.mk f ⋯
⊢ ∫ (x : X) in s, f' x ∂μ = ∫ (x : X) in s, f x ∂μ

Tactic:
apply integral_congr_ae
      apply ae_restrict_of_ae_restrict_of_subset hts
      exact h.1.ae_eq_mk.symm

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

Goal state before:
pp: case e_a
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
f : X → ℝ
hfi : Integrable f μ
h_meas : NullMeasurableSet {x | 0 ≤ f x} μ
x : X
hx : x ∈ {x | 0 ≤ f x}
⊢ ‖f x‖ = f x

Tactic:
Real.norm_eq_abs,

Goal state after:
case e_a
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
f : X → ℝ
hfi : Integrable f μ
h_meas : NullMeasurableSet {x | 0 ≤ f x} μ
x : X
hx : x ∈ {x | 0 ≤ f x}
⊢ |f x| = f x
Module: Mathlib.MeasureTheory.Integral.Bochner.Set

Goal state before:
pp: case e_a
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
f : X → ℝ
hfi : Integrable f μ
h_meas : NullMeasurableSet {x | 0 ≤ f x} μ
x : X
hx : x ∈ {x | 0 ≤ f x}ᶜ
⊢ ‖f x‖ = -f x

Tactic:
Real.norm_eq_abs,

Goal state after:
case e_a
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
f : X → ℝ
hfi : Integrable f μ
h_meas : NullMeasurableSet {x | 0 ≤ f x} μ
x : X
hx : x ∈ {x | 0 ≤ f x}ᶜ
⊢ |f x| = -f 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
inst✝³ : MeasurableSpace R
inst✝² : BorelSpace R
inst✝¹ : SecondCountableTopology R
inst✝ : DenselyOrdered R
_s : ℕ → Set R
hs : ∀ (i : ℕ), MeasurableSet (_s i)
i : ℕ
⊢ MeasurableSet (_s i)

Tactic:
borelize R
    exact hs i

Goal state after:
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
⊢ f.measure (Ioc (u 0) a) ≠ ∞

Tactic:
by simpa only [measure_Ioc] using ENNReal.ofReal_ne_top

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

Goal state before:
pp: X : Type u_1
mX : MeasurableSpace X
μ : Measure X
R : ℝ
f : X → ℝ
hR : 0 ≤ R
hfint : IntegrableOn f {x | R < f x} μ
hμ : μ {x | R < f x} ≠ 0
⊢ ∫⁻ (a : X) in {x | R < f x}, ‖(fun x ↦ R) a‖ₑ ∂μ ≤ ∫⁻ (a : X) in {x | R < f x}, ‖f a‖ₑ ∂μ

Tactic:
refine setLIntegral_mono_ae hfint.1.enorm <| ae_of_all _ fun x hx => ?_

Goal state after:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
R : ℝ
f : X → ℝ
hR : 0 ≤ R
hfint : IntegrableOn f {x | R < f x} μ
hμ : μ {x | R < f x} ≠ 0
x : X
hx : x ∈ {x | R < f x}
⊢ ‖(fun x ↦ R) x‖ₑ ≤ ‖f x‖ₑ
Module: Mathlib.MeasureTheory.Group.FundamentalDomain

Goal state before:
pp: G : Type u_1
α : Type u_3
inst✝⁴ : Group G
inst✝³ : MulAction G α
inst✝² : MeasurableSpace α
ν : Measure α
hasFun : HasFundamentalDomain G α ν
μ μ' : Measure (Quotient α_mod_G)
inst✝¹ : QuotientMeasureEqMeasurePreimage ν μ
inst✝ : QuotientMeasureEqMeasurePreimage ν μ'
⊢ μ = μ'

Tactic:
by
  obtain ⟨𝓕, h𝓕⟩ := hasFun.ExistsIsFundamentalDomain
  rw [h𝓕.projection_respects_measure (μ := μ), h𝓕.projection_respects_measure (μ := μ')]

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 α
ν : Measure α
inst✝⁴ : SMulInvariantMeasure G α ν
inst✝³ : Countable G
inst✝² : MeasurableConstSMul G α
μ : Measure (Quotient α_mod_G)
inst✝¹ : QuotientMeasureEqMeasurePreimage ν μ
inst✝ : IsFiniteMeasure μ
⊢ covolume G α ν < ∞

Tactic:
by_cases hasFun : HasFundamentalDomain G α ν

Goal state after:
case pos
G : Type u_1
α : Type u_3
inst✝⁷ : Group G
inst✝⁶ : MulAction G α
inst✝⁵ : MeasurableSpace α
ν : Measure α
inst✝⁴ : SMulInvariantMeasure G α ν
inst✝³ : Countable G
inst✝² : MeasurableConstSMul G α
μ : Measure (Quotient α_mod_G)
inst✝¹ : QuotientMeasureEqMeasurePreimage ν μ
inst✝ : IsFiniteMeasure μ
hasFun : HasFundamentalDomain G α ν
⊢ covolume G α ν < ∞

case neg
G : Type u_1
α : Type u_3
inst✝⁷ : Group G
inst✝⁶ : MulAction G α
inst✝⁵ : MeasurableSpace α
ν : Measure α
inst✝⁴ : SMulInvariantMeasure G α ν
inst✝³ : Countable G
inst✝² : MeasurableConstSMul G α
μ : Measure (Quotient α_mod_G)
inst✝¹ : QuotientMeasureEqMeasurePreimage ν μ
inst✝ : IsFiniteMeasure μ
hasFun : ¬HasFundamentalDomain G α ν
⊢ covolume G α ν < ∞
Module: Mathlib.MeasureTheory.Measure.Haar.Basic

Goal state before:
pp: case right
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
this : IsCompact (haarProduct ↑K₀)
t : Finset (OpenNhdsOf 1)
V₀ : Set G := ⋯
h1V₀ : IsOpen[inst✝¹] V₀
h2V₀ : 1 ∈ V₀
V : Opens G
hV : 1 ∈ V.carrier
h2V : { toOpens := V, mem' := hV } ∈ t
⊢ prehaar (↑K₀) V₀ ∈ prehaar ↑K₀ '' {U | U ⊆ ↑{ toOpens := V, mem' := hV }.toOpens ∧ IsOpen[inst✝¹] U ∧ 1 ∈ U}

Tactic:
apply mem_image_of_mem

Goal state after:
case right
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
this : IsCompact (haarProduct ↑K₀)
t : Finset (OpenNhdsOf 1)
V₀ : Set G := ⋯
h1V₀ : IsOpen[inst✝¹] V₀
h2V₀ : 1 ∈ V₀
V : Opens G
hV : 1 ∈ V.carrier
h2V : { toOpens := V, mem' := hV } ∈ t
⊢ V₀ ∈ {U | U ⊆ ↑{ toOpens := V, mem' := hV }.toOpens ∧ IsOpen[inst✝¹] U ∧ 1 ∈ U}