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

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
ι : Type u_5
m : MeasurableSpace α
inst✝³ : TopologicalSpace β
inst✝² : PseudoMetrizableSpace β
u : Filter ι
inst✝¹ : u.NeBot
inst✝ : u.IsCountablyGenerated
f : ι → α → β
g : α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
lim : Tendsto f u (𝓝 g)
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
⊢ IsSeparable (range g)

Tactic:
·

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
ι : Type u_5
m : MeasurableSpace α
inst✝³ : TopologicalSpace β
inst✝² : PseudoMetrizableSpace β
u : Filter ι
inst✝¹ : u.NeBot
inst✝ : u.IsCountablyGenerated
f : ι → α → β
g : α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
lim : Tendsto f u (𝓝 g)
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
⊢ IsSeparable (range g)
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (i : β), AEMeasurable (f i) μ
⊢ ⨆ b, ∫⁻ (a : α), ∑ i ∈ b, f i a ∂μ = ⨆ s, ∑ i ∈ s, ∫⁻ (a : α), f i a ∂μ

pp: case hf
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (i : β), AEMeasurable (f i) μ
⊢ ∀ (b : Finset β), AEMeasurable (fun a ↦ ∑ i ∈ b, f i a) μ

pp: case h_directed
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (i : β), AEMeasurable (f i) μ
⊢ Directed (fun x1 x2 ↦ x1 ≤ x2) fun s a ↦ ∑ i ∈ s, f i a

Tactic:
·

Goal state after:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (i : β), AEMeasurable (f i) μ
⊢ ⨆ b, ∫⁻ (a : α), ∑ i ∈ b, f i a ∂μ = ⨆ s, ∑ i ∈ s, ∫⁻ (a : α), f i a ∂μ
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add

Goal state before:
pp: case hf
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (i : β), AEMeasurable (f i) μ
⊢ ∀ (b : Finset β), AEMeasurable (fun a ↦ ∑ i ∈ b, f i a) μ

pp: case h_directed
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (i : β), AEMeasurable (f i) μ
⊢ Directed (fun x1 x2 ↦ x1 ≤ x2) fun s a ↦ ∑ i ∈ s, f i a

Tactic:
·

Goal state after:
case hf
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (i : β), AEMeasurable (f i) μ
⊢ ∀ (b : Finset β), AEMeasurable (fun a ↦ ∑ i ∈ b, f i a) μ
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add

Goal state before:
pp: case h_directed
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (i : β), AEMeasurable (f i) μ
⊢ Directed (fun x1 x2 ↦ x1 ≤ x2) fun s a ↦ ∑ i ∈ s, f i a

Tactic:
·

Goal state after:
case h_directed
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (i : β), AEMeasurable (f i) μ
⊢ Directed (fun x1 x2 ↦ x1 ≤ x2) fun s a ↦ ∑ i ∈ s, f i a
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add

Goal state before:
pp: case h.left
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (i : β), AEMeasurable (f i) μ
s t : Finset β
⊢ (fun x1 x2 ↦ x1 ≤ x2) ((fun s a ↦ ∑ i ∈ s, f i a) s) ((fun s a ↦ ∑ i ∈ s, f i a) (s ∪ t))

pp: case h.right
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (i : β), AEMeasurable (f i) μ
s t : Finset β
⊢ (fun x1 x2 ↦ x1 ≤ x2) ((fun s a ↦ ∑ i ∈ s, f i a) t) ((fun s a ↦ ∑ i ∈ s, f i a) (s ∪ t))

Tactic:
·

Goal state after:
case h.left
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (i : β), AEMeasurable (f i) μ
s t : Finset β
⊢ (fun x1 x2 ↦ x1 ≤ x2) ((fun s a ↦ ∑ i ∈ s, f i a) s) ((fun s a ↦ ∑ i ∈ s, f i a) (s ∪ t))
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add

Goal state before:
pp: case h.right
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (i : β), AEMeasurable (f i) μ
s t : Finset β
⊢ (fun x1 x2 ↦ x1 ≤ x2) ((fun s a ↦ ∑ i ∈ s, f i a) t) ((fun s a ↦ ∑ i ∈ s, f i a) (s ∪ t))

Tactic:
·

Goal state after:
case h.right
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (i : β), AEMeasurable (f i) μ
s t : Finset β
⊢ (fun x1 x2 ↦ x1 ≤ x2) ((fun s a ↦ ∑ i ∈ s, f i a) t) ((fun s a ↦ ∑ i ∈ s, f i a) (s ∪ t))
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hf : Measurable f
⊢ ⨆ n, ∫⁻ (a : α), (const α r * eapprox f n) a ∂μ = ⨆ n, r * (eapprox f n).lintegral μ

pp: case hf
α : Type u_1
m : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hf : Measurable f
⊢ ∀ (n : ℕ), Measurable ⇑(const α r * eapprox f n)

pp: case h_mono
α : Type u_1
m : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hf : Measurable f
⊢ Monotone fun n ↦ ⇑(const α r * eapprox f n)

Tactic:
·

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hf : Measurable f
⊢ ⨆ n, ∫⁻ (a : α), (const α r * eapprox f n) a ∂μ = ⨆ n, r * (eapprox f n).lintegral μ
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add

Goal state before:
pp: case hf
α : Type u_1
m : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hf : Measurable f
⊢ ∀ (n : ℕ), Measurable ⇑(const α r * eapprox f n)

pp: case h_mono
α : Type u_1
m : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hf : Measurable f
⊢ Monotone fun n ↦ ⇑(const α r * eapprox f n)

Tactic:
·

Goal state after:
case hf
α : Type u_1
m : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hf : Measurable f
⊢ ∀ (n : ℕ), Measurable ⇑(const α r * eapprox f n)
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add

Goal state before:
pp: case h_mono
α : Type u_1
m : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hf : Measurable f
⊢ Monotone fun n ↦ ⇑(const α r * eapprox f n)

Tactic:
·

Goal state after:
case h_mono
α : Type u_1
m : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hf : Measurable f
⊢ Monotone fun n ↦ ⇑(const α r * eapprox f n)
Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion

Goal state before:
pp: case neg
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝ : IsFiniteMeasure ν
n : ℕ
hC_lt : ⨆ s, ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), ν s ≤ 1 / ↑n
⊢ ∃ t,
    MeasurableSet t ∧
      SigmaFinite (μ.restrict t) ∧
        (⨆ s, ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), ν s) - 1 / ↑n ≤ ν t

Tactic:
·

Goal state after:
case neg
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝ : IsFiniteMeasure ν
n : ℕ
hC_lt : ⨆ s, ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), ν s ≤ 1 / ↑n
⊢ ∃ t,
    MeasurableSet t ∧
      SigmaFinite (μ.restrict t) ∧
        (⨆ s, ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), ν s) - 1 / ↑n ≤ ν t
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
f g : α → β
m : MeasurableSpace α
inst✝ : TopologicalSpace β
s : Set α
x✝ : DecidablePred fun x ↦ x ∈ s
hs : MeasurableSet s
hf : StronglyMeasurable f
hg : StronglyMeasurable g
x : α
hx : x ∈ s
⊢ Tendsto (fun n ↦ ((fun n ↦ SimpleFunc.piecewise s hs (hf.approx n) (hg.approx n)) n) x) atTop (𝓝 (s.piecewise f g x))

pp: case neg
α : Type u_1
β : Type u_2
f g : α → β
m : MeasurableSpace α
inst✝ : TopologicalSpace β
s : Set α
x✝ : DecidablePred fun x ↦ x ∈ s
hs : MeasurableSet s
hf : StronglyMeasurable f
hg : StronglyMeasurable g
x : α
hx : x ∉ s
⊢ Tendsto (fun n ↦ ((fun n ↦ SimpleFunc.piecewise s hs (hf.approx n) (hg.approx n)) n) x) atTop (𝓝 (s.piecewise f g x))

Tactic:
·

Goal state after:
case pos
α : Type u_1
β : Type u_2
f g : α → β
m : MeasurableSpace α
inst✝ : TopologicalSpace β
s : Set α
x✝ : DecidablePred fun x ↦ x ∈ s
hs : MeasurableSet s
hf : StronglyMeasurable f
hg : StronglyMeasurable g
x : α
hx : x ∈ s
⊢ Tendsto (fun n ↦ ((fun n ↦ SimpleFunc.piecewise s hs (hf.approx n) (hg.approx n)) n) x) atTop (𝓝 (s.piecewise f g x))
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
f g : α → β
m : MeasurableSpace α
inst✝ : TopologicalSpace β
s : Set α
x✝ : DecidablePred fun x ↦ x ∈ s
hs : MeasurableSet s
hf : StronglyMeasurable f
hg : StronglyMeasurable g
x : α
hx : x ∉ s
⊢ Tendsto (fun n ↦ ((fun n ↦ SimpleFunc.piecewise s hs (hf.approx n) (hg.approx n)) n) x) atTop (𝓝 (s.piecewise f g x))

Tactic:
·

Goal state after:
case neg
α : Type u_1
β : Type u_2
f g : α → β
m : MeasurableSpace α
inst✝ : TopologicalSpace β
s : Set α
x✝ : DecidablePred fun x ↦ x ∈ s
hs : MeasurableSet s
hf : StronglyMeasurable f
hg : StronglyMeasurable g
x : α
hx : x ∉ s
⊢ Tendsto (fun n ↦ ((fun n ↦ SimpleFunc.piecewise s hs (hf.approx n) (hg.approx n)) n) x) atTop (𝓝 (s.piecewise f g x))
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
s : Set α
m : MeasurableSpace α
inst✝¹ : TopologicalSpace β
inst✝ : (x : α) → Decidable (x ∈ s)
f : ↑s → β
hf : StronglyMeasurable f
g : ↑sᶜ → β
hg : StronglyMeasurable g
hs : MeasurableSet s
x : α
hx : x ∈ s
⊢ Tendsto (fun n ↦ ((fun n ↦ SimpleFunc.dite s hs (hf.approx n) (hg.approx n)) n) x) atTop
    (𝓝 ((fun x ↦ if hx : x ∈ s then f ⟨x, hx⟩ else g ⟨x, hx⟩) x))

pp: case neg
α : Type u_1
β : Type u_2
s : Set α
m : MeasurableSpace α
inst✝¹ : TopologicalSpace β
inst✝ : (x : α) → Decidable (x ∈ s)
f : ↑s → β
hf : StronglyMeasurable f
g : ↑sᶜ → β
hg : StronglyMeasurable g
hs : MeasurableSet s
x : α
hx : x ∉ s
⊢ Tendsto (fun n ↦ ((fun n ↦ SimpleFunc.dite s hs (hf.approx n) (hg.approx n)) n) x) atTop
    (𝓝 ((fun x ↦ if hx : x ∈ s then f ⟨x, hx⟩ else g ⟨x, hx⟩) x))

Tactic:
·

Goal state after:
case pos
α : Type u_1
β : Type u_2
s : Set α
m : MeasurableSpace α
inst✝¹ : TopologicalSpace β
inst✝ : (x : α) → Decidable (x ∈ s)
f : ↑s → β
hf : StronglyMeasurable f
g : ↑sᶜ → β
hg : StronglyMeasurable g
hs : MeasurableSet s
x : α
hx : x ∈ s
⊢ Tendsto (fun n ↦ ((fun n ↦ SimpleFunc.dite s hs (hf.approx n) (hg.approx n)) n) x) atTop
    (𝓝 ((fun x ↦ if hx : x ∈ s then f ⟨x, hx⟩ else g ⟨x, hx⟩) x))
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
s : Set α
m : MeasurableSpace α
inst✝¹ : TopologicalSpace β
inst✝ : (x : α) → Decidable (x ∈ s)
f : ↑s → β
hf : StronglyMeasurable f
g : ↑sᶜ → β
hg : StronglyMeasurable g
hs : MeasurableSet s
x : α
hx : x ∉ s
⊢ Tendsto (fun n ↦ ((fun n ↦ SimpleFunc.dite s hs (hf.approx n) (hg.approx n)) n) x) atTop
    (𝓝 ((fun x ↦ if hx : x ∈ s then f ⟨x, hx⟩ else g ⟨x, hx⟩) x))

Tactic:
·

Goal state after:
case neg
α : Type u_1
β : Type u_2
s : Set α
m : MeasurableSpace α
inst✝¹ : TopologicalSpace β
inst✝ : (x : α) → Decidable (x ∈ s)
f : ↑s → β
hf : StronglyMeasurable f
g : ↑sᶜ → β
hg : StronglyMeasurable g
hs : MeasurableSet s
x : α
hx : x ∉ s
⊢ Tendsto (fun n ↦ ((fun n ↦ SimpleFunc.dite s hs (hf.approx n) (hg.approx n)) n) x) atTop
    (𝓝 ((fun x ↦ if hx : x ∈ s then f ⟨x, hx⟩ else g ⟨x, hx⟩) x))
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add

Goal state before:
pp: case pos
α : Type u_1
m : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hr : r ≠ ∞
h : r = 0
⊢ ∫⁻ (a : α), r * f a ∂μ = r * ∫⁻ (a : α), f a ∂μ

pp: case neg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hr : r ≠ ∞
h : ¬r = 0
⊢ ∫⁻ (a : α), r * f a ∂μ = r * ∫⁻ (a : α), f a ∂μ

Tactic:
·

Goal state after:
case pos
α : Type u_1
m : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hr : r ≠ ∞
h : r = 0
⊢ ∫⁻ (a : α), r * f a ∂μ = r * ∫⁻ (a : α), f a ∂μ
Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion

Goal state before:
pp: case refine_1
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝ : IsFiniteMeasure ν
this : ∀ (n : ℕ), SigmaFinite (μ.restrict (μ.sigmaFiniteSetGE ν n))
f : ℕ × ℕ → Set α :=
  fun p ↦
    (μ.sigmaFiniteSetWRT' ν)ᶜ ∪ spanningSets (μ.restrict (μ.sigmaFiniteSetGE ν p.1)) p.2 ∩ μ.sigmaFiniteSetGE ν p.1
e : ℕ ≃ ℕ × ℕ := Nat.pairEquiv.symm
n : ℕ
⊢ (μ.restrict (μ.sigmaFiniteSetWRT' ν)) (f (e n)) < ∞

pp: case refine_2
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝ : IsFiniteMeasure ν
this : ∀ (n : ℕ), SigmaFinite (μ.restrict (μ.sigmaFiniteSetGE ν n))
f : ℕ × ℕ → Set α :=
  fun p ↦
    (μ.sigmaFiniteSetWRT' ν)ᶜ ∪ spanningSets (μ.restrict (μ.sigmaFiniteSetGE ν p.1)) p.2 ∩ μ.sigmaFiniteSetGE ν p.1
e : ℕ ≃ ℕ × ℕ := Nat.pairEquiv.symm
⊢ ⋃ i, f (e i) = Set.univ

Tactic:
·

Goal state after:
case refine_1
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝ : IsFiniteMeasure ν
this : ∀ (n : ℕ), SigmaFinite (μ.restrict (μ.sigmaFiniteSetGE ν n))
f : ℕ × ℕ → Set α :=
  fun p ↦
    (μ.sigmaFiniteSetWRT' ν)ᶜ ∪ spanningSets (μ.restrict (μ.sigmaFiniteSetGE ν p.1)) p.2 ∩ μ.sigmaFiniteSetGE ν p.1
e : ℕ ≃ ℕ × ℕ := Nat.pairEquiv.symm
n : ℕ
⊢ (μ.restrict (μ.sigmaFiniteSetWRT' ν)) (f (e n)) < ∞
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : MeasurableSpace α
inst✝⁴ : TopologicalSpace α
inst✝³ : OpensMeasurableSpace α
inst✝² : MeasurableSingletonClass α
inst✝¹ : TopologicalSpace β
inst✝ : PseudoMetrizableSpace β
h : SecondCountableTopologyEither α β
f : α → β
s : Set α
hf : ContinuousOn f s
hs : sᶜ.Countable
h's : MeasurableSet s
this : f = fun x ↦ if hx : x ∈ s then f ↑⟨x, hx⟩ else f ↑⟨x, hx⟩
⊢ StronglyMeasurable fun x ↦ f ↑x

pp: α : Type u_1
β : Type u_2
inst✝⁵ : MeasurableSpace α
inst✝⁴ : TopologicalSpace α
inst✝³ : OpensMeasurableSpace α
inst✝² : MeasurableSingletonClass α
inst✝¹ : TopologicalSpace β
inst✝ : PseudoMetrizableSpace β
h : SecondCountableTopologyEither α β
f : α → β
s : Set α
hf : ContinuousOn f s
hs : sᶜ.Countable
h's : MeasurableSet s
this : f = fun x ↦ if hx : x ∈ s then f ↑⟨x, hx⟩ else f ↑⟨x, hx⟩
⊢ StronglyMeasurable fun x ↦ f ↑x

Tactic:
·

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁵ : MeasurableSpace α
inst✝⁴ : TopologicalSpace α
inst✝³ : OpensMeasurableSpace α
inst✝² : MeasurableSingletonClass α
inst✝¹ : TopologicalSpace β
inst✝ : PseudoMetrizableSpace β
h : SecondCountableTopologyEither α β
f : α → β
s : Set α
hf : ContinuousOn f s
hs : sᶜ.Countable
h's : MeasurableSet s
this : f = fun x ↦ if hx : x ∈ s then f ↑⟨x, hx⟩ else f ↑⟨x, hx⟩
⊢ StronglyMeasurable fun x ↦ f ↑x
Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion

Goal state before:
pp: case refine_2
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝ : IsFiniteMeasure ν
this : ∀ (n : ℕ), SigmaFinite (μ.restrict (μ.sigmaFiniteSetGE ν n))
f : ℕ × ℕ → Set α :=
  fun p ↦
    (μ.sigmaFiniteSetWRT' ν)ᶜ ∪ spanningSets (μ.restrict (μ.sigmaFiniteSetGE ν p.1)) p.2 ∩ μ.sigmaFiniteSetGE ν p.1
e : ℕ ≃ ℕ × ℕ := Nat.pairEquiv.symm
⊢ ⋃ i, f (e i) = Set.univ

Tactic:
·

Goal state after:
case refine_2
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝ : IsFiniteMeasure ν
this : ∀ (n : ℕ), SigmaFinite (μ.restrict (μ.sigmaFiniteSetGE ν n))
f : ℕ × ℕ → Set α :=
  fun p ↦
    (μ.sigmaFiniteSetWRT' ν)ᶜ ∪ spanningSets (μ.restrict (μ.sigmaFiniteSetGE ν p.1)) p.2 ∩ μ.sigmaFiniteSetGE ν p.1
e : ℕ ≃ ℕ × ℕ := Nat.pairEquiv.symm
⊢ ⋃ i, f (e i) = Set.univ
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : MeasurableSpace α
inst✝⁴ : TopologicalSpace α
inst✝³ : OpensMeasurableSpace α
inst✝² : MeasurableSingletonClass α
inst✝¹ : TopologicalSpace β
inst✝ : PseudoMetrizableSpace β
h : SecondCountableTopologyEither α β
f : α → β
s : Set α
hf : ContinuousOn f s
hs : sᶜ.Countable
h's : MeasurableSet s
this : f = fun x ↦ if hx : x ∈ s then f ↑⟨x, hx⟩ else f ↑⟨x, hx⟩
⊢ StronglyMeasurable fun x ↦ f ↑x

Tactic:
·

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁵ : MeasurableSpace α
inst✝⁴ : TopologicalSpace α
inst✝³ : OpensMeasurableSpace α
inst✝² : MeasurableSingletonClass α
inst✝¹ : TopologicalSpace β
inst✝ : PseudoMetrizableSpace β
h : SecondCountableTopologyEither α β
f : α → β
s : Set α
hf : ContinuousOn f s
hs : sᶜ.Countable
h's : MeasurableSet s
this : f = fun x ↦ if hx : x ∈ s then f ↑⟨x, hx⟩ else f ↑⟨x, hx⟩
⊢ StronglyMeasurable fun x ↦ f ↑x
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add

Goal state before:
pp: case refine_1
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : α → ℝ≥0∞
hf : Measurable f
⊢ ∀ (c : ℝ≥0∞) ⦃s : Set α⦄,
    MeasurableSet s → ∫⁻ (a : α), s.indicator (fun x ↦ c) a ∂μ.trim hm = ∫⁻ (a : α), s.indicator (fun x ↦ c) a ∂μ

pp: case refine_2
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : α → ℝ≥0∞
hf : Measurable f
⊢ ∀ ⦃f g : α → ℝ≥0∞⦄,
    Disjoint (Function.support f) (Function.support g) →
      Measurable f →
        Measurable g →
          ∫⁻ (a : α), f a ∂μ.trim hm = ∫⁻ (a : α), f a ∂μ →
            ∫⁻ (a : α), g a ∂μ.trim hm = ∫⁻ (a : α), g a ∂μ →
              ∫⁻ (a : α), (f + g) a ∂μ.trim hm = ∫⁻ (a : α), (f + g) a ∂μ

pp: case refine_3
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : α → ℝ≥0∞
hf : Measurable f
⊢ ∀ ⦃f : ℕ → α → ℝ≥0∞⦄,
    (∀ (n : ℕ), Measurable (f n)) →
      Monotone f →
        (∀ (n : ℕ), ∫⁻ (a : α), f n a ∂μ.trim hm = ∫⁻ (a : α), f n a ∂μ) →
          ∫⁻ (a : α), (fun x ↦ ⨆ n, f n x) a ∂μ.trim hm = ∫⁻ (a : α), (fun x ↦ ⨆ n, f n x) a ∂μ

Tactic:
·

Goal state after:
case refine_1
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : α → ℝ≥0∞
hf : Measurable f
⊢ ∀ (c : ℝ≥0∞) ⦃s : Set α⦄,
    MeasurableSet s → ∫⁻ (a : α), s.indicator (fun x ↦ c) a ∂μ.trim hm = ∫⁻ (a : α), s.indicator (fun x ↦ c) a ∂μ
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add

Goal state before:
pp: case refine_2
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : α → ℝ≥0∞
hf : Measurable f
⊢ ∀ ⦃f g : α → ℝ≥0∞⦄,
    Disjoint (Function.support f) (Function.support g) →
      Measurable f →
        Measurable g →
          ∫⁻ (a : α), f a ∂μ.trim hm = ∫⁻ (a : α), f a ∂μ →
            ∫⁻ (a : α), g a ∂μ.trim hm = ∫⁻ (a : α), g a ∂μ →
              ∫⁻ (a : α), (f + g) a ∂μ.trim hm = ∫⁻ (a : α), (f + g) a ∂μ

pp: case refine_3
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : α → ℝ≥0∞
hf : Measurable f
⊢ ∀ ⦃f : ℕ → α → ℝ≥0∞⦄,
    (∀ (n : ℕ), Measurable (f n)) →
      Monotone f →
        (∀ (n : ℕ), ∫⁻ (a : α), f n a ∂μ.trim hm = ∫⁻ (a : α), f n a ∂μ) →
          ∫⁻ (a : α), (fun x ↦ ⨆ n, f n x) a ∂μ.trim hm = ∫⁻ (a : α), (fun x ↦ ⨆ n, f n x) a ∂μ

Tactic:
·

Goal state after:
case refine_2
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : α → ℝ≥0∞
hf : Measurable f
⊢ ∀ ⦃f g : α → ℝ≥0∞⦄,
    Disjoint (Function.support f) (Function.support g) →
      Measurable f →
        Measurable g →
          ∫⁻ (a : α), f a ∂μ.trim hm = ∫⁻ (a : α), f a ∂μ →
            ∫⁻ (a : α), g a ∂μ.trim hm = ∫⁻ (a : α), g a ∂μ →
              ∫⁻ (a : α), (f + g) a ∂μ.trim hm = ∫⁻ (a : α), (f + g) a ∂μ
Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion

Goal state before:
pp: case a
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝ : IsFiniteMeasure ν
⊢ ν (μ.sigmaFiniteSetWRT' ν) ≤ ⨆ s, ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), ν s

pp: case a
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝ : IsFiniteMeasure ν
⊢ ⨆ s, ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), ν s ≤ ν (μ.sigmaFiniteSetWRT' ν)

Tactic:
·

Goal state after:
case a
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝ : IsFiniteMeasure ν
⊢ ν (μ.sigmaFiniteSetWRT' ν) ≤ ⨆ s, ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), ν s
Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion

Goal state before:
pp: case a
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝ : IsFiniteMeasure ν
⊢ ν (μ.sigmaFiniteSetWRT' ν) ≤ ⨆ s, ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), ν s

Tactic:
refine (le_iSup (f := fun _ ↦ _)
      (sigmaFinite_restrict_sigmaFiniteSetWRT' μ ν)).trans ?_
    exact le_iSup₂ (f := fun s _ ↦ ⨆ (_ : SigmaFinite (μ.restrict s)), ν s) (μ.sigmaFiniteSetWRT' ν)
      measurableSet_sigmaFiniteSetWRT'

Goal state after:
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : α → γ
g' : γ → β
mα : MeasurableSpace α
mγ : MeasurableSpace γ
inst✝ : TopologicalSpace β
hg : MeasurableEmbedding g
hf : StronglyMeasurable f
hg' : StronglyMeasurable g'
x : γ
hx : ∃ y, g y = x
⊢ Tendsto (fun n ↦ ((fun n ↦ (hf.approx n).extend g hg (hg'.approx n)) n) x) atTop (𝓝 (Function.extend g f g' x))

pp: case neg
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : α → γ
g' : γ → β
mα : MeasurableSpace α
mγ : MeasurableSpace γ
inst✝ : TopologicalSpace β
hg : MeasurableEmbedding g
hf : StronglyMeasurable f
hg' : StronglyMeasurable g'
x : γ
hx : ¬∃ y, g y = x
⊢ Tendsto (fun n ↦ ((fun n ↦ (hf.approx n).extend g hg (hg'.approx n)) n) x) atTop (𝓝 (Function.extend g f g' x))

Tactic:
·

Goal state after:
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : α → γ
g' : γ → β
mα : MeasurableSpace α
mγ : MeasurableSpace γ
inst✝ : TopologicalSpace β
hg : MeasurableEmbedding g
hf : StronglyMeasurable f
hg' : StronglyMeasurable g'
x : γ
hx : ∃ y, g y = x
⊢ Tendsto (fun n ↦ ((fun n ↦ (hf.approx n).extend g hg (hg'.approx n)) n) x) atTop (𝓝 (Function.extend g f g' x))
Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion

Goal state before:
pp: case a
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝ : IsFiniteMeasure ν
⊢ ⨆ s, ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), ν s ≤ ν (μ.sigmaFiniteSetWRT' ν)

Tactic:
·

Goal state after:
case a
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝ : IsFiniteMeasure ν
⊢ ⨆ s, ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), ν s ≤ ν (μ.sigmaFiniteSetWRT' ν)
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : α → γ
g' : γ → β
mα : MeasurableSpace α
mγ : MeasurableSpace γ
inst✝ : TopologicalSpace β
hg : MeasurableEmbedding g
hf : StronglyMeasurable f
hg' : StronglyMeasurable g'
x : γ
hx : ¬∃ y, g y = x
⊢ Tendsto (fun n ↦ ((fun n ↦ (hf.approx n).extend g hg (hg'.approx n)) n) x) atTop (𝓝 (Function.extend g f g' x))

Tactic:
·

Goal state after:
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : α → γ
g' : γ → β
mα : MeasurableSpace α
mγ : MeasurableSpace γ
inst✝ : TopologicalSpace β
hg : MeasurableEmbedding g
hf : StronglyMeasurable f
hg' : StronglyMeasurable g'
x : γ
hx : ¬∃ y, g y = x
⊢ Tendsto (fun n ↦ ((fun n ↦ (hf.approx n).extend g hg (hg'.approx n)) n) x) atTop (𝓝 (Function.extend g f g' x))
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add

Goal state before:
pp: case refine_2
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f✝ : α → ℝ≥0∞
hf✝ : Measurable f✝
f g : α → ℝ≥0∞
a✝¹ : Disjoint (Function.support f) (Function.support g)
hf : Measurable f
a✝ : Measurable g
hf_prop : ∫⁻ (a : α), f a ∂μ.trim hm = ∫⁻ (a : α), f a ∂μ
hg_prop : ∫⁻ (a : α), g a ∂μ.trim hm = ∫⁻ (a : α), g a ∂μ
⊢ ∫⁻ (a : α), (f + g) a ∂μ.trim hm = ∫⁻ (a : α), (f + g) a ∂μ

Tactic:
have h_m := lintegral_add_left (μ := Measure.trim μ hm) hf g

Goal state after:
case refine_2
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f✝ : α → ℝ≥0∞
hf✝ : Measurable f✝
f g : α → ℝ≥0∞
a✝¹ : Disjoint (Function.support f) (Function.support g)
hf : Measurable f
a✝ : Measurable g
hf_prop : ∫⁻ (a : α), f a ∂μ.trim hm = ∫⁻ (a : α), f a ∂μ
hg_prop : ∫⁻ (a : α), g a ∂μ.trim hm = ∫⁻ (a : α), g a ∂μ
h_m : ∫⁻ (a : α), f a + g a ∂μ.trim hm = ∫⁻ (a : α), f a ∂μ.trim hm + ∫⁻ (a : α), g a ∂μ.trim hm
⊢ ∫⁻ (a : α), (f + g) a ∂μ.trim hm = ∫⁻ (a : α), (f + g) a ∂μ