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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
s t : Set α
μ : Measure α
ε' : Type u_7
inst✝² : TopologicalSpace ε'
inst✝¹ : ENormedAddMonoid ε'
inst✝ : PseudoMetrizableSpace ε'
f : α → ε'
hf : IntegrableOn f s μ
ht : NullMeasurableSet t μ
h't : ∀ᵐ (x : α) ∂μ, x ∈ t \ s → f x = 0
⊢ IntegrableOn f t μ

Tactic:
let u := { x ∈ s | f x ≠ 0 }
  have hu : IntegrableOn f u μ := hf.mono_set fun x hx => hx.1
  let v := toMeasurable μ u
  have A : IntegrableOn f v μ := by
    rw [IntegrableOn, hu.restrict_toMeasurable]
    · exact hu
    · intro x hx; simpa using hx.2
  have B : IntegrableOn f (t \ v) μ := by
    apply integrableOn_zero.congr
    filter_upwards [ae_restrict_of_ae h't,
      ae_restrict_mem₀ (ht.diff (measurableSet_toMeasurable μ u).nullMeasurableSet)] with x hxt hx
    by_cases h'x : x ∈ s
    · by_contra H
      exact hx.2 (subset_toMeasurable μ u ⟨h'x, Ne.symm H⟩)
    · exact (hxt ⟨hx.1, h'x⟩).symm
  apply (A.union B).mono_set _
  rw [union_sdiff_self]
  exact subset_union_right

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
inst✝⁴ : TopologicalSpace α
inst✝³ : OpensMeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : TopologicalSpace β
inst✝ : BorelSpace β
f : α → β
s : Set α
μ : Measure α
hf : ContinuousOn f s
hs : NullMeasurableSet s μ
⊢ AEMeasurable f (μ.restrict s)

Tactic:
by
  rcases hs.exists_measurable_subset_ae_eq with ⟨t, ts, ht, t_eq_s⟩
  rw [← Measure.restrict_congr_set t_eq_s]
  exact ContinuousOn.aemeasurable (hf.mono ts) ht

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

Goal state before:
pp: case neg
𝕜 : Type u_1
E : Type u_2
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : CompleteSpace 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : TopologicalSpace E
inst✝³ : IsTopologicalAddGroup E
inst✝² : Module 𝕜 E
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : T2Space E
c : E
hc : ¬c = 0
⊢ IsClosedMap fun x ↦ x • c

Tactic:
· exact (isClosedEmbedding_smul_left hc).isClosedMap

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable

Goal state before:
pp: X : Type u_4
E : Type u_5
ι : Type u_6
inst✝⁷ : MeasurableSpace X
inst✝⁶ : CommMonoid E
inst✝⁵ : TopologicalSpace E
inst✝⁴ : ContinuousMul E
L : SummationFilter ι
inst✝³ : L.NeBot
inst✝² : L.filter.IsCountablyGenerated
inst✝¹ : IsCompletelyPseudoMetrizableSpace E
inst✝ : Countable ι
f : ι → X → E
h : ∀ (i : ι), StronglyMeasurable (f i)
⊢ StronglyMeasurable fun x ↦ ∏'[L] (i : ι), f i x

Tactic:
let E := { x | Multipliable (f · x) L }

Goal state after:
X : Type u_4
E✝ : Type u_5
ι : Type u_6
inst✝⁷ : MeasurableSpace X
inst✝⁶ : CommMonoid E✝
inst✝⁵ : TopologicalSpace E✝
inst✝⁴ : ContinuousMul E✝
L : SummationFilter ι
inst✝³ : L.NeBot
inst✝² : L.filter.IsCountablyGenerated
inst✝¹ : IsCompletelyPseudoMetrizableSpace E✝
inst✝ : Countable ι
f : ι → X → E✝
h : ∀ (i : ι), StronglyMeasurable (f i)
E : Set X := {x | Multipliable (fun x_1 ↦ f x_1 x) L}
⊢ StronglyMeasurable fun x ↦ ∏'[L] (i : ι), f i x
Module: Mathlib.MeasureTheory.Function.LocallyIntegrable

Goal state before:
pp: X : Type u_1
ε : Type u_3
ε' : Type u_4
inst✝⁵ : MeasurableSpace X
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace ε
inst✝² : ContinuousENorm ε
inst✝¹ : TopologicalSpace ε'
inst✝ : ContinuousENorm ε'
f : X → ε
μ : Measure X
hf : LocallyIntegrableOn f univ μ
g : X → ε'
hg : AEStronglyMeasurable g μ
h : ∀ᵐ (x : X) ∂μ, ‖g x‖ₑ ≤ ‖f x‖ₑ
⊢ LocallyIntegrableOn g univ μ

Tactic:
exact hf.mono_enorm hg h

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic

Goal state before:
pp: 𝕜 : Type u
ι : Type v
E : ι → Type wE
G : Type wG
G' : Type wG'
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝⁵ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝⁴ : SeminormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
inst✝² : SeminormedAddCommGroup G'
inst✝¹ : NormedSpace 𝕜 G'
inst✝ : Fintype ι
g : G →ₗᵢ[𝕜] G'
f : ContinuousMultilinearMap 𝕜 E G
⊢ ‖g.toContinuousLinearMap.compContinuousMultilinearMap f‖ = ‖f‖

Tactic:
simp only [ContinuousLinearMap.compContinuousMultilinearMap_coe,
    LinearIsometry.coe_toContinuousLinearMap, LinearIsometry.norm_map,
    ContinuousMultilinearMap.norm_def, Function.comp_apply]

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

Goal state before:
pp: β : Type u_2
E : Type u_4
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace E
inst✝² : NormedAddCommGroup E
p : ℝ≥0∞
inst✝¹ : BorelSpace E
f : β → E
hp : Fact (1 ≤ p)
hp_ne_top : p ≠ ∞
μ : Measure β
fmeas : Measurable f
inst✝ : SeparableSpace ↑(Set.range f ∪ {0})
hf : MemLp f p μ
⊢ Tendsto (fun n ↦ MemLp.toLp ⇑(approxOn f fmeas (Set.range f ∪ {0}) 0 ⋯ n) ⋯) atTop (𝓝 (MemLp.toLp f hf))

Tactic:
simpa only [Lp.tendsto_Lp_iff_tendsto_eLpNorm''] using
    tendsto_approxOn_range_Lp_eLpNorm hp_ne_top fmeas hf.2

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

Goal state before:
pp: α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
_i : Fact (1 ≤ p)
hp_ne_top : p ≠ ∞
motive : ↥(Lp E p μ) → Prop
indicatorConst :
  ∀ (c : E) {s : Set α} (hs : MeasurableSet s) (hμs : μ s < ∞), motive ↑(simpleFunc.indicatorConst p hs ⋯ c)
add :
  ∀ ⦃f g : α → E⦄ (hf : MemLp f p μ) (hg : MemLp g p μ),
    Disjoint (support f) (support g) →
      motive (MemLp.toLp f hf) → motive (MemLp.toLp g hg) → motive (MemLp.toLp f hf + MemLp.toLp g hg)
isClosed : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] {f | motive f}
f : ↥(Lp E p μ)
⊢ ∀ (a : ↥(simpleFunc E p μ)), motive ↑a

Tactic:
refine Lp.simpleFunc.induction (α := α) (E := E) (lt_of_lt_of_le zero_lt_one _i.elim).ne'
    hp_ne_top ?_ ?_

Goal state after:
case refine_1
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
_i : Fact (1 ≤ p)
hp_ne_top : p ≠ ∞
motive : ↥(Lp E p μ) → Prop
indicatorConst :
  ∀ (c : E) {s : Set α} (hs : MeasurableSet s) (hμs : μ s < ∞), motive ↑(simpleFunc.indicatorConst p hs ⋯ c)
add :
  ∀ ⦃f g : α → E⦄ (hf : MemLp f p μ) (hg : MemLp g p μ),
    Disjoint (support f) (support g) →
      motive (MemLp.toLp f hf) → motive (MemLp.toLp g hg) → motive (MemLp.toLp f hf + MemLp.toLp g hg)
isClosed : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] {f | motive f}
f : ↥(Lp E p μ)
⊢ ∀ (c : E) {s : Set α} (hs : MeasurableSet s) (hμs : μ s < ∞), motive ↑(simpleFunc.indicatorConst p hs ⋯ c)

case refine_2
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
_i : Fact (1 ≤ p)
hp_ne_top : p ≠ ∞
motive : ↥(Lp E p μ) → Prop
indicatorConst :
  ∀ (c : E) {s : Set α} (hs : MeasurableSet s) (hμs : μ s < ∞), motive ↑(simpleFunc.indicatorConst p hs ⋯ c)
add :
  ∀ ⦃f g : α → E⦄ (hf : MemLp f p μ) (hg : MemLp g p μ),
    Disjoint (support f) (support g) →
      motive (MemLp.toLp f hf) → motive (MemLp.toLp g hg) → motive (MemLp.toLp f hf + MemLp.toLp g hg)
isClosed : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] {f | motive f}
f : ↥(Lp E p μ)
⊢ ∀ ⦃f g : α →ₛ E⦄ (hf : MemLp (⇑f) p μ) (hg : MemLp (⇑g) p μ),
    Disjoint (support ⇑f) (support ⇑g) → motive ↑(f.toLp hf) → motive ↑(g.toLp hg) → motive ↑(f.toLp hf + g.toLp hg)
Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive

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
h_add : FinMeasAdditive μ T
f g : α →ₛ E
hf : Integrable (⇑f) μ
hg : ∀ (y : E), y ≠ 0 → μ (⇑g ⁻¹' {y}) < ∞
x : E
hx_ne : x ≠ 0
⊢ μ (⇑g ⁻¹' (-{x})) < ∞

Tactic:
Set.neg_singleton

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
h_add : FinMeasAdditive μ T
f g : α →ₛ E
hf : Integrable (⇑f) μ
hg : ∀ (y : E), y ≠ 0 → μ (⇑g ⁻¹' {y}) < ∞
x : E
hx_ne : x ≠ 0
⊢ μ (⇑g ⁻¹' {-x}) < ∞
Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive

Goal state before:
pp: α : Type u_1
G' : Type u_7
G'' : Type u_8
inst✝⁶ : NormedAddCommGroup G''
inst✝⁵ : PartialOrder G''
inst✝⁴ : IsOrderedAddMonoid G''
inst✝³ : NormedSpace ℝ G''
inst✝² : NormedAddCommGroup G'
inst✝¹ : PartialOrder G'
inst✝ : NormedSpace ℝ G'
m : MeasurableSpace α
T : Set α → G' →L[ℝ] G''
hT_nonneg : ∀ (s : Set α) (x : G'), 0 ≤ x → 0 ≤ (T s) x
f : α →ₛ G'
hf : 0 ≤ f
i : G'
hi : i ∈ f.range
⊢ 0 ≤ i

Tactic:
mem_range

Goal state after:
α : Type u_1
G' : Type u_7
G'' : Type u_8
inst✝⁶ : NormedAddCommGroup G''
inst✝⁵ : PartialOrder G''
inst✝⁴ : IsOrderedAddMonoid G''
inst✝³ : NormedSpace ℝ G''
inst✝² : NormedAddCommGroup G'
inst✝¹ : PartialOrder G'
inst✝ : NormedSpace ℝ G'
m : MeasurableSpace α
T : Set α → G' →L[ℝ] G''
hT_nonneg : ∀ (s : Set α) (x : G'), 0 ≤ x → 0 ≤ (T s) x
f : α →ₛ G'
hf : 0 ≤ f
i : G'
hi : i ∈ Set.range ⇑f
⊢ 0 ≤ i
Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive

Goal state before:
pp: case neg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
G' : Type u_7
G'' : Type u_8
inst✝⁶ : NormedAddCommGroup G''
inst✝⁵ : PartialOrder G''
inst✝⁴ : IsOrderedAddMonoid G''
inst✝³ : NormedSpace ℝ G''
inst✝² : NormedAddCommGroup G'
inst✝¹ : PartialOrder G'
inst✝ : NormedSpace ℝ G'
T : Set α → G' →L[ℝ] G''
hT_nonneg : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ∀ (x : G'), 0 ≤ x → 0 ≤ (T s) x
f : α →ₛ G'
hf : 0 ≤ f
hfi : Integrable (⇑f) μ
i : G'
hi : i ∈ f.range
h0 : ¬i = 0
⊢ 0 ≤ i

Tactic:
mem_range

Goal state after:
case neg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
G' : Type u_7
G'' : Type u_8
inst✝⁶ : NormedAddCommGroup G''
inst✝⁵ : PartialOrder G''
inst✝⁴ : IsOrderedAddMonoid G''
inst✝³ : NormedSpace ℝ G''
inst✝² : NormedAddCommGroup G'
inst✝¹ : PartialOrder G'
inst✝ : NormedSpace ℝ G'
T : Set α → G' →L[ℝ] G''
hT_nonneg : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ∀ (x : G'), 0 ≤ x → 0 ≤ (T s) x
f : α →ₛ G'
hf : 0 ≤ f
hfi : Integrable (⇑f) μ
i : G'
hi : i ∈ Set.range ⇑f
h0 : ¬i = 0
⊢ 0 ≤ i
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_7
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
f : α → E
fmeas : Measurable f
hf : Integrable f μ
inst✝ : SeparableSpace ↑(range f ∪ {0})
n : ℕ
⊢ IsSeparable (range f)

Tactic:
exact .mono (.of_subtype (range f ∪ {0})) subset_union_left

Goal state after:
Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent

Goal state before:
pp: α : Type u_1
ι : Type u_2
β : Type u_3
inst✝ : NormedField β
l✝ : Filter α
f g : ι → α → β
l : List ι
h : ∀ i ∈ ↑l, f i ~[l✝] g i
⊢ (fun x ↦ (Multiset.map (fun x_1 ↦ f x_1 x) ↑l).prod) ~[l✝] fun x ↦ (Multiset.map (fun x_1 ↦ g x_1 x) ↑l).prod

Tactic:
exact listProd h

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

Goal state before:
pp: case inr.const.inl
α : 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
s : Set α
hs : MeasurableSet s
ε : ℝ≥0∞
εpos : ε ≠ 0
Hs : MemLp (⇑(SimpleFunc.piecewise s hs (SimpleFunc.const α 0) (SimpleFunc.const α 0))) p μ
⊢ ∃ g, eLpNorm (⇑(SimpleFunc.piecewise s hs (SimpleFunc.const α 0) (SimpleFunc.const α 0)) - g) p μ ≤ ε ∧ P g

Tactic:
rcases h0P (0 : E) MeasurableSet.empty (by simp only [measure_empty, zero_lt_top])
          εpos with ⟨g, hg, Pg⟩
      rw [← eLpNorm_neg, neg_sub] at hg
      refine ⟨g, ?_, Pg⟩
      convert! hg
      ext x
      simp

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

Goal state before:
pp: case inr
𝕜 : 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 = ⊥
h✝ : Nontrivial E
⊢ ∃ K > 0, AntilipschitzWith K ⇑f

Tactic:
· 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.Bochner.Basic

Goal state before:
pp: case neg
α : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
hE : CompleteSpace E
mα : MeasurableSpace α
f : α → E
hf : StronglyMeasurable f
a : α
s : Set α
hs : MeasurableSet s
inst✝ : Decidable (a ∈ s)
h✝ : a ∉ s
⊢ ∫ (x : α), f x ∂0 = 0

Tactic:
exact integral_zero_measure _

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

Goal state before:
pp: case neg
α : Type u_1
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
hE : CompleteSpace E
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSingletonClass α
f : α → E
a : α
s : Set α
inst✝ : Decidable (a ∈ s)
h✝ : a ∉ s
⊢ ∫ (x : α), f x ∂0 = 0

Tactic:
exact integral_zero_measure _

Goal state after:
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 𝕜
ι : Type u_1
inst✝ : Finite ι
v : Basis ι 𝕜 E
C : ℝ≥0
hC : C > 0
h : ∀ {u : E →L[𝕜] F} (M : ℝ≥0), (∀ (i : ι), ‖u (v i)‖₊ ≤ M) → ‖u‖₊ ≤ C * M
⊢ ∀ {u : E →L[𝕜] F} {M : ℝ}, 0 ≤ M → (∀ (i : ι), ‖u (v i)‖ ≤ M) → ‖u‖ ≤ ↑C * M

Tactic:
intro u M hM H

Goal state after:
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type v
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type w
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : CompleteSpace 𝕜
ι : Type u_1
inst✝ : Finite ι
v : Basis ι 𝕜 E
C : ℝ≥0
hC : C > 0
h : ∀ {u : E →L[𝕜] F} (M : ℝ≥0), (∀ (i : ι), ‖u (v i)‖₊ ≤ M) → ‖u‖₊ ≤ C * M
u : E →L[𝕜] F
M : ℝ
hM : 0 ≤ M
H : ∀ (i : ι), ‖u (v i)‖ ≤ M
⊢ ‖u‖ ≤ ↑C * M
Module: Mathlib.Topology.ContinuousMap.Bounded.Normed

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : SeminormedAddCommGroup β
f : α →ᵇ β
⊢ ‖f.normComp‖ = ‖f‖

Tactic:
by
  simp only [norm_eq, coe_normComp, norm_norm, Function.comp]

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

Goal state before:
pp: F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
β : Type u_6
m m0 : MeasurableSpace β
μ : Measure β
hm : m ≤ m0
f : β →ₛ F
hf_int : Integrable (⇑f) μ
⊢ ∫ (x : β), (SimpleFunc.toLargerSpace hm f) x ∂μ = ∑ x ∈ f.range, μ.real (⇑(SimpleFunc.toLargerSpace hm f) ⁻¹' {x}) • x

Tactic:
rw [SimpleFunc.integral_eq_sum _ hf_int]

Goal state after:
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
β : Type u_6
m m0 : MeasurableSpace β
μ : Measure β
hm : m ≤ m0
f : β →ₛ F
hf_int : Integrable (⇑f) μ
⊢ ∑ x ∈ (SimpleFunc.toLargerSpace hm f).range, μ.real (⇑(SimpleFunc.toLargerSpace hm f) ⁻¹' {x}) • x =
    ∑ x ∈ f.range, μ.real (⇑(SimpleFunc.toLargerSpace hm f) ⁻¹' {x}) • x
Module: Mathlib.Topology.MetricSpace.ThickenedIndicator

Goal state before:
pp: case inl
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
E : Set α
x y : α
h : infEDist x E ≤ infEDist y E
hle : infEDist x E / ENNReal.ofReal δ ≤ 1
⊢ 1 - infEDist y E / ENNReal.ofReal δ ≤ 1 - infEDist x E / ENNReal.ofReal δ

Tactic:
ENNReal.sub_le_sub_iff_left hle (by simp)

Goal state after:
case inl
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
E : Set α
x y : α
h : infEDist x E ≤ infEDist y E
hle : infEDist x E / ENNReal.ofReal δ ≤ 1
⊢ infEDist x E / ENNReal.ofReal δ ≤ infEDist y E / ENNReal.ofReal δ
Module: Mathlib.MeasureTheory.Integral.SetToL1

Goal state before:
pp: case pos.h_add
α : 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' : ℝ
μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ∞
hμ'_le : μ' ≤ c' • μ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ' T C'
f : α → E
hfμ : Integrable f μ
hF : CompleteSpace F
h_int : ∀ (g : α → E), Integrable g μ → Integrable g μ'
f₂ g₂ : α → E
a✝ : Disjoint (Function.support f₂) (Function.support g₂)
hf₂ : Integrable f₂ μ
hg₂ : Integrable g₂ μ
⊢ setToFun μ T hT f₂ = setToFun μ' T hT' f₂ →
    setToFun μ T hT g₂ = setToFun μ' T hT' g₂ → setToFun μ T hT (f₂ + g₂) = setToFun μ' T hT' (f₂ + g₂)

Tactic:
h_eq_f

Goal state after:
case pos.h_add
α : 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' : ℝ
μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ∞
hμ'_le : μ' ≤ c' • μ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ' T C'
f : α → E
hfμ : Integrable f μ
hF : CompleteSpace F
h_int : ∀ (g : α → E), Integrable g μ → Integrable g μ'
f₂ g₂ : α → E
a✝ : Disjoint (Function.support f₂) (Function.support g₂)
hf₂ : Integrable f₂ μ
hg₂ : Integrable g₂ μ
h_eq_f : setToFun μ T hT f₂ = setToFun μ' T hT' f₂
⊢ setToFun μ T hT g₂ = setToFun μ' T hT' g₂ → setToFun μ T hT (f₂ + g₂) = setToFun μ' T hT' (f₂ + g₂)
Module: Mathlib.Topology.Order.LeftRightLim

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : T2Space β
f : α → β
a : α
hf : ContinuousWithinAt f (Iic a) a
h' : 𝓝[<] a = ⊥
⊢ leftLim f a = f a

pp: case inr
α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : T2Space β
f : α → β
a : α
hf : ContinuousWithinAt f (Iic a) a
h' : (𝓝[<] a).NeBot
⊢ leftLim f a = f a

Tactic:
· simp [leftLim_eq_of_eq_bot f h']

Goal state after:
case inr
α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : T2Space β
f : α → β
a : α
hf : ContinuousWithinAt f (Iic a) a
h' : (𝓝[<] a).NeBot
⊢ leftLim f a = f a
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
⊢ leftLim f x ≤ f y

Tactic:
let : TopologicalSpace α := Preorder.topology α

Goal state after:
α : 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 α
⊢ 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 y : α
h : x < y
⊢ f x ≤ leftLim f y

Tactic:
let : TopologicalSpace α := Preorder.topology α

Goal state after:
α : 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 α
⊢ f x ≤ leftLim 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 y : α
h : x < y
⊢ rightLim f x ≤ leftLim f y

Tactic:
let : TopologicalSpace α := Preorder.topology α

Goal state after:
α : 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 α
⊢ rightLim f x ≤ leftLim f y
Module: Mathlib.MeasureTheory.Measure.Stieltjes

Goal state before:
pp: R : Type u_1
inst✝ : LinearOrder R
a b c : R
hc : a < c
right✝ : c ≤ b
hc' : c ∈ botSet
⊢ False

Tactic:
exact (hc' a).not_gt hc

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 : ℝ
hT : DominatedFinMeasAdditive μ T C
ι : Type u_7
l : Filter ι
inst✝¹ : l.IsCountablyGenerated
F : ι → α → E
inst✝ : IsFiniteMeasure μ
f : α → E
h_meas : ∀ᶠ (n : ι) in l, AEStronglyMeasurable (F n) μ
h_bound : ∃ C, ∀ᶠ (n : ι) in l, ∀ᵐ (ω : α) ∂μ, ‖F n ω‖ ≤ C
h_lim : ∀ᵐ (ω : α) ∂μ, Tendsto (fun n ↦ F n ω) l (𝓝 (f ω))
⊢ Tendsto (fun n ↦ setToFun μ T hT (F n)) l (𝓝 (setToFun μ T hT f))

Tactic:
by
  obtain ⟨c, h_boundc⟩ := h_bound
  let C : α → ℝ := (fun _ => c)
  exact tendsto_setToFun_filter_of_dominated_convergence hT
    C h_meas h_boundc (integrable_const c) h_lim

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
c : R
t : Set R
this : Nonempty R
a b : R
h : t \ botSet ⊆ Ioc a b
⊢ f.length (t ∩ Ioi c) + f.length (t \ Ioi c) ≤ ofReal (↑f b - ↑f a)

Tactic:
rw [← length_sdiff_botSet, inter_sdiff_right_comm, ← length_sdiff_botSet (s := t \ Ioi c),
    sdiff_sdiff_comm]

Goal state after:
R : Type u_1
inst✝¹ : LinearOrder R
inst✝ : TopologicalSpace R
f : StieltjesFunction R
c : R
t : Set R
this : Nonempty R
a b : R
h : t \ botSet ⊆ Ioc a b
⊢ f.length (t \ botSet ∩ Ioi c) + f.length ((t \ botSet) \ Ioi c) ≤ ofReal (↑f b - ↑f a)
Module: Mathlib.MeasureTheory.Measure.Stieltjes

Goal state before:
pp: R : Type u_1
inst✝¹ : LinearOrder R
inst✝ : TopologicalSpace R
f : StieltjesFunction R
c : R
t : Set R
this : Nonempty R
a b : R
h : t \ botSet ⊆ Ioc a b
⊢ f.length (Ioc a b ∩ Ioi c) + f.length (Ioc a b \ Ioi c) ≤ ofReal (↑f b - ↑f a)

Tactic:
rcases le_total a c with hac | hac <;> rcases le_total b c with hbc | hbc

Goal state after:
case inl.inl
R : Type u_1
inst✝¹ : LinearOrder R
inst✝ : TopologicalSpace R
f : StieltjesFunction R
c : R
t : Set R
this : Nonempty R
a b : R
h : t \ botSet ⊆ Ioc a b
hac : a ≤ c
hbc : b ≤ c
⊢ f.length (Ioc a b ∩ Ioi c) + f.length (Ioc a b \ Ioi c) ≤ ofReal (↑f b - ↑f a)

case inl.inr
R : Type u_1
inst✝¹ : LinearOrder R
inst✝ : TopologicalSpace R
f : StieltjesFunction R
c : R
t : Set R
this : Nonempty R
a b : R
h : t \ botSet ⊆ Ioc a b
hac : a ≤ c
hbc : c ≤ b
⊢ f.length (Ioc a b ∩ Ioi c) + f.length (Ioc a b \ Ioi c) ≤ ofReal (↑f b - ↑f a)

case inr.inl
R : Type u_1
inst✝¹ : LinearOrder R
inst✝ : TopologicalSpace R
f : StieltjesFunction R
c : R
t : Set R
this : Nonempty R
a b : R
h : t \ botSet ⊆ Ioc a b
hac : c ≤ a
hbc : b ≤ c
⊢ f.length (Ioc a b ∩ Ioi c) + f.length (Ioc a b \ Ioi c) ≤ ofReal (↑f b - ↑f a)

case inr.inr
R : Type u_1
inst✝¹ : LinearOrder R
inst✝ : TopologicalSpace R
f : StieltjesFunction R
c : R
t : Set R
this : Nonempty R
a b : R
h : t \ botSet ⊆ Ioc a b
hac : c ≤ a
hbc : c ≤ b
⊢ f.length (Ioc a b ∩ Ioi c) + f.length (Ioc a b \ Ioi c) ≤ ofReal (↑f b - ↑f a)
Module: Mathlib.MeasureTheory.Group.FundamentalDomain

Goal state before:
pp: G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
inst✝⁵ : Group G
inst✝⁴ : Group H
inst✝³ : MulAction G α
inst✝² : MeasurableSpace α
inst✝¹ : MulAction H β
inst✝ : MeasurableSpace β
s : Set α
μ : Measure α
ν : Measure β
h : IsFundamentalDomain G s μ
f : α ≃ β
hf : QuasiMeasurePreserving (⇑f.symm) ν μ
e : H ≃ G
hef : ∀ (g : H), Semiconj (⇑f) (fun x ↦ e g • x) fun x ↦ g • x
g : G
x : α
⊢ f.symm ((fun x ↦ e.symm g • x) (f x)) = (fun x ↦ g • x) (f.symm (f x))

Tactic:
rw [← hef _ _, f.symm_apply_apply, f.symm_apply_apply, e.apply_symm_apply]

Goal state after: